doc-src/Intro/theorems.txt

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Intro/theorems.txt	Wed Nov 10 05:06:55 1993 +0100
@@ -0,0 +1,122 @@
+Pretty.setmargin 72;  (*existing macros just allow this margin*)
+print_depth 0;
+
+(*operations for "thm"*)
+
+prth mp; 
+
+prth (mp RS mp);
+
+prth (conjunct1 RS mp);
+prth (conjunct1 RSN (2,mp));
+
+prth (mp RS conjunct1);
+prth (spec RS it);
+prth (standard it);
+
+prth spec;
+prth (it RS mp);
+prth (it RS conjunct1);
+prth (standard it);
+
+- prth spec;
+ALL x. ?P(x) ==> ?P(?x)
+- prth (it RS mp);
+[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==> ?Q2(?x1)
+- prth (it RS conjunct1);
+[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==> ?P6(?x2)
+- prth (standard it);
+[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==> ?Pa(?x)
+
+(*flexflex pairs*)
+- prth refl;
+?a = ?a
+- prth exI;
+?P(?x) ==> EX x. ?P(x)
+- prth (refl RS exI);
+?a3(?x) == ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)
+- prthq (flexflex_rule it);
+EX x. ?a4 = ?a4
+
+(*Usage of RL*)
+- val reflk = prth (read_instantiate [("a","k")] refl);
+k = k
+val reflk = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
+- prth (reflk RS exI);
+
+uncaught exception THM
+- prths ([reflk] RL [exI]);
+EX x. x = x
+
+EX x. k = x
+
+EX x. x = k
+
+EX x. k = k
+
+
+
+(*tactics *)
+
+goal cla_thy "P|P --> P";
+by (resolve_tac [impI] 1);
+by (resolve_tac [disjE] 1);
+by (assume_tac 3);
+by (assume_tac 2);
+by (assume_tac 1);
+val mythm = prth(result());
+
+
+goal cla_thy "(P & Q) | R  --> (P | R)";
+by (resolve_tac [impI] 1);
+by (eresolve_tac [disjE] 1);
+by (dresolve_tac [conjunct1] 1);
+by (resolve_tac [disjI1] 1);
+by (resolve_tac [disjI2] 2);
+by (REPEAT (assume_tac 1));
+
+
+- goal cla_thy "(P & Q) | R  --> (P | R)";
+Level 0
+P & Q | R --> P | R
+ 1. P & Q | R --> P | R
+- by (resolve_tac [impI] 1);
+Level 1
+P & Q | R --> P | R
+ 1. P & Q | R ==> P | R
+- by (eresolve_tac [disjE] 1);
+Level 2
+P & Q | R --> P | R
+ 1. P & Q ==> P | R
+ 2. R ==> P | R
+- by (dresolve_tac [conjunct1] 1);
+Level 3
+P & Q | R --> P | R
+ 1. P ==> P | R
+ 2. R ==> P | R
+- by (resolve_tac [disjI1] 1);
+Level 4
+P & Q | R --> P | R
+ 1. P ==> P
+ 2. R ==> P | R
+- by (resolve_tac [disjI2] 2);
+Level 5
+P & Q | R --> P | R
+ 1. P ==> P
+ 2. R ==> R
+- by (REPEAT (assume_tac 1));
+Level 6
+P & Q | R --> P | R
+No subgoals!
+
+
+goal cla_thy "(P | Q) | R  -->  P | (Q | R)";
+by (resolve_tac [impI] 1);
+by (eresolve_tac [disjE] 1);
+by (eresolve_tac [disjE] 1);
+by (resolve_tac [disjI1] 1);
+by (resolve_tac [disjI2] 2);
+by (resolve_tac [disjI1] 2);
+by (resolve_tac [disjI2] 3);
+by (resolve_tac [disjI2] 3);
+by (REPEAT (assume_tac 1));