105

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 

459

61 
goal FOL.thy "PP > P";

105

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 

459

70 
goal FOL.thy "(P & Q)  R > (P  R)";

105

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 

459

79 
 goal FOL.thy "(P & Q)  R > (P  R)";

105

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 

459

113 
goal FOL.thy "(P  Q)  R > P  (Q  R)";

105

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