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