95 REPEAT_DETERM_N qq o |
95 REPEAT_DETERM_N qq o |
96 (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN' |
96 (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN' |
97 etac @{thm induct_set_step}) THEN' |
97 etac @{thm induct_set_step}) THEN' |
98 atac ORELSE' SELECT_GOAL (auto_tac ctxt); |
98 atac ORELSE' SELECT_GOAL (auto_tac ctxt); |
99 |
99 |
|
100 fun gen_UN_comprehI_tac UnI = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI} THEN' rtac UnI; |
|
101 |
|
102 fun gen_UnIN_tac 1 1 = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI'} |
|
103 | gen_UnIN_tac _ 1 = gen_UN_comprehI_tac @{thm UnI1} THEN' gen_UnIN_tac 1 1 |
|
104 | gen_UnIN_tac n k = gen_UN_comprehI_tac @{thm UnI2} THEN' gen_UnIN_tac (n - 1) (k - 1); |
|
105 |
100 val induct_prem_prem_thms = |
106 val induct_prem_prem_thms = |
101 @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left |
107 @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton |
102 Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv |
108 UN_insert Un_assoc Un_empty_left Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv |
103 snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp sum_map.simps}; |
109 image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp |
|
110 sum_map.simps}; |
104 |
111 |
105 (* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly |
112 (* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly |
106 delay them. *) |
113 delay them. *) |
107 val induct_prem_prem_thms_delayed = |
114 val induct_prem_prem_thms_delayed = |
108 @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]}; |
115 @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]}; |
112 [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, |
119 [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, |
113 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
120 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
114 (pre_set_defs @ set_natural's @ induct_prem_prem_thms)), |
121 (pre_set_defs @ set_natural's @ induct_prem_prem_thms)), |
115 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
122 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
116 (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)), |
123 (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)), |
117 rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE' |
124 gen_UnIN_tac pp jj THEN' mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1; |
118 SELECT_GOAL (auto_tac ctxt)]) (rev ppjjqqkks)) 1; |
|
119 |
125 |
120 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks = |
126 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks = |
121 let val r = length ppjjqqkks in |
127 let val r = length ppjjqqkks in |
122 EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac, |
128 EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac, |
123 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN |
129 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN |