213 |
213 |
214 termination |
214 termination |
215 by lexicographic_order |
215 by lexicographic_order |
216 |
216 |
217 definition psi:: "lt => lt" |
217 definition psi:: "lt => lt" |
218 where "psi V == V*(\<lambda>x. x)" |
218 where [simp]: "psi V == V*(\<lambda>x. x)" |
219 |
219 |
220 section {* Simple consequence of CPS *} |
220 section {* Simple consequence of CPS *} |
|
221 |
|
222 lemma [simp]: "eqvt (\<lambda>x\<Colon>lt. x)" |
|
223 by (simp add: eqvt_def eqvt_bound eqvt_lambda) |
221 |
224 |
222 lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)" |
225 lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)" |
223 apply (cases V rule: lt.exhaust) |
226 apply (cases V rule: lt.exhaust) |
224 apply (auto simp add: psi_def) |
227 apply simp_all |
225 apply (subst CPS1.simps) |
|
226 apply (simp add: eqvt_def eqvt_bound eqvt_lambda) |
|
227 apply rule |
|
228 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
228 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
229 apply (subst CPS1.simps(3)) |
229 apply simp |
230 apply assumption+ |
|
231 apply (subst CPS1.simps(3)) |
|
232 apply (simp add: eqvt_def eqvt_bound eqvt_lambda) |
|
233 apply assumption |
|
234 apply rule |
|
235 done |
230 done |
236 |
231 |
|
232 lemma value_eq2 : "isValue V \<Longrightarrow> V^K = K $ (psi V)" |
|
233 apply (cases V rule: lt.exhaust) |
|
234 apply simp_all |
|
235 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
236 apply simp |
|
237 done |
|
238 |
|
239 lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Abs n (k (Var n))))" |
|
240 by (cases M rule: lt.exhaust) auto |
|
241 |
|
242 |
|
243 |
237 end |
244 end |
238 |
245 |
239 |
246 |
240 |
247 |