src/HOL/Code_Numeral.thy
changeset 58379 c044539a2bda
parent 58377 c6f93b8d2d8e
child 58390 b74d8470b98e
     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Sep 18 16:47:40 2014 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Thu Sep 18 16:57:10 2014 +0200
     1.3 @@ -809,16 +809,24 @@
     1.4    shows P
     1.5    using assms by transfer blast
     1.6  
     1.7 +instantiation natural :: size
     1.8 +begin
     1.9 +
    1.10 +definition size_natural :: "natural \<Rightarrow> nat" where
    1.11 +  [simp, code]: "size_natural = nat_of_natural"
    1.12 +
    1.13 +instance ..
    1.14 +
    1.15 +end
    1.16 +
    1.17  lemma natural_decr [termination_simp]:
    1.18    "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
    1.19    by transfer simp
    1.20  
    1.21 -lemma natural_zero_minus_one:
    1.22 -  "(0::natural) - 1 = 0"
    1.23 -  by simp
    1.24 +lemma natural_zero_minus_one: "(0::natural) - 1 = 0"
    1.25 +  by (rule zero_diff)
    1.26  
    1.27 -lemma Suc_natural_minus_one:
    1.28 -  "Suc n - 1 = n"
    1.29 +lemma Suc_natural_minus_one: "Suc n - 1 = n"
    1.30    by transfer simp
    1.31  
    1.32  hide_const (open) Suc
    1.33 @@ -898,16 +906,13 @@
    1.34    "HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)"
    1.35    by transfer (simp add: equal)
    1.36  
    1.37 -lemma [code nbe]:
    1.38 -  "HOL.equal n (n::natural) \<longleftrightarrow> True"
    1.39 -  by (simp add: equal)
    1.40 +lemma [code nbe]: "HOL.equal n (n::natural) \<longleftrightarrow> True"
    1.41 +  by (rule equal_class.equal_refl)
    1.42  
    1.43 -lemma [code]:
    1.44 -  "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
    1.45 +lemma [code]: "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
    1.46    by transfer simp
    1.47  
    1.48 -lemma [code]:
    1.49 -  "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
    1.50 +lemma [code]: "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
    1.51    by transfer simp
    1.52  
    1.53  hide_const (open) Nat
    1.54 @@ -923,4 +928,3 @@
    1.55    functions integer_of_natural natural_of_integer
    1.56  
    1.57  end
    1.58 -