summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/IsarImplementation/Thy/proof.thy

author | wenzelm |

Sat, 08 Jul 2006 14:01:40 +0200 | |

changeset 20064 | 92aad017b847 |

parent 20041 | ae7aba935986 |

child 20171 | 424739228123 |

permissions | -rw-r--r-- |

tuned;

(* $Id$ *) theory "proof" imports base begin chapter {* Structured reasoning *} section {* Proof context *} subsection {* Local variables *} text FIXME text %mlref {* \begin{mldecls} @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\ @{index_ML Variable.add_fixes: "string list -> Proof.context -> string list * Proof.context"} \\ @{index_ML Variable.import: "bool -> thm list -> Proof.context -> thm list * Proof.context"} \\ @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\ @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\ @{index_ML Variable.monomorphic: "Proof.context -> term list -> term list"} \\ @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ \end{mldecls} \begin{description} \item @{ML Variable.declare_term}~@{text "t ctxt"} declares term @{text "t"} to belong to the context. This fixes free type variables, but not term variables. Constraints for type and term variables are declared uniformly. \item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term variables @{text "xs"} and returns the internal names of the resulting Skolem constants. Note that term fixes refer to \emph{all} type instances that may occur in the future. \item @{ML Variable.invent_fixes} is similar to @{ML Variable.add_fixes}, but the given names merely act as hints for internal fixes produced here. \item @{ML Variable.import}~@{text "open ths ctxt"} augments the context by new fixes for the schematic type and term variables occurring in @{text "ths"}. The @{text "open"} flag indicates whether the fixed names should be accessible to the user, otherwise internal names are chosen. \item @{ML Variable.export}~@{text "inner outer ths"} generalizes fixed type and term variables in @{text "ths"} according to the difference of the @{text "inner"} and @{text "outer"} context. Note that type variables occurring in term variables are still fixed. @{ML Variable.export} essentially reverses the effect of @{ML Variable.import} (up to renaming of schematic variables. \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML Variable.export}, i.e.\ it provides a view on facts with all variables being fixed in the current context. \item @{ML Variable.monomorphic}~@{text "ctxt ts"} introduces fixed type variables for the schematic ones in @{text "ts"}. \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type variables in @{text "ts"} as far as possible, even those occurring in fixed term variables. This operation essentially reverses the default policy of type-inference to introduce local polymorphism as fixed types. \end{description} *} text FIXME section {* Proof state *} text {* FIXME \glossary{Proof state}{The whole configuration of a structured proof, consisting of a \seeglossary{proof context} and an optional \seeglossary{structured goal}. Internally, an Isar proof state is organized as a stack to accomodate block structure of proof texts. For historical reasons, a low-level \seeglossary{tactical goal} is occasionally called ``proof state'' as well.} \glossary{Structured goal}{FIXME} \glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage} *} section {* Methods *} text FIXME section {* Attributes *} text FIXME end