# [isabelle] Classes with two type variables?

Hi

` I am interested in an abstract general theory of refinement.
``Instances of which are process refinement, ADT refinement and operation
``refinement. I can define this as a local (see below - not very readable
``out of ProofGen) but with more than one type variable.
`
Am I correct to assume that classes can only use one type variable?

`Am I correct to assume that if I can define this as a class, rather
``than a locale, it will make it easier to define theories as an instance
``of the general abstract theory?
``So is there some way to do this or would it be better to stay with locales?
`
kind regards david streader
locale gen_r =

`fixes E :: "'a"
``fixes Xi :: "('b)set" ("\<Xi>")
``fixes Opp :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"(infix
``"\<parallel>" 100)
`fixes Observation :: "'c \<Rightarrow> ('atom) list set" ("Ob")

`fixes Ref :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl
``"\<sqsubseteq>" 100)
``defines refine: "(a \<sqsubseteq> c) \<equiv> (\<forall> x. (x \<in>
``\<Xi>) \<longrightarrow> Ob(a \<parallel> x) \<supseteq> Ob(c
``\<parallel> x))"
``fixes relation_sem :: "'a \<Rightarrow> ('b \<times> (('atom)
``list)) set" ( "\<lbrakk>_\<rbrakk>")
``defines rel_sem: "\<lbrakk>a\<rbrakk> \<equiv> {y.(\<exists>x. (x \<in>
``\<Xi> \<and> (\<exists> z. (z \<in> Ob(a \<parallel> x)) \<and> y = (x
``,z))))}"
`

`lemma (in gen_r) "a \<sqsubseteq> c = (\<lbrakk>a\<rbrakk>
``\<supseteq> \<lbrakk>c\<rbrakk>)"
`apply (simp add: relation_sem_def Ref_def)
apply (auto)
done

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