# HG changeset patch # User paulson <lp15@cam.ac.uk> # Date 1666018841 -3600 # Node ID e5162a8baa2458d3e70d0b994491746bfb19fba6 # Parent f89f4aab1cc445aa39a7dcf09a1a08d3df7a0f60 tiny renaming diff -r f89f4aab1cc4 -r e5162a8baa24 src/HOL/Examples/Ackermann.thy --- a/src/HOL/Examples/Ackermann.thy Mon Oct 17 14:53:09 2022 +0100 +++ b/src/HOL/Examples/Ackermann.thy Mon Oct 17 16:00:41 2022 +0100 @@ -102,7 +102,7 @@ | "ack_mset [x] = {#}" | "ack_mset (z#y#l) = mset ((y,z) # map (\<lambda>x. (Suc x, 0)) l)" -lemma base: "ack_mset (Suc n # l) < add_mset (0,n) {# (Suc x, 0). x \<in># mset l #}" +lemma case1: "ack_mset (Suc n # l) < add_mset (0,n) {# (Suc x, 0). x \<in># mset l #}" proof (cases l) case (Cons m list) have "{#(m, Suc n)#} < {#(Suc m, 0)#}" @@ -128,7 +128,7 @@ text \<open>In each recursive call, the function @{term ack_mset} decreases according to the multiset ordering.\<close> termination - by (relation "inv_image {(x,y). x<y} ack_mset") (auto simp: wf base) + by (relation "inv_image {(x,y). x<y} ack_mset") (auto simp: wf case1) text \<open>Another shortcut compared with before: equivalence follows directly from this lemma.\<close> lemma Ackloop_ack: "Ackloop (n # m # l) = Ackloop (ack m n # l)"