instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
authorhuffman
Thu Mar 10 20:19:55 2005 +0100 (2005-03-10)
changeset 1559910cedbd5289e
parent 15598 4ab52355bb53
child 15600 a59f07556a8d
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Up.thy	Thu Mar 10 17:48:36 2005 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Thu Mar 10 20:19:55 2005 +0100
     1.3 @@ -1,6 +1,7 @@
     1.4 -(*  Title:      HOLCF/Up1.thy
     1.5 +(*  Title:      HOLCF/Up.thy
     1.6      ID:         $Id$
     1.7      Author:     Franz Regensburger
     1.8 +                Additions by Brian Huffman
     1.9      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.10  
    1.11  Lifting.
    1.12 @@ -12,13 +13,15 @@
    1.13  imports Cfun Sum_Type Datatype
    1.14  begin
    1.15  
    1.16 +defaultsort cpo
    1.17 +
    1.18  subsection {* Definition of new type for lifting *}
    1.19  
    1.20  typedef (Up) ('a) "u" = "UNIV :: (unit + 'a) set" ..
    1.21  
    1.22  consts
    1.23    Iup         :: "'a => ('a)u"
    1.24 -  Ifup        :: "('a->'b)=>('a)u => 'b"
    1.25 +  Ifup        :: "('a->'b)=>('a)u => 'b::pcpo"
    1.26  
    1.27  defs
    1.28    Iup_def:     "Iup x == Abs_Up(Inr(x))"
    1.29 @@ -140,7 +143,7 @@
    1.30  apply (blast intro: trans_less)
    1.31  done
    1.32  
    1.33 -instance u :: (pcpo) po
    1.34 +instance u :: (cpo) po
    1.35  by intro_classes
    1.36    (assumption | rule refl_less_up antisym_less_up trans_less_up)+
    1.37  
    1.38 @@ -238,17 +241,105 @@
    1.39   lub (range ?Y1) = UU_up
    1.40  *)
    1.41  
    1.42 +text {* New versions where @{typ "'a"} does not have to be a pcpo *}
    1.43 +
    1.44 +lemma up_lemma1a: "EX x. z=Iup(x) ==> Iup(THE a. Iup a = z) = z"
    1.45 +apply (erule exE)
    1.46 +apply (rule theI)
    1.47 +apply (erule sym)
    1.48 +apply simp
    1.49 +apply (erule inject_Iup)
    1.50 +done
    1.51 +
    1.52 +text {* Now some lemmas about chains of @{typ "'a u"} elements *}
    1.53 +
    1.54 +lemma up_chain_lemma1:
    1.55 +  "[| chain Y; EX x. Y j = Iup x |] ==> EX x. Y (i + j) = Iup x"
    1.56 +apply (drule_tac x="j" and y="i + j" in chain_mono3)
    1.57 +apply (rule le_add2)
    1.58 +apply (rule_tac p="Y (i + j)" in upE)
    1.59 +apply auto
    1.60 +done
    1.61 +
    1.62 +lemma up_chain_lemma2:
    1.63 +  "[| chain Y; EX x. Y j = Iup x |] ==>
    1.64 +    Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
    1.65 +apply (drule_tac i=i in up_chain_lemma1)
    1.66 +apply assumption
    1.67 +apply (erule up_lemma1a)
    1.68 +done
    1.69 +
    1.70 +lemma up_chain_lemma3:
    1.71 +  "[| chain Y; EX x. Y j = Iup x |] ==> chain (%i. THE a. Iup a = Y (i + j))"
    1.72 +apply (rule chainI)
    1.73 +apply (rule less_up1c [THEN iffD1])
    1.74 +apply (simp only: up_chain_lemma2)
    1.75 +apply (simp add: chainE)
    1.76 +done
    1.77 +
    1.78 +lemma up_chain_lemma4:
    1.79 +  "[| chain Y; EX x. Y j = Iup x |] ==>
    1.80 +    (%i. Y (i + j)) = (%i. Iup (THE a. Iup a = Y (i + j)))"
    1.81 +apply (rule ext)
    1.82 +apply (rule up_chain_lemma2 [symmetric])
    1.83 +apply assumption+
    1.84 +done
    1.85 +
    1.86 +lemma is_lub_range_shift:
    1.87 +  "[| chain S; range (%i. S (i + j)) <<| x |] ==> range S <<| x"
    1.88 +apply (rule is_lubI)
    1.89 +apply (rule ub_rangeI)
    1.90 +apply (rule trans_less)
    1.91 +apply (erule chain_mono3)
    1.92 +apply (rule le_add1)
    1.93 +apply (erule is_ub_lub)
    1.94 +apply (erule is_lub_lub)
    1.95 +apply (rule ub_rangeI)
    1.96 +apply (erule ub_rangeD)
    1.97 +done
    1.98 +
    1.99 +lemma is_lub_Iup:
   1.100 +  "range S <<| x \<Longrightarrow> range (%i. Iup (S i)) <<| Iup x"
   1.101 +apply (rule is_lubI)
   1.102 +apply (rule ub_rangeI)
   1.103 +apply (subst less_up1c)
   1.104 +apply (erule is_ub_lub)
   1.105 +apply (rule_tac p=u in upE)
   1.106 +apply (drule ub_rangeD)
   1.107 +apply (simp only: less_up1b)
   1.108 +apply (simp only: less_up1c)
   1.109 +apply (erule is_lub_lub)
   1.110 +apply (rule ub_rangeI)
   1.111 +apply (drule_tac i=i in ub_rangeD)
   1.112 +apply (simp only: less_up1c)
   1.113 +done
   1.114 +
   1.115 +lemma lub_up1c: "[|chain(Y); EX x. Y(j)=Iup(x)|]  
   1.116 +      ==> range(Y) <<| Iup(lub(range(%i. THE a. Iup a = Y(i + j))))"
   1.117 +apply (rule_tac j=j in is_lub_range_shift)
   1.118 +apply assumption
   1.119 +apply (subst up_chain_lemma4)
   1.120 +apply assumption+
   1.121 +apply (rule is_lub_Iup)
   1.122 +apply (rule thelubE [OF _ refl])
   1.123 +apply (rule up_chain_lemma3)
   1.124 +apply assumption+
   1.125 +done
   1.126 +
   1.127 +lemmas thelub_up1c = lub_up1c [THEN thelubI, standard]
   1.128 +
   1.129  lemma cpo_up: "chain(Y::nat=>('a)u) ==> EX x. range(Y) <<|x"
   1.130 -apply (case_tac "\<exists> i x. Y i = Iup x")
   1.131 +apply (case_tac "EX i x. Y i = Iup x")
   1.132 +apply (erule exE)
   1.133  apply (rule exI)
   1.134 -apply (erule lub_up1a)
   1.135 +apply (erule lub_up1c)
   1.136  apply assumption
   1.137  apply (rule exI)
   1.138  apply (erule lub_up1b)
   1.139  apply simp
   1.140  done
   1.141  
   1.142 -instance u :: (pcpo) cpo
   1.143 +instance u :: (cpo) cpo
   1.144  by intro_classes (rule cpo_up)
   1.145  
   1.146  subsection {* Type @{typ "'a u"} is pointed *}
   1.147 @@ -263,7 +354,7 @@
   1.148  apply (rule minimal_up [THEN allI])
   1.149  done
   1.150  
   1.151 -instance u :: (pcpo) pcpo
   1.152 +instance u :: (cpo) pcpo
   1.153  by intro_classes (rule least_up)
   1.154  
   1.155  text {* for compatibility with old HOLCF-Version *}
   1.156 @@ -286,25 +377,13 @@
   1.157  
   1.158  text {* continuity for @{term Iup} *}
   1.159  
   1.160 -lemma contlub_Iup: "contlub(Iup)"
   1.161 -apply (rule contlubI [rule_format])
   1.162 -apply (rule trans)
   1.163 -apply (rule_tac [2] thelub_up1a [symmetric])
   1.164 -prefer 3 apply fast
   1.165 -apply (erule_tac [2] monofun_Iup [THEN ch2ch_monofun])
   1.166 -apply (rule_tac f = "Iup" in arg_cong)
   1.167 -apply (rule lub_equal)
   1.168 -apply assumption
   1.169 -apply (rule monofun_Ifup2 [THEN ch2ch_monofun])
   1.170 -apply (erule monofun_Iup [THEN ch2ch_monofun])
   1.171 -apply simp
   1.172 +lemma cont_Iup [iff]: "cont(Iup)"
   1.173 +apply (rule contI [rule_format])
   1.174 +apply (rule is_lub_Iup)
   1.175 +apply (erule thelubE [OF _ refl])
   1.176  done
   1.177  
   1.178 -lemma cont_Iup [iff]: "cont(Iup)"
   1.179 -apply (rule monocontlub2cont)
   1.180 -apply (rule monofun_Iup)
   1.181 -apply (rule contlub_Iup)
   1.182 -done
   1.183 +lemmas contlub_Iup = cont_Iup [THEN cont2contlub]
   1.184  
   1.185  text {* continuity for @{term Ifup} *}
   1.186  
   1.187 @@ -323,16 +402,16 @@
   1.188  
   1.189  lemma contlub_Ifup2: "contlub(Ifup(f))"
   1.190  apply (rule contlubI [rule_format])
   1.191 -apply (rule disjE)
   1.192 -defer 1
   1.193 -apply (subst thelub_up1a)
   1.194 +apply (case_tac "EX i x. Y i = Iup x")
   1.195 +apply (erule exE)
   1.196 +apply (subst thelub_up1c)
   1.197  apply assumption
   1.198  apply assumption
   1.199  apply simp
   1.200  prefer 2
   1.201  apply (subst thelub_up1b)
   1.202  apply assumption
   1.203 -apply assumption
   1.204 +apply simp
   1.205  apply simp
   1.206  apply (rule chain_UU_I_inverse [symmetric])
   1.207  apply (rule allI)
   1.208 @@ -340,28 +419,26 @@
   1.209  apply simp
   1.210  apply simp
   1.211  apply (subst contlub_cfun_arg)
   1.212 -apply  (erule monofun_Ifup2 [THEN ch2ch_monofun])
   1.213 -apply (rule lub_equal2)
   1.214 -apply   (rule_tac [2] monofun_Rep_CFun2 [THEN ch2ch_monofun])
   1.215 -apply   (erule_tac [2] monofun_Ifup2 [THEN ch2ch_monofun])
   1.216 -apply  (erule_tac [2] monofun_Ifup2 [THEN ch2ch_monofun])
   1.217 -apply (rule chain_mono2 [THEN exE])
   1.218 -prefer 2 apply   (assumption)
   1.219 -apply  (erule exE)
   1.220 -apply  (erule exE)
   1.221 -apply  (rule exI)
   1.222 -apply  (rule_tac s = "Iup (x) " and t = "Y (i) " in ssubst)
   1.223 -apply   assumption
   1.224 -apply  (rule defined_Iup2)
   1.225 -apply (rule exI)
   1.226 -apply (intro strip)
   1.227 -apply (rule_tac p = "Y (i) " in upE)
   1.228 -prefer 2 apply simp
   1.229 -apply (rule_tac P = "Y (i) = UU" in notE)
   1.230 -apply  fast
   1.231 -apply (subst inst_up_pcpo)
   1.232 +apply  (erule up_chain_lemma3)
   1.233 +apply  assumption
   1.234 +apply (rule trans)
   1.235 +prefer 2
   1.236 +apply (rule_tac j=i in lub_range_shift)
   1.237 +apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   1.238 +apply (rule lub_equal [rule_format])
   1.239 +apply (rule chain_monofun)
   1.240 +apply (erule up_chain_lemma3)
   1.241  apply assumption
   1.242 -apply fast
   1.243 +apply (rule monofun_Ifup2 [THEN ch2ch_monofun])
   1.244 +apply (erule chain_shift)
   1.245 +apply (drule_tac i=k in up_chain_lemma1)
   1.246 +apply assumption
   1.247 +apply clarify
   1.248 +apply simp
   1.249 +apply (subst the_equality)
   1.250 +apply (rule refl)
   1.251 +apply (erule inject_Iup)
   1.252 +apply (rule refl)
   1.253  done
   1.254  
   1.255  lemma cont_Ifup1: "cont(Ifup)"
   1.256 @@ -381,7 +458,7 @@
   1.257  constdefs  
   1.258          up  :: "'a -> ('a)u"
   1.259         "up  == (LAM x. Iup(x))"
   1.260 -        fup :: "('a->'c)-> ('a)u -> 'c"
   1.261 +        fup :: "('a->'c)-> ('a)u -> 'c::pcpo"
   1.262         "fup == (LAM f p. Ifup(f)(p))"
   1.263  
   1.264  translations