Quelle Quick_Reference.thy

Sprache: Isabelle

(*:maxLineLen=78:*)

theory Quick_Reference
imports Main Base
begin

chapter ‹Isabelle/Isar quick reference \label{ap:refcard}›

section ‹Proof commands›

subsection ‹Main grammar \label{ap:main-grammar}›

text ‹
\begin{tabular}{rcl}
‹main› & = & 🪙‹notepad begin "statement^*" end› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹theorem name: props if name: props for vars "proof"› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹theorem name:› \\
& & \quad🪙‹fixes vars› \\
& & \quad🪙‹assumes name: props› \\
& & \quad🪙‹shows name: props "proof"› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹theorem name:› \\
& & \quad🪙‹fixes vars› \\
& & \quad🪙‹assumes name: props› \\
& & \quad🪙‹obtains (name) vars where props | … "proof"› \\
‹proof› & = & 🪙‹"refinement^*" proper_proof› \\
‹refinement› & = & 🪙‹apply method› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹supply name = thms› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹subgoal premises name for vars "proof"› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹using thms› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹unfolding thms› \\
‹proper_proof› & = & 🪙‹proof "method^?" "statement^*" qed "method^?"› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹done› \\
‹statement› & = & 🪙‹{ "statement^*" }› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹next› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹note name = thms› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹let "term" = "term"› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹write name (mixfix)› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹fix vars› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹assume name: props if props for vars› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹then"^?" goal› \\
‹goal› & = & 🪙‹have name: props if name: props for vars "proof"› \\
& ‹|› & nd='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹show name: props if name: props for vars "proof"› \\
\end{tabular}
›

subsection ‹Primitives›

text ‹
\begin{tabular}{ll}
🪙‹fix x› & augment context by ‹∧x. ◻› \\
🪙‹assume a: A› & augment context by ‹A ==> ◻› \\
🪙‹then› & indicate forward chaining of facts \\
🪙‹have a: A› & prove local result \\
🪙‹show a: A› & prove local result, refining some goal \\
🪙‹using a› & indicate use of additional facts \\
🪙‹unfolding a› & unfold definitional equations \\
🪙‹proof m₁ … qed m₂› & indicate proof structure and refinements \\
🪙‹{ … }› & indicate explicit blocks \\
🪙‹next› & switch proof blocks \\
🪙‹note a = b› & reconsider and declare facts \\
🪙‹let p = t› & abbreviate terms by higher-order matching \\
🪙‹write c (mx)› & declare local mixfix syntax \\
\end{tabular}
›

subsection ‹Abbreviations and synonyms›

text ‹
\begin{tabular}{rcl}
🪙‹by m₁ m₂› & ‹≡› & 🪙‹proof m₁ qed m₂› \\
🪙‹..› & ‹≡› & ntouchend='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹by standard› \\
🪙‹.› & ‹≡› & touchend='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹by this› \\
🪙‹from a› & ‹≡› & 🪙‹note a then› \\
🪙‹with a› & ‹≡› & 🪙‹from a and this› \\
🪙‹from this› & ‹≡› & 🪙‹then› \\
\end{tabular}
›

subsection ‹Derived elements›

text ‹
\begin{tabular}{rcl}
🪙‹also"₀"› & ‹≈› & 🪙‹note calculation = this› \\
🪙‹also"_n₊₁"› & ‹≈› & 🪙‹note calculation = trans [OF calculation this]› \\
🪙‹finally› & ‹≈› & 🪙‹also from calculation› \\[0.5ex]
🪙‹moreover› & ‹≈› & 🪙‹note calculation = calculation this› \\
🪙‹ultimately› & ‹≈› & 🪙‹moreover from calculation› \\[0.5ex]
🪙‹presume a: A› & ‹≈› & 🪙‹assume a: A› \\
🪙‹define x where "x = t"› & ‹≈› & 🪙‹fix x assume x_def: "x = t"› \\
🪙‹consider x where A | …› & ‹≈› & 🪙‹have thesis› \\
& & \quad 🪙‹if "∧x. A ==> thesis" and … for thesis› \\
🪙‹obtain x where a: A 🍋› & ‹≈› & 🪙‹consider x where A 🍋› \\
& & 🪙‹fix x assume a: A› \\
🪙‹case c› & ‹≈› & 🪙‹fix x assume c: A› \\
🪙‹sorry› & ‹≈› & ontouchend='alert("unbekannte/s Formatierung/Symbol theory_text");' >🪙‹by cheating› \\
\end{tabular}
›

subsection ‹Diagnostic commands›

text ‹
\begin{tabular}{ll}
🪙‹typ τ› & print type \\
🪙‹term t› & print term \\
🪙‹prop φ› & print proposition \\
🪙‹thm a› & print fact \\
🪙‹print_statement a› & print fact in long statement form \\
\end{tabular}
›

section ‹Proof methods›

text ‹
\begin{tabular}{ll}
\multicolumn{2}{l}{\‹Single steps (forward-chaining facts)›} \\[0.5ex]
@{method assumption} & apply some goal assumption \\
@{method this} & apply current facts \\
@{method rule}~‹a› & apply some rule \\
@{method standard} & apply standard rule (default for @{command "proof"}) \\
@{method contradiction} & apply ‹¬› elimination rule (any order) \\
@{method cases}~‹t› & case analysis (provides cases) \\
@{method induct}~‹x› & proof by induction (provides cases) \\[2ex]

