src/Doc/Isar_Ref/First_Order_Logic.thy
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (23 months ago)
changeset 66822 4642cf4a7ebb
parent 62279 f054c364b53f
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned signature;
wenzelm@61656
     1
(*:maxLineLen=78:*)
wenzelm@29730
     2
wenzelm@58889
     3
section \<open>Example: First-Order Logic\<close>
wenzelm@29730
     4
wenzelm@29730
     5
theory %visible First_Order_Logic
wenzelm@42651
     6
imports Base  (* FIXME Pure!? *)
wenzelm@29730
     7
begin
wenzelm@29730
     8
wenzelm@58618
     9
text \<open>
wenzelm@62279
    10
  In order to commence a new object-logic within Isabelle/Pure we introduce
wenzelm@62279
    11
  abstract syntactic categories \<open>i\<close> for individuals and \<open>o\<close> for
wenzelm@62279
    12
  object-propositions. The latter is embedded into the language of Pure
wenzelm@62279
    13
  propositions by means of a separate judgment.
wenzelm@58618
    14
\<close>
wenzelm@29730
    15
wenzelm@29730
    16
typedecl i
wenzelm@29730
    17
typedecl o
wenzelm@29730
    18
wenzelm@62279
    19
judgment Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
wenzelm@29730
    20
wenzelm@58618
    21
text \<open>
wenzelm@62279
    22
  Note that the object-logic judgment is implicit in the syntax: writing
wenzelm@62279
    23
  @{prop A} produces @{term "Trueprop A"} internally. From the Pure
wenzelm@62279
    24
  perspective this means ``@{prop A} is derivable in the object-logic''.
wenzelm@58618
    25
\<close>
wenzelm@29730
    26
wenzelm@29730
    27
wenzelm@58618
    28
subsection \<open>Equational reasoning \label{sec:framework-ex-equal}\<close>
wenzelm@29730
    29
wenzelm@58618
    30
text \<open>
wenzelm@29730
    31
  Equality is axiomatized as a binary predicate on individuals, with
wenzelm@62279
    32
  reflexivity as introduction, and substitution as elimination principle. Note
wenzelm@62279
    33
  that the latter is particularly convenient in a framework like Isabelle,
wenzelm@62279
    34
  because syntactic congruences are implicitly produced by unification of
wenzelm@62279
    35
  \<open>B x\<close> against expressions containing occurrences of \<open>x\<close>.
wenzelm@58618
    36
\<close>
wenzelm@29730
    37
wenzelm@62279
    38
axiomatization equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infix "=" 50)
wenzelm@62279
    39
  where refl [intro]: "x = x"
wenzelm@62279
    40
    and subst [elim]: "x = y \<Longrightarrow> B x \<Longrightarrow> B y"
wenzelm@29730
    41
wenzelm@58618
    42
text \<open>
wenzelm@62279
    43
  Substitution is very powerful, but also hard to control in full generality.
wenzelm@62279
    44
  We derive some common symmetry~/ transitivity schemes of @{term equal} as
wenzelm@62279
    45
  particular consequences.
wenzelm@58618
    46
\<close>
wenzelm@29730
    47
wenzelm@29730
    48
theorem sym [sym]:
wenzelm@29730
    49
  assumes "x = y"
wenzelm@29730
    50
  shows "y = x"
wenzelm@29730
    51
proof -
wenzelm@29730
    52
  have "x = x" ..
wenzelm@58618
    53
  with \<open>x = y\<close> show "y = x" ..
wenzelm@29730
    54
qed
wenzelm@29730
    55
wenzelm@29730
    56
theorem forw_subst [trans]:
wenzelm@29730
    57
  assumes "y = x" and "B x"
wenzelm@29730
    58
  shows "B y"
wenzelm@29730
    59
proof -
wenzelm@58618
    60
  from \<open>y = x\<close> have "x = y" ..
wenzelm@58618
    61
  from this and \<open>B x\<close> show "B y" ..
wenzelm@29730
    62
qed
wenzelm@29730
    63
wenzelm@29730
    64
theorem back_subst [trans]:
wenzelm@29730
    65
  assumes "B x" and "x = y"
wenzelm@29730
    66
  shows "B y"
wenzelm@29730
    67
proof -
wenzelm@58618
    68
  from \<open>x = y\<close> and \<open>B x\<close>
wenzelm@29730
    69
  show "B y" ..
wenzelm@29730
    70
qed
wenzelm@29730
    71
wenzelm@29730
    72
theorem trans [trans]:
wenzelm@29730
    73
  assumes "x = y" and "y = z"
wenzelm@29730
    74
  shows "x = z"
wenzelm@29730
    75
proof -
wenzelm@58618
    76
  from \<open>y = z\<close> and \<open>x = y\<close>
wenzelm@29730
    77
  show "x = z" ..
wenzelm@29730
    78
qed
wenzelm@29730
    79
wenzelm@29730
    80
wenzelm@58618
    81
subsection \<open>Basic group theory\<close>
wenzelm@29730
    82
wenzelm@58618
    83
text \<open>
wenzelm@62279
    84
  As an example for equational reasoning we consider some bits of group
wenzelm@62279
    85
  theory. The subsequent locale definition postulates group operations and
wenzelm@62279
    86
  axioms; we also derive some consequences of this specification.
wenzelm@58618
    87
\<close>
wenzelm@29730
    88
wenzelm@29730
    89
locale group =
wenzelm@29730
    90
  fixes prod :: "i \<Rightarrow> i \<Rightarrow> i"  (infix "\<circ>" 70)
wenzelm@29730
    91
    and inv :: "i \<Rightarrow> i"  ("(_\<inverse>)" [1000] 999)
wenzelm@29730
    92
    and unit :: i  ("1")
wenzelm@29730
    93
  assumes assoc: "(x \<circ> y) \<circ> z = x \<circ> (y \<circ> z)"
wenzelm@29730
    94
    and left_unit:  "1 \<circ> x = x"
wenzelm@29730
    95
    and left_inv: "x\<inverse> \<circ> x = 1"
wenzelm@29730
    96
begin
wenzelm@29730
    97
wenzelm@29730
    98
theorem right_inv: "x \<circ> x\<inverse> = 1"
wenzelm@29730
    99
proof -
wenzelm@29730
   100
  have "x \<circ> x\<inverse> = 1 \<circ> (x \<circ> x\<inverse>)" by (rule left_unit [symmetric])
wenzelm@29730
   101
  also have "\<dots> = (1 \<circ> x) \<circ> x\<inverse>" by (rule assoc [symmetric])
wenzelm@29730
   102
  also have "1 = (x\<inverse>)\<inverse> \<circ> x\<inverse>" by (rule left_inv [symmetric])
wenzelm@29730
   103
  also have "\<dots> \<circ> x = (x\<inverse>)\<inverse> \<circ> (x\<inverse> \<circ> x)" by (rule assoc)
wenzelm@29730
   104
  also have "x\<inverse> \<circ> x = 1" by (rule left_inv)
wenzelm@29730
   105
  also have "((x\<inverse>)\<inverse> \<circ> \<dots>) \<circ> x\<inverse> = (x\<inverse>)\<inverse> \<circ> (1 \<circ> x\<inverse>)" by (rule assoc)
wenzelm@29730
   106
  also have "1 \<circ> x\<inverse> = x\<inverse>" by (rule left_unit)
wenzelm@29730
   107
  also have "(x\<inverse>)\<inverse> \<circ> \<dots> = 1" by (rule left_inv)
wenzelm@29730
   108
  finally show "x \<circ> x\<inverse> = 1" .
wenzelm@29730
   109
qed
wenzelm@29730
   110
wenzelm@29730
   111
theorem right_unit: "x \<circ> 1 = x"
wenzelm@29730
   112
proof -
wenzelm@29730
   113
  have "1 = x\<inverse> \<circ> x" by (rule left_inv [symmetric])
wenzelm@29730
   114
  also have "x \<circ> \<dots> = (x \<circ> x\<inverse>) \<circ> x" by (rule assoc [symmetric])
