| products/sources/formale sprachen/Isabelle/Tools/Metis/src/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: Ordered.sig Sprache: Unknown
|
Untersuchungsergebnis.sig Download desIsabelle {Isabelle[126] Abap[146] [0]}zum Wurzelverzeichnis wechseln (* ========================================================================= *) (* FIRST ORDER LOGIC LITERALS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) signature Literal = sig (* ------------------------------------------------------------------------- *) (* A type for storing first order logic literals. *) (* ------------------------------------------------------------------------- *) type polarity = bool type literal = polarity * Atom.atom (* ------------------------------------------------------------------------- *) (* Constructors and destructors. *) (* ------------------------------------------------------------------------- *) val polarity : literal -> polarity val atom : literal -> Atom.atom val name : literal -> Atom.relationName val arguments : literal -> Term.term list val arity : literal -> int val positive : literal -> bool val negative : literal -> bool val negate : literal -> literal val relation : literal -> Atom.relation val functions : literal -> NameAritySet.set val functionNames : literal -> NameSet.set (* Binary relations *) val mkBinop : Atom.relationName -> polarity * Term.term * Term.term -> literal val destBinop : Atom.relationName -> literal -> polarity * Term.term * Term.term val isBinop : Atom.relationName -> literal -> bool (* Formulas *) val toFormula : literal -> Formula.formula val fromFormula : Formula.formula -> literal (* ------------------------------------------------------------------------- *) (* The size of a literal in symbols. *) (* ------------------------------------------------------------------------- *) val symbols : literal -> int (* ------------------------------------------------------------------------- *) (* A total comparison function for literals. *) (* ------------------------------------------------------------------------- *) val compare : literal * literal -> order (* negative < positive *) val equal : literal -> literal -> bool (* ------------------------------------------------------------------------- *) (* Subterms. *) (* ------------------------------------------------------------------------- *) val subterm : literal -> Term.path -> Term.term val subterms : literal -> (Term.path * Term.term) list val replace : literal -> Term.path * Term.term -> literal (* ------------------------------------------------------------------------- *) (* Free variables. *) (* ------------------------------------------------------------------------- *) val freeIn : Term.var -> literal -> bool val freeVars : literal -> NameSet.set (* ------------------------------------------------------------------------- *) (* Substitutions. *) (* ------------------------------------------------------------------------- *) val subst : Subst.subst -> literal -> literal (* ------------------------------------------------------------------------- *) (* Matching. *) (* ------------------------------------------------------------------------- *) val match : (* raises Error *) Subst.subst -> literal -> literal -> Subst.subst (* ------------------------------------------------------------------------- *) (* Unification. *) (* ------------------------------------------------------------------------- *) val unify : (* raises Error *) Subst.subst -> literal -> literal -> Subst.subst (* ------------------------------------------------------------------------- *) (* The equality relation. *) (* ------------------------------------------------------------------------- *) val mkEq : Term.term * Term.term -> literal val destEq : literal -> Term.term * Term.term val isEq : literal -> bool val mkNeq : Term.term * Term.term -> literal val destNeq : literal -> Term.term * Term.term val isNeq : literal -> bool val mkRefl : Term.term -> literal val destRefl : literal -> Term.term val isRefl : literal -> bool val mkIrrefl : Term.term -> literal val destIrrefl : literal -> Term.term val isIrrefl : literal -> bool (* The following work with both equalities and disequalities *) val sym : literal -> literal (* raises Error if given a refl or irrefl *) val lhs : literal -> Term.term val rhs : literal -> Term.term (* ------------------------------------------------------------------------- *) (* Special support for terms with type annotations. *) (* ------------------------------------------------------------------------- *) val typedSymbols : literal -> int val nonVarTypedSubterms : literal -> (Term.path * Term.term) list (* ------------------------------------------------------------------------- *) (* Parsing and pretty-printing. *) (* ------------------------------------------------------------------------- *) val pp : literal Print.pp val toString : literal -> string val fromString : string -> literal val parse : Term.term Parse.quotation -> literal end [ zur Elbe Produktseite wechseln0.96Quellennavigators ] |