(* Author: Brian Huffman *)
(* Version: Isabelle2011 *)

header {* Saturated arithmetic *}

theory Saturated
imports Main "~~/src/HOL/Library/Numeral_Type" "~~/src/HOL/Word/Type_Length"
begin

typedef (open) 'a sat = "{.. CARD('a)}"
  morphisms nat_of Abs_sat
  by auto

text {* Suggestion: use extensionality in primitive proofs about @{typ "'a sat"} *}

lemma sat_eqI:
  "nat_of m = nat_of n \<Longrightarrow> m = n"
  by (simp add: nat_of_inject)

lemma sat_eq_iff:
  "m = n \<longleftrightarrow> nat_of m = nat_of n"
  by (simp add: nat_of_inject)

text {* Suggestion: Use code generation for abstract types *}

lemma [code abstype]:
  "Abs_sat (nat_of n) = n"
  by (fact nat_of_inverse)

definition Sat :: "nat \<Rightarrow> 'a sat" where
  "Sat n = Abs_sat (min CARD('a) n)"

text {* More simp rules are admissible and helpful *}

lemma nat_of_Sat [simp]: "nat_of (Sat n :: 'a sat) = min (CARD('a)) n"
  unfolding Sat_def
  by (rule Abs_sat_inverse) simp

lemma nat_of_le_CARD [simp]: "nat_of (n :: 'a sat) \<le> CARD('a)"
  using nat_of [where x=n] by simp

lemma min_CARD_nat_of [simp]: "min CARD('a) (nat_of (n::'a sat)) = nat_of n"
  by (rule min_max.inf_absorb2 [OF nat_of_le_CARD])

lemma min_nat_of_CARD [simp]: "min (nat_of (n::'a sat)) CARD('a) = nat_of n"
  by (simp add: min_max.inf.commute)

lemma Sat_nat_of [simp]:
  "Sat (nat_of n) = n"
  by (simp add: Sat_def nat_of_inverse)

text {* Suggestion: may can be generalized to class @{class linordered_semiring} *}

lemma nat_mult_min_left:
  fixes x y z :: nat
  shows "min x y * z = min (x * z) (y * z)"
  unfolding min_def by simp

lemma nat_mult_min_right:
  fixes x y z :: nat
  shows "x * min y z = min (x * y) (x * z)"
  unfolding min_def by simp

lemma nat_add_min_left:
  fixes x y z :: nat
  shows "min x y + z = min (x + z) (y + z)"
  unfolding min_def by simp

lemma nat_add_min_right:
  fixes x y z :: nat
  shows "x + min y z = min (x + y) (x + z)"
  unfolding min_def by simp

instantiation sat :: (type) "{minus, comm_semiring_0}"
begin

definition
  zero_sat_def: "0 = Sat 0"

text {* Prove the @{text "Rep ..."} lemmas immediately and use for code generation *}

lemma nat_of_zero_sat [simp, code abstract]:
  "nat_of 0 = 0"
  by (simp add: zero_sat_def)

definition
  plus_sat_def: "x + y = 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) CARD('a)"
  by (simp add: plus_sat_def)

definition
  minus_sat_def: "x - y = 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"
proof -
  from nat_of_le_CARD [of x] have "nat_of x - nat_of y \<le> CARD('a)" by arith
  then show ?thesis by (simp add: minus_sat_def)
qed

definition
  times_sat_def: "x * y = 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) CARD('a)"
  by (simp add: times_sat_def)

instance
apply intro_classes
apply (simp_all add: sat_eq_iff mult.commute)
txt {* Here two subgoals algebraic goals about @{const min} survive, which should possible to be tracked to generic lemmas; still some work, but a vast improvement over the previous apply proof *}
sorry

end

instantiation sat :: (type) ordered_comm_semiring
begin

definition
  less_eq_sat_def: "x \<le> y \<longleftrightarrow> nat_of x \<le> nat_of y"

text {* This formulation is much more nicer for unfolding *}

definition
  less_sat_def: "(x::'a sat) < y \<longleftrightarrow> nat_of x < nat_of y"

instance
apply intro_classes
apply (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff)
txt {* use proper Isar proof *}
sorry

end

text {* Here an experiment on code generation: *}

code_thms "Saturated._" -- {* There is still @{text card} for @{const plus} and @{const times} *}

class len_card = len +
  assumes len_of_card: "len_of TYPE('a) = CARD('a)"

lemma plus_sat_code [code abstract]:
  fixes x y :: "'a::len_card sat"
  shows "nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))"
  by (simp add: len_of_card)

lemma times_sat_code [code abstract]:
  fixes x y :: "'a::len_card sat"
  shows "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
  by (simp add: len_of_card)

export_code "Saturated._" in Haskell file - -- {* Heureka! *}

instance sat :: (type) linorder
proof
  fix x y :: "'a sat"
  show "x \<le> y \<or> y \<le> x"
    unfolding less_eq_sat_def
    by (rule linear)
qed

instantiation sat :: (finite) comm_semiring_1
begin

definition
  one_sat_def: "1 = Abs_sat 1"

lemma nat_of_1 [simp, code abstract]: "nat_of 1 = 1"
  unfolding one_sat_def
  by (rule Abs_sat_inverse) simp

instance proof
qed (auto simp add: sat_eq_iff)

end

instance sat :: (type) finite
proof
  show "finite (UNIV::'a sat set)"
    unfolding type_definition.univ [OF type_definition_sat]
    using finite by simp
qed

instantiation sat :: (type) number
begin

definition
  number_of_sat_def [code del]: "number_of = Sat \<circ> nat"

instance ..

end

instantiation sat :: (type) equal
(*<*)
begin

definition
  "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"

instance proof
qed (simp add: equal_sat_def nat_of_inject)

end

text{* Code generator setup. *}

lemma zero_nat_code [code, code_unfold_post]:
  "0 = (Numeral0 :: 'a sat)"
  by (simp add: sat_eq_iff number_of_sat_def Int.Pls_def)


lemma one_nat_code [code, code_unfold_post]:
  "1 = (Numeral1 :: ('a :: card2) sat)"
  apply (simp add: sat_eq_iff number_of_sat_def Int.Pls_def Int.Bit1_def)
  apply (simp add: min_def) apply auto
  sorry

definition
  f :: "2 sat"
where
  "f \<equiv> 1 + 0"

text {* Add missing instantiations for @{class len_card} *}

end
