| changeset 1664 | aa999d263b10 |
| parent 1603 | 2b367c80c0d7 |
| 1660:d1293d30c657 | 1664:aa999d263b10 |
|---|---|
1 theory Term5 |
1 theory Term5 |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
2 imports "../Nominal2_Atoms" "../Nominal2_Eqvt" "../Nominal2_Supp" "../Abs" "../Perm" "../Fv" "../Rsp" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 datatype rtrm5 = |
7 datatype rtrm5 = |
21 |
21 |
22 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} |
22 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} |
23 print_theorems |
23 print_theorems |
24 |
24 |
25 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") |
25 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") |
26 [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} |
26 [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [(0,NONE), (2,SOME @{term rbv5})]])] *} |
27 print_theorems |
27 print_theorems |
28 |
28 |
29 notation |
29 notation |
30 alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and |
30 alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and |
31 alpha_rlts ("_ \<approx>l _" [100, 100] 100) |
31 alpha_rlts ("_ \<approx>l _" [100, 100] 100) |
32 thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros |
32 thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros |
33 |
33 |
34 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} |
34 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_rel_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} |
35 thm alpha5_inj |
35 thm alpha5_inj |
36 |
36 |
37 lemma rbv5_eqvt[eqvt]: |
37 lemma rbv5_eqvt[eqvt]: |
38 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
38 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
39 apply (induct x) |
39 apply (induct x) |
69 |
69 |
70 lemma alpha5_symp: |
70 lemma alpha5_symp: |
71 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
71 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
72 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
72 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
73 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
73 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
74 apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *}) |
74 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
75 apply (simp_all add: alpha5_inj) |
|
76 apply (erule exE) |
|
77 apply (rule_tac x="-pi" in exI) |
|
78 apply (rule alpha_gen_sym) |
|
79 apply (simp_all add: alphas) |
|
80 apply (case_tac x) |
|
81 apply (case_tac y) |
|
82 apply (simp add: alpha5_eqvt) |
|
83 apply clarify |
|
84 apply simp |
|
75 done |
85 done |
76 |
86 |
77 lemma alpha5_symp1: |
87 lemma alpha5_symp1: |
78 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
88 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
79 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
89 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |