--- 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]