[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)
function policyJoin :: "policy \<Rightarrow> policy \<Rightarrow>
policy" (infixl "|\<or>" 100)
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)"
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] .
However as a typeclass instantiation I get stuck:
definition "leq = policyOrder"
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