--- /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
--- 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