11 nominal_datatype lm = |
11 nominal_datatype lm = |
12 Vr "name" |
12 Vr "name" |
13 | Ap "lm" "lm" |
13 | Ap "lm" "lm" |
14 | Lm x::"name" l::"lm" bind x in l |
14 | Lm x::"name" l::"lm" bind x in l |
15 |
15 |
16 lemma finite_fv: |
16 lemmas supp_fn' = lm.fv[simplified lm.supp] |
17 shows "finite (fv_lm t)" |
|
18 apply(induct t rule: lm.induct) |
|
19 apply(simp_all) |
|
20 done |
|
21 |
|
22 lemma supp_fn: |
|
23 shows "supp t = fv_lm t" |
|
24 apply(induct t rule: lm.induct) |
|
25 apply(simp_all) |
|
26 apply(simp only: supp_def) |
|
27 apply(simp only: lm.perm) |
|
28 apply(simp only: lm.eq_iff) |
|
29 apply(simp only: supp_def[symmetric]) |
|
30 apply(simp only: supp_at_base) |
|
31 apply(simp (no_asm) only: supp_def) |
|
32 apply(simp only: lm.perm) |
|
33 apply(simp only: lm.eq_iff) |
|
34 apply(simp only: de_Morgan_conj) |
|
35 apply(simp only: Collect_disj_eq) |
|
36 apply(simp only: infinite_Un) |
|
37 apply(simp only: Collect_disj_eq) |
|
38 apply(simp only: supp_def[symmetric]) |
|
39 apply(rule_tac t="supp (Lm name lm)" and s="supp (Abs {atom name} lm)" in subst) |
|
40 apply(simp (no_asm) only: supp_def) |
|
41 apply(simp only: lm.perm) |
|
42 apply(simp only: permute_ABS) |
|
43 apply(simp only: lm.eq_iff) |
|
44 apply(simp only: Abs_eq_iff) |
|
45 apply(simp only: insert_eqvt atom_eqvt empty_eqvt) |
|
46 apply(simp only: alpha_gen) |
|
47 apply(simp only: supp_eqvt[symmetric]) |
|
48 apply(simp only: eqvts) |
|
49 apply(simp only: supp_Abs) |
|
50 done |
|
51 |
|
52 lemmas supp_fn' = lm.fv[simplified supp_fn[symmetric]] |
|
53 |
17 |
54 lemma |
18 lemma |
55 fixes c::"'a::fs" |
19 fixes c::"'a::fs" |
56 assumes a1: "\<And>name c. P c (Vr name)" |
20 assumes a1: "\<And>name c. P c (Vr name)" |
57 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
21 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
65 apply(simp only: lm.perm) |
29 apply(simp only: lm.perm) |
66 apply(rule a2) |
30 apply(rule a2) |
67 apply(blast)[1] |
31 apply(blast)[1] |
68 apply(assumption) |
32 apply(assumption) |
69 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))") |
33 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))") |
|
34 defer |
|
35 apply(simp add: fresh_def) |
|
36 apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base) |
|
37 apply(simp add: supp_Pair finite_supp) |
|
38 apply(blast) |
70 apply(erule exE) |
39 apply(erule exE) |
71 apply(rule_tac t="p \<bullet> Lm name lm" and |
40 apply(rule_tac t="p \<bullet> Lm name lm" and |
72 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst) |
41 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst) |
73 apply(simp del: lm.perm) |
42 apply(simp del: lm.perm) |
74 apply(subst lm.perm) |
43 apply(subst lm.perm) |
136 bi::"bp \<Rightarrow> atom set" |
100 bi::"bp \<Rightarrow> atom set" |
137 where |
101 where |
138 "bi (BP x t) = {atom x}" |
102 "bi (BP x t) = {atom x}" |
139 |
103 |
140 thm lam_bp.fv |
104 thm lam_bp.fv |
|
105 thm lam_bp.supp |
141 thm lam_bp.eq_iff |
106 thm lam_bp.eq_iff |
142 thm lam_bp.bn |
107 thm lam_bp.bn |
143 thm lam_bp.perm |
108 thm lam_bp.perm |
144 thm lam_bp.induct |
109 thm lam_bp.induct |
145 thm lam_bp.inducts |
110 thm lam_bp.inducts |
146 thm lam_bp.distinct |
111 thm lam_bp.distinct |
147 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
112 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
148 |
113 thm lam_bp.fv[simplified lam_bp.supp] |
149 term "supp (x :: lam)" |
|
150 |
|
151 lemma bi_eqvt: |
|
152 shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)" |
|
153 by (rule eqvts) |
|
154 |
|
155 lemma supp_fv: |
|
156 shows "supp t = fv_lam t" |
|
157 and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}" |
|
158 apply(induct t and bp rule: lam_bp.inducts) |
|
159 apply(simp_all) |
|
160 (* VAR case *) |
|
161 apply(simp only: supp_def) |
|
162 apply(simp only: lam_bp.perm) |
|
163 apply(simp only: lam_bp.eq_iff) |
|
164 apply(simp only: supp_def[symmetric]) |
|
165 apply(simp only: supp_at_base) |
|
166 (* APP case *) |
|
167 apply(simp only: supp_def) |
|
168 apply(simp only: lam_bp.perm) |
|
169 apply(simp only: lam_bp.eq_iff) |
|
170 apply(simp only: de_Morgan_conj) |
|
171 apply(simp only: Collect_disj_eq) |
|
172 apply(simp only: infinite_Un) |
|
173 apply(simp only: Collect_disj_eq) |
|
174 (* LAM case *) |
|
175 apply(rule_tac t="supp (LAM name lam)" and s="supp (Abs {atom name} lam)" in subst) |
|
176 apply(simp (no_asm) only: supp_def) |
|
177 apply(simp only: lam_bp.perm) |
|
178 apply(simp only: permute_ABS) |
|
179 apply(simp only: lam_bp.eq_iff) |
|
180 apply(simp only: Abs_eq_iff) |
|
181 apply(simp only: insert_eqvt atom_eqvt empty_eqvt) |
|
182 apply(simp only: alpha_gen) |
|
183 apply(simp only: supp_eqvt[symmetric]) |
|
184 apply(simp only: eqvts) |
|
185 apply(simp only: supp_Abs) |
|
186 (* LET case *) |
|
187 apply(rule_tac t="supp (LET bp lam)" and s="supp (Abs (bi bp) lam) \<union> fv_bi bp" in subst) |
|
188 apply(simp (no_asm) only: supp_def) |
|
189 apply(simp only: lam_bp.perm) |
|
190 apply(simp only: permute_ABS) |
|
191 apply(simp only: lam_bp.eq_iff) |
|
192 apply(simp only: eqvts) |
|
193 apply(simp only: Abs_eq_iff) |
|
194 apply(simp only: ex_simps) |
|
195 apply(simp only: de_Morgan_conj) |
|
196 apply(simp only: Collect_disj_eq) |
|
197 apply(simp only: infinite_Un) |
|
198 apply(simp only: Collect_disj_eq) |
|
199 apply(simp only: alpha_gen) |
|
200 apply(simp only: supp_eqvt[symmetric]) |
|
201 apply(simp only: eqvts) |
|
202 apply(blast) |
|
203 apply(simp add: supp_Abs) |
|
204 apply(blast) |
|
205 (* BP case *) |
|
206 apply(simp only: supp_def) |
|
207 apply(simp only: lam_bp.perm) |
|
208 apply(simp only: lam_bp.eq_iff) |
|
209 apply(simp only: de_Morgan_conj) |
|
210 apply(simp only: Collect_disj_eq) |
|
211 apply(simp only: infinite_Un) |
|
212 apply(simp only: Collect_disj_eq) |
|
213 apply(simp only: supp_def[symmetric]) |
|
214 apply(simp only: supp_at_base) |
|
215 apply(simp) |
|
216 done |
|
217 |
|
218 thm lam_bp.fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
|
219 |
114 |
220 ML {* val _ = recursive := true *} |
115 ML {* val _ = recursive := true *} |
221 |
116 |
222 nominal_datatype lam' = |
117 nominal_datatype lam' = |
223 VAR' "name" |
118 VAR' "name" |
238 thm lam'_bp'.induct |
133 thm lam'_bp'.induct |
239 thm lam'_bp'.inducts |
134 thm lam'_bp'.inducts |
240 thm lam'_bp'.distinct |
135 thm lam'_bp'.distinct |
241 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *} |
136 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *} |
242 |
137 |
243 lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
138 thm lam'_bp'.fv[simplified lam'_bp'.supp] |
244 apply (simp add: supp_Abs supp_Pair) |
|
245 apply blast |
|
246 done |
|
247 |
|
248 lemma supp_fv': |
|
249 shows "supp t = fv_lam' t" |
|
250 and "supp bp = fv_bp' bp" |
|
251 apply(induct t and bp rule: lam'_bp'.inducts) |
|
252 apply(simp_all) |
|
253 (* VAR case *) |
|
254 apply(simp only: supp_def) |
|
255 apply(simp only: lam'_bp'.perm) |
|
256 apply(simp only: lam'_bp'.eq_iff) |
|
257 apply(simp only: supp_def[symmetric]) |
|
258 apply(simp only: supp_at_base) |
|
259 (* APP case *) |
|
260 apply(simp only: supp_def) |
|
261 apply(simp only: lam'_bp'.perm) |
|
262 apply(simp only: lam'_bp'.eq_iff) |
|
263 apply(simp only: de_Morgan_conj) |
|
264 apply(simp only: Collect_disj_eq) |
|
265 apply(simp only: infinite_Un) |
|
266 apply(simp only: Collect_disj_eq) |
|
267 (* LAM case *) |
|
268 apply(rule_tac t="supp (LAM' name lam')" and s="supp (Abs {atom name} lam')" in subst) |
|
269 apply(simp (no_asm) only: supp_def) |
|
270 apply(simp only: lam'_bp'.perm) |
|
271 apply(simp only: permute_ABS) |
|
272 apply(simp only: lam'_bp'.eq_iff) |
|
273 apply(simp only: Abs_eq_iff) |
|
274 apply(simp only: insert_eqvt atom_eqvt empty_eqvt) |
|
275 apply(simp only: alpha_gen) |
|
276 apply(simp only: supp_eqvt[symmetric]) |
|
277 apply(simp only: eqvts) |
|
278 apply(simp only: supp_Abs) |
|
279 (* LET case *) |
|
280 apply(rule_tac t="supp (LET' bp' lam')" and |
|
281 s="supp (Abs (bi' bp') (bp', lam'))" in subst) |
|
282 apply(simp (no_asm) only: supp_def) |
|
283 apply(simp only: lam'_bp'.perm) |
|
284 apply(simp only: permute_ABS) |
|
285 apply(simp only: lam'_bp'.eq_iff) |
|
286 apply(simp only: Abs_eq_iff) |
|
287 apply(simp only: alpha_gen) |
|
288 apply(simp only: eqvts split_def fst_conv snd_conv) |
|
289 apply(simp only: eqvts[symmetric] supp_Pair) |
|
290 apply(simp only: eqvts Pair_eq) |
|
291 apply(simp add: supp_Abs supp_Pair) |
|
292 apply blast |
|
293 apply(simp only: supp_def) |
|
294 apply(simp only: lam'_bp'.perm) |
|
295 apply(simp only: lam'_bp'.eq_iff) |
|
296 apply(simp only: de_Morgan_conj) |
|
297 apply(simp only: Collect_disj_eq) |
|
298 apply(simp only: infinite_Un) |
|
299 apply(simp only: Collect_disj_eq) |
|
300 apply(simp only: supp_def[symmetric]) |
|
301 apply(simp only: supp_at_base supp_atom) |
|
302 apply simp |
|
303 done |
|
304 |
|
305 thm lam'_bp'.fv[simplified supp_fv'[symmetric]] |
|
306 |
139 |
307 |
140 |
308 text {* example 2 *} |
141 text {* example 2 *} |
309 |
142 |
310 ML {* val _ = recursive := false *} |
143 ML {* val _ = recursive := false *} |
328 thm trm'_pat'.eq_iff |
161 thm trm'_pat'.eq_iff |
329 thm trm'_pat'.bn |
162 thm trm'_pat'.bn |
330 thm trm'_pat'.perm |
163 thm trm'_pat'.perm |
331 thm trm'_pat'.induct |
164 thm trm'_pat'.induct |
332 thm trm'_pat'.distinct |
165 thm trm'_pat'.distinct |
333 |
166 thm trm'_pat'.fv[simplified trm'_pat'.supp] |
334 lemma supp_fv_trm'_pat': |
|
335 shows "supp t = fv_trm' t" |
|
336 and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp" |
|
337 apply(induct t and bp rule: trm'_pat'.inducts) |
|
338 apply(simp_all) |
|
339 (* VAR case *) |
|
340 apply(simp only: supp_def) |
|
341 apply(simp only: trm'_pat'.perm) |
|
342 apply(simp only: trm'_pat'.eq_iff) |
|
343 apply(simp only: supp_def[symmetric]) |
|
344 apply(simp only: supp_at_base) |
|
345 (* APP case *) |
|
346 apply(simp only: supp_def) |
|
347 apply(simp only: trm'_pat'.perm) |
|
348 apply(simp only: trm'_pat'.eq_iff) |
|
349 apply(simp only: de_Morgan_conj) |
|
350 apply(simp only: Collect_disj_eq) |
|
351 apply(simp only: infinite_Un) |
|
352 apply(simp only: Collect_disj_eq) |
|
353 (* LAM case *) |
|
354 apply(rule_tac t="supp (Lam name trm')" and s="supp (Abs {atom name} trm')" in subst) |
|
355 apply(simp (no_asm) only: supp_def) |
|
356 apply(simp only: trm'_pat'.perm) |
|
357 apply(simp only: permute_ABS) |
|
358 apply(simp only: trm'_pat'.eq_iff) |
|
359 apply(simp only: Abs_eq_iff) |
|
360 apply(simp only: insert_eqvt atom_eqvt empty_eqvt) |
|
361 apply(simp only: alpha_gen) |
|
362 apply(simp only: supp_eqvt[symmetric]) |
|
363 apply(simp only: eqvts) |
|
364 apply(simp only: supp_Abs) |
|
365 (* LET case *) |
|
366 apply(rule_tac t="supp (Let pat' trm'1 trm'2)" |
|
367 and s="supp (Abs (f pat') trm'2) \<union> supp trm'1 \<union> fv_f pat'" in subst) |
|
368 apply(simp (no_asm) only: supp_def) |
|
369 apply(simp only: trm'_pat'.perm) |
|
370 apply(simp only: permute_ABS) |
|
371 apply(simp only: trm'_pat'.eq_iff) |
|
372 apply(simp only: eqvts) |
|
373 apply(simp only: Abs_eq_iff) |
|
374 apply(simp only: ex_simps) |
|
375 apply(simp only: de_Morgan_conj) |
|
376 apply(simp only: Collect_disj_eq) |
|
377 apply(simp only: infinite_Un) |
|
378 apply(simp only: Collect_disj_eq) |
|
379 apply(simp only: alpha_gen) |
|
380 apply(simp only: supp_eqvt[symmetric]) |
|
381 apply(simp only: eqvts) |
|
382 apply(blast) |
|
383 apply(simp add: supp_Abs) |
|
384 apply(blast) |
|
385 (* PN case *) |
|
386 apply(simp only: supp_def) |
|
387 apply(simp only: trm'_pat'.perm) |
|
388 apply(simp only: trm'_pat'.eq_iff) |
|
389 apply(simp) |
|
390 (* PS case *) |
|
391 apply(simp only: supp_def) |
|
392 apply(simp only: trm'_pat'.perm) |
|
393 apply(simp only: trm'_pat'.eq_iff) |
|
394 apply(simp only: supp_def[symmetric]) |
|
395 apply(simp only: supp_at_base) |
|
396 apply(simp) |
|
397 (* PD case *) |
|
398 apply(simp only: supp_def) |
|
399 apply(simp only: trm'_pat'.perm) |
|
400 apply(simp only: trm'_pat'.eq_iff) |
|
401 apply(simp only: de_Morgan_conj) |
|
402 apply(simp only: Collect_disj_eq) |
|
403 apply(simp only: infinite_Un) |
|
404 apply(simp only: Collect_disj_eq) |
|
405 apply(simp only: supp_def[symmetric]) |
|
406 apply(simp add: supp_at_base) |
|
407 done |
|
408 |
|
409 thm trm'_pat'.fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]] |
|
410 |
167 |
411 nominal_datatype trm0 = |
168 nominal_datatype trm0 = |
412 Var0 "name" |
169 Var0 "name" |
413 | App0 "trm0" "trm0" |
170 | App0 "trm0" "trm0" |
414 | Lam0 x::"name" t::"trm0" bind x in t |
171 | Lam0 x::"name" t::"trm0" bind x in t |
443 thm t_tyS.eq_iff |
201 thm t_tyS.eq_iff |
444 thm t_tyS.bn |
202 thm t_tyS.bn |
445 thm t_tyS.perm |
203 thm t_tyS.perm |
446 thm t_tyS.induct |
204 thm t_tyS.induct |
447 thm t_tyS.distinct |
205 thm t_tyS.distinct |
|
206 thm t_tyS.fv[simplified t_tyS.supp] |
448 |
207 |
449 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
208 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
450 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *} |
209 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *} |
451 |
210 |
452 lemma finite_fv_t_tyS: |
211 |
453 fixes T::"t" |
|
454 and S::"tyS" |
|
455 shows "finite (fv_t T)" |
|
456 and "finite (fv_tyS S)" |
|
457 apply(induct T and S rule: t_tyS.inducts) |
|
458 apply(simp_all add: t_tyS.fv) |
|
459 done |
|
460 |
|
461 lemma supp_fv_t_tyS: |
|
462 shows "supp T = fv_t T" |
|
463 and "supp S = fv_tyS S" |
|
464 apply(induct T and S rule: t_tyS.inducts) |
|
465 apply(simp_all) |
|
466 (* VarTS case *) |
|
467 apply(simp only: supp_def) |
|
468 apply(simp only: t_tyS.perm) |
|
469 apply(simp only: t_tyS.eq_iff) |
|
470 apply(simp only: supp_def[symmetric]) |
|
471 apply(simp only: supp_at_base) |
|
472 (* FunTS case *) |
|
473 apply(simp only: supp_def) |
|
474 apply(simp only: t_tyS.perm) |
|
475 apply(simp only: t_tyS.eq_iff) |
|
476 apply(simp only: de_Morgan_conj) |
|
477 apply(simp only: Collect_disj_eq) |
|
478 apply(simp only: infinite_Un) |
|
479 apply(simp only: Collect_disj_eq) |
|
480 (* All case *) |
|
481 apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst) |
|
482 apply(simp (no_asm) only: supp_def) |
|
483 apply(simp only: t_tyS.perm) |
|
484 apply(simp only: permute_ABS) |
|
485 apply(simp only: t_tyS.eq_iff) |
|
486 apply(simp only: Abs_eq_iff) |
|
487 apply(simp only: eqvts) |
|
488 apply(simp only: alpha_gen) |
|
489 apply(simp only: supp_eqvt[symmetric]) |
|
490 apply(simp only: eqvts eqvts_raw) |
|
491 apply(rule trans) |
|
492 apply(rule finite_supp_Abs) |
|
493 apply(simp add: finite_fv_t_tyS) |
|
494 apply(simp) |
|
495 done |
|
496 |
212 |
497 (* example 1 from Terms.thy *) |
213 (* example 1 from Terms.thy *) |
498 |
|
499 |
|
500 |
|
501 |
214 |
502 |
215 |
503 nominal_datatype trm1 = |
216 nominal_datatype trm1 = |
504 Vr1 "name" |
217 Vr1 "name" |
505 | Ap1 "trm1" "trm1" |
218 | Ap1 "trm1" "trm1" |
543 thm trm3_rassigns3.eq_iff |
257 thm trm3_rassigns3.eq_iff |
544 thm trm3_rassigns3.bn |
258 thm trm3_rassigns3.bn |
545 thm trm3_rassigns3.perm |
259 thm trm3_rassigns3.perm |
546 thm trm3_rassigns3.induct |
260 thm trm3_rassigns3.induct |
547 thm trm3_rassigns3.distinct |
261 thm trm3_rassigns3.distinct |
|
262 thm trm3_rassigns3.fv[simplified trm3_rassigns3.supp] |
548 |
263 |
549 (* example 5 from Terms.thy *) |
264 (* example 5 from Terms.thy *) |
550 |
265 |
551 nominal_datatype trm5 = |
266 nominal_datatype trm5 = |
552 Vr5 "name" |
267 Vr5 "name" |
565 thm trm5_lts.eq_iff |
280 thm trm5_lts.eq_iff |
566 thm trm5_lts.bn |
281 thm trm5_lts.bn |
567 thm trm5_lts.perm |
282 thm trm5_lts.perm |
568 thm trm5_lts.induct |
283 thm trm5_lts.induct |
569 thm trm5_lts.distinct |
284 thm trm5_lts.distinct |
570 |
285 thm trm5_lts.fv[simplified trm5_lts.supp] |
571 lemma |
|
572 shows "fv_trm5 t = supp t" |
|
573 and "fv_lts l = supp l \<and> fv_bv5 l = {a. infinite {b. \<not>alpha_bv5 ((a \<rightleftharpoons> b) \<bullet> l) l}}" |
|
574 apply(induct t and l rule: trm5_lts.inducts) |
|
575 apply(simp_all only: trm5_lts.fv) |
|
576 apply(simp_all only: supp_Abs[symmetric]) |
|
577 (*apply(simp_all only: supp_abs_sum)*) |
|
578 apply(simp_all (no_asm) only: supp_def) |
|
579 apply(simp_all only: trm5_lts.perm) |
|
580 apply(simp_all only: permute_ABS) |
|
581 apply(simp_all only: trm5_lts.eq_iff Abs_eq_iff) |
|
582 (*apply(simp_all only: alpha_gen2)*) |
|
583 apply(simp_all only: alpha_gen) |
|
584 apply(simp_all only: eqvts[symmetric] supp_Pair) |
|
585 apply(simp_all only: eqvts Pair_eq) |
|
586 apply(simp_all only: supp_at_base[symmetric,simplified supp_def]) |
|
587 apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) |
|
588 apply(simp_all only: de_Morgan_conj[symmetric]) |
|
589 apply simp_all |
|
590 done |
|
591 |
|
592 (* example from my PHD *) |
|
593 |
|
594 atom_decl coname |
|
595 |
|
596 nominal_datatype phd = |
|
597 Ax "name" "coname" |
|
598 | Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 |
|
599 | AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 |
|
600 | AndL1 n::"name" t::"phd" "name" bind n in t |
|
601 | AndL2 n::"name" t::"phd" "name" bind n in t |
|
602 | ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 |
|
603 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t |
|
604 |
|
605 thm phd.fv |
|
606 thm phd.eq_iff |
|
607 thm phd.bn |
|
608 thm phd.perm |
|
609 thm phd.induct |
|
610 thm phd.distinct |
|
611 |
286 |
612 (* example form Leroy 96 about modules; OTT *) |
287 (* example form Leroy 96 about modules; OTT *) |
613 |
288 |
614 nominal_datatype mexp = |
289 nominal_datatype mexp = |
615 Acc "path" |
290 Acc "path" |
667 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn |
342 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn |
668 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm |
343 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm |
669 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct |
344 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct |
670 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts |
345 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts |
671 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct |
346 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct |
672 |
347 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp |
673 lemma |
348 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp] |
674 "fv_mexp j = supp j \<and> fv_body k = supp k \<and> |
349 |
675 (fv_defn c = supp c \<and> fv_cbinders c = {a. infinite {b. \<not>alpha_cbinders ((a \<rightleftharpoons> b) \<bullet> c) c}}) \<and> |
350 |
676 fv_sexp d = supp d \<and> fv_sbody e = supp e \<and> |
351 (* example from my PHD *) |
677 (fv_spec l = supp l \<and> fv_Cbinders l = {a. infinite {b. \<not>alpha_Cbinders ((a \<rightleftharpoons> b) \<bullet> l) l}}) \<and> |
352 |
678 fv_tyty g = supp g \<and> fv_path h = supp h \<and> fv_trmtrm i = supp i" |
353 atom_decl coname |
679 apply(induct rule: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct) |
354 |
680 apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv) |
355 nominal_datatype phd = |
681 apply(simp_all only: supp_Abs[symmetric]) |
356 Ax "name" "coname" |
682 apply(simp_all (no_asm) only: supp_def) |
357 | Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 |
683 apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm) |
358 | AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 |
684 apply(simp_all only: permute_ABS) |
359 | AndL1 n::"name" t::"phd" "name" bind n in t |
685 apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff Abs_eq_iff) |
360 | AndL2 n::"name" t::"phd" "name" bind n in t |
686 apply(simp_all only: alpha_gen) |
361 | ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 |
687 apply(simp_all only: eqvts[symmetric] supp_Pair) |
362 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t |
688 apply(simp_all only: eqvts Pair_eq) |
363 |
689 apply(simp_all only: supp_at_base[symmetric,simplified supp_def]) |
364 thm phd.fv |
690 apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) |
365 thm phd.eq_iff |
691 apply(simp_all only: de_Morgan_conj[symmetric]) |
366 thm phd.bn |
692 apply simp_all |
367 thm phd.perm |
693 done |
368 thm phd.induct |
|
369 thm phd.distinct |
|
370 thm phd.fv[simplified phd.supp] |
694 |
371 |
695 (* example 3 from Peter Sewell's bestiary *) |
372 (* example 3 from Peter Sewell's bestiary *) |
696 |
373 |
697 nominal_datatype exp = |
374 nominal_datatype exp = |
698 VarP "name" |
375 VarP "name" |