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