isabelle: src/HOL/Tools/BNF/bnf_comp_tactics.ML@89c20f7f3b3b (annotated)

55061 a0adf838e2d1 adjusted comments blanchet parents: 55060 diff changeset	1	(* Title: HOL/Tools/BNF/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
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	11	val mk_comp_bd_card_order_tac: Proof.context -> thm list -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	12	val mk_comp_bd_cinfinite_tac: Proof.context -> thm -> thm -> tactic
75624 22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	13	val mk_comp_bd_regularCard_tac: Proof.context -> thm list -> thm -> thm list -> thm -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	14	val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	15	val mk_comp_map_comp0_tac: Proof.context -> thm -> thm -> thm list -> tactic
55906 abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	16	val mk_comp_map_cong0_tac: Proof.context -> thm list -> thm list -> thm -> thm list -> tactic
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	17	val mk_comp_map_id0_tac: Proof.context -> 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
75624 22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	19	val mk_comp_set_bd_tac: Proof.context -> thm -> thm option -> thm -> thm list -> thm list -> tactic
55906 abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	20	val mk_comp_set_map0_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	21	val mk_comp_wit_tac: Proof.context -> thm list -> thm list -> thm -> thm list -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	22
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	23	val kill_in_alt_tac: Proof.context -> tactic
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 49630 diff changeset	24	val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	25
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	26	val empty_natural_tac: Proof.context -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	27	val lift_in_alt_tac: Proof.context -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	28	val mk_lift_set_bd_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	29
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	30	val mk_permute_in_alt_tac: Proof.context -> ''a list -> ''a list -> tactic
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: 48975 diff changeset	31
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	32	val mk_le_rel_OO_tac: Proof.context -> thm -> thm -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	33	val mk_simple_rel_OO_Grp_tac: Proof.context -> thm -> thm -> tactic
62324 ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61760 diff changeset	34	val mk_simple_pred_set_tac: Proof.context -> thm -> thm -> tactic
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	35	val mk_simple_wit_tac: Proof.context -> thm list -> tactic
55930 25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms traytel parents: 55906 diff changeset	36	val mk_simplified_set_tac: Proof.context -> thm -> tactic
60757 c09598a97436 prefer tactics with explicit context; wenzelm parents: 60752 diff changeset	37	val bd_ordIso_natLeq_tac: Proof.context -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	38	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	39
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	40	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	41	struct
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	open BNF_Util
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	44	open BNF_Tactics
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	val arg_cong_Union = @{thm arg_cong[of _ _ Union]};
55067 a452de24a877 tuned names blanchet parents: 55061 diff changeset	47	val comp_eq_dest_lhs = @{thm comp_eq_dest_lhs};
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	48	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	49	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	50
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	51
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	52	(* Composition *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	53
51766 f19a4d0ab1bf renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus blanchet parents: 51761 diff changeset	54	fun mk_comp_set_alt_tac ctxt collect_set_map =
55067 a452de24a877 tuned names blanchet parents: 55061 diff changeset	55	unfold_thms_tac ctxt @{thms comp_assoc} THEN
51766 f19a4d0ab1bf renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus blanchet parents: 51761 diff changeset	56	unfold_thms_tac ctxt [collect_set_map RS sym] THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	57	rtac ctxt refl 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	58
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	59	fun mk_comp_map_id0_tac ctxt Gmap_id0 Gmap_cong0 map_id0s =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	60	EVERY' ([rtac ctxt @{thm ext}, rtac ctxt (Gmap_cong0 RS trans)] @
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	61	map (fn thm => rtac ctxt (thm RS fun_cong)) map_id0s @ [rtac ctxt (Gmap_id0 RS fun_cong)]) 1;
49630 9f6ca87ab405 tuned tactics traytel parents: 49585 diff changeset	62
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	63	fun mk_comp_map_comp0_tac ctxt Gmap_comp0 Gmap_cong0 map_comp0s =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	64	EVERY' ([rtac ctxt @{thm ext}, rtac ctxt sym, rtac ctxt trans_o_apply,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	65	rtac ctxt (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans), rtac ctxt Gmap_cong0] @
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	66	map (fn thm => rtac ctxt (thm RS sym RS fun_cong)) map_comp0s) 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	67
55906 abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	68	fun mk_comp_set_map0_tac ctxt set'_eq_set Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s =
abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	69	unfold_thms_tac ctxt [set'_eq_set] THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	70	EVERY' ([rtac ctxt @{thm ext}] @
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	71	replicate 3 (rtac ctxt trans_o_apply) @
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	72	[rtac ctxt (arg_cong_Union RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	73	rtac ctxt (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	74	rtac ctxt (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	75	rtac ctxt Gmap_cong0] @
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	76	map (fn thm => rtac ctxt (thm RS fun_cong)) set_map0s @
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	77	[rtac ctxt (Gset_map0 RS comp_eq_dest_lhs), rtac ctxt sym, rtac ctxt trans_o_apply,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	78	rtac ctxt trans_image_cong_o_apply, rtac ctxt trans_image_cong_o_apply,
61760 1647bb489522 tuned whitespace blanchet parents: 60757 diff changeset	79	rtac ctxt (@{thm image_cong} OF [Gset_map0 RS comp_eq_dest_lhs RS arg_cong_Union, refl]
1647bb489522 tuned whitespace blanchet parents: 60757 diff changeset	80	RS trans),
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	81	rtac ctxt @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac ctxt arg_cong_Union,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	82	rtac ctxt @{thm trans[OF comp_eq_dest_lhs[OF image_o_collect[symmetric]]]},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	83	rtac ctxt @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	84	[REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac ctxt @{thm trans[OF image_insert]},
61760 1647bb489522 tuned whitespace blanchet parents: 60757 diff changeset	85	rtac ctxt @{thm arg_cong2[of _ _ _ _ insert]}, rtac ctxt @{thm ext},
1647bb489522 tuned whitespace blanchet parents: 60757 diff changeset	86	rtac ctxt trans_o_apply, rtac ctxt trans_image_cong_o_apply,
1647bb489522 tuned whitespace blanchet parents: 60757 diff changeset	87	rtac ctxt @{thm trans[OF image_image]}, rtac ctxt @{thm sym[OF trans[OF o_apply]]},
1647bb489522 tuned whitespace blanchet parents: 60757 diff changeset	88	rtac ctxt @{thm image_cong[OF refl o_apply]}],
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	89	rtac ctxt @{thm image_empty}]) 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	90
55906 abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	91	fun mk_comp_map_cong0_tac ctxt set'_eq_sets 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	92	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	93	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	94	in
55906 abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	95	unfold_thms_tac ctxt set'_eq_sets THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	96	(if n = 0 then rtac ctxt refl 1
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	97	else rtac ctxt map_cong0 1 THEN
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 49630 diff changeset	98	EVERY' (map_index (fn (i, map_cong0) =>
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	99	rtac ctxt map_cong0 THEN' EVERY' (map_index (fn (k, set_alt) =>
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	100	EVERY' [select_prem_tac ctxt n (dtac ctxt @{thm meta_spec}) (k + 1), etac ctxt meta_mp,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	101	rtac ctxt (equalityD2 RS set_mp), rtac ctxt (set_alt RS fun_cong RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	102	rtac ctxt trans_o_apply, rtac ctxt (@{thm collect_def} RS arg_cong_Union),
61760 1647bb489522 tuned whitespace blanchet parents: 60757 diff changeset	103	rtac ctxt @{thm UnionI}, rtac ctxt @{thm UN_I},
1647bb489522 tuned whitespace blanchet parents: 60757 diff changeset	104	REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1},
1647bb489522 tuned whitespace blanchet parents: 60757 diff changeset	105	rtac ctxt (o_apply RS equalityD2 RS set_mp), etac ctxt @{thm imageI}, assume_tac ctxt])
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	106	comp_set_alts))
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 49630 diff changeset	107	map_cong0s) 1)
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	108	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	109
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	110	fun mk_comp_bd_card_order_tac ctxt Fbd_card_orders Gbd_card_order =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	111	rtac ctxt @{thm natLeq_card_order} 1 ORELSE
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	112	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	113	val (card_orders, last_card_order) = split_last Fbd_card_orders;
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	114	fun gen_before thm = rtac ctxt @{thm card_order_csum} THEN' rtac ctxt thm;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	115	in
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	116	(rtac ctxt @{thm card_order_cprod} THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	117	WRAP' gen_before (K (K all_tac)) card_orders (rtac ctxt last_card_order) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	118	rtac ctxt Gbd_card_order) 1
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	119	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	120
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	121	fun mk_comp_bd_cinfinite_tac ctxt Fbd_cinfinite Gbd_cinfinite =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	122	(rtac ctxt @{thm natLeq_cinfinite} ORELSE'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	123	rtac ctxt @{thm cinfinite_cprod} THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	124	((K (TRY ((rtac ctxt @{thm cinfinite_csum} THEN' rtac ctxt disjI1) 1)) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	125	((rtac ctxt @{thm cinfinite_csum} THEN' rtac ctxt disjI1 THEN' rtac ctxt Fbd_cinfinite) ORELSE'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	126	rtac ctxt Fbd_cinfinite)) ORELSE'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	127	rtac ctxt Fbd_cinfinite) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	128	rtac ctxt Gbd_cinfinite) 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	129
75624 22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	130	fun mk_comp_bd_regularCard_tac ctxt Fbd_regularCards Gbd_regularCard Fbd_Cinfinites Gbd_Cinfinite =
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	131	rtac ctxt @{thm regularCard_natLeq} 1 ORELSE
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	132	EVERY1 [
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	133	rtac ctxt @{thm regularCard_cprod},
75625 0dd3ac5fdbaa tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS traytel parents: 75624 diff changeset	134	resolve_tac ctxt (Fbd_Cinfinites) ORELSE'
0dd3ac5fdbaa tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS traytel parents: 75624 diff changeset	135	((TRY o rtac ctxt @{thm Cinfinite_csum1}) THEN'
0dd3ac5fdbaa tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS traytel parents: 75624 diff changeset	136	resolve_tac ctxt (Fbd_Cinfinites)),
75624 22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	137	rtac ctxt Gbd_Cinfinite,
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	138	REPEAT_DETERM o EVERY' [
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	139	rtac ctxt @{thm regularCard_csum},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	140	resolve_tac ctxt Fbd_Cinfinites,
75625 0dd3ac5fdbaa tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS traytel parents: 75624 diff changeset	141	resolve_tac ctxt (Fbd_Cinfinites) ORELSE'
0dd3ac5fdbaa tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS traytel parents: 75624 diff changeset	142	((TRY o rtac ctxt @{thm Cinfinite_csum1}) THEN'
0dd3ac5fdbaa tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS traytel parents: 75624 diff changeset	143	resolve_tac ctxt (Fbd_Cinfinites)),
75624 22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	144	resolve_tac ctxt Fbd_regularCards
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	145	],
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	146	resolve_tac ctxt Fbd_regularCards,
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	147	rtac ctxt Gbd_regularCard
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	148	];
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	149
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	150	fun mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_opt comp_set_alt Gset_Fset_bds Gbd_Fbd_Cinfinites =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	151	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	152	val (bds, last_bd) = split_last Gset_Fset_bds;
75624 22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	153	fun gen_before bd = EVERY' [
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	154	rtac ctxt @{thm ordLeq_ordLess_trans},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	155	rtac ctxt @{thm Un_csum},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	156	rtac ctxt @{thm csum_mono_strict},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	157	rtac ctxt @{thm card_of_Card_order},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	158	rtac ctxt @{thm card_of_Card_order},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	159	resolve_tac ctxt Gbd_Fbd_Cinfinites,
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	160	defer_tac,
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	161	rtac ctxt bd
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	162	];
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	163	in
55851 3d40cf74726c optimize cardinal bounds involving natLeq (omega) blanchet parents: 55707 diff changeset	164	(case bd_ordIso_natLeq_opt of
75624 22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	165	SOME thm => rtac ctxt (thm RSN (2, @{thm ordLess_ordIso_trans})) 1
55851 3d40cf74726c optimize cardinal bounds involving natLeq (omega) blanchet parents: 55707 diff changeset	166	\| NONE => all_tac) THEN
55906 abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	167	unfold_thms_tac ctxt [set'_eq_set, comp_set_alt] THEN
75624 22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	168	rtac ctxt @{thm comp_set_bd_Union_o_collect_strict} 1 THEN
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49490 diff changeset	169	unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
75624 22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	170	EVERY1 [
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	171	rtac ctxt @{thm ordLess_ordLeq_trans},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	172	WRAP' gen_before (K (K all_tac)) bds (rtac ctxt last_bd),
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	173	rtac ctxt @{thm ordIso_imp_ordLeq},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	174	REPEAT_DETERM_N (length Gset_Fset_bds - 1) o EVERY' [
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	175	rtac ctxt @{thm ordIso_transitive},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	176	REPEAT_DETERM o (rtac ctxt @{thm cprod_csum_distrib1} ORELSE' rtac ctxt @{thm csum_cong2})
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	177	],
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	178	rtac ctxt @{thm cprod_com},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	179	REPEAT_DETERM o EVERY' [
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	180	TRY o rtac ctxt @{thm Cinfinite_csum1},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	181	resolve_tac ctxt Gbd_Fbd_Cinfinites
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	182	]
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	183	]
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	184	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	185
55930 25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms traytel parents: 55906 diff changeset	186	val comp_in_alt_thms = @{thms o_apply collect_def image_insert image_empty Union_insert UN_insert
25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms traytel parents: 55906 diff changeset	187	UN_empty Union_empty Un_empty_right Union_Un_distrib Un_subset_iff conj_subset_def UN_image_subset
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	188	conj_assoc};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	189
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	190	fun mk_comp_in_alt_tac ctxt comp_set_alts =
55930 25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms traytel parents: 55906 diff changeset	191	unfold_thms_tac ctxt comp_set_alts THEN
25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms traytel parents: 55906 diff changeset	192	unfold_thms_tac ctxt comp_in_alt_thms THEN
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49490 diff changeset	193	unfold_thms_tac ctxt @{thms set_eq_subset} THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	194	rtac ctxt conjI 1 THEN
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	195	REPEAT_DETERM (
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	196	rtac ctxt @{thm subsetI} 1 THEN
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49490 diff changeset	197	unfold_thms_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	198	(REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	199	REPEAT_DETERM (CHANGED ((
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	200	(rtac ctxt conjI THEN' (assume_tac ctxt ORELSE' rtac ctxt subset_UNIV)) ORELSE'
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	201	assume_tac ctxt ORELSE'
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	202	(rtac ctxt subset_UNIV)) 1)) ORELSE rtac ctxt subset_UNIV 1));
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	203
55930 25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms traytel parents: 55906 diff changeset	204	val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def UN_insert UN_empty Un_empty_right
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	205	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	206
55906 abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	207	fun mk_comp_wit_tac ctxt set'_eq_sets Gwit_thms collect_set_map Fwit_thms =
abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	208	unfold_thms_tac ctxt set'_eq_sets THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	209	ALLGOALS (dtac ctxt @{thm in_Union_o_assoc}) THEN
55930 25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms traytel parents: 55906 diff changeset	210	unfold_thms_tac ctxt [collect_set_map] THEN
25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms traytel parents: 55906 diff changeset	211	unfold_thms_tac ctxt comp_wit_thms THEN
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	212	REPEAT_DETERM ((assume_tac ctxt ORELSE'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 58181 diff changeset	213	REPEAT_DETERM o eresolve_tac ctxt @{thms UnionE UnE} THEN'
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	214	etac ctxt imageE THEN' TRY o dresolve_tac ctxt Gwit_thms THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	215	(etac ctxt FalseE ORELSE'
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	216	hyp_subst_tac ctxt THEN'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 58181 diff changeset	217	dresolve_tac ctxt Fwit_thms THEN'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	218	(etac ctxt FalseE ORELSE' assume_tac ctxt))) 1);
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	219
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	220
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	221	(* Kill operation *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	222
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 49630 diff changeset	223	fun mk_kill_map_cong0_tac ctxt n m map_cong0 =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	224	(rtac ctxt map_cong0 THEN' EVERY' (replicate n (rtac ctxt refl)) THEN'
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	225	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	226
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	227	fun kill_in_alt_tac ctxt =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	228	((rtac ctxt @{thm Collect_cong} THEN' rtac ctxt iffI) 1 THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	229	REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	230	REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	231	rtac ctxt conjI THEN' rtac ctxt subset_UNIV) 1)) THEN
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	232	(rtac ctxt subset_UNIV ORELSE' assume_tac ctxt) 1 THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	233	REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	234	REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' assume_tac ctxt) 1))) ORELSE
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	235	((rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt CollectI) 1 THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	236	REPEAT_DETERM (TRY (rtac ctxt conjI 1) THEN rtac ctxt subset_UNIV 1));
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	237
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	238
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	239	(* Lift operation *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	240
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	241	fun empty_natural_tac ctxt = rtac ctxt @{thm empty_natural} 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	242
75624 22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	243	fun mk_lift_set_bd_tac ctxt bd_Cinfinite =
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge) traytel parents: 62343 diff changeset	244	(rtac ctxt @{thm Cinfinite_gt_empty} THEN' rtac ctxt bd_Cinfinite) 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	245
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	246	fun lift_in_alt_tac ctxt =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	247	((rtac ctxt @{thm Collect_cong} THEN' rtac ctxt iffI) 1 THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	248	REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	249	REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' assume_tac ctxt) 1)) THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	250	REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	251	REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	252	rtac ctxt conjI THEN' rtac ctxt @{thm empty_subsetI}) 1)) THEN
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	253	(rtac ctxt @{thm empty_subsetI} ORELSE' assume_tac ctxt) 1) ORELSE
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	254	((rtac ctxt sym THEN' rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt CollectI) 1 THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	255	REPEAT_DETERM (TRY (rtac ctxt conjI 1) THEN rtac ctxt @{thm empty_subsetI} 1));
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	256
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	257
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	258	(* Permute operation *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	259
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	260	fun mk_permute_in_alt_tac ctxt src dest =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	261	(rtac ctxt @{thm Collect_cong} THEN'
61760 1647bb489522 tuned whitespace blanchet parents: 60757 diff changeset	262	mk_rotate_eq_tac ctxt (rtac ctxt refl) trans @{thm conj_assoc} @{thm conj_commute}
1647bb489522 tuned whitespace blanchet parents: 60757 diff changeset	263	@{thm conj_cong} dest src) 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	264
55851 3d40cf74726c optimize cardinal bounds involving natLeq (omega) blanchet parents: 55707 diff changeset	265
3d40cf74726c optimize cardinal bounds involving natLeq (omega) blanchet parents: 55707 diff changeset	266	(* Miscellaneous *)
3d40cf74726c optimize cardinal bounds involving natLeq (omega) blanchet parents: 55707 diff changeset	267
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	268	fun mk_le_rel_OO_tac ctxt outer_le_rel_OO outer_rel_mono inner_le_rel_OOs =
62324 ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61760 diff changeset	269	HEADGOAL (EVERY' (map (rtac ctxt) (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono ::
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61760 diff changeset	270	inner_le_rel_OOs)));
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: 48975 diff changeset	271
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	272	fun mk_simple_rel_OO_Grp_tac ctxt rel_OO_Grp in_alt_thm =
62324 ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61760 diff changeset	273	HEADGOAL (rtac ctxt (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]));
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61760 diff changeset	274
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61760 diff changeset	275	fun mk_simple_pred_set_tac ctxt pred_set in_alt_thm =
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61760 diff changeset	276	HEADGOAL (rtac ctxt (pred_set RS trans)) THEN
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61760 diff changeset	277	unfold_thms_tac ctxt @{thms Ball_Collect UNIV_def} THEN
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61760 diff changeset	278	HEADGOAL (rtac ctxt (unfold_thms ctxt @{thms UNIV_def} in_alt_thm RS @{thm Collect_inj} RS sym));
49463 83ac281bcdc2 provide predicator, define relator blanchet parents: 49305 diff changeset	279
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	280	fun mk_simple_wit_tac ctxt wit_thms =
60757 c09598a97436 prefer tactics with explicit context; wenzelm parents: 60752 diff changeset	281	ALLGOALS (assume_tac ctxt ORELSE' eresolve_tac ctxt (@{thm emptyE} :: wit_thms));
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: 48975 diff changeset	282
55851 3d40cf74726c optimize cardinal bounds involving natLeq (omega) blanchet parents: 55707 diff changeset	283	val csum_thms =
3d40cf74726c optimize cardinal bounds involving natLeq (omega) blanchet parents: 55707 diff changeset	284	@{thms csum_cong1 csum_cong2 csum_cong csum_dup[OF natLeq_cinfinite natLeq_Card_order]};
3d40cf74726c optimize cardinal bounds involving natLeq (omega) blanchet parents: 55707 diff changeset	285	val cprod_thms =
3d40cf74726c optimize cardinal bounds involving natLeq (omega) blanchet parents: 55707 diff changeset	286	@{thms cprod_cong1 cprod_cong2 cprod_cong cprod_dup[OF natLeq_cinfinite natLeq_Card_order]};
3d40cf74726c optimize cardinal bounds involving natLeq (omega) blanchet parents: 55707 diff changeset	287
55906 abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	288	val simplified_set_simps =
55930 25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms traytel parents: 55906 diff changeset	289	@{thms collect_def[abs_def] UN_insert UN_empty Un_empty_right Un_empty_left
62343 24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM haftmann parents: 62324 diff changeset	290	o_def Union_Un_distrib UN_empty2 UN_singleton id_bnf_def};
55906 abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	291
55930 25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms traytel parents: 55906 diff changeset	292	fun mk_simplified_set_tac ctxt collect_set_map =
25a90cebbbe5 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms traytel parents: 55906 diff changeset	293	unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	294	unfold_thms_tac ctxt simplified_set_simps THEN rtac ctxt refl 1;
55906 abf91ebd0820 simplify sets in BNF composition blanchet parents: 55905 diff changeset	295
60757 c09598a97436 prefer tactics with explicit context; wenzelm parents: 60752 diff changeset	296	fun bd_ordIso_natLeq_tac ctxt =
c09598a97436 prefer tactics with explicit context; wenzelm parents: 60752 diff changeset	297	HEADGOAL (REPEAT_DETERM o resolve_tac ctxt
55851 3d40cf74726c optimize cardinal bounds involving natLeq (omega) blanchet parents: 55707 diff changeset	298	(@{thm ordIso_refl[OF natLeq_Card_order]} :: csum_thms @ cprod_thms));
3d40cf74726c optimize cardinal bounds involving natLeq (omega) blanchet parents: 55707 diff changeset	299
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	300	end;

author	Fabian Huch <huch@in.tum.de>
	Thu, 27 Jun 2024 11:59:12 +0200
changeset 80415	89c20f7f3b3b
parent 75625	0dd3ac5fdbaa
child 82630	2bb4a8d0111d
permissions	-rw-r--r--