new simprule for int (nat n)
authorpaulson
Thu Mar 06 15:02:51 2003 +0100 (2003-03-06)
changeset 138492584233cf3ef
parent 13848 12ffc04fee22
child 13850 6d1bb3059818
new simprule for int (nat n)
and consequential changes
src/HOL/Integ/IntArith.thy
src/HOL/Real/PReal.ML
src/HOL/Real/RealInt.ML
     1.1 --- a/src/HOL/Integ/IntArith.thy	Thu Mar 06 12:22:28 2003 +0100
     1.2 +++ b/src/HOL/Integ/IntArith.thy	Thu Mar 06 15:02:51 2003 +0100
     1.3 @@ -14,6 +14,9 @@
     1.4      "(abs (z::int) = w) = (z = w \<and> 0 <= z \<or> z = -w \<and> z < 0)"
     1.5    by (auto simp add: zabs_def)
     1.6  
     1.7 +lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
     1.8 +  by simp
     1.9 +
    1.10  lemma split_nat[arith_split]:
    1.11    "P(nat(i::int)) = ((ALL n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
    1.12    (is "?P = (?L & ?R)")
    1.13 @@ -107,3 +110,4 @@
    1.14  done
    1.15  
    1.16  end
    1.17 +
     2.1 --- a/src/HOL/Real/PReal.ML	Thu Mar 06 12:22:28 2003 +0100
     2.2 +++ b/src/HOL/Real/PReal.ML	Thu Mar 06 15:02:51 2003 +0100
     2.3 @@ -122,10 +122,11 @@
     2.4  
     2.5  Goal "!!(x::prat). {xa. xa < x} = {x. x < y} ==> x = y";
     2.6  by (cut_inst_tac [("q1.0","x"),("q2.0","y")] prat_linear 1);
     2.7 -by Auto_tac;
     2.8 +by Safe_tac;
     2.9  by (dtac prat_dense 2 THEN etac exE 2);
    2.10  by (dtac prat_dense 1 THEN etac exE 1);
    2.11 -by (auto_tac (claset() addDs [prat_less_not_sym], simpset()));
    2.12 +by (blast_tac (claset() addDs [prat_less_not_sym]) 1); 
    2.13 +by (blast_tac (claset() addDs [prat_less_not_sym]) 1); 
    2.14  qed "lemma_prat_set_eq";
    2.15  
    2.16  Goal "inj(preal_of_prat)";
     3.1 --- a/src/HOL/Real/RealInt.ML	Thu Mar 06 12:22:28 2003 +0100
     3.2 +++ b/src/HOL/Real/RealInt.ML	Thu Mar 06 15:02:51 2003 +0100
     3.3 @@ -95,8 +95,7 @@
     3.4  qed "real_of_int_real_of_nat";
     3.5  
     3.6  Goal "~neg z ==> real (nat z) = real z";
     3.7 -by (asm_simp_tac (simpset() addsimps [not_neg_nat,
     3.8 -				      real_of_int_real_of_nat RS sym]) 1);
     3.9 +by (asm_full_simp_tac (simpset() addsimps [not_neg_eq_ge_0, real_of_int_real_of_nat RS sym]) 1);
    3.10  qed "real_of_nat_real_of_int";
    3.11  
    3.12  Goal "(real x = 0) = (x = int 0)";