author | blanchet |
Thu, 02 Jan 2014 23:07:49 +0100 | |
changeset 54920 | 8f50ad61b0a9 |
parent 54919 | 7fad0747e40f |
child 54923 | ffed2452f5f6 |
permissions | -rw-r--r-- |
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54174
diff
changeset
|
1 |
(* Title: HOL/BNF/Tools/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 |
54174 | 11 |
val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic |
53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset
|
12 |
val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic |
53693 | 13 |
val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> |
14 |
tactic |
|
54917
a426e38a8a7e
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents:
54916
diff
changeset
|
15 |
val mk_primcorec_disc_iff_tac: Proof.context -> thm -> thm -> thm list list -> thm list -> tactic |
54844 | 16 |
val mk_primcorec_exhaust_tac: int -> thm -> tactic |
54043 | 17 |
val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list -> |
54613 | 18 |
thm list -> int list -> thm list -> thm option -> tactic |
53910 | 19 |
val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list -> |
54279 | 20 |
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
|
21 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
22 |
|
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54174
diff
changeset
|
23 |
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
|
24 |
struct |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
25 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
26 |
open BNF_Util |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
27 |
open BNF_Tactics |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
28 |
|
54899
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54844
diff
changeset
|
29 |
val atomize_conjL = @{thm atomize_conjL}; |
53905 | 30 |
val falseEs = @{thms not_TrueE FalseE}; |
54174 | 31 |
val Let_def = @{thm Let_def}; |
53910 | 32 |
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
|
33 |
val split_if = @{thm split_if}; |
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset
|
34 |
val split_if_asm = @{thm split_if_asm}; |
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset
|
35 |
val split_connectI = @{thms allI impI conjI}; |
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset
|
36 |
|
54844 | 37 |
fun mk_primcorec_exhaust_tac n nchotomy = |
38 |
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
|
39 |
HEADGOAL (atac ORELSE' |
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54900
diff
changeset
|
40 |
cut_tac nchotomy THEN' |
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54900
diff
changeset
|
41 |
EVERY' (map (fn k => |
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54900
diff
changeset
|
42 |
(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
|
43 |
REPEAT o (dtac meta_mp THEN' atac ORELSE' |
8f50ad61b0a9
generalized tactic to the case of several assumptions per equation
blanchet
parents:
54919
diff
changeset
|
44 |
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
|
45 |
atac)) |
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54900
diff
changeset
|
46 |
ks)) |
54844 | 47 |
end; |
48 |
||
53903 | 49 |
fun mk_primcorec_assumption_tac ctxt discIs = |
54044
93ab44e992ae
strengthened tactic (primcorec_sel_tac) + tuning
blanchet
parents:
54043
diff
changeset
|
50 |
SELECT_GOAL (unfold_thms_tac ctxt |
54069
3fd3b1683d2b
strengthen the tactics to bring them in sync with the simplifications taking place in the code (and weaken the simplifications a bit -- let's not deal with implies)
blanchet
parents:
54044
diff
changeset
|
51 |
@{thms not_not not_False_eq_True not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN |
53926 | 52 |
SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE' |
54117
32730ba3ab85
strengthened tactic to deal with 'False ==> ...'
blanchet
parents:
54103
diff
changeset
|
53 |
eresolve_tac falseEs ORELSE' |
53903 | 54 |
resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE' |
53929 | 55 |
dresolve_tac discIs THEN' atac ORELSE' |
56 |
etac notE THEN' atac ORELSE' |
|
54044
93ab44e992ae
strengthened tactic (primcorec_sel_tac) + tuning
blanchet
parents:
54043
diff
changeset
|
57 |
etac disjE)))); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
58 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
59 |
fun mk_primcorec_same_case_tac m = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
60 |
HEADGOAL (if m = 0 then rtac TrueI |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
61 |
else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
62 |
|
54069
3fd3b1683d2b
strengthen the tactics to bring them in sync with the simplifications taking place in the code (and weaken the simplifications a bit -- let's not deal with implies)
blanchet
parents:
54044
diff
changeset
|
63 |
fun mk_primcorec_different_case_tac ctxt m excl = |
3fd3b1683d2b
strengthen the tactics to bring them in sync with the simplifications taking place in the code (and weaken the simplifications a bit -- let's not deal with implies)
blanchet
parents:
54044
diff
changeset
|
64 |
HEADGOAL (if m = 0 then mk_primcorec_assumption_tac ctxt [] |
3fd3b1683d2b
strengthen the tactics to bring them in sync with the simplifications taking place in the code (and weaken the simplifications a bit -- let's not deal with implies)
blanchet
parents:
54044
diff
changeset
|
65 |
else dtac excl THEN' (REPEAT_DETERM_N (m - 1) o atac) THEN' 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
|
66 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
67 |
fun mk_primcorec_cases_tac ctxt k m exclsss = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
68 |
let val n = length exclsss in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
69 |
EVERY (map (fn [] => if k = n then all_tac else mk_primcorec_same_case_tac m |
54069
3fd3b1683d2b
strengthen the tactics to bring them in sync with the simplifications taking place in the code (and weaken the simplifications a bit -- let's not deal with implies)
blanchet
parents:
54044
diff
changeset
|
70 |
| [excl] => mk_primcorec_different_case_tac ctxt m excl) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
71 |
(take k (nth exclsss (k - 1)))) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
72 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
73 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
74 |
fun mk_primcorec_prelude ctxt defs thm = |
54024 | 75 |
unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN |
76 |
unfold_thms_tac ctxt @{thms Let_def split}; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
77 |
|
53706 | 78 |
fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss = |
79 |
mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
80 |
|
54917
a426e38a8a7e
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents:
54916
diff
changeset
|
81 |
fun mk_primcorec_disc_iff_tac ctxt fun_exhaust fun_disc fun_discss disc_excludes = |
54910 | 82 |
HEADGOAL (rtac iffI THEN' |
83 |
rtac fun_exhaust THEN' |
|
54917
a426e38a8a7e
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents:
54916
diff
changeset
|
84 |
EVERY' (map (fn [] => etac FalseE |
a426e38a8a7e
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents:
54916
diff
changeset
|
85 |
| [fun_disc'] => |
a426e38a8a7e
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents:
54916
diff
changeset
|
86 |
if Thm.eq_thm (fun_disc', fun_disc) then |
a426e38a8a7e
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents:
54916
diff
changeset
|
87 |
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
|
88 |
else |
54918 | 89 |
rtac FalseE THEN' rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac THEN' |
90 |
dresolve_tac disc_excludes 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
|
91 |
fun_discss) THEN' |
54910 | 92 |
rtac (unfold_thms ctxt [atomize_conjL] fun_disc) THEN_MAYBE' atac); |
54899
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54844
diff
changeset
|
93 |
|
54900 | 94 |
fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps fun_sel k m |
53910 | 95 |
exclsss = |
54900 | 96 |
mk_primcorec_prelude ctxt defs (fun_sel RS trans) THEN |
53693 | 97 |
mk_primcorec_cases_tac ctxt k m exclsss THEN |
54018
bd2e127389f2
strengthened tactic for right-hand sides involving lambdas
blanchet
parents:
53961
diff
changeset
|
98 |
HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE' |
53905 | 99 |
eresolve_tac falseEs ORELSE' |
53902
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset
|
100 |
resolve_tac split_connectI ORELSE' |
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset
|
101 |
Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' |
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset
|
102 |
Splitter.split_tac (split_if :: splits) ORELSE' |
53910 | 103 |
eresolve_tac (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
|
104 |
etac notE THEN' atac ORELSE' |
93ab44e992ae
strengthened tactic (primcorec_sel_tac) + tuning
blanchet
parents:
54043
diff
changeset
|
105 |
(CHANGED o SELECT_GOAL (unfold_thms_tac ctxt |
54900 | 106 |
(@{thms id_def o_def split_def sum.cases} @ map_comps @ map_idents))))); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
107 |
|
54900 | 108 |
fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_fun sel_funs = |
109 |
HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' |
|
110 |
(the_default (K all_tac) (Option.map rtac maybe_disc_fun)) THEN' REPEAT_DETERM_N m o atac) THEN |
|
111 |
unfold_thms_tac ctxt (Let_def :: sel_funs) THEN HEADGOAL (rtac refl); |
|
53706 | 112 |
|
54138
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
113 |
fun inst_split_eq ctxt split = |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
114 |
(case prop_of split of |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
115 |
@{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
|
116 |
let |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
117 |
val s = Name.uu; |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
118 |
val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0)); |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
119 |
val split' = Drule.instantiate' [] [SOME (certify ctxt eq)] split; |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
120 |
in |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
121 |
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
|
122 |
end |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
123 |
| _ => split); |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
124 |
|
54174 | 125 |
fun distinct_in_prems_tac distincts = |
126 |
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac; |
|
127 |
||
54900 | 128 |
fun mk_primcorec_raw_code_of_ctr_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
|
129 |
let |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
130 |
val splits' = |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
131 |
map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits) |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
132 |
in |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
133 |
HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN |
54900 | 134 |
mk_primcorec_prelude 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
|
135 |
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
|
136 |
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
|
137 |
(rtac refl ORELSE' atac ORELSE' |
54174 | 138 |
resolve_tac (@{thm Code.abort_def} :: split_connectI) ORELSE' |
139 |
Splitter.split_tac (split_if :: splits) ORELSE' |
|
54138
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
140 |
Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
141 |
mk_primcorec_assumption_tac ctxt discIs ORELSE' |
54174 | 142 |
distinct_in_prems_tac distincts ORELSE' |
54138
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
143 |
(TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))))) |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
144 |
end; |
53903 | 145 |
|
54842
a020f7d74fed
renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
blanchet
parents:
54832
diff
changeset
|
146 |
fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'}); |
54832 | 147 |
|
54900 | 148 |
fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms 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
|
149 |
maybe_nchotomy = |
54832 | 150 |
let |
151 |
val n = length ms; |
|
54900 | 152 |
val (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
|
153 |
(case maybe_nchotomy of |
54900 | 154 |
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
|
155 |
| SOME nchotomy => |
54832 | 156 |
(ms |> split_last ||> K [n - 1] |> op @, |
54900 | 157 |
fun_ctrs |
54843
7f30d569da08
made tactic work with theorems with multiple assumptions
blanchet
parents:
54842
diff
changeset
|
158 |
|> split_last |
54899
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54844
diff
changeset
|
159 |
||> unfold_thms ctxt [atomize_conjL] |
54908
f4ae538b0ba5
gracefully handle single-equation case, where 'nchotomy' is 'True'
blanchet
parents:
54907
diff
changeset
|
160 |
||> (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
|
161 |
|> op @)); |
54832 | 162 |
in |
163 |
EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) |
|
54900 | 164 |
ms' fun_ctrs') THEN |
54832 | 165 |
IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN |
166 |
HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI))) |
|
167 |
end; |
|
53693 | 168 |
|
54174 | 169 |
fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw = |
54101 | 170 |
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' |
54174 | 171 |
SELECT_GOAL (unfold_thms_tac ctxt [Let_def]) THEN' REPEAT_DETERM o |
172 |
(rtac refl ORELSE' atac ORELSE' |
|
53904 | 173 |
resolve_tac split_connectI ORELSE' |
174 |
Splitter.split_tac (split_if :: splits) ORELSE' |
|
54174 | 175 |
distinct_in_prems_tac distincts ORELSE' |
176 |
rtac sym THEN' atac ORELSE' |
|
54042 | 177 |
etac notE THEN' atac)); |
53921 | 178 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
179 |
end; |