src/Doc/Isar_Ref/Quick_Reference.thy
author wenzelm
Sun, 12 Jun 2016 13:43:27 +0200
changeset 63292 5a1f5fc10bb0
parent 63286 ce90bb3d2902
child 63293 9adfdaee327e
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61656
cfabbc083977 more uniform jEdit properties;
wenzelm
parents: 61493
diff changeset
     1
(*:maxLineLen=78:*)
cfabbc083977 more uniform jEdit properties;
wenzelm
parents: 61493
diff changeset
     2
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
     3
theory Quick_Reference
42651
e3fdb7c96be5 formal Base theory;
wenzelm
parents: 40536
diff changeset
     4
imports Base Main
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
     5
begin
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
     6
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
     7
chapter \<open>Isabelle/Isar quick reference \label{ap:refcard}\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
     8
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
     9
section \<open>Proof commands\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
    10
62278
c04e97be39d3 misc tuning and updates;
wenzelm
parents: 62270
diff changeset
    11
subsection \<open>Main grammar \label{ap:main-grammar}\<close>
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    12
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    13
text \<open>
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    14
  \begin{tabular}{rcl}
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    15
    \<open>main\<close> & = & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\
63292
wenzelm
parents: 63286
diff changeset
    16
    & \<open>|\<close> & \<^theory_text>\<open>theorem name: props if name: props for vars "proof"\<close> \\
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    17
    & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
63285
e9c777bfd78c clarified syntax;
wenzelm
parents: 63039
diff changeset
    18
    & & \quad\<^theory_text>\<open>fixes vars\<close> \\
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    19
    & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    20
    & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\
63286
ce90bb3d2902 clarified;
wenzelm
parents: 63285
diff changeset
    21
    & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
ce90bb3d2902 clarified;
wenzelm
parents: 63285
diff changeset
    22
    & & \quad\<^theory_text>\<open>fixes vars\<close> \\
ce90bb3d2902 clarified;
wenzelm
parents: 63285
diff changeset
    23
    & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
ce90bb3d2902 clarified;
wenzelm
parents: 63285
diff changeset
    24
    & & \quad\<^theory_text>\<open>obtains (name) vars where props | \<dots> "proof"\<close> \\
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    25
    \<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    26
    & \<open>|\<close> & \<^theory_text>\<open>"refinement\<^sup>*" done\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    27
    \<open>refinement\<close> & = &  \<^theory_text>\<open>apply method\<close> \\
63292
wenzelm
parents: 63286
diff changeset
    28
    & \<open>|\<close> & \<^theory_text>\<open>supply name = thms\<close> \\
63286
ce90bb3d2902 clarified;
wenzelm
parents: 63285
diff changeset
    29
    & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\
63292
wenzelm
parents: 63286
diff changeset
    30
    & \<open>|\<close> & \<^theory_text>\<open>using thms\<close> \\
wenzelm
parents: 63286
diff changeset
    31
    & \<open>|\<close> & \<^theory_text>\<open>unfolding thms\<close> \\
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    32
    \<open>statement\<close> & = & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    33
    & \<open>|\<close> & \<^theory_text>\<open>next\<close> \\
63292
wenzelm
parents: 63286
diff changeset
    34
    & \<open>|\<close> & \<^theory_text>\<open>note name = thms\<close> \\
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    35
    & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    36
    & \<open>|\<close> & \<^theory_text>\<open>write name  (mixfix)\<close> \\
63285
e9c777bfd78c clarified syntax;
wenzelm
parents: 63039
diff changeset
    37
    & \<open>|\<close> & \<^theory_text>\<open>fix vars\<close> \\
e9c777bfd78c clarified syntax;
wenzelm
parents: 63039
diff changeset
    38
    & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for vars\<close> \\
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    39
    & \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\
63286
ce90bb3d2902 clarified;
wenzelm
parents: 63285
diff changeset
    40
    \<open>goal\<close> & = & \<^theory_text>\<open>have name: props if name: props for vars "proof"\<close> \\
63285
e9c777bfd78c clarified syntax;
wenzelm
parents: 63039
diff changeset
    41
    & \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for vars "proof"\<close> \\
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    42
  \end{tabular}
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    43
\<close>
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    44
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    45
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    46
subsection \<open>Primitives\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
    47
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
    48
