isabelle: src/HOL/BNF/Tools/bnf_gfp_tactics.ML@f57f8e7a879f (annotated)

49509 163914705f8d renamed top-level theory from "Codatatype" to "BNF" blanchet parents: 49506 diff changeset	1	(* Title: HOL/BNF/Tools/bnf_gfp_tactics.ML
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	2	Author: Dmitriy Traytel, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	3	Author: Andrei Popescu, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	4	Author: Jasmin Blanchette, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	5	Copyright 2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	6
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	7	Tactics for the codatatype construction.
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	8	*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	9
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	10	signature BNF_GFP_TACTICS =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	11	sig
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	12	val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list ->
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	13	thm list list -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	14	val mk_bd_card_order_tac: thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	15	val mk_bd_cinfinite_tac: thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	16	val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	17	{prems: 'a, context: Proof.context} -> tactic
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	18	val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	19	val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	20	val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	21	val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	22	thm list list -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	23	val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	24	{prems: 'a, context: Proof.context} -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	25	val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	26	tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	27	val mk_coalg_set_tac: thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	28	val mk_coalg_thePull_tac: int -> thm -> thm list -> thm list list -> (int -> tactic) list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	29	{prems: 'a, context: Proof.context} -> tactic
49104 6defdacd595a generate coinductive witnesses for codatatypes traytel parents: 49091 diff changeset	30	val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->
6defdacd595a generate coinductive witnesses for codatatypes traytel parents: 49091 diff changeset	31	{prems: 'a, context: Proof.context} -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	32	val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	33	thm list list -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	34	val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	35	{prems: 'a, context: Proof.context} -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	36	val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	37	val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	38	{prems: 'a, context: Proof.context} -> tactic
51739 3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism; traytel parents: 51447 diff changeset	39	val mk_corec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism; traytel parents: 51447 diff changeset	40	tactic
49581 4e5bd3883429 renamed "dtor_coinduct" etc. to "dtor_map_coinduct" blanchet parents: 49545 diff changeset	41	val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
49585 5c4a12550491 generate high-level "maps", "sets", and "rels" properties blanchet parents: 49581 diff changeset	42	val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	43	val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	44	val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	45	thm -> thm -> thm list -> thm list -> thm list list -> tactic
49501 acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor" blanchet parents: 49499 diff changeset	46	val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor" blanchet parents: 49499 diff changeset	47	{prems: 'a, context: Proof.context} -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	48	val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	49	val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	50	val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	51	{prems: 'a, context: Proof.context} -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	52	val mk_incl_lsbis_tac: int -> int -> thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	53	val mk_length_Lev'_tac: thm -> tactic
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	54	val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	55	val mk_map_comp0_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	56	val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	57	thm list list -> thm list list -> thm list list list -> tactic
53270 c8628119d18e renamed BNF axiom blanchet parents: 53105 diff changeset	58	val mk_map_id0_tac: thm list -> thm -> thm -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	59	val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
49543 53b3c532a082 renamed low-level "map_unique" to have "ctor" or "dtor" in the name blanchet parents: 49542 diff changeset	60	val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	61	val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	62	val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	63	thm list -> {prems: 'a, context: Proof.context} -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	64	val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	65	val mk_mor_UNIV_tac: thm list -> thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	66	val mk_mor_beh_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	67	thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	68	thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	69	thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	70	{prems: 'a, context: Proof.context} -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	71	val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	72	val mk_mor_elim_tac: thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	73	val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	74	thm list -> thm list list -> thm list list -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	75	val mk_mor_incl_tac: thm -> thm list -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	76	val mk_mor_str_tac: 'a list -> thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	77	val mk_mor_sum_case_tac: 'a list -> thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	78	val mk_mor_thePull_fst_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	79	{prems: thm list, context: Proof.context} -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	80	val mk_mor_thePull_snd_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	81	{prems: thm list, context: Proof.context} -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	82	val mk_mor_thePull_pick_tac: thm -> thm list -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	83	{prems: 'a, context: Proof.context} -> tactic
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	84	val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	85	thm list -> tactic
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	86	val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	87	val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	88	val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	89	thm list list -> thm list -> (int -> tactic) list -> {prems: 'a, context: Proof.context} ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	90	tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	91	val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	92	thm list -> thm list -> thm -> thm list -> tactic
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	93	val mk_rel_coinduct_tac: thm list -> thm list -> thm list list -> thm list -> thm list ->
52506 eb80a16a2b72 use long goal format in rel_induct theorem traytel parents: 51925 diff changeset	94	{prems: thm list, context: Proof.context} -> tactic
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	95	val mk_rel_coinduct_coind_tac: int -> thm -> int list -> thm list -> thm list -> thm list ->
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	96	thm list list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	97	val mk_rel_coinduct_ind_tac: int -> int list -> thm list -> thm list list -> int -> thm ->
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	98	{prems: 'a, context: Proof.context} -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	99	val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	100	val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	101	val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	102	thm list -> thm list list -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	103	val mk_set_bd_tac: thm -> thm -> thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	104	val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	105	val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list ->
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	106	thm list -> thm list -> thm list list -> thm list list -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	107	val mk_set_incl_hin_tac: thm list -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	108	val mk_set_incl_hset_tac: thm -> thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	109	val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	110	val mk_set_map0_tac: thm -> thm -> tactic
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	111	val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	112	thm list -> thm list -> thm list list -> thm list list -> tactic
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	113	val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
52731 dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	114	val mk_unfold_transfer_tac: int -> thm -> thm list -> thm list ->
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	115	{prems: thm list, context: Proof.context} -> tactic
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	116	val mk_unique_mor_tac: thm list -> thm -> tactic
49104 6defdacd595a generate coinductive witnesses for codatatypes traytel parents: 49091 diff changeset	117	val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	118	{prems: 'a, context: Proof.context} -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	119	val mk_wpull_tac: int -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	120	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	121
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	122	structure BNF_GFP_Tactics : BNF_GFP_TACTICS =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	123	struct
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	124
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	125	open BNF_Tactics
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	126	open BNF_Util
51850 106afdf5806c renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries blanchet parents: 51798 diff changeset	127	open BNF_FP_Util
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	128	open BNF_GFP_Util
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	129
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	130	val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym;
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	131	val list_inject_iffD1 = @{thm list.inject[THEN iffD1]};
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	132	val nat_induct = @{thm nat_induct};
8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	133	val o_apply_trans_sym = o_apply RS trans RS sym;
8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	134	val ord_eq_le_trans = @{thm ord_eq_le_trans};
8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	135	val ord_eq_le_trans_trans_fun_cong_image_id_id_apply =
8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	136	@{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	137	val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	138	val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
49328 a1c10b46fecd avoided duplicate lemma blanchet parents: 49305 diff changeset	139	val sum_case_weak_cong = @{thm sum_case_weak_cong};
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	140	val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
52659 58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit) traytel parents: 52635 diff changeset	141	val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit) traytel parents: 52635 diff changeset	142	val rev_bspec = Drule.rotate_prems 1 bspec;
52749 ed416f4ac34e more converse(p) theorems; tuned proofs; traytel parents: 52731 diff changeset	143	val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
ed416f4ac34e more converse(p) theorems; tuned proofs; traytel parents: 52731 diff changeset	144	val conversep_in_rel_Id_on =
ed416f4ac34e more converse(p) theorems; tuned proofs; traytel parents: 52731 diff changeset	145	@{thm trans[OF conversep_in_rel arg_cong[of _ _ in_rel, OF converse_Id_on]]};
ed416f4ac34e more converse(p) theorems; tuned proofs; traytel parents: 52731 diff changeset	146	val relcompp_in_rel_Id_on =
ed416f4ac34e more converse(p) theorems; tuned proofs; traytel parents: 52731 diff changeset	147	@{thm trans[OF relcompp_in_rel arg_cong[of _ _ in_rel, OF Id_on_Comp[symmetric]]]};
ed416f4ac34e more converse(p) theorems; tuned proofs; traytel parents: 52731 diff changeset	148	val converse_shift = @{thm converse_subset_swap} RS iffD1;
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	149
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	150	fun mk_coalg_set_tac coalg_def =
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	151	dtac (coalg_def RS iffD1) 1 THEN
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	152	REPEAT_DETERM (etac conjE 1) THEN
52659 58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit) traytel parents: 52635 diff changeset	153	EVERY' [dtac rev_bspec, atac] 1 THEN
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	154	REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	155
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	156	fun mk_mor_elim_tac mor_def =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	157	(dtac (subst OF [mor_def]) THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	158	REPEAT o etac conjE THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	159	TRY o rtac @{thm image_subsetI} THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	160	etac bspec THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	161	atac) 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	162
53285 f09645642984 renamed BNF fact blanchet parents: 53270 diff changeset	163	fun mk_mor_incl_tac mor_def map_ids =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	164	(stac mor_def THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	165	rtac conjI THEN'
53285 f09645642984 renamed BNF fact blanchet parents: 53270 diff changeset	166	CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_ids THEN'
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	167	CONJ_WRAP' (fn thm =>
53285 f09645642984 renamed BNF fact blanchet parents: 53270 diff changeset	168	(EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_ids) 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	169
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	170	fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	171	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	172	fun fbetw_tac image = EVERY' [rtac ballI, stac o_apply, etac image, etac image, atac];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	173	fun mor_tac ((mor_image, morE), map_comp_id) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	174	EVERY' [rtac ballI, stac o_apply, rtac trans, rtac (map_comp_id RS sym), rtac trans,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	175	etac (morE RS arg_cong), atac, etac morE, etac mor_image, atac];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	176	in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	177	(stac mor_def THEN' rtac conjI THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	178	CONJ_WRAP' fbetw_tac mor_images THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	179	CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	180	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	181
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	182	fun mk_mor_UNIV_tac morEs mor_def =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	183	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	184	val n = length morEs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	185	fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	186	rtac UNIV_I, rtac sym, rtac o_apply];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	187	in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	188	EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	189	stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	190	CONJ_WRAP' (fn i =>
52659 58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit) traytel parents: 52635 diff changeset	191	EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm comp_eq_dest}]) (1 upto n)] 1
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	192	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	193
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	194	fun mk_mor_str_tac ks mor_UNIV =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	195	(stac mor_UNIV THEN' CONJ_WRAP' (K (rtac refl)) ks) 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	196
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	197	fun mk_mor_sum_case_tac ks mor_UNIV =
52634 7c4b56bac189 some new lemmas towards getting rid of in_bd BNF property; tuned traytel parents: 52545 diff changeset	198	(stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm sum_case_o_inj(1)[symmetric]})) ks) 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	199
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	200	fun mk_set_incl_hset_tac def rec_Suc =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	201	EVERY' (stac def ::
52659 58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit) traytel parents: 52635 diff changeset	202	map rtac [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	203	sym, rec_Suc]) 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	204
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	205	fun mk_set_hset_incl_hset_tac n defs rec_Suc i =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	206	EVERY' (map (TRY oo stac) defs @
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	207	map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc, UnI2,
49366 3edd1c90f6e6 renamed "mk_UnN" to "mk_UnIN" blanchet parents: 49328 diff changeset	208	mk_UnIN n i] @
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	209	[etac @{thm UN_I}, atac]) 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	210
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	211	fun mk_set_incl_hin_tac incls =
49490 394870e51d18 tuned antiquotations traytel parents: 49488 diff changeset	212	if null incls 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	213	else EVERY' [rtac subsetI, rtac CollectI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	214	CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	215
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	216	fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} =
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	217	EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	218	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	219	CONJ_WRAP' (fn thm => EVERY'
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	220	[rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	221	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	222	CONJ_WRAP' (fn rec_Suc => EVERY'
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	223	[rtac ord_eq_le_trans, rtac rec_Suc,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	224	if m = 0 then K all_tac
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	225	else (rtac @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	226	CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	227	(K (EVERY' [rtac @{thm UN_least}, REPEAT_DETERM o eresolve_tac [allE, conjE],
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	228	rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	229	rec_Sucs] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	230
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	231	fun mk_hset_minimal_tac n hset_defs hset_rec_minimal {context = ctxt, prems = _} =
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	232	(CONJ_WRAP' (fn def => (EVERY' [rtac ord_eq_le_trans, rtac def,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	233	rtac @{thm UN_least}, rtac rev_mp, rtac hset_rec_minimal,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	234	EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	235	REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) hset_defs) 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	236
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	237	fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss =
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	238	EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	239	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	240	CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	241	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	242	CONJ_WRAP'
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	243	(fn (rec_Suc, (morE, ((passive_set_map0s, active_set_map0s), coalg_sets))) =>
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	244	EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	245	if m = 0 then K all_tac
52659 58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit) traytel parents: 52635 diff changeset	246	else EVERY' [rtac Un_cong, rtac box_equals,
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	247	rtac (nth passive_set_map0s (j - 1) RS sym),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	248	rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
52659 58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit) traytel parents: 52635 diff changeset	249	CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	250	(fn (i, (set_map0, coalg_set)) =>
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	251	EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	252	etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map0,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	253	rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	254	ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	255	REPEAT_DETERM o etac allE, atac, atac])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	256	(rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	257	(rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	258
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	259	fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comp0s map_cong0s set_map0ss =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	260	let
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	261	val n = length rel_OO_Grps;
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	262	val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ rel_OO_Grps);
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	263
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	264	fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), rel_OO_Grp) =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	265	EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	266	etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	267	rtac (rel_OO_Grp RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	268	rtac @{thm relcomppI}, rtac @{thm conversepI},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	269	EVERY' (map (fn thm =>
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	270	EVERY' [rtac @{thm GrpI},
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	271	rtac trans, rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	272	REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	273	REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	274	CONJ_WRAP' (fn (i, thm) =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	275	if i <= m
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	276	then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	277	etac @{thm image_mono}, rtac @{thm image_subsetI},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	278	etac @{thm Collect_split_in_relI[OF Id_onI]}]
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	279	else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	280	rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	281	(1 upto (m + n) ~~ set_map0s)])
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	282	@{thms fst_diag_id snd_diag_id})];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	283
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	284	fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), rel_OO_Grp) =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	285	EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	286	etac allE, etac allE, etac impE, atac,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	287	dtac (rel_OO_Grp RS @{thm eq_refl} RS @{thm predicate2D}),
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	288	REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	289	@{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}),
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	290	hyp_subst_tac ctxt,
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	291	rtac bexI, rtac conjI, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
49684 1cf810b8f600 made tactic more robust (less usage of stac) traytel parents: 49585 diff changeset	292	REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
1cf810b8f600 made tactic more robust (less usage of stac) traytel parents: 49585 diff changeset	293	REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	294	atac, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
49684 1cf810b8f600 made tactic more robust (less usage of stac) traytel parents: 49585 diff changeset	295	REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
1cf810b8f600 made tactic more robust (less usage of stac) traytel parents: 49585 diff changeset	296	REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	297	rtac trans, rtac map_cong0,
51447 a19e973fa2cf eliminate duplicated constant (diag vs. Id_on) traytel parents: 51070 diff changeset	298	REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	299	REPEAT_DETERM_N n o rtac refl,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	300	atac, rtac CollectI,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	301	CONJ_WRAP' (fn (i, thm) =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	302	if i <= m
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	303	then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
51447 a19e973fa2cf eliminate duplicated constant (diag vs. Id_on) traytel parents: 51070 diff changeset	304	rtac @{thm Id_on_fst}, etac set_mp, atac]
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	305	else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	306	rtac trans_fun_cong_image_id_id_apply, atac])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	307	(1 upto (m + n) ~~ set_map0s)];
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	308	in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	309	EVERY' [rtac (bis_def RS trans),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	310	rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	311	etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	312	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	313
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	314	fun mk_bis_converse_tac m bis_rel rel_congs rel_converseps =
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	315	EVERY' [stac bis_rel, dtac (bis_rel RS iffD1),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	316	REPEAT_DETERM o etac conjE, rtac conjI,
52749 ed416f4ac34e more converse(p) theorems; tuned proofs; traytel parents: 52731 diff changeset	317	CONJ_WRAP' (K (EVERY' [rtac converse_shift, etac subset_trans,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	318	rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	319	CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	320	EVERY' [rtac allI, rtac allI, rtac impI,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	321	rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
52749 ed416f4ac34e more converse(p) theorems; tuned proofs; traytel parents: 52731 diff changeset	322	REPEAT_DETERM_N m o rtac conversep_in_rel_Id_on,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	323	REPEAT_DETERM_N (length rel_congs) o rtac @{thm conversep_in_rel},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	324	rtac (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	325	REPEAT_DETERM o etac allE,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	326	rtac @{thm conversepI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	327
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	328	fun mk_bis_O_tac ctxt m bis_rel rel_congs rel_OOs =
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	329	EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	330	REPEAT_DETERM o etac conjE, rtac conjI,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	331	CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	332	CONJ_WRAP' (fn (rel_cong, rel_OO) =>
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	333	EVERY' [rtac allI, rtac allI, rtac impI,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	334	rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
52749 ed416f4ac34e more converse(p) theorems; tuned proofs; traytel parents: 52731 diff changeset	335	REPEAT_DETERM_N m o rtac relcompp_in_rel_Id_on,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	336	REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	337	rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	338	etac @{thm relcompE},
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	339	REPEAT_DETERM o dtac Pair_eqD,
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	340	etac conjE, hyp_subst_tac ctxt,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	341	REPEAT_DETERM o etac allE, rtac @{thm relcomppI},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	342	etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	343
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	344	fun mk_bis_Gr_tac bis_rel rel_Grps mor_images morEs coalg_ins
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	345	{context = ctxt, prems = _} =
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	346	unfold_thms_tac ctxt (bis_rel :: @{thm Id_on_Gr} :: @{thm in_rel_Gr} :: rel_Grps) THEN
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	347	EVERY' [rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	348	CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	349	CONJ_WRAP' (fn (coalg_in, morE) =>
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	350	EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrpI}, etac (morE RS trans),
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	351	etac @{thm GrD1}, etac (@{thm GrD2} RS arg_cong), etac coalg_in, etac @{thm GrD1}])
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	352	(coalg_ins ~~ morEs)] 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	353
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	354	fun mk_bis_Union_tac bis_def in_monos {context = ctxt, prems = _} =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	355	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	356	val n = length in_monos;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	357	val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	358	in
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	359	unfold_thms_tac ctxt [bis_def] THEN
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	360	EVERY' [rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	361	CONJ_WRAP' (fn i =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	362	EVERY' [rtac @{thm UN_least}, dtac bspec, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	363	dtac conjunct1, etac (mk_conjunctN n i)]) ks,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	364	CONJ_WRAP' (fn (i, in_mono) =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	365	EVERY' [rtac allI, rtac allI, rtac impI, etac @{thm UN_E}, dtac bspec, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	366	dtac conjunct2, dtac (mk_conjunctN n i), etac allE, etac allE, dtac mp,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	367	atac, etac bexE, rtac bexI, atac, rtac in_mono,
52659 58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit) traytel parents: 52635 diff changeset	368	REPEAT_DETERM_N n o etac @{thm SUP_upper2[OF _ subset_refl]},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	369	atac]) (ks ~~ in_monos)] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	370	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	371
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	372	fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	373	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	374	val n = length lsbis_defs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	375	in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	376	EVERY' [rtac (Thm.permute_prems 0 1 bis_cong), EVERY' (map rtac lsbis_defs),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	377	rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE, exE],
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	378	hyp_subst_tac ctxt, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	379	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	380
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	381	fun mk_incl_lsbis_tac n i lsbis_def =
52659 58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit) traytel parents: 52635 diff changeset	382	EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm SUP_upper2}, rtac CollectI,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	383	REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	384	rtac (mk_nth_conv n i)] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	385
51447 a19e973fa2cf eliminate duplicated constant (diag vs. Id_on) traytel parents: 51070 diff changeset	386	fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	387	EVERY' [rtac (@{thm equiv_def} RS iffD2),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	388
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	389	rtac conjI, rtac (@{thm refl_on_def} RS iffD2),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	390	rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
51447 a19e973fa2cf eliminate duplicated constant (diag vs. Id_on) traytel parents: 51070 diff changeset	391	rtac incl_lsbis, rtac bis_Id_on, atac, etac @{thm Id_onI},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	392
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	393	rtac conjI, rtac (@{thm sym_def} RS iffD2),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	394	rtac allI, rtac allI, rtac impI, rtac set_mp,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	395	rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	396
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	397	rtac (@{thm trans_def} RS iffD2),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	398	rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac set_mp,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	399	rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	400	etac @{thm relcompI}, atac] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	401
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	402	fun mk_coalgT_tac m defs strT_defs set_map0ss {context = ctxt, prems = _} =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	403	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	404	val n = length strT_defs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	405	val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	406	fun coalg_tac (i, ((passive_sets, active_sets), def)) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	407	EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	408	hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	409	rtac (mk_sum_casesN n i), rtac CollectI,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	410	EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
49585 5c4a12550491 generate high-level "maps", "sets", and "rels" properties blanchet parents: 49581 diff changeset	411	etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	412	passive_sets),
8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	413	CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	414	rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	415	rtac conjI,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	416	rtac conjI, etac @{thm empty_Shift}, dtac set_rev_mp,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	417	etac equalityD1, etac CollectD,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	418	rtac conjI, etac @{thm Shift_clists},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	419	rtac conjI, etac @{thm Shift_prefCl},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	420	rtac conjI, rtac ballI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	421	rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1,
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	422	SELECT_GOAL (unfold_thms_tac ctxt @{thms Succ_Shift shift_def}),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	423	etac bspec, etac @{thm ShiftD},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	424	CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	425	dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	426	dtac bspec, rtac CollectI, etac @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	427	REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	428	rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	429	rtac (@{thm append_Cons} RS sym RS arg_cong RS trans), atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	430	REPEAT_DETERM_N m o (rtac conjI THEN' atac),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	431	CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	432	rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	433	rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	434	rtac allI, rtac impI, REPEAT_DETERM o eresolve_tac [allE, impE],
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	435	etac @{thm not_in_Shift}, rtac trans, rtac (@{thm shift_def} RS fun_cong), atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	436	dtac bspec, atac, dtac conjunct2, dtac (mk_conjunctN n i), dtac bspec,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	437	etac @{thm set_mp[OF equalityD1]}, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	438	REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	439	rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	440	etac (@{thm append_Nil} RS sym RS arg_cong RS trans),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	441	REPEAT_DETERM_N m o (rtac conjI THEN' atac),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	442	CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	443	rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	444	rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	445	in
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	446	unfold_thms_tac ctxt defs THEN
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	447	CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_map0ss ~~ strT_defs)) 1
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	448	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	449
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	450	fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	451	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	452	val n = length Lev_0s;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	453	val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	454	in
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	455	EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	456	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	457	CONJ_WRAP' (fn Lev_0 =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	458	EVERY' (map rtac [ord_eq_le_trans, Lev_0, @{thm Nil_clists}])) Lev_0s,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	459	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	460	CONJ_WRAP' (fn (Lev_Suc, to_sbds) =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	461	EVERY' [rtac ord_eq_le_trans, rtac Lev_Suc,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	462	CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	463	(fn (i, to_sbd) => EVERY' [rtac subsetI,
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	464	REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	465	rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	466	etac set_rev_mp, REPEAT_DETERM o etac allE,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	467	etac (mk_conjunctN n i)])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	468	(rev (ks ~~ to_sbds))])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	469	(Lev_Sucs ~~ to_sbdss)] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	470	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	471
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	472	fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	473	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	474	val n = length Lev_0s;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	475	val ks = n downto 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	476	in
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	477	EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	478	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	479	CONJ_WRAP' (fn Lev_0 =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	480	EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	481	etac @{thm singletonE}, etac ssubst, rtac @{thm list.size(3)}]) Lev_0s,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	482	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	483	CONJ_WRAP' (fn Lev_Suc =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	484	EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	485	CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	486	(fn i =>
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	487	EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	488	rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	489	REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	490	Lev_Sucs] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	491	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	492
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	493	fun mk_length_Lev'_tac length_Lev =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	494	EVERY' [ftac length_Lev, etac ssubst, atac] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	495
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	496	fun mk_prefCl_Lev_tac ctxt cts Lev_0s Lev_Sucs =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	497	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	498	val n = length Lev_0s;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	499	val ks = n downto 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	500	in
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	501	EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	502	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	503	CONJ_WRAP' (fn Lev_0 =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	504	EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	505	etac @{thm singletonE}, hyp_subst_tac ctxt,
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	506	dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	507	hyp_subst_tac ctxt,
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	508	rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	509	rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	510	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	511	CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	512	EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	513	CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	514	(fn i =>
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	515	EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	516	dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac ctxt,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	517	rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	518	rtac Lev_0, rtac @{thm singletonI},
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	519	REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	520	rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
49366 3edd1c90f6e6 renamed "mk_UnN" to "mk_UnIN" blanchet parents: 49328 diff changeset	521	rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	522	rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	523	etac mp, etac conjI, atac]) ks])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	524	(Lev_0s ~~ Lev_Sucs)] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	525	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	526
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	527	fun mk_rv_last_tac cTs cts rv_Nils rv_Conss =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	528	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	529	val n = length rv_Nils;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	530	val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	531	in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	532	EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	533	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	534	CONJ_WRAP' (fn rv_Cons =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	535	CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac exI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	536	rtac (@{thm append_Nil} RS arg_cong RS trans),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	537	rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans), rtac rv_Nil]))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	538	(ks ~~ rv_Nils))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	539	rv_Conss,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	540	REPEAT_DETERM o rtac allI, rtac (mk_sumEN n),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	541	EVERY' (map (fn i =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	542	CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	543	CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	544	rtac (@{thm append_Cons} RS arg_cong RS trans),
49328 a1c10b46fecd avoided duplicate lemma blanchet parents: 49305 diff changeset	545	rtac (rv_Cons RS trans), etac (sum_case_weak_cong RS arg_cong RS trans),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	546	rtac (mk_sum_casesN n i RS arg_cong RS trans), atac])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	547	ks])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	548	rv_Conss)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	549	ks)] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	550	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	551
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	552	fun mk_set_rv_Lev_tac ctxt m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	553	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	554	val n = length Lev_0s;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	555	val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	556	in
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	557	EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	558	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	559	CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	560	EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	561	dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	562	rtac (rv_Nil RS arg_cong RS iffD2),
02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	563	rtac (mk_sum_casesN n i RS iffD2),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	564	CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	565	(ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	566	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	567	CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	568	EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	569	CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	570	(fn (i, (from_to_sbd, coalg_set)) =>
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	571	EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	572	rtac (rv_Cons RS arg_cong RS iffD2),
02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	573	rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	574	etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	575	dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	576	etac coalg_set, atac])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	577	(rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	578	((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	579	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	580
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	581	fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	582	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	583	val n = length Lev_0s;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	584	val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	585	in
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	586	EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	587	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	588	CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	589	EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	590	etac @{thm singletonE}, hyp_subst_tac ctxt,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	591	CONJ_WRAP' (fn i' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	592	(if i = i'
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	593	then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac ctxt,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	594	CONJ_WRAP' (fn (i'', Lev_0'') =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	595	EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},
49366 3edd1c90f6e6 renamed "mk_UnN" to "mk_UnIN" blanchet parents: 49328 diff changeset	596	rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i''),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	597	rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	598	etac conjI, rtac (Lev_0'' RS equalityD2 RS set_mp),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	599	rtac @{thm singletonI}])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	600	(ks ~~ Lev_0s)]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	601	else etac (mk_InN_not_InM i' i RS notE)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	602	ks])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	603	((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	604	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	605	CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	606	EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	607	CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	608	(fn (i, from_to_sbd) =>
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	609	EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	610	CONJ_WRAP' (fn i' => rtac impI THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	611	CONJ_WRAP' (fn i'' =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	612	EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),
49366 3edd1c90f6e6 renamed "mk_UnN" to "mk_UnIN" blanchet parents: 49328 diff changeset	613	rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnIN n i),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	614	rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	615	rtac conjI, atac, dtac (sym RS trans RS sym),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	616	rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS trans),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	617	etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	618	dtac (mk_conjunctN n i), dtac mp, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	619	dtac (mk_conjunctN n i'), dtac mp, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	620	dtac (mk_conjunctN n i''), etac mp, atac])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	621	ks)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	622	ks])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	623	(rev (ks ~~ from_to_sbds))])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	624	((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	625	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	626
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	627	fun mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	628	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	629	val n = length Lev_0s;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	630	val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	631	in
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	632	EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	633	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	634	CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	635	EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	636	etac @{thm singletonE}, hyp_subst_tac ctxt,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	637	CONJ_WRAP' (fn i' => rtac impI THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	638	CONJ_WRAP' (fn i'' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	639	(if i = i''
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	640	then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	641	dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i),
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	642	hyp_subst_tac ctxt,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	643	CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	644	(fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	645	dtac list_inject_iffD1 THEN' etac conjE THEN'
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	646	(if k = i'
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	647	then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac ctxt, etac imageI]
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	648	else etac (mk_InN_not_InM i' k RS notE)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	649	(rev ks)]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	650	else etac (mk_InN_not_InM i'' i RS notE)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	651	ks)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	652	ks])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	653	((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	654	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	655	CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	656	EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	657	CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	658	(fn (i, (from_to_sbd, to_sbd_inj)) =>
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	659	REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN'
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	660	CONJ_WRAP' (fn i' => rtac impI THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	661	dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	662	dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	663	CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	664	REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	665	dtac list_inject_iffD1 THEN' etac conjE THEN'
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	666	(if k = i
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	667	then EVERY' [dtac (mk_InN_inject n i),
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	668	dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	669	atac, atac, hyp_subst_tac ctxt] THEN'
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	670	CONJ_WRAP' (fn i'' =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	671	EVERY' [rtac impI, dtac (sym RS trans),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	672	rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	673	etac (from_to_sbd RS arg_cong),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	674	REPEAT_DETERM o etac allE,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	675	dtac (mk_conjunctN n i), dtac mp, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	676	dtac (mk_conjunctN n i'), dtac mp, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	677	dtac (mk_conjunctN n i''), etac mp, etac sym])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	678	ks
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	679	else etac (mk_InN_not_InM i k RS notE)))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	680	(rev ks))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	681	ks)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	682	(rev (ks ~~ (from_to_sbds ~~ to_sbd_injs)))])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	683	((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	684	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	685
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	686	fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	687	to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	688	prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_map0ss coalg_setss
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	689	map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	690	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	691	val n = length beh_defs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	692	val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	693
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	694	fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	695	((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_map0s,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	696	(coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) =
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	697	EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	698	rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	699	rtac conjI,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	700	rtac @{thm UN_I}, rtac UNIV_I, rtac (Lev_0 RS equalityD2 RS set_mp),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	701	rtac @{thm singletonI},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	702	rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	703	rtac @{thm UN_least}, rtac Lev_sbd,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	704	rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	705	rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	706	rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans},
50058 bb1fadeba35e import Sublist rather than PrefixOrder to avoid unnecessary class instantiation traytel parents: 49684 diff changeset	707	etac @{thm prefixeq_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	708	rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	709	rtac ballI, etac @{thm UN_E}, rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	710	if n = 1 then K all_tac else rtac (mk_sumEN n),
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	711	EVERY' (map6 (fn i => fn isNode_def => fn set_map0s =>
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	712	fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	713	EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	714	rtac exI, rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	715	(if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	716	else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
49328 a1c10b46fecd avoided duplicate lemma blanchet parents: 49305 diff changeset	717	etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	718	EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	719	EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	720	rtac trans_fun_cong_image_id_id_apply,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	721	etac set_rv_Lev, TRY o atac, etac conjI, atac])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	722	(take m set_map0s) set_rv_Levs),
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	723	CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	724	EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	725	rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	726	if n = 1 then rtac refl else atac, atac, rtac subsetI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	727	REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	728	rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	729	etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	730	if n = 1 then rtac refl else atac])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	731	(drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	732	ks isNode_defs set_map0ss set_rv_Levss set_Levss set_image_Levss),
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	733	CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	734	(set_rv_Levs, (set_Levs, set_image_Levs)))))) =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	735	EVERY' [rtac ballI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	736	REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	737	rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	738	rtac exI, rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	739	(if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	740	else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
49328 a1c10b46fecd avoided duplicate lemma blanchet parents: 49305 diff changeset	741	etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	742	EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	743	EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	744	rtac trans_fun_cong_image_id_id_apply,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	745	etac set_rv_Lev, TRY o atac, etac conjI, atac])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	746	(take m set_map0s) set_rv_Levs),
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	747	CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	748	EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	749	rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	750	if n = 1 then rtac refl else atac, atac, rtac subsetI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	751	REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	752	REPEAT_DETERM_N 4 o etac thin_rl,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	753	rtac set_image_Lev,
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	754	atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	755	etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	756	if n = 1 then rtac refl else atac])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	757	(drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	758	(ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	759	(set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	760	(**)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	761	rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	762	etac notE, etac @{thm UN_I[OF UNIV_I]},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	763	(root isNode)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	764	rtac (isNode_def RS ssubst), rtac exI, rtac conjI, rtac (@{thm if_P} RS trans),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	765	rtac length_Lev', rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	766	CONVERSION (Conv.top_conv
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	767	(K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	768	if n = 1 then rtac refl else rtac (mk_sum_casesN n i),
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	769	EVERY' (map2 (fn set_map0 => fn coalg_set =>
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	770	EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	771	rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	772	(take m set_map0s) (take m coalg_sets)),
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	773	CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	774	EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	775	rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	776	rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, rtac rv_Nil,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	777	atac, rtac subsetI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	778	REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	779	rtac set_image_Lev, rtac (Lev_0 RS equalityD2 RS set_mp),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	780	rtac @{thm singletonI}, dtac length_Lev',
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	781	etac @{thm set_mp[OF equalityD1[OF arg_cong[OF
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	782	trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	783	rtac rv_Nil])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	784	(drop m set_map0s ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	785
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	786	fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	787	((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	788	EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	789	rtac (@{thm if_P} RS
49328 a1c10b46fecd avoided duplicate lemma blanchet parents: 49305 diff changeset	790	(if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	791	rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	792	rtac Lev_0, rtac @{thm singletonI},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	793	CONVERSION (Conv.top_conv
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	794	(K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	795	if n = 1 then K all_tac
49328 a1c10b46fecd avoided duplicate lemma blanchet parents: 49305 diff changeset	796	else (rtac (sum_case_weak_cong RS trans) THEN'
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	797	rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	798	rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	799	EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	800	DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	801	rtac trans, rtac @{thm Shift_def},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	802	rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	803	REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	804	etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	805	rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	806	CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	807	EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	808	dtac list_inject_iffD1, etac conjE,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	809	if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	810	dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	811	atac, atac, hyp_subst_tac ctxt, etac @{thm UN_I[OF UNIV_I]}]
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	812	else etac (mk_InN_not_InM i' i'' RS notE)])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	813	(rev ks),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	814	rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
49366 3edd1c90f6e6 renamed "mk_UnN" to "mk_UnIN" blanchet parents: 49328 diff changeset	815	rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	816	REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	817	rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	818	rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	819	dtac asm_rl, dtac asm_rl, dtac asm_rl,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	820	dtac (Lev_Suc RS equalityD1 RS set_mp),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	821	CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	822	EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	823	dtac list_inject_iffD1, etac conjE,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	824	if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	825	dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	826	atac, atac, hyp_subst_tac ctxt, atac]
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	827	else etac (mk_InN_not_InM i' i'' RS notE)])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	828	(rev ks),
49366 3edd1c90f6e6 renamed "mk_UnN" to "mk_UnIN" blanchet parents: 49328 diff changeset	829	rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	830	REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	831	CONVERSION (Conv.top_conv
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	832	(K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	833	if n = 1 then K all_tac
49328 a1c10b46fecd avoided duplicate lemma blanchet parents: 49305 diff changeset	834	else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	835	SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	836	rtac refl])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	837	ks to_sbd_injs from_to_sbds)];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	838	in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	839	(rtac mor_cong THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	840	EVERY' (map (fn thm => rtac (thm RS ext)) beh_defs) THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	841	stac mor_def THEN' rtac conjI THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	842	CONJ_WRAP' fbetw_tac
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	843	(ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	844	((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	845	(set_map0ss ~~ (coalg_setss ~~
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	846	(set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	847	CONJ_WRAP' mor_tac
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	848	(ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	849	((map_comp_ids ~~ (map_cong0s ~~ map_arg_congs)) ~~
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	850	(length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	851	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	852
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	853	fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBISs =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	854	EVERY' [rtac @{thm congruentI}, dtac lsbisE,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	855	REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], rtac (o_apply RS trans),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	856	etac (sym RS arg_cong RS trans), rtac (map_comp_id RS trans),
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	857	rtac (map_cong0 RS trans), REPEAT_DETERM_N m o rtac refl,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	858	EVERY' (map (fn equiv_LSBIS =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	859	EVERY' [rtac @{thm equiv_proj}, rtac equiv_LSBIS, etac set_mp, atac])
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	860	equiv_LSBISs), rtac sym, rtac (o_apply RS trans),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	861	etac (sym RS arg_cong RS trans), rtac map_comp_id] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	862
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	863	fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_map0ss coalgT_setss =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	864	EVERY' [stac coalg_def,
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	865	CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	866	EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	867	rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	868	EVERY' (map2 (fn set_map0 => fn coalgT_set =>
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	869	EVERY' [rtac conjI, rtac (set_map0 RS ord_eq_le_trans),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	870	rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	871	etac coalgT_set])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	872	(take m set_map0s) (take m coalgT_sets)),
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	873	CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) =>
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	874	EVERY' [rtac (set_map0 RS ord_eq_le_trans),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	875	rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff},
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	876	rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	877	(equiv_LSBISs ~~ drop m (set_map0s ~~ coalgT_sets))])
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	878	((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	879
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	880	fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	881	EVERY' [stac mor_def, rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	882	CONJ_WRAP' (fn equiv_LSBIS =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	883	EVERY' [rtac ballI, rtac ssubst, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, atac])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	884	equiv_LSBISs,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	885	CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	886	EVERY' [rtac ballI, rtac sym, rtac trans, rtac @{thm univ_commute}, rtac equiv_LSBIS,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	887	rtac congruent_str_final, atac, rtac o_apply])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	888	(equiv_LSBISs ~~ congruent_str_finals)] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	889
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	890	fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	891	{context = ctxt, prems = _} =
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	892	unfold_thms_tac ctxt defs THEN
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	893	EVERY' [rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	894	CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	895	CONJ_WRAP' (fn (Rep, ((map_comp_id, map_cong0L), coalg_final_sets)) =>
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	896	EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_cong0L,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	897	EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	898	EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	899	etac set_rev_mp, rtac coalg_final_set, rtac Rep])
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	900	Abs_inverses (drop m coalg_final_sets))])
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	901	(Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	902
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	903	fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	904	unfold_thms_tac ctxt defs THEN
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	905	EVERY' [rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	906	CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	907	CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	908
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	909	fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	910	EVERY' [rtac iffD2, rtac mor_UNIV,
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	911	CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) =>
49501 acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor" blanchet parents: 49499 diff changeset	912	EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	913	rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	914	rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	915	rtac (o_apply RS trans RS sym), rtac map_cong0,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	916	REPEAT_DETERM_N m o rtac refl,
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	917	EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) unfold_defs)])
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	918	((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_cong0s)))] 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	919
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	920	fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	921	sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	922	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	923	val n = length Rep_injects;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	924	in
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	925	EVERY' [rtac rev_mp, ftac (bis_def RS iffD1),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	926	REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	927	rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	928	rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	929	rtac impI, rtac rev_mp, rtac bis_cong, rtac bis_O, rtac bis_Gr, rtac coalgT,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	930	rtac mor_T_final, rtac bis_O, rtac sbis_lsbis, rtac bis_converse, rtac bis_Gr, rtac coalgT,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	931	rtac mor_T_final, EVERY' (map (fn thm => rtac (thm RS @{thm relInvImage_Gr})) lsbis_incls),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	932	rtac impI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	933	CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	934	EVERY' [rtac subset_trans, rtac @{thm relInvImage_UNIV_relImage}, rtac subset_trans,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	935	rtac @{thm relInvImage_mono}, rtac subset_trans, etac incl_lsbis,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	936	rtac ord_eq_le_trans, rtac @{thm sym[OF relImage_relInvImage]},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	937	rtac @{thm xt1(3)}, rtac @{thm Sigma_cong},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	938	rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	939	rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac,
51447 a19e973fa2cf eliminate duplicated constant (diag vs. Id_on) traytel parents: 51070 diff changeset	940	rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_Id_on},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	941	rtac Rep_inject])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	942	(Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	943	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	944
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	945	fun mk_unique_mor_tac raw_coinds bis =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	946	CONJ_WRAP' (fn raw_coind =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	947	EVERY' [rtac impI, rtac (bis RS raw_coind RS set_mp RS @{thm IdD}), atac,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	948	etac conjunct1, atac, etac conjunct2, rtac @{thm image2_eqI}, rtac refl, rtac refl, atac])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	949	raw_coinds 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	950
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	951	fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs =
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	952	CONJ_WRAP' (fn (raw_coind, unfold_def) =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	953	EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	954	rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	955	rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	956
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	957	fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtors
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	958	{context = ctxt, prems = _} =
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	959	unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	960	rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	961	EVERY' (map (fn thm =>
49585 5c4a12550491 generate high-level "maps", "sets", and "rels" properties blanchet parents: 49581 diff changeset	962	rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
5c4a12550491 generate high-level "maps", "sets", and "rels" properties blanchet parents: 49581 diff changeset	963	rtac sym, rtac id_apply] 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	964
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	965	fun mk_corec_tac m corec_defs unfold map_cong0 corec_Inls {context = ctxt, prems = _} =
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	966	unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	967	rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	968	REPEAT_DETERM_N m o rtac refl,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	969	EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	970
51739 3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism; traytel parents: 51447 diff changeset	971	fun mk_corec_unique_mor_tac corec_defs corec_Inls unfold_unique_mor {context = ctxt, prems = _} =
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism; traytel parents: 51447 diff changeset	972	unfold_thms_tac ctxt
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism; traytel parents: 51447 diff changeset	973	(corec_defs @ map (fn thm => thm RS @{thm sum_case_expand_Inr'}) corec_Inls) THEN
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism; traytel parents: 51447 diff changeset	974	etac unfold_unique_mor 1;
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism; traytel parents: 51447 diff changeset	975
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	976	fun mk_dtor_coinduct_tac m raw_coind bis_rel rel_congs =
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	977	EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_rel, rtac conjI,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	978	CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]}))
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	979	rel_congs,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	980	CONJ_WRAP' (fn rel_cong => EVERY' [rtac allI, rtac allI, rtac impI,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	981	REPEAT_DETERM o etac allE, rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	982	REPEAT_DETERM_N m o rtac @{thm in_rel_Id_on_UNIV[symmetric]},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	983	REPEAT_DETERM_N (length rel_congs) o rtac @{thm in_rel_Collect_split_eq[symmetric]},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	984	etac mp, etac CollectE, etac @{thm splitD}])
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	985	rel_congs,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	986	rtac impI, REPEAT_DETERM o etac conjE,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	987	CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	988	rtac CollectI, etac @{thm prod_caseI}])) rel_congs] 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	989
49581 4e5bd3883429 renamed "dtor_coinduct" etc. to "dtor_map_coinduct" blanchet parents: 49545 diff changeset	990	fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	991	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	992	val n = length ks;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	993	in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	994	EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_def, rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	995	CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	996	CONJ_WRAP' (fn i => EVERY' [select_prem_tac n (dtac asm_rl) i, REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	997	rtac impI, REPEAT_DETERM o dtac @{thm meta_spec}, etac CollectE, etac @{thm meta_impE},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	998	atac, etac exE, etac conjE, etac conjE, rtac bexI, rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	999	etac @{thm fst_conv[THEN subst]}, etac @{thm snd_conv[THEN subst]},
49490 394870e51d18 tuned antiquotations traytel parents: 49488 diff changeset	1000	rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1001	CONJ_WRAP' (fn i' => EVERY' [rtac subsetI, rtac CollectI, dtac (mk_conjunctN n i'),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1002	REPEAT_DETERM o etac allE, etac mp, rtac @{thm ssubst_mem[OF pair_collapse]}, atac])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1003	ks])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1004	ks,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1005	rtac impI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1006	CONJ_WRAP' (fn i => EVERY' [rtac impI, dtac (mk_conjunctN n i),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1007	rtac @{thm subst[OF pair_in_Id_conv]}, etac set_mp,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1008	rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1009	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1010
53288 050d0bc9afa5 renamed BNF fact blanchet parents: 53287 diff changeset	1011	fun mk_map_tac m n cT unfold map_comp map_cong0 =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1012	EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
53288 050d0bc9afa5 renamed BNF fact blanchet parents: 53287 diff changeset	1013	rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS box_equals)), rtac map_cong0,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1014	REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1015	REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1016	rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1017
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1018	fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1019	EVERY' [rtac hset_minimal,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1020	REPEAT_DETERM_N n o rtac @{thm Un_upper1},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1021	REPEAT_DETERM_N n o
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1022	EVERY' (map3 (fn i => fn set_hset => fn set_hset_hsets =>
49366 3edd1c90f6e6 renamed "mk_UnN" to "mk_UnIN" blanchet parents: 49328 diff changeset	1023	EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1024	etac UnE, etac set_hset, REPEAT_DETERM_N (n - 1) o etac UnE,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1025	EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1026	(1 upto n) set_hsets set_hset_hsetss)] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1027
49585 5c4a12550491 generate high-level "maps", "sets", and "rels" properties blanchet parents: 49581 diff changeset	1028	fun mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1029	EVERY' [rtac equalityI, rtac set_le, rtac @{thm Un_least}, rtac set_incl_hset,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1030	REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1031	EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1032
53270 c8628119d18e renamed BNF axiom blanchet parents: 53105 diff changeset	1033	fun mk_map_id0_tac maps unfold_unique unfold_dtor =
52912 bdd610910e2c tuned traytel parents: 52911 diff changeset	1034	EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps),
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1035	rtac unfold_dtor] 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1036
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1037	fun mk_map_comp0_tac m n maps map_comp0s map_cong0s unfold_unique =
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1038	EVERY' [rtac unfold_unique,
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1039	EVERY' (map3 (fn map_thm => fn map_comp0 => fn map_cong0 =>
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1040	EVERY' (map rtac
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1041	([@{thm o_assoc} RS trans,
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1042	@{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1043	@{thm o_assoc} RS trans RS sym,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1044	@{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1045	@{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans,
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1046	@{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans,
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	1047	ext, o_apply RS trans, o_apply RS trans RS sym, map_cong0] @
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1048	replicate m (@{thm id_o} RS fun_cong) @
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1049	replicate n (@{thm o_id} RS fun_cong))))
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1050	maps map_comp0s map_cong0s)] 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1051
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1052	fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_hsetss
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1053	set_hset_hsetsss =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1054	let
53288 050d0bc9afa5 renamed BNF fact blanchet parents: 53287 diff changeset	1055	val n = length map_comps;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1056	val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1057	in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1058	EVERY' ([rtac rev_mp,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1059	coinduct_tac] @
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1060	maps (fn (((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_hsets),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1061	set_hset_hsetss) =>
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	1062	[REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, rtac conjI,
53288 050d0bc9afa5 renamed BNF fact blanchet parents: 53287 diff changeset	1063	rtac conjI, rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
49585 5c4a12550491 generate high-level "maps", "sets", and "rels" properties blanchet parents: 49581 diff changeset	1064	REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1065	REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
53288 050d0bc9afa5 renamed BNF fact blanchet parents: 53287 diff changeset	1066	rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1067	EVERY' (maps (fn set_hset =>
49585 5c4a12550491 generate high-level "maps", "sets", and "rels" properties blanchet parents: 49581 diff changeset	1068	[rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1069	REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1070	REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1071	CONJ_WRAP' (fn (set_map0, set_hset_hsets) =>
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1072	EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD},
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1073	etac set_rev_mp, rtac ord_eq_le_trans, rtac set_map0,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1074	rtac @{thm image_mono}, rtac subsetI, rtac CollectI, etac CollectE,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1075	REPEAT_DETERM o etac conjE,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1076	CONJ_WRAP' (fn set_hset_hset =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1077	EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1078	(drop m set_map0s ~~ set_hset_hsetss)])
53288 050d0bc9afa5 renamed BNF fact blanchet parents: 53287 diff changeset	1079	(map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1080	map_cong0s ~~ set_map0ss ~~ set_hsetss ~~ set_hset_hsetsss) @
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1081	[rtac impI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1082	CONJ_WRAP' (fn k =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1083	EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1084	rtac conjI, rtac refl, rtac refl]) ks]) 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1085	end
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1086
52911 fe4c2418f069 tuned tactic; traytel parents: 52749 diff changeset	1087	fun mk_dtor_map_unique_tac unfold_unique sym_map_comps {context = ctxt, prems = _} =
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1088	rtac unfold_unique 1 THEN
52911 fe4c2418f069 tuned tactic; traytel parents: 52749 diff changeset	1089	unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1090	ALLGOALS (etac sym);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1091
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1092	fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_map0ss
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1093	{context = ctxt, prems = _} =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1094	let
49541 32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps" blanchet parents: 49516 diff changeset	1095	val n = length dtor_maps;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1096	in
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1097	EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1098	REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1099	CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1100	REPEAT_DETERM o rtac allI,
49541 32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps" blanchet parents: 49516 diff changeset	1101	CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY'
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1102	[SELECT_GOAL (unfold_thms_tac ctxt
49541 32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps" blanchet parents: 49516 diff changeset	1103	(rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
52659 58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit) traytel parents: 52635 diff changeset	1104	rtac Un_cong, rtac refl,
58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit) traytel parents: 52635 diff changeset	1105	CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1106	(fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1107	REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1108	(rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1109	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1110
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1111	fun mk_set_map0_tac hset_def col_natural =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1112	EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1113	(o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1114	(@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1115
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1116	fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1117	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1118	val n = length rec_0s;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1119	in
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1120	EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1121	REPEAT_DETERM o rtac allI,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1122	CONJ_WRAP' (fn rec_0 => EVERY' (map rtac [ordIso_ordLeq_trans,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1123	@{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1124	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1125	CONJ_WRAP' (fn (rec_Suc, set_sbds) => EVERY'
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1126	[rtac ordIso_ordLeq_trans, rtac @{thm card_of_ordIso_subst}, rtac rec_Suc,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1127	rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac (nth set_sbds (j - 1)),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1128	REPEAT_DETERM_N (n - 1) o rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1129	EVERY' (map2 (fn i => fn set_sbd => EVERY' [rtac @{thm UNION_Cinfinite_bound},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1130	rtac set_sbd, rtac ballI, REPEAT_DETERM o etac allE,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1131	etac (mk_conjunctN n i), rtac sbd_Cinfinite]) (1 upto n) (drop m set_sbds))])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1132	(rec_Sucs ~~ set_sbdss)] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1133	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1134
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1135	fun mk_set_bd_tac sbd_Cinfinite hset_def col_bd =
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1136	EVERY' (map rtac [ordIso_ordLeq_trans, @{thm card_of_ordIso_subst}, hset_def,
8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1137	ctrans, @{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1138	@{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite,
52545 d2ad6eae514f Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type) traytel parents: 52506 diff changeset	1139	@{thm infinite_ordLeq_cexp}, sbd_Cinfinite]) 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1140
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1141	fun mk_bd_card_order_tac sbd_card_order =
52545 d2ad6eae514f Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type) traytel parents: 52506 diff changeset	1142	EVERY' (map rtac [@{thm card_order_cexp}, sbd_card_order, sbd_card_order]) 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1143
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1144	fun mk_bd_cinfinite_tac sbd_Cinfinite =
52545 d2ad6eae514f Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type) traytel parents: 52506 diff changeset	1145	EVERY' (map rtac [@{thm cinfinite_cexp}, @{thm ctwo_ordLeq_Cinfinite},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1146	sbd_Cinfinite, sbd_Cinfinite]) 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1147
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1148	fun mk_pickWP_assms_tac set_incl_hsets set_incl_hins map_eq =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1149	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1150	val m = length set_incl_hsets;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1151	in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1152	EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1153	EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1154	CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1155	REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1156	EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1157	CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1158	REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1159	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1160
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1161	fun mk_coalg_thePull_tac m coalg_def map_wpulls set_map0ss pickWP_assms_tacs
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1162	{context = ctxt, prems = _} =
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1163	unfold_thms_tac ctxt [coalg_def] THEN
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1164	CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_map0s)) =>
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1165	EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1166	REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	1167	hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1168	EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1169	pickWP_assms_tac,
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1170	SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1171	REPEAT_DETERM o eresolve_tac [CollectE, conjE],
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1172	rtac CollectI,
49490 394870e51d18 tuned antiquotations traytel parents: 49488 diff changeset	1173	REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1174	CONJ_WRAP' (fn set_map0 =>
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1175	EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map0,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1176	rtac trans_fun_cong_image_id_id_apply, atac])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1177	(drop m set_map0s)])
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1178	(map_wpulls ~~ (pickWP_assms_tacs ~~ set_map0ss)) 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1179
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1180	fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comp0s pickWP_assms_tacs
51070 6ca703425c01 made SML/NJ happy traytel parents: 50058 diff changeset	1181	{context = ctxt, prems = _: thm list} =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1182	let
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1183	val n = length map_comp0s;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1184	in
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1185	unfold_thms_tac ctxt [mor_def] THEN
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1186	EVERY' [rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1187	CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1188	CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp0)) =>
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1189	EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1190	REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	1191	hyp_subst_tac ctxt,
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1192	SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1193	rtac (map_comp0 RS trans),
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1194	SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1195	rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1196	pickWP_assms_tac])
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1197	(map_wpulls ~~ (pickWP_assms_tacs ~~ map_comp0s))] 1
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1198	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1199
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1200	val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1201	val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1202
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1203	fun mk_mor_thePull_pick_tac mor_def unfolds map_comp0s {context = ctxt, prems = _} =
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1204	unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1205	CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1206	CONJ_WRAP' (fn (unfold, map_comp0) =>
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1207	EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	1208	hyp_subst_tac ctxt,
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1209	SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp0 :: @{thms comp_def id_def})),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1210	rtac refl])
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1211	(unfolds ~~ map_comp0s) 1;
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1212
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1213	fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_map0ss map_wpulls pickWP_assms_tacs
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1214	{context = ctxt, prems = _} =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1215	let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1216	val n = length rec_0s;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1217	val ks = n downto 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1218	in
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1219	EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1220	REPEAT_DETERM o rtac allI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1221	CONJ_WRAP' (fn thm => EVERY'
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1222	[rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1223	REPEAT_DETERM o rtac allI,
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1224	CONJ_WRAP' (fn (rec_Suc, ((unfold, set_map0s), (map_wpull, pickWP_assms_tac))) =>
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1225	EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1226	REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	1227	hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1228	EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1229	pickWP_assms_tac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1230	rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1231	rtac ord_eq_le_trans, rtac rec_Suc,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1232	rtac @{thm Un_least},
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1233	SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_map0s (j - 1),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1234	@{thm prod.cases}]),
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1235	etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1236	CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map0) =>
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1237	EVERY' [rtac @{thm UN_least},
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1238	SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map0, @{thm prod.cases}]),
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	1239	etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o etac allE,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1240	dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1241	(ks ~~ rev (drop m set_map0s))])
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1242	(rec_Sucs ~~ ((unfolds ~~ set_map0ss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1243	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1244
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1245	fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1246	mor_unique pick_cols hset_defs =
49488 02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations; traytel parents: 49463 diff changeset	1247	EVERY' [rtac (@{thm wpull_def} RS iffD2), REPEAT_DETERM o rtac allI, rtac impI,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1248	REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1249	rtac box_equals, rtac mor_unique,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1250	rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1251	rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1252	rtac mor_thePull_fst, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1253	rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1254	rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm fst_conv},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1255	rtac box_equals, rtac mor_unique,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1256	rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1257	rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1258	rtac mor_thePull_snd, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1259	rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1260	rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm snd_conv},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1261	rtac CollectI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1262	CONJ_WRAP' (fn (pick, def) =>
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1263	EVERY' [rtac (def RS ord_eq_le_trans), rtac @{thm UN_least},
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1264	rtac pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1265	rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1266	rtac @{thm prod_caseI}, etac conjI, etac conjI, atac])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1267	(pick_cols ~~ hset_defs)] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1268
49585 5c4a12550491 generate high-level "maps", "sets", and "rels" properties blanchet parents: 49581 diff changeset	1269	fun mk_wit_tac n dtor_ctors dtor_set wit coind_wits {context = ctxt, prems = _} =
49104 6defdacd595a generate coinductive witnesses for codatatypes traytel parents: 49091 diff changeset	1270	ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1271	REPEAT_DETERM (atac 1 ORELSE
49585 5c4a12550491 generate high-level "maps", "sets", and "rels" properties blanchet parents: 49581 diff changeset	1272	EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1273	K (unfold_thms_tac ctxt dtor_ctors),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1274	REPEAT_DETERM_N n o etac UnE,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1275	REPEAT_DETERM o
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1276	(TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1277	(eresolve_tac wit ORELSE'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1278	(dresolve_tac wit THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1279	(etac FalseE ORELSE'
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	1280	EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1281	K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1282
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1283	fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	1284	rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac ctxt) THEN
49504 df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) blanchet parents: 49501 diff changeset	1285	unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51782 diff changeset	1286	ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
49104 6defdacd595a generate coinductive witnesses for codatatypes traytel parents: 49091 diff changeset	1287	ALLGOALS (TRY o
6defdacd595a generate coinductive witnesses for codatatypes traytel parents: 49091 diff changeset	1288	FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
6defdacd595a generate coinductive witnesses for codatatypes traytel parents: 49091 diff changeset	1289
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1290	fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1291	dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss =
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1292	let
49544 24094fa47e0d renamed "set_incl" etc. to have "ctor" or "dtor" in the name blanchet parents: 49543 diff changeset	1293	val m = length dtor_set_incls;
24094fa47e0d renamed "set_incl" etc. to have "ctor" or "dtor" in the name blanchet parents: 49543 diff changeset	1294	val n = length dtor_set_set_inclss;
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1295	val (passive_set_map0s, active_set_map0s) = chop m set_map0s;
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1296	val in_Jrel = nth in_Jrels (i - 1);
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1297	val if_tac =
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1298	EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1299	rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1300	EVERY' (map2 (fn set_map0 => fn set_incl =>
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1301	EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0,
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1302	rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1303	etac (set_incl RS @{thm subset_trans})])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1304	passive_set_map0s dtor_set_incls),
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1305	CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) =>
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1306	EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1307	rtac @{thm prod_caseI}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
49544 24094fa47e0d renamed "set_incl" etc. to have "ctor" or "dtor" in the name blanchet parents: 49543 diff changeset	1308	CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1309	rtac conjI, rtac refl, rtac refl])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1310	(in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1311	CONJ_WRAP' (fn conv =>
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1312	EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1313	REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1314	REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
49541 32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps" blanchet parents: 49516 diff changeset	1315	rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1316	@{thms fst_conv snd_conv}];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1317	val only_if_tac =
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1318	EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1319	rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1320	CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
49585 5c4a12550491 generate high-level "maps", "sets", and "rels" properties blanchet parents: 49581 diff changeset	1321	EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1322	rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map0,
49501 acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor" blanchet parents: 49499 diff changeset	1323	rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1324	CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1325	(fn (active_set_map0, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1326	rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1327	rtac active_set_map0, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
49305 8241f21d104b tuned antiquotations blanchet parents: 49104 diff changeset	1328	dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1329	dtac @{thm ssubst_mem[OF pair_collapse]},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1330	REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1331	@{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1332	hyp_subst_tac ctxt,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1333	dtac (in_Jrel RS iffD1),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1334	dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1335	TRY o
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1336	EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1337	REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1338	(rev (active_set_map0s ~~ in_Jrels))])
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1339	(dtor_sets ~~ passive_set_map0s),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1340	rtac conjI,
49541 32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps" blanchet parents: 49516 diff changeset	1341	REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1342	rtac box_equals, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
51761 4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" blanchet parents: 51739 diff changeset	1343	rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1344	EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1345	dtac @{thm ssubst_mem[OF pair_collapse]},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1346	REPEAT_DETERM o
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1347	eresolve_tac (CollectE :: conjE :: @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1348	hyp_subst_tac ctxt, dtac (in_Jrel RS iffD1),
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51850 diff changeset	1349	dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jrels),
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1350	atac]]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1351	in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1352	EVERY' [rtac iffI, if_tac, only_if_tac] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1353	end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1354
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1355	fun mk_rel_coinduct_coind_tac m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1356	dtor_unfolds dtor_maps {context = ctxt, prems = _} =
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1357	let val n = length ks;
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1358	in
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1359	EVERY' [DETERM o rtac coinduct,
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1360	EVERY' (map7 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s =>
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1361	fn dtor_unfold => fn dtor_map =>
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1362	EVERY' [REPEAT_DETERM o eresolve_tac [exE, conjE],
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1363	select_prem_tac (length ks) (dtac @{thm spec2}) i, dtac mp, atac,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1364	REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1365	rtac exI, rtac conjI, rtac conjI,
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1366	rtac (map_comp0 RS trans), rtac (dtor_map RS trans RS sym),
271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1367	rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp0, map_cong]),
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1368	REPEAT_DETERM_N m o rtac @{thm trans[OF fun_cong[OF o_id] sym[OF fun_cong[OF id_o]]]},
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1369	REPEAT_DETERM_N n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}),
53287 271b34513bfb renamed BNF axiom blanchet parents: 53285 diff changeset	1370	rtac (map_comp0 RS trans), rtac (map_cong RS trans),
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1371	REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_o]},
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1372	REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}),
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1373	etac (@{thm prod.cases} RS map_arg_cong RS trans),
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1374	SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.cases}),
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1375	CONJ_WRAP' (fn set_map0 =>
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1376	EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1377	dtac (set_map0 RS equalityD1 RS set_mp),
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1378	REPEAT_DETERM o
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1379	eresolve_tac (imageE :: conjE :: @{thms iffD1[OF Pair_eq, elim_format]}),
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1380	hyp_subst_tac ctxt, rtac exI, rtac conjI, etac Collect_splitD_set_mp, atac,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1381	rtac (o_apply RS trans), rtac (@{thm surjective_pairing} RS arg_cong)])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1382	(drop m set_map0s)])
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1383	ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps)] 1
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1384	end;
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1385
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1386	val split_id_unfolds = @{thms prod.cases image_id id_apply};
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1387
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1388	fun mk_rel_coinduct_ind_tac m ks unfolds set_map0ss j set_induct {context = ctxt, prems = _} =
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1389	let val n = length ks;
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1390	in
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1391	rtac set_induct 1 THEN
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1392	EVERY' (map3 (fn unfold => fn set_map0s => fn i =>
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1393	EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1394	select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1395	REPEAT_DETERM o eresolve_tac [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1396	hyp_subst_tac ctxt,
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1397	SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)),
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1398	rtac subset_refl])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1399	unfolds set_map0ss ks) 1 THEN
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1400	EVERY' (map3 (fn unfold => fn set_map0s => fn i =>
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1401	EVERY' (map (fn set_map0 =>
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1402	EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1403	select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1404	REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1405	SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)),
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1406	etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [allE, mp],
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1407	rtac conjI, etac Collect_splitD_set_mp, atac, rtac (@{thm surjective_pairing} RS arg_cong)])
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1408	(drop m set_map0s)))
5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	1409	unfolds set_map0ss ks) 1
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1410	end;
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1411
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1412	fun mk_rel_coinduct_tac in_rels in_Jrels helper_indss helper_coind1s helper_coind2s
52506 eb80a16a2b72 use long goal format in rel_induct theorem traytel parents: 51925 diff changeset	1413	{context = ctxt, prems = CIHs} =
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1414	let val n = length in_rels;
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1415	in
52506 eb80a16a2b72 use long goal format in rel_induct theorem traytel parents: 51925 diff changeset	1416	Method.insert_tac CIHs 1 THEN
51925 e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1417	unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1418	REPEAT_DETERM (etac exE 1) THEN
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1419	CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1420	EVERY' [rtac @{thm predicate2I}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1421	if null helper_inds then rtac UNIV_I
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1422	else rtac CollectI THEN'
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1423	CONJ_WRAP' (fn helper_ind =>
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1424	EVERY' [rtac (helper_ind RS rev_mp), REPEAT_DETERM_N n o atac,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1425	REPEAT_DETERM_N n o etac thin_rl, rtac impI,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1426	REPEAT_DETERM o resolve_tac [subsetI, CollectI, @{thm iffD2[OF split_beta]}],
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1427	dtac bspec, atac, REPEAT_DETERM o eresolve_tac [allE, mp, conjE],
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1428	etac (refl RSN (2, conjI))])
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1429	helper_inds,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1430	rtac conjI,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1431	rtac (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac thin_rl,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1432	rtac impI, etac mp, rtac exI, etac (refl RSN (2, conjI)),
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1433	rtac (helper_coind2 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac thin_rl,
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1434	rtac impI, etac mp, rtac exI, etac (refl RSN (2, conjI))])
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1435	(in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1436	end;
e3b7917186f1 relator coinduction for codatatypes traytel parents: 51893 diff changeset	1437
52731 dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1438	fun mk_unfold_transfer_tac m rel_coinduct map_transfers unfolds {context = ctxt, prems = _} =
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1439	let
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1440	val n = length map_transfers;
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1441	in
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1442	unfold_thms_tac ctxt
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1443	@{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1444	unfold_thms_tac ctxt @{thms fun_rel_iff_geq_image2p} THEN
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1445	HEADGOAL (EVERY'
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1446	[REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_coinduct,
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1447	EVERY' (map (fn map_transfer => EVERY'
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1448	[REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1449	SELECT_GOAL (unfold_thms_tac ctxt unfolds),
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1450	rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer),
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1451	REPEAT_DETERM_N m o rtac @{thm id_transfer},
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1452	REPEAT_DETERM_N n o rtac @{thm fun_rel_image2p},
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1453	etac @{thm predicate2D}, etac @{thm image2pI}])
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1454	map_transfers)])
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1455	end;
dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52659 diff changeset	1456
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1457	end;

author	blanchet
	Thu, 17 Oct 2013 20:49:19 +0200
changeset 54141	f57f8e7a879f
parent 53289	5e0623448bdb
child 54793	c99f0fdb0886
permissions	-rw-r--r--