# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268854962 -3600
# Node ID 4908db645f989100251da3073932943de87b6d89
# Parent  f970ca9b5bec4c81fc4e8d37085c77c17fa18dae# Parent  9923b2cee778496a649ad17bb074d1aab379d006
merged

diff -r f970ca9b5bec -r 4908db645f98 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Mar 17 20:42:22 2010 +0100
+++ b/Nominal/Abs.thy	Wed Mar 17 20:42:42 2010 +0100
@@ -87,33 +87,25 @@
   done
 
 lemma alpha_gen_compose_sym2:
-  assumes a: "(aa, (t1, t2)) \<approx>gen (\<lambda>(x11, x12) (x21, x22). R1 x11 x21 \<and> R1 x21 x11 \<and> R2 x12 x22 \<and> R2 x22 x12)
-  (\<lambda>(b, a). fb b \<union> fa a) pi (ab, (s1, s2))"
+  assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22).
+  (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
   and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
   and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(ab, (s1, s2)) \<approx>gen
- (\<lambda>x1 x2. (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) x1 x2 \<and> (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) x2 x1)
- (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, (t1, t2))"
- using a
-apply(simp add: alpha_gen)
-apply clarify
-apply (rule conjI)
+  shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
+  using a
+  apply(simp add: alpha_gen)
+  apply clarify
+  apply (rule conjI)
   apply(simp add: fresh_star_def fresh_minus_perm)
-apply (rule conjI)
-apply (rotate_tac 3)
-apply (drule_tac pi="- pi" in r1)
-apply simp
-apply (rule conjI)
-apply (rotate_tac -1)
-apply (drule_tac pi="- pi" in r2)
-apply simp
-apply (rule conjI)
-apply (drule_tac pi="- pi" in r1)
-apply simp
-apply (rule conjI)
-apply (drule_tac pi="- pi" in r2)
-apply simp_all
-done
+  apply (rule conjI)
+  apply (rotate_tac 3)
+  apply (drule_tac pi="- pi" in r1)
+  apply simp
+  apply (rule conjI)
+  apply (rotate_tac -1)
+  apply (drule_tac pi="- pi" in r2)
+  apply simp_all
+  done
 
 lemma alpha_gen_compose_trans:
   fixes pi pia
diff -r f970ca9b5bec -r 4908db645f98 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Mar 17 20:42:22 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 17 20:42:42 2010 +0100
@@ -609,10 +609,8 @@
   THEN_ALL_NEW
   split_conjs THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
-  (rtac @{thm alpha_gen_compose_sym} THEN' RANGE [
-    (asm_full_simp_tac (HOL_ss addsimps @{thms plus_perm_eq})),
-    (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
-  ])
+  TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW
+  (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
 *}
 
 ML {*
diff -r f970ca9b5bec -r 4908db645f98 Nominal/Term1.thy
--- a/Nominal/Term1.thy	Wed Mar 17 20:42:22 2010 +0100
+++ b/Nominal/Term1.thy	Wed Mar 17 20:42:42 2010 +0100
@@ -12,9 +12,9 @@
 | rLm1 "name" "rtrm1"        --"name is bound in trm1"
 | rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"
 and bp =
-(*  BUnit*)
- BVr "name"
-(*| BPr "bp" "bp"*)
+  BUnit
+| BVr "name"
+| BPr "bp" "bp"
 
 print_theorems
 
@@ -23,9 +23,9 @@
 primrec 
   bv1
 where
-(*  "bv1 (BUnit) = {}"*)
- "bv1 (BVr x) = {atom x}"
-(*| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"*)
+  "bv1 (BUnit) = {}"
+| "bv1 (BVr x) = {atom x}"
+| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 
 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *}
 thm permute_rtrm1_permute_bp.simps
@@ -33,7 +33,7 @@
 local_setup {*
   snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1")
   [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, true), 0, 2)]],
-  [[](*, [], []*)]] [(@{term bv1}, 1, [(*[],*) [0](*, [0, 1]*)])] *}
+  [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *}
 
 notation
   alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
@@ -52,8 +52,7 @@
 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps} @{context})
 *}
 
