equal
deleted
inserted
replaced
20 |
20 |
21 recdef gcd "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)" |
21 recdef gcd "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)" |
22 "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))" |
22 "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))" |
23 |
23 |
24 definition |
24 definition |
25 is_gcd :: "nat => nat => nat => bool" -- {* @{term gcd} as a relation *} |
25 is_gcd :: "nat => nat => nat => bool" where -- {* @{term gcd} as a relation *} |
26 "is_gcd p m n = (p dvd m \<and> p dvd n \<and> |
26 "is_gcd p m n = (p dvd m \<and> p dvd n \<and> |
27 (\<forall>d. d dvd m \<and> d dvd n --> d dvd p))" |
27 (\<forall>d. d dvd m \<and> d dvd n --> d dvd p))" |
28 |
28 |
29 |
29 |
30 lemma gcd_induct: |
30 lemma gcd_induct: |