104

1 
(**** FOL examples ****)


2 


3 
Pretty.setmargin 72; (*existing macros just allow this margin*)


4 
print_depth 0;


5 


6 
(*** Intuitionistic examples ***)


7 


8 
(*Quantifier example from Logic&Computation*)


9 
goal Int_Rule.thy "(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))";


10 
by (resolve_tac [impI] 1);


11 
by (resolve_tac [allI] 1);


12 
by (resolve_tac [exI] 1);


13 
by (eresolve_tac [exE] 1);


14 
choplev 2;


15 
by (eresolve_tac [exE] 1);


16 
by (resolve_tac [exI] 1);


17 
by (eresolve_tac [allE] 1);


18 
by (assume_tac 1);


19 


20 


21 
(*Example of Dyckhoff's method*)


22 
goalw Int_Rule.thy [not_def] "~ ~ ((P>Q)  (Q>P))";


23 
by (resolve_tac [impI] 1);


24 
by (eresolve_tac [disj_impE] 1);


25 
by (eresolve_tac [imp_impE] 1);


26 
by (eresolve_tac [imp_impE] 1);


27 
by (REPEAT (eresolve_tac [FalseE] 2));


28 
by (assume_tac 1);


29 


30 


31 


32 
 goal Int_Rule.thy "(EX ay. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))";


33 
Level 0


34 
(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))


35 
1. (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))


36 
 by (resolve_tac [impI] 1);


37 
Level 1


38 
(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))


39 
1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)


40 
 by (resolve_tac [allI] 1);


41 
Level 2


42 
(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))


43 
1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)


44 
 by (resolve_tac [exI] 1);


45 
Level 3


46 
(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))


47 
1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))


48 
 by (eresolve_tac [exE] 1);


49 
Level 4


50 
(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))


51 
1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))


52 
 choplev 2;


53 
Level 2


54 
(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))


55 
1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)


56 
 by (eresolve_tac [exE] 1);


57 
Level 3


58 
(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))


59 
1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)


60 
 by (resolve_tac [exI] 1);


61 
Level 4


62 
(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))


63 
1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))


64 
 by (eresolve_tac [allE] 1);


65 
Level 5


66 
(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))


67 
1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))


68 
 by (assume_tac 1);


69 
Level 6


70 
(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))


71 
No subgoals!


72 


73 


74 


75 
> goalw Int_Rule.thy [not_def] "~ ~ ((P>Q)  (Q>P))";


76 
Level 0


77 
~ ~ ((P > Q)  (Q > P))


78 
1. ((P > Q)  (Q > P) > False) > False


79 
> by (resolve_tac [impI] 1);


80 
Level 1


81 
~ ~ ((P > Q)  (Q > P))


82 
1. (P > Q)  (Q > P) > False ==> False


83 
> by (eresolve_tac [disj_impE] 1);


84 
Level 2


85 
~ ~ ((P > Q)  (Q > P))


86 
1. [ (P > Q) > False; (Q > P) > False ] ==> False


87 
> by (eresolve_tac [imp_impE] 1);


88 
Level 3


89 
~ ~ ((P > Q)  (Q > P))


90 
1. [ (Q > P) > False; P; Q > False ] ==> Q


91 
2. [ (Q > P) > False; False ] ==> False


92 
> by (eresolve_tac [imp_impE] 1);


93 
Level 4


94 
~ ~ ((P > Q)  (Q > P))


95 
1. [ P; Q > False; Q; P > False ] ==> P


96 
2. [ P; Q > False; False ] ==> Q


97 
3. [ (Q > P) > False; False ] ==> False


98 
> by (REPEAT (eresolve_tac [FalseE] 2));


99 
Level 5


100 
~ ~ ((P > Q)  (Q > P))


101 
1. [ P; Q > False; Q; P > False ] ==> P


102 
> by (assume_tac 1);


103 
Level 6


104 
~ ~ ((P > Q)  (Q > P))


105 
No subgoals!


106 


107 


108 


109 


110 
(*** Classical examples ***)


111 


112 
goal cla_thy "EX y. ALL x. P(y)>P(x)";


113 
by (resolve_tac [exCI] 1);


114 
by (resolve_tac [allI] 1);


115 
by (resolve_tac [impI] 1);


116 
by (eresolve_tac [allE] 1);


117 
prth (allI RSN (2,swap));


118 
by (eresolve_tac [it] 1);


119 
by (resolve_tac [impI] 1);


120 
by (eresolve_tac [notE] 1);


121 
by (assume_tac 1);


