src/HOLCF/IOA/meta_theory/TLS.thy
author mueller
Mon Jan 12 17:48:23 1998 +0100 (1998-01-12)
changeset 4559 8e604d885b54
child 4577 674b0b354feb
permissions -rw-r--r--
added files containing temproal logic and abstraction;
     1 (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
     2     ID:         $Id$
     3     Author:     Olaf M"uller
     4     Copyright   1997  TU Muenchen
     5 
     6 Temporal Logic of Steps -- tailored for I/O automata
     7 *)   
     8 
     9 		       
    10 TLS = IOA + TL + 
    11 
    12 default term
    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 
    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 (* should be in Option as option_lift1, and option_map should be renamed to 
    41    option_lift2 *)
    42 option_lift_def
    43   "option_lift f s y == case y of None => s | Some x => (f x)"
    44 
    45 (* plift is used to determine that None action is always false in 
    46    transition predicates *)
    47 plift_def
    48   "plift P == option_lift P False"
    49 
    50 temp_sat_def
    51   "ex |== P == ((ex2seq ex) |= P)"
    52 
    53 xt1_def
    54   "xt1 P tr == P (fst tr)"
    55 
    56 xt2_def
    57   "xt2 P tr == P (fst (snd tr))"
    58 
    59 
    60 (* FIX: Clarify type and Herkunft of a !! *)
    61 ex2seq_def
    62   "ex2seq ex == ((ex2seqC `(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 end
    80