# HG changeset patch
# User haftmann
# Date 1163606743 -3600
# Node ID 2b58b308300cdced3af7a06af67a6433b457792e
# Parent  17e6275e13f582598e50bee8bdceb548734cc37d
moved transitivity rules to Orderings.thy

diff -r 17e6275e13f5 -r 2b58b308300c src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Nov 15 17:05:42 2006 +0100
+++ b/src/HOL/Set.thy	Wed Nov 15 17:05:43 2006 +0100
@@ -1031,6 +1031,10 @@
 
 subsection {* Further set-theory lemmas *}
 
+instance set :: (type) order
+  by (intro_classes,
+      (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
+
 subsubsection {* Derived rules involving subsets. *}
 
 text {* @{text insert}. *}
@@ -2104,165 +2108,7 @@
 lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
   by (rule subsetD)
 
-lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
-  by (rule subst)
-
-lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
-  by (rule ssubst)
-
-lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c"
-  by (rule subst)
-
-lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c"
-  by (rule ssubst)
-
-lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
-  (!!x y. x < y ==> f x < f y) ==> f a < c"
-proof -
-  assume r: "!!x y. x < y ==> f x < f y"
-  assume "a < b" hence "f a < f b" by (rule r)
-  also assume "f b < c"
-  finally (order_less_trans) show ?thesis .
-qed
-
-lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
-  (!!x y. x < y ==> f x < f y) ==> a < f c"
-proof -
-  assume r: "!!x y. x < y ==> f x < f y"
-  assume "a < f b"
-  also assume "b < c" hence "f b < f c" by (rule r)
-  finally (order_less_trans) show ?thesis .
-qed
-
-lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
-  (!!x y. x <= y ==> f x <= f y) ==> f a < c"
-proof -
-  assume r: "!!x y. x <= y ==> f x <= f y"
-  assume "a <= b" hence "f a <= f b" by (rule r)
-  also assume "f b < c"
-  finally (order_le_less_trans) show ?thesis .
-qed
-
-lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
-  (!!x y. x < y ==> f x < f y) ==> a < f c"
-proof -
-  assume r: "!!x y. x < y ==> f x < f y"
-  assume "a <= f b"
-  also assume "b < c" hence "f b < f c" by (rule r)
-  finally (order_le_less_trans) show ?thesis .
-qed
-
-lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>
-  (!!x y. x < y ==> f x < f y) ==> f a < c"
-proof -
-  assume r: "!!x y. x < y ==> f x < f y"
-  assume "a < b" hence "f a < f b" by (rule r)
-  also assume "f b <= c"
-  finally (order_less_le_trans) show ?thesis .
-qed
-
-lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
-  (!!x y. x <= y ==> f x <= f y) ==> a < f c"
-proof -
-  assume r: "!!x y. x <= y ==> f x <= f y"
-  assume "a < f b"
-  also assume "b <= c" hence "f b <= f c" by (rule r)
-  finally (order_less_le_trans) show ?thesis .
-qed
-
-lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
-  (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
-proof -
-  assume r: "!!x y. x <= y ==> f x <= f y"
-  assume "a <= f b"
-  also assume "b <= c" hence "f b <= f c" by (rule r)
-  finally (order_trans) show ?thesis .
-qed
-
-lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==>
-  (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
-proof -
-  assume r: "!!x y. x <= y ==> f x <= f y"
-  assume "a <= b" hence "f a <= f b" by (rule r)
-  also assume "f b <= c"
-  finally (order_trans) show ?thesis .
-qed
-
-lemma ord_le_eq_subst: "a <= b ==> f b = c ==>
-  (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
-proof -
-  assume r: "!!x y. x <= y ==> f x <= f y"
-  assume "a <= b" hence "f a <= f b" by (rule r)
-  also assume "f b = c"
-  finally (ord_le_eq_trans) show ?thesis .
-qed
-
-lemma ord_eq_le_subst: "a = f b ==> b <= c ==>
-  (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
-proof -
-  assume r: "!!x y. x <= y ==> f x <= f y"
-  assume "a = f b"
-  also assume "b <= c" hence "f b <= f c" by (rule r)
-  finally (ord_eq_le_trans) show ?thesis .
-qed
-
-lemma ord_less_eq_subst: "a < b ==> f b = c ==>
-  (!!x y. x < y ==> f x < f y) ==> f a < c"
-proof -
-  assume r: "!!x y. x < y ==> f x < f y"
-  assume "a < b" hence "f a < f b" by (rule r)
-  also assume "f b = c"
-  finally (ord_less_eq_trans) show ?thesis .
-qed
-
-lemma ord_eq_less_subst: "a = f b ==> b < c ==>
-  (!!x y. x < y ==> f x < f y) ==> a < f c"
-proof -
-  assume r: "!!x y. x < y ==> f x < f y"
-  assume "a = f b"
-  also assume "b < c" hence "f b < f c" by (rule r)
-  finally (ord_eq_less_trans) show ?thesis .
-qed
-
-instance set :: (type) order
-  by (intro_classes,
-      (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
-
-text {*
-  Note that this list of rules is in reverse order of priorities.
-*}
-
 lemmas basic_trans_rules [trans] =
-  order_less_subst2
-  order_less_subst1
-  order_le_less_subst2
-  order_le_less_subst1
-  order_less_le_subst2
-  order_less_le_subst1
-  order_subst2
-  order_subst1
-  ord_le_eq_subst
-  ord_eq_le_subst
-  ord_less_eq_subst
-  ord_eq_less_subst
-  forw_subst
-  back_subst
-  rev_mp
-  mp
-  set_rev_mp
-  set_mp
-  order_neq_le_trans
-  order_le_neq_trans
-  order_less_trans
-  order_less_asym'
-  order_le_less_trans
-  order_less_le_trans
-  order_trans
-  order_antisym
-  ord_le_eq_trans
-  ord_eq_le_trans
-  ord_less_eq_trans
-  ord_eq_less_trans
-  trans
+  order_trans_rules set_rev_mp set_mp
 
 end