isabelle: src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML@177b90f33f40 (annotated)

55061 a0adf838e2d1 adjusted comments blanchet parents: 55060 diff changeset	1	(* Title: HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	3	Copyright 2013
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	4
54246 8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec') blanchet parents: 54174 diff changeset	5	Tactics for corecursor sugar.
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	6	*)
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	7
54246 8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec') blanchet parents: 54174 diff changeset	8	signature BNF_GFP_REC_SUGAR_TACTICS =
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	9	sig
54044 93ab44e992ae strengthened tactic (primcorec_sel_tac) + tuning blanchet parents: 54043 diff changeset	10	val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic
54978 afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...' blanchet parents: 54977 diff changeset	11	val mk_primcorec_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	12	val mk_primcorec_ctr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
53693 71b020d161c5 new tactics for constructor view blanchet parents: 53692 diff changeset	13	val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
71b020d161c5 new tactics for constructor view blanchet parents: 53692 diff changeset	14	tactic
54969 0ac0b6576d21 generate 'disc_iff' for all discriminators blanchet parents: 54959 diff changeset	15	val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm list -> thm list list ->
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	16	thm list -> tactic
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	17	val mk_primcorec_exhaust_tac: Proof.context -> string list -> int -> thm -> tactic
54924 44373f3560c7 refactoring blanchet parents: 54923 diff changeset	18	val mk_primcorec_nchotomy_tac: Proof.context -> thm list -> tactic
54978 afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...' blanchet parents: 54977 diff changeset	19	val mk_primcorec_raw_code_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...' blanchet parents: 54977 diff changeset	20	int list -> thm list -> thm option -> tactic
53910 2c5055a3583d strengthen tactic blanchet parents: 53908 diff changeset	21	val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
54955 cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes blanchet parents: 54954 diff changeset	22	thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	23	end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	24
54246 8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec') blanchet parents: 54174 diff changeset	25	structure BNF_GFP_Rec_Sugar_Tactics : BNF_GFP_REC_SUGAR_TACTICS =
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	26	struct
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	27
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	28	open BNF_Util
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	29	open BNF_Tactics
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	30	open BNF_FP_Util
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	31
54899 7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec' blanchet parents: 54844 diff changeset	32	val atomize_conjL = @{thm atomize_conjL};
53905 158609f78d0f tuning blanchet parents: 53904 diff changeset	33	val falseEs = @{thms not_TrueE FalseE};
53910 2c5055a3583d strengthen tactic blanchet parents: 53908 diff changeset	34	val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict};
62391 1658fc9b2618 more canonical names nipkow parents: 62320 diff changeset	35	val if_split = @{thm if_split};
1658fc9b2618 more canonical names nipkow parents: 62320 diff changeset	36	val if_split_asm = @{thm if_split_asm};
53902 396999552212 use standard "split" properties instead of ad hoc "eq_...I" blanchet parents: 53901 diff changeset	37	val split_connectI = @{thms allI impI conjI};
54953 a2f4cf3387fc strengthen tac w.r.t. lets with tuples blanchet parents: 54926 diff changeset	38	val unfold_lets = @{thms Let_def[abs_def] split_beta}
53902 396999552212 use standard "split" properties instead of ad hoc "eq_...I" blanchet parents: 53901 diff changeset	39
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	40	fun exhaust_inst_as_projs ctxt frees thm =
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	41	let
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	42	val num_frees = length frees;
59582 0fbed69ff081 tuned signature -- prefer qualified names; wenzelm parents: 59580 diff changeset	43	val fs = Term.add_vars (Thm.prop_of thm) [] \|> filter (can dest_funT o snd);
60784 4f590c08fd5d updated to infer_instantiate; wenzelm parents: 60752 diff changeset	44	fun find x = find_index (curry (op =) x) frees;
4f590c08fd5d updated to infer_instantiate; wenzelm parents: 60752 diff changeset	45	fun mk_inst ((x, i), T) = ((x, i), Thm.cterm_of ctxt (mk_proj T num_frees (find x)));
4f590c08fd5d updated to infer_instantiate; wenzelm parents: 60752 diff changeset	46	in infer_instantiate ctxt (map mk_inst fs) thm end;
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	47
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	48	val exhaust_inst_as_projs_tac = PRIMITIVE oo exhaust_inst_as_projs;
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	49
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	50	fun distinct_in_prems_tac ctxt distincts =
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	51	eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN'
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	52	assume_tac ctxt;
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	53
57983 6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57399 diff changeset	54	fun mk_primcorec_nchotomy_tac ctxt exhaust_discs =
61841 4d3527b94f2a more general types Proof.method / context_tactic; wenzelm parents: 61760 diff changeset	55	HEADGOAL (Method.insert_tac ctxt exhaust_discs THEN' clean_blast_tac ctxt);
54924 44373f3560c7 refactoring blanchet parents: 54923 diff changeset	56
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	57	fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
54844 630ba4d8a206 generate exhaust from nchotomy blanchet parents: 54843 diff changeset	58	let val ks = 1 upto n in
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	59	HEADGOAL (assume_tac ctxt ORELSE'
54905 2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness blanchet parents: 54900 diff changeset	60	cut_tac nchotomy THEN'
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	61	K (exhaust_inst_as_projs_tac ctxt frees) THEN'
54905 2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness blanchet parents: 54900 diff changeset	62	EVERY' (map (fn k =>
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	63	(if k < n then etac ctxt disjE else K all_tac) THEN'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	64	REPEAT o (dtac ctxt meta_mp THEN' assume_tac ctxt ORELSE'
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	65	etac ctxt conjE THEN' dtac ctxt meta_mp THEN' assume_tac ctxt ORELSE'
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	66	assume_tac ctxt))
54905 2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness blanchet parents: 54900 diff changeset	67	ks))
54844 630ba4d8a206 generate exhaust from nchotomy blanchet parents: 54843 diff changeset	68	end;
630ba4d8a206 generate exhaust from nchotomy blanchet parents: 54843 diff changeset	69
53903 27fd72593624 more powerful/robust tactics blanchet parents: 53902 diff changeset	70	fun mk_primcorec_assumption_tac ctxt discIs =
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	71	SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	72	not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
61760 1647bb489522 tuned whitespace blanchet parents: 60801 diff changeset	73	SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
1647bb489522 tuned whitespace blanchet parents: 60801 diff changeset	74	etac ctxt conjE ORELSE'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	75	eresolve_tac ctxt falseEs ORELSE'
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	76	resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	77	dresolve_tac ctxt discIs THEN' assume_tac ctxt ORELSE'
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	78	etac ctxt notE THEN' assume_tac ctxt ORELSE'
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	79	etac ctxt disjE))));
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	80
60735 cf291b55f3d1 made tactic more robust w.r.t. equations containing 'case_prod' blanchet parents: 60728 diff changeset	81	fun ss_fst_snd_conv ctxt =
cf291b55f3d1 made tactic more robust w.r.t. equations containing 'case_prod' blanchet parents: 60728 diff changeset	82	Raw_Simplifier.simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	83
60735 cf291b55f3d1 made tactic more robust w.r.t. equations containing 'case_prod' blanchet parents: 60728 diff changeset	84	fun case_atac ctxt =
cf291b55f3d1 made tactic more robust w.r.t. equations containing 'case_prod' blanchet parents: 60728 diff changeset	85	Simplifier.full_simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	86
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	87	fun same_case_tac ctxt m =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	88	HEADGOAL (if m = 0 then rtac ctxt TrueI
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	89	else REPEAT_DETERM_N (m - 1) o (rtac ctxt conjI THEN' case_atac ctxt) THEN' case_atac ctxt);
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	90
54971 b4b828025880 tuning blanchet parents: 54969 diff changeset	91	fun different_case_tac ctxt m exclude =
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	92	HEADGOAL (if m = 0 then
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	93	mk_primcorec_assumption_tac ctxt []
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	94	else
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	95	dtac ctxt exclude THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN'
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	96	mk_primcorec_assumption_tac ctxt []);
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	97
54971 b4b828025880 tuning blanchet parents: 54969 diff changeset	98	fun cases_tac ctxt k m excludesss =
b4b828025880 tuning blanchet parents: 54969 diff changeset	99	let val n = length excludesss in
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	100	EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m
54971 b4b828025880 tuning blanchet parents: 54969 diff changeset	101	\| [exclude] => different_case_tac ctxt m exclude)
b4b828025880 tuning blanchet parents: 54969 diff changeset	102	(take k (nth excludesss (k - 1))))
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	103	end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	104
62320 dc8374620332 tuning blanchet parents: 61841 diff changeset	105	fun prelude_tac ctxt fun_defs thm =
dc8374620332 tuning blanchet parents: 61841 diff changeset	106	unfold_thms_tac ctxt fun_defs THEN HEADGOAL (rtac ctxt thm) THEN unfold_thms_tac ctxt unfold_lets;
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	107
62320 dc8374620332 tuning blanchet parents: 61841 diff changeset	108	fun mk_primcorec_disc_tac ctxt fun_defs corec_disc k m excludesss =
dc8374620332 tuning blanchet parents: 61841 diff changeset	109	prelude_tac ctxt fun_defs corec_disc THEN cases_tac ctxt k m excludesss;
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	110
54969 0ac0b6576d21 generate 'disc_iff' for all discriminators blanchet parents: 54959 diff changeset	111	fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
57983 6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57399 diff changeset	112	distinct_discs =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	113	HEADGOAL (rtac ctxt iffI THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	114	rtac ctxt fun_exhaust THEN'
54959 30ded82ff806 fixed 'disc_iff' tactic in the case where different equations use different variable names for the function arguments blanchet parents: 54955 diff changeset	115	K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN'
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	116	EVERY' (map (fn [] => etac ctxt FalseE
54969 0ac0b6576d21 generate 'disc_iff' for all discriminators blanchet parents: 54959 diff changeset	117	\| fun_discs' as [fun_disc'] =>
0ac0b6576d21 generate 'disc_iff' for all discriminators blanchet parents: 54959 diff changeset	118	if eq_list Thm.eq_thm (fun_discs', fun_discs) then
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	119	REPEAT_DETERM o etac ctxt conjI THEN' (assume_tac ctxt ORELSE' rtac ctxt TrueI)
54917 a426e38a8a7e made tactic handle corner cases, where some of the 'disc' properties are missing, correctly blanchet parents: 54916 diff changeset	120	else
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	121	rtac ctxt FalseE THEN'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	122	(rotate_tac 1 THEN' dtac ctxt fun_disc' THEN' REPEAT o assume_tac ctxt ORELSE'
54977 63a5e0d8ce3b strengthened tactic to handle 'disc_iff' equations of the form '... = False' blanchet parents: 54971 diff changeset	123	cut_tac fun_disc') THEN'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	124	dresolve_tac ctxt distinct_discs THEN' etac ctxt notE THEN' assume_tac ctxt)
54917 a426e38a8a7e made tactic handle corner cases, where some of the 'disc' properties are missing, correctly blanchet parents: 54916 diff changeset	125	fun_discss) THEN'
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	126	(etac ctxt FalseE ORELSE'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	127	resolve_tac ctxt
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	128	(map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' assume_tac ctxt));
54899 7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec' blanchet parents: 54844 diff changeset	129
62320 dc8374620332 tuning blanchet parents: 61841 diff changeset	130	fun mk_primcorec_sel_tac ctxt fun_defs distincts splits split_asms mapsx map_ident0s map_comps
dc8374620332 tuning blanchet parents: 61841 diff changeset	131	fun_sel k m excludesss =
dc8374620332 tuning blanchet parents: 61841 diff changeset	132	prelude_tac ctxt fun_defs (fun_sel RS trans) THEN
54971 b4b828025880 tuning blanchet parents: 54969 diff changeset	133	cases_tac ctxt k m excludesss THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	134	HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	135	eresolve_tac ctxt falseEs ORELSE'
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	136	resolve_tac ctxt split_connectI ORELSE'
62391 1658fc9b2618 more canonical names nipkow parents: 62320 diff changeset	137	Splitter.split_asm_tac ctxt (if_split_asm :: split_asms) ORELSE'
1658fc9b2618 more canonical names nipkow parents: 62320 diff changeset	138	Splitter.split_tac ctxt (if_split :: splits) ORELSE'
61760 1647bb489522 tuned whitespace blanchet parents: 60801 diff changeset	139	eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN'
1647bb489522 tuned whitespace blanchet parents: 60801 diff changeset	140	assume_tac ctxt ORELSE'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	141	etac ctxt notE THEN' assume_tac ctxt ORELSE'
55067 a452de24a877 tuned names blanchet parents: 55061 diff changeset	142	(CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
57279 88263522c31e made tactic more robust in the face of 'primcorec' specifications containing 'case_sum' blanchet parents: 55990 diff changeset	143	sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
57399 cfc19f0a6261 compile blanchet parents: 57279 diff changeset	144	mapsx @ map_ident0s @ map_comps))) ORELSE'
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	145	fo_rtac ctxt @{thm cong} ORELSE'
26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	146	rtac ctxt @{thm ext} ORELSE'
59610 8273b65620f9 strengthened tactic blanchet parents: 59582 diff changeset	147	mk_primcorec_assumption_tac ctxt []));
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	148
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	149	fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	150	HEADGOAL (rtac ctxt ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
61760 1647bb489522 tuned whitespace blanchet parents: 60801 diff changeset	151	(the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN'
1647bb489522 tuned whitespace blanchet parents: 60801 diff changeset	152	REPEAT_DETERM_N m o assume_tac ctxt) THEN
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	153	unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac ctxt refl);
53706 9e28c41e3595 more primcorec tactics blanchet parents: 53702 diff changeset	154
54138 c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	155	fun inst_split_eq ctxt split =
59582 0fbed69ff081 tuned signature -- prefer qualified names; wenzelm parents: 59580 diff changeset	156	(case Thm.prop_of split of
54138 c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	157	@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) =>
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	158	let
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	159	val s = Name.uu;
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	160	val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
60801 7664e0916eec tuned signature; wenzelm parents: 60784 diff changeset	161	val split' = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split;
54138 c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	162	in
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	163	Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split'
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	164	end
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	165	\| _ => split);
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	166
54978 afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...' blanchet parents: 54977 diff changeset	167	fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
54138 c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	168	let
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	169	val splits' =
62391 1658fc9b2618 more canonical names nipkow parents: 62320 diff changeset	170	map (fn th => th RS iffD2) (@{thm if_split_eq2} :: map (inst_split_eq ctxt) splits);
54138 c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	171	in
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	172	HEADGOAL (REPEAT o (resolve_tac ctxt (splits' @ split_connectI))) THEN
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	173	prelude_tac ctxt [] (fun_ctr RS trans) THEN
54138 c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	174	HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	175	SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	176	(rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	177	resolve_tac ctxt (@{thm Code.abort_def} :: split_connectI) ORELSE'
62391 1658fc9b2618 more canonical names nipkow parents: 62320 diff changeset	178	Splitter.split_tac ctxt (if_split :: splits) ORELSE'
1658fc9b2618 more canonical names nipkow parents: 62320 diff changeset	179	Splitter.split_asm_tac ctxt (if_split_asm :: split_asms) ORELSE'
54138 c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	180	mk_primcorec_assumption_tac ctxt discIs ORELSE'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	181	distinct_in_prems_tac ctxt distincts ORELSE'
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	182	(TRY o dresolve_tac ctxt discIs) THEN' etac ctxt notE THEN' assume_tac ctxt)))))
54138 c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	183	end;
53903 27fd72593624 more powerful/robust tactics blanchet parents: 53902 diff changeset	184
54842 a020f7d74fed renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package) blanchet parents: 54832 diff changeset	185	fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'});
54832 789fbbc092d2 implemented 'exhaustive' option in tactic blanchet parents: 54613 diff changeset	186
54978 afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...' blanchet parents: 54977 diff changeset	187	fun mk_primcorec_raw_code_tac ctxt distincts discIs splits split_asms ms fun_ctrs nchotomy_opt =
54832 789fbbc092d2 implemented 'exhaustive' option in tactic blanchet parents: 54613 diff changeset	188	let
789fbbc092d2 implemented 'exhaustive' option in tactic blanchet parents: 54613 diff changeset	189	val n = length ms;
54900 136fe16e726a generate 'disc_iff' property in 'primcorec' blanchet parents: 54899 diff changeset	190	val (ms', fun_ctrs') =
54926 28b621fce2f9 more SML-ish (less Haskell-ish) naming convention blanchet parents: 54925 diff changeset	191	(case nchotomy_opt of
54900 136fe16e726a generate 'disc_iff' property in 'primcorec' blanchet parents: 54899 diff changeset	192	NONE => (ms, fun_ctrs)
54842 a020f7d74fed renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package) blanchet parents: 54832 diff changeset	193	\| SOME nchotomy =>
54832 789fbbc092d2 implemented 'exhaustive' option in tactic blanchet parents: 54613 diff changeset	194	(ms \|> split_last \|\|> K [n - 1] \|> op @,
54900 136fe16e726a generate 'disc_iff' property in 'primcorec' blanchet parents: 54899 diff changeset	195	fun_ctrs
54843 7f30d569da08 made tactic work with theorems with multiple assumptions blanchet parents: 54842 diff changeset	196	\|> split_last
54899 7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec' blanchet parents: 54844 diff changeset	197	\|\|> unfold_thms ctxt [atomize_conjL]
54908 f4ae538b0ba5 gracefully handle single-equation case, where 'nchotomy' is 'True' blanchet parents: 54907 diff changeset	198	\|\|> (fn thm => [rulify_nchotomy n nchotomy RS thm] handle THM _ => [thm])
54843 7f30d569da08 made tactic work with theorems with multiple assumptions blanchet parents: 54842 diff changeset	199	\|> op @));
54832 789fbbc092d2 implemented 'exhaustive' option in tactic blanchet parents: 54613 diff changeset	200	in
54978 afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...' blanchet parents: 54977 diff changeset	201	EVERY (map2 (raw_code_single_tac ctxt distincts discIs splits split_asms) ms' fun_ctrs') THEN
54832 789fbbc092d2 implemented 'exhaustive' option in tactic blanchet parents: 54613 diff changeset	202	IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	203	HEADGOAL (REPEAT_DETERM o resolve_tac ctxt (refl :: split_connectI)))
54832 789fbbc092d2 implemented 'exhaustive' option in tactic blanchet parents: 54613 diff changeset	204	end;
53693 71b020d161c5 new tactics for constructor view blanchet parents: 53692 diff changeset	205
54978 afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...' blanchet parents: 54977 diff changeset	206	fun mk_primcorec_code_tac ctxt distincts splits raw =
60728 26ffdb966759 {r,e,d,f}tac with proper context in BNF traytel parents: 60251 diff changeset	207	HEADGOAL (rtac ctxt raw ORELSE' rtac ctxt (raw RS trans) THEN'
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	208	SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	209	(rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	210	resolve_tac ctxt split_connectI ORELSE'
62391 1658fc9b2618 more canonical names nipkow parents: 62320 diff changeset	211	Splitter.split_tac ctxt (if_split :: splits) ORELSE'
60752 b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	212	distinct_in_prems_tac ctxt distincts ORELSE'
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	213	rtac ctxt sym THEN' assume_tac ctxt ORELSE'
b48830b670a1 prefer tactics with explicit context; wenzelm parents: 60735 diff changeset	214	etac ctxt notE THEN' assume_tac ctxt));
53921 46fc95abef09 tactic cleanup blanchet parents: 53910 diff changeset	215
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	216	end;

author	wenzelm
	Thu, 18 May 2017 14:14:20 +0200
changeset 65865	177b90f33f40
parent 64629	a331208010b6
child 67700	0455834f7817
permissions	-rw-r--r--