src/HOL/GCD.thy
changeset 31814 7c122634da81
parent 31813 4df828bbc411
child 31952 40501bb2d57c
     1.1 --- a/src/HOL/GCD.thy	Fri Jun 26 10:46:33 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Fri Jun 26 19:44:39 2009 +0200
     1.3 @@ -214,6 +214,15 @@
     1.4  lemma int_lcm_abs: "lcm (x::int) y = lcm (abs x) (abs y)"
     1.5    by (simp add: lcm_int_def)
     1.6  
     1.7 +lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
     1.8 +by(simp add:lcm_int_def)
     1.9 +
    1.10 +lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"
    1.11 +by (metis abs_idempotent lcm_int_def)
    1.12 +
    1.13 +lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
    1.14 +by (metis abs_idempotent lcm_int_def)
    1.15 +
    1.16  lemma int_lcm_cases:
    1.17    fixes x :: int and y
    1.18    assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"