(* Title: HOLCF/IOA/meta_theory/TLS.thy
ID: $Id$
Author: Olaf Müller
License: GPL (GNU GENERAL PUBLIC LICENSE)
A General Temporal Logic.
*)
TL = Pred + Sequence +
default type
types
'a temporal = 'a Seq predicate
consts
suffix :: "'a Seq => 'a Seq => bool"
tsuffix :: "'a Seq => 'a Seq => bool"
validT :: "'a Seq predicate => bool"
unlift :: "'a lift => 'a"
Init ::"'a predicate => 'a temporal" ("<_>" [0] 1000)
Box ::"'a temporal => 'a temporal" ("[] (_)" [80] 80)
Diamond ::"'a temporal => 'a temporal" ("<> (_)" [80] 80)
Next ::"'a temporal => 'a temporal"
Leadsto ::"'a temporal => 'a temporal => 'a temporal" (infixr "~>" 22)
syntax (xsymbols)
"Box" ::"'a temporal => 'a temporal" ("\\<box> (_)" [80] 80)
"Diamond" ::"'a temporal => 'a temporal" ("\\<diamond> (_)" [80] 80)
"Leadsto" ::"'a temporal => 'a temporal => 'a temporal" (infixr "\\<leadsto>" 22)
defs
unlift_def
"unlift x == (case x of
UU => arbitrary
| Def y => y)"
(* this means that for nil and UU the effect is unpredictable *)
Init_def
"Init P s == (P (unlift (HD$s)))"
suffix_def
"suffix s2 s == ? s1. (Finite s1 & s = s1 @@ s2)"
tsuffix_def
"tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"
Box_def
"([] P) s == ! s2. tsuffix s2 s --> P s2"
Next_def
"(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"
Diamond_def
"<> P == .~ ([] (.~ P))"
Leadsto_def
"P ~> Q == ([] (P .--> (<> Q)))"
validT_def
"validT P == ! s. s~=UU & s~=nil --> (s |= P)"
end