src/FOL/ex/Propositional_Int.thy
author haftmann
Thu Nov 23 17:03:27 2017 +0000 (21 months ago)
changeset 67087 733017b19de9
parent 62020 5d208fd2507d
child 69590 e65314985426
permissions -rw-r--r--
generalized more lemmas
wenzelm@23914
     1
(*  Title:      FOL/ex/Propositional_Int.thy
wenzelm@23914
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@23914
     3
    Copyright   1991  University of Cambridge
wenzelm@23914
     4
*)
wenzelm@23914
     5
wenzelm@60770
     6
section \<open>First-Order Logic: propositional examples (intuitionistic version)\<close>
wenzelm@23914
     7
wenzelm@23914
     8
theory Propositional_Int
wenzelm@23914
     9
imports IFOL
wenzelm@23914
    10
begin
wenzelm@23914
    11
wenzelm@62020
    12
text \<open>commutative laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close>
wenzelm@23914
    13
wenzelm@61489
    14
lemma "P \<and> Q \<longrightarrow> Q \<and> P"
wenzelm@51798
    15
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    16
wenzelm@61489
    17
lemma "P \<or> Q \<longrightarrow> Q \<or> P"
wenzelm@51798
    18
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    19
wenzelm@23914
    20
wenzelm@62020
    21
text \<open>associative laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close>
wenzelm@61489
    22
lemma "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)"
wenzelm@51798
    23
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    24
wenzelm@61489
    25
lemma "(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)"
wenzelm@51798
    26
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    27
wenzelm@23914
    28
wenzelm@62020
    29
text \<open>distributive laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close>
wenzelm@61489
    30
lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)"
wenzelm@51798
    31
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    32
wenzelm@61489
    33
lemma "(P \<or> R) \<and> (Q \<or> R) \<longrightarrow> (P \<and> Q) \<or> R"
wenzelm@51798
    34
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    35
wenzelm@61489
    36
lemma "(P \<or> Q) \<and> R \<longrightarrow> (P \<and> R) \<or> (Q \<and> R)"
wenzelm@51798
    37
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    38
wenzelm@61489
    39
lemma "(P \<and> R) \<or> (Q \<and> R) \<longrightarrow> (P \<or> Q) \<and> R"
wenzelm@51798
    40
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    41
wenzelm@23914
    42
wenzelm@60770
    43
text \<open>Laws involving implication\<close>
wenzelm@23914
    44
wenzelm@61489
    45
lemma "(P \<longrightarrow> R) \<and> (Q \<longrightarrow> R) \<longleftrightarrow> (P \<or> Q \<longrightarrow> R)"
wenzelm@51798
    46
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    47
wenzelm@61489
    48
lemma "(P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
wenzelm@51798
    49
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    50
wenzelm@61489
    51
lemma "((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> ((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<longrightarrow> R) \<longrightarrow> R"
wenzelm@51798
    52
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    53
wenzelm@61489
    54
lemma "\<not> (P \<longrightarrow> R) \<longrightarrow> \<not> (Q \<longrightarrow> R) \<longrightarrow> \<not> (P \<and> Q \<longrightarrow> R)"
wenzelm@51798
    55
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    56
wenzelm@61489
    57
lemma "(P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
wenzelm@51798
    58
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    59
wenzelm@23914
    60
wenzelm@60770
    61
text \<open>Propositions-as-types\<close>
wenzelm@23914
    62
wenzelm@62020
    63
\<comment> \<open>The combinator K\<close>
wenzelm@61489
    64
lemma "P \<longrightarrow> (Q \<longrightarrow> P)"
wenzelm@51798
    65
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    66
wenzelm@62020
    67
\<comment> \<open>The combinator S\<close>
wenzelm@61489
    68
lemma "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R)"
wenzelm@51798
    69
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    70
wenzelm@23914
    71
wenzelm@62020
    72
\<comment> \<open>Converse is classical\<close>
wenzelm@61489
    73
lemma "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)"
wenzelm@51798
    74
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    75
wenzelm@61489
    76
lemma "(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
wenzelm@51798
    77
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    78
wenzelm@23914
    79
wenzelm@60770
    80
text \<open>Schwichtenberg's examples (via T. Nipkow)\<close>
wenzelm@23914
    81
wenzelm@61489
    82
lemma stab_imp: "(((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> (((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> P \<longrightarrow> Q"
wenzelm@51798
    83
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    84
wenzelm@23914
    85
lemma stab_to_peirce:
wenzelm@61489
    86
  "(((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> (((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> Q)
wenzelm@61489
    87
    \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
wenzelm@51798
    88
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    89
wenzelm@61489
    90
lemma peirce_imp1:
wenzelm@61489
    91
  "(((Q \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> Q)
wenzelm@61489
    92
    \<longrightarrow> (((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> P \<longrightarrow> Q) \<longrightarrow> P \<longrightarrow> Q"
wenzelm@51798
    93
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
    94
wenzelm@61489
    95
lemma peirce_imp2: "(((P \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> ((P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> P"
wenzelm@61489
    96
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@61489
    97
wenzelm@61489
    98
lemma mints: "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
wenzelm@51798
    99
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
   100
wenzelm@61489
   101
lemma mints_solovev: "(P \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> R"
wenzelm@51798
   102
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
   103
wenzelm@61489
   104
lemma tatsuta:
wenzelm@61489
   105
  "(((P7 \<longrightarrow> P1) \<longrightarrow> P10) \<longrightarrow> P4 \<longrightarrow> P5)
wenzelm@61489
   106
  \<longrightarrow> (((P8 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P3 \<longrightarrow> P10)
wenzelm@61489
   107
  \<longrightarrow> (P1 \<longrightarrow> P8) \<longrightarrow> P6 \<longrightarrow> P7
wenzelm@61489
   108
  \<longrightarrow> (((P3 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P4)
wenzelm@61489
   109
  \<longrightarrow> (P1 \<longrightarrow> P3) \<longrightarrow> (((P6 \<longrightarrow> P1) \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P5"
wenzelm@51798
   110
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
   111
wenzelm@61489
   112
lemma tatsuta1:
wenzelm@61489
   113
  "(((P8 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P3 \<longrightarrow> P10)
wenzelm@61489
   114
  \<longrightarrow> (((P3 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P4)
wenzelm@61489
   115
  \<longrightarrow> (((P6 \<longrightarrow> P1) \<longrightarrow> P2) \<longrightarrow> P9)
wenzelm@61489
   116
  \<longrightarrow> (((P7 \<longrightarrow> P1) \<longrightarrow> P10) \<longrightarrow> P4 \<longrightarrow> P5)
wenzelm@61489
   117
  \<longrightarrow> (P1 \<longrightarrow> P3) \<longrightarrow> (P1 \<longrightarrow> P8) \<longrightarrow> P6 \<longrightarrow> P7 \<longrightarrow> P5"
wenzelm@51798
   118
  by (tactic "IntPr.fast_tac @{context} 1")
wenzelm@23914
   119
wenzelm@23914
   120
end