src/HOL/UNITY/Traces.thy
changeset 4776 1f9362e769c1
child 4837 eab729051897
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Traces.thy	Fri Apr 03 12:34:33 1998 +0200
     1.3 @@ -0,0 +1,24 @@
     1.4 +Traces = UNITY +
     1.5 +
     1.6 +consts traces :: "['a set, ('a * 'a)set set] => 'a list set"
     1.7 +
     1.8 +inductive "traces Init Acts"
     1.9 +  intrs 
    1.10 +         (*Initial trace is empty*)
    1.11 +    Init  "s: Init ==> [s] : traces Init Acts"
    1.12 +
    1.13 +    Acts  "[| act: Acts;  s#evs : traces Init Acts;  (s,s'): act |]
    1.14 +	   ==> s'#s#evs : traces Init Acts"
    1.15 +
    1.16 +
    1.17 +consts reachable :: "['a set, ('a * 'a)set set] => 'a set"
    1.18 +
    1.19 +inductive "reachable Init Acts"
    1.20 +  intrs 
    1.21 +         (*Initial trace is empty*)
    1.22 +    Init  "s: Init ==> s : reachable Init Acts"
    1.23 +
    1.24 +    Acts  "[| act: Acts;  s : reachable Init Acts;  (s,s'): act |]
    1.25 +	   ==> s' : reachable Init Acts"
    1.26 +
    1.27 +end