src/HOLCF/IOA/meta_theory/TLS.thy
author mueller
Thu Nov 26 16:37:56 1998 +0100 (1998-11-26)
changeset 5976 44290b71a85f
parent 5677 4feffde494cf
child 10835 f4745d77e620
permissions -rw-r--r--
tuning to assimiliate it with PhD;
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@5677
    33
mkfin      :: "'a Seq => 'a Seq"
mueller@4559
    34
mueller@4559
    35
ex2seq     :: "('a,'s)execution => ('a option,'s)transition Seq"
mueller@4559
    36
ex2seqC    :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)" 
mueller@4559
    37
mueller@4559
    38
mueller@4559
    39
defs
mueller@4559
    40
mueller@5677
    41
mkfin_def
mueller@5677
    42
  "mkfin s == if Partial s then @t. Finite t & s = t @@ UU
mueller@5677
    43
                           else s"
mueller@5677
    44
mueller@4559
    45
option_lift_def
mueller@4559
    46
  "option_lift f s y == case y of None => s | Some x => (f x)"
mueller@4559
    47
mueller@4559
    48
(* plift is used to determine that None action is always false in 
mueller@4559
    49
   transition predicates *)
mueller@4559
    50
plift_def
mueller@4559
    51
  "plift P == option_lift P False"
mueller@4559
    52
mueller@4559
    53
temp_sat_def
mueller@4559
    54
  "ex |== P == ((ex2seq ex) |= P)"
mueller@4559
    55
mueller@4559
    56
xt1_def
mueller@4559
    57
  "xt1 P tr == P (fst tr)"
mueller@4559
    58
mueller@4559
    59
xt2_def
mueller@4559
    60
  "xt2 P tr == P (fst (snd tr))"
mueller@4559
    61
mueller@4559
    62
ex2seq_def
mueller@5677
    63
  "ex2seq ex == ((ex2seqC `(mkfin (snd ex))) (fst ex))"
mueller@4559
    64
mueller@4559
    65
ex2seqC_def
mueller@4559
    66
  "ex2seqC == (fix`(LAM h ex. (%s. case ex of 
mueller@4559
    67
      nil =>  (s,None,s)>>nil
mueller@4559
    68
    | x##xs => (flift1 (%pr.
mueller@4559
    69
                (s,Some (fst pr), snd pr)>> (h`xs) (snd pr)) 
mueller@4559
    70
                `x)
mueller@4559
    71
      )))"
mueller@4559
    72
mueller@4559
    73
validTE_def
mueller@4559
    74
  "validTE P == ! ex. (ex |== P)"
mueller@4559
    75
mueller@4559
    76
validIOA_def
mueller@4559
    77
  "validIOA A P == ! ex : executions A . (ex |== P)"
mueller@4559
    78
mueller@5976
    79
mueller@5976
    80
mueller@4577
    81
rules
mueller@4577
    82
mueller@5677
    83
mkfin_UU
mueller@5677
    84
  "mkfin UU = nil"
mueller@5677
    85
mueller@5677
    86
mkfin_nil
mueller@5677
    87
  "mkfin nil =nil"
mueller@5677
    88
mueller@5677
    89
mkfin_cons
mueller@5677
    90
  "(mkfin (a>>s)) = (a>>(mkfin s))"
mueller@5677
    91
mueller@4577
    92
mueller@4559
    93
mueller@4559
    94
end
mueller@4559
    95