15 apply (simp_all add: fresh_Pair_elim) |
15 apply (simp_all add: fresh_Pair_elim) |
16 apply (rule_tac y="x" in lt.exhaust) |
16 apply (rule_tac y="x" in lt.exhaust) |
17 apply (auto) |
17 apply (auto) |
18 apply (rule_tac x="name" and ?'a="name" in obtain_fresh) |
18 apply (rule_tac x="name" and ?'a="name" in obtain_fresh) |
19 apply (simp_all add: fresh_at_base)[3] |
19 apply (simp_all add: fresh_at_base)[3] |
20 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
21 apply (simp add: fresh_Pair_elim fresh_at_base)[2] |
|
22 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh) |
20 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh) |
23 apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh) |
21 apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh) |
24 apply (rule_tac x="(a, aa)" and ?'a="name" in obtain_fresh) |
22 apply (rule_tac x="(a, aa)" and ?'a="name" in obtain_fresh) |
25 apply (simp add: fresh_Pair_elim fresh_at_base) |
23 apply (simp add: fresh_Pair_elim fresh_at_base) |
|
24 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
25 apply (simp add: fresh_Pair_elim fresh_at_base)[2] |
26 apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base) |
26 apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base) |
27 --"-" |
27 --"-" |
28 apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans) |
28 apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans) |
29 apply (case_tac "k = ka") |
29 apply (case_tac "k = ka") |
30 apply simp |
30 apply simp |
31 apply(simp (no_asm) add: Abs1_eq_iff del:eqvts) |
31 apply(simp (no_asm) add: Abs1_eq_iff del:eqvts) |
32 apply (simp del: eqvts add: lt.fresh fresh_at_base) |
32 apply (simp del: eqvts add: lt.fresh fresh_at_base) |
33 apply (simp only: lt.perm_simps(1) lt.perm_simps(3) flip_def[symmetric] lt.eq_iff(3)) |
33 apply (simp only: lt.perm_simps(1) lt.perm_simps(2) flip_def[symmetric] lt.eq_iff) |
34 apply (subst flip_at_base_simps(2)) |
34 apply (subst flip_at_base_simps(2)) |
35 apply simp |
35 apply simp |
36 apply (intro conjI refl) |
36 apply (intro conjI refl) |
37 apply (rule flip_fresh_fresh[symmetric]) |
37 apply (rule flip_fresh_fresh[symmetric]) |
38 apply (simp_all add: lt.fresh) |
38 apply (simp_all add: lt.fresh) |