1 theory UF

     2 imports Main rec_def turing_basic GCD abacus

     3 begin

     4 

     5 text {*

     6   This theory file constructs the Universal Function @{text "rec_F"}, which is the UTM defined

     7   in terms of recursive functions. This @{text "rec_F"} is essentially an 

     8   interpreter of Turing Machines. Once the correctness of @{text "rec_F"} is established,

     9   UTM can easil be obtained by compling @{text "rec_F"} into the corresponding Turing Machine.

    10 *}

    11 

    12 

    13 section {* The construction of component functions *}

    14 

    15 text {*

    16   This section constructs a set of component functions used to construct @{text "rec_F"}.

    17   *}

    18 

    19 text {*

    20   The recursive function used to do arithmatic addition.

    21 *}

    22 definition rec_add :: "recf"

    23   where

    24   "rec_add \<equiv>  Pr 1 (id 1 0) (Cn 3 s [id 3 2])"

    25 

    26 text {*

    27   The recursive function used to do arithmatic multiplication.

    28 *}

    29 definition rec_mult :: "recf"

    30   where

    31   "rec_mult = Pr 1 z (Cn 3 rec_add [id 3 0, id 3 2])"

    32 

    33 text {*

    34   The recursive function used to do arithmatic precede.

    35 *}

    36 definition rec_pred :: "recf"

    37   where

    38   "rec_pred = Cn 1 (Pr 1 z (id 3 1)) [id 1 0, id 1 0]"

    39 

    40 text {*

    41   The recursive function used to do arithmatic subtraction.

    42 *}

    43 definition rec_minus :: "recf" 

    44   where

    45   "rec_minus = Pr 1 (id 1 0) (Cn 3 rec_pred [id 3 2])"

    46 

    47 text {*

    48   @{text "constn n"} is the recursive function which computes 

    49   nature number @{text "n"}.

    50 *}

    51 fun constn :: "nat \<Rightarrow> recf"

    52   where

    53   "constn 0 = z"  |

    54   "constn (Suc n) = Cn 1 s [constn n]"

    55 

    56 

    57 text {*

    58   Signal function, which returns 1 when the input argument is greater than @{text "0"}.

    59 *}

    60 definition rec_sg :: "recf"

    61   where

    62   "rec_sg = Cn 1 rec_minus [constn 1, 

    63                   Cn 1 rec_minus [constn 1, id 1 0]]"

    64 

    65 text {*

    66   @{text "rec_less"} compares its two arguments, returns @{text "1"} if

    67   the first is less than the second; otherwise returns @{text "0"}.

    68   *}

    69 definition rec_less :: "recf"

    70   where

    71   "rec_less = Cn 2 rec_sg [Cn 2 rec_minus [id 2 1, id 2 0]]"

    72 

    73 text {*

    74   @{text "rec_not"} inverse its argument: returns @{text "1"} when the

    75   argument is @{text "0"}; returns @{text "0"} otherwise.

    76   *}

    77 definition rec_not :: "recf"

    78   where

    79   "rec_not = Cn 1 rec_minus [constn 1, id 1 0]"

    80 

    81 text {*

    82   @{text "rec_eq"} compares its two arguments: returns @{text "1"}

    83   if they are equal; return @{text "0"} otherwise.

    84   *}

    85 definition rec_eq :: "recf"

    86   where

    87   "rec_eq = Cn 2 rec_minus [Cn 2 (constn 1) [id 2 0], 

    88              Cn 2 rec_add [Cn 2 rec_minus [id 2 0, id 2 1], 

    89                Cn 2 rec_minus [id 2 1, id 2 0]]]"

    90 

    91 text {*

    92   @{text "rec_conj"} computes the conjunction of its two arguments, 

    93   returns @{text "1"} if both of them are non-zero; returns @{text "0"}

    94   otherwise.

    95   *}

    96 definition rec_conj :: "recf"

    97   where

    98   "rec_conj = Cn 2 rec_sg [Cn 2 rec_mult [id 2 0, id 2 1]] "

    99 

   100 text {*

   101   @{text "rec_disj"} computes the disjunction of its two arguments, 

   102   returns @{text "0"} if both of them are zero; returns @{text "0"}

   103   otherwise.

   104   *}

   105 definition rec_disj :: "recf"

   106   where

   107   "rec_disj = Cn 2 rec_sg [Cn 2 rec_add [id 2 0, id 2 1]]"

   108 

   109 

   110 text {*

   111   Computes the arity of recursive function.

   112   *}

   113 

   114 fun arity :: "recf \<Rightarrow> nat"

   115   where

   116   "arity z = 1" 

   117 | "arity s = 1"

   118 | "arity (id m n) = m"

   119 | "arity (Cn n f gs) = n"

   120 | "arity (Pr n f g) = Suc n"

   121 | "arity (Mn n f) = n"

   122 

   123 text {*

   124   @{text "get_fstn_args n (Suc k)"} returns

   125   @{text "[id n 0, id n 1, id n 2, \<dots>, id n k]"}, 

   126   the effect of which is to take out the first @{text "Suc k"} 

   127   arguments out of the @{text "n"} input arguments.

   128   *}

   129 (* get_fstn_args *)

   130 fun get_fstn_args :: "nat \<Rightarrow>  nat \<Rightarrow> recf list"

   131   where

   132   "get_fstn_args n 0 = []"

   133 | "get_fstn_args n (Suc y) = get_fstn_args n y @ [id n y]"

   134 

   135 text {*

   136   @{text "rec_sigma f"} returns the recursive functions which 

   137   sums up the results of @{text "f"}:

   138   \[

   139   (rec\_sigma f)(x, y) = f(x, 0) + f(x, 1) + \cdots + f(x, y)

   140   \]

   141 *}

   142 fun rec_sigma :: "recf \<Rightarrow> recf"

   143   where

   144   "rec_sigma rf = 

   145        (let vl = arity rf in 

   146           Pr (vl - 1) (Cn (vl - 1) rf (get_fstn_args (vl - 1) (vl - 1) @ 

   147                     [Cn (vl - 1) (constn 0) [id (vl - 1) 0]])) 

   148              (Cn (Suc vl) rec_add [id (Suc vl) vl, 

   149                     Cn (Suc vl) rf (get_fstn_args (Suc vl) (vl - 1) 

   150                         @ [Cn (Suc vl) s [id (Suc vl) (vl - 1)]])]))"

   151 

   152 text {*

   153   @{text "rec_exec"} is the interpreter function for

   154   reursive functions. The function is defined such that 

   155   it always returns meaningful results for primitive recursive 

   156   functions.

   157   *}

   158 function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat"

   159   where

   160   "rec_exec z xs = 0" |

   161   "rec_exec s xs = (Suc (xs ! 0))" |

   162   "rec_exec (id m n) xs = (xs ! n)" |

   163   "rec_exec (Cn n f gs) xs = 

   164              (let ys = (map (\<lambda> a. rec_exec a xs) gs) in 

   165                                   rec_exec f ys)" | 

   166   "rec_exec (Pr n f g) xs = 

   167      (if last xs = 0 then 

   168                   rec_exec f (butlast xs)

   169       else rec_exec g (butlast xs @ [last xs - 1] @

   170             [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))" |

   171   "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)"

   172 by pat_completeness auto

   173 termination

   174 proof 

   175   show "wf (measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)])" 

   176     by auto

   177 next

   178   fix n f gs xs x

   179   assume "(x::recf) \<in> set gs" 

   180   thus "((x, xs), Cn n f gs, xs) \<in> 

   181     measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"

   182     by(induct gs, auto)

   183 next

   184   fix n f gs xs x

   185   assume "x = map (\<lambda>a. rec_exec a xs) gs"

   186     "\<And>x. x \<in> set gs \<Longrightarrow> rec_exec_dom (x, xs)" 

   187   thus "((f, x), Cn n f gs, xs) \<in> 

   188     measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"

   189     by(auto)

   190 next

   191   fix n f g xs

   192   show "((f, butlast xs), Pr n f g, xs) \<in>

   193     measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"

   194     by auto

   195 next

   196   fix n f g xs

   197   assume "last xs \<noteq> (0::nat)" thus 

   198     "((Pr n f g, butlast xs @ [last xs - 1]), Pr n f g, xs) 

   199     \<in> measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"

   200     by auto

   201 next

   202   fix n f g xs

   203   show "((g, butlast xs @ [last xs - 1] @ [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]), 

   204     Pr n f g, xs) \<in> measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"

   205     by auto

   206 next

   207   fix n f xs x

   208   show "((f, xs @ [x]), Mn n f, xs) \<in> 

   209     measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"

   210     by auto

   211 qed

   212 

   213 declare rec_exec.simps[simp del] constn.simps[simp del]

   214 

   215 text {*

   216   Correctness of @{text "rec_add"}.

   217   *}

   218 lemma add_lemma: "\<And> x y. rec_exec rec_add [x, y] =  x + y"

   219 by(induct_tac y, auto simp: rec_add_def rec_exec.simps)

   220 

   221 text {*

   222   Correctness of @{text "rec_mult"}.

   223   *}

   224 lemma mult_lemma: "\<And> x y. rec_exec rec_mult [x, y] = x * y"

   225 by(induct_tac y, auto simp: rec_mult_def rec_exec.simps add_lemma)

   226 

   227 text {*

   228   Correctness of @{text "rec_pred"}.

   229   *}

   230 lemma pred_lemma: "\<And> x. rec_exec rec_pred [x] =  x - 1"

   231 by(induct_tac x, auto simp: rec_pred_def rec_exec.simps)

   232 

   233 text {*

   234   Correctness of @{text "rec_minus"}.

   235   *}

   236 lemma minus_lemma: "\<And> x y. rec_exec rec_minus [x, y] = x - y"

   237 by(induct_tac y, auto simp: rec_exec.simps rec_minus_def pred_lemma)

   238 

   239 text {*

   240   Correctness of @{text "rec_sg"}.

   241   *}

   242 lemma sg_lemma: "\<And> x. rec_exec rec_sg [x] = (if x = 0 then 0 else 1)"

   243 by(auto simp: rec_sg_def minus_lemma rec_exec.simps constn.simps)

   244 

   245 text {*

   246   Correctness of @{text "constn"}.

   247   *}

   248 lemma constn_lemma: "rec_exec (constn n) [x] = n"

   249 by(induct n, auto simp: rec_exec.simps constn.simps)

   250 

   251 text {*

   252   Correctness of @{text "rec_less"}.

   253   *}

   254 lemma less_lemma: "\<And> x y. rec_exec rec_less [x, y] = 

   255   (if x < y then 1 else 0)"

   256 by(induct_tac y, auto simp: rec_exec.simps 

   257   rec_less_def minus_lemma sg_lemma)

   258 

   259 text {*

   260   Correctness of @{text "rec_not"}.

   261   *}

   262 lemma not_lemma: 

   263   "\<And> x. rec_exec rec_not [x] = (if x = 0 then 1 else 0)"

   264 by(induct_tac x, auto simp: rec_exec.simps rec_not_def

   265   constn_lemma minus_lemma)

   266 

   267 text {*

   268   Correctness of @{text "rec_eq"}.

   269   *}

   270 lemma eq_lemma: "\<And> x y. rec_exec rec_eq [x, y] = (if x = y then 1 else 0)"

   271 by(induct_tac y, auto simp: rec_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma)

   272 

   273 text {*

   274   Correctness of @{text "rec_conj"}.

   275   *}

   276 lemma conj_lemma: "\<And> x y. rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 

   277                                                        else 1)"

   278 by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)

   279 

   280 

   281 text {*

   282   Correctness of @{text "rec_disj"}.

   283   *}

   284 lemma disj_lemma: "\<And> x y. rec_exec rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0

   285                                                      else 1)"

   286 by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_exec.simps)

   287 

   288 

   289 text {*

   290   @{text "primrec recf n"} is true iff 

   291   @{text "recf"} is a primitive recursive function 

   292   with arity @{text "n"}.

   293   *}

   294 inductive primerec :: "recf \<Rightarrow> nat \<Rightarrow> bool"

   295   where

   296 prime_z[intro]:  "primerec z (Suc 0)" |

   297 prime_s[intro]:  "primerec s (Suc 0)" |

   298 prime_id[intro!]: "\<lbrakk>n < m\<rbrakk> \<Longrightarrow> primerec (id m n) m" |

   299 prime_cn[intro!]: "\<lbrakk>primerec f k; length gs = k; 

   300   \<forall> i < length gs. primerec (gs ! i) m; m = n\<rbrakk> 

   301   \<Longrightarrow> primerec (Cn n f gs) m" |

   302 prime_pr[intro!]: "\<lbrakk>primerec f n; 

   303   primerec g (Suc (Suc n)); m = Suc n\<rbrakk> 

   304   \<Longrightarrow> primerec (Pr n f g) m" 

   305 

   306 inductive_cases prime_cn_reverse'[elim]: "primerec (Cn n f gs) n" 

   307 inductive_cases prime_mn_reverse: "primerec (Mn n f) m" 

   308 inductive_cases prime_z_reverse[elim]: "primerec z n"

   309 inductive_cases prime_s_reverse[elim]: "primerec s n"

   310 inductive_cases prime_id_reverse[elim]: "primerec (id m n) k"

   311 inductive_cases prime_cn_reverse[elim]: "primerec (Cn n f gs) m"

   312 inductive_cases prime_pr_reverse[elim]: "primerec (Pr n f g) m"

   313 

   314 declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp] 

   315         minus_lemma[simp] sg_lemma[simp] constn_lemma[simp] 

   316         less_lemma[simp] not_lemma[simp] eq_lemma[simp]

   317         conj_lemma[simp] disj_lemma[simp]

   318 

   319 text {*

   320   @{text "Sigma"} is the logical specification of 

   321   the recursive function @{text "rec_sigma"}.

   322   *}

   323 function Sigma :: "(nat list \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat"

   324   where

   325   "Sigma g xs = (if last xs = 0 then g xs

   326                  else (Sigma g (butlast xs @ [last xs - 1]) +

   327                        g xs)) "

   328 by pat_completeness auto

   329 termination

   330 proof

   331   show "wf (measure (\<lambda> (f, xs). last xs))" by auto

   332 next

   333   fix g xs

   334   assume "last (xs::nat list) \<noteq> 0"

   335   thus "((g, butlast xs @ [last xs - 1]), g, xs)  

   336                    \<in> measure (\<lambda>(f, xs). last xs)"

   337     by auto

   338 qed

   339 

   340 declare rec_exec.simps[simp del] get_fstn_args.simps[simp del]

   341         arity.simps[simp del] Sigma.simps[simp del]

   342         rec_sigma.simps[simp del]

   343 

   344 

   345 section {* Properties of @{text rec_sigma} *}

   346 

   347 lemma [simp]: "arity z = 1"

   348  by(simp add: arity.simps)

   349 

   350 lemma rec_pr_0_simp_rewrite: "

   351   rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"

   352 by(simp add: rec_exec.simps)

   353 

   354 lemma rec_pr_0_simp_rewrite_single_param: "

   355   rec_exec (Pr n f g) [0] = rec_exec f []"

   356 by(simp add: rec_exec.simps)

   357 

   358 lemma rec_pr_Suc_simp_rewrite: 

   359   "rec_exec (Pr n f g) (xs @ [Suc x]) =

   360                        rec_exec g (xs @ [x] @ 

   361                         [rec_exec (Pr n f g) (xs @ [x])])"

   362 by(simp add: rec_exec.simps)

   363 

   364 lemma rec_pr_Suc_simp_rewrite_single_param: 

   365   "rec_exec (Pr n f g) ([Suc x]) =

   366            rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"

   367 by(simp add: rec_exec.simps)

   368 

   369 thm Sigma.simps

   370 

   371 lemma Sigma_0_simp_rewrite_single_param:

   372   "Sigma f [0] = f [0]"

   373 by(simp add: Sigma.simps)

   374 

   375 lemma Sigma_0_simp_rewrite:

   376   "Sigma f (xs @ [0]) = f (xs @ [0])"

   377 by(simp add: Sigma.simps)

   378 

   379 lemma Sigma_Suc_simp_rewrite: 

   380   "Sigma f (xs @ [Suc x]) = Sigma f (xs @ [x]) + f (xs @ [Suc x])"

   381 by(simp add: Sigma.simps)

   382 

   383 lemma Sigma_Suc_simp_rewrite_single: 

   384   "Sigma f ([Suc x]) = Sigma f ([x]) + f ([Suc x])"

   385 by(simp add: Sigma.simps)

   386 

   387 lemma  [simp]: "(xs @ ys) ! (Suc (length xs)) = ys ! 1"

   388 by(simp add: nth_append)

   389   

   390 lemma get_fstn_args_take: "\<lbrakk>length xs = m; n \<le> m\<rbrakk> \<Longrightarrow> 

   391   map (\<lambda> f. rec_exec f xs) (get_fstn_args m n)= take n xs"

   392 proof(induct n)

   393   case 0 thus "?case"

   394     by(simp add: get_fstn_args.simps)

   395 next

   396   case (Suc n) thus "?case"

   397     by(simp add: get_fstn_args.simps rec_exec.simps 

   398              take_Suc_conv_app_nth)

   399 qed

   400     

   401 lemma [simp]: "primerec f n \<Longrightarrow> arity f = n"

   402   apply(case_tac f)

   403   apply(auto simp: arity.simps )

   404   apply(erule_tac prime_mn_reverse)

   405   done

   406 

   407 lemma rec_sigma_Suc_simp_rewrite: 

   408   "primerec f (Suc (length xs))

   409     \<Longrightarrow> rec_exec (rec_sigma f) (xs @ [Suc x]) = 

   410     rec_exec (rec_sigma f) (xs @ [x]) + rec_exec f (xs @ [Suc x])"

   411   apply(induct x)

   412   apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite

   413                    rec_exec.simps get_fstn_args_take)

   414   done      

   415 

   416 text {*

   417   The correctness of @{text "rec_sigma"} with respect to its specification.

   418   *}

   419 lemma sigma_lemma: 

   420   "primerec rg (Suc (length xs))

   421      \<Longrightarrow> rec_exec (rec_sigma rg) (xs @ [x]) = Sigma (rec_exec rg) (xs @ [x])"

   422 apply(induct x)

   423 apply(auto simp: rec_exec.simps rec_sigma.simps Let_def 

   424          get_fstn_args_take Sigma_0_simp_rewrite

   425          Sigma_Suc_simp_rewrite) 

   426 done

   427 

   428 text {*

   429   @{text "rec_accum f (x1, x2, \<dots>, xn, k) = 

   430            f(x1, x2, \<dots>, xn, 0) * 

   431            f(x1, x2, \<dots>, xn, 1) *

   432                \<dots> 

   433            f(x1, x2, \<dots>, xn, k)"}

   434 *}

   435 fun rec_accum :: "recf \<Rightarrow> recf"

   436   where

   437   "rec_accum rf = 

   438        (let vl = arity rf in 

   439           Pr (vl - 1) (Cn (vl - 1) rf (get_fstn_args (vl - 1) (vl - 1) @ 

   440                      [Cn (vl - 1) (constn 0) [id (vl - 1) 0]])) 

   441              (Cn (Suc vl) rec_mult [id (Suc vl) (vl), 

   442                     Cn (Suc vl) rf (get_fstn_args (Suc vl) (vl - 1) 

   443                       @ [Cn (Suc vl) s [id (Suc vl) (vl - 1)]])]))"

   444 

   445 text {*

   446   @{text "Accum"} is the formal specification of @{text "rec_accum"}.

   447   *}

   448 function Accum :: "(nat list \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat"

   449   where

   450   "Accum f xs = (if last xs = 0 then f xs 

   451                      else (Accum f (butlast xs @ [last xs - 1]) *

   452                        f xs))"

   453 by pat_completeness auto

   454 termination

   455 proof

   456   show "wf (measure (\<lambda> (f, xs). last xs))"

   457     by auto

   458 next

   459   fix f xs

   460   assume "last xs \<noteq> (0::nat)"

   461   thus "((f, butlast xs @ [last xs - 1]), f, xs) \<in> 

   462             measure (\<lambda>(f, xs). last xs)"

   463     by auto

   464 qed

   465 

   466 lemma rec_accum_Suc_simp_rewrite: 

   467   "primerec f (Suc (length xs))

   468     \<Longrightarrow> rec_exec (rec_accum f) (xs @ [Suc x]) = 

   469     rec_exec (rec_accum f) (xs @ [x]) * rec_exec f (xs @ [Suc x])"

   470   apply(induct x)

   471   apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite

   472                    rec_exec.simps get_fstn_args_take)

   473   done  

   474 

   475 text {*

   476   The correctness of @{text "rec_accum"} with respect to its specification.

   477 *}

   478 lemma accum_lemma :

   479   "primerec rg (Suc (length xs))

   480      \<Longrightarrow> rec_exec (rec_accum rg) (xs @ [x]) = Accum (rec_exec rg) (xs @ [x])"

   481 apply(induct x)

   482 apply(auto simp: rec_exec.simps rec_sigma.simps Let_def 

   483                      get_fstn_args_take)

   484 done

   485 

   486 declare rec_accum.simps [simp del]

   487 

   488 text {*

   489   @{text "rec_all t f (x1, x2, \<dots>, xn)"} 

   490   computes the charactrization function of the following FOL formula:

   491   @{text "(\<forall> x \<le> t(x1, x2, \<dots>, xn). (f(x1, x2, \<dots>, xn, x) > 0))"}

   492 *}

   493 fun rec_all :: "recf \<Rightarrow> recf \<Rightarrow> recf"

   494   where

   495   "rec_all rt rf = 

   496     (let vl = arity rf in

   497        Cn (vl - 1) rec_sg [Cn (vl - 1) (rec_accum rf) 

   498                  (get_fstn_args (vl - 1) (vl - 1) @ [rt])])"

   499 

   500 lemma rec_accum_ex: "primerec rf (Suc (length xs)) \<Longrightarrow>

   501      (rec_exec (rec_accum rf) (xs @ [x]) = 0) = 

   502       (\<exists> t \<le> x. rec_exec rf (xs @ [t]) = 0)"

   503 apply(induct x, simp_all add: rec_accum_Suc_simp_rewrite)

   504 apply(simp add: rec_exec.simps rec_accum.simps get_fstn_args_take, 

   505       auto)

   506 apply(rule_tac x = ta in exI, simp)

   507 apply(case_tac "t = Suc x", simp_all)

   508 apply(rule_tac x = t in exI, simp)

   509 done

   510 

   511 text {*

   512   The correctness of @{text "rec_all"}.

   513   *}

   514 lemma all_lemma: 

   515   "\<lbrakk>primerec rf (Suc (length xs));

   516     primerec rt (length xs)\<rbrakk>

   517   \<Longrightarrow> rec_exec (rec_all rt rf) xs = (if (\<forall> x \<le> (rec_exec rt xs). 0 < rec_exec rf (xs @ [x])) then 1

   518                                                                                               else 0)"

   519 apply(auto simp: rec_all.simps)

   520 apply(simp add: rec_exec.simps map_append get_fstn_args_take split: if_splits)

   521 apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex)

   522 apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp_all)

   523 apply(erule_tac exE, erule_tac x = t in allE, simp)

   524 apply(simp add: rec_exec.simps map_append get_fstn_args_take)

   525 apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex)

   526 apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp, simp)

   527 apply(erule_tac x = x in allE, simp)

   528 done

   529 

   530 text {*

   531   @{text "rec_ex t f (x1, x2, \<dots>, xn)"} 

   532   computes the charactrization function of the following FOL formula:

   533   @{text "(\<exists> x \<le> t(x1, x2, \<dots>, xn). (f(x1, x2, \<dots>, xn, x) > 0))"}

   534 *}

   535 fun rec_ex :: "recf \<Rightarrow> recf \<Rightarrow> recf"

   536   where

   537   "rec_ex rt rf = 

   538        (let vl = arity rf in 

   539          Cn (vl - 1) rec_sg [Cn (vl - 1) (rec_sigma rf) 

   540                   (get_fstn_args (vl - 1) (vl - 1) @ [rt])])"

   541 

   542 lemma rec_sigma_ex: "primerec rf (Suc (length xs))

   543           \<Longrightarrow> (rec_exec (rec_sigma rf) (xs @ [x]) = 0) = 

   544                           (\<forall> t \<le> x. rec_exec rf (xs @ [t]) = 0)"

   545 apply(induct x, simp_all add: rec_sigma_Suc_simp_rewrite)

   546 apply(simp add: rec_exec.simps rec_sigma.simps 

   547                 get_fstn_args_take, auto)

   548 apply(case_tac "t = Suc x", simp_all)

   549 done

   550 

   551 text {*

   552   The correctness of @{text "ex_lemma"}.

   553   *}

   554 lemma ex_lemma:"

   555   \<lbrakk>primerec rf (Suc (length xs));

   556    primerec rt (length xs)\<rbrakk>

   557 \<Longrightarrow> (rec_exec (rec_ex rt rf) xs =

   558     (if (\<exists> x \<le> (rec_exec rt xs). 0 <rec_exec rf (xs @ [x])) then 1

   559      else 0))"

   560 apply(auto simp: rec_ex.simps rec_exec.simps map_append get_fstn_args_take 

   561             split: if_splits)

   562 apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp)

   563 apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp)

   564 done

   565 

   566 text {*

   567   Defintiion of @{text "Min[R]"} on page 77 of Boolos's book.

   568 *}

   569 

   570 fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> nat"

   571   where "Minr Rr xs w = (let setx = {y | y. (y \<le> w) \<and> Rr (xs @ [y])} in 

   572                         if (setx = {}) then (Suc w)

   573                                        else (Min setx))"

   574 

   575 declare Minr.simps[simp del] rec_all.simps[simp del]

   576 

   577 text {*

   578   The following is a set of auxilliary lemmas about @{text "Minr"}.

   579 *}

   580 lemma Minr_range: "Minr Rr xs w \<le> w \<or> Minr Rr xs w = Suc w"

   581 apply(auto simp: Minr.simps)

   582 apply(subgoal_tac "Min {x. x \<le> w \<and> Rr (xs @ [x])} \<le> x")

   583 apply(erule_tac order_trans, simp)

   584 apply(rule_tac Min_le, auto)

   585 done

   586 

   587 lemma [simp]: "{x. x \<le> Suc w \<and> Rr (xs @ [x])}

   588     = (if Rr (xs @ [Suc w]) then insert (Suc w) 

   589                               {x. x \<le> w \<and> Rr (xs @ [x])}

   590       else {x. x \<le> w \<and> Rr (xs @ [x])})"

   591 by(auto, case_tac "x = Suc w", auto)

   592 

   593 lemma [simp]: "Minr Rr xs w \<le> w \<Longrightarrow> Minr Rr xs (Suc w) = Minr Rr xs w"

   594 apply(simp add: Minr.simps, auto)

   595 apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)

   596 done

   597 

   598 lemma [simp]: "\<forall>x\<le>w. \<not> Rr (xs @ [x]) \<Longrightarrow>  

   599                            {x. x \<le> w \<and> Rr (xs @ [x])} = {} "

   600 by auto

   601 

   602 lemma [simp]: "\<lbrakk>Minr Rr xs w = Suc w; Rr (xs @ [Suc w])\<rbrakk> \<Longrightarrow> 

   603                                        Minr Rr xs (Suc w) = Suc w"

   604 apply(simp add: Minr.simps)

   605 apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)

   606 done

   607  

   608 lemma [simp]: "\<lbrakk>Minr Rr xs w = Suc w; \<not> Rr (xs @ [Suc w])\<rbrakk> \<Longrightarrow> 

   609                                    Minr Rr xs (Suc w) = Suc (Suc w)"

   610 apply(simp add: Minr.simps)

   611 apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)

   612 apply(subgoal_tac "Min {x. x \<le> w \<and> Rr (xs @ [x])} \<in> 

   613                                 {x. x \<le> w \<and> Rr (xs @ [x])}", simp)

   614 apply(rule_tac Min_in, auto)

   615 done

   616 

   617 lemma Minr_Suc_simp: 

   618    "Minr Rr xs (Suc w) = 

   619       (if Minr Rr xs w \<le> w then Minr Rr xs w

   620        else if (Rr (xs @ [Suc w])) then (Suc w)

   621        else Suc (Suc w))"

   622 by(insert Minr_range[of Rr xs w], auto)

   623 

   624 text {* 

   625   @{text "rec_Minr"} is the recursive function 

   626   used to implement @{text "Minr"}:

   627   if @{text "Rr"} is implemented by a recursive function @{text "recf"},

   628   then @{text "rec_Minr recf"} is the recursive function used to 

   629   implement @{text "Minr Rr"}

   630  *}

   631 fun rec_Minr :: "recf \<Rightarrow> recf"

   632   where

   633   "rec_Minr rf = 

   634      (let vl = arity rf

   635       in let rq = rec_all (id vl (vl - 1)) (Cn (Suc vl) 

   636               rec_not [Cn (Suc vl) rf 

   637                     (get_fstn_args (Suc vl) (vl - 1) @

   638                                         [id (Suc vl) (vl)])]) 

   639       in  rec_sigma rq)"

   640 

   641 lemma length_getpren_params[simp]: "length (get_fstn_args m n) = n"

   642 by(induct n, auto simp: get_fstn_args.simps)

   643 

   644 lemma length_app:

   645   "(length (get_fstn_args (arity rf - Suc 0)

   646                            (arity rf - Suc 0)

   647    @ [Cn (arity rf - Suc 0) (constn 0)

   648            [recf.id (arity rf - Suc 0) 0]]))

   649     = (Suc (arity rf - Suc 0))"

   650   apply(simp)

   651 done

   652 

   653 lemma primerec_accum: "primerec (rec_accum rf) n \<Longrightarrow> primerec rf n"

   654 apply(auto simp: rec_accum.simps Let_def)

   655 apply(erule_tac prime_pr_reverse, simp)

   656 apply(erule_tac prime_cn_reverse, simp only: length_app)

   657 done

   658 

   659 lemma primerec_all: "primerec (rec_all rt rf) n \<Longrightarrow>

   660                        primerec rt n \<and> primerec rf (Suc n)"

   661 apply(simp add: rec_all.simps Let_def)

   662 apply(erule_tac prime_cn_reverse, simp)

   663 apply(erule_tac prime_cn_reverse, simp)

   664 apply(erule_tac x = n in allE, simp add: nth_append primerec_accum)

   665 done

   666 

   667 lemma min_Suc_Suc[simp]: "min (Suc (Suc x)) x = x"

   668  by auto

   669 

   670 declare numeral_3_eq_3[simp]

   671 

   672 lemma [intro]: "primerec rec_pred (Suc 0)"

   673 apply(simp add: rec_pred_def)

   674 apply(rule_tac prime_cn, auto)

   675 apply(case_tac i, auto intro: prime_id)

   676 done

   677 

   678 lemma [intro]: "primerec rec_minus (Suc (Suc 0))"

   679   apply(auto simp: rec_minus_def)

   680   done

   681 

   682 lemma [intro]: "primerec (constn n) (Suc 0)"

   683   apply(induct n)

   684   apply(auto simp: constn.simps intro: prime_z prime_cn prime_s)

   685   done

   686 

   687 lemma [intro]: "primerec rec_sg (Suc 0)" 

   688   apply(simp add: rec_sg_def)

   689   apply(rule_tac k = "Suc (Suc 0)" in prime_cn, auto)

   690   apply(case_tac i, auto)

   691   apply(case_tac ia, auto intro: prime_id)

   692   done

   693 

   694 lemma [simp]: "length (get_fstn_args m n) = n"

   695   apply(induct n)

   696   apply(auto simp: get_fstn_args.simps)

   697   done

   698 

   699 lemma  primerec_getpren[elim]: "\<lbrakk>i < n; n \<le> m\<rbrakk> \<Longrightarrow> primerec (get_fstn_args m n ! i) m"

   700 apply(induct n, auto simp: get_fstn_args.simps)

   701 apply(case_tac "i = n", auto simp: nth_append intro: prime_id)

   702 done

   703 

   704 lemma [intro]: "primerec rec_add (Suc (Suc 0))"

   705 apply(simp add: rec_add_def)

   706 apply(rule_tac prime_pr, auto)

   707 done

   708 

   709 lemma [intro]:"primerec rec_mult (Suc (Suc 0))"

   710 apply(simp add: rec_mult_def )

   711 apply(rule_tac prime_pr, auto intro: prime_z)

   712 apply(case_tac i, auto intro: prime_id)

   713 done  

   714 

   715 lemma [elim]: "\<lbrakk>primerec rf n; n \<ge> Suc (Suc 0)\<rbrakk>   \<Longrightarrow> 

   716                         primerec (rec_accum rf) n"

   717 apply(auto simp: rec_accum.simps)

   718 apply(simp add: nth_append, auto)

   719 apply(case_tac i, auto intro: prime_id)

   720 apply(auto simp: nth_append)

   721 done

   722 

   723 lemma primerec_all_iff: 

   724   "\<lbrakk>primerec rt n; primerec rf (Suc n); n > 0\<rbrakk> \<Longrightarrow> 

   725                                  primerec (rec_all rt rf) n"

   726   apply(simp add: rec_all.simps, auto)

   727   apply(auto, simp add: nth_append, auto)

   728   done

   729 

   730 lemma [simp]: "Rr (xs @ [0]) \<Longrightarrow> 

   731                    Min {x. x = (0::nat) \<and> Rr (xs @ [x])} = 0"

   732 by(rule_tac Min_eqI, simp, simp, simp)

   733 

   734 lemma [intro]: "primerec rec_not (Suc 0)"

   735 apply(simp add: rec_not_def)

   736 apply(rule prime_cn, auto)

   737 apply(case_tac i, auto intro: prime_id)

   738 done

   739 

   740 lemma Min_false1[simp]: "\<lbrakk>\<not> Min {uu. uu \<le> w \<and> 0 < rec_exec rf (xs @ [uu])} \<le> w;

   741        x \<le> w; 0 < rec_exec rf (xs @ [x])\<rbrakk>

   742       \<Longrightarrow>  False"

   743 apply(subgoal_tac "finite {uu. uu \<le> w \<and> 0 < rec_exec rf (xs @ [uu])}")

   744 apply(subgoal_tac "{uu. uu \<le> w \<and> 0 < rec_exec rf (xs @ [uu])} \<noteq> {}")

   745 apply(simp add: Min_le_iff, simp)

   746 apply(rule_tac x = x in exI, simp)

   747 apply(simp)

   748 done

   749 

   750 lemma sigma_minr_lemma: 

   751   assumes prrf:  "primerec rf (Suc (length xs))"

   752   shows "UF.Sigma (rec_exec (rec_all (recf.id (Suc (length xs)) (length xs))

   753      (Cn (Suc (Suc (length xs))) rec_not

   754       [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) 

   755        (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])))

   756       (xs @ [w]) =

   757        Minr (\<lambda>args. 0 < rec_exec rf args) xs w"

   758 proof(induct w)

   759   let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"

   760   let ?rf = "(Cn (Suc (Suc (length xs))) 

   761     rec_not [Cn (Suc (Suc (length xs))) rf 

   762     (get_fstn_args (Suc (Suc (length xs))) (length xs) @ 

   763                 [recf.id (Suc (Suc (length xs))) 

   764     (Suc ((length xs)))])])"

   765   let ?rq = "(rec_all ?rt ?rf)"

   766   have prrf: "primerec ?rf (Suc (length (xs @ [0]))) \<and>

   767         primerec ?rt (length (xs @ [0]))"

   768     apply(auto simp: prrf nth_append)+

   769     done

   770   show "Sigma (rec_exec (rec_all ?rt ?rf)) (xs @ [0])

   771        = Minr (\<lambda>args. 0 < rec_exec rf args) xs 0"

   772     apply(simp add: Sigma.simps)

   773     apply(simp only: prrf all_lemma,  

   774           auto simp: rec_exec.simps get_fstn_args_take Minr.simps)

   775     apply(rule_tac Min_eqI, auto)

   776     done

   777 next

   778   fix w

   779   let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"

   780   let ?rf = "(Cn (Suc (Suc (length xs))) 

   781     rec_not [Cn (Suc (Suc (length xs))) rf 

   782     (get_fstn_args (Suc (Suc (length xs))) (length xs) @ 

   783                 [recf.id (Suc (Suc (length xs))) 

   784     (Suc ((length xs)))])])"

   785   let ?rq = "(rec_all ?rt ?rf)"

   786   assume ind:

   787     "Sigma (rec_exec (rec_all ?rt ?rf)) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w"

   788   have prrf: "primerec ?rf (Suc (length (xs @ [Suc w]))) \<and>

   789         primerec ?rt (length (xs @ [Suc w]))"

   790     apply(auto simp: prrf nth_append)+

   791     done

   792   show "UF.Sigma (rec_exec (rec_all ?rt ?rf))

   793          (xs @ [Suc w]) =

   794         Minr (\<lambda>args. 0 < rec_exec rf args) xs (Suc w)"

   795     apply(auto simp: Sigma_Suc_simp_rewrite ind Minr_Suc_simp)

   796     apply(simp_all only: prrf all_lemma)

   797     apply(auto simp: rec_exec.simps get_fstn_args_take Let_def Minr.simps split: if_splits)

   798     apply(drule_tac Min_false1, simp, simp, simp)

   799     apply(case_tac "x = Suc w", simp, simp)

   800     apply(drule_tac Min_false1, simp, simp, simp)

   801     apply(drule_tac Min_false1, simp, simp, simp)

   802     done

   803 qed

   804 

   805 text {*

   806   The correctness of @{text "rec_Minr"}.

   807   *}

   808 lemma Minr_lemma: "

   809   \<lbrakk>primerec rf (Suc (length xs))\<rbrakk> 

   810      \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = 

   811             Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"

   812 proof -

   813   let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"

   814   let ?rf = "(Cn (Suc (Suc (length xs))) 

   815     rec_not [Cn (Suc (Suc (length xs))) rf 

   816     (get_fstn_args (Suc (Suc (length xs))) (length xs) @ 

   817                 [recf.id (Suc (Suc (length xs))) 

   818     (Suc ((length xs)))])])"

   819   let ?rq = "(rec_all ?rt ?rf)"

   820   assume h: "primerec rf (Suc (length xs))"

   821   have h1: "primerec ?rq (Suc (length xs))"

   822     apply(rule_tac primerec_all_iff)

   823     apply(auto simp: h nth_append)+

   824     done

   825   moreover have "arity rf = Suc (length xs)"

   826     using h by auto

   827   ultimately show "rec_exec (rec_Minr rf) (xs @ [w]) = 

   828     Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"

   829     apply(simp add: rec_exec.simps rec_Minr.simps arity.simps Let_def 

   830                     sigma_lemma all_lemma)

   831     apply(rule_tac  sigma_minr_lemma)

   832     apply(simp add: h)

   833     done

   834 qed

   835     

   836 text {* 

   837   @{text "rec_le"} is the comparasion function 

   838   which compares its two arguments, testing whether the 

   839   first is less or equal to the second.

   840   *}

   841 definition rec_le :: "recf"

   842   where

   843   "rec_le = Cn (Suc (Suc 0)) rec_disj [rec_less, rec_eq]"

   844 

   845 text {*

   846   The correctness of @{text "rec_le"}.

   847   *}

   848 lemma le_lemma: 

   849   "\<And>x y. rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)"

   850 by(auto simp: rec_le_def rec_exec.simps)

   851 

   852 text {*

   853   Defintiion of @{text "Max[Rr]"} on page 77 of Boolos's book.

   854 *}

   855 

   856 fun Maxr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> nat"

   857   where

   858   "Maxr Rr xs w = (let setx = {y. y \<le> w \<and> Rr (xs @[y])} in 

   859                   if setx = {} then 0

   860                   else Max setx)"

   861 

   862 text {*

   863   @{text "rec_maxr"} is the recursive function 

   864   used to implementation @{text "Maxr"}.

   865   *}

   866 fun rec_maxr :: "recf \<Rightarrow> recf"

   867   where

   868   "rec_maxr rr = (let vl = arity rr in 

   869                   let rt = id (Suc vl) (vl - 1) in

   870                   let rf1 = Cn (Suc (Suc vl)) rec_le 

   871                     [id (Suc (Suc vl)) 

   872                      ((Suc vl)), id (Suc (Suc vl)) (vl)] in

   873                   let rf2 = Cn (Suc (Suc vl)) rec_not 

   874                       [Cn (Suc (Suc vl)) 

   875                            rr (get_fstn_args (Suc (Suc vl)) 

   876                             (vl - 1) @ 

   877                              [id (Suc (Suc vl)) ((Suc vl))])] in

   878                   let rf = Cn (Suc (Suc vl)) rec_disj [rf1, rf2] in

   879                   let rq = rec_all rt rf  in

   880                   let Qf = Cn (Suc vl) rec_not [rec_all rt rf]

   881                   in Cn vl (rec_sigma Qf) (get_fstn_args vl vl @

   882                                                          [id vl (vl - 1)]))"

   883 

   884 declare rec_maxr.simps[simp del] Maxr.simps[simp del] 

   885 declare le_lemma[simp]

   886 lemma [simp]: "(min (Suc (Suc (Suc (x)))) (x)) = x"

   887 by simp

   888 

   889 declare numeral_2_eq_2[simp]

   890 

   891 lemma [intro]: "primerec rec_disj (Suc (Suc 0))"

   892   apply(simp add: rec_disj_def, auto)

   893   apply(auto)

   894   apply(case_tac ia, auto intro: prime_id)

   895   done

   896 

   897 lemma [intro]: "primerec rec_less (Suc (Suc 0))"

   898   apply(simp add: rec_less_def, auto)

   899   apply(auto)

   900   apply(case_tac ia , auto intro: prime_id)

   901   done

   902 

   903 lemma [intro]: "primerec rec_eq (Suc (Suc 0))"

   904   apply(simp add: rec_eq_def)

   905   apply(rule_tac prime_cn, auto)

   906   apply(case_tac i, auto)

   907   apply(case_tac ia, auto)

   908   apply(case_tac [!] i, auto intro: prime_id)

   909   done

   910 

   911 lemma [intro]: "primerec rec_le (Suc (Suc 0))"

   912   apply(simp add: rec_le_def)

   913   apply(rule_tac prime_cn, auto)

   914   apply(case_tac i, auto)

   915   done

   916 

   917 lemma [simp]:  

   918   "length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) =  

   919                                                   ys @ [ys ! n]"

   920 apply(simp)

   921 apply(subgoal_tac "\<exists> xs y. ys = xs @ [y]", auto)

   922 apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI)

   923 apply(case_tac "ys = []", simp_all)

   924 done

   925 

   926 lemma Maxr_Suc_simp: 

   927   "Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w

   928      else Maxr Rr xs w)"

   929 apply(auto simp: Maxr.simps)

   930 apply(rule_tac max_absorb1)

   931 apply(subgoal_tac "(Max {y. y \<le> w \<and> Rr (xs @ [y])} \<le> (Suc w)) =

   932   (\<forall>a\<in>{y. y \<le> w \<and> Rr (xs @ [y])}. a \<le> (Suc w))", simp)

   933 apply(rule_tac Max_le_iff, auto)

   934 done

   935 

   936 

   937 lemma [simp]: "min (Suc n) n = n" by simp

   938 

   939 lemma Sigma_0: "\<forall> i \<le> n. (f (xs @ [i]) = 0) \<Longrightarrow> 

   940                               Sigma f (xs @ [n]) = 0"

   941 apply(induct n, simp add: Sigma.simps)

   942 apply(simp add: Sigma_Suc_simp_rewrite)

   943 done

   944   

   945 lemma [elim]: "\<forall>k<Suc w. f (xs @ [k]) = Suc 0

   946         \<Longrightarrow> Sigma f (xs @ [w]) = Suc w"

   947 apply(induct w)

   948 apply(simp add: Sigma.simps, simp)

   949 apply(simp add: Sigma.simps)

   950 done

   951 

   952 lemma Sigma_max_point: "\<lbrakk>\<forall> k < ma. f (xs @ [k]) = 1;

   953         \<forall> k \<ge> ma. f (xs @ [k]) = 0; ma \<le> w\<rbrakk>

   954     \<Longrightarrow> Sigma f (xs @ [w]) = ma"

   955 apply(induct w, auto)

   956 apply(rule_tac Sigma_0, simp)

   957 apply(simp add: Sigma_Suc_simp_rewrite)

   958 apply(case_tac "ma = Suc w", auto)

   959 done

   960 

   961 lemma Sigma_Max_lemma: 

   962   assumes prrf: "primerec rf (Suc (length xs))"

   963   shows "UF.Sigma (rec_exec (Cn (Suc (Suc (length xs))) rec_not

   964   [rec_all (recf.id (Suc (Suc (length xs))) (length xs))

   965   (Cn (Suc (Suc (Suc (length xs)))) rec_disj

   966   [Cn (Suc (Suc (Suc (length xs)))) rec_le

   967   [recf.id (Suc (Suc (Suc (length xs)))) (Suc (Suc (length xs))), 

   968   recf.id (Suc (Suc (Suc (length xs)))) (Suc (length xs))],

   969   Cn (Suc (Suc (Suc (length xs)))) rec_not

   970   [Cn (Suc (Suc (Suc (length xs)))) rf

   971   (get_fstn_args (Suc (Suc (Suc (length xs)))) (length xs) @ 

   972   [recf.id (Suc (Suc (Suc (length xs)))) (Suc (Suc (length xs)))])]])]))

   973   ((xs @ [w]) @ [w]) =

   974        Maxr (\<lambda>args. 0 < rec_exec rf args) xs w"

   975 proof -

   976   let ?rt = "(recf.id (Suc (Suc (length xs))) ((length xs)))"

   977   let ?rf1 = "Cn (Suc (Suc (Suc (length xs))))

   978     rec_le [recf.id (Suc (Suc (Suc (length xs)))) 

   979     ((Suc (Suc (length xs)))), recf.id 

   980     (Suc (Suc (Suc (length xs)))) ((Suc (length xs)))]"

   981   let ?rf2 = "Cn (Suc (Suc (Suc (length xs)))) rf 

   982                (get_fstn_args (Suc (Suc (Suc (length xs))))

   983     (length xs) @ 

   984     [recf.id (Suc (Suc (Suc (length xs))))    

   985     ((Suc (Suc (length xs))))])"

   986   let ?rf3 = "Cn (Suc (Suc (Suc (length xs)))) rec_not [?rf2]"

   987   let ?rf = "Cn (Suc (Suc (Suc (length xs)))) rec_disj [?rf1, ?rf3]"

   988   let ?rq = "rec_all ?rt ?rf"

   989   let ?notrq = "Cn (Suc (Suc (length xs))) rec_not [?rq]"

   990   show "?thesis"

   991   proof(auto simp: Maxr.simps)

   992     assume h: "\<forall>x\<le>w. rec_exec rf (xs @ [x]) = 0"

   993     have "primerec ?rf (Suc (length (xs @ [w, i]))) \<and> 

   994           primerec ?rt (length (xs @ [w, i]))"

   995       using prrf

   996       apply(auto)

   997       apply(case_tac i, auto)

   998       apply(case_tac ia, auto simp: h nth_append)

   999       done

  1000     hence "Sigma (rec_exec ?notrq) ((xs@[w])@[w]) = 0"

  1001       apply(rule_tac Sigma_0)

  1002       apply(auto simp: rec_exec.simps all_lemma

  1003                        get_fstn_args_take nth_append h)

  1004       done

  1005     thus "UF.Sigma (rec_exec ?notrq)

  1006       (xs @ [w, w]) = 0"

  1007       by simp

  1008   next

  1009     fix x

  1010     assume h: "x \<le> w" "0 < rec_exec rf (xs @ [x])"

  1011     hence "\<exists> ma. Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} = ma"

  1012       by auto

  1013     from this obtain ma where k1: 

  1014       "Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} = ma" ..

  1015     hence k2: "ma \<le> w \<and> 0 < rec_exec rf (xs @ [ma])"

  1016       using h

  1017       apply(subgoal_tac

  1018         "Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} \<in>  {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}")

  1019       apply(erule_tac CollectE, simp)

  1020       apply(rule_tac Max_in, auto)

  1021       done

  1022     hence k3: "\<forall> k < ma. (rec_exec ?notrq (xs @ [w, k]) = 1)"

  1023       apply(auto simp: nth_append)

  1024       apply(subgoal_tac "primerec ?rf (Suc (length (xs @ [w, k]))) \<and> 

  1025         primerec ?rt (length (xs @ [w, k]))")

  1026       apply(auto simp: rec_exec.simps all_lemma get_fstn_args_take nth_append)

  1027       using prrf

  1028       apply(case_tac i, auto)

  1029       apply(case_tac ia, auto simp: h nth_append)

  1030       done    

  1031     have k4: "\<forall> k \<ge> ma. (rec_exec ?notrq (xs @ [w, k]) = 0)"

  1032       apply(auto)

  1033       apply(subgoal_tac "primerec ?rf (Suc (length (xs @ [w, k]))) \<and> 

  1034         primerec ?rt (length (xs @ [w, k]))")

  1035       apply(auto simp: rec_exec.simps all_lemma get_fstn_args_take nth_append)

  1036       apply(subgoal_tac "x \<le> Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}",

  1037         simp add: k1)

  1038       apply(rule_tac Max_ge, auto)

  1039       using prrf

  1040       apply(case_tac i, auto)

  1041       apply(case_tac ia, auto simp: h nth_append)

  1042       done 

  1043     from k3 k4 k1 have "Sigma (rec_exec ?notrq) ((xs @ [w]) @ [w]) = ma"

  1044       apply(rule_tac Sigma_max_point, simp, simp, simp add: k2)

  1045       done

  1046     from k1 and this show "Sigma (rec_exec ?notrq) (xs @ [w, w]) =

  1047       Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}"

  1048       by simp

  1049   qed  

  1050 qed

  1051 

  1052 text {*

  1053   The correctness of @{text "rec_maxr"}.

  1054   *}

  1055 lemma Maxr_lemma:

  1056  assumes h: "primerec rf (Suc (length xs))"

  1057  shows   "rec_exec (rec_maxr rf) (xs @ [w]) = 

  1058             Maxr (\<lambda> args. 0 < rec_exec rf args) xs w"

  1059 proof -

  1060   from h have "arity rf = Suc (length xs)"

  1061     by auto

  1062   thus "?thesis"

  1063   proof(simp add: rec_exec.simps rec_maxr.simps nth_append get_fstn_args_take)

  1064     let ?rt = "(recf.id (Suc (Suc (length xs))) ((length xs)))"

  1065     let ?rf1 = "Cn (Suc (Suc (Suc (length xs))))

  1066                      rec_le [recf.id (Suc (Suc (Suc (length xs)))) 

  1067               ((Suc (Suc (length xs)))), recf.id 

  1068              (Suc (Suc (Suc (length xs)))) ((Suc (length xs)))]"

  1069     let ?rf2 = "Cn (Suc (Suc (Suc (length xs)))) rf 

  1070                (get_fstn_args (Suc (Suc (Suc (length xs))))

  1071                 (length xs) @ 

  1072                   [recf.id (Suc (Suc (Suc (length xs))))    

  1073                            ((Suc (Suc (length xs))))])"

  1074     let ?rf3 = "Cn (Suc (Suc (Suc (length xs)))) rec_not [?rf2]"

  1075     let ?rf = "Cn (Suc (Suc (Suc (length xs)))) rec_disj [?rf1, ?rf3]"

  1076     let ?rq = "rec_all ?rt ?rf"

  1077     let ?notrq = "Cn (Suc (Suc (length xs))) rec_not [?rq]"

  1078     have prt: "primerec ?rt (Suc (Suc (length xs)))"

  1079       by(auto intro: prime_id)

  1080     have prrf: "primerec ?rf (Suc (Suc (Suc (length xs))))"

  1081       apply(auto)

  1082       apply(case_tac i, auto)

  1083       apply(case_tac ia, auto intro: prime_id)

  1084       apply(simp add: h)

  1085       apply(simp add: nth_append, auto intro: prime_id)

  1086       done

  1087     from prt and prrf have prrq: "primerec ?rq 

  1088                                        (Suc (Suc (length xs)))"

  1089       by(erule_tac primerec_all_iff, auto)

  1090     hence prnotrp: "primerec ?notrq (Suc (length ((xs @ [w]))))"

  1091       by(rule_tac prime_cn, auto)

  1092     have g1: "rec_exec (rec_sigma ?notrq) ((xs @ [w]) @ [w]) 

  1093       = Maxr (\<lambda>args. 0 < rec_exec rf args) xs w"

  1094       using prnotrp

  1095       using sigma_lemma

  1096       apply(simp only: sigma_lemma)

  1097       apply(rule_tac Sigma_Max_lemma)

  1098       apply(simp add: h)

  1099       done

  1100     thus "rec_exec (rec_sigma ?notrq)

  1101      (xs @ [w, w]) =

  1102     Maxr (\<lambda>args. 0 < rec_exec rf args) xs w"

  1103       apply(simp)

  1104       done

  1105   qed

  1106 qed

  1107       

  1108 text {* 

  1109   @text "quo"} is the formal specification of division.

  1110  *}

  1111 fun quo :: "nat list \<Rightarrow> nat"

  1112   where

  1113   "quo [x, y] = (let Rr = 

  1114                          (\<lambda> zs. ((zs ! (Suc 0) * zs ! (Suc (Suc 0))

  1115                                  \<le> zs ! 0) \<and> zs ! Suc 0 \<noteq> (0::nat)))

  1116                  in Maxr Rr [x, y] x)"

  1117  

  1118 declare quo.simps[simp del]

  1119 

  1120 text {*

  1121   The following lemmas shows more directly the menaing of @{text "quo"}:

  1122   *}

  1123 lemma [elim!]: "y > 0 \<Longrightarrow> quo [x, y] = x div y"

  1124 proof(simp add: quo.simps Maxr.simps, auto,

  1125       rule_tac Max_eqI, simp, auto)

  1126   fix xa ya

  1127   assume h: "y * ya \<le> x"  "y > 0"

  1128   hence "(y * ya) div y \<le> x div y"

  1129     by(insert div_le_mono[of "y * ya" x y], simp)

  1130   from this and h show "ya \<le> x div y" by simp

  1131 next

  1132   fix xa

  1133   show "y * (x div y) \<le> x"

  1134     apply(subgoal_tac "y * (x div y) + x mod y = x")

  1135     apply(rule_tac k = "x mod y" in add_leD1, simp)