USE_SG_THEN
Tactical.USE_SG_THEN : thm_tactic -> int -> int -> list_tactic
Allows the user to use one subgoal to prove another
In USE_SG_THEN ttac nu np, of the current goal list, subgoal number
nu can be used in proving subgoal number np. Subgoal number nu is
used as a lemma by ttac to simplify subgoal number np. That is, if
subgoal number nu is A ?- u, subgoal number np is A1 ?- t1, and
A1 ?- t1
========== ttac (u |- u)
A2 ?- t2
then the list-tactic USE_SG_THEN ttac nu np gives this same result
(new subgoal(s)) for subgoal np.
This list-tactic will be invalid unless A is a subset of A1.
Note that in the interactive system, subgoals are printed in reverse order of their numbering.
Failure
USE_SG_THEN will fail ttac (u |- u) fails on subgoal number np, or
if indices np or nu are out of range. Note that the subgoals in the
current subgoal list are numbered starting from 1.
Where two subgoals are similar and not easy to prove, one can be used to help prove the other.
Example
Here subgoal 1 is assumed, so as to help in proving subgoal 2.
r \/ s
------------------------------------
0. p
1. q
r
------------------------------------
0. p
1. q
2 subgoals
:
proof
> elt (USE_SG_THEN ASSUME_TAC 1 2) ;
OK..
2 subgoals:
val it =
0. q
1. p
2. p'
------------------------------------
q
0. q
1. p
------------------------------------
p'
Here is an example where the assumptions differ. Subgoal 2 is used to
solve subgoal 1, but the assumption p' of subgoal 2 remains to be
proved. Without VALIDATE_LT, the list-tactic would be invalid.
r
------------------------------------
0. p'
1. q
r
------------------------------------
0. p
1. q
2 subgoals
:
proof
> elt (VALIDATE_LT (USE_SG_THEN ACCEPT_TAC 2 1)) ;
Exception- OK..
HOL_ERR at Tactic.ACCEPT_TAC: raised
Comments
Some users may expect the generated tactic to be ttac (A |- u), rather
than ttac (u |- u).