Theory TLS

Up to index of Isabelle/HOLCF/IOA

theory TLS
imports IOA TL
uses [TLS.ML]
begin

(*  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 ss -a--A-> t --> Q t
  ==> ex |==
      <%(s, a, t). P s> ∧ <%(s, a, t). s -a--A-> t> --> Next <%(s, a, t). Q s>