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

```Peter Lammich wrote:
```
```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

```
Some years ago I wrote some code based on the "conversionals" of HOL, to do this sort of thing more easily. Thus, for example,
```
Goal "!!x y a b. f ((x = y) = (a = b)) = P x y a b" ;
by ((Conv.CONV_TAC o Conv.TDSTOP_CONV) (eqc eq_commute)) ;
```
(applies conversions top-down, but stopping (ie, not descending into a resulting term upon success)
```1. !!x y a b. P x y a b = f ((x = y) = (a = b))
by ((Conv.CONV_TAC o Conv.TOPDN_CONV) (eqc eq_commute)) ;
(applies conversions top down)
1. !!x y a b. f ((b = a) = (y = x)) = P x y a b
by ((Conv.CONV_TAC o Conv.BUSTOP_CONV) (eqc eq_commute)) ;
(applies conversions bottom up, stopping upon any success)
1. !!x y a b. f ((a = b) = (x = y)) = P x y a b

```
With these, I usually don't need the following, which makes a conversion succeed only the first and third times it would otherwise have succeeded). by ((Conv.CONV_TAC o Conv.TOPDN_CONV o Conv.NTH_CONV [1,3]) (eqc eq_commute)) ;
```1. !!x y a b. P x y a b = f ((b = a) = (x = y))

```
Incidentally, I found my code doesn't work with schematic variables (I don't know why), so to use it you'd have to wrap your goal in freeze_thaw. Which would presumably solve your problem anyway.
```
But if you're interested in my code, it's at
http://users.rsise.anu.edu.au/~jeremy/isabelle/2005/gen/{conv.ML,eq_conv.ML}

Regards,

Jeremy

```

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