| changeset 1202 | ab942ba2d243 |
| parent 1201 | 6d2200603585 |
| child 1205 | acbf50e8eac2 |
| 1201:6d2200603585 | 1202:ab942ba2d243 |
|---|---|
39 |
39 |
40 notation |
40 notation |
41 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
41 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
42 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
42 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
43 thm alpha_rtrm1_alpha_bp.intros |
43 thm alpha_rtrm1_alpha_bp.intros |
44 thm fv_rtrm1_fv_bp.simps |
|
44 |
45 |
45 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)) *} |
46 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)) *} |
46 thm alpha1_inj |
47 thm alpha1_inj |
47 |
48 |
48 lemma alpha_bp_refl: "alpha_bp a a" |
49 lemma alpha_bp_refl: "alpha_bp a a" |
132 print_theorems |
133 print_theorems |
133 |
134 |
134 lemma alpha_rfv1: |
135 lemma alpha_rfv1: |
135 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
136 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
136 apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1)) |
137 apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1)) |
137 apply(simp_all add: alpha_gen.simps) |
138 apply(simp_all add: alpha_gen.simps alpha_bp_eq) |
138 done |
139 done |
139 |
140 |
140 lemma [quot_respect]: |
141 lemma [quot_respect]: |
141 "(op = ===> alpha_rtrm1) rVr1 rVr1" |
142 "(op = ===> alpha_rtrm1) rVr1 rVr1" |
142 "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" |
143 "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" |
143 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" |
144 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" |
144 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1" |
145 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1" |
145 apply (auto simp add: alpha1_inj) |
146 apply (auto simp add: alpha1_inj alpha_bp_eq) |
146 apply (rule_tac [!] x="0" in exI) |
147 apply (rule_tac [!] x="0" in exI) |
147 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq) |
148 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq) |
148 done |
149 done |
149 |
150 |
150 lemma [quot_respect]: |
151 lemma [quot_respect]: |
236 apply (rule_tac x="(x \<rightleftharpoons> a)" in exI) |
237 apply (rule_tac x="(x \<rightleftharpoons> a)" in exI) |
237 apply auto |
238 apply auto |
238 done |
239 done |
239 |
240 |
240 lemma supp_fv: |
241 lemma supp_fv: |
241 shows "supp t = fv_trm1 t" |
242 "supp t = fv_trm1 t" |
242 apply(induct t rule: trm1_bp_inducts(1)) |
243 "supp b = fv_bp b" |
244 apply(induct t and b rule: trm1_bp_inducts) |
|
243 apply(simp_all) |
245 apply(simp_all) |
244 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
246 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
245 apply(simp only: supp_at_base[simplified supp_def]) |
247 apply(simp only: supp_at_base[simplified supp_def]) |
246 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
248 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
247 apply(simp add: Collect_imp_eq Collect_neg_eq) |
249 apply(simp add: Collect_imp_eq Collect_neg_eq) |
258 apply(simp add: alpha1_INJ alpha_bp_eq) |
260 apply(simp add: alpha1_INJ alpha_bp_eq) |
259 apply(simp add: Abs_eq_iff) |
261 apply(simp add: Abs_eq_iff) |
260 apply(simp add: alpha_gen) |
262 apply(simp add: alpha_gen) |
261 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
263 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
262 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper) |
264 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper) |
265 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
|
266 apply(simp (no_asm) add: supp_def eqvts) |
|
267 apply(fold supp_def) |
|
268 apply(simp add: supp_at_base) |
|
269 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) |
|
270 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) |
|
263 done |
271 done |
264 |
272 |
265 lemma trm1_supp: |
273 lemma trm1_supp: |
266 "supp (Vr1 x) = {atom x}" |
274 "supp (Vr1 x) = {atom x}" |
267 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
275 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
294 "rbv2 (rAs x t) = {atom x}" |
302 "rbv2 (rAs x t) = {atom x}" |
295 |
303 |
296 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} |
304 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} |
297 |
305 |
298 local_setup {* snd o define_fv_alpha "Terms.rtrm2" |
306 local_setup {* snd o define_fv_alpha "Terms.rtrm2" |
299 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]], |
307 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]], |
300 [[[], []]]] *} |
308 [[[], []]]] *} |
301 |
309 |
302 notation |
310 notation |
303 alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and |
311 alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and |
304 alpha_rassign ("_ \<approx>2b _" [100, 100] 100) |
312 alpha_rassign ("_ \<approx>2b _" [100, 100] 100) |
351 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
359 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
352 |
360 |
353 setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} |
361 setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} |
354 |
362 |
355 local_setup {* snd o define_fv_alpha "Terms.trm3" |
363 local_setup {* snd o define_fv_alpha "Terms.trm3" |
356 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv3}, 0)], [(SOME @{term bv3}, 0)]]], |
364 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], |
357 [[], [[], [], []]]] *} |
365 [[], [[], [], []]]] *} |
358 print_theorems |
366 print_theorems |
359 |
367 |
360 notation |
368 notation |
361 alpha_trm3 ("_ \<approx>3 _" [100, 100] 100) and |
369 alpha_trm3 ("_ \<approx>3 _" [100, 100] 100) and |
663 |
671 |
664 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *} |
672 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *} |
665 print_theorems |
673 print_theorems |
666 |
674 |
667 local_setup {* snd o define_fv_alpha "Terms.rtrm6" [ |
675 local_setup {* snd o define_fv_alpha "Terms.rtrm6" [ |
668 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *} |
676 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} |
669 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100) |
677 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100) |
670 (* HERE THE RULES DIFFER *) |
678 (* HERE THE RULES DIFFER *) |
671 thm alpha_rtrm6.intros |
679 thm alpha_rtrm6.intros |
672 |
680 |
673 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} |
681 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} |
734 |
742 |
735 lemma [quot_respect]: |
743 lemma [quot_respect]: |
736 "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6" |
744 "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6" |
737 apply auto |
745 apply auto |
738 apply (simp_all add: alpha6_inj) |
746 apply (simp_all add: alpha6_inj) |
739 apply (rule conjI) |
|
740 apply (rule_tac [!] x="0::perm" in exI) |
747 apply (rule_tac [!] x="0::perm" in exI) |
741 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm) |
748 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm) |
742 (* needs rbv6_rsp *) |
749 (* needs rbv6_rsp *) |
743 oops |
750 oops |
744 |
751 |
760 \<lbrakk>True; |
767 \<lbrakk>True; |
761 \<exists>pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \<and> |
768 \<exists>pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \<and> |
762 (fv_trm6 rtrm6 - {atom name}) \<sharp>* pi \<and> pi \<bullet> rtrm6 = rtrm6a \<and> P (pi \<bullet> rtrm6) rtrm6a\<rbrakk> |
769 (fv_trm6 rtrm6 - {atom name}) \<sharp>* pi \<and> pi \<bullet> rtrm6 = rtrm6a \<and> P (pi \<bullet> rtrm6) rtrm6a\<rbrakk> |
763 \<Longrightarrow> P (Lm6 name rtrm6) (Lm6 namea rtrm6a); |
770 \<Longrightarrow> P (Lm6 name rtrm6) (Lm6 namea rtrm6a); |
764 \<And>rtrm61 rtrm61a rtrm62 rtrm62a. |
771 \<And>rtrm61 rtrm61a rtrm62 rtrm62a. |
765 \<lbrakk>\<exists>pi. fv_trm6 rtrm61 - bv6 rtrm61 = fv_trm6 rtrm61a - bv6 rtrm61a \<and> |
772 \<lbrakk>rtrm61 = rtrm61a; P rtrm61 rtrm61a; |
766 (fv_trm6 rtrm61 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm61 = rtrm61a \<and> P (pi \<bullet> rtrm61) rtrm61a; |
|
767 \<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and> |
773 \<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and> |
768 (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a \<and> P (pi \<bullet> rtrm62) rtrm62a\<rbrakk> |
774 (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a \<and> P (pi \<bullet> rtrm62) rtrm62a\<rbrakk> |
769 \<Longrightarrow> P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\<rbrakk> |
775 \<Longrightarrow> P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\<rbrakk> |
770 \<Longrightarrow> P x1 x2" |
776 \<Longrightarrow> P x1 x2" |
771 apply (lifting alpha_rtrm6.induct[unfolded alpha_gen]) |
777 apply (lifting alpha_rtrm6.induct[unfolded alpha_gen]) |
773 (* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) |
779 (* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) |
774 oops |
780 oops |
775 |
781 |
776 lemma lifted_inject_a3: |
782 lemma lifted_inject_a3: |
777 "(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) = |
783 "(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) = |
778 ((\<exists>pi. fv_trm6 rtrm61 - bv6 rtrm61 = fv_trm6 rtrm61a - bv6 rtrm61a \<and> |
784 (rtrm61 = rtrm61a \<and> |
779 (fv_trm6 rtrm61 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm61 = rtrm61a) \<and> |
|
780 (\<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and> |
785 (\<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and> |
781 (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a))" |
786 (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a))" |
782 apply(lifting alpha6_inj(3)[unfolded alpha_gen]) |
787 apply(lifting alpha6_inj(3)[unfolded alpha_gen]) |
783 apply injection |
788 apply injection |
784 (* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) |
789 (* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) |
803 |
808 |
804 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} |
809 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} |
805 thm permute_rtrm7.simps |
810 thm permute_rtrm7.simps |
806 |
811 |
807 local_setup {* snd o define_fv_alpha "Terms.rtrm7" [ |
812 local_setup {* snd o define_fv_alpha "Terms.rtrm7" [ |
808 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *} |
813 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *} |
809 print_theorems |
814 print_theorems |
810 notation |
815 notation |
811 alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100) |
816 alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100) |
812 (* HERE THE RULES DIFFER *) |
817 (* HERE THE RULES DIFFER *) |
813 thm alpha_rtrm7.intros |
818 thm alpha_rtrm7.intros |
850 |
855 |
851 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *} |
856 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *} |
852 print_theorems |
857 print_theorems |
853 |
858 |
854 local_setup {* snd o define_fv_alpha "Terms.rfoo8" [ |
859 local_setup {* snd o define_fv_alpha "Terms.rfoo8" [ |
855 [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
860 [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
856 notation |
861 notation |
857 alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and |
862 alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and |
858 alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100) |
863 alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100) |
859 (* HERE THE RULE DIFFERS *) |
864 (* HERE THE RULE DIFFERS *) |
860 thm alpha_rfoo8_alpha_rbar8.intros |
865 thm alpha_rfoo8_alpha_rbar8.intros |
886 |
891 |
887 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8" |
892 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8" |
888 apply simp apply clarify |
893 apply simp apply clarify |
889 apply (erule alpha8f_alpha8b.inducts(1)) |
894 apply (erule alpha8f_alpha8b.inducts(1)) |
890 apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) |
895 apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) |
891 apply clarify |
|
892 apply (erule alpha8f_alpha8b.inducts(2)) |
|
893 apply (simp_all) |
|
894 done |
896 done |
895 |
897 |
896 |
898 |
897 |
899 |
898 |
900 |
912 |
914 |
913 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} |
915 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} |
914 print_theorems |
916 print_theorems |
915 |
917 |
916 local_setup {* snd o define_fv_alpha "Terms.rlam9" [ |
918 local_setup {* snd o define_fv_alpha "Terms.rlam9" [ |
917 [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *} |
919 [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *} |
918 notation |
920 notation |
919 alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and |
921 alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and |
920 alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100) |
922 alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100) |
921 (* HERE THE RULES DIFFER *) |
923 (* HERE THE RULES DIFFER *) |
922 thm alpha_rlam9_alpha_rbla9.intros |
924 thm alpha_rlam9_alpha_rbla9.intros |