# HG changeset patch
# User wenzelm
# Date 1306924744 -7200
# Node ID 6e83c2f732403903e1480de4b42662f21b7d7e11
# Parent  36daee4cc9c9af6090121bdf179e7c8d66ebd3fc
some material on "Calculational reasoning";

diff -r 36daee4cc9c9 -r 6e83c2f73240 doc-src/IsarRef/Thy/Synopsis.thy
--- a/doc-src/IsarRef/Thy/Synopsis.thy	Wed Jun 01 12:20:48 2011 +0200
+++ b/doc-src/IsarRef/Thy/Synopsis.thy	Wed Jun 01 12:39:04 2011 +0200
@@ -213,4 +213,153 @@
 
 end
 
+
+section {* Calculational reasoning *}
+
+text {*
+  For example, see @{file "~~/src/HOL/Isar_Examples/Group.thy"}.
+*}
+
+
+subsection {* Special names in Isar proofs *}
+
+text {*
+  \begin{itemize}
+
+  \item term @{text "?thesis"} --- the main conclusion of the
+  innermost pending claim
+
+  \item term @{text "\<dots>"} --- the argument of the last explicitly
+    stated result (for infix application this is the right-hand side)
+
+  \item fact @{text "this"} --- the last result produced in the text
+
+  \end{itemize}
+*}
+
+notepad
+begin
+  have "x = y"
+  proof -
+    term ?thesis
+    show ?thesis sorry
+    term ?thesis  -- {* static! *}
+  qed
+  term "\<dots>"
+  thm this
+end
+
+text {* Calculational reasoning maintains the special fact called
+  ``@{text calculation}'' in the background.  Certain language
+  elements combine primary @{text this} with secondary @{text
+  calculation}. *}
+
+
+subsection {* Transitive chains *}
+
+text {* The Idea is to combine @{text this} and @{text calculation}
+  via typical @{text trans} rules (see also @{command
+  print_trans_rules}): *}
+
+thm trans
+thm less_trans
+thm less_le_trans
+
+notepad
+begin
+  txt {* Plain bottom-up calculation: *}
+  have "a = b" sorry
+  also
+  have "b = c" sorry
+  also
+  have "c = d" sorry
+  finally
+  have "a = d" .
+
+  txt {* Variant using the @{text "\<dots>"} abbreviation: *}
+  have "a = b" sorry
+  also
+  have "\<dots> = c" sorry
+  also
+  have "\<dots> = d" sorry
+  finally
+  have "a = d" .
+
+  txt {* Top-down version with explicit claim at the head: *}
+  have "a = d"
+  proof -
+    have "a = b" sorry
+    also
+    have "\<dots> = c" sorry
+    also
+    have "\<dots> = d" sorry
+    finally
+    show ?thesis .
+  qed
+next
+  txt {* Mixed inequalities (require suitable base type): *}
+  fix a b c d :: nat
+
+  have "a < b" sorry
+  also
+  have "b\<le> c" sorry
+  also
+  have "c = d" sorry
+  finally
+  have "a < d" .
+end
+
+
+subsubsection {* Notes *}
+
+text {*
+  \begin{itemize}
+
+  \item The notion of @{text trans} rule is very general due to the
+  flexibility of Isabelle/Pure rule composition.
+
+  \item User applications may declare there own rules, with some care
+  about the operational details of higher-order unification.
+
+  \end{itemize}
+*}
+
+
+subsection {* Degenerate calculations and bigstep reasoning *}
+
+text {* The Idea is to append @{text this} to @{text calculation},
+  without rule composition.  *}
+
+notepad
+begin
+  txt {* A vacous proof: *}
+  have A sorry
+  moreover
+  have B sorry
+  moreover
+  have C sorry
+  ultimately
+  have A and B and C .
+next
+  txt {* Slightly more content (trivial bigstep reasoning): *}
+  have A sorry
+  moreover
+  have B sorry
+  moreover
+  have C sorry
+  ultimately
+  have "A \<and> B \<and> C" by blast
+next
+  txt {* More ambitous bigstep reasoning involving structured results: *}
+  have "A \<or> B \<or> C" sorry
+  moreover
+  { assume A have R sorry }
+  moreover
+  { assume B have R sorry }
+  moreover
+  { assume C have R sorry }
+  ultimately
+  have R by blast  -- {* ``big-bang integration'' of proof blocks (occasionally fragile) *}
+end
+
 end
