Re: [isabelle] Evaluation of List.coset



Dear Jesus,

I had a look at your theories, and there several problems. I have tested my suggestion with Isabelle2013-RC2.

1. You instantiate the type class equal by
definition "equal_bit0 x y = (x = y)"
This is perfectly ok, but then, equality tests will never terminate, because Isabelle's code generator rewrites the right-hand side to equal_bit0 x y.

You should really implement here (or in a code equation) the equality operation, e.g.,

lemma equal_bit0_code [code]:
  "equal_class.equal x y = (Rep_bit0 x = Rep_bit0 y)"
by(simp add: equal_eq Rep_bit0_inject)

lemma equal_bit1_code [code]:
  "equal_class.equal x y = (Rep_bit1 x = Rep_bit1 y)"
by(simp add: equal_eq Rep_bit1_inject)

2. Numeral_Type lifts all operations in terms of Abs_bit0' and Abs_bit1'. Your code equations implement these via of_int, which uses plus and times, which build on Abs_bit0' and Abs_bit1', so there's another source of non-termination. You should really implement them, e.g., like this:

lemma [code abstract]:
  "Rep_bit0 (Abs_bit0' x :: 'a :: {finite, card_UNIV} bit0) =
   x mod int (CARD('a bit0))"
apply(simp add: Abs_bit0'_def)
apply(rule Abs_bit0_inverse)
apply simp
by (metis bit0.Rep_Abs_mod bit0.Rep_less_n card_bit0 of_nat_numeral zmult_int)

lemma [code abstract]:
"Rep_bit1 (Abs_bit1' x :: 'a :: {finite, card_UNIV} bit1) = x mod int (CARD('a bit1))"
apply(simp add: Abs_bit1'_def)
apply(rule Abs_bit1_inverse)
apply simp
by (metis of_nat_0_less_iff of_nat_Suc of_nat_mult of_nat_numeral pos_mod_conj zero_less_Suc)

3. The implementation of Abs_bit0' and Abs_bit1' needs to compute the size of the type, i.e., CARD('a bit). CARD('a bit) is only executable in equations where 'a has sort card_UNIV (this is why 'a has the sort constraint card_UNIV in the above lemmas). In Isabelle2012, it is not executable at all, but will always raise an exception. Hence, you need to make num0, num1, bit0, and bit1 instances of card_UNIV (I leave the instantiation proofs to you).

instantiation bit1 :: (type) finite_UNIV begin
definition "finite_UNIV = Phantom('a bit1) True"
instance sorry
end

instantiation bit1 :: (card_UNIV) card_UNIV begin
definition "card_UNIV = Phantom('a bit1) (1 + 2 * of_phantom ((card_UNIV :: 'a card_UNIV)))"
instance sorry
end

instantiation bit0 :: (type) finite_UNIV begin
definition "finite_UNIV = Phantom('a bit0) True"
instance sorry
end

instantiation bit0 :: (card_UNIV) card_UNIV begin
definition "card_UNIV = Phantom('a bit0) (2 * of_phantom ((card_UNIV :: 'a card_UNIV)))"
instance sorry
end

instantiation num0 :: card_UNIV begin
definition "finite_UNIV = Phantom(num0) False"
definition "card_UNIV = Phantom(num0) 0"
instance sorry
end

instantiation num1 :: card_UNIV begin
definition "finite_UNIV = Phantom(num1) True"
definition "card_UNIV = Phantom(num1) 1"
instance sorry
end

I send attached a file where some examples of evaluations over
"finite_n" types succeed, whereas the same evaluations over
Numeral_Types (bit0 and bit1) do not terminate; in the file can be
also found some instantiations that I missed in the Library (some of
them were required for the bit0 and bit1 types to be evaluated):

- bit0 and bit1 are intances of "equal"
- bit0 and bit1 are instances of "linorder"
- bit0 and bit1 are instances of "enum"
I do agree that the setup for bit0 and bit1 could be improved, but for Isabelle2013, it is too late already. If you produce a working instantiation that addresses these issues, I'm happy to add that to the Isabelle repository such that it becomes part of the release after Isabelle2013.

Best,
Andreas





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