# HG changeset patch
# User paulson
# Date 909834325 -3600
# Node ID 54276fba84202164be07f6eb05d4c36d66693b64
# Parent  95ac0bf10518896b443509b9c0bfefdfec952672
the Increasing operator

diff -r 95ac0bf10518 -r 54276fba8420 src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Sat Oct 31 12:43:56 1998 +0100
+++ b/src/HOL/UNITY/Constrains.ML	Sat Oct 31 12:45:25 1998 +0100
@@ -150,6 +150,27 @@
 
 
 
+(*** Increasing ***)
+
+Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
+     "Increasing f <= Increasing (length o f)";
+by Auto_tac;
+by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
+qed "Increasing_length";
+
+Goalw [Increasing_def]
+     "Increasing f <= {F. ALL z::nat. F: Stable {s. z < f s}}";
+by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
+by (Blast_tac 1);
+qed "Increasing_less";
+
+Goalw [increasing_def, Increasing_def]
+     "F : increasing f ==> F : Increasing f";
+by (blast_tac (claset() addIs [stable_imp_Stable]) 1);
+qed "increasing_imp_Increasing";
+
+
+
 (*** The Elimination Theorem.  The "free" m has become universally quantified!
      Should the premise be !!m instead of ALL m ?  Would make it harder to use
      in forward proof. ***)
diff -r 95ac0bf10518 -r 54276fba8420 src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Sat Oct 31 12:43:56 1998 +0100
+++ b/src/HOL/UNITY/Constrains.thy	Sat Oct 31 12:45:25 1998 +0100
@@ -23,4 +23,8 @@
   Invariant :: "'a set => 'a program set"
     "Invariant A == {F. Init F <= A} Int Stable 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