122 
goal cla_thy "EX y. ALL x. P(y)>P(x)";


123 
by (best_tac FOL_dup_cs 1);


124 


125 


126 


127 
 goal cla_thy "EX y. ALL x. P(y)>P(x)";


128 
Level 0


129 
EX y. ALL x. P(y) > P(x)


130 
1. EX y. ALL x. P(y) > P(x)


131 
 by (resolve_tac [exCI] 1);


132 
Level 1


133 
EX y. ALL x. P(y) > P(x)


134 
1. ALL y. ~(ALL x. P(y) > P(x)) ==> ALL x. P(?a) > P(x)


135 
 by (resolve_tac [allI] 1);


136 
Level 2


137 
EX y. ALL x. P(y) > P(x)


138 
1. !!x. ALL y. ~(ALL x. P(y) > P(x)) ==> P(?a) > P(x)


139 
 by (resolve_tac [impI] 1);


140 
Level 3


141 
EX y. ALL x. P(y) > P(x)


142 
1. !!x. [ ALL y. ~(ALL x. P(y) > P(x)); P(?a) ] ==> P(x)


143 
 by (eresolve_tac [allE] 1);


144 
Level 4


145 
EX y. ALL x. P(y) > P(x)


146 
1. !!x. [ P(?a); ~(ALL xa. P(?y3(x)) > P(xa)) ] ==> P(x)


147 
 prth (allI RSN (2,swap));


148 
[ ~(ALL x. ?P1(x)); !!x. ~?Q ==> ?P1(x) ] ==> ?Q


149 
 by (eresolve_tac [it] 1);


150 
Level 5


151 
EX y. ALL x. P(y) > P(x)


152 
1. !!x xa. [ P(?a); ~P(x) ] ==> P(?y3(x)) > P(xa)


153 
 by (resolve_tac [impI] 1);


154 
Level 6


155 
EX y. ALL x. P(y) > P(x)


156 
1. !!x xa. [ P(?a); ~P(x); P(?y3(x)) ] ==> P(xa)


157 
 by (eresolve_tac [notE] 1);


158 
Level 7


159 
EX y. ALL x. P(y) > P(x)


160 
1. !!x xa. [ P(?a); P(?y3(x)) ] ==> P(x)


161 
 by (assume_tac 1);


162 
Level 8


163 
EX y. ALL x. P(y) > P(x)


164 
No subgoals!


165 
 goal cla_thy "EX y. ALL x. P(y)>P(x)";


166 
Level 0


167 
EX y. ALL x. P(y) > P(x)


168 
1. EX y. ALL x. P(y) > P(x)


169 
 by (best_tac FOL_dup_cs 1);


170 
Level 1


171 
EX y. ALL x. P(y) > P(x)


172 
No subgoals!


173 


174 


175 
(**** finally, the example FOL/ex/if.ML ****)


176 


177 
> val prems = goalw if_thy [if_def]


178 
# "[ P ==> Q; ~P ==> R ] ==> if(P,Q,R)";


179 
Level 0


180 
if(P,Q,R)


181 
1. P & Q  ~P & R


182 
> by (Classical.fast_tac (FOL_cs addIs prems) 1);


183 
Level 1


184 
if(P,Q,R)


185 
No subgoals!


186 
> val ifI = result();


187 


188 


189 
> val major::prems = goalw if_thy [if_def]


190 
# "[ if(P,Q,R); [ P; Q ] ==> S; [ ~P; R ] ==> S ] ==> S";


191 
Level 0


192 
S


193 
1. S


194 
> by (cut_facts_tac [major] 1);


195 
Level 1


196 
S


197 
1. P & Q  ~P & R ==> S


198 
> by (Classical.fast_tac (FOL_cs addIs prems) 1);


199 
Level 2


200 
S


201 
No subgoals!


202 
> val ifE = result();


203 


204 
> goal if_thy "if(P, if(Q,A,B), if(Q,C,D)) <> if(Q, if(P,A,C), if(P,B,D))";


205 
Level 0


206 
if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))


207 
1. if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))


208 
> by (resolve_tac [iffI] 1);


209 
Level 1


210 
if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))


211 
1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))


212 
2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))


213 
> by (eresolve_tac [ifE] 1);


214 
Level 2


215 
if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))


216 
1. [ P; if(Q,A,B) ] ==> if(Q,if(P,A,C),if(P,B,D))


217 
2. [ ~P; if(Q,C,D) ] ==> if(Q,if(P,A,C),if(P,B,D))


218 
3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))


219 
> by (eresolve_tac [ifE] 1);


220 
Level 3


221 
if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))


222 
1. [ P; Q; A ] ==> if(Q,if(P,A,C),if(P,B,D))


223 
2. [ P; ~Q; B ] ==> if(Q,if(P,A,C),if(P,B,D))


224 
3. [ ~P; if(Q,C,D) ] ==> if(Q,if(P,A,C),if(P,B,D))


225 
4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))


226 
> by (resolve_tac [ifI] 1);


227 
Level 4


228 
if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))


229 
1. [ P; Q; A; Q ] ==> if(P,A,C)


230 
2. [ P; Q; A; ~Q ] ==> if(P,B,D)


231 
3. [ P; ~Q; B ] ==> if(Q,if(P,A,C),if(P,B,D))


232 
4. [ ~P; if(Q,C,D) ] ==> if(Q,if(P,A,C),if(P,B,D))


233 
5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))


234 
> by (resolve_tac [ifI] 1);


235 
Level 5


236 
if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))


237 
1. [ P; Q; A; Q; P ] ==> A


238 
2. [ P; Q; A; Q; ~P ] ==> C


239 
3. [ P; Q; A; ~Q ] ==> if(P,B,D)


240 
4. [ P; ~Q; B ] ==> if(Q,if(P,A,C),if(P,B,D))


241 
5. [ ~P; if(Q,C,D) ] ==> if(Q,if(P,A,C),if(P,B,D))


242 
6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))


243 


244 
> choplev 0;


245 
Level 0


246 
if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))


247 
1. if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))


248 
> val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];


249 
> by (Classical.fast_tac if_cs 1);


250 
Level 1


251 
if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))


252 
No subgoals!


253 
> val if_commute = result();


254 


255 
> goal if_thy "if(if(P,Q,R), A, B) <> if(P, if(Q,A,B), if(R,A,B))";


256 
Level 0


257 
if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))


258 
1. if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))


259 
> by (Classical.fast_tac if_cs 1);


260 
Level 1


261 
if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))


262 
No subgoals!


263 
> val nested_ifs = result();


264 


265 


266 
> choplev 0;


267 
Level 0


268 
if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))


269 
1. if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))


270 
> by (rewrite_goals_tac [if_def]);


271 
Level 1


272 
if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))


273 
1. (P & Q  ~P & R) & A  ~(P & Q  ~P & R) & B <>


274 
P & (Q & A  ~Q & B)  ~P & (R & A  ~R & B)


275 
> by (Classical.fast_tac FOL_cs 1);


276 
Level 2


277 
if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))


278 
No subgoals!


279 


280 


281 
> goal if_thy "if(if(P,Q,R), A, B) <> if(P, if(Q,A,B), if(R,B,A))";


282 
Level 0


283 
if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))


284 
1. if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))


285 
> by (REPEAT (Classical.step_tac if_cs 1));


286 
Level 1


287 
if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))


288 
1. [ A; ~P; R; ~P; R ] ==> B


289 
2. [ B; ~P; ~R; ~P; ~R ] ==> A


290 
3. [ ~P; R; B; ~P; R ] ==> A


291 
4. [ ~P; ~R; A; ~B; ~P ] ==> R


292 


293 
> choplev 0;


294 
Level 0


295 
if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))


296 
1. if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))


297 
> by (rewrite_goals_tac [if_def]);


298 
Level 1


299 
if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))


300 
1. (P & Q  ~P & R) & A  ~(P & Q  ~P & R) & B <>


301 
P & (Q & A  ~Q & B)  ~P & (R & B  ~R & A)


302 
> by (Classical.fast_tac FOL_cs 1);


303 
by: tactic failed


304 
Exception ERROR raised


305 
Exception failure raised


306 


307 
> by (REPEAT (Classical.step_tac FOL_cs 1));


308 
Level 2


309 
if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))


310 
1. [ A; ~P; R; ~P; R; ~False ] ==> B


311 
2. [ A; ~P; R; R; ~False; ~B; ~B ] ==> Q


312 
3. [ B; ~P; ~R; ~P; ~A ] ==> R


313 
4. [ B; ~P; ~R; ~Q; ~A ] ==> R


314 
5. [ B; ~R; ~P; ~A; ~R; Q; ~False ] ==> A


315 
6. [ ~P; R; B; ~P; R; ~False ] ==> A


316 
7. [ ~P; ~R; A; ~B; ~R ] ==> P


317 
8. [ ~P; ~R; A; ~B; ~R ] ==> Q
