author | traytel |
Fri, 21 Sep 2012 11:44:55 +0200 | |
changeset 49488 | 02eb07152998 |
parent 49463 | 83ac281bcdc2 |
child 49490 | 394870e51d18 |
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 |
||
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49452
diff
changeset
|
18 |
val mk_rel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> |
49284 | 19 |
{prems: thm list, context: Proof.context} -> tactic |
20 |
val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic |
|
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49452
diff
changeset
|
21 |
val mk_rel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> |
49284 | 22 |
{prems: thm list, context: Proof.context} -> tactic |
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49452
diff
changeset
|
23 |
val mk_in_rel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic |
49284 | 24 |
val mk_rel_converse_tac: thm -> tactic |
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49452
diff
changeset
|
25 |
val mk_rel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list -> |
49284 | 26 |
{prems: thm list, context: Proof.context} -> tactic |
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49452
diff
changeset
|
27 |
val mk_rel_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}; |
|
39 |
fun mk_in_mono_tac n = if n = 0 then rtac @{thm subset_UNIV} 1 |
|
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 |
||
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49452
diff
changeset
|
66 |
fun mk_rel_Gr_tac rel_O_Grs map_id map_cong map_wpull in_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 |
|
49463 | 72 |
unfold_defs_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 |
73 |
else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_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 allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull, |
|
93 |
REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac, |
|
94 |
rtac conjI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, |
|
95 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
96 |
rtac @{thm image_mono}, atac]) set_naturals, |
|
97 |
rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE], |
|
98 |
rtac @{thm relcompI}, rtac @{thm converseI}, |
|
99 |
REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
100 |
rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, etac sym, |
49284 | 101 |
etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong, |
102 |
REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1 |
|
103 |
end; |
|
104 |
||
105 |
fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} = |
|
49463 | 106 |
unfold_defs_tac ctxt [rel_Gr, @{thm Id_alt}] THEN |
49284 | 107 |
subst_tac ctxt [map_id] 1 THEN |
108 |
(if n = 0 then rtac refl 1 |
|
109 |
else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]}, |
|
110 |
rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI, |
|
111 |
CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1); |
|
112 |
||
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49452
diff
changeset
|
113 |
fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} = |
49463 | 114 |
unfold_defs_tac ctxt rel_O_Grs THEN |
49284 | 115 |
EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]}, |
116 |
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac, |
|
117 |
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1; |
|
118 |
||
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49452
diff
changeset
|
119 |
fun mk_rel_converse_le_tac rel_O_Grs rel_Id map_cong map_comp set_naturals |
49284 | 120 |
{context = ctxt, prems = _} = |
121 |
let |
|
122 |
val n = length set_naturals; |
|
123 |
in |
|
124 |
if null set_naturals then |
|
49463 | 125 |
unfold_defs_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 |
126 |
else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN |
|
49284 | 127 |
EVERY' [rtac @{thm subrelI}, |
128 |
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
|
129 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 130 |
REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI}, |
131 |
rtac @{thm relcompI}, rtac @{thm converseI}, |
|
132 |
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
|
133 |
rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans, |
49284 | 134 |
rtac map_cong, REPEAT_DETERM_N n o rtac thm, |
135 |
rtac (map_comp RS sym), rtac CollectI, |
|
136 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
137 |
etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 |
|
138 |
end; |
|
139 |
||
140 |
fun mk_rel_converse_tac le_converse = |
|
141 |
EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift}, |
|
142 |
rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1; |
|
143 |
||
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49452
diff
changeset
|
144 |
fun mk_rel_O_tac rel_O_Grs rel_Id map_cong map_wppull map_comp set_naturals |
49284 | 145 |
{context = ctxt, prems = _} = |
146 |
let |
|
147 |
val n = length set_naturals; |
|
148 |
fun in_tac nthO_in = rtac CollectI THEN' |
|
149 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
150 |
rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals; |
|
151 |
in |
|
49463 | 152 |
if null set_naturals then unfold_defs_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 |
153 |
else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN |
|
49284 | 154 |
EVERY' [rtac equalityI, rtac @{thm subrelI}, |
155 |
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
|
156 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 157 |
REPEAT_DETERM o etac conjE, hyp_subst_tac, |
158 |
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
|
159 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
49284 | 160 |
rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong, |
161 |
REPEAT_DETERM_N n o rtac @{thm fst_fstO}, |
|
162 |
in_tac @{thm fstO_in}, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
163 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
49284 | 164 |
rtac sym, rtac trans, rtac map_comp, rtac map_cong, |
165 |
REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst, |
|
166 |
rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE, |
|
167 |
etac set_mp, atac], |
|
168 |
in_tac @{thm fstO_in}, |
|
169 |
rtac @{thm relcompI}, rtac @{thm converseI}, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
170 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
49284 | 171 |
rtac sym, rtac trans, rtac map_comp, rtac map_cong, |
172 |
REPEAT_DETERM_N n o rtac o_apply, |
|
173 |
in_tac @{thm sndO_in}, |
|
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
174 |
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, |
49284 | 175 |
rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong, |
176 |
REPEAT_DETERM_N n o rtac @{thm snd_sndO}, |
|
177 |
in_tac @{thm sndO_in}, |
|
178 |
rtac @{thm subrelI}, |
|
179 |
REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}], |
|
180 |
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
|
181 |
REPEAT_DETERM o dtac Pair_eqD, |
49284 | 182 |
REPEAT_DETERM o etac conjE, hyp_subst_tac, |
183 |
rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, |
|
184 |
CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals, |
|
185 |
etac allE, etac impE, etac conjI, etac conjI, atac, |
|
186 |
REPEAT_DETERM o eresolve_tac [bexE, conjE], |
|
187 |
rtac @{thm relcompI}, rtac @{thm converseI}, |
|
188 |
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
|
189 |
rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans, |
49284 | 190 |
rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm, |
191 |
rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1 |
|
192 |
end; |
|
193 |
||
49460
4dd451a075ce
fixed infinite loop with trivial rel_O_Gr + tuning
blanchet
parents:
49452
diff
changeset
|
194 |
fun mk_in_rel_tac rel_O_Grs m {context = ctxt, prems = _} = |
49284 | 195 |
let |
196 |
val ls' = replicate (Int.max (1, m)) (); |
|
197 |
in |
|
49463 | 198 |
unfold_defs_tac ctxt (rel_O_Grs @ |
49284 | 199 |
@{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN |
200 |
EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, |
|
201 |
rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl, |
|
202 |
REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI, |
|
203 |
REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]}, |
|
204 |
CONJ_WRAP' (K atac) ls']] 1 |
|
205 |
end; |
|
206 |
||
207 |
end; |