wenzelm@29730
   115
  also have "x \<circ> x\<inverse> = 1" by (rule right_inv)
wenzelm@29730
   116
  also have "\<dots> \<circ> x = x" by (rule left_unit)
wenzelm@29730
   117
  finally show "x \<circ> 1 = x" .
wenzelm@29730
   118
qed
wenzelm@29730
   119
wenzelm@58618
   120
text \<open>
wenzelm@62279
   121
  Reasoning from basic axioms is often tedious. Our proofs work by producing
wenzelm@62279
   122
  various instances of the given rules (potentially the symmetric form) using
wenzelm@62279
   123
  the pattern ``\<^theory_text>\<open>have eq by (rule r)\<close>'' and composing the chain of results
wenzelm@62279
   124
  via \<^theory_text>\<open>also\<close>/\<^theory_text>\<open>finally\<close>. These steps may involve any of the transitivity
wenzelm@62279
   125
  rules declared in \secref{sec:framework-ex-equal}, namely @{thm trans} in
wenzelm@62279
   126
  combining the first two results in @{thm right_inv} and in the final steps
wenzelm@62279
   127
  of both proofs, @{thm forw_subst} in the first combination of @{thm
wenzelm@29730
   128
  right_unit}, and @{thm back_subst} in all other calculational steps.
wenzelm@29730
   129
wenzelm@62279
   130
  Occasional substitutions in calculations are adequate, but should not be
wenzelm@62279
   131
  over-emphasized. The other extreme is to compose a chain by plain
wenzelm@62279
   132
  transitivity only, with replacements occurring always in topmost position.
wenzelm@62279
   133
  For example:
wenzelm@58618
   134
\<close>
wenzelm@29730
   135
wenzelm@29730
   136
(*<*)
wenzelm@29730
   137
theorem "\<And>A. PROP A \<Longrightarrow> PROP A"
wenzelm@29730
   138
proof -
wenzelm@29730
   139
  assume [symmetric, defn]: "\<And>x y. (x \<equiv> y) \<equiv> Trueprop (x = y)"
wenzelm@56594
   140
  fix x
wenzelm@29730
   141
(*>*)
wenzelm@29730
   142
  have "x \<circ> 1 = x \<circ> (x\<inverse> \<circ> x)" unfolding left_inv ..
wenzelm@29730
   143
  also have "\<dots> = (x \<circ> x\<inverse>) \<circ> x" unfolding assoc ..
wenzelm@29730
   144
  also have "\<dots> = 1 \<circ> x" unfolding right_inv ..
wenzelm@29730
   145
  also have "\<dots> = x" unfolding left_unit ..
wenzelm@29730
   146
  finally have "x \<circ> 1 = x" .
wenzelm@29730
   147
(*<*)
wenzelm@29730
   148
qed
wenzelm@29730
   149
(*>*)
wenzelm@29730
   150
wenzelm@58618
   151
text \<open>
wenzelm@62279
   152
  Here we have re-used the built-in mechanism for unfolding definitions in
wenzelm@62279
   153
  order to normalize each equational problem. A more realistic object-logic
wenzelm@62279
   154
  would include proper setup for the Simplifier (\secref{sec:simplifier}), the
wenzelm@62279
   155
  main automated tool for equational reasoning in Isabelle. Then ``\<^theory_text>\<open>unfolding
wenzelm@62279
   156
  left_inv ..\<close>'' would become ``\<^theory_text>\<open>by (simp only: left_inv)\<close>'' etc.
wenzelm@58618
   157
\<close>
wenzelm@29730
   158
wenzelm@29730
   159
end
wenzelm@29730
   160
wenzelm@29730
   161
wenzelm@58618
   162
subsection \<open>Propositional logic \label{sec:framework-ex-prop}\<close>
wenzelm@29730
   163
wenzelm@58618
   164
text \<open>
wenzelm@29730
   165
  We axiomatize basic connectives of propositional logic: implication,
wenzelm@62279
   166
  disjunction, and conjunction. The associated rules are modeled after
