--- a/doc-src/IsarImplementation/IsaMakefile Mon Sep 04 16:28:36 2006 +0200
+++ b/doc-src/IsarImplementation/IsaMakefile Mon Sep 04 17:06:45 2006 +0200
@@ -21,7 +21,7 @@
Thy: $(LOG)/Pure-Thy.gz
-$(LOG)/Pure-Thy.gz: Thy/ROOT.ML Thy/base.thy Thy/integration.thy \
+$(LOG)/Pure-Thy.gz: Thy/ROOT.ML Thy/base.thy Thy/integration.thy Thy/isar.thy \
Thy/locale.thy Thy/logic.thy Thy/prelim.thy Thy/proof.thy Thy/tactic.thy \
Thy/ML.thy Thy/setup.ML
@$(USEDIR) Pure Thy
--- a/doc-src/IsarImplementation/Thy/ROOT.ML Mon Sep 04 16:28:36 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/ROOT.ML Mon Sep 04 17:06:45 2006 +0200
@@ -5,6 +5,7 @@
use_thy "logic";
use_thy "tactic";
use_thy "proof";
+use_thy "isar";
use_thy "locale";
use_thy "integration";
use_thy "ML";
--- a/doc-src/IsarImplementation/Thy/document/logic.tex Mon Sep 04 16:28:36 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Mon Sep 04 17:06:45 2006 +0200
@@ -23,7 +23,7 @@
}
\isamarkuptrue%
%
-\isamarkupsection{Variable names%
+\isamarkupsection{Names%
}
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/proof.tex Mon Sep 04 16:28:36 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Mon Sep 04 17:06:45 2006 +0200
@@ -299,47 +299,78 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME%
+Local results are established by monotonic reasoning from facts
+ within a context. This admits arbitrary combination of theorems,
+ e.g.\ using \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} elimination, resolution rules, or
+ equational reasoning. Unaccounted context manipulations should be
+ ruled out, such as raw \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} introduction or ad-hoc
+ references to free variables or assumptions not present in the proof
+ context.
+
+ \medskip The \isa{prove} operation provides a separate interface
+ for structured backwards reasoning under program control, with some
+ explicit sanity checks of the result. The goal context can be
+ augmented locally by given fixed variables and assumptions, which
+ will be available as local facts during the proof and discharged
+ into implications in the result.
+
+ The \isa{prove{\isacharunderscore}multi} operation handles several simultaneous
+ claims within a single goal statement, by using meta-level
+ conjunction internally.
+
+ \medskip The tactical proof of a local claim may be structured
+ further by decomposing a sub-goal: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}}
+ is turned into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} after fixing \isa{x} and
+ assuming \isa{A{\isacharparenleft}x{\isacharparenright}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Proof states \label{sec:isar-proof-state}%
-}
-\isamarkuptrue%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
%
\begin{isamarkuptext}%
-FIXME
+\begin{mldecls}
+ \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
+\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
+ \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{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
+\verb| params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
+\verb| prems: thm list} -> tactic) -> Proof.context -> int -> tactic|
+ \end{mldecls}
+
+ \begin{description}
-\glossary{Proof state}{The whole configuration of a structured proof,
-consisting of a \seeglossary{proof context} and an optional
-\seeglossary{structured goal}. Internally, an Isar proof state is
-organized as a stack to accomodate block structure of proof texts.
-For historical reasons, a low-level \seeglossary{tactical goal} is
-occasionally called ``proof state'' as well.}
+ \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context of fixed variables \isa{xs} and assumptions
+ \isa{As} and applies tactic \isa{tac} to solve it. The
+ latter may depend on the local assumptions being presented as facts.
+ The result is essentially \isa{{\isasymAnd}xs{\isachardot}\ As\ {\isasymLongrightarrow}\ C}, but is normalized
+ by pulling \isa{{\isasymAnd}} before \isa{{\isasymLongrightarrow}} (the conclusion \isa{C} itself may be a rule statement), turning the quantifier prefix
+ into schematic variables, and generalizing implicit type-variables.
-\glossary{Structured goal}{FIXME}
+ \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
+ states several conclusions simultaneously. \verb|Tactic.conjunction_tac| may be used to split these into individual
+ subgoals before commencing the actual proof.
-\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}%
+ \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a
+ particular sub-goal, producing an extended context and a reduced
+ goal, which needs to be solved by the given tactic. All schematic
+ parameters of the goal are imported into the context as fixed ones,
+ which may not be instantiated in the sub-proof.
+
+ \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Proof methods%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\endisatagmlref
+{\isafoldmlref}%
%
-\isamarkupsection{Attributes%
-}
-\isamarkuptrue%
+\isadelimmlref
%
-\begin{isamarkuptext}%
-FIXME ?!%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\endisadelimmlref
%
\isadelimtheory
%
--- a/doc-src/IsarImplementation/Thy/document/session.tex Mon Sep 04 16:28:36 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/session.tex Mon Sep 04 17:06:45 2006 +0200
@@ -8,6 +8,8 @@
\input{proof.tex}
+\input{isar.tex}
+
\input{locale.tex}
\input{integration.tex}
--- a/doc-src/IsarImplementation/Thy/document/tactic.tex Mon Sep 04 16:28:36 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/tactic.tex Mon Sep 04 17:06:45 2006 +0200
@@ -163,74 +163,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Programmed proofs%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In order to perform a complete tactical proof under program control,
- one needs to set up an initial goal configuration, apply a tactic,
- and finish the result, cf.\ the rules given in
- \secref{sec:tactical-goals}. Further checks are required to ensure
- that the result is actually an instance of the original claim --
- ill-behaved tactics could have destroyed that information.
-
- Several simultaneous claims may be handled within a single goal
- statement by using meta-level conjunction internally. The whole
- configuration may be considered within a context of
- arbitrary-but-fixed parameters and hypotheses, which will be
- available as local facts during the proof and discharged into
- implications in the result.
-
- All of these administrative tasks are packaged into a separate
- operation, such that the user merely needs to provide the statement
- and tactic to be applied.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
-\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
- \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{Goal.prove-global}\verb|Goal.prove_global: theory -> string list -> term list -> term ->|\isasep\isanewline%
-\verb| (thm list -> tactic) -> thm| \\
- \end{mldecls}
-
- \begin{description}
-
- \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context of arbitrary-but-fixed parameters \isa{xs}
- and hypotheses \isa{As} and applies tactic \isa{tac} to
- solve it. The latter may depend on the local assumptions being
- presented as facts. The result is essentially \isa{{\isasymAnd}xs{\isachardot}\ As\ {\isasymLongrightarrow}\ C}, but is normalized by pulling \isa{{\isasymAnd}} before \isa{{\isasymLongrightarrow}}
- (the conclusion \isa{C} itself may be a rule statement), turning
- the quantifier prefix into schematic variables, and generalizing
- implicit type-variables.
-
- \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
- states several conclusions simultaneously. \verb|Tactic.conjunction_tac| may be used to split these into individual
- subgoals before commencing the actual proof.
-
- \item \verb|Goal.prove_global| is a degraded version of \verb|Goal.prove| for theory level goals; it includes a global \verb|Drule.standard| for the result.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
\isadelimtheory
%
\endisadelimtheory
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/isar.thy Mon Sep 04 17:06:45 2006 +0200
@@ -0,0 +1,36 @@
+
+(* $Id$ *)
+
+theory isar imports base begin
+
+chapter {* Isar proof texts *}
+
+section {* Proof states \label{sec:isar-proof-state} *}
+
+text {*
+ FIXME
+
+\glossary{Proof state}{The whole configuration of a structured proof,
+consisting of a \seeglossary{proof context} and an optional
+\seeglossary{structured goal}. Internally, an Isar proof state is
+organized as a stack to accomodate block structure of proof texts.
+For historical reasons, a low-level \seeglossary{tactical goal} is
+occasionally called ``proof state'' as well.}
+
+\glossary{Structured goal}{FIXME}
+
+\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}
+
+
+*}
+
+section {* Proof methods *}
+
+text FIXME
+
+section {* Attributes *}
+
+text "FIXME ?!"
+
+
+end
--- a/doc-src/IsarImplementation/Thy/logic.thy Mon Sep 04 16:28:36 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy Mon Sep 04 17:06:45 2006 +0200
@@ -5,7 +5,7 @@
chapter {* Primitive logic \label{ch:logic} *}
-section {* Variable names *}
+section {* Names *}
text FIXME
--- a/doc-src/IsarImplementation/Thy/proof.thy Mon Sep 04 16:28:36 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy Mon Sep 04 17:06:45 2006 +0200
@@ -263,34 +263,67 @@
section {* Conclusions *}
-text FIXME
-
-
-section {* Proof states \label{sec:isar-proof-state} *}
-
text {*
- FIXME
+ Local results are established by monotonic reasoning from facts
+ within a context. This admits arbitrary combination of theorems,
+ e.g.\ using @{text "\<And>/\<Longrightarrow>"} elimination, resolution rules, or
+ equational reasoning. Unaccounted context manipulations should be
+ ruled out, such as raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc
+ references to free variables or assumptions not present in the proof
+ context.
-\glossary{Proof state}{The whole configuration of a structured proof,
-consisting of a \seeglossary{proof context} and an optional
-\seeglossary{structured goal}. Internally, an Isar proof state is
-organized as a stack to accomodate block structure of proof texts.
-For historical reasons, a low-level \seeglossary{tactical goal} is
-occasionally called ``proof state'' as well.}
+ \medskip The @{text "prove"} operation provides a separate interface
+ for structured backwards reasoning under program control, with some
+ explicit sanity checks of the result. The goal context can be
+ augmented locally by given fixed variables and assumptions, which
+ will be available as local facts during the proof and discharged
+ into implications in the result.
-\glossary{Structured goal}{FIXME}
+ The @{text "prove_multi"} operation handles several simultaneous
+ claims within a single goal statement, by using meta-level
+ conjunction internally.
-\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}
-
-
+ \medskip The tactical proof of a local claim may be structured
+ further by decomposing a sub-goal: @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"}
+ is turned into @{text "B(x) \<Longrightarrow> \<dots>"} after fixing @{text "x"} and
+ assuming @{text "A(x)"}.
*}
-section {* Proof methods *}
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
+ @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
+ @{index_ML SUBPROOF:
+ "({context: Proof.context, schematics: ctyp list * cterm list,
+ params: cterm list, asms: cterm list, concl: cterm,
+ prems: thm list} -> tactic) -> Proof.context -> int -> tactic"}
+ \end{mldecls}
-text FIXME
+ \begin{description}
-section {* Attributes *}
+ \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
+ "C"} in the context of fixed variables @{text "xs"} and assumptions
+ @{text "As"} and applies tactic @{text "tac"} to solve it. The
+ latter may depend on the local assumptions being presented as facts.
+ The result is essentially @{text "\<And>xs. As \<Longrightarrow> C"}, but is normalized
+ by pulling @{text "\<And>"} before @{text "\<Longrightarrow>"} (the conclusion @{text
+ "C"} itself may be a rule statement), turning the quantifier prefix
+ into schematic variables, and generalizing implicit type-variables.
-text "FIXME ?!"
+ \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
+ states several conclusions simultaneously. @{ML
+ Tactic.conjunction_tac} may be used to split these into individual
+ subgoals before commencing the actual proof.
+
+ \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a
+ particular sub-goal, producing an extended context and a reduced
+ goal, which needs to be solved by the given tactic. All schematic
+ parameters of the goal are imported into the context as fixed ones,
+ which may not be instantiated in the sub-proof.
+
+ \end{description}
+*}
end
--- a/doc-src/IsarImplementation/Thy/tactic.thy Mon Sep 04 16:28:36 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/tactic.thy Mon Sep 04 17:06:45 2006 +0200
@@ -134,61 +134,5 @@
*}
-section {* Programmed proofs *}
-
-text {*
- In order to perform a complete tactical proof under program control,
- one needs to set up an initial goal configuration, apply a tactic,
- and finish the result, cf.\ the rules given in
- \secref{sec:tactical-goals}. Further checks are required to ensure
- that the result is actually an instance of the original claim --
- ill-behaved tactics could have destroyed that information.
-
- Several simultaneous claims may be handled within a single goal
- statement by using meta-level conjunction internally. The whole
- configuration may be considered within a context of
- arbitrary-but-fixed parameters and hypotheses, which will be
- available as local facts during the proof and discharged into
- implications in the result.
-
- All of these administrative tasks are packaged into a separate
- operation, such that the user merely needs to provide the statement
- and tactic to be applied.
-*}
-
-text %mlref {*
- \begin{mldecls}
- @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
- ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
- @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
- ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
- @{index_ML Goal.prove_global: "theory -> string list -> term list -> term ->
- (thm list -> tactic) -> thm"} \\
- \end{mldecls}
-
- \begin{description}
-
- \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
- "C"} in the context of arbitrary-but-fixed parameters @{text "xs"}
- and hypotheses @{text "As"} and applies tactic @{text "tac"} to
- solve it. The latter may depend on the local assumptions being
- presented as facts. The result is essentially @{text "\<And>xs. As \<Longrightarrow>
- C"}, but is normalized by pulling @{text "\<And>"} before @{text "\<Longrightarrow>"}
- (the conclusion @{text "C"} itself may be a rule statement), turning
- the quantifier prefix into schematic variables, and generalizing
- implicit type-variables.
-
- \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
- states several conclusions simultaneously. @{ML
- Tactic.conjunction_tac} may be used to split these into individual
- subgoals before commencing the actual proof.
-
- \item @{ML Goal.prove_global} is a degraded version of @{ML
- Goal.prove} for theory level goals; it includes a global @{ML
- Drule.standard} for the result.
-
- \end{description}
-*}
-
end
--- a/doc-src/IsarImplementation/implementation.tex Mon Sep 04 16:28:36 2006 +0200
+++ b/doc-src/IsarImplementation/implementation.tex Mon Sep 04 17:06:45 2006 +0200
@@ -65,6 +65,7 @@
\input{Thy/document/logic.tex}
\input{Thy/document/tactic.tex}
\input{Thy/document/proof.tex}
+\input{Thy/document/isar.tex}
\input{Thy/document/locale.tex}
\input{Thy/document/integration.tex}