[isabelle] typeclasses?



I've been using locales, but this is my first foray into Isabelle
typeclasses.

This example is in completely standard Isabelle2009-1: December 2009

Here is a cut-down example of a typeclass for types of object-level
terms (here using "nat" for the type of object-level variables) and
substitution.  These are first order terms with no binding.

 types
   var = nat
   'a sbstTyp = "var => 'a"              (* type of substitutions on 'a *)
   'a SbstTyp = "'a => 'a sbstTyp => 'a" (* type of subst operation *)

 (** a typeclass for terms with substitution **)
 class trmCl =
   fixes tvar :: "'a sbstTyp"     (* inject variables into terms *)
   and FV :: "'a => var set"      (* set of free vars in a term *)
   and Sbst :: "'a SbstTyp"       (* operation of substitution *)
   assumes S3 : "\<forall>x \<in> FV t. thet1 x = thet2 x ==>
				Sbst t thet1 = Sbst t thet2"
   and S5 : "FV (tvar x) = {x}"

Now, an actual datatype of first-order terms with its free variable
and substitution operations

 (** a first-order type of terms  **)
 datatype trm =
     lPar var
   | lApp trm trm   ("_ # _"  [100,100] 100)

 (* actual free variable function of trm *)
 primrec GV :: "trm => var set"
 where
   "GV (lPar X) = {X}"
 | "GV (lApp t1 t2) = (GV t1) Un (GV t2)"

 (* actual substitution operation *)
 primrec trm_Sbst :: "trm SbstTyp"    ("_[[_]]")
 where
   "(lPar X)[[thta]] = thta X"
 | "(M1 # M2)[[thta]] = (M1[[thta]]) # (M2[[thta]])"

The punchline is that my attempt to instantiate trmCl with trm fails
with two problems I don't understand.

 instantiation trm :: trmCl
 begin

 definition tvar_def: "tvar = lPar"
 definition FV_def: "FV = GV"
 definition Sbst_def: "Sbst = trm_Sbst"

 instance proof
   fix t::trm and thet1 thet2 :: "trm sbstTyp"
   show "\<forall>x\<in>FV t. thet1 x = thet2 x ==> Sbst t thet1 = Sbst t thet2"
     by (induct t rule:trm.induct, auto simp add: FV_def Sbst_def)

I receive the message 

Successful attempt to solve goal by exported rule:
  ∀x∈FV ?t2. ?thet1.2 x = ?thet2.2 x ==>
  Sbst ?t2 ?thet1.2 = Sbst ?t2 ?thet2.2

BUT a residual goal is still there

 next

goal (2 subgoals):
 1. /\ t thet1 thet2. ∀x∈FV t. thet1 x = thet2 x ==> ∀x∈FV t. thet1 x = thet2 x
 2. /\x. FV (tvar x) = {x}

OK, skip goal 1. and try to solve goal 2.

  fix x::var show "FV (tvar x) = {x}"

*** Local statement will fail to refine any pending goal
*** Failed attempt to solve goal by exported rule:
***   FV (tvar ?x3) = {?x3}
*** At command "show".

I'm stumped.

Thanks for any help,
Randy

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






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