adjusted manual to improved treatment of overloaded constants
authorhaftmann
Fri Jan 26 09:24:35 2007 +0100 (2007-01-26)
changeset 22188a63889770d57
parent 22187 a2c4861363d5
child 22189 10278e568741
adjusted manual to improved treatment of overloaded constants
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Jan 25 16:57:57 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Jan 26 09:24:35 2007 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  (* $Id$ *)
     1.6  
     1.7  (*<*)
     1.8 @@ -365,6 +364,7 @@
     1.9    the file system, with root given by the user.
    1.10  *}
    1.11  
    1.12 +ML {* set Toplevel.debug *}
    1.13  code_gen dummy (Haskell "examples/")
    1.14    (* NOTE: you may use Haskell only once in this document, otherwise
    1.15    you have to work in distinct subdirectories *)
    1.16 @@ -809,7 +809,7 @@
    1.17    \lstsml{Thy/examples/lookup.ML}
    1.18  *}
    1.19  
    1.20 -subsubsection {* lexicographic orderings and coregularity *}
    1.21 +subsubsection {* lexicographic orderings *}
    1.22  
    1.23  text {*
    1.24    Another subtlety
    1.25 @@ -818,23 +818,16 @@
    1.26    us define a lexicographic ordering on tuples:
    1.27  *}
    1.28  
    1.29 -(*<*)
    1.30 -setup {* Sign.add_path "foobar" *}
    1.31 -class ord =
    1.32 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_/ \<^loc>\<le> _)" [50, 51] 50)
    1.33 -  fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_/ \<^loc>< _)" [50, 51] 50)
    1.34 -(*>*)
    1.35 -
    1.36  instance * :: (ord, ord) ord
    1.37    "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
    1.38      x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
    1.39 -  "p1 \<le> p2 \<equiv> p1 < p2 \<or> (p1 \<Colon> 'a\<Colon>ord \<times> 'b\<Colon>ord)  = p2" ..
    1.40 +  "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
    1.41 +    x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" ..
    1.42  
    1.43 -(*<*)
    1.44 -hide "class"  ord
    1.45 -hide const less_eq less
    1.46 -setup {* Sign.parent_path *}
    1.47 -(*>*)
    1.48 +lemma ord_prod [code func]:
    1.49 +  "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
    1.50 +  "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
    1.51 +  unfolding "less_eq_*_def" "less_*_def" by simp_all
    1.52  
    1.53  text {*
    1.54    Then code generation will fail.  Why?  The definition
    1.55 @@ -843,25 +836,38 @@
    1.56    class constraint, thus violating the type discipline
    1.57    for class operations.
    1.58  
    1.59 -  The solution is to add @{text eq} to both sort arguments:
    1.60 +  The solution is to add @{text eq} explicitly to the first sort arguments in the
    1.61 +  code theorems:
    1.62  *}
    1.63  
    1.64 -instance * :: ("{eq, ord}", "{eq, ord}") ord
    1.65 -  "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>{eq, ord}, y1 \<Colon> 'b\<Colon>{eq, ord}) = p1; (x2, y2) = p2 in
    1.66 -    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
    1.67 -  "p1 \<le> p2 \<equiv> p1 < p2 \<or> (p1 \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>{eq, ord})  = p2" ..
    1.68 +(*<*)
    1.69 +declare ord_prod [code del]
    1.70 +(*>*)
    1.71 +
    1.72 +lemma ord_prod_code [code func]:
    1.73 +  "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
    1.74 +  "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
    1.75 +  unfolding ord_prod by rule+
    1.76  
    1.77  text {*
    1.78    Then code generation succeeds:
    1.79  *}
    1.80  
    1.81 -code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>{eq, ord} \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.82 +code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.83    (*<*)(SML #)(*>*)(SML "examples/lexicographic.ML")
    1.84  
    1.85  text {*
    1.86    \lstsml{Thy/examples/lexicographic.ML}
    1.87  *}
    1.88  
    1.89 +text {*
    1.90 +  In general, code theorems for overloaded constants may have more
    1.91 +  restrictive sort constraints than the underlying instance relation
    1.92 +  between class and type constructor as long as the whole system of
    1.93 +  constraints is coregular; code theorems violating coregularity
    1.94 +  are rejected immediately.
    1.95 +*}
    1.96 +
    1.97  subsubsection {* Haskell serialization *}
    1.98  
    1.99  text {*
   1.100 @@ -903,10 +909,10 @@
   1.101    (Haskell "Integer")
   1.102  
   1.103  text {*
   1.104 -    The code generator would produce
   1.105 -    an additional instance, which of course is rejected.
   1.106 -    To suppress this additional instance, use
   1.107 -    @{text "\<CODEINSTANCE>"}:
   1.108 +  The code generator would produce
   1.109 +  an additional instance, which of course is rejected.
   1.110 +  To suppress this additional instance, use
   1.111 +  @{text "\<CODEINSTANCE>"}:
   1.112  *}
   1.113  
   1.114  code_instance %tt bar :: eq
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Jan 25 16:57:57 2007 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri Jan 26 09:24:35 2007 +0100
     2.3 @@ -4,7 +4,6 @@
     2.4  %
     2.5  \isadelimtheory
     2.6  \isanewline
     2.7 -\isanewline
     2.8  %
     2.9  \endisadelimtheory
    2.10  %
    2.11 @@ -490,6 +489,21 @@
    2.12    the file system, with root given by the user.%
    2.13  \end{isamarkuptext}%
    2.14  \isamarkuptrue%
    2.15 +%
    2.16 +\isadelimML
    2.17 +%
    2.18 +\endisadelimML
    2.19 +%
    2.20 +\isatagML
    2.21 +\isacommand{ML}\isamarkupfalse%
    2.22 +\ {\isacharverbatimopen}\ set\ Toplevel{\isachardot}debug\ {\isacharverbatimclose}%
    2.23 +\endisatagML
    2.24 +{\isafoldML}%
    2.25 +%
    2.26 +\isadelimML
    2.27 +%
    2.28 +\endisadelimML
    2.29 +\isanewline
    2.30  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    2.31  \ dummy\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}%
    2.32  \begin{isamarkuptext}%
    2.33 @@ -1095,7 +1109,7 @@
    2.34  \end{isamarkuptext}%
    2.35  \isamarkuptrue%
    2.36  %
    2.37 -\isamarkupsubsubsection{lexicographic orderings and coregularity%
    2.38 +\isamarkupsubsubsection{lexicographic orderings%
    2.39  }
    2.40  \isamarkuptrue%
    2.41  %
    2.42 @@ -1106,68 +1120,12 @@
    2.43    us define a lexicographic ordering on tuples:%
    2.44  \end{isamarkuptext}%
    2.45  \isamarkuptrue%
    2.46 -%
    2.47 -\isadelimML
    2.48 -%
    2.49 -\endisadelimML
    2.50 -%
    2.51 -\isatagML
    2.52 -%
    2.53 -\endisatagML
    2.54 -{\isafoldML}%
    2.55 -%
    2.56 -\isadelimML
    2.57 -%
    2.58 -\endisadelimML
    2.59 -\isanewline
    2.60  \isacommand{instance}\isamarkupfalse%
    2.61  \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
    2.62  \ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
    2.63  \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
    2.64 -\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}p{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ \ {\isacharequal}\ p{\isadigit{2}}{\isachardoublequoteclose}%
    2.65 -\isadelimproof
    2.66 -\ %
    2.67 -\endisadelimproof
    2.68 -%
    2.69 -\isatagproof
    2.70 -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
    2.71 -\isanewline
    2.72 -%
    2.73 -\endisatagproof
    2.74 -{\isafoldproof}%
    2.75 -%
    2.76 -\isadelimproof
    2.77 -%
    2.78 -\endisadelimproof
    2.79 -%
    2.80 -\isadelimML
    2.81 -%
    2.82 -\endisadelimML
    2.83 -%
    2.84 -\isatagML
    2.85 -%
    2.86 -\endisatagML
    2.87 -{\isafoldML}%
    2.88 -%
    2.89 -\isadelimML
    2.90 -%
    2.91 -\endisadelimML
    2.92 -%
    2.93 -\begin{isamarkuptext}%
    2.94 -Then code generation will fail.  Why?  The definition
    2.95 -  of \isa{op\ {\isasymle}} depends on equality on both arguments,
    2.96 -  which are polymorphic and impose an additional \isa{eq}
    2.97 -  class constraint, thus violating the type discipline
    2.98 -  for class operations.
    2.99 -
   2.100 -  The solution is to add \isa{eq} to both sort arguments:%
   2.101 -\end{isamarkuptext}%
   2.102 -\isamarkuptrue%
   2.103 -\isacommand{instance}\isamarkupfalse%
   2.104 -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequoteopen}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isachardoublequoteclose}{\isacharcomma}\ {\isachardoublequoteopen}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}\ ord\isanewline
   2.105 -\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
   2.106 -\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.107 -\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}p{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}\ \ {\isacharequal}\ p{\isadigit{2}}{\isachardoublequoteclose}%
   2.108 +\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
   2.109 +\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
   2.110  \isadelimproof
   2.111  \ %
   2.112  \endisadelimproof
   2.113 @@ -1181,19 +1139,81 @@
   2.114  \isadelimproof
   2.115  %
   2.116  \endisadelimproof
   2.117 +\isanewline
   2.118 +\isanewline
   2.119 +\isacommand{lemma}\isamarkupfalse%
   2.120 +\ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   2.121 +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.122 +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.123 +%
   2.124 +\isadelimproof
   2.125 +\ \ %
   2.126 +\endisadelimproof
   2.127 +%
   2.128 +\isatagproof
   2.129 +\isacommand{unfolding}\isamarkupfalse%
   2.130 +\ {\isachardoublequoteopen}less{\isacharunderscore}eq{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ {\isachardoublequoteopen}less{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   2.131 +\ simp{\isacharunderscore}all%
   2.132 +\endisatagproof
   2.133 +{\isafoldproof}%
   2.134 +%
   2.135 +\isadelimproof
   2.136 +%
   2.137 +\endisadelimproof
   2.138 +%
   2.139 +\begin{isamarkuptext}%
   2.140 +Then code generation will fail.  Why?  The definition
   2.141 +  of \isa{op\ {\isasymle}} depends on equality on both arguments,
   2.142 +  which are polymorphic and impose an additional \isa{eq}
   2.143 +  class constraint, thus violating the type discipline
   2.144 +  for class operations.
   2.145 +
   2.146 +  The solution is to add \isa{eq} explicitly to the first sort arguments in the
   2.147 +  code theorems:%
   2.148 +\end{isamarkuptext}%
   2.149 +\isamarkuptrue%
   2.150 +\isanewline
   2.151 +\isacommand{lemma}\isamarkupfalse%
   2.152 +\ ord{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   2.153 +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.154 +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.155 +%
   2.156 +\isadelimproof
   2.157 +\ \ %
   2.158 +\endisadelimproof
   2.159 +%
   2.160 +\isatagproof
   2.161 +\isacommand{unfolding}\isamarkupfalse%
   2.162 +\ ord{\isacharunderscore}prod\ \isacommand{by}\isamarkupfalse%
   2.163 +\ rule{\isacharplus}%
   2.164 +\endisatagproof
   2.165 +{\isafoldproof}%
   2.166 +%
   2.167 +\isadelimproof
   2.168 +%
   2.169 +\endisadelimproof
   2.170  %
   2.171  \begin{isamarkuptext}%
   2.172  Then code generation succeeds:%
   2.173  \end{isamarkuptext}%
   2.174  \isamarkuptrue%
   2.175  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   2.176 -\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   2.177 +\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   2.178  \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   2.179  \begin{isamarkuptext}%
   2.180  \lstsml{Thy/examples/lexicographic.ML}%
   2.181  \end{isamarkuptext}%
   2.182  \isamarkuptrue%
   2.183  %
   2.184 +\begin{isamarkuptext}%
   2.185 +In general, code theorems for overloaded constants may have more
   2.186 +  restrictive sort constraints than the underlying instance relation
   2.187 +  between class and type constructor as long as the whole system of
   2.188 +  constraints is coregular; code theorems violating coregularity
   2.189 +  are rejected immediately.%
   2.190 +\end{isamarkuptext}%
   2.191 +\isamarkuptrue%
   2.192 +%
   2.193  \isamarkupsubsubsection{Haskell serialization%
   2.194  }
   2.195  \isamarkuptrue%
   2.196 @@ -1298,9 +1318,9 @@
   2.197  %
   2.198  \begin{isamarkuptext}%
   2.199  The code generator would produce
   2.200 -    an additional instance, which of course is rejected.
   2.201 -    To suppress this additional instance, use
   2.202 -    \isa{{\isasymCODEINSTANCE}}:%
   2.203 +  an additional instance, which of course is rejected.
   2.204 +  To suppress this additional instance, use
   2.205 +  \isa{{\isasymCODEINSTANCE}}:%
   2.206  \end{isamarkuptext}%
   2.207  \isamarkuptrue%
   2.208  %
   2.209 @@ -1521,7 +1541,7 @@
   2.210  
   2.211    For technical reasons, we further have to provide a
   2.212    synonym for \isa{None} which in code generator view
   2.213 -  is a function rather than a datatype constructor:%
   2.214 +  is a function rather than a term constructor:%
   2.215  \end{isamarkuptext}%
   2.216  \isamarkuptrue%
   2.217  \isacommand{definition}\isamarkupfalse%
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Jan 25 16:57:57 2007 +0100
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Jan 26 09:24:35 2007 +0100
     3.3 @@ -10,7 +10,7 @@
     3.4  heada (y : xs) = y;
     3.5  heada [] = Codegen.nulla;
     3.6  
     3.7 -null_option :: Maybe b;
     3.8 +null_option :: Maybe a;
     3.9  null_option = Nothing;
    3.10  
    3.11  instance Codegen.Null (Maybe b) where {
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Jan 25 16:57:57 2007 +0100
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Jan 26 09:24:35 2007 +0100
     4.3 @@ -11,15 +11,15 @@
     4.4  structure Codegen = 
     4.5  struct
     4.6  
     4.7 -type 'a null = {null_ : 'a};
     4.8 -fun null (A_:'a null) = #null_ A_;
     4.9 +type 'a null = {Codegen__null : 'a};
    4.10 +fun null (A_:'a null) = #Codegen__null A_;
    4.11  
    4.12 -fun head (A_:'a null) (y :: xs) = y
    4.13 -  | head (A_:'a null) [] = null A_;
    4.14 +fun head A_ (y :: xs) = y
    4.15 +  | head A_ [] = null A_;
    4.16  
    4.17 -val null_option : 'b option = NONE;
    4.18 +val null_option : 'a option = NONE;
    4.19  
    4.20 -fun null_optiona () = {null_ = null_option} : ('b option) null ;;
    4.21 +fun null_optiona () = {Codegen__null = null_option} : ('b option) null;
    4.22  
    4.23  val dummy : Nat.nat option =
    4.24    head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Jan 25 16:57:57 2007 +0100
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Jan 26 09:24:35 2007 +0100
     5.3 @@ -4,29 +4,29 @@
     5.4  structure Code_Generator = 
     5.5  struct
     5.6  
     5.7 -type 'a eq = {op_eq_ : 'a -> 'a -> bool};
     5.8 -fun op_eq (A_:'a eq) = #op_eq_ A_;
     5.9 +type 'a eq = {Code_Generator__op_eq : 'a -> 'a -> bool};
    5.10 +fun op_eq (A_:'a eq) = #Code_Generator__op_eq A_;
    5.11  
    5.12  end; (*struct Code_Generator*)
    5.13  
    5.14  structure List = 
    5.15  struct
    5.16  
    5.17 -fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
    5.18 +fun memberl A_ x (y :: ys) =
    5.19    Code_Generator.op_eq A_ x y orelse memberl A_ x ys
    5.20 -  | memberl (A_:'a Code_Generator.eq) x [] = false;
    5.21 +  | memberl A_ x [] = false;
    5.22  
    5.23  end; (*struct List*)
    5.24  
    5.25  structure Codegen = 
    5.26  struct
    5.27  
    5.28 -fun collect_duplicates (A_:'a Code_Generator.eq) xs ys (z :: zs) =
    5.29 +fun collect_duplicates A_ xs ys (z :: zs) =
    5.30    (if List.memberl A_ z xs
    5.31      then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
    5.32             else collect_duplicates A_ xs (z :: ys) zs)
    5.33      else collect_duplicates A_ (z :: xs) (z :: ys) zs)
    5.34 -  | collect_duplicates (A_:'a Code_Generator.eq) y ys [] = y;
    5.35 +  | collect_duplicates A_ y ys [] = y;
    5.36  
    5.37  end; (*struct Codegen*)
    5.38  
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Thu Jan 25 16:57:57 2007 +0100
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Fri Jan 26 09:24:35 2007 +0100
     6.3 @@ -1,50 +1,31 @@
     6.4  structure ROOT = 
     6.5  struct
     6.6  
     6.7 -structure Code_Generator = 
     6.8 -struct
     6.9 -
    6.10 -type 'a eq = {op_eq_ : 'a -> 'a -> bool};
    6.11 -fun op_eq (A_:'a eq) = #op_eq_ A_;
    6.12 -
    6.13 -end; (*struct Code_Generator*)
    6.14 -
    6.15 -structure Product_Type = 
    6.16 -struct
    6.17 -
    6.18 -fun op_eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq)
    6.19 -  (x1, y1) (x2, y2) =
    6.20 -  Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2;
    6.21 -
    6.22 -end; (*struct Product_Type*)
    6.23 -
    6.24  structure Orderings = 
    6.25  struct
    6.26  
    6.27 -type 'a ord = {less_eq_ : 'a -> 'a -> bool, less_ : 'a -> 'a -> bool};
    6.28 -fun less_eq (A_:'a ord) = #less_eq_ A_;
    6.29 -fun less (A_:'a ord) = #less_ A_;
    6.30 +type 'a ord =
    6.31 +  {Orderings__less_eq : 'a -> 'a -> bool,
    6.32 +    Orderings__less : 'a -> 'a -> bool};
    6.33 +fun less_eq (A_:'a ord) = #Orderings__less_eq A_;
    6.34 +fun less (A_:'a ord) = #Orderings__less A_;
    6.35  
    6.36  end; (*struct Orderings*)
    6.37  
    6.38 +structure Code_Generator = 
    6.39 +struct
    6.40 +
    6.41 +type 'a eq = {Code_Generator__op_eq : 'a -> 'a -> bool};
    6.42 +fun op_eq (A_:'a eq) = #Code_Generator__op_eq A_;
    6.43 +
    6.44 +end; (*struct Code_Generator*)
    6.45 +
    6.46  structure Codegen = 
    6.47  struct
    6.48  
    6.49 -fun less_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
    6.50 -  (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
    6.51 -  let
    6.52 -    val (x1, y1) = p1;
    6.53 -    val (x2, y2) = p2;
    6.54 -  in
    6.55 -    Orderings.less (#2 B_) x1 x2 orelse
    6.56 -      Code_Generator.op_eq (#1 B_) x1 x2 andalso
    6.57 -        Orderings.less (#2 C_) y1 y2
    6.58 -  end;
    6.59 -
    6.60 -fun less_eq_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
    6.61 -  (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
    6.62 -  less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
    6.63 -    Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2;
    6.64 +fun less_eq_prod (A1_, A2_) B_ (x1, y1) (x2, y2) =
    6.65 +  Orderings.less A2_ x1 x2 orelse
    6.66 +    Code_Generator.op_eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2;
    6.67  
    6.68  end; (*struct Codegen*)
    6.69