author | traytel |
Sun, 28 Jul 2013 12:59:59 +0200 | |
changeset 52749 | ed416f4ac34e |
parent 52731 | dacd47a0633f |
child 52813 | 963297a24206 |
permissions | -rw-r--r-- |
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49506
diff
changeset
|
1 |
(* Title: HOL/BNF/Tools/bnf_def_tactics.ML |
49284 | 2 |
Author: Dmitriy Traytel, TU Muenchen |
3 |
Author: Jasmin Blanchette, TU Muenchen |
|
4 |
Copyright 2012 |
|
5 |
||
6 |
Tactics for definition of bounded natural functors. |
|
7 |
*) |
|
8 |
||
9 |
signature BNF_DEF_TACTICS = |
|
10 |
sig |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
11 |
val mk_collect_set_map_tac: thm list -> tactic |
51762 | 12 |
val mk_map_id': thm -> thm |
13 |
val mk_map_comp': thm -> thm |
|
51798 | 14 |
val mk_map_cong_tac: Proof.context -> thm -> tactic |
49284 | 15 |
val mk_in_mono_tac: int -> tactic |
16 |
val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
17 |
val mk_set_map': thm -> thm |
49284 | 18 |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
19 |
val mk_rel_Grp_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> |
49284 | 20 |
{prems: thm list, context: Proof.context} -> tactic |
51894 | 21 |
val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
22 |
val mk_rel_OO_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> |
49284 | 23 |
{prems: thm list, context: Proof.context} -> tactic |
51915 | 24 |
val mk_in_rel_tac: thm -> {prems: 'a, context: Proof.context} -> tactic |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
25 |
val mk_rel_conversep_tac: thm -> thm -> tactic |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
26 |
val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list -> |
49284 | 27 |
{prems: thm list, context: Proof.context} -> tactic |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
28 |
val mk_rel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic |
51916 | 29 |
val mk_rel_mono_strong_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> 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
|
30 |
|
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
31 |
val mk_map_transfer_tac: thm -> thm -> thm list -> thm -> thm -> |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
32 |
{prems: thm list, context: Proof.context} -> tactic |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
33 |
|
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 |
val mk_in_bd_tac: int -> thm -> thm -> thm -> thm list -> thm list -> thm -> thm -> thm -> thm -> |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
35 |
{prems: 'a, context: Proof.context} -> tactic |
49284 | 36 |
end; |
37 |
||
38 |
structure BNF_Def_Tactics : BNF_DEF_TACTICS = |
|
39 |
struct |
|
40 |
||
41 |
open BNF_Util |
|
42 |
open BNF_Tactics |
|
43 |
||
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
44 |
val ord_eq_le_trans = @{thm ord_eq_le_trans}; |
52749 | 45 |
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
|
46 |
|
51762 | 47 |
fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply}; |
48 |
fun mk_map_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp]; |
|
51798 | 49 |
fun mk_map_cong_tac ctxt cong0 = |
50 |
(hyp_subst_tac ctxt THEN' rtac cong0 THEN' |
|
51762 | 51 |
REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1; |
52659
58b87aa4dc3b
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents:
52635
diff
changeset
|
52 |
fun mk_set_map' set_map = set_map RS @{thm comp_eq_dest}; |
49490 | 53 |
fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1 |
49284 | 54 |
else (rtac subsetI THEN' |
55 |
rtac CollectI) 1 THEN |
|
56 |
REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN |
|
57 |
REPEAT_DETERM_N (n - 1) |
|
58 |
((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN |
|
59 |
(etac subset_trans THEN' atac) 1; |
|
60 |
||
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
61 |
fun mk_collect_set_map_tac set_maps = |
49623 | 62 |
(rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN' |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
63 |
EVERY' (map (fn set_map => |
49623 | 64 |
rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN' |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
65 |
rtac set_map) set_maps) THEN' |
49623 | 66 |
rtac @{thm image_empty}) 1; |
49284 | 67 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
68 |
fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_maps = |
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
69 |
if null set_maps then |
49284 | 70 |
EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1 |
71 |
else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, |
|
72 |
REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull, |
|
73 |
REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI, |
|
74 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, 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
|
75 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
49284 | 76 |
rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
77 |
set_maps, |
49284 | 78 |
CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans), |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
79 |
rtac (map_comp RS trans RS sym), rtac map_cong0, |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
80 |
REPEAT_DETERM_N (length set_maps) o EVERY' [rtac (o_apply RS trans), |
49284 | 81 |
rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm, |
82 |
rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1; |
|
83 |
||
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
84 |
fun mk_rel_Grp_tac rel_OO_Grps map_id map_cong0 map_id' map_comp set_maps |
49284 | 85 |
{context = ctxt, prems = _} = |
86 |
let |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
87 |
val n = length set_maps; |
49284 | 88 |
in |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
89 |
if null set_maps then |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
90 |
unfold_thms_tac ctxt ((map_id RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
91 |
rtac @{thm Grp_UNIV_idI[OF refl]} 1 |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
92 |
else unfold_thms_tac ctxt rel_OO_Grps THEN |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
93 |
EVERY' [rtac @{thm antisym}, rtac @{thm predicate2I}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
94 |
REPEAT_DETERM o |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
95 |
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
|
96 |
hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
97 |
REPEAT_DETERM_N n o EVERY' [rtac @{thm Collect_split_Grp_eqD}, etac @{thm set_mp}, atac], |
49284 | 98 |
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
|
99 |
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
|
100 |
rtac @{thm image_subsetI}, rtac @{thm Collect_split_Grp_inD}, etac @{thm set_mp}, atac]) |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
101 |
set_maps, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
102 |
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
|
103 |
hyp_subst_tac ctxt, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
104 |
rtac @{thm relcomppI}, rtac @{thm conversepI}, |
49495 | 105 |
EVERY' (map2 (fn convol => fn map_id => |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
106 |
EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]), |
49495 | 107 |
REPEAT_DETERM_N n o rtac (convol RS fun_cong), |
108 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
|
109 |
rtac CollectI, |
|
110 |
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
|
111 |
EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI}, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
112 |
rtac @{thm convol_mem_GrpI[OF refl]}, etac set_mp, atac]) |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
113 |
set_maps]) |
49495 | 114 |
@{thms fst_convol snd_convol} [map_id', refl])] 1 |
49284 | 115 |
end; |
116 |
||
51894 | 117 |
fun mk_rel_eq_tac n rel_Grp rel_cong map_id = |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
118 |
(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
|
119 |
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
|
120 |
(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
|
121 |
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
|
122 |
rtac @{thm equalityI}, rtac subset_UNIV, rtac subsetI, rtac CollectI, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
123 |
CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id])) 1; |
49284 | 124 |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
125 |
fun mk_rel_mono_tac rel_OO_Grps in_mono {context = ctxt, prems = _} = |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
126 |
unfold_thms_tac ctxt rel_OO_Grps THEN |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
127 |
EVERY' [rtac @{thm relcompp_mono}, rtac @{thm iffD2[OF conversep_mono]}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
128 |
rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
129 |
rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1; |
49284 | 130 |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
131 |
fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps |
49284 | 132 |
{context = ctxt, prems = _} = |
133 |
let |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
134 |
val n = length set_maps; |
49284 | 135 |
in |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
136 |
if null set_maps then rtac (rel_eq RS @{thm leq_conversepI}) 1 |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
137 |
else unfold_thms_tac ctxt (rel_OO_Grps) THEN |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
138 |
EVERY' [rtac @{thm predicate2I}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
139 |
REPEAT_DETERM o |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
140 |
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
|
141 |
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
|
142 |
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
|
143 |
rtac map_cong0, REPEAT_DETERM_N n o rtac thm, |
49284 | 144 |
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
|
145 |
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
|
146 |
etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 |
49284 | 147 |
end; |
148 |
||
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
149 |
fun mk_rel_conversep_tac le_conversep rel_mono = |
52749 | 150 |
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
|
151 |
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
|
152 |
REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1; |
49284 | 153 |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
154 |
fun mk_rel_OO_tac rel_OO_Grs rel_eq map_cong0 map_wppull map_comp set_maps |
49284 | 155 |
{context = ctxt, prems = _} = |
156 |
let |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
157 |
val n = length set_maps; |
49284 | 158 |
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
|
159 |
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51762
diff
changeset
|
160 |
rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps; |
49284 | 161 |
in |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
162 |
if null set_maps then rtac (rel_eq RS @{thm eq_OOI}) 1 |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
163 |
else unfold_thms_tac ctxt rel_OO_Grs THEN |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
164 |
EVERY' [rtac @{thm antisym}, rtac @{thm predicate2I}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
165 |
REPEAT_DETERM o |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
166 |
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
|
167 |
hyp_subst_tac ctxt, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
168 |
rtac @{thm relcomppI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
169 |
rtac trans, rtac map_comp, rtac sym, rtac map_cong0, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
170 |
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
|
171 |
in_tac @{thm fstOp_in}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
172 |
rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
173 |
REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
174 |
rtac ballE, rtac subst, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
175 |
rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE, |
49284 | 176 |
etac set_mp, atac], |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
177 |
in_tac @{thm fstOp_in}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
178 |
rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
179 |
rtac trans, rtac map_comp, rtac map_cong0, |
49284 | 180 |
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
|
181 |
in_tac @{thm sndOp_in}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
182 |
rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac sym, rtac map_cong0, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
183 |
REPEAT_DETERM_N n o rtac @{thm snd_sndOp}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
184 |
in_tac @{thm sndOp_in}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
185 |
rtac @{thm predicate2I}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
186 |
REPEAT_DETERM o eresolve_tac [@{thm relcomppE}, @{thm conversepE}, @{thm GrpE}], |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
187 |
hyp_subst_tac ctxt, |
49284 | 188 |
rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
189 |
CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_maps, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
190 |
etac allE, etac impE, etac conjI, etac conjI, etac sym, |
49284 | 191 |
REPEAT_DETERM o eresolve_tac [bexE, conjE], |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
192 |
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
|
193 |
EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49623
diff
changeset
|
194 |
rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
195 |
rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1 |
49284 | 196 |
end; |
197 |
||
51915 | 198 |
fun mk_in_rel_tac rel_OO_Gr {context = ctxt, prems = _} = |
199 |
EVERY' [rtac (rel_OO_Gr RS fun_cong RS fun_cong RS trans), rtac iffI, |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
200 |
REPEAT_DETERM o eresolve_tac [@{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
|
201 |
hyp_subst_tac ctxt, rtac exI, rtac conjI, atac, rtac conjI, rtac refl, rtac refl, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51798
diff
changeset
|
202 |
REPEAT_DETERM o eresolve_tac [exE, conjE], 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
|
203 |
etac @{thm GrpI}, atac, etac @{thm GrpI}, atac] 1; |
49284 | 204 |
|
51916 | 205 |
fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} = |
206 |
if null set_maps then atac 1 |
|
207 |
else |
|
208 |
unfold_tac [in_rel] ctxt THEN |
|
209 |
REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN |
|
210 |
hyp_subst_tac ctxt 1 THEN |
|
211 |
unfold_tac set_maps ctxt THEN |
|
212 |
EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]}, |
|
213 |
CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1; |
|
214 |
||
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
215 |
fun mk_map_transfer_tac rel_mono in_rel set_map's map_cong0 map_comp' |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
216 |
{context = ctxt, prems = _} = |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
217 |
let |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
218 |
val n = length set_map's; |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
219 |
in |
52725 | 220 |
REPEAT_DETERM_N n (HEADGOAL (rtac @{thm fun_relI})) THEN |
52731 | 221 |
unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN |
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
222 |
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
|
223 |
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
|
224 |
REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt, |
52731 | 225 |
rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI, |
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
226 |
CONJ_WRAP' (fn thm => |
52731 | 227 |
etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]})) |
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
228 |
set_map's, |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
229 |
rtac conjI, |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
230 |
EVERY' (map (fn convol => |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
231 |
rtac (box_equals OF [map_cong0, map_comp' RS sym, map_comp' RS sym]) THEN' |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
232 |
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
|
233 |
end; |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52659
diff
changeset
|
234 |
|
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
235 |
fun mk_in_bd_tac live map_comp' map_id' map_cong0 set_map's set_bds |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
236 |
bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero {context = ctxt, prems = _} = |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
237 |
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
|
238 |
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
|
239 |
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
|
240 |
else |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
241 |
let |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
242 |
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
|
243 |
val inserts = |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
244 |
map (fn set_bd => |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
245 |
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
|
246 |
[set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]]) |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
247 |
set_bds; |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
248 |
in |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
249 |
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
|
250 |
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
|
251 |
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
|
252 |
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
|
253 |
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
|
254 |
else |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
255 |
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
|
256 |
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
|
257 |
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
|
258 |
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
|
259 |
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
|
260 |
rtac (if live = 1 then @{thm card_of_Card_order} else @{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
|
261 |
CONJ_WRAP_GEN' (rtac @{thm Cfinite_csum}) (K (rtac @{thm Cfinite_cone})) set_map's, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
262 |
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
|
263 |
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
|
264 |
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
|
265 |
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
|
266 |
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
|
267 |
(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
|
268 |
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
|
269 |
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
|
270 |
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
|
271 |
unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
272 |
EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac @{thm surj_imp_ordLeq}, rtac subsetI, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
273 |
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
|
274 |
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
|
275 |
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
|
276 |
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
|
277 |
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
|
278 |
CONJ_WRAP_GEN' (rtac @{thm SigmaI}) |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
279 |
(K (etac @{thm If_the_inv_into_in_Func} THEN' atac)) set_map's, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
280 |
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
|
281 |
rtac (Drule.rotate_prems 1 |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
282 |
((box_equals OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f}, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
283 |
map_comp' RS sym, map_id']) RSN (2, trans))), |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
284 |
REPEAT_DETERM_N (2 * live) o atac, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
285 |
REPEAT_DETERM_N live o rtac (@{thm prod.cases} RS trans), |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
286 |
rtac refl, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
287 |
rtac @{thm surj_imp_ordLeq}, rtac subsetI, rtac @{thm image_eqI}, 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
|
288 |
rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF sum_case_o_inj(1)]}, |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
289 |
map_comp' RS sym, map_id']), |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
290 |
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
|
291 |
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
|
292 |
rtac (thm RS ord_eq_le_trans) THEN' etac @{thm subset_trans[OF image_mono Un_upper1]}) |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
293 |
set_map's] 1 |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
51916
diff
changeset
|
294 |
end; |
51916 | 295 |
|
49284 | 296 |
end; |