53 thm foo.fsupp |
53 thm foo.fsupp |
54 thm foo.supp |
54 thm foo.supp |
55 thm foo.fresh |
55 thm foo.fresh |
56 thm foo.bn_finite |
56 thm foo.bn_finite |
57 |
57 |
58 lemma uu1: |
|
59 shows "alpha_bn1 as (permute_bn1 p as)" |
|
60 apply(induct as rule: foo.inducts(2)) |
|
61 apply(auto)[7] |
|
62 apply(simp add: foo.perm_bn_simps) |
|
63 apply(simp add: foo.eq_iff) |
|
64 apply(auto) |
|
65 done |
|
66 |
|
67 lemma uu2: |
|
68 shows "alpha_bn2 as (permute_bn2 p as)" |
|
69 apply(induct as rule: foo.inducts(2)) |
|
70 apply(auto)[7] |
|
71 apply(simp add: foo.perm_bn_simps) |
|
72 apply(simp add: foo.eq_iff) |
|
73 apply(auto) |
|
74 done |
|
75 |
|
76 lemma uu3: |
|
77 shows "alpha_bn3 as (permute_bn3 p as)" |
|
78 apply(induct as rule: foo.inducts(2)) |
|
79 apply(auto)[7] |
|
80 apply(simp add: foo.perm_bn_simps) |
|
81 apply(simp add: foo.eq_iff) |
|
82 apply(auto) |
|
83 done |
|
84 |
|
85 lemma uu4: |
|
86 shows "alpha_bn4 as (permute_bn4 p as)" |
|
87 apply(induct as rule: foo.inducts(3)) |
|
88 apply(auto)[8] |
|
89 apply(simp add: foo.perm_bn_simps) |
|
90 apply(simp add: foo.eq_iff) |
|
91 apply(simp add: foo.perm_bn_simps) |
|
92 apply(simp add: foo.eq_iff) |
|
93 done |
|
94 |
|
95 |
58 |
96 lemma tt1: |
59 lemma tt1: |
97 shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)" |
60 shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)" |
98 apply(induct as rule: foo.inducts(2)) |
61 apply(induct as rule: foo.inducts(2)) |
99 apply(auto)[7] |
62 apply(auto)[7] |
127 apply(simp add: foo.perm_bn_simps foo.bn_defs permute_set_eq) |
90 apply(simp add: foo.perm_bn_simps foo.bn_defs permute_set_eq) |
128 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
91 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
129 apply(simp add: atom_eqvt insert_eqvt) |
92 apply(simp add: atom_eqvt insert_eqvt) |
130 done |
93 done |
131 |
94 |
132 |
|
133 lemma Let1_rename: |
|
134 assumes "supp ([bn1 assn]lst. trm) \<sharp>* p" |
|
135 shows "Let1 assn trm = Let1 (permute_bn1 p assn) (p \<bullet> trm)" |
|
136 using assms |
|
137 apply - |
|
138 apply(drule supp_perm_eq[symmetric]) |
|
139 apply(simp only: permute_Abs) |
|
140 apply(simp only: tt1) |
|
141 apply(simp only: foo.eq_iff) |
|
142 apply(rule conjI) |
|
143 apply(rule refl) |
|
144 apply(rule uu1) |
|
145 done |
|
146 |
|
147 lemma Let1_rename_a: |
|
148 fixes c::"'a::fs" |
|
149 assumes "y = Let1 assn trm" |
|
150 shows "\<exists>p. (p \<bullet> (set (bn1 assn))) \<sharp>* c \<and> y = Let1 (permute_bn1 p assn) (p \<bullet> trm)" |
|
151 using assms |
|
152 apply(simp only: foo.eq_iff uu1 tt1[symmetric] permute_Abs[symmetric]) |
|
153 apply(simp del: permute_Abs) |
|
154 sorry |
|
155 |
|
156 lemma strong_exhaust1: |
95 lemma strong_exhaust1: |
157 fixes c::"'a::fs" |
96 fixes c::"'a::fs" |
158 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
97 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
159 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
98 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
160 and "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" |
99 and "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" |
161 and "\<exists>(c::'a::fs) assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P" |
100 and "\<exists>(c::'a::fs) assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P" |
162 and "\<exists>(c::'a::fs) assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P" |
101 and "\<exists>(c::'a::fs) assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P" |
163 and "\<exists>(c::'a::fs) assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P" |
102 and "\<exists>(c::'a::fs) assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P" |
164 and "\<exists>(c::'a::fs) assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P" |
103 and "\<exists>(c::'a::fs) assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P" |
165 shows "P" |
104 shows "P" |
166 apply(rule_tac y="y" in foo.exhaust(1)) |
105 oops |
167 apply(rule assms(1)) |
|
168 apply(rule exI) |
|
169 apply(assumption) |
|
170 apply(rule assms(2)) |
|
171 apply(rule exI)+ |
|
172 apply(assumption) |
|
173 apply(rule assms(3)) |
|
174 apply(subgoal_tac "\<exists>p::perm. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)") |
|
175 apply(erule exE) |
|
176 apply(perm_simp) |
|
177 apply(rule_tac exI)+ |
|
178 apply(rule conjI) |
|
179 apply(simp add: fresh_star_prod) |
|
180 apply(erule conjE)+ |
|
181 apply(assumption) |
|
182 apply(simp) |
|
183 apply(simp add: foo.eq_iff) |
|
184 (* HERE *) |
|
185 defer |
|
186 defer |
|
187 apply(rule assms(4)) |
|
188 apply(subgoal_tac "\<exists>p::perm. (p \<bullet> (set (bn1 assg))) \<sharp>* (c, assg, trm)") |
|
189 apply(erule exE) |
|
190 apply(perm_simp add: tt1) |
|
191 apply(simp only: fresh_star_prod) |
|
192 apply(erule conjE)+ |
|
193 apply(rule_tac exI)+ |
|
194 apply(rule conjI) |
|
195 apply(assumption) |
|
196 apply(simp add: foo.eq_iff) |
|
197 apply(rule conjI) |
|
198 apply(simp only: tt1[symmetric]) |
|
199 defer |
|
200 apply(rule uu1) |
|
201 defer |
|
202 apply(rule assms(5)) |
|
203 apply(subgoal_tac "\<exists>p::perm. (p \<bullet> (set (bn2 assg))) \<sharp>* (c, assg, trm)") |
|
204 apply(erule exE) |
|
205 apply(perm_simp add: tt2) |
|
206 apply(simp only: fresh_star_prod) |
|
207 apply(erule conjE)+ |
|
208 apply(rule_tac exI)+ |
|
209 apply(rule conjI) |
|
210 apply(assumption) |
|
211 apply(simp add: foo.eq_iff) |
|
212 apply(rule conjI) |
|
213 apply(simp only: tt2[symmetric]) |
|
214 defer |
|
215 apply(rule uu2) |
|
216 defer |
|
217 apply(rule refl) |
|
218 apply(subst (asm) fresh_star_supp_conv) |
|
219 apply(simp) |
|
220 |
106 |
221 |
107 |
222 lemma strong_exhaust2: |
108 lemma strong_exhaust2: |
223 fixes c::"'a::fs" |
109 fixes c::"'a::fs" |
224 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
110 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
227 and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" |
113 and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" |
228 and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" |
114 and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" |
229 and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" |
115 and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" |
230 and "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P" |
116 and "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P" |
231 shows "P" |
117 shows "P" |
232 apply(rule strong_exhaust1[where y="y"]) |
118 oops |
233 apply(erule exE)+ |
|
234 apply(rule assms(1)) |
|
235 apply(assumption) |
|
236 apply(erule exE)+ |
|
237 apply(rule assms(2)) |
|
238 apply(assumption) |
|
239 apply(erule exE | erule conjE)? |
|
240 apply(rule assms(3)) |
|
241 apply(drule_tac x="c" in spec) |
|
242 apply(erule exE | erule conjE)+ |
|
243 apply(assumption)+ |
|
244 apply(drule_tac x="c" in spec) |
|
245 apply(erule exE | erule conjE)+ |
|
246 apply(assumption)+ |
|
247 apply(erule exE | erule conjE)+ |
|
248 apply(rule assms(4)) |
|
249 apply(assumption)+ |
|
250 apply(erule exE | erule conjE)+ |
|
251 apply(rule assms(5)) |
|
252 apply(assumption)+ |
|
253 apply(erule exE | erule conjE)+ |
|
254 apply(rule assms(6)) |
|
255 apply(assumption)+ |
|
256 apply(erule exE | erule conjE)+ |
|
257 apply(rule assms(7)) |
|
258 apply(assumption)+ |
|
259 done |
|
260 |
|
261 |
|
262 |
|
263 |
|
264 |
|
265 |
|
266 |
|
267 |
|
268 |
|
269 |
|
270 |
|
271 |
|
272 apply(rule_tac y="y" in foo.exhaust(1)) |
|
273 apply(rule assms(1)) |
|
274 apply(rule exI) |
|
275 apply(assumption) |
|
276 apply(rule assms(2)) |
|
277 apply(rule exI)+ |
|
278 apply(assumption) |
|
279 apply(rule assms(3)) |
|
280 apply(rule_tac p="p" in permute_boolE) |
|
281 apply(perm_simp) |
|
282 apply(simp) |
|
283 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
|
284 apply(erule exE) |
|
285 apply(erule conjE) |
|
286 apply(rule assms(3)) |
|
287 apply(perm_simp) |
|
288 apply(assumption) |
|
289 apply(simp) |
|
290 apply(drule supp_perm_eq[symmetric]) |
|
291 apply(perm_simp) |
|
292 apply(simp) |
|
293 apply(rule at_set_avoiding2) |
|
294 apply(simp add: finite_supp) |
|
295 apply(simp add: finite_supp) |
|
296 apply(simp add: finite_supp) |
|
297 apply(simp add: foo.fresh fresh_star_def) |
|
298 apply(drule Let1_rename_a) |
|
299 apply(erule exE) |
|
300 apply(erule conjE) |
|
301 apply(rule assms(4)) |
|
302 apply(simp only: set_eqvt tt1) |
|
303 apply(assumption) |
|
304 (* |
|
305 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q") |
|
306 apply(erule exE) |
|
307 apply(erule conjE) |
|
308 *) |
|
309 thm assms(5) |
|
310 apply(rule assms(5)) |
|
311 prefer 2 |
|
312 apply(clarify) |
|
313 unfolding foo.eq_iff |
|
314 apply |
|
315 |
119 |
316 lemma strong_exhaust1: |
120 lemma strong_exhaust1: |
317 fixes c::"'a::fs" |
121 fixes c::"'a::fs" |
318 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
122 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
319 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
123 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
321 and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" |
125 and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" |
322 and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" |
126 and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" |
323 and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" |
127 and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" |
324 and "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P" |
128 and "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P" |
325 shows "P" |
129 shows "P" |
326 apply(rule_tac y="y" in foo.exhaust(1)) |
130 oops |
327 apply(rule assms(1)) |
|
328 apply(assumption) |
|
329 apply(rule assms(2)) |
|
330 apply(assumption) |
|
331 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
|
332 apply(erule exE) |
|
333 apply(erule conjE) |
|
334 apply(rule assms(3)) |
|
335 apply(perm_simp) |
|
336 apply(assumption) |
|
337 apply(simp) |
|
338 apply(drule supp_perm_eq[symmetric]) |
|
339 apply(perm_simp) |
|
340 apply(simp) |
|
341 apply(rule at_set_avoiding2) |
|
342 apply(simp add: finite_supp) |
|
343 apply(simp add: finite_supp) |
|
344 apply(simp add: finite_supp) |
|
345 apply(simp add: foo.fresh fresh_star_def) |
|
346 apply(drule Let1_rename_a) |
|
347 apply(erule exE) |
|
348 apply(erule conjE) |
|
349 apply(rule assms(4)) |
|
350 apply(simp only: set_eqvt tt1) |
|
351 apply(assumption) |
|
352 (* |
|
353 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q") |
|
354 apply(erule exE) |
|
355 apply(erule conjE) |
|
356 *) |
|
357 thm assms(5) |
|
358 apply(rule assms(5)) |
|
359 prefer 2 |
|
360 apply(clarify) |
|
361 unfolding foo.eq_iff |
|
362 apply(rule conjI) |
|
363 prefer 2 |
|
364 apply(rule uu2) |
|
365 apply(simp only: tt2[symmetric]) |
|
366 prefer 2 |
|
367 apply(simp only: tt2[symmetric]) |
|
368 |
|
369 apply(simp_all only:)[2] |
|
370 apply(simp add: set_eqvt) |
|
371 apply(simp add: tt2) |
|
372 apply(simp add: foo.eq_iff) |
|
373 apply(drule supp_perm_eq[symmetric]) |
|
374 apply(simp) |
|
375 apply(simp add: tt2 uu2) |
|
376 apply(rule at_set_avoiding2) |
|
377 apply(simp add: finite_supp) |
|
378 apply(simp add: finite_supp) |
|
379 apply(simp add: finite_supp) |
|
380 apply(simp add: Abs_fresh_star) |
|
381 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn3 assg))) \<sharp>* c \<and> supp ([bn3 assg]lst.trm) \<sharp>* q") |
|
382 apply(erule exE) |
|
383 apply(erule conjE) |
|
384 apply(rule assms(6)) |
|
385 apply(simp add: set_eqvt) |
|
386 apply(simp add: tt3) |
|
387 apply(simp add: foo.eq_iff) |
|
388 apply(drule supp_perm_eq[symmetric]) |
|
389 apply(simp) |
|
390 apply(simp add: tt3 uu3) |
|
391 apply(rule at_set_avoiding2) |
|
392 apply(simp add: finite_supp) |
|
393 apply(simp add: finite_supp) |
|
394 apply(simp add: finite_supp) |
|
395 apply(simp add: Abs_fresh_star) |
|
396 apply(subgoal_tac "\<exists>q. (q \<bullet> (bn4 assg')) \<sharp>* c \<and> supp ([bn4 assg']set.trm) \<sharp>* q") |
|
397 apply(erule exE) |
|
398 apply(erule conjE) |
|
399 apply(rule assms(7)) |
|
400 apply(simp add: tt4) |
|
401 apply(simp add: foo.eq_iff) |
|
402 apply(drule supp_perm_eq[symmetric]) |
|
403 apply(simp) |
|
404 apply(simp add: tt4 uu4) |
|
405 apply(rule at_set_avoiding2) |
|
406 apply(simp add: foo.bn_finite) |
|
407 apply(simp add: finite_supp) |
|
408 apply(simp add: finite_supp) |
|
409 apply(simp add: Abs_fresh_star) |
|
410 done |
|
411 |
|
412 thm strong_exhaust1 foo.exhaust(1) |
|
413 |
|
414 |
|
415 |
131 |
416 lemma strong_exhaust2: |
132 lemma strong_exhaust2: |
417 assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" |
133 assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" |
418 shows "P" |
134 shows "P" |
419 apply(rule_tac y="as" in foo.exhaust(2)) |
135 apply(rule_tac y="as" in foo.exhaust(2)) |
446 and a7: "\<And>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" |
162 and a7: "\<And>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" |
447 and a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)" |
163 and a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)" |
448 and a9: "\<And>c. P3 c (BNil)" |
164 and a9: "\<And>c. P3 c (BNil)" |
449 and a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)" |
165 and a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)" |
450 shows "P1 c t" "P2 c as" "P3 c as'" |
166 shows "P1 c t" "P2 c as" "P3 c as'" |
|
167 oops |
|
168 (* |
451 using assms |
169 using assms |
452 apply(induction_schema) |
170 apply(induction_schema) |
453 apply(rule_tac y="t" and c="c" in strong_exhaust1) |
171 apply(rule_tac y="t" and c="c" in strong_exhaust1) |
454 apply(simp_all)[7] |
172 apply(simp_all)[7] |
455 apply(rule_tac as="as" in strong_exhaust2) |
173 apply(rule_tac as="as" in strong_exhaust2) |