--- a/doc-src/Classes/Thy/document/Classes.tex Wed Feb 23 11:40:18 2011 +0100
+++ b/doc-src/Classes/Thy/document/Classes.tex Wed Feb 23 11:42:01 2011 +0100
@@ -1357,12 +1357,12 @@
{\isaliteral{7D}{\isacharbraceright}}\isanewline
def\ inverse{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ group{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{60}{\isacharbackquote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
-def\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{3A}{\isacharcolon}}\ monoid{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}xa{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}xa{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ match\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+def\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A\ {\isaliteral{3A}{\isacharcolon}}\ monoid{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}xa{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}xa{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ match\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
\ \ case\ {\isaliteral{28}{\isacharparenleft}}Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ neutral{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\isanewline
\ \ case\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
{\isaliteral{7D}{\isacharbraceright}}\isanewline
\isanewline
-def\ pow{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{3A}{\isacharcolon}}\ group{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\isanewline
+def\ pow{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5B}{\isacharbrackleft}}A\ {\isaliteral{3A}{\isacharcolon}}\ group{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\isanewline
\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{29}{\isacharparenright}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}nat{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ else\ inverse{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}nat{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
--- a/doc-src/System/Thy/Presentation.thy Wed Feb 23 11:40:18 2011 +0100
+++ b/doc-src/System/Thy/Presentation.thy Wed Feb 23 11:42:01 2011 +0100
@@ -446,7 +446,7 @@
-D PATH dump generated document sources into PATH
-M MAX multithreading: maximum number of worker threads (default 1)
-P PATH set path for remote theory browsing information
- -Q INT set threshold for sub-proof parallelization (default 100)
+ -Q INT set threshold for sub-proof parallelization (default 50)
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
@@ -568,7 +568,9 @@
proofs (default), @{verbatim 2} toplevel and nested Isar proofs.
The option @{verbatim "-Q"} specifies a threshold for @{verbatim
"-q2"}: nested proofs are only parallelized when the current number
- of forked proofs falls below the given value (default 100).
+ of forked proofs falls below the given value (default 50),
+ multiplied by the number of worker threads (see option @{verbatim
+ "-M"}).
\medskip The @{verbatim "-t"} option produces a more detailed
internal timing report of the session.
@@ -578,16 +580,16 @@
prepared documents.
\medskip The @{verbatim "-M"} option specifies the maximum number of
- parallel threads used for processing independent tasks when checking
- theory sources (multithreading only works on suitable ML platforms).
- The special value of @{verbatim 0} or @{verbatim max} refers to the
- number of actual CPU cores of the underlying machine, which is a
- good starting point for optimal performance tuning. The @{verbatim
- "-T"} option determines the level of detail in tracing output
- concerning the internal locking and scheduling in multithreaded
- operation. This may be helpful in isolating performance
- bottle-necks, e.g.\ due to excessive wait states when locking
- critical code sections.
+ parallel worker threads used for processing independent tasks when
+ checking theory sources (multithreading only works on suitable ML
+ platforms). The special value of @{verbatim 0} or @{verbatim max}
+ refers to the number of actual CPU cores of the underlying machine,
+ which is a good starting point for optimal performance tuning. The
+ @{verbatim "-T"} option determines the level of detail in tracing
+ output concerning the internal locking and scheduling in
+ multithreaded operation. This may be helpful in isolating
+ performance bottle-necks, e.g.\ due to excessive wait states when
+ locking critical code sections.
\medskip Any @{tool usedir} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend
--- a/doc-src/System/Thy/document/Presentation.tex Wed Feb 23 11:40:18 2011 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex Wed Feb 23 11:42:01 2011 +0100
@@ -472,7 +472,7 @@
-D PATH dump generated document sources into PATH
-M MAX multithreading: maximum number of worker threads (default 1)
-P PATH set path for remote theory browsing information
- -Q INT set threshold for sub-proof parallelization (default 100)
+ -Q INT set threshold for sub-proof parallelization (default 50)
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
@@ -584,7 +584,8 @@
proof checking: \verb|0| no proofs, \verb|1| toplevel
proofs (default), \verb|2| toplevel and nested Isar proofs.
The option \verb|-Q| specifies a threshold for \verb|-q2|: nested proofs are only parallelized when the current number
- of forked proofs falls below the given value (default 100).
+ of forked proofs falls below the given value (default 50),
+ multiplied by the number of worker threads (see option \verb|-M|).
\medskip The \verb|-t| option produces a more detailed
internal timing report of the session.
@@ -594,15 +595,16 @@
prepared documents.
\medskip The \verb|-M| option specifies the maximum number of
- parallel threads used for processing independent tasks when checking
- theory sources (multithreading only works on suitable ML platforms).
- The special value of \verb|0| or \verb|max| refers to the
- number of actual CPU cores of the underlying machine, which is a
- good starting point for optimal performance tuning. The \verb|-T| option determines the level of detail in tracing output
- concerning the internal locking and scheduling in multithreaded
- operation. This may be helpful in isolating performance
- bottle-necks, e.g.\ due to excessive wait states when locking
- critical code sections.
+ parallel worker threads used for processing independent tasks when
+ checking theory sources (multithreading only works on suitable ML
+ platforms). The special value of \verb|0| or \verb|max|
+ refers to the number of actual CPU cores of the underlying machine,
+ which is a good starting point for optimal performance tuning. The
+ \verb|-T| option determines the level of detail in tracing
+ output concerning the internal locking and scheduling in
+ multithreaded operation. This may be helpful in isolating
+ performance bottle-necks, e.g.\ due to excessive wait states when
+ locking critical code sections.
\medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend
--- a/src/FOL/FOL.thy Wed Feb 23 11:40:18 2011 +0100
+++ b/src/FOL/FOL.thy Wed Feb 23 11:42:01 2011 +0100
@@ -11,6 +11,7 @@
"~~/src/Provers/blast.ML"
"~~/src/Provers/clasimp.ML"
"~~/src/Tools/induct.ML"
+ "~~/src/Tools/case_product.ML"
("cladata.ML")
("simpdata.ML")
begin
@@ -391,6 +392,8 @@
setup Induct.setup
declare case_split [cases type: o]
+setup Case_Product.setup
+
hide_const (open) eq
--- a/src/FOL/IsaMakefile Wed Feb 23 11:40:18 2011 +0100
+++ b/src/FOL/IsaMakefile Wed Feb 23 11:42:01 2011 +0100
@@ -28,6 +28,7 @@
$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
+ $(SRC)/Tools/case_product.ML \
$(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \
$(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 23 11:40:18 2011 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 23 11:42:01 2011 +0100
@@ -85,27 +85,23 @@
using nb le bnd
by (induct t rule: tm.induct , auto)
-consts
- incrtm0:: "tm \<Rightarrow> tm"
- decrtm0:: "tm \<Rightarrow> tm"
-
-recdef decrtm0 "measure size"
+fun decrtm0:: "tm \<Rightarrow> tm" where
"decrtm0 (Bound n) = Bound (n - 1)"
- "decrtm0 (Neg a) = Neg (decrtm0 a)"
- "decrtm0 (Add a b) = Add (decrtm0 a) (decrtm0 b)"
- "decrtm0 (Sub a b) = Sub (decrtm0 a) (decrtm0 b)"
- "decrtm0 (Mul c a) = Mul c (decrtm0 a)"
- "decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
- "decrtm0 a = a"
+| "decrtm0 (Neg a) = Neg (decrtm0 a)"
+| "decrtm0 (Add a b) = Add (decrtm0 a) (decrtm0 b)"
+| "decrtm0 (Sub a b) = Sub (decrtm0 a) (decrtm0 b)"
+| "decrtm0 (Mul c a) = Mul c (decrtm0 a)"
+| "decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
+| "decrtm0 a = a"
-recdef incrtm0 "measure size"
+fun incrtm0:: "tm \<Rightarrow> tm" where
"incrtm0 (Bound n) = Bound (n + 1)"
- "incrtm0 (Neg a) = Neg (incrtm0 a)"
- "incrtm0 (Add a b) = Add (incrtm0 a) (incrtm0 b)"
- "incrtm0 (Sub a b) = Sub (incrtm0 a) (incrtm0 b)"
- "incrtm0 (Mul c a) = Mul c (incrtm0 a)"
- "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
- "incrtm0 a = a"
+| "incrtm0 (Neg a) = Neg (incrtm0 a)"
+| "incrtm0 (Add a b) = Add (incrtm0 a) (incrtm0 b)"
+| "incrtm0 (Sub a b) = Sub (incrtm0 a) (incrtm0 b)"
+| "incrtm0 (Mul c a) = Mul c (incrtm0 a)"
+| "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
+| "incrtm0 a = a"
lemma decrtm0: assumes nb: "tmbound0 t"
shows "Itm vs (x#bs) t = Itm vs bs (decrtm0 t)"
@@ -213,9 +209,7 @@
(* Simplification *)
consts
- simptm:: "tm \<Rightarrow> tm"
tmadd:: "tm \<times> tm \<Rightarrow> tm"
- tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm"
recdef tmadd "measure (\<lambda> (t,s). size t + size s)"
"tmadd (CNP n1 c1 r1,CNP n2 c2 r2) =
(if n1=n2 then
@@ -245,10 +239,10 @@
lemma tmadd_allpolys_npoly[simp]: "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd(t,s))" by (induct t s rule: tmadd.induct, simp_all add: Let_def polyadd_norm)
-recdef tmmul "measure size"
+fun tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm" where
"tmmul (CP j) = (\<lambda> i. CP (i *\<^sub>p j))"
- "tmmul (CNP n c a) = (\<lambda> i. CNP n (i *\<^sub>p c) (tmmul a i))"
- "tmmul t = (\<lambda> i. Mul i t)"
+| "tmmul (CNP n c a) = (\<lambda> i. CNP n (i *\<^sub>p c) (tmmul a i))"
+| "tmmul t = (\<lambda> i. Mul i t)"
lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)"
by (induct t arbitrary: i rule: tmmul.induct, simp_all add: field_simps)
@@ -306,14 +300,14 @@
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
unfolding tmsub_def by (simp add: isnpoly_def)
-recdef simptm "measure size"
+fun simptm:: "tm \<Rightarrow> tm" where
"simptm (CP j) = CP (polynate j)"
- "simptm (Bound n) = CNP n 1\<^sub>p (CP 0\<^sub>p)"
- "simptm (Neg t) = tmneg (simptm t)"
- "simptm (Add t s) = tmadd (simptm t,simptm s)"
- "simptm (Sub t s) = tmsub (simptm t) (simptm s)"
- "simptm (Mul i t) = (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')"
- "simptm (CNP n c t) = (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))"
+| "simptm (Bound n) = CNP n 1\<^sub>p (CP 0\<^sub>p)"
+| "simptm (Neg t) = tmneg (simptm t)"
+| "simptm (Add t s) = tmadd (simptm t,simptm s)"
+| "simptm (Sub t s) = tmsub (simptm t) (simptm s)"
+| "simptm (Mul i t) = (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')"
+| "simptm (CNP n c t) = (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))"
lemma polynate_stupid:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
@@ -341,16 +335,19 @@
shows "allpolys isnpoly (simptm p)"
by (induct p rule: simptm.induct, auto simp add: Let_def)
-consts split0 :: "tm \<Rightarrow> (poly \<times> tm)"
-recdef split0 "measure tmsize"
+declare let_cong[fundef_cong del]
+
+fun split0 :: "tm \<Rightarrow> (poly \<times> tm)" where
"split0 (Bound 0) = (1\<^sub>p, CP 0\<^sub>p)"
- "split0 (CNP 0 c t) = (let (c',t') = split0 t in (c +\<^sub>p c',t'))"
- "split0 (Neg t) = (let (c,t') = split0 t in (~\<^sub>p c,Neg t'))"
- "split0 (CNP n c t) = (let (c',t') = split0 t in (c',CNP n c t'))"
- "split0 (Add s t) = (let (c1,s') = split0 s ; (c2,t') = split0 t in (c1 +\<^sub>p c2, Add s' t'))"
- "split0 (Sub s t) = (let (c1,s') = split0 s ; (c2,t') = split0 t in (c1 -\<^sub>p c2, Sub s' t'))"
- "split0 (Mul c t) = (let (c',t') = split0 t in (c *\<^sub>p c', Mul c t'))"
- "split0 t = (0\<^sub>p, t)"
+| "split0 (CNP 0 c t) = (let (c',t') = split0 t in (c +\<^sub>p c',t'))"
+| "split0 (Neg t) = (let (c,t') = split0 t in (~\<^sub>p c,Neg t'))"
+| "split0 (CNP n c t) = (let (c',t') = split0 t in (c',CNP n c t'))"
+| "split0 (Add s t) = (let (c1,s') = split0 s ; (c2,t') = split0 t in (c1 +\<^sub>p c2, Add s' t'))"
+| "split0 (Sub s t) = (let (c1,s') = split0 s ; (c2,t') = split0 t in (c1 -\<^sub>p c2, Sub s' t'))"
+| "split0 (Mul c t) = (let (c',t') = split0 t in (c *\<^sub>p c', Mul c t'))"
+| "split0 t = (0\<^sub>p, t)"
+
+declare let_cong[fundef_cong]
lemma split0_stupid[simp]: "\<exists>x y. (x,y) = split0 p"
apply (rule exI[where x="fst (split0 p)"])
@@ -424,18 +421,17 @@
(* A size for fm *)
-consts fmsize :: "fm \<Rightarrow> nat"
-recdef fmsize "measure size"
+fun fmsize :: "fm \<Rightarrow> nat" where
"fmsize (NOT p) = 1 + fmsize p"
- "fmsize (And p q) = 1 + fmsize p + fmsize q"
- "fmsize (Or p q) = 1 + fmsize p + fmsize q"
- "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
- "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
- "fmsize (E p) = 1 + fmsize p"
- "fmsize (A p) = 4+ fmsize p"
- "fmsize p = 1"
+| "fmsize (And p q) = 1 + fmsize p + fmsize q"
+| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
+| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
+| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
+| "fmsize (E p) = 1 + fmsize p"
+| "fmsize (A p) = 4+ fmsize p"
+| "fmsize p = 1"
(* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p > 0"
+lemma fmsize_pos[termination_simp]: "fmsize p > 0"
by (induct p rule: fmsize.induct) simp_all
(* Semantics of formulae (fm) *)
@@ -454,17 +450,16 @@
| "Ifm vs bs (E p) = (\<exists> x. Ifm vs (x#bs) p)"
| "Ifm vs bs (A p) = (\<forall> x. Ifm vs (x#bs) p)"
-consts not:: "fm \<Rightarrow> fm"
-recdef not "measure size"
+fun not:: "fm \<Rightarrow> fm" where
"not (NOT (NOT p)) = not p"
- "not (NOT p) = p"
- "not T = F"
- "not F = T"
- "not (Lt t) = Le (tmneg t)"
- "not (Le t) = Lt (tmneg t)"
- "not (Eq t) = NEq t"
- "not (NEq t) = Eq t"
- "not p = NOT p"
+| "not (NOT p) = p"
+| "not T = F"
+| "not F = T"
+| "not (Lt t) = Le (tmneg t)"
+| "not (Le t) = Lt (tmneg t)"
+| "not (Eq t) = NEq t"
+| "not (NEq t) = Eq t"
+| "not p = NOT p"
lemma not[simp]: "Ifm vs bs (not p) = Ifm vs bs (NOT p)"
by (induct p rule: not.induct) auto
@@ -493,17 +488,17 @@
Iff p q)"
lemma iff[simp]: "Ifm vs bs (iff p q) = Ifm vs bs (Iff p q)"
by (unfold iff_def,cases "p=q", simp,cases "p=NOT q", simp) (cases "NOT p= q", auto)
+
(* Quantifier freeness *)
-consts qfree:: "fm \<Rightarrow> bool"
-recdef qfree "measure size"
+fun qfree:: "fm \<Rightarrow> bool" where
"qfree (E p) = False"
- "qfree (A p) = False"
- "qfree (NOT p) = qfree p"
- "qfree (And p q) = (qfree p \<and> qfree q)"
- "qfree (Or p q) = (qfree p \<and> qfree q)"
- "qfree (Imp p q) = (qfree p \<and> qfree q)"
- "qfree (Iff p q) = (qfree p \<and> qfree q)"
- "qfree p = True"
+| "qfree (A p) = False"
+| "qfree (NOT p) = qfree p"
+| "qfree (And p q) = (qfree p \<and> qfree q)"
+| "qfree (Or p q) = (qfree p \<and> qfree q)"
+| "qfree (Imp p q) = (qfree p \<and> qfree q)"
+| "qfree (Iff p q) = (qfree p \<and> qfree q)"
+| "qfree p = True"
(* Boundedness and substitution *)
@@ -522,22 +517,19 @@
| "boundslt n (E p) = boundslt (Suc n) p"
| "boundslt n (A p) = boundslt (Suc n) p"
-consts
- bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
- decr0 :: "fm \<Rightarrow> fm"
-recdef bound0 "measure size"
+fun bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
"bound0 T = True"
- "bound0 F = True"
- "bound0 (Lt a) = tmbound0 a"
- "bound0 (Le a) = tmbound0 a"
- "bound0 (Eq a) = tmbound0 a"
- "bound0 (NEq a) = tmbound0 a"
- "bound0 (NOT p) = bound0 p"
- "bound0 (And p q) = (bound0 p \<and> bound0 q)"
- "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
- "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
- "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
- "bound0 p = False"
+| "bound0 F = True"
+| "bound0 (Lt a) = tmbound0 a"
+| "bound0 (Le a) = tmbound0 a"
+| "bound0 (Eq a) = tmbound0 a"
+| "bound0 (NEq a) = tmbound0 a"
+| "bound0 (NOT p) = bound0 p"
+| "bound0 (And p q) = (bound0 p \<and> bound0 q)"
+| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
+| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
+| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
+| "bound0 p = False"
lemma bound0_I:
assumes bp: "bound0 p"
shows "Ifm vs (b#bs) p = Ifm vs (b'#bs) p"
@@ -578,17 +570,17 @@
thus ?case by simp
qed auto
-recdef decr0 "measure size"
+fun decr0 :: "fm \<Rightarrow> fm" where
"decr0 (Lt a) = Lt (decrtm0 a)"
- "decr0 (Le a) = Le (decrtm0 a)"
- "decr0 (Eq a) = Eq (decrtm0 a)"
- "decr0 (NEq a) = NEq (decrtm0 a)"
- "decr0 (NOT p) = NOT (decr0 p)"
- "decr0 (And p q) = conj (decr0 p) (decr0 q)"
- "decr0 (Or p q) = disj (decr0 p) (decr0 q)"
- "decr0 (Imp p q) = imp (decr0 p) (decr0 q)"
- "decr0 (Iff p q) = iff (decr0 p) (decr0 q)"
- "decr0 p = p"
+| "decr0 (Le a) = Le (decrtm0 a)"
+| "decr0 (Eq a) = Eq (decrtm0 a)"
+| "decr0 (NEq a) = NEq (decrtm0 a)"
+| "decr0 (NOT p) = NOT (decr0 p)"
+| "decr0 (And p q) = conj (decr0 p) (decr0 q)"
+| "decr0 (Or p q) = disj (decr0 p) (decr0 q)"
+| "decr0 (Imp p q) = imp (decr0 p) (decr0 q)"
+| "decr0 (Iff p q) = iff (decr0 p) (decr0 q)"
+| "decr0 p = p"
lemma decr0: assumes nb: "bound0 p"
shows "Ifm vs (x#bs) p = Ifm vs bs (decr0 p)"
@@ -746,16 +738,14 @@
lemma decr0_qf: "bound0 p \<Longrightarrow> qfree (decr0 p)"
by (induct p, simp_all)
-consts
- isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
-recdef isatom "measure size"
+fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) where
"isatom T = True"
- "isatom F = True"
- "isatom (Lt a) = True"
- "isatom (Le a) = True"
- "isatom (Eq a) = True"
- "isatom (NEq a) = True"
- "isatom p = False"
+| "isatom F = True"
+| "isatom (Lt a) = True"
+| "isatom (Le a) = True"
+| "isatom (Eq a) = True"
+| "isatom (NEq a) = True"
+| "isatom p = False"
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
by (induct p, simp_all)
@@ -783,11 +773,10 @@
shows "qfree (evaldjf f xs)"
using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
-consts disjuncts :: "fm \<Rightarrow> fm list"
-recdef disjuncts "measure size"
+fun disjuncts :: "fm \<Rightarrow> fm list" where
"disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
- "disjuncts F = []"
- "disjuncts p = [p]"
+| "disjuncts F = []"
+| "disjuncts p = [p]"
lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm vs bs q) = Ifm vs bs p"
by(induct p rule: disjuncts.induct, auto)
@@ -846,12 +835,10 @@
finally show "qfree (DJ qe p) \<and> Ifm vs bs (DJ qe p) = Ifm vs bs (E p)" using qfth by blast
qed
-consts conjuncts :: "fm \<Rightarrow> fm list"
-
-recdef conjuncts "measure size"
+fun conjuncts :: "fm \<Rightarrow> fm list" where
"conjuncts (And p q) = (conjuncts p) @ (conjuncts q)"
- "conjuncts T = []"
- "conjuncts p = [p]"
+| "conjuncts T = []"
+| "conjuncts p = [p]"
definition list_conj :: "fm list \<Rightarrow> fm" where
"list_conj ps \<equiv> foldr conj ps T"
@@ -1135,11 +1122,10 @@
fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simpneq_def Let_def split_def neq_nb)
qed
-consts conjs :: "fm \<Rightarrow> fm list"
-recdef conjs "measure size"
+fun conjs :: "fm \<Rightarrow> fm list" where
"conjs (And p q) = (conjs p)@(conjs q)"
- "conjs T = []"
- "conjs p = [p]"
+| "conjs T = []"
+| "conjs p = [p]"
lemma conjs_ci: "(\<forall> q \<in> set (conjs p). Ifm vs bs q) = Ifm vs bs p"
by (induct p rule: conjs.induct, auto)
definition list_disj :: "fm list \<Rightarrow> fm" where
@@ -1318,17 +1304,17 @@
(* Generic quantifier elimination *)
-consts qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
-recdef qelim "measure fmsize"
+function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm" where
"qelim (E p) = (\<lambda> qe. DJ (CJNB qe) (qelim p qe))"
- "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
- "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
- "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))"
- "qelim (Or p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))"
- "qelim (Imp p q) = (\<lambda> qe. imp (qelim p qe) (qelim q qe))"
- "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
- "qelim p = (\<lambda> y. simpfm p)"
-
+| "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
+| "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
+| "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))"
+| "qelim (Or p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))"
+| "qelim (Imp p q) = (\<lambda> qe. imp (qelim p qe) (qelim q qe))"
+| "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
+| "qelim p = (\<lambda> y. simpfm p)"
+by pat_completeness simp_all
+termination by (relation "measure fmsize") auto
lemma qelim:
assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))"
@@ -1338,26 +1324,23 @@
subsection{* Core Procedure *}
-consts
- plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
- minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
-recdef minusinf "measure size"
+fun minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*) where
"minusinf (And p q) = conj (minusinf p) (minusinf q)"
- "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
- "minusinf (Eq (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
- "minusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
- "minusinf (Lt (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP (~\<^sub>p c)))"
- "minusinf (Le (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP (~\<^sub>p c)))"
- "minusinf p = p"
+| "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
+| "minusinf (Eq (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
+| "minusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
+| "minusinf (Lt (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP (~\<^sub>p c)))"
+| "minusinf (Le (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP (~\<^sub>p c)))"
+| "minusinf p = p"
-recdef plusinf "measure size"
+fun plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*) where
"plusinf (And p q) = conj (plusinf p) (plusinf q)"
- "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
- "plusinf (Eq (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
- "plusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
- "plusinf (Lt (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP c))"
- "plusinf (Le (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP c))"
- "plusinf p = p"
+| "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
+| "plusinf (Eq (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
+| "plusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
+| "plusinf (Lt (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP c))"
+| "plusinf (Le (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP c))"
+| "plusinf p = p"
lemma minusinf_inf: assumes lp:"islin p"
shows "\<exists>z. \<forall>x < z. Ifm vs (x#bs) (minusinf p) \<longleftrightarrow> Ifm vs (x#bs) p"
@@ -2492,16 +2475,6 @@
lemma filter_length: "length (List.filter P xs) < Suc (length xs)"
apply (induct xs, auto) done
-consts remdps:: "'a list \<Rightarrow> 'a list"
-
-recdef remdps "measure size"
- "remdps [] = []"
- "remdps (x#xs) = (x#(remdps (List.filter (\<lambda> y. y \<noteq> x) xs)))"
-(hints simp add: filter_length[rule_format])
-
-lemma remdps_set[simp]: "set (remdps xs) = set xs"
- by (induct xs rule: remdps.induct, auto)
-
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)
@@ -2509,7 +2482,7 @@
definition
"ferrack p \<equiv> let q = simpfm p ; mp = minusinf q ; pp = plusinf q
in if (mp = T \<or> pp = T) then T
- else (let U = alluopairs (remdps (uset q))
+ else (let U = alluopairs (remdups (uset q))
in decr0 (disj mp (disj pp (evaldjf (simpfm o (msubst q)) U ))))"
lemma ferrack:
@@ -2521,7 +2494,7 @@
let ?N = "\<lambda> t. Ipoly vs t"
let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
let ?q = "simpfm p"
- let ?U = "remdps(uset ?q)"
+ let ?U = "remdups(uset ?q)"
let ?Up = "alluopairs ?U"
let ?mp = "minusinf ?q"
let ?pp = "plusinf ?q"
@@ -2810,7 +2783,7 @@
definition
"ferrack2 p \<equiv> let q = simpfm p ; mp = minusinf q ; pp = plusinf q
in if (mp = T \<or> pp = T) then T
- else (let U = remdps (uset q)
+ else (let U = remdups (uset q)
in decr0 (list_disj [mp, pp, simpfm (subst0 (CP 0\<^sub>p) q), evaldjf (\<lambda>(c,t). msubst2 q (c *\<^sub>p C (-2, 1)) t) U,
evaldjf (\<lambda>((b,a),(d,c)). msubst2 q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) (alluopairs U)]))"
@@ -2825,7 +2798,7 @@
let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
let ?q = "simpfm p"
let ?qz = "subst0 (CP 0\<^sub>p) ?q"
- let ?U = "remdps(uset ?q)"
+ let ?U = "remdups(uset ?q)"
let ?Up = "alluopairs ?U"
let ?mp = "minusinf ?q"
let ?pp = "plusinf ?q"
--- a/src/HOL/HOL.thy Wed Feb 23 11:40:18 2011 +0100
+++ b/src/HOL/HOL.thy Wed Feb 23 11:42:01 2011 +0100
@@ -31,10 +31,12 @@
("Tools/recfun_codegen.ML")
("Tools/cnf_funcs.ML")
"~~/src/Tools/subtyping.ML"
+ "~~/src/Tools/case_product.ML"
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
setup Subtyping.setup
+setup Case_Product.setup
subsection {* Primitive logic *}
--- a/src/HOL/Hahn_Banach/Function_Order.thy Wed Feb 23 11:40:18 2011 +0100
+++ b/src/HOL/Hahn_Banach/Function_Order.thy Wed Feb 23 11:42:01 2011 +0100
@@ -21,7 +21,7 @@
graph.
*}
-types 'a graph = "('a \<times> real) set"
+type_synonym 'a graph = "('a \<times> real) set"
definition
graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" where
--- a/src/HOL/Induct/Com.thy Wed Feb 23 11:40:18 2011 +0100
+++ b/src/HOL/Induct/Com.thy Wed Feb 23 11:42:01 2011 +0100
@@ -10,7 +10,7 @@
theory Com imports Main begin
typedecl loc
-types state = "loc => nat"
+type_synonym state = "loc => nat"
datatype
exp = N nat
--- a/src/HOL/Induct/Sexp.thy Wed Feb 23 11:40:18 2011 +0100
+++ b/src/HOL/Induct/Sexp.thy Wed Feb 23 11:42:01 2011 +0100
@@ -8,8 +8,7 @@
theory Sexp imports Main begin
-types
- 'a item = "'a Datatype.item"
+type_synonym 'a item = "'a Datatype.item"
abbreviation "Leaf == Datatype.Leaf"
abbreviation "Numb == Datatype.Numb"
--- a/src/HOL/IsaMakefile Wed Feb 23 11:40:18 2011 +0100
+++ b/src/HOL/IsaMakefile Wed Feb 23 11:42:01 2011 +0100
@@ -135,6 +135,7 @@
$(SRC)/Tools/IsaPlanner/zipper.ML \
$(SRC)/Tools/atomize_elim.ML \
$(SRC)/Tools/auto_tools.ML \
+ $(SRC)/Tools/case_product.ML \
$(SRC)/Tools/coherent.ML \
$(SRC)/Tools/cong_tac.ML \
$(SRC)/Tools/eqsubst.ML \
@@ -1026,6 +1027,7 @@
Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \
ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy ex/CTL.thy \
+ ex/Case_Product.thy \
ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \
ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \
ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Wed Feb 23 11:40:18 2011 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Wed Feb 23 11:42:01 2011 +0100
@@ -22,8 +22,7 @@
This is both for abstract syntax and semantics, i.e.\ we use a
``shallow embedding'' here. *}
-types
- 'val binop = "'val => 'val => 'val"
+type_synonym 'val binop = "'val => 'val => 'val"
subsection {* Expressions *}
--- a/src/HOL/Isar_Examples/Hoare.thy Wed Feb 23 11:40:18 2011 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Wed Feb 23 11:42:01 2011 +0100
@@ -19,9 +19,8 @@
\cite[\S6]{Winskel:1993}. See also @{file "~~/src/HOL/Hoare"} and
\cite{Nipkow:1998:Winskel}. *}
-types
- 'a bexp = "'a set"
- 'a assn = "'a set"
+type_synonym 'a bexp = "'a set"
+type_synonym 'a assn = "'a set"
datatype 'a com =
Basic "'a => 'a"
@@ -32,8 +31,7 @@
abbreviation Skip ("SKIP")
where "SKIP == Basic id"
-types
- 'a sem = "'a => 'a => bool"
+type_synonym 'a sem = "'a => 'a => bool"
primrec iter :: "nat => 'a bexp => 'a sem => 'a sem"
where
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Wed Feb 23 11:40:18 2011 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Wed Feb 23 11:42:01 2011 +0100
@@ -256,7 +256,7 @@
record tstate = time :: nat
-types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
+type_synonym 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
primrec timeit :: "'a time com \<Rightarrow> 'a time com"
where
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 23 11:40:18 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 23 11:42:01 2011 +0100
@@ -178,12 +178,6 @@
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \
\option (e.g., \"timeout = " ^
string_of_int (10 + msecs div 1000) ^ "\").")
- | {outcome = SOME (UnknownError _), ...} =>
- (* Failure sometimes mean timeout, unfortunately. *)
- (NONE, "Failure: No proof was found with the current time limit. You \
- \can increase the time limit using the \"timeout\" \
- \option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ "\").")
| {message, ...} => (NONE, "Prover error: " ^ message))
handle ERROR msg => (NONE, "Error: " ^ msg)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Case_Product.thy Wed Feb 23 11:42:01 2011 +0100
@@ -0,0 +1,30 @@
+(* Title: HOL/ex/Case_Product.thy
+ Author: Lars Noschinski
+ Copyright 2011 TU Muenchen
+*)
+
+header {* Examples for the 'case_product' attribute *}
+
+theory Case_Product
+imports Main
+begin
+
+text {*
+ The {@attribute case_product} attribute combines multiple case distinction
+ lemmas into a single case distinction lemma by building the product of all
+ these case distinctions.
+*}
+
+lemmas nat_list_exhaust = nat.exhaust[case_product list.exhaust]
+
+text {*
+ The attribute honors preconditions
+*}
+
+lemmas trancl_acc_cases= trancl.cases[case_product acc.cases]
+
+text {*
+ Also, case names are generated based on the old names
+*}
+
+end
--- a/src/HOL/ex/Fundefs.thy Wed Feb 23 11:40:18 2011 +0100
+++ b/src/HOL/ex/Fundefs.thy Wed Feb 23 11:42:01 2011 +0100
@@ -280,14 +280,12 @@
(* There were some problems with fresh names\<dots> *)
-(* FIXME: tailrec? *)
function k :: "nat \<Rightarrow> nat"
where
"k x = (let a = x; b = x in k x)"
by pat_completeness auto
-(* FIXME: tailrec? *)
function f2 :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
where
"f2 p = (let (x,y) = p in f2 (y,x))"
--- a/src/Pure/goal.ML Wed Feb 23 11:40:18 2011 +0100
+++ b/src/Pure/goal.ML Wed Feb 23 11:42:01 2011 +0100
@@ -138,7 +138,7 @@
(* scheduling parameters *)
val parallel_proofs = Unsynchronized.ref 1;
-val parallel_proofs_threshold = Unsynchronized.ref 100;
+val parallel_proofs_threshold = Unsynchronized.ref 50;
fun future_enabled () =
Multithreading.enabled () andalso ! parallel_proofs >= 1 andalso
@@ -146,7 +146,8 @@
fun local_future_enabled () =
future_enabled () andalso ! parallel_proofs >= 2 andalso
- Synchronized.value forked_proofs < ! parallel_proofs_threshold;
+ Synchronized.value forked_proofs <
+ ! parallel_proofs_threshold * Multithreading.max_threads_value ();
(* future_result *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/case_product.ML Wed Feb 23 11:42:01 2011 +0100
@@ -0,0 +1,117 @@
+(* Title: case_product.ML
+ Author: Lars Noschinski
+
+Combines two case rules into a single one.
+
+Assumes that the theorems are of the form
+ "[| C1; ...; Cm; A1 ==> P; ...; An ==> P |] ==> P"
+where m is given by the "consumes" attribute of the theorem.
+*)
+
+signature CASE_PRODUCT =
+ sig
+
+ val combine: Proof.context -> thm -> thm -> thm
+ val combine_annotated: Proof.context -> thm -> thm -> thm
+ val setup: theory -> theory
+end;
+
+structure Case_Product: CASE_PRODUCT =
+struct
+
+(*Instantiates the conclusion of thm2 to the one of thm1.*)
+fun inst_concl thm1 thm2 =
+ let
+ val cconcl_of = Drule.strip_imp_concl o Thm.cprop_of
+ in Thm.instantiate (Thm.match (cconcl_of thm2, cconcl_of thm1)) thm2 end
+
+fun inst_thms thm1 thm2 ctxt =
+ let
+ val import = yield_singleton (apfst snd oo Variable.import true)
+ val (i_thm1, ctxt') = import thm1 ctxt
+ val (i_thm2, ctxt'') = import (inst_concl i_thm1 thm2) ctxt'
+ in ((i_thm1, i_thm2), ctxt'') end
+
+(*
+Returns list of prems, where loose bounds have been replaced by frees.
+FIXME: Focus
+*)
+fun free_prems t ctxt =
+ let
+ val bs = Term.strip_all_vars t
+ val (names, ctxt') = Variable.variant_fixes (map fst bs) ctxt
+ val subst = map Free (names ~~ map snd bs)
+ val t' = map (Term.subst_bounds o pair (rev subst)) (Logic.strip_assums_hyp t)
+ in ((t', subst), ctxt') end
+
+fun build_concl_prems thm1 thm2 ctxt =
+ let
+ val concl = Thm.concl_of thm1
+
+ fun is_consumes t = not (Logic.strip_assums_concl t aconv concl)
+ val (p_cons1, p_cases1) = chop_while is_consumes (Thm.prems_of thm1)
+ val (p_cons2, p_cases2) = chop_while is_consumes (Thm.prems_of thm2)
+
+ val p_cases_prod = map (fn p1 => map (fn p2 =>
+ let
+ val (((t1, subst1), (t2, subst2)), _) = ctxt
+ |> free_prems p1 ||>> free_prems p2
+ in
+ Logic.list_implies (t1 @ t2, concl)
+ |> fold_rev Logic.all (subst1 @ subst2)
+ end
+ ) p_cases2) p_cases1
+
+ val prems = p_cons1 :: p_cons2 :: p_cases_prod
+ in
+ (concl, prems)
+ end
+
+fun case_product_tac prems struc thm1 thm2 =
+ let
+ val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
+ val thm2' = thm2 OF p_cons2
+ in
+ (Tactic.rtac (thm1 OF p_cons1)
+ THEN' EVERY' (map (fn p =>
+ Tactic.rtac thm2'
+ THEN' EVERY' (map (ProofContext.fact_tac o single) p)) premss)
+ )
+ end
+
+fun combine ctxt thm1 thm2 =
+ let
+ val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt
+ val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt'
+ in
+ Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
+ case_product_tac prems prems_rich i_thm1 i_thm2 1)
+ |> singleton (Variable.export ctxt' ctxt)
+ end;
+
+fun annotation thm1 thm2 =
+ let
+ val (names1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
+ val (names2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
+ val names = map_product (fn x => fn y => x ^ "_" ^y) names1 names2
+ in
+ Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2)
+ end
+
+fun combine_annotated ctxt thm1 thm2 =
+ combine ctxt thm1 thm2
+ |> snd o annotation thm1 thm2 o pair (Context.Proof ctxt)
+
+(* Attribute setup *)
+
+val case_prod_attr = let
+ fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
+ in
+ Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
+ combine_list (Context.proof_of ctxt) thms thm))
+ end
+
+val setup =
+ Attrib.setup @{binding "case_product"} case_prod_attr "product with other case rules"
+
+end;