src/HOLCF/Up.thy
author huffman
Tue Jul 01 02:50:29 2008 +0200 (2008-07-01)
changeset 27414 95ec4bda5bb9
parent 27413 3154f3765cc7
child 29138 661a8db7e647
permissions -rw-r--r--
remove unused lemma is_lub_Iup'
     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 text {* Now some lemmas about chains of @{typ "'a u"} elements *}
    97 
    98 lemma up_lemma1: "z \<noteq> Ibottom \<Longrightarrow> Iup (THE a. Iup a = z) = z"
    99 by (case_tac z, simp_all)
   100 
   101 lemma up_lemma2:
   102   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom"
   103 apply (erule contrapos_nn)
   104 apply (drule_tac i="j" and j="i + j" in chain_mono)
   105 apply (rule le_add2)
   106 apply (case_tac "Y j")
   107 apply assumption
   108 apply simp
   109 done
   110 
   111 lemma up_lemma3:
   112   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
   113 by (rule up_lemma1 [OF up_lemma2])
   114 
   115 lemma up_lemma4:
   116   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
   117 apply (rule chainI)
   118 apply (rule Iup_less [THEN iffD1])
   119 apply (subst up_lemma3, assumption+)+
   120 apply (simp add: chainE)
   121 done
   122 
   123 lemma up_lemma5:
   124   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow>
   125     (\<lambda>i. Y (i + j)) = (\<lambda>i. Iup (THE a. Iup a = Y (i + j)))"
   126 by (rule ext, rule up_lemma3 [symmetric])
   127 
   128 lemma up_lemma6:
   129   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>
   130       \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
   131 apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
   132 apply assumption
   133 apply (subst up_lemma5, assumption+)
   134 apply (rule is_lub_Iup)
   135 apply (rule cpo_lubI)
   136 apply (erule (1) up_lemma4)
   137 done
   138 
   139 lemma up_chain_lemma:
   140   "chain Y \<Longrightarrow>
   141    (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = Iup (\<Squnion>i. A i) \<and>
   142    (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
   143 apply (rule disjCI)
   144 apply (simp add: expand_fun_eq)
   145 apply (erule exE, rename_tac j)
   146 apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
   147 apply (simp add: up_lemma4)
   148 apply (simp add: up_lemma6 [THEN thelubI])
   149 apply (rule_tac x=j in exI)
   150 apply (simp add: up_lemma3)
   151 done
   152 
   153 lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
   154 apply (frule up_chain_lemma, safe)
   155 apply (rule_tac x="Iup (\<Squnion>i. A i)" in exI)
   156 apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
   157 apply (simp add: is_lub_Iup cpo_lubI)
   158 apply (rule exI, rule lub_const)
   159 done
   160 
   161 instance u :: (cpo) cpo
   162 by intro_classes (rule cpo_up)
   163 
   164 subsection {* Lifted cpo is pointed *}
   165 
   166 lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"
   167 apply (rule_tac x = "Ibottom" in exI)
   168 apply (rule minimal_up [THEN allI])
   169 done
   170 
   171 instance u :: (cpo) pcpo
   172 by intro_classes (rule least_up)
   173 
   174 text {* for compatibility with old HOLCF-Version *}
   175 lemma inst_up_pcpo: "\<bottom> = Ibottom"
   176 by (rule minimal_up [THEN UU_I, symmetric])
   177 
   178 subsection {* Continuity of @{term Iup} and @{term Ifup} *}
   179 
   180 text {* continuity for @{term Iup} *}
   181 
   182 lemma cont_Iup: "cont Iup"
   183 apply (rule contI)
   184 apply (rule is_lub_Iup)
   185 apply (erule cpo_lubI)
   186 done
   187 
   188 text {* continuity for @{term Ifup} *}
   189 
   190 lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
   191 by (induct x, simp_all)
   192 
   193 lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
   194 apply (rule monofunI)
   195 apply (case_tac x, simp)
   196 apply (case_tac y, simp)
   197 apply (simp add: monofun_cfun_arg)
   198 done
   199 
   200 lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
   201 apply (rule contI)
   202 apply (frule up_chain_lemma, safe)
   203 apply (rule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
   204 apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   205 apply (simp add: cont_cfun_arg)
   206 apply (simp add: lub_const)
   207 done
   208 
   209 subsection {* Continuous versions of constants *}
   210 
   211 definition
   212   up  :: "'a \<rightarrow> 'a u" where
   213   "up = (\<Lambda> x. Iup x)"
   214 
   215 definition
   216   fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
   217   "fup = (\<Lambda> f p. Ifup f p)"
   218 
   219 translations
   220   "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
   221   "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
   222 
   223 text {* continuous versions of lemmas for @{typ "('a)u"} *}
   224 
   225 lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
   226 apply (induct z)
   227 apply (simp add: inst_up_pcpo)
   228 apply (simp add: up_def cont_Iup)
   229 done
   230 
   231 lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
   232 by (simp add: up_def cont_Iup)
   233 
   234 lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
   235 by simp
   236 
   237 lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
   238 by (simp add: up_def cont_Iup inst_up_pcpo)
   239 
   240 lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
   241 by simp
   242 
   243 lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
   244 by (simp add: up_def cont_Iup)
   245 
   246 lemma upE [cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   247 apply (cases p)
   248 apply (simp add: inst_up_pcpo)
   249 apply (simp add: up_def cont_Iup)
   250 done
   251 
   252 lemma up_induct [induct type: u]: "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
   253 by (cases x, simp_all)
   254 
   255 text {* lifting preserves chain-finiteness *}
   256 
   257 lemma up_chain_cases:
   258   "chain Y \<Longrightarrow>
   259   (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
   260   (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
   261 by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
   262 
   263 lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
   264 apply (rule compactI2)
   265 apply (drule up_chain_cases, safe)
   266 apply (drule (1) compactD2, simp)
   267 apply (erule exE, rule_tac x="i + j" in exI)
   268 apply simp
   269 apply simp
   270 done
   271 
   272 lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
   273 unfolding compact_def
   274 by (drule adm_subst [OF cont_Rep_CFun2 [where f=up]], simp)
   275 
   276 lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
   277 by (safe elim!: compact_up compact_upD)
   278 
   279 instance u :: (chfin) chfin
   280 apply intro_classes
   281 apply (erule compact_imp_max_in_chain)
   282 apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
   283 done
   284 
   285 text {* properties of fup *}
   286 
   287 lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
   288 by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
   289 
   290 lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
   291 by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2)
   292 
   293 lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
   294 by (cases x, simp_all)
   295 
   296 subsection {* Lifted cpo is a bifinite domain *}
   297 
   298 instantiation u :: (profinite) bifinite
   299 begin
   300 
   301 definition
   302   approx_up_def:
   303     "approx = (\<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x)))"
   304 
   305 instance proof
   306   fix i :: nat and x :: "'a u"
   307   show "chain (approx :: nat \<Rightarrow> 'a u \<rightarrow> 'a u)"
   308     unfolding approx_up_def by simp
   309   show "(\<Squnion>i. approx i\<cdot>x) = x"
   310     unfolding approx_up_def
   311     by (simp add: lub_distribs eta_cfun)
   312   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   313     unfolding approx_up_def
   314     by (induct x, simp, simp)
   315   have "{x::'a u. approx i\<cdot>x = x} \<subseteq>
   316         insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x::'a. approx i\<cdot>x = x})"
   317     unfolding approx_up_def
   318     by (rule subsetI, case_tac x, simp_all)
   319   thus "finite {x::'a u. approx i\<cdot>x = x}"
   320     by (rule finite_subset, simp add: finite_fixes_approx)
   321 qed
   322 
   323 end
   324 
   325 lemma approx_up [simp]: "approx i\<cdot>(up\<cdot>x) = up\<cdot>(approx i\<cdot>x)"
   326 unfolding approx_up_def by simp
   327 
   328 end