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