improved;
authorwenzelm
Fri Oct 29 16:48:55 1999 +0200 (1999-10-29)
changeset 797434245feb6e82
parent 7973 0d801c6e4dc0
child 7975 3ee8ddca092d
improved;
doc-src/IsarRef/generic.tex
doc-src/IsarRef/isar-ref.tex
doc-src/IsarRef/pure.tex
doc-src/IsarRef/refcard.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Fri Oct 29 12:49:50 1999 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Fri Oct 29 16:48:55 1999 +0200
     1.3 @@ -317,7 +317,8 @@
     1.4  
     1.5  \subsection{Basic methods}\label{sec:classical-basic}
     1.6  
     1.7 -\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
     1.8 +\indexisarmeth{rule}\indexisarmeth{intro}
     1.9 +\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}
    1.10  \begin{matharray}{rcl}
    1.11    rule & : & \isarmeth \\
    1.12    intro & : & \isarmeth \\
     2.1 --- a/doc-src/IsarRef/isar-ref.tex	Fri Oct 29 12:49:50 1999 +0200
     2.2 +++ b/doc-src/IsarRef/isar-ref.tex	Fri Oct 29 16:48:55 1999 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4  %% $Id$
     2.5  
     2.6  \documentclass[12pt,a4paper,fleqn]{report}
     2.7 -\usepackage{graphicx,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
     2.8 +\usepackage{latexsym,graphicx,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
     2.9  
    2.10  \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
    2.11  \author{\emph{Markus Wenzel} \\ TU M\"unchen}
    2.12 @@ -22,6 +22,7 @@
    2.13  
    2.14  \newcommand{\drv}{\mathrel{\vdash}}
    2.15  \newcommand{\edrv}{\mathop{\drv}\nolimits}
    2.16 +\newcommand{\Or}{\mathrel{\;|\;}}
    2.17  
    2.18  
    2.19  \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    2.20 @@ -32,7 +33,7 @@
    2.21  
    2.22  \renewcommand{\phi}{\varphi}
    2.23  
    2.24 -%\includeonly{pure}
    2.25 +%\includeonly{refcard}
    2.26  
    2.27  
    2.28  
     3.1 --- a/doc-src/IsarRef/pure.tex	Fri Oct 29 12:49:50 1999 +0200
     3.2 +++ b/doc-src/IsarRef/pure.tex	Fri Oct 29 16:48:55 1999 +0200
     3.3 @@ -823,8 +823,8 @@
     3.4  \indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
     3.5  \begin{matharray}{rcl}
     3.6    \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
     3.7 -  \isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\
     3.8 -  \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\
     3.9 +  \BG & : & \isartrans{proof(state)}{proof(state)} \\
    3.10 +  \EN & : & \isartrans{proof(state)}{proof(state)} \\
    3.11  \end{matharray}
    3.12  
    3.13  While Isar is inherently block-structured, opening and closing blocks is
    3.14 @@ -857,12 +857,12 @@
    3.15  
    3.16  \subsection{Diagnostics}
    3.17  
    3.18 -\indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm}
    3.19 +\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}
    3.20  \begin{matharray}{rcl}
    3.21 -  \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
    3.22 +  \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
    3.23    \isarcmd{term} & : & \isarkeep{theory~|~proof} \\
    3.24    \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\
    3.25 -  \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
    3.26 +  \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
    3.27  \end{matharray}
    3.28  
    3.29  These commands are not part of the actual Isabelle/Isar syntax, but assist
    3.30 @@ -870,29 +870,29 @@
    3.31  theory or proof configuration is not changed.
    3.32  
    3.33  \begin{rail}
    3.34 -  'typ' type
    3.35 +  'thm' thmrefs
    3.36    ;
    3.37    'term' term
    3.38    ;
    3.39    'prop' prop
    3.40    ;
    3.41 -  'thm' thmrefs
    3.42 +  'typ' type
    3.43    ;
    3.44  \end{rail}
    3.45  
    3.46  \begin{descr}
    3.47 -\item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
    3.48 -  according to the current theory or proof context.
    3.49 +\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
    3.50 +  theory or proof context.  Note that any attributes included in the theorem
    3.51 +  specifications are applied to a temporary context derived from the current
    3.52 +  theory or proof; the result is discarded, i.e.\ attributes involved in
    3.53 +  $thms$ do not have any permanent effect.
    3.54  \item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-checks
    3.55    and print terms or propositions according to the current theory or proof
    3.56    context; the inferred type of $t$ is output as well.  Note that these
    3.57    commands are also useful in inspecting the current environment of term
    3.58    abbreviations.
    3.59 -\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
    3.60 -  theory or proof context.  Note that any attributes included in the theorem
    3.61 -  specifications are applied to a temporary context derived from the current
    3.62 -  theory or proof; the result is discarded, i.e.\ attributes involved in
    3.63 -  $thms$ do not have any permanent effect.
    3.64 +\item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
    3.65 +  according to the current theory or proof context.
    3.66  \end{descr}
    3.67  
    3.68  
     4.1 --- a/doc-src/IsarRef/refcard.tex	Fri Oct 29 12:49:50 1999 +0200
     4.2 +++ b/doc-src/IsarRef/refcard.tex	Fri Oct 29 16:48:55 1999 +0200
     4.3 @@ -1,6 +1,120 @@
     4.4  
     4.5  \chapter{Isabelle/Isar Quick Reference}
     4.6  
     4.7 +\section{Proof commands}
     4.8 +
     4.9 +\subsection{Primitives and basic syntax}
    4.10 +
    4.11 +\begin{tabular}{ll}
    4.12 +  $\FIX{x}$ & augment context by $\All x \Box$ \\
    4.13 +  $\ASSUME{a}{\phi}$ & augment context by $\phi \Imp \Box$ \\
    4.14 +  $\THEN$ & indicate forward chaining \\
    4.15 +  $\HAVE{a}{\phi}$ & prove local result \\
    4.16 +  $\SHOW{a}{\phi}$ & prove local result, establishing some goal \\
    4.17 +  $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\
    4.18 +  $\BG~\dots~\EN$ & declare explicit blocks \\
    4.19 +  $\isarcmd{next}$ & switch implicit blocks \\
    4.20 +  $\NOTE{a}{a@1~\dots~a@n}$ & reconsider facts \\
    4.21 +  $\LET{p = t}$ & \text{abbreviate terms by matching} \\
    4.22 +\end{tabular}
    4.23 +
    4.24 +\begin{matharray}{rcl}
    4.25 +  theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\
    4.26 +  & \Or & \LEMMA{name}{form}~proof \\
    4.27 +  & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex]
    4.28 +  proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex]
    4.29 +  stmt & = & \BG~stmt^*~\EN \\
    4.30 +  & \Or & \isarcmd{next} \\
    4.31 +  & \Or & \NOTE{name}{name^+} \\
    4.32 +  & \Or & \LET{term = term} \\[0.5ex]
    4.33 +  & \Or & \FIX{var^+} \\
    4.34 +  & \Or & \ASSUME{name}{form^+}\\
    4.35 +  & \Or & \THEN~goal{\dsh}stmt \\
    4.36 +  & \Or & goal{\dsh}stmt \\
    4.37 +  goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\
    4.38 +  & \Or & \SHOW{name}{form}~proof \\
    4.39 +\end{matharray}
    4.40 +
    4.41 +
    4.42 +\subsection{Abbreviations and synonyms}
    4.43 +
    4.44 +\begin{matharray}{rcl}
    4.45 +  \BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\
    4.46 +  \DDOT & \equiv & \BY{rule} \\
    4.47 +  \DOT & \equiv & \BY{assumption} \\
    4.48 +  \HENCENAME & \equiv & \THEN~\HAVENAME \\
    4.49 +  \THUSNAME & \equiv & \THEN~\SHOWNAME \\
    4.50 +  \FROM{a@1~\dots~a@n} & \equiv & \NOTE{this}{a@1~\dots~a@n}~\THEN \\
    4.51 +  \WITH{a@1~\dots~a@n} & \equiv & \FROM{a@1~\dots~a@n~this} \\[1ex]
    4.52 +  \FROM{this} & \equiv & \THEN \\
    4.53 +  \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\
    4.54 +  \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\
    4.55 +\end{matharray}
    4.56 +
    4.57 +
    4.58 +\subsection{Derived elements}
    4.59 +
    4.60 +\begin{matharray}{rcl}
    4.61 +  \ALSO@0 & \approx & \NOTE{calculation}{this} \\
    4.62 +  \ALSO@{n+1} & \approx & \NOTE{calculation}{trans~[OF~calculation~this]} \\
    4.63 +  \FINALLY & \approx & \ALSO~\FROM{calculation} \\
    4.64 +  \PRESUME{a}{\phi} & \approx & \ASSUME{a}{\phi} \\
    4.65 +  \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\
    4.66 +  \isarcmd{sorry} & \approx & \BY{cheating} \\
    4.67 +\end{matharray}
    4.68 +
    4.69 +
    4.70 +\subsection{Diagnostic commands}
    4.71 +
    4.72 +\begin{matharray}{ll}
    4.73 +  \isarcmd{thm}~a@1~\dots~a@n & \text{print theorems} \\
    4.74 +  \isarcmd{term}~t & \text{print term} \\
    4.75 +  \isarcmd{prop}~\phi & \text{print meta-level proposition} \\
    4.76 +  \isarcmd{typ}~\tau & \text{print meta-level type} \\
    4.77 +\end{matharray}
    4.78 +
    4.79 +
    4.80 +\section{Proof methods}
    4.81 +
    4.82 +\begin{tabular}{ll}
    4.83 +  \multicolumn{2}{l}{\textbf{Single rules (forward-chaining facts)}} \\[0.5ex]
    4.84 +  $assumption$ & apply assumption \\
    4.85 +  $rule~a@1~\dots~a@n$ & apply some rule  \\
    4.86 +  $rule$ & apply standard rule (default for $\PROOFNAME$) \\
    4.87 +  $induct~x$ & apply induction rule \\
    4.88 +  $contradiction$ & apply $\neg{}$ elimination rule \\[2ex]
    4.89 +
    4.90 +  \multicolumn{2}{l}{\textbf{Multiple rules (inserting facts)}} \\[0.5ex]
    4.91 +  $-$ & \text{no rules} \\
    4.92 +  $intro~a@1~\dots~a@n$ & \text{introduction rules} \\
    4.93 +  $elim~a@1~\dots~a@n$ & \text{elimination rules} \\[2ex]
    4.94 +
    4.95 +  \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
    4.96 +  $simp$ & Simplifier \\
    4.97 +  $blast$, $fast$ & Classical reasoner \\
    4.98 +  $force$, $auto$ & Simplifier + Classical reasoner \\
    4.99 +  $arith$ & Arithmetic procedure \\
   4.100 +\end{tabular}
   4.101 +
   4.102 +
   4.103 +\section{Attributes}
   4.104 +
   4.105 +\begin{tabular}{ll}
   4.106 +  \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]
   4.107 +  $RS~b$ & resolve fact with rule \\
   4.108 +  $OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\
   4.109 +  $of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\
   4.110 +  $standard$ & put into standard result form \\
   4.111 +  $rulify$ & put into standard object-rule form \\
   4.112 +  $elimify$ & put destruction rule into elimination form \\[1ex]
   4.113 +
   4.114 +  \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
   4.115 +  $simp$ & declare Simplifier rules \\
   4.116 +  $intro$, $elim$, $dest$ & declare Classical reasoner rules (also ``$!$'' or ``$!!$'') \\
   4.117 +  $iff$ & declare Simplifier + Classical reasoner rules \\
   4.118 +  $trans$ & calculational rules (general transitivity) \\
   4.119 +\end{tabular}
   4.120 +
   4.121  
   4.122  %%% Local Variables: 
   4.123  %%% mode: latex