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

Hi Daniel,

Thanks for the reply. Unfortunately, I cannot get this to work at all. Your suggested pattern "!!P. PROP P ==> f u v" raises a type error. After several failed attempts, I am now stuck at the following where something really strange happens.

lemma "âz. A z â B"
 match concl in "f x y" for f x y â â
   match my_thms in R:"âx :: _ :: type. P x â f u v" for P u v â â
     print_fact R,
     print_fact R[of undefined],
     rule R[of undefined]

If I name the bound variable to be matched by a schematic, print_fact R outputs something like foo ?x ?y ?x â ?x â ?y whereas the matched rule is "foo x y z â z â y", i.e., it unifies x with z. If I rename the bound variable !!x to !!z, the rule stays in its general form. Still, the method still fails, because the variable instantiations are done in a strange order (not in the order in which they occur in the theorem).

I do not know the form of the assumption of my matched theorem in my real use case, I just know that there is a variable in the assumptions and that I want to instantiate the first one. How can I express this in Eisbach? I tried to play with "!!x :: _ :: type. PROP P x ==> PROP Q" but this did not match anything I tried.


On 23/04/15 03:48, Daniel Matichuk wrote:
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> 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.

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"
  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]


Thanks for any help,

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.