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