1\DOC FULL_STRUCT_CASES_TAC
2
3\TYPE {FULL_STRUCT_CASES_TAC : thm_tactic}
4
5\SYNOPSIS
6A form of {STRUCT_CASES_TAC} that also applies the case analysis to the assumption list.
7
8\KEYWORDS
9tactic, cases.
10
11\DESCRIBE
12See {STRUCT_CASES_TAC}.
13
14\FAILURE
15Fails unless provided with a theorem that is a conjunction of
16(possibly multiply existentially quantified) terms which assert the equality
17of a variable with some given terms.
18
19\EXAMPLE
20Suppose we have the goal:
21{
22  ~(l:(*)list = []) ?- (LENGTH l) > 0
23}
24then we can get rid of the universal quantifier from the
25inbuilt list theorem {list_CASES}:
26{
27   list_CASES = !l. (l = []) \/ (?t h. l = CONS h t)
28}
29and then use {FULL_STRUCT_CASES_TAC}. This amounts to applying the
30following tactic:
31{
32   FULL_STRUCT_CASES_TAC (SPEC_ALL list_CASES)
33}
34which results in the following two subgoals:
35{
36   ~(CONS h t = []) ?- (LENGTH(CONS h t)) > 0
37
38   ~([] = []) ?- (LENGTH[]) > 0
39}
40Note that this is a rather simple case, since there are no
41constraints, and therefore the resulting subgoals have no extra assumptions.
42
43\USES
44Generating a case split from the axioms specifying a structure.
45
46\SEEALSO
47Tactic.ASM_CASES_TAC, Tactic.BOOL_CASES_TAC, Tactic.COND_CASES_TAC, Tactic.DISJ_CASES_TAC, Tactic.STRUCT_CASES_TAC.
48\ENDDOC
49