--- a/src/HOL/HOL.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/HOL.thy Fri Sep 10 20:04:14 2004 +0200
@@ -8,6 +8,7 @@
theory HOL
imports CPure
files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
+ ("antisym_setup.ML")
begin
subsection {* Primitive logic *}
@@ -737,6 +738,8 @@
lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"
by (blast intro: order_antisym)
+lemma order_antisym_conv: "(y::'a::order) <= x ==> (x <= y) = (x = y)"
+by(blast intro:order_antisym)
text {* Transitivity. *}
@@ -848,6 +851,17 @@
lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R"
by (simp add: linorder_neq_iff, blast)
+lemma linorder_antisym_conv1: "~ (x::'a::linorder) < y ==> (x <= y) = (x = y)"
+by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
+
+lemma linorder_antisym_conv2: "(x::'a::linorder) <= y ==> (~ x < y) = (x = y)"
+by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
+
+lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)"
+by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
+
+use "antisym_setup.ML";
+setup antisym_setup
subsubsection "Min and max on (linear) orders"
@@ -927,8 +941,6 @@
lemma max_commute: "!!x::'a::linorder. max x y = max y x"
apply(simp add:max_def)
-apply(rule conjI)
-apply(blast intro:order_antisym)
apply(simp add:linorder_not_le)
apply(blast dest: order_less_trans)
done
@@ -946,8 +958,6 @@
lemma min_commute: "!!x::'a::linorder. min x y = min y x"
apply(simp add:min_def)
-apply(rule conjI)
-apply(blast intro:order_antisym)
apply(simp add:linorder_not_le)
apply(blast dest: order_less_trans)
done