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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
