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