wenzelm@62279
   167
  Gentzen's system of Natural Deduction @{cite "Gentzen:1935"}.
wenzelm@58618
   168
\<close>
wenzelm@29730
   169
wenzelm@62279
   170
axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
wenzelm@62279
   171
  where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
wenzelm@62279
   172
    and impD [dest]: "(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B"
wenzelm@29730
   173
wenzelm@62279
   174
axiomatization disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
wenzelm@62279
   175
  where disjI\<^sub>1 [intro]: "A \<Longrightarrow> A \<or> B"
wenzelm@62279
   176
    and disjI\<^sub>2 [intro]: "B \<Longrightarrow> A \<or> B"
wenzelm@62279
   177
    and disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@29730
   178
wenzelm@62279
   179
axiomatization conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
wenzelm@62279
   180
  where conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
wenzelm@62279
   181
    and conjD\<^sub>1: "A \<and> B \<Longrightarrow> A"
wenzelm@62279
   182
    and conjD\<^sub>2: "A \<and> B \<Longrightarrow> B"
wenzelm@29730
   183
wenzelm@58618
   184
text \<open>
wenzelm@62279
   185
  The conjunctive destructions have the disadvantage that decomposing @{prop
wenzelm@62279
   186
  "A \<and> B"} involves an immediate decision which component should be projected.
