merged
authorhuffman
Mon, 14 Nov 2011 09:25:05 +0100
changeset 45482 8f32682f78fe
parent 45481 cf937a9ce051 (diff)
parent 45479 3387d482e0a9 (current diff)
child 45483 34d07cf7d207
child 45484 23871e17dddb
child 45498 2dc373f1867a
merged
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Nov 13 20:28:22 2011 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Nov 14 09:25:05 2011 +0100
@@ -1178,15 +1178,6 @@
   from *[OF this] show thesis by blast
 qed
 
-lemma float_remove_real_numeral[simp]: "(number_of k :: float) = (number_of k :: real)"
-proof -
-  have "(number_of k :: float) = real k"
-    unfolding number_of_float_def real_of_float_def pow2_def by auto
-  also have "\<dots> = (number_of k :: int)"
-    by (simp add: number_of_is_id)
-  finally show ?thesis by auto
-qed
-
 lemma cos_periodic_nat[simp]: fixes n :: nat shows "cos (x + n * (2 * pi)) = cos x"
 proof (induct n arbitrary: x)
   case (Suc n)
--- a/src/HOL/Old_Number_Theory/Euler.thy	Sun Nov 13 20:28:22 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Mon Nov 14 09:25:05 2011 +0100
@@ -85,7 +85,7 @@
   apply (auto simp add: MultInvPair_def)
   apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")
   apply auto
-  apply (metis MultInvPair_distinct Pls_def StandardRes_def aux number_of_is_id one_is_num_one)
+  apply (metis MultInvPair_distinct StandardRes_def aux)
   done
 
 
@@ -227,7 +227,7 @@
 lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
     ~(QuadRes p x) |] ==> 
       [x^(nat (((p) - 1) div 2)) = -1](mod p)"
-  by (metis Wilson_Russ number_of_is_id zcong_sym zcong_trans zfact_prop)
+  by (metis Wilson_Russ zcong_sym zcong_trans zfact_prop)
 
 text {* \medskip Prove another part of Euler Criterion: *}
 
@@ -280,13 +280,13 @@
   apply (subgoal_tac "p \<in> zOdd")
   apply (auto simp add: QuadRes_def)
    prefer 2 
-   apply (metis number_of_is_id numeral_1_eq_1 zprime_zOdd_eq_grt_2)
+   apply (metis zprime_zOdd_eq_grt_2)
   apply (frule aux__1, auto)
   apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)
   apply (auto simp add: zpower_zpower) 
   apply (rule zcong_trans)
   apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
-  apply (metis Little_Fermat even_div_2_prop2 mult_Bit0 number_of_is_id odd_minus_one_even one_is_num_one mult_1 aux__2)
+  apply (metis Little_Fermat even_div_2_prop2 odd_minus_one_even mult_1 aux__2)
   done
 
 
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 13 20:28:22 2011 +0100
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Mon Nov 14 09:25:05 2011 +0100
@@ -142,7 +142,7 @@
     prefer 2
     apply (subst zdvd_iff_zgcd [symmetric])
      apply (rule_tac [4] zgcd_zcong_zgcd)
-       apply (simp_all add: zcong_sym)
+       apply (simp_all (no_asm_use) add: zcong_sym)
   done