# HG changeset patch # User blanchet # Date 1275658982 -7200 # Node ID f1734f3e91050fe9cb89c192b7e5fa89c0d10160 # Parent 664d3110beb2da56e8ca6b34f03f56e738bd6436# Parent a1807bf72f760299da70bd8d6ff6368bf089b6a4 merged diff -r a1807bf72f76 -r f1734f3e9105 .hgtags --- a/.hgtags Fri Jun 04 15:41:27 2010 +0200 +++ b/.hgtags Fri Jun 04 15:43:02 2010 +0200 @@ -25,3 +25,4 @@ fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005 5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009 6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1 +935c75359742ccfd4abba0c33a440241e6ef2b1e isa2009-2-test0 diff -r a1807bf72f76 -r f1734f3e9105 Admin/CHECKLIST --- a/Admin/CHECKLIST Fri Jun 04 15:41:27 2010 +0200 +++ b/Admin/CHECKLIST Fri Jun 04 15:43:02 2010 +0200 @@ -1,7 +1,7 @@ Checklist for official releases =============================== -- test polyml-5.3.0, polyml-5.2.1, polyml-5.2, polyml-5.1, polyml-5.0; +- test polyml-5.3.0, polyml-5.2.1, polyml-5.2, polyml-5.1, polyml-5.0, smlnj; - test Proof General; diff -r a1807bf72f76 -r f1734f3e9105 Admin/isatest/settings/mac-poly-M4 --- a/Admin/isatest/settings/mac-poly-M4 Fri Jun 04 15:41:27 2010 +0200 +++ b/Admin/isatest/settings/mac-poly-M4 Fri Jun 04 15:43:02 2010 +0200 @@ -4,7 +4,7 @@ ML_SYSTEM="polyml-5.3.0" ML_PLATFORM="x86-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="--mutable 800 --immutable 2000" + ML_OPTIONS="--mutable 800 --immutable 800" ISABELLE_HOME_USER=~/isabelle-mac-poly-M4 diff -r a1807bf72f76 -r f1734f3e9105 Admin/isatest/settings/mac-poly-M8 --- a/Admin/isatest/settings/mac-poly-M8 Fri Jun 04 15:41:27 2010 +0200 +++ b/Admin/isatest/settings/mac-poly-M8 Fri Jun 04 15:43:02 2010 +0200 @@ -4,7 +4,7 @@ ML_SYSTEM="polyml-5.3.0" ML_PLATFORM="x86-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="--mutable 800 --immutable 2000" + ML_OPTIONS="--mutable 800 --immutable 800" ISABELLE_HOME_USER=~/isabelle-mac-poly-M8 diff -r a1807bf72f76 -r f1734f3e9105 Admin/makebin --- a/Admin/makebin Fri Jun 04 15:41:27 2010 +0200 +++ b/Admin/makebin Fri Jun 04 15:43:02 2010 +0200 @@ -87,11 +87,11 @@ cd "$ISABELLE_NAME" perl -pi \ - -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \ + -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \ etc/settings if [ -n "$DO_LIBRARY" ]; then - perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -i true -d pdf -V outline=/proof,/ML":;' \ + perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \ etc/settings fi diff -r a1807bf72f76 -r f1734f3e9105 Admin/update-keywords --- a/Admin/update-keywords Fri Jun 04 15:41:27 2010 +0200 +++ b/Admin/update-keywords Fri Jun 04 15:43:02 2010 +0200 @@ -12,8 +12,7 @@ isabelle keywords \ "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" \ - "$LOG/IOA.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-SMT.gz" \ - "$LOG/HOL-Statespace.gz" + "$LOG/IOA.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" isabelle keywords -k ZF \ "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz" diff -r a1807bf72f76 -r f1734f3e9105 CONTRIBUTORS --- a/CONTRIBUTORS Fri Jun 04 15:41:27 2010 +0200 +++ b/CONTRIBUTORS Fri Jun 04 15:43:02 2010 +0200 @@ -6,6 +6,10 @@ Contributions to Isabelle2009-2 -------------------------------------- +* 2009/2010: Stefan Berghofer, Alexander Krauss, and Andreas Schropp, TUM, + Makarius Wenzel, TUM / LRI + Elimination of type classes from proof terms. + * April 2010: Florian Haftmann, TUM Reorganization of abstract algebra type classes. @@ -17,6 +21,9 @@ * March 2010: Sascha Boehme, TUM Efficient SHA1 library for Poly/ML. +* February 2010: Cezary Kaliszyk and Christian Urban, TUM + Quotient type package for Isabelle/HOL. + Contributions to Isabelle2009-1 ------------------------------- diff -r a1807bf72f76 -r f1734f3e9105 NEWS --- a/NEWS Fri Jun 04 15:41:27 2010 +0200 +++ b/NEWS Fri Jun 04 15:43:02 2010 +0200 @@ -86,10 +86,13 @@ 'hide_fact' replace the former 'hide' KIND command. Minor INCOMPATIBILITY. +* Improved parallelism of proof term normalization: usedir -p2 -q0 is +more efficient than combinations with -q1 or -q2. + *** Pure *** -* Predicates of locales introduces by classes carry a mandatory +* Predicates of locales introduced by classes carry a mandatory "class" prefix. INCOMPATIBILITY. * Command 'code_reflect' allows to incorporate generated ML code into @@ -137,8 +140,15 @@ within a local theory context. Minor INCOMPATIBILITY. * Proof terms: Type substitutions on proof constants now use canonical -order of type variables. Potential INCOMPATIBILITY for tools working -with proof terms. +order of type variables. INCOMPATIBILITY for tools working with proof +terms. + +* New operation Thm.unconstrainT eliminates all sort constraints from +a theorem and proof, introducing explicit OFCLASS-premises. On the +proof term level, this operation is automatically applied at PThm +boundaries, such that closed proofs are always free of sort +constraints. The old (axiomatic) unconstrain operation has been +discontinued. INCOMPATIBILITY for tools working with proof terms. *** HOL *** @@ -548,6 +558,11 @@ values similar to the ML toplevel. The result is compiler dependent and may fall back on "?" in certain situations. +* Diagnostic commands 'ML_val' and 'ML_command' may refer to +antiquotations @{Isar.state} and @{Isar.goal}. This replaces impure +Isar.state() and Isar.goal(), which belong to the old TTY loop and do +not work with the asynchronous Isar document model. + * Sorts.certify_sort and derived "cert" operations for types and terms no longer minimize sorts. Thus certification at the boundary of the inference kernel becomes invariant under addition of class relations, diff -r a1807bf72f76 -r f1734f3e9105 doc-src/IsarImplementation/Thy/Integration.thy --- a/doc-src/IsarImplementation/Thy/Integration.thy Fri Jun 04 15:41:27 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/Integration.thy Fri Jun 04 15:43:02 2010 +0200 @@ -274,7 +274,6 @@ @{index_ML Isar.loop: "unit -> unit"} \\ @{index_ML Isar.state: "unit -> Toplevel.state"} \\ @{index_ML Isar.exn: "unit -> (exn * string) option"} \\ - @{index_ML Isar.context: "unit -> Proof.context"} \\ @{index_ML Isar.goal: "unit -> {context: Proof.context, facts: thm list, goal: thm}"} \\ \end{mldecls} @@ -291,10 +290,6 @@ toplevel state and error condition, respectively. This only works after having dropped out of the Isar toplevel loop. - \item @{ML "Isar.context ()"} produces the proof context from @{ML - "Isar.state ()"}, analogous to @{ML Context.proof_of} - (\secref{sec:generic-context}). - \item @{ML "Isar.goal ()"} produces the full Isar goal state, consisting of proof context, facts that have been indicated for immediate use, and the tactical goal according to diff -r a1807bf72f76 -r f1734f3e9105 doc-src/IsarImplementation/Thy/document/Integration.tex --- a/doc-src/IsarImplementation/Thy/document/Integration.tex Fri Jun 04 15:41:27 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Fri Jun 04 15:43:02 2010 +0200 @@ -335,7 +335,6 @@ \indexdef{}{ML}{Isar.loop}\verb|Isar.loop: unit -> unit| \\ \indexdef{}{ML}{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\ \indexdef{}{ML}{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\ - \indexdef{}{ML}{Isar.context}\verb|Isar.context: unit -> Proof.context| \\ \indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit ->|\isasep\isanewline% \verb| {context: Proof.context, facts: thm list, goal: thm}| \\ \end{mldecls} @@ -352,9 +351,6 @@ toplevel state and error condition, respectively. This only works after having dropped out of the Isar toplevel loop. - \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|, analogous to \verb|Context.proof_of| - (\secref{sec:generic-context}). - \item \verb|Isar.goal ()| produces the full Isar goal state, consisting of proof context, facts that have been indicated for immediate use, and the tactical goal according to diff -r a1807bf72f76 -r f1734f3e9105 etc/isar-keywords.el --- a/etc/isar-keywords.el Fri Jun 04 15:41:27 2010 +0200 +++ b/etc/isar-keywords.el Fri Jun 04 15:43:02 2010 +0200 @@ -1,6 +1,6 @@ ;; ;; Keyword classification tables for Isabelle/Isar. -;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Boogie + HOL-Nominal + HOL-SMT + HOL-Statespace. +;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Boogie + HOL-Nominal + HOL-Statespace. ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** ;; diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/Extraction/Euclid.thy --- a/src/HOL/Extraction/Euclid.thy Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/Extraction/Euclid.thy Fri Jun 04 15:43:02 2010 +0200 @@ -7,7 +7,7 @@ header {* Euclid's theorem *} theory Euclid -imports "~~/src/HOL/Old_Number_Theory/Factorization" Util Efficient_Nat +imports "~~/src/HOL/Number_Theory/UniqueFactorization" Util Efficient_Nat begin text {* @@ -15,8 +15,18 @@ Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}. *} -lemma prime_eq: "prime p = (1 < p \ (\m. m dvd p \ 1 < m \ m = p))" - apply (simp add: prime_def) +lemma factor_greater_one1: "n = m * k \ m < n \ k < n \ Suc 0 < m" + by (induct m) auto + +lemma factor_greater_one2: "n = m * k \ m < n \ k < n \ Suc 0 < k" + by (induct k) auto + +lemma prod_mn_less_k: + "(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k" + by (induct m) auto + +lemma prime_eq: "prime (p::nat) = (1 < p \ (\m. m dvd p \ 1 < m \ m = p))" + apply (simp add: prime_nat_def) apply (rule iffI) apply blast apply (erule conjE) @@ -33,15 +43,9 @@ apply simp done -lemma prime_eq': "prime p = (1 < p \ (\m k. p = m * k \ 1 < m \ m = p))" +lemma prime_eq': "prime (p::nat) = (1 < p \ (\m k. p = m * k \ 1 < m \ m = p))" by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps) -lemma factor_greater_one1: "n = m * k \ m < n \ k < n \ Suc 0 < m" - by (induct m) auto - -lemma factor_greater_one2: "n = m * k \ m < n \ k < n \ Suc 0 < k" - by (induct k) auto - lemma not_prime_ex_mk: assumes n: "Suc 0 < n" shows "(\m k. Suc 0 < m \ Suc 0 < k \ m < n \ k < n \ n = m * k) \ prime n" @@ -96,7 +100,55 @@ qed qed -lemma factor_exists: "Suc 0 < n \ (\l. primel l \ prod l = n)" +lemma dvd_factorial: "0 < m \ m \ n \ m dvd fact (n::nat)" +proof (induct n rule: nat_induct) + case 0 + then show ?case by simp +next + case (Suc n) + from `m \ Suc n` show ?case + proof (rule le_SucE) + assume "m \ n" + with `0 < m` have "m dvd fact n" by (rule Suc) + then have "m dvd (fact n * Suc n)" by (rule dvd_mult2) + then show ?thesis by (simp add: mult_commute) + next + assume "m = Suc n" + then have "m dvd (fact n * Suc n)" + by (auto intro: dvdI simp: mult_ac) + then show ?thesis by (simp add: mult_commute) + qed +qed + +lemma dvd_prod [iff]: "n dvd (PROD m\nat:#multiset_of (n # ns). m)" + by (simp add: msetprod_Un msetprod_singleton) + +abbreviation (input) "primel ps \ (\(p::nat)\set ps. prime p)" + +lemma prime_primel: "prime n \ primel [n]" + by simp + +lemma split_primel: + assumes "primel ms" and "primel ns" + shows "\qs. primel qs \ (PROD m\nat:#multiset_of qs. m) = + (PROD m\nat:#multiset_of ms. m) * (PROD m\nat:#multiset_of ns. m)" (is "\qs. ?P qs \ ?Q qs") +proof - + from assms have "primel (ms @ ns)" + unfolding set_append ball_Un by iprover + moreover from assms have "(PROD m\nat:#multiset_of (ms @ ns). m) = + (PROD m\nat:#multiset_of ms. m) * (PROD m\nat:#multiset_of ns. m)" + by (simp add: msetprod_Un) + ultimately have "?P (ms @ ns) \ ?Q (ms @ ns)" .. + then show ?thesis .. +qed + +lemma primel_nempty_g_one: + assumes "primel ps" and "ps \ []" + shows "Suc 0 < (PROD m\nat:#multiset_of ps. m)" + using `ps \ []` `primel ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct) + (simp_all add: msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def) + +lemma factor_exists: "Suc 0 < n \ (\l. primel l \ (PROD m\nat:#multiset_of l. m) = n)" proof (induct n rule: nat_wf_ind) case (1 n) from `Suc 0 < n` @@ -107,51 +159,22 @@ assume "\m k. Suc 0 < m \ Suc 0 < k \ m < n \ k < n \ n = m * k" then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n" and kn: "k < n" and nmk: "n = m * k" by iprover - from mn and m have "\l. primel l \ prod l = m" by (rule 1) - then obtain l1 where primel_l1: "primel l1" and prod_l1_m: "prod l1 = m" + from mn and m have "\l. primel l \ (PROD m\nat:#multiset_of l. m) = m" by (rule 1) + then obtain l1 where primel_l1: "primel l1" and prod_l1_m: "(PROD m\nat:#multiset_of l1. m) = m" by iprover - from kn and k have "\l. primel l \ prod l = k" by (rule 1) - then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "prod l2 = k" + from kn and k have "\l. primel l \ (PROD m\nat:#multiset_of l. m) = k" by (rule 1) + then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "(PROD m\nat:#multiset_of l2. m) = k" by iprover from primel_l1 primel_l2 - have "\l. primel l \ prod l = prod l1 * prod l2" + have "\l. primel l \ (PROD m\nat:#multiset_of l. m) = + (PROD m\nat:#multiset_of l1. m) * (PROD m\nat:#multiset_of l2. m)" by (rule split_primel) with prod_l1_m prod_l2_k nmk show ?thesis by simp next - assume "prime n" - hence "primel [n] \ prod [n] = n" by (rule prime_primel) - thus ?thesis .. - qed -qed - -lemma dvd_prod [iff]: "n dvd prod (n # ns)" - by simp - -primrec fact :: "nat \ nat" ("(_!)" [1000] 999) -where - "0! = 1" - | "(Suc n)! = n! * Suc n" - -lemma fact_greater_0 [iff]: "0 < n!" - by (induct n) simp_all - -lemma dvd_factorial: "0 < m \ m \ n \ m dvd n!" -proof (induct n) - case 0 - then show ?case by simp -next - case (Suc n) - from `m \ Suc n` show ?case - proof (rule le_SucE) - assume "m \ n" - with `0 < m` have "m dvd n!" by (rule Suc) - then have "m dvd (n! * Suc n)" by (rule dvd_mult2) - then show ?thesis by simp - next - assume "m = Suc n" - then have "m dvd (n! * Suc n)" - by (auto intro: dvdI simp: mult_ac) - then show ?thesis by simp + assume "prime n" then have "primel [n]" by (rule prime_primel) + moreover have "(PROD m\nat:#multiset_of [n]. m) = n" by (simp add: msetprod_singleton) + ultimately have "primel [n] \ (PROD m\nat:#multiset_of [n]. m) = n" .. + then show ?thesis .. qed qed @@ -160,13 +183,14 @@ shows "\p. prime p \ p dvd n" proof - from N obtain l where primel_l: "primel l" - and prod_l: "n = prod l" using factor_exists + and prod_l: "n = (PROD m\nat:#multiset_of l. m)" using factor_exists by simp iprover - from prems have "l \ []" - by (auto simp add: primel_nempty_g_one) + with N have "l \ []" + by (auto simp add: primel_nempty_g_one msetprod_empty) then obtain x xs where l: "l = x # xs" by (cases l) simp - from primel_l l have "prime x" by (simp add: primel_hd_tl) + then have "x \ set l" by (simp only: insert_def set.simps) (iprover intro: UnI1 CollectI) + with primel_l have "prime x" .. moreover from primel_l l prod_l have "x dvd n" by (simp only: dvd_prod) ultimately show ?thesis by iprover @@ -176,21 +200,21 @@ Euclid's theorem: there are infinitely many primes. *} -lemma Euclid: "\p. prime p \ n < p" +lemma Euclid: "\p::nat. prime p \ n < p" proof - - let ?k = "n! + 1" - have "1 < n! + 1" by simp + let ?k = "fact n + 1" + have "1 < fact n + 1" by simp then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover have "n < p" proof - have "\ p \ n" proof assume pn: "p \ n" - from `prime p` have "0 < p" by (rule prime_g_zero) - then have "p dvd n!" using pn by (rule dvd_factorial) - with dvd have "p dvd ?k - n!" by (rule dvd_diff_nat) + from `prime p` have "0 < p" by (rule prime_gt_0_nat) + then have "p dvd fact n" using pn by (rule dvd_factorial) + with dvd have "p dvd ?k - fact n" by (rule dvd_diff_nat) then have "p dvd 1" by simp - with prime show False using prime_nd_one by auto + with prime show False by auto qed then show ?thesis by simp qed @@ -224,29 +248,27 @@ end +primrec iterate :: "nat \ ('a \ 'a) \ 'a \ 'a list" where + "iterate 0 f x = []" + | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)" + +lemma "factor_exists 1007 = [53, 19]" by eval +lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval +lemma "factor_exists 345 = [23, 5, 3]" by eval +lemma "factor_exists 999 = [37, 3, 3, 3]" by eval +lemma "factor_exists 876 = [73, 3, 2, 2]" by eval + +lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval + consts_code default ("(error \"default\")") lemma "factor_exists 1007 = [53, 19]" by evaluation -lemma "factor_exists 1007 = [53, 19]" by eval - lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by evaluation -lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval - lemma "factor_exists 345 = [23, 5, 3]" by evaluation -lemma "factor_exists 345 = [23, 5, 3]" by eval - lemma "factor_exists 999 = [37, 3, 3, 3]" by evaluation -lemma "factor_exists 999 = [37, 3, 3, 3]" by eval - lemma "factor_exists 876 = [73, 3, 2, 2]" by evaluation -lemma "factor_exists 876 = [73, 3, 2, 2]" by eval - -primrec iterate :: "nat \ ('a \ 'a) \ 'a \ 'a list" where - "iterate 0 f x = []" - | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)" lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by evaluation -lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval end diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/Extraction/Pigeonhole.thy --- a/src/HOL/Extraction/Pigeonhole.thy Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/Extraction/Pigeonhole.thy Fri Jun 04 15:43:02 2010 +0200 @@ -236,10 +236,6 @@ end -consts_code - "default :: nat" ("{* 0::nat *}") - "default :: nat \ nat" ("{* (0::nat, 0::nat) *}") - definition "test n u = pigeonhole n (\m. m - 1)" definition @@ -247,6 +243,19 @@ definition "test'' u = pigeonhole 8 (op ! [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])" +ML "timeit (@{code test} 10)" +ML "timeit (@{code test'} 10)" +ML "timeit (@{code test} 20)" +ML "timeit (@{code test'} 20)" +ML "timeit (@{code test} 25)" +ML "timeit (@{code test'} 25)" +ML "timeit (@{code test} 500)" +ML "timeit @{code test''}" + +consts_code + "default :: nat" ("{* 0::nat *}") + "default :: nat \ nat" ("{* (0::nat, 0::nat) *}") + code_module PH contains test = test @@ -254,27 +263,13 @@ test'' = test'' ML "timeit (PH.test 10)" -ML "timeit (@{code test} 10)" - ML "timeit (PH.test' 10)" -ML "timeit (@{code test'} 10)" - ML "timeit (PH.test 20)" -ML "timeit (@{code test} 20)" - ML "timeit (PH.test' 20)" -ML "timeit (@{code test'} 20)" - ML "timeit (PH.test 25)" -ML "timeit (@{code test} 25)" - ML "timeit (PH.test' 25)" -ML "timeit (@{code test'} 25)" - ML "timeit (PH.test 500)" -ML "timeit (@{code test} 500)" - ML "timeit PH.test''" -ML "timeit @{code test''}" end + diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/Extraction/ROOT.ML --- a/src/HOL/Extraction/ROOT.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/Extraction/ROOT.ML Fri Jun 04 15:43:02 2010 +0200 @@ -1,6 +1,4 @@ (* Examples for program extraction in Higher-Order Logic *) -Proofterm.proofs := 2; - -no_document use_thys ["Efficient_Nat", "~~/src/HOL/Old_Number_Theory/Factorization"]; +no_document use_thys ["Efficient_Nat", "~~/src/HOL/Number_Theory/UniqueFactorization"]; use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"]; diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/Import/ROOT.ML --- a/src/HOL/Import/ROOT.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/Import/ROOT.ML Fri Jun 04 15:43:02 2010 +0200 @@ -1,8 +1,5 @@ (* Title: HOL/Import/ROOT.ML - ID: $Id$ Author: Sebastian Skalberg (TU Muenchen) *) -Proofterm.proofs := 0; -use_thy "HOL4Compat"; -use_thy "HOL4Syntax"; +use_thys ["HOL4Compat", "HOL4Syntax"]; diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/IsaMakefile Fri Jun 04 15:43:02 2010 +0200 @@ -352,6 +352,9 @@ $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES) @$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main +$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES) + @$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs + HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \ Archimedean_Field.thy \ Complex.thy \ @@ -383,9 +386,6 @@ $(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES) @$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL -$(OUT)/HOL-Proofs: ROOT.ML $(HOL_DEPENDENCIES) - @$(ISABELLE_TOOL) usedir -b -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs - ## HOL-Library @@ -506,7 +506,7 @@ HOL-Import: HOL $(LOG)/HOL-Import.gz $(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES) - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Import + @$(ISABELLE_TOOL) usedir -p 0 $(OUT)/HOL Import ## HOL-Generate-HOL @@ -857,7 +857,7 @@ Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy \ Lambda/StrongNorm.thy Lambda/Type.thy Lambda/WeakNorm.thy \ Lambda/ROOT.ML Lambda/document/root.bib Lambda/document/root.tex - @$(ISABELLE_TOOL) usedir -g true -m no_brackets $(OUT)/HOL-Proofs Lambda + @$(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda ## HOL-Prolog @@ -942,7 +942,7 @@ Extraction/Pigeonhole.thy Extraction/QuotRem.thy Extraction/ROOT.ML \ Extraction/Util.thy Extraction/Warshall.thy \ Extraction/document/root.tex Extraction/document/root.bib - @$(ISABELLE_TOOL) usedir $(OUT)/HOL-Proofs Extraction + @$(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction ## HOL-IOA diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/Lambda/ROOT.ML --- a/src/HOL/Lambda/ROOT.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/Lambda/ROOT.ML Fri Jun 04 15:43:02 2010 +0200 @@ -1,5 +1,4 @@ Syntax.ambiguity_level := 100; -Proofterm.proofs := 2; no_document use_thys ["Code_Integer"]; use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"]; diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/Library/Mapping.thy Fri Jun 04 15:43:02 2010 +0200 @@ -287,6 +287,7 @@ by (cases m) simp -hide_const (open) empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload +hide_const (open) empty is_empty lookup update delete ordered_keys keys size + replace default map_entry map_default tabulate bulkload end \ No newline at end of file diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/List.thy --- a/src/HOL/List.thy Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/List.thy Fri Jun 04 15:43:02 2010 +0200 @@ -451,6 +451,23 @@ "(\xs. \ys. length ys < length xs \ P ys \ P xs) \ P xs" by (rule measure_induct [of length]) iprover +lemma list_nonempty_induct [consumes 1, case_names single cons]: + assumes "xs \ []" + assumes single: "\x. P [x]" + assumes cons: "\x xs. xs \ [] \ P xs \ P (x # xs)" + shows "P xs" +using `xs \ []` proof (induct xs) + case Nil then show ?case by simp +next + case (Cons x xs) show ?case proof (cases xs) + case Nil with single show ?thesis by simp + next + case Cons then have "xs \ []" by simp + moreover with Cons.hyps have "P xs" . + ultimately show ?thesis by (rule cons) + qed +qed + subsubsection {* @{const length} *} diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/Number_Theory/Cong.thy --- a/src/HOL/Number_Theory/Cong.thy Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/Number_Theory/Cong.thy Fri Jun 04 15:43:02 2010 +0200 @@ -30,7 +30,7 @@ header {* Congruence *} theory Cong -imports GCD Primes +imports Primes begin subsection {* Turn off One_nat_def *} diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/Number_Theory/Primes.thy --- a/src/HOL/Number_Theory/Primes.thy Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/Number_Theory/Primes.thy Fri Jun 04 15:43:02 2010 +0200 @@ -28,7 +28,7 @@ header {* Primes *} theory Primes -imports GCD +imports "~~/src/HOL/GCD" begin declare One_nat_def [simp del] diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/Number_Theory/UniqueFactorization.thy --- a/src/HOL/Number_Theory/UniqueFactorization.thy Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Fri Jun 04 15:43:02 2010 +0200 @@ -72,6 +72,14 @@ translations "PROD i :# A. b" == "CONST msetprod (%i. b) A" +lemma msetprod_empty: + "msetprod f {#} = 1" + by (simp add: msetprod_def) + +lemma msetprod_singleton: + "msetprod f {#x#} = f x" + by (simp add: msetprod_def) + lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" apply (simp add: msetprod_def power_add) apply (subst setprod_Un2) diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/Product_Type.thy Fri Jun 04 15:43:02 2010 +0200 @@ -856,8 +856,22 @@ lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)" by (simp add: prod_fun_def) -lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)" - by (rule ext) auto +lemma fst_prod_fun[simp]: "fst (prod_fun f g x) = f (fst x)" +by (cases x, auto) + +lemma snd_prod_fun[simp]: "snd (prod_fun f g x) = g (snd x)" +by (cases x, auto) + +lemma fst_comp_prod_fun[simp]: "fst \ prod_fun f g = f \ fst" +by (rule ext) auto + +lemma snd_comp_prod_fun[simp]: "snd \ prod_fun f g = g \ snd" +by (rule ext) auto + + +lemma prod_fun_compose: + "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)" +by (rule ext) auto lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)" by (rule ext) auto @@ -878,6 +892,7 @@ apply blast done + definition apfst :: "('a \ 'c) \ 'a \ 'b \ 'c \ 'b" where "apfst f = prod_fun f id" @@ -1098,6 +1113,66 @@ lemma vimage_Times: "f -` (A \ B) = ((fst \ f) -` A) \ ((snd \ f) -` B)" by (auto, case_tac "f x", auto) +text{* The following @{const prod_fun} lemmas are due to Joachim Breitner: *} + +lemma prod_fun_inj_on: + assumes "inj_on f A" and "inj_on g B" + shows "inj_on (prod_fun f g) (A \ B)" +proof (rule inj_onI) + fix x :: "'a \ 'c" and y :: "'a \ 'c" + assume "x \ A \ B" hence "fst x \ A" and "snd x \ B" by auto + assume "y \ A \ B" hence "fst y \ A" and "snd y \ B" by auto + assume "prod_fun f g x = prod_fun f g y" + hence "fst (prod_fun f g x) = fst (prod_fun f g y)" by (auto) + hence "f (fst x) = f (fst y)" by (cases x,cases y,auto) + with `inj_on f A` and `fst x \ A` and `fst y \ A` + have "fst x = fst y" by (auto dest:dest:inj_onD) + moreover from `prod_fun f g x = prod_fun f g y` + have "snd (prod_fun f g x) = snd (prod_fun f g y)" by (auto) + hence "g (snd x) = g (snd y)" by (cases x,cases y,auto) + with `inj_on g B` and `snd x \ B` and `snd y \ B` + have "snd x = snd y" by (auto dest:dest:inj_onD) + ultimately show "x = y" by(rule prod_eqI) +qed + +lemma prod_fun_surj: + assumes "surj f" and "surj g" + shows "surj (prod_fun f g)" +unfolding surj_def +proof + fix y :: "'b \ 'd" + from `surj f` obtain a where "fst y = f a" by (auto elim:surjE) + moreover + from `surj g` obtain b where "snd y = g b" by (auto elim:surjE) + ultimately have "(fst y, snd y) = prod_fun f g (a,b)" by auto + thus "\x. y = prod_fun f g x" by auto +qed + +lemma prod_fun_surj_on: + assumes "f ` A = A'" and "g ` B = B'" + shows "prod_fun f g ` (A \ B) = A' \ B'" +unfolding image_def +proof(rule set_ext,rule iffI) + fix x :: "'a \ 'c" + assume "x \ {y\'a \ 'c. \x\'b \ 'd\A \ B. y = prod_fun f g x}" + then obtain y where "y \ A \ B" and "x = prod_fun f g y" by blast + from `image f A = A'` and `y \ A \ B` have "f (fst y) \ A'" by auto + moreover from `image g B = B'` and `y \ A \ B` have "g (snd y) \ B'" by auto + ultimately have "(f (fst y), g (snd y)) \ (A' \ B')" by auto + with `x = prod_fun f g y` show "x \ A' \ B'" by (cases y, auto) +next + fix x :: "'a \ 'c" + assume "x \ A' \ B'" hence "fst x \ A'" and "snd x \ B'" by auto + from `image f A = A'` and `fst x \ A'` have "fst x \ image f A" by auto + then obtain a where "a \ A" and "fst x = f a" by (rule imageE) + moreover from `image g B = B'` and `snd x \ B'` + obtain b where "b \ B" and "snd x = g b" by auto + ultimately have "(fst x, snd x) = prod_fun f g (a,b)" by auto + moreover from `a \ A` and `b \ B` have "(a , b) \ A \ B" by auto + ultimately have "\y \ A \ B. x = prod_fun f g y" by auto + thus "x \ {x. \y \ A \ B. x = prod_fun f g y}" by auto +qed + lemma swap_inj_on: "inj_on (\(i, j). (j, i)) A" by (auto intro!: inj_onI) diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Fri Jun 04 15:43:02 2010 +0200 @@ -13,8 +13,6 @@ structure RewriteHOLProof : REWRITE_HOL_PROOF = struct -open Proofterm; - val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT) @@ -311,14 +309,14 @@ | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps) | strip_cong _ _ = NONE; -val subst_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of subst)))); -val sym_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of sym)))); +val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of subst)))); +val sym_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of sym)))); fun make_subst Ts prf xs (_, []) = prf | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) = let val T = fastype_of1 (Ts, x) in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps) - else change_type (SOME [T]) subst_prf %> x %> y %> + else Proofterm.change_type (SOME [T]) subst_prf %> x %> y %> Abs ("z", T, list_comb (incr_boundvars 1 f, map (incr_boundvars 1) xs @ Bound 0 :: map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %% @@ -326,7 +324,8 @@ end; fun make_sym Ts ((x, y), (prf, clprf)) = - ((y, x), (change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf)); + ((y, x), + (Proofterm.change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf)); fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t); @@ -334,15 +333,15 @@ Option.map (make_subst Ts prf2 []) (strip_cong [] prf1) | elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) = Option.map (mk_AbsP P o make_subst Ts (PBound 0) []) - (strip_cong [] (incr_pboundvars 1 0 prf)) + (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf)) | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) = Option.map (make_subst Ts prf2 [] o apsnd (map (make_sym Ts))) (strip_cong [] prf1) | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) = Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o - apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf)) + apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf)) | elim_cong_aux _ _ = NONE; -fun elim_cong Ts hs prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf); +fun elim_cong Ts hs prf = Option.map (rpair Proofterm.no_skel) (elim_cong_aux Ts prf); end; diff -r a1807bf72f76 -r f1734f3e9105 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/HOL/ex/ROOT.ML Fri Jun 04 15:43:02 2010 +0200 @@ -70,7 +70,7 @@ HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese", "Serbian"]; -(setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy)) +(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy)) "Hilbert_Classical"; use_thy "SVC_Oracle"; diff -r a1807bf72f76 -r f1734f3e9105 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Fri Jun 04 15:43:02 2010 +0200 @@ -42,6 +42,8 @@ val disable_pr: Toplevel.transition -> Toplevel.transition val enable_pr: Toplevel.transition -> Toplevel.transition val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition + val diag_state: unit -> Toplevel.state + val diag_goal: unit -> {context: Proof.context, facts: thm list, goal: thm} val cd: Path.T -> Toplevel.transition -> Toplevel.transition val pwd: Toplevel.transition -> Toplevel.transition val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition @@ -299,9 +301,26 @@ (* diagnostic ML evaluation *) +structure Diag_State = Proof_Data +( + type T = Toplevel.state; + fun init _ = Toplevel.toplevel; +); + fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state => - (ML_Context.eval_text_in - (Option.map Context.proof_of (try Toplevel.generic_theory_of state)) verbose pos txt)); + let val opt_ctxt = + try Toplevel.generic_theory_of state + |> Option.map (Context.proof_of #> Diag_State.put state) + in ML_Context.eval_text_in opt_ctxt verbose pos txt end); + +fun diag_state () = Diag_State.get (ML_Context.the_local_context ()); + +fun diag_goal () = + Proof.goal (Toplevel.proof_of (diag_state ())) + handle Toplevel.UNDEF => error "No goal present"; + +val _ = ML_Antiquote.value "Isar.state" (Scan.succeed "Isar_Cmd.diag_state ()"); +val _ = ML_Antiquote.value "Isar.goal" (Scan.succeed "Isar_Cmd.diag_goal ()"); (* current working directory *) diff -r a1807bf72f76 -r f1734f3e9105 src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/Pure/ML/ml_antiquote.ML Fri Jun 04 15:43:02 2010 +0200 @@ -46,7 +46,7 @@ fun declaration kind name scan = ML_Context.add_antiq name (fn _ => scan >> (fn s => fn background => let - val (a, background') = variant name background; + val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background; val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n"; val body = "Isabelle." ^ a; in (K (env, body), background') end)); diff -r a1807bf72f76 -r f1734f3e9105 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/Pure/Proof/extraction.ML Fri Jun 04 15:43:02 2010 +0200 @@ -30,8 +30,6 @@ structure Extraction : EXTRACTION = struct -open Proofterm; - (**** tools ****) fun add_syntax thy = @@ -116,7 +114,7 @@ in rew end; -val chtype = change_type o SOME; +val chtype = Proofterm.change_type o SOME; fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs)); fun corr_name s vs = extr_name s vs ^ "_correctness"; @@ -135,7 +133,7 @@ | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t | strip_abs _ _ = error "strip_abs: not an abstraction"; -val prf_subst_TVars = map_proof_types o typ_subst_TVars; +val prf_subst_TVars = Proofterm.map_proof_types o typ_subst_TVars; fun relevant_vars types prop = List.foldr (fn (Var ((a, _), T), vs) => (case strip_type T of @@ -371,10 +369,10 @@ val xs' = map (map_types typ_map) xs in prf |> - Same.commit (map_proof_same (map_types typ_map) typ_map mk_hyp) |> - fold_rev implies_intr_proof' (map snd constraints) |> - fold_rev forall_intr_proof' xs' |> - fold_rev implies_intr_proof' constraints' + Same.commit (Proofterm.map_proof_same (map_types typ_map) typ_map mk_hyp) |> + fold_rev Proofterm.implies_intr_proof' (map snd constraints) |> + fold_rev Proofterm.forall_intr_proof' xs' |> + fold_rev Proofterm.implies_intr_proof' constraints' end; (** expanding theorems / definitions **) @@ -521,7 +519,7 @@ | corr d defs vs ts Ts hs cs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t = let val (defs', corr_prf) = corr d defs vs [] (T :: Ts) - (dummyt :: hs) cs prf (incr_pboundvars 1 0 prf') + (dummyt :: hs) cs prf (Proofterm.incr_pboundvars 1 0 prf') (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE) in (defs', Abst (s, SOME T, corr_prf)) end @@ -531,13 +529,15 @@ val u = if T = nullT then (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE) else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE); - val (defs', corr_prf) = corr d defs vs [] (T :: Ts) (prop :: hs) - (prop :: cs) (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u; + val (defs', corr_prf) = + corr d defs vs [] (T :: Ts) (prop :: hs) + (prop :: cs) (Proofterm.incr_pboundvars 0 1 prf) + (Proofterm.incr_pboundvars 0 1 prf') u; val rlz = Const ("realizes", T --> propT --> propT) in (defs', if T = nullT then AbsP ("R", SOME (app_rlz_rews Ts vs (rlz $ nullt $ prop)), - prf_subst_bounds [nullt] corr_prf) + Proofterm.prf_subst_bounds [nullt] corr_prf) else Abst (s, SOME T, AbsP ("R", SOME (app_rlz_rews (T :: Ts) vs (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf))) @@ -581,7 +581,7 @@ | corr d defs vs ts Ts hs cs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ = let - val prf = join_proof body; + val prf = Proofterm.join_proof body; val (vs', tye) = find_inst prop Ts ts vs; val shyps = mk_shyps tye; val sprfs = mk_sprfs cs tye; @@ -605,23 +605,26 @@ val corr_prf = mkabsp shyps corr_prf0; val corr_prop = Reconstruct.prop_of corr_prf; val corr_prf' = - proof_combP (proof_combt + Proofterm.proof_combP (Proofterm.proof_combt (PThm (serial (), ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))), - Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop), + Future.value (Proofterm.approximate_proof_body corr_prf))), + vfs_of corr_prop), map PBound (length shyps - 1 downto 0)) |> - fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |> + fold_rev Proofterm.forall_intr_proof' + (map (get_var_type corr_prop) (vfs_of prop)) |> mkabsp shyps in ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'', - proof_combP (prf_subst_TVars tye' corr_prf', sprfs)) + Proofterm.proof_combP (prf_subst_TVars tye' corr_prf', sprfs)) end - | SOME (_, (_, prf')) => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs))) + | SOME (_, (_, prf')) => + (defs', Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs))) | SOME rs => (case find vs' rs of - SOME (_, prf') => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs)) + SOME (_, prf') => (defs', Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs)) | NONE => error ("corr: no realizer for instance of theorem " ^ quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm - (Reconstruct.prop_of (proof_combt (prf0, ts)))))) + (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))) end | corr d defs vs ts Ts hs cs (prf0 as PAxm (s, prop, SOME Ts')) _ _ = @@ -633,10 +636,10 @@ realizes_null vs' prop aconv prop then (defs, prf0) else case find vs' (Symtab.lookup_list realizers s) of SOME (_, prf) => (defs, - proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye)) + Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye)) | NONE => error ("corr: no realizer for instance of axiom " ^ quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm - (Reconstruct.prop_of (proof_combt (prf0, ts))))) + (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))) end | corr d defs vs ts Ts hs _ _ _ _ = error "corr: bad proof" @@ -645,14 +648,14 @@ | extr d defs vs ts Ts hs (Abst (s, SOME T, prf)) = let val (defs', t) = extr d defs vs [] - (T :: Ts) (dummyt :: hs) (incr_pboundvars 1 0 prf) + (T :: Ts) (dummyt :: hs) (Proofterm.incr_pboundvars 1 0 prf) in (defs', Abs (s, T, t)) end | extr d defs vs ts Ts hs (AbsP (s, SOME t, prf)) = let val T = etype_of thy' vs Ts t; - val (defs', t) = extr d defs vs [] (T :: Ts) (t :: hs) - (incr_pboundvars 0 1 prf) + val (defs', t) = + extr d defs vs [] (T :: Ts) (t :: hs) (Proofterm.incr_pboundvars 0 1 prf) in (defs', if T = nullT then subst_bound (nullt, t) else Abs (s, T, t)) end @@ -677,7 +680,7 @@ | extr d defs vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) = let - val prf = join_proof body; + val prf = Proofterm.join_proof body; val (vs', tye) = find_inst prop Ts ts vs; val shyps = mk_shyps tye; val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye @@ -712,20 +715,22 @@ (Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop)); val corr_prf' = mkabsp shyps - (chtype [] equal_elim_axm %> lhs %> rhs %% - (chtype [propT] symmetric_axm %> rhs %> lhs %% - (chtype [T, propT] combination_axm %> f %> f %> c %> t' %% - (chtype [T --> propT] reflexive_axm %> f) %% + (chtype [] Proofterm.equal_elim_axm %> lhs %> rhs %% + (chtype [propT] Proofterm.symmetric_axm %> rhs %> lhs %% + (chtype [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %% + (chtype [T --> propT] Proofterm.reflexive_axm %> f) %% PAxm (cname ^ "_def", eqn, SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf); val corr_prop = Reconstruct.prop_of corr_prf'; val corr_prf'' = - proof_combP (proof_combt + Proofterm.proof_combP (Proofterm.proof_combt (PThm (serial (), ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))), - Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop), + Future.value (Proofterm.approximate_proof_body corr_prf'))), + vfs_of corr_prop), map PBound (length shyps - 1 downto 0)) |> - fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |> + fold_rev Proofterm.forall_intr_proof' + (map (get_var_type corr_prop) (vfs_of prop)) |> mkabsp shyps in ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'', @@ -736,7 +741,7 @@ SOME (t, _) => (defs, subst_TVars tye' t) | NONE => error ("extr: no realizer for instance of theorem " ^ quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm - (Reconstruct.prop_of (proof_combt (prf0, ts)))))) + (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))) end | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) = @@ -748,7 +753,7 @@ SOME (t, _) => (defs, subst_TVars tye' t) | NONE => error ("extr: no realizer for instance of axiom " ^ quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm - (Reconstruct.prop_of (proof_combt (prf0, ts))))) + (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))) end | extr d defs vs ts Ts hs _ = error "extr: bad proof"; diff -r a1807bf72f76 -r f1734f3e9105 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Jun 04 15:43:02 2010 +0200 @@ -22,8 +22,6 @@ structure ProofRewriteRules : PROOF_REWRITE_RULES = struct -open Proofterm; - fun rew b _ _ = let fun ?? x = if b then SOME x else NONE; @@ -33,9 +31,9 @@ let val Type (_, [Type (_, [U, _]), _]) = T in SOME U end else NONE; - val equal_intr_axm = ax equal_intr_axm []; - val equal_elim_axm = ax equal_elim_axm []; - val symmetric_axm = ax symmetric_axm [propT]; + val equal_intr_axm = ax Proofterm.equal_intr_axm []; + val equal_elim_axm = ax Proofterm.equal_elim_axm []; + val symmetric_axm = ax Proofterm.symmetric_axm [propT]; fun rew' (PThm (_, (("Pure.protectD", _, _), _)) % _ %% (PThm (_, (("Pure.protectI", _, _), _)) % _ %% prf)) = SOME prf @@ -71,9 +69,10 @@ val _ $ A $ C = Envir.beta_norm X; val _ $ B $ D = Envir.beta_norm Y in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? B, - equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %% + Proofterm.equal_elim_axm %> C %> D %% Proofterm.incr_pboundvars 2 0 prf2 %% (PBound 1 %% (equal_elim_axm %> B %> A %% - (symmetric_axm % ?? A % ?? B %% incr_pboundvars 2 0 prf1) %% PBound 0))))) + (Proofterm.symmetric_axm % ?? A % ?? B %% Proofterm.incr_pboundvars 2 0 prf1) %% + PBound 0))))) end | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %% @@ -86,8 +85,9 @@ val _ $ B $ D = Envir.beta_norm X in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? A, equal_elim_axm %> D %> C %% - (symmetric_axm % ?? C % ?? D %% incr_pboundvars 2 0 prf2) - %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0))))) + (symmetric_axm % ?? C % ?? D %% Proofterm.incr_pboundvars 2 0 prf2) %% + (PBound 1 %% + (equal_elim_axm %> A %> B %% Proofterm.incr_pboundvars 2 0 prf1 %% PBound 0))))) end | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %% @@ -99,7 +99,7 @@ val _ $ Q = Envir.beta_norm Y; in SOME (AbsP ("H", ?? X, Abst ("x", ty T, equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %% - (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0)))) + (Proofterm.incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0)))) end | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %% @@ -114,7 +114,7 @@ val u = incr_boundvars 1 Q $ Bound 0 in SOME (AbsP ("H", ?? X, Abst ("x", ty T, equal_elim_axm %> t %> u %% - (symmetric_axm % ?? u % ?? t %% (incr_pboundvars 1 1 prf %> Bound 0)) + (symmetric_axm % ?? u % ?? t %% (Proofterm.incr_pboundvars 1 1 prf %> Bound 0)) %% (PBound 0 %> Bound 0)))) end @@ -182,12 +182,12 @@ (PAxm ("Pure.reflexive", _, _) % _)) = let val (U, V) = (case T of Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT)) - in SOME (prf %% (ax combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %% - (ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t))) + in SOME (prf %% (ax Proofterm.combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %% + (ax Proofterm.reflexive_axm [T] % ?? eq) %% (ax Proofterm.reflexive_axm [U] % ?? t))) end | rew' _ = NONE; - in rew' #> Option.map (rpair no_skel) end; + in rew' #> Option.map (rpair Proofterm.no_skel) end; fun rprocs b = [rew b]; val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false))); @@ -231,7 +231,8 @@ (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false) | insert_refl defs Ts (AbsP (s, t, prf)) = (AbsP (s, t, fst (insert_refl defs Ts prf)), false) - | insert_refl defs Ts prf = (case strip_combt prf of + | insert_refl defs Ts prf = + (case Proofterm.strip_combt prf of (PThm (_, ((s, prop, SOME Ts), _)), ts) => if member (op =) defs s then let @@ -242,11 +243,12 @@ (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs), map the ts); in - (change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs', true) + (Proofterm.change_type (SOME [fastype_of1 (Ts, rhs')]) + Proofterm.reflexive_axm %> rhs', true) end else (prf, false) | (_, []) => (prf, false) - | (prf', ts) => (proof_combt' (fst (insert_refl defs Ts prf'), ts), false)); + | (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false)); fun elim_defs thy r defs prf = let @@ -256,7 +258,7 @@ val f = if not r then I else let val cnames = map (fst o dest_Const o fst) defs'; - val thms = fold_proof_atoms true + val thms = Proofterm.fold_proof_atoms true (fn PThm (_, ((name, prop, _), _)) => if member (op =) defnames name orelse not (exists_Const (member (op =) cnames o #1) prop) @@ -291,7 +293,7 @@ | elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T | elim_varst t = t; in - map_proof_terms (fn t => + Proofterm.map_proof_terms (fn t => if Term.exists_subterm hidden_variable t then Envir.beta_norm (elim_varst t) else t) I prf end; @@ -354,16 +356,16 @@ fun reconstruct prf prop = prf |> Reconstruct.reconstruct_proof thy prop |> Reconstruct.expand_proof thy [("", NONE)] |> - Same.commit (map_proof_same Same.same Same.same hyp) + Same.commit (Proofterm.map_proof_same Same.same Same.same hyp) in map2 reconstruct - (of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S)) + (Proofterm.of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S)) (Logic.mk_of_sort (T, S)) end; fun expand_of_class thy Ts hs (OfClass (T, c)) = mk_of_sort_proof thy hs (T, [c]) |> - hd |> rpair no_skel |> SOME + hd |> rpair Proofterm.no_skel |> SOME | expand_of_class thy Ts hs _ = NONE; end; diff -r a1807bf72f76 -r f1734f3e9105 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Fri Jun 04 15:43:02 2010 +0200 @@ -23,8 +23,6 @@ structure Proof_Syntax : PROOF_SYNTAX = struct -open Proofterm; - (**** add special syntax for embedding proof terms ****) val proofT = Type ("proof", []); @@ -98,7 +96,7 @@ fun prf_of [] (Bound i) = PBound i | prf_of Ts (Const (s, Type ("proof", _))) = - change_type (if ty then SOME Ts else NONE) + Proofterm.change_type (if ty then SOME Ts else NONE) (case Long_Name.explode s of "axm" :: xs => let @@ -110,14 +108,15 @@ | "thm" :: xs => let val name = Long_Name.implode xs; in (case AList.lookup (op =) thms name of - SOME thm => fst (strip_combt (fst (strip_combP (Thm.proof_of thm)))) + SOME thm => + fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of thm)))) | NONE => error ("Unknown theorem " ^ quote name)) end | _ => error ("Illegal proof constant name: " ^ quote s)) | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) = (case try Logic.class_of_const c_class of SOME c => - change_type (if ty then SOME Ts else NONE) + Proofterm.change_type (if ty then SOME Ts else NONE) (OfClass (TVar ((Name.aT, 0), []), c)) | NONE => error ("Bad class constant: " ^ quote c_class)) | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop @@ -126,13 +125,13 @@ if T = proofT then error ("Term variable abstraction may not bind proof variable " ^ quote s) else Abst (s, if ty then SOME T else NONE, - incr_pboundvars (~1) 0 (prf_of [] prf)) + Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf)) | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) = AbsP (s, case t of Const ("dummy_pattern", _) => NONE | _ $ Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t), - incr_pboundvars 0 (~1) (prf_of [] prf)) + Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf)) | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) = prf_of [] prf1 %% prf_of [] prf2 | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) = @@ -168,11 +167,11 @@ | term_of Ts (Abst (s, opT, prf)) = let val T = the_default dummyT opT in Const ("Abst", (T --> proofT) --> proofT) $ - Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf)) + Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf)) end | term_of Ts (AbsP (s, t, prf)) = AbsPt $ the_default (Term.dummy_pattern propT) t $ - Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf)) + Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf)) | term_of Ts (prf1 %% prf2) = AppPt $ term_of Ts prf1 $ term_of Ts prf2 | term_of Ts (prf % opt) = @@ -233,10 +232,10 @@ fun proof_syntax prf = let - val thm_names = Symtab.keys (fold_proof_atoms true + val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true (fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I | _ => I) [prf] Symtab.empty); - val axm_names = Symtab.keys (fold_proof_atoms true + val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty); in add_proof_syntax #> @@ -249,8 +248,10 @@ val thy = Thm.theory_of_thm thm; val prop = Thm.full_prop_of thm; val prf = Thm.proof_of thm; - val prf' = (case strip_combt (fst (strip_combP prf)) of - (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then join_proof body else prf + val prf' = + (case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of + (PThm (_, ((_, prop', _), body)), _) => + if prop = prop' then Proofterm.join_proof body else prf | _ => prf) in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end; diff -r a1807bf72f76 -r f1734f3e9105 src/Pure/Proof/proofchecker.ML --- a/src/Pure/Proof/proofchecker.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/Pure/Proof/proofchecker.ML Fri Jun 04 15:43:02 2010 +0200 @@ -13,8 +13,6 @@ structure ProofChecker : PROOF_CHECKER = struct -open Proofterm; - (***** construct a theorem out of a proof term *****) fun lookup_thm thy = @@ -39,8 +37,8 @@ end; fun pretty_prf thy vs Hs prf = - let val prf' = prf |> prf_subst_bounds (map Free vs) |> - prf_subst_pbounds (map (Hyp o prop_of) Hs) + let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |> + Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs) in (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf', Syntax.pretty_term_global thy (Reconstruct.prop_of prf')) diff -r a1807bf72f76 -r f1734f3e9105 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/Pure/Proof/reconstruct.ML Fri Jun 04 15:43:02 2010 +0200 @@ -17,8 +17,6 @@ structure Reconstruct : RECONSTRUCT = struct -open Proofterm; - val quiet_mode = Unsynchronized.ref true; fun message s = if !quiet_mode then () else writeln s; @@ -28,7 +26,7 @@ fun forall_intr_vfs prop = fold_rev Logic.all (vars_of prop @ frees_of prop) prop; -fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' +fun forall_intr_vfs_prf prop prf = fold_rev Proofterm.forall_intr_proof' (vars_of prop @ frees_of prop) prf; @@ -140,9 +138,8 @@ | SOME Ts => (Ts, env)); val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) (forall_intr_vfs prop) handle Library.UnequalLengths => - error ("Wrong number of type arguments for " ^ - quote (get_name [] prop prf)) - in (prop', change_type (SOME Ts) prf, [], env', vTs) end; + error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf)) + in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end; fun head_norm (prop, prf, cnstrts, env, vTs) = (Envir.head_norm env prop, prf, cnstrts, env, vTs); @@ -286,17 +283,17 @@ fun reconstruct_proof thy prop cprf = let - val (cprf' % SOME prop', thawf) = freeze_thaw_prf (cprf % SOME prop); + val (cprf' % SOME prop', thawf) = Proofterm.freeze_thaw_prf (cprf % SOME prop); val _ = message "Collecting constraints..."; val (t, prf, cs, env, _) = make_constraints_cprf thy - (Envir.empty (maxidx_proof cprf ~1)) cprf'; + (Envir.empty (Proofterm.maxidx_proof cprf ~1)) cprf'; val cs' = map (fn p => (true, p, uncurry (union (op =)) (pairself (map (fst o dest_Var) o OldTerm.term_vars) p))) (map (pairself (Envir.norm_term env)) ((t, prop')::cs)); val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ..."); val env' = solve thy cs' env in - thawf (norm_proof env' prf) + thawf (Proofterm.norm_proof env' prf) end; fun prop_of_atom prop Ts = subst_atomic_types @@ -358,24 +355,24 @@ val _ = message ("Reconstructing proof of " ^ a); val _ = message (Syntax.string_of_term_global thy prop); val prf' = forall_intr_vfs_prf prop - (reconstruct_proof thy prop (join_proof body)); + (reconstruct_proof thy prop (Proofterm.join_proof body)); val (maxidx', prfs', prf) = expand - (maxidx_proof prf' ~1) prfs prf' - in (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, + (Proofterm.maxidx_proof prf' ~1) prfs prf' + in (maxidx' + maxidx + 1, Proofterm.incr_indexes (maxidx + 1) prf, ((a, prop), (maxidx', prf)) :: prfs') end | SOME (maxidx', prf) => (maxidx' + maxidx + 1, - incr_indexes (maxidx + 1) prf, prfs)); + Proofterm.incr_indexes (maxidx + 1) prf, prfs)); val tfrees = Term.add_tfrees prop [] |> rev; val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j)) (Term.add_tvars prop [] |> rev) @ map (rpair ~1 o fst) tfrees ~~ Ts; val varify = map_type_tfree (fn p as (a, S) => if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p) in - (maxidx', prfs', map_proof_types (typ_subst_TVars tye o varify) prf) + (maxidx', prfs', Proofterm.map_proof_types (typ_subst_TVars tye o varify) prf) end | expand maxidx prfs prf = (maxidx, prfs, prf); - in #3 (expand (maxidx_proof prf ~1) [] prf) end; + in #3 (expand (Proofterm.maxidx_proof prf ~1) [] prf) end; end; diff -r a1807bf72f76 -r f1734f3e9105 src/Pure/System/isar.ML --- a/src/Pure/System/isar.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/Pure/System/isar.ML Fri Jun 04 15:43:02 2010 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/System/isar.ML Author: Makarius -The global Isabelle/Isar state and main read-eval-print loop. +Global state of the raw Isar read-eval-print loop. *) signature ISAR = @@ -9,7 +9,6 @@ val init: unit -> unit val exn: unit -> (exn * string) option val state: unit -> Toplevel.state - val context: unit -> Proof.context val goal: unit -> {context: Proof.context, facts: thm list, goal: thm} val print: unit -> unit val >> : Toplevel.transition -> bool @@ -57,9 +56,6 @@ fun init () = edit_history 1 (K (K (Toplevel.toplevel, []))); -fun context () = Toplevel.context_of (state ()) - handle Toplevel.UNDEF => error "Unknown context"; - fun goal () = Proof.goal (Toplevel.proof_of (state ())) handle Toplevel.UNDEF => error "No goal present"; diff -r a1807bf72f76 -r f1734f3e9105 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/Pure/proofterm.ML Fri Jun 04 15:43:02 2010 +0200 @@ -136,13 +136,11 @@ val promise_proof: theory -> serial -> term -> proof val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body - val unconstrain_thm_proofs: bool Unsynchronized.ref val thm_proof: theory -> string -> sort list -> term list -> term -> (serial * proof_body future) list -> proof_body -> pthm * proof val unconstrain_thm_proof: theory -> sort list -> term -> (serial * proof_body future) list -> proof_body -> pthm * proof - val get_name: term list -> term -> proof -> string - val get_name_unconstrained: sort list -> term list -> term -> proof -> string + val get_name: sort list -> term list -> term -> proof -> string val guess_name: proof -> string end @@ -1387,10 +1385,12 @@ val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0; in PBody {oracles = oracles, thms = thms, proof = proof} end; -fun fulfill_proof_future _ [] postproc body = Future.value (postproc body) +fun fulfill_proof_future _ [] postproc body = + if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body)) + else Future.map postproc body | fulfill_proof_future thy promises postproc body = - Future.fork_deps (map snd promises) (fn () => - postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) body)); + Future.fork_deps (body :: map snd promises) (fn () => + postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body))); (***** abstraction over sort constraints *****) @@ -1420,7 +1420,7 @@ (***** theorems *****) -fun prepare_thm_proof do_unconstrain thy name shyps hyps concl promises body = +fun prepare_thm_proof thy name shyps hyps concl promises body = let val PBody {oracles = oracles0, thms = thms0, proof = prf} = body; val prop = Logic.list_implies (hyps, concl); @@ -1429,24 +1429,21 @@ if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @ map SOME (frees_of prop); - val (postproc, ofclasses, prop1, args1) = - if do_unconstrain then - let - val ((atyp_map, constraints, outer_constraints), prop1) = - Logic.unconstrainT shyps prop; - val postproc = unconstrainT_body thy (atyp_map, constraints); - val args1 = - (map o Option.map o Term.map_types o Term.map_atyps) - (Type.strip_sorts o atyp_map) args; - in (postproc, map OfClass outer_constraints, prop1, args1) end - else (I, [], prop, args); - val argsP = ofclasses @ map Hyp hyps; + val ((atyp_map, constraints, outer_constraints), prop1) = Logic.unconstrainT shyps prop; + val postproc = unconstrainT_body thy (atyp_map, constraints); + val args1 = + (map o Option.map o Term.map_types o Term.map_atyps) + (Type.strip_sorts o atyp_map) args; + val argsP = map OfClass outer_constraints @ map Hyp hyps; - val proof0 = - if ! proofs = 2 then - #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf))) - else MinProof; - val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0}; + fun full_proof0 () = + #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf))); + + fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0}; + val body0 = + if ! proofs <> 2 then Future.value (make_body0 MinProof) + else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ())) + else Future.fork_pri ~1 (make_body0 o full_proof0); fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0); val (i, body') = @@ -1459,28 +1456,17 @@ val head = PThm (i, ((name, prop1, NONE), body')); in ((i, (name, prop1, body')), head, args, argsP, args1) end; -val unconstrain_thm_proofs = Unsynchronized.ref true; - fun thm_proof thy name shyps hyps concl promises body = - let val (pthm, head, args, argsP, _) = - prepare_thm_proof (! unconstrain_thm_proofs) thy name shyps hyps concl promises body + let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body in (pthm, proof_combP (proof_combt' (head, args), argsP)) end; fun unconstrain_thm_proof thy shyps concl promises body = let - val (pthm, head, _, _, args) = - prepare_thm_proof true thy "" shyps [] concl promises body + val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body in (pthm, proof_combt' (head, args)) end; -fun get_name hyps prop prf = - let val prop = Logic.list_implies (hyps, prop) in - (case strip_combt (fst (strip_combP prf)) of - (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else "" - | _ => "") - end; - -fun get_name_unconstrained shyps hyps prop prf = +fun get_name shyps hyps prop prf = let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in (case strip_combt (fst (strip_combP prf)) of (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else "" diff -r a1807bf72f76 -r f1734f3e9105 src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Jun 04 15:41:27 2010 +0200 +++ b/src/Pure/thm.ML Fri Jun 04 15:43:02 2010 +0200 @@ -156,9 +156,6 @@ structure Thm: THM = struct -structure Pt = Proofterm; - - (*** Certified terms and types ***) (** certified types **) @@ -349,7 +346,7 @@ prop: term} (*conclusion*) and deriv = Deriv of {promises: (serial * thm future) OrdList.T, - body: Pt.proof_body} + body: Proofterm.proof_body} with type conv = cterm -> thm; @@ -486,7 +483,7 @@ fun make_deriv promises oracles thms proof = Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}}; -val empty_deriv = make_deriv [] [] [] Pt.MinProof; +val empty_deriv = make_deriv [] [] [] Proofterm.MinProof; (* inference rules *) @@ -498,10 +495,10 @@ (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) = let val ps = OrdList.union promise_ord ps1 ps2; - val oras = Pt.merge_oracles oras1 oras2; - val thms = Pt.merge_thms thms1 thms2; + val oras = Proofterm.merge_oracles oras1 oras2; + val thms = Proofterm.merge_thms thms1 thms2; val prf = - (case ! Pt.proofs of + (case ! Proofterm.proofs of 2 => f prf1 prf2 | 1 => MinProof | 0 => MinProof @@ -520,14 +517,14 @@ fun raw_body (Thm (Deriv {body, ...}, _)) = body; fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) = - Pt.fulfill_norm_proof (Theory.deref thy_ref) + Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (map #1 promises ~~ fulfill_bodies (map #2 promises)) body and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures)); -val join_proofs = Pt.join_bodies o map fulfill_body; +val join_proofs = Proofterm.join_bodies o map fulfill_body; -fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm); -val proof_of = Pt.proof_of o proof_body_of; +fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm); +val proof_of = Proofterm.proof_of o proof_body_of; (* derivation status *) @@ -537,7 +534,7 @@ val ps = map (Future.peek o snd) promises; val bodies = body :: map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps; - val {oracle, unfinished, failed} = Pt.status_of bodies; + val {oracle, unfinished, failed} = Proofterm.status_of bodies; in {oracle = oracle, unfinished = unfinished orelse exists is_none ps, @@ -571,7 +568,7 @@ val i = serial (); val future = future_thm |> Future.map (future_result i thy sorts prop); in - Thm (make_deriv [(i, future)] [] [] (Pt.promise_proof thy i prop), + Thm (make_deriv [(i, future)] [] [] (Proofterm.promise_proof thy i prop), {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -584,8 +581,8 @@ (* closed derivations with official name *) -fun derivation_name thm = - Pt.guess_name (Pt.proof_of (raw_body thm)); (* FIXME tmp *) +fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = + Proofterm.get_name shyps hyps prop (Proofterm.proof_of body); fun name_derivation name (thm as Thm (der, args)) = let @@ -595,7 +592,7 @@ val ps = map (apsnd (Future.map proof_body_of)) promises; val thy = Theory.deref thy_ref; - val (pthm, proof) = Pt.thm_proof thy name shyps hyps prop ps body; + val (pthm, proof) = Proofterm.thm_proof thy name shyps hyps prop ps body; val der' = make_deriv [] [] [pthm] proof; val _ = Theory.check_thy thy; in Thm (der', args) end; @@ -610,7 +607,7 @@ Symtab.lookup (Theory.axiom_table thy) name |> Option.map (fn prop => let - val der = deriv_rule0 (Pt.axm_proof name prop); + val der = deriv_rule0 (Proofterm.axm_proof name prop); val maxidx = maxidx_of_term prop; val shyps = Sorts.insert_term prop []; in @@ -640,7 +637,7 @@ fun norm_proof (Thm (der, args as {thy_ref, ...})) = let val thy = Theory.deref thy_ref; - val der' = deriv_rule1 (Pt.rew_proof thy) der; + val der' = deriv_rule1 (Proofterm.rew_proof thy) der; val _ = Theory.check_thy thy; in Thm (der', args) end; @@ -666,7 +663,7 @@ raise THM ("assume: prop", 0, []) else if maxidx <> ~1 then raise THM ("assume: variables", maxidx, []) - else Thm (deriv_rule0 (Pt.Hyp prop), + else Thm (deriv_rule0 (Proofterm.Hyp prop), {thy_ref = thy_ref, tags = [], maxidx = ~1, @@ -689,7 +686,7 @@ if T <> propT then raise THM ("implies_intr: assumptions must have type prop", 0, [th]) else - Thm (deriv_rule1 (Pt.implies_intr_proof A) der, + Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der, {thy_ref = merge_thys1 ct th, tags = [], maxidx = Int.max (maxidxA, maxidx), @@ -714,7 +711,7 @@ case prop of Const ("==>", _) $ A $ B => if A aconv propA then - Thm (deriv_rule2 (curry Pt.%%) der derA, + Thm (deriv_rule2 (curry Proofterm.%%) der derA, {thy_ref = merge_thys2 thAB thA, tags = [], maxidx = Int.max (maxA, maxidx), @@ -738,7 +735,7 @@ (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) = let fun result a = - Thm (deriv_rule1 (Pt.forall_intr_proof x a) der, + Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der, {thy_ref = merge_thys1 ct th, tags = [], maxidx = maxidx, @@ -770,7 +767,7 @@ if T <> qary then raise THM ("forall_elim: type mismatch", 0, [th]) else - Thm (deriv_rule1 (Pt.% o rpair (SOME t)) der, + Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der, {thy_ref = merge_thys1 ct th, tags = [], maxidx = Int.max (maxidx, maxt), @@ -787,7 +784,7 @@ t == t *) fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) = - Thm (deriv_rule0 Pt.reflexive, + Thm (deriv_rule0 Proofterm.reflexive, {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -804,7 +801,7 @@ fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = (case prop of (eq as Const ("==", _)) $ t $ u => - Thm (deriv_rule1 Pt.symmetric der, + Thm (deriv_rule1 Proofterm.symmetric der, {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -831,7 +828,7 @@ ((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) => if not (u aconv u') then err "middle term" else - Thm (deriv_rule2 (Pt.transitive u T) der1 der2, + Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2, {thy_ref = merge_thys2 th1 th2, tags = [], maxidx = Int.max (max1, max2), @@ -853,7 +850,7 @@ (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt) | _ => raise THM ("beta_conversion: not a redex", 0, [])); in - Thm (deriv_rule0 Pt.reflexive, + Thm (deriv_rule0 Proofterm.reflexive, {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -864,7 +861,7 @@ end; fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) = - Thm (deriv_rule0 Pt.reflexive, + Thm (deriv_rule0 Proofterm.reflexive, {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -874,7 +871,7 @@ prop = Logic.mk_equals (t, Envir.eta_contract t)}); fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) = - Thm (deriv_rule0 Pt.reflexive, + Thm (deriv_rule0 Proofterm.reflexive, {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -896,7 +893,7 @@ val (t, u) = Logic.dest_equals prop handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]); val result = - Thm (deriv_rule1 (Pt.abstract_rule x a) der, + Thm (deriv_rule1 (Proofterm.abstract_rule x a) der, {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -939,7 +936,7 @@ (Const ("==", Type ("fun", [fT, _])) $ f $ g, Const ("==", Type ("fun", [tT, _])) $ t $ u) => (chktypes fT tT; - Thm (deriv_rule2 (Pt.combination f g t u fT) der1 der2, + Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2, {thy_ref = merge_thys2 th1 th2, tags = [], maxidx = Int.max (max1, max2), @@ -966,7 +963,7 @@ case (prop1, prop2) of (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') => if A aconv A' andalso B aconv B' then - Thm (deriv_rule2 (Pt.equal_intr A B) der1 der2, + Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2, {thy_ref = merge_thys2 th1 th2, tags = [], maxidx = Int.max (max1, max2), @@ -994,7 +991,7 @@ case prop1 of Const ("==", _) $ A $ B => if prop2 aconv A then - Thm (deriv_rule2 (Pt.equal_elim A B) der1 der2, + Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2, {thy_ref = merge_thys2 th1 th2, tags = [], maxidx = Int.max (max1, max2), @@ -1024,7 +1021,7 @@ val tpairs' = tpairs |> map (pairself (Envir.norm_term env)) (*remove trivial tpairs, of the form t==t*) |> filter_out (op aconv); - val der' = deriv_rule1 (Pt.norm_proof' env) der; + val der' = deriv_rule1 (Proofterm.norm_proof' env) der; val prop' = Envir.norm_term env prop; val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'); val shyps = Envir.insert_sorts env shyps; @@ -1064,7 +1061,7 @@ val tpairs' = map (pairself gen) tpairs; val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); in - Thm (deriv_rule1 (Pt.generalize (tfrees, frees) idx) der, + Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der, {thy_ref = thy_ref, tags = [], maxidx = maxidx', @@ -1135,7 +1132,8 @@ val (tpairs', maxidx') = fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1; in - Thm (deriv_rule1 (fn d => Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, + Thm (deriv_rule1 + (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, {thy_ref = thy_ref', tags = [], maxidx = maxidx', @@ -1168,7 +1166,7 @@ if T <> propT then raise THM ("trivial: the term must have type prop", 0, []) else - Thm (deriv_rule0 (Pt.AbsP ("H", NONE, Pt.PBound 0)), + Thm (deriv_rule0 (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)), {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -1190,7 +1188,7 @@ val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c)); in if Sign.of_sort thy (T, [c]) then - Thm (deriv_rule0 (Pt.OfClass (T, c)), + Thm (deriv_rule0 (Proofterm.OfClass (T, c)), {thy_ref = Theory.check_thy thy, tags = [], maxidx = maxidx, @@ -1215,7 +1213,8 @@ |> Sorts.minimal_sorts algebra; val shyps' = fold (Sorts.insert_sort o #2) present extra'; in - Thm (deriv_rule_unconditional (Pt.strip_shyps_proof algebra present witnessed extra') der, + Thm (deriv_rule_unconditional + (Proofterm.strip_shyps_proof algebra present witnessed extra') der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx, shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) end; @@ -1234,7 +1233,8 @@ val ps = map (apsnd (Future.map proof_body_of)) promises; val thy = Theory.deref thy_ref; - val (pthm as (_, (_, prop', _)), proof) = Pt.unconstrain_thm_proof thy shyps prop ps body; + val (pthm as (_, (_, prop', _)), proof) = + Proofterm.unconstrain_thm_proof thy shyps prop ps body; val der' = make_deriv [] [] [pthm] proof; val _ = Theory.check_thy thy; in @@ -1256,7 +1256,7 @@ val (al, prop2) = Type.varify_global tfrees prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in - (al, Thm (deriv_rule1 (Pt.varify_proof prop tfrees) der, + (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der, {thy_ref = thy_ref, tags = [], maxidx = Int.max (0, maxidx), @@ -1275,7 +1275,7 @@ val prop2 = Type.legacy_freeze prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in - Thm (deriv_rule1 (Pt.legacy_freezeT prop1) der, + Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der, {thy_ref = thy_ref, tags = [], maxidx = maxidx_of_term prop2, @@ -1308,7 +1308,7 @@ in if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, []) else - Thm (deriv_rule1 (Pt.lift_proof gprop inc prop) der, + Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der, {thy_ref = merge_thys1 goal orule, tags = [], maxidx = maxidx + inc, @@ -1322,7 +1322,7 @@ if i < 0 then raise THM ("negative increment", 0, [thm]) else if i = 0 then thm else - Thm (deriv_rule1 (Pt.incr_indexes i) der, + Thm (deriv_rule1 (Proofterm.incr_indexes i) der, {thy_ref = thy_ref, tags = [], maxidx = maxidx + i, @@ -1339,8 +1339,8 @@ val (tpairs, Bs, Bi, C) = dest_state (state, i); fun newth n (env, tpairs) = Thm (deriv_rule1 - ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o - Pt.assumption_proof Bs Bi n) der, + ((if Envir.is_empty env then I else (Proofterm.norm_proof' env)) o + Proofterm.assumption_proof Bs Bi n) der, {tags = [], maxidx = Envir.maxidx_of env, shyps = Envir.insert_sorts env shyps, @@ -1377,7 +1377,7 @@ (case find_index (fn asm => Pattern.aeconv (asm, concl)) asms of ~1 => raise THM ("eq_assumption", 0, [state]) | n => - Thm (deriv_rule1 (Pt.assumption_proof Bs Bi (n + 1)) der, + Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der, {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -1406,7 +1406,7 @@ in list_all (params, Logic.list_implies (qs @ ps, concl)) end else raise THM ("rotate_rule", k, [state]); in - Thm (deriv_rule1 (Pt.rotate_proof Bs Bi m) der, + Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der, {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -1437,7 +1437,7 @@ in Logic.list_implies (fixed_prems @ qs @ ps, concl) end else raise THM ("permute_prems: k", k, [rl]); in - Thm (deriv_rule1 (Pt.permute_prems_proof prems j m) der, + Thm (deriv_rule1 (Proofterm.permute_prems_proof prems j m) der, {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -1605,10 +1605,10 @@ Thm (deriv_rule2 ((if Envir.is_empty env then I else if Envir.above env smax then - (fn f => fn der => f (Pt.norm_proof' env der)) + (fn f => fn der => f (Proofterm.norm_proof' env der)) else - curry op oo (Pt.norm_proof' env)) - (Pt.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder, + curry op oo (Proofterm.norm_proof' env)) + (Proofterm.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder, {tags = [], maxidx = Envir.maxidx_of env, shyps = Envir.insert_sorts env (Sorts.union rshyps sshyps), @@ -1624,7 +1624,7 @@ let val (As1, rder') = if not lifted then (As0, rder) else (map (rename_bvars(dpairs,tpairs,B)) As0, - deriv_rule1 (Pt.map_proof_terms + deriv_rule1 (Proofterm.map_proof_terms (rename_bvars (dpairs, tpairs, Bound 0)) I) rder); in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n) handle TERM _ => @@ -1711,7 +1711,7 @@ if T <> propT then raise THM ("Oracle's result must have type prop: " ^ name, 0, []) else - let val (ora, prf) = Pt.oracle_proof name prop in + let val (ora, prf) = Proofterm.oracle_proof name prop in Thm (make_deriv [] [ora] [] prf, {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2), tags = [], diff -r a1807bf72f76 -r f1734f3e9105 src/Tools/jEdit/dist-template/etc/isabelle-jedit.css --- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css Fri Jun 04 15:41:27 2010 +0200 +++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css Fri Jun 04 15:43:02 2010 +0200 @@ -3,7 +3,7 @@ .message { margin-top: 0.3ex; background-color: #F0F0F0; } .writeln { } -.tracing { background-color: #EAF8FF; } +.tracing { background-color: #F0F8FF; } .warning { background-color: #EEE8AA; } .error { background-color: #FFC1C1; } .debug { background-color: #FFE4E1; } diff -r a1807bf72f76 -r f1734f3e9105 src/Tools/jEdit/dist-template/properties/jedit.props --- a/src/Tools/jEdit/dist-template/properties/jedit.props Fri Jun 04 15:41:27 2010 +0200 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Fri Jun 04 15:43:02 2010 +0200 @@ -181,7 +181,7 @@ insert-newline-indent.shortcut= insert-newline.shortcut=ENTER isabelle-output.dock-position=bottom -isabelle-protocol.dock-position=bottom +isabelle-raw-output.dock-position=bottom isabelle.activate.shortcut=CS+ENTER line-end.shortcut=END line-home.shortcut=HOME