1(*  Title:      HOL/Tools/Function/fun_cases.ML
2    Author:     Manuel Eberl, TU Muenchen
3
4The fun_cases command for generating specialised elimination rules for
5function package functions.
6*)
7
8signature FUN_CASES =
9sig
10  val mk_fun_cases: Proof.context -> term -> thm
11  val fun_cases: (Attrib.binding * term list) list -> local_theory ->
12    (string * thm list) list * local_theory
13  val fun_cases_cmd: (Attrib.binding * string list) list -> local_theory ->
14    (string * thm list) list * local_theory
15end;
16
17structure Fun_Cases : FUN_CASES =
18struct
19
20fun mk_fun_cases ctxt prop =
21  let
22    fun err () =
23      error (Pretty.string_of (Pretty.block
24        [Pretty.str "Proposition is not a function equation:",
25         Pretty.fbrk, Syntax.pretty_term ctxt prop]));
26    val ((f, _), _) =
27      Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
28        handle TERM _ => err ();
29    val info = Function.get_info ctxt f handle List.Empty => err ();
30    val {elims, pelims, is_partial, ...} = info;
31    val elims = if is_partial then pelims else the elims;
32    val cprop = Thm.cterm_of ctxt prop;
33    fun mk_elim rl =
34      Thm.implies_intr cprop
35        (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
36      |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
37  in
38    (case get_first (try mk_elim) (flat elims) of
39      SOME r => r
40    | NONE => err ())
41  end;
42
43fun gen_fun_cases prep_att prep_prop args lthy =
44  let
45    val thmss =
46      map snd args
47      |> burrow (grouped 10 Par_List.map_independent (mk_fun_cases lthy o prep_prop lthy));
48    val facts =
49      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
50        args thmss;
51  in lthy |> Local_Theory.notes facts end;
52
53val fun_cases = gen_fun_cases (K I) Syntax.check_prop;
54val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop;
55
56val _ =
57  Outer_Syntax.local_theory \<^command_keyword>\<open>fun_cases\<close>
58    "create simplified instances of elimination rules for function equations"
59    (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo fun_cases_cmd));
60
61end;
62
63