diff -r 0e27325da568 -r 8bcb906e73f2 src/HOL/Hoare/Examples.thy
--- a/src/HOL/Hoare/Examples.thy	Fri Oct 18 20:48:01 2024 +0200
+++ b/src/HOL/Hoare/Examples.thy	Fri Oct 18 21:19:06 2024 +0200
@@ -315,35 +315,36 @@
   Ambiguity warnings of parser are due to \<open>:=\<close> being used
   both for assignment and list update.
 \<close>
-lemma lem: "m - Suc 0 < n ==> m < Suc n"
-by arith
-
-
 lemma Partition:
-"[| leq == \<lambda>A i. \<forall>k. k<i \<longrightarrow> A!k \<le> pivot;
-    geq == \<lambda>A i. \<forall>k. i<k \<and> k<length A \<longrightarrow> pivot \<le> A!k |] ==>
- VARS A u l
- {0 < length(A::('a::order)list)}
- l := 0; u := length A - Suc 0;
- WHILE l \<le> u
-  INV {leq A l \<and> geq A u \<and> u<length A \<and> l\<le>length A}
-  DO WHILE l < length A \<and> A!l \<le> pivot
-     INV {leq A l & geq A u \<and> u<length A \<and> l\<le>length A}
-     DO l := l+1 OD;
-     WHILE 0 < u & pivot \<le> A!u
-     INV {leq A l & geq A u  \<and> u<length A \<and> l\<le>length A}
-     DO u := u - 1 OD;
-     IF l \<le> u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
-  OD
- {leq A u & (\<forall>k. u<k \<and> k<l --> A!k = pivot) \<and> geq A l}"
-\<comment> \<open>expand and delete abbreviations first\<close>
-apply (simp)
-apply (erule thin_rl)+
-apply vcg_simp
-   apply (force simp: neq_Nil_conv)
-  apply (blast elim!: less_SucE intro: Suc_leI)
- apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
-apply (force simp: nth_list_update)
-done
+  fixes pivot
+  defines "leq \<equiv> \<lambda>A i. \<forall>k. k<i \<longrightarrow> A!k \<le> pivot"
+    and "geq \<equiv> \<lambda>A i. \<forall>k. i<k \<and> k<length A \<longrightarrow> pivot \<le> A!k"
+  shows
+    "VARS A u l
+     {0 < length(A::('a::order)list)}
+     l := 0; u := length A - Suc 0;
+     WHILE l \<le> u
+      INV {leq A l \<and> geq A u \<and> u<length A \<and> l\<le>length A}
+      DO WHILE l < length A \<and> A!l \<le> pivot
+         INV {leq A l & geq A u \<and> u<length A \<and> l\<le>length A}
+         DO l := l+1 OD;
+         WHILE 0 < u & pivot \<le> A!u
+         INV {leq A l & geq A u  \<and> u<length A \<and> l\<le>length A}
+         DO u := u - 1 OD;
+         IF l \<le> u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
+      OD
+     {leq A u & (\<forall>k. u<k \<and> k<l --> A!k = pivot) \<and> geq A l}"
+proof -
+  have eq: "m - Suc 0 < n \<Longrightarrow> m < Suc n" for m n
+    by arith
+  show ?thesis
+    apply (simp add: assms)
+    apply vcg_simp
+       apply (force simp: neq_Nil_conv)
+      apply (blast elim!: less_SucE intro: Suc_leI)
+     apply (blast elim!: less_SucE intro: less_imp_diff_less dest: eq)
+    apply (force simp: nth_list_update)
+    done
+qed
 
 end