localized of_nat
authorhaftmann
Thu Aug 09 15:52:47 2007 +0200 (2007-08-09)
changeset 24196f1dbfd7e3223
parent 24195 7d1a16c77f7c
child 24197 c9e3cb5e5681
localized of_nat
src/HOL/IntDef.thy
src/HOL/Nat.thy
src/HOL/Real/rat_arith.ML
src/HOL/Tools/lin_arith.ML
src/HOL/int_arith1.ML
     1.1 --- a/src/HOL/IntDef.thy	Thu Aug 09 15:52:45 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Thu Aug 09 15:52:47 2007 +0200
     1.3 @@ -149,12 +149,7 @@
     1.4      by (simp add: Zero_int_def One_int_def)
     1.5  qed
     1.6  
     1.7 -abbreviation
     1.8 -  int :: "nat \<Rightarrow> int"
     1.9 -where
    1.10 -  "int \<equiv> of_nat"
    1.11 -
    1.12 -lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
    1.13 +lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
    1.14  by (induct m, simp_all add: Zero_int_def One_int_def add)
    1.15  
    1.16  
    1.17 @@ -194,20 +189,20 @@
    1.18  
    1.19  text{*strict, in 1st argument; proof is by induction on k>0*}
    1.20  lemma zmult_zless_mono2_lemma:
    1.21 -     "(i::int)<j ==> 0<k ==> int k * i < int k * j"
    1.22 +     "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
    1.23  apply (induct "k", simp)
    1.24  apply (simp add: left_distrib)
    1.25  apply (case_tac "k=0")
    1.26  apply (simp_all add: add_strict_mono)
    1.27  done
    1.28  
    1.29 -lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
    1.30 +lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
    1.31  apply (cases k)
    1.32  apply (auto simp add: le add int_def Zero_int_def)
    1.33  apply (rule_tac x="x-y" in exI, simp)
    1.34  done
    1.35  
    1.36 -lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
    1.37 +lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
    1.38  apply (cases k)
    1.39  apply (simp add: less int_def Zero_int_def)
    1.40  apply (rule_tac x="x-y" in exI, simp)
    1.41 @@ -258,16 +253,16 @@
    1.42      by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
    1.43  qed
    1.44  
    1.45 -lemma nat_int [simp]: "nat (int n) = n"
    1.46 +lemma nat_int [simp]: "nat (of_nat n) = n"
    1.47  by (simp add: nat int_def)
    1.48  
    1.49  lemma nat_zero [simp]: "nat 0 = 0"
    1.50  by (simp add: Zero_int_def nat)
    1.51  
    1.52 -lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
    1.53 +lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
    1.54  by (cases z, simp add: nat le int_def Zero_int_def)
    1.55  
    1.56 -corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
    1.57 +corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
    1.58  by simp
    1.59  
    1.60  lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
    1.61 @@ -290,21 +285,24 @@
    1.62  apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
    1.63  done
    1.64  
    1.65 -lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
    1.66 -by (blast dest: nat_0_le sym)
    1.67 +lemma nonneg_eq_int:
    1.68 +  fixes z :: int
    1.69 +  assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
    1.70 +  shows P
    1.71 +  using assms by (blast dest: nat_0_le sym)
    1.72  
    1.73 -lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
    1.74 +lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
    1.75  by (cases w, simp add: nat le int_def Zero_int_def, arith)
    1.76  
    1.77 -corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
    1.78 +corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
    1.79  by (simp only: eq_commute [of m] nat_eq_iff)
    1.80  
    1.81 -lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
    1.82 +lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
    1.83  apply (cases w)
    1.84  apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
    1.85  done
    1.86  
    1.87 -lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
    1.88 +lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
    1.89  by (auto simp add: nat_eq_iff2)
    1.90  
    1.91  lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
    1.92 @@ -319,59 +317,56 @@
    1.93  by (cases z, cases z', 
    1.94      simp add: nat add minus diff_minus le Zero_int_def)
    1.95  
    1.96 -lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
    1.97 +lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
    1.98  by (simp add: int_def minus nat Zero_int_def) 
    1.99  
   1.100 -lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   1.101 +lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
   1.102  by (cases z, simp add: nat less int_def, arith)
   1.103  
   1.104  
   1.105 -subsection{*Lemmas about the Function @{term int} and Orderings*}
   1.106 +subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
   1.107  
   1.108 -lemma negative_zless_0: "- (int (Suc n)) < 0"
   1.109 +lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
   1.110  by (simp add: order_less_le del: of_nat_Suc)
   1.111  
   1.112 -lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   1.113 +lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
   1.114  by (rule negative_zless_0 [THEN order_less_le_trans], simp)
   1.115  
   1.116 -lemma negative_zle_0: "- int n \<le> 0"
   1.117 +lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
   1.118  by (simp add: minus_le_iff)
   1.119  
   1.120 -lemma negative_zle [iff]: "- int n \<le> int m"
   1.121 +lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
   1.122  by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
   1.123  
   1.124 -lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   1.125 +lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"
   1.126  by (subst le_minus_iff, simp del: of_nat_Suc)
   1.127  
   1.128 -lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   1.129 +lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
   1.130  by (simp add: int_def le minus Zero_int_def)
   1.131  
   1.132 -lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   1.133 +lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
   1.134  by (simp add: linorder_not_less)
   1.135  
   1.136 -lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
   1.137 -by (force simp add: order_eq_iff [of "- int n"] int_zle_neg)
   1.138 +lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
   1.139 +by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
   1.140  
   1.141 -lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
   1.142 +lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
   1.143  proof -
   1.144    have "(w \<le> z) = (0 \<le> z - w)"
   1.145      by (simp only: le_diff_eq add_0_left)
   1.146 -  also have "\<dots> = (\<exists>n. z - w = int n)"
   1.147 +  also have "\<dots> = (\<exists>n. z - w = of_nat n)"
   1.148      by (auto elim: zero_le_imp_eq_int)
   1.149 -  also have "\<dots> = (\<exists>n. z = w + int n)"
   1.150 +  also have "\<dots> = (\<exists>n. z = w + of_nat n)"
   1.151      by (simp only: group_simps)
   1.152    finally show ?thesis .
   1.153  qed
   1.154  
   1.155 -lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
   1.156 +lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
   1.157  by simp
   1.158  
   1.159 -lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   1.160 +lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
   1.161  by simp
   1.162  
   1.163 -lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
   1.164 -by (rule  of_nat_0_le_iff [THEN abs_of_nonneg]) (* belongs in Nat.thy *)
   1.165 -
   1.166  text{*This version is proved for all ordered rings, not just integers!
   1.167        It is proved here because attribute @{text arith_split} is not available
   1.168        in theory @{text Ring_and_Field}.
   1.169 @@ -393,10 +388,10 @@
   1.170  where
   1.171    "iszero z \<longleftrightarrow> z = 0"
   1.172  
   1.173 -lemma not_neg_int [simp]: "~ neg (int n)"
   1.174 +lemma not_neg_int [simp]: "~ neg (of_nat n)"
   1.175  by (simp add: neg_def)
   1.176  
   1.177 -lemma neg_zminus_int [simp]: "neg (- (int (Suc n)))"
   1.178 +lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
   1.179  by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
   1.180  
   1.181  lemmas neg_eq_less_0 = neg_def
   1.182 @@ -422,7 +417,7 @@
   1.183  lemma neg_nat: "neg z ==> nat z = 0"
   1.184  by (simp add: neg_def order_less_imp_le) 
   1.185  
   1.186 -lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
   1.187 +lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
   1.188  by (simp add: linorder_not_less neg_def)
   1.189  
   1.190  
   1.191 @@ -490,7 +485,7 @@
   1.192  class ring_char_0 = ring_1 + semiring_char_0
   1.193  
   1.194  lemma of_int_eq_iff [simp]:
   1.195 -     "(of_int w = (of_int z::'a::ring_char_0)) = (w = z)"
   1.196 +   "of_int w = (of_int z \<Colon> 'a\<Colon>ring_char_0) \<longleftrightarrow> w = z"
   1.197  apply (cases w, cases z, simp add: of_int)
   1.198  apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
   1.199  apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
   1.200 @@ -586,7 +581,7 @@
   1.201  whether an integer is negative or not.*}
   1.202  
   1.203  lemma zless_iff_Suc_zadd:
   1.204 -    "(w < z) = (\<exists>n. z = w + int (Suc n))"
   1.205 +  "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))"
   1.206  apply (cases z, cases w)
   1.207  apply (auto simp add: less add int_def)
   1.208  apply (rename_tac a b c d) 
   1.209 @@ -594,26 +589,26 @@
   1.210  apply arith
   1.211  done
   1.212  
   1.213 -lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
   1.214 +lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
   1.215  apply (cases x)
   1.216  apply (auto simp add: le minus Zero_int_def int_def order_less_le)
   1.217  apply (rule_tac x="y - Suc x" in exI, arith)
   1.218  done
   1.219  
   1.220  theorem int_cases [cases type: int, case_names nonneg neg]:
   1.221 -     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   1.222 +  "[|!! n. (z \<Colon> int) = of_nat n ==> P;  !! n. z =  - (of_nat (Suc n)) ==> P |] ==> P"
   1.223  apply (cases "z < 0", blast dest!: negD)
   1.224  apply (simp add: linorder_not_less del: of_nat_Suc)
   1.225  apply (blast dest: nat_0_le [THEN sym])
   1.226  done
   1.227  
   1.228  theorem int_induct [induct type: int, case_names nonneg neg]:
   1.229 -     "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   1.230 +     "[|!! n. P (of_nat n \<Colon> int);  !!n. P (- (of_nat (Suc n))) |] ==> P z"
   1.231    by (cases z rule: int_cases) auto
   1.232  
   1.233  text{*Contributed by Brian Huffman*}
   1.234  theorem int_diff_cases [case_names diff]:
   1.235 -assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
   1.236 +assumes prem: "!!m n. (z\<Colon>int) = of_nat m - of_nat n ==> P" shows "P"
   1.237  apply (cases z rule: eq_Abs_Integ)
   1.238  apply (rule_tac m=x and n=y in prem)
   1.239  apply (simp add: int_def diff_def minus add)
   1.240 @@ -673,9 +668,9 @@
   1.241  lemmas zle_int = of_nat_le_iff [where 'a=int]
   1.242  lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
   1.243  lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="?n"]
   1.244 -lemmas int_0 = of_nat_0 [where ?'a_1.0=int]
   1.245 +lemmas int_0 = of_nat_0 [where 'a=int]
   1.246  lemmas int_1 = of_nat_1 [where 'a=int]
   1.247 -lemmas int_Suc = of_nat_Suc [where ?'a_1.0=int]
   1.248 +lemmas int_Suc = of_nat_Suc [where 'a=int]
   1.249  lemmas abs_int_eq = abs_of_nat [where 'a=int and n="?m"]
   1.250  lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
   1.251  lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
   1.252 @@ -683,6 +678,11 @@
   1.253  lemmas int_eq_of_nat = TrueI
   1.254  
   1.255  abbreviation
   1.256 +  int :: "nat \<Rightarrow> int"
   1.257 +where
   1.258 +  "int \<equiv> of_nat"
   1.259 +
   1.260 +abbreviation
   1.261    int_of_nat :: "nat \<Rightarrow> int"
   1.262  where
   1.263    "int_of_nat \<equiv> of_nat"
     2.1 --- a/src/HOL/Nat.thy	Thu Aug 09 15:52:45 2007 +0200
     2.2 +++ b/src/HOL/Nat.thy	Thu Aug 09 15:52:47 2007 +0200
     2.3 @@ -114,25 +114,6 @@
     2.4  class size = type +
     2.5    fixes size :: "'a \<Rightarrow> nat"
     2.6  
     2.7 -text {* now we are ready to re-invent primitive types
     2.8 -  -- dependency on class size is hardwired into datatype package *}
     2.9 -
    2.10 -rep_datatype bool
    2.11 -  distinct True_not_False False_not_True
    2.12 -  induction bool_induct
    2.13 -
    2.14 -rep_datatype unit
    2.15 -  induction unit_induct
    2.16 -
    2.17 -rep_datatype prod
    2.18 -  inject Pair_eq
    2.19 -  induction prod_induct
    2.20 -
    2.21 -rep_datatype sum
    2.22 -  distinct Inl_not_Inr Inr_not_Inl
    2.23 -  inject Inl_eq Inr_eq
    2.24 -  induction sum_induct
    2.25 -
    2.26  rep_datatype nat
    2.27    distinct  Suc_not_Zero Zero_not_Suc
    2.28    inject    Suc_Suc_eq
    2.29 @@ -1101,6 +1082,17 @@
    2.30    using Suc_le_eq less_Suc_eq_le by simp_all
    2.31  
    2.32  
    2.33 +subsection{*Embedding of the Naturals into any
    2.34 +  @{text semiring_1}: @{term of_nat}*}
    2.35 +
    2.36 +context semiring_1
    2.37 +begin
    2.38 +
    2.39 +definition
    2.40 +  of_nat_def: "of_nat = nat_rec \<^loc>0 (\<lambda>_. (op \<^loc>+) \<^loc>1)"
    2.41 +
    2.42 +end
    2.43 +
    2.44  subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
    2.45  
    2.46  lemma subst_equals:
    2.47 @@ -1108,6 +1100,7 @@
    2.48    shows "u = s"
    2.49    using 2 1 by (rule trans)
    2.50  
    2.51 +
    2.52  use "arith_data.ML"
    2.53  declaration {* K arith_data_setup *}
    2.54  
    2.55 @@ -1274,45 +1267,19 @@
    2.56  text{*At present we prove no analogue of @{text not_less_Least} or @{text
    2.57  Least_Suc}, since there appears to be no need.*}
    2.58  
    2.59 -ML
    2.60 -{*
    2.61 -val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
    2.62 -val nat_diff_split = thm "nat_diff_split";
    2.63 -val nat_diff_split_asm = thm "nat_diff_split_asm";
    2.64 -val le_square = thm "le_square";
    2.65 -val le_cube = thm "le_cube";
    2.66 -val diff_less_mono = thm "diff_less_mono";
    2.67 -val less_diff_conv = thm "less_diff_conv";
    2.68 -val le_diff_conv = thm "le_diff_conv";
    2.69 -val le_diff_conv2 = thm "le_diff_conv2";
    2.70 -val diff_diff_cancel = thm "diff_diff_cancel";
    2.71 -val le_add_diff = thm "le_add_diff";
    2.72 -val diff_less = thm "diff_less";
    2.73 -val diff_diff_eq = thm "diff_diff_eq";
    2.74 -val eq_diff_iff = thm "eq_diff_iff";
    2.75 -val less_diff_iff = thm "less_diff_iff";
    2.76 -val le_diff_iff = thm "le_diff_iff";
    2.77 -val diff_le_mono = thm "diff_le_mono";
    2.78 -val diff_le_mono2 = thm "diff_le_mono2";
    2.79 -val diff_less_mono2 = thm "diff_less_mono2";
    2.80 -val diffs0_imp_equal = thm "diffs0_imp_equal";
    2.81 -val one_less_mult = thm "one_less_mult";
    2.82 -val n_less_m_mult_n = thm "n_less_m_mult_n";
    2.83 -val n_less_n_mult_m = thm "n_less_n_mult_m";
    2.84 -val diff_diff_right = thm "diff_diff_right";
    2.85 -val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
    2.86 -val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
    2.87 -*}
    2.88 -
    2.89  
    2.90  subsection{*Embedding of the Naturals into any
    2.91    @{text semiring_1}: @{term of_nat}*}
    2.92  
    2.93 -consts of_nat :: "nat => 'a::semiring_1"
    2.94 +context semiring_1
    2.95 +begin
    2.96  
    2.97 -primrec
    2.98 -  of_nat_0:   "of_nat 0 = 0"
    2.99 -  of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
   2.100 +lemma of_nat_simps [simp, code]:
   2.101 +  shows of_nat_0:   "of_nat 0 = \<^loc>0"
   2.102 +    and of_nat_Suc: "of_nat (Suc m) = \<^loc>1 \<^loc>+ of_nat m"
   2.103 +  unfolding of_nat_def by simp_all
   2.104 +
   2.105 +end
   2.106  
   2.107  lemma of_nat_id [simp]: "(of_nat n \<Colon> nat) = n"
   2.108    by (induct n) auto
   2.109 @@ -1320,7 +1287,7 @@
   2.110  lemma of_nat_1 [simp]: "of_nat 1 = 1"
   2.111    by simp
   2.112  
   2.113 -lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
   2.114 +lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
   2.115    by (induct m) (simp_all add: add_ac)
   2.116  
   2.117  lemma of_nat_mult: "of_nat (m*n) = of_nat m * of_nat n"
   2.118 @@ -1370,8 +1337,10 @@
   2.119  
   2.120  text{*Class for unital semirings with characteristic zero.
   2.121   Includes non-ordered rings like the complex numbers.*}
   2.122 -axclass semiring_char_0 < semiring_1
   2.123 -  of_nat_eq_iff [simp]: "(of_nat m = of_nat n) = (m = n)"
   2.124 +
   2.125 +class semiring_char_0 = semiring_1 +
   2.126 +  assumes of_nat_eq_iff [simp]:
   2.127 +    "(Nat.semiring_1.of_nat \<^loc>1 \<^loc>0 (op \<^loc>+) m = Nat.semiring_1.of_nat \<^loc>1 \<^loc>0 (op \<^loc>+)  n) = (m = n)"
   2.128  
   2.129  text{*Every @{text ordered_semidom} has characteristic zero.*}
   2.130  instance ordered_semidom < semiring_char_0
   2.131 @@ -1391,6 +1360,9 @@
   2.132    by (simp del: of_nat_add
   2.133      add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
   2.134  
   2.135 +lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
   2.136 +  by (rule of_nat_0_le_iff [THEN abs_of_nonneg])
   2.137 +
   2.138  
   2.139  subsection {*The Set of Natural Numbers*}
   2.140  
   2.141 @@ -1444,4 +1416,36 @@
   2.142  lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
   2.143    by (induct n) simp_all
   2.144  
   2.145 +subsection {* legacy bindings *}
   2.146 +
   2.147 +ML
   2.148 +{*
   2.149 +val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
   2.150 +val nat_diff_split = thm "nat_diff_split";
   2.151 +val nat_diff_split_asm = thm "nat_diff_split_asm";
   2.152 +val le_square = thm "le_square";
   2.153 +val le_cube = thm "le_cube";
   2.154 +val diff_less_mono = thm "diff_less_mono";
   2.155 +val less_diff_conv = thm "less_diff_conv";
   2.156 +val le_diff_conv = thm "le_diff_conv";
   2.157 +val le_diff_conv2 = thm "le_diff_conv2";
   2.158 +val diff_diff_cancel = thm "diff_diff_cancel";
   2.159 +val le_add_diff = thm "le_add_diff";
   2.160 +val diff_less = thm "diff_less";
   2.161 +val diff_diff_eq = thm "diff_diff_eq";
   2.162 +val eq_diff_iff = thm "eq_diff_iff";
   2.163 +val less_diff_iff = thm "less_diff_iff";
   2.164 +val le_diff_iff = thm "le_diff_iff";
   2.165 +val diff_le_mono = thm "diff_le_mono";
   2.166 +val diff_le_mono2 = thm "diff_le_mono2";
   2.167 +val diff_less_mono2 = thm "diff_less_mono2";
   2.168 +val diffs0_imp_equal = thm "diffs0_imp_equal";
   2.169 +val one_less_mult = thm "one_less_mult";
   2.170 +val n_less_m_mult_n = thm "n_less_m_mult_n";
   2.171 +val n_less_n_mult_m = thm "n_less_n_mult_m";
   2.172 +val diff_diff_right = thm "diff_diff_right";
   2.173 +val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
   2.174 +val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
   2.175 +*}
   2.176 +
   2.177  end
     3.1 --- a/src/HOL/Real/rat_arith.ML	Thu Aug 09 15:52:45 2007 +0200
     3.2 +++ b/src/HOL/Real/rat_arith.ML	Thu Aug 09 15:52:47 2007 +0200
     3.3 @@ -44,7 +44,7 @@
     3.4      neqE =  neqE,
     3.5      simpset = simpset addsimps simps
     3.6                        addsimprocs simprocs}) #>
     3.7 -  arith_inj_const ("Nat.of_nat", HOLogic.natT --> ratT) #>
     3.8 -  arith_inj_const ("IntDef.of_int", HOLogic.intT --> ratT)
     3.9 +  arith_inj_const (@{const_name of_nat}, HOLogic.natT --> ratT) #>
    3.10 +  arith_inj_const (@{const_name of_int}, HOLogic.intT --> ratT)
    3.11  
    3.12  end;
     4.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Aug 09 15:52:45 2007 +0200
     4.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Aug 09 15:52:47 2007 +0200
     4.3 @@ -478,7 +478,7 @@
     4.4          val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
     4.5          val t1'         = incr_boundvars 1 t1
     4.6          val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
     4.7 -                            (Const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) $ n)
     4.8 +                            (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
     4.9          val t1_lt_zero  = Const (@{const_name HOL.less},
    4.10                              HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
    4.11          val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
     5.1 --- a/src/HOL/int_arith1.ML	Thu Aug 09 15:52:45 2007 +0200
     5.2 +++ b/src/HOL/int_arith1.ML	Thu Aug 09 15:52:47 2007 +0200
     5.3 @@ -600,7 +600,7 @@
     5.4      simpset = simpset addsimps add_rules
     5.5                        addsimprocs Int_Numeral_Base_Simprocs
     5.6                        addcongs [if_weak_cong]}) #>
     5.7 -  arith_inj_const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) #>
     5.8 +  arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
     5.9    arith_discrete "IntDef.int"
    5.10  
    5.11  end;