author haftmann Fri Apr 20 13:11:47 2007 +0200 (2007-04-20) changeset 22751 1bfd75c1f232 parent 22750 bff5d59de79b child 22752 8b3131eeb509
updated
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Apr 20 11:21:53 2007 +0200
1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Apr 20 13:11:47 2007 +0200
1.3 @@ -280,14 +280,11 @@
1.4  text {*
1.5    \noindent which displays a table of constant with corresponding
1.6    defining equations (the additional stuff displayed
1.7 -  shall not bother us for the moment). If this table does
1.8 -  not provide at least one defining
1.9 -  equation for a particular constant, the table of primitive
1.10 -  definitions is searched
1.11 -  whether it provides one.
1.12 +  shall not bother us for the moment).
1.13
1.14    The typical HOL tools are already set up in a way that
1.15 -  function definitions introduced by @{text "\<FUN>"},
1.16 +  function definitions introduced by @{text "\<DEFINITION>"},
1.17 +  @{text "\<FUN>"},
1.18    @{text "\<FUNCTION>"}, @{text "\<PRIMREC>"}
1.19    @{text "\<RECDEF>"} are implicitly propagated
1.20    to this defining equation table. Specific theorems may be
1.21 @@ -861,15 +858,17 @@
1.22  *}
1.23
1.24  instance * :: (ord, ord) ord
1.25 -  "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
1.26 +  less_prod_def: "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
1.27      x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
1.28 -  "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
1.29 +  less_eq_prod_def: "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
1.30      x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" ..
1.31
1.32 +lemmas [code nofunc] = less_prod_def less_eq_prod_def
1.33 +
1.34  lemma ord_prod [code func]:
1.35    "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
1.36    "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
1.37 -  unfolding "less_eq_*_def" "less_*_def" by simp_all
1.38 +  unfolding less_prod_def less_eq_prod_def by simp_all
1.39
1.40  text {*
1.41    Then code generation will fail.  Why?  The definition
1.42 @@ -883,7 +882,7 @@
1.43  *}
1.44
1.45  (*<*)
1.46 -declare ord_prod [code del]
1.47 +lemmas [code nofunc] = ord_prod
1.48  (*>*)
1.49
1.50  lemma ord_prod_code [code func]:
1.51 @@ -907,7 +906,10 @@
1.52    restrictive sort constraints than the underlying instance relation
1.53    between class and type constructor as long as the whole system of
1.54    constraints is coregular; code theorems violating coregularity
1.55 -  are rejected immediately.
1.56 +  are rejected immediately.  Consequently, it might be necessary
1.57 +  to delete disturbing theorems in the code theorem table,
1.58 +  as we have done here with the original definitions @{text less_prod_def}
1.59 +  and @{text less_eq_prod_def}.
1.60  *}
1.61
1.62  subsubsection {* Haskell serialization *}
1.63 @@ -1002,7 +1004,7 @@
1.64    expects dictionaries (namely an \emph{eq} dictionary) but
1.65    has also been given a customary serialization.
1.66
1.67 -  The solution to this dilemma:
1.68 +  \fixme[needs rewrite] The solution to this dilemma:
1.69  *}
1.70
1.71  lemma [code func]:
1.72 @@ -1013,9 +1015,7 @@
1.73  text {*
1.74    \lstsml{Thy/examples/dirty_set.ML}
1.75
1.76 -  Reflexive defining equations by convention are dropped.
1.77 -  But their presence prevents primitive definitions to be
1.78 -  used as defining equations:
1.79 +  Reflexive defining equations by convention are dropped:
1.80  *}
1.81
1.82  code_thms insert
1.83 @@ -1201,12 +1201,12 @@
1.84
1.85  text %mlref {*
1.86    \begin{mldecls}
1.87 -  @{index_ML CodegenData.lazy: "(unit -> thm list) -> thm list Susp.T"}
1.88 +  @{index_ML CodegenData.lazy_thms: "(unit -> thm list) -> thm list Susp.T"}
1.89    \end{mldecls}
1.90
1.91    \begin{description}
1.92
1.93 -  \item @{ML CodegenData.lazy}~@{text f} turns an abstract
1.94 +  \item @{ML CodegenData.lazy_thms}~@{text f} turns an abstract
1.95       theorem computation @{text f} into a suspension of theorems.
1.96
1.97    \end{description}
1.98 @@ -1294,7 +1294,7 @@
1.99    @{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\
1.100    @{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\
1.101    @{index_ML_structure CodegenConsts.Consttab} \\
1.102 -  @{index_ML CodegenFunc.typ_func: "thm -> typ"} \\
1.103 +  @{index_ML CodegenFunc.head_func: "thm -> CodegenConsts.const * typ"} \\
1.104    @{index_ML CodegenFunc.rewrite_func: "thm list -> thm -> thm"} \\
1.105    \end{mldecls}
1.106
1.107 @@ -1309,8 +1309,8 @@
1.108    \item @{ML CodegenConsts.read_const}~@{text thy}~@{text s}
1.109       reads a constant as a concrete term expression @{text s}.
1.110
1.111 -  \item @{ML CodegenFunc.typ_func}~@{text thm}
1.112 -     extracts the type of a constant in a defining equation @{text thm}.
1.113 +  \item @{ML CodegenFunc.head_func}~@{text thm}
1.114 +     extracts the constant and its type from a defining equation @{text thm}.
1.115
1.116    \item @{ML CodegenFunc.rewrite_func}~@{text rews}~@{text thm}
1.117       rewrites a defining equation @{text thm} with a set of rewrite

     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri Apr 20 11:21:53 2007 +0200
2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri Apr 20 13:11:47 2007 +0200
2.3 @@ -332,14 +332,11 @@
2.4  \begin{isamarkuptext}%
2.5  \noindent which displays a table of constant with corresponding
2.6    defining equations (the additional stuff displayed
2.7 -  shall not bother us for the moment). If this table does
2.8 -  not provide at least one defining
2.9 -  equation for a particular constant, the table of primitive
2.10 -  definitions is searched
2.11 -  whether it provides one.
2.12 +  shall not bother us for the moment).
2.13
2.14    The typical HOL tools are already set up in a way that
2.15 -  function definitions introduced by \isa{{\isasymFUN}},
2.16 +  function definitions introduced by \isa{{\isasymDEFINITION}},
2.17 +  \isa{{\isasymFUN}},
2.18    \isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}}
2.19    \isa{{\isasymRECDEF}} are implicitly propagated
2.20    to this defining equation table. Specific theorems may be
2.21 @@ -1154,9 +1151,9 @@
2.22  \isamarkuptrue%
2.23  \isacommand{instance}\isamarkupfalse%
2.24  \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
2.32  \ %
2.33 @@ -1173,6 +1170,9 @@
2.35  \isanewline
2.36  \isanewline
2.37 +\isacommand{lemmas}\isamarkupfalse%
2.38 +\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline
2.39 +\isanewline
2.40  \isacommand{lemma}\isamarkupfalse%
2.41  \ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
2.43 @@ -1184,7 +1184,7 @@
2.44  %
2.45  \isatagproof
2.46  \isacommand{unfolding}\isamarkupfalse%
2.47 -\ {\isachardoublequoteopen}less{\isacharunderscore}eq{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ {\isachardoublequoteopen}less{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
2.48 +\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
2.49  \ simp{\isacharunderscore}all%
2.50  \endisatagproof
2.51  {\isafoldproof}%
2.52 @@ -1242,7 +1242,10 @@
2.53    restrictive sort constraints than the underlying instance relation
2.54    between class and type constructor as long as the whole system of
2.55    constraints is coregular; code theorems violating coregularity
2.56 -  are rejected immediately.%
2.57 +  are rejected immediately.  Consequently, it might be necessary
2.58 +  to delete disturbing theorems in the code theorem table,
2.59 +  as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def}
2.60 +  and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.%
2.61  \end{isamarkuptext}%
2.62  \isamarkuptrue%
2.63  %
2.64 @@ -1430,7 +1433,7 @@
2.65    expects dictionaries (namely an \emph{eq} dictionary) but
2.66    has also been given a customary serialization.
2.67
2.68 -  The solution to this dilemma:%
2.69 +  \fixme[needs rewrite] The solution to this dilemma:%
2.70  \end{isamarkuptext}%
2.71  \isamarkuptrue%
2.72  \isacommand{lemma}\isamarkupfalse%
2.73 @@ -1456,9 +1459,7 @@
2.74  \begin{isamarkuptext}%
2.75  \lstsml{Thy/examples/dirty_set.ML}
2.76
2.77 -  Reflexive defining equations by convention are dropped.
2.78 -  But their presence prevents primitive definitions to be
2.79 -  used as defining equations:%
2.80 +  Reflexive defining equations by convention are dropped:%
2.81  \end{isamarkuptext}%
2.82  \isamarkuptrue%
2.83  \isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
2.84 @@ -1697,12 +1698,12 @@
2.85  %
2.86  \begin{isamarkuptext}%
2.87  \begin{mldecls}
2.88 -  \indexml{CodegenData.lazy}\verb|CodegenData.lazy: (unit -> thm list) -> thm list Susp.T|
2.89 +  \indexml{CodegenData.lazy-thms}\verb|CodegenData.lazy_thms: (unit -> thm list) -> thm list Susp.T|
2.90    \end{mldecls}
2.91
2.92    \begin{description}
2.93
2.94 -  \item \verb|CodegenData.lazy|~\isa{f} turns an abstract
2.95 +  \item \verb|CodegenData.lazy_thms|~\isa{f} turns an abstract
2.96       theorem computation \isa{f} into a suspension of theorems.
2.97
2.98    \end{description}%
2.99 @@ -1822,7 +1823,7 @@
2.100    \indexml{CodegenConsts.eq-const}\verb|CodegenConsts.eq_const: CodegenConsts.const * CodegenConsts.const -> bool| \\
2.102    \indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\
2.103 -  \indexml{CodegenFunc.typ-func}\verb|CodegenFunc.typ_func: thm -> typ| \\
2.105    \indexml{CodegenFunc.rewrite-func}\verb|CodegenFunc.rewrite_func: thm list -> thm -> thm| \\
2.106    \end{mldecls}
2.107
2.108 @@ -1837,8 +1838,8 @@
2.110       reads a constant as a concrete term expression \isa{s}.
2.111
2.112 -  \item \verb|CodegenFunc.typ_func|~\isa{thm}
2.113 -     extracts the type of a constant in a defining equation \isa{thm}.
2.115 +     extracts the constant and its type from a defining equation \isa{thm}.
2.116
2.117    \item \verb|CodegenFunc.rewrite_func|~\isa{rews}~\isa{thm}
2.118       rewrites a defining equation \isa{thm} with a set of rewrite

     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty	Fri Apr 20 11:21:53 2007 +0200
3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty	Fri Apr 20 13:11:47 2007 +0200
3.3 @@ -31,6 +31,7 @@
3.4  \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
3.5  \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
3.6  \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
3.7 +\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
3.8
3.9
3.10  \newdimen\isa@parindent\newdimen\isa@parskip

     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Apr 20 11:21:53 2007 +0200
4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Apr 20 13:11:47 2007 +0200
4.3 @@ -7,7 +7,7 @@
4.4  };
4.5
4.6  heada :: (Codegen.Null a) => [a] -> a;
4.7 -heada (y : xs) = y;
4.8 +heada (x : xs) = x;
4.10
4.11  null_option :: Maybe a;

     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Fri Apr 20 11:21:53 2007 +0200
