Email Gateway (Aug 18 2022 at 17:45): Email Gateway (Aug 18 2022 at 17:45):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Hi,
I'm a newbie on Isabelle typeclasses. Doing an information flow
example, I have:
datatype policy = ...
I want make a lattice out of policies, and I have definitions
function policyMeet :: "policy \<Rightarrow> policy \<Rightarrow>
policy" (infixl "|\<and>" 100)
where ...
function policyJoin :: "policy \<Rightarrow> policy \<Rightarrow>
policy" (infixl "|\<or>" 100)
where ...
I define the order and prove it is a partial order:
define policyOrder :: "policy \<Rightarrow> policy \<Rightarrow> bool"
( "_ \<sqsubseteq> _" )
where "(P1 \<sqsubseteq> P2) = ((P1 |\<and> P2) = P1)"
lemma policyOrderRfl[simp]:
fixes P::policy
shows "P \<sqsubseteq> P"
...
Now to make "policy" into a partial order. As a locale interpretation
this works fine:
interpretation policy: partial_order "policyOrder :: policy
\<Rightarrow> policy \<Rightarrow> bool"
proof (unfold_locales, rule policyOrderRfl)
fix x y z :: policy assume j1:"x \<sqsubseteq> y" and j2:"y \<sqsubseteq> z"
show "x \<sqsubseteq> z" using policyOrderTrn[OF j1 j2] .
next ...
However as a typeclass instantiation I get stuck:
instantiation policy::partial_order
begin
definition "leq = policyOrder"
instance
proof (intro_classes)
The first goal is
\<And>x. x \<sqsubseteq> x
So I try
fix x::policy show "x \<sqsubseteq> x"
Already this is not accepted. Perhaps there is an ambiguity between
the \<sqsubseteq> of policyOrder and the \<sqsubseteq> of the
partial_order class (in spite of the explicit annotation (x::policy").
So I try
fix x::policy show "leq x x" using policyOrderRfl .
Here the "show" is accepted, but the last step "." still fails.
What is my problem? Thanks for any info.
Randy
Email Gateway (Aug 18 2022 at 17:45):From: Alexander Krauss <krauss@in.tum.de>
Hi Randy,
[...]
However as a typeclass instantiation I get stuck:
instantiation policy::partial_order
First of all, you seem to be using the partial_order class from
HOL/Lattice session. There is nothing wrong with this, but note that
there is also a similar class "order" in HOL/Orderings.thy and "lattice"
in HOL/Lattices.thy. These are already part of the HOL image, and I
think they are better integrated in terms of reasoning infrastructure,
but I am not sure. These classes use the symbol \<le> rather than
\<sqsubseteq> and also include a strict variant.
begin
definition "leq = policyOrder"
instance
proof (intro_classes)The first goal is
\<And>x. x \<sqsubseteq> x
So I try
fix x::policy show "x \<sqsubseteq> x"
Already this is not accepted. Perhaps there is an ambiguity between
the \<sqsubseteq> of policyOrder and the \<sqsubseteq> of the
partial_order class (in spite of the explicit annotation (x::policy").So I try
fix x::policy show "leq x x" using policyOrderRfl .
Here the "show" is accepted, but the last step "." still fails.
What is my problem? Thanks for any info.
You are confusing the two constants, "leq" and "policyOrder". They are
defined to be equal, but the definition must be used explicitly. Since
you have ambiguous notation, \<sqsubseteq> refers to policyOrder, which
is why the first attempt fails. In the second attempt, your goal is OK,
but the proof is not, because policyOrderRfl uses a different constant.
You should unfold the definition (I think in this context it will be
called something like leq_policy_def) explicitly.
It may also be a good idea to get rid of the syntax for policyOrder. It
makes your grammar ambiguous (which produces tons of warnings), and once
you have the instance, you can use it anyway, since it is defined for
the type class.
Hope this helps,
Alex
Email Gateway (Aug 18 2022 at 17:46):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Thanks Alex. I'm using "order" in HOL/Orderings.thy and "lattice" in
HOL/Lattices.thy as Alex suggested. My typeclass instantiation works.
Now I want to work with the dual of a given lattice. In HOL/Lattices.thy I see
lemma dual_lattice:
"class.lattice (op \<ge>) (op >) sup inf"
by [...]
What does that mean? How can I use this lemma? Please point me to
examples;. This lemma is not even used to prove lemma
dual_bounded_lattice in the same file.
Looking at the HOL/Lattice session I found the following kind of example
datatype 'a dual = dual 'a
primrec undual :: "'a dual \<Rightarrow> 'a" where
undual_dual: "undual (dual x) = x"
instantiation dual:: (lattice) lattice
begin
definition "inf_dual x y = dual (sup (undual x) (undual y))"
[...]
instance
proof
Now I get 12 subgoals (which I can probably prove) but I haven't taken advantage
of lemma dual_lattice.
Please explain how this is intended to be done.
Thanks,
Randy
Email Gateway (Aug 18 2022 at 17:46):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Randy,
Now I want to work with the dual of a given lattice. In HOL/Lattices.thy I see
lemma dual_lattice:
"class.lattice (op \<ge>) (op >) sup inf"
by [...]What does that mean?
This lemma is proven in the context lattice, i.e. it holds for all instances of
the lattice type class. Thus, this means that the assumptions of the type class
lattice (expressed by the predicate class.lattice) hold for the operations >=,
, sup, inf for all instances of the lattice type class. Less formally:
Whenever <=, <, inf, sup form a lattice, so do >=, >, sup, inf.
How can I use this lemma? Please point me to
examples;.
There is just one example in HOL/Lattices for dual_lattice (in the proof of
dual_distrib_lattice). But there are more examples for dual_semilattice, which
is essentially the same concept. Lemmas less_supI1 and less_supI2 show how it is
meant to use this lemma.
Looking at the HOL/Lattice session I found the following kind of example
datatype 'a dual = dual 'a
primrec undual :: "'a dual \<Rightarrow> 'a" where
undual_dual: "undual (dual x) = x"instantiation dual:: (lattice) lattice
begin
definition "inf_dual x y = dual (sup (undual x) (undual y))"
[...]
instance
proofNow I get 12 subgoals (which I can probably prove) but I haven't taken advantage
of lemma dual_lattice.Please explain how this is intended to be done.
The HOL/Lattice development and Lattices.thy are not compatible connected to
each other. This is just another way of dealing with dual lattices (or symmetric
instances of type classes, in general).
Let me briefly compare the two approaches:
On the one hand, Lattices.thy assumes that you mainly work with the normal type
class instantiation. In case you need the dual, the recommended scheme is as in
lemmas less_supI1 and less_supI2, i.e. interpret the local context that is
associated with the type class with the operations instantiated for the dual
lattice. Then, use these theorems to prove your goal. This works nicely in terms
of tool support, but you have to do the local interpretation for every lemma
that needs the dual. Moreover, you do not get a dual instance for type class
instances.
On the other hand, the dual type in HOL/Lattice provides a type wrapper for dual
lattices. In Isabelle, every type may instantiate a type class only once. Hence,
you cannot have instantiations of a lattice and its dual for the same type.
Instead, the type dual instantiates the lattice type classes for the dual
lattice operations. Suppose you are working on a concrete type my_type which
instantiates the lattice type class. Then, if you need the operations from the
lattice, work in type my_type. If you need to work in the dual lattice, transfer
your statement to type "my_type dual". An example how this can be used, is in
HOL/Lattice/Lattices.thy in lemmas join_assoc and join_commute.
Hope this helps,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC