author | blanchet |
Thu, 29 Aug 2013 22:39:46 +0200 | |
changeset 53288 | 050d0bc9afa5 |
parent 53287 | 271b34513bfb |
child 53289 | 5e0623448bdb |
permissions | -rw-r--r-- |
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49506
diff
changeset
|
1 |
(* Title: HOL/BNF/Tools/bnf_lfp_tactics.ML |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Author: Andrei Popescu, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
Tactics for the datatype construction. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
signature BNF_LFP_TACTICS = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
sig |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
11 |
val mk_alg_min_alg_tac: int -> thm -> thm list -> thm -> thm -> thm list list -> thm list -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
thm list -> tactic |
51798 | 13 |
val mk_alg_not_empty_tac: Proof.context -> thm -> thm list -> thm list -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
val mk_alg_select_tac: thm -> {prems: 'a, context: Proof.context} -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
15 |
val mk_alg_set_tac: thm -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
val mk_bd_card_order_tac: thm list -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
17 |
val mk_bd_limit_tac: int -> thm -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
18 |
val mk_card_of_min_alg_tac: thm -> thm -> thm -> thm -> thm -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
19 |
val mk_copy_alg_tac: thm list list -> thm list -> thm -> thm -> thm -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
20 |
val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic |
51798 | 21 |
val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm -> |
22 |
thm list -> thm list -> thm list -> tactic |
|
49501 | 23 |
val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list -> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
{prems: 'a, context: Proof.context} -> tactic |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49544
diff
changeset
|
25 |
val mk_ctor_set_tac: thm -> thm -> thm list -> tactic |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
26 |
val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list -> |
51798 | 27 |
thm -> thm -> thm list -> thm list -> thm list list -> tactic |
49506 | 28 |
val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic |
49501 | 29 |
val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
val mk_init_ex_mor_tac: thm -> thm -> thm -> thm list -> thm -> thm -> thm -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
{prems: 'a, context: Proof.context} -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
val mk_init_induct_tac: int -> thm -> 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
|
33 |
val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
34 |
thm list -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
35 |
val mk_iso_alt_tac: thm list -> thm -> tactic |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
36 |
val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic |
52731 | 37 |
val mk_fold_transfer_tac: int -> thm -> thm list -> thm list -> |
38 |
{prems: thm list, context: Proof.context} -> tactic |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
39 |
val mk_least_min_alg_tac: thm -> thm -> tactic |
51798 | 40 |
val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> |
41 |
thm list list -> thm list list list -> thm list -> tactic |
|
53287 | 42 |
val mk_map_comp0_tac: thm list -> thm list -> thm -> int -> tactic |
53270 | 43 |
val mk_map_id0_tac: thm list -> thm -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
44 |
val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic |
52911 | 45 |
val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
47 |
{prems: 'a, context: Proof.context} -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm -> |
51812 | 49 |
thm -> thm -> thm -> thm -> thm -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
50 |
val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic |
51798 | 51 |
val mk_min_algs_mono_tac: Proof.context -> thm -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
val mk_min_algs_tac: thm -> thm list -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
53 |
val mk_mor_Abs_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
|
54 |
val mk_mor_Rep_tac: thm list -> thm -> thm list -> thm list -> thm list -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
{prems: 'a, context: Proof.context} -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
val mk_mor_UNIV_tac: int -> thm list -> thm -> tactic |
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 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_convol_tac: 'a list -> 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_elim_tac: thm -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
60 |
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
|
61 |
val mk_mor_inv_tac: thm -> thm -> thm list list -> thm list -> thm list -> thm list -> tactic |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
62 |
val mk_mor_fold_tac: ctyp -> cterm -> thm list -> thm -> thm -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
63 |
val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
thm list -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
65 |
val mk_mor_str_tac: 'a list -> thm -> tactic |
51918 | 66 |
val mk_rel_induct_tac: int -> thm -> int list -> thm list -> thm list -> |
52506 | 67 |
{prems: thm list, context: Proof.context} -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49585
diff
changeset
|
69 |
val mk_rec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> |
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49585
diff
changeset
|
70 |
tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
val mk_set_bd_tac: int -> (int -> tactic) -> thm -> thm list list -> thm list -> int -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
72 |
{prems: 'a, context: Proof.context} -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
73 |
val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
74 |
thm list -> int -> {prems: 'a, context: Proof.context} -> tactic |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
75 |
val mk_set_map_tac: thm -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
76 |
val mk_set_tac: thm -> tactic |
51798 | 77 |
val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
78 |
val mk_wpull_tac: thm -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
80 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
81 |
structure BNF_LFP_Tactics : BNF_LFP_TACTICS = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
struct |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
83 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
84 |
open BNF_Tactics |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
85 |
open BNF_LFP_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
open BNF_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
|
49306 | 88 |
val fst_snd_convs = @{thms fst_conv snd_conv}; |
89 |
val ord_eq_le_trans = @{thm ord_eq_le_trans}; |
|
90 |
val subset_trans = @{thm subset_trans}; |
|
91 |
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
|
92 |
val rev_bspec = Drule.rotate_prems 1 bspec; |
58b87aa4dc3b
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents:
52635
diff
changeset
|
93 |
val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]} |
49306 | 94 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
95 |
fun mk_alg_set_tac alg_def = |
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
96 |
dtac (alg_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
|
97 |
REPEAT_DETERM (etac conjE 1) THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
98 |
EVERY' [etac bspec, rtac CollectI] 1 THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
99 |
REPEAT_DETERM (etac conjI 1) THEN atac 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
100 |
|
51798 | 101 |
fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits = |
102 |
(EVERY' [rtac notI, hyp_subst_tac ctxt, ftac alg_set] THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
103 |
REPEAT_DETERM o FIRST' |
49306 | 104 |
[rtac subset_UNIV, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
105 |
EVERY' [rtac @{thm subset_emptyI}, eresolve_tac wits], |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
106 |
EVERY' [rtac subsetI, rtac FalseE, eresolve_tac wits], |
51798 | 107 |
EVERY' [rtac subsetI, dresolve_tac wits, hyp_subst_tac ctxt, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
108 |
FIRST' (map (fn thm => rtac thm THEN' atac) alg_sets)]] THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
109 |
etac @{thm emptyE}) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
110 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
111 |
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
|
112 |
(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
|
113 |
REPEAT o etac conjE THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
114 |
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
|
115 |
etac bspec THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
116 |
atac) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
117 |
|
53285 | 118 |
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
|
119 |
(stac mor_def THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
120 |
rtac conjI THEN' |
53285 | 121 |
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
|
122 |
CONJ_WRAP' (fn thm => |
53285 | 123 |
(EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_ids) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
124 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
125 |
fun mk_mor_comp_tac mor_def set_map's map_comp_ids = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
126 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
127 |
val fbetw_tac = EVERY' [rtac ballI, stac o_apply, etac bspec, etac bspec, atac]; |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
128 |
fun mor_tac (set_map', map_comp_id) = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
129 |
EVERY' [rtac ballI, stac o_apply, rtac trans, |
52659
58b87aa4dc3b
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents:
52635
diff
changeset
|
130 |
rtac trans, dtac rev_bspec, atac, etac arg_cong, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
131 |
REPEAT o eresolve_tac [CollectE, conjE], etac bspec, rtac CollectI] THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
132 |
CONJ_WRAP' (fn thm => |
49306 | 133 |
FIRST' [rtac subset_UNIV, |
134 |
(EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI}, |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
135 |
etac bspec, etac set_mp, atac])]) set_map' THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
136 |
rtac (map_comp_id RS arg_cong); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
137 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
138 |
(dtac (mor_def RS subst) THEN' dtac (mor_def RS subst) THEN' stac mor_def THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
139 |
REPEAT o etac conjE THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
140 |
rtac conjI THEN' |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
141 |
CONJ_WRAP' (K fbetw_tac) set_map's THEN' |
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
142 |
CONJ_WRAP' mor_tac (set_map's ~~ map_comp_ids)) 1 |
48975
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 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
145 |
fun mk_mor_inv_tac alg_def mor_def set_map's morEs map_comp_ids map_cong0Ls = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
146 |
let |
49306 | 147 |
val fbetw_tac = EVERY' [rtac ballI, etac set_mp, etac imageI]; |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
148 |
fun Collect_tac set_map' = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
149 |
CONJ_WRAP' (fn thm => |
49306 | 150 |
FIRST' [rtac subset_UNIV, |
151 |
(EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans, |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
152 |
etac @{thm image_mono}, atac])]) set_map'; |
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
153 |
fun mor_tac (set_map', ((morE, map_comp_id), map_cong0L)) = |
52659
58b87aa4dc3b
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents:
52635
diff
changeset
|
154 |
EVERY' [rtac ballI, ftac rev_bspec, atac, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
155 |
REPEAT o eresolve_tac [CollectE, conjE], rtac sym, rtac trans, rtac sym, |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
156 |
etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_map', |
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
157 |
rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map', |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
158 |
rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_cong0L RS arg_cong), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
159 |
REPEAT_DETERM_N (length morEs) o |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
160 |
(EVERY' [rtac subst, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
161 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
162 |
(stac mor_def THEN' |
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
163 |
dtac (alg_def RS iffD1) THEN' |
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
164 |
dtac (alg_def RS iffD1) THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
165 |
REPEAT o etac conjE THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
166 |
rtac conjI THEN' |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
167 |
CONJ_WRAP' (K fbetw_tac) set_map's THEN' |
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
168 |
CONJ_WRAP' mor_tac (set_map's ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
169 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
170 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
171 |
fun mk_mor_str_tac ks mor_def = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
172 |
(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
|
173 |
CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) ks THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
174 |
CONJ_WRAP' (K (EVERY' [rtac ballI, rtac refl])) ks) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
175 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
176 |
fun mk_mor_convol_tac ks mor_def = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
177 |
(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
|
178 |
CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) ks THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
179 |
CONJ_WRAP' (K (EVERY' [rtac ballI, rtac trans, rtac @{thm fst_convol'}, rtac o_apply])) ks) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
180 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
181 |
fun mk_mor_UNIV_tac m morEs mor_def = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
182 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
183 |
val n = length morEs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
184 |
fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE, |
49306 | 185 |
rtac CollectI, CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto m + n), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
186 |
rtac sym, rtac o_apply]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
187 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
188 |
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
|
189 |
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
|
190 |
REPEAT_DETERM o etac conjE, REPEAT_DETERM_N n o dtac (@{thm fun_eq_iff} RS subst), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
191 |
CONJ_WRAP' (K (EVERY' [rtac ballI, REPEAT_DETERM o etac allE, rtac trans, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
192 |
etac (o_apply RS subst), rtac o_apply])) morEs] 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
193 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
194 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
195 |
fun mk_iso_alt_tac mor_images mor_inv = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
196 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
197 |
val n = length mor_images; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
198 |
fun if_wrap_tac thm = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
199 |
EVERY' [rtac ssubst, rtac @{thm bij_betw_iff_ex}, rtac exI, rtac conjI, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
200 |
rtac @{thm inver_surj}, etac thm, etac thm, atac, etac conjI, atac] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
201 |
val if_tac = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
202 |
EVERY' [etac thin_rl, etac thin_rl, REPEAT o eresolve_tac [conjE, exE], |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
203 |
rtac conjI, atac, CONJ_WRAP' if_wrap_tac mor_images]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
204 |
val only_if_tac = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
205 |
EVERY' [rtac conjI, etac conjunct1, EVERY' (map (fn thm => |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
206 |
EVERY' [rtac exE, rtac @{thm bij_betw_ex_weakE}, etac (conjunct2 RS thm)]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
207 |
(map (mk_conjunctN n) (1 upto n))), REPEAT o rtac exI, rtac conjI, rtac mor_inv, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
208 |
etac conjunct1, atac, atac, REPEAT_DETERM_N n o atac, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
209 |
CONJ_WRAP' (K (etac conjunct2)) mor_images]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
210 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
211 |
(rtac iffI THEN' if_tac THEN' only_if_tac) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
212 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
213 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
214 |
fun mk_copy_str_tac set_map's alg_def alg_sets = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
215 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
216 |
val n = length alg_sets; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
217 |
val bij_betw_inv_tac = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
218 |
EVERY' [etac thin_rl, REPEAT_DETERM_N n o EVERY' [dtac @{thm bij_betwI}, atac, atac], |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
219 |
REPEAT_DETERM_N (2 * n) o etac thin_rl, REPEAT_DETERM_N (n - 1) o etac conjI, atac]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
220 |
fun set_tac thms = |
49306 | 221 |
EVERY' [rtac ord_eq_le_trans, resolve_tac thms, rtac subset_trans, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
222 |
etac @{thm image_mono}, rtac equalityD1, etac @{thm bij_betw_imageE}]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
223 |
val copy_str_tac = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
224 |
CONJ_WRAP' (fn (thms, thm) => |
49306 | 225 |
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
226 |
rtac equalityD1, etac @{thm bij_betw_imageE}, rtac imageI, etac thm, |
49306 | 227 |
REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)]) |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
228 |
(set_map's ~~ alg_sets); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
229 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
230 |
(rtac rev_mp THEN' DETERM o bij_betw_inv_tac THEN' rtac impI THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
231 |
stac alg_def THEN' copy_str_tac) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
232 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
233 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
234 |
fun mk_copy_alg_tac set_map's alg_sets mor_def iso_alt copy_str = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
235 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
236 |
val n = length alg_sets; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
237 |
val fbetw_tac = CONJ_WRAP' (K (etac @{thm bij_betwE})) alg_sets; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
238 |
fun set_tac thms = |
49306 | 239 |
EVERY' [rtac ord_eq_le_trans, resolve_tac thms, rtac subset_trans, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
240 |
REPEAT_DETERM o etac conjE, etac @{thm image_mono}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
241 |
rtac equalityD1, etac @{thm bij_betw_imageE}]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
242 |
val mor_tac = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
243 |
CONJ_WRAP' (fn (thms, thm) => |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
244 |
EVERY' [rtac ballI, etac CollectE, etac @{thm inverE}, etac thm, |
49306 | 245 |
REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)]) |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
246 |
(set_map's ~~ alg_sets); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
247 |
in |
52904 | 248 |
(rtac (iso_alt RS iffD2) THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
249 |
etac copy_str THEN' REPEAT_DETERM o atac THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
250 |
rtac conjI THEN' stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
251 |
CONJ_WRAP' (K atac) alg_sets) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
252 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
253 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
254 |
fun mk_ex_copy_alg_tac n copy_str copy_alg = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
255 |
EVERY' [REPEAT_DETERM_N n o rtac exI, rtac conjI, etac copy_str, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
256 |
REPEAT_DETERM_N n o atac, |
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 etac @{thm bij_betw_inver2}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
258 |
REPEAT_DETERM_N n o etac @{thm bij_betw_inver1}, etac copy_alg, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
259 |
REPEAT_DETERM_N n o atac, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
260 |
REPEAT_DETERM_N n o etac @{thm bij_betw_inver2}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
261 |
REPEAT_DETERM_N n o etac @{thm bij_betw_inver1}] 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
262 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
263 |
fun mk_bd_limit_tac n bd_Cinfinite = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
264 |
EVERY' [REPEAT_DETERM o etac conjE, rtac rev_mp, rtac @{thm Cinfinite_limit_finite}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
265 |
REPEAT_DETERM_N n o rtac @{thm finite.insertI}, rtac @{thm finite.emptyI}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
266 |
REPEAT_DETERM_N n o etac @{thm insert_subsetI}, rtac @{thm empty_subsetI}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
267 |
rtac bd_Cinfinite, rtac impI, etac bexE, rtac bexI, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
268 |
CONJ_WRAP' (fn i => |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
269 |
EVERY' [etac bspec, REPEAT_DETERM_N i o rtac @{thm insertI2}, rtac @{thm insertI1}]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
270 |
(0 upto n - 1), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
271 |
atac] 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
272 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
273 |
fun mk_min_algs_tac worel in_congs = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
274 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
275 |
val minG_tac = EVERY' [rtac @{thm UN_cong}, rtac refl, dtac bspec, atac, etac arg_cong]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
276 |
fun minH_tac thm = |
52659
58b87aa4dc3b
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents:
52635
diff
changeset
|
277 |
EVERY' [rtac Un_cong, minG_tac, rtac @{thm image_cong}, rtac thm, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
278 |
REPEAT_DETERM_N (length in_congs) o minG_tac, rtac refl]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
279 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
280 |
(rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ssubst THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
281 |
rtac meta_eq_to_obj_eq THEN' rtac (worel RS @{thm wo_rel.adm_wo_def}) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
282 |
REPEAT_DETERM_N 3 o rtac allI THEN' rtac impI THEN' |
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49463
diff
changeset
|
283 |
CONJ_WRAP_GEN' (EVERY' [rtac Pair_eqI, rtac conjI]) minH_tac in_congs) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
284 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
285 |
|
51798 | 286 |
fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
287 |
rtac impI, rtac @{thm case_split}, rtac @{thm xt1(3)}, rtac min_algs, etac @{thm FieldI2}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
288 |
rtac subsetI, rtac UnI1, rtac @{thm UN_I}, etac @{thm underS_I}, atac, atac, |
51798 | 289 |
rtac equalityD1, dtac @{thm notnotD}, hyp_subst_tac ctxt, rtac refl] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
290 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
291 |
fun mk_min_algs_card_of_tac cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero |
51812 | 292 |
suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
293 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
294 |
val induct = worel RS |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
295 |
Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
296 |
val src = 1 upto m + 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
297 |
val dest = (m + 1) :: (1 upto m); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
298 |
val absorbAs_tac = 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
|
299 |
else EVERY' [rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
300 |
rtac @{thm ordIso_transitive}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
301 |
BNF_Tactics.mk_rotate_eq_tac (rtac @{thm ordIso_refl} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
302 |
FIRST' [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
303 |
rtac @{thm Card_order_cexp}]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
304 |
@{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
305 |
src dest, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
306 |
rtac @{thm csum_absorb1}, rtac Asuc_Cinfinite, rtac ctrans, rtac @{thm ordLeq_csum1}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
307 |
FIRST' [rtac @{thm Card_order_csum}, rtac @{thm card_of_Card_order}], |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
308 |
rtac @{thm ordLeq_cexp1}, rtac suc_Cnotzero, rtac @{thm Card_order_csum}]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
309 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
310 |
val minG_tac = EVERY' [rtac @{thm UNION_Cinfinite_bound}, rtac @{thm ordLess_imp_ordLeq}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
311 |
rtac @{thm ordLess_transitive}, rtac @{thm card_of_underS}, rtac suc_Card_order, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
312 |
atac, rtac suc_Asuc, rtac ballI, etac allE, dtac mp, etac @{thm underS_E}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
313 |
dtac mp, etac @{thm underS_Field}, REPEAT o etac conjE, atac, rtac Asuc_Cinfinite] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
314 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
315 |
fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac @{thm ordIso_ordLeq_trans}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
316 |
rtac @{thm card_of_ordIso_subst}, etac min_alg, rtac @{thm Un_Cinfinite_bound}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
317 |
minG_tac, rtac ctrans, rtac @{thm card_of_image}, rtac ctrans, rtac in_bd, rtac ctrans, |
51782
84e7225f5ab6
removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents:
51766
diff
changeset
|
318 |
rtac @{thm cexp_mono1}, rtac @{thm csum_mono1}, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
319 |
REPEAT_DETERM_N m o rtac @{thm csum_mono2}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
320 |
CONJ_WRAP_GEN' (rtac @{thm csum_cinfinite_bound}) (K minG_tac) min_algs, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
321 |
REPEAT_DETERM o FIRST' |
51782
84e7225f5ab6
removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents:
51766
diff
changeset
|
322 |
[rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum}, |
84e7225f5ab6
removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents:
51766
diff
changeset
|
323 |
rtac Asuc_Cinfinite, rtac bd_Card_order], |
84e7225f5ab6
removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents:
51766
diff
changeset
|
324 |
rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong1}, absorbAs_tac, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
325 |
rtac @{thm csum_absorb1}, rtac Asuc_Cinfinite, rtac @{thm ctwo_ordLeq_Cinfinite}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
326 |
rtac Asuc_Cinfinite, rtac bd_Card_order, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
327 |
rtac @{thm ordIso_imp_ordLeq}, rtac @{thm cexp_cprod_ordLeq}, |
51782
84e7225f5ab6
removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents:
51766
diff
changeset
|
328 |
resolve_tac @{thms Card_order_csum Card_order_ctwo}, rtac suc_Cinfinite, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
329 |
rtac bd_Cnotzero, rtac @{thm cardSuc_ordLeq}, rtac bd_Card_order, rtac Asuc_Cinfinite]; |
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 |
(rtac induct THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
332 |
rtac impI THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
333 |
CONJ_WRAP' mk_minH_tac (min_algs ~~ in_bds)) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
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_min_algs_least_tac cT ct worel min_algs alg_sets = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
337 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
338 |
val induct = worel RS |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
339 |
Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
340 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
341 |
val minG_tac = EVERY' [rtac @{thm UN_least}, etac allE, dtac mp, etac @{thm underS_E}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
342 |
dtac mp, etac @{thm underS_Field}, REPEAT_DETERM o etac conjE, atac]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
343 |
|
49306 | 344 |
fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ord_eq_le_trans, etac min_alg, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
345 |
rtac @{thm Un_least}, minG_tac, rtac @{thm image_subsetI}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
346 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac alg_set, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
347 |
REPEAT_DETERM o FIRST' [atac, etac subset_trans THEN' minG_tac]]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
348 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
349 |
(rtac induct THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
350 |
rtac impI THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
351 |
CONJ_WRAP' mk_minH_tac (min_algs ~~ alg_sets)) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
352 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
353 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
354 |
fun mk_alg_min_alg_tac m alg_def min_alg_defs bd_limit bd_Cinfinite |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
355 |
set_bdss min_algs min_alg_monos = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
356 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
357 |
val n = length min_algs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
358 |
fun mk_cardSuc_UNION_tac set_bds (mono, def) = EVERY' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
359 |
[rtac bexE, rtac @{thm cardSuc_UNION_Cinfinite}, rtac bd_Cinfinite, rtac mono, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
360 |
etac (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve_tac set_bds]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
361 |
fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) = |
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, conjE], |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
363 |
EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac bexE, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
364 |
rtac bd_limit, REPEAT_DETERM_N (n - 1) o etac conjI, atac, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
365 |
rtac (min_alg_def RS @{thm set_mp[OF equalityD2]}), |
49306 | 366 |
rtac @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac thin_rl, atac, rtac set_mp, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
367 |
rtac equalityD2, rtac min_alg, atac, rtac UnI2, rtac @{thm image_eqI}, rtac refl, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
368 |
rtac CollectI, REPEAT_DETERM_N m o dtac asm_rl, REPEAT_DETERM_N n o etac thin_rl, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
369 |
REPEAT_DETERM o etac conjE, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
370 |
CONJ_WRAP' (K (FIRST' [atac, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
371 |
EVERY' [etac subset_trans, rtac subsetI, rtac @{thm UN_I}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
372 |
etac @{thm underS_I}, atac, atac]])) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
373 |
set_bds]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
374 |
in |
52904 | 375 |
(rtac (alg_def RS iffD2) THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
376 |
CONJ_WRAP' mk_conjunct_tac (set_bdss ~~ (min_algs ~~ min_alg_defs))) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
377 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
378 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
379 |
fun mk_card_of_min_alg_tac min_alg_def card_of suc_Card_order suc_Asuc Asuc_Cinfinite = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
380 |
EVERY' [stac min_alg_def, rtac @{thm UNION_Cinfinite_bound}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
381 |
rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_Field_ordIso}, rtac suc_Card_order, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
382 |
rtac @{thm ordLess_imp_ordLeq}, rtac suc_Asuc, rtac ballI, dtac rev_mp, rtac card_of, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
383 |
REPEAT_DETERM o etac conjE, atac, rtac Asuc_Cinfinite] 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
384 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
385 |
fun mk_least_min_alg_tac min_alg_def least = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
386 |
EVERY' [stac min_alg_def, rtac @{thm UN_least}, dtac least, dtac mp, atac, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
387 |
REPEAT_DETERM o etac conjE, atac] 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
388 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
389 |
fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} = |
51798 | 390 |
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
391 |
unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
392 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
393 |
fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
394 |
alg_sets set_map's str_init_defs = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
395 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
396 |
val n = length alg_sets; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
397 |
val fbetw_tac = |
52659
58b87aa4dc3b
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents:
52635
diff
changeset
|
398 |
CONJ_WRAP' (K (EVERY' [rtac ballI, etac rev_bspec, etac CollectE, atac])) alg_sets; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
399 |
val mor_tac = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
400 |
CONJ_WRAP' (fn thm => EVERY' [rtac ballI, rtac thm]) str_init_defs; |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
401 |
fun alg_epi_tac ((alg_set, str_init_def), set_map') = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
402 |
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
403 |
rtac ballI, ftac (alg_select RS bspec), stac str_init_def, etac alg_set, |
49306 | 404 |
REPEAT_DETERM o FIRST' [rtac subset_UNIV, |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
405 |
EVERY' [rtac ord_eq_le_trans, resolve_tac set_map', rtac subset_trans, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
406 |
etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]]]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
407 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
408 |
(rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm o_id}) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
409 |
rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
410 |
stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' rtac mor_incl_min_alg THEN' |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
411 |
stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_map's)) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
412 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
413 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
414 |
fun mk_init_ex_mor_tac Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
415 |
mor_comp mor_select mor_incl_min_alg {context = ctxt, prems = _} = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
416 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
417 |
val n = length card_of_min_algs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
418 |
val card_of_ordIso_tac = EVERY' [rtac ssubst, rtac @{thm card_of_ordIso}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
419 |
rtac @{thm ordIso_symmetric}, rtac conjunct1, rtac conjunct2, atac]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
420 |
fun internalize_tac card_of = EVERY' [rtac subst, rtac @{thm internalize_card_of_ordLeq2}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
421 |
rtac @{thm ordLeq_ordIso_trans}, rtac card_of, rtac subst, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
422 |
rtac @{thm Card_order_iff_ordIso_card_of}, rtac @{thm Card_order_cexp}]; |
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 |
(rtac rev_mp THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
425 |
REPEAT_DETERM_N (2 * n) o (rtac mp THEN' rtac @{thm ex_mono} THEN' rtac impI) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
426 |
REPEAT_DETERM_N (n + 1) o etac thin_rl THEN' rtac (alg_min_alg RS copy_alg_ex) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
427 |
REPEAT_DETERM_N n o atac THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
428 |
REPEAT_DETERM_N n o card_of_ordIso_tac THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
429 |
EVERY' (map internalize_tac card_of_min_algs) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
430 |
rtac impI THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
431 |
REPEAT_DETERM o eresolve_tac [exE, conjE] THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
432 |
REPEAT_DETERM o rtac exI THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
433 |
rtac mor_select THEN' atac THEN' rtac CollectI THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
434 |
REPEAT_DETERM o rtac exI THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
435 |
rtac conjI THEN' rtac refl THEN' atac THEN' |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
436 |
K (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
437 |
etac mor_comp THEN' etac mor_incl_min_alg) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
438 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
439 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
440 |
fun mk_init_unique_mor_tac m |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
441 |
alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_cong0s = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
442 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
443 |
val n = length least_min_algs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
444 |
val ks = (1 upto n); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
445 |
|
49306 | 446 |
fun mor_tac morE in_mono = EVERY' [etac morE, rtac set_mp, rtac in_mono, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
447 |
REPEAT_DETERM_N n o rtac @{thm Collect_restrict}, rtac CollectI, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
448 |
REPEAT_DETERM_N (m + n) o (TRY o rtac conjI THEN' atac)]; |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
449 |
fun cong_tac map_cong0 = EVERY' [rtac (map_cong0 RS arg_cong), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
450 |
REPEAT_DETERM_N m o rtac refl, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
451 |
REPEAT_DETERM_N n o (etac @{thm prop_restrict} THEN' atac)]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
452 |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
453 |
fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong0))) = EVERY' [rtac ballI, rtac CollectI, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
454 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set), |
49306 | 455 |
REPEAT_DETERM_N m o rtac subset_UNIV, |
456 |
REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}), |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
457 |
rtac trans, mor_tac morE in_mono, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
458 |
rtac trans, cong_tac map_cong0, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
459 |
rtac sym, mor_tac morE in_mono]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
460 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
461 |
fun mk_unique_tac (k, least_min_alg) = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
462 |
select_prem_tac n (etac @{thm prop_restrict}) k THEN' rtac least_min_alg THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
463 |
stac alg_def THEN' |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
464 |
CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s))); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
465 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
466 |
CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
467 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
468 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
469 |
fun mk_init_induct_tac m alg_def alg_min_alg least_min_algs alg_sets = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
470 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
471 |
val n = length least_min_algs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
472 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
473 |
fun mk_alg_tac alg_set = EVERY' [rtac ballI, rtac CollectI, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
474 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set), |
49306 | 475 |
REPEAT_DETERM_N m o rtac subset_UNIV, |
476 |
REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}), |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
477 |
rtac mp, etac bspec, rtac CollectI, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
478 |
REPEAT_DETERM_N m o (rtac conjI THEN' atac), |
49306 | 479 |
CONJ_WRAP' (K (etac subset_trans THEN' rtac @{thm Collect_restrict})) alg_sets, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
480 |
CONJ_WRAP' (K (rtac ballI THEN' etac @{thm prop_restrict} THEN' atac)) alg_sets]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
481 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
482 |
fun mk_induct_tac least_min_alg = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
483 |
rtac ballI THEN' etac @{thm prop_restrict} THEN' rtac least_min_alg THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
484 |
stac alg_def THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
485 |
CONJ_WRAP' mk_alg_tac alg_sets; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
486 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
487 |
CONJ_WRAP' mk_induct_tac least_min_algs 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
488 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
489 |
|
49501 | 490 |
fun mk_mor_Rep_tac ctor_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} = |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
491 |
(K (unfold_thms_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
492 |
EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
493 |
EVERY' (map rtac inver_Abss) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
494 |
EVERY' (map rtac inver_Reps)) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
495 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
496 |
fun mk_mor_Abs_tac inv inver_Abss inver_Reps = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
497 |
(rtac inv THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
498 |
EVERY' (map2 (fn inver_Abs => fn inver_Rep => |
49306 | 499 |
EVERY' [rtac conjI, rtac subset_UNIV, rtac conjI, rtac inver_Rep, rtac inver_Abs]) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
500 |
inver_Abss inver_Reps)) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
501 |
|
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
502 |
fun mk_mor_fold_tac cT ct fold_defs ex_mor mor = |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
503 |
(EVERY' (map stac fold_defs) THEN' EVERY' [rtac rev_mp, rtac ex_mor, rtac impI] THEN' |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
504 |
REPEAT_DETERM_N (length fold_defs) o etac exE THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
505 |
rtac (Drule.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac mor) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
506 |
|
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
507 |
fun mk_fold_unique_mor_tac type_defs init_unique_mors Reps mor_comp mor_Abs mor_fold = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
508 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
509 |
fun mk_unique type_def = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
510 |
EVERY' [rtac @{thm surj_fun_eq}, rtac (type_def RS @{thm type_definition.Abs_image}), |
49227 | 511 |
rtac ballI, resolve_tac init_unique_mors, |
512 |
EVERY' (map (fn thm => atac ORELSE' rtac thm) Reps), |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
513 |
rtac mor_comp, rtac mor_Abs, atac, |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
514 |
rtac mor_comp, rtac mor_Abs, rtac mor_fold]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
515 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
516 |
CONJ_WRAP' mk_unique type_defs 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
517 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
518 |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
519 |
fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_folds = |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
520 |
EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
521 |
rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L, |
49306 | 522 |
EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
523 |
ctor_o_folds), |
49306 | 524 |
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
|
525 |
|
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
526 |
fun mk_rec_tac rec_defs foldx fst_recs {context = ctxt, prems = _}= |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
527 |
unfold_thms_tac ctxt |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
528 |
(rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
529 |
EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (foldx RS @{thm arg_cong[of _ _ snd]}), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
530 |
rtac @{thm snd_convol'}] 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
531 |
|
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49585
diff
changeset
|
532 |
fun mk_rec_unique_mor_tac rec_defs fst_recs fold_unique_mor {context = ctxt, prems = _} = |
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49585
diff
changeset
|
533 |
unfold_thms_tac ctxt |
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49585
diff
changeset
|
534 |
(rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN |
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49585
diff
changeset
|
535 |
etac fold_unique_mor 1; |
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49585
diff
changeset
|
536 |
|
51798 | 537 |
fun mk_ctor_induct_tac ctxt m set_map'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
538 |
let |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
539 |
val n = length set_map'ss; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
540 |
val ks = 1 upto n; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
541 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
542 |
fun mk_IH_tac Rep_inv Abs_inv set_map' = |
49306 | 543 |
DETERM o EVERY' [dtac meta_mp, rtac (Rep_inv RS arg_cong RS subst), etac bspec, |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
544 |
dtac set_rev_mp, rtac equalityD1, rtac set_map', etac imageE, |
51798 | 545 |
hyp_subst_tac ctxt, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
546 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
547 |
fun mk_closed_tac (k, (morE, set_map's)) = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
548 |
EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
549 |
rtac (mor_Abs RS morE RS arg_cong RS ssubst), atac, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
550 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec}, |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
551 |
EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_map's)), atac]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
552 |
|
49227 | 553 |
fun mk_induct_tac (Rep, Rep_inv) = |
554 |
EVERY' [rtac (Rep_inv RS arg_cong RS subst), etac (Rep RSN (2, bspec))]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
555 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
556 |
(rtac mp THEN' rtac impI THEN' |
49227 | 557 |
DETERM o CONJ_WRAP_GEN' (etac conjE THEN' rtac conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
558 |
rtac init_induct THEN' |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
559 |
DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_map'ss))) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
560 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
561 |
|
49501 | 562 |
fun mk_ctor_induct2_tac cTs cts ctor_induct weak_ctor_inducts {context = ctxt, prems = _} = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
563 |
let |
49501 | 564 |
val n = length weak_ctor_inducts; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
565 |
val ks = 1 upto n; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
566 |
fun mk_inner_induct_tac induct i = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
567 |
EVERY' [rtac allI, fo_rtac induct ctxt, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
568 |
select_prem_tac n (dtac @{thm meta_spec2}) i, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
569 |
REPEAT_DETERM_N n o |
49306 | 570 |
EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac, |
571 |
REPEAT_DETERM o dtac @{thm meta_spec}, etac (spec RS meta_mp), atac], |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
572 |
atac]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
573 |
in |
49501 | 574 |
EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts ctor_induct), |
575 |
EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac impI, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
576 |
REPEAT_DETERM o eresolve_tac [conjE, allE], |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
577 |
CONJ_WRAP' (K atac) ks] 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
578 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
579 |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
580 |
fun mk_map_tac m n foldx map_comp_id map_cong0 = |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
581 |
EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, 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
|
582 |
rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong0 RS arg_cong), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
583 |
REPEAT_DETERM_N m o rtac refl, |
49306 | 584 |
REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
585 |
rtac sym, rtac o_apply] 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
586 |
|
52911 | 587 |
fun mk_ctor_map_unique_tac fold_unique sym_map_comps {context = ctxt, prems = _} = |
588 |
rtac fold_unique 1 THEN |
|
589 |
unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc[symmetric] id_o o_id}) THEN |
|
590 |
ALLGOALS atac; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
591 |
|
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
592 |
fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply, |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
593 |
rtac trans, rtac foldx, rtac sym, rtac o_apply] 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
594 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
595 |
fun mk_ctor_set_tac set set_map' set_map's = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
596 |
let |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
597 |
val n = length set_map's; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
598 |
fun mk_UN thm = rtac (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
599 |
rtac @{thm Union_image_eq}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
600 |
in |
52659
58b87aa4dc3b
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents:
52635
diff
changeset
|
601 |
EVERY' [rtac (set RS @{thm comp_eq_dest} RS trans), rtac Un_cong, |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
602 |
rtac (trans OF [set_map', trans_fun_cong_image_id_id_apply]), |
52659
58b87aa4dc3b
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents:
52635
diff
changeset
|
603 |
REPEAT_DETERM_N (n - 1) o rtac Un_cong, |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
604 |
EVERY' (map mk_UN set_map's)] 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
605 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
606 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
607 |
fun mk_set_nat_tac m induct_tac set_map'ss |
49542
b39354db8629
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset
|
608 |
ctor_maps csets ctor_sets i {context = ctxt, prems = _} = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
609 |
let |
49541 | 610 |
val n = length ctor_maps; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
611 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
612 |
fun useIH set_nat = EVERY' [rtac trans, rtac @{thm image_UN}, rtac trans, rtac @{thm UN_cong}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
613 |
rtac refl, Goal.assume_rule_tac ctxt, rtac sym, rtac trans, rtac @{thm UN_cong}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
614 |
rtac set_nat, rtac refl, rtac @{thm UN_simps(10)}]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
615 |
|
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49544
diff
changeset
|
616 |
fun mk_set_nat cset ctor_map ctor_set set_nats = |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49544
diff
changeset
|
617 |
EVERY' [rtac trans, rtac @{thm image_cong}, rtac ctor_set, rtac refl, |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49544
diff
changeset
|
618 |
rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, ctor_set RS trans]), |
52659
58b87aa4dc3b
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents:
52635
diff
changeset
|
619 |
rtac sym, EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
620 |
rtac sym, rtac (nth set_nats (i - 1)), |
52659
58b87aa4dc3b
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents:
52635
diff
changeset
|
621 |
REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
622 |
EVERY' (map useIH (drop m set_nats))]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
623 |
in |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
624 |
(induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_map'ss)) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
625 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
626 |
|
49542
b39354db8629
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset
|
627 |
fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i {context = ctxt, prems = _} = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
628 |
let |
49542
b39354db8629
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset
|
629 |
val n = length ctor_sets; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
630 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
631 |
fun useIH set_bd = EVERY' [rtac @{thm UNION_Cinfinite_bound}, rtac set_bd, rtac ballI, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
632 |
Goal.assume_rule_tac ctxt, rtac bd_Cinfinite]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
633 |
|
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49544
diff
changeset
|
634 |
fun mk_set_nat ctor_set set_bds = |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49544
diff
changeset
|
635 |
EVERY' [rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_ordIso_subst}, rtac ctor_set, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
636 |
rtac (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac (nth set_bds (i - 1)), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
637 |
REPEAT_DETERM_N (n - 1) o rtac (bd_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
|
638 |
EVERY' (map useIH (drop m set_bds))]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
639 |
in |
49542
b39354db8629
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset
|
640 |
(induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
641 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
642 |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
643 |
fun mk_mcong_tac induct_tac set_setsss map_cong0s ctor_maps {context = ctxt, prems = _} = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
644 |
let |
49306 | 645 |
fun use_asm thm = EVERY' [etac bspec, etac set_rev_mp, rtac thm]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
646 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
647 |
fun useIH set_sets = EVERY' [rtac mp, Goal.assume_rule_tac ctxt, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
648 |
CONJ_WRAP' (fn thm => |
49306 | 649 |
EVERY' [rtac ballI, etac bspec, etac set_rev_mp, etac thm]) set_sets]; |
48975
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_map_cong0 ctor_map map_cong0 set_setss = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
652 |
EVERY' [rtac impI, REPEAT_DETERM o etac conjE, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
653 |
rtac trans, rtac ctor_map, rtac trans, rtac (map_cong0 RS arg_cong), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
654 |
EVERY' (map use_asm (map hd set_setss)), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
655 |
EVERY' (map useIH (transpose (map tl set_setss))), |
49541 | 656 |
rtac sym, rtac ctor_map]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
657 |
in |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
51739
diff
changeset
|
658 |
(induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
659 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
660 |
|
51798 | 661 |
fun mk_lfp_map_wpull_tac ctxt m induct_tac wpulls ctor_maps ctor_setss set_setsss ctor_injects = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
662 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
663 |
val n = length wpulls; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
664 |
val ks = 1 upto n; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
665 |
val ls = 1 upto m; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
666 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
667 |
fun use_pass_asm thm = rtac conjI THEN' etac (thm RS subset_trans); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
668 |
fun use_act_asm thm = etac (thm RS subset_trans) THEN' atac; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
669 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
670 |
fun useIH set_sets i = EVERY' [rtac ssubst, rtac @{thm wpull_def}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
671 |
REPEAT_DETERM_N m o etac thin_rl, select_prem_tac n (dtac asm_rl) i, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
672 |
rtac allI, rtac allI, rtac impI, REPEAT_DETERM o etac conjE, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
673 |
REPEAT_DETERM o dtac @{thm meta_spec}, |
49306 | 674 |
dtac meta_mp, atac, |
675 |
dtac meta_mp, atac, etac mp, |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
676 |
rtac conjI, rtac CollectI, CONJ_WRAP' use_act_asm set_sets, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
677 |
rtac conjI, rtac CollectI, CONJ_WRAP' use_act_asm set_sets, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
678 |
atac]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
679 |
|
49306 | 680 |
fun mk_subset thm = EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm Un_least}, atac, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
681 |
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
|
682 |
REPEAT_DETERM_N n o |
49306 | 683 |
EVERY' [rtac @{thm UN_least}, rtac CollectE, etac set_rev_mp, atac, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
684 |
REPEAT_DETERM o etac conjE, atac]]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
685 |
|
49542
b39354db8629
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset
|
686 |
fun mk_wpull wpull ctor_map ctor_sets set_setss ctor_inject = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
687 |
EVERY' [rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
688 |
rtac rev_mp, rtac wpull, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
689 |
EVERY' (map (fn i => REPEAT_DETERM_N (i - 1) o etac thin_rl THEN' atac) ls), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
690 |
EVERY' (map2 useIH (transpose (map tl set_setss)) ks), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
691 |
rtac impI, REPEAT_DETERM_N (m + n) o etac thin_rl, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
692 |
dtac @{thm subst[OF wpull_def, of "%x. x"]}, etac allE, etac allE, etac impE, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
693 |
rtac conjI, rtac CollectI, EVERY' (map (use_pass_asm o hd) set_setss), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
694 |
CONJ_WRAP' (K (rtac subset_refl)) ks, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
695 |
rtac conjI, rtac CollectI, EVERY' (map (use_pass_asm o hd) set_setss), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
696 |
CONJ_WRAP' (K (rtac subset_refl)) ks, |
49541 | 697 |
rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac ctor_map, |
698 |
rtac trans, atac, rtac ctor_map, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], |
|
51798 | 699 |
hyp_subst_tac ctxt, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI, |
49542
b39354db8629
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset
|
700 |
CONJ_WRAP' mk_subset ctor_sets]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
701 |
in |
49542
b39354db8629
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset
|
702 |
(induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps ctor_setss set_setsss ctor_injects)) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
703 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
704 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
705 |
(* BNF tactics *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
706 |
|
53270 | 707 |
fun mk_map_id0_tac map_id0s unique = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
708 |
(rtac sym THEN' rtac unique THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
709 |
EVERY' (map (fn thm => |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
710 |
EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id}, |
53270 | 711 |
rtac (thm RS sym RS arg_cong)]) map_id0s)) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
712 |
|
53287 | 713 |
fun mk_map_comp0_tac map_comp0s ctor_maps unique iplus1 = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
714 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
715 |
val i = iplus1 - 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
716 |
val unique' = Thm.permute_prems 0 i unique; |
53288 | 717 |
val map_comp0s' = drop i map_comp0s @ take i map_comp0s; |
49541 | 718 |
val ctor_maps' = drop i ctor_maps @ take i ctor_maps; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
719 |
fun mk_comp comp simp = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
720 |
EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac o_apply, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
721 |
rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
722 |
rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
723 |
in |
53288 | 724 |
(rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
725 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
726 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
727 |
fun mk_set_map_tac set_nat = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
728 |
EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
729 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
730 |
fun mk_bd_card_order_tac bd_card_orders = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
731 |
(rtac @{thm card_order_cpow} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
732 |
CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
733 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
734 |
fun mk_wpull_tac wpull = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
735 |
EVERY' [rtac ssubst, rtac @{thm wpull_def}, rtac allI, rtac allI, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
736 |
rtac wpull, REPEAT_DETERM o atac] 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
737 |
|
51798 | 738 |
fun mk_wit_tac ctxt n ctor_set wit = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
739 |
REPEAT_DETERM (atac 1 ORELSE |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49544
diff
changeset
|
740 |
EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
741 |
REPEAT_DETERM o |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
742 |
(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
|
743 |
(eresolve_tac wit ORELSE' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
744 |
(dresolve_tac wit THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
745 |
(etac FalseE ORELSE' |
51798 | 746 |
EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
747 |
REPEAT_DETERM_N n o etac UnE]))))] 1); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
748 |
|
53287 | 749 |
fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
750 |
ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
751 |
let |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
752 |
val m = length ctor_set_incls; |
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
753 |
val n = length ctor_set_set_inclss; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
754 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
755 |
val (passive_set_maps, active_set_maps) = chop m set_maps; |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
756 |
val in_Irel = nth in_Irels (i - 1); |
49501 | 757 |
val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans; |
758 |
val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
759 |
val if_tac = |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
760 |
EVERY' [dtac (in_Irel 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:
51812
diff
changeset
|
761 |
rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI, |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
762 |
EVERY' (map2 (fn set_map => fn ctor_set_incl => |
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
763 |
EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map, |
49306 | 764 |
rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply, |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
765 |
rtac (ctor_set_incl RS subset_trans), etac le_arg_cong_ctor_dtor]) |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
766 |
passive_set_maps ctor_set_incls), |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
767 |
CONJ_WRAP' (fn (in_Irel, (set_map, ctor_set_set_incls)) => |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
768 |
EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
769 |
rtac @{thm prod_caseI}, rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
770 |
CONJ_WRAP' (fn thm => |
49501 | 771 |
EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor])) |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
772 |
ctor_set_set_incls, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
773 |
rtac conjI, rtac refl, rtac refl]) |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
774 |
(in_Irels ~~ (active_set_maps ~~ ctor_set_set_inclss)), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
775 |
CONJ_WRAP' (fn conv => |
53287 | 776 |
EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
777 |
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
778 |
REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]), |
49541 | 779 |
rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map, |
49501 | 780 |
etac eq_arg_cong_ctor_dtor]) |
49306 | 781 |
fst_snd_convs]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
782 |
val only_if_tac = |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
783 |
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:
51812
diff
changeset
|
784 |
rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI, |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
785 |
CONJ_WRAP' (fn (ctor_set, passive_set_map) => |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49544
diff
changeset
|
786 |
EVERY' [rtac ord_eq_le_trans, rtac ctor_set, rtac @{thm Un_least}, |
49306 | 787 |
rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]}, |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
788 |
rtac passive_set_map, 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
|
789 |
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
790 |
(fn (active_set_map, in_Irel) => EVERY' [rtac ord_eq_le_trans, |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
791 |
rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map, rtac @{thm UN_least}, |
49306 | 792 |
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:
51812
diff
changeset
|
793 |
dtac @{thm ssubst_mem[OF pair_collapse]}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
794 |
REPEAT_DETERM o eresolve_tac (CollectE :: conjE :: |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
795 |
@{thms prod_caseE iffD1[OF Pair_eq, elim_format]}), |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
796 |
hyp_subst_tac ctxt, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
797 |
dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
798 |
TRY o |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
799 |
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:
51812
diff
changeset
|
800 |
REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac]) |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
801 |
(rev (active_set_maps ~~ in_Irels))]) |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
802 |
(ctor_sets ~~ passive_set_maps), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
803 |
rtac conjI, |
49541 | 804 |
REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2), |
53287 | 805 |
rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
806 |
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
807 |
EVERY' (map (fn in_Irel => 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:
51812
diff
changeset
|
808 |
dtac @{thm ssubst_mem[OF pair_collapse]}, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
809 |
REPEAT_DETERM o |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
810 |
eresolve_tac (CollectE :: conjE :: @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}), |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
811 |
hyp_subst_tac ctxt, |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
812 |
dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51812
diff
changeset
|
813 |
in_Irels), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
814 |
atac]] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
815 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
816 |
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
|
817 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
818 |
|
52506 | 819 |
fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = IHs} = |
51918 | 820 |
let val n = length ks; |
821 |
in |
|
822 |
unfold_tac @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} ctxt THEN |
|
823 |
EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2, |
|
52506 | 824 |
EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong => |
825 |
EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp), |
|
826 |
etac rel_mono_strong, |
|
51918 | 827 |
REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]}, |
828 |
EVERY' (map (fn j => |
|
829 |
EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]}, |
|
830 |
Goal.assume_rule_tac ctxt]) ks)]) |
|
52506 | 831 |
IHs ctor_rels rel_mono_strongs)] 1 |
51918 | 832 |
end; |
833 |
||
52731 | 834 |
fun mk_fold_transfer_tac m rel_induct map_transfers folds {context = ctxt, prems = _} = |
835 |
let |
|
836 |
val n = length map_transfers; |
|
837 |
in |
|
838 |
unfold_thms_tac ctxt |
|
839 |
@{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN |
|
840 |
unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN |
|
841 |
HEADGOAL (EVERY' |
|
842 |
[REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_induct, |
|
843 |
EVERY' (map (fn map_transfer => EVERY' |
|
844 |
[REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}], |
|
845 |
SELECT_GOAL (unfold_thms_tac ctxt folds), |
|
846 |
etac @{thm predicate2D_vimage2p}, |
|
847 |
rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer), |
|
848 |
REPEAT_DETERM_N m o rtac @{thm id_transfer}, |
|
849 |
REPEAT_DETERM_N n o rtac @{thm vimage2p_fun_rel}, |
|
850 |
atac]) |
|
851 |
map_transfers)]) |
|
852 |
end; |
|
853 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
854 |
end; |