# Re: [isabelle] code generation for saturated naturals

```> Maybe your Abs_sat' can just be called Sat.

When going through Dlist a further suggestion came to my mind:

I have modified the theory further: Abs_sat' is called Sat, and Rep_sat
nat_of.  Both are operations to be expected to be used in »user space«
and should therefore carry readable names.

Hope this helps,
Florian

--

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
```
```(* Author: Brian Huffman *)
(* Version: Isabelle2011 *)

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"

lemma sat_eq_iff:
"m = n \<longleftrightarrow> nat_of m = nat_of n"

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)"

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"

lemma Sat_nat_of [simp]:
"Sat (nat_of n) = n"

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

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

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"

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)"

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)"

instance
apply intro_classes
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))"

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))"

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

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

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
```

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.