isabelle: src/HOL/Tools/BNF/bnf_def_tactics.ML@a8e47bd31965 (annotated)

55061 a0adf838e2d1 adjusted comments blanchet parents: 55060 diff changeset	1	(* Title: HOL/Tools/BNF/bnf_def_tactics.ML
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	2	Author: Dmitriy Traytel, TU Muenchen
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	3	Author: Jasmin Blanchette, TU Muenchen
57668 09d2b853b20c tuning blanchet parents: 56903 diff changeset	4	Author: Martin Desharnais, TU Muenchen
62324 ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	5	Author: Ondrej Kuncar, TU Muenchen
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	6	Copyright 2012, 2013, 2014, 2015
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	7
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	8	Tactics for definition of bounded natural functors.
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	9	*)
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	10
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	11	signature BNF_DEF_TACTICS =
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	12	sig
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	13	val mk_collect_set_map_tac: Proof.context -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	14	val mk_in_mono_tac: Proof.context -> int -> tactic
57970 eaa986cd285a generate 'inj_map_strong' for BNFs desharna parents: 57967 diff changeset	15	val mk_inj_map_strong_tac: Proof.context -> thm -> thm list -> thm -> tactic
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	16	val mk_inj_map_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
53285 f09645642984 renamed BNF fact blanchet parents: 53270 diff changeset	17	val mk_map_id: thm -> thm
56903 69b6369a98fa generate 'map_ident' theorem for BNFs desharna parents: 56635 diff changeset	18	val mk_map_ident: Proof.context -> thm -> thm
75276 686a6d7d0991 generated lemma map_ident_strong for BNFs desharna parents: 74545 diff changeset	19	val mk_map_ident_strong: Proof.context -> thm -> thm -> thm
53288 050d0bc9afa5 renamed BNF fact blanchet parents: 53287 diff changeset	20	val mk_map_comp: thm -> thm
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51766 diff changeset	21	val mk_map_cong_tac: Proof.context -> thm -> tactic
53290 b6c3be868217 renamed BNF fact blanchet parents: 53289 diff changeset	22	val mk_set_map: thm -> thm
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	23
55197 5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	24	val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	25	val mk_rel_eq_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
55197 5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	26	val mk_rel_OO_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	27	val mk_rel_conversep_tac: Proof.context -> thm -> thm -> tactic
55197 5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	28	val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
57932 c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	29	val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	30	val mk_rel_mono_tac: Proof.context -> thm list -> thm -> tactic
57967 e6d2e998c30f renamed 'rel_mono_strong' to 'rel_mono_strong0' desharna parents: 57932 diff changeset	31	val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic
61242 1f92b0ac9c96 congruence rules for the relator traytel parents: 60757 diff changeset	32	val mk_rel_cong_tac: Proof.context -> thm list * thm list -> thm -> tactic
62324 ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	33	val mk_rel_eq_onp_tac: Proof.context -> thm -> thm -> thm -> tactic
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	34	val mk_pred_mono_strong0_tac: Proof.context -> thm -> thm -> tactic
63714 b62f4f765353 derive pred_mono property for BNFs traytel parents: 63399 diff changeset	35	val mk_pred_mono_tac: Proof.context -> thm -> thm -> tactic
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	36
55197 5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	37	val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
62329 9f7fa08d2307 derive transfer rule for predicator traytel parents: 62324 diff changeset	38	val mk_pred_transfer_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
9f7fa08d2307 derive transfer rule for predicator traytel parents: 62324 diff changeset	39	val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic
9f7fa08d2307 derive transfer rule for predicator traytel parents: 62324 diff changeset	40	val mk_set_transfer_tac: Proof.context -> thm -> thm list -> tactic
52719 480a3479fa47 transfer rule for map (not yet registered as a transfer rule) traytel parents: 52659 diff changeset	41
55197 5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	42	val mk_in_bd_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm list -> thm list ->
5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	43	thm -> thm -> thm -> thm -> tactic
54189 c0186a0d8cb3 define a trivial nonemptiness witness if none is provided traytel parents: 53562 diff changeset	44
55197 5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	45	val mk_trivial_wit_tac: Proof.context -> thm list -> thm list -> tactic
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	46	end;
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	47
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	48	structure BNF_Def_Tactics : BNF_DEF_TACTICS =
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	49	struct
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	50
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	51	open BNF_Util
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	52	open BNF_Tactics
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	53
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	54	val ord_eq_le_trans = @{thm ord_eq_le_trans};
52844 66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS) traytel parents: 52813 diff changeset	55	val ord_le_eq_trans = @{thm ord_le_eq_trans};
52749 ed416f4ac34e more converse(p) theorems; tuned proofs; traytel parents: 52731 diff changeset	56	val conversep_shift = @{thm conversep_le_swap} RS iffD1;
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	57
53285 f09645642984 renamed BNF fact blanchet parents: 53270 diff changeset	58	fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply};
56903 69b6369a98fa generate 'map_ident' theorem for BNFs desharna parents: 56635 diff changeset	59	fun mk_map_ident ctxt = unfold_thms ctxt @{thms id_def};
75276 686a6d7d0991 generated lemma map_ident_strong for BNFs desharna parents: 74545 diff changeset	60	fun mk_map_ident_strong ctxt map_cong0 map_id =
686a6d7d0991 generated lemma map_ident_strong for BNFs desharna parents: 74545 diff changeset	61	(trans OF [map_cong0, map_id])
686a6d7d0991 generated lemma map_ident_strong for BNFs desharna parents: 74545 diff changeset	62	\|> unfold_thms ctxt @{thms id_apply}
55067 a452de24a877 tuned names blanchet parents: 55061 diff changeset	63	fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp];
51798 ad3a241def73 uniform Proof.context for hyp_subst_tac; wenzelm parents: 51766 diff changeset	64	fun mk_map_cong_tac ctxt cong0 =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	65	(hyp_subst_tac ctxt THEN' rtac ctxt cong0 THEN'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	66	REPEAT_DETERM o (dtac ctxt meta_spec THEN' etac ctxt meta_mp THEN' assume_tac ctxt)) 1;
53290 b6c3be868217 renamed BNF fact blanchet parents: 53289 diff changeset	67	fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest};
60757 c09598a97436 prefer tactics with explicit context; wenzelm parents: 60752 diff changeset	68
c09598a97436 prefer tactics with explicit context; wenzelm parents: 60752 diff changeset	69	fun mk_in_mono_tac ctxt n =
c09598a97436 prefer tactics with explicit context; wenzelm parents: 60752 diff changeset	70	if n = 0 then rtac ctxt subset_UNIV 1
c09598a97436 prefer tactics with explicit context; wenzelm parents: 60752 diff changeset	71	else
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	72	(rtac ctxt @{thm subsetI} THEN' rtac ctxt @{thm CollectI}) 1 THEN
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	73	REPEAT_DETERM (eresolve_tac ctxt @{thms CollectE conjE} 1) THEN
60757 c09598a97436 prefer tactics with explicit context; wenzelm parents: 60752 diff changeset	74	REPEAT_DETERM_N (n - 1)
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	75	((rtac ctxt conjI THEN' etac ctxt @{thm subset_trans} THEN' assume_tac ctxt) 1) THEN
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	76	(etac ctxt @{thm subset_trans} THEN' assume_tac ctxt) 1;
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	77
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	78	fun mk_inj_map_tac ctxt n map_id map_comp map_cong0 map_cong =
56635 b07c8ad23010 added 'inj_map' as auxiliary BNF theorem blanchet parents: 55990 diff changeset	79	let
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem blanchet parents: 55990 diff changeset	80	val map_cong' = map_cong OF (asm_rl :: replicate n refl);
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem blanchet parents: 55990 diff changeset	81	val map_cong0' = map_cong0 OF (replicate n @{thm the_inv_f_o_f_id});
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem blanchet parents: 55990 diff changeset	82	in
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	83	HEADGOAL (rtac ctxt @{thm injI} THEN' etac ctxt (map_cong' RS box_equals) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	84	REPEAT_DETERM_N 2 o (rtac ctxt (box_equals OF [map_cong0', map_comp RS sym, map_id]) THEN'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	85	REPEAT_DETERM_N n o assume_tac ctxt))
56635 b07c8ad23010 added 'inj_map' as auxiliary BNF theorem blanchet parents: 55990 diff changeset	86	end;
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem blanchet parents: 55990 diff changeset	87
57970 eaa986cd285a generate 'inj_map_strong' for BNFs desharna parents: 57967 diff changeset	88	fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong =
eaa986cd285a generate 'inj_map_strong' for BNFs desharna parents: 57967 diff changeset	89	let
eaa986cd285a generate 'inj_map_strong' for BNFs desharna parents: 57967 diff changeset	90	val rel_eq' = rel_eq RS @{thm predicate2_eqD};
eaa986cd285a generate 'inj_map_strong' for BNFs desharna parents: 57967 diff changeset	91	val rel_maps' = map (fn thm => thm RS iffD1) rel_maps;
eaa986cd285a generate 'inj_map_strong' for BNFs desharna parents: 57967 diff changeset	92	in
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	93	HEADGOAL (dtac ctxt (rel_eq' RS iffD2) THEN' rtac ctxt (rel_eq' RS iffD1)) THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	94	EVERY (map (HEADGOAL o dtac ctxt) rel_maps') THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	95	HEADGOAL (etac ctxt rel_mono_strong) THEN
57970 eaa986cd285a generate 'inj_map_strong' for BNFs desharna parents: 57967 diff changeset	96	TRYALL (Goal.assume_rule_tac ctxt)
eaa986cd285a generate 'inj_map_strong' for BNFs desharna parents: 57967 diff changeset	97	end;
eaa986cd285a generate 'inj_map_strong' for BNFs desharna parents: 57967 diff changeset	98
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	99	fun mk_collect_set_map_tac ctxt set_map0s =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	100	(rtac ctxt (@{thm collect_comp} RS trans) THEN' rtac ctxt @{thm arg_cong[of _ _ collect]} THEN'
53289 5e0623448bdb renamed BNF axiom blanchet parents: 53288 diff changeset	101	EVERY' (map (fn set_map0 =>
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	102	rtac ctxt (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	103	rtac ctxt set_map0) set_map0s) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	104	rtac ctxt @{thm image_empty}) 1;
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	105
55197 5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	106	fun mk_rel_Grp_tac ctxt rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps =
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	107	let
54792 641ea768f535 tuned traytel parents: 54189 diff changeset	108	val n = length set_maps;
61760 1647bb489522 tuned whitespace blanchet parents: 61424 diff changeset	109	val rel_OO_Grps_tac =
1647bb489522 tuned whitespace blanchet parents: 61424 diff changeset	110	if null rel_OO_Grps then K all_tac else rtac ctxt (hd rel_OO_Grps RS trans);
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	111	in
54792 641ea768f535 tuned traytel parents: 54189 diff changeset	112	if null set_maps then
53270 c8628119d18e renamed BNF axiom blanchet parents: 52986 diff changeset	113	unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
62617 b5ec623952d2 strengthened tactics blanchet parents: 62329 diff changeset	114	resolve_tac ctxt @{thms refl Grp_UNIV_idI[OF refl]} 1
52844 66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS) traytel parents: 52813 diff changeset	115	else
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	116	EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm antisym}, rtac ctxt @{thm predicate2I},
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	117	REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE},
61760 1647bb489522 tuned whitespace blanchet parents: 61424 diff changeset	118	hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp,
1647bb489522 tuned whitespace blanchet parents: 61424 diff changeset	119	rtac ctxt map_cong0,
1647bb489522 tuned whitespace blanchet parents: 61424 diff changeset	120	REPEAT_DETERM_N n o EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD},
1647bb489522 tuned whitespace blanchet parents: 61424 diff changeset	121	etac ctxt @{thm set_mp}, assume_tac ctxt],
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	122	rtac ctxt @{thm CollectI},
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	123	CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
61424 c3658c18b7bc prod_case as canonical name for product type eliminator haftmann parents: 61242 diff changeset	124	rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_case_prod_Grp_in},
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	125	etac ctxt @{thm set_mp}, assume_tac ctxt])
54792 641ea768f535 tuned traytel parents: 54189 diff changeset	126	set_maps,
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	127	rtac ctxt @{thm predicate2I}, REPEAT_DETERM o eresolve_tac ctxt [@{thm GrpE}, exE, conjE],
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51798 diff changeset	128	hyp_subst_tac ctxt,
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	129	rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI},
53270 c8628119d18e renamed BNF axiom blanchet parents: 52986 diff changeset	130	EVERY' (map2 (fn convol => fn map_id0 =>
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	131	EVERY' [rtac ctxt @{thm GrpI},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	132	rtac ctxt (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_id0]),
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	133	REPEAT_DETERM_N n o rtac ctxt (convol RS fun_cong),
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	134	REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	135	rtac ctxt @{thm CollectI},
49495 675b9df572df rel_Gr does not depend on map_wpull traytel parents: 49490 diff changeset	136	CONJ_WRAP' (fn thm =>
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	137	EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	138	rtac ctxt @{thm convol_mem_GrpI}, etac ctxt set_mp, assume_tac ctxt])
54792 641ea768f535 tuned traytel parents: 54189 diff changeset	139	set_maps])
53285 f09645642984 renamed BNF fact blanchet parents: 53270 diff changeset	140	@{thms fst_convol snd_convol} [map_id, refl])] 1
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	141	end;
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	142
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	143	fun mk_rel_eq_tac ctxt n rel_Grp rel_cong map_id0 =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	144	(EVERY' (rtac ctxt (rel_cong RS trans) :: replicate n (rtac ctxt @{thm eq_alt})) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	145	rtac ctxt (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN'
62617 b5ec623952d2 strengthened tactics blanchet parents: 62329 diff changeset	146	(if n = 0 then SELECT_GOAL (unfold_thms_tac ctxt (no_refl [map_id0])) THEN' rtac ctxt refl
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	147	else EVERY' [rtac ctxt @{thm arg_cong2[of _ _ _ _ "Grp"]},
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	148	rtac ctxt @{thm equalityI}, rtac ctxt subset_UNIV,
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	149	rtac ctxt @{thm subsetI}, rtac ctxt @{thm CollectI},
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	150	CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto n), rtac ctxt map_id0])) 1;
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	151
57932 c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	152	fun mk_rel_map0_tac ctxt live rel_compp rel_conversep rel_Grp map_id =
c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	153	if live = 0 then
c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	154	HEADGOAL (Goal.conjunction_tac) THEN
c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	155	unfold_thms_tac ctxt @{thms id_apply} THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	156	ALLGOALS (rtac ctxt refl)
57932 c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	157	else
c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	158	let
c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	159	val ks = 1 upto live;
c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	160	in
c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	161	Goal.conjunction_tac 1 THEN
c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	162	unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	163	TRYALL (EVERY' [rtac ctxt iffI, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm GrpI},
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	164	resolve_tac ctxt [map_id, refl], rtac ctxt @{thm CollectI},
61760 1647bb489522 tuned whitespace blanchet parents: 61424 diff changeset	165	CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI},
1647bb489522 tuned whitespace blanchet parents: 61424 diff changeset	166	assume_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	167	resolve_tac ctxt [map_id, refl], rtac ctxt @{thm CollectI},
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	168	CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks,
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 58446 diff changeset	169	REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	170	dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, assume_tac ctxt])
57932 c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	171	end;
c29659f77f8d generate 'rel_map' theorem for BNFs desharna parents: 57668 diff changeset	172
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	173	fun mk_rel_mono_tac ctxt rel_OO_Grps in_mono =
52844 66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS) traytel parents: 52813 diff changeset	174	let
66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS) traytel parents: 52813 diff changeset	175	val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	176	else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	177	rtac ctxt (hd rel_OO_Grps RS sym RSN (2, ord_le_eq_trans));
52844 66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS) traytel parents: 52813 diff changeset	178	in
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	179	EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm relcompp_mono}, rtac ctxt @{thm iffD2[OF conversep_mono]},
61424 c3658c18b7bc prod_case as canonical name for product type eliminator haftmann parents: 61242 diff changeset	180	rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono},
c3658c18b7bc prod_case as canonical name for product type eliminator haftmann parents: 61242 diff changeset	181	rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono}] 1
52844 66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS) traytel parents: 52813 diff changeset	182	end;
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	183
55197 5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	184	fun mk_rel_conversep_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	185	let
54792 641ea768f535 tuned traytel parents: 54189 diff changeset	186	val n = length set_maps;
52844 66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS) traytel parents: 52813 diff changeset	187	val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	188	else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	189	rtac ctxt (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans));
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	190	in
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	191	if null set_maps then rtac ctxt (rel_eq RS @{thm leq_conversepI}) 1
52844 66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS) traytel parents: 52813 diff changeset	192	else
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	193	EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I},
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51798 diff changeset	194	REPEAT_DETERM o
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	195	eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE},
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	196	hyp_subst_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	197	EVERY' (map (fn thm => EVERY' [rtac ctxt @{thm GrpI}, rtac ctxt sym, rtac ctxt trans,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	198	rtac ctxt map_cong0, REPEAT_DETERM_N n o rtac ctxt thm,
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	199	rtac ctxt (map_comp RS sym), rtac ctxt @{thm CollectI},
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	200	CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	201	etac ctxt @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	202	end;
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	203
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	204	fun mk_rel_conversep_tac ctxt le_conversep rel_mono =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	205	EVERY' [rtac ctxt @{thm antisym}, rtac ctxt le_conversep, rtac ctxt @{thm xt1(6)}, rtac ctxt conversep_shift,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	206	rtac ctxt le_conversep, rtac ctxt @{thm iffD2[OF conversep_mono]}, rtac ctxt rel_mono,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	207	REPEAT_DETERM o rtac ctxt @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	208
55197 5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	209	fun mk_rel_OO_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	210	let
54792 641ea768f535 tuned traytel parents: 54189 diff changeset	211	val n = length set_maps;
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	212	fun in_tac nthO_in = rtac ctxt @{thm CollectI} THEN'
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	213	CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	214	rtac ctxt @{thm image_subsetI}, rtac ctxt nthO_in, etac ctxt set_mp, assume_tac ctxt]) set_maps;
52844 66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS) traytel parents: 52813 diff changeset	215	val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	216	else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
67399 eab6ce8368fa ran isabelle update_op on all sources nipkow parents: 67223 diff changeset	217	rtac ctxt (@{thm arg_cong2[of _ _ _ _ "(OO)"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN
54841 af71b753c459 express weak pullback property of bnfs only in terms of the relator traytel parents: 54792 diff changeset	218	(2, ord_le_eq_trans));
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	219	in
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	220	if null set_maps then rtac ctxt (rel_eq RS @{thm leq_OOI}) 1
52844 66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS) traytel parents: 52813 diff changeset	221	else
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	222	EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I},
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	223	REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE},
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51798 diff changeset	224	hyp_subst_tac ctxt,
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	225	rtac ctxt @{thm relcomppI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	226	rtac ctxt trans, rtac ctxt map_comp, rtac ctxt sym, rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	227	REPEAT_DETERM_N n o rtac ctxt @{thm fst_fstOp},
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51798 diff changeset	228	in_tac @{thm fstOp_in},
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	229	rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	230	REPEAT_DETERM_N n o EVERY' [rtac ctxt trans, rtac ctxt o_apply,
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	231	rtac ctxt @{thm ballE}, rtac ctxt subst,
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	232	rtac ctxt @{thm csquare_def}, rtac ctxt @{thm csquare_fstOp_sndOp}, assume_tac ctxt,
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	233	etac ctxt notE, etac ctxt set_mp, assume_tac ctxt],
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51798 diff changeset	234	in_tac @{thm fstOp_in},
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	235	rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	236	rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	237	REPEAT_DETERM_N n o rtac ctxt o_apply,
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 51798 diff changeset	238	in_tac @{thm sndOp_in},
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	239	rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt sym, rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	240	REPEAT_DETERM_N n o rtac ctxt @{thm snd_sndOp},
54841 af71b753c459 express weak pullback property of bnfs only in terms of the relator traytel parents: 54792 diff changeset	241	in_tac @{thm sndOp_in}] 1
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	242	end;
5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	243
57967 e6d2e998c30f renamed 'rel_mono_strong' to 'rel_mono_strong0' desharna parents: 57932 diff changeset	244	fun mk_rel_mono_strong0_tac ctxt in_rel set_maps =
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	245	if null set_maps then assume_tac ctxt 1
51916 eac9e9a45bf5 stronger monotonicity property for relators traytel parents: 51915 diff changeset	246	else
54998 8601434fa334 tuned signature; wenzelm parents: 54841 diff changeset	247	unfold_tac ctxt [in_rel] THEN
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	248	REPEAT_DETERM (eresolve_tac ctxt @{thms exE CollectE conjE} 1) THEN
51916 eac9e9a45bf5 stronger monotonicity property for relators traytel parents: 51915 diff changeset	249	hyp_subst_tac ctxt 1 THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	250	EVERY' [rtac ctxt exI, rtac ctxt @{thm conjI[OF CollectI conjI[OF refl refl]]},
55163 a740f312d9e4 made tactic more robust traytel parents: 55067 diff changeset	251	CONJ_WRAP' (fn thm =>
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	252	(etac ctxt (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' assume_tac ctxt))
55163 a740f312d9e4 made tactic more robust traytel parents: 55067 diff changeset	253	set_maps] 1;
51916 eac9e9a45bf5 stronger monotonicity property for relators traytel parents: 51915 diff changeset	254
58104 c5316f843f72 generate 'rel_transfer' for BNFs desharna parents: 57970 diff changeset	255	fun mk_rel_transfer_tac ctxt in_rel rel_map rel_mono_strong =
c5316f843f72 generate 'rel_transfer' for BNFs desharna parents: 57970 diff changeset	256	let
c5316f843f72 generate 'rel_transfer' for BNFs desharna parents: 57970 diff changeset	257	fun last_tac iffD =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	258	HEADGOAL (etac ctxt rel_mono_strong) THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	259	REPEAT_DETERM (HEADGOAL (etac ctxt (@{thm predicate2_transferD} RS iffD) THEN'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	260	REPEAT_DETERM o assume_tac ctxt));
58104 c5316f843f72 generate 'rel_transfer' for BNFs desharna parents: 57970 diff changeset	261	in
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	262	REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	263	(HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl) ORELSE
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 58446 diff changeset	264	REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) ::
58104 c5316f843f72 generate 'rel_transfer' for BNFs desharna parents: 57970 diff changeset	265	@{thms exE conjE CollectE}))) THEN
67222 19809bc9d7ff made tactics more robust traytel parents: 63714 diff changeset	266	HEADGOAL (hyp_subst_tac ctxt) THEN
19809bc9d7ff made tactics more robust traytel parents: 63714 diff changeset	267	REPEAT_DETERM (HEADGOAL (resolve_tac ctxt (maps (fn thm =>
19809bc9d7ff made tactics more robust traytel parents: 63714 diff changeset	268	[thm RS trans, thm RS @{thm trans[rotated, OF sym]}]) rel_map))) THEN
19809bc9d7ff made tactics more robust traytel parents: 63714 diff changeset	269	HEADGOAL (rtac ctxt iffI) THEN
67223 711eec20aecd removed debug output traytel parents: 67222 diff changeset	270	last_tac iffD1 THEN last_tac iffD2)
58104 c5316f843f72 generate 'rel_transfer' for BNFs desharna parents: 57970 diff changeset	271	end;
c5316f843f72 generate 'rel_transfer' for BNFs desharna parents: 57970 diff changeset	272
55197 5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	273	fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =
52719 480a3479fa47 transfer rule for map (not yet registered as a transfer rule) traytel parents: 52659 diff changeset	274	let
53290 b6c3be868217 renamed BNF fact blanchet parents: 53289 diff changeset	275	val n = length set_maps;
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	276	val in_tac =
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	277	if n = 0 then rtac ctxt @{thm UNIV_I}
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	278	else
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	279	rtac ctxt @{thm CollectI} THEN' CONJ_WRAP' (fn thm =>
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	280	etac ctxt (thm RS
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	281	@{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	282	set_maps;
52719 480a3479fa47 transfer rule for map (not yet registered as a transfer rule) traytel parents: 52659 diff changeset	283	in
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	284	REPEAT_DETERM_N n (HEADGOAL (rtac ctxt rel_funI)) THEN
55945 e96383acecf9 renamed 'fun_rel' to 'rel_fun' blanchet parents: 55642 diff changeset	285	unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	286	HEADGOAL (EVERY' [rtac ctxt @{thm order_trans}, rtac ctxt rel_mono,
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	287	REPEAT_DETERM_N n o assume_tac ctxt,
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	288	rtac ctxt @{thm predicate2I}, dtac ctxt (in_rel RS iffD1),
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	289	REPEAT_DETERM o eresolve_tac ctxt @{thms exE CollectE conjE}, hyp_subst_tac ctxt,
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	290	rtac ctxt @{thm vimage2pI}, rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, in_tac,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	291	rtac ctxt conjI,
52719 480a3479fa47 transfer rule for map (not yet registered as a transfer rule) traytel parents: 52659 diff changeset	292	EVERY' (map (fn convol =>
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	293	rtac ctxt (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	294	REPEAT_DETERM_N n o rtac ctxt (convol RS fun_cong)) @{thms fst_convol snd_convol})])
52719 480a3479fa47 transfer rule for map (not yet registered as a transfer rule) traytel parents: 52659 diff changeset	295	end;
480a3479fa47 transfer rule for map (not yet registered as a transfer rule) traytel parents: 52659 diff changeset	296
55197 5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	297	fun mk_in_bd_tac ctxt live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds
5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	298	bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero =
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	299	if live = 0 then
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	300	rtac ctxt @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order]
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	301	ordLeq_cexp2[OF ordLeq_refl[OF Card_order_ctwo] Card_order_csum]]} 1
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	302	else
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	303	let
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	304	val bd'_Cinfinite = bd_Cinfinite RS @{thm Cinfinite_csum1};
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	305	val inserts =
57970 eaa986cd285a generate 'inj_map_strong' for BNFs desharna parents: 57967 diff changeset	306	map (fn set_bd =>
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	307	iffD2 OF [@{thm card_of_ordLeq}, @{thm ordLeq_ordIso_trans} OF
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	308	[set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]])
57970 eaa986cd285a generate 'inj_map_strong' for BNFs desharna parents: 57967 diff changeset	309	set_bds;
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	310	in
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	311	EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt @{thm cprod_cinfinite_bound},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	312	rtac ctxt (ctrans OF @{thms ordLeq_csum2 ordLeq_cexp2}), rtac ctxt @{thm card_of_Card_order},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	313	rtac ctxt @{thm ordLeq_csum2}, rtac ctxt @{thm Card_order_ctwo}, rtac ctxt @{thm Card_order_csum},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	314	rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm cexp_cong1},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	315	if live = 1 then rtac ctxt @{thm ordIso_refl[OF Card_order_csum]}
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	316	else
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	317	REPEAT_DETERM_N (live - 2) o rtac ctxt @{thm ordIso_transitive[OF csum_cong2]} THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	318	REPEAT_DETERM_N (live - 1) o rtac ctxt @{thm csum_csum},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	319	rtac ctxt bd_Card_order, rtac ctxt (@{thm cexp_mono2_Cnotzero} RS ctrans), rtac ctxt @{thm ordLeq_csum1},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	320	rtac ctxt bd_Card_order, rtac ctxt @{thm Card_order_csum}, rtac ctxt bd_Cnotzero,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	321	rtac ctxt @{thm csum_Cfinite_cexp_Cinfinite},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	322	rtac ctxt (if live = 1 then @{thm card_of_Card_order} else @{thm Card_order_csum}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	323	CONJ_WRAP_GEN' (rtac ctxt @{thm Cfinite_csum}) (K (rtac ctxt @{thm Cfinite_cone})) set_maps,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	324	rtac ctxt bd'_Cinfinite, rtac ctxt @{thm card_of_Card_order},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	325	rtac ctxt @{thm Card_order_cexp}, rtac ctxt @{thm Cinfinite_cexp}, rtac ctxt @{thm ordLeq_csum2},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	326	rtac ctxt @{thm Card_order_ctwo}, rtac ctxt bd'_Cinfinite,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	327	rtac ctxt (Drule.rotate_prems 1 (@{thm cprod_mono2} RSN (2, ctrans))),
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	328	REPEAT_DETERM_N (live - 1) o
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	329	(rtac ctxt (bd_Cinfinite RS @{thm cprod_cexp_csum_cexp_Cinfinite} RSN (2, ctrans)) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	330	rtac ctxt @{thm ordLeq_ordIso_trans[OF cprod_mono2 ordIso_symmetric[OF cprod_cexp]]}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	331	rtac ctxt @{thm ordLeq_refl[OF Card_order_cexp]}] 1 THEN
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	332	unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	333	unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	334	EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst,
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	335	rtac ctxt @{thm subsetI},
61841 4d3527b94f2a more general types Proof.method / context_tactic; wenzelm parents: 61760 diff changeset	336	Method.insert_tac ctxt inserts, REPEAT_DETERM o dtac ctxt meta_spec,
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	337	REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1],
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	338	etac ctxt @{thm CollectE},
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	339	if live = 1 then K all_tac
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	340	else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	341	rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), rtac ctxt @{thm SigmaI}, rtac ctxt @{thm UNIV_I},
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	342	CONJ_WRAP_GEN' (rtac ctxt @{thm SigmaI})
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	343	(K (etac ctxt @{thm If_the_inv_into_in_Func} THEN' assume_tac ctxt)) set_maps,
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	344	rtac ctxt sym,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	345	rtac ctxt (Drule.rotate_prems 1
55990 41c6b99c5fb7 more antiquotations; wenzelm parents: 55945 diff changeset	346	((@{thm box_equals} OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
53288 050d0bc9afa5 renamed BNF fact blanchet parents: 53287 diff changeset	347	map_comp RS sym, map_id]) RSN (2, trans))),
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	348	REPEAT_DETERM_N (2 * live) o assume_tac ctxt,
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	349	REPEAT_DETERM_N live o rtac ctxt (@{thm prod.case} RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	350	rtac ctxt refl,
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	351	rtac ctxt @{thm surj_imp_ordLeq},
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	352	rtac ctxt @{thm subsetI},
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	353	rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}),
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	354	REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt @{thm CollectI},
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	355	CONJ_WRAP' (fn thm =>
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	356	rtac ctxt (thm RS ord_eq_le_trans) THEN' etac ctxt @{thm subset_trans[OF image_mono Un_upper1]})
53290 b6c3be868217 renamed BNF fact blanchet parents: 53289 diff changeset	357	set_maps,
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	358	rtac ctxt sym,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	359	rtac ctxt (@{thm box_equals} OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]},
53288 050d0bc9afa5 renamed BNF fact blanchet parents: 53287 diff changeset	360	map_comp RS sym, map_id])] 1
52635 4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id) traytel parents: 51916 diff changeset	361	end;
51916 eac9e9a45bf5 stronger monotonicity property for relators traytel parents: 51915 diff changeset	362
55197 5a54ed681ba2 less hermetic tactics traytel parents: 55163 diff changeset	363	fun mk_trivial_wit_tac ctxt wit_defs set_maps =
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	364	unfold_thms_tac ctxt wit_defs THEN
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	365	HEADGOAL (EVERY' (map (fn thm =>
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	366	dtac ctxt (thm RS @{thm equalityD1} RS set_mp) THEN'
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	367	etac ctxt @{thm imageE} THEN' assume_tac ctxt) set_maps)) THEN
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	368	ALLGOALS (assume_tac ctxt);
54189 c0186a0d8cb3 define a trivial nonemptiness witness if none is provided traytel parents: 53562 diff changeset	369
58106 c8cba801c483 generate 'set_transfer' for BNFs desharna parents: 58104 diff changeset	370	fun mk_set_transfer_tac ctxt in_rel set_maps =
c8cba801c483 generate 'set_transfer' for BNFs desharna parents: 58104 diff changeset	371	Goal.conjunction_tac 1 THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	372	EVERY (map (fn set_map => HEADGOAL (rtac ctxt rel_funI) THEN
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 58446 diff changeset	373	REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) ::
58106 c8cba801c483 generate 'set_transfer' for BNFs desharna parents: 58104 diff changeset	374	@{thms exE conjE CollectE}))) THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	375	HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 59498 diff changeset	376	rtac ctxt @{thm rel_setI}) THEN
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	377	REPEAT (HEADGOAL (etac ctxt @{thm imageE} THEN' dtac ctxt @{thm set_mp} THEN' assume_tac ctxt THEN'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 58446 diff changeset	378	REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN'
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	379	rtac ctxt @{thm bexI} THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt @{thm imageI})))
d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	380	set_maps);
58106 c8cba801c483 generate 'set_transfer' for BNFs desharna parents: 58104 diff changeset	381
61242 1f92b0ac9c96 congruence rules for the relator traytel parents: 60757 diff changeset	382	fun mk_rel_cong_tac ctxt (eqs, prems) mono =
1f92b0ac9c96 congruence rules for the relator traytel parents: 60757 diff changeset	383	let
1f92b0ac9c96 congruence rules for the relator traytel parents: 60757 diff changeset	384	fun mk_tac thm = etac ctxt thm THEN_ALL_NEW assume_tac ctxt;
62324 ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	385	fun mk_tacs iffD = etac ctxt mono ::
61242 1f92b0ac9c96 congruence rules for the relator traytel parents: 60757 diff changeset	386	map (fn thm => (unfold_thms ctxt @{thms simp_implies_def} thm RS iffD)
1f92b0ac9c96 congruence rules for the relator traytel parents: 60757 diff changeset	387	\|> Drule.rotate_prems ~1 \|> mk_tac) prems;
1f92b0ac9c96 congruence rules for the relator traytel parents: 60757 diff changeset	388	in
1f92b0ac9c96 congruence rules for the relator traytel parents: 60757 diff changeset	389	unfold_thms_tac ctxt eqs THEN
1f92b0ac9c96 congruence rules for the relator traytel parents: 60757 diff changeset	390	HEADGOAL (EVERY' (rtac ctxt iffI :: mk_tacs iffD1 @ mk_tacs iffD2))
1f92b0ac9c96 congruence rules for the relator traytel parents: 60757 diff changeset	391	end;
1f92b0ac9c96 congruence rules for the relator traytel parents: 60757 diff changeset	392
62324 ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	393	fun subst_conv ctxt thm =
74545 6c123914883a clarified context; wenzelm parents: 67399 diff changeset	394	(Conv.arg_conv o Conv.arg_conv)
6c123914883a clarified context; wenzelm parents: 67399 diff changeset	395	(Conv.top_sweep_rewrs_conv [safe_mk_meta_eq thm] ctxt);
62324 ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	396
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	397	fun mk_rel_eq_onp_tac ctxt pred_def map_id0 rel_Grp =
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	398	HEADGOAL (EVERY'
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	399	[SELECT_GOAL (unfold_thms_tac ctxt (pred_def :: @{thms UNIV_def eq_onp_Grp Ball_Collect})),
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	400	CONVERSION (subst_conv ctxt (map_id0 RS sym)),
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	401	rtac ctxt (unfold_thms ctxt @{thms UNIV_def} rel_Grp)]);
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	402
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	403	fun mk_pred_mono_strong0_tac ctxt pred_rel rel_mono_strong0 =
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	404	unfold_thms_tac ctxt [pred_rel] THEN
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	405	HEADGOAL (etac ctxt rel_mono_strong0 THEN_ALL_NEW etac ctxt @{thm eq_onp_mono0});
ae44f16dcea5 make predicator a first-class bnf citizen traytel parents: 61841 diff changeset	406
63714 b62f4f765353 derive pred_mono property for BNFs traytel parents: 63399 diff changeset	407	fun mk_pred_mono_tac ctxt rel_eq_onp rel_mono =
b62f4f765353 derive pred_mono property for BNFs traytel parents: 63399 diff changeset	408	unfold_thms_tac ctxt (map mk_sym [@{thm eq_onp_mono_iff}, rel_eq_onp]) THEN
b62f4f765353 derive pred_mono property for BNFs traytel parents: 63399 diff changeset	409	HEADGOAL (rtac ctxt rel_mono THEN_ALL_NEW assume_tac ctxt);
b62f4f765353 derive pred_mono property for BNFs traytel parents: 63399 diff changeset	410
62329 9f7fa08d2307 derive transfer rule for predicator traytel parents: 62324 diff changeset	411	fun mk_pred_transfer_tac ctxt n in_rel pred_map pred_cong =
9f7fa08d2307 derive transfer rule for predicator traytel parents: 62324 diff changeset	412	HEADGOAL (EVERY' [REPEAT_DETERM_N (n + 1) o rtac ctxt rel_funI, dtac ctxt (in_rel RS iffD1),
63399 d1742d1b7f0f more antiquotations; wenzelm parents: 62617 diff changeset	413	REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE}, hyp_subst_tac ctxt,
62329 9f7fa08d2307 derive transfer rule for predicator traytel parents: 62324 diff changeset	414	rtac ctxt (box_equals OF [@{thm _}, pred_map RS sym, pred_map RS sym]),
9f7fa08d2307 derive transfer rule for predicator traytel parents: 62324 diff changeset	415	rtac ctxt (refl RS pred_cong), REPEAT_DETERM_N n o
67399 eab6ce8368fa ran isabelle update_op on all sources nipkow parents: 67223 diff changeset	416	(etac ctxt @{thm rel_fun_Collect_case_prodD[where B="(=)"]} THEN_ALL_NEW assume_tac ctxt)]);
62329 9f7fa08d2307 derive transfer rule for predicator traytel parents: 62324 diff changeset	417
49284 5f39b7940b49 spin off "bnf_def_tactics.ML" blanchet parents: diff changeset	418	end;

author	wenzelm
	Tue, 22 Jul 2025 12:02:53 +0200
changeset 82894	a8e47bd31965
parent 75276	686a6d7d0991
permissions	-rw-r--r--