various localizations

--- a/src/HOL/IntDef.thy	Thu Oct 25 16:57:57 2007 +0200
+++ b/src/HOL/IntDef.thy	Thu Oct 25 19:27:50 2007 +0200
@@ -426,8 +426,11 @@
 
 subsection{*Embedding of the Integers into any @{text ring_1}: @{term of_int}*}
 
+context ring_1
+begin
+
 definition
-  of_int :: "int \<Rightarrow> 'a\<Colon>ring_1"
+  of_int :: "int \<Rightarrow> 'a"
 where
   "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
 lemmas [code func del] = of_int_def
@@ -453,15 +456,21 @@
 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
 by (cases z, simp add: compare_rls of_int minus)
 
-lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z"
-by (simp add: diff_minus)
-
 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
 apply (cases w, cases z)
 apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
                  mult add_ac of_nat_mult)
 done
 
+text{*Collapse nested embeddings*}
+lemma of_int_of_nat_eq [simp]: "of_int (Nat.of_nat n) = of_nat n"
+  by (induct n, auto)
+
+end
+
+lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z"
+by (simp add: diff_minus)
+
 lemma of_int_le_iff [simp]:
      "(of_int w \<le> (of_int z::'a::ordered_idom)) = (w \<le> z)"
 apply (cases w)
@@ -474,7 +483,6 @@
 lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]
 lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]
 
-
 lemma of_int_less_iff [simp]:
      "(of_int w < (of_int z::'a::ordered_idom)) = (w < z)"
 by (simp add: linorder_not_le [symmetric])
@@ -486,83 +494,83 @@
 text{*Class for unital rings with characteristic zero.
  Includes non-ordered rings like the complex numbers.*}
 class ring_char_0 = ring_1 + semiring_char_0
+begin
 
 lemma of_int_eq_iff [simp]:
-   "of_int w = (of_int z \<Colon> 'a\<Colon>ring_char_0) \<longleftrightarrow> w = z"
+   "of_int w = of_int z \<longleftrightarrow> w = z"
 apply (cases w, cases z, simp add: of_int)
 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
 done
 
-text{*Every @{text ordered_idom} has characteristic zero.*}
-instance ordered_idom < ring_char_0 ..
-
 text{*Special cases where either operand is zero*}
 lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
 lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified]
 
-lemma of_int_eq_id [simp]: "of_int = (id :: int => int)"
+end
+
+text{*Every @{text ordered_idom} has characteristic zero.*}
+instance ordered_idom \<subseteq> ring_char_0 ..
+
+lemma of_int_eq_id [simp]: "of_int = id"
 proof
-  fix z
-  show "of_int z = id z"
-    by (cases z)
-      (simp add: of_int add minus int_def diff_minus)
+  fix z show "of_int z = id z"
+    by (cases z) (simp add: of_int add minus int_def diff_minus)
 qed
 
-lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
+lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
 by (cases z rule: eq_Abs_Integ)
    (simp add: nat le of_int Zero_int_def of_nat_diff)
 
 
 subsection{*The Set of Integers*}
 
-constdefs
-  Ints  :: "'a::ring_1 set"
-  "Ints == range of_int"
+context ring_1
+begin
+
+definition
+  Ints  :: "'a set"
+where
+  "Ints = range of_int"
+
+end
 
 notation (xsymbols)
   Ints  ("\<int>")
 
-lemma Ints_0 [simp]: "0 \<in> Ints"
+context ring_1
+begin
+
+lemma Ints_0 [simp]: "0 \<in> \<int>"
 apply (simp add: Ints_def)
 apply (rule range_eqI)
 apply (rule of_int_0 [symmetric])
 done
 
-lemma Ints_1 [simp]: "1 \<in> Ints"
+lemma Ints_1 [simp]: "1 \<in> \<int>"
 apply (simp add: Ints_def)
 apply (rule range_eqI)
 apply (rule of_int_1 [symmetric])
 done
 
