# HG changeset patch # User wenzelm # Date 1158075958 -7200 # Node ID 05fd007bdeb912252416b6904c135293fdcdc2d7 # Parent d7ad1217c24a8c58aacc1de16e76fac9b1291769 tuned; diff -r d7ad1217c24a -r 05fd007bdeb9 doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Tue Sep 12 17:23:34 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/ML.thy Tue Sep 12 17:45:58 2006 +0200 @@ -13,7 +13,7 @@ chapter {* Basic library functions *} -text {* FIXME beyond the basis library definition *} +text {* FIXME beyond the NJ basis library proposal *} chapter {* Cookbook *} diff -r d7ad1217c24a -r 05fd007bdeb9 doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue Sep 12 17:23:34 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue Sep 12 17:45:58 2006 +0200 @@ -35,7 +35,7 @@ \isamarkuptrue% % \begin{isamarkuptext}% -FIXME beyond the basis library definition% +FIXME beyond the NJ basis library proposal% \end{isamarkuptext}% \isamarkuptrue% % diff -r d7ad1217c24a -r 05fd007bdeb9 doc-src/IsarImplementation/Thy/document/isar.tex --- a/doc-src/IsarImplementation/Thy/document/isar.tex Tue Sep 12 17:23:34 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/isar.tex Tue Sep 12 17:45:58 2006 +0200 @@ -23,7 +23,16 @@ } \isamarkuptrue% % -\isamarkupsection{Proof states \label{sec:isar-proof-state}% +\isamarkupsection{Proof context% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +FIXME% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Proof state \label{sec:isar-proof-state}% } \isamarkuptrue% % diff -r d7ad1217c24a -r 05fd007bdeb9 doc-src/IsarImplementation/Thy/document/locale.tex --- a/doc-src/IsarImplementation/Thy/document/locale.tex Tue Sep 12 17:23:34 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/locale.tex Tue Sep 12 17:45:58 2006 +0200 @@ -32,7 +32,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsection{Type-checking specifications% +\isamarkupsection{Type-inference% } \isamarkuptrue% % diff -r d7ad1217c24a -r 05fd007bdeb9 doc-src/IsarImplementation/Thy/document/logic.tex --- a/doc-src/IsarImplementation/Thy/document/logic.tex Tue Sep 12 17:23:34 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex Tue Sep 12 17:45:58 2006 +0200 @@ -132,9 +132,9 @@ \indexml{fold-atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\ \indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\ \indexml{Sign.of-sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\ - \indexml{Sign.add-types}\verb|Sign.add_types: (bstring * int * mixfix) list -> theory -> theory| \\ + \indexml{Sign.add-types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\ \indexml{Sign.add-tyabbrs-i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline% -\verb| (bstring * string list * typ * mixfix) list -> theory -> theory| \\ +\verb| (string * string list * typ * mixfix) list -> theory -> theory| \\ \indexml{Sign.primitive-class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\ \indexml{Sign.primitive-classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\ \indexml{Sign.primitive-arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\ @@ -201,11 +201,11 @@ \glossary{Term}{FIXME} The language of terms is that of simply-typed \isa{{\isasymlambda}}-calculus - with de-Bruijn indices for bound variables - \cite{debruijn72,paulson-ml2}, and named free variables and - constants. Terms with loose bound variables are usually considered - malformed. The types of variables and constants is stored - explicitly at each occurrence in the term. + with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72} + or \cite{paulson-ml2}), and named free variables and constants. + Terms with loose bound variables are usually considered malformed. + The types of variables and constants is stored explicitly at each + occurrence in the term. \medskip A \emph{bound variable} is a natural number \isa{b}, which refers to the next binder that is \isa{b} steps upwards @@ -319,9 +319,9 @@ \indexml{fastype-of}\verb|fastype_of: term -> typ| \\ \indexml{lambda}\verb|lambda: term -> term -> term| \\ \indexml{betapply}\verb|betapply: term * term -> term| \\ - \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (bstring * typ * mixfix) list -> theory -> theory| \\ + \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory| \\ \indexml{Sign.add-abbrevs}\verb|Sign.add_abbrevs: string * bool ->|\isasep\isanewline% -\verb| ((bstring * mixfix) * term) list -> theory -> theory| \\ +\verb| ((string * mixfix) * term) list -> theory -> theory| \\ \indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\ \indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\ \end{mldecls} @@ -356,10 +356,10 @@ well-formed term, while omitting any sanity checks. This operation is relatively slow. - \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. + \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. - \item \verb|betapply|~\isa{t\ u} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion \isa{t} is an - abstraction. + \item \verb|betapply|~\isa{t\ u} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion if \isa{t} happens to + be an abstraction. \item \verb|Sign.add_consts_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix syntax. @@ -368,11 +368,10 @@ declares a new term abbreviation \isa{c\ {\isasymequiv}\ t} with optional mixfix syntax. - \item \verb|Sign.const_typargs|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} produces the - type arguments of the instance \isa{c\isactrlisub {\isasymtau}} wrt.\ its - declaration in the theory. - - \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. + \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}} + convert between the two representations of constants, namely full + type instance vs.\ compact type arguments form (depending on the + most general declaration given in the context). \end{description}% \end{isamarkuptext}% @@ -481,7 +480,7 @@ option to control the generation of full proof terms. \medskip The axiomatization of a theory is implicitly closed by - forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymtheta}} for + forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymvartheta}} for any substitution instance of axiom \isa{{\isasymturnstile}\ A}. By pushing substitution through derivations inductively, we get admissible substitution rules for theorems shown in \figref{fig:subst-rules}. diff -r d7ad1217c24a -r 05fd007bdeb9 doc-src/IsarImplementation/Thy/document/proof.tex --- a/doc-src/IsarImplementation/Thy/document/proof.tex Tue Sep 12 17:23:34 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex Tue Sep 12 17:45:58 2006 +0200 @@ -278,7 +278,7 @@ % \endisadelimmlref % -\isamarkupsection{Conclusions% +\isamarkupsection{Results% } \isamarkuptrue% % diff -r d7ad1217c24a -r 05fd007bdeb9 doc-src/IsarImplementation/Thy/isar.thy --- a/doc-src/IsarImplementation/Thy/isar.thy Tue Sep 12 17:23:34 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/isar.thy Tue Sep 12 17:45:58 2006 +0200 @@ -5,7 +5,12 @@ chapter {* Isar proof texts *} -section {* Proof states \label{sec:isar-proof-state} *} +section {* Proof context *} + +text FIXME + + +section {* Proof state \label{sec:isar-proof-state} *} text {* FIXME diff -r d7ad1217c24a -r 05fd007bdeb9 doc-src/IsarImplementation/Thy/locale.thy --- a/doc-src/IsarImplementation/Thy/locale.thy Tue Sep 12 17:23:34 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/locale.thy Tue Sep 12 17:45:58 2006 +0200 @@ -10,7 +10,7 @@ text FIXME -section {* Type-checking specifications *} +section {* Type-inference *} text FIXME diff -r d7ad1217c24a -r 05fd007bdeb9 doc-src/IsarImplementation/Thy/logic.thy --- a/doc-src/IsarImplementation/Thy/logic.thy Tue Sep 12 17:23:34 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/logic.thy Tue Sep 12 17:45:58 2006 +0200 @@ -126,9 +126,9 @@ @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\ @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\ @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\ - @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\ + @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\ @{index_ML Sign.add_tyabbrs_i: " - (bstring * string list * typ * mixfix) list -> theory -> theory"} \\ + (string * string list * typ * mixfix) list -> theory -> theory"} \\ @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\ @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\ @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\ @@ -192,11 +192,11 @@ \glossary{Term}{FIXME} The language of terms is that of simply-typed @{text "\"}-calculus - with de-Bruijn indices for bound variables - \cite{debruijn72,paulson-ml2}, and named free variables and - constants. Terms with loose bound variables are usually considered - malformed. The types of variables and constants is stored - explicitly at each occurrence in the term. + with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72} + or \cite{paulson-ml2}), and named free variables and constants. + Terms with loose bound variables are usually considered malformed. + The types of variables and constants is stored explicitly at each + occurrence in the term. \medskip A \emph{bound variable} is a natural number @{text "b"}, which refers to the next binder that is @{text "b"} steps upwards @@ -317,9 +317,9 @@ @{index_ML fastype_of: "term -> typ"} \\ @{index_ML lambda: "term -> term -> term"} \\ @{index_ML betapply: "term * term -> term"} \\ - @{index_ML Sign.add_consts_i: "(bstring * typ * mixfix) list -> theory -> theory"} \\ + @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\ @{index_ML Sign.add_abbrevs: "string * bool -> - ((bstring * mixfix) * term) list -> theory -> theory"} \\ + ((string * mixfix) * term) list -> theory -> theory"} \\ @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\ @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\ \end{mldecls} @@ -358,11 +358,11 @@ \item @{ML lambda}~@{text "a b"} produces an abstraction @{text "\a. b"}, where occurrences of the original (atomic) term @{text - "a"} are replaced by bound variables. + "a"} in the body @{text "b"} are replaced by bound variables. \item @{ML betapply}~@{text "t u"} produces an application @{text "t - u"}, with topmost @{text "\"}-conversion @{text "t"} is an - abstraction. + u"}, with topmost @{text "\"}-conversion if @{text "t"} happens to + be an abstraction. \item @{ML Sign.add_consts_i}~@{text "[(c, \, mx), \]"} declares a new constant @{text "c :: \"} with optional mixfix syntax. @@ -371,13 +371,11 @@ declares a new term abbreviation @{text "c \ t"} with optional mixfix syntax. - \item @{ML Sign.const_typargs}~@{text "thy (c, \)"} produces the - type arguments of the instance @{text "c\<^isub>\"} wrt.\ its - declaration in the theory. - - \item @{ML Sign.const_instance}~@{text "thy (c, [\\<^isub>1, \, - \\<^isub>n])"} produces the full instance @{text "c(\\<^isub>1, \, - \\<^isub>n)"} wrt.\ its declaration in the theory. + \item @{ML Sign.const_typargs}~@{text "thy (c, \)"} and @{ML + Sign.const_instance}~@{text "thy (c, [\\<^isub>1, \, \\<^isub>n])"} + convert between the two representations of constants, namely full + type instance vs.\ compact type arguments form (depending on the + most general declaration given in the context). \end{description} *} @@ -479,7 +477,7 @@ option to control the generation of full proof terms. \medskip The axiomatization of a theory is implicitly closed by - forming all instances of type and term variables: @{text "\ A\"} for + forming all instances of type and term variables: @{text "\ A\"} for any substitution instance of axiom @{text "\ A"}. By pushing substitution through derivations inductively, we get admissible substitution rules for theorems shown in \figref{fig:subst-rules}. diff -r d7ad1217c24a -r 05fd007bdeb9 doc-src/IsarImplementation/Thy/proof.thy --- a/doc-src/IsarImplementation/Thy/proof.thy Tue Sep 12 17:23:34 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/proof.thy Tue Sep 12 17:45:58 2006 +0200 @@ -247,7 +247,7 @@ *} -section {* Conclusions *} +section {* Results *} text {* Local results are established by monotonic reasoning from facts