author  wenzelm 
Sat, 30 Jul 2016 21:10:02 +0200  
changeset 63568  e63c8f2fbd28 
parent 63312  d75d1e399698 
child 67399  eab6ce8368fa 
permissions  rwrr 
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 relatoruse (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_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

59 
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

60 
val mk_mor_fold_tac: Proof.context > ctyp > cterm > thm list > thm > thm > tactic 
60728  61 
val mk_mor_select_tac: Proof.context > thm > thm > thm > thm > thm > thm > thm list > 
62 
thm list list > thm list > tactic 

63 
val mk_mor_str_tac: Proof.context > 'a list > thm > tactic 

55197  64 
val mk_rel_induct_tac: Proof.context > thm list > int > thm > int list > thm list > 
65 
thm list > tactic 

66 
val mk_rec_tac: Proof.context > thm list > thm > thm list > tactic 

67 
val mk_rec_unique_mor_tac: Proof.context > thm list > thm list > thm > tactic 

68 
val mk_set_bd_tac: Proof.context > int > (int > tactic) > thm > thm list list > thm list > 

69 
int > tactic 

70 
val mk_set_nat_tac: Proof.context > int > (int > tactic) > thm list list > thm list > 

71 
cterm list > thm list > int > tactic 

60728  72 
val mk_set_map0_tac: Proof.context > thm > tactic 
73 
val mk_set_tac: Proof.context > thm > tactic 

51798  74 
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

75 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

76 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

77 
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

78 
struct 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

79 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

80 
open BNF_Tactics 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

81 
open BNF_LFP_Util 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

82 
open BNF_Util 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

83 

49306  84 
val fst_snd_convs = @{thms fst_conv snd_conv}; 
85 
val ord_eq_le_trans = @{thm ord_eq_le_trans}; 

86 
val subset_trans = @{thm subset_trans}; 

87 
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

88 
val rev_bspec = Drule.rotate_prems 1 bspec; 
56114  89 
val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]}; 
90 
val relChainD = @{thm iffD2[OF meta_eq_to_obj_eq[OF relChain_def]]}; 

49306  91 

60728  92 
fun mk_alg_set_tac ctxt alg_def = 
93 
EVERY' [dtac ctxt (alg_def RS iffD1), REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, rtac ctxt CollectI, 

60752  94 
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

95 

51798  96 
fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits = 
60728  97 
(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

98 
REPEAT_DETERM o FIRST' 
60728  99 
[EVERY' [rtac ctxt @{thm subset_emptyI}, eresolve_tac ctxt wits], 
100 
EVERY' [rtac ctxt subsetI, rtac ctxt FalseE, eresolve_tac ctxt wits], 

101 
EVERY' [rtac ctxt subsetI, dresolve_tac ctxt wits, hyp_subst_tac ctxt, 

60752  102 
FIRST' (map (fn thm => rtac ctxt thm THEN' assume_tac ctxt) alg_sets)]] THEN' 
60728  103 
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

104 

60728  105 
fun mk_mor_elim_tac ctxt mor_def = 
106 
(dtac ctxt (mor_def RS iffD1) THEN' 

107 
REPEAT o etac ctxt conjE THEN' 

108 
TRY o rtac ctxt @{thm image_subsetI} THEN' 

109 
etac ctxt bspec THEN' 

60752  110 
assume_tac ctxt) 1; 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

111 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset

112 
fun mk_mor_incl_tac ctxt mor_def map_ids = 
60728  113 
(rtac ctxt (mor_def RS iffD2) THEN' 
114 
rtac ctxt conjI THEN' 

115 
CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})])) 

56114  116 
map_ids THEN' 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

117 
CONJ_WRAP' (fn thm => 
60728  118 
(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

119 

60728  120 
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

121 
let 
56114  122 
val fbetw_tac = 
60752  123 
EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}), 
124 
etac ctxt bspec, etac ctxt bspec, assume_tac ctxt]; 

53290  125 
fun mor_tac (set_map, map_comp_id) = 
60728  126 
EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt trans, 
60752  127 
rtac ctxt trans, dtac ctxt rev_bspec, assume_tac ctxt, etac ctxt arg_cong, 
60757  128 
REPEAT o eresolve_tac ctxt [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

129 
CONJ_WRAP' (fn thm => 
60728  130 
FIRST' [rtac ctxt subset_UNIV, 
131 
(EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI}, 

60752  132 
etac ctxt bspec, etac ctxt set_mp, assume_tac ctxt])]) set_map THEN' 
60728  133 
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

