equal
deleted
inserted
replaced
97 by (blast intro!: gcd_greatest intro: dvd_trans) |
97 by (blast intro!: gcd_greatest intro: dvd_trans) |
98 |
98 |
99 |
99 |
100 (**** The material below was omitted from the book ****) |
100 (**** The material below was omitted from the book ****) |
101 |
101 |
102 constdefs |
102 definition is_gcd :: "[nat,nat,nat] \<Rightarrow> bool" where (*gcd as a relation*) |
103 is_gcd :: "[nat,nat,nat] \<Rightarrow> bool" (*gcd as a relation*) |
|
104 "is_gcd p m n == p dvd m \<and> p dvd n \<and> |
103 "is_gcd p m n == p dvd m \<and> p dvd n \<and> |
105 (ALL d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)" |
104 (ALL d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)" |
106 |
105 |
107 (*Function gcd yields the Greatest Common Divisor*) |
106 (*Function gcd yields the Greatest Common Divisor*) |
108 lemma is_gcd: "is_gcd (gcd m n) m n" |
107 lemma is_gcd: "is_gcd (gcd m n) m n" |