
diff -r 6d2200603585 -r ab942ba2d243 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Sat Feb 20 06:31:03 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Sun Feb 21 22:39:11 2010 +0100
@@ -41,6 +41,7 @@
   alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
   alpha_bp ("_ \<approx>1b _" [100, 100] 100)
 thm alpha_rtrm1_alpha_bp.intros
+thm fv_rtrm1_fv_bp.simps
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *}
 thm alpha1_inj
@@ -134,7 +135,7 @@
 lemma alpha_rfv1:
   shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
   apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1))
-  apply(simp_all add: alpha_gen.simps)
+  apply(simp_all add: alpha_gen.simps alpha_bp_eq)
   done
 
 lemma [quot_respect]:
@@ -142,7 +143,7 @@
  "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1"
  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1"
  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1"
-apply (auto simp add: alpha1_inj)
+apply (auto simp add: alpha1_inj alpha_bp_eq)
 apply (rule_tac [!] x="0" in exI)
 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq)
 done
@@ -238,8 +239,9 @@
 done
 
 lemma supp_fv:
-  shows "supp t = fv_trm1 t"
-apply(induct t rule: trm1_bp_inducts(1))
+  "supp t = fv_trm1 t"
+  "supp b = fv_bp b"
+apply(induct t and b rule: trm1_bp_inducts)
 apply(simp_all)
 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 apply(simp only: supp_at_base[simplified supp_def])
@@ -260,6 +262,12 @@
 apply(simp add: alpha_gen)
 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper)
+apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
+apply(simp (no_asm) add: supp_def eqvts)
+apply(fold supp_def)
+apply(simp add: supp_at_base)
+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])
 done
 
 lemma trm1_supp:
@@ -296,7 +304,7 @@
 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
 
 local_setup {* snd o define_fv_alpha "Terms.rtrm2"
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]],
+  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],
    [[[], []]]] *}
 
 notation
@@ -353,7 +361,7 @@
 setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}
 
 local_setup {* snd o define_fv_alpha "Terms.trm3"
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv3}, 0)], [(SOME @{term bv3}, 0)]]],
+  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
    [[], [[], [], []]]] *}
 print_theorems
 
@@ -665,7 +673,7 @@
 print_theorems
 
 local_setup {* snd o define_fv_alpha "Terms.rtrm6" [
-  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *}
+  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}
 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100)
 (* HERE THE RULES DIFFER *)
 thm alpha_rtrm6.intros
@@ -736,7 +744,6 @@
  "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6"
 apply auto
 apply (simp_all add: alpha6_inj)
-apply (rule conjI)
 apply (rule_tac [!] x="0::perm" in exI)
 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm)
 (* needs rbv6_rsp *)
@@ -762,8 +769,7 @@
           (fv_trm6 rtrm6 - {atom name}) \<sharp>* pi \<and> pi \<bullet> rtrm6 = rtrm6a \<and> P (pi \<bullet> rtrm6) rtrm6a\<rbrakk>
     \<Longrightarrow> P (Lm6 name rtrm6) (Lm6 namea rtrm6a);
  \<And>rtrm61 rtrm61a rtrm62 rtrm62a.
-    \<lbrakk>\<exists>pi. fv_trm6 rtrm61 - bv6 rtrm61 = fv_trm6 rtrm61a - bv6 rtrm61a \<and>
-          (fv_trm6 rtrm61 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm61 = rtrm61a \<and> P (pi \<bullet> rtrm61) rtrm61a;
+    \<lbrakk>rtrm61 = rtrm61a; P rtrm61 rtrm61a;
      \<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>
           (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a \<and> P (pi \<bullet> rtrm62) rtrm62a\<rbrakk>
     \<Longrightarrow> P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\<rbrakk>
@@ -775,8 +781,7 @@
 
 lemma lifted_inject_a3:
 "(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) =
-((\<exists>pi. fv_trm6 rtrm61 - bv6 rtrm61 = fv_trm6 rtrm61a - bv6 rtrm61a \<and>
-       (fv_trm6 rtrm61 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm61 = rtrm61a) \<and>
+(rtrm61 = rtrm61a \<and>
  (\<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>
        (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a))"
 apply(lifting alpha6_inj(3)[unfolded alpha_gen])
@@ -805,7 +810,7 @@
 thm permute_rtrm7.simps
 
 local_setup {* snd o define_fv_alpha "Terms.rtrm7" [
-  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *}
+  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}
 print_theorems
 notation
   alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100)
@@ -852,7 +857,7 @@
 print_theorems
 
 local_setup {* snd o define_fv_alpha "Terms.rfoo8" [
-  [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+  [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
 notation
   alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and
   alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100)
@@ -888,9 +893,6 @@
   apply simp apply clarify
   apply (erule alpha8f_alpha8b.inducts(1))
   apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
-  apply clarify
-  apply (erule alpha8f_alpha8b.inducts(2))
-  apply (simp_all)
 done
 
 
@@ -914,7 +916,7 @@
 print_theorems
 
 local_setup {* snd o define_fv_alpha "Terms.rlam9" [
-  [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *}
+  [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *}
 notation
   alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and
   alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100)