\multicolumn{2}{l}{\‹Repeated steps (inserting facts)›} \\[0.5ex]
@{method "-"} & no rules \\
@{method intro}~‹a› & introduction rules \\
@{method intro_classes} & class introduction rules \\
@{method intro_locales} & locale introduction rules (without body) \\
@{method unfold_locales} & locale introduction rules (with body) \\
@{method elim}~‹a› & elimination rules \\
@{method unfold}~‹a› & definitional rewrite rules \\[2ex]

\multicolumn{2}{l}{\‹Automated proof tools (inserting facts)›} \\[0.5ex]
@{method iprover} & intuitionistic proof search \\
@{method blast}, @{method fast} & Classical Reasoner \\
@{method simp}, @{method simp_all} & Simplifier (+ Splitter) \\
@{method auto}, @{method force} & Simplifier + Classical Reasoner \\
@{method arith} & Arithmetic procedures \\
\end{tabular}
›

section ‹Attributes›

text ‹
\begin{tabular}{ll}
\multicolumn{2}{l}{\‹Rules›} \\[0.5ex]
@{attribute OF}~‹a› & rule resolved with facts (skipping ``‹_›'') \\
@{attribute of}~‹t› & rule instantiated with terms (skipping ``‹_›'') \\
@{attribute "where"}~‹x = t› & rule instantiated with terms, by variable name \\
@{attribute symmetric} & resolution with symmetry rule \\
@{attribute THEN}~‹b› & resolution with another rule \\
@{attribute rule_format} & result put into standard rule format \\
@{attribute elim_format} & destruct rule turned into elimination rule format \\[1ex]

\multicolumn{2}{l}{\‹Declarations›} \\[0.5ex]
@{attribute simp} & Simplifier rule \\
@{attribute intro}, @{attribute elim}, @{attribute dest} & Pure or Classical Reasoner rule \\
@{attribute iff} & Simplifier + Classical Reasoner rule \\
@{attribute split} & case split rule \\
@{attribute trans} & transitivity rule \\
@{attribute sym} & symmetry rule \\
\end{tabular}
›

section ‹Rule declarations and methods›

text ‹
\begin{tabular}{l|lllll}
& @{method rule} & @{method iprover} & @{method blast} & @{method simp} & @{method auto} \\
& & & @{method fast} & @{method simp_all} & @{method force} \\
\hline
@{attribute Pure.elim}‹!› @{attribute Pure.intro}‹!›
& ‹×› & ‹×› \\
@{attribute Pure.elim} @{attribute Pure.intro}
& ‹×› & ‹×› \\
@{attribute elim}‹!› @{attribute intro}‹!›
& ‹×› & & ‹×› & & ‹×› \\
@{attribute elim} @{attribute intro}
& ‹×› & & ‹×› & & ‹×› \\
@{attribute iff}
& ‹×› & & ‹×› & ‹×› & ‹×› \\
@{attribute iff}‹?›
& ‹×› \\
@{attribute elim}‹?› @{attribute intro}‹?›
& ‹×› \\
@{attribute simp}
& & & & ‹×› & ‹×› \\
@{attribute cong}
& & & & ‹×› & ‹×› \\
@{attribute split}
& & & & ‹×› & ‹×› \\
\end{tabular}
›

section ‹Proof scripts›

subsection ‹Commands›

text ‹
\begin{tabular}{ll}
🪙‹apply m› & apply proof method during backwards refinement \\
🪙‹apply_end m› & apply proof method (as if in terminal position) \\
🪙‹supply a› & supply facts during backwards refinement \\
🪙‹subgoal› & nested proof during backwards refinement \\
🪙‹defer n› & move subgoal to end \\
🪙‹prefer n› & move subgoal to start \\
🪙‹back› & backtrack last command \\
🪙‹done› & complete proof \\
\end{tabular}
›

subsection ‹Methods›

text ‹
\begin{tabular}{ll}
@{method rule_tac}~‹insts› & resolution (with instantiation) \\
@{method erule_tac}~‹insts› & elim-resolution (with instantiation) \\
@{method drule_tac}~‹insts› & destruct-resolution (with instantiation) \\
@{method frule_tac}~‹insts› & forward-resolution (with instantiation) \\
@{method cut_tac}~‹insts› & insert facts (with instantiation) \\
@{method thin_tac}~‹φ› & delete assumptions \\
@{method subgoal_tac}~‹φ› & new claims \\
@{method rename_tac}~‹x› & rename innermost goal parameters \\
@{method rotate_tac}~‹n› & rotate assumptions of goal \\
@{method tactic}~‹text› & arbitrary ML tactic \\
@{method case_tac}~‹t› & exhaustion (datatypes) \\
@{method induct_tac}~‹x› & induction (datatypes) \\
@{method ind_cases}~‹t› & exhaustion + simplification (inductive predicates) \\
\end{tabular}
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.24 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.