author | blanchet |
Sat, 21 Dec 2013 09:44:30 +0100 | |
changeset 54844 | 630ba4d8a206 |
parent 54701 | 4ed7454aebde |
child 54905 | 2fdec6c29eb7 |
permissions | -rw-r--r-- |
54701 | 1 |
(* Title: HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
54397 | 3 |
Copyright 2012, 2013 |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
4 |
|
51797 | 5 |
Tactics for wrapping existing freely generated type's constructors. |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
6 |
*) |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
7 |
|
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
8 |
signature CTR_SUGAR_GENERAL_TACTICS = |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
9 |
sig |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
10 |
val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
11 |
val unfold_thms_tac: Proof.context -> thm list -> tactic |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
12 |
end; |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
13 |
|
54006 | 14 |
signature CTR_SUGAR_TACTICS = |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
15 |
sig |
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
16 |
include CTR_SUGAR_GENERAL_TACTICS |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
17 |
|
49148
93f281430e77
fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case
blanchet
parents:
49137
diff
changeset
|
18 |
val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic |
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
19 |
val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
20 |
val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic |
54491 | 21 |
val mk_case_eq_if_tac: Proof.context -> int -> thm -> thm list -> thm list list -> |
22 |
thm list list -> tactic |
|
49118 | 23 |
val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic |
49029 | 24 |
val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
25 |
val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list -> |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
26 |
thm list list list -> thm list list list -> tactic |
51798 | 27 |
val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
28 |
val mk_nchotomy_tac: int -> thm -> tactic |
49122 | 29 |
val mk_other_half_disc_exclude_tac: thm -> tactic |
53916 | 30 |
val mk_sel_exhaust_tac: int -> thm -> thm list -> tactic |
54491 | 31 |
val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> |
32 |
thm list list list -> tactic |
|
49044 | 33 |
val mk_split_asm_tac: Proof.context -> thm -> tactic |
49137 | 34 |
val mk_unique_disc_def_tac: int -> thm -> tactic |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
35 |
end; |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
36 |
|
54006 | 37 |
structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS = |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
38 |
struct |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
39 |
|
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
40 |
open Ctr_Sugar_Util |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
41 |
|
49486 | 42 |
val meta_mp = @{thm meta_mp}; |
43 |
||
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
44 |
fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl, |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
45 |
tac, REPEAT_DETERM_N (n - k) o etac thin_rl]); |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
46 |
|
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
47 |
fun unfold_thms_tac _ [] = all_tac |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
48 |
| unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms); |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
49 |
|
49212 | 50 |
fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P}); |
49031 | 51 |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
52 |
fun mk_nchotomy_tac n exhaust = |
52325 | 53 |
HEADGOAL (rtac allI THEN' rtac exhaust THEN' |
52966 | 54 |
EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))); |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
55 |
|
49486 | 56 |
fun mk_unique_disc_def_tac m uexhaust = |
52325 | 57 |
HEADGOAL (EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl]); |
49137 | 58 |
|
49486 | 59 |
fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust = |
52325 | 60 |
HEADGOAL (EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans), |
49630 | 61 |
rtac @{thm iffI_np}, REPEAT_DETERM o etac exE, |
51798 | 62 |
hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, |
49486 | 63 |
rtac distinct, rtac uexhaust] @ |
49174
41790d616f63
by default, only generate one discriminator for a two-value datatype
blanchet
parents:
49168
diff
changeset
|
64 |
(([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac]) |
52325 | 65 |
|> k = 1 ? swap |> op @))); |
49116
3d520eec2746
allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents:
49075
diff
changeset
|
66 |
|
51798 | 67 |
fun mk_half_disc_exclude_tac ctxt m discD disc' = |
52325 | 68 |
HEADGOAL (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN' |
69 |
rtac disc'); |
|
49028 | 70 |
|
52325 | 71 |
fun mk_other_half_disc_exclude_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half); |
49028 | 72 |
|
53916 | 73 |
fun mk_disc_or_sel_exhaust_tac n exhaust destIs = |
52325 | 74 |
HEADGOAL (rtac exhaust THEN' |
53916 | 75 |
EVERY' (map2 (fn k => fn destI => dtac destI THEN' |
76 |
select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) destIs)); |
|
77 |
||
78 |
val mk_disc_exhaust_tac = mk_disc_or_sel_exhaust_tac; |
|
79 |
||
80 |
fun mk_sel_exhaust_tac n disc_exhaust collapses = |
|
53920
c6de7f20c845
made tactic more robust in case somebody specified a discriminator for a one-constructor type
blanchet
parents:
53917
diff
changeset
|
81 |
mk_disc_or_sel_exhaust_tac n disc_exhaust collapses ORELSE |
c6de7f20c845
made tactic more robust in case somebody specified a discriminator for a one-constructor type
blanchet
parents:
53917
diff
changeset
|
82 |
HEADGOAL (etac meta_mp THEN' resolve_tac collapses); |
49029 | 83 |
|
49484 | 84 |
fun mk_collapse_tac ctxt m discD sels = |
52325 | 85 |
HEADGOAL (dtac discD THEN' |
86 |
(if m = 0 then |
|
87 |
atac |
|
88 |
else |
|
89 |
REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN' |
|
90 |
SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)); |
|
49030 | 91 |
|
51742
b5ff7393642d
fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
blanchet
parents:
51717
diff
changeset
|
92 |
fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss |
b5ff7393642d
fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
blanchet
parents:
51717
diff
changeset
|
93 |
disc_excludesss' = |
49486 | 94 |
if ms = [0] then |
52325 | 95 |
HEADGOAL (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN' |
96 |
TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac]) |
|
49486 | 97 |
else |
51742
b5ff7393642d
fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
blanchet
parents:
51717
diff
changeset
|
98 |
let val ks = 1 upto n in |
52325 | 99 |
HEADGOAL (rtac udisc_exhaust THEN' |
54844 | 100 |
EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => fn uuncollapse => |
101 |
EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, rtac sym, rtac vdisc_exhaust, |
|
52325 | 102 |
EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse => |
103 |
EVERY' |
|
104 |
(if k' = k then |
|
105 |
[rtac (vuncollapse RS trans), TRY o atac] @ |
|
106 |
(if m = 0 then |
|
107 |
[rtac refl] |
|
108 |
else |
|
109 |
[if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac], |
|
110 |
REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE, |
|
111 |
asm_simp_tac (ss_only [] ctxt)]) |
|
112 |
else |
|
113 |
[dtac (the_single (if k = n then disc_excludes else disc_excludes')), |
|
114 |
etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}), |
|
115 |
atac, atac])) |
|
116 |
ks disc_excludess disc_excludess' uncollapses)]) |
|
117 |
ks ms disc_excludesss disc_excludesss' uncollapses)) |
|
49486 | 118 |
end; |
119 |
||
52967 | 120 |
fun mk_case_same_ctr_tac ctxt injects = |
121 |
REPEAT_DETERM o etac exE THEN' etac conjE THEN' |
|
122 |
(case injects of |
|
123 |
[] => atac |
|
124 |
| [inject] => dtac (inject RS iffD1) THEN' REPEAT_DETERM o etac conjE THEN' |
|
125 |
hyp_subst_tac ctxt THEN' rtac refl); |
|
126 |
||
127 |
fun mk_case_distinct_ctrs_tac ctxt distincts = |
|
128 |
REPEAT_DETERM o etac exE THEN' etac conjE THEN' full_simp_tac (ss_only distincts ctxt); |
|
129 |
||
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
130 |
fun mk_case_tac ctxt n k case_def injects distinctss = |
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
131 |
let |
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
132 |
val case_def' = mk_unabs_def (n + 1) (case_def RS meta_eq_to_obj_eq); |
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
133 |
val ks = 1 upto n; |
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
134 |
in |
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
135 |
HEADGOAL (rtac (case_def' RS trans) THEN' rtac @{thm the_equality} THEN' |
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
136 |
rtac (mk_disjIN n k) THEN' REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN' |
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
137 |
rtac refl THEN' |
52967 | 138 |
EVERY' (map2 (fn k' => fn distincts => |
139 |
(if k' < n then etac disjE else K all_tac) THEN' |
|
140 |
(if k' = k then mk_case_same_ctr_tac ctxt injects |
|
141 |
else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss)) |
|
142 |
end; |
|
143 |
||
54491 | 144 |
fun mk_case_cong_tac ctxt uexhaust cases = |
145 |
HEADGOAL (rtac uexhaust THEN' |
|
146 |
EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases)); |
|
147 |
||
148 |
fun mk_case_eq_if_tac ctxt n uexhaust cases discss' selss = |
|
52325 | 149 |
HEADGOAL (rtac uexhaust THEN' |
150 |
EVERY' (map3 (fn casex => fn if_discs => fn sels => |
|
151 |
EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), |
|
152 |
rtac casex]) |
|
153 |
cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)); |
|
49031 | 154 |
|
53917 | 155 |
fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss = |
52325 | 156 |
HEADGOAL (rtac uexhaust) THEN |
51798 | 157 |
ALLGOALS (fn k => (hyp_subst_tac ctxt THEN' |
53917 | 158 |
simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @ |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
159 |
flat (nth distinctsss (k - 1))) ctxt)) k) THEN |
51937 | 160 |
ALLGOALS (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt)); |
49032 | 161 |
|
49044 | 162 |
val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex}; |
163 |
||
164 |
fun mk_split_asm_tac ctxt split = |
|
52325 | 165 |
HEADGOAL (rtac (split RS trans)) THEN unfold_thms_tac ctxt split_asm_thms THEN |
166 |
HEADGOAL (rtac refl); |
|
49044 | 167 |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
168 |
end; |
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
169 |
|
54491 | 170 |
structure Ctr_Sugar_General_Tactics : CTR_SUGAR_GENERAL_TACTICS = Ctr_Sugar_Tactics; |