--- a/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 09 09:02:54 2010 -0700
+++ b/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 09 21:51:01 2010 +0200
@@ -223,6 +223,13 @@
   shows "a \<sharp> ()"
   by (simp add: fresh_def supp_unit)
 
+lemma permute_eqvt_raw:
+  shows "p \<bullet> permute = permute"
+apply(simp add: expand_fun_eq permute_fun_def)
+apply(subst permute_eqvt)
+apply(simp)
+done
+
 section {* Equivariance automation *}
 
 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}
@@ -237,9 +244,7 @@
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  (*permute_eqvt commented out since it loops *)
   supp_eqvt fresh_eqvt
-  permute_pure
 
   (* datatypes *)
   permute_prod.simps append_eqvt rev_eqvt set_eqvt
@@ -251,6 +256,9 @@
 
   atom_eqvt add_perm_eqvt
 
+lemmas [eqvt_raw] =
+  permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) 
+
 thm eqvts
 thm eqvts_raw
 
@@ -274,31 +282,93 @@
   shows "p \<bullet> unpermute p x \<equiv> x"
   unfolding unpermute_def by simp
 
+ML {* @{const Trueprop} *}
+
 use "nominal_permeq.ML"
-
+setup Nominal_Permeq.setup
 
-lemma "p \<bullet> (A \<longrightarrow> B = C)"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) 
+method_setup perm_simp =
+ {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms))) *}
+ {* pushes permutations inside *}
+
+declare [[trace_eqvt = true]]
+
+lemma 
+  fixes B::"'a::pt"
+  shows "p \<bullet> (B = C)"
+apply(perm_simp)
 oops
 
-lemma "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+lemma 
+  fixes B::"bool"
+  shows "p \<bullet> (B = C)"
+apply(perm_simp)
+oops
+
+lemma 
+  fixes B::"bool"
+  shows "p \<bullet> (A \<longrightarrow> B = C)"
+apply (perm_simp) 
+oops
+
+lemma 
+  shows "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo"
+apply(perm_simp)
+oops
+
+lemma 
+  shows "p \<bullet> (\<lambda>B::bool. A \<longrightarrow> (B = C)) = foo"
+apply (perm_simp)
+oops
+
+lemma 
+  shows "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
+apply (perm_simp)
 oops
 
-lemma "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+lemma 
+  shows "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
+apply (perm_simp)
+oops
+
+lemma 
+  fixes p q::"perm"
+  and   x::"'a::pt"
+  shows "p \<bullet> (q \<bullet> x) = foo"
+apply(perm_simp)
+oops
+
+lemma 
+  fixes p q r::"perm"
+  and   x::"'a::pt"
+  shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
+apply(perm_simp)
 oops
 
-lemma "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+lemma 
+  fixes p r::"perm"
+  shows "p \<bullet> (\<lambda>q::perm. q \<bullet> (r \<bullet> x)) = foo"
+apply (perm_simp)
 oops
 
-lemma "p \<bullet> (\<lambda>q. q \<bullet> (r \<bullet> x)) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+lemma 
+  fixes p q r::"perm"
+  and   x::"'a::pt"
+  shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
+apply(perm_simp)
 oops
 
-lemma "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+lemma 
+  fixes C D::"bool"
+  shows "B (p \<bullet> (C = D))"
+apply(perm_simp)
+oops
+
+declare [[trace_eqvt = false]]
+
+text {* Problem: there is no raw eqvt-rule for The *}
+lemma "p \<bullet> (THE x. P x) = foo"
+apply(perm_simp)
 oops
 
 

--- a/Nominal-General/nominal_permeq.ML	Fri Apr 09 09:02:54 2010 -0700
+++ b/Nominal-General/nominal_permeq.ML	Fri Apr 09 21:51:01 2010 +0200
@@ -4,8 +4,9 @@
 
 signature NOMINAL_PERMEQ =
 sig
