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
```