minor adjustments
authorpaulson <lp15@cam.ac.uk>
Wed Jan 29 15:40:33 2014 +0000 (2014-01-29)
changeset 551618eb891539804
parent 55159 608c157d743d
child 55162 09818414b6a5
minor adjustments
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Residues.thy
     1.1 --- a/src/HOL/Number_Theory/Cong.thy	Wed Jan 29 12:51:37 2014 +0000
     1.2 +++ b/src/HOL/Number_Theory/Cong.thy	Wed Jan 29 15:40:33 2014 +0000
     1.3 @@ -593,8 +593,7 @@
     1.4  lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
     1.5    apply (cases "a = 0")
     1.6    apply force
     1.7 -  apply (frule cong_solve_nat [of a n])
     1.8 -  apply auto
     1.9 +  apply (metis cong_solve_nat)
    1.10    done
    1.11  
    1.12  lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
    1.13 @@ -602,23 +601,31 @@
    1.14    apply auto
    1.15    apply (cases "n \<ge> 0")
    1.16    apply auto
    1.17 -  apply (frule cong_solve_int [of a n])
    1.18 -  apply auto
    1.19 +  apply (metis cong_solve_int)
    1.20 +  done
    1.21 +
    1.22 +lemma coprime_iff_invertible_nat: "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
    1.23 +  apply (auto intro: cong_solve_coprime_nat)
    1.24 +  apply (metis cong_Suc_0_nat cong_solve_nat gcd_nat.left_neutral)
    1.25 +  apply (metis One_nat_def cong_gcd_eq_nat coprime_lmult_nat 
    1.26 +      gcd_lcm_complete_lattice_nat.inf_bot_right gcd_nat.commute)
    1.27    done
    1.28  
    1.29 -lemma coprime_iff_invertible_nat: "m > Suc 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
    1.30 -  apply (auto intro: cong_solve_coprime_nat)
    1.31 -  apply (metis cong_solve_nat gcd_nat.left_neutral nat_neq_iff)
    1.32 -  apply (unfold cong_nat_def, auto intro: invertible_coprime_nat [unfolded One_nat_def])
    1.33 +lemma coprime_iff_invertible_int: "m > (0::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
    1.34 +  apply (auto intro: cong_solve_coprime_int)
    1.35 +  apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd_int.commute gcd_red_int)
    1.36    done
    1.37  
    1.38 -lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
    1.39 -  apply (auto intro: cong_solve_coprime_int)
    1.40 -  apply (unfold cong_int_def)
    1.41 -  apply (auto intro: invertible_coprime_int)
    1.42 +lemma coprime_iff_invertible'_nat: "m > 0 \<Longrightarrow> coprime a m =
    1.43 +    (EX x. 0 \<le> x & x < m & [a * x = Suc 0] (mod m))"
    1.44 +  apply (subst coprime_iff_invertible_nat)
    1.45 +  apply auto
    1.46 +  apply (auto simp add: cong_nat_def)
    1.47 +  apply (rule_tac x = "x mod m" in exI)
    1.48 +  apply (metis mod_less_divisor mod_mult_right_eq)
    1.49    done
    1.50  
    1.51 -lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
    1.52 +lemma coprime_iff_invertible'_int: "m > (0::int) \<Longrightarrow> coprime a m =
    1.53      (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
    1.54    apply (subst coprime_iff_invertible_int)
    1.55    apply auto
    1.56 @@ -627,7 +634,6 @@
    1.57    apply (auto simp add: mod_mult_right_eq [symmetric])
    1.58    done
    1.59  
    1.60 -
    1.61  lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
    1.62      [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
    1.63    apply (cases "y \<le> x")
     2.1 --- a/src/HOL/Number_Theory/Residues.thy	Wed Jan 29 12:51:37 2014 +0000
     2.2 +++ b/src/HOL/Number_Theory/Residues.thy	Wed Jan 29 15:40:33 2014 +0000
     2.3 @@ -108,7 +108,7 @@
     2.4    apply (subgoal_tac "x ~= 0")
     2.5    apply auto
     2.6    apply (subst (asm) coprime_iff_invertible'_int)
     2.7 -  apply (rule m_gt_one)
     2.8 +  apply arith
     2.9    apply (auto simp add: cong_int_def mult_commute)
    2.10    done
    2.11  
    2.12 @@ -453,7 +453,7 @@
    2.13    apply (subst fact_altdef_int, simp)
    2.14    apply (subst cong_int_def)
    2.15    apply simp
    2.16 -  apply arith
    2.17 +  apply presburger
    2.18    apply (rule residues_prime.wilson_theorem1)
    2.19    apply (rule residues_prime.intro)
    2.20    apply auto