[isabelle-dev] SELECT_GOAL

Makarius makarius at sketis.net
Thu Jun 27 13:09:17 CEST 2013

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

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

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


More information about the isabelle-dev mailing list