*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] SELECT_GOAL and schematic variables*From*: Peter Lammich <lammich at in.tum.de>*Date*: Fri, 22 Mar 2013 18:19:43 +0100*In-reply-to*: <75F4C99D-8D66-4A5A-B2A3-124ED0867EF7@cam.ac.uk>*References*: <1363883108.11600.102.camel@lapbroy33> <75F4C99D-8D66-4A5A-B2A3-124ED0867EF7@cam.ac.uk>

Unfortunately, this problem does not only affect the (admittedly low-level) SELECT_GOAL, but also high-level proof scripts, as the following example demonstrates: inductive P for x where I: "P x" lemma J: "P (\<lambda>_. R)" by (rule I) schematic_lemma "\<And>a b. P (?R a) \<or> P (?R)" "TERM ?R4" apply (rule disjI2, rule J) [] *** exception TYPE raised (line 109 of "envir.ML"): *** Variable "?R4" has two distinct types *** 'c *** 'd note that everything works fine without the []. -- Peter On Fr, 2013-03-22 at 15:11 +0000, Lawrence Paulson wrote: > I'm afraid that I really can't answer this question without a time machine. > > In the early days, I must have introduced SELECT_GOAL in the context of some specific application where it worked fine. Then it got put in the standard libraries of tacticals and more or less forgotten. I know that a lot of derivations that involve new variables in sub-proofs can go wrong as you describe. The usual method of getting around such problems was to freeze variables prior to applying the tactic, thawing them afterwards. That was a hack, but it generally worked. My impression is that Makarius has replaced such trickery by more robust methods, but it's possible that quite a lot about old code is still there and running. I'm not sure about the current best practice for dealing with this sort of situation. > > Larry Paulson > > > On 21 Mar 2013, at 16:25, Peter Lammich <lammich at in.tum.de> wrote: > > > Hi all, > > > > I recently spotted down a problem with SELECT_GOAL and schematic > > variables. If new schematic variables are produced in the proof of the > > selected goal, their names may clash with existing schematics in the > > outer proof state, resulting in unexpected error messages: > > > > inductive P for x where I: "P x" > > lemma J: "P (\<lambda>_. R)" by (rule I) > > > > schematic_lemma "\<And>a. P (?R a) \<or> P (?R)" "TERM ?R3" > > apply - > > apply (tactic {* SELECT_GOAL ( > > rtac @{thm disjI2} 1 THEN rtac @{thm J} 1 > > (*THEN PRIMITIVE zero_var_indexes*) > > THEN print_tac "Proof state after inner tactic" > > ) 1 > > *}) > > > > *** exception TYPE raised (line 109 of "envir.ML"): > > *** Variable "?R3" has two distinct types > > *** 'c > > *** 'd > > > > What happened here is that the tactic inside SELECT_GOAL produced the > > proof state: "\<And>a b. P ?R3 \<or> P (\<lambda>_. ?R3)" > > And when retrofitting this into the outer proof state, ?R3 happens to > > clash with the ?R3 there. > > > > > > Moreover, if one directly changes schematic variables that occur in the > > selected goal, like the "zero_var_indexes" does in the commented out > > line of the example, the unifier runs havoc and produces errors like: > > > > *** mk_ff_list > > *** At command "apply" (line 9 of > > "/home/lammich/lehre/praktWS1112/cava/Libs/Refine/Autoref/Scratch.thy") > > > > (I also got some exceptions about "Var name confusion" from the unifier, > > that I cannot reproduce any more) > > > > > > These observations result in two main questions: > > 1. What are the conventions that tactics must stick to when > > instantiating schematic variables? E.g. is it ok to do > > PRIMITIVE zero_var_indexes or not? > > > > 2. Is SELECT_GOAL implemented correctly and was never supposed to > > work with schematics, or should it be fixed? > > > > > > Regards and thanks for any comments/workarounds on this, > > Peter > > > > > > >

**References**:**[isabelle] SELECT_GOAL and schematic variables***From:*Peter Lammich

**Re: [isabelle] SELECT_GOAL and schematic variables***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] SELECT_GOAL and schematic variables
- Next by Date: Re: [isabelle] SELECT_GOAL and schematic variables
- Previous by Thread: Re: [isabelle] SELECT_GOAL and schematic variables
- Next by Thread: Re: [isabelle] SELECT_GOAL and schematic variables
- Cl-isabelle-users March 2013 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