Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/Pure/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 3 kB

Quelle thm_name.ML Sprache: SML

(*  Title:      Pure/thm_name.ML
    Author:     Makarius

Systematic naming of individual theorems, as selections from multi-facts.

  (NAME, 0): the single entry of a singleton fact NAME
  (NAME, i): entry i of a non-singleton fact (1 <= i <= length)
*)

signature THM_NAME =
sig
  type T = string * int
  val ord: T ord
  structure Set: SET
  structure Table: TABLE
  val empty: T
  val is_empty: T -> bool
  val make_list: string * 'a list -> (T * 'a) list

  type P = T * Position.T
  val none: P
  val list: string * Position.T -> 'a list -> (P * 'a) list
  val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list

  val parse: string -> T
  val print_prefix: Proof.context -> Name_Space.T -> T -> Markup.T * string
  val print_suffix: T -> string
  val print: T -> string
  val print_pos: P -> string
  val short: T -> string
  val encode: T XML.Encode.T
  val decode: T XML.Decode.T
  val encode_pos: P XML.Encode.T
  val decode_pos: P XML.Decode.T
end;

structure Thm_Name: THM_NAME =
struct

(* type T *)

type T = string * int;
val ord = prod_ord string_ord int_ord;

structure Set = Set(type key = T val ord = ord);
structure Table = Table(Set.Key);

val empty: T = ("", 0);
fun is_empty ((a, _): T) = a = "";

fun make_list (a, [b]) = [((a, 0): T, b)]
  | make_list (a, bs) = map_index (fn (i, b) => ((a, i + 1), b)) bs;

(* type P *)

type P = T * Position.T;

val none: P = (empty, Position.none);

fun list (name, pos) [x] = [(((name, 0), pos): P, x)]
  | list ("", pos) xs = map (fn thm => ((empty, pos), thm)) xs
  | list (name, pos) xs = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) xs;

fun expr name = burrow_fst (burrow (list name));

(* parse *)

local

fun is_bg c = c = #"(";
fun is_en c = c = #")";
fun is_digit c = #"0" <= c andalso c <= #"9";
fun get_digit c = Char.ord c - Char.ord #"0";

in

fun parse string =
  let
    val n = size string;
    fun char i = if 0 <= i andalso i < n then String.nth string i else #"\000";
    fun test pred i = pred (char i);

    fun scan i k m =
      let val c = char i in
        if is_digit c then scan (i - 1) (k * 10) (m + k * get_digit c)
        else if is_bg c then (String.substring (string, 0, i), m)
        else (string, 0)
      end;
  in
    if test is_en (n - 1) andalso test is_digit (n - 2)
    then scan (n - 2) 1 0
    else (string, 0)
  end;

end;

(* print *)

fun print_prefix ctxt space ((name, _): T) =
  if name = "" then (Markup.empty, "")
  else (Name_Space.markup space name, Name_Space.extern ctxt space name);

fun print_suffix (name, index) =
  if name = "" orelse index = 0 then ""
  else enclose "(" ")" (string_of_int index);

fun print (name, index) = name ^ print_suffix (name, index);

fun print_pos (thm_name, pos) = print thm_name ^ Position.here pos;

fun short (name, index) =
  if name = "" orelse index = 0 then name
  else name ^ "_" ^ string_of_int index;

(* XML data representation *)

val encode = let open XML.Encode in pair string int end;
val decode = let open XML.Decode in pair string int end;

val encode_pos = let open XML.Encode in pair encode (properties o Position.properties_of) end;
val decode_pos = let open XML.Decode in pair decode (Position.of_properties o properties) end;

end;

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

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.