195 |
195 |
196 (* TODO: permute_ABS should be in eqvt? *) |
196 (* TODO: permute_ABS should be in eqvt? *) |
197 |
197 |
198 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}" |
198 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}" |
199 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
199 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
|
200 |
|
201 lemma " |
|
202 {a\<Colon>atom. infinite ({b\<Colon>atom. \<not> (\<exists>pi\<Colon>perm. P pi a b \<and> Q pi a b)})} = |
|
203 {a\<Colon>atom. infinite {b\<Colon>atom. \<not> (\<exists>p\<Colon>perm. P p a b)}} \<union> |
|
204 {a\<Colon>atom. infinite {b\<Colon>atom. \<not> (\<exists>p\<Colon>perm. Q p a b)}}" |
|
205 oops |
|
206 |
|
207 lemma inf_or: "(infinite x \<or> infinite y) = infinite (x \<union> y)" |
|
208 by (simp add: finite_Un) |
|
209 |
|
210 |
|
211 lemma supp_fv_let: |
|
212 assumes sa : "fv_bp bp = supp bp" |
|
213 shows "\<lbrakk>fv_trm1 rtrm11 = supp rtrm11; fv_trm1 rtrm12 = supp rtrm12\<rbrakk> |
|
214 \<Longrightarrow> supp (Lt1 bp rtrm11 rtrm12) = fv_trm1 (Lt1 bp rtrm11 rtrm12)" |
|
215 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv]) |
|
216 apply(fold supp_Abs) |
|
217 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
|
218 apply(simp (no_asm) only: supp_def permute_set_eq permute_trm1 alpha1_INJ) |
|
219 apply(simp only: ex_out Collect_neg_conj permute_ABS Abs_eq_iff) |
|
220 apply(simp only: alpha_bp_eq fv_eq_bv) |
|
221 apply(simp only: alpha_gen fv_eq_bv supp_Pair) |
|
222 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
|
223 apply(simp only: Un_left_commute) |
|
224 apply simp |
|
225 apply(simp add: fresh_star_def) apply(fold fresh_star_def) |
|
226 apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
|
227 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
|
228 apply(simp only: Un_assoc[symmetric]) |
|
229 apply(simp only: Un_commute) |
|
230 apply(simp only: Un_left_commute) |
|
231 apply(simp only: Un_assoc[symmetric]) |
|
232 apply(simp only: Un_commute) |
|
233 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
|
234 apply(simp only: Collect_disj_eq[symmetric] inf_or) |
|
235 sorry |
200 |
236 |
201 lemma supp_fv: |
237 lemma supp_fv: |
202 "supp t = fv_trm1 t" |
238 "supp t = fv_trm1 t" |
203 "supp b = fv_bp b" |
239 "supp b = fv_bp b" |
204 apply(induct t and b rule: trm1_bp_inducts) |
240 apply(induct t and b rule: trm1_bp_inducts) |
219 apply(simp (no_asm) add: supp_def eqvts) |
255 apply(simp (no_asm) add: supp_def eqvts) |
220 apply(fold supp_def) |
256 apply(fold supp_def) |
221 apply(simp add: supp_at_base) |
257 apply(simp add: supp_at_base) |
222 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) |
258 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) |
223 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) |
259 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) |
|
260 (*apply(rule supp_fv_let) apply(simp_all)*) |
224 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \<union> supp(rtrm11)") |
261 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \<union> supp(rtrm11)") |
225 (*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \<union> supp(rtrm11)")*) |
262 (*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \<union> supp(rtrm11)")*) |
226 apply(simp add: supp_Abs fv_trm1 supp_Pair Un_Diff Un_assoc fv_eq_bv) |
263 apply(simp add: supp_Abs fv_trm1 supp_Pair Un_Diff Un_assoc fv_eq_bv) |
227 apply(blast) (* Un_commute in a good place *) |
264 apply(blast) (* Un_commute in a good place *) |
228 apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1) |
265 apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1) |