18 end; |
18 end; |
19 |
19 |
20 signature INDUCT_METHOD = |
20 signature INDUCT_METHOD = |
21 sig |
21 sig |
22 val cases_tac: Proof.context -> bool -> term option list list -> thm option -> |
22 val cases_tac: Proof.context -> bool -> term option list list -> thm option -> |
23 thm list -> int -> RuleCases.tactic |
23 thm list -> int -> cases_tactic |
24 val fix_tac: (string * typ) list -> int -> tactic |
24 val fix_tac: (string * typ) list -> int -> tactic |
25 val induct_tac: Proof.context -> bool -> (string option * term) option list list -> |
25 val induct_tac: Proof.context -> bool -> (string option * term) option list list -> |
26 (string * typ) list list -> thm option -> thm list -> int -> RuleCases.tactic |
26 (string * typ) list list -> thm option -> thm list -> int -> cases_tactic |
27 val coinduct_tac: Proof.context -> bool -> term option list -> thm option -> |
27 val coinduct_tac: Proof.context -> bool -> term option list -> thm option -> |
28 thm list -> int -> RuleCases.tactic |
28 thm list -> int -> cases_tactic |
29 val setup: (theory -> theory) list |
29 val setup: (theory -> theory) list |
30 end; |
30 end; |
31 |
31 |
32 functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD = |
32 functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD = |
33 struct |
33 struct |
103 local |
102 local |
104 |
103 |
105 fun find_casesT ctxt ((SOME t :: _) :: _) = InductAttrib.find_casesT ctxt (Term.fastype_of t) |
104 fun find_casesT ctxt ((SOME t :: _) :: _) = InductAttrib.find_casesT ctxt (Term.fastype_of t) |
106 | find_casesT _ _ = []; |
105 | find_casesT _ _ = []; |
107 |
106 |
108 fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt fact |
107 fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt (Thm.concl_of fact) |
109 | find_casesS _ _ = []; |
108 | find_casesS _ _ = []; |
110 |
109 |
111 in |
110 in |
112 |
111 |
113 fun cases_tac ctxt is_open insts opt_rule facts = |
112 fun cases_tac ctxt is_open insts opt_rule facts = |
114 let |
113 let |
|
114 val _ = warn_open is_open; |
115 val thy = ProofContext.theory_of ctxt; |
115 val thy = ProofContext.theory_of ctxt; |
116 val cert = Thm.cterm_of thy; |
116 val cert = Thm.cterm_of thy; |
117 |
117 |
118 fun inst_rule r = |
118 fun inst_rule r = |
119 if null insts then RuleCases.add r |
119 if null insts then `RuleCases.get r |
120 else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts |
120 else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts |
121 |> (List.concat o map (prep_inst thy align_left I)) |
121 |> (List.concat o map (prep_inst thy align_left I)) |
122 |> Drule.cterm_instantiate) r |> rpair (RuleCases.get r); |
122 |> Drule.cterm_instantiate) r |> pair (RuleCases.get r); |
123 |
123 |
124 val ruleq = |
124 val ruleq = |
125 (case opt_rule of |
125 (case opt_rule of |
126 SOME r => Seq.single (inst_rule r) |
126 SOME r => Seq.single (inst_rule r) |
127 | NONE => |
127 | NONE => |
128 (find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default]) |
128 (find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default]) |
129 |> tap (trace_rules ctxt InductAttrib.casesN) |
129 |> tap (trace_rules ctxt InductAttrib.casesN) |
130 |> Seq.of_list |> Seq.maps (Seq.try inst_rule)) |
130 |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); |
131 |> Seq.maps (fn (th, (cases, n)) => |
|
132 Method.multi_resolves (Library.take (n, facts)) [th] |
|
133 |> Seq.map (apsnd (rpair (Library.drop (n, facts))) o rpair cases)); |
|
134 in |
131 in |
135 fn i => fn st => |
132 fn i => fn st => |
136 ruleq |> Seq.maps (fn (rule, (cases, more_facts)) => |
133 ruleq |
137 (Method.insert_tac more_facts THEN' Tactic.rtac rule) i st |
134 |> Seq.maps (RuleCases.consume facts) |
138 |> Seq.map (rpair (make_cases is_open rule cases))) |
135 |> Seq.maps (fn ((cases, (_, more_facts)), rule) => |
|
136 CASES (make_cases is_open rule cases) |
|
137 (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st) |
139 end; |
138 end; |
140 |
139 |
141 val cases_meth = Method.METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo |
140 val cases_meth = Method.METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo |
142 (fn (ctxt, (is_open, (insts, opt_rule))) => cases_tac ctxt is_open insts opt_rule)); |
141 (fn (ctxt, (is_open, (insts, opt_rule))) => cases_tac ctxt is_open insts opt_rule)); |
143 |
142 |
346 fun find_inductT ctxt insts = |
345 fun find_inductT ctxt insts = |
347 fold_rev multiply (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts) |
346 fold_rev multiply (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts) |
348 |> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]] |
347 |> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]] |
349 |> map join_rules |> List.concat; |
348 |> map join_rules |> List.concat; |
350 |
349 |
351 fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact |
350 fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt (Thm.concl_of fact) |
352 | find_inductS _ _ = []; |
351 | find_inductS _ _ = []; |
353 |
352 |
354 in |
353 in |
355 |
354 |
356 fun induct_tac ctxt is_open def_insts fixes opt_rule facts = |
355 fun induct_tac ctxt is_open def_insts fixes opt_rule facts = |
357 let |
356 let |
|
357 val _ = warn_open is_open; |
358 val thy = ProofContext.theory_of ctxt; |
358 val thy = ProofContext.theory_of ctxt; |
359 val cert = Thm.cterm_of thy; |
359 val cert = Thm.cterm_of thy; |
360 |
360 |
361 val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; |
361 val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; |
362 |
362 |
363 val inst_rule = apfst (fn r => |
363 val inst_rule = apsnd (fn r => |
364 if null insts then r |
364 if null insts then r |
365 else (align_right "Rule has fewer conclusions than arguments given" |
365 else (align_right "Rule has fewer conclusions than arguments given" |
366 (Data.dest_concls (Thm.concl_of r)) insts |
366 (Data.dest_concls (Thm.concl_of r)) insts |
367 |> (List.concat o map (prep_inst thy align_right (atomize_term thy))) |
367 |> (List.concat o map (prep_inst thy align_right (atomize_term thy))) |
368 |> Drule.cterm_instantiate) r); |
368 |> Drule.cterm_instantiate) r); |
372 SOME r => r |> rule_versions |> Seq.map inst_rule |
372 SOME r => r |> rule_versions |> Seq.map inst_rule |
373 | NONE => |
373 | NONE => |
374 (find_inductS ctxt facts @ |
374 (find_inductS ctxt facts @ |
375 map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts)) |
375 map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts)) |
376 |> tap (trace_rules ctxt InductAttrib.inductN) |
376 |> tap (trace_rules ctxt InductAttrib.inductN) |
377 |> Seq.of_list |> Seq.maps rule_versions |> Seq.maps (Seq.try inst_rule)) |
377 |> Seq.of_list |> Seq.maps rule_versions |> Seq.maps (Seq.try inst_rule)); |
378 |> Seq.maps (fn (th, (cases, n)) => |
378 |
379 Method.multi_resolves (Library.take (n, facts)) [th] |
379 fun rule_cases rule = RuleCases.make is_open (SOME (Thm.prop_of rule)) (rulified_term rule); |
380 |> Seq.map (rpair (cases, n - length facts, Library.drop (n, facts)))); |
|
381 |
|
382 fun rule_cases rule = |
|
383 RuleCases.make (tap warn_open is_open) (SOME (Thm.prop_of rule)) (rulified_term rule); |
|
384 in |
380 in |
385 (fn i => fn st => |
381 (fn i => fn st => |
386 ruleq |> Seq.maps (fn (rule, (cases, k, more_facts)) => |
382 ruleq |
|
383 |> Seq.maps (RuleCases.consume facts) |
|
384 |> Seq.maps (fn ((cases, (k, more_facts)), rule) => |
387 (CONJUNCTS (ALLGOALS (fn j => |
385 (CONJUNCTS (ALLGOALS (fn j => |
388 Method.insert_tac (more_facts @ nth_list defs (j - 1)) j |
386 Method.insert_tac (more_facts @ nth_list defs (j - 1)) j |
389 THEN fix_tac (nth_list fixes (j - 1)) j)) |
387 THEN fix_tac (nth_list fixes (j - 1)) j)) |
390 THEN' atomize_tac) i st |> Seq.maps (fn st' => |
388 THEN' atomize_tac) i st |> Seq.maps (fn st' => |
391 divinate_inst (internalize k rule) i st' |> Seq.maps (fn rule' => |
389 divinate_inst (internalize k rule) i st' |> Seq.maps (fn rule' => |
392 Tactic.rtac rule' i st' |
390 CASES (rule_cases rule' cases) |
393 |> Seq.maps (ProofContext.exports defs_ctxt ctxt) |
391 (Tactic.rtac rule' i THEN |
394 |> Seq.map (rpair (rule_cases rule' cases)))))) |
392 PRIMSEQ (ProofContext.exports defs_ctxt ctxt)) st')))) |
395 THEN_ALL_NEW_CASES rulify_tac |
393 THEN_ALL_NEW_CASES rulify_tac |
396 end; |
394 end; |
397 |
395 |
398 val induct_meth = Method.RAW_METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo |
396 val induct_meth = Method.RAW_METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo |
399 (fn (ctxt, (is_open, (insts, (fixes, opt_rule)))) => |
397 (fn (ctxt, (is_open, (insts, (fixes, opt_rule)))) => |
405 |
403 |
406 (** coinduct method **) |
404 (** coinduct method **) |
407 |
405 |
408 (* |
406 (* |
409 rule selection scheme: |
407 rule selection scheme: |
410 `x:A` coinduct ... - set coinduction |
408 goal "x:A" coinduct ... - set coinduction |
411 coinduct x - type coinduction |
409 coinduct x - type coinduction |
412 ... coinduct ... r - explicit rule |
410 coinduct ... r - explicit rule |
413 *) |
411 *) |
414 |
412 |
415 local |
413 local |
416 |
414 |
417 fun find_coinductT ctxt (SOME t :: _) = InductAttrib.find_coinductT ctxt (Term.fastype_of t) |
415 fun find_coinductT ctxt (SOME t :: _) = InductAttrib.find_coinductT ctxt (Term.fastype_of t) |
418 | find_coinductT _ _ = []; |
416 | find_coinductT _ _ = []; |
419 |
417 |
420 fun find_coinductS ctxt (fact :: _) = InductAttrib.find_coinductS ctxt fact |
418 fun find_coinductS ctxt goal = InductAttrib.find_coinductS ctxt (Logic.strip_assums_concl goal); |
421 | find_coinductS _ _ = []; |
|
422 |
419 |
423 in |
420 in |
424 |
421 |
425 fun coinduct_tac ctxt is_open inst opt_rule facts = |
422 fun coinduct_tac ctxt is_open inst opt_rule facts = |
426 let |
423 let |
|
424 val _ = warn_open is_open; |
427 val thy = ProofContext.theory_of ctxt; |
425 val thy = ProofContext.theory_of ctxt; |
428 val cert = Thm.cterm_of thy; |
426 val cert = Thm.cterm_of thy; |
429 |
427 |
430 val inst_rule = apfst (fn r => |
428 val inst_rule = apsnd (fn r => |
431 if null inst then r |
429 if null inst then r |
432 else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r); |
430 else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r); |
433 |
431 |
434 val ruleq = |
432 fun ruleq goal = |
435 (case opt_rule of |
433 (case opt_rule of |
436 SOME r => r |> rule_versions |> Seq.map inst_rule |
434 SOME r => r |> rule_versions |> Seq.map inst_rule |
437 | NONE => |
435 | NONE => |
438 (find_coinductS ctxt facts @ find_coinductT ctxt inst) |
436 (find_coinductS ctxt goal @ find_coinductT ctxt inst) |
439 |> tap (trace_rules ctxt InductAttrib.coinductN) |
437 |> tap (trace_rules ctxt InductAttrib.coinductN) |
440 |> Seq.of_list |> Seq.maps rule_versions |> Seq.maps (Seq.try inst_rule)) |
438 |> Seq.of_list |> Seq.maps rule_versions |> Seq.maps (Seq.try inst_rule)); |
441 |> Seq.maps (fn (th, (cases, n)) => |
|
442 Method.multi_resolves (Library.take (n, facts)) [th] |
|
443 |> Seq.map (apsnd (rpair (Library.drop (n, facts))) o rpair cases)); |
|
444 in |
439 in |
445 fn i => fn st => |
440 SUBGOAL_CASES (fn (goal, i) => fn st => |
446 ruleq |> Seq.maps (fn (rule, (cases, more_facts)) => |
441 ruleq goal |
447 (Method.insert_tac more_facts THEN' Tactic.rtac rule) i st |> Seq.maps (fn st' => |
442 |> Seq.maps (RuleCases.consume facts) |
448 divinate_inst rule i st' |> Seq.maps (fn rule' => |
443 |> Seq.maps (fn ((cases, (_, more_facts)), rule) => |
449 Tactic.rtac rule' i st' |
444 divinate_inst rule i st |> Seq.maps (fn rule' => |
450 |> Seq.map (rpair (make_cases is_open rule' cases))))) |
445 CASES (make_cases is_open rule' cases) |
|
446 (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st))) |
451 end; |
447 end; |
452 |
448 |
453 val coinduct_meth = Method.RAW_METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo |
449 val coinduct_meth = Method.RAW_METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo |
454 (fn (ctxt, (is_open, (insts, opt_rule))) => |
450 (fn (ctxt, (is_open, (insts, opt_rule))) => |
455 coinduct_tac ctxt is_open insts opt_rule)); |
451 coinduct_tac ctxt is_open insts opt_rule)); |