src/HOLCF/Up.thy
author huffman
Mon Jan 14 21:42:58 2008 +0100 (2008-01-14)
changeset 25911 cc3f00949986
parent 25906 2179c6661218
child 25921 0ca392ab7f37
permissions -rw-r--r--
added bifinite class instance
     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 Bifinite
    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 subsection {* Lifted cpo is pointed *}
   181 
   182 lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"
   183 apply (rule_tac x = "Ibottom" in exI)
   184 apply (rule minimal_up [THEN allI])
   185 done
   186 
   187 instance u :: (cpo) pcpo
   188 by intro_classes (rule least_up)
   189 
   190 text {* for compatibility with old HOLCF-Version *}
   191 lemma inst_up_pcpo: "\<bottom> = Ibottom"
   192 by (rule minimal_up [THEN UU_I, symmetric])
   193 
   194 subsection {* Continuity of @{term Iup} and @{term Ifup} *}
   195 
   196 text {* continuity for @{term Iup} *}
   197 
   198 lemma cont_Iup: "cont Iup"
   199 apply (rule contI)
   200 apply (rule is_lub_Iup)
   201 apply (erule thelubE [OF _ refl])
   202 done
   203 
   204 text {* continuity for @{term Ifup} *}
   205 
   206 lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
   207 by (induct x, simp_all)
   208 
   209 lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
   210 apply (rule monofunI)
   211 apply (case_tac x, simp)
   212 apply (case_tac y, simp)
   213 apply (simp add: monofun_cfun_arg)
   214 done
   215 
   216 lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
   217 apply (rule contI)
   218 apply (frule up_chain_lemma, safe)
   219 apply (rule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
   220 apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   221 apply (simp add: cont_cfun_arg)
   222 apply (simp add: lub_const)
   223 done
   224 
   225 subsection {* Continuous versions of constants *}
   226 
   227 definition
   228   up  :: "'a \<rightarrow> 'a u" where
   229   "up = (\<Lambda> x. Iup x)"
   230 
   231 definition
   232   fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
   233   "fup = (\<Lambda> f p. Ifup f p)"
   234 
   235 translations
   236   "case l of CONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
   237   "\<Lambda>(CONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
   238 
   239 text {* continuous versions of lemmas for @{typ "('a)u"} *}
   240 
   241 lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
   242 apply (induct z)
   243 apply (simp add: inst_up_pcpo)
   244 apply (simp add: up_def cont_Iup)
   245 done
   246 
   247 lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
   248 by (simp add: up_def cont_Iup)
   249 
   250 lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
   251 by simp
   252 
   253 lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
   254 by (simp add: up_def cont_Iup inst_up_pcpo)
   255 
   256 lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
   257 by simp
   258 
   259 lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
   260 by (simp add: up_def cont_Iup)
   261 
   262 lemma upE [cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   263 apply (cases p)
   264 apply (simp add: inst_up_pcpo)
   265 apply (simp add: up_def cont_Iup)
   266 done
   267 
   268 lemma up_induct [induct type: u]: "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
   269 by (cases x, simp_all)
   270 
   271 text {* lifting preserves chain-finiteness *}
   272 
   273 lemma up_chain_cases:
   274   "chain Y \<Longrightarrow>
   275   (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
   276   (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
   277 by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
   278 
   279 lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
   280 apply (rule compactI2)
   281 apply (drule up_chain_cases, safe)
   282 apply (drule (1) compactD2, simp)
   283 apply (erule exE, rule_tac x="i + j" in exI)
   284 apply simp
   285 apply simp
   286 done
   287 
   288 lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
   289 unfolding compact_def
   290 by (drule adm_subst [OF cont_Rep_CFun2 [where f=up]], simp)
   291 
   292 lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
   293 by (safe elim!: compact_up compact_upD)
   294 
   295 instance u :: (chfin) chfin
   296 apply (intro_classes, clarify)
   297 apply (erule compact_imp_max_in_chain)
   298 apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
   299 done
   300 
   301 text {* properties of fup *}
   302 
   303 lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
   304 by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
   305 
   306 lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
   307 by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2)
   308 
   309 lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
   310 by (cases x, simp_all)
   311 
   312 subsection {* Lifted cpo is a bifinite domain *}
   313 
   314 instance u :: (bifinite_cpo) approx ..
   315 
   316 defs (overloaded)
   317   approx_up_def:
   318     "approx \<equiv> \<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x))"
   319 
   320 instance u :: (bifinite_cpo) bifinite
   321 proof
   322   fix i :: nat and x :: "'a u"
   323   show "chain (\<lambda>i. approx i\<cdot>x)"
   324     unfolding approx_up_def by simp
   325   show "(\<Squnion>i. approx i\<cdot>x) = x"
   326     unfolding approx_up_def
   327     by (simp add: lub_distribs eta_cfun)
   328   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   329     unfolding approx_up_def
   330     by (induct x, simp, simp)
   331   have "{x::'a u. approx i\<cdot>x = x} \<subseteq>
   332         insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x::'a. approx i\<cdot>x = x})"
   333     unfolding approx_up_def
   334     by (rule subsetI, rule_tac p=x in upE, simp_all)
   335   thus "finite {x::'a u. approx i\<cdot>x = x}"
   336     by (rule finite_subset, simp add: finite_fixes_approx)
   337 qed
   338 
   339 lemma approx_up [simp]: "approx i\<cdot>(up\<cdot>x) = up\<cdot>(approx i\<cdot>x)"
   340 unfolding approx_up_def by simp
   341 
   342 end