author | wenzelm |
Wed, 26 Jul 2006 19:37:41 +0200 | |
changeset 20218 | be3bfb0699ba |
parent 20171 | 424739228123 |
child 20451 | 27ea2ba48fa3 |
permissions | -rw-r--r-- |
18537 | 1 |
|
2 |
(* $Id$ *) |
|
3 |
||
4 |
theory "proof" imports base begin |
|
5 |
||
6 |
chapter {* Structured reasoning *} |
|
7 |
||
8 |
section {* Proof context *} |
|
9 |
||
20026 | 10 |
subsection {* Local variables *} |
11 |
||
20064 | 12 |
text FIXME |
13 |
||
20026 | 14 |
text %mlref {* |
15 |
\begin{mldecls} |
|
16 |
@{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\ |
|
20064 | 17 |
@{index_ML Variable.add_fixes: "string list -> Proof.context -> string list * Proof.context"} \\ |
20218
be3bfb0699ba
Variable.import(T): result includes fixed types/terms;
wenzelm
parents:
20171
diff
changeset
|
18 |
@{index_ML Variable.import: "bool -> thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context"} \\ |
20026 | 19 |
@{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\ |
20 |
@{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\ |
|
21 |
@{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ |
|
22 |
\end{mldecls} |
|
23 |
||
24 |
\begin{description} |
|
25 |
||
20064 | 26 |
\item @{ML Variable.declare_term}~@{text "t ctxt"} declares term |
27 |
@{text "t"} to belong to the context. This fixes free type |
|
28 |
variables, but not term variables. Constraints for type and term |
|
29 |
variables are declared uniformly. |
|
30 |
||
31 |
\item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term |
|
32 |
variables @{text "xs"} and returns the internal names of the |
|
33 |
resulting Skolem constants. Note that term fixes refer to |
|
34 |
\emph{all} type instances that may occur in the future. |
|
35 |
||
36 |
\item @{ML Variable.invent_fixes} is similar to @{ML |
|
37 |
Variable.add_fixes}, but the given names merely act as hints for |
|
38 |
internal fixes produced here. |
|
20026 | 39 |
|
20064 | 40 |
\item @{ML Variable.import}~@{text "open ths ctxt"} augments the |
41 |
context by new fixes for the schematic type and term variables |
|
42 |
occurring in @{text "ths"}. The @{text "open"} flag indicates |
|
43 |
whether the fixed names should be accessible to the user, otherwise |
|
44 |
internal names are chosen. |
|
20026 | 45 |
|
20064 | 46 |
\item @{ML Variable.export}~@{text "inner outer ths"} generalizes |
47 |
fixed type and term variables in @{text "ths"} according to the |
|
48 |
difference of the @{text "inner"} and @{text "outer"} context. Note |
|
49 |
that type variables occurring in term variables are still fixed. |
|
50 |
||
51 |
@{ML Variable.export} essentially reverses the effect of @{ML |
|
52 |
Variable.import} (up to renaming of schematic variables. |
|
20026 | 53 |
|
54 |
\item @{ML Variable.trade} composes @{ML Variable.import} and @{ML |
|
20041 | 55 |
Variable.export}, i.e.\ it provides a view on facts with all |
56 |
variables being fixed in the current context. |
|
20026 | 57 |
|
20064 | 58 |
\item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type |
59 |
variables in @{text "ts"} as far as possible, even those occurring |
|
60 |
in fixed term variables. This operation essentially reverses the |
|
61 |
default policy of type-inference to introduce local polymorphism as |
|
62 |
fixed types. |
|
20026 | 63 |
|
64 |
\end{description} |
|
65 |
*} |
|
66 |
||
18537 | 67 |
text FIXME |
68 |
||
69 |
section {* Proof state *} |
|
70 |
||
71 |
text {* |
|
72 |
FIXME |
|
73 |
||
74 |
\glossary{Proof state}{The whole configuration of a structured proof, |
|
75 |
consisting of a \seeglossary{proof context} and an optional |
|
76 |
\seeglossary{structured goal}. Internally, an Isar proof state is |
|
77 |
organized as a stack to accomodate block structure of proof texts. |
|
78 |
For historical reasons, a low-level \seeglossary{tactical goal} is |
|
79 |
occasionally called ``proof state'' as well.} |
|
80 |
||
81 |
\glossary{Structured goal}{FIXME} |
|
82 |
||
83 |
\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage} |
|
84 |
||
85 |
||
86 |
*} |
|
87 |
||
88 |
section {* Methods *} |
|
89 |
||
90 |
text FIXME |
|
91 |
||
92 |
section {* Attributes *} |
|
93 |
||
94 |
text FIXME |
|
95 |
||
96 |
end |