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/HOL/Tools/Function/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 1 kB

Quelle relation.ML Sprache: SML

(*  Title:      HOL/Tools/Function/relation.ML
    Author:     Alexander Krauss, TU Muenchen

Tactics to start a termination proof using a user-specified relation.
*)

signature FUNCTION_RELATION =
sig
  val relation_tac: Proof.context -> (typ -> term) -> int -> tactic
  val relation_infer_tac: Proof.context -> term -> int -> tactic
end

structure Function_Relation: FUNCTION_RELATION =
struct

(* tactic version *)

fun inst_state_tac ctxt inst =
  SUBGOAL (fn (goal, _) =>
    (case Term.add_vars goal [] of
      [v as (_, T)] =>
        PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make1 (v, Thm.cterm_of ctxt (inst T))))
    | _ => no_tac));

fun relation_tac ctxt rel i =
  TRY (Function_Common.termination_rule_tac ctxt i)
  THEN inst_state_tac ctxt rel i;

(* version with type inference *)

fun inst_state_infer_tac ctxt rel =
  SUBGOAL (fn (goal, _) =>
    (case Term.add_vars goal [] of
      [v as (_, T)] =>
        let
          val rel' =
            singleton (Variable.polymorphic ctxt) rel
            |> map_types Type_Infer.paramify_vars
            |> Type.constraint T
            |> Syntax.check_term ctxt;
        in PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make1 (v, Thm.cterm_of ctxt rel'))) end
    | _ => no_tac));

fun relation_infer_tac ctxt rel i =
  TRY (Function_Common.termination_rule_tac ctxt i)
  THEN inst_state_infer_tac ctxt rel i;

end

quality99%

¤ Dauer der Verarbeitung: 0.13 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.