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.