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