add lemma cpo_lubI
authorhuffman
Thu Jan 31 21:48:14 2008 +0100 (2008-01-31)
changeset 2602787cb69d27558
parent 26026 f9647c040b58
child 26028 74668c3a8f70
add lemma cpo_lubI
src/HOLCF/Cont.thy
src/HOLCF/Cprod.thy
src/HOLCF/Pcpodef.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Cont.thy	Thu Jan 31 21:37:20 2008 +0100
     1.2 +++ b/src/HOLCF/Cont.thy	Thu Jan 31 21:48:14 2008 +0100
     1.3 @@ -165,7 +165,7 @@
     1.4  apply (erule ch2ch_monofun [OF mono])
     1.5  apply (rule ub2ub_monofun [OF mono])
     1.6  apply (rule is_lubD1)
     1.7 -apply (erule thelubE, rule refl)
     1.8 +apply (erule cpo_lubI)
     1.9  done
    1.10  
    1.11  subsection {* Continuity of basic functions *}
    1.12 @@ -174,8 +174,7 @@
    1.13  
    1.14  lemma cont_id: "cont (\<lambda>x. x)"
    1.15  apply (rule contI)
    1.16 -apply (erule thelubE)
    1.17 -apply (rule refl)
    1.18 +apply (erule cpo_lubI)
    1.19  done
    1.20  
    1.21  text {* constant functions are continuous *}
     2.1 --- a/src/HOLCF/Cprod.thy	Thu Jan 31 21:37:20 2008 +0100
     2.2 +++ b/src/HOLCF/Cprod.thy	Thu Jan 31 21:48:14 2008 +0100
     2.3 @@ -111,11 +111,11 @@
     2.4    have "chain (\<lambda>i. fst (S i))"
     2.5      using monofun_fst S by (rule ch2ch_monofun)
     2.6    hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
     2.7 -    by (rule thelubE [OF _ refl])
     2.8 +    by (rule cpo_lubI)
     2.9    have "chain (\<lambda>i. snd (S i))"
    2.10      using monofun_snd S by (rule ch2ch_monofun)
    2.11    hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
    2.12 -    by (rule thelubE [OF _ refl])
    2.13 +    by (rule cpo_lubI)
    2.14    show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
    2.15      using is_lub_Pair [OF 1 2] by simp
    2.16  qed
    2.17 @@ -161,7 +161,7 @@
    2.18  lemma cont_pair1: "cont (\<lambda>x. (x, y))"
    2.19  apply (rule contI)
    2.20  apply (rule is_lub_Pair)
    2.21 -apply (erule thelubE [OF _ refl])
    2.22 +apply (erule cpo_lubI)
    2.23  apply (rule lub_const)
    2.24  done
    2.25  
    2.26 @@ -169,7 +169,7 @@
    2.27  apply (rule contI)
    2.28  apply (rule is_lub_Pair)
    2.29  apply (rule lub_const)
    2.30 -apply (erule thelubE [OF _ refl])
    2.31 +apply (erule cpo_lubI)
    2.32  done
    2.33  
    2.34  lemma contlub_fst: "contlub fst"
     3.1 --- a/src/HOLCF/Pcpodef.thy	Thu Jan 31 21:37:20 2008 +0100
     3.2 +++ b/src/HOLCF/Pcpodef.thy	Thu Jan 31 21:48:14 2008 +0100
     3.3 @@ -151,7 +151,7 @@
     3.4   apply (rule contI)
     3.5   apply (simp only: typedef_thelub [OF type less adm])
     3.6   apply (simp only: Abs_inverse_lub_Rep [OF type less adm])
     3.7 - apply (rule thelubE [OF _ refl])
     3.8 + apply (rule cpo_lubI)
     3.9   apply (erule ch2ch_Rep [OF less])
    3.10  done
    3.11  
     4.1 --- a/src/HOLCF/Up.thy	Thu Jan 31 21:37:20 2008 +0100
     4.2 +++ b/src/HOLCF/Up.thy	Thu Jan 31 21:48:14 2008 +0100
     4.3 @@ -148,7 +148,7 @@
     4.4  apply assumption
     4.5  apply (subst up_lemma5, assumption+)
     4.6  apply (rule is_lub_Iup)
     4.7 -apply (rule thelubE [OF _ refl])
     4.8 +apply (rule cpo_lubI)
     4.9  apply (erule (1) up_lemma4)
    4.10  done
    4.11  
    4.12 @@ -170,7 +170,7 @@
    4.13  apply (frule up_chain_lemma, safe)
    4.14  apply (rule_tac x="Iup (lub (range A))" in exI)
    4.15  apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
    4.16 -apply (simp add: is_lub_Iup thelubE)
    4.17 +apply (simp add: is_lub_Iup cpo_lubI)
    4.18  apply (rule exI, rule lub_const)
    4.19  done
    4.20  
    4.21 @@ -198,7 +198,7 @@
    4.22  lemma cont_Iup: "cont Iup"
    4.23  apply (rule contI)
    4.24  apply (rule is_lub_Iup)
    4.25 -apply (erule thelubE [OF _ refl])
    4.26 +apply (erule cpo_lubI)
    4.27  done
    4.28  
    4.29  text {* continuity for @{term Ifup} *}