59 (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), |
59 (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), |
60 build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} |
60 build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} |
61 print_theorems |
61 print_theorems |
62 |
62 |
63 lemma alpha5_reflp: |
63 lemma alpha5_reflp: |
64 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)" |
64 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 x x)" |
65 apply (rule rtrm5_rlts.induct) |
65 apply (rule rtrm5_rlts.induct) |
66 apply (simp_all add: alpha5_inj) |
66 apply (simp_all add: alpha5_inj) |
67 apply (rule_tac x="0::perm" in exI) |
67 apply (rule_tac x="0::perm" in exI) |
68 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) |
68 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) |
69 done |
69 done |
70 |
70 |
71 lemma alpha5_symp: |
71 lemma alpha5_symp: |
72 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
72 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
73 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
73 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
74 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)" |
74 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
75 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
75 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
76 apply (simp_all add: alpha5_inj) |
76 apply (simp_all add: alpha5_inj) |
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 (rule conjI) |
81 apply (simp add: alpha5_eqvt) |
81 apply (erule_tac [!] alpha_gen_compose_sym) |
82 (* Works for non-recursive, proof is done here *) |
82 apply (simp_all add: alpha5_eqvt) |
83 apply(clarify) |
|
84 apply (rotate_tac 1) |
|
85 apply (frule_tac p="- pi" in alpha5_eqvt(1)) |
|
86 apply simp |
|
87 done |
83 done |
88 |
84 |
89 lemma alpha5_transp: |
85 lemma alpha5_transp: |
90 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and> |
86 "(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> |
87 (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))" |
88 (alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 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 *})*) |
89 (*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) |
90 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
95 apply (rule_tac [!] allI) |
91 apply (rule_tac [!] allI) |
96 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
92 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
97 apply (simp_all add: alpha5_inj) |
93 apply (simp_all add: alpha5_inj) |
99 apply (simp_all add: alpha5_inj) |
95 apply (simp_all add: alpha5_inj) |
100 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
96 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
101 apply (simp_all add: alpha5_inj) |
97 apply (simp_all add: alpha5_inj) |
102 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) |
98 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) |
103 apply clarify |
99 apply clarify |
104 apply simp |
100 apply (rule conjI) |
105 apply (erule alpha_gen_compose_trans) |
101 apply (erule alpha_gen_compose_trans) |
106 apply (assumption) |
102 apply (assumption) |
107 apply (simp add: alpha5_eqvt) |
103 apply (simp add: alpha5_eqvt) |
108 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
104 apply (erule alpha_gen_compose_trans) |
109 apply (simp_all add: alpha5_inj) |
105 apply (assumption) |
110 apply (rule allI) |
106 apply (simp add: alpha5_eqvt) |
111 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
107 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
112 apply (simp_all add: alpha5_inj) |
108 apply (simp_all add: alpha5_inj) |
113 apply (rule allI) |
109 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
114 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
110 apply (simp_all add: alpha5_inj) |
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 |
111 done |
126 |
112 |
127 lemma alpha5_equivp: |
113 lemma alpha5_equivp: |
128 "equivp alpha_rtrm5" |
114 "equivp alpha_rtrm5" |
129 "equivp alpha_rlts" |
115 "equivp alpha_rlts" |
155 print_theorems |
141 print_theorems |
156 |
142 |
157 lemma alpha5_rfv: |
143 lemma alpha5_rfv: |
158 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
144 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
159 "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m \<and> fv_rbv5 l = fv_rbv5 m))" |
145 "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m \<and> fv_rbv5 l = fv_rbv5 m))" |
160 "(alpha_rbv5 p b c \<Longrightarrow> fv_rbv5 (p \<bullet> b) = fv_rbv5 c)" |
146 "(alpha_rbv5 b c \<Longrightarrow> fv_rbv5 b = fv_rbv5 c)" |
161 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
147 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
162 apply(simp_all add: eqvts) |
148 apply(simp_all add: eqvts) |
163 thm alpha5_inj |
|
164 apply(simp add: alpha_gen) |
149 apply(simp add: alpha_gen) |
165 apply(clarify) |
150 apply(clarify) |
166 apply(simp) |
151 apply(simp) |
167 sorry |
152 sorry |
168 |
153 |
183 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
168 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
184 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
169 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
185 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
170 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
186 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
171 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
187 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
172 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
188 "(op = ===> alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
173 "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
189 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
174 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
190 apply (clarify) |
175 apply (clarify) |
191 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
176 apply (rule_tac x="0" in exI) |
192 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
177 apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
193 apply (simp_all add: alpha5_inj) |
|
194 apply clarify |
|
195 apply clarify |
178 apply clarify |
196 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
179 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
197 apply simp_all |
180 apply simp_all |
198 apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
181 apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
199 apply simp_all |
182 apply simp_all |
232 lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted] |
215 lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted] |
233 lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted] |
216 lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted] |
234 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
217 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
235 |
218 |
236 lemma lets_bla: |
219 lemma lets_bla: |
237 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" |
220 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" |
238 apply (simp only: alpha5_INJ) |
221 apply (simp only: alpha5_INJ) |
239 apply (simp only: bv5) |
222 apply (simp only: bv5) |
240 apply simp |
223 apply simp |
241 apply (rule_tac x="(z \<leftrightarrow> y)" in exI) |
224 apply (rule allI) |
242 apply (simp_all add: alpha_gen) |
225 apply (simp_all add: alpha_gen) |
243 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts) |
226 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts) |
244 done |
227 apply (rule impI) |
|
228 apply (rule impI) |
|
229 sorry (* The assumption is false, so it is true *) |
245 |
230 |
246 lemma lets_ok: |
231 lemma lets_ok: |
247 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
232 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
248 thm alpha5_INJ |
233 thm alpha5_INJ |
249 apply (simp only: alpha5_INJ) |
234 apply (simp only: alpha5_INJ) |
260 apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) |
245 apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) |
261 done |
246 done |
262 |
247 |
263 |
248 |
264 lemma lets_not_ok1: |
249 lemma lets_not_ok1: |
265 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
250 "x \<noteq> y \<Longrightarrow> |
|
251 (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
266 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
252 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
267 apply (simp add: alpha5_INJ alpha_gen) |
253 apply (simp add: alpha5_INJ alpha_gen) |
268 apply (rule_tac x="0::perm" in exI) |
254 apply (simp add: permute_trm5_lts eqvts) |
269 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) |
255 apply (simp add: alpha5_INJ(5)) |
270 apply auto |
256 apply (simp add: alpha5_INJ(1)) |
271 done |
257 done |
272 |
258 |
273 lemma distinct_helper: |
259 lemma distinct_helper: |
274 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
260 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
275 apply auto |
261 apply auto |