# HG changeset patch
# User paulson
# Date 906538509 -7200
# Node ID c55bf0487abedc3d37380fc788e1223dd8348b50
# Parent  c2bd39a2c0eec341d6d87b6c95d38467ba83d18f
a few new theorems

diff -r c2bd39a2c0ee -r c55bf0487abe src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Wed Sep 23 10:12:01 1998 +0200
+++ b/src/HOL/Ord.ML	Wed Sep 23 10:15:09 1998 +0200
@@ -25,6 +25,8 @@
 
 section "Orders";
 
+(** Reflexivity **)
+
 Addsimps [order_refl];
 
 (*This form is useful with the classical reasoner*)
@@ -44,6 +46,35 @@
 by (blast_tac (claset() addSIs [order_refl]) 1);
 qed "order_le_less";
 
+(** Asymmetry **)
+
+Goal "(x::'a::order) < y ==> ~ (y<x)";
+by (asm_full_simp_tac (simpset() addsimps [order_less_le, order_antisym]) 1);
+qed "order_less_not_sym";
+
+(* [| n<m;  ~P ==> m<n |] ==> P *)
+bind_thm ("order_less_asym", order_less_not_sym RS swap);
+
+
+(** Useful for simplification, but too risky to include by default. **)
+
+Goal "(x::'a::order) < y ==>  (~ y < x) = True";
+by (blast_tac (claset() addEs [order_less_asym]) 1);
+qed "order_less_imp_not_less";
+
+Goal "(x::'a::order) < y ==>  (y < x --> P) = True";
+by (blast_tac (claset() addEs [order_less_asym]) 1);
+qed "order_less_imp_triv";
+
+Goal "(x::'a::order) < y ==>  (x = y) = False";
+by Auto_tac;
+qed "order_less_imp_not_eq";
+
+Goal "(x::'a::order) < y ==>  (y = x) = False";
+by Auto_tac;
+qed "order_less_imp_not_eq2";
+
+
 (** min **)
 
 val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";