4 theory "proof" imports base begin
6 chapter {* Structured proofs *}
8 section {* Local variables *}
14 @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
15 @{index_ML Variable.add_fixes: "string list -> Proof.context -> string list * Proof.context"} \\
16 @{index_ML Variable.import: "bool -> thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context"} \\
17 @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
18 @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
19 @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
24 \item @{ML Variable.declare_term}~@{text "t ctxt"} declares term
25 @{text "t"} to belong to the context. This fixes free type
26 variables, but not term variables. Constraints for type and term
27 variables are declared uniformly.
29 \item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term
30 variables @{text "xs"} and returns the internal names of the
31 resulting Skolem constants. Note that term fixes refer to
32 \emph{all} type instances that may occur in the future.
34 \item @{ML Variable.invent_fixes} is similar to @{ML
35 Variable.add_fixes}, but the given names merely act as hints for
36 internal fixes produced here.
38 \item @{ML Variable.import}~@{text "open ths ctxt"} augments the
39 context by new fixes for the schematic type and term variables
40 occurring in @{text "ths"}. The @{text "open"} flag indicates
41 whether the fixed names should be accessible to the user, otherwise
42 internal names are chosen.
44 \item @{ML Variable.export}~@{text "inner outer ths"} generalizes
45 fixed type and term variables in @{text "ths"} according to the
46 difference of the @{text "inner"} and @{text "outer"} context. Note
47 that type variables occurring in term variables are still fixed.
49 @{ML Variable.export} essentially reverses the effect of @{ML
50 Variable.import} (up to renaming of schematic variables.
52 \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML
53 Variable.export}, i.e.\ it provides a view on facts with all
54 variables being fixed in the current context.
56 \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type
57 variables in @{text "ts"} as far as possible, even those occurring
58 in fixed term variables. This operation essentially reverses the
59 default policy of type-inference to introduce local polymorphism as
68 section {* Schematic polymorphism *}
73 section {* Assumptions *}
78 section {* Conclusions *}
83 section {* Structured proofs \label{sec:isar-proof-state} *}
88 \glossary{Proof state}{The whole configuration of a structured proof,
89 consisting of a \seeglossary{proof context} and an optional
90 \seeglossary{structured goal}. Internally, an Isar proof state is
91 organized as a stack to accomodate block structure of proof texts.
92 For historical reasons, a low-level \seeglossary{tactical goal} is
93 occasionally called ``proof state'' as well.}
95 \glossary{Structured goal}{FIXME}
97 \glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}
102 section {* Proof methods *}
106 section {* Attributes *}