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;
mueller@4559
     1
(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
mueller@4559
     2
    ID:         $Id$
mueller@4559
     3
    Author:     Olaf M"uller
mueller@4559
     4
    Copyright   1997  TU Muenchen
mueller@4559
     5
mueller@4559
     6
Temporal Logic of Steps -- tailored for I/O automata
mueller@4559
     7
*)   
mueller@4559
     8
mueller@4559
     9
		       
mueller@4559
    10
TLS = IOA + TL + 
mueller@4559
    11
mueller@4559
    12
default term
mueller@4559
    13
mueller@4559
    14
types
mueller@4559
    15
mueller@4559
    16
 ('a,'s)ioa_temp       = "('a option,'s)transition temporal" 
mueller@4559
    17
 ('a,'s)step_pred      = "('a option,'s)transition predicate"
mueller@4559
    18
  's state_pred        = "'s predicate"
mueller@4559
    19
 
mueller@4559
    20
consts
mueller@4559
    21
mueller@4559
    22
mueller@4559
    23
option_lift :: "('a => 'b) => 'b => ('a option => 'b)"
mueller@4559
    24
plift       :: "('a => bool) => ('a option => bool)"
mueller@4559
    25
 
mueller@4559
    26
temp_sat   :: "('a,'s)execution => ('a,'s)ioa_temp => bool"    (infixr "|==" 22)
mueller@4559
    27
xt1        :: "'s predicate => ('a,'s)step_pred"
mueller@4559
    28
xt2        :: "'a option predicate => ('a,'s)step_pred"
mueller@4559
    29
mueller@4559
    30
validTE    :: "('a,'s)ioa_temp => bool"
mueller@4559
    31
validIOA   :: "('a,'s)ioa => ('a,'s)ioa_temp => bool"
mueller@4559
    32
mueller@4559
    33
mueller@4559
    34
ex2seq     :: "('a,'s)execution => ('a option,'s)transition Seq"
mueller@4559
    35
ex2seqC    :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)" 
mueller@4559
    36
mueller@4559
    37
mueller@4559
    38
defs
mueller@4559
    39
mueller@4559
    40
(* should be in Option as option_lift1, and option_map should be renamed to 
mueller@4559
    41
   option_lift2 *)
mueller@4559
    42
option_lift_def
mueller@4559
    43
  "option_lift f s y == case y of None => s | Some x => (f x)"
mueller@4559
    44
mueller@4559
    45
(* plift is used to determine that None action is always false in 
mueller@4559
    46
   transition predicates *)
mueller@4559
    47
plift_def
mueller@4559
    48
  "plift P == option_lift P False"
mueller@4559
    49
mueller@4559
    50
temp_sat_def
mueller@4559
    51
  "ex |== P == ((ex2seq ex) |= P)"
mueller@4559
    52
mueller@4559
    53
xt1_def
mueller@4559
    54
  "xt1 P tr == P (fst tr)"
mueller@4559
    55
mueller@4559
    56
xt2_def
mueller@4559
    57
  "xt2 P tr == P (fst (snd tr))"
mueller@4559
    58
mueller@4559
    59
mueller@4559
    60
(* FIX: Clarify type and Herkunft of a !! *)
mueller@4559
    61
ex2seq_def
mueller@4559
    62
  "ex2seq ex == ((ex2seqC `(snd ex)) (fst ex))"
mueller@4559
    63
mueller@4559
    64
ex2seqC_def
mueller@4559
    65
  "ex2seqC == (fix`(LAM h ex. (%s. case ex of 
mueller@4559
    66
      nil =>  (s,None,s)>>nil
mueller@4559
    67
    | x##xs => (flift1 (%pr.
mueller@4559
    68
                (s,Some (fst pr), snd pr)>> (h`xs) (snd pr)) 
mueller@4559
    69
                `x)
mueller@4559
    70
      )))"
mueller@4559
    71
mueller@4559
    72
validTE_def
mueller@4559
    73
  "validTE P == ! ex. (ex |== P)"
mueller@4559
    74
mueller@4559
    75
validIOA_def
mueller@4559
    76
  "validIOA A P == ! ex : executions A . (ex |== P)"
mueller@4559
    77
mueller@4559
    78
mueller@4559
    79
end
mueller@4559
    80