src/HOLCF/IOA/meta_theory/TLS.thy
changeset 4559 8e604d885b54
child 4577 674b0b354feb
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Mon Jan 12 17:48:23 1998 +0100
     1.3 @@ -0,0 +1,80 @@
     1.4 +(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Olaf M"uller
     1.7 +    Copyright   1997  TU Muenchen
     1.8 +
     1.9 +Temporal Logic of Steps -- tailored for I/O automata
    1.10 +*)   
    1.11 +
    1.12 +		       
    1.13 +TLS = IOA + TL + 
    1.14 +
    1.15 +default term
    1.16 +
    1.17 +types
    1.18 +
    1.19 + ('a,'s)ioa_temp       = "('a option,'s)transition temporal" 
    1.20 + ('a,'s)step_pred      = "('a option,'s)transition predicate"
    1.21 +  's state_pred        = "'s predicate"
    1.22 + 
    1.23 +consts
    1.24 +
    1.25 +
    1.26 +option_lift :: "('a => 'b) => 'b => ('a option => 'b)"
    1.27 +plift       :: "('a => bool) => ('a option => bool)"
    1.28 + 
    1.29 +temp_sat   :: "('a,'s)execution => ('a,'s)ioa_temp => bool"    (infixr "|==" 22)
    1.30 +xt1        :: "'s predicate => ('a,'s)step_pred"
    1.31 +xt2        :: "'a option predicate => ('a,'s)step_pred"
    1.32 +
    1.33 +validTE    :: "('a,'s)ioa_temp => bool"
    1.34 +validIOA   :: "('a,'s)ioa => ('a,'s)ioa_temp => bool"
    1.35 +
    1.36 +
    1.37 +ex2seq     :: "('a,'s)execution => ('a option,'s)transition Seq"
    1.38 +ex2seqC    :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)" 
    1.39 +
    1.40 +
    1.41 +defs
    1.42 +
    1.43 +(* should be in Option as option_lift1, and option_map should be renamed to 
    1.44 +   option_lift2 *)
    1.45 +option_lift_def
    1.46 +  "option_lift f s y == case y of None => s | Some x => (f x)"
    1.47 +
    1.48 +(* plift is used to determine that None action is always false in 
    1.49 +   transition predicates *)
    1.50 +plift_def
    1.51 +  "plift P == option_lift P False"
    1.52 +
    1.53 +temp_sat_def
    1.54 +  "ex |== P == ((ex2seq ex) |= P)"
    1.55 +
    1.56 +xt1_def
    1.57 +  "xt1 P tr == P (fst tr)"
    1.58 +
    1.59 +xt2_def
    1.60 +  "xt2 P tr == P (fst (snd tr))"
    1.61 +
    1.62 +
    1.63 +(* FIX: Clarify type and Herkunft of a !! *)
    1.64 +ex2seq_def
    1.65 +  "ex2seq ex == ((ex2seqC `(snd ex)) (fst ex))"
    1.66 +
    1.67 +ex2seqC_def
    1.68 +  "ex2seqC == (fix`(LAM h ex. (%s. case ex of 
    1.69 +      nil =>  (s,None,s)>>nil
    1.70 +    | x##xs => (flift1 (%pr.
    1.71 +                (s,Some (fst pr), snd pr)>> (h`xs) (snd pr)) 
    1.72 +                `x)
    1.73 +      )))"
    1.74 +
    1.75 +validTE_def
    1.76 +  "validTE P == ! ex. (ex |== P)"
    1.77 +
    1.78 +validIOA_def
    1.79 +  "validIOA A P == ! ex : executions A . (ex |== P)"
    1.80 +
    1.81 +
    1.82 +end
    1.83 +