src/HOL/Set.thy

 (*  Title:      HOL/Set.thy
     ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1993  University of Cambridge
+    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {* Set theory for higher-order logic *}
 
 theory Set = HOL

 
 lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
   by (unfold Un_def) blast
 
 
-section {* Binary intersection -- Int *}
+subsection {* Binary intersection -- Int *}
 
 lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   by (unfold Int_def) blast
 
 lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"

 
 lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
   by simp
 
 
-section {* Set difference *}
+subsection {* Set difference *}
 
 lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
   by (unfold set_diff_def) blast
 
 lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"

    apply fast
   apply (rule LeastI2)
   apply (auto elim: monoD intro!: order_antisym)
   done
 
+
+section {* Transitivity rules for calculational reasoning *}
+
+lemma forw_subst: "a = b ==> P b ==> P a"
+  by (rule ssubst)
+
+lemma back_subst: "P a ==> a = b ==> P b"
+  by (rule subst)
+
+lemma set_rev_mp: "x:A ==> A <= B ==> x:B"
+  by (rule subsetD)
+
+lemma set_mp: "A <= B ==> x:A ==> x:B"
+  by (rule subsetD)
+
+lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
+  by (simp add: order_less_le)
+
+lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
+  by (simp add: order_less_le)
+
+lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
+  by (rule order_less_asym)
+
+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
+
+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
+
 end