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