[isabelle] Eisbach matching with schematic variables



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.