text \<open>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
    49
  \begin{tabular}{ll}
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    50
    \<^theory_text>\<open>fix x\<close> & augment context by \<open>\<And>x. \<box>\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    51
    \<^theory_text>\<open>assume a: A\<close> & augment context by \<open>A \<Longrightarrow> \<box>\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    52
    \<^theory_text>\<open>then\<close> & indicate forward chaining of facts \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    53
    \<^theory_text>\<open>have a: A\<close> & prove local result \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    54
    \<^theory_text>\<open>show a: A\<close> & prove local result, refining some goal \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    55
    \<^theory_text>\<open>using a\<close> & indicate use of additional facts \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    56
    \<^theory_text>\<open>unfolding a\<close> & unfold definitional equations \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    57
    \<^theory_text>\<open>proof m\<^sub>1 \<dots> qed m\<^sub>2\<close> & indicate proof structure and refinements \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    58
    \<^theory_text>\<open>{ \<dots> }\<close> & indicate explicit blocks \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    59
    \<^theory_text>\<open>next\<close> & switch proof blocks \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    60
    \<^theory_text>\<open>note a = b\<close> & reconsider and declare facts \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    61
    \<^theory_text>\<open>let p = t\<close> & abbreviate terms by higher-order matching \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    62
    \<^theory_text>\<open>write c  (mx)\<close> & declare local mixfix syntax \\
26852
a31203f58b20 misc tuning;
wenzelm
parents: 26780
diff changeset
    63
  \end{tabular}
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
    64
\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
    65
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
    66
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
    67
subsection \<open>Abbreviations and synonyms\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
    68
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
    69
text \<open>
26852
a31203f58b20 misc tuning;
wenzelm
parents: 26780
diff changeset
    70
  \begin{tabular}{rcl}
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    71
    \<^theory_text>\<open>by m\<^sub>1 m\<^sub>2\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>proof m\<^sub>1 qed m\<^sub>2\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    72
    \<^theory_text>\<open>..\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>by standard\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    73
    \<^theory_text>\<open>.\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>by this\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    74
    \<^theory_text>\<open>from a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>note a then\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    75
    \<^theory_text>\<open>with a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>from a and this\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    76
    \<^theory_text>\<open>from this\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>then\<close> \\
26852
a31203f58b20 misc tuning;
wenzelm
parents: 26780
diff changeset
    77
  \end{tabular}
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
    78
\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
    79
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
    80
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
    81
subsection \<open>Derived elements\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
    82
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
    83
text \<open>
26852
a31203f58b20 misc tuning;
wenzelm
parents: 26780
diff changeset
    84
  \begin{tabular}{rcl}
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    85
    \<^theory_text>\<open>also"\<^sub>0"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>note calculation = this\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    86
    \<^theory_text>\<open>also"\<^sub>n\<^sub>+\<^sub>1"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>note calculation = trans [OF calculation this]\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    87
    \<^theory_text>\<open>finally\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>also from calculation\<close> \\[0.5ex]
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    88
    \<^theory_text>\<open>moreover\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>note calculation = calculation this\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    89
    \<^theory_text>\<open>ultimately\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>moreover from calculation\<close> \\[0.5ex]
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    90
    \<^theory_text>\<open>presume a: A\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>assume a: A\<close> \\
63039
1a20fd9cf281 added Isar command 'define';
wenzelm
parents: 62337
diff changeset
    91
    \<^theory_text>\<open>define x where "x = t"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>fix x assume x_def: "x = t"\<close> \\
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    92
    \<^theory_text>\<open>consider x where A | \<dots>\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>have thesis\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    93
    & & \quad \<^theory_text>\<open>if "\<And>x. A \<Longrightarrow> thesis" and \<dots> for thesis\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    94
    \<^theory_text>\<open>obtain x where a: A \<proof>\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>consider x where A \<proof>\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    95
    & & \<^theory_text>\<open>fix x assume a: A\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    96
    \<^theory_text>\<open>case c\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>fix x assume c: A\<close> \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
    97
    \<^theory_text>\<open>sorry\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>by cheating\<close> \\
26852
a31203f58b20 misc tuning;
wenzelm
parents: 26780
diff changeset
    98
  \end{tabular}
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
    99
