--- a/src/HOL/UNITY/Traces.thy Wed Dec 02 16:14:09 1998 +0100
+++ b/src/HOL/UNITY/Traces.thy Thu Dec 03 10:45:06 1998 +0100
@@ -25,17 +25,32 @@
typedef (Program)
- 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
+ 'a program = "{(states :: 'a set,
+ init :: 'a set,
+ acts :: ('a * 'a)set set).
+ init <= states &
+ acts <= Pow(states Times states) &
+ diag states : acts}"
constdefs
- mk_program :: "('a set * ('a * 'a)set set) => 'a program"
- "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
+ restrict_rel :: "['a set, ('a * 'a) set] => ('a * 'a) set"
+ "restrict_rel A r == (A Times A) Int r"
- Init :: "'a program => 'a set"
- "Init F == fst (Rep_Program F)"
+ mk_program :: "('a set * 'a set * ('a * 'a)set set) => 'a program"
+ "mk_program ==
+ %(states, init, acts).
+ Abs_Program (states,
+ states Int init,
+ restrict_rel states `` (insert Id acts))"
- Acts :: "'a program => ('a * 'a)set set"
- "Acts F == snd (Rep_Program F)"
+ States :: "'a program => 'a set"
+ "States F == (%(states, init, acts). states) (Rep_Program F)"
+
+ Init :: "'a program => 'a set"
+ "Init F == (%(states, init, acts). init) (Rep_Program F)"
+
+ Acts :: "'a program => ('a * 'a)set set"
+ "Acts F == (%(states, init, acts). acts) (Rep_Program F)"
consts reachable :: "'a program => 'a set"