86 subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN |
89 subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN |
87 Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN |
90 Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN |
88 Local_Defs.unfold_tac ctxt @{thms id_def} THEN |
91 Local_Defs.unfold_tac ctxt @{thms id_def} THEN |
89 TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1); |
92 TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1); |
90 |
93 |
91 fun mk_induct_prelude_tac ctxt ctr_defs fld_induct' = |
94 (* TODO: Get rid of "auto_tac" (or at least use a naked context) *) |
92 Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN smash_spurious_fs_tac ctxt; |
|
93 |
95 |
94 fun mk_induct_prepare_prem_tac n m k = |
96 fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI} |
95 EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac, |
97 | mk_induct_prem_prem_endgame_tac ctxt qq = |
96 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1; |
98 REPEAT_DETERM_N qq o |
97 |
99 (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN' |
98 (* FIXME: why not in "Pure"? *) |
100 etac @{thm induct_set_step}) THEN' |
99 fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1); |
101 atac ORELSE' SELECT_GOAL (auto_tac ctxt); |
100 |
|
101 fun mk_induct_prepare_prem_prems_tac r = |
|
102 REPEAT_DETERM_N r (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2) THEN |
|
103 PRIMITIVE Raw_Simplifier.norm_hhf; |
|
104 |
102 |
105 val induct_prem_prem_thms = |
103 val induct_prem_prem_thms = |
106 @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left |
104 @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left |
107 Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv |
105 Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv |
108 snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp sum_map.simps}; |
106 snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp sum_map.simps}; |
110 (* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly |
108 (* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly |
111 delay them. *) |
109 delay them. *) |
112 val induct_prem_prem_thms_delayed = |
110 val induct_prem_prem_thms_delayed = |
113 @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]}; |
111 @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]}; |
114 |
112 |
115 (* TODO: Get rid of "auto_tac" (or at least use a naked context) *) |
113 fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs = |
116 fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI} |
114 EVERY' (maps (fn ((pp, jj), (qq, kk)) => |
117 | mk_induct_prem_prem_endgame_tac ctxt qq = |
115 [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, |
118 REPEAT_DETERM_N qq o |
116 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
119 (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN' |
117 (pre_set_defs @ set_natural's @ induct_prem_prem_thms)), |
120 etac @{thm induct_set_step}) THEN' |
118 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
121 atac ORELSE' SELECT_GOAL (auto_tac ctxt); |
119 (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)), |
|
120 rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE' |
|
121 SELECT_GOAL (auto_tac ctxt)]) (rev ppjjqqkks)) 1; |
122 |
122 |
123 fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs = |
123 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks = |
124 EVERY' (maps (fn ((pp, jj), (qq, kk)) => |
124 EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac, |
125 [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, |
125 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN |
126 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
126 EVERY [REPEAT_DETERM_N (length ppjjqqkks) |
127 (pre_set_defs @ set_natural's @ induct_prem_prem_thms)), |
127 (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2), |
128 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
128 PRIMITIVE Raw_Simplifier.norm_hhf, atac 1, |
129 (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)), |
129 mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs]; |
130 rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE' |
|
131 SELECT_GOAL (auto_tac ctxt)]) |
|
132 (rev ixs)) 1; |
|
133 |
130 |
134 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ixs = |
131 fun mk_induct_tac ctxt ns mss ppjjqqkksss ctr_defs fld_induct' set_natural's pre_set_defss = |
135 EVERY [mk_induct_prepare_prem_tac n m k, |
|
136 mk_induct_prepare_prem_prems_tac (length ixs), atac 1, |
|
137 mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs]; |
|
138 |
|
139 fun mk_induct_tac ctxt ns mss ixsss ctr_defs fld_induct' set_natural's pre_set_defss = |
|
140 let |
132 let |
141 val nn = length ns; |
133 val nn = length ns; |
142 val n = Integer.sum ns; |
134 val n = Integer.sum ns; |
143 in |
135 in |
144 mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN |
136 Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN smash_spurious_fs_tac ctxt THEN |
145 EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's) |
137 EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's) |
146 pre_set_defss mss (unflat mss (1 upto n)) ixsss) |
138 pre_set_defss mss (unflat mss (1 upto n)) ppjjqqkksss) |
147 end; |
139 end; |
148 |
140 |
149 end; |
141 end; |