author | desharna |
Mon, 06 Oct 2014 13:34:12 +0200 | |
changeset 58568 | 727e014c6dbd |
parent 58446 | e89f57d1e46c |
child 59498 | 50b60f501b05 |
permissions | -rw-r--r-- |
55061 | 1 |
(* Title: HOL/Tools/BNF/bnf_def_tactics.ML |
49284 | 2 |
Author: Dmitriy Traytel, TU Muenchen |
3 |
Author: Jasmin Blanchette, TU Muenchen |
|
57668 | 4 |
Author: Martin Desharnais, TU Muenchen |
5 |
Copyright 2012, 2013, 2014 |
|
49284 | 6 |
|
7 |
Tactics for definition of bounded natural functors. |
|
8 |
*) |
|
9 |
||
10 |
signature BNF_DEF_TACTICS = |
|
11 |
sig |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
12 |
val mk_collect_set_map_tac: thm list -> tactic |
56635 | 13 |
val mk_in_mono_tac: int -> tactic |
57970 | 14 |
val mk_inj_map_strong_tac: Proof.context -> thm -> thm list -> thm -> tactic |
56635 | 15 |
val mk_inj_map_tac: int -> thm -> thm -> thm -> thm -> tactic |
53285 | 16 |
val mk_map_id: thm -> thm |
56903 | 17 |
val mk_map_ident: Proof.context -> thm -> thm |
53288 | 18 |
val mk_map_comp: thm -> thm |
51798 | 19 |
val mk_map_cong_tac: Proof.context -> thm -> tactic |
53290 | 20 |
val mk_set_map: thm -> thm |
58106 | 21 |
val mk_set_transfer_tac: Proof.context -> thm -> thm list -> tactic |
49284 | 22 |
|
55197 | 23 |
val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic |
51894 | 24 |
val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic |
55197 | 25 |
val mk_rel_OO_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
26 |
val mk_rel_conversep_tac: thm -> thm -> tactic |
55197 | 27 |
val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic |
57932 | 28 |
val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic |
52844
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
29 |
val mk_rel_mono_tac: thm list -> thm -> tactic |
57967 | 30 |
val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic |
58104 | 31 |
val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
32 |
|
55197 | 33 |
val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic |
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
34 |
|
55197 | 35 |
val mk_in_bd_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm list -> thm list -> |
36 |
thm -> thm -> thm -> thm -> tactic |
|
54189
c0186a0d8cb3
define a trivial nonemptiness witness if none is provided
traytel
parents:
53562
diff
changeset
|
37 |
|
55197 | 38 |
val mk_trivial_wit_tac: Proof.context -> thm list -> thm list -> tactic |
49284 | 39 |
end; |
40 |
||
41 |
structure BNF_Def_Tactics : BNF_DEF_TACTICS = |
|
42 |
struct |
|
43 |
||
44 |
open BNF_Util |
|
45 |
open BNF_Tactics |
|
46 |
||
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
47 |
val ord_eq_le_trans = @{thm ord_eq_le_trans}; |
52844
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
48 |
val ord_le_eq_trans = @{thm ord_le_eq_trans}; |
52749 | 49 |
val conversep_shift = @{thm conversep_le_swap} RS iffD1; |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
50 |
|
53285 | 51 |
fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply}; |
56903 | 52 |
fun mk_map_ident ctxt = unfold_thms ctxt @{thms id_def}; |
55067 | 53 |
fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp]; |
51798 | 54 |
fun mk_map_cong_tac ctxt cong0 = |
55 |
(hyp_subst_tac ctxt THEN' rtac cong0 THEN' |
|
51762 | 56 |
REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1; |
53290 | 57 |
fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest}; |
49490 | 58 |
fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1 |
49284 | 59 |
else (rtac subsetI THEN' |
60 |
rtac CollectI) 1 THEN |
|
61 |
REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN |
|
62 |
REPEAT_DETERM_N (n - 1) |
|
63 |
((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN |
|
64 |
(etac subset_trans THEN' atac) 1; |
|
65 |
||
56635 | 66 |
fun mk_inj_map_tac n map_id map_comp map_cong0 map_cong = |
67 |
let |
|
68 |
val map_cong' = map_cong OF (asm_rl :: replicate n refl); |
|
69 |
val map_cong0' = map_cong0 OF (replicate n @{thm the_inv_f_o_f_id}); |
|
70 |
in |
|
71 |
HEADGOAL (rtac @{thm injI} THEN' etac (map_cong' RS box_equals) THEN' |
|
72 |
REPEAT_DETERM_N 2 o (rtac (box_equals OF [map_cong0', map_comp RS sym, map_id]) THEN' |
|
73 |
REPEAT_DETERM_N n o atac)) |
|
74 |
end; |
|
75 |
||
57970 | 76 |
fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong = |
77 |
let |
|
78 |
val rel_eq' = rel_eq RS @{thm predicate2_eqD}; |
|
79 |
val rel_maps' = map (fn thm => thm RS iffD1) rel_maps; |
|
80 |
in |
|
81 |
HEADGOAL (dtac (rel_eq' RS iffD2) THEN' rtac (rel_eq' RS iffD1)) THEN |
|
82 |
EVERY (map (HEADGOAL o dtac) rel_maps') THEN |
|
83 |
HEADGOAL (etac rel_mono_strong) THEN |
|
84 |
TRYALL (Goal.assume_rule_tac ctxt) |
|
85 |
end; |
|
86 |
||
53289 | 87 |
fun mk_collect_set_map_tac set_map0s = |
55067 | 88 |
(rtac (@{thm collect_comp} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN' |
53289 | 89 |
EVERY' (map (fn set_map0 => |
49623 | 90 |
rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN' |
53289 | 91 |
rtac set_map0) set_map0s) THEN' |
49623 | 92 |
rtac @{thm image_empty}) 1; |
49284 | 93 |
|
55197 | 94 |
fun mk_rel_Grp_tac ctxt rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps = |
49284 | 95 |
let |
54792 | 96 |
val n = length set_maps; |
52844
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
97 |
val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans); |
49284 | 98 |
in |
54792 | 99 |
if null set_maps then |
53270 | 100 |
unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
101 |
rtac @{thm Grp_UNIV_idI[OF refl]} 1 |
52844
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
102 |
else |
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
103 |
EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I}, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
104 |
REPEAT_DETERM o |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
105 |
eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], |
54792 | 106 |
hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
107 |
REPEAT_DETERM_N n o EVERY' [rtac @{thm Collect_split_Grp_eqD}, etac @{thm set_mp}, atac], |
49284 | 108 |
rtac CollectI, |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
109 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
110 |
rtac @{thm image_subsetI}, rtac @{thm Collect_split_Grp_inD}, etac @{thm set_mp}, atac]) |
54792 | 111 |
set_maps, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
112 |
rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE], |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
113 |
hyp_subst_tac ctxt, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
114 |
rtac @{thm relcomppI}, rtac @{thm conversepI}, |
53270 | 115 |
EVERY' (map2 (fn convol => fn map_id0 => |
55990 | 116 |
EVERY' [rtac @{thm GrpI}, |
117 |
rtac (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_id0]), |
|
49495 | 118 |
REPEAT_DETERM_N n o rtac (convol RS fun_cong), |
119 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
|
120 |
rtac CollectI, |
|
121 |
CONJ_WRAP' (fn thm => |
|
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
122 |
EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI}, |
52986
7f7bbeb16538
eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)
traytel
parents:
52844
diff
changeset
|
123 |
rtac @{thm convol_mem_GrpI}, etac set_mp, atac]) |
54792 | 124 |
set_maps]) |
53285 | 125 |
@{thms fst_convol snd_convol} [map_id, refl])] 1 |
49284 | 126 |
end; |
127 |
||
53270 | 128 |
fun mk_rel_eq_tac n rel_Grp rel_cong map_id0 = |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
129 |
(EVERY' (rtac (rel_cong RS trans) :: replicate n (rtac @{thm eq_alt})) THEN' |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
130 |
rtac (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN' |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
131 |
(if n = 0 then rtac refl |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
132 |
else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ "Grp"]}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
133 |
rtac @{thm equalityI}, rtac subset_UNIV, rtac subsetI, rtac CollectI, |
53270 | 134 |
CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id0])) 1; |
49284 | 135 |
|
57932 | 136 |
fun mk_rel_map0_tac ctxt live rel_compp rel_conversep rel_Grp map_id = |
137 |
if live = 0 then |
|
138 |
HEADGOAL (Goal.conjunction_tac) THEN |
|
139 |
unfold_thms_tac ctxt @{thms id_apply} THEN |
|
140 |
ALLGOALS (rtac refl) |
|
141 |
else |
|
142 |
let |
|
143 |
val ks = 1 upto live; |
|
144 |
in |
|
145 |
Goal.conjunction_tac 1 THEN |
|
146 |
unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN |
|
147 |
TRYALL (EVERY' [rtac iffI, rtac @{thm relcomppI}, rtac @{thm GrpI}, |
|
148 |
resolve_tac [map_id, refl], rtac CollectI, |
|
149 |
CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks, rtac @{thm relcomppI}, atac, |
|
150 |
rtac @{thm conversepI}, rtac @{thm GrpI}, resolve_tac [map_id, refl], rtac CollectI, |
|
151 |
CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks, |
|
152 |
REPEAT_DETERM o eresolve_tac @{thms relcomppE conversepE GrpE}, |
|
153 |
dtac (trans OF [sym, map_id]), hyp_subst_tac ctxt, atac]) |
|
154 |
end; |
|
155 |
||
52844
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
156 |
fun mk_rel_mono_tac rel_OO_Grps in_mono = |
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
157 |
let |
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
158 |
val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac |
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
159 |
else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN' |
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
160 |
rtac (hd rel_OO_Grps RS sym RSN (2, ord_le_eq_trans)); |
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
161 |
in |
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
162 |
EVERY' [rel_OO_Grps_tac, rtac @{thm relcompp_mono}, rtac @{thm iffD2[OF conversep_mono]}, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
163 |
rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}, |
52844
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
164 |
rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1 |
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
165 |
end; |
49284 | 166 |
|
55197 | 167 |
fun mk_rel_conversep_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps = |
49284 | 168 |
let |
54792 | 169 |
val n = length set_maps; |
52844
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
170 |
val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac |
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
171 |
else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN' |
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
172 |
rtac (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans)); |
49284 | 173 |
in |
54792 | 174 |
if null set_maps then rtac (rel_eq RS @{thm leq_conversepI}) 1 |
52844
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
175 |
else |
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
176 |
EVERY' [rel_OO_Grps_tac, rtac @{thm predicate2I}, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
177 |
REPEAT_DETERM o |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
178 |
eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
179 |
hyp_subst_tac ctxt, rtac @{thm conversepI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
180 |
EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac sym, rtac trans, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
181 |
rtac map_cong0, REPEAT_DETERM_N n o rtac thm, |
54792 | 182 |
rtac (map_comp RS sym), rtac CollectI, |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
183 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
54792 | 184 |
etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 |
49284 | 185 |
end; |
186 |
||
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
187 |
fun mk_rel_conversep_tac le_conversep rel_mono = |
52749 | 188 |
EVERY' [rtac @{thm antisym}, rtac le_conversep, rtac @{thm xt1(6)}, rtac conversep_shift, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
189 |
rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
190 |
REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1; |
49284 | 191 |
|
55197 | 192 |
fun mk_rel_OO_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps = |
49284 | 193 |
let |
54792 | 194 |
val n = length set_maps; |
49284 | 195 |
fun in_tac nthO_in = rtac CollectI THEN' |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
196 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
54792 | 197 |
rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps; |
52844
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
198 |
val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac |
54841
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54792
diff
changeset
|
199 |
else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN' |
52844
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
200 |
rtac (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN |
54841
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54792
diff
changeset
|
201 |
(2, ord_le_eq_trans)); |
49284 | 202 |
in |
54841
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54792
diff
changeset
|
203 |
if null set_maps then rtac (rel_eq RS @{thm leq_OOI}) 1 |
52844
66fa0f602cc4
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents:
52813
diff
changeset
|
204 |
else |
54841
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54792
diff
changeset
|
205 |
EVERY' [rel_OO_Grps_tac, rtac @{thm predicate2I}, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
206 |
REPEAT_DETERM o |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
207 |
eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
208 |
hyp_subst_tac ctxt, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
209 |
rtac @{thm relcomppI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI}, |
54792 | 210 |
rtac trans, rtac map_comp, rtac sym, rtac map_cong0, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
211 |
REPEAT_DETERM_N n o rtac @{thm fst_fstOp}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
212 |
in_tac @{thm fstOp_in}, |
54792 | 213 |
rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0, |
57970 | 214 |
REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
215 |
rtac ballE, rtac subst, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
216 |
rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE, |
49284 | 217 |
etac set_mp, atac], |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
218 |
in_tac @{thm fstOp_in}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
219 |
rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI}, |
54792 | 220 |
rtac trans, rtac map_comp, rtac map_cong0, |
49284 | 221 |
REPEAT_DETERM_N n o rtac o_apply, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
222 |
in_tac @{thm sndOp_in}, |
54792 | 223 |
rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac sym, rtac map_cong0, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
224 |
REPEAT_DETERM_N n o rtac @{thm snd_sndOp}, |
54841
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54792
diff
changeset
|
225 |
in_tac @{thm sndOp_in}] 1 |
49284 | 226 |
end; |
227 |
||
57967 | 228 |
fun mk_rel_mono_strong0_tac ctxt in_rel set_maps = |
54792 | 229 |
if null set_maps then atac 1 |
51916 | 230 |
else |
54998 | 231 |
unfold_tac ctxt [in_rel] THEN |
51916 | 232 |
REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN |
233 |
hyp_subst_tac ctxt 1 THEN |
|
234 |
EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]}, |
|
55163 | 235 |
CONJ_WRAP' (fn thm => |
236 |
(etac (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' atac)) |
|
237 |
set_maps] 1; |
|
51916 | 238 |
|
58104 | 239 |
fun mk_rel_transfer_tac ctxt in_rel rel_map rel_mono_strong = |
240 |
let |
|
241 |
fun last_tac iffD = |
|
242 |
HEADGOAL (etac rel_mono_strong) THEN |
|
243 |
REPEAT_DETERM (HEADGOAL (etac (@{thm predicate2_transferD} RS iffD) THEN' |
|
244 |
REPEAT_DETERM o atac)); |
|
245 |
in |
|
58446 | 246 |
REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN |
58104 | 247 |
(HEADGOAL (hyp_subst_tac ctxt THEN' rtac refl) ORELSE |
248 |
REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) :: |
|
249 |
@{thms exE conjE CollectE}))) THEN |
|
250 |
HEADGOAL (hyp_subst_tac ctxt) THEN unfold_thms_tac ctxt rel_map THEN HEADGOAL (rtac iffI) THEN |
|
251 |
last_tac iffD1 THEN last_tac iffD2) |
|
252 |
end; |
|
253 |
||
55197 | 254 |
fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp = |
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
255 |
let |
53290 | 256 |
val n = length set_maps; |
53562 | 257 |
val in_tac = if n = 0 then rtac UNIV_I else |
258 |
rtac CollectI THEN' CONJ_WRAP' (fn thm => |
|
259 |
etac (thm RS |
|
260 |
@{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]})) |
|
261 |
set_maps; |
|
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
262 |
in |
58446 | 263 |
REPEAT_DETERM_N n (HEADGOAL (rtac rel_funI)) THEN |
55945 | 264 |
unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN |
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
265 |
HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac, |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
266 |
rtac @{thm predicate2I}, dtac (in_rel RS iffD1), |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
267 |
REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt, |
53562 | 268 |
rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, in_tac, |
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
269 |
rtac conjI, |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
270 |
EVERY' (map (fn convol => |
55990 | 271 |
rtac (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN' |
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
272 |
REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})]) |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
273 |
end; |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
274 |
|
55197 | 275 |
fun mk_in_bd_tac ctxt live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds |
276 |
bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero = |
|
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
277 |
if live = 0 then |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
278 |
rtac @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order] |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
279 |
ordLeq_cexp2[OF ordLeq_refl[OF Card_order_ctwo] Card_order_csum]]} 1 |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
280 |
else |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
281 |
let |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
282 |
val bd'_Cinfinite = bd_Cinfinite RS @{thm Cinfinite_csum1}; |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
283 |
val inserts = |
57970 | 284 |
map (fn set_bd => |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
285 |
iffD2 OF [@{thm card_of_ordLeq}, @{thm ordLeq_ordIso_trans} OF |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
286 |
[set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]]) |
57970 | 287 |
set_bds; |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
288 |
in |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
289 |
EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac @{thm cprod_cinfinite_bound}, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
290 |
rtac (ctrans OF @{thms ordLeq_csum2 ordLeq_cexp2}), rtac @{thm card_of_Card_order}, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
291 |
rtac @{thm ordLeq_csum2}, rtac @{thm Card_order_ctwo}, rtac @{thm Card_order_csum}, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
292 |
rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong1}, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
293 |
if live = 1 then rtac @{thm ordIso_refl[OF Card_order_csum]} |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
294 |
else |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
295 |
REPEAT_DETERM_N (live - 2) o rtac @{thm ordIso_transitive[OF csum_cong2]} THEN' |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
296 |
REPEAT_DETERM_N (live - 1) o rtac @{thm csum_csum}, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
297 |
rtac bd_Card_order, rtac (@{thm cexp_mono2_Cnotzero} RS ctrans), rtac @{thm ordLeq_csum1}, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
298 |
rtac bd_Card_order, rtac @{thm Card_order_csum}, rtac bd_Cnotzero, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
299 |
rtac @{thm csum_Cfinite_cexp_Cinfinite}, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
300 |
rtac (if live = 1 then @{thm card_of_Card_order} else @{thm Card_order_csum}), |
53290 | 301 |
CONJ_WRAP_GEN' (rtac @{thm Cfinite_csum}) (K (rtac @{thm Cfinite_cone})) set_maps, |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
302 |
rtac bd'_Cinfinite, rtac @{thm card_of_Card_order}, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
303 |
rtac @{thm Card_order_cexp}, rtac @{thm Cinfinite_cexp}, rtac @{thm ordLeq_csum2}, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
304 |
rtac @{thm Card_order_ctwo}, rtac bd'_Cinfinite, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
305 |
rtac (Drule.rotate_prems 1 (@{thm cprod_mono2} RSN (2, ctrans))), |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
306 |
REPEAT_DETERM_N (live - 1) o |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
307 |
(rtac (bd_Cinfinite RS @{thm cprod_cexp_csum_cexp_Cinfinite} RSN (2, ctrans)) THEN' |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
308 |
rtac @{thm ordLeq_ordIso_trans[OF cprod_mono2 ordIso_symmetric[OF cprod_cexp]]}), |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
309 |
rtac @{thm ordLeq_refl[OF Card_order_cexp]}] 1 THEN |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
310 |
unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
311 |
unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN |
52813 | 312 |
EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac surj_imp_ordLeq_inst, rtac subsetI, |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
313 |
Method.insert_tac inserts, REPEAT_DETERM o dtac meta_spec, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
314 |
REPEAT_DETERM o eresolve_tac [exE, Tactic.make_elim conjunct1], etac CollectE, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
315 |
if live = 1 then K all_tac |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
316 |
else REPEAT_DETERM_N (live - 2) o (etac conjE THEN' rotate_tac ~1) THEN' etac conjE, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
317 |
rtac (Drule.rotate_prems 1 @{thm image_eqI}), rtac @{thm SigmaI}, rtac @{thm UNIV_I}, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
318 |
CONJ_WRAP_GEN' (rtac @{thm SigmaI}) |
53290 | 319 |
(K (etac @{thm If_the_inv_into_in_Func} THEN' atac)) set_maps, |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
320 |
rtac sym, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
321 |
rtac (Drule.rotate_prems 1 |
55990 | 322 |
((@{thm box_equals} OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f}, |
53288 | 323 |
map_comp RS sym, map_id]) RSN (2, trans))), |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
324 |
REPEAT_DETERM_N (2 * live) o atac, |
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55414
diff
changeset
|
325 |
REPEAT_DETERM_N live o rtac (@{thm prod.case} RS trans), |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
326 |
rtac refl, |
52813 | 327 |
rtac @{thm surj_imp_ordLeq}, rtac subsetI, rtac (Drule.rotate_prems 1 @{thm image_eqI}), |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
328 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
329 |
CONJ_WRAP' (fn thm => |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
330 |
rtac (thm RS ord_eq_le_trans) THEN' etac @{thm subset_trans[OF image_mono Un_upper1]}) |
53290 | 331 |
set_maps, |
52813 | 332 |
rtac sym, |
55990 | 333 |
rtac (@{thm box_equals} OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]}, |
53288 | 334 |
map_comp RS sym, map_id])] 1 |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
335 |
end; |
51916 | 336 |
|
55197 | 337 |
fun mk_trivial_wit_tac ctxt wit_defs set_maps = |
54189
c0186a0d8cb3
define a trivial nonemptiness witness if none is provided
traytel
parents:
53562
diff
changeset
|
338 |
unfold_thms_tac ctxt wit_defs THEN HEADGOAL (EVERY' (map (fn thm => |
c0186a0d8cb3
define a trivial nonemptiness witness if none is provided
traytel
parents:
53562
diff
changeset
|
339 |
dtac (thm RS equalityD1 RS set_mp) THEN' etac imageE THEN' atac) set_maps)) THEN ALLGOALS atac; |
c0186a0d8cb3
define a trivial nonemptiness witness if none is provided
traytel
parents:
53562
diff
changeset
|
340 |
|
58106 | 341 |
fun mk_set_transfer_tac ctxt in_rel set_maps = |
342 |
Goal.conjunction_tac 1 THEN |
|
58446 | 343 |
EVERY (map (fn set_map => HEADGOAL (rtac rel_funI) THEN |
58106 | 344 |
REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) :: |
345 |
@{thms exE conjE CollectE}))) THEN |
|
346 |
HEADGOAL (hyp_subst_tac ctxt THEN' rtac (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN' |
|
347 |
rtac @{thm rel_setI}) THEN |
|
348 |
REPEAT (HEADGOAL (etac imageE THEN' dtac @{thm set_mp} THEN' atac THEN' |
|
349 |
REPEAT_DETERM o (eresolve_tac @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN' |
|
350 |
rtac bexI THEN' etac @{thm subst_Pair[OF _ refl]} THEN' etac imageI))) set_maps); |
|
351 |
||
49284 | 352 |
end; |