Defining linearity of integrals using Temporal Logic of Actions

[marta zhango]

I would like to make a proof using Temporal Logic of Actions (TLA) to show the linearity of the Fourier Transform.  I want to define the linearity of integrals so that I can using as a conditions in the proof.  

Perhaps with a let using some letter to define the action, say `A`.  Then say that `by A` means by the linearity of integrals at the end of the line  How would it look like?

For instance I can define the action

$\mathcal{I}(h(t)) \triangleq \int_a^b h(t) \, dt$

and stating linearity of integrals as an axiom

$\text{Linearity} : \quad \mathcal{I}(a f(t) + b g(t)) = a \mathcal{I}(f(t)) + b \mathcal{I}(g(t))$

The proof would look like

$\mathcal{F}\{h(t)\} = \int_{-\infty}^{\infty} \big(a f(t) + b g(t)\big) e^{-i\omega t} \, dt$

$\mathcal{F}\{h(t)\} = a \int_{-\infty}^{\infty} f(t) e^{-i\omega t} \, dt + b \int_{-\infty}^{\infty} g(t) e^{-i\omega t} \, dt \;\;\;$ by [linearity]

What should I put instead of `by [linearity]` in my proof and how would the linearity statement be defined?

$\rule{8cm}{0.3mm}$

Have proceeded as follows

LET: $\;\;\; h(t) \triangleq a \cdot f(t) + b \cdot g(t)$

$\;\;\;\;\;\;\; \mathcal{I}(h(t)) \triangleq \int_a^b h(t) \, dt = a \int_a^b  f(t) \, dt + b \int_a^b g(t) \, dx$

$\;\;\;\;\;\;\; \mathcal{F}\{h(t)\} \triangleq \int_{-\infty}^{\infty} h(t) \, e^{-i\omega t} \, dt$

$\langle 1 \rangle \;\; \mathcal{F}\{h(t)\} = \int_{-\infty}^{\infty} (a f(t) + b g(t)) \, e^{-i\omega t} \, dt$

$\quad\quad\quad\quad \;\;\; = \int_{-\infty}^{\infty} a \left( f(t) e^{-i\omega t} \right) + b \left( g(t) \, e^{-i\omega t} \right) \, dt$

$\quad\quad\quad\quad \;\;\; = a \int_{-\infty}^{\infty} f(t) e^{-i\omega t} \, dt + b \int_{-\infty}^{\infty} g(t) e^{-i\omega t} \, dt \;\;\;\;\; [\mathcal{I}(h(t))]$

[Andrew Helwer]

As stated in the other thread, TLAPM does not yet support checking proofs involving real numbers. However, if you are just looking to write the proof in the TLA+ structured proof formalism without machine-checking its correctness, that can certainly be done.

Andrew Helwer