--- a/doc-src/Classes/Thy/document/Classes.tex Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Thu Apr 02 13:41:31 2009 +0200
@@ -1191,7 +1191,7 @@
\hspace*{0pt}\\
\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
-\hspace*{0pt}pow{\char95}nat (Suc n) xa = mult xa (pow{\char95}nat n xa);\\
+\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
\hspace*{0pt}\\
\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
\hspace*{0pt}pow{\char95}int k x =\\
@@ -1272,8 +1272,8 @@
\hspace*{0pt} ~IntInf.int group;\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
-\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) xa =\\
-\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) xa (pow{\char95}nat A{\char95}~n xa);\\
+\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
+\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
\hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
--- a/doc-src/Codegen/Thy/Adaption.thy Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/Thy/Adaption.thy Thu Apr 02 13:41:31 2009 +0200
@@ -59,42 +59,7 @@
supposed to be:
\begin{figure}[here]
- \begin{tikzpicture}[scale = 0.5]
- \tikzstyle water=[color = blue, thick]
- \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
- \tikzstyle process=[color = green, semithick, ->]
- \tikzstyle adaption=[color = red, semithick, ->]
- \tikzstyle target=[color = black]
- \foreach \x in {0, ..., 24}
- \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
- + (0.25, -0.25) cos + (0.25, 0.25);
- \draw[style=ice] (1, 0) --
- (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
- \draw[style=ice] (9, 0) --
- (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
- \draw[style=ice] (15, -6) --
- (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
- \draw[style=process]
- (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
- \draw[style=process]
- (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
- \node (adaption) at (11, -2) [style=adaption] {adaption};
- \node at (19, 3) [rotate=90] {generated};
- \node at (19.5, -5) {language};
- \node at (19.5, -3) {library};
- \node (includes) at (19.5, -1) {includes};
- \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
- \draw[style=process]
- (includes) -- (serialisation);
- \draw[style=process]
- (reserved) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (includes);
- \draw[style=adaption]
- (adaption) -- (reserved);
- \end{tikzpicture}
+ \includegraphics{Thy/pictures/adaption}
\caption{The adaption principle}
\label{fig:adaption}
\end{figure}
--- a/doc-src/Codegen/Thy/Introduction.thy Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Thu Apr 02 13:41:31 2009 +0200
@@ -121,29 +121,7 @@
how it works.
\begin{figure}[h]
- \begin{tikzpicture}[x = 4.2cm, y = 1cm]
- \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
- \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
- \tikzstyle process_arrow=[->, semithick, color = green];
- \node (HOL) at (0, 4) [style=entity] {@{text "Isabelle/HOL"} theory};
- \node (eqn) at (2, 2) [style=entity] {code equations};
- \node (iml) at (2, 0) [style=entity] {intermediate language};
- \node (seri) at (1, 0) [style=process] {serialisation};
- \node (SML) at (0, 3) [style=entity] {@{text SML}};
- \node (OCaml) at (0, 2) [style=entity] {@{text OCaml}};
- \node (further) at (0, 1) [style=entity] {@{text "\<dots>"}};
- \node (Haskell) at (0, 0) [style=entity] {@{text Haskell}};
- \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
- node [style=process, near start] {selection}
- node [style=process, near end] {preprocessing}
- (eqn);
- \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
- \draw [style=process_arrow] (iml) -- (seri);
- \draw [style=process_arrow] (seri) -- (SML);
- \draw [style=process_arrow] (seri) -- (OCaml);
- \draw [style=process_arrow, dashed] (seri) -- (further);
- \draw [style=process_arrow] (seri) -- (Haskell);
- \end{tikzpicture}
+ \includegraphics{Thy/pictures/architecture}
\caption{Code generator architecture}
\label{fig:arch}
\end{figure}
@@ -164,35 +142,29 @@
\begin{itemize}
- \item Out of the vast collection of theorems proven in a
- \qn{theory}, a reasonable subset modelling
- code equations is \qn{selected}.
-
- \item On those selected theorems, certain
- transformations are carried out
- (\qn{preprocessing}). Their purpose is to turn theorems
- representing non- or badly executable
- specifications into equivalent but executable counterparts.
- The result is a structured collection of \qn{code theorems}.
+ \item Starting point is a collection of raw code equations in a
+ theory; due to proof irrelevance it is not relevant where they
+ stem from but typically they are either descendant of specification
+ tools or explicit proofs by the user.
+
+ \item Before these raw code equations are continued
+ with, they can be subjected to theorem transformations. This
+ \qn{preprocessor} is an interface which allows to apply the full
+ expressiveness of ML-based theorem transformations to code
+ generation. The result of the preprocessing step is a
+ structured collection of code equations.
- \item Before the selected code equations are continued with,
- they can be \qn{preprocessed}, i.e. subjected to theorem
- transformations. This \qn{preprocessor} is an interface which
- allows to apply
- the full expressiveness of ML-based theorem transformations
- to code generation; motivating examples are shown below, see
- \secref{sec:preproc}.
- The result of the preprocessing step is a structured collection
- of code equations.
-
- \item These code equations are \qn{translated} to a program
- in an abstract intermediate language. Think of it as a kind
+ \item These code equations are \qn{translated} to a program in an
+ abstract intermediate language. Think of it as a kind
of \qt{Mini-Haskell} with four \qn{statements}: @{text data}
(for datatypes), @{text fun} (stemming from code equations),
also @{text class} and @{text inst} (for type classes).
\item Finally, the abstract program is \qn{serialised} into concrete
source code of a target language.
+ This step only produces concrete syntax but does not change the
+ program in essence; all conceptual transformations occur in the
+ translation step.
\end{itemize}
--- a/doc-src/Codegen/Thy/document/Adaption.tex Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Adaption.tex Thu Apr 02 13:41:31 2009 +0200
@@ -96,42 +96,7 @@
supposed to be:
\begin{figure}[here]
- \begin{tikzpicture}[scale = 0.5]
- \tikzstyle water=[color = blue, thick]
- \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
- \tikzstyle process=[color = green, semithick, ->]
- \tikzstyle adaption=[color = red, semithick, ->]
- \tikzstyle target=[color = black]
- \foreach \x in {0, ..., 24}
- \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
- + (0.25, -0.25) cos + (0.25, 0.25);
- \draw[style=ice] (1, 0) --
- (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
- \draw[style=ice] (9, 0) --
- (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
- \draw[style=ice] (15, -6) --
- (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
- \draw[style=process]
- (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
- \draw[style=process]
- (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
- \node (adaption) at (11, -2) [style=adaption] {adaption};
- \node at (19, 3) [rotate=90] {generated};
- \node at (19.5, -5) {language};
- \node at (19.5, -3) {library};
- \node (includes) at (19.5, -1) {includes};
- \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
- \draw[style=process]
- (includes) -- (serialisation);
- \draw[style=process]
- (reserved) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (includes);
- \draw[style=adaption]
- (adaption) -- (reserved);
- \end{tikzpicture}
+ \includegraphics{Thy/pictures/adaption}
\caption{The adaption principle}
\label{fig:adaption}
\end{figure}
--- a/doc-src/Codegen/Thy/document/Introduction.tex Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Thu Apr 02 13:41:31 2009 +0200
@@ -284,29 +284,7 @@
how it works.
\begin{figure}[h]
- \begin{tikzpicture}[x = 4.2cm, y = 1cm]
- \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
- \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
- \tikzstyle process_arrow=[->, semithick, color = green];
- \node (HOL) at (0, 4) [style=entity] {\isa{Isabelle{\isacharslash}HOL} theory};
- \node (eqn) at (2, 2) [style=entity] {code equations};
- \node (iml) at (2, 0) [style=entity] {intermediate language};
- \node (seri) at (1, 0) [style=process] {serialisation};
- \node (SML) at (0, 3) [style=entity] {\isa{SML}};
- \node (OCaml) at (0, 2) [style=entity] {\isa{OCaml}};
- \node (further) at (0, 1) [style=entity] {\isa{{\isasymdots}}};
- \node (Haskell) at (0, 0) [style=entity] {\isa{Haskell}};
- \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
- node [style=process, near start] {selection}
- node [style=process, near end] {preprocessing}
- (eqn);
- \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
- \draw [style=process_arrow] (iml) -- (seri);
- \draw [style=process_arrow] (seri) -- (SML);
- \draw [style=process_arrow] (seri) -- (OCaml);
- \draw [style=process_arrow, dashed] (seri) -- (further);
- \draw [style=process_arrow] (seri) -- (Haskell);
- \end{tikzpicture}
+ \includegraphics{Thy/pictures/architecture}
\caption{Code generator architecture}
\label{fig:arch}
\end{figure}
@@ -327,35 +305,29 @@
\begin{itemize}
- \item Out of the vast collection of theorems proven in a
- \qn{theory}, a reasonable subset modelling
- code equations is \qn{selected}.
-
- \item On those selected theorems, certain
- transformations are carried out
- (\qn{preprocessing}). Their purpose is to turn theorems
- representing non- or badly executable
- specifications into equivalent but executable counterparts.
- The result is a structured collection of \qn{code theorems}.
+ \item Starting point is a collection of raw code equations in a
+ theory; due to proof irrelevance it is not relevant where they
+ stem from but typically they are either descendant of specification
+ tools or explicit proofs by the user.
+
+ \item Before these raw code equations are continued
+ with, they can be subjected to theorem transformations. This
+ \qn{preprocessor} is an interface which allows to apply the full
+ expressiveness of ML-based theorem transformations to code
+ generation. The result of the preprocessing step is a
+ structured collection of code equations.
- \item Before the selected code equations are continued with,
- they can be \qn{preprocessed}, i.e. subjected to theorem
- transformations. This \qn{preprocessor} is an interface which
- allows to apply
- the full expressiveness of ML-based theorem transformations
- to code generation; motivating examples are shown below, see
- \secref{sec:preproc}.
- The result of the preprocessing step is a structured collection
- of code equations.
-
- \item These code equations are \qn{translated} to a program
- in an abstract intermediate language. Think of it as a kind
+ \item These code equations are \qn{translated} to a program in an
+ abstract intermediate language. Think of it as a kind
of \qt{Mini-Haskell} with four \qn{statements}: \isa{data}
(for datatypes), \isa{fun} (stemming from code equations),
also \isa{class} and \isa{inst} (for type classes).
\item Finally, the abstract program is \qn{serialised} into concrete
source code of a target language.
+ This step only produces concrete syntax but does not change the
+ program in essence; all conceptual transformations occur in the
+ translation step.
\end{itemize}
--- a/doc-src/Codegen/Thy/pictures/adaption.tex Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/Thy/pictures/adaption.tex Thu Apr 02 13:41:31 2009 +0200
@@ -1,7 +1,5 @@
\documentclass[12pt]{article}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
\usepackage{tikz}
\begin{document}
@@ -10,7 +8,7 @@
\setlength{\fboxrule}{0.01pt}
\setlength{\fboxsep}{4pt}
-\fbox{
+\fcolorbox{white}{white}{
\begin{tikzpicture}[scale = 0.5]
\tikzstyle water=[color = blue, thick]
--- a/doc-src/Codegen/Thy/pictures/architecture.tex Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/Thy/pictures/architecture.tex Thu Apr 02 13:41:31 2009 +0200
@@ -1,8 +1,8 @@
\documentclass[12pt]{article}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
\usepackage{tikz}
+\usetikzlibrary{shapes}
+\usetikzlibrary{arrows}
\begin{document}
@@ -10,30 +10,39 @@
\setlength{\fboxrule}{0.01pt}
\setlength{\fboxsep}{4pt}
-\fbox{
+\fcolorbox{white}{white}{
+
+\newcommand{\sys}[1]{\emph{#1}}
-\begin{tikzpicture}[x = 4.2cm, y = 1cm]
- \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
- \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
- \tikzstyle process_arrow=[->, semithick, color = green];
- \node (HOL) at (0, 4) [style=entity] {Isabelle/HOL theory};
- \node (eqn) at (2, 2) [style=entity] {code equations};
- \node (iml) at (2, 0) [style=entity] {intermediate language};
- \node (seri) at (1, 0) [style=process] {serialisation};
- \node (SML) at (0, 3) [style=entity] {SML};
- \node (OCaml) at (0, 2) [style=entity] {OCaml};
- \node (further) at (0, 1) [style=entity] {\ldots};
- \node (Haskell) at (0, 0) [style=entity] {Haskell};
- \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
- node [style=process, near start] {selection}
- node [style=process, near end] {preprocessing}
- (eqn);
- \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
- \draw [style=process_arrow] (iml) -- (seri);
- \draw [style=process_arrow] (seri) -- (SML);
- \draw [style=process_arrow] (seri) -- (OCaml);
- \draw [style=process_arrow, dashed] (seri) -- (further);
- \draw [style=process_arrow] (seri) -- (Haskell);
+\begin{tikzpicture}[x = 4cm, y = 1cm]
+ \tikzstyle positive=[color = black, fill = white];
+ \tikzstyle negative=[color = white, fill = black];
+ \tikzstyle entity=[rounded corners, draw, thick];
+ \tikzstyle process=[ellipse, draw, thick];
+ \tikzstyle arrow=[-stealth, semithick];
+ \node (spec) at (0, 3) [entity, positive] {specification tools};
+ \node (user) at (1, 3) [entity, positive] {user proofs};
+ \node (spec_user_join) at (0.5, 3) [shape=coordinate] {};
+ \node (raw) at (0.5, 4) [entity, positive] {raw code equations};
+ \node (pre) at (1.5, 4) [process, positive] {preprocessing};
+ \node (eqn) at (2.5, 4) [entity, positive] {code equations};
+ \node (iml) at (0.5, 0) [entity, positive] {intermediate program};
+ \node (seri) at (1.5, 0) [process, positive] {serialisation};
+ \node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
+ \node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
+ \node (further) at (2.5, 1) [entity, positive] {(\ldots)};
+ \node (Haskell) at (2.5, 0) [entity, positive] {\sys{Haskell}};
+ \draw [semithick] (spec) -- (spec_user_join);
+ \draw [semithick] (user) -- (spec_user_join);
+ \draw [-diamond, semithick] (spec_user_join) -- (raw);
+ \draw [arrow] (raw) -- (pre);
+ \draw [arrow] (pre) -- (eqn);
+ \draw [arrow] (eqn) -- node (transl) [process, positive] {translation} (iml);
+ \draw [arrow] (iml) -- (seri);
+ \draw [arrow] (seri) -- (SML);
+ \draw [arrow] (seri) -- (OCaml);
+ \draw [arrow, dashed] (seri) -- (further);
+ \draw [arrow] (seri) -- (Haskell);
\end{tikzpicture}
}
--- a/doc-src/Codegen/codegen.tex Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/codegen.tex Thu Apr 02 13:41:31 2009 +0200
@@ -5,9 +5,6 @@
\usepackage{../iman,../extra,../isar,../proof}
\usepackage{../isabelle,../isabellesym}
\usepackage{style}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
-\usepackage{tikz}
\usepackage{../pdfsetup}
\hyphenation{Isabelle}
--- a/src/HOL/Divides.thy Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Divides.thy Thu Apr 02 13:41:31 2009 +0200
@@ -238,6 +238,10 @@
by (simp only: mod_add_eq [symmetric])
qed
+lemma div_add[simp]: "z dvd x \<Longrightarrow> z dvd y
+ \<Longrightarrow> (x + y) div z = x div z + y div z"
+by(cases "z=0", simp, unfold dvd_def, auto simp add: algebra_simps)
+
text {* Multiplication respects modular equivalence. *}
lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
@@ -765,7 +769,7 @@
(* Monotonicity of div in first argument *)
-lemma div_le_mono [rule_format (no_asm)]:
+lemma div_le_mono [rule_format]:
"\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
apply (case_tac "k=0", simp)
apply (induct "n" rule: nat_less_induct, clarify)
@@ -820,6 +824,12 @@
apply (simp_all)
done
+lemma nat_div_eq_0 [simp]: "(n::nat) > 0 ==> ((m div n) = 0) = (m < n)"
+by(auto, subst mod_div_equality [of m n, symmetric], auto)
+
+lemma nat_div_gt_0 [simp]: "(n::nat) > 0 ==> ((m div n) > 0) = (m >= n)"
+by (subst neq0_conv [symmetric], auto)
+
declare div_less_dividend [simp]
text{*A fact for the mutilated chess board*}
@@ -905,13 +915,10 @@
done
lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
- apply (unfold dvd_def, clarify)
- apply (simp_all (no_asm_use) add: zero_less_mult_iff)
- apply (erule conjE)
- apply (rule le_trans)
- apply (rule_tac [2] le_refl [THEN mult_le_mono])
- apply (erule_tac [2] Suc_leI, simp)
- done
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+
+lemma nat_dvd_not_less: "(0::nat) < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
apply (subgoal_tac "m mod n = 0")
@@ -1148,9 +1155,4 @@
with j show ?thesis by blast
qed
-lemma nat_dvd_not_less:
- fixes m n :: nat
- shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
-by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
-
end
--- a/src/HOL/Finite_Set.thy Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Finite_Set.thy Thu Apr 02 13:41:31 2009 +0200
@@ -1084,10 +1084,8 @@
qed
lemma setsum_mono_zero_right:
- assumes fT: "finite T" and ST: "S \<subseteq> T"
- and z: "\<forall>i \<in> T - S. f i = 0"
- shows "setsum f T = setsum f S"
-using setsum_mono_zero_left[OF fT ST z] by simp
+ "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
+by(blast intro!: setsum_mono_zero_left[symmetric])
lemma setsum_mono_zero_cong_left:
assumes fT: "finite T" and ST: "S \<subseteq> T"
@@ -1645,7 +1643,7 @@
"A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
by(fastsimp simp: setprod_def intro: fold_image_cong)
-lemma strong_setprod_cong:
+lemma strong_setprod_cong[cong]:
"A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
@@ -1662,7 +1660,7 @@
then show ?thesis apply simp
apply (rule setprod_cong)
apply simp
- by (erule eq[symmetric])
+ by (simp add: eq)
qed
lemma setprod_Un_one:
@@ -1694,6 +1692,20 @@
==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
by (subst setprod_Un_Int [symmetric], auto)
+lemma setprod_mono_one_left:
+ assumes fT: "finite T" and ST: "S \<subseteq> T"
+ and z: "\<forall>i \<in> T - S. f i = 1"
+ shows "setprod f S = setprod f T"
+proof-
+ have eq: "T = S \<union> (T - S)" using ST by blast
+ have d: "S \<inter> (T - S) = {}" using ST by blast
+ from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
+ show ?thesis
+ by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
+qed
+
+lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
+
lemma setprod_delta:
assumes fS: "finite S"
shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
@@ -1776,49 +1788,26 @@
done
lemma setprod_nonneg [rule_format]:
- "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
-apply (case_tac "finite A")
-apply (induct set: finite, force, clarsimp)
-apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
-apply (rule mult_mono, assumption+)
-apply (auto simp add: setprod_def)
-done
-
-lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
+ "(ALL x: A. (0::'a::ordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
+by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
+
+lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_semidom) < f x)
--> 0 < setprod f A"
-apply (case_tac "finite A")
-apply (induct set: finite, force, clarsimp)
-apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
-apply (rule mult_strict_mono, assumption+)
-apply (auto simp add: setprod_def)
-done
-
-lemma setprod_nonzero [rule_format]:
- "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
- finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
-by (erule finite_induct, auto)
-
-lemma setprod_zero_eq:
- "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
- finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
-by (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
-
-lemma setprod_nonzero_field:
- "finite A ==> (ALL x: A. f x \<noteq> (0::'a::idom)) ==> setprod f A \<noteq> 0"
-by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_field:
- "finite A ==> (setprod f A = (0::'a::idom)) = (EX x: A. f x = 0)"
-by (rule setprod_zero_eq, auto)
+by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
+
+lemma setprod_zero_iff[simp]: "finite A ==>
+ (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
+ (EX x: A. f x = 0)"
+by (erule finite_induct, auto simp:no_zero_divisors)
+
+lemma setprod_pos_nat:
+ "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
+using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
(setprod f (A Un B) :: 'a ::{field})
= setprod f A * setprod f B / setprod f (A Int B)"
-apply (subst setprod_Un_Int [symmetric], auto)
-apply (subgoal_tac "finite (A Int B)")
-apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
-apply (subst times_divide_eq_right [THEN sym], auto)
-done
+by (subst setprod_Un_Int [symmetric], auto)
lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
(setprod f (A - {a}) :: 'a :: {field}) =
--- a/src/HOL/Int.thy Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Int.thy Thu Apr 02 13:41:31 2009 +0200
@@ -1382,8 +1382,6 @@
subsection {* @{term setsum} and @{term setprod} *}
-text {*By Jeremy Avigad*}
-
lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
apply (cases "finite A")
apply (erule finite_induct, auto)
@@ -1404,22 +1402,6 @@
apply (erule finite_induct, auto)
done
-lemma setprod_nonzero_nat:
- "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
- by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_nat:
- "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
- by (rule setprod_zero_eq, auto)
-
-lemma setprod_nonzero_int:
- "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
- by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_int:
- "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
- by (rule setprod_zero_eq, auto)
-
lemmas int_setsum = of_nat_setsum [where 'a=int]
lemmas int_setprod = of_nat_setprod [where 'a=int]
--- a/src/HOL/Library/Binomial.thy Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Library/Binomial.thy Thu Apr 02 13:41:31 2009 +0200
@@ -267,8 +267,6 @@
moreover
{assume n0: "n \<noteq> 0"
then have ?thesis apply (simp add: h pochhammer_Suc_setprod)
- apply (rule iffD2[OF setprod_zero_eq])
- apply auto
apply (rule_tac x="n" in bexI)
using h kn by auto}
ultimately show ?thesis by blast
@@ -281,8 +279,7 @@
moreover
{fix h assume h: "k = Suc h"
then have ?thesis apply (simp add: pochhammer_Suc_setprod)
- apply (subst setprod_zero_eq_field)
- using h kn by (auto simp add: ring_simps)}
+ using h kn by (auto simp add: algebra_simps)}
ultimately show ?thesis by (cases k, auto)
qed
@@ -299,15 +296,14 @@
where "a gchoose n = (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
lemma gbinomial_0[simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
- apply (simp_all add: gbinomial_def)
- apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
- apply simp
- apply (rule iffD2[OF setprod_zero_eq])
- by auto
+apply (simp_all add: gbinomial_def)
+apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
+ apply (simp del:setprod_zero_iff)
+apply simp
+done
lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)"
proof-
-
{assume "n=0" then have ?thesis by simp}
moreover
{assume n0: "n\<noteq>0"
@@ -388,7 +384,6 @@
unfolding mult_assoc[symmetric]
unfolding setprod_timesf[symmetric]
apply simp
- apply (rule disjI2)
apply (rule strong_setprod_reindex_cong[where f= "op - n"])
apply (auto simp add: inj_on_def image_iff Bex_def)
apply presburger
--- a/src/HOL/Library/Determinants.thy Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Library/Determinants.thy Thu Apr 02 13:41:31 2009 +0200
@@ -106,7 +106,7 @@
moreover
{assume fS: "finite S"
then have ?thesis
- apply (simp add: setprod_def)
+ apply (simp add: setprod_def cong del:strong_setprod_cong)
apply (rule ab_semigroup_mult.fold_image_permute)
apply (auto simp add: p)
apply unfold_locales
@@ -115,7 +115,7 @@
qed
lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}"
- by (auto intro: setprod_permute)
+ by (blast intro!: setprod_permute)
(* ------------------------------------------------------------------------- *)
(* Basic determinant properties. *)
@@ -310,10 +310,7 @@
using r
apply (simp add: row_def det_def Cart_eq)
apply (rule setsum_0')
-apply (clarsimp simp add: sign_nz)
-apply (rule setprod_zero)
-apply simp
-apply auto
+apply (auto simp: sign_nz)
done
lemma det_zero_column:
--- a/src/HOL/Library/Formal_Power_Series.thy Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Thu Apr 02 13:41:31 2009 +0200
@@ -1289,10 +1289,6 @@
apply auto
unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0, unfolded k]
apply (clarsimp simp add: natpermute_def nth_append)
- apply (rule_tac f="\<lambda>x. x * a (Suc k) $ (n - foldl op + 0 aa)" in cong[OF refl])
- apply (rule setprod_cong)
- apply simp
- apply simp
done
finally have "?P m n" .}
ultimately show "?P m n " by (cases m, auto)
@@ -1321,9 +1317,7 @@
{fix n assume m: "m = Suc n"
have c: "m = card {0..n}" using m by simp
have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}"
- apply (simp add: m fps_power_nth del: replicate.simps power_Suc)
- apply (rule setprod_cong)
- by (simp_all del: replicate.simps)
+ by (simp add: m fps_power_nth del: replicate.simps power_Suc)
also have "\<dots> = (a$0) ^ m"
unfolding c by (rule setprod_constant, simp)
finally have ?thesis .}
--- a/src/HOL/NumberTheory/Gauss.thy Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy Thu Apr 02 13:41:31 2009 +0200
@@ -290,7 +290,7 @@
using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
- using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime)
+by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
subsection {* Relationships Between Gauss Sets *}
@@ -416,8 +416,8 @@
then have one:
"[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
apply simp
- apply (insert p_g_0 finite_E)
- by (auto simp add: StandardRes_prod)
+ apply (insert p_g_0 finite_E StandardRes_prod)
+ by (auto)
moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
apply clarify
apply (insert zcong_id [of p])
@@ -435,10 +435,9 @@
ultimately have c:
"[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
apply simp
- apply (insert finite_E p_g_0)
- apply (rule setprod_same_function_zcong
- [of E "StandardRes p o (op - p)" uminus p], auto)
- done
+ using finite_E p_g_0
+ setprod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
+ by auto
then have two: "[setprod id F = setprod (uminus) E](mod p)"
apply (insert one c)
apply (rule zcong_trans [of "setprod id F"
@@ -463,11 +462,11 @@
"[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
proof -
have "[setprod id A = setprod id F * setprod id D](mod p)"
- by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
+ by (auto simp add: prod_D_F_eq_prod_A zmult_commute cong del:setprod_cong)
then have "[setprod id A = ((-1)^(card E) * setprod id E) *
setprod id D] (mod p)"
apply (rule zcong_trans)
- apply (auto simp add: prod_F_zcong zcong_scalar)
+ apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod_cong)
done
then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
apply (rule zcong_trans)
@@ -476,14 +475,14 @@
done
then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
apply (rule zcong_trans)
- apply (simp add: C_B_zcong_prod zcong_scalar2)
+ apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod_cong)
done
then have "[setprod id A = ((-1)^(card E) *
(setprod id ((%x. x * a) ` A)))] (mod p)"
by (simp add: B_def)
then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
(mod p)"
- by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
+ by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong)
moreover have "setprod (%x. x * a) A =
setprod (%x. a) A * setprod id A"
using finite_A by (induct set: finite) auto
@@ -506,7 +505,7 @@
then have "[setprod id A * (-1)^(card E) = setprod id A *
a^(card A)](mod p)"
apply (rule zcong_trans)
- apply (simp add: aux)
+ apply (simp add: aux cong del:setprod_cong)
done
with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
--- a/src/HOL/Tools/atp_manager.ML Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML Thu Apr 02 13:41:31 2009 +0200
@@ -85,36 +85,25 @@
(* state of thread manager *)
datatype T = State of
- {timeout_heap: ThreadHeap.T,
+ {managing_thread: Thread.thread option,
+ timeout_heap: ThreadHeap.T,
oldest_heap: ThreadHeap.T,
active: (Thread.thread * (Time.time * Time.time * string)) list,
cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
messages: string list,
store: string list};
-fun make_state timeout_heap oldest_heap active cancelling messages store =
- State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
+fun make_state managing_thread timeout_heap oldest_heap active cancelling messages store =
+ State {managing_thread = managing_thread, timeout_heap = timeout_heap, oldest_heap = oldest_heap,
active = active, cancelling = cancelling, messages = messages, store = store};
-fun empty_state state =
- let
- val State {active = active, cancelling = cancelling, messages = messages, ...} =
- Synchronized.value state
- in (null active) andalso (null cancelling) andalso (null messages) end;
-
-val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] [] []);
-
-
-(* the managing thread *)
-
-(*watches over running threads and interrupts them if required*)
-val managing_thread = ref (NONE: Thread.thread option);
-
+val state = Synchronized.var "atp_manager"
+ (make_state NONE ThreadHeap.empty ThreadHeap.empty [] [] [] []);
(* unregister thread *)
fun unregister (success, message) thread = Synchronized.change state
- (fn state as State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
(case lookup_thread active thread of
SOME (birthtime, _, description) =>
let
@@ -132,7 +121,9 @@
val store' = message' ::
(if length store <= message_store_limit then store
else #1 (chop message_store_limit store))
- in make_state timeout_heap oldest_heap active' cancelling' (message' :: messages) store' end
+ in make_state
+ managing_thread timeout_heap oldest_heap active' cancelling' (message' :: messages) store'
+ end
| NONE => state));
@@ -147,12 +138,13 @@
fun kill_oldest () =
let exception Unchanged in
Synchronized.change_result state
- (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
then raise Unchanged
else
let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
- in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages store) end)
+ in (oldest_thread,
+ make_state managing_thread timeout_heap oldest_heap' active cancelling messages store) end)
|> unregister (false, "Interrupted (maximum number of ATPs exceeded)")
handle Unchanged => ()
end;
@@ -167,8 +159,8 @@
fun print_new_messages () =
let val to_print = Synchronized.change_result state
- (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
- (messages, make_state timeout_heap oldest_heap active cancelling [] store))
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (messages, make_state managing_thread timeout_heap oldest_heap active cancelling [] store))
in
if null to_print then ()
else priority ("Sledgehammer: " ^ space_implode "\n\n" to_print)
@@ -177,55 +169,66 @@
(* start a watching thread -- only one may exist *)
-fun check_thread_manager () = CRITICAL (fn () =>
- if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false)
- then () else managing_thread := SOME (SimpleThread.fork false (fn () =>
- let
- val min_wait_time = Time.fromMilliseconds 300
- val max_wait_time = Time.fromSeconds 10
+fun check_thread_manager () = Synchronized.change state
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ if (case managing_thread of SOME thread => Thread.isActive thread | NONE => false)
+ then make_state managing_thread timeout_heap oldest_heap active cancelling messages store
+ else let val managing_thread = SOME (SimpleThread.fork false (fn () =>
+ let
+ val min_wait_time = Time.fromMilliseconds 300
+ val max_wait_time = Time.fromSeconds 10
- (* wait for next thread to cancel, or maximum*)
- fun time_limit (State {timeout_heap, ...}) =
- (case try ThreadHeap.min timeout_heap of
- NONE => SOME (Time.+ (Time.now (), max_wait_time))
- | SOME (time, _) => SOME time)
+ (* wait for next thread to cancel, or maximum*)
+ fun time_limit (State {timeout_heap, ...}) =
+ (case try ThreadHeap.min timeout_heap of
+ NONE => SOME (Time.+ (Time.now (), max_wait_time))
+ | SOME (time, _) => SOME time)
- (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
- fun action (State {timeout_heap, oldest_heap, active, cancelling, messages, store}) =
- let val (timeout_threads, timeout_heap') =
- ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
- in
- if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
- then NONE
- else
- let
- val _ = List.app (SimpleThread.interrupt o #1) cancelling
- val cancelling' = filter (Thread.isActive o #1) cancelling
- val state' = make_state timeout_heap' oldest_heap active cancelling' messages store
- in SOME (map #2 timeout_threads, state') end
- end
- in
- while not (empty_state state) do
- (Synchronized.timed_access state time_limit action
- |> these
- |> List.app (unregister (false, "Interrupted (reached timeout)"));
- kill_excessive ();
- print_new_messages ();
- (*give threads time to respond to interrupt*)
- OS.Process.sleep min_wait_time)
- end)));
+ (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
+ fun action (State {managing_thread, timeout_heap, oldest_heap, active, cancelling,
+ messages, store}) =
+ let val (timeout_threads, timeout_heap') =
+ ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
+ in
+ if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
+ then NONE
+ else
+ let
+ val _ = List.app (SimpleThread.interrupt o #1) cancelling
+ val cancelling' = filter (Thread.isActive o #1) cancelling
+ val state' = make_state
+ managing_thread timeout_heap' oldest_heap active cancelling' messages store
+ in SOME (map #2 timeout_threads, state') end
+ end
+ in
+ while Synchronized.change_result state
+ (fn st as
+ State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ if (null active) andalso (null cancelling) andalso (null messages)
+ then (false, make_state NONE timeout_heap oldest_heap active cancelling messages store)
+ else (true, st))
+ do
+ (Synchronized.timed_access state time_limit action
+ |> these
+ |> List.app (unregister (false, "Interrupted (reached timeout)"));
+ kill_excessive ();
+ print_new_messages ();
+ (*give threads time to respond to interrupt*)
+ OS.Process.sleep min_wait_time)
+ end))
+ in make_state managing_thread timeout_heap oldest_heap active cancelling messages store end);
(* thread is registered here by sledgehammer *)
fun register birthtime deadtime (thread, desc) =
(Synchronized.change state
- (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
let
val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
val active' = update_thread (thread, (birthtime, deadtime, desc)) active
- in make_state timeout_heap' oldest_heap' active' cancelling messages store end);
+ in make_state managing_thread timeout_heap' oldest_heap' active' cancelling messages store end);
check_thread_manager ());
@@ -235,9 +238,11 @@
(* kill: move all threads to cancelling *)
fun kill () = Synchronized.change state
- (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
- in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store end);
+ in make_state
+ managing_thread timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store
+ end);
(* ATP info *)
--- a/src/HOL/Tools/function_package/fundef_common.ML Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Thu Apr 02 13:41:31 2009 +0200
@@ -246,6 +246,8 @@
("Head symbol of left hand side must be "
^ plural "" "one out of " fnames ^ commas_quote fnames)
+ val _ = length args > 0 orelse input_error "Function has no arguments:"
+
fun add_bvs t is = add_loose_bnos (t, 0, is)
val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
|> map (fst o nth (rev qs))
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Thu Apr 02 13:41:31 2009 +0200
@@ -610,7 +610,7 @@
|> (snd o PureThy.add_thmss [
((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]),
((Binding.name "exhaust" , [exhaust] ), []),
- ((Binding.name "casedist" , [casedist]), [Induct.cases_type (Long_Name.base_name dname)]),
+ ((Binding.name "casedist" , [casedist]), [Induct.cases_type dname]),
((Binding.name "when_rews", when_rews ), [Simplifier.simp_add]),
((Binding.name "compacts", con_compacts), [Simplifier.simp_add]),
((Binding.name "con_rews", con_rews), [Simplifier.simp_add]),
@@ -999,6 +999,9 @@
in pg [] goal (K tacs) end;
end; (* local *)
+val inducts = ProjectRule.projections (ProofContext.init thy) ind;
+fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
+
in thy |> Sign.add_path comp_dnam
|> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
("take_rews" , take_rews ),
@@ -1007,6 +1010,7 @@
("finite_ind", [finite_ind]),
("ind" , [ind ]),
("coind" , [coind ])])))
+ |> (snd o (PureThy.add_thmss (map ind_rule (dnames ~~ inducts))))
|> Sign.parent_path |> pair take_rews
end; (* let *)
end; (* local *)
--- a/src/Pure/README Thu Apr 02 13:41:02 2009 +0200
+++ b/src/Pure/README Thu Apr 02 13:41:31 2009 +0200
@@ -15,7 +15,6 @@
Now the Pure session may be compiled interactively as follows:
- isabelle-process -u RAW
+ isabelle tty -l RAW
+ use "ROOT.ML";
-See ROOT.ML for further information.
-
--- a/src/Pure/ROOT.ML Thu Apr 02 13:41:02 2009 +0200
+++ b/src/Pure/ROOT.ML Thu Apr 02 13:41:31 2009 +0200
@@ -1,7 +1,4 @@
-(* Title: Pure/ROOT.ML
-
-Pure Isabelle.
-*)
+(* Pure Isabelle *)
structure Distribution = (*filled-in by makedist*)
struct