Email Gateway (Aug 18 2022 at 14:26): Email Gateway (Aug 18 2022 at 14:26):From: Randy Pollack <rpollack@inf.ed.ac.uk>
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):
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
Email Gateway (Aug 18 2022 at 14:26):From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, Dec 22, 2009 at 5:46 AM, Randy Pollack <rpollack@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.2BUT 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,
Email Gateway (Aug 18 2022 at 14:26):From: Tobias Nipkow <nipkow@in.tum.de>
If you find this behavior to be confusing, it is best to simply avoid
using "==>" with "show". Just use "assumes" instead.
It is only confusing if you have multiple subgoals. With a single
subgoal ==> works fine and avoids some noise in case of inductions ---
otherwise the assume-show style is simpler.
Tobias
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
Last updated: Apr 26 2024 at 01:06 UTC