equal
deleted
inserted
replaced
419 proof |
419 proof |
420 interpret semiring_Gcd 1 0 times |
420 interpret semiring_Gcd 1 0 times |
421 Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm |
421 Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm |
422 Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm |
422 Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm |
423 divide plus minus unit_factor normalize |
423 divide plus minus unit_factor normalize |
424 rewrites "dvd.dvd ( * ) = Rings.dvd" |
424 rewrites "dvd.dvd (*) = Rings.dvd" |
425 by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff) |
425 by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff) |
426 show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)" |
426 show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)" |
427 proof (rule ext)+ |
427 proof (rule ext)+ |
428 fix a b :: 'a |
428 fix a b :: 'a |
429 show "Euclidean_Algorithm.gcd a b = gcd a b" |
429 show "Euclidean_Algorithm.gcd a b = gcd a b" |
573 proof |
573 proof |
574 interpret semiring_Gcd 1 0 times |
574 interpret semiring_Gcd 1 0 times |
575 "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm" |
575 "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm" |
576 "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm" |
576 "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm" |
577 divide plus minus unit_factor normalize |
577 divide plus minus unit_factor normalize |
578 rewrites "dvd.dvd ( * ) = Rings.dvd" |
578 rewrites "dvd.dvd (*) = Rings.dvd" |
579 by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff) |
579 by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff) |
580 show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd" |
580 show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd" |
581 proof (rule ext)+ |
581 proof (rule ext)+ |
582 fix m n :: nat |
582 fix m n :: nat |
583 show "Euclidean_Algorithm.gcd m n = gcd m n" |
583 show "Euclidean_Algorithm.gcd m n = gcd m n" |
610 proof |
610 proof |
611 interpret semiring_Gcd 1 0 times |
611 interpret semiring_Gcd 1 0 times |
612 "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm" |
612 "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm" |
613 "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm" |
613 "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm" |
614 divide plus minus unit_factor normalize |
614 divide plus minus unit_factor normalize |
615 rewrites "dvd.dvd ( * ) = Rings.dvd" |
615 rewrites "dvd.dvd (*) = Rings.dvd" |
616 by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff) |
616 by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff) |
617 show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd" |
617 show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd" |
618 proof (rule ext)+ |
618 proof (rule ext)+ |
619 fix k l :: int |
619 fix k l :: int |
620 show "Euclidean_Algorithm.gcd k l = gcd k l" |
620 show "Euclidean_Algorithm.gcd k l = gcd k l" |