-  val eqvt_tac: Proof.context -> int -> tactic 
-
+  val eqvt_tac: Proof.context -> thm list -> int -> tactic 
+  val trace_eqvt: bool Config.T
+  val setup: theory -> theory
 end;
 
 (* TODO:
@@ -14,20 +15,40 @@
 
  - print a warning if for a constant no eqvt lemma is stored
 
- - there seems to be too much simplified in case of multiple 
-   permutations, like
-
-      p o q o r o x 
-
-   we usually only want the outermost permutation to "float" in
 *)
 
 
 structure Nominal_Permeq: NOMINAL_PERMEQ =
 struct
 
-local
+fun is_head_Trueprop trm = 
+  case (head_of trm) of 
+    @{const "Trueprop"} => true 
+  | _ => false 
+
+(* debugging infrastructure *)
+val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false);
+
+fun trace_enabled ctxt = Config.get ctxt trace_eqvt
 
+fun trace_conv ctxt conv ct =
+let
+  val result = conv ct
+  val _ = 
+    if trace_enabled ctxt andalso not (Thm.is_reflexive result) 
+    then  
+      let
+        val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result))
+        val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result))
+      in
+        warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) 
+      end
+    else ()
+in
+  result
+end;
+
+(* conversion for applications *)
 fun eqvt_apply_conv ctxt ct =
   case (term_of ct) of
     (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) =>
@@ -38,34 +59,45 @@
         val a = ctyp_of_term x;
         val b = ctyp_of_term t;
         val ty_insts = map SOME [b, a]
-        val term_insts = map SOME [p, f, x]
+        val term_insts = map SOME [p, f, x]                        
       in
         Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
       end
   | _ => Conv.no_conv ct
 
+(* conversion for lambdas *)
 fun eqvt_lambda_conv ctxt ct =
   case (term_of ct) of
     (Const (@{const_name "permute"}, _) $ _ $ Abs _) =>
       Conv.rewr_conv @{thm eqvt_lambda} ct
   | _ => Conv.no_conv ct
 
+
+(* main conversion *)
+fun eqvt_conv ctxt thms ctrm =
+let
+  val trm = term_of ctrm 
+  val _ = if trace_enabled ctxt andalso not (is_head_Trueprop trm)
+    then warning ("analysing " ^ Syntax.string_of_term ctxt trm) 
+    else ()
+  val wrapper = if trace_enabled ctxt then trace_conv ctxt else I			
 in
-
-fun eqvt_conv ctxt ct =
-  Conv.first_conv
-    [ Conv.rewr_conv @{thm eqvt_bound},
-      eqvt_apply_conv ctxt
-        then_conv Conv.comb_conv (eqvt_conv ctxt),
-      eqvt_lambda_conv ctxt
-        then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt,
+  Conv.first_conv (map wrapper
+    [ More_Conv.rewrs_conv thms,
+      Conv.rewr_conv @{thm eqvt_bound},
       More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt),
+      eqvt_apply_conv ctxt,
+      eqvt_lambda_conv ctxt,
+      More_Conv.rewrs_conv @{thms permute_pure[THEN eq_reflection]},
       Conv.all_conv
-    ] ct
-
-fun eqvt_tac ctxt = 
-  CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt)
-
+    ]) ctrm
 end
 
+
+fun eqvt_tac ctxt thms = 
+  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt thms) ctxt)
+
+val setup =
+  trace_eqvt_setup
+
 end; (* structure *)
\ No newline at end of file

--- a/Nominal-General/nominal_thmdecls.ML	Fri Apr 09 09:02:54 2010 -0700
+++ b/Nominal-General/nominal_thmdecls.ML	Fri Apr 09 21:51:01 2010 +0200
@@ -60,7 +60,18 @@
 val add_thm = EqvtData.map o Item_Net.update;
 val del_thm = EqvtData.map o Item_Net.remove;
 
-val add_raw_thm = EqvtRawData.map o Item_Net.update;
+fun is_equiv (Const ("==", _) $ _ $ _) = true
+  | is_equiv _ = false
+
+fun add_raw_thm thm = 
+let
+  val trm = prop_of thm
+  val _ = if is_equiv trm then () 
+    else raise THM ("Theorem must be a meta-equality", 0, [thm]) 
+in
+  (EqvtRawData.map o Item_Net.update) thm
+end
+
 val del_raw_thm = EqvtRawData.map o Item_Net.remove;
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
@@ -78,7 +89,7 @@
    rtac (thm RS @{thm trans}),
    rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
 
