Quelle  First_Order_Logic.thy

(*:maxLineLen=78:*)

section ‹Example: First-Order Logic›

theory %visible First_Order_Logic
imports Base  (* FIXME Pure!? *)
begin

text ‹
 In order to commence a new object-logic within Isabelle/Pure we introduce
 abstract syntactic categories ‹i› for individuals and ‹o› for
 object-propositions. The latter is embedded into the language of Pure
 propositions by means of a separate judgment.
 ›

typedecl i
typedecl o

judgment Trueprop :: "o ==> prop"    (‹_› 5)

text ‹
 Note that the object-logic judgment is implicit in the syntax: writing
 prop‹A› produces term‹Trueprop A› internally. From the Pure
 perspective this means ``prop‹A› is derivable in the object-logic''.
 ›


subsection ‹Equational reasoning \label{sec:framework-ex-equal}›

text ‹
 Equality is axiomatized as a binary predicate on individuals, with
 reflexivity as introduction, and substitution as elimination principle. Note
 that the latter is particularly convenient in a framework like Isabelle,
 because syntactic congruences are implicitly produced by unification of
 ‹B x› against expressions containing occurrences of ‹x›.
 ›

axiomatization equal :: "i ==> i ==> o"  (infix ‹=› 50)
  where refl [intro]: "x = x"
    and subst [elim]: "x = y ==> B x ==> B y"

text ‹
 Substitution is very powerful, but also hard to control in full generality.
 We derive some common symmetry~/ transitivity schemes of term‹equal› as
 particular consequences.
 ›

theorem sym [sym]:
  assumes "x = y"
  shows "y = x"
proof -
  have "x = x" ..
  with ‹x = y› show "y = x" ..
qed

theorem forw_subst [trans]:
  assumes "y = x" and "B x"
  shows "B y"
proof -
  from ‹y = x› have "x = y" ..
  from this and ‹B x› show "B y" ..
qed

theorem back_subst [trans]:
  assumes "B x" and "x = y"
  shows "B y"
proof -
  from ‹x = y› and ‹B x›
  show "B y" ..
qed

theorem trans [trans]:
  assumes "x = y" and "y = z"
  shows "x = z"
proof -
  from ‹y = z› and ‹x = y›
  show "x = z" ..
qed


subsection ‹Basic group theory›

text ‹
 As an example for equational reasoning we consider some bits of group
 theory. The subsequent locale definition postulates group operations and
 axioms; we also derive some consequences of this specification.
 ›

locale group =
  fixes prod :: "i ==> i ==> i"  (infix ‹∘› 70)
    and inv :: "i ==> i"  (‹(_^-1)› [1000] 999)
    and unit :: i  (‹1›)
  assumes assoc: "(x ∘ y) ∘ z = x ∘ (y ∘ z)"
    and left_unit:  "1 ∘ x = x"
    and left_inv: "x^-1 ∘ x = 1"
begin

theorem right_inv: "x ∘ x^-1 = 1"
proof -
  have "x ∘ x^-1 = 1 ∘ (x ∘ x^-1)" by (rule left_unit [symmetric])
  also have "… = (1 ∘ x) ∘ x^-1" by (rule assoc [symmetric])
  also have "1 = (x^-1)^-1 ∘ x^-1" by (rule left_inv [symmetric])
  also have "… ∘ x = (x^-1)^-1 ∘ (x^-1 ∘ x)" by (rule assoc)
  also have "x^-1 ∘ x = 1" by (rule left_inv)
  also have "((x^-1)^-1 ∘ …) ∘ x^-1 = (x^-1)^-1 ∘ (1 ∘ x^-1)" by (rule assoc)
  also have "1 ∘ x^-1 = x^-1" by (rule left_unit)
  also have "(x^-1)^-1 ∘ … = 1" by (rule left_inv)
  finally show "x ∘ x^-1 = 1" .
qed

theorem right_unit: "x ∘ 1 = x"
proof -
  have "1 = x^-1 ∘ x" by (rule left_inv [symmetric])
  also have "x ∘ … = (x ∘ x^-1) ∘ x" by (rule assoc [symmetric])
  also have "x ∘ x^-1 = 1" by (rule right_inv)
  also have "… ∘ x = x" by (rule left_unit)
  finally show "x ∘ 1 = x" .
qed

text ‹
 Reasoning from basic axioms is often tedious. Our proofs work by producing
 various instances of the given rules (potentially the symmetric form) using
 the pattern ``🪙‹have eq by (rule r)›'' and composing the chain of results
 via 🪙‹also›/🪙‹finally›. These steps may involve any of the transitivity
 rules declared in \secref{sec:framework-ex-equal}, namely @{thm trans} in
 combining the first two results in @{thm right_inv} and in the final steps
 of both proofs, @{thm forw_subst} in the first combination of @{thm
 right_unit}, and @{thm back_subst} in all other calculational steps.

 Occasional substitutions in calculations are adequate, but should not be
 over-emphasized. The other extreme is to compose a chain by plain
 transitivity only, with replacements occurring always in topmost position.
 For example:
 ›

(*<*)
theorem "∧A. PROP A ==> PROP A"
proof -
  assume [symmetric, defn]: "∧x y. (x ≡ y) ≡ Trueprop (x = y)"
  fix x
(*>*)
  have "x ∘ 1 = x ∘ (x^-1 ∘ x)" unfolding left_inv ..
  also have "… = (x ∘ x^-1) ∘ x" unfolding assoc ..
  also have "… = 1 ∘ x" unfolding right_inv ..
  also have "… = x" unfolding left_unit ..
  finally have "x ∘ 1 = x" .
(*<*)
qed
(*>*)

text ‹
 Here we have re-used the built-in mechanism for unfolding definitions in
 order to normalize each equational problem. A more realistic object-logic
 would include proper setup for the Simplifier (\secref{sec:simplifier}), the
 main automated tool for equational reasoning in Isabelle. Then ``🪙‹unfolding
 left_inv ..›'' would become ``🪙‹by (simp only: left_inv)›'' etc.
 ›

end


subsection ‹Propositional logic \label{sec:framework-ex-prop}›

text ‹
 We axiomatize basic connectives of propositional logic: implication,
 disjunction, and conjunction. The associated rules are modeled after
 Gentzen's system of Natural Deduction cite‹"Gentzen:1935"›.
 ›

axiomatization imp :: "o ==> o ==> o"  (infixr ‹⟶› 25)
  where impI [intro]: "(A ==> B) ==> A ⟶ B"
    and impD [dest]: "(A ⟶ B) ==> A ==> B"

axiomatization disj :: "o ==> o ==> o"  (infixr ‹∨› 30)
  where disjI₁ [intro]: "A ==> A ∨ B"
    and disjI₂ [intro]: "B ==> A ∨ B"
    and disjE [elim]: "A ∨ B ==> (A ==> C) ==> (B ==> C) ==> C"

axiomatization conj :: "o ==> o ==> o"  (infixr ‹∧› 35)
  where conjI [intro]: "A ==> B ==> A ∧ B"
    and conjD₁: "A ∧ B ==> A"
    and conjD₂: "A ∧ B ==> B"

text ‹
 The conjunctive destructions have the disadvantage that decomposing prop‹A ∧ B› involves an immediate decision which component should be projected.
 The more convenient simultaneous elimination prop‹A ∧ B ==> (A ==> B ==> C) ==>
 C› can be derived as follows:
 ›

theorem conjE [elim]:
  assumes "A ∧ B"
  obtains A and B
proof
  from ‹A ∧ B› show A by (rule conjD₁)
  from ‹A ∧ B› show B by (rule conjD₂)
qed

text ‹
 Here is an example of swapping conjuncts with a single intermediate
 elimination step:
 ›

(*<*)
lemma "∧A. PROP A ==> PROP A"
proof -
  fix A B
(*>*)
  assume "A ∧ B"
  then obtain B and A ..
  then have "B ∧ A" ..
(*<*)
qed
(*>*)

text ‹
 Note that the analogous elimination rule for disjunction ``🪙‹assumes "A ∨ B"
 obtains A 🪙 B›'' coincides with the original axiomatization of @{thm
 disjE}.

 🪙
 We continue propositional logic by introducing absurdity with its
 characteristic elimination. Plain truth may then be defined as a proposition
 that is trivially true.
 ›

axiomatization false :: o  (‹⊥›)
  where falseE [elim]: "⊥ ==> A"

definition true :: o  (‹⊤›)
  where "⊤ ≡ ⊥ ⟶ ⊥"

theorem trueI [intro]: ⊤
  unfolding true_def ..

text ‹
 🪙
 Now negation represents an implication towards absurdity:
 ›

definition not :: "o ==> o"  (‹¬ _› [40] 40)
  where "¬ A ≡ A ⟶ ⊥"

theorem notI [intro]:
  assumes "A ==> ⊥"
  shows "¬ A"
unfolding not_def
proof
  assume A
  then show ⊥ by (rule ‹A ==> ⊥›)
qed

theorem notE [elim]:
  assumes "¬ A" and A
  shows B
proof -
  from ‹¬ A› have "A ⟶ ⊥" unfolding not_def .
  from ‹A ⟶ ⊥› and ‹A› have ⊥ ..
  then show B ..
qed


subsection ‹Classical logic›

text ‹
 Subsequently we state the principle of classical contradiction as a local
 assumption. Thus we refrain from forcing the object-logic into the classical
 perspective. Within that context, we may derive well-known consequences of
 the classical principle.
 ›

locale classical =
  assumes classical: "(¬ C ==> C) ==> C"
begin

theorem double_negation:
  assumes "¬ ¬ C"
  shows C
proof (rule classical)
  assume "¬ C"
  with ‹¬ ¬ C› show C ..
qed

theorem tertium_non_datur: "C ∨ ¬ C"
proof (rule double_negation)
  show "¬ ¬ (C ∨ ¬ C)"
  proof
    assume "¬ (C ∨ ¬ C)"
    have "¬ C"
    proof
      assume C then have "C ∨ ¬ C" ..
      with ‹¬ (C ∨ ¬ C)› show ⊥ ..
    qed
    then have "C ∨ ¬ C" ..
    with ‹¬ (C ∨ ¬ C)› show ⊥ ..
  qed
qed

text ‹
 These examples illustrate both classical reasoning and non-trivial
 propositional proofs in general. All three rules characterize classical
 logic independently, but the original rule is already the most convenient to
 use, because it leaves the conclusion unchanged. Note that prop‹(¬ C ==> C)
 ==> C› fits again into our format for eliminations, despite the additional
 twist that the context refers to the main conclusion. So we may write @{thm
 classical} as the Isar statement ``🪙‹obtains ¬ thesis›''. This also explains
 nicely how classical reasoning really works: whatever the main ‹thesis›
 might be, we may always assume its negation!
 ›

end


subsection ‹Quantifiers \label{sec:framework-ex-quant}›

text ‹
 Representing quantifiers is easy, thanks to the higher-order nature of the
 underlying framework. According to the well-known technique introduced by
 Church cite‹"church40"›, quantifiers are operators on predicates, which
 are syntactically represented as ‹λ›-terms of type 🍋‹i ==> o›. Binder
 notation turns ‹All (λx. B x)› into ‹∀x. B x› etc.
 ›

axiomatization All :: "(i ==> o) ==> o"  (binder ‹∀› 10)
  where allI [intro]: "(∧x. B x) ==> ∀x. B x"
    and allD [dest]: "(∀x. B x) ==> B a"

axiomatization Ex :: "(i ==> o) ==> o"  (binder ‹∃› 10)
  where exI [intro]: "B a ==> (∃x. B x)"
    and exE [elim]: "(∃x. B x) ==> (∧x. B x ==> C) ==> C"

text ‹
 The statement of @{thm exE} corresponds to ``🪙‹assumes "∃x. B x" obtains x
 where "B x"›'' in Isar. In the subsequent example we illustrate quantifier
 reasoning involving all four rules:
 ›

theorem
  assumes "∃x. ∀y. R x y"
  shows "∀y. ∃x. R x y"
