doc-src/IsarRef/refcard.tex
 changeset 7987 d9aef93c0e32 parent 7981 5120a2a15d06 child 8195 af2575a5c5ae
     1.1 --- a/doc-src/IsarRef/refcard.tex	Sat Oct 30 20:41:30 1999 +0200
1.2 +++ b/doc-src/IsarRef/refcard.tex	Sun Oct 31 15:20:35 1999 +0100
1.3 @@ -14,13 +14,13 @@
1.4    $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\
1.5    $\BG~\dots~\EN$ & declare explicit blocks \\
1.6    $\isarcmd{next}$ & switch implicit blocks \\
1.7 -  $\NOTE{a}{a@1~\dots~a@n}$ & reconsider facts \\
1.8 -  $\LET{p = t}$ & \text{abbreviate terms by matching} \\
1.9 +  $\NOTE{a}{a@1\;\dots\;a@n}$ & reconsider facts \\
1.10 +  $\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\
1.11  \end{tabular}
1.12
1.13  \begin{matharray}{rcl}
1.14 -  theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\
1.15 -  & \Or & \LEMMA{name}{form}~proof \\
1.16 +  theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\
1.17 +  & \Or & \LEMMA{name}{prop}~proof \\
1.18    & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex]
1.19    proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex]
1.20    stmt & = & \BG~stmt^*~\EN \\
1.21 @@ -28,11 +28,11 @@
1.22    & \Or & \NOTE{name}{name^+} \\
1.23    & \Or & \LET{term = term} \\[0.5ex]
1.24    & \Or & \FIX{var^+} \\
1.25 -  & \Or & \ASSUME{name}{form^+}\\
1.26 +  & \Or & \ASSUME{name}{prop^+}\\
1.27    & \Or & \THEN~goal{\dsh}stmt \\
1.28    & \Or & goal{\dsh}stmt \\
1.29 -  goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\
1.30 -  & \Or & \SHOW{name}{form}~proof \\
1.31 +  goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\
1.32 +  & \Or & \SHOW{name}{prop}~proof \\
1.33  \end{matharray}
1.34
1.35
1.36 @@ -44,8 +44,8 @@
1.37    \DOT & \equiv & \BY{assumption} \\
1.38    \HENCENAME & \equiv & \THEN~\HAVENAME \\
1.39    \THUSNAME & \equiv & \THEN~\SHOWNAME \\
1.40 -  \FROM{a@1~\dots~a@n} & \equiv & \NOTE{this}{a@1~\dots~a@n}~\THEN \\
1.41 -  \WITH{a@1~\dots~a@n} & \equiv & \FROM{a@1~\dots~a@n~this} \\[1ex]
1.42 +  \FROM{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\
1.43 +  \WITH{a@1\;\dots\;a@n} & \equiv & \FROM{a@1\;\dots\;a@n~this} \\[1ex]
1.44    \FROM{this} & \equiv & \THEN \\
1.45    \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\
1.46    \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\
1.47 @@ -67,7 +67,7 @@
1.48  \subsection{Diagnostic commands}
1.49
1.50  \begin{matharray}{ll}
1.51 -  \isarcmd{thm}~a@1~\dots~a@n & \text{print theorems} \\
1.52 +  \isarcmd{thm}~a@1\;\dots\;a@n & \text{print theorems} \\
1.53    \isarcmd{term}~t & \text{print term} \\
1.54    \isarcmd{prop}~\phi & \text{print meta-level proposition} \\
1.55    \isarcmd{typ}~\tau & \text{print meta-level type} \\
1.56 @@ -78,22 +78,22 @@
1.57
1.58  \begin{tabular}{ll}
1.59    \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
1.60 -  $assumption$ & apply assumption \\
1.61 -  $rule~a@1~\dots~a@n$ & apply some rule  \\
1.62 +  $assumption$ & apply some assumption \\
1.63 +  $rule~a@1\;\dots\;a@n$ & apply some rule  \\
1.64    $rule$ & apply standard rule (default for $\PROOFNAME$) \\
1.65    $induct~x$ & apply induction rule \\
1.66 -  $contradiction$ & apply $\neg{}$ elimination rule \\[2ex]
1.67 +  $contradiction$ & apply $\neg{}$ elimination rule (any order) \\[2ex]
1.68
1.69    \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
1.70    $-$ & \text{no rules} \\
1.71 -  $intro~a@1~\dots~a@n$ & \text{introduction rules} \\
1.72 -  $elim~a@1~\dots~a@n$ & \text{elimination rules} \\
1.73 -  $unfold~a@1~\dots~a@n$ & \text{definitions} \\[2ex]
1.74 +  $intro~a@1\;\dots\;a@n$ & \text{introduction rules} \\
1.75 +  $elim~a@1\;\dots\;a@n$ & \text{elimination rules} \\
1.76 +  $unfold~a@1\;\dots\;a@n$ & \text{definitions} \\[2ex]
1.77
1.78    \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
1.79    $simp$ & Simplifier \\
1.80 -  $blast$, $fast$ & Classical reasoner \\
1.81 -  $force$, $auto$ & Simplifier + Classical reasoner \\
1.82 +  $blast$, $fast$ & Classical Reasoner \\
1.83 +  $force$, $auto$ & Simplifier + Classical Reasoner \\
1.84    $arith$ & Arithmetic procedure \\
1.85  \end{tabular}
1.86
1.87 @@ -102,8 +102,8 @@
1.88
1.89  \begin{tabular}{ll}
1.90    \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]
1.91 -  $OF~a@1~\dots~a@n$ & apply rule to facts (skip $_$'') \\
1.92 -  $of~t@1~\dots~t@n$ & apply rule to terms (skip $_$'') \\
1.93 +  $OF~a@1\;\dots\;a@n$ & apply rule to facts (skipping $_$'') \\
1.94 +  $of~t@1\;\dots\;t@n$ & apply rule to terms (skipping $_$'') \\
1.95    $RS~b$ & resolve fact with rule \\
1.96    $standard$ & put into standard result form \\
1.97    $rulify$ & put into object-rule form \\
1.98 @@ -111,12 +111,11 @@
1.99
1.100    \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
1.101    $simp$ & declare Simplifier rules \\
1.102 -  $intro$, $elim$, $dest$ & declare Classical reasoner rules (also $!$'' or $!!$'') \\
1.103 -  $iff$ & declare Simplifier + Classical reasoner rules \\
1.104 -  $trans$ & calculational rules (general transitivity) \\
1.105 +  $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also $!$'' or $!!$'') \\
1.106 +  $iff$ & declare Simplifier + Classical Reasoner rules \\
1.107 +  $trans$ & declare calculational rules (general transitivity) \\
1.108  \end{tabular}
1.109
1.110 -
1.111  %%% Local Variables:
1.112  %%% mode: latex
1.113  %%% TeX-master: "isar-ref"