src/HOL/HOLCF/Up.thy
author blanchet
Thu Sep 11 19:32:36 2014 +0200 (2014-09-11)
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 58880 0baae4311a9f
permissions -rw-r--r--
updated news
     1 (*  Title:      HOL/HOLCF/Up.thy
     2     Author:     Franz Regensburger
     3     Author:     Brian Huffman
     4 *)
     5 
     6 header {* The type of lifted values *}
     7 
     8 theory Up
     9 imports Cfun
    10 begin
    11 
    12 default_sort cpo
    13 
    14 subsection {* Definition of new type for lifting *}
    15 
    16 datatype 'a u = Ibottom | Iup 'a
    17 
    18 type_notation (xsymbols)
    19   u  ("(_\<^sub>\<bottom>)" [1000] 999)
    20 
    21 primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
    22     "Ifup f Ibottom = \<bottom>"
    23  |  "Ifup f (Iup x) = f\<cdot>x"
    24 
    25 subsection {* Ordering on lifted cpo *}
    26 
    27 instantiation u :: (cpo) below
    28 begin
    29 
    30 definition
    31   below_up_def:
    32     "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
    33       (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
    34 
    35 instance ..
    36 end
    37 
    38 lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
    39 by (simp add: below_up_def)
    40 
    41 lemma not_Iup_below [iff]: "Iup x \<notsqsubseteq> Ibottom"
    42 by (simp add: below_up_def)
    43 
    44 lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
    45 by (simp add: below_up_def)
    46 
    47 subsection {* Lifted cpo is a partial order *}
    48 
    49 instance u :: (cpo) po
    50 proof
    51   fix x :: "'a u"
    52   show "x \<sqsubseteq> x"
    53     unfolding below_up_def by (simp split: u.split)
    54 next
    55   fix x y :: "'a u"
    56   assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
    57     unfolding below_up_def
    58     by (auto split: u.split_asm intro: below_antisym)
    59 next
    60   fix x y z :: "'a u"
    61   assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    62     unfolding below_up_def
    63     by (auto split: u.split_asm intro: below_trans)
    64 qed
    65 
    66 subsection {* Lifted cpo is a cpo *}
    67 
    68 lemma is_lub_Iup:
    69   "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
    70 unfolding is_lub_def is_ub_def ball_simps
    71 by (auto simp add: below_up_def split: u.split)
    72 
    73 lemma up_chain_lemma:
    74   assumes Y: "chain Y" obtains "\<forall>i. Y i = Ibottom"
    75   | A k where "\<forall>i. Iup (A i) = Y (i + k)" and "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
    76 proof (cases "\<exists>k. Y k \<noteq> Ibottom")
    77   case True
    78   then obtain k where k: "Y k \<noteq> Ibottom" ..
    79   def A \<equiv> "\<lambda>i. THE a. Iup a = Y (i + k)"
    80   have Iup_A: "\<forall>i. Iup (A i) = Y (i + k)"
    81   proof
    82     fix i :: nat
    83     from Y le_add2 have "Y k \<sqsubseteq> Y (i + k)" by (rule chain_mono)
    84     with k have "Y (i + k) \<noteq> Ibottom" by (cases "Y k", auto)
    85     thus "Iup (A i) = Y (i + k)"
    86       by (cases "Y (i + k)", simp_all add: A_def)
    87   qed
    88   from Y have chain_A: "chain A"
    89     unfolding chain_def Iup_below [symmetric]
    90     by (simp add: Iup_A)
    91   hence "range A <<| (\<Squnion>i. A i)"
    92     by (rule cpo_lubI)
    93   hence "range (\<lambda>i. Iup (A i)) <<| Iup (\<Squnion>i. A i)"
    94     by (rule is_lub_Iup)
    95   hence "range (\<lambda>i. Y (i + k)) <<| Iup (\<Squnion>i. A i)"
    96     by (simp only: Iup_A)
    97   hence "range (\<lambda>i. Y i) <<| Iup (\<Squnion>i. A i)"
    98     by (simp only: is_lub_range_shift [OF Y])
    99   with Iup_A chain_A show ?thesis ..
   100 next
   101   case False
   102   then have "\<forall>i. Y i = Ibottom" by simp
   103   then show ?thesis ..
   104 qed
   105 
   106 instance u :: (cpo) cpo
   107 proof
   108   fix S :: "nat \<Rightarrow> 'a u"
   109   assume S: "chain S"
   110   thus "\<exists>x. range (\<lambda>i. S i) <<| x"
   111   proof (rule up_chain_lemma)
   112     assume "\<forall>i. S i = Ibottom"
   113     hence "range (\<lambda>i. S i) <<| Ibottom"
   114       by (simp add: is_lub_const)
   115     thus ?thesis ..
   116   next
   117     fix A :: "nat \<Rightarrow> 'a"
   118     assume "range S <<| Iup (\<Squnion>i. A i)"
   119     thus ?thesis ..
   120   qed
   121 qed
   122 
   123 subsection {* Lifted cpo is pointed *}
   124 
   125 instance u :: (cpo) pcpo
   126 by intro_classes fast
   127 
   128 text {* for compatibility with old HOLCF-Version *}
   129 lemma inst_up_pcpo: "\<bottom> = Ibottom"
   130 by (rule minimal_up [THEN bottomI, symmetric])
   131 
   132 subsection {* Continuity of \emph{Iup} and \emph{Ifup} *}
   133 
   134 text {* continuity for @{term Iup} *}
   135 
   136 lemma cont_Iup: "cont Iup"
   137 apply (rule contI)
   138 apply (rule is_lub_Iup)
   139 apply (erule cpo_lubI)
   140 done
   141 
   142 text {* continuity for @{term Ifup} *}
   143 
   144 lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
   145 by (induct x, simp_all)
   146 
   147 lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
   148 apply (rule monofunI)
   149 apply (case_tac x, simp)
   150 apply (case_tac y, simp)
   151 apply (simp add: monofun_cfun_arg)
   152 done
   153 
   154 lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
   155 proof (rule contI2)
   156   fix Y assume Y: "chain Y" and Y': "chain (\<lambda>i. Ifup f (Y i))"
   157   from Y show "Ifup f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. Ifup f (Y i))"
   158   proof (rule up_chain_lemma)
   159     fix A and k
   160     assume A: "\<forall>i. Iup (A i) = Y (i + k)"
   161     assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
   162     hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
   163       by (simp add: lub_eqI contlub_cfun_arg)
   164     also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
   165       by (simp add: A)
   166     also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
   167       using Y' by (rule lub_range_shift)
   168     finally show ?thesis by simp
   169   qed simp
   170 qed (rule monofun_Ifup2)
   171 
   172 subsection {* Continuous versions of constants *}
   173 
   174 definition
   175   up  :: "'a \<rightarrow> 'a u" where
   176   "up = (\<Lambda> x. Iup x)"
   177 
   178 definition
   179   fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
   180   "fup = (\<Lambda> f p. Ifup f p)"
   181 
   182 translations
   183   "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
   184   "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
   185   "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
   186 
   187 text {* continuous versions of lemmas for @{typ "('a)u"} *}
   188 
   189 lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
   190 apply (induct z)
   191 apply (simp add: inst_up_pcpo)
   192 apply (simp add: up_def cont_Iup)
   193 done
   194 
   195 lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
   196 by (simp add: up_def cont_Iup)
   197 
   198 lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
   199 by simp
   200 
   201 lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
   202 by (simp add: up_def cont_Iup inst_up_pcpo)
   203 
   204 lemma not_up_less_UU: "up\<cdot>x \<notsqsubseteq> \<bottom>"
   205 by simp (* FIXME: remove? *)
   206 
   207 lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
   208 by (simp add: up_def cont_Iup)
   209 
   210 lemma upE [case_names bottom up, cases type: u]:
   211   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   212 apply (cases p)
   213 apply (simp add: inst_up_pcpo)
   214 apply (simp add: up_def cont_Iup)
   215 done
   216 
   217 lemma up_induct [case_names bottom up, induct type: u]:
   218   "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
   219 by (cases x, simp_all)
   220 
   221 text {* lifting preserves chain-finiteness *}
   222 
   223 lemma up_chain_cases:
   224   assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
   225   | A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)"
   226 apply (rule up_chain_lemma [OF Y])
   227 apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
   228 done
   229 
   230 lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
   231 apply (rule compactI2)
   232 apply (erule up_chain_cases)
   233 apply simp
   234 apply (drule (1) compactD2, simp)
   235 apply (erule exE)
   236 apply (drule_tac f="up" and x="x" in monofun_cfun_arg)
   237 apply (simp, erule exI)
   238 done
   239 
   240 lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
   241 unfolding compact_def
   242 by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp)
   243 
   244 lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
   245 by (safe elim!: compact_up compact_upD)
   246 
   247 instance u :: (chfin) chfin
   248 apply intro_classes
   249 apply (erule compact_imp_max_in_chain)
   250 apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
   251 done
   252 
   253 text {* properties of fup *}
   254 
   255 lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
   256 by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)
   257 
   258 lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
   259 by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM)
   260 
   261 lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
   262 by (cases x, simp_all)
   263 
   264 end