src/FOL/ex/prop.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 1459 d12da312eff4
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	FOL/ex/prop
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@0
     6
First-Order Logic: propositional examples (intuitionistic and classical)
clasohm@0
     7
Needs declarations of the theory "thy" and the tactic "tac"
clasohm@0
     8
*)
clasohm@0
     9
clasohm@0
    10
writeln"File FOL/ex/prop.";
clasohm@0
    11
clasohm@0
    12
clasohm@0
    13
writeln"commutative laws of & and | ";
clasohm@0
    14
goal thy "P & Q  -->  Q & P";
clasohm@0
    15
by tac;
clasohm@0
    16
result();
clasohm@0
    17
clasohm@0
    18
goal thy "P | Q  -->  Q | P";
clasohm@0
    19
by tac;
clasohm@0
    20
result();
clasohm@0
    21
clasohm@0
    22
clasohm@0
    23
writeln"associative laws of & and | ";
clasohm@0
    24
goal thy "(P & Q) & R  -->  P & (Q & R)";
clasohm@0
    25
by tac;
clasohm@0
    26
result();
clasohm@0
    27
clasohm@0
    28
goal thy "(P | Q) | R  -->  P | (Q | R)";
clasohm@0
    29
by tac;
clasohm@0
    30
result();
clasohm@0
    31
clasohm@0
    32
clasohm@0
    33
clasohm@0
    34
writeln"distributive laws of & and | ";
clasohm@0
    35
goal thy "(P & Q) | R  --> (P | R) & (Q | R)";
clasohm@0
    36
by tac;
clasohm@0
    37
result();
clasohm@0
    38
clasohm@0
    39
goal thy "(P | R) & (Q | R)  --> (P & Q) | R";
clasohm@0
    40
by tac;
clasohm@0
    41
result();
clasohm@0
    42
clasohm@0
    43
goal thy "(P | Q) & R  --> (P & R) | (Q & R)";
clasohm@0
    44
by tac;
clasohm@0
    45
result();
clasohm@0
    46
clasohm@0
    47
clasohm@0
    48
goal thy "(P & R) | (Q & R)  --> (P | Q) & R";
clasohm@0
    49
by tac;
clasohm@0
    50
result();
clasohm@0
    51
clasohm@0
    52
clasohm@0
    53
writeln"Laws involving implication";
clasohm@0
    54
clasohm@0
    55
goal thy "(P-->R) & (Q-->R) <-> (P|Q --> R)";
clasohm@0
    56
by tac;
clasohm@0
    57
result();
clasohm@0
    58
clasohm@0
    59
clasohm@0
    60
goal thy "(P & Q --> R) <-> (P--> (Q-->R))";
clasohm@0
    61
by tac;
clasohm@0
    62
result();
clasohm@0
    63
clasohm@0
    64
clasohm@0
    65
goal thy "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";
clasohm@0
    66
by tac;
clasohm@0
    67
result();
clasohm@0
    68
clasohm@0
    69
goal thy "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";
clasohm@0
    70
by tac;
clasohm@0
    71
result();
clasohm@0
    72
clasohm@0
    73
goal thy "(P --> Q & R) <-> (P-->Q)  &  (P-->R)";
clasohm@0
    74
by tac;
clasohm@0
    75
result();
clasohm@0
    76
clasohm@0
    77
clasohm@0
    78
writeln"Propositions-as-types";
clasohm@0
    79
clasohm@0
    80
(*The combinator K*)
clasohm@0
    81
goal thy "P --> (Q --> P)";
clasohm@0
    82
by tac;
clasohm@0
    83
result();
clasohm@0
    84
clasohm@0
    85
(*The combinator S*)
clasohm@0
    86
goal thy "(P-->Q-->R)  --> (P-->Q) --> (P-->R)";
clasohm@0
    87
by tac;
clasohm@0
    88
result();
clasohm@0
    89
clasohm@0
    90
clasohm@0
    91
(*Converse is classical*)
clasohm@0
    92
goal thy "(P-->Q) | (P-->R)  -->  (P --> Q | R)";
clasohm@0
    93
by tac;
clasohm@0
    94
result();
clasohm@0
    95
clasohm@0
    96
goal thy "(P-->Q)  -->  (~Q --> ~P)";
clasohm@0
    97
by tac;
clasohm@0
    98
result();
clasohm@0
    99
clasohm@0
   100
clasohm@0
   101
writeln"Schwichtenberg's examples (via T. Nipkow)";
clasohm@0
   102
clasohm@0
   103
(* stab-imp *)
clasohm@0
   104
goal thy "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q";
clasohm@0
   105
by tac;
clasohm@0
   106
result();
clasohm@0
   107
clasohm@0
   108
(* stab-to-peirce *)
clasohm@0
   109
goal thy "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
clasohm@0
   110
\	      --> ((P --> Q) --> P) --> P";
clasohm@0
   111
by tac;
clasohm@0
   112
result();
clasohm@0
   113
clasohm@0
   114
(* peirce-imp1 *)
clasohm@0
   115
goal thy "(((Q --> R) --> Q) --> Q) \
clasohm@0
   116
\	       --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
clasohm@0
   117
by tac;
clasohm@0
   118
result();
clasohm@0
   119
  
clasohm@0
   120
(* peirce-imp2 *)
clasohm@0
   121
goal thy "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
clasohm@0
   122
by tac;
clasohm@0
   123
result();
clasohm@0
   124
clasohm@0
   125
(* mints  *)
clasohm@0
   126
goal thy "((((P --> Q) --> P) --> P) --> Q) --> Q";
clasohm@0
   127
by tac;
clasohm@0
   128
result();
clasohm@0
   129
clasohm@0
   130
(* mints-solovev *)
clasohm@0
   131
goal thy "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
clasohm@0
   132
by tac;
clasohm@0
   133
result();
clasohm@0
   134
clasohm@0
   135
(* tatsuta *)
clasohm@0
   136
goal thy "(((P7 --> P1) --> P10) --> P4 --> P5) \
clasohm@0
   137
\	  --> (((P8 --> P2) --> P9) --> P3 --> P10) \
clasohm@0
   138
\	  --> (P1 --> P8) --> P6 --> P7 \
clasohm@0
   139
\	  --> (((P3 --> P2) --> P9) --> P4) \
clasohm@0
   140
\	  --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5";
clasohm@0
   141
by tac;
clasohm@0
   142
result();
clasohm@0
   143
clasohm@0
   144
(* tatsuta1 *)
clasohm@0
   145
goal thy "(((P8 --> P2) --> P9) --> P3 --> P10) \
clasohm@0
   146
\    --> (((P3 --> P2) --> P9) --> P4) \
clasohm@0
   147
\    --> (((P6 --> P1) --> P2) --> P9) \
clasohm@0
   148
\    --> (((P7 --> P1) --> P10) --> P4 --> P5) \
clasohm@0
   149
\    --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5";
clasohm@0
   150
by tac;
clasohm@0
   151
result();
clasohm@0
   152
clasohm@0
   153
writeln"Reached end of file.";