1 (* Title: HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2013 |
|
4 |
|
5 Tactics for corecursor sugar. |
|
6 *) |
|
7 |
|
8 signature BNF_GFP_REC_SUGAR_TACTICS = |
|
9 sig |
|
10 val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic |
|
11 val mk_primcorec_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic |
|
12 val mk_primcorec_ctr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic |
|
13 val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> |
|
14 tactic |
|
15 val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm list -> thm list list -> |
|
16 thm list -> tactic |
|
17 val mk_primcorec_exhaust_tac: Proof.context -> string list -> int -> thm -> tactic |
|
18 val mk_primcorec_nchotomy_tac: Proof.context -> thm list -> tactic |
|
19 val mk_primcorec_raw_code_tac: Proof.context -> thm list -> thm list -> thm list -> thm list -> |
|
20 int list -> thm list -> thm option -> tactic |
|
21 val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list -> |
|
22 thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic |
|
23 end; |
|
24 |
|
25 structure BNF_GFP_Rec_Sugar_Tactics : BNF_GFP_REC_SUGAR_TACTICS = |
|
26 struct |
|
27 |
|
28 open BNF_Util |
|
29 open BNF_Tactics |
|
30 open BNF_FP_Util |
|
31 |
|
32 val atomize_conjL = @{thm atomize_conjL}; |
|
33 val falseEs = @{thms not_TrueE FalseE}; |
|
34 val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict}; |
|
35 val split_if = @{thm split_if}; |
|
36 val split_if_asm = @{thm split_if_asm}; |
|
37 val split_connectI = @{thms allI impI conjI}; |
|
38 val unfold_lets = @{thms Let_def[abs_def] split_beta} |
|
39 |
|
40 fun exhaust_inst_as_projs ctxt frees thm = |
|
41 let |
|
42 val num_frees = length frees; |
|
43 val fs = Term.add_vars (prop_of thm) [] |> filter (can dest_funT o snd); |
|
44 fun find s = find_index (curry (op =) s) frees; |
|
45 fun mk_cfp (f as ((s, _), T)) = |
|
46 (certify ctxt (Var f), certify ctxt (mk_proj T num_frees (find s))); |
|
47 val cfps = map mk_cfp fs; |
|
48 in |
|
49 Drule.cterm_instantiate cfps thm |
|
50 end; |
|
51 |
|
52 val exhaust_inst_as_projs_tac = PRIMITIVE oo exhaust_inst_as_projs; |
|
53 |
|
54 fun distinct_in_prems_tac distincts = |
|
55 eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac; |
|
56 |
|
57 fun mk_primcorec_nchotomy_tac ctxt disc_exhausts = |
|
58 HEADGOAL (Method.insert_tac disc_exhausts THEN' clean_blast_tac ctxt); |
|
59 |
|
60 fun mk_primcorec_exhaust_tac ctxt frees n nchotomy = |
|
61 let val ks = 1 upto n in |
|
62 HEADGOAL (atac ORELSE' |
|
63 cut_tac nchotomy THEN' |
|
64 K (exhaust_inst_as_projs_tac ctxt frees) THEN' |
|
65 EVERY' (map (fn k => |
|
66 (if k < n then etac disjE else K all_tac) THEN' |
|
67 REPEAT o (dtac meta_mp THEN' atac ORELSE' |
|
68 etac conjE THEN' dtac meta_mp THEN' atac ORELSE' |
|
69 atac)) |
|
70 ks)) |
|
71 end; |
|
72 |
|
73 fun mk_primcorec_assumption_tac ctxt discIs = |
|
74 SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True |
|
75 not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN |
|
76 SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE' |
|
77 eresolve_tac falseEs ORELSE' |
|
78 resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE' |
|
79 dresolve_tac discIs THEN' atac ORELSE' |
|
80 etac notE THEN' atac ORELSE' |
|
81 etac disjE)))); |
|
82 |
|
83 val ss_fst_snd_conv = simpset_of (ss_only @{thms fst_conv snd_conv} @{context}); |
|
84 |
|
85 fun case_atac ctxt = simp_tac (put_simpset ss_fst_snd_conv ctxt); |
|
86 |
|
87 fun same_case_tac ctxt m = |
|
88 HEADGOAL (if m = 0 then rtac TrueI |
|
89 else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' case_atac ctxt) THEN' case_atac ctxt); |
|
90 |
|
91 fun different_case_tac ctxt m exclude = |
|
92 HEADGOAL (if m = 0 then |
|
93 mk_primcorec_assumption_tac ctxt [] |
|
94 else |
|
95 dtac exclude THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN' |
|
96 mk_primcorec_assumption_tac ctxt []); |
|
97 |
|
98 fun cases_tac ctxt k m excludesss = |
|
99 let val n = length excludesss in |
|
100 EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m |
|
101 | [exclude] => different_case_tac ctxt m exclude) |
|
102 (take k (nth excludesss (k - 1)))) |
|
103 end; |
|
104 |
|
105 fun prelude_tac ctxt defs thm = |
|
106 unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt unfold_lets; |
|
107 |
|
108 fun mk_primcorec_disc_tac ctxt defs disc_corec k m excludesss = |
|
109 prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m excludesss; |
|
110 |
|
111 fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss |
|
112 disc_excludes = |
|
113 HEADGOAL (rtac iffI THEN' |
|
114 rtac fun_exhaust THEN' |
|
115 K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN' |
|
116 EVERY' (map (fn [] => etac FalseE |
|
117 | fun_discs' as [fun_disc'] => |
|
118 if eq_list Thm.eq_thm (fun_discs', fun_discs) then |
|
119 REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI) |
|
120 else |
|
121 rtac FalseE THEN' |
|
122 (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac ORELSE' |
|
123 cut_tac fun_disc') THEN' |
|
124 dresolve_tac disc_excludes THEN' etac notE THEN' atac) |
|
125 fun_discss) THEN' |
|
126 (etac FalseE ORELSE' |
|
127 resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac)); |
|
128 |
|
129 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_idents map_comps fun_sel k |
|
130 m excludesss = |
|
131 prelude_tac ctxt defs (fun_sel RS trans) THEN |
|
132 cases_tac ctxt k m excludesss THEN |
|
133 HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE' |
|
134 eresolve_tac falseEs ORELSE' |
|
135 resolve_tac split_connectI ORELSE' |
|
136 Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' |
|
137 Splitter.split_tac (split_if :: splits) ORELSE' |
|
138 eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' |
|
139 etac notE THEN' atac ORELSE' |
|
140 (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def o_def split_def |
|
141 sum.cases} @ mapsx @ map_comps @ map_idents))))); |
|
142 |
|
143 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = |
|
144 HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' |
|
145 (the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN |
|
146 unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl); |
|
147 |
|
148 fun inst_split_eq ctxt split = |
|
149 (case prop_of split of |
|
150 @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) => |
|
151 let |
|
152 val s = Name.uu; |
|
153 val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0)); |
|
154 val split' = Drule.instantiate' [] [SOME (certify ctxt eq)] split; |
|
155 in |
|
156 Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split' |
|
157 end |
|
158 | _ => split); |
|
159 |
|
160 fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr = |
|
161 let |
|
162 val splits' = |
|
163 map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits) |
|
164 in |
|
165 HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN |
|
166 prelude_tac ctxt [] (fun_ctr RS trans) THEN |
|
167 HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN' |
|
168 SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o |
|
169 (rtac refl ORELSE' atac ORELSE' |
|
170 resolve_tac (@{thm Code.abort_def} :: split_connectI) ORELSE' |
|
171 Splitter.split_tac (split_if :: splits) ORELSE' |
|
172 Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' |
|
173 mk_primcorec_assumption_tac ctxt discIs ORELSE' |
|
174 distinct_in_prems_tac distincts ORELSE' |
|
175 (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))))) |
|
176 end; |
|
177 |
|
178 fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'}); |
|
179 |
|
180 fun mk_primcorec_raw_code_tac ctxt distincts discIs splits split_asms ms fun_ctrs nchotomy_opt = |
|
181 let |
|
182 val n = length ms; |
|
183 val (ms', fun_ctrs') = |
|
184 (case nchotomy_opt of |
|
185 NONE => (ms, fun_ctrs) |
|
186 | SOME nchotomy => |
|
187 (ms |> split_last ||> K [n - 1] |> op @, |
|
188 fun_ctrs |
|
189 |> split_last |
|
190 ||> unfold_thms ctxt [atomize_conjL] |
|
191 ||> (fn thm => [rulify_nchotomy n nchotomy RS thm] handle THM _ => [thm]) |
|
192 |> op @)); |
|
193 in |
|
194 EVERY (map2 (raw_code_single_tac ctxt distincts discIs splits split_asms) ms' fun_ctrs') THEN |
|
195 IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN |
|
196 HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI))) |
|
197 end; |
|
198 |
|
199 fun mk_primcorec_code_tac ctxt distincts splits raw = |
|
200 HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' |
|
201 SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o |
|
202 (rtac refl ORELSE' atac ORELSE' |
|
203 resolve_tac split_connectI ORELSE' |
|
204 Splitter.split_tac (split_if :: splits) ORELSE' |
|
205 distinct_in_prems_tac distincts ORELSE' |
|
206 rtac sym THEN' atac ORELSE' |
|
207 etac notE THEN' atac)); |
|
208 |
|
209 end; |
|