# HG changeset patch
# User nipkow
# Date 1074035584 -3600
# Node ID 67e2e96bfe361840fb2e527e2c300c3340aa4aa7
# Parent  988aa464859722e060241ef33c57e7a61ee999fd
Told linear arithmetic package about injections "real" from nat/int into real.

diff -r 988aa4648597 -r 67e2e96bfe36 src/HOL/Hyperreal/IntFloor.ML
--- a/src/HOL/Hyperreal/IntFloor.ML	Tue Jan 13 10:37:52 2004 +0100
+++ b/src/HOL/Hyperreal/IntFloor.ML	Wed Jan 14 00:13:04 2004 +0100
@@ -92,10 +92,6 @@
 Goal "0 <= r ==> EX n. real (n) <= r & r < real (Suc n)";
 by (dtac reals_Archimedean6 1);
 by Auto_tac;
-by (res_inst_tac [("x","n - 1")] exI 1);
-by (subgoal_tac "0 < n" 1);
-by (dtac order_le_less_trans 2);
-by Auto_tac;
 qed "reals_Archimedean6a";
 
 Goal "0 <= r ==> EX n. real n <= r & r < real ((n::int) + 1)";
@@ -136,11 +132,6 @@
 by (cut_inst_tac [("r","r")] real_lb_ub_int 1 THEN Step_tac 1);
 by (rtac theI2 1);
 by Auto_tac;
-by (blast_tac (claset() addIs [lemma_floor]) 1);
-by (ALLGOALS(dres_inst_tac [("x","n")] spec) THEN Auto_tac);
-by (force_tac (claset() addDs [lemma_floor],simpset()) 1);
-by (dtac (real_of_int_le_iff RS iffD2) 1);
-by (blast_tac (claset() addIs [real_le_trans]) 1);
 qed "real_of_int_floor_le";
 Addsimps [real_of_int_floor_le];
 
@@ -169,8 +160,6 @@
 by (cut_inst_tac [("r","x")] real_lb_ub_int 1 THEN etac exE 1);
 by (rtac theI2 1);
 by (auto_tac (claset() addIs [lemma_floor],simpset()));
-by (force_tac (claset() addDs [lemma_floor],simpset()) 1);
-by (force_tac (claset() addDs [lemma_floor2],simpset()) 1);
 qed "real_of_int_floor_cancel";
 Addsimps [real_of_int_floor_cancel];
 
@@ -212,7 +201,6 @@
 by (cut_inst_tac [("r","r")] real_lb_ub_int 1 THEN Step_tac 1);
 by (rtac theI2 1);
 by (auto_tac (claset() addIs [lemma_floor],simpset()));
-by (force_tac (claset() addDs [lemma_floor],simpset()) 1);
 qed "real_of_int_floor_ge_diff_one";
 Addsimps [real_of_int_floor_ge_diff_one];
 
diff -r 988aa4648597 -r 67e2e96bfe36 src/HOL/Hyperreal/NthRoot.thy
--- a/src/HOL/Hyperreal/NthRoot.thy	Tue Jan 13 10:37:52 2004 +0100
+++ b/src/HOL/Hyperreal/NthRoot.thy	Wed Jan 14 00:13:04 2004 +0100
@@ -122,8 +122,7 @@
 
 lemma real_mult_add_one_minus_ge_zero:
      "0 < r ==>  0 <= r*(1 + -inverse(real (Suc n)))"
-apply (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff) 
-apply (simp add: real_of_nat_Suc) 
+apply (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff)
 done
 
 lemma lemma_nth_realpow_isLub_le:
diff -r 988aa4648597 -r 67e2e96bfe36 src/HOL/Hyperreal/SEQ.ML
--- a/src/HOL/Hyperreal/SEQ.ML	Tue Jan 13 10:37:52 2004 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML	Wed Jan 14 00:13:04 2004 +0100
@@ -1150,9 +1150,6 @@
 by (cut_inst_tac [("x","y")] reals_Archimedean2 1);
 by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
 by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
-by (subgoal_tac "y < real na" 1);
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [order_less_le_trans]) 1);  
 qed "LIMSEQ_inverse_real_of_nat";
 
 Goal "(%n. inverse(real(Suc n))) ----NS> 0";
diff -r 988aa4648597 -r 67e2e96bfe36 src/HOL/Hyperreal/Transcendental.ML
--- a/src/HOL/Hyperreal/Transcendental.ML	Tue Jan 13 10:37:52 2004 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML	Wed Jan 14 00:13:04 2004 +0100
@@ -1601,8 +1601,6 @@
 by (ALLGOALS(Asm_simp_tac));
 by (TRYALL(rtac real_less_trans));
 by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc] delsimps [fact_Suc]));
-by (res_inst_tac [("y","0")] order_less_le_trans 1);
-by (ALLGOALS(Asm_simp_tac));
 qed "sin_gt_zero";
 
 Goal "[|0 < x; x < 2 |] ==> 0 < sin x";
diff -r 988aa4648597 -r 67e2e96bfe36 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jan 13 10:37:52 2004 +0100
+++ b/src/HOL/IsaMakefile	Wed Jan 14 00:13:04 2004 +0100
@@ -153,6 +153,7 @@
   Hyperreal/HyperArith.thy Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \
   Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
   Hyperreal/HyperOrd.thy Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
+  Hyperreal/IntFloor.thy Hyperreal/IntFloor.ML\
   Hyperreal/Lim.ML Hyperreal/Lim.thy  Hyperreal/Log.ML Hyperreal/Log.thy\
   Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\
   Hyperreal/NatStar.ML Hyperreal/NatStar.thy\
diff -r 988aa4648597 -r 67e2e96bfe36 src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Tue Jan 13 10:37:52 2004 +0100
+++ b/src/HOL/Real/real_arith.ML	Wed Jan 14 00:13:04 2004 +0100
@@ -267,7 +267,17 @@
 (* reduce contradictory <= to False *)
 val simps = [True_implies_equals,
              inst "a" "(number_of ?v)::real" right_distrib,
-             divide_1,times_divide_eq_right,times_divide_eq_left];
+             divide_1,times_divide_eq_right,times_divide_eq_left,
+         real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, real_of_nat_mult,
+         real_of_int_zero, real_of_one, real_of_int_add RS sym,
+         real_of_int_minus RS sym, real_of_int_diff RS sym,
+         real_of_int_mult RS sym];
+
+val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2,
+                    real_of_int_inject RS iffD2];
+
+val nat_inj_thms = [real_of_nat_le_iff RS iffD2, real_of_nat_less_iff RS iffD2,
+                    real_of_nat_inject RS iffD2];
 
 in
 
@@ -279,11 +289,13 @@
  [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    {add_mono_thms = add_mono_thms @ add_mono_thms_real,
     mult_mono_thms = mult_mono_thms @ real_mult_mono_thms,
-    inj_thms = inj_thms, (*FIXME: add real*)
-    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the reals are dense!*)
+    inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
+    lessD = lessD,  (*Can't change lessD: the reals are dense!*)
     simpset = simpset addsimps add_rules
                       addsimps simps
                       addsimprocs simprocs}),
+  arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT),
+  arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT),
   arith_discrete ("RealDef.real",false),
   Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];