--- a/src/HOL/UNITY/UNITY.thy Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/UNITY.thy Thu Oct 15 11:35:07 1998 +0200
@@ -8,20 +8,33 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-UNITY = LessThan +
+UNITY = Traces + Prefix +
constdefs
- constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool"
- "constrains acts A B == ALL act:acts. act^^A <= B"
+ 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)set set => 'a set => bool"
- "stable acts A == constrains acts A 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 :: "[('a * 'a)set set, 'a set] => 'a set"
- "strongest_rhs acts A == Inter {B. constrains acts A B}"
+ (*The traditional word for inductive properties. Anyway, INDUCTIVE is
+ reserved!*)
+ invariant :: "'a set => 'a program set"
+ "invariant A == {F. Init F <= A} Int stable A"
- unless :: "[('a * 'a)set set, 'a set, 'a set] => bool"
- "unless acts A B == constrains acts (A-B) (A Un B)"
+ (*Safety properties*)
+ always :: "'a set => 'a program set"
+ "always A == {F. reachable F <= A}"
+
+ (*Polymorphic in both states and the meaning of <= *)
+ increasing :: "['a => 'b::{ord}] => 'a program set"
+ "increasing f == INT z. stable {s. z <= f s}"
end