author | blanchet |
Fri, 03 Jan 2014 14:14:16 +0100 | |
changeset 54926 | 28b621fce2f9 |
parent 54925 | c63223067cab |
child 54953 | a2f4cf3387fc |
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 |
|
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
15 |
val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm -> thm list list -> |
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 | 18 |
val mk_primcorec_nchotomy_tac: Proof.context -> thm list -> tactic |
54043 | 19 |
val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list -> |
54613 | 20 |
thm list -> int list -> thm list -> thm option -> tactic |
53910 | 21 |
val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list -> |
54279 | 22 |
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 | 33 |
val falseEs = @{thms not_TrueE FalseE}; |
54174 | 34 |
val Let_def = @{thm Let_def}; |
53910 | 35 |
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
|
36 |
val split_if = @{thm split_if}; |
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset
|
37 |
val split_if_asm = @{thm split_if_asm}; |
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset
|
38 |
val split_connectI = @{thms allI impI conjI}; |
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; |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
43 |
val fs = Term.add_vars (prop_of thm) [] |> filter (can dest_funT o snd); |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
44 |
fun find s = find_index (curry (op =) s) frees; |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
45 |
fun mk_cfp (f as ((s, _), T)) = |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
46 |
(certify ctxt (Var f), certify ctxt (mk_proj T num_frees (find s))); |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
47 |
val cfps = map mk_cfp fs; |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
48 |
in |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
49 |
Drule.cterm_instantiate cfps thm |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
50 |
end; |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
51 |
|
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
52 |
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
|
53 |
|
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
54 |
fun distinct_in_prems_tac distincts = |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
55 |
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac; |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
56 |
|
54924 | 57 |
fun mk_primcorec_nchotomy_tac ctxt disc_exhausts = |
54925 | 58 |
HEADGOAL (Method.insert_tac disc_exhausts THEN' clean_blast_tac ctxt); |
54924 | 59 |
|
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
60 |
fun mk_primcorec_exhaust_tac ctxt frees n nchotomy = |
54844 | 61 |
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
|
62 |
HEADGOAL (atac ORELSE' |
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54900
diff
changeset
|
63 |
cut_tac nchotomy THEN' |
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
64 |
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
|
65 |
EVERY' (map (fn k => |
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54900
diff
changeset
|
66 |
(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
|
67 |
REPEAT o (dtac meta_mp THEN' atac ORELSE' |
8f50ad61b0a9
generalized tactic to the case of several assumptions per equation
blanchet
parents:
54919
diff
changeset
|
68 |
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
|
69 |
atac)) |
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54900
diff
changeset
|
70 |
ks)) |
54844 | 71 |
end; |
72 |
||
53903 | 73 |
fun mk_primcorec_assumption_tac ctxt discIs = |
54044
93ab44e992ae
strengthened tactic (primcorec_sel_tac) + tuning
blanchet
parents:
54043
diff
changeset
|
74 |
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
|
75 |
@{thms not_not not_False_eq_True not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN |
53926 | 76 |
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
|
77 |
eresolve_tac falseEs ORELSE' |
53903 | 78 |
resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE' |
53929 | 79 |
dresolve_tac discIs THEN' atac ORELSE' |
80 |
etac notE THEN' atac ORELSE' |
|
54044
93ab44e992ae
strengthened tactic (primcorec_sel_tac) + tuning
blanchet
parents:
54043
diff
changeset
|
81 |
etac disjE)))); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
82 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
83 |
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
|
84 |
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
|
85 |
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
|
86 |
|
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
|
87 |
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
|
88 |
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
|
89 |
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
|
90 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
91 |
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
|
92 |
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
|
93 |
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
|
94 |
| [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
|
95 |
(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
|
96 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
97 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
98 |
fun mk_primcorec_prelude ctxt defs thm = |
54024 | 99 |
unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN |
100 |
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
|
101 |
|
53706 | 102 |
fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss = |
103 |
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
|
104 |
|
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
105 |
fun mk_primcorec_disc_iff_tac ctxt frees fun_exhaust fun_disc fun_discss disc_excludes = |
54910 | 106 |
HEADGOAL (rtac iffI THEN' |
107 |
rtac fun_exhaust THEN' |
|
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
108 |
K (exhaust_inst_as_projs_tac ctxt frees) THEN' |
54917
a426e38a8a7e
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents:
54916
diff
changeset
|
109 |
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
|
110 |
| [fun_disc'] => |
a426e38a8a7e
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents:
54916
diff
changeset
|
111 |
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
|
112 |
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
|
113 |
else |
54918 | 114 |
rtac FalseE THEN' rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac THEN' |
115 |
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
|
116 |
fun_discss) THEN' |
54910 | 117 |
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
|
118 |
|
54900 | 119 |
fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps fun_sel k m |
53910 | 120 |
exclsss = |
54900 | 121 |
mk_primcorec_prelude ctxt defs (fun_sel RS trans) THEN |
53693 | 122 |
mk_primcorec_cases_tac ctxt k m exclsss THEN |
54018
bd2e127389f2
strengthened tactic for right-hand sides involving lambdas
blanchet
parents:
53961
diff
changeset
|
123 |
HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE' |
53905 | 124 |
eresolve_tac falseEs ORELSE' |
53902
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset
|
125 |
resolve_tac split_connectI ORELSE' |
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset
|
126 |
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
|
127 |
Splitter.split_tac (split_if :: splits) ORELSE' |
53910 | 128 |
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
|
129 |
etac notE THEN' atac ORELSE' |
93ab44e992ae
strengthened tactic (primcorec_sel_tac) + tuning
blanchet
parents:
54043
diff
changeset
|
130 |
(CHANGED o SELECT_GOAL (unfold_thms_tac ctxt |
54900 | 131 |
(@{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
|
132 |
|
54926
28b621fce2f9
more SML-ish (less Haskell-ish) naming convention
blanchet
parents:
54925
diff
changeset
|
133 |
fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc_fun_opt sel_funs = |
54900 | 134 |
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
|
135 |
(the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN |
54900 | 136 |
unfold_thms_tac ctxt (Let_def :: sel_funs) THEN HEADGOAL (rtac refl); |
53706 | 137 |
|
54138
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
138 |
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
|
139 |
(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
|
140 |
@{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
|
141 |
let |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
142 |
val s = Name.uu; |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
143 |
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
|
144 |
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
|
145 |
in |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
146 |
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
|
147 |
end |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
148 |
| _ => split); |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
149 |
|
54900 | 150 |
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
|
151 |
let |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
152 |
val splits' = |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
153 |
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
|
154 |
in |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
155 |
HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN |
54900 | 156 |
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
|
157 |
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
|
158 |
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
|
159 |
(rtac refl ORELSE' atac ORELSE' |
54174 | 160 |
resolve_tac (@{thm Code.abort_def} :: split_connectI) ORELSE' |
161 |
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
|
162 |
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
|
163 |
mk_primcorec_assumption_tac ctxt discIs ORELSE' |
54174 | 164 |
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
|
165 |
(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
|
166 |
end; |
53903 | 167 |
|
54842
a020f7d74fed
renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
blanchet
parents:
54832
diff
changeset
|
168 |
fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'}); |
54832 | 169 |
|
54900 | 170 |
fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms fun_ctrs |
54926
28b621fce2f9
more SML-ish (less Haskell-ish) naming convention
blanchet
parents:
54925
diff
changeset
|
171 |
nchotomy_opt = |
54832 | 172 |
let |
173 |
val n = length ms; |
|
54900 | 174 |
val (ms', fun_ctrs') = |
54926
28b621fce2f9
more SML-ish (less Haskell-ish) naming convention
blanchet
parents:
54925
diff
changeset
|
175 |
(case nchotomy_opt of |
54900 | 176 |
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
|
177 |
| SOME nchotomy => |
54832 | 178 |
(ms |> split_last ||> K [n - 1] |> op @, |
54900 | 179 |
fun_ctrs |
54843
7f30d569da08
made tactic work with theorems with multiple assumptions
blanchet
parents:
54842
diff
changeset
|
180 |
|> split_last |
54899
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54844
diff
changeset
|
181 |
||> unfold_thms ctxt [atomize_conjL] |
54908
f4ae538b0ba5
gracefully handle single-equation case, where 'nchotomy' is 'True'
blanchet
parents:
54907
diff
changeset
|
182 |
||> (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
|
183 |
|> op @)); |
54832 | 184 |
in |
185 |
EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) |
|
54900 | 186 |
ms' fun_ctrs') THEN |
54832 | 187 |
IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN |
188 |
HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI))) |
|
189 |
end; |
|
53693 | 190 |
|
54174 | 191 |
fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw = |
54101 | 192 |
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' |
54174 | 193 |
SELECT_GOAL (unfold_thms_tac ctxt [Let_def]) THEN' REPEAT_DETERM o |
194 |
(rtac refl ORELSE' atac ORELSE' |
|
53904 | 195 |
resolve_tac split_connectI ORELSE' |
196 |
Splitter.split_tac (split_if :: splits) ORELSE' |
|
54174 | 197 |
distinct_in_prems_tac distincts ORELSE' |
198 |
rtac sym THEN' atac ORELSE' |
|
54042 | 199 |
etac notE THEN' atac)); |
53921 | 200 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
201 |
end; |