# HG changeset patch
# User paulson
# Date 977235623 -3600
# Node ID f02834001fca3e9b78bb6412febe21cb230589cc
# Parent  58c3c00d9fdf44bca06fafe207d094eb7494d1ab
re-orienting equations with 0, 1, 2 on the lhs

diff -r 58c3c00d9fdf -r f02834001fca src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Tue Dec 19 15:19:12 2000 +0100
+++ b/src/HOL/NatDef.ML	Tue Dec 19 15:20:23 2000 +0100
@@ -521,3 +521,24 @@
 by (Force_tac 1);
 by (force_tac (claset(), simpset() addsimps [less_eq,not_le_iff_less]) 1);
 qed "nonempty_has_least";
+
+(** Re-orientation of the equations 0=x and Suc n = x. *
+
+  The condition "True" is a hack to prevent looping for e.g. Suc m = Suc n.
+  Conditional rewrite rules are tried after unconditional ones.
+**)
+
+Goal "True ==> (0 = x) = (x = (0::nat))";
+by Auto_tac;  
+qed "zero_reorient";
+Addsimps [zero_reorient];
+
+Goal "True ==> (1 = x) = (x = 1)";
+by Auto_tac;  
+qed "one_reorient";
+Addsimps [one_reorient];
+
+Goal "True ==> (2 = x) = (x = 2)";
+by Auto_tac;  
+qed "two_reorient";
+Addsimps [two_reorient];