104 apply(simp only: supp_at_base) |
104 apply(simp only: supp_at_base) |
105 apply(simp) |
105 apply(simp) |
106 done |
106 done |
107 |
107 |
108 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
108 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
|
109 |
|
110 lemma supports_lam_bp: |
|
111 "(supp (atom a)) supports (VAR a)" |
|
112 "(supp t \<union> supp s) supports (APP t s)" |
|
113 "(supp (atom a) \<union> supp t) supports (LAM a t)" |
|
114 "(supp b \<union> supp t) supports (LET b t)" |
|
115 "(supp (atom a) \<union> supp t) supports (BP a t)" |
|
116 apply - |
|
117 apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *}) |
|
118 apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *}) |
|
119 apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *}) |
|
120 apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *}) |
|
121 apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *}) |
|
122 done |
|
123 |
|
124 lemma finite_supp_lam_bp: |
|
125 fixes lam::"lam" |
|
126 and bp::"bp" |
|
127 shows "finite (supp lam)" |
|
128 and "finite (supp bp)" |
|
129 apply(induct lam and bp rule: lam_bp_inducts) |
|
130 apply(rule supports_finite) |
|
131 apply(rule supports_lam_bp) |
|
132 apply(simp add: supp_atom) |
|
133 apply(rule supports_finite) |
|
134 apply(rule supports_lam_bp) |
|
135 apply(simp) |
|
136 apply(rule supports_finite) |
|
137 apply(rule supports_lam_bp) |
|
138 apply(simp add: supp_atom) |
|
139 apply(rule supports_finite) |
|
140 apply(rule supports_lam_bp) |
|
141 apply(simp) |
|
142 apply(rule supports_finite) |
|
143 apply(rule supports_lam_bp) |
|
144 apply(simp add: supp_atom) |
|
145 done |
|
146 |
109 |
147 |
110 ML {* val _ = cheat_alpha_eqvt := true *} |
148 ML {* val _ = cheat_alpha_eqvt := true *} |
111 ML {* val _ = recursive := true *} |
149 ML {* val _ = recursive := true *} |
112 |
150 |
113 nominal_datatype lam' = |
151 nominal_datatype lam' = |
333 thm t_tyS_distinct |
371 thm t_tyS_distinct |
334 |
372 |
335 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
373 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
336 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *} |
374 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *} |
337 |
375 |
|
376 lemma supports_subset: |
|
377 fixes S1 S2 :: "atom set" |
|
378 assumes a: "S1 supports x" |
|
379 and b: "S1 \<subseteq> S2" |
|
380 shows "S2 supports x" |
|
381 using a b |
|
382 by (auto simp add: supports_def) |
|
383 |
|
384 lemma finite_fv_t_tyS: |
|
385 fixes T::"t" |
|
386 and S::"tyS" |
|
387 shows "finite (fv_t T)" |
|
388 and "finite (fv_tyS S)" |
|
389 apply(induct T and S rule: t_tyS_inducts) |
|
390 apply(simp_all add: t_tyS_fv) |
|
391 done |
|
392 |
338 lemma supp_fv_t_tyS: |
393 lemma supp_fv_t_tyS: |
339 shows "supp T = fv_t T" |
394 shows "supp T = fv_t T" |
340 and "supp S = fv_tyS S" |
395 and "supp S = fv_tyS S" |
341 apply(induct T and S rule: t_tyS_inducts) |
396 apply(induct T and S rule: t_tyS_inducts) |
342 apply(simp_all add: t_tyS_fv) |
397 apply(simp_all add: t_tyS_fv) |
363 apply(simp only: Abs_eq_iff) |
418 apply(simp only: Abs_eq_iff) |
364 apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw) |
419 apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw) |
365 apply(simp only: alpha_gen) |
420 apply(simp only: alpha_gen) |
366 apply(simp only: supp_eqvt[symmetric]) |
421 apply(simp only: supp_eqvt[symmetric]) |
367 apply(simp only: eqvts) |
422 apply(simp only: eqvts) |
368 oops |
423 apply(rule trans) |
369 (*apply(simp only: supp_Abs) |
424 apply(rule finite_supp_Abs) |
370 done*) |
425 apply(simp add: finite_fv_t_tyS) |
|
426 apply(simp) |
|
427 done |
371 |
428 |
372 (* example 1 from Terms.thy *) |
429 (* example 1 from Terms.thy *) |
373 |
430 |
374 nominal_datatype trm1 = |
431 nominal_datatype trm1 = |
375 Vr1 "name" |
432 Vr1 "name" |