# HG changeset patch # User Christian Urban # Date 1368119796 -3600 # Node ID 745547bdc1c771ffec0e9e98568b280035569b6c # Parent 6e7244ae43b8f0d453af0af6a7ef6fe8369d831b added lemmas about a pairing function diff -r 6e7244ae43b8 -r 745547bdc1c7 thys/Recs.thy --- a/thys/Recs.thy Thu May 02 13:19:50 2013 +0100 +++ b/thys/Recs.thy Thu May 09 18:16:36 2013 +0100 @@ -1,5 +1,7 @@ theory Recs -imports Main Fact "~~/src/HOL/Number_Theory/Primes" +imports Main + "~~/src/HOL/Number_Theory/Primes" + Fact begin (* @@ -104,7 +106,8 @@ fixes f::"nat \ nat" assumes "\i \ n. f i \ 1" shows "(\i \ n. f i) \ 1" -using assms by (induct n) (auto intro: nat_mult_le_one) +using assms +by (induct n) (auto intro: nat_mult_le_one) lemma setprod_greater_zero: fixes f::"nat \ nat" @@ -537,14 +540,14 @@ "rec_eval rec_prime [x] = (if prime x then 1 else 0)" by (auto simp add: rec_prime_def Let_def prime_alt_def) -section {* Bounded Min and Maximisation *} +section {* Bounded Maximisation *} fun BMax_rec where "BMax_rec R 0 = 0" | "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)" definition BMax_set :: "(nat \ bool) \ nat \ nat" - where "BMax_set R x = Max ({z | z. z \ x \ R z} \ {0})" + where "BMax_set R x = Max ({z. z \ x \ R z} \ {0})" definition (in ord) Great :: "('a \ bool) \ 'a" (binder "GREAT " 10) where @@ -555,8 +558,7 @@ assumes "P x" "\y. P y \ y \ x" shows "Great P = x" unfolding Great_def -using assms -by(rule_tac the_equality) (auto intro: le_antisym) +using assms by(rule_tac the_equality) (auto intro: le_antisym) lemma BMax_rec_eq1: "BMax_rec R x = (GREAT z. (R z \ z \ x) \ z = 0)" @@ -566,28 +568,310 @@ by metis lemma BMax_rec_eq2: - "BMax_rec R x = Max ({z | z. z \ x \ R z} \ {0})" + "BMax_rec R x = Max ({z. z \ x \ R z} \ {0})" apply(induct x) apply(auto intro: Max_eqI Max_eqI[symmetric]) apply(simp add: le_Suc_eq) by metis definition - "rec_max1 f = PR (constn 0) - (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 1])" + "rec_max1 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 1])" lemma max1_lemma [simp]: "rec_eval (rec_max1 f) [x, y] = BMax_rec (\u. rec_eval f [u, y] = 0) x" by (induct x) (simp_all add: rec_max1_def) definition - "rec_max2 f = PR (constn 0) - (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])" + "rec_max2 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])" lemma max2_lemma [simp]: "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\u. rec_eval f [u, y1, y2] = 0) x" by (induct x) (simp_all add: rec_max2_def) +section {* Encodings *} + +fun log :: "nat \ nat" where + [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))" + +lemma log_zero [simp]: + "log 0 = 0" + by (simp add: log.simps) + +lemma log_one [simp]: + "log 1 = 0" + by (simp add: log.simps) + +lemma log_suc [simp]: + "log (Suc 0) = 0" + by (simp add: log.simps) + +lemma log_rec: + "n \ 2 \ log n = Suc (log (n div 2))" + by (simp add: log.simps) + +lemma log_twice [simp]: + "n \ 0 \ log (2 * n) = Suc (log n)" + by (simp add: log_rec) + +lemma log_half [simp]: + "log (n div 2) = log n - 1" +proof (cases "n < 2") + case True + then have "n = 0 \ n = 1" by arith + then show ?thesis by (auto simp del: One_nat_def) +next + case False then show ?thesis by (simp add: log_rec) +qed + +lemma log_exp [simp]: + "log (2 ^ n) = n" + by (induct n) simp_all + +fun divby2 :: "nat \ nat" where + [simp del]: "divby2 n = (if n = 0 then 0 + else if even n then divby2 (n div 2) else n)" + +lemma divby2[simp]: + "divby2 0 = 0" + "odd n \ divby2 n = n" + "even n \ divby2 n = divby2 (n div 2)" +apply(simp_all add: divby2.simps) +done + +lemma divby2_odd: + "divby2 n = 0 \ odd (divby2 n)" +apply(induct n rule: nat_less_induct) +apply(case_tac "n = 0") +apply(simp) +apply(case_tac "odd n") +apply(auto) +done + +lemma bigger: "divby2 (Suc n) > 0" +apply(induct n rule: nat_less_induct) +apply(case_tac "n = 0") +apply(simp) +apply(case_tac "odd n") +apply(auto) +apply(drule_tac x="n div 2" in spec) +apply(drule mp) +apply(auto) +by (smt numeral_2_eq_2 odd_nat_plus_one_div_two) + +fun pencode :: "nat \ nat \ nat" where + "pencode m n = (2 ^ m) * ((2 * n) + 1) - 1" + +fun pdecode2 :: "nat \ nat" where + "pdecode2 z = (divby2 (Suc z) - 1) div 2" + +fun pdecode1 :: "nat \ nat" where + "pdecode1 z = log ((Suc z) div (divby2 (Suc z)))" + +lemma k: + "odd n \ divby2 (2 ^ m * n) = n" +apply(induct m) +apply(simp_all) +done + +lemma ww: "\k. n = 2 ^ k * divby2 n" +apply(induct n rule: nat_less_induct) +apply(case_tac "n=0") +apply(simp) +apply(case_tac "odd n") +apply(simp) +apply(rule_tac x="0" in exI) +apply(simp) +apply(simp) +apply(drule_tac x="n div 2" in spec) +apply(erule impE) +apply(simp) +apply(erule exE) +apply(rule_tac x="Suc k" in exI) +apply(simp) +by (metis div_mult_self2_is_id even_mult_two_ex nat_mult_assoc nat_mult_commute zero_neq_numeral) + + + +lemma t: + "(Suc (Suc m)) div 2 = Suc (m div 2)" +by (induct m) (auto) + +lemma u: + "((Suc (Suc m)) mod 2 = 0) <-> m mod 2 = 0" +by (auto) + +lemma u2: + "0 < n ==> 2 * 2 ^ (n - 1) = (2::nat) ^ (n::nat)" +by (induct n) (simp_all) + +lemma test: "x = y \ 2 * x = 2 * y" +by simp + +lemma m: "0 < n ==> 2 ^ log (n div (divby2 n)) = n div (divby2 n)" +apply(induct n rule: nat_less_induct) +apply(case_tac "n=0") +apply(simp) +apply(case_tac "odd n") +apply(simp) +apply(drule_tac x="n div 2" in spec) +apply(drule mp) +apply(auto)[1] +apply(drule mp) +apply (metis One_nat_def Suc_lessI div_2_gt_zero odd_1_nat) +apply(subst (asm) divby2(3)[symmetric]) +apply(simp) +apply(subst (asm) divby2(3)[symmetric]) +apply(simp) +apply(subgoal_tac "n div 2 div divby2 n = n div (divby2 n) div 2") +prefer 2 +apply (metis div_mult2_eq nat_mult_commute) +apply(simp only: log_half) +apply(case_tac "n div divby2 n = 0") +apply(simp) +apply(simp del: divby2) +apply(drule test) +apply(subst (asm) power.simps(2)[symmetric]) +apply(subgoal_tac "Suc (log (n div divby2 n) - 1) = log (n div divby2 n)") +prefer 2 +apply (smt Recs.log.simps Suc_1 div_less div_mult_self1_is_id log_half log_zero numeral_1_eq_Suc_0 numeral_One odd_1_nat odd_nat_plus_one_div_two one_less_numeral_iff power_one_right semiring_norm(76)) +apply(simp only:) +apply(subst dvd_mult_div_cancel) +apply (smt Suc_1 div_by_0 div_mult_self2_is_id divby2_odd dvd_power even_Suc even_numeral_nat even_product_nat nat_even_iff_2_dvd power_0 ww) +apply(simp (no_asm)) +done + +lemma m1: "n div divby2 n * divby2 n = n" +apply(induct n rule: nat_less_induct) +apply(case_tac "n=0") +apply(simp) +apply(case_tac "odd n") +apply(simp) +apply(simp) +apply(drule_tac x="n div 2" in spec) +apply(drule mp) +apply(auto)[1] +by (metis add_eq_if diff_add_inverse divby2(3) mod_eq_0_iff mult_div_cancel nat_mult_commute ww) + + +lemma m2: "0 < n ==> 2 ^ log (n div (divby2 n)) * (divby2 n) = n" +apply(subst m) +apply(simp) +apply(subst m1) +apply(simp) +done + +lemma y1: + "pdecode2 (pencode m n) = n" +apply(simp) +apply(subst k) +apply(auto) +done + +lemma y2: + "pdecode1 (pencode m n) = m" +apply(simp) +apply(subst k) +apply(auto)[1] +apply(simp) +done + +lemma yy: + "pencode (pdecode1 m) (pdecode2 m) = m" +apply(induct m rule: nat_less_induct) +apply(simp (no_asm)) +apply(case_tac "n = 0") +apply(simp) +apply(subst dvd_mult_div_cancel) +using divby2_odd +apply - +apply(drule_tac x="Suc n" in meta_spec) +apply(erule disjE) +apply(auto)[1] +apply (metis even_num_iff nat_even_iff_2_dvd odd_pos) +using bigger +apply - +apply(rotate_tac 3) +apply(drule_tac x="n" in meta_spec) +apply(simp del: pencode.simps pdecode2.simps pdecode1.simps) +apply(subst m2) +apply(simp) +apply(simp) +done + +fun penc where + "penc (m, n) = pencode m n" + +fun pdec where + "pdec m = (pdecode1 m, pdecode2 m)" + +lemma q1: "penc (pdec m) = m" +apply(simp only: penc.simps pdec.simps) +apply(rule yy) +done + +lemma q2: "pdec (penc m) = m" +apply(simp only: penc.simps pdec.simps) +apply(case_tac m) +apply(simp only: penc.simps pdec.simps) +apply(subst y1) +apply(subst y2) +apply(simp) +done + +lemma inj_penc: "inj_on penc A" +apply(rule inj_on_inverseI) +apply(rule q2) +done + +lemma inj_pdec: "inj_on pdec A" +apply(rule inj_on_inverseI) +apply(rule q1) +done + +lemma surj_penc: "surj penc" +apply(rule surjI) +apply(rule q1) +done + +lemma surj_pdec: "surj pdec" +apply(rule surjI) +apply(rule q2) +done + +lemma + "bij pdec" +by(simp add: bij_def surj_pdec inj_pdec) + +lemma + "bij penc" +by(simp add: bij_def surj_penc inj_penc) + +lemma "a \ penc (a, 0)" +apply(induct a) +apply(simp) +apply(simp) +by (smt nat_one_le_power) + +lemma "penc(a, 0) \ penc (a, b)" +apply(simp) +by (metis diff_le_mono le_add1 mult_2_right mult_le_mono1 nat_add_commute nat_mult_1 nat_mult_commute) + +lemma "b \ penc (a, b)" +apply(simp) +proof - + have f1: "(1\nat) + 1 = 2" + by (metis mult_2 nat_mult_1_right) + have f2: "\x\<^isub>1 x\<^isub>2. (x\<^isub>1\nat) \ x\<^isub>1 * x\<^isub>2 \ \ 1 \ x\<^isub>2" + by (metis mult_le_mono2 nat_mult_1_right) + have "1 + (b + b) \ 1 + b \ b \ (1 + (b + b)) * (1 + 1) ^ a - 1" + by (metis le_add1 le_trans nat_add_left_cancel_le) + hence "(1 + (b + b)) * (1 + 1) ^ a \ 1 + b \ b \ (1 + (b + b)) * (1 + 1) ^ a - 1" + using f2 by (metis le_add1 le_trans one_le_power) + hence "b \ 2 ^ a * (b + b + 1) - 1" + using f1 by (metis le_diff_conv nat_add_commute nat_le_linear nat_mult_commute) + thus "b \ 2 ^ a * (2 * b + 1) - 1" + by (metis mult_2) +qed section {* Discrete Logarithms *} @@ -625,7 +909,7 @@ @{text "NextPrime x"} returns the first prime number after @{text "x"}; @{text "Pi i"} returns the i-th prime number. *} -fun NextPrime ::"nat \ nat" +definition NextPrime ::"nat \ nat" where "NextPrime x = (LEAST y. y \ Suc (fact x) \ x < y \ prime y)" @@ -639,14 +923,33 @@ lemma nextprime_lemma [simp]: "rec_eval rec_nextprime [x] = NextPrime x" -by (simp add: rec_nextprime_def Let_def) +by (simp add: rec_nextprime_def Let_def NextPrime_def) +lemma NextPrime_simps [simp]: + shows "NextPrime 2 = 3" + and "NextPrime 3 = 5" +apply(simp_all add: NextPrime_def) +apply(rule Least_equality) +apply(auto) +apply(eval) +apply(rule Least_equality) +apply(auto) +apply(eval) +apply(case_tac "y = 4") +apply(auto) +done fun Pi :: "nat \ nat" where "Pi 0 = 2" | "Pi (Suc x) = NextPrime (Pi x)" +lemma Pi_simps [simp]: + shows "Pi 1 = 3" + and "Pi 2 = 5" +using NextPrime_simps +by(simp_all add: numeral_eq_Suc One_nat_def) + definition "rec_pi = PR (constn 2) (CN rec_nextprime [Id 2 1])" diff -r 6e7244ae43b8 -r 745547bdc1c7 thys/Turing.thy --- a/thys/Turing.thy Thu May 02 13:19:50 2013 +0100 +++ b/thys/Turing.thy Thu May 09 18:16:36 2013 +0100 @@ -111,6 +111,10 @@ shows "is_final (s, tp) = (s = 0)" by (case_tac tp) (auto) +lemma is_finalI [intro]: + shows "is_final (0, tp)" +by (simp add: is_final_eq) + lemma after_is_final: assumes "is_final c" shows "is_final (steps c p n)" @@ -120,6 +124,16 @@ apply(auto) done +lemma is_final: + assumes a: "is_final (steps c p n1)" + and b: "n1 \ n2" + shows "is_final (steps c p n2)" +proof - + obtain n3 where eq: "n2 = n1 + n3" using b by (metis le_iff_add) + from a show "is_final (steps c p n2)" unfolding eq + by (simp add: after_is_final) +qed + lemma not_is_final: assumes a: "\ is_final (steps c p n1)" and b: "n2 \ n1" @@ -164,6 +178,29 @@ qed qed +lemma least_steps: + assumes "steps0 (1, tp) A n = (0, tp')" + shows "\ n'. (\n'' < n'. \ is_final (steps0 (1, tp) A n'')) \ + (\n'' \ n'. is_final (steps0 (1, tp) A n''))" +proof - + from before_final[OF assms] + obtain n' where + before: "\ is_final (steps0 (1, tp) A n')" and + final: "steps0 (1, tp) A (Suc n') = (0, tp')" by auto + from before + have "\n'' < Suc n'. \ is_final (steps0 (1, tp) A n'')" + using not_is_final by auto + moreover + from final + have "\n'' \ Suc n'. is_final (steps0 (1, tp) A n'')" + using is_final[of _ _ "Suc n'"] by (auto simp add: is_final_eq) + ultimately + show "\ n'. (\n'' < n'. \ is_final (steps0 (1, tp) A n'')) \ (\n'' \ n'. is_final (steps0 (1, tp) A n''))" + by blast +qed + + + (* well-formedness of Turing machine programs *) abbreviation "is_even n \ (n::nat) mod 2 = 0" diff -r 6e7244ae43b8 -r 745547bdc1c7 thys/UF.thy --- a/thys/UF.thy Thu May 02 13:19:50 2013 +0100 +++ b/thys/UF.thy Thu May 09 18:16:36 2013 +0100 @@ -3752,10 +3752,10 @@ done lemma [simp]: "left (trpl l st r) = l" -apply(simp add: left.simps trpl.simps lo.simps - loR.simps mod_dvd_simp, auto simp: conf_decode1) -apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r", - auto) +apply(simp add: left.simps trpl.simps lo.simps loR.simps mod_dvd_simp) +apply(auto simp: conf_decode1) +apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r") +apply(auto) apply(erule_tac x = l in allE, auto) done @@ -4613,6 +4613,7 @@ "\steps0 (Suc 0, Bk\l, ) tp stp = (0, Bk\m, Oc\rs@Bk\n); tm_wf (tp,0); 0 \ rec_exec rec_F [code tp, (bl2wc ())] = (rs - Suc 0)" +thm halt_least_step nonstop_t_eq nonstop_lemma rec_t_eq_steps conf_lemma apply(frule_tac halt_least_step, auto) apply(frule_tac nonstop_t_eq, auto simp: nonstop_lemma) using rec_t_eq_steps[of tp l lm stp] diff -r 6e7244ae43b8 -r 745547bdc1c7 thys/UF_Rec.thy --- a/thys/UF_Rec.thy Thu May 02 13:19:50 2013 +0100 +++ b/thys/UF_Rec.thy Thu May 09 18:16:36 2013 +0100 @@ -2,11 +2,11 @@ imports Recs Turing_Hoare begin -section {* Universal Function *} -text{* coding of the configuration *} + +section {* Universal Function in HOL *} text {* @{text "Entry sr i"} returns the @{text "i"}-th entry of a list of natural @@ -15,33 +15,16 @@ fun Entry where "Entry sr i = Lo sr (Pi (Suc i))" -definition - "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]" - -lemma entry_lemma [simp]: - "rec_eval rec_entry [sr, i] = Entry sr i" -by(simp add: rec_entry_def) - - fun Listsum2 :: "nat list \ nat \ nat" where "Listsum2 xs 0 = 0" | "Listsum2 xs (Suc n) = Listsum2 xs n + xs ! n" -fun rec_listsum2 :: "nat \ nat \ recf" - where - "rec_listsum2 vl 0 = CN Z [Id vl 0]" -| "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]" - -lemma listsum2_lemma [simp]: - "length xs = vl \ rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n" -by (induct n) (simp_all) - text {* @{text "Strt"} corresponds to the @{text "strt"} function on page 90 of the - B book, but this definition generalises the original one to deal with multiple - input arguments. - *} + B book, but this definition generalises the original one in order to deal + with multiple input arguments. *} + fun Strt' :: "nat list \ nat \ nat" where "Strt' xs 0 = 0" @@ -52,55 +35,11 @@ where "Strt xs = (let ys = map Suc xs in Strt' ys (length ys))" -fun rec_strt' :: "nat \ nat \ recf" - where - "rec_strt' xs 0 = Z" -| "rec_strt' xs (Suc n) = - (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in - let t1 = CN rec_power [constn 2, dbound] in - let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in - CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])" - -fun rec_map :: "recf \ nat \ recf list" - where - "rec_map rf vl = map (\i. CN rf [Id vl i]) [0.. recf" - where - "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)" - -lemma strt'_lemma [simp]: - "length xs = vl \ rec_eval (rec_strt' vl n) xs = Strt' xs n" -by (induct n) (simp_all add: Let_def) - - -lemma map_suc: - "map (\x. Suc (xs ! x)) [0.. (\x. xs ! x) = (\x. Suc (xs ! x))" by (simp add: comp_def) - then have "map (\x. Suc (xs ! x)) [0.. (\x. xs ! x)) [0..x. xs ! x) [0..x. Suc (xs ! x)) [0.. rec_eval (rec_strt vl) xs = Strt xs" -by (simp add: comp_def map_suc[symmetric]) - - text {* The @{text "Scan"} function on page 90 of B book. *} fun Scan :: "nat \ nat" where "Scan r = r mod 2" -definition - "rec_scan = CN rec_mod [Id 1 0, constn 2]" - -lemma scan_lemma [simp]: - "rec_eval rec_scan [r] = r mod 2" -by(simp add: rec_scan_def) - text {* The @{text Newleft} and @{text Newright} functions on page 91 of B book. *} fun Newleft :: "nat \ nat \ nat \ nat" @@ -118,119 +57,52 @@ else if a = 3 then r div 2 else r)" -definition - "rec_newleft = - (let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], CN rec_eq [Id 3 2, constn 1]] in - let cond2 = CN rec_eq [Id 3 2, constn 2] in - let cond3 = CN rec_eq [Id 3 2, constn 3] in - let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0], - CN rec_mod [Id 3 1, constn 2]] in - CN rec_if [cond1, Id 3 0, - CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2], - CN rec_if [cond3, case3, Id 3 0]]])" - -definition - "rec_newright = - (let condn = \n. CN rec_eq [Id 3 2, constn n] in - let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in - let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in - let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1], - CN rec_mod [Id 3 0, constn 2]] in - let case3 = CN rec_quo [Id 2 1, constn 2] in - CN rec_if [condn 0, case0, - CN rec_if [condn 1, case1, - CN rec_if [condn 2, case2, - CN rec_if [condn 3, case3, Id 3 1]]]])" - -lemma newleft_lemma [simp]: - "rec_eval rec_newleft [p, r, a] = Newleft p r a" -by (simp add: rec_newleft_def Let_def) - -lemma newright_lemma [simp]: - "rec_eval rec_newright [p, r, a] = Newright p r a" -by (simp add: rec_newright_def Let_def) - text {* The @{text "Actn"} function given on page 92 of B book, which is used to fetch Turing Machine intructions. In @{text "Actn m q r"}, @{text "m"} is the Goedel coding of a Turing Machine, @{text "q"} is the current state of - Turing Machine, @{text "r"} is the right number of Turing Machine tape. - *} + Turing Machine, @{text "r"} is the right number of Turing Machine tape. *} + fun Actn :: "nat \ nat \ nat \ nat" where "Actn m q r = (if q \ 0 then Entry m (4 * (q - 1) + 2 * Scan r) else 4)" -definition - "rec_actn = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in - let add2 = CN rec_mult [constn 2, CN rec_scan [Id 3 2]] in - let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]] - in CN rec_if [Id 3 1, entry, constn 4])" - -lemma actn_lemma [simp]: - "rec_eval rec_actn [m, q, r] = Actn m q r" -by (simp add: rec_actn_def) - fun Newstat :: "nat \ nat \ nat \ nat" where "Newstat m q r = (if q \ 0 then Entry m (4 * (q - 1) + 2 * Scan r + 1) else 0)" -definition rec_newstat :: "recf" - where - "rec_newstat = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in - let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in - let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]] - in CN rec_if [Id 3 1, entry, Z])" - -lemma newstat_lemma [simp]: - "rec_eval rec_newstat [m, q, r] = Newstat m q r" -by (simp add: rec_newstat_def) - - fun Trpl :: "nat \ nat \ nat \ nat" where "Trpl p q r = (Pi 0) ^ p * (Pi 1) ^ q * (Pi 2) ^ r" -definition - "rec_trpl = CN rec_mult [CN rec_mult - [CN rec_power [constn (Pi 0), Id 3 0], - CN rec_power [constn (Pi 1), Id 3 1]], - CN rec_power [constn (Pi 2), Id 3 2]]" - -lemma trpl_lemma [simp]: - "rec_eval rec_trpl [p, q, r] = Trpl p q r" -by (simp add: rec_trpl_def) - - - fun Left where "Left c = Lo c (Pi 0)" -definition - "rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]" - -lemma left_lemma [simp]: - "rec_eval rec_left [c] = Left c" -by(simp add: rec_left_def) - fun Right where "Right c = Lo c (Pi 2)" -definition - "rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]" - -lemma right_lemma [simp]: - "rec_eval rec_right [c] = Right c" -by(simp add: rec_right_def) - fun Stat where "Stat c = Lo c (Pi 1)" -definition - "rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]" +lemma mod_dvd_simp: + "(x mod y = (0::nat)) = (y dvd x)" +by(auto simp add: dvd_def) -lemma stat_lemma [simp]: - "rec_eval rec_stat [c] = Stat c" -by(simp add: rec_stat_def) +lemma Trpl_Left [simp]: + "Left (Trpl p q r) = p" +apply(simp) +apply(subst Lo_def) +apply(subst dvd_eq_mod_eq_0[symmetric]) +apply(simp) +apply(auto) +thm Lo_def +thm mod_dvd_simp +apply(simp add: left.simps trpl.simps lo.simps + loR.simps mod_dvd_simp, auto simp: conf_decode1) +apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r", + auto) +apply(erule_tac x = l in allE, auto) + fun Inpt :: "nat \ nat list \ nat" where @@ -242,43 +114,20 @@ (Newstat m (Stat c) (Right c)) (Newright (Left c) (Right c) (Actn m (Stat c) (Right c)))" -definition - "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in - let left = CN rec_left [Id 2 1] in - let right = CN rec_right [Id 2 1] in - let stat = CN rec_stat [Id 2 1] in - let one = CN rec_newleft [left, right, act] in - let two = CN rec_newstat [Id 2 0, stat, right] in - let three = CN rec_newright [left, right, act] - in CN rec_trpl [one, two, three])" - -lemma newconf_lemma [simp]: - "rec_eval rec_newconf [m, c] = Newconf m c" -by (simp add: rec_newconf_def Let_def) - text {* @{text "Conf k m r"} computes the TM configuration after @{text "k"} steps of execution of TM coded as @{text "m"} starting from the initial configuration where the left - number equals @{text "0"}, right number equals @{text "r"}. - *} + number equals @{text "0"}, right number equals @{text "r"}. *} + fun Conf :: "nat \ nat \ nat \ nat" where "Conf 0 m r = Trpl 0 1 r" | "Conf (Suc k) m r = Newconf m (Conf k m r)" -definition - "rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1]) - (CN rec_newconf [Id 4 2 , Id 4 1])" - -lemma conf_lemma [simp]: - "rec_eval rec_conf [k, m, r] = Conf k m r" -by(induct k) (simp_all add: rec_conf_def) - - text {* @{text "Nstd c"} returns true if the configuration coded - by @{text "c"} is not a stardard final configuration. - *} + by @{text "c"} is not a stardard final configuration. *} + fun Nstd :: "nat \ bool" where "Nstd c = (Stat c \ 0 \ @@ -286,70 +135,39 @@ Right c \ 2 ^ (Lg (Suc (Right c)) 2) - 1 \ Right c = 0)" -definition - "rec_nstd = (let disj1 = CN rec_noteq [rec_stat, constn 0] in - let disj2 = CN rec_noteq [rec_left, constn 0] in - let rhs = CN rec_pred [CN rec_power [constn 2, CN rec_lg [CN S [rec_right], constn 2]]] in - let disj3 = CN rec_noteq [rec_right, rhs] in - let disj4 = CN rec_eq [rec_right, constn 0] in - CN rec_disj [CN rec_disj [CN rec_disj [disj1, disj2], disj3], disj4])" - -lemma nstd_lemma [simp]: - "rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)" -by(simp add: rec_nstd_def) - text{* @{text "Nostop t m r"} means that afer @{text "t"} steps of - execution, the TM coded by @{text "m"} is not at a stardard - final configuration. - *} + execution the TM coded by @{text "m"} is not at a stardard + final configuration. *} + fun Nostop :: "nat \ nat \ nat \ bool" where "Nostop t m r = Nstd (Conf t m r)" -definition - "rec_nostop = CN rec_nstd [rec_conf]" - -lemma nostop_lemma [simp]: - "rec_eval rec_nostop [t, m, r] = (if Nostop t m r then 1 else 0)" -by (simp add: rec_nostop_def) - - fun Value where "Value x = (Lg (Suc x) 2) - 1" -definition - "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]" - -lemma value_lemma [simp]: - "rec_eval rec_value [x] = Value x" -by (simp add: rec_value_def) - text{* @{text "rec_halt"} is the recursive function calculating the steps a TM needs to execute before to reach a stardard final configuration. This recursive function is the only one using @{text "Mn"} combinator. So it is the only non-primitive recursive function - needs to be used in the construction of the universal function @{text "rec_uf"}. - *} + needs to be used in the construction of the universal function @{text "rec_uf"}. *} -definition - "rec_halt = MN rec_nostop" +fun Halt :: "nat \ nat \ nat" + where + "Halt m r = (LEAST t. \ Nostop t m r)" + +fun UF :: "nat \ nat \ nat" + where + "UF c m = Value (Right (Conf (Halt c m) c m))" -definition - "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]" +section {* Coding of Turing Machines *} text {* - The correctness of @{text "rec_uf"}, nonhalt case. - *} - -subsection {* Coding function of TMs *} - -text {* - The purpose of this section is to get the coding function of Turing Machine, - which is going to be named @{text "code"}. - *} + The purpose of this section is to construct the coding function of Turing + Machine, which is going to be named @{text "code"}. *} fun bl2nat :: "cell list \ nat \ nat" where @@ -361,9 +179,29 @@ where "bl2wc xs = bl2nat xs 0" -fun trpl_code :: "config \ nat" +lemma bl2nat_double [simp]: + "bl2nat xs (Suc n) = 2 * bl2nat xs n" +apply(induct xs arbitrary: n) +apply(auto) +apply(case_tac a) +apply(auto) +done + +lemma bl2nat_simps1 [simp]: + shows "bl2nat (Bk \ y) n = 0" +by (induct y) (auto) + +lemma bl2nat_simps2 [simp]: + shows "bl2nat (Oc \ y) 0 = 2 ^ y - 1" +apply(induct y) +apply(auto) +apply(case_tac "(2::nat)^ y") +apply(auto) +done + +fun Trpl_code :: "config \ nat" where - "trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)" + "Trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)" fun action_map :: "action \ nat" where @@ -405,13 +243,259 @@ where "Code tp = Goedel_code (modify_tprog tp)" + +section {* Universal Function as Recursive Functions *} + +definition + "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]" + +fun rec_listsum2 :: "nat \ nat \ recf" + where + "rec_listsum2 vl 0 = CN Z [Id vl 0]" +| "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]" + +fun rec_strt' :: "nat \ nat \ recf" + where + "rec_strt' xs 0 = Z" +| "rec_strt' xs (Suc n) = + (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in + let t1 = CN rec_power [constn 2, dbound] in + let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in + CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])" + +fun rec_map :: "recf \ nat \ recf list" + where + "rec_map rf vl = map (\i. CN rf [Id vl i]) [0.. recf" + where + "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)" + +definition + "rec_scan = CN rec_mod [Id 1 0, constn 2]" + +definition + "rec_newleft = + (let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], CN rec_eq [Id 3 2, constn 1]] in + let cond2 = CN rec_eq [Id 3 2, constn 2] in + let cond3 = CN rec_eq [Id 3 2, constn 3] in + let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0], + CN rec_mod [Id 3 1, constn 2]] in + CN rec_if [cond1, Id 3 0, + CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2], + CN rec_if [cond3, case3, Id 3 0]]])" + +definition + "rec_newright = + (let condn = \n. CN rec_eq [Id 3 2, constn n] in + let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in + let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in + let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1], + CN rec_mod [Id 3 0, constn 2]] in + let case3 = CN rec_quo [Id 2 1, constn 2] in + CN rec_if [condn 0, case0, + CN rec_if [condn 1, case1, + CN rec_if [condn 2, case2, + CN rec_if [condn 3, case3, Id 3 1]]]])" + +definition + "rec_actn = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in + let add2 = CN rec_mult [constn 2, CN rec_scan [Id 3 2]] in + let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]] + in CN rec_if [Id 3 1, entry, constn 4])" + +definition rec_newstat :: "recf" + where + "rec_newstat = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in + let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in + let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]] + in CN rec_if [Id 3 1, entry, Z])" + +definition + "rec_trpl = CN rec_mult [CN rec_mult + [CN rec_power [constn (Pi 0), Id 3 0], + CN rec_power [constn (Pi 1), Id 3 1]], + CN rec_power [constn (Pi 2), Id 3 2]]" + +definition + "rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]" + +definition + "rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]" + +definition + "rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]" + +definition + "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in + let left = CN rec_left [Id 2 1] in + let right = CN rec_right [Id 2 1] in + let stat = CN rec_stat [Id 2 1] in + let one = CN rec_newleft [left, right, act] in + let two = CN rec_newstat [Id 2 0, stat, right] in + let three = CN rec_newright [left, right, act] + in CN rec_trpl [one, two, three])" + +definition + "rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1]) + (CN rec_newconf [Id 4 2 , Id 4 1])" + +definition + "rec_nstd = (let disj1 = CN rec_noteq [rec_stat, constn 0] in + let disj2 = CN rec_noteq [rec_left, constn 0] in + let rhs = CN rec_pred [CN rec_power [constn 2, CN rec_lg [CN S [rec_right], constn 2]]] in + let disj3 = CN rec_noteq [rec_right, rhs] in + let disj4 = CN rec_eq [rec_right, constn 0] in + CN rec_disj [CN rec_disj [CN rec_disj [disj1, disj2], disj3], disj4])" + +definition + "rec_nostop = CN rec_nstd [rec_conf]" + +definition + "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]" + +definition + "rec_halt = MN rec_nostop" + +definition + "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]" + + + +section {* Correctness Proofs for Recursive Functions *} + +lemma entry_lemma [simp]: + "rec_eval rec_entry [sr, i] = Entry sr i" +by(simp add: rec_entry_def) + +lemma listsum2_lemma [simp]: + "length xs = vl \ rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n" +by (induct n) (simp_all) + +lemma strt'_lemma [simp]: + "length xs = vl \ rec_eval (rec_strt' vl n) xs = Strt' xs n" +by (induct n) (simp_all add: Let_def) + +lemma map_suc: + "map (\x. Suc (xs ! x)) [0.. (\x. xs ! x) = (\x. Suc (xs ! x))" by (simp add: comp_def) + then have "map (\x. Suc (xs ! x)) [0.. (\x. xs ! x)) [0..x. xs ! x) [0..x. Suc (xs ! x)) [0.. rec_eval (rec_strt vl) xs = Strt xs" +by (simp add: comp_def map_suc[symmetric]) + +lemma scan_lemma [simp]: + "rec_eval rec_scan [r] = r mod 2" +by(simp add: rec_scan_def) + +lemma newleft_lemma [simp]: + "rec_eval rec_newleft [p, r, a] = Newleft p r a" +by (simp add: rec_newleft_def Let_def) + +lemma newright_lemma [simp]: + "rec_eval rec_newright [p, r, a] = Newright p r a" +by (simp add: rec_newright_def Let_def) + +lemma actn_lemma [simp]: + "rec_eval rec_actn [m, q, r] = Actn m q r" +by (simp add: rec_actn_def) + +lemma newstat_lemma [simp]: + "rec_eval rec_newstat [m, q, r] = Newstat m q r" +by (simp add: rec_newstat_def) + +lemma trpl_lemma [simp]: + "rec_eval rec_trpl [p, q, r] = Trpl p q r" +by (simp add: rec_trpl_def) + +lemma left_lemma [simp]: + "rec_eval rec_left [c] = Left c" +by(simp add: rec_left_def) + +lemma right_lemma [simp]: + "rec_eval rec_right [c] = Right c" +by(simp add: rec_right_def) + +lemma stat_lemma [simp]: + "rec_eval rec_stat [c] = Stat c" +by(simp add: rec_stat_def) + +lemma newconf_lemma [simp]: + "rec_eval rec_newconf [m, c] = Newconf m c" +by (simp add: rec_newconf_def Let_def) + +lemma conf_lemma [simp]: + "rec_eval rec_conf [k, m, r] = Conf k m r" +by(induct k) (simp_all add: rec_conf_def) + +lemma nstd_lemma [simp]: + "rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)" +by(simp add: rec_nstd_def) + +lemma nostop_lemma [simp]: + "rec_eval rec_nostop [t, m, r] = (if Nostop t m r then 1 else 0)" +by (simp add: rec_nostop_def) + +lemma value_lemma [simp]: + "rec_eval rec_value [x] = Value x" +by (simp add: rec_value_def) + +lemma halt_lemma [simp]: + "rec_eval rec_halt [m, r] = Halt m r" +by (simp add: rec_halt_def) + +lemma uf_lemma [simp]: + "rec_eval rec_uf [m, r] = UF m r" +by (simp add: rec_uf_def) + + subsection {* Relating interperter functions to the execution of TMs *} +lemma rec_step: + assumes "(\ (s, l, r). s \ length tp div 2) c" + shows "Trpl_code (step0 c tp) = Newconf (Code tp) (Trpl_code c)" +apply(cases c) +apply(simp only: Trpl_code.simps) +apply(simp only: Let_def step.simps) +apply(case_tac "fetch tp (a - 0) (read ca)") +apply(simp only: prod.cases) +apply(case_tac "update aa (b, ca)") +apply(simp only: prod.cases) +apply(simp only: Trpl_code.simps) +apply(simp only: Newconf.simps) +apply(simp only: Left.simps) +oops + +lemma rec_steps: + assumes "tm_wf0 tp" + shows "Trpl_code (steps0 (1, Bk \ l, ) tp stp) = Conf stp (Code tp) (bl2wc ())" +apply(induct stp) +apply(simp) +apply(simp) +oops + lemma F_correct: - assumes tp: "steps0 (1, Bk \ l, ) tp stp = (0, Bk \ m, Oc \ rs @ Bk \ n)" + assumes tm: "steps0 (1, Bk \ l, ) tp stp = (0, Bk \ m, Oc \ rs @ Bk \ n)" and wf: "tm_wf0 tp" "0 < rs" shows "rec_eval rec_uf [Code tp, bl2wc ()] = (rs - Suc 0)" +proof - + from least_steps[OF tm] + obtain stp_least where + before: "\stp' < stp_least. \ is_final (steps0 (1, Bk \ l, ) tp stp')" and + after: "\stp' \ stp_least. is_final (steps0 (1, Bk \ l, ) tp stp')" by blast + have "Halt (Code tp) (bl2wc ()) = stp_least" sorry + show ?thesis + apply(simp only: uf_lemma) + apply(simp only: UF.simps) + apply(simp only: Halt.simps) + oops end