equal
deleted
inserted
replaced
61 apply clarify |
61 apply clarify |
62 apply (case_tac "k = k'", case_tac [!] "m' = k",case_tac [!]"m = k'",case_tac[!] "m = m'") |
62 apply (case_tac "k = k'", case_tac [!] "m' = k",case_tac [!]"m = k'",case_tac[!] "m = m'") |
63 apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff) |
63 apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff) |
64 by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+ |
64 by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+ |
65 |
65 |
66 termination (eqvt) by lexicographic_order |
66 nominal_termination (eqvt) by lexicographic_order |
67 |
67 |
68 lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim] |
68 lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim] |
69 |
69 |
70 lemma [simp]: "supp (M*) = supp M" |
70 lemma [simp]: "supp (M*) = supp M" |
71 by (induct rule: CPS.induct, simp_all add: lt.supp supp_at_base fresh_at_base fresh_def supp_Pair) |
71 by (induct rule: CPS.induct, simp_all add: lt.supp supp_at_base fresh_at_base fresh_def supp_Pair) |
87 using [[simproc del: alpha_lst]] |
87 using [[simproc del: alpha_lst]] |
88 apply (simp_all) |
88 apply (simp_all) |
89 apply (simp add: Abs1_eq_iff CPS.eqvt) |
89 apply (simp add: Abs1_eq_iff CPS.eqvt) |
90 by blast |
90 by blast |
91 |
91 |
92 termination (eqvt) |
92 nominal_termination (eqvt) |
93 by (relation "measure size") (simp_all) |
93 by (relation "measure size") (simp_all) |
94 |
94 |
95 lemma convert_supp[simp]: |
95 lemma convert_supp[simp]: |
96 shows "supp (M+) = supp M" |
96 shows "supp (M+) = supp M" |
97 by (induct M rule: lt.induct, simp_all add: lt.supp) |
97 by (induct M rule: lt.induct, simp_all add: lt.supp) |
141 apply simp_all |
141 apply simp_all |
142 apply (case_tac "m = na") |
142 apply (case_tac "m = na") |
143 apply(simp_all add: flip_fresh_fresh) |
143 apply(simp_all add: flip_fresh_fresh) |
144 done |
144 done |
145 |
145 |
146 termination (eqvt) |
146 nominal_termination (eqvt) |
147 by (relation "measure (\<lambda>(t, _). size t)") (simp_all) |
147 by (relation "measure (\<lambda>(t, _). size t)") (simp_all) |
148 |
148 |
149 section{* lemma related to Kapply *} |
149 section{* lemma related to Kapply *} |
150 |
150 |
151 lemma [simp]: "isValue V \<Longrightarrow> V; K = K $$ (V+)" |
151 lemma [simp]: "isValue V \<Longrightarrow> V; K = K $$ (V+)" |