various localizations
authorhaftmann
Thu Oct 25 19:27:50 2007 +0200 (2007-10-25)
changeset 25193e2e1a4b00de3
parent 25192 b568f8c5d5ca
child 25194 37a1743f0fc3
various localizations
src/HOL/IntDef.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/IntDef.thy	Thu Oct 25 16:57:57 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Thu Oct 25 19:27:50 2007 +0200
     1.3 @@ -426,8 +426,11 @@
     1.4  
     1.5  subsection{*Embedding of the Integers into any @{text ring_1}: @{term of_int}*}
     1.6  
     1.7 +context ring_1
     1.8 +begin
     1.9 +
    1.10  definition
    1.11 -  of_int :: "int \<Rightarrow> 'a\<Colon>ring_1"
    1.12 +  of_int :: "int \<Rightarrow> 'a"
    1.13  where
    1.14    "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
    1.15  lemmas [code func del] = of_int_def
    1.16 @@ -453,15 +456,21 @@
    1.17  lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
    1.18  by (cases z, simp add: compare_rls of_int minus)
    1.19  
    1.20 -lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z"
    1.21 -by (simp add: diff_minus)
    1.22 -
    1.23  lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
    1.24  apply (cases w, cases z)
    1.25  apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
    1.26                   mult add_ac of_nat_mult)
    1.27  done
    1.28  
    1.29 +text{*Collapse nested embeddings*}
    1.30 +lemma of_int_of_nat_eq [simp]: "of_int (Nat.of_nat n) = of_nat n"
    1.31 +  by (induct n, auto)
    1.32 +
    1.33 +end
    1.34 +
    1.35 +lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z"
    1.36 +by (simp add: diff_minus)
    1.37 +
    1.38  lemma of_int_le_iff [simp]:
    1.39       "(of_int w \<le> (of_int z::'a::ordered_idom)) = (w \<le> z)"
    1.40  apply (cases w)
    1.41 @@ -474,7 +483,6 @@
    1.42  lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]
    1.43  lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]
    1.44  
    1.45 -
    1.46  lemma of_int_less_iff [simp]:
    1.47       "(of_int w < (of_int z::'a::ordered_idom)) = (w < z)"
    1.48  by (simp add: linorder_not_le [symmetric])
    1.49 @@ -486,83 +494,83 @@
    1.50  text{*Class for unital rings with characteristic zero.
    1.51   Includes non-ordered rings like the complex numbers.*}
    1.52  class ring_char_0 = ring_1 + semiring_char_0
    1.53 +begin
    1.54  
    1.55  lemma of_int_eq_iff [simp]:
    1.56 -   "of_int w = (of_int z \<Colon> 'a\<Colon>ring_char_0) \<longleftrightarrow> w = z"
    1.57 +   "of_int w = of_int z \<longleftrightarrow> w = z"
    1.58  apply (cases w, cases z, simp add: of_int)
    1.59  apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
    1.60  apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
    1.61  done
    1.62  
    1.63 -text{*Every @{text ordered_idom} has characteristic zero.*}
    1.64 -instance ordered_idom < ring_char_0 ..
    1.65 -
    1.66  text{*Special cases where either operand is zero*}
    1.67  lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
    1.68  lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified]
    1.69  
    1.70 -lemma of_int_eq_id [simp]: "of_int = (id :: int => int)"
    1.71 +end
    1.72 +
    1.73 +text{*Every @{text ordered_idom} has characteristic zero.*}
    1.74 +instance ordered_idom \<subseteq> ring_char_0 ..
    1.75 +
    1.76 +lemma of_int_eq_id [simp]: "of_int = id"
    1.77  proof
    1.78 -  fix z
    1.79 -  show "of_int z = id z"
    1.80 -    by (cases z)
    1.81 -      (simp add: of_int add minus int_def diff_minus)
    1.82 +  fix z show "of_int z = id z"
    1.83 +    by (cases z) (simp add: of_int add minus int_def diff_minus)
    1.84  qed
    1.85  
    1.86 -lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
    1.87 +lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
    1.88  by (cases z rule: eq_Abs_Integ)
    1.89     (simp add: nat le of_int Zero_int_def of_nat_diff)
    1.90  
    1.91  
    1.92  subsection{*The Set of Integers*}
    1.93  
    1.94 -constdefs
    1.95 -  Ints  :: "'a::ring_1 set"
    1.96 -  "Ints == range of_int"
    1.97 +context ring_1
    1.98 +begin
    1.99 +
   1.100 +definition
   1.101 +  Ints  :: "'a set"
   1.102 +where
   1.103 +  "Ints = range of_int"
   1.104 +
   1.105 +end
   1.106  
   1.107  notation (xsymbols)
   1.108    Ints  ("\<int>")
   1.109  
   1.110 -lemma Ints_0 [simp]: "0 \<in> Ints"
   1.111 +context ring_1
   1.112 +begin
   1.113 +
   1.114 +lemma Ints_0 [simp]: "0 \<in> \<int>"
   1.115  apply (simp add: Ints_def)
   1.116  apply (rule range_eqI)
   1.117  apply (rule of_int_0 [symmetric])
   1.118  done
   1.119  
   1.120 -lemma Ints_1 [simp]: "1 \<in> Ints"
   1.121 +lemma Ints_1 [simp]: "1 \<in> \<int>"
   1.122  apply (simp add: Ints_def)
   1.123  apply (rule range_eqI)
   1.124  apply (rule of_int_1 [symmetric])
   1.125  done
   1.126  
   1.127 -lemma Ints_add [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a+b \<in> Ints"
   1.128 +lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
   1.129  apply (auto simp add: Ints_def)
   1.130  apply (rule range_eqI)
   1.131  apply (rule of_int_add [symmetric])
   1.132  done
   1.133  
   1.134 -lemma Ints_minus [simp]: "a \<in> Ints ==> -a \<in> Ints"
   1.135 +lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
   1.136  apply (auto simp add: Ints_def)
   1.137  apply (rule range_eqI)
   1.138  apply (rule of_int_minus [symmetric])
   1.139  done
   1.140  
   1.141 -lemma Ints_diff [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a-b \<in> Ints"
   1.142 -apply (auto simp add: Ints_def)
   1.143 -apply (rule range_eqI)
   1.144 -apply (rule of_int_diff [symmetric])
   1.145 -done
   1.146 -
   1.147 -lemma Ints_mult [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a*b \<in> Ints"
   1.148 +lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
   1.149  apply (auto simp add: Ints_def)
   1.150  apply (rule range_eqI)
   1.151  apply (rule of_int_mult [symmetric])
   1.152  done
   1.153  
   1.154 -text{*Collapse nested embeddings*}
   1.155 -lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
   1.156 -by (induct n, auto)
   1.157 -
   1.158  lemma Ints_cases [cases set: Ints]:
   1.159    assumes "q \<in> \<int>"
   1.160    obtains (of_int) z where "q = of_int z"
   1.161 @@ -574,9 +582,17 @@
   1.162  qed
   1.163  
   1.164  lemma Ints_induct [case_names of_int, induct set: Ints]:
   1.165 -  "q \<in> \<int> ==> (!!z. P (of_int z)) ==> P q"
   1.166 +  "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
   1.167    by (rule Ints_cases) auto
   1.168  
   1.169 +end
   1.170 +
   1.171 +lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a-b \<in> \<int>"
   1.172 +apply (auto simp add: Ints_def)
   1.173 +apply (rule range_eqI)
   1.174 +apply (rule of_int_diff [symmetric])
   1.175 +done
   1.176 +
   1.177  
   1.178  subsection {* @{term setsum} and @{term setprod} *}
   1.179  
     2.1 --- a/src/HOL/Nat.thy	Thu Oct 25 16:57:57 2007 +0200
     2.2 +++ b/src/HOL/Nat.thy	Thu Oct 25 19:27:50 2007 +0200
     2.3 @@ -1147,8 +1147,8 @@
     2.4    using Suc_le_eq less_Suc_eq_le by simp_all
     2.5  
     2.6  
     2.7 -subsection{*Embedding of the Naturals into any
     2.8 -  @{text semiring_1}: @{term of_nat}*}
     2.9 +subsection {* Embedding of the Naturals into any
    2.10 +  @{text semiring_1}: @{term of_nat} *}
    2.11  
    2.12  context semiring_1
    2.13  begin
    2.14 @@ -1156,8 +1156,102 @@
    2.15  definition
    2.16    of_nat_def: "of_nat = nat_rec 0 (\<lambda>_. (op +) 1)"
    2.17  
    2.18 +lemma of_nat_simps [simp, code]:
    2.19 +  shows of_nat_0:   "of_nat 0 = 0"
    2.20 +    and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
    2.21 +  unfolding of_nat_def by simp_all
    2.22 +
    2.23 +lemma of_nat_1 [simp]: "of_nat 1 = 1"
    2.24 +  by simp
    2.25 +
    2.26 +lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
    2.27 +  by (induct m) (simp_all add: add_ac)
    2.28 +
    2.29 +lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
    2.30 +  by (induct m) (simp_all add: add_ac left_distrib)
    2.31 +
    2.32  end
    2.33  
    2.34 +context ordered_semidom
    2.35 +begin
    2.36 +
    2.37 +lemma zero_le_imp_of_nat: "0 \<le> of_nat m"
    2.38 +  apply (induct m, simp_all)
    2.39 +  apply (erule order_trans)
    2.40 +  apply (rule ord_le_eq_trans [OF _ add_commute])
    2.41 +  apply (rule less_add_one [THEN less_imp_le])
    2.42 +  done
    2.43 +
    2.44 +lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
    2.45 +  apply (induct m n rule: diff_induct, simp_all)
    2.46 +  apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
    2.47 +  done
    2.48 +
    2.49 +lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
    2.50 +  apply (induct m n rule: diff_induct, simp_all)
    2.51 +  apply (insert zero_le_imp_of_nat)
    2.52 +  apply (force simp add: not_less [symmetric])
    2.53 +  done
    2.54 +
    2.55 +lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
    2.56 +  by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
    2.57 +
    2.58 +text{*Special cases where either operand is zero*}
    2.59 +
    2.60 +lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
    2.61 +  by (rule of_nat_less_iff [of 0, simplified])
    2.62 +
    2.63 +lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
    2.64 +  by (rule of_nat_less_iff [of _ 0, simplified])
    2.65 +
    2.66 +lemma of_nat_le_iff [simp]:
    2.67 +  "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
    2.68 +  by (simp add: not_less [symmetric] linorder_not_less [symmetric])
    2.69 +
    2.70 +text{*Special cases where either operand is zero*}
    2.71 +
    2.72 +lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
    2.73 +  by (rule of_nat_le_iff [of 0, simplified])
    2.74 +
    2.75 +lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
    2.76 +  by (rule of_nat_le_iff [of _ 0, simplified])
    2.77 +
    2.78 +end
    2.79 +
    2.80 +lemma of_nat_id [simp]: "of_nat n = n"
    2.81 +  by (induct n) auto
    2.82 +
    2.83 +lemma of_nat_eq_id [simp]: "of_nat = id"
    2.84 +  by (auto simp add: expand_fun_eq)
    2.85 +
    2.86 +text{*Class for unital semirings with characteristic zero.
    2.87 + Includes non-ordered rings like the complex numbers.*}
    2.88 +
    2.89 +class semiring_char_0 = semiring_1 +
    2.90 +  assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
    2.91 +
    2.92 +text{*Every @{text ordered_semidom} has characteristic zero.*}
    2.93 +
    2.94 +subclass (in ordered_semidom) semiring_char_0
    2.95 +  by unfold_locales (simp add: eq_iff order_eq_iff)
    2.96 +
    2.97 +context semiring_char_0
    2.98 +begin
    2.99 +
   2.100 +text{*Special cases where either operand is zero*}
   2.101 +
   2.102 +lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
   2.103 +  by (rule of_nat_eq_iff [of 0, simplified])
   2.104 +
   2.105 +lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
   2.106 +  by (rule of_nat_eq_iff [of _ 0, simplified])
   2.107 +
   2.108 +lemma inj_of_nat: "inj of_nat"
   2.109 +  by (simp add: inj_on_def)
   2.110 +
   2.111 +end
   2.112 +
   2.113 +
   2.114  subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
   2.115  
   2.116  lemma subst_equals:
   2.117 @@ -1165,7 +1259,6 @@
   2.118    shows "u = s"
   2.119    using 2 1 by (rule trans)
   2.120  
   2.121 -
   2.122  use "arith_data.ML"
   2.123  declaration {* K arith_data_setup *}
   2.124  
   2.125 @@ -1186,6 +1279,18 @@
   2.126      -- {* elimination of @{text -} on @{text nat} *}
   2.127  by (cases "a<b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
   2.128  
   2.129 +context ring_1
   2.130 +begin
   2.131 +
   2.132 +lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
   2.133 +  by (simp del: of_nat_add
   2.134 +    add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
   2.135 +
   2.136 +end
   2.137 +
   2.138 +lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
   2.139 +  by (rule of_nat_0_le_iff [THEN abs_of_nonneg])
   2.140 +
   2.141  lemma nat_diff_split_asm:
   2.142    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
   2.143      -- {* elimination of @{text -} on @{text nat} in assumptions *}
   2.144 @@ -1333,141 +1438,52 @@
   2.145  Least_Suc}, since there appears to be no need.*}
   2.146  
   2.147  
   2.148 -subsection{*Embedding of the Naturals into any
   2.149 -  @{text semiring_1}: @{term of_nat}*}
   2.150 +subsection {*The Set of Natural Numbers*}
   2.151  
   2.152  context semiring_1
   2.153  begin
   2.154  
   2.155 -lemma of_nat_simps [simp, code]:
   2.156 -  shows of_nat_0:   "of_nat 0 = 0"
   2.157 -    and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
   2.158 -  unfolding of_nat_def by simp_all
   2.159 +definition
   2.160 +  Nats  :: "'a set"
   2.161 +where
   2.162 +  "Nats = range of_nat"
   2.163  
   2.164  end
   2.165  
   2.166 -lemma of_nat_id [simp]: "(of_nat n \<Colon> nat) = n"
   2.167 -by (induct n) auto
   2.168 -
   2.169 -lemma of_nat_1 [simp]: "of_nat 1 = 1"
   2.170 -by simp
   2.171 -
   2.172 -lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
   2.173 -by (induct m) (simp_all add: add_ac)
   2.174 -
   2.175 -lemma of_nat_mult: "of_nat (m*n) = of_nat m * of_nat n"
   2.176 -by (induct m) (simp_all add: add_ac left_distrib)
   2.177 -
   2.178 -lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
   2.179 -  apply (induct m, simp_all)
   2.180 -  apply (erule order_trans)
   2.181 -  apply (rule ord_le_eq_trans [OF _ add_commute])
   2.182 -  apply (rule less_add_one [THEN order_less_imp_le])
   2.183 -  done
   2.184 -
   2.185 -lemma less_imp_of_nat_less:
   2.186 -    "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
   2.187 -  apply (induct m n rule: diff_induct, simp_all)
   2.188 -  apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
   2.189 -  done
   2.190 -
   2.191 -lemma of_nat_less_imp_less:
   2.192 -    "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
   2.193 -  apply (induct m n rule: diff_induct, simp_all)
   2.194 -  apply (insert zero_le_imp_of_nat)
   2.195 -  apply (force simp add: linorder_not_less [symmetric])
   2.196 -  done
   2.197 -
   2.198 -lemma of_nat_less_iff [simp]:
   2.199 -  "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
   2.200 -by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
   2.201 -
   2.202 -text{*Special cases where either operand is zero*}
   2.203 -
   2.204 -lemma of_nat_0_less_iff [simp]: "((0::'a::ordered_semidom) < of_nat n) = (0 < n)"
   2.205 -by (rule of_nat_less_iff [of 0, simplified])
   2.206 -
   2.207 -lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < (0::'a::ordered_semidom)"
   2.208 -by (rule of_nat_less_iff [of _ 0, simplified])
   2.209 -
   2.210 -lemma of_nat_le_iff [simp]:
   2.211 -  "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
   2.212 -by (simp add: linorder_not_less [symmetric])
   2.213 -
   2.214 -text{*Special cases where either operand is zero*}
   2.215 -lemma of_nat_0_le_iff [simp]: "(0::'a::ordered_semidom) \<le> of_nat n"
   2.216 -by (rule of_nat_le_iff [of 0, simplified])
   2.217 -lemma of_nat_le_0_iff [simp,noatp]: "(of_nat m \<le> (0::'a::ordered_semidom)) = (m = 0)"
   2.218 -by (rule of_nat_le_iff [of _ 0, simplified])
   2.219 -
   2.220 -text{*Class for unital semirings with characteristic zero.
   2.221 - Includes non-ordered rings like the complex numbers.*}
   2.222 -
   2.223 -class semiring_char_0 = semiring_1 +
   2.224 -  assumes of_nat_eq_iff [simp]:
   2.225 -    "of_nat m = of_nat n \<longleftrightarrow> m = n"
   2.226 -
   2.227 -text{*Every @{text ordered_semidom} has characteristic zero.*}
   2.228 -instance ordered_semidom < semiring_char_0
   2.229 -by intro_classes (simp add: order_eq_iff)
   2.230 -
   2.231 -text{*Special cases where either operand is zero*}
   2.232 -lemma of_nat_0_eq_iff [simp,noatp]: "((0::'a::semiring_char_0) = of_nat n) = (0 = n)"
   2.233 -by (rule of_nat_eq_iff [of 0, simplified])
   2.234 -lemma of_nat_eq_0_iff [simp,noatp]: "(of_nat m = (0::'a::semiring_char_0)) = (m = 0)"
   2.235 -by (rule of_nat_eq_iff [of _ 0, simplified])
   2.236 -
   2.237 -lemma inj_of_nat: "inj (of_nat :: nat \<Rightarrow> 'a::semiring_char_0)"
   2.238 -by (simp add: inj_on_def)
   2.239 -
   2.240 -lemma of_nat_diff:
   2.241 -  "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
   2.242 -by (simp del: of_nat_add
   2.243 -    add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
   2.244 -
   2.245 -lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
   2.246 -by (rule of_nat_0_le_iff [THEN abs_of_nonneg])
   2.247 -
   2.248 -
   2.249 -subsection {*The Set of Natural Numbers*}
   2.250 -
   2.251 -definition
   2.252 -  Nats  :: "'a::semiring_1 set"
   2.253 -where
   2.254 -  "Nats = range of_nat"
   2.255 -
   2.256  notation (xsymbols)
   2.257    Nats  ("\<nat>")
   2.258  
   2.259 -lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
   2.260 -by (simp add: Nats_def)
   2.261 +context semiring_1
   2.262 +begin
   2.263  
   2.264 -lemma Nats_0 [simp]: "0 \<in> Nats"
   2.265 +lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
   2.266 +  by (simp add: Nats_def)
   2.267 +
   2.268 +lemma Nats_0 [simp]: "0 \<in> \<nat>"
   2.269  apply (simp add: Nats_def)
   2.270  apply (rule range_eqI)
   2.271  apply (rule of_nat_0 [symmetric])
   2.272  done
   2.273  
   2.274 -lemma Nats_1 [simp]: "1 \<in> Nats"
   2.275 +lemma Nats_1 [simp]: "1 \<in> \<nat>"
   2.276  apply (simp add: Nats_def)
   2.277  apply (rule range_eqI)
   2.278  apply (rule of_nat_1 [symmetric])
   2.279  done
   2.280  
   2.281 -lemma Nats_add [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a+b \<in> Nats"
   2.282 +lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>"
   2.283  apply (auto simp add: Nats_def)
   2.284  apply (rule range_eqI)
   2.285  apply (rule of_nat_add [symmetric])
   2.286  done
   2.287  
   2.288 -lemma Nats_mult [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a*b \<in> Nats"
   2.289 +lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>"
   2.290  apply (auto simp add: Nats_def)
   2.291  apply (rule range_eqI)
   2.292  apply (rule of_nat_mult [symmetric])
   2.293  done
   2.294  
   2.295 -lemma of_nat_eq_id [simp]: "of_nat = (id :: nat => nat)"
   2.296 -by (auto simp add: expand_fun_eq)
   2.297 +end
   2.298  
   2.299  
   2.300  text {* the lattice order on @{typ nat} *}
     3.1 --- a/src/HOL/Orderings.thy	Thu Oct 25 16:57:57 2007 +0200
     3.2 +++ b/src/HOL/Orderings.thy	Thu Oct 25 19:27:50 2007 +0200
     3.3 @@ -685,17 +685,22 @@
     3.4  
     3.5  subsection {* Transitivity reasoning *}
     3.6  
     3.7 -lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
     3.8 -by (rule subst)
     3.9 +context ord
    3.10 +begin
    3.11  
    3.12 -lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
    3.13 -by (rule ssubst)
    3.14 +lemma ord_le_eq_trans: "a \<le> b \<Longrightarrow> b = c \<Longrightarrow> a \<le> c"
    3.15 +  by (rule subst)
    3.16  
    3.17 -lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c"
    3.18 -by (rule subst)
    3.19 +lemma ord_eq_le_trans: "a = b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"
    3.20 +  by (rule ssubst)
    3.21  
    3.22 -lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c"
    3.23 -by (rule ssubst)
    3.24 +lemma ord_less_eq_trans: "a < b \<Longrightarrow> b = c \<Longrightarrow> a < c"
    3.25 +  by (rule subst)
    3.26 +
    3.27 +lemma ord_eq_less_trans: "a = b \<Longrightarrow> b < c \<Longrightarrow> a < c"
    3.28 +  by (rule ssubst)
    3.29 +
    3.30 +end
    3.31  
    3.32  lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
    3.33    (!!x y. x < y ==> f x < f y) ==> f a < c"
     4.1 --- a/src/HOL/Ring_and_Field.thy	Thu Oct 25 16:57:57 2007 +0200
     4.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Oct 25 19:27:50 2007 +0200
     4.3 @@ -1908,15 +1908,20 @@
     4.4  
     4.5  subsection {* Ordered Fields are Dense *}
     4.6  
     4.7 -lemma less_add_one: "a < (a+1::'a::ordered_semidom)"
     4.8 +context ordered_semidom
     4.9 +begin
    4.10 +
    4.11 +lemma less_add_one: "a < a + 1"
    4.12  proof -
    4.13 -  have "a+0 < (a+1::'a::ordered_semidom)"
    4.14 +  have "a + 0 < a + 1"
    4.15      by (blast intro: zero_less_one add_strict_left_mono)
    4.16    thus ?thesis by simp
    4.17  qed
    4.18  
    4.19 -lemma zero_less_two: "0 < (1+1::'a::ordered_semidom)"
    4.20 -by (blast intro: order_less_trans zero_less_one less_add_one)
    4.21 +lemma zero_less_two: "0 < 1 + 1"
    4.22 +  by (blast intro: less_trans zero_less_one less_add_one)
    4.23 +
    4.24 +end
    4.25  
    4.26  lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
    4.27  by (simp add: field_simps zero_less_two)