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 |
43 assume "dropWhile Not ps = q # qs" |
43 assume "dropWhile Not ps = q # qs" |
44 then have "length (q # qs) = length (dropWhile Not ps)" by simp |
44 then have "length qs < length (dropWhile Not ps)" |
45 then have "length qs < length (dropWhile Not ps)" by simp |
45 by simp |
46 moreover have "length (dropWhile Not ps) \<le> length ps" |
46 also have "length (dropWhile Not ps) \<le> length ps" |
47 by (simp add: length_dropWhile_le) |
47 by (simp add: length_dropWhile_le) |
48 ultimately show "length qs < length ps" by auto |
48 finally show "length qs < length ps" . |
49 qed |
49 qed |
50 |
50 |
51 primrec natify :: "nat \<Rightarrow> bool list \<Rightarrow> nat list" where |
51 primrec natify :: "nat \<Rightarrow> bool list \<Rightarrow> nat list" where |
52 "natify _ [] = []" |
52 "natify _ [] = []" |
53 | "natify n (p#ps) = (if p then n # natify (Suc n) ps else natify (Suc n) ps)" |
53 | "natify n (p#ps) = (if p then n # natify (Suc n) ps else natify (Suc n) ps)" |
59 subsubsection \<open>Naive factorisation\<close> |
59 subsubsection \<open>Naive factorisation\<close> |
60 |
60 |
61 function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where |
61 function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where |
62 "factorise_from k n = (if 1 < k \<and> k \<le> n |
62 "factorise_from k n = (if 1 < k \<and> k \<le> n |
63 then |
63 then |
64 let (q, r) = Divides.divmod_nat n k |
64 let (q, r) = Euclidean_Division.divmod_nat n k |
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 \<comment> \<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 apply (relation "measure (\<lambda>(k, n). 2 * n - k)") |
71 apply (relation "measure (\<lambda>(k, n). 2 * n - k)") |
72 apply (auto simp add: prod_eq_iff algebra_simps elim!: dvdE) |
72 apply (auto simp add: Euclidean_Division.divmod_nat_def algebra_simps elim!: dvdE) |
73 apply (case_tac "k \<le> ka * 2") |
73 subgoal for m n |
74 apply (auto intro: diff_less_mono) |
74 apply (cases "m \<le> n * 2") |
|
75 apply (auto intro: diff_less_mono) |
|
76 done |
75 done |
77 done |
76 |
78 |
77 definition factorise :: "nat \<Rightarrow> nat list" where |
79 definition factorise :: "nat \<Rightarrow> nat list" where |
78 "factorise n = factorise_from 2 n" |
80 "factorise n = factorise_from 2 n" |
79 |
81 |