tm: comparison thys/Abacus.thy

equal deleted inserted replaced

-:d5a0e25c4742
+:a9003e6d0463
 (* Title: thys/Abacus.thy
 Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 *)
-header {* Abacus Machines *}
+chapter {* Abacus Machines *}
 theory Abacus
 imports Turing_Hoare Abacus_Mopup
 begin
 TM in the finall TM.
 *}
 fun start_of :: "nat list \<Rightarrow> nat \<Rightarrow> 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"}
 assuming the TM of @{text "i"} starts from state @{text "ss"}
 within the overal layout @{text "lo"}.
 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)
+concat (drop (Suc (Suc n)) tps)")
-apply(rule_tac concat_drop_suc_iff, simp)
+apply (metis append_take_drop_id concat_append)
-apply(rule_tac concat_take_suc_iff, simp)
+apply(rule concat_drop_suc_iff,force)
-done
+by (simp add: concat_suc)
 declare append_assoc[simp]
 lemma map_of:  "n < length xs \<Longrightarrow> (map f xs) ! n = f (xs ! n)"
 by(auto)
 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)+
+by(auto)
-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)
+by(auto)
-done
 lemma [simp]: "length (layout_of aprog) = length aprog"
-apply(auto simp: layout_of.simps)
+by(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)
+by (auto simp: start_of.simps tms_of.simps layout_of.simps
-apply(auto simp: start_of.simps tms_of.simps layout_of.simps
+tpairs_of.simps ci_length take_Suc take_Suc_conv_app_nth)
-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 =
+using concat_suc.
-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)
+by(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(cases "ap ! n")
-apply(case_tac "ap ! n", auto simp: ci.simps length_findnth tinc_b_def tdec_b_def)
+by (auto simp: tms_of.simps tpairs_of.simps 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)
+proof(induct n)
-apply(case_tac "n < length (tms_of ap)", simp add: take_Suc_conv_app_nth, auto)
+case 0
-(*apply(subgoal_tac "length (tms_of ap ! n) mod 2 = 0")
+then show ?case by (auto simp add: take_Suc_conv_app_nth)
-apply arith
+next
-by auto
+case (Suc n)
-*)
+hence "n < length (tms_of ap) \<Longrightarrow> is_even (length (concat (take (Suc n) (tms_of ap))))"
-done
+unfolding take_Suc_conv_app_nth by fastforce
+with Suc show ?case by(cases "n < length (tms_of ap)", auto)
+qed
 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)"
 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)
+by(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(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"
 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)
+by (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)
+by(drule_tac b= b and ins = ins in step_eq_fetch', auto)
-done
 qed
 lemma step_eq_in:
 assumes layout: "ly = layout_of ap"
 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 (auto simp: Cons_replicate_eq)
-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 = []
 (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
+apply(auto simp:tape_of_nat_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>
+lemma inv_locate_a[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
+lemma inv_locate_b[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 [simp]:  "<[x::nat]> = Oc\<up>(Suc x)"
+lemma tape_nat[simp]:  "<[x::nat]> = Oc\<up>(Suc x)"
-apply(simp add: tape_of_nat_abv tape_of_nl_abv)
+apply(simp add: tape_of_nat_def tape_of_list_def)
 done
-lemma [simp]: " <([]::nat list)> = []"
+lemma tape_empty_list[simp]: " <([]::nat list)> = []"
-apply(simp add: tape_of_nl_abv)
+apply(simp add: tape_of_list_def)
 done
-lemma [simp]: "\<lbrakk>inv_locate_b (as, am) (q, aaa, Bk # xs) ires; \<exists>n. xs = Bk\<up>n\<rbrakk>
+lemma inv_locate[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 = 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
+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 \<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 "[]"])
 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 from_on_left_moving_to_check_left_moving[simp]: "inv_on_left_moving_in_middle_B (as, lm)
-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_abv tape_of_nat_list.simps)
+apply(case_tac [!] lista, simp_all add: tape_of_nat_def tape_of_list_def)
 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 )
 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_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 [1] lm2, auto simp:tape_of_nat_def)
-apply(case_tac [3] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto)
+apply(case_tac [3] lm2, auto simp:tape_of_nat_def)
-apply(case_tac [!] lista, simp_all add: tape_of_nat_abv tape_of_nat_list.simps)
+apply(case_tac [!] lista, simp_all add: tape_of_nat_def)
 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"
 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)
+using Suc_1 add.commute by metis
 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)
 (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)
+by(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"
 apply(case_tac b, auto simp: ci.simps adjust.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))"
+length tp = 2 * sum_list (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))"
+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)
 apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth adjust.simps length_of.simps
 split: abc_inst.splits)

changeset 288	a9003e6d0463
parent 285	447b433b67fa
child 290	6e1c03614d36