24 |
24 |
25 recdef xzgcda |
25 recdef xzgcda |
26 "measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r) |
26 "measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r) |
27 :: int * int * int * int *int * int * int * int => nat)" |
27 :: int * int * int * int *int * int * int * int => nat)" |
28 "xzgcda (m, n, r', r, s', s, t', t) = |
28 "xzgcda (m, n, r', r, s', s, t', t) = |
29 (if r \<le> 0 then (r', s', t') |
29 (if r \<le> 0 then (r', s', t') |
30 else xzgcda (m, n, r, r' mod r, |
30 else xzgcda (m, n, r, r' mod r, |
31 s, s' - (r' div r) * s, |
31 s, s' - (r' div r) * s, |
32 t, t' - (r' div r) * t))" |
32 t, t' - (r' div r) * t))" |
33 |
33 |
34 definition |
34 definition |
35 zprime :: "int \<Rightarrow> bool" where |
35 zprime :: "int \<Rightarrow> bool" where |
36 "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))" |
36 "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))" |
37 |
37 |