# HG changeset patch
# User paulson
# Date 1617362675 -3600
# Node ID 5fa2e2786ecf0102c4bf44f231163fbe4723cc40
# Parent  89cf7c903acad179e40c10f2f6643d3c21448f47# Parent  c89922715bf5e6c36e20bab0304afc87bcdc888d
merged

diff -r 89cf7c903aca -r 5fa2e2786ecf src/HOL/Examples/Ackermann.thy
--- a/src/HOL/Examples/Ackermann.thy	Thu Apr 01 19:14:43 2021 +0200
+++ b/src/HOL/Examples/Ackermann.thy	Fri Apr 02 12:24:35 2021 +0100
@@ -44,26 +44,16 @@
 
 text \<open>Termination is trivial if the length of the list is less then two.
 The following lemma is the key to proving termination for longer lists.\<close>
-lemma "\<And>n l. ackloop_dom (ack m n # l) \<Longrightarrow> ackloop_dom (n # m # l)"
-proof (induction m)
+lemma "ackloop_dom (ack m n # l) \<Longrightarrow> ackloop_dom (n # m # l)"
+proof (induction m arbitrary: n l)
   case 0
   then show ?case
     by auto
 next
   case (Suc m)
-  note IH = Suc
-  have "\<And>l. ackloop_dom (ack (Suc m) n # l) \<Longrightarrow> ackloop_dom (n # Suc m # l)"
-  proof (induction n)
-    case 0
-    then show ?case
-      by (simp add: IH)
-  next
-    case (Suc n)
-    then show ?case
-      by (auto simp: IH)
-  qed
-  then show ?case
-    using Suc.prems by blast
+  show ?case
+    using Suc.prems
+    by (induction n arbitrary: l) (simp_all add: Suc)
 qed
 
 text \<open>The proof above (which actually is unused) can be expressed concisely as follows.\<close>