src/HOL/HOLCF/Ssum.thy

 (*  Title:      HOL/HOLCF/Ssum.thy
     Author:     Franz Regensburger
     Author:     Brian Huffman
 *)
 
-section {* The type of strict sums *}
+section \<open>The type of strict sums\<close>
 
 theory Ssum
 imports Tr
 begin
 
 default_sort pcpo
 
-subsection {* Definition of strict sum type *}
+subsection \<open>Definition of strict sum type\<close>
 
 definition
   "ssum =
     {p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
       (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>

 
 type_notation (ASCII)
   ssum  (infixr "++" 10)
 
 
-subsection {* Definitions of constructors *}
+subsection \<open>Definitions of constructors\<close>
 
 definition
   sinl :: "'a \<rightarrow> ('a ++ 'b)" where
   "sinl = (\<Lambda> a. Abs_ssum (seq\<cdot>a\<cdot>TT, a, \<bottom>))"
 

 lemmas Rep_ssum_simps =
   Rep_ssum_inject [symmetric] below_ssum_def
   prod_eq_iff below_prod_def
   Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr
 
-subsection {* Properties of \emph{sinl} and \emph{sinr} *}
-
-text {* Ordering *}
+subsection \<open>Properties of \emph{sinl} and \emph{sinr}\<close>
+
+text \<open>Ordering\<close>
 
 lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
 by (simp add: Rep_ssum_simps seq_conv_if)
 
 lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"

 by (simp add: Rep_ssum_simps seq_conv_if)
 
 lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
 by (simp add: Rep_ssum_simps seq_conv_if)
 
-text {* Equality *}
+text \<open>Equality\<close>
 
 lemma sinl_eq [simp]: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)"
 by (simp add: po_eq_conv)
 
 lemma sinr_eq [simp]: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)"

 by (rule sinl_eq [THEN iffD1])
 
 lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y"
 by (rule sinr_eq [THEN iffD1])
 
-text {* Strictness *}
+text \<open>Strictness\<close>
 
 lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
 by (simp add: Rep_ssum_simps)
 
 lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"

 by simp
 
 lemma sinr_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
 by simp
 
-text {* Compactness *}
+text \<open>Compactness\<close>
 
 lemma compact_sinl: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
 by (rule compact_ssum, simp add: Rep_ssum_sinl)
 
 lemma compact_sinr: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"

 by (safe elim!: compact_sinl compact_sinlD)
 
 lemma compact_sinr_iff [simp]: "compact (sinr\<cdot>x) = compact x"
 by (safe elim!: compact_sinr compact_sinrD)
 
-subsection {* Case analysis *}
+subsection \<open>Case analysis\<close>
 
 lemma ssumE [case_names bottom sinl sinr, cases type: ssum]:
   obtains "p = \<bottom>"
   | x where "p = sinl\<cdot>x" and "x \<noteq> \<bottom>"
   | y where "p = sinr\<cdot>y" and "y \<noteq> \<bottom>"

 by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
 
 lemma below_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
 by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
 
-subsection {* Case analysis combinator *}
+subsection \<open>Case analysis combinator\<close>
 
 definition
   sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where
   "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s))"
 

 unfolding beta_sscase by (simp add: Rep_ssum_sinr)
 
 lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
 by (cases z, simp_all)
 
-subsection {* Strict sum preserves flatness *}
+subsection \<open>Strict sum preserves flatness\<close>
 
 instance ssum :: (flat, flat) flat
 apply (intro_classes, clarify)
 apply (case_tac x, simp)
 apply (case_tac y, simp_all add: flat_below_iff)