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