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