479 |
479 |
480 definition |
480 definition |
481 seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" where |
481 seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" where |
482 "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)" |
482 "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)" |
483 |
483 |
484 lemma cont_seq: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)" |
484 lemma cont2cont_if_bottom [cont2cont, simp]: |
485 unfolding cont_def is_lub_def is_ub_def ball_simps |
485 assumes f: "cont (\<lambda>x. f x)" and g: "cont (\<lambda>x. g x)" |
486 by (simp add: lub_eq_bottom_iff) |
486 shows "cont (\<lambda>x. if f x = \<bottom> then \<bottom> else g x)" |
|
487 proof (rule cont_apply [OF f]) |
|
488 show "\<And>x. cont (\<lambda>y. if y = \<bottom> then \<bottom> else g x)" |
|
489 unfolding cont_def is_lub_def is_ub_def ball_simps |
|
490 by (simp add: lub_eq_bottom_iff) |
|
491 show "\<And>y. cont (\<lambda>x. if y = \<bottom> then \<bottom> else g x)" |
|
492 by (simp add: g) |
|
493 qed |
487 |
494 |
488 lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)" |
495 lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)" |
489 unfolding seq_def by (simp add: cont_seq) |
496 unfolding seq_def by simp |
490 |
497 |
491 lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>" |
498 lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>" |
492 by (simp add: seq_conv_if) |
499 by (simp add: seq_conv_if) |
493 |
500 |
494 lemma seq2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID" |
501 lemma seq2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID" |