equal
deleted
inserted
replaced
59 text \<open>The proof above (which actually is unused) can be expressed concisely as follows.\<close> |
59 text \<open>The proof above (which actually is unused) can be expressed concisely as follows.\<close> |
60 lemma ackloop_dom_longer: |
60 lemma ackloop_dom_longer: |
61 "ackloop_dom (ack m n # l) \<Longrightarrow> ackloop_dom (n # m # l)" |
61 "ackloop_dom (ack m n # l) \<Longrightarrow> ackloop_dom (n # m # l)" |
62 by (induction m n arbitrary: l rule: ack.induct) auto |
62 by (induction m n arbitrary: l rule: ack.induct) auto |
63 |
63 |
64 lemma "ackloop_dom (ack m n # l) \<Longrightarrow> ackloop_dom (n # m # l)" |
|
65 by (induction m n arbitrary: l rule: ack.induct) auto |
|
66 |
|
67 text\<open>This function codifies what @{term ackloop} is designed to do. |
64 text\<open>This function codifies what @{term ackloop} is designed to do. |
68 Proving the two functions equivalent also shows that @{term ackloop} can be used |
65 Proving the two functions equivalent also shows that @{term ackloop} can be used |
69 to compute Ackermann's function.\<close> |
66 to compute Ackermann's function.\<close> |
70 fun acklist :: "nat list \<Rightarrow> nat" where |
67 fun acklist :: "nat list \<Rightarrow> nat" where |
71 "acklist (n#m#l) = acklist (ack m n # l)" |
68 "acklist (n#m#l) = acklist (ack m n # l)" |