# HG changeset patch # User wenzelm # Date 1157380107 -7200 # Node ID c839b38a1f3203dc4b173b03e116dc1d34bac5a2 # Parent bb75c1cdf913a3788e3e337cc326a552c6c73245 more on variables; tuned; diff -r bb75c1cdf913 -r c839b38a1f32 doc-src/IsarImplementation/Thy/logic.thy --- a/doc-src/IsarImplementation/Thy/logic.thy Mon Sep 04 15:27:30 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/logic.thy Mon Sep 04 16:28:27 2006 +0200 @@ -3,7 +3,7 @@ theory logic imports base begin -chapter {* Primitive logic *} +chapter {* Primitive logic \label{ch:logic} *} section {* Variable names *} diff -r bb75c1cdf913 -r c839b38a1f32 doc-src/IsarImplementation/Thy/prelim.thy --- a/doc-src/IsarImplementation/Thy/prelim.thy Mon Sep 04 15:27:30 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/prelim.thy Mon Sep 04 16:28:27 2006 +0200 @@ -393,11 +393,11 @@ argument structure. The resulting structure provides data init and access operations as described above. - \item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous for - type @{ML_type Proof.context}. + \item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous to + @{ML_functor TheoryDataFun} for type @{ML_type Proof.context}. - \item @{ML_functor GenericDataFun}@{text "(spec)"} is analogous for - type @{ML_type Context.generic}. + \item @{ML_functor GenericDataFun}@{text "(spec)"} is analogous to + @{ML_functor TheoryDataFun} for type @{ML_type Context.generic}. \end{description} *} @@ -406,6 +406,8 @@ section {* Name spaces *} text {* + FIXME tune + By general convention, each kind of formal entities (logical constant, type, type class, theorem, method etc.) lives in a separate name space. It is usually clear from the syntactic context @@ -443,6 +445,8 @@ subsection {* Strings of symbols *} text {* + FIXME tune + Isabelle strings consist of a sequence of symbols\glossary{Symbol}{The smallest unit of text in Isabelle, subsumes plain ASCII characters as well as an infinite collection of @@ -539,6 +543,8 @@ subsection {* Qualified names *} text {* + FIXME tune + A \emph{qualified name} essentially consists of a non-empty list of basic name components. The packad notation uses a dot as separator, as in @{text "A.b"}, for example. The very last component is called diff -r bb75c1cdf913 -r c839b38a1f32 doc-src/IsarImplementation/Thy/proof.thy --- a/doc-src/IsarImplementation/Thy/proof.thy Mon Sep 04 15:27:30 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/proof.thy Mon Sep 04 16:28:27 2006 +0200 @@ -7,53 +7,137 @@ section {* Variables *} -text FIXME +text {* + Any variable that is not explicitly bound by @{text "\"}-abstraction + is considered as ``free''. Logically, free variables act like + outermost universal quantification (at the sequent level): @{text + "A\<^isub>1(x), \, A\<^isub>n(x) \ B(x)"} means that the result + holds \emph{for all} values of @{text "x"}. Free variables for + terms (not types) can be fully internalized into the logic: @{text + "\ B(x)"} and @{text "\ \x. B(x)"} are interchangeable provided that + @{text "x"} does not occur elsewhere in the context. Inspecting + @{text "\ \x. B(x)"} more closely, we see that inside the + quantifier, @{text "x"} is essentially ``arbitrary, but fixed'', + while from outside it appears as a place-holder for instantiation + (thanks to @{text "\"}-elimination). + + The Pure logic represents the notion of variables being either + inside or outside the current scope by providing separate syntactic + categories for \emph{fixed variables} (e.g.\ @{text "x"}) vs.\ + \emph{schematic variables} (e.g.\ @{text "?x"}). Incidently, a + universal result @{text "\ \x. B(x)"} has the canonical form @{text + "\ B(?x)"}, which represents its generality nicely without requiring + an explicit quantifier. The same principle works for type variables + as well: @{text "\ B(?\)"} expresses the idea of ``@{text "\ + \\. B(\)"}'' without demanding a truly polymorphic framework. + + \medskip Additional care is required to treat type variables in a + way that facilitates type-inference. In principle, term variables + depend on type variables, which means that type variables would have + to be declared first. For example, a raw type-theoretic framework + would demand the context to be constructed in stages as follows: + @{text "\ = \: type, x: \, a: A(x\<^isub>\)"}. + + We allow a slightly less formalistic mode of operation: term + variables @{text "x"} are fixed without specifying a type yet + (essentially \emph{all} potential occurrences of some instance + @{text "x\<^isub>\"} will be fixed); the first occurrence of @{text + "x"} within a specific term assigns its most general type, which is + then maintained consistently in the context. The above example + becomes @{text "\ = x: term, \: type, A(x\<^isub>\)"}, where type + @{text "\"} is fixed \emph{after} term @{text "x"}, and the + constraint @{text "x: \"} is an implicit consequence of the + occurrence of @{text "x\<^isub>\"} in the subsequent proposition. + + This twist of dependencies is also accommodated by the reverse + operation of exporting results from a context: a type variable + @{text "\"} is considered fixed as long as it occurs in some fixed + term variable of the context. For example, exporting @{text "x: + term, \: type \ x\<^isub>\ = x\<^isub>\"} produces @{text "x: term \ + x\<^isub>\ = x\<^isub>\"} for fixed @{text "\"} in the first step, + and @{text "\ ?x\<^isub>?\<^isub>\ = ?x\<^isub>?\<^isub>\"} for + schematic @{text "?x"} and @{text "?\"} only in the second step. + + \medskip The Isabelle/Isar proof context manages the gory details of + term vs.\ type variables, with high-level principles for moving the + frontier between fixed and schematic variables. By observing a + simple discipline of fixing variables and declaring terms + explicitly, the fine points are treated by the @{text "export"} + operation. + + There is also a separate @{text "import"} operation makes a + generalized fact a genuine part of the context, by inventing fixed + variables for the schematic ones. The effect can be reversed by + using @{text "export"} later, with a potentially extended context, + but the result will be only equivalent modulo renaming of schematic + variables. + + The @{text "focus"} operation provides a variant of @{text "import"} + for nested propositions (with explicit quantification): @{text + "\x. B(x)"} is decomposed by inventing a fixed variable @{text "x"} + and for the body @{text "B(x)"}. +*} text %mlref {* \begin{mldecls} + @{index_ML Variable.add_fixes: "string list -> Proof.context -> string list * Proof.context"} \\ + @{index_ML Variable.invent_fixes: "string list -> Proof.context -> string list * Proof.context"} \\ @{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.declare_constraints: "term -> Proof.context -> Proof.context"} \\ + @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\ + @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ @{index_ML Variable.import: "bool -> thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context"} \\ - @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\ - @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ + @{index_ML Variable.focus: "cterm -> Proof.context -> (cterm list * cterm) * Proof.context"} \\ \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. + variables @{text "xs"}, returning the resulting internal names. By + default, the internal representation coincides with the external + one, which also means that the given variables must not have been + fixed already. Within a local proof body, the given names are just + hints for newly invented Skolem variables. \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. + Variable.add_fixes}, but always produces fresh variants of the given + hints. + + \item @{ML Variable.declare_term}~@{text "t ctxt"} declares term + @{text "t"} to belong to the context. This automatically fixes new + type variables, but not term variables. Syntactic constraints for + type and term variables are declared uniformly. + + \item @{ML Variable.declare_constraints}~@{text "t ctxt"} derives + type-inference information from term @{text "t"}, without making it + part of the context yet. - \item @{ML Variable.import}~@{text "open ths ctxt"} augments the + \item @{ML Variable.export}~@{text "inner outer thms"} generalizes + fixed type and term variables in @{text "thms"} according to the + difference of the @{text "inner"} and @{text "outer"} context, + following the principles sketched above. + + \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type + variables in @{text "ts"} as far as possible, even those occurring + in fixed term variables. The default policy of type-inference is to + fix newly introduced type variables; this is essentially reversed + with @{ML Variable.polymorphic}, the given terms are detached from + the context as far as possible. + + \item @{ML Variable.import}~@{text "open thms ctxt"} augments the context by new fixes for the schematic type and term variables - occurring in @{text "ths"}. The @{text "open"} flag indicates + occurring in @{text "thms"}. 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}, modulo renaming of schematic variables. - @{ML Variable.export} essentially reverses the effect of @{ML - Variable.import} (up to renaming of schematic variables. - - \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. + \item @{ML Variable.focus}~@{text "\x\<^isub>1 \ + x\<^isub>n. B(x\<^isub>1, \, x\<^isub>n)"} invents fixed variables + for @{text "x\<^isub>1, \, x\<^isub>n"} and replaces these in the + body. \end{description} *} diff -r bb75c1cdf913 -r c839b38a1f32 doc-src/IsarImplementation/Thy/unused.thy --- a/doc-src/IsarImplementation/Thy/unused.thy Mon Sep 04 15:27:30 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/unused.thy Mon Sep 04 16:28:27 2006 +0200 @@ -1,6 +1,17 @@ text {* + + + A \emph{fixed variable} acts like a local constant in the current + context, representing some simple type @{text "\"}, or some value + @{text "x: \"} (for a fixed type expression @{text "\"}). A + \emph{schematic variable} acts like a placeholder for arbitrary + elements, similar to outermost quantification. The division between + fixed and schematic variables tells which abstract entities are + inside and outside the current context. + + @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\ diff -r bb75c1cdf913 -r c839b38a1f32 doc-src/IsarImplementation/style.sty --- a/doc-src/IsarImplementation/style.sty Mon Sep 04 15:27:30 2006 +0200 +++ b/doc-src/IsarImplementation/style.sty Mon Sep 04 16:28:27 2006 +0200 @@ -7,6 +7,7 @@ %% references \newcommand{\secref}[1]{\S\ref{#1}} +\newcommand{\chref}[1]{chapter~\ref{#1}} \newcommand{\figref}[1]{figure~\ref{#1}} %% glossary