Re: [isabelle] typeclasses?



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





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