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