--- a/NEWS Mon Feb 28 15:06:36 2011 +0000
+++ b/NEWS Mon Feb 28 15:06:55 2011 +0000
@@ -27,6 +27,9 @@
- sledgehammer available_provers ~> sledgehammer supported_provers
INCOMPATIBILITY.
+* Function package: discontinued option "tailrec".
+INCOMPATIBILITY. Use partial_function instead.
+
*** Document preparation ***
--- a/doc-src/Functions/Thy/Functions.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/doc-src/Functions/Thy/Functions.thy Mon Feb 28 15:06:55 2011 +0000
@@ -702,11 +702,10 @@
for a zero of a given function f.
*}
-function (*<*)(domintros, tailrec)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
+function (*<*)(domintros)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
where
"findzero f n = (if f n = 0 then n else findzero f (Suc n))"
by pat_completeness auto
-(*<*)declare findzero.simps[simp del](*>*)
text {*
\noindent Clearly, any attempt of a termination proof must fail. And without
@@ -959,79 +958,6 @@
for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}.
*}
-(*lemma findzero_nicer_domintros:
- "f x = 0 \<Longrightarrow> findzero_dom (f, x)"
- "findzero_dom (f, Suc x) \<Longrightarrow> findzero_dom (f, x)"
-by (rule accpI, erule findzero_rel.cases, auto)+
-*)
-
-subsection {* A Useful Special Case: Tail recursion *}
-
-text {*
- The domain predicate is our trick that allows us to model partiality
- in a world of total functions. The downside of this is that we have
- to carry it around all the time. The termination proof above allowed
- us to replace the abstract @{term "findzero_dom (f, n)"} by the more
- concrete @{term "(x \<ge> n \<and> f x = (0::nat))"}, but the condition is still
- there and can only be discharged for special cases.
- In particular, the domain predicate guards the unfolding of our
- function, since it is there as a condition in the @{text psimp}
- rules.
-
- Now there is an important special case: We can actually get rid
- of the condition in the simplification rules, \emph{if the function
- is tail-recursive}. The reason is that for all tail-recursive
- equations there is a total function satisfying them, even if they
- are non-terminating.
-
-% A function is tail recursive, if each call to the function is either
-% equal
-%
-% So the outer form of the
-%
-%if it can be written in the following
-% form:
-% {term[display] "f x = (if COND x then BASE x else f (LOOP x))"}
-
-
- The function package internally does the right construction and can
- derive the unconditional simp rules, if we ask it to do so. Luckily,
- our @{const "findzero"} function is tail-recursive, so we can just go
- back and add another option to the \cmd{function} command:
-
-\vspace{1ex}
-\noindent\cmd{function} @{text "(domintros, tailrec) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
-\cmd{where}\isanewline%
-\ \ \ldots\\%
-
-
- \noindent Now, we actually get unconditional simplification rules, even
- though the function is partial:
-*}
-
-thm findzero.simps
-
-text {*
- @{thm[display] findzero.simps}
-
- \noindent Of course these would make the simplifier loop, so we better remove
- them from the simpset:
-*}
-
-declare findzero.simps[simp del]
-
-text {*
- Getting rid of the domain conditions in the simplification rules is
- not only useful because it simplifies proofs. It is also required in
- order to use Isabelle's code generator to generate ML code
- from a function definition.
- Since the code generator only works with equations, it cannot be
- used with @{text "psimp"} rules. Thus, in order to generate code for
- partial functions, they must be defined as a tail recursion.
- Luckily, many functions have a relatively natural tail recursive
- definition.
-*}
-
section {* Nested recursion *}
text {*
--- a/doc-src/Functions/Thy/document/Functions.tex Mon Feb 28 15:06:36 2011 +0000
+++ b/doc-src/Functions/Thy/document/Functions.tex Mon Feb 28 15:06:55 2011 +0000
@@ -1464,78 +1464,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{A Useful Special Case: Tail recursion%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The domain predicate is our trick that allows us to model partiality
- in a world of total functions. The downside of this is that we have
- to carry it around all the time. The termination proof above allowed
- us to replace the abstract \isa{findzero{\isaliteral{5F}{\isacharunderscore}}dom\ {\isaliteral{28}{\isacharparenleft}}f{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}} by the more
- concrete \isa{n\ {\isaliteral{5C3C6C653E}{\isasymle}}\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ f\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}}, but the condition is still
- there and can only be discharged for special cases.
- In particular, the domain predicate guards the unfolding of our
- function, since it is there as a condition in the \isa{psimp}
- rules.
-
- Now there is an important special case: We can actually get rid
- of the condition in the simplification rules, \emph{if the function
- is tail-recursive}. The reason is that for all tail-recursive
- equations there is a total function satisfying them, even if they
- are non-terminating.
-
-% A function is tail recursive, if each call to the function is either
-% equal
-%
-% So the outer form of the
-%
-%if it can be written in the following
-% form:
-% {term[display] "f x = (if COND x then BASE x else f (LOOP x))"}
-
-
- The function package internally does the right construction and can
- derive the unconditional simp rules, if we ask it to do so. Luckily,
- our \isa{findzero} function is tail-recursive, so we can just go
- back and add another option to the \cmd{function} command:
-
-\vspace{1ex}
-\noindent\cmd{function} \isa{{\isaliteral{28}{\isacharparenleft}}domintros{\isaliteral{2C}{\isacharcomma}}\ tailrec{\isaliteral{29}{\isacharparenright}}\ findzero\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequote}}}\\%
-\cmd{where}\isanewline%
-\ \ \ldots\\%
-
-
- \noindent Now, we actually get unconditional simplification rules, even
- though the function is partial:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{thm}\isamarkupfalse%
-\ findzero{\isaliteral{2E}{\isachardot}}simps%
-\begin{isamarkuptext}%
-\begin{isabelle}%
-findzero\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isaliteral{3F}{\isacharquery}}n\ else\ findzero\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{3F}{\isacharquery}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-
- \noindent Of course these would make the simplifier loop, so we better remove
- them from the simpset:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{declare}\isamarkupfalse%
-\ findzero{\isaliteral{2E}{\isachardot}}simps{\isaliteral{5B}{\isacharbrackleft}}simp\ del{\isaliteral{5D}{\isacharbrackright}}%
-\begin{isamarkuptext}%
-Getting rid of the domain conditions in the simplification rules is
- not only useful because it simplifies proofs. It is also required in
- order to use Isabelle's code generator to generate ML code
- from a function definition.
- Since the code generator only works with equations, it cannot be
- used with \isa{psimp} rules. Thus, in order to generate code for
- partial functions, they must be defined as a tail recursion.
- Luckily, many functions have a relatively natural tail recursive
- definition.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Nested recursion%
}
\isamarkuptrue%
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Feb 28 15:06:55 2011 +0000
@@ -444,7 +444,7 @@
;
equations: (thmdecl? prop + '|')
;
- functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
+ functionopts: '(' (('sequential' | 'domintros') + ',') ')'
;
'termination' ( term )?
\end{rail}
@@ -515,14 +515,6 @@
introduction rules for the domain predicate. While mostly not
needed, they can be helpful in some proofs about partial functions.
- \item @{text tailrec} generates the unconstrained recursive
- equations even without a termination proof, provided that the
- function is tail-recursive. This currently only works
-
- \item @{text "default d"} allows to specify a default value for a
- (partial) function, which will ensure that @{text "f x = d x"}
- whenever @{text "x \<notin> f_dom"}.
-
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Feb 28 15:06:36 2011 +0000
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Feb 28 15:06:55 2011 +0000
@@ -454,7 +454,7 @@
;
equations: (thmdecl? prop + '|')
;
- functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
+ functionopts: '(' (('sequential' | 'domintros') + ',') ')'
;
'termination' ( term )?
\end{rail}
@@ -523,14 +523,6 @@
introduction rules for the domain predicate. While mostly not
needed, they can be helpful in some proofs about partial functions.
- \item \isa{tailrec} generates the unconstrained recursive
- equations even without a termination proof, provided that the
- function is tail-recursive. This currently only works
-
- \item \isa{{\isaliteral{22}{\isachardoublequote}}default\ d{\isaliteral{22}{\isachardoublequote}}} allows to specify a default value for a
- (partial) function, which will ensure that \isa{{\isaliteral{22}{\isachardoublequote}}f\ x\ {\isaliteral{3D}{\isacharequal}}\ d\ x{\isaliteral{22}{\isachardoublequote}}}
- whenever \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f{\isaliteral{5F}{\isacharunderscore}}dom{\isaliteral{22}{\isachardoublequote}}}.
-
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Decision_Procs/DP_Library.thy Mon Feb 28 15:06:55 2011 +0000
@@ -0,0 +1,36 @@
+theory DP_Library
+imports Main
+begin
+
+primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
+ "alluopairs [] = []"
+| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
+
+lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
+by (induct xs, auto)
+
+lemma alluopairs_set:
+ "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "
+by (induct xs, auto)
+
+lemma alluopairs_bex:
+ assumes Pc: "\<forall> x \<in> set xs. \<forall>y\<in> set xs. P x y = P y x"
+ shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
+proof
+ assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"
+ then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y" by blast
+ from alluopairs_set[OF x y] P Pc x y show"\<exists>(x, y)\<in>set (alluopairs xs). P x y"
+ by auto
+next
+ assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"
+ then obtain "x" and "y" where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+
+ from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast
+ with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
+qed
+
+lemma alluopairs_ex:
+ "\<forall> x y. P x y = P y x \<Longrightarrow>
+ (\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
+by(blast intro!: alluopairs_bex)
+
+end
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Feb 28 15:06:55 2011 +0000
@@ -277,10 +277,7 @@
end
(* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
-lemma dnf[no_atp]:
- "(P & (Q | R)) = ((P&Q) | (P&R))"
- "((Q | R) & P) = ((Q&P) | (R&P))"
- by blast+
+lemmas dnf[no_atp] = conj_disj_distribL conj_disj_distribR
lemmas weak_dnf_simps[no_atp] = simp_thms dnf
@@ -875,7 +872,7 @@
{isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss}
end
*}
-
+(*
lemma upper_bound_finite_set:
assumes fS: "finite S"
shows "\<exists>(a::'a::linorder). \<forall>x \<in> S. f x \<le> a"
@@ -927,7 +924,6 @@
hence ?thesis by blast}
ultimately show ?thesis by blast
qed
-
-
+*)
end
--- a/src/HOL/Decision_Procs/Ferrack.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Decision_Procs/Ferrack.thy Mon Feb 28 15:06:55 2011 +0000
@@ -3,48 +3,14 @@
*)
theory Ferrack
-imports Complex_Main Dense_Linear_Order "~~/src/HOL/Library/Efficient_Nat"
+imports Complex_Main Dense_Linear_Order DP_Library
+ "~~/src/HOL/Library/Efficient_Nat"
uses ("ferrack_tac.ML")
begin
section {* Quantifier elimination for @{text "\<real> (0, 1, +, <)"} *}
(*********************************************************************************)
- (* SOME GENERAL STUFF< HAS TO BE MOVED IN SOME LIB *)
- (*********************************************************************************)
-
-primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
- "alluopairs [] = []"
-| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
-
-lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
-by (induct xs, auto)
-
-lemma alluopairs_set:
- "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "
-by (induct xs, auto)
-
-lemma alluopairs_ex:
- assumes Pc: "\<forall> x y. P x y = P y x"
- shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
-proof
- assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"
- then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y" by blast
- from alluopairs_set[OF x y] P Pc show"\<exists>(x, y)\<in>set (alluopairs xs). P x y"
- by auto
-next
- assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"
- then obtain "x" and "y" where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+
- from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast
- with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
-qed
-
-lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
-using Nat.gr0_conv_Suc
-by clarsimp
-
-
- (*********************************************************************************)
(**** SHADOW SYNTAX AND SEMANTICS ****)
(*********************************************************************************)
@@ -240,7 +206,7 @@
assumes nb: "numbound0 a"
shows "Inum (b#bs) a = Inum (b'#bs) a"
using nb
-by (induct a) (simp_all add: nth_pos2)
+by (induct a) simp_all
primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
"bound0 T = True"
@@ -263,7 +229,7 @@
assumes bp: "bound0 p"
shows "Ifm (b#bs) p = Ifm (b'#bs) p"
using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
-by (induct p) (auto simp add: nth_pos2)
+by (induct p) auto
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
by (cases p, auto)
@@ -316,12 +282,12 @@
lemma decrnum: assumes nb: "numbound0 t"
shows "Inum (x#bs) t = Inum bs (decrnum t)"
- using nb by (induct t rule: decrnum.induct, simp_all add: nth_pos2)
+ using nb by (induct t rule: decrnum.induct, simp_all)
lemma decr: assumes nb: "bound0 p"
shows "Ifm (x#bs) p = Ifm bs (decr p)"
using nb
- by (induct p rule: decr.induct, simp_all add: nth_pos2 decrnum)
+ by (induct p rule: decr.induct, simp_all add: decrnum)
lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
by (induct p, simp_all)
@@ -1420,7 +1386,7 @@
also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
-qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2)
+qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"])
lemma uset_l:
assumes lp: "isrlfm p"
@@ -1436,7 +1402,7 @@
proof-
have "\<exists> (s,m) \<in> set (uset p). real m * x \<ge> Inum (a#bs) s " (is "\<exists> (s,m) \<in> ?U p. real m *x \<ge> ?N a s")
using lp nmi ex
- by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2)
+ by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
then obtain s m where smU: "(s,m) \<in> set (uset p)" and mx: "real m * x \<ge> ?N a s" by blast
from uset_l[OF lp] smU have mp: "real m > 0" by auto
from pos_divide_le_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \<ge> ?N a s / real m"
@@ -1452,7 +1418,7 @@
proof-
have "\<exists> (s,m) \<in> set (uset p). real m * x \<le> Inum (a#bs) s " (is "\<exists> (s,m) \<in> ?U p. real m *x \<le> ?N a s")
using lp nmi ex
- by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2)
+ by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
then obtain s m where smU: "(s,m) \<in> set (uset p)" and mx: "real m * x \<le> ?N a s" by blast
from uset_l[OF lp] smU have mp: "real m > 0" by auto
from pos_le_divide_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \<le> ?N a s / real m"
@@ -1563,7 +1529,7 @@
hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps)
thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"]
by (simp add: algebra_simps)
-qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
+qed (auto simp add: numbound0_I[where bs="bs" and b="y" and b'="x"])
lemma finite_set_intervals:
assumes px: "P (x::real)"
@@ -1600,20 +1566,6 @@
from ainS binS noy ax xb px show ?thesis by blast
qed
-lemma finite_set_intervals2:
- assumes px: "P (x::real)"
- and lx: "l \<le> x" and xu: "x \<le> u"
- and linS: "l\<in> S" and uinS: "u \<in> S"
- and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
- shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < b \<and> P x)"
-proof-
- from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
- obtain a and b where
- as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S" and axb: "a \<le> x \<and> x \<le> b \<and> P x" by auto
- from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by auto
- thus ?thesis using px as bs noS by blast
-qed
-
lemma rinf_uset:
assumes lp: "isrlfm p"
and nmi: "\<not> (Ifm (x#bs) (minusinf p))" (is "\<not> (Ifm (x#bs) (?M p))")
--- a/src/HOL/Decision_Procs/MIR.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Decision_Procs/MIR.thy Mon Feb 28 15:06:55 2011 +0000
@@ -3,7 +3,8 @@
*)
theory MIR
-imports Complex_Main Dense_Linear_Order "~~/src/HOL/Library/Efficient_Nat"
+imports Complex_Main Dense_Linear_Order DP_Library
+ "~~/src/HOL/Library/Efficient_Nat"
uses ("mir_tac.ML")
begin
@@ -11,57 +12,13 @@
declare real_of_int_floor_cancel [simp del]
-primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
- "alluopairs [] = []"
-| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
-
-lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
-by (induct xs, auto)
-
-lemma alluopairs_set:
- "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "
-by (induct xs, auto)
-
-lemma alluopairs_ex:
- assumes Pc: "\<forall> x y. P x y = P y x"
- shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
-proof
- assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"
- then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y" by blast
- from alluopairs_set[OF x y] P Pc show"\<exists>(x, y)\<in>set (alluopairs xs). P x y"
- by auto
-next
- assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"
- then obtain "x" and "y" where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+
- from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast
- with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
-qed
-
-lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
-using Nat.gr0_conv_Suc
-by clarsimp
-
-
-lemma myl: "\<forall> (a::'a::{ordered_ab_group_add}) (b::'a). (a \<le> b) = (0 \<le> b - a)"
-proof(clarify)
- fix x y ::"'a"
- have "(x \<le> y) = (x - y \<le> 0)" by (simp only: le_iff_diff_le_0[where a="x" and b="y"])
- also have "\<dots> = (- (y - x) \<le> 0)" by simp
- also have "\<dots> = (0 \<le> y - x)" by (simp only: neg_le_0_iff_le[where a="y-x"])
- finally show "(x \<le> y) = (0 \<le> y - x)" .
-qed
-
-lemma myless: "\<forall> (a::'a::{ordered_ab_group_add}) (b::'a). (a < b) = (0 < b - a)"
-proof(clarify)
- fix x y ::"'a"
- have "(x < y) = (x - y < 0)" by (simp only: less_iff_diff_less_0[where a="x" and b="y"])
- also have "\<dots> = (- (y - x) < 0)" by simp
- also have "\<dots> = (0 < y - x)" by (simp only: neg_less_0_iff_less[where a="y-x"])
- finally show "(x < y) = (0 < y - x)" .
-qed
-
-lemma myeq: "\<forall> (a::'a::{ordered_ab_group_add}) (b::'a). (a = b) = (0 = b - a)"
- by auto
+lemma myle: fixes a b :: "'a::{ordered_ab_group_add}"
+ shows "(a \<le> b) = (0 \<le> b - a)"
+by (metis add_0_left add_le_cancel_right diff_add_cancel)
+
+lemma myless: fixes a b :: "'a::{ordered_ab_group_add}"
+ shows "(a < b) = (0 < b - a)"
+by (metis le_iff_diff_le_0 less_le_not_le myle)
(* Maybe should be added to the library \<dots> *)
lemma floor_int_eq: "(real n\<le> x \<and> x < real (n+1)) = (floor x = n)"
@@ -144,15 +101,6 @@
shows "(real (n::int) * real (k::int) rdvd x * real k) = (real n rdvd x)"
using knz by (simp add:rdvd_def)
-lemma rdvd_trans: assumes mn:"m rdvd n" and nk:"n rdvd k"
- shows "m rdvd k"
-proof-
- from rdvd_def mn obtain c where nmc:"n = m * real (c::int)" by auto
- from rdvd_def nk obtain c' where nkc:"k = n * real (c'::int)" by auto
- hence "k = m * real (c * c')" using nmc by simp
- thus ?thesis using rdvd_def by blast
-qed
-
(*********************************************************************************)
(**** SHADOW SYNTAX AND SEMANTICS ****)
(*********************************************************************************)
@@ -335,7 +283,7 @@
lemma numbound0_I:
assumes nb: "numbound0 a"
shows "Inum (b#bs) a = Inum (b'#bs) a"
- using nb by (induct a) (auto simp add: nth_pos2)
+ using nb by (induct a) auto
lemma numbound0_gen:
assumes nb: "numbound0 t" and ti: "isint t (x#bs)"
@@ -371,7 +319,7 @@
assumes bp: "bound0 p"
shows "Ifm (b#bs) p = Ifm (b'#bs) p"
using bp numbound0_I [where b="b" and bs="bs" and b'="b'"]
- by (induct p) (auto simp add: nth_pos2)
+ by (induct p) auto
primrec numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *) where
"numsubst0 t (C c) = (C c)"
@@ -386,12 +334,7 @@
lemma numsubst0_I:
shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
- by (induct t) (simp_all add: nth_pos2)
-
-lemma numsubst0_I':
- assumes nb: "numbound0 a"
- shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
- by (induct t) (simp_all add: nth_pos2 numbound0_I[OF nb, where b="b" and b'="b'"])
+ by (induct t) simp_all
primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where
"subst0 t T = T"
@@ -413,7 +356,7 @@
lemma subst0_I: assumes qfp: "qfree p"
shows "Ifm (b#bs) (subst0 a p) = Ifm ((Inum (b#bs) a)#bs) p"
using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
- by (induct p) (simp_all add: nth_pos2 )
+ by (induct p) simp_all
fun decrnum:: "num \<Rightarrow> num" where
"decrnum (Bound n) = Bound (n - 1)"
@@ -444,12 +387,12 @@
lemma decrnum: assumes nb: "numbound0 t"
shows "Inum (x#bs) t = Inum bs (decrnum t)"
- using nb by (induct t rule: decrnum.induct, simp_all add: nth_pos2)
+ using nb by (induct t rule: decrnum.induct, simp_all)
lemma decr: assumes nb: "bound0 p"
shows "Ifm (x#bs) p = Ifm bs (decr p)"
using nb
- by (induct p rule: decr.induct, simp_all add: nth_pos2 decrnum)
+ by (induct p rule: decr.induct, simp_all add: decrnum)
lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
by (induct p, simp_all)
@@ -513,24 +456,9 @@
| "conjuncts T = []"
| "conjuncts p = [p]"
-lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm bs q) = Ifm bs p"
-by(induct p rule: disjuncts.induct, auto)
lemma conjuncts: "(\<forall> q\<in> set (conjuncts p). Ifm bs q) = Ifm bs p"
by(induct p rule: conjuncts.induct, auto)
-lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). bound0 q"
-proof-
- assume nb: "bound0 p"
- hence "list_all bound0 (disjuncts p)" by (induct p rule:disjuncts.induct,auto)
- thus ?thesis by (simp only: list_all_iff)
-qed
-lemma conjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (conjuncts p). bound0 q"
-proof-
- assume nb: "bound0 p"
- hence "list_all bound0 (conjuncts p)" by (induct p rule:conjuncts.induct,auto)
- thus ?thesis by (simp only: list_all_iff)
-qed
-
lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q"
proof-
assume qf: "qfree p"
@@ -652,9 +580,6 @@
declare dvd_trans [trans add]
-lemma natabs0: "(nat (abs x) = 0) = (x = 0)"
-by arith
-
lemma numgcd0:
assumes g0: "numgcd t = 0"
shows "Inum bs t = 0"
@@ -1138,8 +1063,6 @@
by (cases "p=F \<or> q=T",simp_all add: imp_def)
lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def)
-lemma imp_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"
- using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def)
definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
"iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else
@@ -1150,8 +1073,6 @@
(cases "not p= q", auto simp add:not)
lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
by (unfold iff_def,cases "p=q", auto)
-lemma iff_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"
-using iff_def by (unfold iff_def,cases "p=q", auto)
fun check_int:: "num \<Rightarrow> bool" where
"check_int (C i) = True"
@@ -1657,8 +1578,6 @@
using conj_def by (cases p,auto)
lemma disj_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm q bs \<Longrightarrow> iszlfm (disj p q) bs"
using disj_def by (cases p,auto)
-lemma not_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm (not p) bs"
- by (induct p rule:iszlfm.induct ,auto)
recdef zlfm "measure fmsize"
"zlfm (And p q) = conj (zlfm p) (zlfm q)"
@@ -1739,7 +1658,7 @@
"(real (a::int) + b > 0) = (real a + real (floor b) > 0 \<or> (real a + real (floor b) = 0 \<and> real (floor b) - b < 0))"
proof-
have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith
- show ?thesis using myless[rule_format, where b="real (floor b)"]
+ show ?thesis using myless[of _ "real (floor b)"]
by (simp only:th split_int_less_real'[where a="-a" and b="-b"])
(simp add: algebra_simps diff_minus[symmetric],arith)
qed
@@ -2291,7 +2210,7 @@
by blast
thus "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e" using rdvd_def by simp
qed
-qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="real(x - k*d)" and b'="real x"] simp del: real_of_int_mult real_of_int_diff)
+qed (auto simp add: numbound0_I[where bs="bs" and b="real(x - k*d)" and b'="real x"] simp del: real_of_int_mult real_of_int_diff)
lemma minusinf_ex:
assumes lin: "iszlfm p (real (a::int) #bs)"
@@ -2428,7 +2347,7 @@
from prems th show ?case
by (simp add: algebra_simps
numbound0_I[where bs="bs" and b'="real x" and b="- real x"])
-qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"] nth_pos2)
+qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"])
lemma mirror_l: "iszlfm p (a#bs) \<Longrightarrow> iszlfm (mirror p) (a#bs)"
by (induct p rule: mirror.induct, auto simp add: isint_neg)
@@ -2636,7 +2555,7 @@
using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp
also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp
finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] rdvd_def be isint_Mul[OF ei] mult_strict_mono[OF ldcp jp ldcp ] by simp
-qed (simp_all add: nth_pos2 numbound0_I[where bs="bs" and b="real (l * x)" and b'="real x"] isint_Mul del: real_of_int_mult)
+qed (simp_all add: numbound0_I[where bs="bs" and b="real (l * x)" and b'="real x"] isint_Mul del: real_of_int_mult)
lemma a\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d\<beta> p l" and lp: "l>0"
shows "(\<exists> x. l dvd x \<and> Ifm (real x #bs) (a\<beta> p l)) = (\<exists> (x::int). Ifm (real x#bs) p)"
@@ -2780,7 +2699,7 @@
also have "\<dots> = (\<not> real j rdvd real x - real d + ?e)"
using ie by simp
finally show ?case using numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] c1 p by simp
-qed (auto simp add: numbound0_I[where bs="bs" and b="real (x - d)" and b'="real x"] nth_pos2 simp del: real_of_int_diff)
+qed (auto simp add: numbound0_I[where bs="bs" and b="real (x - d)" and b'="real x"] simp del: real_of_int_diff)
lemma \<beta>':
assumes lp: "iszlfm p (a #bs)"
@@ -2900,27 +2819,6 @@
(* Simulates normal substituion by modifying the formula see correctness theorem *)
-recdef a\<rho> "measure size"
- "a\<rho> (And p q) = (\<lambda> k. And (a\<rho> p k) (a\<rho> q k))"
- "a\<rho> (Or p q) = (\<lambda> k. Or (a\<rho> p k) (a\<rho> q k))"
- "a\<rho> (Eq (CN 0 c e)) = (\<lambda> k. if k dvd c then (Eq (CN 0 (c div k) e))
- else (Eq (CN 0 c (Mul k e))))"
- "a\<rho> (NEq (CN 0 c e)) = (\<lambda> k. if k dvd c then (NEq (CN 0 (c div k) e))
- else (NEq (CN 0 c (Mul k e))))"
- "a\<rho> (Lt (CN 0 c e)) = (\<lambda> k. if k dvd c then (Lt (CN 0 (c div k) e))
- else (Lt (CN 0 c (Mul k e))))"
- "a\<rho> (Le (CN 0 c e)) = (\<lambda> k. if k dvd c then (Le (CN 0 (c div k) e))
- else (Le (CN 0 c (Mul k e))))"
- "a\<rho> (Gt (CN 0 c e)) = (\<lambda> k. if k dvd c then (Gt (CN 0 (c div k) e))
- else (Gt (CN 0 c (Mul k e))))"
- "a\<rho> (Ge (CN 0 c e)) = (\<lambda> k. if k dvd c then (Ge (CN 0 (c div k) e))
- else (Ge (CN 0 c (Mul k e))))"
- "a\<rho> (Dvd i (CN 0 c e)) = (\<lambda> k. if k dvd c then (Dvd i (CN 0 (c div k) e))
- else (Dvd (i*k) (CN 0 c (Mul k e))))"
- "a\<rho> (NDvd i (CN 0 c e)) = (\<lambda> k. if k dvd c then (NDvd i (CN 0 (c div k) e))
- else (NDvd (i*k) (CN 0 c (Mul k e))))"
- "a\<rho> p = (\<lambda> k. p)"
-
definition \<sigma> :: "fm \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where
"\<sigma> p k t \<equiv> And (Dvd k t) (\<sigma>\<rho> p (t,k))"
@@ -3108,110 +3006,8 @@
by (simp add: ti)
finally have ?case . }
ultimately show ?case by blast
-qed (simp_all add: nth_pos2 bound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"] numbound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"])
-
-
-lemma a\<rho>:
- assumes lp: "iszlfm p (real (x::int)#bs)" and kp: "real k > 0"
- shows "Ifm (real (x*k)#bs) (a\<rho> p k) = Ifm (real x#bs) p" (is "?I (x*k) (?f p k) = ?I x p")
-using lp bound0_I[where bs="bs" and b="real (x*k)" and b'="real x"] numbound0_I[where bs="bs" and b="real (x*k)" and b'="real x"]
-proof(induct p rule: a\<rho>.induct)
- case (3 c e)
- from prems have cp: "c > 0" and nb: "numbound0 e" by auto
- from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
- {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp }
- moreover
- {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}
- ultimately show ?case by blast
-next
- case (4 c e)
- from prems have cp: "c > 0" and nb: "numbound0 e" by auto
- from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
- {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp }
- moreover
- {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}
- ultimately show ?case by blast
-next
- case (5 c e)
- from prems have cp: "c > 0" and nb: "numbound0 e" by auto
- from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
- {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp }
- moreover
- {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_less_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}
- ultimately show ?case by blast
-next
- case (6 c e)
- from prems have cp: "c > 0" and nb: "numbound0 e" by auto
- from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
- {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp }
- moreover
- {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_le_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}
- ultimately show ?case by blast
-next
- case (7 c e)
- from prems have cp: "c > 0" and nb: "numbound0 e" by auto
- from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
- {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp }
- moreover
- {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_less_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}
- ultimately show ?case by blast
-next
- case (8 c e)
- from prems have cp: "c > 0" and nb: "numbound0 e" by auto
- from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
- {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp }
- moreover
- {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_le_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}
- ultimately show ?case by blast
-next
- case (9 i c e)
- from prems have cp: "c > 0" and nb: "numbound0 e" by auto
- from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
- {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp }
- moreover
- {assume "\<not> k dvd c"
- hence "Ifm (real (x*k)#bs) (a\<rho> (Dvd i (CN 0 c e)) k) =
- (real i * real k rdvd (real c * real x + Inum (real x#bs) e) * real k)"
- using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"]
- by (simp add: algebra_simps)
- also have "\<dots> = (Ifm (real x#bs) (Dvd i (CN 0 c e)))" by (simp add: rdvd_mult[OF knz, where n="i"])
- finally have ?case . }
- ultimately show ?case by blast
-next
- case (10 i c e)
- from prems have cp: "c > 0" and nb: "numbound0 e" by auto
- from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
- {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp }
- moreover
- {assume "\<not> k dvd c"
- hence "Ifm (real (x*k)#bs) (a\<rho> (NDvd i (CN 0 c e)) k) =
- (\<not> (real i * real k rdvd (real c * real x + Inum (real x#bs) e) * real k))"
- using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"]
- by (simp add: algebra_simps)
- also have "\<dots> = (Ifm (real x#bs) (NDvd i (CN 0 c e)))" by (simp add: rdvd_mult[OF knz, where n="i"])
- finally have ?case . }
- ultimately show ?case by blast
-qed (simp_all add: nth_pos2)
-
-lemma a\<rho>_ex:
- assumes lp: "iszlfm p (real (x::int)#bs)" and kp: "k > 0"
- shows "(\<exists> (x::int). real k rdvd real x \<and> Ifm (real x#bs) (a\<rho> p k)) =
- (\<exists> (x::int). Ifm (real x#bs) p)" (is "(\<exists> x. ?D x \<and> ?P' x) = (\<exists> x. ?P x)")
-proof-
- have "(\<exists> x. ?D x \<and> ?P' x) = (\<exists> x. k dvd x \<and> ?P' x)" using int_rdvd_iff by simp
- also have "\<dots> = (\<exists>x. ?P' (x*k))" using unity_coeff_ex[where P="?P'" and l="k", simplified]
- by (simp add: algebra_simps)
- also have "\<dots> = (\<exists> x. ?P x)" using a\<rho> iszlfm_gen[OF lp] kp by auto
- finally show ?thesis .
-qed
-
-lemma \<sigma>\<rho>': assumes lp: "iszlfm p (real (x::int)#bs)" and kp: "k > 0" and nb: "numbound0 t"
- shows "Ifm (real x#bs) (\<sigma>\<rho> p (t,k)) = Ifm ((Inum (real x#bs) t)#bs) (a\<rho> p k)"
-using lp
-by(induct p rule: \<sigma>\<rho>.induct, simp_all add:
- numbound0_I[OF nb, where bs="bs" and b="Inum (real x#bs) t" and b'="real x"]
- numbound0_I[where bs="bs" and b="Inum (real x#bs) t" and b'="real x"]
- bound0_I[where bs="bs" and b="Inum (real x#bs) t" and b'="real x"] nth_pos2 cong: imp_cong)
+qed (simp_all add: bound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"] numbound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"])
+
lemma \<sigma>\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t"
shows "bound0 (\<sigma>\<rho> p (t,k))"
@@ -3229,20 +3025,6 @@
using lp isint_add [OF isint_c[where j="- 1"],where bs="real i#bs"]
by (induct p rule: \<alpha>\<rho>.induct, auto)
-lemma zminusinf_\<rho>:
- assumes lp: "iszlfm p (real (i::int)#bs)"
- and nmi: "\<not> (Ifm (real i#bs) (minusinf p))" (is "\<not> (Ifm (real i#bs) (?M p))")
- and ex: "Ifm (real i#bs) p" (is "?I i p")
- shows "\<exists> (e,c) \<in> set (\<rho> p). real (c*i) > Inum (real i#bs) e" (is "\<exists> (e,c) \<in> ?R p. real (c*i) > ?N i e")
- using lp nmi ex
-by (induct p rule: minusinf.induct, auto)
-
-
-lemma \<sigma>_And: "Ifm bs (\<sigma> (And p q) k t) = Ifm bs (And (\<sigma> p k t) (\<sigma> q k t))"
-using \<sigma>_def by auto
-lemma \<sigma>_Or: "Ifm bs (\<sigma> (Or p q) k t) = Ifm bs (Or (\<sigma> p k t) (\<sigma> q k t))"
-using \<sigma>_def by auto
-
lemma \<rho>: assumes lp: "iszlfm p (real (i::int) #bs)"
and pi: "Ifm (real i#bs) p"
and d: "d\<delta> p d"
@@ -3374,7 +3156,7 @@
finally show ?case
using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p
by (simp add: algebra_simps)
-qed(auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] nth_pos2)
+qed(auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"])
lemma \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t"
shows "bound0 (\<sigma> p k t)"
@@ -3511,8 +3293,6 @@
by pat_completeness auto
termination by (relation "measure num_size") auto
-lemma not_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm (not p)"
- by (induct p rule: isrlfm.induct, auto)
lemma conj_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (conj p q)"
using conj_def by (cases p, auto)
lemma disj_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (disj p q)"
@@ -3760,7 +3540,7 @@
from real_in_int_intervals th have "\<exists> j\<in> {0 .. n}. real j \<le> real n *x + ?N s - ?N (Floor s)\<and> real n *x + ?N s - ?N (Floor s) < real (j+1)" by simp
hence "\<exists> j\<in> {0 .. n}. 0 \<le> real n *x + ?N s - ?N (Floor s) - real j \<and> real n *x + ?N s - ?N (Floor s) - real (j+1) < 0"
- by(simp only: myl[rule_format, where b="real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"])
+ by(simp only: myle[of _ "real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"])
hence "\<exists> j\<in> {0.. n}. ?I (?p (p,n,s) j)"
using pns by (simp add: fp_def np algebra_simps numsub numadd)
then obtain "j" where j_def: "j\<in> {0 .. n} \<and> ?I (?p (p,n,s) j)" by blast
@@ -3787,7 +3567,7 @@
from real_in_int_intervals th have "\<exists> j\<in> {n .. 0}. real j \<le> real n *x + ?N s - ?N (Floor s)\<and> real n *x + ?N s - ?N (Floor s) < real (j+1)" by simp
hence "\<exists> j\<in> {n .. 0}. 0 \<le> real n *x + ?N s - ?N (Floor s) - real j \<and> real n *x + ?N s - ?N (Floor s) - real (j+1) < 0"
- by(simp only: myl[rule_format, where b="real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"])
+ by(simp only: myle[of _ "real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"])
hence "\<exists> j\<in> {n .. 0}. 0 \<ge> - (real n *x + ?N s - ?N (Floor s) - real j) \<and> - (real n *x + ?N s - ?N (Floor s) - real (j+1)) > 0" by (simp only: th1[rule_format] th2[rule_format])
hence "\<exists> j\<in> {n.. 0}. ?I (?p (p,n,s) j)"
using pns by (simp add: fp_def nn diff_minus add_ac mult_ac numfloor numadd numneg
@@ -3885,7 +3665,7 @@
fix a n s
assume H: "?N a = ?N (CN 0 n s)"
show "?I (lt n s) = ?I (Lt a)" using H by (cases "n=0", (simp add: lt_def))
- (cases "n > 0", simp_all add: lt_def algebra_simps myless[rule_format, where b="0"])
+ (cases "n > 0", simp_all add: lt_def algebra_simps myless[of _ "0"])
qed
lemma lt_l: "isrlfm (rsplit lt a)"
@@ -3897,7 +3677,7 @@
fix a n s
assume H: "?N a = ?N (CN 0 n s)"
show "?I (le n s) = ?I (Le a)" using H by (cases "n=0", (simp add: le_def))
- (cases "n > 0", simp_all add: le_def algebra_simps myl[rule_format, where b="0"])
+ (cases "n > 0", simp_all add: le_def algebra_simps myle[of _ "0"])
qed
lemma le_l: "isrlfm (rsplit le a)"
@@ -3909,7 +3689,7 @@
fix a n s
assume H: "?N a = ?N (CN 0 n s)"
show "?I (gt n s) = ?I (Gt a)" using H by (cases "n=0", (simp add: gt_def))
- (cases "n > 0", simp_all add: gt_def algebra_simps myless[rule_format, where b="0"])
+ (cases "n > 0", simp_all add: gt_def algebra_simps myless[of _ "0"])
qed
lemma gt_l: "isrlfm (rsplit gt a)"
by (rule rsplit_l[where f="gt" and a="a"], auto simp add: gt_def)
@@ -3920,7 +3700,7 @@
fix a n s
assume H: "?N a = ?N (CN 0 n s)"
show "?I (ge n s) = ?I (Ge a)" using H by (cases "n=0", (simp add: ge_def))
- (cases "n > 0", simp_all add: ge_def algebra_simps myl[rule_format, where b="0"])
+ (cases "n > 0", simp_all add: ge_def algebra_simps myle[of _ "0"])
qed
lemma ge_l: "isrlfm (rsplit ge a)"
by (rule rsplit_l[where f="ge" and a="a"], auto simp add: ge_def)
@@ -3962,9 +3742,9 @@
shows "(real (i::int) rdvd real (n::int) * u - s) = (\<exists> j\<in> {0 .. n - 1}. real n * u = s - real (floor s) + real j \<and> real i rdvd real (j - floor s))" (is "?lhs = ?rhs")
proof-
let ?ss = "s - real (floor s)"
- from real_of_int_floor_add_one_gt[where r="s", simplified myless[rule_format,where a="s"]]
+ from real_of_int_floor_add_one_gt[where r="s", simplified myless[of "s"]]
real_of_int_floor_le[where r="s"] have ss0:"?ss \<ge> 0" and ss1:"?ss < 1"
- by (auto simp add: myl[rule_format, where b="s", symmetric] myless[rule_format, where a="?ss"])
+ by (auto simp add: myle[of _ "s", symmetric] myless[of "?ss"])
from np have n0: "real n \<ge> 0" by simp
from mult_left_mono[OF up n0] mult_strict_left_mono[OF u1 np]
have nu0:"real n * u - s \<ge> -s" and nun:"real n * u -s < real n - s" by auto
@@ -4141,12 +3921,6 @@
lemma bound0at_l : "\<lbrakk>isatom p ; bound0 p\<rbrakk> \<Longrightarrow> isrlfm p"
by (induct p rule: isrlfm.induct, auto)
-lemma zgcd_le1: assumes ip: "(0::int) < i" shows "gcd i j \<le> i"
-proof-
- from gcd_dvd1_int have th: "gcd i j dvd i" by blast
- from zdvd_imp_le[OF th ip] show ?thesis .
-qed
-
lemma simpfm_rl: "isrlfm p \<Longrightarrow> isrlfm (simpfm p)"
proof (induct p)
@@ -4165,7 +3939,7 @@
with numgcd_pos[where t="CN 0 c (simpnum e)"]
have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
- by (simp add: numgcd_def zgcd_le1)
+ by (simp add: numgcd_def)
from prems have th': "c\<noteq>0" by auto
from prems have cp: "c \<ge> 0" by simp
from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
@@ -4190,7 +3964,7 @@
with numgcd_pos[where t="CN 0 c (simpnum e)"]
have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
- by (simp add: numgcd_def zgcd_le1)
+ by (simp add: numgcd_def)
from prems have th': "c\<noteq>0" by auto
from prems have cp: "c \<ge> 0" by simp
from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
@@ -4215,7 +3989,7 @@
with numgcd_pos[where t="CN 0 c (simpnum e)"]
have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
- by (simp add: numgcd_def zgcd_le1)
+ by (simp add: numgcd_def)
from prems have th': "c\<noteq>0" by auto
from prems have cp: "c \<ge> 0" by simp
from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
@@ -4240,7 +4014,7 @@
with numgcd_pos[where t="CN 0 c (simpnum e)"]
have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
- by (simp add: numgcd_def zgcd_le1)
+ by (simp add: numgcd_def)
from prems have th': "c\<noteq>0" by auto
from prems have cp: "c \<ge> 0" by simp
from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
@@ -4265,7 +4039,7 @@
with numgcd_pos[where t="CN 0 c (simpnum e)"]
have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
- by (simp add: numgcd_def zgcd_le1)
+ by (simp add: numgcd_def)
from prems have th': "c\<noteq>0" by auto
from prems have cp: "c \<ge> 0" by simp
from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
@@ -4290,7 +4064,7 @@
with numgcd_pos[where t="CN 0 c (simpnum e)"]
have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
- by (simp add: numgcd_def zgcd_le1)
+ by (simp add: numgcd_def)
from prems have th': "c\<noteq>0" by auto
from prems have cp: "c \<ge> 0" by simp
from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
@@ -4674,7 +4448,7 @@
also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
-qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2)
+qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"])
lemma \<Upsilon>_l:
assumes lp: "isrlfm p"
@@ -4690,7 +4464,7 @@
proof-
have "\<exists> (s,m) \<in> set (\<Upsilon> p). real m * x \<ge> Inum (a#bs) s " (is "\<exists> (s,m) \<in> ?U p. real m *x \<ge> ?N a s")
using lp nmi ex
- by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2)
+ by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
then obtain s m where smU: "(s,m) \<in> set (\<Upsilon> p)" and mx: "real m * x \<ge> ?N a s" by blast
from \<Upsilon>_l[OF lp] smU have mp: "real m > 0" by auto
from pos_divide_le_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \<ge> ?N a s / real m"
@@ -4706,7 +4480,7 @@
proof-
have "\<exists> (s,m) \<in> set (\<Upsilon> p). real m * x \<le> Inum (a#bs) s " (is "\<exists> (s,m) \<in> ?U p. real m *x \<le> ?N a s")
using lp nmi ex
- by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2)
+ by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
then obtain s m where smU: "(s,m) \<in> set (\<Upsilon> p)" and mx: "real m * x \<le> ?N a s" by blast
from \<Upsilon>_l[OF lp] smU have mp: "real m > 0" by auto
from pos_le_divide_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \<le> ?N a s / real m"
@@ -4817,56 +4591,7 @@
hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps)
thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"]
by (simp add: algebra_simps)
-qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
-
-lemma finite_set_intervals:
- assumes px: "P (x::real)"
- and lx: "l \<le> x" and xu: "x \<le> u"
- and linS: "l\<in> S" and uinS: "u \<in> S"
- and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
- shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a \<le> x \<and> x \<le> b \<and> P x"
-proof-
- let ?Mx = "{y. y\<in> S \<and> y \<le> x}"
- let ?xM = "{y. y\<in> S \<and> x \<le> y}"
- let ?a = "Max ?Mx"
- let ?b = "Min ?xM"
- have MxS: "?Mx \<subseteq> S" by blast
- hence fMx: "finite ?Mx" using fS finite_subset by auto
- from lx linS have linMx: "l \<in> ?Mx" by blast
- hence Mxne: "?Mx \<noteq> {}" by blast
- have xMS: "?xM \<subseteq> S" by blast
- hence fxM: "finite ?xM" using fS finite_subset by auto
- from xu uinS have linxM: "u \<in> ?xM" by blast
- hence xMne: "?xM \<noteq> {}" by blast
- have ax:"?a \<le> x" using Mxne fMx by auto
- have xb:"x \<le> ?b" using xMne fxM by auto
- have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast
- have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast
- have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
- proof(clarsimp)
- fix y
- assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"
- from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by auto
- moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by simp}
- moreover {assume "y \<in> ?xM" hence "y \<ge> ?b" using xMne fxM by auto with yb have "False" by simp}
- ultimately show "False" by blast
- qed
- from ainS binS noy ax xb px show ?thesis by blast
-qed
-
-lemma finite_set_intervals2:
- assumes px: "P (x::real)"
- and lx: "l \<le> x" and xu: "x \<le> u"
- and linS: "l\<in> S" and uinS: "u \<in> S"
- and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
- shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < b \<and> P x)"
-proof-
- from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
- obtain a and b where
- as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S" and axb: "a \<le> x \<and> x \<le> b \<and> P x" by auto
- from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by auto
- thus ?thesis using px as bs noS by blast
-qed
+qed (auto simp add: numbound0_I[where bs="bs" and b="y" and b'="x"])
lemma rinf_\<Upsilon>:
assumes lp: "isrlfm p"
@@ -5059,7 +4784,7 @@
shows "(Ifm bs (E p)) = (\<exists> (i::int). Ifm (real i#bs) (E (And (And (Ge(CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))) (exsplit p))))" (is "?lhs = ?rhs")
proof-
have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real i)#bs) (exsplit p))"
- by (simp add: myless[rule_format, where b="1"] myless[rule_format, where b="0"] add_ac diff_minus)
+ by (simp add: myless[of _ "1"] myless[of _ "0"] add_ac diff_minus)
also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real i + x) #bs) p)"
by (simp only: exsplit[OF qf] add_ac)
also have "\<dots> = (\<exists> x. Ifm (x#bs) p)"
@@ -5896,4 +5621,6 @@
apply mir
done
+unused_thms
+
end
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Feb 28 15:06:55 2011 +0000
@@ -5,9 +5,7 @@
header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
theory Parametric_Ferrante_Rackoff
-imports
- Reflected_Multivariate_Polynomial
- Dense_Linear_Order
+imports Reflected_Multivariate_Polynomial Dense_Linear_Order DP_Library
"~~/src/HOL/Library/Efficient_Nat"
begin
@@ -67,7 +65,7 @@
assumes nb: "tmbound0 a"
shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"
using nb
-by (induct a rule: tm.induct,auto simp add: nth_pos2)
+by (induct a rule: tm.induct,auto)
primrec tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *) where
"tmbound n (CP c) = True"
@@ -105,10 +103,10 @@
lemma decrtm0: assumes nb: "tmbound0 t"
shows "Itm vs (x#bs) t = Itm vs bs (decrtm0 t)"
- using nb by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
+ using nb by (induct t rule: decrtm0.induct, simp_all)
lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t"
- by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
+ by (induct t rule: decrtm0.induct, simp_all)
primrec decrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm" where
"decrtm m (CP c) = (CP c)"
@@ -175,10 +173,10 @@
| "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
lemma tmsubst0:
shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
- by (induct a rule: tm.induct) (auto simp add: nth_pos2)
+ by (induct a rule: tm.induct) auto
lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
- by (induct a rule: tm.induct) (auto simp add: nth_pos2)
+ by (induct a rule: tm.induct) auto
primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where
"tmsubst n t (CP c) = CP c"
@@ -193,7 +191,7 @@
lemma tmsubst: assumes nb: "tmboundslt (length bs) a" and nlt: "n \<le> length bs"
shows "Itm vs bs (tmsubst n t a) = Itm vs (bs[n:= Itm vs bs t]) a"
using nb nlt
-by (induct a rule: tm.induct,auto simp add: nth_pos2)
+by (induct a rule: tm.induct,auto)
lemma tmsubst_nb0: assumes tnb: "tmbound0 t"
shows "tmbound0 (tmsubst 0 t a)"
@@ -534,7 +532,7 @@
assumes bp: "bound0 p"
shows "Ifm vs (b#bs) p = Ifm vs (b'#bs) p"
using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
-by (induct p rule: bound0.induct,auto simp add: nth_pos2)
+by (induct p rule: bound0.induct,auto)
primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *) where
"bound m T = True"
@@ -1585,7 +1583,7 @@
proof-
have "\<exists> (c,s) \<in> set (uset p). (Ipoly vs c < 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s) \<or> (Ipoly vs c > 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s)"
using lp nmi ex
- apply (induct p rule: minusinf.induct, auto simp add: eq le lt nth_pos2 polyneg_norm)
+ apply (induct p rule: minusinf.induct, auto simp add: eq le lt polyneg_norm)
apply (auto simp add: linorder_not_less order_le_less)
done
then obtain c s where csU: "(c,s) \<in> set (uset p)" and x: "(Ipoly vs c < 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s) \<or> (Ipoly vs c > 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s)" by blast
@@ -1618,7 +1616,7 @@
proof-
have "\<exists> (c,s) \<in> set (uset p). (Ipoly vs c < 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s) \<or> (Ipoly vs c > 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s)"
using lp nmi ex
- apply (induct p rule: minusinf.induct, auto simp add: eq le lt nth_pos2 polyneg_norm)
+ apply (induct p rule: minusinf.induct, auto simp add: eq le lt polyneg_norm)
apply (auto simp add: linorder_not_less order_le_less)
done
then obtain c s where csU: "(c,s) \<in> set (uset p)" and x: "(Ipoly vs c < 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s) \<or> (Ipoly vs c > 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s)" by blast
@@ -1798,7 +1796,7 @@
from yne c eq_divide_eq[of "y" "- ?Nt x s" "?N c"] have ?case
by (simp add: field_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric]) }
ultimately show ?case by blast
-qed (auto simp add: nth_pos2 tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"] bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"])
+qed (auto simp add: tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"] bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"])
lemma one_plus_one_pos[simp]: "(1::'a::{linordered_field}) + 1 > 0"
proof-
@@ -2440,38 +2438,6 @@
from fr_eq[OF lp, of vs bs x, simplified th'] show ?thesis .
qed
-text {* Rest of the implementation *}
-
-primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
- "alluopairs [] = []"
-| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
-
-lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
-by (induct xs, auto)
-
-lemma alluopairs_set:
- "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "
-by (induct xs, auto)
-
-lemma alluopairs_ex:
- assumes Pc: "\<forall> x \<in> set xs. \<forall>y\<in> set xs. P x y = P y x"
- shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
-proof
- assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"
- then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y" by blast
- from alluopairs_set[OF x y] P Pc x y show"\<exists>(x, y)\<in>set (alluopairs xs). P x y"
- by auto
-next
- assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"
- then obtain "x" and "y" where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+
- from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast
- with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
-qed
-
-lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
-using Nat.gr0_conv_Suc
-by clarsimp
-
lemma simpfm_lin: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)
@@ -2520,7 +2486,7 @@
from decr0_qf[OF th1] have thqf: "qfree (ferrack p)" by (simp add: ferrack_def Let_def)
have "?lhs \<longleftrightarrow> (\<exists>x. Ifm vs (x#bs) ?q)" by simp
also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> (\<exists>(c, t)\<in>set ?U. \<exists>(d, s)\<in>set ?U. ?I (msubst (simpfm p) ((c, t), d, s)))" using fr_eq_msubst[OF lq, of vs bs x] by simp
- also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> (\<exists> (x,y) \<in> set ?Up. ?I ((simpfm o (msubst ?q)) (x,y)))" using alluopairs_ex[OF th0] by simp
+ also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> (\<exists> (x,y) \<in> set ?Up. ?I ((simpfm o (msubst ?q)) (x,y)))" using alluopairs_bex[OF th0] by simp
also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (evaldjf (simpfm o (msubst ?q)) ?Up)"
by (simp add: evaldjf_ex)
also have "\<dots> \<longleftrightarrow> ?I (disj ?mp (disj ?pp (evaldjf (simpfm o (msubst ?q)) ?Up)))" by simp
@@ -2861,7 +2827,7 @@
also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (subst0 (CP 0\<^sub>p) ?q) \<or> (\<exists>(n,t) \<in> set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \<or> (\<exists> x\<in>set ?U. \<exists> y \<in>set ?U. ?I (?s (x,y)))"
by (simp add: split_def)
also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (subst0 (CP 0\<^sub>p) ?q) \<or> (\<exists>(n,t) \<in> set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \<or> (\<exists> (x,y) \<in> set ?Up. ?I (?s (x,y)))"
- using alluopairs_ex[OF th0] by simp
+ using alluopairs_bex[OF th0] by simp
also have "\<dots> \<longleftrightarrow> ?I ?R"
by (simp add: list_disj_def evaldjf_ex split_def)
also have "\<dots> \<longleftrightarrow> ?rhs"
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Feb 28 15:06:55 2011 +0000
@@ -210,11 +210,6 @@
"poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
| "poly_deriv p = 0\<^sub>p"
- (* Verification *)
-lemma nth_pos2[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
-using Nat.gr0_conv_Suc
-by clarsimp
-
subsection{* Semantics of the polynomial representation *}
primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy Mon Feb 28 15:06:55 2011 +0000
@@ -83,11 +83,11 @@
lemma jth_n[simp]: "Fin n = #s ==> jth n (s ooo <a>) = a"
apply (simp add: jth_def, auto)
apply (simp add: i_th_def rt_sconc1)
-by (simp add: inat_defs split: inat_splits)
+by (simp add: inat_defs split: inat.splits)
lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a"
apply (simp add: last_def)
-apply (simp add: inat_defs split:inat_splits)
+apply (simp add: inat_defs split:inat.splits)
by (drule sym, auto)
lemma last_fsingleton[simp]: "last (<a>) = a"
@@ -103,7 +103,7 @@
by (simp add: last_def)
lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
-by (simp add: jth_def inat_defs split:inat_splits, auto)
+by (simp add: jth_def inat_defs split:inat.splits, auto)
lemma jth_UU[simp]:"jth n UU = undefined"
by (simp add: jth_def)
--- a/src/HOL/Hoare_Parallel/Graph.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Hoare_Parallel/Graph.thy Mon Feb 28 15:06:55 2011 +0000
@@ -140,11 +140,8 @@
apply simp
apply(subgoal_tac "(length path - Suc m) + nat \<le> length path")
prefer 2 apply arith
-apply(drule nth_drop)
-apply simp
apply(subgoal_tac "length path - Suc m + nat = length path - Suc 0")
prefer 2 apply arith
-apply simp
apply clarify
apply(case_tac "i")
apply(force simp add: nth_list_update)
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Mon Feb 28 15:06:55 2011 +0000
@@ -111,8 +111,6 @@
apply simp
apply clarify
apply simp
- apply(case_tac j,simp)
- apply simp
apply simp
apply(rule conjI)
apply clarify
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Mon Feb 28 15:06:55 2011 +0000
@@ -871,12 +871,8 @@
apply(simp add:comm_def)
apply clarify
apply(erule_tac x="Suc(length xs + i)" in allE,simp)
-apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift del:map.simps)
- apply(simp add:last_length)
- apply(erule mp)
- apply(case_tac "last xs")
- apply(simp add:lift_def)
-apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
+apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift last_conv_nth lift_def split_def)
+apply(simp add:Cons_lift_append nth_append snd_lift)
done
lemma While_sound_aux [rule_format]:
--- a/src/HOL/Hoare_Parallel/RG_Tran.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Hoare_Parallel/RG_Tran.thy Mon Feb 28 15:06:55 2011 +0000
@@ -130,8 +130,6 @@
lemma last_length: "((a#xs)!(length xs))=last (a#xs)"
apply simp
apply(induct xs,simp+)
-apply(case_tac xs)
-apply simp_all
done
lemma div_seq [rule_format]: "list \<in> cptn_mod \<Longrightarrow>
@@ -304,10 +302,10 @@
apply(erule CptnEnv)
apply(erule CptnComp,simp)
apply(rule CptnComp)
- apply(erule CondT,simp)
+ apply(erule CondT,simp)
apply(rule CptnComp)
- apply(erule CondF,simp)
---{* Seq1 *}
+ apply(erule CondF,simp)
+--{* Seq1 *}
apply(erule cptn.cases,simp_all)
apply(rule CptnOne)
apply clarify
@@ -332,37 +330,27 @@
apply(drule_tac P=P1 in lift_is_cptn)
apply(simp add:lift_def)
apply simp
-apply(case_tac "xs\<noteq>[]")
- apply(drule_tac P=P1 in last_lift)
- apply(rule last_fst_esp)
- apply (simp add:last_length)
- apply(simp add:Cons_lift del:map.simps)
- apply(rule conjI, clarify, simp)
- apply(case_tac "(((Some P0, s) # xs) ! length xs)")
- apply clarify
- apply (simp add:lift_def last_length)
-apply (simp add:last_length)
+apply(simp split: split_if_asm)
+apply(frule_tac P=P1 in last_lift)
+ apply(rule last_fst_esp)
+ apply (simp add:last_length)
+apply(simp add:Cons_lift lift_def split_def last_conv_nth)
--{* While1 *}
apply(rule CptnComp)
-apply(rule WhileT,simp)
+ apply(rule WhileT,simp)
apply(drule_tac P="While b P" in lift_is_cptn)
apply(simp add:lift_def)
--{* While2 *}
apply(rule CptnComp)
-apply(rule WhileT,simp)
+ apply(rule WhileT,simp)
apply(rule cptn_append_is_cptn)
-apply(drule_tac P="While b P" in lift_is_cptn)
+ apply(drule_tac P="While b P" in lift_is_cptn)
apply(simp add:lift_def)
apply simp
-apply(case_tac "xs\<noteq>[]")
- apply(drule_tac P="While b P" in last_lift)
- apply(rule last_fst_esp,simp add:last_length)
- apply(simp add:Cons_lift del:map.simps)
- apply(rule conjI, clarify, simp)
- apply(case_tac "(((Some P, s) # xs) ! length xs)")
- apply clarify
- apply (simp add:last_length lift_def)
-apply simp
+apply(simp split: split_if_asm)
+apply(frule_tac P="While b P" in last_lift)
+ apply(rule last_fst_esp,simp add:last_length)
+apply(simp add:Cons_lift lift_def split_def last_conv_nth)
done
theorem cptn_iff_cptn_mod: "(c \<in> cptn) = (c \<in> cptn_mod)"
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Mon Feb 28 15:06:55 2011 +0000
@@ -421,11 +421,6 @@
apply (induct xs arbitrary: a i j)
apply simp
apply simp
-apply (case_tac j)
-apply simp
-apply auto
-apply (case_tac nat)
-apply auto
done
(* suffices that j \<le> length xs and length ys *)
@@ -443,7 +438,6 @@
apply (case_tac i', auto)
apply (erule_tac x="Suc i'" in allE, auto)
apply (erule_tac x="i' - 1" in allE, auto)
- apply (case_tac i', auto)
apply (erule_tac x="Suc i'" in allE, auto)
done
qed
@@ -459,11 +453,9 @@
lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
apply (induct xs arbitrary: i j k)
-apply auto
+apply simp
apply (case_tac k)
apply auto
-apply (case_tac i)
-apply auto
done
lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
--- a/src/HOL/IsaMakefile Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/IsaMakefile Mon Feb 28 15:06:55 2011 +0000
@@ -1530,6 +1530,7 @@
HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
$(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
+ Library/Nat_Infinity.thy \
HOLCF/Library/Defl_Bifinite.thy \
HOLCF/Library/Bool_Discrete.thy \
HOLCF/Library/Char_Discrete.thy \
@@ -1563,7 +1564,6 @@
HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
- Library/Nat_Infinity.thy \
HOLCF/ex/Dagstuhl.thy \
HOLCF/ex/Dnat.thy \
HOLCF/ex/Domain_Proofs.thy \
@@ -1583,6 +1583,7 @@
HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF HOLCF/FOCUS/ROOT.ML \
+ Library/Nat_Infinity.thy \
HOLCF/Library/Stream.thy \
HOLCF/FOCUS/Fstreams.thy \
HOLCF/FOCUS/Fstream.thy \
--- a/src/HOL/Library/Nat_Infinity.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Library/Nat_Infinity.thy Mon Feb 28 15:06:55 2011 +0000
@@ -1,5 +1,6 @@
(* Title: HOL/Library/Nat_Infinity.thy
Author: David von Oheimb, TU Muenchen; Florian Haftmann, TU Muenchen
+ Contributions: David Trachtenherz, TU Muenchen
*)
header {* Natural numbers with infinity *}
@@ -31,6 +32,10 @@
by (cases x) auto
+primrec the_Fin :: "inat \<Rightarrow> nat"
+where "the_Fin (Fin n) = n"
+
+
subsection {* Constructors and numbers *}
instantiation inat :: "{zero, one, number}"
@@ -168,8 +173,16 @@
lemma plus_1_iSuc:
"1 + q = iSuc q"
"q + 1 = iSuc q"
- unfolding iSuc_plus_1 by (simp_all add: add_ac)
+by (simp_all add: iSuc_plus_1 add_ac)
+
+lemma iadd_Suc: "iSuc m + n = iSuc (m + n)"
+by (simp_all add: iSuc_plus_1 add_ac)
+lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)"
+by (simp only: add_commute[of m] iadd_Suc)
+
+lemma iadd_is_0: "(m + n = (0::inat)) = (m = 0 \<and> n = 0)"
+by (cases m, cases n, simp_all add: zero_inat_def)
subsection {* Multiplication *}
@@ -232,6 +245,56 @@
then show "inj (\<lambda>n. of_nat n :: inat)" by (simp add: of_nat_eq_Fin)
qed
+lemma imult_is_0[simp]: "((m::inat) * n = 0) = (m = 0 \<or> n = 0)"
+by(auto simp add: times_inat_def zero_inat_def split: inat.split)
+
+lemma imult_is_Infty: "((a::inat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
+by(auto simp add: times_inat_def zero_inat_def split: inat.split)
+
+
+subsection {* Subtraction *}
+
+instantiation inat :: minus
+begin
+
+definition diff_inat_def:
+"a - b = (case a of (Fin x) \<Rightarrow> (case b of (Fin y) \<Rightarrow> Fin (x - y) | \<infinity> \<Rightarrow> 0)
+ | \<infinity> \<Rightarrow> \<infinity>)"
+
+instance ..
+
+end
+
+lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)"
+by(simp add: diff_inat_def)
+
+lemma idiff_Infty[simp,code]: "\<infinity> - n = \<infinity>"
+by(simp add: diff_inat_def)
+
+lemma idiff_Infty_right[simp,code]: "Fin a - \<infinity> = 0"
+by(simp add: diff_inat_def)
+
+lemma idiff_0[simp]: "(0::inat) - n = 0"
+by (cases n, simp_all add: zero_inat_def)
+
+lemmas idiff_Fin_0[simp] = idiff_0[unfolded zero_inat_def]
+
+lemma idiff_0_right[simp]: "(n::inat) - 0 = n"
+by (cases n) (simp_all add: zero_inat_def)
+
+lemmas idiff_Fin_0_right[simp] = idiff_0_right[unfolded zero_inat_def]
+
+lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::inat) - n = 0"
+by(auto simp: zero_inat_def)
+
+lemma iSuc_minus_iSuc [simp]: "iSuc n - iSuc m = n - m"
+by(simp add: iSuc_def split: inat.split)
+
+lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n"
+by(simp add: one_inat_def iSuc_Fin[symmetric] zero_inat_def[symmetric])
+
+(*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_inat_def]*)
+
subsection {* Ordering *}
@@ -286,8 +349,8 @@
lemma i0_lb [simp]: "(0\<Colon>inat) \<le> n"
by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
-lemma i0_neq [simp]: "n \<le> (0\<Colon>inat) \<longleftrightarrow> n = 0"
- by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
+lemma ile0_eq [simp]: "n \<le> (0\<Colon>inat) \<longleftrightarrow> n = 0"
+by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m \<Longrightarrow> R"
by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
@@ -295,11 +358,11 @@
lemma Infty_ilessE [elim!]: "\<infinity> < Fin m \<Longrightarrow> R"
by simp
-lemma not_ilessi0 [simp]: "\<not> n < (0\<Colon>inat)"
+lemma not_iless0 [simp]: "\<not> n < (0\<Colon>inat)"
by (simp add: zero_inat_def less_inat_def split: inat.splits)
-lemma i0_eq [simp]: "(0\<Colon>inat) < n \<longleftrightarrow> n \<noteq> 0"
- by (simp add: zero_inat_def less_inat_def split: inat.splits)
+lemma i0_less [simp]: "(0\<Colon>inat) < n \<longleftrightarrow> n \<noteq> 0"
+by (simp add: zero_inat_def less_inat_def split: inat.splits)
lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m \<longleftrightarrow> n \<le> m"
by (simp add: iSuc_def less_eq_inat_def split: inat.splits)
@@ -316,6 +379,9 @@
lemma i0_iless_iSuc [simp]: "0 < iSuc n"
by (simp add: zero_inat_def iSuc_def less_inat_def split: inat.splits)
+lemma iless_iSuc0[simp]: "(n < iSuc 0) = (n = 0)"
+by (simp add: zero_inat_def iSuc_def less_inat_def split: inat.split)
+
lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
by (simp add: iSuc_def less_eq_inat_def less_inat_def split: inat.splits)
@@ -325,6 +391,19 @@
lemma iless_Suc_eq [simp]: "Fin m < iSuc n \<longleftrightarrow> Fin m \<le> n"
by (auto simp add: iSuc_def less_inat_def split: inat.splits)
+lemma imult_Infty: "(0::inat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
+by (simp add: zero_inat_def less_inat_def split: inat.splits)
+
+lemma imult_Infty_right: "(0::inat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
+by (simp add: zero_inat_def less_inat_def split: inat.splits)
+
+lemma inat_0_less_mult_iff: "(0 < (m::inat) * n) = (0 < m \<and> 0 < n)"
+by (simp only: i0_less imult_is_0, simp)
+
+lemma mono_iSuc: "mono iSuc"
+by(simp add: mono_def)
+
+
lemma min_inat_simps [simp]:
"min (Fin m) (Fin n) = Fin (min m n)"
"min q 0 = 0"
@@ -419,6 +498,4 @@
lemmas inat_defs = zero_inat_def one_inat_def number_of_inat_def iSuc_def
plus_inat_def less_eq_inat_def less_inat_def
-lemmas inat_splits = inat.splits
-
end
--- a/src/HOL/List.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/List.thy Mon Feb 28 15:06:55 2011 +0000
@@ -1321,6 +1321,9 @@
declare nth.simps [simp del]
+lemma nth_Cons_pos[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
+by(auto simp: Nat.gr0_conv_Suc)
+
lemma nth_append:
"(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
apply (induct xs arbitrary: n, simp)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Feb 28 15:06:55 2011 +0000
@@ -4473,6 +4473,24 @@
subsection {* monotone convergence (bounded interval first). *}
+lemma upper_bound_finite_set:
+ assumes fS: "finite S"
+ shows "\<exists>(a::'a::linorder). \<forall>x \<in> S. f x \<le> a"
+proof(induct rule: finite_induct[OF fS])
+ case 1 thus ?case by simp
+next
+ case (2 x F)
+ from "2.hyps" obtain a where a:"\<forall>x \<in>F. f x \<le> a" by blast
+ let ?a = "max a (f x)"
+ have m: "a \<le> ?a" "f x \<le> ?a" by simp_all
+ {fix y assume y: "y \<in> insert x F"
+ {assume "y = x" hence "f y \<le> ?a" using m by simp}
+ moreover
+ {assume yF: "y\<in> F" from a[rule_format, OF yF] m have "f y \<le> ?a" by (simp add: max_def)}
+ ultimately have "f y \<le> ?a" using y by blast}
+ then show ?case by blast
+qed
+
lemma monotone_convergence_interval: fixes f::"nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
assumes "\<forall>k. (f k) integrable_on {a..b}"
"\<forall>k. \<forall>x\<in>{a..b}.(f k x) \<le> (f (Suc k) x)"
@@ -4530,7 +4548,8 @@
proof safe show "gauge d" using c(1) unfolding gauge_def d_def by auto
next fix p assume p:"p tagged_division_of {a..b}" "d fine p"
note p'=tagged_division_ofD[OF p(1)]
- have "\<exists>a. \<forall>x\<in>p. m (fst x) \<le> a" by(rule upper_bound_finite_set,fact)
+ have "\<exists>a. \<forall>x\<in>p. m (fst x) \<le> a"
+ by (metis finite_imageI finite_nat_set_iff_bounded_le p'(1) rev_image_eqI)
then guess s .. note s=this
have *:"\<forall>a b c d. norm(a - b) \<le> e / 4 \<and> norm(b - c) < e / 2 \<and>
norm(c - d) < e / 4 \<longrightarrow> norm(a - d) < e"
--- a/src/HOL/Tools/Function/fun.ML Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Tools/Function/fun.ML Mon Feb 28 15:06:55 2011 +0000
@@ -137,7 +137,7 @@
val fun_config = FunctionConfig { sequential=true, default=NONE,
- domintros=false, partials=false, tailrec=false }
+ domintros=false, partials=false }
fun gen_add_fun add fixes statements config lthy =
let
--- a/src/HOL/Tools/Function/function.ML Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Tools/Function/function.ML Mon Feb 28 15:06:55 2011 +0000
@@ -85,11 +85,7 @@
val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
val defname = mk_defname fixes
- val FunctionConfig {partials, tailrec, default, ...} = config
- val _ =
- if tailrec then Output.legacy_feature
- "'function (tailrec)' command. Use 'partial_function (tailrec)'."
- else ()
+ val FunctionConfig {partials, default, ...} = config
val _ =
if is_some default then Output.legacy_feature
"'function (default)'. Use 'partial_function'."
@@ -100,7 +96,7 @@
fun afterqed [[proof]] lthy =
let
- val FunctionResult {fs, R, psimps, trsimps, simple_pinducts,
+ val FunctionResult {fs, R, psimps, simple_pinducts,
termination, domintros, cases, ...} =
cont (Thm.close_derivation proof)
@@ -115,9 +111,6 @@
lthy
|> addsmps (conceal_partial o Binding.qualify false "partial")
"psimps" conceal_partial psimp_attribs psimps
- ||> (case trsimps of NONE => I | SOME thms =>
- addsmps I "simps" I simp_attribs thms #> snd
- #> Spec_Rules.add Spec_Rules.Equational (fs, thms))
||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
[Attrib.internal (K (Rule_Cases.case_names cnames)),
Attrib.internal (K (Rule_Cases.consumes 1)),
--- a/src/HOL/Tools/Function/function_common.ML Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Tools/Function/function_common.ML Mon Feb 28 15:06:55 2011 +0000
@@ -87,10 +87,7 @@
{fs: term list,
G: term,
R: term,
-
psimps : thm list,
- trsimps : thm list option,
-
simple_pinducts : thm list,
cases : thm,
termination : thm,
@@ -187,29 +184,25 @@
| Default of string
| DomIntros
| No_Partials
- | Tailrec
datatype function_config = FunctionConfig of
{sequential: bool,
default: string option,
domintros: bool,
- partials: bool,
- tailrec: bool}
+ partials: bool}
-fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
- FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec}
- | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
- FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, tailrec=tailrec}
- | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
- FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials, tailrec=tailrec}
- | apply_opt Tailrec (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
- FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=partials, tailrec=true}
- | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
- FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false, tailrec=true}
+fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials}) =
+ FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials}
+ | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials}) =
+ FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials}
+ | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials}) =
+ FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials}
+ | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials}) =
+ FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false}
val default_config =
FunctionConfig { sequential=false, default=NONE,
- domintros=false, partials=true, tailrec=false }
+ domintros=false, partials=true}
(* Analyzing function equations *)
@@ -344,8 +337,7 @@
((Parse.reserved "sequential" >> K Sequential)
|| ((Parse.reserved "default" |-- Parse.term) >> Default)
|| (Parse.reserved "domintros" >> K DomIntros)
- || (Parse.reserved "no_partials" >> K No_Partials)
- || (Parse.reserved "tailrec" >> K Tailrec))
+ || (Parse.reserved "no_partials" >> K No_Partials))
fun config_parser default =
(Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
--- a/src/HOL/Tools/Function/function_core.ML Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Tools/Function/function_core.ML Mon Feb 28 15:06:55 2011 +0000
@@ -817,61 +817,9 @@
-(* Tail recursion (probably very fragile)
- *
- * FIXME:
- * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
- * - Must we really replace the fvar by f here?
- * - Splitting is not configured automatically: Problems with case?
- *)
-fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
- let
- val Globals {domT, ranT, fvar, ...} = globals
-
- val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
-
- val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *)
- Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
- (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
- (fn {prems=[a], ...} =>
- ((rtac (G_induct OF [a]))
- THEN_ALL_NEW rtac accI
- THEN_ALL_NEW etac R_cases
- THEN_ALL_NEW asm_full_simp_tac (simpset_of octxt)) 1)
-
- val default_thm =
- forall_intr_vars graph_implies_dom COMP (f_def COMP fundef_default_value)
-
- fun mk_trsimp clause psimp =
- let
- val ClauseInfo {qglr = (oqs, _, _, _), cdata =
- ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause
- val thy = ProofContext.theory_of ctxt
- val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
-
- val trsimp = Logic.list_implies(gs,
- HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
- val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
- fun simp_default_tac ss =
- asm_full_simp_tac (ss addsimps [default_thm, Let_def])
- in
- Goal.prove ctxt [] [] trsimp (fn _ =>
- rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
- THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
- THEN (simp_default_tac (simpset_of ctxt) 1)
- THEN TRY ((etac not_acc_down 1)
- THEN ((etac R_cases)
- THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1))
- |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
- end
- in
- map2 mk_trsimp clauses psimps
- end
-
-
fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
let
- val FunctionConfig {domintros, tailrec, default=default_opt, ...} = config
+ val FunctionConfig {domintros, default=default_opt, ...} = config
val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*)
val fvar = Free (fname, fT)
@@ -932,9 +880,6 @@
(prove_stuff lthy globals G f R xclauses complete compat
compat_store G_elim) f_defthm
- val mk_trsimps =
- mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
-
fun mk_partial_rules provedgoal =
let
val newthy = theory_of_thm provedgoal (*FIXME*)
@@ -959,13 +904,10 @@
if domintros then SOME (PROFILE "Proving domain introduction rules"
(map (mk_domain_intro lthy globals R R_elim)) xclauses)
else NONE
- val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
-
in
FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
psimps=psimps, simple_pinducts=[simple_pinduct],
- termination=total_intro, trsimps=trsimps,
- domintros=dom_intros}
+ termination=total_intro, domintros=dom_intros}
end
in
((f, goalstate, mk_partial_rules), lthy)
--- a/src/HOL/Tools/Function/mutual.ML Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Tools/Function/mutual.ML Mon Feb 28 15:06:55 2011 +0000
@@ -249,7 +249,7 @@
fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
let
val result = inner_cont proof
- val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
+ val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
termination, domintros, ...} = result
val (all_f_defs, fs) =
@@ -266,7 +266,6 @@
val rew_ss = HOL_basic_ss addsimps all_f_defs
val mpsimps = map2 mk_mpsimp fqgars psimps
- val mtrsimps = Option.map (map2 mk_mpsimp fqgars) trsimps
val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
val mtermination = full_simplify rew_ss termination
val mdomintros = Option.map (map (full_simplify rew_ss)) domintros
@@ -274,7 +273,7 @@
FunctionResult { fs=fs, G=G, R=R,
psimps=mpsimps, simple_pinducts=minducts,
cases=cases, termination=mtermination,
- domintros=mdomintros, trsimps=mtrsimps}
+ domintros=mdomintros}
end
fun prepare_function_mutual config defname fixes eqss lthy =
--- a/src/HOL/Word/Bool_List_Representation.thy Mon Feb 28 15:06:36 2011 +0000
+++ b/src/HOL/Word/Bool_List_Representation.thy Mon Feb 28 15:06:55 2011 +0000
@@ -308,12 +308,7 @@
apply clarsimp
apply clarsimp
apply (case_tac w rule: bin_exhaust)
- apply clarsimp
- apply (case_tac "n - m")
- apply arith
apply simp
- apply (rule_tac f = "%n. bl ! n" in arg_cong)
- apply arith
done
lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
--- a/src/Pure/Tools/find_theorems.ML Mon Feb 28 15:06:36 2011 +0000
+++ b/src/Pure/Tools/find_theorems.ML Mon Feb 28 15:06:55 2011 +0000
@@ -9,15 +9,21 @@
datatype 'term criterion =
Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
Pattern of 'term
+
+ datatype theorem =
+ Internal of Facts.ref * thm | External of Facts.ref * term
+
val tac_limit: int Unsynchronized.ref
val limit: int Unsynchronized.ref
val find_theorems: Proof.context -> thm option -> int option -> bool ->
(bool * string criterion) list -> int option * (Facts.ref * thm) list
- val filter_facts: Proof.context -> (Facts.ref * thm) list -> thm option ->
+ val filter_theorems: Proof.context -> theorem list -> thm option ->
int option -> bool -> (bool * string criterion) list ->
- int option * (Facts.ref * thm) list
+ int option * theorem list
+ val pretty_theorem: Proof.context -> theorem -> Pretty.T
val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
+
end;
structure Find_Theorems: FIND_THEOREMS =
@@ -75,11 +81,29 @@
end;
+(** theorems, either internal or external (without proof) **)
+
+datatype theorem =
+ Internal of Facts.ref * thm |
+ External of Facts.ref * term;
+
+fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
+ | prop_of (External (_, prop)) = prop;
+
+fun nprems_of (Internal (_, thm)) = Thm.nprems_of thm
+ | nprems_of (External (_, prop)) = Logic.count_prems prop;
+
+fun major_prem_of (Internal (_, thm)) = Thm.major_prem_of thm
+ | major_prem_of (External (_, prop)) =
+ Logic.strip_assums_concl (hd (Logic.strip_imp_prems prop));
+
+fun fact_ref_of (Internal (fact_ref, _)) = fact_ref
+ | fact_ref_of (External (fact_ref, _)) = fact_ref;
(** search criterion filters **)
(*generated filters are to be of the form
- input: (Facts.ref * thm)
+ input: theorem
output: (p:int, s:int) option, where
NONE indicates no match
p is the primary sorting criterion
@@ -142,43 +166,43 @@
(* filter_name *)
-fun filter_name str_pat (thmref, _) =
- if match_string str_pat (Facts.name_of_ref thmref)
+fun filter_name str_pat theorem =
+ if match_string str_pat (Facts.name_of_ref (fact_ref_of theorem))
then SOME (0, 0) else NONE;
(* filter intro/elim/dest/solves rules *)
-fun filter_dest ctxt goal (_, thm) =
+fun filter_dest ctxt goal theorem =
let
val extract_dest =
- (fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm],
+ (fn theorem => if nprems_of theorem = 0 then [] else [prop_of theorem],
hd o Logic.strip_imp_prems);
val prems = Logic.prems_of_goal goal 1;
- fun try_subst prem = is_matching_thm false extract_dest ctxt true prem thm;
+ fun try_subst prem = is_matching_thm false extract_dest ctxt true prem theorem;
val successful = prems |> map_filter try_subst;
in
(*if possible, keep best substitution (one with smallest size)*)
(*dest rules always have assumptions, so a dest with one
assumption is as good as an intro rule with none*)
if not (null successful)
- then SOME (Thm.nprems_of thm - 1, foldl1 Int.min successful) else NONE
+ then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
end;
-fun filter_intro doiff ctxt goal (_, thm) =
+fun filter_intro doiff ctxt goal theorem =
let
- val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl);
+ val extract_intro = (single o prop_of, Logic.strip_imp_concl);
val concl = Logic.concl_of_goal goal 1;
- val ss = is_matching_thm doiff extract_intro ctxt true concl thm;
+ val ss = is_matching_thm doiff extract_intro ctxt true concl theorem;
in
- if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
+ if is_some ss then SOME (nprems_of theorem, the ss) else NONE
end;
-fun filter_elim ctxt goal (_, thm) =
- if not (Thm.no_prems thm) then
+fun filter_elim ctxt goal theorem =
+ if nprems_of theorem > 0 then
let
- val rule = Thm.full_prop_of thm;
+ val rule = prop_of theorem;
val prems = Logic.prems_of_goal goal 1;
val goal_concl = Logic.concl_of_goal goal 1;
val rule_mp = hd (Logic.strip_imp_prems rule);
@@ -192,9 +216,9 @@
in
(*elim rules always have assumptions, so an elim with one
assumption is as good as an intro rule with none*)
- if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm)
+ if is_nontrivial (ProofContext.theory_of ctxt) (major_prem_of theorem)
andalso not (null successful)
- then SOME (Thm.nprems_of thm - 1, foldl1 Int.min successful) else NONE
+ then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
end
else NONE
@@ -207,29 +231,30 @@
if Thm.no_prems thm then rtac thm 1 goal
else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
in
- fn (_, thm) =>
+ fn Internal (_, thm) =>
if is_some (Seq.pull (try_thm thm))
then SOME (Thm.nprems_of thm, 0) else NONE
+ | External _ => NONE
end;
(* filter_simp *)
-fun filter_simp ctxt t (_, thm) =
- let
- val mksimps = Simplifier.mksimps (simpset_of ctxt);
- val extract_simp =
- (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
- val ss = is_matching_thm false extract_simp ctxt false t thm;
- in
- if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
- end;
+fun filter_simp ctxt t (Internal (_, thm)) =
+ let
+ val mksimps = Simplifier.mksimps (simpset_of ctxt);
+ val extract_simp =
+ (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
+ val ss = is_matching_thm false extract_simp ctxt false t thm;
+ in
+ if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
+ end
+ | filter_simp _ _ (External _) = NONE;
(* filter_pattern *)
fun get_names t = Term.add_const_names t (Term.add_free_names t []);
-fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm);
(*Including all constants and frees is only sound because
matching uses higher-order patterns. If full matching
@@ -246,10 +271,10 @@
let
val pat_consts = get_names pat;
- fun check (t, NONE) = check (t, SOME (get_thm_names t))
- | check ((_, thm), c as SOME thm_consts) =
+ fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem)))
+ | check (theorem, c as SOME thm_consts) =
(if subset (op =) (pat_consts, thm_consts) andalso
- Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm)
+ Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, prop_of theorem)
then SOME (0, 0) else NONE, c);
in check end;
@@ -297,16 +322,16 @@
fun filter_criterion ctxt opt_goal (b, c) =
(if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c;
-fun sorted_filter filters thms =
+fun sorted_filter filters theorems =
let
- fun eval_filters thm = app_filters thm (SOME (0, 0), NONE, filters);
+ fun eval_filters theorem = app_filters theorem (SOME (0, 0), NONE, filters);
(*filters return: (number of assumptions, substitution size) option, so
sort (desc. in both cases) according to number of assumptions first,
then by the substitution size*)
- fun thm_ord (((p0, s0), _), ((p1, s1), _)) =
+ fun result_ord (((p0, s0), _), ((p1, s1), _)) =
prod_ord int_ord int_ord ((p1, s1), (p0, s0));
- in map_filter eval_filters thms |> sort thm_ord |> map #2 end;
+ in map_filter eval_filters theorems |> sort result_ord |> map #2 end;
fun lazy_filter filters =
let
@@ -342,9 +367,9 @@
let
fun rem_c rev_seen [] = rev rev_seen
| rem_c rev_seen [x] = rem_c (x :: rev_seen) []
- | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) =
- if Thm.eq_thm_prop (t, t')
- then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
+ | rem_c rev_seen ((x as (t, _)) :: (y as (t', _)) :: xs) =
+ if (prop_of t) aconv (prop_of t')
+ then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs)
else rem_c (x :: rev_seen) (y :: xs)
in rem_c [] xs end;
@@ -367,7 +392,7 @@
fun rem_thm_dups nicer xs =
xs ~~ (1 upto length xs)
- |> sort (Term_Ord.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
+ |> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1))
|> rem_cdups nicer
|> sort (int_ord o pairself #2)
|> map #1;
@@ -385,12 +410,14 @@
in
maps Facts.selections
(visible_facts (Global_Theory.facts_of (ProofContext.theory_of ctxt)) @
+
+
visible_facts (ProofContext.facts_of ctxt))
end;
val limit = Unsynchronized.ref 40;
-fun filter_facts ctxt facts opt_goal opt_limit rem_dups raw_criteria =
+fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups raw_criteria =
let
val assms =
ProofContext.get_fact ctxt (Facts.named "local.assms")
@@ -401,9 +428,9 @@
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
val filters = map (filter_criterion ctxt opt_goal') criteria;
- fun find_all facts =
+ fun find_all theorems =
let
- val raw_matches = sorted_filter filters facts;
+ val raw_matches = sorted_filter filters theorems;
val matches =
if rem_dups
@@ -419,20 +446,30 @@
then find_all
else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;
- in find facts end;
+ in find theorems end;
-fun find_theorems ctxt = filter_facts ctxt (all_facts_of ctxt)
+fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
+ filter_theorems ctxt (map Internal (all_facts_of ctxt)) opt_goal opt_limit
+ rem_dups raw_criteria
+ |> apsnd (map (fn Internal f => f));
-fun pretty_thm ctxt (thmref, thm) = Pretty.block
- [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
- Display.pretty_thm ctxt thm];
+fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block
+ [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
+ Display.pretty_thm ctxt thm]
+ | pretty_theorem ctxt (External (thmref, prop)) = Pretty.block
+ [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
+ Syntax.unparse_term ctxt prop];
-fun print_theorems ctxt (foundo, thms) raw_criteria =
+fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
+
+fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
let
val start = start_timing ();
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
- val returned = length thms;
+ val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
+ opt_goal opt_limit rem_dups raw_criteria;
+ val returned = length theorems;
val tally_msg =
(case foundo of
@@ -447,10 +484,10 @@
in
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
Pretty.str "" ::
- (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
+ (if null theorems then [Pretty.str ("nothing found" ^ end_msg)]
else
[Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
- map (pretty_thm ctxt) thms)
+ map (pretty_theorem ctxt) theorems)
end |> Pretty.chunks |> Pretty.writeln;
@@ -486,8 +523,7 @@
let
val ctxt = Toplevel.context_of state;
val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
- val found = find_theorems ctxt opt_goal opt_lim rem_dups spec;
- in print_theorems ctxt found spec end)));
+ in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
end;