author | blanchet |
Tue, 30 Apr 2013 12:13:28 +0200 | |
changeset 51832 | 35911d5acfa9 |
parent 51798 | ad3a241def73 |
child 51893 | 596baae88a88 |
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_comp_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: Jasmin Blanchette, 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 composition of bounded natural functors. |
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_COMP_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_comp_bd_card_order_tac: thm list -> thm -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
val mk_comp_bd_cinfinite_tac: thm -> thm -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
val mk_comp_in_bd_tac: thm -> thm list -> thm -> thm list -> thm -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
15 |
val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
16 |
val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic |
49630 | 17 |
val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
18 |
val mk_comp_set_alt_tac: Proof.context -> thm -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
19 |
val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
20 |
val mk_comp_set_map_tac: thm -> thm -> thm -> thm list -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
21 |
val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
22 |
|
49304 | 23 |
val mk_kill_bd_card_order_tac: int -> thm -> tactic |
24 |
val mk_kill_bd_cinfinite_tac: thm -> tactic |
|
25 |
val kill_in_alt_tac: tactic |
|
26 |
val mk_kill_in_bd_tac: int -> bool -> thm -> thm -> thm -> thm -> thm -> tactic |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
27 |
val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic |
49304 | 28 |
val mk_kill_set_bd_tac: thm -> thm -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
29 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
val empty_natural_tac: tactic |
49304 | 31 |
val lift_in_alt_tac: tactic |
32 |
val mk_lift_in_bd_tac: int -> thm -> thm -> thm -> tactic |
|
33 |
val mk_lift_set_bd_tac: thm -> tactic |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
34 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
35 |
val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
36 |
val mk_permute_in_bd_tac: ''a list -> ''a list -> thm -> thm -> thm -> tactic |
49284 | 37 |
|
38 |
val mk_map_wpull_tac: thm -> thm list -> thm -> tactic |
|
49506 | 39 |
val mk_simple_srel_O_Gr_tac: Proof.context -> thm -> thm -> thm -> tactic |
49284 | 40 |
val mk_simple_wit_tac: thm list -> tactic |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
41 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
42 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
structure BNF_Comp_Tactics : BNF_COMP_TACTICS = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
44 |
struct |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
45 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
open BNF_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
47 |
open BNF_Tactics |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
|
49305 | 49 |
val Card_order_csum = @{thm Card_order_csum}; |
50 |
val Card_order_ctwo = @{thm Card_order_ctwo}; |
|
51 |
val Cnotzero_UNIV = @{thm Cnotzero_UNIV}; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
val arg_cong_Union = @{thm arg_cong[of _ _ Union]}; |
49305 | 53 |
val card_of_Card_order = @{thm card_of_Card_order}; |
54 |
val csum_Cnotzero1 = @{thm csum_Cnotzero1}; |
|
55 |
val csum_Cnotzero2 = @{thm csum_Cnotzero2}; |
|
56 |
val ctwo_Cnotzero = @{thm ctwo_Cnotzero}; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
val o_eq_dest_lhs = @{thm o_eq_dest_lhs}; |
49305 | 58 |
val ordIso_transitive = @{thm ordIso_transitive}; |
59 |
val ordLeq_csum2 = @{thm ordLeq_csum2}; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
60 |
val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
61 |
val trans_o_apply = @{thm trans[OF o_apply]}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
62 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
63 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
65 |
(* Composition *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
66 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
67 |
fun mk_comp_set_alt_tac ctxt collect_set_map = |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49490
diff
changeset
|
68 |
unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
69 |
unfold_thms_tac ctxt [collect_set_map RS sym] THEN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
70 |
rtac refl 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
72 |
fun mk_comp_map_id_tac Gmap_id Gmap_cong0 map_ids = |
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
73 |
EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @ |
49630 | 74 |
map (fn thm => rtac (thm RS fun_cong)) map_ids @ [rtac (Gmap_id RS fun_cong)]) 1; |
75 |
||
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
76 |
fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
77 |
EVERY' ([rtac ext, rtac sym, rtac trans_o_apply, |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
78 |
rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @ |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
map (fn thm => rtac (thm RS sym RS fun_cong)) map_comps) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
80 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
81 |
fun mk_comp_set_map_tac Gmap_comp Gmap_cong0 Gset_map set_maps = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
EVERY' ([rtac ext] @ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
83 |
replicate 3 (rtac trans_o_apply) @ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
84 |
[rtac (arg_cong_Union RS trans), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
85 |
rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
87 |
rtac Gmap_cong0] @ |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
88 |
map (fn thm => rtac (thm RS fun_cong)) set_maps @ |
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
89 |
[rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply, |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
91 |
rtac (@{thm image_cong} OF [Gset_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
92 |
rtac @{thm trans[OF pointfreeE[OF Union_natural[symmetric]]]}, rtac arg_cong_Union, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
93 |
rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
94 |
rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @ |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
95 |
[REPEAT_DETERM_N (length set_maps) o EVERY' [rtac @{thm trans[OF image_insert]}, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
96 |
rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply, |
49305 | 97 |
rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]}, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
98 |
rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}], |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
99 |
rtac @{thm image_empty}]) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
100 |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
101 |
fun mk_comp_map_cong0_tac comp_set_alts map_cong0 map_cong0s = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
102 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
103 |
val n = length comp_set_alts; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
104 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
105 |
(if n = 0 then rtac refl 1 |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
106 |
else rtac map_cong0 1 THEN |
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
107 |
EVERY' (map_index (fn (i, map_cong0) => |
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
108 |
rtac map_cong0 THEN' EVERY' (map_index (fn (k, set_alt) => |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49512
diff
changeset
|
109 |
EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac meta_mp, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
110 |
rtac (equalityD2 RS set_mp), rtac (set_alt RS fun_cong RS trans), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
111 |
rtac trans_o_apply, rtac (@{thm collect_def} RS arg_cong_Union), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
112 |
rtac @{thm UnionI}, rtac @{thm UN_I}, REPEAT_DETERM_N i o rtac @{thm insertI2}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
113 |
rtac @{thm insertI1}, rtac (o_apply RS equalityD2 RS set_mp), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
114 |
etac @{thm imageI}, atac]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
115 |
comp_set_alts)) |
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
116 |
map_cong0s) 1) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
117 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
118 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
119 |
fun mk_comp_bd_card_order_tac Fbd_card_orders Gbd_card_order = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
120 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
121 |
val (card_orders, last_card_order) = split_last Fbd_card_orders; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
122 |
fun gen_before thm = rtac @{thm card_order_csum} THEN' rtac thm; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
123 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
124 |
(rtac @{thm card_order_cprod} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
125 |
WRAP' gen_before (K (K all_tac)) card_orders (rtac last_card_order) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
126 |
rtac Gbd_card_order) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
127 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
128 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
129 |
fun mk_comp_bd_cinfinite_tac Fbd_cinfinite Gbd_cinfinite = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
130 |
(rtac @{thm cinfinite_cprod} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
131 |
((K (TRY ((rtac @{thm cinfinite_csum} THEN' rtac disjI1) 1)) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
132 |
((rtac @{thm cinfinite_csum} THEN' rtac disjI1 THEN' rtac Fbd_cinfinite) ORELSE' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
133 |
rtac Fbd_cinfinite)) ORELSE' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
134 |
rtac Fbd_cinfinite) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
135 |
rtac Gbd_cinfinite) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
136 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
137 |
fun mk_comp_set_bd_tac ctxt comp_set_alt Gset_Fset_bds = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
138 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
139 |
val (bds, last_bd) = split_last Gset_Fset_bds; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
140 |
fun gen_before bd = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
141 |
rtac ctrans THEN' rtac @{thm Un_csum} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
142 |
rtac ctrans THEN' rtac @{thm csum_mono} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
143 |
rtac bd; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
144 |
fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
145 |
in |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49490
diff
changeset
|
146 |
unfold_thms_tac ctxt [comp_set_alt] THEN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
147 |
rtac @{thm comp_set_bd_Union_o_collect} 1 THEN |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49490
diff
changeset
|
148 |
unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
149 |
(rtac ctrans THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
150 |
WRAP' gen_before gen_after bds (rtac last_bd) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
151 |
rtac @{thm ordIso_imp_ordLeq} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
152 |
rtac @{thm cprod_com}) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
153 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
154 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
155 |
val comp_in_alt_thms = @{thms o_apply collect_def SUP_def image_insert image_empty Union_insert |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
156 |
Union_empty Un_empty_right Union_Un_distrib Un_subset_iff conj_subset_def UN_image_subset |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
157 |
conj_assoc}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
158 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
159 |
fun mk_comp_in_alt_tac ctxt comp_set_alts = |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49490
diff
changeset
|
160 |
unfold_thms_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49490
diff
changeset
|
161 |
unfold_thms_tac ctxt @{thms set_eq_subset} THEN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
162 |
rtac conjI 1 THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
163 |
REPEAT_DETERM ( |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
164 |
rtac @{thm subsetI} 1 THEN |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49490
diff
changeset
|
165 |
unfold_thms_tac ctxt @{thms mem_Collect_eq Ball_def} THEN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
166 |
(REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
167 |
REPEAT_DETERM (CHANGED (( |
49305 | 168 |
(rtac conjI THEN' (atac ORELSE' rtac subset_UNIV)) ORELSE' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
169 |
atac ORELSE' |
49305 | 170 |
(rtac subset_UNIV)) 1)) ORELSE rtac subset_UNIV 1)); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
171 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
172 |
fun mk_comp_in_bd_tac comp_in_alt Fin_bds Gin_bd Fbd_Cinfs Gbd_Card_order = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
173 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
174 |
val (bds, last_bd) = split_last Fin_bds; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
175 |
val (Cinfs, _) = split_last Fbd_Cinfs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
176 |
fun gen_before (bd, _) = rtac ctrans THEN' rtac @{thm csum_mono} THEN' rtac bd; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
177 |
fun gen_after (_, (bd_Cinf, next_bd_Cinf)) = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
178 |
TRY o (rtac @{thm csum_cexp} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
179 |
rtac bd_Cinf THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
180 |
(TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac next_bd_Cinf ORELSE' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
181 |
rtac next_bd_Cinf) THEN' |
49305 | 182 |
((rtac Card_order_csum THEN' rtac ordLeq_csum2) ORELSE' |
183 |
(rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl})) THEN' |
|
184 |
rtac Card_order_ctwo); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
185 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
186 |
(rtac @{thm ordIso_ordLeq_trans} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
187 |
rtac @{thm card_of_ordIso_subst} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
188 |
rtac comp_in_alt THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
189 |
rtac ctrans THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
190 |
rtac Gin_bd THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
191 |
rtac @{thm ordLeq_ordIso_trans} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
192 |
rtac @{thm cexp_mono1} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
193 |
rtac @{thm ordLeq_ordIso_trans} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
194 |
rtac @{thm csum_mono1} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
195 |
WRAP' gen_before gen_after (bds ~~ (Cinfs ~~ tl Fbd_Cinfs)) (rtac last_bd) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
196 |
rtac @{thm csum_absorb1} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
197 |
rtac @{thm Cinfinite_cexp} THEN' |
49305 | 198 |
(rtac ordLeq_csum2 ORELSE' rtac @{thm ordLeq_refl}) THEN' |
199 |
rtac Card_order_ctwo THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
200 |
(TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
201 |
rtac (hd Fbd_Cinfs)) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
202 |
rtac @{thm ctwo_ordLeq_Cinfinite} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
203 |
rtac @{thm Cinfinite_cexp} THEN' |
49305 | 204 |
(rtac ordLeq_csum2 ORELSE' rtac @{thm ordLeq_refl}) THEN' |
205 |
rtac Card_order_ctwo THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
206 |
(TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
207 |
rtac (hd Fbd_Cinfs)) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
208 |
rtac Gbd_Card_order THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
209 |
rtac @{thm cexp_cprod} THEN' |
51782
84e7225f5ab6
removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents:
51766
diff
changeset
|
210 |
rtac @{thm Card_order_csum}) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
211 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
212 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
213 |
val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
214 |
Union_image_insert Union_image_empty}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
215 |
|
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
216 |
fun mk_comp_wit_tac ctxt Gwit_thms collect_set_map Fwit_thms = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
217 |
ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN |
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51761
diff
changeset
|
218 |
unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
219 |
REPEAT_DETERM ( |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
220 |
atac 1 ORELSE |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
221 |
REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
222 |
(TRY o dresolve_tac Gwit_thms THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
223 |
(etac FalseE ORELSE' |
51798 | 224 |
hyp_subst_tac ctxt THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
225 |
dresolve_tac Fwit_thms THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
226 |
(etac FalseE ORELSE' atac))) 1); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
227 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
228 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
229 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
230 |
(* Kill operation *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
231 |
|
51761
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
232 |
fun mk_kill_map_cong0_tac ctxt n m map_cong0 = |
4c9f08836d87
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents:
49630
diff
changeset
|
233 |
(rtac map_cong0 THEN' EVERY' (replicate n (rtac refl)) THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
234 |
EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
235 |
|
49304 | 236 |
fun mk_kill_bd_card_order_tac n bd_card_order = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
237 |
(rtac @{thm card_order_cprod} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
238 |
K (REPEAT_DETERM_N (n - 1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
239 |
((rtac @{thm card_order_csum} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
240 |
rtac @{thm card_of_card_order_on}) 1)) THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
241 |
rtac @{thm card_of_card_order_on} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
242 |
rtac bd_card_order) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
243 |
|
49304 | 244 |
fun mk_kill_bd_cinfinite_tac bd_Cinfinite = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
245 |
(rtac @{thm cinfinite_cprod2} THEN' |
49305 | 246 |
TRY o rtac csum_Cnotzero1 THEN' |
247 |
rtac Cnotzero_UNIV THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
248 |
rtac bd_Cinfinite) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
249 |
|
49304 | 250 |
fun mk_kill_set_bd_tac bd_Card_order set_bd = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
251 |
(rtac ctrans THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
252 |
rtac set_bd THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
253 |
rtac @{thm ordLeq_cprod2} THEN' |
49305 | 254 |
TRY o rtac csum_Cnotzero1 THEN' |
255 |
rtac Cnotzero_UNIV THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
256 |
rtac bd_Card_order) 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
257 |
|
49304 | 258 |
val kill_in_alt_tac = |
49305 | 259 |
((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
260 |
REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
261 |
REPEAT_DETERM (CHANGED ((etac conjI ORELSE' |
49305 | 262 |
rtac conjI THEN' rtac subset_UNIV) 1)) THEN |
263 |
(rtac subset_UNIV ORELSE' atac) 1 THEN |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
264 |
REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
265 |
REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1))) ORELSE |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
266 |
((rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN |
49305 | 267 |
REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac subset_UNIV 1)); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
268 |
|
49304 | 269 |
fun mk_kill_in_bd_tac n nontrivial_kill_in in_alt in_bd bd_Card_order bd_Cinfinite bd_Cnotzero = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
270 |
(rtac @{thm ordIso_ordLeq_trans} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
271 |
rtac @{thm card_of_ordIso_subst} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
272 |
rtac in_alt THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
273 |
rtac ctrans THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
274 |
rtac in_bd THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
275 |
rtac @{thm ordIso_ordLeq_trans} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
276 |
rtac @{thm cexp_cong1}) 1 THEN |
49304 | 277 |
(if nontrivial_kill_in then |
49305 | 278 |
rtac ordIso_transitive 1 THEN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
279 |
REPEAT_DETERM_N (n - 1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
280 |
((rtac @{thm csum_cong1} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
281 |
rtac @{thm ordIso_symmetric} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
282 |
rtac @{thm csum_assoc} THEN' |
49305 | 283 |
rtac ordIso_transitive) 1) THEN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
284 |
(rtac @{thm ordIso_refl} THEN' |
49305 | 285 |
rtac Card_order_csum THEN' |
286 |
rtac ordIso_transitive THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
287 |
rtac @{thm csum_assoc} THEN' |
49305 | 288 |
rtac ordIso_transitive THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
289 |
rtac @{thm csum_cong1} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
290 |
K (mk_flatten_assoc_tac |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
291 |
(rtac @{thm ordIso_refl} THEN' |
49305 | 292 |
FIRST' [rtac card_of_Card_order, rtac Card_order_csum]) |
293 |
ordIso_transitive @{thm csum_assoc} @{thm csum_cong}) THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
294 |
rtac @{thm ordIso_refl} THEN' |
49305 | 295 |
(rtac card_of_Card_order ORELSE' rtac Card_order_csum)) 1 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
296 |
else all_tac) THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
297 |
(rtac @{thm csum_com} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
298 |
rtac bd_Card_order THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
299 |
rtac @{thm ordLeq_ordIso_trans} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
300 |
rtac @{thm cexp_mono1} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
301 |
rtac ctrans THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
302 |
rtac @{thm csum_mono2} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
303 |
rtac @{thm ordLeq_cprod1} THEN' |
49305 | 304 |
(rtac card_of_Card_order ORELSE' rtac Card_order_csum) THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
305 |
rtac bd_Cnotzero THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
306 |
rtac @{thm csum_cexp'} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
307 |
rtac @{thm Cinfinite_cprod2} THEN' |
49305 | 308 |
TRY o rtac csum_Cnotzero1 THEN' |
309 |
rtac Cnotzero_UNIV THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
310 |
rtac bd_Cinfinite THEN' |
49305 | 311 |
((rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl}) ORELSE' |
312 |
(rtac Card_order_csum THEN' rtac ordLeq_csum2)) THEN' |
|
313 |
rtac Card_order_ctwo THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
314 |
rtac bd_Card_order THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
315 |
rtac @{thm cexp_cprod_ordLeq} THEN' |
51782
84e7225f5ab6
removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents:
51766
diff
changeset
|
316 |
resolve_tac @{thms Card_order_csum Card_order_ctwo} THEN' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
317 |
rtac @{thm Cinfinite_cprod2} THEN' |
49305 | 318 |
TRY o rtac csum_Cnotzero1 THEN' |
319 |
rtac Cnotzero_UNIV THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
320 |
rtac bd_Cinfinite THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
321 |
rtac bd_Cnotzero THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
322 |
rtac @{thm ordLeq_cprod2} THEN' |
49305 | 323 |
TRY o rtac csum_Cnotzero1 THEN' |
324 |
rtac Cnotzero_UNIV THEN' |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
325 |
rtac bd_Card_order) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
326 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
327 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
328 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
329 |
(* Lift operation *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
330 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
331 |
val empty_natural_tac = rtac @{thm empty_natural} 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
332 |
|
49304 | 333 |
fun mk_lift_set_bd_tac bd_Card_order = (rtac @{thm Card_order_empty} THEN' rtac bd_Card_order) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
334 |
|
49304 | 335 |
val lift_in_alt_tac = |
49305 | 336 |
((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
337 |
REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
338 |
REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1)) THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
339 |
REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
340 |
REPEAT_DETERM (CHANGED ((etac conjI ORELSE' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
341 |
rtac conjI THEN' rtac @{thm empty_subsetI}) 1)) THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
342 |
(rtac @{thm empty_subsetI} ORELSE' atac) 1) ORELSE |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
343 |
((rtac sym THEN' rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
344 |
REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm empty_subsetI} 1)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
345 |
|
49304 | 346 |
fun mk_lift_in_bd_tac n in_alt in_bd bd_Card_order = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
347 |
(rtac @{thm ordIso_ordLeq_trans} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
348 |
rtac @{thm card_of_ordIso_subst} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
349 |
rtac in_alt THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
350 |
rtac ctrans THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
351 |
rtac in_bd THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
352 |
rtac @{thm cexp_mono1}) 1 THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
353 |
((rtac @{thm csum_mono1} 1 THEN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
354 |
REPEAT_DETERM_N (n - 1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
355 |
((rtac ctrans THEN' |
49305 | 356 |
rtac ordLeq_csum2 THEN' |
357 |
(rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) THEN |
|
358 |
(rtac ordLeq_csum2 THEN' |
|
359 |
(rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) ORELSE |
|
360 |
(rtac ordLeq_csum2 THEN' rtac Card_order_ctwo) 1) THEN |
|
51782
84e7225f5ab6
removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents:
51766
diff
changeset
|
361 |
(rtac bd_Card_order) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
362 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
363 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
364 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
365 |
(* Permute operation *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
366 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
367 |
fun mk_permute_in_alt_tac src dest = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
368 |
(rtac @{thm Collect_cong} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
369 |
mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
370 |
dest src) 1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
371 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
372 |
fun mk_permute_in_bd_tac src dest in_alt in_bd bd_Card_order = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
373 |
(rtac @{thm ordIso_ordLeq_trans} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
374 |
rtac @{thm card_of_ordIso_subst} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
375 |
rtac in_alt THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
376 |
rtac @{thm ordLeq_ordIso_trans} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
377 |
rtac in_bd THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
378 |
rtac @{thm cexp_cong1} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
379 |
rtac @{thm csum_cong1} THEN' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
380 |
mk_rotate_eq_tac |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
381 |
(rtac @{thm ordIso_refl} THEN' |
49305 | 382 |
FIRST' [rtac card_of_Card_order, rtac Card_order_csum]) |
383 |
ordIso_transitive @{thm csum_assoc} @{thm csum_com} @{thm csum_cong} |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
384 |
src dest THEN' |
51782
84e7225f5ab6
removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents:
51766
diff
changeset
|
385 |
rtac bd_Card_order) 1; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
386 |
|
49284 | 387 |
fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull = |
388 |
(rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN |
|
389 |
WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN |
|
390 |
TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1)); |
|
391 |
||
49506 | 392 |
fun mk_simple_srel_O_Gr_tac ctxt srel_def srel_O_Gr in_alt_thm = |
393 |
rtac (unfold_thms ctxt [srel_def] |
|
49512 | 394 |
(trans OF [srel_O_Gr, in_alt_thm RS @{thm O_Gr_cong} RS sym])) 1; |
49463 | 395 |
|
49284 | 396 |
fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms)); |
397 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
398 |
end; |