src/HOLCF/Up.thy
author huffman
Mon Jan 14 03:58:30 2008 +0100 (2008-01-14)
changeset 25898 d8f17d8cf9d4
parent 25879 98b93782c3b1
child 25906 2179c6661218
permissions -rw-r--r--
compact_chfin is now declared simp
     1 (*  Title:      HOLCF/Up.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger and Brian Huffman
     4 
     5 Lifting.
     6 *)
     7 
     8 header {* The type of lifted values *}
     9 
    10 theory Up
    11 imports Cfun
    12 begin
    13 
    14 defaultsort cpo
    15 
    16 subsection {* Definition of new type for lifting *}
    17 
    18 datatype 'a u = Ibottom | Iup 'a
    19 
    20 syntax (xsymbols)
    21   "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
    22 
    23 consts
    24   Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
    25 
    26 primrec
    27   "Ifup f Ibottom = \<bottom>"
    28   "Ifup f (Iup x) = f\<cdot>x"
    29 
    30 subsection {* Ordering on lifted cpo *}
    31 
    32 instantiation u :: (cpo) sq_ord
    33 begin
    34 
    35 definition
    36   less_up_def:
    37     "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
    38       (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
    39 
    40 instance ..
    41 end
    42 
    43 lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
    44 by (simp add: less_up_def)
    45 
    46 lemma not_Iup_less [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
    47 by (simp add: less_up_def)
    48 
    49 lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
    50 by (simp add: less_up_def)
    51 
    52 subsection {* Lifted cpo is a partial order *}
    53 
    54 instance u :: (cpo) po
    55 proof
    56   fix x :: "'a u"
    57   show "x \<sqsubseteq> x"
    58     unfolding less_up_def by (simp split: u.split)
    59 next
    60   fix x y :: "'a u"
    61   assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
    62     unfolding less_up_def
    63     by (auto split: u.split_asm intro: antisym_less)
    64 next
    65   fix x y z :: "'a u"
    66   assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    67     unfolding less_up_def
    68     by (auto split: u.split_asm intro: trans_less)
    69 qed
    70 
    71 lemma u_UNIV: "UNIV = insert Ibottom (range Iup)"
    72 by (auto, case_tac x, auto)
    73 
    74 instance u :: (finite_po) finite_po
    75 by (intro_classes, simp add: u_UNIV)
    76 
    77 
    78 subsection {* Lifted cpo is a cpo *}
    79 
    80 lemma is_lub_Iup:
    81   "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
    82 apply (rule is_lubI)
    83 apply (rule ub_rangeI)
    84 apply (subst Iup_less)
    85 apply (erule is_ub_lub)
    86 apply (case_tac u)
    87 apply (drule ub_rangeD)
    88 apply simp
    89 apply simp
    90 apply (erule is_lub_lub)
    91 apply (rule ub_rangeI)
    92 apply (drule_tac i=i in ub_rangeD)
    93 apply simp
    94 done
    95 
    96 lemma is_lub_Iup': "\<lbrakk>directed S; S <<| x\<rbrakk> \<Longrightarrow> (Iup ` S) <<| Iup x"
    97 apply (rule is_lubI)
    98 apply (rule ub_imageI)
    99 apply (subst Iup_less)
   100 apply (erule (1) is_ubD [OF is_lubD1])
   101 apply (case_tac u)
   102 apply (drule directedD1, erule exE)
   103 apply (drule (1) ub_imageD)
   104 apply simp
   105 apply simp
   106 apply (erule is_lub_lub)
   107 apply (rule is_ubI)
   108 apply (drule (1) ub_imageD)
   109 apply simp
   110 done
   111 
   112 text {* Now some lemmas about chains of @{typ "'a u"} elements *}
   113 
   114 lemma up_lemma1: "z \<noteq> Ibottom \<Longrightarrow> Iup (THE a. Iup a = z) = z"
   115 by (case_tac z, simp_all)
   116 
   117 lemma up_lemma2:
   118   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom"
   119 apply (erule contrapos_nn)
   120 apply (drule_tac x="j" and y="i + j" in chain_mono3)
   121 apply (rule le_add2)
   122 apply (case_tac "Y j")
   123 apply assumption
   124 apply simp
   125 done
   126 
   127 lemma up_lemma3:
   128   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
   129 by (rule up_lemma1 [OF up_lemma2])
   130 
   131 lemma up_lemma4:
   132   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
   133 apply (rule chainI)
   134 apply (rule Iup_less [THEN iffD1])
   135 apply (subst up_lemma3, assumption+)+
   136 apply (simp add: chainE)
   137 done
   138 
   139 lemma up_lemma5:
   140   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow>
   141     (\<lambda>i. Y (i + j)) = (\<lambda>i. Iup (THE a. Iup a = Y (i + j)))"
   142 by (rule ext, rule up_lemma3 [symmetric])
   143 
   144 lemma up_lemma6:
   145   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>
   146       \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
   147 apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
   148 apply assumption
   149 apply (subst up_lemma5, assumption+)
   150 apply (rule is_lub_Iup)
   151 apply (rule thelubE [OF _ refl])
   152 apply (erule (1) up_lemma4)
   153 done
   154 
   155 lemma up_chain_lemma:
   156   "chain Y \<Longrightarrow>
   157    (\<exists>A. chain A \<and> lub (range Y) = Iup (lub (range A)) \<and>
   158    (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
   159 apply (rule disjCI)
   160 apply (simp add: expand_fun_eq)
   161 apply (erule exE, rename_tac j)
   162 apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
   163 apply (simp add: up_lemma4)
   164 apply (simp add: up_lemma6 [THEN thelubI])
   165 apply (rule_tac x=j in exI)
   166 apply (simp add: up_lemma3)
   167 done
   168 
   169 lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
   170 apply (frule up_chain_lemma, safe)
   171 apply (rule_tac x="Iup (lub (range A))" in exI)
   172 apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
   173 apply (simp add: is_lub_Iup thelubE)
   174 apply (rule exI, rule lub_const)
   175 done
   176 
   177 instance u :: (cpo) cpo
   178 by intro_classes (rule cpo_up)
   179 
   180 lemma up_directed_lemma:
   181   "directed (S::'a::dcpo u set) \<Longrightarrow>
   182     (directed (Iup -` S) \<and> S <<| Iup (lub (Iup -` S))) \<or>
   183     S = {Ibottom}"
   184 apply (case_tac "\<exists>x. Iup x \<in> S")
   185 apply (rule disjI1)
   186 apply (subgoal_tac "directed (Iup -` S)")
   187 apply (rule conjI, assumption)
   188 apply (rule is_lubI)
   189 apply (rule is_ubI)
   190 apply (case_tac x, simp, simp)
   191 apply (erule is_ub_thelub', simp)
   192 apply (case_tac u)
   193 apply (erule exE)
   194 apply (drule (1) is_ubD)
   195 apply simp
   196 apply simp
   197 apply (erule is_lub_thelub')
   198 apply (rule is_ubI, simp)
   199 apply (drule (1) is_ubD, simp)
   200 apply (rule directedI)
   201 apply (erule exE)
   202 apply (rule exI)
   203 apply (erule vimageI2)
   204 apply simp
   205 apply (drule_tac x="Iup x" and y="Iup y" in directedD2, assumption+)
   206 apply (erule bexE, rename_tac z)
   207 apply (case_tac z)
   208 apply simp
   209 apply (rule_tac x=a in bexI)
   210 apply simp
   211 apply simp
   212 apply (rule disjI2)
   213 apply (simp, safe)
   214 apply (case_tac x, simp, simp)
   215 apply (drule directedD1)
   216 apply (clarify, rename_tac x)
   217 apply (case_tac x, simp, simp)
   218 done
   219 
   220 lemma dcpo_up: "directed (S::'a::dcpo u set) \<Longrightarrow> \<exists>x. S <<| x"
   221 apply (frule up_directed_lemma, safe)
   222 apply (erule exI)
   223 apply (rule exI, rule is_lub_singleton)
   224 done
   225 
   226 instance u :: (dcpo) dcpo
   227 by intro_classes (rule dcpo_up)
   228 
   229 subsection {* Lifted cpo is pointed *}
   230 
   231 lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"
   232 apply (rule_tac x = "Ibottom" in exI)
   233 apply (rule minimal_up [THEN allI])
   234 done
   235 
   236 instance u :: (cpo) pcpo
   237 by intro_classes (rule least_up)
   238 
   239 text {* for compatibility with old HOLCF-Version *}
   240 lemma inst_up_pcpo: "\<bottom> = Ibottom"
   241 by (rule minimal_up [THEN UU_I, symmetric])
   242 
   243 subsection {* Continuity of @{term Iup} and @{term Ifup} *}
   244 
   245 text {* continuity for @{term Iup} *}
   246 
   247 lemma cont_Iup: "cont Iup"
   248 apply (rule contI)
   249 apply (rule is_lub_Iup)
   250 apply (erule thelubE [OF _ refl])
   251 done
   252 
   253 text {* continuity for @{term Ifup} *}
   254 
   255 lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
   256 by (induct x, simp_all)
   257 
   258 lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
   259 apply (rule monofunI)
   260 apply (case_tac x, simp)
   261 apply (case_tac y, simp)
   262 apply (simp add: monofun_cfun_arg)
   263 done
   264 
   265 lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
   266 apply (rule contI)
   267 apply (frule up_chain_lemma, safe)
   268 apply (rule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
   269 apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   270 apply (simp add: cont_cfun_arg)
   271 apply (simp add: lub_const)
   272 done
   273 
   274 subsection {* Continuous versions of constants *}
   275 
   276 definition
   277   up  :: "'a \<rightarrow> 'a u" where
   278   "up = (\<Lambda> x. Iup x)"
   279 
   280 definition
   281   fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
   282   "fup = (\<Lambda> f p. Ifup f p)"
   283 
   284 translations
   285   "case l of CONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
   286   "\<Lambda>(CONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
   287 
   288 text {* continuous versions of lemmas for @{typ "('a)u"} *}
   289 
   290 lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
   291 apply (induct z)
   292 apply (simp add: inst_up_pcpo)
   293 apply (simp add: up_def cont_Iup)
   294 done
   295 
   296 lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
   297 by (simp add: up_def cont_Iup)
   298 
   299 lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
   300 by simp
   301 
   302 lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
   303 by (simp add: up_def cont_Iup inst_up_pcpo)
   304 
   305 lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
   306 by simp
   307 
   308 lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
   309 by (simp add: up_def cont_Iup)
   310 
   311 lemma upE [cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   312 apply (cases p)
   313 apply (simp add: inst_up_pcpo)
   314 apply (simp add: up_def cont_Iup)
   315 done
   316 
   317 lemma up_induct [induct type: u]: "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
   318 by (cases x, simp_all)
   319 
   320 text {* lifting preserves chain-finiteness *}
   321 
   322 lemma up_chain_cases:
   323   "chain Y \<Longrightarrow>
   324   (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
   325   (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
   326 by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
   327 
   328 lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
   329 apply (rule compactI2)
   330 apply (drule up_chain_cases, safe)
   331 apply (drule (1) compactD2, simp)
   332 apply (erule exE, rule_tac x="i + j" in exI)
   333 apply simp
   334 apply simp
   335 done
   336 
   337 lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
   338 unfolding compact_def
   339 by (drule adm_subst [OF cont_Rep_CFun2 [where f=up]], simp)
   340 
   341 lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
   342 by (safe elim!: compact_up compact_upD)
   343 
   344 instance u :: (chfin) chfin
   345 apply (intro_classes, clarify)
   346 apply (erule compact_imp_max_in_chain)
   347 apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
   348 done
   349 
   350 text {* properties of fup *}
   351 
   352 lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
   353 by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
   354 
   355 lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
   356 by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2)
   357 
   358 lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
   359 by (cases x, simp_all)
   360 
   361 end