105

1 
(**** quantifier examples  process using Doc/tout quant.txt ****)


2 


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


4 
print_depth 0;


5 


6 


7 
goal Int_Rule.thy "(ALL x y.P(x,y)) > (ALL z w.P(w,z))";


8 
by (resolve_tac [impI] 1);


9 
by (dresolve_tac [spec] 1);


10 
by (resolve_tac [allI] 1);


11 
by (dresolve_tac [spec] 1);


12 
by (resolve_tac [allI] 1);


13 
by (assume_tac 1);


14 
choplev 1;


15 
by (resolve_tac [allI] 1);


16 
by (resolve_tac [allI] 1);


17 
by (dresolve_tac [spec] 1);


18 
by (dresolve_tac [spec] 1);


19 
by (assume_tac 1);


20 


21 
choplev 0;


22 
by (REPEAT (assume_tac 1


23 
ORELSE resolve_tac [impI,allI] 1


24 
ORELSE dresolve_tac [spec] 1));


25 


26 


27 
 goal Int_Rule.thy "(ALL x y.P(x,y)) > (ALL z w.P(w,z))";


28 
Level 0


29 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


30 
1. (ALL x y. P(x,y)) > (ALL z w. P(w,z))


31 
val it = [] : thm list


32 
 by (resolve_tac [impI] 1);


33 
Level 1


34 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


35 
1. ALL x y. P(x,y) ==> ALL z w. P(w,z)


36 
val it = () : unit


37 
 by (dresolve_tac [spec] 1);


38 
Level 2


39 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


40 
1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)


41 
val it = () : unit


42 
 by (resolve_tac [allI] 1);


43 
Level 3


44 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


45 
1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)


46 
val it = () : unit


47 
 by (dresolve_tac [spec] 1);


48 
Level 4


49 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


50 
1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)


51 
val it = () : unit


52 
 by (resolve_tac [allI] 1);


53 
Level 5


54 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


55 
1. !!z w. P(?x1,?y3(z)) ==> P(w,z)


56 
val it = () : unit


57 
 by (assume_tac 1);


58 
by: tactic returned no results


59 


60 
uncaught exception ERROR


61 
 choplev 1;


62 
Level 1


63 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


64 
1. ALL x y. P(x,y) ==> ALL z w. P(w,z)


65 
val it = () : unit


66 
 by (resolve_tac [allI] 1);


67 
Level 2


68 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


69 
1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)


70 
val it = () : unit


71 
 by (resolve_tac [allI] 1);


72 
Level 3


73 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


74 
1. !!z w. ALL x y. P(x,y) ==> P(w,z)


75 
val it = () : unit


76 
 by (dresolve_tac [spec] 1);


77 
Level 4


78 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


79 
1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)


80 
val it = () : unit


81 
 by (dresolve_tac [spec] 1);


82 
Level 5


83 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


84 
1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)


85 
val it = () : unit


86 
 by (assume_tac 1);


87 
Level 6


88 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


89 
No subgoals!


90 


91 
> choplev 0;


92 
Level 0


93 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


94 
1. (ALL x y. P(x,y)) > (ALL z w. P(w,z))


95 
> by (REPEAT (assume_tac 1


96 
# ORELSE resolve_tac [impI,allI] 1


97 
# ORELSE dresolve_tac [spec] 1));


98 
Level 1


99 
(ALL x y. P(x,y)) > (ALL z w. P(w,z))


100 
No subgoals!


101 


102 


103 


104 
goal FOL_thy "ALL x. EX y. x=y";


105 
by (resolve_tac [allI] 1);


106 
by (resolve_tac [exI] 1);


107 
by (resolve_tac [refl] 1);


108 


109 
 goal Int_Rule.thy "ALL x. EX y. x=y";


110 
Level 0


111 
ALL x. EX y. x = y


112 
1. ALL x. EX y. x = y


113 
val it = [] : thm list


114 
 by (resolve_tac [allI] 1);


115 
Level 1


116 
ALL x. EX y. x = y


117 
1. !!x. EX y. x = y


118 
val it = () : unit


119 
 by (resolve_tac [exI] 1);


120 
Level 2


121 
ALL x. EX y. x = y


122 
1. !!x. x = ?y1(x)


123 
val it = () : unit


124 
 by (resolve_tac [refl] 1);


125 
Level 3


126 
ALL x. EX y. x = y


127 
No subgoals!


128 
val it = () : unit


129 



130 


131 
goal FOL_thy "EX y. ALL x. x=y";


132 
by (resolve_tac [exI] 1);


133 
by (resolve_tac [allI] 1);


134 
by (resolve_tac [refl] 1);


135 


136 
 goal Int_Rule.thy "EX y. ALL x. x=y";


137 
Level 0


138 
EX y. ALL x. x = y


139 
1. EX y. ALL x. x = y


140 
val it = [] : thm list


141 
 by (resolve_tac [exI] 1);


142 
Level 1


143 
EX y. ALL x. x = y


144 
1. ALL x. x = ?y


145 
val it = () : unit


146 
 by (resolve_tac [allI] 1);


147 
Level 2


148 
EX y. ALL x. x = y


149 
1. !!x. x = ?y


150 
val it = () : unit


151 
 by (resolve_tac [refl] 1);


152 
by: tactic returned no results


153 


154 
uncaught exception ERROR


155 


156 


157 


158 
goal FOL_thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";


159 
by (resolve_tac [exI, allI] 1);


160 
by (resolve_tac [exI, allI] 1);


161 
by (resolve_tac [exI, allI] 1);


162 
by (resolve_tac [exI, allI] 1);


163 
by (resolve_tac [exI, allI] 1);


164 


165 
 goal Int_Rule.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";


166 
Level 0


167 
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)


168 
1. EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)


