diff --git a/metadata/entries/Universal_Turing_Machine.toml b/metadata/entries/Universal_Turing_Machine.toml --- a/metadata/entries/Universal_Turing_Machine.toml +++ b/metadata/entries/Universal_Turing_Machine.toml @@ -1,66 +1,67 @@ title = "Universal Turing Machine" date = 2019-02-08 topics = [ "Logic/Computability", "Computer science/Automata and formal languages", ] abstract = """ -This entry formalises results from computability theory: recursive functions, -undecidability of the halting problem, and the existence of a -universal Turing machine. This formalisation is the AFP entry +

This entry formalises results from computability theory, +for example recursive functions, +undecidability of the halting problem, the existence of a +universal Turing machine and so on. This formalisation is the AFP entry corresponding to the paper Mechanising Turing Machines and Computability Theory -in Isabelle/HOL, ITP 2013. The main book used for this formalisation is -by Boolos, Burgess, and Jeffrey on Computability and Logic. +in Isabelle/HOL from ITP 2013. The main book used for this formalisation is +by Boolos, Burgess, and Jeffrey on Computability and Logic.

-Joosten contributed mainly by making the files ready for the -AFP. His need for a formalisation of Turing Machines arose from +

Joosten contributed by making the files ready for the +AFP in 2019. His need for a formalisation of Turing Machines arose from realising that the current formalisation of saturation graphs (also in the AFP) was missing a key undecidability result -present in his paper on Finding models through graph saturation. +present in his paper on Finding models through graph saturation.

-Regensburger contributed by adding definitions for +

Regensburger contributed in 2022 by adding definitions for concepts like Turing Decidability, Turing Computability and Turing Reducibility for problem reduction. He also enhanced the result about the undecidability of the General Halting Problem given in the original AFP entry by first proving the undecidability of the Special Halting Problem and then proving its reducibility to the general problem. The original version of this AFP entry did only prove a weak form of the undecidability theorem. The main motivation behind this contribution is to make the AFP entry -accessible for bachelor and master students. +accessible for bachelor and master students.

""" license = "bsd" note = "" [authors] [authors.xu] [authors.zhangx] [authors.urban] homepage = "urban_homepage" [authors.joosten] homepage = "joosten_homepage" [authors.regensburger] homepage = "regensburger_homepage" [contributors] [notify] joosten = "joosten_email1" urban = "urban_email" regensburger = "regensburger_email" [history] 2019-01-16 = """ Sebastiaan Joosten made the code ready for the AFP.
""" 2022-09-07 = """ Franz Regensburger added substantial material and made some modifications.
""" [extra] [related] diff --git a/thys/Universal_Turing_Machine/Recursive.thy b/thys/Universal_Turing_Machine/Recursive.thy --- a/thys/Universal_Turing_Machine/Recursive.thy +++ b/thys/Universal_Turing_Machine/Recursive.thy @@ -1,2869 +1,2869 @@ (* Title: thys/Recursive.thy Author: Jian Xu, Xingyuan Zhang, and Christian Urban Modifications: Sebastiaan Joosten Modifications: Franz Regensburger (FABR) 08/2022 Added LaTeX sections and comments *) section \Compilation of Recursive Functions into Abacus Programs\ theory Recursive imports Abacus Rec_Def Abacus_Hoare begin fun addition :: "nat \ nat \ nat \ abc_prog" where "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]" fun mv_box :: "nat \ nat \ abc_prog" where "mv_box m n = [Dec m 3, Inc n, Goto 0]" text \The compilation of \z\-operator.\ definition rec_ci_z :: "abc_inst list" where "rec_ci_z \ [Goto 1]" text \The compilation of \s\-operator.\ definition rec_ci_s :: "abc_inst list" where "rec_ci_s \ (addition 0 1 2 [+] [Inc 1])" text \The compilation of \id i j\-operator\ fun rec_ci_id :: "nat \ nat \ abc_inst list" where "rec_ci_id i j = addition j i (i + 1)" fun mv_boxes :: "nat \ nat \ nat \ abc_inst list" where "mv_boxes ab bb 0 = []" | "mv_boxes ab bb (Suc n) = mv_boxes ab bb n [+] mv_box (ab + n) (bb + n)" fun empty_boxes :: "nat \ abc_inst list" where "empty_boxes 0 = []" | "empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]" fun cn_merge_gs :: "(abc_inst list \ nat \ nat) list \ nat \ abc_inst list" where "cn_merge_gs [] p = []" | "cn_merge_gs (g # gs) p = (let (gprog, gpara, gn) = g in gprog [+] mv_box gpara p [+] cn_merge_gs gs (Suc p))" subsection \Definition of the compiler rec\_ci\ text \ The compiler of recursive functions, where \rec_ci recf\ return \(ap, arity, fp)\, where \ap\ is the Abacus program, \arity\ is the arity of the recursive function \recf\, \fp\ is the amount of memory which is going to be used by \ap\ for its execution. \ fun rec_ci :: "recf \ abc_inst list \ nat \ nat" where "rec_ci z = (rec_ci_z, 1, 2)" | "rec_ci s = (rec_ci_s, 1, 3)" | "rec_ci (id m n) = (rec_ci_id m n, m, m + 2)" | "rec_ci (Cn n f gs) = (let cied_gs = map (\ g. rec_ci g) gs in let (fprog, fpara, fn) = rec_ci f in let pstr = Max (set (Suc n # fn # (map (\ (aprog, p, n). n) cied_gs))) in let qstr = pstr + Suc (length gs) in (cn_merge_gs cied_gs pstr [+] mv_boxes 0 qstr n [+] mv_boxes pstr 0 (length gs) [+] fprog [+] mv_box fpara pstr [+] empty_boxes (length gs) [+] mv_box pstr n [+] mv_boxes qstr 0 n, n, qstr + n))" | "rec_ci (Pr n f g) = (let (fprog, fpara, fn) = rec_ci f in let (gprog, gpara, gn) = rec_ci g in let p = Max (set ([n + 3, fn, gn])) in let e = length gprog + 7 in (mv_box n p [+] fprog [+] mv_box n (Suc n) [+] (([Dec p e] [+] gprog [+] [Inc n, Dec (Suc n) 3, Goto 1]) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gprog + 4)]), Suc n, p + 1))" | "rec_ci (Mn n f) = (let (fprog, fpara, fn) = rec_ci f in let len = length (fprog) in (fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3), Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn))" subsection \Correctness of the compiler rec\_ci\ declare rec_ci.simps [simp del] rec_ci_s_def[simp del] rec_ci_z_def[simp del] rec_ci_id.simps[simp del] mv_boxes.simps[simp del] mv_box.simps[simp del] addition.simps[simp del] declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del] abc_step_l.simps[simp del] inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs" inductive_cases terminate_z_reverse[elim!]: "terminate z xs" inductive_cases terminate_s_reverse[elim!]: "terminate s xs" inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs" inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs" inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs" fun addition_inv :: "nat \ nat list \ nat \ nat \ nat \ nat list \ bool" where "addition_inv (as, lm') m n p lm = (let sn = lm ! n in let sm = lm ! m in lm ! p = 0 \ (if as = 0 then \ x. x \ lm ! m \ lm' = lm[m := x, n := (sn + sm - x), p := (sm - x)] else if as = 1 then \ x. x < lm ! m \ lm' = lm[m := x, n := (sn + sm - x - 1), p := (sm - x - 1)] else if as = 2 then \ x. x < lm ! m \ lm' = lm[m := x, n := (sn + sm - x), p := (sm - x - 1)] else if as = 3 then \ x. x < lm ! m \ lm' = lm[m := x, n := (sn + sm - x), p := (sm - x)] else if as = 4 then \ x. x \ lm ! m \ lm' = lm[m := x, n := (sn + sm), p := (sm - x)] else if as = 5 then \ x. x < lm ! m \ lm' = lm[m := x, n := (sn + sm), p := (sm - x - 1)] else if as = 6 then \ x. x < lm ! m \ lm' = lm[m := Suc x, n := (sn + sm), p := (sm - x - 1)] else if as = 7 then lm' = lm[m := sm, n := (sn + sm)] else False))" fun addition_stage1 :: "nat \ nat list \ nat \ nat \ nat" where "addition_stage1 (as, lm) m p = (if as = 0 \ as = 1 \ as = 2 \ as = 3 then 2 else if as = 4 \ as = 5 \ as = 6 then 1 else 0)" fun addition_stage2 :: "nat \ nat list \ nat \ nat \ nat" where "addition_stage2 (as, lm) m p = (if 0 \ as \ as \ 3 then lm ! m else if 4 \ as \ as \ 6 then lm ! p else 0)" fun addition_stage3 :: "nat \ nat list \ nat \ nat \ nat" where "addition_stage3 (as, lm) m p = (if as = 1 then 4 else if as = 2 then 3 else if as = 3 then 2 else if as = 0 then 1 else if as = 5 then 2 else if as = 6 then 1 else if as = 4 then 0 else 0)" fun addition_measure :: "((nat \ nat list) \ nat \ nat) \ (nat \ nat \ nat)" where "addition_measure ((as, lm), m, p) = (addition_stage1 (as, lm) m p, addition_stage2 (as, lm) m p, addition_stage3 (as, lm) m p)" definition addition_LE :: "(((nat \ nat list) \ nat \ nat) \ ((nat \ nat list) \ nat \ nat)) set" where "addition_LE \ (inv_image lex_triple addition_measure)" lemma wf_additon_LE[simp]: "wf addition_LE" by(auto simp: addition_LE_def lex_triple_def lex_pair_def) declare addition_inv.simps[simp del] lemma update_zero_to_zero[simp]: "\am ! n = (0::nat); n < length am\ \ am[n := 0] = am" apply(simp add: list_update_same_conv) done lemma addition_inv_init: "\m \ n; max m n < p; length lm > p; lm ! p = 0\ \ addition_inv (0, lm) m n p lm" apply(simp add: addition_inv.simps Let_def ) apply(rule_tac x = "lm ! m" in exI, simp) done lemma abs_fetch[simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)" "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)" "abc_fetch 2 (addition m n p) = Some (Inc p)" "abc_fetch 3 (addition m n p) = Some (Goto 0)" "abc_fetch 4 (addition m n p) = Some (Dec p 7)" "abc_fetch 5 (addition m n p) = Some (Inc m)" "abc_fetch 6 (addition m n p) = Some (Goto 4)" by(simp_all add: abc_fetch.simps addition.simps) lemma exists_small_list_elem1[simp]: "\m \ n; p < length lm; lm ! p = 0; m < p; n < p; x \ lm ! m; 0 < x\ \ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\ \ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\ \ \xam \ n; p < length lm; lm ! p = (0::nat); m < p; n < p; x < lm ! m\ \ \xa\lm ! m. lm[m := x, n := lm ! n + lm ! m - x, p := lm ! m - x] = lm[m := xa, n := lm ! n + lm ! m - xa, p := lm ! m - xa]" apply(rule_tac x = x in exI, simp) done lemma exists_small_list_elem5[simp]: "\m \ n; p < length lm; lm ! p = 0; m < p; n < p; x \ lm ! m; lm ! m \ x\ \ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\ \ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\ \ \xa\lm ! m. lm[m := Suc x, n := lm ! n + lm ! m, p := lm ! m - Suc x] = lm[m := xa, n := lm ! n + lm ! m, p := lm ! m - xa]" apply(rule_tac x = "Suc x" in exI, simp) done lemma abc_steps_zero: "abc_steps_l asm ap 0 = asm" apply(cases asm, simp add: abc_steps_l.simps) done lemma list_double_update_2: "lm[a := x, b := y, a := z] = lm[b := y, a:=z]" by (metis list_update_overwrite list_update_swap) declare Let_def[simp] lemma addition_halt_lemma: "\m \ n; max m n < p; length lm > p\ \ \na. \ (\(as, lm') (m, p). as = 7) (abc_steps_l (0, lm) (addition m n p) na) (m, p) \ addition_inv (abc_steps_l (0, lm) (addition m n p) na) m n p lm \ addition_inv (abc_steps_l (0, lm) (addition m n p) (Suc na)) m n p lm \ ((abc_steps_l (0, lm) (addition m n p) (Suc na), m, p), abc_steps_l (0, lm) (addition m n p) na, m, p) \ addition_LE" proof - assume assms_1: "m\n" and assms_2: "max m n < p" and assms_3: "length lm > p" { fix na obtain a b where ab:"abc_steps_l (0, lm) (addition m n p) na = (a, b)" by force assume assms2: "\ (\(as, lm') (m, p). as = 7) (abc_steps_l (0, lm) (addition m n p) na) (m, p)" "addition_inv (abc_steps_l (0, lm) (addition m n p) na) m n p lm" have r1:"addition_inv (abc_steps_l (0, lm) (addition m n p) (Suc na)) m n p lm" using assms_1 assms_2 assms_3 assms2 unfolding abc_step_red2 ab abc_step_l.simps abc_lm_v.simps abc_lm_s.simps addition_inv.simps by (auto split:if_splits simp add: addition_inv.simps Suc_diff_Suc) have r2:"((abc_steps_l (0, lm) (addition m n p) (Suc na), m, p), abc_steps_l (0, lm) (addition m n p) na, m, p) \ addition_LE" using assms_1 assms_2 assms_3 assms2 unfolding abc_step_red2 ab apply(auto split:if_splits simp add: addition_inv.simps abc_steps_zero) by(auto simp add: addition_LE_def lex_triple_def lex_pair_def abc_step_l.simps abc_lm_v.simps abc_lm_s.simps split: if_splits) note r1 r2 } thus ?thesis by auto qed lemma addition_correct': "\m \ n; max m n < p; length lm > p; lm ! p = 0\ \ \ stp. (\ (as, lm'). as = 7 \ addition_inv (as, lm') m n p lm) (abc_steps_l (0, lm) (addition m n p) stp)" apply(insert halt_lemma2[of addition_LE "\ ((as, lm'), m, p). addition_inv (as, lm') m n p lm" "\ stp. (abc_steps_l (0, lm) (addition m n p) stp, m, p)" "\ ((as, lm'), m, p). as = 7"], simp add: abc_steps_zero addition_inv_init) apply(drule_tac addition_halt_lemma,force,force) apply (simp,erule_tac exE) apply(rename_tac na) apply(rule_tac x = na in exI) apply(auto) done lemma length_addition[simp]: "length (addition a b c) = 7" by(auto simp: addition.simps) lemma addition_correct: assumes "m \ n" "max m n < p" "length lm > p" "lm ! p = 0" shows "\\ a. a = lm\ (addition m n p) \\ nl. addition_inv (7, nl) m n p lm\" using assms proof(rule_tac abc_Hoare_haltI, simp) fix lma assume "m \ n" "m < p \ n < p" "p < length lm" "lm ! p = 0" then have "\ stp. (\ (as, lm'). as = 7 \ addition_inv (as, lm') m n p lm) (abc_steps_l (0, lm) (addition m n p) stp)" by(rule_tac addition_correct', auto simp: addition_inv.simps) then obtain stp where "(\ (as, lm'). as = 7 \ addition_inv (as, lm') m n p lm) (abc_steps_l (0, lm) (addition m n p) stp)" using exE by presburger thus "\na. abc_final (abc_steps_l (0, lm) (addition m n p) na) (addition m n p) \ (\nl. addition_inv (7, nl) m n p lm) abc_holds_for abc_steps_l (0, lm) (addition m n p) na" by(auto intro:exI[of _ stp]) qed subsubsection \Correctness of compilation for constructor s\ lemma compile_s_correct': "\\nl. nl = n # 0 \ 2 @ anything\ addition 0 (Suc 0) 2 [+] [Inc (Suc 0)] \\nl. nl = n # Suc n # 0 # anything\" proof(rule_tac abc_Hoare_plus_halt) show "\\nl. nl = n # 0 \ 2 @ anything\ addition 0 (Suc 0) 2 \\ nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \ 2 @ anything)\" by(rule_tac addition_correct, auto simp: numeral_2_eq_2) next show "\\nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \ 2 @ anything)\ [Inc (Suc 0)] \\nl. nl = n # Suc n # 0 # anything\" by(rule_tac abc_Hoare_haltI, rule_tac x = 1 in exI, auto simp: addition_inv.simps abc_steps_l.simps abc_step_l.simps abc_fetch.simps numeral_2_eq_2 abc_lm_s.simps abc_lm_v.simps) qed declare rec_exec.simps[simp del] lemma abc_comp_commute: "(A [+] B) [+] C = A [+] (B [+] C)" apply(auto simp: abc_comp.simps abc_shift.simps) apply(rename_tac x) apply(case_tac x, auto) done lemma compile_s_correct: "\rec_ci s = (ap, arity, fp); rec_exec s [n] = r\ \ \\nl. nl = n # 0 \ (fp - arity) @ anything\ ap \\nl. nl = n # r # 0 \ (fp - Suc arity) @ anything\" apply(auto simp: rec_ci.simps rec_ci_s_def compile_s_correct' rec_exec.simps) done subsubsection \Correctness of compilation for constructor z\ lemma compile_z_correct: "\rec_ci z = (ap, arity, fp); rec_exec z [n] = r\ \ \\nl. nl = n # 0 \ (fp - arity) @ anything\ ap \\nl. nl = n # r # 0 \ (fp - Suc arity) @ anything\" apply(rule_tac abc_Hoare_haltI) apply(rule_tac x = 1 in exI) apply(auto simp: abc_steps_l.simps rec_ci.simps rec_ci_z_def numeral_2_eq_2 abc_fetch.simps abc_step_l.simps rec_exec.simps) done subsubsection \Correctness of compilation for constructor id\ lemma compile_id_correct': assumes "n < length args" shows "\\nl. nl = args @ 0 \ 2 @ anything\ addition n (length args) (Suc (length args)) \\nl. nl = args @ rec_exec (recf.id (length args) n) args # 0 # anything\" proof - have "\\nl. nl = args @ 0 \ 2 @ anything\ addition n (length args) (Suc (length args)) \\nl. addition_inv (7, nl) n (length args) (Suc (length args)) (args @ 0 \ 2 @ anything)\" using assms by(rule_tac addition_correct, auto simp: numeral_2_eq_2 nth_append) thus "?thesis" using assms by(simp add: addition_inv.simps rec_exec.simps nth_append numeral_2_eq_2 list_update_append) qed lemma compile_id_correct: "\n < m; length xs = m; rec_ci (recf.id m n) = (ap, arity, fp); rec_exec (recf.id m n) xs = r\ \ \\nl. nl = xs @ 0 \ (fp - arity) @ anything\ ap \\nl. nl = xs @ r # 0 \ (fp - Suc arity) @ anything\" apply(auto simp: rec_ci.simps rec_ci_id.simps compile_id_correct') done subsubsection \Correctness of compilation for constructor Cn\ lemma cn_merge_gs_tl_app: "cn_merge_gs (gs @ [g]) pstr = cn_merge_gs gs pstr [+] cn_merge_gs [g] (pstr + length gs)" apply(induct gs arbitrary: pstr, simp add: cn_merge_gs.simps, auto) apply(simp add: abc_comp_commute) done lemma footprint_ge: "rec_ci a = (p, arity, fp) \ arity < fp" proof(induct a) case (Cn x1 a x3) then show ?case by(cases "rec_ci a", auto simp:rec_ci.simps) next case (Pr x1 a1 a2) then show ?case by(cases "rec_ci a1";cases "rec_ci a2", auto simp:rec_ci.simps) next case (Mn x1 a) then show ?case by(cases "rec_ci a", auto simp:rec_ci.simps) qed (auto simp: rec_ci.simps) lemma param_pattern: "\terminate f xs; rec_ci f = (p, arity, fp)\ \ length xs = arity" proof(induct arbitrary: p arity fp rule: terminate.induct) case (termi_cn f xs gs n) thus ?case by(cases "rec_ci f", (auto simp: rec_ci.simps)) next case (termi_pr x g xs n f) thus ?case by (cases "rec_ci f", cases "rec_ci g", auto simp: rec_ci.simps) next case (termi_mn xs n f r) thus ?case by (cases "rec_ci f", auto simp: rec_ci.simps) qed (auto simp: rec_ci.simps) lemma replicate_merge_anywhere: "x\a @ x\b @ ys = x\(a+b) @ ys" by(simp add:replicate_add) fun mv_box_inv :: "nat \ nat list \ nat \ nat \ nat list \ bool" where "mv_box_inv (as, lm) m n initlm = (let plus = initlm ! m + initlm ! n in length initlm > max m n \ m \ n \ (if as = 0 then \ k l. lm = initlm[m := k, n := l] \ k + l = plus \ k \ initlm ! m else if as = 1 then \ k l. lm = initlm[m := k, n := l] \ k + l + 1 = plus \ k < initlm ! m else if as = 2 then \ k l. lm = initlm[m := k, n := l] \ k + l = plus \ k \ initlm ! m else if as = 3 then lm = initlm[m := 0, n := plus] else False))" fun mv_box_stage1 :: "nat \ nat list \ nat \ nat" where "mv_box_stage1 (as, lm) m = (if as = 3 then 0 else 1)" fun mv_box_stage2 :: "nat \ nat list \ nat \ nat" where "mv_box_stage2 (as, lm) m = (lm ! m)" fun mv_box_stage3 :: "nat \ nat list \ nat \ nat" where "mv_box_stage3 (as, lm) m = (if as = 1 then 3 else if as = 2 then 2 else if as = 0 then 1 else 0)" fun mv_box_measure :: "((nat \ nat list) \ nat) \ (nat \ nat \ nat)" where "mv_box_measure ((as, lm), m) = (mv_box_stage1 (as, lm) m, mv_box_stage2 (as, lm) m, mv_box_stage3 (as, lm) m)" definition lex_pair :: "((nat \ nat) \ nat \ nat) set" where "lex_pair = less_than <*lex*> less_than" definition lex_triple :: "((nat \ (nat \ nat)) \ (nat \ (nat \ nat))) set" where "lex_triple \ less_than <*lex*> lex_pair" definition mv_box_LE :: "(((nat \ nat list) \ nat) \ ((nat \ nat list) \ nat)) set" where "mv_box_LE \ (inv_image lex_triple mv_box_measure)" lemma wf_lex_triple: "wf lex_triple" by (auto simp:lex_triple_def lex_pair_def) lemma wf_mv_box_le[intro]: "wf mv_box_LE" by(auto intro:wf_lex_triple simp: mv_box_LE_def) declare mv_box_inv.simps[simp del] lemma mv_box_inv_init: "\m < length initlm; n < length initlm; m \ n\ \ mv_box_inv (0, initlm) m n initlm" apply(simp add: abc_steps_l.simps mv_box_inv.simps) apply(rule_tac x = "initlm ! m" in exI, rule_tac x = "initlm ! n" in exI, simp) done lemma abc_fetch[simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)" "abc_fetch (Suc 0) (mv_box m n) = Some (Inc n)" "abc_fetch 2 (mv_box m n) = Some (Goto 0)" "abc_fetch 3 (mv_box m n) = None" apply(simp_all add: mv_box.simps abc_fetch.simps) done lemma replicate_Suc_iff_anywhere: "x # x\b @ ys = x\(Suc b) @ ys" by simp lemma exists_smaller_in_list0[simp]: "\m \ n; m < length initlm; n < length initlm; k + l = initlm ! m + initlm ! n; k \ initlm ! m; 0 < k\ \ \ka la. initlm[m := k, n := l, m := k - Suc 0] = initlm[m := ka, n := la] \ Suc (ka + la) = initlm ! m + initlm ! n \ ka < initlm ! m" apply(rule_tac x = "k - Suc 0" in exI, rule_tac x = l in exI, auto) apply(subgoal_tac "initlm[m := k, n := l, m := k - Suc 0] = initlm[n := l, m := k, m := k - Suc 0]",force intro:list_update_swap) by(simp add: list_update_swap) lemma exists_smaller_in_list1[simp]: "\m \ n; m < length initlm; n < length initlm; Suc (k + l) = initlm ! m + initlm ! n; k < initlm ! m\ \ \ka la. initlm[m := k, n := l, n := Suc l] = initlm[m := ka, n := la] \ ka + la = initlm ! m + initlm ! n \ ka \ initlm ! m" apply(rule_tac x = k in exI, rule_tac x = "Suc l" in exI, auto) done lemma abc_steps_prop[simp]: "\length initlm > max m n; m \ n\ \ \ (\(as, lm) m. as = 3) (abc_steps_l (0, initlm) (mv_box m n) na) m \ mv_box_inv (abc_steps_l (0, initlm) (mv_box m n) na) m n initlm \ mv_box_inv (abc_steps_l (0, initlm) (mv_box m n) (Suc na)) m n initlm \ ((abc_steps_l (0, initlm) (mv_box m n) (Suc na), m), abc_steps_l (0, initlm) (mv_box m n) na, m) \ mv_box_LE" apply(rule impI, simp add: abc_step_red2) apply(cases "(abc_steps_l (0, initlm) (mv_box m n) na)", simp) apply(auto split:if_splits simp add:abc_steps_l.simps mv_box_inv.simps) apply(auto simp add: mv_box_LE_def lex_triple_def lex_pair_def abc_step_l.simps abc_steps_l.simps mv_box_inv.simps abc_lm_v.simps abc_lm_s.simps split: if_splits ) apply(rule_tac x = k in exI, rule_tac x = "Suc l" in exI, simp) done lemma mv_box_inv_halt: "\length initlm > max m n; m \ n\ \ \ stp. (\ (as, lm). as = 3 \ mv_box_inv (as, lm) m n initlm) (abc_steps_l (0::nat, initlm) (mv_box m n) stp)" apply(insert halt_lemma2[of mv_box_LE "\ ((as, lm), m). mv_box_inv (as, lm) m n initlm" "\ stp. (abc_steps_l (0, initlm) (mv_box m n) stp, m)" "\ ((as, lm), m). as = (3::nat)" ]) apply(insert wf_mv_box_le) apply(simp add: mv_box_inv_init abc_steps_zero) apply(erule_tac exE) by (metis (no_types, lifting) case_prodE' case_prodI) lemma mv_box_halt_cond: "\m \ n; mv_box_inv (a, b) m n lm; a = 3\ \ b = lm[n := lm ! m + lm ! n, m := 0]" apply(simp add: mv_box_inv.simps, auto) apply(simp add: list_update_swap) done lemma mv_box_correct': "\length lm > max m n; m \ n\ \ \ stp. abc_steps_l (0::nat, lm) (mv_box m n) stp = (3, (lm[n := (lm ! m + lm ! n)])[m := 0::nat])" by(drule mv_box_inv_halt, auto dest:mv_box_halt_cond) lemma length_mvbox[simp]: "length (mv_box m n) = 3" by(simp add: mv_box.simps) lemma mv_box_correct: "\length lm > max m n; m\n\ \ \\ nl. nl = lm\ mv_box m n \\ nl. nl = lm[n := (lm ! m + lm ! n), m:=0]\" apply(drule_tac mv_box_correct', simp) apply(auto simp: abc_Hoare_halt_def) by (metis abc_final.simps abc_holds_for.simps length_mvbox) declare list_update.simps(2)[simp del] lemma zero_case_rec_exec[simp]: "\length xs < gf; gf \ ft; n < length gs\ \ (rec_exec (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) [ft + n - length xs := rec_exec (gs ! n) xs, 0 := 0] = 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything" using list_update_append[of "rec_exec (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_exec i xs) (take n gs)" "0 \ (length gs - n) @ 0 # 0 \ length xs @ anything" "ft + n - length xs" "rec_exec (gs ! n) xs"] apply(auto) apply(cases "length gs - n", simp, simp add: list_update.simps replicate_Suc_iff_anywhere Suc_diff_Suc del: replicate_Suc) apply(simp add: list_update.simps) done lemma compile_cn_gs_correct': assumes g_cond: "\g\set (take n gs). terminate g xs \ (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. \\nl. nl = xs @ 0 \ (xb - xa) @ xc\ x \\nl. nl = xs @ rec_exec g xs # 0 \ (xb - Suc xa) @ xc\))" and ft: "ft = max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" shows "\\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything\ cn_merge_gs (map rec_ci (take n gs)) ft \\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ 0\(length gs - n) @ 0 \ Suc (length xs) @ anything\" using g_cond proof(induct n) case 0 have "ft > length xs" using ft by simp thus "?case" apply(rule_tac abc_Hoare_haltI) apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps replicate_add[THEN sym] replicate_Suc[THEN sym] del: replicate_Suc) done next case (Suc n) have ind': "\g\set (take n gs). terminate g xs \ (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. \\nl. nl = xs @ 0 \ (xb - xa) @ xc\ x \\nl. nl = xs @ rec_exec g xs # 0 \ (xb - Suc xa) @ xc\)) \ \\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything\ cn_merge_gs (map rec_ci (take n gs)) ft \\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything\" by fact have g_newcond: "\g\set (take (Suc n) gs). terminate g xs \ (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. \\nl. nl = xs @ 0 \ (xb - xa) @ xc\ x \\nl. nl = xs @ rec_exec g xs # 0 \ (xb - Suc xa) @ xc\))" by fact from g_newcond have ind: "\\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything\ cn_merge_gs (map rec_ci (take n gs)) ft \\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything\" apply(rule_tac ind', rule_tac ballI, erule_tac x = g in ballE, simp_all add: take_Suc) by(cases "n < length gs", simp add:take_Suc_conv_app_nth, simp) show "?case" proof(cases "n < length gs") case True have h: "n < length gs" by fact thus "?thesis" proof(simp add: take_Suc_conv_app_nth cn_merge_gs_tl_app) obtain gp ga gf where a: "rec_ci (gs!n) = (gp, ga, gf)" by (metis prod_cases3) moreover have "min (length gs) n = n" using h by simp moreover have "\\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything\ cn_merge_gs (map rec_ci (take n gs)) ft [+] (gp [+] mv_box ga (ft + n)) \\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything\" proof(rule_tac abc_Hoare_plus_halt) show "\\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything\ cn_merge_gs (map rec_ci (take n gs)) ft \\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything\" using ind by simp next have x: "gs!n \ set (take (Suc n) gs)" using h by(simp add: take_Suc_conv_app_nth) have b: "terminate (gs!n) xs" using a g_newcond h x by(erule_tac x = "gs!n" in ballE, simp_all) hence c: "length xs = ga" using a param_pattern by metis have d: "gf > ga" using footprint_ge a by simp have e: "ft \ gf" using ft a h Max_ge image_eqI by(simp, rule_tac max.coboundedI2, rule_tac Max_ge, simp, rule_tac insertI2, rule_tac f = "(\(aprog, p, n). n)" and x = "rec_ci (gs!n)" in image_eqI, simp, rule_tac x = "gs!n" in image_eqI, simp, simp) show "\\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything\ gp [+] mv_box ga (ft + n) \\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything\" proof(rule_tac abc_Hoare_plus_halt) show "\\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything\ gp \\nl. nl = xs @ (rec_exec (gs!n) xs) # 0 \ (ft - Suc (length xs)) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything\" proof - have "(\\nl. nl = xs @ 0 \ (gf - ga) @ 0\(ft - gf)@map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything\ gp \\nl. nl = xs @ (rec_exec (gs!n) xs) # 0 \ (gf - Suc ga) @ 0\(ft - gf)@map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 \ Suc (length xs) @ anything\)" using a g_newcond h x apply(erule_tac x = "gs!n" in ballE) apply(simp, simp) done thus "?thesis" using a b c d e by(simp add: replicate_merge_anywhere) qed next show "\\nl. nl = xs @ rec_exec (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything\ mv_box ga (ft + n) \\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything\" proof - have "\\nl. nl = xs @ rec_exec (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything\ mv_box ga (ft + n) \\nl. nl = (xs @ rec_exec (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) [ft + n := (xs @ rec_exec (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) ! ga + (xs @ rec_exec (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) ! (ft + n), ga := 0]\" using a c d e h apply(rule_tac mv_box_correct) apply(simp_all) done moreover have "(xs @ rec_exec (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) [ft + n := (xs @ rec_exec (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) ! ga + (xs @ rec_exec (gs ! n) xs # 0 \ (ft - Suc (length xs)) @ map (\i. rec_exec i xs) (take n gs) @ 0 \ (length gs - n) @ 0 # 0 \ length xs @ anything) ! (ft + n), ga := 0]= xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything" using a c d e h by(simp add: list_update_append nth_append split: if_splits, auto) ultimately show "?thesis" by(simp) qed qed qed ultimately show "\\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything\ cn_merge_gs (map rec_ci (take n gs)) ft [+] (case rec_ci (gs ! n) of (gprog, gpara, gn) \ gprog [+] mv_box gpara (ft + n)) \\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \ (length gs - Suc n) @ 0 # 0 \ length xs @ anything\" by simp qed next case False have h: "\ n < length gs" by fact hence ind': "\\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything\ cn_merge_gs (map rec_ci gs) ft \\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) gs @ 0 \ Suc (length xs) @ anything\" using ind by simp thus "?thesis" using h by(simp) qed qed lemma compile_cn_gs_correct: assumes g_cond: "\g\set gs. terminate g xs \ (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. \\nl. nl = xs @ 0 \ (xb - xa) @ xc\ x \\nl. nl = xs @ rec_exec g xs # 0 \ (xb - Suc xa) @ xc\))" and ft: "ft = max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" shows "\\nl. nl = xs @ 0 # 0 \ (ft + length gs) @ anything\ cn_merge_gs (map rec_ci gs) ft \\nl. nl = xs @ 0 \ (ft - length xs) @ map (\i. rec_exec i xs) gs @ 0 \ Suc (length xs) @ anything\" using assms using compile_cn_gs_correct'[of "length gs" gs xs ft ffp anything ] apply(auto) done lemma length_mvboxes[simp]: "length (mv_boxes aa ba n) = 3*n" by(induct n, auto simp: mv_boxes.simps) lemma exp_suc: "a\Suc b = a\b @ [a]" by(simp add: exp_ind del: replicate.simps) lemma last_0[simp]: "\Suc n \ ba - aa; length lm2 = Suc n; length lm3 = ba - Suc (aa + n)\ \ (last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba - aa) = (0::nat)" proof - assume h: "Suc n \ ba - aa" and g: "length lm2 = Suc n" "length lm3 = ba - Suc (aa + n)" from h and g have k: "ba - aa = Suc (length lm3 + n)" by arith from k show "(last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba - aa) = 0" apply(simp, insert g) apply(simp add: nth_append) done qed lemma butlast_last[simp]: "length lm1 = aa \ (lm1 @ 0\n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (aa + n) = last lm2" apply(simp add: nth_append) done lemma arith_as_simp[simp]: "\Suc n \ ba - aa; aa < ba\ \ (ba < Suc (aa + (ba - Suc (aa + n) + n))) = False" apply arith done lemma butlast_elem[simp]: "\Suc n \ ba - aa; aa < ba; length lm1 = aa; length lm2 = Suc n; length lm3 = ba - Suc (aa + n)\ \ (lm1 @ 0\n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba + n) = 0" using nth_append[of "lm1 @ (0::'a)\n @ last lm2 # lm3 @ butlast lm2" "(0::'a) # lm4" "ba + n"] apply(simp) done lemma update_butlast_eq0[simp]: "\Suc n \ ba - aa; aa < ba; length lm1 = aa; length lm2 = Suc n; length lm3 = ba - Suc (aa + n)\ \ (lm1 @ 0\n @ last lm2 # lm3 @ butlast lm2 @ (0::nat) # lm4) [ba + n := last lm2, aa + n := 0] = lm1 @ 0 # 0\n @ lm3 @ lm2 @ lm4" using list_update_append[of "lm1 @ 0\n @ last lm2 # lm3 @ butlast lm2" "0 # lm4" "ba + n" "last lm2"] apply(simp add: list_update_append list_update.simps(2-) replicate_Suc_iff_anywhere exp_suc del: replicate_Suc) apply(cases lm2, simp, simp) done lemma update_butlast_eq1[simp]: "\Suc (length lm1 + n) \ ba; length lm2 = Suc n; length lm3 = ba - Suc (length lm1 + n); \ ba - Suc (length lm1) < ba - Suc (length lm1 + n); \ ba + n - length lm1 < n\ \ (0::nat) \ n @ (last lm2 # lm3 @ butlast lm2 @ 0 # lm4)[ba - length lm1 := last lm2, 0 := 0] = 0 # 0 \ n @ lm3 @ lm2 @ lm4" apply(subgoal_tac "ba - length lm1 = Suc n + length lm3", simp add: list_update.simps(2-) list_update_append) apply(simp add: replicate_Suc_iff_anywhere exp_suc del: replicate_Suc) apply(cases lm2, simp, simp) apply(auto) done lemma mv_boxes_correct: "\aa + n \ ba; ba > aa; length lm1 = aa; length lm2 = n; length lm3 = ba - aa - n\ \ \\ nl. nl = lm1 @ lm2 @ lm3 @ 0\n @ lm4\ (mv_boxes aa ba n) \\ nl. nl = lm1 @ 0\n @ lm3 @ lm2 @ lm4\" proof(induct n arbitrary: lm2 lm3 lm4) case 0 thus "?case" by(simp add: mv_boxes.simps abc_Hoare_halt_def, rule_tac x = 0 in exI, simp add: abc_steps_l.simps) next case (Suc n) have ind: "\lm2 lm3 lm4. \aa + n \ ba; aa < ba; length lm1 = aa; length lm2 = n; length lm3 = ba - aa - n\ \ \\nl. nl = lm1 @ lm2 @ lm3 @ 0 \ n @ lm4\ mv_boxes aa ba n \\nl. nl = lm1 @ 0 \ n @ lm3 @ lm2 @ lm4\" by fact have h1: "aa + Suc n \ ba" by fact have h2: "aa < ba" by fact have h3: "length lm1 = aa" by fact have h4: "length lm2 = Suc n" by fact have h5: "length lm3 = ba - aa - Suc n" by fact have "\\nl. nl = lm1 @ lm2 @ lm3 @ 0 \ Suc n @ lm4\ mv_boxes aa ba n [+] mv_box (aa + n) (ba + n) \\nl. nl = lm1 @ 0 \ Suc n @ lm3 @ lm2 @ lm4\" proof(rule_tac abc_Hoare_plus_halt) have "\\nl. nl = lm1 @ butlast lm2 @ (last lm2 # lm3) @ 0 \ n @ (0 # lm4)\ mv_boxes aa ba n \\ nl. nl = lm1 @ 0\n @ (last lm2 # lm3) @ butlast lm2 @ (0 # lm4)\" using h1 h2 h3 h4 h5 by(rule_tac ind, simp_all) moreover have " lm1 @ butlast lm2 @ (last lm2 # lm3) @ 0 \ n @ (0 # lm4) = lm1 @ lm2 @ lm3 @ 0 \ Suc n @ lm4" using h4 by(simp add: replicate_Suc[THEN sym] exp_suc del: replicate_Suc, cases lm2, simp_all) ultimately show "\\nl. nl = lm1 @ lm2 @ lm3 @ 0 \ Suc n @ lm4\ mv_boxes aa ba n \\ nl. nl = lm1 @ 0\n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4\" by (metis append_Cons) next let ?lm = "lm1 @ 0 \ n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4" have "\\nl. nl = ?lm\ mv_box (aa + n) (ba + n) \\ nl. nl = ?lm[(ba + n) := ?lm!(aa+n) + ?lm!(ba+n), (aa+n):=0]\" using h1 h2 h3 h4 h5 by(rule_tac mv_box_correct, simp_all) moreover have "?lm[(ba + n) := ?lm!(aa+n) + ?lm!(ba+n), (aa+n):=0] = lm1 @ 0 \ Suc n @ lm3 @ lm2 @ lm4" using h1 h2 h3 h4 h5 by(auto simp: nth_append list_update_append split: if_splits) ultimately show "\\nl. nl = lm1 @ 0 \ n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4\ mv_box (aa + n) (ba + n) \\nl. nl = lm1 @ 0 \ Suc n @ lm3 @ lm2 @ lm4\" by simp qed thus "?case" by(simp add: mv_boxes.simps) qed lemma update_butlast_eq2[simp]: "\Suc n \ aa - length lm1; length lm1 < aa; length lm2 = aa - Suc (length lm1 + n); length lm3 = Suc n; \ aa - Suc (length lm1) < aa - Suc (length lm1 + n); \ aa + n - length lm1 < n\ \ butlast lm3 @ ((0::nat) # lm2 @ 0 \ n @ last lm3 # lm4)[0 := last lm3, aa - length lm1 := 0] = lm3 @ lm2 @ 0 # 0 \ n @ lm4" apply(subgoal_tac "aa - length lm1 = length lm2 + Suc n") apply(simp add: list_update.simps list_update_append) apply(simp add: replicate_Suc[THEN sym] exp_suc del: replicate_Suc) apply(cases lm3, simp, simp) apply(auto) done lemma mv_boxes_correct2: "\n \ aa - ba; ba < aa; length (lm1::nat list) = ba; length (lm2::nat list) = aa - ba - n; length (lm3::nat list) = n\ \\\ nl. nl = lm1 @ 0\n @ lm2 @ lm3 @ lm4\ (mv_boxes aa ba n) \\ nl. nl = lm1 @ lm3 @ lm2 @ 0\n @ lm4\" proof(induct n arbitrary: lm2 lm3 lm4) case 0 thus "?case" by(simp add: mv_boxes.simps abc_Hoare_halt_def, rule_tac x = 0 in exI, simp add: abc_steps_l.simps) next case (Suc n) have ind: "\lm2 lm3 lm4. \n \ aa - ba; ba < aa; length lm1 = ba; length lm2 = aa - ba - n; length lm3 = n\ \ \\nl. nl = lm1 @ 0 \ n @ lm2 @ lm3 @ lm4\ mv_boxes aa ba n \\nl. nl = lm1 @ lm3 @ lm2 @ 0 \ n @ lm4\" by fact have h1: "Suc n \ aa - ba" by fact have h2: "ba < aa" by fact have h3: "length lm1 = ba" by fact have h4: "length lm2 = aa - ba - Suc n" by fact have h5: "length lm3 = Suc n" by fact have "\\nl. nl = lm1 @ 0 \ Suc n @ lm2 @ lm3 @ lm4\ mv_boxes aa ba n [+] mv_box (aa + n) (ba + n) \\nl. nl = lm1 @ lm3 @ lm2 @ 0 \ Suc n @ lm4\" proof(rule_tac abc_Hoare_plus_halt) have "\\ nl. nl = lm1 @ 0 \ n @ (0 # lm2) @ (butlast lm3) @ (last lm3 # lm4)\ mv_boxes aa ba n \\ nl. nl = lm1 @ butlast lm3 @ (0 # lm2) @ 0\n @ (last lm3 # lm4)\" using h1 h2 h3 h4 h5 by(rule_tac ind, simp_all) moreover have "lm1 @ 0 \ n @ (0 # lm2) @ (butlast lm3) @ (last lm3 # lm4) = lm1 @ 0 \ Suc n @ lm2 @ lm3 @ lm4" using h5 by(simp add: replicate_Suc_iff_anywhere exp_suc del: replicate_Suc, cases lm3, simp_all) ultimately show "\\nl. nl = lm1 @ 0 \ Suc n @ lm2 @ lm3 @ lm4\ mv_boxes aa ba n \\ nl. nl = lm1 @ butlast lm3 @ (0 # lm2) @ 0\n @ (last lm3 # lm4)\" by metis next thm mv_box_correct let ?lm = "lm1 @ butlast lm3 @ (0 # lm2) @ 0 \ n @ last lm3 # lm4" have "\\nl. nl = ?lm\ mv_box (aa + n) (ba + n) \\nl. nl = ?lm[ba+n := ?lm!(aa+n)+?lm!(ba+n), (aa+n):=0]\" using h1 h2 h3 h4 h5 by(rule_tac mv_box_correct, simp_all) moreover have "?lm[ba+n := ?lm!(aa+n)+?lm!(ba+n), (aa+n):=0] = lm1 @ lm3 @ lm2 @ 0 \ Suc n @ lm4" using h1 h2 h3 h4 h5 by(auto simp: nth_append list_update_append split: if_splits) ultimately show "\\nl. nl = lm1 @ butlast lm3 @ (0 # lm2) @ 0 \ n @ last lm3 # lm4\ mv_box (aa + n) (ba + n) \\nl. nl = lm1 @ lm3 @ lm2 @ 0 \ Suc n @ lm4\" by simp qed thus "?case" by(simp add: mv_boxes.simps) qed lemma save_paras: "\\nl. nl = xs @ 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) - length xs) @ map (\i. rec_exec i xs) gs @ 0 \ Suc (length xs) @ anything\ mv_boxes 0 (Suc (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) (length xs) \\nl. nl = 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\i. rec_exec i xs) gs @ 0 # xs @ anything\" proof - let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" have "\\nl. nl = [] @ xs @ (0\(?ft - length xs) @ map (\i. rec_exec i xs) gs @ [0]) @ 0 \ (length xs) @ anything\ mv_boxes 0 (Suc ?ft + length gs) (length xs) \\nl. nl = [] @ 0 \ (length xs) @ (0\(?ft - length xs) @ map (\i. rec_exec i xs) gs @ [0]) @ xs @ anything\" by(rule_tac mv_boxes_correct, auto) thus "?thesis" by(simp add: replicate_merge_anywhere) qed lemma length_le_max_insert_rec_ci[intro]: "length gs \ ffp \ length gs \ max x1 (Max (insert ffp (x2 ` x3 ` set gs)))" apply(rule_tac max.coboundedI2) apply(simp add: Max_ge_iff) done lemma restore_new_paras: "ffp \ length gs \ \\nl. nl = 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\i. rec_exec i xs) gs @ 0 # xs @ anything\ mv_boxes (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))) 0 (length gs) \\nl. nl = map (\i. rec_exec i xs) gs @ 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ 0 # xs @ anything\" proof - let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" assume j: "ffp \ length gs" hence "\\ nl. nl = [] @ 0\length gs @ 0\(?ft - length gs) @ map (\i. rec_exec i xs) gs @ ((0 # xs) @ anything)\ mv_boxes ?ft 0 (length gs) \\ nl. nl = [] @ map (\i. rec_exec i xs) gs @ 0\(?ft - length gs) @ 0\length gs @ ((0 # xs) @ anything)\" by(rule_tac mv_boxes_correct2, auto) moreover have "?ft \ length gs" using j by(auto) ultimately show "?thesis" using j by(simp add: replicate_merge_anywhere le_add_diff_inverse) qed lemma le_max_insert[intro]: "ffp \ max x0 (Max (insert ffp (x1 ` x2 ` set gs)))" by (rule max.coboundedI2) auto declare max_less_iff_conj[simp del] lemma save_rs: "\far = length gs; ffp \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))); far < ffp\ \ \\nl. nl = map (\i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ xs @ anything\ mv_box far (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))) \\nl. nl = map (\i. rec_exec i xs) gs @ 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) - length gs) @ rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything\" proof - let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" thm mv_box_correct let ?lm= " map (\i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \ ?ft @ xs @ anything" assume h: "far = length gs" "ffp \ ?ft" "far < ffp" hence "\\ nl. nl = ?lm\ mv_box far ?ft \\ nl. nl = ?lm[?ft := ?lm!far + ?lm!?ft, far := 0]\" apply(rule_tac mv_box_correct) by( auto) moreover have "?lm[?ft := ?lm!far + ?lm!?ft, far := 0] = map (\i. rec_exec i xs) gs @ 0 \ (?ft - length gs) @ rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything" using h apply(simp add: nth_append) using list_update_length[of "map (\i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (?ft - Suc (length gs))" 0 "0 \ length gs @ xs @ anything" "rec_exec (Cn (length xs) f gs) xs"] apply(simp add: replicate_merge_anywhere replicate_Suc_iff_anywhere del: replicate_Suc) by(simp add: list_update_append list_update.simps replicate_Suc_iff_anywhere del: replicate_Suc) ultimately show "?thesis" by(simp) qed lemma length_empty_boxes[simp]: "length (empty_boxes n) = 2*n" apply(induct n, simp, simp) done lemma empty_one_box_correct: "\\nl. nl = 0 \ n @ x # lm\ [Dec n 2, Goto 0] \\nl. nl = 0 # 0 \ n @ lm\" proof(induct x) case 0 thus "?case" by(simp add: abc_Hoare_halt_def, rule_tac x = 1 in exI, simp add: abc_steps_l.simps abc_step_l.simps abc_fetch.simps abc_lm_v.simps nth_append abc_lm_s.simps replicate_Suc[THEN sym] exp_suc del: replicate_Suc) next case (Suc x) have "\\nl. nl = 0 \ n @ x # lm\ [Dec n 2, Goto 0] \\nl. nl = 0 # 0 \ n @ lm\" by fact then obtain stp where "abc_steps_l (0, 0 \ n @ x # lm) [Dec n 2, Goto 0] stp = (Suc (Suc 0), 0 # 0 \ n @ lm)" apply(auto simp: abc_Hoare_halt_def) by (smt abc_final.simps abc_holds_for.elims(2) length_Cons list.size(3)) moreover have "abc_steps_l (0, 0\n @ Suc x # lm) [Dec n 2, Goto 0] (Suc (Suc 0)) = (0, 0 \ n @ x # lm)" by(auto simp: abc_steps_l.simps abc_step_l.simps abc_fetch.simps abc_lm_v.simps nth_append abc_lm_s.simps list_update.simps list_update_append) ultimately have "abc_steps_l (0, 0\n @ Suc x # lm) [Dec n 2, Goto 0] (Suc (Suc 0) + stp) = (Suc (Suc 0), 0 # 0\n @ lm)" by(simp only: abc_steps_add) thus "?case" apply(simp add: abc_Hoare_halt_def) apply(rule_tac x = "Suc (Suc stp)" in exI, simp) done qed lemma empty_boxes_correct: "length lm \ n \ \\ nl. nl = lm\ empty_boxes n \\ nl. nl = 0\n @ drop n lm\" proof(induct n) case 0 thus "?case" by(simp add: empty_boxes.simps abc_Hoare_halt_def, rule_tac x = 0 in exI, simp add: abc_steps_l.simps) next case (Suc n) have ind: "n \ length lm \ \\nl. nl = lm\ empty_boxes n \\nl. nl = 0 \ n @ drop n lm\" by fact have h: "Suc n \ length lm" by fact have "\\nl. nl = lm\ empty_boxes n [+] [Dec n 2, Goto 0] \\nl. nl = 0 # 0 \ n @ drop (Suc n) lm\" proof(rule_tac abc_Hoare_plus_halt) show "\\nl. nl = lm\ empty_boxes n \\nl. nl = 0 \ n @ drop n lm\" using h by(rule_tac ind, simp) next show "\\nl. nl = 0 \ n @ drop n lm\ [Dec n 2, Goto 0] \\nl. nl = 0 # 0 \ n @ drop (Suc n) lm\" using empty_one_box_correct[of n "lm ! n" "drop (Suc n) lm"] using h by(simp add: Cons_nth_drop_Suc) qed thus "?case" by(simp add: empty_boxes.simps) qed lemma insert_dominated[simp]: "length gs \ ffp \ length gs + (max xs (Max (insert ffp (x1 ` x2 ` set gs))) - length gs) = max xs (Max (insert ffp (x1 ` x2 ` set gs)))" apply(rule_tac le_add_diff_inverse) apply(rule_tac max.coboundedI2) apply(simp add: Max_ge_iff) done lemma clean_paras: "ffp \ length gs \ \\nl. nl = map (\i. rec_exec i xs) gs @ 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) - length gs) @ rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything\ empty_boxes (length gs) \\nl. nl = 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything\" proof- let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" assume h: "length gs \ ffp" let ?lm = "map (\i. rec_exec i xs) gs @ 0 \ (?ft - length gs) @ rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything" have "\\ nl. nl = ?lm\ empty_boxes (length gs) \\ nl. nl = 0\length gs @ drop (length gs) ?lm\" by(rule_tac empty_boxes_correct, simp) moreover have "0\length gs @ drop (length gs) ?lm = 0 \ ?ft @ rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything" using h by(simp add: replicate_merge_anywhere) ultimately show "?thesis" by metis qed lemma restore_rs: "\\nl. nl = 0 \ max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) @ rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything\ mv_box (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))) (length xs) \\nl. nl = 0 \ length xs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) - (length xs)) @ 0 \ length gs @ xs @ anything\" proof - let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" let ?lm = "0\(length xs) @ 0\(?ft - (length xs)) @ rec_exec (Cn (length xs) f gs) xs # 0 \ length gs @ xs @ anything" thm mv_box_correct have "\\ nl. nl = ?lm\ mv_box ?ft (length xs) \\ nl. nl = ?lm[length xs := ?lm!?ft + ?lm!(length xs), ?ft := 0]\" by(rule_tac mv_box_correct, simp, simp) moreover have "?lm[length xs := ?lm!?ft + ?lm!(length xs), ?ft := 0] = 0 \ length xs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (?ft - (length xs)) @ 0 \ length gs @ xs @ anything" apply(auto simp: list_update_append nth_append) (* ~ 7 sec *) apply(cases ?ft, simp_all add: Suc_diff_le list_update.simps) apply(simp add: exp_suc replicate_Suc[THEN sym] del: replicate_Suc) done ultimately show "?thesis" by(simp add: replicate_merge_anywhere) qed lemma restore_orgin_paras: "\\nl. nl = 0 \ length xs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) - length xs) @ 0 \ length gs @ xs @ anything\ mv_boxes (Suc (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) 0 (length xs) \\nl. nl = xs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs) @ anything\" proof - let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" thm mv_boxes_correct2 have "\\ nl. nl = [] @ 0\(length xs) @ (rec_exec (Cn (length xs) f gs) xs # 0 \ (?ft - length xs) @ 0 \ length gs) @ xs @ anything\ mv_boxes (Suc ?ft + length gs) 0 (length xs) \\ nl. nl = [] @ xs @ (rec_exec (Cn (length xs) f gs) xs # 0 \ (?ft - length xs) @ 0 \ length gs) @ 0\length xs @ anything\" by(rule_tac mv_boxes_correct2, auto) thus "?thesis" by(simp add: replicate_merge_anywhere) qed lemma compile_cn_correct': assumes f_ind: "\ anything r. rec_exec f (map (\g. rec_exec g xs) gs) = rec_exec (Cn (length xs) f gs) xs \ \\nl. nl = map (\g. rec_exec g xs) gs @ 0 \ (ffp - far) @ anything\ fap \\nl. nl = map (\g. rec_exec g xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (ffp - Suc far) @ anything\" and compile: "rec_ci f = (fap, far, ffp)" and term_f: "terminate f (map (\g. rec_exec g xs) gs)" and g_cond: "\g\set gs. terminate g xs \ (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. \\nl. nl = xs @ 0 \ (xb - xa) @ xc\ x \\nl. nl = xs @ rec_exec g xs # 0 \ (xb - Suc xa) @ xc\))" shows "\\nl. nl = xs @ 0 # 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs) @ anything\ cn_merge_gs (map rec_ci gs) (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))) [+] (mv_boxes 0 (Suc (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) (length xs) [+] (mv_boxes (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))) 0 (length gs) [+] (fap [+] (mv_box far (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))) [+] (empty_boxes (length gs) [+] (mv_box (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))) (length xs) [+] mv_boxes (Suc (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) 0 (length xs))))))) \\nl. nl = xs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs))) + length gs) @ anything\" proof - let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\(aprog, p, n). n) ` rec_ci ` set gs)))" let ?A = "cn_merge_gs (map rec_ci gs) ?ft" let ?B = "mv_boxes 0 (Suc (?ft+length gs)) (length xs)" let ?C = "mv_boxes ?ft 0 (length gs)" let ?D = fap let ?E = "mv_box far ?ft" let ?F = "empty_boxes (length gs)" let ?G = "mv_box ?ft (length xs)" let ?H = "mv_boxes (Suc (?ft + length gs)) 0 (length xs)" let ?P1 = "\nl. nl = xs @ 0 # 0 \ (?ft + length gs) @ anything" let ?S = "\nl. nl = xs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (?ft + length gs) @ anything" let ?Q1 = "\ nl. nl = xs @ 0\(?ft - length xs) @ map (\ i. rec_exec i xs) gs @ 0\(Suc (length xs)) @ anything" show "\?P1\ (?A [+] (?B [+] (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H))))))) \?S\" proof(rule_tac abc_Hoare_plus_halt) show "\?P1\ ?A \?Q1\" using g_cond by(rule_tac compile_cn_gs_correct, auto) next let ?Q2 = "\nl. nl = 0 \ ?ft @ map (\i. rec_exec i xs) gs @ 0 # xs @ anything" show "\?Q1\ (?B [+] (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H)))))) \?S\" proof(rule_tac abc_Hoare_plus_halt) show "\?Q1\ ?B \?Q2\" by(rule_tac save_paras) next let ?Q3 = "\ nl. nl = map (\i. rec_exec i xs) gs @ 0\?ft @ 0 # xs @ anything" show "\?Q2\ (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H))))) \?S\" proof(rule_tac abc_Hoare_plus_halt) have "ffp \ length gs" using compile term_f apply(subgoal_tac "length gs = far") apply(drule_tac footprint_ge, simp) by(drule_tac param_pattern, auto) thus "\?Q2\ ?C \?Q3\" by(erule_tac restore_new_paras) next let ?Q4 = "\ nl. nl = map (\i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0\?ft @ xs @ anything" have a: "far = length gs" using compile term_f by(drule_tac param_pattern, auto) have b:"?ft \ ffp" by auto have c: "ffp > far" using compile by(erule_tac footprint_ge) show "\?Q3\ (?D [+] (?E [+] (?F [+] (?G [+] ?H)))) \?S\" proof(rule_tac abc_Hoare_plus_halt) have "\\nl. nl = map (\g. rec_exec g xs) gs @ 0 \ (ffp - far) @ 0\(?ft - ffp + far) @ 0 # xs @ anything\ fap \\nl. nl = map (\g. rec_exec g xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \ (ffp - Suc far) @ 0\(?ft - ffp + far) @ 0 # xs @ anything\" by(rule_tac f_ind, simp add: rec_exec.simps) thus "\?Q3\ fap \?Q4\" using a b c by(simp add: replicate_merge_anywhere, cases "?ft", simp_all add: exp_suc del: replicate_Suc) next let ?Q5 = "\nl. nl = map (\i. rec_exec i xs) gs @ 0\(?ft - length gs) @ rec_exec (Cn (length xs) f gs) xs # 0\(length gs)@ xs @ anything" show "\?Q4\ (?E [+] (?F [+] (?G [+] ?H))) \?S\" proof(rule_tac abc_Hoare_plus_halt) from a b c show "\?Q4\ ?E \?Q5\" by(erule_tac save_rs, simp_all) next let ?Q6 = "\nl. nl = 0\?ft @ rec_exec (Cn (length xs) f gs) xs # 0\(length gs)@ xs @ anything" show "\?Q5\ (?F [+] (?G [+] ?H)) \?S\" proof(rule_tac abc_Hoare_plus_halt) have "length gs \ ffp" using a b c by simp thus "\?Q5\ ?F \?Q6\" by(erule_tac clean_paras) next let ?Q7 = "\nl. nl = 0\length xs @ rec_exec (Cn (length xs) f gs) xs # 0\(?ft - (length xs)) @ 0\(length gs)@ xs @ anything" show "\?Q6\ (?G [+] ?H) \?S\" proof(rule_tac abc_Hoare_plus_halt) show "\?Q6\ ?G \?Q7\" by(rule_tac restore_rs) next show "\?Q7\ ?H \?S\" by(rule_tac restore_orgin_paras) qed qed qed qed qed qed qed qed lemma compile_cn_correct: assumes termi_f: "terminate f (map (\g. rec_exec g xs) gs)" and f_ind: "\ap arity fp anything. rec_ci f = (ap, arity, fp) \ \\nl. nl = map (\g. rec_exec g xs) gs @ 0 \ (fp - arity) @ anything\ ap \\nl. nl = map (\g. rec_exec g xs) gs @ rec_exec f (map (\g. rec_exec g xs) gs) # 0 \ (fp - Suc arity) @ anything\" and g_cond: "\g\set gs. terminate g xs \ (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. \\nl. nl = xs @ 0 \ (xb - xa) @ xc\ x \\nl. nl = xs @ rec_exec g xs # 0 \ (xb - Suc xa) @ xc\))" and compile: "rec_ci (Cn n f gs) = (ap, arity, fp)" and len: "length xs = n" shows "\\nl. nl = xs @ 0 \ (fp - arity) @ anything\ ap \\nl. nl = xs @ rec_exec (Cn n f gs) xs # 0 \ (fp - Suc arity) @ anything\" proof(cases "rec_ci f") fix fap far ffp assume h: "rec_ci f = (fap, far, ffp)" then have f_newind: "\ anything .\\nl. nl = map (\g. rec_exec g xs) gs @ 0 \ (ffp - far) @ anything\ fap \\nl. nl = map (\g. rec_exec g xs) gs @ rec_exec f (map (\g. rec_exec g xs) gs) # 0 \ (ffp - Suc far) @ anything\" by(rule_tac f_ind, simp_all) thus "\\nl. nl = xs @ 0 \ (fp - arity) @ anything\ ap \\nl. nl = xs @ rec_exec (Cn n f gs) xs # 0 \ (fp - Suc arity) @ anything\" using compile len h termi_f g_cond apply(auto simp: rec_ci.simps abc_comp_commute) apply(rule_tac compile_cn_correct', simp_all) done qed subsubsection \Correctness of compilation for constructor Pr\ lemma mv_box_correct_simp[simp]: "\length xs = n; ft = max (n+3) (max fft gft)\ \ \\nl. nl = xs @ 0 # 0 \ (ft - n) @ anything\ mv_box n ft \\nl. nl = xs @ 0 # 0 \ (ft - n) @ anything\" using mv_box_correct[of n ft "xs @ 0 # 0 \ (ft - n) @ anything"] by(auto) lemma length_under_max[simp]: "length xs < max (length xs + 3) fft" by auto lemma save_init_rs: "\length xs = n; ft = max (n+3) (max fft gft)\ \ \\nl. nl = xs @ rec_exec f xs # 0 \ (ft - n) @ anything\ mv_box n (Suc n) \\nl. nl = xs @ 0 # rec_exec f xs # 0 \ (ft - Suc n) @ anything\" using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \ (ft - n) @ anything"] apply(auto simp: list_update_append list_update.simps nth_append split: if_splits) apply(cases "(max (length xs + 3) (max fft gft))", simp_all add: list_update.simps Suc_diff_le) done lemma less_then_max_plus2[simp]: "n + (2::nat) < max (n + 3) x" by auto lemma less_then_max_plus3[simp]: "n < max (n + (3::nat)) x" by auto lemma mv_box_max_plus_3_correct[simp]: "length xs = n \ \\nl. nl = xs @ x # 0 \ (max (n + (3::nat)) (max fft gft) - n) @ anything\ mv_box n (max (n + 3) (max fft gft)) \\nl. nl = xs @ 0 \ (max (n + 3) (max fft gft) - n) @ x # anything\" proof - assume h: "length xs = n" let ?ft = "max (n+3) (max fft gft)" let ?lm = "xs @ x # 0\(?ft - Suc n) @ 0 # anything" have g: "?ft > n + 2" by simp thm mv_box_correct have a: "\\ nl. nl = ?lm\ mv_box n ?ft \\ nl. nl = ?lm[?ft := ?lm!n + ?lm!?ft, n := 0]\" using h by(rule_tac mv_box_correct, auto) have b:"?lm = xs @ x # 0 \ (max (n + 3) (max fft gft) - n) @ anything" by(cases ?ft, simp_all add: Suc_diff_le exp_suc del: replicate_Suc) have c: "?lm[?ft := ?lm!n + ?lm!?ft, n := 0] = xs @ 0 \ (max (n + 3) (max fft gft) - n) @ x # anything" using h g apply(auto simp: nth_append list_update_append split: if_splits) using list_update_append[of "x # 0 \ (max (length xs + 3) (max fft gft) - Suc (length xs))" "0 # anything" "max (length xs + 3) (max fft gft) - length xs" "x"] apply(auto simp: if_splits) apply(simp add: list_update.simps replicate_Suc[THEN sym] del: replicate_Suc) done from a c show "?thesis" using h apply(simp) using b by simp qed lemma max_less_suc_suc[simp]: "max n (Suc n) < Suc (Suc (max (n + 3) x + anything - Suc 0))" by arith lemma suc_less_plus_3[simp]: "Suc n < max (n + 3) x" by arith lemma mv_box_ok_suc_simp[simp]: "length xs = n \ \\nl. nl = xs @ rec_exec f xs # 0 \ (max (n + 3) (max fft gft) - Suc n) @ x # anything\ mv_box n (Suc n) \\nl. nl = xs @ 0 # rec_exec f xs # 0 \ (max (n + 3) (max fft gft) - Suc (Suc n)) @ x # anything\" using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \ (max (n + 3) (max fft gft) - Suc n) @ x # anything"] apply(simp add: nth_append list_update_append list_update.simps) apply(cases "max (n + 3) (max fft gft)", simp_all) apply(cases "max (n + 3) (max fft gft) - 1", simp_all add: Suc_diff_le list_update.simps(2)) done lemma abc_append_first_steps_eq_pre: assumes notfinal: "abc_notfinal (abc_steps_l (0, lm) A n) A" and notnull: "A \ []" shows "abc_steps_l (0, lm) (A @ B) n = abc_steps_l (0, lm) A n" using notfinal proof(induct n) case 0 thus "?case" by(simp add: abc_steps_l.simps) next case (Suc n) have ind: "abc_notfinal (abc_steps_l (0, lm) A n) A \ abc_steps_l (0, lm) (A @ B) n = abc_steps_l (0, lm) A n" by fact have h: "abc_notfinal (abc_steps_l (0, lm) A (Suc n)) A" by fact then have a: "abc_notfinal (abc_steps_l (0, lm) A n) A" by(simp add: notfinal_Suc) then have b: "abc_steps_l (0, lm) (A @ B) n = abc_steps_l (0, lm) A n" using ind by simp obtain s lm' where c: "abc_steps_l (0, lm) A n = (s, lm')" by (metis prod.exhaust) then have d: "s < length A \ abc_steps_l (0, lm) (A @ B) n = (s, lm')" using a b by simp thus "?case" using c by(simp add: abc_step_red2 abc_fetch.simps abc_step_l.simps nth_append) qed lemma abc_append_first_step_eq_pre: "st < length A \ abc_step_l (st, lm) (abc_fetch st (A @ B)) = abc_step_l (st, lm) (abc_fetch st A)" by(simp add: abc_step_l.simps abc_fetch.simps nth_append) lemma abc_append_first_steps_halt_eq': assumes final: "abc_steps_l (0, lm) A n = (length A, lm')" and notnull: "A \ []" shows "\ n'. abc_steps_l (0, lm) (A @ B) n' = (length A, lm')" proof - have "\ n'. abc_notfinal (abc_steps_l (0, lm) A n') A \ abc_final (abc_steps_l (0, lm) A (Suc n')) A" using assms by(rule_tac n = n in abc_before_final, simp_all) then obtain na where a: "abc_notfinal (abc_steps_l (0, lm) A na) A \ abc_final (abc_steps_l (0, lm) A (Suc na)) A" .. obtain sa lma where b: "abc_steps_l (0, lm) A na = (sa, lma)" by (metis prod.exhaust) then have c: "abc_steps_l (0, lm) (A @ B) na = (sa, lma)" using a abc_append_first_steps_eq_pre[of lm A na B] assms by simp have d: "sa < length A" using b a by simp then have e: "abc_step_l (sa, lma) (abc_fetch sa (A @ B)) = abc_step_l (sa, lma) (abc_fetch sa A)" by(rule_tac abc_append_first_step_eq_pre) from a have "abc_steps_l (0, lm) A (Suc na) = (length A, lm')" using final equal_when_halt by(cases "abc_steps_l (0, lm) A (Suc na)" , simp) then have "abc_steps_l (0, lm) (A @ B) (Suc na) = (length A, lm')" using a b c e by(simp add: abc_step_red2) thus "?thesis" by blast qed lemma abc_append_first_steps_halt_eq: assumes final: "abc_steps_l (0, lm) A n = (length A, lm')" shows "\ n'. abc_steps_l (0, lm) (A @ B) n' = (length A, lm')" using final apply(cases "A = []") apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps abc_exec_null) apply(rule_tac abc_append_first_steps_halt_eq', simp_all) done lemma suc_suc_max_simp[simp]: "Suc (Suc (max (xs + 3) fft - Suc (Suc ( xs)))) = max ( xs + 3) fft - ( xs)" by arith lemma contract_dec_ft_length_plus_7[simp]: "\ft = max (n + 3) (max fft gft); length xs = n\ \ \\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything\ [Dec ft (length gap + 7)] \\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything\" apply (simp add: abc_Hoare_halt_def) apply (rule_tac x = 1 in exI) apply (auto simp add: max_def) apply(auto simp: abc_steps_l.simps abc_step_l.simps abc_fetch.simps nth_append abc_lm_v.simps abc_lm_s.simps list_update_append) using list_update_length [of "(x - Suc y) # rec_exec (Pr (length xs) f g) (xs @ [x - Suc y]) # 0 \ (max (length xs + 3) (max fft gft) - Suc (Suc (length xs)))" "Suc y" anything y] apply (auto simp add: Suc_diff_Suc) using numeral_3_eq_3 apply presburger using numeral_3_eq_3 apply presburger done lemma adjust_paras': "length xs = n \ \\nl. nl = xs @ x # y # anything\ [Inc n] [+] [Dec (Suc n) 2, Goto 0] \\nl. nl = xs @ Suc x # 0 # anything\" proof(rule_tac abc_Hoare_plus_halt) assume "length xs = n" thus "\\nl. nl = xs @ x # y # anything\ [Inc n] \\ nl. nl = xs @ Suc x # y # anything\" apply(simp add: abc_Hoare_halt_def) apply(rule_tac x = 1 in exI, force simp add: abc_steps_l.simps abc_step_l.simps abc_fetch.simps abc_comp.simps abc_lm_v.simps abc_lm_s.simps nth_append list_update_append list_update.simps(2)) done next assume h: "length xs = n" thus "\\nl. nl = xs @ Suc x # y # anything\ [Dec (Suc n) 2, Goto 0] \\nl. nl = xs @ Suc x # 0 # anything\" proof(induct y) case 0 thus "?case" apply(simp add: abc_Hoare_halt_def) apply(rule_tac x = 1 in exI, simp add: abc_steps_l.simps abc_step_l.simps abc_fetch.simps abc_comp.simps abc_lm_v.simps abc_lm_s.simps nth_append list_update_append list_update.simps(2)) done next case (Suc y) have "length xs = n \ \\nl. nl = xs @ Suc x # y # anything\ [Dec (Suc n) 2, Goto 0] \\nl. nl = xs @ Suc x # 0 # anything\" by fact then obtain stp where "abc_steps_l (0, xs @ Suc x # y # anything) [Dec (Suc n) 2, Goto 0] stp = (2, xs @ Suc x # 0 # anything)" using h apply(auto simp: abc_Hoare_halt_def numeral_2_eq_2) by (metis (mono_tags, lifting) abc_final.simps abc_holds_for.elims(2) length_Cons list.size(3)) moreover have "abc_steps_l (0, xs @ Suc x # Suc y # anything) [Dec (Suc n) 2, Goto 0] 2 = (0, xs @ Suc x # y # anything)" using h by(simp add: abc_steps_l.simps numeral_2_eq_2 abc_step_l.simps abc_fetch.simps abc_lm_v.simps abc_lm_s.simps nth_append list_update_append list_update.simps(2)) ultimately show "?case" apply(simp add: abc_Hoare_halt_def) by(rule exI[of _ "2 + stp"], simp only: abc_steps_add, simp) qed qed lemma adjust_paras: "length xs = n \ \\nl. nl = xs @ x # y # anything\ [Inc n, Dec (Suc n) 3, Goto (Suc 0)] \\nl. nl = xs @ Suc x # 0 # anything\" using adjust_paras'[of xs n x y anything] by(simp add: abc_comp.simps abc_shift.simps numeral_2_eq_2 numeral_3_eq_3) lemma rec_ci_SucSuc_n[simp]: "\rec_ci g = (gap, gar, gft); \yx\ \ gar = Suc (Suc n)" by(auto dest:param_pattern elim!:allE[of _ y]) lemma loop_back': assumes h: "length A = length gap + 4" "length xs = n" and le: "y \ x" shows "\ stp. abc_steps_l (length A, xs @ m # (y - x) # x # anything) (A @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]) stp = (length A, xs @ m # y # 0 # anything)" using le proof(induct x) case 0 thus "?case" using h by(rule_tac x = 0 in exI, auto simp: abc_steps_l.simps abc_step_l.simps abc_fetch.simps nth_append abc_lm_s.simps abc_lm_v.simps) next case (Suc x) have "x \ y \ \stp. abc_steps_l (length A, xs @ m # (y - x) # x # anything) (A @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]) stp = (length A, xs @ m # y # 0 # anything)" by fact moreover have "Suc x \ y" by fact moreover then have "\ stp. abc_steps_l (length A, xs @ m # (y - Suc x) # Suc x # anything) (A @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]) stp = (length A, xs @ m # (y - x) # x # anything)" using h apply(rule_tac x = 3 in exI) by(simp add: abc_steps_l.simps numeral_3_eq_3 abc_step_l.simps abc_fetch.simps nth_append abc_lm_v.simps abc_lm_s.simps list_update_append list_update.simps(2)) ultimately show "?case" apply(auto simp add: abc_steps_add) by (metis abc_steps_add) qed lemma loop_back: assumes h: "length A = length gap + 4" "length xs = n" shows "\ stp. abc_steps_l (length A, xs @ m # 0 # x # anything) (A @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]) stp = (0, xs @ m # x # 0 # anything)" using loop_back'[of A gap xs n x x m anything] assms apply(auto) apply(rename_tac stp) apply(rule_tac x = "stp + 1" in exI) apply(simp only: abc_steps_add, simp) apply(simp add: abc_steps_l.simps abc_step_l.simps abc_fetch.simps nth_append abc_lm_v.simps abc_lm_s.simps) done lemma rec_exec_pr_0_simps: "rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs" by(simp add: rec_exec.simps) lemma rec_exec_pr_Suc_simps: "rec_exec (Pr n f g) (xs @ [Suc y]) = rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])" apply(induct y) apply(simp add: rec_exec.simps) apply(simp add: rec_exec.simps) done lemma suc_max_simp[simp]: "Suc (max (n + 3) fft - Suc (Suc (Suc n))) = max (n + 3) fft - Suc (Suc n)" by arith lemma pr_loop: assumes code: "code = ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]" and len: "length xs = n" and g_ind: "\ yanything. \\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything\ gap \\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything\)" and compile_g: "rec_ci g = (gap, gar, gft)" and termi_g: "\ y x" shows "\stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) code stp = (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (ft - Suc (Suc n)) @ y # anything)" proof - let ?A = "[Dec ft (length gap + 7)]" let ?B = "gap" let ?C = "[Inc n, Dec (Suc n) 3, Goto (Suc 0)]" let ?D = "[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]" have "\ stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) ((?A [+] (?B [+] ?C)) @ ?D) stp = (length (?A [+] (?B [+] ?C)), xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything)" proof - have "\ stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) ((?A [+] (?B [+] ?C))) stp = (length (?A [+] (?B [+] ?C)), xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything)" proof - have "\\ nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything\ (?A [+] (?B [+] ?C)) \\ nl. nl = xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything\" proof(rule_tac abc_Hoare_plus_halt) show "\\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything\ [Dec ft (length gap + 7)] \\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything\" using ft len by(simp) next show "\\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything\ ?B [+] ?C \\nl. nl = xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything\" proof(rule_tac abc_Hoare_plus_halt) have a: "gar = Suc (Suc n)" using compile_g termi_g len less by simp have b: "gft > gar" using compile_g by(erule_tac footprint_ge) show "\\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ y # anything\ gap \\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything\" proof - have "\\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (gft - gar) @ 0\(ft - gft) @ y # anything\ gap \\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # rec_exec g (xs @ [(x - Suc y), rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (gft - Suc gar) @ 0\(ft - gft) @ y # anything\" using g_ind less by simp thus "?thesis" using a b ft by(simp add: replicate_merge_anywhere numeral_3_eq_3) qed next show "\\nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything\ [Inc n, Dec (Suc n) 3, Goto (Suc 0)] \\nl. nl = xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything\" using len less using adjust_paras[of xs n "x - Suc y" " rec_exec (Pr n f g) (xs @ [x - Suc y])" " rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything"] by(simp add: Suc_diff_Suc) qed qed thus "?thesis" apply(simp add: abc_Hoare_halt_def, auto) apply(rename_tac na) apply(rule_tac x = na in exI, case_tac "abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) ([Dec ft (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) na", simp) done qed then obtain stpa where "abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (ft - Suc (Suc n)) @ Suc y # anything) ((?A [+] (?B [+] ?C))) stpa = (length (?A [+] (?B [+] ?C)), xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything)" .. thus "?thesis" by(erule_tac abc_append_first_steps_halt_eq) qed moreover have "\ stp. abc_steps_l (length (?A [+] (?B [+] ?C)), xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything) ((?A [+] (?B [+] ?C)) @ ?D) stp = (0, xs @ (x - y) # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 # 0 \ (ft - Suc (Suc (Suc n))) @ y # anything)" using len by(rule_tac loop_back, simp_all) moreover have "rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) = rec_exec (Pr n f g) (xs @ [x - y])" using less apply(cases "x - y", simp_all add: rec_exec_pr_Suc_simps) apply(rename_tac nat) by(subgoal_tac "nat = x - Suc y", simp, arith) ultimately show "?thesis" using code ft apply (auto simp add: abc_steps_add replicate_Suc_iff_anywhere) apply(rename_tac stp stpa) apply(rule_tac x = "stp + stpa" in exI) by (simp add: abc_steps_add replicate_Suc_iff_anywhere del: replicate_Suc) qed lemma abc_lm_s_simp0[simp]: "length xs = n \ abc_lm_s (xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc (Suc n)) @ 0 # anything) (max (n + 3) (max fft gft)) 0 = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc n) @ anything" apply(simp add: abc_lm_s.simps) using list_update_length[of "xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc (Suc n))" 0 anything 0] apply(auto simp: Suc_diff_Suc) apply(simp add: exp_suc[THEN sym] Suc_diff_Suc del: replicate_Suc) done lemma index_at_zero_elem[simp]: "(xs @ x # re # 0 \ (max (length xs + 3) (max fft gft) - Suc (Suc (length xs))) @ 0 # anything) ! max (length xs + 3) (max fft gft) = 0" using nth_append_length[of "xs @ x # re # 0 \ (max (length xs + 3) (max fft gft) - Suc (Suc (length xs)))" 0 anything] by(simp) lemma pr_loop_correct: assumes less: "y \ x" and len: "length xs = n" and compile_g: "rec_ci g = (gap, gar, gft)" and termi_g: "\ y yanything. \\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything\ gap \\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything\)" shows "\\nl. nl = xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (max (n + 3) (max fft gft) - Suc (Suc n)) @ y # anything\ ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)] \\nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc n) @ anything\" using less proof(induct y) case 0 thus "?case" using len apply(simp add: abc_Hoare_halt_def) apply(rule_tac x = 1 in exI) by(auto simp: abc_steps_l.simps abc_step_l.simps abc_fetch.simps nth_append abc_comp.simps abc_shift.simps, simp add: abc_lm_v.simps) next case (Suc y) let ?ft = "max (n + 3) (max fft gft)" let ?C = "[Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]" have ind: "y \ x \ \\nl. nl = xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything\ ?C \\nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (?ft - Suc n) @ anything\" by fact have less: "Suc y \ x" by fact have stp1: "\ stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (?ft - Suc (Suc n)) @ Suc y # anything) ?C stp = (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything)" using assms less by(rule_tac pr_loop, auto) then obtain stp1 where a: "abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \ (?ft - Suc (Suc n)) @ Suc y # anything) ?C stp1 = (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything)" .. moreover have "\ stp. abc_steps_l (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything) ?C stp = (length ?C, xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (?ft - Suc n) @ anything)" using ind less apply(auto simp: abc_Hoare_halt_def) apply(rename_tac na,case_tac "abc_steps_l (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything) ?C na", rule_tac x = na in exI) by simp then obtain stp2 where b: "abc_steps_l (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \ (?ft - Suc (Suc n)) @ y # anything) ?C stp2 = (length ?C, xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (?ft - Suc n) @ anything)" .. from a b show "?case" apply(simp add: abc_Hoare_halt_def) apply(rule_tac x = "stp1 + stp2" in exI, simp add: abc_steps_add). qed lemma compile_pr_correct': assumes termi_g: "\ y yanything. \\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything\ gap \\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything\)" and termi_f: "terminate f xs" and f_ind: "\ anything. \\nl. nl = xs @ 0 \ (fft - far) @ anything\ fap \\nl. nl = xs @ rec_exec f xs # 0 \ (fft - Suc far) @ anything\" and len: "length xs = n" and compile1: "rec_ci f = (fap, far, fft)" and compile2: "rec_ci g = (gap, gar, gft)" shows "\\nl. nl = xs @ x # 0 \ (max (n + 3) (max fft gft) - n) @ anything\ mv_box n (max (n + 3) (max fft gft)) [+] (fap [+] (mv_box n (Suc n) [+] ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]))) \\nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (max (n + 3) (max fft gft) - Suc n) @ anything\" proof - let ?ft = "max (n+3) (max fft gft)" let ?A = "mv_box n ?ft" let ?B = "fap" let ?C = "mv_box n (Suc n)" let ?D = "[Dec ?ft (length gap + 7)]" let ?E = "gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]" let ?F = "[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]" let ?P = "\nl. nl = xs @ x # 0 \ (?ft - n) @ anything" let ?S = "\nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (?ft - Suc n) @ anything" let ?Q1 = "\nl. nl = xs @ 0 \ (?ft - n) @ x # anything" show "\?P\ (?A [+] (?B [+] (?C [+] (?D [+] ?E @ ?F)))) \?S\" proof(rule_tac abc_Hoare_plus_halt) show "\?P\ ?A \?Q1\" using len by simp next let ?Q2 = "\nl. nl = xs @ rec_exec f xs # 0 \ (?ft - Suc n) @ x # anything" have a: "?ft \ fft" by arith have b: "far = n" using compile1 termi_f len by(drule_tac param_pattern, auto) have c: "fft > far" using compile1 by(simp add: footprint_ge) show "\?Q1\ (?B [+] (?C [+] (?D [+] ?E @ ?F))) \?S\" proof(rule_tac abc_Hoare_plus_halt) have "\\nl. nl = xs @ 0 \ (fft - far) @ 0\(?ft - fft) @ x # anything\ fap \\nl. nl = xs @ rec_exec f xs # 0 \ (fft - Suc far) @ 0\(?ft - fft) @ x # anything\" by(rule_tac f_ind) moreover have "fft - far + ?ft - fft = ?ft - far" using a b c by arith moreover have "fft - Suc n + ?ft - fft = ?ft - Suc n" using a b c by arith ultimately show "\?Q1\ ?B \?Q2\" using b by(simp add: replicate_merge_anywhere) next let ?Q3 = "\ nl. nl = xs @ 0 # rec_exec f xs # 0\(?ft - Suc (Suc n)) @ x # anything" show "\?Q2\ (?C [+] (?D [+] ?E @ ?F)) \?S\" proof(rule_tac abc_Hoare_plus_halt) show "\?Q2\ (?C) \?Q3\" using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \ (max (n + 3) (max fft gft) - Suc n) @ x # anything"] using len by(auto) next show "\?Q3\ (?D [+] ?E @ ?F) \?S\" using pr_loop_correct[of x x xs n g gap gar gft f fft anything] assms by(simp add: rec_exec_pr_0_simps) qed qed qed qed lemma compile_pr_correct: assumes g_ind: "\y (\x xa xb. rec_ci g = (x, xa, xb) \ (\xc. \\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \ (xb - xa) @ xc\ x \\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \ (xb - Suc xa) @ xc\))" and termi_f: "terminate f xs" and f_ind: "\ap arity fp anything. rec_ci f = (ap, arity, fp) \ \\nl. nl = xs @ 0 \ (fp - arity) @ anything\ ap \\nl. nl = xs @ rec_exec f xs # 0 \ (fp - Suc arity) @ anything\" and len: "length xs = n" and compile: "rec_ci (Pr n f g) = (ap, arity, fp)" shows "\\nl. nl = xs @ x # 0 \ (fp - arity) @ anything\ ap \\nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \ (fp - Suc arity) @ anything\" proof(cases "rec_ci f", cases "rec_ci g") fix fap far fft gap gar gft assume h: "rec_ci f = (fap, far, fft)" "rec_ci g = (gap, gar, gft)" have g: "\y (\anything. \\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything\ gap \\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything\))" using g_ind h by(auto) hence termi_g: "\ y yanything. \\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \ (gft - gar) @ anything\ gap \\nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \ (gft - Suc gar) @ anything\)" by auto have f_newind: "\ anything. \\nl. nl = xs @ 0 \ (fft - far) @ anything\ fap \\nl. nl = xs @ rec_exec f xs # 0 \ (fft - Suc far) @ anything\" using h by(rule_tac f_ind, simp) show "?thesis" using termi_f termi_g h compile apply(simp add: rec_ci.simps abc_comp_commute, auto) using g_newind f_newind len by(rule_tac compile_pr_correct', simp_all) qed subsubsection \Correctness of compilation for constructor Mn\ fun mn_ind_inv :: "nat \ nat list \ nat \ nat \ nat \ nat list \ nat list \ bool" where "mn_ind_inv (as, lm') ss x rsx suf_lm lm = (if as = ss then lm' = lm @ x # rsx # suf_lm else if as = ss + 1 then \y. (lm' = lm @ x # y # suf_lm) \ y \ rsx else if as = ss + 2 then \y. (lm' = lm @ x # y # suf_lm) \ y \ rsx else if as = ss + 3 then lm' = lm @ x # 0 # suf_lm else if as = ss + 4 then lm' = lm @ Suc x # 0 # suf_lm else if as = 0 then lm' = lm @ Suc x # 0 # suf_lm else False )" fun mn_stage1 :: "nat \ nat list \ nat \ nat \ nat" where "mn_stage1 (as, lm) ss n = (if as = 0 then 0 else if as = ss + 4 then 1 else if as = ss + 3 then 2 else if as = ss + 2 \ as = ss + 1 then 3 else if as = ss then 4 else 0 )" fun mn_stage2 :: "nat \ nat list \ nat \ nat \ nat" where "mn_stage2 (as, lm) ss n = (if as = ss + 1 \ as = ss + 2 then (lm ! (Suc n)) else 0)" fun mn_stage3 :: "nat \ nat list \ nat \ nat \ nat" where "mn_stage3 (as, lm) ss n = (if as = ss + 2 then 1 else 0)" fun mn_measure :: "((nat \ nat list) \ nat \ nat) \ (nat \ nat \ nat)" where "mn_measure ((as, lm), ss, n) = (mn_stage1 (as, lm) ss n, mn_stage2 (as, lm) ss n, mn_stage3 (as, lm) ss n)" definition mn_LE :: "(((nat \ nat list) \ nat \ nat) \ ((nat \ nat list) \ nat \ nat)) set" where "mn_LE \ (inv_image lex_triple mn_measure)" lemma wf_mn_le[intro]: "wf mn_LE" by(auto intro:wf_inv_image wf_lex_triple simp: mn_LE_def) declare mn_ind_inv.simps[simp del] lemma put_in_tape_small_enough0[simp]: "0 < rsx \ \y. (xs @ x # rsx # anything)[Suc (length xs) := rsx - Suc 0] = xs @ x # y # anything \ y \ rsx" apply(rule_tac x = "rsx - 1" in exI) apply(simp add: list_update_append list_update.simps) done lemma put_in_tape_small_enough1[simp]: "\y \ rsx; 0 < y\ \ \ya. (xs @ x # y # anything)[Suc (length xs) := y - Suc 0] = xs @ x # ya # anything \ ya \ rsx" apply(rule_tac x = "y - 1" in exI) apply(simp add: list_update_append list_update.simps) done lemma abc_comp_null[simp]: "(A [+] B = []) = (A = [] \ B = [])" by(auto simp: abc_comp.simps abc_shift.simps) lemma rec_ci_not_null[simp]: "(rec_ci f \ ([], a, b))" proof(cases f) case (Cn x41 x42 x43) then show ?thesis by(cases "rec_ci x42", auto simp: mv_box.simps rec_ci.simps rec_ci_id.simps) next case (Pr x51 x52 x53) then show ?thesis apply(cases "rec_ci x52", cases "rec_ci x53") by (auto simp: mv_box.simps rec_ci.simps rec_ci_id.simps) next case (Mn x61 x62) then show ?thesis by(cases "rec_ci x62") (auto simp: rec_ci.simps rec_ci_id.simps) qed (auto simp: rec_ci_z_def rec_ci_s_def rec_ci.simps addition.simps rec_ci_id.simps) lemma mn_correct: assumes compile: "rec_ci rf = (fap, far, fft)" and ge: "0 < rsx" and len: "length xs = arity" and B: "B = [Dec (Suc arity) (length fap + 5), Dec (Suc arity) (length fap + 3), Goto (Suc (length fap)), Inc arity, Goto 0]" and f: "f = (\ stp. (abc_steps_l (length fap, xs @ x # rsx # anything) (fap @ B) stp, (length fap), arity)) " and P: "P =(\ ((as, lm), ss, arity). as = 0)" and Q: "Q = (\ ((as, lm), ss, arity). mn_ind_inv (as, lm) (length fap) x rsx anything xs)" shows "\ stp. P (f stp) \ Q (f stp)" proof(rule_tac halt_lemma2) show "wf mn_LE" using wf_mn_le by simp next show "Q (f 0)" by(auto simp: Q f abc_steps_l.simps mn_ind_inv.simps) next have "fap \ []" using compile by auto thus "\ P (f 0)" by(auto simp: f P abc_steps_l.simps) next have "fap \ []" using compile by auto then have "\\ P (f stp); Q (f stp)\ \ Q (f (Suc stp)) \ (f (Suc stp), f stp) \ mn_LE" for stp using ge len apply(cases "(abc_steps_l (length fap, xs @ x # rsx # anything) (fap @ B) stp)") apply(simp add: abc_step_red2 B f P Q) apply(auto split:if_splits simp add:abc_steps_l.simps mn_ind_inv.simps abc_steps_zero B abc_fetch.simps nth_append) by(auto simp: mn_LE_def lex_triple_def lex_pair_def abc_step_l.simps abc_steps_l.simps mn_ind_inv.simps abc_lm_v.simps abc_lm_s.simps nth_append abc_fetch.simps split: if_splits) thus "\stp. \ P (f stp) \ Q (f stp) \ Q (f (Suc stp)) \ (f (Suc stp), f stp) \ mn_LE" by(auto) qed lemma abc_Hoare_haltE: "\\ nl. nl = lm1\ p \\ nl. nl = lm2\ \ \ stp. abc_steps_l (0, lm1) p stp = (length p, lm2)" by(auto simp:abc_Hoare_halt_def elim!: abc_holds_for.elims) lemma mn_loop: assumes B: "B = [Dec (Suc arity) (length fap + 5), Dec (Suc arity) (length fap + 3), Goto (Suc (length fap)), Inc arity, Goto 0]" and ft: "ft = max (Suc arity) fft" and len: "length xs = arity" and far: "far = Suc arity" and ind: " (\xc. (\\nl. nl = xs @ x # 0 \ (fft - far) @ xc\ fap \\nl. nl = xs @ x # rec_exec f (xs @ [x]) # 0 \ (fft - Suc far) @ xc\))" and exec_less: "rec_exec f (xs @ [x]) > 0" and compile: "rec_ci f = (fap, far, fft)" shows "\ stp > 0. abc_steps_l (0, xs @ x # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 \ (ft - Suc arity) @ anything)" proof - have "\ stp. abc_steps_l (0, xs @ x # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything)" proof - have "\ stp. abc_steps_l (0, xs @ x # 0 \ (ft - Suc arity) @ anything) fap stp = (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything)" proof - have "\\nl. nl = xs @ x # 0 \ (fft - far) @ 0\(ft - fft) @ anything\ fap \\nl. nl = xs @ x # rec_exec f (xs @ [x]) # 0 \ (fft - Suc far) @ 0\(ft - fft) @ anything\" using ind by simp moreover have "fft > far" using compile by(erule_tac footprint_ge) ultimately show "?thesis" using ft far apply(drule_tac abc_Hoare_haltE) by(simp add: replicate_merge_anywhere max_absorb2) qed then obtain stp where "abc_steps_l (0, xs @ x # 0 \ (ft - Suc arity) @ anything) fap stp = (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything)" .. thus "?thesis" by(erule_tac abc_append_first_steps_halt_eq) qed moreover have "\ stp > 0. abc_steps_l (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 # 0 \ (ft - Suc (Suc arity)) @ anything)" using mn_correct[of f fap far fft "rec_exec f (xs @ [x])" xs arity B "(\stp. (abc_steps_l (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \ (ft - Suc (Suc arity)) @ anything) (fap @ B) stp, length fap, arity))" x "0 \ (ft - Suc (Suc arity)) @ anything" "(\((as, lm), ss, arity). as = 0)" "(\((as, lm), ss, aritya). mn_ind_inv (as, lm) (length fap) x (rec_exec f (xs @ [x])) (0 \ (ft - Suc (Suc arity)) @ anything) xs) "] B compile exec_less len apply(subgoal_tac "fap \ []", auto) apply(rename_tac stp y) apply(rule_tac x = stp in exI, auto simp: mn_ind_inv.simps) by(case_tac "stp", simp_all add: abc_steps_l.simps) moreover have "fft > far" using compile by(erule_tac footprint_ge) ultimately show "?thesis" using ft far apply(auto) apply(rename_tac stp1 stp2) by(rule_tac x = "stp1 + stp2" in exI, simp add: abc_steps_add replicate_Suc[THEN sym] diff_Suc_Suc del: replicate_Suc) qed lemma mn_loop_correct': assumes B: "B = [Dec (Suc arity) (length fap + 5), Dec (Suc arity) (length fap + 3), Goto (Suc (length fap)), Inc arity, Goto 0]" and ft: "ft = max (Suc arity) fft" and len: "length xs = arity" and ind_all: "\i\x. (\xc. (\\nl. nl = xs @ i # 0 \ (fft - far) @ xc\ fap \\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (fft - Suc far) @ xc\))" and exec_ge: "\ i\x. rec_exec f (xs @ [i]) > 0" and compile: "rec_ci f = (fap, far, fft)" and far: "far = Suc arity" shows "\ stp > x. abc_steps_l (0, xs @ 0 # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 \ (ft - Suc arity) @ anything)" using ind_all exec_ge proof(induct x) case 0 thus "?case" using assms by(rule_tac mn_loop, simp_all) next case (Suc x) have ind': "\\i\x. \xc. \\nl. nl = xs @ i # 0 \ (fft - far) @ xc\ fap \\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (fft - Suc far) @ xc\; \i\x. 0 < rec_exec f (xs @ [i])\ \ \stp > x. abc_steps_l (0, xs @ 0 # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 \ (ft - Suc arity) @ anything)" by fact have exec_ge: "\i\Suc x. 0 < rec_exec f (xs @ [i])" by fact have ind_all: "\i\Suc x. \xc. \\nl. nl = xs @ i # 0 \ (fft - far) @ xc\ fap \\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (fft - Suc far) @ xc\" by fact have ind: "\stp > x. abc_steps_l (0, xs @ 0 # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 \ (ft - Suc arity) @ anything)" using ind' exec_ge ind_all by simp have stp: "\ stp > 0. abc_steps_l (0, xs @ Suc x # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ Suc (Suc x) # 0 \ (ft - Suc arity) @ anything)" using ind_all exec_ge B ft len far compile by(rule_tac mn_loop, simp_all) from ind stp show "?case" apply(auto simp add: abc_steps_add) apply(rename_tac stp1 stp2) by(rule_tac x = "stp1 + stp2" in exI, simp add: abc_steps_add) qed lemma mn_loop_correct: assumes B: "B = [Dec (Suc arity) (length fap + 5), Dec (Suc arity) (length fap + 3), Goto (Suc (length fap)), Inc arity, Goto 0]" and ft: "ft = max (Suc arity) fft" and len: "length xs = arity" and ind_all: "\i\x. (\xc. (\\nl. nl = xs @ i # 0 \ (fft - far) @ xc\ fap \\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (fft - Suc far) @ xc\))" and exec_ge: "\ i\x. rec_exec f (xs @ [i]) > 0" and compile: "rec_ci f = (fap, far, fft)" and far: "far = Suc arity" shows "\ stp. abc_steps_l (0, xs @ 0 # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 \ (ft - Suc arity) @ anything)" proof - have "\stp>x. abc_steps_l (0, xs @ 0 # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 \ (ft - Suc arity) @ anything)" using assms by(rule_tac mn_loop_correct', simp_all) thus "?thesis" by(auto) qed lemma compile_mn_correct': assumes B: "B = [Dec (Suc arity) (length fap + 5), Dec (Suc arity) (length fap + 3), Goto (Suc (length fap)), Inc arity, Goto 0]" and ft: "ft = max (Suc arity) fft" and len: "length xs = arity" and termi_f: "terminate f (xs @ [r])" and f_ind: "\anything. \\nl. nl = xs @ r # 0 \ (fft - far) @ anything\ fap \\nl. nl = xs @ r # 0 # 0 \ (fft - Suc far) @ anything\" and ind_all: "\i < r. (\xc. (\\nl. nl = xs @ i # 0 \ (fft - far) @ xc\ fap \\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (fft - Suc far) @ xc\))" and exec_less: "\ i 0" and exec: "rec_exec f (xs @ [r]) = 0" and compile: "rec_ci f = (fap, far, fft)" shows "\\nl. nl = xs @ 0 \ (max (Suc arity) fft - arity) @ anything\ fap @ B \\nl. nl = xs @ rec_exec (Mn arity f) xs # 0 \ (max (Suc arity) fft - Suc arity) @ anything\" proof - have a: "far = Suc arity" using len compile termi_f by(drule_tac param_pattern, auto) have b: "fft > far" using compile by(erule_tac footprint_ge) have "\ stp. abc_steps_l (0, xs @ 0 # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ r # 0 \ (ft - Suc arity) @ anything)" using assms a apply(cases r, rule_tac x = 0 in exI, simp add: abc_steps_l.simps, simp) by(rule_tac mn_loop_correct, auto) moreover have "\ stp. abc_steps_l (0, xs @ r # 0 \ (ft - Suc arity) @ anything) (fap @ B) stp = (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything)" proof - have "\ stp. abc_steps_l (0, xs @ r # 0 \ (ft - Suc arity) @ anything) fap stp = (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything)" proof - have "\\nl. nl = xs @ r # 0 \ (fft - far) @ 0\(ft - fft) @ anything\ fap \\nl. nl = xs @ r # rec_exec f (xs @ [r]) # 0 \ (fft - Suc far) @ 0\(ft - fft) @ anything\" using f_ind exec by simp thus "?thesis" using ft a b apply(drule_tac abc_Hoare_haltE) by(simp add: replicate_merge_anywhere max_absorb2) qed then obtain stp where "abc_steps_l (0, xs @ r # 0 \ (ft - Suc arity) @ anything) fap stp = (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything)" .. thus "?thesis" by(erule_tac abc_append_first_steps_halt_eq) qed moreover have "\ stp. abc_steps_l (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything) (fap @ B) stp = (length fap + 5, xs @ r # rec_exec f (xs @ [r]) # 0 \ (ft - Suc (Suc arity)) @ anything)" using ft a b len B exec apply(rule_tac x = 1 in exI, auto) by(auto simp: abc_steps_l.simps B abc_step_l.simps abc_fetch.simps nth_append max_absorb2 abc_lm_v.simps abc_lm_s.simps) moreover have "rec_exec (Mn (length xs) f) xs = r" using exec exec_less apply(auto simp: rec_exec.simps Least_def) thm the_equality apply(rule_tac the_equality, auto) apply(metis exec_less less_not_refl3 linorder_not_less) by (metis le_neq_implies_less less_not_refl3) ultimately show "?thesis" using ft a b len B exec apply(auto simp: abc_Hoare_halt_def) apply(rename_tac stp1 stp2 stp3) apply(rule_tac x = "stp1 + stp2 + stp3" in exI) by(simp add: abc_steps_add replicate_Suc_iff_anywhere max_absorb2 Suc_diff_Suc del: replicate_Suc) qed lemma compile_mn_correct: assumes len: "length xs = n" and termi_f: "terminate f (xs @ [r])" and f_ind: "\ap arity fp anything. rec_ci f = (ap, arity, fp) \ \\nl. nl = xs @ r # 0 \ (fp - arity) @ anything\ ap \\nl. nl = xs @ r # 0 # 0 \ (fp - Suc arity) @ anything\" and exec: "rec_exec f (xs @ [r]) = 0" and ind_all: "\i (\x xa xb. rec_ci f = (x, xa, xb) \ (\xc. \\nl. nl = xs @ i # 0 \ (xb - xa) @ xc\ x \\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (xb - Suc xa) @ xc\)) \ 0 < rec_exec f (xs @ [i])" and compile: "rec_ci (Mn n f) = (ap, arity, fp)" shows "\\nl. nl = xs @ 0 \ (fp - arity) @ anything\ ap \\nl. nl = xs @ rec_exec (Mn n f) xs # 0 \ (fp - Suc arity) @ anything\" proof(cases "rec_ci f") fix fap far fft assume h: "rec_ci f = (fap, far, fft)" hence f_newind: "\anything. \\nl. nl = xs @ r # 0 \ (fft - far) @ anything\ fap \\nl. nl = xs @ r # 0 # 0 \ (fft - Suc far) @ anything\" by(rule_tac f_ind, simp) have newind_all: "\i < r. (\xc. (\\nl. nl = xs @ i # 0 \ (fft - far) @ xc\ fap \\nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \ (fft - Suc far) @ xc\))" using ind_all h by(auto) have all_less: "\ i 0" using ind_all by auto show "?thesis" using h compile f_newind newind_all all_less len termi_f exec apply(auto simp: rec_ci.simps) by(rule_tac compile_mn_correct', auto) qed subsubsection \Correctness of entire compilation process rec\_ci\ lemma recursive_compile_correct: "\terminate recf args; rec_ci recf = (ap, arity, fp)\ \ \\ nl. nl = args @ 0\(fp - arity) @ anything\ ap \\ nl. nl = args@ rec_exec recf args # 0\(fp - Suc arity) @ anything\" apply(induct arbitrary: ap arity fp anything rule: terminate.induct) apply(simp_all add: compile_s_correct compile_z_correct compile_id_correct compile_cn_correct compile_pr_correct compile_mn_correct) done definition dummy_abc :: "nat \ abc_inst list" where "dummy_abc k = [Inc k, Dec k 0, Goto 3]" definition abc_list_crsp:: "nat list \ nat list \ bool" where "abc_list_crsp xs ys = (\ n. xs = ys @ 0\n \ ys = xs @ 0\n)" lemma abc_list_crsp_simp1[intro]: "abc_list_crsp (lm @ 0\m) lm" by(auto simp: abc_list_crsp_def) lemma abc_list_crsp_lm_v: "abc_list_crsp lma lmb \ abc_lm_v lma n = abc_lm_v lmb n" by(auto simp: abc_list_crsp_def abc_lm_v.simps nth_append) lemma abc_list_crsp_elim: "\abc_list_crsp lma lmb; \ n. lma = lmb @ 0\n \ lmb = lma @ 0\n \ P \ \ P" by(auto simp: abc_list_crsp_def) lemma abc_list_crsp_simp[simp]: "\abc_list_crsp lma lmb; m < length lma; m < length lmb\ \ abc_list_crsp (lma[m := n]) (lmb[m := n])" by(auto simp: abc_list_crsp_def list_update_append) lemma abc_list_crsp_simp2[simp]: "\abc_list_crsp lma lmb; m < length lma; \ m < length lmb\ \ abc_list_crsp (lma[m := n]) (lmb @ 0 \ (m - length lmb) @ [n])" apply(auto simp: abc_list_crsp_def list_update_append) apply(rename_tac N) apply(rule_tac x = "N + length lmb - Suc m" in exI) apply(rule_tac disjI1) apply(simp add: upd_conv_take_nth_drop min_absorb1) done lemma abc_list_crsp_simp3[simp]: "\abc_list_crsp lma lmb; \ m < length lma; m < length lmb\ \ abc_list_crsp (lma @ 0 \ (m - length lma) @ [n]) (lmb[m := n])" apply(auto simp: abc_list_crsp_def list_update_append) apply(rename_tac N) apply(rule_tac x = "N + length lma - Suc m" in exI) apply(rule_tac disjI2) apply(simp add: upd_conv_take_nth_drop min_absorb1) done lemma abc_list_crsp_simp4[simp]: "\abc_list_crsp lma lmb; \ m < length lma; \ m < length lmb\ \ abc_list_crsp (lma @ 0 \ (m - length lma) @ [n]) (lmb @ 0 \ (m - length lmb) @ [n])" by(auto simp: abc_list_crsp_def list_update_append replicate_merge_anywhere) lemma abc_list_crsp_lm_s: "abc_list_crsp lma lmb \ abc_list_crsp (abc_lm_s lma m n) (abc_lm_s lmb m n)" by(auto simp: abc_lm_s.simps) lemma abc_list_crsp_step: "\abc_list_crsp lma lmb; abc_step_l (aa, lma) i = (a, lma'); abc_step_l (aa, lmb) i = (a', lmb')\ \ a' = a \ abc_list_crsp lma' lmb'" apply(cases i, auto simp: abc_step_l.simps abc_list_crsp_lm_s abc_list_crsp_lm_v split: abc_inst.splits if_splits) done lemma abc_list_crsp_steps: "\abc_steps_l (0, lm @ 0\m) aprog stp = (a, lm'); aprog \ []\ \ \ lma. abc_steps_l (0, lm) aprog stp = (a, lma) \ abc_list_crsp lm' lma" proof(induct stp arbitrary: a lm') case (Suc stp) then show ?case using [[simproc del: defined_all]] apply(cases "abc_steps_l (0, lm @ 0\m) aprog stp", simp add: abc_step_red) proof - fix stp a lm' aa b assume ind: "\a lm'. aa = a \ b = lm' \ \lma. abc_steps_l (0, lm) aprog stp = (a, lma) \ abc_list_crsp lm' lma" and h: "abc_step_l (aa, b) (abc_fetch aa aprog) = (a, lm')" "abc_steps_l (0, lm @ 0\m) aprog stp = (aa, b)" "aprog \ []" have "\lma. abc_steps_l (0, lm) aprog stp = (aa, lma) \ abc_list_crsp b lma" apply(rule_tac ind, simp) done from this obtain lma where g2: "abc_steps_l (0, lm) aprog stp = (aa, lma) \ abc_list_crsp b lma" .. hence g3: "abc_steps_l (0, lm) aprog (Suc stp) = abc_step_l (aa, lma) (abc_fetch aa aprog)" apply(rule_tac abc_step_red, simp) done show "\lma. abc_steps_l (0, lm) aprog (Suc stp) = (a, lma) \ abc_list_crsp lm' lma" using g2 g3 h apply(auto) apply(cases "abc_step_l (aa, b) (abc_fetch aa aprog)", cases "abc_step_l (aa, lma) (abc_fetch aa aprog)", simp) apply(rule_tac abc_list_crsp_step, auto) done qed qed (force simp add: abc_steps_l.simps) lemma list_crsp_simp2: "abc_list_crsp (lm1 @ 0\n) lm2 \ abc_list_crsp lm1 lm2" proof(induct n) case 0 thus "?case" by(auto simp: abc_list_crsp_def) next case (Suc n) have ind: "abc_list_crsp (lm1 @ 0 \ n) lm2 \ abc_list_crsp lm1 lm2" by fact have h: "abc_list_crsp (lm1 @ 0 \ Suc n) lm2" by fact then have "abc_list_crsp (lm1 @ 0 \ n) lm2" apply(auto simp only: exp_suc abc_list_crsp_def ) apply (metis Suc_pred append_eq_append_conv append_eq_append_conv2 butlast_append butlast_snoc length_replicate list.distinct(1) neq0_conv replicate_Suc replicate_Suc_iff_anywhere replicate_app_Cons_same replicate_empty self_append_conv self_append_conv2) apply (auto,metis replicate_Suc) . thus "?case" using ind by auto qed lemma recursive_compile_correct_norm': "\rec_ci f = (ap, arity, ft); terminate f args\ \ \ stp rl. (abc_steps_l (0, args) ap stp) = (length ap, rl) \ abc_list_crsp (args @ [rec_exec f args]) rl" using recursive_compile_correct[of f args ap arity ft "[]"] apply(auto simp: abc_Hoare_halt_def) apply(rename_tac n) apply(rule_tac x = n in exI) apply(case_tac "abc_steps_l (0, args @ 0 \ (ft - arity)) ap n", auto) apply(drule_tac abc_list_crsp_steps, auto) apply(rule_tac list_crsp_simp2, auto) done lemma find_exponent_rec_exec[simp]: assumes a: "args @ [rec_exec f args] = lm @ 0 \ n" and b: "length args < length lm" shows "\m. lm = args @ rec_exec f args # 0 \ m" using assms apply(cases n, simp) apply(rule_tac x = 0 in exI, simp) apply(drule_tac length_equal, simp) done lemma find_exponent_complex[simp]: "\args @ [rec_exec f args] = lm @ 0 \ n; \ length args < length lm\ \ \m. (lm @ 0 \ (length args - length lm) @ [Suc 0])[length args := 0] = args @ rec_exec f args # 0 \ m" apply(cases n, simp_all add: exp_suc list_update_append list_update.simps del: replicate_Suc) apply(subgoal_tac "length args = Suc (length lm)", simp) apply(rule_tac x = "Suc (Suc 0)" in exI, simp) apply(drule_tac length_equal, simp, auto) done lemma compile_append_dummy_correct: assumes compile: "rec_ci f = (ap, ary, fp)" and termi: "terminate f args" shows "\\ nl. nl = args\ (ap [+] dummy_abc (length args)) \\ nl. (\ m. nl = args @ rec_exec f args # 0\m)\" proof(rule_tac abc_Hoare_plus_halt) show "\\nl. nl = args\ ap \\ nl. abc_list_crsp (args @ [rec_exec f args]) nl\" using compile termi recursive_compile_correct_norm'[of f ap ary fp args] apply(auto simp: abc_Hoare_halt_def) by (metis abc_final.simps abc_holds_for.simps) next show "\abc_list_crsp (args @ [rec_exec f args])\ dummy_abc (length args) \\nl. \m. nl = args @ rec_exec f args # 0 \ m\" apply(auto simp: dummy_abc_def abc_Hoare_halt_def) apply(rule_tac x = 3 in exI) by(force simp: abc_steps_l.simps abc_list_crsp_def abc_step_l.simps numeral_3_eq_3 abc_fetch.simps abc_lm_v.simps nth_append abc_lm_s.simps) qed lemma cn_merge_gs_split: "\i < length gs; rec_ci (gs!i) = (ga, gb, gc)\ \ cn_merge_gs (map rec_ci gs) p = cn_merge_gs (map rec_ci (take i gs)) p [+] (ga [+] mv_box gb (p + i)) [+] cn_merge_gs (map rec_ci (drop (Suc i) gs)) (p + Suc i)" proof(induct i arbitrary: gs p) case 0 then show ?case by(cases gs; simp) next case (Suc i) then show ?case by(cases gs, simp, cases "rec_ci (hd gs)", simp add: abc_comp_commute[THEN sym]) qed lemma cn_unhalt_case: assumes compile1: "rec_ci (Cn n f gs) = (ap, ar, ft) \ length args = ar" and g: "i < length gs" and compile2: "rec_ci (gs!i) = (gap, gar, gft) \ gar = length args" and g_unhalt: "\ anything. \\ nl. nl = args @ 0\(gft - gar) @ anything\ gap \" and g_ind: "\ apj arj ftj j anything. \j < i; rec_ci (gs!j) = (apj, arj, ftj)\ \ \\ nl. nl = args @ 0\(ftj - arj) @ anything\ apj \\ nl. nl = args @ rec_exec (gs!j) args # 0\(ftj - Suc arj) @ anything\" and all_termi: "\ j\ nl. nl = args @ 0\(ft - ar) @ anything\ ap \" using compile1 apply(cases "rec_ci f", auto simp: rec_ci.simps abc_comp_commute) proof(rule_tac abc_Hoare_plus_unhalt1) fix fap far fft let ?ft = "max (Suc (length args)) (Max (insert fft ((\(aprog, p, n). n) ` rec_ci ` set gs)))" let ?Q = "\nl. nl = args @ 0\ (?ft - length args) @ map (\i. rec_exec i args) (take i gs) @ 0\(length gs - i) @ 0\ Suc (length args) @ anything" have "cn_merge_gs (map rec_ci gs) ?ft = cn_merge_gs (map rec_ci (take i gs)) ?ft [+] (gap [+] mv_box gar (?ft + i)) [+] cn_merge_gs (map rec_ci (drop (Suc i) gs)) (?ft + Suc i)" using g compile2 cn_merge_gs_split by simp thus "\\nl. nl = args @ 0 # 0 \ (?ft + length gs) @ anything\ (cn_merge_gs (map rec_ci gs) ?ft) \" proof(simp, rule_tac abc_Hoare_plus_unhalt1, rule_tac abc_Hoare_plus_unhalt2, rule_tac abc_Hoare_plus_unhalt1) let ?Q_tmp = "\nl. nl = args @ 0\ (gft - gar) @ 0\(?ft - (length args) - (gft -gar)) @ map (\i. rec_exec i args) (take i gs) @ 0\(length gs - i) @ 0\ Suc (length args) @ anything" have a: "\?Q_tmp\ gap \" using g_unhalt[of "0 \ (?ft - (length args) - (gft - gar)) @ map (\i. rec_exec i args) (take i gs) @ 0 \ (length gs - i) @ 0 \ Suc (length args) @ anything"] by simp moreover have "?ft \ gft" using g compile2 apply(rule_tac max.coboundedI2, rule_tac Max_ge, simp, rule_tac insertI2) apply(rule_tac x = "rec_ci (gs ! i)" in image_eqI, simp) by(rule_tac x = "gs!i" in image_eqI, simp, simp) then have b:"?Q_tmp = ?Q" using compile2 apply(rule_tac arg_cong) by(simp add: replicate_merge_anywhere) thus "\?Q\ gap \" using a by simp next show "\\nl. nl = args @ 0 # 0 \ (?ft + length gs) @ anything\ cn_merge_gs (map rec_ci (take i gs)) ?ft \\nl. nl = args @ 0 \ (?ft - length args) @ map (\i. rec_exec i args) (take i gs) @ 0 \ (length gs - i) @ 0 \ Suc (length args) @ anything\" using all_termi by(rule_tac compile_cn_gs_correct', auto simp: set_conv_nth intro:g_ind) qed qed lemma mn_unhalt_case': assumes compile: "rec_ci f = (a, b, c)" and all_termi: "\i. terminate f (args @ [i]) \ 0 < rec_exec f (args @ [i])" and B: "B = [Dec (Suc (length args)) (length a + 5), Dec (Suc (length args)) (length a + 3), Goto (Suc (length a)), Inc (length args), Goto 0]" shows "\\nl. nl = args @ 0 \ (max (Suc (length args)) c - length args) @ anything\ a @ B \" proof(rule_tac abc_Hoare_unhaltI, auto) fix n have a: "b = Suc (length args)" using all_termi compile apply(erule_tac x = 0 in allE) by(auto, drule_tac param_pattern,auto) moreover have b: "c > b" using compile by(elim footprint_ge) ultimately have c: "max (Suc (length args)) c = c" by arith have "\ stp > n. abc_steps_l (0, args @ 0 # 0\(c - Suc (length args)) @ anything) (a @ B) stp = (0, args @ Suc n # 0\(c - Suc (length args)) @ anything)" using assms a b c proof(rule_tac mn_loop_correct', auto) fix i xc show "\\nl. nl = args @ i # 0 \ (c - Suc (length args)) @ xc\ a \\nl. nl = args @ i # rec_exec f (args @ [i]) # 0 \ (c - Suc (Suc (length args))) @ xc\" using all_termi recursive_compile_correct[of f "args @ [i]" a b c xc] compile a by(simp) qed then obtain stp where d: "stp > n \ abc_steps_l (0, args @ 0 # 0\(c - Suc (length args)) @ anything) (a @ B) stp = (0, args @ Suc n # 0\(c - Suc (length args)) @ anything)" .. then obtain d where e: "stp = n + Suc d" by (metis add_Suc_right less_iff_Suc_add) obtain s nl where f: "abc_steps_l (0, args @ 0 # 0\(c - Suc (length args)) @ anything) (a @ B) n = (s, nl)" by (metis prod.exhaust) have g: "s < length (a @ B)" using d e f apply(rule_tac classical, simp only: abc_steps_add) by(simp add: halt_steps2 leI) from f g show "abc_notfinal (abc_steps_l (0, args @ 0 \ (max (Suc (length args)) c - length args) @ anything) (a @ B) n) (a @ B)" using c b a by(simp add: replicate_Suc_iff_anywhere Suc_diff_Suc del: replicate_Suc) qed lemma mn_unhalt_case: assumes compile: "rec_ci (Mn n f) = (ap, ar, ft) \ length args = ar" and all_term: "\ i. terminate f (args @ [i]) \ rec_exec f (args @ [i]) > 0" shows "\ (\ nl. nl = args @ 0\(ft - ar) @ anything) \ ap \ " using assms apply(cases "rec_ci f", auto simp: rec_ci.simps abc_comp_commute) by(rule_tac mn_unhalt_case', simp_all) section \Compilers composed: Compiling Recursive Functions into Turing Machines\ fun tm_of_rec :: "recf \ instr list" where "tm_of_rec recf = (let (ap, k, fp) = rec_ci recf in let tp = tm_of (ap [+] dummy_abc k) in tp @ (shift (mopup_n_tm k) (length tp div 2)))" lemma recursive_compile_to_tm_correct1: assumes compile: "rec_ci recf = (ap, ary, fp)" and termi: " terminate recf args" and tp: "tp = tm_of (ap [+] dummy_abc (length args))" shows "\ stp m l. steps0 (Suc 0, Bk # Bk # ires, @ Bk\rn) (tp @ shift (mopup_n_tm (length args)) (length tp div 2)) stp = (0, Bk\m @ Bk # Bk # ires, Oc\Suc (rec_exec recf args) @ Bk\l)" proof - have "\\nl. nl = args\ ap [+] dummy_abc (length args) \\nl. \m. nl = args @ rec_exec recf args # 0 \ m\" using compile termi compile by(rule_tac compile_append_dummy_correct, auto) then obtain stp m where h: "abc_steps_l (0, args) (ap [+] dummy_abc (length args)) stp = (length (ap [+] dummy_abc (length args)), args @ rec_exec recf args # 0\m) " apply(simp add: abc_Hoare_halt_def, auto) apply(rename_tac n) by(case_tac "abc_steps_l (0, args) (ap [+] dummy_abc (length args)) n", auto) thus "?thesis" using assms tp compile_correct_halt[OF refl refl _ h _ _ refl] by(auto simp: crsp.simps start_of.simps abc_lm_v.simps) qed lemma recursive_compile_to_tm_correct2: assumes termi: " terminate recf args" shows "\ stp m l. steps0 (Suc 0, [Bk, Bk], ) (tm_of_rec recf) stp = (0, Bk\Suc (Suc m), Oc\Suc (rec_exec recf args) @ Bk\l)" proof(cases "rec_ci recf", simp ) fix ap ar fp assume "rec_ci recf = (ap, ar, fp)" thus "\stp m l. steps0 (Suc 0, [Bk, Bk], ) (tm_of (ap [+] dummy_abc ar) @ shift (mopup_n_tm ar) (sum_list (layout_of (ap [+] dummy_abc ar)))) stp = (0, Bk # Bk # Bk \ m, Oc # Oc \ rec_exec recf args @ Bk \ l)" using recursive_compile_to_tm_correct1[of recf ap ar fp args "tm_of (ap [+] dummy_abc (length args))" "[]" 0] assms param_pattern[of recf args ap ar fp] by(simp add: replicate_Suc[THEN sym] replicate_Suc_iff_anywhere del: replicate_Suc, simp add: exp_suc del: replicate_Suc) qed lemma recursive_compile_to_tm_correct3: assumes termi: "terminate recf args" shows "\\ tp. tp =([Bk, Bk], )\ (tm_of_rec recf) \\ tp. \ k l. tp = (Bk\ k, @ Bk \ l)\" using recursive_compile_to_tm_correct2[OF assms] apply(auto simp add: Hoare_halt_def ) apply(rename_tac stp M l) apply(rule_tac x = stp in exI) apply(auto simp add: tape_of_nat_def) apply(rule_tac x = "Suc (Suc M)" in exI) apply(simp) done subsection \Appending the mopup TM\ lemma list_all_suc_many[simp]: "list_all (\(acn, s). s \ Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \ list_all (\(acn, s). s \ Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))))) xs" proof(induct xs) case (Cons a xs) then show ?case by(cases a, simp) qed simp lemma shift_append: "shift (xs @ ys) n = shift xs n @ shift ys n" apply(simp add: shift.simps) done lemma length_shift_mopup[simp]: "length (shift (mopup_n_tm n) ss) = 4 * n + 12" apply(auto simp: mopup_n_tm.simps shift_append mopup_b_def) done lemma length_tm_even[intro]: "length (tm_of ap) mod 2 = 0" apply(simp add: tm_of.simps) done lemma tms_of_at_index[simp]: "k < length ap \ tms_of ap ! k = ci (layout_of ap) (start_of (layout_of ap) k) (ap ! k)" apply(simp add: tms_of.simps tpairs_of.simps) done lemma start_of_suc_inc: "\k < length ap; ap ! k = Inc n\ \ start_of (layout_of ap) (Suc k) = start_of (layout_of ap) k + 2 * n + 9" apply(rule_tac start_of_Suc1, auto simp: abc_fetch.simps) done lemma start_of_suc_dec: "\k < length ap; ap ! k = (Dec n e)\ \ start_of (layout_of ap) (Suc k) = start_of (layout_of ap) k + 2 * n + 16" apply(rule_tac start_of_Suc2, auto simp: abc_fetch.simps) done lemma inc_state_all_le: "\k < length ap; ap ! k = Inc n; (a, b) \ set (shift (shift tinc_b (2 * n)) (start_of (layout_of ap) k - Suc 0))\ \ b \ start_of (layout_of ap) (length ap)" apply(subgoal_tac "b \ start_of (layout_of ap) (Suc k)") apply(subgoal_tac "start_of (layout_of ap) (Suc k) \ start_of (layout_of ap) (length ap) ") apply(arith) apply(cases "Suc k = length ap", simp) apply(rule_tac start_of_less, simp) apply(auto simp: tinc_b_def shift.simps start_of_suc_inc length_of.simps ) done lemma findnth_le[elim]: "(a, b) \ set (shift (findnth n) (start_of (layout_of ap) k - Suc 0)) \ b \ Suc (start_of (layout_of ap) k + 2 * n)" apply(induct n, force simp add: shift.simps) apply(simp add: shift_append, auto) apply(auto simp: shift.simps) done lemma findnth_state_all_le1: "\k < length ap; ap ! k = Inc n; (a, b) \ set (shift (findnth n) (start_of (layout_of ap) k - Suc 0))\ \ b \ start_of (layout_of ap) (length ap)" apply(subgoal_tac "b \ start_of (layout_of ap) (Suc k)") apply(subgoal_tac "start_of (layout_of ap) (Suc k) \ start_of (layout_of ap) (length ap) ") apply(arith) apply(cases "Suc k = length ap", simp) apply(rule_tac start_of_less, simp) apply(subgoal_tac "b \ start_of (layout_of ap) k + 2*n + 1 \ start_of (layout_of ap) k + 2*n + 1 \ start_of (layout_of ap) (Suc k)", auto) apply(auto simp: tinc_b_def shift.simps length_of.simps start_of_suc_inc) done lemma start_of_eq: "length ap < as \ start_of (layout_of ap) as = start_of (layout_of ap) (length ap)" proof(induct as) case (Suc as) then show ?case apply(cases "length ap < as", simp add: start_of.simps) apply(subgoal_tac "as = length ap") apply(simp add: start_of.simps) apply arith done qed simp lemma start_of_all_le: "start_of (layout_of ap) as \ start_of (layout_of ap) (length ap)" apply(subgoal_tac "as > length ap \ as = length ap \ as < length ap", auto simp: start_of_eq start_of_less) done lemma findnth_state_all_le2: "\k < length ap; ap ! k = Dec n e; (a, b) \ set (shift (findnth n) (start_of (layout_of ap) k - Suc 0))\ \ b \ start_of (layout_of ap) (length ap)" apply(subgoal_tac "b \ start_of (layout_of ap) k + 2*n + 1 \ start_of (layout_of ap) k + 2*n + 1 \ start_of (layout_of ap) (Suc k) \ start_of (layout_of ap) (Suc k) \ start_of (layout_of ap) (length ap)", auto) apply(subgoal_tac "start_of (layout_of ap) (Suc k) = start_of (layout_of ap) k + 2*n + 16", simp) apply(simp add: start_of_suc_dec) apply(rule_tac start_of_all_le) done lemma dec_state_all_le[simp]: "\k < length ap; ap ! k = Dec n e; (a, b) \ set (shift (shift tdec_b (2 * n)) (start_of (layout_of ap) k - Suc 0))\ \ b \ start_of (layout_of ap) (length ap)" apply(subgoal_tac "2*n + start_of (layout_of ap) k + 16 \ start_of (layout_of ap) (length ap) \ start_of (layout_of ap) k > 0") prefer 2 apply(subgoal_tac "start_of (layout_of ap) (Suc k) = start_of (layout_of ap) k + 2*n + 16 \ start_of (layout_of ap) (Suc k) \ start_of (layout_of ap) (length ap)") apply(simp, rule_tac conjI) apply(simp add: start_of_suc_dec) apply(rule_tac start_of_all_le) apply(auto simp: tdec_b_def shift.simps) done lemma tms_any_less: "\k < length ap; (a, b) \ set (tms_of ap ! k)\ \ b \ start_of (layout_of ap) (length ap)" apply(cases "ap!k", auto simp: tms_of.simps tpairs_of.simps ci.simps shift_append adjust.simps) apply(erule_tac findnth_state_all_le1, simp_all) apply(erule_tac inc_state_all_le, simp_all) apply(erule_tac findnth_state_all_le2, simp_all) apply(rule_tac start_of_all_le) apply(rule_tac start_of_all_le) done lemma concat_in: "i < length (concat xs) \ \k < length xs. concat xs ! i \ set (xs ! k)" proof(induct xs rule: rev_induct) case (snoc x xs) then show ?case apply(cases "i < length (concat xs)", simp) apply(erule_tac exE, rule_tac x = k in exI) apply(simp add: nth_append) apply(rule_tac x = "length xs" in exI, simp) apply(simp add: nth_append) done qed auto declare length_concat[simp] lemma in_tms: "i < length (tm_of ap) \ \ k < length ap. (tm_of ap ! i) \ set (tms_of ap ! k)" apply(simp only: tm_of.simps) using concat_in[of i "tms_of ap"] apply(auto) done lemma all_le_start_of: "list_all (\(acn, s). s \ start_of (layout_of ap) (length ap)) (tm_of ap)" apply(simp only: list_all_length) apply(rule_tac allI, rule_tac impI) apply(drule_tac in_tms, auto elim: tms_any_less) done lemma length_ci: "\k < length ap; length (ci ly y (ap ! k)) = 2 * qa\ \ layout_of ap ! k = qa" apply(cases "ap ! k") apply(auto simp: layout_of.simps ci.simps length_of.simps tinc_b_def tdec_b_def length_findnth adjust.simps) done lemma ci_even[intro]: "length (ci ly y i) mod 2 = 0" apply(cases i, auto simp: ci.simps length_findnth tinc_b_def adjust.simps tdec_b_def) done lemma sum_list_ci_even[intro]: "sum_list (map (length \ (\(x, y). ci ly x y)) zs) mod 2 = 0" proof(induct zs rule: rev_induct) case (snoc x xs) then show ?case apply(cases x, simp) apply(subgoal_tac "length (ci ly (fst x) (snd x)) mod 2 = 0") apply(auto) done qed (simp) lemma zip_pre: "(length ys) \ length ap \ zip ys ap = zip ys (take (length ys) (ap::'a list))" proof(induct ys arbitrary: ap) case (Cons a ys) from Cons(2) have z:"ap = aa # list \ zip (a # ys) ap = zip (a # ys) (take (length (a # ys)) ap)" for aa list using Cons(1)[of list] by simp thus ?case by (cases ap;simp) qed simp lemma length_start_of_tm: "start_of (layout_of ap) (length ap) = Suc (length (tm_of ap) div 2)" using tpa_states[of "tm_of ap" "length ap" ap] by(simp add: tm_of.simps) lemma list_all_add_6E[elim]: "list_all (\(acn, s). s \ Suc q) xs \ list_all (\(acn, s). s \ q + (2 * n + 6)) xs" by(auto simp: list_all_length) lemma mopup_b_12[simp]: "length mopup_b = 12" by(simp add: mopup_b_def) lemma mp_up_all_le: "list_all (\(acn, s). s \ q + (2 * n + 6)) [(R, Suc (Suc (2 * n + q))), (R, Suc (2 * n + q)), (L, 5 + 2 * n + q), (WB, Suc (Suc (Suc (2 * n + q)))), (R, 4 + 2 * n + q), (WB, Suc (Suc (Suc (2 * n + q)))), (R, Suc (Suc (2 * n + q))), (WB, Suc (Suc (Suc (2 * n + q)))), (L, 5 + 2 * n + q), (L, 6 + 2 * n + q), (R, 0), (L, 6 + 2 * n + q)]" by(auto) lemma mopup_le6[simp]: "(a, b) \ set (mopup_a n) \ b \ 2 * n + 6" by(induct n, auto ) lemma shift_le2[simp]: "(a, b) \ set (shift (mopup_n_tm n) x) \ b \ (2 * x + length (mopup_n_tm n)) div 2" apply(auto simp: mopup_n_tm.simps shift_append shift.simps) apply(auto simp: mopup_b_def) done lemma mopup_ge2[intro]: " 2 \ x + length (mopup_n_tm n)" apply(simp add: mopup_n_tm.simps) done lemma mopup_even[intro]: " (2 * x + length (mopup_n_tm n)) mod 2 = 0" by(auto simp: mopup_n_tm.simps) lemma mopup_div_2[simp]: "b \ Suc x \ b \ (2 * x + length (mopup_n_tm n)) div 2" by(auto simp: mopup_n_tm.simps) -subsection \A Turing Machine with mopup code appended is composable\ +subsection \A Turing Machine compiled from an Abacus program with mopup code appended is composable\ lemma composable_tm_from_abacus: assumes "tp = tm_of ap" shows "composable_tm0 (tp @ shift (mopup_n_tm n) (length tp div 2))" proof - have "is_even (length (mopup_n_tm n))" for n using composable_tm.simps by blast moreover have "(aa, ba) \ set (mopup_n_tm n) \ ba \ length (mopup_n_tm n) div 2" for aa ba by (metis (no_types, lifting) add_cancel_left_right case_prodD composable_tm.simps composable_mopup_n_tm) moreover have "(\x\set (tm_of ap). case x of (acn, s::nat) \ s \ Suc (sum_list (layout_of ap))) \ (a, b) \ set (tm_of ap) \ b \ sum_list (layout_of ap) + length (mopup_n_tm n) div 2" for a b and s::nat by (metis (no_types, lifting) add_Suc add_cancel_left_right case_prodD div_mult_mod_eq le_SucE mult_2_right not_numeral_le_zero composable_tm.simps trans_le_add1 composable_mopup_n_tm) ultimately show ?thesis unfolding assms using length_start_of_tm[of ap] all_le_start_of[of ap] composable_tm.simps by(auto simp: List.list_all_iff shift.simps) qed -subsection \A Turing Machine with mopup code appended is composable\ +subsection \A Turing Machine compiled from a recursive function is composable\ lemma composable_tm_from_recf: assumes compile: "tp = tm_of_rec recf" shows "composable_tm0 tp" proof - obtain a b c where "rec_ci recf = (a, b, c)" by (metis prod_cases3) thus "?thesis" using compile using composable_tm_from_abacus[of "tm_of (a [+] dummy_abc b)" "(a [+] dummy_abc b)" b] by simp qed end diff --git a/thys/Universal_Turing_Machine/document/root.tex b/thys/Universal_Turing_Machine/document/root.tex --- a/thys/Universal_Turing_Machine/document/root.tex +++ b/thys/Universal_Turing_Machine/document/root.tex @@ -1,124 +1,124 @@ \documentclass{report} %\documentclass[runningheads]{llncs} \usepackage{isabelle} \usepackage{isabellesym} \usepackage{times} \usepackage{amssymb} \usepackage{amsmath} \usepackage{stmaryrd} \usepackage{mathpartir} \usepackage{tikz} \usepackage{pgf} \usepackage{color} \usetikzlibrary{calc} \usetikzlibrary{positioning} %% for testing %\usepackage{endnotes} %\let\footnote=\endnote \def\inst#1{\unskip$^{#1}$} % urls in roman style, theory text in math-similar italics \isabellestyle{it} % this should be the last package used \usepackage{pdfsetup} % gray boxes \definecolor{mygrey}{rgb}{.80,.80,.80} % mathpatir \mprset{sep=0.9em} \mprset{center=false} \mprset{flushleft=true} % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} \renewcommand{\isasymequiv}{$\dn$} \renewcommand{\isasymemptyset}{$\varnothing$} \renewcommand{\isacharunderscore}{\mbox{$\_$}} \renewcommand{\isasymiota}{} \newcommand{\isasymulcorner}{$\ulcorner$} \newcommand{\isasymurcorner}{$\urcorner$} %\newcommand{\chapter}{\section} \setcounter{tocdepth}{3} \setcounter{secnumdepth}{3} \begin{document} \title{Universal Turing Machine and Computability Theory in Isabelle/HOL} \author{Jian Xu\inst{2} \and Xingyuan Zhang\inst{2} \and Christian Urban\inst{1} \and Sebastiaan J. C. Joosten\inst{3} \and Franz A. B. Regensburger\inst{4} \vspace{3pt} \\ \inst{1}King's College London, UK \\ \inst{2}PLA University of Science and Technology, China \\ \inst{3}University of Twente, the Netherlands \\ \inst{4}Technische Hochschule Ingolstadt, Germany} \maketitle \begin{abstract} We formalise results from computability theory: Turing decidability, Turing computability, reduction of decision problems, recursive functions, undecidability of the special and the general halting problem, and the existence of a universal Turing machine. This formalisation extends the original AFP entry of 2014 that corresponded to: Mechanising Turing Machines and Computability Theory in Isabelle/HOL, ITP 2013 \end{abstract} The AFP entry and by extension this document is largely written by Xu, Zhang and Urban. The Universal Turing Machine is explained in this document, starting at Figure~\ref{prepare_input}. You may want to also consult the original ITP article~\cite{Xu13}. If you are interested in results about Turing Machines and Computability theory: the main book used for this formalisation is by Boolos, Burgess and Jeffrey~\cite{Boolos07}. Joosten contributed mainly by making the files ready for the AFP. The need for a good formalisation of Turing Machines arose from realising that the current formalisation of saturation graphs~\cite{Graph_Saturation-AFP} is missing a key undecidability result present in the original paper~\cite{Joosten18}. Recently, an undecidability result has been added to the AFP by Felgenhauer~\cite{Minsky_Machines-AFP}, using a definition of computably enumerable sets formalised by Nedzelsky~\cite{Recursion-Theory-I-AFP}. This entry establishes the equivalence of these entirely separate notions of computability, but decidability remains future work. In 2022, Regensburger contributed by adding definitions for concepts like Turing Decidability, Turing Computability and Turing Reducibility for problem reduction. He also enhanced the result about the undecidability of the General Halting Problem given in the original AFP entry by first proving the undecidability of the Special Halting Problem and then proving its reducibility to the general problem. The original version of this AFP entry did only prove a weak form of the undecidability theorem. The main motivation behind this contribution is to make the AFP entry accessible for bachelor and master students. As a result, the presentation of the first chapter about Turing Machines has been considerably restructured and, in this context some minor changes in the naming of concepts were performed as well. In the rest of the theories the sectioning of the \LaTeX{} document was improved. -The overal contribution approximately doubled the size of the code base. +The overall contribution approximately doubled the size of the code base. Please refer to the CHANGELOG in the AFP entry for more details. % generated text of all theories \input{session} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: