doc-src/IsarAdvanced/Codegen/Thy/Program.thy
changeset 28428 fd007794561f
parent 28419 f65e8b318581
child 28447 df77ed974a78
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Tue Sep 30 14:19:28 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Tue Sep 30 14:30:44 2008 +0200
     1.3 @@ -124,14 +124,14 @@
     1.4  
     1.5  text {*
     1.6    \noindent An inspection reveals that the equations stemming from the
     1.7 -  @{text primrec} statement within instantiation of class
     1.8 +  @{command primrec} statement within instantiation of class
     1.9    @{class semigroup} with type @{typ nat} are mapped to a separate
    1.10 -  function declaration @{text mult_nat} which in turn is used
    1.11 -  to provide the right hand side for the @{text "instance Semigroup Nat"}
    1.12 -  \fixme[courier fuer code text, isastyle fuer class].  This perfectly
    1.13 +  function declaration @{verbatim mult_nat} which in turn is used
    1.14 +  to provide the right hand side for the @{verbatim "instance Semigroup Nat"}.
    1.15 +  This perfectly
    1.16    agrees with the restriction that @{text inst} statements may
    1.17    only contain one single equation for each class class parameter
    1.18 -  The @{text instantiation} mechanism manages that for each
    1.19 +  The @{command instantiation} mechanism manages that for each
    1.20    overloaded constant @{text "f [\<kappa> \<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"}
    1.21    a \emph{shadow constant} @{text "f\<^isub>\<kappa> [\<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"} is
    1.22    declared satisfying @{text "f [\<kappa> \<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>] \<equiv> f\<^isub>\<kappa> [\<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"}.
    1.23 @@ -344,7 +344,7 @@
    1.24        else collect_duplicates (z#xs) (z#ys) zs)"
    1.25  
    1.26  text {*
    1.27 -  The membership test during preprocessing is rewritten,
    1.28 +  \noindent The membership test during preprocessing is rewritten,
    1.29    resulting in @{const List.member}, which itself
    1.30    performs an explicit equality check.
    1.31  *}
    1.32 @@ -368,32 +368,30 @@
    1.33    us define a lexicographic ordering on tuples:
    1.34  *}
    1.35  
    1.36 -instantiation * :: (ord, ord) ord
    1.37 +instantiation %quoteme * :: (ord, ord) ord
    1.38  begin
    1.39  
    1.40 -definition
    1.41 -  [code func del]: "p1 < p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in
    1.42 -    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2))"
    1.43 +definition %quoteme [code func del]:
    1.44 +  "p1 < p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \<or> (x1 = x2 \<and> y1 < y2))"
    1.45 +
    1.46 +definition %quoteme [code func del]:
    1.47 +  "p1 \<le> p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2))"
    1.48  
    1.49 -definition
    1.50 -  [code func del]: "p1 \<le> p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in
    1.51 -    x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2))"
    1.52 +instance %quoteme ..
    1.53  
    1.54 -instance ..
    1.55 +end %quoteme
    1.56  
    1.57 -end
    1.58 -
    1.59 -lemma ord_prod [code func(*<*), code func del(*>*)]:
    1.60 +lemma %quoteme ord_prod [code func]:
    1.61    "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
    1.62    "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
    1.63    unfolding less_prod_def less_eq_prod_def by simp_all
    1.64  
    1.65  text {*
    1.66 -  Then code generation will fail.  Why?  The definition
    1.67 +  \noindent Then code generation will fail.  Why?  The definition
    1.68    of @{term "op \<le>"} depends on equality on both arguments,
    1.69    which are polymorphic and impose an additional @{class eq}
    1.70 -  class constraint, thus violating the type discipline
    1.71 -  for class operations.
    1.72 +  class constraint, which the preprocessort does not propagate for technical
    1.73 +  reasons.
    1.74  
    1.75    The solution is to add @{class eq} explicitly to the first sort arguments in the
    1.76    code theorems:
    1.77 @@ -413,15 +411,6 @@
    1.78  text %quoteme {*@{code_stmts "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" (SML)}*}
    1.79  
    1.80  text {*
    1.81 -  In general, code theorems for overloaded constants may have more
    1.82 -  restrictive sort constraints than the underlying instance relation
    1.83 -  between class and type constructor as long as the whole system of
    1.84 -  constraints is coregular; code theorems violating coregularity
    1.85 -  are rejected immediately.  Consequently, it might be necessary
    1.86 -  to delete disturbing theorems in the code theorem table,
    1.87 -  as we have done here with the original definitions @{fact less_prod_def}
    1.88 -  and @{fact less_eq_prod_def}.
    1.89 -
    1.90    In some cases, the automatically derived defining equations
    1.91    for equality on a particular type may not be appropriate.
    1.92    As example, watch the following datatype representing
    1.93 @@ -442,7 +431,7 @@
    1.94    the theorem @{thm monotype_eq [no_vars]} already requires the
    1.95    instance @{text "monotype \<Colon> eq"}, which itself requires
    1.96    @{thm monotype_eq [no_vars]};  Haskell has no problem with mutually
    1.97 -  recursive @{text instance} and @{text function} definitions,
    1.98 +  recursive @{text inst} and @{text fun} definitions,
    1.99    but the SML serializer does not support this.
   1.100  
   1.101    In such cases, you have to provide you own equality equations