src/HOL/UNITY/Traces.thy
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 4837 eab729051897
permissions -rw-r--r--
New UNITY theory
paulson@4776
     1
Traces = UNITY +
paulson@4776
     2
paulson@4776
     3
consts traces :: "['a set, ('a * 'a)set set] => 'a list set"
paulson@4776
     4
paulson@4776
     5
inductive "traces Init Acts"
paulson@4776
     6
  intrs 
paulson@4776
     7
         (*Initial trace is empty*)
paulson@4776
     8
    Init  "s: Init ==> [s] : traces Init Acts"
paulson@4776
     9
paulson@4776
    10
    Acts  "[| act: Acts;  s#evs : traces Init Acts;  (s,s'): act |]
paulson@4776
    11
	   ==> s'#s#evs : traces Init Acts"
paulson@4776
    12
paulson@4776
    13
paulson@4776
    14
consts reachable :: "['a set, ('a * 'a)set set] => 'a set"
paulson@4776
    15
paulson@4776
    16
inductive "reachable Init Acts"
paulson@4776
    17
  intrs 
paulson@4776
    18
         (*Initial trace is empty*)
paulson@4776
    19
    Init  "s: Init ==> s : reachable Init Acts"
paulson@4776
    20
paulson@4776
    21
    Acts  "[| act: Acts;  s : reachable Init Acts;  (s,s'): act |]
paulson@4776
    22
	   ==> s' : reachable Init Acts"
paulson@4776
    23
paulson@4776
    24
end