5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Fri Apr 20 13:11:47 2007 +0200
5.3 @@ -6,9 +6,9 @@
5.4
5.5  datatype boola = True | False;
5.6
5.7 -fun op_and y True = y
5.8 +fun op_and x True = x
5.9    | op_and x False = False
5.10 -  | op_and True y = y
5.11 +  | op_and True x = x
5.12    | op_and False x = False;
5.13
5.14  end; (*struct HOL*)

     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Apr 20 11:21:53 2007 +0200
6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Apr 20 13:11:47 2007 +0200
6.3 @@ -14,7 +14,7 @@
6.4  type 'a null = {null : 'a};
6.5  fun null (A_:'a null) = #null A_;
6.6
6.7 -fun head A_ (y :: xs) = y
6.8 +fun head A_ (x :: xs) = x
6.9    | head A_ [] = null A_;
6.10
6.11  val null_option : 'a option = NONE;

     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Fri Apr 20 11:21:53 2007 +0200
7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Fri Apr 20 13:11:47 2007 +0200
7.3 @@ -14,7 +14,7 @@
7.4  type 'a null = {null : 'a};;
7.5  let null _A = _A.null;;
7.6
7.7 -let rec head _A = function y :: xs -> y
7.8 +let rec head _A = function x :: xs -> x
7.9                    | [] -> null _A;;
7.10
7.11  let rec null_option = None;;

     8.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Apr 20 11:21:53 2007 +0200
