23150
|
1 |
(* Title: HOL/Tools/TFL/casesplit.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lucas Dixon, University of Edinburgh
|
|
4 |
|
|
5 |
A structure that defines a tactic to program case splits.
|
|
6 |
|
|
7 |
casesplit_free :
|
|
8 |
string * typ -> int -> thm -> thm Seq.seq
|
|
9 |
|
|
10 |
casesplit_name :
|
|
11 |
string -> int -> thm -> thm Seq.seq
|
|
12 |
|
|
13 |
These use the induction theorem associated with the recursive data
|
|
14 |
type to be split.
|
|
15 |
|
|
16 |
The structure includes a function to try and recursively split a
|
|
17 |
conjecture into a list sub-theorems:
|
|
18 |
|
|
19 |
splitto : thm list -> thm -> thm
|
|
20 |
*)
|
|
21 |
|
|
22 |
(* logic-specific *)
|
|
23 |
signature CASE_SPLIT_DATA =
|
|
24 |
sig
|
|
25 |
val dest_Trueprop : term -> term
|
|
26 |
val mk_Trueprop : term -> term
|
|
27 |
val atomize : thm list
|
|
28 |
val rulify : thm list
|
|
29 |
end;
|
|
30 |
|
|
31 |
structure CaseSplitData_HOL : CASE_SPLIT_DATA =
|
|
32 |
struct
|
|
33 |
val dest_Trueprop = HOLogic.dest_Trueprop;
|
|
34 |
val mk_Trueprop = HOLogic.mk_Trueprop;
|
|
35 |
|
|
36 |
val atomize = thms "induct_atomize";
|
|
37 |
val rulify = thms "induct_rulify";
|
|
38 |
val rulify_fallback = thms "induct_rulify_fallback";
|
|
39 |
|
|
40 |
end;
|
|
41 |
|
|
42 |
|
|
43 |
signature CASE_SPLIT =
|
|
44 |
sig
|
|
45 |
(* failure to find a free to split on *)
|
|
46 |
exception find_split_exp of string
|
|
47 |
|
|
48 |
(* getting a case split thm from the induction thm *)
|
|
49 |
val case_thm_of_ty : theory -> typ -> thm
|
|
50 |
val cases_thm_of_induct_thm : thm -> thm
|
|
51 |
|
|
52 |
(* case split tactics *)
|
|
53 |
val casesplit_free :
|
|
54 |
string * typ -> int -> thm -> thm Seq.seq
|
|
55 |
val casesplit_name : string -> int -> thm -> thm Seq.seq
|
|
56 |
|
|
57 |
(* finding a free var to split *)
|
|
58 |
val find_term_split :
|
|
59 |
term * term -> (string * typ) option
|
|
60 |
val find_thm_split :
|
|
61 |
thm -> int -> thm -> (string * typ) option
|
|
62 |
val find_thms_split :
|
|
63 |
thm list -> int -> thm -> (string * typ) option
|
|
64 |
|
|
65 |
(* try to recursively split conjectured thm to given list of thms *)
|
|
66 |
val splitto : thm list -> thm -> thm
|
|
67 |
|
|
68 |
(* for use with the recdef package *)
|
|
69 |
val derive_init_eqs :
|
|
70 |
theory ->
|
|
71 |
(thm * int) list -> term list -> (thm * int) list
|
|
72 |
end;
|
|
73 |
|
|
74 |
functor CaseSplitFUN(Data : CASE_SPLIT_DATA) =
|
|
75 |
struct
|
|
76 |
|
|
77 |
val rulify_goals = MetaSimplifier.rewrite_goals_rule Data.rulify;
|
|
78 |
val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize;
|
|
79 |
|
|
80 |
(* beta-eta contract the theorem *)
|
|
81 |
fun beta_eta_contract thm =
|
|
82 |
let
|
|
83 |
val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
|
|
84 |
val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
|
|
85 |
in thm3 end;
|
|
86 |
|
|
87 |
(* make a casethm from an induction thm *)
|
|
88 |
val cases_thm_of_induct_thm =
|
|
89 |
Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
|
|
90 |
|
|
91 |
(* get the case_thm (my version) from a type *)
|
|
92 |
fun case_thm_of_ty sgn ty =
|
|
93 |
let
|
|
94 |
val dtypestab = DatatypePackage.get_datatypes sgn;
|
|
95 |
val ty_str = case ty of
|
|
96 |
Type(ty_str, _) => ty_str
|
|
97 |
| TFree(s,_) => error ("Free type: " ^ s)
|
|
98 |
| TVar((s,i),_) => error ("Free variable: " ^ s)
|
|
99 |
val dt = case Symtab.lookup dtypestab ty_str
|
|
100 |
of SOME dt => dt
|
|
101 |
| NONE => error ("Not a Datatype: " ^ ty_str)
|
|
102 |
in
|
|
103 |
cases_thm_of_induct_thm (#induction dt)
|
|
104 |
end;
|
|
105 |
|
|
106 |
(*
|
|
107 |
val ty = (snd o hd o map Term.dest_Free o Term.term_frees) t;
|
|
108 |
*)
|
|
109 |
|
|
110 |
|
|
111 |
(* for use when there are no prems to the subgoal *)
|
|
112 |
(* does a case split on the given variable *)
|
|
113 |
fun mk_casesplit_goal_thm sgn (vstr,ty) gt =
|
|
114 |
let
|
|
115 |
val x = Free(vstr,ty)
|
|
116 |
val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
|
|
117 |
|
|
118 |
val ctermify = Thm.cterm_of sgn;
|
|
119 |
val ctypify = Thm.ctyp_of sgn;
|
|
120 |
val case_thm = case_thm_of_ty sgn ty;
|
|
121 |
|
|
122 |
val abs_ct = ctermify abst;
|
|
123 |
val free_ct = ctermify x;
|
|
124 |
|
|
125 |
val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm));
|
|
126 |
|
|
127 |
val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
|
|
128 |
val (Pv, Dv, type_insts) =
|
|
129 |
case (Thm.concl_of case_thm) of
|
|
130 |
(_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
|
|
131 |
(Pv, Dv,
|
|
132 |
Sign.typ_match sgn (Dty, ty) Vartab.empty)
|
|
133 |
| _ => error "not a valid case thm";
|
|
134 |
val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
|
|
135 |
(Vartab.dest type_insts);
|
|
136 |
val cPv = ctermify (Envir.subst_TVars type_insts Pv);
|
|
137 |
val cDv = ctermify (Envir.subst_TVars type_insts Dv);
|
|
138 |
in
|
|
139 |
(beta_eta_contract
|
|
140 |
(case_thm
|
|
141 |
|> Thm.instantiate (type_cinsts, [])
|
|
142 |
|> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])))
|
|
143 |
end;
|
|
144 |
|
|
145 |
|
|
146 |
(* for use when there are no prems to the subgoal *)
|
|
147 |
(* does a case split on the given variable (Free fv) *)
|
|
148 |
fun casesplit_free fv i th =
|
|
149 |
let
|
|
150 |
val (subgoalth, exp) = IsaND.fix_alls i th;
|
|
151 |
val subgoalth' = atomize_goals subgoalth;
|
|
152 |
val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
|
|
153 |
val sgn = Thm.theory_of_thm th;
|
|
154 |
|
|
155 |
val splitter_thm = mk_casesplit_goal_thm sgn fv gt;
|
|
156 |
val nsplits = Thm.nprems_of splitter_thm;
|
|
157 |
|
|
158 |
val split_goal_th = splitter_thm RS subgoalth';
|
|
159 |
val rulified_split_goal_th = rulify_goals split_goal_th;
|
|
160 |
in
|
|
161 |
IsaND.export_back exp rulified_split_goal_th
|
|
162 |
end;
|
|
163 |
|
|
164 |
|
|
165 |
(* for use when there are no prems to the subgoal *)
|
|
166 |
(* does a case split on the given variable *)
|
|
167 |
fun casesplit_name vstr i th =
|
|
168 |
let
|
|
169 |
val (subgoalth, exp) = IsaND.fix_alls i th;
|
|
170 |
val subgoalth' = atomize_goals subgoalth;
|
|
171 |
val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
|
|
172 |
|
|
173 |
val freets = Term.term_frees gt;
|
|
174 |
fun getter x =
|
|
175 |
let val (n,ty) = Term.dest_Free x in
|
|
176 |
(if vstr = n orelse vstr = Name.dest_skolem n
|
|
177 |
then SOME (n,ty) else NONE )
|
|
178 |
handle Fail _ => NONE (* dest_skolem *)
|
|
179 |
end;
|
|
180 |
val (n,ty) = case Library.get_first getter freets
|
|
181 |
of SOME (n, ty) => (n, ty)
|
|
182 |
| _ => error ("no such variable " ^ vstr);
|
|
183 |
val sgn = Thm.theory_of_thm th;
|
|
184 |
|
|
185 |
val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt;
|
|
186 |
val nsplits = Thm.nprems_of splitter_thm;
|
|
187 |
|
|
188 |
val split_goal_th = splitter_thm RS subgoalth';
|
|
189 |
|
|
190 |
val rulified_split_goal_th = rulify_goals split_goal_th;
|
|
191 |
in
|
|
192 |
IsaND.export_back exp rulified_split_goal_th
|
|
193 |
end;
|
|
194 |
|
|
195 |
|
|
196 |
(* small example:
|
|
197 |
Goal "P (x :: nat) & (C y --> Q (y :: nat))";
|
|
198 |
by (rtac (thm "conjI") 1);
|
|
199 |
val th = topthm();
|
|
200 |
val i = 2;
|
|
201 |
val vstr = "y";
|
|
202 |
|
|
203 |
by (casesplit_name "y" 2);
|
|
204 |
|
|
205 |
val th = topthm();
|
|
206 |
val i = 1;
|
|
207 |
val th' = casesplit_name "x" i th;
|
|
208 |
*)
|
|
209 |
|
|
210 |
|
|
211 |
(* the find_XXX_split functions are simply doing a lightwieght (I
|
|
212 |
think) term matching equivalent to find where to do the next split *)
|
|
213 |
|
|
214 |
(* assuming two twems are identical except for a free in one at a
|
|
215 |
subterm, or constant in another, ie assume that one term is a plit of
|
|
216 |
another, then gives back the free variable that has been split. *)
|
|
217 |
exception find_split_exp of string
|
|
218 |
fun find_term_split (Free v, _ $ _) = SOME v
|
|
219 |
| find_term_split (Free v, Const _) = SOME v
|
|
220 |
| find_term_split (Free v, Abs _) = SOME v (* do we really want this case? *)
|
|
221 |
| find_term_split (Free v, Var _) = NONE (* keep searching *)
|
|
222 |
| find_term_split (a $ b, a2 $ b2) =
|
|
223 |
(case find_term_split (a, a2) of
|
|
224 |
NONE => find_term_split (b,b2)
|
|
225 |
| vopt => vopt)
|
|
226 |
| find_term_split (Abs(_,ty,t1), Abs(_,ty2,t2)) =
|
|
227 |
find_term_split (t1, t2)
|
|
228 |
| find_term_split (Const (x,ty), Const(x2,ty2)) =
|
|
229 |
if x = x2 then NONE else (* keep searching *)
|
|
230 |
raise find_split_exp (* stop now *)
|
|
231 |
"Terms are not identical upto a free varaible! (Consts)"
|
|
232 |
| find_term_split (Bound i, Bound j) =
|
|
233 |
if i = j then NONE else (* keep searching *)
|
|
234 |
raise find_split_exp (* stop now *)
|
|
235 |
"Terms are not identical upto a free varaible! (Bound)"
|
|
236 |
| find_term_split (a, b) =
|
|
237 |
raise find_split_exp (* stop now *)
|
|
238 |
"Terms are not identical upto a free varaible! (Other)";
|
|
239 |
|
|
240 |
(* assume that "splitth" is a case split form of subgoal i of "genth",
|
|
241 |
then look for a free variable to split, breaking the subgoal closer to
|
|
242 |
splitth. *)
|
|
243 |
fun find_thm_split splitth i genth =
|
|
244 |
find_term_split (Logic.get_goal (Thm.prop_of genth) i,
|
|
245 |
Thm.concl_of splitth) handle find_split_exp _ => NONE;
|
|
246 |
|
|
247 |
(* as above but searches "splitths" for a theorem that suggest a case split *)
|
|
248 |
fun find_thms_split splitths i genth =
|
|
249 |
Library.get_first (fn sth => find_thm_split sth i genth) splitths;
|
|
250 |
|
|
251 |
|
|
252 |
(* split the subgoal i of "genth" until we get to a member of
|
|
253 |
splitths. Assumes that genth will be a general form of splitths, that
|
|
254 |
can be case-split, as needed. Otherwise fails. Note: We assume that
|
|
255 |
all of "splitths" are split to the same level, and thus it doesn't
|
|
256 |
matter which one we choose to look for the next split. Simply add
|
|
257 |
search on splitthms and split variable, to change this. *)
|
|
258 |
(* Note: possible efficiency measure: when a case theorem is no longer
|
|
259 |
useful, drop it? *)
|
|
260 |
(* Note: This should not be a separate tactic but integrated into the
|
|
261 |
case split done during recdef's case analysis, this would avoid us
|
|
262 |
having to (re)search for variables to split. *)
|
|
263 |
fun splitto splitths genth =
|
|
264 |
let
|
|
265 |
val _ = not (null splitths) orelse error "splitto: no given splitths";
|
|
266 |
val sgn = Thm.theory_of_thm genth;
|
|
267 |
|
|
268 |
(* check if we are a member of splitths - FIXME: quicker and
|
|
269 |
more flexible with discrim net. *)
|
|
270 |
fun solve_by_splitth th split =
|
|
271 |
Thm.biresolution false [(false,split)] 1 th;
|
|
272 |
|
|
273 |
fun split th =
|
|
274 |
(case find_thms_split splitths 1 th of
|
|
275 |
NONE =>
|
|
276 |
(writeln "th:";
|
|
277 |
Display.print_thm th; writeln "split ths:";
|
|
278 |
Display.print_thms splitths; writeln "\n--";
|
|
279 |
error "splitto: cannot find variable to split on")
|
|
280 |
| SOME v =>
|
|
281 |
let
|
|
282 |
val gt = Data.dest_Trueprop (List.nth(Thm.prems_of th, 0));
|
|
283 |
val split_thm = mk_casesplit_goal_thm sgn v gt;
|
|
284 |
val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm;
|
|
285 |
in
|
|
286 |
expf (map recsplitf subthms)
|
|
287 |
end)
|
|
288 |
|
|
289 |
and recsplitf th =
|
|
290 |
(* note: multiple unifiers! we only take the first element,
|
|
291 |
probably fine -- there is probably only one anyway. *)
|
|
292 |
(case Library.get_first (Seq.pull o solve_by_splitth th) splitths of
|
|
293 |
NONE => split th
|
|
294 |
| SOME (solved_th, more) => solved_th)
|
|
295 |
in
|
|
296 |
recsplitf genth
|
|
297 |
end;
|
|
298 |
|
|
299 |
|
|
300 |
(* Note: We dont do this if wf conditions fail to be solved, as each
|
|
301 |
case may have a different wf condition - we could group the conditions
|
|
302 |
togeather and say that they must be true to solve the general case,
|
|
303 |
but that would hide from the user which sub-case they were related
|
|
304 |
to. Probably this is not important, and it would work fine, but I
|
|
305 |
prefer leaving more fine grain control to the user. *)
|
|
306 |
|
|
307 |
(* derive eqs, assuming strict, ie the rules have no assumptions = all
|
|
308 |
the well-foundness conditions have been solved. *)
|
|
309 |
fun derive_init_eqs sgn rules eqs =
|
|
310 |
let
|
|
311 |
fun get_related_thms i =
|
|
312 |
List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE));
|
|
313 |
fun add_eq (i, e) xs =
|
|
314 |
(e, (get_related_thms i rules), i) :: xs
|
|
315 |
fun solve_eq (th, [], i) =
|
|
316 |
error "derive_init_eqs: missing rules"
|
|
317 |
| solve_eq (th, [a], i) = (a, i)
|
|
318 |
| solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th, i);
|
|
319 |
val eqths =
|
|
320 |
map (Thm.trivial o Thm.cterm_of sgn o Data.mk_Trueprop) eqs;
|
|
321 |
in
|
|
322 |
[]
|
|
323 |
|> fold_index add_eq eqths
|
|
324 |
|> map solve_eq
|
|
325 |
|> rev
|
|
326 |
end;
|
|
327 |
|
|
328 |
end;
|
|
329 |
|
|
330 |
|
|
331 |
structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL);
|