134 
in 
60728  135 
(dtac ctxt (mor_def RS iffD1) THEN' dtac ctxt (mor_def RS iffD1) THEN' rtac ctxt (mor_def RS iffD2) THEN' 
136 
REPEAT o etac ctxt conjE THEN' 

137 
rtac ctxt conjI THEN' 

53290  138 
CONJ_WRAP' (K fbetw_tac) set_maps THEN' 
139 
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

140 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

141 

60728  142 
fun mk_mor_str_tac ctxt ks mor_def = 
143 
(rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN' 

144 
CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt UNIV_I])) ks THEN' 

145 
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

146 

60728  147 
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

148 
let 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

149 
val n = length morEs; 
60728  150 
fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE, 
151 
rtac ctxt CollectI, CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto m + n), 

152 
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

153 
in 
60728  154 
EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs, 
155 
rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) morEs, 

156 
REPEAT_DETERM o etac ctxt conjE, REPEAT_DETERM_N n o dtac ctxt (@{thm fun_eq_iff} RS iffD1), 

157 
CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE, rtac ctxt trans, 

158 
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

159 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

160 

60728  161 
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

162 
let 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

163 
val n = length alg_sets; 
56237  164 
fun set_tac thm = 
60728  165 
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans, etac ctxt @{thm image_mono}, 
62906  166 
rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on}]; 
56237  167 
val alg_tac = 
168 
CONJ_WRAP' (fn (set_maps, alg_set) => 

60757  169 
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt set_mp, 
62906  170 
rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on[OF bij_betw_the_inv_into]}, 
60728  171 
rtac ctxt imageI, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))]) 
56237  172 
(set_mapss ~~ alg_sets); 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

173 

60728  174 
val mor_tac = rtac ctxt conjI THEN' CONJ_WRAP' (K (etac ctxt @{thm bij_betwE})) alg_sets THEN' 
56237  175 
CONJ_WRAP' (fn (set_maps, alg_set) => 
60757  176 
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], 
60728  177 
etac ctxt @{thm f_the_inv_into_f_bij_betw}, etac ctxt alg_set, 
56237  178 
EVERY' (map set_tac (drop m set_maps))]) 
179 
(set_mapss ~~ alg_sets); 

48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

180 
in 
60728  181 
(REPEAT_DETERM_N n o rtac ctxt exI THEN' rtac ctxt conjI THEN' 
182 
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

183 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

184 

60728  185 
fun mk_bd_limit_tac ctxt n bd_Cinfinite = 
186 
EVERY' [REPEAT_DETERM o etac ctxt conjE, rtac ctxt rev_mp, rtac ctxt @{thm Cinfinite_limit_finite}, 

187 
REPEAT_DETERM_N n o rtac ctxt @{thm finite.insertI}, rtac ctxt @{thm finite.emptyI}, 

188 
REPEAT_DETERM_N n o etac ctxt @{thm insert_subsetI}, rtac ctxt @{thm empty_subsetI}, 

189 
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

190 
CONJ_WRAP' (fn i => 
60728  191 
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

192 
(0 upto n  1), 
60752  193 
assume_tac ctxt] 1; 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

194 

60728  195 
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

196 
let 
60752  197 
val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt bspec, 
198 
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

199 
fun minH_tac thm = 
60728  200 
EVERY' [rtac ctxt Un_cong, minG_tac, rtac ctxt @{thm image_cong}, rtac ctxt thm, 
201 
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

