--- a/src/HOL/UNITY/UNITY.thy Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/UNITY.thy Thu Apr 29 10:51:58 1999 +0200
@@ -14,6 +14,9 @@
typedef (Program)
'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
+consts
+ co, unless :: "['a set, 'a set] => 'a program set" (infixl 60)
+
constdefs
mk_program :: "('a set * ('a * 'a)set set) => 'a program"
"mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
@@ -24,17 +27,11 @@
Acts :: "'a program => ('a * 'a)set set"
"Acts F == (%(init, acts). acts) (Rep_Program F)"
- constrains :: "['a set, 'a set] => 'a program set"
- "constrains A B == {F. ALL act: Acts F. act^^A <= B}"
-
stable :: "'a set => 'a program set"
- "stable A == constrains A A"
+ "stable A == A co A"
strongest_rhs :: "['a program, 'a set] => 'a set"
- "strongest_rhs F A == Inter {B. F : constrains A B}"
-
- unless :: "['a set, 'a set] => 'a program set"
- "unless A B == constrains (A-B) (A Un B)"
+ "strongest_rhs F A == Inter {B. F : A co B}"
invariant :: "'a set => 'a program set"
"invariant A == {F. Init F <= A} Int stable A"
@@ -43,4 +40,10 @@
increasing :: "['a => 'b::{ord}] => 'a program set"
"increasing f == INT z. stable {s. z <= f s}"
+
+defs
+ constrains_def "A co B == {F. ALL act: Acts F. act^^A <= B}"
+
+ unless_def "A unless B == (A-B) co (A Un B)"
+
end