--- a/NEWS Fri Mar 26 23:58:27 2010 +0100
+++ b/NEWS Sat Mar 27 00:08:39 2010 +0100
@@ -61,6 +61,15 @@
* Use of cumulative prems via "!" in some proof methods has been
discontinued (legacy feature).
+* References 'trace_simp' and 'debug_simp' have been replaced by
+configuration options stored in the context. Enabling tracing
+(the case of debugging is similar) in proofs works via
+
+ using [[trace_simp=true]]
+
+Tracing is then active for all invocations of the simplifier
+in subsequent goal refinement steps.
+
*** Pure ***
--- a/src/HOL/IsaMakefile Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/IsaMakefile Sat Mar 27 00:08:39 2010 +0100
@@ -322,6 +322,7 @@
Tools/Sledgehammer/sledgehammer_hol_clause.ML \
Tools/Sledgehammer/sledgehammer_isar.ML \
Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
+ Tools/Sledgehammer/sledgehammer_util.ML \
Tools/string_code.ML \
Tools/string_syntax.ML \
Tools/transfer.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Mar 27 00:08:39 2010 +0100
@@ -280,7 +280,8 @@
fun get_atp thy args =
let
- fun default_atp_name () = hd (ATP_Manager.get_atps ())
+ fun default_atp_name () =
+ hd (#atps (Sledgehammer_Isar.default_params thy []))
handle Empty => error "No ATP available."
fun get_prover name =
(case ATP_Manager.get_prover thy name of
@@ -302,22 +303,28 @@
fun run_sh prover hard_timeout timeout dir st =
let
val {context = ctxt, facts, goal} = Proof.goal st
+ val thy = ProofContext.theory_of ctxt
val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I)
val ctxt' =
ctxt
|> change_dir dir
|> Config.put ATP_Wrapper.measure_runtime true
- val problem = ATP_Manager.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
-
+ val params = Sledgehammer_Isar.default_params thy []
+ val problem =
+ {subgoal = 1, goal = (ctxt', (facts, goal)),
+ relevance_override = {add = [], del = [], only = false},
+ axiom_clauses = NONE, filtered_clauses = NONE}
val time_limit =
(case hard_timeout of
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
- val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Manager.prover_result,
- time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
+ val ({success, message, relevant_thm_names,
+ atp_run_time_in_msecs = time_atp, ...}: ATP_Manager.prover_result,
+ time_isa) = time_limit (Mirabelle.cpu_time
+ (prover params (Time.fromSeconds timeout))) problem
in
- if success then (message, SH_OK (time_isa, time_atp, theorem_names))
- else (message, SH_FAIL(time_isa, time_atp))
+ if success then (message, SH_OK (time_isa, time_atp, relevant_thm_names))
+ else (message, SH_FAIL (time_isa, time_atp))
end
handle Sledgehammer_HOL_Clause.TRIVIAL => ("trivial", SH_OK (0, 0, []))
| ERROR msg => ("error: " ^ msg, SH_ERROR)
@@ -375,16 +382,19 @@
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
let
open ATP_Minimal
+ open Sledgehammer_Isar
+ val thy = Proof.theory_of st
val n0 = length (these (!named_thms))
- val (prover_name, prover) = get_atp (Proof.theory_of st) args
- val minimize = minimize_theorems linear_minimize prover prover_name
+ val (prover_name, prover) = get_atp thy args
val timeout =
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o explode)
|> the_default 5
+ val params = default_params thy [("minimize_timeout", Int.toString timeout)]
+ val minimize = minimize_theorems params linear_minimize prover prover_name
val _ = log separator
in
- case minimize timeout st (these (!named_thms)) of
+ case minimize st (these (!named_thms)) of
(SOME named_thms', msg) =>
(change_data id inc_min_succs;
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
--- a/src/HOL/Probability/Lebesgue.thy Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Probability/Lebesgue.thy Sat Mar 27 00:08:39 2010 +0100
@@ -1542,31 +1542,6 @@
integral_cong[of "\<lambda>x. f x * indicator_fn (space M) x" f]
by (auto simp add: indicator_fn_def)
-lemma integral_finite_singleton:
- assumes fin: "finite (space M)" and "Pow (space M) = sets M"
- shows "integral f = (\<Sum>x \<in> space M. f x * measure M {x})"
-proof -
- have "f \<in> borel_measurable M"
- unfolding borel_measurable_le_iff
- using assms by auto
- { fix r let ?x = "f -` {r} \<inter> space M"
- have "?x \<subseteq> space M" by auto
- with assms have "measure M ?x = (\<Sum>i \<in> ?x. measure M {i})"
- by (auto intro!: measure_real_sum_image) }
- note measure_eq_setsum = this
- show ?thesis
- unfolding integral_finite[OF `f \<in> borel_measurable M` fin]
- measure_eq_setsum setsum_right_distrib
- apply (subst setsum_Sigma)
- apply (simp add: assms)
- apply (simp add: assms)
- proof (rule setsum_reindex_cong[symmetric])
- fix a assume "a \<in> Sigma (f ` space M) (\<lambda>x. f -` {x} \<inter> space M)"
- thus "(\<lambda>(x, y). x * measure M {y}) a = f (snd a) * measure_space.measure M {snd a}"
- by auto
- qed (auto intro!: image_eqI inj_onI)
-qed
-
section "Radon–Nikodym derivative"
definition
@@ -1574,48 +1549,103 @@
f \<in> borel_measurable M \<and>
(\<forall>a \<in> sets M. (integral (\<lambda>x. f x * indicator_fn a x) = v a))"
-lemma RN_deriv_finite_singleton:
+end
+
+locale finite_measure_space = measure_space +
+ assumes finite_space: "finite (space M)"
+ and sets_eq_Pow: "sets M = Pow (space M)"
+
+lemma sigma_algebra_cong:
+ fixes M :: "('a, 'b) algebra_scheme" and M' :: "('a, 'c) algebra_scheme"
+ assumes *: "sigma_algebra M"
+ and cong: "space M = space M'" "sets M = sets M'"
+ shows "sigma_algebra M'"
+using * unfolding sigma_algebra_def algebra_def sigma_algebra_axioms_def unfolding cong .
+
+lemma finite_Pow_additivity_sufficient:
+ assumes "finite (space M)" and "sets M = Pow (space M)"
+ and "positive M (measure M)" and "additive M (measure M)"
+ shows "finite_measure_space M"
+proof -
+ have "sigma_algebra M"
+ using assms by (auto intro!: sigma_algebra_cong[OF sigma_algebra_Pow])
+
+ have "measure_space M"
+ by (rule Measure.finite_additivity_sufficient) (fact+)
+ thus ?thesis
+ unfolding finite_measure_space_def finite_measure_space_axioms_def
+ using assms by simp
+qed
+
+lemma finite_measure_spaceI:
+ assumes "measure_space M" and "finite (space M)" and "sets M = Pow (space M)"
+ shows "finite_measure_space M"
+ unfolding finite_measure_space_def finite_measure_space_axioms_def
+ using assms by simp
+
+lemma (in finite_measure_space) integral_finite_singleton:
+ "integral f = (\<Sum>x \<in> space M. f x * measure M {x})"
+proof -
+ have "f \<in> borel_measurable M"
+ unfolding borel_measurable_le_iff
+ using sets_eq_Pow by auto
+ { fix r let ?x = "f -` {r} \<inter> space M"
+ have "?x \<subseteq> space M" by auto
+ with finite_space sets_eq_Pow have "measure M ?x = (\<Sum>i \<in> ?x. measure M {i})"
+ by (auto intro!: measure_real_sum_image) }
+ note measure_eq_setsum = this
+ show ?thesis
+ unfolding integral_finite[OF `f \<in> borel_measurable M` finite_space]
+ measure_eq_setsum setsum_right_distrib
+ apply (subst setsum_Sigma)
+ apply (simp add: finite_space)
+ apply (simp add: finite_space)
+ proof (rule setsum_reindex_cong[symmetric])
+ fix a assume "a \<in> Sigma (f ` space M) (\<lambda>x. f -` {x} \<inter> space M)"
+ thus "(\<lambda>(x, y). x * measure M {y}) a = f (snd a) * measure_space.measure M {snd a}"
+ by auto
+ qed (auto intro!: image_eqI inj_onI)
+qed
+
+lemma (in finite_measure_space) RN_deriv_finite_singleton:
fixes v :: "'a set \<Rightarrow> real"
- assumes finite: "finite (space M)" and Pow: "Pow (space M) = sets M"
- and ms_v: "measure_space (M\<lparr>measure := v\<rparr>)"
+ assumes ms_v: "measure_space (M\<lparr>measure := v\<rparr>)"
and eq_0: "\<And>x. measure M {x} = 0 \<Longrightarrow> v {x} = 0"
and "x \<in> space M" and "measure M {x} \<noteq> 0"
shows "RN_deriv v x = v {x} / (measure M {x})" (is "_ = ?v x")
unfolding RN_deriv_def
proof (rule someI2_ex[where Q = "\<lambda>f. f x = ?v x"], rule exI[where x = ?v], safe)
show "(\<lambda>a. v {a} / measure_space.measure M {a}) \<in> borel_measurable M"
- unfolding borel_measurable_le_iff using Pow by auto
+ unfolding borel_measurable_le_iff using sets_eq_Pow by auto
next
fix a assume "a \<in> sets M"
hence "a \<subseteq> space M" and "finite a"
- using sets_into_space finite by (auto intro: finite_subset)
+ using sets_into_space finite_space by (auto intro: finite_subset)
have *: "\<And>x a. (if measure M {x} = 0 then 0 else v {x} * indicator_fn a x) =
v {x} * indicator_fn a x" using eq_0 by auto
from measure_space.measure_real_sum_image[OF ms_v, of a]
- Pow `a \<in> sets M` sets_into_space `finite a`
+ sets_eq_Pow `a \<in> sets M` sets_into_space `finite a`
have "v a = (\<Sum>x\<in>a. v {x})" by auto
thus "integral (\<lambda>x. v {x} / measure_space.measure M {x} * indicator_fn a x) = v a"
- apply (simp add: eq_0 integral_finite_singleton[OF finite Pow])
+ apply (simp add: eq_0 integral_finite_singleton)
apply (unfold divide_1)
- by (simp add: * indicator_fn_def if_distrib setsum_cases finite `a \<subseteq> space M` Int_absorb1)
+ by (simp add: * indicator_fn_def if_distrib setsum_cases finite_space `a \<subseteq> space M` Int_absorb1)
next
fix w assume "w \<in> borel_measurable M"
assume int_eq_v: "\<forall>a\<in>sets M. integral (\<lambda>x. w x * indicator_fn a x) = v a"
- have "{x} \<in> sets M" using Pow `x \<in> space M` by auto
+ have "{x} \<in> sets M" using sets_eq_Pow `x \<in> space M` by auto
have "w x * measure M {x} =
(\<Sum>y\<in>space M. w y * indicator_fn {x} y * measure M {y})"
apply (subst (3) mult_commute)
- unfolding indicator_fn_def if_distrib setsum_cases[OF finite]
+ unfolding indicator_fn_def if_distrib setsum_cases[OF finite_space]
using `x \<in> space M` by simp
also have "... = v {x}"
using int_eq_v[rule_format, OF `{x} \<in> sets M`]
- by (simp add: integral_finite_singleton[OF finite Pow])
+ by (simp add: integral_finite_singleton)
finally show "w x = v {x} / measure M {x}"
using `measure M {x} \<noteq> 0` by (simp add: eq_divide_eq)
qed fact
end
-
-end
--- a/src/HOL/Probability/Measure.thy Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Probability/Measure.thy Sat Mar 27 00:08:39 2010 +0100
@@ -10,7 +10,34 @@
"prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
- by (auto simp add: prod_sets_def)
+ by (auto simp add: prod_sets_def)
+
+lemma sigma_prod_sets_finite:
+ assumes "finite A" and "finite B"
+ shows "sets (sigma (A \<times> B) (prod_sets (Pow A) (Pow B))) = Pow (A \<times> B)"
+proof (simp add: sigma_def, safe)
+ have fin: "finite (A \<times> B)" using assms by (rule finite_cartesian_product)
+
+ fix x assume subset: "x \<subseteq> A \<times> B"
+ hence "finite x" using fin by (rule finite_subset)
+ from this subset show "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))"
+ (is "x \<in> sigma_sets ?prod ?sets")
+ proof (induct x)
+ case empty show ?case by (rule sigma_sets.Empty)
+ next
+ case (insert a x)
+ hence "{a} \<in> sigma_sets ?prod ?sets" by (auto simp: prod_sets_def intro!: sigma_sets.Basic)
+ moreover have "x \<in> sigma_sets ?prod ?sets" using insert by auto
+ ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un)
+ qed
+next
+ fix x a b
+ assume "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))" and "(a, b) \<in> x"
+ from sigma_sets_into_sp[OF _ this(1)] this(2)
+ show "a \<in> A" and "b \<in> B"
+ by (auto simp: prod_sets_def)
+qed
+
definition
closed_cdi where
@@ -26,7 +53,7 @@
smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
for M
where
- Basic [intro]:
+ Basic [intro]:
"a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
| Compl [intro]:
"a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
--- a/src/HOL/Probability/Probability_Space.thy Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Probability/Probability_Space.thy Sat Mar 27 00:08:39 2010 +0100
@@ -350,75 +350,6 @@
assumes "finite (space M) \<and> random_variable borel_space X"
shows "expectation X = (\<Sum> r \<in> X ` (space M). r * distribution X {r})"
using assms unfolding distribution_def using finite_expectation1 by auto
-
-lemma finite_marginal_product_space_POW:
- assumes "Pow (space M) = events"
- assumes "random_variable \<lparr> space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X"
- assumes "random_variable \<lparr> space = Y ` (space M), sets = Pow (Y ` (space M))\<rparr> Y"
- assumes "finite (space M)"
- shows "measure_space \<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))),
- sets = Pow ((X ` (space M)) \<times> (Y ` (space M))),
- measure = (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) -` a \<inter> space M))\<rparr>"
- using assms
-proof -
- let "?S" = "\<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))),
- sets = Pow ((X ` (space M)) \<times> (Y ` (space M)))\<rparr>"
- let "?M" = "\<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))),
- sets = Pow ((X ` (space M)) \<times> (Y ` (space M)))\<rparr>"
- have pos: "positive ?S (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) -` a \<inter> space M))"
- unfolding positive_def using positive'[unfolded positive_def] assms by auto
- { fix x y
- have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms by auto
- have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms by auto
- assume "x \<inter> y = {}"
- from additive[unfolded additive_def, rule_format, OF A B] this
- have "prob (((\<lambda>x. (X x, Y x)) -` x \<union>
- (\<lambda>x. (X x, Y x)) -` y) \<inter> space M) =
- prob ((\<lambda>x. (X x, Y x)) -` x \<inter> space M) +
- prob ((\<lambda>x. (X x, Y x)) -` y \<inter> space M)"
- apply (subst Int_Un_distrib2)
- by auto }
- hence add: "additive ?S (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) -` a \<inter> space M))"
- unfolding additive_def by auto
- interpret S: sigma_algebra "?S"
- unfolding sigma_algebra_def algebra_def
- sigma_algebra_axioms_def by auto
- show ?thesis
- using add pos S.finite_additivity_sufficient assms by auto
-qed
-
-lemma finite_marginal_product_space_POW2:
- assumes "Pow (space M) = events"
- assumes "random_variable \<lparr>space = s1, sets = Pow s1\<rparr> X"
- assumes "random_variable \<lparr>space = s2, sets = Pow s2\<rparr> Y"
- assumes "finite (space M)"
- assumes "finite s1" "finite s2"
- shows "measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>"
-proof -
- let "?S" = "\<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2) \<rparr>"
- let "?M" = "\<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y \<rparr>"
- have pos: "positive ?S (joint_distribution X Y)" using positive'
- unfolding positive_def joint_distribution_def using assms by auto
- { fix x y
- have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms by auto
- have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms by auto
- assume "x \<inter> y = {}"
- from additive[unfolded additive_def, rule_format, OF A B] this
- have "prob (((\<lambda>x. (X x, Y x)) -` x \<union>
- (\<lambda>x. (X x, Y x)) -` y) \<inter> space M) =
- prob ((\<lambda>x. (X x, Y x)) -` x \<inter> space M) +
- prob ((\<lambda>x. (X x, Y x)) -` y \<inter> space M)"
- apply (subst Int_Un_distrib2)
- by auto }
- hence add: "additive ?S (joint_distribution X Y)"
- unfolding additive_def joint_distribution_def by auto
- interpret S: sigma_algebra "?S"
- unfolding sigma_algebra_def algebra_def
- sigma_algebra_axioms_def by auto
- show ?thesis
- using add pos S.finite_additivity_sufficient assms by auto
-qed
-
lemma prob_x_eq_1_imp_prob_y_eq_0:
assumes "{x} \<in> events"
assumes "(prob {x} = 1)"
@@ -453,6 +384,45 @@
ultimately show ?thesis by auto
qed
+
end
+locale finite_prob_space = prob_space + finite_measure_space
+
+lemma (in finite_prob_space) finite_marginal_product_space_POW2:
+ assumes "finite s1" "finite s2"
+ shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>"
+ (is "finite_measure_space ?M")
+proof (rule finite_Pow_additivity_sufficient)
+ show "positive ?M (measure ?M)"
+ unfolding positive_def using positive'[unfolded positive_def] assms sets_eq_Pow
+ by (simp add: joint_distribution_def)
+
+ show "additive ?M (measure ?M)" unfolding additive_def
+ proof safe
+ fix x y
+ have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto
+ have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto
+ assume "x \<inter> y = {}"
+ from additive[unfolded additive_def, rule_format, OF A B] this
+ show "measure ?M (x \<union> y) = measure ?M x + measure ?M y"
+ apply (simp add: joint_distribution_def)
+ apply (subst Int_Un_distrib2)
+ by auto
+ qed
+
+ show "finite (space ?M)"
+ using assms by auto
+
+ show "sets ?M = Pow (space ?M)"
+ by simp
+qed
+
+lemma (in finite_prob_space) finite_marginal_product_space_POW:
+ shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M,
+ sets = Pow (X ` space M \<times> Y ` space M),
+ measure = joint_distribution X Y\<rparr>"
+ (is "finite_measure_space ?M")
+ using finite_space by (auto intro!: finite_marginal_product_space_POW2)
+
end
--- a/src/HOL/Probability/Product_Measure.thy Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Probability/Product_Measure.thy Sat Mar 27 00:08:39 2010 +0100
@@ -32,129 +32,66 @@
by simp
qed
-
-
-lemma measure_space_finite_prod_measure:
- fixes M :: "('a, 'b) measure_space_scheme"
- and M' :: "('c, 'd) measure_space_scheme"
- assumes "measure_space M" and "measure_space M'"
- and finM: "finite (space M)" "Pow (space M) = sets M"
- and finM': "finite (space M')" "Pow (space M') = sets M'"
- shows "measure_space (prod_measure_space M M')"
-proof (rule finite_additivity_sufficient)
- interpret M: measure_space M by fact
- interpret M': measure_space M' by fact
+lemma finite_prod_measure_space:
+ assumes "finite_measure_space M" and "finite_measure_space M'"
+ shows "prod_measure_space M M' =
+ \<lparr> space = space M \<times> space M',
+ sets = Pow (space M \<times> space M'),
+ measure = prod_measure M M' \<rparr>"
+proof -
+ interpret M: finite_measure_space M by fact
+ interpret M': finite_measure_space M' by fact
+ show ?thesis using M.finite_space M'.finite_space
+ by (simp add: sigma_prod_sets_finite M.sets_eq_Pow M'.sets_eq_Pow
+ prod_measure_space_def)
+qed
- have measure: "measure_space.measure (prod_measure_space M M') = prod_measure M M'"
- unfolding prod_measure_space_def by simp
-
- have prod_sets: "prod_sets (sets M) (sets M') \<subseteq> Pow (space M \<times> space M')"
- using M.sets_into_space M'.sets_into_space unfolding prod_sets_def by auto
- show sigma: "sigma_algebra (prod_measure_space M M')" unfolding prod_measure_space_def
- by (rule sigma_algebra_sigma_sets[where a="prod_sets (sets M) (sets M')"])
- (simp_all add: sigma_def prod_sets)
+lemma finite_measure_space_finite_prod_measure:
+ assumes "finite_measure_space M" and "finite_measure_space M'"
+ shows "finite_measure_space (prod_measure_space M M')"
+proof (rule finite_Pow_additivity_sufficient)
+ interpret M: finite_measure_space M by fact
+ interpret M': finite_measure_space M' by fact
- then interpret sa: sigma_algebra "prod_measure_space M M'" .
-
- { fix x y assume "y \<in> sets (prod_measure_space M M')" and "x \<in> space M"
- hence "y \<subseteq> space M \<times> space M'"
- using sa.sets_into_space unfolding prod_measure_space_def by simp
- hence "Pair x -` y \<in> sets M'"
- using `x \<in> space M` unfolding finM'(2)[symmetric] by auto }
- note Pair_in_sets = this
+ from M.finite_space M'.finite_space
+ show "finite (space (prod_measure_space M M'))" and
+ "sets (prod_measure_space M M') = Pow (space (prod_measure_space M M'))"
+ by (simp_all add: finite_prod_measure_space[OF assms])
show "additive (prod_measure_space M M') (measure (prod_measure_space M M'))"
- unfolding measure additive_def
- proof safe
- fix x y assume x: "x \<in> sets (prod_measure_space M M')" and y: "y \<in> sets (prod_measure_space M M')"
+ unfolding additive_def finite_prod_measure_space[OF assms]
+ proof (simp, safe)
+ fix x y assume subs: "x \<subseteq> space M \<times> space M'" "y \<subseteq> space M \<times> space M'"
and disj_x_y: "x \<inter> y = {}"
- { fix z have "Pair z -` x \<inter> Pair z -` y = {}" using disj_x_y by auto }
- note Pair_disj = this
-
- from M'.measure_additive[OF Pair_in_sets[OF x] Pair_in_sets[OF y] Pair_disj, symmetric]
- show "prod_measure M M' (x \<union> y) = prod_measure M M' x + prod_measure M M' y"
- unfolding prod_measure_def
- apply (subst (1 2 3) M.integral_finite_singleton[OF finM])
+ have "\<And>z. measure M' (Pair z -` x \<union> Pair z -` y) =
+ measure M' (Pair z -` x) + measure M' (Pair z -` y)"
+ using disj_x_y subs by (subst M'.measure_additive) (auto simp: M'.sets_eq_Pow)
+ thus "prod_measure M M' (x \<union> y) = prod_measure M M' x + prod_measure M M' y"
+ unfolding prod_measure_def M.integral_finite_singleton
by (simp_all add: setsum_addf[symmetric] field_simps)
qed
- show "finite (space (prod_measure_space M M'))"
- unfolding prod_measure_space_def using finM finM' by simp
-
- have singletonM: "\<And>x. x \<in> space M \<Longrightarrow> {x} \<in> sets M"
- unfolding finM(2)[symmetric] by simp
-
show "positive (prod_measure_space M M') (measure (prod_measure_space M M'))"
unfolding positive_def
- proof (safe, simp add: M.integral_zero prod_measure_space_def prod_measure_def)
- fix Q assume "Q \<in> sets (prod_measure_space M M')"
- from Pair_in_sets[OF this]
- show "0 \<le> measure (prod_measure_space M M') Q"
- unfolding prod_measure_space_def prod_measure_def
- apply (subst M.integral_finite_singleton[OF finM])
- using M.positive M'.positive singletonM
- by (auto intro!: setsum_nonneg mult_nonneg_nonneg)
- qed
+ by (auto intro!: setsum_nonneg mult_nonneg_nonneg M'.positive M.positive
+ simp add: M.integral_zero finite_prod_measure_space[OF assms]
+ prod_measure_def M.integral_finite_singleton
+ M.sets_eq_Pow M'.sets_eq_Pow)
qed
-lemma measure_space_finite_prod_measure_alterantive:
- assumes "measure_space M" and "measure_space M'"
- and finM: "finite (space M)" "Pow (space M) = sets M"
- and finM': "finite (space M')" "Pow (space M') = sets M'"
- shows "measure_space \<lparr> space = space M \<times> space M',
- sets = Pow (space M \<times> space M'),
- measure = prod_measure M M' \<rparr>"
- (is "measure_space ?space")
-proof (rule finite_additivity_sufficient)
- interpret M: measure_space M by fact
- interpret M': measure_space M' by fact
-
- show "sigma_algebra ?space"
- using sigma_algebra.sigma_algebra_extend[where M="\<lparr> space = space M \<times> space M', sets = Pow (space M \<times> space M') \<rparr>"]
- by (auto intro!: sigma_algebra_Pow)
- then interpret sa: sigma_algebra ?space .
-
- have measure: "measure_space.measure (prod_measure_space M M') = prod_measure M M'"
- unfolding prod_measure_space_def by simp
-
- { fix x y assume "y \<in> sets ?space" and "x \<in> space M"
- hence "y \<subseteq> space M \<times> space M'"
- using sa.sets_into_space by simp
- hence "Pair x -` y \<in> sets M'"
- using `x \<in> space M` unfolding finM'(2)[symmetric] by auto }
- note Pair_in_sets = this
+lemma finite_measure_space_finite_prod_measure_alterantive:
+ assumes M: "finite_measure_space M" and M': "finite_measure_space M'"
+ shows "finite_measure_space \<lparr> space = space M \<times> space M', sets = Pow (space M \<times> space M'), measure = prod_measure M M' \<rparr>"
+ (is "finite_measure_space ?M")
+proof -
+ interpret M: finite_measure_space M by fact
+ interpret M': finite_measure_space M' by fact
- show "additive ?space (measure ?space)"
- unfolding measure additive_def
- proof safe
- fix x y assume x: "x \<in> sets ?space" and y: "y \<in> sets ?space"
- and disj_x_y: "x \<inter> y = {}"
- { fix z have "Pair z -` x \<inter> Pair z -` y = {}" using disj_x_y by auto }
- note Pair_disj = this
-
- from M'.measure_additive[OF Pair_in_sets[OF x] Pair_in_sets[OF y] Pair_disj, symmetric]
- show "measure ?space (x \<union> y) = measure ?space x + measure ?space y"
- apply (simp add: prod_measure_def)
- apply (subst (1 2 3) M.integral_finite_singleton[OF finM])
- by (simp_all add: setsum_addf[symmetric] field_simps)
- qed
-
- show "finite (space ?space)" using finM finM' by simp
-
- have singletonM: "\<And>x. x \<in> space M \<Longrightarrow> {x} \<in> sets M"
- unfolding finM(2)[symmetric] by simp
-
- show "positive ?space (measure ?space)"
- unfolding positive_def
- proof (safe, simp add: M.integral_zero prod_measure_def)
- fix Q assume "Q \<in> sets ?space"
- from Pair_in_sets[OF this]
- show "0 \<le> measure ?space Q"
- unfolding prod_measure_space_def prod_measure_def
- apply (subst M.integral_finite_singleton[OF finM])
- using M.positive M'.positive singletonM
- by (auto intro!: setsum_nonneg mult_nonneg_nonneg)
- qed
+ show ?thesis
+ using finite_measure_space_finite_prod_measure[OF assms]
+ unfolding prod_measure_space_def M.sets_eq_Pow M'.sets_eq_Pow
+ using M.finite_space M'.finite_space
+ by (simp add: sigma_prod_sets_finite)
qed
end
\ No newline at end of file
--- a/src/HOL/Sledgehammer.thy Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Sledgehammer.thy Sat Mar 27 00:08:39 2010 +0100
@@ -12,6 +12,7 @@
uses
"Tools/polyhash.ML"
"~~/src/Tools/Metis/metis.ML"
+ "Tools/Sledgehammer/sledgehammer_util.ML"
("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Sat Mar 27 00:08:39 2010 +0100
@@ -1,71 +1,92 @@
(* Title: HOL/Tools/ATP_Manager/atp_manager.ML
Author: Fabian Immler, TU Muenchen
Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
Central manager component for ATP threads.
*)
signature ATP_MANAGER =
sig
+ type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+ type params =
+ {debug: bool,
+ verbose: bool,
+ atps: string list,
+ full_types: bool,
+ relevance_threshold: real,
+ higher_order: bool option,
+ respect_no_atp: bool,
+ follow_defs: bool,
+ isar_proof: bool,
+ timeout: Time.time,
+ minimize_timeout: Time.time}
type problem =
- {with_full_types: bool,
- subgoal: int,
- goal: Proof.context * (thm list * thm),
- axiom_clauses: (thm * (string * int)) list option,
- filtered_clauses: (thm * (string * int)) list option}
- val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
+ {subgoal: int,
+ goal: Proof.context * (thm list * thm),
+ relevance_override: relevance_override,
+ axiom_clauses: (thm * (string * int)) list option,
+ filtered_clauses: (thm * (string * int)) list option}
type prover_result =
- {success: bool,
- message: string,
- theorem_names: string list,
- runtime: int,
- proof: string,
- internal_thm_names: string Vector.vector,
- filtered_clauses: (thm * (string * int)) list}
- type prover = int -> problem -> prover_result
+ {success: bool,
+ message: string,
+ relevant_thm_names: string list,
+ atp_run_time_in_msecs: int,
+ proof: string,
+ internal_thm_names: string Vector.vector,
+ filtered_clauses: (thm * (string * int)) list}
+ type prover = params -> Time.time -> problem -> prover_result
val atps: string Unsynchronized.ref
- val get_atps: unit -> string list
val timeout: int Unsynchronized.ref
val full_types: bool Unsynchronized.ref
- val kill: unit -> unit
- val info: unit -> unit
+ val kill_atps: unit -> unit
+ val running_atps: unit -> unit
val messages: int option -> unit
val add_prover: string * prover -> theory -> theory
val get_prover: theory -> string -> prover option
- val print_provers: theory -> unit
- val sledgehammer: string list -> Proof.state -> unit
+ val available_atps: theory -> unit
+ val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit
end;
structure ATP_Manager : ATP_MANAGER =
struct
-(** problems, results, and provers **)
+type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+
+(** parameters, problems, results, and provers **)
+
+(* TODO: "theory_const", "blacklist_filter", "convergence" *)
+type params =
+ {debug: bool,
+ verbose: bool,
+ atps: string list,
+ full_types: bool,
+ relevance_threshold: real,
+ higher_order: bool option,
+ respect_no_atp: bool,
+ follow_defs: bool,
+ isar_proof: bool,
+ timeout: Time.time,
+ minimize_timeout: Time.time}
type problem =
- {with_full_types: bool,
- subgoal: int,
- goal: Proof.context * (thm list * thm),
- axiom_clauses: (thm * (string * int)) list option,
- filtered_clauses: (thm * (string * int)) list option};
-
-fun problem_of_goal with_full_types subgoal goal : problem =
- {with_full_types = with_full_types,
- subgoal = subgoal,
- goal = goal,
- axiom_clauses = NONE,
- filtered_clauses = NONE};
+ {subgoal: int,
+ goal: Proof.context * (thm list * thm),
+ relevance_override: relevance_override,
+ axiom_clauses: (thm * (string * int)) list option,
+ filtered_clauses: (thm * (string * int)) list option};
type prover_result =
- {success: bool,
- message: string,
- theorem_names: string list, (*relevant theorems*)
- runtime: int, (*user time of the ATP, in milliseconds*)
- proof: string,
- internal_thm_names: string Vector.vector,
- filtered_clauses: (thm * (string * int)) list};
+ {success: bool,
+ message: string,
+ relevant_thm_names: string list,
+ atp_run_time_in_msecs: int,
+ proof: string,
+ internal_thm_names: string Vector.vector,
+ filtered_clauses: (thm * (string * int)) list};
-type prover = int -> problem -> prover_result;
+type prover = params -> Time.time -> problem -> prover_result;
(** preferences **)
@@ -74,8 +95,6 @@
val message_display_limit = 5;
val atps = Unsynchronized.ref "e spass remote_vampire";
-fun get_atps () = String.tokens (Symbol.is_ascii_blank o String.str) (! atps);
-
val timeout = Unsynchronized.ref 60;
val full_types = Unsynchronized.ref false;
@@ -218,9 +237,9 @@
(** user commands **)
-(* kill *)
+(* kill ATPs *)
-fun kill () = Synchronized.change global_state
+fun kill_atps () = Synchronized.change global_state
(fn {manager, timeout_heap, active, cancelling, messages, store} =>
let
val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active;
@@ -228,11 +247,11 @@
in state' end);
-(* info *)
+(* running_atps *)
fun seconds time = string_of_int (Time.toSeconds time) ^ "s";
-fun info () =
+fun running_atps () =
let
val {active, cancelling, ...} = Synchronized.value global_state;
@@ -287,44 +306,51 @@
fun get_prover thy name =
Option.map #1 (Symtab.lookup (Provers.get thy) name);
-fun print_provers thy = Pretty.writeln
- (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
+fun available_atps thy = Pretty.writeln
+ (Pretty.strs ("ATPs:" :: sort_strings (Symtab.keys (Provers.get thy))));
(* start prover thread *)
-fun start_prover name birth_time death_time i proof_state =
+fun start_prover (params as {timeout, ...}) birth_time death_time i
+ relevance_override proof_state name =
(case get_prover (Proof.theory_of proof_state) name of
- NONE => warning ("Unknown external prover: " ^ quote name)
+ NONE => warning ("Unknown ATP: " ^ quote name)
| SOME prover =>
let
val {context = ctxt, facts, goal} = Proof.goal proof_state;
val desc =
- "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
+ "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
val _ = Toplevel.thread true (fn () =>
let
val _ = register birth_time death_time (Thread.self (), desc);
- val problem = problem_of_goal (! full_types) i (ctxt, (facts, goal));
- val message = #message (prover (! timeout) problem)
+ val problem =
+ {subgoal = i, goal = (ctxt, (facts, goal)),
+ relevance_override = relevance_override, axiom_clauses = NONE,
+ filtered_clauses = NONE}
+ val message = #message (prover params timeout problem)
handle Sledgehammer_HOL_Clause.TRIVIAL => (* FIXME !? *)
- "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
+ "Try this command: " ^
+ Markup.markup Markup.sendback "by metis" ^ "."
| ERROR msg => ("Error: " ^ msg);
val _ = unregister message (Thread.self ());
in () end);
in () end);
-(* sledghammer for first subgoal *)
+(* Sledgehammer the given subgoal *)
-fun sledgehammer names proof_state =
+fun sledgehammer (params as {atps, timeout, ...}) i relevance_override
+ proof_state =
let
- val provers = if null names then get_atps () else names;
- val birth_time = Time.now ();
- val death_time = Time.+ (birth_time, Time.fromSeconds (! timeout));
- val _ = kill (); (*RACE wrt. other invocations of sledgehammer*)
- val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers;
- in () end;
+ val birth_time = Time.now ()
+ val death_time = Time.+ (birth_time, timeout)
+ val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
+ val _ = priority "Sledgehammering..."
+ val _ = List.app (start_prover params birth_time death_time i
+ relevance_override proof_state) atps
+ in () end
end;
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Sat Mar 27 00:08:39 2010 +0100
@@ -6,6 +6,7 @@
signature ATP_MINIMAL =
sig
+ type params = ATP_Manager.params
type prover = ATP_Manager.prover
type prover_result = ATP_Manager.prover_result
type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
@@ -13,7 +14,7 @@
val linear_minimize : 'a minimize_fun
val binary_minimize : 'a minimize_fun
val minimize_theorems :
- (string * thm list) minimize_fun -> prover -> string -> int
+ params -> (string * thm list) minimize_fun -> prover -> string
-> Proof.state -> (string * thm list) list
-> (string * thm list) list option * string
end;
@@ -109,8 +110,8 @@
(* wrapper for calling external prover *)
-fun sledgehammer_test_theorems prover time_limit subgoalno state filtered
- name_thms_pairs =
+fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
+ timeout subgoalno state filtered name_thms_pairs =
let
val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
" theorems... ")
@@ -118,26 +119,26 @@
val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
- {with_full_types = ! ATP_Manager.full_types,
- subgoal = subgoalno,
- goal = (ctxt, (facts, goal)),
- axiom_clauses = SOME axclauses,
- filtered_clauses = filtered}
- val (result, proof) = produce_answer (prover time_limit problem)
+ {subgoal = subgoalno, goal = (ctxt, (facts, goal)),
+ relevance_override = {add = [], del = [], only = false},
+ axiom_clauses = SOME axclauses, filtered_clauses = filtered}
+ val (result, proof) = produce_answer (prover params timeout problem)
val _ = priority (string_of_result result)
in (result, proof) end
(* minimalization of thms *)
-fun minimize_theorems gen_min prover prover_name time_limit state
- name_thms_pairs =
+fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover
+ prover_name state name_thms_pairs =
let
+ val msecs = Time.toMilliseconds minimize_timeout
val _ =
priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
- " theorems, prover: " ^ prover_name ^
- ", time limit: " ^ string_of_int time_limit ^ " seconds")
- val test_thms_fun = sledgehammer_test_theorems prover time_limit 1 state
+ " theorems, ATP: " ^ prover_name ^
+ ", time limit: " ^ string_of_int msecs ^ " ms")
+ val test_thms_fun =
+ sledgehammer_test_theorems params prover minimize_timeout 1 state
fun test_thms filtered thms =
case test_thms_fun filtered thms of (Success _, _) => true | _ => false
in
@@ -157,18 +158,22 @@
val _ = priority (cat_lines
["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
in
- (SOME min_thms, "Try this command: " ^
- Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
+ (SOME min_thms,
+ "Try this command: " ^
+ Markup.markup Markup.sendback
+ ("by (metis " ^ space_implode " " min_names ^ ")")
+ ^ ".")
end
| (Timeout, _) =>
(NONE, "Timeout: You may need to increase the time limit of " ^
- string_of_int time_limit ^ " seconds. Call atp_minimize [time=...] ")
+ string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".")
| (Error, msg) =>
(NONE, "Error in prover: " ^ msg)
| (Failure, _) =>
(NONE, "Failure: No proof with the theorems supplied"))
handle Sledgehammer_HOL_Clause.TRIVIAL =>
- (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+ (SOME [], "Trivial: Try this command: " ^
+ Markup.markup Markup.sendback "by metis" ^ ".")
| ERROR msg => (NONE, "Error: " ^ msg)
end
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Sat Mar 27 00:08:39 2010 +0100
@@ -20,6 +20,7 @@
structure ATP_Wrapper : ATP_WRAPPER =
struct
+open Sledgehammer_Fact_Preprocessor
open Sledgehammer_HOL_Clause
open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
@@ -43,11 +44,11 @@
type prover_config =
{command: Path.T,
- arguments: int -> string,
+ arguments: Time.time -> string,
failure_strs: string list,
max_new_clauses: int,
- insert_theory_const: bool,
- emit_structured_proof: bool};
+ add_theory_const: bool,
+ supports_isar_proofs: bool};
(* basic template *)
@@ -64,24 +65,25 @@
else SOME "Ill-formed ATP output"
| (failure :: _) => SOME failure
-fun external_prover relevance_filter prepare write cmd args failure_strs
- produce_answer name ({with_full_types, subgoal, goal, axiom_clauses,
- filtered_clauses}: problem) =
+fun generic_prover get_facts prepare write cmd args failure_strs produce_answer
+ name ({full_types, ...} : params)
+ ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
+ : problem) =
let
(* get clauses and prepare them for writing *)
val (ctxt, (chain_ths, th)) = goal;
val thy = ProofContext.theory_of ctxt;
val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
- val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal);
+ val goal_cls = #1 (neg_conjecture_clauses ctxt th subgoal);
val the_filtered_clauses =
(case filtered_clauses of
- NONE => relevance_filter goal goal_cls
+ NONE => get_facts relevance_override goal goal_cls
| SOME fcls => fcls);
val the_axiom_clauses =
(case axiom_clauses of
NONE => the_filtered_clauses
| SOME axcls => axcls);
- val (thm_names, clauses) =
+ val (internal_thm_names, clauses) =
prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
(* path to unique problem file *)
@@ -121,7 +123,7 @@
if Config.get ctxt measure_runtime then split_time s else (s, 0)
fun run_on probfile =
if File.exists cmd then
- write with_full_types probfile clauses
+ write full_types probfile clauses
|> pair (apfst split_time' (bash_output (cmd_line probfile)))
else error ("Bad executable: " ^ Path.implode cmd);
@@ -131,21 +133,24 @@
if destdir' = "" then ()
else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof;
- val (((proof, time), rc), conj_pos) =
+ val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
with_path cleanup export run_on (prob_pathname subgoal);
(* check for success and print out some information on failure *)
val failure = find_failure failure_strs proof;
val success = rc = 0 andalso is_none failure;
- val (message, real_thm_names) =
+ val (message, relevant_thm_names) =
if is_some failure then ("External prover failed.", [])
else if rc <> 0 then ("External prover failed: " ^ proof, [])
- else apfst (fn s => "Try this command: " ^ s)
- (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoal));
+ else
+ (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
+ subgoal));
in
{success = success, message = message,
- theorem_names = real_thm_names, runtime = time, proof = proof,
- internal_thm_names = thm_names, filtered_clauses = the_filtered_clauses}
+ relevant_thm_names = relevant_thm_names,
+ atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof,
+ internal_thm_names = internal_thm_names,
+ filtered_clauses = the_filtered_clauses}
end;
@@ -153,96 +158,87 @@
fun generic_tptp_prover
(name, {command, arguments, failure_strs, max_new_clauses,
- insert_theory_const, emit_structured_proof}) timeout =
- external_prover (get_relevant_facts max_new_clauses insert_theory_const)
- (prepare_clauses false) write_tptp_file command (arguments timeout)
- failure_strs
- (if emit_structured_proof then structured_isar_proof
- else metis_lemma_list false) name;
+ add_theory_const, supports_isar_proofs})
+ (params as {relevance_threshold, higher_order, follow_defs, isar_proof,
+ ...}) timeout =
+ generic_prover
+ (get_relevant_facts relevance_threshold higher_order follow_defs
+ max_new_clauses add_theory_const)
+ (prepare_clauses higher_order false) write_tptp_file command
+ (arguments timeout) failure_strs
+ (if supports_isar_proofs andalso isar_proof then structured_isar_proof
+ else metis_lemma_list false) name params;
-fun tptp_prover (name, p) = (name, generic_tptp_prover (name, p));
+fun tptp_prover name p = (name, generic_tptp_prover (name, p));
(** common provers **)
(* Vampire *)
-(*NB: Vampire does not work without explicit timelimit*)
-
-val vampire_failure_strs =
- ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
-val vampire_max_new_clauses = 60;
-val vampire_insert_theory_const = false;
+(* NB: Vampire does not work without explicit time limit. *)
-fun vampire_prover_config isar : prover_config =
- {command = Path.explode "$VAMPIRE_HOME/vampire",
- arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
- " -t " ^ string_of_int timeout),
- failure_strs = vampire_failure_strs,
- max_new_clauses = vampire_max_new_clauses,
- insert_theory_const = vampire_insert_theory_const,
- emit_structured_proof = isar};
-
-val vampire = tptp_prover ("vampire", vampire_prover_config false);
-val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
+val vampire_config : prover_config =
+ {command = Path.explode "$VAMPIRE_HOME/vampire",
+ arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^
+ string_of_int (Time.toSeconds timeout)),
+ failure_strs =
+ ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"],
+ max_new_clauses = 60,
+ add_theory_const = false,
+ supports_isar_proofs = true}
+val vampire = tptp_prover "vampire" vampire_config
(* E prover *)
-val eprover_failure_strs =
- ["SZS status: Satisfiable", "SZS status Satisfiable",
- "SZS status: ResourceOut", "SZS status ResourceOut",
- "# Cannot determine problem status"];
-val eprover_max_new_clauses = 100;
-val eprover_insert_theory_const = false;
-
-fun eprover_config isar : prover_config =
- {command = Path.explode "$E_HOME/eproof",
- arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
- " --silent --cpu-limit=" ^ string_of_int timeout),
- failure_strs = eprover_failure_strs,
- max_new_clauses = eprover_max_new_clauses,
- insert_theory_const = eprover_insert_theory_const,
- emit_structured_proof = isar};
-
-val eprover = tptp_prover ("e", eprover_config false);
-val eprover_isar = tptp_prover ("e_isar", eprover_config true);
+val e_config : prover_config =
+ {command = Path.explode "$E_HOME/eproof",
+ arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \
+ \-tAutoDev --silent --cpu-limit=" ^
+ string_of_int (Time.toSeconds timeout)),
+ failure_strs =
+ ["SZS status: Satisfiable", "SZS status Satisfiable",
+ "SZS status: ResourceOut", "SZS status ResourceOut",
+ "# Cannot determine problem status"],
+ max_new_clauses = 100,
+ add_theory_const = false,
+ supports_isar_proofs = true}
+val e = tptp_prover "e" e_config
(* SPASS *)
-val spass_failure_strs =
- ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
- "SPASS beiseite: Maximal number of loops exceeded."];
-val spass_max_new_clauses = 40;
-val spass_insert_theory_const = true;
-
-fun spass_config insert_theory_const: prover_config =
- {command = Path.explode "$SPASS_HOME/SPASS",
- arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
- " -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout),
- failure_strs = spass_failure_strs,
- max_new_clauses = spass_max_new_clauses,
- insert_theory_const = insert_theory_const,
- emit_structured_proof = false};
-
fun generic_dfg_prover
(name, ({command, arguments, failure_strs, max_new_clauses,
- insert_theory_const, ...} : prover_config)) timeout =
- external_prover
- (get_relevant_facts max_new_clauses insert_theory_const)
- (prepare_clauses true)
- write_dfg_file
- command
- (arguments timeout)
- failure_strs
- (metis_lemma_list true)
- name;
+ add_theory_const, ...} : prover_config))
+ (params as {relevance_threshold, higher_order, follow_defs, ...})
+ timeout =
+ generic_prover
+ (get_relevant_facts relevance_threshold higher_order follow_defs
+ max_new_clauses add_theory_const)
+ (prepare_clauses higher_order true) write_dfg_file command
+ (arguments timeout) failure_strs (metis_lemma_list true) name params;
fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
-val spass = dfg_prover ("spass", spass_config spass_insert_theory_const);
-val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false);
+fun spass_config_for add_theory_const : prover_config =
+ {command = Path.explode "$SPASS_HOME/SPASS",
+ arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
+ " -FullRed=0 -DocProof -TimeLimit=" ^
+ string_of_int (Time.toSeconds timeout)),
+ failure_strs =
+ ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
+ "SPASS beiseite: Maximal number of loops exceeded."],
+ max_new_clauses = 40,
+ add_theory_const = add_theory_const,
+ supports_isar_proofs = false};
+
+val spass_config = spass_config_for true
+val spass = dfg_prover ("spass", spass_config)
+
+val spass_no_tc_config = spass_config_for false
+val spass_no_tc = dfg_prover ("spass_no_tc", spass_no_tc_config)
(* remote prover invocation via SystemOnTPTP *)
@@ -251,10 +247,12 @@
fun get_systems () =
let
- val (answer, rc) = bash_output ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
+ val (answer, rc) = bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w"
in
- if rc <> 0 then error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
- else split_lines answer
+ if rc <> 0 then
+ error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
+ else
+ split_lines answer
end;
fun refresh_systems_on_tptp () =
@@ -271,27 +269,34 @@
val remote_failure_strs = ["Remote-script could not extract proof"];
-fun remote_prover_config prover_prefix args max_new insert_tc: prover_config =
- {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
- arguments = (fn timeout =>
- args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
- failure_strs = remote_failure_strs,
- max_new_clauses = max_new,
- insert_theory_const = insert_tc,
- emit_structured_proof = false};
+fun remote_prover_config prover_prefix args max_new_clauses add_theory_const
+ : prover_config =
+ {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
+ arguments = (fn timeout =>
+ args ^ " -t " ^ string_of_int (Time.toSeconds timeout) ^ " -s " ^
+ the_system prover_prefix),
+ failure_strs = remote_failure_strs,
+ max_new_clauses = max_new_clauses,
+ add_theory_const = add_theory_const,
+ supports_isar_proofs = false}
-val remote_vampire = tptp_prover ("remote_vampire", remote_prover_config
- "Vampire---9" "" vampire_max_new_clauses vampire_insert_theory_const);
+val remote_vampire =
+ tptp_prover "remote_vampire"
+ (remote_prover_config "Vampire---9" ""
+ (#max_new_clauses vampire_config) (#add_theory_const vampire_config))
-val remote_eprover = tptp_prover ("remote_e", remote_prover_config
- "EP---" "" eprover_max_new_clauses eprover_insert_theory_const);
+val remote_e =
+ tptp_prover "remote_e"
+ (remote_prover_config "EP---" ""
+ (#max_new_clauses e_config) (#add_theory_const e_config))
-val remote_spass = tptp_prover ("remote_spass", remote_prover_config
- "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
+val remote_spass =
+ tptp_prover "remote_spass"
+ (remote_prover_config "SPASS---" "-x"
+ (#max_new_clauses spass_config) (#add_theory_const spass_config))
val provers =
- [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc,
- remote_vampire, remote_spass, remote_eprover]
+ [spass, vampire, e, spass_no_tc, remote_vampire, remote_spass, remote_e]
val prover_setup = fold add_prover provers
val setup =
--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Mar 27 00:08:39 2010 +0100
@@ -346,7 +346,7 @@
fun monotonicity_message Ts extra =
let val ss = map (quote o string_for_type ctxt) Ts in
"The type" ^ plural_s_for_list ss ^ " " ^
- space_implode " " (serial_commas "and" ss) ^ " " ^
+ space_implode " " (Sledgehammer_Util.serial_commas "and" ss) ^ " " ^
(if none_true monos then
"passed the monotonicity test"
else
@@ -684,7 +684,8 @@
options
in
print ("Try again with " ^
- space_implode " " (serial_commas "and" ss) ^
+ space_implode " "
+ (Sledgehammer_Util.serial_commas "and" ss) ^
" to confirm that the " ^ das_wort_model ^
" is genuine.")
end
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Mar 27 00:08:39 2010 +0100
@@ -24,6 +24,8 @@
open Nitpick_Nut
open Nitpick
+structure K = OuterKeyword and P = OuterParse
+
val auto = Unsynchronized.ref false;
val _ =
@@ -34,48 +36,48 @@
type raw_param = string * string list
val default_default_params =
- [("card", ["1\<midarrow>8"]),
- ("iter", ["0,1,2,4,8,12,16,24"]),
- ("bits", ["1,2,3,4,6,8,10,12"]),
- ("bisim_depth", ["7"]),
- ("box", ["smart"]),
- ("finitize", ["smart"]),
- ("mono", ["smart"]),
- ("std", ["true"]),
- ("wf", ["smart"]),
- ("sat_solver", ["smart"]),
- ("batch_size", ["smart"]),
- ("blocking", ["true"]),
- ("falsify", ["true"]),
- ("user_axioms", ["smart"]),
- ("assms", ["true"]),
- ("merge_type_vars", ["false"]),
- ("binary_ints", ["smart"]),
- ("destroy_constrs", ["true"]),
- ("specialize", ["true"]),
- ("skolemize", ["true"]),
- ("star_linear_preds", ["true"]),
- ("uncurry", ["true"]),
- ("fast_descrs", ["true"]),
- ("peephole_optim", ["true"]),
- ("timeout", ["30 s"]),
- ("tac_timeout", ["500 ms"]),
- ("sym_break", ["20"]),
- ("sharing_depth", ["3"]),
- ("flatten_props", ["false"]),
- ("max_threads", ["0"]),
- ("verbose", ["false"]),
- ("debug", ["false"]),
- ("overlord", ["false"]),
- ("show_all", ["false"]),
- ("show_skolems", ["true"]),
- ("show_datatypes", ["false"]),
- ("show_consts", ["false"]),
- ("format", ["1"]),
- ("max_potential", ["1"]),
- ("max_genuine", ["1"]),
- ("check_potential", ["false"]),
- ("check_genuine", ["false"])]
+ [("card", "1\<midarrow>8"),
+ ("iter", "0,1,2,4,8,12,16,24"),
+ ("bits", "1,2,3,4,6,8,10,12"),
+ ("bisim_depth", "7"),
+ ("box", "smart"),
+ ("finitize", "smart"),
+ ("mono", "smart"),
+ ("std", "true"),
+ ("wf", "smart"),
+ ("sat_solver", "smart"),
+ ("batch_size", "smart"),
+ ("blocking", "true"),
+ ("falsify", "true"),
+ ("user_axioms", "smart"),
+ ("assms", "true"),
+ ("merge_type_vars", "false"),
+ ("binary_ints", "smart"),
+ ("destroy_constrs", "true"),
+ ("specialize", "true"),
+ ("skolemize", "true"),
+ ("star_linear_preds", "true"),
+ ("uncurry", "true"),
+ ("fast_descrs", "true"),
+ ("peephole_optim", "true"),
+ ("timeout", "30 s"),
+ ("tac_timeout", "500 ms"),
+ ("sym_break", "20"),
+ ("sharing_depth", "3"),
+ ("flatten_props", "false"),
+ ("max_threads", "0"),
+ ("debug", "false"),
+ ("verbose", "false"),
+ ("overlord", "false"),
+ ("show_all", "false"),
+ ("show_skolems", "true"),
+ ("show_datatypes", "false"),
+ ("show_consts", "false"),
+ ("format", "1"),
+ ("max_potential", "1"),
+ ("max_genuine", "1"),
+ ("check_potential", "false"),
+ ("check_genuine", "false")]
val negated_params =
[("dont_box", "box"),
@@ -97,8 +99,8 @@
("full_descrs", "fast_descrs"),
("no_peephole_optim", "peephole_optim"),
("dont_flatten_props", "flatten_props"),
+ ("no_debug", "debug"),
("quiet", "verbose"),
- ("no_debug", "debug"),
("no_overlord", "overlord"),
("dont_show_all", "show_all"),
("hide_skolems", "show_skolems"),
@@ -119,7 +121,7 @@
(* string * 'a -> unit *)
fun check_raw_param (s, _) =
if is_known_raw_param s then ()
- else error ("Unknown parameter " ^ quote s ^ ".")
+ else error ("Unknown parameter: " ^ quote s ^ ".")
(* string -> string option *)
fun unnegate_param_name name =
@@ -139,20 +141,15 @@
| NONE => (name, value)
structure Data = Theory_Data(
- type T = {params: raw_param list}
- val empty = {params = rev default_default_params}
+ type T = raw_param list
+ val empty = default_default_params |> map (apsnd single)
val extend = I
- fun merge ({params = ps1}, {params = ps2}) : T =
- {params = AList.merge (op =) (K true) (ps1, ps2)})
+ fun merge p : T = AList.merge (op =) (K true) p)
(* raw_param -> theory -> theory *)
-fun set_default_raw_param param thy =
- let val {params} = Data.get thy in
- Data.put {params = AList.update (op =) (unnegate_raw_param param) params}
- thy
- end
+val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
(* theory -> raw_param list *)
-val default_raw_params = #params o Data.get
+val default_raw_params = Data.get
(* string -> bool *)
fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
@@ -164,26 +161,6 @@
s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
stringify_raw_param_value (s2 :: ss)
-(* bool -> string -> string -> bool option *)
-fun bool_option_from_string option name s =
- (case s of
- "smart" => if option then NONE else raise Option
- | "false" => SOME false
- | "true" => SOME true
- | "" => SOME true
- | _ => raise Option)
- handle Option.Option =>
- let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
- error ("Parameter " ^ quote name ^ " must be assigned " ^
- space_implode " " (serial_commas "or" ss) ^ ".")
- end
-(* bool -> raw_param list -> bool option -> string -> bool option *)
-fun general_lookup_bool option raw_params default_value name =
- case AList.lookup (op =) raw_params name of
- SOME s => s |> stringify_raw_param_value
- |> bool_option_from_string option name
- | NONE => default_value
-
(* int -> string -> int *)
fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
@@ -192,14 +169,19 @@
let
val override_params = map unnegate_raw_param override_params
val raw_params = rev override_params @ rev default_params
+ (* string -> string *)
val lookup =
Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
- (* string -> string *)
- fun lookup_string name = the_default "" (lookup name)
+ val lookup_string = the_default "" o lookup
+ (* bool -> bool option -> string -> bool option *)
+ fun general_lookup_bool option default_value name =
+ case lookup name of
+ SOME s => Sledgehammer_Util.parse_bool_option option name s
+ | NONE => default_value
(* string -> bool *)
- val lookup_bool = the o general_lookup_bool false raw_params (SOME false)
+ val lookup_bool = the o general_lookup_bool false (SOME false)
(* string -> bool option *)
- val lookup_bool_option = general_lookup_bool true raw_params NONE
+ val lookup_bool_option = general_lookup_bool true NONE
(* string -> string option -> int *)
fun do_int name value =
case value of
@@ -253,7 +235,8 @@
:: map (fn (name, value) =>
(SOME (read (String.extract (name, size prefix + 1, NONE))),
value |> stringify_raw_param_value
- |> bool_option_from_string false name |> the))
+ |> Sledgehammer_Util.parse_bool_option false name
+ |> the))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
(* (string -> 'a) -> string -> ('a option * bool option) list *)
fun lookup_bool_option_assigns read prefix =
@@ -261,28 +244,13 @@
:: map (fn (name, value) =>
(SOME (read (String.extract (name, size prefix + 1, NONE))),
value |> stringify_raw_param_value
- |> bool_option_from_string true name))
+ |> Sledgehammer_Util.parse_bool_option true name))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
(* string -> Time.time option *)
fun lookup_time name =
case lookup name of
NONE => NONE
- | SOME "none" => NONE
- | SOME s =>
- let
- val msecs =
- case space_explode " " s of
- [s1, "min"] => 60000 * the (Int.fromString s1)
- | [s1, "s"] => 1000 * the (Int.fromString s1)
- | [s1, "ms"] => the (Int.fromString s1)
- | _ => 0
- in
- if msecs <= 0 then
- error ("Parameter " ^ quote name ^ " must be assigned a positive \
- \time value (e.g., \"60 s\", \"200 ms\") or \"none\".")
- else
- SOME (Time.fromMilliseconds msecs)
- end
+ | SOME s => Sledgehammer_Util.parse_time_option name s
(* string -> term list *)
val lookup_term_list =
AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt
@@ -368,22 +336,18 @@
extract_params (ProofContext.init thy) false (default_raw_params thy)
o map (apsnd single)
-(* OuterParse.token list -> string * OuterParse.token list *)
-val scan_key = Scan.repeat1 OuterParse.typ_group >> space_implode " "
-
-(* OuterParse.token list -> string list * OuterParse.token list *)
-val scan_value =
- Scan.repeat1 (OuterParse.minus >> single
- || Scan.repeat1 (Scan.unless OuterParse.minus OuterParse.name)
- || OuterParse.$$$ "," |-- OuterParse.number >> prefix ","
- >> single) >> flat
-
-(* OuterParse.token list -> raw_param * OuterParse.token list *)
-val scan_param =
- scan_key -- (Scan.option (OuterParse.$$$ "=" |-- scan_value) >> these)
-(* OuterParse.token list -> raw_param list option * OuterParse.token list *)
-val scan_params = Scan.option (OuterParse.$$$ "[" |-- OuterParse.list scan_param
- --| OuterParse.$$$ "]")
+(* P.token list -> string * P.token list *)
+val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
+(* P.token list -> string list * P.token list *)
+val parse_value =
+ Scan.repeat1 (P.minus >> single
+ || Scan.repeat1 (Scan.unless P.minus P.name)
+ || P.$$$ "," |-- P.number >> prefix "," >> single) >> flat
+(* P.token list -> raw_param * P.token list *)
+val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
+(* P.token list -> raw_param list * P.token list *)
+val parse_params =
+ Scan.optional (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") []
(* Proof.context -> ('a -> 'a) -> 'a -> 'a *)
fun handle_exceptions ctxt f x =
@@ -423,7 +387,6 @@
| Refute.REFUTE (loc, details) =>
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
-
(* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *)
fun pick_nits override_params auto i step state =
let
@@ -445,21 +408,20 @@
else (Toplevel.thread true (fn () => (go (); ())); (false, state))
end
-(* raw_param list option * int option -> Toplevel.transition
- -> Toplevel.transition *)
-fun nitpick_trans (opt_params, opt_i) =
+(* raw_param list * int -> Toplevel.transition -> Toplevel.transition *)
+fun nitpick_trans (params, i) =
Toplevel.keep (fn st =>
- (pick_nits (these opt_params) false (the_default 1 opt_i)
- (Toplevel.proof_position_of st) (Toplevel.proof_of st); ()))
+ (pick_nits params false i (Toplevel.proof_position_of st)
+ (Toplevel.proof_of st); ()))
(* raw_param -> string *)
fun string_for_raw_param (name, value) =
name ^ " = " ^ stringify_raw_param_value value
-(* raw_param list option -> Toplevel.transition -> Toplevel.transition *)
-fun nitpick_params_trans opt_params =
+(* raw_param list -> Toplevel.transition -> Toplevel.transition *)
+fun nitpick_params_trans params =
Toplevel.theory
- (fold set_default_raw_param (these opt_params)
+ (fold set_default_raw_param params
#> tap (fn thy =>
writeln ("Default parameters for Nitpick:\n" ^
(case rev (default_raw_params thy) of
@@ -469,18 +431,18 @@
params |> map string_for_raw_param
|> sort_strings |> cat_lines)))))
-(* OuterParse.token list
- -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
-val scan_nitpick_command =
- (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
-val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
+(* P.token list
+ -> (Toplevel.transition -> Toplevel.transition) * P.token list *)
+val parse_nitpick_command =
+ (parse_params -- Scan.optional P.nat 1) #>> nitpick_trans
+val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
val _ = OuterSyntax.improper_command "nitpick"
"try to find a counterexample for a given subgoal using Kodkod"
- OuterKeyword.diag scan_nitpick_command
+ K.diag parse_nitpick_command
val _ = OuterSyntax.command "nitpick_params"
"set and display the default parameters for Nitpick"
- OuterKeyword.thy_decl scan_nitpick_params_command
+ K.thy_decl parse_nitpick_params_command
(* Proof.state -> bool * Proof.state *)
fun auto_nitpick state =
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Sat Mar 27 00:08:39 2010 +0100
@@ -194,8 +194,11 @@
else
[])
in
- if null ss then []
- else serial_commas "and" ss |> map Pretty.str |> Pretty.breaks
+ if null ss then
+ []
+ else
+ Sledgehammer_Util.serial_commas "and" ss
+ |> map Pretty.str |> Pretty.breaks
end
(* scope -> string *)
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Mar 27 00:08:39 2010 +0100
@@ -46,7 +46,6 @@
val triple_lookup :
(''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option
val is_substring_of : string -> string -> bool
- val serial_commas : string -> string list -> string list
val plural_s : int -> string
val plural_s_for_list : 'a list -> string
val flip_polarity : polarity -> polarity
@@ -233,13 +232,6 @@
not (Substring.isEmpty (snd (Substring.position needle
(Substring.full stack))))
-(* string -> string list -> string list *)
-fun serial_commas _ [] = ["??"]
- | serial_commas _ [s] = [s]
- | serial_commas conj [s1, s2] = [s1, conj, s2]
- | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
- | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-
(* int -> string *)
fun plural_s n = if n = 1 then "" else "s"
(* 'a list -> string *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sat Mar 27 00:08:39 2010 +0100
@@ -9,12 +9,19 @@
type axiom_name = Sledgehammer_HOL_Clause.axiom_name
type hol_clause = Sledgehammer_HOL_Clause.hol_clause
type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
+ type relevance_override =
+ {add: Facts.ref list,
+ del: Facts.ref list,
+ only: bool}
+
val tvar_classes_of_terms : term list -> string list
val tfree_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
- val get_relevant_facts : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
- (thm * (string * int)) list
- val prepare_clauses : bool -> thm list -> thm list ->
+ val get_relevant_facts :
+ real -> bool option -> bool -> int -> bool -> relevance_override
+ -> Proof.context * (thm list * 'a) -> thm list
+ -> (thm * (string * int)) list
+ val prepare_clauses : bool option -> bool -> thm list -> thm list ->
(thm * (axiom_name * hol_clause_id)) list ->
(thm * (axiom_name * hol_clause_id)) list -> theory ->
axiom_name vector *
@@ -29,29 +36,21 @@
open Sledgehammer_Fact_Preprocessor
open Sledgehammer_HOL_Clause
-type axiom_name = axiom_name
-type hol_clause = hol_clause
-type hol_clause_id = hol_clause_id
+type relevance_override =
+ {add: Facts.ref list,
+ del: Facts.ref list,
+ only: bool}
(********************************************************************)
(* some settings for both background automatic ATP calling procedure*)
(* and also explicit ATP invocation methods *)
(********************************************************************)
-(* Translation mode can be auto-detected, or forced to be first-order or
- higher-order *)
-datatype mode = Auto | Fol | Hol;
-
-val translation_mode = Auto;
-
(*** background linkup ***)
val run_blacklist_filter = true;
(*** relevance filter parameters ***)
-val run_relevance_filter = true;
-val pass_mark = 0.5;
val convergence = 3.2; (*Higher numbers allow longer inference chains*)
-val follow_defs = false; (*Follow definitions. Makes problems bigger.*)
(***************************************************************)
(* Relevance Filtering *)
@@ -139,8 +138,8 @@
(*Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account.*)
-fun const_prop_of theory_const th =
- if theory_const then
+fun const_prop_of add_theory_const th =
+ if add_theory_const then
let val name = Context.theory_name (theory_of_thm th)
val t = Const (name ^ ". 1", HOLogic.boolT)
in t $ prop_of th end
@@ -169,7 +168,7 @@
structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
-fun count_axiom_consts theory_const thy ((thm,_), tab) =
+fun count_axiom_consts add_theory_const thy ((thm,_), tab) =
let fun count_const (a, T, tab) =
let val (c, cts) = const_with_typ thy (a,T)
in (*Two-dimensional table update. Constant maps to types maps to count.*)
@@ -182,7 +181,7 @@
count_term_consts (t, count_term_consts (u, tab))
| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
| count_term_consts (_, tab) = tab
- in count_term_consts (const_prop_of theory_const thm, tab) end;
+ in count_term_consts (const_prop_of add_theory_const thm, tab) end;
(**** Actual Filtering Code ****)
@@ -214,8 +213,8 @@
let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
in Symtab.fold add_expand_pairs tab [] end;
-fun pair_consts_typs_axiom theory_const thy (thm,name) =
- ((thm,name), (consts_typs_of_term thy (const_prop_of theory_const thm)));
+fun pair_consts_typs_axiom add_theory_const thy (p as (thm, _)) =
+ (p, (consts_typs_of_term thy (const_prop_of add_theory_const thm)));
exception ConstFree;
fun dest_ConstFree (Const aT) = aT
@@ -234,9 +233,10 @@
end
handle ConstFree => false
in
- case tm of @{const Trueprop} $ (Const(@{const_name "op ="}, _) $ lhs $ rhs) =>
- defs lhs rhs
- | _ => false
+ case tm of
+ @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) =>
+ defs lhs rhs
+ | _ => false
end;
type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
@@ -263,8 +263,12 @@
end
end;
-fun relevant_clauses max_new thy ctab p rel_consts =
- let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*)
+fun relevant_clauses ctxt follow_defs max_new
+ (relevance_override as {add, del, only}) thy ctab p
+ rel_consts =
+ let val add_thms = maps (ProofContext.get_fact ctxt) add
+ val del_thms = maps (ProofContext.get_fact ctxt) del
+ fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*)
| relevant (newpairs,rejects) [] =
let val (newrels,more_rejects) = take_best max_new newpairs
val new_consts = maps #2 newrels
@@ -272,11 +276,17 @@
val newp = p + (1.0-p) / convergence
in
trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
- (map #1 newrels) @
- (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
+ map #1 newrels @
+ relevant_clauses ctxt follow_defs max_new relevance_override thy ctab
+ newp rel_consts' (more_rejects @ rejects)
end
- | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
- let val weight = clause_weight ctab rel_consts consts_typs
+ | relevant (newrels, rejects)
+ ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
+ let
+ val weight = if member Thm.eq_thm del_thms thm then 0.0
+ else if member Thm.eq_thm add_thms thm then 1.0
+ else if only then 0.0
+ else clause_weight ctab rel_consts consts_typs
in
if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
@@ -285,23 +295,30 @@
else relevant (newrels, ax::rejects) axs
end
in trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
- relevant ([],[])
+ relevant ([],[])
end;
-fun relevance_filter max_new theory_const thy axioms goals =
- if run_relevance_filter andalso pass_mark >= 0.1
- then
- let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
+fun relevance_filter ctxt relevance_threshold follow_defs max_new
+ add_theory_const relevance_override thy axioms goals =
+ if relevance_threshold > 0.0 then
+ let
+ val const_tab = List.foldl (count_axiom_consts add_theory_const thy)
+ Symtab.empty axioms
val goal_const_tab = get_goal_consts_typs thy goals
- val _ = trace_msg (fn () => ("Initial constants: " ^
- space_implode ", " (Symtab.keys goal_const_tab)));
- val rels = relevant_clauses max_new thy const_tab (pass_mark)
- goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms)
- in
- trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
- rels
- end
- else axioms;
+ val _ =
+ trace_msg (fn () => "Initial constants: " ^
+ commas (Symtab.keys goal_const_tab))
+ val relevant =
+ relevant_clauses ctxt follow_defs max_new relevance_override thy
+ const_tab relevance_threshold goal_const_tab
+ (map (pair_consts_typs_axiom add_theory_const thy)
+ axioms)
+ in
+ trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
+ relevant
+ end
+ else
+ axioms;
(***************************************************************)
(* Retrieving and filtering lemmas *)
@@ -526,34 +543,37 @@
likely to lead to unsound proofs.*)
fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
-fun is_first_order thy goal_cls =
- case translation_mode of
- Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
- | Fol => true
- | Hol => false
+fun is_first_order thy higher_order goal_cls =
+ case higher_order of
+ NONE => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
+ | SOME b => not b
-fun get_relevant_facts max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
+fun get_relevant_facts relevance_threshold higher_order follow_defs max_new
+ add_theory_const relevance_override
+ (ctxt, (chain_ths, th)) goal_cls =
let
val thy = ProofContext.theory_of ctxt
- val is_FO = is_first_order thy goal_cls
+ val is_FO = is_first_order thy higher_order goal_cls
val included_cls = get_all_lemmas ctxt
|> cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy is_FO
|> remove_unwanted_clauses
in
- relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
+ relevance_filter ctxt relevance_threshold follow_defs max_new
+ add_theory_const relevance_override thy included_cls
+ (map prop_of goal_cls)
end;
(* prepare for passing to writer,
create additional clauses based on the information from extra_cls *)
-fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
+fun prepare_clauses higher_order dfg goal_cls chain_ths axcls extra_cls thy =
let
(* add chain thms *)
val chain_cls =
cnf_rules_pairs thy (filter check_named (map pairname chain_ths))
val axcls = chain_cls @ axcls
val extra_cls = chain_cls @ extra_cls
- val is_FO = is_first_order thy goal_cls
+ val is_FO = is_first_order thy higher_order goal_cls
val ccls = subtract_cls goal_cls extra_cls
val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
val ccltms = map prop_of ccls
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Mar 27 00:08:39 2010 +0100
@@ -51,9 +51,9 @@
conclusion variable to False.*)
fun transform_elim th =
case concl_of th of (*conclusion variable*)
- Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
+ @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
- | v as Var(_, Type("prop",[])) =>
+ | v as Var(_, @{typ prop}) =>
Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
| _ => th;
@@ -76,7 +76,7 @@
fun declare_skofuns s th =
let
val nref = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
+ fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (_, T, p))) (axs, thy) =
(*Existential: declare a Skolem function, then insert into body and continue*)
let
val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
@@ -95,20 +95,20 @@
Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
- | dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx =
+ | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
(*Universal quant: insert a free variable into body and continue*)
let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
in dec_sko (subst_bound (Free (fname, T), p)) thx end
- | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
- | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
- | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
+ | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
+ | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
+ | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
| dec_sko t thx = thx (*Do nothing otherwise*)
in fn thy => dec_sko (Thm.prop_of th) ([], thy) end;
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skofuns s th =
let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
+ fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs(_,T,p))) defs =
(*Existential: declare a Skolem function, then insert into body and continue*)
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
@@ -123,13 +123,13 @@
in dec_sko (subst_bound (list_comb(c,args), p))
(def :: defs)
end
- | dec_sko (Const ("All",_) $ Abs (a, T, p)) defs =
+ | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
(*Universal quant: insert a free variable into body and continue*)
let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
in dec_sko (subst_bound (Free(fname,T), p)) defs end
- | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
+ | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
| dec_sko t defs = defs (*Do nothing otherwise*)
in dec_sko (prop_of th) [] end;
@@ -156,7 +156,7 @@
fun strip_lambdas 0 th = th
| strip_lambdas n th =
case prop_of th of
- _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
+ _ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) =>
strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
| _ => th;
@@ -171,7 +171,7 @@
let
val thy = theory_of_cterm ct
val Abs(x,_,body) = term_of ct
- val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
+ val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
in
@@ -262,8 +262,9 @@
val (chilbert,cabs) = Thm.dest_comb ch
val thy = Thm.theory_of_cterm chilbert
val t = Thm.term_of chilbert
- val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
- | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
+ val T = case t of
+ Const (@{const_name Eps}, Type (@{type_name fun},[_,T])) => T
+ | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
val cex = Thm.cterm_of thy (HOLogic.exists_const T)
val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
@@ -289,7 +290,7 @@
map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
-(*** Blacklisting (duplicated in "Sledgehammer_Fact_Filter"?) ***)
+(*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***)
val max_lambda_nesting = 3;
@@ -320,7 +321,8 @@
fun is_strange_thm th =
case head_of (concl_of th) of
- Const (a, _) => (a <> "Trueprop" andalso a <> "==")
+ Const (a, _) => (a <> @{const_name Trueprop} andalso
+ a <> @{const_name "=="})
| _ => false;
fun bad_for_atp th =
@@ -328,9 +330,10 @@
orelse exists_type type_has_topsort (prop_of th)
orelse is_strange_thm th;
+(* FIXME: put other record thms here, or declare as "no_atp" *)
val multi_base_blacklist =
- ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",
- "cases","ext_cases"]; (* FIXME put other record thms here, or declare as "no_atp" *)
+ ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
+ "split_asm", "cases", "ext_cases"];
(*Keep the full complexity of the original name*)
fun flatten_name s = space_implode "_X" (Long_Name.explode s);
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Sat Mar 27 00:08:39 2010 +0100
@@ -48,7 +48,7 @@
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
-(* Parameter t_full below indicates that full type information is to be
+(* Parameter "full_types" below indicates that full type information is to be
exported *)
(* If true, each function will be directly applied to as many arguments as
@@ -210,10 +210,8 @@
fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
| head_needs_hBOOL _ _ = true;
-fun wrap_type t_full (s, tp) =
- if t_full then
- type_wrapper ^ paren_pack [s, string_of_fol_type tp]
- else s;
+fun wrap_type full_types (s, tp) =
+ if full_types then type_wrapper ^ paren_pack [s, string_of_fol_type tp] else s;
fun apply ss = "hAPP" ^ paren_pack ss;
@@ -224,7 +222,7 @@
(*Apply an operator to the argument strings, using either the "apply" operator or
direct function application.*)
-fun string_of_applic t_full cma (CombConst (c, _, tvars), args) =
+fun string_of_applic full_types cma (CombConst (c, _, tvars), args) =
let val c = if c = "equal" then "c_fequal" else c
val nargs = min_arity_of cma c
val args1 = List.take(args, nargs)
@@ -232,21 +230,22 @@
Int.toString nargs ^ " but is applied to " ^
space_implode ", " args)
val args2 = List.drop(args, nargs)
- val targs = if not t_full then map string_of_fol_type tvars else []
+ val targs = if full_types then [] else map string_of_fol_type tvars
in
string_apply (c ^ paren_pack (args1@targs), args2)
end
| string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
| string_of_applic _ _ _ = error "string_of_applic";
-fun wrap_type_if t_full cnh (head, s, tp) =
- if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
+fun wrap_type_if full_types cnh (head, s, tp) =
+ if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else s;
-fun string_of_combterm (params as (t_full, cma, cnh)) t =
+fun string_of_combterm (params as (full_types, cma, cnh)) t =
let val (head, args) = strip_combterm_comb t
- in wrap_type_if t_full cnh (head,
- string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
- type_of_combterm t)
+ in wrap_type_if full_types cnh (head,
+ string_of_applic full_types cma
+ (head, map (string_of_combterm (params)) args),
+ type_of_combterm t)
end;
(*Boolean-valued terms are here converted to literals.*)
@@ -318,11 +317,11 @@
fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
-fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
+fun add_decls (full_types, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
if c = "equal" then (addtypes tvars funcs, preds)
else
let val arity = min_arity_of cma c
- val ntys = if not t_full then length tvars else 0
+ val ntys = if not full_types then length tvars else 0
val addit = Symtab.update(c, arity+ntys)
in
if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
@@ -452,12 +451,12 @@
(* TPTP format *)
-fun write_tptp_file t_full file clauses =
+fun write_tptp_file full_types file clauses =
let
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
- val params = (t_full, cma, cnh)
+ val params = (full_types, cma, cnh)
val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
val _ =
@@ -474,12 +473,12 @@
(* DFG format *)
-fun write_dfg_file t_full file clauses =
+fun write_dfg_file full_types file clauses =
let
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
- val params = (t_full, cma, cnh)
+ val params = (full_types, cma, cnh)
val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
and probname = Path.implode (Path.base file)
val axstrs = map (#1 o (clause2dfg params)) axclauses
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Mar 27 00:08:39 2010 +0100
@@ -4,84 +4,292 @@
Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
*)
-structure Sledgehammer_Isar : sig end =
+signature SLEDGEHAMMER_ISAR =
+sig
+ type params = ATP_Manager.params
+
+ val default_params : theory -> (string * string) list -> params
+end;
+
+structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
struct
+open Sledgehammer_Util
open ATP_Manager
open ATP_Minimal
+open ATP_Wrapper
structure K = OuterKeyword and P = OuterParse
-val _ =
- OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
+fun add_to_relevance_override ns : relevance_override =
+ {add = ns, del = [], only = false}
+fun del_from_relevance_override ns : relevance_override =
+ {add = [], del = ns, only = false}
+fun only_relevance_override ns : relevance_override =
+ {add = ns, del = [], only = true}
+val default_relevance_override = add_to_relevance_override []
+fun merge_relevance_override_pairwise r1 r2 : relevance_override =
+ {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
+ only = #only r1 orelse #only r2}
+fun merge_relevance_overrides rs =
+ fold merge_relevance_override_pairwise rs default_relevance_override
-val _ =
- OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
+type raw_param = string * string list
+
+val default_default_params =
+ [("debug", "false"),
+ ("verbose", "false"),
+ ("relevance_threshold", "50"),
+ ("higher_order", "smart"),
+ ("respect_no_atp", "true"),
+ ("follow_defs", "false"),
+ ("isar_proof", "false"),
+ ("minimize_timeout", "5 s")]
-val _ =
- OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
- (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
- (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
+val negated_params =
+ [("no_debug", "debug"),
+ ("quiet", "verbose"),
+ ("partial_types", "full_types"),
+ ("first_order", "higher_order"),
+ ("ignore_no_atp", "respect_no_atp"),
+ ("dont_follow_defs", "follow_defs"),
+ ("metis_proof", "isar_proof")]
+
+val property_dependent_params = ["atps", "full_types", "timeout"]
+
+fun is_known_raw_param s =
+ AList.defined (op =) default_default_params s orelse
+ AList.defined (op =) negated_params s orelse
+ member (op =) property_dependent_params s
-val _ =
- OuterSyntax.improper_command "print_atps" "print external provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
- Toplevel.keep (print_provers o Toplevel.theory_of)));
+fun check_raw_param (s, _) =
+ if is_known_raw_param s then ()
+ else error ("Unknown parameter: " ^ quote s ^ ".")
+
+fun unnegate_raw_param (name, value) =
+ case AList.lookup (op =) negated_params name of
+ SOME name' => (name', case value of
+ ["false"] => ["true"]
+ | ["true"] => ["false"]
+ | [] => ["false"]
+ | _ => value)
+ | NONE => (name, value)
+
+structure Data = Theory_Data(
+ type T = raw_param list
+ val empty = default_default_params |> map (apsnd single)
+ val extend = I
+ fun merge p : T = AList.merge (op =) (K true) p)
-val _ =
- OuterSyntax.command "sledgehammer"
- "search for first-order proof using automatic theorem provers" K.diag
- (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
+val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
+fun default_raw_params thy =
+ [("atps", [!atps]),
+ ("full_types", [if !full_types then "true" else "false"]),
+ ("timeout", [string_of_int (!timeout) ^ " s"])] @
+ Data.get thy
-val default_minimize_prover = "remote_vampire"
-val default_minimize_time_limit = 5
+val infinity_time_in_secs = 60 * 60 * 24 * 365
+val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
-fun atp_minimize_command args thm_names state =
+fun extract_params thy default_params override_params =
let
- fun theorems_from_names ctxt =
- map (fn (name, interval) =>
+ val override_params = map unnegate_raw_param override_params
+ val raw_params = rev override_params @ rev default_params
+ val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
+ val lookup_string = the_default "" o lookup
+ fun general_lookup_bool option default_value name =
+ case lookup name of
+ SOME s => parse_bool_option option name s
+ | NONE => default_value
+ val lookup_bool = the o general_lookup_bool false (SOME false)
+ val lookup_bool_option = general_lookup_bool true NONE
+ fun lookup_time name =
+ the_timeout (case lookup name of
+ NONE => NONE
+ | SOME s => parse_time_option name s)
+ fun lookup_int name =
+ case lookup name of
+ NONE => 0
+ | SOME s => case Int.fromString s of
+ SOME n => n
+ | NONE => error ("Parameter " ^ quote name ^
+ " must be assigned an integer value.")
+ val debug = lookup_bool "debug"
+ val verbose = debug orelse lookup_bool "verbose"
+ val atps = lookup_string "atps" |> space_explode " "
+ val full_types = lookup_bool "full_types"
+ val relevance_threshold =
+ 0.01 * Real.fromInt (lookup_int "relevance_threshold")
+ val higher_order = lookup_bool_option "higher_order"
+ val respect_no_atp = lookup_bool "respect_no_atp"
+ val follow_defs = lookup_bool "follow_defs"
+ val isar_proof = lookup_bool "isar_proof"
+ val timeout = lookup_time "timeout"
+ val minimize_timeout = lookup_time "minimize_timeout"
+ in
+ {debug = debug, verbose = verbose, atps = atps, full_types = full_types,
+ relevance_threshold = relevance_threshold, higher_order = higher_order,
+ respect_no_atp = respect_no_atp, follow_defs = follow_defs,
+ isar_proof = isar_proof, timeout = timeout,
+ minimize_timeout = minimize_timeout}
+ end
+
+fun get_params thy = extract_params thy (default_raw_params thy)
+fun default_params thy = get_params thy o map (apsnd single)
+
+fun atp_minimize_command override_params old_style_args fact_refs state =
+ let
+ val thy = Proof.theory_of state
+ val ctxt = Proof.context_of state
+ fun theorems_from_refs ctxt =
+ map (fn fact_ref =>
let
- val thmref = Facts.Named ((name, Position.none), interval)
- val ths = ProofContext.get_fact ctxt thmref
- val name' = Facts.string_of_ref thmref
+ val ths = ProofContext.get_fact ctxt fact_ref
+ val name' = Facts.string_of_ref fact_ref
in (name', ths) end)
- fun get_time_limit_arg time_string =
- (case Int.fromString time_string of
- SOME t => t
- | NONE => error ("Invalid time limit: " ^ quote time_string))
+ fun get_time_limit_arg s =
+ (case Int.fromString s of
+ SOME t => Time.fromSeconds t
+ | NONE => error ("Invalid time limit: " ^ quote s))
fun get_opt (name, a) (p, t) =
(case name of
"time" => (p, get_time_limit_arg a)
| "atp" => (a, t)
| n => error ("Invalid argument: " ^ n))
- fun get_options args =
- fold get_opt args (default_minimize_prover, default_minimize_time_limit)
- val (prover_name, time_limit) = get_options args
+ val {atps, minimize_timeout, ...} = get_params thy override_params
+ val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout)
+ val params =
+ get_params thy
+ [("atps", [atp]),
+ ("minimize_timeout",
+ [string_of_int (Time.toSeconds timeout) ^ " s"])]
val prover =
- (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
+ (case get_prover thy atp of
SOME prover => prover
- | NONE => error ("Unknown prover: " ^ quote prover_name))
- val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
+ | NONE => error ("Unknown ATP: " ^ quote atp))
+ val name_thms_pairs = theorems_from_refs ctxt fact_refs
in
- writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
- state name_thms_pairs))
+ writeln (#2 (minimize_theorems params linear_minimize prover atp state
+ name_thms_pairs))
+ end
+
+val runN = "run"
+val minimizeN = "minimize"
+val messagesN = "messages"
+val available_atpsN = "available_atps"
+val running_atpsN = "running_atps"
+val kill_atpsN = "kill_atps"
+val refresh_tptpN = "refresh_tptp"
+val helpN = "help"
+
+val addN = "add"
+val delN = "del"
+val onlyN = "only"
+
+fun hammer_away override_params subcommand opt_i relevance_override state =
+ let
+ val thy = Proof.theory_of state
+ val _ = List.app check_raw_param override_params
+ in
+ if subcommand = runN then
+ sledgehammer (get_params thy override_params) (the_default 1 opt_i)
+ relevance_override state
+ else if subcommand = minimizeN then
+ atp_minimize_command override_params [] (#add relevance_override) state
+ else if subcommand = messagesN then
+ messages opt_i
+ else if subcommand = available_atpsN then
+ available_atps thy
+ else if subcommand = running_atpsN then
+ running_atps ()
+ else if subcommand = kill_atpsN then
+ kill_atps ()
+ else if subcommand = refresh_tptpN then
+ refresh_systems_on_tptp ()
+ else
+ error ("Unknown subcommand: " ^ quote subcommand ^ ".")
end
-local structure K = OuterKeyword and P = OuterParse in
+fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) =
+ Toplevel.keep (hammer_away params subcommand opt_i relevance_override
+ o Toplevel.proof_of)
+
+fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value
+
+fun sledgehammer_params_trans params =
+ Toplevel.theory
+ (fold set_default_raw_param params
+ #> tap (fn thy =>
+ writeln ("Default parameters for Sledgehammer:\n" ^
+ (case rev (default_raw_params thy) of
+ [] => "none"
+ | params =>
+ (map check_raw_param params;
+ params |> map string_for_raw_param
+ |> sort_strings |> cat_lines)))))
-val parse_args =
- Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
-val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
+val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
+val parse_value = Scan.repeat1 P.xname
+val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
+val parse_params = Scan.optional (Args.bracks (P.list parse_param)) []
+val parse_fact_refs =
+ Scan.repeat1 (Scan.unless (P.name -- Args.colon)
+ (P.xname -- Scan.option Attrib.thm_sel)
+ >> (fn (name, interval) =>
+ Facts.Named ((name, Position.none), interval)))
+val parse_relevance_chunk =
+ (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
+ || (Args.del |-- Args.colon |-- parse_fact_refs
+ >> del_from_relevance_override)
+ || (P.$$$ onlyN |-- Args.colon |-- parse_fact_refs >> only_relevance_override)
+val parse_relevance_override =
+ Scan.optional (Args.parens
+ (Scan.optional (parse_fact_refs >> only_relevance_override)
+ default_relevance_override
+ -- Scan.repeat parse_relevance_chunk)
+ >> op :: >> merge_relevance_overrides)
+ default_relevance_override
+val parse_sledgehammer_command =
+ (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
+ -- Scan.option P.nat) #>> sledgehammer_trans
+val parse_sledgehammer_params_command =
+ parse_params #>> sledgehammer_params_trans
+
+val parse_minimize_args =
+ Scan.optional (Args.bracks (P.list (P.short_ident --| P.$$$ "=" -- P.xname)))
+ []
+val _ =
+ OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_atps))
+val _ =
+ OuterSyntax.improper_command "atp_info"
+ "print information about managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative running_atps))
+val _ =
+ OuterSyntax.improper_command "atp_messages"
+ "print recent messages issued by managed provers" K.diag
+ (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
+ (fn limit => Toplevel.no_timing
+ o Toplevel.imperative (fn () => messages limit)))
+val _ =
+ OuterSyntax.improper_command "print_atps" "print external provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+ Toplevel.keep (available_atps o Toplevel.theory_of)))
+val _ =
+ OuterSyntax.improper_command "atp_minimize"
+ "minimize theorem list with external prover" K.diag
+ (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) =>
+ Toplevel.no_timing o Toplevel.unknown_proof o
+ Toplevel.keep (atp_minimize_command [] args fact_refs
+ o Toplevel.proof_of)))
val _ =
- OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
- (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
- Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
-
-end
+ OuterSyntax.improper_command "sledgehammer"
+ "search for first-order proof using automatic theorem provers" K.diag
+ parse_sledgehammer_command
+val _ =
+ OuterSyntax.command "sledgehammer_params"
+ "set and display the default parameters for Sledgehammer" K.thy_decl
+ parse_sledgehammer_params_command
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sat Mar 27 00:08:39 2010 +0100
@@ -339,18 +339,18 @@
let
val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt)
- fun have_or_show "show" _ = "show \""
- | have_or_show have lname = have ^ " " ^ lname ^ ": \""
+ fun have_or_show "show" _ = " show \""
+ | have_or_show have lname = " " ^ have ^ " " ^ lname ^ ": \""
fun do_line _ (lname, t, []) =
(* No deps: it's a conjecture clause, with no proof. *)
(case permuted_clause t ctms of
- SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
+ SOME u => " assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
| NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
[t]))
| do_line have (lname, t, deps) =
have_or_show have lname ^
string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^
- "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
+ "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
| do_lines ((lname, t, deps) :: lines) =
do_line "have" (lname, t, deps) :: do_lines lines
@@ -535,18 +535,20 @@
val kill_chained = filter_out (curry (op =) chained_hint)
(* metis-command *)
-fun metis_line [] = "apply metis"
- | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
+fun metis_line [] = "by metis"
+ | metis_line xs = "by (metis " ^ space_implode " " xs ^ ")"
-(* atp_minimize [atp=<prover>] <lemmas> *)
fun minimize_line _ [] = ""
- | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
- Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
- space_implode " " (kill_chained lemmas))
+ | minimize_line name lemmas =
+ "To minimize the number of lemmas, try this command:\n" ^
+ Markup.markup Markup.sendback
+ ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
+ space_implode " " (kill_chained lemmas) ^ ")") ^ "."
fun metis_lemma_list dfg name result =
let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
- (Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^
+ ("Try this command: " ^
+ Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ ".\n" ^
minimize_line name lemmas ^
(if used_conj then
""
@@ -570,8 +572,11 @@
if member (op =) tokens chained_hint then ""
else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
in
- (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback isar_proof,
- lemma_names)
+ (* Hack: The " \n" shouldn't be part of the markup. This is a workaround
+ for a strange ProofGeneral bug, whereby the first two letters of the word
+ "proof" are not highlighted. *)
+ (one_line_proof ^ "\n\nStructured proof:" ^
+ Markup.markup Markup.sendback (" \n" ^ isar_proof), lemma_names)
end
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Mar 27 00:08:39 2010 +0100
@@ -0,0 +1,53 @@
+(* Title: HOL/Sledgehammer/sledgehammer_util.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+General-purpose functions used by the Sledgehammer modules.
+*)
+
+signature SLEDGEHAMMER_UTIL =
+sig
+ val serial_commas : string -> string list -> string list
+ val parse_bool_option : bool -> string -> string -> bool option
+ val parse_time_option : string -> string -> Time.time option
+end;
+
+structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
+struct
+
+fun serial_commas _ [] = ["??"]
+ | serial_commas _ [s] = [s]
+ | serial_commas conj [s1, s2] = [s1, conj, s2]
+ | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
+ | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
+
+fun parse_bool_option option name s =
+ (case s of
+ "smart" => if option then NONE else raise Option
+ | "false" => SOME false
+ | "true" => SOME true
+ | "" => SOME true
+ | _ => raise Option)
+ handle Option.Option =>
+ let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
+ error ("Parameter " ^ quote name ^ " must be assigned " ^
+ space_implode " " (serial_commas "or" ss) ^ ".")
+ end
+
+fun parse_time_option _ "none" = NONE
+ | parse_time_option name s =
+ let
+ val msecs =
+ case space_explode " " s of
+ [s1, "min"] => 60000 * the (Int.fromString s1)
+ | [s1, "s"] => 1000 * the (Int.fromString s1)
+ | [s1, "ms"] => the (Int.fromString s1)
+ | _ => 0
+ in
+ if msecs <= 0 then
+ error ("Parameter " ^ quote name ^ " must be assigned a positive time \
+ \value (e.g., \"60 s\", \"200 ms\") or \"none\".")
+ else
+ SOME (Time.fromMilliseconds msecs)
+ end
+
+end;
--- a/src/Pure/General/graph.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/Pure/General/graph.ML Sat Mar 27 00:08:39 2010 +0100
@@ -202,13 +202,17 @@
fun no_edges (i, _) = (i, ([], []));
-fun join f (Graph tab1, G2 as Graph tab2) =
- let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1)
- in fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end;
+fun join f (G1 as Graph tab1, G2 as Graph tab2) =
+ let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in
+ if pointer_eq (G1, G2) then G1
+ else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2)))
+ end;
-fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
- let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2)
- in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end;
+fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) =
+ let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2) in
+ if pointer_eq (G1, G2) then G1
+ else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2)))
+ end;
fun merge eq GG = gen_merge add_edge eq GG;
@@ -273,9 +277,11 @@
|> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]);
fun merge_trans_acyclic eq (G1, G2) =
- merge_acyclic eq (G1, G2)
- |> fold add_edge_trans_acyclic (diff_edges G1 G2)
- |> fold add_edge_trans_acyclic (diff_edges G2 G1);
+ if pointer_eq (G1, G2) then G1
+ else
+ merge_acyclic eq (G1, G2)
+ |> fold add_edge_trans_acyclic (diff_edges G1 G2)
+ |> fold add_edge_trans_acyclic (diff_edges G2 G1);
(*final declarations of this structure!*)
--- a/src/Pure/Isar/attrib.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/Pure/Isar/attrib.ML Sat Mar 27 00:08:39 2010 +0100
@@ -396,6 +396,8 @@
register_config Unify.search_bound_value #>
register_config Unify.trace_simp_value #>
register_config Unify.trace_types_value #>
- register_config MetaSimplifier.simp_depth_limit_value));
+ register_config MetaSimplifier.simp_depth_limit_value #>
+ register_config MetaSimplifier.debug_simp_value #>
+ register_config MetaSimplifier.trace_simp_value));
end;
--- a/src/Pure/ProofGeneral/preferences.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML Sat Mar 27 00:08:39 2010 +0100
@@ -146,10 +146,7 @@
"Show leading question mark of variable name"];
val tracing_preferences =
- [bool_pref trace_simp
- "trace-simplifier"
- "Trace simplification rules.",
- nat_pref trace_simp_depth_limit
+ [nat_pref trace_simp_depth_limit
"trace-simplifier-depth"
"Trace simplifier depth limit.",
bool_pref trace_rules
--- a/src/Pure/axclass.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/Pure/axclass.ML Sat Mar 27 00:08:39 2010 +0100
@@ -37,9 +37,6 @@
val param_of_inst: theory -> string * string -> string
val inst_of_param: theory -> string -> (string * string) option
val thynames_of_arity: theory -> class * string -> string list
- type cache
- val of_sort: theory -> typ * sort -> cache -> thm list * cache (*exception Sorts.CLASS_ERROR*)
- val cache: cache
val introN: string
val axiomsN: string
end;
@@ -190,7 +187,7 @@
Sign.super_classes thy c
|> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t));
- val completions = map (fn c1 => (Sorts.weaken algebra
+ val completions = map (fn c1 => (Sorts.classrel_derivation algebra
(fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
|> Thm.close_derivation, c1)) super_class_completions;
val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), (th1, thy_name))))
@@ -564,59 +561,4 @@
end;
-
-
-(** explicit derivations -- cached **)
-
-datatype cache = Types of (class * thm) list Typtab.table;
-
-local
-
-fun lookup_type (Types cache) = AList.lookup (op =) o Typtab.lookup_list cache;
-fun insert_type T der (Types cache) = Types (Typtab.insert_list (eq_fst op =) (T, der) cache);
-
-fun derive_type _ (_, []) = []
- | derive_type thy (typ, sort) =
- let
- val certT = Thm.ctyp_of thy;
- val vars = Term.fold_atyps
- (fn T as TFree (_, S) => insert (eq_fst op =) (T, S)
- | T as TVar (_, S) => insert (eq_fst op =) (T, S)
- | _ => I) typ [];
- val hyps = vars
- |> map (fn (T, S) => (T, Thm.of_sort (certT T, S) ~~ S));
- val ths = (typ, sort)
- |> Sorts.of_sort_derivation (Sign.classes_of thy)
- {class_relation =
- fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
- type_constructor =
- fn a => fn dom => fn c =>
- let val Ss = map (map snd) dom and ths = maps (map fst) dom
- in ths MRS the_arity thy a (c, Ss) end,
- type_variable =
- the_default [] o AList.lookup (op =) hyps};
- in ths end;
-
-in
-
-fun of_sort thy (typ, sort) cache =
- let
- val sort' = filter (is_none o lookup_type cache typ) sort;
- val ths' = derive_type thy (typ, sort')
- handle ERROR msg => cat_error msg ("The error(s) above occurred for sort derivation: " ^
- Syntax.string_of_typ_global thy typ ^ " :: " ^ Syntax.string_of_sort_global thy sort');
- val cache' = cache |> fold (insert_type typ) (sort' ~~ ths');
- val ths =
- sort |> map (fn c =>
- Goal.finish
- (Syntax.init_pretty_global thy)
- (the (lookup_type cache' typ c) RS
- Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c))))
- |> Thm.adjust_maxidx_thm ~1);
- in (ths, cache') end;
-
end;
-
-val cache = Types Typtab.empty;
-
-end;
--- a/src/Pure/library.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/Pure/library.ML Sat Mar 27 00:08:39 2010 +0100
@@ -774,6 +774,8 @@
| NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
in match (space_explode "*" pat) str end;
+
+
(** lists as sets -- see also Pure/General/ord_list.ML **)
(* canonical operations *)
--- a/src/Pure/meta_simplifier.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/Pure/meta_simplifier.ML Sat Mar 27 00:08:39 2010 +0100
@@ -11,8 +11,10 @@
signature BASIC_META_SIMPLIFIER =
sig
- val debug_simp: bool Unsynchronized.ref
- val trace_simp: bool Unsynchronized.ref
+ val debug_simp: bool Config.T
+ val debug_simp_value: Config.value Config.T
+ val trace_simp: bool Config.T
+ val trace_simp_value: Config.value Config.T
val trace_simp_depth_limit: int Unsynchronized.ref
type rrule
val eq_rrule: rrule * rrule -> bool
@@ -271,8 +273,11 @@
exception SIMPLIFIER of string * thm;
-val debug_simp = Unsynchronized.ref false;
-val trace_simp = Unsynchronized.ref false;
+val debug_simp_value = Config.declare false "debug_simp" (Config.Bool false);
+val debug_simp = Config.bool debug_simp_value;
+
+val trace_simp_value = Config.declare false "trace_simp" (Config.Bool false);
+val trace_simp = Config.bool trace_simp_value;
local
@@ -285,33 +290,39 @@
fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
+fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
+ Syntax.string_of_term ctxt
+ (if Config.get ctxt debug_simp then t else show_bounds ss t));
+
in
-fun print_term ss warn a thy t = prnt ss warn (a ^ "\n" ^
- Syntax.string_of_term_global thy (if ! debug_simp then t else show_bounds ss t));
+fun print_term_global ss warn a thy t =
+ print_term ss warn (K a) t (ProofContext.init thy);
-fun debug warn a ss = if ! debug_simp then prnt ss warn (a ()) else ();
-fun trace warn a ss = if ! trace_simp then prnt ss warn (a ()) else ();
+fun if_enabled (Simpset ({context, ...}, _)) flag f =
+ (case context of
+ SOME ctxt => if Config.get ctxt flag then f ctxt else ()
+ | NONE => ())
-fun debug_term warn a ss thy t = if ! debug_simp then print_term ss warn (a ()) thy t else ();
-fun trace_term warn a ss thy t = if ! trace_simp then print_term ss warn (a ()) thy t else ();
+fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ()));
+fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ()));
+
+fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t);
+fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t);
fun trace_cterm warn a ss ct =
- if ! trace_simp then print_term ss warn (a ()) (Thm.theory_of_cterm ct) (Thm.term_of ct)
- else ();
+ if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
fun trace_thm a ss th =
- if ! trace_simp then print_term ss false (a ()) (Thm.theory_of_thm th) (Thm.full_prop_of th)
- else ();
+ if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
fun trace_named_thm a ss (th, name) =
- if ! trace_simp then
- print_term ss false (if name = "" then a () else a () ^ " " ^ quote name ^ ":")
- (Thm.theory_of_thm th) (Thm.full_prop_of th)
- else ();
+ if_enabled ss trace_simp (print_term ss false
+ (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
+ (Thm.full_prop_of th));
fun warn_thm a ss th =
- print_term ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
+ print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
fun cond_warn_thm a (ss as Simpset ({context, ...}, _)) th =
if is_some context then () else warn_thm a ss th;
@@ -824,7 +835,7 @@
val _ $ _ $ prop0 = Thm.prop_of thm;
in
trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
- trace_term false (fn () => "Should have proved:") ss thy prop0;
+ trace_term false (fn () => "Should have proved:") ss prop0;
NONE
end;
@@ -943,7 +954,7 @@
fun proc_rews [] = NONE
| proc_rews (Proc {name, proc, lhs, ...} :: ps) =
if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
- (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss thyt eta_t;
+ (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss eta_t;
case proc ss eta_t' of
NONE => (debug false (fn () => "FAILED") ss; proc_rews ps)
| SOME raw_thm =>
@@ -1216,7 +1227,7 @@
| _ => I) (term_of ct) [];
in
if null bs then ()
- else print_term ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs)
+ else print_term_global ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs)
(Thm.theory_of_cterm ct) (Thm.term_of ct)
end
else ();
--- a/src/Pure/sorts.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/Pure/sorts.ML Sat Mar 27 00:08:39 2010 +0100
@@ -56,12 +56,13 @@
-> sort Vartab.table -> sort Vartab.table (*exception CLASS_ERROR*)
val meet_sort_typ: algebra -> typ * sort -> typ -> typ (*exception CLASS_ERROR*)
val of_sort: algebra -> typ * sort -> bool
- val weaken: algebra -> ('a * class -> class -> 'a) -> 'a * class -> class -> 'a
val of_sort_derivation: algebra ->
{class_relation: 'a * class -> class -> 'a,
type_constructor: string -> ('a * class) list list -> class -> 'a,
type_variable: typ -> ('a * class) list} ->
typ * sort -> 'a list (*exception CLASS_ERROR*)
+ val classrel_derivation: algebra ->
+ ('a * class -> class -> 'a) -> 'a * class -> class -> 'a (*exception CLASS_ERROR*)
val witness_sorts: algebra -> string list -> (typ * sort) list -> sort list -> (typ * sort) list
end;
@@ -253,18 +254,21 @@
(filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars)
else err_conflict pp t NONE (c, Ss) (c, Ss'));
-fun insert_ars pp algebra (t, ars) arities =
+in
+
+fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
+
+fun insert_complete_ars pp algebra (t, ars) arities =
let val ars' =
Symtab.lookup_list arities t
- |> fold_rev (fold_rev (insert pp algebra t)) (map (complete algebra) ars)
+ |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars);
in Symtab.update (t, ars') arities end;
-in
-
-fun add_arities pp arg algebra = algebra |> map_arities (insert_ars pp algebra arg);
+fun add_arities pp arg algebra =
+ algebra |> map_arities (insert_complete_ars pp algebra arg);
fun add_arities_table pp algebra =
- Symtab.fold (fn (t, ars) => insert_ars pp algebra (t, map snd ars));
+ Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, map snd ars));
end;
@@ -290,11 +294,22 @@
let
val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
handle Graph.DUP c => err_dup_class c
- | Graph.CYCLES css => err_cyclic_classes pp css;
+ | Graph.CYCLES css => err_cyclic_classes pp css;
val algebra0 = make_algebra (classes', Symtab.empty);
- val arities' = Symtab.empty
- |> add_arities_table pp algebra0 arities1
- |> add_arities_table pp algebra0 arities2;
+ val arities' =
+ (case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
+ (true, true) => arities1
+ | (true, false) => (*no completion*)
+ (arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) =>
+ if pointer_eq (ars1, ars2) then raise Symtab.SAME
+ else insert_ars pp algebra0 t ars2 ars1)
+ | (false, true) => (*unary completion*)
+ Symtab.empty
+ |> add_arities_table pp algebra0 arities1
+ | (false, false) => (*binary completion*)
+ Symtab.empty
+ |> add_arities_table pp algebra0 arities1
+ |> add_arities_table pp algebra0 arities2);
in make_algebra (classes', arities') end;
@@ -317,7 +332,7 @@
(** sorts of types **)
-(* errors -- delayed message composition *)
+(* errors -- performance tuning via delayed message composition *)
datatype class_error =
NoClassrel of class * class |
@@ -391,24 +406,13 @@
(* animating derivations *)
-fun weaken algebra class_relation =
- let
- fun path (x, c1 :: c2 :: cs) = path (class_relation (x, c1) c2, c2 :: cs)
- | path (x, _) = x;
- in fn (x, c1) => fn c2 =>
- (case Graph.irreducible_paths (classes_of algebra) (c1, c2) of
- [] => raise CLASS_ERROR (NoClassrel (c1, c2))
- | cs :: _ => path (x, cs))
- end;
-
fun of_sort_derivation algebra {class_relation, type_constructor, type_variable} =
let
- val weaken = weaken algebra class_relation;
val arities = arities_of algebra;
- fun weakens S1 S2 = S2 |> map (fn c2 =>
+ fun weaken S1 S2 = S2 |> map (fn c2 =>
(case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
- SOME d1 => weaken d1 c2
+ SOME d1 => class_relation d1 c2
| NONE => raise CLASS_ERROR (NoSubsort (map #2 S1, S2))));
fun derive _ [] = []
@@ -420,12 +424,23 @@
S |> map (fn c =>
let
val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
- val dom' = map2 (fn d => fn S' => weakens d S' ~~ S') dom Ss';
- in weaken (type_constructor a dom' c0, c0) c end)
+ val dom' = map2 (fn d => fn S' => weaken d S' ~~ S') dom Ss';
+ in class_relation (type_constructor a dom' c0, c0) c end)
end
- | derive T S = weakens (type_variable T) S;
+ | derive T S = weaken (type_variable T) S;
in uncurry derive end;
+fun classrel_derivation algebra class_relation =
+ let
+ fun path (x, c1 :: c2 :: cs) = path (class_relation (x, c1) c2, c2 :: cs)
+ | path (x, _) = x;
+ in
+ fn (x, c1) => fn c2 =>
+ (case Graph.irreducible_paths (classes_of algebra) (c1, c2) of
+ [] => raise CLASS_ERROR (NoClassrel (c1, c2))
+ | cs :: _ => path (x, cs))
+ end;
+
(* witness_sorts *)
--- a/src/Tools/Code/code_thingol.ML Fri Mar 26 23:58:27 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML Sat Mar 27 00:08:39 2010 +0100
@@ -774,7 +774,8 @@
val sort' = proj_sort sort;
in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
val typargs = Sorts.of_sort_derivation algebra
- {class_relation = class_relation, type_constructor = type_constructor,
+ {class_relation = Sorts.classrel_derivation algebra class_relation,
+ type_constructor = type_constructor,
type_variable = type_variable} (ty, proj_sort sort)
handle Sorts.CLASS_ERROR e => not_wellsorted thy some_thm ty sort e;
fun mk_dict (Global (inst, yss)) =