95 | _ => split); |
95 | _ => split); |
96 |
96 |
97 fun distinct_in_prems_tac distincts = |
97 fun distinct_in_prems_tac distincts = |
98 eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac; |
98 eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac; |
99 |
99 |
100 (* TODO: reduce code duplication with selector tactic above *) |
|
101 fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr = |
100 fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr = |
102 let |
101 let |
103 val splits' = |
102 val splits' = |
104 map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits) |
103 map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits) |
105 in |
104 in |
114 mk_primcorec_assumption_tac ctxt discIs ORELSE' |
113 mk_primcorec_assumption_tac ctxt discIs ORELSE' |
115 distinct_in_prems_tac distincts ORELSE' |
114 distinct_in_prems_tac distincts ORELSE' |
116 (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))))) |
115 (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))))) |
117 end; |
116 end; |
118 |
117 |
119 (* TODO: implement "exhaustive" (maybe_exh) *) |
118 fun rulify_exhaust n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'}); |
120 fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs maybe_exh = |
119 |
121 EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) ms |
120 fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs |
122 f_ctrs) THEN |
121 maybe_exhaust = |
123 IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN |
122 let |
124 HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI))); |
123 val n = length ms; |
|
124 val (ms', f_ctrs') = |
|
125 (case maybe_exhaust of |
|
126 NONE => (ms, f_ctrs) |
|
127 | SOME exhaust => |
|
128 (ms |> split_last ||> K [n - 1] |> op @, |
|
129 f_ctrs |> split_last ||> (fn thm => [rulify_exhaust n exhaust RS thm]) |> op @)); |
|
130 in |
|
131 EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) |
|
132 ms' f_ctrs') THEN |
|
133 IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN |
|
134 HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI))) |
|
135 end; |
125 |
136 |
126 fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw = |
137 fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw = |
127 HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' |
138 HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' |
128 SELECT_GOAL (unfold_thms_tac ctxt [Let_def]) THEN' REPEAT_DETERM o |
139 SELECT_GOAL (unfold_thms_tac ctxt [Let_def]) THEN' REPEAT_DETERM o |
129 (rtac refl ORELSE' atac ORELSE' |
140 (rtac refl ORELSE' atac ORELSE' |