|
1 (* Title: Tools/induct.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 Proof by cases and induction. |
|
6 *) |
|
7 |
|
8 signature INDUCT_DATA = |
|
9 sig |
|
10 val cases_default: thm |
|
11 val atomize: thm list |
|
12 val rulify: thm list |
|
13 val rulify_fallback: thm list |
|
14 end; |
|
15 |
|
16 signature INDUCT = |
|
17 sig |
|
18 (*rule declarations*) |
|
19 val vars_of: term -> term list |
|
20 val dest_rules: Proof.context -> |
|
21 {type_cases: (string * thm) list, set_cases: (string * thm) list, |
|
22 type_induct: (string * thm) list, set_induct: (string * thm) list, |
|
23 type_coinduct: (string * thm) list, set_coinduct: (string * thm) list} |
|
24 val print_rules: Proof.context -> unit |
|
25 val lookup_casesT: Proof.context -> string -> thm option |
|
26 val lookup_casesS: Proof.context -> string -> thm option |
|
27 val lookup_inductT: Proof.context -> string -> thm option |
|
28 val lookup_inductS: Proof.context -> string -> thm option |
|
29 val lookup_coinductT: Proof.context -> string -> thm option |
|
30 val lookup_coinductS: Proof.context -> string -> thm option |
|
31 val find_casesT: Proof.context -> typ -> thm list |
|
32 val find_casesS: Proof.context -> term -> thm list |
|
33 val find_inductT: Proof.context -> typ -> thm list |
|
34 val find_inductS: Proof.context -> term -> thm list |
|
35 val find_coinductT: Proof.context -> typ -> thm list |
|
36 val find_coinductS: Proof.context -> term -> thm list |
|
37 val cases_type: string -> attribute |
|
38 val cases_set: string -> attribute |
|
39 val induct_type: string -> attribute |
|
40 val induct_set: string -> attribute |
|
41 val coinduct_type: string -> attribute |
|
42 val coinduct_set: string -> attribute |
|
43 val casesN: string |
|
44 val inductN: string |
|
45 val coinductN: string |
|
46 val typeN: string |
|
47 val setN: string |
|
48 (*proof methods*) |
|
49 val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic |
|
50 val add_defs: (string option * term) option list -> Proof.context -> |
|
51 (term option list * thm list) * Proof.context |
|
52 val atomize_term: theory -> term -> term |
|
53 val atomize_tac: int -> tactic |
|
54 val inner_atomize_tac: int -> tactic |
|
55 val rulified_term: thm -> theory * term |
|
56 val rulify_tac: int -> tactic |
|
57 val internalize: int -> thm -> thm |
|
58 val guess_instance: thm -> int -> thm -> thm Seq.seq |
|
59 val cases_tac: Proof.context -> bool -> term option list list -> thm option -> |
|
60 thm list -> int -> cases_tactic |
|
61 val induct_tac: Proof.context -> bool -> (string option * term) option list list -> |
|
62 (string * typ) list list -> term option list -> thm list option -> thm list -> int -> |
|
63 cases_tactic |
|
64 val coinduct_tac: Proof.context -> bool -> term option list -> term option list -> |
|
65 thm option -> thm list -> int -> cases_tactic |
|
66 val setup: theory -> theory |
|
67 end; |
|
68 |
|
69 functor InductFun(Data: INDUCT_DATA): INDUCT = |
|
70 struct |
|
71 |
|
72 |
|
73 (** misc utils **) |
|
74 |
|
75 (* encode_type -- for indexing purposes *) |
|
76 |
|
77 fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts) |
|
78 | encode_type (TFree (a, _)) = Free (a, dummyT) |
|
79 | encode_type (TVar (a, _)) = Var (a, dummyT); |
|
80 |
|
81 |
|
82 (* variables -- ordered left-to-right, preferring right *) |
|
83 |
|
84 fun vars_of tm = |
|
85 rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm [])); |
|
86 |
|
87 local |
|
88 |
|
89 val mk_var = encode_type o #2 o Term.dest_Var; |
|
90 |
|
91 fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty => |
|
92 raise THM ("No variables in conclusion of rule", 0, [thm]); |
|
93 |
|
94 in |
|
95 |
|
96 fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty => |
|
97 raise THM ("No variables in major premise of rule", 0, [thm]); |
|
98 |
|
99 val left_var_concl = concl_var hd; |
|
100 val right_var_concl = concl_var List.last; |
|
101 |
|
102 end; |
|
103 |
|
104 |
|
105 |
|
106 (** induct data **) |
|
107 |
|
108 (* rules *) |
|
109 |
|
110 type rules = (string * thm) NetRules.T; |
|
111 |
|
112 val init_rules = |
|
113 NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso |
|
114 Thm.eq_thm_prop (th1, th2)); |
|
115 |
|
116 fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs); |
|
117 |
|
118 fun pretty_rules ctxt kind rs = |
|
119 let val thms = map snd (NetRules.rules rs) |
|
120 in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end; |
|
121 |
|
122 |
|
123 (* context data *) |
|
124 |
|
125 structure Induct = GenericDataFun |
|
126 ( |
|
127 type T = (rules * rules) * (rules * rules) * (rules * rules); |
|
128 val empty = |
|
129 ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)), |
|
130 (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)), |
|
131 (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2))); |
|
132 val extend = I; |
|
133 fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)), |
|
134 ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) = |
|
135 ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)), |
|
136 (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)), |
|
137 (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2))); |
|
138 ); |
|
139 |
|
140 val get_local = Induct.get o Context.Proof; |
|
141 |
|
142 fun dest_rules ctxt = |
|
143 let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in |
|
144 {type_cases = NetRules.rules casesT, |
|
145 set_cases = NetRules.rules casesS, |
|
146 type_induct = NetRules.rules inductT, |
|
147 set_induct = NetRules.rules inductS, |
|
148 type_coinduct = NetRules.rules coinductT, |
|
149 set_coinduct = NetRules.rules coinductS} |
|
150 end; |
|
151 |
|
152 fun print_rules ctxt = |
|
153 let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in |
|
154 [pretty_rules ctxt "coinduct type:" coinductT, |
|
155 pretty_rules ctxt "coinduct set:" coinductS, |
|
156 pretty_rules ctxt "induct type:" inductT, |
|
157 pretty_rules ctxt "induct set:" inductS, |
|
158 pretty_rules ctxt "cases type:" casesT, |
|
159 pretty_rules ctxt "cases set:" casesS] |
|
160 |> Pretty.chunks |> Pretty.writeln |
|
161 end; |
|
162 |
|
163 val _ = OuterSyntax.add_parsers [ |
|
164 OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules" |
|
165 OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
|
166 Toplevel.keep (print_rules o Toplevel.context_of)))]; |
|
167 |
|
168 |
|
169 (* access rules *) |
|
170 |
|
171 val lookup_casesT = lookup_rule o #1 o #1 o get_local; |
|
172 val lookup_casesS = lookup_rule o #2 o #1 o get_local; |
|
173 val lookup_inductT = lookup_rule o #1 o #2 o get_local; |
|
174 val lookup_inductS = lookup_rule o #2 o #2 o get_local; |
|
175 val lookup_coinductT = lookup_rule o #1 o #3 o get_local; |
|
176 val lookup_coinductS = lookup_rule o #2 o #3 o get_local; |
|
177 |
|
178 |
|
179 fun find_rules which how ctxt x = |
|
180 map snd (NetRules.retrieve (which (get_local ctxt)) (how x)); |
|
181 |
|
182 val find_casesT = find_rules (#1 o #1) encode_type; |
|
183 val find_casesS = find_rules (#2 o #1) I; |
|
184 val find_inductT = find_rules (#1 o #2) encode_type; |
|
185 val find_inductS = find_rules (#2 o #2) I; |
|
186 val find_coinductT = find_rules (#1 o #3) encode_type; |
|
187 val find_coinductS = find_rules (#2 o #3) I; |
|
188 |
|
189 |
|
190 |
|
191 (** attributes **) |
|
192 |
|
193 local |
|
194 |
|
195 fun mk_att f g name arg = |
|
196 let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end; |
|
197 |
|
198 fun map1 f (x, y, z) = (f x, y, z); |
|
199 fun map2 f (x, y, z) = (x, f y, z); |
|
200 fun map3 f (x, y, z) = (x, y, f z); |
|
201 |
|
202 fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x; |
|
203 fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x; |
|
204 fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x; |
|
205 fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x; |
|
206 fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x; |
|
207 fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x; |
|
208 |
|
209 fun consumes0 x = RuleCases.consumes_default 0 x; |
|
210 fun consumes1 x = RuleCases.consumes_default 1 x; |
|
211 |
|
212 in |
|
213 |
|
214 val cases_type = mk_att add_casesT consumes0; |
|
215 val cases_set = mk_att add_casesS consumes1; |
|
216 val induct_type = mk_att add_inductT consumes0; |
|
217 val induct_set = mk_att add_inductS consumes1; |
|
218 val coinduct_type = mk_att add_coinductT consumes0; |
|
219 val coinduct_set = mk_att add_coinductS consumes1; |
|
220 |
|
221 end; |
|
222 |
|
223 |
|
224 |
|
225 (** attribute syntax **) |
|
226 |
|
227 val casesN = "cases"; |
|
228 val inductN = "induct"; |
|
229 val coinductN = "coinduct"; |
|
230 |
|
231 val typeN = "type"; |
|
232 val setN = "set"; |
|
233 |
|
234 local |
|
235 |
|
236 fun spec k arg = |
|
237 Scan.lift (Args.$$$ k -- Args.colon) |-- arg || |
|
238 Scan.lift (Args.$$$ k) >> K ""; |
|
239 |
|
240 fun attrib add_type add_set = |
|
241 Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set); |
|
242 |
|
243 val cases_att = attrib cases_type cases_set; |
|
244 val induct_att = attrib induct_type induct_set; |
|
245 val coinduct_att = attrib coinduct_type coinduct_set; |
|
246 |
|
247 in |
|
248 |
|
249 val attrib_setup = Attrib.add_attributes |
|
250 [(casesN, cases_att, "declaration of cases rule for type or set"), |
|
251 (inductN, induct_att, "declaration of induction rule for type or set"), |
|
252 (coinductN, coinduct_att, "declaration of coinduction rule for type or set")]; |
|
253 |
|
254 end; |
|
255 |
|
256 |
|
257 |
|
258 (** method utils **) |
|
259 |
|
260 (* alignment *) |
|
261 |
|
262 fun align_left msg xs ys = |
|
263 let val m = length xs and n = length ys |
|
264 in if m < n then error msg else (Library.take (n, xs) ~~ ys) end; |
|
265 |
|
266 fun align_right msg xs ys = |
|
267 let val m = length xs and n = length ys |
|
268 in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end; |
|
269 |
|
270 |
|
271 (* prep_inst *) |
|
272 |
|
273 fun prep_inst thy align tune (tm, ts) = |
|
274 let |
|
275 val cert = Thm.cterm_of thy; |
|
276 fun prep_var (x, SOME t) = |
|
277 let |
|
278 val cx = cert x; |
|
279 val {T = xT, thy, ...} = Thm.rep_cterm cx; |
|
280 val ct = cert (tune t); |
|
281 in |
|
282 if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct) |
|
283 else error (Pretty.string_of (Pretty.block |
|
284 [Pretty.str "Ill-typed instantiation:", Pretty.fbrk, |
|
285 Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1, |
|
286 Display.pretty_ctyp (#T (Thm.crep_cterm ct))])) |
|
287 end |
|
288 | prep_var (_, NONE) = NONE; |
|
289 val xs = vars_of tm; |
|
290 in |
|
291 align "Rule has fewer variables than instantiations given" xs ts |
|
292 |> map_filter prep_var |
|
293 end; |
|
294 |
|
295 |
|
296 (* trace_rules *) |
|
297 |
|
298 fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule") |
|
299 | trace_rules ctxt _ rules = Method.trace ctxt rules; |
|
300 |
|
301 |
|
302 (* make_cases *) |
|
303 |
|
304 fun make_cases is_open rule = |
|
305 RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule); |
|
306 |
|
307 fun warn_open true = legacy_feature "open rule cases in proof method" |
|
308 | warn_open false = (); |
|
309 |
|
310 |
|
311 |
|
312 (** cases method **) |
|
313 |
|
314 (* |
|
315 rule selection scheme: |
|
316 cases - default case split |
|
317 `x:A` cases ... - set cases |
|
318 cases t - type cases |
|
319 ... cases ... r - explicit rule |
|
320 *) |
|
321 |
|
322 local |
|
323 |
|
324 fun get_casesT ctxt ((SOME t :: _) :: _) = find_casesT ctxt (Term.fastype_of t) |
|
325 | get_casesT _ _ = []; |
|
326 |
|
327 fun get_casesS ctxt (fact :: _) = find_casesS ctxt (Thm.concl_of fact) |
|
328 | get_casesS _ _ = []; |
|
329 |
|
330 in |
|
331 |
|
332 fun cases_tac ctxt is_open insts opt_rule facts = |
|
333 let |
|
334 val _ = warn_open is_open; |
|
335 val thy = ProofContext.theory_of ctxt; |
|
336 val cert = Thm.cterm_of thy; |
|
337 |
|
338 fun inst_rule r = |
|
339 if null insts then `RuleCases.get r |
|
340 else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts |
|
341 |> maps (prep_inst thy align_left I) |
|
342 |> Drule.cterm_instantiate) r |> pair (RuleCases.get r); |
|
343 |
|
344 val ruleq = |
|
345 (case opt_rule of |
|
346 SOME r => Seq.single (inst_rule r) |
|
347 | NONE => |
|
348 (get_casesS ctxt facts @ get_casesT ctxt insts @ [Data.cases_default]) |
|
349 |> tap (trace_rules ctxt casesN) |
|
350 |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); |
|
351 in |
|
352 fn i => fn st => |
|
353 ruleq |
|
354 |> Seq.maps (RuleCases.consume [] facts) |
|
355 |> Seq.maps (fn ((cases, (_, more_facts)), rule) => |
|
356 CASES (make_cases is_open rule cases) |
|
357 (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st) |
|
358 end; |
|
359 |
|
360 end; |
|
361 |
|
362 |
|
363 |
|
364 (** induct method **) |
|
365 |
|
366 val conjunction_congs = [@{thm Pure.all_conjunction}, @{thm imp_conjunction}]; |
|
367 |
|
368 |
|
369 (* atomize *) |
|
370 |
|
371 fun atomize_term thy = |
|
372 MetaSimplifier.rewrite_term thy Data.atomize [] |
|
373 #> ObjectLogic.drop_judgment thy; |
|
374 |
|
375 val atomize_cterm = MetaSimplifier.rewrite true Data.atomize; |
|
376 |
|
377 val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize; |
|
378 |
|
379 val inner_atomize_tac = |
|
380 Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac; |
|
381 |
|
382 |
|
383 (* rulify *) |
|
384 |
|
385 fun rulify_term thy = |
|
386 MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #> |
|
387 MetaSimplifier.rewrite_term thy Data.rulify_fallback []; |
|
388 |
|
389 fun rulified_term thm = |
|
390 let |
|
391 val thy = Thm.theory_of_thm thm; |
|
392 val rulify = rulify_term thy; |
|
393 val (As, B) = Logic.strip_horn (Thm.prop_of thm); |
|
394 in (thy, Logic.list_implies (map rulify As, rulify B)) end; |
|
395 |
|
396 val rulify_tac = |
|
397 Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN' |
|
398 Simplifier.rewrite_goal_tac Data.rulify_fallback THEN' |
|
399 Goal.conjunction_tac THEN_ALL_NEW |
|
400 (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac); |
|
401 |
|
402 |
|
403 (* prepare rule *) |
|
404 |
|
405 fun rule_instance thy inst rule = |
|
406 Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule; |
|
407 |
|
408 fun internalize k th = |
|
409 th |> Thm.permute_prems 0 k |
|
410 |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm); |
|
411 |
|
412 |
|
413 (* guess rule instantiation -- cannot handle pending goal parameters *) |
|
414 |
|
415 local |
|
416 |
|
417 fun dest_env thy (env as Envir.Envir {iTs, ...}) = |
|
418 let |
|
419 val cert = Thm.cterm_of thy; |
|
420 val certT = Thm.ctyp_of thy; |
|
421 val pairs = Envir.alist_of env; |
|
422 val ts = map (cert o Envir.norm_term env o #2 o #2) pairs; |
|
423 val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts); |
|
424 in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end; |
|
425 |
|
426 in |
|
427 |
|
428 fun guess_instance rule i st = |
|
429 let |
|
430 val {thy, maxidx, ...} = Thm.rep_thm st; |
|
431 val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) |
|
432 val params = rev (rename_wrt_term goal (Logic.strip_params goal)); |
|
433 in |
|
434 if not (null params) then |
|
435 (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ |
|
436 commas_quote (map (Sign.string_of_term thy o Syntax.mark_boundT) params)); |
|
437 Seq.single rule) |
|
438 else |
|
439 let |
|
440 val rule' = Thm.incr_indexes (maxidx + 1) rule; |
|
441 val concl = Logic.strip_assums_concl goal; |
|
442 in |
|
443 Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] |
|
444 (Envir.empty (#maxidx (Thm.rep_thm rule'))) |
|
445 |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule') |
|
446 end |
|
447 end handle Subscript => Seq.empty; |
|
448 |
|
449 end; |
|
450 |
|
451 |
|
452 (* special renaming of rule parameters *) |
|
453 |
|
454 fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] = |
|
455 let |
|
456 val x = ProofContext.revert_skolem ctxt z; |
|
457 fun index i [] = [] |
|
458 | index i (y :: ys) = |
|
459 if x = y then x ^ string_of_int i :: index (i + 1) ys |
|
460 else y :: index i ys; |
|
461 fun rename_params [] = [] |
|
462 | rename_params ((y, Type (U, _)) :: ys) = |
|
463 (if U = T then x else y) :: rename_params ys |
|
464 | rename_params ((y, _) :: ys) = y :: rename_params ys; |
|
465 fun rename_asm A = |
|
466 let |
|
467 val xs = rename_params (Logic.strip_params A); |
|
468 val xs' = |
|
469 (case List.filter (equal x) xs of |
|
470 [] => xs | [_] => xs | _ => index 1 xs); |
|
471 in Logic.list_rename_params (xs', A) end; |
|
472 fun rename_prop p = |
|
473 let val (As, C) = Logic.strip_horn p |
|
474 in Logic.list_implies (map rename_asm As, C) end; |
|
475 val cp' = cterm_fun rename_prop (Thm.cprop_of thm); |
|
476 val thm' = Thm.equal_elim (Thm.reflexive cp') thm; |
|
477 in [RuleCases.save thm thm'] end |
|
478 | special_rename_params _ _ ths = ths; |
|
479 |
|
480 |
|
481 (* fix_tac *) |
|
482 |
|
483 local |
|
484 |
|
485 fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B) |
|
486 | goal_prefix 0 _ = Term.dummy_pattern propT |
|
487 | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B |
|
488 | goal_prefix _ _ = Term.dummy_pattern propT; |
|
489 |
|
490 fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1 |
|
491 | goal_params 0 _ = 0 |
|
492 | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B |
|
493 | goal_params _ _ = 0; |
|
494 |
|
495 fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) => |
|
496 let |
|
497 val thy = ProofContext.theory_of ctxt; |
|
498 val cert = Thm.cterm_of thy; |
|
499 val certT = Thm.ctyp_of thy; |
|
500 |
|
501 val v = Free (x, T); |
|
502 fun spec_rule prfx (xs, body) = |
|
503 @{thm Pure.meta_spec} |
|
504 |> Thm.rename_params_rule ([ProofContext.revert_skolem ctxt x], 1) |
|
505 |> Thm.lift_rule (cert prfx) |
|
506 |> `(Thm.prop_of #> Logic.strip_assums_concl) |
|
507 |-> (fn pred $ arg => |
|
508 Drule.cterm_instantiate |
|
509 [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))), |
|
510 (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]); |
|
511 |
|
512 fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B |
|
513 | goal_concl 0 xs B = |
|
514 if not (Term.exists_subterm (fn t => t aconv v) B) then NONE |
|
515 else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B)) |
|
516 | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B |
|
517 | goal_concl _ _ _ = NONE; |
|
518 in |
|
519 (case goal_concl n [] goal of |
|
520 SOME concl => |
|
521 (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i |
|
522 | NONE => all_tac) |
|
523 end); |
|
524 |
|
525 fun miniscope_tac p = |
|
526 CONVERSION (Conv.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq])); |
|
527 |
|
528 in |
|
529 |
|
530 fun fix_tac _ _ [] = K all_tac |
|
531 | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) => |
|
532 (EVERY' (map (meta_spec_tac ctxt n) xs) THEN' |
|
533 (miniscope_tac (goal_params n goal))) i); |
|
534 |
|
535 end; |
|
536 |
|
537 |
|
538 (* add_defs *) |
|
539 |
|
540 fun add_defs def_insts = |
|
541 let |
|
542 fun add (SOME (SOME x, t)) ctxt = |
|
543 let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt |
|
544 in ((SOME lhs, [th]), ctxt') end |
|
545 | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt) |
|
546 | add NONE ctxt = ((NONE, []), ctxt); |
|
547 in fold_map add def_insts #> apfst (split_list #> apsnd flat) end; |
|
548 |
|
549 |
|
550 (* induct_tac *) |
|
551 |
|
552 (* |
|
553 rule selection scheme: |
|
554 `x:A` induct ... - set induction |
|
555 induct x - type induction |
|
556 ... induct ... r - explicit rule |
|
557 *) |
|
558 |
|
559 local |
|
560 |
|
561 fun get_inductT ctxt insts = |
|
562 fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts) |
|
563 |> map (find_inductT ctxt o Term.fastype_of)) [[]] |
|
564 |> filter_out (forall PureThy.is_internal); |
|
565 |
|
566 fun get_inductS ctxt (fact :: _) = map single (find_inductS ctxt (Thm.concl_of fact)) |
|
567 | get_inductS _ _ = []; |
|
568 |
|
569 in |
|
570 |
|
571 fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts = |
|
572 let |
|
573 val _ = warn_open is_open; |
|
574 val thy = ProofContext.theory_of ctxt; |
|
575 val cert = Thm.cterm_of thy; |
|
576 |
|
577 val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; |
|
578 val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs; |
|
579 |
|
580 fun inst_rule (concls, r) = |
|
581 (if null insts then `RuleCases.get r |
|
582 else (align_left "Rule has fewer conclusions than arguments given" |
|
583 (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts |
|
584 |> maps (prep_inst thy align_right (atomize_term thy)) |
|
585 |> Drule.cterm_instantiate) r |> pair (RuleCases.get r)) |
|
586 |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th)); |
|
587 |
|
588 val ruleq = |
|
589 (case opt_rule of |
|
590 SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs)) |
|
591 | NONE => |
|
592 (get_inductS ctxt facts @ |
|
593 map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts)) |
|
594 |> map_filter (RuleCases.mutual_rule ctxt) |
|
595 |> tap (trace_rules ctxt inductN o map #2) |
|
596 |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); |
|
597 |
|
598 fun rule_cases rule = |
|
599 RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule); |
|
600 in |
|
601 (fn i => fn st => |
|
602 ruleq |
|
603 |> Seq.maps (RuleCases.consume (flat defs) facts) |
|
604 |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => |
|
605 (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => |
|
606 (CONJUNCTS (ALLGOALS |
|
607 (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1)) |
|
608 THEN' fix_tac defs_ctxt |
|
609 (nth concls (j - 1) + more_consumes) |
|
610 (nth_list arbitrary (j - 1)))) |
|
611 THEN' inner_atomize_tac) j)) |
|
612 THEN' atomize_tac) i st |> Seq.maps (fn st' => |
|
613 guess_instance (internalize more_consumes rule) i st' |
|
614 |> Seq.map (rule_instance thy taking) |
|
615 |> Seq.maps (fn rule' => |
|
616 CASES (rule_cases rule' cases) |
|
617 (Tactic.rtac rule' i THEN |
|
618 PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) |
|
619 THEN_ALL_NEW_CASES rulify_tac |
|
620 end; |
|
621 |
|
622 end; |
|
623 |
|
624 |
|
625 |
|
626 (** coinduct method **) |
|
627 |
|
628 (* |
|
629 rule selection scheme: |
|
630 goal "x:A" coinduct ... - set coinduction |
|
631 coinduct x - type coinduction |
|
632 coinduct ... r - explicit rule |
|
633 *) |
|
634 |
|
635 local |
|
636 |
|
637 fun get_coinductT ctxt (SOME t :: _) = find_coinductT ctxt (Term.fastype_of t) |
|
638 | get_coinductT _ _ = []; |
|
639 |
|
640 fun get_coinductS ctxt goal = find_coinductS ctxt (Logic.strip_assums_concl goal); |
|
641 |
|
642 in |
|
643 |
|
644 fun coinduct_tac ctxt is_open inst taking opt_rule facts = |
|
645 let |
|
646 val _ = warn_open is_open; |
|
647 val thy = ProofContext.theory_of ctxt; |
|
648 val cert = Thm.cterm_of thy; |
|
649 |
|
650 fun inst_rule r = |
|
651 if null inst then `RuleCases.get r |
|
652 else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r |
|
653 |> pair (RuleCases.get r); |
|
654 |
|
655 fun ruleq goal = |
|
656 (case opt_rule of |
|
657 SOME r => Seq.single (inst_rule r) |
|
658 | NONE => |
|
659 (get_coinductS ctxt goal @ get_coinductT ctxt inst) |
|
660 |> tap (trace_rules ctxt coinductN) |
|
661 |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); |
|
662 in |
|
663 SUBGOAL_CASES (fn (goal, i) => fn st => |
|
664 ruleq goal |
|
665 |> Seq.maps (RuleCases.consume [] facts) |
|
666 |> Seq.maps (fn ((cases, (_, more_facts)), rule) => |
|
667 guess_instance rule i st |
|
668 |> Seq.map (rule_instance thy taking) |
|
669 |> Seq.maps (fn rule' => |
|
670 CASES (make_cases is_open rule' cases) |
|
671 (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st))) |
|
672 end; |
|
673 |
|
674 end; |
|
675 |
|
676 |
|
677 |
|
678 (** concrete syntax **) |
|
679 |
|
680 val openN = "open"; |
|
681 val arbitraryN = "arbitrary"; |
|
682 val takingN = "taking"; |
|
683 val ruleN = "rule"; |
|
684 |
|
685 local |
|
686 |
|
687 fun single_rule [rule] = rule |
|
688 | single_rule _ = error "Single rule expected"; |
|
689 |
|
690 fun named_rule k arg get = |
|
691 Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|-- |
|
692 (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name => |
|
693 (case get (Context.proof_of context) name of SOME x => x |
|
694 | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))); |
|
695 |
|
696 fun rule get_type get_set = |
|
697 named_rule typeN Args.tyname get_type || |
|
698 named_rule setN Args.const get_set || |
|
699 Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms; |
|
700 |
|
701 val cases_rule = rule lookup_casesT lookup_casesS >> single_rule; |
|
702 val induct_rule = rule lookup_inductT lookup_inductS; |
|
703 val coinduct_rule = rule lookup_coinductT lookup_coinductS >> single_rule; |
|
704 |
|
705 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME; |
|
706 |
|
707 val def_inst = |
|
708 ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME) |
|
709 -- Args.term) >> SOME || |
|
710 inst >> Option.map (pair NONE); |
|
711 |
|
712 val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) => |
|
713 error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t)); |
|
714 |
|
715 fun unless_more_args scan = Scan.unless (Scan.lift |
|
716 ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN || |
|
717 Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan; |
|
718 |
|
719 val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |-- |
|
720 Args.and_list1 (Scan.repeat (unless_more_args free))) []; |
|
721 |
|
722 val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |-- |
|
723 Scan.repeat1 (unless_more_args inst)) []; |
|
724 |
|
725 in |
|
726 |
|
727 fun cases_meth src = |
|
728 Method.syntax (Args.mode openN -- |
|
729 (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src |
|
730 #> (fn ((is_open, (insts, opt_rule)), ctxt) => |
|
731 Method.METHOD_CASES (fn facts => |
|
732 Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts)))); |
|
733 |
|
734 fun induct_meth src = |
|
735 Method.syntax (Args.mode openN -- |
|
736 (Args.and_list (Scan.repeat (unless_more_args def_inst)) -- |
|
737 (arbitrary -- taking -- Scan.option induct_rule))) src |
|
738 #> (fn ((is_open, (insts, ((arbitrary, taking), opt_rule))), ctxt) => |
|
739 Method.RAW_METHOD_CASES (fn facts => |
|
740 Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts)))); |
|
741 |
|
742 fun coinduct_meth src = |
|
743 Method.syntax (Args.mode openN -- |
|
744 (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src |
|
745 #> (fn ((is_open, ((insts, taking), opt_rule)), ctxt) => |
|
746 Method.RAW_METHOD_CASES (fn facts => |
|
747 Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts)))); |
|
748 |
|
749 end; |
|
750 |
|
751 |
|
752 |
|
753 (** theory setup **) |
|
754 |
|
755 val setup = |
|
756 attrib_setup #> |
|
757 Method.add_methods |
|
758 [(casesN, cases_meth, "case analysis on types or sets"), |
|
759 (inductN, induct_meth, "induction on types or sets"), |
|
760 (coinductN, coinduct_meth, "coinduction on types or sets")]; |
|
761 |
|
762 end; |