author | wenzelm |
Thu, 31 Aug 2006 23:01:16 +0200 | |
changeset 20452 | 6d8b29c7a960 |
parent 20451 | 27ea2ba48fa3 |
child 20458 | ab1d60e1ee31 |
permissions | -rw-r--r-- |
18537 | 1 |
|
2 |
(* $Id$ *) |
|
3 |
||
4 |
theory "proof" imports base begin |
|
5 |
||
20451 | 6 |
chapter {* Structured proofs *} |
18537 | 7 |
|
20452 | 8 |
section {* Variables and schematic polymorphism *} |
20026 | 9 |
|
20064 | 10 |
text FIXME |
11 |
||
20026 | 12 |
text %mlref {* |
13 |
\begin{mldecls} |
|
14 |
@{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\ |
|
20064 | 15 |
@{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
|
16 |
@{index_ML Variable.import: "bool -> thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context"} \\ |
20026 | 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"} \\ |
|
20 |
\end{mldecls} |
|
21 |
||
22 |
\begin{description} |
|
23 |
||
20064 | 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. |
|
28 |
||
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. |
|
33 |
||
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. |
|
20026 | 37 |
|
20064 | 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. |
|
20026 | 43 |
|
20064 | 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. |
|
48 |
||
49 |
@{ML Variable.export} essentially reverses the effect of @{ML |
|
50 |
Variable.import} (up to renaming of schematic variables. |
|
20026 | 51 |
|
52 |
\item @{ML Variable.trade} composes @{ML Variable.import} and @{ML |
|
20041 | 53 |
Variable.export}, i.e.\ it provides a view on facts with all |
54 |
variables being fixed in the current context. |
|
20026 | 55 |
|
20064 | 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 |
|
60 |
fixed types. |
|
20026 | 61 |
|
62 |
\end{description} |
|
63 |
*} |
|
64 |
||
18537 | 65 |
text FIXME |
66 |
||
20451 | 67 |
|
68 |
section {* Assumptions *} |
|
69 |
||
70 |
text FIXME |
|
71 |
||
72 |
||
73 |
section {* Conclusions *} |
|
74 |
||
75 |
text FIXME |
|
76 |
||
77 |
||
20452 | 78 |
section {* Proof states \label{sec:isar-proof-state} *} |
18537 | 79 |
|
80 |
text {* |
|
81 |
FIXME |
|
82 |
||
83 |
\glossary{Proof state}{The whole configuration of a structured proof, |
|
84 |
consisting of a \seeglossary{proof context} and an optional |
|
85 |
\seeglossary{structured goal}. Internally, an Isar proof state is |
|
86 |
organized as a stack to accomodate block structure of proof texts. |
|
87 |
For historical reasons, a low-level \seeglossary{tactical goal} is |
|
88 |
occasionally called ``proof state'' as well.} |
|
89 |
||
90 |
\glossary{Structured goal}{FIXME} |
|
91 |
||
92 |
\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage} |
|
93 |
||
94 |
||
95 |
*} |
|
96 |
||
20451 | 97 |
section {* Proof methods *} |
18537 | 98 |
|
99 |
text FIXME |
|
100 |
||
101 |
section {* Attributes *} |
|
102 |
||
20451 | 103 |
text "FIXME ?!" |
18537 | 104 |
|
105 |
end |