Re: [isabelle] code generation for saturated naturals



Hi Peter, hi Brian,

> In his zest to ensure all uses of numerals are algebraically
well-organised, Brian manufactured the attached theory of "saturated"
arithmetic for the naturals for me.
>
> I'm now struggling to get it to work with the code generator. The
problem is that the CARD('a) construct leans on the card function, and
for some reason the code generator wants to enumerate nat while
calculating card. I can't see why it wants to do that. Can you suggest a
way forward? (The attached theory should break at an opportune point.)
>

find attached an experiment of mine which hopefully turn out to be helpful.

First, it is important that we keep such discussions on the public
mailing list, since more eyes see more than less and also to make sure
the generic Isabelle knowledge stays publicly available and is able to grow.

Here now, the answers proper to your issues:

a) avoiding CARD('a) in generated code

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

This connects len_of TYPE('a) to CARD('a) and allows you to generate
code for type 'a::len_card sat.  Of course you have to give appropriate
instantiations, or replace CARD('a) by len_of TYPE('a) in your
specification throughout to gain full flexibility.  @Brian: Did you ever
think about including such a class as len_card into the Word libraries
directly?

b) use abstract type for code generation

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)

(call on me again if this sounds like Bohemian villages for you)

c) prove simp rules for your "abtract" operation of the form:

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

Together with extensionality on sat values, this will greatly simplify
your proofs and make them less cumbersome.  Look at the theory to get
more ideas.

> I humbly suggest that a working version of this theory make its way
into HOL/Library. I'd be happy to round out the theory with some guidance.

Yes, indeed.  I'd first suggest to round up the proofs a little, and
maybe others want to comment also on that.

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

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

Attachment: signature.asc
Description: OpenPGP digital signature



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