Re: [isabelle] SELECT_GOAL and schematic variables



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.