--- a/thys/Abacus.thy Wed Dec 19 16:47:10 2018 +0100
+++ b/thys/Abacus.thy Fri Dec 21 12:31:36 2018 +0100
@@ -285,8 +285,8 @@
*}
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)
+lemma start_of_nonzero[simp]: "start_of ly as > 0" "(start_of ly as = 0) = False"
+apply(auto simp: start_of.simps)
done
lemma abc_steps_l_0: "abc_steps_l ac ap 0 = ac"
@@ -461,7 +461,7 @@
lemma map_of: "n < length xs \<Longrightarrow> (map f xs) ! n = f (xs ! n)"
by(auto)
-lemma [simp]: "length (tms_of aprog) = length aprog"
+lemma length_tms_of[simp]: "length (tms_of aprog) = length aprog"
apply(auto simp: tms_of.simps tpairs_of.simps)
done
@@ -504,7 +504,7 @@
(x + y) mod 2 = 0"
by(auto)
-lemma [simp]: "length (layout_of aprog) = length aprog"
+lemma length_layout_of[simp]: "length (layout_of aprog) = length aprog"
by(auto simp: layout_of.simps)
lemma start_of_ind: "\<lbrakk>as < length aprog; ly = layout_of aprog\<rbrakk> \<Longrightarrow>
@@ -517,16 +517,13 @@
concat (take (Suc n) xs) = concat (take n xs) @ (xs ! n)"
using concat_suc.
-lemma [simp]:
+lemma ci_in_set[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)"
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"
+lemma length_tms_of_elem_even[intro]: "n < length ap \<Longrightarrow> length (tms_of ap ! n) mod 2 = 0"
apply(cases "ap ! n")
by (auto simp: tms_of.simps tpairs_of.simps ci.simps length_findnth tinc_b_def tdec_b_def)
@@ -1125,43 +1122,20 @@
declare findnth_inv.simps[simp del]
-lemma [simp]:
+lemma x_is_2n_arith[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
+
+lemma between_sucs:"x < Suc n \<Longrightarrow> \<not> x < n \<Longrightarrow> x = n" by auto
+
+lemma fetch_findnth[simp]:
+ "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 = Suc 0\<rbrakk> \<Longrightarrow> fetch (findnth n) a Oc = (R, Suc a)"
+ "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> fetch (findnth n) a Oc = (R, a)"
+ "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> fetch (findnth n) a Bk = (R, Suc a)"
+ "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 = Suc 0\<rbrakk> \<Longrightarrow> fetch (findnth n) a Bk = (W1, a)"
+by(cases a;induct n;force simp: length_findnth nth_append dest!:between_sucs)+
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]
@@ -1179,27 +1153,27 @@
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"
-by (metis replicate_0 replicate_Suc)
-
-lemma [intro]: "at_begin_norm (as, am) (q, aaa, []) ires
+lemma replicate_once[intro]: "\<exists>rn. [Bk] = Bk \<up> rn"
+by (metis replicate.simps)
+
+lemma at_begin_norm_Bk[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
+lemma at_begin_fst_bwtn_Bk[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
+lemma at_begin_fst_awtn_Bk[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
+lemma inv_locate_a_Bk[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)
@@ -1295,22 +1269,15 @@
apply(case_tac [!] n, simp_all)
done
-lemma [simp]: "(Oc # r = Bk \<up> rn) = False"
+lemma repeat_Bk_no_Oc[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"
+lemma repeat_Bk[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]:
+lemma inv_locate_b_Oc_via_a[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
@@ -1334,7 +1301,7 @@
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;
+lemma inv_locate_a_Bk_via_b[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)
@@ -1359,7 +1326,7 @@
done
-lemma [simp]: "inv_locate_b (as, am) (q, l, []) ires
+lemma inv_locate_b_Bk[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)+
@@ -1371,68 +1338,31 @@
(*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"
+lemma not_even_then_odd[simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 0) "
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"
+lemma div_rounding_down[simp]: "(2*q - Suc 0) div 2 = (q - 1)" "(Suc (2*q)) div 2 = q"
+by arith+
+
+lemma even_plus_one_odd[simp]: "x mod 2 = 0 \<Longrightarrow> Suc x mod 2 = Suc 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 odd_plus_one_even[simp]: "x mod 2 = Suc 0 \<Longrightarrow> Suc x mod 2 = 0"
+by arith
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
+ done
(*inv: from locate_b to after_write*)
-lemma [simp]:
+lemma findnth_inv_layout_of_via_crsp[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
+by(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"
@@ -1470,10 +1400,11 @@
qed
qed
-lemma [intro]: "inv_locate_a (as, lm) (0, Bk # Bk # ires, <lm> @ Bk \<up> x) ires"
+lemma inv_locate_aI[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"
+lemma inv_locate_a_via_crsp[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
@@ -1578,24 +1509,6 @@
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)))
@@ -1611,7 +1524,7 @@
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>
+lemma inv_after_write_via_locate_b[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 "[]"])
@@ -1620,52 +1533,49 @@
(*inv: from after_write to after_move*)
-lemma [simp]: "inv_after_write (as, lm) (x, l, Oc # r) ires
+lemma inv_after_move_Oc_via_write[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)
+lemma inv_after_write_Suc[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 )
+apply(auto simp: inv_after_write.simps )
done
(*inv: from after_move to after_clear*)
-lemma [simp]: "inv_after_move (as, lm) (s, l, Oc # r) ires
+lemma inv_after_clear_Bk_via_Oc[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>
+ assumes "inv_after_move (as, lm) (s, l, Bk # r) ires"
+ shows "(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
+proof (cases l)
+ case (Cons a list)
+ from assms Cons show ?thesis
+ apply(simp only: inv_after_move.simps inv_on_left_moving.simps)
+ apply(rule conjI, force, 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) apply (auto split:if_splits)
+ apply(case_tac [1-2] rn, simp_all)
+ by(case_tac [!] lm2, simp_all add: tape_of_nl_cons split: if_splits)
+next
+ case Nil thus ?thesis using assms
+ unfolding inv_after_move.simps inv_on_left_moving.simps
+ by (auto split:if_splits)
+qed
lemma inv_after_move_2_inv_on_left_moving_B[simp]:
@@ -1684,11 +1594,6 @@
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"
@@ -1703,17 +1608,17 @@
apply(case_tac [!] rn, simp_all)
done
-lemma [simp]: "inv_after_clear (as, lm) (x, l, []) ires\<Longrightarrow>
+lemma inv_after_clear_singleton_Bk[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
+lemma inv_on_right_moving_Bk[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
+lemma inv_on_right_moving_Oc[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,
@@ -1735,31 +1640,31 @@
apply(case_tac mr, auto simp: split: if_splits)
done
-lemma [simp]: "inv_on_right_moving (as, lm) (x, l, []) ires\<Longrightarrow>
+lemma inv_on_right_moving_singleton_Bk[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
+lemma inv_after_write_singleton_Oc[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)
+lemma no_inv_on_left_moving_in_middle_B_Oc[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
+lemma no_inv_on_left_moving_norm_Bk[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]:
+lemma inv_on_left_moving_in_middle_B_Bk[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"
@@ -1773,7 +1678,7 @@
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;
+lemma inv_on_left_moving_norm_Oc_Oc[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"
@@ -1785,13 +1690,13 @@
apply(case_tac ml, auto simp: split: if_splits)
done
-lemma [simp]: "inv_on_left_moving_norm (as, lm) (s, [], Oc # r) ires
+lemma inv_on_left_moving_in_middle_B_Bk_Oc[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
+lemma inv_on_left_moving_Oc_cases[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)
@@ -1809,22 +1714,22 @@
apply(case_tac [!] lista, simp_all add: tape_of_nat_def tape_of_list_def)
done
-lemma [simp]:
+lemma inv_check_left_moving_in_middle_no_Bk[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]:
+lemma inv_check_left_moving_on_leftmost_Bk_Bk[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)
+lemma inv_check_left_moving_on_leftmost_no_Oc[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)
+lemma inv_check_left_moving_in_middle_Oc_Bk[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
@@ -1841,53 +1746,53 @@
apply(case_tac a, simp, simp)
done
-lemma [simp]: "inv_on_left_moving_norm (as, lm) (s, l, []) ires = False"
+lemma inv_on_left_moving_norm_no_empty[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>
+lemma inv_on_left_moving_Bk[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"
+lemma inv_on_left_moving_no_empty[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
+lemma inv_on_left_moving_cases_left[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 Bk_plus_one[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_nat_def tape_of_list_def tape_of_nat_list.simps)
-apply(case_tac [!] a, simp_all)
-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]:
+assumes "inv_check_left_moving_in_middle (as, lm) (s, Bk # list, Oc # r) ires"
+shows "inv_on_left_moving_in_middle_B (as, lm) (s', list, Bk # Oc # r) ires"
+ using assms
+ 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_def tape_of_list_def tape_of_nat_list.simps)
+ apply(case_tac [!] a, simp_all)
+ 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 inv_check_left_moving_in_middle_Bk_Oc[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]:
+lemma inv_on_left_moving_in_middle_B_Bk_Oc_via_check[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
@@ -1895,7 +1800,7 @@
as lm n "[]" r], simp)
done
-lemma [simp]: "inv_check_left_moving_in_middle (as, lm)
+lemma inv_on_left_moving_norm_Oc_Oc_via_middle[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
@@ -1910,7 +1815,7 @@
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
+lemma inv_check_left_moving_Oc_cases[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,
@@ -1919,58 +1824,57 @@
done
(*inv: check_left_moving to after_left_moving*)
-lemma [simp]: "inv_check_left_moving (as, lm) (s, l, Bk # r) ires
+lemma inv_after_left_moving_Bk_via_check[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
+lemma inv_after_left_moving_Bk_empty_via_check[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
+lemma inv_stop_Bk_move[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
+lemma inv_stop_Bk_empty[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>
+lemma inv_stop_indep_fst[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"
+lemma inv_after_clear_no_Oc[simp]: "inv_after_clear (as, lm) (s, aaa, Oc # xs) ires= False"
apply(auto simp: inv_after_clear.simps )
done
-lemma [simp]:
+lemma inv_after_left_moving_no_Oc[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"
+lemma inv_after_clear_Suc_nonempty[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)))
+lemma inv_on_left_moving_Suc_nonempty[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> []"
+lemma inv_check_left_moving_Suc_nonempty[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 numeral_4_eq_4: "4 = Suc (Suc (Suc (Suc 0)))"
-by arith
+ done
lemma tinc_correct_pre:
assumes layout: "ly = layout_of ap"
@@ -2003,12 +1907,12 @@
apply(simp add: inc_inv.simps)
apply(case_tac c, case_tac [2] aa)
apply(auto simp: Let_def step.simps tinc_b_def 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_2_eq_2 numeral_3_eq_3
- numeral_4_eq_4 numeral_6_eq_6 numeral_7_eq_7 numeral_8_eq_8 numeral_9_eq_9)
+ apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def
+ numeral)
done
qed
qed
-
+
lemma tinc_correct:
assumes layout: "ly = layout_of ap"
and inv_start: "inv_locate_a (as, lm) (n, l, r) ires"
@@ -2024,7 +1928,7 @@
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"
+lemma is_even_4[simp]: "(4::nat) * n mod 2 = 0"
apply(arith)
done
@@ -2194,19 +2098,62 @@
else False)"
declare fetch.simps[simp del]
-lemma [simp]:
+
+
+lemma x_plus_helpers:
+ "x + 4 = Suc (x + 3)"
+ "x + 5 = Suc (x + 4)"
+ "x + 6 = Suc (x + 5)"
+ "x + 7 = Suc (x + 6)"
+ "x + 8 = Suc (x + 7)"
+ "x + 9 = Suc (x + 8)"
+ "x + 10 = Suc (x + 9)"
+ "x + 11 = Suc (x + 10)"
+ "x + 12 = Suc (x + 11)"
+ "x + 13 = Suc (x + 12)"
+ "14 + x = Suc (x + 13)"
+ "15 + x = Suc (x + 14)"
+ "16 + x = Suc (x + 15)"
+ by auto
+
+lemma fetch_Dec[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 adjust.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 adjust.simps shift.simps tdec_b_def)
-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)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Bk
+ = (L, start_of ly as + 2*n + 13)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (Suc (Suc (2 * n)))) Oc
+ = (R, start_of ly as + 2*n + 2)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (Suc (Suc (2 * n)))) Bk
+ = (L, start_of ly as + 2*n + 3)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 4) Oc = (W0, start_of ly as + 2*n + 3)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 4) Bk = (R, start_of ly as + 2*n + 4)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 5) Bk = (R, start_of ly as + 2*n + 5)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 6) Bk = (L, start_of ly as + 2*n + 6)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 6) Oc = (L, start_of ly as + 2*n + 7)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 7) Bk = (L, start_of ly as + 2*n + 10)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 8) Bk = (W1, start_of ly as + 2*n + 7)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 8) Oc = (R, start_of ly as + 2*n + 8)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 9) Bk = (L, start_of ly as + 2*n + 9)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 9) Oc = (R, start_of ly as + 2*n + 8)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 10) Bk = (R, start_of ly as + 2*n + 4)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 10) Oc = (W0, start_of ly as + 2*n + 9)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 11) Oc = (L, start_of ly as + 2*n + 10)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 11) Bk = (L, start_of ly as + 2*n + 11)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 12) Oc = (L, start_of ly as + 2*n + 10)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 12) Bk = (R, start_of ly as + 2*n + 12)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 13) Bk = (R, start_of ly as + 2*n + 16)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (14 + 2 * n) Oc = (L, start_of ly as + 2*n + 13)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (14 + 2 * n) Bk = (L, start_of ly as + 2*n + 14)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (15 + 2 * n) Oc = (L, start_of ly as + 2*n + 13)"
+ "fetch (ci (ly) (start_of ly as) (Dec n e)) (15 + 2 * n) Bk = (R, start_of ly as + 2*n + 15)"
+ "fetch (ci (ly) (start_of (ly) as) (Dec n e)) (16 + 2 * n) Bk = (R, start_of (ly) e)"
+ unfolding x_plus_helpers fetch.simps
+ by(auto simp: ci.simps findnth.simps
+ nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
+
+lemma steps_start_of_invb_inv_locate_a1[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),
@@ -2217,7 +2164,7 @@
apply(case_tac r, simp_all)
done
-lemma [simp]:
+lemma steps_start_of_invb_inv_locate_a2[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),
@@ -2333,278 +2280,32 @@
by arith
qed
-lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as < e;
+lemma abc_fetch_contrE[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;
+ by(drule_tac start_of_ge, auto)
+
+lemma abc_fetch_contrE2[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);
+lemma abc_fetch_contrE3[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
+lemma fetch_c_Oc[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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.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 adjust.simps)
-done
declare dec_inv_1.simps[simp del]
-lemma [simp]:
+lemma start_of_ineq1[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>
@@ -2626,7 +2327,7 @@
apply(case_tac "e = as", simp, simp)
done
-lemma [simp]: "\<lbrakk>abc_fetch as aprog = Some (Dec n e); ly = layout_of aprog\<rbrakk>
+lemma start_of_ineq2[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>
@@ -2647,15 +2348,15 @@
apply(case_tac "e = as", simp, simp)
done
-lemma [simp]: "inv_locate_b (as, lm) (n, [], []) ires = False"
+lemma inv_locate_b_nonempty[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"
+lemma inv_locate_b_no_Bk[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 [simp]:
+lemma dec_first_on_right_moving_Oc[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)
@@ -2667,12 +2368,12 @@
apply(case_tac [!] mr, auto)
done
-lemma [simp]:
+lemma dec_first_on_right_moving_Bk_nonempty[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]:
+lemma replicateE[elim]:
"\<lbrakk>\<not> length lm1 < length am;
am @ replicate (length lm1 - length am) 0 @ [0::nat] =
lm1 @ m # lm2;
@@ -2682,7 +2383,7 @@
apply(drule_tac length_equal, simp)
done
-lemma [simp]:
+lemma dec_after_clear_Bk_strip_hd[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
@@ -2696,7 +2397,7 @@
apply(case_tac [!] mr, auto)
done
-lemma [simp]:
+lemma dec_first_on_right_moving_dec_after_clear_cases[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,
@@ -2713,27 +2414,27 @@
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>
+lemma dec_after_clear_Bk_via_Oc[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>
+lemma dec_right_move_Bk_via_clear_Bk[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>
+lemma dec_right_move_Bk_via_clear_empty[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>
+lemma dec_right_move_Bk_Bk_via_clear[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"
+lemma dec_right_move_no_Oc[simp]:"dec_right_move (as, am) (s, l, Oc # r) ires = False"
apply(auto simp: dec_right_move.simps)
done
@@ -2743,27 +2444,27 @@
apply(auto simp: dec_right_move.simps dec_check_right_move.simps split: if_splits)
done
-lemma [simp]: "(<lm::nat list> = []) = (lm = [])"
+lemma lm_iff_empty[simp]: "(<lm::nat list> = []) = (lm = [])"
apply(case_tac lm, simp_all add: tape_of_nl_cons)
done
-lemma [simp]:
+lemma dec_right_move_asif_Bk_singleton[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>
+lemma dec_check_right_move_Bk_via_move[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> []"
+lemma dec_check_right_move_nonempty[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>
+lemma dec_check_right_move_Oc_tail[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,
@@ -2772,7 +2473,7 @@
-lemma [simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, Bk # r) ires\<rbrakk>
+lemma dec_left_move_Bk_tail[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)
@@ -2781,35 +2482,35 @@
apply(rule_tac [!] x = "(Suc rn)" in exI, simp_all)
done
-lemma [simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, []) ires\<rbrakk>
+lemma dec_left_move_tail[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"
+lemma dec_left_move_no_Oc[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
+lemma dec_left_move_nonempty[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])
+lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bks[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])
+lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bk[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>
+lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bks_rev[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)
@@ -2817,7 +2518,7 @@
apply(simp add: tape_of_nl_cons split: if_splits)
done
-lemma [simp]: "lm1 \<noteq> [] \<Longrightarrow>
+lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bk_rev[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)
@@ -2825,17 +2526,17 @@
apply(simp add: tape_of_nl_cons split: if_splits)
done
-lemma [simp]: "dec_left_move (as, am) (s, l, Bk # r) ires
+lemma inv_on_left_moving_Bk_tail[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]: "dec_left_move (as, am) (s, l, []) ires
+lemma inv_on_left_moving_tail[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
+lemma dec_on_right_moving_Oc_mv[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,
@@ -2844,17 +2545,17 @@
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
+lemma dec_after_write_Oc_via_Bk[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
+lemma dec_after_write_Oc_empty[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
+lemma dec_on_right_moving_Oc_move[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)+
@@ -2865,24 +2566,24 @@
apply(case_tac mr, auto)
done
-lemma [simp]: "dec_on_right_moving (as, am) (s, l, r) ires\<Longrightarrow> l \<noteq> []"
+lemma dec_on_right_moving_nonempty[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
+lemma dec_after_clear_Bk_tail[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
+lemma dec_after_clear_tail[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]:
+lemma inv_stop_abc_lm_s_nonempty[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
@@ -2906,7 +2607,7 @@
simp add: exp_ind del: replicate.simps, simp)
done
-lemma [simp]:
+lemma inv_on_left_moving_Bk_tl[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)
@@ -2928,7 +2629,7 @@
done
-lemma [simp]:
+lemma inv_on_left_moving_tl[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)
@@ -2948,15 +2649,15 @@
apply(case_tac [!] m, simp_all)
done
-lemma [simp]: "\<lbrakk>am ! n = (0::nat); n < length am\<rbrakk> \<Longrightarrow> am[n := 0] = am"
+lemma update_zero_to_zero[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"
+lemma abc_lm_v_zero: "\<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]:
+lemma inv_locate_a_via_stop[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"
@@ -2965,7 +2666,7 @@
apply(auto simp: inv_stop.simps at_begin_norm.simps)
done
-lemma [simp]:
+lemma inv_locate_b_cases_via_stop[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>
@@ -2987,16 +2688,11 @@
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]:
+lemma inv_locate_n_b_Oc_via_at_begin_fst_bwtn[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"
@@ -3008,21 +2704,7 @@
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]:
+lemma dec_first_on_right_moving_Oc_via_inv_locate_n_b[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"
@@ -3049,24 +2731,20 @@
simp add: Suc_diff_le exp_ind del: replicate.simps, simp)
done
-lemma [simp]: "inv_on_left_moving (as, am) (s, [], r) ires
+lemma inv_on_left_moving_nonempty[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]:
+lemma inv_check_left_moving_startof_nonempty[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);
+lemma start_of_lessE[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"
@@ -3141,7 +2819,7 @@
apply(rule_tac x = stp in exI, simp)
done
-lemma [simp]:
+lemma crsp_abc_step_via_stop[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"
@@ -3301,20 +2979,20 @@
lemma fix_add: "fetch ap ((x::nat) + 2*n) b = fetch ap (2*n + x) b"
using Suc_1 add.commute by metis
-lemma [elim]:
+lemma inv_locate_n_b_Bk_elim[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]:
+ done
+
+lemma inv_locate_n_b_nonemptyE[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
+lemma no_Ocs_dec_after_write[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)+
@@ -3323,7 +3001,7 @@
apply(case_tac a, simp only: takeWhile.simps , simp_all split: if_splits)
done
-lemma [simp]:
+lemma fewer_Ocs_dec_on_right_moving[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>
@@ -3335,7 +3013,7 @@
apply(case_tac mr, auto split: if_splits)
done
-lemma [simp]:
+lemma more_Ocs_dec_after_clear[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 +
@@ -3346,21 +3024,24 @@
apply(simp split: if_splits )
done
-lemma [simp]:
+lemma more_Ocs_dec_after_clear2[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
+lemma inv_check_left_moving_nonemptyE[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]:
+lemma inv_check_left_moving_nonempty[simp]:
+ "inv_check_left_moving (as, lm) (s, [], Oc # list) ires = False"
+ by auto
+
+lemma inv_locate_n_b_Oc_via_at_begin_norm[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"
@@ -3372,7 +3053,7 @@
apply(case_tac "lm2", auto simp: tape_of_nl_cons split: if_splits)
done
-lemma [simp]:
+lemma inv_locate_n_b_Oc_via_at_begin_fst_awtn[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"
@@ -3386,13 +3067,13 @@
apply(auto)
done
-lemma [simp]:
+lemma inv_locate_n_b_Oc_via_inv_locate_n_a[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]:
+lemma more_Oc_dec_on_right_moving[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>
@@ -3458,7 +3139,7 @@
qed
qed
-lemma [simp]:
+lemma crsp_abc_step_l_start_of[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;
@@ -3647,10 +3328,7 @@
apply(simp add: layout_of.simps)
done
-lemma [simp]: "length (layout_of xs) = length xs"
-by(simp add: layout_of.simps)
-
-lemma [simp]:
+lemma map_start_of_layout[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)
@@ -3698,7 +3376,7 @@
done
qed
-lemma [simp]:
+lemma fetch_Nops[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)"