169 
val it = [] : thm list


170 
 by (resolve_tac [exI, allI] 1);


171 
Level 1


172 
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)


173 
1. ALL x. EX v. ALL y. EX w. P(?u,x,v,y,w)


174 
val it = () : unit


175 
 by (resolve_tac [exI, allI] 1);


176 
Level 2


177 
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)


178 
1. !!x. EX v. ALL y. EX w. P(?u,x,v,y,w)


179 
val it = () : unit


180 
 by (resolve_tac [exI, allI] 1);


181 
Level 3


182 
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)


183 
1. !!x. ALL y. EX w. P(?u,x,?v2(x),y,w)


184 
val it = () : unit


185 
 by (resolve_tac [exI, allI] 1);


186 
Level 4


187 
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)


188 
1. !!x y. EX w. P(?u,x,?v2(x),y,w)


189 
val it = () : unit


190 
 by (resolve_tac [exI, allI] 1);


191 
Level 5


192 
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)


193 
1. !!x y. P(?u,x,?v2(x),y,?w4(x,y))


194 
val it = () : unit


195 


196 


197 
goal FOL_thy "(ALL x.P(x) > Q) > (EX x.P(x))>Q";


198 
by (REPEAT (resolve_tac [impI] 1));


199 
by (eresolve_tac [exE] 1);


200 
by (dresolve_tac [spec] 1);


201 
by (eresolve_tac [mp] 1);


202 
by (assume_tac 1);


203 


204 
 goal Int_Rule.thy "(ALL x.P(x) > Q) > (EX x.P(x))>Q";


205 
Level 0


206 
(ALL x. P(x) > Q) > (EX x. P(x)) > Q


207 
1. (ALL x. P(x) > Q) > (EX x. P(x)) > Q


208 
val it = [] : thm list


209 
 by (REPEAT (resolve_tac [impI] 1));


210 
Level 1


211 
(ALL x. P(x) > Q) > (EX x. P(x)) > Q


212 
1. [ ALL x. P(x) > Q; EX x. P(x) ] ==> Q


213 
val it = () : unit


214 
 by (eresolve_tac [exE] 1);


215 
Level 2


216 
(ALL x. P(x) > Q) > (EX x. P(x)) > Q


217 
1. !!x. [ ALL x. P(x) > Q; P(x) ] ==> Q


218 
val it = () : unit


219 
 by (dresolve_tac [spec] 1);


220 
Level 3


221 
(ALL x. P(x) > Q) > (EX x. P(x)) > Q


222 
1. !!x. [ P(x); P(?x3(x)) > Q ] ==> Q


223 
val it = () : unit


224 
 by (eresolve_tac [mp] 1);


225 
Level 4


226 
(ALL x. P(x) > Q) > (EX x. P(x)) > Q


227 
1. !!x. P(x) ==> P(?x3(x))


228 
val it = () : unit


229 
 by (assume_tac 1);


230 
Level 5


231 
(ALL x. P(x) > Q) > (EX x. P(x)) > Q


232 
No subgoals!


233 


234 


235 
goal FOL_thy "((EX x.P(x)) > Q) > (ALL x.P(x)>Q)";


236 
by (REPEAT (resolve_tac [impI] 1));


237 


238 


239 
goal FOL_thy "(EX x.P(x) > Q) > (ALL x.P(x))>Q";


240 
by (REPEAT (resolve_tac [impI] 1));


241 
by (eresolve_tac [exE] 1);


242 
by (eresolve_tac [mp] 1);


243 
by (eresolve_tac [spec] 1);


244 
