*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Problem with schematic variables, subst and flex-flex pairs*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Fri, 19 Sep 2008 11:06:52 +1000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <48D2516D.4020405@uni-muenster.de>*References*: <48D119CE.4070504@uni-muenster.de> <20080917141644.6hu70p1740ck8cc4@webmail.pdx.edu> <48D2516D.4020405@uni-muenster.de>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

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 bIn my concrete proof, ?P also occurs in other subgoals, it is theresult 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 withduplicate parameters gets very long until Isabelle only spits out tonsof trace output and does not terminate any more.What happens here? Is there a way to get rid of introducing newschematics during subst, and get the desired subgoal:1. !!x y a b. f ((y = x) = (b = a)) = ?P x y a bSomething that simplifies the subgoal after each substitution stepwould also be ok.Regards and thanks in advance for any help, Peter

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)) ;

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

1. !!x y a b. P x y a b = f ((b = a) = (x = y))

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

**References**:**[isabelle] subst translated to ML-level ?***From:*Peter Lammich

**Re: [isabelle] subst translated to ML-level ?***From:*Brian Huffman

**[isabelle] Problem with schematic variables, subst and flex-flex pairs***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Problem with schematic variables, subst and flex-flex pairs
- Next by Date: [isabelle] Question about locales
- Previous by Thread: Re: [isabelle] Problem with schematic variables, subst and flex-flex pairs
- Next by Thread: [isabelle] Question about locales
- Cl-isabelle-users September 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list