Tuned proof of lcm_1_iff_int, because metis produced enormous proof term.
authorberghofe
Mon Jul 13 19:07:05 2009 +0200 (2009-07-13)
changeset 319961d93369079c4
parent 31995 8f37cf60b885
child 32001 fafefd0b341c
child 32040 830141c9e528
child 32065 9fa18f1c2b2d
Tuned proof of lcm_1_iff_int, because metis produced enormous proof term.
src/HOL/GCD.thy
     1.1 --- a/src/HOL/GCD.thy	Sun Jul 12 14:48:01 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Mon Jul 13 19:07:05 2009 +0200
     1.3 @@ -1503,7 +1503,7 @@
     1.4  by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
     1.5  
     1.6  lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
     1.7 -by (metis abs_minus_one abs_mult_self lcm_proj1_if_dvd_int lcm_unique_int one_dvd zmult_eq_1_iff)
     1.8 +by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
     1.9  
    1.10  
    1.11  subsection {* Primes *}