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