author | traytel |
Wed, 17 Feb 2016 15:18:06 +0100 | |
changeset 62329 | 9f7fa08d2307 |
parent 62324 | ae44f16dcea5 |
child 62617 | b5ec623952d2 |
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 |
62324 | 5 |
Author: Ondrej Kuncar, TU Muenchen |
6 |
Copyright 2012, 2013, 2014, 2015 |
|
49284 | 7 |
|
8 |
Tactics for definition of bounded natural functors. |
|
9 |
*) |
|
10 |
||
11 |
signature BNF_DEF_TACTICS = |
|
12 |
sig |
|
60728 | 13 |
val mk_collect_set_map_tac: Proof.context -> thm list -> tactic |
14 |
val mk_in_mono_tac: Proof.context -> int -> tactic |
|
57970 | 15 |
val mk_inj_map_strong_tac: Proof.context -> thm -> thm list -> thm -> tactic |
60728 | 16 |
val mk_inj_map_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic |
53285 | 17 |
val mk_map_id: thm -> thm |
56903 | 18 |
val mk_map_ident: Proof.context -> thm -> thm |
53288 | 19 |
val mk_map_comp: thm -> thm |
51798 | 20 |
val mk_map_cong_tac: Proof.context -> thm -> tactic |
53290 | 21 |
val mk_set_map: thm -> thm |
49284 | 22 |
|
55197 | 23 |
val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic |
60728 | 24 |
val mk_rel_eq_tac: Proof.context -> int -> thm -> thm -> thm -> tactic |
55197 | 25 |
val mk_rel_OO_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic |
60728 | 26 |
val mk_rel_conversep_tac: Proof.context -> 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 |
60728 | 29 |
val mk_rel_mono_tac: Proof.context -> thm list -> thm -> tactic |
57967 | 30 |
val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic |
61242 | 31 |
val mk_rel_cong_tac: Proof.context -> thm list * thm list -> thm -> tactic |
62324 | 32 |
val mk_rel_eq_onp_tac: Proof.context -> thm -> thm -> thm -> tactic |
33 |
val mk_pred_mono_strong0_tac: Proof.context -> thm -> 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
|
34 |
|
55197 | 35 |
val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic |
62329 | 36 |
val mk_pred_transfer_tac: Proof.context -> int -> thm -> thm -> thm -> tactic |
37 |
val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic |
|
38 |
val mk_set_transfer_tac: Proof.context -> thm -> thm list -> tactic |
|
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
39 |
|
55197 | 40 |
val mk_in_bd_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm list -> thm list -> |
41 |
thm -> thm -> thm -> thm -> tactic |
|
54189
c0186a0d8cb3
define a trivial nonemptiness witness if none is provided
traytel
parents:
53562
diff
changeset
|
42 |
|
55197 | 43 |
val mk_trivial_wit_tac: Proof.context -> thm list -> thm list -> tactic |
49284 | 44 |
end; |
45 |
||
46 |
structure BNF_Def_Tactics : BNF_DEF_TACTICS = |
|
47 |
struct |
|
48 |
||
49 |
open BNF_Util |
|
50 |
open BNF_Tactics |
|
51 |
||
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
52 |
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
|
53 |
val ord_le_eq_trans = @{thm ord_le_eq_trans}; |
52749 | 54 |
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
|
55 |
|
53285 | 56 |
fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply}; |
56903 | 57 |
fun mk_map_ident ctxt = unfold_thms ctxt @{thms id_def}; |
55067 | 58 |
fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp]; |
51798 | 59 |
fun mk_map_cong_tac ctxt cong0 = |
60728 | 60 |
(hyp_subst_tac ctxt THEN' rtac ctxt cong0 THEN' |
60752 | 61 |
REPEAT_DETERM o (dtac ctxt meta_spec THEN' etac ctxt meta_mp THEN' assume_tac ctxt)) 1; |
53290 | 62 |
fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest}; |
60757 | 63 |
|
64 |
fun mk_in_mono_tac ctxt n = |
|
65 |
if n = 0 then rtac ctxt subset_UNIV 1 |
|
66 |
else |
|
67 |
(rtac ctxt subsetI THEN' rtac ctxt CollectI) 1 THEN |
|
68 |
REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) THEN |
|
69 |
REPEAT_DETERM_N (n - 1) |
|
70 |
((rtac ctxt conjI THEN' etac ctxt subset_trans THEN' assume_tac ctxt) 1) THEN |
|
71 |
(etac ctxt subset_trans THEN' assume_tac ctxt) 1; |
|
49284 | 72 |
|
60728 | 73 |
fun mk_inj_map_tac ctxt n map_id map_comp map_cong0 map_cong = |
56635 | 74 |
let |
75 |
val map_cong' = map_cong OF (asm_rl :: replicate n refl); |
|
76 |
val map_cong0' = map_cong0 OF (replicate n @{thm the_inv_f_o_f_id}); |
|
77 |
in |
|
60728 | 78 |
HEADGOAL (rtac ctxt @{thm injI} THEN' etac ctxt (map_cong' RS box_equals) THEN' |
79 |
REPEAT_DETERM_N 2 o (rtac ctxt (box_equals OF [map_cong0', map_comp RS sym, map_id]) THEN' |
|
60752 | 80 |
REPEAT_DETERM_N n o assume_tac ctxt)) |
56635 | 81 |
end; |
82 |
||
57970 | 83 |
fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong = |
84 |
let |
|
85 |
val rel_eq' = rel_eq RS @{thm predicate2_eqD}; |
|
86 |
val rel_maps' = map (fn thm => thm RS iffD1) rel_maps; |
|
87 |
in |
|
60728 | 88 |
HEADGOAL (dtac ctxt (rel_eq' RS iffD2) THEN' rtac ctxt (rel_eq' RS iffD1)) THEN |
89 |
EVERY (map (HEADGOAL o dtac ctxt) rel_maps') THEN |
|
90 |
HEADGOAL (etac ctxt rel_mono_strong) THEN |
|
57970 | 91 |
TRYALL (Goal.assume_rule_tac ctxt) |
92 |
end; |
|
93 |
||
60728 | 94 |
fun mk_collect_set_map_tac ctxt set_map0s = |
95 |
(rtac ctxt (@{thm collect_comp} RS trans) THEN' rtac ctxt @{thm arg_cong[of _ _ collect]} THEN' |
|
53289 | 96 |
EVERY' (map (fn set_map0 => |
60728 | 97 |
rtac ctxt (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN' |
98 |
rtac ctxt set_map0) set_map0s) THEN' |
|
99 |
rtac ctxt @{thm image_empty}) 1; |
|
49284 | 100 |
|
55197 | 101 |
fun mk_rel_Grp_tac ctxt rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps = |
49284 | 102 |
let |
54792 | 103 |
val n = length set_maps; |
61760 | 104 |
val rel_OO_Grps_tac = |
105 |
if null rel_OO_Grps then K all_tac else rtac ctxt (hd rel_OO_Grps RS trans); |
|
49284 | 106 |
in |
54792 | 107 |
if null set_maps then |
53270 | 108 |
unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN |
60728 | 109 |
rtac ctxt @{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
|
110 |
else |
60728 | 111 |
EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm antisym}, rtac ctxt @{thm predicate2I}, |
61760 | 112 |
REPEAT_DETERM o eresolve_tac ctxt |
113 |
[CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], |
|
114 |
hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, |
|
115 |
rtac ctxt map_cong0, |
|
116 |
REPEAT_DETERM_N n o EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD}, |
|
117 |
etac ctxt @{thm set_mp}, assume_tac ctxt], |
|
60728 | 118 |
rtac ctxt CollectI, |
119 |
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans), |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61242
diff
changeset
|
120 |
rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_case_prod_Grp_in}, |
60752 | 121 |
etac ctxt @{thm set_mp}, assume_tac ctxt]) |
54792 | 122 |
set_maps, |
60728 | 123 |
rtac ctxt @{thm predicate2I}, REPEAT_DETERM o eresolve_tac ctxt [@{thm GrpE}, exE, conjE], |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
124 |
hyp_subst_tac ctxt, |
60728 | 125 |
rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, |
53270 | 126 |
EVERY' (map2 (fn convol => fn map_id0 => |
60728 | 127 |
EVERY' [rtac ctxt @{thm GrpI}, |
128 |
rtac ctxt (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_id0]), |
|
129 |
REPEAT_DETERM_N n o rtac ctxt (convol RS fun_cong), |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58446
diff
changeset
|
130 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], |
60728 | 131 |
rtac ctxt CollectI, |
49495 | 132 |
CONJ_WRAP' (fn thm => |
60728 | 133 |
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI}, |
60752 | 134 |
rtac ctxt @{thm convol_mem_GrpI}, etac ctxt set_mp, assume_tac ctxt]) |
54792 | 135 |
set_maps]) |
53285 | 136 |
@{thms fst_convol snd_convol} [map_id, refl])] 1 |
49284 | 137 |
end; |
138 |
||
60728 | 139 |
fun mk_rel_eq_tac ctxt n rel_Grp rel_cong map_id0 = |
140 |
(EVERY' (rtac ctxt (rel_cong RS trans) :: replicate n (rtac ctxt @{thm eq_alt})) THEN' |
|
141 |
rtac ctxt (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN' |
|
142 |
(if n = 0 then rtac ctxt refl |
|
143 |
else EVERY' [rtac ctxt @{thm arg_cong2[of _ _ _ _ "Grp"]}, |
|
144 |
rtac ctxt @{thm equalityI}, rtac ctxt subset_UNIV, rtac ctxt subsetI, rtac ctxt CollectI, |
|
145 |
CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto n), rtac ctxt map_id0])) 1; |
|
49284 | 146 |
|
57932 | 147 |
fun mk_rel_map0_tac ctxt live rel_compp rel_conversep rel_Grp map_id = |
148 |
if live = 0 then |
|
149 |
HEADGOAL (Goal.conjunction_tac) THEN |
|
150 |
unfold_thms_tac ctxt @{thms id_apply} THEN |
|
60728 | 151 |
ALLGOALS (rtac ctxt refl) |
57932 | 152 |
else |
153 |
let |
|
154 |
val ks = 1 upto live; |
|
155 |
in |
|
156 |
Goal.conjunction_tac 1 THEN |
|
157 |
unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN |
|
60728 | 158 |
TRYALL (EVERY' [rtac ctxt iffI, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm GrpI}, |
159 |
resolve_tac ctxt [map_id, refl], rtac ctxt CollectI, |
|
61760 | 160 |
CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI}, |
161 |
assume_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, |
|
162 |
resolve_tac ctxt [map_id, refl], rtac ctxt CollectI, |
|
60728 | 163 |
CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58446
diff
changeset
|
164 |
REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE}, |
60752 | 165 |
dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, assume_tac ctxt]) |
57932 | 166 |
end; |
167 |
||
60728 | 168 |
fun mk_rel_mono_tac ctxt rel_OO_Grps in_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
|
169 |
let |
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 |
60728 | 171 |
else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN' |
172 |
rtac ctxt (hd rel_OO_Grps RS sym RSN (2, ord_le_eq_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
|
173 |
in |
60728 | 174 |
EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm relcompp_mono}, rtac ctxt @{thm iffD2[OF conversep_mono]}, |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61242
diff
changeset
|
175 |
rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono}, |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61242
diff
changeset
|
176 |
rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono}] 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
|
177 |
end; |
49284 | 178 |
|
55197 | 179 |
fun mk_rel_conversep_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps = |
49284 | 180 |
let |
54792 | 181 |
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
|
182 |
val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac |
60728 | 183 |
else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN' |
184 |
rtac ctxt (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans)); |
|
49284 | 185 |
in |
60728 | 186 |
if null set_maps then rtac ctxt (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
|
187 |
else |
60728 | 188 |
EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I}, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
189 |
REPEAT_DETERM o |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58446
diff
changeset
|
190 |
eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], |
60728 | 191 |
hyp_subst_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, |
192 |
EVERY' (map (fn thm => EVERY' [rtac ctxt @{thm GrpI}, rtac ctxt sym, rtac ctxt trans, |
|
193 |
rtac ctxt map_cong0, REPEAT_DETERM_N n o rtac ctxt thm, |
|
194 |
rtac ctxt (map_comp RS sym), rtac ctxt CollectI, |
|
195 |
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans), |
|
196 |
etac ctxt @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 |
|
49284 | 197 |
end; |
198 |
||
60728 | 199 |
fun mk_rel_conversep_tac ctxt le_conversep rel_mono = |
200 |
EVERY' [rtac ctxt @{thm antisym}, rtac ctxt le_conversep, rtac ctxt @{thm xt1(6)}, rtac ctxt conversep_shift, |
|
201 |
rtac ctxt le_conversep, rtac ctxt @{thm iffD2[OF conversep_mono]}, rtac ctxt rel_mono, |
|
202 |
REPEAT_DETERM o rtac ctxt @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1; |
|
49284 | 203 |
|
55197 | 204 |
fun mk_rel_OO_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps = |
49284 | 205 |
let |
54792 | 206 |
val n = length set_maps; |
60728 | 207 |
fun in_tac nthO_in = rtac ctxt CollectI THEN' |
208 |
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans), |
|
60752 | 209 |
rtac ctxt @{thm image_subsetI}, rtac ctxt nthO_in, etac ctxt set_mp, assume_tac ctxt]) 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
|
210 |
val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac |
60728 | 211 |
else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN' |
212 |
rtac ctxt (@{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
|
213 |
(2, ord_le_eq_trans)); |
49284 | 214 |
in |
60728 | 215 |
if null set_maps then rtac ctxt (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
|
216 |
else |
60728 | 217 |
EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I}, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
218 |
REPEAT_DETERM o |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58446
diff
changeset
|
219 |
eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
220 |
hyp_subst_tac ctxt, |
60728 | 221 |
rtac ctxt @{thm relcomppI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, |
222 |
rtac ctxt trans, rtac ctxt map_comp, rtac ctxt sym, rtac ctxt map_cong0, |
|
223 |
REPEAT_DETERM_N n o rtac ctxt @{thm fst_fstOp}, |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
224 |
in_tac @{thm fstOp_in}, |
60728 | 225 |
rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0, |
226 |
REPEAT_DETERM_N n o EVERY' [rtac ctxt trans, rtac ctxt o_apply, |
|
227 |
rtac ctxt ballE, rtac ctxt subst, |
|
60752 | 228 |
rtac ctxt @{thm csquare_def}, rtac ctxt @{thm csquare_fstOp_sndOp}, assume_tac ctxt, |
229 |
etac ctxt notE, etac ctxt set_mp, assume_tac ctxt], |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
230 |
in_tac @{thm fstOp_in}, |
60728 | 231 |
rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, |
232 |
rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0, |
|
233 |
REPEAT_DETERM_N n o rtac ctxt o_apply, |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
234 |
in_tac @{thm sndOp_in}, |
60728 | 235 |
rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt sym, rtac ctxt map_cong0, |
236 |
REPEAT_DETERM_N n o rtac ctxt @{thm snd_sndOp}, |
|
54841
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54792
diff
changeset
|
237 |
in_tac @{thm sndOp_in}] 1 |
49284 | 238 |
end; |
239 |
||
57967 | 240 |
fun mk_rel_mono_strong0_tac ctxt in_rel set_maps = |
60752 | 241 |
if null set_maps then assume_tac ctxt 1 |
51916 | 242 |
else |
54998 | 243 |
unfold_tac ctxt [in_rel] THEN |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58446
diff
changeset
|
244 |
REPEAT_DETERM (eresolve_tac ctxt [exE, CollectE, conjE] 1) THEN |
51916 | 245 |
hyp_subst_tac ctxt 1 THEN |
60728 | 246 |
EVERY' [rtac ctxt exI, rtac ctxt @{thm conjI[OF CollectI conjI[OF refl refl]]}, |
55163 | 247 |
CONJ_WRAP' (fn thm => |
60752 | 248 |
(etac ctxt (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' assume_tac ctxt)) |
55163 | 249 |
set_maps] 1; |
51916 | 250 |
|
58104 | 251 |
fun mk_rel_transfer_tac ctxt in_rel rel_map rel_mono_strong = |
252 |
let |
|
253 |
fun last_tac iffD = |
|
60728 | 254 |
HEADGOAL (etac ctxt rel_mono_strong) THEN |
255 |
REPEAT_DETERM (HEADGOAL (etac ctxt (@{thm predicate2_transferD} RS iffD) THEN' |
|
60752 | 256 |
REPEAT_DETERM o assume_tac ctxt)); |
58104 | 257 |
in |
60728 | 258 |
REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN |
259 |
(HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl) ORELSE |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58446
diff
changeset
|
260 |
REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) :: |
58104 | 261 |
@{thms exE conjE CollectE}))) THEN |
60728 | 262 |
HEADGOAL (hyp_subst_tac ctxt) THEN unfold_thms_tac ctxt rel_map THEN HEADGOAL (rtac ctxt iffI) THEN |
58104 | 263 |
last_tac iffD1 THEN last_tac iffD2) |
264 |
end; |
|
265 |
||
55197 | 266 |
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
|
267 |
let |
53290 | 268 |
val n = length set_maps; |
60728 | 269 |
val in_tac = if n = 0 then rtac ctxt UNIV_I else |
270 |
rtac ctxt CollectI THEN' CONJ_WRAP' (fn thm => |
|
271 |
etac ctxt (thm RS |
|
53562 | 272 |
@{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]})) |
273 |
set_maps; |
|
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
274 |
in |
60728 | 275 |
REPEAT_DETERM_N n (HEADGOAL (rtac ctxt rel_funI)) THEN |
55945 | 276 |
unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN |
60752 | 277 |
HEADGOAL (EVERY' [rtac ctxt @{thm order_trans}, rtac ctxt rel_mono, |
278 |
REPEAT_DETERM_N n o assume_tac ctxt, |
|
60728 | 279 |
rtac ctxt @{thm predicate2I}, dtac ctxt (in_rel RS iffD1), |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58446
diff
changeset
|
280 |
REPEAT_DETERM o eresolve_tac ctxt [exE, CollectE, conjE], hyp_subst_tac ctxt, |
60728 | 281 |
rtac ctxt @{thm vimage2pI}, rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, in_tac, |
282 |
rtac ctxt conjI, |
|
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
283 |
EVERY' (map (fn convol => |
60728 | 284 |
rtac ctxt (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN' |
285 |
REPEAT_DETERM_N n o rtac ctxt (convol RS fun_cong)) @{thms fst_convol snd_convol})]) |
|
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
286 |
end; |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
287 |
|
55197 | 288 |
fun mk_in_bd_tac ctxt live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds |
289 |
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
|
290 |
if live = 0 then |
60728 | 291 |
rtac ctxt @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order] |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
292 |
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
|
293 |
else |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
294 |
let |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
295 |
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
|
296 |
val inserts = |
57970 | 297 |
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
|
298 |
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
|
299 |
[set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]]) |
57970 | 300 |
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
|
301 |
in |
60728 | 302 |
EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt @{thm cprod_cinfinite_bound}, |
303 |
rtac ctxt (ctrans OF @{thms ordLeq_csum2 ordLeq_cexp2}), rtac ctxt @{thm card_of_Card_order}, |
|
304 |
rtac ctxt @{thm ordLeq_csum2}, rtac ctxt @{thm Card_order_ctwo}, rtac ctxt @{thm Card_order_csum}, |
|
305 |
rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm cexp_cong1}, |
|
306 |
if live = 1 then rtac ctxt @{thm ordIso_refl[OF Card_order_csum]} |
|
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
307 |
else |
60728 | 308 |
REPEAT_DETERM_N (live - 2) o rtac ctxt @{thm ordIso_transitive[OF csum_cong2]} THEN' |
309 |
REPEAT_DETERM_N (live - 1) o rtac ctxt @{thm csum_csum}, |
|
310 |
rtac ctxt bd_Card_order, rtac ctxt (@{thm cexp_mono2_Cnotzero} RS ctrans), rtac ctxt @{thm ordLeq_csum1}, |
|
311 |
rtac ctxt bd_Card_order, rtac ctxt @{thm Card_order_csum}, rtac ctxt bd_Cnotzero, |
|
312 |
rtac ctxt @{thm csum_Cfinite_cexp_Cinfinite}, |
|
313 |
rtac ctxt (if live = 1 then @{thm card_of_Card_order} else @{thm Card_order_csum}), |
|
314 |
CONJ_WRAP_GEN' (rtac ctxt @{thm Cfinite_csum}) (K (rtac ctxt @{thm Cfinite_cone})) set_maps, |
|
315 |
rtac ctxt bd'_Cinfinite, rtac ctxt @{thm card_of_Card_order}, |
|
316 |
rtac ctxt @{thm Card_order_cexp}, rtac ctxt @{thm Cinfinite_cexp}, rtac ctxt @{thm ordLeq_csum2}, |
|
317 |
rtac ctxt @{thm Card_order_ctwo}, rtac ctxt bd'_Cinfinite, |
|
318 |
rtac ctxt (Drule.rotate_prems 1 (@{thm cprod_mono2} RSN (2, ctrans))), |
|
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
319 |
REPEAT_DETERM_N (live - 1) o |
60728 | 320 |
(rtac ctxt (bd_Cinfinite RS @{thm cprod_cexp_csum_cexp_Cinfinite} RSN (2, ctrans)) THEN' |
321 |
rtac ctxt @{thm ordLeq_ordIso_trans[OF cprod_mono2 ordIso_symmetric[OF cprod_cexp]]}), |
|
322 |
rtac ctxt @{thm ordLeq_refl[OF Card_order_cexp]}] 1 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
|
323 |
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
|
324 |
unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN |
60728 | 325 |
EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst, rtac ctxt subsetI, |
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61760
diff
changeset
|
326 |
Method.insert_tac ctxt inserts, REPEAT_DETERM o dtac ctxt meta_spec, |
60728 | 327 |
REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1], etac ctxt CollectE, |
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 |
if live = 1 then K all_tac |
60728 | 329 |
else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE, |
330 |
rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), rtac ctxt @{thm SigmaI}, rtac ctxt @{thm UNIV_I}, |
|
331 |
CONJ_WRAP_GEN' (rtac ctxt @{thm SigmaI}) |
|
60752 | 332 |
(K (etac ctxt @{thm If_the_inv_into_in_Func} THEN' assume_tac ctxt)) set_maps, |
60728 | 333 |
rtac ctxt sym, |
334 |
rtac ctxt (Drule.rotate_prems 1 |
|
55990 | 335 |
((@{thm box_equals} OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f}, |
53288 | 336 |
map_comp RS sym, map_id]) RSN (2, trans))), |
60752 | 337 |
REPEAT_DETERM_N (2 * live) o assume_tac ctxt, |
60728 | 338 |
REPEAT_DETERM_N live o rtac ctxt (@{thm prod.case} RS trans), |
339 |
rtac ctxt refl, |
|
340 |
rtac ctxt @{thm surj_imp_ordLeq}, rtac ctxt subsetI, rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), |
|
341 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt 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
|
342 |
CONJ_WRAP' (fn thm => |
60728 | 343 |
rtac ctxt (thm RS ord_eq_le_trans) THEN' etac ctxt @{thm subset_trans[OF image_mono Un_upper1]}) |
53290 | 344 |
set_maps, |
60728 | 345 |
rtac ctxt sym, |
346 |
rtac ctxt (@{thm box_equals} OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]}, |
|
53288 | 347 |
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
|
348 |
end; |
51916 | 349 |
|
55197 | 350 |
fun mk_trivial_wit_tac ctxt wit_defs set_maps = |
60752 | 351 |
unfold_thms_tac ctxt wit_defs THEN |
352 |
HEADGOAL (EVERY' (map (fn thm => |
|
353 |
dtac ctxt (thm RS equalityD1 RS set_mp) THEN' etac ctxt imageE THEN' assume_tac ctxt) set_maps)) THEN |
|
354 |
ALLGOALS (assume_tac ctxt); |
|
54189
c0186a0d8cb3
define a trivial nonemptiness witness if none is provided
traytel
parents:
53562
diff
changeset
|
355 |
|
58106 | 356 |
fun mk_set_transfer_tac ctxt in_rel set_maps = |
357 |
Goal.conjunction_tac 1 THEN |
|
60728 | 358 |
EVERY (map (fn set_map => HEADGOAL (rtac ctxt rel_funI) THEN |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58446
diff
changeset
|
359 |
REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) :: |
58106 | 360 |
@{thms exE conjE CollectE}))) THEN |
60728 | 361 |
HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN' |
362 |
rtac ctxt @{thm rel_setI}) THEN |
|
60752 | 363 |
REPEAT (HEADGOAL (etac ctxt imageE THEN' dtac ctxt @{thm set_mp} THEN' assume_tac ctxt THEN' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58446
diff
changeset
|
364 |
REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN' |
60728 | 365 |
rtac ctxt bexI THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt imageI))) set_maps); |
58106 | 366 |
|
61242 | 367 |
fun mk_rel_cong_tac ctxt (eqs, prems) mono = |
368 |
let |
|
369 |
fun mk_tac thm = etac ctxt thm THEN_ALL_NEW assume_tac ctxt; |
|
62324 | 370 |
fun mk_tacs iffD = etac ctxt mono :: |
61242 | 371 |
map (fn thm => (unfold_thms ctxt @{thms simp_implies_def} thm RS iffD) |
372 |
|> Drule.rotate_prems ~1 |> mk_tac) prems; |
|
373 |
in |
|
374 |
unfold_thms_tac ctxt eqs THEN |
|
375 |
HEADGOAL (EVERY' (rtac ctxt iffI :: mk_tacs iffD1 @ mk_tacs iffD2)) |
|
376 |
end; |
|
377 |
||
62324 | 378 |
fun subst_conv ctxt thm = |
379 |
Conv.arg_conv (Conv.arg_conv |
|
380 |
(Conv.top_sweep_conv (K (Conv.rewr_conv (safe_mk_meta_eq thm))) ctxt)); |
|
381 |
||
382 |
fun mk_rel_eq_onp_tac ctxt pred_def map_id0 rel_Grp = |
|
383 |
HEADGOAL (EVERY' |
|
384 |
[SELECT_GOAL (unfold_thms_tac ctxt (pred_def :: @{thms UNIV_def eq_onp_Grp Ball_Collect})), |
|
385 |
CONVERSION (subst_conv ctxt (map_id0 RS sym)), |
|
386 |
rtac ctxt (unfold_thms ctxt @{thms UNIV_def} rel_Grp)]); |
|
387 |
||
388 |
fun mk_pred_mono_strong0_tac ctxt pred_rel rel_mono_strong0 = |
|
389 |
unfold_thms_tac ctxt [pred_rel] THEN |
|
390 |
HEADGOAL (etac ctxt rel_mono_strong0 THEN_ALL_NEW etac ctxt @{thm eq_onp_mono0}); |
|
391 |
||
62329 | 392 |
fun mk_pred_transfer_tac ctxt n in_rel pred_map pred_cong = |
393 |
HEADGOAL (EVERY' [REPEAT_DETERM_N (n + 1) o rtac ctxt rel_funI, dtac ctxt (in_rel RS iffD1), |
|
394 |
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], hyp_subst_tac ctxt, |
|
395 |
rtac ctxt (box_equals OF [@{thm _}, pred_map RS sym, pred_map RS sym]), |
|
396 |
rtac ctxt (refl RS pred_cong), REPEAT_DETERM_N n o |
|
397 |
(etac ctxt @{thm rel_fun_Collect_case_prodD[where B="op ="]} THEN_ALL_NEW assume_tac ctxt)]); |
|
398 |
||
49284 | 399 |
end; |