wenzelm@45692: (*  Title:      HOL/Library/Saturated.thy
wenzelm@45692:     Author:     Brian Huffman
wenzelm@45692:     Author:     Peter Gammie
wenzelm@45692:     Author:     Florian Haftmann
wenzelm@45692: *)
haftmann@44819: 
haftmann@44819: header {* Saturated arithmetic *}
haftmann@44819: 
haftmann@44819: theory Saturated
haftmann@44819: imports Main "~~/src/HOL/Library/Numeral_Type" "~~/src/HOL/Word/Type_Length"
haftmann@44819: begin
haftmann@44819: 
haftmann@44819: subsection {* The type of saturated naturals *}
haftmann@44819: 
haftmann@44819: typedef (open) ('a::len) sat = "{.. len_of TYPE('a)}"
haftmann@44819:   morphisms nat_of Abs_sat
haftmann@44819:   by auto
haftmann@44819: 
haftmann@44819: lemma sat_eqI:
haftmann@44819:   "nat_of m = nat_of n \<Longrightarrow> m = n"
haftmann@44819:   by (simp add: nat_of_inject)
haftmann@44819: 
haftmann@44819: lemma sat_eq_iff:
haftmann@44819:   "m = n \<longleftrightarrow> nat_of m = nat_of n"
haftmann@44819:   by (simp add: nat_of_inject)
haftmann@44819: 
huffman@44883: lemma Abs_sat_nat_of [code abstype]:
haftmann@44819:   "Abs_sat (nat_of n) = n"
haftmann@44819:   by (fact nat_of_inverse)
haftmann@44819: 
huffman@44883: definition Abs_sat' :: "nat \<Rightarrow> 'a::len sat" where
huffman@44883:   "Abs_sat' n = Abs_sat (min (len_of TYPE('a)) n)"
haftmann@44819: 
huffman@44883: lemma nat_of_Abs_sat' [simp]:
huffman@44883:   "nat_of (Abs_sat' n :: ('a::len) sat) = min (len_of TYPE('a)) n"
huffman@44883:   unfolding Abs_sat'_def by (rule Abs_sat_inverse) simp
haftmann@44819: 
haftmann@44819: lemma nat_of_le_len_of [simp]:
haftmann@44819:   "nat_of (n :: ('a::len) sat) \<le> len_of TYPE('a)"
haftmann@44819:   using nat_of [where x = n] by simp
haftmann@44819: 
haftmann@44819: lemma min_len_of_nat_of [simp]:
haftmann@44819:   "min (len_of TYPE('a)) (nat_of (n::('a::len) sat)) = nat_of n"
haftmann@44819:   by (rule min_max.inf_absorb2 [OF nat_of_le_len_of])
haftmann@44819: 
haftmann@44819: lemma min_nat_of_len_of [simp]:
haftmann@44819:   "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
haftmann@44819:   by (subst min_max.inf.commute) simp
haftmann@44819: 
huffman@44883: lemma Abs_sat'_nat_of [simp]:
huffman@44883:   "Abs_sat' (nat_of n) = n"
huffman@44883:   by (simp add: Abs_sat'_def nat_of_inverse)
haftmann@44819: 
haftmann@44819: instantiation sat :: (len) linorder
haftmann@44819: begin
haftmann@44819: 
haftmann@44819: definition
haftmann@44819:   less_eq_sat_def: "x \<le> y \<longleftrightarrow> nat_of x \<le> nat_of y"
haftmann@44819: 
haftmann@44819: definition
haftmann@44819:   less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
haftmann@44819: 
haftmann@44819: instance
haftmann@44819: by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
haftmann@44819: 
haftmann@44819: end
haftmann@44819: 
huffman@44849: instantiation sat :: (len) "{minus, comm_semiring_1}"
haftmann@44819: begin
haftmann@44819: 
haftmann@44819: definition
huffman@44883:   "0 = Abs_sat' 0"
haftmann@44819: 
haftmann@44819: definition
huffman@44883:   "1 = Abs_sat' 1"
haftmann@44819: 
haftmann@44819: lemma nat_of_zero_sat [simp, code abstract]:
haftmann@44819:   "nat_of 0 = 0"
haftmann@44819:   by (simp add: zero_sat_def)
haftmann@44819: 
haftmann@44819: lemma nat_of_one_sat [simp, code abstract]:
haftmann@44819:   "nat_of 1 = min 1 (len_of TYPE('a))"
haftmann@44819:   by (simp add: one_sat_def)
haftmann@44819: 
haftmann@44819: definition
huffman@44883:   "x + y = Abs_sat' (nat_of x + nat_of y)"
haftmann@44819: 
haftmann@44819: lemma nat_of_plus_sat [simp, code abstract]:
haftmann@44819:   "nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))"
haftmann@44819:   by (simp add: plus_sat_def)
haftmann@44819: 
haftmann@44819: definition
huffman@44883:   "x - y = Abs_sat' (nat_of x - nat_of y)"
haftmann@44819: 
haftmann@44819: lemma nat_of_minus_sat [simp, code abstract]:
haftmann@44819:   "nat_of (x - y) = nat_of x - nat_of y"
haftmann@44819: proof -
haftmann@44819:   from nat_of_le_len_of [of x] have "nat_of x - nat_of y \<le> len_of TYPE('a)" by arith
haftmann@44819:   then show ?thesis by (simp add: minus_sat_def)
haftmann@44819: qed
haftmann@44819: 
haftmann@44819: definition
huffman@44883:   "x * y = Abs_sat' (nat_of x * nat_of y)"
haftmann@44819: 
haftmann@44819: lemma nat_of_times_sat [simp, code abstract]:
haftmann@44819:   "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
haftmann@44819:   by (simp add: times_sat_def)
haftmann@44819: 
haftmann@44819: instance proof
haftmann@44819:   fix a b c :: "('a::len) sat"
haftmann@44819:   show "a * b * c = a * (b * c)"
haftmann@44819:   proof(cases "a = 0")
haftmann@44819:     case True thus ?thesis by (simp add: sat_eq_iff)
haftmann@44819:   next
haftmann@44819:     case False show ?thesis
haftmann@44819:     proof(cases "c = 0")
haftmann@44819:       case True thus ?thesis by (simp add: sat_eq_iff)
haftmann@44819:     next
haftmann@44819:       case False with `a \<noteq> 0` show ?thesis
haftmann@44819:         by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult_assoc min_max.inf_assoc min_max.inf_absorb2)
haftmann@44819:     qed
haftmann@44819:   qed
haftmann@44819: next
haftmann@44819:   fix a :: "('a::len) sat"
haftmann@44819:   show "1 * a = a"
haftmann@44819:     apply (simp add: sat_eq_iff)
haftmann@44819:     apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min_max.le_iff_inf min_nat_of_len_of nat_mult_1_right nat_mult_commute)
haftmann@44819:     done
haftmann@44819: next
haftmann@44819:   fix a b c :: "('a::len) sat"
haftmann@44819:   show "(a + b) * c = a * c + b * c"
haftmann@44819:   proof(cases "c = 0")
haftmann@44819:     case True thus ?thesis by (simp add: sat_eq_iff)
haftmann@44819:   next
haftmann@44819:     case False thus ?thesis
huffman@44848:       by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min_max.inf_assoc min_max.inf_absorb2)
haftmann@44819:   qed
haftmann@44819: qed (simp_all add: sat_eq_iff mult.commute)
haftmann@44819: 
haftmann@44819: end
haftmann@44819: 
haftmann@44819: instantiation sat :: (len) ordered_comm_semiring
haftmann@44819: begin
haftmann@44819: 
haftmann@44819: instance
haftmann@44819: by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
haftmann@44819: 
haftmann@44819: end
haftmann@44819: 
huffman@44883: lemma Abs_sat'_eq_of_nat: "Abs_sat' n = of_nat n"
huffman@44849:   by (rule sat_eqI, induct n, simp_all)
huffman@44849: 
huffman@44883: abbreviation Sat :: "nat \<Rightarrow> 'a::len sat" where
huffman@44883:   "Sat \<equiv> of_nat"
huffman@44883: 
huffman@44883: lemma nat_of_Sat [simp]:
huffman@44883:   "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
huffman@44883:   by (rule nat_of_Abs_sat' [unfolded Abs_sat'_eq_of_nat])
huffman@44883: 
huffman@44849: instantiation sat :: (len) number_semiring
haftmann@44819: begin
haftmann@44819: 
haftmann@44819: definition
haftmann@44819:   number_of_sat_def [code del]: "number_of = Sat \<circ> nat"
haftmann@44819: 
huffman@44849: instance
huffman@44883:   by default (simp add: number_of_sat_def)
haftmann@44819: 
haftmann@44819: end
haftmann@44819: 
haftmann@44819: lemma [code abstract]:
haftmann@44819:   "nat_of (number_of n :: ('a::len) sat) = min (nat n) (len_of TYPE('a))"
haftmann@44819:   unfolding number_of_sat_def by simp
haftmann@44819: 
haftmann@44819: instance sat :: (len) finite
haftmann@44819: proof
haftmann@44819:   show "finite (UNIV::'a sat set)"
haftmann@44819:     unfolding type_definition.univ [OF type_definition_sat]
haftmann@44819:     using finite by simp
haftmann@44819: qed
haftmann@44819: 
haftmann@44819: instantiation sat :: (len) equal
haftmann@44819: begin
haftmann@44819: 
haftmann@44819: definition
haftmann@44819:   "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
haftmann@44819: 
haftmann@44819: instance proof
haftmann@44819: qed (simp add: equal_sat_def nat_of_inject)
haftmann@44819: 
haftmann@44819: end
haftmann@44819: 
haftmann@44819: instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
haftmann@44819: begin
haftmann@44819: 
haftmann@44819: definition
haftmann@44819:   "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
haftmann@44819: 
haftmann@44819: definition
haftmann@44819:   "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
haftmann@44819: 
haftmann@44819: definition
haftmann@44819:   "bot = (0 :: 'a sat)"
haftmann@44819: 
haftmann@44819: definition
haftmann@44819:   "top = Sat (len_of TYPE('a))"
haftmann@44819: 
haftmann@44819: instance proof
haftmann@44819: qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def min_max.sup_inf_distrib1,
haftmann@44819:   simp_all add: less_eq_sat_def)
haftmann@44819: 
haftmann@44819: end
haftmann@44819: 
haftmann@44819: instantiation sat :: (len) complete_lattice
haftmann@44819: begin
haftmann@44819: 
haftmann@44819: definition
haftmann@45994:   "Inf (A :: 'a sat set) = Finite_Set.fold min top A"
haftmann@44819: 
haftmann@44819: definition
haftmann@45994:   "Sup (A :: 'a sat set) = Finite_Set.fold max bot A"
haftmann@44819: 
haftmann@44819: instance proof
haftmann@44819:   fix x :: "'a sat"
haftmann@44819:   fix A :: "'a sat set"
haftmann@44819:   note finite
haftmann@44819:   moreover assume "x \<in> A"
haftmann@45994:   ultimately have "Finite_Set.fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf)
haftmann@44819:   then show "Inf A \<le> x" by (simp add: Inf_sat_def)
haftmann@44819: next
haftmann@44819:   fix z :: "'a sat"
haftmann@44819:   fix A :: "'a sat set"
haftmann@44819:   note finite
haftmann@44819:   moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
haftmann@45994:   ultimately have "min z top \<le> Finite_Set.fold min top A" by (blast intro: min_max.inf_le_fold_inf)
haftmann@44819:   then show "z \<le> Inf A" by (simp add: Inf_sat_def min_def)
haftmann@44819: next
haftmann@44819:   fix x :: "'a sat"
haftmann@44819:   fix A :: "'a sat set"
haftmann@44819:   note finite
haftmann@44819:   moreover assume "x \<in> A"
haftmann@45994:   ultimately have "max x bot \<le> Finite_Set.fold max bot A" by (rule min_max.sup_le_fold_sup)
haftmann@44819:   then show "x \<le> Sup A" by (simp add: Sup_sat_def)
haftmann@44819: next
haftmann@44819:   fix z :: "'a sat"
haftmann@44819:   fix A :: "'a sat set"
haftmann@44819:   note finite
haftmann@44819:   moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
haftmann@45994:   ultimately have "Finite_Set.fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup)
haftmann@44819:   then show "Sup A \<le> z" by (simp add: Sup_sat_def max_def bot_unique)
haftmann@44819: qed
haftmann@44819: 
haftmann@44819: end
haftmann@44819: 
haftmann@44819: end