equal
deleted
inserted
replaced
260 apply (erule_tac x="p" in allE) |
260 apply (erule_tac x="p" in allE) |
261 apply simp |
261 apply simp |
262 apply (simp add: atom_eqvt[symmetric]) |
262 apply (simp add: atom_eqvt[symmetric]) |
263 sorry |
263 sorry |
264 |
264 |
|
265 thm trm1_bp_inducts |
|
266 |
265 lemma supp_fv: |
267 lemma supp_fv: |
266 "supp t = fv_trm1 t" |
268 "supp t = fv_trm1 t" |
267 "supp b = fv_bp b" |
269 "supp b = fv_bp b" |
268 apply(induct t and b rule: trm1_bp_inducts) |
270 apply(induct t and b rule: trm1_bp_inducts) |
269 apply(simp_all) |
271 apply(simp_all) |
278 apply(simp add: Abs_eq_iff) |
280 apply(simp add: Abs_eq_iff) |
279 apply(simp add: alpha_gen.simps) |
281 apply(simp add: alpha_gen.simps) |
280 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
282 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
281 defer |
283 defer |
282 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
284 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
283 apply(simp (no_asm) add: supp_def eqvts) |
285 apply(simp only: supp_at_base[simplified supp_def]) |
284 apply(fold supp_def) |
|
285 apply(simp add: supp_at_base) |
|
286 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) |
286 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) |
287 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) |
287 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) |
288 (*apply(rule supp_fv_let) apply(simp_all)*) |
288 (*apply(rule supp_fv_let) apply(simp_all)*) |
289 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \<union> supp(rtrm11)") |
289 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \<union> supp(rtrm11)") |
290 (*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \<union> supp(rtrm11)")*) |
290 (*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \<union> supp(rtrm11)")*) |
298 apply(simp only: alpha_gen fv_eq_bv supp_Pair) |
298 apply(simp only: alpha_gen fv_eq_bv supp_Pair) |
299 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
299 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
300 apply(simp only: ex_out) |
300 apply(simp only: ex_out) |
301 apply(simp only: Collect_neg_conj finite_Un Diff_cancel) |
301 apply(simp only: Collect_neg_conj finite_Un Diff_cancel) |
302 apply(simp) |
302 apply(simp) |
303 apply(simp add: Collect_imp_eq) |
|
304 apply(simp add: Collect_neg_eq[symmetric] fresh_star_def) |
|
305 apply(fold supp_def) |
303 apply(fold supp_def) |
306 sorry |
304 sorry |
307 |
305 |
308 lemma trm1_supp: |
306 lemma trm1_supp: |
309 "supp (Vr1 x) = {atom x}" |
307 "supp (Vr1 x) = {atom x}" |