40 in |
40 in |
41 Drule.cterm_instantiate cfs thm |
41 Drule.cterm_instantiate cfs thm |
42 end; |
42 end; |
43 |
43 |
44 val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs; |
44 val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs; |
|
45 |
|
46 fun mk_set_rhs set_lhs T = |
|
47 let |
|
48 val Type (_, Ts0) = domain_type (fastype_of set_lhs); |
|
49 val Type (_, Ts) = domain_type T; |
|
50 in |
|
51 Term.subst_atomic_types (Ts0 ~~ Ts) set_lhs |
|
52 end; |
|
53 |
|
54 val mk_fsts_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm fsts_def[abs_def]}))); |
|
55 val mk_snds_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm snds_def[abs_def]}))); |
|
56 val mk_setl_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setl_def[abs_def]}))); |
|
57 val mk_setr_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setr_def[abs_def]}))); |
|
58 |
|
59 (* TODO: Put this in "Balanced_Tree" *) |
|
60 fun balanced_tree_middle n = n div 2; |
|
61 |
|
62 val sum_prod_sel_defs = |
|
63 @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]}; |
|
64 |
|
65 fun unfold_sum_prod_sets ctxt ms thm = |
|
66 let |
|
67 fun unf_prod 0 f = f |
|
68 | unf_prod 1 f = f |
|
69 | unf_prod m (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6)))) |
|
70 $ (t7 $ f $ g)) = |
|
71 t1 $ (t2 $ (t3 $ (t4 $ mk_fsts_rhs T1 $ (t5 $ mk_snds_rhs T2 $ t6)))) |
|
72 $ (t7 $ f $ unf_prod (m - 1) g) |
|
73 | unf_prod _ f = f; |
|
74 fun unf_sum [m] f = unf_prod m f |
|
75 | unf_sum ms (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6)))) |
|
76 $ (t7 $ f $ g)) = |
|
77 let val (ms1, ms2) = chop (balanced_tree_middle (length ms)) ms in |
|
78 t1 $ (t2 $ (t3 $ (t4 $ mk_setl_rhs T1 $ (t5 $ mk_setr_rhs T2 $ t6)))) |
|
79 $ (t7 $ unf_sum ms1 f $ unf_sum ms2 g) |
|
80 end |
|
81 | unf_sum _ f = f; |
|
82 |
|
83 val P = prop_of thm; |
|
84 val P' = Logic.dest_equals P ||> unf_sum ms; |
|
85 val goal = Logic.mk_implies (P, Logic.mk_equals P'); |
|
86 in |
|
87 Skip_Proof.prove ctxt [] [] goal (fn {context = ctxt, ...} => |
|
88 Local_Defs.unfold_tac ctxt sum_prod_sel_defs THEN atac 1) |
|
89 OF [thm] |
|
90 end; |
45 |
91 |
46 fun mk_case_tac ctxt n k m case_def ctr_def unf_fld = |
92 fun mk_case_tac ctxt n k m case_def ctr_def unf_fld = |
47 Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN |
93 Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN |
48 (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN' |
94 (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN' |
49 REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN' |
95 REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN' |
86 subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN |
132 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 |
133 Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN |
88 Local_Defs.unfold_tac ctxt @{thms id_def} THEN |
134 Local_Defs.unfold_tac ctxt @{thms id_def} THEN |
89 TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1); |
135 TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1); |
90 |
136 |
91 (* TODO: Get rid of "auto_tac" (or at least use a naked context) *) |
137 val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI}; |
92 |
138 |
93 fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI} |
139 fun mk_induct_prem_prem_endgame_tac _ 0 = maybe_singletonI_tac |
94 | mk_induct_prem_prem_endgame_tac ctxt qq = |
140 | mk_induct_prem_prem_endgame_tac ctxt qq = |
95 REPEAT_DETERM_N qq o |
141 REPEAT_DETERM_N qq o |
96 (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN' |
142 (SELECT_GOAL (Local_Defs.unfold_tac ctxt |
97 etac @{thm induct_set_step}) THEN' |
143 @{thms trans[OF Union_iff bex_simps(6)] mem_compreh_eq_iff ex_mem_singleton}) THEN' |
98 atac ORELSE' SELECT_GOAL (auto_tac ctxt); |
144 eresolve_tac @{thms induct_set_step}) THEN' maybe_singletonI_tac; |
99 |
145 |
100 fun gen_UN_comprehI_tac UnI = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI} THEN' rtac UnI; |
146 fun gen_UN_comprehI_tac UnI = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI} THEN' rtac UnI; |
101 |
147 |
102 fun gen_UnIN_tac 1 1 = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI'} |
148 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 |
149 | gen_UnIN_tac _ 1 = gen_UN_comprehI_tac @{thm UnI1} THEN' gen_UnIN_tac 1 1 |
107 @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton |
153 @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton |
108 UN_insert Un_assoc Un_empty_left Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv |
154 UN_insert Un_assoc Un_empty_left Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv |
109 image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp |
155 image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp |
110 sum_map.simps}; |
156 sum_map.simps}; |
111 |
157 |
112 (* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly |
|
113 delay them. *) |
|
114 val induct_prem_prem_thms_delayed = |
|
115 @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]}; |
|
116 |
|
117 fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs = |
158 fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs = |
118 EVERY' (maps (fn ((pp, jj), (qq, kk)) => |
159 EVERY' (maps (fn ((pp, jj), (qq, kk)) => |
119 [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, |
160 [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, |
120 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
161 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
121 (pre_set_defs @ set_natural's @ induct_prem_prem_thms)), |
162 (pre_set_defs @ set_natural's @ induct_prem_prem_thms)), |
122 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
163 gen_UnIN_tac pp jj, mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1; |
123 (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)), |
|
124 gen_UnIN_tac pp jj THEN' mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1; |
|
125 |
164 |
126 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks = |
165 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks = |
127 let val r = length ppjjqqkks in |
166 let val r = length ppjjqqkks in |
128 EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac, |
167 EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac, |
129 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN |
168 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN |
135 |
174 |
136 fun mk_induct_tac ctxt ns mss ppjjqqkksss ctr_defs fld_induct' set_natural's pre_set_defss = |
175 fun mk_induct_tac ctxt ns mss ppjjqqkksss ctr_defs fld_induct' set_natural's pre_set_defss = |
137 let |
176 let |
138 val nn = length ns; |
177 val nn = length ns; |
139 val n = Integer.sum ns; |
178 val n = Integer.sum ns; |
|
179 val pre_set_defss' = map2 (map o unfold_sum_prod_sets ctxt) mss pre_set_defss; |
140 in |
180 in |
141 Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN |
181 Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN |
142 EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's) |
182 EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's) |
143 pre_set_defss mss (unflat mss (1 upto n)) ppjjqqkksss) |
183 pre_set_defss' mss (unflat mss (1 upto n)) ppjjqqkksss) |
144 end; |
184 end; |
145 |
185 |
146 end; |
186 end; |