8.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Apr 20 13:11:47 2007 +0200
8.3 @@ -26,7 +26,7 @@
8.4      then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
8.5             else collect_duplicates A_ xs (z :: ys) zs)
8.6      else collect_duplicates A_ (z :: xs) (z :: ys) zs)
8.7 -  | collect_duplicates A_ y ys [] = y;
8.8 +  | collect_duplicates A_ xs ys [] = xs;
8.9
8.10  end; (*struct Codegen*)
8.11

     9.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Fri Apr 20 11:21:53 2007 +0200
9.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Fri Apr 20 13:11:47 2007 +0200
9.3 @@ -7,7 +7,7 @@
9.4  datatype nat = Zero_nat | Suc of nat;
9.5
9.6  fun plus_nat (Suc m) n = plus_nat m (Suc n)
9.7 -  | plus_nat Zero_nat y = y;
9.8 +  | plus_nat Zero_nat n = n;
9.9
9.10  fun times_nat (Suc m) n = plus_nat n (times_nat m n)
9.11    | times_nat Zero_nat n = Zero_nat;

    10.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Fri Apr 20 11:21:53 2007 +0200
10.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Fri Apr 20 13:11:47 2007 +0200
10.3 @@ -7,7 +7,7 @@
10.4  datatype nat = Zero_nat | Suc of nat;
10.5
10.6  fun plus_nat (Suc m) n = plus_nat m (Suc n)
10.7 -  | plus_nat Zero_nat y = y;
10.8 +  | plus_nat Zero_nat n = n;
10.9
10.10  fun times_nat (Suc m) n = plus_nat n (times_nat m n)
10.11    | times_nat Zero_nat n = Zero_nat;

    11.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Fri Apr 20 11:21:53 2007 +0200
11.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Fri Apr 20 13:11:47 2007 +0200
11.3 @@ -13,7 +13,7 @@
11.4
11.5  fun minus_nat (Suc m) (Suc n) = minus_nat m n
11.6    | minus_nat Zero_nat n = Zero_nat
11.7 -  | minus_nat y Zero_nat = y;
11.8 +  | minus_nat m Zero_nat = m;
11.9
11.10  end; (*struct Nat*)
11.11

    12.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Fri Apr 20 11:21:53 2007 +0200
12.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Fri Apr 20 13:11:47 2007 +0200
12.3 @@ -13,7 +13,7 @@
12.4
12.5  fun minus_nat (Suc m) (Suc n) = minus_nat m n
12.6    | minus_nat Zero_nat n = Zero_nat
12.7 -  | minus_nat y Zero_nat = y;
12.8 +  | minus_nat m Zero_nat = m;
12.9
12.10  end; (*struct Nat*)
12.11