--- a/src/HOL/Complete_Lattice.thy Sun Mar 07 15:51:29 2010 +0100
+++ b/src/HOL/Complete_Lattice.thy Sun Mar 07 10:03:16 2010 -0800
@@ -82,6 +82,12 @@
"\<Squnion>UNIV = top"
by (simp add: Inf_Sup Inf_empty [symmetric])
+lemma Sup_le_iff: "Sup A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
+ by (auto intro: Sup_least dest: Sup_upper)
+
+lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
+ by (auto intro: Inf_greatest dest: Inf_lower)
+
definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
"SUPR A f = \<Squnion> (f ` A)"
@@ -126,6 +132,12 @@
lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (INF i:A. M i)"
by (auto simp add: INFI_def intro: Inf_greatest)
+lemma SUP_le_iff: "(SUP i:A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
+ unfolding SUPR_def by (auto simp add: Sup_le_iff)
+
+lemma le_INF_iff: "u \<sqsubseteq> (INF i:A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
+ unfolding INFI_def by (auto simp add: le_Inf_iff)
+
lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
by (auto intro: antisym SUP_leI le_SUPI)
@@ -384,7 +396,7 @@
by blast
lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
- by blast
+ by (fact SUP_le_iff)
lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
by blast
@@ -591,7 +603,7 @@
by blast
lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
- by blast
+ by (fact le_INF_iff)
lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
by blast
--- a/src/HOL/Int.thy Sun Mar 07 15:51:29 2010 +0100
+++ b/src/HOL/Int.thy Sun Mar 07 10:03:16 2010 -0800
@@ -1262,6 +1262,15 @@
notation (xsymbols)
Ints ("\<int>")
+lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
+ by (simp add: Ints_def)
+
+lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
+apply (simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_of_nat_eq [symmetric])
+done
+
lemma Ints_0 [simp]: "0 \<in> \<int>"
apply (simp add: Ints_def)
apply (rule range_eqI)
@@ -1286,12 +1295,21 @@
apply (rule of_int_minus [symmetric])
done
+lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_diff [symmetric])
+done
+
lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
apply (auto simp add: Ints_def)
apply (rule range_eqI)
apply (rule of_int_mult [symmetric])
done
+lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
+by (induct n) simp_all
+
lemma Ints_cases [cases set: Ints]:
assumes "q \<in> \<int>"
obtains (of_int) z where "q = of_int z"
@@ -1308,12 +1326,6 @@
end
-lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a-b \<in> \<int>"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_diff [symmetric])
-done
-
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
lemma Ints_double_eq_0_iff:
@@ -1350,10 +1362,15 @@
qed
qed
-lemma Ints_number_of:
+lemma Ints_number_of [simp]:
"(number_of w :: 'a::number_ring) \<in> Ints"
unfolding number_of_eq Ints_def by simp
+lemma Nats_number_of [simp]:
+ "Int.Pls \<le> w \<Longrightarrow> (number_of w :: 'a::number_ring) \<in> Nats"
+unfolding Int.Pls_def number_of_eq
+by (simp only: of_nat_nat [symmetric] of_nat_in_Nats)
+
lemma Ints_odd_less_0:
assumes in_Ints: "a \<in> Ints"
shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
--- a/src/HOL/Nat.thy Sun Mar 07 15:51:29 2010 +0100
+++ b/src/HOL/Nat.thy Sun Mar 07 10:03:16 2010 -0800
@@ -1400,6 +1400,20 @@
apply (rule of_nat_mult [symmetric])
done
+lemma Nats_cases [cases set: Nats]:
+ assumes "x \<in> \<nat>"
+ obtains (of_nat) n where "x = of_nat n"
+ unfolding Nats_def
+proof -
+ from `x \<in> \<nat>` have "x \<in> range of_nat" unfolding Nats_def .
+ then obtain n where "x = of_nat n" ..
+ then show thesis ..
+qed
+
+lemma Nats_induct [case_names of_nat, induct set: Nats]:
+ "x \<in> \<nat> \<Longrightarrow> (\<And>n. P (of_nat n)) \<Longrightarrow> P x"
+ by (rule Nats_cases) auto
+
end
--- a/src/HOL/Nat_Numeral.thy Sun Mar 07 15:51:29 2010 +0100
+++ b/src/HOL/Nat_Numeral.thy Sun Mar 07 10:03:16 2010 -0800
@@ -113,7 +113,7 @@
end
-context linordered_ring_strict
+context linordered_ring
begin
lemma sum_squares_ge_zero:
@@ -124,6 +124,11 @@
"\<not> x * x + y * y < 0"
by (simp add: not_less sum_squares_ge_zero)
+end
+
+context linordered_ring_strict
+begin
+
lemma sum_squares_eq_zero_iff:
"x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
by (simp add: add_nonneg_eq_0_iff)
@@ -134,14 +139,7 @@
lemma sum_squares_gt_zero_iff:
"0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
-proof -
- have "x * x + y * y \<noteq> 0 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
- by (simp add: sum_squares_eq_zero_iff)
- then have "0 \<noteq> x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
- by auto
- then show ?thesis
- by (simp add: less_le sum_squares_ge_zero)
-qed
+ by (simp add: not_le [symmetric] sum_squares_le_zero_iff)
end
--- a/src/HOL/Parity.thy Sun Mar 07 15:51:29 2010 +0100
+++ b/src/HOL/Parity.thy Sun Mar 07 10:03:16 2010 -0800
@@ -218,7 +218,7 @@
done
lemma zero_le_even_power: "even n ==>
- 0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n"
+ 0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
apply (simp add: even_nat_equiv_def2)
apply (erule exE)
apply (erule ssubst)
--- a/src/HOL/RealDef.thy Sun Mar 07 15:51:29 2010 +0100
+++ b/src/HOL/RealDef.thy Sun Mar 07 10:03:16 2010 -0800
@@ -701,6 +701,9 @@
lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x"
by (insert real_of_int_div2 [of n x], simp)
+lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints"
+unfolding real_of_int_def by (rule Ints_of_int)
+
subsection{*Embedding the Naturals into the Reals*}
@@ -852,6 +855,12 @@
apply (simp only: real_of_int_real_of_nat)
done
+lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
+unfolding real_of_nat_def by (rule of_nat_in_Nats)
+
+lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints"
+unfolding real_of_nat_def by (rule Ints_of_nat)
+
subsection{* Rationals *}
--- a/src/HOL/RealPow.thy Sun Mar 07 15:51:29 2010 +0100
+++ b/src/HOL/RealPow.thy Sun Mar 07 10:03:16 2010 -0800
@@ -24,71 +24,76 @@
apply (rule two_realpow_ge_one)
done
-lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma realpow_Suc_le_self:
+ fixes r :: "'a::linordered_semidom"
+ shows "[| 0 \<le> r; r \<le> 1 |] ==> r ^ Suc n \<le> r"
by (insert power_decreasing [of 1 "Suc n" r], simp)
-lemma realpow_minus_mult [rule_format]:
- "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
-apply (simp split add: nat_diff_split)
-done
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma realpow_minus_mult:
+ fixes x :: "'a::monoid_mult"
+ shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
+by (simp add: power_commutes split add: nat_diff_split)
+(* TODO: no longer real-specific; rename and move elsewhere *)
lemma realpow_two_diff:
- "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
+ fixes x :: "'a::comm_ring_1"
+ shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
by (simp add: algebra_simps)
+(* TODO: move elsewhere *)
+lemma add_eq_0_iff:
+ fixes x y :: "'a::group_add"
+ shows "x + y = 0 \<longleftrightarrow> y = - x"
+by (auto dest: minus_unique)
+
+(* TODO: no longer real-specific; rename and move elsewhere *)
lemma realpow_two_disj:
- "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
-apply (cut_tac x = x and y = y in realpow_two_diff)
-apply auto
-done
+ fixes x :: "'a::idom"
+ shows "(x^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
+using realpow_two_diff [of x y]
+by (auto simp add: add_eq_0_iff)
subsection{* Squares of Reals *}
+(* FIXME: declare this [simp] for all types, or not at all *)
lemma real_two_squares_add_zero_iff [simp]:
"(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
by (rule sum_squares_eq_zero_iff)
-lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
-by simp
-
-lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
-by simp
-
-lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
-by (simp add: real_add_eq_0_iff [symmetric])
-
-lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
-by (simp add: left_distrib right_diff_distrib)
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma real_squared_diff_one_factored:
+ fixes x :: "'a::ring_1"
+ shows "x * x - 1 = (x + 1) * (x - 1)"
+by (simp add: algebra_simps)
-lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)"
-apply auto
-apply (drule right_minus_eq [THEN iffD2])
-apply (auto simp add: real_squared_diff_one_factored)
-done
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma real_mult_is_one [simp]:
+ fixes x :: "'a::ring_1_no_zero_divisors"
+ shows "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
+proof -
+ have "x * x = 1 \<longleftrightarrow> (x + 1) * (x - 1) = 0"
+ by (simp add: algebra_simps)
+ also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1"
+ by (auto simp add: add_eq_0_iff minus_equation_iff [of _ 1])
+ finally show ?thesis .
+qed
-lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)"
-by simp
-
-lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)"
-by simp
-
+(* FIXME: declare this [simp] for all types, or not at all *)
lemma realpow_two_sum_zero_iff [simp]:
"(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
by (rule sum_power2_eq_zero_iff)
+(* FIXME: declare this [simp] for all types, or not at all *)
lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
by (rule sum_power2_ge_zero)
+(* FIXME: declare this [simp] for all types, or not at all *)
lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
by (intro add_nonneg_nonneg zero_le_power2)
-lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
-by (simp add: sum_squares_gt_zero_iff)
-
-lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y"
-by (simp add: sum_squares_gt_zero_iff)
-
lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
by (rule_tac j = 0 in real_le_trans, auto)
@@ -96,8 +101,9 @@
by (auto simp add: power2_eq_square)
(* The following theorem is by Benjamin Porter *)
+(* TODO: no longer real-specific; rename and move elsewhere *)
lemma real_sq_order:
- fixes x::real
+ fixes x :: "'a::linordered_semidom"
assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
shows "x \<le> y"
proof -
@@ -150,8 +156,11 @@
apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
done
-lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
-by (case_tac "n", auto)
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma realpow_num_eq_if:
+ fixes m :: "'a::power"
+ shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
+by (cases n, auto)
end
--- a/src/HOL/Rings.thy Sun Mar 07 15:51:29 2010 +0100
+++ b/src/HOL/Rings.thy Sun Mar 07 10:03:16 2010 -0800
@@ -796,6 +796,13 @@
auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
qed (auto simp add: abs_if)
+lemma zero_le_square [simp]: "0 \<le> a * a"
+ using linear [of 0 a]
+ by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
+
+lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
+ by (simp add: not_less)
+
end
(* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
@@ -873,12 +880,6 @@
apply force
done
-lemma zero_le_square [simp]: "0 \<le> a * a"
-by (simp add: zero_le_mult_iff linear)
-
-lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
-by (simp add: not_less)
-
text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
also with the relations @{text "\<le>"} and equality.*}
--- a/src/HOL/Tools/arith_data.ML Sun Mar 07 15:51:29 2010 +0100
+++ b/src/HOL/Tools/arith_data.ML Sun Mar 07 10:03:16 2010 -0800
@@ -55,7 +55,7 @@
let
val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt
fun invoke (_, (name, tac)) k st = (if verbose
- then warning ("Trying " ^ name ^ "...") else ();
+ then priority ("Trying " ^ name ^ "...") else ();
tac verbose ctxt k st);
in FIRST' (map invoke (rev tactics)) end;
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sun Mar 07 15:51:29 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sun Mar 07 10:03:16 2010 -0800
@@ -168,13 +168,17 @@
val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
end;
+val case_ns =
+ "bottom" :: map (fn (b,_,_) => Binding.name_of b) (snd dom_eqn);
+
in
thy
|> Sign.add_path (Long_Name.base_name dname)
|> snd o PureThy.add_thmss [
((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]),
((Binding.name "exhaust" , [exhaust] ), []),
- ((Binding.name "casedist" , [casedist] ), [Induct.cases_type dname]),
+ ((Binding.name "casedist" , [casedist] ),
+ [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
((Binding.name "when_rews" , when_rews ), [Simplifier.simp_add]),
((Binding.name "compacts" , con_compacts), [Simplifier.simp_add]),
((Binding.name "con_rews" , con_rews ),
@@ -422,8 +426,20 @@
| ERROR _ =>
(warning "Cannot prove induction rule"; ([], TrueI));
+val case_ns =
+ let
+ val bottoms =
+ if length dnames = 1 then ["bottom"] else
+ map (fn s => "bottom_" ^ Long_Name.base_name s) dnames;
+ fun one_eq bot (_,cons) =
+ bot :: map (fn (c,_) => Long_Name.base_name c) cons;
+ in flat (map2 one_eq bottoms eqs) end;
+
val inducts = Project_Rule.projections (ProofContext.init thy) ind;
-fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
+fun ind_rule (dname, rule) =
+ ((Binding.empty, [rule]),
+ [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
+
val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
in thy |> Sign.add_path comp_dnam