--- 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)