src/Doc/Isar_Ref/First_Order_Logic.thy

avoid odd permissions of fresh tmp_file;

section \<open>Example: First-Order Logic\<close>

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

text \<open>
  In order to commence a new object-logic within
  Isabelle/Pure we introduce abstract syntactic categories @{text "i"}
  for individuals and @{text "o"} for object-propositions.  The latter
  is embedded into the language of Pure propositions by means of a
  separate judgment.
\<close>

typedecl i
typedecl o

judgment
  Trueprop :: "o \<Rightarrow> prop"    ("_" 5)

text \<open>
  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''.
\<close>


subsection \<open>Equational reasoning \label{sec:framework-ex-equal}\<close>

text \<open>
  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 @{term "B x"} against
  expressions containing occurrences of @{term x}.
\<close>

axiomatization
  equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infix "=" 50)
where
  refl [intro]: "x = x" and
  subst [elim]: "x = y \<Longrightarrow> B x \<Longrightarrow> B y"

text \<open>
  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.
\<close>

theorem sym [sym]:
  assumes "x = y"
  shows "y = x"
proof -
  have "x = x" ..
  with \<open>x = y\<close> show "y = x" ..
qed

theorem forw_subst [trans]:
  assumes "y = x" and "B x"
  shows "B y"
proof -
  from \<open>y = x\<close> have "x = y" ..
  from this and \<open>B x\<close> show "B y" ..
qed

theorem back_subst [trans]:
  assumes "B x" and "x = y"
  shows "B y"
proof -
  from \<open>x = y\<close> and \<open>B x\<close>
  show "B y" ..
qed

theorem trans [trans]:
  assumes "x = y" and "y = z"
  shows "x = z"
proof -
  from \<open>y = z\<close> and \<open>x = y\<close>
  show "x = z" ..
qed


subsection \<open>Basic group theory\<close>

text \<open>
  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.
\<close>

locale group =
  fixes prod :: "i \<Rightarrow> i \<Rightarrow> i"  (infix "\<circ>" 70)
    and inv :: "i \<Rightarrow> i"  ("(_\<inverse>)" [1000] 999)
    and unit :: i  ("1")
  assumes assoc: "(x \<circ> y) \<circ> z = x \<circ> (y \<circ> z)"
    and left_unit:  "1 \<circ> x = x"
    and left_inv: "x\<inverse> \<circ> x = 1"
begin

theorem right_inv: "x \<circ> x\<inverse> = 1"
proof -
  have "x \<circ> x\<inverse> = 1 \<circ> (x \<circ> x\<inverse>)" by (rule left_unit [symmetric])
  also have "\<dots> = (1 \<circ> x) \<circ> x\<inverse>" by (rule assoc [symmetric])
  also have "1 = (x\<inverse>)\<inverse> \<circ> x\<inverse>" by (rule left_inv [symmetric])
  also have "\<dots> \<circ> x = (x\<inverse>)\<inverse> \<circ> (x\<inverse> \<circ> x)" by (rule assoc)
  also have "x\<inverse> \<circ> x = 1" by (rule left_inv)
  also have "((x\<inverse>)\<inverse> \<circ> \<dots>) \<circ> x\<inverse> = (x\<inverse>)\<inverse> \<circ> (1 \<circ> x\<inverse>)" by (rule assoc)
  also have "1 \<circ> x\<inverse> = x\<inverse>" by (rule left_unit)
  also have "(x\<inverse>)\<inverse> \<circ> \<dots> = 1" by (rule left_inv)
  finally show "x \<circ> x\<inverse> = 1" .
qed

theorem right_unit: "x \<circ> 1 = x"
proof -
  have "1 = x\<inverse> \<circ> x" by (rule left_inv [symmetric])
  also have "x \<circ> \<dots> = (x \<circ> x\<inverse>) \<circ> x" by (rule assoc [symmetric])
  also have "x \<circ> x\<inverse> = 1" by (rule right_inv)
  also have "\<dots> \<circ> x = x" by (rule left_unit)
  finally show "x \<circ> 1 = x" .
qed

text \<open>
  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 ``@{command have}~@{text
  eq}~@{command "by"}~@{text "(rule r)"}'' and composing the chain of
  results via @{command also}/@{command 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:
\<close>

(*<*)
theorem "\<And>A. PROP A \<Longrightarrow> PROP A"
proof -
  assume [symmetric, defn]: "\<And>x y. (x \<equiv> y) \<equiv> Trueprop (x = y)"
  fix x
(*>*)
  have "x \<circ> 1 = x \<circ> (x\<inverse> \<circ> x)" unfolding left_inv ..
  also have "\<dots> = (x \<circ> x\<inverse>) \<circ> x" unfolding assoc ..
  also have "\<dots> = 1 \<circ> x" unfolding right_inv ..
  also have "\<dots> = x" unfolding left_unit ..
  finally have "x \<circ> 1 = x" .
(*<*)
qed
(*>*)

text \<open>
  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 ``@{command unfolding}~@{thm
  left_inv}~@{command ".."}'' would become ``@{command "by"}~@{text
  "(simp only: left_inv)"}'' etc.
\<close>

end


subsection \<open>Propositional logic \label{sec:framework-ex-prop}\<close>

text \<open>
  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"}.
\<close>

axiomatization
  imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25) where
  impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
  impD [dest]: "(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B"

