# HG changeset patch # User blanchet # Date 1411052230 -7200 # Node ID c044539a2bdaa98679044d743b03bee5ade21454 # Parent cf6f16bc11a7b5f8352a104ff8e32c904bb09be7 reintroduced an instantiation of 'size' for 'numerals' diff -r cf6f16bc11a7 -r c044539a2bda src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/Code_Numeral.thy Thu Sep 18 16:57:10 2014 +0200 @@ -809,16 +809,24 @@ shows P using assms by transfer blast +instantiation natural :: size +begin + +definition size_natural :: "natural \ nat" where + [simp, code]: "size_natural = nat_of_natural" + +instance .. + +end + lemma natural_decr [termination_simp]: "n \ 0 \ nat_of_natural n - Nat.Suc 0 < nat_of_natural n" by transfer simp -lemma natural_zero_minus_one: - "(0::natural) - 1 = 0" - by simp +lemma natural_zero_minus_one: "(0::natural) - 1 = 0" + by (rule zero_diff) -lemma Suc_natural_minus_one: - "Suc n - 1 = n" +lemma Suc_natural_minus_one: "Suc n - 1 = n" by transfer simp hide_const (open) Suc @@ -898,16 +906,13 @@ "HOL.equal m n \ HOL.equal (integer_of_natural m) (integer_of_natural n)" by transfer (simp add: equal) -lemma [code nbe]: - "HOL.equal n (n::natural) \ True" - by (simp add: equal) +lemma [code nbe]: "HOL.equal n (n::natural) \ True" + by (rule equal_class.equal_refl) -lemma [code]: - "m \ n \ integer_of_natural m \ integer_of_natural n" +lemma [code]: "m \ n \ integer_of_natural m \ integer_of_natural n" by transfer simp -lemma [code]: - "m < n \ integer_of_natural m < integer_of_natural n" +lemma [code]: "m < n \ integer_of_natural m < integer_of_natural n" by transfer simp hide_const (open) Nat @@ -923,4 +928,3 @@ functions integer_of_natural natural_of_integer end -