author | wenzelm |

Thu Oct 21 18:04:07 1999 +0200 (1999-10-21) | |

changeset 7897 | 7f18f5ffbb92 |

parent 7896 | 36865f14e5ce |

child 7898 | d7e65a52acf9 |

*** empty log message ***

doc-src/IsarRef/generic.tex | file | annotate | diff | revisions | |

doc-src/IsarRef/refcard.tex | file | annotate | diff | revisions |

1.1 --- a/doc-src/IsarRef/generic.tex Thu Oct 21 17:42:42 1999 +0200 1.2 +++ b/doc-src/IsarRef/generic.tex Thu Oct 21 18:04:07 1999 +0200 1.3 @@ -29,29 +29,30 @@ 1.4 plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than 1.5 $\PROOFNAME$ alone. 1.6 \item [$assumption$] solves some goal by assumption. Any facts given are 1.7 - guaranteed to participate in the refinement. 1.8 + guaranteed to participate in the refinement. Note that ``$\DOT$'' (dot) 1.9 + abbreviates $\BY{assumption}$. 1.10 \item [$rule~thms$] applies some rule given as argument in backward manner; 1.11 facts are used to reduce the rule before applying it to the goal. Thus 1.12 $rule$ without facts is plain \emph{introduction}, while with facts it 1.13 - becomes an \emph{elimination}. 1.14 + becomes a (generalized) \emph{elimination}. 1.15 1.16 Note that the classical reasoner introduces another version of $rule$ that 1.17 is able to pick appropriate rules automatically, whenever explicit $thms$ 1.18 are omitted (see \S\ref{sec:classical-basic}); that method is the default 1.19 - one for initial proof steps, such as $\PROOFNAME$ and ``$\DDOT$'' (two 1.20 - dots). 1.21 + for $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates 1.22 + $\BY{default}$. 1.23 \item [$erule~thms$] is similar to $rule$, but applies rules by 1.24 elim-resolution. This is an improper method, mainly for experimentation and 1.25 porting of old scripts. Actual elimination proofs are usually done with 1.26 - $rule$ (single step, involving facts) or $elim$ (multiple steps, see 1.27 + $rule$ (single step, involving facts) or $elim$ (repeated steps, see 1.28 \S\ref{sec:classical-basic}). 1.29 \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given 1.30 meta-level definitions throughout all goals; any facts provided are 1.31 \emph{ignored}. 1.32 \item [$succeed$] yields a single (unchanged) result; it is the identify of 1.33 - the ``\texttt{,}'' method combinator. 1.34 + the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}). 1.35 \item [$fail$] yields an empty result sequence; it is the identify of the 1.36 - ``\texttt{|}'' method combinator. 1.37 + ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}). 1.38 \end{descr} 1.39 1.40 1.41 @@ -91,9 +92,9 @@ 1.42 \end{rail} 1.43 1.44 \begin{descr} 1.45 -\item [$tag~tags$ and $untag~tags$] add and remove $tags$ to the theorem, 1.46 +\item [$tag~tags$ and $untag~tags$] add and remove $tags$ of the theorem, 1.47 respectively. Tags may be any list of strings that serve as comment for 1.48 - some tools (e.g.\ $\LEMMANAME$ causes tag ``$lemma$'' to be added to the 1.49 + some tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the 1.50 result). 1.51 \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules. $OF$ applies 1.52 $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note 1.53 @@ -102,8 +103,7 @@ 1.54 1.55 $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$ 1.56 that does not include the automatic lifting process that is normally 1.57 - intended (see also \texttt{RS} and \texttt{COMP} in 1.58 - \cite[\S5]{isabelle-ref}). 1.59 + intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}). 1.60 1.61 \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named 1.62 instantiation, respectively. The terms given in $of$ are substituted for 1.63 @@ -113,7 +113,8 @@ 1.64 \item [$standard$] puts a theorem into the standard form of object-rules, just 1.65 as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}). 1.66 1.67 -\item [$elimify$] turns an destruction rule into an elimination. 1.68 +\item [$elimify$] turns an destruction rule into an elimination, just as the 1.69 + ML function \texttt{make\_elim} (see \cite{isabelle-ref}). 1.70 1.71 \item [$export$] lifts a local result out of the current proof context, 1.72 generalizing all fixed variables and discharging all assumptions. Note that 1.73 @@ -139,12 +140,12 @@ 1.74 Calculational proof is forward reasoning with implicit application of 1.75 transitivity rules (such those of $=$, $\le$, $<$). Isabelle/Isar maintains 1.76 an auxiliary register $calculation$\indexisarthm{calculation} for accumulating 1.77 -results obtained by transitivity obtained together with the current result. 1.78 -Command $\ALSO$ updates $calculation$ from the most recent result, while 1.79 -$\FINALLY$ exhibits the final result by forward chaining towards the next goal 1.80 -statement. Both commands require valid current facts, i.e.\ may occur only 1.81 -after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or 1.82 -some finished $\HAVENAME$ or $\SHOWNAME$. 1.83 +results obtained by transitivity composed with the current result. Command 1.84 +$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the 1.85 +final $calculation$ by forward chaining towards the next goal statement. Both 1.86 +commands require valid current facts, i.e.\ may occur only after commands that 1.87 +produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of 1.88 +$\HAVENAME$, $\SHOWNAME$ etc. 1.89 1.90 Also note that the automatic term abbreviation ``$\dots$'' has its canonical 1.91 application with calculational proofs. It automatically refers to the 1.92 @@ -179,17 +180,19 @@ 1.93 \item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as 1.94 $\ALSO$, and concludes the current calculational thread. The final result 1.95 is exhibited as fact for forward chaining towards the next goal. Basically, 1.96 - $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. A typical proof 1.97 - idiom is ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$''. 1.98 + $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Typical proof 1.99 + idioms are``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and 1.100 + ``$\FINALLY~\HAVE{}{\phi}~\DOT$''. 1.101 1.102 \item [$trans$] maintains the set of transitivity rules of the theory or proof 1.103 context, by adding or deleting theorems (the default is to add). 1.104 \end{descr} 1.105 1.106 -See theory \texttt{HOL/Isar_examples/Group} for a simple application of 1.107 -calculations for basic equational reasoning. 1.108 -\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced 1.109 -calculational steps in combination with natural deduction. 1.110 +%FIXME 1.111 +%See theory \texttt{HOL/Isar_examples/Group} for a simple application of 1.112 +%calculations for basic equational reasoning. 1.113 +%\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced 1.114 +%calculational steps in combination with natural deduction. 1.115 1.116 1.117 \section{Axiomatic Type Classes}\label{sec:axclass} 1.118 @@ -231,7 +234,7 @@ 1.119 establish the characteristic theorems of the type classes involved. After 1.120 finishing the proof the theory will be augmented by a type signature 1.121 declaration corresponding to the resulting theorem. 1.122 -\item [$intro_classes$] iteratively expands the class introduction rules of 1.123 +\item [$intro_classes$] repeatedly expands the class introduction rules of 1.124 this theory. 1.125 \end{descr} 1.126 1.127 @@ -243,17 +246,13 @@ 1.128 1.129 \subsection{Simplification methods}\label{sec:simp} 1.130 1.131 -\indexisarmeth{simp}\indexisarmeth{asm-simp} 1.132 +\indexisarmeth{simp} 1.133 \begin{matharray}{rcl} 1.134 simp & : & \isarmeth \\ 1.135 - asm_simp & : & \isarmeth \\ 1.136 \end{matharray} 1.137 1.138 -\railalias{asmsimp}{asm\_simp} 1.139 -\railterm{asmsimp} 1.140 - 1.141 \begin{rail} 1.142 - ('simp' | asmsimp) (simpmod * ) 1.143 + 'simp' (simpmod * ) 1.144 ; 1.145 1.146 simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs 1.147 @@ -261,15 +260,20 @@ 1.148 \end{rail} 1.149 1.150 \begin{descr} 1.151 -\item [$simp$ and $asm_simp$] invoke Isabelle's simplifier, after modifying 1.152 - the context by adding or deleting given rules. The \railtoken{only} 1.153 - modifier first removes all other rewrite rules and congruences, and then is 1.154 - like \railtoken{add}. In contrast, \railtoken{other} ignores its arguments; 1.155 +\item [$simp$] invokes Isabelle's simplifier, after modifying the context by 1.156 + adding or deleting rules as specified. The \railtoken{only} modifier first 1.157 + removes all other rewrite rules and congruences, and then is like 1.158 + \railtoken{add}. In contrast, \railtoken{other} ignores its arguments; 1.159 nevertheless there may be side-effects on the context via attributes. This 1.160 provides a back door for arbitrary context manipulation. 1.161 1.162 - Both of these methods are based on \texttt{asm_full_simp_tac}, see 1.163 - \cite[\S10]{isabelle-ref}; $simp$ removes any premises of the goal, before 1.164 + The $simp$ method is based on \texttt{asm_full_simp_tac} (see also 1.165 + \cite[\S10]{isabelle-ref}), but is much better behaved in practice. Only 1.166 + the local premises of the actual goal are involved by default. Additional 1.167 + facts may be insert via forward-chaining (using $\THEN$, $\FROMNAME$ etc.). 1.168 + The full context of assumptions is 1.169 + 1.170 +; $simp$ removes any premises of the goal, before 1.171 inserting the goal facts; $asm_simp$ leaves the premises. Thus $asm_simp$ 1.172 may refer to premises that are not explicitly spelled out, potentially 1.173 obscuring the reasoning. The plain $simp$ method is more faithful in the

2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 2.2 +++ b/doc-src/IsarRef/refcard.tex Thu Oct 21 18:04:07 1999 +0200 2.3 @@ -0,0 +1,8 @@ 2.4 + 2.5 +\chapter{Isabelle/Isar Quick Reference} 2.6 + 2.7 + 2.8 +%%% Local Variables: 2.9 +%%% mode: latex 2.10 +%%% TeX-master: "isar-ref" 2.11 +%%% End: