author | blanchet |
Wed, 24 Apr 2013 15:42:00 +0200 | |
changeset 51762 | 219a3063ed29 |
parent 51761 | 4c9f08836d87 |
child 51766 | f19a4d0ab1bf |
permissions | -rw-r--r-- |
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49506
diff
changeset
|
1 |
(* Title: HOL/BNF/Tools/bnf_def_tactics.ML |
49284 | 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 |
|
49623 | 11 |
val mk_collect_set_natural_tac: thm list -> tactic |
51762 | 12 |
val mk_map_id': thm -> thm |
13 |
val mk_map_comp': thm -> thm |
|
14 |
val mk_map_cong_tac: thm -> tactic |
|
49284 | 15 |
val mk_in_mono_tac: int -> tactic |
16 |
val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic |
|
17 |
val mk_set_natural': thm -> thm |
|
18 |
||
49506 | 19 |
val mk_srel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> |
49284 | 20 |
{prems: thm list, context: Proof.context} -> tactic |
49506 | 21 |
val mk_srel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic |
22 |
val mk_srel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> |
|
49284 | 23 |
{prems: thm list, context: Proof.context} -> tactic |
49506 | 24 |
val mk_in_srel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic |
25 |
val mk_srel_converse_tac: thm -> tactic |
|
26 |
val mk_srel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list -> |
|
49284 | 27 |
{prems: thm list, context: Proof.context} -> tactic |
49506 | 28 |
val mk_srel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic |
49284 | 29 |
end; |
30 |
||
31 |
structure BNF_Def_Tactics : BNF_DEF_TACTICS = |
|
32 |
struct |
|
33 |
||
34 |
open BNF_Util |
|
35 |
open BNF_Tactics |
|
36 |
||
51762 | 37 |
fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply}; |
38 |
fun mk_map_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp]; |
|
39 |
fun mk_map_cong_tac cong0 = |
|
40 |
(hyp_subst_tac THEN' rtac cong0 THEN' |
|
41 |
REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1; |
|
49284 | 42 |
fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE}; |
49490 | 43 |
fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1 |
49284 | 44 |
else (rtac subsetI THEN' |
45 |
rtac CollectI) 1 THEN |
|
46 |
REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN |
|
47 |
REPEAT_DETERM_N (n - 1) |
|
48 |
((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN |
|
49 |
(etac subset_trans THEN' atac) 1; |
|
50 |
||
49623 | 51 |
fun mk_collect_set_natural_tac set_naturals = |
52 |
(rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN' |
|
53 |
EVERY' (map (fn set_natural => |
|
54 |
rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN' |
|
55 |
rtac set_natural) set_naturals) THEN' |
|
56 |
rtac @{thm image_empty}) 1; |
|
49284 | 57 |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
58 |
fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_naturals = |
49284 | 59 |
if null set_naturals then |
60 |
EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1 |
|
61 |
else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, |
|
62 |
REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull, |
|
63 |
REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI, |
|
64 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI, |
|
65 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
66 |
rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) |
|
67 |
set_naturals, |
|
68 |
CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans), |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
69 |
rtac (map_comp RS trans RS sym), rtac map_cong0, |
49284 | 70 |
REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans), |
71 |
rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm, |
|
72 |
rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1; |
|
73 |
||
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
74 |
fun mk_srel_Gr_tac srel_O_Grs map_id map_cong0 map_id' map_comp set_naturals |
49284 | 75 |
{context = ctxt, prems = _} = |
76 |
let |
|
77 |
val n = length set_naturals; |
|
78 |
in |
|
79 |
if null set_naturals then |
|
49506 | 80 |
unfold_thms_tac ctxt srel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 |
81 |
else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN |
|
49284 | 82 |
EVERY' [rtac equalityI, rtac subsetI, |
83 |
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
84 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 85 |
REPEAT_DETERM o etac conjE, hyp_subst_tac, |
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
86 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
87 |
rtac sym, rtac trans, rtac map_comp, rtac map_cong0, |
49284 | 88 |
REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac, |
89 |
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
90 |
rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans), |
|
91 |
rtac (@{thm snd_conv} RS sym)], |
|
92 |
rtac CollectI, |
|
93 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
94 |
rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac, |
|
95 |
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
96 |
stac @{thm fst_conv}, atac]) set_naturals, |
|
97 |
rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE], |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
98 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 99 |
REPEAT_DETERM o etac conjE, hyp_subst_tac, |
100 |
rtac @{thm relcompI}, rtac @{thm converseI}, |
|
49495 | 101 |
EVERY' (map2 (fn convol => fn map_id => |
102 |
EVERY' [rtac CollectI, rtac exI, rtac conjI, |
|
103 |
rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
104 |
rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]), |
49495 | 105 |
REPEAT_DETERM_N n o rtac (convol RS fun_cong), |
106 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
|
107 |
rtac CollectI, |
|
108 |
CONJ_WRAP' (fn thm => |
|
109 |
EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI}, |
|
110 |
rtac @{thm convol_memI[of id _ "%x. x", OF id_apply refl]}, etac set_mp, atac]) |
|
111 |
set_naturals]) |
|
112 |
@{thms fst_convol snd_convol} [map_id', refl])] 1 |
|
49284 | 113 |
end; |
114 |
||
49506 | 115 |
fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} = |
116 |
unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN |
|
49621 | 117 |
(if n = 0 then rtac refl 1 |
118 |
else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]}, |
|
119 |
rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI, |
|
120 |
CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id] 1); |
|
49284 | 121 |
|
49506 | 122 |
fun mk_srel_mono_tac srel_O_Grs in_mono {context = ctxt, prems = _} = |
123 |
unfold_thms_tac ctxt srel_O_Grs THEN |
|
49284 | 124 |
EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]}, |
125 |
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac, |
|
126 |
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1; |
|
127 |
||
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
128 |
fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong0 map_comp set_naturals |
49284 | 129 |
{context = ctxt, prems = _} = |
130 |
let |
|
131 |
val n = length set_naturals; |
|
132 |
in |
|
133 |
if null set_naturals then |
|
49506 | 134 |
unfold_thms_tac ctxt [srel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 |
135 |
else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN |
|
49284 | 136 |
EVERY' [rtac @{thm subrelI}, |
137 |
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
138 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 139 |
REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI}, |
140 |
rtac @{thm relcompI}, rtac @{thm converseI}, |
|
141 |
EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
142 |
rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
143 |
rtac map_cong0, REPEAT_DETERM_N n o rtac thm, |
49284 | 144 |
rtac (map_comp RS sym), rtac CollectI, |
145 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
146 |
etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 |
|
147 |
end; |
|
148 |
||
49506 | 149 |
fun mk_srel_converse_tac le_converse = |
49284 | 150 |
EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift}, |
151 |
rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1; |
|
152 |
||
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
153 |
fun mk_srel_O_tac srel_O_Grs srel_Id map_cong0 map_wppull map_comp set_naturals |
49284 | 154 |
{context = ctxt, prems = _} = |
155 |
let |
|
156 |
val n = length set_naturals; |
|
157 |
fun in_tac nthO_in = rtac CollectI THEN' |
|
158 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
159 |
rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals; |
|
160 |
in |
|
49506 | 161 |
if null set_naturals then unfold_thms_tac ctxt [srel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 |
162 |
else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN |
|
49284 | 163 |
EVERY' [rtac equalityI, rtac @{thm subrelI}, |
164 |
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
165 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 166 |
REPEAT_DETERM o etac conjE, hyp_subst_tac, |
167 |
rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI}, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
168 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
169 |
rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0, |
49284 | 170 |
REPEAT_DETERM_N n o rtac @{thm fst_fstO}, |
171 |
in_tac @{thm fstO_in}, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
172 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
173 |
rtac sym, rtac trans, rtac map_comp, rtac map_cong0, |
49284 | 174 |
REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst, |
175 |
rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE, |
|
176 |
etac set_mp, atac], |
|
177 |
in_tac @{thm fstO_in}, |
|
178 |
rtac @{thm relcompI}, rtac @{thm converseI}, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
179 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
180 |
rtac sym, rtac trans, rtac map_comp, rtac map_cong0, |
49284 | 181 |
REPEAT_DETERM_N n o rtac o_apply, |
182 |
in_tac @{thm sndO_in}, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
183 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
184 |
rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0, |
49284 | 185 |
REPEAT_DETERM_N n o rtac @{thm snd_sndO}, |
186 |
in_tac @{thm sndO_in}, |
|
187 |
rtac @{thm subrelI}, |
|
188 |
REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}], |
|
189 |
REPEAT_DETERM o eresolve_tac [exE, conjE], |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
190 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 191 |
REPEAT_DETERM o etac conjE, hyp_subst_tac, |
192 |
rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, |
|
193 |
CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals, |
|
194 |
etac allE, etac impE, etac conjI, etac conjI, atac, |
|
195 |
REPEAT_DETERM o eresolve_tac [bexE, conjE], |
|
196 |
rtac @{thm relcompI}, rtac @{thm converseI}, |
|
197 |
EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
198 |
rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
199 |
rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm, |
49284 | 200 |
rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1 |
201 |
end; |
|
202 |
||
49506 | 203 |
fun mk_in_srel_tac srel_O_Grs m {context = ctxt, prems = _} = |
49284 | 204 |
let |
205 |
val ls' = replicate (Int.max (1, m)) (); |
|
206 |
in |
|
49506 | 207 |
unfold_thms_tac ctxt (srel_O_Grs @ |
49284 | 208 |
@{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN |
209 |
EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, |
|
210 |
rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl, |
|
211 |
REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI, |
|
212 |
REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]}, |
|
213 |
CONJ_WRAP' (K atac) ls']] 1 |
|
214 |
end; |
|
215 |
||
216 |
end; |