# The Gauge Integral Theory in HOL4

Authors: Zhiping Shi; Weiqing Gu; Xiaojuan Li; Yong Guan; Shiwei Ye; Jie Zhang; Hongxing Wei
Journal: Journal of Applied Mathematics
 (2013)

---

## Abstract

The integral is one of the most important foundations for modeling dynamical systems. The gauge integral is a generalization of the Riemann integral and the Lebesgue integral and applies to a much wider class of functions. In this paper, we formalize the operational properties which contain the linearity, monotonicity, integration by parts, the Cauchy-type integrability criterion, and other important theorems of the gauge integral in higher-order logic 4 (HOL4) and then use them to verify an inverting integrator. The formalized theorem library has been accepted by the HOL4 authority and will appear in HOL4 Kananaskis-9.


---

## Body

## 1. Introduction

In the recent years, hardware and software systems are widely used in safety critical applications like car, highway and air control systems, medical instruments, and so on. The cost of a failure in these systems is unacceptably high, thus making it important to make sure of the correctness of the functions in design. The traditional verification methods, which include simulation and testing, are not sufficient to validate confidence. Formal methods can be helpful in proving the correctness of systems. Theorem proving is one method for performing verification on formal specifications of system models [1]. It allows to mathematically reason about system properties by representing the behavior of a system in logic in a general model. In this way, the specification and implementation are expressed as the general mathematical model so that all the cases are covered when they are proved to be equivalent.The integral is a mathematical tool to solve many practical problems in geometry, physics, economics, electrical systems, and so on. In order to formalize dynamic systems, some theorem provers have already formalized integral theorem library. The Isabelle/Isar theorem prover has the formalization of the Lebesgue integral [2], and the Isabelle/HOL has the formalization of the gauge Integral [3]. Cruz-Filipe reported a constructive theory of real analysis [4], which includes continuous functions and differential, integral, and transcendental functions in the COQ theorem prover. The PVS theorem prover has the Riemann integral formalized by Butler [5]. Mhamdi et al. [6] formalized the Lebesgue integration in HOL4 in order to formalize statistical properties of continuous random variables. Harrison formalized the gauge integral in HOL light [7]. Although there are the definition of the gauge integral and the fundamental theorem of calculus in HOL4 [7], there are no operation property and other theorems yet.This paper presents the formalization of the complete gauge integral theory in HOL4 [8], including linearity, inequality, integration by parts, and the Cauchy-type integrability criterion, as well as the formal analysis of an integral circuit based on the formalization. The properties of vectors and matrices are characterized in accordance with linear space properties. In this paper, we use HOL4 notations, and some notations are listed in Table 1.Table 1
Some HOL4 notations and their semantics.
Meaning
HOL notations
Standard notations
Truth
T
T
Falsity
F
⊥
Negation
~t
¬t
Disjunction
t
1
∨
t
2
t
1
∨
t
2
Conjunction
t1∧t2
t
1
∧
t
2
Implication
t1==>t2
t
1
⇒
t
2
Equality
t1=t2
t
1
=
t
2
∀-quantification
!x · t
∀
x
·
t
∃-quantification
?x · t
∃
x
·
t
Lambda
∖
x · t
λ
x
·
tThe rest of the paper is organized as follows. In Section2, we give an overview of the gauge integral and present the formalization of the properties and theorems in HOL4. In Section 3, the formal analysis of an integral circuit is presented. Section 4 concludes the paper. The definitions and theorems in this paper are described as formalizations in HOL4 and have been verified for correctness using the HOL4 theorem prover.


## 2. The Gauge Integral in HOL4

There are many ways of formally defining an integral, not all of which are equivalent. The differences exist mostly to deal with differing special cases which may not be integrable under other definitions. The definitions include the Newton integral, the Riemann integral, the Lebesgue integral, and the gauge integral, which had been proposed in different senses. The gauge integral proposed by Kurzweil and Henstock is a generalization of the Riemann integral and the Lebesgue integral, and it is suitable for wider situations [8]. The gauge integral is far simpler than the Lebesgue integral—it is not to be preceded by explanations of sigma-algebras and measures [9] but to be based on the special properties of the closed interval [8]. Harrison made a detailed analysis of advantages of the gauge integral [7].For any functionf, which may be not a derivative, we say that it has the gauge integral I on the interval [a,b] if for any ε>0, there is a gauge δ such that for any δ-fine division, the usual Riemann-type sum approaches I are closer than ε:
(1)|∑i=0nf(ti)(xi+1-xi)-I|<ε.So, the above reasoning shows that a derivativef′ always has the gauge integral f(b)-f(a) over the interval [a,b]; that is, the fundamental theorem of calculus holds.Definition 1 (the gauge integral).
Letf:[a,b]→R be some function, and let V be some number. We say that V is the gauge integral of f, written V=∫abf(t)dt, if for each number ε>0, there exists a corresponding function δ:[a,b]→(0,+∞) with the following property: whenever n is a positive integer and t0,t1,t2,…,tn and s1,s2,…,sn are some numbers satisfying a=t0≤s1≤t1≤s2≤t2≤⋯≤tn-1≤sn≤tn=b and ti-ti-1<δ(si) for all i, then |V-∑i=1nf(si)(ti-ti-1)|<ε.
Definition1 is formalized in HOL4 as [7]|-
!a b f k.Dint(a,b)fk<=>!e. 0<e ==>?g. gauge (∖x.a<=x∧x<=b)g∧!D p. tdiv (a,b) (D,p)∧ fine g(D,p) ==>abs(rsum(D,p)f-k)<e,
where division(a,b) D denotes a division D on interval [a,b]:division(a,b) D<=>(D0=a)∧?N.(!n.n<N==>Dn<D(SUCn))∧!n.n>=N==>(Dn=b).tdiv (a,b)(D,p) denotes to get any value between two contiguous dividing points:tdiv(a,b)(D,p) <=> division (a,b)D∧!n.Dn<=pn∧pn<=D(SUCn).The gauge Eg indicates that g is a measure over a set E (an interval commonly), formally as|-!Eg. gauge Eg<=>!x.Ex==>0<gx,and fine means as follows:|-!gDp. fine g(D,p)<=>!n.n<dsizeD==>D(SUCn)-Dn<g(pn).dsize D denotes the number of divisions of the interval divided by the division D:dsizeD=@N.!n.n<N==>Dn<D(SUCn))∧!n.n>=N==>(Dn=DN).
In sum, “Dint(a,b)fk” denotes the integral of f on [a,b] is k.  Then, we give the definitions of integrable and integral based on Definition 1.Definition 2 (integrable).
Functionf is integrable on interval [a,b] means that there exist a number i that satisfy Definition 1.
Definition2 is formalized in HOL4 as
integrable=|-!abf. integrable (a,b)f<=>?i. Dint (a,b)fi.Definition 3 (integral value).
A function’s integral value is formalized as follows:
integral=|-!abf. integral (a,b)f=@i. Dint (a,b)fi.
The relations between the definitions are described in Theorems4 and 5.Theorem 4 (INTEGRABLE_DINT).
One has
|
-
!
f
a
b. integrable (a,b)f==>Dint  (a,b)f (integral (a,b)f).Theorem 5 (DINT_INTEGRAL).
Consider
|
-
!
f
a
b
i. a<=b∧ Dint  (a,b)fi==> (integral (a,b)f=i).Then, we formalizes the operational properties of the gauge integral [8].


### 2.1. Linearity of the Gauge Integral

In this subsection, the formalizations of the linear properties are presented after the respective mathematical expressions.Theorem 6 (DINT_CONST).
The integral of a constant function is computed by:(2)∫abcdx=c*(b-a).The formalization is as follows:(3)|-!abc.Dint(a,b)(∖x.c)(c*(b-a)).Theorem 7 (DINT_0).
The integral of zero is zero:(4)∫ab0dx=0.The formalization is as follows:(5)|-!ab.Dint(a,b)(∖x.0)0.Theorem 8 (DINT_NEG).
The integral is negated when the function is negated:(6)∫abf(x)dx=i⟹∫ab(-f(x))dx=-i.The formalization is as follows:(7)|-!fabi.Dint(a,b)fi==>Dint(a,b)(∖x.-fx)(-i).Theorem 9 (DINT_CMUL).
The integral of the product of a function multiplied by a constant equals the product of the constant and the integral of the function:(8)∫abf(x)dx=i⟹∫abc*f(x)dx=c*i.The formalization is as follows:(9)|-!fabci.Dint(a,b)fi==>Dint(a,b)(∖x.c*fx)(c*i).Theorem 10 (DINT_ADD).
The integral of the sum of two functions is the sum of the integrals of the two functions:(10)∫abf(x)dx=i∧∫abg(x)dx=j⟹∫ab(f(x)+g(x))dx=i+j.The formalization is as follows:(11)|-!fgabij.Dint(a,b)fi∧Dint(a,b)gj==>Dint(a,b)(∖x.fx+gx)(i+j).Theorem 11 (DINT_SUB).
The integral of the difference of two functions is the difference of the integrals of the two functions:(12)∫abf(x)dx=i∧∫abg(x)dx=j⟹∫ab(f(x)-g(x))dx=i-j.The formalization is as follows:(13)|-!fgabij.Dint(a,b)fi∧Dint(a,b)gj==>Dint(a,b)(∖x.fx-gx)(i-j).Theorem 12 (DINT_LINEAR).
The integral is linear:(14)∫abf(x)dx=i∧∫abg(x)dx=j⟹∫ab(m*f(x)+n*g(x))dx=m*i+n*j.The formalization is as follows:(15)|-!fgabij.Dint(a,b)fi∧Dint(a,b)gj==>Dint(a,b)(∖x.m*fx+n*gx)(m*i+n*j).These theorems are proven based on the definition of the gauge integral.


### 2.2. Inequalities of the Gauge Integral

The three inequalities are formalized in this subsection.Theorem 13 (upper and lower bounds).
An integrable functionfover [a,b] is necessarily bounded on that interval. Thus, there are real numbers m and M so that m≤f(x)≤M for all x in [a,b]. Since the lower and upper sums of f over [a,b] are therefore bounded by, respectively, m(b-a) and M(b-a), it follows that
(16)m(b-a)≤∫abf(x)dx≤M(b-a).The formalization is as follows:INTEGRAL_MVT_LE:|-!fab.a<b∧ (!x. a<=x∧x<=b==>fcontlx)∧(!x. a<=x∧x<=b==>m<=fx:fx<=M)==>m*(b-a)<= integral (a,b)f∧  integral (a,b)f<=M*(b-a).Theorem 14 (inequalities between functions).
Iff(x)≤g(x)  for each x in [a,b], then each of the upper and lower sums of f is bounded above by the upper and lower sums of g, respectively:
(17)∫abf(x)dx≤∫abg(x)dx.The formalization is as follows:INTEGRAL_LE:|-!fgabij.a<=b∧  integrable (a,b)f∧  integrable (a,b)g∧(!x. a<=x∧x<=b==>fx<=gx)==>integral(a,b)f<= integral (a,b)g.DINT_LE:|-!fgabij. a<=b∧Dint(a,b)fi∧ Dint(a,b)gj∧(!x. a<=x∧x<=b==>f(x)<=g(x))==>i<=j.Theorem 15 (inequality of absolute value).
Iff is the gauge-integrable on [a,b], then the same is true for |f| and
(18)|∫abf(x)dx|≤∫ab|f(x)|dx.The formalization is as follows:DINT_TRIANGLE:|-!fabij.a<=b∧ Dint(a,b)fi∧ Dint(a,b)(∖x. abs(fx))j==>absi<=j.This theorem could be proved by Theorem14.


### 2.3. The Integral of the Pointwise Perturbation and the Spike Functions

Theorem 16 (DINT_DELTA).
The integral of the delta function, which equals 1 only at one certain point otherwise keeps zero, is zero:(19)f(x)={1x=c0else⟹∫abf(x)dx=0.The formalization is as follows:|
-!abc. Dint  (a,b) (∖x. if x=c then 1 else 0) 0.Theorem 17 (DINT_POINT_SPIKE).
The two functions which are equal except at a certain point have same integrals:(20)∀x∈[a,b]∧x≠c⟹(f(x)=g(x))∧∫abf(x)dx=i⟹∫abg(x)dx=i.The formalization is as follows:|-!fgabci.(!x. a<= x∧x<= b∧x<>c ==>(fx=gx))∧Dint(a,b)fi ==> Dint(a,b)gi.This shows that if one changes a function at one point, then its integral does not change.


### 2.4. Other Important Properties

Theorem 18 (integrable on subinterval).
For allcd.a≤c∧c≤d∧d≤b, if f is integrable over [a,b], then f is integrable over [c,d].The formalization is as follows:INTEGRABLE_SUBINTERVAL:|-!fabcd. a<=c∧c<=d∧d<=b∧ integrable (a,b)  f==> integrable (c,d)f.In order to prove Theorem18, the following three lemmas need to be proved:INTEGRABLE_SPLIT_SIDES=|- ! fabc.a<=c∧c<=b∧ integrable (a,b)f==>?i. ! e. 0<e==>?g. gauge (∖x. a<=x∧x<=b)g∧!d1 p1 d2 p2.tdiv(a,c) (d1,p1) ∧ fine g(d1,p1)∧tdiv(c,b) (d2,p2) ∧ fine g(d2,p2)==>abs (rsum(d1,p1)f+rsum (d2,p2)f-i)<eINTEGRABLE_SUBINTERVAL_LEFT =|- ! fabc. a<=c∧c<=b∧ integrable (a,b)f==> integrable (a,c)fINTEGRABLE_SUBINTERVAL_RIGHT =|- ! fabc. a<=c∧c<=b∧integrable  (a,b)f==>integrable  (c,b)f.The INTEGRABLE_SPLIT_SIDES is used to prove INTEGRABLE_SUBINTERVAL_LEFT and INTEGRABLE_SUBINTERVAL_RIGHT, then the theorem INTEGRABLE_SUBINTERVAL can be proved by the transitivity of real number.Theorem 19 (additivity of integration on intervals).
Ifb is any element of [a,c], then
(21)∫abf(x)dx+∫bcf(x)dx=∫acf(x)dx.The formalization is as follows:INTEGRAL_COMBINE:|- !fabc.a<=b∧b<=c∧integrable(a,c)f==>(integral(a,c)f=integral(a,b)f+integral(b,c)f).The proof of Theorem19 is sophisticated. We utilize multiple lemmas shown in Table 2.Table 2
The lemmas proving Theorem19.
Name of lemma
Description in HOL4
DIVISION_LE_SUC
∀ dab. division (a, b) d ==> ∀n. d n <= d (SUC n)
DIVISION_MONO_LE
∀
d
a
b. division (a, b) d ==> ∀m n. m <= n ==> d m <= d n
DIVISION_MONO_LE_SUC
∀
d
a
b. division (a, b) d ==> ∀n. d n <= d (SUC n)
DIVISION_INTERMEDIATE
∀ dabc. division (a, b) d∧a <= c∧c <= b ==> ∃ n. n <= dsize d∧d n <= c∧c <= d (SUC n)
DIVISION_DSIZE_LE
∀ abdn. division (a, b) d∧ (d (SUC n) = d n) ==> dsize d <= n
DIVISION_DSIZE_GE
∀ abdn. division (a, b) d∧d n < d (SUC n) ==> SUC n <= dsize d
DIVISION_DSIZE_EQ
∀ abdn. division (a, b) d∧d n < d (SUC n) ∧ (d (SUC (SUC n)) = d (SUC n)) ==>  (dsize d = SUC n)
DIVISION_DSIZE_EQ_ALT
∀ abdn. division (a, b) d∧ (d (SUC n) = d n) ∧  (∀i. i < n ==> d i < d (SUC i)) ==> (dsize d = n)The proof is branched based ona<=b∧b<=c. It is easy in case of a=b or b=c. In case  a<b∧b<c, b is the tie point of two measure intervals. It needs the lemmas of Table 1 to prove interval measure and division fine. The proof program consists of over 400 lines of HOL4 code. The proof procedure is described as follows.In casea<b∧b<c, the proof goal is extended as follows:
(22)abs(sum(0,dsized)(∖n.f(pn)*(d(SUCn)-dn))-(i+j))<e.The proof goal transfers by using the fourth lemma:(23)abs(sum(0,m+n)(∖n.f(pn)*(d(SUCn)-dn))-(i+j))<e.This lemma is proven with two cases based onn=0 or n≠0. In case of n≠0, the goal is
(24)abs(sum(0,m)(∖n.f(pn)*(d(SUCn)-dn))+(f(pm)*(d(SUCm)-dm)+sum(m+1,PREn)×(∖n.f(pn)*(d(SUCn)-dn)))-(i+j))<e.The goal is rewritten bypm=b:
(25)abs(sum(0,m)(∖n.f(pn)*(d(SUCn)-dn))+(fb*(d(SUCm)-dm)+sum(m+1,PREn)×(∖n.f(pn)*(d(SUCn)-dn)))-(i+j))<e.Lets1 denote sum (0,m)(∖n.f(pn)*(d(SUCn)-dn)), and let s2 denote sum (m+1,PREn)(∖n.f(pn)*(d(SUCn)-dn)); the simplized goal is as follows:
(26)abs(s1+fb*(b-dm)-i)<e2∧abs(s2+fb*(d(SUCm)-b)-j)<e2.For abs(s1+fb*(b-dm)-i)<e/2, we prove it based on dm=b and dm≠b. Similarly, for abs (s2+fb*(d(SUCm)-b)-j)<e/2, we prove it based on the cases d(SUCm)=b or d(SUCm)≠b, then the goal is proved.Theorem 20 (the Cauchy-type integrability criterion).
Letf:[a,b]→ℝ. Then, f is integrable over [a,b] if and only if for every ε>0, there is a gauge γ on [a,b] such that if D1,D2≪γ, then |S(f,D1)-S(f,D2)|<ε, where S(f,D) is a Riemann sum, and D1, D2 are partitions of [a,b].The formalization is as follows:INTEGRABLE_CAUCHY:|- !fab.integrable(a,b)f<=>!e. 0<e==>?g. gauge (∖x. a<=x∧x<=b) g∧!d1p1d2p2.tdiv(a,b)(d1,p1)∧ fine g(d1,p1)∧tdiv(a,b)(d2,p2)∧ fine g(d2,p2)==>abs (rsum(d1,p1)f-rsum(d2,p2)f)<e.The Cauchy criterion indicates that an integrable function is always convergent for any division on the interval.First of all, we should prove that a function for any gauge over the set isδ-fine; we formalized the lemma as GAUGE_MIN_FINITE:|- !sgsm.(!m. m<=n==> gauge s(gsm))==>?g.gaugesg∧!dp. fine (d,p)==> !m. m<=n==> fine (gsm) (d,p).Theorem 21 (limit theorem).
Letf:[a,b]→ℝ and assume that for every ε>0, there exists an integrable function g:[a,b]→ℝ such that |f-g|≤ε on [a,b]. Then, f is integrable over [a,b].The formalization is as follows:INTEGRABLE_LIMIT:|-!fab.(!e. 0<e==>?g. (!x. a<=x∧x<=b==>abs(fx-gx)<=e)∧integrable(a,b)g)==>integrable(a,b)f.In order to make the proof easier, we proved the RSUM_DIFF_BOUND at first:|-!abdpefg.tdiv(a,b)(d,p)∧(!x. a<=x∧x<=b==>abs(fx-gx)<=e)==>abs(rsum(d,p)f-rsum(d,p)g)<=e*(b-a).Theorem 22 (integrability of continuous functions).
Iff:[a,b]→ℝ is continuous, then f is integrable over [a,b].The formalization is as follows:INTEGRABLE_CONTINUOUS:|-!fab. (!x. a<=x∧x<=b==>fcontlx) ==> integrable (a,b)f.To prove Theorem22, we first prove the uniform continuity theorem.Iff:[a,b]→ℝ is continuous, f is uniformly continuous. And then, the result is given by that the uniformly continuous functions are integrable. The uniform continuity theorem is formalized as follows:CONT_UNIFORM:|-!fab.a<=b∧ (!x. a<=x∧x<=b==>fcontlx)==>!e. 0<e==>?d. 0<d∧!xy. a<=x∧x<=b∧a<=y∧y<=b∧abs(x-y)<d==>abs(fx-fy)<e.


## 2.1. Linearity of the Gauge Integral

In this subsection, the formalizations of the linear properties are presented after the respective mathematical expressions.Theorem 6 (DINT_CONST).
The integral of a constant function is computed by:(2)∫abcdx=c*(b-a).The formalization is as follows:(3)|-!abc.Dint(a,b)(∖x.c)(c*(b-a)).Theorem 7 (DINT_0).
The integral of zero is zero:(4)∫ab0dx=0.The formalization is as follows:(5)|-!ab.Dint(a,b)(∖x.0)0.Theorem 8 (DINT_NEG).
The integral is negated when the function is negated:(6)∫abf(x)dx=i⟹∫ab(-f(x))dx=-i.The formalization is as follows:(7)|-!fabi.Dint(a,b)fi==>Dint(a,b)(∖x.-fx)(-i).Theorem 9 (DINT_CMUL).
The integral of the product of a function multiplied by a constant equals the product of the constant and the integral of the function:(8)∫abf(x)dx=i⟹∫abc*f(x)dx=c*i.The formalization is as follows:(9)|-!fabci.Dint(a,b)fi==>Dint(a,b)(∖x.c*fx)(c*i).Theorem 10 (DINT_ADD).
The integral of the sum of two functions is the sum of the integrals of the two functions:(10)∫abf(x)dx=i∧∫abg(x)dx=j⟹∫ab(f(x)+g(x))dx=i+j.The formalization is as follows:(11)|-!fgabij.Dint(a,b)fi∧Dint(a,b)gj==>Dint(a,b)(∖x.fx+gx)(i+j).Theorem 11 (DINT_SUB).
The integral of the difference of two functions is the difference of the integrals of the two functions:(12)∫abf(x)dx=i∧∫abg(x)dx=j⟹∫ab(f(x)-g(x))dx=i-j.The formalization is as follows:(13)|-!fgabij.Dint(a,b)fi∧Dint(a,b)gj==>Dint(a,b)(∖x.fx-gx)(i-j).Theorem 12 (DINT_LINEAR).
The integral is linear:(14)∫abf(x)dx=i∧∫abg(x)dx=j⟹∫ab(m*f(x)+n*g(x))dx=m*i+n*j.The formalization is as follows:(15)|-!fgabij.Dint(a,b)fi∧Dint(a,b)gj==>Dint(a,b)(∖x.m*fx+n*gx)(m*i+n*j).These theorems are proven based on the definition of the gauge integral.


## 2.2. Inequalities of the Gauge Integral

The three inequalities are formalized in this subsection.Theorem 13 (upper and lower bounds).
An integrable functionfover [a,b] is necessarily bounded on that interval. Thus, there are real numbers m and M so that m≤f(x)≤M for all x in [a,b]. Since the lower and upper sums of f over [a,b] are therefore bounded by, respectively, m(b-a) and M(b-a), it follows that
(16)m(b-a)≤∫abf(x)dx≤M(b-a).The formalization is as follows:INTEGRAL_MVT_LE:|-!fab.a<b∧ (!x. a<=x∧x<=b==>fcontlx)∧(!x. a<=x∧x<=b==>m<=fx:fx<=M)==>m*(b-a)<= integral (a,b)f∧  integral (a,b)f<=M*(b-a).Theorem 14 (inequalities between functions).
Iff(x)≤g(x)  for each x in [a,b], then each of the upper and lower sums of f is bounded above by the upper and lower sums of g, respectively:
(17)∫abf(x)dx≤∫abg(x)dx.The formalization is as follows:INTEGRAL_LE:|-!fgabij.a<=b∧  integrable (a,b)f∧  integrable (a,b)g∧(!x. a<=x∧x<=b==>fx<=gx)==>integral(a,b)f<= integral (a,b)g.DINT_LE:|-!fgabij. a<=b∧Dint(a,b)fi∧ Dint(a,b)gj∧(!x. a<=x∧x<=b==>f(x)<=g(x))==>i<=j.Theorem 15 (inequality of absolute value).
Iff is the gauge-integrable on [a,b], then the same is true for |f| and
(18)|∫abf(x)dx|≤∫ab|f(x)|dx.The formalization is as follows:DINT_TRIANGLE:|-!fabij.a<=b∧ Dint(a,b)fi∧ Dint(a,b)(∖x. abs(fx))j==>absi<=j.This theorem could be proved by Theorem14.


## 2.3. The Integral of the Pointwise Perturbation and the Spike Functions

Theorem 16 (DINT_DELTA).
The integral of the delta function, which equals 1 only at one certain point otherwise keeps zero, is zero:(19)f(x)={1x=c0else⟹∫abf(x)dx=0.The formalization is as follows:|
-!abc. Dint  (a,b) (∖x. if x=c then 1 else 0) 0.Theorem 17 (DINT_POINT_SPIKE).
The two functions which are equal except at a certain point have same integrals:(20)∀x∈[a,b]∧x≠c⟹(f(x)=g(x))∧∫abf(x)dx=i⟹∫abg(x)dx=i.The formalization is as follows:|-!fgabci.(!x. a<= x∧x<= b∧x<>c ==>(fx=gx))∧Dint(a,b)fi ==> Dint(a,b)gi.This shows that if one changes a function at one point, then its integral does not change.


## 2.4. Other Important Properties

Theorem 18 (integrable on subinterval).
For allcd.a≤c∧c≤d∧d≤b, if f is integrable over [a,b], then f is integrable over [c,d].The formalization is as follows:INTEGRABLE_SUBINTERVAL:|-!fabcd. a<=c∧c<=d∧d<=b∧ integrable (a,b)  f==> integrable (c,d)f.In order to prove Theorem18, the following three lemmas need to be proved:INTEGRABLE_SPLIT_SIDES=|- ! fabc.a<=c∧c<=b∧ integrable (a,b)f==>?i. ! e. 0<e==>?g. gauge (∖x. a<=x∧x<=b)g∧!d1 p1 d2 p2.tdiv(a,c) (d1,p1) ∧ fine g(d1,p1)∧tdiv(c,b) (d2,p2) ∧ fine g(d2,p2)==>abs (rsum(d1,p1)f+rsum (d2,p2)f-i)<eINTEGRABLE_SUBINTERVAL_LEFT =|- ! fabc. a<=c∧c<=b∧ integrable (a,b)f==> integrable (a,c)fINTEGRABLE_SUBINTERVAL_RIGHT =|- ! fabc. a<=c∧c<=b∧integrable  (a,b)f==>integrable  (c,b)f.The INTEGRABLE_SPLIT_SIDES is used to prove INTEGRABLE_SUBINTERVAL_LEFT and INTEGRABLE_SUBINTERVAL_RIGHT, then the theorem INTEGRABLE_SUBINTERVAL can be proved by the transitivity of real number.Theorem 19 (additivity of integration on intervals).
Ifb is any element of [a,c], then
(21)∫abf(x)dx+∫bcf(x)dx=∫acf(x)dx.The formalization is as follows:INTEGRAL_COMBINE:|- !fabc.a<=b∧b<=c∧integrable(a,c)f==>(integral(a,c)f=integral(a,b)f+integral(b,c)f).The proof of Theorem19 is sophisticated. We utilize multiple lemmas shown in Table 2.Table 2
The lemmas proving Theorem19.
Name of lemma
Description in HOL4
DIVISION_LE_SUC
∀ dab. division (a, b) d ==> ∀n. d n <= d (SUC n)
DIVISION_MONO_LE
∀
d
a
b. division (a, b) d ==> ∀m n. m <= n ==> d m <= d n
DIVISION_MONO_LE_SUC
∀
d
a
b. division (a, b) d ==> ∀n. d n <= d (SUC n)
DIVISION_INTERMEDIATE
∀ dabc. division (a, b) d∧a <= c∧c <= b ==> ∃ n. n <= dsize d∧d n <= c∧c <= d (SUC n)
DIVISION_DSIZE_LE
∀ abdn. division (a, b) d∧ (d (SUC n) = d n) ==> dsize d <= n
DIVISION_DSIZE_GE
∀ abdn. division (a, b) d∧d n < d (SUC n) ==> SUC n <= dsize d
DIVISION_DSIZE_EQ
∀ abdn. division (a, b) d∧d n < d (SUC n) ∧ (d (SUC (SUC n)) = d (SUC n)) ==>  (dsize d = SUC n)
DIVISION_DSIZE_EQ_ALT
∀ abdn. division (a, b) d∧ (d (SUC n) = d n) ∧  (∀i. i < n ==> d i < d (SUC i)) ==> (dsize d = n)The proof is branched based ona<=b∧b<=c. It is easy in case of a=b or b=c. In case  a<b∧b<c, b is the tie point of two measure intervals. It needs the lemmas of Table 1 to prove interval measure and division fine. The proof program consists of over 400 lines of HOL4 code. The proof procedure is described as follows.In casea<b∧b<c, the proof goal is extended as follows:
(22)abs(sum(0,dsized)(∖n.f(pn)*(d(SUCn)-dn))-(i+j))<e.The proof goal transfers by using the fourth lemma:(23)abs(sum(0,m+n)(∖n.f(pn)*(d(SUCn)-dn))-(i+j))<e.This lemma is proven with two cases based onn=0 or n≠0. In case of n≠0, the goal is
(24)abs(sum(0,m)(∖n.f(pn)*(d(SUCn)-dn))+(f(pm)*(d(SUCm)-dm)+sum(m+1,PREn)×(∖n.f(pn)*(d(SUCn)-dn)))-(i+j))<e.The goal is rewritten bypm=b:
(25)abs(sum(0,m)(∖n.f(pn)*(d(SUCn)-dn))+(fb*(d(SUCm)-dm)+sum(m+1,PREn)×(∖n.f(pn)*(d(SUCn)-dn)))-(i+j))<e.Lets1 denote sum (0,m)(∖n.f(pn)*(d(SUCn)-dn)), and let s2 denote sum (m+1,PREn)(∖n.f(pn)*(d(SUCn)-dn)); the simplized goal is as follows:
(26)abs(s1+fb*(b-dm)-i)<e2∧abs(s2+fb*(d(SUCm)-b)-j)<e2.For abs(s1+fb*(b-dm)-i)<e/2, we prove it based on dm=b and dm≠b. Similarly, for abs (s2+fb*(d(SUCm)-b)-j)<e/2, we prove it based on the cases d(SUCm)=b or d(SUCm)≠b, then the goal is proved.Theorem 20 (the Cauchy-type integrability criterion).
Letf:[a,b]→ℝ. Then, f is integrable over [a,b] if and only if for every ε>0, there is a gauge γ on [a,b] such that if D1,D2≪γ, then |S(f,D1)-S(f,D2)|<ε, where S(f,D) is a Riemann sum, and D1, D2 are partitions of [a,b].The formalization is as follows:INTEGRABLE_CAUCHY:|- !fab.integrable(a,b)f<=>!e. 0<e==>?g. gauge (∖x. a<=x∧x<=b) g∧!d1p1d2p2.tdiv(a,b)(d1,p1)∧ fine g(d1,p1)∧tdiv(a,b)(d2,p2)∧ fine g(d2,p2)==>abs (rsum(d1,p1)f-rsum(d2,p2)f)<e.The Cauchy criterion indicates that an integrable function is always convergent for any division on the interval.First of all, we should prove that a function for any gauge over the set isδ-fine; we formalized the lemma as GAUGE_MIN_FINITE:|- !sgsm.(!m. m<=n==> gauge s(gsm))==>?g.gaugesg∧!dp. fine (d,p)==> !m. m<=n==> fine (gsm) (d,p).Theorem 21 (limit theorem).
Letf:[a,b]→ℝ and assume that for every ε>0, there exists an integrable function g:[a,b]→ℝ such that |f-g|≤ε on [a,b]. Then, f is integrable over [a,b].The formalization is as follows:INTEGRABLE_LIMIT:|-!fab.(!e. 0<e==>?g. (!x. a<=x∧x<=b==>abs(fx-gx)<=e)∧integrable(a,b)g)==>integrable(a,b)f.In order to make the proof easier, we proved the RSUM_DIFF_BOUND at first:|-!abdpefg.tdiv(a,b)(d,p)∧(!x. a<=x∧x<=b==>abs(fx-gx)<=e)==>abs(rsum(d,p)f-rsum(d,p)g)<=e*(b-a).Theorem 22 (integrability of continuous functions).
Iff:[a,b]→ℝ is continuous, then f is integrable over [a,b].The formalization is as follows:INTEGRABLE_CONTINUOUS:|-!fab. (!x. a<=x∧x<=b==>fcontlx) ==> integrable (a,b)f.To prove Theorem22, we first prove the uniform continuity theorem.Iff:[a,b]→ℝ is continuous, f is uniformly continuous. And then, the result is given by that the uniformly continuous functions are integrable. The uniform continuity theorem is formalized as follows:CONT_UNIFORM:|-!fab.a<=b∧ (!x. a<=x∧x<=b==>fcontlx)==>!e. 0<e==>?d. 0<d∧!xy. a<=x∧x<=b∧a<=y∧y<=b∧abs(x-y)<d==>abs(fx-fy)<e.


## 3. Verifying a Summing Inverting Integrator

In order to illustrate the usefulness of the proposed approach, we use our formalization to analyze a summing integrator. Integration circuits are widely used in electronic circuits; they are often used for waveform transformation, amplifier offset voltage elimination, integral compensation in feedback control, and so on. In this section, we use the formalization above to verify a summing inverting integrator. Figure1 shows the basic summing  inverting integral circuit.Figure 1
The summing inverting circuit.The relation between output and input voltage can be present as the following formula:(27)vo(x)=-1C∫0x[vi1(t)R1+vi2(t)R2]dt.We assumed the integral constant-1/R1C=m, -1/R2C=n, then formula 1 can be simplified as the following formula:
(28)v0(x)=∫0x(m*vi1(t)+n*vi2(t))dt.WhenVi1(t)=cost, Vi2(t)=sint, we can get
(29)Vo(x)=∫0x(m*cost+n*sint)dt=m*sinx+n*(cos0-cosx).Formula (29) can be formalized in HOL4 as follows:SUMMING_INTEGRATOR:|-!x. 0<=x==>(integral(0,x)(∖t.(m*cost)+(n*sint))=m*sinx+n*(cos0-cosx)).The detailed formalization and proof are shown in Algorithm1.Algorithm 1:The formalization and proof of SUMMING_INTEGRATOR.
val SUMMING_INTEGRATOR = store_thm(“SUMMING_INTEGRATOR”,
“!x. 0<=x ==> (integral(0, x) (∖t. (m * cos t) + (n * sin t)) = m * sin x + n *(cos 0 − cos x))”,
RW_TAC std_ss[] THEN REWRITE_TAC[integral] THEN
SELECT_ELIM_TAC THEN CONJ_TAC THENL
[EXISTS_TAC“m * sin x + n * (cos 0 − cos x)” THEN
MATCH_MP_TAC DINT_LINEAR THEN CONJ_TAC THENL
[SUBGOAL_THEN“sin x = sin x − sin 0”ASSUME_TAC THENL
[SIMP_TAC std_ss[SIN_0] THEN REAL_ARITH_TAC, ONCE_ASM_REWRITE_TAC[]] THEN
MATCH_MP_TAC FTC1 THEN RW_TAC std_ss[] THEN
ASM_SIMP_TAC arith_ss[DIFF_SIN], ALL_TAC] THEN
SUBGOAL_THEN“cos 0 − cos x = −cos x − cos 0”ASSUME_TAC THENL
[REWRITE_TAC[REAL_SUB_NEG2], ALL_TAC] THEN
ONCE_ASM_REWRITE_TAC[] THEN HO_MATCH_MP_TAC FTC1 THEN
ASM_SIMP_TAC std_ss[DIFF_NEG_COS],ALL_TAC] THEN
RW_TAC std_ss[] THEN MATCH_MP_TAC DINT_UNIQ THEN
MAP_EVERY EXISTS_TAC[“0:real”,“x:real”,
“(∖t. (m * cos t) + (n * sin t)):real->real”] THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC DINT_LINEAR THEN
CONJ_TAC THENL
[SUBGOAL_THEN “sin x = sin x − sin 0”ASSUME_TAC THENL
[SIMP_TAC std_ss[SIN_0] THEN REAL_ARITH_TAC,
ONCE_ASM_REWRITE_TAC[] THEN MATCH_MP_TAC FTC1 THEN
RW_TAC std_ss[] THEN ASM_SIMP_TAC arith_ss[DIFF_SIN]], ALL_TAC] THEN
SUBGOAL_THEN“cos 0 − cosx = −cos x − cos 0”ASSUME_TAC THENL
[REWRITE_TAC[REAL_SUB_NEG2], ONCE_ASM_REWRITE_TAC[]] THEN
HO_MATCH_MP_TAC FTC1 THEN ASM_SIMP_TAC std_ss[DIFF_NEG_COS]);In this proof, we employ the linear property of integral DINT_LINEAR to divide the integral of the addition of two functions into the addition of two integrals of the two functions; then we prove the two integrals, respectively. For instantiating the input variableVi1 and Vi2, the derivative of negative cosine is proved in advance:
(30)ddt(-cost)|t=x=sinx,val DIFF_NEG_COS = store_thm(“DIFF_NEG_COS”),“!x. ((∖t.-cost) diffl sin(x)) (x)”,GEN_TAC THEN SUBGOAL_THEN“sinx=-sinx” ASSUME_TAC THENL[REWRITE_TAC[REAL_NEGNEG],ALL_TAC] THENONCE_ASM_REWRITE_TAC[] THENMATCH_MP_TAC DIFF_NEG THEN REWRITE_TAC[DIFF_COS]).


## 4. Conclusion

In this paper, we presented a higher-order logic formalization of the gauge integral. The major properties of the gauge integral, including the linearity, boundedness, monotonicity, integration by parts, and Cauchy-type integrability criterion, were formalized and proven in HOL4, and then a formal proving of an inverting integrator was presented. The proposed integral theorem library has been accepted by HOL4 authority and will appear in HOL4 Kananaskis-9.



---

*Source: 160875-2013-05-02.xml*