diff -r 30950dadd09f -r c8ff97d9f8da thys/abacus.thy --- a/thys/abacus.thy Sun Jan 20 05:04:19 2013 +0000 +++ b/thys/abacus.thy Sun Jan 20 16:01:16 2013 +0000 @@ -3,7 +3,7 @@ *} theory abacus -imports Main turing_basic +imports Main turing_hoare begin text {* @@ -217,8 +217,7 @@ fun tdec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list" where - "tdec ss n e = sete (shift (findnth n @ shift tdec_b (2 * n)) - (ss - 1)) e" + "tdec ss n e = shift (findnth n) (ss - 1) @ sete (shift (shift tdec_b (2 * n)) (ss - 1)) e" text {* @{text "tgoto f(label)"} returns the TM simulating the execution of Abacus instruction @@ -348,6 +347,23 @@ A more general definition of TM execution. *} +(* +fun nnth_of :: "(taction \<times> nat) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (taction \<times> nat)" + where + "nnth_of p s b = (if 2*s < length p + then (p ! (2*s + b)) else (Nop, 0))" + +thm nth_of.simps + +fun nfetch :: "tprog \<Rightarrow> nat \<Rightarrow> block \<Rightarrow> taction \<times> nat" + where + "nfetch p 0 b = (Nop, 0)" | + "nfetch p (Suc s) b = + (case b of + Bk \<Rightarrow> nnth_of p s 0 | + Oc \<Rightarrow> nnth_of p s 1)" +*) + text {* The type of invarints expressing correspondence between @@ -362,7 +378,6 @@ ci.simps [simp del] length_of.simps[simp del] layout_of.simps[simp del] - (* subsection {* The compilation of @{text "Inc n"} *} *) @@ -372,16 +387,36 @@ the compilation of @{text "Inc n"} instruction. *} - declare abc_step_l.simps[simp del] abc_steps_l.simps[simp del] lemma [simp]: "start_of ly as > 0" apply(simp add: start_of.simps) done +lemma abc_steps_l_0: "abc_steps_l ac ap 0 = ac" +by(case_tac ac, simp add: abc_steps_l.simps) + lemma abc_step_red: - "abc_steps_l ac aprog stp = (as, am) \<Longrightarrow> - abc_steps_l ac aprog (Suc stp) = abc_step_l (as, am) (abc_fetch as aprog) " -oops + "abc_steps_l (as, am) ap stp = (bs, bm) \<Longrightarrow> + abc_steps_l (as, am) ap (Suc stp) = abc_step_l (bs, bm) (abc_fetch bs ap) " +proof(induct stp arbitrary: as am bs bm) + case 0 + thus "?case" + by(simp add: abc_steps_l.simps abc_steps_l_0) +next + case (Suc stp as am bs bm) + have ind: "\<And>as am bs bm. abc_steps_l (as, am) ap stp = (bs, bm) \<Longrightarrow> + abc_steps_l (as, am) ap (Suc stp) = abc_step_l (bs, bm) (abc_fetch bs ap)" + by fact + have h:" abc_steps_l (as, am) ap (Suc stp) = (bs, bm)" by fact + obtain as' am' where g: "abc_step_l (as, am) (abc_fetch as ap) = (as', am')" + by(case_tac "abc_step_l (as, am) (abc_fetch as ap)", auto) + then have "abc_steps_l (as', am') ap (Suc stp) = abc_step_l (bs, bm) (abc_fetch bs ap)" + using h + by(rule_tac ind, simp add: abc_steps_l.simps) + thus "?case" + using g + by(simp add: abc_steps_l.simps) +qed lemma tm_shift_fetch: "\<lbrakk>fetch A s b = (ac, ns); ns \<noteq> 0 \<rbrakk> @@ -400,10 +435,10 @@ apply(drule_tac [!] off = off in tm_shift_fetch, simp_all) done +declare step.simps[simp del] steps.simps[simp del] shift.simps[simp del] + lemma tm_shift_eq_steps: - assumes layout: "ly = layout_of ap" - and compile: "tp = tm_of ap" - and exec: "steps (s, l, r) (A, 0) stp = (s', l', r')" + assumes exec: "steps (s, l, r) (A, 0) stp = (s', l', r')" and notfinal: "s' \<noteq> 0" shows "steps (s + off, l, r) (shift A off, off) stp = (s' + off, l', r')" using exec notfinal @@ -416,7 +451,8 @@ apply(case_tac "steps (s, l, r) (A, 0) stp") by blast moreover then have "s1 \<noteq> 0" using h - apply(simp add: step_red, case_tac "0 < s1", simp, simp) + apply(simp add: step_red) + apply(case_tac "0 < s1", auto) done ultimately have "steps (s + off, l, r) (shift A off, off) stp = (s1 + off, l1, r1)" @@ -437,6 +473,284 @@ apply(simp add: start_of.simps) done +lemma start_of_Suc1: "\<lbrakk>ly = layout_of ap; + abc_fetch as ap = Some (Inc n)\<rbrakk> + \<Longrightarrow> start_of ly (Suc as) = start_of ly as + 2 * n + 9" +apply(auto simp: start_of.simps layout_of.simps + length_of.simps abc_fetch.simps + take_Suc_conv_app_nth split: if_splits) +done + +lemma start_of_Suc2: + "\<lbrakk>ly = layout_of ap; + abc_fetch as ap = Some (Dec n e)\<rbrakk> \<Longrightarrow> + start_of ly (Suc as) = + start_of ly as + 2 * n + 16" +apply(auto simp: start_of.simps layout_of.simps + length_of.simps abc_fetch.simps + take_Suc_conv_app_nth split: if_splits) +done + +lemma start_of_Suc3: + "\<lbrakk>ly = layout_of ap; + abc_fetch as ap = Some (Goto n)\<rbrakk> \<Longrightarrow> + start_of ly (Suc as) = start_of ly as + 1" +apply(auto simp: start_of.simps layout_of.simps + length_of.simps abc_fetch.simps + take_Suc_conv_app_nth split: if_splits) +done + +lemma length_ci_inc: + "length (ci ly ss (Inc n)) = 4*n + 18" +apply(auto simp: ci.simps length_findnth tinc_b_def) +done + +lemma length_ci_dec: + "length (ci ly ss (Dec n e)) = 4*n + 32" +apply(auto simp: ci.simps length_findnth tdec_b_def) +done + +lemma length_ci_goto: + "length (ci ly ss (Goto n )) = 2" +apply(auto simp: ci.simps length_findnth tdec_b_def) +done + +lemma take_Suc_last[elim]: "Suc as \<le> length xs \<Longrightarrow> + take (Suc as) xs = take as xs @ [xs ! as]" +apply(induct xs arbitrary: as, simp, simp) +apply(case_tac as, simp, simp) +done + +lemma concat_suc: "Suc as \<le> length xs \<Longrightarrow> + concat (take (Suc as) xs) = concat (take as xs) @ xs! as" +apply(subgoal_tac "take (Suc as) xs = take as xs @ [xs ! as]", simp) +by auto + +lemma concat_take_suc_iff: "Suc n \<le> length tps \<Longrightarrow> + concat (take n tps) @ (tps ! n) = concat (take (Suc n) tps)" +apply(drule_tac concat_suc, simp) +done + +lemma concat_drop_suc_iff: + "Suc n < length tps \<Longrightarrow> concat (drop (Suc n) tps) = + tps ! Suc n @ concat (drop (Suc (Suc n)) tps)" +apply(induct tps arbitrary: n, simp, simp) +apply(case_tac tps, simp, simp) +apply(case_tac n, simp, simp) +done + +declare append_assoc[simp del] + +lemma tm_append: + "\<lbrakk>n < length tps; tp = tps ! n\<rbrakk> \<Longrightarrow> + \<exists> tp1 tp2. concat tps = tp1 @ tp @ tp2 \<and> tp1 = + concat (take n tps) \<and> tp2 = concat (drop (Suc n) tps)" +apply(rule_tac x = "concat (take n tps)" in exI) +apply(rule_tac x = "concat (drop (Suc n) tps)" in exI) +apply(auto) +apply(induct n, simp) +apply(case_tac tps, simp, simp, simp) +apply(subgoal_tac "concat (take n tps) @ (tps ! n) = + concat (take (Suc n) tps)") +apply(simp only: append_assoc[THEN sym], simp only: append_assoc) +apply(subgoal_tac " concat (drop (Suc n) tps) = tps ! Suc n @ + concat (drop (Suc (Suc n)) tps)", simp) +apply(rule_tac concat_drop_suc_iff, simp) +apply(rule_tac concat_take_suc_iff, simp) +done + +declare append_assoc[simp] + +lemma map_of: "n < length xs \<Longrightarrow> (map f xs) ! n = f (xs ! n)" +by(auto) + +lemma [simp]: "length (tms_of aprog) = length aprog" +apply(auto simp: tms_of.simps tpairs_of.simps) +done + +lemma ci_nth: + "\<lbrakk>ly = layout_of aprog; + abc_fetch as aprog = Some ins\<rbrakk> + \<Longrightarrow> ci ly (start_of ly as) ins = tms_of aprog ! as" +apply(simp add: tms_of.simps tpairs_of.simps + abc_fetch.simps map_of del: map_append split: if_splits) +done + +lemma t_split:"\<lbrakk> + ly = layout_of aprog; + abc_fetch as aprog = Some ins\<rbrakk> + \<Longrightarrow> \<exists> tp1 tp2. concat (tms_of aprog) = + tp1 @ (ci ly (start_of ly as) ins) @ tp2 + \<and> tp1 = concat (take as (tms_of aprog)) \<and> + tp2 = concat (drop (Suc as) (tms_of aprog))" +apply(insert tm_append[of "as" "tms_of aprog" + "ci ly (start_of ly as) ins"], simp) +apply(subgoal_tac "ci ly (start_of ly as) ins = (tms_of aprog) ! as") +apply(subgoal_tac "length (tms_of aprog) = length aprog") +apply(simp add: abc_fetch.simps split: if_splits, simp) +apply(rule_tac ci_nth, auto) +done + +lemma math_sub: "\<lbrakk>x >= Suc 0; x - 1 = z\<rbrakk> \<Longrightarrow> x + y - Suc 0 = z + y" +by auto + +lemma start_more_one: "as \<noteq> 0 \<Longrightarrow> start_of ly as >= Suc 0" +apply(induct as, simp add: start_of.simps) +apply(case_tac as, auto simp: start_of.simps) +done + +lemma div_apart: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> + \<Longrightarrow> (x + y) div 2 = x div 2 + y div 2" +apply(drule mod_eqD)+ +apply(auto) +done + +lemma div_apart_iff: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> \<Longrightarrow> + (x + y) mod 2 = 0" +apply(auto) +done + +lemma [simp]: "length (layout_of aprog) = length aprog" +apply(auto simp: layout_of.simps) +done + +lemma start_of_ind: "\<lbrakk>as < length aprog; ly = layout_of aprog\<rbrakk> \<Longrightarrow> + start_of ly (Suc as) = start_of ly as + + length ((tms_of aprog) ! as) div 2" +apply(simp only: start_of.simps, simp) +apply(auto simp: start_of.simps tms_of.simps layout_of.simps + tpairs_of.simps) +apply(simp add: ci_length take_Suc take_Suc_conv_app_nth) +done + +lemma concat_take_suc: "Suc n \<le> length xs \<Longrightarrow> + concat (take (Suc n) xs) = concat (take n xs) @ (xs ! n)" +apply(subgoal_tac "take (Suc n) xs = + take n xs @ [xs ! n]") +apply(auto) +done + +lemma [simp]: + "\<lbrakk>as < length aprog; (abc_fetch as aprog) = Some ins\<rbrakk> + \<Longrightarrow> ci (layout_of aprog) + (start_of (layout_of aprog) as) (ins) \<in> set (tms_of aprog)" +apply(insert ci_nth[of "layout_of aprog" aprog as], simp) +done + +lemma [simp]: "length (tms_of ap) = length ap" +by(auto simp: tms_of.simps tpairs_of.simps) + +lemma [intro]: "n < length ap \<Longrightarrow> length (tms_of ap ! n) mod 2 = 0" +apply(auto simp: tms_of.simps tpairs_of.simps) +apply(case_tac "ap ! n", auto simp: ci.simps length_findnth tinc_b_def tdec_b_def) +apply arith +by arith + +lemma compile_mod2: "length (concat (take n (tms_of ap))) mod 2 = 0" +apply(induct n, auto) +apply(case_tac "n < length (tms_of ap)", simp add: take_Suc_conv_app_nth, auto) +apply(subgoal_tac "length (tms_of ap ! n) mod 2 = 0") +apply arith +by auto + +lemma tpa_states: + "\<lbrakk>tp = concat (take as (tms_of ap)); + as \<le> length ap\<rbrakk> \<Longrightarrow> + start_of (layout_of ap) as = Suc (length tp div 2)" +proof(induct as arbitrary: tp) + case 0 + thus "?case" + by(simp add: start_of.simps) +next + case (Suc as tp) + have ind: "\<And>tp. \<lbrakk>tp = concat (take as (tms_of ap)); as \<le> length ap\<rbrakk> \<Longrightarrow> + start_of (layout_of ap) as = Suc (length tp div 2)" by fact + have tp: "tp = concat (take (Suc as) (tms_of ap))" by fact + have le: "Suc as \<le> length ap" by fact + have a: "start_of (layout_of ap) as = Suc (length (concat (take as (tms_of ap))) div 2)" + using le + by(rule_tac ind, simp_all) + from a tp le show "?case" + apply(simp add: start_of.simps take_Suc_conv_app_nth) + apply(subgoal_tac "length (concat (take as (tms_of ap))) mod 2= 0") + apply(subgoal_tac " length (tms_of ap ! as) mod 2 = 0") + apply(simp add: abacus.div_apart) + apply(simp add: layout_of.simps ci_length tms_of.simps tpairs_of.simps) + apply(auto intro: compile_mod2) + done +qed + +lemma append_append_fetch: + "\<lbrakk>length tp1 mod 2 = 0; length tp mod 2 = 0; + length tp1 div 2 < a \<and> a \<le> length tp1 div 2 + length tp div 2\<rbrakk> + \<Longrightarrow>fetch (tp1 @ tp @ tp2) a b = fetch tp (a - length tp1 div 2) b " +apply(subgoal_tac "\<exists> x. a = length tp1 div 2 + x", erule exE, simp) +apply(case_tac x, simp) +apply(subgoal_tac "length tp1 div 2 + Suc nat = + Suc (length tp1 div 2 + nat)") +apply(simp only: fetch.simps nth_of.simps, auto) +apply(case_tac b, simp) +apply(subgoal_tac "2 * (length tp1 div 2) = length tp1", simp) +apply(subgoal_tac "2 * nat < length tp", simp add: nth_append, simp) +apply(subgoal_tac "2 * (length tp1 div 2) = length tp1", simp) +apply(subgoal_tac "2 * nat < length tp", simp add: nth_append, auto) +apply(auto simp: nth_append) +apply(rule_tac x = "a - length tp1 div 2" in exI, simp) +done + +lemma step_eq_fetch': + assumes layout: "ly = layout_of ap" + and compile: "tp = tm_of ap" + and fetch: "abc_fetch as ap = Some ins" + and range1: "s \<ge> start_of ly as" + and range2: "s < start_of ly (Suc as)" + shows "fetch tp s b = fetch (ci ly (start_of ly as) ins) + (Suc s - start_of ly as) b " +proof - + have "\<exists>tp1 tp2. concat (tms_of ap) = tp1 @ ci ly (start_of ly as) ins @ tp2 \<and> + tp1 = concat (take as (tms_of ap)) \<and> tp2 = concat (drop (Suc as) (tms_of ap))" + using assms + by(rule_tac t_split, simp_all) + then obtain tp1 tp2 where a: "concat (tms_of ap) = tp1 @ ci ly (start_of ly as) ins @ tp2 \<and> + tp1 = concat (take as (tms_of ap)) \<and> tp2 = concat (drop (Suc as) (tms_of ap))" by blast + then have b: "start_of (layout_of ap) as = Suc (length tp1 div 2)" + using fetch + apply(rule_tac tpa_states, simp, simp add: abc_fetch.simps split: if_splits) + done + have "fetch (tp1 @ (ci ly (start_of ly as) ins) @ tp2) s b = + fetch (ci ly (start_of ly as) ins) (s - length tp1 div 2) b" + proof(rule_tac append_append_fetch) + show "length tp1 mod 2 = 0" + using a + by(auto, rule_tac compile_mod2) + next + show "length (ci ly (start_of ly as) ins) mod 2 = 0" + apply(case_tac ins, auto simp: ci.simps length_findnth tinc_b_def tdec_b_def) + by(arith, arith) + next + show "length tp1 div 2 < s \<and> s \<le> + length tp1 div 2 + length (ci ly (start_of ly as) ins) div 2" + proof - + have "length (ci ly (start_of ly as) ins) div 2 = length_of ins" + using ci_length by simp + moreover have "start_of ly (Suc as) = start_of ly as + length_of ins" + using fetch layout + apply(simp add: start_of.simps abc_fetch.simps List.take_Suc_conv_app_nth + split: if_splits) + apply(simp add: layout_of.simps) + done + ultimately show "?thesis" + using b layout range1 range2 + apply(simp) + done + qed + qed + thus "?thesis" + using b layout a compile + apply(simp add: tm_of.simps) + done +qed + lemma step_eq_fetch: assumes layout: "ly = layout_of ap" and compile: "tp = tm_of ap" @@ -445,8 +759,55 @@ (Suc s - start_of ly as) b = (ac, ns)" and notfinal: "ns \<noteq> 0" shows "fetch tp s b = (ac, ns)" -oops - +proof - + have "s \<ge> start_of ly as" + proof(cases "s \<ge> start_of ly as") + case True thus "?thesis" by simp + next + case False + have "\<not> start_of ly as \<le> s" by fact + then have "Suc s - start_of ly as = 0" + by arith + then have "fetch (ci ly (start_of ly as) ins) + (Suc s - start_of ly as) b = (Nop, 0)" + by(simp add: fetch.simps) + with notfinal fetch show "?thesis" + by(simp) + qed + moreover have "s < start_of ly (Suc as)" + proof(cases "s < start_of ly (Suc as)") + case True thus "?thesis" by simp + next + case False + have h: "\<not> s < start_of ly (Suc as)" + by fact + then have "s > start_of ly as" + using abc_fetch layout + apply(simp add: start_of.simps abc_fetch.simps split: if_splits) + apply(simp add: List.take_Suc_conv_app_nth, auto) + apply(subgoal_tac "layout_of ap ! as > 0") + apply arith + apply(simp add: layout_of.simps) + apply(case_tac "ap!as", auto simp: length_of.simps) + done + from this and h have "fetch (ci ly (start_of ly as) ins) (Suc s - start_of ly as) b = (Nop, 0)" + using abc_fetch layout + apply(case_tac b, simp_all add: Suc_diff_le) + apply(case_tac [!] ins, simp_all add: start_of_Suc2 start_of_Suc1 start_of_Suc3) + apply(simp_all only: length_ci_inc length_ci_dec length_ci_goto, auto) + using layout + apply(subgoal_tac [!] "start_of ly (Suc as) = start_of ly as + 2*nat1 + 16", simp_all) + apply(rule_tac [!] start_of_Suc2, auto) + done + from fetch and notfinal this show "?thesis"by simp + qed + ultimately show "?thesis" + using assms + apply(drule_tac b= b and ins = ins in step_eq_fetch', auto) + done +qed + + lemma step_eq_in: assumes layout: "ly = layout_of ap" and compile: "tp = tm_of ap" @@ -505,21 +866,65 @@ done lemma tm_append_first_step_eq: - assumes "step (s, l, r) (A, 0) = (s', l', r')" + assumes "step (s, l, r) (A, off) = (s', l', r')" and "s' \<noteq> 0" - shows "step (s, l, r) (A @ B, 0) = (s', l', r')" + shows "step (s, l, r) (A @ B, off) = (s', l', r')" using assms apply(simp add: step.simps) -apply(case_tac "fetch A s (read r)") +apply(case_tac "fetch A (s - off) (read r)") apply(frule_tac B = B and b = "read r" in tm_append_fetch_first, auto) done lemma tm_append_first_steps_eq: - assumes "steps (s, l, r) (A, 0) stp = (s', l', r')" + assumes "steps (s, l, r) (A, off) stp = (s', l', r')" and "s' \<noteq> 0" - shows "steps (s, l, r) (A @ B, 0) stp = (s', l', r')" + shows "steps (s, l, r) (A @ B, off) stp = (s', l', r')" using assms -sorry +proof(induct stp arbitrary: s' l' r', simp add: steps.simps) + fix stp s' l' r' + assume ind: "\<And>s' l' r'. \<lbrakk>steps (s, l, r) (A, off) stp = (s', l', r'); s' \<noteq> 0\<rbrakk> + \<Longrightarrow> steps (s, l, r) (A @ B, off) stp = (s', l', r')" + and h: "steps (s, l, r) (A, off) (Suc stp) = (s', l', r')" "s' \<noteq> 0" + obtain sa la ra where a: "steps (s, l, r) (A, off) stp = (sa, la, ra)" + apply(case_tac "steps (s, l, r) (A, off) stp") by blast + hence "steps (s, l, r) (A @ B, off) stp = (sa, la, ra) \<and> sa \<noteq> 0" + using h ind[of sa la ra] + apply(case_tac sa, simp_all) + done + thus "steps (s, l, r) (A @ B, off) (Suc stp) = (s', l', r')" + using h a + apply(simp add: step_red) + apply(rule_tac tm_append_first_step_eq, simp_all) + done +qed + +lemma tm_append_second_fetch_eq: + assumes + even: "length A mod 2 = 0" + and off: "off = length A div 2" + and fetch: "fetch B s b = (ac, ns)" + and notfinal: "ns \<noteq> 0" + shows "fetch (A @ shift B off) (s + off) b = (ac, ns + off)" +using assms +apply(case_tac b) +apply(case_tac [!] s, auto simp: fetch.simps nth_append shift.simps + split: if_splits) +done + + +lemma tm_append_second_step_eq: + assumes + exec: "step0 (s, l, r) B = (s', l', r')" + and notfinal: "s' \<noteq> 0" + and off: "off = length A div 2" + and even: "length A mod 2 = 0" + shows "step0 (s + off, l, r) (A @ shift B off) = (s' + off, l', r')" +using assms +apply(simp add: step.simps) +apply(case_tac "fetch B s (read r)") +apply(frule_tac tm_append_second_fetch_eq, simp_all, auto) +done + lemma tm_append_second_steps_eq: assumes @@ -528,8 +933,90 @@ and off: "off = length A div 2" and even: "length A mod 2 = 0" shows "steps (s + off, l, r) (A @ shift B off, 0) stp = (s' + off, l', r')" +using exec notfinal +proof(induct stp arbitrary: s' l' r') + case 0 + thus "steps0 (s + off, l, r) (A @ shift B off) 0 = (s' + off, l', r')" + by(simp add: steps.simps) +next + case (Suc stp s' l' r') + have ind: "\<And>s' l' r'. \<lbrakk>steps0 (s, l, r) B stp = (s', l', r'); s' \<noteq> 0\<rbrakk> \<Longrightarrow> + steps0 (s + off, l, r) (A @ shift B off) stp = (s' + off, l', r')" + by fact + have h: "steps0 (s, l, r) B (Suc stp) = (s', l', r')" by fact + have k: "s' \<noteq> 0" by fact + obtain s'' l'' r'' where a: "steps0 (s, l, r) B stp = (s'', l'', r'')" + by (metis prod_cases3) + then have b: "s'' \<noteq> 0" + using h k + by(rule_tac notI, auto simp: step_red) + from a b have c: "steps0 (s + off, l, r) (A @ shift B off) stp = (s'' + off, l'', r'')" + by(erule_tac ind, simp) + from c b h a k assms show "?case" + thm tm_append_second_step_eq + apply(simp add: step_red) by(rule tm_append_second_step_eq, simp_all) +qed + +lemma tm_append_second_fetch0_eq: + assumes + even: "length A mod 2 = 0" + and off: "off = length A div 2" + and fetch: "fetch B s b = (ac, 0)" + and notfinal: "s \<noteq> 0" + shows "fetch (A @ shift B off) (s + off) b = (ac, 0)" using assms -sorry +apply(case_tac b) +apply(case_tac [!] s, auto simp: fetch.simps nth_append shift.simps + split: if_splits) +done + +lemma tm_append_second_halt_eq: + assumes + exec: "steps (Suc 0, l, r) (B, 0) stp = (0, l', r')" + and wf_B: "tm_wf (B, 0)" + and off: "off = length A div 2" + and even: "length A mod 2 = 0" + shows "steps (Suc off, l, r) (A @ shift B off, 0) stp = (0, l', r')" +proof - + thm before_final + have "\<exists>n. \<not> is_final (steps0 (1, l, r) B n) \<and> steps0 (1, l, r) B (Suc n) = (0, l', r')" + using exec by(rule_tac before_final, simp) + then obtain n where a: + "\<not> is_final (steps0 (1, l, r) B n) \<and> steps0 (1, l, r) B (Suc n) = (0, l', r')" .. + obtain s'' l'' r'' where b: "steps0 (1, l, r) B n = (s'', l'', r'') \<and> s'' >0" + using a + by(case_tac "steps0 (1, l, r) B n", auto) + have c: "steps (Suc 0 + off, l, r) (A @ shift B off, 0) n = (s'' + off, l'', r'')" + using a b assms + by(rule_tac tm_append_second_steps_eq, simp_all) + obtain ac where d: "fetch B s'' (read r'') = (ac, 0)" + using b a + by(case_tac "fetch B s'' (read r'')", auto simp: step_red step.simps) + then have "fetch (A @ shift B off) (s'' + off) (read r'') = (ac, 0)" + using assms b + by(rule_tac tm_append_second_fetch0_eq, simp_all) + then have e: "steps (Suc 0 + off, l, r) (A @ shift B off, 0) (Suc n) = (0, l', r')" + using a b assms c d + by(simp add: step_red step.simps) + from a have "n < stp" + using exec + proof(cases "n < stp") + case True thus "?thesis" by simp + next + case False + have "\<not> n < stp" by fact + then obtain d where "n = stp + d" + by (metis add.comm_neutral less_imp_add_positive nat_neq_iff) + thus "?thesis" + using a e exec + by(simp add: steps_add) + qed + then obtain d where "stp = Suc n + d" + by(metis add_Suc less_iff_Suc_add) + thus "?thesis" + using e + by(simp only: steps_add, simp) +qed lemma tm_append_steps: assumes @@ -555,38 +1042,2759 @@ subsection {* Crsp of Inc*} +fun at_begin_fst_bwtn :: "inc_inv_t" + where + "at_begin_fst_bwtn (as, lm) (s, l, r) ires = + (\<exists> lm1 tn rn. lm1 = (lm @ 0\<up>tn) \<and> length lm1 = s \<and> + (if lm1 = [] then l = Bk # Bk # ires + else l = [Bk]@<rev lm1>@Bk#Bk#ires) \<and> r = Bk\<up>rn)" + + +fun at_begin_fst_awtn :: "inc_inv_t" + where + "at_begin_fst_awtn (as, lm) (s, l, r) ires = + (\<exists> lm1 tn rn. lm1 = (lm @ 0\<up>tn) \<and> length lm1 = s \<and> + (if lm1 = [] then l = Bk # Bk # ires + else l = [Bk]@<rev lm1>@Bk#Bk#ires) \<and> r = [Oc]@Bk\<up>rn)" + +fun at_begin_norm :: "inc_inv_t" + where + "at_begin_norm (as, lm) (s, l, r) ires= + (\<exists> lm1 lm2 rn. lm = lm1 @ lm2 \<and> length lm1 = s \<and> + (if lm1 = [] then l = Bk # Bk # ires + else l = Bk # <rev lm1> @ Bk # Bk # ires ) \<and> r = <lm2>@Bk\<up>rn)" + +fun in_middle :: "inc_inv_t" + where + "in_middle (as, lm) (s, l, r) ires = + (\<exists> lm1 lm2 tn m ml mr rn. lm @ 0\<up>tn = lm1 @ [m] @ lm2 + \<and> length lm1 = s \<and> m + 1 = ml + mr \<and> + ml \<noteq> 0 \<and> tn = s + 1 - length lm \<and> + (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires + else l = Oc\<up>ml@[Bk]@<rev lm1>@ + Bk # Bk # ires) \<and> (r = Oc\<up>mr @ [Bk] @ <lm2>@ Bk\<up>rn \<or> + (lm2 = [] \<and> r = Oc\<up>mr)) + )" + +fun inv_locate_a :: "inc_inv_t" + where "inv_locate_a (as, lm) (s, l, r) ires = + (at_begin_norm (as, lm) (s, l, r) ires \<or> + at_begin_fst_bwtn (as, lm) (s, l, r) ires \<or> + at_begin_fst_awtn (as, lm) (s, l, r) ires + )" + +fun inv_locate_b :: "inc_inv_t" + where "inv_locate_b (as, lm) (s, l, r) ires = + (in_middle (as, lm) (s, l, r)) ires " + +fun inv_after_write :: "inc_inv_t" + where "inv_after_write (as, lm) (s, l, r) ires = + (\<exists> rn m lm1 lm2. lm = lm1 @ m # lm2 \<and> + (if lm1 = [] then l = Oc\<up>m @ Bk # Bk # ires + else Oc # l = Oc\<up>Suc m@ Bk # <rev lm1> @ + Bk # Bk # ires) \<and> r = [Oc] @ <lm2> @ Bk\<up>rn)" + +fun inv_after_move :: "inc_inv_t" + where "inv_after_move (as, lm) (s, l, r) ires = + (\<exists> rn m lm1 lm2. lm = lm1 @ m # lm2 \<and> + (if lm1 = [] then l = Oc\<up>Suc m @ Bk # Bk # ires + else l = Oc\<up>Suc m@ Bk # <rev lm1> @ Bk # Bk # ires) \<and> + r = <lm2> @ Bk\<up>rn)" + +fun inv_after_clear :: "inc_inv_t" + where "inv_after_clear (as, lm) (s, l, r) ires = + (\<exists> rn m lm1 lm2 r'. lm = lm1 @ m # lm2 \<and> + (if lm1 = [] then l = Oc\<up>Suc m @ Bk # Bk # ires + else l = Oc\<up>Suc m @ Bk # <rev lm1> @ Bk # Bk # ires) \<and> + r = Bk # r' \<and> Oc # r' = <lm2> @ Bk\<up>rn)" + +fun inv_on_right_moving :: "inc_inv_t" + where "inv_on_right_moving (as, lm) (s, l, r) ires = + (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> + ml + mr = m \<and> + (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires + else l = Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> + ((r = Oc\<up>mr @ [Bk] @ <lm2> @ Bk\<up>rn) \<or> + (r = Oc\<up>mr \<and> lm2 = [])))" + +fun inv_on_left_moving_norm :: "inc_inv_t" + where "inv_on_left_moving_norm (as, lm) (s, l, r) ires = + (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> + ml + mr = Suc m \<and> mr > 0 \<and> (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires + else l = Oc\<up>ml @ Bk # <rev lm1> @ Bk # Bk # ires) + \<and> (r = Oc\<up>mr @ Bk # <lm2> @ Bk\<up>rn \<or> + (lm2 = [] \<and> r = Oc\<up>mr)))" + +fun inv_on_left_moving_in_middle_B:: "inc_inv_t" + where "inv_on_left_moving_in_middle_B (as, lm) (s, l, r) ires = + (\<exists> lm1 lm2 rn. lm = lm1 @ lm2 \<and> + (if lm1 = [] then l = Bk # ires + else l = <rev lm1> @ Bk # Bk # ires) \<and> + r = Bk # <lm2> @ Bk\<up>rn)" + +fun inv_on_left_moving :: "inc_inv_t" + where "inv_on_left_moving (as, lm) (s, l, r) ires = + (inv_on_left_moving_norm (as, lm) (s, l, r) ires \<or> + inv_on_left_moving_in_middle_B (as, lm) (s, l, r) ires)" + + +fun inv_check_left_moving_on_leftmost :: "inc_inv_t" + where "inv_check_left_moving_on_leftmost (as, lm) (s, l, r) ires = + (\<exists> rn. l = ires \<and> r = [Bk, Bk] @ <lm> @ Bk\<up>rn)" + +fun inv_check_left_moving_in_middle :: "inc_inv_t" + where "inv_check_left_moving_in_middle (as, lm) (s, l, r) ires = + (\<exists> lm1 lm2 r' rn. lm = lm1 @ lm2 \<and> + (Oc # l = <rev lm1> @ Bk # Bk # ires) \<and> r = Oc # Bk # r' \<and> + r' = <lm2> @ Bk\<up>rn)" + +fun inv_check_left_moving :: "inc_inv_t" + where "inv_check_left_moving (as, lm) (s, l, r) ires = + (inv_check_left_moving_on_leftmost (as, lm) (s, l, r) ires \<or> + inv_check_left_moving_in_middle (as, lm) (s, l, r) ires)" + +fun inv_after_left_moving :: "inc_inv_t" + where "inv_after_left_moving (as, lm) (s, l, r) ires= + (\<exists> rn. l = Bk # ires \<and> r = Bk # <lm> @ Bk\<up>rn)" + +fun inv_stop :: "inc_inv_t" + where "inv_stop (as, lm) (s, l, r) ires= + (\<exists> rn. l = Bk # Bk # ires \<and> r = <lm> @ Bk\<up>rn)" + + +lemma halt_lemma2': + "\<lbrakk>wf LE; \<forall> n. ((\<not> P (f n) \<and> Q (f n)) \<longrightarrow> + (Q (f (Suc n)) \<and> (f (Suc n), (f n)) \<in> LE)); Q (f 0)\<rbrakk> + \<Longrightarrow> \<exists> n. P (f n)" +apply(intro exCI, simp) +apply(subgoal_tac "\<forall> n. Q (f n)", simp) +apply(drule_tac f = f in wf_inv_image) +apply(simp add: inv_image_def) +apply(erule wf_induct, simp) +apply(erule_tac x = x in allE) +apply(erule_tac x = n in allE, erule_tac x = n in allE) +apply(erule_tac x = "Suc x" in allE, simp) +apply(rule_tac allI) +apply(induct_tac n, simp) +apply(erule_tac x = na in allE, simp) +done + +lemma halt_lemma2'': + "\<lbrakk>P (f n); \<not> P (f (0::nat))\<rbrakk> \<Longrightarrow> + \<exists> n. (P (f n) \<and> (\<forall> i < n. \<not> P (f i)))" +apply(induct n rule: nat_less_induct, auto) +done + +lemma halt_lemma2''': + "\<lbrakk>\<forall>n. \<not> P (f n) \<and> Q (f n) \<longrightarrow> Q (f (Suc n)) \<and> (f (Suc n), f n) \<in> LE; + Q (f 0); \<forall>i<na. \<not> P (f i)\<rbrakk> \<Longrightarrow> Q (f na)" +apply(induct na, simp, simp) +done + +lemma halt_lemma2: + "\<lbrakk>wf LE; + Q (f 0); \<not> P (f 0); + \<forall> n. ((\<not> P (f n) \<and> Q (f n)) \<longrightarrow> (Q (f (Suc n)) \<and> (f (Suc n), (f n)) \<in> LE))\<rbrakk> + \<Longrightarrow> \<exists> n. P (f n) \<and> Q (f n)" +apply(insert halt_lemma2' [of LE P f Q], simp, erule_tac exE) +apply(subgoal_tac "\<exists> n. (P (f n) \<and> (\<forall> i < n. \<not> P (f i)))") +apply(erule_tac exE)+ +apply(rule_tac x = na in exI, auto) +apply(rule halt_lemma2''', simp, simp, simp) +apply(erule_tac halt_lemma2'', simp) +done + + +fun findnth_inv :: "layout \<Rightarrow> nat \<Rightarrow> inc_inv_t" + where + "findnth_inv ly n (as, lm) (s, l, r) ires = + (if s = 0 then False + else if s \<le> Suc (2*n) then + if s mod 2 = 1 then inv_locate_a (as, lm) ((s - 1) div 2, l, r) ires + else inv_locate_b (as, lm) ((s - 1) div 2, l, r) ires + else False)" + + +fun findnth_state :: "config \<Rightarrow> nat \<Rightarrow> nat" + where + "findnth_state (s, l, r) n = (Suc (2*n) - s)" + +fun findnth_step :: "config \<Rightarrow> nat \<Rightarrow> nat" + where + "findnth_step (s, l, r) n = + (if s mod 2 = 1 then + (if (r \<noteq> [] \<and> hd r = Oc) then 0 + else 1) + else length r)" + +fun findnth_measure :: "config \<times> nat \<Rightarrow> nat \<times> nat" + where + "findnth_measure (c, n) = + (findnth_state c n, findnth_step c n)" + +definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set" + where + "lex_pair \<equiv> less_than <*lex*> less_than" + +definition findnth_LE :: "((config \<times> nat) \<times> (config \<times> nat)) set" + where + "findnth_LE \<equiv> (inv_image lex_pair findnth_measure)" + +lemma wf_findnth_LE: "wf findnth_LE" +by(auto intro:wf_inv_image simp: findnth_LE_def lex_pair_def) + +declare findnth_inv.simps[simp del] + +lemma [simp]: + "\<lbrakk>x < Suc (Suc (2 * n)); Suc x mod 2 = Suc 0; \<not> x < 2 * n\<rbrakk> + \<Longrightarrow> x = 2*n" +by arith + +lemma [simp]: + "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 = Suc 0\<rbrakk> + \<Longrightarrow> fetch (findnth n) a Bk = (W1, a)" +apply(case_tac a, simp_all) +apply(induct n, auto simp: findnth.simps length_findnth nth_append) +apply arith +done + +lemma [simp]: + "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 = Suc 0\<rbrakk> + \<Longrightarrow> fetch (findnth n) a Oc = (R, Suc a)" +apply(case_tac a, simp_all) +apply(induct n, auto simp: findnth.simps length_findnth nth_append) +apply(subgoal_tac "nat = 2 * n", simp) +by arith + +lemma [simp]: + "\<lbrakk>0 < a; a < Suc (2*n); a mod 2 \<noteq> Suc 0\<rbrakk> + \<Longrightarrow> fetch (findnth n) a Oc = (R, a)" +apply(case_tac a, simp_all) +apply(induct n, auto simp: findnth.simps length_findnth nth_append) +apply(subgoal_tac "nat = Suc (2 * n)", simp) +apply arith +done + +lemma [simp]: + "\<lbrakk>0 < a; a < Suc (2*n); a mod 2 \<noteq> Suc 0\<rbrakk> + \<Longrightarrow> fetch (findnth n) a Bk = (R, Suc a)" +apply(case_tac a, simp_all) +apply(induct n, auto simp: findnth.simps length_findnth nth_append) +apply(subgoal_tac "nat = Suc (2 * n)", simp) +by arith + +declare at_begin_norm.simps[simp del] at_begin_fst_bwtn.simps[simp del] + at_begin_fst_awtn.simps[simp del] in_middle.simps[simp del] + abc_lm_s.simps[simp del] abc_lm_v.simps[simp del] + ci.simps[simp del] inv_after_move.simps[simp del] + inv_on_left_moving_norm.simps[simp del] + inv_on_left_moving_in_middle_B.simps[simp del] + inv_after_clear.simps[simp del] + inv_after_write.simps[simp del] inv_on_left_moving.simps[simp del] + inv_on_right_moving.simps[simp del] + inv_check_left_moving.simps[simp del] + inv_check_left_moving_in_middle.simps[simp del] + inv_check_left_moving_on_leftmost.simps[simp del] + inv_after_left_moving.simps[simp del] + inv_stop.simps[simp del] inv_locate_a.simps[simp del] + inv_locate_b.simps[simp del] + +lemma [intro]: "\<exists>rn. [Bk] = Bk \<up> rn" +apply(rule_tac x = "Suc 0" in exI, simp) +done + +lemma [intro]: "at_begin_norm (as, am) (q, aaa, []) ires + \<Longrightarrow> at_begin_norm (as, am) (q, aaa, [Bk]) ires" +apply(simp add: at_begin_norm.simps, erule_tac exE, erule_tac exE) +apply(rule_tac x = lm1 in exI, simp, auto) +done + +lemma [intro]: "at_begin_fst_bwtn (as, am) (q, aaa, []) ires + \<Longrightarrow> at_begin_fst_bwtn (as, am) (q, aaa, [Bk]) ires" +apply(simp only: at_begin_fst_bwtn.simps, erule_tac exE, erule_tac exE, erule_tac exE) +apply(rule_tac x = "am @ 0\<up>tn" in exI, auto) +done + +lemma [intro]: "at_begin_fst_awtn (as, am) (q, aaa, []) ires + \<Longrightarrow> at_begin_fst_awtn (as, am) (q, aaa, [Bk]) ires" +apply(auto simp: at_begin_fst_awtn.simps) +done + +lemma [intro]: "inv_locate_a (as, am) (q, aaa, []) ires + \<Longrightarrow> inv_locate_a (as, am) (q, aaa, [Bk]) ires" +apply(simp only: inv_locate_a.simps) +apply(erule disj_forward) +defer +apply(erule disj_forward, auto) +done + +lemma tape_of_nl_cons: "<m # lm> = (if lm = [] then Oc\<up>(Suc m) + else Oc\<up>(Suc m) @ Bk # <lm>)" +apply(case_tac lm, simp_all add: tape_of_nl_abv split: if_splits) +done + + +lemma locate_a_2_locate_a[simp]: "inv_locate_a (as, am) (q, aaa, Bk # xs) ires + \<Longrightarrow> inv_locate_a (as, am) (q, aaa, Oc # xs) ires" +apply(simp only: inv_locate_a.simps at_begin_norm.simps + at_begin_fst_bwtn.simps at_begin_fst_awtn.simps) +apply(erule_tac disjE, erule exE, erule exE, erule exE, + rule disjI2, rule disjI2) +defer +apply(erule_tac disjE, erule exE, erule exE, + erule exE, rule disjI2, rule disjI2) +prefer 2 +apply(simp) +proof- + fix lm1 tn rn + assume k: "lm1 = am @ 0\<up>tn \<and> length lm1 = q \<and> (if lm1 = [] then aaa = Bk # Bk # + ires else aaa = [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> Bk # xs = Bk\<up>rn" + thus "\<exists>lm1 tn rn. lm1 = am @ 0 \<up> tn \<and> length lm1 = q \<and> + (if lm1 = [] then aaa = Bk # Bk # ires else aaa = [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> Oc # xs = [Oc] @ Bk \<up> rn" + (is "\<exists>lm1 tn rn. ?P lm1 tn rn") + proof - + from k have "?P lm1 tn (rn - 1)" + apply(auto simp: Oc_def) + by(case_tac [!] "rn::nat", auto) + thus ?thesis by blast + qed +next + fix lm1 lm2 rn + assume h1: "am = lm1 @ lm2 \<and> length lm1 = q \<and> (if lm1 = [] + then aaa = Bk # Bk # ires else aaa = Bk # <rev lm1> @ Bk # Bk # ires) \<and> + Bk # xs = <lm2> @ Bk\<up>rn" + from h1 have h2: "lm2 = []" + apply(auto split: if_splits) + apply(case_tac [!] lm2, simp_all add: tape_of_nl_cons split: if_splits) + done + from h1 and h2 show "\<exists>lm1 tn rn. lm1 = am @ 0\<up>tn \<and> length lm1 = q \<and> + (if lm1 = [] then aaa = Bk # Bk # ires else aaa = [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> + Oc # xs = [Oc] @ Bk\<up>rn" + (is "\<exists>lm1 tn rn. ?P lm1 tn rn") + proof - + from h1 and h2 have "?P lm1 0 (rn - 1)" + apply(auto simp: Oc_def + tape_of_nl_abv tape_of_nat_list.simps) + by(case_tac "rn::nat", simp, simp) + thus ?thesis by blast + qed +qed + +lemma [simp]: "inv_locate_a (as, am) (q, aaa, []) ires \<Longrightarrow> + inv_locate_a (as, am) (q, aaa, [Oc]) ires" +apply(insert locate_a_2_locate_a [of as am q aaa "[]"]) +apply(subgoal_tac "inv_locate_a (as, am) (q, aaa, [Bk]) ires", auto) +done + +(*inv: from locate_b to locate_b*) +lemma [simp]: "inv_locate_b (as, am) (q, aaa, Oc # xs) ires + \<Longrightarrow> inv_locate_b (as, am) (q, Oc # aaa, xs) ires" +apply(simp only: inv_locate_b.simps in_middle.simps) +apply(erule exE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = tn in exI, rule_tac x = m in exI) +apply(rule_tac x = "Suc ml" in exI, rule_tac x = "mr - 1" in exI, + rule_tac x = rn in exI) +apply(case_tac mr, simp_all, auto) +done + +(* +lemma zero_and_nil[intro]: "(Bk # Bk\<^bsup>n\<^esup> = Oc\<^bsup>mr\<^esup> @ Bk # <lm::nat list> @ + Bk\<^bsup>rn \<^esup>) \<or> (lm2 = [] \<and> Bk # Bk\<^bsup>n\<^esup> = Oc\<^bsup>mr\<^esup>) + \<Longrightarrow> mr = 0 \<and> lm = []" +apply(rule context_conjI) +apply(case_tac mr, auto simp:exponent_def) +apply(insert BkCons_nil[of "replicate (n - 1) Bk" lm rn]) +apply(case_tac n, auto simp: exponent_def Bk_def tape_of_nl_nil_eq) +done + +lemma tape_of_nat_def: "<[m::nat]> = Oc # Oc\<^bsup>m\<^esup>" +apply(simp add: tape_of_nl_abv tape_of_nat_list.simps) +done +*) +lemma [simp]: "<[x::nat]> = Oc\<up>(Suc x)" +apply(simp add: tape_of_nat_abv tape_of_nl_abv) +done + +lemma [simp]: " <([]::nat list)> = []" +apply(simp add: tape_of_nl_abv) +done + +lemma [simp]: "\<lbrakk>inv_locate_b (as, am) (q, aaa, Bk # xs) ires; \<exists>n. xs = Bk\<up>n\<rbrakk> + \<Longrightarrow> inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires" +apply(simp add: inv_locate_b.simps inv_locate_a.simps) +apply(rule_tac disjI2, rule_tac disjI1) +apply(simp only: in_middle.simps at_begin_fst_bwtn.simps) +apply(erule_tac exE)+ +apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = tn in exI, simp split: if_splits) +apply(case_tac mr, simp_all) +apply(case_tac "length am", simp_all, case_tac tn, simp_all) +apply(case_tac lm2, simp_all add: tape_of_nl_cons split: if_splits) +apply(case_tac am, simp_all) +apply(case_tac n, simp_all) +apply(case_tac n, simp_all) +apply(case_tac mr, simp_all) +apply(case_tac lm2, simp_all add: tape_of_nl_cons split: if_splits, auto) +apply(case_tac [!] n, simp_all) +done + +lemma [simp]: "(Oc # r = Bk \<up> rn) = False" +apply(case_tac rn, simp_all) +done + +lemma [simp]: "(\<exists>rna. Bk \<up> rn = Bk # Bk \<up> rna) \<or> rn = 0" +apply(case_tac rn, auto) +done + +lemma [simp]: "(\<forall> x. a \<noteq> x) = False" +by auto + +lemma exp_ind: "a\<up>(Suc x) = a\<up>x @ [a]" +apply(induct x, auto) +done + +lemma [simp]: + "inv_locate_a (as, lm) (q, l, Oc # r) ires + \<Longrightarrow> inv_locate_b (as, lm) (q, Oc # l, r) ires" +apply(simp only: inv_locate_a.simps inv_locate_b.simps in_middle.simps + at_begin_norm.simps at_begin_fst_bwtn.simps + at_begin_fst_awtn.simps) +apply(erule disjE, erule exE, erule exE, erule exE) +apply(rule_tac x = lm1 in exI, rule_tac x = "tl lm2" in exI, simp) +apply(rule_tac x = 0 in exI, rule_tac x = "hd lm2" in exI) +apply(case_tac lm2, auto simp: tape_of_nl_cons ) +apply(rule_tac x = 1 in exI, rule_tac x = a in exI, auto) +apply(case_tac list, simp_all) +apply(case_tac rn, simp_all) +apply(rule_tac x = "lm @ replicate tn 0" in exI, + rule_tac x = "[]" in exI, + rule_tac x = "Suc tn" in exI, + rule_tac x = 0 in exI, auto) +apply(simp only: replicate_Suc[THEN sym] exp_ind) +apply(rule_tac x = "Suc 0" in exI, auto) +done + +lemma length_equal: "xs = ys \<Longrightarrow> length xs = length ys" +by auto + +lemma [simp]: "\<lbrakk>inv_locate_b (as, am) (q, aaa, Bk # xs) ires; + \<not> (\<exists>n. xs = Bk\<up>n)\<rbrakk> + \<Longrightarrow> inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires" +apply(simp add: inv_locate_b.simps inv_locate_a.simps) +apply(rule_tac disjI1) +apply(simp only: in_middle.simps at_begin_norm.simps) +apply(erule_tac exE)+ +apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = lm2 in exI, simp) +apply(subgoal_tac "tn = 0", simp , auto split: if_splits) +apply(case_tac [!] mr, simp_all, auto) +apply(simp add: tape_of_nl_cons) +apply(drule_tac length_equal, simp) +apply(case_tac "length am", simp_all, erule_tac x = rn in allE, simp) +apply(drule_tac length_equal, simp) +apply(case_tac "(Suc (length lm1) - length am)", simp_all) +apply(case_tac lm2, simp, simp) +done + +lemma locate_b_2_a[intro]: + "inv_locate_b (as, am) (q, aaa, Bk # xs) ires + \<Longrightarrow> inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires" +apply(case_tac "\<exists> n. xs = Bk\<up>n", simp, simp) +done + + +lemma [simp]: "inv_locate_b (as, am) (q, l, []) ires + \<Longrightarrow> inv_locate_b (as, am) (q, l, [Bk]) ires" +apply(simp only: inv_locate_b.simps in_middle.simps) +apply(erule exE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = tn in exI, rule_tac x = m in exI, + rule_tac x = ml in exI, rule_tac x = mr in exI) +apply(auto) +done + +(*inv: from locate_b to after_write*) + +lemma [simp]: "(a mod 2 \<noteq> Suc 0) = (a mod 2 = 0) " +by arith + +lemma [simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 0) " +by arith + +lemma mod_ex1: "(a mod 2 = Suc 0) = (\<exists> q. a = Suc (2 * q))" +by arith + +lemma mod_ex2: "(a mod (2::nat) = 0) = (\<exists> q. a = 2 * q)" +by arith + +lemma [simp]: "(2*q - Suc 0) div 2 = (q - 1)" +by arith + +lemma [simp]: "(Suc (2*q)) div 2 = q" +by arith + +lemma mod_2: "x mod 2 = 0 \<or> x mod 2 = Suc 0" +by arith + +lemma [simp]: "x mod 2 = 0 \<Longrightarrow> Suc x mod 2 = Suc 0" +by arith + +lemma [simp]: "x mod 2 = Suc 0 \<Longrightarrow> Suc x mod 2 = 0" +by arith + +lemma [simp]: "inv_locate_b (as, am) (q, l, []) ires + \<Longrightarrow> inv_locate_b (as, am) (q, l, [Bk]) ires" +apply(simp only: inv_locate_b.simps in_middle.simps) +apply(erule exE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = tn in exI, rule_tac x = m in exI, + rule_tac x = ml in exI, rule_tac x = mr in exI) +apply(auto) +done + +lemma locate_b_2_locate_a[simp]: + "\<lbrakk>q > 0; inv_locate_b (as, am) (q - Suc 0, aaa, Bk # xs) ires\<rbrakk> + \<Longrightarrow> inv_locate_a (as, am) (q, Bk # aaa, xs) ires" +apply(insert locate_b_2_a [of as am "q - 1" aaa xs ires], simp) +done + + +lemma [simp]: "inv_locate_b (as, am) (q, l, []) ires + \<Longrightarrow> inv_locate_b (as, am) (q, l, [Bk]) ires" +apply(simp only: inv_locate_b.simps in_middle.simps) +apply(erule exE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = tn in exI, rule_tac x = m in exI, + rule_tac x = ml in exI, rule_tac x = mr in exI) +apply(auto) +done + +(*inv: from locate_b to after_write*) + +lemma [simp]: + "crsp (layout_of ap) (as, lm) (s, l, r) ires + \<Longrightarrow> findnth_inv (layout_of ap) n (as, lm) (Suc 0, l, r) ires" +apply(auto simp: crsp.simps findnth_inv.simps inv_locate_a.simps + at_begin_norm.simps at_begin_fst_awtn.simps at_begin_fst_bwtn.simps) +done + +lemma findnth_correct_pre: + assumes layout: "ly = layout_of ap" + and crsp: "crsp ly (as, lm) (s, l, r) ires" + and not0: "n > 0" + and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (findnth n, 0) stp, n))" + and P: "P = (\<lambda> ((s, l, r), n). s = Suc (2 * n))" + and Q: "Q = (\<lambda> ((s, l, r), n). findnth_inv ly n (as, lm) (s, l, r) ires)" + shows "\<exists> stp. P (f stp) \<and> Q (f stp)" +thm halt_lemma2 +proof(rule_tac LE = findnth_LE in halt_lemma2) + show "wf findnth_LE" by(intro wf_findnth_LE) +next + show "Q (f 0)" + using crsp layout + apply(simp add: f P Q steps.simps) + done +next + show "\<not> P (f 0)" + using not0 + apply(simp add: f P steps.simps) + done +next + show "\<forall>n. \<not> P (f n) \<and> Q (f n) \<longrightarrow> Q (f (Suc n)) \<and> (f (Suc n), f n) + \<in> findnth_LE" + proof(rule_tac allI, rule_tac impI, simp add: f, + case_tac "steps (Suc 0, l, r) (findnth n, 0) na", simp add: P) + fix na a b c + assume "a \<noteq> Suc (2 * n) \<and> Q ((a, b, c), n)" + thus "Q (step (a, b, c) (findnth n, 0), n) \<and> + ((step (a, b, c) (findnth n, 0), n), (a, b, c), n) \<in> findnth_LE" + apply(case_tac c, case_tac [2] aa) + apply(simp_all add: step.simps findnth_LE_def Q findnth_inv.simps mod_2 lex_pair_def split: if_splits) + apply(auto simp: mod_ex1 mod_ex2) + done + qed +qed + +lemma [intro]: "inv_locate_a (as, lm) (0, Bk # Bk # ires, <lm> @ Bk \<up> x) ires" +apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps) +done +lemma [simp]: "crsp ly (as, lm) (s, l, r) ires \<Longrightarrow> inv_locate_a (as, lm) (0, l, r) ires" +apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps) +done + +lemma findnth_correct: + assumes layout: "ly = layout_of ap" + and crsp: "crsp ly (as, lm) (s, l, r) ires" + shows "\<exists> stp l' r'. steps (Suc 0, l, r) (findnth n, 0) stp = (Suc (2 * n), l', r') + \<and> inv_locate_a (as, lm) (n, l', r') ires" + using crsp + apply(case_tac "n = 0") + apply(rule_tac x = 0 in exI, auto simp: steps.simps) + using assms + apply(drule_tac findnth_correct_pre, auto) + apply(rule_tac x = stp in exI, simp add: findnth_inv.simps) + done + + +fun inc_inv :: "nat \<Rightarrow> inc_inv_t" + where + "inc_inv n (as, lm) (s, l, r) ires = + (let lm' = abc_lm_s lm n (Suc (abc_lm_v lm n)) in + if s = 0 then False + else if s = 1 then + inv_locate_a (as, lm) (n, l, r) ires + else if s = 2 then + inv_locate_b (as, lm) (n, l, r) ires + else if s = 3 then + inv_after_write (as, lm') (s, l, r) ires + else if s = Suc 3 then + inv_after_move (as, lm') (s, l, r) ires + else if s = Suc 4 then + inv_after_clear (as, lm') (s, l, r) ires + else if s = Suc (Suc 4) then + inv_on_right_moving (as, lm') (s, l, r) ires + else if s = Suc (Suc 5) then + inv_on_left_moving (as, lm') (s, l, r) ires + else if s = Suc (Suc (Suc 5)) then + inv_check_left_moving (as, lm') (s, l, r) ires + else if s = Suc (Suc (Suc (Suc 5))) then + inv_after_left_moving (as, lm') (s, l, r) ires + else if s = Suc (Suc (Suc (Suc (Suc 5)))) then + inv_stop (as, lm') (s, l, r) ires + else False)" + + +fun abc_inc_stage1 :: "config \<Rightarrow> nat" + where + "abc_inc_stage1 (s, l, r) = + (if s = 0 then 0 + else if s \<le> 2 then 5 + else if s \<le> 6 then 4 + else if s \<le> 8 then 3 + else if s = 9 then 2 + else 1)" + +fun abc_inc_stage2 :: "config \<Rightarrow> nat" + where + "abc_inc_stage2 (s, l, r) = + (if s = 1 then 2 + else if s = 2 then 1 + else if s = 3 then length r + else if s = 4 then length r + else if s = 5 then length r + else if s = 6 then + if r \<noteq> [] then length r + else 1 + else if s = 7 then length l + else if s = 8 then length l + else 0)" + +fun abc_inc_stage3 :: "config \<Rightarrow> nat" + where + "abc_inc_stage3 (s, l, r) = ( + if s = 4 then 4 + else if s = 5 then 3 + else if s = 6 then + if r \<noteq> [] \<and> hd r = Oc then 2 + else 1 + else if s = 3 then 0 + else if s = 2 then length r + else if s = 1 then + if (r \<noteq> [] \<and> hd r = Oc) then 0 + else 1 + else 10 - s)" + + +definition inc_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat" + where + "inc_measure c = + (abc_inc_stage1 c, abc_inc_stage2 c, abc_inc_stage3 c)" + +definition lex_triple :: + "((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set" + where "lex_triple \<equiv> less_than <*lex*> lex_pair" + +definition inc_LE :: "(config \<times> config) set" + where + "inc_LE \<equiv> (inv_image lex_triple inc_measure)" + +declare inc_inv.simps[simp del] + +lemma wf_inc_le[intro]: "wf inc_LE" +by(auto intro:wf_inv_image simp: inc_LE_def lex_triple_def lex_pair_def) + +lemma numeral_5_eq_5: "5 = Suc (Suc (Suc (Suc (Suc 0))))" +by arith + +lemma numeral_6_eq_6: "6 = Suc (Suc (Suc (Suc (Suc 1))))" +by arith + +lemma numeral_7_eq_7: "7 = Suc (Suc (Suc (Suc (Suc 2))))" +by arith + +lemma numeral_8_eq_8: "8 = Suc (Suc (Suc (Suc (Suc 3))))" +by arith + +lemma numeral_9_eq_9: "9 = Suc (Suc (Suc (Suc (Suc (Suc 3)))))" +by arith + +lemma numeral_10_eq_10: "10 = Suc (Suc (Suc (Suc (Suc (Suc (Suc 3))))))" +by arith + +lemma inv_locate_b_2_after_write[simp]: + "inv_locate_b (as, am) (n, aaa, Bk # xs) ires + \<Longrightarrow> inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) + (s, aaa, Oc # xs) ires" +apply(auto simp: in_middle.simps inv_after_write.simps + abc_lm_v.simps abc_lm_s.simps inv_locate_b.simps) +apply(case_tac [!] mr, auto split: if_splits) +apply(rule_tac x = rn in exI, rule_tac x = "Suc m" in exI, + rule_tac x = "lm1" in exI, simp) +apply(rule_tac x = "lm2" in exI, simp) +apply(simp only: Suc_diff_le exp_ind) +apply(subgoal_tac "lm2 = []", simp) +apply(drule_tac length_equal, simp) +done + +lemma [simp]: "inv_locate_b (as, am) (n, aaa, []) ires \<Longrightarrow> + inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) + (s, aaa, [Oc]) ires" +apply(insert inv_locate_b_2_after_write [of as am n aaa "[]"]) +by(simp) + + + +(*inv: from after_write to after_move*) +lemma [simp]: "inv_after_write (as, lm) (x, l, Oc # r) ires + \<Longrightarrow> inv_after_move (as, lm) (y, Oc # l, r) ires" +apply(auto simp:inv_after_move.simps inv_after_write.simps split: if_splits) +done + +lemma [simp]: "inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n) + )) (x, aaa, Bk # xs) ires = False" +apply(simp add: inv_after_write.simps ) +done + +lemma [simp]: + "inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) + (x, aaa, []) ires = False" +apply(simp add: inv_after_write.simps ) +done + +(*inv: from after_move to after_clear*) +lemma [simp]: "inv_after_move (as, lm) (s, l, Oc # r) ires + \<Longrightarrow> inv_after_clear (as, lm) (s', l, Bk # r) ires" +apply(auto simp: inv_after_move.simps inv_after_clear.simps split: if_splits) +done + +(*inv: from after_move to on_leftmoving*) +lemma [intro]: "Bk \<up> rn = Bk # Bk \<up> (rn - Suc 0) \<or> rn = 0" +apply(case_tac rn, auto) +done + +lemma inv_after_move_2_inv_on_left_moving[simp]: + "inv_after_move (as, lm) (s, l, Bk # r) ires + \<Longrightarrow> (l = [] \<longrightarrow> + inv_on_left_moving (as, lm) (s', [], Bk # Bk # r) ires) \<and> + (l \<noteq> [] \<longrightarrow> + inv_on_left_moving (as, lm) (s', tl l, hd l # Bk # r) ires)" +apply(simp only: inv_after_move.simps inv_on_left_moving.simps) +apply(subgoal_tac "l \<noteq> []", rule conjI, simp, rule impI, + rule disjI1, simp only: inv_on_left_moving_norm.simps) +apply(erule exE)+ +apply(subgoal_tac "lm2 = []") +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = m in exI, rule_tac x = m in exI, + rule_tac x = 1 in exI, + rule_tac x = "rn - 1" in exI, auto) +apply(auto split: if_splits) +apply(case_tac [1-2] rn, simp_all) +apply(case_tac [!] lm2, simp_all add: tape_of_nl_cons split: if_splits) +done + + +lemma inv_after_move_2_inv_on_left_moving_B[simp]: + "inv_after_move (as, lm) (s, l, []) ires + \<Longrightarrow> (l = [] \<longrightarrow> inv_on_left_moving (as, lm) (s', [], [Bk]) ires) \<and> + (l \<noteq> [] \<longrightarrow> inv_on_left_moving (as, lm) (s', tl l, [hd l]) ires)" +apply(simp only: inv_after_move.simps inv_on_left_moving.simps) +apply(subgoal_tac "l \<noteq> []", rule conjI, simp, rule impI, rule disjI1, + simp only: inv_on_left_moving_norm.simps) +apply(erule exE)+ +apply(subgoal_tac "lm2 = []") +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = m in exI, rule_tac x = m in exI, + rule_tac x = 1 in exI, rule_tac x = "rn - 1" in exI, simp, case_tac rn) +apply(auto split: if_splits) +apply(case_tac [!] lm2, auto simp: tape_of_nl_cons split: if_splits) +done + +(*inv: from after_clear to on_right_moving*) +lemma [simp]: "Oc # r = replicate rn Bk = False" +apply(case_tac rn, simp, simp) +done + +lemma inv_after_clear_2_inv_on_right_moving[simp]: + "inv_after_clear (as, lm) (x, l, Bk # r) ires + \<Longrightarrow> inv_on_right_moving (as, lm) (y, Bk # l, r) ires" +apply(auto simp: inv_after_clear.simps inv_on_right_moving.simps ) +apply(subgoal_tac "lm2 \<noteq> []") +apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = "tl lm2" in exI, + rule_tac x = "hd lm2" in exI, simp) +apply(rule_tac x = 0 in exI, rule_tac x = "hd lm2" in exI) +apply(simp, rule conjI) +apply(case_tac [!] "lm2::nat list", auto) +apply(case_tac rn, auto split: if_splits simp: tape_of_nl_cons) +apply(case_tac [!] rn, simp_all) +done + +lemma [simp]: "inv_after_clear (as, lm) (x, l, []) ires\<Longrightarrow> + inv_after_clear (as, lm) (y, l, [Bk]) ires" +by(auto simp: inv_after_clear.simps) + +lemma [simp]: "inv_after_clear (as, lm) (x, l, []) ires + \<Longrightarrow> inv_on_right_moving (as, lm) (y, Bk # l, []) ires" +by(insert + inv_after_clear_2_inv_on_right_moving[of as lm n l "[]"], simp) + +(*inv: from on_right_moving to on_right_movign*) +lemma [simp]: "inv_on_right_moving (as, lm) (x, l, Oc # r) ires + \<Longrightarrow> inv_on_right_moving (as, lm) (y, Oc # l, r) ires" +apply(auto simp: inv_on_right_moving.simps) +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = "ml + mr" in exI, simp) +apply(rule_tac x = "Suc ml" in exI, + rule_tac x = "mr - 1" in exI, simp) +apply(case_tac mr, auto) +apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, + rule_tac x = "ml + mr" in exI, simp) +apply(rule_tac x = "Suc ml" in exI, + rule_tac x = "mr - 1" in exI, simp) +apply(case_tac mr, auto split: if_splits) +done + +lemma inv_on_right_moving_2_inv_on_right_moving[simp]: + "inv_on_right_moving (as, lm) (x, l, Bk # r) ires + \<Longrightarrow> inv_after_write (as, lm) (y, l, Oc # r) ires" +apply(auto simp: inv_on_right_moving.simps inv_after_write.simps ) +apply(case_tac mr, auto simp: split: if_splits) +apply(case_tac [!] mr, simp_all) +done + +lemma [simp]: "inv_on_right_moving (as, lm) (x, l, []) ires\<Longrightarrow> + inv_on_right_moving (as, lm) (y, l, [Bk]) ires" +apply(auto simp: inv_on_right_moving.simps) +apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, simp) +done + +(*inv: from on_right_moving to after_write*) +lemma [simp]: "inv_on_right_moving (as, lm) (x, l, []) ires + \<Longrightarrow> inv_after_write (as, lm) (y, l, [Oc]) ires" +apply(rule_tac inv_on_right_moving_2_inv_on_right_moving, simp) +done + +(*inv: from on_left_moving to on_left_moving*) +lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm) + (s, l, Oc # r) ires = False" +apply(auto simp: inv_on_left_moving_in_middle_B.simps ) +done + +lemma [simp]: "inv_on_left_moving_norm (as, lm) (s, l, Bk # r) ires + = False" +apply(auto simp: inv_on_left_moving_norm.simps) +apply(case_tac [!] mr, auto simp: ) +done + +lemma [simp]: + "\<lbrakk>inv_on_left_moving_norm (as, lm) (s, l, Oc # r) ires; + hd l = Bk; l \<noteq> []\<rbrakk> \<Longrightarrow> + inv_on_left_moving_in_middle_B (as, lm) (s, tl l, Bk # Oc # r) ires" +apply(case_tac l, simp, simp) +apply(simp only: inv_on_left_moving_norm.simps + inv_on_left_moving_in_middle_B.simps) +apply(erule_tac exE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = "m # lm2" in exI, auto) +apply(case_tac [!] ml, auto) +apply(auto simp: tape_of_nl_cons split: if_splits) +apply(rule_tac [!] x = "Suc rn" in exI, simp_all) +done + +lemma [simp]: "\<lbrakk>inv_on_left_moving_norm (as, lm) (s, l, Oc # r) ires; + hd l = Oc; l \<noteq> []\<rbrakk> + \<Longrightarrow> inv_on_left_moving_norm (as, lm) + (s, tl l, Oc # Oc # r) ires" +apply(simp only: inv_on_left_moving_norm.simps) +apply(erule exE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = m in exI, rule_tac x = "ml - 1" in exI, + rule_tac x = "Suc mr" in exI, rule_tac x = rn in exI, simp) +apply(case_tac ml, auto simp: split: if_splits) +done + +lemma [simp]: "inv_on_left_moving_norm (as, lm) (s, [], Oc # r) ires + \<Longrightarrow> inv_on_left_moving_in_middle_B (as, lm) (s, [], Bk # Oc # r) ires" +apply(auto simp: inv_on_left_moving_norm.simps + inv_on_left_moving_in_middle_B.simps split: if_splits) +done + +lemma [simp]:"inv_on_left_moving (as, lm) (s, l, Oc # r) ires + \<Longrightarrow> (l = [] \<longrightarrow> inv_on_left_moving (as, lm) (s, [], Bk # Oc # r) ires) + \<and> (l \<noteq> [] \<longrightarrow> inv_on_left_moving (as, lm) (s, tl l, hd l # Oc # r) ires)" +apply(simp add: inv_on_left_moving.simps) +apply(case_tac "l \<noteq> []", rule conjI, simp, simp) +apply(case_tac "hd l", simp, simp, simp) +done + +(*inv: from on_left_moving to check_left_moving*) +lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm) + (s, Bk # list, Bk # r) ires + \<Longrightarrow> inv_check_left_moving_on_leftmost (as, lm) + (s', list, Bk # Bk # r) ires" +apply(auto simp: inv_on_left_moving_in_middle_B.simps + inv_check_left_moving_on_leftmost.simps split: if_splits) +apply(case_tac [!] "rev lm1", simp_all) +apply(case_tac [!] lista, simp_all add: tape_of_nl_abv tape_of_nat_list.simps) +done + +lemma [simp]: + "inv_check_left_moving_in_middle (as, lm) (s, l, Bk # r) ires= False" +by(auto simp: inv_check_left_moving_in_middle.simps ) + +lemma [simp]: + "inv_on_left_moving_in_middle_B (as, lm) (s, [], Bk # r) ires\<Longrightarrow> + inv_check_left_moving_on_leftmost (as, lm) (s', [], Bk # Bk # r) ires" +apply(auto simp: inv_on_left_moving_in_middle_B.simps + inv_check_left_moving_on_leftmost.simps split: if_splits) +done + +lemma [simp]: "inv_check_left_moving_on_leftmost (as, lm) + (s, list, Oc # r) ires= False" +by(auto simp: inv_check_left_moving_on_leftmost.simps split: if_splits) + +lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm) + (s, Oc # list, Bk # r) ires + \<Longrightarrow> inv_check_left_moving_in_middle (as, lm) (s', list, Oc # Bk # r) ires" +apply(auto simp: inv_on_left_moving_in_middle_B.simps + inv_check_left_moving_in_middle.simps split: if_splits) +done + +lemma inv_on_left_moving_2_check_left_moving[simp]: + "inv_on_left_moving (as, lm) (s, l, Bk # r) ires + \<Longrightarrow> (l = [] \<longrightarrow> inv_check_left_moving (as, lm) (s', [], Bk # Bk # r) ires) + \<and> (l \<noteq> [] \<longrightarrow> + inv_check_left_moving (as, lm) (s', tl l, hd l # Bk # r) ires)" +apply(simp add: inv_on_left_moving.simps inv_check_left_moving.simps) +apply(case_tac l, simp, simp) +apply(case_tac a, simp, simp) +done + +lemma [simp]: "inv_on_left_moving_norm (as, lm) (s, l, []) ires = False" +apply(auto simp: inv_on_left_moving_norm.simps) +done + +lemma [simp]: "inv_on_left_moving (as, lm) (s, l, []) ires\<Longrightarrow> + inv_on_left_moving (as, lm) (6 + 2 * n, l, [Bk]) ires" +apply(simp add: inv_on_left_moving.simps) +apply(auto simp: inv_on_left_moving_in_middle_B.simps) +done + +lemma [simp]: "inv_on_left_moving (as, lm) (s, l, []) ires = False" +apply(simp add: inv_on_left_moving.simps) +apply(simp add: inv_on_left_moving_in_middle_B.simps) +done + +lemma [simp]: "inv_on_left_moving (as, lm) (s, l, []) ires + \<Longrightarrow> (l = [] \<longrightarrow> inv_check_left_moving (as, lm) (s', [], [Bk]) ires) \<and> + (l \<noteq> [] \<longrightarrow> inv_check_left_moving (as, lm) (s', tl l, [hd l]) ires)" +by simp + +lemma [intro]: "\<exists>rna. Bk # Bk \<up> rn = Bk \<up> rna" +apply(rule_tac x = "Suc rn" in exI, simp) +done + +lemma +inv_check_left_moving_in_middle_2_on_left_moving_in_middle_B[simp]: +"inv_check_left_moving_in_middle (as, lm) (s, Bk # list, Oc # r) ires + \<Longrightarrow> inv_on_left_moving_in_middle_B (as, lm) (s', list, Bk # Oc # r) ires" +apply(simp only: inv_check_left_moving_in_middle.simps + inv_on_left_moving_in_middle_B.simps) +apply(erule_tac exE)+ +apply(rule_tac x = "rev (tl (rev lm1))" in exI, + rule_tac x = "[hd (rev lm1)] @ lm2" in exI, auto) +apply(case_tac [!] "rev lm1",simp_all add: tape_of_nl_abv tape_of_nat_list.simps) +apply(case_tac [!] a, simp_all) +apply(case_tac [1] lm2, simp_all add: tape_of_nat_list.simps, auto) +apply(case_tac [3] lm2, simp_all add: tape_of_nat_list.simps, auto) +apply(case_tac [!] lista, simp_all add: tape_of_nat_list.simps) +done + +lemma [simp]: + "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires\<Longrightarrow> + inv_check_left_moving_in_middle (as, lm) (s', [Bk], Oc # r) ires" +apply(auto simp: inv_check_left_moving_in_middle.simps ) +done + +lemma [simp]: + "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires + \<Longrightarrow> inv_on_left_moving_in_middle_B (as, lm) (s', [], Bk # Oc # r) ires" +apply(insert +inv_check_left_moving_in_middle_2_on_left_moving_in_middle_B[of + as lm n "[]" r], simp) +done + +lemma [simp]: "inv_check_left_moving_in_middle (as, lm) + (s, Oc # list, Oc # r) ires + \<Longrightarrow> inv_on_left_moving_norm (as, lm) (s', list, Oc # Oc # r) ires" +apply(auto simp: inv_check_left_moving_in_middle.simps + inv_on_left_moving_norm.simps) +apply(rule_tac x = "rev (tl (rev lm1))" in exI, + rule_tac x = lm2 in exI, rule_tac x = "hd (rev lm1)" in exI) +apply(rule_tac conjI) +apply(case_tac "rev lm1", simp, simp) +apply(rule_tac x = "hd (rev lm1) - 1" in exI, auto) +apply(rule_tac [!] x = "Suc (Suc 0)" in exI, simp) +apply(case_tac [!] "rev lm1", simp_all) +apply(case_tac [!] a, simp_all add: tape_of_nl_cons split: if_splits) +done + +lemma [simp]: "inv_check_left_moving (as, lm) (s, l, Oc # r) ires +\<Longrightarrow> (l = [] \<longrightarrow> inv_on_left_moving (as, lm) (s', [], Bk # Oc # r) ires) \<and> + (l \<noteq> [] \<longrightarrow> inv_on_left_moving (as, lm) (s', tl l, hd l # Oc # r) ires)" +apply(case_tac l, + auto simp: inv_check_left_moving.simps inv_on_left_moving.simps) +apply(case_tac a, simp, simp) +done + +(*inv: check_left_moving to after_left_moving*) +lemma [simp]: "inv_check_left_moving (as, lm) (s, l, Bk # r) ires + \<Longrightarrow> inv_after_left_moving (as, lm) (s', Bk # l, r) ires" +apply(auto simp: inv_check_left_moving.simps + inv_check_left_moving_on_leftmost.simps inv_after_left_moving.simps) +done + + +lemma [simp]:"inv_check_left_moving (as, lm) (s, l, []) ires + \<Longrightarrow> inv_after_left_moving (as, lm) (s', Bk # l, []) ires" +by(simp add: inv_check_left_moving.simps +inv_check_left_moving_in_middle.simps +inv_check_left_moving_on_leftmost.simps) + +(*inv: after_left_moving to inv_stop*) +lemma [simp]: "inv_after_left_moving (as, lm) (s, l, Bk # r) ires + \<Longrightarrow> inv_stop (as, lm) (s', Bk # l, r) ires" +apply(auto simp: inv_after_left_moving.simps inv_stop.simps) +done + +lemma [simp]: "inv_after_left_moving (as, lm) (s, l, []) ires + \<Longrightarrow> inv_stop (as, lm) (s', Bk # l, []) ires" +by(auto simp: inv_after_left_moving.simps) + +(*inv: stop to stop*) +lemma [simp]: "inv_stop (as, lm) (x, l, r) ires \<Longrightarrow> + inv_stop (as, lm) (y, l, r) ires" +apply(simp add: inv_stop.simps) +done + +lemma [simp]: "inv_after_clear (as, lm) (s, aaa, Oc # xs) ires= False" +apply(auto simp: inv_after_clear.simps ) +done + +lemma [simp]: + "inv_after_left_moving (as, lm) (s, aaa, Oc # xs) ires = False" +by(auto simp: inv_after_left_moving.simps ) + +lemma [simp]: "inv_after_clear (as, abc_lm_s lm n (Suc (abc_lm_v lm n))) (s, b, []) ires = False" +apply(auto simp: inv_after_clear.simps) +done + +lemma [simp]: "inv_on_left_moving (as, abc_lm_s lm n (Suc (abc_lm_v lm n))) + (s, b, Oc # list) ires \<Longrightarrow> b \<noteq> []" +apply(auto simp: inv_on_left_moving.simps inv_on_left_moving_norm.simps split: if_splits) +done + +lemma [simp]: "inv_check_left_moving (as, abc_lm_s lm n (Suc (abc_lm_v lm n))) (s, b, Oc # list) ires \<Longrightarrow> b \<noteq> []" +apply(auto simp: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps split: if_splits) +done + +lemma tinc_correct_pre: + assumes layout: "ly = layout_of ap" + and inv_start: "inv_locate_a (as, lm) (n, l, r) ires" + and lm': "lm' = abc_lm_s lm n (Suc (abc_lm_v lm n))" + and f: "f = steps (Suc 0, l, r) (tinc_b, 0)" + and P: "P = (\<lambda> (s, l, r). s = 10)" + and Q: "Q = (\<lambda> (s, l, r). inc_inv n (as, lm) (s, l, r) ires)" + shows "\<exists> stp. P (f stp) \<and> Q (f stp)" +proof(rule_tac LE = inc_LE in halt_lemma2) + show "wf inc_LE" by(auto) +next + show "Q (f 0)" + using inv_start + apply(simp add: f P Q steps.simps inc_inv.simps) + done +next + show "\<not> P (f 0)" + apply(simp add: f P steps.simps) + done +next + show "\<forall>n. \<not> P (f n) \<and> Q (f n) \<longrightarrow> Q (f (Suc n)) \<and> (f (Suc n), f n) + \<in> inc_LE" + proof(rule_tac allI, rule_tac impI, simp add: f, + case_tac "steps (Suc 0, l, r) (tinc_b, 0) n", simp add: P) + fix n a b c + assume "a \<noteq> 10 \<and> Q (a, b, c)" + thus "Q (step (a, b, c) (tinc_b, 0)) \<and> (step (a, b, c) (tinc_b, 0), a, b, c) \<in> inc_LE" + apply(simp add:Q) + apply(simp add: inc_inv.simps) + apply(case_tac c, case_tac [2] aa) + apply(auto simp: Let_def step.simps tinc_b_def numeral_2_eq_2 numeral_3_eq_3 split: if_splits) + apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def numeral_5_eq_5 + numeral_6_eq_6 numeral_7_eq_7 numeral_8_eq_8 numeral_9_eq_9) + done + qed +qed + + +lemma tinc_correct: + assumes layout: "ly = layout_of ap" + and inv_start: "inv_locate_a (as, lm) (n, l, r) ires" + and lm': "lm' = abc_lm_s lm n (Suc (abc_lm_v lm n))" + shows "\<exists> stp l' r'. steps (Suc 0, l, r) (tinc_b, 0) stp = (10, l', r') + \<and> inv_stop (as, lm') (10, l', r') ires" + using assms + apply(drule_tac tinc_correct_pre, auto) + apply(rule_tac x = stp in exI, simp) + apply(simp add: inc_inv.simps) + done + +declare inv_locate_a.simps[simp del] abc_lm_s.simps[simp del] + abc_lm_v.simps[simp del] + +lemma [simp]: "(4::nat) * n mod 2 = 0" +apply(arith) +done + +lemma crsp_step_inc_pre: + assumes layout: "ly = layout_of ap" + and crsp: "crsp ly (as, lm) (s, l, r) ires" + and aexec: "abc_step_l (as, lm) (Some (Inc n)) = (asa, lma)" + shows "\<exists> stp k. steps (Suc 0, l, r) (findnth n @ shift tinc_b (2 * n), 0) stp + = (2*n + 10, Bk # Bk # ires, <lma> @ Bk\<up>k) \<and> stp > 0" +proof - + thm tm_append_steps + have "\<exists> stp l' r'. steps (Suc 0, l, r) (findnth n, 0) stp = (Suc (2 * n), l', r') + \<and> inv_locate_a (as, lm) (n, l', r') ires" + using assms + apply(rule_tac findnth_correct, simp_all add: crsp layout) + done + from this obtain stp l' r' where a: + "steps (Suc 0, l, r) (findnth n, 0) stp = (Suc (2 * n), l', r') + \<and> inv_locate_a (as, lm) (n, l', r') ires" by blast + moreover have + "\<exists> stp la ra. steps (Suc 0, l', r') (tinc_b, 0) stp = (10, la, ra) + \<and> inv_stop (as, lma) (10, la, ra) ires" + using assms a + proof(rule_tac lm' = lma and n = n and lm = lm and ly = ly and ap = ap in tinc_correct, + simp, simp) + show "lma = abc_lm_s lm n (Suc (abc_lm_v lm n))" + using aexec + apply(simp add: abc_step_l.simps) + done + qed + from this obtain stpa la ra where b: + "steps (Suc 0, l', r') (tinc_b, 0) stpa = (10, la, ra) + \<and> inv_stop (as, lma) (10, la, ra) ires" by blast + from a b show "\<exists>stp k. steps (Suc 0, l, r) (findnth n @ shift tinc_b (2 * n), 0) stp + = (2 * n + 10, Bk # Bk # ires, <lma> @ Bk \<up> k) \<and> stp > 0" + apply(rule_tac x = "stp + stpa" in exI) + using tm_append_steps[of "Suc 0" l r "findnth n" stp l' r' tinc_b stpa 10 la ra "length (findnth n) div 2"] + apply(simp add: length_findnth inv_stop.simps) + apply(case_tac stpa, simp_all add: steps.simps) + done +qed + lemma crsp_step_inc: assumes layout: "ly = layout_of ap" and crsp: "crsp ly (as, lm) (s, l, r) ires" and fetch: "abc_fetch as ap = Some (Inc n)" - shows "\<exists>stp. crsp ly (abc_step_l (as, lm) (Some (Inc n))) + shows "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Inc n))) (steps (s, l, r) (ci ly (start_of ly as) (Inc n), start_of ly as - Suc 0) stp) ires" - sorry +proof(case_tac "(abc_step_l (as, lm) (Some (Inc n)))") + fix a b + assume aexec: "abc_step_l (as, lm) (Some (Inc n)) = (a, b)" + then have "\<exists> stp k. steps (Suc 0, l, r) (findnth n @ shift tinc_b (2 * n), 0) stp + = (2*n + 10, Bk # Bk # ires, <b> @ Bk\<up>k) \<and> stp > 0" + using assms + apply(rule_tac crsp_step_inc_pre, simp_all) + done + thus "?thesis" + using assms aexec + apply(erule_tac exE) + apply(erule_tac exE) + apply(erule_tac conjE) + apply(rule_tac x = stp in exI, simp add: ci.simps tm_shift_eq_steps) + apply(drule_tac off = "(start_of (layout_of ap) as - Suc 0)" in tm_shift_eq_steps) + apply(auto simp: crsp.simps abc_step_l.simps fetch start_of_Suc1) + done +qed subsection{* Crsp of Dec n e*} +declare sete.simps[simp del] + +type_synonym dec_inv_t = "(nat * nat list) \<Rightarrow> config \<Rightarrow> cell list \<Rightarrow> bool" + +fun dec_first_on_right_moving :: "nat \<Rightarrow> dec_inv_t" + where + "dec_first_on_right_moving n (as, lm) (s, l, r) ires = + (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> + ml + mr = Suc m \<and> length lm1 = n \<and> ml > 0 \<and> m > 0 \<and> + (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires + else l = Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> + ((r = Oc\<up>mr @ [Bk] @ <lm2> @ Bk\<up>rn) \<or> (r = Oc\<up>mr \<and> lm2 = [])))" + +fun dec_on_right_moving :: "dec_inv_t" + where + "dec_on_right_moving (as, lm) (s, l, r) ires = + (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> + ml + mr = Suc (Suc m) \<and> + (if lm1 = [] then l = Oc\<up>ml@ Bk # Bk # ires + else l = Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> + ((r = Oc\<up>mr @ [Bk] @ <lm2> @ Bk\<up>rn) \<or> (r = Oc\<up>mr \<and> lm2 = [])))" + +fun dec_after_clear :: "dec_inv_t" + where + "dec_after_clear (as, lm) (s, l, r) ires = + (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> + ml + mr = Suc m \<and> ml = Suc m \<and> r \<noteq> [] \<and> r \<noteq> [] \<and> + (if lm1 = [] then l = Oc\<up>ml@ Bk # Bk # ires + else l = Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> + (tl r = Bk # <lm2> @ Bk\<up>rn \<or> tl r = [] \<and> lm2 = []))" + +fun dec_after_write :: "dec_inv_t" + where + "dec_after_write (as, lm) (s, l, r) ires = + (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> + ml + mr = Suc m \<and> ml = Suc m \<and> lm2 \<noteq> [] \<and> + (if lm1 = [] then l = Bk # Oc\<up>ml @ Bk # Bk # ires + else l = Bk # Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> + tl r = <lm2> @ Bk\<up>rn)" + +fun dec_right_move :: "dec_inv_t" + where + "dec_right_move (as, lm) (s, l, r) ires = + (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 + \<and> ml = Suc m \<and> mr = (0::nat) \<and> + (if lm1 = [] then l = Bk # Oc\<up>ml @ Bk # Bk # ires + else l = Bk # Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) + \<and> (r = Bk # <lm2> @ Bk\<up>rn \<or> r = [] \<and> lm2 = []))" + +fun dec_check_right_move :: "dec_inv_t" + where + "dec_check_right_move (as, lm) (s, l, r) ires = + (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> + ml = Suc m \<and> mr = (0::nat) \<and> + (if lm1 = [] then l = Bk # Bk # Oc\<up>ml @ Bk # Bk # ires + else l = Bk # Bk # Oc\<up>ml @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> + r = <lm2> @ Bk\<up>rn)" + +fun dec_left_move :: "dec_inv_t" + where + "dec_left_move (as, lm) (s, l, r) ires = + (\<exists> lm1 m rn. (lm::nat list) = lm1 @ [m::nat] \<and> + rn > 0 \<and> + (if lm1 = [] then l = Bk # Oc\<up>Suc m @ Bk # Bk # ires + else l = Bk # Oc\<up>Suc m @ Bk # <rev lm1> @ Bk # Bk # ires) \<and> r = Bk\<up>rn)" + +declare + dec_on_right_moving.simps[simp del] dec_after_clear.simps[simp del] + dec_after_write.simps[simp del] dec_left_move.simps[simp del] + dec_check_right_move.simps[simp del] dec_right_move.simps[simp del] + dec_first_on_right_moving.simps[simp del] + +fun inv_locate_n_b :: "inc_inv_t" + where + "inv_locate_n_b (as, lm) (s, l, r) ires= + (\<exists> lm1 lm2 tn m ml mr rn. lm @ 0\<up>tn = lm1 @ [m] @ lm2 \<and> + length lm1 = s \<and> m + 1 = ml + mr \<and> + ml = 1 \<and> tn = s + 1 - length lm \<and> + (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires + else l = Oc\<up>ml @ Bk # <rev lm1> @ Bk # Bk # ires) \<and> + (r = Oc\<up>mr @ [Bk] @ <lm2>@ Bk\<up>rn \<or> (lm2 = [] \<and> r = Oc\<up>mr)) + )" +(* +fun dec_inv_1 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t" + where + "dec_inv_1 ly n e (as, am) (s, l, r) ires = + (let ss = start_of ly as in + let am' = abc_lm_s am n (abc_lm_v am n - Suc 0) in + let am'' = abc_lm_s am n (abc_lm_v am n) in + if s = start_of ly e then inv_stop (as, am'') (s, l, r) ires + else if s = ss then False + else if s = ss + 2 * n then + inv_locate_a (as, am) (n, l, r) ires + \<or> inv_locate_a (as, am'') (n, l, r) ires + else if s = ss + 2 * n + 1 then + inv_locate_b (as, am) (n, l, r) ires + else if s = ss + 2 * n + 13 then + inv_on_left_moving (as, am'') (s, l, r) ires + else if s = ss + 2 * n + 14 then + inv_check_left_moving (as, am'') (s, l, r) ires + else if s = ss + 2 * n + 15 then + inv_after_left_moving (as, am'') (s, l, r) ires + else False)" +*) + + +fun dec_inv_1 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t" + where + "dec_inv_1 ly n e (as, am) (s, l, r) ires = + (let ss = start_of ly as in + let am' = abc_lm_s am n (abc_lm_v am n - Suc 0) in + let am'' = abc_lm_s am n (abc_lm_v am n) in + if s = start_of ly e then inv_stop (as, am'') (s, l, r) ires + else if s = ss then False + else if s = ss + 2 * n + 1 then + inv_locate_b (as, am) (n, l, r) ires + else if s = ss + 2 * n + 13 then + inv_on_left_moving (as, am'') (s, l, r) ires + else if s = ss + 2 * n + 14 then + inv_check_left_moving (as, am'') (s, l, r) ires + else if s = ss + 2 * n + 15 then + inv_after_left_moving (as, am'') (s, l, r) ires + else False)" + +declare fetch.simps[simp del] +lemma [simp]: + "fetch (ci ly (start_of ly as) (Dec n e)) (Suc (2 * n)) Bk = (W1, start_of ly as + 2 *n)" +apply(auto simp: fetch.simps length_ci_dec) +apply(auto simp: ci.simps nth_append length_findnth sete.simps shift.simps tdec_b_def) +using startof_not0[of ly as] by simp + +lemma [simp]: + "fetch (ci ly (start_of ly as) (Dec n e)) (Suc (2 * n)) Oc = (R, Suc (start_of ly as) + 2 *n)" +apply(auto simp: fetch.simps length_ci_dec) +apply(auto simp: ci.simps nth_append length_findnth sete.simps shift.simps tdec_b_def) +done + +lemma [simp]: + "\<lbrakk>r = [] \<or> hd r = Bk; inv_locate_a (as, lm) (n, l, r) ires\<rbrakk> + \<Longrightarrow> \<exists>stp la ra. + steps (start_of ly as + 2 * n, l, r) (ci ly (start_of ly as) (Dec n e), + start_of ly as - Suc 0) stp = (Suc (start_of ly as + 2 * n), la, ra) \<and> + inv_locate_b (as, lm) (n, la, ra) ires" +apply(rule_tac x = "Suc (Suc 0)" in exI) +apply(auto simp: steps.simps step.simps length_ci_dec) +apply(case_tac r, simp_all) +done + +lemma [simp]: + "\<lbrakk>inv_locate_a (as, lm) (n, l, r) ires; r \<noteq> [] \<and> hd r \<noteq> Bk\<rbrakk> + \<Longrightarrow> \<exists>stp la ra. + steps (start_of ly as + 2 * n, l, r) (ci ly (start_of ly as) (Dec n e), + start_of ly as - Suc 0) stp = (Suc (start_of ly as + 2 * n), la, ra) \<and> + inv_locate_b (as, lm) (n, la, ra) ires" +apply(rule_tac x = "(Suc 0)" in exI, case_tac "hd r", simp_all) +apply(auto simp: steps.simps step.simps length_ci_dec) +apply(case_tac r, simp_all) +done + +fun abc_dec_1_stage1:: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" + where + "abc_dec_1_stage1 (s, l, r) ss n = + (if s > ss \<and> s \<le> ss + 2*n + 1 then 4 + else if s = ss + 2 * n + 13 \<or> s = ss + 2*n + 14 then 3 + else if s = ss + 2*n + 15 then 2 + else 0)" + +fun abc_dec_1_stage2:: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" + where + "abc_dec_1_stage2 (s, l, r) ss n = + (if s \<le> ss + 2 * n + 1 then (ss + 2 * n + 16 - s) + else if s = ss + 2*n + 13 then length l + else if s = ss + 2*n + 14 then length l + else 0)" + +fun abc_dec_1_stage3 :: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" + where + "abc_dec_1_stage3 (s, l, r) ss n = + (if s \<le> ss + 2*n + 1 then + if (s - ss) mod 2 = 0 then + if r \<noteq> [] \<and> hd r = Oc then 0 else 1 + else length r + else if s = ss + 2 * n + 13 then + if r \<noteq> [] \<and> hd r = Oc then 2 + else 1 + else if s = ss + 2 * n + 14 then + if r \<noteq> [] \<and> hd r = Oc then 3 else 0 + else 0)" + +fun abc_dec_1_measure :: "(config \<times> nat \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)" + where + "abc_dec_1_measure (c, ss, n) = (abc_dec_1_stage1 c ss n, + abc_dec_1_stage2 c ss n, abc_dec_1_stage3 c ss n)" + +definition abc_dec_1_LE :: + "((config \<times> nat \<times> + nat) \<times> (config \<times> nat \<times> nat)) set" + where "abc_dec_1_LE \<equiv> (inv_image lex_triple abc_dec_1_measure)" + +lemma wf_dec_le: "wf abc_dec_1_LE" +by(auto intro:wf_inv_image simp:abc_dec_1_LE_def lex_triple_def lex_pair_def) + +lemma startof_Suc2: + "abc_fetch as ap = Some (Dec n e) \<Longrightarrow> + start_of (layout_of ap) (Suc as) = + start_of (layout_of ap) as + 2 * n + 16" +apply(auto simp: start_of.simps layout_of.simps + length_of.simps abc_fetch.simps + take_Suc_conv_app_nth split: if_splits) +done + +lemma start_of_less_2: + "start_of ly e \<le> start_of ly (Suc e)" +thm take_Suc +apply(case_tac "e < length ly") +apply(auto simp: start_of.simps take_Suc take_Suc_conv_app_nth) +done + +lemma start_of_less_1: "start_of ly e \<le> start_of ly (e + d)" +proof(induct d) + case 0 thus "?case" by simp +next + case (Suc d) + have "start_of ly e \<le> start_of ly (e + d)" by fact + moreover have "start_of ly (e + d) \<le> start_of ly (Suc (e + d))" + by(rule_tac start_of_less_2) + ultimately show"?case" + by(simp) +qed + +lemma start_of_less: + assumes "e < as" + shows "start_of ly e \<le> start_of ly as" +proof - + obtain d where " as = e + d" + using assms by (metis less_imp_add_positive) + thus "?thesis" + by(simp add: start_of_less_1) +qed + +lemma start_of_ge: + assumes fetch: "abc_fetch as ap = Some (Dec n e)" + and layout: "ly = layout_of ap" + and great: "e > as" + shows "start_of ly e \<ge> start_of ly as + 2*n + 16" +proof(cases "e = Suc as") + case True + have "e = Suc as" by fact + moreover hence "start_of ly (Suc as) = start_of ly as + 2*n + 16" + using layout fetch + by(simp add: startof_Suc2) + ultimately show "?thesis" by (simp) +next + case False + have "e \<noteq> Suc as" by fact + then have "e > Suc as" using great by arith + then have "start_of ly (Suc as) \<le> start_of ly e" + by(simp add: start_of_less) + moreover have "start_of ly (Suc as) = start_of ly as + 2*n + 16" + using layout fetch + by(simp add: startof_Suc2) + ultimately show "?thesis" + by arith +qed + +lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as < e; + Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR" +apply(drule_tac start_of_ge, simp_all) +apply(auto) +done + +lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as > e; + Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR" +apply(drule_tac ly = "layout_of ap" in start_of_less[of]) +apply(arith) +done + +lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); + Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR" +apply(subgoal_tac "as = e \<or> as < e \<or> as > e", auto) +done + +lemma [simp]:"fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (2 * n)) Oc + = (R, start_of ly as + 2*n + 1)" +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: "(start_of ly as = 0) = False" +apply(simp add: start_of.simps) +done + +lemma [simp]: "fetch (ci (ly) + (start_of ly as) (Dec n e)) (Suc (2 * n)) Bk + = (W1, start_of ly as + 2*n)" +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Oc + = (R, start_of ly as + 2*n + 2)" +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + + +lemma [simp]: "fetch (ci (ly) + (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Bk + = (L, start_of ly as + 2*n + 13)" +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + + +lemma [simp]: "fetch (ci (ly) + (start_of ly as) (Dec n e)) (Suc (Suc (Suc (2 * n)))) Oc + = (R, start_of ly as + 2*n + 2)" +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + + +lemma [simp]: "fetch (ci (ly) (start_of ly as) (Dec n e)) + (Suc (Suc (Suc (2 * n)))) Bk + = (L, start_of ly as + 2*n + 3)" +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 4) Oc + = (W0, start_of ly as + 2*n + 3)" +apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 4) Bk + = (R, start_of ly as + 2*n + 4)" +apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]:"fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 5) Bk + = (R, start_of ly as + 2*n + 5)" +apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 6) Bk + = (L, start_of ly as + 2*n + 6)" +apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: + "fetch (ci (ly) (start_of ly as) + (Dec n e)) (2 * n + 6) Oc + = (L, start_of ly as + 2*n + 7)" +apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]:"fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 7) Bk + = (L, start_of ly as + 2*n + 10)" +apply(subgoal_tac "2*n + 7 = Suc (2*n + 6)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 8) Bk + = (W1, start_of ly as + 2*n + 7)" +apply(subgoal_tac "2*n + 8 = Suc (2*n + 7)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 8) Oc + = (R, start_of ly as + 2*n + 8)" +apply(subgoal_tac "2*n + 8 = Suc (2*n + 7)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 9) Bk + = (L, start_of ly as + 2*n + 9)" +apply(subgoal_tac "2*n + 9 = Suc (2*n + 8)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 9) Oc + = (R, start_of ly as + 2*n + 8)" +apply(subgoal_tac "2*n + 9 = Suc (2*n + 8)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 10) Bk + = (R, start_of ly as + 2*n + 4)" +apply(subgoal_tac "2*n + 10 = Suc (2*n + 9)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 10) Oc + = (W0, start_of ly as + 2*n + 9)" +apply(subgoal_tac "2*n + 10 = Suc (2*n + 9)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 11) Oc + = (L, start_of ly as + 2*n + 10)" +apply(subgoal_tac "2*n + 11 = Suc (2*n + 10)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 11) Bk + = (L, start_of ly as + 2*n + 11)" +apply(subgoal_tac "2*n + 11 = Suc (2*n + 10)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 12) Oc + = (L, start_of ly as + 2*n + 10)" +apply(subgoal_tac "2*n + 12 = Suc (2*n + 11)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 12) Bk + = (R, start_of ly as + 2*n + 12)" +apply(subgoal_tac "2*n + 12 = Suc (2*n + 11)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (2 * n + 13) Bk + = (R, start_of ly as + 2*n + 16)" +apply(subgoal_tac "2*n + 13 = Suc (2*n + 12)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (14 + 2 * n) Oc + = (L, start_of ly as + 2*n + 13)" +apply(subgoal_tac "14 + 2*n = Suc (2*n + 13)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (14 + 2 * n) Bk + = (L, start_of ly as + 2*n + 14)" +apply(subgoal_tac "14 + 2*n = Suc (2*n + 13)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (15 + 2 * n) Oc + = (L, start_of ly as + 2*n + 13)" +apply(subgoal_tac "15 + 2*n = Suc (2*n + 14)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: + "fetch (ci (ly) + (start_of ly as) (Dec n e)) (15 + 2 * n) Bk + = (R, start_of ly as + 2*n + 15)" +apply(subgoal_tac "15 + 2*n = Suc (2*n + 14)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +lemma [simp]: + "abc_fetch as aprog = Some (Dec n e) \<Longrightarrow> + fetch (ci (ly) (start_of (ly) as) + (Dec n e)) (16 + 2 * n) Bk + = (R, start_of (ly) e)" +apply(subgoal_tac "16 + 2*n = Suc (2*n + 15)", simp only: fetch.simps) +apply(auto simp: ci.simps findnth.simps fetch.simps + nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) +done + +declare dec_inv_1.simps[simp del] + + +lemma [simp]: + "\<lbrakk>abc_fetch as aprog = Some (Dec n e); ly = layout_of aprog\<rbrakk> + \<Longrightarrow> (start_of ly e \<noteq> Suc (start_of ly as + 2 * n) \<and> + start_of ly e \<noteq> Suc (Suc (start_of ly as + 2 * n)) \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 3 \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 4 \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 5 \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 6 \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 7 \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 8 \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 9 \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 10 \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 11 \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 12 \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 13 \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 14 \<and> + start_of ly e \<noteq> start_of ly as + 2 * n + 15)" +using start_of_ge[of as aprog n e ly] start_of_less[of e as ly] +apply(case_tac "e < as", simp) +apply(case_tac "e = as", simp, simp) +done + +lemma [simp]: "\<lbrakk>abc_fetch as aprog = Some (Dec n e); ly = layout_of aprog\<rbrakk> + \<Longrightarrow> (Suc (start_of ly as + 2 * n) \<noteq> start_of ly e \<and> + Suc (Suc (start_of ly as + 2 * n)) \<noteq> start_of ly e \<and> + start_of ly as + 2 * n + 3 \<noteq> start_of ly e \<and> + start_of ly as + 2 * n + 4 \<noteq> start_of ly e \<and> + start_of ly as + 2 * n + 5 \<noteq>start_of ly e \<and> + start_of ly as + 2 * n + 6 \<noteq> start_of ly e \<and> + start_of ly as + 2 * n + 7 \<noteq> start_of ly e \<and> + start_of ly as + 2 * n + 8 \<noteq> start_of ly e \<and> + start_of ly as + 2 * n + 9 \<noteq> start_of ly e \<and> + start_of ly as + 2 * n + 10 \<noteq> start_of ly e \<and> + start_of ly as + 2 * n + 11 \<noteq> start_of ly e \<and> + start_of ly as + 2 * n + 12 \<noteq> start_of ly e \<and> + start_of ly as + 2 * n + 13 \<noteq> start_of ly e \<and> + start_of ly as + 2 * n + 14 \<noteq> start_of ly e \<and> + start_of ly as + 2 * n + 15 \<noteq> start_of ly e)" +using start_of_ge[of as aprog n e ly] start_of_less[of e as ly] +apply(case_tac "e < as", simp, simp) +apply(case_tac "e = as", simp, simp) +done + +lemma [simp]: "inv_locate_b (as, lm) (n, [], []) ires = False" +apply(auto simp: inv_locate_b.simps in_middle.simps split: if_splits) +done + +lemma [simp]: "inv_locate_b (as, lm) (n, [], Bk # list) ires = False" +apply(auto simp: inv_locate_b.simps in_middle.simps split: if_splits) +done + +(* + +lemma inv_locate_b_2_on_left_moving_b[simp]: + "inv_locate_b (as, am) (n, l, []) ires + \<Longrightarrow> inv_on_left_moving (as, + abc_lm_s am n (abc_lm_v am n)) (s, [], [Bk]) ires" +apply(auto simp: inv_locate_b.simps inv_on_left_moving.simps inv_on_left_moving_in_middle_B.simps + in_middle.simps split: if_splits) +apply(drule_tac length_equal, simp) + +apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s]) +apply(simp only: inv_on_left_moving.simps, simp) +apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B + (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp) +*) + +(* +lemma [simp]: + "inv_locate_b (as, am) (n, l, []) ires; l \<noteq> []\<rbrakk> + \<Longrightarrow> inv_on_left_moving (as, abc_lm_s am n + (abc_lm_v am n)) (s, tl l, [hd l]) ires" +apply(auto simp: inv_locate_b.simps inv_on_left_moving.simps inv_on_left_moving_in_middle_B.simps + in_middle.simps split: if_splits) +apply(drule_tac length_equal, simp) + +apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s]) +apply(simp only: inv_on_left_moving.simps, simp) +apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B + (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp) + +apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s]) +apply(simp only: inv_on_left_moving.simps, simp) +apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B + (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp) +apply(simp only: inv_on_left_moving_norm.simps) +apply(erule_tac exE)+ +apply(erule_tac conjE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = m in exI, rule_tac x = ml in exI, + rule_tac x = mr in exI, simp) +apply(case_tac mr, simp, simp, case_tac nat, auto intro: nil_2_nil) +done +*) + +lemma [simp]: + "\<lbrakk>dec_first_on_right_moving n (as, am) (s, aaa, Oc # xs) ires\<rbrakk> + \<Longrightarrow> dec_first_on_right_moving n (as, am) (s', Oc # aaa, xs) ires" +apply(simp only: dec_first_on_right_moving.simps) +apply(erule exE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = m in exI, simp) +apply(rule_tac x = "Suc ml" in exI, + rule_tac x = "mr - 1" in exI, auto) +apply(case_tac [!] mr, auto) +done + +lemma [simp]: + "dec_first_on_right_moving n (as, am) (s, l, Bk # xs) ires \<Longrightarrow> l \<noteq> []" +apply(auto simp: dec_first_on_right_moving.simps split: if_splits) +done + +lemma [elim]: + "\<lbrakk>\<not> length lm1 < length am; + am @ replicate (length lm1 - length am) 0 @ [0::nat] = + lm1 @ m # lm2; + 0 < m\<rbrakk> + \<Longrightarrow> RR" +apply(subgoal_tac "lm2 = []", simp) +apply(drule_tac length_equal, simp) +done + +lemma [simp]: + "\<lbrakk>dec_first_on_right_moving n (as, + abc_lm_s am n (abc_lm_v am n)) (s, l, Bk # xs) ires\<rbrakk> +\<Longrightarrow> dec_after_clear (as, abc_lm_s am n + (abc_lm_v am n - Suc 0)) (s', tl l, hd l # Bk # xs) ires" +apply(simp only: dec_first_on_right_moving.simps + dec_after_clear.simps abc_lm_s.simps abc_lm_v.simps) +apply(erule_tac exE)+ +apply(case_tac "n < length am") +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = "m - 1" in exI, auto simp: ) +apply(case_tac [!] mr, auto) +done + +lemma [simp]: + "\<lbrakk>dec_first_on_right_moving n (as, + abc_lm_s am n (abc_lm_v am n)) (s, l, []) ires\<rbrakk> +\<Longrightarrow> (l = [] \<longrightarrow> dec_after_clear (as, + abc_lm_s am n (abc_lm_v am n - Suc 0)) (s', [], [Bk]) ires) \<and> + (l \<noteq> [] \<longrightarrow> dec_after_clear (as, abc_lm_s am n + (abc_lm_v am n - Suc 0)) (s', tl l, [hd l]) ires)" +apply(subgoal_tac "l \<noteq> []", + simp only: dec_first_on_right_moving.simps + dec_after_clear.simps abc_lm_s.simps abc_lm_v.simps) +apply(erule_tac exE)+ +apply(case_tac "n < length am", simp) +apply(rule_tac x = lm1 in exI, rule_tac x = "m - 1" in exI, auto) +apply(case_tac [1-2] m, auto) +apply(auto simp: dec_first_on_right_moving.simps split: if_splits) +done + +lemma [simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, Oc # r) ires\<rbrakk> + \<Longrightarrow> dec_after_clear (as, am) (s', l, Bk # r) ires" +apply(auto simp: dec_after_clear.simps) +done + +lemma [simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, Bk # r) ires\<rbrakk> + \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, r) ires" +apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits) +done + +lemma [simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk> + \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, []) ires" +apply(auto simp: dec_after_clear.simps dec_right_move.simps ) +done + +lemma [simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk> + \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, [Bk]) ires" +apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits) +done + +lemma [simp]:"dec_right_move (as, am) (s, l, Oc # r) ires = False" +apply(auto simp: dec_right_move.simps) +done + +lemma dec_right_move_2_check_right_move[simp]: + "\<lbrakk>dec_right_move (as, am) (s, l, Bk # r) ires\<rbrakk> + \<Longrightarrow> dec_check_right_move (as, am) (s', Bk # l, r) ires" +apply(auto simp: dec_right_move.simps dec_check_right_move.simps split: if_splits) +done + +lemma [simp]: "(<lm::nat list> = []) = (lm = [])" +apply(case_tac lm, simp_all add: tape_of_nl_cons) +done + +lemma [simp]: + "dec_right_move (as, am) (s, l, []) ires= + dec_right_move (as, am) (s, l, [Bk]) ires" +apply(simp add: dec_right_move.simps) +done + +lemma [simp]: "\<lbrakk>dec_right_move (as, am) (s, l, []) ires\<rbrakk> + \<Longrightarrow> dec_check_right_move (as, am) (s, Bk # l, []) ires" +apply(insert dec_right_move_2_check_right_move[of as am s l "[]" s'], + simp) +done + +lemma [simp]: "dec_check_right_move (as, am) (s, l, r) ires\<Longrightarrow> l \<noteq> []" +apply(auto simp: dec_check_right_move.simps split: if_splits) +done + +lemma [simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, Oc # r) ires\<rbrakk> + \<Longrightarrow> dec_after_write (as, am) (s', tl l, hd l # Oc # r) ires" +apply(auto simp: dec_check_right_move.simps dec_after_write.simps) +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = m in exI, auto) +done + + + +lemma [simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, Bk # r) ires\<rbrakk> + \<Longrightarrow> dec_left_move (as, am) (s', tl l, hd l # Bk # r) ires" +apply(auto simp: dec_check_right_move.simps + dec_left_move.simps inv_after_move.simps) +apply(rule_tac x = lm1 in exI, rule_tac x = m in exI, auto split: if_splits) +apply(case_tac [!] lm2, simp_all add: tape_of_nl_cons split: if_splits) +apply(rule_tac [!] x = "(Suc rn)" in exI, simp_all) +done + +lemma [simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, []) ires\<rbrakk> + \<Longrightarrow> dec_left_move (as, am) (s', tl l, [hd l]) ires" +apply(auto simp: dec_check_right_move.simps + dec_left_move.simps inv_after_move.simps) +apply(rule_tac x = lm1 in exI, rule_tac x = m in exI, auto) +done + +lemma [simp]: "dec_left_move (as, am) (s, aaa, Oc # xs) ires = False" +apply(auto simp: dec_left_move.simps inv_after_move.simps) +done + +lemma [simp]: "dec_left_move (as, am) (s, l, r) ires + \<Longrightarrow> l \<noteq> []" +apply(auto simp: dec_left_move.simps split: if_splits) +done + +lemma [simp]: "inv_on_left_moving_in_middle_B (as, [m]) + (s', Oc # Oc\<up>m @ Bk # Bk # ires, Bk # Bk\<up>rn) ires" +apply(simp add: inv_on_left_moving_in_middle_B.simps) +apply(rule_tac x = "[m]" in exI, auto) +done + +lemma [simp]: "inv_on_left_moving_in_middle_B (as, [m]) + (s', Oc # Oc\<up>m @ Bk # Bk # ires, [Bk]) ires" +apply(simp add: inv_on_left_moving_in_middle_B.simps) +done + + +lemma [simp]: "lm1 \<noteq> [] \<Longrightarrow> + inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', + Oc # Oc\<up>m @ Bk # <rev lm1> @ Bk # Bk # ires, Bk # Bk\<up>rn) ires" +apply(simp only: inv_on_left_moving_in_middle_B.simps) +apply(rule_tac x = "lm1 @ [m ]" in exI, rule_tac x = "[]" in exI, simp) +apply(simp add: tape_of_nl_cons split: if_splits) +done + +lemma [simp]: "lm1 \<noteq> [] \<Longrightarrow> + inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', + Oc # Oc\<up> m @ Bk # <rev lm1> @ Bk # Bk # ires, [Bk]) ires" +apply(simp only: inv_on_left_moving_in_middle_B.simps) +apply(rule_tac x = "lm1 @ [m ]" in exI, rule_tac x = "[]" in exI, simp) +apply(simp add: tape_of_nl_cons split: if_splits) +done + +lemma [simp]: "dec_left_move (as, am) (s, l, Bk # r) ires + \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, hd l # Bk # r) ires" +apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits) +done + +(* +lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm1 @ [m]) + (s', Oc # Oc\<^bsup>m\<^esup> @ Bk # <rev lm1> @ Bk\<^bsup>ln\<^esup>, [Bk]) ires" +apply(auto simp: inv_on_left_moving_in_middle_B.simps) +apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = "[]" in exI, auto) +done +*) + +lemma [simp]: "dec_left_move (as, am) (s, l, []) ires + \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, [hd l]) ires" +apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits) +done + +lemma [simp]: "dec_after_write (as, am) (s, l, Oc # r) ires + \<Longrightarrow> dec_on_right_moving (as, am) (s', Oc # l, r) ires" +apply(auto simp: dec_after_write.simps dec_on_right_moving.simps) +apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = "tl lm2" in exI, + rule_tac x = "hd lm2" in exI, simp) +apply(rule_tac x = "Suc 0" in exI,rule_tac x = "Suc (hd lm2)" in exI) +apply(case_tac lm2, auto split: if_splits simp: tape_of_nl_cons) +done + +lemma [simp]: "dec_after_write (as, am) (s, l, Bk # r) ires + \<Longrightarrow> dec_after_write (as, am) (s', l, Oc # r) ires" +apply(auto simp: dec_after_write.simps) +done + +lemma [simp]: "dec_after_write (as, am) (s, aaa, []) ires + \<Longrightarrow> dec_after_write (as, am) (s', aaa, [Oc]) ires" +apply(auto simp: dec_after_write.simps) +done + +lemma [simp]: "dec_on_right_moving (as, am) (s, l, Oc # r) ires + \<Longrightarrow> dec_on_right_moving (as, am) (s', Oc # l, r) ires" +apply(simp only: dec_on_right_moving.simps) +apply(erule_tac exE)+ +apply(erule conjE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = "m" in exI, rule_tac x = "Suc ml" in exI, + rule_tac x = "mr - 1" in exI, simp) +apply(case_tac mr, auto) +done + +lemma [simp]: "dec_on_right_moving (as, am) (s, l, r) ires\<Longrightarrow> l \<noteq> []" +apply(auto simp: dec_on_right_moving.simps split: if_splits) +done + +lemma [simp]: "dec_on_right_moving (as, am) (s, l, Bk # r) ires + \<Longrightarrow> dec_after_clear (as, am) (s', tl l, hd l # Bk # r) ires" +apply(auto simp: dec_on_right_moving.simps dec_after_clear.simps) +apply(case_tac [!] mr, auto split: if_splits) +done + +lemma [simp]: "dec_on_right_moving (as, am) (s, l, []) ires + \<Longrightarrow> dec_after_clear (as, am) (s', tl l, [hd l]) ires" +apply(auto simp: dec_on_right_moving.simps dec_after_clear.simps) +apply(simp_all split: if_splits) +apply(rule_tac x = lm1 in exI, simp) +done + +lemma [simp]: + "inv_stop (as, abc_lm_s am n (abc_lm_v am n)) (s, l, r) ires \<Longrightarrow> l \<noteq> []" +apply(auto simp: inv_stop.simps) +done + +lemma dec_false_1[simp]: + "\<lbrakk>abc_lm_v am n = 0; inv_locate_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk> + \<Longrightarrow> False" +apply(auto simp: inv_locate_b.simps in_middle.simps) +apply(case_tac "length lm1 \<ge> length am", auto) +apply(subgoal_tac "lm2 = []", simp, subgoal_tac "m = 0", simp) +apply(case_tac mr, auto simp: ) +apply(subgoal_tac "Suc (length lm1) - length am = + Suc (length lm1 - length am)", + simp add: exp_ind del: replicate.simps, simp) +apply(drule_tac xs = "am @ replicate (Suc (length lm1) - length am) 0" + and ys = "lm1 @ m # lm2" in length_equal, simp) +apply(case_tac mr, auto simp: abc_lm_v.simps) +apply(case_tac "mr = 0", simp_all split: if_splits) +apply(subgoal_tac "Suc (length lm1) - length am = + Suc (length lm1 - length am)", + simp add: exp_ind del: replicate.simps, simp) +done + +lemma [simp]: + "\<lbrakk>inv_locate_b (as, am) (n, aaa, Bk # xs) ires; + abc_lm_v am n = 0\<rbrakk> + \<Longrightarrow> inv_on_left_moving (as, abc_lm_s am n 0) + (s, tl aaa, hd aaa # Bk # xs) ires" +apply(simp add: inv_on_left_moving.simps) +apply(simp only: inv_locate_b.simps in_middle.simps) +apply(erule_tac exE)+ +apply(simp add: inv_on_left_moving.simps) +apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B + (as, abc_lm_s am n 0) (s, tl aaa, hd aaa # Bk # xs) ires", simp) +apply(simp only: inv_on_left_moving_norm.simps) +apply(erule_tac conjE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = m in exI, rule_tac x = m in exI, + rule_tac x = "Suc 0" in exI, simp add: abc_lm_s.simps) +apply(case_tac mr, simp_all, auto simp: abc_lm_v.simps) +apply(simp only: exp_ind[THEN sym] replicate_Suc Nat.Suc_diff_le) +apply(auto simp: inv_on_left_moving_in_middle_B.simps split: if_splits) +done + + +lemma [simp]: + "\<lbrakk>abc_lm_v am n = 0; inv_locate_b (as, am) (n, aaa, []) ires\<rbrakk> + \<Longrightarrow> inv_on_left_moving (as, abc_lm_s am n 0) (s, tl aaa, [hd aaa]) ires" +apply(simp add: inv_on_left_moving.simps) +apply(simp only: inv_locate_b.simps in_middle.simps) +apply(erule_tac exE)+ +apply(simp add: inv_on_left_moving.simps) +apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B + (as, abc_lm_s am n 0) (s, tl aaa, [hd aaa]) ires", simp) +apply(simp only: inv_on_left_moving_norm.simps) +apply(erule_tac conjE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = m in exI, rule_tac x = m in exI, + rule_tac x = "Suc 0" in exI, simp add: abc_lm_s.simps) +apply(case_tac mr, simp_all, auto simp: abc_lm_v.simps) +apply(simp_all only: exp_ind Nat.Suc_diff_le del: replicate_Suc, simp_all) +apply(auto simp: inv_on_left_moving_in_middle_B.simps split: if_splits) +apply(case_tac [!] m, simp_all) +done + +lemma [simp]: "\<lbrakk>am ! n = (0::nat); n < length am\<rbrakk> \<Longrightarrow> am[n := 0] = am" +apply(simp add: list_update_same_conv) +done + +lemma [intro]: "\<lbrakk>abc_lm_v (a # list) 0 = 0\<rbrakk> \<Longrightarrow> a = 0" +apply(simp add: abc_lm_v.simps split: if_splits) +done + +lemma [simp]: + "inv_stop (as, abc_lm_s am n 0) + (start_of (layout_of aprog) e, aaa, Oc # xs) ires + \<Longrightarrow> inv_locate_a (as, abc_lm_s am n 0) (0, aaa, Oc # xs) ires" +apply(simp add: inv_locate_a.simps) +apply(rule disjI1) +apply(auto simp: inv_stop.simps at_begin_norm.simps) +done + +lemma [simp]: + "\<lbrakk>inv_stop (as, abc_lm_s am n 0) + (start_of (layout_of aprog) e, aaa, Oc # xs) ires\<rbrakk> + \<Longrightarrow> inv_locate_b (as, am) (0, Oc # aaa, xs) ires \<or> + inv_locate_b (as, abc_lm_s am n 0) (0, Oc # aaa, xs) ires" +apply(simp) +done + +lemma dec_false2: + "inv_stop (as, abc_lm_s am n 0) + (start_of (layout_of aprog) e, aaa, Bk # xs) ires = False" +apply(auto simp: inv_stop.simps abc_lm_s.simps) +apply(case_tac [!] am, auto) +apply(case_tac [!] n, auto simp: tape_of_nl_cons split: if_splits) +done + +lemma dec_false3: + "inv_stop (as, abc_lm_s am n 0) + (start_of (layout_of aprog) e, aaa, []) ires = False" +apply(auto simp: inv_stop.simps abc_lm_s.simps) +done + +lemma [simp]: + "fetch (ci (layout_of aprog) + (start_of (layout_of aprog) as) (Dec n e)) 0 b = (Nop, 0)" +by(simp add: fetch.simps) + +declare dec_inv_1.simps[simp del] + +declare inv_locate_n_b.simps [simp del] + +lemma [simp]: + "\<lbrakk>0 < abc_lm_v am n; 0 < n; + at_begin_fst_bwtn (as, am) (n, aaa, Oc # xs) ires\<rbrakk> + \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires" +apply(simp add: at_begin_fst_bwtn.simps inv_locate_n_b.simps ) +done + +lemma Suc_minus:"length am + tn = n + \<Longrightarrow> Suc tn = Suc n - length am " +apply(arith) +done + +lemma [simp]: + "\<lbrakk>0 < abc_lm_v am n; 0 < n; + at_begin_fst_awtn (as, am) (n, aaa, Oc # xs) ires\<rbrakk> + \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires" +apply(simp only: at_begin_fst_awtn.simps inv_locate_n_b.simps ) +apply(erule exE)+ +apply(erule conjE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, + rule_tac x = "Suc tn" in exI, rule_tac x = 0 in exI) +apply(simp add: exp_ind del: replicate.simps) +apply(rule conjI)+ +apply(auto) +done + +lemma [simp]: + "\<lbrakk>inv_locate_n_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk> + \<Longrightarrow> dec_first_on_right_moving n (as, abc_lm_s am n (abc_lm_v am n)) + (s, Oc # aaa, xs) ires" +apply(auto simp: inv_locate_n_b.simps dec_first_on_right_moving.simps + abc_lm_s.simps abc_lm_v.simps) +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = m in exI, simp) +apply(rule_tac x = "Suc (Suc 0)" in exI, + rule_tac x = "m - 1" in exI, simp) +apply(case_tac m, auto) +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = m in exI, + simp add: Suc_diff_le exp_ind del: replicate.simps) +apply(rule_tac x = "Suc (Suc 0)" in exI, + rule_tac x = "m - 1" in exI, simp) +apply(case_tac m, auto) +apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, + rule_tac x = m in exI, simp) +apply(rule_tac x = "Suc (Suc 0)" in exI, + rule_tac x = "m - 1" in exI, simp) +apply(case_tac m, auto) +apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, + rule_tac x = m in exI, + simp add: Suc_diff_le exp_ind del: replicate.simps, simp) +done + +lemma [simp]: "inv_on_left_moving (as, am) (s, [], r) ires + = False" +apply(simp add: inv_on_left_moving.simps inv_on_left_moving_norm.simps + inv_on_left_moving_in_middle_B.simps) +done + +lemma [simp]: + "inv_check_left_moving (as, abc_lm_s am n 0) + (start_of (layout_of aprog) as + 2 * n + 14, [], Oc # xs) ires + = False" +apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps) +done + +lemma [simp]: "inv_check_left_moving (as, abc_lm_s lm n (abc_lm_v lm n)) (s, [], Oc # list) ires = False" +apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps) +done + +lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); + start_of (layout_of ap) as < start_of (layout_of ap) e; + start_of (layout_of ap) e \<le> Suc (start_of (layout_of ap) as + 2 * n)\<rbrakk> + \<Longrightarrow> RR" + using start_of_less[of e as "layout_of ap"] start_of_ge[of as ap n e "layout_of ap"] +apply(case_tac "as < e", simp) +apply(case_tac "as = e", simp, simp) +done + +lemma crsp_step_dec_b_e_pre': + assumes layout: "ly = layout_of ap" + and inv_start: "inv_locate_b (as, lm) (n, la, ra) ires" + and fetch: "abc_fetch as ap = Some (Dec n e)" + and dec_0: "abc_lm_v lm n = 0" + and f: "f = (\<lambda> stp. (steps (Suc (start_of ly as) + 2 * n, la, ra) (ci ly (start_of ly as) (Dec n e), + start_of ly as - Suc 0) stp, start_of ly as, n))" + and P: "P = (\<lambda> ((s, l, r), ss, x). s = start_of ly e)" + and Q: "Q = (\<lambda> ((s, l, r), ss, x). dec_inv_1 ly x e (as, lm) (s, l, r) ires)" + shows "\<exists> stp. P (f stp) \<and> Q (f stp)" +proof(rule_tac LE = abc_dec_1_LE in halt_lemma2) + show "wf abc_dec_1_LE" by(intro wf_dec_le) +next + show "Q (f 0)" + using layout fetch + apply(simp add: f steps.simps Q dec_inv_1.simps) + apply(subgoal_tac "e > as \<or> e = as \<or> e < as") + apply(auto simp: Let_def start_of_ge start_of_less inv_start) + done +next + show "\<not> P (f 0)" + using layout fetch + apply(simp add: f steps.simps P) + done +next + show "\<forall>n. \<not> P (f n) \<and> Q (f n) \<longrightarrow> Q (f (Suc n)) \<and> (f (Suc n), f n) \<in> abc_dec_1_LE" + using fetch + proof(rule_tac allI, rule_tac impI) + fix na + assume "\<not> P (f na) \<and> Q (f na)" + thus "Q (f (Suc na)) \<and> (f (Suc na), f na) \<in> abc_dec_1_LE" + apply(simp add: f) + apply(case_tac "steps (Suc (start_of ly as + 2 * n), la, ra) + (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) na", simp) + proof - + fix a b c + assume "\<not> P ((a, b, c), start_of ly as, n) \<and> Q ((a, b, c), start_of ly as, n)" + thus "Q (step (a, b, c) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0), start_of ly as, n) \<and> + ((step (a, b, c) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0), start_of ly as, n), + (a, b, c), start_of ly as, n) \<in> abc_dec_1_LE" + apply(simp add: Q) + apply(case_tac c, case_tac [2] aa) + apply(simp_all add: dec_inv_1.simps Let_def split: if_splits) + using fetch layout dec_0 + apply(auto simp: step.simps P dec_inv_1.simps Let_def abc_dec_1_LE_def lex_triple_def lex_pair_def) + using dec_0 + apply(drule_tac dec_false_1, simp_all) + done + qed + qed +qed + +lemma crsp_step_dec_b_e_pre: + assumes "ly = layout_of ap" + and inv_start: "inv_locate_b (as, lm) (n, la, ra) ires" + and dec_0: "abc_lm_v lm n = 0" + and fetch: "abc_fetch as ap = Some (Dec n e)" + shows "\<exists>stp lb rb. + steps (Suc (start_of ly as) + 2 * n, la, ra) (ci ly (start_of ly as) (Dec n e), + start_of ly as - Suc 0) stp = (start_of ly e, lb, rb) \<and> + dec_inv_1 ly n e (as, lm) (start_of ly e, lb, rb) ires" + using assms + apply(drule_tac crsp_step_dec_b_e_pre', auto) + apply(rule_tac x = stp in exI, simp) + done + +lemma [simp]: + "\<lbrakk>abc_lm_v lm n = 0; + inv_stop (as, abc_lm_s lm n (abc_lm_v lm n)) (start_of ly e, lb, rb) ires\<rbrakk> + \<Longrightarrow> crsp ly (abc_step_l (as, lm) (Some (Dec n e))) (start_of ly e, lb, rb) ires" +apply(auto simp: crsp.simps abc_step_l.simps inv_stop.simps) +done + +lemma crsp_step_dec_b_e: + assumes layout: "ly = layout_of ap" + and inv_start: "inv_locate_a (as, lm) (n, l, r) ires" + and dec_0: "abc_lm_v lm n = 0" + and fetch: "abc_fetch as ap = Some (Dec n e)" + shows "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Dec n e))) + (steps (start_of ly as + 2 * n, l, r) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) stp) ires" +proof - + let ?P = "ci ly (start_of ly as) (Dec n e)" + let ?off = "start_of ly as - Suc 0" + have "\<exists> stp la ra. steps (start_of ly as + 2 * n, l, r) (?P, ?off) stp = (Suc (start_of ly as) + 2*n, la, ra) + \<and> inv_locate_b (as, lm) (n, la, ra) ires" + using inv_start + apply(case_tac "r = [] \<or> hd r = Bk", simp_all) + done + from this obtain stpa la ra where a: + "steps (start_of ly as + 2 * n, l, r) (?P, ?off) stpa = (Suc (start_of ly as) + 2*n, la, ra) + \<and> inv_locate_b (as, lm) (n, la, ra) ires" by blast + term dec_inv_1 + have "\<exists> stp lb rb. steps (Suc (start_of ly as) + 2 * n, la, ra) (?P, ?off) stp = (start_of ly e, lb, rb) + \<and> dec_inv_1 ly n e (as, lm) (start_of ly e, lb, rb) ires" + using assms a + apply(rule_tac crsp_step_dec_b_e_pre, auto) + done + from this obtain stpb lb rb where b: + "steps (Suc (start_of ly as) + 2 * n, la, ra) (?P, ?off) stpb = (start_of ly e, lb, rb) + \<and> dec_inv_1 ly n e (as, lm) (start_of ly e, lb, rb) ires" by blast + from a b show "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Dec n e))) + (steps (start_of ly as + 2 * n, l, r) (?P, ?off) stp) ires" + apply(rule_tac x = "stpa + stpb" in exI) + apply(simp add: steps_add) + using dec_0 + apply(simp add: dec_inv_1.simps) + apply(case_tac stpa, simp_all add: steps.simps) + done +qed + +fun dec_inv_2 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t" + where + "dec_inv_2 ly n e (as, am) (s, l, r) ires = + (let ss = start_of ly as in + let am' = abc_lm_s am n (abc_lm_v am n - Suc 0) in + let am'' = abc_lm_s am n (abc_lm_v am n) in + if s = 0 then False + else if s = ss + 2 * n then + inv_locate_a (as, am) (n, l, r) ires + else if s = ss + 2 * n + 1 then + inv_locate_n_b (as, am) (n, l, r) ires + else if s = ss + 2 * n + 2 then + dec_first_on_right_moving n (as, am'') (s, l, r) ires + else if s = ss + 2 * n + 3 then + dec_after_clear (as, am') (s, l, r) ires + else if s = ss + 2 * n + 4 then + dec_right_move (as, am') (s, l, r) ires + else if s = ss + 2 * n + 5 then + dec_check_right_move (as, am') (s, l, r) ires + else if s = ss + 2 * n + 6 then + dec_left_move (as, am') (s, l, r) ires + else if s = ss + 2 * n + 7 then + dec_after_write (as, am') (s, l, r) ires + else if s = ss + 2 * n + 8 then + dec_on_right_moving (as, am') (s, l, r) ires + else if s = ss + 2 * n + 9 then + dec_after_clear (as, am') (s, l, r) ires + else if s = ss + 2 * n + 10 then + inv_on_left_moving (as, am') (s, l, r) ires + else if s = ss + 2 * n + 11 then + inv_check_left_moving (as, am') (s, l, r) ires + else if s = ss + 2 * n + 12 then + inv_after_left_moving (as, am') (s, l, r) ires + else if s = ss + 2 * n + 16 then + inv_stop (as, am') (s, l, r) ires + else False)" + +declare dec_inv_2.simps[simp del] +fun abc_dec_2_stage1 :: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" + where + "abc_dec_2_stage1 (s, l, r) ss n = + (if s \<le> ss + 2*n + 1 then 7 + else if s = ss + 2*n + 2 then 6 + else if s = ss + 2*n + 3 then 5 + else if s \<ge> ss + 2*n + 4 \<and> s \<le> ss + 2*n + 9 then 4 + else if s = ss + 2*n + 6 then 3 + else if s = ss + 2*n + 10 \<or> s = ss + 2*n + 11 then 2 + else if s = ss + 2*n + 12 then 1 + else 0)" + +fun abc_dec_2_stage2 :: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" + where + "abc_dec_2_stage2 (s, l, r) ss n = + (if s \<le> ss + 2 * n + 1 then (ss + 2 * n + 16 - s) + else if s = ss + 2*n + 10 then length l + else if s = ss + 2*n + 11 then length l + else if s = ss + 2*n + 4 then length r - 1 + else if s = ss + 2*n + 5 then length r + else if s = ss + 2*n + 7 then length r - 1 + else if s = ss + 2*n + 8 then + length r + length (takeWhile (\<lambda> a. a = Oc) l) - 1 + else if s = ss + 2*n + 9 then + length r + length (takeWhile (\<lambda> a. a = Oc) l) - 1 + else 0)" + +fun abc_dec_2_stage3 :: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" + where + "abc_dec_2_stage3 (s, l, r) ss n = + (if s \<le> ss + 2*n + 1 then + if (s - ss) mod 2 = 0 then if r \<noteq> [] \<and> + hd r = Oc then 0 else 1 + else length r + else if s = ss + 2 * n + 10 then + if r \<noteq> [] \<and> hd r = Oc then 2 + else 1 + else if s = ss + 2 * n + 11 then + if r \<noteq> [] \<and> hd r = Oc then 3 + else 0 + else (ss + 2 * n + 16 - s))" + +fun abc_dec_2_stage4 :: "config \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" + where + "abc_dec_2_stage4 (s, l, r) ss n = + (if s = ss + 2*n + 2 then length r + else if s = ss + 2*n + 8 then length r + else if s = ss + 2*n + 3 then + if r \<noteq> [] \<and> hd r = Oc then 1 + else 0 + else if s = ss + 2*n + 7 then + if r \<noteq> [] \<and> hd r = Oc then 0 + else 1 + else if s = ss + 2*n + 9 then + if r \<noteq> [] \<and> hd r = Oc then 1 + else 0 + else 0)" + +fun abc_dec_2_measure :: "(config \<times> nat \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat \<times> nat)" + where + "abc_dec_2_measure (c, ss, n) = + (abc_dec_2_stage1 c ss n, + abc_dec_2_stage2 c ss n, abc_dec_2_stage3 c ss n, abc_dec_2_stage4 c ss n)" + +definition lex_square:: + "((nat \<times> nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat \<times> nat)) set" + where "lex_square \<equiv> less_than <*lex*> lex_triple" + +definition abc_dec_2_LE :: + "((config \<times> nat \<times> + nat) \<times> (config \<times> nat \<times> nat)) set" + where "abc_dec_2_LE \<equiv> (inv_image lex_square abc_dec_2_measure)" + +lemma wf_dec2_le: "wf abc_dec_2_LE" +by(auto intro:wf_inv_image simp:abc_dec_2_LE_def lex_square_def lex_triple_def lex_pair_def) + +lemma fix_add: "fetch ap ((x::nat) + 2*n) b = fetch ap (2*n + x) b" +by (metis Suc_1 mult_2 nat_add_commute) + +lemma [elim]: + "\<lbrakk>0 < abc_lm_v am n; inv_locate_n_b (as, am) (n, aaa, Bk # xs) ires\<rbrakk> + \<Longrightarrow> RR" +apply(auto simp: inv_locate_n_b.simps abc_lm_v.simps split: if_splits) +apply(case_tac [!] m, auto) +done + +lemma [elim]: + "\<lbrakk>0 < abc_lm_v am n; inv_locate_n_b (as, am) + (n, aaa, []) ires\<rbrakk> \<Longrightarrow> RR" +apply(auto simp: inv_locate_n_b.simps abc_lm_v.simps split: if_splits) +done + +lemma [simp]: "dec_after_write (as, am) (s, aa, r) ires + \<Longrightarrow> takeWhile (\<lambda>a. a = Oc) aa = []" +apply(simp only : dec_after_write.simps) +apply(erule exE)+ +apply(erule_tac conjE)+ +apply(case_tac aa, simp) +apply(case_tac a, simp only: takeWhile.simps , simp_all split: if_splits) +done + +lemma [simp]: + "\<lbrakk>dec_on_right_moving (as, lm) (s, aa, []) ires; + length (takeWhile (\<lambda>a. a = Oc) (tl aa)) + \<noteq> length (takeWhile (\<lambda>a. a = Oc) aa) - Suc 0\<rbrakk> + \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (tl aa)) < + length (takeWhile (\<lambda>a. a = Oc) aa) - Suc 0" +apply(simp only: dec_on_right_moving.simps) +apply(erule_tac exE)+ +apply(erule_tac conjE)+ +apply(case_tac mr, auto split: if_splits) +done + +lemma [simp]: + "dec_after_clear (as, abc_lm_s am n (abc_lm_v am n - Suc 0)) + (start_of (layout_of aprog) as + 2 * n + 9, aa, Bk # xs) ires + \<Longrightarrow> length xs - Suc 0 < length xs + + length (takeWhile (\<lambda>a. a = Oc) aa)" +apply(simp only: dec_after_clear.simps) +apply(erule_tac exE)+ +apply(erule conjE)+ +apply(simp split: if_splits ) +done + +lemma [simp]: + "\<lbrakk>dec_after_clear (as, abc_lm_s am n (abc_lm_v am n - Suc 0)) + (start_of (layout_of aprog) as + 2 * n + 9, aa, []) ires\<rbrakk> + \<Longrightarrow> Suc 0 < length (takeWhile (\<lambda>a. a = Oc) aa)" +apply(simp add: dec_after_clear.simps split: if_splits) +done + +lemma [elim]: + "inv_check_left_moving (as, lm) + (s, [], Oc # xs) ires + \<Longrightarrow> RR" +apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps) +done + +lemma [simp]: +"\<lbrakk>0 < abc_lm_v am n; + at_begin_norm (as, am) (n, aaa, Oc # xs) ires\<rbrakk> + \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires" +apply(simp only: at_begin_norm.simps inv_locate_n_b.simps) +apply(erule_tac exE)+ +apply(rule_tac x = lm1 in exI, simp) +apply(case_tac "length lm2", simp) +apply(case_tac "lm2", simp, simp) +apply(case_tac "lm2", auto simp: tape_of_nl_cons split: if_splits) +done + +lemma [simp]: + "\<lbrakk>0 < abc_lm_v am n; + at_begin_fst_awtn (as, am) (n, aaa, Oc # xs) ires\<rbrakk> + \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires" +apply(simp only: at_begin_fst_awtn.simps inv_locate_n_b.simps ) +apply(erule exE)+ +apply(erule conjE)+ +apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, + rule_tac x = "Suc tn" in exI, rule_tac x = 0 in exI) +apply(simp add: exp_ind del: replicate.simps) +apply(rule conjI)+ +apply(auto) +done + +lemma [simp]: + "\<lbrakk>0 < abc_lm_v am n; inv_locate_a (as, am) (n, aaa, Oc # xs) ires\<rbrakk> + \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc#aaa, xs) ires" +apply(auto simp: inv_locate_a.simps at_begin_fst_bwtn.simps) +done + +lemma [simp]: + "\<lbrakk>dec_on_right_moving (as, am) (s, aa, Bk # xs) ires; + Suc (length (takeWhile (\<lambda>a. a = Oc) (tl aa))) + \<noteq> length (takeWhile (\<lambda>a. a = Oc) aa)\<rbrakk> + \<Longrightarrow> Suc (length (takeWhile (\<lambda>a. a = Oc) (tl aa))) + < length (takeWhile (\<lambda>a. a = Oc) aa)" +apply(simp only: dec_on_right_moving.simps) +apply(erule exE)+ +apply(erule conjE)+ +apply(case_tac ml, auto split: if_splits ) +done + +lemma crsp_step_dec_b_suc_pre: + assumes layout: "ly = layout_of ap" + and crsp: "crsp ly (as, lm) (s, l, r) ires" + and inv_start: "inv_locate_a (as, lm) (n, la, ra) ires" + and fetch: "abc_fetch as ap = Some (Dec n e)" + and dec_suc: "0 < abc_lm_v lm n" + and f: "f = (\<lambda> stp. (steps (start_of ly as + 2 * n, la, ra) (ci ly (start_of ly as) (Dec n e), + start_of ly as - Suc 0) stp, start_of ly as, n))" + and P: "P = (\<lambda> ((s, l, r), ss, x). s = start_of ly as + 2*n + 16)" + and Q: "Q = (\<lambda> ((s, l, r), ss, x). dec_inv_2 ly x e (as, lm) (s, l, r) ires)" + shows "\<exists> stp. P (f stp) \<and> Q(f stp)" + proof(rule_tac LE = abc_dec_2_LE in halt_lemma2) + show "wf abc_dec_2_LE" by(intro wf_dec2_le) +next + show "Q (f 0)" + using layout fetch inv_start + apply(simp add: f steps.simps Q) + apply(simp only: dec_inv_2.simps) + apply(auto simp: Let_def start_of_ge start_of_less inv_start dec_inv_2.simps) + done +next + show "\<not> P (f 0)" + using layout fetch + apply(simp add: f steps.simps P) + done +next + show "\<forall>n. \<not> P (f n) \<and> Q (f n) \<longrightarrow> Q (f (Suc n)) \<and> (f (Suc n), f n) \<in> abc_dec_2_LE" + using fetch + proof(rule_tac allI, rule_tac impI) + fix na + assume "\<not> P (f na) \<and> Q (f na)" + thus "Q (f (Suc na)) \<and> (f (Suc na), f na) \<in> abc_dec_2_LE" + apply(simp add: f) + apply(case_tac "steps ((start_of ly as + 2 * n), la, ra) + (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) na", simp) + proof - + fix a b c + assume "\<not> P ((a, b, c), start_of ly as, n) \<and> Q ((a, b, c), start_of ly as, n)" + thus "Q (step (a, b, c) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0), start_of ly as, n) \<and> + ((step (a, b, c) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0), start_of ly as, n), + (a, b, c), start_of ly as, n) \<in> abc_dec_2_LE" + apply(simp add: Q) + apply(erule_tac conjE) + apply(case_tac c, case_tac [2] aa) + apply(simp_all add: dec_inv_2.simps Let_def) + apply(simp_all split: if_splits) + using fetch layout dec_suc + apply(auto simp: step.simps P dec_inv_2.simps Let_def abc_dec_2_LE_def lex_triple_def lex_pair_def lex_square_def + fix_add numeral_3_eq_3) + done + qed + qed +qed + +lemma [simp]: + "\<lbrakk>inv_stop (as, abc_lm_s lm n (abc_lm_v lm n - Suc 0)) + (start_of (layout_of ap) as + 2 * n + 16, a, b) ires; + abc_lm_v lm n > 0; + abc_fetch as ap = Some (Dec n e)\<rbrakk> + \<Longrightarrow> crsp (layout_of ap) (abc_step_l (as, lm) (Some (Dec n e))) + (start_of (layout_of ap) as + 2 * n + 16, a, b) ires" +apply(auto simp: inv_stop.simps crsp.simps abc_step_l.simps startof_Suc2) +apply(drule_tac startof_Suc2, simp) +done + +lemma crsp_step_dec_b_suc: + assumes layout: "ly = layout_of ap" + and crsp: "crsp ly (as, lm) (s, l, r) ires" + and inv_start: "inv_locate_a (as, lm) (n, la, ra) ires" + and fetch: "abc_fetch as ap = Some (Dec n e)" + and dec_suc: "0 < abc_lm_v lm n" + shows "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Dec n e))) + (steps (start_of ly as + 2 * n, la, ra) (ci (layout_of ap) + (start_of ly as) (Dec n e), start_of ly as - Suc 0) stp) ires" + using assms + apply(drule_tac crsp_step_dec_b_suc_pre, auto) + apply(rule_tac x = stp in exI, simp) + apply(simp add: dec_inv_2.simps) + apply(case_tac stp, simp_all add: steps.simps) + done + +lemma crsp_step_dec_b: + assumes layout: "ly = layout_of ap" + and crsp: "crsp ly (as, lm) (s, l, r) ires" + and inv_start: "inv_locate_a (as, lm) (n, la, ra) ires" + and fetch: "abc_fetch as ap = Some (Dec n e)" + shows "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Dec n e))) + (steps (start_of ly as + 2 * n, la, ra) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) stp) ires" +using assms +apply(case_tac "abc_lm_v lm n = 0") +apply(rule_tac crsp_step_dec_b_e, simp_all) +apply(rule_tac crsp_step_dec_b_suc, simp_all) +done + lemma crsp_step_dec: assumes layout: "ly = layout_of ap" and crsp: "crsp ly (as, lm) (s, l, r) ires" - shows "\<exists>stp. crsp ly (abc_step_l (as, lm) (Some (Dec n e))) + and fetch: "abc_fetch as ap = Some (Dec n e)" + shows "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Dec n e))) (steps (s, l, r) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) stp) ires" -sorry - +proof(simp add: ci.simps) + let ?off = "start_of ly as - Suc 0" + let ?A = "findnth n" + let ?B = "sete (shift (shift tdec_b (2 * n)) ?off) (start_of ly e)" + have "\<exists> stp la ra. steps (s, l, r) (shift ?A ?off @ ?B, ?off) stp = (start_of ly as + 2*n, la, ra) + \<and> inv_locate_a (as, lm) (n, la, ra) ires" + proof - + have "\<exists>stp l' r'. steps (Suc 0, l, r) (?A, 0) stp = (Suc (2 * n), l', r') \<and> + inv_locate_a (as, lm) (n, l', r') ires" + using assms + apply(rule_tac findnth_correct, simp_all) + done + then obtain stp l' r' where a: + "steps (Suc 0, l, r) (?A, 0) stp = (Suc (2 * n), l', r') \<and> + inv_locate_a (as, lm) (n, l', r') ires" by blast + then have "steps (Suc 0 + ?off, l, r) (shift ?A ?off, ?off) stp = (Suc (2 * n) + ?off, l', r')" + apply(rule_tac tm_shift_eq_steps, simp_all) + done + moreover have "s = start_of ly as" + using crsp + apply(auto simp: crsp.simps) + done + ultimately show "\<exists> stp la ra. steps (s, l, r) (shift ?A ?off @ ?B, ?off) stp = (start_of ly as + 2*n, la, ra) + \<and> inv_locate_a (as, lm) (n, la, ra) ires" + using a + apply(drule_tac B = ?B in tm_append_first_steps_eq, auto) + apply(rule_tac x = stp in exI, simp) + done + qed + from this obtain stpa la ra where a: + "steps (s, l, r) (shift ?A ?off @ ?B, ?off) stpa = (start_of ly as + 2*n, la, ra) + \<and> inv_locate_a (as, lm) (n, la, ra) ires" by blast + have "\<exists>stp. crsp ly (abc_step_l (as, lm) (Some (Dec n e))) + (steps (start_of ly as + 2*n, la, ra) (shift ?A ?off @ ?B, ?off) stp) ires \<and> stp > 0" + using assms a + apply(drule_tac crsp_step_dec_b, auto) + apply(rule_tac x = stp in exI, simp add: ci.simps) + done + then obtain stpb where b: + "crsp ly (abc_step_l (as, lm) (Some (Dec n e))) + (steps (start_of ly as + 2*n, la, ra) (shift ?A ?off @ ?B, ?off) stpb) ires \<and> stpb > 0" .. + from a b show "\<exists> stp>0. crsp ly (abc_step_l (as, lm) (Some (Dec n e))) + (steps (s, l, r) (shift ?A ?off @ ?B, ?off) stp) ires" + apply(rule_tac x = "stpa + stpb" in exI) + apply(simp add: steps_add) + done +qed + subsection{*Crsp of Goto*} + lemma crsp_step_goto: assumes layout: "ly = layout_of ap" and crsp: "crsp ly (as, lm) (s, l, r) ires" - shows "\<exists>stp. crsp ly (abc_step_l (as, lm) (Some (Goto n))) + shows "\<exists>stp>0. crsp ly (abc_step_l (as, lm) (Some (Goto n))) (steps (s, l, r) (ci ly (start_of ly as) (Goto n), start_of ly as - Suc 0) stp) ires" -sorry - +using crsp +apply(rule_tac x = "Suc 0" in exI) +apply(case_tac r, case_tac [2] a) +apply(simp_all add: ci.simps steps.simps step.simps crsp.simps fetch.simps + crsp.simps abc_step_l.simps) +done lemma crsp_step_in: assumes layout: "ly = layout_of ap" and compile: "tp = tm_of ap" and crsp: "crsp ly (as, lm) (s, l, r) ires" and fetch: "abc_fetch as ap = Some ins" - shows "\<exists> stp. crsp ly (abc_step_l (as, lm) (Some ins)) + shows "\<exists> stp>0. crsp ly (abc_step_l (as, lm) (Some ins)) (steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) ires" using assms apply(case_tac ins, simp_all) @@ -600,15 +3808,15 @@ and compile: "tp = tm_of ap" and crsp: "crsp ly (as, lm) (s, l, r) ires" and fetch: "abc_fetch as ap = Some ins" - shows "\<exists> stp. crsp ly (abc_step_l (as, lm) (Some ins)) + shows "\<exists> stp>0. crsp ly (abc_step_l (as, lm) (Some ins)) (steps (s, l, r) (tp, 0) stp) ires" proof - - have "\<exists> stp. crsp ly (abc_step_l (as, lm) (Some ins)) + have "\<exists> stp>0. crsp ly (abc_step_l (as, lm) (Some ins)) (steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) ires" using assms - apply(erule_tac crsp_step_in, simp_all) + apply(rule_tac crsp_step_in, simp_all) done - from this obtain stp where d: "crsp ly (abc_step_l (as, lm) (Some ins)) + from this obtain stp where d: "stp > 0 \<and> crsp ly (abc_step_l (as, lm) (Some ins)) (steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) ires" .. obtain s' l' r' where e: "(steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) = (s', l', r')" @@ -620,7 +3828,7 @@ apply(simp_all) apply(case_tac "(abc_step_l (as, lm) (Some ins))", simp add: crsp.simps) done - thus " \<exists>stp. crsp ly (abc_step_l (as, lm) (Some ins)) (steps (s, l, r) (tp, 0) stp) ires" + thus " \<exists>stp>0. crsp ly (abc_step_l (as, lm) (Some ins)) (steps (s, l, r) (tp, 0) stp) ires" using d e apply(rule_tac x = stp in exI, simp) done @@ -632,6 +3840,33 @@ and crsp: "crsp ly (as, lm) (s, l, r) ires" shows "\<exists> stp. crsp ly (abc_steps_l (as, lm) ap n) (steps (s, l, r) (tp, 0) stp) ires" +(* +proof(induct n) + case 0 + have "crsp ly (abc_steps_l (as, lm) ap 0) (steps (s, l, r) (tp, 0) 0) ires" + using crsp by(simp add: steps.simps abc_steps_l.simps) + thus "?case" + by(rule_tac x = 0 in exI, simp) +next + case (Suc n) + obtain as' lm' where a: "abc_steps_l (as, lm) ap n = (as', lm')" + by(case_tac "abc_steps_l (as, lm) ap n", auto) + have "\<exists>stp\<ge>n. crsp ly (abc_steps_l (as, lm) ap n) (steps (s, l, r) (tp, 0) stp) ires" + by fact + from this a obtain stpa where b: + "stpa\<ge>n \<and> crsp ly (as', lm') (steps (s, l, r) (tp, 0) stpa) ires" by auto + obtain s' l' r' where "steps (s, l, r) (tp, 0) stpa = (s', l', r')" + by(case_tac "steps (s, l, r) (tp, 0) stpa") + then have "stpa\<ge>n \<and> crsp ly (as', lm') (s', l', r') ires" using b by simp + from a and this show "?case" + proof(cases "abc_fetch as' ap") + case None + + + + have "crsp ly (abc_steps_l (as, lm) ap 0) (steps (s, l, r) (tp, 0) stp) ires" + apply(simp add: steps.simps abc_steps_l.simps) +*) using crsp apply(induct n) apply(rule_tac x = 0 in exI) @@ -657,19 +3892,114 @@ apply(case_tac "steps (Suc 0, l, r) (tm_of ap, 0) stpa", simp add: crsp.simps) done -(***normalize the tp compiled from ap, and we can use Hoare_plus when composed with mopup machine*) -definition tp_norm :: "abc_prog \<Rightarrow> instr list" - where - "tp_norm ap = tm_of ap @ [(Nop, 0), (Nop, 0)]" - +text{*The tp @ [(Nop, 0), (Nop, 0)] is nomoral turing machines, so we can use Hoare_plus when composing with Mop machine*} + +thm layout_of.simps +lemma layout_id_cons: "layout_of (ap @ [p]) = layout_of ap @ [length_of p]" +apply(simp add: layout_of.simps) +done + +lemma [simp]: "length (layout_of xs) = length xs" +by(simp add: layout_of.simps) + +thm tms_of.simps +term ci +thm tms_of.simps +thm tpairs_of.simps + +lemma [simp]: + "map (start_of (layout_of xs @ [length_of x])) [0..<length xs] = (map (start_of (layout_of xs)) [0..<length xs])" +apply(auto) +apply(simp add: layout_of.simps start_of.simps) +done + +lemma tpairs_id_cons: + "tpairs_of (xs @ [x]) = tpairs_of xs @ [(start_of (layout_of (xs @ [x])) (length xs), x)]" +apply(auto simp: tpairs_of.simps layout_id_cons ) +done + +lemma map_length_ci: + "(map (length \<circ> (\<lambda>(xa, y). ci (layout_of xs @ [length_of x]) xa y)) (tpairs_of xs)) = + (map (length \<circ> (\<lambda>(x, y). ci (layout_of xs) x y)) (tpairs_of xs)) " +apply(auto) +apply(case_tac b, auto simp: ci.simps sete.simps) +done + +lemma length_tp'[simp]: + "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow> + length tp = 2 * listsum (take (length ap) (layout_of ap))" +proof(induct ap arbitrary: ly tp rule: rev_induct) + case Nil + thus "?case" + by(simp add: tms_of.simps tm_of.simps tpairs_of.simps) +next + fix x xs ly tp + assume ind: "\<And>ly tp. \<lbrakk>ly = layout_of xs; tp = tm_of xs\<rbrakk> \<Longrightarrow> + length tp = 2 * listsum (take (length xs) (layout_of xs))" + and layout: "ly = layout_of (xs @ [x])" + and tp: "tp = tm_of (xs @ [x])" + obtain ly' where a: "ly' = layout_of xs" + by metis + obtain tp' where b: "tp' = tm_of xs" + by metis + have c: "length tp' = 2 * listsum (take (length xs) (layout_of xs))" + using a b + by(erule_tac ind, simp) + thus "length tp = 2 * + listsum (take (length (xs @ [x])) (layout_of (xs @ [x])))" + using tp b + apply(auto simp: layout_id_cons tm_of.simps tms_of.simps length_concat tpairs_id_cons map_length_ci) + apply(case_tac x) + apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth sete.simps length_of.simps + split: abc_inst.splits) + done +qed + +lemma [simp]: + "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow> + fetch (tp @ [(Nop, 0), (Nop, 0)]) (start_of ly (length ap)) b = + (Nop, 0)" +apply(case_tac b) +apply(simp_all add: start_of.simps fetch.simps nth_append) +done +(* lemma tp_correct: assumes layout: "ly = layout_of ap" + and compile: "tp = tm_of ap" and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires" and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)" - shows "\<exists> stp k. steps (Suc 0, l, r) (tp_norm ap, 0) stp = (0, Bk # Bk # ires, <am> @ Bk\<up>k)" - sorry - -(****mop_up***) + shows "\<exists> stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp = (0, Bk # Bk # ires, <am> @ Bk\<up>k)" + using assms +proof - + have "\<exists> stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp = + (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)" + proof - + have "\<exists> stp k. steps (Suc 0, l, r) (tp, 0) stp = + (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)" + using assms + apply(rule_tac tp_correct', simp_all) + done + from this obtain stp k where "steps (Suc 0, l, r) (tp, 0) stp = + (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)" by blast + thus "?thesis" + apply(rule_tac x = stp in exI, rule_tac x = k in exI) + apply(drule_tac tm_append_first_steps_eq, simp_all) + done + qed + from this obtain stp k where + "steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp = + (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)" + by blast + thus "\<exists>stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp + = (0, Bk # Bk # ires, <am> @ Bk \<up> k)" + using assms + apply(rule_tac x = "stp + Suc 0" in exI) + apply(simp add: steps_add) + apply(auto simp: step.simps) + done +qed + *) +(********for mopup***********) fun mopup_a :: "nat \<Rightarrow> instr list" where "mopup_a 0 = []" | @@ -686,22 +4016,946 @@ "mopup n = mopup_a n @ shift mopup_b (2*n)" (****) +type_synonym mopup_type = "config \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> cell list \<Rightarrow> bool" + +fun mopup_stop :: "mopup_type" + where + "mopup_stop (s, l, r) lm n ires= + (\<exists> ln rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> r = <abc_lm_v lm n> @ Bk\<up>rn)" + +fun mopup_bef_erase_a :: "mopup_type" + where + "mopup_bef_erase_a (s, l, r) lm n ires= + (\<exists> ln m rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> + r = Oc\<up>m@ Bk # <(drop ((s + 1) div 2) lm)> @ Bk\<up>rn)" + +fun mopup_bef_erase_b :: "mopup_type" + where + "mopup_bef_erase_b (s, l, r) lm n ires = + (\<exists> ln m rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> r = Bk # Oc\<up>m @ Bk # + <(drop (s div 2) lm)> @ Bk\<up>rn)" + +fun mopup_jump_over1 :: "mopup_type" + where + "mopup_jump_over1 (s, l, r) lm n ires = + (\<exists> ln m1 m2 rn. m1 + m2 = Suc (abc_lm_v lm n) \<and> + l = Oc\<up>m1 @ Bk\<up>ln @ Bk # Bk # ires \<and> + (r = Oc\<up>m2 @ Bk # <(drop (Suc n) lm)> @ Bk\<up>rn \<or> + (r = Oc\<up>m2 \<and> (drop (Suc n) lm) = [])))" + +fun mopup_aft_erase_a :: "mopup_type" + where + "mopup_aft_erase_a (s, l, r) lm n ires = + (\<exists> lnl lnr rn (ml::nat list) m. + m = Suc (abc_lm_v lm n) \<and> l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> + (r = <ml> @ Bk\<up>rn))" + +fun mopup_aft_erase_b :: "mopup_type" + where + "mopup_aft_erase_b (s, l, r) lm n ires= + (\<exists> lnl lnr rn (ml::nat list) m. + m = Suc (abc_lm_v lm n) \<and> + l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> + (r = Bk # <ml> @ Bk\<up>rn \<or> + r = Bk # Bk # <ml> @ Bk\<up>rn))" + +fun mopup_aft_erase_c :: "mopup_type" + where + "mopup_aft_erase_c (s, l, r) lm n ires = + (\<exists> lnl lnr rn (ml::nat list) m. + m = Suc (abc_lm_v lm n) \<and> + l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> + (r = <ml> @ Bk\<up>rn \<or> r = Bk # <ml> @ Bk\<up>rn))" + +fun mopup_left_moving :: "mopup_type" + where + "mopup_left_moving (s, l, r) lm n ires = + (\<exists> lnl lnr rn m. + m = Suc (abc_lm_v lm n) \<and> + ((l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> r = Bk\<up>rn) \<or> + (l = Oc\<up>(m - 1) @ Bk\<up>lnl @ Bk # Bk # ires \<and> r = Oc # Bk\<up>rn)))" + +fun mopup_jump_over2 :: "mopup_type" + where + "mopup_jump_over2 (s, l, r) lm n ires = + (\<exists> ln rn m1 m2. + m1 + m2 = Suc (abc_lm_v lm n) + \<and> r \<noteq> [] + \<and> (hd r = Oc \<longrightarrow> (l = Oc\<up>m1 @ Bk\<up>ln @ Bk # Bk # ires \<and> r = Oc\<up>m2 @ Bk\<up>rn)) + \<and> (hd r = Bk \<longrightarrow> (l = Bk\<up>ln @ Bk # ires \<and> r = Bk # Oc\<up>(m1+m2)@ Bk\<up>rn)))" + + +fun mopup_inv :: "mopup_type" + where + "mopup_inv (s, l, r) lm n ires = + (if s = 0 then mopup_stop (s, l, r) lm n ires + else if s \<le> 2*n then + if s mod 2 = 1 then mopup_bef_erase_a (s, l, r) lm n ires + else mopup_bef_erase_b (s, l, r) lm n ires + else if s = 2*n + 1 then + mopup_jump_over1 (s, l, r) lm n ires + else if s = 2*n + 2 then mopup_aft_erase_a (s, l, r) lm n ires + else if s = 2*n + 3 then mopup_aft_erase_b (s, l, r) lm n ires + else if s = 2*n + 4 then mopup_aft_erase_c (s, l, r) lm n ires + else if s = 2*n + 5 then mopup_left_moving (s, l, r) lm n ires + else if s = 2*n + 6 then mopup_jump_over2 (s, l, r) lm n ires + else False)" + +lemma mopup_fetch_0[simp]: + "(fetch (mopup_a n @ shift mopup_b (2 * n)) 0 b) = (Nop, 0)" +by(simp add: fetch.simps) + +lemma mop_bef_length[simp]: "length (mopup_a n) = 4 * n" +apply(induct n, simp_all add: mopup_a.simps) +done + +lemma mopup_a_nth: + "\<lbrakk>q < n; x < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + x) = + mopup_a (Suc q) ! ((4 * q) + x)" +apply(induct n, simp) +apply(case_tac "q < n", simp add: mopup_a.simps, auto) +apply(simp add: nth_append) +apply(subgoal_tac "q = n", simp) +apply(arith) +done + +lemma fetch_bef_erase_a_o[simp]: + "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> + \<Longrightarrow> (fetch (mopup_a n @ shift mopup_b (2 * n)) s Oc) = (W0, s + 1)" +apply(subgoal_tac "\<exists> q. s = 2*q + 1", auto) +apply(subgoal_tac "length (mopup_a n) = 4*n") +apply(auto simp: fetch.simps nth_of.simps nth_append) +apply(subgoal_tac "mopup_a n ! (4 * q + 1) = + mopup_a (Suc q) ! ((4 * q) + 1)", + simp add: mopup_a.simps nth_append) +apply(rule mopup_a_nth, auto) +apply arith +done + +lemma fetch_bef_erase_a_b[simp]: + "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> + \<Longrightarrow> (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s + 2)" +apply(subgoal_tac "\<exists> q. s = 2*q + 1", auto) +apply(subgoal_tac "length (mopup_a n) = 4*n") +apply(auto simp: fetch.simps nth_of.simps nth_append) +apply(subgoal_tac "mopup_a n ! (4 * q + 0) = + mopup_a (Suc q) ! ((4 * q + 0))", + simp add: mopup_a.simps nth_append) +apply(rule mopup_a_nth, auto) +apply arith +done + +lemma fetch_bef_erase_b_b: + "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = 0\<rbrakk> \<Longrightarrow> + (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s - 1)" +apply(subgoal_tac "\<exists> q. s = 2 * q", auto) +apply(case_tac qa, simp, simp) +apply(auto simp: fetch.simps nth_of.simps nth_append) +apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = + mopup_a (Suc nat) ! ((4 * nat) + 2)", + simp add: mopup_a.simps nth_append) +apply(rule mopup_a_nth, auto) +done + +lemma fetch_jump_over1_o: + "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Oc + = (R, Suc (2 * n))" +apply(subgoal_tac "length (mopup_a n) = 4 * n") +apply(auto simp: fetch.simps nth_of.simps mopup_b_def nth_append + shift.simps) +done + +lemma fetch_jump_over1_b: + "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Bk + = (R, Suc (Suc (2 * n)))" +apply(subgoal_tac "length (mopup_a n) = 4 * n") +apply(auto simp: fetch.simps nth_of.simps mopup_b_def + nth_append shift.simps) +done + +lemma fetch_aft_erase_a_o: + "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Oc + = (W0, Suc (2 * n + 2))" +apply(subgoal_tac "length (mopup_a n) = 4 * n") +apply(auto simp: fetch.simps nth_of.simps mopup_b_def + nth_append shift.simps) +done + +lemma fetch_aft_erase_a_b: + "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Bk + = (L, Suc (2 * n + 4))" +apply(subgoal_tac "length (mopup_a n) = 4 * n") +apply(auto simp: fetch.simps nth_of.simps mopup_b_def + nth_append shift.simps) +done + +lemma fetch_aft_erase_b_b: + "fetch (mopup_a n @ shift mopup_b (2 * n)) (2*n + 3) Bk + = (R, Suc (2 * n + 3))" +apply(subgoal_tac "length (mopup_a n) = 4 * n") +apply(subgoal_tac "2*n + 3 = Suc (2*n + 2)", simp only: fetch.simps) +apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) +done + +lemma fetch_aft_erase_c_o: + "fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Oc + = (W0, Suc (2 * n + 2))" +apply(subgoal_tac "length (mopup_a n) = 4 * n") +apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps) +apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) +done + +lemma fetch_aft_erase_c_b: + "fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Bk + = (R, Suc (2 * n + 1))" +apply(subgoal_tac "length (mopup_a n) = 4 * n") +apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps) +apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) +done + +lemma fetch_left_moving_o: + "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Oc) + = (L, 2*n + 6)" +apply(subgoal_tac "length (mopup_a n) = 4 * n") +apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps) +apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) +done + +lemma fetch_left_moving_b: + "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Bk) + = (L, 2*n + 5)" +apply(subgoal_tac "length (mopup_a n) = 4 * n") +apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps) +apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) +done + +lemma fetch_jump_over2_b: + "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Bk) + = (R, 0)" +apply(subgoal_tac "length (mopup_a n) = 4 * n") +apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps) +apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) +done + +lemma fetch_jump_over2_o: +"(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Oc) + = (L, 2*n + 6)" +apply(subgoal_tac "length (mopup_a n) = 4 * n") +apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps) +apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) +done + +lemmas mopupfetchs = +fetch_bef_erase_a_o fetch_bef_erase_a_b fetch_bef_erase_b_b +fetch_jump_over1_o fetch_jump_over1_b fetch_aft_erase_a_o +fetch_aft_erase_a_b fetch_aft_erase_b_b fetch_aft_erase_c_o +fetch_aft_erase_c_b fetch_left_moving_o fetch_left_moving_b +fetch_jump_over2_b fetch_jump_over2_o + +declare + mopup_jump_over2.simps[simp del] mopup_left_moving.simps[simp del] + mopup_aft_erase_c.simps[simp del] mopup_aft_erase_b.simps[simp del] + mopup_aft_erase_a.simps[simp del] mopup_jump_over1.simps[simp del] + mopup_bef_erase_a.simps[simp del] mopup_bef_erase_b.simps[simp del] + mopup_stop.simps[simp del] + +lemma [simp]: + "\<lbrakk>mopup_bef_erase_a (s, l, Oc # xs) lm n ires\<rbrakk> \<Longrightarrow> + mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires" +apply(auto simp: mopup_bef_erase_a.simps mopup_bef_erase_b.simps ) +apply(rule_tac x = "m - 1" in exI, rule_tac x = rn in exI) +apply(case_tac m, simp, simp) +done + +lemma mopup_false1: + "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0; \<not> Suc s \<le> 2 * n\<rbrakk> + \<Longrightarrow> RR" +apply(arith) +done + +lemma [simp]: + "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; + mopup_bef_erase_a (s, l, Oc # xs) lm n ires; r = Oc # xs\<rbrakk> + \<Longrightarrow> (Suc s \<le> 2 * n \<longrightarrow> mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires) \<and> + (\<not> Suc s \<le> 2 * n \<longrightarrow> mopup_jump_over1 (Suc s, l, Bk # xs) lm n ires) " +apply(auto elim: mopup_false1) +done + +lemma drop_tape_of_cons: + "\<lbrakk>Suc q < length lm; x = lm ! q\<rbrakk> \<Longrightarrow> <drop q lm> = Oc # Oc \<up> x @ Bk # <drop (Suc q) lm>" +by (metis Suc_lessD append_Cons list.simps(2) nth_drop' replicate_Suc tape_of_nl_cons) + +lemma erase2jumpover1: + "\<lbrakk>q < length list; + \<forall>rn. <drop q list> \<noteq> Oc # Oc \<up> abc_lm_v (a # list) (Suc q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk> + \<Longrightarrow> <drop q list> = Oc # Oc \<up> abc_lm_v (a # list) (Suc q)" +apply(erule_tac x = 0 in allE, simp) +apply(case_tac "Suc q < length list") +apply(erule_tac notE) +apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps) +apply(subgoal_tac "length list = Suc q", auto) +apply(subgoal_tac "drop q list = [list ! q]") +apply(simp add: tape_of_nl_abv) +by (metis append_Nil2 append_eq_conv_conj lessI nth_drop') + +lemma erase2jumpover2: + "\<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> + Oc # Oc \<up> abc_lm_v (a # list) (Suc q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk> + \<Longrightarrow> RR" +apply(case_tac "Suc q < length list") +apply(erule_tac x = "Suc n" in allE, simp) +apply(erule_tac notE) +apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps) +apply(subgoal_tac "length list = Suc q", auto) +apply(erule_tac x = "n" in allE, simp) +by (metis append_Nil2 append_eq_conv_conj lessI nth_drop' + replicate_Suc tape_of_nat_list.simps(2) tape_of_nl_abv) + +lemma mopup_bef_erase_a_2_jump_over[simp]: + "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; + mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> (Suc (Suc s) \<le> 2 * n)\<rbrakk> +\<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires" +apply(auto simp: mopup_bef_erase_a.simps mopup_jump_over1.simps) +apply(case_tac m, auto simp: mod_ex1) +apply(subgoal_tac "n = Suc q", auto) +apply(rule_tac x = "Suc ln" in exI, rule_tac x = 0 in exI, auto) +apply(case_tac [!] lm, simp_all) +apply(case_tac [!] rn, auto elim: erase2jumpover1 erase2jumpover2) +apply(erule_tac x = 0 in allE, simp) +apply(rule_tac classical, simp) +apply(erule_tac notE) +apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps) +done + +lemma Suc_Suc_div: "\<lbrakk>0 < s; s mod 2 = Suc 0; Suc (Suc s) \<le> 2 * n\<rbrakk> + \<Longrightarrow> (Suc (Suc (s div 2))) \<le> n" +apply(arith) +done + +lemma mopup_bef_erase_a_2_a[simp]: + "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; + mopup_bef_erase_a (s, l, Bk # xs) lm n ires; + Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> + mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires" +apply(auto simp: mopup_bef_erase_a.simps) +apply(subgoal_tac "drop (Suc (Suc (s div 2))) lm \<noteq> []") +apply(case_tac m, simp_all) +apply(rule_tac x = "Suc (abc_lm_v lm (Suc (s div 2)))" in exI, + rule_tac x = rn in exI, auto simp: mod_ex1) +apply(rule_tac drop_tape_of_cons) +apply arith +apply(simp add: abc_lm_v.simps) +done + +lemma mopup_false2: + "\<lbrakk>0 < s; s \<le> 2 * n; + s mod 2 = Suc 0; Suc s \<noteq> 2 * n; + \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> RR" +apply(arith) +done + +lemma [simp]: "mopup_bef_erase_a (s, l, []) lm n ires \<Longrightarrow> + mopup_bef_erase_a (s, l, [Bk]) lm n ires" +apply(auto simp: mopup_bef_erase_a.simps) +done + +lemma [simp]: + "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; \<not> Suc (Suc s) \<le> 2 *n; + mopup_bef_erase_a (s, l, []) lm n ires\<rbrakk> + \<Longrightarrow> mopup_jump_over1 (s', Bk # l, []) lm n ires" +by auto + +lemma "mopup_bef_erase_b (s, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []" +apply(auto simp: mopup_bef_erase_b.simps) +done + +lemma [simp]: "mopup_bef_erase_b (s, l, Oc # xs) lm n ires = False" +apply(auto simp: mopup_bef_erase_b.simps ) +done + +lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> + (s - Suc 0) mod 2 = Suc 0" +apply(arith) +done + +lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> + s - Suc 0 \<le> 2 * n" +apply(simp) +done + +lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> \<not> s \<le> Suc 0" +apply(arith) +done + +lemma [simp]: "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; + s mod 2 \<noteq> Suc 0; + mopup_bef_erase_b (s, l, Bk # xs) lm n ires; r = Bk # xs\<rbrakk> + \<Longrightarrow> mopup_bef_erase_a (s - Suc 0, Bk # l, xs) lm n ires" +apply(auto simp: mopup_bef_erase_b.simps mopup_bef_erase_a.simps) +done + +lemma [simp]: "\<lbrakk>mopup_bef_erase_b (s, l, []) lm n ires\<rbrakk> \<Longrightarrow> + mopup_bef_erase_a (s - Suc 0, Bk # l, []) lm n ires" +apply(auto simp: mopup_bef_erase_b.simps mopup_bef_erase_a.simps) +done + +lemma [simp]: + "\<lbrakk>n < length lm; + mopup_jump_over1 (Suc (2 * n), l, Oc # xs) lm n ires; + r = Oc # xs\<rbrakk> + \<Longrightarrow> mopup_jump_over1 (Suc (2 * n), Oc # l, xs) lm n ires" +apply(auto simp: mopup_jump_over1.simps) +apply(rule_tac x = ln in exI, rule_tac x = "Suc m1" in exI, + rule_tac x = "m2 - 1" in exI, simp) +apply(case_tac "m2", simp, simp) +apply(rule_tac x = ln in exI, rule_tac x = "Suc m1" in exI, + rule_tac x = "m2 - 1" in exI) +apply(case_tac m2, simp, simp) +done + +lemma mopup_jump_over1_2_aft_erase_a[simp]: + "\<lbrakk>n < length lm; mopup_jump_over1 (Suc (2 * n), l, Bk # xs) lm n ires\<rbrakk> + \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires" +apply(simp only: mopup_jump_over1.simps mopup_aft_erase_a.simps) +apply(erule_tac exE)+ +apply(rule_tac x = ln in exI, rule_tac x = "Suc 0" in exI) +apply(case_tac m2, simp) +apply(rule_tac x = rn in exI, rule_tac x = "drop (Suc n) lm" in exI, + simp) +apply(simp) +done + +lemma [simp]: + "\<lbrakk>n < length lm; mopup_jump_over1 (Suc (2 * n), l, []) lm n ires\<rbrakk> \<Longrightarrow> + mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires" +apply(rule mopup_jump_over1_2_aft_erase_a, simp) +apply(auto simp: mopup_jump_over1.simps) +apply(rule_tac x = ln in exI, rule_tac x = "Suc (abc_lm_v lm n)" in exI, + rule_tac x = 0 in exI, simp add: ) +done + + +lemma [simp]: + "\<lbrakk>n < length lm; + mopup_aft_erase_a (Suc (Suc (2 * n)), l, Oc # xs) lm n ires\<rbrakk> + \<Longrightarrow> mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires" +apply(auto simp: mopup_aft_erase_a.simps mopup_aft_erase_b.simps ) +apply(case_tac ml) +apply(simp_all add: tape_of_nl_cons split: if_splits) +apply(case_tac a, simp_all) +apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp) +apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp) +apply(case_tac a, simp_all) +apply(rule_tac x = rn in exI, rule_tac x = "list" in exI, simp) +apply(rule_tac x = rn in exI) +apply(rule_tac x = "nat # list" in exI, simp add: tape_of_nl_cons) +done + +lemma [simp]: + "mopup_aft_erase_a (Suc (Suc (2 * n)), l, Bk # xs) lm n ires \<Longrightarrow> l \<noteq> []" +apply(auto simp: mopup_aft_erase_a.simps) +done + +lemma [simp]: + "\<lbrakk>n < length lm; + mopup_aft_erase_a (Suc (Suc (2 * n)), l, Bk # xs) lm n ires\<rbrakk> + \<Longrightarrow> mopup_left_moving (5 + 2 * n, tl l, hd l # Bk # xs) lm n ires" +apply(simp only: mopup_aft_erase_a.simps mopup_left_moving.simps) +apply(erule exE)+ +apply(case_tac lnr, simp) +apply(case_tac ml, simp, simp add: tape_of_nl_cons split: if_splits) +apply(auto) +apply(case_tac ml, simp_all add: tape_of_nl_cons split: if_splits) +apply(rule_tac x = "Suc rn" in exI, simp) +done + +lemma [simp]: + "mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires \<Longrightarrow> l \<noteq> []" +apply(simp only: mopup_aft_erase_a.simps) +apply(erule exE)+ +apply(auto) +done + +lemma [simp]: + "\<lbrakk>n < length lm; mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires\<rbrakk> + \<Longrightarrow> mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires" +apply(simp only: mopup_aft_erase_a.simps mopup_left_moving.simps) +apply(erule exE)+ +apply(subgoal_tac "ml = [] \<and> rn = 0", erule conjE, erule conjE, simp) +apply(case_tac lnr, simp) +apply(rule_tac x = lnl in exI, simp) +apply(rule_tac x = 1 in exI, simp) +apply(case_tac ml, simp, simp) +done + + +lemma [simp]: "mopup_aft_erase_b (2 * n + 3, l, Oc # xs) lm n ires = False" +apply(auto simp: mopup_aft_erase_b.simps ) +done + +lemma tape_of_ex1[intro]: + "\<exists>rna ml. Oc \<up> a @ Bk \<up> rn = <ml::nat list> @ Bk \<up> rna \<or> Oc \<up> a @ Bk \<up> rn = Bk # <ml> @ Bk \<up> rna" +apply(case_tac a, simp_all) +apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp) +apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp) +done + +lemma [intro]: "\<exists>rna ml. Oc \<up> a @ Bk # <list::nat list> @ Bk \<up> rn = + <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = Bk # <ml::nat list> @ Bk \<up> rna" +apply(case_tac "list = []", simp add: replicate_Suc[THEN sym] del: replicate_Suc) +apply(rule_tac rn = "Suc rn" in tape_of_ex1) +apply(case_tac a, simp) +apply(rule_tac x = rn in exI, rule_tac x = list in exI, simp) +apply(rule_tac x = rn in exI, rule_tac x = "nat # list" in exI) +apply(simp add: tape_of_nl_cons) +done + +lemma [simp]: + "\<lbrakk>n < length lm; + mopup_aft_erase_c (2 * n + 4, l, Oc # xs) lm n ires\<rbrakk> + \<Longrightarrow> mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires" +apply(auto simp: mopup_aft_erase_c.simps mopup_aft_erase_b.simps ) +apply(case_tac ml, simp_all add: tape_of_nl_cons split: if_splits, auto) +done + +lemma mopup_aft_erase_c_aft_erase_a[simp]: + "\<lbrakk>n < length lm; mopup_aft_erase_c (2 * n + 4, l, Bk # xs) lm n ires\<rbrakk> + \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires" +apply(simp only: mopup_aft_erase_c.simps mopup_aft_erase_a.simps ) +apply(erule_tac exE)+ +apply(erule conjE, erule conjE, erule disjE) +apply(subgoal_tac "ml = []", simp, case_tac rn, + simp, simp, rule conjI) +apply(rule_tac x = lnl in exI, rule_tac x = "Suc lnr" in exI, simp) +apply(rule_tac x = nat in exI, rule_tac x = "[]" in exI, simp) +apply(case_tac ml, simp, simp add: tape_of_nl_cons split: if_splits) +apply(rule_tac x = lnl in exI, rule_tac x = "Suc lnr" in exI, simp) +apply(rule_tac x = rn in exI, rule_tac x = "ml" in exI, simp) +done + +lemma [simp]: + "\<lbrakk>n < length lm; mopup_aft_erase_c (2 * n + 4, l, []) lm n ires\<rbrakk> + \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires" +apply(rule mopup_aft_erase_c_aft_erase_a, simp) +apply(simp only: mopup_aft_erase_c.simps) +apply(erule exE)+ +apply(rule_tac x = lnl in exI, rule_tac x = lnr in exI, simp add: ) +apply(rule_tac x = 0 in exI, rule_tac x = "[]" in exI, simp) +done + +lemma mopup_aft_erase_b_2_aft_erase_c[simp]: + "\<lbrakk>n < length lm; mopup_aft_erase_b (2 * n + 3, l, Bk # xs) lm n ires\<rbrakk> + \<Longrightarrow> mopup_aft_erase_c (4 + 2 * n, Bk # l, xs) lm n ires" +apply(auto simp: mopup_aft_erase_b.simps mopup_aft_erase_c.simps) +apply(rule_tac x = "lnl" in exI, rule_tac x = "Suc lnr" in exI, simp) +apply(rule_tac x = "lnl" in exI, rule_tac x = "Suc lnr" in exI, simp) +done + +lemma [simp]: + "\<lbrakk>n < length lm; mopup_aft_erase_b (2 * n + 3, l, []) lm n ires\<rbrakk> + \<Longrightarrow> mopup_aft_erase_c (4 + 2 * n, Bk # l, []) lm n ires" +apply(rule_tac mopup_aft_erase_b_2_aft_erase_c, simp) +apply(simp add: mopup_aft_erase_b.simps) +done + +lemma [simp]: + "mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []" +apply(auto simp: mopup_left_moving.simps) +done + +lemma [simp]: + "\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires\<rbrakk> + \<Longrightarrow> mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires" +apply(simp only: mopup_left_moving.simps mopup_jump_over2.simps) +apply(erule_tac exE)+ +apply(erule conjE, erule disjE, erule conjE) +apply(case_tac rn, simp, simp add: ) +apply(case_tac "hd l", simp add: ) +apply(case_tac "abc_lm_v lm n", simp) +apply(rule_tac x = "lnl" in exI, rule_tac x = rn in exI, + rule_tac x = "Suc 0" in exI, rule_tac x = 0 in exI) +apply(case_tac lnl, simp, simp, simp add: exp_ind[THEN sym], simp) +apply(case_tac "abc_lm_v lm n", simp) +apply(case_tac lnl, simp, simp) +apply(rule_tac x = lnl in exI, rule_tac x = rn in exI) +apply(rule_tac x = nat in exI, rule_tac x = "Suc (Suc 0)" in exI, simp) +done + +lemma [simp]: "mopup_left_moving (2 * n + 5, l, xs) lm n ires \<Longrightarrow> l \<noteq> []" +apply(auto simp: mopup_left_moving.simps) +done + +lemma [simp]: + "\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, Bk # xs) lm n ires\<rbrakk> + \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, hd l # Bk # xs) lm n ires" +apply(simp only: mopup_left_moving.simps) +apply(erule exE)+ +apply(case_tac lnr, simp) +apply(rule_tac x = lnl in exI, rule_tac x = nat in exI, simp) +apply(rule_tac x = "Suc rn" in exI, simp) +done + +lemma [simp]: +"\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, []) lm n ires\<rbrakk> + \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, [hd l]) lm n ires" +apply(simp only: mopup_left_moving.simps) +apply(erule exE)+ +apply(case_tac lnr, auto) +done + + +lemma [simp]: + "mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []" +apply(auto simp: mopup_jump_over2.simps ) +done + +lemma [simp]: +"\<lbrakk>n < length lm; mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires\<rbrakk> + \<Longrightarrow> mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires" +apply(simp only: mopup_jump_over2.simps) +apply(erule_tac exE)+ +apply(simp add: , erule conjE, erule_tac conjE) +apply(case_tac m1, simp) +apply(rule_tac x = ln in exI, rule_tac x = rn in exI, + rule_tac x = 0 in exI, simp) +apply(case_tac ln, simp, simp, simp only: exp_ind[THEN sym], simp) +apply(rule_tac x = ln in exI, rule_tac x = rn in exI, + rule_tac x = nat in exI, rule_tac x = "Suc m2" in exI, simp) +done + +lemma [simp]: + "\<lbrakk>n < length lm; mopup_jump_over2 (2 * n + 6, l, Bk # xs) lm n ires\<rbrakk> + \<Longrightarrow> mopup_stop (0, Bk # l, xs) lm n ires" +apply(auto simp: mopup_jump_over2.simps mopup_stop.simps) +apply(simp_all add: tape_of_nat_abv exp_ind[THEN sym]) +done + +lemma [simp]: "mopup_jump_over2 (2 * n + 6, l, []) lm n ires = False" +apply(simp only: mopup_jump_over2.simps, simp) +done + +lemma mopup_inv_step: + "\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> + \<Longrightarrow> mopup_inv (step (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0)) lm n ires" +apply(case_tac r, case_tac [2] a) +apply(auto split:if_splits simp add:step.simps) +apply(simp_all add: mopupfetchs) +done + +declare mopup_inv.simps[simp del] +lemma mopup_inv_steps: +"\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> + mopup_inv (steps (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp) lm n ires" +apply(induct_tac stp, simp add: steps.simps) +apply(simp add: step_red) +apply(case_tac "steps (s, l, r) + (mopup_a n @ shift mopup_b (2 * n), 0) na", simp) +apply(rule_tac mopup_inv_step, simp, simp) +done + +fun abc_mopup_stage1 :: "config \<Rightarrow> nat \<Rightarrow> nat" + where + "abc_mopup_stage1 (s, l, r) n = + (if s > 0 \<and> s \<le> 2*n then 6 + else if s = 2*n + 1 then 4 + else if s \<ge> 2*n + 2 \<and> s \<le> 2*n + 4 then 3 + else if s = 2*n + 5 then 2 + else if s = 2*n + 6 then 1 + else 0)" + +fun abc_mopup_stage2 :: "config \<Rightarrow> nat \<Rightarrow> nat" + where + "abc_mopup_stage2 (s, l, r) n = + (if s > 0 \<and> s \<le> 2*n then length r + else if s = 2*n + 1 then length r + else if s = 2*n + 5 then length l + else if s = 2*n + 6 then length l + else if s \<ge> 2*n + 2 \<and> s \<le> 2*n + 4 then length r + else 0)" + +fun abc_mopup_stage3 :: "config \<Rightarrow> nat \<Rightarrow> nat" + where + "abc_mopup_stage3 (s, l, r) n = + (if s > 0 \<and> s \<le> 2*n then + if hd r = Bk then 0 + else 1 + else if s = 2*n + 2 then 1 + else if s = 2*n + 3 then 0 + else if s = 2*n + 4 then 2 + else 0)" + +fun abc_mopup_measure :: "(config \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)" + where + "abc_mopup_measure (c, n) = + (abc_mopup_stage1 c n, abc_mopup_stage2 c n, + abc_mopup_stage3 c n)" + +definition abc_mopup_LE :: + "(((nat \<times> cell list \<times> cell list) \<times> nat) \<times> + ((nat \<times> cell list \<times> cell list) \<times> nat)) set" + where + "abc_mopup_LE \<equiv> (inv_image lex_triple abc_mopup_measure)" + +lemma wf_abc_mopup_le[intro]: "wf abc_mopup_LE" +by(auto intro:wf_inv_image simp:abc_mopup_LE_def lex_triple_def lex_pair_def) + +lemma [simp]: "mopup_bef_erase_a (a, aa, []) lm n ires = False" +apply(auto simp: mopup_bef_erase_a.simps) +done + +lemma [simp]: "mopup_bef_erase_b (a, aa, []) lm n ires = False" +apply(auto simp: mopup_bef_erase_b.simps) +done + +lemma [simp]: "mopup_aft_erase_b (2 * n + 3, aa, []) lm n ires = False" +apply(auto simp: mopup_aft_erase_b.simps) +done + +declare mopup_inv.simps[simp del] +term mopup_inv + +lemma [simp]: + "\<lbrakk>0 < q; q \<le> n\<rbrakk> \<Longrightarrow> + (fetch (mopup_a n @ shift mopup_b (2 * n)) (2*q) Bk) = (R, 2*q - 1)" +apply(case_tac q, simp, simp) +apply(auto simp: fetch.simps nth_of.simps nth_append) +apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = + mopup_a (Suc nat) ! ((4 * nat) + 2)", + simp add: mopup_a.simps nth_append) +apply(rule mopup_a_nth, auto) +done + +lemma mopup_halt: + assumes + less: "n < length lm" + and inv: "mopup_inv (Suc 0, l, r) lm n ires" + and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))" + and P: "P = (\<lambda> (c, n). is_final c)" + shows "\<exists> stp. P (f stp)" +proof(rule_tac LE = abc_mopup_LE in halt_lemma) + show "wf abc_mopup_LE" by(auto) +next + show "\<forall>n. \<not> P (f n) \<longrightarrow> (f (Suc n), f n) \<in> abc_mopup_LE" + proof(rule_tac allI, rule_tac impI) + fix na + assume h: "\<not> P (f na)" + show "(f (Suc na), f na) \<in> abc_mopup_LE" + proof(simp add: f) + obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)" + apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto) + done + then have "mopup_inv (a, b, c) lm n ires" + thm mopup_inv_steps + using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na] + apply(simp) + done + moreover have "a > 0" + using h g + apply(simp add: f P) + done + ultimately have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_LE" + apply(case_tac c, case_tac [2] aa) + apply(auto split:if_splits simp add:step.simps mopup_inv.simps) + apply(simp_all add: mopupfetchs abc_mopup_LE_def lex_triple_def lex_pair_def ) + done + thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) + (mopup_a n @ shift mopup_b (2 * n), 0), n), + steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n) + \<in> abc_mopup_LE" + using g by simp + qed + qed +qed + +lemma mopup_inv_start: + "n < length am \<Longrightarrow> mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires" +apply(auto simp: mopup_inv.simps mopup_bef_erase_a.simps mopup_jump_over1.simps) +apply(case_tac [!] am, auto split: if_splits simp: tape_of_nl_cons) +apply(rule_tac x = "Suc a" in exI, rule_tac x = k in exI, simp) +apply(case_tac [!] n, simp_all add: abc_lm_v.simps) +apply(case_tac k, simp, simp_all) +done + +lemma mopup_correct: + assumes less: "n < length (am::nat list)" + and rs: "abc_lm_v am n = rs" + shows "\<exists> stp i j. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp) + = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)" +using less +proof - + have a: "mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires" + using less + apply(simp add: mopup_inv_start) + done + then have "\<exists> stp. is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)" + using less mopup_halt[of n am "Bk # Bk # ires" "<am> @ Bk \<up> k" ires + "(\<lambda>stp. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))" + "(\<lambda>(c, n). is_final c)"] + apply(simp) + done + from this obtain stp where b: + "is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)" .. + from a b have + "mopup_inv (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp) + am n ires" + apply(rule_tac mopup_inv_steps, simp_all add: less) + done + from b and this show "?thesis" + apply(rule_tac x = stp in exI, simp) + apply(case_tac "steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) + (mopup_a n @ shift mopup_b (2 * n), 0) stp") + apply(simp add: mopup_inv.simps mopup_stop.simps rs) + using rs + apply(simp add: tape_of_nat_abv) + done +qed + (*we can use Hoare_plus here*) + +lemma wf_mopup[intro]: "tm_wf (mopup n, 0)" +apply(induct n, simp add: mopup.simps shift.simps mopup_b_def tm_wf.simps) +apply(auto simp: mopup.simps shift.simps mopup_b_def tm_wf.simps) +done + +lemma length_tp: + "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow> + start_of ly (length ap) = Suc (length tp div 2)" +apply(frule_tac length_tp', simp_all) +apply(simp add: start_of.simps) +done + lemma compile_correct_halt: assumes layout: "ly = layout_of ap" + and compile: "tp = tm_of ap" and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires" and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)" and rs_loc: "n < length am" - and rs: "rs = abc_lm_v am n" - shows "\<exists> stp i j. steps (Suc 0, l, r) (tp_norm ap |+| mopup n, 0) stp = (0, Bk\<up>i @ Bk # Bk # ires, Oc\<up>Suc rs @ Bk\<up>j)" -sorry - + and rs: "abc_lm_v am n = rs" + and off: "off = length tp div 2" + shows "\<exists> stp i j. steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp = (0, Bk\<up>i @ Bk # Bk # ires, Oc\<up>Suc rs @ Bk\<up>j)" +proof - + have "\<exists> stp k. steps (Suc 0, l, r) (tp, 0) stp = (Suc off, Bk # Bk # ires, <am> @ Bk\<up>k)" + using assms tp_correct'[of ly ap tp lm l r ires stp am] + by(simp add: length_tp) + then obtain stp k where "steps (Suc 0, l, r) (tp, 0) stp = (Suc off, Bk # Bk # ires, <am> @ Bk\<up>k)" + by blast + then have a: "steps (Suc 0, l, r) (tp@shift (mopup n) off , 0) stp = (Suc off, Bk # Bk # ires, <am> @ Bk\<up>k)" + using assms + by(auto intro: tm_append_first_steps_eq) + have "\<exists> stp i j. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp) + = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)" + using assms + by(auto intro: mopup_correct) + then obtain stpb i j where + "steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stpb + = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)" by blast + then have b: "steps (Suc 0 + off, Bk # Bk # ires, <am> @ Bk \<up> k) (tp @ shift (mopup n) off, 0) stpb + = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)" + using assms wf_mopup + thm tm_append_second_halt_eq + apply(drule_tac tm_append_second_halt_eq, auto) + done + from a b show "?thesis" + by(rule_tac x = "stp + stpb" in exI, simp add: steps_add) +qed + +declare mopup.simps[simp del] +lemma abc_step_red2: + "abc_steps_l (s, lm) p (Suc n) = (let (as', am') = abc_steps_l (s, lm) p n in + abc_step_l (as', am') (abc_fetch as' p))" +apply(case_tac "abc_steps_l (s, lm) p n", simp) +apply(drule_tac abc_step_red, simp) +done + +lemma crsp_steps2: + assumes + layout: "ly = layout_of ap" + and compile: "tp = tm_of ap" + and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires" + and nothalt: "as < length ap" + and aexec: "abc_steps_l (0, lm) ap stp = (as, am)" + shows "\<exists>stpa\<ge>stp. crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires" +using nothalt aexec +proof(induct stp arbitrary: as am) + case 0 + thus "?case" + using crsp + by(rule_tac x = 0 in exI, auto simp: abc_steps_l.simps steps.simps crsp) +next + case (Suc stp as am) + have ind: + "\<And> as am. \<lbrakk>as < length ap; abc_steps_l (0, lm) ap stp = (as, am)\<rbrakk> + \<Longrightarrow> \<exists>stpa\<ge>stp. crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires" by fact + have a: "as < length ap" by fact + have b: "abc_steps_l (0, lm) ap (Suc stp) = (as, am)" by fact + obtain as' am' where c: "abc_steps_l (0, lm) ap stp = (as', am')" + by(case_tac "abc_steps_l (0, lm) ap stp", auto) + then have d: "as' < length ap" + using a b + by(simp add: abc_step_red2, case_tac "as' < length ap", simp, + simp add: abc_fetch.simps abc_steps_l.simps abc_step_l.simps) + have "\<exists>stpa\<ge>stp. crsp ly (as', am') (steps (Suc 0, l, r) (tp, 0) stpa) ires" + using d c ind by simp + from this obtain stpa where e: + "stpa \<ge> stp \<and> crsp ly (as', am') (steps (Suc 0, l, r) (tp, 0) stpa) ires" + by blast + obtain s' l' r' where f: "steps (Suc 0, l, r) (tp, 0) stpa = (s', l', r')" + by(case_tac "steps (Suc 0, l, r) (tp, 0) stpa", auto) + obtain ins where g: "abc_fetch as' ap = Some ins" using d + by(case_tac "abc_fetch as' ap",auto simp: abc_fetch.simps) + then have "\<exists>stp> (0::nat). crsp ly (abc_step_l (as', am') (Some ins)) + (steps (s', l', r') (tp, 0) stp) ires " + using layout compile e f + by(rule_tac crsp_step, simp_all) + then obtain stpb where "stpb > 0 \<and> crsp ly (abc_step_l (as', am') (Some ins)) + (steps (s', l', r') (tp, 0) stpb) ires" .. + from this show "?case" using b e g f c + by(rule_tac x = "stpa + stpb" in exI, simp add: steps_add abc_step_red2) +qed + lemma compile_correct_unhalt: assumes layout: "ly = layout_of ap" + and compile: "tp = tm_of ap" and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires" + and off: "off = length tp div 2" and abc_unhalt: "\<forall> stp. (\<lambda> (as, am). as < length ap) (abc_steps_l (0, lm) ap stp)" - shows "\<forall> stp.\<not> is_final (steps (Suc 0, l, r) (tp_norm ap |+| mopup n, 0) stp)" -sorry + shows "\<forall> stp.\<not> is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp)" +using assms +proof(rule_tac allI, rule_tac notI) + fix stp + assume h: "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp)" + obtain as am where a: "abc_steps_l (0, lm) ap stp = (as, am)" + by(case_tac "abc_steps_l (0, lm) ap stp", auto) + then have b: "as < length ap" + using abc_unhalt + by(erule_tac x = stp in allE, simp) + have "\<exists> stpa\<ge>stp. crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires " + using assms b a + apply(rule_tac crsp_steps2, simp_all) + done + then obtain stpa where + "stpa\<ge>stp \<and> crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires" .. + then obtain s' l' r' where b: "(steps (Suc 0, l, r) (tp, 0) stpa) = (s', l', r') \<and> + stpa\<ge>stp \<and> crsp ly (as, am) (s', l', r') ires" + by(case_tac "steps (Suc 0, l, r) (tp, 0) stpa", auto) + hence c: + "(steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa) = (s', l', r')" + by(rule_tac tm_append_first_steps_eq, simp_all add: crsp.simps) + from b have d: "s' > 0 \<and> stpa \<ge> stp" + by(simp add: crsp.simps) + then obtain diff where e: "stpa = stp + diff" by (metis le_iff_add) + obtain s'' l'' r'' where f: + "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')" + using h + by(case_tac "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp", auto) + + then have "is_final (steps (s'', l'', r'') (tp @ shift (mopup n) off, 0) diff)" + by(auto intro: is_final_steps) + then have "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa)" + using e + by(simp add: steps_add f) + from this and c d show "False" by simp +qed end