482 subsection {* Strictified functions *} |
482 subsection {* Strictified functions *} |
483 |
483 |
484 default_sort pcpo |
484 default_sort pcpo |
485 |
485 |
486 definition |
486 definition |
487 strict :: "'a \<rightarrow> 'b \<rightarrow> 'b" where |
487 seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" where |
488 "strict = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)" |
488 "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)" |
489 |
489 |
490 lemma cont_strict: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)" |
490 lemma cont_seq: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)" |
491 unfolding cont_def is_lub_def is_ub_def ball_simps |
491 unfolding cont_def is_lub_def is_ub_def ball_simps |
492 by (simp add: lub_eq_bottom_iff) |
492 by (simp add: lub_eq_bottom_iff) |
493 |
493 |
494 lemma strict_conv_if: "strict\<cdot>x = (if x = \<bottom> then \<bottom> else ID)" |
494 lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)" |
495 unfolding strict_def by (simp add: cont_strict) |
495 unfolding seq_def by (simp add: cont_seq) |
496 |
496 |
497 lemma strict1 [simp]: "strict\<cdot>\<bottom> = \<bottom>" |
497 lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>" |
498 by (simp add: strict_conv_if) |
498 by (simp add: seq_conv_if) |
499 |
499 |
500 lemma strict2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strict\<cdot>x = ID" |
500 lemma seq2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID" |
501 by (simp add: strict_conv_if) |
501 by (simp add: seq_conv_if) |
502 |
502 |
503 lemma strict3 [simp]: "strict\<cdot>x\<cdot>\<bottom> = \<bottom>" |
503 lemma seq3 [simp]: "seq\<cdot>x\<cdot>\<bottom> = \<bottom>" |
504 by (simp add: strict_conv_if) |
504 by (simp add: seq_conv_if) |
505 |
505 |
506 definition |
506 definition |
507 strictify :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where |
507 strictify :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where |
508 "strictify = (\<Lambda> f x. strict\<cdot>x\<cdot>(f\<cdot>x))" |
508 "strictify = (\<Lambda> f x. seq\<cdot>x\<cdot>(f\<cdot>x))" |
509 |
509 |
510 lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)" |
510 lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)" |
511 unfolding strictify_def by simp |
511 unfolding strictify_def by simp |
512 |
512 |
513 lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>" |
513 lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>" |