11 val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic |
11 val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic |
12 val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic |
12 val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic |
13 val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> |
13 val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> |
14 tactic |
14 tactic |
15 val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic |
15 val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic |
16 val mk_induct_tac: Proof.context -> int list -> int list list -> |
16 val mk_induct_tac: Proof.context -> int list -> int list list -> int list list list -> thm list -> |
17 ((int * int) * (int * int)) list list list -> thm list -> thm -> thm list -> thm list list -> |
17 thm -> thm list -> thm list list -> tactic |
18 tactic |
|
19 val mk_inject_tac: Proof.context -> thm -> thm -> tactic |
18 val mk_inject_tac: Proof.context -> thm -> thm -> tactic |
20 val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic |
19 val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic |
21 end; |
20 end; |
22 |
21 |
23 structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS = |
22 structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS = |
40 in |
39 in |
41 Drule.cterm_instantiate cfs thm |
40 Drule.cterm_instantiate cfs thm |
42 end; |
41 end; |
43 |
42 |
44 val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs; |
43 val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs; |
45 |
|
46 fun mk_set_rhs def T = |
|
47 let |
|
48 val lhs = snd (Logic.dest_equals (prop_of def)); |
|
49 val Type (_, Ts0) = domain_type (fastype_of lhs); |
|
50 val Type (_, Ts) = domain_type T; |
|
51 in |
|
52 Term.subst_atomic_types (Ts0 ~~ Ts) lhs |
|
53 end; |
|
54 |
|
55 val mk_fsts_rhs = mk_set_rhs @{thm fsts_def[abs_def]}; |
|
56 val mk_snds_rhs = mk_set_rhs @{thm snds_def[abs_def]}; |
|
57 val mk_setl_rhs = mk_set_rhs @{thm sum_setl_def[abs_def]}; |
|
58 val mk_setr_rhs = mk_set_rhs @{thm sum_setr_def[abs_def]}; |
|
59 |
|
60 (* TODO: Put this in "Balanced_Tree" *) |
|
61 fun balanced_tree_middle n = n div 2; |
|
62 |
|
63 val sum_prod_sel_defs = |
|
64 @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]}; |
|
65 |
|
66 fun unfold_sum_prod_sets ctxt ms thm = |
|
67 let |
|
68 fun unf_prod 0 f = f |
|
69 | unf_prod 1 f = f |
|
70 | unf_prod m (t1 $ (t2 $ (t3 $ (t4 $ Const (@{const_name fsts}, T1) $ |
|
71 (t5 $ Const (@{const_name snds}, T2) $ t6)))) $ (t7 $ f $ g)) = |
|
72 t1 $ (t2 $ (t3 $ (t4 $ mk_fsts_rhs T1 $ (t5 $ mk_snds_rhs T2 $ t6)))) |
|
73 $ (t7 $ f $ unf_prod (m - 1) g) |
|
74 | unf_prod _ f = f; |
|
75 fun unf_sum [m] f = unf_prod m f |
|
76 | unf_sum ms (t1 $ (t2 $ (t3 $ (t4 $ Const (@{const_name sum_setl}, T1) $ |
|
77 (t5 $ Const (@{const_name sum_setr}, T2) $ t6)))) $ (t7 $ f $ g)) = |
|
78 let val (ms1, ms2) = chop (balanced_tree_middle (length ms)) ms in |
|
79 t1 $ (t2 $ (t3 $ (t4 $ mk_setl_rhs T1 $ (t5 $ mk_setr_rhs T2 $ t6)))) |
|
80 $ (t7 $ unf_sum ms1 f $ unf_sum ms2 g) |
|
81 end |
|
82 | unf_sum _ f = f; |
|
83 |
|
84 val P = prop_of thm; |
|
85 val P' = Logic.dest_equals P ||> unf_sum ms; |
|
86 val goal = Logic.mk_implies (P, Logic.mk_equals P'); |
|
87 in |
|
88 Skip_Proof.prove ctxt [] [] goal (fn {context = ctxt, ...} => |
|
89 Local_Defs.unfold_tac ctxt sum_prod_sel_defs THEN atac 1) |
|
90 OF [thm] |
|
91 end; |
|
92 |
44 |
93 fun mk_case_tac ctxt n k m case_def ctr_def unf_fld = |
45 fun mk_case_tac ctxt n k m case_def ctr_def unf_fld = |
94 Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN |
46 Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN |
95 (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN' |
47 (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN' |
96 REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN' |
48 REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN' |
135 Local_Defs.unfold_tac ctxt @{thms id_def} THEN |
87 Local_Defs.unfold_tac ctxt @{thms id_def} THEN |
136 TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1); |
88 TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1); |
137 |
89 |
138 val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI}; |
90 val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI}; |
139 |
91 |
140 fun solve_prem_prem_tac ctxt = |
92 val solve_prem_prem_tac = |
141 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
93 REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE' |
142 @{thms Un_iff eq_UN_compreh_Un mem_Collect_eq mem_UN_compreh_eq}) THEN' |
94 hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN' |
143 REPEAT o (etac @{thm rev_bexI} ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN' |
95 (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI}); |
144 (atac ORELSE' rtac refl ORELSE' rtac @{thm singletonI}); |
|
145 |
96 |
146 val induct_prem_prem_thms = |
97 val induct_prem_prem_thms = |
147 @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton |
98 @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton |
148 UN_insert Un_assoc Un_empty_left Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv |
99 UN_insert Un_assoc Un_empty_left Un_empty_right Un_iff Union_Un_distrib collect_def[abs_def] |
149 image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp |
100 eq_UN_compreh_Un fst_conv image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right |
150 sum_map.simps}; |
101 fst_map_pair map_pair_simp mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps |
|
102 sum_set_simps}; |
151 |
103 |
152 fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs = |
104 fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs = |
153 EVERY' (maps (fn ((pp, jj), (qq, kk)) => |
105 EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, |
154 [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, |
|
155 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
106 SELECT_GOAL (Local_Defs.unfold_tac ctxt |
156 (pre_set_defs @ set_natural's @ induct_prem_prem_thms)), |
107 (pre_set_defs @ set_natural's @ induct_prem_prem_thms)), |
157 solve_prem_prem_tac ctxt]) (rev ppjjqqkks)) 1; |
108 solve_prem_prem_tac]) (rev kks)) 1; |
158 |
109 |
159 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks = |
110 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks = |
160 let val r = length ppjjqqkks in |
111 let val r = length kks in |
161 EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac, |
112 EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac, |
162 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN |
113 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN |
163 EVERY [REPEAT_DETERM_N r |
114 EVERY [REPEAT_DETERM_N r |
164 (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2), |
115 (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2), |
165 if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1, |
116 if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1, |
166 mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs] |
117 mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs] |
167 end; |
118 end; |
168 |
119 |
169 fun mk_induct_tac ctxt ns mss ppjjqqkksss ctr_defs fld_induct' set_natural's pre_set_defss = |
120 fun mk_induct_tac ctxt ns mss kkss ctr_defs fld_induct' set_natural's pre_set_defss = |
170 let |
121 let |
171 val nn = length ns; |
122 val nn = length ns; |
172 val n = Integer.sum ns; |
123 val n = Integer.sum ns; |
173 val pre_set_defss' = map2 (map o unfold_sum_prod_sets ctxt) mss pre_set_defss; |
|
174 in |
124 in |
175 Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN |
125 Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN |
176 EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's) |
126 EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's) |
177 pre_set_defss' mss (unflat mss (1 upto n)) ppjjqqkksss) |
127 pre_set_defss mss (unflat mss (1 upto n)) kkss) |
178 end; |
128 end; |
179 |
129 |
180 end; |
130 end; |