1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/IsarRef/Thy/Quick_Reference.thy Sat May 03 13:26:08 2008 +0200
1.3 @@ -0,0 +1,219 @@
1.4 +(* $Id$ *)
1.5 +
1.6 +theory Quick_Reference
1.7 +imports Main
1.8 +begin
1.9 +
1.10 +chapter {* Isabelle/Isar quick reference \label{ap:refcard} *}
1.11 +
1.12 +section {* Proof commands *}
1.13 +
1.14 +subsection {* Primitives and basic syntax *}
1.15 +
1.16 +text {*
1.17 + \begin{tabular}{ll}
1.18 + @{command "fix"}~@{text x} & augment context by @{text "\<And>x. \<box>"} \\
1.19 + @{command "assume"}~@{text "a: \<phi>"} & augment context by @{text "\<phi> \<Longrightarrow> \<box>"} \\
1.20 + @{command "then"} & indicate forward chaining of facts \\
1.21 + @{command "have"}~@{text "a: \<phi>"} & prove local result \\
1.22 + @{command "show"}~@{text "a: \<phi>"} & prove local result, refining some goal \\
1.23 + @{command "using"}~@{text a} & indicate use of additional facts \\
1.24 + @{command "unfolding"}~@{text a} & unfold definitional equations \\
1.25 + @{command "proof"}~@{text "m\<^sub>1"}~\dots~@{command "qed"}~@{text "m\<^sub>2"} & indicate proof structure and refinements \\
1.26 + @{command "{"}~\dots~@{command "}"} & indicate explicit blocks \\
1.27 + @{command "next"} & switch blocks \\
1.28 + @{command "note"}~@{text "a = b"} & reconsider facts \\
1.29 + @{command "let"}~@{text "p = t"} & abbreviate terms by higher-order matching \\
1.30 + \end{tabular}
1.31 +
1.32 + \begin{matharray}{rcl}
1.33 + @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: prop proof"} \Or @{command "definition"}~\dots \Or \dots \\[1ex]
1.34 + @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method stmt\<^sup>*"}~@{command "qed"}~@{text method} \\
1.35 + & \Or & @{text "prfx\<^sup>*"}~@{command "done"} \\[1ex]
1.36 + @{text prfx} & = & @{command "apply"}~@{text method} \\
1.37 + & \Or & @{command "using"}~@{text "name\<^sup>+"} \\
1.38 + & \Or & @{command "unfolding"}~@{text "name\<^sup>+"} \\
1.39 + @{text stmt} & = & @{command "{"}~@{text "stmt\<^sup>*"}~@{command "}"} \\
1.40 + & \Or & @{command "next"} \\
1.41 + & \Or & @{command "note"}~@{text "name = name\<^sup>+"} \\
1.42 + & \Or & @{command "let"}~@{text "term = term"} \\
1.43 + & \Or & @{command "fix"}~@{text "var\<^sup>+"} \\
1.44 + & \Or & @{command "assume"}~@{text "name: prop\<^sup>+"} \\
1.45 + & \Or & @{command "then"}@{text "\<^sup>?"}~@{text goal} \\
1.46 + @{text goal} & = & @{command "have"}~@{text "name: prop\<^sup>+ proof"} \\
1.47 + & \Or & @{command "show"}~@{text "name: prop\<^sup>+ proof"} \\
1.48 + \end{matharray}
1.49 +*}
1.50 +
1.51 +
1.52 +subsection {* Abbreviations and synonyms *}
1.53 +
1.54 +text {*
1.55 + \begin{matharray}{rcl}
1.56 + @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} & \equiv & @{command "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"} \\
1.57 + @{command ".."} & \equiv & @{command "by"}~@{text rule} \\
1.58 + @{command "."} & \equiv & @{command "by"}~@{text this} \\
1.59 + @{command "hence"} & \equiv & @{command "then"}~@{command "have"} \\
1.60 + @{command "thus"} & \equiv & @{command "then"}~@{command "show"} \\
1.61 + @{command "from"}~@{text a} & \equiv & @{command "note"}~@{text a}~@{command "then"} \\
1.62 + @{command "with"}~@{text a} & \equiv & @{command "from"}~@{text "a \<AND> this"} \\[1ex]
1.63 + @{command "from"}~@{text this} & \equiv & @{command "then"} \\
1.64 + @{command "from"}~@{text this}~@{command "have"} & \equiv & @{command "hence"} \\
1.65 + @{command "from"}~@{text this}~@{command "show"} & \equiv & @{command "thus"} \\
1.66 + \end{matharray}
1.67 +*}
1.68 +
1.69 +
1.70 +subsection {* Derived elements *}
1.71 +
1.72 +text {*
1.73 + \begin{matharray}{rcl}
1.74 + @{command "also"}@{text "\<^sub>0"} & \approx & @{command "note"}~@{text "calculation = this"} \\
1.75 + @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \approx & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\
1.76 + @{command "finally"} & \approx & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
1.77 + @{command "moreover"} & \approx & @{command "note"}~@{text "calculation = calculation this"} \\
1.78 + @{command "ultimately"} & \approx & @{command "moreover"}~@{command "from"}~@{text calculation} \\[0.5ex]
1.79 + @{command "presume"}~@{text "a: \<phi>"} & \approx & @{command "assume"}~@{text "a: \<phi>"} \\
1.80 + @{command "def"}~@{text "a: x \<equiv> t"} & \approx & @{command "fix"}~@{text x}~@{command "assume"}~@{text "a: x \<equiv> t"} \\
1.81 + @{command "obtain"}~@{text "x \<WHERE> a: \<phi>"} & \approx & \dots~@{command "fix"}~@{text x}~@{command "assume"}~@{text "a: \<phi>"} \\
1.82 + @{command "case"}~@{text c} & \approx & @{command "fix"}~@{text x}~@{command "assume"}~@{text "c: \<phi>"} \\
1.83 + @{command "sorry"} & \approx & @{command "by"}~@{text cheating} \\
1.84 + \end{matharray}
1.85 +*}
1.86 +
1.87 +
1.88 +subsection {* Diagnostic commands *}
1.89 +
1.90 +text {*
1.91 + \begin{tabular}{ll}
1.92 + @{command "pr"} & print current state \\
1.93 + @{command "thm"}~@{text a} & print fact \\
1.94 + @{command "term"}~@{text t} & print term \\
1.95 + @{command "prop"}~@{text \<phi>} & print meta-level proposition \\
1.96 + @{command "typ"}~@{text \<tau>} & print meta-level type \\
1.97 + \end{tabular}
1.98 +*}
1.99 +
1.100 +
1.101 +section {* Proof methods *}
1.102 +
1.103 +text {*
1.104 + \begin{tabular}{ll}
1.105 + \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
1.106 + @{method assumption} & apply some assumption \\
1.107 + @{method this} & apply current facts \\
1.108 + @{method rule}~@{text a} & apply some rule \\
1.109 + @{method rule} & apply standard rule (default for @{command "proof"}) \\
1.110 + @{method contradiction} & apply @{text "\<not>"} elimination rule (any order) \\
1.111 + @{method cases}~@{text t} & case analysis (provides cases) \\
1.112 + @{method induct}~@{text x} & proof by induction (provides cases) \\[2ex]
1.113 +
1.114 + \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
1.115 + @{method "-"} & no rules \\
1.116 + @{method intro}~@{text a} & introduction rules \\
1.117 + @{method intro_classes} & class introduction rules \\
1.118 + @{method elim}~@{text a} & elimination rules \\
1.119 + @{method unfold}~@{text a} & definitional rewrite rules \\[2ex]
1.120 +
1.121 + \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts)}} \\[0.5ex]
1.122 + @{method iprover} & intuitionistic proof search \\
1.123 + @{method blast}, @{method fast} & Classical Reasoner \\
1.124 + @{method simp}, @{method simp_all} & Simplifier (+ Splitter) \\
1.125 + @{method auto}, @{method force} & Simplifier + Classical Reasoner \\
1.126 + @{method arith} & Arithmetic procedures \\
1.127 + \end{tabular}
1.128 +*}
1.129 +
1.130 +
1.131 +section {* Attributes *}
1.132 +
1.133 +text {*
1.134 + \begin{tabular}{ll}
1.135 + \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
1.136 + @{attribute OF}~@{text a} & rule resolved with facts (skipping ``@{text _}'') \\
1.137 + @{attribute of}~@{text t} & rule instantiated with terms (skipping ``@{text _}'') \\
1.138 + @{attribute "where"}~@{text "x = t"} & rule instantiated with terms, by variable name \\
1.139 + @{attribute symmetric} & resolution with symmetry rule \\
1.140 + @{attribute THEN}~@{text b} & resolution with another rule \\
1.141 + @{attribute rule_format} & result put into standard rule format \\
1.142 + @{attribute elim_format} & destruct rule turned into elimination rule format \\[1ex]
1.143 +
1.144 + \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
1.145 + @{attribute simp} & Simplifier rule \\
1.146 + @{attribute intro}, @{attribute elim}, @{attribute dest} & Pure or Classical Reasoner rule \\
1.147 + @{attribute iff} & Simplifier + Classical Reasoner rule \\
1.148 + @{attribute split} & case split rule \\
1.149 + @{attribute trans} & transitivity rule \\
1.150 + @{attribute sym} & symmetry rule \\
1.151 + \end{tabular}
1.152 +*}
1.153 +
1.154 +
1.155 +section {* Rule declarations and methods *}
1.156 +
1.157 +text {*
1.158 + \begin{tabular}{l|lllll}
1.159 + & @{method rule} & @{method iprover} & @{method blast} & @{method simp} & @{method auto} \\
1.160 + & & & @{method fast} & @{method simp_all} & @{method force} \\
1.161 + \hline
1.162 + @{attribute Pure.elim}@{text "!"} @{attribute Pure.intro}@{text "!"}
1.163 + & @{text "\<times>"} & @{text "\<times>"} \\
1.164 + @{attribute Pure.elim} @{attribute Pure.intro}
1.165 + & @{text "\<times>"} & @{text "\<times>"} \\
1.166 + @{attribute elim}@{text "!"} @{attribute intro}@{text "!"}
1.167 + & @{text "\<times>"} & & @{text "\<times>"} & & @{text "\<times>"} \\
1.168 + @{attribute elim} @{attribute intro}
1.169 + & @{text "\<times>"} & & @{text "\<times>"} & & @{text "\<times>"} \\
1.170 + @{attribute iff}
1.171 + & @{text "\<times>"} & & @{text "\<times>"} & @{text "\<times>"} & @{text "\<times>"} \\
1.172 + @{attribute iff}@{text "?"}
1.173 + & @{text "\<times>"} \\
1.174 + @{attribute elim}@{text "?"} @{attribute intro}@{text "?"}
1.175 + & @{text "\<times>"} \\
1.176 + @{attribute simp}
1.177 + & & & & @{text "\<times>"} & @{text "\<times>"} \\
1.178 + @{attribute cong}
1.179 + & & & & @{text "\<times>"} & @{text "\<times>"} \\
1.180 + @{attribute split}
1.181 + & & & & @{text "\<times>"} & @{text "\<times>"} \\
1.182 + \end{tabular}
1.183 +*}
1.184 +
1.185 +
1.186 +section {* Emulating tactic scripts *}
1.187 +
1.188 +subsection {* Commands *}
1.189 +
1.190 +text {*
1.191 + \begin{tabular}{ll}
1.192 + @{command "apply"}~@{text m} & apply proof method at initial position \\
1.193 + @{command "apply_end"}~@{text m} & apply proof method near terminal position \\
1.194 + @{command "done"} & complete proof \\
1.195 + @{command "defer"}~@{text n} & move subgoal to end \\
1.196 + @{command "prefer"}~@{text n} & move subgoal to beginning \\
1.197 + @{command "back"} & backtrack last command \\
1.198 + \end{tabular}
1.199 +*}
1.200 +
1.201 +
1.202 +subsection {* Methods *}
1.203 +
1.204 +text {*
1.205 + \begin{tabular}{ll}
1.206 + @{method rule_tac}~@{text insts} & resolution (with instantiation) \\
1.207 + @{method erule_tac}~@{text insts} & elim-resolution (with instantiation) \\
1.208 + @{method drule_tac}~@{text insts} & destruct-resolution (with instantiation) \\
1.209 + @{method frule_tac}~@{text insts} & forward-resolution (with instantiation) \\
1.210 + @{method cut_tac}~@{text insts} & insert facts (with instantiation) \\
1.211 + @{method thin_tac}~@{text \<phi>} & delete assumptions \\
1.212 + @{method subgoal_tac}~@{text \<phi>} & new claims \\
1.213 + @{method rename_tac}~@{text x} & rename innermost goal parameters \\
1.214 + @{method rotate_tac}~@{text n} & rotate assumptions of goal \\
1.215 + @{method tactic}~@{text "text"} & arbitrary ML tactic \\
1.216 + @{method case_tac}~@{text t} & exhaustion (datatypes) \\
1.217 + @{method induct_tac}~@{text x} & induction (datatypes) \\
1.218 + @{method ind_cases}~@{text t} & exhaustion + simplification (inductive predicates) \\
1.219 + \end{tabular}
1.220 +*}
1.221 +
1.222 +end