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