--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Apr 20 13:11:47 2007 +0200
@@ -280,14 +280,11 @@
text {*
\noindent which displays a table of constant with corresponding
defining equations (the additional stuff displayed
- shall not bother us for the moment). If this table does
- not provide at least one defining
- equation for a particular constant, the table of primitive
- definitions is searched
- whether it provides one.
+ shall not bother us for the moment).
The typical HOL tools are already set up in a way that
- function definitions introduced by @{text "\<FUN>"},
+ function definitions introduced by @{text "\<DEFINITION>"},
+ @{text "\<FUN>"},
@{text "\<FUNCTION>"}, @{text "\<PRIMREC>"}
@{text "\<RECDEF>"} are implicitly propagated
to this defining equation table. Specific theorems may be
@@ -861,15 +858,17 @@
*}
instance * :: (ord, ord) ord
- "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
+ less_prod_def: "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
- "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
+ less_eq_prod_def: "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" ..
+lemmas [code nofunc] = less_prod_def less_eq_prod_def
+
lemma ord_prod [code func]:
"(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
"(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
- unfolding "less_eq_*_def" "less_*_def" by simp_all
+ unfolding less_prod_def less_eq_prod_def by simp_all
text {*
Then code generation will fail. Why? The definition
@@ -883,7 +882,7 @@
*}
(*<*)
-declare ord_prod [code del]
+lemmas [code nofunc] = ord_prod
(*>*)
lemma ord_prod_code [code func]:
@@ -907,7 +906,10 @@
restrictive sort constraints than the underlying instance relation
between class and type constructor as long as the whole system of
constraints is coregular; code theorems violating coregularity
- are rejected immediately.
+ are rejected immediately. Consequently, it might be necessary
+ to delete disturbing theorems in the code theorem table,
+ as we have done here with the original definitions @{text less_prod_def}
+ and @{text less_eq_prod_def}.
*}
subsubsection {* Haskell serialization *}
@@ -1002,7 +1004,7 @@
expects dictionaries (namely an \emph{eq} dictionary) but
has also been given a customary serialization.
- The solution to this dilemma:
+ \fixme[needs rewrite] The solution to this dilemma:
*}
lemma [code func]:
@@ -1013,9 +1015,7 @@
text {*
\lstsml{Thy/examples/dirty_set.ML}
- Reflexive defining equations by convention are dropped.
- But their presence prevents primitive definitions to be
- used as defining equations:
+ Reflexive defining equations by convention are dropped:
*}
code_thms insert
@@ -1201,12 +1201,12 @@
text %mlref {*
\begin{mldecls}
- @{index_ML CodegenData.lazy: "(unit -> thm list) -> thm list Susp.T"}
+ @{index_ML CodegenData.lazy_thms: "(unit -> thm list) -> thm list Susp.T"}
\end{mldecls}
\begin{description}
- \item @{ML CodegenData.lazy}~@{text f} turns an abstract
+ \item @{ML CodegenData.lazy_thms}~@{text f} turns an abstract
theorem computation @{text f} into a suspension of theorems.
\end{description}
@@ -1294,7 +1294,7 @@
@{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\
@{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\
@{index_ML_structure CodegenConsts.Consttab} \\
- @{index_ML CodegenFunc.typ_func: "thm -> typ"} \\
+ @{index_ML CodegenFunc.head_func: "thm -> CodegenConsts.const * typ"} \\
@{index_ML CodegenFunc.rewrite_func: "thm list -> thm -> thm"} \\
\end{mldecls}
@@ -1309,8 +1309,8 @@
\item @{ML CodegenConsts.read_const}~@{text thy}~@{text s}
reads a constant as a concrete term expression @{text s}.
- \item @{ML CodegenFunc.typ_func}~@{text thm}
- extracts the type of a constant in a defining equation @{text thm}.
+ \item @{ML CodegenFunc.head_func}~@{text thm}
+ extracts the constant and its type from a defining equation @{text thm}.
\item @{ML CodegenFunc.rewrite_func}~@{text rews}~@{text thm}
rewrites a defining equation @{text thm} with a set of rewrite
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Apr 20 13:11:47 2007 +0200
@@ -332,14 +332,11 @@
\begin{isamarkuptext}%
\noindent which displays a table of constant with corresponding
defining equations (the additional stuff displayed
- shall not bother us for the moment). If this table does
- not provide at least one defining
- equation for a particular constant, the table of primitive
- definitions is searched
- whether it provides one.
+ shall not bother us for the moment).
The typical HOL tools are already set up in a way that
- function definitions introduced by \isa{{\isasymFUN}},
+ function definitions introduced by \isa{{\isasymDEFINITION}},
+ \isa{{\isasymFUN}},
\isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}}
\isa{{\isasymRECDEF}} are implicitly propagated
to this defining equation table. Specific theorems may be
@@ -1154,9 +1151,9 @@
\isamarkuptrue%
\isacommand{instance}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
-\ \ {\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
+\ \ less{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\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
\ \ \ \ 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
-\ \ {\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
+\ \ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\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
\ \ \ \ 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}%
\isadelimproof
\ %
@@ -1173,6 +1170,9 @@
\endisadelimproof
\isanewline
\isanewline
+\isacommand{lemmas}\isamarkupfalse%
+\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline
+\isanewline
\isacommand{lemma}\isamarkupfalse%
\ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\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
@@ -1184,7 +1184,7 @@
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
-\ {\isachardoublequoteopen}less{\isacharunderscore}eq{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ {\isachardoublequoteopen}less{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all%
\endisatagproof
{\isafoldproof}%
@@ -1242,7 +1242,10 @@
restrictive sort constraints than the underlying instance relation
between class and type constructor as long as the whole system of
constraints is coregular; code theorems violating coregularity
- are rejected immediately.%
+ are rejected immediately. Consequently, it might be necessary
+ to delete disturbing theorems in the code theorem table,
+ as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def}
+ and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1430,7 +1433,7 @@
expects dictionaries (namely an \emph{eq} dictionary) but
has also been given a customary serialization.
- The solution to this dilemma:%
+ \fixme[needs rewrite] The solution to this dilemma:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
@@ -1456,9 +1459,7 @@
\begin{isamarkuptext}%
\lstsml{Thy/examples/dirty_set.ML}
- Reflexive defining equations by convention are dropped.
- But their presence prevents primitive definitions to be
- used as defining equations:%
+ Reflexive defining equations by convention are dropped:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
@@ -1697,12 +1698,12 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{CodegenData.lazy}\verb|CodegenData.lazy: (unit -> thm list) -> thm list Susp.T|
+ \indexml{CodegenData.lazy-thms}\verb|CodegenData.lazy_thms: (unit -> thm list) -> thm list Susp.T|
\end{mldecls}
\begin{description}
- \item \verb|CodegenData.lazy|~\isa{f} turns an abstract
+ \item \verb|CodegenData.lazy_thms|~\isa{f} turns an abstract
theorem computation \isa{f} into a suspension of theorems.
\end{description}%
@@ -1822,7 +1823,7 @@
\indexml{CodegenConsts.eq-const}\verb|CodegenConsts.eq_const: CodegenConsts.const * CodegenConsts.const -> bool| \\
\indexml{CodegenConsts.read-const}\verb|CodegenConsts.read_const: theory -> string -> CodegenConsts.const| \\
\indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\
- \indexml{CodegenFunc.typ-func}\verb|CodegenFunc.typ_func: thm -> typ| \\
+ \indexml{CodegenFunc.head-func}\verb|CodegenFunc.head_func: thm -> CodegenConsts.const * typ| \\
\indexml{CodegenFunc.rewrite-func}\verb|CodegenFunc.rewrite_func: thm list -> thm -> thm| \\
\end{mldecls}
@@ -1837,8 +1838,8 @@
\item \verb|CodegenConsts.read_const|~\isa{thy}~\isa{s}
reads a constant as a concrete term expression \isa{s}.
- \item \verb|CodegenFunc.typ_func|~\isa{thm}
- extracts the type of a constant in a defining equation \isa{thm}.
+ \item \verb|CodegenFunc.head_func|~\isa{thm}
+ extracts the constant and its type from a defining equation \isa{thm}.
\item \verb|CodegenFunc.rewrite_func|~\isa{rews}~\isa{thm}
rewrites a defining equation \isa{thm} with a set of rewrite
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty Fri Apr 20 13:11:47 2007 +0200
@@ -31,6 +31,7 @@
\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
+\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
\newdimen\isa@parindent\newdimen\isa@parskip
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Fri Apr 20 13:11:47 2007 +0200
@@ -7,7 +7,7 @@
};
heada :: (Codegen.Null a) => [a] -> a;
-heada (y : xs) = y;
+heada (x : xs) = x;
heada [] = Codegen.nulla;
null_option :: Maybe a;
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Fri Apr 20 13:11:47 2007 +0200
@@ -6,9 +6,9 @@
datatype boola = True | False;
-fun op_and y True = y
+fun op_and x True = x
| op_and x False = False
- | op_and True y = y
+ | op_and True x = x
| op_and False x = False;
end; (*struct HOL*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Fri Apr 20 13:11:47 2007 +0200
@@ -14,7 +14,7 @@
type 'a null = {null : 'a};
fun null (A_:'a null) = #null A_;
-fun head A_ (y :: xs) = y
+fun head A_ (x :: xs) = x
| head A_ [] = null A_;
val null_option : 'a option = NONE;
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Fri Apr 20 13:11:47 2007 +0200
@@ -14,7 +14,7 @@
type 'a null = {null : 'a};;
let null _A = _A.null;;
-let rec head _A = function y :: xs -> y
+let rec head _A = function x :: xs -> x
| [] -> null _A;;
let rec null_option = None;;
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Fri Apr 20 13:11:47 2007 +0200
@@ -26,7 +26,7 @@
then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
else collect_duplicates A_ xs (z :: ys) zs)
else collect_duplicates A_ (z :: xs) (z :: ys) zs)
- | collect_duplicates A_ y ys [] = y;
+ | collect_duplicates A_ xs ys [] = xs;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Fri Apr 20 13:11:47 2007 +0200
@@ -7,7 +7,7 @@
datatype nat = Zero_nat | Suc of nat;
fun plus_nat (Suc m) n = plus_nat m (Suc n)
- | plus_nat Zero_nat y = y;
+ | plus_nat Zero_nat n = n;
fun times_nat (Suc m) n = plus_nat n (times_nat m n)
| times_nat Zero_nat n = Zero_nat;
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Fri Apr 20 13:11:47 2007 +0200
@@ -7,7 +7,7 @@
datatype nat = Zero_nat | Suc of nat;
fun plus_nat (Suc m) n = plus_nat m (Suc n)
- | plus_nat Zero_nat y = y;
+ | plus_nat Zero_nat n = n;
fun times_nat (Suc m) n = plus_nat n (times_nat m n)
| times_nat Zero_nat n = Zero_nat;
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Fri Apr 20 13:11:47 2007 +0200
@@ -13,7 +13,7 @@
fun minus_nat (Suc m) (Suc n) = minus_nat m n
| minus_nat Zero_nat n = Zero_nat
- | minus_nat y Zero_nat = y;
+ | minus_nat m Zero_nat = m;
end; (*struct Nat*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Fri Apr 20 13:11:47 2007 +0200
@@ -13,7 +13,7 @@
fun minus_nat (Suc m) (Suc n) = minus_nat m n
| minus_nat Zero_nat n = Zero_nat
- | minus_nat y Zero_nat = y;
+ | minus_nat m Zero_nat = m;
end; (*struct Nat*)