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