--- 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
--- 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;
--- 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
--- 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
--- 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
--- 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"
--- 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
-------------------------------
--- 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,
--- 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
--- 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
--- 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 ***
;;
--- 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 \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))"
- apply (simp add: prime_def)
+lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
+ by (induct m) auto
+
+lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> 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 \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> 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 \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
+lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps)
-lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
- by (induct m) auto
-
-lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k"
- by (induct k) auto
-
lemma not_prime_ex_mk:
assumes n: "Suc 0 < n"
shows "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n"
@@ -96,7 +100,55 @@
qed
qed
-lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> prod l = n)"
+lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact (n::nat)"
+proof (induct n rule: nat_induct)
+ case 0
+ then show ?case by simp
+next
+ case (Suc n)
+ from `m \<le> Suc n` show ?case
+ proof (rule le_SucE)
+ assume "m \<le> 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\<Colon>nat:#multiset_of (n # ns). m)"
+ by (simp add: msetprod_Un msetprod_singleton)
+
+abbreviation (input) "primel ps \<equiv> (\<forall>(p::nat)\<in>set ps. prime p)"
+
+lemma prime_primel: "prime n \<Longrightarrow> primel [n]"
+ by simp
+
+lemma split_primel:
+ assumes "primel ms" and "primel ns"
+ shows "\<exists>qs. primel qs \<and> (PROD m\<Colon>nat:#multiset_of qs. m) =
+ (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
+proof -
+ from assms have "primel (ms @ ns)"
+ unfolding set_append ball_Un by iprover
+ moreover from assms have "(PROD m\<Colon>nat:#multiset_of (ms @ ns). m) =
+ (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)"
+ by (simp add: msetprod_Un)
+ ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
+ then show ?thesis ..
+qed
+
+lemma primel_nempty_g_one:
+ assumes "primel ps" and "ps \<noteq> []"
+ shows "Suc 0 < (PROD m\<Colon>nat:#multiset_of ps. m)"
+ using `ps \<noteq> []` `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 \<Longrightarrow> (\<exists>l. primel l \<and> (PROD m\<Colon>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 "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> 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 "\<exists>l. primel l \<and> 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 "\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) = m" by (rule 1)
+ then obtain l1 where primel_l1: "primel l1" and prod_l1_m: "(PROD m\<Colon>nat:#multiset_of l1. m) = m"
by iprover
- from kn and k have "\<exists>l. primel l \<and> 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 "\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) = k" by (rule 1)
+ then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "(PROD m\<Colon>nat:#multiset_of l2. m) = k"
by iprover
from primel_l1 primel_l2
- have "\<exists>l. primel l \<and> prod l = prod l1 * prod l2"
+ have "\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) =
+ (PROD m\<Colon>nat:#multiset_of l1. m) * (PROD m\<Colon>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] \<and> 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 \<Rightarrow> 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 \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd n!"
-proof (induct n)
- case 0
- then show ?case by simp
-next
- case (Suc n)
- from `m \<le> Suc n` show ?case
- proof (rule le_SucE)
- assume "m \<le> 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\<Colon>nat:#multiset_of [n]. m) = n" by (simp add: msetprod_singleton)
+ ultimately have "primel [n] \<and> (PROD m\<Colon>nat:#multiset_of [n]. m) = n" ..
+ then show ?thesis ..
qed
qed
@@ -160,13 +183,14 @@
shows "\<exists>p. prime p \<and> 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\<Colon>nat:#multiset_of l. m)" using factor_exists
by simp iprover
- from prems have "l \<noteq> []"
- by (auto simp add: primel_nempty_g_one)
+ with N have "l \<noteq> []"
+ 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 \<in> 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: "\<exists>p. prime p \<and> n < p"
+lemma Euclid: "\<exists>p::nat. prime p \<and> 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 "\<not> p \<le> n"
proof
assume pn: "p \<le> 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 \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> '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 \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> '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
--- 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 \<times> nat" ("{* (0::nat, 0::nat) *}")
-
definition
"test n u = pigeonhole n (\<lambda>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 \<times> 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
+
--- 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"];
--- 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"];
--- 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
--- 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"];
--- 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
--- 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 @@
"(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
by (rule measure_induct [of length]) iprover
+lemma list_nonempty_induct [consumes 1, case_names single cons]:
+ assumes "xs \<noteq> []"
+ assumes single: "\<And>x. P [x]"
+ assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"
+ shows "P xs"
+using `xs \<noteq> []` 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 \<noteq> []" by simp
+ moreover with Cons.hyps have "P xs" .
+ ultimately show ?thesis by (rule cons)
+ qed
+qed
+
subsubsection {* @{const length} *}
--- 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 *}
--- 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]
--- 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)
--- 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 \<circ> prod_fun f g = f \<circ> fst"
+by (rule ext) auto
+
+lemma snd_comp_prod_fun[simp]: "snd \<circ> prod_fun f g = g \<circ> 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 \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
"apfst f = prod_fun f id"
@@ -1098,6 +1113,66 @@
lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> 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 \<times> B)"
+proof (rule inj_onI)
+ fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
+ assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
+ assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> 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 \<in> A` and `fst y \<in> 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 \<in> B` and `snd y \<in> 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 \<times> '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 "\<exists>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 \<times> B) = A' \<times> B'"
+unfolding image_def
+proof(rule set_ext,rule iffI)
+ fix x :: "'a \<times> 'c"
+ assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = prod_fun f g x}"
+ then obtain y where "y \<in> A \<times> B" and "x = prod_fun f g y" by blast
+ from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
+ moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
+ ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
+ with `x = prod_fun f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
+next
+ fix x :: "'a \<times> 'c"
+ assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
+ from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
+ then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
+ moreover from `image g B = B'` and `snd x \<in> B'`
+ obtain b where "b \<in> 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 \<in> A` and `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
+ ultimately have "\<exists>y \<in> A \<times> B. x = prod_fun f g y" by auto
+ thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = prod_fun f g y}" by auto
+qed
+
lemma swap_inj_on:
"inj_on (\<lambda>(i, j). (j, i)) A"
by (auto intro!: inj_onI)
--- 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;
--- 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";
--- 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 *)
--- 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));
--- 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";
--- 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;
--- 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;
--- 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'))
--- 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;
--- 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";
--- 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 ""
--- 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 = [],
--- 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; }
--- 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