--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu May 10 04:06:56 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu May 10 10:21:44 2007 +0200
@@ -81,7 +81,7 @@
by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
So, for the moment, there are two distinct code generators
in Isabelle.
- Also note that while the framework itself is largely
+ Also note that while the framework itself is
object-logic independent, only @{text HOL} provides a reasonable
framework setup.
\end{warn}
@@ -91,7 +91,8 @@
section {* An example: a simple theory of search trees \label{sec:example} *}
text {*
- When writing executable specifications, it is convenient to use
+ When writing executable specifications using @{text HOL},
+ it is convenient to use
three existing packages: the datatype package for defining
datatypes, the function package for (recursive) functions,
and the class package for overloaded definitions.
@@ -208,7 +209,7 @@
subsection {* Invoking the code generator *}
text {*
- Thanks to a reasonable setup of the HOL theories, in
+ Thanks to a reasonable setup of the @{text HOL} theories, in
most cases code generation proceeds without further ado:
*}
@@ -277,7 +278,7 @@
defining equations (the additional stuff displayed
shall not bother us for the moment).
- The typical HOL tools are already set up in a way that
+ The typical @{text HOL} tools are already set up in a way that
function definitions introduced by @{text "\<DEFINITION>"},
@{text "\<FUN>"},
@{text "\<FUNCTION>"}, @{text "\<PRIMREC>"},
@@ -450,17 +451,18 @@
subsection {* Library theories \label{sec:library} *}
text {*
- The HOL \emph{Main} theory already provides a code generator setup
+ The @{text HOL} @{text Main} theory already provides a code
+ generator setup
which should be suitable for most applications. Common extensions
- and modifications are available by certain theories of the HOL
+ and modifications are available by certain theories of the @{text HOL}
library; beside being useful in applications, they may serve
as a tutorial for customizing the code generator setup.
\begin{description}
- \item[@{text "Pretty_Int"}] represents HOL integers by big
+ \item[@{text "Pretty_Int"}] represents @{text HOL} integers by big
integer literals in target languages.
- \item[@{text "Pretty_Char"}] represents HOL characters by
+ \item[@{text "Pretty_Char"}] represents @{text HOL} characters by
character literals in target languages.
\item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char_chr"},
but also offers treatment of character codes; includes
@@ -474,11 +476,18 @@
matching with @{const "0\<Colon>nat"} / @{const "Suc"}
is eliminated; includes @{text "Pretty_Int"}.
\item[@{text "MLString"}] provides an additional datatype @{text "mlstring"};
- in the HOL default setup, strings in HOL are mapped to list
- of HOL characters in SML; values of type @{text "mlstring"} are
+ in the @{text HOL} default setup, strings in HOL are mapped to list
+ of @{text HOL} characters in SML; values of type @{text "mlstring"} are
mapped to strings in SML.
\end{description}
+
+ \begin{warn}
+ When importing any of these theories, they should form the last
+ items in an import list. Since these theories adapt the
+ code generator setup in a non-conservative fashion,
+ strange effects may occur otherwise.
+ \end{warn}
*}
subsection {* Preprocessing *}
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu May 10 04:06:56 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu May 10 10:21:44 2007 +0200
@@ -106,7 +106,7 @@
by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
So, for the moment, there are two distinct code generators
in Isabelle.
- Also note that while the framework itself is largely
+ Also note that while the framework itself is
object-logic independent, only \isa{HOL} provides a reasonable
framework setup.
\end{warn}%
@@ -118,7 +118,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-When writing executable specifications, it is convenient to use
+When writing executable specifications using \isa{HOL},
+ it is convenient to use
three existing packages: the datatype package for defining
datatypes, the function package for (recursive) functions,
and the class package for overloaded definitions.
@@ -241,7 +242,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Thanks to a reasonable setup of the HOL theories, in
+Thanks to a reasonable setup of the \isa{HOL} theories, in
most cases code generation proceeds without further ado:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -330,7 +331,7 @@
defining equations (the additional stuff displayed
shall not bother us for the moment).
- The typical HOL tools are already set up in a way that
+ The typical \isa{HOL} tools are already set up in a way that
function definitions introduced by \isa{{\isasymDEFINITION}},
\isa{{\isasymFUN}},
\isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}},
@@ -571,17 +572,18 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The HOL \emph{Main} theory already provides a code generator setup
+The \isa{HOL} \isa{Main} theory already provides a code
+ generator setup
which should be suitable for most applications. Common extensions
- and modifications are available by certain theories of the HOL
+ and modifications are available by certain theories of the \isa{HOL}
library; beside being useful in applications, they may serve
as a tutorial for customizing the code generator setup.
\begin{description}
- \item[\isa{Pretty{\isacharunderscore}Int}] represents HOL integers by big
+ \item[\isa{Pretty{\isacharunderscore}Int}] represents \isa{HOL} integers by big
integer literals in target languages.
- \item[\isa{Pretty{\isacharunderscore}Char}] represents HOL characters by
+ \item[\isa{Pretty{\isacharunderscore}Char}] represents \isa{HOL} characters by
character literals in target languages.
\item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr},
but also offers treatment of character codes; includes
@@ -595,11 +597,18 @@
matching with \isa{{\isadigit{0}}} / \isa{Suc}
is eliminated; includes \isa{Pretty{\isacharunderscore}Int}.
\item[\isa{MLString}] provides an additional datatype \isa{mlstring};
- in the HOL default setup, strings in HOL are mapped to list
- of HOL characters in SML; values of type \isa{mlstring} are
+ in the \isa{HOL} default setup, strings in HOL are mapped to list
+ of \isa{HOL} characters in SML; values of type \isa{mlstring} are
mapped to strings in SML.
- \end{description}%
+ \end{description}
+
+ \begin{warn}
+ When importing any of these theories, they should form the last
+ items in an import list. Since these theories adapt the
+ code generator setup in a non-conservative fashion,
+ strange effects may occur otherwise.
+ \end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/src/HOL/Divides.thy Thu May 10 04:06:56 2007 +0200
+++ b/src/HOL/Divides.thy Thu May 10 10:21:44 2007 +0200
@@ -34,7 +34,7 @@
instance nat :: "Divides.div"
mod_def: "m mod n == wfrec (pred_nat^+)
(%f j. if j<n | n=0 then j else f (j-n)) m"
- div_def: "m div n == wfrec (pred_nat^+)
+ div_def: "m div n == wfrec (pred_nat^+)
(%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
definition
--- a/src/HOL/Lattices.thy Thu May 10 04:06:56 2007 +0200
+++ b/src/HOL/Lattices.thy Thu May 10 10:21:44 2007 +0200
@@ -13,8 +13,8 @@
text{*
This theory of lattices only defines binary sup and inf
- operations. The extension to (finite) sets is done in theories
- @{text FixedPoint} and @{text Finite_Set}.
+ operations. The extension to complete lattices is done in theory
+ @{text FixedPoint}.
*}
class lower_semilattice = order +
@@ -278,17 +278,24 @@
qed
-subsection {* min/max on linear orders as special case of inf/sup *}
+subsection {* @{const min}/@{const max} on linear orders as
+ special case of @{const inf}/@{const sup} *}
+
+lemma (in linorder) distrib_lattice_min_max:
+ "distrib_lattice_pred (op \<^loc>\<le>) (op \<^loc><) min max"
+proof unfold_locales
+ have aux: "\<And>x y \<Colon> 'a. x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
+ by (auto simp add: less_le antisym)
+ fix x y z
+ show "max x (min y z) = min (max x y) (max x z)"
+ unfolding min_def max_def
+ by (auto simp add: intro: antisym, unfold not_le,
+ auto intro: less_trans le_less_trans aux)
+qed (auto simp add: min_def max_def not_le less_imp_le)
interpretation min_max:
distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
-apply unfold_locales
-apply (simp add: min_def linorder_not_le order_less_imp_le)
-apply (simp add: min_def linorder_not_le order_less_imp_le)
-apply (simp add: min_def linorder_not_le order_less_imp_le)
-apply (simp add: max_def linorder_not_le order_less_imp_le)
-apply (simp add: max_def linorder_not_le order_less_imp_le)
-unfolding min_def max_def by auto
+ by (rule distrib_lattice_min_max [unfolded linorder_class_min linorder_class_max])
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
by (rule ext)+ auto
--- a/src/HOL/Library/AssocList.thy Thu May 10 04:06:56 2007 +0200
+++ b/src/HOL/Library/AssocList.thy Thu May 10 10:21:44 2007 +0200
@@ -7,7 +7,6 @@
theory AssocList
imports Map
-
begin
text {*
@@ -541,32 +540,20 @@
subsection {* @{const compose} *}
(* ******************************************************************************** *)
-lemma compose_induct [case_names Nil Cons]:
- fixes xs ys
- assumes Nil: "P [] ys"
- assumes Cons: "\<And>x xs.
- (\<And>v. map_of ys (snd x) = Some v \<Longrightarrow> P xs ys)
- \<Longrightarrow> (map_of ys (snd x) = None \<Longrightarrow> P (delete (fst x) xs) ys)
- \<Longrightarrow> P (x # xs) ys"
- shows "P xs ys"
-by (induct xs rule: compose.induct [where ?P="\<lambda>xs zs. P xs ys"])
- (auto intro: Nil Cons)
lemma compose_first_None [simp]:
assumes "map_of xs k = None"
shows "map_of (compose xs ys) k = None"
-using prems
-by (induct xs ys rule: compose_induct) (auto split: option.splits split_if_asm)
+using prems by (induct xs ys rule: compose.induct)
+ (auto split: option.splits split_if_asm)
lemma compose_conv:
shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
-proof (induct xs ys rule: compose_induct)
- case Nil thus ?case by simp
+proof (induct xs ys rule: compose.induct)
+ case 1 then show ?case by simp
next
- case (Cons x xs)
- show ?case
+ case (2 x xs ys) show ?case
proof (cases "map_of ys (snd x)")
- case None
- with Cons
+ case None with 2
have hyp: "map_of (compose (delete (fst x) xs) ys) k =
(map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
by simp
@@ -589,7 +576,7 @@
qed
next
case (Some v)
- with Cons
+ with 2
have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
by simp
with Some show ?thesis
@@ -607,14 +594,14 @@
using prems by (simp add: compose_conv)
lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
-proof (induct xs ys rule: compose_induct)
- case Nil thus ?case by simp
+proof (induct xs ys rule: compose.induct)
+ case 1 thus ?case by simp
next
- case (Cons x xs)
+ case (2 x xs ys)
show ?case
proof (cases "map_of ys (snd x)")
case None
- with Cons.hyps
+ with "2.hyps"
have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
by simp
also
@@ -625,7 +612,7 @@
by auto
next
case (Some v)
- with Cons.hyps
+ with "2.hyps"
have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
by simp
with Some show ?thesis
@@ -637,30 +624,30 @@
assumes "distinct (map fst xs)"
shows "distinct (map fst (compose xs ys))"
using prems
-proof (induct xs ys rule: compose_induct)
- case Nil thus ?case by simp
+proof (induct xs ys rule: compose.induct)
+ case 1 thus ?case by simp
next
- case (Cons x xs)
+ case (2 x xs ys)
show ?case
proof (cases "map_of ys (snd x)")
case None
- with Cons show ?thesis by simp
+ with 2 show ?thesis by simp
next
case (Some v)
- with Cons dom_compose [of xs ys] show ?thesis
+ with 2 dom_compose [of xs ys] show ?thesis
by (auto)
qed
qed
lemma compose_delete_twist: "(compose (delete k xs) ys) = delete k (compose xs ys)"
-proof (induct xs ys rule: compose_induct)
- case Nil thus ?case by simp
+proof (induct xs ys rule: compose.induct)
+ case 1 thus ?case by simp
next
- case (Cons x xs)
+ case (2 x xs ys)
show ?case
proof (cases "map_of ys (snd x)")
case None
- with Cons have
+ with 2 have
hyp: "compose (delete k (delete (fst x) xs)) ys =
delete k (compose (delete (fst x) xs) ys)"
by simp
@@ -678,14 +665,14 @@
qed
next
case (Some v)
- with Cons have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp
+ with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp
with Some show ?thesis
by simp
qed
qed
lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
- by (induct xs ys rule: compose_induct)
+ by (induct xs ys rule: compose.induct)
(auto simp add: map_of_clearjunk split: option.splits)
lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
@@ -695,8 +682,7 @@
lemma compose_empty [simp]:
"compose xs [] = []"
- by (induct xs rule: compose_induct [where ys="[]"]) auto
-
+ by (induct xs) (auto simp add: compose_delete_twist)
lemma compose_Some_iff:
"(map_of (compose xs ys) k = Some v) =
--- a/src/HOL/Orderings.thy Thu May 10 04:06:56 2007 +0200
+++ b/src/HOL/Orderings.thy Thu May 10 10:21:44 2007 +0200
@@ -81,6 +81,8 @@
notation (input)
greater_eq (infix "\<ge>" 50)
+hide const min max
+
definition
min :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
"min a b = (if a \<le> b then a else b)"
@@ -89,11 +91,11 @@
max :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
"max a b = (if a \<le> b then b else a)"
-lemma min_linorder:
+lemma linorder_class_min:
"ord.min (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = min"
by rule+ (simp add: min_def ord_class.min_def)
-lemma max_linorder:
+lemma linorder_class_max:
"ord.max (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = max"
by rule+ (simp add: max_def ord_class.max_def)
@@ -193,6 +195,14 @@
lemma less_asym': "a \<^loc>< b \<Longrightarrow> b \<^loc>< a \<Longrightarrow> P"
by (rule less_asym)
+
+text {* Reverse order *}
+
+lemma order_reverse:
+ "order_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+ by unfold_locales
+ (simp add: less_le, auto intro: antisym order_trans)
+
end
@@ -252,6 +262,15 @@
lemma not_leE: "\<not> y \<^loc>\<le> x \<Longrightarrow> x \<^loc>< y"
unfolding not_le .
+
+text {* Reverse order *}
+
+lemma linorder_reverse:
+ "linorder_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+ by unfold_locales
+ (simp add: less_le, auto intro: antisym order_trans simp add: linear)
+
+
text {* min/max properties *}
lemma min_le_iff_disj:
@@ -288,8 +307,7 @@
end
-
-subsection {* Name duplicates *}
+subsection {* Name duplicates -- including min/max interpretation *}
lemmas order_less_le = less_le
lemmas order_eq_refl = order_class.eq_refl
@@ -330,6 +348,15 @@
lemmas leD = linorder_class.leD
lemmas not_leE = linorder_class.not_leE
+lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [unfolded linorder_class_min]
+lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [unfolded linorder_class_max]
+lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [unfolded linorder_class_min]
+lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [unfolded linorder_class_max]
+lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [unfolded linorder_class_min]
+lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [unfolded linorder_class_max]
+lemmas split_min = linorder_class.split_min [unfolded linorder_class_min]
+lemmas split_max = linorder_class.split_max [unfolded linorder_class_max]
+
subsection {* Reasoning tools setup *}
@@ -346,18 +373,18 @@
T <> HOLogic.natT andalso T <> HOLogic.intT
andalso T <> HOLogic.realT andalso Sign.of_sort thy (T, sort)
end;
- fun dec (Const ("Not", _) $ t) = (case dec t
+ fun dec (Const (@{const_name Not}, _) $ t) = (case dec t
of NONE => NONE
| SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
- | dec (Const ("op =", _) $ t1 $ t2) =
+ | dec (Const (@{const_name "op ="}, _) $ t1 $ t2) =
if of_sort t1
then SOME (t1, "=", t2)
else NONE
- | dec (Const ("Orderings.less_eq", _) $ t1 $ t2) =
+ | dec (Const (@{const_name less_eq}, _) $ t1 $ t2) =
if of_sort t1
then SOME (t1, "<=", t2)
else NONE
- | dec (Const ("Orderings.less", _) $ t1 $ t2) =
+ | dec (Const (@{const_name less}, _) $ t1 $ t2) =
if of_sort t1
then SOME (t1, "<", t2)
else NONE
@@ -417,7 +444,7 @@
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
let val prems = prems_of_ss ss;
- val less = Const("Orderings.less",T);
+ val less = Const (@{const_name less}, T);
val t = HOLogic.mk_Trueprop(le $ s $ r);
in case find_first (prp t) prems of
NONE =>
@@ -432,7 +459,7 @@
fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
let val prems = prems_of_ss ss;
- val le = Const("Orderings.less_eq",T);
+ val le = Const (@{const_name less_eq}, T);
val t = HOLogic.mk_Trueprop(le $ r $ s);
in case find_first (prp t) prems of
NONE =>
@@ -521,12 +548,12 @@
print_translation {*
let
- val All_binder = Syntax.binder_name @{const_syntax "All"};
- val Ex_binder = Syntax.binder_name @{const_syntax "Ex"};
+ val All_binder = Syntax.binder_name @{const_syntax All};
+ val Ex_binder = Syntax.binder_name @{const_syntax Ex};
val impl = @{const_syntax "op -->"};
val conj = @{const_syntax "op &"};
- val less = @{const_syntax "less"};
- val less_eq = @{const_syntax "less_eq"};
+ val less = @{const_syntax less};
+ val less_eq = @{const_syntax less_eq};
val trans =
[((All_binder, impl, less), ("_All_less", "_All_greater")),
@@ -801,7 +828,7 @@
instance bool :: order
le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
- by default (auto simp add: le_bool_def less_bool_def)
+ by intro_classes (auto simp add: le_bool_def less_bool_def)
lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
by (simp add: le_bool_def)
@@ -854,15 +881,6 @@
apply (auto intro!: order_antisym)
done
-lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [unfolded min_linorder]
-lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [unfolded max_linorder]
-lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [unfolded min_linorder]
-lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [unfolded max_linorder]
-lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [unfolded min_linorder]
-lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [unfolded max_linorder]
-lemmas split_min = linorder_class.split_min [unfolded min_linorder]
-lemmas split_max = linorder_class.split_max [unfolded max_linorder]
-
lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
by (simp add: min_def)
--- a/src/Pure/Tools/codegen_func.ML Thu May 10 04:06:56 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML Thu May 10 10:21:44 2007 +0200
@@ -103,7 +103,7 @@
| check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
| check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
then bad_thm
- ("Partially applied constant on left hand side of equation"
+ ("Partially applied constant on left hand side of equation\n"
^ Display.string_of_thm thm)
else ();
val _ = map (check 0) args;