merged
authorpaulson
Fri, 02 Apr 2021 12:24:35 +0100
changeset 73787 5fa2e2786ecf
parent 73785 89cf7c903aca (current diff)
parent 73786 c89922715bf5 (diff)
child 73788 543d5539306d
merged
--- 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>