202 
in 
60728  203 
(rtac ctxt (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ctxt iffD2 THEN' 
204 
rtac ctxt meta_eq_to_obj_eq THEN' rtac ctxt (worel RS @{thm wo_rel.adm_wo_def}) THEN' 

205 
REPEAT_DETERM_N 3 o rtac ctxt allI THEN' rtac ctxt impI THEN' 

206 
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

207 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

208 

60728  209 
fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac ctxt relChainD, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, 
210 
rtac ctxt @{thm case_split}, rtac ctxt @{thm xt1(3)}, rtac ctxt min_algs, etac ctxt @{thm FieldI2}, rtac ctxt subsetI, 

60752  211 
rtac ctxt UnI1, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, assume_tac ctxt, 
212 
assume_tac ctxt, rtac ctxt equalityD1, dtac ctxt @{thm notnotD}, 

213 
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

214 

60728  215 
fun mk_min_algs_card_of_tac ctxt cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero 
51812  216 
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

217 
let 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

218 
val induct = worel RS 
60801  219 
Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp}; 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

220 
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

221 
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

222 
val absorbAs_tac = if m = 0 then K (all_tac) 
60728  223 
else EVERY' [rtac ctxt @{thm ordIso_transitive}, rtac ctxt @{thm csum_cong1}, 
224 
rtac ctxt @{thm ordIso_transitive}, 

225 
BNF_Tactics.mk_rotate_eq_tac ctxt (rtac ctxt @{thm ordIso_refl} THEN' 

226 
FIRST' [rtac ctxt @{thm card_of_Card_order}, rtac ctxt @{thm Card_order_csum}, 

227 
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

228 
@{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

229 
src dest, 
60728  230 
rtac ctxt @{thm csum_absorb1}, rtac ctxt Asuc_Cinfinite, rtac ctxt ctrans, rtac ctxt @{thm ordLeq_csum1}, 
231 
FIRST' [rtac ctxt @{thm Card_order_csum}, rtac ctxt @{thm card_of_Card_order}], 

232 
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

233 

60728  234 
val minG_tac = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordLess_imp_ordLeq}, 
235 
rtac ctxt @{thm ordLess_transitive}, rtac ctxt @{thm card_of_underS}, rtac ctxt suc_Card_order, 

60752  236 
assume_tac ctxt, rtac ctxt suc_Asuc, rtac ctxt ballI, etac ctxt allE, 
237 
dtac ctxt mp, etac ctxt @{thm underS_E}, 

238 
dtac ctxt mp, etac ctxt @{thm underS_Field}, 

239 
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

240 

60728  241 
fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, 
242 
rtac ctxt @{thm card_of_ordIso_subst}, etac ctxt min_alg, rtac ctxt @{thm Un_Cinfinite_bound}, 

243 
minG_tac, rtac ctxt ctrans, rtac ctxt @{thm card_of_image}, rtac ctxt ctrans, rtac ctxt in_bd, rtac ctxt ctrans, 

244 
rtac ctxt @{thm cexp_mono1}, rtac ctxt @{thm csum_mono1}, 

245 
REPEAT_DETERM_N m o rtac ctxt @{thm csum_mono2}, 

246 
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

247 
REPEAT_DETERM o FIRST' 
60728  248 
[rtac ctxt @{thm card_of_Card_order}, rtac ctxt @{thm Card_order_csum}, 
249 
rtac ctxt Asuc_Cinfinite, rtac ctxt bd_Card_order], 

250 
rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm cexp_cong1}, absorbAs_tac, 

251 
rtac ctxt @{thm csum_absorb1}, rtac ctxt Asuc_Cinfinite, rtac ctxt @{thm ctwo_ordLeq_Cinfinite}, 

252 
rtac ctxt Asuc_Cinfinite, rtac ctxt bd_Card_order, 

253 
rtac ctxt @{thm ordIso_imp_ordLeq}, rtac ctxt @{thm cexp_cprod_ordLeq}, 

60757  254 
resolve_tac ctxt @{thms Card_order_csum Card_order_ctwo}, rtac ctxt suc_Cinfinite, 
60728  255 
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

256 
in 
60728  257 
(rtac ctxt induct THEN' 
258 
rtac ctxt impI THEN' 

48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

259 
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

260 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

261 

60728  262 
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

263 
let 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

264 
val induct = worel RS 
60801  265 
Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp}; 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

266 

60752  267 
val minG_tac = 
268 
EVERY' [rtac ctxt @{thm UN_least}, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E}, 

269 
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

270 

60728  271 
fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ctxt ord_eq_le_trans, etac ctxt min_alg, 
272 
rtac ctxt @{thm Un_least}, minG_tac, rtac ctxt @{thm image_subsetI}, 

60757  273 
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], etac ctxt alg_set, 
60728  274 
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

275 
in 
60728  276 
(rtac ctxt induct THEN' 
277 
rtac ctxt impI THEN' 

48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

278 
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

279 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

280 

60728  281 
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

282 
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

283 
let 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

284 
val n = length min_algs; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

285 
fun mk_cardSuc_UNION_tac set_bds (mono, def) = EVERY' 
60728  286 
[rtac ctxt bexE, rtac ctxt @{thm cardSuc_UNION_Cinfinite}, rtac ctxt bd_Cinfinite, rtac ctxt mono, 
60757  287 
etac ctxt (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve_tac ctxt set_bds]; 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

288 
fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) = 
60757  289 
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], 
60728  290 
EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt bexE, 
60752  291 
rtac ctxt bd_limit, REPEAT_DETERM_N (n  1) o etac ctxt conjI, assume_tac ctxt, 
60728  292 
rtac ctxt (min_alg_def RS @{thm set_mp[OF equalityD2]}), 
60752  293 
rtac ctxt @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac ctxt thin_rl, 
294 
assume_tac ctxt, rtac ctxt set_mp, 

295 
rtac ctxt equalityD2, rtac ctxt min_alg, assume_tac ctxt, rtac ctxt UnI2, 

296 
rtac ctxt @{thm image_eqI}, rtac ctxt refl, 

60728  297 
rtac ctxt CollectI, REPEAT_DETERM_N m o dtac ctxt asm_rl, REPEAT_DETERM_N n o etac ctxt thin_rl, 
298 
REPEAT_DETERM o etac ctxt conjE, 

60752  299 
CONJ_WRAP' (K (FIRST' [assume_tac ctxt, 
60728  300 
EVERY' [etac ctxt subset_trans, rtac ctxt subsetI, rtac ctxt @{thm UN_I}, 
60752  301 
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

302 
set_bds]; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

