166 s="supp (Abs (bi' bp'_raw) (bp'_raw, lam'_raw))" in subst) |
167 s="supp (Abs (bi' bp'_raw) (bp'_raw, lam'_raw))" in subst) |
167 apply(simp (no_asm) only: supp_def) |
168 apply(simp (no_asm) only: supp_def) |
168 apply(simp only: lam'_bp'_perm) |
169 apply(simp only: lam'_bp'_perm) |
169 apply(simp only: permute_ABS) |
170 apply(simp only: permute_ABS) |
170 apply(simp only: lam'_bp'_inject) |
171 apply(simp only: lam'_bp'_inject) |
171 apply(simp only: eqvts) |
|
172 apply(simp only: Abs_eq_iff) |
172 apply(simp only: Abs_eq_iff) |
173 apply(rule Collect_cong) |
173 apply(simp only: alpha_gen) |
174 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
174 apply(simp only: eqvts split_def fst_conv snd_conv) |
175 apply(simp) |
175 apply(simp only: eqvts[symmetric] supp_Pair) |
176 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
176 apply(simp only: eqvts Pair_eq) |
177 apply(simp) |
|
178 apply(rule Collect_cong) |
|
179 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
180 apply(simp) |
|
181 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
182 apply(simp) |
|
183 apply(rule ext) |
|
184 apply(rule sym) |
|
185 apply(subgoal_tac "fv_bp' = supp") |
|
186 apply(subgoal_tac "fv_lam' = supp") |
|
187 apply(simp) |
|
188 apply(rule trans) |
|
189 apply(rule alpha_abs_Pair[symmetric]) |
|
190 apply(simp add: alpha_gen supp_Pair) |
|
191 oops |
177 oops |
192 |
178 |
193 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
179 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
194 |
180 |
195 |
181 |