doc-src/IsarImplementation/Thy/logic.thy
changeset 20542 a54ca4e90874
parent 20537 b6b49903db7e
child 20543 dc294418ff17
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 14 21:42:21 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 14 22:48:37 2006 +0200
     1.3 @@ -489,7 +489,7 @@
     1.4    @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
     1.5    @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\
     1.6    \end{tabular}
     1.7 -  \caption{Conceptual axiomatization of @{text "\<equiv>"}}\label{fig:pure-equality}
     1.8 +  \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
     1.9    \end{center}
    1.10    \end{figure}
    1.11  
    1.12 @@ -512,12 +512,6 @@
    1.13    \cite{Barendregt-Geuvers:2001}, where @{text "x : A"} hypotheses are
    1.14    treated explicitly for types, in the same way as propositions.}
    1.15  
    1.16 -  \medskip FIXME @{text "\<alpha>\<beta>\<eta>"}-equivalence and primitive definitions
    1.17 -
    1.18 -  Since the basic representation of terms already accounts for @{text
    1.19 -  "\<alpha>"}-conversion, Pure equality essentially acts like @{text
    1.20 -  "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
    1.21 -
    1.22    \medskip The axiomatization of a theory is implicitly closed by
    1.23    forming all instances of type and term variables: @{text "\<turnstile>
    1.24    A\<vartheta>"} holds for any substitution instance of an axiom
    1.25 @@ -550,6 +544,34 @@
    1.26    "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is correct, but
    1.27    @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold --- the result
    1.28    belongs to a different proof context.
    1.29 +
    1.30 +  \medskip The system allows axioms to be stated either as plain
    1.31 +  propositions, or as arbitrary functions (``oracles'') that produce
    1.32 +  propositions depending on given arguments.  It is possible to trace
    1.33 +  the used of axioms (and defined theorems) in derivations.
    1.34 +  Invocations of oracles are recorded invariable.
    1.35 +
    1.36 +  Axiomatizations should be limited to the bare minimum, typically as
    1.37 +  part of the initial logical basis of an object-logic formalization.
    1.38 +  Normally, theories will be developed definitionally, by stating
    1.39 +  restricted equalities over constants.
    1.40 +
    1.41 +  A \emph{simple definition} consists of a constant declaration @{text
    1.42 +  "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text
    1.43 +  "t"} is a closed term without any hidden polymorphism.  The RHS may
    1.44 +  depend on further defined constants, but not @{text "c"} itself.
    1.45 +  Definitions of constants with function type may be presented
    1.46 +  liberally as @{text "c \<^vec> \<equiv> t"} instead of the puristic @{text
    1.47 +  "c \<equiv> \<lambda>\<^vec>x. t"}.
    1.48 +
    1.49 +  An \emph{overloaded definition} consists may give zero or one
    1.50 +  equality axioms @{text "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type
    1.51 +  constructor @{text "\<kappa>"}, with distinct variables @{text "\<^vec>\<alpha>"}
    1.52 +  as formal arguments.  The RHS may mention previously defined
    1.53 +  constants as above, or arbitrary constants @{text "d(\<alpha>\<^isub>i)"}
    1.54 +  for some @{text "\<alpha>\<^isub>i"} projected from @{text "\<^vec>\<alpha>"}.
    1.55 +  Thus overloaded definitions essentially work by primitive recursion
    1.56 +  over the syntactic structure of a single type argument.
    1.57  *}
    1.58  
    1.59  text %mlref {*
    1.60 @@ -557,15 +579,83 @@
    1.61    @{index_ML_type ctyp} \\
    1.62    @{index_ML_type cterm} \\
    1.63    @{index_ML_type thm} \\
    1.64 +  @{index_ML proofs: "int ref"} \\
    1.65 +  @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
    1.66 +  @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
    1.67 +  @{index_ML Thm.assume: "cterm -> thm"} \\
    1.68 +  @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
    1.69 +  @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
    1.70 +  @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
    1.71 +  @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
    1.72 +  @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
    1.73 +  @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
    1.74 +  @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
    1.75 +  @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
    1.76 +  @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
    1.77 +  @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
    1.78 +  @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
    1.79 +  @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
    1.80    \end{mldecls}
    1.81  
    1.82    \begin{description}
    1.83  
    1.84 -  \item @{ML_type ctyp} FIXME
    1.85 +  \item @{ML_type ctyp} and @{ML_type cterm} represent certified types
    1.86 +  and terms, respectively.  These are abstract datatypes that
    1.87 +  guarantee that its values have passed the full well-formedness (and
    1.88 +  well-typedness) checks, relative to the declarations of type
    1.89 +  constructors, constants etc. in the theory.
    1.90 +
    1.91 +  This representation avoids syntactic rechecking in tight loops of
    1.92 +  inferences.  There are separate operations to decompose certified
    1.93 +  entities (including actual theorems).
    1.94 +
    1.95 +  \item @{ML_type thm} represents proven propositions.  This is an
    1.96 +  abstract datatype that guarantees that its values have been
    1.97 +  constructed by basic principles of the @{ML_struct Thm} module.
    1.98 +
    1.99 +  \item @{ML proofs} determines the detail of proof recording: @{ML 0}
   1.100 +  records only oracles, @{ML 1} records oracles, axioms and named
   1.101 +  theorems, @{ML 2} records full proof terms.
   1.102 +
   1.103 +  \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
   1.104 +  Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
   1.105 +  correspond to the primitive inferences of \figref{fig:prim-rules}.
   1.106 +
   1.107 +  \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}
   1.108 +  corresponds to the @{text "generalize"} rules of
   1.109 +  \figref{fig:subst-rules}.  A collection of type and term variables
   1.110 +  is generalized simultaneously, according to the given basic names.
   1.111  
   1.112 -  \item @{ML_type cterm} FIXME
   1.113 +  \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,
   1.114 +  \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules
   1.115 +  of \figref{fig:subst-rules}.  Type variables are substituted before
   1.116 +  term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
   1.117 +  refer to the instantiated versions.
   1.118 +
   1.119 +  \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
   1.120 +  axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
   1.121 +
   1.122 +  \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes the
   1.123 +  oracle function @{text "name"} of the theory.  Logically, this is
   1.124 +  just another instance of @{text "axiom"} in \figref{fig:prim-rules},
   1.125 +  but the system records an explicit trace of oracle invocations with
   1.126 +  the @{text "thm"} value.
   1.127  
   1.128 -  \item @{ML_type thm} FIXME
   1.129 +  \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} adds
   1.130 +  arbitrary axioms, without any checking of the proposition.
   1.131 +
   1.132 +  \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an
   1.133 +  oracle, i.e.\ a function for generating arbitrary axioms.
   1.134 +
   1.135 +  \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
   1.136 +  \<^vec>d\<^isub>\<sigma>"} declares dependencies of a new specification for
   1.137 +  constant @{text "c\<^isub>\<tau>"} from relative to existing ones for
   1.138 +  constants @{text "\<^vec>d\<^isub>\<sigma>"}.
   1.139 +
   1.140 +  \item @{ML Theory.add_defs_i}~@{text "unchecked overloaded [(name, c
   1.141 +  \<^vec>x \<equiv> t), \<dots>]"} states a definitional axiom for an already
   1.142 +  declared constant @{text "c"}.  Dependencies are recorded using @{ML
   1.143 +  Theory.add_deps}, unless the @{text "unchecked"} option is set.
   1.144  
   1.145    \end{description}
   1.146  *}
   1.147 @@ -640,7 +730,22 @@
   1.148  
   1.149    \begin{description}
   1.150  
   1.151 -  \item FIXME
   1.152 +  \item @{ML Conjunction.intr} derives @{text "A & B"} from @{text
   1.153 +  "A"} and @{text "B"}.
   1.154 +
   1.155 +  \item @{ML Conjunction.intr} derives @{text "A"} and @{text "B"}
   1.156 +  from @{text "A & B"}.
   1.157 +
   1.158 +  \item @{ML Drule.mk_term}~@{text "t"} derives @{text "TERM t"}.
   1.159 +
   1.160 +  \item @{ML Drule.dest_term}~@{text "TERM t"} recovers term @{text
   1.161 +  "t"}.
   1.162 +
   1.163 +  \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text
   1.164 +  "TYPE(\<tau>)"}.
   1.165 +
   1.166 +  \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type
   1.167 +  @{text "\<tau>"}.
   1.168  
   1.169    \end{description}
   1.170  *}