*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] typeclasses?*From*: Randy Pollack <rpollack at inf.ed.ac.uk>*Date*: Tue, 22 Dec 2009 13:46:56 +0000

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.

**Follow-Ups**:**Re: [isabelle] typeclasses?***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Sequents evaluation
- Next by Date: Re: [isabelle] typeclasses?
- Previous by Thread: Re: [isabelle] Sequents evaluation
- Next by Thread: Re: [isabelle] typeclasses?
- Cl-isabelle-users December 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list