tuned;
authorwenzelm
Tue Sep 12 17:45:58 2006 +0200 (2006-09-12)
changeset 2052005fd007bdeb9
parent 20519 d7ad1217c24a
child 20521 189811b39869
tuned;
doc-src/IsarImplementation/Thy/ML.thy
doc-src/IsarImplementation/Thy/document/ML.tex
doc-src/IsarImplementation/Thy/document/isar.tex
doc-src/IsarImplementation/Thy/document/locale.tex
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/document/proof.tex
doc-src/IsarImplementation/Thy/isar.thy
doc-src/IsarImplementation/Thy/locale.thy
doc-src/IsarImplementation/Thy/logic.thy
doc-src/IsarImplementation/Thy/proof.thy
     1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Tue Sep 12 17:23:34 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue Sep 12 17:45:58 2006 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  chapter {* Basic library functions *}
     1.6  
     1.7 -text {* FIXME beyond the basis library definition *}
     1.8 +text {* FIXME beyond the NJ basis library proposal *}
     1.9  
    1.10  
    1.11  chapter {* Cookbook *}
     2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Tue Sep 12 17:23:34 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Tue Sep 12 17:45:58 2006 +0200
     2.3 @@ -35,7 +35,7 @@
     2.4  \isamarkuptrue%
     2.5  %
     2.6  \begin{isamarkuptext}%
     2.7 -FIXME beyond the basis library definition%
     2.8 +FIXME beyond the NJ basis library proposal%
     2.9  \end{isamarkuptext}%
    2.10  \isamarkuptrue%
    2.11  %
     3.1 --- a/doc-src/IsarImplementation/Thy/document/isar.tex	Tue Sep 12 17:23:34 2006 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/isar.tex	Tue Sep 12 17:45:58 2006 +0200
     3.3 @@ -23,7 +23,16 @@
     3.4  }
     3.5  \isamarkuptrue%
     3.6  %
     3.7 -\isamarkupsection{Proof states \label{sec:isar-proof-state}%
     3.8 +\isamarkupsection{Proof context%
     3.9 +}
    3.10 +\isamarkuptrue%
    3.11 +%
    3.12 +\begin{isamarkuptext}%
    3.13 +FIXME%
    3.14 +\end{isamarkuptext}%
    3.15 +\isamarkuptrue%
    3.16 +%
    3.17 +\isamarkupsection{Proof state \label{sec:isar-proof-state}%
    3.18  }
    3.19  \isamarkuptrue%
    3.20  %
     4.1 --- a/doc-src/IsarImplementation/Thy/document/locale.tex	Tue Sep 12 17:23:34 2006 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/locale.tex	Tue Sep 12 17:45:58 2006 +0200
     4.3 @@ -32,7 +32,7 @@
     4.4  \end{isamarkuptext}%
     4.5  \isamarkuptrue%
     4.6  %
     4.7 -\isamarkupsection{Type-checking specifications%
     4.8 +\isamarkupsection{Type-inference%
     4.9  }
    4.10  \isamarkuptrue%
    4.11  %
     5.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Tue Sep 12 17:23:34 2006 +0200
     5.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Tue Sep 12 17:45:58 2006 +0200
     5.3 @@ -132,9 +132,9 @@
     5.4    \indexml{fold-atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
     5.5    \indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
     5.6    \indexml{Sign.of-sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
     5.7 -  \indexml{Sign.add-types}\verb|Sign.add_types: (bstring * int * mixfix) list -> theory -> theory| \\
     5.8 +  \indexml{Sign.add-types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
     5.9    \indexml{Sign.add-tyabbrs-i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
    5.10 -\verb|  (bstring * string list * typ * mixfix) list -> theory -> theory| \\
    5.11 +\verb|  (string * string list * typ * mixfix) list -> theory -> theory| \\
    5.12    \indexml{Sign.primitive-class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
    5.13    \indexml{Sign.primitive-classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
    5.14    \indexml{Sign.primitive-arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
    5.15 @@ -201,11 +201,11 @@
    5.16  \glossary{Term}{FIXME}
    5.17  
    5.18    The language of terms is that of simply-typed \isa{{\isasymlambda}}-calculus
    5.19 -  with de-Bruijn indices for bound variables
    5.20 -  \cite{debruijn72,paulson-ml2}, and named free variables and
    5.21 -  constants.  Terms with loose bound variables are usually considered
    5.22 -  malformed.  The types of variables and constants is stored
    5.23 -  explicitly at each occurrence in the term.
    5.24 +  with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
    5.25 +  or \cite{paulson-ml2}), and named free variables and constants.
    5.26 +  Terms with loose bound variables are usually considered malformed.
    5.27 +  The types of variables and constants is stored explicitly at each
    5.28 +  occurrence in the term.
    5.29  
    5.30    \medskip A \emph{bound variable} is a natural number \isa{b},
    5.31    which refers to the next binder that is \isa{b} steps upwards
    5.32 @@ -319,9 +319,9 @@
    5.33    \indexml{fastype-of}\verb|fastype_of: term -> typ| \\
    5.34    \indexml{lambda}\verb|lambda: term -> term -> term| \\
    5.35    \indexml{betapply}\verb|betapply: term * term -> term| \\
    5.36 -  \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (bstring * typ * mixfix) list -> theory -> theory| \\
    5.37 +  \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory| \\
    5.38    \indexml{Sign.add-abbrevs}\verb|Sign.add_abbrevs: string * bool ->|\isasep\isanewline%
    5.39 -\verb|  ((bstring * mixfix) * term) list -> theory -> theory| \\
    5.40 +\verb|  ((string * mixfix) * term) list -> theory -> theory| \\
    5.41    \indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
    5.42    \indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
    5.43    \end{mldecls}
    5.44 @@ -356,10 +356,10 @@
    5.45    well-formed term, while omitting any sanity checks.  This operation
    5.46    is relatively slow.
    5.47  
    5.48 -  \item \verb|lambda|~\isa{a\ b} produces an abstraction \isa{{\isasymlambda}a{\isachardot}\ b}, where occurrences of the original (atomic) term \isa{a} are replaced by bound variables.
    5.49 +  \item \verb|lambda|~\isa{a\ b} produces an abstraction \isa{{\isasymlambda}a{\isachardot}\ b}, where occurrences of the original (atomic) term \isa{a} in the body \isa{b} are replaced by bound variables.
    5.50  
    5.51 -  \item \verb|betapply|~\isa{t\ u} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion \isa{t} is an
    5.52 -  abstraction.
    5.53 +  \item \verb|betapply|~\isa{t\ u} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion if \isa{t} happens to
    5.54 +  be an abstraction.
    5.55  
    5.56    \item \verb|Sign.add_consts_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a
    5.57    new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix syntax.
    5.58 @@ -368,11 +368,10 @@
    5.59    declares a new term abbreviation \isa{c\ {\isasymequiv}\ t} with optional
    5.60    mixfix syntax.
    5.61  
    5.62 -  \item \verb|Sign.const_typargs|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} produces the
    5.63 -  type arguments of the instance \isa{c\isactrlisub {\isasymtau}} wrt.\ its
    5.64 -  declaration in the theory.
    5.65 -
    5.66 -  \item \verb|Sign.const_instance|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharbrackright}{\isacharparenright}} produces the full instance \isa{c{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}} wrt.\ its declaration in the theory.
    5.67 +  \item \verb|Sign.const_typargs|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} and \verb|Sign.const_instance|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharbrackright}{\isacharparenright}}
    5.68 +  convert between the two representations of constants, namely full
    5.69 +  type instance vs.\ compact type arguments form (depending on the
    5.70 +  most general declaration given in the context).
    5.71  
    5.72    \end{description}%
    5.73  \end{isamarkuptext}%
    5.74 @@ -481,7 +480,7 @@
    5.75    option to control the generation of full proof terms.
    5.76  
    5.77    \medskip The axiomatization of a theory is implicitly closed by
    5.78 -  forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymtheta}} for
    5.79 +  forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymvartheta}} for
    5.80    any substitution instance of axiom \isa{{\isasymturnstile}\ A}.  By pushing
    5.81    substitution through derivations inductively, we get admissible
    5.82    substitution rules for theorems shown in \figref{fig:subst-rules}.
     6.1 --- a/doc-src/IsarImplementation/Thy/document/proof.tex	Tue Sep 12 17:23:34 2006 +0200
     6.2 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Tue Sep 12 17:45:58 2006 +0200
     6.3 @@ -278,7 +278,7 @@
     6.4  %
     6.5  \endisadelimmlref
     6.6  %
     6.7 -\isamarkupsection{Conclusions%
     6.8 +\isamarkupsection{Results%
     6.9  }
    6.10  \isamarkuptrue%
    6.11  %
     7.1 --- a/doc-src/IsarImplementation/Thy/isar.thy	Tue Sep 12 17:23:34 2006 +0200
     7.2 +++ b/doc-src/IsarImplementation/Thy/isar.thy	Tue Sep 12 17:45:58 2006 +0200
     7.3 @@ -5,7 +5,12 @@
     7.4  
     7.5  chapter {* Isar proof texts *}
     7.6  
     7.7 -section {* Proof states \label{sec:isar-proof-state} *}
     7.8 +section {* Proof context *}
     7.9 +
    7.10 +text FIXME
    7.11 +
    7.12 +
    7.13 +section {* Proof state \label{sec:isar-proof-state} *}
    7.14  
    7.15  text {*
    7.16    FIXME
     8.1 --- a/doc-src/IsarImplementation/Thy/locale.thy	Tue Sep 12 17:23:34 2006 +0200
     8.2 +++ b/doc-src/IsarImplementation/Thy/locale.thy	Tue Sep 12 17:45:58 2006 +0200
     8.3 @@ -10,7 +10,7 @@
     8.4  text FIXME
     8.5  
     8.6  
     8.7 -section {* Type-checking specifications *}
     8.8 +section {* Type-inference *}
     8.9  
    8.10  text FIXME
    8.11  
     9.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 12 17:23:34 2006 +0200
     9.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 12 17:45:58 2006 +0200
     9.3 @@ -126,9 +126,9 @@
     9.4    @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
     9.5    @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
     9.6    @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
     9.7 -  @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
     9.8 +  @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
     9.9    @{index_ML Sign.add_tyabbrs_i: "
    9.10 -  (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
    9.11 +  (string * string list * typ * mixfix) list -> theory -> theory"} \\
    9.12    @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
    9.13    @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
    9.14    @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
    9.15 @@ -192,11 +192,11 @@
    9.16    \glossary{Term}{FIXME}
    9.17  
    9.18    The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
    9.19 -  with de-Bruijn indices for bound variables
    9.20 -  \cite{debruijn72,paulson-ml2}, and named free variables and
    9.21 -  constants.  Terms with loose bound variables are usually considered
    9.22 -  malformed.  The types of variables and constants is stored
    9.23 -  explicitly at each occurrence in the term.
    9.24 +  with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
    9.25 +  or \cite{paulson-ml2}), and named free variables and constants.
    9.26 +  Terms with loose bound variables are usually considered malformed.
    9.27 +  The types of variables and constants is stored explicitly at each
    9.28 +  occurrence in the term.
    9.29  
    9.30    \medskip A \emph{bound variable} is a natural number @{text "b"},
    9.31    which refers to the next binder that is @{text "b"} steps upwards
    9.32 @@ -317,9 +317,9 @@
    9.33    @{index_ML fastype_of: "term -> typ"} \\
    9.34    @{index_ML lambda: "term -> term -> term"} \\
    9.35    @{index_ML betapply: "term * term -> term"} \\
    9.36 -  @{index_ML Sign.add_consts_i: "(bstring * typ * mixfix) list -> theory -> theory"} \\
    9.37 +  @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
    9.38    @{index_ML Sign.add_abbrevs: "string * bool ->
    9.39 -  ((bstring * mixfix) * term) list -> theory -> theory"} \\
    9.40 +  ((string * mixfix) * term) list -> theory -> theory"} \\
    9.41    @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
    9.42    @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
    9.43    \end{mldecls}
    9.44 @@ -358,11 +358,11 @@
    9.45  
    9.46    \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
    9.47    "\<lambda>a. b"}, where occurrences of the original (atomic) term @{text
    9.48 -  "a"} are replaced by bound variables.
    9.49 +  "a"} in the body @{text "b"} are replaced by bound variables.
    9.50  
    9.51    \item @{ML betapply}~@{text "t u"} produces an application @{text "t
    9.52 -  u"}, with topmost @{text "\<beta>"}-conversion @{text "t"} is an
    9.53 -  abstraction.
    9.54 +  u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} happens to
    9.55 +  be an abstraction.
    9.56  
    9.57    \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
    9.58    new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
    9.59 @@ -371,13 +371,11 @@
    9.60    declares a new term abbreviation @{text "c \<equiv> t"} with optional
    9.61    mixfix syntax.
    9.62  
    9.63 -  \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} produces the
    9.64 -  type arguments of the instance @{text "c\<^isub>\<tau>"} wrt.\ its
    9.65 -  declaration in the theory.
    9.66 -
    9.67 -  \item @{ML Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>,
    9.68 -  \<tau>\<^isub>n])"} produces the full instance @{text "c(\<tau>\<^isub>1, \<dots>,
    9.69 -  \<tau>\<^isub>n)"} wrt.\ its declaration in the theory.
    9.70 +  \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
    9.71 +  Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
    9.72 +  convert between the two representations of constants, namely full
    9.73 +  type instance vs.\ compact type arguments form (depending on the
    9.74 +  most general declaration given in the context).
    9.75  
    9.76    \end{description}
    9.77  *}
    9.78 @@ -479,7 +477,7 @@
    9.79    option to control the generation of full proof terms.
    9.80  
    9.81    \medskip The axiomatization of a theory is implicitly closed by
    9.82 -  forming all instances of type and term variables: @{text "\<turnstile> A\<theta>"} for
    9.83 +  forming all instances of type and term variables: @{text "\<turnstile> A\<vartheta>"} for
    9.84    any substitution instance of axiom @{text "\<turnstile> A"}.  By pushing
    9.85    substitution through derivations inductively, we get admissible
    9.86    substitution rules for theorems shown in \figref{fig:subst-rules}.
    10.1 --- a/doc-src/IsarImplementation/Thy/proof.thy	Tue Sep 12 17:23:34 2006 +0200
    10.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy	Tue Sep 12 17:45:58 2006 +0200
    10.3 @@ -247,7 +247,7 @@
    10.4  *}
    10.5  
    10.6  
    10.7 -section {* Conclusions *}
    10.8 +section {* Results *}
    10.9  
   10.10  text {*
   10.11    Local results are established by monotonic reasoning from facts