# HG changeset patch
# User wenzelm
# Date 962473868 -7200
# Node ID 672b03038110970070a7f8f26e954901f0800bd5
# Parent  298ae5f69b18dd8f0a2300da4a5dcaad33076f8d
added subst rules for ord(er), including monotonicity conditions;
name all rules;
tuned;

diff -r 298ae5f69b18 -r 672b03038110 src/HOL/Calculation.thy
--- a/src/HOL/Calculation.thy	Sat Jul 01 19:49:48 2000 +0200
+++ b/src/HOL/Calculation.thy	Sat Jul 01 19:51:08 2000 +0200
@@ -1,58 +1,191 @@
 (*  Title:      HOL/Calculation.thy
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Setup transitivity rules for calculational proofs.  Note that in the
-list below later rules have priority.
+Setup transitivity rules for calculational proofs.
 *)
 
 theory Calculation = IntArith:
 
-theorem [trans]: "[| s = t; P t |] ==> P s"                     (*  =  x  x  *)
+theorem forw_subst: "a = b ==> P b ==> P a"
   by (rule ssubst)
 
-theorem [trans]: "[| P s; s = t |] ==> P t"                     (*  x  =  x  *)
+theorem back_subst: "P a ==> a = b ==> P b"
   by (rule subst)
 
-theorems [trans] = rev_mp mp                                    (*  x --> x  *)
-                                                                (*  --> x x  *)
-
-theorems [trans] = dvd_trans                                    (* dvd dvd dvd *)
-
-theorem [trans]: "[| c:A; A <= B |] ==> c:B"
+theorem set_rev_mp: "x:A ==> A <= B ==> x:B"
   by (rule subsetD)
 
-theorem [trans]: "[| A <= B; c:A |] ==> c:B"
+theorem set_mp: "A <= B ==> x:A ==> x:B"
   by (rule subsetD)
 
-theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y"  (*  ~=  <=  < *)
-  by (simp! add: order_less_le)
+theorem order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
+  by (simp add: order_less_le)
 
-theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y"  (*  <=  ~=  < *)
-  by (simp! add: order_less_le)
+theorem order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
+  by (simp add: order_less_le)
 
-theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P"        (*  <  >  P  *)
+theorem order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
   by (rule order_less_asym)
 
-theorems [trans] = order_less_trans                             (*  <  <  <  *)
-theorems [trans] = order_le_less_trans                          (*  <= <  <  *)
-theorems [trans] = order_less_le_trans                          (*  <  <= <  *)
-theorems [trans] = order_trans                                  (*  <= <= <= *)
-theorems [trans] = order_antisym                                (*  <= >= =  *)
+theorem ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
+  by (rule subst)
 
-theorem [trans]: "[| x <= y; y = z |] ==> x <= z"               (*  <= =  <= *)
+theorem ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
+  by (rule ssubst)
+
+theorem ord_less_eq_trans: "a < b ==> b = c ==> a < c"
   by (rule subst)
 
-theorem [trans]: "[| x = y; y <= z |] ==> x <= z"               (*  =  <= <= *)
+theorem ord_eq_less_trans: "a = b ==> b < c ==> a < c"
   by (rule ssubst)
 
-theorem [trans]: "[| x < y; y = z |] ==> x < z"                 (*  <  =  <  *)
-  by (rule subst)
+theorem 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
+
+theorem 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
+
+theorem 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
+
+theorem 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
+
+theorem 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
+
+theorem 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
+
+theorem 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
+
+theorem 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
 
-theorem [trans]: "[| x = y; y < z |] ==> x < z"                 (*  =  <  <  *)
-  by (rule ssubst)
+theorem 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
+
+theorem 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
+
+theorem 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
+
+theorem 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
 
-theorems [trans] = trans                                        (*  =  =  =  *)
+text {*
+  Note that this list of rules is in reverse order of priorities.
+*}
+
+theorems 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_asym'
+  order_less_trans
+  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
 
 theorems [elim??] = sym