303 
in 
60728  304 
(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

305 
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

306 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

307 

60728  308 
fun mk_card_of_min_alg_tac ctxt min_alg_def card_of suc_Card_order suc_Asuc Asuc_Cinfinite = 
309 
EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt (min_alg_def RS @{thm card_of_ordIso_subst}), 

310 
rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordIso_ordLeq_trans}, 

311 
rtac ctxt @{thm card_of_Field_ordIso}, rtac ctxt suc_Card_order, rtac ctxt @{thm ordLess_imp_ordLeq}, 

60752  312 
rtac ctxt suc_Asuc, rtac ctxt ballI, dtac ctxt rev_mp, rtac ctxt card_of, 
313 
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

314 

60728  315 
fun mk_least_min_alg_tac ctxt min_alg_def least = 
60752  316 
EVERY' [rtac ctxt (min_alg_def RS ord_eq_le_trans), rtac ctxt @{thm UN_least}, 
317 
dtac ctxt least, dtac ctxt mp, assume_tac ctxt, 

318 
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

319 

55197  320 
fun mk_alg_select_tac ctxt Abs_inverse = 
60728  321 
EVERY' [rtac ctxt ballI, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset

322 
REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN 
60752  323 
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

324 

60728  325 
fun mk_mor_select_tac ctxt mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets 
53290  326 
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

327 
let 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

328 
val n = length alg_sets; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

329 
val fbetw_tac = 
60752  330 
CONJ_WRAP' 
331 
(K (EVERY' [rtac ctxt ballI, etac ctxt rev_bspec, 

332 
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

333 
val mor_tac = 
60728  334 
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs; 
53290  335 
fun alg_epi_tac ((alg_set, str_init_def), set_map) = 
60757  336 
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI, 
60777  337 
rtac ctxt ballI, forward_tac ctxt [alg_select RS bspec], 
338 
rtac ctxt (str_init_def RS @{thm ssubst_mem}), 

60757  339 
etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map, 
60728  340 
rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec, 
60752  341 
assume_tac ctxt]]; 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

342 
in 
60728  343 
EVERY' [rtac ctxt mor_cong, REPEAT_DETERM_N n o (rtac ctxt sym THEN' rtac ctxt @{thm comp_id}), 
344 
rtac ctxt (Thm.permute_prems 0 1 mor_comp), etac ctxt (Thm.permute_prems 0 1 mor_comp), 

345 
rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, fbetw_tac, mor_tac, rtac ctxt mor_incl_min_alg, 

346 
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

347 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

348 

56237  349 
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

350 
let 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

351 
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

352 
in 
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61424
diff
changeset

353 
EVERY' [Method.insert_tac ctxt (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs), 
61334
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
60801
diff
changeset

354 
REPEAT_DETERM o dtac ctxt meta_spec, REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp, 
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
60801
diff
changeset

355 
rtac ctxt copy, REPEAT_DETERM_N n o assume_tac ctxt, 
60757  356 
rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI, 
60728  357 
rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, 
60752  358 
rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt, 
56237  359 
SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)), 
60728  360 
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

361 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

362 

60728  363 
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

364 
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

365 
let 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

366 
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

367 
val ks = (1 upto n); 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

368 

60728  369 
fun mor_tac morE in_mono = EVERY' [etac ctxt morE, rtac ctxt set_mp, rtac ctxt in_mono, 
370 
REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt CollectI, 

60752  371 
REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' assume_tac ctxt)]; 
56263  372 
fun cong_tac ct map_cong0 = EVERY' 
60784  373 
[rtac ctxt (map_cong0 RS infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong), 
60728  374 
REPEAT_DETERM_N m o rtac ctxt refl, 
60752  375 
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

376 

56263  377 
fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) = 
60728  378 
EVERY' [rtac ctxt ballI, rtac ctxt CollectI, 
60757  379 
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set), 
60728  380 
REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}), 
381 
rtac ctxt trans, mor_tac morE in_mono, 

382 
rtac ctxt trans, cong_tac ct map_cong0, 

383 
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

384 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

385 
fun mk_unique_tac (k, least_min_alg) = 
60728  386 
select_prem_tac ctxt n (etac ctxt @{thm prop_restrict}) k THEN' rtac ctxt least_min_alg THEN' 
387 
rtac ctxt (alg_def RS iffD2) THEN' 

56263  388 
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

389 
in 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

390 
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

391 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

392 

60728  393 
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

394 
let 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

395 
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

396 

60728  397 
fun mk_alg_tac alg_set = EVERY' [rtac ctxt ballI, rtac ctxt CollectI, 
60757  398 
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set), 
60728  399 
REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}), 
400 
rtac ctxt mp, etac ctxt bspec, rtac ctxt CollectI, 

