Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Evaluation of List.coset

view this post on Zulip Email Gateway (Aug 19 2022 at 09:45):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Jesus,

By default, Isabelle represents sets as the list of its elements
(constructor set) or of the complement (List.coset). The latter is
mainly needed for representing UNIV as "List.coset []". Of course, you
can implement List.coset in terms of set and enum, but then, you can
only evaluate sets whose element type is an instance of enum - at least
with the present setup for the code generator.

If you want this, you must do the following:

  1. Declare List.set as the only implementation constructor for sets:
    code_datatype set

  2. Remove all code equations that pattern-match on List.coset, e.g.,
    declare union_coset_filter[code del]

You can look in List.thy for which code equation pattern-match on
List.coset, or print the whole code generator setup.

  1. Implement List.coset as you have already tried. This will pull in the
    enum type class in many of the code equations for sets, so you will be
    restricted to elements of type enum, which excludes, e.g., nat.

Best,
Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 09:45):

From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Hi Andreas,

thanks for your explanation.

In the Isabelle development version I observed that the file
"Cardinality.thy" has suffered some changes related to the behaviour
of "List.coset"; more concretely, the line 467 in
http://isabelle.in.tum.de/repos/isabelle/file/744934b818c7/src/HOL/Library/Cardinality.thy
proves some results about "List.coset" of enumerated types "by eval";

does this means that in the incoming release of Isabelle 2013
"List.coset" will be really evaluated for "enum" types?

Looking forward for Isabelle 2013 ;-),

Jesus

view this post on Zulip Email Gateway (Aug 19 2022 at 09:45):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jesus,

No, I have adapted Cardinality such that equality and subset between
sets and complements can be evaluated (cf. changeset 9014e78ccde2),
provided that the element type instatiates the new type class card_UNIV.
There's no enumeration involved.

Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 09:45):

From: Makarius <makarius@sketis.net>
You can start using Isabelle2013-RC2 right now, see again
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-January/msg00157.html

It also points to https://bitbucket.org/isabelle_project/isabelle-release
which collects relevant information about this final stage before
lift-off of the final Isabelle2013 release.

Anything you see on the main Isabelle repository happening now is for the
release after it (but 744934b818c7 mentioned above is from long ago).

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 09:49):

From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Thanks Andreas and Makarius for your hints.

Andreas, just to make it clear, a type which has been proven to be an
instance of "enum" (and also with a finite cardinal, of course) could
be proved to be an instance of the new class "card_UNIV"?

Then, "List.coset" should be evaluated for instances of the
"card_UNIV" type class?

My intuition is that the following question is related to the previous one;

The following command:

value "remdups [finite_5.a_1,finite_5.a_2,finite_5.a_3]"

successfully removes duplicates from the input list (none in this
case), whereas the following one (I had to prove the bit0 and bit1
type constructors to be instances of "equal", and also some code
abstype and code abstract lemmas for Abs_bit1, Abs_bit0, Rep_bit0 and
Rep_bit1 type morphisms):

value "remdups [1::5,2::5,1::5]"

does not produce any output.

What information is missed in the code generator to evaluate
successfully the previous command? Is it related to the cardinal of
the underlying type, which is needed to compute the representation of
the "1::5", "2::5" or "7::5" elements?

As a more general question, in the HOL library, in file "Enum.thy"
there are defined "datatypes" finite_1 up to finite_5, which are
defined by enumerating its constants (a1, a1 and a2, and so on). Then,
in "Numeral_Type.thy", there are generic ordinal types (for any
n::nat) defined ("typedef"), in terms of a bit0 and bit1
representation, as subsets of the integers.

Could not be the types "finite_n" be seen as particular cases of the
ordinal types? Are there good reasons to stick with the "finite_n"
types, being the ordinals far more general?

Sorry for the long mail, I have been a few days working with both
kinds of types and still am a bit confused,

thanks for any help,

Jesus

view this post on Zulip Email Gateway (Aug 19 2022 at 09:50):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Jesus,
On 01/30/2013 07:49 PM, Jesus Aransay wrote:

Andreas, just to make it clear, a type which has been proven to be an
instance of "enum" (and also with a finite cardinal, of course) could
be proved to be an instance of the new class "card_UNIV"?
The card_UNIV type class is only definitional, i.e., every type can be
shown an instance of it. The type class card_UNIV merely defines an
overloaded constant card_UNIV with the meaning of card (UNIV :: 'a set)
which the different instantiations can implement as needed, e.g.
card_UNIV = 2 for bool, card_UNIV = 256 for char and card_UNIV =
card_UNIV * card_UNIV for pairs. The idea behind card_UNIV is described
in [1].

Then, "List.coset" should be evaluated for instances of the
"card_UNIV" type class?
If you understand "evaluated" as value "List.coset [True]" returns "set
[False]", then no. card_UNIV only evaluates comparisons between sets,
i.e., "List.coset [True] = set [False]" returns true, but without ever
computing explicitly that the left-hand side is in fact "set [False]".

What information is missed in the code generator to evaluate
successfully the previous command? Is it related to the cardinal of
the underlying type, which is needed to compute the representation of
the "1::5", "2::5" or "7::5" elements?
I cannot guess from the information you gave what could be the reason.
If you can send your theory, I can have a look at it. The cardinality
should not matter.

Could not be the types "finite_n" be seen as particular cases of the
ordinal types? Are there good reasons to stick with the "finite_n"
types, being the ordinals far more general?
Yes, they could, but the finite_n types are not meant for
general-purpose applications. Lukas introduced them such that quickcheck
can instantiate type variables in theorems with finite types before
checking.

Andreas

[1] Andreas Lochbihler. Formalising FinFuns - Generating Code for
Functions as Data from Isabelle/HOL. TPHOLs 2009, LNCS 5674, pp.
310--326, Springer, August 2009.
http://www.infsec.ethz.ch/people/andreloc/publications/lochbihler09tphols.pdf

view this post on Zulip Email Gateway (Aug 19 2022 at 09:51):

From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Dear Andreas,

thanks for your comments, they were really useful;

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

Any suggestions are really welcome,

Jesus
Num_Types_Enum_Types.thy

view this post on Zulip Email Gateway (Aug 19 2022 at 09:51):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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)

  1. 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)

  1. 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 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

Last updated: Nov 21 2024 at 12:39 UTC