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