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