--- a/src/HOL/UNITY/UNITY.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/UNITY.thy Sat Sep 23 16:02:01 2000 +0200
@@ -11,21 +11,30 @@
UNITY = Main +
typedef (Program)
- 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
+ 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
+ allowed :: ('a * 'a)set set). Id:acts & Id: allowed}"
consts
constrains :: "['a set, 'a set] => 'a program set" (infixl "co" 60)
op_unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 60)
constdefs
- mk_program :: "('a set * ('a * 'a)set set) => 'a program"
- "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
+ mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
+ => 'a program"
+ "mk_program == %(init, acts, allowed).
+ Abs_Program (init, insert Id acts, insert Id allowed)"
Init :: "'a program => 'a set"
- "Init F == (%(init, acts). init) (Rep_Program F)"
+ "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
Acts :: "'a program => ('a * 'a)set set"
- "Acts F == (%(init, acts). acts) (Rep_Program F)"
+ "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
+
+ AllowedActs :: "'a program => ('a * 'a)set set"
+ "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
+
+ Allowed :: "'a program => 'a program set"
+ "Allowed F == {G. Acts G <= AllowedActs F}"
stable :: "'a set => 'a program set"
"stable A == A co A"