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