60752  401 
REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt), 
60728  402 
CONJ_WRAP' (K (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict})) alg_sets, 
60752  403 
CONJ_WRAP' (K (rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)) 
404 
alg_sets]; 

48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

405 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

406 
fun mk_induct_tac least_min_alg = 
60728  407 
rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' rtac ctxt least_min_alg THEN' 
408 
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

409 
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

410 
in 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

411 
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

412 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

413 

56237  414 
fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses alg_min_alg alg_sets set_mapss = 
415 
unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN 

60728  416 
EVERY' [rtac ctxt conjI, 
417 
CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' rtac ctxt thm) Reps, 

56237  418 
CONJ_WRAP' (fn (Abs_inverse, (set_maps, alg_set)) => 
60728  419 
EVERY' [rtac ctxt ballI, rtac ctxt Abs_inverse, rtac ctxt (alg_min_alg RS alg_set), 
56237  420 
EVERY' (map2 (fn Rep => fn set_map => 
60728  421 
EVERY' [rtac ctxt (set_map RS ord_eq_le_trans), rtac ctxt @{thm image_subsetI}, rtac ctxt Rep]) 
56237  422 
Reps (drop m set_maps))]) 
423 
(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

424 

56237  425 
fun mk_mor_Abs_tac ctxt cts defs Abs_inverses map_comp_ids map_congLs = 
426 
unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN 

60728  427 
EVERY' [rtac ctxt conjI, 
428 
CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses, 

56237  429 
CONJ_WRAP' (fn (ct, thm) => 
60728  430 
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], 
60784  431 
rtac ctxt (thm RS (infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong) RS sym), 
56237  432 
EVERY' (map (fn Abs_inverse => 
60752  433 
EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse), 
434 
assume_tac ctxt]) 

56237  435 
Abs_inverses)]) 
63568  436 
(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

437 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset

438 
fun mk_mor_fold_tac ctxt cT ct fold_defs ex_mor mor = 
60728  439 
(EVERY' (map (stac ctxt) fold_defs) THEN' EVERY' [rtac ctxt rev_mp, rtac ctxt ex_mor, rtac ctxt impI] THEN' 
440 
REPEAT_DETERM_N (length fold_defs) o etac ctxt exE THEN' 

60801  441 
rtac ctxt (Thm.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

442 

60728  443 
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

444 
let 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

445 
fun mk_unique type_def = 
60728  446 
EVERY' [rtac ctxt @{thm surj_fun_eq}, rtac ctxt (type_def RS @{thm type_definition.Abs_image}), 
60757  447 
rtac ctxt ballI, resolve_tac ctxt init_unique_mors, 
60752  448 
EVERY' (map (fn thm => assume_tac ctxt ORELSE' rtac ctxt thm) Reps), 
449 
rtac ctxt mor_comp, rtac ctxt mor_Abs, assume_tac ctxt, 

60728  450 
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

451 
in 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

452 
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

453 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

454 

60728  455 
fun mk_dtor_o_ctor_tac ctxt dtor_def foldx map_comp_id map_cong0L ctor_o_folds = 
456 
EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt (dtor_def RS fun_cong RS trans), 

457 
rtac ctxt trans, rtac ctxt foldx, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L, 

458 
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

459 
ctor_o_folds), 
60728  460 
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

461 

55197  462 
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

463 
unfold_thms_tac ctxt 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

464 
(rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN 
60728  465 
EVERY' [rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt (foldx RS @{thm arg_cong[of _ _ snd]}), 
466 
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

467 

55197  468 
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

469 
unfold_thms_tac ctxt 
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49585
diff
changeset

470 
(rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN 
60728  471 
etac ctxt fold_unique_mor 1; 
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49585
diff
changeset

472 

53290  473 
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

474 
let 
53290  475 
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

476 
val ks = 1 upto n; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

477 

53290  478 
fun mk_IH_tac Rep_inv Abs_inv set_map = 
60728  479 
DETERM o EVERY' [dtac ctxt meta_mp, rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt bspec, 
480 
dtac ctxt set_rev_mp, rtac ctxt equalityD1, rtac ctxt set_map, etac ctxt imageE, 

60752  481 
hyp_subst_tac ctxt, rtac ctxt (Abs_inv RS @{thm ssubst_mem}), etac ctxt set_mp, 
482 
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

483 

53290  484 
fun mk_closed_tac (k, (morE, set_maps)) = 
60728  485 
EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) k, rtac ctxt ballI, rtac ctxt impI, 
60752  486 
rtac ctxt (mor_Abs RS morE RS arg_cong RS iffD2), assume_tac ctxt, 
60728  487 
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], dtac ctxt @{thm meta_spec}, 
60752  488 
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

489 