wenzelm@62279
   187
  The more convenient simultaneous elimination @{prop "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow>
wenzelm@62279
   188
  C"} can be derived as follows:
wenzelm@58618
   189
\<close>
wenzelm@29730
   190
wenzelm@29730
   191
theorem conjE [elim]:
wenzelm@29730
   192
  assumes "A \<and> B"
wenzelm@29730
   193
  obtains A and B
wenzelm@29730
   194
proof
wenzelm@58618
   195
  from \<open>A \<and> B\<close> show A by (rule conjD\<^sub>1)
wenzelm@58618
   196
  from \<open>A \<and> B\<close> show B by (rule conjD\<^sub>2)
wenzelm@29730
   197
qed
wenzelm@29730
   198
wenzelm@58618
   199
text \<open>
wenzelm@62279
   200
  Here is an example of swapping conjuncts with a single intermediate
wenzelm@62279
   201
  elimination step:
wenzelm@58618
   202
\<close>
wenzelm@29730
   203
wenzelm@29730
   204
(*<*)
wenzelm@29730
   205
lemma "\<And>A. PROP A \<Longrightarrow> PROP A"
wenzelm@29730
   206
proof -
wenzelm@62279
   207
  fix A B
wenzelm@29730
   208
(*>*)
wenzelm@29730
   209
  assume "A \<and> B"
wenzelm@29730
   210
  then obtain B and A ..
wenzelm@29730
   211
  then have "B \<and> A" ..
wenzelm@29730
   212
(*<*)
wenzelm@29730
   213
qed
wenzelm@29730
   214
(*>*)
wenzelm@29730
   215
wenzelm@58618
   216
text \<open>
wenzelm@62279
   217
  Note that the analogous elimination rule for disjunction ``\<^theory_text>\<open>assumes "A \<or> B"
wenzelm@62279
   218
  obtains A \<BBAR> B\<close>'' coincides with the original axiomatization of @{thm
wenzelm@62279
   219
  disjE}.
wenzelm@29730
   220
wenzelm@61421
   221
  \<^medskip>
wenzelm@62279
   222
  We continue propositional logic by introducing absurdity with its
wenzelm@62279
   223
  characteristic elimination. Plain truth may then be defined as a proposition
wenzelm@62279
   224
  that is trivially true.
wenzelm@58618
   225
\<close>
wenzelm@29730
   226
wenzelm@62279
   227
axiomatization false :: o  ("\<bottom>")
wenzelm@62279
   228
  where falseE [elim]: "\<bottom> \<Longrightarrow> A"
wenzelm@29730
   229
wenzelm@62279
   230
definition true :: o  ("\<top>")
wenzelm@62279
   231
  where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
wenzelm@29730
   232
wenzelm@29730
   233
theorem trueI [intro]: \<top>
wenzelm@29730
   234
  unfolding true_def ..
wenzelm@29730
   235
wenzelm@58618
   236
text \<open>
wenzelm@61421
   237
  \<^medskip>
wenzelm@61421
   238
  Now negation represents an implication towards absurdity:
wenzelm@58618
   239
\<close>
wenzelm@29730
   240
wenzelm@62279
   241
definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
wenzelm@62279
   242
  where "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
wenzelm@29730
   243
wenzelm@29730
   244
theorem notI [intro]:
wenzelm@29730
   245
  assumes "A \<Longrightarrow> \<bottom>"
wenzelm@29730
   246
  shows "\<not> A"
wenzelm@29730
   247
unfolding not_def
wenzelm@29730
   248
proof
wenzelm@29730
   249
  assume A
wenzelm@58618
   250
  then show \<bottom> by (rule \<open>A \<Longrightarrow> \<bottom>\<close>)
wenzelm@29730
   251
qed
wenzelm@29730
   252
wenzelm@29730
   253
theorem notE [elim]:
wenzelm@29730
   254
  assumes "\<not> A" and A
wenzelm@29730
   255
  shows B
wenzelm@29730
   256
proof -
wenzelm@58618
   257
  from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def .
wenzelm@58618
   258
  from \<open>A \<longrightarrow> \<bottom>\<close> and \<open>A\<close> have \<bottom> ..
wenzelm@29730
   259
  then show B ..
wenzelm@29730
   260
qed
wenzelm@29730
   261
wenzelm@29730
   262
wenzelm@58618
   263
subsection \<open>Classical logic\<close>
wenzelm@29730
   264
wenzelm@58618
   265
text \<open>
wenzelm@62279
   266
  Subsequently we state the principle of classical contradiction as a local
wenzelm@62279
   267
  assumption. Thus we refrain from forcing the object-logic into the classical
wenzelm@62279
   268
  perspective. Within that context, we may derive well-known consequences of
wenzelm@62279
   269
  the classical principle.
wenzelm@58618
   270
\<close>
wenzelm@29730
   271
wenzelm@29730
   272
locale classical =
wenzelm@29730
   273
  assumes classical: "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@29730
   274
begin
wenzelm@29730
   275
wenzelm@29730
   276
theorem double_negation:
wenzelm@29730
   277
  assumes "\<not> \<not> C"
wenzelm@29730
   278
  shows C
wenzelm@29730
   279
proof (rule classical)
wenzelm@29730
   280
  assume "\<not> C"
wenzelm@58618
   281
  with \<open>\<not> \<not> C\<close> show C ..
wenzelm@29730
   282
qed
wenzelm@29730
   283
wenzelm@29730
   284
theorem tertium_non_datur: "C \<or> \<not> C"
wenzelm@29730
   285
proof (rule double_negation)
wenzelm@29730
   286
  show "\<not> \<not> (C \<or> \<not> C)"
wenzelm@29730
   287
  proof
wenzelm@29730
   288
    assume "\<not> (C \<or> \<not> C)"
wenzelm@29730
   289
    have "\<not> C"
wenzelm@29730
   290
    proof
wenzelm@29730
   291
      assume C then have "C \<or> \<not> C" ..
wenzelm@58618
   292
      with \<open>\<not> (C \<or> \<not> C)\<close> show \<bottom> ..
wenzelm@29730
   293
    qed
wenzelm@29730
   294
    then have "C \<or> \<not> C" ..
wenzelm@58618
   295
    with \<open>\<not> (C \<or> \<not> C)\<close> show \<bottom> ..
wenzelm@29730
   296
  qed
wenzelm@29730
   297
qed
wenzelm@29730
   298
wenzelm@58618
   299
text \<open>
wenzelm@62279
   300
  These examples illustrate both classical reasoning and non-trivial
wenzelm@62279
   301
  propositional proofs in general. All three rules characterize classical
wenzelm@62279
   302
  logic independently, but the original rule is already the most convenient to
wenzelm@62279
   303
  use, because it leaves the conclusion unchanged. Note that @{prop "(\<not> C \<Longrightarrow> C)
wenzelm@62279
   304
  \<Longrightarrow> C"} fits again into our format for eliminations, despite the additional
wenzelm@62279
   305
  twist that the context refers to the main conclusion. So we may write @{thm
wenzelm@62279
   306
  classical} as the Isar statement ``\<^theory_text>\<open>obtains \<not> thesis\<close>''. This also explains
wenzelm@62279
   307
  nicely how classical reasoning really works: whatever the main \<open>thesis\<close>
wenzelm@62279
   308
  might be, we may always assume its negation!
wenzelm@58618
   309
\<close>
wenzelm@29730
   310
wenzelm@29730
   311
end
wenzelm@29730
   312
wenzelm@29730
   313
wenzelm@58618
   314
subsection \<open>Quantifiers \label{sec:framework-ex-quant}\<close>
wenzelm@29730
   315
wenzelm@58618
   316
text \<open>
wenzelm@62279
   317
  Representing quantifiers is easy, thanks to the higher-order nature of the
wenzelm@62279
   318
  underlying framework. According to the well-known technique introduced by
wenzelm@62279
   319
  Church @{cite "church40"}, quantifiers are operators on predicates, which
wenzelm@62279
   320
  are syntactically represented as \<open>\<lambda>\<close>-terms of type @{typ "i \<Rightarrow> o"}. Binder
wenzelm@62279
   321
  notation turns \<open>All (\<lambda>x. B x)\<close> into \<open>\<forall>x. B x\<close> etc.
wenzelm@58618
   322
\<close>
wenzelm@29730
   323
wenzelm@62279
   324
axiomatization All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
wenzelm@62279
   325
  where allI [intro]: "(\<And>x. B x) \<Longrightarrow> \<forall>x. B x"
wenzelm@62279
   326
    and allD [dest]: "(\<forall>x. B x) \<Longrightarrow> B a"
wenzelm@29730
   327
wenzelm@62279
   328
axiomatization Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
wenzelm@62279
   329
  where exI [intro]: "B a \<Longrightarrow> (\<exists>x. B x)"
wenzelm@62279
   330
    and exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@29730
   331
wenzelm@58618
   332
text \<open>
wenzelm@62279
   333
  The statement of @{thm exE} corresponds to ``\<^theory_text>\<open>assumes "\<exists>x. B x" obtains x
wenzelm@62279
   334
  where "B x"\<close>'' in Isar. In the subsequent example we illustrate quantifier
wenzelm@62279
   335
  reasoning involving all four rules:
wenzelm@58618
   336
\<close>
wenzelm@29730
   337
wenzelm@29730
   338
theorem
wenzelm@29730
   339
  assumes "\<exists>x. \<forall>y. R x y"
wenzelm@29730
   340
  shows "\<forall>y. \<exists>x. R x y"
wenzelm@61580
   341
proof    \<comment> \<open>\<open>\<forall>\<close> introduction\<close>
wenzelm@61580
   342
  obtain x where "\<forall>y. R x y" using \<open>\<exists>x. \<forall>y. R x y\<close> ..    \<comment> \<open>\<open>\<exists>\<close> elimination\<close>
wenzelm@61580
   343
  fix y have "R x y" using \<open>\<forall>y. R x y\<close> ..    \<comment> \<open>\<open>\<forall>\<close> destruction\<close>
wenzelm@61580
   344
  then show "\<exists>x. R x y" ..    \<comment> \<open>\<open>\<exists>\<close> introduction\<close>
wenzelm@29730
   345
qed
wenzelm@29730
   346
wenzelm@29734
   347
wenzelm@58618
   348
subsection \<open>Canonical reasoning patterns\<close>
wenzelm@29734
   349
wenzelm@58618
   350
text \<open>
wenzelm@29734
   351
  The main rules of first-order predicate logic from
wenzelm@62279
   352
  \secref{sec:framework-ex-prop} and \secref{sec:framework-ex-quant} can now
wenzelm@62279
   353
  be summarized as follows, using the native Isar statement format of
wenzelm@62279
   354
  \secref{sec:framework-stmt}.
wenzelm@29734
   355
wenzelm@61421
   356
  \<^medskip>
wenzelm@29734
   357
  \begin{tabular}{l}
wenzelm@62279
   358
  \<^theory_text>\<open>impI: assumes "A \<Longrightarrow> B" shows "A \<longrightarrow> B"\<close> \\
wenzelm@62279
   359
  \<^theory_text>\<open>impD: assumes "A \<longrightarrow> B" and A shows B\<close> \\[1ex]
wenzelm@29734
   360
wenzelm@62279
   361
  \<^theory_text>\<open>disjI\<^sub>1: assumes A shows "A \<or> B"\<close> \\
wenzelm@62279
   362
  \<^theory_text>\<open>disjI\<^sub>2: assumes B shows "A \<or> B"\<close> \\
wenzelm@62279
   363
  \<^theory_text>\<open>disjE: assumes "A \<or> B" obtains A \<BBAR> B\<close> \\[1ex]
wenzelm@29734
   364
wenzelm@62279
   365
  \<^theory_text>\<open>conjI: assumes A and B shows A \<and> B\<close> \\
wenzelm@62279
   366
  \<^theory_text>\<open>conjE: assumes "A \<and> B" obtains A and B\<close> \\[1ex]
wenzelm@29734
   367
wenzelm@62279
   368
  \<^theory_text>\<open>falseE: assumes \<bottom> shows A\<close> \\
wenzelm@62279
   369
  \<^theory_text>\<open>trueI: shows \<top>\<close> \\[1ex]
wenzelm@29734
   370
wenzelm@62279
   371
  \<^theory_text>\<open>notI: assumes "A \<Longrightarrow> \<bottom>" shows "\<not> A"\<close> \\
wenzelm@62279
   372
  \<^theory_text>\<open>notE: assumes "\<not> A" and A shows B\<close> \\[1ex]
wenzelm@29734
   373
wenzelm@62279
   374
  \<^theory_text>\<open>allI: assumes "\<And>x. B x" shows "\<forall>x. B x"\<close> \\
wenzelm@62279
   375
  \<^theory_text>\<open>allE: assumes "\<forall>x. B x" shows "B a"\<close> \\[1ex]
wenzelm@29734
   376
wenzelm@62279
   377
  \<^theory_text>\<open>exI: assumes "B a" shows "\<exists>x. B x"\<close> \\
wenzelm@62279
   378
  \<^theory_text>\<open>exE: assumes "\<exists>x. B x" obtains a where "B a"\<close>
wenzelm@29734
   379
  \end{tabular}
wenzelm@61421
   380
  \<^medskip>
wenzelm@29734
   381
wenzelm@62279
   382
  This essentially provides a declarative reading of Pure rules as Isar
wenzelm@62279
   383
  reasoning patterns: the rule statements tells how a canonical proof outline
wenzelm@62279
   384
  shall look like. Since the above rules have already been declared as
wenzelm@62279
   385
  @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure)
wenzelm@62279
   386
  dest} --- each according to its particular shape --- we can immediately
