Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: relation.ML Sprache: SML

Original von: Isabelle^©

(*  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 ([], [(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 ([], [(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

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