| changeset 1664 | aa999d263b10 |
| parent 1602 | a7e60da429e2 |
| 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}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} |
26 [[[], [], [(SOME (@{term rbv5}, false), 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) |
63 |
63 |
64 lemma alpha5_symp: |
64 lemma alpha5_symp: |
65 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
65 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
66 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
66 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
67 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
67 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
68 sorry |
68 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
69 apply (simp_all add: alpha5_inj) |
|
70 apply (erule conjE)+ |
|
71 apply (erule exE) |
|
72 apply (rule_tac x="-pi" in exI) |
|
73 apply (rule alpha_gen_sym) |
|
74 apply (simp add: alphas) |
|
75 apply (simp add: alpha5_eqvt) |
|
76 apply (simp add: alphas) |
|
77 apply clarify |
|
78 apply simp |
|
79 done |
|
69 |
80 |
70 lemma alpha5_transp: |
81 lemma alpha5_transp: |
71 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and> |
82 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and> |
72 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and> |
83 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and> |
73 (alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))" |
84 (alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))" |
74 sorry |
85 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
86 apply (rule_tac [!] allI) |
|
87 apply (simp_all add: alpha5_inj) |
|
88 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
89 apply (simp_all add: alpha5_inj) |
|
90 defer |
|
91 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
92 apply (simp_all add: alpha5_inj) |
|
93 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
94 apply (simp_all add: alpha5_inj) |
|
95 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
96 apply (simp_all add: alpha5_inj) |
|
97 apply (erule conjE)+ |
|
98 apply (erule exE)+ |
|
99 apply (rule_tac x="pi + pia" in exI) |
|
100 apply (rule alpha_gen_trans) |
|
101 prefer 6 |
|
102 apply assumption |
|
103 apply (simp_all add: alphas alpha5_eqvt) |
|
104 apply (clarify) |
|
105 apply simp |
|
106 done |
|
75 |
107 |
76 lemma alpha5_equivp: |
108 lemma alpha5_equivp: |
77 "equivp alpha_rtrm5" |
109 "equivp alpha_rtrm5" |
78 "equivp alpha_rlts" |
110 "equivp alpha_rlts" |
79 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
111 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |