Cosmetic: no !! in the lemma statement
authorpaulson <lp15@cam.ac.uk>
Fri, 02 Apr 2021 12:24:29 +0100
changeset 73786 c89922715bf5
parent 73782 c72fd8f1fceb
child 73787 5fa2e2786ecf
Cosmetic: no !! in the lemma statement
src/HOL/Examples/Ackermann.thy
--- a/src/HOL/Examples/Ackermann.thy	Thu Apr 01 07:35:03 2021 +0200
+++ b/src/HOL/Examples/Ackermann.thy	Fri Apr 02 12:24:29 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>