10 *}

    10 *}

    11 

    11 

    12 section {* Univeral Function *}

    12 section {* Univeral Function *}

    13 

    13 

    14 subsection {* The construction of component functions *}

    14 subsection {* The construction of component functions *}

    19 

    15 

    20 text {*

    16 text {*

    21   The recursive function used to do arithmatic addition.

    17   The recursive function used to do arithmatic addition.

    22 *}

    18 *}

    23 definition rec_add :: "recf"

    19 definition rec_add :: "recf"

  2426     "[Cn 3 rec_disj [Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 0) 

  2422     "[Cn 3 rec_disj [Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 0) 

  2427      [recf.id 3 0]], Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 1) [recf.id 3 0]]], 

  2423      [recf.id 3 0]], Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 1) [recf.id 3 0]]], 

  2428      Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 2) [recf.id 3 0]],

  2424      Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 2) [recf.id 3 0]],

  2429      Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 3) [recf.id 3 0]],

  2425      Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 3) [recf.id 3 0]],

  2430      Cn 3 rec_less [Cn 3 (constn 3) [recf.id 3 0], recf.id 3 2]]"

  2426      Cn 3 rec_less [Cn 3 (constn 3) [recf.id 3 0], recf.id 3 2]]"

  2432   have k1: "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a]

  2427   have k1: "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a]

  2433                          = Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a]"

  2428                          = Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a]"

  2434     apply(rule_tac embranch_lemma )

  2429     apply(rule_tac embranch_lemma )

  2435     apply(auto simp: numeral_3_eq_3 numeral_2_eq_2 rec_newleft0_def 

  2430     apply(auto simp: numeral_3_eq_3 numeral_2_eq_2 rec_newleft0_def 

  2436              rec_newleft1_def rec_newleft2_def rec_newleft3_def)+

  2431              rec_newleft1_def rec_newleft2_def rec_newleft3_def)+

  2641   "stat c = lo c (Pi 1)"

  2636   "stat c = lo c (Pi 1)"

  2642 

  2637 

  2643 fun rght :: "nat \<Rightarrow> nat"

  2638 fun rght :: "nat \<Rightarrow> nat"

  2644   where

  2639   where

  2645   "rght c = lo c (Pi 2)"

  2640   "rght c = lo c (Pi 2)"

  2648 

  2641 

  2649 fun inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"

  2642 fun inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"

  2650   where

  2643   where

  2651   "inpt m xs = trpl 0 1 (strt xs)"

  2644   "inpt m xs = trpl 0 1 (strt xs)"

  2652 

  2645 

  3101         apply(erule_tac prime_pr_reverse, simp)

  3094         apply(erule_tac prime_pr_reverse, simp)

  3102         apply(case_tac "last xs", simp)

  3095         apply(case_tac "last xs", simp)

  3103         apply(rule_tac calc_pr_zero, simp)

  3096         apply(rule_tac calc_pr_zero, simp)

  3104         using ind1[of "rec_exec (Pr n f g) (butlast xs @ [0])"]

  3097         using ind1[of "rec_exec (Pr n f g) (butlast xs @ [0])"]

  3105         apply(simp add: rec_exec.simps, simp, simp, simp)

  3098         apply(simp add: rec_exec.simps, simp, simp, simp)

  3107         apply(rule_tac rk = "rec_exec (Pr n f g)

  3099         apply(rule_tac rk = "rec_exec (Pr n f g)

  3108                (butlast xs@[last xs - Suc 0])" in calc_pr_ind)

  3100                (butlast xs@[last xs - Suc 0])" in calc_pr_ind)

  3109         using ind2[of "rec_exec (Pr n f g)

  3101         using ind2[of "rec_exec (Pr n f g)

  3110                  (butlast xs @ [last xs - Suc 0])"] h

  3102                  (butlast xs @ [last xs - Suc 0])"] h

  3111         apply(simp, simp, simp)

  3103         apply(simp, simp, simp)

  3538               godel_code nl)"

  3530               godel_code nl)"

  3539 

  3531 

  3540 subsection {* Relating interperter functions to the execution of TMs *}

  3532 subsection {* Relating interperter functions to the execution of TMs *}

  3541 

  3533 

  3542 lemma [simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps)

  3534 lemma [simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps)

  3544 

  3535 

  3545 lemma [simp]: "\<lbrakk>fetch tp 0 b = (nact, ns)\<rbrakk> \<Longrightarrow> action_map nact = 4"

  3536 lemma [simp]: "\<lbrakk>fetch tp 0 b = (nact, ns)\<rbrakk> \<Longrightarrow> action_map nact = 4"

  3546 apply(simp add: fetch.simps)

  3537 apply(simp add: fetch.simps)

  3547 done

  3538 done

  3548 

  3539 

  3584   "\<lbrakk>i < length nl; \<not> Suc 0 < godel_code nl\<rbrakk> \<Longrightarrow> nl ! i = 0"

  3575   "\<lbrakk>i < length nl; \<not> Suc 0 < godel_code nl\<rbrakk> \<Longrightarrow> nl ! i = 0"

  3585 using godel_code_great[of nl] godel_code_eq_1[of nl]

  3576 using godel_code_great[of nl] godel_code_eq_1[of nl]

  3586 apply(simp)

  3577 apply(simp)

  3587 done

  3578 done

  3588 

  3579 

  3590 lemma prime_coprime: "\<lbrakk>Prime x; Prime y; x\<noteq>y\<rbrakk> \<Longrightarrow> coprime x y"

  3580 lemma prime_coprime: "\<lbrakk>Prime x; Prime y; x\<noteq>y\<rbrakk> \<Longrightarrow> coprime x y"

  3591 proof(simp only: Prime.simps coprime_nat, auto simp: dvd_def,

  3581 proof(simp only: Prime.simps coprime_nat, auto simp: dvd_def,

  3592       rule_tac classical, simp)

  3582       rule_tac classical, simp)

  3593   fix d k ka

  3583   fix d k ka

  3594   assume case_ka: "\<forall>u<d * ka. \<forall>v<d * ka. u * v \<noteq> d * ka" 

  3584   assume case_ka: "\<forall>u<d * ka. \<forall>v<d * ka. u * v \<noteq> d * ka"