diff -r d5a0e25c4742 -r a9003e6d0463 thys/Abacus.thy --- a/thys/Abacus.thy Wed Jan 14 09:08:51 2015 +0000 +++ b/thys/Abacus.thy Wed Dec 19 16:10:58 2018 +0100 @@ -2,7 +2,7 @@ Author: Jian Xu, Xingyuan Zhang, and Christian Urban *) -header {* Abacus Machines *} +chapter {* Abacus Machines *} theory Abacus imports Turing_Hoare Abacus_Mopup @@ -203,7 +203,7 @@ fun start_of :: "nat list \ nat \ nat" where - "start_of ly x = (Suc (listsum (take x ly))) " + "start_of ly x = (Suc (sum_list (take x ly))) " text {* @{text "ci lo ss i"} complies Abacus instruction @{text "i"} @@ -451,10 +451,10 @@ 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 + concat (drop (Suc (Suc n)) tps)") + apply (metis append_take_drop_id concat_append) + apply(rule concat_drop_suc_iff,force) + by (simp add: concat_suc) declare append_assoc[simp] @@ -498,59 +498,48 @@ lemma div_apart: "\x mod (2::nat) = 0; y mod 2 = 0\ \ (x + y) div 2 = x div 2 + y div 2" -apply(drule mod_eqD)+ -apply(auto) -done + by(auto) lemma div_apart_iff: "\x mod (2::nat) = 0; y mod 2 = 0\ \ (x + y) mod 2 = 0" -apply(auto) -done +by(auto) lemma [simp]: "length (layout_of aprog) = length aprog" -apply(auto simp: layout_of.simps) -done +by(auto simp: layout_of.simps) lemma start_of_ind: "\as < length aprog; ly = layout_of aprog\ \ 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 + by (auto simp: start_of.simps tms_of.simps layout_of.simps + tpairs_of.simps ci_length take_Suc take_Suc_conv_app_nth) lemma concat_take_suc: "Suc n \ length xs \ 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 + using concat_suc. lemma [simp]: "\as < length aprog; (abc_fetch as aprog) = Some ins\ \ ci (layout_of aprog) (start_of (layout_of aprog) as) (ins) \ set (tms_of aprog)" -apply(insert ci_nth[of "layout_of aprog" aprog as], simp) -done + by(insert ci_nth[of "layout_of aprog" aprog as], simp) lemma [simp]: "length (tms_of ap) = length ap" by(auto simp: tms_of.simps tpairs_of.simps) lemma [intro]: "n < length ap \ 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 + apply(cases "ap ! n") + by (auto simp: tms_of.simps tpairs_of.simps ci.simps length_findnth tinc_b_def tdec_b_def) 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 -*) -done +proof(induct n) + case 0 + then show ?case by (auto simp add: take_Suc_conv_app_nth) +next + case (Suc n) + hence "n < length (tms_of ap) \ is_even (length (concat (take (Suc n) (tms_of ap))))" + unfolding take_Suc_conv_app_nth by fastforce + with Suc show ?case by(cases "n < length (tms_of ap)", auto) +qed lemma tpa_states: "\tp = concat (take as (tms_of ap)); @@ -615,8 +604,7 @@ tp1 = concat (take as (tms_of ap)) \ 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 + by(rule_tac tpa_states, simp, simp add: abc_fetch.simps split: if_splits) 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) @@ -625,8 +613,7 @@ 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) + by(case_tac ins, auto simp: ci.simps length_findnth tinc_b_def tdec_b_def) next show "length tp1 div 2 < s \ s \ length tp1 div 2 + length (ci ly (start_of ly as) ins) div 2" @@ -694,17 +681,12 @@ 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 + by (simp_all only: length_ci_inc length_ci_dec length_ci_goto, auto) 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 + by(drule_tac b= b and ins = ins in step_eq_fetch', auto) qed @@ -1245,8 +1227,7 @@ (is "\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) + by (auto simp: Cons_replicate_eq) thus ?thesis by blast qed next @@ -1264,21 +1245,20 @@ (is "\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) + apply(auto simp:tape_of_nat_def) by(case_tac "rn::nat", simp, simp) thus ?thesis by blast qed qed -lemma [simp]: "inv_locate_a (as, am) (q, aaa, []) ires \ +lemma inv_locate_a[simp]: "inv_locate_a (as, am) (q, aaa, []) ires \ 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 +lemma inv_locate_b[simp]: "inv_locate_b (as, am) (q, aaa, Oc # xs) ires \ inv_locate_b (as, am) (q, Oc # aaa, xs) ires" apply(simp only: inv_locate_b.simps in_middle.simps) apply(erule exE)+ @@ -1289,15 +1269,15 @@ apply(case_tac mr, simp_all, auto) done -lemma [simp]: "<[x::nat]> = Oc\(Suc x)" -apply(simp add: tape_of_nat_abv tape_of_nl_abv) +lemma tape_nat[simp]: "<[x::nat]> = Oc\(Suc x)" +apply(simp add: tape_of_nat_def tape_of_list_def) done -lemma [simp]: " <([]::nat list)> = []" -apply(simp add: tape_of_nl_abv) +lemma tape_empty_list[simp]: " <([]::nat list)> = []" +apply(simp add: tape_of_list_def) done -lemma [simp]: "\inv_locate_b (as, am) (q, aaa, Bk # xs) ires; \n. xs = Bk\n\ +lemma inv_locate[simp]: "\inv_locate_b (as, am) (q, aaa, Bk # xs) ires; \n. xs = Bk\n\ \ 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) @@ -1628,8 +1608,8 @@ 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 + apply(drule_tac length_equal, simp) + by (metis (no_types, lifting) add_diff_inverse_nat append.assoc append_eq_append_conv length_append length_replicate list.inject) lemma [simp]: "inv_locate_b (as, am) (n, aaa, []) ires \ inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) @@ -1819,15 +1799,14 @@ 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) +lemma from_on_left_moving_to_check_left_moving[simp]: "inv_on_left_moving_in_middle_B (as, lm) (s, Bk # list, Bk # r) ires \ 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_abv tape_of_nat_list.simps) +apply(case_tac [!] lista, simp_all add: tape_of_nat_def tape_of_list_def) done lemma [simp]: @@ -1895,11 +1874,11 @@ 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_nat_abv tape_of_nl_abv tape_of_nat_list.simps) +apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_def tape_of_list_def tape_of_nat_list.simps) apply(case_tac [!] a, simp_all) -apply(case_tac [1] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto) -apply(case_tac [3] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto) -apply(case_tac [!] lista, simp_all add: tape_of_nat_abv tape_of_nat_list.simps) +apply(case_tac [1] lm2, auto simp:tape_of_nat_def) +apply(case_tac [3] lm2, auto simp:tape_of_nat_def) +apply(case_tac [!] lista, simp_all add: tape_of_nat_def) done lemma [simp]: @@ -3320,7 +3299,7 @@ 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) + using Suc_1 add.commute by metis lemma [elim]: "\0 < abc_lm_v am n; inv_locate_n_b (as, am) (n, aaa, Bk # xs) ires\ @@ -3486,9 +3465,7 @@ abc_fetch as ap = Some (Dec n e)\ \ 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 + by(auto simp: inv_stop.simps crsp.simps abc_step_l.simps startof_Suc2) lemma crsp_step_dec_b_suc: assumes layout: "ly = layout_of ap" @@ -3693,7 +3670,7 @@ lemma length_tp'[simp]: "\ly = layout_of ap; tp = tm_of ap\ \ - length tp = 2 * listsum (take (length ap) (layout_of ap))" + length tp = 2 * sum_list (take (length ap) (layout_of ap))" proof(induct ap arbitrary: ly tp rule: rev_induct) case Nil thus "?case" @@ -3701,18 +3678,18 @@ next fix x xs ly tp assume ind: "\ly tp. \ly = layout_of xs; tp = tm_of xs\ \ - length tp = 2 * listsum (take (length xs) (layout_of xs))" + length tp = 2 * sum_list (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))" + have c: "length tp' = 2 * sum_list (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])))" + sum_list (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)