proof    ― ‹‹∀› introduction›
  obtain x where "∀y. R x y" using ‹∃x. ∀y. R x y› ..    ― ‹‹∃› elimination›
  fix y have "R x y" using ‹∀y. R x y› ..    ― ‹‹∀› destruction›
  then show "∃x. R x y" ..    ― ‹‹∃› introduction›
qed


subsection ‹Canonical reasoning patterns›

text ‹
 The main rules of first-order predicate logic from
 \secref{sec:framework-ex-prop} and \secref{sec:framework-ex-quant} can now
 be summarized as follows, using the native Isar statement format of
 \secref{sec:framework-stmt}.

 🪙
 \begin{tabular}{l}
 🪙‹impI: assumes "A ==> B" shows "A ⟶ B"› \\
 🪙‹impD: assumes "A ⟶ B" and A shows B› \\[1ex]

 🪙‹disjI₁: assumes A shows "A ∨ B"› \\
 🪙‹disjI₂: assumes B shows "A ∨ B"› \\
 🪙‹disjE: assumes "A ∨ B" obtains A 🪙 B› \\[1ex]

 🪙‹conjI: assumes A and B shows A ∧ B› \\
 🪙‹conjE: assumes "A ∧ B" obtains A and B› \\[1ex]

 🪙‹falseE: assumes ⊥ shows A› \\
 🪙‹trueI: shows ⊤› \\[1ex]

 🪙‹notI: assumes "A ==> ⊥" shows "¬ A"› \\
 🪙‹notE: assumes "¬ A" and A shows B› \\[1ex]

 🪙‹allI: assumes "∧x. B x" shows "∀x. B x"› \\
 🪙‹allE: assumes "∀x. B x" shows "B a"› \\[1ex]

 🪙‹exI: assumes "B a" shows "∃x. B x"› \\
 🪙‹exE: assumes "∃x. B x" obtains a where "B a"›
 \end{tabular}
 🪙

 This essentially provides a declarative reading of Pure rules as Isar
 reasoning patterns: the rule statements tells how a canonical proof outline
 shall look like. Since the above rules have already been declared as
 @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure)
 dest} --- each according to its particular shape --- we can immediately
 write Isar proof texts as follows:
 ›

(*<*)
theorem "∧A. PROP A ==> PROP A"
proof -
(*>*)

  text_raw ‹\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have "A ⟶ B"
  proof
    assume A
    show B 🍋
  qed

  text_raw ‹\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have "A ⟶ B" and A 🍋
  then have B ..

  text_raw ‹\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have A 🍋
  then have "A ∨ B" ..

  have B 🍋
  then have "A ∨ B" ..

  text_raw ‹\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have "A ∨ B" 🍋
  then have C
  proof
    assume A
    then show C 🍋
  next
    assume B
    then show C 🍋
  qed

  text_raw ‹\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have A and B 🍋
  then have "A ∧ B" ..

  text_raw ‹\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have "A ∧ B" 🍋
  then obtain A and B ..

  text_raw ‹\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have "⊥" 🍋
  then have A ..

  text_raw ‹\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have "⊤" ..

  text_raw ‹\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have "¬ A"
  proof
    assume A
    then show "⊥" 🍋
  qed

  text_raw ‹\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have "¬ A" and A 🍋
  then have B ..

  text_raw ‹\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have "∀x. B x"
  proof
    fix x
    show "B x" 🍋
  qed

  text_raw ‹\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have "∀x. B x" 🍋
  then have "B a" ..

  text_raw ‹\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have "∃x. B x"
  proof
    show "B a" 🍋
  qed

  text_raw ‹\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}›(*<*)next(*>*)

  have "∃x. B x" 🍋
  then obtain a where "B a" ..

  text_raw ‹\end{minipage}›

(*<*)
qed
(*>*)

text ‹
 🪙
 Of course, these proofs are merely examples. As sketched in
 \secref{sec:framework-subproof}, there is a fair amount of flexibility in
 expressing Pure deductions in Isar. Here the user is asked to express
 himself adequately, aiming at proof texts of literary quality.
 ›

end %visible