author | wenzelm |
Sat, 18 Jul 2015 20:47:08 +0200 | |
changeset 60752 | b48830b670a1 |
parent 60728 | 26ffdb966759 |
child 60757 | c09598a97436 |
permissions | -rw-r--r-- |
55061 | 1 |
(* Title: HOL/Tools/BNF/bnf_lfp_tactics.ML |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Author: Andrei Popescu, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
|
58315 | 6 |
Tactics for the datatype construction. |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
signature BNF_LFP_TACTICS = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
sig |
60728 | 11 |
val mk_alg_min_alg_tac: Proof.context -> int -> thm -> thm list -> thm -> thm -> thm list list -> |
12 |
thm list -> thm list -> tactic |
|
51798 | 13 |
val mk_alg_not_empty_tac: Proof.context -> thm -> thm list -> thm list -> tactic |
55197 | 14 |
val mk_alg_select_tac: Proof.context -> thm -> tactic |
60728 | 15 |
val mk_alg_set_tac: Proof.context -> thm -> tactic |
16 |
val mk_bd_card_order_tac: Proof.context -> thm list -> tactic |
|
17 |
val mk_bd_limit_tac: Proof.context -> int -> thm -> tactic |
|
18 |
val mk_card_of_min_alg_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> tactic |
|
19 |
val mk_copy_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list list -> tactic |
|
51798 | 20 |
val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm -> |
21 |
thm list -> thm list -> thm list -> tactic |
|
55197 | 22 |
val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm -> |
23 |
thm list -> tactic |
|
60728 | 24 |
val mk_ctor_set_tac: Proof.context -> thm -> thm -> thm list -> tactic |
58444 | 25 |
val mk_ctor_rec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list -> |
26 |
thm list -> tactic |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
27 |
val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list -> |
51798 | 28 |
thm -> thm -> thm list -> thm list -> thm list list -> tactic |
60728 | 29 |
val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic |
56237 | 30 |
val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> thm -> thm -> |
55197 | 31 |
tactic |
60728 | 32 |
val mk_init_induct_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> tactic |
33 |
val mk_init_unique_mor_tac: Proof.context -> cterm list -> int -> thm -> thm -> thm list -> |
|
34 |
thm list -> thm list -> thm list -> thm list -> tactic |
|
35 |
val mk_fold_unique_mor_tac: Proof.context -> thm list -> thm list -> thm list -> thm -> thm -> |
|
36 |
thm -> tactic |
|
55197 | 37 |
val mk_fold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic |
60728 | 38 |
val mk_least_min_alg_tac: Proof.context -> thm -> thm -> tactic |
55197 | 39 |
val mk_le_rel_OO_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list -> |
40 |
thm list -> tactic |
|
60728 | 41 |
val mk_map_comp0_tac: Proof.context -> thm list -> thm list -> thm -> int -> tactic |
42 |
val mk_map_id0_tac: Proof.context -> thm list -> thm -> tactic |
|
43 |
val mk_map_tac: Proof.context -> int -> int -> thm -> thm -> thm -> tactic |
|
55197 | 44 |
val mk_ctor_map_unique_tac: Proof.context -> thm -> thm list -> tactic |
45 |
val mk_mcong_tac: Proof.context -> (int -> tactic) -> thm list list list -> thm list -> |
|
46 |
thm list -> tactic |
|
60728 | 47 |
val mk_min_algs_card_of_tac: Proof.context -> ctyp -> cterm -> int -> thm -> thm list -> |
48 |
thm list -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> tactic |
|
49 |
val mk_min_algs_least_tac: Proof.context -> ctyp -> cterm -> thm -> thm list -> thm list -> tactic |
|
51798 | 50 |
val mk_min_algs_mono_tac: Proof.context -> thm -> tactic |
60728 | 51 |
val mk_min_algs_tac: Proof.context -> thm -> thm list -> tactic |
56263 | 52 |
val mk_mor_Abs_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list -> thm list -> |
53 |
tactic |
|
56237 | 54 |
val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> thm list -> |
55 |
thm list list -> tactic |
|
60728 | 56 |
val mk_mor_UNIV_tac: Proof.context -> int -> thm list -> thm -> tactic |
57 |
val mk_mor_comp_tac: Proof.context -> thm -> thm list list -> thm list -> tactic |
|
58 |
val mk_mor_convol_tac: Proof.context -> 'a list -> thm -> tactic |
|
59 |
val mk_mor_elim_tac: Proof.context -> thm -> tactic |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
60 |
val mk_mor_incl_tac: Proof.context -> thm -> thm list -> tactic |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
61 |
val mk_mor_fold_tac: Proof.context -> ctyp -> cterm -> thm list -> thm -> thm -> tactic |
60728 | 62 |
val mk_mor_select_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> |
63 |
thm list list -> thm list -> tactic |
|
64 |
val mk_mor_str_tac: Proof.context -> 'a list -> thm -> tactic |
|
55197 | 65 |
val mk_rel_induct_tac: Proof.context -> thm list -> int -> thm -> int list -> thm list -> |
66 |
thm list -> tactic |
|
67 |
val mk_rec_tac: Proof.context -> thm list -> thm -> thm list -> tactic |
|
68 |
val mk_rec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic |
|
69 |
val mk_set_bd_tac: Proof.context -> int -> (int -> tactic) -> thm -> thm list list -> thm list -> |
|
70 |
int -> tactic |
|
71 |
val mk_set_nat_tac: Proof.context -> int -> (int -> tactic) -> thm list list -> thm list -> |
|
72 |
cterm list -> thm list -> int -> tactic |
|
60728 | 73 |
val mk_set_map0_tac: Proof.context -> thm -> tactic |
74 |
val mk_set_tac: Proof.context -> thm -> tactic |
|
51798 | 75 |
val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
76 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
77 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
78 |
structure BNF_LFP_Tactics : BNF_LFP_TACTICS = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
struct |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
80 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
81 |
open BNF_Tactics |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
open BNF_LFP_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
83 |
open BNF_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
84 |
|
49306 | 85 |
val fst_snd_convs = @{thms fst_conv snd_conv}; |
86 |
val ord_eq_le_trans = @{thm ord_eq_le_trans}; |
|
87 |
val subset_trans = @{thm subset_trans}; |
|
88 |
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]}; |
|
52659
58b87aa4dc3b
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents:
52635
diff
changeset
|
89 |
val rev_bspec = Drule.rotate_prems 1 bspec; |
56114 | 90 |
val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]}; |
91 |
val relChainD = @{thm iffD2[OF meta_eq_to_obj_eq[OF relChain_def]]}; |
|
49306 | 92 |
|
60728 | 93 |
fun mk_alg_set_tac ctxt alg_def = |
94 |
EVERY' [dtac ctxt (alg_def RS iffD1), REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, rtac ctxt CollectI, |
|
60752 | 95 |
REPEAT_DETERM o (rtac ctxt (subset_UNIV RS conjI) ORELSE' etac ctxt conjI), assume_tac ctxt] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
96 |
|
51798 | 97 |
fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits = |
60728 | 98 |
(EVERY' [rtac ctxt notI, hyp_subst_tac ctxt, forward_tac ctxt [alg_set]] THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
99 |
REPEAT_DETERM o FIRST' |
60728 | 100 |
[EVERY' [rtac ctxt @{thm subset_emptyI}, eresolve_tac ctxt wits], |
101 |
EVERY' [rtac ctxt subsetI, rtac ctxt FalseE, eresolve_tac ctxt wits], |
|
102 |
EVERY' [rtac ctxt subsetI, dresolve_tac ctxt wits, hyp_subst_tac ctxt, |
|
60752 | 103 |
FIRST' (map (fn thm => rtac ctxt thm THEN' assume_tac ctxt) alg_sets)]] THEN' |
60728 | 104 |
etac ctxt @{thm emptyE}) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
105 |
|
60728 | 106 |
fun mk_mor_elim_tac ctxt mor_def = |
107 |
(dtac ctxt (mor_def RS iffD1) THEN' |
|
108 |
REPEAT o etac ctxt conjE THEN' |
|
109 |
TRY o rtac ctxt @{thm image_subsetI} THEN' |
|
110 |
etac ctxt bspec THEN' |
|
60752 | 111 |
assume_tac ctxt) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
112 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
113 |
fun mk_mor_incl_tac ctxt mor_def map_ids = |
60728 | 114 |
(rtac ctxt (mor_def RS iffD2) THEN' |
115 |
rtac ctxt conjI THEN' |
|
116 |
CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})])) |
|
56114 | 117 |
map_ids THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
118 |
CONJ_WRAP' (fn thm => |
60728 | 119 |
(EVERY' [rtac ctxt ballI, rtac ctxt trans, rtac ctxt id_apply, stac ctxt thm, rtac ctxt refl])) map_ids) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
120 |
|
60728 | 121 |
fun mk_mor_comp_tac ctxt mor_def set_maps map_comp_ids = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
122 |
let |
56114 | 123 |
val fbetw_tac = |
60752 | 124 |
EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}), |
125 |
etac ctxt bspec, etac ctxt bspec, assume_tac ctxt]; |
|
53290 | 126 |
fun mor_tac (set_map, map_comp_id) = |
60728 | 127 |
EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt trans, |
60752 | 128 |
rtac ctxt trans, dtac ctxt rev_bspec, assume_tac ctxt, etac ctxt arg_cong, |
60728 | 129 |
REPEAT o eresolve0_tac [CollectE, conjE], etac ctxt bspec, rtac ctxt CollectI] THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
130 |
CONJ_WRAP' (fn thm => |
60728 | 131 |
FIRST' [rtac ctxt subset_UNIV, |
132 |
(EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI}, |
|
60752 | 133 |
etac ctxt bspec, etac ctxt set_mp, assume_tac ctxt])]) set_map THEN' |
60728 | 134 |
rtac ctxt (map_comp_id RS arg_cong); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
135 |
in |
60728 | 136 |
(dtac ctxt (mor_def RS iffD1) THEN' dtac ctxt (mor_def RS iffD1) THEN' rtac ctxt (mor_def RS iffD2) THEN' |
137 |
REPEAT o etac ctxt conjE THEN' |
|
138 |
rtac ctxt conjI THEN' |
|
53290 | 139 |
CONJ_WRAP' (K fbetw_tac) set_maps THEN' |
140 |
CONJ_WRAP' mor_tac (set_maps ~~ map_comp_ids)) 1 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
141 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
142 |
|
60728 | 143 |
fun mk_mor_str_tac ctxt ks mor_def = |
144 |
(rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN' |
|
145 |
CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt UNIV_I])) ks THEN' |
|
146 |
CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt refl])) ks) 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
147 |
|
60728 | 148 |
fun mk_mor_convol_tac ctxt ks mor_def = |
149 |
(rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN' |
|
150 |
CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt UNIV_I])) ks THEN' |
|
151 |
CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt trans, rtac ctxt @{thm fst_convol'}, rtac ctxt o_apply])) ks) 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
152 |
|
60728 | 153 |
fun mk_mor_UNIV_tac ctxt m morEs mor_def = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
154 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
155 |
val n = length morEs; |
60728 | 156 |
fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE, |
157 |
rtac ctxt CollectI, CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto m + n), |
|
158 |
rtac ctxt sym, rtac ctxt o_apply]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
159 |
in |
60728 | 160 |
EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs, |
161 |
rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) morEs, |
|
162 |
REPEAT_DETERM o etac ctxt conjE, REPEAT_DETERM_N n o dtac ctxt (@{thm fun_eq_iff} RS iffD1), |
|
163 |
CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE, rtac ctxt trans, |
|
164 |
etac ctxt (o_apply RS sym RS trans), rtac ctxt o_apply])) morEs] 1 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
165 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
166 |
|
60728 | 167 |
fun mk_copy_tac ctxt m alg_def mor_def alg_sets set_mapss = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
168 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
169 |
val n = length alg_sets; |
56237 | 170 |
fun set_tac thm = |
60728 | 171 |
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans, etac ctxt @{thm image_mono}, |
172 |
rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE}]; |
|
56237 | 173 |
val alg_tac = |
174 |
CONJ_WRAP' (fn (set_maps, alg_set) => |
|
60728 | 175 |
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt set_mp, |
176 |
rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE[OF bij_betw_the_inv_into]}, |
|
177 |
rtac ctxt imageI, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))]) |
|
56237 | 178 |
(set_mapss ~~ alg_sets); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
179 |
|
60728 | 180 |
val mor_tac = rtac ctxt conjI THEN' CONJ_WRAP' (K (etac ctxt @{thm bij_betwE})) alg_sets THEN' |
56237 | 181 |
CONJ_WRAP' (fn (set_maps, alg_set) => |
60728 | 182 |
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE], |
183 |
etac ctxt @{thm f_the_inv_into_f_bij_betw}, etac ctxt alg_set, |
|
56237 | 184 |
EVERY' (map set_tac (drop m set_maps))]) |
185 |
(set_mapss ~~ alg_sets); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
186 |
in |
60728 | 187 |
(REPEAT_DETERM_N n o rtac ctxt exI THEN' rtac ctxt conjI THEN' |
188 |
rtac ctxt (alg_def RS iffD2) THEN' alg_tac THEN' rtac ctxt (mor_def RS iffD2) THEN' mor_tac) 1 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
189 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
190 |
|
60728 | 191 |
fun mk_bd_limit_tac ctxt n bd_Cinfinite = |
192 |
EVERY' [REPEAT_DETERM o etac ctxt conjE, rtac ctxt rev_mp, rtac ctxt @{thm Cinfinite_limit_finite}, |
|
193 |
REPEAT_DETERM_N n o rtac ctxt @{thm finite.insertI}, rtac ctxt @{thm finite.emptyI}, |
|
194 |
REPEAT_DETERM_N n o etac ctxt @{thm insert_subsetI}, rtac ctxt @{thm empty_subsetI}, |
|
195 |
rtac ctxt bd_Cinfinite, rtac ctxt impI, etac ctxt bexE, rtac ctxt bexI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
196 |
CONJ_WRAP' (fn i => |
60728 | 197 |
EVERY' [etac ctxt bspec, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1}]) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
198 |
(0 upto n - 1), |
60752 | 199 |
assume_tac ctxt] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
200 |
|
60728 | 201 |
fun mk_min_algs_tac ctxt worel in_congs = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
202 |
let |
60752 | 203 |
val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt bspec, |
204 |
assume_tac ctxt, etac ctxt arg_cong]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
205 |
fun minH_tac thm = |
60728 | 206 |
EVERY' [rtac ctxt Un_cong, minG_tac, rtac ctxt @{thm image_cong}, rtac ctxt thm, |
207 |
REPEAT_DETERM_N (length in_congs) o minG_tac, rtac ctxt refl]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
208 |
in |
60728 | 209 |
(rtac ctxt (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ctxt iffD2 THEN' |
210 |
rtac ctxt meta_eq_to_obj_eq THEN' rtac ctxt (worel RS @{thm wo_rel.adm_wo_def}) THEN' |
|
211 |
REPEAT_DETERM_N 3 o rtac ctxt allI THEN' rtac ctxt impI THEN' |
|
212 |
CONJ_WRAP_GEN' (EVERY' [rtac ctxt prod_injectI, rtac ctxt conjI]) minH_tac in_congs) 1 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
213 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
214 |
|
60728 | 215 |
fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac ctxt relChainD, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, |
216 |
rtac ctxt @{thm case_split}, rtac ctxt @{thm xt1(3)}, rtac ctxt min_algs, etac ctxt @{thm FieldI2}, rtac ctxt subsetI, |
|
60752 | 217 |
rtac ctxt UnI1, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, assume_tac ctxt, |
218 |
assume_tac ctxt, rtac ctxt equalityD1, dtac ctxt @{thm notnotD}, |
|
219 |
hyp_subst_tac ctxt, rtac ctxt refl] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
220 |
|
60728 | 221 |
fun mk_min_algs_card_of_tac ctxt cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero |
51812 | 222 |
suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
223 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
224 |
val induct = worel RS |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
225 |
Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
226 |
val src = 1 upto m + 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
227 |
val dest = (m + 1) :: (1 upto m); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
228 |
val absorbAs_tac = if m = 0 then K (all_tac) |
60728 | 229 |
else EVERY' [rtac ctxt @{thm ordIso_transitive}, rtac ctxt @{thm csum_cong1}, |
230 |
rtac ctxt @{thm ordIso_transitive}, |
|
231 |
BNF_Tactics.mk_rotate_eq_tac ctxt (rtac ctxt @{thm ordIso_refl} THEN' |
|
232 |
FIRST' [rtac ctxt @{thm card_of_Card_order}, rtac ctxt @{thm Card_order_csum}, |
|
233 |
rtac ctxt @{thm Card_order_cexp}]) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
234 |
@{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
235 |
src dest, |
60728 | 236 |
rtac ctxt @{thm csum_absorb1}, rtac ctxt Asuc_Cinfinite, rtac ctxt ctrans, rtac ctxt @{thm ordLeq_csum1}, |
237 |
FIRST' [rtac ctxt @{thm Card_order_csum}, rtac ctxt @{thm card_of_Card_order}], |
|
238 |
rtac ctxt @{thm ordLeq_cexp1}, rtac ctxt suc_Cnotzero, rtac ctxt @{thm Card_order_csum}]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
239 |
|
60728 | 240 |
val minG_tac = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordLess_imp_ordLeq}, |
241 |
rtac ctxt @{thm ordLess_transitive}, rtac ctxt @{thm card_of_underS}, rtac ctxt suc_Card_order, |
|
60752 | 242 |
assume_tac ctxt, rtac ctxt suc_Asuc, rtac ctxt ballI, etac ctxt allE, |
243 |
dtac ctxt mp, etac ctxt @{thm underS_E}, |
|
244 |
dtac ctxt mp, etac ctxt @{thm underS_Field}, |
|
245 |
REPEAT o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite] |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
246 |
|
60728 | 247 |
fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, |
248 |
rtac ctxt @{thm card_of_ordIso_subst}, etac ctxt min_alg, rtac ctxt @{thm Un_Cinfinite_bound}, |
|
249 |
minG_tac, rtac ctxt ctrans, rtac ctxt @{thm card_of_image}, rtac ctxt ctrans, rtac ctxt in_bd, rtac ctxt ctrans, |
|
250 |
rtac ctxt @{thm cexp_mono1}, rtac ctxt @{thm csum_mono1}, |
|
251 |
REPEAT_DETERM_N m o rtac ctxt @{thm csum_mono2}, |
|
252 |
CONJ_WRAP_GEN' (rtac ctxt @{thm csum_cinfinite_bound}) (K minG_tac) min_algs, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
253 |
REPEAT_DETERM o FIRST' |
60728 | 254 |
[rtac ctxt @{thm card_of_Card_order}, rtac ctxt @{thm Card_order_csum}, |
255 |
rtac ctxt Asuc_Cinfinite, rtac ctxt bd_Card_order], |
|
256 |
rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm cexp_cong1}, absorbAs_tac, |
|
257 |
rtac ctxt @{thm csum_absorb1}, rtac ctxt Asuc_Cinfinite, rtac ctxt @{thm ctwo_ordLeq_Cinfinite}, |
|
258 |
rtac ctxt Asuc_Cinfinite, rtac ctxt bd_Card_order, |
|
259 |
rtac ctxt @{thm ordIso_imp_ordLeq}, rtac ctxt @{thm cexp_cprod_ordLeq}, |
|
260 |
resolve0_tac @{thms Card_order_csum Card_order_ctwo}, rtac ctxt suc_Cinfinite, |
|
261 |
rtac ctxt bd_Cnotzero, rtac ctxt @{thm cardSuc_ordLeq}, rtac ctxt bd_Card_order, rtac ctxt Asuc_Cinfinite]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
262 |
in |
60728 | 263 |
(rtac ctxt induct THEN' |
264 |
rtac ctxt impI THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
265 |
CONJ_WRAP' mk_minH_tac (min_algs ~~ in_bds)) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
266 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
267 |
|
60728 | 268 |
fun mk_min_algs_least_tac ctxt cT ct worel min_algs alg_sets = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
269 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
270 |
val induct = worel RS |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
271 |
Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
272 |
|
60752 | 273 |
val minG_tac = |
274 |
EVERY' [rtac ctxt @{thm UN_least}, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E}, |
|
275 |
dtac ctxt mp, etac ctxt @{thm underS_Field}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
276 |
|
60728 | 277 |
fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ctxt ord_eq_le_trans, etac ctxt min_alg, |
278 |
rtac ctxt @{thm Un_least}, minG_tac, rtac ctxt @{thm image_subsetI}, |
|
279 |
REPEAT_DETERM o eresolve0_tac [CollectE, conjE], etac ctxt alg_set, |
|
280 |
REPEAT_DETERM o (etac ctxt subset_trans THEN' minG_tac)]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
281 |
in |
60728 | 282 |
(rtac ctxt induct THEN' |
283 |
rtac ctxt impI THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
284 |
CONJ_WRAP' mk_minH_tac (min_algs ~~ alg_sets)) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
285 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
286 |
|
60728 | 287 |
fun mk_alg_min_alg_tac ctxt m alg_def min_alg_defs bd_limit bd_Cinfinite |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
288 |
set_bdss min_algs min_alg_monos = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
289 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
290 |
val n = length min_algs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
291 |
fun mk_cardSuc_UNION_tac set_bds (mono, def) = EVERY' |
60728 | 292 |
[rtac ctxt bexE, rtac ctxt @{thm cardSuc_UNION_Cinfinite}, rtac ctxt bd_Cinfinite, rtac ctxt mono, |
293 |
etac ctxt (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve0_tac set_bds]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
294 |
fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) = |
60728 | 295 |
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE], |
296 |
EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt bexE, |
|
60752 | 297 |
rtac ctxt bd_limit, REPEAT_DETERM_N (n - 1) o etac ctxt conjI, assume_tac ctxt, |
60728 | 298 |
rtac ctxt (min_alg_def RS @{thm set_mp[OF equalityD2]}), |
60752 | 299 |
rtac ctxt @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac ctxt thin_rl, |
300 |
assume_tac ctxt, rtac ctxt set_mp, |
|
301 |
rtac ctxt equalityD2, rtac ctxt min_alg, assume_tac ctxt, rtac ctxt UnI2, |
|
302 |
rtac ctxt @{thm image_eqI}, rtac ctxt refl, |
|
60728 | 303 |
rtac ctxt CollectI, REPEAT_DETERM_N m o dtac ctxt asm_rl, REPEAT_DETERM_N n o etac ctxt thin_rl, |
304 |
REPEAT_DETERM o etac ctxt conjE, |
|
60752 | 305 |
CONJ_WRAP' (K (FIRST' [assume_tac ctxt, |
60728 | 306 |
EVERY' [etac ctxt subset_trans, rtac ctxt subsetI, rtac ctxt @{thm UN_I}, |
60752 | 307 |
etac ctxt @{thm underS_I}, assume_tac ctxt, assume_tac ctxt]])) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
308 |
set_bds]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
309 |
in |
60728 | 310 |
(rtac ctxt (alg_def RS iffD2) THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
311 |
CONJ_WRAP' mk_conjunct_tac (set_bdss ~~ (min_algs ~~ min_alg_defs))) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
312 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
313 |
|
60728 | 314 |
fun mk_card_of_min_alg_tac ctxt min_alg_def card_of suc_Card_order suc_Asuc Asuc_Cinfinite = |
315 |
EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt (min_alg_def RS @{thm card_of_ordIso_subst}), |
|
316 |
rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordIso_ordLeq_trans}, |
|
317 |
rtac ctxt @{thm card_of_Field_ordIso}, rtac ctxt suc_Card_order, rtac ctxt @{thm ordLess_imp_ordLeq}, |
|
60752 | 318 |
rtac ctxt suc_Asuc, rtac ctxt ballI, dtac ctxt rev_mp, rtac ctxt card_of, |
319 |
REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
320 |
|
60728 | 321 |
fun mk_least_min_alg_tac ctxt min_alg_def least = |
60752 | 322 |
EVERY' [rtac ctxt (min_alg_def RS ord_eq_le_trans), rtac ctxt @{thm UN_least}, |
323 |
dtac ctxt least, dtac ctxt mp, assume_tac ctxt, |
|
324 |
REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
325 |
|
55197 | 326 |
fun mk_alg_select_tac ctxt Abs_inverse = |
60728 | 327 |
EVERY' [rtac ctxt ballI, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
328 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN |
60752 | 329 |
unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN assume_tac ctxt 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
330 |
|
60728 | 331 |
fun mk_mor_select_tac ctxt mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets |
53290 | 332 |
set_maps str_init_defs = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
333 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
334 |
val n = length alg_sets; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
335 |
val fbetw_tac = |
60752 | 336 |
CONJ_WRAP' |
337 |
(K (EVERY' [rtac ctxt ballI, etac ctxt rev_bspec, |
|
338 |
etac ctxt CollectE, assume_tac ctxt])) alg_sets; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
339 |
val mor_tac = |
60728 | 340 |
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs; |
53290 | 341 |
fun alg_epi_tac ((alg_set, str_init_def), set_map) = |
60728 | 342 |
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt CollectI, |
343 |
rtac ctxt ballI, ftac ctxt (alg_select RS bspec), rtac ctxt (str_init_def RS @{thm ssubst_mem}), |
|
344 |
etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve0_tac set_map, |
|
345 |
rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec, |
|
60752 | 346 |
assume_tac ctxt]]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
347 |
in |
60728 | 348 |
EVERY' [rtac ctxt mor_cong, REPEAT_DETERM_N n o (rtac ctxt sym THEN' rtac ctxt @{thm comp_id}), |
349 |
rtac ctxt (Thm.permute_prems 0 1 mor_comp), etac ctxt (Thm.permute_prems 0 1 mor_comp), |
|
350 |
rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, fbetw_tac, mor_tac, rtac ctxt mor_incl_min_alg, |
|
351 |
rtac ctxt (alg_def RS iffD2), CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)] 1 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
352 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
353 |
|
56237 | 354 |
fun mk_init_ex_mor_tac ctxt Abs_inverse copy card_of_min_algs mor_Rep mor_comp mor_select mor_incl = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
355 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
356 |
val n = length card_of_min_algs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
357 |
in |
56237 | 358 |
EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs), |
60752 | 359 |
REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp, rtac ctxt copy, |
360 |
REPEAT_DETERM_N n o assume_tac ctxt, |
|
60728 | 361 |
rtac ctxt impI, REPEAT_DETERM o eresolve0_tac [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI, |
362 |
rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, |
|
60752 | 363 |
rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt, |
56237 | 364 |
SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)), |
60728 | 365 |
etac ctxt mor_comp, rtac ctxt mor_incl, REPEAT_DETERM_N n o rtac ctxt subset_UNIV] 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
366 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
367 |
|
60728 | 368 |
fun mk_init_unique_mor_tac ctxt cts m |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
369 |
alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_cong0s = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
370 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
371 |
val n = length least_min_algs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
372 |
val ks = (1 upto n); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
373 |
|
60728 | 374 |
fun mor_tac morE in_mono = EVERY' [etac ctxt morE, rtac ctxt set_mp, rtac ctxt in_mono, |
375 |
REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt CollectI, |
|
60752 | 376 |
REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' assume_tac ctxt)]; |
56263 | 377 |
fun cong_tac ct map_cong0 = EVERY' |
60728 | 378 |
[rtac ctxt (map_cong0 RS cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong), |
379 |
REPEAT_DETERM_N m o rtac ctxt refl, |
|
60752 | 380 |
REPEAT_DETERM_N n o (etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
381 |
|
56263 | 382 |
fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) = |
60728 | 383 |
EVERY' [rtac ctxt ballI, rtac ctxt CollectI, |
384 |
REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set), |
|
385 |
REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}), |
|
386 |
rtac ctxt trans, mor_tac morE in_mono, |
|
387 |
rtac ctxt trans, cong_tac ct map_cong0, |
|
388 |
rtac ctxt sym, mor_tac morE in_mono]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
389 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
390 |
fun mk_unique_tac (k, least_min_alg) = |
60728 | 391 |
select_prem_tac ctxt n (etac ctxt @{thm prop_restrict}) k THEN' rtac ctxt least_min_alg THEN' |
392 |
rtac ctxt (alg_def RS iffD2) THEN' |
|
56263 | 393 |
CONJ_WRAP' mk_alg_tac (cts ~~ (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s)))); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
394 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
395 |
CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
396 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
397 |
|
60728 | 398 |
fun mk_init_induct_tac ctxt m alg_def alg_min_alg least_min_algs alg_sets = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
399 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
400 |
val n = length least_min_algs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
401 |
|
60728 | 402 |
fun mk_alg_tac alg_set = EVERY' [rtac ctxt ballI, rtac ctxt CollectI, |
403 |
REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set), |
|
404 |
REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}), |
|
405 |
rtac ctxt mp, etac ctxt bspec, rtac ctxt CollectI, |
|
60752 | 406 |
REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt), |
60728 | 407 |
CONJ_WRAP' (K (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict})) alg_sets, |
60752 | 408 |
CONJ_WRAP' (K (rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)) |
409 |
alg_sets]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
410 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
411 |
fun mk_induct_tac least_min_alg = |
60728 | 412 |
rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' rtac ctxt least_min_alg THEN' |
413 |
rtac ctxt (alg_def RS iffD2) THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
414 |
CONJ_WRAP' mk_alg_tac alg_sets; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
415 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
416 |
CONJ_WRAP' mk_induct_tac least_min_algs 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
417 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
418 |
|
56237 | 419 |
fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses alg_min_alg alg_sets set_mapss = |
420 |
unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN |
|
60728 | 421 |
EVERY' [rtac ctxt conjI, |
422 |
CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' rtac ctxt thm) Reps, |
|
56237 | 423 |
CONJ_WRAP' (fn (Abs_inverse, (set_maps, alg_set)) => |
60728 | 424 |
EVERY' [rtac ctxt ballI, rtac ctxt Abs_inverse, rtac ctxt (alg_min_alg RS alg_set), |
56237 | 425 |
EVERY' (map2 (fn Rep => fn set_map => |
60728 | 426 |
EVERY' [rtac ctxt (set_map RS ord_eq_le_trans), rtac ctxt @{thm image_subsetI}, rtac ctxt Rep]) |
56237 | 427 |
Reps (drop m set_maps))]) |
428 |
(Abs_inverses ~~ (set_mapss ~~ alg_sets))] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
429 |
|
56237 | 430 |
fun mk_mor_Abs_tac ctxt cts defs Abs_inverses map_comp_ids map_congLs = |
431 |
unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN |
|
60728 | 432 |
EVERY' [rtac ctxt conjI, |
433 |
CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses, |
|
56237 | 434 |
CONJ_WRAP' (fn (ct, thm) => |
60728 | 435 |
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], |
436 |
rtac ctxt (thm RS (cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong) RS sym), |
|
56237 | 437 |
EVERY' (map (fn Abs_inverse => |
60752 | 438 |
EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse), |
439 |
assume_tac ctxt]) |
|
56237 | 440 |
Abs_inverses)]) |
441 |
(cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
442 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
443 |
fun mk_mor_fold_tac ctxt cT ct fold_defs ex_mor mor = |
60728 | 444 |
(EVERY' (map (stac ctxt) fold_defs) THEN' EVERY' [rtac ctxt rev_mp, rtac ctxt ex_mor, rtac ctxt impI] THEN' |
445 |
REPEAT_DETERM_N (length fold_defs) o etac ctxt exE THEN' |
|
446 |
rtac ctxt (Drule.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac ctxt mor) 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
447 |
|
60728 | 448 |
fun mk_fold_unique_mor_tac ctxt type_defs init_unique_mors Reps mor_comp mor_Abs mor_fold = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
449 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
450 |
fun mk_unique type_def = |
60728 | 451 |
EVERY' [rtac ctxt @{thm surj_fun_eq}, rtac ctxt (type_def RS @{thm type_definition.Abs_image}), |
452 |
rtac ctxt ballI, resolve0_tac init_unique_mors, |
|
60752 | 453 |
EVERY' (map (fn thm => assume_tac ctxt ORELSE' rtac ctxt thm) Reps), |
454 |
rtac ctxt mor_comp, rtac ctxt mor_Abs, assume_tac ctxt, |
|
60728 | 455 |
rtac ctxt mor_comp, rtac ctxt mor_Abs, rtac ctxt mor_fold]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
456 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
457 |
CONJ_WRAP' mk_unique type_defs 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
458 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
459 |
|
60728 | 460 |
fun mk_dtor_o_ctor_tac ctxt dtor_def foldx map_comp_id map_cong0L ctor_o_folds = |
461 |
EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt (dtor_def RS fun_cong RS trans), |
|
462 |
rtac ctxt trans, rtac ctxt foldx, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L, |
|
463 |
EVERY' (map (fn thm => rtac ctxt ballI THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply])) |
|
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
464 |
ctor_o_folds), |
60728 | 465 |
rtac ctxt sym, rtac ctxt id_apply] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
466 |
|
55197 | 467 |
fun mk_rec_tac ctxt rec_defs foldx fst_recs = |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
468 |
unfold_thms_tac ctxt |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
469 |
(rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN |
60728 | 470 |
EVERY' [rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt (foldx RS @{thm arg_cong[of _ _ snd]}), |
471 |
rtac ctxt @{thm snd_convol'}] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
472 |
|
55197 | 473 |
fun mk_rec_unique_mor_tac ctxt rec_defs fst_recs fold_unique_mor = |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49585
diff
changeset
|
474 |
unfold_thms_tac ctxt |
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49585
diff
changeset
|
475 |
(rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN |
60728 | 476 |
etac ctxt fold_unique_mor 1; |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49585
diff
changeset
|
477 |
|
53290 | 478 |
fun mk_ctor_induct_tac ctxt m set_mapss init_induct morEs mor_Abs Rep_invs Abs_invs Reps = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
479 |
let |
53290 | 480 |
val n = length set_mapss; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
481 |
val ks = 1 upto n; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
482 |
|
53290 | 483 |
fun mk_IH_tac Rep_inv Abs_inv set_map = |
60728 | 484 |
DETERM o EVERY' [dtac ctxt meta_mp, rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt bspec, |
485 |
dtac ctxt set_rev_mp, rtac ctxt equalityD1, rtac ctxt set_map, etac ctxt imageE, |
|
60752 | 486 |
hyp_subst_tac ctxt, rtac ctxt (Abs_inv RS @{thm ssubst_mem}), etac ctxt set_mp, |
487 |
assume_tac ctxt, assume_tac ctxt]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
488 |
|
53290 | 489 |
fun mk_closed_tac (k, (morE, set_maps)) = |
60728 | 490 |
EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) k, rtac ctxt ballI, rtac ctxt impI, |
60752 | 491 |
rtac ctxt (mor_Abs RS morE RS arg_cong RS iffD2), assume_tac ctxt, |
60728 | 492 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], dtac ctxt @{thm meta_spec}, |
60752 | 493 |
EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), assume_tac ctxt]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
494 |
|
49227 | 495 |
fun mk_induct_tac (Rep, Rep_inv) = |
60728 | 496 |
EVERY' [rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt (Rep RSN (2, bspec))]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
497 |
in |
60728 | 498 |
(rtac ctxt mp THEN' rtac ctxt impI THEN' |
499 |
DETERM o CONJ_WRAP_GEN' (etac ctxt conjE THEN' rtac ctxt conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN' |
|
500 |
rtac ctxt init_induct THEN' |
|
53290 | 501 |
DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_mapss))) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
502 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
503 |
|
55197 | 504 |
fun mk_ctor_induct2_tac ctxt cTs cts ctor_induct weak_ctor_inducts = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
505 |
let |
49501 | 506 |
val n = length weak_ctor_inducts; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
507 |
val ks = 1 upto n; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
508 |
fun mk_inner_induct_tac induct i = |
60728 | 509 |
EVERY' [rtac ctxt allI, fo_rtac ctxt induct, |
510 |
select_prem_tac ctxt n (dtac ctxt @{thm meta_spec2}) i, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
511 |
REPEAT_DETERM_N n o |
60728 | 512 |
EVERY' [dtac ctxt meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt, |
60752 | 513 |
REPEAT_DETERM o dtac ctxt @{thm meta_spec}, etac ctxt (spec RS meta_mp), |
514 |
assume_tac ctxt], |
|
515 |
assume_tac ctxt]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
516 |
in |
60728 | 517 |
EVERY' [rtac ctxt rev_mp, rtac ctxt (Drule.instantiate' cTs cts ctor_induct), |
518 |
EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac ctxt impI, |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
519 |
REPEAT_DETERM o eresolve_tac ctxt [conjE, allE], |
60752 | 520 |
CONJ_WRAP' (K (assume_tac ctxt)) ks] 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
521 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
522 |
|
60728 | 523 |
fun mk_map_tac ctxt m n foldx map_comp_id map_cong0 = |
524 |
EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt foldx, rtac ctxt trans, |
|
525 |
rtac ctxt o_apply, |
|
526 |
rtac ctxt trans, rtac ctxt (map_comp_id RS arg_cong), rtac ctxt trans, rtac ctxt (map_cong0 RS arg_cong), |
|
527 |
REPEAT_DETERM_N m o rtac ctxt refl, |
|
528 |
REPEAT_DETERM_N n o (EVERY' (map (rtac ctxt) [trans, o_apply, id_apply])), |
|
529 |
rtac ctxt sym, rtac ctxt o_apply] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
530 |
|
55197 | 531 |
fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps = |
60728 | 532 |
rtac ctxt fold_unique 1 THEN |
55067 | 533 |
unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN |
60752 | 534 |
ALLGOALS (assume_tac ctxt); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
535 |
|
60728 | 536 |
fun mk_set_tac ctxt foldx = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, |
537 |
rtac ctxt trans, rtac ctxt foldx, rtac ctxt sym, rtac ctxt o_apply] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
538 |
|
60728 | 539 |
fun mk_ctor_set_tac ctxt set set_map set_maps = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
540 |
let |
53290 | 541 |
val n = length set_maps; |
60728 | 542 |
fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN' |
543 |
rtac ctxt @{thm Union_image_eq}; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
544 |
in |
60728 | 545 |
EVERY' [rtac ctxt (set RS @{thm comp_eq_dest} RS trans), rtac ctxt Un_cong, |
546 |
rtac ctxt (trans OF [set_map, trans_fun_cong_image_id_id_apply]), |
|
547 |
REPEAT_DETERM_N (n - 1) o rtac ctxt Un_cong, |
|
53290 | 548 |
EVERY' (map mk_UN set_maps)] 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
549 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
550 |
|
55197 | 551 |
fun mk_set_nat_tac ctxt m induct_tac set_mapss ctor_maps csets ctor_sets i = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
552 |
let |
49541 | 553 |
val n = length ctor_maps; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
554 |
|
60728 | 555 |
fun useIH set_nat = EVERY' [rtac ctxt trans, rtac ctxt @{thm image_UN}, rtac ctxt trans, rtac ctxt @{thm SUP_cong}, |
556 |
rtac ctxt refl, Goal.assume_rule_tac ctxt, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm SUP_cong}, |
|
557 |
rtac ctxt set_nat, rtac ctxt refl, rtac ctxt @{thm UN_simps(10)}]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
558 |
|
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49544
diff
changeset
|
559 |
fun mk_set_nat cset ctor_map ctor_set set_nats = |
60728 | 560 |
EVERY' [rtac ctxt trans, rtac ctxt @{thm image_cong}, rtac ctxt ctor_set, rtac ctxt refl, rtac ctxt sym, |
561 |
rtac ctxt (trans OF [ctor_map RS cterm_instantiate_pos [NONE, NONE, SOME cset] arg_cong, |
|
56262 | 562 |
ctor_set RS trans]), |
60728 | 563 |
rtac ctxt sym, EVERY' (map (rtac ctxt) [trans, @{thm image_Un}, Un_cong]), |
564 |
rtac ctxt sym, rtac ctxt (nth set_nats (i - 1)), |
|
565 |
REPEAT_DETERM_N (n - 1) o EVERY' (map (rtac ctxt) [trans, @{thm image_Un}, Un_cong]), |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
566 |
EVERY' (map useIH (drop m set_nats))]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
567 |
in |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58446
diff
changeset
|
568 |
(induct_tac THEN' EVERY' (@{map 4} mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
569 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
570 |
|
55197 | 571 |
fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
572 |
let |
49542
b39354db8629
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset
|
573 |
val n = length ctor_sets; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
574 |
|
60728 | 575 |
fun useIH set_bd = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt set_bd, rtac ctxt ballI, |
576 |
Goal.assume_rule_tac ctxt, rtac ctxt bd_Cinfinite]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
577 |
|
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49544
diff
changeset
|
578 |
fun mk_set_nat ctor_set set_bds = |
60728 | 579 |
EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm card_of_ordIso_subst}, rtac ctxt ctor_set, |
580 |
rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac ctxt (nth set_bds (i - 1)), |
|
581 |
REPEAT_DETERM_N (n - 1) o rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
582 |
EVERY' (map useIH (drop m set_bds))]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
583 |
in |
49542
b39354db8629
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset
|
584 |
(induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
585 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
586 |
|
55197 | 587 |
fun mk_mcong_tac ctxt induct_tac set_setsss map_cong0s ctor_maps = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
588 |
let |
60728 | 589 |
fun use_asm thm = EVERY' [etac ctxt bspec, etac ctxt set_rev_mp, rtac ctxt thm]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
590 |
|
60728 | 591 |
fun useIH set_sets = EVERY' [rtac ctxt mp, Goal.assume_rule_tac ctxt, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
592 |
CONJ_WRAP' (fn thm => |
60728 | 593 |
EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_rev_mp, etac ctxt thm]) set_sets]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
594 |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
595 |
fun mk_map_cong0 ctor_map map_cong0 set_setss = |
60728 | 596 |
EVERY' [rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE, |
597 |
rtac ctxt trans, rtac ctxt ctor_map, rtac ctxt trans, rtac ctxt (map_cong0 RS arg_cong), |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
598 |
EVERY' (map use_asm (map hd set_setss)), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
599 |
EVERY' (map useIH (transpose (map tl set_setss))), |
60728 | 600 |
rtac ctxt sym, rtac ctxt ctor_map]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
601 |
in |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58446
diff
changeset
|
602 |
(induct_tac THEN' EVERY' (@{map 3} mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
603 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
604 |
|
57967 | 605 |
fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs = |
60728 | 606 |
EVERY' (rtac ctxt induct :: |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58446
diff
changeset
|
607 |
@{map 4} (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO => |
60728 | 608 |
EVERY' [rtac ctxt impI, etac ctxt (nchotomy RS @{thm nchotomy_relcomppE}), |
609 |
REPEAT_DETERM_N 2 o dtac ctxt (Irel RS iffD1), rtac ctxt (Irel RS iffD2), |
|
610 |
rtac ctxt rel_mono, rtac ctxt (le_rel_OO RS @{thm predicate2D}), |
|
60752 | 611 |
rtac ctxt @{thm relcomppI}, assume_tac ctxt, assume_tac ctxt, |
612 |
REPEAT_DETERM_N m o EVERY' [rtac ctxt ballI, rtac ctxt ballI, rtac ctxt impI, assume_tac ctxt], |
|
57726 | 613 |
REPEAT_DETERM_N (length le_rel_OOs) o |
60728 | 614 |
EVERY' [rtac ctxt ballI, rtac ctxt ballI, Goal.assume_rule_tac ctxt]]) |
57967 | 615 |
ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
616 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
617 |
(* BNF tactics *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
618 |
|
60728 | 619 |
fun mk_map_id0_tac ctxt map_id0s unique = |
620 |
(rtac ctxt sym THEN' rtac ctxt unique THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
621 |
EVERY' (map (fn thm => |
60728 | 622 |
EVERY' [rtac ctxt trans, rtac ctxt @{thm id_comp}, rtac ctxt trans, rtac ctxt sym, rtac ctxt @{thm comp_id}, |
623 |
rtac ctxt (thm RS sym RS arg_cong)]) map_id0s)) 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
624 |
|
60728 | 625 |
fun mk_map_comp0_tac ctxt map_comp0s ctor_maps unique iplus1 = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
626 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
627 |
val i = iplus1 - 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
628 |
val unique' = Thm.permute_prems 0 i unique; |
53288 | 629 |
val map_comp0s' = drop i map_comp0s @ take i map_comp0s; |
49541 | 630 |
val ctor_maps' = drop i ctor_maps @ take i ctor_maps; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
631 |
fun mk_comp comp simp = |
60728 | 632 |
EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt o_apply, |
633 |
rtac ctxt trans, rtac ctxt (simp RS arg_cong), rtac ctxt trans, rtac ctxt simp, |
|
634 |
rtac ctxt trans, rtac ctxt (comp RS arg_cong), rtac ctxt sym, rtac ctxt o_apply]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
635 |
in |
60728 | 636 |
(rtac ctxt sym THEN' rtac ctxt unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
637 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
638 |
|
60728 | 639 |
fun mk_set_map0_tac ctxt set_nat = |
640 |
EVERY' (map (rtac ctxt) [@{thm ext}, trans, o_apply, sym, trans, o_apply, set_nat]) 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
641 |
|
60728 | 642 |
fun mk_bd_card_order_tac ctxt bd_card_orders = |
643 |
CONJ_WRAP_GEN' (rtac ctxt @{thm card_order_csum}) (rtac ctxt) bd_card_orders 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
644 |
|
51798 | 645 |
fun mk_wit_tac ctxt n ctor_set wit = |
60752 | 646 |
REPEAT_DETERM (assume_tac ctxt 1 ORELSE |
60728 | 647 |
EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
648 |
REPEAT_DETERM o |
60728 | 649 |
(TRY o REPEAT_DETERM o etac ctxt UnE THEN' TRY o etac ctxt @{thm UN_E} THEN' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
650 |
(eresolve_tac ctxt wit ORELSE' |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
651 |
(dresolve_tac ctxt wit THEN' |
60728 | 652 |
(etac ctxt FalseE ORELSE' |
653 |
EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set, |
|
654 |
REPEAT_DETERM_N n o etac ctxt UnE]))))] 1); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
655 |
|
53287 | 656 |
fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject |
53289 | 657 |
ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
658 |
let |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
659 |
val m = length ctor_set_incls; |
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
660 |
val n = length ctor_set_set_inclss; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
661 |
|
53289 | 662 |
val (passive_set_map0s, active_set_map0s) = chop m set_map0s; |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
663 |
val in_Irel = nth in_Irels (i - 1); |
49501 | 664 |
val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans; |
665 |
val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
666 |
val if_tac = |
60728 | 667 |
EVERY' [dtac ctxt (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], |
668 |
rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, |
|
53289 | 669 |
EVERY' (map2 (fn set_map0 => fn ctor_set_incl => |
60728 | 670 |
EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, |
671 |
rtac ctxt ord_eq_le_trans, rtac ctxt trans_fun_cong_image_id_id_apply, |
|
672 |
rtac ctxt (ctor_set_incl RS subset_trans), etac ctxt le_arg_cong_ctor_dtor]) |
|
53289 | 673 |
passive_set_map0s ctor_set_incls), |
674 |
CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) => |
|
60728 | 675 |
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, |
676 |
rtac ctxt @{thm case_prodI}, rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
677 |
CONJ_WRAP' (fn thm => |
60728 | 678 |
EVERY' (map (etac ctxt) [thm RS subset_trans, le_arg_cong_ctor_dtor])) |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
679 |
ctor_set_set_incls, |
60728 | 680 |
rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl]) |
53289 | 681 |
(in_Irels ~~ (active_set_map0s ~~ ctor_set_set_inclss)), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
682 |
CONJ_WRAP' (fn conv => |
60728 | 683 |
EVERY' [rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0, |
684 |
REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]}, |
|
685 |
REPEAT_DETERM_N n o EVERY' (map (rtac ctxt) [trans, o_apply, conv]), |
|
686 |
rtac ctxt (ctor_inject RS iffD1), rtac ctxt trans, rtac ctxt sym, rtac ctxt ctor_map, |
|
687 |
etac ctxt eq_arg_cong_ctor_dtor]) |
|
49306 | 688 |
fst_snd_convs]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
689 |
val only_if_tac = |
60728 | 690 |
EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], |
691 |
rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, |
|
53289 | 692 |
CONJ_WRAP' (fn (ctor_set, passive_set_map0) => |
60728 | 693 |
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt ctor_set, rtac ctxt @{thm Un_least}, |
694 |
rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals[OF _ refl]}, |
|
60752 | 695 |
rtac ctxt passive_set_map0, rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt, |
60728 | 696 |
CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least})) |
697 |
(fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans, |
|
698 |
rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least}, |
|
699 |
dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE, |
|
700 |
dtac ctxt @{thm ssubst_mem[OF pair_collapse]}, |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
701 |
REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE :: |
56765 | 702 |
@{thms case_prodE iffD1[OF prod.inject, elim_format]}), |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
703 |
hyp_subst_tac ctxt, |
60728 | 704 |
dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, |
60752 | 705 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt]) |
53289 | 706 |
(rev (active_set_map0s ~~ in_Irels))]) |
707 |
(ctor_sets ~~ passive_set_map0s), |
|
60728 | 708 |
rtac ctxt conjI, |
709 |
REPEAT_DETERM_N 2 o EVERY' [rtac ctxt trans, rtac ctxt ctor_map, rtac ctxt (ctor_inject RS iffD2), |
|
710 |
rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0, |
|
711 |
REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]}, |
|
60752 | 712 |
EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, |
713 |
dtac ctxt set_rev_mp, assume_tac ctxt, |
|
60728 | 714 |
dtac ctxt @{thm ssubst_mem[OF pair_collapse]}, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
715 |
REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE :: |
56765 | 716 |
@{thms case_prodE iffD1[OF prod.inject, elim_format]}), |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
717 |
hyp_subst_tac ctxt, |
60752 | 718 |
dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, |
719 |
REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]) |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
720 |
in_Irels), |
60752 | 721 |
assume_tac ctxt]] |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
722 |
in |
60728 | 723 |
EVERY' [rtac ctxt iffI, if_tac, only_if_tac] 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
724 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
725 |
|
58444 | 726 |
fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers |
727 |
ctor_rels = |
|
58446 | 728 |
CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) => |
60728 | 729 |
REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN |
58446 | 730 |
unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN |
60728 | 731 |
HEADGOAL (rtac ctxt @{thm rel_funD[OF snd_transfer]} THEN' |
732 |
etac ctxt (mk_rel_funDN_rotated (n + 1) ctor_fold_transfer) THEN' |
|
58446 | 733 |
EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel => |
60728 | 734 |
etac ctxt (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN' |
735 |
rtac ctxt (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN' |
|
736 |
rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN' |
|
737 |
REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN' |
|
738 |
REPEAT_DETERM o rtac ctxt @{thm fst_transfer} THEN' |
|
739 |
rtac ctxt rel_funI THEN' |
|
740 |
etac ctxt (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels))) |
|
58446 | 741 |
(ctor_rec_defs ~~ ctor_fold_transfers); |
58444 | 742 |
|
57967 | 743 |
fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s = |
51918 | 744 |
let val n = length ks; |
745 |
in |
|
54998 | 746 |
unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN |
60728 | 747 |
EVERY' [REPEAT_DETERM o rtac ctxt allI, rtac ctxt ctor_induct2, |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58446
diff
changeset
|
748 |
EVERY' (@{map 3} (fn IH => fn ctor_rel => fn rel_mono_strong0 => |
60728 | 749 |
EVERY' [rtac ctxt impI, dtac ctxt (ctor_rel RS iffD1), rtac ctxt (IH RS @{thm spec2} RS mp), |
750 |
etac ctxt rel_mono_strong0, |
|
751 |
REPEAT_DETERM_N m o rtac ctxt @{thm ballI[OF ballI[OF imp_refl]]}, |
|
51918 | 752 |
EVERY' (map (fn j => |
60728 | 753 |
EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) j, rtac ctxt @{thm ballI[OF ballI]}, |
51918 | 754 |
Goal.assume_rule_tac ctxt]) ks)]) |
57967 | 755 |
IHs ctor_rels rel_mono_strong0s)] 1 |
51918 | 756 |
end; |
757 |
||
55901
8c6d49dd8ae1
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
blanchet
parents:
55756
diff
changeset
|
758 |
fun mk_fold_transfer_tac ctxt m ctor_rel_induct map_transfers folds = |
52731 | 759 |
let |
760 |
val n = length map_transfers; |
|
761 |
in |
|
762 |
unfold_thms_tac ctxt |
|
55945 | 763 |
@{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN |
764 |
unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN |
|
52731 | 765 |
HEADGOAL (EVERY' |
60728 | 766 |
[REPEAT_DETERM o resolve_tac ctxt [allI, impI], rtac ctxt ctor_rel_induct, |
52731 | 767 |
EVERY' (map (fn map_transfer => EVERY' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
768 |
[REPEAT_DETERM o resolve_tac ctxt [allI, impI, @{thm vimage2pI}], |
52731 | 769 |
SELECT_GOAL (unfold_thms_tac ctxt folds), |
60728 | 770 |
etac ctxt @{thm predicate2D_vimage2p}, |
771 |
rtac ctxt (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer), |
|
772 |
REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer}, |
|
773 |
REPEAT_DETERM_N n o rtac ctxt @{thm vimage2p_rel_fun}, |
|
60752 | 774 |
assume_tac ctxt]) |
52731 | 775 |
map_transfers)]) |
776 |
end; |
|
777 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
778 |
end; |