# HG changeset patch
# User paulson
# Date 935660263 -7200
# Node ID eddb3d77a36316bfb5d63f3227a7a8c7349d04ea
# Parent  f08fade5ea0d50d35a525466d67b161ae553401c
new destruction rules

diff -r f08fade5ea0d -r eddb3d77a363 src/HOL/UNITY/Follows.ML
--- a/src/HOL/UNITY/Follows.ML	Thu Aug 26 11:37:22 1999 +0200
+++ b/src/HOL/UNITY/Follows.ML	Thu Aug 26 11:37:43 1999 +0200
@@ -12,10 +12,9 @@
 by (blast_tac (claset() addIs [monoD]) 1);
 qed "mono_Always_o";
 
-Goalw [Follows_def]
-    "mono (h::'a::order => 'b::order) \
-\    ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <= \
-\        (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})";
+Goal "mono (h::'a::order => 'b::order) \
+\     ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <= \
+\         (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})";
 by Auto_tac;
 by (rtac single_LeadsTo_I 1);
 by (dres_inst_tac [("x", "g s")] spec 1);
@@ -38,6 +37,29 @@
 qed "Follows_trans";
 
 
+(** Destructiom rules **)
+
+Goalw [Follows_def]
+     "F : f Fols g ==> F : Increasing f";
+by (Blast_tac 1);
+qed "Follows_Increasing1";
+
+Goalw [Follows_def]
+     "F : f Fols g ==> F : Increasing g";
+by (Blast_tac 1);
+qed "Follows_Increasing2";
+
+Goalw [Follows_def]
+     "F : f Fols g ==> F : Always {s. f s <= g s}";
+by (Blast_tac 1);
+qed "Follows_Bounded";
+
+Goalw [Follows_def]
+     "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}";
+by (Blast_tac 1);
+qed "Follows_LeadsTo";
+
+
 (*Can replace "Un" by any sup.  But existing max only works for linorders.*)
 
 Goalw [increasing_def, stable_def, constrains_def]