axiomatization
  disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30) where
  disjI\<^sub>1 [intro]: "A \<Longrightarrow> A \<or> B" and
  disjI\<^sub>2 [intro]: "B \<Longrightarrow> A \<or> B" and
  disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"

axiomatization
  conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35) where
  conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" and
  conjD\<^sub>1: "A \<and> B \<Longrightarrow> A" and
  conjD\<^sub>2: "A \<and> B \<Longrightarrow> B"

text \<open>
  The conjunctive destructions have the disadvantage that
  decomposing @{prop "A \<and> B"} involves an immediate decision which
  component should be projected.  The more convenient simultaneous
  elimination @{prop "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"} can be derived as
  follows:
\<close>

theorem conjE [elim]:
  assumes "A \<and> B"
  obtains A and B
proof
  from \<open>A \<and> B\<close> show A by (rule conjD\<^sub>1)
  from \<open>A \<and> B\<close> show B by (rule conjD\<^sub>2)
qed

text \<open>
  Here is an example of swapping conjuncts with a single
  intermediate elimination step:
\<close>

(*<*)
lemma "\<And>A. PROP A \<Longrightarrow> PROP A"
proof -
(*>*)
  assume "A \<and> B"
  then obtain B and A ..
  then have "B \<and> A" ..
(*<*)
qed
(*>*)

text \<open>
  Note that the analogous elimination rule for disjunction
  ``@{text "\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"}'' coincides with
  the original axiomatization of @{thm disjE}.

  \<^medskip>
  We continue propositional logic by introducing absurdity
  with its characteristic elimination.  Plain truth may then be
  defined as a proposition that is trivially true.
\<close>

axiomatization
  false :: o  ("\<bottom>") where
  falseE [elim]: "\<bottom> \<Longrightarrow> A"

definition
  true :: o  ("\<top>") where
  "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"

theorem trueI [intro]: \<top>
  unfolding true_def ..

text \<open>
  \<^medskip>
  Now negation represents an implication towards absurdity:
\<close>

definition
  not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40) where
  "\<not> A \<equiv> A \<longrightarrow> \<bottom>"

theorem notI [intro]:
  assumes "A \<Longrightarrow> \<bottom>"
  shows "\<not> A"
unfolding not_def
proof
  assume A
  then show \<bottom> by (rule \<open>A \<Longrightarrow> \<bottom>\<close>)
qed

theorem notE [elim]:
  assumes "\<not> A" and A
  shows B
proof -
  from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def .
  from \<open>A \<longrightarrow> \<bottom>\<close> and \<open>A\<close> have \<bottom> ..
  then show B ..
qed


subsection \<open>Classical logic\<close>

text \<open>
  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.
\<close>

locale classical =
  assumes classical: "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"
begin

theorem double_negation:
  assumes "\<not> \<not> C"
  shows C
proof (rule classical)
  assume "\<not> C"
  with \<open>\<not> \<not> C\<close> show C ..
qed

theorem tertium_non_datur: "C \<or> \<not> C"
proof (rule double_negation)
  show "\<not> \<not> (C \<or> \<not> C)"
  proof
    assume "\<not> (C \<or> \<not> C)"
    have "\<not> C"
    proof
      assume C then have "C \<or> \<not> C" ..
      with \<open>\<not> (C \<or> \<not> C)\<close> show \<bottom> ..
    qed
    then have "C \<or> \<not> C" ..
    with \<open>\<not> (C \<or> \<not> C)\<close> show \<bottom> ..
  qed
qed

text \<open>
  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 "(\<not> C \<Longrightarrow> C) \<Longrightarrow> 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 ``@{text "\<OBTAINS> \<not> thesis"}''.
  This also explains nicely how classical reasoning really works:
  whatever the main @{text thesis} might be, we may always assume its
  negation!
\<close>

end


subsection \<open>Quantifiers \label{sec:framework-ex-quant}\<close>

text \<open>
  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 @{text "\<lambda>"}-terms
  of type @{typ "i \<Rightarrow> o"}.  Binder notation turns @{text "All (\<lambda>x. B
  x)"} into @{text "\<forall>x. B x"} etc.
\<close>

