131 val solve_prem_prem_tac = |
131 val solve_prem_prem_tac = |
132 REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE' |
132 REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE' |
133 hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN' |
133 hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN' |
134 (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI}); |
134 (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI}); |
135 |
135 |
136 fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs = |
136 fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs = |
137 EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, |
137 EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, |
138 SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_natural's @ sum_prod_thms_set0)), |
138 SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_map's @ sum_prod_thms_set0)), |
139 solve_prem_prem_tac]) (rev kks)) 1; |
139 solve_prem_prem_tac]) (rev kks)) 1; |
140 |
140 |
141 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks = |
141 fun mk_induct_discharge_prem_tac ctxt nn n set_map's pre_set_defs m k kks = |
142 let val r = length kks in |
142 let val r = length kks in |
143 EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac, |
143 EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac, |
144 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN |
144 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN |
145 EVERY [REPEAT_DETERM_N r |
145 EVERY [REPEAT_DETERM_N r |
146 (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2), |
146 (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2), |
147 if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1, |
147 if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1, |
148 mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs] |
148 mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs] |
149 end; |
149 end; |
150 |
150 |
151 fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_natural's pre_set_defss = |
151 fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_map's pre_set_defss = |
152 let val n = Integer.sum ns in |
152 let val n = Integer.sum ns in |
153 unfold_thms_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_as_projs_tac ctxt 1 THEN |
153 unfold_thms_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_as_projs_tac ctxt 1 THEN |
154 EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's) |
154 EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_map's) pre_set_defss |
155 pre_set_defss mss (unflat mss (1 upto n)) kkss) |
155 mss (unflat mss (1 upto n)) kkss) |
156 end; |
156 end; |
157 |
157 |
158 fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels = |
158 fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels = |
159 hyp_subst_tac THEN' |
159 hyp_subst_tac THEN' |
160 CONVERSION (hhf_concl_conv |
160 CONVERSION (hhf_concl_conv |