-(*
-local_setup {*
+(*local_setup {*
 snd o build_eqvts @{binding fv_rtrm1_fv_bv1_eqvt} [@{term fv_rtrm1}, @{term fv_bv1}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bv1.simps permute_rtrm1_permute_bp.simps} @{context})
 *}
 print_theorems
@@ -64,16 +63,9 @@
 print_theorems
 *)
 
-lemma alpha1_eqvt: 
-  "(rtrm1 \<approx>1 rtrm1a \<longrightarrow> (p \<bullet> rtrm1) \<approx>1 (p \<bullet> rtrm1a)) \<and> 
-   (bp \<approx>1b bpa \<longrightarrow> (p \<bullet> bp) \<approx>1b (p \<bullet> bpa)) \<and>
-   (alpha_bv1 a b c \<longrightarrow> alpha_bv1 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))"
-by (tactic {* alpha_eqvt_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms alpha1_inj permute_rtrm1_permute_bp.simps} @{context} 1 *})
-
-(*
 local_setup {*
 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []),
-build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} ctxt) ctxt)) *}*)
+build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}, @{term alpha_bv1}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms permute_rtrm1_permute_bp.simps alpha1_inj} ctxt 1) ctxt) ctxt)) *}
 
 lemma alpha1_eqvt_proper[eqvt]:
   "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))"
@@ -92,6 +84,10 @@
 done
 thm eqvts_raw(1)
 
+lemma "(b \<approx>1 a \<longrightarrow> a \<approx>1 b) \<and> (x \<approx>1b y \<longrightarrow> y \<approx>1b x) \<and> (alpha_bv1 x y \<longrightarrow> alpha_bv1 y x)"
+apply (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} @{context} 1 *})
+done
+
 lemma alpha1_equivp:
   "equivp alpha_rtrm1"
   "equivp alpha_bp"
@@ -99,9 +95,8 @@
 
 (*
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
-  (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}
-thm alpha1_equivp
-*)
+  (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}, @{term alpha_bv1}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}
+thm alpha1_equivp*)
 
 local_setup  {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))]
   (rtac @{thm alpha1_equivp(1)} 1) *}
@@ -138,17 +133,17 @@
 lemmas
     permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]
 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
-and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt(1)[quot_lifted]
-and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt[quot_lifted]
+and alpha1_INJ = alpha1_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen]
 
 lemma supports:
   "(supp (atom x)) supports (Vr1 x)"
   "(supp t \<union> supp s) supports (Ap1 t s)"
   "(supp (atom x) \<union> supp t) supports (Lm1 x t)"
   "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)"
-(*  "{} supports BUnit"*)
+  "{} supports BUnit"
   "(supp (atom x)) supports (BVr x)"
-(*  "(supp a \<union> supp b) supports (BPr a b)"*)
+  "(supp a \<union> supp b) supports (BPr a b)"
 apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *})
 done
 
@@ -197,84 +192,32 @@
 apply (blast)+
 done
 
-lemma "(Abs bs (x, x') = Abs cs (y, y')) = (\<exists>p. (bs, x) \<approx>gen op = supp p (cs, y) \<and> (bs, x') \<approx>gen op = supp p (cs, y'))"
-thm Abs_eq_iff
-apply (simp add: Abs_eq_iff)
-apply (rule arg_cong[of _ _ "Ex"])
-apply (rule ext)
-apply (simp only: alpha_gen)
-apply (simp only: supp_Pair eqvts)
-apply rule
-apply (erule conjE)+
-oops
-
-lemma "(f (p \<bullet> bp), p \<bullet> bp) \<approx>gen op = f pi (f bp, bp) = False"
-apply (simp add: alpha_gen fresh_star_def)
-oops
-
-(* TODO: permute_ABS should be in eqvt? *)
-
 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
 
-lemma "
-{a\<Colon>atom. infinite ({b\<Colon>atom. \<not> (\<exists>pi\<Colon>perm. P pi a b \<and> Q pi a b)})} =
-{a\<Colon>atom. infinite {b\<Colon>atom. \<not> (\<exists>p\<Colon>perm. P p a b)}} \<union>
-{a\<Colon>atom. infinite {b\<Colon>atom. \<not> (\<exists>p\<Colon>perm. Q p a b)}}"
-oops
-
 lemma inf_or: "(infinite x \<or> infinite y) = infinite (x \<union> y)"
 by (simp add: finite_Un)
 
-
-
 lemma supp_fv_let:
   assumes sa : "fv_bp bp = supp bp"
