*To*: Randy Pollack <rpollack at inf.ed.ac.uk>*Subject*: Re: [isabelle] typeclasses?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 22 Dec 2009 07:53:29 -0800*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <19248.52688.111907.528046@locatelli.inf.ed.ac.uk>*References*: <19248.52688.111907.528046@locatelli.inf.ed.ac.uk>*Sender*: huffman.brian.c at gmail.com

On Tue, Dec 22, 2009 at 5:46 AM, Randy Pollack <rpollack at inf.ed.ac.uk> wrote: > > 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}" ... > 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} This is just how the Isar proof language works when you use a meta-implication (==>) in a "show" command. When you use "show <prop>", it is as if you had proved "lemma foo: <prop>" separately, and then done "apply (rule foo)" to the current proof state (Isabelle will apply the rule to the first subgoal that matches). For example, if you have a proof state with subgoals "A1 ==> A" and "B1 ==> B", and then do 'show "C ==> B"', Isabelle will apply the rule "C ==> B" to the second subgoal, and the new proof state will have subgoals "A1 ==> A" and "B1 ==> C". At the end of your proof script, any remaining subgoals of the form "A ==> A" will be solved by assumption by "qed". This is the case with your proof; if you can discharge the second subgoal, the first goal (which is solvable by assumption) will be handled by qed. If you find this behavior to be confusing, it is best to simply avoid using "==>" with "show". Just use "assumes" instead. > > 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". It looks like you need a type annotation here. Since "FV" and "tvar" are both overloaded constants, Isabelle can't tell what the return type of "tvar" should be. (Turn on "show consts" to see the inferred type; it probably introduces a new free type variable.) Try this instead: fix x::var show "FV (tvar x :: trm) = {x}" (Note to Isabelle developers: Introducing a new type variable in the middle of a proof like this is not something users usually do on purpose. Would it be possible to print a warning message when this happens?) Hope this helps, - Brian

**Follow-Ups**:**Re: [isabelle] typeclasses?***From:*Tobias Nipkow

**References**:**[isabelle] typeclasses?***From:*Randy Pollack

- Previous by Date: [isabelle] typeclasses?
- Next by Date: Re: [isabelle] typeclasses?
- Previous by Thread: [isabelle] typeclasses?
- 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