57 val (Some pred) = gen_assoc (op aconv) (ind_alist, X) |
57 val (Some pred) = gen_assoc (op aconv) (ind_alist, X) |
58 val concl = mk_tprop (pred $ t) |
58 val concl = mk_tprop (pred $ t) |
59 in list_all_free (quantfrees, list_implies (iprems,concl)) end |
59 in list_all_free (quantfrees, list_implies (iprems,concl)) end |
60 handle Bind => error"Recursion term not found in conclusion"; |
60 handle Bind => error"Recursion term not found in conclusion"; |
61 |
61 |
62 (*Avoids backtracking by delivering the correct premise to each goal*) |
62 (*Reduces backtracking by delivering the correct premise to each goal. |
|
63 Intro rules with extra Vars in premises still cause some backtracking *) |
63 fun ind_tac [] 0 = all_tac |
64 fun ind_tac [] 0 = all_tac |
64 | ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI, prem, refl] i) THEN |
65 | ind_tac(prem::prems) i = |
65 ind_tac prems (i-1); |
66 DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN |
|
67 ind_tac prems (i-1); |
66 |
68 |
67 val pred = Free(pred_name, iT-->oT); |
69 val pred = Free(pred_name, iT-->oT); |
68 |
70 |
69 val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms; |
71 val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms; |
70 |
72 |
134 val cmonos = [subset_refl RS Collect_mono] RL monos RLN (2,[rev_subsetD]); |
136 val cmonos = [subset_refl RS Collect_mono] RL monos RLN (2,[rev_subsetD]); |
135 |
137 |
136 (*Avoids backtracking by delivering the correct premise to each goal*) |
138 (*Avoids backtracking by delivering the correct premise to each goal*) |
137 fun mutual_ind_tac [] 0 = all_tac |
139 fun mutual_ind_tac [] 0 = all_tac |
138 | mutual_ind_tac(prem::prems) i = |
140 | mutual_ind_tac(prem::prems) i = |
139 SELECT_GOAL |
141 DETERM |
140 ((*unpackage and use "prem" in the corresponding place*) |
142 (SELECT_GOAL |
141 REPEAT (FIRSTGOAL |
143 ((*unpackage and use "prem" in the corresponding place*) |
142 (eresolve_tac ([conjE,mp]@cmonos) ORELSE' |
144 REPEAT (FIRSTGOAL |
143 ares_tac [prem,impI,conjI])) |
145 (etac conjE ORELSE' eq_mp_tac ORELSE' |
144 (*prove remaining goals by contradiction*) |
146 ares_tac [impI, conjI])) |
145 THEN rewrite_goals_tac (con_defs@part_rec_defs) |
147 (*prem is not allowed in the REPEAT, lest it loop!*) |
146 THEN REPEAT (eresolve_tac (PartE :: sumprod_free_SEs) 1)) |
148 THEN TRYALL (rtac prem) |
147 i THEN mutual_ind_tac prems (i-1); |
149 THEN REPEAT |
|
150 (FIRSTGOAL (ares_tac [impI] ORELSE' |
|
151 eresolve_tac (mp::cmonos))) |
|
152 (*prove remaining goals by contradiction*) |
|
153 THEN rewrite_goals_tac (con_defs@part_rec_defs) |
|
154 THEN DEPTH_SOLVE (eresolve_tac (PartE :: sumprod_free_SEs) 1)) |
|
155 i) |
|
156 THEN mutual_ind_tac prems (i-1); |
148 |
157 |
149 val mutual_induct_fsplit = |
158 val mutual_induct_fsplit = |
150 prove_goalw_cterm [] |
159 prove_goalw_cterm [] |
151 (cterm_of sign |
160 (cterm_of sign |
152 (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms, |
161 (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms, |