doc-src/Intro/theorems.txt

clarified

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 FOL.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 FOL.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 FOL.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 FOL.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));