author wenzelm Thu, 14 Sep 2006 22:48:37 +0200 changeset 20542 a54ca4e90874 parent 20541 f614c619b1e1 child 20543 dc294418ff17
more on theorems;
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Sep 14 21:42:21 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Sep 14 22:48:37 2006 +0200
@@ -493,7 +493,7 @@
\isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ f\ x\ {\isasymequiv}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isasymequiv}\ g} & extensionality \\
\isa{{\isasymturnstile}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymequiv}\ B} & logical equivalence \\
\end{tabular}
-  \caption{Conceptual axiomatization of \isa{{\isasymequiv}}}\label{fig:pure-equality}
+  \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
\end{center}
\end{figure}

@@ -512,10 +512,6 @@
\cite{Barendregt-Geuvers:2001}, where \isa{x\ {\isacharcolon}\ A} hypotheses are
treated explicitly for types, in the same way as propositions.}

-  \medskip FIXME \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-equivalence and primitive definitions
-
-  Since the basic representation of terms already accounts for \isa{{\isasymalpha}}-conversion, Pure equality essentially acts like \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-equivalence on terms, while coinciding with bi-implication.
-
\medskip The axiomatization of a theory is implicitly closed by
forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymvartheta}} holds for any substitution instance of an axiom
\isa{{\isasymturnstile}\ A}.  By pushing substitution through derivations
@@ -544,7 +540,32 @@
In principle, variables could be substituted in hypotheses as well,
but this would disrupt monotonicity reasoning: deriving \isa{{\isasymGamma}{\isasymvartheta}\ {\isasymturnstile}\ B{\isasymvartheta}} from \isa{{\isasymGamma}\ {\isasymturnstile}\ B} is correct, but
\isa{{\isasymGamma}{\isasymvartheta}\ {\isasymsupseteq}\ {\isasymGamma}} does not necessarily hold --- the result
-  belongs to a different proof context.%
+  belongs to a different proof context.
+
+  \medskip The system allows axioms to be stated either as plain
+  propositions, or as arbitrary functions (oracles'') that produce
+  propositions depending on given arguments.  It is possible to trace
+  the used of axioms (and defined theorems) in derivations.
+  Invocations of oracles are recorded invariable.
+
+  Axiomatizations should be limited to the bare minimum, typically as
+  part of the initial logical basis of an object-logic formalization.
+  Normally, theories will be developed definitionally, by stating
+  restricted equalities over constants.
+
+  A \emph{simple definition} consists of a constant declaration \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} together with an axiom \isa{{\isasymturnstile}\ c\ {\isasymequiv}\ t}, where \isa{t} is a closed term without any hidden polymorphism.  The RHS may
+  depend on further defined constants, but not \isa{c} itself.
+  Definitions of constants with function type may be presented
+  liberally as \isa{c\ \isactrlvec \ {\isasymequiv}\ t} instead of the puristic \isa{c\ {\isasymequiv}\ {\isasymlambda}\isactrlvec x{\isachardot}\ t}.
+
+  An \emph{overloaded definition} consists may give zero or one
+  equality axioms \isa{c{\isacharparenleft}{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}{\isacharparenright}\ {\isasymequiv}\ t} for each type
+  constructor \isa{{\isasymkappa}}, with distinct variables \isa{\isactrlvec {\isasymalpha}}
+  as formal arguments.  The RHS may mention previously defined
+  constants as above, or arbitrary constants \isa{d{\isacharparenleft}{\isasymalpha}\isactrlisub i{\isacharparenright}}
+  for some \isa{{\isasymalpha}\isactrlisub i} projected from \isa{\isactrlvec {\isasymalpha}}.
+  Thus overloaded definitions essentially work by primitive recursion
+  over the syntactic structure of a single type argument.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -559,15 +580,78 @@
\indexmltype{ctyp}\verb|type ctyp| \\
\indexmltype{cterm}\verb|type cterm| \\
\indexmltype{thm}\verb|type thm| \\
+  \indexml{proofs}\verb|proofs: int ref| \\
+  \indexml{Thm.ctyp-of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
+  \indexml{Thm.cterm-of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
+  \indexml{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
+  \indexml{Thm.forall-intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
+  \indexml{Thm.forall-elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
+  \indexml{Thm.implies-intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
+  \indexml{Thm.implies-elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
+  \indexml{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
+  \indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
+  \indexml{Thm.get-axiom-i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\
+  \indexml{Thm.invoke-oracle-i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\
+  \indexml{Theory.add-deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
+  \indexml{Theory.add-oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\
+  \indexml{Theory.add-defs-i}\verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory| \\
\end{mldecls}

\begin{description}

-  \item \verb|ctyp| FIXME
+  \item \verb|ctyp| and \verb|cterm| represent certified types
+  and terms, respectively.  These are abstract datatypes that
+  guarantee that its values have passed the full well-formedness (and
+  well-typedness) checks, relative to the declarations of type
+  constructors, constants etc. in the theory.
+
+  This representation avoids syntactic rechecking in tight loops of
+  inferences.  There are separate operations to decompose certified
+  entities (including actual theorems).
+
+  \item \verb|thm| represents proven propositions.  This is an
+  abstract datatype that guarantees that its values have been
+  constructed by basic principles of the \verb|Thm| module.
+
+  \item \verb|proofs| determines the detail of proof recording: \verb|0|
+  records only oracles, \verb|1| records oracles, axioms and named
+  theorems, \verb|2| records full proof terms.
+
+  \item \verb|Thm.assume|, \verb|Thm.forall_intr|, \verb|Thm.forall_elim|, \verb|Thm.implies_intr|, and \verb|Thm.implies_elim|
+  correspond to the primitive inferences of \figref{fig:prim-rules}.
+
+  \item \verb|Thm.generalize|~\isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharcomma}\ \isactrlvec x{\isacharparenright}}
+  corresponds to the \isa{generalize} rules of
+  \figref{fig:subst-rules}.  A collection of type and term variables
+  is generalized simultaneously, according to the given basic names.

-  \item \verb|cterm| FIXME
+  \item \verb|Thm.instantiate|~\isa{{\isacharparenleft}\isactrlvec {\isasymalpha}\isactrlisub s{\isacharcomma}\ \isactrlvec x\isactrlisub {\isasymtau}{\isacharparenright}} corresponds to the \isa{instantiate} rules
+  of \figref{fig:subst-rules}.  Type variables are substituted before
+  term variables.  Note that the types in \isa{\isactrlvec x\isactrlisub {\isasymtau}}
+  refer to the instantiated versions.
+
+  \item \verb|Thm.get_axiom_i|~\isa{thy\ name} retrieves a named
+  axiom, cf.\ \isa{axiom} in \figref{fig:prim-rules}.

-  \item \verb|thm| FIXME
+  \item \verb|Thm.invoke_oracle_i|~\isa{thy\ name\ arg} invokes the
+  oracle function \isa{name} of the theory.  Logically, this is
+  just another instance of \isa{axiom} in \figref{fig:prim-rules},
+  but the system records an explicit trace of oracle invocations with
+  the \isa{thm} value.
+
+  arbitrary axioms, without any checking of the proposition.
+
+  \item \verb|Theory.add_oracle|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}} declares an
+  oracle, i.e.\ a function for generating arbitrary axioms.
+
+  \item \verb|Theory.add_deps|~\isa{name\ c\isactrlisub {\isasymtau}\ \isactrlvec d\isactrlisub {\isasymsigma}} declares dependencies of a new specification for
+  constant \isa{c\isactrlisub {\isasymtau}} from relative to existing ones for
+  constants \isa{\isactrlvec d\isactrlisub {\isasymsigma}}.
+
+  \item \verb|Theory.add_defs_i|~\isa{unchecked\ overloaded\ {\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ c\ \isactrlvec x\ {\isasymequiv}\ t{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} states a definitional axiom for an already
+  declared constant \isa{c}.  Dependencies are recorded using \verb|Theory.add_deps|, unless the \isa{unchecked} option is set.

\end{description}%
\end{isamarkuptext}%
@@ -653,7 +737,19 @@

\begin{description}

-  \item FIXME
+  \item \verb|Conjunction.intr| derives \isa{A\ {\isacharampersand}\ B} from \isa{A} and \isa{B}.
+
+  \item \verb|Conjunction.intr| derives \isa{A} and \isa{B}
+  from \isa{A\ {\isacharampersand}\ B}.
+
+  \item \verb|Drule.mk_term|~\isa{t} derives \isa{TERM\ t}.
+
+  \item \verb|Drule.dest_term|~\isa{TERM\ t} recovers term \isa{t}.
+
+  \item \verb|Logic.mk_type|~\isa{{\isasymtau}} produces the term \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}}.
+
+  \item \verb|Logic.dest_type|~\isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} recovers the type
+  \isa{{\isasymtau}}.

\end{description}%
\end{isamarkuptext}%
--- a/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Sep 14 21:42:21 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Sep 14 22:48:37 2006 +0200
@@ -334,7 +334,7 @@
\indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
\verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
\indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
-\verb|  thm list -> Proof.context -> (cterm list * thm list) * Proof.context|
+\verb|  thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\
\end{mldecls}

\begin{description}
--- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 14 21:42:21 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 14 22:48:37 2006 +0200
@@ -489,7 +489,7 @@
@{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
@{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\
\end{tabular}
-  \caption{Conceptual axiomatization of @{text "\<equiv>"}}\label{fig:pure-equality}
+  \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
\end{center}
\end{figure}

@@ -512,12 +512,6 @@
\cite{Barendregt-Geuvers:2001}, where @{text "x : A"} hypotheses are
treated explicitly for types, in the same way as propositions.}

-  \medskip FIXME @{text "\<alpha>\<beta>\<eta>"}-equivalence and primitive definitions
-
-  Since the basic representation of terms already accounts for @{text
-  "\<alpha>"}-conversion, Pure equality essentially acts like @{text
-  "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
-
\medskip The axiomatization of a theory is implicitly closed by
forming all instances of type and term variables: @{text "\<turnstile>
A\<vartheta>"} holds for any substitution instance of an axiom
@@ -550,6 +544,34 @@
"\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is correct, but
@{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold --- the result
belongs to a different proof context.
+
+  \medskip The system allows axioms to be stated either as plain
+  propositions, or as arbitrary functions (oracles'') that produce
+  propositions depending on given arguments.  It is possible to trace
+  the used of axioms (and defined theorems) in derivations.
+  Invocations of oracles are recorded invariable.
+
+  Axiomatizations should be limited to the bare minimum, typically as
+  part of the initial logical basis of an object-logic formalization.
+  Normally, theories will be developed definitionally, by stating
+  restricted equalities over constants.
+
+  A \emph{simple definition} consists of a constant declaration @{text
+  "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text
+  "t"} is a closed term without any hidden polymorphism.  The RHS may
+  depend on further defined constants, but not @{text "c"} itself.
+  Definitions of constants with function type may be presented
+  liberally as @{text "c \<^vec> \<equiv> t"} instead of the puristic @{text
+  "c \<equiv> \<lambda>\<^vec>x. t"}.
+
+  An \emph{overloaded definition} consists may give zero or one
+  equality axioms @{text "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type
+  constructor @{text "\<kappa>"}, with distinct variables @{text "\<^vec>\<alpha>"}
+  as formal arguments.  The RHS may mention previously defined
+  constants as above, or arbitrary constants @{text "d(\<alpha>\<^isub>i)"}
+  for some @{text "\<alpha>\<^isub>i"} projected from @{text "\<^vec>\<alpha>"}.
+  Thus overloaded definitions essentially work by primitive recursion
+  over the syntactic structure of a single type argument.
*}

text %mlref {*
@@ -557,15 +579,83 @@
@{index_ML_type ctyp} \\
@{index_ML_type cterm} \\
@{index_ML_type thm} \\
+  @{index_ML proofs: "int ref"} \\
+  @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
+  @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
+  @{index_ML Thm.assume: "cterm -> thm"} \\
+  @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
+  @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
+  @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
+  @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
+  @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
+  @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
+  @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
+  @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
+  @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
+  @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
+  @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
+  @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
\end{mldecls}

\begin{description}

-  \item @{ML_type ctyp} FIXME
+  \item @{ML_type ctyp} and @{ML_type cterm} represent certified types
+  and terms, respectively.  These are abstract datatypes that
+  guarantee that its values have passed the full well-formedness (and
+  well-typedness) checks, relative to the declarations of type
+  constructors, constants etc. in the theory.
+
+  This representation avoids syntactic rechecking in tight loops of
+  inferences.  There are separate operations to decompose certified
+  entities (including actual theorems).
+
+  \item @{ML_type thm} represents proven propositions.  This is an
+  abstract datatype that guarantees that its values have been
+  constructed by basic principles of the @{ML_struct Thm} module.
+
+  \item @{ML proofs} determines the detail of proof recording: @{ML 0}
+  records only oracles, @{ML 1} records oracles, axioms and named
+  theorems, @{ML 2} records full proof terms.
+
+  \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
+  Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
+  correspond to the primitive inferences of \figref{fig:prim-rules}.
+
+  \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}
+  corresponds to the @{text "generalize"} rules of
+  \figref{fig:subst-rules}.  A collection of type and term variables
+  is generalized simultaneously, according to the given basic names.

-  \item @{ML_type cterm} FIXME
+  \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,
+  \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules
+  of \figref{fig:subst-rules}.  Type variables are substituted before
+  term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
+  refer to the instantiated versions.
+
+  \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
+  axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
+
+  \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes the
+  oracle function @{text "name"} of the theory.  Logically, this is
+  just another instance of @{text "axiom"} in \figref{fig:prim-rules},
+  but the system records an explicit trace of oracle invocations with
+  the @{text "thm"} value.

-  \item @{ML_type thm} FIXME
+  arbitrary axioms, without any checking of the proposition.
+
+  \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an
+  oracle, i.e.\ a function for generating arbitrary axioms.
+
+  \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
+  \<^vec>d\<^isub>\<sigma>"} declares dependencies of a new specification for
+  constant @{text "c\<^isub>\<tau>"} from relative to existing ones for
+  constants @{text "\<^vec>d\<^isub>\<sigma>"}.
+
+  \<^vec>x \<equiv> t), \<dots>]"} states a definitional axiom for an already
+  declared constant @{text "c"}.  Dependencies are recorded using @{ML
+  Theory.add_deps}, unless the @{text "unchecked"} option is set.

\end{description}
*}
@@ -640,7 +730,22 @@

\begin{description}

-  \item FIXME
+  \item @{ML Conjunction.intr} derives @{text "A & B"} from @{text
+  "A"} and @{text "B"}.
+
+  \item @{ML Conjunction.intr} derives @{text "A"} and @{text "B"}
+  from @{text "A & B"}.
+
+  \item @{ML Drule.mk_term}~@{text "t"} derives @{text "TERM t"}.
+
+  \item @{ML Drule.dest_term}~@{text "TERM t"} recovers term @{text
+  "t"}.
+
+  \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text
+  "TYPE(\<tau>)"}.
+
+  \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type
+  @{text "\<tau>"}.

\end{description}
*}
--- a/doc-src/IsarImplementation/Thy/proof.thy	Thu Sep 14 21:42:21 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy	Thu Sep 14 22:48:37 2006 +0200
@@ -295,7 +295,7 @@
@{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
@{index_ML Obtain.result: "(Proof.context -> tactic) ->
-  thm list -> Proof.context -> (cterm list * thm list) * Proof.context"}
+  thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} \\
\end{mldecls}

\begin{description}