(* Title: HOLCF/IOA/meta_theory/TLS.thy ID: $Id: TL.thy,v 1.10 2005/09/02 15:24:03 wenzelm Exp $ Author: Olaf Müller *) header {* A General Temporal Logic *} theory TL imports Pred Sequence begin defaultsort 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)" ML {* use_legacy_bindings (the_context ()) *} end
theorem simple:
[] <> (¬ P) = (¬ <> [] P)
theorem Boxnil:
nil |= [] P
theorem Diamondnil:
¬ (nil |= <> P)
theorem Diamond_def2:
(<> F) s = (∃s2. tsuffix s2 s ∧ F s2)
theorem suffix_refl:
suffix s s
theorem reflT:
s ≠ UU ∧ s ≠ nil --> (s |= [] F --> F)
theorem suffix_trans:
[| suffix y x; suffix z y |] ==> suffix z x
theorem transT:
s |= [] F --> [] [] F
theorem normalT:
s |= [] (F --> G) --> [] F --> [] G
theorem STL1a:
validT P ==> validT ([] P)
theorem STL1b:
valid P ==> validT <P>
theorem STL1:
valid P ==> validT ([] <P>)
theorem STL4:
valid (P --> Q) ==> validT ([] <P> --> [] <Q>)
theorem tsuffix_TL:
[| s ≠ UU ∧ s ≠ nil; tsuffix s2.0 (TL·s) |] ==> tsuffix s2.0 s
theorem LTL1:
s ≠ UU ∧ s ≠ nil --> (s |= [] F --> F ∧ Next ([] F))
theorem LTL2a:
s |= ¬ Next F --> Next (¬ F)
theorem LTL2b:
s |= Next (¬ F) --> ¬ Next F
theorem LTL3:
ex |= Next (F --> G) --> Next F --> Next G
theorem ModusPonens:
[| validT (P --> Q); validT P |] ==> validT Q