--- a/doc-src/Classes/Thy/Classes.thy Wed May 27 20:35:16 2009 +0200
+++ b/doc-src/Classes/Thy/Classes.thy Wed May 27 21:08:47 2009 +0200
@@ -485,14 +485,23 @@
qed
qed intro_locales
+text {*
+ \noindent This pattern is also helpful to reuse abstract
+ specifications on the \emph{same} type. For example, think of a
+ class @{text preorder}; for type @{typ nat}, there are at least two
+ possible instances: the natural order or the order induced by the
+ divides relation. But only one of these instances can be used for
+ @{command instantiation}; using the locale behind the class @{text
+ preorder}, it is still possible to utilise the same abstract
+ specification again using @{command interpretation}.
+*}
subsection {* Additional subclass relations *}
text {*
- Any @{text "group"} is also a @{text "monoid"}; this
- can be made explicit by claiming an additional
- subclass relation,
- together with a proof of the logical difference:
+ Any @{text "group"} is also a @{text "monoid"}; this can be made
+ explicit by claiming an additional subclass relation, together with
+ a proof of the logical difference:
*}
subclass %quote (in group) monoid
@@ -559,7 +568,7 @@
subsection {* A note on syntax *}
text {*
- As a commodity, class context syntax allows to refer
+ As a convenience, class context syntax allows to refer
to local class operations and their global counterparts
uniformly; type inference resolves ambiguities. For example:
*}
--- a/doc-src/Classes/Thy/document/Classes.tex Wed May 27 20:35:16 2009 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Wed May 27 21:08:47 2009 +0200
@@ -922,15 +922,25 @@
%
\endisadelimquote
%
+\begin{isamarkuptext}%
+\noindent This pattern is also helpful to reuse abstract
+ specifications on the \emph{same} type. For example, think of a
+ class \isa{preorder}; for type \isa{nat}, there are at least two
+ possible instances: the natural order or the order induced by the
+ divides relation. But only one of these instances can be used for
+ \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}; using the locale behind the class \isa{preorder}, it is still possible to utilise the same abstract
+ specification again using \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Additional subclass relations%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Any \isa{group} is also a \isa{monoid}; this
- can be made explicit by claiming an additional
- subclass relation,
- together with a proof of the logical difference:%
+Any \isa{group} is also a \isa{monoid}; this can be made
+ explicit by claiming an additional subclass relation, together with
+ a proof of the logical difference:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1038,7 +1048,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-As a commodity, class context syntax allows to refer
+As a convenience, class context syntax allows to refer
to local class operations and their global counterparts
uniformly; type inference resolves ambiguities. For example:%
\end{isamarkuptext}%
--- a/doc-src/Classes/classes.tex Wed May 27 20:35:16 2009 +0200
+++ b/doc-src/Classes/classes.tex Wed May 27 21:08:47 2009 +0200
@@ -21,12 +21,11 @@
\maketitle
\begin{abstract}
- \noindent This tutorial introduces the look-and-feel of Isar type classes
- to the end-user; Isar type classes are a convenient mechanism
- for organizing specifications, overcoming some drawbacks
- of raw axiomatic type classes. Essentially, they combine
- an operational aspect (in the manner of Haskell) with
- a logical aspect, both managed uniformly.
+ \noindent This tutorial introduces the look-and-feel of
+ Isar type classes to the end-user. Isar type classes
+ are a convenient mechanism for organizing specifications.
+ Essentially, they combine an operational aspect (in the
+ manner of Haskell) with a logical aspect, both managed uniformly.
\end{abstract}
\thispagestyle{empty}\clearpage
--- a/doc-src/Codegen/Thy/Program.thy Wed May 27 20:35:16 2009 +0200
+++ b/doc-src/Codegen/Thy/Program.thy Wed May 27 21:08:47 2009 +0200
@@ -204,7 +204,7 @@
interface.
\noindent The current setup of the preprocessor may be inspected using
- the @{command print_codesetup} command.
+ the @{command print_codeproc} command.
@{command code_thms} provides a convenient
mechanism to inspect the impact of a preprocessor setup
on code equations.
--- a/doc-src/Codegen/Thy/document/Program.tex Wed May 27 20:35:16 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex Wed May 27 21:08:47 2009 +0200
@@ -486,7 +486,7 @@
interface.
\noindent The current setup of the preprocessor may be inspected using
- the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
+ the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command.
\hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
mechanism to inspect the impact of a preprocessor setup
on code equations.
--- a/doc-src/Functions/functions.tex Wed May 27 20:35:16 2009 +0200
+++ b/doc-src/Functions/functions.tex Wed May 27 21:08:47 2009 +0200
@@ -16,7 +16,6 @@
\newcommand{\isasymLOCALE}{\cmd{locale}}
\newcommand{\isasymINCLUDES}{\cmd{includes}}
\newcommand{\isasymDATATYPE}{\cmd{datatype}}
-\newcommand{\isasymAXCLASS}{\cmd{axclass}}
\newcommand{\isasymDEFINES}{\cmd{defines}}
\newcommand{\isasymNOTES}{\cmd{notes}}
\newcommand{\isasymCLASS}{\cmd{class}}
--- a/doc-src/IsarOverview/Isar/Calc.thy Wed May 27 20:35:16 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-theory Calc imports Main begin
-
-subsection{* Chains of equalities *}
-
-axclass
- group < zero, plus, minus
- assoc: "(x + y) + z = x + (y + z)"
- left_0: "0 + x = x"
- left_minus: "-x + x = 0"
-
-theorem right_minus: "x + -x = (0::'a::group)"
-proof -
- have "x + -x = (-(-x) + -x) + (x + -x)"
- by (simp only: left_0 left_minus)
- also have "... = -(-x) + ((-x + x) + -x)"
- by (simp only: group.assoc)
- also have "... = 0"
- by (simp only: left_0 left_minus)
- finally show ?thesis .
-qed
-
-subsection{* Inequalities and substitution *}
-
-lemmas distrib = zadd_zmult_distrib zadd_zmult_distrib2
- zdiff_zmult_distrib zdiff_zmult_distrib2
-declare numeral_2_eq_2[simp]
-
-
-lemma fixes a :: int shows "(a+b)\<twosuperior> \<le> 2*(a\<twosuperior> + b\<twosuperior>)"
-proof -
- have "(a+b)\<twosuperior> \<le> (a+b)\<twosuperior> + (a-b)\<twosuperior>" by simp
- also have "(a+b)\<twosuperior> \<le> a\<twosuperior> + b\<twosuperior> + 2*a*b" by(simp add:distrib)
- also have "(a-b)\<twosuperior> = a\<twosuperior> + b\<twosuperior> - 2*a*b" by(simp add:distrib)
- finally show ?thesis by simp
-qed
-
-
-subsection{* More transitivity *}
-
-lemma assumes R: "(a,b) \<in> R" "(b,c) \<in> R" "(c,d) \<in> R"
- shows "(a,d) \<in> R\<^sup>*"
-proof -
- have "(a,b) \<in> R\<^sup>*" ..
- also have "(b,c) \<in> R\<^sup>*" ..
- also have "(c,d) \<in> R\<^sup>*" ..
- finally show ?thesis .
-qed
-
-end
\ No newline at end of file
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed May 27 20:35:16 2009 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed May 27 21:08:47 2009 +0200
@@ -1065,6 +1065,7 @@
@{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{attribute_def (HOL) code} & : & @{text attribute} \\
\end{matharray}
@@ -1228,8 +1229,10 @@
preprocessing.
\item @{command (HOL) "print_codesetup"} gives an overview on
- selected code equations, code generator datatypes and
- preprocessor setup.
+ selected code equations and code generator datatypes.
+
+ \item @{command (HOL) "print_codeproc"} prints the setup
+ of the code generator preprocessor.
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed May 27 20:35:16 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed May 27 21:08:47 2009 +0200
@@ -1074,6 +1074,7 @@
\indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
\end{matharray}
@@ -1234,8 +1235,10 @@
preprocessing.
\item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
- selected code equations, code generator datatypes and
- preprocessor setup.
+ selected code equations and code generator datatypes.
+
+ \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup
+ of the code generator preprocessor.
\end{description}%
\end{isamarkuptext}%
--- a/doc-src/manual.bib Wed May 27 20:35:16 2009 +0200
+++ b/doc-src/manual.bib Wed May 27 21:08:47 2009 +0200
@@ -1344,14 +1344,6 @@
institution = {TU Munich},
note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
-@manual{isabelle-axclass,
- author = {Markus Wenzel},
- title = {Using Axiomatic Type Classes in {I}sabelle},
- institution = {TU Munich},
- year = 2000,
- note = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}}
-
-
@InProceedings{Wenzel:1999:TPHOL,
author = {Markus Wenzel},
title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
--- a/src/HOL/Integration.thy Wed May 27 20:35:16 2009 +0200
+++ b/src/HOL/Integration.thy Wed May 27 21:08:47 2009 +0200
@@ -11,301 +11,163 @@
text{*We follow John Harrison in formalizing the Gauge integral.*}
-definition
- --{*Partitions and tagged partitions etc.*}
-
- partition :: "[(real*real),nat => real] => bool" where
- [code del]: "partition = (%(a,b) D. D 0 = a &
- (\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
- (\<forall>n \<ge> N. D(n) = b)))"
-
-definition
- psize :: "(nat => real) => nat" where
- [code del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
- (\<forall>n \<ge> N. D(n) = D(N)))"
+subsection {* Gauges *}
definition
- tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where
- [code del]:"tpart = (%(a,b) (D,p). partition(a,b) D &
- (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))"
+ gauge :: "[real set, real => real] => bool" where
+ [code del]:"gauge E g = (\<forall>x\<in>E. 0 < g(x))"
+
+
+subsection {* Gauge-fine divisions *}
+
+inductive
+ fine :: "[real \<Rightarrow> real, real \<times> real, (real \<times> real \<times> real) list] \<Rightarrow> bool"
+for
+ \<delta> :: "real \<Rightarrow> real"
+where
+ fine_Nil:
+ "fine \<delta> (a, a) []"
+| fine_Cons:
+ "\<lbrakk>fine \<delta> (b, c) D; a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk>
+ \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
+
+lemmas fine_induct [induct set: fine] =
+ fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv, standard]
+
+lemma fine_single:
+ "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
+by (rule fine_Cons [OF fine_Nil])
+
+lemma fine_append:
+ "\<lbrakk>fine \<delta> (a, b) D; fine \<delta> (b, c) D'\<rbrakk> \<Longrightarrow> fine \<delta> (a, c) (D @ D')"
+by (induct set: fine, simp, simp add: fine_Cons)
+
+lemma fine_imp_le: "fine \<delta> (a, b) D \<Longrightarrow> a \<le> b"
+by (induct set: fine, simp_all)
+
+lemma nonempty_fine_imp_less: "\<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b"
+apply (induct set: fine, simp)
+apply (drule fine_imp_le, simp)
+done
+
+lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b"
+by (induct set: fine, simp_all)
+
+lemma fine_eq: "fine \<delta> (a, b) D \<Longrightarrow> a = b \<longleftrightarrow> D = []"
+apply (cases "D = []")
+apply (drule (1) empty_fine_imp_eq, simp)
+apply (drule (1) nonempty_fine_imp_less, simp)
+done
- --{*Gauges and gauge-fine divisions*}
+lemma mem_fine:
+ "\<lbrakk>fine \<delta> (a, b) D; (u, x, v) \<in> set D\<rbrakk> \<Longrightarrow> u < v \<and> u \<le> x \<and> x \<le> v"
+by (induct set: fine, simp, force)
+
+lemma mem_fine2: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> a \<le> u \<and> v \<le> b"
+apply (induct arbitrary: z u v set: fine, auto)
+apply (simp add: fine_imp_le)
+apply (erule order_trans [OF less_imp_le], simp)
+done
+
+lemma mem_fine3: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> v - u < \<delta> z"
+by (induct arbitrary: z u v set: fine) auto
+
+lemma BOLZANO:
+ fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
+ assumes 1: "a \<le> b"
+ assumes 2: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
+ assumes 3: "\<And>x. \<exists>d>0. \<forall>a b. a \<le> x & x \<le> b & (b-a) < d \<longrightarrow> P a b"
+ shows "P a b"
+apply (subgoal_tac "split P (a,b)", simp)
+apply (rule lemma_BOLZANO [OF _ _ 1])
+apply (clarify, erule (3) 2)
+apply (clarify, rule 3)
+done
-definition
- gauge :: "[real => bool, real => real] => bool" where
- [code del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))"
+text{*We can always find a division that is fine wrt any gauge*}
+
+lemma fine_exists:
+ assumes "a \<le> b" and "gauge {a..b} \<delta>" shows "\<exists>D. fine \<delta> (a, b) D"
+proof -
+ {
+ fix u v :: real assume "u \<le> v"
+ have "a \<le> u \<Longrightarrow> v \<le> b \<Longrightarrow> \<exists>D. fine \<delta> (u, v) D"
+ apply (induct u v rule: BOLZANO, rule `u \<le> v`)
+ apply (simp, fast intro: fine_append)
+ apply (case_tac "a \<le> x \<and> x \<le> b")
+ apply (rule_tac x="\<delta> x" in exI)
+ apply (rule conjI)
+ apply (simp add: `gauge {a..b} \<delta>` [unfolded gauge_def])
+ apply (clarify, rename_tac u v)
+ apply (case_tac "u = v")
+ apply (fast intro: fine_Nil)
+ apply (subgoal_tac "u < v", fast intro: fine_single, simp)
+ apply (rule_tac x="1" in exI, clarsimp)
+ done
+ }
+ with `a \<le> b` show ?thesis by auto
+qed
+
+
+subsection {* Riemann sum *}
definition
- fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where
- [code del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
+ rsum :: "[(real \<times> real \<times> real) list, real \<Rightarrow> real] \<Rightarrow> real" where
+ "rsum D f = (\<Sum>(u, x, v)\<leftarrow>D. f x * (v - u))"
+
+lemma rsum_Nil [simp]: "rsum [] f = 0"
+unfolding rsum_def by simp
- --{*Riemann sum*}
+lemma rsum_Cons [simp]: "rsum ((u, x, v) # D) f = f x * (v - u) + rsum D f"
+unfolding rsum_def by simp
+
+lemma rsum_zero [simp]: "rsum D (\<lambda>x. 0) = 0"
+by (induct D, auto)
-definition
- rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real" where
- "rsum = (%(D,p) f. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n) - D(n)))"
+lemma rsum_left_distrib: "rsum D f * c = rsum D (\<lambda>x. f x * c)"
+by (induct D, auto simp add: algebra_simps)
+
+lemma rsum_right_distrib: "c * rsum D f = rsum D (\<lambda>x. c * f x)"
+by (induct D, auto simp add: algebra_simps)
- --{*Gauge integrability (definite)*}
+lemma rsum_add: "rsum D (\<lambda>x. f x + g x) = rsum D f + rsum D g"
+by (induct D, auto simp add: algebra_simps)
+
+
+subsection {* Gauge integrability (definite) *}
definition
Integral :: "[(real*real),real=>real,real] => bool" where
[code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
- (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
- (\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
- \<bar>rsum(D,p) f - k\<bar> < e)))"
-
-
-lemma psize_unique:
- assumes 1: "\<forall>n < N. D(n) < D(Suc n)"
- assumes 2: "\<forall>n \<ge> N. D(n) = D(N)"
- shows "psize D = N"
-unfolding psize_def
-proof (rule some_equality)
- show "(\<forall>n<N. D(n) < D(Suc n)) \<and> (\<forall>n\<ge>N. D(n) = D(N))" using prems ..
-next
- fix M assume "(\<forall>n<M. D(n) < D(Suc n)) \<and> (\<forall>n\<ge>M. D(n) = D(M))"
- hence 3: "\<forall>n<M. D(n) < D(Suc n)" and 4: "\<forall>n\<ge>M. D(n) = D(M)" by fast+
- show "M = N"
- proof (rule linorder_cases)
- assume "M < N"
- hence "D(M) < D(Suc M)" by (rule 1 [rule_format])
- also have "D(Suc M) = D(M)" by (rule 4 [rule_format], simp)
- finally show "M = N" by simp
- next
- assume "N < M"
- hence "D(N) < D(Suc N)" by (rule 3 [rule_format])
- also have "D(Suc N) = D(N)" by (rule 2 [rule_format], simp)
- finally show "M = N" by simp
- next
- assume "M = N" thus "M = N" .
- qed
-qed
-
-lemma partition_zero [simp]: "a = b ==> psize (%n. if n = 0 then a else b) = 0"
-by (rule psize_unique, simp_all)
-
-lemma partition_one [simp]: "a < b ==> psize (%n. if n = 0 then a else b) = 1"
-by (rule psize_unique, simp_all)
-
-lemma partition_single [simp]:
- "a \<le> b ==> partition(a,b)(%n. if n = 0 then a else b)"
-by (auto simp add: partition_def order_le_less)
-
-lemma partition_lhs: "partition(a,b) D ==> (D(0) = a)"
-by (simp add: partition_def)
-
-lemma partition:
- "(partition(a,b) D) =
- ((D 0 = a) &
- (\<forall>n < psize D. D n < D(Suc n)) &
- (\<forall>n \<ge> psize D. D n = b))"
-apply (simp add: partition_def)
-apply (rule iffI, clarify)
-apply (subgoal_tac "psize D = N", simp)
-apply (rule psize_unique, assumption, simp)
-apply (simp, rule_tac x="psize D" in exI, simp)
-done
-
-lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)"
-by (simp add: partition)
-
-lemma partition_rhs2: "[|partition(a,b) D; psize D \<le> n |] ==> (D n = b)"
-by (simp add: partition)
-
-lemma lemma_partition_lt_gen [rule_format]:
- "partition(a,b) D & m + Suc d \<le> n & n \<le> (psize D) --> D(m) < D(m + Suc d)"
-apply (induct "d", auto simp add: partition)
-apply (blast dest: Suc_le_lessD intro: less_le_trans order_less_trans)
-done
-
-lemma less_eq_add_Suc: "m < n ==> \<exists>d. n = m + Suc d"
-by (auto simp add: less_iff_Suc_add)
-
-lemma partition_lt_gen:
- "[|partition(a,b) D; m < n; n \<le> (psize D)|] ==> D(m) < D(n)"
-by (auto dest: less_eq_add_Suc intro: lemma_partition_lt_gen)
-
-lemma partition_lt: "partition(a,b) D ==> n < (psize D) ==> D(0) < D(Suc n)"
-apply (induct "n")
-apply (auto simp add: partition)
-done
-
-lemma partition_le: "partition(a,b) D ==> a \<le> b"
-apply (frule partition [THEN iffD1], safe)
-apply (drule_tac x = "psize D" and P="%n. psize D \<le> n --> ?P n" in spec, safe)
-apply (case_tac "psize D = 0")
-apply (drule_tac [2] n = "psize D - Suc 0" in partition_lt, auto)
-done
-
-lemma partition_gt: "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)"
-by (auto intro: partition_lt_gen)
-
-lemma partition_eq: "partition(a,b) D ==> ((a = b) = (psize D = 0))"
-apply (frule partition [THEN iffD1], safe)
-apply (rotate_tac 2)
-apply (drule_tac x = "psize D" in spec)
-apply (rule ccontr)
-apply (drule_tac n = "psize D - Suc 0" in partition_lt)
-apply auto
-done
-
-lemma partition_lb: "partition(a,b) D ==> a \<le> D(r)"
-apply (frule partition [THEN iffD1], safe)
-apply (induct "r")
-apply (cut_tac [2] y = "Suc r" and x = "psize D" in linorder_le_less_linear)
-apply (auto intro: partition_le)
-apply (drule_tac x = r in spec)
-apply arith;
-done
+ (\<exists>\<delta>. gauge {a .. b} \<delta> &
+ (\<forall>D. fine \<delta> (a,b) D -->
+ \<bar>rsum D f - k\<bar> < e)))"
-lemma partition_lb_lt: "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)"
-apply (rule_tac t = a in partition_lhs [THEN subst], assumption)
-apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear)
-apply (frule partition [THEN iffD1], safe)
- apply (blast intro: partition_lt less_le_trans)
-apply (rotate_tac 3)
-apply (drule_tac x = "Suc n" in spec)
-apply (erule impE)
-apply (erule less_imp_le)
-apply (frule partition_rhs)
-apply (drule partition_gt[of _ _ _ 0], arith)
-apply (simp (no_asm_simp))
-done
-
-lemma partition_ub: "partition(a,b) D ==> D(r) \<le> b"
-apply (frule partition [THEN iffD1])
-apply (cut_tac x = "psize D" and y = r in linorder_le_less_linear, safe, blast)
-apply (subgoal_tac "\<forall>x. D ((psize D) - x) \<le> b")
-apply (rotate_tac 4)
-apply (drule_tac x = "psize D - r" in spec)
-apply (subgoal_tac "psize D - (psize D - r) = r")
-apply simp
-apply arith
-apply safe
-apply (induct_tac "x")
-apply (simp (no_asm), blast)
-apply (case_tac "psize D - Suc n = 0")
-apply (erule_tac V = "\<forall>n. psize D \<le> n --> D n = b" in thin_rl)
-apply (simp (no_asm_simp) add: partition_le)
-apply (rule order_trans)
- prefer 2 apply assumption
-apply (subgoal_tac "psize D - n = Suc (psize D - Suc n)")
- prefer 2 apply arith
-apply (drule_tac x = "psize D - Suc n" in spec, simp)
-done
-
-lemma partition_ub_lt: "[| partition(a,b) D; n < psize D |] ==> D(n) < b"
-by (blast intro: partition_rhs [THEN subst] partition_gt)
-
-lemma lemma_partition_append1:
- "[| partition (a, b) D1; partition (b, c) D2 |]
- ==> (\<forall>n < psize D1 + psize D2.
- (if n < psize D1 then D1 n else D2 (n - psize D1))
- < (if Suc n < psize D1 then D1 (Suc n)
- else D2 (Suc n - psize D1))) &
- (\<forall>n \<ge> psize D1 + psize D2.
- (if n < psize D1 then D1 n else D2 (n - psize D1)) =
- (if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2)
- else D2 (psize D1 + psize D2 - psize D1)))"
-apply (auto intro: partition_lt_gen)
-apply (subgoal_tac "psize D1 = Suc n")
-apply (auto intro!: partition_lt_gen simp add: partition_lhs partition_ub_lt)
-apply (auto intro!: partition_rhs2 simp add: partition_rhs
- split: nat_diff_split)
-done
-
-lemma lemma_psize1:
- "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |]
- ==> D1(N) < D2 (psize D2)"
-apply (rule_tac y = "D1 (psize D1)" in order_less_le_trans)
-apply (erule partition_gt)
-apply (auto simp add: partition_rhs partition_le)
-done
-
-lemma lemma_partition_append2:
- "[| partition (a, b) D1; partition (b, c) D2 |]
- ==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) =
- psize D1 + psize D2"
-apply (rule psize_unique)
-apply (erule (1) lemma_partition_append1 [THEN conjunct1])
-apply (erule (1) lemma_partition_append1 [THEN conjunct2])
-done
-
-lemma tpart_eq_lhs_rhs: "[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b"
-by (auto simp add: tpart_def partition_eq)
-
-lemma tpart_partition: "tpart(a,b) (D,p) ==> partition(a,b) D"
-by (simp add: tpart_def)
-
-lemma partition_append:
- "[| tpart(a,b) (D1,p1); fine(g) (D1,p1);
- tpart(b,c) (D2,p2); fine(g) (D2,p2) |]
- ==> \<exists>D p. tpart(a,c) (D,p) & fine(g) (D,p)"
-apply (rule_tac x = "%n. if n < psize D1 then D1 n else D2 (n - psize D1)"
- in exI)
-apply (rule_tac x = "%n. if n < psize D1 then p1 n else p2 (n - psize D1)"
- in exI)
-apply (case_tac "psize D1 = 0")
-apply (auto dest: tpart_eq_lhs_rhs)
- prefer 2
-apply (simp add: fine_def
- lemma_partition_append2 [OF tpart_partition tpart_partition])
- --{*But must not expand @{term fine} in other subgoals*}
-apply auto
-apply (subgoal_tac "psize D1 = Suc n")
- prefer 2 apply arith
-apply (drule tpart_partition [THEN partition_rhs])
-apply (drule tpart_partition [THEN partition_lhs])
-apply (auto split: nat_diff_split)
-apply (auto simp add: tpart_def)
-defer 1
- apply (subgoal_tac "psize D1 = Suc n")
- prefer 2 apply arith
- apply (drule partition_rhs)
- apply (drule partition_lhs, auto)
-apply (simp split: nat_diff_split)
-apply (subst partition)
-apply (subst (1 2) lemma_partition_append2, assumption+)
-apply (rule conjI)
-apply (simp add: partition_lhs)
-apply (drule lemma_partition_append1)
-apply assumption;
-apply (simp add: partition_rhs)
-done
-
-
-text{*We can always find a division that is fine wrt any gauge*}
-
-lemma partition_exists:
- "[| a \<le> b; gauge(%x. a \<le> x & x \<le> b) g |]
- ==> \<exists>D p. tpart(a,b) (D,p) & fine g (D,p)"
-apply (cut_tac P = "%(u,v). a \<le> u & v \<le> b -->
- (\<exists>D p. tpart (u,v) (D,p) & fine (g) (D,p))"
- in lemma_BOLZANO2)
-apply safe
-apply (blast intro: order_trans)+
-apply (auto intro: partition_append)
-apply (case_tac "a \<le> x & x \<le> b")
-apply (rule_tac [2] x = 1 in exI, auto)
-apply (rule_tac x = "g x" in exI)
-apply (auto simp add: gauge_def)
-apply (rule_tac x = "%n. if n = 0 then aa else ba" in exI)
-apply (rule_tac x = "%n. if n = 0 then x else ba" in exI)
-apply (auto simp add: tpart_def fine_def)
+lemma Integral_def2:
+ "Integral = (%(a,b) f k. \<forall>e>0. (\<exists>\<delta>. gauge {a..b} \<delta> &
+ (\<forall>D. fine \<delta> (a,b) D -->
+ \<bar>rsum D f - k\<bar> \<le> e)))"
+unfolding Integral_def
+apply (safe intro!: ext)
+apply (fast intro: less_imp_le)
+apply (drule_tac x="e/2" in spec)
+apply force
done
text{*Lemmas about combining gauges*}
lemma gauge_min:
"[| gauge(E) g1; gauge(E) g2 |]
- ==> gauge(E) (%x. if g1(x) < g2(x) then g1(x) else g2(x))"
+ ==> gauge(E) (%x. min (g1(x)) (g2(x)))"
by (simp add: gauge_def)
lemma fine_min:
- "fine (%x. if g1(x) < g2(x) then g1(x) else g2(x)) (D,p)
- ==> fine(g1) (D,p) & fine(g2) (D,p)"
-by (auto simp add: fine_def split: split_if_asm)
-
+ "fine (%x. min (g1(x)) (g2(x))) (a,b) D
+ ==> fine(g1) (a,b) D & fine(g2) (a,b) D"
+apply (erule fine.induct)
+apply (simp add: fine_Nil)
+apply (simp add: fine_Cons)
+done
text{*The integral is unique if it exists*}
@@ -315,12 +177,12 @@
apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)+
apply auto
apply (drule gauge_min, assumption)
-apply (drule_tac g = "%x. if g x < ga x then g x else ga x"
- in partition_exists, assumption, auto)
+apply (drule_tac \<delta> = "%x. min (\<delta> x) (\<delta>' x)"
+ in fine_exists, assumption, auto)
apply (drule fine_min)
apply (drule spec)+
apply auto
-apply (subgoal_tac "\<bar>(rsum (D,p) f - k2) - (rsum (D,p) f - k1)\<bar> < \<bar>k1 - k2\<bar>")
+apply (subgoal_tac "\<bar>(rsum D f - k2) - (rsum D f - k1)\<bar> < \<bar>k1 - k2\<bar>")
apply arith
apply (drule add_strict_mono, assumption)
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
@@ -330,65 +192,58 @@
lemma Integral_zero [simp]: "Integral(a,a) f 0"
apply (auto simp add: Integral_def)
apply (rule_tac x = "%x. 1" in exI)
-apply (auto dest: partition_eq simp add: gauge_def tpart_def rsum_def)
+apply (auto dest: fine_eq simp add: gauge_def rsum_def)
done
-lemma sumr_partition_eq_diff_bounds [simp]:
- "(\<Sum>n=0..<m. D (Suc n) - D n::real) = D(m) - D 0"
-by (induct "m", auto)
+lemma fine_rsum_const: "fine \<delta> (a,b) D \<Longrightarrow> rsum D (\<lambda>x. c) = (c * (b - a))"
+unfolding rsum_def
+by (induct set: fine, auto simp add: algebra_simps)
lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
-apply (auto simp add: order_le_less rsum_def Integral_def)
+apply (cases "a = b", simp)
+apply (simp add: Integral_def, clarify)
apply (rule_tac x = "%x. b - a" in exI)
-apply (auto simp add: gauge_def abs_less_iff tpart_def partition)
+apply (rule conjI, simp add: gauge_def)
+apply (clarify)
+apply (subst fine_rsum_const, assumption, simp)
done
lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b - a))"
-apply (auto simp add: order_le_less rsum_def Integral_def)
+apply (cases "a = b", simp)
+apply (simp add: Integral_def, clarify)
apply (rule_tac x = "%x. b - a" in exI)
-apply (auto simp add: setsum_right_distrib [symmetric] gauge_def abs_less_iff
- right_diff_distrib [symmetric] partition tpart_def)
+apply (rule conjI, simp add: gauge_def)
+apply (clarify)
+apply (subst fine_rsum_const, assumption, simp)
done
lemma Integral_mult:
"[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
apply (auto simp add: order_le_less
dest: Integral_unique [OF order_refl Integral_zero])
-apply (auto simp add: rsum_def Integral_def setsum_right_distrib[symmetric] mult_assoc)
-apply (rule_tac a2 = c in abs_ge_zero [THEN order_le_imp_less_or_eq, THEN disjE])
- prefer 2 apply force
-apply (drule_tac x = "e/abs c" in spec, auto)
-apply (simp add: zero_less_mult_iff divide_inverse)
-apply (rule exI, auto)
-apply (drule spec)+
-apply auto
-apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1])
-apply (auto simp add: abs_mult divide_inverse [symmetric] right_diff_distrib [symmetric])
+apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc)
+apply (case_tac "c = 0", force)
+apply (drule_tac x = "e/abs c" in spec)
+apply (simp add: divide_pos_pos)
+apply clarify
+apply (rule_tac x="\<delta>" in exI, clarify)
+apply (drule_tac x="D" in spec, clarify)
+apply (simp add: pos_less_divide_eq abs_mult [symmetric]
+ algebra_simps rsum_right_distrib)
done
+
text{*Fundamental theorem of calculus (Part I)*}
text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *}
-lemma choiceP: "\<forall>x. P(x) --> (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) --> Q x (f x))"
-by (insert bchoice [of "Collect P" Q], simp)
-
-(*UNUSED
-lemma choice2: "\<forall>x. (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==>
- \<exists>f fa. (\<forall>x. R(f x) & Q x (f x) (fa x))"
-*)
-
-
-(* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance
- they break the original proofs and make new proofs longer!*)
lemma strad1:
- "\<lbrakk>\<forall>xa::real. xa \<noteq> x \<and> \<bar>xa - x\<bar> < s \<longrightarrow>
- \<bar>(f xa - f x) / (xa - x) - f' x\<bar> * 2 < e;
- 0 < e; a \<le> x; x \<le> b; 0 < s\<rbrakk>
- \<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> * 2 \<le> e * \<bar>z - x\<bar>"
-apply auto
-apply (case_tac "0 < \<bar>z - x\<bar>")
- prefer 2 apply (simp add: zero_less_abs_iff)
+ "\<lbrakk>\<forall>z::real. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow>
+ \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2;
+ 0 < s; 0 < e; a \<le> x; x \<le> b\<rbrakk>
+ \<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
+apply clarify
+apply (case_tac "z = x", simp)
apply (drule_tac x = z in spec)
apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>"
in real_mult_le_cancel_iff2 [THEN iffD1])
@@ -405,71 +260,82 @@
done
lemma lemma_straddle:
- "[| \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x); 0 < e |]
- ==> \<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
+ assumes f': "\<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x)" and "0 < e"
+ shows "\<exists>g. gauge {a..b} g &
(\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
--> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
-apply (simp add: gauge_def)
-apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b -->
+proof -
+ have "\<forall>x\<in>{a..b}.
(\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d -->
- \<bar>(f (v) - f (u)) - (f' (x) * (v - u))\<bar> \<le> e * (v - u))")
-apply (drule choiceP, auto)
-apply (drule spec, auto)
-apply (auto simp add: DERIV_iff2 LIM_def)
-apply (drule_tac x = "e/2" in spec, auto)
-apply (frule strad1, assumption+)
-apply (rule_tac x = s in exI, auto)
-apply (rule_tac x = u and y = v in linorder_cases, auto)
-apply (rule_tac y = "\<bar>(f (v) - f (x)) - (f' (x) * (v - x))\<bar> +
- \<bar>(f (x) - f (u)) - (f' (x) * (x - u))\<bar>"
- in order_trans)
-apply (rule abs_triangle_ineq [THEN [2] order_trans])
-apply (simp add: right_diff_distrib)
-apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
-apply (rule add_mono)
-apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
- prefer 2 apply simp
-apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' - x\<bar> < s --> ?P x'" in thin_rl)
-apply (drule_tac x = v in spec, simp add: times_divide_eq)
-apply (drule_tac x = u in spec, auto)
-apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
-apply (rule order_trans)
-apply (auto simp add: abs_le_iff)
-apply (simp add: right_diff_distrib)
-done
+ \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
+ proof (clarsimp)
+ fix x :: real assume "a \<le> x" and "x \<le> b"
+ with f' have "DERIV f x :> f'(x)" by simp
+ then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
+ by (simp add: DERIV_iff2 LIM_def)
+ with `0 < e` obtain s
+ where "\<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s"
+ by (drule_tac x="e/2" in spec, auto)
+ then have strad [rule_format]:
+ "\<forall>z. \<bar>z - x\<bar> < s --> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
+ using `0 < e` `a \<le> x` `x \<le> b` by (rule strad1)
+ show "\<exists>d>0. \<forall>u v. u \<le> x \<and> x \<le> v \<and> v - u < d \<longrightarrow> \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)"
+ proof (safe intro!: exI)
+ show "0 < s" by fact
+ next
+ fix u v :: real assume "u \<le> x" and "x \<le> v" and "v - u < s"
+ have "\<bar>f v - f u - f' x * (v - u)\<bar> =
+ \<bar>(f v - f x - f' x * (v - x)) + (f x - f u - f' x * (x - u))\<bar>"
+ by (simp add: right_diff_distrib)
+ also have "\<dots> \<le> \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f x - f u - f' x * (x - u)\<bar>"
+ by (rule abs_triangle_ineq)
+ also have "\<dots> = \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f u - f x - f' x * (u - x)\<bar>"
+ by (simp add: right_diff_distrib)
+ also have "\<dots> \<le> (e/2) * \<bar>v - x\<bar> + (e/2) * \<bar>u - x\<bar>"
+ using `u \<le> x` `x \<le> v` `v - u < s` by (intro add_mono strad, simp_all)
+ also have "\<dots> \<le> e * (v - u) / 2 + e * (v - u) / 2"
+ using `u \<le> x` `x \<le> v` `0 < e` by (intro add_mono, simp_all)
+ also have "\<dots> = e * (v - u)"
+ by simp
+ finally show "\<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)" .
+ qed
+ qed
+ thus ?thesis
+ by (simp add: gauge_def) (drule bchoice, auto)
+qed
+
+lemma fine_listsum_eq_diff:
+ fixes f :: "real \<Rightarrow> real"
+ shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
+by (induct set: fine) simp_all
lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
==> Integral(a,b) f' (f(b) - f(a))"
-apply (drule order_le_imp_less_or_eq, auto)
-apply (auto simp add: Integral_def)
-apply (rule ccontr)
-apply (subgoal_tac "\<forall>e > 0. \<exists>g. gauge (%x. a \<le> x & x \<le> b) g & (\<forall>D p. tpart (a, b) (D, p) & fine g (D, p) --> \<bar>rsum (D, p) f' - (f b - f a)\<bar> \<le> e)")
-apply (rotate_tac 3)
-apply (drule_tac x = "e/2" in spec, auto)
-apply (drule spec, auto)
-apply ((drule spec)+, auto)
-apply (drule_tac e = "ea/ (b - a)" in lemma_straddle)
-apply (auto simp add: zero_less_divide_iff)
-apply (rule exI)
-apply (auto simp add: tpart_def rsum_def)
-apply (subgoal_tac "(\<Sum>n=0..<psize D. f(D(Suc n)) - f(D n)) = f b - f a")
- prefer 2
- apply (cut_tac D = "%n. f (D n)" and m = "psize D"
- in sumr_partition_eq_diff_bounds)
- apply (simp add: partition_lhs partition_rhs)
-apply (drule sym, simp)
-apply (simp (no_asm) add: setsum_subtractf[symmetric])
-apply (rule setsum_abs [THEN order_trans])
-apply (subgoal_tac "ea = (\<Sum>n=0..<psize D. (ea / (b - a)) * (D (Suc n) - (D n)))")
-apply (simp add: abs_minus_commute)
-apply (rule_tac t = ea in ssubst, assumption)
-apply (rule setsum_mono)
-apply (rule_tac [2] setsum_right_distrib [THEN subst])
-apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub
- fine_def)
+ apply (drule order_le_imp_less_or_eq, auto)
+ apply (auto simp add: Integral_def2)
+ apply (drule_tac e = "e / (b - a)" in lemma_straddle)
+ apply (simp add: divide_pos_pos)
+ apply clarify
+ apply (rule_tac x="g" in exI, clarify)
+ apply (clarsimp simp add: rsum_def)
+ apply (frule fine_listsum_eq_diff [where f=f])
+ apply (erule subst)
+ apply (subst listsum_subtractf [symmetric])
+ apply (rule listsum_abs [THEN order_trans])
+ apply (subst map_compose [symmetric, unfolded o_def])
+ apply (subgoal_tac "e = (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))")
+ apply (erule ssubst)
+ apply (simp add: abs_minus_commute)
+ apply (rule listsum_mono)
+ apply (clarify, rename_tac u x v)
+ apply ((drule spec)+, erule mp)
+ apply (simp add: mem_fine mem_fine2 mem_fine3)
+ apply (frule fine_listsum_eq_diff [where f="\<lambda>x. x"])
+ apply (simp only: split_def)
+ apply (subst listsum_const_mult)
+ apply simp
done
-
lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
by simp
@@ -485,320 +351,40 @@
apply (drule_tac [3] ?k2.0 = "f c - f b" in Integral_unique, auto)
done
-lemma partition_psize_Least:
- "partition(a,b) D ==> psize D = (LEAST n. D(n) = b)"
-apply (auto intro!: Least_equality [symmetric] partition_rhs)
-apply (auto dest: partition_ub_lt simp add: linorder_not_less [symmetric])
-done
-
-lemma lemma_partition_bounded: "partition (a, c) D ==> ~ (\<exists>n. c < D(n))"
-apply safe
-apply (drule_tac r = n in partition_ub, auto)
-done
-
-lemma lemma_partition_eq:
- "partition (a, c) D ==> D = (%n. if D n < c then D n else c)"
-apply (rule ext, auto)
-apply (auto dest!: lemma_partition_bounded)
-apply (drule_tac x = n in spec, auto)
-done
-
-lemma lemma_partition_eq2:
- "partition (a, c) D ==> D = (%n. if D n \<le> c then D n else c)"
-apply (rule ext, auto)
-apply (auto dest!: lemma_partition_bounded)
-apply (drule_tac x = n in spec, auto)
-done
-
-lemma partition_lt_Suc:
- "[| partition(a,b) D; n < psize D |] ==> D n < D (Suc n)"
-by (auto simp add: partition)
-
-lemma tpart_tag_eq: "tpart(a,c) (D,p) ==> p = (%n. if D n < c then p n else c)"
-apply (rule ext)
-apply (auto simp add: tpart_def)
-apply (drule linorder_not_less [THEN iffD1])
-apply (drule_tac r = "Suc n" in partition_ub)
-apply (drule_tac x = n in spec, auto)
-done
-
-subsection{*Lemmas for Additivity Theorem of Gauge Integral*}
-
-lemma lemma_additivity1:
- "[| a \<le> D n; D n < b; partition(a,b) D |] ==> n < psize D"
-by (auto simp add: partition linorder_not_less [symmetric])
-
-lemma lemma_additivity2: "[| a \<le> D n; partition(a,D n) D |] ==> psize D \<le> n"
-apply (rule ccontr, drule not_leE)
-apply (frule partition [THEN iffD1], safe)
-apply (frule_tac r = "Suc n" in partition_ub)
-apply (auto dest!: spec)
-done
-
-lemma partition_eq_bound:
- "[| partition(a,b) D; psize D < m |] ==> D(m) = D(psize D)"
-by (auto simp add: partition)
-
-lemma partition_ub2: "[| partition(a,b) D; psize D < m |] ==> D(r) \<le> D(m)"
-by (simp add: partition partition_ub)
-
-lemma tag_point_eq_partition_point:
- "[| tpart(a,b) (D,p); psize D \<le> m |] ==> p(m) = D(m)"
-apply (simp add: tpart_def, auto)
-apply (drule_tac x = m in spec)
-apply (auto simp add: partition_rhs2)
-done
-
-lemma partition_lt_cancel: "[| partition(a,b) D; D m < D n |] ==> m < n"
-apply (cut_tac less_linear [of n "psize D"], auto)
-apply (cut_tac less_linear [of m n])
-apply (cut_tac less_linear [of m "psize D"])
-apply (auto dest: partition_gt)
-apply (drule_tac n = m in partition_lt_gen, auto)
-apply (frule partition_eq_bound)
-apply (drule_tac [2] partition_gt, auto)
-apply (metis linear not_less partition_rhs partition_rhs2)
-apply (metis lemma_additivity1 order_less_trans partition_eq_bound partition_lb partition_rhs)
-done
-
-lemma lemma_additivity4_psize_eq:
- "[| a \<le> D n; D n < b; partition (a, b) D |]
- ==> psize (%x. if D x < D n then D(x) else D n) = n"
-apply (frule (2) lemma_additivity1)
-apply (rule psize_unique, auto)
-apply (erule partition_lt_Suc, erule (1) less_trans)
-apply (erule notE)
-apply (erule (1) partition_lt_gen, erule less_imp_le)
-apply (drule (1) partition_lt_cancel, simp)
-done
-
-lemma lemma_psize_left_less_psize:
- "partition (a, b) D
- ==> psize (%x. if D x < D n then D(x) else D n) \<le> psize D"
-apply (frule_tac r = n in partition_ub)
-apply (drule_tac x = "D n" in order_le_imp_less_or_eq)
-apply (auto simp add: lemma_partition_eq [symmetric])
-apply (frule_tac r = n in partition_lb)
-apply (drule (2) lemma_additivity4_psize_eq)
-apply (rule ccontr, auto)
-apply (frule_tac not_leE [THEN [2] partition_eq_bound])
-apply (auto simp add: partition_rhs)
-done
-
-lemma lemma_psize_left_less_psize2:
- "[| partition(a,b) D; na < psize (%x. if D x < D n then D(x) else D n) |]
- ==> na < psize D"
-by (erule lemma_psize_left_less_psize [THEN [2] less_le_trans])
-
-
-lemma lemma_additivity3:
- "[| partition(a,b) D; D na < D n; D n < D (Suc na);
- n < psize D |]
- ==> False"
-by (metis not_less_eq partition_lt_cancel real_of_nat_less_iff)
-
-
-lemma psize_const [simp]: "psize (%x. k) = 0"
-by (auto simp add: psize_def)
-
-lemma lemma_additivity3a:
- "[| partition(a,b) D; D na < D n; D n < D (Suc na);
- na < psize D |]
- ==> False"
-apply (frule_tac m = n in partition_lt_cancel)
-apply (auto intro: lemma_additivity3)
-done
-
-lemma better_lemma_psize_right_eq1:
- "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) \<le> psize D - n"
-apply (simp add: psize_def [of "(%x. D (x + n))"]);
-apply (rule_tac a = "psize D - n" in someI2, auto)
- apply (simp add: partition less_diff_conv)
- apply (simp add: le_diff_conv partition_rhs2 split: nat_diff_split)
-apply (drule_tac x = "psize D - n" in spec, auto)
-apply (frule partition_rhs, safe)
-apply (frule partition_lt_cancel, assumption)
-apply (drule partition [THEN iffD1], safe)
-apply (subgoal_tac "~ D (psize D - n + n) < D (Suc (psize D - n + n))")
- apply blast
-apply (drule_tac x = "Suc (psize D)" and P="%n. ?P n \<longrightarrow> D n = D (psize D)"
- in spec)
-apply simp
-done
-
-lemma psize_le_n: "partition (a, D n) D ==> psize D \<le> n"
-apply (rule ccontr, drule not_leE)
-apply (frule partition_lt_Suc, assumption)
-apply (frule_tac r = "Suc n" in partition_ub, auto)
-done
-
-lemma better_lemma_psize_right_eq1a:
- "partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D - n"
-apply (simp add: psize_def [of "(%x. D (x + n))"]);
-apply (rule_tac a = "psize D - n" in someI2, auto)
- apply (simp add: partition less_diff_conv)
- apply (simp add: le_diff_conv)
-apply (case_tac "psize D \<le> n")
- apply (force intro: partition_rhs2)
- apply (simp add: partition linorder_not_le)
-apply (rule ccontr, drule not_leE)
-apply (frule psize_le_n)
-apply (drule_tac x = "psize D - n" in spec, simp)
-apply (drule partition [THEN iffD1], safe)
-apply (drule_tac x = "Suc n" and P="%na. ?s \<le> na \<longrightarrow> D na = D n" in spec, auto)
-done
-
-lemma better_lemma_psize_right_eq:
- "partition(a,b) D ==> psize (%x. D (x + n)) \<le> psize D - n"
-apply (frule_tac r1 = n in partition_ub [THEN order_le_imp_less_or_eq])
-apply (blast intro: better_lemma_psize_right_eq1a better_lemma_psize_right_eq1)
-done
-
-lemma lemma_psize_right_eq1:
- "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) \<le> psize D"
-apply (simp add: psize_def [of "(%x. D (x + n))"])
-apply (rule_tac a = "psize D - n" in someI2, auto)
- apply (simp add: partition less_diff_conv)
- apply (subgoal_tac "n \<le> psize D")
- apply (simp add: partition le_diff_conv)
- apply (rule ccontr, drule not_leE)
- apply (drule_tac less_imp_le [THEN [2] partition_rhs2], assumption, simp)
-apply (drule_tac x = "psize D" in spec)
-apply (simp add: partition)
-done
-
-(* should be combined with previous theorem; also proof has redundancy *)
-lemma lemma_psize_right_eq1a:
- "partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D"
-apply (simp add: psize_def [of "(%x. D (x + n))"]);
-apply (rule_tac a = "psize D - n" in someI2, auto)
- apply (simp add: partition less_diff_conv)
- apply (case_tac "psize D \<le> n")
- apply (force intro: partition_rhs2 simp add: le_diff_conv)
- apply (simp add: partition le_diff_conv)
-apply (rule ccontr, drule not_leE)
-apply (drule_tac x = "psize D" in spec)
-apply (simp add: partition)
-done
-
-lemma lemma_psize_right_eq:
- "[| partition(a,b) D |] ==> psize (%x. D (x + n)) \<le> psize D"
-apply (frule_tac r1 = n in partition_ub [THEN order_le_imp_less_or_eq])
-apply (blast intro: lemma_psize_right_eq1a lemma_psize_right_eq1)
-done
-
-lemma tpart_left1:
- "[| a \<le> D n; tpart (a, b) (D, p) |]
- ==> tpart(a, D n) (%x. if D x < D n then D(x) else D n,
- %x. if D x < D n then p(x) else D n)"
-apply (frule_tac r = n in tpart_partition [THEN partition_ub])
-apply (drule_tac x = "D n" in order_le_imp_less_or_eq)
-apply (auto simp add: tpart_partition [THEN lemma_partition_eq, symmetric] tpart_tag_eq [symmetric])
-apply (frule_tac tpart_partition [THEN [3] lemma_additivity1])
-apply (auto simp add: tpart_def)
-apply (drule_tac [2] linorder_not_less [THEN iffD1, THEN order_le_imp_less_or_eq], auto)
- prefer 3 apply (drule_tac x=na in spec, arith)
- prefer 2 apply (blast dest: lemma_additivity3)
-apply (frule (2) lemma_additivity4_psize_eq)
-apply (rule partition [THEN iffD2])
-apply (frule partition [THEN iffD1])
-apply safe
-apply (auto simp add: partition_lt_gen)
-apply (drule (1) partition_lt_cancel, arith)
-done
-
-lemma fine_left1:
- "[| a \<le> D n; tpart (a, b) (D, p); gauge (%x. a \<le> x & x \<le> D n) g;
- fine (%x. if x < D n then min (g x) ((D n - x)/ 2)
- else if x = D n then min (g (D n)) (ga (D n))
- else min (ga x) ((x - D n)/ 2)) (D, p) |]
- ==> fine g
- (%x. if D x < D n then D(x) else D n,
- %x. if D x < D n then p(x) else D n)"
-apply (auto simp add: fine_def tpart_def gauge_def)
-apply (frule_tac [!] na=na in lemma_psize_left_less_psize2)
-apply (drule_tac [!] x = na in spec, auto)
-apply (drule_tac [!] x = na in spec, auto)
-apply (auto dest: lemma_additivity3a simp add: split_if_asm)
-done
-
-lemma tpart_right1:
- "[| a \<le> D n; tpart (a, b) (D, p) |]
- ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))"
-apply (simp add: tpart_def partition_def, safe)
-apply (rule_tac x = "N - n" in exI, auto)
-done
-
-lemma fine_right1:
- "[| a \<le> D n; tpart (a, b) (D, p); gauge (%x. D n \<le> x & x \<le> b) ga;
- fine (%x. if x < D n then min (g x) ((D n - x)/ 2)
- else if x = D n then min (g (D n)) (ga (D n))
- else min (ga x) ((x - D n)/ 2)) (D, p) |]
- ==> fine ga (%x. D(x + n),%x. p(x + n))"
-apply (auto simp add: fine_def gauge_def)
-apply (drule_tac x = "na + n" in spec)
-apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto)
-apply (simp add: tpart_def, safe)
-apply (subgoal_tac "D n \<le> p (na + n)")
-apply (drule_tac y = "p (na + n)" in order_le_imp_less_or_eq)
-apply safe
-apply (simp split: split_if_asm, simp)
-apply (drule less_le_trans, assumption)
-apply (rotate_tac 5)
-apply (drule_tac x = "na + n" in spec, safe)
-apply (rule_tac y="D (na + n)" in order_trans)
-apply (case_tac "na = 0", auto)
-apply (erule partition_lt_gen [THEN order_less_imp_le])
-apply arith
-apply arith
-done
-
-lemma rsum_add: "rsum (D, p) (%x. f x + g x) = rsum (D, p) f + rsum(D, p) g"
-by (simp add: rsum_def setsum_addf left_distrib)
+subsection {* Additivity Theorem of Gauge Integral *}
text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
lemma Integral_add_fun:
"[| a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 |]
==> Integral(a,b) (%x. f x + g x) (k1 + k2)"
-apply (simp add: Integral_def, auto)
-apply ((drule_tac x = "e/2" in spec)+)
-apply auto
-apply (drule gauge_min, assumption)
-apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x)" in exI)
-apply auto
+unfolding Integral_def
+apply clarify
+apply (drule_tac x = "e/2" in spec)+
+apply clarsimp
+apply (rule_tac x = "\<lambda>x. min (\<delta> x) (\<delta>' x)" in exI)
+apply (rule conjI, erule (1) gauge_min)
+apply clarify
apply (drule fine_min)
-apply ((drule spec)+, auto)
-apply (drule_tac a = "\<bar>rsum (D, p) f - k1\<bar> * 2" and c = "\<bar>rsum (D, p) g - k2\<bar> * 2" in add_strict_mono, assumption)
+apply (drule_tac x=D in spec, simp)+
+apply (drule_tac a = "\<bar>rsum D f - k1\<bar> * 2" and c = "\<bar>rsum D g - k2\<bar> * 2" in add_strict_mono, assumption)
apply (auto simp only: rsum_add left_distrib [symmetric]
mult_2_right [symmetric] real_mult_less_iff1)
done
-lemma partition_lt_gen2:
- "[| partition(a,b) D; r < psize D |] ==> 0 < D (Suc r) - D r"
-by (auto simp add: partition)
-
-lemma lemma_Integral_le:
- "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
- tpart(a,b) (D,p)
- |] ==> \<forall>n \<le> psize D. f (p n) \<le> g (p n)"
-apply (simp add: tpart_def)
-apply (auto, frule partition [THEN iffD1], auto)
-apply (drule_tac x = "p n" in spec, auto)
-apply (case_tac "n = 0", simp)
-apply (rule partition_lt_gen [THEN order_less_le_trans, THEN order_less_imp_le], auto)
-apply (drule le_imp_less_or_eq, auto)
-apply (drule_tac [2] x = "psize D" in spec, auto)
-apply (drule_tac r = "Suc n" in partition_ub)
-apply (drule_tac x = n in spec, auto)
-done
-
lemma lemma_Integral_rsum_le:
"[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
- tpart(a,b) (D,p)
- |] ==> rsum(D,p) f \<le> rsum(D,p) g"
-apply (simp add: rsum_def)
-apply (auto intro!: setsum_mono dest: tpart_partition [THEN partition_lt_gen2]
- dest!: lemma_Integral_le)
+ fine \<delta> (a,b) D
+ |] ==> rsum D f \<le> rsum D g"
+unfolding rsum_def
+apply (rule listsum_mono)
+apply clarify
+apply (rule mult_right_mono)
+apply (drule spec, erule mp)
+apply (frule (1) mem_fine)
+apply (frule (1) mem_fine2)
+apply simp
+apply (frule (1) mem_fine)
+apply simp
done
lemma Integral_le:
@@ -811,13 +397,11 @@
apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)
apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec, auto)
apply (drule gauge_min, assumption)
-apply (drule_tac g = "%x. if ga x < gaa x then ga x else gaa x"
- in partition_exists, assumption, auto)
+apply (drule_tac \<delta> = "\<lambda>x. min (\<delta> x) (\<delta>' x)" in fine_exists, assumption, clarify)
apply (drule fine_min)
-apply (drule_tac x = D in spec, drule_tac x = D in spec)
-apply (drule_tac x = p in spec, drule_tac x = p in spec, auto)
+apply (drule_tac x = D in spec, drule_tac x = D in spec, clarsimp)
apply (frule lemma_Integral_rsum_le, assumption)
-apply (subgoal_tac "\<bar>(rsum (D,p) f - k1) - (rsum (D,p) g - k2)\<bar> < \<bar>k1 - k2\<bar>")
+apply (subgoal_tac "\<bar>(rsum D f - k1) - (rsum D g - k2)\<bar> < \<bar>k1 - k2\<bar>")
apply arith
apply (drule add_strict_mono, assumption)
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
@@ -826,18 +410,18 @@
lemma Integral_imp_Cauchy:
"(\<exists>k. Integral(a,b) f k) ==>
- (\<forall>e > 0. \<exists>g. gauge (%x. a \<le> x & x \<le> b) g &
- (\<forall>D1 D2 p1 p2.
- tpart(a,b) (D1, p1) & fine g (D1,p1) &
- tpart(a,b) (D2, p2) & fine g (D2,p2) -->
- \<bar>rsum(D1,p1) f - rsum(D2,p2) f\<bar> < e))"
+ (\<forall>e > 0. \<exists>\<delta>. gauge {a..b} \<delta> &
+ (\<forall>D1 D2.
+ fine \<delta> (a,b) D1 &
+ fine \<delta> (a,b) D2 -->
+ \<bar>rsum D1 f - rsum D2 f\<bar> < e))"
apply (simp add: Integral_def, auto)
apply (drule_tac x = "e/2" in spec, auto)
apply (rule exI, auto)
apply (frule_tac x = D1 in spec)
-apply (frule_tac x = D2 in spec)
-apply ((drule spec)+, auto)
-apply (erule_tac V = "0 < e" in thin_rl)
+apply (drule_tac x = D2 in spec)
+apply simp
+apply (thin_tac "0 < e")
apply (drule add_strict_mono, assumption)
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
real_mult_less_iff1)
@@ -854,11 +438,6 @@
apply (drule_tac x = na in spec, auto)
done
-lemma partition_exists2:
- "[| a \<le> b; \<forall>n. gauge (%x. a \<le> x & x \<le> b) (fa n) |]
- ==> \<forall>n. \<exists>D p. tpart (a, b) (D, p) & fine (fa n) (D, p)"
-by (blast dest: partition_exists)
-
lemma monotonic_anti_derivative:
fixes f g :: "real => real" shows
"[| a \<le> b; \<forall>c. a \<le> c & c \<le> b --> f' c \<le> g' c;
--- a/src/HOL/IsaMakefile Wed May 27 20:35:16 2009 +0200
+++ b/src/HOL/IsaMakefile Wed May 27 21:08:47 2009 +0200
@@ -244,6 +244,7 @@
Tools/numeral_simprocs.ML \
Tools/numeral_syntax.ML \
Tools/polyhash.ML \
+ Tools/quickcheck_generators.ML \
Tools/Qelim/cooper_data.ML \
Tools/Qelim/cooper.ML \
Tools/Qelim/generated_cooper.ML \
--- a/src/HOL/List.thy Wed May 27 20:35:16 2009 +0200
+++ b/src/HOL/List.thy Wed May 27 21:08:47 2009 +0200
@@ -1365,6 +1365,13 @@
"(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
by (induct xs, auto)
+lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]"
+by(induct xs arbitrary: k)(auto split:nat.splits)
+
+lemma rev_update:
+ "k < length xs \<Longrightarrow> rev (xs[k:= y]) = (rev xs)[length xs - k - 1 := y]"
+by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)
+
lemma update_zip:
"(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
@@ -2212,6 +2219,36 @@
shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
by (induct xs) simp_all
+lemma listsum_addf:
+ fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"
+ shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
+by (induct xs) (simp_all add: algebra_simps)
+
+lemma listsum_subtractf:
+ fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"
+ shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
+by (induct xs) simp_all
+
+lemma listsum_const_mult:
+ fixes f :: "'a \<Rightarrow> 'b::semiring_0"
+ shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
+by (induct xs, simp_all add: algebra_simps)
+
+lemma listsum_mult_const:
+ fixes f :: "'a \<Rightarrow> 'b::semiring_0"
+ shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
+by (induct xs, simp_all add: algebra_simps)
+
+lemma listsum_abs:
+ fixes xs :: "'a::pordered_ab_group_add_abs list"
+ shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
+by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
+
+lemma listsum_mono:
+ fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, pordered_ab_semigroup_add}"
+ shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)"
+by (induct xs, simp, simp add: add_mono)
+
subsubsection {* @{text upt} *}
--- a/src/HOL/Quickcheck.thy Wed May 27 20:35:16 2009 +0200
+++ b/src/HOL/Quickcheck.thy Wed May 27 21:08:47 2009 +0200
@@ -4,6 +4,7 @@
theory Quickcheck
imports Random Code_Eval
+uses ("Tools/quickcheck_generators.ML")
begin
notation fcomp (infixl "o>" 60)
@@ -16,59 +17,7 @@
fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-subsection {* Quickcheck generator *}
-
-ML {*
-structure Quickcheck =
-struct
-
-open Quickcheck;
-
-val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
-
-val target = "Quickcheck";
-
-fun mk_generator_expr thy prop tys =
- let
- val bound_max = length tys - 1;
- val bounds = map_index (fn (i, ty) =>
- (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
- val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
- val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
- val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
- $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
- val return = @{term "Pair \<Colon> term list option \<Rightarrow> Random.seed \<Rightarrow> term list option \<times> Random.seed"};
- fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
- fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
- fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
- liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
- fun mk_split ty = Sign.mk_const thy
- (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
- fun mk_scomp_split ty t t' =
- mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t
- (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
- fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
- (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
- in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
-
-fun compile_generator_expr thy t =
- let
- val tys = (map snd o fst o strip_abs) t;
- val t' = mk_generator_expr thy t tys;
- val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
- (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
- in f #> Random_Engine.run end;
-
-end
-*}
-
-setup {*
- Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I))
- #> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
-*}
-
-
-subsection {* Fundamental types*}
+subsection {* Fundamental and numeric types*}
instantiation bool :: random
begin
@@ -91,66 +40,6 @@
end
-text {* Type @{typ "'a \<Rightarrow> 'b"} *}
-
-ML {*
-structure Random_Engine =
-struct
-
-open Random_Engine;
-
-fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
- (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed)
- (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
- (seed : Random_Engine.seed) =
- let
- val (seed', seed'') = random_split seed;
- val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
- val fun_upd = Const (@{const_name fun_upd},
- (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
- fun random_fun' x =
- let
- val (seed, fun_map, f_t) = ! state;
- in case AList.lookup (uncurry eq) fun_map x
- of SOME y => y
- | NONE => let
- val t1 = term_of x;
- val ((y, t2), seed') = random seed;
- val fun_map' = (x, y) :: fun_map;
- val f_t' = fun_upd $ f_t $ t1 $ t2 ();
- val _ = state := (seed', fun_map', f_t');
- in y end
- end;
- fun term_fun' () = #3 (! state);
- in ((random_fun', term_fun'), seed'') end;
-
-end
-*}
-
-axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
- \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
- \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-
-code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun")
- -- {* With enough criminal energy this can be abused to derive @{prop False};
- for this reason we use a distinguished target @{text Quickcheck}
- not spoiling the regular trusted code generation *}
-
-instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
-begin
-
-definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
- "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
-
-instance ..
-
-end
-
-code_reserved Quickcheck Random_Engine
-
-
-subsection {* Numeric types *}
-
instantiation nat :: random
begin
@@ -175,59 +64,40 @@
end
-subsection {* Type copies *}
+
+subsection {* Complex generators *}
+
+definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+ "collapse f = (f o\<rightarrow> id)"
-setup {*
-let
+definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
+ "beyond k l = (if l > k then l else 0)"
+
+use "Tools/quickcheck_generators.ML"
+setup {* Quickcheck_Generators.setup *}
+
+code_reserved Quickcheck Quickcheck_Generators
+
+text {* Type @{typ "'a \<Rightarrow> 'b"} *}
-fun mk_random_typecopy tyco vs constr typ thy =
- let
- val Ts = map TFree vs;
- val T = Type (tyco, Ts);
- fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"})
- val Ttm = mk_termifyT T;
- val typtm = mk_termifyT typ;
- fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
- fun mk_random T = mk_const @{const_name random} [T];
- val size = @{term "k\<Colon>code_numeral"};
- val v = "x";
- val t_v = Free (v, typtm);
- val t_constr = mk_const constr Ts;
- val lhs = mk_random T $ size;
- val rhs = HOLogic.mk_ST [(((mk_random typ) $ size, @{typ Random.seed}), SOME (v, typtm))]
- (HOLogic.mk_return Ttm @{typ Random.seed}
- (mk_const "Code_Eval.valapp" [typ, T]
- $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
- @{typ Random.seed} (SOME Ttm, @{typ Random.seed});
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
- in
- thy
- |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
- |> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
- |> snd
- |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end;
+axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
+ \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
+ \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-fun ensure_random_typecopy tyco thy =
- let
- val SOME { vs = raw_vs, constr, typ = raw_typ, ... } =
- TypecopyPackage.get_info thy tyco;
- val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
- val typ = map_atyps (fn TFree (v, sort) =>
- TFree (v, constrain sort @{sort random})) raw_typ;
- val vs' = Term.add_tfreesT typ [];
- val vs = map (fn (v, sort) =>
- (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
- val do_inst = Sign.of_sort thy (typ, @{sort random});
- in if do_inst then mk_random_typecopy tyco vs constr typ thy else thy end;
+code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun")
+ -- {* With enough criminal energy this can be abused to derive @{prop False};
+ for this reason we use a distinguished target @{text Quickcheck}
+ not spoiling the regular trusted code generation *}
-in
+instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
+begin
-TypecopyPackage.interpretation ensure_random_typecopy
+definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+ "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
+
+instance ..
end
-*}
no_notation fcomp (infixl "o>" 60)
--- a/src/HOL/Random.thy Wed May 27 20:35:16 2009 +0200
+++ b/src/HOL/Random.thy Wed May 27 21:08:47 2009 +0200
@@ -119,7 +119,7 @@
qed
lemma select_weigth_drop_zero:
- "Random.select_weight (filter (\<lambda>(k, _). k > 0) xs) = Random.select_weight xs"
+ "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
proof -
have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
by (induct xs) auto
@@ -128,9 +128,9 @@
lemma select_weigth_select:
assumes "xs \<noteq> []"
- shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
+ shows "select_weight (map (Pair 1) xs) = select xs"
proof -
- have less: "\<And>s. fst (Random.range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
+ have less: "\<And>s. fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
using assms by (intro range) simp
moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)"
by (induct xs) simp_all
--- a/src/HOL/Tools/datatype_codegen.ML Wed May 27 20:35:16 2009 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Wed May 27 21:08:47 2009 +0200
@@ -6,6 +6,7 @@
signature DATATYPE_CODEGEN =
sig
+ val find_shortest_path: DatatypeAux.descr -> int -> (string * int) option
val mk_eq_eqns: theory -> string -> (thm * bool) list
val mk_case_cert: theory -> string -> thm
val setup: theory -> theory
@@ -24,8 +25,9 @@
fun find_nonempty (descr: DatatypeAux.descr) is i =
let
- val (_, _, constrs) = valOf (AList.lookup (op =) descr i);
- fun arg_nonempty (_, DatatypeAux.DtRec i) = if i mem is then NONE
+ val (_, _, constrs) = the (AList.lookup (op =) descr i);
+ fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
+ then NONE
else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i)
| arg_nonempty _ = SOME 0;
fun max xs = Library.foldl
@@ -33,10 +35,12 @@
| (SOME i, SOME j) => SOME (Int.max (i, j))
| (_, NONE) => NONE) (SOME 0, xs);
val xs = sort (int_ord o pairself snd)
- (List.mapPartial (fn (s, dts) => Option.map (pair s)
+ (map_filter (fn (s, dts) => Option.map (pair s)
(max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs)
in case xs of [] => NONE | x :: _ => SOME x end;
+fun find_shortest_path descr i = find_nonempty descr [i] i;
+
fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr =
let
val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
@@ -109,7 +113,7 @@
val T = Type (tname, Us);
val (cs1, cs2) =
List.partition (exists DatatypeAux.is_rec_type o snd) cs;
- val SOME (cname, _) = find_nonempty descr [i] i;
+ val SOME (cname, _) = find_shortest_path descr i;
fun mk_delay p = Pretty.block
[str "fn () =>", Pretty.brk 1, p];
--- a/src/HOL/Tools/datatype_package.ML Wed May 27 20:35:16 2009 +0200
+++ b/src/HOL/Tools/datatype_package.ML Wed May 27 21:08:47 2009 +0200
@@ -16,9 +16,10 @@
val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
val get_datatype_constrs : theory -> string -> (string * typ) list option
val construction_interpretation : theory
- -> {atom : typ -> 'a, dtyp : string -> 'a, rtyp : string -> 'a list -> 'a}
+ -> {atom : typ -> 'a, dtyp : string -> 'a, rtyp : string * typ list -> 'a list -> 'a}
-> (string * sort) list -> string list
-> (string * (string * 'a list) list) list
+ * ((string * typ list) * (string * 'a list) list) list
val distinct_simproc : simproc
val make_case : Proof.context -> bool -> string list -> term ->
(term * term) list -> term * (term * (int * bool)) list
@@ -149,16 +150,24 @@
val descr = (#descr o the_datatype thy o hd) tycos;
val k = length tycos;
val descr_of = the o AList.lookup (op =) descr;
- fun interpT (T as DtTFree _) = atom (typ_of_dtyp descr sorts T)
- | interpT (T as DtType (tyco, Ts)) = if is_rec_type T
- then rtyp tyco (map interpT Ts)
- else atom (typ_of_dtyp descr sorts T)
+ val typ_of_dtyp = typ_of_dtyp descr sorts;
+ fun interpT (dT as DtTFree _) = atom (typ_of_dtyp dT)
+ | interpT (dT as DtType (tyco, dTs)) =
+ let
+ val Ts = map typ_of_dtyp dTs;
+ in if is_rec_type dT
+ then rtyp (tyco, Ts) (map interpT dTs)
+ else atom (Type (tyco, Ts))
+ end
| interpT (DtRec l) = if l < k then (dtyp o #1 o descr_of) l
- else let val (tyco, Ts, _) = descr_of l
- in rtyp tyco (map interpT Ts) end;
- fun interpC (c, Ts) = (c, map interpT Ts);
- fun interpK (_, (tyco, _, cs)) = (tyco, map interpC cs);
- in map interpK (Library.take (k, descr)) end;
+ else let
+ val (tyco, dTs, _) = descr_of l;
+ val Ts = map typ_of_dtyp dTs;
+ in rtyp (tyco, Ts) (map interpT dTs) end;
+ fun interpC (c, dTs) = (c, map interpT dTs);
+ fun interpD (_, (tyco, _, cs)) = (tyco, map interpC cs);
+ fun interpR (_, (tyco, dTs, cs)) = ((tyco, map typ_of_dtyp dTs), map interpC cs);
+ in chop k descr |> (apfst o map) interpD |> (apsnd o map) interpR end;
--- a/src/HOL/Tools/primrec_package.ML Wed May 27 20:35:16 2009 +0200
+++ b/src/HOL/Tools/primrec_package.ML Wed May 27 21:08:47 2009 +0200
@@ -16,6 +16,8 @@
val add_primrec_overloaded: (string * (string * typ) * bool) list ->
(binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> theory -> thm list * theory
+ val add_primrec_simple: ((binding * typ) * mixfix) list -> (binding * term) list ->
+ local_theory -> (string * thm list list) * local_theory
end;
structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -211,22 +213,12 @@
else find_dts dt_info tnames' tnames);
-(* primrec definition *)
+(* distill primitive definition(s) from primrec specification *)
-local
-
-fun prove_spec ctxt names rec_rewrites defs eqs =
+fun distill lthy fixes eqs =
let
- val rewrites = map mk_meta_eq rec_rewrites @ map (snd o snd) defs;
- fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
- val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
- in map (fn (a, t) => (a, [Goal.prove ctxt [] [] t tac])) eqs end;
-
-fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
- let
- val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
- orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes) o snd) spec [];
+ orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) eqs [];
val tnames = distinct (op =) (map (#1 o snd) eqns);
val dts = find_dts (DatatypePackage.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
val main_fns = map (fn (tname, {index, ...}) =>
@@ -236,31 +228,59 @@
("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
else snd (hd dts);
val (fnames, fnss) = fold_rev (process_fun descr eqns) main_fns ([], []);
- val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
- val names1 = map snd fnames;
- val names2 = map fst eqns;
- val _ = if gen_eq_set (op =) (names1, names2) then ()
- else primrec_error ("functions " ^ commas_quote names2 ^
+ val (fs, raw_defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
+ val defs = map (make_def lthy fixes fs) raw_defs;
+ val names = map snd fnames;
+ val names_eqns = map fst eqns;
+ val _ = if gen_eq_set (op =) (names, names_eqns) then ()
+ else primrec_error ("functions " ^ commas_quote names_eqns ^
"\nare not mutually recursive");
- val prefix = space_implode "_" (map (Long_Name.base_name o #1) defs);
- val qualify = Binding.qualify false prefix;
- val spec' = (map o apfst)
- (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
- val simp_atts = map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add];
+ val rec_rewrites' = map mk_meta_eq rec_rewrites;
+ val prefix = space_implode "_" (map (Long_Name.base_name o #1) raw_defs);
+ fun prove lthy defs =
+ let
+ val rewrites = rec_rewrites' @ map (snd o snd) defs;
+ fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
+ val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
+ in map (fn eq => [Goal.prove lthy [] [] eq tac]) eqs end;
+ in ((prefix, (fs, defs)), prove) end
+ handle PrimrecError (msg, some_eqn) =>
+ error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
+ of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn)
+ | NONE => ""));
+
+
+(* primrec definition *)
+
+fun add_primrec_simple fixes spec lthy =
+ let
+ val ((prefix, (fs, defs)), prove) = distill lthy fixes (map snd spec);
+ in
+ lthy
+ |> fold_map (LocalTheory.define Thm.definitionK) defs
+ |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
+ end;
+
+local
+
+fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
+ let
+ val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
+ fun attr_bindings prefix = map (fn ((b, attrs), _) =>
+ (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
+ fun simp_attr_binding prefix = (Binding.qualify false prefix (Binding.name "simps"),
+ map (Attrib.internal o K)
+ [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]);
in
lthy
|> set_group ? LocalTheory.set_group (serial_string ())
- |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
- |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
- |-> (fn simps => fold_map (LocalTheory.note Thm.generatedK) simps)
- |-> (fn simps' => LocalTheory.note Thm.generatedK
- ((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps'))
+ |> add_primrec_simple fixes spec
+ |-> (fn (prefix, simps) => fold_map (LocalTheory.note Thm.generatedK)
+ (attr_bindings prefix ~~ simps)
+ #-> (fn simps' => LocalTheory.note Thm.generatedK
+ (simp_attr_binding prefix, maps snd simps')))
|>> snd
- end handle PrimrecError (msg, some_eqn) =>
- error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
- of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn)
- | NONE => ""));
+ end;
in
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/quickcheck_generators.ML Wed May 27 21:08:47 2009 +0200
@@ -0,0 +1,145 @@
+(* Author: Florian Haftmann, TU Muenchen
+
+Quickcheck generators for various types.
+*)
+
+signature QUICKCHECK_GENERATORS =
+sig
+ val compile_generator_expr: theory -> term -> int -> term list option
+ type seed = Random_Engine.seed
+ val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
+ -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
+ -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
+ val ensure_random_typecopy: string -> theory -> theory
+ val eval_ref: (unit -> int -> int * int -> term list option * (int * int)) option ref
+ val setup: theory -> theory
+end;
+
+structure Quickcheck_Generators : QUICKCHECK_GENERATORS =
+struct
+
+(** building and compiling generator expressions **)
+
+val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
+
+val target = "Quickcheck";
+
+fun mk_generator_expr thy prop tys =
+ let
+ val bound_max = length tys - 1;
+ val bounds = map_index (fn (i, ty) =>
+ (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
+ val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
+ val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
+ val check = @{term "If :: bool => term list option => term list option => term list option"}
+ $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option "} $ terms);
+ val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"};
+ fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
+ fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit => term"});
+ fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
+ liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
+ fun mk_split ty = Sign.mk_const thy
+ (@{const_name split}, [ty, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
+ fun mk_scomp_split ty t t' =
+ mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t
+ (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit => term"}, t')));
+ fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
+ (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
+ in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
+
+fun compile_generator_expr thy t =
+ let
+ val tys = (map snd o fst o strip_abs) t;
+ val t' = mk_generator_expr thy t tys;
+ val f = Code_ML.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
+ (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+ in f #> Random_Engine.run end;
+
+
+(** typ "'a => 'b" **)
+
+type seed = Random_Engine.seed;
+
+fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
+ (random : seed -> ('b * (unit -> term)) * seed)
+ (random_split : seed -> seed * seed)
+ (seed : seed) =
+ let
+ val (seed', seed'') = random_split seed;
+ val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
+ val fun_upd = Const (@{const_name fun_upd},
+ (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
+ fun random_fun' x =
+ let
+ val (seed, fun_map, f_t) = ! state;
+ in case AList.lookup (uncurry eq) fun_map x
+ of SOME y => y
+ | NONE => let
+ val t1 = term_of x;
+ val ((y, t2), seed') = random seed;
+ val fun_map' = (x, y) :: fun_map;
+ val f_t' = fun_upd $ f_t $ t1 $ t2 ();
+ val _ = state := (seed', fun_map', f_t');
+ in y end
+ end;
+ fun term_fun' () = #3 (! state);
+ in ((random_fun', term_fun'), seed'') end;
+
+
+(** type copies **)
+
+fun mk_random_typecopy tyco vs constr typ thy =
+ let
+ val Ts = map TFree vs;
+ val T = Type (tyco, Ts);
+ fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
+ val Ttm = mk_termifyT T;
+ val typtm = mk_termifyT typ;
+ fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
+ fun mk_random T = mk_const @{const_name random} [T];
+ val size = @{term "j::code_numeral"};
+ val v = "x";
+ val t_v = Free (v, typtm);
+ val t_constr = mk_const constr Ts;
+ val lhs = mk_random T $ size;
+ val rhs = HOLogic.mk_ST [(((mk_random typ) $ size, @{typ Random.seed}), SOME (v, typtm))]
+ (HOLogic.mk_return Ttm @{typ Random.seed}
+ (mk_const "Code_Eval.valapp" [typ, T]
+ $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
+ @{typ Random.seed} (SOME Ttm, @{typ Random.seed});
+ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+ in
+ thy
+ |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
+ |> `(fn lthy => Syntax.check_term lthy eq)
+ |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
+ |> snd
+ |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+ end;
+
+fun ensure_random_typecopy tyco thy =
+ let
+ val SOME { vs = raw_vs, constr, typ = raw_typ, ... } =
+ TypecopyPackage.get_info thy tyco;
+ val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
+ val typ = map_atyps (fn TFree (v, sort) =>
+ TFree (v, constrain sort @{sort random})) raw_typ;
+ val vs' = Term.add_tfreesT typ [];
+ val vs = map (fn (v, sort) =>
+ (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
+ val do_inst = Sign.of_sort thy (typ, @{sort random});
+ in if do_inst then mk_random_typecopy tyco vs constr typ thy else thy end;
+
+
+(** datatypes **)
+
+(* still under construction *)
+
+
+(** setup **)
+
+val setup = Code_Target.extend_target (target, (Code_ML.target_Eval, K I))
+ #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of)
+ #> TypecopyPackage.interpretation ensure_random_typecopy;
+
+end;
--- a/src/HOL/ex/Quickcheck_Generators.thy Wed May 27 20:35:16 2009 +0200
+++ b/src/HOL/ex/Quickcheck_Generators.thy Wed May 27 21:08:47 2009 +0200
@@ -79,10 +79,11 @@
else raise TYP
("Will not generate random elements for type(s) " ^ quote (hd tycos));
fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>code_numeral"} $ @{term "j\<Colon>code_numeral"});
- fun rtyp tyco tys = raise REC
+ fun rtyp (tyco, Ts) _ = raise REC
("Will not generate random elements for mutual recursive type " ^ quote (hd tycos));
val rhss = DatatypePackage.construction_interpretation thy
{ atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos
+ |> fst
|> (map o apsnd o map) (mk_cons thy this_ty)
|> (map o apsnd) (List.partition fst)
|> map (mk_clauses thy this_ty)
--- a/src/HOL/ex/Records.thy Wed May 27 20:35:16 2009 +0200
+++ b/src/HOL/ex/Records.thy Wed May 27 21:08:47 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Records.thy
- ID: $Id$
Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel,
TU Muenchen
*)
--- a/src/Pure/Isar/class_target.ML Wed May 27 20:35:16 2009 +0200
+++ b/src/Pure/Isar/class_target.ML Wed May 27 21:08:47 2009 +0200
@@ -441,12 +441,11 @@
fun synchronize_inst_syntax ctxt =
let
val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
- val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of (ProofContext.theory_of ctxt));
- fun subst (c, ty) = case inst_tyco_of (c, ty)
- of SOME tyco => (case AList.lookup (op =) params (c, tyco)
- of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
- | NONE => NONE)
- | NONE => NONE;
+
+ val lookup_inst_param = AxClass.lookup_inst_param (Sign.consts_of (ProofContext.theory_of ctxt)) params;
+ fun subst (c, ty) = case lookup_inst_param (c, ty)
+ of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
+ | NONE => NONE;
val unchecks =
map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
in
@@ -494,38 +493,35 @@
fun init_instantiation (tycos, vs, sort) thy =
let
val _ = if null tycos then error "At least one arity must be given" else ();
- val params = these_params thy (filter (can (AxClass.get_info thy)) sort);
+ val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
fun get_param tyco (param, (_, (c, ty))) =
if can (AxClass.param_of_inst thy) (c, tyco)
then NONE else SOME ((c, tyco),
(param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
- val inst_params = map_product get_param tycos params |> map_filter I;
+ val params = map_product get_param tycos class_params |> map_filter I;
val primary_constraints = map (apsnd
- (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) params;
+ (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
val pp = Syntax.pp_global thy;
val algebra = Sign.classes_of thy
|> fold (fn tyco => Sorts.add_arities pp
(tyco, map (fn class => (class, map snd vs)) sort)) tycos;
val consts = Sign.consts_of thy;
val improve_constraints = AList.lookup (op =)
- (map (fn (_, (class, (c, _))) => (c, [[class]])) params);
+ (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
of NONE => NONE
| SOME ts' => SOME (ts', ctxt);
- val inst_tyco_of = AxClass.inst_tyco_of consts;
+ val lookup_inst_param = AxClass.lookup_inst_param consts params;
val typ_instance = Type.typ_instance (Sign.tsig_of thy);
- fun improve (c, ty) = case inst_tyco_of (c, ty)
- of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
- of SOME (_, ty') => if typ_instance (ty', ty)
- then SOME (ty, ty') else NONE
- | NONE => NONE)
+ fun improve (c, ty) = case lookup_inst_param (c, ty)
+ of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE
| NONE => NONE;
in
thy
|> ProofContext.init
- |> Instantiation.put (mk_instantiation ((tycos, vs, sort), inst_params))
+ |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
|> fold (Variable.declare_typ o TFree) vs
- |> fold (Variable.declare_names o Free o snd) inst_params
+ |> fold (Variable.declare_names o Free o snd) params
|> (Overloading.map_improvable_syntax o apfst)
(K ((primary_constraints, []), (((improve, K NONE), false), [])))
|> Overloading.add_improvable_syntax
--- a/src/Pure/axclass.ML Wed May 27 20:35:16 2009 +0200
+++ b/src/Pure/axclass.ML Wed May 27 21:08:47 2009 +0200
@@ -26,7 +26,6 @@
val axiomatize_arity: arity -> theory -> theory
val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
val instance_name: string * class -> string
- val inst_tyco_of: Consts.T -> string * typ -> string option
val declare_overloaded: string * typ -> theory -> term * theory
val define_overloaded: binding -> string * term -> theory -> thm * theory
val unoverload: theory -> thm -> thm
@@ -34,6 +33,7 @@
val unoverload_conv: theory -> conv
val overload_conv: theory -> conv
val unoverload_const: theory -> string * typ -> string
+ val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
val param_of_inst: theory -> string * string -> string
val inst_of_param: theory -> string -> (string * string) option
val arity_property: theory -> class * string -> string -> string list
@@ -249,8 +249,7 @@
fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
(get_inst_params thy) [];
-fun inst_tyco_of consts = try (fst o dest_Type o the_single o Consts.typargs consts);
-val inst_tyco_of' = inst_tyco_of o Sign.consts_of;
+fun get_inst_tyco consts = try (fst o dest_Type o the_single o Consts.typargs consts);
fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
@@ -258,9 +257,13 @@
fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
+fun lookup_inst_param consts params (c, T) = case get_inst_tyco consts (c, T)
+ of SOME tyco => AList.lookup (op =) params (c, tyco)
+ | NONE => NONE;
+
fun unoverload_const thy (c_ty as (c, _)) =
case class_of_param thy c
- of SOME class => (case inst_tyco_of' thy c_ty
+ of SOME class => (case get_inst_tyco (Sign.consts_of thy) c_ty
of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
| NONE => c)
| NONE => c;
@@ -289,15 +292,17 @@
(* declaration and definition of instances of overloaded constants *)
+fun inst_tyco_of thy (c, T) = case get_inst_tyco (Sign.consts_of thy) (c, T)
+ of SOME tyco => tyco
+ | NONE => error ("Illegal type for instantiation of class parameter: "
+ ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
+
fun declare_overloaded (c, T) thy =
let
val class = case class_of_param thy c
of SOME class => class
| NONE => error ("Not a class parameter: " ^ quote c);
- val tyco = case inst_tyco_of' thy (c, T)
- of SOME tyco => tyco
- | NONE => error ("Illegal type for instantiation of class parameter: "
- ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
+ val tyco = inst_tyco_of thy (c, T);
val name_inst = instance_name (tyco, class) ^ "_inst";
val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco;
val T' = Type.strip_sorts T;
@@ -319,7 +324,7 @@
fun define_overloaded b (c, t) thy =
let
val T = Term.fastype_of t;
- val SOME tyco = inst_tyco_of' thy (c, T);
+ val tyco = inst_tyco_of thy (c, T);
val (c', eq) = get_inst_param thy (c, tyco);
val prop = Logic.mk_equals (Const (c', T), t);
val b' = Thm.def_binding_optional
--- a/src/Pure/library.ML Wed May 27 20:35:16 2009 +0200
+++ b/src/Pure/library.ML Wed May 27 21:08:47 2009 +0200
@@ -27,6 +27,7 @@
val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
val funpow: int -> ('a -> 'a) -> 'a -> 'a
+ val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
(*errors*)
exception SYS_ERROR of string
@@ -109,6 +110,7 @@
val split_list: ('a * 'b) list -> 'a list * 'b list
val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+ val multiply: 'a list -> 'a list list -> 'a list list
val separate: 'a -> 'a list -> 'a list
val surround: 'a -> 'a list -> 'a list
val replicate: int -> 'a -> 'a list
@@ -157,7 +159,6 @@
val unsuffix: string -> string -> string
val replicate_string: int -> string -> string
val translate_string: (string -> string) -> string -> string
- val multiply: 'a list -> 'a list list -> 'a list list
val match_string: string -> string -> bool
(*lists as sets -- see also Pure/General/ord_list.ML*)
@@ -266,10 +267,12 @@
fun (f ooo g) x y z = f (g x y z);
fun (f oooo g) x y z w = f (g x y z w);
-(*function exponentiation: f(...(f x)...) with n applications of f*)
-fun funpow (0: int) _ x = x
- | funpow n f x = funpow (n - 1) f (f x);
+(*function exponentiation: f (... (f x) ...) with n applications of f*)
+fun funpow (0 : int) _ = I
+ | funpow n f = f #> funpow (n - 1) f;
+fun funpow_yield (0 : int) _ x = ([], x)
+ | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
(* errors *)
@@ -552,8 +555,6 @@
else rep (n, [])
end;
-fun translate_string f = String.translate (f o String.str);
-
(*multiply [a, b, c, ...] * [xs, ys, zs, ...]*)
fun multiply [] _ = []
| multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
@@ -790,6 +791,8 @@
if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
else replicate_string (k div 2) (a ^ a) ^ a;
+fun translate_string f = String.translate (f o String.str);
+
(*crude matching of str against simple glob pat*)
fun match_string pat str =
let
--- a/src/Pure/tactic.ML Wed May 27 20:35:16 2009 +0200
+++ b/src/Pure/tactic.ML Wed May 27 21:08:47 2009 +0200
@@ -19,9 +19,9 @@
val dresolve_tac: thm list -> int -> tactic
val atac: int -> tactic
val rtac: thm -> int -> tactic
- val dtac: thm -> int ->tactic
- val etac: thm -> int ->tactic
- val ftac: thm -> int ->tactic
+ val dtac: thm -> int -> tactic
+ val etac: thm -> int -> tactic
+ val ftac: thm -> int -> tactic
val datac: thm -> int -> int -> tactic
val eatac: thm -> int -> int -> tactic
val fatac: thm -> int -> int -> tactic