diff -r 00ae320bb804 -r a8785fa80278 thys/turing_basic.thy --- a/thys/turing_basic.thy Mon Jan 14 21:40:38 2013 +0000 +++ b/thys/turing_basic.thy Tue Jan 15 19:05:15 2013 +0000 @@ -1,400 +1,605 @@ -(* Title: Turing machines - Author: Xu Jian - Maintainer: Xu Jian -*) - -theory turing_basic -imports Main -begin - -section {* Basic definitions of Turing machine *} - -definition - "iseven n \ \x. n = 2 * x" - -datatype action = W0 | W1 | L | R | Nop - -datatype cell = Bk | Oc - -type_synonym tape = "cell list \ cell list" - -type_synonym state = nat - -type_synonym instr = "action \ state" - -type_synonym tprog = "instr list" - -type_synonym config = "state \ tape" - -fun nth_of where - "nth_of [] _ = None" -| "nth_of (x # xs) 0 = Some x" -| "nth_of (x # xs) (Suc n) = nth_of xs n" - -lemma nth_of_map [simp]: - shows "nth_of (map f p) n = (case (nth_of p n) of None \ None | Some x \ Some (f x))" -apply(induct p arbitrary: n) -apply(auto) -apply(case_tac n) -apply(auto) -done - -fun - fetch :: "tprog \ state \ cell \ instr" -where - "fetch p 0 b = (Nop, 0)" -| "fetch p (Suc s) Bk = - (case nth_of p (2 * s) of - Some i \ i - | None \ (Nop, 0))" -|"fetch p (Suc s) Oc = - (case nth_of p ((2 * s) + 1) of - Some i \ i - | None \ (Nop, 0))" - -lemma fetch_Nil [simp]: - shows "fetch [] s b = (Nop, 0)" -apply(case_tac s) -apply(auto) -apply(case_tac b) -apply(auto) -done - -fun - update :: "action \ tape \ tape" -where - "update W0 (l, r) = (l, Bk # (tl r))" -| "update W1 (l, r) = (l, Oc # (tl r))" -| "update L (l, r) = (if l = [] then ([], Bk # r) else (tl l, (hd l) # r))" -| "update R (l, r) = (if r = [] then (Bk # l, []) else ((hd r) # l, tl r))" -| "update Nop (l, r) = (l, r)" - -abbreviation - "read r == if (r = []) then Bk else hd r" - - -fun - step :: "config \ tprog \ config" -where - "step (s, l, r) p = (let (a, s') = fetch p s (read r) in (s', update a (l, r)))" - -fun steps :: "config \ tprog \ nat \ config" - where - "steps c p 0 = c" | - "steps c p (Suc n) = steps (step c p) p n" - -lemma step_red [simp]: - shows "steps c p (Suc n) = step (steps c p n) p" -by (induct n arbitrary: c) (auto) - -lemma steps_add [simp]: - shows "steps c p (m + n) = steps (steps c p m) p n" -by (induct m arbitrary: c) (auto) - -definition - tm_wf :: "tprog \ bool" -where - "tm_wf p = (length p \ 2 \ iseven (length p) \ (\(a, s) \ set p. s \ length p div 2))" - - -(* FIXME: needed? *) -lemma halt_lemma: - "\wf LE; \n. (\ P (f n) \ (f (Suc n), (f n)) \ LE)\ \ \n. P (f n)" -by (metis wf_iff_no_infinite_down_chain) - -abbreviation exponent :: "'a \ nat \ 'a list" ("_ \ _" [100, 99] 100) - where "x \ n == replicate n x" - -definition tinres :: "cell list \ cell list \ bool" - where - "tinres xs ys = (\n. xs = ys @ Bk \ n \ ys = xs @ Bk \ n)" - -fun - shift :: "tprog \ nat \ tprog" -where - "shift p n = (map (\ (a, s). (a, (if s = 0 then 0 else s + n))) p)" - - -lemma length_shift [simp]: - "length (shift p n) = length p" -by (simp) - -fun - adjust :: "tprog \ tprog" -where - "adjust p = map (\ (a, s). (a, if s = 0 then ((length p) div 2) + 1 else s)) p" - -lemma length_adjust[simp]: - shows "length (adjust p) = length p" -by (induct p) (auto) - -definition - tm_comp :: "tprog \ tprog \ tprog" ("_ |+| _" [0, 0] 100) -where - "tm_comp p1 p2 = ((adjust p1) @ (shift p2 ((length p1) div 2)))" - -fun - is_final :: "config \ bool" -where - "is_final (s, l, r) = (s = 0)" - -lemma is_final_steps: - assumes "is_final (s, l, r)" - shows "is_final (steps (s, l, r) p n)" -using assms by (induct n) (auto) - -fun - holds_for :: "(tape \ bool) \ config \ bool" ("_ holds'_for _" [100, 99] 100) -where - "P holds_for (s, l, r) = P (l, r)" - -lemma step_0 [simp]: - shows "step (0, (l, r)) p = (0, (l, r))" -by simp - -lemma steps_0 [simp]: - shows "steps (0, (l, r)) p n = (0, (l, r))" -by (induct n) (simp_all) - -lemma is_final_holds[simp]: - assumes "is_final c" - shows "Q holds_for (steps c p n) = Q holds_for c" -using assms -apply(induct n) -apply(case_tac [!] c) -apply(auto) -done - -type_synonym assert = "tape \ bool" - -definition assert_imp :: "assert \ assert \ bool" ("_ \ _" [0, 0] 100) - where - "assert_imp P Q = (\l r. P (l, r) \ Q (l, r))" - -lemma holds_for_imp: - assumes "P holds_for c" - and "P \ Q" - shows "Q holds_for c" -using assms unfolding assert_imp_def by (case_tac c, auto) - -lemma test: - assumes "is_final (steps (1, (l, r)) p n1)" - and "is_final (steps (1, (l, r)) p n2)" - shows "Q holds_for (steps (1, (l, r)) p n1) \ Q holds_for (steps (1, (l, r)) p n2)" -proof - - obtain n3 where "n1 = n2 + n3 \ n2 = n1 + n3" - by (metis le_iff_add nat_le_linear) - with assms show "Q holds_for (steps (1, (l, r)) p n1) \ Q holds_for (steps (1, (l, r)) p n2)" - by auto -qed - -definition - Hoare :: "assert \ tprog \ assert \ bool" ("({(1_)}/ (_)/ {(1_)})" 50) -where - "{P} p {Q} \ - (\l r. P (l, r) \ (\n. is_final (steps (1, (l, r)) p n) \ Q holds_for (steps (1, (l, r)) p n)))" - -lemma HoareI: - assumes "\l r. P (l, r) \ \n. is_final (steps (1, (l, r)) p n) \ Q holds_for (steps (1, (l, r)) p n)" - shows "{P} p {Q}" -unfolding Hoare_def using assms by auto - -text {* -{P1} A {Q1} {P2} B {Q2} Q1 \ P2 ------------------------------------ - {P1} A |+| B {Q2} -*} - -lemma before_final: - assumes "steps (1, tp) A n = (0, tp')" - obtains n' where "\ is_final (steps (1, tp) A n')" and "steps (1, tp) A (Suc n') = (0, tp')" -using assms -apply(induct n) -apply(auto) -by (metis is_final.simps step_red steps.simps steps_0 surj_pair) - -lemma t_merge_fetch_pre: - assumes "fetch A s b = (ac, ns)" "s \ length A div 2" "tm_wf A" "s \ 0" - shows "fetch (adjustA |+| B) s b = (ac, if ns = 0 then Suc (length A div 2) else ns)" -using assms -unfolding tm_comp_def -apply(induct A) -apply(auto) -apply(subgoal_tac "2 * (s - Suc 0) < length A \ Suc (2 * (s - Suc 0)) < length A") -apply(auto simp: tm_wf_def iseven_def tm_comp_def split: if_splits cell.splits) -oops - -lemma t_merge_pre_eq_step: - "\step (a, b, c) A = cf; tm_wf A; \ is_final cf\ - \ step (a, b, c) (A |+| B) = cf" -apply(subgoal_tac "a \ length A div 2 \ a \ 0") -apply(simp) -apply(case_tac "fetch A a (read c)", simp) -apply(auto) -oops - -lemma t_merge_pre_eq: - "\steps (Suc 0, tp) A stp = cf; \ is_final cf; tm_wf A\ - \ steps (Suc 0, tp) (A |+| B) stp = cf" -apply(induct stp arbitrary: cf) -apply(auto)[1] -apply(auto) -oops - -lemma t_merge_pre_halt_same: - assumes a_ht: "steps (1, tp) A n = (0, tp')" - and a_wf: "t_correct A" - obtains n' where "steps (1, tp) (A |+| B) n' = (Suc (length A div 2), tp')" -proof - - assume a: "\n. steps (1, tp) (A |+| B) n = (Suc (length A div 2), tp') \ thesis" - - obtain stp' where "\ is_final (steps (1, tp) A stp')" and "steps (1, tp) A (Suc stp') = (0, tp')" - using a_ht before_final by blast - then have "steps (1, tp) (A |+| B) (Suc stp') = (Suc (length A div 2), tp')" - sorry (*using a_wf t_merge_pre_halt_same' by blast*) - with a show thesis by blast -qed - - - -lemma steps_comp: - assumes a1: "steps (1, l, r) A n1 = (s1, l1, r1)" - and a2: "steps (1, l1, r1) B n2 = (s2, l2, r2)" - shows "steps (1, l, r) (A |+| B) (n1 + n2) = (s2, l2, r2)" -using assms -apply(induct n2) -apply(simp) -apply(simp add: tm_comp_def) -oops - -lemma Hoare_plus: - assumes aimpb: "Q1 \ P2" - and A_wf : "tm_wf A" - and B_wf : "tm_wf B" - and A_halt : "{P1} A {Q1}" - and B_halt : "{P2} B {Q2}" - shows "{P1} A |+| B {Q2}" -proof(rule HoareI) - fix l r - assume h: "P1 (l, r)" - then obtain n1 where a: "is_final (steps (1, l, r) A n1)" and b: "Q1 holds_for (steps (1, l, r) A n1)" - using A_halt unfolding Hoare_def by auto - from b aimpb have "P2 holds_for (steps (1, l, r) A n1)" - by (rule holds_for_imp) - then obtain l' r' where "P2 (l', r')" - apply(auto) - apply(case_tac "steps (Suc 0, l, r) A n1") - apply(simp) - done - then obtain n2 where a: "is_final (steps (1, l', r') B n2)" and b: "Q2 holds_for (steps (1, l', r') B n2)" - using B_halt unfolding Hoare_def by auto - show "\n. is_final (steps (1, l, r) (A |+| B) n) \ Q2 holds_for (steps (1, l, r) (A |+| B) n)" - apply(rule_tac x="n1 + n2" in exI) - apply(rule conjI) - apply(simp) - apply(simp only: steps_add[symmetric]) - sorry -qed - - - - - -locale turing_merge = - fixes A :: "tprog" and B :: "tprog" and P1 :: "assert" - and P2 :: "assert" - and P3 :: "assert" - and P4 :: "assert" - and Q1:: "assert" - and Q2 :: "assert" - assumes - A_wf : "tm_wf A" - and B_wf : "tm_wf B" - and A_halt : "P1 tp \ \ stp. let (s, tp') = steps (Suc 0, tp) A stp in s = 0 \ Q1 tp'" - and B_halt : "P2 tp \ \ stp. let (s, tp') = steps (Suc 0, tp) B stp in s = 0 \ Q2 tp'" - and A_uhalt : "P3 tp \ \ (\ stp. is_final (steps (Suc 0, tp) A stp))" - and B_uhalt: "P4 tp \ \ (\ stp. is_final (steps (Suc 0, tp) B stp))" -begin - - -text {* - The following lemma tries to derive the Hoare logic rule for sequentially combined TMs. - It deals with the situtation when both @{text "A"} and @{text "B"} are terminated. -*} - - - -lemma t_merge_uhalt_tmp: - assumes B_uh: "\stp. \ is_final (steps (Suc 0, b, c) B stp)" - and merge_ah: "steps (Suc 0, tp) (A |+| B) stpa = (Suc (length A div 2), b, c)" - shows "\ stp. \ is_final (steps (Suc 0, tp) (A |+| B) stp)" - using B_uh merge_ah -apply(rule_tac allI) -apply(case_tac "stp > stpa") -apply(erule_tac x = "stp - stpa" in allE) -apply(case_tac "(steps (Suc 0, b, c) B (stp - stpa))", simp) -proof - - fix stp a ba ca - assume h1: "\ is_final (a, ba, ca)" "stpa < stp" - and h2: "steps (Suc 0, b, c) B (stp - stpa) = (a, ba, ca)" - have "steps (Suc 0 + length A div 2, b, c) (A |+| B) (stp - stpa) = - (if a = 0 then 0 else a + length A div 2, ba, ca)" - using A_wf B_wf h2 - by(rule_tac t_merge_snd_eq_steps, auto) - moreover have "a > 0" using h1 by(simp add: is_final_def) - moreover have "\ stpb. stp = stpa + stpb" - using h1 by(rule_tac x = "stp - stpa" in exI, simp) - ultimately show "\ is_final (steps (Suc 0, tp) (A |+| B) stp)" - using merge_ah - by(auto simp: steps_add is_final_def) -next - fix stp - assume h: "steps (Suc 0, tp) (A |+| B) stpa = (Suc (length A div 2), b, c)" "\ stpa < stp" - hence "\ stpb. stpa = stp + stpb" apply(rule_tac x = "stpa - stp" in exI, auto) done - thus "\ is_final (steps (Suc 0, tp) (A |+| B) stp)" - using h - apply(auto) - apply(cases "steps (Suc 0, tp) (A |+| B) stp", simp add: steps_add is_final_def steps_0) - done -qed - -text {* - The following lemma deals with the situation when TM @{text "B"} can not terminate. - *} - -lemma t_merge_uhalt: - assumes aimpb: "Q1 \ P4" - shows "P1 \ \ tp. \ (\ stp. is_final (steps (Suc 0, tp) (A |+| B) stp))" -proof(simp only: assert_imp_def, rule_tac allI, rule_tac impI) - fix tp - assume init_asst: "P1 tp" - show "\ (\stp. is_final (steps (Suc 0, tp) (A |+| B) stp))" - proof - - have "\ stp. let (s, tp') = steps (Suc 0, tp) A stp in s = 0 \ Q1 tp'" - using A_halt[of tp] init_asst - by(simp) - from this obtain stpx where "let (s, tp') = steps (Suc 0, tp) A stpx in s = 0 \ Q1 tp'" .. - thus "?thesis" - proof(cases "steps (Suc 0, tp) A stpx", simp, erule_tac conjE) - fix a b c - assume "Q1 (b, c)" - and h3: "steps (Suc 0, tp) A stpx = (0, b, c)" - hence h2: "P4 (b, c)" using aimpb - by(simp add: assert_imp_def) - have "\ stp. steps (Suc 0, tp) (A |+| B) stp = (Suc (length A div 2), b, c)" - using h3 A_wf B_wf - apply(rule_tac stp = stpx in t_merge_pre_halt_same, auto) - done - from this obtain stpa where h4:"steps (Suc 0, tp) (A |+| B) stpa = (Suc (length A div 2), b, c)" .. - have " \ (\ stp. is_final (steps (Suc 0, b, c) B stp))" - using B_uhalt [of "(b, c)"] h2 apply simp - done - from this and h4 show "\stp. \ is_final (steps (Suc 0, tp) (A |+| B) stp)" - by(rule_tac t_merge_uhalt_tmp, auto) - qed - qed -qed -end - -end - +(* Title: Turing machines + Author: Xu Jian + Maintainer: Xu Jian +*) + +theory turing_basic +imports Main +begin + +section {* Basic definitions of Turing machine *} + +datatype action = W0 | W1 | L | R | Nop + +datatype cell = Bk | Oc + +type_synonym tape = "cell list \ cell list" + +type_synonym state = nat + +type_synonym instr = "action \ state" + +type_synonym tprog = "instr list \ nat" + +type_synonym config = "state \ tape" + +fun nth_of where + "nth_of xs i = (if i \ length xs then None + else Some (xs ! i))" + +lemma nth_of_map [simp]: + shows "nth_of (map f p) n = (case (nth_of p n) of None \ None | Some x \ Some (f x))" +apply(induct p arbitrary: n) +apply(auto) +apply(case_tac n) +apply(auto) +done + +fun + fetch :: "instr list \ state \ cell \ instr" +where + "fetch p 0 b = (Nop, 0)" +| "fetch p (Suc s) Bk = + (case nth_of p (2 * s) of + Some i \ i + | None \ (Nop, 0))" +|"fetch p (Suc s) Oc = + (case nth_of p ((2 * s) + 1) of + Some i \ i + | None \ (Nop, 0))" + +lemma fetch_Nil [simp]: + shows "fetch [] s b = (Nop, 0)" +apply(case_tac s) +apply(auto) +apply(case_tac b) +apply(auto) +done + +fun + update :: "action \ tape \ tape" +where + "update W0 (l, r) = (l, Bk # (tl r))" +| "update W1 (l, r) = (l, Oc # (tl r))" +| "update L (l, r) = (if l = [] then ([], Bk # r) else (tl l, (hd l) # r))" +| "update R (l, r) = (if r = [] then (Bk # l, []) else ((hd r) # l, tl r))" +| "update Nop (l, r) = (l, r)" + +abbreviation + "read r == if (r = []) then Bk else hd r" + +fun step :: "config \ tprog \ config" + where + "step (s, l, r) (p, off) = + (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))" + +fun steps :: "config \ tprog \ nat \ config" + where + "steps c p 0 = c" | + "steps c p (Suc n) = steps (step c p) p n" + +lemma step_red [simp]: + shows "steps c p (Suc n) = step (steps c p n) p" +by (induct n arbitrary: c) (auto) + +lemma steps_add [simp]: + shows "steps c p (m + n) = steps (steps c p m) p n" +by (induct m arbitrary: c) (auto) + +fun + tm_wf :: "tprog \ bool" +where + "tm_wf (p, off) = (length p \ 2 \ length p mod 2 = 0 \ + (\(a, s) \ set p. s \ length p div 2 + + off \ s \ off))" + + +(* FIXME: needed? *) +lemma halt_lemma: + "\wf LE; \n. (\ P (f n) \ (f (Suc n), (f n)) \ LE)\ \ \n. P (f n)" +by (metis wf_iff_no_infinite_down_chain) + +abbreviation exponent :: "'a \ nat \ 'a list" ("_ \ _" [100, 99] 100) + where "x \ n == replicate n x" + +definition tinres :: "cell list \ cell list \ bool" + where + "tinres xs ys = (\n. xs = ys @ Bk \ n \ ys = xs @ Bk \ n)" + +fun + shift :: "instr list \ nat \ instr list" +where + "shift p n = (map (\ (a, s). (a, (if s = 0 then 0 else s + n))) p)" + + +lemma length_shift [simp]: + "length (shift p n) = length p" +by (simp) + +fun + adjust :: "instr list \ instr list" +where + "adjust p = map (\ (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p" + +lemma length_adjust[simp]: + shows "length (adjust p) = length p" +by (induct p) (auto) + +fun + tm_comp :: "instr list \ instr list \ instr list" ("_ |+| _" [0, 0] 100) +where + "tm_comp p1 p2 = ((adjust p1) @ (shift p2 ((length p1) div 2)))" + +fun + is_final :: "config \ bool" +where + "is_final (s, l, r) = (s = 0)" + +lemma is_final_steps: + assumes "is_final (s, l, r)" + shows "is_final (steps (s, l, r) (p, off) n)" +using assms by (induct n) (auto) + +fun + holds_for :: "(tape \ bool) \ config \ bool" ("_ holds'_for _" [100, 99] 100) +where + "P holds_for (s, l, r) = P (l, r)" + +(* +lemma step_0 [simp]: + shows "step (0, (l, r)) p = (0, (l, r))" +by simp + +lemma steps_0 [simp]: + shows "steps (0, (l, r)) p n = (0, (l, r))" +by (induct n) (simp_all) +*) + +lemma is_final_holds[simp]: + assumes "is_final c" + shows "Q holds_for (steps c (p, off) n) = Q holds_for c" +using assms +apply(induct n) +apply(case_tac [!] c) +apply(auto) +done + +type_synonym assert = "tape \ bool" + +definition assert_imp :: "assert \ assert \ bool" ("_ \ _" [0, 0] 100) + where + "assert_imp P Q = (\l r. P (l, r) \ Q (l, r))" + +lemma holds_for_imp: + assumes "P holds_for c" + and "P \ Q" + shows "Q holds_for c" +using assms unfolding assert_imp_def by (case_tac c, auto) + +lemma test: + assumes "is_final (steps (1, (l, r)) p n1)" + and "is_final (steps (1, (l, r)) p n2)" + shows "Q holds_for (steps (1, (l, r)) p n1) \ Q holds_for (steps (1, (l, r)) p n2)" +proof - + obtain n3 where "n1 = n2 + n3 \ n2 = n1 + n3" + by (metis le_iff_add nat_le_linear) + with assms show "Q holds_for (steps (1, (l, r)) p n1) \ Q holds_for (steps (1, (l, r)) p n2)" + by(case_tac p) (auto) +qed + +definition + Hoare :: "assert \ tprog \ assert \ bool" ("({(1_)}/ (_)/ {(1_)})" 50) +where + "{P} p {Q} \ + (\l r. P (l, r) \ (\n. is_final (steps (1, (l, r)) p n) \ Q holds_for (steps (1, (l, r)) p n)))" + +lemma HoareI: + assumes "\l r. P (l, r) \ \n. is_final (steps (1, (l, r)) p n) \ Q holds_for (steps (1, (l, r)) p n)" + shows "{P} p {Q}" +unfolding Hoare_def using assms by auto + +text {* +{P1} A {Q1} {P2} B {Q2} Q1 \ P2 +----------------------------------- + {P1} A |+| B {Q2} +*} + +lemma step_0 [simp]: + shows "step (0, (l, r)) p = (0, (l, r))" +by (case_tac p, simp) + +lemma steps_0 [simp]: + shows "steps (0, (l, r)) p n = (0, (l, r))" +by (induct n) (simp_all) + +declare steps.simps[simp del] + +lemma before_final: + assumes "steps (1, tp) A n = (0, tp')" + obtains n' where "\ is_final (steps (1, tp) A n')" + and "steps (1, tp) A (Suc n') = (0, tp')" +proof - + from assms have "\ n'. \ is_final (steps (1, tp) A n') \ + steps (1, tp) A (Suc n') = (0, tp')" + proof(induct n arbitrary: tp', simp add: steps.simps) + fix n tp' + assume ind: + "\tp'. steps (1, tp) A n = (0, tp') \ + \n'. \ is_final (steps (1, tp) A n') \ steps (1, tp) A (Suc n') = (0, tp')" + and h: " steps (1, tp) A (Suc n) = (0, tp')" + from h show "\n'. \ is_final (steps (1, tp) A n') \ steps (1, tp) A (Suc n') = (0, tp')" + proof(simp add: step_red del: steps.simps, + case_tac "(steps (Suc 0, tp) A n)", case_tac "a = 0", simp) + fix a b c + assume " steps (Suc 0, tp) A n = (0, tp')" + hence "\n'. \ is_final (steps (1, tp) A n') \ steps (1, tp) A (Suc n') = (0, tp')" + apply(rule_tac ind, simp) + done + thus "\n'. \ is_final (steps (Suc 0, tp) A n') \ step (steps (Suc 0, tp) A n') A = (0, tp')" + apply(simp) + done + next + fix a b c + assume "steps (Suc 0, tp) A n = (a, b, c)" + "step (steps (Suc 0, tp) A n) A = (0, tp')" + "a \ 0" + thus "\n'. \ is_final (steps (Suc 0, tp) A n') \ + step (steps (Suc 0, tp) A n') A = (0, tp')" + apply(rule_tac x = n in exI, simp) + done + qed + qed + thus "(\n'. \\ is_final (steps (1, tp) A n'); + steps (1, tp) A (Suc n') = (0, tp')\ \ thesis) \ thesis" + by auto +qed + +declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] + +lemma length_comp: +"length (A |+| B) = length A + length B" +apply(auto simp: tm_comp.simps) +done + +lemma tmcomp_fetch_in_first: + assumes "case (fetch A a x) of (ac, ns) \ ns \ 0" + shows "fetch (A |+| B) a x = fetch A a x" +using assms +apply(case_tac a, case_tac [!] x, +auto simp: length_comp tm_comp.simps length_adjust nth_append) +apply(simp_all add: adjust.simps) +done + + +lemma is_final_eq: "is_final (ba, tp) = (ba = 0)" +apply(case_tac tp, simp add: is_final.simps) +done + +lemma t_merge_pre_eq_step: + assumes step: "step (a, b, c) (A, 0) = cf" + and tm_wf: "tm_wf (A, 0)" + and unfinal: "\ is_final cf" + shows "step (a, b, c) (A |+| B, 0) = cf" +proof - + have "fetch (A |+| B) a (read c) = fetch A a (read c)" + proof(rule_tac tmcomp_fetch_in_first) + from step and unfinal show "case fetch A a (read c) of (ac, ns) \ ns \ 0" + apply(auto simp: is_final.simps) + apply(case_tac "fetch A a (read c)", simp_all add: is_final_eq) + done + qed + thus "?thesis" + using step + apply(auto simp: step.simps is_final.simps) + done +qed + +declare tm_wf.simps[simp del] step.simps[simp del] + +lemma t_merge_pre_eq: + "\steps (Suc 0, tp) (A, 0) stp = cf; \ is_final cf; tm_wf (A, 0)\ + \ steps (Suc 0, tp) (A |+| B, 0) stp = cf" +proof(induct stp arbitrary: cf, simp add: steps.simps) + fix stp cf + assume ind: "\cf. \steps (Suc 0, tp) (A, 0) stp = cf; \ is_final cf; tm_wf (A, 0)\ + \ steps (Suc 0, tp) (A |+| B, 0) stp = cf" + and h: "steps (Suc 0, tp) (A, 0) (Suc stp) = cf" + "\ is_final cf" "tm_wf (A, 0)" + from h show "steps (Suc 0, tp) (A |+| B, 0) (Suc stp) = cf" + proof(simp add: step_red, case_tac "(steps (Suc 0, tp) (A, 0) stp)", simp) + fix a b c + assume g: "steps (Suc 0, tp) (A, 0) stp = (a, b, c)" + "step (a, b, c) (A, 0) = cf" + have "(steps (Suc 0, tp) (A |+| B, 0) stp) = (a, b, c)" + proof(rule ind, simp_all add: h g) + show "0 < a" + using g h + apply(simp add: step_red) + apply(case_tac a, auto simp: step_0) + apply(case_tac "steps (Suc 0, tp) (A, 0) stp", simp) + done + qed + thus "step (steps (Suc 0, tp) (A |+| B, 0) stp) (A |+| B, 0) = cf" + apply(simp) + apply(rule_tac t_merge_pre_eq_step, simp_all add: g h) + done + qed +qed + +lemma tmcomp_fetch_in_first2: + assumes "fetch A a x = (ac, 0)" + "tm_wf (A, 0)" + "a \ length A div 2" "a > 0" + shows "fetch (A |+| B) a x = (ac, Suc (length A div 2))" +using assms +apply(case_tac a, case_tac [!] x, +auto simp: length_comp tm_comp.simps length_adjust nth_append) +apply(simp_all add: adjust.simps) +done + +lemma tmcomp_exec_after_first: + "\0 < a; step (a, b, c) (A, 0) = (0, tp'); tm_wf (A, 0); + a \ length A div 2\ + \ step (a, b, c) (A |+| B, 0) = (Suc (length A div 2), tp')" +apply(simp add: step.simps, auto) +apply(case_tac "fetch A a Bk", simp add: tmcomp_fetch_in_first2) +apply(case_tac "fetch A a (hd c)", simp add: tmcomp_fetch_in_first2) +done + +lemma step_nothalt_pre: "\step (aa, ba, ca) (A, 0) = (a, b, c); 0 < a\ \ 0 < aa" +apply(case_tac "aa = 0", simp add: step_0, simp) +done + +lemma nth_in_set: + "\ A ! i = x; i < length A\ \ x \ set A" +by auto + +lemma step_nothalt: + "\step (aa, ba, ca) (A, 0) = (a, b, c); 0 < a; tm_wf (A, 0)\ \ + a \ length A div 2" +apply(simp add: step.simps) +apply(case_tac aa, case_tac [!] aa, auto split: if_splits simp: tm_wf.simps) +apply(case_tac "A ! (2 * nat)", simp) +apply(erule_tac x = "(aa, a)" in ballE, simp_all add: nth_in_set) +apply(case_tac "hd ca", auto split: if_splits simp: tm_wf.simps) +apply(case_tac "A ! (2 * nat)", simp) +apply(erule_tac x = "(aa, a)" in ballE, simp_all add: nth_in_set) +apply(case_tac "A ! (Suc (2 * nat))") +apply(erule_tac x = "(aa,bb)" in ballE, simp_all add: nth_in_set) +done + +lemma steps_in_range: + " \0 < a; steps (Suc 0, tp) (A, 0) stp = (a, b, c); tm_wf (A, 0)\ + \ a \ length A div 2" +proof(induct stp arbitrary: a b c) + fix a b c + assume h: "0 < a" "steps (Suc 0, tp) (A, 0) 0 = (a, b, c)" + "tm_wf (A, 0)" + thus "a \ length A div 2" + apply(simp add: steps.simps tm_wf.simps, auto) + done +next + fix stp a b c + assume ind: "\a b c. \0 < a; steps (Suc 0, tp) (A, 0) stp = (a, b, c); + tm_wf (A, 0)\ \ a \ length A div 2" + and h: "0 < a" "steps (Suc 0, tp) (A, 0) (Suc stp) = (a, b, c)" "tm_wf (A, 0)" + from h show "a \ length A div 2" + proof(simp add: step_red, case_tac "(steps (Suc 0, tp) (A, 0) stp)", simp) + fix aa ba ca + assume g: "step (aa, ba, ca) (A, 0) = (a, b, c)" + "steps (Suc 0, tp) (A, 0) stp = (aa, ba, ca)" + hence "aa \ length A div 2" + apply(rule_tac ind, auto simp: h step_nothalt_pre) + done + thus "?thesis" + using g h + apply(rule_tac step_nothalt, auto) + done + qed +qed + +lemma t_merge_pre_halt_same: + assumes a_ht: "steps (1, tp) (A, 0) n = (0, tp')" + and a_wf: "tm_wf (A, 0)" + obtains n' where "steps (1, tp) (A |+| B, 0) n' = (Suc (length A div 2), tp')" +proof - + assume a: "\n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \ thesis" + obtain stp' where "\ is_final (steps (1, tp) (A, 0) stp')" and + "steps (1, tp) (A, 0) (Suc stp') = (0, tp')" + using a_ht before_final by blast + then have "steps (1, tp) (A |+| B, 0) (Suc stp') = (Suc (length A div 2), tp')" + proof(simp add: step_red) + assume "\ is_final (steps (Suc 0, tp) (A, 0) stp')" + " step (steps (Suc 0, tp) (A, 0) stp') (A, 0) = (0, tp')" + moreover hence "(steps (Suc 0, tp) (A |+| B, 0) stp') = (steps (Suc 0, tp) (A, 0) stp')" + apply(rule_tac t_merge_pre_eq) + apply(simp_all add: a_wf a_ht) + done + ultimately show "step (steps (Suc 0, tp) (A |+| B, 0) stp') (A |+| B, 0) = (Suc (length A div 2), tp')" + apply(case_tac " steps (Suc 0, tp) (A, 0) stp'", simp) + apply(rule tmcomp_exec_after_first, simp_all add: a_wf) + apply(erule_tac steps_in_range, auto simp: a_wf) + done + qed + with a show thesis by blast +qed + +lemma tm_comp_fetch_second_zero: + "\fetch B sa' x = (a, 0); tm_wf (A, 0); tm_wf (B, 0); sa' > 0\ + \ fetch (A |+| B) (sa' + (length A div 2)) x = (a, 0)" +apply(case_tac x) +apply(case_tac [!] sa', + auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps + tm_wf.simps shift.simps split: if_splits) +done + +lemma tm_comp_fetch_second_inst: + "\sa > 0; s > 0; tm_wf (A, 0); tm_wf (B, 0); fetch B sa x = (a, s)\ + \ fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)" +apply(case_tac x) +apply(case_tac [!] sa, + auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps + tm_wf.simps shift.simps split: if_splits) +done + +lemma t_merge_second_same: + assumes a_wf: "tm_wf (A, 0)" + and b_wf: "tm_wf (B, 0)" + and steps: "steps (Suc 0, l, r) (B, 0) stp = (s, l', r')" + shows "steps (Suc (length A div 2), l, r) (A |+| B, 0) stp + = (if s = 0 then 0 + else s + length A div 2, l', r')" +using a_wf b_wf steps +proof(induct stp arbitrary: s l' r', simp add: steps.simps, simp) + fix stpa sa l'a r'a + assume ind: "\s l' r'. steps (Suc 0, l, r) (B, 0) stpa = (s, l', r') \ + steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa = + (if s = 0 then 0 else s + length A div 2, l', r')" + and h: "step (steps (Suc 0, l, r) (B, 0) stpa) (B, 0) = (sa, l'a, r'a)" + obtain sa' l'' r'' where a: "(steps (Suc 0, l, r) (B, 0) stpa) = (sa', l'', r'')" + apply(case_tac "steps (Suc 0, l, r) (B, 0) stpa", auto) + done + from this have b: "steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa = + (if sa' = 0 then 0 else sa' + length A div 2, l'', r'')" + apply(erule_tac ind) + done + from a b h show + "(sa = 0 \ step (steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa) (A |+| B, 0) = (0, l'a, r'a)) \ + (0 < sa \ step (steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa) (A |+| B, 0) = (sa + length A div 2, l'a, r'a))" + proof(case_tac "sa' = 0", auto) + assume "step (sa', l'', r'') (B, 0) = (0, l'a, r'a)" "0 < sa'" + thus "step (sa' + length A div 2, l'', r'') (A |+| B, 0) = (0, l'a, r'a)" + using a_wf b_wf + apply(simp add: step.simps) + apply(case_tac "fetch B sa' (read r'')", auto) + apply(simp_all add: step.simps tm_comp_fetch_second_zero) + done + next + assume "step (sa', l'', r'') (B, 0) = (sa, l'a, r'a)" "0 < sa'" "0 < sa" + thus "step (sa' + length A div 2, l'', r'') (A |+| B, 0) = (sa + length A div 2, l'a, r'a)" + using a_wf b_wf + apply(simp add: step.simps) + apply(case_tac "fetch B sa' (read r'')", auto) + apply(simp_all add: step.simps tm_comp_fetch_second_inst) + done + qed +qed + +lemma t_merge_second_halt_same: + "\tm_wf (A, 0); tm_wf (B, 0); + steps (1, l, r) (B, 0) stp = (0, l', r')\ + \ steps (Suc (length A div 2), l, r) (A |+| B, 0) stp + = (0, l', r')" +using t_merge_second_same[where s = "0"] +apply(auto) +done + +lemma Hoare_plus_halt: + assumes aimpb: "Q1 \ P2" + and A_wf : "tm_wf (A, 0)" + and B_wf : "tm_wf (B, 0)" + and A_halt : "{P1} (A, 0) {Q1}" + and B_halt : "{P2} (B, 0) {Q2}" + shows "{P1} (A |+| B, 0) {Q2}" +proof(rule HoareI) + fix l r + assume h: "P1 (l, r)" + then obtain n1 where a: "is_final (steps (1, l, r) (A, 0) n1)" and b: "Q1 holds_for (steps (1, l, r) (A, 0) n1)" + using A_halt unfolding Hoare_def by auto + then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" + by(case_tac "steps (1, l, r) (A, 0) n1", auto) + then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')" + using A_wf + by(rule_tac t_merge_pre_halt_same, auto) + from c aimpb have "P2 holds_for (0, l', r')" + by(rule holds_for_imp) + from this have "P2 (l', r')" by auto + from this obtain n2 where e: "is_final (steps (1, l', r') (B, 0) n2)" and f: "Q2 holds_for (steps (1, l', r') (B, 0) n2)" + using B_halt unfolding Hoare_def + by auto + then obtain l'' r'' where "steps (1, l', r') (B, 0) n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')" + by(case_tac "steps (1, l', r') (B, 0) n2", auto) + from this have "steps (Suc (length A div 2), l', r') (A |+| B, 0) n2 + = (0, l'', r'')" + apply(rule_tac t_merge_second_halt_same, auto simp: A_wf B_wf) + done + thus "\n. is_final (steps (1, l, r) (A |+| B, 0) n) \ Q2 holds_for (steps (1, l, r) (A |+| B, 0) n)" + using d g + apply(rule_tac x = "stpa + n2" in exI) + apply(simp add: steps_add) + done +qed + +definition + Hoare_unhalt :: "assert \ tprog \ bool" ("({(1_)}/ (_))" 50) +where + "{P} p \ + (\l r. P (l, r) \ (\ n . \ (is_final (steps (1, (l, r)) p n))))" + +lemma Hoare_unhalt_I: + assumes "\l r. P (l, r) \ \ n. \ is_final (steps (1, (l, r)) p n)" + shows "{P} p" +unfolding Hoare_unhalt_def using assms by auto + +lemma Hoare_plus_unhalt: + assumes aimpb: "Q1 \ P2" + and A_wf : "tm_wf (A, 0)" + and B_wf : "tm_wf (B, 0)" + and A_halt : "{P1} (A, 0) {Q1}" + and B_uhalt : "{P2} (B, 0)" + shows "{P1} (A |+| B, 0)" +proof(rule_tac Hoare_unhalt_I) + fix l r + assume h: "P1 (l, r)" + then obtain n1 where a: "is_final (steps (1, l, r) (A, 0) n1)" and b: "Q1 holds_for (steps (1, l, r) (A, 0) n1)" + using A_halt unfolding Hoare_def by auto + then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" + by(case_tac "steps (1, l, r) (A, 0) n1", auto) + then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')" + using A_wf + by(rule_tac t_merge_pre_halt_same, auto) + from c aimpb have "P2 holds_for (0, l', r')" + by(rule holds_for_imp) + from this have "P2 (l', r')" by auto + from this have e: "\ n. \ is_final (steps (Suc 0, l', r') (B, 0) n) " + using B_uhalt unfolding Hoare_unhalt_def + by auto + from e show "\n. \ is_final (steps (1, l, r) (A |+| B, 0) n)" + proof(rule_tac allI, case_tac "n > stpa") + fix n + assume h2: "stpa < n" + hence "\ is_final (steps (Suc 0, l', r') (B, 0) (n - stpa))" + using e + apply(erule_tac x = "n - stpa" in allE) by simp + then obtain s'' l'' r'' where f: "steps (Suc 0, l', r') (B, 0) (n - stpa) = (s'', l'', r'')" and g: "s'' \ 0" + apply(case_tac "steps (Suc 0, l', r') (B, 0) (n - stpa)", auto) + done + have k: "steps (Suc (length A div 2), l', r') (A |+| B, 0) (n - stpa) = (s''+ length A div 2, l'', r'') " + using A_wf B_wf f g + apply(drule_tac t_merge_second_same, auto) + done + show "\ is_final (steps (1, l, r) (A |+| B, 0) n)" + proof - + have "\ is_final (steps (1, l, r) (A |+| B, 0) (stpa + (n - stpa)))" + using d k A_wf + apply(simp only: steps_add d, simp add: tm_wf.simps) + done + thus "\ is_final (steps (1, l, r) (A |+| B, 0) n)" + using h2 by simp + qed + next + fix n + assume h2: "\ stpa < n" + with d show "\ is_final (steps (1, l, r) (A |+| B, 0) n)" + apply(auto) + apply(subgoal_tac "\ d. stpa = n + d", auto) + apply(case_tac "(steps (Suc 0, l, r) (A |+| B, 0) n)", simp) + apply(rule_tac x = "stpa - n" in exI, simp) + done + qed +qed + + + +end +