# HG changeset patch
# User huffman
# Date 1267984996 28800
# Node ID e0b2a6e773db7d45fd842b76c9c779b942477a1d
# Parent  fe9b43a08187c444a67e9f56197317de72484074# Parent  f1456d045151406ef0da6f085493b398acb34cfa
merged

diff -r f1456d045151 -r e0b2a6e773db src/HOL/Complete_Lattice.thy
--- 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
diff -r f1456d045151 -r e0b2a6e773db src/HOL/Int.thy
--- 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))"
diff -r f1456d045151 -r e0b2a6e773db src/HOL/Nat.thy
--- 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
 
 
diff -r f1456d045151 -r e0b2a6e773db src/HOL/Nat_Numeral.thy
--- 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
 
diff -r f1456d045151 -r e0b2a6e773db src/HOL/Parity.thy
--- 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)
diff -r f1456d045151 -r e0b2a6e773db src/HOL/RealDef.thy
--- 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 *}
 
diff -r f1456d045151 -r e0b2a6e773db src/HOL/RealPow.thy
--- 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
diff -r f1456d045151 -r e0b2a6e773db src/HOL/Rings.thy
--- 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.*}
 
diff -r f1456d045151 -r e0b2a6e773db src/HOL/Tools/arith_data.ML
--- 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;
 
diff -r f1456d045151 -r e0b2a6e773db src/HOLCF/Tools/Domain/domain_theorems.ML
--- 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