# HG changeset patch
# User paulson
# Date 1046959371 -3600
# Node ID 2584233cf3ef9572b398af04449dc588bd70a203
# Parent  12ffc04fee2207bd321b167c0f7aceb711ece2e2
new simprule for int (nat n)
and consequential changes

diff -r 12ffc04fee22 -r 2584233cf3ef src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Thu Mar 06 12:22:28 2003 +0100
+++ b/src/HOL/Integ/IntArith.thy	Thu Mar 06 15:02:51 2003 +0100
@@ -14,6 +14,9 @@
     "(abs (z::int) = w) = (z = w \<and> 0 <= z \<or> z = -w \<and> z < 0)"
   by (auto simp add: zabs_def)
 
+lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
+  by simp
+
 lemma split_nat[arith_split]:
   "P(nat(i::int)) = ((ALL n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   (is "?P = (?L & ?R)")
@@ -107,3 +110,4 @@
 done
 
 end
+
diff -r 12ffc04fee22 -r 2584233cf3ef src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Thu Mar 06 12:22:28 2003 +0100
+++ b/src/HOL/Real/PReal.ML	Thu Mar 06 15:02:51 2003 +0100
@@ -122,10 +122,11 @@
 
 Goal "!!(x::prat). {xa. xa < x} = {x. x < y} ==> x = y";
 by (cut_inst_tac [("q1.0","x"),("q2.0","y")] prat_linear 1);
-by Auto_tac;
+by Safe_tac;
 by (dtac prat_dense 2 THEN etac exE 2);
 by (dtac prat_dense 1 THEN etac exE 1);
-by (auto_tac (claset() addDs [prat_less_not_sym], simpset()));
+by (blast_tac (claset() addDs [prat_less_not_sym]) 1); 
+by (blast_tac (claset() addDs [prat_less_not_sym]) 1); 
 qed "lemma_prat_set_eq";
 
 Goal "inj(preal_of_prat)";
diff -r 12ffc04fee22 -r 2584233cf3ef src/HOL/Real/RealInt.ML
--- a/src/HOL/Real/RealInt.ML	Thu Mar 06 12:22:28 2003 +0100
+++ b/src/HOL/Real/RealInt.ML	Thu Mar 06 15:02:51 2003 +0100
@@ -95,8 +95,7 @@
 qed "real_of_int_real_of_nat";
 
 Goal "~neg z ==> real (nat z) = real z";
-by (asm_simp_tac (simpset() addsimps [not_neg_nat,
-				      real_of_int_real_of_nat RS sym]) 1);
+by (asm_full_simp_tac (simpset() addsimps [not_neg_eq_ge_0, real_of_int_real_of_nat RS sym]) 1);
 qed "real_of_nat_real_of_int";
 
 Goal "(real x = 0) = (x = int 0)";