src/HOL/UNITY/Traces.thy
author oheimb
Mon, 27 Apr 1998 19:30:40 +0200
changeset 4837 eab729051897
parent 4776 1f9362e769c1
child 5111 8f4b72f0c15d
permissions -rw-r--r--
removed wrong comment
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     1
Traces = UNITY +
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     2
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     3
consts traces :: "['a set, ('a * 'a)set set] => 'a list set"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     4
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     5
inductive "traces Init Acts"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     6
  intrs 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
         (*Initial trace is empty*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     8
    Init  "s: Init ==> [s] : traces Init Acts"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     9
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    10
    Acts  "[| act: Acts;  s#evs : traces Init Acts;  (s,s'): act |]
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    11
	   ==> s'#s#evs : traces Init Acts"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    12
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    13
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    14
consts reachable :: "['a set, ('a * 'a)set set] => 'a set"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    15
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    16
inductive "reachable Init Acts"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    17
  intrs 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    18
    Init  "s: Init ==> s : reachable Init Acts"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    19
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    20
    Acts  "[| act: Acts;  s : reachable Init Acts;  (s,s'): act |]
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    21
	   ==> s' : reachable Init Acts"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    22
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    23
end