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