# HG changeset patch
# User avigad
# Date 1123073316 -7200
# Node ID 036c46df9576a2ff0288ccf3f52ee7f84dcbce8c
# Parent  08f8408853e34728db0f463279052bbfbdb1eabd
added extra transitivity rules

diff -r 08f8408853e3 -r 036c46df9576 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Aug 03 14:48:30 2005 +0200
+++ b/src/HOL/Orderings.thy	Wed Aug 03 14:48:36 2005 +0200
@@ -583,4 +583,124 @@
 end
 *}
 
+subsection {* Extra transitivity rules *}
+
+text {* These support proving chains of decreasing inequalities
+    a >= b >= c ... in Isar proofs. *}
+
+lemma xt1: "a = b ==> b > c ==> a > c"
+by simp
+
+lemma xt2: "a > b ==> b = c ==> a > c"
+by simp
+
+lemma xt3: "a = b ==> b >= c ==> a >= c"
+by simp
+
+lemma xt4: "a >= b ==> b = c ==> a >= c"
+by simp
+
+lemma xt5: "(x::'a::order) >= y ==> y >= x ==> x = y"
+by simp
+
+lemma xt6: "(x::'a::order) >= y ==> y >= z ==> x >= z"
+by simp
+
+lemma xt7: "(x::'a::order) > y ==> y >= z ==> x > z"
+by simp
+
+lemma xt8: "(x::'a::order) >= y ==> y > z ==> x > z"
+by simp
+
+lemma xt9: "(a::'a::order) > b ==> b > a ==> ?P"
+by simp
+
+lemma xt10: "(x::'a::order) > y ==> y > z ==> x > z"
+by simp
+
+lemma xt11: "(a::'a::order) >= b ==> a ~= b ==> a > b"
+by simp
+
+lemma xt12: "(a::'a::order) ~= b ==> a >= b ==> a > b"
+by simp
+
+lemma xt13: "a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==>
+    a > f c" 
+by simp
+
+lemma xt14: "a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==>
+    f a > c"
+by auto
+
+lemma xt15: "a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==>
+    a >= f c"
+by simp
+
+lemma xt16: "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==>
+    f a >= c"
+by auto
+
+lemma xt17: "(a::'a::order) >= f b ==> b >= c ==> 
+    (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
+by (subgoal_tac "f b >= f c", force, force)
+
+lemma xt18: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==> 
+    (!!x y. x >= y ==> f x >= f y) ==> f a >= c"
+by (subgoal_tac "f a >= f b", force, force)
+
+lemma xt19: "(a::'a::order) > f b ==> (b::'b::order) >= c ==>
+  (!!x y. x >= y ==> f x >= f y) ==> a > f c"
+by (subgoal_tac "f b >= f c", force, force)
+
+lemma xt20: "(a::'a::order) > b ==> (f b::'b::order) >= c==>
+    (!!x y. x > y ==> f x > f y) ==> f a > c"
+by (subgoal_tac "f a > f b", force, force)
+
+lemma xt21: "(a::'a::order) >= f b ==> b > c ==>
+    (!!x y. x > y ==> f x > f y) ==> a > f c"
+by (subgoal_tac "f b > f c", force, force)
+
+lemma xt22: "(a::'a::order) >= b ==> (f b::'b::order) > c ==>
+    (!!x y. x >= y ==> f x >= f y) ==> f a > c"
+by (subgoal_tac "f a >= f b", force, force)
+
+lemma xt23: "(a::'a::order) > f b ==> (b::'b::order) > c ==>
+    (!!x y. x > y ==> f x > f y) ==> a > f c"
+by (subgoal_tac "f b > f c", force, force)
+
+lemma xt24: "(a::'a::order) > b ==> (f b::'b::order) > c ==>
+    (!!x y. x > y ==> f x > f y) ==> f a > c"
+by (subgoal_tac "f a > f b", force, force)
+
+
+lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 xt10 xt11 xt12
+    xt13 xt14 xt15 xt15 xt17 xt18 xt19 xt20 xt21 xt22 xt23 xt24
+
+(* 
+  Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands
+  for the wrong thing in an Isar proof.
+
+  The extra transitivity rules can be used as follows: 
+
+lemma "(a::'a::order) > z"
+proof -
+  have "a >= b" (is "_ >= ?rhs")
+    sorry
+  also have "?rhs >= c" (is "_ >= ?rhs")
+    sorry
+  also (xtrans) have "?rhs = d" (is "_ = ?rhs")
+    sorry
+  also (xtrans) have "?rhs >= e" (is "_ >= ?rhs")
+    sorry
+  also (xtrans) have "?rhs > f" (is "_ > ?rhs")
+    sorry
+  also (xtrans) have "?rhs > z"
+    sorry
+  finally (xtrans) show ?thesis .
+qed
+
+  Alternatively, one can use "declare xtrans [trans]" and then
+  leave out the "(xtrans)" above.
+*)
+
 end