(* Title: HOLCF/IOA/meta_theory/TLS.thy ID: $Id: TLS.thy,v 1.9 2005/09/02 15:24:03 wenzelm Exp $ Author: Olaf Müller *) header {* Temporal Logic of Steps -- tailored for I/O automata *} theory TLS imports IOA TL begin defaultsort type types ('a, 's) ioa_temp = "('a option,'s)transition temporal" ('a, 's) step_pred = "('a option,'s)transition predicate" 's state_pred = "'s predicate" consts option_lift :: "('a => 'b) => 'b => ('a option => 'b)" plift :: "('a => bool) => ('a option => bool)" temp_sat :: "('a,'s)execution => ('a,'s)ioa_temp => bool" (infixr "|==" 22) xt1 :: "'s predicate => ('a,'s)step_pred" xt2 :: "'a option predicate => ('a,'s)step_pred" validTE :: "('a,'s)ioa_temp => bool" validIOA :: "('a,'s)ioa => ('a,'s)ioa_temp => bool" mkfin :: "'a Seq => 'a Seq" ex2seq :: "('a,'s)execution => ('a option,'s)transition Seq" ex2seqC :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)" defs mkfin_def: "mkfin s == if Partial s then @t. Finite t & s = t @@ UU else s" option_lift_def: "option_lift f s y == case y of None => s | Some x => (f x)" (* plift is used to determine that None action is always false in transition predicates *) plift_def: "plift P == option_lift P False" temp_sat_def: "ex |== P == ((ex2seq ex) |= P)" xt1_def: "xt1 P tr == P (fst tr)" xt2_def: "xt2 P tr == P (fst (snd tr))" ex2seq_def: "ex2seq ex == ((ex2seqC $(mkfin (snd ex))) (fst ex))" ex2seqC_def: "ex2seqC == (fix$(LAM h ex. (%s. case ex of nil => (s,None,s)>>nil | x##xs => (flift1 (%pr. (s,Some (fst pr), snd pr)>> (h$xs) (snd pr)) $x) )))" validTE_def: "validTE P == ! ex. (ex |== P)" validIOA_def: "validIOA A P == ! ex : executions A . (ex |== P)" axioms mkfin_UU: "mkfin UU = nil" mkfin_nil: "mkfin nil =nil" mkfin_cons: "(mkfin (a>>s)) = (a>>(mkfin s))" ML {* use_legacy_bindings (the_context ()) *} end
theorem ex2seqC_unfold:
ex2seqC = (LAM ex. (%s. case ex of nil => [(s, None, s)!] | x ## xs => (FLIFT pr. (s, Some (fst pr), snd pr)>>(ex2seqC·xs) (snd pr))·x))
theorem ex2seqC_UU:
(ex2seqC·UU) s = UU
theorem ex2seqC_nil:
(ex2seqC·nil) s = [(s, None, s)!]
theorem ex2seqC_cons:
(ex2seqC·((a, t)>>xs)) s = (s, Some a, t)>>(ex2seqC·xs) t
theorem ex2seq_UU:
ex2seq (s, UU) = [(s, None, s)!]
theorem ex2seq_nil:
ex2seq (s, nil) = [(s, None, s)!]
theorem ex2seq_cons:
ex2seq (s, (a, t)>>ex) = (s, Some a, t)>>ex2seq (t, ex)
theorem ex2seq_nUUnnil:
ex2seq exec ≠ UU ∧ ex2seq exec ≠ nil
theorem TL_TLS:
∀s a t. P s ∧ s -a--A-> t --> Q t ==> ex |== <%(s, a, t). P s> ∧ <%(s, a, t). s -a--A-> t> --> Next <%(s, a, t). Q s>