doc-src/Intro/quant.txt

Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.

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