author | blanchet |
Fri, 21 Sep 2012 15:53:29 +0200 | |
changeset 49506 | aeb0cc8889f2 |
parent 49504 | df9b897fb254 |
child 49509 | 163914705f8d |
permissions | -rw-r--r-- |
49284 | 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 |
||
49506 | 18 |
val mk_srel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> |
49284 | 19 |
{prems: thm list, context: Proof.context} -> tactic |
49506 | 20 |
val mk_srel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic |
21 |
val mk_srel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> |
|
49284 | 22 |
{prems: thm list, context: Proof.context} -> tactic |
49506 | 23 |
val mk_in_srel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic |
24 |
val mk_srel_converse_tac: thm -> tactic |
|
25 |
val mk_srel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list -> |
|
49284 | 26 |
{prems: thm list, context: Proof.context} -> tactic |
49506 | 27 |
val mk_srel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic |
49284 | 28 |
end; |
29 |
||
30 |
structure BNF_Def_Tactics : BNF_DEF_TACTICS = |
|
31 |
struct |
|
32 |
||
33 |
open BNF_Util |
|
34 |
open BNF_Tactics |
|
35 |
||
36 |
fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply}; |
|
37 |
fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp]; |
|
38 |
fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE}; |
|
49490 | 39 |
fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1 |
49284 | 40 |
else (rtac subsetI THEN' |
41 |
rtac CollectI) 1 THEN |
|
42 |
REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN |
|
43 |
REPEAT_DETERM_N (n - 1) |
|
44 |
((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN |
|
45 |
(etac subset_trans THEN' atac) 1; |
|
46 |
||
47 |
fun mk_collect_set_natural_tac ctxt set_naturals = |
|
48 |
substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1; |
|
49 |
||
50 |
fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals = |
|
51 |
if null set_naturals then |
|
52 |
EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1 |
|
53 |
else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, |
|
54 |
REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull, |
|
55 |
REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI, |
|
56 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI, |
|
57 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
58 |
rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) |
|
59 |
set_naturals, |
|
60 |
CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans), |
|
61 |
rtac (map_comp RS trans RS sym), rtac map_cong, |
|
62 |
REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans), |
|
63 |
rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm, |
|
64 |
rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1; |
|
65 |
||
49506 | 66 |
fun mk_srel_Gr_tac srel_O_Grs map_id map_cong map_id' map_comp set_naturals |
49284 | 67 |
{context = ctxt, prems = _} = |
68 |
let |
|
69 |
val n = length set_naturals; |
|
70 |
in |
|
71 |
if null set_naturals then |
|
49506 | 72 |
unfold_thms_tac ctxt srel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 |
73 |
else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN |
|
49284 | 74 |
EVERY' [rtac equalityI, rtac subsetI, |
75 |
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
|
76 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 77 |
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
|
78 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
49284 | 79 |
rtac sym, rtac trans, rtac map_comp, rtac map_cong, |
80 |
REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac, |
|
81 |
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
82 |
rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans), |
|
83 |
rtac (@{thm snd_conv} RS sym)], |
|
84 |
rtac CollectI, |
|
85 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
86 |
rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac, |
|
87 |
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
88 |
stac @{thm fst_conv}, atac]) set_naturals, |
|
89 |
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
|
90 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 91 |
REPEAT_DETERM o etac conjE, hyp_subst_tac, |
92 |
rtac @{thm relcompI}, rtac @{thm converseI}, |
|
49495 | 93 |
EVERY' (map2 (fn convol => fn map_id => |
94 |
EVERY' [rtac CollectI, rtac exI, rtac conjI, |
|
95 |
rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, |
|
96 |
rtac (box_equals OF [map_cong, map_comp RS sym, map_id]), |
|
97 |
REPEAT_DETERM_N n o rtac (convol RS fun_cong), |
|
98 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
|
99 |
rtac CollectI, |
|
100 |
CONJ_WRAP' (fn thm => |
|
101 |
EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI}, |
|
102 |
rtac @{thm convol_memI[of id _ "%x. x", OF id_apply refl]}, etac set_mp, atac]) |
|
103 |
set_naturals]) |
|
104 |
@{thms fst_convol snd_convol} [map_id', refl])] 1 |
|
49284 | 105 |
end; |
106 |
||
49506 | 107 |
fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} = |
108 |
unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN |
|
49284 | 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]}, |
|
49490 | 112 |
rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI, |
113 |
CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac refl] 1); |
|
49284 | 114 |
|
49506 | 115 |
fun mk_srel_mono_tac srel_O_Grs in_mono {context = ctxt, prems = _} = |
116 |
unfold_thms_tac ctxt srel_O_Grs THEN |
|
49284 | 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 |
||
49506 | 121 |
fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong map_comp set_naturals |
49284 | 122 |
{context = ctxt, prems = _} = |
123 |
let |
|
124 |
val n = length set_naturals; |
|
125 |
in |
|
126 |
if null set_naturals then |
|
49506 | 127 |
unfold_thms_tac ctxt [srel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 |
128 |
else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN |
|
49284 | 129 |
EVERY' [rtac @{thm subrelI}, |
130 |
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
|
131 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 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, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
135 |
rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans, |
49284 | 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 |
||
49506 | 142 |
fun mk_srel_converse_tac le_converse = |
49284 | 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 |
||
49506 | 146 |
fun mk_srel_O_tac srel_O_Grs srel_Id map_cong map_wppull map_comp set_naturals |
49284 | 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 |
|
49506 | 154 |
if null set_naturals then unfold_thms_tac ctxt [srel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 |
155 |
else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN |
|
49284 | 156 |
EVERY' [rtac equalityI, rtac @{thm subrelI}, |
157 |
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
|
158 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 159 |
REPEAT_DETERM o etac conjE, hyp_subst_tac, |
160 |
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
|
161 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
49284 | 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}, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
165 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
49284 | 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}, |
|
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, |
49284 | 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}, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
176 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
49284 | 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], |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
183 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 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, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
191 |
rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans, |
49284 | 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 |
||
49506 | 196 |
fun mk_in_srel_tac srel_O_Grs m {context = ctxt, prems = _} = |
49284 | 197 |
let |
198 |
val ls' = replicate (Int.max (1, m)) (); |
|
199 |
in |
|
49506 | 200 |
unfold_thms_tac ctxt (srel_O_Grs @ |
49284 | 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; |