1 theory UF_Rec

     2 imports Recs

     3 begin

     4 

     5 section {* Universal Function *}

     6 

     7 text {* @{text "NextPrime x"} returns the first prime number after @{text "x"}. *}

     8 

     9 fun NextPrime ::"nat \<Rightarrow> nat"

    10   where

    11   "NextPrime x = (LEAST y. y \<le> Suc (fact x) \<and> x < y \<and> prime y)"

    12 

    13 definition rec_nextprime :: "recf"

    14   where

    15   "rec_nextprime = (let conj1 = CN rec_le [Id 2 0, CN S [CN rec_fact [Id 2 1]]] in

    16                     let conj2 = CN rec_less [Id 2 1, Id 2 0] in

    17                     let conj3 = CN rec_prime [Id 2 0] in 

    18                     let conjs = CN rec_conj [CN rec_conj [conj2, conj1], conj3]

    19                     in MN (CN rec_not [conjs]))"

    20 

    21 lemma nextprime_lemma [simp]:

    22   "rec_eval rec_nextprime [x] = NextPrime x"

    23 by (simp add: rec_nextprime_def Let_def)

    24 

    25 

    26 fun Pi :: "nat \<Rightarrow> nat"

    27   where

    28   "Pi 0 = 2" |

    29   "Pi (Suc x) = NextPrime (Pi x)"

    30 

    31 definition 

    32   "rec_pi = PR (constn 2) (CN rec_nextprime [Id 2 1])"

    33 

    34 lemma pi_lemma [simp]:

    35   "rec_eval rec_pi [x] = Pi x"

    36 by (induct x) (simp_all add: rec_pi_def)

    37 

    38 

    39 

    40 text{* coding of the configuration *}

    41 

    42 text {*

    43   @{text "Entry sr i"} returns the @{text "i"}-th entry of a list of natural 

    44   numbers encoded by number @{text "sr"} using Godel's coding.

    45   *}

    46 fun Entry where

    47   "Entry sr i = Lo sr (Pi (Suc i))"

    48 

    49 definition 

    50   "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]"

    51 

    52 lemma entry_lemma [simp]:

    53   "rec_eval rec_entry [sr, i] = Entry sr i"

    54 by(simp add: rec_entry_def)

    55 

    56 

    57 fun Listsum2 :: "nat list \<Rightarrow> nat \<Rightarrow> nat"

    58   where

    59   "Listsum2 xs 0 = 0"

    60 | "Listsum2 xs (Suc n) = Listsum2 xs n + xs ! n"

    61 

    62 fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf"

    63   where

    64   "rec_listsum2 vl 0 = CN Z [Id vl 0]"

    65 | "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]"

    66 

    67 lemma listsum2_lemma [simp]: 

    68   "length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n"

    69 by (induct n) (simp_all)

    70 

    71 text {*

    72   @{text "Strt"} corresponds to the @{text "strt"} function on page 90 of the 

    73   B book, but this definition generalises the original one to deal with multiple 

    74   input arguments.

    75   *}

    76 fun Strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"

    77   where

    78   "Strt' xs 0 = 0"

    79 | "Strt' xs (Suc n) = (let dbound = Listsum2 xs n + n 

    80                        in Strt' xs n + (2 ^ (xs ! n + dbound) - 2 ^ dbound))"

    81 

    82 fun Strt :: "nat list \<Rightarrow> nat"

    83   where

    84   "Strt xs = (let ys = map Suc xs in Strt' ys (length ys))"

    85 

    86 fun rec_strt' :: "nat \<Rightarrow> nat \<Rightarrow> recf"

    87   where

    88   "rec_strt' xs 0 = Z"

    89 | "rec_strt' xs (Suc n) = 

    90       (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in

    91        let t1 = CN rec_power [constn 2, dbound] in

    92        let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in

    93        CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])"

    94 

    95 fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list"

    96   where

    97   "rec_map rf vl = map (\<lambda>i. CN rf [Id vl i]) [0..<vl]"

    98 

    99 fun rec_strt :: "nat \<Rightarrow> recf"

   100   where

   101   "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)"

   102 

   103 lemma strt'_lemma [simp]:

   104   "length xs = vl \<Longrightarrow> rec_eval (rec_strt' vl n) xs = Strt' xs n"

   105 by (induct n) (simp_all add: Let_def)

   106 

   107 

   108 lemma map_suc:

   109   "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs"

   110 proof -

   111   have "Suc \<circ> (\<lambda>x. xs ! x) = (\<lambda>x. Suc (xs ! x))" by (simp add: comp_def)

   112   then have "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map (Suc \<circ> (\<lambda>x. xs ! x)) [0..<length xs]" by simp

   113   also have "... = map Suc (map (\<lambda>x. xs ! x) [0..<length xs])" by simp

   114   also have "... = map Suc xs" by (simp add: map_nth)

   115   finally show "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs" .

   116 qed

   117 

   118 lemma strt_lemma [simp]: 

   119   "length xs = vl \<Longrightarrow> rec_eval (rec_strt vl) xs = Strt xs"

   120 by (simp add: comp_def map_suc[symmetric])

   121 

   122 

   123 text {* The @{text "Scan"} function on page 90 of B book. *}

   124 fun Scan :: "nat \<Rightarrow> nat"

   125   where

   126   "Scan r = r mod 2"

   127 

   128 definition 

   129   "rec_scan = CN rec_rem [Id 1 0, constn 2]"

   130 

   131 lemma scan_lemma [simp]: 

   132   "rec_eval rec_scan [r] = r mod 2"

   133 by(simp add: rec_scan_def)

   134 

   135 text {* The @{text Newleft} and @{text Newright} functions on page 91 of B book. *}

   136 

   137 fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

   138   where

   139   "Newleft p r a = (if a = 0 \<or> a = 1 then p 

   140                     else if a = 2 then p div 2

   141                     else if a = 3 then 2 * p + r mod 2

   142                     else p)"

   143 

   144 fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

   145   where

   146   "Newright p r a  = (if a = 0 then r - Scan r

   147                       else if a = 1 then r + 1 - Scan r

   148                       else if a = 2 then 2 * r + p mod 2

   149                       else if a = 3 then r div 2

   150                       else r)"

   151 

   152 definition

   153     "rec_newleft =

   154        (let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], CN rec_eq [Id 3 2, constn 1]] in

   155         let cond2 = CN rec_eq [Id 3 2, constn 2] in

   156         let cond3 = CN rec_eq [Id 3 2, constn 3] in

   157         let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0], 

   158                                 CN rec_rem [Id 3 1, constn 2]] in

   159         CN rec_if [cond1, Id 3 0, 

   160           CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2],

   161             CN rec_if [cond3, case3, Id 3 0]]])"

   162 

   163 definition

   164     "rec_newright =

   165        (let condn = \<lambda>n. CN rec_eq [Id 3 2, constn n] in

   166         let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in

   167         let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in

   168         let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1],                     

   169                                 CN rec_rem [Id 3 0, constn 2]] in

   170         let case3 = CN rec_quo [Id 2 1, constn 2] in

   171         CN rec_if [condn 0, case0, 

   172           CN rec_if [condn 1, case1,

   173             CN rec_if [condn 2, case2,

   174               CN rec_if [condn 3, case3, Id 3 1]]]])"

   175 

   176 lemma newleft_lemma [simp]:

   177   "rec_eval rec_newleft [p, r, a] = Newleft p r a"

   178 by (simp add: rec_newleft_def Let_def)

   179 

   180 lemma newright_lemma [simp]:

   181   "rec_eval rec_newright [p, r, a] = Newright p r a"

   182 by (simp add: rec_newright_def Let_def)

   183 

   184 text {*

   185   The @{text "Actn"} function given on page 92 of B book, which is used to 

   186   fetch Turing Machine intructions. In @{text "Actn m q r"}, @{text "m"} is 

   187   the Goedel coding of a Turing Machine, @{text "q"} is the current state of 

   188   Turing Machine, @{text "r"} is the right number of Turing Machine tape.

   189   *}

   190 fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

   191   where

   192   "Actn m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r) else 4)"

   193 

   194 definition 

   195   "rec_actn = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in

   196                let add2 = CN rec_mult [constn 2, CN rec_scan [Id 3 2]] in

   197                let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]

   198                in CN rec_if [Id 3 1, entry, constn 4])"

   199 

   200 lemma actn_lemma [simp]:

   201   "rec_eval rec_actn [m, q, r] = Actn m q r"

   202 by (simp add: rec_actn_def)

   203 

   204 fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

   205   where

   206   "Newstat m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r + 1) else 0)"

   207 

   208 definition rec_newstat :: "recf"

   209   where

   210   "rec_newstat = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in

   211                   let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in

   212                   let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]

   213                   in CN rec_if [Id 3 1, entry, Z])"

   214 

   215 lemma newstat_lemma [simp]: 

   216   "rec_eval rec_newstat [m, q, r] = Newstat m q r"

   217 by (simp add: rec_newstat_def)

   218 

   219 

   220 fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

   221   where

   222   "Trpl p q r = (Pi 0) ^ p * (Pi 1) ^ q * (Pi 2) ^ r"

   223 

   224 definition 

   225   "rec_trpl = CN rec_mult [CN rec_mult 

   226        [CN rec_power [constn (Pi 0), Id 3 0], 

   227         CN rec_power [constn (Pi 1), Id 3 1]],

   228         CN rec_power [constn (Pi 2), Id 3 2]]"

   229 

   230 lemma trpl_lemma [simp]: 

   231   "rec_eval rec_trpl [p, q, r] = Trpl p q r"

   232 by (simp add: rec_trpl_def)

   233 

   234 

   235 

   236 fun Left where

   237   "Left c = Lo c (Pi 0)"

   238 

   239 definition

   240   "rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]"

   241 

   242 lemma left_lemma [simp]:

   243   "rec_eval rec_left [c] = Left c" 

   244 by(simp add: rec_left_def)

   245 

   246 fun Right where

   247   "Right c = Lo c (Pi 2)"

   248 

   249 definition 

   250   "rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]"

   251 

   252 lemma right_lemma [simp]:

   253   "rec_eval rec_right [c] = Right c" 

   254 by(simp add: rec_right_def)

   255 

   256 fun Stat where

   257   "Stat c = Lo c (Pi 1)"

   258 

   259 definition 

   260   "rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]"

   261 

   262 lemma stat_lemma [simp]:

   263   "rec_eval rec_stat [c] = Stat c" 

   264 by(simp add: rec_stat_def)

   265 

   266 fun Inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"

   267   where

   268   "Inpt m xs = Trpl 0 1 (Strt xs)"

   269 

   270 fun Newconf :: "nat \<Rightarrow> nat \<Rightarrow> nat"

   271   where

   272   "Newconf m c = Trpl (Newleft (Left c) (Right c) (Actn m (Stat c) (Right c)))

   273                       (Newstat m (Stat c) (Right c)) 

   274                       (Newright (Left c) (Right c) (Actn m (Stat c) (Right c)))"

   275 

   276 definition 

   277   "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in

   278                   let left = CN rec_left [Id 2 1] in

   279                   let right = CN rec_right [Id 2 1] in

   280                   let stat = CN rec_stat [Id 2 1] in

   281                   let one = CN rec_newleft [left, right, act] in

   282                   let two = CN rec_newstat [Id 2 0, stat, right] in

   283                   let three = CN rec_newright [left, right, act]

   284                   in CN rec_trpl [one, two, three])" 

   285 

   286 lemma newconf_lemma [simp]: 

   287   "rec_eval rec_newconf [m, c] = Newconf m c"

   288 by (simp add: rec_newconf_def Let_def)

   289 

   290 text {*

   291   @{text "Conf k m r"} computes the TM configuration after @{text "k"} steps of execution

   292   of TM coded as @{text "m"} starting from the initial configuration where the left 

   293   number equals @{text "0"}, right number equals @{text "r"}. 

   294   *}

   295 fun Conf :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

   296   where

   297   "Conf 0 m r  = Trpl 0 1 r"

   298 | "Conf (Suc k) m r = Newconf m (Conf k m r)"

   299 

   300 definition 

   301   "rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1])

   302                  (CN rec_newconf [Id 4 2 , Id 4 1])"

   303 

   304 lemma conf_lemma [simp]: 

   305   "rec_eval rec_conf [k, m, r] = Conf k m r"

   306 by(induct k) (simp_all add: rec_conf_def)

   307 

   308 

   309 text {*

   310   @{text "Nstd c"} returns true if the configuration coded 

   311   by @{text "c"} is not a stardard final configuration.

   312   *}

   313 fun Nstd :: "nat \<Rightarrow> bool"

   314   where

   315   "Nstd c = (Stat c \<noteq> 0 \<or> 

   316              Left c \<noteq> 0 \<or> 

   317              Right c \<noteq> 2 ^ (Lg (Suc (Right c)) 2) - 1 \<or> 

   318              Right c = 0)"

   319 

   320 definition 

   321   "rec_nstd = (let disj1 = CN rec_noteq [rec_stat, constn 0] in

   322                let disj2 = CN rec_noteq [rec_left, constn 0] in

   323                let rhs = CN rec_pred [CN rec_power [constn 2, CN rec_lg [CN S [rec_right], constn 2]]] in

   324                let disj3 = CN rec_noteq [rec_right, rhs] in

   325                let disj4 = CN rec_eq [rec_right, constn 0] in

   326                CN rec_disj [CN rec_disj [CN rec_disj [disj1, disj2], disj3], disj4])"

   327 

   328 lemma nstd_lemma [simp]:

   329   "rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)"

   330 by(simp add: rec_nstd_def)

   331 

   332 

   333 text{* 

   334   @{text "Nostop t m r"} means that afer @{text "t"} steps of 

   335   execution, the TM coded by @{text "m"} is not at a stardard 

   336   final configuration.

   337   *}

   338 fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"

   339   where

   340   "Nostop t m r = Nstd (Conf t m r)"

   341 

   342 definition 

   343   "rec_nostop = CN rec_nstd [rec_conf]"

   344 

   345 lemma nostop_lemma [simp]:

   346   "rec_eval rec_nostop [t, m, r] = (if Nostop t m r then 1 else 0)" 

   347 by (simp add: rec_nostop_def)

   348 

   349 

   350 fun Value where

   351   "Value x = (Lg (Suc x) 2) - 1"

   352 

   353 definition 

   354   "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"

   355 

   356 lemma value_lemma [simp]:

   357   "rec_eval rec_value [x] = Value x"

   358 by (simp add: rec_value_def)

   359 

   360 text{*

   361   @{text "rec_halt"} is the recursive function calculating the steps a TM needs to execute before

   362   to reach a stardard final configuration. This recursive function is the only one

   363   using @{text "Mn"} combinator. So it is the only non-primitive recursive function 

   364   needs to be used in the construction of the universal function @{text "rec_uf"}.

   365   *}

   366 

   367 definition 

   368   "rec_halt = MN rec_nostop" 

   369 

   370 

   371 definition 

   372   "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]"

   373 

   374 end

   375 

   376 

   377 (*

   378 

   379 

   380 

   381 fun mtest where

   382   "mtest R 0 = if R 0 then 0 else 1"

   383 | "mtest R (Suc n) = (if R n then mtest R n else (Suc n))"

   384 

   385 

   386 lemma 

   387   "rec_eval (rec_maxr2 f) [x, y1, y2] = XXX"

   388 apply(simp only: rec_maxr2_def)

   389 apply(case_tac x)

   390 apply(clarify)

   391 apply(subst rec_eval.simps)

   392 apply(simp only: constn_lemma)

   393 defer

   394 apply(clarify)

   395 apply(subst rec_eval.simps)

   396 apply(simp only: rec_maxr2_def[symmetric])

   397 apply(subst rec_eval.simps)

   398 apply(simp only: map.simps nth)

   399 apply(subst rec_eval.simps)

   400 apply(simp only: map.simps nth)

   401 apply(subst rec_eval.simps)

   402 apply(simp only: map.simps nth)

   403 apply(subst rec_eval.simps)

   404 apply(simp only: map.simps nth)

   405 apply(subst rec_eval.simps)

   406 apply(simp only: map.simps nth)

   407 apply(subst rec_eval.simps)

   408 apply(simp only: map.simps nth)

   409 

   410 

   411 definition

   412   "rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))"

   413 

   414 definition

   415   "rec_maxr2 f = rec_sigma2 (CN rec_sign [CN (rec_sigma2 f) [S]])"

   416 

   417 definition Minr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"

   418   where "Minr R x ys = Min ({z | z. z \<le> x \<and> R z ys} \<union> {Suc x})"

   419 

   420 definition Maxr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"

   421   where "Maxr R x ys = Max ({z | z. z \<le> x \<and> R z ys} \<union> {0})"

   422 

   423 lemma rec_minr2_le_Suc:

   424   "rec_eval (rec_minr2 f) [x, y1, y2] \<le> Suc x"

   425 apply(simp add: rec_minr2_def)

   426 apply(auto intro!: setsum_one_le setprod_one_le)

   427 done

   428 

   429 lemma rec_minr2_eq_Suc:

   430   assumes "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0"

   431   shows "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x"

   432 using assms by (simp add: rec_minr2_def)

   433 

   434 lemma rec_minr2_le:

   435   assumes h1: "y \<le> x" 

   436   and     h2: "0 < rec_eval f [y, y1, y2]" 

   437   shows "rec_eval (rec_minr2 f) [x, y1, y2] \<le> y"

   438 apply(simp add: rec_minr2_def)

   439 apply(subst setsum_cut_off_le[OF h1])

   440 using h2 apply(auto)

   441 apply(auto intro!: setsum_one_less setprod_one_le)

   442 done

   443 

   444 (* ??? *)

   445 lemma setsum_eq_one_le2:

   446   fixes n::nat

   447   assumes "\<forall>i \<le> n. f i \<le> 1" 

   448   shows "((\<Sum>i \<le> n. f i) \<ge> Suc n) \<Longrightarrow> (\<forall>i \<le> n. f i = 1)"  

   449 using assms

   450 apply(induct n)

   451 apply(simp add: One_nat_def)

   452 apply(simp)

   453 apply(auto simp add: One_nat_def)

   454 apply(drule_tac x="Suc n" in spec)

   455 apply(auto)

   456 by (metis le_Suc_eq)

   457 

   458 

   459 lemma rec_min2_not:

   460   assumes "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x"

   461   shows "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0"

   462 using assms

   463 apply(simp add: rec_minr2_def)

   464 apply(subgoal_tac "\<forall>i \<le> x. (\<Prod>z\<le>i. if rec_eval f [z, y1, y2] = 0 then 1 else 0) = (1::nat)")

   465 apply(simp)

   466 apply (metis atMost_iff le_refl zero_neq_one)

   467 apply(rule setsum_eq_one_le2)

   468 apply(auto)

   469 apply(rule setprod_one_le)

   470 apply(auto)

   471 done

   472 

   473 lemma disjCI2:

   474   assumes "~P ==> Q" shows "P|Q"

   475 apply (rule classical)

   476 apply (iprover intro: assms disjI1 disjI2 notI elim: notE)

   477 done

   478 

   479 lemma minr_lemma [simp]:

   480 shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z.  (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)"

   481 apply(induct x)

   482 apply(rule Least_equality[symmetric])

   483 apply(simp add: rec_minr2_def)

   484 apply(erule disjE)

   485 apply(rule rec_minr2_le)

   486 apply(auto)[2]

   487 apply(simp)

   488 apply(rule rec_minr2_le_Suc)

   489 apply(simp)

   490 

   491 apply(rule rec_minr2_le)

   492 

   493 

   494 apply(rule rec_minr2_le_Suc)

   495 apply(rule disjCI)

   496 apply(simp add: rec_minr2_def)

   497 

   498 apply(ru le setsum_one_less)

   499 apply(clarify)

   500 apply(rule setprod_one_le)

   501 apply(auto)[1]

   502 apply(simp)

   503 apply(rule setsum_one_le)

   504 apply(clarify)

   505 apply(rule setprod_one_le)

   506 apply(auto)[1]

   507 thm disj_CE

   508 apply(auto)

   509 

   510 lemma minr_lemma:

   511 shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]"

   512 apply(simp only: Minr_def)

   513 apply(rule sym)

   514 apply(rule Min_eqI)

   515 apply(auto)[1]

   516 apply(simp)

   517 apply(erule disjE)

   518 apply(simp)

   519 apply(rule rec_minr2_le_Suc)

   520 apply(rule rec_minr2_le)

   521 apply(auto)[2]

   522 apply(simp)

   523 apply(induct x)

   524 apply(simp add: rec_minr2_def)

   525 apply(

   526 apply(rule disjCI)

   527 apply(rule rec_minr2_eq_Suc)

   528 apply(simp)

   529 apply(auto)

   530 

   531 apply(rule setsum_one_le)

   532 apply(auto)[1]

   533 apply(rule setprod_one_le)

   534 apply(auto)[1]

   535 apply(subst setsum_cut_off_le)

   536 apply(auto)[2]

   537 apply(rule setsum_one_less)

   538 apply(auto)[1]

   539 apply(rule setprod_one_le)

   540 apply(auto)[1]

   541 apply(simp)

   542 thm setsum_eq_one_le

   543 apply(subgoal_tac "(\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \<or>

   544                    (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))")

   545 prefer 2

   546 apply(auto)[1]

   547 apply(erule disjE)

   548 apply(rule disjI1)

   549 apply(rule setsum_eq_one_le)

   550 apply(simp)

   551 apply(rule disjI2)

   552 apply(simp)

   553 apply(clarify)

   554 apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])")

   555 defer

   556 apply metis

   557 apply(erule exE)

   558 apply(subgoal_tac "l \<le> x")

   559 defer

   560 apply (metis not_leE not_less_Least order_trans)

   561 apply(subst setsum_least_eq)

   562 apply(rotate_tac 4)

   563 apply(assumption)

   564 apply(auto)[1]

   565 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")

   566 prefer 2

   567 apply(auto)[1]

   568 apply(rotate_tac 5)

   569 apply(drule not_less_Least)

   570 apply(auto)[1]

   571 apply(auto)

   572 apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI)

   573 apply(simp)

   574 apply (metis LeastI_ex)

   575 apply(subst setsum_least_eq)

   576 apply(rotate_tac 3)

   577 apply(assumption)

   578 apply(simp)

   579 apply(auto)[1]

   580 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")

   581 prefer 2

   582 apply(auto)[1]

   583 apply (metis neq0_conv not_less_Least)

   584 apply(auto)[1]

   585 apply (metis (mono_tags) LeastI_ex)

   586 by (metis LeastI_ex)

   587 

   588 lemma minr_lemma:

   589 shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]"

   590 apply(simp only: Minr_def rec_minr2_def)

   591 apply(simp)

   592 apply(rule sym)

   593 apply(rule Min_eqI)

   594 apply(auto)[1]

   595 apply(simp)

   596 apply(erule disjE)

   597 apply(simp)

   598 apply(rule setsum_one_le)

   599 apply(auto)[1]

   600 apply(rule setprod_one_le)

   601 apply(auto)[1]

   602 apply(subst setsum_cut_off_le)

   603 apply(auto)[2]

   604 apply(rule setsum_one_less)

   605 apply(auto)[1]

   606 apply(rule setprod_one_le)

   607 apply(auto)[1]

   608 apply(simp)

   609 thm setsum_eq_one_le

   610 apply(subgoal_tac "(\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \<or>

   611                    (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))")

   612 prefer 2

   613 apply(auto)[1]

   614 apply(erule disjE)

   615 apply(rule disjI1)

   616 apply(rule setsum_eq_one_le)

   617 apply(simp)

   618 apply(rule disjI2)

   619 apply(simp)

   620 apply(clarify)

   621 apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])")

   622 defer

   623 apply metis

   624 apply(erule exE)

   625 apply(subgoal_tac "l \<le> x")

   626 defer

   627 apply (metis not_leE not_less_Least order_trans)

   628 apply(subst setsum_least_eq)

   629 apply(rotate_tac 4)

   630 apply(assumption)

   631 apply(auto)[1]

   632 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")

   633 prefer 2

   634 apply(auto)[1]

   635 apply(rotate_tac 5)

   636 apply(drule not_less_Least)

   637 apply(auto)[1]

   638 apply(auto)

   639 apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI)

   640 apply(simp)

   641 apply (metis LeastI_ex)

   642 apply(subst setsum_least_eq)

   643 apply(rotate_tac 3)

   644 apply(assumption)

   645 apply(simp)

   646 apply(auto)[1]

   647 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")

   648 prefer 2

   649 apply(auto)[1]

   650 apply (metis neq0_conv not_less_Least)

   651 apply(auto)[1]

   652 apply (metis (mono_tags) LeastI_ex)

   653 by (metis LeastI_ex)

   654 

   655 lemma disjCI2:

   656   assumes "~P ==> Q" shows "P|Q"

   657 apply (rule classical)

   658 apply (iprover intro: assms disjI1 disjI2 notI elim: notE)

   659 done

   660 

   661 

   662 lemma minr_lemma [simp]:

   663 shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z.  (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)"

   664 (*apply(simp add: rec_minr2_def)*)

   665 apply(rule Least_equality[symmetric])

   666 prefer 2

   667 apply(erule disjE)

   668 apply(rule rec_minr2_le)

   669 apply(auto)[2]

   670 apply(clarify)

   671 apply(rule rec_minr2_le_Suc)

   672 apply(rule disjCI)

   673 apply(simp add: rec_minr2_def)

   674 

   675 apply(ru le setsum_one_less)

   676 apply(clarify)

   677 apply(rule setprod_one_le)

   678 apply(auto)[1]

   679 apply(simp)

   680 apply(rule setsum_one_le)

   681 apply(clarify)

   682 apply(rule setprod_one_le)

   683 apply(auto)[1]

   684 thm disj_CE

   685 apply(auto)

   686 apply(auto)

   687 prefer 2

   688 apply(rule le_tran

   689 

   690 apply(rule le_trans)

   691 apply(simp)

   692 defer

   693 apply(auto)

   694 apply(subst setsum_cut_off_le)

   695 

   696 

   697 lemma 

   698   "Minr R x ys = (LEAST z. (R z ys \<or> z = Suc x))" 

   699 apply(simp add: Minr_def)

   700 apply(rule Min_eqI)

   701 apply(auto)[1]

   702 apply(simp)

   703 apply(rule Least_le)

   704 apply(auto)[1]

   705 apply(rule LeastI2_wellorder)

   706 apply(auto)

   707 done

   708 

   709 definition (in ord)

   710   Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where

   711   "Great P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x))"

   712 

   713 (*

   714 lemma Great_equality:

   715   assumes "P x"

   716     and "\<And>y. P y \<Longrightarrow> y \<le> x"

   717   shows "Great P = x"

   718 unfolding Great_def 

   719 apply(rule the_equality)

   720 apply(blast intro: assms)

   721 *)

   722 

   723 

   724 

   725 lemma 

   726   "Maxr R x ys = (GREAT z. (R z ys \<or> z = 0))" 

   727 apply(simp add: Maxr_def)

   728 apply(rule Max_eqI)

   729 apply(auto)[1]

   730 apply(simp)

   731 thm Least_le Greatest_le

   732 oops

   733 

   734 lemma

   735   "Maxr R x ys = x - Minr (\<lambda>z. R (x - z)) x ys"

   736 apply(simp add: Maxr_def Minr_def)

   737 apply(rule Max_eqI)

   738 apply(auto)[1]

   739 apply(simp)

   740 apply(erule disjE)

   741 apply(simp)

   742 apply(auto)[1]

   743 defer

   744 apply(simp)

   745 apply(auto)[1]

   746 thm Min_insert

   747 defer

   748 oops

   749 

   750 

   751 

   752 definition quo :: "nat \<Rightarrow> nat \<Rightarrow> nat"

   753   where

   754   "quo x y = (if y = 0 then 0 else x div y)"

   755 

   756 

   757 definition 

   758   "rec_quo = CN rec_mult [CN rec_sign [Id 2 1],  

   759       CN (rec_minr2 (CN rec_less [Id 3 1, CN rec_mult [CN S [Id 3 0], Id 3 2]])) 

   760                 [Id 2 0, Id 2 0, Id 2 1]]"

   761 

   762 lemma div_lemma [simp]:

   763   "rec_eval rec_quo [x, y] = quo x y"

   764 apply(simp add: rec_quo_def quo_def)

   765 apply(rule impI)

   766 apply(rule Min_eqI)

   767 apply(auto)[1]

   768 apply(simp)

   769 apply(erule disjE)

   770 apply(simp)

   771 apply(auto)[1]

   772 apply (metis div_le_dividend le_SucI)

   773 defer

   774 apply(simp)

   775 apply(auto)[1]

   776 apply (metis mult_Suc_right nat_mult_commute split_div_lemma)

   777 apply(auto)[1]

   778 

   779 apply (smt div_le_dividend fst_divmod_nat)

   780 apply(simp add: quo_def)

   781 apply(auto)[1]

   782 

   783 apply(auto)

   784 

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

   786   where "Minr R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in 

   787                         if (setx = {}) then (Suc x) else (Min setx))"

   788 

   789 definition

   790   "rec_minr f = rec_sigma1 (rec_accum1 (CN rec_not [f]))"

   791 

   792 lemma minr_lemma [simp]:

   793 shows "rec_eval (rec_minr f) [x, y] = Minr (\<lambda>xs. (0 < rec_eval f xs)) x y"

   794 apply(simp only: rec_minr_def)

   795 apply(simp only: sigma1_lemma)

   796 apply(simp only: accum1_lemma)

   797 apply(subst rec_eval.simps)

   798 apply(simp only: map.simps nth)

   799 apply(simp only: Minr.simps Let_def)

   800 apply(auto simp del: not_lemma)

   801 apply(simp)

   802 apply(simp only: not_lemma sign_lemma)

   803 apply(rule sym)

   804 apply(rule Min_eqI)

   805 apply(auto)[1]

   806 apply(simp)

   807 apply(subst setsum_cut_off_le[where m="ya"])

   808 apply(simp)

   809 apply(simp)

   810 apply(metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq)

   811 apply(rule setsum_one_less)

   812 apply(default)

   813 apply(rule impI)

   814 apply(rule setprod_one_le)

   815 apply(auto split: if_splits)[1]

   816 apply(simp)

   817 apply(rule conjI)

   818 apply(subst setsum_cut_off_le[where m="xa"])

   819 apply(simp)

   820 apply(simp)

   821 apply (metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq)

   822 apply(rule le_trans)

   823 apply(rule setsum_one_less)

   824 apply(default)

   825 apply(rule impI)

   826 apply(rule setprod_one_le)

   827 apply(auto split: if_splits)[1]

   828 apply(simp)

   829 apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y])")

   830 defer

   831 apply metis

   832 apply(erule exE)

   833 apply(subgoal_tac "l \<le> x")

   834 defer

   835 apply (metis not_leE not_less_Least order_trans)

   836 apply(subst setsum_least_eq)

   837 apply(rotate_tac 3)

   838 apply(assumption)

   839 prefer 3

   840 apply (metis LeastI_ex)

   841 apply(auto)[1]

   842 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y])")

   843 prefer 2

   844 apply(auto)[1]

   845 apply(rotate_tac 5)

   846 apply(drule not_less_Least)

   847 apply(auto)[1]

   848 apply(auto)

   849 by (metis (mono_tags) LeastI_ex)

   850 

   851 

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

   853   where "Minr2 R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in 

   854                         Min (setx \<union> {Suc x}))"

   855 

   856 lemma Minr2_Minr: 

   857   "Minr2 R x y = Minr R x y"

   858 apply(auto)

   859 apply (metis (lifting, no_types) Min_singleton empty_Collect_eq)

   860 apply(rule min_absorb2)

   861 apply(subst Min_le_iff)

   862 apply(auto)  

   863 done

   864  *)