doc-src/Intro/quant.txt

adding examples of function predicate replacement and arithmetic examples for the predicate compiler; tuned

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

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


goal Int_Rule.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
by (resolve_tac [impI] 1);
by (dresolve_tac [spec] 1);
by (resolve_tac [allI] 1);
by (dresolve_tac [spec] 1);
by (resolve_tac [allI] 1);
by (assume_tac 1);
choplev 1;
by (resolve_tac [allI] 1);
by (resolve_tac [allI] 1);
by (dresolve_tac [spec] 1);
by (dresolve_tac [spec] 1);
by (assume_tac 1);

choplev 0;
by (REPEAT (assume_tac 1
     ORELSE resolve_tac [impI,allI] 1
     ORELSE dresolve_tac [spec] 1));


- goal Int_Rule.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
Level 0
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
val it = [] : thm list
- by (resolve_tac [impI] 1);
Level 1
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)
val it = () : unit
- by (dresolve_tac [spec] 1);
Level 2
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)
val it = () : unit
- by (resolve_tac [allI] 1);
Level 3
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)
val it = () : unit
- by (dresolve_tac [spec] 1);
Level 4
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)
val it = () : unit
- by (resolve_tac [allI] 1);
Level 5
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. !!z w. P(?x1,?y3(z)) ==> P(w,z)
val it = () : unit
- by (assume_tac 1);
by: tactic returned no results

uncaught exception ERROR
- choplev 1;
Level 1
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)
val it = () : unit
- by (resolve_tac [allI] 1);
Level 2
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)
val it = () : unit
- by (resolve_tac [allI] 1);
Level 3
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. !!z w. ALL x y. P(x,y) ==> P(w,z)
val it = () : unit
- by (dresolve_tac [spec] 1);
Level 4
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)
val it = () : unit
- by (dresolve_tac [spec] 1);
Level 5
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)
val it = () : unit
- by (assume_tac 1);
Level 6
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
No subgoals!

> choplev 0;
Level 0
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
> by (REPEAT (assume_tac 1
#      ORELSE resolve_tac [impI,allI] 1
#      ORELSE dresolve_tac [spec] 1));
Level 1
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
No subgoals!



goal FOL_thy "ALL x. EX y. x=y";
by (resolve_tac [allI] 1);
by (resolve_tac [exI] 1);
by (resolve_tac [refl] 1);

- goal Int_Rule.thy "ALL x. EX y. x=y";
Level 0
ALL x. EX y. x = y
 1. ALL x. EX y. x = y
val it = [] : thm list
- by (resolve_tac [allI] 1);
Level 1
ALL x. EX y. x = y
 1. !!x. EX y. x = y
val it = () : unit
- by (resolve_tac [exI] 1);
Level 2
ALL x. EX y. x = y
 1. !!x. x = ?y1(x)
val it = () : unit
- by (resolve_tac [refl] 1);
Level 3
ALL x. EX y. x = y
No subgoals!
val it = () : unit
-

goal FOL_thy "EX y. ALL x. x=y";
by (resolve_tac [exI] 1);
by (resolve_tac [allI] 1);
by (resolve_tac [refl] 1);

- goal Int_Rule.thy "EX y. ALL x. x=y";
Level 0
EX y. ALL x. x = y
 1. EX y. ALL x. x = y
val it = [] : thm list
- by (resolve_tac [exI] 1);
Level 1
EX y. ALL x. x = y
 1. ALL x. x = ?y
val it = () : unit
- by (resolve_tac [allI] 1);
Level 2
EX y. ALL x. x = y
 1. !!x. x = ?y
val it = () : unit
- by (resolve_tac [refl] 1);
by: tactic returned no results

uncaught exception ERROR



goal FOL_thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);

- goal Int_Rule.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
Level 0
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
 1. EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
val it = [] : thm list
- by (resolve_tac [exI, allI] 1);
Level 1
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
 1. ALL x. EX v. ALL y. EX w. P(?u,x,v,y,w)
val it = () : unit
- by (resolve_tac [exI, allI] 1);
Level 2
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
 1. !!x. EX v. ALL y. EX w. P(?u,x,v,y,w)
val it = () : unit
- by (resolve_tac [exI, allI] 1);
Level 3
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
 1. !!x. ALL y. EX w. P(?u,x,?v2(x),y,w)
val it = () : unit
- by (resolve_tac [exI, allI] 1);
Level 4
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
 1. !!x y. EX w. P(?u,x,?v2(x),y,w)
val it = () : unit
- by (resolve_tac [exI, allI] 1);
Level 5
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
 1. !!x y. P(?u,x,?v2(x),y,?w4(x,y))
val it = () : unit


goal FOL_thy "(ALL x.P(x) --> Q) --> (EX x.P(x))-->Q";
by (REPEAT (resolve_tac [impI] 1));
by (eresolve_tac [exE] 1);
by (dresolve_tac [spec] 1);
by (eresolve_tac [mp] 1);
by (assume_tac 1);

- goal Int_Rule.thy "(ALL x.P(x) --> Q) --> (EX x.P(x))-->Q";
Level 0
(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
 1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
val it = [] : thm list
- by (REPEAT (resolve_tac [impI] 1));
Level 1
(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
 1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q
val it = () : unit
- by (eresolve_tac [exE] 1);
Level 2
(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
 1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q
val it = () : unit
- by (dresolve_tac [spec] 1);
Level 3
(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
 1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q
val it = () : unit
- by (eresolve_tac [mp] 1);
Level 4
(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
 1. !!x. P(x) ==> P(?x3(x))
val it = () : unit
- by (assume_tac 1);
Level 5
(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
No subgoals!


goal FOL_thy "((EX x.P(x)) --> Q) --> (ALL x.P(x)-->Q)";
by (REPEAT (resolve_tac [impI] 1));


goal FOL_thy "(EX x.P(x) --> Q) --> (ALL x.P(x))-->Q";
by (REPEAT (resolve_tac [impI] 1));
by (eresolve_tac [exE] 1);
by (eresolve_tac [mp] 1);
by (eresolve_tac [spec] 1);