[isabelle] lattices, typeclasses, notations?


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
definition "leq = policyOrder"
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.


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