-  shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb\<rbrakk>
-       \<Longrightarrow> supp (Lt1 bp ta tb) = fv_trm1 (Lt1 bp ta tb)"
-apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv])
-apply simp
+  shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\<rbrakk>
+       \<Longrightarrow> supp (Lt1 bp ta tb) = supp ta \<union> (supp (bp, tb) - supp bp)"
 apply(fold supp_Abs)
-apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric])
+apply(simp (no_asm) only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric])
 apply(simp (no_asm) only: supp_def)
 apply(simp only: permute_set_eq permute_trm1)
-apply(simp only: alpha1_INJ)
+apply(simp only: alpha1_INJ alpha_bp_eq)
 apply(simp only: ex_out)
 apply(simp only: Collect_neg_conj)
 apply(simp only: permute_ABS)
 apply(simp only: Abs_eq_iff)
-apply(simp only: alpha_gen fv_eq_bv supp_Pair)
+apply(simp only: alpha_gen supp_Pair split_conv eqvts)
 apply(simp only: inf_or[symmetric])
 apply(simp only: Collect_disj_eq)
 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
-apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv sa[simplified fv_eq_bv,symmetric])
-apply(induct bp)
-apply(simp_all only: TrueI)
-apply(simp_all only: permute_trm1)
-apply(simp_all only: bv1.simps)
-apply(simp_all only: alpha1_INJ) (* Doesn't look true... *)
-apply(simp)
-sorry
-
-lemma
-"(\<not> (\<exists>p. (a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)} = supp tb - {atom name} \<and>
- ({atom (p \<bullet> (a \<rightleftharpoons> b) \<bullet> name)} = {atom name}) \<and>
- ((a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)}) \<sharp>* p \<and>
- p \<bullet> (a \<rightleftharpoons> b) \<bullet> tb = tb)) =
- (\<not> (\<exists>p. (a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)} = supp tb - {atom name} \<and>
- ((a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)}) \<sharp>* p \<and>
- p \<bullet> (a \<rightleftharpoons> b) \<bullet> tb = tb))"
-apply simp
-apply rule
-prefer 2
-apply (meson)[2]
-apply clarify
-apply (erule_tac x="p" in allE)
-apply simp
-apply (simp add: atom_eqvt[symmetric])
-sorry
-
-thm trm1_bp_inducts
+apply (simp only: eqvts[symmetric] fv_trm1_eqvt[symmetric])
+apply (simp only: eqvts Pair_eq)
+done
 
 lemma supp_fv:
   "supp t = fv_trm1 t"
@@ -292,28 +235,16 @@
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen.simps)
 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
-defer
-apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
+apply(simp add: supp_fv_let fv_trm1 fv_eq_bv supp_Pair)
+apply blast
+apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
+apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 apply(simp only: supp_at_base[simplified supp_def])
-apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq)
-apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric])
-(*apply(rule supp_fv_let) apply(simp_all)*)
-apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \<union> supp(rtrm11)")
-(*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \<union> supp(rtrm11)")*)
-apply(simp add: supp_Abs fv_trm1 supp_Pair Un_Diff Un_assoc fv_eq_bv)
-apply(blast) (* Un_commute in a good place *)
-apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1)
-apply(simp only: alpha1_INJ permute_ABS permute_prod.simps Abs_eq_iff)
-apply(simp only: ex_out)
-apply(simp only: Un_commute)
-apply(simp only: alpha_bp_eq fv_eq_bv)
-apply(simp only: alpha_gen fv_eq_bv supp_Pair)
-apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
-apply(simp only: ex_out)
-apply(simp only: Collect_neg_conj finite_Un Diff_cancel)
-apply(simp)
+apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1 alpha1_INJ[simplified alpha_bp_eq])
+apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric])
 apply(fold supp_def)
-sorry
+apply simp
+done
 
 lemma trm1_supp:
   "supp (Vr1 x) = {atom x}"
diff -r f970ca9b5bec -r 4908db645f98 Nominal/Term5.thy
--- a/Nominal/Term5.thy	Wed Mar 17 20:42:22 2010 +0100
+++ b/Nominal/Term5.thy	Wed Mar 17 20:42:42 2010 +0100
@@ -71,6 +71,8 @@
 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
+apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *})
+(*
 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
 apply (simp_all add: alpha5_inj)
 apply (erule exE)
@@ -89,7 +91,7 @@
 apply (rotate_tac 6)
 apply simp
 apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1])
-apply (simp)
+apply (simp)*)
 done
 
 lemma alpha5_transp: