src/HOL/HOLCF/Tutorial/Fixrec_ex.thy
changeset 62175 8ffc4d0e652d
parent 58880 0baae4311a9f
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/HOLCF/Tutorial/Fixrec_ex.thy	Wed Jan 13 23:02:28 2016 +0100
     1.2 +++ b/src/HOL/HOLCF/Tutorial/Fixrec_ex.thy	Wed Jan 13 23:07:06 2016 +0100
     1.3 @@ -2,50 +2,50 @@
     1.4      Author:     Brian Huffman
     1.5  *)
     1.6  
     1.7 -section {* Fixrec package examples *}
     1.8 +section \<open>Fixrec package examples\<close>
     1.9  
    1.10  theory Fixrec_ex
    1.11  imports HOLCF
    1.12  begin
    1.13  
    1.14 -subsection {* Basic @{text fixrec} examples *}
    1.15 +subsection \<open>Basic \<open>fixrec\<close> examples\<close>
    1.16  
    1.17 -text {*
    1.18 +text \<open>
    1.19    Fixrec patterns can mention any constructor defined by the domain
    1.20    package, as well as any of the following built-in constructors:
    1.21    Pair, spair, sinl, sinr, up, ONE, TT, FF.
    1.22 -*}
    1.23 +\<close>
    1.24  
    1.25 -text {* Typical usage is with lazy constructors. *}
    1.26 +text \<open>Typical usage is with lazy constructors.\<close>
    1.27  
    1.28  fixrec down :: "'a u \<rightarrow> 'a"
    1.29  where "down\<cdot>(up\<cdot>x) = x"
    1.30  
    1.31 -text {* With strict constructors, rewrite rules may require side conditions. *}
    1.32 +text \<open>With strict constructors, rewrite rules may require side conditions.\<close>
    1.33  
    1.34  fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
    1.35  where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
    1.36  
    1.37 -text {* Lifting can turn a strict constructor into a lazy one. *}
    1.38 +text \<open>Lifting can turn a strict constructor into a lazy one.\<close>
    1.39  
    1.40  fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
    1.41  where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
    1.42  
    1.43 -text {* Fixrec also works with the HOL pair constructor. *}
    1.44 +text \<open>Fixrec also works with the HOL pair constructor.\<close>
    1.45  
    1.46  fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
    1.47  where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
    1.48  
    1.49  
    1.50 -subsection {* Examples using @{text fixrec_simp} *}
    1.51 +subsection \<open>Examples using \<open>fixrec_simp\<close>\<close>
    1.52  
    1.53 -text {* A type of lazy lists. *}
    1.54 +text \<open>A type of lazy lists.\<close>
    1.55  
    1.56  domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
    1.57  
    1.58 -text {* A zip function for lazy lists. *}
    1.59 +text \<open>A zip function for lazy lists.\<close>
    1.60  
    1.61 -text {* Notice that the patterns are not exhaustive. *}
    1.62 +text \<open>Notice that the patterns are not exhaustive.\<close>
    1.63  
    1.64  fixrec
    1.65    lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
    1.66 @@ -53,8 +53,8 @@
    1.67    "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
    1.68  | "lzip\<cdot>lNil\<cdot>lNil = lNil"
    1.69  
    1.70 -text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
    1.71 -text {* Note that pattern matching is done in left-to-right order. *}
    1.72 +text \<open>\<open>fixrec_simp\<close> is useful for producing strictness theorems.\<close>
    1.73 +text \<open>Note that pattern matching is done in left-to-right order.\<close>
    1.74  
    1.75  lemma lzip_stricts [simp]:
    1.76    "lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
    1.77 @@ -62,7 +62,7 @@
    1.78    "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
    1.79  by fixrec_simp+
    1.80  
    1.81 -text {* @{text fixrec_simp} can also produce rules for missing cases. *}
    1.82 +text \<open>\<open>fixrec_simp\<close> can also produce rules for missing cases.\<close>
    1.83  
    1.84  lemma lzip_undefs [simp]:
    1.85    "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
    1.86 @@ -70,14 +70,13 @@
    1.87  by fixrec_simp+
    1.88  
    1.89  
    1.90 -subsection {* Pattern matching with bottoms *}
    1.91 +subsection \<open>Pattern matching with bottoms\<close>
    1.92  
    1.93 -text {*
    1.94 -  As an alternative to using @{text fixrec_simp}, it is also possible
    1.95 +text \<open>
    1.96 +  As an alternative to using \<open>fixrec_simp\<close>, it is also possible
    1.97    to use bottom as a constructor pattern.  When using a bottom
    1.98 -  pattern, the right-hand-side must also be bottom; otherwise, @{text
    1.99 -  fixrec} will not be able to prove the equation.
   1.100 -*}
   1.101 +  pattern, the right-hand-side must also be bottom; otherwise, \<open>fixrec\<close> will not be able to prove the equation.
   1.102 +\<close>
   1.103  
   1.104  fixrec
   1.105    from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
   1.106 @@ -85,18 +84,18 @@
   1.107    "from_sinr_up\<cdot>\<bottom> = \<bottom>"
   1.108  | "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
   1.109  
   1.110 -text {*
   1.111 +text \<open>
   1.112    If the function is already strict in that argument, then the bottom
   1.113    pattern does not change the meaning of the function.  For example,
   1.114    in the definition of @{term from_sinr_up}, the first equation is
   1.115    actually redundant, and could have been proven separately by
   1.116 -  @{text fixrec_simp}.
   1.117 -*}
   1.118 +  \<open>fixrec_simp\<close>.
   1.119 +\<close>
   1.120  
   1.121 -text {*
   1.122 +text \<open>
   1.123    A bottom pattern can also be used to make a function strict in a
   1.124    certain argument, similar to a bang-pattern in Haskell.
   1.125 -*}
   1.126 +\<close>
   1.127  
   1.128  fixrec
   1.129    seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
   1.130 @@ -105,15 +104,15 @@
   1.131  | "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
   1.132  
   1.133  
   1.134 -subsection {* Skipping proofs of rewrite rules *}
   1.135 +subsection \<open>Skipping proofs of rewrite rules\<close>
   1.136  
   1.137 -text {* Another zip function for lazy lists. *}
   1.138 +text \<open>Another zip function for lazy lists.\<close>
   1.139  
   1.140 -text {*
   1.141 +text \<open>
   1.142    Notice that this version has overlapping patterns.
   1.143    The second equation cannot be proved as a theorem
   1.144    because it only applies when the first pattern fails.
   1.145 -*}
   1.146 +\<close>
   1.147  
   1.148  fixrec
   1.149    lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
   1.150 @@ -121,13 +120,13 @@
   1.151    "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip2\<cdot>xs\<cdot>ys)"
   1.152  | (unchecked) "lzip2\<cdot>xs\<cdot>ys = lNil"
   1.153  
   1.154 -text {*
   1.155 +text \<open>
   1.156    Usually fixrec tries to prove all equations as theorems.
   1.157    The "unchecked" option overrides this behavior, so fixrec
   1.158    does not attempt to prove that particular equation.
   1.159 -*}
   1.160 +\<close>
   1.161  
   1.162 -text {* Simp rules can be generated later using @{text fixrec_simp}. *}
   1.163 +text \<open>Simp rules can be generated later using \<open>fixrec_simp\<close>.\<close>
   1.164  
   1.165  lemma lzip2_simps [simp]:
   1.166    "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
   1.167 @@ -141,17 +140,17 @@
   1.168  by fixrec_simp+
   1.169  
   1.170  
   1.171 -subsection {* Mutual recursion with @{text fixrec} *}
   1.172 +subsection \<open>Mutual recursion with \<open>fixrec\<close>\<close>
   1.173  
   1.174 -text {* Tree and forest types. *}
   1.175 +text \<open>Tree and forest types.\<close>
   1.176  
   1.177  domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
   1.178  and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
   1.179  
   1.180 -text {*
   1.181 +text \<open>
   1.182    To define mutually recursive functions, give multiple type signatures
   1.183 -  separated by the keyword @{text "and"}.
   1.184 -*}
   1.185 +  separated by the keyword \<open>and\<close>.
   1.186 +\<close>
   1.187  
   1.188  fixrec
   1.189    map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
   1.190 @@ -182,25 +181,25 @@
   1.191  *)
   1.192  
   1.193  
   1.194 -subsection {* Looping simp rules *}
   1.195 +subsection \<open>Looping simp rules\<close>
   1.196  
   1.197 -text {*
   1.198 +text \<open>
   1.199    The defining equations of a fixrec definition are declared as simp
   1.200    rules by default.  In some cases, especially for constants with no
   1.201    arguments or functions with variable patterns, the defining
   1.202    equations may cause the simplifier to loop.  In these cases it will
   1.203 -  be necessary to use a @{text "[simp del]"} declaration.
   1.204 -*}
   1.205 +  be necessary to use a \<open>[simp del]\<close> declaration.
   1.206 +\<close>
   1.207  
   1.208  fixrec
   1.209    repeat :: "'a \<rightarrow> 'a llist"
   1.210  where
   1.211    [simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)"
   1.212  
   1.213 -text {*
   1.214 +text \<open>
   1.215    We can derive other non-looping simp rules for @{const repeat} by
   1.216 -  using the @{text subst} method with the @{text repeat.simps} rule.
   1.217 -*}
   1.218 +  using the \<open>subst\<close> method with the \<open>repeat.simps\<close> rule.
   1.219 +\<close>
   1.220  
   1.221  lemma repeat_simps [simp]:
   1.222    "repeat\<cdot>x \<noteq> \<bottom>"
   1.223 @@ -212,11 +211,11 @@
   1.224    "llist_case\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
   1.225  by (subst repeat.simps, simp)
   1.226  
   1.227 -text {*
   1.228 +text \<open>
   1.229    For mutually-recursive constants, looping might only occur if all
   1.230    equations are in the simpset at the same time.  In such cases it may
   1.231 -  only be necessary to declare @{text "[simp del]"} on one equation.
   1.232 -*}
   1.233 +  only be necessary to declare \<open>[simp del]\<close> on one equation.
   1.234 +\<close>
   1.235  
   1.236  fixrec
   1.237    inf_tree :: "'a tree" and inf_forest :: "'a forest"
   1.238 @@ -225,7 +224,7 @@
   1.239  | "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)"
   1.240  
   1.241  
   1.242 -subsection {* Using @{text fixrec} inside locales *}
   1.243 +subsection \<open>Using \<open>fixrec\<close> inside locales\<close>
   1.244  
   1.245  locale test =
   1.246    fixes foo :: "'a \<rightarrow> 'a"