570 (* HERE *)

   577 definition 

   571 

   578   "rec_step = (let left = CN rec_left [Id 2 0] in

   572 definition 

   579                let right = CN rec_right [Id 2 0] in

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

   580                let state = CN rec_state [Id 2 0] in

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

   581                let read = CN rec_read [right] in

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

   582                let action = CN rec_action [Id 2 1, state, read] in

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

   583                let newstate = CN rec_newstate [Id 2 1, state, read] in

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

   584                let newleft = CN rec_newleft [left, right, action] in

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

   585                let newright = CN rec_newright [left, right, action] 

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

   586                in CN rec_conf [newstate, newleft, newright])" 

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

   587 

   581 

   588 lemma step_lemma [simp]:

   582 definition 

   589   "rec_eval rec_step [cf, m] = Step cf m"

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

   590 by (simp add: Let_def rec_step_def)

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

   591 

   585 

   592 definition 

   586 definition 

   593   "rec_steps = PR (Id 3 0)

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

   594                   (CN rec_step [Id 4 1, Id 4 3])"

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

   595 

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

   596 lemma steps_lemma [simp]:

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

   597   "rec_eval rec_steps [n, cf, p] = Steps cf p n"

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

   598 by (induct n) (simp_all add: rec_steps_def Step_Steps_comm del: Step.simps)

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

   599 

   593 

   600 

   594 definition 

   601 definition

   595   "rec_nostop = CN rec_nstd [rec_conf]"

   602   "rec_stknum = CN rec_minus 

   596 

   603                   [CN (rec_sigma1 (CN rec_ldec [Id 2 1, Id 2 0])) [CN rec_enclen [Id 1 0], Id 1 0],

   597 definition 

   604                    CN rec_ldec [Id 1 0, CN rec_enclen [Id 1 0]]]"

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

   605 

   599 

   606 lemma stknum_lemma [simp]:

   600 definition 

   607   "rec_eval rec_stknum [z] = Stknum z"

   601   "rec_halt = MN rec_nostop" 

   608 by (simp add: rec_stknum_def Stknum_def lessThan_Suc_atMost[symmetric])

   602 

   609 

   603 definition 

   610 definition

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

   611   "rec_right_std = (let bound = CN rec_enclen [Id 1 0] in

   605 

   612                     let cond1 = CN rec_le [constn 1, Id 2 0] in

   606 

   613                     let cond2 = rec_all1_less (CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], constn 1]) in

   607 

   614                     let bound2 = CN rec_minus [CN rec_enclen [Id 2 1], Id 2 0] in

   608 section {* Correctness Proofs for Recursive Functions *}

   615                     let cond3 = CN (rec_all2_less 

   609 

   616                                      (CN rec_eq [CN rec_ldec [Id 3 2, CN rec_add [Id 3 1, Id 3 0]], Z])) 

   610 lemma entry_lemma [simp]:

   617                                 [bound2, Id 2 0, Id 2 1] in

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

   618                     CN (rec_ex1 (CN rec_conj [CN rec_conj [cond1, cond2], cond3])) [bound, Id 1 0])"

   612 by(simp add: rec_entry_def)

   619 

   613 

   620 definition

   614 lemma listsum2_lemma [simp]: 

   621   "rec_left_std = (let cond = CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], Z]

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

   622                    in CN (rec_all1_less cond) [CN rec_enclen [Id 1 0], Id 1 0])"

   616 by (induct n) (simp_all)

   623 

   617 

   624 lemma left_std_lemma [simp]:

   618 lemma strt'_lemma [simp]:

   625   "rec_eval rec_left_std [z] = (if left_std z then 1 else 0)"

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

   626 by (simp add: Let_def rec_left_std_def left_std_def)

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

   627 

   621 

   628 lemma right_std_lemma [simp]:

   622 lemma map_suc:

   629   "rec_eval rec_right_std [z] = (if right_std z then 1 else 0)"

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

   630 by (simp add: Let_def rec_right_std_def right_std_def)

   624 proof -

   631 

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

   632 definition

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

   633   "rec_std = CN rec_conj [CN rec_left_std [CN rec_left [Id 1 0]],

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

   634                           CN rec_right_std [CN rec_right [Id 1 0]]]"

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

   635 

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

   636 definition 

   630 qed

   637   "rec_final = CN rec_eq [CN rec_state [Id 1 0], Z]"

   631 

   638 

   632 lemma strt_lemma [simp]: 

   639 definition 

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

   640   "rec_stop = (let steps = CN rec_steps [Id 3 2, Id 3 1, Id 3 0] in

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

   641                CN rec_conj [CN rec_final [steps], CN rec_std [steps]])"

   635 

   642 

   636 lemma scan_lemma [simp]: 

   643 lemma std_lemma [simp]:

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

   644   "rec_eval rec_std [cf] = (if Std cf then 1 else 0)"

   638 by(simp add: rec_scan_def)

   645 by (simp add: rec_std_def)

   639 

   646 

   640 lemma newleft_lemma [simp]:

   647 lemma final_lemma [simp]:

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

   648   "rec_eval rec_final [cf] = (if Final cf then 1 else 0)"

   642 by (simp add: rec_newleft_def Let_def)

   649 by (simp add: rec_final_def)

   643 

   650 

   644 lemma newright_lemma [simp]:

   651 lemma stop_lemma [simp]:

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

   652   "rec_eval rec_stop [m, cf, k] = (if Stop m cf k then 1 else 0)"

   646 by (simp add: rec_newright_def Let_def)

   653 by (simp add: Let_def rec_stop_def)

   647 

   654 

   648 lemma actn_lemma [simp]:

   655 definition

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

   656   "rec_halt = MN (CN rec_not [CN rec_stop [Id 3 1, Id 3 2, Id 3 0]])"

   650 by (simp add: rec_actn_def)

   651 

   652 lemma newstat_lemma [simp]: 

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

   654 by (simp add: rec_newstat_def)

   655 

   656 lemma trpl_lemma [simp]: 

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

   658 apply(simp)

   659 apply (simp add: rec_trpl_def)

   660 

   661 lemma left_lemma [simp]:

   662   "rec_eval rec_left [c] = Left c" 

   663 by(simp add: rec_left_def)

   664 

   665 lemma right_lemma [simp]:

   666   "rec_eval rec_right [c] = Right c" 

   667 by(simp add: rec_right_def)

   668 

   669 lemma stat_lemma [simp]:

   670   "rec_eval rec_stat [c] = Stat c" 

   671 by(simp add: rec_stat_def)

   672 

   673 lemma newconf_lemma [simp]: 

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

   675 by (simp add: rec_newconf_def Let_def)

   676 

   677 lemma conf_lemma [simp]: 

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

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

   680 

   681 lemma nstd_lemma [simp]:

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

   683 by(simp add: rec_nstd_def)

   684 

   685 lemma nostop_lemma [simp]:

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

   687 by (simp add: rec_nostop_def)

   688 

   689 lemma value_lemma [simp]:

   690   "rec_eval rec_value [x] = Value x"

   691 by (simp add: rec_value_def)

   694   "rec_eval rec_halt [m, r] = Halt m r"

   659   "rec_eval rec_halt [m, cf] = Halt m cf"

   695 by (simp add: rec_halt_def)

   660 by (simp add: rec_halt_def del: Stop.simps)

   661 

   662 definition 

   663   "rec_uf = CN rec_pred 

   664               [CN rec_stknum 

   665                   [CN rec_right 

   666                      [CN rec_steps [CN rec_halt [Id 2 0, Id 2 1], Id 2 1, Id 2 0]]]]"

   698   "rec_eval rec_uf [m, r] = UF m r"

   669   "rec_eval rec_uf [m, cf] = UF m cf"