wenzelm@62279
   387
  write Isar proof texts as follows:
wenzelm@58618
   388
\<close>
wenzelm@29734
   389
wenzelm@29734
   390
(*<*)
wenzelm@29734
   391
theorem "\<And>A. PROP A \<Longrightarrow> PROP A"
wenzelm@29734
   392
proof -
wenzelm@29734
   393
(*>*)
wenzelm@29734
   394
wenzelm@58999
   395
  text_raw \<open>\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   396
wenzelm@29734
   397
  have "A \<longrightarrow> B"
wenzelm@29734
   398
  proof
wenzelm@29734
   399
    assume A
wenzelm@62271
   400
    show B \<proof>
wenzelm@29734
   401
  qed
wenzelm@29734
   402
wenzelm@58999
   403
  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   404
wenzelm@62271
   405
  have "A \<longrightarrow> B" and A \<proof>
wenzelm@29734
   406
  then have B ..
wenzelm@29734
   407
wenzelm@58999
   408
  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   409
wenzelm@62271
   410
  have A \<proof>
wenzelm@29734
   411
  then have "A \<or> B" ..
wenzelm@29734
   412
wenzelm@62271
   413
  have B \<proof>
wenzelm@29734
   414
  then have "A \<or> B" ..
wenzelm@29734
   415
