doc-src/Intro/theorems.txt
author lcp
Wed Nov 10 05:06:55 1993 +0100 (1993-11-10)
changeset 105 216d6ed87399
child 459 03b445551763
permissions -rw-r--r--
Initial revision
lcp@105
     1
Pretty.setmargin 72;  (*existing macros just allow this margin*)
lcp@105
     2
print_depth 0;
lcp@105
     3
lcp@105
     4
(*operations for "thm"*)
lcp@105
     5
lcp@105
     6
prth mp; 
lcp@105
     7
lcp@105
     8
prth (mp RS mp);
lcp@105
     9
lcp@105
    10
prth (conjunct1 RS mp);
lcp@105
    11
prth (conjunct1 RSN (2,mp));
lcp@105
    12
lcp@105
    13
prth (mp RS conjunct1);
lcp@105
    14
prth (spec RS it);
lcp@105
    15
prth (standard it);
lcp@105
    16
lcp@105
    17
prth spec;
lcp@105
    18
prth (it RS mp);
lcp@105
    19
prth (it RS conjunct1);
lcp@105
    20
prth (standard it);
lcp@105
    21
lcp@105
    22
- prth spec;
lcp@105
    23
ALL x. ?P(x) ==> ?P(?x)
lcp@105
    24
- prth (it RS mp);
lcp@105
    25
[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==> ?Q2(?x1)
lcp@105
    26
- prth (it RS conjunct1);
lcp@105
    27
[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==> ?P6(?x2)
lcp@105
    28
- prth (standard it);
lcp@105
    29
[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==> ?Pa(?x)
lcp@105
    30
lcp@105
    31
(*flexflex pairs*)
lcp@105
    32
- prth refl;
lcp@105
    33
?a = ?a
lcp@105
    34
- prth exI;
lcp@105
    35
?P(?x) ==> EX x. ?P(x)
lcp@105
    36
- prth (refl RS exI);
lcp@105
    37
?a3(?x) == ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)
lcp@105
    38
- prthq (flexflex_rule it);
lcp@105
    39
EX x. ?a4 = ?a4
lcp@105
    40
lcp@105
    41
(*Usage of RL*)
lcp@105
    42
- val reflk = prth (read_instantiate [("a","k")] refl);
lcp@105
    43
k = k
lcp@105
    44
val reflk = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
lcp@105
    45
- prth (reflk RS exI);
lcp@105
    46
lcp@105
    47
uncaught exception THM
lcp@105
    48
- prths ([reflk] RL [exI]);
lcp@105
    49
EX x. x = x
lcp@105
    50
lcp@105
    51
EX x. k = x
lcp@105
    52
lcp@105
    53
EX x. x = k
lcp@105
    54
lcp@105
    55
EX x. k = k
lcp@105
    56
lcp@105
    57
lcp@105
    58
lcp@105
    59
(*tactics *)
lcp@105
    60
lcp@105
    61
goal cla_thy "P|P --> P";
lcp@105
    62
by (resolve_tac [impI] 1);
lcp@105
    63
by (resolve_tac [disjE] 1);
lcp@105
    64
by (assume_tac 3);
lcp@105
    65
by (assume_tac 2);
lcp@105
    66
by (assume_tac 1);
lcp@105
    67
val mythm = prth(result());
lcp@105
    68
lcp@105
    69
lcp@105
    70
goal cla_thy "(P & Q) | R  --> (P | R)";
lcp@105
    71
by (resolve_tac [impI] 1);
lcp@105
    72
by (eresolve_tac [disjE] 1);
lcp@105
    73
by (dresolve_tac [conjunct1] 1);
lcp@105
    74
by (resolve_tac [disjI1] 1);
lcp@105
    75
by (resolve_tac [disjI2] 2);
lcp@105
    76
by (REPEAT (assume_tac 1));
lcp@105
    77
lcp@105
    78
lcp@105
    79
- goal cla_thy "(P & Q) | R  --> (P | R)";
lcp@105
    80
Level 0
lcp@105
    81
P & Q | R --> P | R
lcp@105
    82
 1. P & Q | R --> P | R
lcp@105
    83
- by (resolve_tac [impI] 1);
lcp@105
    84
Level 1
lcp@105
    85
P & Q | R --> P | R
lcp@105
    86
 1. P & Q | R ==> P | R
lcp@105
    87
- by (eresolve_tac [disjE] 1);
lcp@105
    88
Level 2
lcp@105
    89
P & Q | R --> P | R
lcp@105
    90
 1. P & Q ==> P | R
lcp@105
    91
 2. R ==> P | R
lcp@105
    92
- by (dresolve_tac [conjunct1] 1);
lcp@105
    93
Level 3
lcp@105
    94
P & Q | R --> P | R
lcp@105
    95
 1. P ==> P | R
lcp@105
    96
 2. R ==> P | R
lcp@105
    97
- by (resolve_tac [disjI1] 1);
lcp@105
    98
Level 4
lcp@105
    99
P & Q | R --> P | R
lcp@105
   100
 1. P ==> P
lcp@105
   101
 2. R ==> P | R
lcp@105
   102
- by (resolve_tac [disjI2] 2);
lcp@105
   103
Level 5
lcp@105
   104
P & Q | R --> P | R
lcp@105
   105
 1. P ==> P
lcp@105
   106
 2. R ==> R
lcp@105
   107
- by (REPEAT (assume_tac 1));
lcp@105
   108
Level 6
lcp@105
   109
P & Q | R --> P | R
lcp@105
   110
No subgoals!
lcp@105
   111
lcp@105
   112
lcp@105
   113
goal cla_thy "(P | Q) | R  -->  P | (Q | R)";
lcp@105
   114
by (resolve_tac [impI] 1);
lcp@105
   115
by (eresolve_tac [disjE] 1);
lcp@105
   116
by (eresolve_tac [disjE] 1);
lcp@105
   117
by (resolve_tac [disjI1] 1);
lcp@105
   118
by (resolve_tac [disjI2] 2);
lcp@105
   119
by (resolve_tac [disjI1] 2);
lcp@105
   120
by (resolve_tac [disjI2] 3);
lcp@105
   121
by (resolve_tac [disjI2] 3);
lcp@105
   122
by (REPEAT (assume_tac 1));