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