*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Problem with schematic variables, subst and flex-flex pairs*From*: Lucas Dixon <ldixon at inf.ed.ac.uk>*Date*: Thu, 18 Sep 2008 16:43:17 +0200*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 2.0.0.16 (X11/20080724)

Hi Peter, 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. Thelist of flex-flex pairs and newly introduced schematics withduplicate parameters gets very long until Isabelle only spits outtons of trace output and does not terminate any more. What happens here?

I think this is caused by Isabelle doing gratuitous lifting of

If you do fix your parameters to free variables, then you get something more reasonable: lemma "(A ?P) ==> f ((x = y) = (a = b)) = ?P x" apply (subst (1 3) eq_commute) ... fixed variables: A, f, x, y, a, b goal (lemma, 1 subgoal): 1. A ?P ==> f ((y = x) = (b = a)) = ?P2 x flex-flex pairs: ?P2 x =?= ?P1 x ?P1 x =?= ?P x But, depending on your context (other subgoals, assumptions etc), that may give incorrect results as it allows meta-variables to capture the bounds (which are being represented as Frees) - if the meta-variable also occurs outside of the scope of the parameters and is instantiated to a term containing the bound variable, you end up with a badly formed instantiation w.r.t. the context.

was necessary, and is probably also the reason for the duplication of

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.

best, lucas -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

**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: [isabelle] Problem with schematic variables, subst and flex-flex pairs
- Next by Date: Re: [isabelle] Problem with schematic variables, subst and flex-flex pairs
- Previous by Thread: [isabelle] Problem with schematic variables, subst and flex-flex pairs
- Next by Thread: Re: [isabelle] Problem with schematic variables, subst and flex-flex pairs
- 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