wenzelm@58999
   416
  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   417
wenzelm@62271
   418
  have "A \<or> B" \<proof>
wenzelm@29734
   419
  then have C
wenzelm@29734
   420
  proof
wenzelm@29734
   421
    assume A
wenzelm@62271
   422
    then show C \<proof>
wenzelm@29734
   423
  next
wenzelm@29734
   424
    assume B
wenzelm@62271
   425
    then show C \<proof>
wenzelm@29734
   426
  qed
wenzelm@29734
   427
wenzelm@58999
   428
  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   429
wenzelm@62271
   430
  have A and B \<proof>
wenzelm@29734
   431
  then have "A \<and> B" ..
wenzelm@29734
   432
wenzelm@58999
   433
  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   434
wenzelm@62271
   435
  have "A \<and> B" \<proof>
wenzelm@29734
   436
  then obtain A and B ..
wenzelm@29734
   437
wenzelm@58999
   438
  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   439
wenzelm@62271
   440
  have "\<bottom>" \<proof>
wenzelm@29734
   441
  then have A ..
wenzelm@29734
   442
wenzelm@58999
   443
  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   444
wenzelm@29734
   445
  have "\<top>" ..
wenzelm@29734
   446
wenzelm@58999
   447
  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   448
wenzelm@29734
   449
  have "\<not> A"
