# HG changeset patch # User paulson # Date 1251462740 -3600 # Node ID 22b463e232a3ef274620b505cc30718aeae146f7 # Parent 0a94e1f264ce6b2d8a20a52bedfbe87d2d000456# Parent 569e8d6729a119e8cf6e0ab11003de8beee0c110 merged diff -r 569e8d6729a1 -r 22b463e232a3 Admin/isatest/isatest-makeall --- 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="" ;; diff -r 569e8d6729a1 -r 22b463e232a3 Admin/isatest/isatest-makedist --- 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 diff -r 569e8d6729a1 -r 22b463e232a3 Admin/isatest/isatest-stats --- 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 \ diff -r 569e8d6729a1 -r 22b463e232a3 NEWS --- 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 diff -r 569e8d6729a1 -r 22b463e232a3 etc/settings --- 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 diff -r 569e8d6729a1 -r 22b463e232a3 src/HOL/List.thy --- 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"\i\{a..b::int}"} and @{text"\n:{a.."}. *} + +function all_from_to_nat :: "(nat \ bool) \ nat \ nat \ 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.. bool) \ int \ int \ 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 diff -r 569e8d6729a1 -r 22b463e232a3 src/HOL/ex/Predicate_Compile_ex.thy --- 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 diff -r 569e8d6729a1 -r 22b463e232a3 src/Pure/Concurrent/future.ML --- 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; " ^