--- a/Admin/isatest/isatest-makeall Thu Aug 27 15:49:45 2009 +0100
+++ b/Admin/isatest/isatest-makeall Fri Aug 28 13:32:20 2009 +0100
@@ -80,7 +80,7 @@
NICE=""
;;
- macbroy21)
+ macbroy22)
MFLAGS="-k"
NICE=""
;;
--- a/Admin/isatest/isatest-makedist Thu Aug 27 15:49:45 2009 +0100
+++ b/Admin/isatest/isatest-makedist Fri Aug 28 13:32:20 2009 +0100
@@ -94,13 +94,13 @@
$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
# give test some time to copy settings and start
sleep 15
-$SSH macbroy21 "$MAKEALL $HOME/settings/at-poly"
+$SSH macbroy22 "$MAKEALL $HOME/settings/at-poly"
sleep 15
$SSH macbroy20 "$MAKEALL $HOME/settings/at-poly-5.1-para-e"
sleep 15
#$SSH macbroy24 "$MAKEALL -l HOL proofterms $HOME/settings/at-sml-dev-p"
#sleep 15
-$SSH macbroy22 "$MAKEALL $HOME/settings/at64-poly-5.1-para"
+$SSH macbroy21 "$MAKEALL $HOME/settings/at64-poly-5.1-para"
sleep 15
$SSH macbroy23 -l HOL images "$MAKEALL $HOME/settings/at-sml-dev-e"
sleep 15
--- a/Admin/isatest/isatest-stats Thu Aug 27 15:49:45 2009 +0100
+++ b/Admin/isatest/isatest-stats Fri Aug 28 13:32:20 2009 +0100
@@ -6,7 +6,7 @@
THIS=$(cd "$(dirname "$0")"; pwd -P)
-PLATFORMS="at-poly at64-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev"
+PLATFORMS="at-poly at64-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev"
ISABELLE_SESSIONS="\
HOL-Plain \
--- a/NEWS Thu Aug 27 15:49:45 2009 +0100
+++ b/NEWS Fri Aug 28 13:32:20 2009 +0100
@@ -18,22 +18,25 @@
*** HOL ***
-* New testing tool "Mirabelle" for automated (proof) tools. Applies several
-tools and tactics like sledgehammer, metis, or quickcheck, to every proof step
-in a theory. To be used in batch mode via "isabelle mirabelle".
-
-* New proof method "sos" (sum of squares) for nonlinear real arithmetic
-(originally due to John Harison). It requires Library/Sum_Of_Squares.
-It is not a complete decision procedure but works well in practice
-on quantifier-free real arithmetic with +, -, *, ^, =, <= and <,
-i.e. boolean combinations of equalities and inequalities between
-polynomials. It makes use of external semidefinite programming solvers.
-For more information and examples see Library/Sum_Of_Squares.
-
-* Set.UNIV and Set.empty are mere abbreviations for top and bot. INCOMPATIBILITY.
-
-* More convenient names for set intersection and union. INCOMPATIBILITY:
-
+* New testing tool "Mirabelle" for automated (proof) tools. Applies
+several tools and tactics like sledgehammer, metis, or quickcheck, to
+every proof step in a theory. To be used in batch mode via the
+"mirabelle" utility.
+
+* New proof method "sos" (sum of squares) for nonlinear real
+arithmetic (originally due to John Harison). It requires
+Library/Sum_Of_Squares. It is not a complete decision procedure but
+works well in practice on quantifier-free real arithmetic with +, -,
+*, ^, =, <= and <, i.e. boolean combinations of equalities and
+inequalities between polynomials. It makes use of external
+semidefinite programming solvers. For more information and examples
+see src/HOL/Library/Sum_Of_Squares.
+
+* Set.UNIV and Set.empty are mere abbreviations for top and bot.
+INCOMPATIBILITY.
+
+* More convenient names for set intersection and union.
+INCOMPATIBILITY:
Set.Int ~> Set.inter
Set.Un ~> Set.union
@@ -43,8 +46,6 @@
etc.
INCOMPATIBILITY.
-* New quickcheck implementation using new code generator.
-
* New class "boolean_algebra".
* Refinements to lattices classes:
@@ -81,15 +82,16 @@
multiplicative monoids retains syntax "^" and is now defined generic
in class power. INCOMPATIBILITY.
-* Relation composition "R O S" now has a "more standard" argument order,
-i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }".
+* Relation composition "R O S" now has a "more standard" argument
+order, i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }".
INCOMPATIBILITY: Rewrite propositions with "S O R" --> "R O S". Proofs
-may occationally break, since the O_assoc rule was not rewritten like this.
-Fix using O_assoc[symmetric].
-The same applies to the curried version "R OO S".
-
-* GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm of finite and
-infinite sets. It is shown that they form a complete lattice.
+may occationally break, since the O_assoc rule was not rewritten like
+this. Fix using O_assoc[symmetric]. The same applies to the curried
+version "R OO S".
+
+* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
+of finite and infinite sets. It is shown that they form a complete
+lattice.
* ML antiquotation @{code_datatype} inserts definition of a datatype
generated by the code generator; see Predicate.thy for an example.
@@ -97,9 +99,9 @@
* New method "linarith" invokes existing linear arithmetic decision
procedure only.
-* Implementation of quickcheck using generic code generator; default
-generators are provided for all suitable HOL types, records and
-datatypes.
+* New implementation of quickcheck uses generic code generator;
+default generators are provided for all suitable HOL types, records
+and datatypes.
* Constants Set.Pow and Set.image now with authentic syntax;
object-logic definitions Set.Pow_def and Set.image_def.
@@ -121,17 +123,13 @@
DatatypePackage ~> Datatype
InductivePackage ~> Inductive
- etc.
-
INCOMPATIBILITY.
* NewNumberTheory: Jeremy Avigad's new version of part of
NumberTheory. If possible, use NewNumberTheory, not NumberTheory.
-* Simplified interfaces of datatype module. INCOMPATIBILITY.
-
-* Abbreviation "arbitrary" of "undefined" has disappeared; use
-"undefined" directly. INCOMPATIBILITY.
+* Discontinued abbreviation "arbitrary" of constant
+"undefined". INCOMPATIBILITY, use "undefined" directly.
* New evaluator "approximate" approximates an real valued term using
the same method as the approximation method.
@@ -155,10 +153,14 @@
* PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
parallel tactical reasoning.
-* Tactical FOCUS is similar to SUBPROOF, but allows the body tactic to
-introduce new subgoals and schematic variables. FOCUS_PARAMS is
-similar, but focuses on the parameter prefix only, leaving subgoal
-premises unchanged.
+* Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS
+are similar to SUBPROOF, but are slightly more flexible: only the
+specified parts of the subgoal are imported into the context, and the
+body tactic may introduce new subgoals and schematic variables.
+
+* Old tactical METAHYPS, which does not observe the proof context, has
+been renamed to Old_Goals.METAHYPS and awaits deletion. Use SUBPROOF
+or Subgoal.FOCUS etc.
* Renamed functor TableFun to Table, and GraphFun to Graph. (Since
functors have their own ML name space there is no point to mark them
--- a/etc/settings Thu Aug 27 15:49:45 2009 +0100
+++ b/etc/settings Fri Aug 28 13:32:20 2009 +0100
@@ -173,7 +173,7 @@
# The pdf file viewer
if [ $(uname -s) = Darwin ]; then
- PDF_VIEWER=open
+ PDF_VIEWER="open -W -n"
else
PDF_VIEWER=xpdf
fi
--- a/src/HOL/List.thy Thu Aug 27 15:49:45 2009 +0100
+++ b/src/HOL/List.thy Fri Aug 28 13:32:20 2009 +0100
@@ -3835,4 +3835,117 @@
"setsum f (set [i..j::int]) = listsum (map f [i..j])"
by (rule setsum_set_distinct_conv_listsum) simp
+
+text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
+and similiarly for @{text"\<exists>"}. *}
+
+function all_from_to_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
+"all_from_to_nat P i j =
+ (if i < j then if P i then all_from_to_nat P (i+1) j else False
+ else True)"
+by auto
+termination
+by (relation "measure(%(P,i,j). j - i)") auto
+
+declare all_from_to_nat.simps[simp del]
+
+lemma all_from_to_nat_iff_ball:
+ "all_from_to_nat P i j = (ALL n : {i ..< j}. P n)"
+proof(induct P i j rule:all_from_to_nat.induct)
+ case (1 P i j)
+ let ?yes = "i < j & P i"
+ show ?case
+ proof (cases)
+ assume ?yes
+ hence "all_from_to_nat P i j = (P i & all_from_to_nat P (i+1) j)"
+ by(simp add: all_from_to_nat.simps)
+ also have "... = (P i & (ALL n : {i+1 ..< j}. P n))" using `?yes` 1 by simp
+ also have "... = (ALL n : {i ..< j}. P n)" (is "?L = ?R")
+ proof
+ assume L: ?L
+ show ?R
+ proof clarify
+ fix n assume n: "n : {i..<j}"
+ show "P n"
+ proof cases
+ assume "n = i" thus "P n" using L by simp
+ next
+ assume "n ~= i"
+ hence "i+1 <= n" using n by auto
+ thus "P n" using L n by simp
+ qed
+ qed
+ next
+ assume R: ?R thus ?L using `?yes` 1 by auto
+ qed
+ finally show ?thesis .
+ next
+ assume "~?yes" thus ?thesis by(auto simp add: all_from_to_nat.simps)
+ qed
+qed
+
+
+lemma list_all_iff_all_from_to_nat[code_unfold]:
+ "list_all P [i..<j] = all_from_to_nat P i j"
+by(simp add: all_from_to_nat_iff_ball list_all_iff)
+
+lemma list_ex_iff_not_all_from_to_not_nat[code_unfold]:
+ "list_ex P [i..<j] = (~all_from_to_nat (%x. ~P x) i j)"
+by(simp add: all_from_to_nat_iff_ball list_ex_iff)
+
+
+function all_from_to_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
+"all_from_to_int P i j =
+ (if i <= j then if P i then all_from_to_int P (i+1) j else False
+ else True)"
+by auto
+termination
+by (relation "measure(%(P,i,j). nat(j - i + 1))") auto
+
+declare all_from_to_int.simps[simp del]
+
+lemma all_from_to_int_iff_ball:
+ "all_from_to_int P i j = (ALL n : {i .. j}. P n)"
+proof(induct P i j rule:all_from_to_int.induct)
+ case (1 P i j)
+ let ?yes = "i <= j & P i"
+ show ?case
+ proof (cases)
+ assume ?yes
+ hence "all_from_to_int P i j = (P i & all_from_to_int P (i+1) j)"
+ by(simp add: all_from_to_int.simps)
+ also have "... = (P i & (ALL n : {i+1 .. j}. P n))" using `?yes` 1 by simp
+ also have "... = (ALL n : {i .. j}. P n)" (is "?L = ?R")
+ proof
+ assume L: ?L
+ show ?R
+ proof clarify
+ fix n assume n: "n : {i..j}"
+ show "P n"
+ proof cases
+ assume "n = i" thus "P n" using L by simp
+ next
+ assume "n ~= i"
+ hence "i+1 <= n" using n by auto
+ thus "P n" using L n by simp
+ qed
+ qed
+ next
+ assume R: ?R thus ?L using `?yes` 1 by auto
+ qed
+ finally show ?thesis .
+ next
+ assume "~?yes" thus ?thesis by(auto simp add: all_from_to_int.simps)
+ qed
+qed
+
+lemma list_all_iff_all_from_to_int[code_unfold]:
+ "list_all P [i..j] = all_from_to_int P i j"
+by(simp add: all_from_to_int_iff_ball list_all_iff)
+
+lemma list_ex_iff_not_all_from_to_not_int[code_unfold]:
+ "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
+by(simp add: all_from_to_int_iff_ball list_ex_iff)
+
+
end
--- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Aug 27 15:49:45 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Fri Aug 28 13:32:20 2009 +0100
@@ -99,6 +99,35 @@
values 20 "{(n, m). tranclp succ n m}"
*)
+subsection{* IMP *}
+
+types
+ var = nat
+ state = "int list"
+
+datatype com =
+ Skip |
+ Ass var "state => int" |
+ Seq com com |
+ IF "state => bool" com com |
+ While "state => bool" com
+
+inductive exec :: "com => state => state => bool" where
+"exec Skip s s" |
+"exec (Ass x e) s (s[x := e(s)])" |
+"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
+"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
+"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
+"~b s ==> exec (While b c) s s" |
+"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
+
+code_pred exec .
+
+values "{t. exec
+ (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
+ [3,5] t}"
+
+
subsection{* CCS *}
text{* This example formalizes finite CCS processes without communication or
--- a/src/Pure/Concurrent/future.ML Thu Aug 27 15:49:45 2009 +0100
+++ b/src/Pure/Concurrent/future.ML Fri Aug 28 13:32:20 2009 +0100
@@ -237,7 +237,7 @@
val total = length (! workers);
val active = count_active ();
in
- "SCHEDULE: " ^
+ "SCHEDULE " ^ string_of_int (Time.toMilliseconds now) ^ ": " ^
string_of_int ready ^ " ready, " ^
string_of_int pending ^ " pending, " ^
string_of_int running ^ " running; " ^