--- 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 \<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"}
@@ -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: "\<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
+ by(auto)
lemma div_apart_iff: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> \<Longrightarrow>
(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: "\<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
+ 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 \<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
+ using concat_suc.
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
+ 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 \<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
+ 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) \<Longrightarrow> 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:
"\<lbrakk>tp = concat (take as (tms_of ap));
@@ -615,8 +604,7 @@
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
+ 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 \<and> s \<le>
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 "\<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)
+ by (auto simp: Cons_replicate_eq)
thus ?thesis by blast
qed
next
@@ -1264,21 +1245,20 @@
(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)
+ 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 \<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)+
@@ -1289,15 +1269,15 @@
apply(case_tac mr, simp_all, auto)
done
-lemma [simp]: "<[x::nat]> = Oc\<up>(Suc x)"
-apply(simp add: tape_of_nat_abv tape_of_nl_abv)
+lemma tape_nat[simp]: "<[x::nat]> = Oc\<up>(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]: "\<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)
@@ -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 \<Longrightarrow>
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
\<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]:
@@ -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]:
"\<lbrakk>0 < abc_lm_v am n; inv_locate_n_b (as, am) (n, aaa, Bk # xs) ires\<rbrakk>
@@ -3486,9 +3465,7 @@
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
+ 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]:
"\<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"
@@ -3701,18 +3678,18 @@
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)