src/HOL/UNITY/Constrains.ML
changeset 5784 54276fba8420
parent 5669 f5d9caafc3bd
child 5804 8e0a4c4fd67b
--- 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. ***)