src/HOL/Library/Saturated.thy
changeset 47108 2a1953f0d20d
parent 45994 38a46e029784
child 49834 b27bbb021df1
     1.1 --- a/src/HOL/Library/Saturated.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Library/Saturated.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -157,20 +157,16 @@
     1.4    "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
     1.5    by (rule nat_of_Abs_sat' [unfolded Abs_sat'_eq_of_nat])
     1.6  
     1.7 -instantiation sat :: (len) number_semiring
     1.8 -begin
     1.9 +lemma [code_abbrev]:
    1.10 +  "of_nat (numeral k) = (numeral k :: 'a::len sat)"
    1.11 +  by simp
    1.12  
    1.13 -definition
    1.14 -  number_of_sat_def [code del]: "number_of = Sat \<circ> nat"
    1.15 -
    1.16 -instance
    1.17 -  by default (simp add: number_of_sat_def)
    1.18 -
    1.19 -end
    1.20 +definition sat_of_nat :: "nat \<Rightarrow> ('a::len) sat"
    1.21 +  where [code_abbrev]: "sat_of_nat = of_nat"
    1.22  
    1.23  lemma [code abstract]:
    1.24 -  "nat_of (number_of n :: ('a::len) sat) = min (nat n) (len_of TYPE('a))"
    1.25 -  unfolding number_of_sat_def by simp
    1.26 +  "nat_of (sat_of_nat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
    1.27 +  by (simp add: sat_of_nat_def)
    1.28  
    1.29  instance sat :: (len) finite
    1.30  proof
    1.31 @@ -252,4 +248,6 @@
    1.32  
    1.33  end
    1.34  
    1.35 +hide_const (open) sat_of_nat
    1.36 +
    1.37  end