author | wenzelm |
Sat, 18 Jul 2015 21:44:18 +0200 | |
changeset 60757 | c09598a97436 |
parent 60752 | b48830b670a1 |
child 60777 | ee811a49c8f6 |
permissions | -rw-r--r-- |
55061 | 1 |
(* Title: HOL/Tools/BNF/bnf_gfp_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 |
Author: Jasmin Blanchette, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
Tactics for the codatatype construction. |
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 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
signature BNF_GFP_TACTICS = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
11 |
sig |
55197 | 12 |
val mk_bis_Gr_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm list -> tactic |
51798 | 13 |
val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic |
55197 | 14 |
val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic |
60728 | 15 |
val mk_bis_converse_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic |
16 |
val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list -> |
|
51798 | 17 |
thm list list -> tactic |
55197 | 18 |
val mk_coalgT_tac: Proof.context -> int -> thm list -> thm list -> thm list list -> tactic |
60728 | 19 |
val mk_coalg_final_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list list -> |
20 |
thm list list -> tactic |
|
21 |
val mk_coalg_set_tac: Proof.context -> thm -> tactic |
|
55197 | 22 |
val mk_coind_wit_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic |
60728 | 23 |
val mk_col_bd_tac: Proof.context -> int -> int -> cterm option list -> thm list -> thm list -> |
24 |
thm -> thm -> thm list list -> tactic |
|
55197 | 25 |
val mk_col_natural_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list -> |
26 |
thm list list -> tactic |
|
60728 | 27 |
val mk_congruent_str_final_tac: Proof.context -> int -> thm -> thm -> thm -> thm list -> tactic |
55197 | 28 |
val mk_corec_tac: Proof.context -> int -> thm list -> thm -> thm -> thm list -> tactic |
29 |
val mk_corec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic |
|
60728 | 30 |
val mk_dtor_coinduct_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic |
58445 | 31 |
val mk_dtor_corec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list -> |
32 |
thm list -> tactic |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
33 |
val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list -> |
51798 | 34 |
thm -> thm -> thm list -> thm list -> thm list list -> tactic |
55197 | 35 |
val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic |
60728 | 36 |
val mk_equiv_lsbis_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> tactic |
56179 | 37 |
val mk_Jset_minimal_tac: Proof.context -> int -> thm -> tactic |
56113 | 38 |
val mk_col_minimal_tac: Proof.context -> int -> cterm option list -> thm list -> thm list -> |
55197 | 39 |
tactic |
60728 | 40 |
val mk_incl_lsbis_tac: Proof.context -> int -> int -> thm -> tactic |
41 |
val mk_length_Lev'_tac: Proof.context -> thm -> tactic |
|
51798 | 42 |
val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic |
60728 | 43 |
val mk_map_comp0_tac: Proof.context -> thm list -> thm list -> thm -> tactic |
51798 | 44 |
val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list -> |
55644 | 45 |
thm list list -> thm list list -> thm list list list -> thm list -> tactic |
60728 | 46 |
val mk_map_id0_tac: Proof.context -> thm list -> thm -> thm -> tactic |
47 |
val mk_map_tac: Proof.context -> int -> int -> thm -> thm -> thm -> thm -> tactic |
|
55197 | 48 |
val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic |
49 |
val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic |
|
55541
fd9ea8ae28f6
syntactic simplifications of internal (co)datatype constructions
traytel
parents:
55414
diff
changeset
|
50 |
val mk_mor_Rep_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list -> |
55197 | 51 |
thm list -> thm list -> tactic |
60728 | 52 |
val mk_mor_T_final_tac: Proof.context -> thm -> thm list -> thm list -> tactic |
53 |
val mk_mor_UNIV_tac: Proof.context -> thm list -> thm -> tactic |
|
55197 | 54 |
val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list -> |
55 |
thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> |
|
55577
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
56 |
thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> |
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
57 |
thm list list -> thm list -> thm list -> tactic |
60728 | 58 |
val mk_mor_case_sum_tac: Proof.context -> 'a list -> 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_comp_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic |
60728 | 60 |
val mk_mor_elim_tac: Proof.context -> thm -> tactic |
61 |
val mk_mor_col_tac: Proof.context -> int -> int -> cterm option list -> int -> thm list -> |
|
62 |
thm list -> thm list -> thm list list -> thm list list -> tactic |
|
63 |
val mk_mor_incl_tac: Proof.context -> thm -> thm list -> tactic |
|
64 |
val mk_mor_str_tac: Proof.context -> 'a list -> thm -> tactic |
|
65 |
val mk_mor_unfold_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list -> |
|
66 |
thm list -> thm list -> thm list -> tactic |
|
67 |
val mk_raw_coind_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> |
|
68 |
thm -> thm list -> thm list -> thm list -> thm -> thm list -> tactic |
|
55197 | 69 |
val mk_rel_coinduct_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list -> |
70 |
thm list -> thm list -> tactic |
|
55644 | 71 |
val mk_rel_coinduct_coind_tac: Proof.context -> bool -> int -> thm -> int list -> thm list -> |
72 |
thm list -> thm list -> thm list list -> thm list -> thm list -> thm list -> tactic |
|
55197 | 73 |
val mk_rel_coinduct_ind_tac: Proof.context -> int -> int list -> thm list -> thm list list -> |
74 |
int -> thm -> tactic |
|
60728 | 75 |
val mk_rv_last_tac: Proof.context -> ctyp option list -> cterm option list -> thm list -> |
76 |
thm list -> tactic |
|
51798 | 77 |
val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic |
78 |
val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list -> |
|
79 |
thm list -> thm list list -> tactic |
|
60728 | 80 |
val mk_set_bd_tac: Proof.context -> thm -> thm -> tactic |
81 |
val mk_set_Jset_incl_Jset_tac: Proof.context -> int -> thm -> int -> tactic |
|
51798 | 82 |
val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> |
83 |
thm list -> thm list -> thm list list -> thm list list -> tactic |
|
60728 | 84 |
val mk_set_incl_Jset_tac: Proof.context -> thm -> tactic |
85 |
val mk_set_ge_tac: Proof.context -> int -> thm -> thm list -> tactic |
|
86 |
val mk_set_le_tac: Proof.context -> int -> thm -> thm list -> thm list list -> tactic |
|
87 |
val mk_set_map0_tac: Proof.context -> thm -> tactic |
|
88 |
val mk_unfold_unique_mor_tac: Proof.context -> thm list -> thm -> thm -> thm list -> tactic |
|
55197 | 89 |
val mk_unfold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic |
90 |
val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list -> tactic |
|
60728 | 91 |
val mk_le_rel_OO_tac: Proof.context -> thm -> 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
|
92 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
93 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
94 |
structure BNF_GFP_Tactics : BNF_GFP_TACTICS = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
95 |
struct |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
96 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
97 |
open BNF_Tactics |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
98 |
open BNF_Util |
51850
106afdf5806c
renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
blanchet
parents:
51798
diff
changeset
|
99 |
open BNF_FP_Util |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
100 |
open BNF_GFP_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
101 |
|
55644 | 102 |
val fst_convol_fun_cong_sym = @{thm fst_convol[unfolded convol_def]} RS fun_cong RS sym; |
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
103 |
val list_inject_iffD1 = @{thm list.inject[THEN iffD1]}; |
49305 | 104 |
val nat_induct = @{thm nat_induct}; |
105 |
val o_apply_trans_sym = o_apply RS trans RS sym; |
|
106 |
val ord_eq_le_trans = @{thm ord_eq_le_trans}; |
|
107 |
val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans}; |
|
55644 | 108 |
val snd_convol_fun_cong_sym = @{thm snd_convol[unfolded convol_def]} RS fun_cong RS sym; |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57806
diff
changeset
|
109 |
val sum_case_cong_weak = @{thm sum.case_cong_weak}; |
49305 | 110 |
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
|
111 |
val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]}; |
58b87aa4dc3b
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents:
52635
diff
changeset
|
112 |
val rev_bspec = Drule.rotate_prems 1 bspec; |
52749 | 113 |
val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]}; |
114 |
val converse_shift = @{thm converse_subset_swap} RS iffD1; |
|
49305 | 115 |
|
60728 | 116 |
fun mk_coalg_set_tac ctxt coalg_def = |
117 |
dtac ctxt (coalg_def RS iffD1) 1 THEN |
|
118 |
REPEAT_DETERM (etac ctxt conjE 1) THEN |
|
60752 | 119 |
EVERY' [dtac ctxt rev_bspec, assume_tac ctxt] 1 THEN |
60757 | 120 |
REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) 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
|
121 |
|
60728 | 122 |
fun mk_mor_elim_tac ctxt mor_def = |
123 |
(dtac ctxt (mor_def RS iffD1) THEN' |
|
124 |
REPEAT o etac ctxt conjE THEN' |
|
125 |
TRY o rtac ctxt @{thm image_subsetI} THEN' |
|
126 |
etac ctxt bspec THEN' |
|
60752 | 127 |
assume_tac ctxt) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
128 |
|
60728 | 129 |
fun mk_mor_incl_tac ctxt mor_def map_ids = |
130 |
(rtac ctxt (mor_def RS iffD2) THEN' |
|
131 |
rtac ctxt conjI THEN' |
|
132 |
CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})])) |
|
56114 | 133 |
map_ids THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
134 |
CONJ_WRAP' (fn thm => |
60728 | 135 |
(EVERY' [rtac ctxt ballI, rtac ctxt (thm RS trans), rtac ctxt sym, rtac ctxt (id_apply RS arg_cong)])) map_ids) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
136 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
137 |
fun mk_mor_comp_tac ctxt mor_def mor_images morEs map_comp_ids = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
138 |
let |
60728 | 139 |
fun fbetw_tac image = EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}), etac ctxt image, |
60752 | 140 |
etac ctxt image, assume_tac ctxt]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
141 |
fun mor_tac ((mor_image, morE), map_comp_id) = |
60728 | 142 |
EVERY' [rtac ctxt ballI, stac ctxt o_apply, rtac ctxt trans, rtac ctxt (map_comp_id RS sym), rtac ctxt trans, |
60752 | 143 |
etac ctxt (morE RS arg_cong), assume_tac ctxt, etac ctxt morE, |
144 |
etac ctxt mor_image, assume_tac ctxt]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
145 |
in |
60728 | 146 |
(rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
147 |
CONJ_WRAP' fbetw_tac mor_images THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
148 |
CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
149 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
150 |
|
60728 | 151 |
fun mk_mor_UNIV_tac ctxt morEs mor_def = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
152 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
153 |
val n = length morEs; |
60728 | 154 |
fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE, |
155 |
rtac ctxt UNIV_I, 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
|
156 |
in |
60728 | 157 |
EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs, |
158 |
rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) morEs, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
159 |
CONJ_WRAP' (fn i => |
60728 | 160 |
EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt ballI, etac ctxt @{thm comp_eq_dest}]) (1 upto n)] 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
161 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
162 |
|
60728 | 163 |
fun mk_mor_str_tac ctxt ks mor_UNIV = |
164 |
(rtac ctxt (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (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
|
165 |
|
60728 | 166 |
fun mk_mor_case_sum_tac ctxt ks mor_UNIV = |
167 |
(rtac ctxt (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac ctxt @{thm case_sum_o_inj(1)[symmetric]})) ks) 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
168 |
|
60728 | 169 |
fun mk_set_incl_Jset_tac ctxt rec_Suc = |
170 |
EVERY' (map (rtac ctxt) [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, sym, |
|
56113 | 171 |
rec_Suc]) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
172 |
|
60728 | 173 |
fun mk_set_Jset_incl_Jset_tac ctxt n rec_Suc i = |
174 |
EVERY' (map (rtac ctxt) [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, |
|
60752 | 175 |
rec_Suc, UnI2, mk_UnIN n i] @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
176 |
|
56113 | 177 |
fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs = |
60728 | 178 |
EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct), |
179 |
REPEAT_DETERM o rtac ctxt allI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
180 |
CONJ_WRAP' (fn thm => EVERY' |
60728 | 181 |
[rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm empty_subsetI}]) rec_0s, |
182 |
REPEAT_DETERM o rtac ctxt allI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
183 |
CONJ_WRAP' (fn rec_Suc => EVERY' |
60728 | 184 |
[rtac ctxt ord_eq_le_trans, rtac ctxt rec_Suc, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
185 |
if m = 0 then K all_tac |
60728 | 186 |
else (rtac ctxt @{thm Un_least} THEN' Goal.assume_rule_tac ctxt), |
187 |
CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least})) |
|
188 |
(K (EVERY' [rtac ctxt @{thm UN_least}, REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], |
|
60752 | 189 |
rtac ctxt subset_trans, assume_tac ctxt, Goal.assume_rule_tac ctxt])) rec_0s]) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
190 |
rec_Sucs] 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
191 |
|
56179 | 192 |
fun mk_Jset_minimal_tac ctxt n col_minimal = |
60728 | 193 |
(CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm UN_least}, rtac ctxt rev_mp, rtac ctxt col_minimal, |
194 |
EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac ctxt impI, |
|
60752 | 195 |
REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], assume_tac ctxt])) (1 upto n)) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
196 |
|
60728 | 197 |
fun mk_mor_col_tac ctxt m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss = |
198 |
EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct), |
|
199 |
REPEAT_DETERM o rtac ctxt allI, |
|
200 |
CONJ_WRAP' (fn thm => EVERY' (map (rtac ctxt) [impI, thm RS trans, thm RS sym])) rec_0s, |
|
201 |
REPEAT_DETERM o rtac ctxt allI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
202 |
CONJ_WRAP' |
53289 | 203 |
(fn (rec_Suc, (morE, ((passive_set_map0s, active_set_map0s), coalg_sets))) => |
60728 | 204 |
EVERY' [rtac ctxt impI, rtac ctxt (rec_Suc RS trans), rtac ctxt (rec_Suc RS trans RS sym), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
205 |
if m = 0 then K all_tac |
60728 | 206 |
else EVERY' [rtac ctxt Un_cong, rtac ctxt @{thm box_equals}, |
207 |
rtac ctxt (nth passive_set_map0s (j - 1) RS sym), |
|
60752 | 208 |
rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt (morE RS arg_cong), |
209 |
assume_tac ctxt], |
|
60728 | 210 |
CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 Un_cong)) |
53289 | 211 |
(fn (i, (set_map0, coalg_set)) => |
60728 | 212 |
EVERY' [rtac ctxt sym, rtac ctxt trans, rtac ctxt (refl RSN (2, @{thm SUP_cong})), |
60752 | 213 |
etac ctxt (morE RS sym RS arg_cong RS trans), assume_tac ctxt, rtac ctxt set_map0, |
60728 | 214 |
rtac ctxt (@{thm UN_simps(10)} RS trans), rtac ctxt (refl RS @{thm SUP_cong}), |
60752 | 215 |
ftac ctxt coalg_set, assume_tac ctxt, dtac ctxt set_mp, assume_tac ctxt, |
216 |
rtac ctxt mp, rtac ctxt (mk_conjunctN n i), |
|
217 |
REPEAT_DETERM o etac ctxt allE, assume_tac ctxt, assume_tac ctxt]) |
|
53289 | 218 |
(rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))]) |
219 |
(rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 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_bis_rel_tac ctxt m bis_def in_rels map_comp0s map_cong0s set_map0ss = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
222 |
let |
56017 | 223 |
val n = length in_rels; |
224 |
val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ in_rels); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
225 |
|
56017 | 226 |
fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) = |
60728 | 227 |
EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, dtac ctxt (mk_conjunctN n i), |
60752 | 228 |
etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, etac ctxt bexE, |
60757 | 229 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], |
60728 | 230 |
rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI), |
231 |
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt trans, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt map_cong0, |
|
232 |
REPEAT_DETERM_N m o rtac ctxt thm, REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong), |
|
60752 | 233 |
assume_tac ctxt]) |
56017 | 234 |
@{thms fst_diag_id snd_diag_id}, |
60728 | 235 |
rtac ctxt CollectI, |
56017 | 236 |
CONJ_WRAP' (fn (i, thm) => |
237 |
if i <= m |
|
60728 | 238 |
then EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans, |
239 |
etac ctxt @{thm image_mono}, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, |
|
240 |
rtac ctxt @{thm case_prodI}, rtac ctxt refl] |
|
241 |
else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm, |
|
242 |
rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt @{thm Collect_split_in_rel_leI}]) |
|
56017 | 243 |
(1 upto (m + n) ~~ set_map0s)]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
244 |
|
56017 | 245 |
fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) = |
60728 | 246 |
EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, |
60752 | 247 |
etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, |
60728 | 248 |
dtac ctxt (in_rel RS @{thm iffD1}), |
60757 | 249 |
REPEAT_DETERM o eresolve_tac ctxt ([CollectE, conjE, exE] @ |
56017 | 250 |
@{thms CollectE Collect_split_in_rel_leE}), |
60728 | 251 |
rtac ctxt bexI, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0, |
252 |
REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong), |
|
253 |
REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong), |
|
60752 | 254 |
assume_tac ctxt, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0, |
60728 | 255 |
REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong), |
256 |
REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong), |
|
257 |
rtac ctxt trans, rtac ctxt map_cong0, |
|
60752 | 258 |
REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_splitD}, etac ctxt set_mp, assume_tac ctxt], |
60728 | 259 |
REPEAT_DETERM_N n o rtac ctxt refl, |
60752 | 260 |
assume_tac ctxt, rtac ctxt CollectI, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
261 |
CONJ_WRAP' (fn (i, thm) => |
60728 | 262 |
if i <= m then rtac ctxt subset_UNIV |
263 |
else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm, |
|
60752 | 264 |
rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt]) |
53289 | 265 |
(1 upto (m + n) ~~ set_map0s)]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
266 |
in |
60728 | 267 |
EVERY' [rtac ctxt (bis_def RS trans), |
268 |
rtac ctxt iffI, etac ctxt conjE, etac ctxt conjI, CONJ_WRAP' mk_if_tac thms, |
|
269 |
etac ctxt conjE, etac ctxt conjI, CONJ_WRAP' mk_only_if_tac thms] 1 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
270 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
271 |
|
60728 | 272 |
fun mk_bis_converse_tac ctxt m bis_rel rel_congs rel_converseps = |
273 |
EVERY' [rtac ctxt (bis_rel RS iffD2), dtac ctxt (bis_rel RS iffD1), |
|
274 |
REPEAT_DETERM o etac ctxt conjE, rtac ctxt conjI, |
|
275 |
CONJ_WRAP' (K (EVERY' [rtac ctxt converse_shift, etac ctxt subset_trans, |
|
276 |
rtac ctxt equalityD2, rtac ctxt @{thm converse_Times}])) rel_congs, |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
277 |
CONJ_WRAP' (fn (rel_cong, rel_conversep) => |
60728 | 278 |
EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, |
279 |
rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}), |
|
280 |
REPEAT_DETERM_N m o rtac ctxt @{thm conversep_eq}, |
|
281 |
REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm conversep_in_rel}, |
|
282 |
rtac ctxt (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}), |
|
283 |
REPEAT_DETERM o etac ctxt allE, |
|
284 |
rtac ctxt @{thm conversepI}, etac ctxt mp, etac ctxt @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
285 |
|
57726 | 286 |
fun mk_bis_O_tac ctxt m bis_rel rel_congs le_rel_OOs = |
60728 | 287 |
EVERY' [rtac ctxt (bis_rel RS iffD2), REPEAT_DETERM o dtac ctxt (bis_rel RS iffD1), |
288 |
REPEAT_DETERM o etac ctxt conjE, rtac ctxt conjI, |
|
60752 | 289 |
CONJ_WRAP' (K (EVERY' [etac ctxt @{thm relcomp_subset_Sigma}, assume_tac ctxt])) rel_congs, |
57726 | 290 |
CONJ_WRAP' (fn (rel_cong, le_rel_OO) => |
60728 | 291 |
EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, |
292 |
rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}), |
|
293 |
REPEAT_DETERM_N m o rtac ctxt @{thm eq_OO}, |
|
294 |
REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm relcompp_in_rel}, |
|
295 |
rtac ctxt (le_rel_OO RS @{thm predicate2D}), |
|
296 |
etac ctxt @{thm relcompE}, |
|
297 |
REPEAT_DETERM o dtac ctxt prod_injectD, |
|
298 |
etac ctxt conjE, hyp_subst_tac ctxt, |
|
299 |
REPEAT_DETERM o etac ctxt allE, rtac ctxt @{thm relcomppI}, |
|
60752 | 300 |
etac ctxt mp, assume_tac ctxt, etac ctxt mp, assume_tac ctxt]) (rel_congs ~~ le_rel_OOs)] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
301 |
|
55197 | 302 |
fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins = |
55541
fd9ea8ae28f6
syntactic simplifications of internal (co)datatype constructions
traytel
parents:
55414
diff
changeset
|
303 |
unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN |
60728 | 304 |
EVERY' [rtac ctxt conjI, |
305 |
CONJ_WRAP' (fn thm => rtac ctxt (@{thm Gr_incl} RS iffD2) THEN' etac ctxt thm) mor_images, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
306 |
CONJ_WRAP' (fn (coalg_in, morE) => |
60728 | 307 |
EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt @{thm GrpI}, etac ctxt (morE RS trans), |
308 |
etac ctxt @{thm GrD1}, etac ctxt (@{thm GrD2} RS arg_cong), etac ctxt coalg_in, etac ctxt @{thm GrD1}]) |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
309 |
(coalg_ins ~~ morEs)] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
310 |
|
55197 | 311 |
fun mk_bis_Union_tac ctxt bis_def in_monos = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
312 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
313 |
val n = length in_monos; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
314 |
val ks = 1 upto n; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
315 |
in |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49501
diff
changeset
|
316 |
unfold_thms_tac ctxt [bis_def] THEN |
60728 | 317 |
EVERY' [rtac ctxt conjI, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
318 |
CONJ_WRAP' (fn i => |
60752 | 319 |
EVERY' [rtac ctxt @{thm UN_least}, dtac ctxt bspec, assume_tac ctxt, |
60728 | 320 |
dtac ctxt conjunct1, etac ctxt (mk_conjunctN n i)]) ks, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
321 |
CONJ_WRAP' (fn (i, in_mono) => |
60752 | 322 |
EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, etac ctxt @{thm UN_E}, |
323 |
dtac ctxt bspec, assume_tac ctxt, |
|
60728 | 324 |
dtac ctxt conjunct2, dtac ctxt (mk_conjunctN n i), etac ctxt allE, etac ctxt allE, dtac ctxt mp, |
60752 | 325 |
assume_tac ctxt, etac ctxt bexE, rtac ctxt bexI, assume_tac ctxt, rtac ctxt in_mono, |
60728 | 326 |
REPEAT_DETERM_N n o etac ctxt @{thm SUP_upper2[OF _ subset_refl]}, |
60752 | 327 |
assume_tac ctxt]) (ks ~~ in_monos)] 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
328 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
329 |
|
51798 | 330 |
fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
331 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
332 |
val n = length lsbis_defs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
333 |
in |
60728 | 334 |
EVERY' [rtac ctxt (Thm.permute_prems 0 1 bis_cong), EVERY' (map (rtac ctxt) lsbis_defs), |
335 |
rtac ctxt bis_Union, rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, exE], |
|
336 |
hyp_subst_tac ctxt, etac ctxt bis_cong, EVERY' (map (rtac ctxt o mk_nth_conv n) (1 upto n))] 1 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
337 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
338 |
|
60728 | 339 |
fun mk_incl_lsbis_tac ctxt n i lsbis_def = |
340 |
EVERY' [rtac ctxt @{thm xt1(3)}, rtac ctxt lsbis_def, rtac ctxt @{thm SUP_upper2}, rtac ctxt CollectI, |
|
60752 | 341 |
REPEAT_DETERM_N n o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt, |
342 |
rtac ctxt equalityD2, rtac ctxt (mk_nth_conv n i)] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
343 |
|
60728 | 344 |
fun mk_equiv_lsbis_tac ctxt sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O = |
345 |
EVERY' [rtac ctxt (@{thm equiv_def} RS iffD2), |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
346 |
|
60728 | 347 |
rtac ctxt conjI, rtac ctxt (@{thm refl_on_def} RS iffD2), |
348 |
rtac ctxt conjI, rtac ctxt lsbis_incl, rtac ctxt ballI, rtac ctxt set_mp, |
|
60752 | 349 |
rtac ctxt incl_lsbis, rtac ctxt bis_Id_on, assume_tac ctxt, etac ctxt @{thm Id_onI}, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
350 |
|
60728 | 351 |
rtac ctxt conjI, rtac ctxt (@{thm sym_def} RS iffD2), |
352 |
rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt set_mp, |
|
353 |
rtac ctxt incl_lsbis, rtac ctxt bis_converse, rtac ctxt sbis_lsbis, etac ctxt @{thm converseI}, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
354 |
|
60728 | 355 |
rtac ctxt (@{thm trans_def} RS iffD2), |
356 |
rtac ctxt allI, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt impI, rtac ctxt set_mp, |
|
357 |
rtac ctxt incl_lsbis, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt sbis_lsbis, |
|
60752 | 358 |
etac ctxt @{thm relcompI}, assume_tac ctxt] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
359 |
|
55197 | 360 |
fun mk_coalgT_tac ctxt m defs strT_defs set_map0ss = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
361 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
362 |
val n = length strT_defs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
363 |
val ks = 1 upto n; |
55541
fd9ea8ae28f6
syntactic simplifications of internal (co)datatype constructions
traytel
parents:
55414
diff
changeset
|
364 |
fun coalg_tac (i, (active_sets, def)) = |
60728 | 365 |
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], |
366 |
hyp_subst_tac ctxt, rtac ctxt (def RS trans RS @{thm ssubst_mem}), etac ctxt (arg_cong RS trans), |
|
367 |
rtac ctxt (mk_sum_caseN n i), rtac ctxt CollectI, |
|
368 |
REPEAT_DETERM_N m o EVERY' [rtac ctxt conjI, rtac ctxt subset_UNIV], |
|
369 |
CONJ_WRAP' (fn (i, thm) => EVERY' [rtac ctxt (thm RS ord_eq_le_trans), |
|
370 |
rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt exI, rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, |
|
371 |
rtac ctxt conjI, |
|
372 |
rtac ctxt conjI, etac ctxt @{thm empty_Shift}, dtac ctxt set_rev_mp, |
|
373 |
etac ctxt equalityD1, etac ctxt CollectD, |
|
374 |
rtac ctxt ballI, |
|
375 |
CONJ_WRAP' (fn i => EVERY' [rtac ctxt ballI, etac ctxt CollectE, dtac ctxt @{thm ShiftD}, |
|
60752 | 376 |
dtac ctxt bspec, etac ctxt thin_rl, assume_tac ctxt, dtac ctxt (mk_conjunctN n i), |
60728 | 377 |
dtac ctxt bspec, rtac ctxt CollectI, etac ctxt @{thm set_mp[OF equalityD1[OF Succ_Shift]]}, |
378 |
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI, |
|
379 |
rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans), |
|
60752 | 380 |
rtac ctxt (@{thm append_Cons} RS sym RS arg_cong RS trans), assume_tac ctxt, |
60728 | 381 |
CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong}, |
382 |
rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift}, |
|
383 |
rtac ctxt (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks, |
|
60752 | 384 |
dtac ctxt bspec, assume_tac ctxt, dtac ctxt (mk_conjunctN n i), dtac ctxt bspec, |
385 |
etac ctxt @{thm set_mp[OF equalityD1]}, assume_tac ctxt, |
|
60728 | 386 |
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI, |
387 |
rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans), |
|
388 |
etac ctxt (@{thm append_Nil} RS sym RS arg_cong RS trans), |
|
60752 | 389 |
REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt), |
60728 | 390 |
CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong}, |
391 |
rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift}, |
|
392 |
rtac ctxt (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
393 |
in |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49501
diff
changeset
|
394 |
unfold_thms_tac ctxt defs THEN |
55541
fd9ea8ae28f6
syntactic simplifications of internal (co)datatype constructions
traytel
parents:
55414
diff
changeset
|
395 |
CONJ_WRAP' coalg_tac (ks ~~ (map (drop m) set_map0ss ~~ strT_defs)) 1 |
48975
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 |
|
51798 | 398 |
fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs = |
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 Lev_0s; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
401 |
val ks = n downto 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
402 |
in |
60728 | 403 |
EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct), |
404 |
REPEAT_DETERM o rtac ctxt allI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
405 |
CONJ_WRAP' (fn Lev_0 => |
60728 | 406 |
EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp), |
407 |
etac ctxt @{thm singletonE}, etac ctxt ssubst, rtac ctxt @{thm list.size(3)}]) Lev_0s, |
|
408 |
REPEAT_DETERM o rtac ctxt allI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
409 |
CONJ_WRAP' (fn Lev_Suc => |
60728 | 410 |
EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp), |
411 |
CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) |
|
51798 | 412 |
(fn i => |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
413 |
EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt, |
60728 | 414 |
rtac ctxt trans, rtac ctxt @{thm length_Cons}, rtac ctxt @{thm arg_cong[of _ _ Suc]}, |
60752 | 415 |
REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i), |
416 |
etac ctxt mp, assume_tac ctxt]) ks]) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
417 |
Lev_Sucs] 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
418 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
419 |
|
60728 | 420 |
fun mk_length_Lev'_tac ctxt length_Lev = |
60752 | 421 |
EVERY' [ftac ctxt length_Lev, etac ctxt ssubst, assume_tac ctxt] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
422 |
|
60728 | 423 |
fun mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
424 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
425 |
val n = length rv_Nils; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
426 |
val ks = 1 upto n; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
427 |
in |
60728 | 428 |
EVERY' [rtac ctxt (Drule.instantiate' cTs cts @{thm list.induct}), |
429 |
REPEAT_DETERM o rtac ctxt allI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
430 |
CONJ_WRAP' (fn rv_Cons => |
60728 | 431 |
CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac ctxt exI, |
432 |
rtac ctxt (@{thm append_Nil} RS arg_cong RS trans), |
|
433 |
rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS trans), rtac ctxt rv_Nil])) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
434 |
(ks ~~ rv_Nils)) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
435 |
rv_Conss, |
60728 | 436 |
REPEAT_DETERM o rtac ctxt allI, rtac ctxt (mk_sumEN n), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
437 |
EVERY' (map (fn i => |
60728 | 438 |
CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i), |
439 |
CONJ_WRAP' (fn i' => EVERY' [dtac ctxt (mk_conjunctN n i'), etac ctxt exE, rtac ctxt exI, |
|
440 |
rtac ctxt (@{thm append_Cons} RS arg_cong RS trans), rtac ctxt (rv_Cons RS trans), |
|
441 |
if n = 1 then K all_tac else etac ctxt (sum_case_cong_weak RS trans), |
|
60752 | 442 |
rtac ctxt (mk_sum_caseN n i RS trans), assume_tac ctxt]) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
443 |
ks]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
444 |
rv_Conss) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
445 |
ks)] 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
446 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
447 |
|
51798 | 448 |
fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss = |
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 |
val n = length Lev_0s; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
451 |
val ks = 1 upto n; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
452 |
in |
60728 | 453 |
EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct), |
454 |
REPEAT_DETERM o rtac ctxt allI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
455 |
CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) => |
60728 | 456 |
EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp), |
457 |
etac ctxt @{thm singletonE}, hyp_subst_tac ctxt, |
|
458 |
CONJ_WRAP' (fn i' => rtac ctxt impI THEN' dtac ctxt (sym RS trans) THEN' rtac ctxt rv_Nil THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
459 |
(if i = i' |
60728 | 460 |
then EVERY' [dtac ctxt (mk_InN_inject n i), hyp_subst_tac ctxt, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
461 |
CONJ_WRAP' (fn (i'', Lev_0'') => |
60728 | 462 |
EVERY' [rtac ctxt impI, rtac ctxt @{thm ssubst_mem[OF append_Nil]}, |
463 |
rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), rtac ctxt (mk_UnIN n i''), |
|
464 |
rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, |
|
465 |
etac ctxt conjI, rtac ctxt (Lev_0'' RS equalityD2 RS set_mp), |
|
466 |
rtac ctxt @{thm singletonI}]) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
467 |
(ks ~~ Lev_0s)] |
60728 | 468 |
else etac ctxt (mk_InN_not_InM i' i RS notE))) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
469 |
ks]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
470 |
((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils), |
60728 | 471 |
REPEAT_DETERM o rtac ctxt allI, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
472 |
CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) => |
60728 | 473 |
EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp), |
474 |
CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
475 |
(fn (i, from_to_sbd) => |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
476 |
EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt, |
60728 | 477 |
CONJ_WRAP' (fn i' => rtac ctxt impI THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
478 |
CONJ_WRAP' (fn i'' => |
60728 | 479 |
EVERY' [rtac ctxt impI, rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), |
480 |
rtac ctxt @{thm ssubst_mem[OF append_Cons]}, rtac ctxt (mk_UnIN n i), |
|
481 |
rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, |
|
60752 | 482 |
rtac ctxt conjI, assume_tac ctxt, dtac ctxt (sym RS trans RS sym), |
60728 | 483 |
rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS trans), |
484 |
etac ctxt (from_to_sbd RS arg_cong), REPEAT_DETERM o etac ctxt allE, |
|
60752 | 485 |
dtac ctxt (mk_conjunctN n i), dtac ctxt mp, assume_tac ctxt, |
486 |
dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, assume_tac ctxt, |
|
487 |
dtac ctxt (mk_conjunctN n i''), etac ctxt mp, assume_tac ctxt]) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
488 |
ks) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
489 |
ks]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
490 |
(rev (ks ~~ from_to_sbds))]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
491 |
((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
492 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
493 |
|
51798 | 494 |
fun mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
495 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
496 |
val n = length Lev_0s; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
497 |
val ks = 1 upto n; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
498 |
in |
60728 | 499 |
EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct), |
500 |
REPEAT_DETERM o rtac ctxt allI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
501 |
CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) => |
60728 | 502 |
EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp), |
503 |
etac ctxt @{thm singletonE}, hyp_subst_tac ctxt, |
|
504 |
CONJ_WRAP' (fn i' => rtac ctxt impI THEN' |
|
505 |
CONJ_WRAP' (fn i'' => rtac ctxt impI THEN' dtac ctxt (sym RS trans) THEN' rtac ctxt rv_Nil THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
506 |
(if i = i'' |
60728 | 507 |
then EVERY' [dtac ctxt @{thm ssubst_mem[OF sym[OF append_Nil]]}, |
508 |
dtac ctxt (Lev_Suc RS equalityD1 RS set_mp), dtac ctxt (mk_InN_inject n i), |
|
51798 | 509 |
hyp_subst_tac ctxt, |
60728 | 510 |
CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
511 |
(fn k => REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN' |
60728 | 512 |
dtac ctxt list_inject_iffD1 THEN' etac ctxt conjE THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
513 |
(if k = i' |
60728 | 514 |
then EVERY' [dtac ctxt (mk_InN_inject n k), hyp_subst_tac ctxt, etac ctxt imageI] |
515 |
else etac ctxt (mk_InN_not_InM i' k RS notE))) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
516 |
(rev ks)] |
60728 | 517 |
else etac ctxt (mk_InN_not_InM i'' i RS notE))) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
518 |
ks) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
519 |
ks]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
520 |
((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils), |
60728 | 521 |
REPEAT_DETERM o rtac ctxt allI, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
522 |
CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) => |
60728 | 523 |
EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp), |
524 |
CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
525 |
(fn (i, (from_to_sbd, to_sbd_inj)) => |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
526 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN' |
60728 | 527 |
CONJ_WRAP' (fn i' => rtac ctxt impI THEN' |
528 |
dtac ctxt @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN' |
|
529 |
dtac ctxt (Lev_Suc RS equalityD1 RS set_mp) THEN' |
|
530 |
CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) (fn k => |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
531 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN' |
60728 | 532 |
dtac ctxt list_inject_iffD1 THEN' etac ctxt conjE THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
533 |
(if k = i |
60728 | 534 |
then EVERY' [dtac ctxt (mk_InN_inject n i), |
535 |
dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)), |
|
60752 | 536 |
assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt] THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
537 |
CONJ_WRAP' (fn i'' => |
60728 | 538 |
EVERY' [rtac ctxt impI, dtac ctxt (sym RS trans), |
539 |
rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS arg_cong RS trans), |
|
540 |
etac ctxt (from_to_sbd RS arg_cong), |
|
541 |
REPEAT_DETERM o etac ctxt allE, |
|
60752 | 542 |
dtac ctxt (mk_conjunctN n i), dtac ctxt mp, assume_tac ctxt, |
543 |
dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, assume_tac ctxt, |
|
60728 | 544 |
dtac ctxt (mk_conjunctN n i''), etac ctxt mp, etac ctxt sym]) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
545 |
ks |
60728 | 546 |
else etac ctxt (mk_InN_not_InM i k RS notE))) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
547 |
(rev ks)) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
548 |
ks) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
549 |
(rev (ks ~~ (from_to_sbds ~~ to_sbd_injs)))]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
550 |
((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
551 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
552 |
|
55577
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
553 |
fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs to_sbd_injss |
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
554 |
from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss length_Levs length_Lev's rv_lastss set_Levsss |
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
555 |
set_image_Levsss set_map0ss map_comp_ids map_cong0s = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
556 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
557 |
val n = length beh_defs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
558 |
val ks = 1 upto n; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
559 |
|
55577
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
560 |
fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, ((length_Lev, length_Lev'), |
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
561 |
(rv_lasts, (set_map0s, (set_Levss, set_image_Levss))))))))) = |
60728 | 562 |
EVERY' [rtac ctxt ballI, rtac ctxt (carT_def RS equalityD2 RS set_mp), |
563 |
rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, rtac ctxt conjI, |
|
564 |
rtac ctxt conjI, |
|
565 |
rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, rtac ctxt (Lev_0 RS equalityD2 RS set_mp), |
|
566 |
rtac ctxt @{thm singletonI}, |
|
55577
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
567 |
(**) |
60728 | 568 |
rtac ctxt ballI, etac ctxt @{thm UN_E}, |
53289 | 569 |
CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s, |
55541
fd9ea8ae28f6
syntactic simplifications of internal (co)datatype constructions
traytel
parents:
55414
diff
changeset
|
570 |
(set_Levs, set_image_Levs))))) => |
60728 | 571 |
EVERY' [rtac ctxt ballI, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
572 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}], |
60728 | 573 |
rtac ctxt (rev_mp OF [rv_last, impI]), etac ctxt exE, rtac ctxt (isNode_def RS iffD2), |
574 |
rtac ctxt exI, rtac ctxt conjI, |
|
575 |
if n = 1 then rtac ctxt refl |
|
576 |
else etac ctxt (sum_case_cong_weak RS trans) THEN' rtac ctxt (mk_sum_caseN n i), |
|
53289 | 577 |
CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) => |
60728 | 578 |
EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI}, |
579 |
rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, etac ctxt set_Lev, |
|
60752 | 580 |
if n = 1 then rtac ctxt refl else assume_tac ctxt, assume_tac ctxt, rtac ctxt subsetI, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
581 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}], |
60728 | 582 |
REPEAT_DETERM_N 4 o etac ctxt thin_rl, |
583 |
rtac ctxt set_image_Lev, |
|
60752 | 584 |
assume_tac ctxt, dtac ctxt length_Lev, hyp_subst_tac ctxt, dtac ctxt length_Lev', |
60728 | 585 |
etac ctxt @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]}, |
60752 | 586 |
if n = 1 then rtac ctxt refl else assume_tac ctxt]) |
53289 | 587 |
(drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))]) |
588 |
(ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~ |
|
55541
fd9ea8ae28f6
syntactic simplifications of internal (co)datatype constructions
traytel
parents:
55414
diff
changeset
|
589 |
(set_Levss ~~ set_image_Levss))))), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
590 |
(*root isNode*) |
60728 | 591 |
rtac ctxt (isNode_def RS iffD2), rtac ctxt exI, rtac ctxt conjI, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
592 |
CONVERSION (Conv.top_conv |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
593 |
(K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt), |
60728 | 594 |
if n = 1 then rtac ctxt refl else rtac ctxt (mk_sum_caseN n i), |
53289 | 595 |
CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) => |
60728 | 596 |
EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI}, |
597 |
rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, rtac ctxt set_Lev, |
|
598 |
rtac ctxt (Lev_0 RS equalityD2 RS set_mp), rtac ctxt @{thm singletonI}, rtac ctxt rv_Nil, |
|
60752 | 599 |
assume_tac ctxt, rtac ctxt subsetI, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
600 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}], |
60728 | 601 |
rtac ctxt set_image_Lev, rtac ctxt (Lev_0 RS equalityD2 RS set_mp), |
602 |
rtac ctxt @{thm singletonI}, dtac ctxt length_Lev', |
|
603 |
etac ctxt @{thm set_mp[OF equalityD1[OF arg_cong[OF |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
604 |
trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]}, |
60728 | 605 |
rtac ctxt rv_Nil]) |
53289 | 606 |
(drop m set_map0s ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
607 |
|
55577
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
608 |
fun mor_tac (i, (strT_def, ((Lev_Suc, (rv_Nil, rv_Cons)), |
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
609 |
((map_comp_id, map_cong0), (length_Lev', (from_to_sbds, to_sbd_injs)))))) = |
60728 | 610 |
EVERY' [rtac ctxt ballI, rtac ctxt sym, rtac ctxt trans, rtac ctxt strT_def, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
611 |
CONVERSION (Conv.top_conv |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
612 |
(K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
613 |
if n = 1 then K all_tac |
60728 | 614 |
else (rtac ctxt (sum_case_cong_weak RS trans) THEN' |
615 |
rtac ctxt (mk_sum_caseN n i) THEN' rtac ctxt (mk_sum_caseN n i RS trans)), |
|
616 |
rtac ctxt (map_comp_id RS trans), rtac ctxt (map_cong0 OF replicate m refl), |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58446
diff
changeset
|
617 |
EVERY' (@{map 3} (fn i' => fn to_sbd_inj => fn from_to_sbd => |
60728 | 618 |
DETERM o EVERY' [rtac ctxt trans, rtac ctxt o_apply, rtac ctxt prod_injectI, rtac ctxt conjI, |
619 |
rtac ctxt trans, rtac ctxt @{thm Shift_def}, |
|
620 |
rtac ctxt equalityI, rtac ctxt subsetI, etac ctxt thin_rl, |
|
621 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm UN_E}], dtac ctxt length_Lev', dtac ctxt asm_rl, |
|
622 |
etac ctxt thin_rl, dtac ctxt @{thm set_rev_mp[OF _ equalityD1]}, |
|
623 |
rtac ctxt (@{thm length_Cons} RS arg_cong RS trans), rtac ctxt Lev_Suc, |
|
624 |
CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) (fn i'' => |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
625 |
EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], |
60728 | 626 |
dtac ctxt list_inject_iffD1, etac ctxt conjE, |
627 |
if i' = i'' then EVERY' [dtac ctxt (mk_InN_inject n i'), |
|
628 |
dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)), |
|
60752 | 629 |
assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt, etac ctxt @{thm UN_I[OF UNIV_I]}] |
60728 | 630 |
else etac ctxt (mk_InN_not_InM i' i'' RS notE)]) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
631 |
(rev ks), |
60728 | 632 |
rtac ctxt @{thm UN_least}, rtac ctxt subsetI, rtac ctxt CollectI, rtac ctxt @{thm UN_I[OF UNIV_I]}, |
633 |
rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), rtac ctxt (mk_UnIN n i'), rtac ctxt CollectI, |
|
60752 | 634 |
REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, etac ctxt conjI, assume_tac ctxt, |
60728 | 635 |
rtac ctxt trans, rtac ctxt @{thm shift_def}, rtac ctxt iffD2, rtac ctxt @{thm fun_eq_iff}, rtac ctxt allI, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
636 |
CONVERSION (Conv.top_conv |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
637 |
(K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
638 |
if n = 1 then K all_tac |
60728 | 639 |
else rtac ctxt sum_case_cong_weak THEN' rtac ctxt (mk_sum_caseN n i' RS trans), |
640 |
SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac ctxt refl]) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
641 |
ks to_sbd_injs from_to_sbds)]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
642 |
in |
60728 | 643 |
(rtac ctxt mor_cong THEN' |
644 |
EVERY' (map (fn thm => rtac ctxt (thm RS @{thm ext})) beh_defs) THEN' |
|
645 |
rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
646 |
CONJ_WRAP' fbetw_tac |
55577
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
647 |
(ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ ((length_Levs ~~ length_Lev's) ~~ |
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
648 |
(rv_lastss ~~ (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))) THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
649 |
CONJ_WRAP' mor_tac |
55577
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
650 |
(ks ~~ (strT_defs ~~ ((Lev_Sucs ~~ (rv_Nils ~~ rv_Conss)) ~~ |
a6c2379078c8
simplifications of internal codatatype construction
traytel
parents:
55541
diff
changeset
|
651 |
((map_comp_ids ~~ map_cong0s) ~~ |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
652 |
(length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
653 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
654 |
|
60728 | 655 |
fun mk_congruent_str_final_tac ctxt m lsbisE map_comp_id map_cong0 equiv_LSBISs = |
656 |
EVERY' [rtac ctxt @{thm congruentI}, dtac ctxt lsbisE, |
|
60757 | 657 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, bexE], rtac ctxt (o_apply RS trans), |
60728 | 658 |
etac ctxt (sym RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans), |
659 |
rtac ctxt (map_cong0 RS trans), REPEAT_DETERM_N m o rtac ctxt refl, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
660 |
EVERY' (map (fn equiv_LSBIS => |
60752 | 661 |
EVERY' [rtac ctxt @{thm equiv_proj}, rtac ctxt equiv_LSBIS, etac ctxt set_mp, assume_tac ctxt]) |
60728 | 662 |
equiv_LSBISs), rtac ctxt sym, rtac ctxt (o_apply RS trans), |
663 |
etac ctxt (sym RS arg_cong RS trans), rtac ctxt map_comp_id] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
664 |
|
60728 | 665 |
fun mk_coalg_final_tac ctxt m coalg_def congruent_str_finals equiv_LSBISs set_map0ss coalgT_setss = |
666 |
EVERY' [rtac ctxt (coalg_def RS iffD2), |
|
53289 | 667 |
CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) => |
60728 | 668 |
EVERY' [rtac ctxt @{thm univ_preserves}, rtac ctxt equiv_LSBIS, rtac ctxt congruent_str_final, |
669 |
rtac ctxt ballI, rtac ctxt @{thm ssubst_mem}, rtac ctxt o_apply, rtac ctxt CollectI, |
|
670 |
REPEAT_DETERM_N m o EVERY' [rtac ctxt conjI, rtac ctxt subset_UNIV], |
|
53289 | 671 |
CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) => |
60728 | 672 |
EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans), |
673 |
rtac ctxt @{thm image_subsetI}, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff}, |
|
674 |
rtac ctxt equiv_LSBIS, etac ctxt set_rev_mp, etac ctxt coalgT_set]) |
|
55541
fd9ea8ae28f6
syntactic simplifications of internal (co)datatype constructions
traytel
parents:
55414
diff
changeset
|
675 |
(equiv_LSBISs ~~ (drop m set_map0s ~~ coalgT_sets))]) |
53289 | 676 |
((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
677 |
|
60728 | 678 |
fun mk_mor_T_final_tac ctxt mor_def congruent_str_finals equiv_LSBISs = |
679 |
EVERY' [rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
680 |
CONJ_WRAP' (fn equiv_LSBIS => |
60752 | 681 |
EVERY' [rtac ctxt ballI, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff}, |
682 |
rtac ctxt equiv_LSBIS, assume_tac ctxt]) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
683 |
equiv_LSBISs, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
684 |
CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) => |
60728 | 685 |
EVERY' [rtac ctxt ballI, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm univ_commute}, rtac ctxt equiv_LSBIS, |
60752 | 686 |
rtac ctxt congruent_str_final, assume_tac ctxt, rtac ctxt o_apply]) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
687 |
(equiv_LSBISs ~~ congruent_str_finals)] 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
688 |
|
55541
fd9ea8ae28f6
syntactic simplifications of internal (co)datatype constructions
traytel
parents:
55414
diff
changeset
|
689 |
fun mk_mor_Rep_tac ctxt defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls = |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49501
diff
changeset
|
690 |
unfold_thms_tac ctxt defs THEN |
60728 | 691 |
EVERY' [rtac ctxt conjI, |
692 |
CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' rtac ctxt thm) Reps, |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
693 |
CONJ_WRAP' (fn (Rep, ((map_comp_id, map_cong0L), coalg_final_sets)) => |
60728 | 694 |
EVERY' [rtac ctxt ballI, rtac ctxt (map_comp_id RS trans), rtac ctxt map_cong0L, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
695 |
EVERY' (map2 (fn Abs_inverse => fn coalg_final_set => |
60728 | 696 |
EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt Abs_inverse, |
697 |
etac ctxt set_rev_mp, rtac ctxt coalg_final_set, rtac ctxt Rep]) |
|
55541
fd9ea8ae28f6
syntactic simplifications of internal (co)datatype constructions
traytel
parents:
55414
diff
changeset
|
698 |
Abs_inverses coalg_final_sets)]) |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
699 |
(Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
700 |
|
55197 | 701 |
fun mk_mor_Abs_tac ctxt defs Abs_inverses = |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49501
diff
changeset
|
702 |
unfold_thms_tac ctxt defs THEN |
60728 | 703 |
EVERY' [rtac ctxt conjI, |
704 |
CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses, |
|
705 |
CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' etac ctxt (thm RS arg_cong RS sym)) Abs_inverses] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
706 |
|
60728 | 707 |
fun mk_mor_unfold_tac ctxt m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s = |
708 |
EVERY' [rtac ctxt iffD2, rtac ctxt mor_UNIV, |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
709 |
CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) => |
60728 | 710 |
EVERY' [rtac ctxt @{thm ext}, rtac ctxt (o_apply RS trans RS sym), rtac ctxt (dtor_def RS trans), |
711 |
rtac ctxt (unfold_def RS arg_cong RS trans), rtac ctxt (Abs_inverse RS arg_cong RS trans), |
|
712 |
rtac ctxt (morE RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans), |
|
713 |
rtac ctxt (o_apply RS trans RS sym), rtac ctxt map_cong0, |
|
714 |
REPEAT_DETERM_N m o rtac ctxt refl, |
|
715 |
EVERY' (map (fn thm => rtac ctxt (thm RS trans) THEN' rtac ctxt (o_apply RS sym)) unfold_defs)]) |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
716 |
((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_cong0s)))] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
717 |
|
60728 | 718 |
fun mk_raw_coind_tac ctxt bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
719 |
sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
720 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
721 |
val n = length Rep_injects; |
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 rev_mp, ftac ctxt (bis_def RS iffD1), |
724 |
REPEAT_DETERM o etac ctxt conjE, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_converse, |
|
60752 | 725 |
rtac ctxt bis_Gr, rtac ctxt tcoalg, rtac ctxt mor_Rep, rtac ctxt bis_O, assume_tac ctxt, |
726 |
rtac ctxt bis_Gr, rtac ctxt tcoalg, |
|
60728 | 727 |
rtac ctxt mor_Rep, REPEAT_DETERM_N n o etac ctxt @{thm relImage_Gr}, |
728 |
rtac ctxt impI, rtac ctxt rev_mp, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_Gr, rtac ctxt coalgT, |
|
729 |
rtac ctxt mor_T_final, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt bis_converse, rtac ctxt bis_Gr, rtac ctxt coalgT, |
|
730 |
rtac ctxt mor_T_final, EVERY' (map (fn thm => rtac ctxt (thm RS @{thm relInvImage_Gr})) lsbis_incls), |
|
731 |
rtac ctxt impI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
732 |
CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) => |
60728 | 733 |
EVERY' [rtac ctxt subset_trans, rtac ctxt @{thm relInvImage_UNIV_relImage}, rtac ctxt subset_trans, |
734 |
rtac ctxt @{thm relInvImage_mono}, rtac ctxt subset_trans, etac ctxt incl_lsbis, |
|
735 |
rtac ctxt ord_eq_le_trans, rtac ctxt @{thm sym[OF relImage_relInvImage]}, |
|
736 |
rtac ctxt @{thm xt1(3)}, rtac ctxt @{thm Sigma_cong}, |
|
737 |
rtac ctxt @{thm proj_image}, rtac ctxt @{thm proj_image}, rtac ctxt lsbis_incl, |
|
60752 | 738 |
rtac ctxt subset_trans, rtac ctxt @{thm relImage_mono}, rtac ctxt incl_lsbis, assume_tac ctxt, |
60728 | 739 |
rtac ctxt @{thm relImage_proj}, rtac ctxt equiv_LSBIS, rtac ctxt @{thm relInvImage_Id_on}, |
740 |
rtac ctxt Rep_inject]) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
741 |
(Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
742 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
743 |
|
60728 | 744 |
fun mk_unfold_unique_mor_tac ctxt raw_coinds bis mor unfold_defs = |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49501
diff
changeset
|
745 |
CONJ_WRAP' (fn (raw_coind, unfold_def) => |
60728 | 746 |
EVERY' [rtac ctxt @{thm ext}, etac ctxt (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac ctxt mor, |
747 |
rtac ctxt @{thm image2_eqI}, rtac ctxt refl, rtac ctxt (unfold_def RS arg_cong RS trans), |
|
748 |
rtac ctxt (o_apply RS sym), rtac ctxt UNIV_I]) (raw_coinds ~~ unfold_defs) 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
749 |
|
55197 | 750 |
fun mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtors = |
60728 | 751 |
unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, |
752 |
rtac ctxt trans, rtac ctxt unfold, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
753 |
EVERY' (map (fn thm => |
60728 | 754 |
rtac ctxt ballI THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors), |
755 |
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
|
756 |
|
55197 | 757 |
fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls = |
60728 | 758 |
unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac ctxt trans, rtac ctxt (o_apply RS arg_cong), |
759 |
rtac ctxt trans, rtac ctxt unfold, fo_rtac ctxt (@{thm sum.case(2)} RS arg_cong RS trans), |
|
760 |
rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt refl, |
|
761 |
EVERY' (map (fn thm => rtac ctxt @{thm case_sum_expand_Inr} THEN' rtac ctxt thm) corec_Inls)] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
762 |
|
55197 | 763 |
fun mk_corec_unique_mor_tac ctxt corec_defs corec_Inls unfold_unique_mor = |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
51447
diff
changeset
|
764 |
unfold_thms_tac ctxt |
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55393
diff
changeset
|
765 |
(corec_defs @ map (fn thm => thm RS @{thm case_sum_expand_Inr'}) corec_Inls) THEN |
60728 | 766 |
etac ctxt unfold_unique_mor 1; |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
51447
diff
changeset
|
767 |
|
60728 | 768 |
fun mk_dtor_coinduct_tac ctxt m raw_coind bis_rel rel_congs = |
769 |
EVERY' [rtac ctxt rev_mp, rtac ctxt raw_coind, rtac ctxt iffD2, rtac ctxt bis_rel, rtac ctxt conjI, |
|
770 |
CONJ_WRAP' (K (rtac ctxt @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
771 |
rel_congs, |
60728 | 772 |
CONJ_WRAP' (fn rel_cong => EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, |
773 |
REPEAT_DETERM o etac ctxt allE, rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}), |
|
774 |
REPEAT_DETERM_N m o rtac ctxt refl, |
|
775 |
REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm in_rel_Collect_split_eq[symmetric]}, |
|
776 |
etac ctxt mp, etac ctxt CollectE, etac ctxt @{thm splitD}]) |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
777 |
rel_congs, |
60728 | 778 |
rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE, |
779 |
CONJ_WRAP' (K (EVERY' [rtac ctxt impI, rtac ctxt @{thm IdD}, etac ctxt set_mp, |
|
780 |
rtac ctxt CollectI, etac ctxt @{thm case_prodI}])) rel_congs] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
781 |
|
60728 | 782 |
fun mk_map_tac ctxt m n map_arg_cong unfold map_comp map_cong0 = |
783 |
EVERY' [rtac ctxt @{thm ext}, rtac ctxt (o_apply RS trans RS sym), rtac ctxt (o_apply RS trans RS sym), |
|
784 |
rtac ctxt (unfold RS trans), rtac ctxt (Thm.permute_prems 0 1 (map_comp RS @{thm box_equals})), |
|
785 |
rtac ctxt map_cong0, |
|
786 |
REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong), |
|
787 |
REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong), |
|
788 |
rtac ctxt map_arg_cong, rtac ctxt (o_apply RS sym)] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
789 |
|
60728 | 790 |
fun mk_set_le_tac ctxt n Jset_minimal set_Jsets set_Jset_Jsetss = |
791 |
EVERY' [rtac ctxt Jset_minimal, |
|
792 |
REPEAT_DETERM_N n o rtac ctxt @{thm Un_upper1}, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
793 |
REPEAT_DETERM_N n o |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58446
diff
changeset
|
794 |
EVERY' (@{map 3} (fn i => fn set_Jset => fn set_Jset_Jsets => |
60728 | 795 |
EVERY' [rtac ctxt subsetI, rtac ctxt @{thm UnI2}, rtac ctxt (mk_UnIN n i), etac ctxt @{thm UN_I}, |
796 |
etac ctxt UnE, etac ctxt set_Jset, REPEAT_DETERM_N (n - 1) o etac ctxt UnE, |
|
60752 | 797 |
EVERY' (map (fn thm => EVERY' [etac ctxt @{thm UN_E}, etac ctxt thm, assume_tac ctxt]) set_Jset_Jsets)]) |
56179 | 798 |
(1 upto n) set_Jsets set_Jset_Jsetss)] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
799 |
|
60728 | 800 |
fun mk_set_ge_tac ctxt n set_incl_Jset set_Jset_incl_Jsets = |
801 |
EVERY' [rtac ctxt @{thm Un_least}, rtac ctxt set_incl_Jset, |
|
802 |
REPEAT_DETERM_N (n - 1) o rtac ctxt @{thm Un_least}, |
|
803 |
EVERY' (map (fn thm => rtac ctxt @{thm UN_least} THEN' etac ctxt thm) set_Jset_incl_Jsets)] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
804 |
|
60728 | 805 |
fun mk_map_id0_tac ctxt maps unfold_unique unfold_dtor = |
806 |
EVERY' [rtac ctxt (unfold_unique RS trans), EVERY' (map (rtac ctxt o mk_sym) maps), |
|
807 |
rtac ctxt unfold_dtor] 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
808 |
|
60728 | 809 |
fun mk_map_comp0_tac ctxt maps map_comp0s map_unique = |
810 |
EVERY' [rtac ctxt map_unique, |
|
54841
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54793
diff
changeset
|
811 |
EVERY' (map2 (fn map_thm => fn map_comp0 => |
60728 | 812 |
EVERY' (map (rtac ctxt) |
55067 | 813 |
[@{thm comp_assoc[symmetric]} RS trans, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
814 |
@{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans, |
55067 | 815 |
@{thm comp_assoc[symmetric]} RS sym RS trans, map_thm RS arg_cong RS trans, |
816 |
@{thm comp_assoc[symmetric]} RS trans, |
|
54841
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54793
diff
changeset
|
817 |
@{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl]])) |
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54793
diff
changeset
|
818 |
maps map_comp0s)] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
819 |
|
56179 | 820 |
fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_Jsetss |
821 |
set_Jset_Jsetsss in_rels = |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
822 |
let |
53288 | 823 |
val n = length map_comps; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
824 |
val ks = 1 upto n; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
825 |
in |
60728 | 826 |
EVERY' ([rtac ctxt rev_mp, coinduct_tac] @ |
56179 | 827 |
maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_Jsets), |
828 |
set_Jset_Jsetss), in_rel) => |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
829 |
[REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2], |
60728 | 830 |
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], hyp_subst_tac ctxt, rtac ctxt exI, |
831 |
rtac ctxt (Drule.rotate_prems 1 conjI), |
|
832 |
rtac ctxt conjI, rtac ctxt map_comp_trans, rtac ctxt sym, rtac ctxt dtor_maps_trans, rtac ctxt map_cong0, |
|
833 |
REPEAT_DETERM_N m o (rtac ctxt o_apply_trans_sym THEN' rtac ctxt @{thm fst_conv}), |
|
834 |
REPEAT_DETERM_N n o rtac ctxt fst_convol_fun_cong_sym, |
|
835 |
rtac ctxt map_comp_trans, rtac ctxt sym, rtac ctxt dtor_maps_trans, rtac ctxt map_cong0, |
|
56179 | 836 |
EVERY' (maps (fn set_Jset => |
60728 | 837 |
[rtac ctxt o_apply_trans_sym, rtac ctxt (@{thm snd_conv} RS trans), etac ctxt CollectE, |
838 |
REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, etac ctxt set_Jset]) set_Jsets), |
|
839 |
REPEAT_DETERM_N n o rtac ctxt snd_convol_fun_cong_sym, |
|
840 |
rtac ctxt CollectI, |
|
841 |
EVERY' (map (fn set_map0 => EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, |
|
842 |
rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI}, rtac ctxt refl]) |
|
55644 | 843 |
(take m set_map0s)), |
56179 | 844 |
CONJ_WRAP' (fn (set_map0, set_Jset_Jsets) => |
60728 | 845 |
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, |
846 |
rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI}, rtac ctxt exI, rtac ctxt conjI, |
|
847 |
rtac ctxt CollectI, etac ctxt CollectE, |
|
848 |
REPEAT_DETERM o etac ctxt conjE, |
|
56179 | 849 |
CONJ_WRAP' (fn set_Jset_Jset => |
60752 | 850 |
EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_Jset_Jset, assume_tac ctxt]) set_Jset_Jsets, |
60728 | 851 |
rtac ctxt (conjI OF [refl, refl])]) |
56179 | 852 |
(drop m set_map0s ~~ set_Jset_Jsetss)]) |
53288 | 853 |
(map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~ |
56179 | 854 |
map_cong0s ~~ set_map0ss ~~ set_Jsetss ~~ set_Jset_Jsetsss ~~ in_rels) @ |
60728 | 855 |
[rtac ctxt impI, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
856 |
CONJ_WRAP' (fn k => |
60728 | 857 |
EVERY' [rtac ctxt impI, dtac ctxt (mk_conjunctN n k), etac ctxt mp, rtac ctxt exI, rtac ctxt conjI, etac ctxt CollectI, |
858 |
rtac ctxt conjI, rtac ctxt refl, 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
|
859 |
end |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
860 |
|
55197 | 861 |
fun mk_dtor_map_unique_tac ctxt unfold_unique sym_map_comps = |
60728 | 862 |
rtac ctxt unfold_unique 1 THEN |
55067 | 863 |
unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc[symmetric] id_comp comp_id}) THEN |
60728 | 864 |
ALLGOALS (etac ctxt sym); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
865 |
|
55197 | 866 |
fun mk_col_natural_tac ctxt cts rec_0s rec_Sucs dtor_maps set_map0ss = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
867 |
let |
49541 | 868 |
val n = length dtor_maps; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
869 |
in |
60728 | 870 |
EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct), |
871 |
REPEAT_DETERM o rtac ctxt allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s), |
|
872 |
CONJ_WRAP' (K (rtac ctxt @{thm image_empty})) rec_0s, |
|
873 |
REPEAT_DETERM o rtac ctxt allI, |
|
49541 | 874 |
CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY' |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49501
diff
changeset
|
875 |
[SELECT_GOAL (unfold_thms_tac ctxt |
49541 | 876 |
(rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})), |
60728 | 877 |
rtac ctxt Un_cong, rtac ctxt refl, |
878 |
CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 Un_cong)) |
|
879 |
(fn i => EVERY' [rtac ctxt @{thm SUP_cong[OF refl]}, |
|
880 |
REPEAT_DETERM o etac ctxt allE, etac ctxt (mk_conjunctN n i)]) (n downto 1)]) |
|
53289 | 881 |
(rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
882 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
883 |
|
60728 | 884 |
fun mk_set_map0_tac ctxt col_natural = |
885 |
EVERY' (map (rtac ctxt) [@{thm ext}, o_apply RS trans, sym, o_apply RS trans, |
|
886 |
@{thm image_UN} RS trans, refl RS @{thm SUP_cong}, col_natural]) 1; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
887 |
|
60728 | 888 |
fun mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
889 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
890 |
val n = length rec_0s; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
891 |
in |
60728 | 892 |
EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct), |
893 |
REPEAT_DETERM o rtac ctxt allI, |
|
894 |
CONJ_WRAP' (fn rec_0 => EVERY' (map (rtac ctxt) [ordIso_ordLeq_trans, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
895 |
@{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s, |
60728 | 896 |
REPEAT_DETERM o rtac ctxt allI, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
897 |
CONJ_WRAP' (fn (rec_Suc, set_sbds) => EVERY' |
60728 | 898 |
[rtac ctxt ordIso_ordLeq_trans, rtac ctxt @{thm card_of_ordIso_subst}, rtac ctxt rec_Suc, |
899 |
rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac ctxt (nth set_sbds (j - 1)), |
|
900 |
REPEAT_DETERM_N (n - 1) o rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), |
|
901 |
EVERY' (map2 (fn i => fn set_sbd => EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, |
|
902 |
rtac ctxt set_sbd, rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE, |
|
903 |
etac ctxt (mk_conjunctN n i), rtac ctxt sbd_Cinfinite]) (1 upto n) (drop m set_sbds))]) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
904 |
(rec_Sucs ~~ set_sbdss)] 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
905 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
906 |
|
60728 | 907 |
fun mk_set_bd_tac ctxt sbd_Cinfinite col_bd = |
908 |
EVERY' (map (rtac ctxt) [@{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat}, |
|
54793 | 909 |
@{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite]) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
910 |
|
60728 | 911 |
fun mk_le_rel_OO_tac ctxt coinduct rel_Jrels le_rel_OOs = |
912 |
EVERY' (rtac ctxt coinduct :: map2 (fn rel_Jrel => fn le_rel_OO => |
|
54841
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54793
diff
changeset
|
913 |
let val Jrel_imp_rel = rel_Jrel RS iffD1; |
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54793
diff
changeset
|
914 |
in |
60728 | 915 |
EVERY' [rtac ctxt (le_rel_OO RS @{thm predicate2D}), etac ctxt @{thm relcomppE}, |
916 |
rtac ctxt @{thm relcomppI}, etac ctxt Jrel_imp_rel, etac ctxt Jrel_imp_rel] |
|
54841
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54793
diff
changeset
|
917 |
end) |
57726 | 918 |
rel_Jrels le_rel_OOs) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
919 |
|
55197 | 920 |
fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits = |
60728 | 921 |
ALLGOALS (TRY o (eresolve_tac ctxt coind_wits THEN' rtac ctxt refl)) THEN |
60752 | 922 |
REPEAT_DETERM (assume_tac ctxt 1 ORELSE |
60728 | 923 |
EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt dtor_set, |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49501
diff
changeset
|
924 |
K (unfold_thms_tac ctxt dtor_ctors), |
60728 | 925 |
REPEAT_DETERM_N n o etac ctxt UnE, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
926 |
REPEAT_DETERM o |
60728 | 927 |
(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
|
928 |
(eresolve_tac ctxt wit ORELSE' |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
929 |
(dresolve_tac ctxt wit THEN' |
60728 | 930 |
(etac ctxt FalseE ORELSE' |
931 |
EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt dtor_set, |
|
932 |
K (unfold_thms_tac ctxt dtor_ctors), 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
|
933 |
|
55197 | 934 |
fun mk_coind_wit_tac ctxt induct unfolds set_nats wits = |
60728 | 935 |
rtac ctxt induct 1 THEN ALLGOALS (TRY o rtac ctxt impI THEN' TRY o hyp_subst_tac ctxt) THEN |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49501
diff
changeset
|
936 |
unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN |
60728 | 937 |
ALLGOALS (REPEAT_DETERM o etac ctxt imageE THEN' TRY o hyp_subst_tac ctxt) THEN |
49104 | 938 |
ALLGOALS (TRY o |
60728 | 939 |
FIRST' [rtac ctxt TrueI, rtac ctxt refl, etac ctxt (refl RSN (2, mp)), dresolve_tac ctxt wits THEN' etac ctxt FalseE]); |
58445 | 940 |
|
941 |
fun mk_dtor_corec_transfer_tac ctxt n m dtor_corec_defs dtor_unfold_transfer pre_T_map_transfers |
|
942 |
dtor_rels = |
|
58446 | 943 |
CONJ_WRAP (fn (dtor_corec_def, dtor_unfold_transfer) => |
60728 | 944 |
REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN |
58446 | 945 |
unfold_thms_tac ctxt [dtor_corec_def, o_apply] THEN |
60728 | 946 |
HEADGOAL (rtac ctxt (mk_rel_funDN (n + 1) dtor_unfold_transfer) THEN' |
58446 | 947 |
EVERY' (map2 (fn pre_T_map_transfer => fn dtor_rel => |
60728 | 948 |
etac ctxt (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN' |
949 |
rtac ctxt (mk_rel_funDN 2 @{thm comp_transfer}) THEN' |
|
950 |
rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN' |
|
951 |
REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN' |
|
952 |
REPEAT_DETERM_N n o rtac ctxt @{thm Inl_transfer} THEN' |
|
953 |
rtac ctxt rel_funI THEN' |
|
954 |
etac ctxt (dtor_rel RS iffD1)) pre_T_map_transfers dtor_rels) THEN' |
|
955 |
etac ctxt (mk_rel_funDN 1 @{thm Inr_transfer}))) |
|
58446 | 956 |
(dtor_corec_defs ~~ dtor_unfold_transfer); |
49104 | 957 |
|
53287 | 958 |
fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject |
53289 | 959 |
dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
960 |
let |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
961 |
val m = length dtor_set_incls; |
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
962 |
val n = length dtor_set_set_inclss; |
53289 | 963 |
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:
51850
diff
changeset
|
964 |
val in_Jrel = nth in_Jrels (i - 1); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
965 |
val if_tac = |
60728 | 966 |
EVERY' [dtac ctxt (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], |
967 |
rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, |
|
53289 | 968 |
EVERY' (map2 (fn set_map0 => fn set_incl => |
60728 | 969 |
EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, |
970 |
rtac ctxt ord_eq_le_trans, rtac ctxt trans_fun_cong_image_id_id_apply, |
|
971 |
etac ctxt (set_incl RS @{thm subset_trans})]) |
|
53289 | 972 |
passive_set_map0s dtor_set_incls), |
973 |
CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) => |
|
60728 | 974 |
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, |
975 |
rtac ctxt @{thm case_prodI}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, |
|
60752 | 976 |
CONJ_WRAP' (fn thm => etac ctxt (thm RS @{thm subset_trans}) THEN' assume_tac ctxt) dtor_set_set_incls, |
60728 | 977 |
rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl]) |
53289 | 978 |
(in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
979 |
CONJ_WRAP' (fn conv => |
60728 | 980 |
EVERY' [rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0, |
981 |
REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]}, |
|
982 |
REPEAT_DETERM_N n o EVERY' (map (rtac ctxt) [trans, o_apply, conv]), |
|
60752 | 983 |
rtac ctxt trans, rtac ctxt sym, rtac ctxt dtor_map, rtac ctxt (dtor_inject RS iffD2), assume_tac ctxt]) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
984 |
@{thms fst_conv snd_conv}]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
985 |
val only_if_tac = |
60728 | 986 |
EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], |
987 |
rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, |
|
53289 | 988 |
CONJ_WRAP' (fn (dtor_set, passive_set_map0) => |
60728 | 989 |
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt dtor_set, rtac ctxt @{thm Un_least}, |
990 |
rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals}, rtac ctxt passive_set_map0, |
|
60752 | 991 |
rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt, |
60728 | 992 |
CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least})) |
993 |
(fn (active_set_map0, in_Jrel) => EVERY' [rtac ctxt ord_eq_le_trans, |
|
994 |
rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt @{thm box_equals[OF _ _ refl]}, |
|
995 |
rtac ctxt active_set_map0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt @{thm UN_least}, |
|
996 |
dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE, |
|
997 |
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
|
998 |
REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE :: |
56765 | 999 |
@{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:
51850
diff
changeset
|
1000 |
hyp_subst_tac ctxt, |
60728 | 1001 |
dtac ctxt (in_Jrel RS iffD1), |
1002 |
dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, |
|
60752 | 1003 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt]) |
53289 | 1004 |
(rev (active_set_map0s ~~ in_Jrels))]) |
1005 |
(dtor_sets ~~ passive_set_map0s), |
|
60728 | 1006 |
rtac ctxt conjI, |
1007 |
REPEAT_DETERM_N 2 o EVERY'[rtac ctxt (dtor_inject RS iffD1), rtac ctxt trans, rtac ctxt dtor_map, |
|
1008 |
rtac ctxt @{thm box_equals}, rtac ctxt map_comp0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans, |
|
1009 |
rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]}, |
|
60752 | 1010 |
EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, assume_tac ctxt, |
60728 | 1011 |
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
|
1012 |
REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE :: |
56765 | 1013 |
@{thms case_prodE iffD1[OF prod.inject, elim_format]}), |
60728 | 1014 |
hyp_subst_tac ctxt, dtac ctxt (in_Jrel RS iffD1), |
60752 | 1015 |
dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]) in_Jrels), |
1016 |
assume_tac ctxt]] |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1017 |
in |
60728 | 1018 |
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
|
1019 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1020 |
|
58445 | 1021 |
fun mk_rel_coinduct_coind_tac ctxt fst m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss |
55644 | 1022 |
dtor_unfolds dtor_maps in_rels = |
1023 |
let |
|
1024 |
val n = length ks; |
|
1025 |
val fst_diag_nth = if fst then @{thm fst_diag_fst} else @{thm fst_diag_snd}; |
|
1026 |
val snd_diag_nth = if fst then @{thm snd_diag_fst} else @{thm snd_diag_snd}; |
|
51925 | 1027 |
in |
60728 | 1028 |
EVERY' [rtac ctxt coinduct, |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58446
diff
changeset
|
1029 |
EVERY' (@{map 8} (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s => |
55644 | 1030 |
fn dtor_unfold => fn dtor_map => fn in_rel => |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
1031 |
EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2], |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
1032 |
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], |
60752 | 1033 |
select_prem_tac ctxt (length ks) (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
1034 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt, |
60728 | 1035 |
rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI), rtac ctxt conjI, |
1036 |
rtac ctxt (map_comp0 RS trans), rtac ctxt (dtor_map RS trans RS sym), |
|
1037 |
rtac ctxt (dtor_unfold RS map_arg_cong RS trans), rtac ctxt (trans OF [map_comp0, map_cong]), |
|
1038 |
REPEAT_DETERM_N m o rtac ctxt (fst_diag_nth RS @{thm fun_cong[OF trans[OF o_id sym]]}), |
|
1039 |
REPEAT_DETERM_N n o (rtac ctxt @{thm sym[OF trans[OF o_apply]]} THEN' rtac ctxt @{thm fst_conv}), |
|
1040 |
rtac ctxt (map_comp0 RS trans), rtac ctxt (map_cong RS trans), |
|
1041 |
REPEAT_DETERM_N m o rtac ctxt (snd_diag_nth RS fun_cong), |
|
1042 |
REPEAT_DETERM_N n o (rtac ctxt @{thm trans[OF o_apply]} THEN' rtac ctxt @{thm snd_conv}), |
|
1043 |
etac ctxt (@{thm prod.case} RS map_arg_cong RS trans), |
|
55644 | 1044 |
SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.case o_def fst_conv snd_conv}), |
60728 | 1045 |
rtac ctxt CollectI, |
53289 | 1046 |
CONJ_WRAP' (fn set_map0 => |
60728 | 1047 |
EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans), |
1048 |
rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI}, |
|
60752 | 1049 |
FIRST' [rtac ctxt refl, EVERY'[rtac ctxt exI, rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, |
1050 |
assume_tac ctxt, rtac ctxt (@{thm surjective_pairing} RS arg_cong)]]]) |
|
55644 | 1051 |
set_map0s]) |
1052 |
ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps in_rels)] 1 |
|
51925 | 1053 |
end; |
1054 |
||
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55606
diff
changeset
|
1055 |
val split_id_unfolds = @{thms prod.case image_id id_apply}; |
51925 | 1056 |
|
55197 | 1057 |
fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct = |
51925 | 1058 |
let val n = length ks; |
1059 |
in |
|
60728 | 1060 |
rtac ctxt set_induct 1 THEN |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58446
diff
changeset
|
1061 |
EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i => |
60728 | 1062 |
EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE, |
60752 | 1063 |
select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
1064 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp], |
51925 | 1065 |
hyp_subst_tac ctxt, |
53289 | 1066 |
SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)), |
60728 | 1067 |
rtac ctxt subset_refl]) |
53289 | 1068 |
unfolds set_map0ss ks) 1 THEN |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58446
diff
changeset
|
1069 |
EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i => |
53289 | 1070 |
EVERY' (map (fn set_map0 => |
60728 | 1071 |
EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE, |
60752 | 1072 |
select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
1073 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt, |
53289 | 1074 |
SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)), |
60728 | 1075 |
etac ctxt imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp], |
60752 | 1076 |
rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, assume_tac ctxt, |
1077 |
rtac ctxt (@{thm surjective_pairing} RS arg_cong)]) |
|
53289 | 1078 |
(drop m set_map0s))) |
1079 |
unfolds set_map0ss ks) 1 |
|
51925 | 1080 |
end; |
1081 |
||
55197 | 1082 |
fun mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_indss helper_coind1s helper_coind2s = |
51925 | 1083 |
let val n = length in_rels; |
1084 |
in |
|
52506 | 1085 |
Method.insert_tac CIHs 1 THEN |
51925 | 1086 |
unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN |
60728 | 1087 |
REPEAT_DETERM (etac ctxt exE 1) THEN |
51925 | 1088 |
CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) => |
60728 | 1089 |
EVERY' [rtac ctxt @{thm predicate2I}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, |
1090 |
if null helper_inds then rtac ctxt UNIV_I |
|
1091 |
else rtac ctxt CollectI THEN' |
|
51925 | 1092 |
CONJ_WRAP' (fn helper_ind => |
60752 | 1093 |
EVERY' [rtac ctxt (helper_ind RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt, |
60728 | 1094 |
REPEAT_DETERM_N n o etac ctxt thin_rl, rtac ctxt impI, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58634
diff
changeset
|
1095 |
REPEAT_DETERM o resolve_tac ctxt [subsetI, CollectI, @{thm iffD2[OF split_beta]}], |
60752 | 1096 |
dtac ctxt bspec, assume_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE], |
60728 | 1097 |
etac ctxt (refl RSN (2, conjI))]) |
51925 | 1098 |
helper_inds, |
60728 | 1099 |
rtac ctxt conjI, |
60752 | 1100 |
rtac ctxt (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt, |
1101 |
REPEAT_DETERM_N n o etac ctxt thin_rl, |
|
60728 | 1102 |
rtac ctxt impI, etac ctxt mp, rtac ctxt exI, etac ctxt (refl RSN (2, conjI)), |
60752 | 1103 |
rtac ctxt (helper_coind2 RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt, |
1104 |
REPEAT_DETERM_N n o etac ctxt thin_rl, |
|
60728 | 1105 |
rtac ctxt impI, etac ctxt mp, rtac ctxt exI, etac ctxt (refl RSN (2, conjI))]) |
51925 | 1106 |
(in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1 |
1107 |
end; |
|
1108 |
||
55901
8c6d49dd8ae1
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
blanchet
parents:
55644
diff
changeset
|
1109 |
fun mk_unfold_transfer_tac ctxt m ctor_rel_coinduct map_transfers unfolds = |
52731 | 1110 |
let |
1111 |
val n = length map_transfers; |
|
1112 |
in |
|
1113 |
unfold_thms_tac ctxt |
|
55945 | 1114 |
@{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN |
1115 |
unfold_thms_tac ctxt @{thms rel_fun_iff_geq_image2p} THEN |
|
52731 | 1116 |
HEADGOAL (EVERY' |
60728 | 1117 |
[REPEAT_DETERM o resolve_tac ctxt [allI, impI], rtac ctxt ctor_rel_coinduct, |
52731 | 1118 |
EVERY' (map (fn map_transfer => EVERY' |
60728 | 1119 |
[REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt @{thm image2pE}, hyp_subst_tac ctxt, |
52731 | 1120 |
SELECT_GOAL (unfold_thms_tac ctxt unfolds), |
60728 | 1121 |
rtac ctxt (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer), |
1122 |
REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer}, |
|
1123 |
REPEAT_DETERM_N n o rtac ctxt @{thm rel_fun_image2p}, |
|
1124 |
etac ctxt @{thm predicate2D}, etac ctxt @{thm image2pI}]) |
|
52731 | 1125 |
map_transfers)]) |
1126 |
end; |
|
1127 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1128 |
end; |