src/HOL/HOLCF/Cpodef.thy
changeset 62175 8ffc4d0e652d
parent 58880 0baae4311a9f
child 67312 0d25e02759b7
     1.1 --- a/src/HOL/HOLCF/Cpodef.thy	Wed Jan 13 23:02:28 2016 +0100
     1.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Wed Jan 13 23:07:06 2016 +0100
     1.3 @@ -2,21 +2,21 @@
     1.4      Author:     Brian Huffman
     1.5  *)
     1.6  
     1.7 -section {* Subtypes of pcpos *}
     1.8 +section \<open>Subtypes of pcpos\<close>
     1.9  
    1.10  theory Cpodef
    1.11  imports Adm
    1.12  keywords "pcpodef" "cpodef" :: thy_goal
    1.13  begin
    1.14  
    1.15 -subsection {* Proving a subtype is a partial order *}
    1.16 +subsection \<open>Proving a subtype is a partial order\<close>
    1.17  
    1.18 -text {*
    1.19 +text \<open>
    1.20    A subtype of a partial order is itself a partial order,
    1.21    if the ordering is defined in the standard way.
    1.22 -*}
    1.23 +\<close>
    1.24  
    1.25 -setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
    1.26 +setup \<open>Sign.add_const_constraint (@{const_name Porder.below}, NONE)\<close>
    1.27  
    1.28  theorem typedef_po:
    1.29    fixes Abs :: "'a::po \<Rightarrow> 'b::type"
    1.30 @@ -30,10 +30,10 @@
    1.31   apply (erule (1) below_antisym)
    1.32  done
    1.33  
    1.34 -setup {* Sign.add_const_constraint (@{const_name Porder.below},
    1.35 -  SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
    1.36 +setup \<open>Sign.add_const_constraint (@{const_name Porder.below},
    1.37 +  SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"})\<close>
    1.38  
    1.39 -subsection {* Proving a subtype is finite *}
    1.40 +subsection \<open>Proving a subtype is finite\<close>
    1.41  
    1.42  lemma typedef_finite_UNIV:
    1.43    fixes Abs :: "'a::type \<Rightarrow> 'b::type"
    1.44 @@ -46,7 +46,7 @@
    1.45      by (simp only: type_definition.Abs_image [OF type])
    1.46  qed
    1.47  
    1.48 -subsection {* Proving a subtype is chain-finite *}
    1.49 +subsection \<open>Proving a subtype is chain-finite\<close>
    1.50  
    1.51  lemma ch2ch_Rep:
    1.52    assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    1.53 @@ -65,15 +65,15 @@
    1.54   apply (simp add: type_definition.Rep_inject [OF type])
    1.55  done
    1.56  
    1.57 -subsection {* Proving a subtype is complete *}
    1.58 +subsection \<open>Proving a subtype is complete\<close>
    1.59  
    1.60 -text {*
    1.61 +text \<open>
    1.62    A subtype of a cpo is itself a cpo if the ordering is
    1.63    defined in the standard way, and the defining subset
    1.64    is closed with respect to limits of chains.  A set is
    1.65    closed if and only if membership in the set is an
    1.66    admissible predicate.
    1.67 -*}
    1.68 +\<close>
    1.69  
    1.70  lemma typedef_is_lubI:
    1.71    assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    1.72 @@ -122,9 +122,9 @@
    1.73    thus "\<exists>x. range S <<| x" ..
    1.74  qed
    1.75  
    1.76 -subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
    1.77 +subsubsection \<open>Continuity of \emph{Rep} and \emph{Abs}\<close>
    1.78  
    1.79 -text {* For any sub-cpo, the @{term Rep} function is continuous. *}
    1.80 +text \<open>For any sub-cpo, the @{term Rep} function is continuous.\<close>
    1.81  
    1.82  theorem typedef_cont_Rep:
    1.83    fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
    1.84 @@ -140,11 +140,11 @@
    1.85   apply (erule ch2ch_Rep [OF below])
    1.86  done
    1.87  
    1.88 -text {*
    1.89 +text \<open>
    1.90    For a sub-cpo, we can make the @{term Abs} function continuous
    1.91    only if we restrict its domain to the defining subset by
    1.92    composing it with another continuous function.
    1.93 -*}
    1.94 +\<close>
    1.95  
    1.96  theorem typedef_cont_Abs:
    1.97    fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
    1.98 @@ -157,7 +157,7 @@
    1.99  unfolding cont_def is_lub_def is_ub_def ball_simps below
   1.100  by (simp add: type_definition.Abs_inverse [OF type f_in_A])
   1.101  
   1.102 -subsection {* Proving subtype elements are compact *}
   1.103 +subsection \<open>Proving subtype elements are compact\<close>
   1.104  
   1.105  theorem typedef_compact:
   1.106    fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   1.107 @@ -173,12 +173,12 @@
   1.108    thus "adm (\<lambda>x. k \<notsqsubseteq> x)" by (unfold below)
   1.109  qed
   1.110  
   1.111 -subsection {* Proving a subtype is pointed *}
   1.112 +subsection \<open>Proving a subtype is pointed\<close>
   1.113  
   1.114 -text {*
   1.115 +text \<open>
   1.116    A subtype of a cpo has a least element if and only if
   1.117    the defining subset has a least element.
   1.118 -*}
   1.119 +\<close>
   1.120  
   1.121  theorem typedef_pcpo_generic:
   1.122    fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   1.123 @@ -194,10 +194,10 @@
   1.124   apply (rule z_least [OF type_definition.Rep [OF type]])
   1.125  done
   1.126  
   1.127 -text {*
   1.128 +text \<open>
   1.129    As a special case, a subtype of a pcpo has a least element
   1.130    if the defining subset contains @{term \<bottom>}.
   1.131 -*}
   1.132 +\<close>
   1.133  
   1.134  theorem typedef_pcpo:
   1.135    fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
   1.136 @@ -207,12 +207,12 @@
   1.137    shows "OFCLASS('b, pcpo_class)"
   1.138  by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)
   1.139  
   1.140 -subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
   1.141 +subsubsection \<open>Strictness of \emph{Rep} and \emph{Abs}\<close>
   1.142  
   1.143 -text {*
   1.144 +text \<open>
   1.145    For a sub-pcpo where @{term \<bottom>} is a member of the defining
   1.146    subset, @{term Rep} and @{term Abs} are both strict.
   1.147 -*}
   1.148 +\<close>
   1.149  
   1.150  theorem typedef_Abs_strict:
   1.151    assumes type: "type_definition Rep Abs A"
   1.152 @@ -250,7 +250,7 @@
   1.153   apply (simp add: type_definition.Rep_inject [OF type])
   1.154  done
   1.155  
   1.156 -subsection {* Proving a subtype is flat *}
   1.157 +subsection \<open>Proving a subtype is flat\<close>
   1.158  
   1.159  theorem typedef_flat:
   1.160    fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
   1.161 @@ -265,7 +265,7 @@
   1.162   apply (simp add: ax_flat)
   1.163  done
   1.164  
   1.165 -subsection {* HOLCF type definition package *}
   1.166 +subsection \<open>HOLCF type definition package\<close>
   1.167  
   1.168  ML_file "Tools/cpodef.ML"
   1.169