--- a/NEWS Mon Aug 23 17:45:06 2010 +0200
+++ b/NEWS Mon Aug 23 17:46:13 2010 +0200
@@ -35,6 +35,8 @@
*** HOL ***
+* Dropped type classes mult_mono and mult_mono1. INCOMPATIBILITY.
+
* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
canonical names for instance definitions for functions; various improvements.
INCOMPATIBILITY.
--- a/src/HOL/Library/Convex.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Library/Convex.thy Mon Aug 23 17:46:13 2010 +0200
@@ -244,7 +244,7 @@
shows "convex_on s (\<lambda>x. c * f x)"
proof-
have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps)
- show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto
+ show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)] unfolding convex_on_def and * by auto
qed
lemma convex_lower:
@@ -253,7 +253,7 @@
proof-
let ?m = "max (f x) (f y)"
have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
- using assms(4,5) by(auto simp add: mult_mono1 add_mono)
+ using assms(4,5) by (auto simp add: mult_left_mono add_mono)
also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto
finally show ?thesis
using assms unfolding convex_on_def by fastsimp
@@ -481,8 +481,8 @@
hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastsimp
have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
\<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
- using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
- mult_mono1[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
+ using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
+ mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
hence "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
by (auto simp add:field_simps)
thus "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
--- a/src/HOL/Library/Function_Algebras.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Library/Function_Algebras.thy Mon Aug 23 17:46:13 2010 +0200
@@ -105,12 +105,6 @@
instance "fun" :: (type, mult_zero) mult_zero proof
qed (simp_all add: zero_fun_def times_fun_def)
-instance "fun" :: (type, mult_mono) mult_mono proof
-qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
-
-instance "fun" :: (type, mult_mono1) mult_mono1 proof
-qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_mono1)
-
instance "fun" :: (type, zero_neq_one) zero_neq_one proof
qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
@@ -186,9 +180,11 @@
instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
-instance "fun" :: (type, ordered_semiring) ordered_semiring ..
+instance "fun" :: (type, ordered_semiring) ordered_semiring proof
+qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
-instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring ..
+instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
+qed (fact mult_left_mono)
instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Aug 23 17:46:13 2010 +0200
@@ -2507,7 +2507,7 @@
fix i assume i:"i<DIM('a)" thus "0 < x $$ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
unfolding dist_norm by(auto simp add: inner_simps euclidean_component_def dot_basis elim!:allE[where x=i])
next have **:"dist x (x + (e / 2) *\<^sub>R basis 0) < e" using `e>0`
- unfolding dist_norm by(auto intro!: mult_strict_left_mono_comm)
+ unfolding dist_norm by(auto intro!: mult_strict_left_mono)
have "\<And>i. i<DIM('a) \<Longrightarrow> (x + (e / 2) *\<^sub>R basis 0) $$ i = x$$i + (if i = 0 then e/2 else 0)"
unfolding euclidean_component_def by(auto simp add:inner_simps dot_basis)
hence *:"setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)} = setsum (\<lambda>i. x$$i + (if 0 = i then e/2 else 0)) {..<DIM('a)}"
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Aug 23 17:46:13 2010 +0200
@@ -220,7 +220,7 @@
fixes x :: "'a::real_normed_vector"
shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
unfolding norm_scaleR
- apply (erule mult_mono1)
+ apply (erule mult_left_mono)
apply simp
done
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy Mon Aug 23 17:46:13 2010 +0200
@@ -107,7 +107,7 @@
apply (subst mult_assoc)
apply (rule order_trans)
apply (rule onorm(1)[OF lf])
- apply (rule mult_mono1)
+ apply (rule mult_left_mono)
apply (rule onorm(1)[OF lg])
apply (rule onorm_pos_le[OF lf])
done
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 23 17:46:13 2010 +0200
@@ -5678,7 +5678,7 @@
next
case (Suc m)
hence "c * dist (z m) (z (Suc m)) \<le> c ^ Suc m * d"
- using `0 \<le> c` using mult_mono1_class.mult_mono1[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
+ using `0 \<le> c` using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
thus ?case using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]
unfolding fzn and mult_le_cancel_left by auto
qed
--- a/src/HOL/NSA/StarDef.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy Mon Aug 23 17:46:13 2010 +0200
@@ -925,12 +925,12 @@
done
instance star :: (ordered_comm_semiring) ordered_comm_semiring
-by (intro_classes, transfer, rule mult_mono1_class.mult_mono1)
+by (intro_classes, transfer, rule mult_left_mono)
instance star :: (ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
instance star :: (linordered_comm_semiring_strict) linordered_comm_semiring_strict
-by (intro_classes, transfer, rule mult_strict_left_mono_comm)
+by (intro_classes, transfer, rule mult_strict_left_mono)
instance star :: (ordered_ring) ordered_ring ..
instance star :: (ordered_ring_abs) ordered_ring_abs
--- a/src/HOL/Orderings.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Orderings.thy Mon Aug 23 17:46:13 2010 +0200
@@ -1264,7 +1264,8 @@
begin
definition
- top_fun_eq: "top = (\<lambda>x. top)"
+ top_fun_eq [no_atp]: "top = (\<lambda>x. top)"
+declare top_fun_eq_raw [no_atp]
instance proof
qed (simp add: top_fun_eq le_fun_def)
--- a/src/HOL/Predicate.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Predicate.thy Mon Aug 23 17:46:13 2010 +0200
@@ -92,7 +92,7 @@
lemma top2I [intro!]: "top x y"
by (simp add: top_fun_eq top_bool_eq)
-lemma bot1E [elim!]: "bot x \<Longrightarrow> P"
+lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
by (simp add: bot_fun_eq bot_bool_eq)
lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
--- a/src/HOL/Probability/Lebesgue.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Probability/Lebesgue.thy Mon Aug 23 17:46:13 2010 +0200
@@ -700,7 +700,7 @@
using `a \<in> nnfis f` unfolding nnfis_def by auto
with `0 \<le> z`show ?thesis unfolding nnfis_def mono_convergent_def incseq_def
by (auto intro!: exI[of _ "\<lambda>n w. z * u n w"] exI[of _ "\<lambda>n. z * x n"]
- LIMSEQ_mult LIMSEQ_const psfis_mult mult_mono1)
+ LIMSEQ_mult LIMSEQ_const psfis_mult mult_left_mono)
qed
lemma nnfis_add:
--- a/src/HOL/Rings.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Rings.thy Mon Aug 23 17:46:13 2010 +0200
@@ -628,10 +628,6 @@
end
-class mult_mono = times + zero + ord +
- assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
- assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
-
text {*
The theory of partially ordered rings is taken from the books:
\begin{itemize}
@@ -645,31 +641,29 @@
\end{itemize}
*}
-class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add
+class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
+ assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
+ assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
begin
lemma mult_mono:
- "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
- \<Longrightarrow> a * c \<le> b * d"
+ "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
apply (erule mult_right_mono [THEN order_trans], assumption)
apply (erule mult_left_mono, assumption)
done
lemma mult_mono':
- "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
- \<Longrightarrow> a * c \<le> b * d"
+ "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
apply (rule mult_mono)
apply (fast intro: order_trans)+
done
end
-class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add
- + semiring + cancel_comm_monoid_add
+class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
begin
subclass semiring_0_cancel ..
-subclass ordered_semiring ..
lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
using mult_left_mono [of 0 b a] by simp
@@ -689,7 +683,7 @@
end
-class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono
+class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
begin
subclass ordered_cancel_semiring ..
@@ -854,41 +848,38 @@
end
-class mult_mono1 = times + zero + ord +
- assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
-
-class ordered_comm_semiring = comm_semiring_0
- + ordered_ab_semigroup_add + mult_mono1
+class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
+ assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
begin
subclass ordered_semiring
proof
fix a b c :: 'a
assume "a \<le> b" "0 \<le> c"
- thus "c * a \<le> c * b" by (rule mult_mono1)
+ thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
thus "a * c \<le> b * c" by (simp only: mult_commute)
qed
end
-class ordered_cancel_comm_semiring = comm_semiring_0_cancel
- + ordered_ab_semigroup_add + mult_mono1
+class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
begin
+subclass comm_semiring_0_cancel ..
subclass ordered_comm_semiring ..
subclass ordered_cancel_semiring ..
end
class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
- assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
+ assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
begin
subclass linordered_semiring_strict
proof
fix a b c :: 'a
assume "a < b" "0 < c"
- thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
+ thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
thus "a * c < b * c" by (simp only: mult_commute)
qed
--- a/src/HOL/Set.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Set.thy Mon Aug 23 17:46:13 2010 +0200
@@ -495,7 +495,7 @@
apply (rule Collect_mem_eq)
done
-lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))"
+lemma expand_set_eq [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
by(auto intro:set_ext)
lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
@@ -852,7 +852,7 @@
lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
by blast
-lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
+lemma image_subset_iff [no_atp]: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
-- {* This rewrite rule would confuse users if made default. *}
by blast
@@ -1203,7 +1203,7 @@
lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
by (fact inf_eq_top_iff)
-lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
+lemma Int_subset_iff [no_atp, simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
by (fact le_inf_iff)
lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
@@ -1294,7 +1294,7 @@
lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
by (fact sup_eq_bot_iff)
-lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
+lemma Un_subset_iff [no_atp, simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
by (fact le_sup_iff)
lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
@@ -1490,7 +1490,7 @@
lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
by blast
-lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
+lemma subset_iff [no_atp]: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
by blast
lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 23 17:46:13 2010 +0200
@@ -16,6 +16,7 @@
{exec: string * string,
required_execs: (string * string) list,
arguments: bool -> Time.time -> string,
+ has_incomplete_mode: bool,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
default_max_relevant_per_iter: int,
@@ -48,6 +49,7 @@
{exec: string * string,
required_execs: (string * string) list,
arguments: bool -> Time.time -> string,
+ has_incomplete_mode: bool,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
default_max_relevant_per_iter: int,
@@ -136,6 +138,7 @@
arguments = fn _ => fn timeout =>
"--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
string_of_int (to_generous_secs timeout),
+ has_incomplete_mode = false,
proof_delims = [tstp_proof_delims],
known_failures =
[(Unprovable, "SZS status: CounterSatisfiable"),
@@ -146,7 +149,7 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- default_max_relevant_per_iter = 50 (* FIXME *),
+ default_max_relevant_per_iter = 60 (* FUDGE *),
default_theory_relevant = false,
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -159,12 +162,11 @@
val spass_config : prover_config =
{exec = ("ISABELLE_ATP", "scripts/spass"),
required_execs = [("SPASS_HOME", "SPASS")],
- (* "div 2" accounts for the fact that SPASS is often run twice. *)
arguments = fn complete => fn timeout =>
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
- \-VarWeight=3 -TimeLimit=" ^
- string_of_int ((to_generous_secs timeout + 1) div 2))
+ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
|> not complete ? prefix "-SOS=1 ",
+ has_incomplete_mode = true,
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
known_perl_failures @
@@ -174,7 +176,7 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg")],
- default_max_relevant_per_iter = 35 (* FIXME *),
+ default_max_relevant_per_iter = 32 (* FUDGE *),
default_theory_relevant = true,
explicit_forall = true,
use_conjecture_for_hypotheses = true}
@@ -190,6 +192,7 @@
arguments = fn _ => fn timeout =>
"--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
" --thanks Andrei --input_file",
+ has_incomplete_mode = false,
proof_delims =
[("=========== Refutation ==========",
"======= End of refutation ======="),
@@ -200,8 +203,9 @@
(IncompleteUnprovable, "CANNOT PROVE"),
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
+ (Unprovable, "Termination reason: Satisfiable"),
(VampireTooOld, "not a valid option")],
- default_max_relevant_per_iter = 45 (* FIXME *),
+ default_max_relevant_per_iter = 45 (* FUDGE *),
default_theory_relevant = false,
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -242,6 +246,7 @@
arguments = fn _ => fn timeout =>
" -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
the_system system_prefix,
+ has_incomplete_mode = false,
proof_delims = insert (op =) tstp_proof_delims proof_delims,
known_failures =
known_failures @ known_perl_failures @
@@ -274,10 +279,10 @@
val remote_vampire = remotify_prover vampire "Vampire---9"
val remote_sine_e =
remote_prover "sine_e" "SInE---" []
- [(Unprovable, "says Unknown")] 150 (* FIXME *) false true
+ [(Unprovable, "says Unknown")] 150 (* FUDGE *) false true
val remote_snark =
remote_prover "snark" "SNARK---" [("refutation.", "end_refutation.")] []
- 50 (* FIXME *) false true
+ 50 (* FUDGE *) false true
(* Setup *)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 23 17:46:13 2010 +0200
@@ -141,7 +141,6 @@
hol_context -> bool -> styp -> int -> styp
val sel_no_from_name : string -> int
val close_form : term -> term
- val eta_expand : typ list -> term -> int -> term
val distinctness_formula : typ -> term list -> term
val register_frac_type :
string -> (string * string) list -> morphism -> Context.generic
@@ -919,14 +918,6 @@
| aux zs t = close_up zs (Term.add_vars t zs) t
in aux [] end
-fun eta_expand _ t 0 = t
- | eta_expand Ts (Abs (s, T, t')) n =
- Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
- | eta_expand Ts t n =
- fold_rev (curry3 Abs ("x" ^ nat_subscript n))
- (List.take (binder_types (fastype_of1 (Ts, t)), n))
- (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
-
fun distinctness_formula T =
all_distinct_unordered_pairs_of
#> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Aug 23 17:46:13 2010 +0200
@@ -52,6 +52,7 @@
val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
+ val nat_subscript : int -> string
val flip_polarity : polarity -> polarity
val prop_T : typ
val bool_T : typ
@@ -67,7 +68,7 @@
val monomorphic_term : Type.tyenv -> term -> term
val specialize_type : theory -> string * typ -> term -> term
val varify_type : Proof.context -> typ -> typ
- val nat_subscript : int -> string
+ val eta_expand : typ list -> term -> int -> term
val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
@@ -237,6 +238,18 @@
val parse_bool_option = Sledgehammer_Util.parse_bool_option
val parse_time_option = Sledgehammer_Util.parse_time_option
+val i_subscript = implode o map (prefix "\<^isub>") o explode
+fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
+fun nat_subscript n =
+ let val s = signed_string_of_int n in
+ if print_mode_active Symbol.xsymbolsN then
+ (* cheap trick to ensure proper alphanumeric ordering for one- and
+ two-digit numbers *)
+ (if n <= 9 then be_subscript else i_subscript) s
+ else
+ s
+ end
+
fun flip_polarity Pos = Neg
| flip_polarity Neg = Pos
| flip_polarity Neut = Neut
@@ -258,17 +271,7 @@
Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
|> snd |> the_single |> dest_Const |> snd
-val i_subscript = implode o map (prefix "\<^isub>") o explode
-fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
-fun nat_subscript n =
- let val s = signed_string_of_int n in
- if print_mode_active Symbol.xsymbolsN then
- (* cheap trick to ensure proper alphanumeric ordering for one- and
- two-digit numbers *)
- (if n <= 9 then be_subscript else i_subscript) s
- else
- s
- end
+val eta_expand = Sledgehammer_Util.eta_expand
fun time_limit NONE = I
| time_limit (SOME delay) = TimeLimit.timeLimit delay
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 23 17:46:13 2010 +0200
@@ -7,7 +7,6 @@
signature CLAUSIFIER =
sig
- val transform_elim_theorem : thm -> thm
val extensionalize_theorem : thm -> thm
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
@@ -25,7 +24,7 @@
(* Converts an elim-rule into an equivalent theorem that does not have the
predicate variable. Leaves other theorems unchanged. We simply instantiate
the conclusion variable to False. (Cf. "transform_elim_term" in
- "ATP_Systems".) *)
+ "Sledgehammer_Util".) *)
fun transform_elim_theorem th =
case concl_of th of (*conclusion variable*)
@{const Trueprop} $ (v as Var (_, @{typ bool})) =>
@@ -78,10 +77,6 @@
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
-(*Returns the vars of a theorem*)
-fun vars_of_thm th =
- map (cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
-
val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
(* Removes the lambdas from an equation of the form "t = (%x. u)".
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Aug 23 17:46:13 2010 +0200
@@ -99,7 +99,7 @@
(@{const_name "op &"}, "and"),
(@{const_name "op |"}, "or"),
(@{const_name "op -->"}, "implies"),
- (@{const_name Set.member}, "in"),
+ (@{const_name Set.member}, "member"),
(@{const_name fequal}, "fequal"),
(@{const_name COMBI}, "COMBI"),
(@{const_name COMBK}, "COMBK"),
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 23 17:46:13 2010 +0200
@@ -775,9 +775,6 @@
[])
end;
-val type_has_top_sort =
- exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-
(* Extensionalize "th", because that makes sense and that's what Sledgehammer
does, but also keep an unextensionalized version of "th" for backward
compatibility. *)
@@ -794,6 +791,9 @@
#> map Clausifier.introduce_combinators_in_theorem
#> Meson.finish_cnf
+val type_has_top_sort =
+ exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+
fun generic_metis_tac mode ctxt ths i st0 =
let
val _ = trace_msg (fn () =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 23 17:46:13 2010 +0200
@@ -207,8 +207,8 @@
(* generic TPTP-based provers *)
fun prover_fun atp_name
- {exec, required_execs, arguments, proof_delims, known_failures,
- default_max_relevant_per_iter, default_theory_relevant,
+ {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
+ known_failures, default_max_relevant_per_iter, default_theory_relevant,
explicit_forall, use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
relevance_threshold, relevance_convergence,
@@ -260,7 +260,7 @@
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
(* write out problem file and call prover *)
- fun command_line complete probfile =
+ fun command_line complete timeout probfile =
let
val core = File.shell_path command ^ " " ^ arguments complete timeout ^
" " ^ File.shell_path probfile
@@ -288,9 +288,9 @@
| [] =>
if File.exists command then
let
- fun do_run complete =
+ fun do_run complete timeout =
let
- val command = command_line complete probfile
+ val command = command_line complete timeout probfile
val ((output, msecs), res_code) =
bash_output command
|>> (if overlord then
@@ -316,13 +316,20 @@
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
|> map single
val _ = print_d (fn () => "Running " ^ quote atp_name ^ "...")
+ val timer = Timer.startRealTimer ()
val result =
- do_run false
- |> (fn (_, msecs0, _, SOME _) =>
- do_run true
- |> (fn (output, msecs, proof, outcome) =>
- (output, msecs0 + msecs, proof, outcome))
- | result => result)
+ do_run false (if has_incomplete_mode then
+ Time.fromMilliseconds
+ (2 * Time.toMilliseconds timeout div 3)
+ else
+ timeout)
+ |> has_incomplete_mode
+ ? (fn (_, msecs0, _, SOME _) =>
+ do_run true
+ (Time.- (timeout, Timer.checkRealTimer timer))
+ |> (fn (output, msecs, proof, outcome) =>
+ (output, msecs0 + msecs, proof, outcome))
+ | result => result)
in ((pool, conjecture_shape, axiom_names), result) end
else
error ("Bad executable: " ^ Path.implode command ^ ".")
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 23 17:46:13 2010 +0200
@@ -23,6 +23,8 @@
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
struct
+open Sledgehammer_Util
+
val trace = Unsynchronized.ref false
fun trace_msg msg = if !trace then tracing (msg ()) else ()
@@ -43,7 +45,7 @@
val name = Facts.string_of_ref xref
|> forall (member Thm.eq_thm chained_ths) ths
? prefix chained_prefix
- in (name, ths |> map Clausifier.transform_elim_theorem) end
+ in (name, ths) end
(***************************************************************)
@@ -84,11 +86,10 @@
Symtab.map_default (c, [ctyps])
(fn [] => [] | ctypss => insert (op =) ctyps ctypss)
-val fresh_prefix = "Sledgehammer.Fresh."
+val fresh_prefix = "Sledgehammer.FRESH."
val flip = Option.map not
(* These are typically simplified away by "Meson.presimplify". *)
-val boring_consts =
- [@{const_name If}, @{const_name Let} (* TODO: , @{const_name Set.member}, @{const_name Collect} *)]
+val boring_consts = [@{const_name If}, @{const_name Let}]
fun get_consts_typs thy pos ts =
let
@@ -100,10 +101,7 @@
Const x => add_const_type_to_table (const_with_typ thy x)
| Free (s, _) => add_const_type_to_table (s, [])
| t1 $ t2 => do_term t1 #> do_term t2
- | Abs (_, _, t) =>
- (* Abstractions lead to combinators, so we add a penalty for them. *)
- add_const_type_to_table (gensym fresh_prefix, [])
- #> do_term t
+ | Abs (_, _, t') => do_term t'
| _ => I
fun do_quantifier will_surely_be_skolemized body_t =
do_formula pos body_t
@@ -424,7 +422,7 @@
val exists_sledgehammer_const =
exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
-fun is_strange_thm th =
+fun is_strange_theorem th =
case head_of (concl_of th) of
Const (a, _) => (a <> @{const_name Trueprop} andalso
a <> @{const_name "=="})
@@ -490,29 +488,37 @@
are omitted. *)
fun is_dangerous_term full_types t =
not full_types andalso
- (has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t)
+ ((has_bound_or_var_of_type dangerous_types t andalso
+ has_bound_or_var_of_type dangerous_types (transform_elim_term t))
+ orelse is_exhaustive_finite t)
fun is_theorem_bad_for_atps full_types thm =
let val t = prop_of thm in
is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
- is_strange_thm thm
+ is_strange_theorem thm
end
fun all_name_thms_pairs ctxt full_types add_thms chained_ths =
let
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
- val local_facts = ProofContext.facts_of ctxt;
+ val local_facts = ProofContext.facts_of ctxt
+ val named_locals = local_facts |> Facts.dest_static []
+ val unnamed_locals =
+ local_facts |> Facts.props
+ |> filter_out (fn th => exists (fn (_, ths) => member Thm.eq_thm ths th)
+ named_locals)
+ |> map (pair "" o single)
val full_space =
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
-
- fun valid_facts facts =
- (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
- if (Facts.is_concealed facts name orelse
+ fun valid_facts facts pairs =
+ (pairs, []) |-> fold (fn (name, ths0) =>
+ if name <> "" andalso
+ forall (not o member Thm.eq_thm add_thms) ths0 andalso
+ (Facts.is_concealed facts name orelse
(respect_no_atp andalso is_package_def name) orelse
member (op =) multi_base_blacklist (Long_Name.base_name name) orelse
- String.isSuffix "_def_raw" (* FIXME: crude hack *) name) andalso
- forall (not o member Thm.eq_thm add_thms) ths0 then
+ String.isSuffix "_def_raw" (* FIXME: crude hack *) name) then
I
else
let
@@ -523,17 +529,25 @@
val name1 = Facts.extern facts name;
val name2 = Name_Space.extern full_space name;
val ths =
- ths0 |> map Clausifier.transform_elim_theorem
- |> filter ((not o is_theorem_bad_for_atps full_types) orf
- member Thm.eq_thm add_thms)
+ ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf
+ member Thm.eq_thm add_thms)
+ val name' =
+ case find_first check_thms [name1, name2, name] of
+ SOME name' => name'
+ | NONE =>
+ ths |> map (fn th =>
+ "`" ^ Print_Mode.setmp [Print_Mode.input]
+ (Syntax.string_of_term ctxt)
+ (prop_of th) ^ "`")
+ |> space_implode " "
in
- case find_first check_thms [name1, name2, name] of
- NONE => I
- | SOME name' =>
- cons (name' |> forall (member Thm.eq_thm chained_ths) ths
- ? prefix chained_prefix, ths)
+ cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
+ ? prefix chained_prefix, ths)
end)
- in valid_facts global_facts @ valid_facts local_facts end;
+ in
+ valid_facts local_facts (unnamed_locals @ named_locals) @
+ valid_facts global_facts (Facts.dest_static [] global_facts)
+ end
fun multi_name a th (n, pairs) =
(n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 23 17:46:13 2010 +0200
@@ -119,8 +119,12 @@
@{const Not} $ t1 => @{const Not} $ aux Ts t1
| (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name All}, _)) $ t1 =>
+ aux Ts (t0 $ eta_expand Ts t1 1)
| (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
+ aux Ts (t0 $ eta_expand Ts t1 1)
| (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
@@ -175,8 +179,10 @@
let
val thy = ProofContext.theory_of ctxt
val t = t |> Envir.beta_eta_contract
+ |> transform_elim_term
|> atomize_term
- val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
+ val need_trueprop = (fastype_of t = HOLogic.boolT)
+ val t = t |> need_trueprop ? HOLogic.mk_Trueprop
|> extensionalize_term
|> presimp ? presimplify_term thy
|> perhaps (try (HOLogic.dest_Trueprop))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Aug 23 17:46:13 2010 +0200
@@ -16,6 +16,8 @@
val unyxml : string -> string
val maybe_quote : string -> string
val monomorphic_term : Type.tyenv -> term -> term
+ val eta_expand : typ list -> term -> int -> term
+ val transform_elim_term : term -> term
val specialize_type : theory -> (string * typ) -> term -> term
val subgoal_count : Proof.state -> int
val strip_subgoal : thm -> int -> (string * typ) list * term list * term
@@ -107,6 +109,25 @@
| NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
\variable", [t]))) t
+fun eta_expand _ t 0 = t
+ | eta_expand Ts (Abs (s, T, t')) n =
+ Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
+ | eta_expand Ts t n =
+ fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t'))
+ (List.take (binder_types (fastype_of1 (Ts, t)), n))
+ (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
+
+(* Converts an elim-rule into an equivalent theorem that does not have the
+ predicate variable. Leaves other theorems unchanged. We simply instantiate
+ the conclusion variable to False. (Cf. "transform_elim_theorem" in
+ "Clausifier".) *)
+fun transform_elim_term t =
+ case Logic.strip_imp_concl t of
+ @{const Trueprop} $ Var (z, @{typ bool}) =>
+ subst_Vars [(z, @{const False})] t
+ | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
+ | _ => t
+
fun specialize_type thy (s, T) t =
let
fun subst_for (Const (s', T')) =
--- a/src/HOL/Transcendental.thy Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Transcendental.thy Mon Aug 23 17:46:13 2010 +0200
@@ -2790,7 +2790,7 @@
lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\<bar>x\<bar> < 1" shows "x^2 < 1"
proof -
- from mult_mono1[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
+ from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
have "\<bar> x^2 \<bar> < 1" using `\<bar> x \<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto
thus ?thesis using zero_le_power2 by auto
qed