\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   100
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   101
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   102
subsection \<open>Diagnostic commands\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   103
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   104
text \<open>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   105
  \begin{tabular}{ll}
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   106
    \<^theory_text>\<open>typ \<tau>\<close> & print type \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   107
    \<^theory_text>\<open>term t\<close> & print term \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   108
    \<^theory_text>\<open>prop \<phi>\<close> & print proposition \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   109
    \<^theory_text>\<open>thm a\<close> & print fact \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   110
    \<^theory_text>\<open>print_statement a\<close> & print fact in long statement form \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   111
  \end{tabular}
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   112
\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   113
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   114
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   115
section \<open>Proof methods\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   116
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   117
text \<open>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   118
  \begin{tabular}{ll}
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61421
diff changeset
   119
    \multicolumn{2}{l}{\<^bold>\<open>Single steps (forward-chaining facts)\<close>} \\[0.5ex]
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   120
    @{method assumption} & apply some goal assumption \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   121
    @{method this} & apply current facts \\
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   122
    @{method rule}~\<open>a\<close> & apply some rule  \\
60618
4c79543cc376 renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents: 58618
diff changeset
   123
    @{method standard} & apply standard rule (default for @{command "proof"}) \\
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   124
    @{method contradiction} & apply \<open>\<not>\<close> elimination rule (any order) \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   125
    @{method cases}~\<open>t\<close> & case analysis (provides cases) \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   126
    @{method induct}~\<open>x\<close> & proof by induction (provides cases) \\[2ex]
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   127
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61421
diff changeset
   128
    \multicolumn{2}{l}{\<^bold>\<open>Repeated steps (inserting facts)\<close>} \\[0.5ex]
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   129
    @{method "-"} & no rules \\
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   130
    @{method intro}~\<open>a\<close> & introduction rules \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   131
    @{method intro_classes} & class introduction rules \\
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   132
    @{method intro_locales} & locale introduction rules (without body) \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   133
    @{method unfold_locales} & locale introduction rules (with body) \\
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   134
    @{method elim}~\<open>a\<close> & elimination rules \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   135
    @{method unfold}~\<open>a\<close> & definitional rewrite rules \\[2ex]
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   136
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61421
diff changeset
   137
    \multicolumn{2}{l}{\<^bold>\<open>Automated proof tools (inserting facts)\<close>} \\[0.5ex]
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   138
    @{method iprover} & intuitionistic proof search \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   139
    @{method blast}, @{method fast} & Classical Reasoner \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   140
    @{method simp}, @{method simp_all} & Simplifier (+ Splitter) \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   141
    @{method auto}, @{method force} & Simplifier + Classical Reasoner \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   142
    @{method arith} & Arithmetic procedures \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   143
  \end{tabular}
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   144
\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   145
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   146
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   147
section \<open>Attributes\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   148
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   149
text \<open>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   150
  \begin{tabular}{ll}
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61421
diff changeset
   151
    \multicolumn{2}{l}{\<^bold>\<open>Rules\<close>} \\[0.5ex]
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   152
    @{attribute OF}~\<open>a\<close> & rule resolved with facts (skipping ``\<open>_\<close>'') \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   153
    @{attribute of}~\<open>t\<close> & rule instantiated with terms (skipping ``\<open>_\<close>'') \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   154
    @{attribute "where"}~\<open>x = t\<close> & rule instantiated with terms, by variable name \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   155
    @{attribute symmetric} & resolution with symmetry rule \\
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   156
    @{attribute THEN}~\<open>b\<close> & resolution with another rule \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   157
    @{attribute rule_format} & result put into standard rule format \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   158
    @{attribute elim_format} & destruct rule turned into elimination rule format \\[1ex]
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   159
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61421
diff changeset
   160
    \multicolumn{2}{l}{\<^bold>\<open>Declarations\<close>} \\[0.5ex]
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   161
    @{attribute simp} & Simplifier rule \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   162
    @{attribute intro}, @{attribute elim}, @{attribute dest} & Pure or Classical Reasoner rule \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   163
    @{attribute iff} & Simplifier + Classical Reasoner rule \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   164
    @{attribute split} & case split rule \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   165
    @{attribute trans} & transitivity rule \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   166
    @{attribute sym} & symmetry rule \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   167
  \end{tabular}
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   168
\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   169
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   170
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   171
section \<open>Rule declarations and methods\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   172
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   173
text \<open>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   174
  \begin{tabular}{l|lllll}
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   175
      & @{method rule} & @{method iprover} & @{method blast} & @{method simp} & @{method auto} \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   176
      &                &                   & @{method fast} & @{method simp_all} & @{method force} \\
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   177
    \hline
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   178
    @{attribute Pure.elim}\<open>!\<close> @{attribute Pure.intro}\<open>!\<close>
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   179
      & \<open>\<times>\<close>    & \<open>\<times>\<close> \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   180
    @{attribute Pure.elim} @{attribute Pure.intro}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   181
      & \<open>\<times>\<close>    & \<open>\<times>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   182
    @{attribute elim}\<open>!\<close> @{attribute intro}\<open>!\<close>
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   183
      & \<open>\<times>\<close>    &                    & \<open>\<times>\<close>          &                     & \<open>\<times>\<close> \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   184
    @{attribute elim} @{attribute intro}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   185
      & \<open>\<times>\<close>    &                    & \<open>\<times>\<close>          &                     & \<open>\<times>\<close> \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   186
    @{attribute iff}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   187
      & \<open>\<times>\<close>    &                    & \<open>\<times>\<close>          & \<open>\<times>\<close>         & \<open>\<times>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   188
    @{attribute iff}\<open>?\<close>
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   189
      & \<open>\<times>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   190
    @{attribute elim}\<open>?\<close> @{attribute intro}\<open>?\<close>
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   191
      & \<open>\<times>\<close> \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   192
    @{attribute simp}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   193
      &                &                    &                      & \<open>\<times>\<close>         & \<open>\<times>\<close> \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   194
    @{attribute cong}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   195
      &                &                    &                      & \<open>\<times>\<close>         & \<open>\<times>\<close> \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   196
    @{attribute split}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   197
      &                &                    &                      & \<open>\<times>\<close>         & \<open>\<times>\<close> \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   198
  \end{tabular}
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   199
\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   200
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   201
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   202
section \<open>Proof scripts\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   203
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   204
subsection \<open>Commands\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   205
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   206
text \<open>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   207
  \begin{tabular}{ll}
