src/HOL/HOLCF/Up.thy

 (*  Title:      HOL/HOLCF/Up.thy
     Author:     Franz Regensburger
     Author:     Brian Huffman
 *)
 
-section {* The type of lifted values *}
+section \<open>The type of lifted values\<close>
 
 theory Up
 imports Cfun
 begin
 
 default_sort cpo
 
-subsection {* Definition of new type for lifting *}
+subsection \<open>Definition of new type for lifting\<close>
 
 datatype 'a u  ("(_\<^sub>\<bottom>)" [1000] 999) = Ibottom | Iup 'a
 
 primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
     "Ifup f Ibottom = \<bottom>"
  |  "Ifup f (Iup x) = f\<cdot>x"
 
-subsection {* Ordering on lifted cpo *}
+subsection \<open>Ordering on lifted cpo\<close>
 
 instantiation u :: (cpo) below
 begin
 
 definition

 by (simp add: below_up_def)
 
 lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
 by (simp add: below_up_def)
 
-subsection {* Lifted cpo is a partial order *}
+subsection \<open>Lifted cpo is a partial order\<close>
 
 instance u :: (cpo) po
 proof
   fix x :: "'a u"
   show "x \<sqsubseteq> x"

   assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
     unfolding below_up_def
     by (auto split: u.split_asm intro: below_trans)
 qed
 
-subsection {* Lifted cpo is a cpo *}
+subsection \<open>Lifted cpo is a cpo\<close>
 
 lemma is_lub_Iup:
   "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
 unfolding is_lub_def is_ub_def ball_simps
 by (auto simp add: below_up_def split: u.split)

     assume "range S <<| Iup (\<Squnion>i. A i)"
     thus ?thesis ..
   qed
 qed
 
-subsection {* Lifted cpo is pointed *}
+subsection \<open>Lifted cpo is pointed\<close>
 
 instance u :: (cpo) pcpo
 by intro_classes fast
 
-text {* for compatibility with old HOLCF-Version *}
+text \<open>for compatibility with old HOLCF-Version\<close>
 lemma inst_up_pcpo: "\<bottom> = Ibottom"
 by (rule minimal_up [THEN bottomI, symmetric])
 
-subsection {* Continuity of \emph{Iup} and \emph{Ifup} *}
-
-text {* continuity for @{term Iup} *}
+subsection \<open>Continuity of \emph{Iup} and \emph{Ifup}\<close>
+
+text \<open>continuity for @{term Iup}\<close>
 
 lemma cont_Iup: "cont Iup"
 apply (rule contI)
 apply (rule is_lub_Iup)
 apply (erule cpo_lubI)
 done
 
-text {* continuity for @{term Ifup} *}
+text \<open>continuity for @{term Ifup}\<close>
 
 lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
 by (induct x, simp_all)
 
 lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"

       using Y' by (rule lub_range_shift)
     finally show ?thesis by simp
   qed simp
 qed (rule monofun_Ifup2)
 
-subsection {* Continuous versions of constants *}
+subsection \<open>Continuous versions of constants\<close>
 
 definition
   up  :: "'a \<rightarrow> 'a u" where
   "up = (\<Lambda> x. Iup x)"
 

 translations
   "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
   "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
   "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
 
-text {* continuous versions of lemmas for @{typ "('a)u"} *}
+text \<open>continuous versions of lemmas for @{typ "('a)u"}\<close>
 
 lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
 apply (induct z)
 apply (simp add: inst_up_pcpo)
 apply (simp add: up_def cont_Iup)

 
 lemma up_induct [case_names bottom up, induct type: u]:
   "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
 by (cases x, simp_all)
 
-text {* lifting preserves chain-finiteness *}
+text \<open>lifting preserves chain-finiteness\<close>
 
 lemma up_chain_cases:
   assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
   | 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)"
 apply (rule up_chain_lemma [OF Y])

 apply intro_classes
 apply (erule compact_imp_max_in_chain)
 apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
 done
 
-text {* properties of fup *}
+text \<open>properties of fup\<close>
 
 lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
 by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)
 
 lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"