--- a/NEWS Thu Dec 02 15:09:02 2010 +0100
+++ b/NEWS Thu Dec 02 15:32:48 2010 +0100
@@ -92,6 +92,22 @@
*** HOL ***
+* Functions can be declared as coercions and type inference will add them
+as necessary upon input of a term. In Complex_Main, real :: nat => real
+and real :: int => real are declared as coercions. A new coercion function
+f is declared like this:
+
+declare [[coercion f]]
+
+To lift coercions through type constructors (eg from nat => real to
+nat list => real list), map functions can be declared, e.g.
+
+declare [[coercion_map map]]
+
+Currently coercion inference is activated only in theories including real
+numbers, i.e. descendants of Complex_Main. In other theories it needs to be
+loaded explicitly: uses "~~/src/Tools/subtyping.ML"
+
* Abandoned locales equiv, congruent and congruent2 for equivalence relations.
INCOMPATIBILITY: use equivI rather than equiv_intro (same for congruent(2)).
--- a/src/HOL/Complex_Main.thy Thu Dec 02 15:09:02 2010 +0100
+++ b/src/HOL/Complex_Main.thy Thu Dec 02 15:32:48 2010 +0100
@@ -10,9 +10,6 @@
Ln
Taylor
Deriv
-uses "~~/src/Tools/subtyping.ML"
begin
-setup Subtyping.setup
-
end
--- a/src/HOL/Ln.thy Thu Dec 02 15:09:02 2010 +0100
+++ b/src/HOL/Ln.thy Thu Dec 02 15:32:48 2010 +0100
@@ -9,13 +9,13 @@
begin
lemma exp_first_two_terms: "exp x = 1 + x + suminf (%n.
- inverse(real (fact (n+2))) * (x ^ (n+2)))"
+ inverse(fact (n+2)) * (x ^ (n+2)))"
proof -
- have "exp x = suminf (%n. inverse(real (fact n)) * (x ^ n))"
+ have "exp x = suminf (%n. inverse(fact n) * (x ^ n))"
by (simp add: exp_def)
- also from summable_exp have "... = (SUM n : {0..<2}.
- inverse(real (fact n)) * (x ^ n)) + suminf (%n.
- inverse(real (fact (n+2))) * (x ^ (n+2)))" (is "_ = ?a + _")
+ also from summable_exp have "... = (SUM n::nat : {0..<2}.
+ inverse(fact n) * (x ^ n)) + suminf (%n.
+ inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _")
by (rule suminf_split_initial_segment)
also have "?a = 1 + x"
by (simp add: numerals)
@@ -23,7 +23,7 @@
qed
lemma exp_tail_after_first_two_terms_summable:
- "summable (%n. inverse(real (fact (n+2))) * (x ^ (n+2)))"
+ "summable (%n. inverse(fact (n+2)) * (x ^ (n+2)))"
proof -
note summable_exp
thus ?thesis
@@ -31,20 +31,19 @@
qed
lemma aux1: assumes a: "0 <= x" and b: "x <= 1"
- shows "inverse (real (fact ((n::nat) + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
+ shows "inverse (fact ((n::nat) + 2)) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
proof (induct n)
- show "inverse (real (fact ((0::nat) + 2))) * x ^ (0 + 2) <=
+ show "inverse (fact ((0::nat) + 2)) * x ^ (0 + 2) <=
x ^ 2 / 2 * (1 / 2) ^ 0"
by (simp add: real_of_nat_Suc power2_eq_square)
next
fix n :: nat
- assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)
+ assume c: "inverse (fact (n + 2)) * x ^ (n + 2)
<= x ^ 2 / 2 * (1 / 2) ^ n"
- show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2)
+ show "inverse (fact (Suc n + 2)) * x ^ (Suc n + 2)
<= x ^ 2 / 2 * (1 / 2) ^ Suc n"
proof -
- have "inverse(real (fact (Suc n + 2))) <=
- (1 / 2) *inverse (real (fact (n+2)))"
+ have "inverse(fact (Suc n + 2)) <= (1/2) * inverse (fact (n+2))"
proof -
have "Suc n + 2 = Suc (n + 2)" by simp
then have "fact (Suc n + 2) = Suc (n + 2) * fact (n + 2)"
@@ -57,12 +56,12 @@
by (rule real_of_nat_mult)
finally have "real (fact (Suc n + 2)) =
real (Suc (n + 2)) * real (fact (n + 2))" .
- then have "inverse(real (fact (Suc n + 2))) =
- inverse(real (Suc (n + 2))) * inverse(real (fact (n + 2)))"
+ then have "inverse(fact (Suc n + 2)) =
+ inverse(Suc (n + 2)) * inverse(fact (n + 2))"
apply (rule ssubst)
apply (rule inverse_mult_distrib)
done
- also have "... <= (1/2) * inverse(real (fact (n + 2)))"
+ also have "... <= (1/2) * inverse(fact (n + 2))"
apply (rule mult_right_mono)
apply (subst inverse_eq_divide)
apply simp
@@ -78,8 +77,8 @@
apply (rule mult_nonneg_nonneg, rule a)+
apply (rule zero_le_power, rule a)
done
- ultimately have "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2) <=
- (1 / 2 * inverse (real (fact (n + 2)))) * x ^ (n + 2)"
+ ultimately have "inverse (fact (Suc n + 2)) * x ^ (Suc n + 2) <=
+ (1 / 2 * inverse (fact (n + 2))) * x ^ (n + 2)"
apply (rule mult_mono)
apply (rule mult_nonneg_nonneg)
apply simp
@@ -88,7 +87,7 @@
apply (rule zero_le_power)
apply (rule a)
done
- also have "... = 1 / 2 * (inverse (real (fact (n + 2))) * x ^ (n + 2))"
+ also have "... = 1 / 2 * (inverse (fact (n + 2)) * x ^ (n + 2))"
by simp
also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)"
apply (rule mult_left_mono)
@@ -122,12 +121,12 @@
proof -
assume a: "0 <= x"
assume b: "x <= 1"
- have c: "exp x = 1 + x + suminf (%n. inverse(real (fact (n+2))) *
+ have c: "exp x = 1 + x + suminf (%n. inverse(fact (n+2)) *
(x ^ (n+2)))"
by (rule exp_first_two_terms)
- moreover have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <= x^2"
+ moreover have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x^2"
proof -
- have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <=
+ have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <=
suminf (%n. (x^2/2) * ((1/2)^n))"
apply (rule summable_le)
apply (auto simp only: aux1 prems)
--- a/src/HOL/RealDef.thy Thu Dec 02 15:09:02 2010 +0100
+++ b/src/HOL/RealDef.thy Thu Dec 02 15:32:48 2010 +0100
@@ -9,6 +9,7 @@
theory RealDef
imports Rat
+uses "~~/src/Tools/subtyping.ML"
begin
text {*
@@ -1109,6 +1110,11 @@
real_of_nat_def [code_unfold]: "real == real_of_nat"
real_of_int_def [code_unfold]: "real == real_of_int"
+setup Subtyping.setup
+
+declare [[coercion "real::nat\<Rightarrow>real"]]
+declare [[coercion "real::int\<Rightarrow>real"]]
+
lemma real_eq_of_nat: "real = of_nat"
unfolding real_of_nat_def ..
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Dec 02 15:09:02 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Dec 02 15:32:48 2010 +0100
@@ -554,22 +554,32 @@
fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
fun replay_one_inference ctxt mode skolem_params (fol_th, inf) thpairs =
- let
- val _ = trace_msg ctxt (fn () => "=============================================")
- val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
- val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
- val th = step ctxt mode skolem_params thpairs (fol_th, inf)
- |> flexflex_first_order
- val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
- val _ = trace_msg ctxt (fn () => "=============================================")
- val num_metis_lits =
- fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList
- |> count is_metis_literal_genuine
- val num_isabelle_lits =
- th |> prems_of |> count is_isabelle_literal_genuine
- val _ = if num_metis_lits = num_isabelle_lits then ()
- else error "Cannot replay Metis proof in Isabelle: Out of sync."
- in (fol_th, th) :: thpairs end
+ if not (null thpairs) andalso prop_of (snd (hd thpairs)) aconv @{prop False} then
+ (* Isabelle sometimes identifies literals (premises) that are distinct in
+ Metis (e.g., because of type variables). We give the Isabelle proof the
+ benefice of the doubt. *)
+ thpairs
+ else
+ let
+ val _ = trace_msg ctxt
+ (fn () => "=============================================")
+ val _ = trace_msg ctxt
+ (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
+ val _ = trace_msg ctxt
+ (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
+ val th = step ctxt mode skolem_params thpairs (fol_th, inf)
+ |> flexflex_first_order
+ val _ = trace_msg ctxt
+ (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
+ val _ = trace_msg ctxt
+ (fn () => "=============================================")
+ val num_metis_lits =
+ count is_metis_literal_genuine
+ (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
+ val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)
+ val _ = if num_metis_lits >= num_isabelle_lits then ()
+ else error "Cannot replay Metis proof in Isabelle: Out of sync."
+ in (fol_th, th) :: thpairs end
fun term_instantiate thy = cterm_instantiate o map (pairself (cterm_of thy))