Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
authorhuffman
Sun Sep 11 07:21:45 2011 -0700 (2011-09-11)
changeset 44883a7f9c97378b3
parent 44878 1cbe20966cdb
child 44884 02efd5a6b6e5
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
src/HOL/Library/Saturated.thy
     1.1 --- a/src/HOL/Library/Saturated.thy	Sun Sep 11 15:20:09 2011 +0200
     1.2 +++ b/src/HOL/Library/Saturated.thy	Sun Sep 11 07:21:45 2011 -0700
     1.3 @@ -22,16 +22,16 @@
     1.4    "m = n \<longleftrightarrow> nat_of m = nat_of n"
     1.5    by (simp add: nat_of_inject)
     1.6  
     1.7 -lemma Abs_sa_nat_of [code abstype]:
     1.8 +lemma Abs_sat_nat_of [code abstype]:
     1.9    "Abs_sat (nat_of n) = n"
    1.10    by (fact nat_of_inverse)
    1.11  
    1.12 -definition Sat :: "nat \<Rightarrow> 'a::len sat" where
    1.13 -  "Sat n = Abs_sat (min (len_of TYPE('a)) n)"
    1.14 +definition Abs_sat' :: "nat \<Rightarrow> 'a::len sat" where
    1.15 +  "Abs_sat' n = Abs_sat (min (len_of TYPE('a)) n)"
    1.16  
    1.17 -lemma nat_of_Sat [simp]:
    1.18 -  "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
    1.19 -  unfolding Sat_def by (rule Abs_sat_inverse) simp
    1.20 +lemma nat_of_Abs_sat' [simp]:
    1.21 +  "nat_of (Abs_sat' n :: ('a::len) sat) = min (len_of TYPE('a)) n"
    1.22 +  unfolding Abs_sat'_def by (rule Abs_sat_inverse) simp
    1.23  
    1.24  lemma nat_of_le_len_of [simp]:
    1.25    "nat_of (n :: ('a::len) sat) \<le> len_of TYPE('a)"
    1.26 @@ -45,9 +45,9 @@
    1.27    "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
    1.28    by (subst min_max.inf.commute) simp
    1.29  
    1.30 -lemma Sat_nat_of [simp]:
    1.31 -  "Sat (nat_of n) = n"
    1.32 -  by (simp add: Sat_def nat_of_inverse)
    1.33 +lemma Abs_sat'_nat_of [simp]:
    1.34 +  "Abs_sat' (nat_of n) = n"
    1.35 +  by (simp add: Abs_sat'_def nat_of_inverse)
    1.36  
    1.37  instantiation sat :: (len) linorder
    1.38  begin
    1.39 @@ -67,10 +67,10 @@
    1.40  begin
    1.41  
    1.42  definition
    1.43 -  "0 = Sat 0"
    1.44 +  "0 = Abs_sat' 0"
    1.45  
    1.46  definition
    1.47 -  "1 = Sat 1"
    1.48 +  "1 = Abs_sat' 1"
    1.49  
    1.50  lemma nat_of_zero_sat [simp, code abstract]:
    1.51    "nat_of 0 = 0"
    1.52 @@ -81,14 +81,14 @@
    1.53    by (simp add: one_sat_def)
    1.54  
    1.55  definition
    1.56 -  "x + y = Sat (nat_of x + nat_of y)"
    1.57 +  "x + y = Abs_sat' (nat_of x + nat_of y)"
    1.58  
    1.59  lemma nat_of_plus_sat [simp, code abstract]:
    1.60    "nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))"
    1.61    by (simp add: plus_sat_def)
    1.62  
    1.63  definition
    1.64 -  "x - y = Sat (nat_of x - nat_of y)"
    1.65 +  "x - y = Abs_sat' (nat_of x - nat_of y)"
    1.66  
    1.67  lemma nat_of_minus_sat [simp, code abstract]:
    1.68    "nat_of (x - y) = nat_of x - nat_of y"
    1.69 @@ -98,7 +98,7 @@
    1.70  qed
    1.71  
    1.72  definition
    1.73 -  "x * y = Sat (nat_of x * nat_of y)"
    1.74 +  "x * y = Abs_sat' (nat_of x * nat_of y)"
    1.75  
    1.76  lemma nat_of_times_sat [simp, code abstract]:
    1.77    "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
    1.78 @@ -145,9 +145,16 @@
    1.79  
    1.80  end
    1.81  
    1.82 -lemma Sat_eq_of_nat: "Sat n = of_nat n"
    1.83 +lemma Abs_sat'_eq_of_nat: "Abs_sat' n = of_nat n"
    1.84    by (rule sat_eqI, induct n, simp_all)
    1.85  
    1.86 +abbreviation Sat :: "nat \<Rightarrow> 'a::len sat" where
    1.87 +  "Sat \<equiv> of_nat"
    1.88 +
    1.89 +lemma nat_of_Sat [simp]:
    1.90 +  "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
    1.91 +  by (rule nat_of_Abs_sat' [unfolded Abs_sat'_eq_of_nat])
    1.92 +
    1.93  instantiation sat :: (len) number_semiring
    1.94  begin
    1.95  
    1.96 @@ -155,7 +162,7 @@
    1.97    number_of_sat_def [code del]: "number_of = Sat \<circ> nat"
    1.98  
    1.99  instance
   1.100 -  by default (simp add: number_of_sat_def Sat_eq_of_nat)
   1.101 +  by default (simp add: number_of_sat_def)
   1.102  
   1.103  end
   1.104