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 _ = recursive := true *} |
148 ML {* val _ = recursive := true *} |
111 |
149 |
112 nominal_datatype lam' = |
150 nominal_datatype lam' = |
113 VAR' "name" |
151 VAR' "name" |
332 thm t_tyS_distinct |
370 thm t_tyS_distinct |
333 |
371 |
334 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
372 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
335 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *} |
373 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *} |
336 |
374 |
|
375 lemma supports_subset: |
|
376 fixes S1 S2 :: "atom set" |
|
377 assumes a: "S1 supports x" |
|
378 and b: "S1 \<subseteq> S2" |
|
379 shows "S2 supports x" |
|
380 using a b |
|
381 by (auto simp add: supports_def) |
|
382 |
|
383 lemma finite_fv_t_tyS: |
|
384 fixes T::"t" |
|
385 and S::"tyS" |
|
386 shows "finite (fv_t T)" |
|
387 and "finite (fv_tyS S)" |
|
388 apply(induct T and S rule: t_tyS_inducts) |
|
389 apply(simp_all add: t_tyS_fv) |
|
390 done |
|
391 |
337 lemma supp_fv_t_tyS: |
392 lemma supp_fv_t_tyS: |
338 shows "supp T = fv_t T" |
393 shows "supp T = fv_t T" |
339 and "supp S = fv_tyS S" |
394 and "supp S = fv_tyS S" |
340 apply(induct T and S rule: t_tyS_inducts) |
395 apply(induct T and S rule: t_tyS_inducts) |
341 apply(simp_all add: t_tyS_fv) |
396 apply(simp_all add: t_tyS_fv) |
362 apply(simp only: Abs_eq_iff) |
417 apply(simp only: Abs_eq_iff) |
363 apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw) |
418 apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw) |
364 apply(simp only: alpha_gen) |
419 apply(simp only: alpha_gen) |
365 apply(simp only: supp_eqvt[symmetric]) |
420 apply(simp only: supp_eqvt[symmetric]) |
366 apply(simp only: eqvts) |
421 apply(simp only: eqvts) |
367 oops |
422 apply(rule trans) |
368 (*apply(simp only: supp_Abs) |
423 apply(rule finite_supp_Abs) |
369 done*) |
424 apply(simp add: finite_fv_t_tyS) |
|
425 apply(simp) |
|
426 done |
370 |
427 |
371 (* example 1 from Terms.thy *) |
428 (* example 1 from Terms.thy *) |
372 |
429 |
373 nominal_datatype trm1 = |
430 nominal_datatype trm1 = |
374 Vr1 "name" |
431 Vr1 "name" |