[isabelle-dev] SELECT_GOAL

[Makarius]

On Thu, 27 Jun 2013, Makarius wrote:

> This is a continuation of the following threads from some weeks ago:
>
>  [isabelle] SELECT_GOAL and schematic variables

In Isabelle/a3b175675843 the examples from that thread now work without 
surprises (even after shifting indexes erratically):


inductive P for x where I: "P x"
lemma J: "P (λ_. R)" by (rule I)

schematic_lemma "⋀a. P (?R a) ∨ 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
     *})
   oops

schematic_lemma "⋀a b. P (?R a) ∨ P (?R)" "TERM ?R4"
  apply (rule disjI2, rule J) []
  oops


Note that PRIMITIVE zero_var_indexes is apt to cause some confusion: it 
refers to the whole goal state, including its main conclusion that is 
supposed to be invisible for tactics.  On the other hand, global 
instantiations of goal states do conform to the general notion of tactical 
goal states.  So it might or might not be OK, depending on the overall 
situation.  (Normally you just keep indexes growing until the very end of 
a proof.)


 	Makarius