66 in list_all_free (quantfrees, list_implies (iprems,concl)) end |
66 in list_all_free (quantfrees, list_implies (iprems,concl)) end |
67 handle Bind => error"Recursion term not found in conclusion"; |
67 handle Bind => error"Recursion term not found in conclusion"; |
68 |
68 |
69 (*Avoids backtracking by delivering the correct premise to each goal*) |
69 (*Avoids backtracking by delivering the correct premise to each goal*) |
70 fun ind_tac [] 0 = all_tac |
70 fun ind_tac [] 0 = all_tac |
71 | ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI, prem, refl] i) THEN |
71 | ind_tac(prem::prems) i = |
72 ind_tac prems (i-1); |
72 DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN |
|
73 ind_tac prems (i-1); |
73 |
74 |
74 val pred = Free(pred_name, elem_type --> boolT); |
75 val pred = Free(pred_name, elem_type --> boolT); |
75 |
76 |
76 val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms; |
77 val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms; |
77 |
78 |
138 val cmonos = [subset_refl RS Int_Collect_mono] RL monos RLN (2,[rev_subsetD]); |
139 val cmonos = [subset_refl RS Int_Collect_mono] RL monos RLN (2,[rev_subsetD]); |
139 |
140 |
140 (*Avoids backtracking by delivering the correct premise to each goal*) |
141 (*Avoids backtracking by delivering the correct premise to each goal*) |
141 fun mutual_ind_tac [] 0 = all_tac |
142 fun mutual_ind_tac [] 0 = all_tac |
142 | mutual_ind_tac(prem::prems) i = |
143 | mutual_ind_tac(prem::prems) i = |
143 SELECT_GOAL |
144 DETERM |
144 ((*unpackage and use "prem" in the corresponding place*) |
145 (SELECT_GOAL |
145 REPEAT (FIRSTGOAL |
146 ((*unpackage and use "prem" in the corresponding place*) |
146 (eresolve_tac ([conjE,mp]@cmonos) ORELSE' |
147 REPEAT (FIRSTGOAL |
147 ares_tac [prem,impI,conjI])) |
148 (etac conjE ORELSE' eq_mp_tac ORELSE' |
148 (*prove remaining goals by contradiction*) |
149 ares_tac [impI, conjI])) |
149 THEN rewrite_goals_tac (con_defs@part_rec_defs) |
150 (*prem is not allowed in the REPEAT, lest it loop!*) |
150 THEN REPEAT (eresolve_tac (PartE :: sumprod_free_SEs) 1)) |
151 THEN TRYALL (rtac prem) |
151 i THEN mutual_ind_tac prems (i-1); |
152 THEN REPEAT |
|
153 (FIRSTGOAL (ares_tac [impI] ORELSE' |
|
154 eresolve_tac (mp::cmonos))) |
|
155 (*prove remaining goals by contradiction*) |
|
156 THEN rewrite_goals_tac (con_defs@part_rec_defs) |
|
157 THEN DEPTH_SOLVE (eresolve_tac (PartE :: sumprod_free_SEs) 1)) |
|
158 i) |
|
159 THEN mutual_ind_tac prems (i-1); |
152 |
160 |
153 val mutual_induct_split = |
161 val mutual_induct_split = |
154 prove_goalw_cterm [] |
162 prove_goalw_cterm [] |
155 (cterm_of sign |
163 (cterm_of sign |
156 (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms, |
164 (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms, |