# 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 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>