Theory First_Order_Logic

(*: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"  ("(_¯)" [1000] 999)
    and unit :: i  ("1")
  assumes assoc: "(x ∘ y) ∘ z = x ∘ (y ∘ z)"
    and left_unit:  "1 ∘ x = x"
    and left_inv: "x¯ ∘ x = 1"
begin

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

theorem right_unit: "x ∘ 1 = x"
proof -
  have "1 = x¯ ∘ x" by (rule left_inv [symmetric])
  also have "x ∘ … = (x ∘ x¯) ∘ x" by (rule assoc [symmetric])
  also have "x ∘ x¯ = 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¯ ∘ x)" unfolding left_inv ..
  also have "… = (x ∘ x¯) ∘ 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⇩1 [intro]: "A ⟹ A ∨ B"
    and disjI⇩2 [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⇩1: "A ∧ B ⟹ A"
    and conjD⇩2: "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⇩1)
  from ‹A ∧ B› show B by (rule conjD⇩2)
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 \<BBAR> 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 \<^typ>‹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⇩1: assumes A shows "A ∨ B"› \\
  ⬚‹disjI⇩2: assumes B shows "A ∨ B"› \\
  ⬚‹disjE: assumes "A ∨ B" obtains A \<BBAR> 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 \<proof>
  qed

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

  have "A ⟶ B" and A \<proof>
  then have B ..

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

  have A \<proof>
  then have "A ∨ B" ..

  have B \<proof>
  then have "A ∨ B" ..

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

  have "A ∨ B" \<proof>
  then have C
  proof
    assume A
    then show C \<proof>
  next
    assume B
    then show C \<proof>
  qed

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

  have A and B \<proof>
  then have "A ∧ B" ..

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

  have "A ∧ B" \<proof>
  then obtain A and B ..

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

  have "⊥" \<proof>
  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 "⊥" \<proof>
  qed

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

  have "¬ A" and A \<proof>
  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" \<proof>
  qed

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

  have "∀x. B x" \<proof>
  then have "B a" ..

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

  have "∃x. B x"
  proof
    show "B a" \<proof>
  qed

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

  have "∃x. B x" \<proof>
  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