doc-src/Intro/theorems.txt
changeset 105 216d6ed87399
child 459 03b445551763
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Intro/theorems.txt	Wed Nov 10 05:06:55 1993 +0100
     1.3 @@ -0,0 +1,122 @@
     1.4 +Pretty.setmargin 72;  (*existing macros just allow this margin*)
     1.5 +print_depth 0;
     1.6 +
     1.7 +(*operations for "thm"*)
     1.8 +
     1.9 +prth mp; 
    1.10 +
    1.11 +prth (mp RS mp);
    1.12 +
    1.13 +prth (conjunct1 RS mp);
    1.14 +prth (conjunct1 RSN (2,mp));
    1.15 +
    1.16 +prth (mp RS conjunct1);
    1.17 +prth (spec RS it);
    1.18 +prth (standard it);
    1.19 +
    1.20 +prth spec;
    1.21 +prth (it RS mp);
    1.22 +prth (it RS conjunct1);
    1.23 +prth (standard it);
    1.24 +
    1.25 +- prth spec;
    1.26 +ALL x. ?P(x) ==> ?P(?x)
    1.27 +- prth (it RS mp);
    1.28 +[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==> ?Q2(?x1)
    1.29 +- prth (it RS conjunct1);
    1.30 +[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==> ?P6(?x2)
    1.31 +- prth (standard it);
    1.32 +[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==> ?Pa(?x)
    1.33 +
    1.34 +(*flexflex pairs*)
    1.35 +- prth refl;
    1.36 +?a = ?a
    1.37 +- prth exI;
    1.38 +?P(?x) ==> EX x. ?P(x)
    1.39 +- prth (refl RS exI);
    1.40 +?a3(?x) == ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)
    1.41 +- prthq (flexflex_rule it);
    1.42 +EX x. ?a4 = ?a4
    1.43 +
    1.44 +(*Usage of RL*)
    1.45 +- val reflk = prth (read_instantiate [("a","k")] refl);
    1.46 +k = k
    1.47 +val reflk = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
    1.48 +- prth (reflk RS exI);
    1.49 +
    1.50 +uncaught exception THM
    1.51 +- prths ([reflk] RL [exI]);
    1.52 +EX x. x = x
    1.53 +
    1.54 +EX x. k = x
    1.55 +
    1.56 +EX x. x = k
    1.57 +
    1.58 +EX x. k = k
    1.59 +
    1.60 +
    1.61 +
    1.62 +(*tactics *)
    1.63 +
    1.64 +goal cla_thy "P|P --> P";
    1.65 +by (resolve_tac [impI] 1);
    1.66 +by (resolve_tac [disjE] 1);
    1.67 +by (assume_tac 3);
    1.68 +by (assume_tac 2);
    1.69 +by (assume_tac 1);
    1.70 +val mythm = prth(result());
    1.71 +
    1.72 +
    1.73 +goal cla_thy "(P & Q) | R  --> (P | R)";
    1.74 +by (resolve_tac [impI] 1);
    1.75 +by (eresolve_tac [disjE] 1);
    1.76 +by (dresolve_tac [conjunct1] 1);
    1.77 +by (resolve_tac [disjI1] 1);
    1.78 +by (resolve_tac [disjI2] 2);
    1.79 +by (REPEAT (assume_tac 1));
    1.80 +
    1.81 +
    1.82 +- goal cla_thy "(P & Q) | R  --> (P | R)";
    1.83 +Level 0
    1.84 +P & Q | R --> P | R
    1.85 + 1. P & Q | R --> P | R
    1.86 +- by (resolve_tac [impI] 1);
    1.87 +Level 1
    1.88 +P & Q | R --> P | R
    1.89 + 1. P & Q | R ==> P | R
    1.90 +- by (eresolve_tac [disjE] 1);
    1.91 +Level 2
    1.92 +P & Q | R --> P | R
    1.93 + 1. P & Q ==> P | R
    1.94 + 2. R ==> P | R
    1.95 +- by (dresolve_tac [conjunct1] 1);
    1.96 +Level 3
    1.97 +P & Q | R --> P | R
    1.98 + 1. P ==> P | R
    1.99 + 2. R ==> P | R
   1.100 +- by (resolve_tac [disjI1] 1);
   1.101 +Level 4
   1.102 +P & Q | R --> P | R
   1.103 + 1. P ==> P
   1.104 + 2. R ==> P | R
   1.105 +- by (resolve_tac [disjI2] 2);
   1.106 +Level 5
   1.107 +P & Q | R --> P | R
   1.108 + 1. P ==> P
   1.109 + 2. R ==> R
   1.110 +- by (REPEAT (assume_tac 1));
   1.111 +Level 6
   1.112 +P & Q | R --> P | R
   1.113 +No subgoals!
   1.114 +
   1.115 +
   1.116 +goal cla_thy "(P | Q) | R  -->  P | (Q | R)";
   1.117 +by (resolve_tac [impI] 1);
   1.118 +by (eresolve_tac [disjE] 1);
   1.119 +by (eresolve_tac [disjE] 1);
   1.120 +by (resolve_tac [disjI1] 1);
   1.121 +by (resolve_tac [disjI2] 2);
   1.122 +by (resolve_tac [disjI1] 2);
   1.123 +by (resolve_tac [disjI2] 3);
   1.124 +by (resolve_tac [disjI2] 3);
   1.125 +by (REPEAT (assume_tac 1));