-(* transform equations into the required form *)
+(* transform equations into the "p o c = c"-form *)
 fun transform_eq ctxt thm lhs rhs = 
 let
   val (p, t) = dest_perm lhs

--- a/Nominal/Ex/ExCoreHaskell.thy	Fri Apr 09 09:02:54 2010 -0700
+++ b/Nominal/Ex/ExCoreHaskell.thy	Fri Apr 09 21:51:01 2010 +0200
@@ -5,6 +5,9 @@
 (* core haskell *)
 
 ML {* val _ = recursive := false *}
+(* this should not be a raw equivariant rule *)
+declare permute_pure[eqvt]
+
 
 atom_decl var
 atom_decl cvar
@@ -88,6 +91,7 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
+
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm

--- a/Nominal/Ex/Lambda.thy	Fri Apr 09 09:02:54 2010 -0700
+++ b/Nominal/Ex/Lambda.thy	Fri Apr 09 21:51:01 2010 +0200
@@ -4,12 +4,14 @@
 
 atom_decl name
 
-nominal_datatype lm =
-  Vr "name"
-| Ap "lm" "lm"
-| Lm x::"name" l::"lm"  bind x in l
+nominal_datatype lam =
+  Var "name"
+| App "lam" "lam"
+| Lam x::"name" l::"lam"  bind x in l
 
-lemmas supp_fn' = lm.fv[simplified lm.supp]
+lemmas supp_fn' = lam.fv[simplified lam.supp]
+
+section {* Strong Induction Principles*}
 
 (* 
   Old way of establishing strong induction
@@ -17,31 +19,31 @@
 *)
 lemma
   fixes c::"'a::fs"
-  assumes a1: "\<And>name c. P c (Vr name)"
-  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
-  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
-  shows "P c lm"
+  assumes a1: "\<And>name c. P c (Var name)"
+  and     a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
+  and     a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
+  shows "P c lam"
 proof -
-  have "\<And>p. P c (p \<bullet> lm)"
-    apply(induct lm arbitrary: c rule: lm.induct)
-    apply(simp only: lm.perm)
+  have "\<And>p. P c (p \<bullet> lam)"
+    apply(induct lam arbitrary: c rule: lam.induct)
+    apply(simp only: lam.perm)
     apply(rule a1)
-    apply(simp only: lm.perm)
+    apply(simp only: lam.perm)
     apply(rule a2)
     apply(assumption)
     apply(assumption)
-    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))")
+    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lam (p \<bullet> name) (p \<bullet> lam))")
     defer
     apply(simp add: fresh_def)
-    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
+    apply(rule_tac X="supp (c, Lam (p \<bullet> name) (p \<bullet> lam))" in obtain_at_base)
     apply(simp add: supp_Pair finite_supp)
     apply(blast)
     apply(erule exE)
