[isabelle] SELECT_GOAL and schematic variables



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.