Filter
Top Products
82 CHAPTER 10. TACTICS
#top_thm();;
it : thm = |- p /\ q ==> p
If a tactic splits a goal into more than one subgoal, they are presented one at a
time. When one subgoal is solved the next unsolved one is presented. For example:
#g ‘p /\ q /\ r ==> q /\ p /\ r‘;;
it : goalstack = 1 subgoal (1 total)
‘p /\ q /\ r ==> q /\ p /\ r‘
#e DISCH_TAC;;
it : goalstack = 1 subgoal (1 total)
‘q /\ p /\ r‘
0 [‘p /\ q /\ r‘]
#e CONJ_TAC;;
it : goalstack = 2 subgoals (2 total)
‘p /\ r‘
0 [‘p /\ q /\ r‘]
‘q‘
0 [‘p /\ q /\ r‘]
#e(ASM_REWRITE_TAC[]);;
it : goalstack = 1 subgoal (1 total)
‘p /\ r‘
0 [‘p /\ q /\ r‘]
#e CONJ_TAC;;
it : goalstack = 2 subgoals (2 total)
‘r‘
0 [‘p /\ q /\ r‘]
‘p‘
0 [‘p /\ q /\ r‘]
#e(ASM_REWRITE_TAC[]);;
it : goalstack = 1 subgoal (1 total)
‘r‘
0 [‘p /\ q /\ r‘]
#e(ASM_REWRITE_TAC[]);;
it : goalstack = No subgoals
Effectively, the user is always at a point in the fringe of the partial proof tree.
The position can be rotated by n goals by doing r n.