isabelle: src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML@2da9b632069b (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};
53902 396999552212 use standard "split" properties instead of ad hoc "eq_...I" blanchet parents: 53901 diff changeset	35	val split_if = @{thm split_if};
396999552212 use standard "split" properties instead of ad hoc "eq_...I" blanchet parents: 53901 diff changeset	36	val split_if_asm = @{thm split_if_asm};
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
60251 98754695b421 made split-rule tactic go beyond constructors with 20 arguments blanchet parents: 59621 diff changeset	40	fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
98754695b421 made split-rule tactic go beyond constructors with 20 arguments blanchet parents: 59621 diff changeset	41
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	42	fun exhaust_inst_as_projs ctxt frees thm =
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	43	let
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	44	val num_frees = length frees;
59582 0fbed69ff081 tuned signature -- prefer qualified names; wenzelm parents: 59580 diff changeset	45	val fs = Term.add_vars (Thm.prop_of thm) [] \|> filter (can dest_funT o snd);
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	46	fun find s = find_index (curry (op =) s) frees;
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	47	fun mk_cfp (f as ((s, _), T)) =
59621 291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context; wenzelm parents: 59611 diff changeset	48	(Thm.cterm_of ctxt (Var f), Thm.cterm_of ctxt (mk_proj T num_frees (find s)));
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	49	val cfps = map mk_cfp fs;
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	50	in
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	51	Drule.cterm_instantiate cfps thm
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	52	end;
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	53
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	54	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	55
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	56	fun distinct_in_prems_tac distincts =
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	57	eresolve0_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	58
57983 6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57399 diff changeset	59	fun mk_primcorec_nchotomy_tac ctxt exhaust_discs =
6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57399 diff changeset	60	HEADGOAL (Method.insert_tac exhaust_discs THEN' clean_blast_tac ctxt);
54924 44373f3560c7 refactoring blanchet parents: 54923 diff changeset	61
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	62	fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
54844 630ba4d8a206 generate exhaust from nchotomy blanchet parents: 54843 diff changeset	63	let val ks = 1 upto n in
54905 2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness blanchet parents: 54900 diff changeset	64	HEADGOAL (atac ORELSE'
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness blanchet parents: 54900 diff changeset	65	cut_tac nchotomy THEN'
54923 ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble blanchet parents: 54920 diff changeset	66	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	67	EVERY' (map (fn k =>
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness blanchet parents: 54900 diff changeset	68	(if k < n then etac disjE else K all_tac) THEN'
54920 8f50ad61b0a9 generalized tactic to the case of several assumptions per equation blanchet parents: 54919 diff changeset	69	REPEAT o (dtac meta_mp THEN' atac ORELSE'
8f50ad61b0a9 generalized tactic to the case of several assumptions per equation blanchet parents: 54919 diff changeset	70	etac conjE THEN' dtac meta_mp THEN' atac ORELSE'
8f50ad61b0a9 generalized tactic to the case of several assumptions per equation blanchet parents: 54919 diff changeset	71	atac))
54905 2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness blanchet parents: 54900 diff changeset	72	ks))
54844 630ba4d8a206 generate exhaust from nchotomy blanchet parents: 54843 diff changeset	73	end;
630ba4d8a206 generate exhaust from nchotomy blanchet parents: 54843 diff changeset	74
53903 27fd72593624 more powerful/robust tactics blanchet parents: 53902 diff changeset	75	fun mk_primcorec_assumption_tac ctxt discIs =
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	76	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	77	not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
53926 9fc9a59ad579 strengthened tactic blanchet parents: 53922 diff changeset	78	SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	79	eresolve_tac ctxt falseEs ORELSE'
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	80	resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE'
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	81	dresolve_tac ctxt discIs THEN' atac ORELSE'
53929 8c5aaf557421 further strengthening of tactics blanchet parents: 53926 diff changeset	82	etac notE THEN' atac ORELSE'
54044 93ab44e992ae strengthened tactic (primcorec_sel_tac) + tuning blanchet parents: 54043 diff changeset	83	etac disjE))));
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	84
59274 67afe7e6a516 use proper context in function desharna parents: 58956 diff changeset	85	fun ss_fst_snd_conv ctxt = 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	86
59274 67afe7e6a516 use proper context in function desharna parents: 58956 diff changeset	87	fun case_atac ctxt = 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	88
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	89	fun same_case_tac ctxt m =
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	90	HEADGOAL (if m = 0 then rtac TrueI
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	91	else REPEAT_DETERM_N (m - 1) o (rtac 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	92
54971 b4b828025880 tuning blanchet parents: 54969 diff changeset	93	fun different_case_tac ctxt m exclude =
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	94	HEADGOAL (if m = 0 then
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	95	mk_primcorec_assumption_tac ctxt []
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	96	else
54971 b4b828025880 tuning blanchet parents: 54969 diff changeset	97	dtac 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	98	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	99
54971 b4b828025880 tuning blanchet parents: 54969 diff changeset	100	fun cases_tac ctxt k m excludesss =
b4b828025880 tuning blanchet parents: 54969 diff changeset	101	let val n = length excludesss in
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	102	EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m
54971 b4b828025880 tuning blanchet parents: 54969 diff changeset	103	\| [exclude] => different_case_tac ctxt m exclude)
b4b828025880 tuning blanchet parents: 54969 diff changeset	104	(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	105	end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	106
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	107	fun prelude_tac ctxt defs thm =
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	108	unfold_thms_tac ctxt defs THEN HEADGOAL (rtac 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	109
57983 6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57399 diff changeset	110	fun mk_primcorec_disc_tac ctxt defs corec_disc k m excludesss =
6edc3529bb4e reordered some (co)datatype property names for more consistency blanchet parents: 57399 diff changeset	111	prelude_tac ctxt 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	112
54969 0ac0b6576d21 generate 'disc_iff' for all discriminators blanchet parents: 54959 diff changeset	113	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	114	distinct_discs =
54910 0ec2cccbf8ad properly synchronize parallel lists blanchet parents: 54909 diff changeset	115	HEADGOAL (rtac iffI THEN'
0ec2cccbf8ad properly synchronize parallel lists blanchet parents: 54909 diff changeset	116	rtac 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	117	K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN'
54917 a426e38a8a7e made tactic handle corner cases, where some of the 'disc' properties are missing, correctly blanchet parents: 54916 diff changeset	118	EVERY' (map (fn [] => etac FalseE
54969 0ac0b6576d21 generate 'disc_iff' for all discriminators blanchet parents: 54959 diff changeset	119	\| fun_discs' as [fun_disc'] =>
0ac0b6576d21 generate 'disc_iff' for all discriminators blanchet parents: 54959 diff changeset	120	if eq_list Thm.eq_thm (fun_discs', fun_discs) then
54917 a426e38a8a7e made tactic handle corner cases, where some of the 'disc' properties are missing, correctly blanchet parents: 54916 diff changeset	121	REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI)
a426e38a8a7e made tactic handle corner cases, where some of the 'disc' properties are missing, correctly blanchet parents: 54916 diff changeset	122	else
54977 63a5e0d8ce3b strengthened tactic to handle 'disc_iff' equations of the form '... = False' blanchet parents: 54971 diff changeset	123	rtac FalseE THEN'
59611 63f8527db07f strengthened tactic blanchet parents: 59610 diff changeset	124	(rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT o atac ORELSE'
54977 63a5e0d8ce3b strengthened tactic to handle 'disc_iff' equations of the form '... = False' blanchet parents: 54971 diff changeset	125	cut_tac fun_disc') THEN'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	126	dresolve_tac ctxt distinct_discs THEN' etac notE THEN' atac)
54917 a426e38a8a7e made tactic handle corner cases, where some of the 'disc' properties are missing, correctly blanchet parents: 54916 diff changeset	127	fun_discss) THEN'
54977 63a5e0d8ce3b strengthened tactic to handle 'disc_iff' equations of the form '... = False' blanchet parents: 54971 diff changeset	128	(etac FalseE ORELSE'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	129	resolve_tac ctxt (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac));
54899 7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec' blanchet parents: 54844 diff changeset	130
57399 cfc19f0a6261 compile blanchet parents: 57279 diff changeset	131	fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k
54971 b4b828025880 tuning blanchet parents: 54969 diff changeset	132	m excludesss =
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	133	prelude_tac ctxt defs (fun_sel RS trans) THEN
54971 b4b828025880 tuning blanchet parents: 54969 diff changeset	134	cases_tac ctxt k m excludesss THEN
55341 3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas blanchet parents: 55067 diff changeset	135	HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	136	eresolve_tac ctxt falseEs ORELSE'
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	137	resolve_tac ctxt split_connectI ORELSE'
58956 a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options); wenzelm parents: 57983 diff changeset	138	Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options); wenzelm parents: 57983 diff changeset	139	Splitter.split_tac ctxt (split_if :: splits) ORELSE'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	140	eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
54044 93ab44e992ae strengthened tactic (primcorec_sel_tac) + tuning blanchet parents: 54043 diff changeset	141	etac notE THEN' atac 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'
55341 3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas blanchet parents: 55067 diff changeset	145	fo_rtac @{thm cong} ctxt ORELSE'
59610 8273b65620f9 strengthened tactic blanchet parents: 59582 diff changeset	146	rtac @{thm ext} ORELSE'
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 =
54900 136fe16e726a generate 'disc_iff' property in 'primcorec' blanchet parents: 54899 diff changeset	150	HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
54926 28b621fce2f9 more SML-ish (less Haskell-ish) naming convention blanchet parents: 54925 diff changeset	151	(the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN
55004 96dfb73bb11a repaired 'ctr' tactic w.r.t. 'split' blanchet parents: 54978 diff changeset	152	unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl);
53706 9e28c41e3595 more primcorec tactics blanchet parents: 53702 diff changeset	153
54138 c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	154	fun inst_split_eq ctxt split =
59582 0fbed69ff081 tuned signature -- prefer qualified names; wenzelm parents: 59580 diff changeset	155	(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	156	@{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	157	let
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	158	val s = Name.uu;
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	159	val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
59621 291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context; wenzelm parents: 59611 diff changeset	160	val split' = Drule.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	161	in
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	162	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	163	end
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	164	\| _ => split);
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	165
54978 afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...' blanchet parents: 54977 diff changeset	166	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	167	let
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	168	val splits' =
55342 1bd9e637ac9f tuning blanchet parents: 55341 diff changeset	169	map (fn th => th RS iffD2) (@{thm split_if_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	170	in
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	171	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	172	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	173	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	174	SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	175	(rtac refl ORELSE' atac ORELSE'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	176	resolve_tac ctxt (@{thm Code.abort_def} :: split_connectI) ORELSE'
58956 a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options); wenzelm parents: 57983 diff changeset	177	Splitter.split_tac ctxt (split_if :: splits) ORELSE'
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options); wenzelm parents: 57983 diff changeset	178	Splitter.split_asm_tac ctxt (split_if_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	179	mk_primcorec_assumption_tac ctxt discIs ORELSE'
54174 c6291ae7cd18 strengthened tactic blanchet parents: 54164 diff changeset	180	distinct_in_prems_tac distincts ORELSE'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	181	(TRY o dresolve_tac ctxt discIs) THEN' etac notE THEN' atac)))))
54138 c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk blanchet parents: 54133 diff changeset	182	end;
53903 27fd72593624 more powerful/robust tactics blanchet parents: 53902 diff changeset	183
54842 a020f7d74fed renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package) blanchet parents: 54832 diff changeset	184	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	185
54978 afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...' blanchet parents: 54977 diff changeset	186	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	187	let
789fbbc092d2 implemented 'exhaustive' option in tactic blanchet parents: 54613 diff changeset	188	val n = length ms;
54900 136fe16e726a generate 'disc_iff' property in 'primcorec' blanchet parents: 54899 diff changeset	189	val (ms', fun_ctrs') =
54926 28b621fce2f9 more SML-ish (less Haskell-ish) naming convention blanchet parents: 54925 diff changeset	190	(case nchotomy_opt of
54900 136fe16e726a generate 'disc_iff' property in 'primcorec' blanchet parents: 54899 diff changeset	191	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	192	\| SOME nchotomy =>
54832 789fbbc092d2 implemented 'exhaustive' option in tactic blanchet parents: 54613 diff changeset	193	(ms \|> split_last \|\|> K [n - 1] \|> op @,
54900 136fe16e726a generate 'disc_iff' property in 'primcorec' blanchet parents: 54899 diff changeset	194	fun_ctrs
54843 7f30d569da08 made tactic work with theorems with multiple assumptions blanchet parents: 54842 diff changeset	195	\|> split_last
54899 7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec' blanchet parents: 54844 diff changeset	196	\|\|> unfold_thms ctxt [atomize_conjL]
54908 f4ae538b0ba5 gracefully handle single-equation case, where 'nchotomy' is 'True' blanchet parents: 54907 diff changeset	197	\|\|> (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	198	\|> op @));
54832 789fbbc092d2 implemented 'exhaustive' option in tactic blanchet parents: 54613 diff changeset	199	in
54978 afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...' blanchet parents: 54977 diff changeset	200	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	201	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	202	HEADGOAL (REPEAT_DETERM o resolve_tac ctxt (refl :: split_connectI)))
54832 789fbbc092d2 implemented 'exhaustive' option in tactic blanchet parents: 54613 diff changeset	203	end;
53693 71b020d161c5 new tactics for constructor view blanchet parents: 53692 diff changeset	204
54978 afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...' blanchet parents: 54977 diff changeset	205	fun mk_primcorec_code_tac ctxt distincts splits raw =
54101 94f2dc9aea7a strengthened tactic w.r.t. "let" blanchet parents: 54075 diff changeset	206	HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'
54954 a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples blanchet parents: 54953 diff changeset	207	SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
54174 c6291ae7cd18 strengthened tactic blanchet parents: 54164 diff changeset	208	(rtac refl ORELSE' atac ORELSE'
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 59274 diff changeset	209	resolve_tac ctxt split_connectI ORELSE'
58956 a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options); wenzelm parents: 57983 diff changeset	210	Splitter.split_tac ctxt (split_if :: splits) ORELSE'
54174 c6291ae7cd18 strengthened tactic blanchet parents: 54164 diff changeset	211	distinct_in_prems_tac distincts ORELSE'
c6291ae7cd18 strengthened tactic blanchet parents: 54164 diff changeset	212	rtac sym THEN' atac ORELSE'
54042 ad7a2cfb8cb2 got rid of needless argument blanchet parents: 54024 diff changeset	213	etac notE THEN' atac));
53921 46fc95abef09 tactic cleanup blanchet parents: 53910 diff changeset	214
53303 ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository blanchet parents: diff changeset	215	end;

author	haftmann
	Sat, 27 Jun 2015 20:20:33 +0200
changeset 60597	2da9b632069b
parent 60251	98754695b421
child 60728	26ffdb966759
permissions	-rw-r--r--