Re: [isabelle] Problem with schematic variables, subst and flex-flex pairs
Peter Lammich wrote:
Some years ago I wrote some code based on the "conversionals" of HOL, to
do this sort of thing more easily. Thus, for example,
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)
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
%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,
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and