\ No newline at end of file
diff -r 36daee4cc9c9 -r 6e83c2f73240 doc-src/IsarRef/Thy/document/Synopsis.tex
--- a/doc-src/IsarRef/Thy/document/Synopsis.tex	Wed Jun 01 12:20:48 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Synopsis.tex	Wed Jun 01 12:39:04 2011 +0200
@@ -480,6 +480,368 @@
 \endisadelimproof
 \isanewline
 \isacommand{end}\isamarkupfalse%
+%
+\isamarkupsection{Calculational reasoning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+For example, see \verb|~~/src/HOL/Isar_Examples/Group.thy|.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Special names in Isar proofs%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{itemize}
+
+  \item term \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}thesis{\isaliteral{22}{\isachardoublequote}}} --- the main conclusion of the
+  innermost pending claim
+
+  \item term \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} --- the argument of the last explicitly
+    stated result (for infix application this is the right-hand side)
+
+  \item fact \isa{{\isaliteral{22}{\isachardoublequote}}this{\isaliteral{22}{\isachardoublequote}}} --- the last result produced in the text
+
+  \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\ {\isaliteral{2D}{\isacharminus}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\ \ \ \ \isacommand{term}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\isanewline
+%
+\isadelimproof
+\ \ \ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{show}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\ \ \ \ \isacommand{term}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \ %
+\isamarkupcmt{static!%
+}
+\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\ \ \isacommand{term}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isacommand{thm}\isamarkupfalse%
+\ this\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Calculational reasoning maintains the special fact called
+  ``\isa{calculation}'' in the background.  Certain language
+  elements combine primary \isa{this} with secondary \isa{calculation}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Transitive chains%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The Idea is to combine \isa{this} and \isa{calculation}
+  via typical \isa{trans} rules (see also \hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{5F}{\isacharunderscore}}rules}}}}):%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{thm}\isamarkupfalse%
+\ trans\isanewline
+\isacommand{thm}\isamarkupfalse%
+\ less{\isaliteral{5F}{\isacharunderscore}}trans\isanewline
+\isacommand{thm}\isamarkupfalse%
+\ less{\isaliteral{5F}{\isacharunderscore}}le{\isaliteral{5F}{\isacharunderscore}}trans\isanewline
+\isanewline
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+Plain bottom-up calculation:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{also}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{also}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}c\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{finally}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+Variant using the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} abbreviation:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{also}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{also}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{finally}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+Top-down version with explicit claim at the head:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
+\ \ \ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{also}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{also}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{finally}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
+\isacommand{next}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+Mixed inequalities (require suitable base type):%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{fix}\isamarkupfalse%
+\ a\ b\ c\ d\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3C}{\isacharless}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{also}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}b{\isaliteral{5C3C6C653E}{\isasymle}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{also}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}c\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{finally}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3C}{\isacharless}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\isamarkupsubsubsection{Notes%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{itemize}
+
+  \item The notion of \isa{trans} rule is very general due to the
+  flexibility of Isabelle/Pure rule composition.
+
+  \item User applications may declare there own rules, with some care
+  about the operational details of higher-order unification.
+
+  \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Degenerate calculations and bigstep reasoning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The Idea is to append \isa{this} to \isa{calculation},
+  without rule composition.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+A vacous proof:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{have}\isamarkupfalse%
+\ A\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{moreover}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ B\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{moreover}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ C\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{ultimately}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ A\ \isakeyword{and}\ B\ \isakeyword{and}\ C\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
+\isanewline
+\isacommand{next}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+Slightly more content (trivial bigstep reasoning):%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{have}\isamarkupfalse%
+\ A\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{moreover}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ B\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{moreover}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ C\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{ultimately}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
+\ blast\isanewline
+\isacommand{next}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+More ambitous bigstep reasoning involving structured results:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{moreover}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
+\ \isacommand{assume}\isamarkupfalse%
+\ A\ \isacommand{have}\isamarkupfalse%
+\ R\ \isacommand{sorry}\isamarkupfalse%
+\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{moreover}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
+\ \isacommand{assume}\isamarkupfalse%
+\ B\ \isacommand{have}\isamarkupfalse%
+\ R\ \isacommand{sorry}\isamarkupfalse%
+\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{moreover}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
+\ \isacommand{assume}\isamarkupfalse%
+\ C\ \isacommand{have}\isamarkupfalse%
+\ R\ \isacommand{sorry}\isamarkupfalse%
+\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{ultimately}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ R\ \isacommand{by}\isamarkupfalse%
+\ blast\ \ %
+\isamarkupcmt{``big-bang integration'' of proof blocks (occasionally fragile)%
+}
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isacommand{end}\isamarkupfalse%
 \isanewline
 %
 \isadelimtheory