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