--- a/NEWS Mon Jul 20 16:49:05 2009 +0200
+++ b/NEWS Mon Jul 20 16:50:59 2009 +0200
@@ -128,6 +128,9 @@
* Removed "compress" option from isabelle-process and isabelle usedir;
this is always enabled.
+* More fine-grained control of proof parallelism, cf.
+Goal.parallel_proofs in ML and usedir option -q LEVEL.
+
New in Isabelle2009 (April 2009)
--- a/doc-src/System/Thy/Presentation.thy Mon Jul 20 16:49:05 2009 +0200
+++ b/doc-src/System/Thy/Presentation.thy Mon Jul 20 16:50:59 2009 +0200
@@ -451,7 +451,8 @@
-g BOOL generate session graph image for document (default false)
-i BOOL generate theory browser information (default false)
-m MODE add print mode for output
- -p LEVEL set level of detail for proof objects
+ -p LEVEL set level of detail for proof objects (default 0)
+ -q LEVEL set level of parallel proof checking (default 1)
-r reset session path
-s NAME override session NAME
-t BOOL internal session timing (default false)
@@ -564,6 +565,12 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \medskip The @{verbatim "-q"} option specifies the level of parallel
+ proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel
+ proofs (default), @{verbatim 2} toplevel and nested Isar proofs.
+ The resulting speedup may vary, depending on the number of worker
+ threads, granularity of proofs, and whether proof terms are enabled.
+
\medskip The @{verbatim "-t"} option produces a more detailed
internal timing report of the session.
@@ -583,13 +590,6 @@
bottle-necks, e.g.\ due to excessive wait states when locking
critical code sections.
- \medskip The @{verbatim "-Q"} option tells whether individual proofs
- should be checked in parallel; the default is @{verbatim true}.
- Note that fine-grained proof parallelism requires considerable
- amounts of extra memory, since full proof context information is
- maintained for each independent derivation thread, until checking is
- completed.
-
\medskip Any @{tool usedir} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend
on others. For example, consider @{verbatim "Pure/FOL/ex"}, which
--- a/doc-src/System/Thy/document/Presentation.tex Mon Jul 20 16:49:05 2009 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex Mon Jul 20 16:50:59 2009 +0200
@@ -477,7 +477,8 @@
-g BOOL generate session graph image for document (default false)
-i BOOL generate theory browser information (default false)
-m MODE add print mode for output
- -p LEVEL set level of detail for proof objects
+ -p LEVEL set level of detail for proof objects (default 0)
+ -q LEVEL set level of parallel proof checking (default 1)
-r reset session path
-s NAME override session NAME
-t BOOL internal session timing (default false)
@@ -581,6 +582,12 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \medskip The \verb|-q| option specifies the level of parallel
+ proof checking: \verb|0| no proofs, \verb|1| toplevel
+ proofs (default), \verb|2| toplevel and nested Isar proofs.
+ The resulting speedup may vary, depending on the number of worker
+ threads, granularity of proofs, and whether proof terms are enabled.
+
\medskip The \verb|-t| option produces a more detailed
internal timing report of the session.
@@ -599,13 +606,6 @@
bottle-necks, e.g.\ due to excessive wait states when locking
critical code sections.
- \medskip The \verb|-Q| option tells whether individual proofs
- should be checked in parallel; the default is \verb|true|.
- Note that fine-grained proof parallelism requires considerable
- amounts of extra memory, since full proof context information is
- maintained for each independent derivation thread, until checking is
- completed.
-
\medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend
on others. For example, consider \verb|Pure/FOL/ex|, which
--- a/etc/settings Mon Jul 20 16:49:05 2009 +0200
+++ b/etc/settings Mon Jul 20 16:50:59 2009 +0200
@@ -96,7 +96,7 @@
# Specifically for the HOL image
HOL_USEDIR_OPTIONS=""
-#HOL_USEDIR_OPTIONS="-p 2 -Q false"
+#HOL_USEDIR_OPTIONS="-p 2 -q 1"
#Source file identification (default: full name + date stamp)
ISABELLE_FILE_IDENT=""
--- a/lib/Tools/usedir Mon Jul 20 16:49:05 2009 +0200
+++ b/lib/Tools/usedir Mon Jul 20 16:50:59 2009 +0200
@@ -19,7 +19,6 @@
echo " -D PATH dump generated document sources into PATH"
echo " -M MAX multithreading: maximum number of worker threads (default 1)"
echo " -P PATH set path for remote theory browsing information"
- echo " -Q BOOL check proofs in parallel (default true)"
echo " -T LEVEL multithreading: trace level (default 0)"
echo " -V VERSION declare alternative document VERSION"
echo " -b build mode (output heap image, using current dir)"
@@ -28,7 +27,8 @@
echo " -g BOOL generate session graph image for document (default false)"
echo " -i BOOL generate HTML and graph browser information (default false)"
echo " -m MODE add print mode for output"
- echo " -p LEVEL set level of detail for proof objects"
+ echo " -p LEVEL set level of detail for proof objects (default 0)"
+ echo " -q LEVEL set level of parallel proof checking (default 1)"
echo " -r reset session path"
echo " -s NAME override session NAME"
echo " -t BOOL internal session timing (default false)"
@@ -73,7 +73,6 @@
DUMP=""
MAXTHREADS="1"
RPATH=""
-PARALLEL_PROOFS="true"
TRACETHREADS="0"
DOCUMENT_VERSIONS=""
BUILD=""
@@ -84,14 +83,15 @@
MODES=""
RESET=false
SESSION=""
-PROOFS=0
+PROOFS="0"
+PARALLEL_PROOFS="1"
TIMING=false
VERBOSE=false
function getoptions()
{
OPTIND=1
- while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:t:v:" OPT
+ while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
do
case "$OPT" in
C)
@@ -112,9 +112,6 @@
P)
RPATH="$OPTARG"
;;
- Q)
- PARALLEL_PROOFS="$OPTARG"
- ;;
T)
check_number "$OPTARG"
TRACETHREADS="$OPTARG"
@@ -154,6 +151,10 @@
check_number "$OPTARG"
PROOFS="$OPTARG"
;;
+ q)
+ check_number "$OPTARG"
+ PARALLEL_PROOFS="$OPTARG"
+ ;;
r)
RESET=true
;;
--- a/src/HOL/Set.thy Mon Jul 20 16:49:05 2009 +0200
+++ b/src/HOL/Set.thy Mon Jul 20 16:50:59 2009 +0200
@@ -8,9 +8,7 @@
imports Lattices
begin
-text {* A set in HOL is simply a predicate. *}
-
-subsection {* Basic definitions and syntax *}
+subsection {* Sets as predicates *}
global
@@ -49,34 +47,48 @@
not_mem ("op \<notin>") and
not_mem ("(_/ \<notin> _)" [50, 51] 50)
+text {* Set comprehensions *}
+
syntax
"@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})")
translations
"{x. P}" == "Collect (%x. P)"
-definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
- "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
-
-definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
- "A Un B \<equiv> {x. x \<in> A \<or> x \<in> B}"
-
-notation (xsymbols)
- "Int" (infixl "\<inter>" 70) and
- "Un" (infixl "\<union>" 65)
-
-notation (HTML output)
- "Int" (infixl "\<inter>" 70) and
- "Un" (infixl "\<union>" 65)
+syntax
+ "@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})")
+ "@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ :/ _./ _})")
+
+syntax (xsymbols)
+ "@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ \<in>/ _./ _})")
+
+translations
+ "{x:A. P}" => "{x. x:A & P}"
+
+lemma mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
+ by (simp add: Collect_def mem_def)
+
+lemma Collect_mem_eq [simp]: "{x. x:A} = A"
+ by (simp add: Collect_def mem_def)
+
+lemma CollectI: "P(a) ==> a : {x. P(x)}"
+ by simp
+
+lemma CollectD: "a : {x. P(x)} ==> P(a)"
+ by simp
+
+lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
+ by simp
+
+lemmas CollectE = CollectD [elim_format]
+
+text {* Set enumerations *}
definition empty :: "'a set" ("{}") where
"empty \<equiv> {x. False}"
definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "insert a B \<equiv> {x. x = a} \<union> B"
-
-definition UNIV :: "'a set" where
- "UNIV \<equiv> {x. True}"
+ insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
syntax
"@Finset" :: "args => 'a set" ("{(_)}")
@@ -85,6 +97,49 @@
"{x, xs}" == "CONST insert x {xs}"
"{x}" == "CONST insert x {}"
+
+subsection {* Subsets and bounded quantifiers *}
+
+abbreviation
+ subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+ "subset \<equiv> less"
+
+abbreviation
+ subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+ "subset_eq \<equiv> less_eq"
+
+notation (output)
+ subset ("op <") and
+ subset ("(_/ < _)" [50, 51] 50) and
+ subset_eq ("op <=") and
+ subset_eq ("(_/ <= _)" [50, 51] 50)
+
+notation (xsymbols)
+ subset ("op \<subset>") and
+ subset ("(_/ \<subset> _)" [50, 51] 50) and
+ subset_eq ("op \<subseteq>") and
+ subset_eq ("(_/ \<subseteq> _)" [50, 51] 50)
+
+notation (HTML output)
+ subset ("op \<subset>") and
+ subset ("(_/ \<subset> _)" [50, 51] 50) and
+ subset_eq ("op \<subseteq>") and
+ subset_eq ("(_/ \<subseteq> _)" [50, 51] 50)
+
+abbreviation (input)
+ supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+ "supset \<equiv> greater"
+
+abbreviation (input)
+ supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+ "supset_eq \<equiv> greater_eq"
+
+notation (xsymbols)
+ supset ("op \<supset>") and
+ supset ("(_/ \<supset> _)" [50, 51] 50) and
+ supset_eq ("op \<supseteq>") and
+ supset_eq ("(_/ \<supseteq> _)" [50, 51] 50)
+
global
consts
@@ -127,63 +182,6 @@
"EX! x:A. P" == "Bex1 A (%x. P)"
"LEAST x:A. P" => "LEAST x. x:A & P"
-
-subsection {* Additional concrete syntax *}
-
-syntax
- "@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})")
- "@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ :/ _./ _})")
-
-syntax (xsymbols)
- "@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ \<in>/ _./ _})")
-
-translations
- "{x:A. P}" => "{x. x:A & P}"
-
-abbreviation
- subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- "subset \<equiv> less"
-
-abbreviation
- subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- "subset_eq \<equiv> less_eq"
-
-notation (output)
- subset ("op <") and
- subset ("(_/ < _)" [50, 51] 50) and
- subset_eq ("op <=") and
- subset_eq ("(_/ <= _)" [50, 51] 50)
-
-notation (xsymbols)
- subset ("op \<subset>") and
- subset ("(_/ \<subset> _)" [50, 51] 50) and
- subset_eq ("op \<subseteq>") and
- subset_eq ("(_/ \<subseteq> _)" [50, 51] 50)
-
-notation (HTML output)
- subset ("op \<subset>") and
- subset ("(_/ \<subset> _)" [50, 51] 50) and
- subset_eq ("op \<subseteq>") and
- subset_eq ("(_/ \<subseteq> _)" [50, 51] 50)
-
-abbreviation (input)
- supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- "supset \<equiv> greater"
-
-abbreviation (input)
- supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- "supset_eq \<equiv> greater_eq"
-
-notation (xsymbols)
- supset ("op \<supset>") and
- supset ("(_/ \<supset> _)" [50, 51] 50) and
- supset_eq ("op \<supseteq>") and
- supset_eq ("(_/ \<supseteq> _)" [50, 51] 50)
-
-
-
-subsubsection "Bounded quantifiers"
-
syntax (output)
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10)
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10)
@@ -313,31 +311,6 @@
in [("Collect", setcompr_tr')] end;
*}
-
-subsection {* Lemmas and proof tool setup *}
-
-subsubsection {* Relating predicates and sets *}
-
-lemma mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
- by (simp add: Collect_def mem_def)
-
-lemma Collect_mem_eq [simp]: "{x. x:A} = A"
- by (simp add: Collect_def mem_def)
-
-lemma CollectI: "P(a) ==> a : {x. P(x)}"
- by simp
-
-lemma CollectD: "a : {x. P(x)} ==> P(a)"
- by simp
-
-lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
- by simp
-
-lemmas CollectE = CollectD [elim_format]
-
-
-subsubsection {* Bounded quantifiers *}
-
lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
by (simp add: Ball_def)
@@ -428,8 +401,7 @@
Addsimprocs [defBALL_regroup, defBEX_regroup];
*}
-
-subsubsection {* Congruence rules *}
+text {* Congruence rules *}
lemma ball_cong:
"A = B ==> (!!x. x:B ==> P x = Q x) ==>
@@ -452,6 +424,8 @@
by (simp add: simp_implies_def Bex_def cong: conj_cong)
+subsection {* Basic operations *}
+
subsubsection {* Subsets *}
lemma subsetI [atp,intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B"
@@ -499,10 +473,19 @@
by blast
lemma subset_refl [simp,atp]: "A \<subseteq> A"
- by fast
+ by (fact order_refl)
lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
- by blast
+ by (fact order_trans)
+
+lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B"
+ by (rule subsetD)
+
+lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
+ by (rule subsetD)
+
+lemmas basic_trans_rules [trans] =
+ order_trans_rules set_rev_mp set_mp
subsubsection {* Equality *}
@@ -554,6 +537,9 @@
subsubsection {* The universal set -- UNIV *}
+definition UNIV :: "'a set" where
+ "UNIV \<equiv> {x. True}"
+
lemma UNIV_I [simp]: "x : UNIV"
by (simp add: UNIV_def)
@@ -565,6 +551,9 @@
lemma subset_UNIV [simp]: "A \<subseteq> UNIV"
by (rule subsetI) (rule UNIV_I)
+lemma top_set_eq: "top = UNIV"
+ by (iprover intro!: subset_antisym subset_UNIV top_greatest)
+
text {*
\medskip Eta-contracting these two rules (to remove @{text P})
causes them to be ignored because of their interaction with
@@ -593,11 +582,14 @@
-- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
by blast
+lemma bot_set_eq: "bot = {}"
+ by (iprover intro!: subset_antisym empty_subsetI bot_least)
+
lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
by blast
lemma equals0D: "A = {} ==> a \<notin> A"
- -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *}
+ -- {* Use for reasoning about disjointness: @{text "A Int B = {}"} *}
by blast
lemma ball_empty [simp]: "Ball {} P = True"
@@ -654,6 +646,18 @@
subsubsection {* Binary union -- Un *}
+definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
+ "A Un B \<equiv> {x. x \<in> A \<or> x \<in> B}"
+
+notation (xsymbols)
+ "Un" (infixl "\<union>" 65)
+
+notation (HTML output)
+ "Un" (infixl "\<union>" 65)
+
+lemma sup_set_eq: "sup A B = A \<union> B"
+ by (simp add: sup_fun_eq sup_bool_eq Un_def Collect_def mem_def)
+
lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
by (unfold Un_def) blast
@@ -674,9 +678,29 @@
lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
by (unfold Un_def) blast
+lemma insert_def: "insert a B \<equiv> {x. x = a} \<union> B"
+ by (simp add: Collect_def mem_def insert_compr Un_def)
+
+lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
+ apply (fold sup_set_eq)
+ apply (erule mono_sup)
+ done
+
subsubsection {* Binary intersection -- Int *}
+definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
+ "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
+
+notation (xsymbols)
+ "Int" (infixl "\<inter>" 70)
+
+notation (HTML output)
+ "Int" (infixl "\<inter>" 70)
+
+lemma inf_set_eq: "inf A B = A \<inter> B"
+ by (simp add: inf_fun_eq inf_bool_eq Int_def Collect_def mem_def)
+
lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
by (unfold Int_def) blast
@@ -692,6 +716,11 @@
lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
by simp
+lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
+ apply (fold inf_set_eq)
+ apply (erule mono_inf)
+ done
+
subsubsection {* Set difference *}
@@ -854,6 +883,76 @@
by blast
+subsubsection {* Some proof tools *}
+
+text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
+
+lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
+by auto
+
+lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
+by auto
+
+text {*
+Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
+to the front (and similarly for @{text "t=x"}):
+*}
+
+ML{*
+ local
+ val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
+ ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
+ DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
+ in
+ val defColl_regroup = Simplifier.simproc @{theory}
+ "defined Collect" ["{x. P x & Q x}"]
+ (Quantifier1.rearrange_Coll Coll_perm_tac)
+ end;
+
+ Addsimprocs [defColl_regroup];
+*}
+
+text {*
+ Rewrite rules for boolean case-splitting: faster than @{text
+ "split_if [split]"}.
+*}
+
+lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"
+ by (rule split_if)
+
+lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"
+ by (rule split_if)
+
+text {*
+ Split ifs on either side of the membership relation. Not for @{text
+ "[simp]"} -- can cause goals to blow up!
+*}
+
+lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"
+ by (rule split_if)
+
+lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"
+ by (rule split_if [where P="%S. a : S"])
+
+lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
+
+(*Would like to add these, but the existing code only searches for the
+ outer-level constant, which in this case is just "op :"; we instead need
+ to use term-nets to associate patterns with rules. Also, if a rule fails to
+ apply, then the formula should be kept.
+ [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]),
+ ("Int", [IntD1,IntD2]),
+ ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
+ *)
+
+ML {*
+ val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
+*}
+declaration {* fn _ =>
+ Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
+*}
+
+
subsection {* Complete lattices *}
notation
@@ -989,7 +1088,7 @@
end
-subsection {* Bool as complete lattice *}
+subsubsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
instantiation bool :: complete_lattice
begin
@@ -1013,9 +1112,6 @@
"\<not> \<Squnion>{}"
unfolding Sup_bool_def by auto
-
-subsection {* Fun as complete lattice *}
-
instantiation "fun" :: (type, complete_lattice) complete_lattice
begin
@@ -1040,47 +1136,24 @@
by rule (simp add: Sup_fun_def, simp add: empty_def)
-subsection {* Set as lattice *}
-
-definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
- "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
+subsubsection {* Unions of families *}
definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
"UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
-definition Inter :: "'a set set \<Rightarrow> 'a set" where
- "Inter S \<equiv> INTER S (\<lambda>x. x)"
-
-definition Union :: "'a set set \<Rightarrow> 'a set" where
- "Union S \<equiv> UNION S (\<lambda>x. x)"
-
-notation (xsymbols)
- Inter ("\<Inter>_" [90] 90) and
- Union ("\<Union>_" [90] 90)
-
syntax
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 10] 10)
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 10] 10)
syntax (xsymbols)
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" [0, 10] 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
syntax (latex output)
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
translations
- "INT x y. B" == "INT x. INT y. B"
- "INT x. B" == "CONST INTER CONST UNIV (%x. B)"
- "INT x. B" == "INT x:CONST UNIV. B"
- "INT x:A. B" == "CONST INTER A (%x. B)"
"UN x y. B" == "UN x. UN y. B"
"UN x. B" == "CONST UNION CONST UNIV (%x. B)"
"UN x. B" == "UN x:CONST UNIV. B"
@@ -1101,86 +1174,9 @@
fun btr' syn [A, Abs abs] =
let val (x, t) = atomic_abs_tr' abs
in Syntax.const syn $ x $ A $ t end
-in [(@{const_syntax UNION}, btr' "@UNION"),(@{const_syntax INTER}, btr' "@INTER")] end
+in [(@{const_syntax UNION}, btr' "@UNION")] end
*}
-lemma Inter_image_eq [simp]:
- "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
- by (auto simp add: Inter_def INTER_def image_def)
-
-lemma Union_image_eq [simp]:
- "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
- by (auto simp add: Union_def UNION_def image_def)
-
-lemma inf_set_eq: "A \<sqinter> B = A \<inter> B"
- by (simp add: inf_fun_eq inf_bool_eq Int_def Collect_def mem_def)
-
-lemma sup_set_eq: "A \<squnion> B = A \<union> B"
- by (simp add: sup_fun_eq sup_bool_eq Un_def Collect_def mem_def)
-
-lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
- apply (fold inf_set_eq sup_set_eq)
- apply (erule mono_inf)
- done
-
-lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
- apply (fold inf_set_eq sup_set_eq)
- apply (erule mono_sup)
- done
-
-lemma top_set_eq: "top = UNIV"
- by (iprover intro!: subset_antisym subset_UNIV top_greatest)
-
-lemma bot_set_eq: "bot = {}"
- by (iprover intro!: subset_antisym empty_subsetI bot_least)
-
-lemma Inter_eq:
- "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
- by (simp add: Inter_def INTER_def)
-
-lemma Union_eq:
- "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
- by (simp add: Union_def UNION_def)
-
-lemma Inf_set_eq:
- "\<Sqinter>S = \<Inter>S"
-proof (rule set_ext)
- fix x
- have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
- by auto
- then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
- by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
-qed
-
-lemma Sup_set_eq:
- "\<Squnion>S = \<Union>S"
-proof (rule set_ext)
- fix x
- have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
- by auto
- then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
- by (simp add: Union_eq Sup_fun_def Sup_bool_def) (simp add: mem_def)
-qed
-
-lemma INFI_set_eq:
- "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
- by (simp add: INFI_def Inf_set_eq)
-
-lemma SUPR_set_eq:
- "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
- by (simp add: SUPR_def Sup_set_eq)
-
-no_notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50) and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter>_" [900] 900) and
- Sup ("\<Squnion>_" [900] 900)
-
-
-subsubsection {* Unions of families *}
-
declare UNION_def [noatp]
lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
@@ -1208,6 +1204,36 @@
subsubsection {* Intersections of families *}
+definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+ "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
+
+syntax
+ "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
+ "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 10] 10)
+
+syntax (xsymbols)
+ "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
+ "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
+
+syntax (latex output)
+ "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+ "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
+
+translations
+ "INT x y. B" == "INT x. INT y. B"
+ "INT x. B" == "CONST INTER CONST UNIV (%x. B)"
+ "INT x. B" == "INT x:CONST UNIV. B"
+ "INT x:A. B" == "CONST INTER A (%x. B)"
+
+(* To avoid eta-contraction of body: *)
+print_translation {*
+let
+ fun btr' syn [A, Abs abs] =
+ let val (x, t) = atomic_abs_tr' abs
+ in Syntax.const syn $ x $ A $ t end
+in [(@{const_syntax INTER}, btr' "@INTER")] end
+*}
+
lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
by (unfold INTER_def) blast
@@ -1228,6 +1254,34 @@
subsubsection {* Union *}
+definition Union :: "'a set set \<Rightarrow> 'a set" where
+ "Union S \<equiv> UNION S (\<lambda>x. x)"
+
+notation (xsymbols)
+ Union ("\<Union>_" [90] 90)
+
+lemma Union_image_eq [simp]:
+ "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
+ by (auto simp add: Union_def UNION_def image_def)
+
+lemma Union_eq:
+ "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
+ by (simp add: Union_def UNION_def)
+
+lemma Sup_set_eq:
+ "\<Squnion>S = \<Union>S"
+proof (rule set_ext)
+ fix x
+ have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
+ by auto
+ then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
+ by (simp add: Union_eq Sup_fun_def Sup_bool_def) (simp add: mem_def)
+qed
+
+lemma SUPR_set_eq:
+ "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
+ by (simp add: SUPR_def Sup_set_eq)
+
lemma Union_iff [simp,noatp]: "(A : Union C) = (EX X:C. A:X)"
by (unfold Union_def) blast
@@ -1242,6 +1296,34 @@
subsubsection {* Inter *}
+definition Inter :: "'a set set \<Rightarrow> 'a set" where
+ "Inter S \<equiv> INTER S (\<lambda>x. x)"
+
+notation (xsymbols)
+ Inter ("\<Inter>_" [90] 90)
+
+lemma Inter_image_eq [simp]:
+ "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
+ by (auto simp add: Inter_def INTER_def image_def)
+
+lemma Inter_eq:
+ "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
+ by (simp add: Inter_def INTER_def)
+
+lemma Inf_set_eq:
+ "\<Sqinter>S = \<Inter>S"
+proof (rule set_ext)
+ fix x
+ have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
+ by auto
+ then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
+ by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
+qed
+
+lemma INFI_set_eq:
+ "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
+ by (simp add: INFI_def Inf_set_eq)
+
lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
by (unfold Inter_def) blast
@@ -1263,75 +1345,16 @@
by (unfold Inter_def) blast
-subsubsection {* Set reasoning tools *}
-
-text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
-
-lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
-by auto
-
-lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
-by auto
-
-text {*
-Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
-to the front (and similarly for @{text "t=x"}):
-*}
-
-ML{*
- local
- val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
- ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
- DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
- in
- val defColl_regroup = Simplifier.simproc @{theory}
- "defined Collect" ["{x. P x & Q x}"]
- (Quantifier1.rearrange_Coll Coll_perm_tac)
- end;
-
- Addsimprocs [defColl_regroup];
-*}
-
-text {*
- Rewrite rules for boolean case-splitting: faster than @{text
- "split_if [split]"}.
-*}
-
-lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"
- by (rule split_if)
-
-lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"
- by (rule split_if)
-
-text {*
- Split ifs on either side of the membership relation. Not for @{text
- "[simp]"} -- can cause goals to blow up!
-*}
-
-lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"
- by (rule split_if)
-
-lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"
- by (rule split_if [where P="%S. a : S"])
-
-lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
-
-(*Would like to add these, but the existing code only searches for the
- outer-level constant, which in this case is just "op :"; we instead need
- to use term-nets to associate patterns with rules. Also, if a rule fails to
- apply, then the formula should be kept.
- [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]),
- ("Int", [IntD1,IntD2]),
- ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
- *)
-
-ML {*
- val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
-*}
-declaration {* fn _ =>
- Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
-*}
-
+no_notation
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50) and
+ inf (infixl "\<sqinter>" 70) and
+ sup (infixl "\<squnion>" 65) and
+ Inf ("\<Sqinter>_" [900] 900) and
+ Sup ("\<Squnion>_" [900] 900)
+
+
+subsection {* Further operations and lemmas *}
subsubsection {* The ``proper subset'' relation *}
@@ -1378,9 +1401,6 @@
lemmas [symmetric, rulify] = atomize_ball
and [symmetric, defn] = atomize_ball
-
-subsection {* Further set-theory lemmas *}
-
subsubsection {* Derived rules involving subsets. *}
text {* @{text insert}. *}
@@ -2334,15 +2354,12 @@
by iprover
-subsection {* Inverse image of a function *}
+subsubsection {* Inverse image of a function *}
constdefs
vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90)
[code del]: "f -` B == {x. f x : B}"
-
-subsubsection {* Basic rules *}
-
lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
by (unfold vimage_def) blast
@@ -2361,9 +2378,6 @@
lemma vimageD: "a : f -` A ==> f a : A"
by (unfold vimage_def) fast
-
-subsubsection {* Equations *}
-
lemma vimage_empty [simp]: "f -` {} = {}"
by blast
@@ -2428,7 +2442,7 @@
by blast
-subsection {* Getting the Contents of a Singleton Set *}
+subsubsection {* Getting the Contents of a Singleton Set *}
definition contents :: "'a set \<Rightarrow> 'a" where
[code del]: "contents X = (THE x. X = {x})"
@@ -2437,19 +2451,7 @@
by (simp add: contents_def)
-subsection {* Transitivity rules for calculational reasoning *}
-
-lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B"
- by (rule subsetD)
-
-lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
- by (rule subsetD)
-
-lemmas basic_trans_rules [trans] =
- order_trans_rules set_rev_mp set_mp
-
-
-subsection {* Least value operator *}
+subsubsection {* Least value operator *}
lemma Least_mono:
"mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
@@ -2461,8 +2463,9 @@
apply (auto elim: monoD intro!: order_antisym)
done
-
-subsection {* Rudimentary code generation *}
+subsection {* Misc *}
+
+text {* Rudimentary code generation *}
lemma empty_code [code]: "{} x \<longleftrightarrow> False"
unfolding empty_def Collect_def ..
@@ -2482,8 +2485,7 @@
lemma vimage_code [code]: "(f -` A) x = A (f x)"
unfolding vimage_def Collect_def mem_def ..
-
-subsection {* Misc theorem and ML bindings *}
+text {* Misc theorem and ML bindings *}
lemmas equalityI = subset_antisym
lemmas mem_simps =
--- a/src/HOL/Tools/Function/fundef_core.ML Mon Jul 20 16:49:05 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML Mon Jul 20 16:50:59 2009 +0200
@@ -176,7 +176,7 @@
end
-(* lowlevel term function *)
+(* lowlevel term function. FIXME: remove *)
fun abstract_over_list vs body =
let
fun abs lev v tm =
@@ -184,12 +184,10 @@
else
(case tm of
Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
- | t $ u =>
- (abs lev v t $ (abs lev v u handle Same.SAME => u)
- handle Same.SAME => t $ abs lev v u)
- | _ => raise Same.SAME);
+ | t $ u => abs lev v t $ abs lev v u
+ | t => t);
in
- fold_index (fn (i, v) => fn t => abs i v t handle Same.SAME => t) vs body
+ fold_index (fn (i, v) => fn t => abs i v t) vs body
end
--- a/src/Pure/Concurrent/future.ML Mon Jul 20 16:49:05 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Jul 20 16:50:59 2009 +0200
@@ -29,7 +29,7 @@
val enabled: unit -> bool
type task = Task_Queue.task
type group = Task_Queue.group
- val thread_data: unit -> (string * task) option
+ val is_worker: unit -> bool
type 'a future
val task_of: 'a future -> task
val group_of: 'a future -> group
@@ -40,6 +40,7 @@
val fork_group: group -> (unit -> 'a) -> 'a future
val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
val fork_pri: int -> (unit -> 'a) -> 'a future
+ val fork_local: int -> (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
val join_result: 'a future -> 'a Exn.result
val join: 'a future -> 'a
@@ -66,11 +67,16 @@
type task = Task_Queue.task;
type group = Task_Queue.group;
-local val tag = Universal.tag () : (string * task) option Universal.tag in
+local
+ val tag = Universal.tag () : (string * task * group) option Universal.tag;
+in
fun thread_data () = the_default NONE (Thread.getLocal tag);
- fun setmp_thread_data data f x = Library.setmp_thread_data tag (thread_data ()) (SOME data) f x;
+ fun setmp_thread_data data f x =
+ Library.setmp_thread_data tag (thread_data ()) (SOME data) f x;
end;
+val is_worker = is_some o thread_data;
+
(* datatype future *)
@@ -148,7 +154,7 @@
let
val _ = trace_active ();
val valid = Task_Queue.is_valid group;
- val ok = setmp_thread_data (name, task) (fn () =>
+ val ok = setmp_thread_data (name, task, group) (fn () =>
fold (fn job => fn ok => job valid andalso ok) jobs true) ();
val _ = SYNCHRONIZED "execute" (fn () =>
(change queue (Task_Queue.finish task);
@@ -277,6 +283,7 @@
fun fork_group group e = fork_future (SOME group) [] 0 e;
fun fork_deps deps e = fork_future NONE (map task_of deps) 0 e;
fun fork_pri pri e = fork_future NONE [] pri e;
+fun fork_local pri e = fork_future (Option.map #3 (thread_data ())) [] pri e;
(* join *)
@@ -285,21 +292,10 @@
fun get_result x = the_default (Exn.Exn (SYS_ERROR "unfinished future")) (peek x);
-fun join_wait x =
- if SYNCHRONIZED "join_wait" (fn () => is_finished x orelse (wait (); false))
- then () else join_wait x;
-
-fun join_next x = (*requires SYNCHRONIZED*)
- if is_finished x then NONE
- else
- (case change_result queue Task_Queue.dequeue of
- NONE => (worker_wait (); join_next x)
- | some => some);
-
-fun join_loop x =
- (case SYNCHRONIZED "join" (fn () => join_next x) of
+fun join_deps deps =
+ (case SYNCHRONIZED "join" (fn () => change_result queue (Task_Queue.dequeue_towards deps)) of
NONE => ()
- | SOME work => (execute "join" work; join_loop x));
+ | SOME (work, deps') => (execute "join" work; join_deps deps'));
in
@@ -310,10 +306,16 @@
val _ = scheduler_check "join check";
val _ = Multithreading.self_critical () andalso
error "Cannot join future values within critical section";
- val _ =
- if is_some (thread_data ())
- then List.app join_loop xs (*proper task -- continue work*)
- else List.app join_wait xs; (*alien thread -- refrain from contending for resources*)
+
+ val worker = is_worker ();
+ fun join_wait x =
+ if SYNCHRONIZED "join_wait" (fn () =>
+ is_finished x orelse (if worker then worker_wait () else wait (); false))
+ then () else join_wait x;
+
+ val _ = if worker then join_deps (map task_of xs) else ();
+ val _ = List.app join_wait xs;
+
in map get_result xs end) ();
end;
@@ -347,7 +349,7 @@
fun interruptible_task f x =
if Multithreading.available then
Multithreading.with_attributes
- (if is_some (thread_data ())
+ (if is_worker ()
then Multithreading.restricted_interrupts
else Multithreading.regular_interrupts)
(fn _ => f) x
--- a/src/Pure/Concurrent/task_queue.ML Mon Jul 20 16:49:05 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Mon Jul 20 16:50:59 2009 +0200
@@ -24,6 +24,8 @@
val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> task * queue
val extend: task -> (bool -> bool) -> queue -> queue option
val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
+ val dequeue_towards: task list -> queue ->
+ (((task * group * (bool -> bool) list) * task list) option * queue)
val interrupt: queue -> task -> unit
val interrupt_external: queue -> string -> unit
val cancel: queue -> group -> bool
@@ -150,6 +152,28 @@
end;
+(* dequeue_towards -- adhoc dependencies *)
+
+fun dequeue_towards deps (queue as Queue {groups, jobs, ...}) =
+ let
+ fun ready task =
+ (case Task_Graph.get_node jobs task of
+ (group, Job list) =>
+ if null (Task_Graph.imm_preds jobs task) then SOME (task, group, rev list)
+ else NONE
+ | _ => NONE);
+ val tasks = filter (can (Task_Graph.get_node jobs)) deps;
+ in
+ (case get_first ready (Task_Graph.all_preds jobs tasks) of
+ NONE => (NONE, queue)
+ | SOME (result as (task, _, _)) =>
+ let
+ val jobs' = set_job task (Running (Thread.self ())) jobs;
+ val cache' = Unknown;
+ in (SOME (result, tasks), make_queue groups jobs' cache') end)
+ end;
+
+
(* sporadic interrupts *)
fun interrupt (Queue {jobs, ...}) task =
--- a/src/Pure/Isar/isar_cmd.ML Mon Jul 20 16:49:05 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Jul 20 16:50:59 2009 +0200
@@ -230,7 +230,7 @@
(* local endings *)
fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
-val local_terminal_proof = Toplevel.proof o Proof.local_terminal_proof;
+val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof;
val local_default_proof = Toplevel.proof Proof.local_default_proof;
val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
val local_done_proof = Toplevel.proof Proof.local_done_proof;
--- a/src/Pure/Isar/proof.ML Mon Jul 20 16:49:05 2009 +0200
+++ b/src/Pure/Isar/proof.ML Mon Jul 20 16:50:59 2009 +0200
@@ -1002,6 +1002,7 @@
val _ = assert_backward state;
val (goal_ctxt, (_, goal)) = find_goal state;
val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
+ val goal_txt = prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt);
val _ = is_relevant state andalso error "Cannot fork relevant proof";
@@ -1017,13 +1018,13 @@
val result_ctxt =
state
- |> map_contexts (Variable.declare_term prop)
+ |> map_contexts (fold Variable.declare_term goal_txt)
|> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))
|> fork_proof;
val future_thm = result_ctxt |> Future.map (fn (_, x) =>
ProofContext.get_fact_single (get_context x) (Facts.named this_name));
- val finished_goal = exception_trace (fn () => Goal.future_result goal_ctxt future_thm prop');
+ val finished_goal = Goal.future_result goal_ctxt future_thm prop';
val state' =
state
|> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
@@ -1043,9 +1044,9 @@
local
fun future_terminal_proof proof1 proof2 meths int state =
- if int orelse is_relevant state orelse not (Goal.future_enabled ())
+ if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
then proof1 meths state
- else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
+ else snd (proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))) state);
in
--- a/src/Pure/ProofGeneral/preferences.ML Mon Jul 20 16:49:05 2009 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Mon Jul 20 16:50:59 2009 +0200
@@ -84,6 +84,12 @@
fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
+val parallel_proof_pref =
+ let
+ fun get () = PgipTypes.bool_to_pgstring (! Goal.parallel_proofs >= 1);
+ fun set s = Goal.parallel_proofs := (if PgipTypes.read_pgipbool s then 1 else 0);
+ in mkpref get set PgipTypes.Pgipbool "parallel-proofs" "Check proofs in parallel" end;
+
val thm_depsN = "thm_deps";
val thm_deps_pref =
let
@@ -171,9 +177,7 @@
nat_pref Multithreading.max_threads
"max-threads"
"Maximum number of threads",
- bool_pref Goal.parallel_proofs
- "parallel-proofs"
- "Check proofs in parallel"];
+ parallel_proof_pref];
val pure_preferences =
[(category_display, display_preferences),
--- a/src/Pure/System/session.ML Mon Jul 20 16:49:05 2009 +0200
+++ b/src/Pure/System/session.ML Mon Jul 20 16:50:59 2009 +0200
@@ -11,7 +11,7 @@
val welcome: unit -> string
val use_dir: string -> string -> bool -> string list -> bool -> bool ->
string -> bool -> string list -> string -> string -> bool * string ->
- string -> int -> bool -> bool -> int -> int -> bool -> unit
+ string -> int -> bool -> bool -> int -> int -> int -> unit
val finish: unit -> unit
end;
--- a/src/Pure/Thy/thy_info.ML Mon Jul 20 16:49:05 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Jul 20 16:50:59 2009 +0200
@@ -350,7 +350,7 @@
val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
(case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
- val par_proofs = ! parallel_proofs;
+ val par_proofs = ! parallel_proofs >= 1;
fun fork (name, body) tab =
let
--- a/src/Pure/goal.ML Mon Jul 20 16:49:05 2009 +0200
+++ b/src/Pure/goal.ML Mon Jul 20 16:50:59 2009 +0200
@@ -6,7 +6,7 @@
signature BASIC_GOAL =
sig
- val parallel_proofs: bool ref
+ val parallel_proofs: int ref
val SELECT_GOAL: tactic -> int -> tactic
val CONJUNCTS: tactic -> int -> tactic
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -21,6 +21,7 @@
val finish: thm -> thm
val norm_result: thm -> thm
val future_enabled: unit -> bool
+ val local_future_enabled: unit -> bool
val future_result: Proof.context -> thm future -> term -> thm
val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
val prove_multi: Proof.context -> string list -> term list -> term list ->
@@ -95,10 +96,12 @@
(* future_enabled *)
-val parallel_proofs = ref true;
+val parallel_proofs = ref 1;
fun future_enabled () =
- Future.enabled () andalso ! parallel_proofs andalso is_some (Future.thread_data ());
+ Future.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
+
+fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
(* future_result *)
@@ -120,14 +123,15 @@
val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
val global_prop =
- Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)));
+ cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
+ |> Thm.weaken_sorts (Variable.sorts_of ctxt);
val global_result = result |> Future.map
(Thm.adjust_maxidx_thm ~1 #>
Drule.implies_intr_list assms #>
Drule.forall_intr_list fixes #>
Thm.generalize (map #1 tfrees, []) 0);
val local_result =
- Thm.future global_result (cert global_prop)
+ Thm.future global_result global_prop
|> Thm.instantiate (instT, [])
|> Drule.forall_elim_list fixes
|> fold (Thm.elim_implies o Thm.assume) assms;
--- a/src/Pure/proofterm.ML Mon Jul 20 16:49:05 2009 +0200
+++ b/src/Pure/proofterm.ML Mon Jul 20 16:50:59 2009 +0200
@@ -207,7 +207,8 @@
in ((oracle, true, failed), seen') end)
end);
in ((oracle orelse not (null oracles), unfinished, failed), seen) end;
- val (oracle, unfinished, failed) = #1 (fold status bodies ((false, false, false), Inttab.empty));
+ val (oracle, unfinished, failed) =
+ #1 (fold status bodies ((false, false, false), Inttab.empty));
in {oracle = oracle, unfinished = unfinished, failed = failed} end;
@@ -221,13 +222,14 @@
val all_oracles_of =
let
- fun collect (PBody {oracles, thms, ...}) = thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
- if Inttab.defined seen i then (x, seen)
- else
- let
- val body' = Future.join body;
- val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
- in (merge_oracles oracles x', seen') end);
+ fun collect (PBody {oracles, thms, ...}) =
+ thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
+ if Inttab.defined seen i then (x, seen)
+ else
+ let
+ val body' = Future.join body;
+ val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
+ in (merge_oracles oracles x', seen') end);
in fn body => #1 (collect body ([], Inttab.empty)) end;
fun approximate_proof_body prf =
@@ -292,7 +294,8 @@
| proof (OfClass (T, c)) = OfClass (typ T, c)
| proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
| proof (Promise (i, prop, Ts)) = Promise (i, prop, typs Ts)
- | proof (PThm (i, ((a, prop, SOME Ts), body))) = PThm (i, ((a, prop, SOME (typs Ts)), body))
+ | proof (PThm (i, ((a, prop, SOME Ts), body))) =
+ PThm (i, ((a, prop, SOME (typs Ts)), body))
| proof _ = raise Same.SAME;
in Same.commit proof end;
@@ -332,7 +335,8 @@
| change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
| change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
| change_type opTs (Promise _) = error "change_type: unexpected promise"
- | change_type opTs (PThm (i, ((name, prop, _), body))) = PThm (i, ((name, prop, opTs), body))
+ | change_type opTs (PThm (i, ((name, prop, _), body))) =
+ PThm (i, ((name, prop, opTs), body))
| change_type _ prf = prf;
@@ -513,7 +517,8 @@
| subst' _ _ = raise Same.SAME
and substh' lev t = (subst' lev t handle Same.SAME => t);
- fun subst lev (AbsP (a, t, body)) = (AbsP (a, Same.map_option (subst' lev) t, substh lev body)
+ fun subst lev (AbsP (a, t, body)) =
+ (AbsP (a, Same.map_option (subst' lev) t, substh lev body)
handle Same.SAME => AbsP (a, t, subst lev body))
| subst lev (Abst (a, T, body)) = Abst (a, T, subst (lev+1) body)
| subst lev (prf %% prf') = (subst lev prf %% substh lev prf'
--- a/src/Pure/pure_thy.ML Mon Jul 20 16:49:05 2009 +0200
+++ b/src/Pure/pure_thy.ML Mon Jul 20 16:50:59 2009 +0200
@@ -59,11 +59,11 @@
structure FactsData = TheoryDataFun
(
- type T = Facts.T * (unit lazy list * Task_Queue.group list);
- val empty = (Facts.empty, ([], []));
+ type T = Facts.T * (unit lazy list * Task_Queue.group Inttab.table);
+ val empty = (Facts.empty, ([], Inttab.empty));
val copy = I;
- fun extend (facts, _) = (facts, ([], []));
- fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
+ fun extend (facts, _) = (facts, ([], Inttab.empty));
+ fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], Inttab.empty));
);
@@ -84,7 +84,9 @@
fun join_proofs thy =
map_filter (Exn.get_exn o Lazy.force_result) (rev (#1 (#2 (FactsData.get thy))));
-fun cancel_proofs thy = List.app Future.cancel_group (#2 (#2 (FactsData.get thy)));
+fun cancel_proofs thy =
+ Inttab.fold (fn (_, group) => fn () => Future.cancel_group group)
+ (#2 (#2 (FactsData.get thy))) ();
@@ -144,9 +146,14 @@
(* enter_thms *)
+val pending_groups =
+ Thm.promises_of #> fold (fn (_, future) =>
+ if Future.is_finished future then I
+ else Inttab.update (`Task_Queue.group_id (Future.group_of future)));
+
fun enter_proofs (thy, thms) =
(FactsData.map (apsnd (fn (proofs, groups) =>
- (fold (cons o lazy_proof) thms proofs, fold Thm.pending_groups thms groups))) thy, thms);
+ (fold (cons o lazy_proof) thms proofs, fold pending_groups thms groups))) thy, thms);
fun enter_thms pre_name post_name app_att (b, thms) thy =
if Binding.is_empty b
--- a/src/Pure/thm.ML Mon Jul 20 16:49:05 2009 +0200
+++ b/src/Pure/thm.ML Mon Jul 20 16:50:59 2009 +0200
@@ -141,12 +141,12 @@
val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
val rename_boundvars: term -> term -> thm -> thm
- val future: thm future -> cterm -> thm
- val pending_groups: thm -> Task_Queue.group list -> Task_Queue.group list
- val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
val join_proof: thm -> unit
+ val promises_of: thm -> (serial * thm future) list
+ val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
+ val future: thm future -> cterm -> thm
val get_name: thm -> string
val put_name: string -> thm -> thm
val extern_oracles: theory -> xstring list
@@ -345,9 +345,7 @@
tpairs: (term * term) list, (*flex-flex pairs*)
prop: term} (*conclusion*)
and deriv = Deriv of
- {max_promise: serial,
- open_promises: (serial * thm future) OrdList.T,
- promises: (serial * thm future) OrdList.T,
+ {promises: (serial * thm future) OrdList.T,
body: Pt.proof_body};
type conv = cterm -> thm;
@@ -504,11 +502,10 @@
(** derivations **)
-fun make_deriv max_promise open_promises promises oracles thms proof =
- Deriv {max_promise = max_promise, open_promises = open_promises, promises = promises,
- body = PBody {oracles = oracles, thms = thms, proof = proof}};
+fun make_deriv promises oracles thms proof =
+ Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
-val empty_deriv = make_deriv ~1 [] [] [] [] Pt.MinProof;
+val empty_deriv = make_deriv [] [] [] Pt.MinProof;
(* inference rules *)
@@ -516,13 +513,9 @@
fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
fun deriv_rule2 f
- (Deriv {max_promise = max1, open_promises = open_ps1, promises = ps1,
- body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
- (Deriv {max_promise = max2, open_promises = open_ps2, promises = ps2,
- body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
+ (Deriv {promises = ps1, body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
+ (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
let
- val max = Int.max (max1, max2);
- val open_ps = OrdList.union promise_ord open_ps1 open_ps2;
val ps = OrdList.union promise_ord ps1 ps2;
val oras = Pt.merge_oracles oras1 oras2;
val thms = Pt.merge_thms thms1 thms2;
@@ -532,10 +525,10 @@
| 1 => MinProof
| 0 => MinProof
| i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
- in make_deriv max open_ps ps oras thms prf end;
+ in make_deriv ps oras thms prf end;
fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
-fun deriv_rule0 prf = deriv_rule1 I (make_deriv ~1 [] [] [] [] prf);
+fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
@@ -1614,6 +1607,36 @@
(*** Future theorems -- proofs with promises ***)
+(* fulfilled proofs *)
+
+fun raw_body (Thm (Deriv {body, ...}, _)) = body;
+
+fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
+ let val ps = map (apsnd (fulfill_body o Future.join)) promises
+ in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
+
+fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
+val proof_of = Pt.proof_of o proof_body_of;
+val join_proof = ignore o proof_body_of;
+
+
+(* derivation status *)
+
+fun promises_of (Thm (Deriv {promises, ...}, _)) = promises;
+
+fun status_of (Thm (Deriv {promises, body}, _)) =
+ let
+ val ps = map (Future.peek o snd) promises;
+ val bodies = body ::
+ map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
+ val {oracle, unfinished, failed} = Pt.status_of bodies;
+ in
+ {oracle = oracle,
+ unfinished = unfinished orelse exists is_none ps,
+ failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
+ end;
+
+
(* future rule *)
fun future_result i orig_thy orig_shyps orig_prop raw_thm =
@@ -1623,12 +1646,13 @@
val _ = Theory.check_thy orig_thy;
fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
- val Thm (Deriv {max_promise, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
+ val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
val _ = prop aconv orig_prop orelse err "bad prop";
val _ = null tpairs orelse err "bad tpairs";
val _ = null hyps orelse err "bad hyps";
val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
- val _ = max_promise < i orelse err "bad dependencies";
+ val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
+ val _ = List.app (ignore o fulfill_body o Future.join o #2) promises;
in thm end;
fun future future_thm ct =
@@ -1639,9 +1663,8 @@
val i = serial ();
val future = future_thm |> Future.map (future_result i thy sorts prop);
- val promise = (i, future);
in
- Thm (make_deriv i [promise] [promise] [] [] (Pt.promise_proof thy i prop),
+ Thm (make_deriv [(i, future)] [] [] (Pt.promise_proof thy i prop),
{thy_ref = thy_ref,
tags = [],
maxidx = maxidx,
@@ -1652,57 +1675,21 @@
end;
-(* derivation status *)
-
-fun raw_proof_body_of (Thm (Deriv {body, ...}, _)) = body;
-val raw_proof_of = Proofterm.proof_of o raw_proof_body_of;
-
-fun pending_groups (Thm (Deriv {open_promises, ...}, _)) =
- fold (insert Task_Queue.eq_group o Future.group_of o #2) open_promises;
-
-fun status_of (Thm (Deriv {promises, body, ...}, _)) =
- let
- val ps = map (Future.peek o snd) promises;
- val bodies = body ::
- map_filter (fn SOME (Exn.Result th) => SOME (raw_proof_body_of th) | _ => NONE) ps;
- val {oracle, unfinished, failed} = Pt.status_of bodies;
- in
- {oracle = oracle,
- unfinished = unfinished orelse exists is_none ps,
- failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
- end;
-
-
-(* fulfilled proofs *)
-
-fun proof_body_of (Thm (Deriv {open_promises, promises, body, ...}, {thy_ref, ...})) =
- let
- val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));
- val ps = map (apsnd (raw_proof_body_of o Future.join)) promises;
- in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
-
-val proof_of = Proofterm.proof_of o proof_body_of;
-val join_proof = ignore o proof_body_of;
-
-
(* closed derivations with official name *)
fun get_name thm =
- Pt.get_name (hyps_of thm) (prop_of thm) (raw_proof_of thm);
+ Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
fun put_name name (thm as Thm (der, args)) =
let
- val Deriv {max_promise, open_promises, promises, body, ...} = der;
+ val Deriv {promises, body} = der;
val {thy_ref, hyps, prop, tpairs, ...} = args;
val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
val ps = map (apsnd (Future.map proof_body_of)) promises;
val thy = Theory.deref thy_ref;
val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
-
- val open_promises' = open_promises |> filter (fn (_, p) =>
- (case Future.peek p of SOME (Exn.Result _) => false | _ => true));
- val der' = make_deriv max_promise open_promises' [] [] [pthm] proof;
+ val der' = make_deriv [] [] [pthm] proof;
val _ = Theory.check_thy thy;
in Thm (der', args) end;
@@ -1718,7 +1705,7 @@
raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
else
let val (ora, prf) = Pt.oracle_proof name prop in
- Thm (make_deriv ~1 [] [] [ora] [] prf,
+ Thm (make_deriv [] [ora] [] prf,
{thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
tags = [],
maxidx = maxidx,