17 val mk_comp_set_alt_tac: Proof.context -> thm -> tactic |
17 val mk_comp_set_alt_tac: Proof.context -> thm -> tactic |
18 val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic |
18 val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic |
19 val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic |
19 val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic |
20 val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic |
20 val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic |
21 |
21 |
22 val mk_kill_bd_card_order_tac: int -> thm -> tactic |
|
23 val mk_kill_bd_cinfinite_tac: thm -> tactic |
|
24 val kill_in_alt_tac: tactic |
22 val kill_in_alt_tac: tactic |
25 val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic |
23 val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic |
26 val mk_kill_set_bd_tac: thm -> thm -> tactic |
|
27 |
24 |
28 val empty_natural_tac: tactic |
25 val empty_natural_tac: tactic |
29 val lift_in_alt_tac: tactic |
26 val lift_in_alt_tac: tactic |
30 val mk_lift_set_bd_tac: thm -> tactic |
27 val mk_lift_set_bd_tac: thm -> tactic |
31 |
28 |
40 struct |
37 struct |
41 |
38 |
42 open BNF_Util |
39 open BNF_Util |
43 open BNF_Tactics |
40 open BNF_Tactics |
44 |
41 |
45 val Cnotzero_UNIV = @{thm Cnotzero_UNIV}; |
|
46 val arg_cong_Union = @{thm arg_cong[of _ _ Union]}; |
42 val arg_cong_Union = @{thm arg_cong[of _ _ Union]}; |
47 val comp_eq_dest_lhs = @{thm comp_eq_dest_lhs}; |
43 val comp_eq_dest_lhs = @{thm comp_eq_dest_lhs}; |
48 val csum_Cnotzero1 = @{thm csum_Cnotzero1}; |
|
49 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]}; |
44 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]}; |
50 val trans_o_apply = @{thm trans[OF o_apply]}; |
45 val trans_o_apply = @{thm trans[OF o_apply]}; |
51 |
46 |
52 |
47 |
53 |
48 |
178 |
173 |
179 fun mk_kill_map_cong0_tac ctxt n m map_cong0 = |
174 fun mk_kill_map_cong0_tac ctxt n m map_cong0 = |
180 (rtac map_cong0 THEN' EVERY' (replicate n (rtac refl)) THEN' |
175 (rtac map_cong0 THEN' EVERY' (replicate n (rtac refl)) THEN' |
181 EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1; |
176 EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1; |
182 |
177 |
183 fun mk_kill_bd_card_order_tac n bd_card_order = |
|
184 (rtac @{thm card_order_cprod} THEN' |
|
185 K (REPEAT_DETERM_N (n - 1) |
|
186 ((rtac @{thm card_order_csum} THEN' |
|
187 rtac @{thm card_of_card_order_on}) 1)) THEN' |
|
188 rtac @{thm card_of_card_order_on} THEN' |
|
189 rtac bd_card_order) 1; |
|
190 |
|
191 fun mk_kill_bd_cinfinite_tac bd_Cinfinite = |
|
192 (rtac @{thm cinfinite_cprod2} THEN' |
|
193 TRY o rtac csum_Cnotzero1 THEN' |
|
194 rtac Cnotzero_UNIV THEN' |
|
195 rtac bd_Cinfinite) 1; |
|
196 |
|
197 fun mk_kill_set_bd_tac bd_Card_order set_bd = |
|
198 (rtac ctrans THEN' |
|
199 rtac set_bd THEN' |
|
200 rtac @{thm ordLeq_cprod2} THEN' |
|
201 TRY o rtac csum_Cnotzero1 THEN' |
|
202 rtac Cnotzero_UNIV THEN' |
|
203 rtac bd_Card_order) 1 |
|
204 |
|
205 val kill_in_alt_tac = |
178 val kill_in_alt_tac = |
206 ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN |
179 ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN |
207 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
180 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
208 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' |
181 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' |
209 rtac conjI THEN' rtac subset_UNIV) 1)) THEN |
182 rtac conjI THEN' rtac subset_UNIV) 1)) THEN |