src/HOLCF/IOA/meta_theory/LiveIOA.thy
changeset 17233 41eee2e7b465
parent 14981 e73f8140af78
child 19741 f65265d71426
     1.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Fri Sep 02 15:54:47 2005 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Fri Sep 02 17:23:59 2005 +0200
     1.3 @@ -1,18 +1,19 @@
     1.4  (*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
     1.5      ID:         $Id$
     1.6      Author:     Olaf Müller
     1.7 +*)
     1.8  
     1.9 -Live I/O automata -- specified by temproal formulas.
    1.10 -*) 
    1.11 -  
    1.12 -LiveIOA = TLS + 
    1.13 +header {* Live I/O automata -- specified by temproal formulas *}
    1.14  
    1.15 -default type
    1.16 +theory LiveIOA
    1.17 +imports TLS
    1.18 +begin
    1.19 +
    1.20 +defaultsort type
    1.21  
    1.22  types
    1.23 +  ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
    1.24  
    1.25 - ('a,'s)live_ioa       = "('a,'s)ioa * ('a,'s)ioa_temp"
    1.26 - 
    1.27  consts
    1.28  
    1.29  validLIOA   :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool"
    1.30 @@ -25,36 +26,37 @@
    1.31  live_implements   :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
    1.32  is_live_ref_map   :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
    1.33  
    1.34 - 
    1.35 +
    1.36  defs
    1.37  
    1.38 -validLIOA_def
    1.39 +validLIOA_def:
    1.40    "validLIOA AL P == validIOA (fst AL) ((snd AL) .--> P)"
    1.41  
    1.42  
    1.43 -WF_def
    1.44 +WF_def:
    1.45    "WF A acts ==  <> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
    1.46  
    1.47 -SF_def
    1.48 +SF_def:
    1.49    "SF A acts ==  [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
    1.50 - 
    1.51 +
    1.52  
    1.53 -liveexecutions_def
    1.54 +liveexecutions_def:
    1.55     "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
    1.56  
    1.57 -livetraces_def
    1.58 +livetraces_def:
    1.59    "livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
    1.60  
    1.61 -live_implements_def
    1.62 -  "live_implements CL AM == (inp (fst CL) = inp (fst AM)) & 
    1.63 +live_implements_def:
    1.64 +  "live_implements CL AM == (inp (fst CL) = inp (fst AM)) &
    1.65                              (out (fst CL) = out (fst AM)) &
    1.66                              livetraces CL <= livetraces AM"
    1.67  
    1.68 -is_live_ref_map_def
    1.69 -   "is_live_ref_map f CL AM ==  
    1.70 -            is_ref_map f (fst CL ) (fst AM) & 
    1.71 -            (! exec : executions (fst CL). (exec |== (snd CL)) --> 
    1.72 +is_live_ref_map_def:
    1.73 +   "is_live_ref_map f CL AM ==
    1.74 +            is_ref_map f (fst CL ) (fst AM) &
    1.75 +            (! exec : executions (fst CL). (exec |== (snd CL)) -->
    1.76                                             ((corresp_ex (fst AM) f exec) |== (snd AM)))"
    1.77  
    1.78 +ML {* use_legacy_bindings (the_context ()) *}
    1.79  
    1.80 -end
    1.81 \ No newline at end of file
    1.82 +end