Re: [isabelle] Isabelle2015-RC1: Rule instantiation in Eisbach



Hi Andreas,

Unfortunately the ITP paper is slightly out of date, specifically regarding rule instantiation. The "match" method is now meant to guard rule instantiation at run-time by ensuring that the matched theorem(s) has
the correct slots available. This is done by using meta-quantifiers in your patterns. Specifically the semantics of a match are that a "for-fixed" variable may match anything, whereas a meta-quantified variable
must match against a schematic. So in your example, assuming you wish to instantiate "P", your pattern should be "!!P. PROP P ==> f u v" for u v". This statically ensures that any matched rule can be instantiated appropriately (so the failure occurs in the match, rather than the rule instantiation).
The motivation for this requirement is perhaps more clear when using match to define an Eisbach method, rather than when used in-place.

It's also worth noting that a pattern like "f x y" for f x y will produce a large set of possible matches, due to "match" using the unifier internally. The usual best-practice approach is to add type annotations to your pattern to restrict the matches.
There is some argument for extending the match pattern language to support more precise term deconstruction, but I'm waiting to see more use cases before adding more complexity.





> On 20 Apr 2015, at 10:49 pm, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
>
> Dear Eisbach developers,
>
> First of all, thanks for designing and implementing Eisbach. Unfortunately, I am struggling with instantiating variables in rules when I write my own proof methods in Eisbach.
>
> Abstractly,
> 1. I select a rule R by matching a list L of theorems against a term, and
> 2. then instantiate a variable in R with a term obtained by matching the conclusion against a pattern.
>
> Unfortunately, I always get the error "More instantiations than variables in theorem" although all the theorems in the list L contain at least one variable. I do not know where this error comes from. Below is a small example:
>
> theory Scratch imports Main "~~/src/HOL/Eisbach/Eisbach_Tools" begin
>
> consts foo :: "'a â 'a â 'a â bool"
> lemma my_thms: "foo x y z â z â y" "foo x y y â x â z" sorry
>
> lemma "âz. A z â B"
> apply(
>  match concl in "f x y" for f x y â â
>    match my_thms in R:"PROP P â f u v" for P u v â â
>      rule R[of x]
>    â
>  â
> )
> oops
>
> end
>
>
> Thanks for any help,
> Andreas
>
> PS: I am trying to build something similar to the apply_split method in the Eisbach paper presented at ITP2014.
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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