axiomatization
  All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10) where
  allI [intro]: "(\<And>x. B x) \<Longrightarrow> \<forall>x. B x" and
  allD [dest]: "(\<forall>x. B x) \<Longrightarrow> B a"

axiomatization
  Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10) where
  exI [intro]: "B a \<Longrightarrow> (\<exists>x. B x)" and
  exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C"

text \<open>
  The statement of @{thm exE} corresponds to ``@{text
  "\<ASSUMES> \<exists>x. B x \<OBTAINS> x \<WHERE> B x"}'' in Isar.  In the
  subsequent example we illustrate quantifier reasoning involving all
  four rules:
\<close>

theorem
  assumes "\<exists>x. \<forall>y. R x y"
  shows "\<forall>y. \<exists>x. R x y"
proof    -- \<open>@{text "\<forall>"} introduction\<close>
  obtain x where "\<forall>y. R x y" using \<open>\<exists>x. \<forall>y. R x y\<close> ..    -- \<open>@{text "\<exists>"} elimination\<close>
  fix y have "R x y" using \<open>\<forall>y. R x y\<close> ..    -- \<open>@{text "\<forall>"} destruction\<close>
  then show "\<exists>x. R x y" ..    -- \<open>@{text "\<exists>"} introduction\<close>
qed


subsection \<open>Canonical reasoning patterns\<close>

text \<open>
  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}.

  \<^medskip>
  \begin{tabular}{l}
  @{text "impI: \<ASSUMES> A \<Longrightarrow> B \<SHOWS> A \<longrightarrow> B"} \\
  @{text "impD: \<ASSUMES> A \<longrightarrow> B \<AND> A \<SHOWS> B"} \\[1ex]

  @{text "disjI\<^sub>1: \<ASSUMES> A \<SHOWS> A \<or> B"} \\
  @{text "disjI\<^sub>2: \<ASSUMES> B \<SHOWS> A \<or> B"} \\
  @{text "disjE: \<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"} \\[1ex]

  @{text "conjI: \<ASSUMES> A \<AND> B \<SHOWS> A \<and> B"} \\
  @{text "conjE: \<ASSUMES> A \<and> B \<OBTAINS> A \<AND> B"} \\[1ex]

  @{text "falseE: \<ASSUMES> \<bottom> \<SHOWS> A"} \\
  @{text "trueI: \<SHOWS> \<top>"} \\[1ex]

  @{text "notI: \<ASSUMES> A \<Longrightarrow> \<bottom> \<SHOWS> \<not> A"} \\
  @{text "notE: \<ASSUMES> \<not> A \<AND> A \<SHOWS> B"} \\[1ex]

  @{text "allI: \<ASSUMES> \<And>x. B x \<SHOWS> \<forall>x. B x"} \\
  @{text "allE: \<ASSUMES> \<forall>x. B x \<SHOWS> B a"} \\[1ex]

  @{text "exI: \<ASSUMES> B a \<SHOWS> \<exists>x. B x"} \\
  @{text "exE: \<ASSUMES> \<exists>x. B x \<OBTAINS> a \<WHERE> B a"}
  \end{tabular}
  \<^medskip>

  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:
\<close>

(*<*)
theorem "\<And>A. PROP A \<Longrightarrow> PROP A"
proof -
(*>*)

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

  have "A \<longrightarrow> B"
  proof
    assume A
    show B sorry %noproof
  qed

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

  have "A \<longrightarrow> B" and A sorry %noproof
  then have B ..

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

  have A sorry %noproof
  then have "A \<or> B" ..

  have B sorry %noproof
  then have "A \<or> B" ..

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

  have "A \<or> B" sorry %noproof
  then have C
  proof
    assume A
    then show C sorry %noproof
  next
    assume B
    then show C sorry %noproof
  qed

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

  have A and B sorry %noproof
  then have "A \<and> B" ..

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

  have "A \<and> B" sorry %noproof
  then obtain A and B ..

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

  have "\<bottom>" sorry %noproof
  then have A ..

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

  have "\<top>" ..

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

  have "\<not> A"
  proof
    assume A
    then show "\<bottom>" sorry %noproof
  qed

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

  have "\<not> A" and A sorry %noproof
  then have B ..

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

  have "\<forall>x. B x"
  proof
    fix x
    show "B x" sorry %noproof
  qed

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

  have "\<forall>x. B x" sorry %noproof
  then have "B a" ..

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

  have "\<exists>x. B x"
  proof
    show "B a" sorry %noproof
  qed

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

  have "\<exists>x. B x" sorry %noproof
  then obtain a where "B a" ..

  text_raw \<open>\end{minipage}\<close>

(*<*)
qed
(*>*)

text \<open>
  \<^bigskip>
  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.
\<close>

end %visible