77 apply (erule exE) |
77 apply (erule exE) |
78 apply (rule_tac x="- pi" in exI) |
78 apply (rule_tac x="- pi" in exI) |
79 apply clarify |
79 apply clarify |
80 apply (erule alpha_gen_compose_sym) |
80 apply (erule alpha_gen_compose_sym) |
81 apply (simp add: alpha5_eqvt) |
81 apply (simp add: alpha5_eqvt) |
|
82 (* Works for non-recursive, proof is done here *) |
82 apply(clarify) |
83 apply(clarify) |
83 apply (rotate_tac 1) |
84 apply (rotate_tac 1) |
84 apply (frule_tac p="- pi" in alpha5_eqvt(1)) |
85 apply (frule_tac p="- pi" in alpha5_eqvt(1)) |
85 apply simp |
86 apply simp |
86 done |
87 done |
87 |
88 |
88 |
89 lemma alpha5_transp: |
|
90 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and> |
|
91 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and> |
|
92 (alpha_rbv5 p k l \<longrightarrow> (\<forall>m q. alpha_rbv5 q l m \<longrightarrow> alpha_rbv5 (q + p) k m))" |
|
93 (*apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})*) |
|
94 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
|
95 apply (rule_tac [!] allI) |
|
96 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
97 apply (simp_all add: alpha5_inj) |
|
98 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
99 apply (simp_all add: alpha5_inj) |
|
100 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
101 apply (simp_all add: alpha5_inj) |
|
102 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) |
|
103 apply clarify |
|
104 apply simp |
|
105 apply (erule alpha_gen_compose_trans) |
|
106 apply (assumption) |
|
107 apply (simp add: alpha5_eqvt) |
|
108 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
109 apply (simp_all add: alpha5_inj) |
|
110 apply (rule allI) |
|
111 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
112 apply (simp_all add: alpha5_inj) |
|
113 apply (rule allI) |
|
114 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
115 apply (simp_all add: alpha5_inj) |
|
116 (* Works for non-recursive, proof is done here *) |
|
117 apply clarify |
|
118 apply (rotate_tac 1) |
|
119 apply (frule_tac p="- pia" in alpha5_eqvt(1)) |
|
120 apply (erule_tac x="- pia \<bullet> rtrm5aa" in allE) |
|
121 apply simp |
|
122 apply (rotate_tac -1) |
|
123 apply (frule_tac p="pia" in alpha5_eqvt(1)) |
|
124 apply simp |
|
125 done |
89 |
126 |
90 lemma alpha5_equivp: |
127 lemma alpha5_equivp: |
91 "equivp alpha_rtrm5" |
128 "equivp alpha_rtrm5" |
92 "equivp alpha_rlts" |
129 "equivp alpha_rlts" |
93 "equivp (alpha_rbv5 p)" |
130 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
94 sorry |
131 apply (simp_all only: alpha5_reflp) |
|
132 apply (meson alpha5_symp alpha5_transp) |
|
133 apply (meson alpha5_symp alpha5_transp) |
|
134 done |
95 |
135 |
96 quotient_type |
136 quotient_type |
97 trm5 = rtrm5 / alpha_rtrm5 |
137 trm5 = rtrm5 / alpha_rtrm5 |
98 and |
138 and |
99 lts = rlts / alpha_rlts |
139 lts = rlts / alpha_rlts |