299 |
298 |
300 subsection {* Continuity simplification procedure *} |
299 subsection {* Continuity simplification procedure *} |
301 |
300 |
302 text {* cont2cont lemma for @{term Rep_CFun} *} |
301 text {* cont2cont lemma for @{term Rep_CFun} *} |
303 |
302 |
304 lemma cont2cont_Rep_CFun: |
303 lemma cont2cont_Rep_CFun [cont2cont]: |
305 assumes f: "cont (\<lambda>x. f x)" |
304 assumes f: "cont (\<lambda>x. f x)" |
306 assumes t: "cont (\<lambda>x. t x)" |
305 assumes t: "cont (\<lambda>x. t x)" |
307 shows "cont (\<lambda>x. (f x)\<cdot>(t x))" |
306 shows "cont (\<lambda>x. (f x)\<cdot>(t x))" |
308 proof - |
307 proof - |
309 have "cont (\<lambda>x. Rep_CFun (f x))" |
308 have "cont (\<lambda>x. Rep_CFun (f x))" |
319 \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)" |
318 \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)" |
320 unfolding monofun_def expand_cfun_less by simp |
319 unfolding monofun_def expand_cfun_less by simp |
321 |
320 |
322 text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *} |
321 text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *} |
323 |
322 |
|
323 text {* |
|
324 Not suitable as a cont2cont rule, because on nested lambdas |
|
325 it causes exponential blow-up in the number of subgoals. |
|
326 *} |
|
327 |
324 lemma cont2cont_LAM: |
328 lemma cont2cont_LAM: |
325 assumes f1: "\<And>x. cont (\<lambda>y. f x y)" |
329 assumes f1: "\<And>x. cont (\<lambda>y. f x y)" |
326 assumes f2: "\<And>y. cont (\<lambda>x. f x y)" |
330 assumes f2: "\<And>y. cont (\<lambda>x. f x y)" |
327 shows "cont (\<lambda>x. \<Lambda> y. f x y)" |
331 shows "cont (\<lambda>x. \<Lambda> y. f x y)" |
328 proof (rule cont_Abs_CFun) |
332 proof (rule cont_Abs_CFun) |
329 fix x |
333 fix x |
330 from f1 show "f x \<in> CFun" by (simp add: CFun_def) |
334 from f1 show "f x \<in> CFun" by (simp add: CFun_def) |
331 from f2 show "cont f" by (rule cont2cont_lambda) |
335 from f2 show "cont f" by (rule cont2cont_lambda) |
332 qed |
336 qed |
333 |
337 |
334 text {* continuity simplification procedure *} |
338 text {* |
|
339 This version does work as a cont2cont rule, since it |
|
340 has only a single subgoal. |
|
341 *} |
|
342 |
|
343 lemma cont2cont_LAM' [cont2cont]: |
|
344 fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo" |
|
345 assumes f: "cont (\<lambda>p. f (fst p) (snd p))" |
|
346 shows "cont (\<lambda>x. \<Lambda> y. f x y)" |
|
347 proof (rule cont2cont_LAM) |
|
348 fix x :: 'a |
|
349 have "cont (\<lambda>y. (x, y))" |
|
350 by (rule cont_pair2) |
|
351 with f have "cont (\<lambda>y. f (fst (x, y)) (snd (x, y)))" |
|
352 by (rule cont2cont_app3) |
|
353 thus "cont (\<lambda>y. f x y)" |
|
354 by (simp only: fst_conv snd_conv) |
|
355 next |
|
356 fix y :: 'b |
|
357 have "cont (\<lambda>x. (x, y))" |
|
358 by (rule cont_pair1) |
|
359 with f have "cont (\<lambda>x. f (fst (x, y)) (snd (x, y)))" |
|
360 by (rule cont2cont_app3) |
|
361 thus "cont (\<lambda>x. f x y)" |
|
362 by (simp only: fst_conv snd_conv) |
|
363 qed |
|
364 |
|
365 lemma cont2cont_LAM_discrete [cont2cont]: |
|
366 "(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)" |
|
367 by (simp add: cont2cont_LAM) |
335 |
368 |
336 lemmas cont_lemmas1 = |
369 lemmas cont_lemmas1 = |
337 cont_const cont_id cont_Rep_CFun2 cont2cont_Rep_CFun cont2cont_LAM |
370 cont_const cont_id cont_Rep_CFun2 cont2cont_Rep_CFun cont2cont_LAM |
338 |
|
339 use "Tools/cont_proc.ML"; |
|
340 setup ContProc.setup; |
|
341 |
|
342 (*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*) |
|
343 (*val cont_tacR = (fn i => (REPEAT (cont_tac i)));*) |
|
344 |
371 |
345 subsection {* Miscellaneous *} |
372 subsection {* Miscellaneous *} |
346 |
373 |
347 text {* Monotonicity of @{term Abs_CFun} *} |
374 text {* Monotonicity of @{term Abs_CFun} *} |
348 |
375 |
528 |
555 |
529 lemmas cont_strictify2 = |
556 lemmas cont_strictify2 = |
530 monocontlub2cont [OF monofun_strictify2 contlub_strictify2, standard] |
557 monocontlub2cont [OF monofun_strictify2 contlub_strictify2, standard] |
531 |
558 |
532 lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)" |
559 lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)" |
533 by (unfold strictify_def, simp add: cont_strictify1 cont_strictify2) |
560 unfolding strictify_def |
|
561 by (simp add: cont_strictify1 cont_strictify2 cont2cont_LAM) |
534 |
562 |
535 lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>" |
563 lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>" |
536 by (simp add: strictify_conv_if) |
564 by (simp add: strictify_conv_if) |
537 |
565 |
538 lemma strictify2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strictify\<cdot>f\<cdot>x = f\<cdot>x" |
566 lemma strictify2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strictify\<cdot>f\<cdot>x = f\<cdot>x" |