equal
deleted
inserted
replaced
32 "sieve m ps = (case dropWhile Not ps |
32 "sieve m ps = (case dropWhile Not ps |
33 of [] \<Rightarrow> ps |
33 of [] \<Rightarrow> ps |
34 | p#ps' \<Rightarrow> let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))" |
34 | p#ps' \<Rightarrow> let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))" |
35 by pat_completeness auto |
35 by pat_completeness auto |
36 |
36 |
37 termination -- \<open>tuning of this proof is left as an exercise to the reader\<close> |
37 termination \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close> |
38 apply (relation "measure (length \<circ> snd)") |
38 apply (relation "measure (length \<circ> snd)") |
39 apply rule |
39 apply rule |
40 apply (auto simp add: length_dropWhile_le) |
40 apply (auto simp add: length_dropWhile_le) |
41 proof - |
41 proof - |
42 fix ps qs q |
42 fix ps qs q |
65 in if r = 0 then k # factorise_from k q |
65 in if r = 0 then k # factorise_from k q |
66 else factorise_from (Suc k) n |
66 else factorise_from (Suc k) n |
67 else [])" |
67 else [])" |
68 by pat_completeness auto |
68 by pat_completeness auto |
69 |
69 |
70 termination factorise_from -- \<open>tuning of this proof is left as an exercise to the reader\<close> |
70 termination factorise_from \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close> |
71 term measure |
71 term measure |
72 apply (relation "measure (\<lambda>(k, n). 2 * n - k)") |
72 apply (relation "measure (\<lambda>(k, n). 2 * n - k)") |
73 apply (auto simp add: prod_eq_iff) |
73 apply (auto simp add: prod_eq_iff) |
74 apply (case_tac "k \<le> 2 * q") |
74 apply (case_tac "k \<le> 2 * q") |
75 apply (rule diff_less_mono) |
75 apply (rule diff_less_mono) |