Re: [isabelle] Eisbach matching with schematic variables



Hi Dan,

Thanks for the suggestion with fail in the interesting case. That indeed gets me out of the subgoal focus of match. Indeed, a light-weight match without subgoal focus and without binding in the first place would be nice.

Andreas

On 26/10/16 02:23, Daniel.Matichuk at data61.csiro.au wrote:
Hi Andreas,

The incompatibility with match and schematic variables is a known limitation, and unfortunately it's actually a hard problem to solve in general. Currently the "match" method performs a subgoal focus when matching on the conclusion or premises in order to turn them into proper terms/facts. This allows you to, for example, refer to "p1" (in your example) inside your method body and have it still make sense if p1 contained a goal parameter. This focus, however, needs to turns schematics into fixed terms for a number of reasons, most of which is so that they can't suddenly depend on goal parameters that they didn't before (i.e. in the case of "!!x y. (?P x) /\ (?Q y)").

Makarius and I had some discussions about how to handle this particular situation, we were leaning towards making methods "smarter" and realising that certain fixed parameters were actually schematics in the context and knowing how to instantiate them.

The other more lightweight solution we thought of was to introduce a non-focusing match, i.e. a match that does not manipulate the goal state or try to bind goal elements. This seems more like what you would want in your current situation. It's not immediately clear how this would interact with nested matches, however.

That all being said, I believe your particular situation can be resolved simply by putting "rule my_rules" outside of the match body itself. This is not the most elegant solution, but it should get the job done.

method step =
 ((match conclusion in
   "foo p1 p2 p3" for p1 p2 p3 â âfailâ
   Â H for H â âsolves âclarsimpââ) | (rule my_rules))

The match will not backtrack past the fact that it matched "foo p1 p2 p3" and will immediately fail through to "rule my_rules".

Hopefully this resolves your issue.

-Dan

P.S.

The "_" pattern is valid in the match method, so we can make your method a bit more succinct.

method step =
 ((match conclusion in
   "foo _ _ _" â âfailâ
   Â _ â âsolves âclarsimpââ) | (rule my_rules))[1]




On 22 Oct. 2016, at 1:29 am, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:

Dear Eisbach experts and users,

I have trouble to write a proof method that does the following:

1. Apply a rule called foo.
It has two premises that both contain variables that are not bound by the conclusion of foo. Hence, the goal state consists of two goals with a schematic variable ?x in them.

2. Work on the first subgoal by applying rules from a named_theorems collection my_rules. This is supposed to instantiate the variable ?x. All these rules in my_rules have one constant C as the head term, and they have premises with the same head constant, but there may also be premises with other terms (let's call them side conditions). As long as the current subgoal has C as head symbol, I want to apply the rules in my_rules, and I want to apply some proof automation (like clarsimp or auto) to the side conditions. In particular, I want to make sure that clarsimp and auto are _never_ applied to a goal with C as head symbol.

This should be done iteratively until either
(a) the goal arising from step 1 is solved or
(b) the current subgoal has C as head symbol, but there's no matching rule in my_rules, or
(c) one of the side conditions is not solved by clarsimp and auto.

I tried to write the proof method with Eisbach, but I failed to make the distinction based on the head symbol. Here's my attempt:

method step =
 (match conclusion in "foo p1 p2 p3" for p1 p2 p3 => rule my_rules
 \<bar> H for H => \<open>solves \<open>clarsimp\<close>\<close>)
method my_method = (rule foo, (step+)?)

The problem is that the match method seems to turn the schematic variable ?x into a fixed variable x, which the rules in my_rules can no longer instantiate.

Can I somehow achieve with Eisbach what I want?

Best,
Andreas








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