# HG changeset patch # User haftmann # Date 1248101459 -7200 # Node ID 35084ad81bd42e370967bafc6d4ada26e5f09968 # Parent bafffa63ebfd5bdb8a4903fe421767891739ea97# Parent 1fb676ab8d9937a6bde7dcd73529eebf69a66f54 merged diff -r bafffa63ebfd -r 35084ad81bd4 NEWS --- 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) diff -r bafffa63ebfd -r 35084ad81bd4 doc-src/System/Thy/Presentation.thy --- 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 diff -r bafffa63ebfd -r 35084ad81bd4 doc-src/System/Thy/document/Presentation.tex --- 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 diff -r bafffa63ebfd -r 35084ad81bd4 etc/settings --- 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="" diff -r bafffa63ebfd -r 35084ad81bd4 lib/Tools/usedir --- 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 ;; diff -r bafffa63ebfd -r 35084ad81bd4 src/HOL/Set.thy --- 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 \") and not_mem ("(_/ \ _)" [50, 51] 50) +text {* Set comprehensions *} + syntax "@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})") translations "{x. P}" == "Collect (%x. P)" -definition Int :: "'a set \ 'a set \ 'a set" (infixl "Int" 70) where - "A Int B \ {x. x \ A \ x \ B}" - -definition Un :: "'a set \ 'a set \ 'a set" (infixl "Un" 65) where - "A Un B \ {x. x \ A \ x \ B}" - -notation (xsymbols) - "Int" (infixl "\" 70) and - "Un" (infixl "\" 65) - -notation (HTML output) - "Int" (infixl "\" 70) and - "Un" (infixl "\" 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{_ \/ _./ _})") + +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 \ {x. False}" definition insert :: "'a \ 'a set \ 'a set" where - "insert a B \ {x. x = a} \ B" - -definition UNIV :: "'a set" where - "UNIV \ {x. True}" + insert_compr: "insert a B = {x. x = a \ x \ 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 \ 'a set \ bool" where + "subset \ less" + +abbreviation + subset_eq :: "'a set \ 'a set \ bool" where + "subset_eq \ 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 \") and + subset ("(_/ \ _)" [50, 51] 50) and + subset_eq ("op \") and + subset_eq ("(_/ \ _)" [50, 51] 50) + +notation (HTML output) + subset ("op \") and + subset ("(_/ \ _)" [50, 51] 50) and + subset_eq ("op \") and + subset_eq ("(_/ \ _)" [50, 51] 50) + +abbreviation (input) + supset :: "'a set \ 'a set \ bool" where + "supset \ greater" + +abbreviation (input) + supset_eq :: "'a set \ 'a set \ bool" where + "supset_eq \ greater_eq" + +notation (xsymbols) + supset ("op \") and + supset ("(_/ \ _)" [50, 51] 50) and + supset_eq ("op \") and + supset_eq ("(_/ \ _)" [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{_ \/ _./ _})") - -translations - "{x:A. P}" => "{x. x:A & P}" - -abbreviation - subset :: "'a set \ 'a set \ bool" where - "subset \ less" - -abbreviation - subset_eq :: "'a set \ 'a set \ bool" where - "subset_eq \ 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 \") and - subset ("(_/ \ _)" [50, 51] 50) and - subset_eq ("op \") and - subset_eq ("(_/ \ _)" [50, 51] 50) - -notation (HTML output) - subset ("op \") and - subset ("(_/ \ _)" [50, 51] 50) and - subset_eq ("op \") and - subset_eq ("(_/ \ _)" [50, 51] 50) - -abbreviation (input) - supset :: "'a set \ 'a set \ bool" where - "supset \ greater" - -abbreviation (input) - supset_eq :: "'a set \ 'a set \ bool" where - "supset_eq \ greater_eq" - -notation (xsymbols) - supset ("op \") and - supset ("(_/ \ _)" [50, 51] 50) and - supset_eq ("op \") and - supset_eq ("(_/ \ _)" [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 \ B" @@ -499,10 +473,19 @@ by blast lemma subset_refl [simp,atp]: "A \ A" - by fast + by (fact order_refl) lemma subset_trans: "A \ B ==> B \ C ==> A \ C" - by blast + by (fact order_trans) + +lemma set_rev_mp: "x:A ==> A \ B ==> x:B" + by (rule subsetD) + +lemma set_mp: "A \ 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 \ {x. True}" + lemma UNIV_I [simp]: "x : UNIV" by (simp add: UNIV_def) @@ -565,6 +551,9 @@ lemma subset_UNIV [simp]: "A \ 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 \ A ==> False) ==> A = {}" by blast lemma equals0D: "A = {} ==> a \ 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 \ 'a set \ 'a set" (infixl "Un" 65) where + "A Un B \ {x. x \ A \ x \ B}" + +notation (xsymbols) + "Un" (infixl "\" 65) + +notation (HTML output) + "Un" (infixl "\" 65) + +lemma sup_set_eq: "sup A B = A \ 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 \ {x. x = a} \ B" + by (simp add: Collect_def mem_def insert_compr Un_def) + +lemma mono_Un: "mono f \ f A \ f B \ f (A \ B)" + apply (fold sup_set_eq) + apply (erule mono_sup) + done + subsubsection {* Binary intersection -- Int *} +definition Int :: "'a set \ 'a set \ 'a set" (infixl "Int" 70) where + "A Int B \ {x. x \ A \ x \ B}" + +notation (xsymbols) + "Int" (infixl "\" 70) + +notation (HTML output) + "Int" (infixl "\" 70) + +lemma inf_set_eq: "inf A B = A \ 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 \ f (A \ B) \ f A \ 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. \ & x=t & \}"}. *} + +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. \ & x=t & \}"} +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 "_ \ _"} as complete lattice *} instantiation bool :: complete_lattice begin @@ -1013,9 +1112,6 @@ "\ \{}" 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 \ ('a \ 'b set) \ 'b set" where - "INTER A B \ {y. \x\A. y \ B x}" +subsubsection {* Unions of families *} definition UNION :: "'a set \ ('a \ 'b set) \ 'b set" where "UNION A B \ {y. \x\A. y \ B x}" -definition Inter :: "'a set set \ 'a set" where - "Inter S \ INTER S (\x. x)" - -definition Union :: "'a set set \ 'a set" where - "Union S \ UNION S (\x. x)" - -notation (xsymbols) - Inter ("\_" [90] 90) and - 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\_./ _)" [0, 10] 10) "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" [0, 10] 10) - "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 10] 10) "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 10] 10) syntax (latex output) - "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) - "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^esub>)/ _)" [0, 10] 10) "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^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]: - "\(B`A) = (\x\A. B x)" - by (auto simp add: Inter_def INTER_def image_def) - -lemma Union_image_eq [simp]: - "\(B`A) = (\x\A. B x)" - by (auto simp add: Union_def UNION_def image_def) - -lemma inf_set_eq: "A \ B = A \ B" - by (simp add: inf_fun_eq inf_bool_eq Int_def Collect_def mem_def) - -lemma sup_set_eq: "A \ B = A \ B" - by (simp add: sup_fun_eq sup_bool_eq Un_def Collect_def mem_def) - -lemma mono_Int: "mono f \ f (A \ B) \ f A \ f B" - apply (fold inf_set_eq sup_set_eq) - apply (erule mono_inf) - done - -lemma mono_Un: "mono f \ f A \ f B \ f (A \ 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: - "\A = {x. \B \ A. x \ B}" - by (simp add: Inter_def INTER_def) - -lemma Union_eq: - "\A = {x. \B \ A. x \ B}" - by (simp add: Union_def UNION_def) - -lemma Inf_set_eq: - "\S = \S" -proof (rule set_ext) - fix x - have "(\Q\{P. \A\S. P \ x \ A}. Q) \ (\A\S. x \ A)" - by auto - then show "x \ \S \ x \ \S" - by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def) -qed - -lemma Sup_set_eq: - "\S = \S" -proof (rule set_ext) - fix x - have "(\Q\{P. \A\S. P \ x \ A}. Q) \ (\A\S. x \ A)" - by auto - then show "x \ \S \ x \ \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) = (\x\S. f x)" - by (simp add: INFI_def Inf_set_eq) - -lemma SUPR_set_eq: - "(SUP x:S. f x) = (\x\S. f x)" - by (simp add: SUPR_def Sup_set_eq) - -no_notation - less_eq (infix "\" 50) and - less (infix "\" 50) and - inf (infixl "\" 70) and - sup (infixl "\" 65) and - Inf ("\_" [900] 900) and - Sup ("\_" [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 \ ('a \ 'b set) \ 'b set" where + "INTER A B \ {y. \x\A. y \ 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\_./ _)" [0, 10] 10) + "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 10] 10) + +syntax (latex output) + "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) + "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^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 \ 'a set" where + "Union S \ UNION S (\x. x)" + +notation (xsymbols) + Union ("\_" [90] 90) + +lemma Union_image_eq [simp]: + "\(B`A) = (\x\A. B x)" + by (auto simp add: Union_def UNION_def image_def) + +lemma Union_eq: + "\A = {x. \B \ A. x \ B}" + by (simp add: Union_def UNION_def) + +lemma Sup_set_eq: + "\S = \S" +proof (rule set_ext) + fix x + have "(\Q\{P. \A\S. P \ x \ A}. Q) \ (\A\S. x \ A)" + by auto + then show "x \ \S \ x \ \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) = (\x\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 \ 'a set" where + "Inter S \ INTER S (\x. x)" + +notation (xsymbols) + Inter ("\_" [90] 90) + +lemma Inter_image_eq [simp]: + "\(B`A) = (\x\A. B x)" + by (auto simp add: Inter_def INTER_def image_def) + +lemma Inter_eq: + "\A = {x. \B \ A. x \ B}" + by (simp add: Inter_def INTER_def) + +lemma Inf_set_eq: + "\S = \S" +proof (rule set_ext) + fix x + have "(\Q\{P. \A\S. P \ x \ A}. Q) \ (\A\S. x \ A)" + by auto + then show "x \ \S \ x \ \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) = (\x\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. \ & x=t & \}"}. *} - -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. \ & x=t & \}"} -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 "\" 50) and + less (infix "\" 50) and + inf (infixl "\" 70) and + sup (infixl "\" 65) and + Inf ("\_" [900] 900) and + Sup ("\_" [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 \ '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 \ B ==> x:B" - by (rule subsetD) - -lemma set_mp: "A \ 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 \ 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 = diff -r bafffa63ebfd -r 35084ad81bd4 src/HOL/Tools/Function/fundef_core.ML --- 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 diff -r bafffa63ebfd -r 35084ad81bd4 src/Pure/Concurrent/future.ML --- 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 diff -r bafffa63ebfd -r 35084ad81bd4 src/Pure/Concurrent/task_queue.ML --- 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 = diff -r bafffa63ebfd -r 35084ad81bd4 src/Pure/Isar/isar_cmd.ML --- 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; diff -r bafffa63ebfd -r 35084ad81bd4 src/Pure/Isar/proof.ML --- 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 diff -r bafffa63ebfd -r 35084ad81bd4 src/Pure/Isar/toplevel.ML diff -r bafffa63ebfd -r 35084ad81bd4 src/Pure/ProofGeneral/preferences.ML --- 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), diff -r bafffa63ebfd -r 35084ad81bd4 src/Pure/System/session.ML --- 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; diff -r bafffa63ebfd -r 35084ad81bd4 src/Pure/Thy/thy_info.ML --- 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 diff -r bafffa63ebfd -r 35084ad81bd4 src/Pure/goal.ML --- 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; diff -r bafffa63ebfd -r 35084ad81bd4 src/Pure/proofterm.ML --- 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' diff -r bafffa63ebfd -r 35084ad81bd4 src/Pure/pure_thy.ML --- 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 diff -r bafffa63ebfd -r 35084ad81bd4 src/Pure/thm.ML --- 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,