--- a/src/HOL/ex/Parallel_Example.thy Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/ex/Parallel_Example.thy Sun Aug 21 06:18:23 2022 +0000
@@ -41,11 +41,11 @@
proof -
fix ps qs q
assume "dropWhile Not ps = q # qs"
- then have "length (q # qs) = length (dropWhile Not ps)" by simp
- then have "length qs < length (dropWhile Not ps)" by simp
- moreover have "length (dropWhile Not ps) \<le> length ps"
+ then have "length qs < length (dropWhile Not ps)"
+ by simp
+ also have "length (dropWhile Not ps) \<le> length ps"
by (simp add: length_dropWhile_le)
- ultimately show "length qs < length ps" by auto
+ finally show "length qs < length ps" .
qed
primrec natify :: "nat \<Rightarrow> bool list \<Rightarrow> nat list" where
@@ -61,7 +61,7 @@
function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
"factorise_from k n = (if 1 < k \<and> k \<le> n
then
- let (q, r) = Divides.divmod_nat n k
+ let (q, r) = Euclidean_Division.divmod_nat n k
in if r = 0 then k # factorise_from k q
else factorise_from (Suc k) n
else [])"
@@ -69,9 +69,11 @@
termination factorise_from \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close>
apply (relation "measure (\<lambda>(k, n). 2 * n - k)")
- apply (auto simp add: prod_eq_iff algebra_simps elim!: dvdE)
- apply (case_tac "k \<le> ka * 2")
- apply (auto intro: diff_less_mono)
+ apply (auto simp add: Euclidean_Division.divmod_nat_def algebra_simps elim!: dvdE)
+ subgoal for m n
+ apply (cases "m \<le> n * 2")
+ apply (auto intro: diff_less_mono)
+ done
done
definition factorise :: "nat \<Rightarrow> nat list" where