62270
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   208
    \<^theory_text>\<open>apply m\<close> & apply proof method during backwards refinement \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   209
    \<^theory_text>\<open>apply_end m\<close> & apply proof method (as if in terminal position) \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   210
    \<^theory_text>\<open>supply a\<close> & supply facts during backwards refinement \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   211
    \<^theory_text>\<open>subgoal\<close> & nested proof during backwards refinement \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   212
    \<^theory_text>\<open>defer n\<close> & move subgoal to end \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   213
    \<^theory_text>\<open>prefer n\<close> & move subgoal to start \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   214
    \<^theory_text>\<open>back\<close> & backtrack last command \\
77e3ffb5aeb3 misc tuning and updates;
wenzelm
parents: 62268
diff changeset
   215
    \<^theory_text>\<open>done\<close> & complete proof \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   216
  \end{tabular}
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   217
\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   218
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   219
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   220
subsection \<open>Methods\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   221
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   222
text \<open>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   223
  \begin{tabular}{ll}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   224
    @{method rule_tac}~\<open>insts\<close> & resolution (with instantiation) \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   225
    @{method erule_tac}~\<open>insts\<close> & elim-resolution (with instantiation) \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   226
    @{method drule_tac}~\<open>insts\<close> & destruct-resolution (with instantiation) \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   227
    @{method frule_tac}~\<open>insts\<close> & forward-resolution (with instantiation) \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   228
    @{method cut_tac}~\<open>insts\<close> & insert facts (with instantiation) \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   229
    @{method thin_tac}~\<open>\<phi>\<close> & delete assumptions \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   230
    @{method subgoal_tac}~\<open>\<phi>\<close> & new claims \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   231
    @{method rename_tac}~\<open>x\<close> & rename innermost goal parameters \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   232
    @{method rotate_tac}~\<open>n\<close> & rotate assumptions of goal \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   233
    @{method tactic}~\<open>text\<close> & arbitrary ML tactic \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   234
    @{method case_tac}~\<open>t\<close> & exhaustion (datatypes) \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   235
    @{method induct_tac}~\<open>x\<close> & induction (datatypes) \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   236
    @{method ind_cases}~\<open>t\<close> & exhaustion + simplification (inductive predicates) \\
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   237
  \end{tabular}
58618
782f0b662cae more cartouches;
wenzelm
parents: 57479
diff changeset
   238
\<close>
26779
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   239
35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
diff changeset
   240
end