# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1591701195 -3600
# Node ID 35a2ac83a262c2a9bc335223c39c12c0c6be5cd5
# Parent  73ff22f99d3825a6e218bca1e3c14030dd918ddf
New Ackermann development

diff -r 73ff22f99d38 -r 35a2ac83a262 src/HOL/Examples/Ackermann.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Ackermann.thy	Tue Jun 09 12:13:15 2020 +0100
@@ -0,0 +1,98 @@
+section \<open>A Tail-Recursive, Stack-Based Ackermann's Function\<close>
+
+theory Ackermann imports Main
+
+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>
+
+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)"
+
+text\<open>Here is the stack-based version, which 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"
+  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.
+
+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>
+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>
+lemma "\<And>n l. ackloop_dom (ack m n # l) \<Longrightarrow> ackloop_dom (n # m # l)"
+proof (induction m)
+  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
+qed
+
+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
+
+lemma "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>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)
+
+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>
+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)
+
+end
diff -r 73ff22f99d38 -r 35a2ac83a262 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Jun 08 22:49:06 2020 +0200
+++ b/src/HOL/ROOT	Tue Jun 09 12:13:15 2020 +0100
@@ -20,6 +20,7 @@
   sessions
     "HOL-Library"
   theories
+    Ackermann
     Knaster_Tarski
     Peirce
     Drinker