49227  490 
fun mk_induct_tac (Rep, Rep_inv) = 
60728  491 
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

492 
in 
60728  493 
(rtac ctxt mp THEN' rtac ctxt impI THEN' 
494 
DETERM o CONJ_WRAP_GEN' (etac ctxt conjE THEN' rtac ctxt conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN' 

495 
rtac ctxt init_induct THEN' 

53290  496 
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

497 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

498 

55197  499 
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

500 
let 
49501  501 
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

502 
val ks = 1 upto n; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

503 
fun mk_inner_induct_tac induct i = 
60728  504 
EVERY' [rtac ctxt allI, fo_rtac ctxt induct, 
505 
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

506 
REPEAT_DETERM_N n o 
60728  507 
EVERY' [dtac ctxt meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt, 
60752  508 
REPEAT_DETERM o dtac ctxt @{thm meta_spec}, etac ctxt (spec RS meta_mp), 
509 
assume_tac ctxt], 

510 
assume_tac ctxt]; 

48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

511 
in 
60801  512 
EVERY' [rtac ctxt rev_mp, rtac ctxt (Thm.instantiate' cTs cts ctor_induct), 
60728  513 
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

514 
REPEAT_DETERM o eresolve_tac ctxt [conjE, allE], 
60752  515 
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

516 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

517 

60728  518 
fun mk_map_tac ctxt m n foldx map_comp_id map_cong0 = 
519 
EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt foldx, rtac ctxt trans, 

520 
rtac ctxt o_apply, 

521 
rtac ctxt trans, rtac ctxt (map_comp_id RS arg_cong), rtac ctxt trans, rtac ctxt (map_cong0 RS arg_cong), 

522 
REPEAT_DETERM_N m o rtac ctxt refl, 

523 
REPEAT_DETERM_N n o (EVERY' (map (rtac ctxt) [trans, o_apply, id_apply])), 

524 
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

525 

55197  526 
fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps = 
60728  527 
rtac ctxt fold_unique 1 THEN 
55067  528 
unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN 
60752  529 
ALLGOALS (assume_tac ctxt); 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

530 

60728  531 
fun mk_set_tac ctxt foldx = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, 
532 
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

533 

60728  534 
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

535 
let 
53290  536 
val n = length set_maps; 
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61841
diff
changeset

537 
fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans) 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61841
diff
changeset

538 
THEN' rtac ctxt @{thm refl}; 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

539 
in 
60728  540 
EVERY' [rtac ctxt (set RS @{thm comp_eq_dest} RS trans), rtac ctxt Un_cong, 
541 
rtac ctxt (trans OF [set_map, trans_fun_cong_image_id_id_apply]), 

542 
REPEAT_DETERM_N (n  1) o rtac ctxt Un_cong, 

53290  543 
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

544 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

545 

55197  546 
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

547 
let 
49541  548 
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

549 

60728  550 
fun useIH set_nat = EVERY' [rtac ctxt trans, rtac ctxt @{thm image_UN}, rtac ctxt trans, rtac ctxt @{thm SUP_cong}, 
551 
rtac ctxt refl, Goal.assume_rule_tac ctxt, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm SUP_cong}, 

552 
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

553 

49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49544
diff
changeset

554 
fun mk_set_nat cset ctor_map ctor_set set_nats = 
60728  555 
EVERY' [rtac ctxt trans, rtac ctxt @{thm image_cong}, rtac ctxt ctor_set, rtac ctxt refl, rtac ctxt sym, 
60784  556 
rtac ctxt (trans OF [ctor_map RS infer_instantiate' ctxt [NONE, NONE, SOME cset] arg_cong, 
56262  557 
ctor_set RS trans]), 
60728  558 
rtac ctxt sym, EVERY' (map (rtac ctxt) [trans, @{thm image_Un}, Un_cong]), 
559 
rtac ctxt sym, rtac ctxt (nth set_nats (i  1)), 

560 
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

561 
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

562 
in 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58446
diff
changeset

563 
(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

564 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

565 

55197  566 
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

567 
let 
49542
b39354db8629
renamed lowlevel "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset

568 
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

569 

60728  570 
fun useIH set_bd = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt set_bd, rtac ctxt ballI, 
571 
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

572 

49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49544
diff
changeset

573 
fun mk_set_nat ctor_set set_bds = 
60728  574 
EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm card_of_ordIso_subst}, rtac ctxt ctor_set, 
575 
rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac ctxt (nth set_bds (i  1)), 

576 
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

577 
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

578 
in 
49542
b39354db8629
renamed lowlevel "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset

