# HG changeset patch
# User huffman
# Date 1315750905 25200
# Node ID a7f9c97378b3f1b41c94dfa7efc0d10506fd201e
# Parent  1cbe20966cdb0823507886066b36096de5400869
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'

diff -r 1cbe20966cdb -r a7f9c97378b3 src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Sun Sep 11 15:20:09 2011 +0200
+++ b/src/HOL/Library/Saturated.thy	Sun Sep 11 07:21:45 2011 -0700
@@ -22,16 +22,16 @@
   "m = n \<longleftrightarrow> nat_of m = nat_of n"
   by (simp add: nat_of_inject)
 
-lemma Abs_sa_nat_of [code abstype]:
+lemma Abs_sat_nat_of [code abstype]:
   "Abs_sat (nat_of n) = n"
   by (fact nat_of_inverse)
 
-definition Sat :: "nat \<Rightarrow> 'a::len sat" where
-  "Sat n = Abs_sat (min (len_of TYPE('a)) n)"
+definition Abs_sat' :: "nat \<Rightarrow> 'a::len sat" where
+  "Abs_sat' n = Abs_sat (min (len_of TYPE('a)) n)"
 
-lemma nat_of_Sat [simp]:
-  "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
-  unfolding Sat_def by (rule Abs_sat_inverse) simp
+lemma nat_of_Abs_sat' [simp]:
+  "nat_of (Abs_sat' n :: ('a::len) sat) = min (len_of TYPE('a)) n"
+  unfolding Abs_sat'_def by (rule Abs_sat_inverse) simp
 
 lemma nat_of_le_len_of [simp]:
   "nat_of (n :: ('a::len) sat) \<le> len_of TYPE('a)"
@@ -45,9 +45,9 @@
   "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
   by (subst min_max.inf.commute) simp
 
-lemma Sat_nat_of [simp]:
-  "Sat (nat_of n) = n"
-  by (simp add: Sat_def nat_of_inverse)
+lemma Abs_sat'_nat_of [simp]:
+  "Abs_sat' (nat_of n) = n"
+  by (simp add: Abs_sat'_def nat_of_inverse)
 
 instantiation sat :: (len) linorder
 begin
@@ -67,10 +67,10 @@
 begin
 
 definition
-  "0 = Sat 0"
+  "0 = Abs_sat' 0"
 
 definition
-  "1 = Sat 1"
+  "1 = Abs_sat' 1"
 
 lemma nat_of_zero_sat [simp, code abstract]:
   "nat_of 0 = 0"
@@ -81,14 +81,14 @@
   by (simp add: one_sat_def)
 
 definition
-  "x + y = Sat (nat_of x + nat_of y)"
+  "x + y = Abs_sat' (nat_of x + nat_of y)"
 
 lemma nat_of_plus_sat [simp, code abstract]:
   "nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))"
   by (simp add: plus_sat_def)
 
 definition
-  "x - y = Sat (nat_of x - nat_of y)"
+  "x - y = Abs_sat' (nat_of x - nat_of y)"
 
 lemma nat_of_minus_sat [simp, code abstract]:
   "nat_of (x - y) = nat_of x - nat_of y"
@@ -98,7 +98,7 @@
 qed
 
 definition
-  "x * y = Sat (nat_of x * nat_of y)"
+  "x * y = Abs_sat' (nat_of x * nat_of y)"
 
 lemma nat_of_times_sat [simp, code abstract]:
   "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
@@ -145,9 +145,16 @@
 
 end
 
-lemma Sat_eq_of_nat: "Sat n = of_nat n"
+lemma Abs_sat'_eq_of_nat: "Abs_sat' n = of_nat n"
   by (rule sat_eqI, induct n, simp_all)
 
+abbreviation Sat :: "nat \<Rightarrow> 'a::len sat" where
+  "Sat \<equiv> of_nat"
+
+lemma nat_of_Sat [simp]:
+  "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
+  by (rule nat_of_Abs_sat' [unfolded Abs_sat'_eq_of_nat])
+
 instantiation sat :: (len) number_semiring
 begin
 
@@ -155,7 +162,7 @@
   number_of_sat_def [code del]: "number_of = Sat \<circ> nat"
 
 instance
-  by default (simp add: number_of_sat_def Sat_eq_of_nat)
+  by default (simp add: number_of_sat_def)
 
 end