src/HOLCF/Cfun.thy
changeset 16093 cdcbf5a7f38d
parent 16085 c004b9bc970e
child 16094 a92ee2833938
equal deleted inserted replaced
16092:a1a481ee9425 16093:cdcbf5a7f38d
   630 
   630 
   631 lemma contlub_Istrictify1: "contlub (\<lambda>f. Istrictify f x)"
   631 lemma contlub_Istrictify1: "contlub (\<lambda>f. Istrictify f x)"
   632 apply (rule contlubI [rule_format])
   632 apply (rule contlubI [rule_format])
   633 apply (case_tac "x = \<bottom>")
   633 apply (case_tac "x = \<bottom>")
   634 apply (simp add: Istrictify1)
   634 apply (simp add: Istrictify1)
   635 apply (simp add: lub_const [THEN thelubI])
   635 apply (simp add: thelub_const)
   636 apply (simp add: Istrictify2)
   636 apply (simp add: Istrictify2)
   637 apply (erule contlub_cfun_fun)
   637 apply (erule contlub_cfun_fun)
   638 done
   638 done
   639 
   639 
   640 lemma contlub_Istrictify2: "contlub (\<lambda>x. Istrictify f x)"
   640 lemma contlub_Istrictify2: "contlub (\<lambda>x. Istrictify f x)"
   641 apply (rule contlubI [rule_format])
   641 apply (rule contlubI [rule_format])
   642 apply (case_tac "lub (range Y) = \<bottom>")
   642 apply (case_tac "lub (range Y) = \<bottom>")
   643 apply (simp add: Istrictify1 chain_UU_I)
   643 apply (simp add: Istrictify1 chain_UU_I)
   644 apply (simp add: lub_const [THEN thelubI])
   644 apply (simp add: thelub_const)
   645 apply (simp add: Istrictify2)
   645 apply (simp add: Istrictify2)
   646 apply (simp add: contlub_cfun_arg)
   646 apply (simp add: contlub_cfun_arg)
   647 apply (rule lub_equal2)
   647 apply (rule lub_equal2)
   648 apply (rule chain_mono2 [THEN exE])
   648 apply (rule chain_mono2 [THEN exE])
   649 apply (erule chain_UU_I_inverse2)
   649 apply (erule chain_UU_I_inverse2)