src/HOL/Nat.thy
changeset 52289 83ce5d2841e7
parent 51329 4a3c453f99a1
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/Nat.thy	Sun Jun 02 10:57:21 2013 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sun Jun 02 20:44:55 2013 +0200
     1.3 @@ -456,7 +456,8 @@
     1.4  end
     1.5  
     1.6  instance nat :: no_top
     1.7 -  by default (auto intro: less_Suc_eq_le[THEN iffD2])
     1.8 +  by default (auto intro: less_Suc_eq_le [THEN iffD2])
     1.9 +
    1.10  
    1.11  subsubsection {* Introduction properties *}
    1.12  
    1.13 @@ -714,10 +715,9 @@
    1.14  text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
    1.15  instance nat :: linordered_semidom
    1.16  proof
    1.17 -  fix i j k :: nat
    1.18    show "0 < (1::nat)" by simp
    1.19 -  show "i \<le> j ==> k + i \<le> k + j" by simp
    1.20 -  show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
    1.21 +  show "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
    1.22 +  show "\<And>m n q :: nat. m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
    1.23  qed
    1.24  
    1.25  instance nat :: no_zero_divisors
    1.26 @@ -1067,6 +1067,11 @@
    1.27  lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
    1.28    by (auto simp: le_add1 dest!: le_add_diff_inverse sym [of _ n])
    1.29  
    1.30 +instance nat :: ordered_cancel_comm_monoid_diff
    1.31 +proof
    1.32 +  show "\<And>m n :: nat. m \<le> n \<longleftrightarrow> (\<exists>q. n = m + q)" by (fact le_iff_add)
    1.33 +qed
    1.34 +
    1.35  lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
    1.36  by (rule le_less_trans, rule diff_le_self)
    1.37