144 apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *}) |
144 apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *}) |
145 done |
145 done |
146 |
146 |
147 instance trm1 and bp :: fs |
147 instance trm1 and bp :: fs |
148 apply default |
148 apply default |
149 apply (rule rtrm1_bp_fs)+ |
149 apply (simp_all add: rtrm1_bp_fs) |
150 done |
150 done |
151 |
151 |
152 lemma fv_eq_bv_pre: "fv_bp bp = bv1 bp" |
152 lemma fv_eq_bv_pre: "fv_bp bp = bv1 bp" |
153 apply(induct bp rule: trm1_bp_inducts(2)) |
153 apply(induct bp rule: trm1_bp_inducts(2)) |
154 apply(simp_all) |
154 apply(simp_all) |
218 lemma supp_fv_let: |
218 lemma supp_fv_let: |
219 assumes sa : "fv_bp bp = supp bp" |
219 assumes sa : "fv_bp bp = supp bp" |
220 shows "\<lbrakk>fv_trm1 trm11 = supp trm11; fv_trm1 trm12 = supp trm12\<rbrakk> |
220 shows "\<lbrakk>fv_trm1 trm11 = supp trm11; fv_trm1 trm12 = supp trm12\<rbrakk> |
221 \<Longrightarrow> supp (Lt1 bp trm11 trm12) = fv_trm1 (Lt1 bp trm11 trm12)" |
221 \<Longrightarrow> supp (Lt1 bp trm11 trm12) = fv_trm1 (Lt1 bp trm11 trm12)" |
222 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv]) |
222 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv]) |
|
223 apply simp |
223 apply(fold supp_Abs) |
224 apply(fold supp_Abs) |
224 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
225 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
225 apply(simp (no_asm) only: supp_def permute_set_eq permute_trm1 alpha1_INJ) |
226 apply(simp (no_asm) only: supp_def) |
226 apply(simp only: ex_out Collect_neg_conj permute_ABS Abs_eq_iff) |
227 apply(simp only: permute_set_eq permute_trm1) |
227 (*apply(simp only: alpha_bp_eq fv_eq_bv)*) |
228 apply(simp only: alpha1_INJ) |
|
229 apply(simp only: ex_out) |
|
230 apply(simp only: Collect_neg_conj) |
|
231 apply(simp only: permute_ABS) |
|
232 apply(simp only: Abs_eq_iff) |
228 apply(simp only: alpha_gen fv_eq_bv supp_Pair) |
233 apply(simp only: alpha_gen fv_eq_bv supp_Pair) |
|
234 apply(simp only: inf_or[symmetric]) |
|
235 apply(simp only: Collect_disj_eq) |
|
236 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
229 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
237 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
230 apply(simp only: Un_left_commute) |
|
231 apply simp |
|
232 apply(simp add: fresh_star_def) apply(fold fresh_star_def) |
|
233 apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
238 apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
234 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
|
235 apply(simp only: Un_assoc[symmetric]) |
|
236 apply(simp only: Un_commute) |
|
237 apply(simp only: Un_left_commute) |
|
238 apply(simp only: Un_assoc[symmetric]) |
|
239 apply(simp only: Un_commute) |
|
240 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
|
241 apply(simp only: Collect_disj_eq[symmetric] inf_or) |
|
242 apply(simp only: HOL.imp_disj2[symmetric] HOL.not_ex[symmetric] HOL.disj_not1[symmetric] HOL.de_Morgan_conj[symmetric]) |
239 apply(simp only: HOL.imp_disj2[symmetric] HOL.not_ex[symmetric] HOL.disj_not1[symmetric] HOL.de_Morgan_conj[symmetric]) |
243 sorry |
240 sorry |
244 |
241 |
245 lemma supp_fv: |
242 lemma supp_fv: |
246 "supp t = fv_trm1 t" |
243 "supp t = fv_trm1 t" |