(* 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)}"
  by auto

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

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

lemma Rep_Abs_sat' [simp]: "Rep_sat (Abs_sat' n :: 'a sat) = min (CARD('a)) n"
  unfolding Abs_sat'_def
  by (rule Abs_sat_inverse) simp

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

lemma min_CARD_Rep_sat [simp]: "min CARD('a) (Rep_sat (n::'a sat)) = Rep_sat n"
  by (rule min_max.inf_absorb2 [OF Rep_sat_le_CARD])

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

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

lemma Abs_Rep_sat' [simp, code abstype]:
  "Abs_sat' (Rep_sat n) = n"
  by (simp add: Abs_sat'_def min_CARD_Rep_sat Rep_sat_inverse)

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

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

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

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 = Abs_sat' 0"

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

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

definition
  plus_sat_def: "x + y = Abs_sat' (Rep_sat x + Rep_sat y)"

lemma Rep_plus_sat [simp, code abstract]:
  "Rep_sat (x + y) = min (Rep_sat x + Rep_sat y) CARD('a)"
  by (simp add: plus_sat_def)

definition
  minus_sat_def: "x - y = Abs_sat' (Rep_sat x - Rep_sat y)"

lemma Rep_minus_sat [simp, code abstract]:
  "Rep_sat (x - y) = Rep_sat x - Rep_sat y"
proof -
  from Rep_sat_le_CARD [of x] have "Rep_sat x - Rep_sat y \<le> CARD('a)" by arith
  then show ?thesis by (simp add: minus_sat_def)
qed

definition
  times_sat_def: "x * y = Abs_sat' (Rep_sat x * Rep_sat y)"

lemma Rep_times_sat [simp, code abstract]:
  "Rep_sat (x * y) = min (Rep_sat x * Rep_sat 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> Rep_sat x \<le> Rep_sat y"

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

definition
  less_sat_def: "(x::'a sat) < y \<longleftrightarrow> Rep_sat x < Rep_sat 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 "Rep_sat (x + y) = min (Rep_sat x + Rep_sat 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 "Rep_sat (x * y) = min (Rep_sat x * Rep_sat 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 Rep_sat_1: "Rep_sat 1 = 1"
  unfolding one_sat_def
  by (rule Abs_sat_inverse) simp

instance
apply intro_classes
apply (unfold times_sat_def)
apply (unfold Rep_sat_inject [symmetric])
apply (unfold Rep_Abs_sat' Rep_sat_0 Rep_sat_1)
apply (simp add: min_CARD_Rep_sat)
apply simp
done

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 = Abs_sat' \<circ> nat"

instance ..

end

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

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

instance proof
qed (simp add: equal_sat_def Rep_sat_inject)

end

text{* Code generator setup. *}

code_datatype number_sat_inst.number_of_sat

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

lemma one_nat_code [code, code_unfold_post]:
  "1 = (Numeral1 :: ('a :: card2) sat)"
  apply (simp add: number_of_sat_def Abs_sat'_def one_sat_def Int.Pls_def)
  apply (subst Abs_sat_inject)
  apply simp
  apply simp
  sorry

(*
lemma Suc_code [code]:
  "Suc n = n + 1"
  by simp
*)

declare plus_sat_def[code]

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

code_thms f

export_code
  "f"
in -


lemma plus_sat_code[code]:
  "n + m = nat (of_nat n + of_nat m)"
  by simp


lemma minus_nat_code [code]:
  "n - m = nat (of_nat n - of_nat m)"
  by simp

end