src/HOLCF/IOA/meta_theory/TLS.thy
author wenzelm
Fri Sep 02 17:23:59 2005 +0200 (2005-09-02)
changeset 17233 41eee2e7b465
parent 14981 e73f8140af78
child 19741 f65265d71426
permissions -rw-r--r--
converted specifications to Isar theories;
     1 (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
     2     ID:         $Id$
     3     Author:     Olaf Müller
     4 *)
     5 
     6 header {* Temporal Logic of Steps -- tailored for I/O automata *}
     7 
     8 theory TLS
     9 imports IOA TL
    10 begin
    11 
    12 defaultsort type
    13 
    14 types
    15   ('a, 's) ioa_temp  = "('a option,'s)transition temporal"
    16   ('a, 's) step_pred = "('a option,'s)transition predicate"
    17   's state_pred      = "'s predicate"
    18 
    19 consts
    20 
    21 option_lift :: "('a => 'b) => 'b => ('a option => 'b)"
    22 plift       :: "('a => bool) => ('a option => bool)"
    23 
    24 temp_sat   :: "('a,'s)execution => ('a,'s)ioa_temp => bool"    (infixr "|==" 22)
    25 xt1        :: "'s predicate => ('a,'s)step_pred"
    26 xt2        :: "'a option predicate => ('a,'s)step_pred"
    27 
    28 validTE    :: "('a,'s)ioa_temp => bool"
    29 validIOA   :: "('a,'s)ioa => ('a,'s)ioa_temp => bool"
    30 
    31 mkfin      :: "'a Seq => 'a Seq"
    32 
    33 ex2seq     :: "('a,'s)execution => ('a option,'s)transition Seq"
    34 ex2seqC    :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)"
    35 
    36 
    37 defs
    38 
    39 mkfin_def:
    40   "mkfin s == if Partial s then @t. Finite t & s = t @@ UU
    41                            else s"
    42 
    43 option_lift_def:
    44   "option_lift f s y == case y of None => s | Some x => (f x)"
    45 
    46 (* plift is used to determine that None action is always false in
    47    transition predicates *)
    48 plift_def:
    49   "plift P == option_lift P False"
    50 
    51 temp_sat_def:
    52   "ex |== P == ((ex2seq ex) |= P)"
    53 
    54 xt1_def:
    55   "xt1 P tr == P (fst tr)"
    56 
    57 xt2_def:
    58   "xt2 P tr == P (fst (snd tr))"
    59 
    60 ex2seq_def:
    61   "ex2seq ex == ((ex2seqC $(mkfin (snd ex))) (fst ex))"
    62 
    63 ex2seqC_def:
    64   "ex2seqC == (fix$(LAM h ex. (%s. case ex of
    65       nil =>  (s,None,s)>>nil
    66     | x##xs => (flift1 (%pr.
    67                 (s,Some (fst pr), snd pr)>> (h$xs) (snd pr))
    68                 $x)
    69       )))"
    70 
    71 validTE_def:
    72   "validTE P == ! ex. (ex |== P)"
    73 
    74 validIOA_def:
    75   "validIOA A P == ! ex : executions A . (ex |== P)"
    76 
    77 
    78 axioms
    79 
    80 mkfin_UU:
    81   "mkfin UU = nil"
    82 
    83 mkfin_nil:
    84   "mkfin nil =nil"
    85 
    86 mkfin_cons:
    87   "(mkfin (a>>s)) = (a>>(mkfin s))"
    88 
    89 ML {* use_legacy_bindings (the_context ()) *}
    90 
    91 end