13958

1 
(* Title : Integration.thy


2 
Author : Jacques D. Fleuriot


3 
Copyright : 2000 University of Edinburgh


4 
Description : Theory of integration (cf. Harrison's HOL development)


5 
*)


6 


7 
Integration = MacLaurin +


8 


9 


10 
constdefs


11 


12 


13 
(*  *)


14 
(* Partitions and tagged partitions etc. *)


15 
(*  *)


16 


17 
partition :: "[(real*real),nat => real] => bool"


18 
"partition == %(a,b) D. ((D 0 = a) &


19 
(EX N. ((ALL n. n < N > D(n) < D(Suc n)) &


20 
(ALL n. N <= n > (D(n) = b)))))"


21 


22 
psize :: (nat => real) => nat


23 
"psize D == @N. (ALL n. n < N > D(n) < D(Suc n)) &


24 
(ALL n. N <= n > (D(n) = D(N)))"


25 


26 
tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"


27 
"tpart == %(a,b) (D,p). partition(a,b) D &


28 
(ALL n. D(n) <= p(n) & p(n) <= D(Suc n))"


29 


30 
(*  *)


31 
(* Gauges and gaugefine divisions *)


32 
(*  *)


33 


34 
gauge :: [real => bool, real => real] => bool


35 
"gauge E g == ALL x. E x > 0 < g(x)"


36 


37 
fine :: "[real => real, ((nat => real)*(nat => real))] => bool"


38 
"fine == % g (D,p). ALL n. n < (psize D) > D(Suc n)  D(n) < g(p n)"


39 


40 
(*  *)


41 
(* Riemann sum *)


42 
(*  *)


43 


44 
rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"


45 
"rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n)  D(n)))"


46 


47 
(*  *)


48 
(* Gauge integrability (definite) *)


49 
(*  *)


50 


51 
Integral :: "[(real*real),real=>real,real] => bool"


52 
"Integral == %(a,b) f k. ALL e. 0 < e >


53 
(EX g. gauge(%x. a <= x & x <= b) g &


54 
(ALL D p. tpart(a,b) (D,p) & fine(g)(D,p) >


55 
abs(rsum(D,p) f  k) < e))"


56 
end


57 


58 
