equal
deleted
inserted
replaced
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 thm Abs1_eq_iff |
31 thm Abs1_eq_iff |
32 apply(subst Abs1_eq_iff) |
32 apply(subst Abs1_eq_iff) |
33 apply(auto)[2] |
|
34 apply(rule disjI2) |
33 apply(rule disjI2) |
35 apply(rule conjI) |
34 apply(rule conjI) |
36 apply(simp) |
35 apply(simp) |
37 apply(rule conjI) |
36 apply(rule conjI) |
38 apply (simp only: lt.perm_simps(1) lt.perm_simps(2) flip_def[symmetric] lt.eq_iff) |
37 apply (simp only: lt.perm_simps(1) lt.perm_simps(2) flip_def[symmetric] lt.eq_iff) |
128 apply (simp add: fresh_Pair_elim fresh_at_base) |
127 apply (simp add: fresh_Pair_elim fresh_at_base) |
129 apply (auto simp add: Abs1_eq_iff eqvts)[1] |
128 apply (auto simp add: Abs1_eq_iff eqvts)[1] |
130 apply (rename_tac M N u K) |
129 apply (rename_tac M N u K) |
131 apply (subgoal_tac "Lam n (M+ $$ n~ $$ K) = Lam u (M+ $$ u~ $$ K)") |
130 apply (subgoal_tac "Lam n (M+ $$ n~ $$ K) = Lam u (M+ $$ u~ $$ K)") |
132 apply (simp only:) |
131 apply (simp only:) |
133 apply (auto simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)[1] |
132 apply (auto simp add: Abs1_eq_iff flip_fresh_fresh fresh_at_base)[1] |
134 apply (subgoal_tac "Lam m (Na* $$ Lam n (m~ $$ n~ $$ Ka)) = Lam ma (Na* $$ Lam na (ma~ $$ na~ $$ Ka))") |
133 apply (subgoal_tac "Lam m (Na* $$ Lam n (m~ $$ n~ $$ Ka)) = Lam ma (Na* $$ Lam na (ma~ $$ na~ $$ Ka))") |
135 apply (simp only:) |
134 apply (simp only:) |
136 apply (simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base) |
135 apply (simp add: Abs1_eq_iff flip_fresh_fresh fresh_at_base) |
137 apply(simp_all add: flip_def[symmetric]) |
|
138 apply (case_tac "m = ma") |
136 apply (case_tac "m = ma") |
139 apply simp_all |
137 apply simp_all |
140 apply (case_tac "m = na") |
138 apply (case_tac "m = na") |
141 apply(simp_all add: flip_fresh_fresh) |
139 apply(simp_all add: flip_fresh_fresh) |
142 done |
140 done |