equal
deleted
inserted
replaced
284 shows "g (flex r f s v) = flex r (g o f) s v" |
284 shows "g (flex r f s v) = flex r (g o f) s v" |
285 apply(induct s arbitrary: g f r v) |
285 apply(induct s arbitrary: g f r v) |
286 apply(simp_all add: comp_def) |
286 apply(simp_all add: comp_def) |
287 by meson |
287 by meson |
288 |
288 |
|
289 lemma flex_fun_apply2: |
|
290 shows "g (flex r id s v) = flex r g s v" |
|
291 by (simp add: flex_fun_apply) |
|
292 |
|
293 |
289 lemma flex_append: |
294 lemma flex_append: |
290 shows "flex r f (s1 @ s2) = flex (ders s1 r) (flex r f s1) s2" |
295 shows "flex r f (s1 @ s2) = flex (ders s1 r) (flex r f s1) s2" |
291 apply(induct s1 arbitrary: s2 r f) |
296 apply(induct s1 arbitrary: s2 r f) |
292 apply(simp_all) |
297 apply(simp_all) |
293 done |
298 done |
395 |
400 |
396 lemma flex_injval: |
401 lemma flex_injval: |
397 shows "flex (der a r) (injval r a) s v = injval r a (flex (der a r) id s v)" |
402 shows "flex (der a r) (injval r a) s v = injval r a (flex (der a r) id s v)" |
398 by (simp add: flex_fun_apply) |
403 by (simp add: flex_fun_apply) |
399 |
404 |
400 |
405 lemma Prf_flex: |
401 |
406 assumes "\<Turnstile> v : ders s r" |
|
407 shows "\<Turnstile> flex r id s v : r" |
|
408 using assms |
|
409 apply(induct s arbitrary: v r) |
|
410 apply(simp) |
|
411 apply(simp) |
|
412 by (simp add: Prf_injval flex_injval) |
|
413 |
402 |
414 |
403 end |
415 end |