# HG changeset patch # User paulson # Date 1046959396 -3600 # Node ID 6d1bb3059818ec1f67c182f99ca8434a4cfb4322 # Parent 2584233cf3ef9572b398af04449dc588bd70a203 new logical equivalences diff -r 2584233cf3ef -r 6d1bb3059818 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Thu Mar 06 15:02:51 2003 +0100 +++ b/src/HOL/SetInterval.thy Thu Mar 06 15:03:16 2003 +0100 @@ -33,7 +33,8 @@ atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") "{l..u} == {l..} Int {..u}" -(* Setup of transitivity reasoner *) + +subsection {* Setup of transitivity reasoner *} ML {* @@ -73,156 +74,158 @@ {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac)) *} {* simple transitivity reasoner *} -(*** lessThan ***) -lemma lessThan_iff: "(i: lessThan k) = (i atLeast y) = (y \ (x::'a::order))" +by (blast intro: order_trans) + +lemma atLeast_eq_iff [iff]: + "(atLeast x = atLeast y) = (x = (y::'a::linorder))" +by (blast intro: order_antisym order_trans) + +lemma greaterThan_subset_iff [iff]: + "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))" +apply (auto simp add: greaterThan_def) + apply (subst linorder_not_less [symmetric], blast) +apply (blast intro: order_le_less_trans) +done + +lemma greaterThan_eq_iff [iff]: + "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" +apply (rule iffI) + apply (erule equalityE) + apply (simp add: greaterThan_subset_iff order_antisym, simp) +done + +lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))" +by (blast intro: order_trans) + +lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" +by (blast intro: order_antisym order_trans) + +lemma lessThan_subset_iff [iff]: + "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))" +apply (auto simp add: lessThan_def) + apply (subst linorder_not_less [symmetric], blast) +apply (blast intro: order_less_le_trans) +done + +lemma lessThan_eq_iff [iff]: + "(lessThan x = lessThan y) = (x = (y::'a::linorder))" +apply (rule iffI) + apply (erule equalityE) + apply (simp add: lessThan_subset_iff order_antisym, simp) done -(*** Combined properties ***) +subsection {*Combined properties*} lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" -apply (blast intro: order_antisym) -done +by (blast intro: order_antisym) -(*** Two-sided intervals ***) +subsection {*Two-sided intervals*} (* greaterThanLessThan *) @@ -252,7 +255,8 @@ If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int seems to take forever (more than one hour). *) -(*** The following lemmas are useful with the summation operator setsum ***) +subsection {*Lemmas useful with the summation operator setsum*} + (* For examples, see Algebra/poly/UnivPoly.thy *) (** Disjoint Unions **)