29 % |
29 % |
30 \isamarkupsubsection{Local variables% |
30 \isamarkupsubsection{Local variables% |
31 } |
31 } |
32 \isamarkuptrue% |
32 \isamarkuptrue% |
33 % |
33 % |
|
34 \begin{isamarkuptext}% |
|
35 FIXME% |
|
36 \end{isamarkuptext}% |
|
37 \isamarkuptrue% |
|
38 % |
34 \isadelimmlref |
39 \isadelimmlref |
35 % |
40 % |
36 \endisadelimmlref |
41 \endisadelimmlref |
37 % |
42 % |
38 \isatagmlref |
43 \isatagmlref |
39 % |
44 % |
40 \begin{isamarkuptext}% |
45 \begin{isamarkuptext}% |
41 \begin{mldecls} |
46 \begin{mldecls} |
42 \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\ |
47 \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\ |
|
48 \indexml{Variable.add-fixes}\verb|Variable.add_fixes: string list -> Proof.context -> string list * Proof.context| \\ |
43 \indexml{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context -> thm list * Proof.context| \\ |
49 \indexml{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context -> thm list * Proof.context| \\ |
44 \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\ |
50 \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\ |
45 \indexml{Variable.trade}\verb|Variable.trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list| \\ |
51 \indexml{Variable.trade}\verb|Variable.trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list| \\ |
46 \indexml{Variable.monomorphic}\verb|Variable.monomorphic: Proof.context -> term list -> term list| \\ |
52 \indexml{Variable.monomorphic}\verb|Variable.monomorphic: Proof.context -> term list -> term list| \\ |
47 \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\ |
53 \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\ |
48 \end{mldecls} |
54 \end{mldecls} |
49 |
55 |
50 \begin{description} |
56 \begin{description} |
51 |
57 |
52 \item \verb|Variable.declare_term| declares a term as belonging to |
58 \item \verb|Variable.declare_term|~\isa{t\ ctxt} declares term |
53 the current context. This fixes free type variables, but not term |
59 \isa{t} to belong to the context. This fixes free type |
54 variables; constraints for type and term variables are declared |
60 variables, but not term variables. Constraints for type and term |
55 uniformly. |
61 variables are declared uniformly. |
56 |
62 |
57 \item \verb|Variable.import| introduces new fixes for schematic type |
63 \item \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term |
58 and term variables occurring in given facts. The effect may be |
64 variables \isa{xs} and returns the internal names of the |
59 reversed (up to renaming) via \verb|Variable.export|. |
65 resulting Skolem constants. Note that term fixes refer to |
|
66 \emph{all} type instances that may occur in the future. |
60 |
67 |
61 \item \verb|Variable.export| generalizes fixed type and term |
68 \item \verb|Variable.invent_fixes| is similar to \verb|Variable.add_fixes|, but the given names merely act as hints for |
62 variables according to the difference of the two contexts. Note |
69 internal fixes produced here. |
63 that type variables occurring in term variables are still fixed, |
70 |
64 even though they got introduced later (e.g.\ by type-inference). |
71 \item \verb|Variable.import|~\isa{open\ ths\ ctxt} augments the |
|
72 context by new fixes for the schematic type and term variables |
|
73 occurring in \isa{ths}. The \isa{open} flag indicates |
|
74 whether the fixed names should be accessible to the user, otherwise |
|
75 internal names are chosen. |
|
76 |
|
77 \item \verb|Variable.export|~\isa{inner\ outer\ ths} generalizes |
|
78 fixed type and term variables in \isa{ths} according to the |
|
79 difference of the \isa{inner} and \isa{outer} context. Note |
|
80 that type variables occurring in term variables are still fixed. |
|
81 |
|
82 \verb|Variable.export| essentially reverses the effect of \verb|Variable.import| (up to renaming of schematic variables. |
65 |
83 |
66 \item \verb|Variable.trade| composes \verb|Variable.import| and \verb|Variable.export|, i.e.\ it provides a view on facts with all |
84 \item \verb|Variable.trade| composes \verb|Variable.import| and \verb|Variable.export|, i.e.\ it provides a view on facts with all |
67 variables being fixed in the current context. |
85 variables being fixed in the current context. |
68 |
86 |
69 \item \verb|Variable.monomorphic| introduces fixed type variables for |
87 \item \verb|Variable.monomorphic|~\isa{ctxt\ ts} introduces fixed |
70 the schematic of the given facts. |
88 type variables for the schematic ones in \isa{ts}. |
71 |
89 |
72 \item \verb|Variable.polymorphic| generalizes type variables as far |
90 \item \verb|Variable.polymorphic|~\isa{ctxt\ ts} generalizes type |
73 as possible, even those occurring in fixed term variables. This |
91 variables in \isa{ts} as far as possible, even those occurring |
74 operation essentially reverses the default policy of type-inference |
92 in fixed term variables. This operation essentially reverses the |
75 to introduce local polymorphism entities in fixed form. |
93 default policy of type-inference to introduce local polymorphism as |
|
94 fixed types. |
76 |
95 |
77 \end{description}% |
96 \end{description}% |
78 \end{isamarkuptext}% |
97 \end{isamarkuptext}% |
79 \isamarkuptrue% |
98 \isamarkuptrue% |
80 % |
99 % |