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