1.1 --- a/doc-src/IsarRef/IsaMakefile Sat May 03 13:25:27 2008 +0200
1.2 +++ b/doc-src/IsarRef/IsaMakefile Sat May 03 13:26:08 2008 +0200
1.3 @@ -22,7 +22,7 @@
1.4 Thy: $(LOG)/HOL-Thy.gz
1.5
1.6 $(LOG)/HOL-Thy.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \
1.7 - Thy/pure.thy Thy/syntax.thy
1.8 + Thy/pure.thy Thy/syntax.thy Thy/Quick_Reference.thy
1.9 @$(USEDIR) HOL Thy
1.10
1.11
2.1 --- a/doc-src/IsarRef/Makefile Sat May 03 13:25:27 2008 +0200
2.2 +++ b/doc-src/IsarRef/Makefile Sat May 03 13:26:08 2008 +0200
2.3 @@ -14,7 +14,8 @@
2.4 NAME = isar-ref
2.5
2.6 FILES = isar-ref.tex Thy/document/intro.tex basics.tex Thy/document/syntax.tex \
2.7 - Thy/document/pure.tex generic.tex logics.tex refcard.tex conversion.tex \
2.8 + Thy/document/pure.tex generic.tex logics.tex Thy/document/Quick_Reference.tex \
2.9 + conversion.tex \
2.10 ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \
2.11 ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
2.12
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/IsarRef/Thy/Quick_Reference.thy Sat May 03 13:26:08 2008 +0200
3.3 @@ -0,0 +1,219 @@
3.4 +(* $Id$ *)
3.5 +
3.6 +theory Quick_Reference
3.7 +imports Main
3.8 +begin
3.9 +
3.10 +chapter {* Isabelle/Isar quick reference \label{ap:refcard} *}
3.11 +
3.12 +section {* Proof commands *}
3.13 +
3.14 +subsection {* Primitives and basic syntax *}
3.15 +
3.16 +text {*
3.17 + \begin{tabular}{ll}
3.18 + @{command "fix"}~@{text x} & augment context by @{text "\<And>x. \<box>"} \\
3.19 + @{command "assume"}~@{text "a: \<phi>"} & augment context by @{text "\<phi> \<Longrightarrow> \<box>"} \\
3.20 + @{command "then"} & indicate forward chaining of facts \\
3.21 + @{command "have"}~@{text "a: \<phi>"} & prove local result \\
3.22 + @{command "show"}~@{text "a: \<phi>"} & prove local result, refining some goal \\
3.23 + @{command "using"}~@{text a} & indicate use of additional facts \\
3.24 + @{command "unfolding"}~@{text a} & unfold definitional equations \\
3.25 + @{command "proof"}~@{text "m\<^sub>1"}~\dots~@{command "qed"}~@{text "m\<^sub>2"} & indicate proof structure and refinements \\
3.26 + @{command "{"}~\dots~@{command "}"} & indicate explicit blocks \\
3.27 + @{command "next"} & switch blocks \\
3.28 + @{command "note"}~@{text "a = b"} & reconsider facts \\
3.29 + @{command "let"}~@{text "p = t"} & abbreviate terms by higher-order matching \\
3.30 + \end{tabular}
3.31 +
3.32 + \begin{matharray}{rcl}
3.33 + @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: prop proof"} \Or @{command "definition"}~\dots \Or \dots \\[1ex]
3.34 + @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method stmt\<^sup>*"}~@{command "qed"}~@{text method} \\
3.35 + & \Or & @{text "prfx\<^sup>*"}~@{command "done"} \\[1ex]
3.36 + @{text prfx} & = & @{command "apply"}~@{text method} \\
3.37 + & \Or & @{command "using"}~@{text "name\<^sup>+"} \\
3.38 + & \Or & @{command "unfolding"}~@{text "name\<^sup>+"} \\
3.39 + @{text stmt} & = & @{command "{"}~@{text "stmt\<^sup>*"}~@{command "}"} \\
3.40 + & \Or & @{command "next"} \\
3.41 + & \Or & @{command "note"}~@{text "name = name\<^sup>+"} \\
3.42 + & \Or & @{command "let"}~@{text "term = term"} \\
3.43 + & \Or & @{command "fix"}~@{text "var\<^sup>+"} \\
3.44 + & \Or & @{command "assume"}~@{text "name: prop\<^sup>+"} \\
3.45 + & \Or & @{command "then"}@{text "\<^sup>?"}~@{text goal} \\
3.46 + @{text goal} & = & @{command "have"}~@{text "name: prop\<^sup>+ proof"} \\
3.47 + & \Or & @{command "show"}~@{text "name: prop\<^sup>+ proof"} \\
3.48 + \end{matharray}
3.49 +*}
3.50 +
3.51 +
3.52 +subsection {* Abbreviations and synonyms *}
3.53 +
3.54 +text {*
3.55 + \begin{matharray}{rcl}
3.56 + @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} & \equiv & @{command "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"} \\
3.57 + @{command ".."} & \equiv & @{command "by"}~@{text rule} \\
3.58 + @{command "."} & \equiv & @{command "by"}~@{text this} \\
3.59 + @{command "hence"} & \equiv & @{command "then"}~@{command "have"} \\
3.60 + @{command "thus"} & \equiv & @{command "then"}~@{command "show"} \\
3.61 + @{command "from"}~@{text a} & \equiv & @{command "note"}~@{text a}~@{command "then"} \\
3.62 + @{command "with"}~@{text a} & \equiv & @{command "from"}~@{text "a \<AND> this"} \\[1ex]
3.63 + @{command "from"}~@{text this} & \equiv & @{command "then"} \\
3.64 + @{command "from"}~@{text this}~@{command "have"} & \equiv & @{command "hence"} \\
3.65 + @{command "from"}~@{text this}~@{command "show"} & \equiv & @{command "thus"} \\
3.66 + \end{matharray}
3.67 +*}
3.68 +
3.69 +
3.70 +subsection {* Derived elements *}
3.71 +
3.72 +text {*
3.73 + \begin{matharray}{rcl}
3.74 + @{command "also"}@{text "\<^sub>0"} & \approx & @{command "note"}~@{text "calculation = this"} \\
3.75 + @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \approx & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\
3.76 + @{command "finally"} & \approx & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
3.77 + @{command "moreover"} & \approx & @{command "note"}~@{text "calculation = calculation this"} \\
3.78 + @{command "ultimately"} & \approx & @{command "moreover"}~@{command "from"}~@{text calculation} \\[0.5ex]
3.79 + @{command "presume"}~@{text "a: \<phi>"} & \approx & @{command "assume"}~@{text "a: \<phi>"} \\
3.80 + @{command "def"}~@{text "a: x \<equiv> t"} & \approx & @{command "fix"}~@{text x}~@{command "assume"}~@{text "a: x \<equiv> t"} \\
3.81 + @{command "obtain"}~@{text "x \<WHERE> a: \<phi>"} & \approx & \dots~@{command "fix"}~@{text x}~@{command "assume"}~@{text "a: \<phi>"} \\
3.82 + @{command "case"}~@{text c} & \approx & @{command "fix"}~@{text x}~@{command "assume"}~@{text "c: \<phi>"} \\
3.83 + @{command "sorry"} & \approx & @{command "by"}~@{text cheating} \\
3.84 + \end{matharray}
3.85 +*}
3.86 +
3.87 +
3.88 +subsection {* Diagnostic commands *}
3.89 +
3.90 +text {*
3.91 + \begin{tabular}{ll}
3.92 + @{command "pr"} & print current state \\
3.93 + @{command "thm"}~@{text a} & print fact \\
3.94 + @{command "term"}~@{text t} & print term \\
3.95 + @{command "prop"}~@{text \<phi>} & print meta-level proposition \\
3.96 + @{command "typ"}~@{text \<tau>} & print meta-level type \\
3.97 + \end{tabular}
3.98 +*}
3.99 +
3.100 +
3.101 +section {* Proof methods *}
3.102 +
3.103 +text {*
3.104 + \begin{tabular}{ll}
3.105 + \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
3.106 + @{method assumption} & apply some assumption \\
3.107 + @{method this} & apply current facts \\
3.108 + @{method rule}~@{text a} & apply some rule \\
3.109 + @{method rule} & apply standard rule (default for @{command "proof"}) \\
3.110 + @{method contradiction} & apply @{text "\<not>"} elimination rule (any order) \\
3.111 + @{method cases}~@{text t} & case analysis (provides cases) \\
3.112 + @{method induct}~@{text x} & proof by induction (provides cases) \\[2ex]
3.113 +
3.114 + \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
3.115 + @{method "-"} & no rules \\
3.116 + @{method intro}~@{text a} & introduction rules \\
3.117 + @{method intro_classes} & class introduction rules \\
3.118 + @{method elim}~@{text a} & elimination rules \\
3.119 + @{method unfold}~@{text a} & definitional rewrite rules \\[2ex]
3.120 +
3.121 + \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts)}} \\[0.5ex]
3.122 + @{method iprover} & intuitionistic proof search \\
3.123 + @{method blast}, @{method fast} & Classical Reasoner \\
3.124 + @{method simp}, @{method simp_all} & Simplifier (+ Splitter) \\
3.125 + @{method auto}, @{method force} & Simplifier + Classical Reasoner \\
3.126 + @{method arith} & Arithmetic procedures \\
3.127 + \end{tabular}
3.128 +*}
3.129 +
3.130 +
3.131 +section {* Attributes *}
3.132 +
3.133 +text {*
3.134 + \begin{tabular}{ll}
3.135 + \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
3.136 + @{attribute OF}~@{text a} & rule resolved with facts (skipping ``@{text _}'') \\
3.137 + @{attribute of}~@{text t} & rule instantiated with terms (skipping ``@{text _}'') \\
3.138 + @{attribute "where"}~@{text "x = t"} & rule instantiated with terms, by variable name \\
3.139 + @{attribute symmetric} & resolution with symmetry rule \\
3.140 + @{attribute THEN}~@{text b} & resolution with another rule \\
3.141 + @{attribute rule_format} & result put into standard rule format \\
3.142 + @{attribute elim_format} & destruct rule turned into elimination rule format \\[1ex]
3.143 +
3.144 + \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
3.145 + @{attribute simp} & Simplifier rule \\
3.146 + @{attribute intro}, @{attribute elim}, @{attribute dest} & Pure or Classical Reasoner rule \\
3.147 + @{attribute iff} & Simplifier + Classical Reasoner rule \\
3.148 + @{attribute split} & case split rule \\
3.149 + @{attribute trans} & transitivity rule \\
3.150 + @{attribute sym} & symmetry rule \\
3.151 + \end{tabular}
3.152 +*}
3.153 +
3.154 +
3.155 +section {* Rule declarations and methods *}
3.156 +
3.157 +text {*
3.158 + \begin{tabular}{l|lllll}
3.159 + & @{method rule} & @{method iprover} & @{method blast} & @{method simp} & @{method auto} \\
3.160 + & & & @{method fast} & @{method simp_all} & @{method force} \\
3.161 + \hline
3.162 + @{attribute Pure.elim}@{text "!"} @{attribute Pure.intro}@{text "!"}
3.163 + & @{text "\<times>"} & @{text "\<times>"} \\
3.164 + @{attribute Pure.elim} @{attribute Pure.intro}
3.165 + & @{text "\<times>"} & @{text "\<times>"} \\
3.166 + @{attribute elim}@{text "!"} @{attribute intro}@{text "!"}
3.167 + & @{text "\<times>"} & & @{text "\<times>"} & & @{text "\<times>"} \\
3.168 + @{attribute elim} @{attribute intro}
3.169 + & @{text "\<times>"} & & @{text "\<times>"} & & @{text "\<times>"} \\
3.170 + @{attribute iff}
3.171 + & @{text "\<times>"} & & @{text "\<times>"} & @{text "\<times>"} & @{text "\<times>"} \\
3.172 + @{attribute iff}@{text "?"}
3.173 + & @{text "\<times>"} \\
3.174 + @{attribute elim}@{text "?"} @{attribute intro}@{text "?"}
3.175 + & @{text "\<times>"} \\
3.176 + @{attribute simp}
3.177 + & & & & @{text "\<times>"} & @{text "\<times>"} \\
3.178 + @{attribute cong}
3.179 + & & & & @{text "\<times>"} & @{text "\<times>"} \\
3.180 + @{attribute split}
3.181 + & & & & @{text "\<times>"} & @{text "\<times>"} \\
3.182 + \end{tabular}
3.183 +*}
3.184 +
3.185 +
3.186 +section {* Emulating tactic scripts *}
3.187 +
3.188 +subsection {* Commands *}
3.189 +
3.190 +text {*
3.191 + \begin{tabular}{ll}
3.192 + @{command "apply"}~@{text m} & apply proof method at initial position \\
3.193 + @{command "apply_end"}~@{text m} & apply proof method near terminal position \\
3.194 + @{command "done"} & complete proof \\
3.195 + @{command "defer"}~@{text n} & move subgoal to end \\
3.196 + @{command "prefer"}~@{text n} & move subgoal to beginning \\
3.197 + @{command "back"} & backtrack last command \\
3.198 + \end{tabular}
3.199 +*}
3.200 +
3.201 +
3.202 +subsection {* Methods *}
3.203 +
3.204 +text {*
3.205 + \begin{tabular}{ll}
3.206 + @{method rule_tac}~@{text insts} & resolution (with instantiation) \\
3.207 + @{method erule_tac}~@{text insts} & elim-resolution (with instantiation) \\
3.208 + @{method drule_tac}~@{text insts} & destruct-resolution (with instantiation) \\
3.209 + @{method frule_tac}~@{text insts} & forward-resolution (with instantiation) \\
3.210 + @{method cut_tac}~@{text insts} & insert facts (with instantiation) \\
3.211 + @{method thin_tac}~@{text \<phi>} & delete assumptions \\
3.212 + @{method subgoal_tac}~@{text \<phi>} & new claims \\
3.213 + @{method rename_tac}~@{text x} & rename innermost goal parameters \\
3.214 + @{method rotate_tac}~@{text n} & rotate assumptions of goal \\
3.215 + @{method tactic}~@{text "text"} & arbitrary ML tactic \\
3.216 + @{method case_tac}~@{text t} & exhaustion (datatypes) \\
3.217 + @{method induct_tac}~@{text x} & induction (datatypes) \\
3.218 + @{method ind_cases}~@{text t} & exhaustion + simplification (inductive predicates) \\
3.219 + \end{tabular}
3.220 +*}
3.221 +
3.222 +end
4.1 --- a/doc-src/IsarRef/Thy/ROOT.ML Sat May 03 13:25:27 2008 +0200
4.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML Sat May 03 13:26:08 2008 +0200
4.3 @@ -5,3 +5,4 @@
4.4 use_thy "intro";
4.5 use_thy "syntax";
4.6 use_thy "pure";
4.7 +use_thy "Quick_Reference";
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex Sat May 03 13:26:08 2008 +0200
5.3 @@ -0,0 +1,278 @@
5.4 +%
5.5 +\begin{isabellebody}%
5.6 +\def\isabellecontext{Quick{\isacharunderscore}Reference}%
5.7 +%
5.8 +\isadelimtheory
5.9 +\isanewline
5.10 +\isanewline
5.11 +%
5.12 +\endisadelimtheory
5.13 +%
5.14 +\isatagtheory
5.15 +\isacommand{theory}\isamarkupfalse%
5.16 +\ Quick{\isacharunderscore}Reference\isanewline
5.17 +\isakeyword{imports}\ Main\isanewline
5.18 +\isakeyword{begin}%
5.19 +\endisatagtheory
5.20 +{\isafoldtheory}%
5.21 +%
5.22 +\isadelimtheory
5.23 +%
5.24 +\endisadelimtheory
5.25 +%
5.26 +\isamarkupchapter{Isabelle/Isar quick reference \label{ap:refcard}%
5.27 +}
5.28 +\isamarkuptrue%
5.29 +%
5.30 +\isamarkupsection{Proof commands%
5.31 +}
5.32 +\isamarkuptrue%
5.33 +%
5.34 +\isamarkupsubsection{Primitives and basic syntax%
5.35 +}
5.36 +\isamarkuptrue%
5.37 +%
5.38 +\begin{isamarkuptext}%
5.39 +\begin{tabular}{ll}
5.40 + \mbox{\isa{\isacommand{fix}}}~\isa{x} & augment context by \isa{{\isasymAnd}x{\isachardot}\ {\isasymbox}} \\
5.41 + \mbox{\isa{\isacommand{assume}}}~\isa{a{\isacharcolon}\ {\isasymphi}} & augment context by \isa{{\isasymphi}\ {\isasymLongrightarrow}\ {\isasymbox}} \\
5.42 + \mbox{\isa{\isacommand{then}}} & indicate forward chaining of facts \\
5.43 + \mbox{\isa{\isacommand{have}}}~\isa{a{\isacharcolon}\ {\isasymphi}} & prove local result \\
5.44 + \mbox{\isa{\isacommand{show}}}~\isa{a{\isacharcolon}\ {\isasymphi}} & prove local result, refining some goal \\
5.45 + \mbox{\isa{\isacommand{using}}}~\isa{a} & indicate use of additional facts \\
5.46 + \mbox{\isa{\isacommand{unfolding}}}~\isa{a} & unfold definitional equations \\
5.47 + \mbox{\isa{\isacommand{proof}}}~\isa{m\isactrlsub {\isadigit{1}}}~\dots~\mbox{\isa{\isacommand{qed}}}~\isa{m\isactrlsub {\isadigit{2}}} & indicate proof structure and refinements \\
5.48 + \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\dots~\mbox{\isa{\isacommand{{\isacharbraceright}}}} & indicate explicit blocks \\
5.49 + \mbox{\isa{\isacommand{next}}} & switch blocks \\
5.50 + \mbox{\isa{\isacommand{note}}}~\isa{a\ {\isacharequal}\ b} & reconsider facts \\
5.51 + \mbox{\isa{\isacommand{let}}}~\isa{p\ {\isacharequal}\ t} & abbreviate terms by higher-order matching \\
5.52 + \end{tabular}
5.53 +
5.54 + \begin{matharray}{rcl}
5.55 + \isa{theory{\isasymdash}stmt} & = & \mbox{\isa{\isacommand{theorem}}}~\isa{name{\isacharcolon}\ prop\ proof} \Or \mbox{\isa{\isacommand{definition}}}~\dots \Or \dots \\[1ex]
5.56 + \isa{proof} & = & \isa{prfx\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{proof}}}~\isa{method\ stmt\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{qed}}}~\isa{method} \\
5.57 + & \Or & \isa{prfx\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{done}}} \\[1ex]
5.58 + \isa{prfx} & = & \mbox{\isa{\isacommand{apply}}}~\isa{method} \\
5.59 + & \Or & \mbox{\isa{\isacommand{using}}}~\isa{name\isactrlsup {\isacharplus}} \\
5.60 + & \Or & \mbox{\isa{\isacommand{unfolding}}}~\isa{name\isactrlsup {\isacharplus}} \\
5.61 + \isa{stmt} & = & \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\isa{stmt\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{{\isacharbraceright}}}} \\
5.62 + & \Or & \mbox{\isa{\isacommand{next}}} \\
5.63 + & \Or & \mbox{\isa{\isacommand{note}}}~\isa{name\ {\isacharequal}\ name\isactrlsup {\isacharplus}} \\
5.64 + & \Or & \mbox{\isa{\isacommand{let}}}~\isa{term\ {\isacharequal}\ term} \\
5.65 + & \Or & \mbox{\isa{\isacommand{fix}}}~\isa{var\isactrlsup {\isacharplus}} \\
5.66 + & \Or & \mbox{\isa{\isacommand{assume}}}~\isa{name{\isacharcolon}\ prop\isactrlsup {\isacharplus}} \\
5.67 + & \Or & \mbox{\isa{\isacommand{then}}}\isa{\isactrlsup {\isacharquery}}~\isa{goal} \\
5.68 + \isa{goal} & = & \mbox{\isa{\isacommand{have}}}~\isa{name{\isacharcolon}\ prop\isactrlsup {\isacharplus}\ proof} \\
5.69 + & \Or & \mbox{\isa{\isacommand{show}}}~\isa{name{\isacharcolon}\ prop\isactrlsup {\isacharplus}\ proof} \\
5.70 + \end{matharray}%
5.71 +\end{isamarkuptext}%
5.72 +\isamarkuptrue%
5.73 +%
5.74 +\isamarkupsubsection{Abbreviations and synonyms%
5.75 +}
5.76 +\isamarkuptrue%
5.77 +%
5.78 +\begin{isamarkuptext}%
5.79 +\begin{matharray}{rcl}
5.80 + \mbox{\isa{\isacommand{by}}}~\isa{m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}} & \equiv & \mbox{\isa{\isacommand{proof}}}~\isa{m\isactrlsub {\isadigit{1}}}~\mbox{\isa{\isacommand{qed}}}~\isa{m\isactrlsub {\isadigit{2}}} \\
5.81 + \mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}} & \equiv & \mbox{\isa{\isacommand{by}}}~\isa{rule} \\
5.82 + \mbox{\isa{\isacommand{{\isachardot}}}} & \equiv & \mbox{\isa{\isacommand{by}}}~\isa{this} \\
5.83 + \mbox{\isa{\isacommand{hence}}} & \equiv & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}} \\
5.84 + \mbox{\isa{\isacommand{thus}}} & \equiv & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}} \\
5.85 + \mbox{\isa{\isacommand{from}}}~\isa{a} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{a}~\mbox{\isa{\isacommand{then}}} \\
5.86 + \mbox{\isa{\isacommand{with}}}~\isa{a} & \equiv & \mbox{\isa{\isacommand{from}}}~\isa{a\ {\isasymAND}\ this} \\[1ex]
5.87 + \mbox{\isa{\isacommand{from}}}~\isa{this} & \equiv & \mbox{\isa{\isacommand{then}}} \\
5.88 + \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{have}}} & \equiv & \mbox{\isa{\isacommand{hence}}} \\
5.89 + \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{show}}} & \equiv & \mbox{\isa{\isacommand{thus}}} \\
5.90 + \end{matharray}%
5.91 +\end{isamarkuptext}%
5.92 +\isamarkuptrue%
5.93 +%
5.94 +\isamarkupsubsection{Derived elements%
5.95 +}
5.96 +\isamarkuptrue%
5.97 +%
5.98 +\begin{isamarkuptext}%
5.99 +\begin{matharray}{rcl}
5.100 + \mbox{\isa{\isacommand{also}}}\isa{\isactrlsub {\isadigit{0}}} & \approx & \mbox{\isa{\isacommand{note}}}~\isa{calculation\ {\isacharequal}\ this} \\
5.101 + \mbox{\isa{\isacommand{also}}}\isa{\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}} & \approx & \mbox{\isa{\isacommand{note}}}~\isa{calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}} \\
5.102 + \mbox{\isa{\isacommand{finally}}} & \approx & \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
5.103 + \mbox{\isa{\isacommand{moreover}}} & \approx & \mbox{\isa{\isacommand{note}}}~\isa{calculation\ {\isacharequal}\ calculation\ this} \\
5.104 + \mbox{\isa{\isacommand{ultimately}}} & \approx & \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
5.105 + \mbox{\isa{\isacommand{presume}}}~\isa{a{\isacharcolon}\ {\isasymphi}} & \approx & \mbox{\isa{\isacommand{assume}}}~\isa{a{\isacharcolon}\ {\isasymphi}} \\
5.106 + \mbox{\isa{\isacommand{def}}}~\isa{a{\isacharcolon}\ x\ {\isasymequiv}\ t} & \approx & \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{a{\isacharcolon}\ x\ {\isasymequiv}\ t} \\
5.107 + \mbox{\isa{\isacommand{obtain}}}~\isa{x\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}} & \approx & \dots~\mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{a{\isacharcolon}\ {\isasymphi}} \\
5.108 + \mbox{\isa{\isacommand{case}}}~\isa{c} & \approx & \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{c{\isacharcolon}\ {\isasymphi}} \\
5.109 + \mbox{\isa{\isacommand{sorry}}} & \approx & \mbox{\isa{\isacommand{by}}}~\isa{cheating} \\
5.110 + \end{matharray}%
5.111 +\end{isamarkuptext}%
5.112 +\isamarkuptrue%
5.113 +%
5.114 +\isamarkupsubsection{Diagnostic commands%
5.115 +}
5.116 +\isamarkuptrue%
5.117 +%
5.118 +\begin{isamarkuptext}%
5.119 +\begin{tabular}{ll}
5.120 + \mbox{\isa{\isacommand{pr}}} & print current state \\
5.121 + \mbox{\isa{\isacommand{thm}}}~\isa{a} & print fact \\
5.122 + \mbox{\isa{\isacommand{term}}}~\isa{t} & print term \\
5.123 + \mbox{\isa{\isacommand{prop}}}~\isa{{\isasymphi}} & print meta-level proposition \\
5.124 + \mbox{\isa{\isacommand{typ}}}~\isa{{\isasymtau}} & print meta-level type \\
5.125 + \end{tabular}%
5.126 +\end{isamarkuptext}%
5.127 +\isamarkuptrue%
5.128 +%
5.129 +\isamarkupsection{Proof methods%
5.130 +}
5.131 +\isamarkuptrue%
5.132 +%
5.133 +\begin{isamarkuptext}%
5.134 +\begin{tabular}{ll}
5.135 + \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
5.136 + \mbox{\isa{assumption}} & apply some assumption \\
5.137 + \mbox{\isa{this}} & apply current facts \\
5.138 + \mbox{\isa{rule}}~\isa{a} & apply some rule \\
5.139 + \mbox{\isa{rule}} & apply standard rule (default for \mbox{\isa{\isacommand{proof}}}) \\
5.140 + \mbox{\isa{contradiction}} & apply \isa{{\isasymnot}} elimination rule (any order) \\
5.141 + \mbox{\isa{cases}}~\isa{t} & case analysis (provides cases) \\
5.142 + \mbox{\isa{induct}}~\isa{x} & proof by induction (provides cases) \\[2ex]
5.143 +
5.144 + \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
5.145 + \mbox{\isa{{\isacharminus}}} & no rules \\
5.146 + \mbox{\isa{intro}}~\isa{a} & introduction rules \\
5.147 + \mbox{\isa{intro{\isacharunderscore}classes}} & class introduction rules \\
5.148 + \mbox{\isa{elim}}~\isa{a} & elimination rules \\
5.149 + \mbox{\isa{unfold}}~\isa{a} & definitional rewrite rules \\[2ex]
5.150 +
5.151 + \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts)}} \\[0.5ex]
5.152 + \mbox{\isa{iprover}} & intuitionistic proof search \\
5.153 + \mbox{\isa{blast}}, \mbox{\isa{fast}} & Classical Reasoner \\
5.154 + \mbox{\isa{simp}}, \mbox{\isa{simp{\isacharunderscore}all}} & Simplifier (+ Splitter) \\
5.155 + \mbox{\isa{auto}}, \mbox{\isa{force}} & Simplifier + Classical Reasoner \\
5.156 + \mbox{\isa{arith}} & Arithmetic procedures \\
5.157 + \end{tabular}%
5.158 +\end{isamarkuptext}%
5.159 +\isamarkuptrue%
5.160 +%
5.161 +\isamarkupsection{Attributes%
5.162 +}
5.163 +\isamarkuptrue%
5.164 +%
5.165 +\begin{isamarkuptext}%
5.166 +\begin{tabular}{ll}
5.167 + \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
5.168 + \mbox{\isa{OF}}~\isa{a} & rule resolved with facts (skipping ``\isa{{\isacharunderscore}}'') \\
5.169 + \mbox{\isa{of}}~\isa{t} & rule instantiated with terms (skipping ``\isa{{\isacharunderscore}}'') \\
5.170 + \mbox{\isa{where}}~\isa{x\ {\isacharequal}\ t} & rule instantiated with terms, by variable name \\
5.171 + \mbox{\isa{symmetric}} & resolution with symmetry rule \\
5.172 + \mbox{\isa{THEN}}~\isa{b} & resolution with another rule \\
5.173 + \mbox{\isa{rule{\isacharunderscore}format}} & result put into standard rule format \\
5.174 + \mbox{\isa{elim{\isacharunderscore}format}} & destruct rule turned into elimination rule format \\[1ex]
5.175 +
5.176 + \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
5.177 + \mbox{\isa{simp}} & Simplifier rule \\
5.178 + \mbox{\isa{intro}}, \mbox{\isa{elim}}, \mbox{\isa{dest}} & Pure or Classical Reasoner rule \\
5.179 + \mbox{\isa{iff}} & Simplifier + Classical Reasoner rule \\
5.180 + \mbox{\isa{split}} & case split rule \\
5.181 + \mbox{\isa{trans}} & transitivity rule \\
5.182 + \mbox{\isa{sym}} & symmetry rule \\
5.183 + \end{tabular}%
5.184 +\end{isamarkuptext}%
5.185 +\isamarkuptrue%
5.186 +%
5.187 +\isamarkupsection{Rule declarations and methods%
5.188 +}
5.189 +\isamarkuptrue%
5.190 +%
5.191 +\begin{isamarkuptext}%
5.192 +\begin{tabular}{l|lllll}
5.193 + & \mbox{\isa{rule}} & \mbox{\isa{iprover}} & \mbox{\isa{blast}} & \mbox{\isa{simp}} & \mbox{\isa{auto}} \\
5.194 + & & & \mbox{\isa{fast}} & \mbox{\isa{simp{\isacharunderscore}all}} & \mbox{\isa{force}} \\
5.195 + \hline
5.196 + \mbox{\isa{Pure{\isachardot}elim}}\isa{{\isacharbang}} \mbox{\isa{Pure{\isachardot}intro}}\isa{{\isacharbang}}
5.197 + & \isa{{\isasymtimes}} & \isa{{\isasymtimes}} \\
5.198 + \mbox{\isa{Pure{\isachardot}elim}} \mbox{\isa{Pure{\isachardot}intro}}
5.199 + & \isa{{\isasymtimes}} & \isa{{\isasymtimes}} \\
5.200 + \mbox{\isa{elim}}\isa{{\isacharbang}} \mbox{\isa{intro}}\isa{{\isacharbang}}
5.201 + & \isa{{\isasymtimes}} & & \isa{{\isasymtimes}} & & \isa{{\isasymtimes}} \\
5.202 + \mbox{\isa{elim}} \mbox{\isa{intro}}
5.203 + & \isa{{\isasymtimes}} & & \isa{{\isasymtimes}} & & \isa{{\isasymtimes}} \\
5.204 + \mbox{\isa{iff}}
5.205 + & \isa{{\isasymtimes}} & & \isa{{\isasymtimes}} & \isa{{\isasymtimes}} & \isa{{\isasymtimes}} \\
5.206 + \mbox{\isa{iff}}\isa{{\isacharquery}}
5.207 + & \isa{{\isasymtimes}} \\
5.208 + \mbox{\isa{elim}}\isa{{\isacharquery}} \mbox{\isa{intro}}\isa{{\isacharquery}}
5.209 + & \isa{{\isasymtimes}} \\
5.210 + \mbox{\isa{simp}}
5.211 + & & & & \isa{{\isasymtimes}} & \isa{{\isasymtimes}} \\
5.212 + \mbox{\isa{cong}}
5.213 + & & & & \isa{{\isasymtimes}} & \isa{{\isasymtimes}} \\
5.214 + \mbox{\isa{split}}
5.215 + & & & & \isa{{\isasymtimes}} & \isa{{\isasymtimes}} \\
5.216 + \end{tabular}%
5.217 +\end{isamarkuptext}%
5.218 +\isamarkuptrue%
5.219 +%
5.220 +\isamarkupsection{Emulating tactic scripts%
5.221 +}
5.222 +\isamarkuptrue%
5.223 +%
5.224 +\isamarkupsubsection{Commands%
5.225 +}
5.226 +\isamarkuptrue%
5.227 +%
5.228 +\begin{isamarkuptext}%
5.229 +\begin{tabular}{ll}
5.230 + \mbox{\isa{\isacommand{apply}}}~\isa{m} & apply proof method at initial position \\
5.231 + \mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}~\isa{m} & apply proof method near terminal position \\
5.232 + \mbox{\isa{\isacommand{done}}} & complete proof \\
5.233 + \mbox{\isa{\isacommand{defer}}}~\isa{n} & move subgoal to end \\
5.234 + \mbox{\isa{\isacommand{prefer}}}~\isa{n} & move subgoal to beginning \\
5.235 + \mbox{\isa{\isacommand{back}}} & backtrack last command \\
5.236 + \end{tabular}%
5.237 +\end{isamarkuptext}%
5.238 +\isamarkuptrue%
5.239 +%
5.240 +\isamarkupsubsection{Methods%
5.241 +}
5.242 +\isamarkuptrue%
5.243 +%
5.244 +\begin{isamarkuptext}%
5.245 +\begin{tabular}{ll}
5.246 + \mbox{\isa{rule{\isacharunderscore}tac}}~\isa{insts} & resolution (with instantiation) \\
5.247 + \mbox{\isa{erule{\isacharunderscore}tac}}~\isa{insts} & elim-resolution (with instantiation) \\
5.248 + \mbox{\isa{drule{\isacharunderscore}tac}}~\isa{insts} & destruct-resolution (with instantiation) \\
5.249 + \mbox{\isa{frule{\isacharunderscore}tac}}~\isa{insts} & forward-resolution (with instantiation) \\
5.250 + \mbox{\isa{cut{\isacharunderscore}tac}}~\isa{insts} & insert facts (with instantiation) \\
5.251 + \mbox{\isa{thin{\isacharunderscore}tac}}~\isa{{\isasymphi}} & delete assumptions \\
5.252 + \mbox{\isa{subgoal{\isacharunderscore}tac}}~\isa{{\isasymphi}} & new claims \\
5.253 + \mbox{\isa{rename{\isacharunderscore}tac}}~\isa{x} & rename innermost goal parameters \\
5.254 + \mbox{\isa{rotate{\isacharunderscore}tac}}~\isa{n} & rotate assumptions of goal \\
5.255 + \mbox{\isa{tactic}}~\isa{text} & arbitrary ML tactic \\
5.256 + \mbox{\isa{case{\isacharunderscore}tac}}~\isa{t} & exhaustion (datatypes) \\
5.257 + \mbox{\isa{induct{\isacharunderscore}tac}}~\isa{x} & induction (datatypes) \\
5.258 + \mbox{\isa{ind{\isacharunderscore}cases}}~\isa{t} & exhaustion + simplification (inductive predicates) \\
5.259 + \end{tabular}%
5.260 +\end{isamarkuptext}%
5.261 +\isamarkuptrue%
5.262 +%
5.263 +\isadelimtheory
5.264 +%
5.265 +\endisadelimtheory
5.266 +%
5.267 +\isatagtheory
5.268 +\isacommand{end}\isamarkupfalse%
5.269 +%
5.270 +\endisatagtheory
5.271 +{\isafoldtheory}%
5.272 +%
5.273 +\isadelimtheory
5.274 +%
5.275 +\endisadelimtheory
5.276 +\isanewline
5.277 +\end{isabellebody}%
5.278 +%%% Local Variables:
5.279 +%%% mode: latex
5.280 +%%% TeX-master: "root"
5.281 +%%% End:
6.1 --- a/doc-src/IsarRef/Thy/document/session.tex Sat May 03 13:25:27 2008 +0200
6.2 +++ b/doc-src/IsarRef/Thy/document/session.tex Sat May 03 13:26:08 2008 +0200
6.3 @@ -4,6 +4,8 @@
6.4
6.5 \input{pure.tex}
6.6
6.7 +\input{Quick_Reference.tex}
6.8 +
6.9 %%% Local Variables:
6.10 %%% mode: latex
6.11 %%% TeX-master: "root"
7.1 --- a/doc-src/IsarRef/isar-ref.tex Sat May 03 13:25:27 2008 +0200
7.2 +++ b/doc-src/IsarRef/isar-ref.tex Sat May 03 13:26:08 2008 +0200
7.3 @@ -76,7 +76,7 @@
7.4 \input{logics.tex}
7.5
7.6 \appendix
7.7 -\input{refcard.tex}
7.8 +\input{Thy/document/Quick_Reference.tex}
7.9 \input{conversion.tex}
7.10
7.11 \begingroup
8.1 --- a/doc-src/IsarRef/refcard.tex Sat May 03 13:25:27 2008 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,192 +0,0 @@
8.4 -
8.5 -\chapter{Isabelle/Isar quick reference}\label{ap:refcard}
8.6 -
8.7 -\section{Proof commands}
8.8 -
8.9 -\subsection{Primitives and basic syntax}
8.10 -
8.11 -\begin{tabular}{ll}
8.12 - $\FIX{\vec x}$ & augment context by $\All {\vec x} \Box$ \\
8.13 - $\ASSUME{a}{\vec\phi}$ & augment context by $\vec\phi \Imp \Box$ \\
8.14 - $\THEN$ & indicate forward chaining of facts \\
8.15 - $\HAVE{a}{\phi}$ & prove local result \\
8.16 - $\SHOW{a}{\phi}$ & prove local result, refining some goal \\
8.17 - $\USING{\vec a}$ & indicate use of additional facts \\
8.18 - $\UNFOLDING{\vec a}$ & unfold definitional equations \\
8.19 - $\PROOF{m@1}~\dots~\QED{m@2}$ & indicate proof structure and refinements \\
8.20 - $\BG~\dots~\EN$ & declare explicit blocks \\
8.21 - $\NEXT$ & switch blocks \\
8.22 - $\NOTE{a}{\vec b}$ & reconsider facts \\
8.23 - $\LET{p = t}$ & \Text{abbreviate terms by higher-order matching} \\
8.24 -\end{tabular}
8.25 -
8.26 -\begin{matharray}{rcl}
8.27 - theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \Or \isarkeyword{definition}~\dots \Or \dots \\[1ex]
8.28 - proof & = & prfx^*~\PROOF{method}~stmt^*~\QED{method} \\
8.29 - & \Or & prfx^*~\DONE \\[1ex]
8.30 - prfx & = & \APPLY{method} \\
8.31 - & \Or & \USING{name^+} \\
8.32 - & \Or & \UNFOLDING{name^+} \\
8.33 - stmt & = & \BG~stmt^*~\EN \\
8.34 - & \Or & \NEXT \\
8.35 - & \Or & \NOTE{name}{name^+} \\
8.36 - & \Or & \LET{term = term} \\
8.37 - & \Or & \FIX{var^+} \\
8.38 - & \Or & \ASSUME{name}{prop^+}\\
8.39 - & \Or & \THEN^?~goal \\
8.40 - goal & = & \HAVE{name}{prop}~proof \\
8.41 - & \Or & \SHOW{name}{prop}~proof \\
8.42 -\end{matharray}
8.43 -
8.44 -
8.45 -\subsection{Abbreviations and synonyms}
8.46 -
8.47 -\begin{matharray}{rcl}
8.48 - \BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\
8.49 - \DDOT & \equiv & \BY{rule} \\
8.50 - \DOT & \equiv & \BY{this} \\
8.51 - \HENCENAME & \equiv & \THEN~\HAVENAME \\
8.52 - \THUSNAME & \equiv & \THEN~\SHOWNAME \\
8.53 - \FROM{\vec a} & \equiv & \NOTE{this}{\vec a}~\THEN \\
8.54 - \WITH{\vec a} & \equiv & \FROM{\vec a~\AND~this} \\[1ex]
8.55 - \FROM{this} & \equiv & \THEN \\
8.56 - \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\
8.57 - \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\
8.58 -\end{matharray}
8.59 -
8.60 -
8.61 -\subsection{Derived elements}
8.62 -
8.63 -\begin{matharray}{rcl}
8.64 - \ALSO@0 & \approx & \NOTE{calculation}{this} \\
8.65 - \ALSO@{n+1} & \approx & \NOTE{calculation}{trans~[OF~calculation~this]} \\
8.66 - \FINALLY & \approx & \ALSO~\FROM{calculation} \\[0.5ex]
8.67 - \MOREOVER & \approx & \NOTE{calculation}{calculation~this} \\
8.68 - \ULTIMATELY & \approx & \MOREOVER~\FROM{calculation} \\[0.5ex]
8.69 - \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi} \\
8.70 -% & & \Text{(permissive assumption)} \\
8.71 - \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\
8.72 -% & & \Text{(definitional assumption)} \\
8.73 - \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
8.74 -% & & \Text{(generalized existence)} \\
8.75 - \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\
8.76 -% & & \Text{(named context)} \\[0.5ex]
8.77 - \SORRY & \approx & \BY{cheating} \\
8.78 -\end{matharray}
8.79 -
8.80 -
8.81 -\subsection{Diagnostic commands}
8.82 -
8.83 -\begin{matharray}{ll}
8.84 - \isarkeyword{pr} & \Text{print current state} \\
8.85 - \isarkeyword{thm}~\vec a & \Text{print theorems} \\
8.86 - \isarkeyword{term}~t & \Text{print term} \\
8.87 - \isarkeyword{prop}~\phi & \Text{print meta-level proposition} \\
8.88 - \isarkeyword{typ}~\tau & \Text{print meta-level type} \\
8.89 -\end{matharray}
8.90 -
8.91 -
8.92 -\section{Proof methods}
8.93 -
8.94 -\begin{tabular}{ll}
8.95 - \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
8.96 - $assumption$ & apply some assumption \\
8.97 - $this$ & apply current facts \\
8.98 - $rule~\vec a$ & apply some rule \\
8.99 - $rule$ & apply standard rule (default for $\PROOFNAME$) \\
8.100 - $contradiction$ & apply $\neg{}$ elimination rule (any order) \\
8.101 - $cases~t$ & case analysis (provides cases) \\
8.102 - $induct~\vec x$ & proof by induction (provides cases) \\[2ex]
8.103 -
8.104 - \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
8.105 - $-$ & \Text{no rules} \\
8.106 - $intro~\vec a$ & \Text{introduction rules} \\
8.107 - $intro_classes$ & \Text{class introduction rules} \\
8.108 - $elim~\vec a$ & \Text{elimination rules} \\
8.109 - $unfold~\vec a$ & \Text{definitions} \\[2ex]
8.110 -
8.111 - \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
8.112 - $rules$ & \Text{intuitionistic proof search} \\
8.113 - $blast$, $fast$ & Classical Reasoner \\
8.114 - $simp$, $simp_all$ & Simplifier (+ Splitter) \\
8.115 - $auto$, $force$ & Simplifier + Classical Reasoner \\
8.116 - $arith$ & Arithmetic procedure \\
8.117 -\end{tabular}
8.118 -
8.119 -
8.120 -\section{Attributes}
8.121 -
8.122 -\begin{tabular}{ll}
8.123 - \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
8.124 - $OF~\vec a$ & rule resolved with facts (skipping ``$_$'') \\
8.125 - $of~\vec t$ & rule instantiated with terms (skipping ``$_$'') \\
8.126 - $where~\vec x = \vec t$ & rule instantiated with terms, by variable name \\
8.127 - $symmetric$ & resolution with symmetry rule \\
8.128 - $THEN~b$ & resolution with another rule \\
8.129 - $rule_format$ & result put into standard rule format \\
8.130 - $elim_format$ & destruct rule turned into elimination rule format \\[1ex]
8.131 -
8.132 - \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
8.133 - $simp$ & Simplifier rule \\
8.134 - $intro$, $elim$, $dest$ & Pure or Classical Reasoner rule \\
8.135 - $iff$ & Simplifier + Classical Reasoner rule \\
8.136 - $split$ & case split rule \\
8.137 - $trans$ & transitivity rule \\
8.138 - $sym$ & symmetry rule \\
8.139 -\end{tabular}
8.140 -
8.141 -
8.142 -\section{Rule declarations and methods}
8.143 -
8.144 -\begin{tabular}{l|lllll}
8.145 - & $rule$ & $rules$ & $blast$ etc. & $simp$ etc. & $auto$ etc. \\
8.146 - \hline
8.147 - $elim!$ $intro!$ (Pure) & $\times$ & $\times$ \\
8.148 - $elim$ $intro$ (Pure) & $\times$ & $\times$ \\
8.149 - $elim!$ $intro!$ & $\times$ & & $\times$ & & $\times$ \\
8.150 - $elim$ $intro$ & $\times$ & & $\times$ & & $\times$ \\
8.151 - $iff$ & $\times$ & & $\times$ & $\times$ & $\times$ \\
8.152 - $iff?$ & $\times$ \\
8.153 - $elim?$ $intro?$ & $\times$ \\
8.154 - $simp$ & & & & $\times$ & $\times$ \\
8.155 - $cong$ & & & & $\times$ & $\times$ \\
8.156 - $split$ & & & & $\times$ & $\times$ \\
8.157 -\end{tabular}
8.158 -
8.159 -
8.160 -\section{Emulating tactic scripts}
8.161 -
8.162 -\subsection{Commands}
8.163 -
8.164 -\begin{tabular}{ll}
8.165 - $\APPLY{m}$ & apply proof method at initial position \\
8.166 - $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\
8.167 - $\isarkeyword{done}$ & complete proof \\
8.168 - $\isarkeyword{defer}~n$ & move subgoal to end \\
8.169 - $\isarkeyword{prefer}~n$ & move subgoal to beginning \\
8.170 - $\isarkeyword{back}$ & backtrack last command \\
8.171 -\end{tabular}
8.172 -
8.173 -\subsection{Methods}
8.174 -
8.175 -\begin{tabular}{ll}
8.176 - $rule_tac~insts$ & resolution (with instantiation) \\
8.177 - $erule_tac~insts$ & elim-resolution (with instantiation) \\
8.178 - $drule_tac~insts$ & destruct-resolution (with instantiation) \\
8.179 - $frule_tac~insts$ & forward-resolution (with instantiation) \\
8.180 - $cut_tac~insts$ & insert facts (with instantiation) \\
8.181 - $thin_tac~\phi$ & delete assumptions \\
8.182 - $subgoal_tac~\phi$ & new claims \\
8.183 - $rename_tac~\vec x$ & rename suffix of goal parameters \\
8.184 - $rotate_tac~n$ & rotate assumptions of goal \\
8.185 - $tactic~text$ & arbitrary ML tactic \\
8.186 - $case_tac~t$ & exhaustion (datatypes) \\
8.187 - $induct_tac~\vec x$ & induction (datatypes) \\
8.188 - $ind_cases~t$ & exhaustion + simplification (inductive sets) \\
8.189 -\end{tabular}
8.190 -
8.191 -
8.192 -%%% Local Variables:
8.193 -%%% mode: latex
8.194 -%%% TeX-master: "isar-ref"
8.195 -%%% End: