1
2Here is a translation of ITL into HOL. 
3
4A pair of numbers (m,n) represents the interval from time m to time n
5inclusive. In pictures:
6
7Time: 0 1 2 3 4  ...  m  ...  n  ...
8                      |       |
9                      *-------*
10                          |
11                   the interval (m,n)  
12
13Each ITL expresssion translates to a function of type ":num#num->ty", where
14ty is the type of the expression's value. The idea is that if e translates to
15f, then e having value v on the interval (m,n) corresponds to f(m,n)=v.
16
17Similarly each ITL formula translates to a function of type ":num#num->bool".
18The idea is that if w translates to p, then w is true on the interval (m,n)
19if and only if p(m,n)=T.
20
21ITL variables of type ty are simulated by HOL variables of type "num->ty",
22the number argument representing time. For example, (X 6) is the value
23of X at the 6th time instant.
24
25Here is the translation; "T[e] = t" means "the translation of the ITL 
26construct e is the HOL term t".
27
28
29T[c]           =  \(m,n). c         {if c is a constant}
30
31T[v]           =  \(m,n). (v m)     {if v is a variable}
32
33T[O e]         =  \(m,n). T[e](m+1,n)
34
35T[e1 gets e2]  =  \(m,n). !i. (m<=i)/\(i<n) ==> (T[e1](i+1,n)=T[e2](i,n))
36
37T[empty]       =  \(m,n). (m=n)
38
39T[length]      =  \(m,n). (n-m)
40
41T[len e]       =  \(m,n). (T[e](m,n)=(n-m))
42
43T[~w]          =  \(m,n). ~(T[e](m,n))
44
45T[w1/\w2]      =  \(m,n). T[w1](m,n) /\ T[w2](m,n)
46
47T[O w]         =  \(m,n). (n>m) /\ T[w](m+1,n)
48
49T[BOX w]       =  \(m,n). !i. (m<=i)/\(i<=n) ==> T[w](i,n)
50
51T[w1;w2]       =  \(m,n). ?i. (m<=i) /\ (i<=n) /\ T[w1](m,i) /\ T[w2](i,n)
52
53T[EXISTS v. w] =  \(m,n). ?v. T[w](m,n)
54
55Easy, isn't it!
56
57
58