isabelle: src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML@1d85ac286c72 (annotated)

54701 4ed7454aebde tuning -- moved ML files to subdirectory blanchet parents: 54491 diff changeset	1	(* Title: HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
54397 f4b4fa25ce56 tuned headers blanchet parents: 54396 diff changeset	3	Copyright 2012, 2013
49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	4
51797 182454c06a80 tuned ML and thy file names blanchet parents: 51742 diff changeset	5	Tactics for wrapping existing freely generated type's constructors.
49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	6	*)
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	7
54008 b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies blanchet parents: 54007 diff changeset	8	signature CTR_SUGAR_GENERAL_TACTICS =
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies blanchet parents: 54007 diff changeset	9	sig
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	10	val select_prem_tac: Proof.context -> int -> (int -> tactic) -> int -> int -> tactic
54008 b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies blanchet parents: 54007 diff changeset	11	val unfold_thms_tac: Proof.context -> thm list -> tactic
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies blanchet parents: 54007 diff changeset	12	end;
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies blanchet parents: 54007 diff changeset	13
54006 9fe1bd54d437 renamed theory file blanchet parents: 53920 diff changeset	14	signature CTR_SUGAR_TACTICS =
49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	15	sig
54008 b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies blanchet parents: 54007 diff changeset	16	include CTR_SUGAR_GENERAL_TACTICS
b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies blanchet parents: 54007 diff changeset	17
49148 93f281430e77 fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case blanchet parents: 49137 diff changeset	18	val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
52968 2b430bbb5a1a define case constant from other 'free constructor' axioms blanchet parents: 52967 diff changeset	19	val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
51717 9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 51686 diff changeset	20	val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
59266 776964a0589f generate 'case_distrib' for Ctr_Sugars desharna parents: 58634 diff changeset	21	val mk_case_distrib_tac: Proof.context -> cterm -> thm -> thm list -> tactic
54491 27966e17d075 case_if -> case_eq_if + docs blanchet parents: 54422 diff changeset	22	val mk_case_eq_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
27966e17d075 case_if -> case_eq_if + docs blanchet parents: 54422 diff changeset	23	thm list list -> tactic
49118 b815fa776b91 renamed theorem blanchet parents: 49116 diff changeset	24	val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
59271 c448752e8b9d generate 'disc_eq_case' for Ctr_Sugars desharna parents: 59266 diff changeset	25	val mk_disc_eq_case_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list ->
c448752e8b9d generate 'disc_eq_case' for Ctr_Sugars desharna parents: 59266 diff changeset	26	tactic
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	27	val mk_exhaust_disc_tac: Proof.context -> int -> thm -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	28	val mk_exhaust_sel_tac: Proof.context -> int -> thm -> thm list -> tactic
51717 9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 51686 diff changeset	29	val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 51686 diff changeset	30	thm list list list -> thm list list list -> tactic
57983 6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57525 diff changeset	31	val mk_half_distinct_disc_tac: Proof.context -> int -> thm -> thm -> tactic
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	32	val mk_nchotomy_tac: Proof.context -> int -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	33	val mk_other_half_distinct_disc_tac: Proof.context -> thm -> tactic
64430 1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	34	val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list ->
1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	35	thm list list list -> tactic
49044 c4a34ae5504d generate "split_asm" property blanchet parents: 49043 diff changeset	36	val mk_split_asm_tac: Proof.context -> thm -> tactic
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	37	val mk_unique_disc_def_tac: Proof.context -> int -> thm -> tactic
49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	38	end;
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	39
54006 9fe1bd54d437 renamed theory file blanchet parents: 53920 diff changeset	40	structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS =
49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	41	struct
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	42
54008 b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies blanchet parents: 54007 diff changeset	43	open Ctr_Sugar_Util
49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	44
49486 64cc57c0d0fe generate "expand" property blanchet parents: 49484 diff changeset	45	val meta_mp = @{thm meta_mp};
64cc57c0d0fe generate "expand" property blanchet parents: 49484 diff changeset	46
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	47	fun select_prem_tac ctxt n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac ctxt thin_rl,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	48	tac, REPEAT_DETERM_N (n - k) o etac ctxt thin_rl]);
54008 b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies blanchet parents: 54007 diff changeset	49
63223 bcf4828bb125 clarified aliases (no warning for duplicates); wenzelm parents: 63170 diff changeset	50	val unfold_thms_tac = Local_Defs.unfold0_tac;
54008 b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies blanchet parents: 54007 diff changeset	51
49212 ca59649170b0 more sugar on codatatypes blanchet parents: 49174 diff changeset	52	fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
49031 632ee0da3c5b generate "case_disc" property blanchet parents: 49030 diff changeset	53
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	54	fun mk_nchotomy_tac ctxt n exhaust =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	55	HEADGOAL (rtac ctxt allI THEN' rtac ctxt exhaust THEN'
61760 1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	56	EVERY' (maps (fn k =>
1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	57	[rtac ctxt (mk_disjIN n k), REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt])
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	58	(1 upto n)));
49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	59
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	60	fun mk_unique_disc_def_tac ctxt m uexhaust =
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	61	HEADGOAL (EVERY'
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	62	[rtac ctxt iffI, rtac ctxt uexhaust, REPEAT_DETERM_N m o rtac ctxt exI,
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	63	assume_tac ctxt, rtac ctxt refl]);
49137 5c8fefe0f103 fixed bugs in one-constructor case blanchet parents: 49122 diff changeset	64
49486 64cc57c0d0fe generate "expand" property blanchet parents: 49484 diff changeset	65	fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	66	HEADGOAL (EVERY' ([rtac ctxt (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	67	rtac ctxt @{thm iffI_np}, REPEAT_DETERM o etac ctxt exE,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	68	hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac ctxt allI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	69	rtac ctxt distinct, rtac ctxt uexhaust] @
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	70	(([etac ctxt notE, REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt],
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	71	[REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt])
52325 a74e0a4741df tuning blanchet parents: 51937 diff changeset	72	\|> k = 1 ? swap \|> op @)));
49116 3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes) blanchet parents: 49075 diff changeset	73
57983 6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57525 diff changeset	74	fun mk_half_distinct_disc_tac ctxt m discD disc' =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	75	HEADGOAL (dtac ctxt discD THEN' REPEAT_DETERM_N m o etac ctxt exE THEN' hyp_subst_tac ctxt THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	76	rtac ctxt disc');
49028 487427a02bee generate "disc_distinct" theorems blanchet parents: 49022 diff changeset	77
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	78	fun mk_other_half_distinct_disc_tac ctxt half =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	79	HEADGOAL (etac ctxt @{thm contrapos_pn} THEN' etac ctxt half);
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	80
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	81	fun mk_exhaust_disc_or_sel_tac ctxt n exhaust destIs =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	82	HEADGOAL (rtac ctxt exhaust THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	83	EVERY' (map2 (fn k => fn destI => dtac ctxt destI THEN'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	84	select_prem_tac ctxt n (etac ctxt meta_mp) k THEN' assume_tac ctxt) (1 upto n) destIs));
53916 37c31a619eee generate "sel_exhaust" theorem blanchet parents: 53857 diff changeset	85
57983 6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57525 diff changeset	86	val mk_exhaust_disc_tac = mk_exhaust_disc_or_sel_tac;
53916 37c31a619eee generate "sel_exhaust" theorem blanchet parents: 53857 diff changeset	87
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	88	fun mk_exhaust_sel_tac ctxt n exhaust_disc collapses =
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	89	mk_exhaust_disc_or_sel_tac ctxt n exhaust_disc collapses ORELSE
60757 c09598a97436 prefer tactics with explicit context; wenzelm parents: 60752 diff changeset	90	HEADGOAL (etac ctxt meta_mp THEN' resolve_tac ctxt collapses);
49029 f0ecfa9575a9 generate "disc_exhaust" property blanchet parents: 49028 diff changeset	91
49484 0194a18f80cf finished "disc_coiter_iff" etc. generation blanchet parents: 49463 diff changeset	92	fun mk_collapse_tac ctxt m discD sels =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	93	HEADGOAL (dtac ctxt discD THEN'
52325 a74e0a4741df tuning blanchet parents: 51937 diff changeset	94	(if m = 0 then
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	95	assume_tac ctxt
52325 a74e0a4741df tuning blanchet parents: 51937 diff changeset	96	else
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	97	REPEAT_DETERM_N m o etac ctxt exE THEN' hyp_subst_tac ctxt THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	98	SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac ctxt refl));
49030 d0f4f113e43d generate "ctr_sels" theorems blanchet parents: 49029 diff changeset	99
59271 c448752e8b9d generate 'disc_eq_case' for Ctr_Sugars desharna parents: 59266 diff changeset	100	fun mk_disc_eq_case_tac ctxt ct exhaust discs distincts cases =
c448752e8b9d generate 'disc_eq_case' for Ctr_Sugars desharna parents: 59266 diff changeset	101	HEADGOAL Goal.conjunction_tac THEN
60784 4f590c08fd5d updated to infer_instantiate; wenzelm parents: 60757 diff changeset	102	ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
59271 c448752e8b9d generate 'disc_eq_case' for Ctr_Sugars desharna parents: 59266 diff changeset	103	(hyp_subst_tac ctxt THEN'
c448752e8b9d generate 'disc_eq_case' for Ctr_Sugars desharna parents: 59266 diff changeset	104	SELECT_GOAL (unfold_thms_tac ctxt (@{thms not_True_eq_False not_False_eq_True} @ cases @
c448752e8b9d generate 'disc_eq_case' for Ctr_Sugars desharna parents: 59266 diff changeset	105	((refl :: discs @ distincts) RL [eqTrueI, eqFalseI]))) THEN'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59271 diff changeset	106	resolve_tac ctxt @{thms TrueI True_not_False False_not_True}));
59271 c448752e8b9d generate 'disc_eq_case' for Ctr_Sugars desharna parents: 59266 diff changeset	107
57983 6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57525 diff changeset	108	fun mk_expand_tac ctxt n ms uexhaust_disc vexhaust_disc uncollapses distinct_discsss
6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57525 diff changeset	109	distinct_discsss' =
49486 64cc57c0d0fe generate "expand" property blanchet parents: 49484 diff changeset	110	if ms = [0] then
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	111	HEADGOAL (rtac ctxt (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	112	TRY o
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	113	EVERY' [rtac ctxt uexhaust_disc, assume_tac ctxt, rtac ctxt vexhaust_disc, assume_tac ctxt])
49486 64cc57c0d0fe generate "expand" property blanchet parents: 49484 diff changeset	114	else
51742 b5ff7393642d fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil) blanchet parents: 51717 diff changeset	115	let val ks = 1 upto n in
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	116	HEADGOAL (rtac ctxt uexhaust_disc THEN'
61760 1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	117	EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' =>
1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	118	fn uuncollapse =>
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	119	EVERY' [rtac ctxt (uuncollapse RS trans) THEN'
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	120	TRY o assume_tac ctxt, rtac ctxt sym, rtac ctxt vexhaust_disc,
58634 9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N}; wenzelm parents: 57983 diff changeset	121	EVERY' (@{map 4} (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
52325 a74e0a4741df tuning blanchet parents: 51937 diff changeset	122	EVERY'
a74e0a4741df tuning blanchet parents: 51937 diff changeset	123	(if k' = k then
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	124	[rtac ctxt (vuncollapse RS trans), TRY o assume_tac ctxt] @
52325 a74e0a4741df tuning blanchet parents: 51937 diff changeset	125	(if m = 0 then
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	126	[rtac ctxt refl]
52325 a74e0a4741df tuning blanchet parents: 51937 diff changeset	127	else
61760 1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	128	[if n = 1 then
1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	129	K all_tac
1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	130	else
1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	131	EVERY' [dtac ctxt meta_mp, assume_tac ctxt, dtac ctxt meta_mp,
1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	132	assume_tac ctxt],
1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	133	REPEAT_DETERM_N (Int.max (0, m - 1)) o etac ctxt conjE,
1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	134	asm_simp_tac (ss_only [] ctxt)])
52325 a74e0a4741df tuning blanchet parents: 51937 diff changeset	135	else
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	136	[dtac ctxt (the_single (if k = n then distinct_discs else distinct_discs')),
61760 1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	137	etac ctxt (if k = n then @{thm iff_contradict(1)}
1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	138	else @{thm iff_contradict(2)}),
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	139	assume_tac ctxt, assume_tac ctxt]))
57983 6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57525 diff changeset	140	ks distinct_discss distinct_discss' uncollapses)])
6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57525 diff changeset	141	ks ms distinct_discsss distinct_discsss' uncollapses))
49486 64cc57c0d0fe generate "expand" property blanchet parents: 49484 diff changeset	142	end;
64cc57c0d0fe generate "expand" property blanchet parents: 49484 diff changeset	143
52967 5e25877c51d4 introduced case tactics blanchet parents: 52966 diff changeset	144	fun mk_case_same_ctr_tac ctxt injects =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	145	REPEAT_DETERM o etac ctxt exE THEN' etac ctxt conjE THEN'
52967 5e25877c51d4 introduced case tactics blanchet parents: 52966 diff changeset	146	(case injects of
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60728 diff changeset	147	[] => assume_tac ctxt
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	148	\| [inject] => dtac ctxt (inject RS iffD1) THEN' REPEAT_DETERM o etac ctxt conjE THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	149	hyp_subst_tac ctxt THEN' rtac ctxt refl);
52967 5e25877c51d4 introduced case tactics blanchet parents: 52966 diff changeset	150
5e25877c51d4 introduced case tactics blanchet parents: 52966 diff changeset	151	fun mk_case_distinct_ctrs_tac ctxt distincts =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	152	REPEAT_DETERM o etac ctxt exE THEN' etac ctxt conjE THEN' full_simp_tac (ss_only distincts ctxt);
52967 5e25877c51d4 introduced case tactics blanchet parents: 52966 diff changeset	153
52968 2b430bbb5a1a define case constant from other 'free constructor' axioms blanchet parents: 52967 diff changeset	154	fun mk_case_tac ctxt n k case_def injects distinctss =
2b430bbb5a1a define case constant from other 'free constructor' axioms blanchet parents: 52967 diff changeset	155	let
2b430bbb5a1a define case constant from other 'free constructor' axioms blanchet parents: 52967 diff changeset	156	val case_def' = mk_unabs_def (n + 1) (case_def RS meta_eq_to_obj_eq);
2b430bbb5a1a define case constant from other 'free constructor' axioms blanchet parents: 52967 diff changeset	157	val ks = 1 upto n;
2b430bbb5a1a define case constant from other 'free constructor' axioms blanchet parents: 52967 diff changeset	158	in
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	159	HEADGOAL (rtac ctxt (case_def' RS trans) THEN' rtac ctxt @{thm the_equality} THEN'
61760 1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	160	rtac ctxt (mk_disjIN n k) THEN' REPEAT_DETERM o rtac ctxt exI THEN' rtac ctxt conjI THEN'
1647bb489522 tuned whitespace blanchet parents: 60784 diff changeset	161	rtac ctxt refl THEN' rtac ctxt refl THEN'
52967 5e25877c51d4 introduced case tactics blanchet parents: 52966 diff changeset	162	EVERY' (map2 (fn k' => fn distincts =>
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	163	(if k' < n then etac ctxt disjE else K all_tac) THEN'
52967 5e25877c51d4 introduced case tactics blanchet parents: 52966 diff changeset	164	(if k' = k then mk_case_same_ctr_tac ctxt injects
5e25877c51d4 introduced case tactics blanchet parents: 52966 diff changeset	165	else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
5e25877c51d4 introduced case tactics blanchet parents: 52966 diff changeset	166	end;
5e25877c51d4 introduced case tactics blanchet parents: 52966 diff changeset	167
59266 776964a0589f generate 'case_distrib' for Ctr_Sugars desharna parents: 58634 diff changeset	168	fun mk_case_distrib_tac ctxt ct exhaust cases =
60784 4f590c08fd5d updated to infer_instantiate; wenzelm parents: 60757 diff changeset	169	HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust)) THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	170	ALLGOALS (hyp_subst_tac ctxt THEN' SELECT_GOAL (unfold_thms_tac ctxt cases) THEN' rtac ctxt refl);
59266 776964a0589f generate 'case_distrib' for Ctr_Sugars desharna parents: 58634 diff changeset	171
54491 27966e17d075 case_if -> case_eq_if + docs blanchet parents: 54422 diff changeset	172	fun mk_case_cong_tac ctxt uexhaust cases =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	173	HEADGOAL (rtac ctxt uexhaust THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	174	EVERY' (maps (fn casex => [dtac ctxt sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
54491 27966e17d075 case_if -> case_eq_if + docs blanchet parents: 54422 diff changeset	175
27966e17d075 case_if -> case_eq_if + docs blanchet parents: 54422 diff changeset	176	fun mk_case_eq_if_tac ctxt n uexhaust cases discss' selss =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	177	HEADGOAL (rtac ctxt uexhaust THEN'
58634 9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N}; wenzelm parents: 57983 diff changeset	178	EVERY' (@{map 3} (fn casex => fn if_discs => fn sels =>
52325 a74e0a4741df tuning blanchet parents: 51937 diff changeset	179	EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	180	rtac ctxt casex])
52325 a74e0a4741df tuning blanchet parents: 51937 diff changeset	181	cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
49031 632ee0da3c5b generate "case_disc" property blanchet parents: 49030 diff changeset	182
64430 1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	183	fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss =
1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	184	HEADGOAL (rtac ctxt uexhaust) THEN
1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	185	ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	186	simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	187	flat (nth distinctsss (k - 1))) ctxt)) k) THEN
1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	188	ALLGOALS (etac ctxt thin_rl THEN' rtac ctxt iffI THEN'
1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	189	REPEAT_DETERM o rtac ctxt allI THEN' rtac ctxt impI THEN'
1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	190	REPEAT_DETERM o etac ctxt conjE THEN'
1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	191	hyp_subst_tac ctxt THEN' assume_tac ctxt THEN'
1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	192	REPEAT_DETERM o etac ctxt allE THEN' etac ctxt impE THEN'
1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	193	REPEAT_DETERM o (rtac ctxt conjI THEN' rtac ctxt refl) THEN'
1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63223 diff changeset	194	rtac ctxt refl THEN' assume_tac ctxt);
49032 c2a7bedd57d8 generate "case_cong" property blanchet parents: 49031 diff changeset	195
49044 c4a34ae5504d generate "split_asm" property blanchet parents: 49043 diff changeset	196	val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
c4a34ae5504d generate "split_asm" property blanchet parents: 49043 diff changeset	197
c4a34ae5504d generate "split_asm" property blanchet parents: 49043 diff changeset	198	fun mk_split_asm_tac ctxt split =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	199	HEADGOAL (rtac ctxt (split RS trans)) THEN unfold_thms_tac ctxt split_asm_thms THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60279 diff changeset	200	HEADGOAL (rtac ctxt refl);
49044 c4a34ae5504d generate "split_asm" property blanchet parents: 49043 diff changeset	201
49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	202	end;
54008 b15cfc2864de refactoring -- splitting between constructor sugar dependencies and true BNF dependencies blanchet parents: 54007 diff changeset	203
54491 27966e17d075 case_if -> case_eq_if + docs blanchet parents: 54422 diff changeset	204	structure Ctr_Sugar_General_Tactics : CTR_SUGAR_GENERAL_TACTICS = Ctr_Sugar_Tactics;

author	blanchet
	Sat, 29 Oct 2016 00:39:33 +0200
changeset 64430	1d85ac286c72
parent 63223	bcf4828bb125
child 67710	cc2db3239932
permissions	-rw-r--r--