src/HOL/Code_Numeral.thy
changeset 58390 b74d8470b98e
parent 58379 c044539a2bda
child 58399 c5430cf9aa87
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Sep 19 13:27:04 2014 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Sep 19 13:27:04 2014 +0200
     1.3 @@ -809,15 +809,19 @@
     1.4    shows P
     1.5    using assms by transfer blast
     1.6  
     1.7 -instantiation natural :: size
     1.8 -begin
     1.9 +lemma [simp, code]: "size_natural = nat_of_natural"
    1.10 +proof (rule ext)
    1.11 +  fix n
    1.12 +  show "size_natural n = nat_of_natural n"
    1.13 +    by (induct n) simp_all
    1.14 +qed
    1.15  
    1.16 -definition size_natural :: "natural \<Rightarrow> nat" where
    1.17 -  [simp, code]: "size_natural = nat_of_natural"
    1.18 -
    1.19 -instance ..
    1.20 -
    1.21 -end
    1.22 +lemma [simp, code]: "size = nat_of_natural"
    1.23 +proof (rule ext)
    1.24 +  fix n
    1.25 +  show "size n = nat_of_natural n"
    1.26 +    by (induct n) simp_all
    1.27 +qed
    1.28  
    1.29  lemma natural_decr [termination_simp]:
    1.30    "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"