[isabelle] Problem with schematic variables, subst and flex-flex pairs



Consider the following subgoal

1. "!!x y a b. f ((x = y) = (a = b)) = ?P x y a b"
now, I do:
 apply (subst (1 3) eq_commute)

and get:
goal (1 subgoal):
1. !!x y a b. f ((y = x) = (b = a)) = ?P6 x x x y y y a a a b b b
flex-flex pairs:
 %x y a b. ?P6 x x x y y y a a a b b b =?= %x y a b. ?P4 x x y y a a b b

In my concrete proof, ?P also occurs in other subgoals, it is the result of applying exI to a goal of the form EX P. a1=P & a2=P. The list of flex-flex pairs and newly introduced schematics with duplicate parameters gets very long until Isabelle only spits out tons of trace output and does not terminate any more.

What happens here? Is there a way to get rid of introducing new schematics during subst, and get the desired subgoal:
1. !!x y a b. f ((y = x) = (b = a)) = ?P x y a b

Something that simplifies the subgoal after each substitution step would also be ok.


Regards and thanks in advance for any help,
 Peter





Brian Huffman wrote:
Quoting Peter Lammich <peter.lammich at uni-muenster.de>:

Hi all,

I cannot figure out how to write
 apply (subst theorem)
in the form:
 apply (tactic {* ... *})

Hi Peter,

Here is a silly example:

lemma "(x = y) = (a = b)"
apply (subst (1 3) eq_commute)
-- New subgoal is "(y = x) = (b = a)"

Note that there are three places that the eq_commute rule could apply to this subgoal; the optional (1 3) argument to "subst" says to apply the rule to the first and third, but not the second.

You can get the same result with:
apply (tactic {* EqSubst.eqsubst_tac @{context} [1,3] [ at {thm eq_commute}] 1 *})

(The "1" at the end just says that the tactic should be applied to the first subgoal.)

If you use [0] as the occL argument, this corresponds to the default behavior of subst where the optional argument is omitted. (There is a comment in eqsubst.ML to this effect.) So the following are equivalent:

apply (subst eq_commute)
apply (tactic {* EqSubst.eqsubst_tac @{context} [0] [ at {thm eq_commute}] 1 *})

Hope this helps.

- Brian

The file Provers/eqsubst.thy seems to define this method, but it lacks
documentation in the isabelle reference manual, the chapter on
substitution there describes "stac" instead, which is not quite the
same.

Maybe my question reduces to the stupid question: What to fill in for
the parameters of "fun eqsubst_tac ctxt occL thms i th", when I want to
use it inside an:
 apply (tactic {* ... *}) ?

Regards and thanks in advance for any help,
 Peter










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