|
1 (* Title: HOL/Codatatype/Tools/bnf_def_tactics.ML |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 Copyright 2012 |
|
5 |
|
6 Tactics for definition of bounded natural functors. |
|
7 *) |
|
8 |
|
9 signature BNF_DEF_TACTICS = |
|
10 sig |
|
11 val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic |
|
12 val mk_id': thm -> thm |
|
13 val mk_comp': thm -> thm |
|
14 val mk_in_mono_tac: int -> tactic |
|
15 val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic |
|
16 val mk_set_natural': thm -> thm |
|
17 |
|
18 val mk_rel_Gr_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> |
|
19 {prems: thm list, context: Proof.context} -> tactic |
|
20 val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic |
|
21 val mk_rel_O_tac: thm -> thm -> thm -> thm -> thm -> thm list -> |
|
22 {prems: thm list, context: Proof.context} -> tactic |
|
23 val mk_in_rel_tac: thm -> int -> {prems: 'b, context: Proof.context} -> tactic |
|
24 val mk_rel_converse_tac: thm -> tactic |
|
25 val mk_rel_converse_le_tac: thm -> thm -> thm -> thm -> thm list -> |
|
26 {prems: thm list, context: Proof.context} -> tactic |
|
27 val mk_rel_mono_tac: thm -> thm -> {prems: 'a, context: Proof.context} -> tactic |
|
28 end; |
|
29 |
|
30 structure BNF_Def_Tactics : BNF_DEF_TACTICS = |
|
31 struct |
|
32 |
|
33 open BNF_Util |
|
34 open BNF_Tactics |
|
35 |
|
36 val set_mp = @{thm set_mp}; |
|
37 |
|
38 fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply}; |
|
39 fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp]; |
|
40 fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE}; |
|
41 fun mk_in_mono_tac n = if n = 0 then rtac @{thm subset_UNIV} 1 |
|
42 else (rtac subsetI THEN' |
|
43 rtac CollectI) 1 THEN |
|
44 REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN |
|
45 REPEAT_DETERM_N (n - 1) |
|
46 ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN |
|
47 (etac subset_trans THEN' atac) 1; |
|
48 |
|
49 fun mk_collect_set_natural_tac ctxt set_naturals = |
|
50 substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1; |
|
51 |
|
52 fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals = |
|
53 if null set_naturals then |
|
54 EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1 |
|
55 else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, |
|
56 REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull, |
|
57 REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI, |
|
58 REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI, |
|
59 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
60 rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) |
|
61 set_naturals, |
|
62 CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans), |
|
63 rtac (map_comp RS trans RS sym), rtac map_cong, |
|
64 REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans), |
|
65 rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm, |
|
66 rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1; |
|
67 |
|
68 fun mk_rel_Gr_tac rel_def map_id map_cong map_wpull in_cong map_id' map_comp set_naturals |
|
69 {context = ctxt, prems = _} = |
|
70 let |
|
71 val n = length set_naturals; |
|
72 in |
|
73 if null set_naturals then |
|
74 Local_Defs.unfold_tac ctxt [rel_def] THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 |
|
75 else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN |
|
76 EVERY' [rtac equalityI, rtac subsetI, |
|
77 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
|
78 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
79 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
|
80 rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, |
|
81 rtac sym, rtac trans, rtac map_comp, rtac map_cong, |
|
82 REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac, |
|
83 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
84 rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans), |
|
85 rtac (@{thm snd_conv} RS sym)], |
|
86 rtac CollectI, |
|
87 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
88 rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac, |
|
89 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
90 stac @{thm fst_conv}, atac]) set_naturals, |
|
91 rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE], |
|
92 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
93 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
|
94 rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull, |
|
95 REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac, |
|
96 rtac conjI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, |
|
97 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
98 rtac @{thm image_mono}, atac]) set_naturals, |
|
99 rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE], |
|
100 rtac @{thm relcompI}, rtac @{thm converseI}, |
|
101 REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI, |
|
102 rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, etac sym, |
|
103 etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong, |
|
104 REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1 |
|
105 end; |
|
106 |
|
107 fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} = |
|
108 Local_Defs.unfold_tac ctxt [rel_Gr, @{thm Id_alt}] THEN |
|
109 subst_tac ctxt [map_id] 1 THEN |
|
110 (if n = 0 then rtac refl 1 |
|
111 else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]}, |
|
112 rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI, |
|
113 CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1); |
|
114 |
|
115 fun mk_rel_mono_tac rel_def in_mono {context = ctxt, prems = _} = |
|
116 Local_Defs.unfold_tac ctxt [rel_def] THEN |
|
117 EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]}, |
|
118 rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac, |
|
119 rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1; |
|
120 |
|
121 fun mk_rel_converse_le_tac rel_def rel_Id map_cong map_comp set_naturals |
|
122 {context = ctxt, prems = _} = |
|
123 let |
|
124 val n = length set_naturals; |
|
125 in |
|
126 if null set_naturals then |
|
127 Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 |
|
128 else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN |
|
129 EVERY' [rtac @{thm subrelI}, |
|
130 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
|
131 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
132 REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI}, |
|
133 rtac @{thm relcompI}, rtac @{thm converseI}, |
|
134 EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI, |
|
135 rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac trans, |
|
136 rtac map_cong, REPEAT_DETERM_N n o rtac thm, |
|
137 rtac (map_comp RS sym), rtac CollectI, |
|
138 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
139 etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 |
|
140 end; |
|
141 |
|
142 fun mk_rel_converse_tac le_converse = |
|
143 EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift}, |
|
144 rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1; |
|
145 |
|
146 fun mk_rel_O_tac rel_def rel_Id map_cong map_wppull map_comp set_naturals |
|
147 {context = ctxt, prems = _} = |
|
148 let |
|
149 val n = length set_naturals; |
|
150 fun in_tac nthO_in = rtac CollectI THEN' |
|
151 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
152 rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals; |
|
153 in |
|
154 if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 |
|
155 else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN |
|
156 EVERY' [rtac equalityI, rtac @{thm subrelI}, |
|
157 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
|
158 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
159 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
|
160 rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI}, |
|
161 rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, |
|
162 rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong, |
|
163 REPEAT_DETERM_N n o rtac @{thm fst_fstO}, |
|
164 in_tac @{thm fstO_in}, |
|
165 rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, |
|
166 rtac sym, rtac trans, rtac map_comp, rtac map_cong, |
|
167 REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst, |
|
168 rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE, |
|
169 etac set_mp, atac], |
|
170 in_tac @{thm fstO_in}, |
|
171 rtac @{thm relcompI}, rtac @{thm converseI}, |
|
172 rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, |
|
173 rtac sym, rtac trans, rtac map_comp, rtac map_cong, |
|
174 REPEAT_DETERM_N n o rtac o_apply, |
|
175 in_tac @{thm sndO_in}, |
|
176 rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, |
|
177 rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong, |
|
178 REPEAT_DETERM_N n o rtac @{thm snd_sndO}, |
|
179 in_tac @{thm sndO_in}, |
|
180 rtac @{thm subrelI}, |
|
181 REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}], |
|
182 REPEAT_DETERM o eresolve_tac [exE, conjE], |
|
183 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
184 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
|
185 rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, |
|
186 CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals, |
|
187 etac allE, etac impE, etac conjI, etac conjI, atac, |
|
188 REPEAT_DETERM o eresolve_tac [bexE, conjE], |
|
189 rtac @{thm relcompI}, rtac @{thm converseI}, |
|
190 EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI, |
|
191 rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac sym, rtac trans, |
|
192 rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm, |
|
193 rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1 |
|
194 end; |
|
195 |
|
196 fun mk_in_rel_tac rel_def m {context = ctxt, prems = _} = |
|
197 let |
|
198 val ls' = replicate (Int.max (1, m)) (); |
|
199 in |
|
200 Local_Defs.unfold_tac ctxt (rel_def :: |
|
201 @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN |
|
202 EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, |
|
203 rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl, |
|
204 REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI, |
|
205 REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]}, |
|
206 CONJ_WRAP' (K atac) ls']] 1 |
|
207 end; |
|
208 |
|
209 end; |