author | blanchet |
Tue, 01 Dec 2015 13:07:40 +0100 | |
changeset 61760 | 1647bb489522 |
parent 60801 | 7664e0916eec |
child 61841 | 4d3527b94f2a |
permissions | -rw-r--r-- |
55061 | 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 | 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 |
|
54969 | 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 | 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 | 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 |
|
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 | 45 |
val fs = Term.add_vars (Thm.prop_of thm) [] |> filter (can dest_funT o snd); |
60784 | 46 |
fun find x = find_index (curry (op =) x) frees; |
47 |
fun mk_inst ((x, i), T) = ((x, i), Thm.cterm_of ctxt (mk_proj T num_frees (find x))); |
|
48 |
in infer_instantiate ctxt (map mk_inst fs) thm end; |
|
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
49 |
|
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
50 |
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
|
51 |
|
60752 | 52 |
fun distinct_in_prems_tac ctxt distincts = |
53 |
eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' |
|
54 |
assume_tac ctxt; |
|
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
55 |
|
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57399
diff
changeset
|
56 |
fun mk_primcorec_nchotomy_tac ctxt exhaust_discs = |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57399
diff
changeset
|
57 |
HEADGOAL (Method.insert_tac exhaust_discs THEN' clean_blast_tac ctxt); |
54924 | 58 |
|
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
59 |
fun mk_primcorec_exhaust_tac ctxt frees n nchotomy = |
54844 | 60 |
let val ks = 1 upto n in |
60752 | 61 |
HEADGOAL (assume_tac ctxt ORELSE' |
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54900
diff
changeset
|
62 |
cut_tac nchotomy THEN' |
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54920
diff
changeset
|
63 |
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
|
64 |
EVERY' (map (fn k => |
60728 | 65 |
(if k < n then etac ctxt disjE else K all_tac) THEN' |
60752 | 66 |
REPEAT o (dtac ctxt meta_mp THEN' assume_tac ctxt ORELSE' |
67 |
etac ctxt conjE THEN' dtac ctxt meta_mp THEN' assume_tac ctxt ORELSE' |
|
68 |
assume_tac ctxt)) |
|
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54900
diff
changeset
|
69 |
ks)) |
54844 | 70 |
end; |
71 |
||
53903 | 72 |
fun mk_primcorec_assumption_tac ctxt discIs = |
54954 | 73 |
SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True |
74 |
not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN |
|
61760 | 75 |
SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' |
76 |
etac ctxt conjE ORELSE' |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59274
diff
changeset
|
77 |
eresolve_tac ctxt falseEs ORELSE' |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59274
diff
changeset
|
78 |
resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE' |
60752 | 79 |
dresolve_tac ctxt discIs THEN' assume_tac ctxt ORELSE' |
80 |
etac ctxt notE THEN' assume_tac ctxt ORELSE' |
|
60728 | 81 |
etac ctxt disjE)))); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
82 |
|
60735
cf291b55f3d1
made tactic more robust w.r.t. equations containing 'case_prod'
blanchet
parents:
60728
diff
changeset
|
83 |
fun ss_fst_snd_conv ctxt = |
cf291b55f3d1
made tactic more robust w.r.t. equations containing 'case_prod'
blanchet
parents:
60728
diff
changeset
|
84 |
Raw_Simplifier.simpset_of (ss_only @{thms fst_conv snd_conv} ctxt); |
54954 | 85 |
|
60735
cf291b55f3d1
made tactic more robust w.r.t. equations containing 'case_prod'
blanchet
parents:
60728
diff
changeset
|
86 |
fun case_atac ctxt = |
cf291b55f3d1
made tactic more robust w.r.t. equations containing 'case_prod'
blanchet
parents:
60728
diff
changeset
|
87 |
Simplifier.full_simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt); |
54954 | 88 |
|
89 |
fun same_case_tac ctxt m = |
|
60728 | 90 |
HEADGOAL (if m = 0 then rtac ctxt TrueI |
91 |
else REPEAT_DETERM_N (m - 1) o (rtac ctxt conjI THEN' case_atac ctxt) THEN' case_atac ctxt); |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
92 |
|
54971 | 93 |
fun different_case_tac ctxt m exclude = |
54954 | 94 |
HEADGOAL (if m = 0 then |
95 |
mk_primcorec_assumption_tac ctxt [] |
|
96 |
else |
|
60728 | 97 |
dtac ctxt exclude THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN' |
54954 | 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 | 100 |
fun cases_tac ctxt k m excludesss = |
101 |
let val n = length excludesss in |
|
54954 | 102 |
EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m |
54971 | 103 |
| [exclude] => different_case_tac ctxt m exclude) |
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 | 107 |
fun prelude_tac ctxt defs thm = |
60728 | 108 |
unfold_thms_tac ctxt defs THEN HEADGOAL (rtac ctxt thm) THEN unfold_thms_tac ctxt unfold_lets; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
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 | 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 = |
60728 | 115 |
HEADGOAL (rtac ctxt iffI THEN' |
116 |
rtac ctxt fun_exhaust THEN' |
|
54959
30ded82ff806
fixed 'disc_iff' tactic in the case where different equations use different variable names for the function arguments
blanchet
parents:
54955
diff
changeset
|
117 |
K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN' |
60728 | 118 |
EVERY' (map (fn [] => etac ctxt FalseE |
54969 | 119 |
| fun_discs' as [fun_disc'] => |
120 |
if eq_list Thm.eq_thm (fun_discs', fun_discs) then |
|
60752 | 121 |
REPEAT_DETERM o etac ctxt conjI THEN' (assume_tac ctxt ORELSE' rtac ctxt TrueI) |
54917
a426e38a8a7e
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents:
54916
diff
changeset
|
122 |
else |
60728 | 123 |
rtac ctxt FalseE THEN' |
60752 | 124 |
(rotate_tac 1 THEN' dtac ctxt fun_disc' THEN' REPEAT o assume_tac ctxt ORELSE' |
54977
63a5e0d8ce3b
strengthened tactic to handle 'disc_iff' equations of the form '... = False'
blanchet
parents:
54971
diff
changeset
|
125 |
cut_tac fun_disc') THEN' |
60752 | 126 |
dresolve_tac ctxt distinct_discs THEN' etac ctxt notE THEN' assume_tac ctxt) |
54917
a426e38a8a7e
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents:
54916
diff
changeset
|
127 |
fun_discss) THEN' |
60728 | 128 |
(etac ctxt FalseE ORELSE' |
60752 | 129 |
resolve_tac ctxt |
130 |
(map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' assume_tac ctxt)); |
|
54899
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54844
diff
changeset
|
131 |
|
57399 | 132 |
fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k |
54971 | 133 |
m excludesss = |
54954 | 134 |
prelude_tac ctxt defs (fun_sel RS trans) THEN |
54971 | 135 |
cases_tac ctxt k m excludesss THEN |
60728 | 136 |
HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59274
diff
changeset
|
137 |
eresolve_tac ctxt falseEs ORELSE' |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59274
diff
changeset
|
138 |
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
|
139 |
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
|
140 |
Splitter.split_tac ctxt (split_if :: splits) ORELSE' |
61760 | 141 |
eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' |
142 |
assume_tac ctxt ORELSE' |
|
60752 | 143 |
etac ctxt notE THEN' assume_tac ctxt ORELSE' |
55067 | 144 |
(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
|
145 |
sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @ |
57399 | 146 |
mapsx @ map_ident0s @ map_comps))) ORELSE' |
60728 | 147 |
fo_rtac ctxt @{thm cong} ORELSE' |
148 |
rtac ctxt @{thm ext} ORELSE' |
|
59610 | 149 |
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
|
150 |
|
54954 | 151 |
fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = |
60728 | 152 |
HEADGOAL (rtac ctxt ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' |
61760 | 153 |
(the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN' |
154 |
REPEAT_DETERM_N m o assume_tac ctxt) THEN |
|
60728 | 155 |
unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac ctxt refl); |
53706 | 156 |
|
54138
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
157 |
fun inst_split_eq ctxt split = |
59582 | 158 |
(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
|
159 |
@{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
|
160 |
let |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
161 |
val s = Name.uu; |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
162 |
val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0)); |
60801 | 163 |
val split' = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split; |
54138
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
164 |
in |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
165 |
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
|
166 |
end |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
167 |
| _ => split); |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
168 |
|
54978
afc156c7e4f7
cope gracefully with missing ctr equations by plugging in 'False ==> ...'
blanchet
parents:
54977
diff
changeset
|
169 |
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
|
170 |
let |
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
171 |
val splits' = |
55342 | 172 |
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
|
173 |
in |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59274
diff
changeset
|
174 |
HEADGOAL (REPEAT o (resolve_tac ctxt (splits' @ split_connectI))) THEN |
54954 | 175 |
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
|
176 |
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
|
177 |
SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o |
60752 | 178 |
(rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59274
diff
changeset
|
179 |
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
|
180 |
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
|
181 |
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
|
182 |
mk_primcorec_assumption_tac ctxt discIs ORELSE' |
60752 | 183 |
distinct_in_prems_tac ctxt distincts ORELSE' |
184 |
(TRY o dresolve_tac ctxt discIs) THEN' etac ctxt notE THEN' assume_tac ctxt))))) |
|
54138
c7119e1cde3e
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents:
54133
diff
changeset
|
185 |
end; |
53903 | 186 |
|
54842
a020f7d74fed
renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
blanchet
parents:
54832
diff
changeset
|
187 |
fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'}); |
54832 | 188 |
|
54978
afc156c7e4f7
cope gracefully with missing ctr equations by plugging in 'False ==> ...'
blanchet
parents:
54977
diff
changeset
|
189 |
fun mk_primcorec_raw_code_tac ctxt distincts discIs splits split_asms ms fun_ctrs nchotomy_opt = |
54832 | 190 |
let |
191 |
val n = length ms; |
|
54900 | 192 |
val (ms', fun_ctrs') = |
54926
28b621fce2f9
more SML-ish (less Haskell-ish) naming convention
blanchet
parents:
54925
diff
changeset
|
193 |
(case nchotomy_opt of |
54900 | 194 |
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
|
195 |
| SOME nchotomy => |
54832 | 196 |
(ms |> split_last ||> K [n - 1] |> op @, |
54900 | 197 |
fun_ctrs |
54843
7f30d569da08
made tactic work with theorems with multiple assumptions
blanchet
parents:
54842
diff
changeset
|
198 |
|> split_last |
54899
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54844
diff
changeset
|
199 |
||> unfold_thms ctxt [atomize_conjL] |
54908
f4ae538b0ba5
gracefully handle single-equation case, where 'nchotomy' is 'True'
blanchet
parents:
54907
diff
changeset
|
200 |
||> (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
|
201 |
|> op @)); |
54832 | 202 |
in |
54978
afc156c7e4f7
cope gracefully with missing ctr equations by plugging in 'False ==> ...'
blanchet
parents:
54977
diff
changeset
|
203 |
EVERY (map2 (raw_code_single_tac ctxt distincts discIs splits split_asms) ms' fun_ctrs') THEN |
54832 | 204 |
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
|
205 |
HEADGOAL (REPEAT_DETERM o resolve_tac ctxt (refl :: split_connectI))) |
54832 | 206 |
end; |
53693 | 207 |
|
54978
afc156c7e4f7
cope gracefully with missing ctr equations by plugging in 'False ==> ...'
blanchet
parents:
54977
diff
changeset
|
208 |
fun mk_primcorec_code_tac ctxt distincts splits raw = |
60728 | 209 |
HEADGOAL (rtac ctxt raw ORELSE' rtac ctxt (raw RS trans) THEN' |
54954 | 210 |
SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o |
60752 | 211 |
(rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59274
diff
changeset
|
212 |
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
|
213 |
Splitter.split_tac ctxt (split_if :: splits) ORELSE' |
60752 | 214 |
distinct_in_prems_tac ctxt distincts ORELSE' |
215 |
rtac ctxt sym THEN' assume_tac ctxt ORELSE' |
|
216 |
etac ctxt notE THEN' assume_tac ctxt)); |
|
53921 | 217 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
218 |
end; |