src/HOL/Code_Numeral.thy
changeset 67332 cb96edae56ef
parent 66886 960509bfd47e
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Code_Numeral.thy	Tue Jan 02 23:04:15 2018 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Wed Jan 03 11:06:13 2018 +0100
     1.3 @@ -938,19 +938,14 @@
     1.4    shows P
     1.5    using assms by transfer blast
     1.6  
     1.7 -lemma [simp, code]: "size_natural = nat_of_natural"
     1.8 -proof (rule ext)
     1.9 -  fix n
    1.10 -  show "size_natural n = nat_of_natural n"
    1.11 -    by (induct n) simp_all
    1.12 -qed
    1.13 +instantiation natural :: size
    1.14 +begin
    1.15  
    1.16 -lemma [simp, code]: "size = nat_of_natural"
    1.17 -proof (rule ext)
    1.18 -  fix n
    1.19 -  show "size n = nat_of_natural n"
    1.20 -    by (induct n) simp_all
    1.21 -qed
    1.22 +definition size_nat where [simp, code]: "size_nat = nat_of_natural"
    1.23 +
    1.24 +instance ..
    1.25 +
    1.26 +end
    1.27  
    1.28  lemma natural_decr [termination_simp]:
    1.29    "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"