--- a/Admin/isatest/isatest-statistics Sun Jan 11 14:18:17 2009 +0100
+++ b/Admin/isatest/isatest-statistics Sun Jan 11 14:18:32 2009 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
# DESCRIPTION: Produce statistics from isatest session logs.
@@ -93,7 +92,7 @@
for SESSION in $SESSIONS
do
- fgrep "$SESSION " "$ALL_DATA" > "$SESSION_DATA"
+ grep "^${SESSION} " "$ALL_DATA" > "$SESSION_DATA"
PLOT="plot [] [0:] \"$SESSION_DATA\" using 2:3 smooth sbezier title \"interpolated cpu time\", \"$SESSION_DATA\" using 2:3 smooth csplines title \"cpu time\""
if [ "$PARALLEL" = true ]; then
PLOT="${PLOT}, \"$SESSION_DATA\" using 2:4 smooth sbezier title \"interpolated elapsed time\", \"$SESSION_DATA\" using 2:4 smooth csplines title \"elapsed time\""
--- a/Admin/isatest/settings/at-mac-poly-5.1-para Sun Jan 11 14:18:17 2009 +0100
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Sun Jan 11 14:18:32 2009 +0100
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-5.2.1"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="--mutable 500 --immutable 1500"
+ ML_OPTIONS="--mutable 200 --immutable 1200"
ISABELLE_HOME_USER=~/isabelle-at-mac-poly-e
--- a/doc-src/System/Thy/Presentation.thy Sun Jan 11 14:18:17 2009 +0100
+++ b/doc-src/System/Thy/Presentation.thy Sun Jan 11 14:18:32 2009 +0100
@@ -442,6 +442,7 @@
-D PATH dump generated document sources into PATH
-M MAX multithreading: maximum number of worker threads (default 1)
-P PATH set path for remote theory browsing information
+ -Q BOOL check proofs in parallel (default true)
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
@@ -461,6 +462,11 @@
ISABELLE_USEDIR_OPTIONS=
HOL_USEDIR_OPTIONS=
+
+ ML_PLATFORM=x86-linux
+ ML_HOME=/usr/local/polyml-5.2.1/x86-linux
+ ML_SYSTEM=polyml-5.2.1
+ ML_OPTIONS=-H 500
\end{ttbox}
Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
@@ -574,6 +580,13 @@
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 Sun Jan 11 14:18:17 2009 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex Sun Jan 11 14:18:32 2009 +0100
@@ -468,6 +468,7 @@
-D PATH dump generated document sources into PATH
-M MAX multithreading: maximum number of worker threads (default 1)
-P PATH set path for remote theory browsing information
+ -Q BOOL check proofs in parallel (default true)
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
@@ -487,6 +488,11 @@
ISABELLE_USEDIR_OPTIONS=
HOL_USEDIR_OPTIONS=
+
+ ML_PLATFORM=x86-linux
+ ML_HOME=/usr/local/polyml-5.2.1/x86-linux
+ ML_SYSTEM=polyml-5.2.1
+ ML_OPTIONS=-H 500
\end{ttbox}
Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}}
@@ -590,6 +596,13 @@
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/lib/Tools/usedir Sun Jan 11 14:18:17 2009 +0100
+++ b/lib/Tools/usedir Sun Jan 11 14:18:32 2009 +0100
@@ -19,6 +19,7 @@
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)"
@@ -72,6 +73,7 @@
DUMP=""
MAXTHREADS="1"
RPATH=""
+PARALLEL_PROOFS="true"
TRACETHREADS="0"
DOCUMENT_VERSIONS=""
BUILD=""
@@ -89,7 +91,7 @@
function getoptions()
{
OPTIND=1
- while getopts "C:D:M:P:T:V:bc:d:f:g:i:m:p:rs:v:" OPT
+ while getopts "C:D:M:P:Q:T:V:bc:d:f:g:i:m:p:rs:v:" OPT
do
case "$OPT" in
C)
@@ -101,15 +103,18 @@
;;
M)
if [ "$OPTARG" = max ]; then
- MAXTHREADS=0
- else
+ MAXTHREADS=0
+ else
check_number "$OPTARG"
MAXTHREADS="$OPTARG"
- fi
+ fi
;;
P)
RPATH="$OPTARG"
;;
+ Q)
+ PARALLEL_PROOFS="$OPTARG"
+ ;;
T)
check_number "$OPTARG"
TRACETHREADS="$OPTARG"
@@ -232,7 +237,7 @@
[ "$COMPRESS" = true ] && OPT_C="-c"
"$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS;" \
+ -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
$OPT_C -q -w $LOGIC $NAME > "$LOG"
RC="$?"
else
@@ -241,7 +246,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS; quit();" \
+ -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
-r -q "$LOGIC" > "$LOG"
RC="$?"
cd ..
--- a/src/HOL/Algebra/IntRing.thy Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/Algebra/IntRing.thy Sun Jan 11 14:18:32 2009 +0100
@@ -348,8 +348,8 @@
"(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)"
apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
apply (rule, clarify)
-apply (simp add: dvd_def, clarify)
-apply (simp add: int.m_comm)
+apply (simp add: dvd_def)
+apply (simp add: dvd_def mult_ac)
done
lemma dvds_eq_Idl:
--- a/src/HOL/Divides.thy Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/Divides.thy Sun Jan 11 14:18:32 2009 +0100
@@ -33,6 +33,10 @@
unfolding mult_commute [of b]
by (rule mod_div_equality)
+lemma mod_div_equality': "a mod b + a div b * b = a"
+ using mod_div_equality [of a b]
+ by (simp only: add_ac)
+
lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
by (simp add: mod_div_equality)
@@ -143,6 +147,173 @@
then show "b mod a = 0" by simp
qed
+lemma mod_div_trivial [simp]: "a mod b div b = 0"
+proof (cases "b = 0")
+ assume "b = 0"
+ thus ?thesis by simp
+next
+ assume "b \<noteq> 0"
+ hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
+ by (rule div_mult_self1 [symmetric])
+ also have "\<dots> = a div b"
+ by (simp only: mod_div_equality')
+ also have "\<dots> = a div b + 0"
+ by simp
+ finally show ?thesis
+ by (rule add_left_imp_eq)
+qed
+
+lemma mod_mod_trivial [simp]: "a mod b mod b = a mod b"
+proof -
+ have "a mod b mod b = (a mod b + a div b * b) mod b"
+ by (simp only: mod_mult_self1)
+ also have "\<dots> = a mod b"
+ by (simp only: mod_div_equality')
+ finally show ?thesis .
+qed
+
+text {* Addition respects modular equivalence. *}
+
+lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
+proof -
+ have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
+ by (simp only: mod_div_equality)
+ also have "\<dots> = (a mod c + b + a div c * c) mod c"
+ by (simp only: add_ac)
+ also have "\<dots> = (a mod c + b) mod c"
+ by (rule mod_mult_self1)
+ finally show ?thesis .
+qed
+
+lemma mod_add_right_eq: "(a + b) mod c = (a + b mod c) mod c"
+proof -
+ have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
+ by (simp only: mod_div_equality)
+ also have "\<dots> = (a + b mod c + b div c * c) mod c"
+ by (simp only: add_ac)
+ also have "\<dots> = (a + b mod c) mod c"
+ by (rule mod_mult_self1)
+ finally show ?thesis .
+qed
+
+lemma mod_add_eq: "(a + b) mod c = (a mod c + b mod c) mod c"
+by (rule trans [OF mod_add_left_eq mod_add_right_eq])
+
+lemma mod_add_cong:
+ assumes "a mod c = a' mod c"
+ assumes "b mod c = b' mod c"
+ shows "(a + b) mod c = (a' + b') mod c"
+proof -
+ have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
+ unfolding assms ..
+ thus ?thesis
+ by (simp only: mod_add_eq [symmetric])
+qed
+
+text {* Multiplication respects modular equivalence. *}
+
+lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
+proof -
+ have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
+ by (simp only: mod_div_equality)
+ also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
+ by (simp only: left_distrib right_distrib add_ac mult_ac)
+ also have "\<dots> = (a mod c * b) mod c"
+ by (rule mod_mult_self1)
+ finally show ?thesis .
+qed
+
+lemma mod_mult_right_eq: "(a * b) mod c = (a * (b mod c)) mod c"
+proof -
+ have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
+ by (simp only: mod_div_equality)
+ also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
+ by (simp only: left_distrib right_distrib add_ac mult_ac)
+ also have "\<dots> = (a * (b mod c)) mod c"
+ by (rule mod_mult_self1)
+ finally show ?thesis .
+qed
+
+lemma mod_mult_eq: "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
+by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
+
+lemma mod_mult_cong:
+ assumes "a mod c = a' mod c"
+ assumes "b mod c = b' mod c"
+ shows "(a * b) mod c = (a' * b') mod c"
+proof -
+ have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
+ unfolding assms ..
+ thus ?thesis
+ by (simp only: mod_mult_eq [symmetric])
+qed
+
+lemma mod_mod_cancel:
+ assumes "c dvd b"
+ shows "a mod b mod c = a mod c"
+proof -
+ from `c dvd b` obtain k where "b = c * k"
+ by (rule dvdE)
+ have "a mod b mod c = a mod (c * k) mod c"
+ by (simp only: `b = c * k`)
+ also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
+ by (simp only: mod_mult_self1)
+ also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
+ by (simp only: add_ac mult_ac)
+ also have "\<dots> = a mod c"
+ by (simp only: mod_div_equality)
+ finally show ?thesis .
+qed
+
+end
+
+class ring_div = semiring_div + comm_ring_1
+begin
+
+text {* Negation respects modular equivalence. *}
+
+lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
+proof -
+ have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
+ by (simp only: mod_div_equality)
+ also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
+ by (simp only: minus_add_distrib minus_mult_left add_ac)
+ also have "\<dots> = (- (a mod b)) mod b"
+ by (rule mod_mult_self1)
+ finally show ?thesis .
+qed
+
+lemma mod_minus_cong:
+ assumes "a mod b = a' mod b"
+ shows "(- a) mod b = (- a') mod b"
+proof -
+ have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
+ unfolding assms ..
+ thus ?thesis
+ by (simp only: mod_minus_eq [symmetric])
+qed
+
+text {* Subtraction respects modular equivalence. *}
+
+lemma mod_diff_left_eq: "(a - b) mod c = (a mod c - b) mod c"
+ unfolding diff_minus
+ by (intro mod_add_cong mod_minus_cong) simp_all
+
+lemma mod_diff_right_eq: "(a - b) mod c = (a - b mod c) mod c"
+ unfolding diff_minus
+ by (intro mod_add_cong mod_minus_cong) simp_all
+
+lemma mod_diff_eq: "(a - b) mod c = (a mod c - b mod c) mod c"
+ unfolding diff_minus
+ by (intro mod_add_cong mod_minus_cong) simp_all
+
+lemma mod_diff_cong:
+ assumes "a mod c = a' mod c"
+ assumes "b mod c = b' mod c"
+ shows "(a - b) mod c = (a' - b') mod c"
+ unfolding diff_minus using assms
+ by (intro mod_add_cong mod_minus_cong)
+
end
@@ -467,22 +638,14 @@
done
lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
-apply (cases "c = 0", simp)
-apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN mod_eq])
-done
+ by (rule mod_mult_right_eq)
lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
- apply (rule trans)
- apply (rule_tac s = "b*a mod c" in trans)
- apply (rule_tac [2] mod_mult1_eq)
- apply (simp_all add: mult_commute)
- done
+ by (rule mod_mult_left_eq)
lemma mod_mult_distrib_mod:
"(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
-apply (rule mod_mult1_eq' [THEN trans])
-apply (rule mod_mult1_eq)
-done
+ by (rule mod_mult_eq)
lemma divmod_rel_add1_eq:
"[| divmod_rel a c aq ar; divmod_rel b c bq br; c > 0 |]
@@ -497,9 +660,7 @@
done
lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
-apply (cases "c = 0", simp)
-apply (blast intro: divmod_rel_add1_eq [THEN mod_eq] divmod_rel)
-done
+ by (rule mod_add_eq)
lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
apply (cut_tac m = q and n = c in mod_less_divisor)
@@ -618,11 +779,11 @@
apply (auto simp add: Suc_diff_le le_mod_geq)
done
-lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
- by (cases "n = 0") auto
+lemma nat_mod_div_trivial: "m mod n div n = (0 :: nat)"
+ by simp
-lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"
- by (cases "n = 0") auto
+lemma nat_mod_mod_trivial: "m mod n mod n = (m mod n :: nat)"
+ by simp
subsubsection {* The Divides Relation *}
@@ -718,18 +879,6 @@
apply (simp add: power_add)
done
-lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c"
- apply (rule trans [symmetric])
- apply (rule mod_add1_eq, simp)
- apply (rule mod_add1_eq [symmetric])
- done
-
-lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c"
- apply (rule trans [symmetric])
- apply (rule mod_add1_eq, simp)
- apply (rule mod_add1_eq [symmetric])
- done
-
lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
by (induct n) auto
--- a/src/HOL/IntDiv.thy Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/IntDiv.thy Sun Jan 11 14:18:32 2009 +0100
@@ -747,12 +747,12 @@
lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
by (simp add: zdiv_zmult1_eq)
-lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
+lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
apply (case_tac "b = 0", simp)
apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
done
-lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
+lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)"
apply (case_tac "b = 0", simp)
apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
done
@@ -776,72 +776,50 @@
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
done
-lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
-by (simp add: zdiv_zadd1_eq)
-
-lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
-by (simp add: zdiv_zadd1_eq)
-
-instance int :: semiring_div
+instance int :: ring_div
proof
fix a b c :: int
assume not0: "b \<noteq> 0"
show "(a + c * b) div b = c + a div b"
unfolding zdiv_zadd1_eq [of a "c * b"] using not0
- by (simp add: zmod_zmult1_eq)
+ by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
qed auto
-lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
-by (subst mult_commute, erule zdiv_zmult_self1)
+lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
+by (rule div_add_self1) (* already declared [simp] *)
+
+lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
+by (rule div_add_self2) (* already declared [simp] *)
-lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)"
-by (simp add: zmod_zmult1_eq)
+lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a"
+by (rule div_mult_self1_is_id) (* already declared [simp] *)
-lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)"
-by (simp add: mult_commute zmod_zmult1_eq)
+lemma zmod_zmult_self1: "(a*b) mod b = (0::int)"
+by (rule mod_mult_self2_is_0) (* already declared [simp] *)
+
+lemma zmod_zmult_self2: "(b*a) mod b = (0::int)"
+by (rule mod_mult_self1_is_0) (* already declared [simp] *)
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
-proof
- assume "m mod d = 0"
- with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto
-next
- assume "EX q::int. m = d*q"
- thus "m mod d = 0" by auto
-qed
+by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
+(* REVISIT: should this be generalized to all semiring_div types? *)
lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
-apply (rule trans [symmetric])
-apply (rule zmod_zadd1_eq, simp)
-apply (rule zmod_zadd1_eq [symmetric])
-done
+by (rule mod_add_left_eq)
lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"
-apply (rule trans [symmetric])
-apply (rule zmod_zadd1_eq, simp)
-apply (rule zmod_zadd1_eq [symmetric])
-done
+by (rule mod_add_right_eq)
-lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
-apply (case_tac "a = 0", simp)
-apply (simp add: zmod_zadd1_eq)
-done
+lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)"
+by (rule mod_add_self1) (* already declared [simp] *)
-lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)"
-apply (case_tac "a = 0", simp)
-apply (simp add: zmod_zadd1_eq)
-done
-
+lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
+by (rule mod_add_self2) (* already declared [simp] *)
-lemma zmod_zdiff1_eq: fixes a::int
- shows "(a - b) mod c = (a mod c - b mod c) mod c" (is "?l = ?r")
-proof -
- have "?l = (c + (a mod c - b mod c)) mod c"
- using zmod_zadd1_eq[of a "-b" c] by(simp add:ring_simps zmod_zminus1_eq_if)
- also have "\<dots> = ?r" by simp
- finally show ?thesis .
-qed
+lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)"
+by (rule mod_diff_eq)
subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *}
@@ -954,18 +932,8 @@
apply (auto simp add: mult_commute)
done
-lemma zmod_zmod_cancel:
-assumes "n dvd m" shows "(k::int) mod m mod n = k mod n"
-proof -
- from `n dvd m` obtain r where "m = n*r" by(auto simp:dvd_def)
- have "k mod n = (m * (k div m) + k mod m) mod n"
- using zmod_zdiv_equality[of k m] by simp
- also have "\<dots> = (m * (k div m) mod n + k mod m mod n) mod n"
- by(subst zmod_zadd1_eq, rule refl)
- also have "m * (k div m) mod n = 0" using `m = n*r`
- by(simp add:mult_ac)
- finally show ?thesis by simp
-qed
+lemma zmod_zmod_cancel: "n dvd m \<Longrightarrow> (k::int) mod m mod n = k mod n"
+by (rule mod_mod_cancel)
subsection {*Splitting Rules for div and mod*}
@@ -1169,50 +1137,31 @@
subsection {* The Divides Relation *}
lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
- by (simp add: dvd_def zmod_eq_0_iff)
+ by (rule dvd_eq_mod_eq_0)
lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
-lemma zdvd_0_right [iff]: "(m::int) dvd 0"
- by (simp add: dvd_def)
+lemma zdvd_0_right: "(m::int) dvd 0"
+ by (rule dvd_0_right) (* already declared [iff] *)
-lemma zdvd_0_left [iff,noatp]: "(0 dvd (m::int)) = (m = 0)"
- by (simp add: dvd_def)
+lemma zdvd_0_left: "(0 dvd (m::int)) = (m = 0)"
+ by (rule dvd_0_left_iff) (* already declared [noatp,simp] *)
-lemma zdvd_1_left [iff]: "1 dvd (m::int)"
- by (simp add: dvd_def)
+lemma zdvd_1_left: "1 dvd (m::int)"
+ by (rule one_dvd) (* already declared [simp] *)
lemma zdvd_refl [simp]: "m dvd (m::int)"
- by (auto simp add: dvd_def intro: zmult_1_right [symmetric])
+ by (rule dvd_refl) (* TODO: declare generic dvd_refl [simp] *)
lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
- by (auto simp add: dvd_def intro: mult_assoc)
+ by (rule dvd_trans)
lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
-proof
- assume "m dvd - n"
- then obtain k where "- n = m * k" ..
- then have "n = m * - k" by simp
- then show "m dvd n" ..
-next
- assume "m dvd n"
- then have "m dvd n * -1" by (rule dvd_mult2)
- then show "m dvd - n" by simp
-qed
+ by (rule dvd_minus_iff)
lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
-proof
- assume "- m dvd n"
- then obtain k where "n = - m * k" ..
- then have "n = m * - k" by simp
- then show "m dvd n" ..
-next
- assume "m dvd n"
- then obtain k where "n = m * k" ..
- then have "n = - m * - k" by simp
- then show "- m dvd n" ..
-qed
+ by (rule minus_dvd_iff)
lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
@@ -1227,9 +1176,7 @@
done
lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
- apply (simp add: dvd_def)
- apply (blast intro: right_distrib [symmetric])
- done
+ by (rule dvd_add)
lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a"
shows "\<bar>a\<bar> = \<bar>b\<bar>"
@@ -1244,9 +1191,7 @@
qed
lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
- apply (simp add: dvd_def)
- apply (blast intro: right_diff_distrib [symmetric])
- done
+ by (rule Ring_and_Field.dvd_diff)
lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
apply (subgoal_tac "m = n + (m - n)")
@@ -1255,34 +1200,22 @@
done
lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
- apply (simp add: dvd_def)
- apply (blast intro: mult_left_commute)
- done
+ by (rule dvd_mult)
lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
- apply (subst mult_commute)
- apply (erule zdvd_zmult)
- done
+ by (rule dvd_mult2)
-lemma zdvd_triv_right [iff]: "(k::int) dvd m * k"
- apply (rule zdvd_zmult)
- apply (rule zdvd_refl)
- done
+lemma zdvd_triv_right: "(k::int) dvd m * k"
+ by (rule dvd_triv_right) (* already declared [simp] *)
-lemma zdvd_triv_left [iff]: "(k::int) dvd k * m"
- apply (rule zdvd_zmult2)
- apply (rule zdvd_refl)
- done
+lemma zdvd_triv_left: "(k::int) dvd k * m"
+ by (rule dvd_triv_left) (* already declared [simp] *)
lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
- apply (simp add: dvd_def)
- apply (simp add: mult_assoc, blast)
- done
+ by (rule dvd_mult_left)
lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
- apply (rule zdvd_zmultD2)
- apply (subst mult_commute, assumption)
- done
+ by (rule dvd_mult_right)
lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
by (rule mult_dvd_mono)
@@ -1333,7 +1266,7 @@
{assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
with h have False by (simp add: mult_assoc)}
hence "n = m * h" by blast
- thus ?thesis by blast
+ thus ?thesis by simp
qed
lemma zdvd_zmult_cancel_disj[simp]:
@@ -1371,8 +1304,8 @@
then show ?thesis by (simp only: negative_eq_positive) auto
qed
qed
- then show ?thesis by (auto elim!: dvdE simp only: zmult_int [symmetric])
-qed
+ then show ?thesis by (auto elim!: dvdE simp only: zdvd_triv_left int_mult)
+qed
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
proof
@@ -1404,10 +1337,10 @@
by (auto simp add: dvd_int_iff)
lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
- by (simp add: zdvd_zminus2_iff)
+ by (rule minus_dvd_iff)
lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
- by (simp add: zdvd_zminus_iff)
+ by (rule dvd_minus_iff)
lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
apply (rule_tac z=n in int_cases)
@@ -1449,20 +1382,13 @@
text {* by Brian Huffman *}
lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
-by (simp only: zmod_zminus1_eq_if mod_mod_trivial)
+by (rule mod_minus_eq [symmetric])
lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
-by (simp only: diff_def zmod_zadd_left_eq [symmetric])
+by (rule mod_diff_left_eq [symmetric])
lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
-proof -
- have "(x + - (y mod m) mod m) mod m = (x + - y mod m) mod m"
- by (simp only: zminus_zmod)
- hence "(x + - (y mod m)) mod m = (x + - y) mod m"
- by (simp only: zmod_zadd_right_eq [symmetric])
- thus "(x - y mod m) mod m = (x - y) mod m"
- by (simp only: diff_def)
-qed
+by (rule mod_diff_right_eq [symmetric])
lemmas zmod_simps =
IntDiv.zmod_zadd_left_eq [symmetric]
--- a/src/HOL/NatBin.thy Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/NatBin.thy Sun Jan 11 14:18:32 2009 +0100
@@ -29,14 +29,14 @@
unfolding nat_number_of_def ..
abbreviation (xsymbols)
- square :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
+ power2 :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
"x\<twosuperior> == x^2"
notation (latex output)
- square ("(_\<twosuperior>)" [1000] 999)
+ power2 ("(_\<twosuperior>)" [1000] 999)
notation (HTML output)
- square ("(_\<twosuperior>)" [1000] 999)
+ power2 ("(_\<twosuperior>)" [1000] 999)
subsection {* Predicate for negative binary numbers *}
--- a/src/HOL/Nominal/nominal_package.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Sun Jan 11 14:18:32 2009 +0100
@@ -571,7 +571,7 @@
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = false, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
- skip_mono = true}
+ skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
(rep_set_names' ~~ recTs'))
[] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
@@ -1509,7 +1509,7 @@
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
- skip_mono = true}
+ skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
--- a/src/HOL/NumberTheory/IntPrimes.thy Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy Sun Jan 11 14:18:32 2009 +0100
@@ -94,7 +94,7 @@
lemma zgcd_zdvd_zgcd_zmult: "zgcd m n dvd zgcd (k * m) n"
apply (simp add: zgcd_greatest_iff)
- apply (blast intro: zdvd_trans)
+ apply (blast intro: zdvd_trans dvd_triv_right)
done
lemma zgcd_zmult_zdvd_zgcd:
--- a/src/HOL/Ring_and_Field.thy Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Sun Jan 11 14:18:32 2009 +0100
@@ -235,19 +235,21 @@
lemma minus_mult_right: "- (a * b) = a * - b"
by (rule equals_zero_I) (simp add: right_distrib [symmetric])
+text{*Extract signs from products*}
+lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
+lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
+
lemma minus_mult_minus [simp]: "- a * - b = a * b"
- by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
+ by simp
lemma minus_mult_commute: "- a * b = a * - b"
- by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
+ by simp
lemma right_diff_distrib: "a * (b - c) = a * b - a * c"
- by (simp add: right_distrib diff_minus
- minus_mult_left [symmetric] minus_mult_right [symmetric])
+ by (simp add: right_distrib diff_minus)
lemma left_diff_distrib: "(a - b) * c = a * c - b * c"
- by (simp add: left_distrib diff_minus
- minus_mult_left [symmetric] minus_mult_right [symmetric])
+ by (simp add: left_distrib diff_minus)
lemmas ring_distribs =
right_distrib left_distrib left_diff_distrib right_diff_distrib
@@ -293,6 +295,33 @@
subclass ring_1 ..
subclass comm_semiring_1_cancel ..
+lemma dvd_minus_iff: "x dvd - y \<longleftrightarrow> x dvd y"
+proof
+ assume "x dvd - y"
+ then have "x dvd - 1 * - y" by (rule dvd_mult)
+ then show "x dvd y" by simp
+next
+ assume "x dvd y"
+ then have "x dvd - 1 * y" by (rule dvd_mult)
+ then show "x dvd - y" by simp
+qed
+
+lemma minus_dvd_iff: "- x dvd y \<longleftrightarrow> x dvd y"
+proof
+ assume "- x dvd y"
+ then obtain k where "y = - x * k" ..
+ then have "y = x * - k" by simp
+ then show "x dvd y" ..
+next
+ assume "x dvd y"
+ then obtain k where "y = x * k" ..
+ then have "y = - x * - k" by simp
+ then show "- x dvd y" ..
+qed
+
+lemma dvd_diff: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
+ by (simp add: diff_minus dvd_add dvd_minus_iff)
+
end
class ring_no_zero_divisors = ring + no_zero_divisors
@@ -397,67 +426,47 @@
apply auto
done
-lemma nonzero_inverse_minus_eq:
- assumes "a \<noteq> 0"
- shows "inverse (- a) = - inverse a"
-proof -
- have "- a * inverse (- a) = - a * - inverse a"
- using assms by simp
- then show ?thesis unfolding mult_cancel_left using assms by simp
-qed
-
-lemma nonzero_inverse_inverse_eq:
- assumes "a \<noteq> 0"
- shows "inverse (inverse a) = a"
-proof -
- have "(inverse (inverse a) * inverse a) * a = a"
- using assms by (simp add: nonzero_imp_inverse_nonzero)
- then show ?thesis using assms by (simp add: mult_assoc)
-qed
-
-lemma nonzero_inverse_eq_imp_eq:
- assumes inveq: "inverse a = inverse b"
- and anz: "a \<noteq> 0"
- and bnz: "b \<noteq> 0"
- shows "a = b"
-proof -
- have "a * inverse b = a * inverse a"
- by (simp add: inveq)
- hence "(a * inverse b) * b = (a * inverse a) * b"
- by simp
- then show "a = b"
- by (simp add: mult_assoc anz bnz)
-qed
-
-lemma inverse_1 [simp]: "inverse 1 = 1"
-proof -
- have "inverse 1 * 1 = 1"
- by (rule left_inverse) (rule one_neq_zero)
- then show ?thesis by simp
-qed
-
lemma inverse_unique:
assumes ab: "a * b = 1"
shows "inverse a = b"
proof -
have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
- moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
- ultimately show ?thesis by (simp add: mult_assoc [symmetric])
+ moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
+ ultimately show ?thesis by (simp add: mult_assoc [symmetric])
qed
+lemma nonzero_inverse_minus_eq:
+ "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
+ by (rule inverse_unique) simp
+
+lemma nonzero_inverse_inverse_eq:
+ "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
+ by (rule inverse_unique) simp
+
+lemma nonzero_inverse_eq_imp_eq:
+ assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
+ shows "a = b"
+proof -
+ from `inverse a = inverse b`
+ have "inverse (inverse a) = inverse (inverse b)"
+ by (rule arg_cong)
+ with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
+ by (simp add: nonzero_inverse_inverse_eq)
+qed
+
+lemma inverse_1 [simp]: "inverse 1 = 1"
+ by (rule inverse_unique) simp
+
lemma nonzero_inverse_mult_distrib:
- assumes anz: "a \<noteq> 0"
- and bnz: "b \<noteq> 0"
+ assumes "a \<noteq> 0" and "b \<noteq> 0"
shows "inverse (a * b) = inverse b * inverse a"
proof -
- have "inverse (a * b) * (a * b) * inverse b = inverse b"
- by (simp add: anz bnz)
- hence "inverse (a * b) * a = inverse b"
- by (simp add: mult_assoc bnz)
- hence "inverse (a * b) * a * inverse a = inverse b * inverse a"
- by simp
+ have "a * (b * inverse b) * inverse a = 1"
+ using assms by simp
+ hence "a * b * (inverse b * inverse a) = 1"
+ by (simp only: mult_assoc)
thus ?thesis
- by (simp add: mult_assoc anz)
+ by (rule inverse_unique)
qed
lemma division_ring_inverse_add:
@@ -1266,19 +1275,19 @@
subsection {* Division and Unary Minus *}
lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
-by (simp add: divide_inverse minus_mult_left)
+by (simp add: divide_inverse)
lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"
-by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)
+by (simp add: divide_inverse nonzero_inverse_minus_eq)
lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
by (simp add: divide_inverse nonzero_inverse_minus_eq)
lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
-by (simp add: divide_inverse minus_mult_left [symmetric])
+by (simp add: divide_inverse)
lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
-by (simp add: divide_inverse minus_mult_right [symmetric])
+by (simp add: divide_inverse)
text{*The effect is to extract signs from divisions*}
@@ -1286,11 +1295,6 @@
lemmas divide_minus_right = minus_divide_right [symmetric]
declare divide_minus_left [simp] divide_minus_right [simp]
-text{*Also, extract signs from products*}
-lemmas mult_minus_left = minus_mult_left [symmetric]
-lemmas mult_minus_right = minus_mult_right [symmetric]
-declare mult_minus_left [simp] mult_minus_right [simp]
-
lemma minus_divide_divide [simp]:
"(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
apply (cases "b=0", simp)
--- a/src/HOL/Tools/datatype_abs_proofs.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Sun Jan 11 14:18:32 2009 +0100
@@ -155,7 +155,7 @@
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
- skip_mono = true}
+ skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Sun Jan 11 14:18:32 2009 +0100
@@ -183,7 +183,7 @@
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
- skip_mono = true}
+ skip_mono = true, fork_mono = false}
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
(map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1;
--- a/src/HOL/Tools/function_package/inductive_wrap.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML Sun Jan 11 14:18:32 2009 +0100
@@ -48,7 +48,8 @@
coind = false,
no_elim = false,
no_ind = false,
- skip_mono = true}
+ skip_mono = true,
+ fork_mono = false}
[((Binding.name R, T), NoSyn)] (* the relation *)
[] (* no parameters *)
(map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *)
--- a/src/HOL/Tools/inductive_package.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Sun Jan 11 14:18:32 2009 +0100
@@ -46,7 +46,7 @@
(Binding.T * string option * mixfix) list ->
(Attrib.binding * string) list ->
(Facts.ref * Attrib.src list) list ->
- local_theory -> inductive_result * local_theory
+ bool -> local_theory -> inductive_result * local_theory
val add_inductive_global: string -> inductive_flags ->
((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
thm list -> theory -> inductive_result * theory
@@ -74,9 +74,9 @@
(Binding.T * string option * mixfix) list ->
(Binding.T * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
- local_theory -> inductive_result * local_theory
+ bool -> local_theory -> inductive_result * local_theory
val gen_ind_decl: add_ind_def -> bool ->
- OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list
+ OuterParse.token list -> (bool -> local_theory -> local_theory) * OuterParse.token list
end;
structure InductivePackage: INDUCTIVE_PACKAGE =
@@ -312,10 +312,11 @@
(* prove monotonicity *)
-fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
- (message (quiet_mode orelse skip_mono andalso !quick_and_dirty)
+fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
+ (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
" Proving monotonicity ...";
- (if skip_mono then SkipProof.prove else Goal.prove) ctxt [] []
+ (if skip_mono then SkipProof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
+ [] []
(HOLogic.mk_Trueprop
(Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
(fn _ => EVERY [rtac @{thm monoI} 1,
@@ -582,7 +583,7 @@
(** specification of (co)inductive predicates **)
-fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
+fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
let
val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
@@ -662,9 +663,11 @@
val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
- val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt''
+ val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt'';
+ val ((_, [mono']), ctxt''') =
+ LocalTheory.note Thm.internalK (Attrib.empty_binding, [mono]) ctxt'';
- in (ctxt'', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
+ in (ctxt''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
list_comb (rec_const, params), preds, argTs, bs, xs)
end;
@@ -718,7 +721,7 @@
type inductive_flags =
{quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T,
- coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool}
+ coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
type add_ind_def =
inductive_flags ->
@@ -726,7 +729,7 @@
term list -> (Binding.T * mixfix) list ->
local_theory -> inductive_result * local_theory
-fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
+fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
cs intros monos params cnames_syn ctxt =
let
val _ = null cnames_syn andalso error "No inductive predicates given";
@@ -739,7 +742,7 @@
apfst split_list (split_list (map (check_rule ctxt cs params) intros));
val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
- argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
+ argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
monos params cnames_syn ctxt;
val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
@@ -780,7 +783,7 @@
(* external interfaces *)
fun gen_add_inductive_i mk_def
- (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono})
+ (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
cnames_syn pnames spec monos lthy =
let
val thy = ProofContext.theory_of lthy;
@@ -836,7 +839,7 @@
||> fold (snd oo LocalTheory.abbrev Syntax.mode_default) abbrevs
end;
-fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
+fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
let
val ((vars, specs), _) = lthy |> ProofContext.set_mode ProofContext.mode_abbrev
|> Specification.read_specification
@@ -845,7 +848,8 @@
val intrs = map (apsnd the_single) specs;
val monos = Attrib.eval_thms lthy raw_monos;
val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
- alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false, skip_mono = false};
+ alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
+ skip_mono = false, fork_mono = not int};
in
lthy
|> LocalTheory.set_group (serial_string ())
@@ -956,12 +960,12 @@
Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] --
Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
>> (fn (((preds, params), specs), monos) =>
- (snd o gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
+ (snd oo gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
val ind_decl = gen_ind_decl add_ind_def;
-val _ = OuterSyntax.local_theory "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
-val _ = OuterSyntax.local_theory "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
+val _ = OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
+val _ = OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
val _ =
OuterSyntax.local_theory "inductive_cases"
--- a/src/HOL/Tools/inductive_realizer.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Jan 11 14:18:32 2009 +0100
@@ -347,7 +347,7 @@
val (ind_info, thy3') = thy2 |>
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
- coind = false, no_elim = false, no_ind = false, skip_mono = false}
+ coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
((Binding.name (Sign.base_name (name_of_thm intr)), []),
subst_atomic rlzpreds' (Logic.unvarify rintr)))
--- a/src/HOL/Tools/inductive_set_package.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Sun Jan 11 14:18:32 2009 +0100
@@ -20,7 +20,7 @@
(Binding.T * string option * mixfix) list ->
(Binding.T * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
- local_theory -> InductivePackage.inductive_result * local_theory
+ bool -> local_theory -> InductivePackage.inductive_result * local_theory
val codegen_preproc: theory -> thm list -> thm list
val setup: theory -> theory
end;
@@ -403,7 +403,8 @@
(**** definition of inductive sets ****)
-fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
+fun add_ind_set_def
+ {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
cs intros monos params cnames_syn ctxt =
let
val thy = ProofContext.theory_of ctxt;
@@ -468,7 +469,8 @@
val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
InductivePackage.add_ind_def
{quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty,
- coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
+ coind = coind, no_elim = no_elim, no_ind = no_ind,
+ skip_mono = skip_mono, fork_mono = fork_mono}
cs' intros' monos' params1 cnames_syn' ctxt;
(* define inductive sets using previously defined predicates *)
@@ -550,10 +552,10 @@
val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def;
val _ =
- OuterSyntax.local_theory "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
+ OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
val _ =
- OuterSyntax.local_theory "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
+ OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
end;
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Sun Jan 11 14:18:32 2009 +0100
@@ -10,6 +10,12 @@
structure Domain_Theorems = struct
+val quiet_mode = ref false;
+val trace_domain = ref false;
+
+fun message s = if !quiet_mode then () else writeln s;
+fun trace s = if !trace_domain then tracing s else ();
+
local
val adm_impl_admw = @{thm adm_impl_admw};
@@ -115,7 +121,7 @@
fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
let
-val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
+val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
val pg = pg' thy;
(* ----- getting the axioms and definitions --------------------------------- *)
@@ -158,6 +164,8 @@
(* ----- generating beta reduction rules from definitions-------------------- *)
+val _ = trace " Proving beta reduction rules...";
+
local
fun arglist (Const _ $ Abs (s, _, t)) =
let
@@ -179,7 +187,9 @@
in pg (def::betas) appl (K [rtac reflexive_thm 1]) end;
end;
+val _ = trace "Proving when_appl...";
val when_appl = appl_of_def ax_when_def;
+val _ = trace "Proving con_appls...";
val con_appls = map appl_of_def axs_con_def;
local
@@ -229,7 +239,9 @@
rewrite_goals_tac [mk_meta_eq iso_swap],
rtac thm3 1];
in
+ val _ = trace " Proving exhaust...";
val exhaust = pg con_appls (mk_trp exh) (K tacs);
+ val _ = trace " Proving casedist...";
val casedist =
standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
end;
@@ -239,6 +251,7 @@
fun bound_fun i _ = Bound (length cons - i);
val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons);
in
+ val _ = trace " Proving when_strict...";
val when_strict =
let
val axs = [when_appl, mk_meta_eq rep_strict];
@@ -246,6 +259,7 @@
val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
in pg axs goal (K tacs) end;
+ val _ = trace " Proving when_apps...";
val when_apps =
let
fun one_when n (con,args) =
@@ -276,6 +290,7 @@
val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
in pg axs_dis_def goal (K tacs) end;
+ val _ = trace " Proving dis_apps...";
val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
fun dis_defin (con, args) =
@@ -288,7 +303,9 @@
(asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
in pg [] goal (K tacs) end;
+ val _ = trace " Proving dis_stricts...";
val dis_stricts = map dis_strict cons;
+ val _ = trace " Proving dis_defins...";
val dis_defins = map dis_defin cons;
in
val dis_rews = dis_stricts @ dis_defins @ dis_apps;
@@ -301,6 +318,7 @@
val tacs = [rtac when_strict 1];
in pg axs_mat_def goal (K tacs) end;
+ val _ = trace " Proving mat_stricts...";
val mat_stricts = map mat_strict cons;
fun one_mat c (con, args) =
@@ -314,6 +332,7 @@
val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
in pg axs_mat_def goal (K tacs) end;
+ val _ = trace " Proving mat_apps...";
val mat_apps =
maps (fn (c,_) => map (one_mat c) cons) cons;
in
@@ -346,7 +365,9 @@
val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
in pg axs goal (K tacs) end;
+ val _ = trace " Proving pat_stricts...";
val pat_stricts = map pat_strict cons;
+ val _ = trace " Proving pat_apps...";
val pat_apps = maps (fn c => map (pat_app c) cons) cons;
in
val pat_rews = pat_stricts @ pat_apps;
@@ -374,7 +395,9 @@
asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
in pg [] goal tacs end;
in
+ val _ = trace " Proving con_stricts...";
val con_stricts = maps con_strict cons;
+ val _ = trace " Proving pat_defins...";
val con_defins = map con_defin cons;
val con_rews = con_stricts @ con_defins;
end;
@@ -391,6 +414,7 @@
REPEAT (resolve_tac rules 1 ORELSE atac 1)];
in pg con_appls goal (K tacs) end;
in
+ val _ = trace " Proving con_compacts...";
val con_compacts = map con_compact cons;
end;
@@ -402,6 +426,7 @@
fun sel_strict (_, args) =
List.mapPartial (Option.map one_sel o sel_of) args;
in
+ val _ = trace " Proving sel_stricts...";
val sel_stricts = maps sel_strict cons;
end;
@@ -439,6 +464,7 @@
fun one_con (c, args) =
flat (map_filter I (mapn (one_sel' c) 0 args));
in
+ val _ = trace " Proving sel_apps...";
val sel_apps = maps one_con cons;
end;
@@ -453,6 +479,7 @@
(asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
in pg [] goal (K tacs) end;
in
+ val _ = trace " Proving sel_defins...";
val sel_defins =
if length cons = 1
then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
@@ -463,6 +490,7 @@
val sel_rews = sel_stricts @ sel_defins @ sel_apps;
val rev_contrapos = @{thm rev_contrapos};
+val _ = trace " Proving dist_les...";
val distincts_le =
let
fun dist (con1, args1) (con2, args2) =
@@ -487,6 +515,8 @@
| distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
in distincts cons end;
val dist_les = flat (flat distincts_le);
+
+val _ = trace " Proving dist_eqs...";
val dist_eqs =
let
fun distinct (_,args1) ((_,args2), leqs) =
@@ -517,6 +547,7 @@
in pg con_appls prop end;
val cons' = List.filter (fn (_,args) => args<>[]) cons;
in
+ val _ = trace " Proving inverts...";
val inverts =
let
val abs_less = ax_abs_iso RS (allI RS injection_less);
@@ -524,6 +555,7 @@
[asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end;
+ val _ = trace " Proving injects...";
val injects =
let
val abs_eq = ax_abs_iso RS (allI RS injection_eq);
@@ -551,6 +583,7 @@
val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1];
in pg [ax_copy_def] goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
in
+ val _ = trace " Proving copy_apps...";
val copy_apps = map copy_app cons;
end;
@@ -565,6 +598,7 @@
fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
in
+ val _ = trace " Proving copy_stricts...";
val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons);
end;
@@ -603,7 +637,7 @@
val conss = map snd eqs;
val comp_dname = Sign.full_bname thy comp_dnam;
-val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
+val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
val pg = pg' thy;
(* ----- getting the composite axiom and definitions ------------------------ *)
@@ -639,6 +673,7 @@
val copy_con_rews = copy_rews @ con_rews;
val copy_take_defs =
(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
+ val _ = trace " Proving take_stricts...";
val take_stricts =
let
fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
@@ -656,6 +691,7 @@
in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
val take_0s = mapn take_0 1 dnames;
fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
+ val _ = trace " Proving take_apps...";
val take_apps =
let
fun mk_eqn dn (con, args) =
@@ -737,6 +773,7 @@
val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
end;
in (* local *)
+ val _ = trace " Proving finite_ind...";
val finite_ind =
let
fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
@@ -768,6 +805,7 @@
end;
in pg'' thy [] goal tacf end;
+ val _ = trace " Proving take_lemmas...";
val take_lemmas =
let
fun take_lemma n (dn, ax_reach) =
@@ -793,6 +831,7 @@
(* ----- theorems concerning finiteness and induction ----------------------- *)
+ val _ = trace " Proving finites, ind...";
val (finites, ind) =
if is_finite
then (* finite case *)
@@ -914,6 +953,7 @@
fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
val take_ss = HOL_ss addsimps take_rews;
val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
+ val _ = trace " Proving coind_lemma...";
val coind_lemma =
let
fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
@@ -940,6 +980,7 @@
flat (mapn (x_tacs ctxt) 0 xs);
in pg [ax_bisim_def] goal tacs end;
in
+ val _ = trace " Proving coind...";
val coind =
let
fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
--- a/src/Pure/Concurrent/future.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/Concurrent/future.ML Sun Jan 11 14:18:32 2009 +0100
@@ -45,6 +45,7 @@
val join: 'a future -> 'a
val map: ('a -> 'b) -> 'a future -> 'b future
val interrupt_task: string -> unit
+ val cancel_group: group -> unit
val cancel: 'a future -> unit
val shutdown: unit -> unit
end;
@@ -330,17 +331,18 @@
end;
-(* cancel *)
+(* cancellation *)
(*interrupt: permissive signal, may get ignored*)
fun interrupt_task id = SYNCHRONIZED "interrupt"
(fn () => Task_Queue.interrupt_external (! queue) id);
(*cancel: present and future group members will be interrupted eventually*)
-fun cancel x =
+fun cancel_group group =
(scheduler_check "cancel check";
- SYNCHRONIZED "cancel" (fn () => (do_cancel (group_of x); notify_all ())));
+ SYNCHRONIZED "cancel" (fn () => (do_cancel group; notify_all ())));
+fun cancel x = cancel_group (group_of x);
(** global join and shutdown **)
--- a/src/Pure/General/lazy.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/General/lazy.ML Sun Jan 11 14:18:32 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/lazy.ML
- ID: $Id$
Author: Florian Haftmann and Makarius, TU Muenchen
Lazy evaluation with memoing. Concurrency may lead to multiple
@@ -13,6 +12,7 @@
val lazy: (unit -> 'a) -> 'a lazy
val value: 'a -> 'a lazy
val peek: 'a lazy -> 'a Exn.result option
+ val force_result: 'a lazy -> 'a Exn.result
val force: 'a lazy -> 'a
val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
end
@@ -41,7 +41,7 @@
(* force result *)
-fun force r =
+fun force_result r =
let
(*potentially concurrent evaluation*)
val res =
@@ -53,7 +53,9 @@
(case ! r of
Lazy _ => (r := Result res; res)
| Result res' => res'));
- in Exn.release res' end;
+ in res' end;
+
+fun force r = Exn.release (force_result r);
fun map_force f = value o f o force;
--- a/src/Pure/General/markup.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/General/markup.ML Sun Jan 11 14:18:32 2009 +0100
@@ -85,8 +85,9 @@
val subgoalN: string val subgoal: T
val sendbackN: string val sendback: T
val hiliteN: string val hilite: T
+ val taskN: string
val unprocessedN: string val unprocessed: T
- val runningN: string val running: T
+ val runningN: string val running: string -> T
val failedN: string val failed: T
val finishedN: string val finished: T
val disposedN: string val disposed: T
@@ -259,8 +260,10 @@
(* command status *)
+val taskN = "task";
+
val (unprocessedN, unprocessed) = markup_elem "unprocessed";
-val (runningN, running) = markup_elem "running";
+val (runningN, running) = markup_string "running" taskN;
val (failedN, failed) = markup_elem "failed";
val (finishedN, finished) = markup_elem "finished";
val (disposedN, disposed) = markup_elem "disposed";
--- a/src/Pure/General/markup.scala Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/General/markup.scala Sun Jan 11 14:18:32 2009 +0100
@@ -110,6 +110,8 @@
/* command status */
+ val TASK = "task"
+
val UNPROCESSED = "unprocessed"
val RUNNING = "running"
val FAILED = "failed"
--- a/src/Pure/Isar/isar.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/Isar/isar.ML Sun Jan 11 14:18:32 2009 +0100
@@ -194,7 +194,7 @@
Finished of Toplevel.state;
fun status_markup Unprocessed = Markup.unprocessed
- | status_markup Running = Markup.running
+ | status_markup Running = (Markup.runningN, [])
| status_markup (Failed _) = Markup.failed
| status_markup (Finished _) = Markup.finished;
--- a/src/Pure/Isar/outer_syntax.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Sun Jan 11 14:18:32 2009 +0100
@@ -32,7 +32,7 @@
type isar
val isar: bool -> isar
val prepare_command: Position.T -> string -> Toplevel.transition
- val load_thy: string -> Position.T -> string list -> bool -> unit
+ val load_thy: string -> Position.T -> string list -> bool -> unit -> unit
end;
structure OuterSyntax: OUTER_SYNTAX =
@@ -288,16 +288,13 @@
(fn () => HTML.html_mode (implode o map ThySyntax.present_span) spans);
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
- val _ = cond_timeit time "" (fn () =>
- let
- val (results, commit_exit) = Toplevel.excursion units;
- val _ =
- ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup results toks
- |> Buffer.content
- |> Present.theory_output name
- val _ = commit_exit ();
- in () end);
+ val results = cond_timeit time "" (fn () => Toplevel.excursion units);
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
- in () end;
+
+ fun after_load () =
+ ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup (Lazy.force results) toks
+ |> Buffer.content
+ |> Present.theory_output name;
+ in after_load end;
end;
--- a/src/Pure/Isar/proof.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/Isar/proof.ML Sun Jan 11 14:18:32 2009 +0100
@@ -345,7 +345,8 @@
(case filter_out (fn s => s = "") strs of [] => ""
| strs' => enclose " (" ")" (commas strs'));
- fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) =
+ fun prt_goal (SOME (ctxt, (i,
+ {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
pretty_facts "using " ctxt
(if mode <> Backward orelse null using then NONE else SOME using) @
[Pretty.str ("goal" ^
@@ -1040,7 +1041,7 @@
local
fun future_terminal_proof proof1 proof2 meths int state =
- if int orelse is_relevant state orelse not (Future.enabled ())
+ if int orelse is_relevant state orelse not (Future.enabled () andalso ! Goal.parallel_proofs)
then proof1 meths state
else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
--- a/src/Pure/Isar/session.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/Isar/session.ML Sun Jan 11 14:18:32 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/session.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Session management -- maintain state of logic images.
@@ -11,7 +10,7 @@
val name: unit -> string
val welcome: unit -> string
val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
- string -> string -> bool * string -> string -> int -> bool -> int -> int -> unit
+ string -> string -> bool * string -> string -> int -> bool -> int -> int -> bool -> unit
val finish: unit -> unit
end;
@@ -87,7 +86,7 @@
| dumping (cp, path) = SOME (cp, Path.explode path);
fun use_dir root build modes reset info doc doc_graph doc_versions
- parent name dump rpath level verbose max_threads trace_threads =
+ parent name dump rpath level verbose max_threads trace_threads parallel_proofs =
((fn () =>
(init reset parent name;
Present.init build info doc doc_graph doc_versions (path ()) name
@@ -96,6 +95,7 @@
finish ()))
|> setmp_noncritical Proofterm.proofs level
|> setmp_noncritical print_mode (modes @ print_mode_value ())
+ |> setmp_noncritical Goal.parallel_proofs parallel_proofs
|> setmp_noncritical Multithreading.trace trace_threads
|> setmp_noncritical Multithreading.max_threads
(if Multithreading.available then max_threads
--- a/src/Pure/Isar/skip_proof.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/Isar/skip_proof.ML Sun Jan 11 14:18:32 2009 +0100
@@ -34,7 +34,8 @@
ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
fun prove ctxt xs asms prop tac =
- (if Future.enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
+ (if Future.enabled () andalso ! Goal.parallel_proofs then Goal.prove_future else Goal.prove)
+ ctxt xs asms prop
(fn args => fn st =>
if ! quick_and_dirty
then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
--- a/src/Pure/Isar/toplevel.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Sun Jan 11 14:18:32 2009 +0100
@@ -96,7 +96,7 @@
val transition: bool -> transition -> state -> (state * (exn * string) option) option
val commit_exit: Position.T -> transition
val command: transition -> state -> state
- val excursion: (transition * transition list) list -> (transition * state) list * (unit -> unit)
+ val excursion: (transition * transition list) list -> (transition * state) list lazy
end;
structure Toplevel: TOPLEVEL =
@@ -745,13 +745,13 @@
let
val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
- val immediate = not (Future.enabled ());
- val (future_results, end_state) = fold_map (proof_result immediate) input toplevel;
+ val immediate = not (Future.enabled () andalso ! Goal.parallel_proofs);
+ val (results, end_state) = fold_map (proof_result immediate) input toplevel;
val _ =
(case end_state of
- State (NONE, SOME (Theory (Context.Theory _, _), _)) => ()
+ State (NONE, SOME (Theory (Context.Theory _, _), _)) =>
+ command (commit_exit end_pos) end_state
| _ => error "Unfinished development at end of input");
- val results = maps Lazy.force future_results;
- in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end;
+ in Lazy.lazy (fn () => maps Lazy.force results) end;
end;
--- a/src/Pure/ProofGeneral/preferences.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML Sun Jan 11 14:18:32 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/preferences.ML
- ID: $Id$
Author: David Aspinall and Markus Wenzel
User preferences for Isabelle which are maintained by the interface.
@@ -164,7 +163,10 @@
proof_pref,
nat_pref Multithreading.max_threads
"max-threads"
- "Maximum number of threads"];
+ "Maximum number of threads",
+ bool_pref Goal.parallel_proofs
+ "parallel-proofs"
+ "Check proofs in parallel"];
val pure_preferences =
[("Display", display_preferences),
--- a/src/Pure/Thy/thy_info.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/Thy/thy_info.ML Sun Jan 11 14:18:32 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/thy_info.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Main part of theory loader database, including handling of theory and
@@ -24,6 +23,8 @@
val get_parents: string -> string list
val touch_thy: string -> unit
val touch_child_thys: string -> unit
+ val remove_thy: string -> unit
+ val kill_thy: string -> unit
val provide_file: Path.T -> string -> unit
val load_file: bool -> Path.T -> unit
val exec_file: bool -> Path.T -> Context.generic -> Context.generic
@@ -32,8 +33,6 @@
val use_thys: string list -> unit
val use_thy: string -> unit
val time_use_thy: string -> unit
- val remove_thy: string -> unit
- val kill_thy: string -> unit
val thy_ord: theory * theory -> order
val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
val end_theory: theory -> unit
@@ -232,6 +231,35 @@
end;
+(* manage pending proofs *)
+
+fun join_thy name =
+ (case lookup_theory name of
+ NONE => []
+ | SOME thy => PureThy.join_proofs thy);
+
+fun cancel_thy name =
+ (case lookup_theory name of
+ NONE => ()
+ | SOME thy => PureThy.cancel_proofs thy);
+
+
+(* remove theory *)
+
+fun remove_thy name =
+ if is_finished name then error (loader_msg "cannot remove finished theory" [name])
+ else
+ let
+ val succs = thy_graph Graph.all_succs [name];
+ val _ = List.app cancel_thy succs;
+ val _ = priority (loader_msg "removing" succs);
+ val _ = CRITICAL (fn () =>
+ (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)));
+ in () end;
+
+val kill_thy = if_known_thy remove_thy;
+
+
(* load_file *)
local
@@ -300,33 +328,29 @@
val _ = CRITICAL (fn () =>
change_deps name (Option.map (fn {master, text, parents, files, ...} =>
make_deps upd_time master text parents files)));
- val _ = OuterSyntax.load_thy name pos text (time orelse ! Output.timing);
- in
- CRITICAL (fn () =>
- (change_deps name
- (Option.map (fn {update_time, master, parents, files, ...} =>
- make_deps update_time master [] parents files));
- perform Update name))
- end;
+ val after_load = OuterSyntax.load_thy name pos text (time orelse ! Output.timing);
+ val _ =
+ CRITICAL (fn () =>
+ (change_deps name
+ (Option.map (fn {update_time, master, parents, files, ...} =>
+ make_deps update_time master [] parents files));
+ perform Update name));
+ in after_load end;
(* scheduling loader tasks *)
-datatype task = Task of (unit -> unit) | Finished | Running;
+datatype task = Task of (unit -> unit -> unit) | Finished | Running;
fun task_finished Finished = true | task_finished _ = false;
local
-fun schedule_seq tasks =
- Graph.topological_order tasks
- |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ()));
-
fun schedule_futures task_graph =
let
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));
- fun future (name, body) tab =
+ fun fork (name, body) tab =
let
val deps = Graph.imm_preds task_graph name
|> map_filter (fn parent =>
@@ -338,12 +362,23 @@
[] => body ()
| bad => error (loader_msg
("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
+ in Symtab.update (name, x) tab end;
- in (x, Symtab.update (name, x) tab) end;
+ val futures = fold fork tasks Symtab.empty;
- val thy_results = Future.join_results (#1 (fold_map future tasks Symtab.empty));
- val proof_results = PureThy.join_proofs (map_filter (try get_theory o #1) tasks);
- in ignore (Exn.release_all (thy_results @ proof_results)) end;
+ val exns = rev tasks |> maps (fn (name, _) =>
+ let
+ val after_load = Future.join (the (Symtab.lookup futures name));
+ val proof_exns = join_thy name;
+ val _ = null proof_exns orelse raise Exn.EXCEPTIONS proof_exns;
+ val _ = after_load ();
+ in [] end handle exn => (kill_thy name; [exn]));
+
+ in ignore (Exn.release_all (map Exn.Exn (rev exns))) end;
+
+fun schedule_seq tasks =
+ Graph.topological_order tasks
+ |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () () | _ => ()));
in
@@ -464,19 +499,6 @@
end;
-(* remove theory *)
-
-fun remove_thy name =
- if is_finished name then error (loader_msg "cannot remove finished theory" [name])
- else
- let val succs = thy_graph Graph.all_succs [name] in
- priority (loader_msg "removing" succs);
- CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)))
- end;
-
-val kill_thy = if_known_thy remove_thy;
-
-
(* update_time *)
structure UpdateTime = TheoryDataFun
--- a/src/Pure/Thy/thy_load.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/Thy/thy_load.ML Sun Jan 11 14:18:32 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/thy_load.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Theory loader primitives, including load path.
@@ -22,6 +21,7 @@
val ml_exts: string list
val ml_path: string -> Path.T
val thy_path: string -> Path.T
+ val split_thy_path: Path.T -> Path.T * string
val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
val check_thy: Path.T -> string -> Path.T * File.ident
@@ -62,6 +62,11 @@
val ml_path = Path.ext "ML" o Path.basic;
val thy_path = Path.ext "thy" o Path.basic;
+fun split_thy_path path =
+ (case Path.split_ext path of
+ (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
+ | _ => error ("Bad theory file specification " ^ Path.implode path));
+
(* check files *)
--- a/src/Pure/goal.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/goal.ML Sun Jan 11 14:18:32 2009 +0100
@@ -6,6 +6,7 @@
signature BASIC_GOAL =
sig
+ val parallel_proofs: bool ref
val SELECT_GOAL: tactic -> int -> tactic
val CONJUNCTS: tactic -> int -> tactic
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -123,6 +124,8 @@
|> fold (Thm.elim_implies o Thm.assume) assms;
in local_result end;
+val parallel_proofs = ref true;
+
(** tactical theorem proving **)
@@ -172,7 +175,8 @@
else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
end);
val res =
- if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (Future.enabled ())
+ if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse
+ not (Future.enabled () andalso ! parallel_proofs)
then result ()
else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
in
--- a/src/Pure/pure_thy.ML Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/pure_thy.ML Sun Jan 11 14:18:32 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/pure_thy.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Theorem storage. Pure theory syntax and logical content.
@@ -11,7 +10,8 @@
val intern_fact: theory -> xstring -> string
val defined_fact: theory -> string -> bool
val hide_fact: bool -> string -> theory -> theory
- val join_proofs: theory list -> unit Exn.result list
+ val join_proofs: theory -> exn list
+ val cancel_proofs: theory -> unit
val get_fact: Context.generic -> theory -> Facts.ref -> thm list
val get_thms: theory -> xstring -> thm list
val get_thm: theory -> xstring -> thm
@@ -59,11 +59,11 @@
structure FactsData = TheoryDataFun
(
- type T = Facts.T * unit lazy list;
- val empty = (Facts.empty, []);
+ type T = Facts.T * (unit lazy list * Task_Queue.group list);
+ val empty = (Facts.empty, ([], []));
val copy = I;
- fun extend (facts, _) = (facts, []);
- fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
+ fun extend (facts, _) = (facts, ([], []));
+ fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
);
@@ -81,7 +81,10 @@
fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
-val join_proofs = maps (fn thy => map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy))));
+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)));
@@ -142,7 +145,8 @@
(* enter_thms *)
fun enter_proofs (thy, thms) =
- (FactsData.map (apsnd (fold (cons o lazy_proof) thms)) thy, thms);
+ (FactsData.map (apsnd (fn (proofs, groups) =>
+ (fold (cons o lazy_proof) thms proofs, fold Thm.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 Sun Jan 11 14:18:17 2009 +0100
+++ b/src/Pure/thm.ML Sun Jan 11 14:18:32 2009 +0100
@@ -146,6 +146,7 @@
val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
val freezeT: thm -> thm
val future: thm future -> cterm -> thm
+ val pending_groups: thm -> Task_Queue.group list -> Task_Queue.group list
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
val join_proof: thm -> unit
@@ -1626,7 +1627,13 @@
end;
-(* fulfilled proof *)
+(* pending task groups *)
+
+fun pending_groups (Thm (Deriv {open_promises, ...}, _)) =
+ fold (insert Task_Queue.eq_group o Future.group_of o #2) open_promises;
+
+
+(* fulfilled proofs *)
fun raw_proof_of (Thm (Deriv {body, ...}, _)) = Proofterm.proof_of body;