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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.