| changeset 1184 | 85501074fd4f |
| parent 1183 | cb3da5b540f2 |
| child 1185 | 7566b899ca6a |
| 1183:cb3da5b540f2 | 1184:85501074fd4f |
|---|---|
26 "bv1 (BUnit) = {}" |
26 "bv1 (BUnit) = {}" |
27 | "bv1 (BVr x) = {atom x}" |
27 | "bv1 (BVr x) = {atom x}" |
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
29 |
29 |
30 local_setup {* define_raw_fv "Terms.rtrm1" |
30 local_setup {* define_raw_fv "Terms.rtrm1" |
31 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
31 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
32 [[], [[]], [[], []]]] *} |
32 [[], [[]], [[], []]]] *} |
33 print_theorems |
33 print_theorems |
34 |
34 |
35 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} |
35 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} |
36 |
36 |
60 apply (induct x) |
60 apply (induct x) |
61 apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt eqvts) |
61 apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt eqvts) |
62 done |
62 done |
63 |
63 |
64 lemma fv_rtrm1_eqvt[eqvt]: |
64 lemma fv_rtrm1_eqvt[eqvt]: |
65 shows "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)" |
65 "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)" |
66 apply (induct t) |
66 "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)" |
67 apply (induct t and b) |
|
67 apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt) |
68 apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt) |
68 done |
69 done |
69 |
70 |
70 |
71 |
71 lemma alpha1_eqvt: |
72 lemma alpha1_eqvt: |
129 |
130 |
130 lemma alpha_rfv1: |
131 lemma alpha_rfv1: |
131 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
132 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
132 apply(induct rule: alpha1.induct) |
133 apply(induct rule: alpha1.induct) |
133 apply(simp_all add: alpha_gen.simps) |
134 apply(simp_all add: alpha_gen.simps) |
134 done |
135 sorry |
135 |
136 |
136 lemma [quot_respect]: |
137 lemma [quot_respect]: |
137 "(op = ===> alpha1) rVr1 rVr1" |
138 "(op = ===> alpha1) rVr1 rVr1" |
138 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1" |
139 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1" |
139 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1" |
140 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1" |
220 apply(rule lm1_supp_pre) |
221 apply(rule lm1_supp_pre) |
221 apply(simp add: supp_Pair supp_atom) |
222 apply(simp add: supp_Pair supp_atom) |
222 apply(rule supports_finite) |
223 apply(rule supports_finite) |
223 apply(rule lt1_supp_pre) |
224 apply(rule lt1_supp_pre) |
224 apply(simp add: supp_Pair supp_atom bp_supp) |
225 apply(simp add: supp_Pair supp_atom bp_supp) |
226 done |
|
227 |
|
228 lemma fv_eq_bv: "fv_bp bp = bv1 bp" |
|
229 apply(induct bp rule: trm1_bp_inducts(2)) |
|
230 apply(simp_all) |
|
225 done |
231 done |
226 |
232 |
227 lemma supp_fv: |
233 lemma supp_fv: |
228 shows "supp t = fv_trm1 t" |
234 shows "supp t = fv_trm1 t" |
229 apply(induct t rule: trm1_bp_inducts(1)) |
235 apply(induct t rule: trm1_bp_inducts(1)) |
238 apply(simp add: alpha1_INJ) |
244 apply(simp add: alpha1_INJ) |
239 apply(simp add: Abs_eq_iff) |
245 apply(simp add: Abs_eq_iff) |
240 apply(simp add: alpha_gen.simps) |
246 apply(simp add: alpha_gen.simps) |
241 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
247 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
242 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
248 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
243 apply(simp add: supp_Abs fv_trm1) |
249 apply(simp add: supp_Abs fv_trm1 fv_eq_bv) |
244 apply(simp (no_asm) add: supp_def) |
250 apply(simp (no_asm) add: supp_def) |
245 apply(simp add: alpha1_INJ) |
251 apply(simp add: alpha1_INJ) |
246 apply(simp add: Abs_eq_iff) |
252 apply(simp add: Abs_eq_iff) |
247 apply(simp add: alpha_gen) |
253 apply(simp add: alpha_gen) |
248 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt) |
254 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt) |
252 lemma trm1_supp: |
258 lemma trm1_supp: |
253 "supp (Vr1 x) = {atom x}" |
259 "supp (Vr1 x) = {atom x}" |
254 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
260 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
255 "supp (Lm1 x t) = (supp t) - {atom x}" |
261 "supp (Lm1 x t) = (supp t) - {atom x}" |
256 "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)" |
262 "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)" |
257 by (simp_all only: supp_fv fv_trm1) |
263 by (simp_all add: supp_fv fv_trm1 fv_eq_bv) |
258 |
264 |
259 lemma trm1_induct_strong: |
265 lemma trm1_induct_strong: |
260 assumes "\<And>name b. P b (Vr1 name)" |
266 assumes "\<And>name b. P b (Vr1 name)" |
261 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)" |
267 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)" |
262 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)" |
268 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)" |
279 rbv2 |
285 rbv2 |
280 where |
286 where |
281 "rbv2 (rAs x t) = {atom x}" |
287 "rbv2 (rAs x t) = {atom x}" |
282 |
288 |
283 local_setup {* define_raw_fv "Terms.rtrm2" |
289 local_setup {* define_raw_fv "Terms.rtrm2" |
284 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]], |
290 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]], |
285 [[[(NONE, 0)], []]]] *} |
291 [[[], []]]] *} |
286 print_theorems |
292 print_theorems |
287 |
293 |
288 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} |
294 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} |
289 |
295 |
290 inductive |
296 inductive |
330 where |
336 where |
331 "bv3 ANil = {}" |
337 "bv3 ANil = {}" |
332 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
338 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
333 |
339 |
334 local_setup {* define_raw_fv "Terms.trm3" |
340 local_setup {* define_raw_fv "Terms.trm3" |
335 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], |
341 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv3}, 0)], [(SOME @{term bv3}, 0)]]], |
336 [[], [[(NONE, 0)], [], []]]] *} |
342 [[], [[], [], []]]] *} |
337 print_theorems |
343 print_theorems |
338 |
344 |
339 setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} |
345 setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} |
340 |
346 |
341 inductive |
347 inductive |
425 where |
431 where |
426 "rbv5 rLnil = {}" |
432 "rbv5 rLnil = {}" |
427 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
433 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
428 |
434 |
429 local_setup {* define_raw_fv "Terms.rtrm5" [ |
435 local_setup {* define_raw_fv "Terms.rtrm5" [ |
430 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE, 0)], [], []]] ] *} |
436 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} |
431 print_theorems |
437 print_theorems |
432 |
438 |
433 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} |
439 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} |
434 print_theorems |
440 print_theorems |
435 |
441 |
718 "rbv6 (rVr6 n) = {}" |
724 "rbv6 (rVr6 n) = {}" |
719 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t" |
725 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t" |
720 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r" |
726 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r" |
721 |
727 |
722 local_setup {* define_raw_fv "Terms.rtrm6" [ |
728 local_setup {* define_raw_fv "Terms.rtrm6" [ |
723 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} |
729 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *} |
724 print_theorems |
730 print_theorems |
725 |
731 |
726 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *} |
732 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *} |
727 print_theorems |
733 print_theorems |
728 |
734 |
874 "rbv7 (rVr7 n) = {atom n}" |
880 "rbv7 (rVr7 n) = {atom n}" |
875 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}" |
881 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}" |
876 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r" |
882 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r" |
877 |
883 |
878 local_setup {* define_raw_fv "Terms.rtrm7" [ |
884 local_setup {* define_raw_fv "Terms.rtrm7" [ |
879 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *} |
885 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *} |
880 print_theorems |
886 print_theorems |
881 |
887 |
882 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} |
888 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} |
883 print_theorems |
889 print_theorems |
884 |
890 |
886 alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100) |
892 alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100) |
887 where |
893 where |
888 a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)" |
894 a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)" |
889 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s" |
895 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s" |
890 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2" |
896 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2" |
891 |
|
892 lemma bvfv7: "rbv7 x = fv_rtrm7 x" |
|
893 apply induct |
|
894 apply simp_all |
|
895 done |
|
896 |
897 |
897 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7" |
898 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7" |
898 apply simp |
899 apply simp |
899 apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI) |
900 apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI) |
900 apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI) |
901 apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI) |
922 where |
923 where |
923 "rbv8 (Bar0 x) = {}" |
924 "rbv8 (Bar0 x) = {}" |
924 | "rbv8 (Bar1 v x b) = {atom v}" |
925 | "rbv8 (Bar1 v x b) = {atom v}" |
925 |
926 |
926 local_setup {* define_raw_fv "Terms.rfoo8" [ |
927 local_setup {* define_raw_fv "Terms.rfoo8" [ |
927 [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
928 [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
928 print_theorems |
929 print_theorems |
929 |
930 |
930 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *} |
931 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *} |
931 print_theorems |
932 print_theorems |
932 |
933 |
956 |
957 |
957 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8" |
958 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8" |
958 apply simp apply clarify |
959 apply simp apply clarify |
959 apply (erule alpha8f_alpha8b.inducts(1)) |
960 apply (erule alpha8f_alpha8b.inducts(1)) |
960 apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) |
961 apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) |
962 apply clarify |
|
963 apply (erule alpha8f_alpha8b.inducts(2)) |
|
964 apply (simp_all) |
|
961 done |
965 done |
962 |
966 |
963 |
967 |
964 |
968 |
965 |
969 |
976 where |
980 where |
977 "rbv9 (Var9 x) = {}" |
981 "rbv9 (Var9 x) = {}" |
978 | "rbv9 (Lam9 x b) = {atom x}" |
982 | "rbv9 (Lam9 x b) = {atom x}" |
979 |
983 |
980 local_setup {* define_raw_fv "Terms.rlam9" [ |
984 local_setup {* define_raw_fv "Terms.rlam9" [ |
981 [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *} |
985 [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *} |
982 print_theorems |
986 print_theorems |
983 |
987 |
984 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} |
988 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} |
985 print_theorems |
989 print_theorems |
986 |
990 |