40 fun mk_primcorec_assumption_tac ctxt discIs = |
40 fun mk_primcorec_assumption_tac ctxt discIs = |
41 HEADGOAL (SELECT_GOAL (unfold_thms_tac ctxt |
41 HEADGOAL (SELECT_GOAL (unfold_thms_tac ctxt |
42 @{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN |
42 @{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN |
43 SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE' |
43 SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE' |
44 resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE' |
44 resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE' |
45 dresolve_tac discIs THEN' atac))))); |
45 dresolve_tac discIs THEN' atac ORELSE' |
|
46 etac notE THEN' atac ORELSE' |
|
47 etac disjE))))); |
46 |
48 |
47 fun mk_primcorec_same_case_tac m = |
49 fun mk_primcorec_same_case_tac m = |
48 HEADGOAL (if m = 0 then rtac TrueI |
50 HEADGOAL (if m = 0 then rtac TrueI |
49 else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac); |
51 else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac); |
50 |
52 |
86 (* TODO: reduce code duplication with selector tactic above *) |
88 (* TODO: reduce code duplication with selector tactic above *) |
87 fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr = |
89 fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr = |
88 HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN |
90 HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN |
89 mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN |
91 mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN |
90 REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN |
92 REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN |
91 HEADGOAL (SELECT_GOAL (HEADGOAL (REPEAT_DETERM o |
93 HEADGOAL (SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o |
92 (rtac refl ORELSE' atac ORELSE' |
94 (rtac refl ORELSE' atac ORELSE' |
93 resolve_tac split_connectI ORELSE' |
95 resolve_tac split_connectI ORELSE' |
94 Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' |
96 Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' |
95 Splitter.split_tac (split_if :: splits) ORELSE' |
97 Splitter.split_tac (split_if :: splits) ORELSE' |
|
98 K (mk_primcorec_assumption_tac ctxt discIs) ORELSE' |
96 eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' |
99 eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' |
97 (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))); |
100 (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))))); |
98 |
101 |
99 fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs splits split_asms ms ctr_thms = |
102 fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs splits split_asms ms ctr_thms = |
100 EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) |
103 EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) |
101 ms ctr_thms); |
104 ms ctr_thms); |
102 |
105 |