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 section {* Univeral Function *}

    13 

    14 subsection {* The construction of component functions *}

    15 

    16 text {*

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

    18   *}

    19 

    20 text {*

    21   The recursive function used to do arithmatic addition.

    22 *}

    23 definition rec_add :: "recf"

    24   where

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

    26 

    27 text {*

    28   The recursive function used to do arithmatic multiplication.

    29 *}

    30 definition rec_mult :: "recf"

    31   where

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

    33 

    34 text {*

    35   The recursive function used to do arithmatic precede.

    36 *}

    37 definition rec_pred :: "recf"

    38   where

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

    40 

    41 text {*

    42   The recursive function used to do arithmatic subtraction.

    43 *}

    44 definition rec_minus :: "recf" 

    45   where

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

    47 

    48 text {*

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

    50   nature number @{text "n"}.

    51 *}

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

    53   where

    54   "constn 0 = z"  |

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

    56 

    57 

    58 text {*

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

    60 *}

    61 definition rec_sg :: "recf"

    62   where

    63   "rec_sg = Cn 1 rec_minus [constn 1, 

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

    65 

    66 text {*

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

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

    69   *}

    70 definition rec_less :: "recf"

    71   where

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

    73 

    74 text {*

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

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

    77   *}

    78 definition rec_not :: "recf"

    79   where

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

    81 

    82 text {*

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

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

    85   *}

    86 definition rec_eq :: "recf"

    87   where

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

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

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

    91 

    92 text {*

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

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

    95   otherwise.

    96   *}

    97 definition rec_conj :: "recf"

    98   where

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

   100 

   101 text {*

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

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

   104   otherwise.

   105   *}

   106 definition rec_disj :: "recf"

   107   where

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

   109 

   110 

   111 text {*

   112   Computes the arity of recursive function.

   113   *}

   114 

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

   116   where

   117   "arity z = 1" 

   118 | "arity s = 1"

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

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

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

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

   123 

   124 text {*

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

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

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

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

   129   *}

   130 

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

   132   where

   133   "get_fstn_args n 0 = []"

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

   135 

   136 text {*

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

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

   139   \[

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

   141   \]

   142 *}

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

   144   where

   145   "rec_sigma rf = 

   146        (let vl = arity rf in 

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

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

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

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

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

   152 

   153 text {*

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

   155   reursive functions. The function is defined such that 

   156   it always returns meaningful results for primitive recursive 

   157   functions.

   158   *}

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

   160   where

   161   "rec_exec z xs = 0" |

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

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

   164   "rec_exec (Cn n f gs) xs = 

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

   166                                   rec_exec f ys)" | 

   167   "rec_exec (Pr n f g) xs = 

   168      (if last xs = 0 then 

   169                   rec_exec f (butlast xs)

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

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

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

   173 by pat_completeness auto

   174 termination

   175 proof 

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

   177     by auto

   178 next

   179   fix n f gs xs x

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

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

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

   183     by(induct gs, auto)

   184 next

   185   fix n f gs xs x

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

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

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

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

   190     by(auto)

   191 next

   192   fix n f g xs

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

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

   195     by auto

   196 next

   197   fix n f g xs

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

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

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

   201     by auto

   202 next

   203   fix n f g xs

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

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

   206     by auto

   207 next

   208   fix n f xs x

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

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

   211     by auto

   212 qed

   213 

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

   215 

   216 text {*

   217   Correctness of @{text "rec_add"}.

   218   *}

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

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

   221 

   222 text {*

   223   Correctness of @{text "rec_mult"}.

   224   *}

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

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

   227 

   228 text {*

   229   Correctness of @{text "rec_pred"}.

   230   *}

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

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

   233 

   234 text {*

   235   Correctness of @{text "rec_minus"}.

   236   *}

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

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

   239 

   240 text {*

   241   Correctness of @{text "rec_sg"}.

   242   *}

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

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

   245 

   246 text {*

   247   Correctness of @{text "constn"}.

   248   *}

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

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

   251 

   252 text {*

   253   Correctness of @{text "rec_less"}.

   254   *}

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

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

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

   258   rec_less_def minus_lemma sg_lemma)

   259 

   260 text {*

   261   Correctness of @{text "rec_not"}.

   262   *}

   263 lemma not_lemma: 

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

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

   266   constn_lemma minus_lemma)

   267 

   268 text {*

   269   Correctness of @{text "rec_eq"}.

   270   *}

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

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

   273 

   274 text {*

   275   Correctness of @{text "rec_conj"}.

   276   *}

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

   278                                                        else 1)"

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

   280 

   281 

   282 text {*

   283   Correctness of @{text "rec_disj"}.

   284   *}

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

   286                                                      else 1)"

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

   288 

   289 

   290 text {*

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

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

   293   with arity @{text "n"}.

   294   *}

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

   296   where

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

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

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

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

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

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

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

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

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

   306 

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

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

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

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

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

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

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

   314 

   315 declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp] 

   316         minus_lemma[simp] sg_lemma[simp] constn_lemma[simp] 

   317         less_lemma[simp] not_lemma[simp] eq_lemma[simp]

   318         conj_lemma[simp] disj_lemma[simp]

   319 

   320 text {*

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

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

   323   *}

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

   325   where

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

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

   328                        g xs)) "

   329 by pat_completeness auto

   330 termination

   331 proof

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

   333 next

   334   fix g xs

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

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

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

   338     by auto

   339 qed

   340 

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

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

   343         rec_sigma.simps[simp del]

   344 

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

   346  by(simp add: arity.simps)

   347 

   348 lemma rec_pr_0_simp_rewrite: "

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

   350 by(simp add: rec_exec.simps)

   351 

   352 lemma rec_pr_0_simp_rewrite_single_param: "

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

   354 by(simp add: rec_exec.simps)

   355 

   356 lemma rec_pr_Suc_simp_rewrite: 

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

   358                        rec_exec g (xs @ [x] @ 

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

   360 by(simp add: rec_exec.simps)

   361 

   362 lemma rec_pr_Suc_simp_rewrite_single_param: 

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

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

   365 by(simp add: rec_exec.simps)

   366 

   367 lemma Sigma_0_simp_rewrite_single_param:

   368   "Sigma f [0] = f [0]"

   369 by(simp add: Sigma.simps)

   370 

   371 lemma Sigma_0_simp_rewrite:

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

   373 by(simp add: Sigma.simps)

   374 

   375 lemma Sigma_Suc_simp_rewrite: 

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

   377 by(simp add: Sigma.simps)

   378 

   379 lemma Sigma_Suc_simp_rewrite_single: 

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

   381 by(simp add: Sigma.simps)

   382 

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

   384 by(simp add: nth_append)

   385   

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

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

   388 proof(induct n)

   389   case 0 thus "?case"

   390     by(simp add: get_fstn_args.simps)

   391 next

   392   case (Suc n) thus "?case"

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

   394              take_Suc_conv_app_nth)

   395 qed

   396     

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

   398   apply(case_tac f)

   399   apply(auto simp: arity.simps )

   400   apply(erule_tac prime_mn_reverse)

   401   done

   402 

   403 lemma rec_sigma_Suc_simp_rewrite: 

   404   "primerec f (Suc (length xs))

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

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

   407   apply(induct x)

   408   apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite

   409                    rec_exec.simps get_fstn_args_take)

   410   done      

   411 

   412 text {*

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

   414   *}

   415 lemma sigma_lemma: 

   416   "primerec rg (Suc (length xs))

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

   418 apply(induct x)

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

   420          get_fstn_args_take Sigma_0_simp_rewrite

   421          Sigma_Suc_simp_rewrite) 

   422 done

   423 

   424 text {*

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

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

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

   428                \<dots> 

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

   430 *}

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

   432   where

   433   "rec_accum rf = 

   434        (let vl = arity rf in 

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

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

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

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

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

   440 

   441 text {*

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

   443   *}

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

   445   where

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

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

   448                        f xs))"

   449 by pat_completeness auto

   450 termination

   451 proof

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

   453     by auto

   454 next

   455   fix f xs

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

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

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

   459     by auto

   460 qed

   461 

   462 lemma rec_accum_Suc_simp_rewrite: 

   463   "primerec f (Suc (length xs))

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

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

   466   apply(induct x)

   467   apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite

   468                    rec_exec.simps get_fstn_args_take)

   469   done  

   470 

   471 text {*

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

   473 *}

   474 lemma accum_lemma :

   475   "primerec rg (Suc (length xs))

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

   477 apply(induct x)

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

   479                      get_fstn_args_take)

   480 done

   481 

   482 declare rec_accum.simps [simp del]

   483 

   484 text {*

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

   486   computes the charactrization function of the following FOL formula:

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

   488 *}

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

   490   where

   491   "rec_all rt rf = 

   492     (let vl = arity rf in

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

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

   495 

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

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

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

   499 apply(induct x, simp_all add: rec_accum_Suc_simp_rewrite)

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

   501       auto)

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

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

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

   505 done

   506 

   507 text {*

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

   509   *}

   510 lemma all_lemma: 

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

   512     primerec rt (length xs)\<rbrakk>

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

   514                                                                                               else 0)"

   515 apply(auto simp: rec_all.simps)

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

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

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

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

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

   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, simp)

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

   524 done

   525 

   526 text {*

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

   528   computes the charactrization function of the following FOL formula:

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

   530 *}

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

   532   where

   533   "rec_ex rt rf = 

   534        (let vl = arity rf in 

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

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

   537 

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

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

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

   541 apply(induct x, simp_all add: rec_sigma_Suc_simp_rewrite)

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

   543                 get_fstn_args_take, auto)

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

   545 done

   546 

   547 text {*

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

   549   *}

   550 lemma ex_lemma:"

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

   552    primerec rt (length xs)\<rbrakk>

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

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

   555      else 0))"

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

   557             split: if_splits)

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

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

   560 done

   561 

   562 text {*

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

   564 *}

   565 

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

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

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

   569                                        else (Min setx))"

   570 

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

   572 

   573 text {*

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

   575 *}

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

   577 apply(auto simp: Minr.simps)

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

   579 apply(erule_tac order_trans, simp)

   580 apply(rule_tac Min_le, auto)

   581 done

   582 

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

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

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

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

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

   588 

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

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

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

   592 done

   593 

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

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

   596 by auto

   597 

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

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

   600 apply(simp add: Minr.simps)

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

   602 done

   603  

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

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

   606 apply(simp add: Minr.simps)

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

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

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

   610 apply(rule_tac Min_in, auto)

   611 done

   612 

   613 lemma Minr_Suc_simp: 

   614    "Minr Rr xs (Suc w) = 

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

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

   617        else Suc (Suc w))"

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

   619 

   620 text {* 

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

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

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

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

   625   implement @{text "Minr Rr"}

   626  *}

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

   628   where

   629   "rec_Minr rf = 

   630      (let vl = arity rf

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

   632               rec_not [Cn (Suc vl) rf 

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

   634                                         [id (Suc vl) (vl)])]) 

   635       in  rec_sigma rq)"

   636 

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

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

   639 

   640 lemma length_app:

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

   642                            (arity rf - Suc 0)

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

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

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

   646   apply(simp)

   647 done

   648 

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

   650 apply(auto simp: rec_accum.simps Let_def)

   651 apply(erule_tac prime_pr_reverse, simp)

   652 apply(erule_tac prime_cn_reverse, simp only: length_app)

   653 done

   654 

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

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

   657 apply(simp add: rec_all.simps Let_def)

   658 apply(erule_tac prime_cn_reverse, simp)

   659 apply(erule_tac prime_cn_reverse, simp)

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

   661 done

   662 

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

   664  by auto

   665 

   666 declare numeral_3_eq_3[simp]

   667 

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

   669 apply(simp add: rec_pred_def)

   670 apply(rule_tac prime_cn, auto)

   671 apply(case_tac i, auto intro: prime_id)

   672 done

   673 

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

   675   apply(auto simp: rec_minus_def)

   676   done

   677 

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

   679   apply(induct n)

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

   681   done

   682 

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

   684   apply(simp add: rec_sg_def)

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

   686   apply(case_tac i, auto)

   687   apply(case_tac ia, auto intro: prime_id)

   688   done

   689 

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

   691   apply(induct n)

   692   apply(auto simp: get_fstn_args.simps)

   693   done

   694 

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

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

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

   698 done

   699 

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

   701 apply(simp add: rec_add_def)

   702 apply(rule_tac prime_pr, auto)

   703 done

   704 

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

   706 apply(simp add: rec_mult_def )

   707 apply(rule_tac prime_pr, auto intro: prime_z)

   708 apply(case_tac i, auto intro: prime_id)

   709 done  

   710 

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

   712                         primerec (rec_accum rf) n"

   713 apply(auto simp: rec_accum.simps)

   714 apply(simp add: nth_append, auto)

   715 apply(case_tac i, auto intro: prime_id)

   716 apply(auto simp: nth_append)

   717 done

   718 

   719 lemma primerec_all_iff: 

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

   721                                  primerec (rec_all rt rf) n"

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

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

   724   done

   725 

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

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

   728 by(rule_tac Min_eqI, simp, simp, simp)

   729 

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

   731 apply(simp add: rec_not_def)

   732 apply(rule prime_cn, auto)

   733 apply(case_tac i, auto intro: prime_id)

   734 done

   735 

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

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

   738       \<Longrightarrow>  False"

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

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

   741 apply(simp add: Min_le_iff, simp)

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

   743 apply(simp)

   744 done

   745 

   746 lemma sigma_minr_lemma: 

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

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

   749      (Cn (Suc (Suc (length xs))) rec_not

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

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

   752       (xs @ [w]) =

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

   754 proof(induct w)

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

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

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

   758     (get_fstn_args (Suc (Suc (length xs))) (length xs) @ 

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

   760     (Suc ((length xs)))])])"

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

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

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

   764     apply(auto simp: prrf nth_append)+

   765     done

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

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

   768     apply(simp add: Sigma.simps)

   769     apply(simp only: prrf all_lemma,  

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

   771     apply(rule_tac Min_eqI, auto)

   772     done

   773 next

   774   fix w

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

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

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

   778     (get_fstn_args (Suc (Suc (length xs))) (length xs) @ 

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

   780     (Suc ((length xs)))])])"

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

   782   assume ind:

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

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

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

   786     apply(auto simp: prrf nth_append)+

   787     done

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

   789          (xs @ [Suc w]) =

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

   791     apply(auto simp: Sigma_Suc_simp_rewrite ind Minr_Suc_simp)

   792     apply(simp_all only: prrf all_lemma)

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

   794     apply(drule_tac Min_false1, simp, simp, simp)

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

   796     apply(drule_tac Min_false1, simp, simp, simp)

   797     apply(drule_tac Min_false1, simp, simp, simp)

   798     done

   799 qed

   800 

   801 text {*

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

   803   *}

   804 lemma Minr_lemma: "

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

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

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

   808 proof -

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

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

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

   812     (get_fstn_args (Suc (Suc (length xs))) (length xs) @ 

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

   814     (Suc ((length xs)))])])"

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

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

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

   818     apply(rule_tac primerec_all_iff)

   819     apply(auto simp: h nth_append)+

   820     done

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

   822     using h by auto

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

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

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

   826                     sigma_lemma all_lemma)

   827     apply(rule_tac  sigma_minr_lemma)

   828     apply(simp add: h)

   829     done

   830 qed

   831     

   832 text {* 

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

   834   which compares its two arguments, testing whether the 

   835   first is less or equal to the second.

   836   *}

   837 definition rec_le :: "recf"

   838   where

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

   840 

   841 text {*

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

   843   *}

   844 lemma le_lemma: 

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

   846 by(auto simp: rec_le_def rec_exec.simps)

   847 

   848 text {*

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

   850 *}

   851 

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

   853   where

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

   855                   if setx = {} then 0

   856                   else Max setx)"

   857 

   858 text {*

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

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

   861   *}

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

   863   where

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

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

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

   867                     [id (Suc (Suc vl)) 

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

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

   870                       [Cn (Suc (Suc vl)) 

   871                            rr (get_fstn_args (Suc (Suc vl)) 

   872                             (vl - 1) @ 

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

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

   875                   let rq = rec_all rt rf  in

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

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

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

   879 

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

   881 declare le_lemma[simp]

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

   883 by simp

   884 

   885 declare numeral_2_eq_2[simp]

   886 

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

   888   apply(simp add: rec_disj_def, auto)

   889   apply(auto)

   890   apply(case_tac ia, auto intro: prime_id)

   891   done

   892 

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

   894   apply(simp add: rec_less_def, auto)

   895   apply(auto)

   896   apply(case_tac ia , auto intro: prime_id)

   897   done

   898 

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

   900   apply(simp add: rec_eq_def)

   901   apply(rule_tac prime_cn, auto)

   902   apply(case_tac i, auto)

   903   apply(case_tac ia, auto)

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

   905   done

   906 

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

   908   apply(simp add: rec_le_def)

   909   apply(rule_tac prime_cn, auto)

   910   apply(case_tac i, auto)

   911   done

   912 

   913 lemma [simp]:  

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

   915                                                   ys @ [ys ! n]"

   916 apply(simp)

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

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

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

   920 done

   921 

   922 lemma Maxr_Suc_simp: 

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

   924      else Maxr Rr xs w)"

   925 apply(auto simp: Maxr.simps Max.insert)

   926 apply(rule_tac Max_eqI, auto)

   927 done

   928 

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

   930 

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

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

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

   934 apply(simp add: Sigma_Suc_simp_rewrite)

   935 done

   936   

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

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

   939 apply(induct w)

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

   941 apply(simp add: Sigma.simps)

   942 done

   943 

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

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

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

   947 apply(induct w, auto)

   948 apply(rule_tac Sigma_0, simp)

   949 apply(simp add: Sigma_Suc_simp_rewrite)

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

   951 done

   952 

   953 lemma Sigma_Max_lemma: 

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

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

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

   957   (Cn (Suc (Suc (Suc (length xs)))) rec_disj

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

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

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

   961   Cn (Suc (Suc (Suc (length xs)))) rec_not

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

   963   (get_fstn_args (Suc (Suc (Suc (length xs)))) (length xs) @ 

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

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

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

   967 proof -

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

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

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

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

   972     (Suc (Suc (Suc (length xs)))) ((Suc (length xs)))]"

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

   974                (get_fstn_args (Suc (Suc (Suc (length xs))))

   975     (length xs) @ 

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

   977     ((Suc (Suc (length xs))))])"

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

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

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

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

   982   show "?thesis"

   983   proof(auto simp: Maxr.simps)

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

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

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

   987       using prrf

   988       apply(auto)

   989       apply(case_tac i, auto)

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

   991       done

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

   993       apply(rule_tac Sigma_0)

   994       apply(auto simp: rec_exec.simps all_lemma

   995                        get_fstn_args_take nth_append h)

   996       done

   997     thus "UF.Sigma (rec_exec ?notrq)

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

   999       by simp

  1000   next

  1001     fix x

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

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

  1004       by auto

  1005     from this obtain ma where k1: 

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

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

  1008       using h

  1009       apply(subgoal_tac

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

  1011       apply(erule_tac CollectE, simp)

  1012       apply(rule_tac Max_in, auto)

  1013       done

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

  1015       apply(auto simp: nth_append)

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

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

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

  1019       using prrf

  1020       apply(case_tac i, auto)

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

  1022       done    

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

  1024       apply(auto)

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

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

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

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

  1029         simp add: k1)

  1030       apply(rule_tac Max_ge, auto)

  1031       using prrf

  1032       apply(case_tac i, auto)

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

  1034       done 

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

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

  1037       done

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

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

  1040       by simp

  1041   qed  

  1042 qed

  1043 

  1044 text {*

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

  1046   *}

  1047 lemma Maxr_lemma:

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

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

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

  1051 proof -

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

  1053     by auto

  1054   thus "?thesis"

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

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

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

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

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

  1060              (Suc (Suc (Suc (length xs)))) ((Suc (length xs)))]"

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

  1062                (get_fstn_args (Suc (Suc (Suc (length xs))))

  1063                 (length xs) @ 

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

  1065                            ((Suc (Suc (length xs))))])"

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

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

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

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

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

  1071       by(auto intro: prime_id)

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

  1073       apply(auto)

  1074       apply(case_tac i, auto)

  1075       apply(case_tac ia, auto intro: prime_id)

  1076       apply(simp add: h)

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

  1078       done

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

  1080                                        (Suc (Suc (length xs)))"

  1081       by(erule_tac primerec_all_iff, auto)

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

  1083       by(rule_tac prime_cn, auto)

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

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

  1086       using prnotrp

  1087       using sigma_lemma

  1088       apply(simp only: sigma_lemma)

  1089       apply(rule_tac Sigma_Max_lemma)

  1090       apply(simp add: h)

  1091       done

  1092     thus "rec_exec (rec_sigma ?notrq)

  1093      (xs @ [w, w]) =

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

  1095       apply(simp)

  1096       done

  1097   qed

  1098 qed

  1099       

  1100 text {* 

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

  1102  *}

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

  1104   where

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

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

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

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

  1109  

  1110 declare quo.simps[simp del]

  1111 

  1112 text {*

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

  1114   *}

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

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

  1117       rule_tac Max_eqI, simp, auto)

  1118   fix xa ya

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

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

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

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

  1123 next

  1124   fix xa

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

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

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

  1128     apply(simp)

  1129     done

  1130 qed

  1131 

  1132 lemma [intro]: "quo [x, 0] = 0"

  1133 by(simp add: quo.simps Maxr.simps)

  1134 

  1135 lemma quo_div: "quo [x, y] = x div y"