src/HOL/GCD.thy
changeset 61944 5d06ecfdb472
parent 61929 b8e242e52c97
child 61954 1d43f86f48be
     1.1 --- a/src/HOL/GCD.thy	Sun Dec 27 22:07:17 2015 +0100
     1.2 +++ b/src/HOL/GCD.thy	Mon Dec 28 01:26:34 2015 +0100
     1.3 @@ -605,14 +605,14 @@
     1.4  definition
     1.5    gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
     1.6  where
     1.7 -  "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
     1.8 +  "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
     1.9  
    1.10  definition
    1.11    lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
    1.12  where
    1.13 -  "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
    1.14 +  "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
    1.15  
    1.16 -instance proof qed
    1.17 +instance ..
    1.18  
    1.19  end
    1.20  
    1.21 @@ -676,16 +676,16 @@
    1.22    "gcd x (- numeral n :: int) = gcd x (numeral n)"
    1.23    by (fact gcd_neg2_int)
    1.24  
    1.25 -lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
    1.26 +lemma abs_gcd_int[simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
    1.27  by(simp add: gcd_int_def)
    1.28  
    1.29 -lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)"
    1.30 +lemma gcd_abs_int: "gcd (x::int) y = gcd \<bar>x\<bar> \<bar>y\<bar>"
    1.31  by (simp add: gcd_int_def)
    1.32  
    1.33 -lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
    1.34 +lemma gcd_abs1_int[simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
    1.35  by (metis abs_idempotent gcd_abs_int)
    1.36  
    1.37 -lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
    1.38 +lemma gcd_abs2_int[simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
    1.39  by (metis abs_idempotent gcd_abs_int)
    1.40  
    1.41  lemma gcd_cases_int:
    1.42 @@ -695,7 +695,7 @@
    1.43        and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
    1.44        and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
    1.45    shows "P (gcd x y)"
    1.46 -by (insert assms, auto, arith)
    1.47 +  by (insert assms, auto, arith)
    1.48  
    1.49  lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
    1.50    by (simp add: gcd_int_def)
    1.51 @@ -706,17 +706,17 @@
    1.52  lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
    1.53    by (simp add: lcm_int_def)
    1.54  
    1.55 -lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)"
    1.56 +lemma lcm_abs_int: "lcm (x::int) y = lcm \<bar>x\<bar> \<bar>y\<bar>"
    1.57    by (simp add: lcm_int_def)
    1.58  
    1.59 -lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
    1.60 -by(simp add:lcm_int_def)
    1.61 +lemma abs_lcm_int [simp]: "\<bar>lcm i j::int\<bar> = lcm i j"
    1.62 +  by (simp add:lcm_int_def)
    1.63  
    1.64 -lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"
    1.65 -by (metis abs_idempotent lcm_int_def)
    1.66 +lemma lcm_abs1_int[simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
    1.67 +  by (metis abs_idempotent lcm_int_def)
    1.68  
    1.69 -lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
    1.70 -by (metis abs_idempotent lcm_int_def)
    1.71 +lemma lcm_abs2_int[simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
    1.72 +  by (metis abs_idempotent lcm_int_def)
    1.73  
    1.74  lemma lcm_cases_int:
    1.75    fixes x :: int and y
    1.76 @@ -735,13 +735,13 @@
    1.77    by simp
    1.78  
    1.79  (* was igcd_0, etc. *)
    1.80 -lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
    1.81 +lemma gcd_0_int [simp]: "gcd (x::int) 0 = \<bar>x\<bar>"
    1.82    by (unfold gcd_int_def, auto)
    1.83  
    1.84  lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
    1.85    by simp
    1.86  
    1.87 -lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
    1.88 +lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = \<bar>x\<bar>"
    1.89    by (unfold gcd_int_def, auto)
    1.90  
    1.91  lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
    1.92 @@ -764,7 +764,7 @@
    1.93  lemma gcd_idem_nat: "gcd (x::nat) x = x"
    1.94  by simp
    1.95  
    1.96 -lemma gcd_idem_int: "gcd (x::int) x = abs x"
    1.97 +lemma gcd_idem_int: "gcd (x::int) x = \<bar>x\<bar>"
    1.98  by (auto simp add: gcd_int_def)
    1.99  
   1.100  declare gcd_nat.simps [simp del]
   1.101 @@ -882,10 +882,10 @@
   1.102  lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   1.103    by (fact gcd_nat.absorb2)
   1.104  
   1.105 -lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
   1.106 +lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = \<bar>x\<bar>"
   1.107    by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
   1.108  
   1.109 -lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
   1.110 +lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = \<bar>y\<bar>"
   1.111    by (metis gcd_proj1_if_dvd_int gcd_commute_int)
   1.112  
   1.113  text \<open>
   1.114 @@ -900,7 +900,7 @@
   1.115    apply (simp_all add: gcd_non_0_nat)
   1.116  done
   1.117  
   1.118 -lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   1.119 +lemma gcd_mult_distrib_int: "\<bar>k::int\<bar> * gcd m n = gcd (k * m) (k * n)"
   1.120    apply (subst (1 2) gcd_abs_int)
   1.121    apply (subst (1 2) abs_mult)
   1.122    apply (rule gcd_mult_distrib_nat [transferred])
   1.123 @@ -1064,8 +1064,8 @@
   1.124  lemma finite_divisors_int[simp]:
   1.125    assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
   1.126  proof-
   1.127 -  have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
   1.128 -  hence "finite{d. abs d <= abs i}" by simp
   1.129 +  have "{d. \<bar>d\<bar> <= \<bar>i\<bar>} = {- \<bar>i\<bar> .. \<bar>i\<bar>}" by(auto simp:abs_if)
   1.130 +  hence "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}" by simp
   1.131    from finite_subset[OF _ this] show ?thesis using assms
   1.132      by (simp add: dvd_imp_le_int subset_iff)
   1.133  qed
   1.134 @@ -1076,7 +1076,7 @@
   1.135  apply simp
   1.136  done
   1.137  
   1.138 -lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
   1.139 +lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
   1.140  apply(rule antisym)
   1.141   apply(rule Max_le_iff [THEN iffD2])
   1.142    apply (auto intro: abs_le_D1 dvd_imp_le_int)
   1.143 @@ -1507,7 +1507,7 @@
   1.144    by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1)
   1.145  
   1.146  lemma coprime_common_divisor_int:
   1.147 -  "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> abs x = 1"
   1.148 +  "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
   1.149    using gcd_greatest_iff [of x a b] by auto
   1.150  
   1.151  lemma coprime_divisors_nat:
   1.152 @@ -1763,7 +1763,7 @@
   1.153  
   1.154  subsection \<open>LCM properties\<close>
   1.155  
   1.156 -lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
   1.157 +lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   1.158    by (simp add: lcm_int_def lcm_nat_def zdiv_int
   1.159      of_nat_mult gcd_int_def)
   1.160  
   1.161 @@ -1771,7 +1771,7 @@
   1.162    unfolding lcm_nat_def
   1.163    by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
   1.164  
   1.165 -lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
   1.166 +lemma prod_gcd_lcm_int: "\<bar>m::int\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
   1.167    unfolding lcm_int_def gcd_int_def
   1.168    apply (subst int_mult [symmetric])
   1.169    apply (subst prod_gcd_lcm_nat [symmetric])
   1.170 @@ -1871,7 +1871,7 @@
   1.171    apply auto
   1.172  done
   1.173  
   1.174 -lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
   1.175 +lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
   1.176    apply (rule sym)
   1.177    apply (subst lcm_unique_int [symmetric])
   1.178    apply auto
   1.179 @@ -1880,7 +1880,7 @@
   1.180  lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
   1.181  by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
   1.182  
   1.183 -lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
   1.184 +lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
   1.185  by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
   1.186  
   1.187  lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
   1.188 @@ -1889,10 +1889,10 @@
   1.189  lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
   1.190  by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
   1.191  
   1.192 -lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
   1.193 +lemma lcm_proj1_iff_int[simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
   1.194  by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
   1.195  
   1.196 -lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
   1.197 +lemma lcm_proj2_iff_int[simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
   1.198  by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
   1.199  
   1.200  lemma (in semiring_gcd) comp_fun_idem_gcd:
   1.201 @@ -2162,7 +2162,7 @@
   1.202    "Lcm (insert (n::int) N) = lcm n (Lcm N)"
   1.203    by (fact Lcm_insert)
   1.204  
   1.205 -lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat (abs x) dvd nat (abs y)"
   1.206 +lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>"
   1.207    by (fact dvd_int_unfold_dvd_nat)
   1.208  
   1.209  lemma dvd_Lcm_int [simp]:
   1.210 @@ -2223,7 +2223,7 @@
   1.211    "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   1.212  by transfer(fact gcd_code_int)
   1.213  
   1.214 -lemma lcm_code_integer [code]: "lcm (a::integer) b = (abs a) * (abs b) div gcd a b"
   1.215 +lemma lcm_code_integer [code]: "lcm (a::integer) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   1.216  by transfer(fact lcm_altdef_int)
   1.217  
   1.218  end