doc-src/IsarImplementation/Thy/logic.thy
changeset 20547 796ae7fa1049
parent 20543 dc294418ff17
child 20929 cd2a6d00ec47
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 15 20:08:38 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 15 22:56:08 2006 +0200
     1.3 @@ -123,6 +123,8 @@
     1.4    @{index_ML_type typ} \\
     1.5    @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\
     1.6    @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
     1.7 +  \end{mldecls}
     1.8 +  \begin{mldecls}
     1.9    @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
    1.10    @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
    1.11    @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
    1.12 @@ -315,10 +317,12 @@
    1.13    \begin{mldecls}
    1.14    @{index_ML_type term} \\
    1.15    @{index_ML "op aconv": "term * term -> bool"} \\
    1.16 -  @{index_ML map_term_types: "(typ -> typ) -> term -> term"} \\  %FIXME rename map_types
    1.17 +  @{index_ML map_types: "(typ -> typ) -> term -> term"} \\
    1.18    @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
    1.19    @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
    1.20    @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
    1.21 +  \end{mldecls}
    1.22 +  \begin{mldecls}
    1.23    @{index_ML fastype_of: "term -> typ"} \\
    1.24    @{index_ML lambda: "term -> term -> term"} \\
    1.25    @{index_ML betapply: "term * term -> term"} \\
    1.26 @@ -341,7 +345,7 @@
    1.27    on type @{ML_type term}; raw datatype equality should only be used
    1.28    for operations related to parsing or printing!
    1.29  
    1.30 -  \item @{ML map_term_types}~@{text "f t"} applies the mapping @{text
    1.31 +  \item @{ML map_types}~@{text "f t"} applies the mapping @{text
    1.32    "f"} to all types occurring in @{text "t"}.
    1.33  
    1.34    \item @{ML fold_types}~@{text "f t"} iterates the operation @{text
    1.35 @@ -576,10 +580,12 @@
    1.36    \begin{mldecls}
    1.37    @{index_ML_type ctyp} \\
    1.38    @{index_ML_type cterm} \\
    1.39 +  @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
    1.40 +  @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
    1.41 +  \end{mldecls}
    1.42 +  \begin{mldecls}
    1.43    @{index_ML_type thm} \\
    1.44    @{index_ML proofs: "int ref"} \\
    1.45 -  @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
    1.46 -  @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
    1.47    @{index_ML Thm.assume: "cterm -> thm"} \\
    1.48    @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
    1.49    @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
    1.50 @@ -589,6 +595,8 @@
    1.51    @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
    1.52    @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
    1.53    @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
    1.54 +  \end{mldecls}
    1.55 +  \begin{mldecls}
    1.56    @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
    1.57    @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
    1.58    @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
    1.59 @@ -603,9 +611,14 @@
    1.60    well-typedness) checks, relative to the declarations of type
    1.61    constructors, constants etc. in the theory.
    1.62  
    1.63 -  This representation avoids syntactic rechecking in tight loops of
    1.64 -  inferences.  There are separate operations to decompose certified
    1.65 -  entities (including actual theorems).
    1.66 +  \item @{ML ctyp_of}~@{text "thy \<tau>"} and @{ML cterm_of}~@{text "thy
    1.67 +  t"} explicitly checks types and terms, respectively.  This also
    1.68 +  involves some basic normalizations, such expansion of type and term
    1.69 +  abbreviations from the theory context.
    1.70 +
    1.71 +  Re-certification is relatively slow and should be avoided in tight
    1.72 +  reasoning loops.  There are separate operations to decompose
    1.73 +  certified entities (including actual theorems).
    1.74  
    1.75    \item @{ML_type thm} represents proven propositions.  This is an
    1.76    abstract datatype that guarantees that its values have been