579 
(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

580 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

581 

55197  582 
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

583 
let 
60728  584 
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

585 

60728  586 
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

587 
CONJ_WRAP' (fn thm => 
60728  588 
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

589 

51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset

590 
fun mk_map_cong0 ctor_map map_cong0 set_setss = 
60728  591 
EVERY' [rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE, 
592 
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

593 
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

594 
EVERY' (map useIH (transpose (map tl set_setss))), 
60728  595 
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

596 
in 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58446
diff
changeset

597 
(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

598 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

599 

57967  600 
fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs = 
60728  601 
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

602 
@{map 4} (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO => 
60728  603 
EVERY' [rtac ctxt impI, etac ctxt (nchotomy RS @{thm nchotomy_relcomppE}), 
604 
REPEAT_DETERM_N 2 o dtac ctxt (Irel RS iffD1), rtac ctxt (Irel RS iffD2), 

605 
rtac ctxt rel_mono, rtac ctxt (le_rel_OO RS @{thm predicate2D}), 

60752  606 
rtac ctxt @{thm relcomppI}, assume_tac ctxt, assume_tac ctxt, 
607 
REPEAT_DETERM_N m o EVERY' [rtac ctxt ballI, rtac ctxt ballI, rtac ctxt impI, assume_tac ctxt], 

57726  608 
REPEAT_DETERM_N (length le_rel_OOs) o 
60728  609 
EVERY' [rtac ctxt ballI, rtac ctxt ballI, Goal.assume_rule_tac ctxt]]) 
57967  610 
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

611 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

612 
(* BNF tactics *) 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

613 

60728  614 
fun mk_map_id0_tac ctxt map_id0s unique = 
615 
(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

616 
EVERY' (map (fn thm => 
60728  617 
EVERY' [rtac ctxt trans, rtac ctxt @{thm id_comp}, rtac ctxt trans, rtac ctxt sym, rtac ctxt @{thm comp_id}, 
618 
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

619 

60728  620 
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

621 
let 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

622 
val i = iplus1  1; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

623 
val unique' = Thm.permute_prems 0 i unique; 
53288  624 
val map_comp0s' = drop i map_comp0s @ take i map_comp0s; 
49541  625 
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

626 
fun mk_comp comp simp = 
60728  627 
EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt o_apply, 
628 
rtac ctxt trans, rtac ctxt (simp RS arg_cong), rtac ctxt trans, rtac ctxt simp, 

629 
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

630 
in 
60728  631 
(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

632 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

633 

60728  634 
fun mk_set_map0_tac ctxt set_nat = 
635 
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

636 

60728  637 
fun mk_bd_card_order_tac ctxt bd_card_orders = 
638 
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

639 

51798  640 
fun mk_wit_tac ctxt n ctor_set wit = 
60752  641 
REPEAT_DETERM (assume_tac ctxt 1 ORELSE 
60728  642 
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

643 
REPEAT_DETERM o 
60728  644 
(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

645 
(eresolve_tac ctxt wit ORELSE' 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset

646 
(dresolve_tac ctxt wit THEN' 
60728  647 
(etac ctxt FalseE ORELSE' 
648 
EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set, 

649 
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

650 

53287  651 
fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject 
53289  652 
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

653 
let 
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset

654 
val m = length ctor_set_incls; 
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset

655 
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

656 

53289  657 
val (passive_set_map0s, active_set_map0s) = chop m set_map0s; 
51893
596baae88a88
got rid of the set based relatoruse (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset

658 
val in_Irel = nth in_Irels (i  1); 
49501  659 
val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans; 
660 
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

661 
val if_tac = 
60728  662 
EVERY' [dtac ctxt (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], 
663 
rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, 

53289  664 
EVERY' (map2 (fn set_map0 => fn ctor_set_incl => 
60728  665 
EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, 
666 
rtac ctxt ord_eq_le_trans, rtac ctxt trans_fun_cong_image_id_id_apply, 

667 
rtac ctxt (ctor_set_incl RS subset_trans), etac ctxt le_arg_cong_ctor_dtor]) 

53289  668 
passive_set_map0s ctor_set_incls), 
669 
CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) => 

60728  670 
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, 
671 
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

672 
CONJ_WRAP' (fn thm => 
60728  673 
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

674 
ctor_set_set_incls, 
60728  675 
rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl]) 
53289  676 
(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

677 
CONJ_WRAP' (fn conv => 
60728  678 
EVERY' [rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0, 
679 
REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]}, 

680 
REPEAT_DETERM_N n o EVERY' (map (rtac ctxt) [trans, o_apply, conv]), 

681 
rtac ctxt (ctor_inject RS iffD1), rtac ctxt trans, rtac ctxt sym, rtac ctxt ctor_map, 

682 
etac ctxt eq_arg_cong_ctor_dtor]) 

49306  683 
fst_snd_convs]; 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

684 
val only_if_tac = 
60728  685 
EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], 
686 
rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, 

53289  687 
CONJ_WRAP' (fn (ctor_set, passive_set_map0) => 
60728  688 
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt ctor_set, rtac ctxt @{thm Un_least}, 
689 
rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals[OF _ refl]}, 

