(* 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 \ m = n" by (simp add: nat_of_inject) lemma sat_eq_iff: "m = n \ 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 \ '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) \ 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 \ 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 \ y \ nat_of x \ nat_of y" text {* This formulation is much more nicer for unfolding *} definition less_sat_def: "(x::'a sat) < y \ 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 \ y \ y \ 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 \ nat" instance .. end instantiation sat :: (type) equal (*<*) begin definition "HOL.equal A B \ 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 \ 1 + 0" text {* Add missing instantiations for @{class len_card} *} end