# HG changeset patch # User wenzelm # Date 1328812463 -3600 # Node ID 2548a85b0e024e3147bd4532f3388d9af62623f9 # Parent f9a1cd2599dda3c02509a878e707df3f6e6ecbec basic setup for equational reasoning; updated rewrite_goals_tac and fold_goals_tac; diff -r f9a1cd2599dd -r 2548a85b0e02 doc-src/IsarImplementation/IsaMakefile --- a/doc-src/IsarImplementation/IsaMakefile Tue Feb 07 18:56:40 2012 +0100 +++ b/doc-src/IsarImplementation/IsaMakefile Thu Feb 09 19:34:23 2012 +0100 @@ -21,10 +21,10 @@ Thy: $(LOG)/HOL-Thy.gz -$(LOG)/HOL-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Integration.thy \ - Thy/Isar.thy Thy/Local_Theory.thy Thy/Logic.thy Thy/Prelim.thy \ - Thy/Proof.thy Thy/Syntax.thy Thy/Tactic.thy Thy/ML.thy \ - ../antiquote_setup.ML +$(LOG)/HOL-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Eq.thy \ + Thy/Integration.thy Thy/Isar.thy Thy/Local_Theory.thy Thy/Logic.thy \ + Thy/Prelim.thy Thy/Proof.thy Thy/Syntax.thy Thy/Tactic.thy \ + Thy/ML.thy ../antiquote_setup.ML @$(USEDIR) HOL Thy @rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \ Thy/document/pdfsetup.sty Thy/document/session.tex diff -r f9a1cd2599dd -r 2548a85b0e02 doc-src/IsarImplementation/Makefile --- a/doc-src/IsarImplementation/Makefile Tue Feb 07 18:56:40 2012 +0100 +++ b/doc-src/IsarImplementation/Makefile Thu Feb 09 19:34:23 2012 +0100 @@ -13,11 +13,12 @@ FILES = ../extra.sty ../iman.sty ../../lib/texinputs/isabelle.sty \ ../../lib/texinputs/isabellesym.sty \ ../../lib/texinputs/railsetup.sty ../isar.sty ../manual.bib \ - ../pdfsetup.sty ../proof.sty Thy/document/Integration.tex \ - Thy/document/Isar.tex Thy/document/Local_Theory.tex \ - Thy/document/Logic.tex Thy/document/Prelim.tex \ - Thy/document/Proof.tex Thy/document/Syntax.tex \ - Thy/document/Tactic.tex implementation.tex style.sty + ../pdfsetup.sty ../proof.sty Thy/document/Eq.tex \ + Thy/document/Integration.tex Thy/document/Isar.tex \ + Thy/document/Local_Theory.tex Thy/document/Logic.tex \ + Thy/document/Prelim.tex Thy/document/Proof.tex \ + Thy/document/Syntax.tex Thy/document/Tactic.tex implementation.tex \ + style.sty dvi: $(NAME).dvi diff -r f9a1cd2599dd -r 2548a85b0e02 doc-src/IsarImplementation/Thy/Eq.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarImplementation/Thy/Eq.thy Thu Feb 09 19:34:23 2012 +0100 @@ -0,0 +1,75 @@ +theory Eq +imports Base +begin + +chapter {* Equational reasoning *} + +text {* Equality is one of the most fundamental concepts of + mathematics. The Isabelle/Pure logic (\chref{ch:logic}) provides a + builtin relation @{text "\ :: \ \ \ \ prop"} that expresses equality + of arbitrary terms (or propositions) at the framework level, as + expressed by certain basic inference rules (\secref{sec:eq-rules}). + + Equational reasoning means to replace equals by equals, using + reflexivity and transitivity to form chains of replacement steps, + and congruence rules to access sub-structures. Conversions + (\secref{sec:conv}) provide a convenient framework to compose basic + equational steps to build specific equational reasoning tools. + + Higher-order matching is able to provide suitable instantiations for + giving equality rules, which leads to the versatile concept of + @{text "\"}-term rewriting (\secref{sec:rewriting}). Internally + this is based on the general-purpose Simplifier engine of Isabelle, + which is more specific and more efficient than plain conversions. + + Object-logics usually introduce specific notions of equality or + equivalence, and relate it with the Pure equality. This enables to + re-use the Pure tools for equational reasoning for particular + object-logic connectives as well. +*} + + +section {* Basic equality rules \label{sec:eq-rules} *} + +text {* FIXME *} + + +section {* Conversions \label{sec:conv} *} + +text {* FIXME *} + + +section {* Rewriting \label{sec:rewriting} *} + +text {* Rewriting normalizes a given term (theorem or goal) by + replacing instances of given equalities @{text "t \ u"} in subterms. + Rewriting continues until no rewrites are applicable to any subterm. + This may be used to unfold simple definitions of the form @{text "f + x\<^sub>1 \ x\<^sub>n \ u"}, but is slightly more general than that. +*} + +text %mlref {* + \begin{mldecls} + @{index_ML rewrite_goal_tac: "thm list -> int -> tactic"} \\ + @{index_ML rewrite_goals_tac: "thm list -> tactic"} \\ + @{index_ML fold_goals_tac: "thm list -> tactic"} \\ + \end{mldecls} + + \begin{description} + + \item @{ML rewrite_goal_tac}~@{text "rules i"} rewrites subgoal + @{text "i"} by the given rewrite rules. + + \item @{ML rewrite_goals_tac}~@{text "rules"} rewrites all subgoals + by the given rewrite rules. + + \item @{ML fold_goals_tac}~@{text "rules"} essentially uses @{ML + rewrite_goals_tac} with the symmetric form of each member of @{text + "rules"}, re-ordered to fold longer expression first. This supports + to idea to fold primitive definitions that appear in expended form + in the proof state. + + \end{description} +*} + +end diff -r f9a1cd2599dd -r 2548a85b0e02 doc-src/IsarImplementation/Thy/ROOT.ML --- a/doc-src/IsarImplementation/Thy/ROOT.ML Tue Feb 07 18:56:40 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/ROOT.ML Thu Feb 09 19:34:23 2012 +0100 @@ -1,4 +1,5 @@ use_thys [ + "Eq", "Integration", "Isar", "Local_Theory", diff -r f9a1cd2599dd -r 2548a85b0e02 doc-src/IsarImplementation/Thy/document/Eq.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarImplementation/Thy/document/Eq.tex Thu Feb 09 19:34:23 2012 +0100 @@ -0,0 +1,135 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Eq}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Eq\isanewline +\isakeyword{imports}\ Base\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupchapter{Equational reasoning% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Equality is one of the most fundamental concepts of + mathematics. The Isabelle/Pure logic (\chref{ch:logic}) provides a + builtin relation \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} that expresses equality + of arbitrary terms (or propositions) at the framework level, as + expressed by certain basic inference rules (\secref{sec:eq-rules}). + + Equational reasoning means to replace equals by equals, using + reflexivity and transitivity to form chains of replacement steps, + and congruence rules to access sub-structures. Conversions + (\secref{sec:conv}) provide a convenient framework to compose basic + equational steps to build specific equational reasoning tools. + + Higher-order matching is able to provide suitable instantiations for + giving equality rules, which leads to the versatile concept of + \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-term rewriting (\secref{sec:rewriting}). Internally + this is based on the general-purpose Simplifier engine of Isabelle, + which is more specific and more efficient than plain conversions. + + Object-logics usually introduce specific notions of equality or + equivalence, and relate it with the Pure equality. This enables to + re-use the Pure tools for equational reasoning for particular + object-logic connectives as well.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Basic equality rules \label{sec:eq-rules}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +FIXME% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Conversions \label{sec:conv}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +FIXME% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Rewriting \label{sec:rewriting}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Rewriting normalizes a given term (theorem or goal) by + replacing instances of given equalities \isa{t\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ u} in subterms. + Rewriting continues until no rewrites are applicable to any subterm. + This may be used to unfold simple definitions of the form \isa{f\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ u}, but is slightly more general than that.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{rewrite\_goal\_tac}\verb|rewrite_goal_tac: thm list -> int -> tactic| \\ + \indexdef{}{ML}{rewrite\_goals\_tac}\verb|rewrite_goals_tac: thm list -> tactic| \\ + \indexdef{}{ML}{fold\_goals\_tac}\verb|fold_goals_tac: thm list -> tactic| \\ + \end{mldecls} + + \begin{description} + + \item \verb|rewrite_goal_tac|~\isa{rules\ i} rewrites subgoal + \isa{i} by the given rewrite rules. + + \item \verb|rewrite_goals_tac|~\isa{rules} rewrites all subgoals + by the given rewrite rules. + + \item \verb|fold_goals_tac|~\isa{rules} essentially uses \verb|rewrite_goals_tac| with the symmetric form of each member of \isa{rules}, re-ordered to fold longer expression first. This supports + to idea to fold primitive definitions that appear in expended form + in the proof state. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r f9a1cd2599dd -r 2548a85b0e02 doc-src/IsarImplementation/implementation.tex --- a/doc-src/IsarImplementation/implementation.tex Tue Feb 07 18:56:40 2012 +0100 +++ b/doc-src/IsarImplementation/implementation.tex Thu Feb 09 19:34:23 2012 +0100 @@ -86,6 +86,7 @@ \input{Thy/document/Logic.tex} \input{Thy/document/Syntax.tex} \input{Thy/document/Tactic.tex} +\input{Thy/document/Eq.tex} \input{Thy/document/Proof.tex} \input{Thy/document/Isar.tex} \input{Thy/document/Local_Theory.tex} diff -r f9a1cd2599dd -r 2548a85b0e02 doc-src/Ref/tactic.tex --- a/doc-src/Ref/tactic.tex Tue Feb 07 18:56:40 2012 +0100 +++ b/doc-src/Ref/tactic.tex Thu Feb 09 19:34:23 2012 +0100 @@ -29,44 +29,6 @@ \end{ttdescription} -\subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals} -\index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold} -\index{definitions} - -Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a -constant or a constant applied to a list of variables, for example $\it -sqr(n)\equiv n\times n$. Conditional definitions, $\phi\Imp t\equiv u$, -are also supported. {\bf Unfolding} the definition ${t\equiv u}$ means using -it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bf -Folding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues until -no rewrites are applicable to any subterm. - -There are rules for unfolding and folding definitions; Isabelle does not do -this automatically. The corresponding tactics rewrite the proof state, -yielding a single next state. -\begin{ttbox} -rewrite_goals_tac : thm list -> tactic -fold_goals_tac : thm list -> tactic -\end{ttbox} -\begin{ttdescription} -\item[\ttindexbold{rewrite_goals_tac} {\it defs}] -unfolds the {\it defs} throughout the subgoals of the proof state, while -leaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to a -particular subgoal. - -\item[\ttindexbold{fold_goals_tac} {\it defs}] -folds the {\it defs} throughout the subgoals of the proof state, while -leaving the main goal unchanged. -\end{ttdescription} - -\begin{warn} - These tactics only cope with definitions expressed as meta-level - equalities ($\equiv$). More general equivalences are handled by the - simplifier, provided that it is set up appropriately for your logic - (see Chapter~\ref{chap:simplification}). -\end{warn} - - \subsection{Composition: resolution without lifting} \index{tactics!for composition} \begin{ttbox}