60752  690 
rtac ctxt passive_set_map0, rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt, 
60728  691 
CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least})) 
692 
(fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans, 

693 
rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least}, 

694 
dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE, 

61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61334
diff
changeset

695 
dtac ctxt @{thm ssubst_mem[OF prod.collapse]}, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset

696 
REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE :: 
56765  697 
@{thms case_prodE iffD1[OF prod.inject, elim_format]}), 
51893
596baae88a88
got rid of the set based relatoruse (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset

698 
hyp_subst_tac ctxt, 
60728  699 
dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, 
60752  700 
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt]) 
53289  701 
(rev (active_set_map0s ~~ in_Irels))]) 
702 
(ctor_sets ~~ passive_set_map0s), 

60728  703 
rtac ctxt conjI, 
704 
REPEAT_DETERM_N 2 o EVERY' [rtac ctxt trans, rtac ctxt ctor_map, rtac ctxt (ctor_inject RS iffD2), 

705 
rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0, 

706 
REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]}, 

60752  707 
EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, 
708 
dtac ctxt set_rev_mp, assume_tac ctxt, 

61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61334
diff
changeset

709 
dtac ctxt @{thm ssubst_mem[OF prod.collapse]}, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset

710 
REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE :: 
56765  711 
@{thms case_prodE iffD1[OF prod.inject, elim_format]}), 
51893
596baae88a88
got rid of the set based relatoruse (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset

712 
hyp_subst_tac ctxt, 
60752  713 
dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, 
714 
REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]) 

51893
596baae88a88
got rid of the set based relatoruse (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset

715 
in_Irels), 
60752  716 
assume_tac ctxt]] 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

717 
in 
60728  718 
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

719 
end; 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

720 

58444  721 
fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers 
722 
ctor_rels = 

58446  723 
CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) => 
60728  724 
REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN 
58446  725 
unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN 
60728  726 
HEADGOAL (rtac ctxt @{thm rel_funD[OF snd_transfer]} THEN' 
727 
etac ctxt (mk_rel_funDN_rotated (n + 1) ctor_fold_transfer) THEN' 

58446  728 
EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel => 
60728  729 
etac ctxt (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN' 
730 
rtac ctxt (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN' 

731 
rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN' 

732 
REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN' 

733 
REPEAT_DETERM o rtac ctxt @{thm fst_transfer} THEN' 

734 
rtac ctxt rel_funI THEN' 

735 
etac ctxt (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels))) 

58446  736 
(ctor_rec_defs ~~ ctor_fold_transfers); 
58444  737 

57967  738 
fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s = 
51918  739 
let val n = length ks; 
740 
in 

54998  741 
unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN 
60728  742 
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

743 
EVERY' (@{map 3} (fn IH => fn ctor_rel => fn rel_mono_strong0 => 
60728  744 
EVERY' [rtac ctxt impI, dtac ctxt (ctor_rel RS iffD1), rtac ctxt (IH RS @{thm spec2} RS mp), 
745 
etac ctxt rel_mono_strong0, 

746 
REPEAT_DETERM_N m o rtac ctxt @{thm ballI[OF ballI[OF imp_refl]]}, 

51918  747 
EVERY' (map (fn j => 
60728  748 
EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) j, rtac ctxt @{thm ballI[OF ballI]}, 
51918  749 
Goal.assume_rule_tac ctxt]) ks)]) 
57967  750 
IHs ctor_rels rel_mono_strong0s)] 1 
51918  751 
end; 
752 

55901
8c6d49dd8ae1
renamed a pair of lowlevel theorems to have c/dtor in their names (like the others)
blanchet
parents:
55756
diff
changeset

753 
fun mk_fold_transfer_tac ctxt m ctor_rel_induct map_transfers folds = 
52731  754 
let 
755 
val n = length map_transfers; 

756 
in 

757 
unfold_thms_tac ctxt 

55945  758 
@{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN 
759 
unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN 

52731  760 
HEADGOAL (EVERY' 
60728  761 
[REPEAT_DETERM o resolve_tac ctxt [allI, impI], rtac ctxt ctor_rel_induct, 
52731  762 
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

763 
[REPEAT_DETERM o resolve_tac ctxt [allI, impI, @{thm vimage2pI}], 
52731  764 
SELECT_GOAL (unfold_thms_tac ctxt folds), 
60728  765 
etac ctxt @{thm predicate2D_vimage2p}, 
766 
rtac ctxt (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer), 

767 
REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer}, 

768 
REPEAT_DETERM_N n o rtac ctxt @{thm vimage2p_rel_fun}, 

60752  769 
assume_tac ctxt]) 
52731  770 
map_transfers)]) 
771 
end; 

772 

48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

773 
end; 