# HG changeset patch
# User wenzelm
# Date 1719832143 -7200
# Node ID 7fe5aa0ca3c42dcace8899db62a181f1febbbed4
# Parent  98d7d21c1bde9405537e80389b39e0766772d790
tuned document layout, for more prominent presentation;

diff -r 98d7d21c1bde -r 7fe5aa0ca3c4 src/HOL/Examples/Ackermann.thy
--- a/src/HOL/Examples/Ackermann.thy	Mon Jul 01 12:59:46 2024 +0200
+++ b/src/HOL/Examples/Ackermann.thy	Mon Jul 01 13:09:03 2024 +0200
@@ -4,48 +4,57 @@
 
 section \<open>A Tail-Recursive, Stack-Based Ackermann's Function\<close>
 
-theory Ackermann imports "HOL-Library.Multiset_Order" "HOL-Library.Product_Lexorder" 
-
+theory Ackermann
+  imports "HOL-Library.Multiset_Order" "HOL-Library.Product_Lexorder"
 begin
 
-text\<open>This theory investigates a stack-based implementation of Ackermann's function.
-Let's recall the traditional definition,
-as modified by R{\'o}zsa P\'eter and Raphael Robinson.\<close>
+text \<open>
+  This theory investigates a stack-based implementation of Ackermann's
+  function. Let's recall the traditional definition, as modified by Péter
+  Rózsa and Raphael Robinson.
+\<close>
+fun ack :: "[nat, nat] \<Rightarrow> nat"
+  where
+    "ack 0 n             = Suc n"
+  | "ack (Suc m) 0       = ack m 1"
+  | "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)"
 
-fun ack :: "[nat,nat] \<Rightarrow> nat" where
-  "ack 0 n             = Suc n"
-| "ack (Suc m) 0       = ack m 1"
-| "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)"
 
 subsection \<open>Example of proving termination by reasoning about the domain\<close>
 
-text\<open>The stack-based version uses lists.\<close>
+text \<open>The stack-based version uses lists.\<close>
 
-function (domintros) ackloop :: "nat list \<Rightarrow> nat" where
-  "ackloop (n # 0 # l)         = ackloop (Suc n # l)"
-| "ackloop (0 # Suc m # l)     = ackloop (1 # m # l)"
-| "ackloop (Suc n # Suc m # l) = ackloop (n # Suc m # m # l)"
-| "ackloop [m] = m"
-| "ackloop [] =  0"
+function (domintros) ackloop :: "nat list \<Rightarrow> nat"
+  where
+    "ackloop (n # 0 # l)         = ackloop (Suc n # l)"
+  | "ackloop (0 # Suc m # l)     = ackloop (1 # m # l)"
+  | "ackloop (Suc n # Suc m # l) = ackloop (n # Suc m # m # l)"
+  | "ackloop [m] = m"
+  | "ackloop [] =  0"
   by pat_completeness auto
 
-text\<open>
-The key task is to prove termination. In the first recursive call, the head of the list gets bigger
-while the list gets shorter, suggesting that the length of the list should be the primary
-termination criterion. But in the third recursive call, the list gets longer. The idea of trying
-a multiset-based termination argument is frustrated by the second recursive call when m = 0:
-the list elements are simply permuted.
+text \<open>
+  The key task is to prove termination. In the first recursive call, the head of
+  the list gets bigger while the list gets shorter, suggesting that the length
+  of the list should be the primary termination criterion. But in the third
+  recursive call, the list gets longer. The idea of trying a multiset-based
+  termination argument is frustrated by the second recursive call when \<open>m = 0\<close>:
+  the list elements are simply permuted.
 
-Fortunately, the function definition package allows us to define a function and only later identify its domain of termination.
-Instead, it makes all the recursion equations conditional on satisfying
-the function's domain predicate. Here we shall eventually be able
-to show that the predicate is always satisfied.\<close>
+  Fortunately, the function definition package allows us to define a function
+  and only later identify its domain of termination. Instead, it makes all the
+  recursion equations conditional on satisfying the function's domain predicate.
+  Here we shall eventually be able to show that the predicate is always
+  satisfied.
+\<close>
 
-text\<open>@{thm [display] ackloop.domintros[no_vars]}\<close>
+text \<open>@{thm [display] ackloop.domintros[no_vars]}\<close>
 declare ackloop.domintros [simp]
 
-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>
+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 "ackloop_dom (ack m n # l) \<Longrightarrow> ackloop_dom (n # m # l)"
 proof (induction m arbitrary: n l)
   case 0
@@ -58,20 +67,26 @@
     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>
+text \<open>
+  The proof above (which actually is unused) can be expressed concisely as
+  follows.
+\<close>
 lemma ackloop_dom_longer:
   "ackloop_dom (ack m n # l) \<Longrightarrow> ackloop_dom (n # m # l)"
   by (induction m n arbitrary: l rule: ack.induct) auto
 
-text\<open>This function codifies what @{term ackloop} is designed to do.
-Proving the two functions equivalent also shows that @{term ackloop} can be used
-to compute Ackermann's function.\<close>
-fun acklist :: "nat list \<Rightarrow> nat" where
-  "acklist (n#m#l) = acklist (ack m n # l)"
-| "acklist [m] = m"
-| "acklist [] =  0"
+text \<open>
+  This function codifies what @{term ackloop} is designed to do. Proving the
+  two functions equivalent also shows that @{term ackloop} can be used to
+  compute Ackermann's function.
+\<close>
+fun acklist :: "nat list \<Rightarrow> nat"
+  where
+    "acklist (n#m#l) = acklist (ack m n # l)"
+  | "acklist [m] = m"
+  | "acklist [] =  0"
 
-text\<open>The induction rule for @{term acklist} is @{thm [display] acklist.induct[no_vars]}.\<close>
+text \<open>The induction rule for @{term acklist} is @{thm [display] acklist.induct[no_vars]}.\<close>
 
 lemma ackloop_dom: "ackloop_dom l"
   by (induction l rule: acklist.induct) (auto simp: ackloop_dom_longer)
@@ -79,28 +94,36 @@
 termination ackloop
   by (simp add: ackloop_dom)
 
-text\<open>This result is trivial even by inspection of the function definitions
-(which faithfully follow the definition of Ackermann's function).
-All that we needed was termination.\<close>
+text \<open>
+  This result is trivial even by inspection of the function definitions (which
+  faithfully follow the definition of Ackermann's function). All that we
+  needed was termination.
+\<close>
 lemma ackloop_acklist: "ackloop l = acklist l"
   by (induction l rule: ackloop.induct) auto
 
 theorem ack: "ack m n = ackloop [n,m]"
   by (simp add: ackloop_acklist)
 
+
 subsection \<open>Example of proving termination using a multiset ordering\<close>
 
-text \<open>This termination proof uses the argument from
-Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings.
-Communications of the ACM 22 (8) 1979, 465--476.\<close>
+text \<open>
+  This termination proof uses the argument from
+  Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings.
+  Communications of the ACM 22 (8) 1979, 465--476.
+\<close>
 
-text\<open>Setting up the termination proof. Note that Dershowitz had @{term z} as a global variable.
-The top two stack elements are treated differently from the rest.\<close>
-
-fun ack_mset :: "nat list \<Rightarrow> (nat\<times>nat) multiset" where
-  "ack_mset [] = {#}"
-| "ack_mset [x] = {#}"
-| "ack_mset (z#y#l) = mset ((y,z) # map (\<lambda>x. (Suc x, 0)) l)"
+text \<open>
+  Setting up the termination proof. Note that Dershowitz had @{term z} as a
+  global variable. The top two stack elements are treated differently from the
+  rest.
+\<close>
+fun ack_mset :: "nat list \<Rightarrow> (nat\<times>nat) multiset"
+  where
+    "ack_mset [] = {#}"
+  | "ack_mset [x] = {#}"
+  | "ack_mset (z#y#l) = mset ((y,z) # map (\<lambda>x. (Suc x, 0)) l)"
 
 lemma case1: "ack_mset (Suc n # l) < add_mset (0,n) {# (Suc x, 0). x \<in># mset l #}"
 proof (cases l)
@@ -109,28 +132,38 @@
     by auto
   also have "\<dots> \<le> {#(Suc m, 0), (0,n)#}"
     by auto
-  finally show ?thesis  
+  finally show ?thesis
     by (simp add: Cons)
-qed auto
-
-text\<open>The stack-based version again. We need a fresh copy because 
-  we've already proved the termination of @{term ackloop}.\<close>
+next
+  case Nil
+  then show ?thesis by auto
+qed
 
-function Ackloop :: "nat list \<Rightarrow> nat" where
-  "Ackloop (n # 0 # l)         = Ackloop (Suc n # l)"
-| "Ackloop (0 # Suc m # l)     = Ackloop (1 # m # l)"
-| "Ackloop (Suc n # Suc m # l) = Ackloop (n # Suc m # m # l)"
-| "Ackloop [m] = m"
-| "Ackloop [] =  0"
+text \<open>
+  The stack-based version again. We need a fresh copy because we've already
+  proved the termination of @{term ackloop}.
+\<close>
+function Ackloop :: "nat list \<Rightarrow> nat"
+  where
+    "Ackloop (n # 0 # l)         = Ackloop (Suc n # l)"
+  | "Ackloop (0 # Suc m # l)     = Ackloop (1 # m # l)"
+  | "Ackloop (Suc n # Suc m # l) = Ackloop (n # Suc m # m # l)"
+  | "Ackloop [m] = m"
+  | "Ackloop [] =  0"
   by pat_completeness auto
 
 
-text \<open>In each recursive call, the function @{term ack_mset} decreases according to the multiset
-ordering.\<close>
+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 case1)
 
-text \<open>Another shortcut compared with before: equivalence follows directly from this lemma.\<close>
+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)"
   by (induction m n arbitrary: l rule: ack.induct) auto