tidied up HOL/ex/Primrec
authorpaulson <lp15@cam.ac.uk>
Sun Mar 10 00:09:45 2019 +0000 (6 weeks ago ago)
changeset 70061fe3c12990893
parent 70056 03bc14eab432
child 70062 6a6cdf34e980
tidied up HOL/ex/Primrec
src/HOL/ex/Primrec.thy
     1.1 --- a/src/HOL/ex/Primrec.thy	Thu Mar 07 16:59:12 2019 +0000
     1.2 +++ b/src/HOL/ex/Primrec.thy	Sun Mar 10 00:09:45 2019 +0000
     1.3 @@ -1,12 +1,9 @@
     1.4  (*  Title:      HOL/ex/Primrec.thy
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Copyright   1997  University of Cambridge
     1.7 -
     1.8 -Ackermann's Function and the
     1.9 -Primitive Recursive Functions.
    1.10  *)
    1.11  
    1.12 -section \<open>Primitive Recursive Functions\<close>
    1.13 +section \<open>Ackermann's Function and the Primitive Recursive Functions\<close>
    1.14  
    1.15  theory Primrec imports Main begin
    1.16  
    1.17 @@ -25,37 +22,34 @@
    1.18  
    1.19  subsection\<open>Ackermann's Function\<close>
    1.20  
    1.21 -fun ack :: "nat => nat => nat" where
    1.22 -"ack 0 n =  Suc n" |
    1.23 -"ack (Suc m) 0 = ack m 1" |
    1.24 -"ack (Suc m) (Suc n) = ack m (ack (Suc m) n)"
    1.25 +fun ack :: "[nat,nat] \<Rightarrow> nat" where
    1.26 +  "ack 0 n =  Suc n"
    1.27 +| "ack (Suc m) 0 = ack m 1"
    1.28 +| "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)"
    1.29  
    1.30  
    1.31  text \<open>PROPERTY A 4\<close>
    1.32  
    1.33  lemma less_ack2 [iff]: "j < ack i j"
    1.34 -by (induct i j rule: ack.induct) simp_all
    1.35 +  by (induct i j rule: ack.induct) simp_all
    1.36  
    1.37  
    1.38  text \<open>PROPERTY A 5-, the single-step lemma\<close>
    1.39  
    1.40  lemma ack_less_ack_Suc2 [iff]: "ack i j < ack i (Suc j)"
    1.41 -by (induct i j rule: ack.induct) simp_all
    1.42 +  by (induct i j rule: ack.induct) simp_all
    1.43  
    1.44  
    1.45  text \<open>PROPERTY A 5, monotonicity for \<open><\<close>\<close>
    1.46  
    1.47 -lemma ack_less_mono2: "j < k ==> ack i j < ack i k"
    1.48 -using lift_Suc_mono_less[where f = "ack i"]
    1.49 -by (metis ack_less_ack_Suc2)
    1.50 +lemma ack_less_mono2: "j < k \<Longrightarrow> ack i j < ack i k"
    1.51 +  by (simp add: lift_Suc_mono_less)
    1.52  
    1.53  
    1.54  text \<open>PROPERTY A 5', monotonicity for \<open>\<le>\<close>\<close>
    1.55  
    1.56 -lemma ack_le_mono2: "j \<le> k ==> ack i j \<le> ack i k"
    1.57 -apply (simp add: order_le_less)
    1.58 -apply (blast intro: ack_less_mono2)
    1.59 -done
    1.60 +lemma ack_le_mono2: "j \<le> k \<Longrightarrow> ack i j \<le> ack i k"
    1.61 +  by (simp add: ack_less_mono2 less_mono_imp_le_mono)
    1.62  
    1.63  
    1.64  text \<open>PROPERTY A 6\<close>
    1.65 @@ -64,37 +58,41 @@
    1.66  proof (induct j)
    1.67    case 0 show ?case by simp
    1.68  next
    1.69 -  case (Suc j) show ?case 
    1.70 -    by (auto intro!: ack_le_mono2)
    1.71 -      (metis Suc Suc_leI Suc_lessI less_ack2 linorder_not_less)
    1.72 +  case (Suc j) show ?case
    1.73 +    by (metis Suc ack.simps(3) ack_le_mono2 le_trans less_ack2 less_eq_Suc_le) 
    1.74  qed
    1.75  
    1.76  
    1.77  text \<open>PROPERTY A 7-, the single-step lemma\<close>
    1.78  
    1.79  lemma ack_less_ack_Suc1 [iff]: "ack i j < ack (Suc i) j"
    1.80 -by (blast intro: ack_less_mono2 less_le_trans)
    1.81 +  by (blast intro: ack_less_mono2 less_le_trans)
    1.82  
    1.83  
    1.84  text \<open>PROPERTY A 4'? Extra lemma needed for \<^term>\<open>CONSTANT\<close> case, constant functions\<close>
    1.85  
    1.86  lemma less_ack1 [iff]: "i < ack i j"
    1.87 -apply (induct i)
    1.88 - apply simp_all
    1.89 -apply (blast intro: Suc_leI le_less_trans)
    1.90 -done
    1.91 +proof (induct i)
    1.92 +  case 0
    1.93 +  then show ?case 
    1.94 +    by simp
    1.95 +next
    1.96 +  case (Suc i)
    1.97 +  then show ?case
    1.98 +    using less_trans_Suc by blast
    1.99 +qed
   1.100  
   1.101  
   1.102  text \<open>PROPERTY A 8\<close>
   1.103  
   1.104  lemma ack_1 [simp]: "ack (Suc 0) j = j + 2"
   1.105 -by (induct j) simp_all
   1.106 +  by (induct j) simp_all
   1.107  
   1.108  
   1.109  text \<open>PROPERTY A 9.  The unary \<open>1\<close> and \<open>2\<close> in \<^term>\<open>ack\<close> is essential for the rewriting.\<close>
   1.110  
   1.111  lemma ack_2 [simp]: "ack (Suc (Suc 0)) j = 2 * j + 3"
   1.112 -by (induct j) simp_all
   1.113 +  by (induct j) simp_all
   1.114  
   1.115  
   1.116  text \<open>PROPERTY A 7, monotonicity for \<open><\<close> [not clear why
   1.117 @@ -103,209 +101,213 @@
   1.118  lemma ack_less_mono1_aux: "ack i k < ack (Suc (i +i')) k"
   1.119  proof (induct i k rule: ack.induct)
   1.120    case (1 n) show ?case
   1.121 -    by (simp, metis ack_less_ack_Suc1 less_ack2 less_trans_Suc) 
   1.122 +    using less_le_trans by auto
   1.123  next
   1.124    case (2 m) thus ?case by simp
   1.125  next
   1.126    case (3 m n) thus ?case
   1.127 -    by (simp, blast intro: less_trans ack_less_mono2)
   1.128 +    using ack_less_mono2 less_trans by fastforce
   1.129  qed
   1.130  
   1.131 -lemma ack_less_mono1: "i < j ==> ack i k < ack j k"
   1.132 -apply (drule less_imp_Suc_add)
   1.133 -apply (blast intro!: ack_less_mono1_aux)
   1.134 -done
   1.135 +lemma ack_less_mono1: "i < j \<Longrightarrow> ack i k < ack j k"
   1.136 +  using ack_less_mono1_aux less_iff_Suc_add by auto
   1.137  
   1.138  
   1.139  text \<open>PROPERTY A 7', monotonicity for \<open>\<le>\<close>\<close>
   1.140  
   1.141 -lemma ack_le_mono1: "i \<le> j ==> ack i k \<le> ack j k"
   1.142 -apply (simp add: order_le_less)
   1.143 -apply (blast intro: ack_less_mono1)
   1.144 -done
   1.145 +lemma ack_le_mono1: "i \<le> j \<Longrightarrow> ack i k \<le> ack j k"
   1.146 +  using ack_less_mono1 le_eq_less_or_eq by auto
   1.147  
   1.148  
   1.149  text \<open>PROPERTY A 10\<close>
   1.150  
   1.151  lemma ack_nest_bound: "ack i1 (ack i2 j) < ack (2 + (i1 + i2)) j"
   1.152 -apply simp
   1.153 -apply (rule ack2_le_ack1 [THEN [2] less_le_trans])
   1.154 -apply simp
   1.155 -apply (rule le_add1 [THEN ack_le_mono1, THEN le_less_trans])
   1.156 -apply (rule ack_less_mono1 [THEN ack_less_mono2])
   1.157 -apply (simp add: le_imp_less_Suc le_add2)
   1.158 -done
   1.159 +proof -
   1.160 +  have "ack i1 (ack i2 j) < ack (i1 + i2) (ack (Suc (i1 + i2)) j)"
   1.161 +    by (meson ack_le_mono1 ack_less_mono1 ack_less_mono2 le_add1 le_trans less_add_Suc2 not_less)
   1.162 +  also have "... = ack (Suc (i1 + i2)) (Suc j)"
   1.163 +    by simp
   1.164 +  also have "... \<le> ack (2 + (i1 + i2)) j"
   1.165 +    using ack2_le_ack1 add_2_eq_Suc by presburger
   1.166 +  finally show ?thesis .
   1.167 +qed
   1.168 +
   1.169  
   1.170  
   1.171  text \<open>PROPERTY A 11\<close>
   1.172  
   1.173  lemma ack_add_bound: "ack i1 j + ack i2 j < ack (4 + (i1 + i2)) j"
   1.174 -apply (rule less_trans [of _ "ack (Suc (Suc 0)) (ack (i1 + i2) j)"])
   1.175 - prefer 2
   1.176 - apply (rule ack_nest_bound [THEN less_le_trans])
   1.177 - apply (simp add: Suc3_eq_add_3)
   1.178 -apply simp
   1.179 -apply (cut_tac i = i1 and m1 = i2 and k = j in le_add1 [THEN ack_le_mono1])
   1.180 -apply (cut_tac i = "i2" and m1 = i1 and k = j in le_add2 [THEN ack_le_mono1])
   1.181 -apply auto
   1.182 -done
   1.183 +proof -
   1.184 +  have "ack i1 j \<le> ack (i1 + i2) j" "ack i2 j \<le> ack (i1 + i2) j"
   1.185 +    by (simp_all add: ack_le_mono1)
   1.186 +  then have "ack i1 j + ack i2 j < ack (Suc (Suc 0)) (ack (i1 + i2) j)"
   1.187 +    by simp
   1.188 +  also have "... < ack (4 + (i1 + i2)) j"
   1.189 +    by (metis ack_nest_bound add.assoc numeral_2_eq_2 numeral_Bit0)
   1.190 +  finally show ?thesis .
   1.191 +qed
   1.192  
   1.193  
   1.194  text \<open>PROPERTY A 12.  Article uses existential quantifier but the ALF proof
   1.195    used \<open>k + 4\<close>.  Quantified version must be nested \<open>\<exists>k'. \<forall>i j. ...\<close>\<close>
   1.196  
   1.197 -lemma ack_add_bound2: "i < ack k j ==> i + j < ack (4 + k) j"
   1.198 -apply (rule less_trans [of _ "ack k j + ack 0 j"])
   1.199 - apply (blast intro: add_less_mono) 
   1.200 -apply (rule ack_add_bound [THEN less_le_trans])
   1.201 -apply simp
   1.202 -done
   1.203 +lemma ack_add_bound2: 
   1.204 +  assumes "i < ack k j" shows "i + j < ack (4 + k) j"
   1.205 +proof -
   1.206 +  have "i + j < ack k j + ack 0 j"
   1.207 +    using assms by auto
   1.208 +  also have "... < ack (4 + k) j"
   1.209 +    by (metis ack_add_bound add.right_neutral)
   1.210 +  finally show ?thesis .
   1.211 +qed
   1.212  
   1.213  
   1.214  subsection\<open>Primitive Recursive Functions\<close>
   1.215  
   1.216 -primrec hd0 :: "nat list => nat" where
   1.217 -"hd0 [] = 0" |
   1.218 -"hd0 (m # ms) = m"
   1.219 +primrec hd0 :: "nat list \<Rightarrow> nat" where
   1.220 +  "hd0 [] = 0" 
   1.221 +| "hd0 (m # ms) = m"
   1.222  
   1.223  
   1.224 -text \<open>Inductive definition of the set of primitive recursive functions of type \<^typ>\<open>nat list => nat\<close>.\<close>
   1.225 +text \<open>Inductive definition of the set of primitive recursive functions of type \<^typ>\<open>nat list \<Rightarrow> nat\<close>.\<close>
   1.226  
   1.227 -definition SC :: "nat list => nat" where
   1.228 -"SC l = Suc (hd0 l)"
   1.229 +definition SC :: "nat list \<Rightarrow> nat" 
   1.230 +  where "SC l = Suc (hd0 l)"
   1.231  
   1.232 -definition CONSTANT :: "nat => nat list => nat" where
   1.233 -"CONSTANT k l = k"
   1.234 +definition CONSTANT :: "nat \<Rightarrow> nat list \<Rightarrow> nat" 
   1.235 +  where "CONSTANT k l = k"
   1.236  
   1.237 -definition PROJ :: "nat => nat list => nat" where
   1.238 -"PROJ i l = hd0 (drop i l)"
   1.239 -
   1.240 -definition
   1.241 -COMP :: "(nat list => nat) => (nat list => nat) list => nat list => nat"
   1.242 -where "COMP g fs l = g (map (\<lambda>f. f l) fs)"
   1.243 +definition PROJ :: "nat \<Rightarrow> nat list \<Rightarrow> nat" 
   1.244 +  where "PROJ i l = hd0 (drop i l)"
   1.245  
   1.246 -definition PREC :: "(nat list => nat) => (nat list => nat) => nat list => nat"
   1.247 -where
   1.248 -  "PREC f g l =
   1.249 -    (case l of
   1.250 -      [] => 0
   1.251 -    | x # l' => rec_nat (f l') (\<lambda>y r. g (r # y # l')) x)"
   1.252 -  \<comment> \<open>Note that \<^term>\<open>g\<close> is applied first to \<^term>\<open>PREC f g y\<close> and then to \<^term>\<open>y\<close>!\<close>
   1.253 +definition COMP :: "[nat list \<Rightarrow> nat, (nat list \<Rightarrow> nat) list, nat list] \<Rightarrow> nat"
   1.254 +  where "COMP g fs l = g (map (\<lambda>f. f l) fs)"
   1.255  
   1.256 -inductive PRIMREC :: "(nat list => nat) => bool" where
   1.257 -SC: "PRIMREC SC" |
   1.258 -CONSTANT: "PRIMREC (CONSTANT k)" |
   1.259 -PROJ: "PRIMREC (PROJ i)" |
   1.260 -COMP: "PRIMREC g ==> \<forall>f \<in> set fs. PRIMREC f ==> PRIMREC (COMP g fs)" |
   1.261 -PREC: "PRIMREC f ==> PRIMREC g ==> PRIMREC (PREC f g)"
   1.262 +fun PREC :: "[nat list \<Rightarrow> nat, nat list \<Rightarrow> nat, nat list] \<Rightarrow> nat"
   1.263 +  where
   1.264 +    "PREC f g [] = 0"
   1.265 +  | "PREC f g (x # l) = rec_nat (f l) (\<lambda>y r. g (r # y # l)) x"
   1.266 +    \<comment> \<open>Note that \<^term>\<open>g\<close> is applied first to \<^term>\<open>PREC f g y\<close> and then to \<^term>\<open>y\<close>!\<close>
   1.267 +
   1.268 +inductive PRIMREC :: "(nat list \<Rightarrow> nat) \<Rightarrow> bool" where
   1.269 +  SC: "PRIMREC SC"
   1.270 +| CONSTANT: "PRIMREC (CONSTANT k)"
   1.271 +| PROJ: "PRIMREC (PROJ i)"
   1.272 +| COMP: "PRIMREC g \<Longrightarrow> \<forall>f \<in> set fs. PRIMREC f \<Longrightarrow> PRIMREC (COMP g fs)"
   1.273 +| PREC: "PRIMREC f \<Longrightarrow> PRIMREC g \<Longrightarrow> PRIMREC (PREC f g)"
   1.274  
   1.275  
   1.276  text \<open>Useful special cases of evaluation\<close>
   1.277  
   1.278  lemma SC [simp]: "SC (x # l) = Suc x"
   1.279 -by (simp add: SC_def)
   1.280 -
   1.281 -lemma CONSTANT [simp]: "CONSTANT k l = k"
   1.282 -by (simp add: CONSTANT_def)
   1.283 +  by (simp add: SC_def)
   1.284  
   1.285  lemma PROJ_0 [simp]: "PROJ 0 (x # l) = x"
   1.286 -by (simp add: PROJ_def)
   1.287 +  by (simp add: PROJ_def)
   1.288  
   1.289  lemma COMP_1 [simp]: "COMP g [f] l = g [f l]"
   1.290 -by (simp add: COMP_def)
   1.291 +  by (simp add: COMP_def)
   1.292  
   1.293 -lemma PREC_0 [simp]: "PREC f g (0 # l) = f l"
   1.294 -by (simp add: PREC_def)
   1.295 +lemma PREC_0: "PREC f g (0 # l) = f l"
   1.296 +  by simp
   1.297  
   1.298  lemma PREC_Suc [simp]: "PREC f g (Suc x # l) = g (PREC f g (x # l) # x # l)"
   1.299 -by (simp add: PREC_def)
   1.300 +  by auto
   1.301  
   1.302  
   1.303 -text \<open>MAIN RESULT\<close>
   1.304 +subsection \<open>MAIN RESULT\<close>
   1.305  
   1.306  lemma SC_case: "SC l < ack 1 (sum_list l)"
   1.307 -apply (unfold SC_def)
   1.308 -apply (induct l)
   1.309 -apply (simp_all add: le_add1 le_imp_less_Suc)
   1.310 -done
   1.311 +  unfolding SC_def
   1.312 +  by (induct l) (simp_all add: le_add1 le_imp_less_Suc)
   1.313  
   1.314  lemma CONSTANT_case: "CONSTANT k l < ack k (sum_list l)"
   1.315 -by simp
   1.316 +  by (simp add: CONSTANT_def)
   1.317  
   1.318  lemma PROJ_case: "PROJ i l < ack 0 (sum_list l)"
   1.319 -apply (simp add: PROJ_def)
   1.320 -apply (induct l arbitrary:i)
   1.321 - apply (auto simp add: drop_Cons split: nat.split)
   1.322 -apply (blast intro: less_le_trans le_add2)
   1.323 -done
   1.324 +  unfolding PROJ_def
   1.325 +proof (induct l arbitrary: i)
   1.326 +  case Nil
   1.327 +  then show ?case
   1.328 +    by simp
   1.329 +next
   1.330 +  case (Cons a l)
   1.331 +  then show ?case
   1.332 +    by (metis ack.simps(1) add.commute drop_Cons' hd0.simps(2) leD leI lessI not_less_eq sum_list.Cons trans_le_add2)
   1.333 +qed
   1.334  
   1.335  
   1.336  text \<open>\<^term>\<open>COMP\<close> case\<close>
   1.337  
   1.338  lemma COMP_map_aux: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l))
   1.339 -  ==> \<exists>k. \<forall>l. sum_list (map (\<lambda>f. f l) fs) < ack k (sum_list l)"
   1.340 -apply (induct fs)
   1.341 - apply (rule_tac x = 0 in exI)
   1.342 - apply simp
   1.343 -apply simp
   1.344 -apply (blast intro: add_less_mono ack_add_bound less_trans)
   1.345 -done
   1.346 +  \<Longrightarrow> \<exists>k. \<forall>l. sum_list (map (\<lambda>f. f l) fs) < ack k (sum_list l)"
   1.347 +proof (induct fs)
   1.348 +  case Nil
   1.349 +  then show ?case
   1.350 +    by auto
   1.351 +next
   1.352 +  case (Cons a fs)
   1.353 +  then show ?case
   1.354 +    by simp (blast intro: add_less_mono ack_add_bound less_trans)
   1.355 +qed
   1.356  
   1.357  lemma COMP_case:
   1.358 -  "\<forall>l. g l < ack kg (sum_list l) ==>
   1.359 -  \<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l))
   1.360 -  ==> \<exists>k. \<forall>l. COMP g fs  l < ack k (sum_list l)"
   1.361 -apply (unfold COMP_def)
   1.362 -apply (drule COMP_map_aux)
   1.363 -apply (meson ack_less_mono2 ack_nest_bound less_trans)
   1.364 -done
   1.365 -
   1.366 +  assumes 1: "\<forall>l. g l < ack kg (sum_list l)" 
   1.367 +      and 2: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l))"
   1.368 +  shows "\<exists>k. \<forall>l. COMP g fs  l < ack k (sum_list l)"
   1.369 +  unfolding COMP_def
   1.370 +  using 1 COMP_map_aux [OF 2] by (meson ack_less_mono2 ack_nest_bound less_trans)
   1.371  
   1.372  text \<open>\<^term>\<open>PREC\<close> case\<close>
   1.373  
   1.374  lemma PREC_case_aux:
   1.375 -  "\<forall>l. f l + sum_list l < ack kf (sum_list l) ==>
   1.376 -    \<forall>l. g l + sum_list l < ack kg (sum_list l) ==>
   1.377 -    PREC f g l + sum_list l < ack (Suc (kf + kg)) (sum_list l)"
   1.378 -apply (unfold PREC_def)
   1.379 -apply (case_tac l)
   1.380 - apply simp_all
   1.381 - apply (blast intro: less_trans)
   1.382 -apply (erule ssubst) \<comment> \<open>get rid of the needless assumption\<close>
   1.383 -apply (induct_tac a)
   1.384 - apply simp_all
   1.385 - txt \<open>base case\<close>
   1.386 - apply (blast intro: le_add1 [THEN le_imp_less_Suc, THEN ack_less_mono1] less_trans)
   1.387 -txt \<open>induction step\<close>
   1.388 -apply (rule Suc_leI [THEN le_less_trans])
   1.389 - apply (rule le_refl [THEN add_le_mono, THEN le_less_trans])
   1.390 -  prefer 2
   1.391 -  apply (erule spec)
   1.392 - apply (simp add: le_add2)
   1.393 -txt \<open>final part of the simplification\<close>
   1.394 -apply simp
   1.395 -apply (rule le_add2 [THEN ack_le_mono1, THEN le_less_trans])
   1.396 -apply (erule ack_less_mono2)
   1.397 -done
   1.398 +  assumes f: "\<And>l. f l + sum_list l < ack kf (sum_list l)"
   1.399 +      and g: "\<And>l. g l + sum_list l < ack kg (sum_list l)"
   1.400 +  shows "PREC f g l + sum_list l < ack (Suc (kf + kg)) (sum_list l)"
   1.401 +proof (cases l)
   1.402 +  case Nil
   1.403 +  then show ?thesis
   1.404 +    by (simp add: Suc_lessD)
   1.405 +next
   1.406 +  case (Cons m l)
   1.407 +  have "rec_nat (f l) (\<lambda>y r. g (r # y # l)) m + (m + sum_list l) < ack (Suc (kf + kg)) (m + sum_list l)"
   1.408 +  proof (induct m)
   1.409 +    case 0
   1.410 +    then show ?case
   1.411 +      using ack_less_mono1_aux f less_trans by fastforce
   1.412 +  next
   1.413 +    case (Suc m)
   1.414 +    let ?r = "rec_nat (f l) (\<lambda>y r. g (r # y # l)) m"
   1.415 +    have "\<not> g (?r # m # l) + sum_list (?r # m # l) < g (?r # m # l) + (m + sum_list l)"
   1.416 +      by force
   1.417 +    then have "g (?r # m # l) + (m + sum_list l) < ack kg (sum_list (?r # m # l))"
   1.418 +      by (meson assms(2) leI less_le_trans)
   1.419 +    moreover 
   1.420 +    have "... < ack (kf + kg) (ack (Suc (kf + kg)) (m + sum_list l))"
   1.421 +      using Suc.hyps by simp (meson ack_le_mono1 ack_less_mono2 le_add2 le_less_trans)
   1.422 +    ultimately show ?case
   1.423 +      by auto
   1.424 +  qed
   1.425 +  then show ?thesis
   1.426 +    by (simp add: local.Cons)
   1.427 +qed
   1.428  
   1.429 -lemma PREC_case:
   1.430 -  "\<forall>l. f l < ack kf (sum_list l) ==>
   1.431 -    \<forall>l. g l < ack kg (sum_list l) ==>
   1.432 -    \<exists>k. \<forall>l. PREC f g l < ack k (sum_list l)"
   1.433 -by (metis le_less_trans [OF le_add1 PREC_case_aux] ack_add_bound2)
   1.434 +proposition PREC_case:
   1.435 +  "\<lbrakk>\<And>l. f l < ack kf (sum_list l); \<And>l. g l < ack kg (sum_list l)\<rbrakk> 
   1.436 +  \<Longrightarrow> \<exists>k. \<forall>l. PREC f g l < ack k (sum_list l)"
   1.437 +  by (metis le_less_trans [OF le_add1 PREC_case_aux] ack_add_bound2)
   1.438  
   1.439 -lemma ack_bounds_PRIMREC: "PRIMREC f ==> \<exists>k. \<forall>l. f l < ack k (sum_list l)"
   1.440 -apply (erule PRIMREC.induct)
   1.441 -    apply (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+
   1.442 -done
   1.443 +lemma ack_bounds_PRIMREC: "PRIMREC f \<Longrightarrow> \<exists>k. \<forall>l. f l < ack k (sum_list l)"
   1.444 +  by (erule PRIMREC.induct) (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+
   1.445  
   1.446  theorem ack_not_PRIMREC:
   1.447 -  "\<not> PRIMREC (\<lambda>l. case l of [] => 0 | x # l' => ack x x)"
   1.448 -apply (rule notI)
   1.449 -apply (erule ack_bounds_PRIMREC [THEN exE])
   1.450 -apply (rule less_irrefl [THEN notE])
   1.451 -apply (drule_tac x = "[x]" in spec)
   1.452 -apply simp
   1.453 -done
   1.454 +  "\<not> PRIMREC (\<lambda>l. case l of [] \<Rightarrow> 0 | x # l' \<Rightarrow> ack x x)"
   1.455 +proof
   1.456 +  assume *: "PRIMREC (\<lambda>l. case l of [] \<Rightarrow> 0 | x # l' \<Rightarrow> ack x x)"
   1.457 +  then obtain m where m: "\<And>l. (case l of [] \<Rightarrow> 0 | x # l' \<Rightarrow> ack x x) < ack m (sum_list l)"
   1.458 +    using ack_bounds_PRIMREC by metis
   1.459 +  show False
   1.460 +    using m [of "[m]"] by simp
   1.461 +qed
   1.462  
   1.463  end