author | blanchet |
Fri, 10 Jan 2014 09:48:11 +0100 | |
changeset 54959 | 30ded82ff806 |
parent 54955 | cf8d429dc24e |
child 54969 | 0ac0b6576d21 |
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 |
54954 | 12 |
val mk_primcorec_ctr_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 -> |
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 | 33 |
val falseEs = @{thms not_TrueE FalseE}; |
53910 | 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 | 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; |
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 = |
54954 | 74 |
SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True |
75 |
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 |
|
54954 | 83 |
val ss_fst_snd_conv = simpset_of (ss_only @{thms fst_conv snd_conv} @{context}); |
84 |
||
85 |
fun case_atac ctxt = simp_tac (put_simpset ss_fst_snd_conv ctxt); |
|
86 |
||
87 |
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
|
88 |
HEADGOAL (if m = 0 then rtac TrueI |
54954 | 89 |
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
|
90 |
|
54954 | 91 |
fun different_case_tac ctxt m excl = |
92 |
HEADGOAL (if m = 0 then |
|
93 |
mk_primcorec_assumption_tac ctxt [] |
|
94 |
else |
|
95 |
dtac excl THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN' |
|
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 |
|
54954 | 98 |
fun 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
|
99 |
let val n = length exclsss in |
54954 | 100 |
EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m |
101 |
| [excl] => 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
|
102 |
(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
|
103 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
104 |
|
54954 | 105 |
fun prelude_tac ctxt defs thm = |
106 |
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
|
107 |
|
53706 | 108 |
fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss = |
54954 | 109 |
prelude_tac ctxt defs disc_corec THEN 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
|
110 |
|
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
|
111 |
fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_disc fun_discss disc_excludes = |
54910 | 112 |
HEADGOAL (rtac iffI THEN' |
113 |
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
|
114 |
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
|
115 |
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
|
116 |
| [fun_disc'] => |
a426e38a8a7e
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents:
54916
diff
changeset
|
117 |
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
|
118 |
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
|
119 |
else |
54918 | 120 |
rtac FalseE THEN' rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac THEN' |
121 |
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
|
122 |
fun_discss) THEN' |
54910 | 123 |
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
|
124 |
|
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset
|
125 |
fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_idents map_comps fun_sel k |
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset
|
126 |
m exclsss = |
54954 | 127 |
prelude_tac ctxt defs (fun_sel RS trans) THEN |
128 |
cases_tac ctxt k m exclsss THEN |
|
54018
bd2e127389f2
strengthened tactic for right-hand sides involving lambdas
blanchet
parents:
53961
diff
changeset
|
129 |
HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE' |
53905 | 130 |
eresolve_tac falseEs ORELSE' |
53902
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset
|
131 |
resolve_tac split_connectI ORELSE' |
396999552212
use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents:
53901
diff
changeset
|
132 |
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
|
133 |
Splitter.split_tac (split_if :: splits) ORELSE' |
53910 | 134 |
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
|
135 |
etac notE THEN' atac ORELSE' |
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset
|
136 |
(CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def o_def split_def |
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset
|
137 |
sum.cases} @ mapsx @ 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
|
138 |
|
54954 | 139 |
fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = |
54900 | 140 |
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
|
141 |
(the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN |
54953 | 142 |
unfold_thms_tac ctxt (unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl); |
53706 | 143 |
|
54138
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
144 |
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
|
145 |
(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
|
146 |
@{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
|
147 |
let |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
148 |
val s = Name.uu; |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
149 |
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
|
150 |
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
|
151 |
in |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
152 |
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
|
153 |
end |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
154 |
| _ => split); |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
155 |
|
54954 | 156 |
fun 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
|
157 |
let |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
158 |
val splits' = |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
159 |
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
|
160 |
in |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
161 |
HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN |
54954 | 162 |
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
|
163 |
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
|
164 |
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
|
165 |
(rtac refl ORELSE' atac ORELSE' |
54174 | 166 |
resolve_tac (@{thm Code.abort_def} :: split_connectI) ORELSE' |
167 |
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
|
168 |
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
|
169 |
mk_primcorec_assumption_tac ctxt discIs ORELSE' |
54174 | 170 |
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
|
171 |
(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
|
172 |
end; |
53903 | 173 |
|
54842
a020f7d74fed
renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
blanchet
parents:
54832
diff
changeset
|
174 |
fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'}); |
54832 | 175 |
|
54900 | 176 |
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
|
177 |
nchotomy_opt = |
54832 | 178 |
let |
179 |
val n = length ms; |
|
54900 | 180 |
val (ms', fun_ctrs') = |
54926
28b621fce2f9
more SML-ish (less Haskell-ish) naming convention
blanchet
parents:
54925
diff
changeset
|
181 |
(case nchotomy_opt of |
54900 | 182 |
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
|
183 |
| SOME nchotomy => |
54832 | 184 |
(ms |> split_last ||> K [n - 1] |> op @, |
54900 | 185 |
fun_ctrs |
54843
7f30d569da08
made tactic work with theorems with multiple assumptions
blanchet
parents:
54842
diff
changeset
|
186 |
|> split_last |
54899
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54844
diff
changeset
|
187 |
||> unfold_thms ctxt [atomize_conjL] |
54908
f4ae538b0ba5
gracefully handle single-equation case, where 'nchotomy' is 'True'
blanchet
parents:
54907
diff
changeset
|
188 |
||> (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
|
189 |
|> op @)); |
54832 | 190 |
in |
54954 | 191 |
EVERY (map2 (raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) |
54900 | 192 |
ms' fun_ctrs') THEN |
54832 | 193 |
IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN |
194 |
HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI))) |
|
195 |
end; |
|
53693 | 196 |
|
54174 | 197 |
fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw = |
54101 | 198 |
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' |
54954 | 199 |
SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o |
54174 | 200 |
(rtac refl ORELSE' atac ORELSE' |
53904 | 201 |
resolve_tac split_connectI ORELSE' |
202 |
Splitter.split_tac (split_if :: splits) ORELSE' |
|
54174 | 203 |
distinct_in_prems_tac distincts ORELSE' |
204 |
rtac sym THEN' atac ORELSE' |
|
54042 | 205 |
etac notE THEN' atac)); |
53921 | 206 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
207 |
end; |