Quelle Base.thy

Sprache: Isabelle

(*:maxLineLen=78:*)

section ‹Basic setup that is not included in the document›

theory Base
imports Main
begin

ML_file ‹~~/src/Doc/antiquote_setup.ML›

ML‹
fun get_split_rule ctxt target =
let
val (head, args) = strip_comb (Envir.eta_contract target);
val const_name = dest_Const_name head;
val const_name_components = Long_Name.explode const_name;

val _ =
if String.isPrefix "case_" (List.last const_name_components) then ()
else raise TERM ("Not a case statement", [target]);

val type_name = Long_Name.implode (rev (tl (rev const_name_components)));
val split = Proof_Context.get_thm ctxt (type_name ^ ".split");
val vars = Term.add_vars (Thm.prop_of split) [];

val datatype_name = nth (rev const_name_components) 1;

fun is_datatype (Type (a, _)) = Long_Name.base_name a = Long_Name.base_name datatype_name
| is_datatype _ = false;

val datatype_var =
(case find_first (fn (_, T') => is_datatype T') vars of
SOME (xi, _) => xi
| NONE => error ("Couldn't find datatype in thm: " ^ datatype_name));
in
SOME (infer_instantiate ctxt [(datatype_var, Thm.cterm_of ctxt (List.last args))] split)
end
handle TERM _ => NONE;
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet am 2026-04-28) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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 und die Messung sind noch experimentell.