# HG changeset patch
# User wenzelm
# Date 1007595479 -3600
# Node ID d6913de7655f17507f7d265e687bf30757ec17ba
# Parent  b20a37eb8338087334a251a51204a2edfdae4323
this material already part of HOL/Set.thy;

diff -r b20a37eb8338 -r d6913de7655f src/HOL/Calculation.thy
--- a/src/HOL/Calculation.thy	Wed Dec 05 20:58:00 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,191 +0,0 @@
-(*  Title:      HOL/Calculation.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
-
-Setup transitivity rules for calculational proofs.
-*)
-
-theory Calculation = IntArith:
-
-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
-  dvd_trans
-  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
-  transitive
-  trans
-
-end