--- a/Quot/Nominal/Terms.thy Thu Feb 18 08:37:45 2010 +0100
+++ b/Quot/Nominal/Terms.thy Thu Feb 18 08:43:13 2010 +0100
@@ -28,7 +28,7 @@
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
local_setup {* define_raw_fv "Terms.rtrm1"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
+ [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
[[], [[]], [[], []]]] *}
print_theorems
@@ -62,8 +62,9 @@
done
lemma fv_rtrm1_eqvt[eqvt]:
- shows "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
- apply (induct t)
+ "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
+ "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
+ apply (induct t and b)
apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
done
@@ -131,7 +132,7 @@
shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
apply(induct rule: alpha1.induct)
apply(simp_all add: alpha_gen.simps)
- done
+ sorry
lemma [quot_respect]:
"(op = ===> alpha1) rVr1 rVr1"
@@ -224,6 +225,11 @@
apply(simp add: supp_Pair supp_atom bp_supp)
done
+lemma fv_eq_bv: "fv_bp bp = bv1 bp"
+apply(induct bp rule: trm1_bp_inducts(2))
+apply(simp_all)
+done
+
lemma supp_fv:
shows "supp t = fv_trm1 t"
apply(induct t rule: trm1_bp_inducts(1))
@@ -240,7 +246,7 @@
apply(simp add: alpha_gen.simps)
apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
-apply(simp add: supp_Abs fv_trm1)
+apply(simp add: supp_Abs fv_trm1 fv_eq_bv)
apply(simp (no_asm) add: supp_def)
apply(simp add: alpha1_INJ)
apply(simp add: Abs_eq_iff)
@@ -254,7 +260,7 @@
"supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
"supp (Lm1 x t) = (supp t) - {atom x}"
"supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
- by (simp_all only: supp_fv fv_trm1)
+by (simp_all add: supp_fv fv_trm1 fv_eq_bv)
lemma trm1_induct_strong:
assumes "\<And>name b. P b (Vr1 name)"
@@ -281,8 +287,8 @@
"rbv2 (rAs x t) = {atom x}"
local_setup {* define_raw_fv "Terms.rtrm2"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],
- [[[(NONE, 0)], []]]] *}
+ [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]],
+ [[[], []]]] *}
print_theorems
setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
@@ -332,8 +338,8 @@
| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
local_setup {* define_raw_fv "Terms.trm3"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
- [[], [[(NONE, 0)], [], []]]] *}
+ [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv3}, 0)], [(SOME @{term bv3}, 0)]]],
+ [[], [[], [], []]]] *}
print_theorems
setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}
@@ -427,7 +433,7 @@
| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
local_setup {* define_raw_fv "Terms.rtrm5" [
- [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE, 0)], [], []]] ] *}
+ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *}
print_theorems
setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
@@ -720,7 +726,7 @@
| "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
local_setup {* define_raw_fv "Terms.rtrm6" [
- [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}
+ [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *}
print_theorems
setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}
@@ -876,7 +882,7 @@
| "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
local_setup {* define_raw_fv "Terms.rtrm7" [
- [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}
+ [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *}
print_theorems
setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}
@@ -889,11 +895,6 @@
| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
| a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
-lemma bvfv7: "rbv7 x = fv_rtrm7 x"
- apply induct
- apply simp_all
-done
-
lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
apply simp
apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
@@ -924,7 +925,7 @@
| "rbv8 (Bar1 v x b) = {atom v}"
local_setup {* define_raw_fv "Terms.rfoo8" [
- [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+ [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
print_theorems
setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}
@@ -958,6 +959,9 @@
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
@@ -978,7 +982,7 @@
| "rbv9 (Lam9 x b) = {atom x}"
local_setup {* define_raw_fv "Terms.rlam9" [
- [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *}
+ [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *}
print_theorems
setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}