-lemma Ints_add [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a+b \<in> Ints"
+lemma Ints_add [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_add [symmetric])
 done
 
-lemma Ints_minus [simp]: "a \<in> Ints ==> -a \<in> Ints"
+lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
 apply (auto simp add: Ints_def)
 apply (rule range_eqI)
 apply (rule of_int_minus [symmetric])
 done
 
-lemma Ints_diff [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a-b \<in> Ints"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_diff [symmetric])
-done
-
-lemma Ints_mult [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a*b \<in> Ints"
+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
 
-text{*Collapse nested embeddings*}
-lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
-by (induct n, auto)
-
 lemma Ints_cases [cases set: Ints]:
   assumes "q \<in> \<int>"
   obtains (of_int) z where "q = of_int z"
@@ -574,9 +582,17 @@
 qed
 
 lemma Ints_induct [case_names of_int, induct set: Ints]:
-  "q \<in> \<int> ==> (!!z. P (of_int z)) ==> P q"
+  "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
   by (rule Ints_cases) auto
 
+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
+
 
 subsection {* @{term setsum} and @{term setprod} *}
 

--- a/src/HOL/Nat.thy	Thu Oct 25 16:57:57 2007 +0200
+++ b/src/HOL/Nat.thy	Thu Oct 25 19:27:50 2007 +0200
@@ -1147,8 +1147,8 @@
   using Suc_le_eq less_Suc_eq_le by simp_all
 
 
-subsection{*Embedding of the Naturals into any
-  @{text semiring_1}: @{term of_nat}*}
+subsection {* Embedding of the Naturals into any
+  @{text semiring_1}: @{term of_nat} *}
 
 context semiring_1
 begin
@@ -1156,8 +1156,102 @@
 definition
   of_nat_def: "of_nat = nat_rec 0 (\<lambda>_. (op +) 1)"
 
+lemma of_nat_simps [simp, code]:
+  shows of_nat_0:   "of_nat 0 = 0"
+    and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
+  unfolding of_nat_def by simp_all
+
+lemma of_nat_1 [simp]: "of_nat 1 = 1"
+  by simp
+
+lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
+  by (induct m) (simp_all add: add_ac)
+
+lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
+  by (induct m) (simp_all add: add_ac left_distrib)
+
 end
 
+context ordered_semidom
+begin
+
+lemma zero_le_imp_of_nat: "0 \<le> of_nat m"
+  apply (induct m, simp_all)
+  apply (erule order_trans)
+  apply (rule ord_le_eq_trans [OF _ add_commute])
+  apply (rule less_add_one [THEN less_imp_le])
+  done
+
+lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
+  apply (induct m n rule: diff_induct, simp_all)
+  apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
+  done
+
+lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
+  apply (induct m n rule: diff_induct, simp_all)
+  apply (insert zero_le_imp_of_nat)
+  apply (force simp add: not_less [symmetric])
+  done
+
+lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
+  by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
+
+text{*Special cases where either operand is zero*}
+
+lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
+  by (rule of_nat_less_iff [of 0, simplified])
+
+lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
+  by (rule of_nat_less_iff [of _ 0, simplified])
+
+lemma of_nat_le_iff [simp]:
+  "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
+  by (simp add: not_less [symmetric] linorder_not_less [symmetric])
+
+text{*Special cases where either operand is zero*}
+
+lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
+  by (rule of_nat_le_iff [of 0, simplified])
+
+lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
+  by (rule of_nat_le_iff [of _ 0, simplified])
+
+end
+
+lemma of_nat_id [simp]: "of_nat n = n"
+  by (induct n) auto
+
+lemma of_nat_eq_id [simp]: "of_nat = id"
+  by (auto simp add: expand_fun_eq)
+
+text{*Class for unital semirings with characteristic zero.
+ Includes non-ordered rings like the complex numbers.*}
+
+class semiring_char_0 = semiring_1 +
+  assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
+
+text{*Every @{text ordered_semidom} has characteristic zero.*}
+
+subclass (in ordered_semidom) semiring_char_0
+  by unfold_locales (simp add: eq_iff order_eq_iff)
+
+context semiring_char_0
+begin
+
+text{*Special cases where either operand is zero*}
+
+lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
+  by (rule of_nat_eq_iff [of 0, simplified])
+
+lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
+  by (rule of_nat_eq_iff [of _ 0, simplified])
+
+lemma inj_of_nat: "inj of_nat"
+  by (simp add: inj_on_def)
+
+end
+
+
 subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
 
 lemma subst_equals:
@@ -1165,7 +1259,6 @@
   shows "u = s"
   using 2 1 by (rule trans)
 
-
 use "arith_data.ML"
 declaration {* K arith_data_setup *}
 
@@ -1186,6 +1279,18 @@
     -- {* elimination of @{text -} on @{text nat} *}
 by (cases "a<b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
 
+context ring_1
+begin
+
+lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
+  by (simp del: of_nat_add
+    add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
+
+end
+
+lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
+  by (rule of_nat_0_le_iff [THEN abs_of_nonneg])
+
 lemma nat_diff_split_asm:
   "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
     -- {* elimination of @{text -} on @{text nat} in assumptions *}
@@ -1333,141 +1438,52 @@
 Least_Suc}, since there appears to be no need.*}
 
 
-subsection{*Embedding of the Naturals into any
-  @{text semiring_1}: @{term of_nat}*}
+subsection {*The Set of Natural Numbers*}
 
 context semiring_1
 begin
 
-lemma of_nat_simps [simp, code]:
-  shows of_nat_0:   "of_nat 0 = 0"
-    and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
-  unfolding of_nat_def by simp_all
+definition
+  Nats  :: "'a set"
+where
+  "Nats = range of_nat"
 
 end
 
-lemma of_nat_id [simp]: "(of_nat n \<Colon> nat) = n"
-by (induct n) auto
-
-lemma of_nat_1 [simp]: "of_nat 1 = 1"
-by simp
-
-lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
-by (induct m) (simp_all add: add_ac)
-
-lemma of_nat_mult: "of_nat (m*n) = of_nat m * of_nat n"
-by (induct m) (simp_all add: add_ac left_distrib)
-
-lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
-  apply (induct m, simp_all)
-  apply (erule order_trans)
-  apply (rule ord_le_eq_trans [OF _ add_commute])
-  apply (rule less_add_one [THEN order_less_imp_le])
-  done
-
-lemma less_imp_of_nat_less:
-    "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
-  apply (induct m n rule: diff_induct, simp_all)
-  apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
-  done
-
-lemma of_nat_less_imp_less:
-    "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
-  apply (induct m n rule: diff_induct, simp_all)
-  apply (insert zero_le_imp_of_nat)
-  apply (force simp add: linorder_not_less [symmetric])
-  done
-
-lemma of_nat_less_iff [simp]:
-  "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
-by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
-
-text{*Special cases where either operand is zero*}
-
-lemma of_nat_0_less_iff [simp]: "((0::'a::ordered_semidom) < of_nat n) = (0 < n)"
-by (rule of_nat_less_iff [of 0, simplified])
-
-lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < (0::'a::ordered_semidom)"
-by (rule of_nat_less_iff [of _ 0, simplified])
-
-lemma of_nat_le_iff [simp]:
-  "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
-by (simp add: linorder_not_less [symmetric])
-
-text{*Special cases where either operand is zero*}
-lemma of_nat_0_le_iff [simp]: "(0::'a::ordered_semidom) \<le> of_nat n"
-by (rule of_nat_le_iff [of 0, simplified])
-lemma of_nat_le_0_iff [simp,noatp]: "(of_nat m \<le> (0::'a::ordered_semidom)) = (m = 0)"
-by (rule of_nat_le_iff [of _ 0, simplified])
-
-text{*Class for unital semirings with characteristic zero.
- Includes non-ordered rings like the complex numbers.*}
-
-class semiring_char_0 = semiring_1 +
-  assumes of_nat_eq_iff [simp]:
-    "of_nat m = of_nat n \<longleftrightarrow> m = n"
-
-text{*Every @{text ordered_semidom} has characteristic zero.*}
-instance ordered_semidom < semiring_char_0
-by intro_classes (simp add: order_eq_iff)
-
-text{*Special cases where either operand is zero*}
-lemma of_nat_0_eq_iff [simp,noatp]: "((0::'a::semiring_char_0) = of_nat n) = (0 = n)"
-by (rule of_nat_eq_iff [of 0, simplified])
-lemma of_nat_eq_0_iff [simp,noatp]: "(of_nat m = (0::'a::semiring_char_0)) = (m = 0)"
-by (rule of_nat_eq_iff [of _ 0, simplified])
-
-lemma inj_of_nat: "inj (of_nat :: nat \<Rightarrow> 'a::semiring_char_0)"
-by (simp add: inj_on_def)
-
-lemma of_nat_diff:
-  "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
-by (simp del: of_nat_add
-    add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
-
-lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
-by (rule of_nat_0_le_iff [THEN abs_of_nonneg])
-
-
-subsection {*The Set of Natural Numbers*}
-
-definition
-  Nats  :: "'a::semiring_1 set"
-where
-  "Nats = range of_nat"
-
 notation (xsymbols)
   Nats  ("\<nat>")
 
-lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
-by (simp add: Nats_def)
+context semiring_1
+begin
 
-lemma Nats_0 [simp]: "0 \<in> Nats"
+lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
+  by (simp add: Nats_def)
+
+lemma Nats_0 [simp]: "0 \<in> \<nat>"
 apply (simp add: Nats_def)
 apply (rule range_eqI)
 apply (rule of_nat_0 [symmetric])
 done
 
-lemma Nats_1 [simp]: "1 \<in> Nats"
+lemma Nats_1 [simp]: "1 \<in> \<nat>"
 apply (simp add: Nats_def)
 apply (rule range_eqI)
 apply (rule of_nat_1 [symmetric])
 done
 
-lemma Nats_add [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a+b \<in> Nats"
+lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>"
 apply (auto simp add: Nats_def)
 apply (rule range_eqI)
 apply (rule of_nat_add [symmetric])
 done
 
-lemma Nats_mult [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a*b \<in> Nats"
+lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>"
 apply (auto simp add: Nats_def)
 apply (rule range_eqI)
 apply (rule of_nat_mult [symmetric])
 done
 
-lemma of_nat_eq_id [simp]: "of_nat = (id :: nat => nat)"
-by (auto simp add: expand_fun_eq)
+end
 
 
 text {* the lattice order on @{typ nat} *}

--- a/src/HOL/Orderings.thy	Thu Oct 25 16:57:57 2007 +0200
+++ b/src/HOL/Orderings.thy	Thu Oct 25 19:27:50 2007 +0200
@@ -685,17 +685,22 @@
 
 subsection {* Transitivity reasoning *}
 
-lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
-by (rule subst)
+context ord
+begin
 
-lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
-by (rule ssubst)
+lemma ord_le_eq_trans: "a \<le> b \<Longrightarrow> b = c \<Longrightarrow> a \<le> c"
+  by (rule subst)
 
-lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c"
-by (rule subst)
+lemma ord_eq_le_trans: "a = b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"
+  by (rule ssubst)
 
-lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c"
-by (rule ssubst)
+lemma ord_less_eq_trans: "a < b \<Longrightarrow> b = c \<Longrightarrow> a < c"
+  by (rule subst)
+
+lemma ord_eq_less_trans: "a = b \<Longrightarrow> b < c \<Longrightarrow> a < c"
+  by (rule ssubst)
+
+end
 
 lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
   (!!x y. x < y ==> f x < f y) ==> f a < c"

--- a/src/HOL/Ring_and_Field.thy	Thu Oct 25 16:57:57 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Thu Oct 25 19:27:50 2007 +0200
@@ -1908,15 +1908,20 @@
 
 subsection {* Ordered Fields are Dense *}
 
-lemma less_add_one: "a < (a+1::'a::ordered_semidom)"
+context ordered_semidom
+begin
+
+lemma less_add_one: "a < a + 1"
 proof -
-  have "a+0 < (a+1::'a::ordered_semidom)"
+  have "a + 0 < a + 1"
     by (blast intro: zero_less_one add_strict_left_mono)
   thus ?thesis by simp
 qed
 
-lemma zero_less_two: "0 < (1+1::'a::ordered_semidom)"
-by (blast intro: order_less_trans zero_less_one less_add_one)
+lemma zero_less_two: "0 < 1 + 1"
+  by (blast intro: less_trans zero_less_one less_add_one)
+
+end
 
 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
 by (simp add: field_simps zero_less_two)