doc-src/IsarImplementation/Thy/logic.thy
changeset 20520 05fd007bdeb9
parent 20519 d7ad1217c24a
child 20521 189811b39869
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 12 17:23:34 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 12 17:45:58 2006 +0200
     1.3 @@ -126,9 +126,9 @@
     1.4    @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
     1.5    @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
     1.6    @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
     1.7 -  @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
     1.8 +  @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
     1.9    @{index_ML Sign.add_tyabbrs_i: "
    1.10 -  (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
    1.11 +  (string * string list * typ * mixfix) list -> theory -> theory"} \\
    1.12    @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
    1.13    @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
    1.14    @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
    1.15 @@ -192,11 +192,11 @@
    1.16    \glossary{Term}{FIXME}
    1.17  
    1.18    The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
    1.19 -  with de-Bruijn indices for bound variables
    1.20 -  \cite{debruijn72,paulson-ml2}, and named free variables and
    1.21 -  constants.  Terms with loose bound variables are usually considered
    1.22 -  malformed.  The types of variables and constants is stored
    1.23 -  explicitly at each occurrence in the term.
    1.24 +  with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
    1.25 +  or \cite{paulson-ml2}), and named free variables and constants.
    1.26 +  Terms with loose bound variables are usually considered malformed.
    1.27 +  The types of variables and constants is stored explicitly at each
    1.28 +  occurrence in the term.
    1.29  
    1.30    \medskip A \emph{bound variable} is a natural number @{text "b"},
    1.31    which refers to the next binder that is @{text "b"} steps upwards
    1.32 @@ -317,9 +317,9 @@
    1.33    @{index_ML fastype_of: "term -> typ"} \\
    1.34    @{index_ML lambda: "term -> term -> term"} \\
    1.35    @{index_ML betapply: "term * term -> term"} \\
    1.36 -  @{index_ML Sign.add_consts_i: "(bstring * typ * mixfix) list -> theory -> theory"} \\
    1.37 +  @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
    1.38    @{index_ML Sign.add_abbrevs: "string * bool ->
    1.39 -  ((bstring * mixfix) * term) list -> theory -> theory"} \\
    1.40 +  ((string * mixfix) * term) list -> theory -> theory"} \\
    1.41    @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
    1.42    @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
    1.43    \end{mldecls}
    1.44 @@ -358,11 +358,11 @@
    1.45  
    1.46    \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
    1.47    "\<lambda>a. b"}, where occurrences of the original (atomic) term @{text
    1.48 -  "a"} are replaced by bound variables.
    1.49 +  "a"} in the body @{text "b"} are replaced by bound variables.
    1.50  
    1.51    \item @{ML betapply}~@{text "t u"} produces an application @{text "t
    1.52 -  u"}, with topmost @{text "\<beta>"}-conversion @{text "t"} is an
    1.53 -  abstraction.
    1.54 +  u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} happens to
    1.55 +  be an abstraction.
    1.56  
    1.57    \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
    1.58    new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
    1.59 @@ -371,13 +371,11 @@
    1.60    declares a new term abbreviation @{text "c \<equiv> t"} with optional
    1.61    mixfix syntax.
    1.62  
    1.63 -  \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} produces the
    1.64 -  type arguments of the instance @{text "c\<^isub>\<tau>"} wrt.\ its
    1.65 -  declaration in the theory.
    1.66 -
    1.67 -  \item @{ML Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>,
    1.68 -  \<tau>\<^isub>n])"} produces the full instance @{text "c(\<tau>\<^isub>1, \<dots>,
    1.69 -  \<tau>\<^isub>n)"} wrt.\ its declaration in the theory.
    1.70 +  \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
    1.71 +  Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
    1.72 +  convert between the two representations of constants, namely full
    1.73 +  type instance vs.\ compact type arguments form (depending on the
    1.74 +  most general declaration given in the context).
    1.75  
    1.76    \end{description}
    1.77  *}
    1.78 @@ -479,7 +477,7 @@
    1.79    option to control the generation of full proof terms.
    1.80  
    1.81    \medskip The axiomatization of a theory is implicitly closed by
    1.82 -  forming all instances of type and term variables: @{text "\<turnstile> A\<theta>"} for
    1.83 +  forming all instances of type and term variables: @{text "\<turnstile> A\<vartheta>"} for
    1.84    any substitution instance of axiom @{text "\<turnstile> A"}.  By pushing
    1.85    substitution through derivations inductively, we get admissible
    1.86    substitution rules for theorems shown in \figref{fig:subst-rules}.