Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: yaml.xml Sprache: SML

Original von: Isabelle^©

(*  Title:      HOL/Tools/Function/fun_cases.ML
    Author:     Manuel Eberl, TU Muenchen

The fun_cases command for generating specialised elimination rules for
function package functions.
*)

signature FUN_CASES =
sig
  val mk_fun_cases: Proof.context -> term -> thm
  val fun_cases: (Attrib.binding * term list) list -> local_theory ->
    (string * thm list) list * local_theory
  val fun_cases_cmd: (Attrib.binding * string list) list -> local_theory ->
    (string * thm list) list * local_theory
end;

structure Fun_Cases : FUN_CASES =
struct

fun mk_fun_cases ctxt prop =
  let
    fun err () =
      error (Pretty.string_of (Pretty.block
        [Pretty.str "Proposition is not a function equation:",
         Pretty.fbrk, Syntax.pretty_term ctxt prop]));
    val ((f, _), _) =
      Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
        handle TERM _ => err ();
    val info = Function.get_info ctxt f handle List.Empty => err ();
    val {elims, pelims, is_partial, ...} = info;
    val elims = if is_partial then pelims else the elims;
    val cprop = Thm.cterm_of ctxt prop;
    fun mk_elim rl =
      Thm.implies_intr cprop
        (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
      |> singleton (Proof_Context.export (Proof_Context.augment prop ctxt) ctxt);
  in
    (case get_first (try mk_elim) (flat elims) of
      SOME r => r
    | NONE => err ())
  end;

fun gen_fun_cases prep_att prep_prop args lthy =
  let
    val thmss =
      map snd args
      |> burrow (grouped 10 Par_List.map_independent (mk_fun_cases lthy o prep_prop lthy));
    val facts =
      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
        args thmss;
  in lthy |> Local_Theory.notes facts end;

val fun_cases = gen_fun_cases (K I) Syntax.check_prop;
val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop;

val _ =
  Outer_Syntax.local_theory \<^command_keyword>\<open>fun_cases\<close>
    "create simplified instances of elimination rules for function equations"
    (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo fun_cases_cmd));

end;

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.