wenzelm@29734
   450
  proof
wenzelm@29734
   451
    assume A
wenzelm@62271
   452
    then show "\<bottom>" \<proof>
wenzelm@29734
   453
  qed
wenzelm@29734
   454
wenzelm@58999
   455
  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   456
wenzelm@62271
   457
  have "\<not> A" and A \<proof>
wenzelm@29734
   458
  then have B ..
wenzelm@29734
   459
wenzelm@58999
   460
  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   461
wenzelm@29734
   462
  have "\<forall>x. B x"
wenzelm@29734
   463
  proof
wenzelm@29734
   464
    fix x
wenzelm@62271
   465
    show "B x" \<proof>
wenzelm@29734
   466
  qed
wenzelm@29734
   467
wenzelm@58999
   468
  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   469
wenzelm@62271
   470
  have "\<forall>x. B x" \<proof>
wenzelm@29734
   471
  then have "B a" ..
wenzelm@29734
   472
wenzelm@58999
   473
  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   474
wenzelm@29734
   475
  have "\<exists>x. B x"
wenzelm@29734
   476
  proof
wenzelm@62271
   477
    show "B a" \<proof>
wenzelm@29734
   478
  qed
wenzelm@29734
   479
wenzelm@58999
   480
  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
wenzelm@29734
   481
wenzelm@62271
   482
  have "\<exists>x. B x" \<proof>
wenzelm@29734
   483
  then obtain a where "B a" ..
wenzelm@29734
   484
wenzelm@58999
   485
  text_raw \<open>\end{minipage}\<close>
wenzelm@29734
   486
wenzelm@29734
   487
(*<*)
wenzelm@29734
   488
qed
wenzelm@29734
   489
(*>*)
wenzelm@29734
   490
wenzelm@58618
   491
text \<open>
wenzelm@61421
   492
  \<^bigskip>
wenzelm@62279
   493
  Of course, these proofs are merely examples. As sketched in
wenzelm@62279
   494
  \secref{sec:framework-subproof}, there is a fair amount of flexibility in
wenzelm@62279
   495
  expressing Pure deductions in Isar. Here the user is asked to express
wenzelm@62279
   496
  himself adequately, aiming at proof texts of literary quality.
wenzelm@58618
   497
\<close>
wenzelm@29734
   498
wenzelm@29730
   499
end %visible