src/Sequents/LK/Propositional.thy
author wenzelm
Sat Jun 02 22:40:03 2018 +0200 (18 months ago)
changeset 68358 e761afd35baa
parent 61386 0a29a984a91b
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      Sequents/LK/Propositional.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1992  University of Cambridge
     4 *)
     5 
     6 section \<open>Classical sequent calculus: examples with propositional connectives\<close>
     7 
     8 theory Propositional
     9 imports "../LK"
    10 begin
    11 
    12 text "absorptive laws of \<and> and \<or>"
    13 
    14 lemma "\<turnstile> P \<and> P \<longleftrightarrow> P"
    15   by fast_prop
    16 
    17 lemma "\<turnstile> P \<or> P \<longleftrightarrow> P"
    18   by fast_prop
    19 
    20 
    21 text "commutative laws of \<and> and \<or>"
    22 
    23 lemma "\<turnstile> P \<and> Q \<longleftrightarrow> Q \<and> P"
    24   by fast_prop
    25 
    26 lemma "\<turnstile> P \<or> Q \<longleftrightarrow> Q \<or> P"
    27   by fast_prop
    28 
    29 
    30 text "associative laws of \<and> and \<or>"
    31 
    32 lemma "\<turnstile> (P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
    33   by fast_prop
    34 
    35 lemma "\<turnstile> (P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
    36   by fast_prop
    37 
    38 
    39 text "distributive laws of \<and> and \<or>"
    40 
    41 lemma "\<turnstile> (P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)"
    42   by fast_prop
    43 
    44 lemma "\<turnstile> (P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R) \<or> (Q \<and> R)"
    45   by fast_prop
    46 
    47 
    48 text "Laws involving implication"
    49 
    50 lemma "\<turnstile> (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
    51   by fast_prop
    52 
    53 lemma "\<turnstile> (P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
    54   by fast_prop
    55 
    56 lemma "\<turnstile> (P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
    57   by fast_prop
    58 
    59 
    60 text "Classical theorems"
    61 
    62 lemma "\<turnstile> P \<or> Q \<longrightarrow> P \<or> \<not> P \<and> Q"
    63   by fast_prop
    64 
    65 lemma "\<turnstile> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<or> R)"
    66   by fast_prop
    67 
    68 lemma "\<turnstile> P \<and> Q \<or> \<not> P \<and> R \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R)"
    69   by fast_prop
    70 
    71 lemma "\<turnstile> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
    72   by fast_prop
    73 
    74 
    75 (*If and only if*)
    76 
    77 lemma "\<turnstile> (P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
    78   by fast_prop
    79 
    80 lemma "\<turnstile> \<not> (P \<longleftrightarrow> \<not> P)"
    81   by fast_prop
    82 
    83 
    84 (*Sample problems from 
    85   F. J. Pelletier, 
    86   Seventy-Five Problems for Testing Automatic Theorem Provers,
    87   J. Automated Reasoning 2 (1986), 191-216.
    88   Errata, JAR 4 (1988), 236-236.
    89 *)
    90 
    91 (*1*)
    92 lemma "\<turnstile> (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
    93   by fast_prop
    94 
    95 (*2*)
    96 lemma "\<turnstile> \<not> \<not> P \<longleftrightarrow> P"
    97   by fast_prop
    98 
    99 (*3*)
   100 lemma "\<turnstile> \<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
   101   by fast_prop
   102 
   103 (*4*)
   104 lemma "\<turnstile> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"
   105   by fast_prop
   106 
   107 (*5*)
   108 lemma "\<turnstile> ((P \<or> Q) \<longrightarrow> (P \<or> R)) \<longrightarrow> (P \<or> (Q \<longrightarrow> R))"
   109   by fast_prop
   110 
   111 (*6*)
   112 lemma "\<turnstile> P \<or> \<not> P"
   113   by fast_prop
   114 
   115 (*7*)
   116 lemma "\<turnstile> P \<or> \<not> \<not> \<not> P"
   117   by fast_prop
   118 
   119 (*8.  Peirce's law*)
   120 lemma "\<turnstile> ((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
   121   by fast_prop
   122 
   123 (*9*)
   124 lemma "\<turnstile> ((P \<or> Q) \<and> (\<not> P \<or> Q) \<and> (P \<or> \<not> Q)) \<longrightarrow> \<not> (\<not> P \<or> \<not> Q)"
   125   by fast_prop
   126 
   127 (*10*)
   128 lemma "Q \<longrightarrow> R, R \<longrightarrow> P \<and> Q, P \<longrightarrow> (Q \<or> R) \<turnstile> P \<longleftrightarrow> Q"
   129   by fast_prop
   130 
   131 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
   132 lemma "\<turnstile> P \<longleftrightarrow> P"
   133   by fast_prop
   134 
   135 (*12.  "Dijkstra's law"*)
   136 lemma "\<turnstile> ((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
   137   by fast_prop
   138 
   139 (*13.  Distributive law*)
   140 lemma "\<turnstile> P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
   141   by fast_prop
   142 
   143 (*14*)
   144 lemma "\<turnstile> (P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P))"
   145   by fast_prop
   146 
   147 (*15*)
   148 lemma "\<turnstile> (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
   149   by fast_prop
   150 
   151 (*16*)
   152 lemma "\<turnstile> (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"
   153   by fast_prop
   154 
   155 (*17*)
   156 lemma "\<turnstile> ((P \<and> (Q \<longrightarrow> R)) \<longrightarrow> S) \<longleftrightarrow> ((\<not> P \<or> Q \<or> S) \<and> (\<not> P \<or> \<not> R \<or> S))"
   157   by fast_prop
   158 
   159 end