# HG changeset patch # User wenzelm # Date 1157382405 -7200 # Node ID e993073eda4c26f468e684f17b09b5d9e7324a25 # Parent ffafbd4103c02a5de964c2b4fecb43a8743c45fe tuned; diff -r ffafbd4103c0 -r e993073eda4c doc-src/IsarImplementation/IsaMakefile --- 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 diff -r ffafbd4103c0 -r e993073eda4c doc-src/IsarImplementation/Thy/ROOT.ML --- 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"; diff -r ffafbd4103c0 -r e993073eda4c doc-src/IsarImplementation/Thy/document/logic.tex --- 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% % diff -r ffafbd4103c0 -r e993073eda4c doc-src/IsarImplementation/Thy/document/proof.tex --- 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 % diff -r ffafbd4103c0 -r e993073eda4c doc-src/IsarImplementation/Thy/document/session.tex --- 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} diff -r ffafbd4103c0 -r e993073eda4c doc-src/IsarImplementation/Thy/document/tactic.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 diff -r ffafbd4103c0 -r e993073eda4c doc-src/IsarImplementation/Thy/isar.thy --- /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 diff -r ffafbd4103c0 -r e993073eda4c doc-src/IsarImplementation/Thy/logic.thy --- 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 diff -r ffafbd4103c0 -r e993073eda4c doc-src/IsarImplementation/Thy/proof.thy --- 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 "\/\"} elimination, resolution rules, or + equational reasoning. Unaccounted context manipulations should be + ruled out, such as raw @{text "\/\"} 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 "(\x. A(x) \ B(x)) \ \"} + is turned into @{text "B(x) \ \"} 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 "\xs. As \ C"}, but is normalized + by pulling @{text "\"} before @{text "\"} (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 diff -r ffafbd4103c0 -r e993073eda4c doc-src/IsarImplementation/Thy/tactic.thy --- 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 "\xs. As \ - C"}, but is normalized by pulling @{text "\"} before @{text "\"} - (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 diff -r ffafbd4103c0 -r e993073eda4c doc-src/IsarImplementation/implementation.tex --- 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}