# HG changeset patch
# User wenzelm
# Date 1004734918 -3600
# Node ID a243730869083679de912a6eaa11c998e7a05e5e
# Parent  abe9b7c6016e5957af74b3ed3a69f3a48abe55f7
theory Calculation move to Set;

diff -r abe9b7c6016e -r a24373086908 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Nov 02 22:01:07 2001 +0100
+++ b/src/HOL/IsaMakefile	Fri Nov 02 22:01:58 2001 +0100
@@ -76,7 +76,7 @@
   $(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \
   $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
   $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
-  $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML Calculation.thy \
+  $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
   Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides.ML \
   Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
   Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
diff -r abe9b7c6016e -r a24373086908 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Fri Nov 02 22:01:07 2001 +0100
+++ b/src/HOL/PreList.thy	Fri Nov 02 22:01:58 2001 +0100
@@ -9,7 +9,10 @@
 
 theory PreList =
   Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
-  Relation_Power + Calculation + SVC_Oracle:
+  Relation_Power + SVC_Oracle:
+
+(*belongs to theory Divides*)
+declare dvd_trans [trans]
 
 (*belongs to theory Wellfounded_Recursion*)
 declare wf_induct [induct set: wf]
diff -r abe9b7c6016e -r a24373086908 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Nov 02 22:01:07 2001 +0100
+++ b/src/HOL/Set.thy	Fri Nov 02 22:01:58 2001 +0100
@@ -1,7 +1,7 @@
 (*  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 *}
@@ -575,7 +575,7 @@
   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
@@ -593,7 +593,7 @@
   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
@@ -904,4 +904,185 @@
   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