-    apply(rule_tac t="p \<bullet> Lm name lm" and 
-                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
-    apply(simp del: lm.perm)
-    apply(subst lm.perm)
-    apply(subst (2) lm.perm)
+    apply(rule_tac t="p \<bullet> Lam name lam" and 
+                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lam name lam" in subst)
+    apply(simp del: lam.perm)
+    apply(subst lam.perm)
+    apply(subst (2) lam.perm)
     apply(rule flip_fresh_fresh)
     apply(simp add: fresh_def)
     apply(simp only: supp_fn')
@@ -53,8 +55,8 @@
     apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
     apply(simp)
     done
-  then have "P c (0 \<bullet> lm)" by blast
-  then show "P c lm" by simp
+  then have "P c (0 \<bullet> lam)" by blast
+  then show "P c lam" by simp
 qed
 
 (* 
@@ -63,25 +65,25 @@
 *)
 lemma
   fixes c::"'a::fs"
-  assumes a1: "\<And>name c. P c (Vr name)"
-  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
-  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
-  shows "P c lm"
+  assumes a1: "\<And>name c. P c (Var name)"
+  and     a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
+  and     a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
+  shows "P c lam"
 proof -
-  have "\<And>p. P c (p \<bullet> lm)"
-    apply(induct lm arbitrary: c rule: lm.induct)
-    apply(simp only: lm.perm)
+  have "\<And>p. P c (p \<bullet> lam)"
+    apply(induct lam arbitrary: c rule: lam.induct)
+    apply(simp only: lam.perm)
     apply(rule a1)
-    apply(simp only: lm.perm)
+    apply(simp only: lam.perm)
     apply(rule a2)
     apply(assumption)
     apply(assumption)
-    apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q")
+    apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lam name lam) \<sharp>* q")
     apply(erule exE)
-    apply(rule_tac t="p \<bullet> Lm name lm" and 
-                   s="q \<bullet> p \<bullet> Lm name lm" in subst)
+    apply(rule_tac t="p \<bullet> Lam name lam" and 
+                   s="q \<bullet> p \<bullet> Lam name lam" in subst)
     defer
-    apply(simp add: lm.perm)
+    apply(simp add: lam.perm)
     apply(rule a3)
     apply(simp add: eqvts fresh_star_def)
     apply(drule_tac x="q + p" in meta_spec)
@@ -90,15 +92,172 @@
     apply(simp add: finite_supp)
     apply(simp add: finite_supp)
     apply(simp add: finite_supp)
-    apply(simp only: lm.perm atom_eqvt)
+    apply(simp only: lam.perm atom_eqvt)
     apply(simp add: fresh_star_def fresh_def supp_fn')
     apply(rule supp_perm_eq)
     apply(simp)
     done
-  then have "P c (0 \<bullet> lm)" by blast
-  then show "P c lm" by simp
+  then have "P c (0 \<bullet> lam)" by blast
+  then show "P c lam" by simp
 qed
 
+section {* size function *}
+
+lemma size_eqvt_raw:
+  fixes t::"lam_raw"
+  shows "size (pi \<bullet> t)  = size t"
+  apply (induct rule: lam_raw.inducts)
+  apply simp_all
+  done
+
+instantiation lam :: size 
+begin
+
+quotient_definition
+  "size_lam :: lam \<Rightarrow> nat"
+is
+  "size :: lam_raw \<Rightarrow> nat"
+
+lemma size_rsp:
+  "alpha_lam_raw x y \<Longrightarrow> size x = size y"
+  apply (induct rule: alpha_lam_raw.inducts)
+  apply (simp_all only: lam_raw.size)
+  apply (simp_all only: alphas)
+  apply clarify
+  apply (simp_all only: size_eqvt_raw)
+  done
+
+lemma [quot_respect]:
+  "(alpha_lam_raw ===> op =) size size"
+  by (simp_all add: size_rsp)
+
+lemma [quot_preserve]:
+  "(rep_lam ---> id) size = size"
+  by (simp_all add: size_lam_def)
+
+instance
+  by default
+
+end
+
+lemmas size_lam[simp] = 
+  lam_raw.size(4)[quot_lifted]
+  lam_raw.size(5)[quot_lifted]
+  lam_raw.size(6)[quot_lifted]
+
+(* is this needed? *)
+lemma [measure_function]: 
+  "is_measure (size::lam\<Rightarrow>nat)" 
+  by (rule is_measure_trivial)
+
+section {* Matching *}
+
+definition
+  MATCH :: "('c::pt \<Rightarrow> (bool * 'a::pt * 'b::pt)) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+  "MATCH M d x \<equiv> if (\<exists>!r. \<exists>q. M q = (True, x, r)) then (THE r. \<exists>q. M q = (True, x, r)) else d"
+
+(*
+lemma MATCH_eqvt:
+  shows "p \<bullet> (MATCH M d x) = MATCH (p \<bullet> M) (p \<bullet> d) (p \<bullet> x)"
+unfolding MATCH_def
+apply(perm_simp the_eqvt)
+apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+apply(simp)
+thm eqvts_raw 
+apply(subst if_eqvt)
+apply(subst ex1_eqvt)
+apply(subst permute_fun_def)
+apply(subst ex_eqvt)
+apply(subst permute_fun_def)
+apply(subst eq_eqvt)
+apply(subst permute_fun_app_eq[where f="M"])
+apply(simp only: permute_minus_cancel)
+apply(subst permute_prod.simps)
+apply(subst permute_prod.simps)
+apply(simp only: permute_minus_cancel)
+apply(simp only: permute_bool_def)
+apply(simp)
+apply(subst ex1_eqvt)
+apply(subst permute_fun_def)
+apply(subst ex_eqvt)
+apply(subst permute_fun_def)
+apply(subst eq_eqvt)
+
+apply(simp only: eqvts)
+apply(simp)
+apply(subgoal_tac "(p \<bullet> (\<exists>!r. \<exists>q. M q = (True, x, r))) = (\<exists>!r. \<exists>q. (p \<bullet> M) q = (True, p \<bullet> x, r))")
+apply(drule sym)
+apply(simp)
+apply(rule impI)
+apply(simp add: perm_bool)
+apply(rule trans)
+apply(rule pt_the_eqvt[OF pta at])
+apply(assumption)
+apply(simp add: pt_ex_eqvt[OF pt at])
+apply(simp add: pt_eq_eqvt[OF ptb at])
+apply(rule cheat)
+apply(rule trans)
+apply(rule pt_ex1_eqvt)
+apply(rule pta)
+apply(rule at)
+apply(simp add: pt_ex_eqvt[OF pt at])
+apply(simp add: pt_eq_eqvt[OF ptb at])
+apply(subst pt_pi_rev[OF pta at])
+apply(subst pt_fun_app_eq[OF pt at])
+apply(subst pt_pi_rev[OF pt at])
+apply(simp)
+done
+
+lemma MATCH_cng:
+  assumes a: "M1 = M2" "d1 = d2"
+  shows "MATCH M1 d1 x = MATCH M2 d2 x"
+using a by simp
+
+lemma MATCH_eq:
+  assumes a: "t = l x" "G x" "\<And>x'. t = l x' \<Longrightarrow> G x' \<Longrightarrow> r x' = r x"
+  shows "MATCH (\<lambda>x. (G x, l x, r x)) d t = r x"
+using a
+unfolding MATCH_def
+apply(subst if_P)
+apply(rule_tac a="r x" in ex1I)
+apply(rule_tac x="x" in exI)
+apply(blast)
+apply(erule exE)
+apply(drule_tac x="q" in meta_spec)
+apply(auto)[1]
+apply(rule the_equality)
+apply(blast)
+apply(erule exE)
+apply(drule_tac x="q" in meta_spec)
+apply(auto)[1]
+done
+
+lemma MATCH_eq2:
+  assumes a: "t = l x1 x2" "G x1 x2" "\<And>x1' x2'. t = l x1' x2' \<Longrightarrow> G x1' x2' \<Longrightarrow> r x1' x2' = r x1 x2"
+  shows "MATCH (\<lambda>(x1,x2). (G x1 x2, l x1 x2, r x1 x2)) d t = r x1 x2"
+sorry
+
+lemma MATCH_neq:
+  assumes a: "\<And>x. t = l x \<Longrightarrow> G x \<Longrightarrow> False"
+  shows "MATCH (\<lambda>x. (G x, l x, r x)) d t = d"
+using a
+unfolding MATCH_def
+apply(subst if_not_P)
+apply(blast)
+apply(rule refl)
+done
+
+lemma MATCH_neq2:
+  assumes a: "\<And>x1 x2. t = l x1 x2 \<Longrightarrow> G x1 x2 \<Longrightarrow> False"
+  shows "MATCH (\<lambda>(x1,x2). (G x1 x2, l x1 x2, r x1 x2)) d t = d"
+using a
+unfolding MATCH_def
+apply(subst if_not_P)
+apply(auto)
+done
+*)
+
 end