--- a/thys/Abacus.thy Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Abacus.thy Fri Dec 21 15:30:24 2018 +0100
@@ -362,10 +362,6 @@
done
qed
-lemma startof_not0[simp]: "0 < start_of ly as"
-apply(simp add: start_of.simps)
-done
-
lemma startof_ge1[simp]: "Suc 0 \<le> start_of ly as"
apply(simp add: start_of.simps)
done
@@ -423,11 +419,6 @@
apply(subgoal_tac "take (Suc as) xs = take as xs @ [xs ! as]", simp)
by auto
-lemma concat_take_suc_iff: "Suc n \<le> length tps \<Longrightarrow>
- concat (take n tps) @ (tps ! n) = concat (take (Suc n) tps)"
-apply(drule_tac concat_suc, simp)
-done
-
lemma concat_drop_suc_iff:
"Suc n < length tps \<Longrightarrow> concat (drop (Suc n) tps) =
tps ! Suc n @ concat (drop (Suc (Suc n)) tps)"
@@ -458,9 +449,6 @@
declare append_assoc[simp]
-lemma map_of: "n < length xs \<Longrightarrow> (map f xs) ! n = f (xs ! n)"
-by(auto)
-
lemma length_tms_of[simp]: "length (tms_of aprog) = length aprog"
apply(auto simp: tms_of.simps tpairs_of.simps)
done
@@ -470,7 +458,7 @@
abc_fetch as aprog = Some ins\<rbrakk>
\<Longrightarrow> ci ly (start_of ly as) ins = tms_of aprog ! as"
apply(simp add: tms_of.simps tpairs_of.simps
- abc_fetch.simps map_of del: map_append split: if_splits)
+ abc_fetch.simps del: map_append split: if_splits)
done
lemma t_split:"\<lbrakk>
@@ -488,41 +476,13 @@
apply(rule_tac ci_nth, auto)
done
-lemma math_sub: "\<lbrakk>x >= Suc 0; x - 1 = z\<rbrakk> \<Longrightarrow> x + y - Suc 0 = z + y"
-by auto
-
-lemma start_more_one: "as \<noteq> 0 \<Longrightarrow> start_of ly as >= Suc 0"
-apply(induct as, simp add: start_of.simps)
-apply(case_tac as, auto simp: start_of.simps)
-done
-
lemma div_apart: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk>
\<Longrightarrow> (x + y) div 2 = x div 2 + y div 2"
by(auto)
-lemma div_apart_iff: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> \<Longrightarrow>
- (x + y) mod 2 = 0"
-by(auto)
-
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>
- start_of ly (Suc as) = start_of ly as +
- length ((tms_of aprog) ! as) div 2"
- 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)"
- using concat_suc.
-
-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 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)
@@ -1247,10 +1207,6 @@
apply(simp add: tape_of_nat_def tape_of_list_def)
done
-lemma tape_empty_list[simp]: " <([]::nat list)> = []"
-apply(simp add: tape_of_list_def)
-done
-
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)
@@ -1338,9 +1294,6 @@
(*inv: from locate_b to after_write*)
-lemma not_even_then_odd[simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 0) "
-by arith
-
lemma div_rounding_down[simp]: "(2*q - Suc 0) div 2 = (q - 1)" "(Suc (2*q)) div 2 = q"
by arith+
@@ -1399,10 +1352,7 @@
done
qed
qed
-
-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 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)
@@ -1524,14 +1474,6 @@
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 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 "[]"])
-by(simp)
-
-
-
(*inv: from after_write to after_move*)
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"
@@ -1608,15 +1550,6 @@
apply(case_tac [!] rn, simp_all)
done
-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 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 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"
@@ -1646,12 +1579,6 @@
apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, simp)
done
-(*inv: from on_right_moving to after_write*)
-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 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"
@@ -1750,22 +1677,11 @@
apply(auto simp: inv_on_left_moving_norm.simps)
done
-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 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 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 Bk_plus_one[intro]: "\<exists>rna. Bk # Bk \<up> rn = Bk \<up> rna"
apply(rule_tac x = "Suc rn" in exI, simp)
done
@@ -1792,13 +1708,6 @@
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 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
-inv_check_left_moving_in_middle_2_on_left_moving_in_middle_B[of
- as lm n "[]" r], simp)
-done
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
@@ -2280,31 +2189,8 @@
by arith
qed
-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"
- 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 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 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
-
-
declare dec_inv_1.simps[simp del]
-
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>
@@ -2424,11 +2310,6 @@
apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits)
done
-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 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)
@@ -2454,12 +2335,6 @@
apply(simp add: dec_right_move.simps)
done
-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 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
@@ -2504,11 +2379,6 @@
apply(rule_tac x = "[m]" in exI, auto)
done
-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 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',
@@ -2518,14 +2388,6 @@
apply(simp add: tape_of_nl_cons split: if_splits)
done
-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)
-apply(rule_tac x = "lm1 @ [m ]" in exI, rule_tac x = "[]" in exI, simp)
-apply(simp add: tape_of_nl_cons split: if_splits)
-done
-
lemma 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)
@@ -2583,11 +2445,6 @@
apply(rule_tac x = lm1 in exI, simp)
done
-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
-
lemma dec_false_1[simp]:
"\<lbrakk>abc_lm_v am n = 0; inv_locate_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
\<Longrightarrow> False"
@@ -2647,63 +2504,12 @@
apply(simp_all only: exp_ind Nat.Suc_diff_le del: replicate_Suc, simp_all)
apply(auto simp: inv_on_left_moving_in_middle_B.simps split: if_splits)
apply(case_tac [!] m, simp_all)
-done
-
-lemma 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 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 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"
-apply(simp add: inv_locate_a.simps)
-apply(rule disjI1)
-apply(auto simp: inv_stop.simps at_begin_norm.simps)
-done
-
-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>
- inv_locate_b (as, abc_lm_s am n 0) (0, Oc # aaa, xs) ires"
-apply(simp)
-done
-
-lemma dec_false2:
- "inv_stop (as, abc_lm_s am n 0)
- (start_of (layout_of aprog) e, aaa, Bk # xs) ires = False"
-apply(auto simp: inv_stop.simps abc_lm_s.simps)
-apply(case_tac [!] am, auto)
-apply(case_tac [!] n, auto simp: tape_of_nl_cons split: if_splits)
-done
-
-lemma dec_false3:
- "inv_stop (as, abc_lm_s am n 0)
- (start_of (layout_of aprog) e, aaa, []) ires = False"
-apply(auto simp: inv_stop.simps abc_lm_s.simps)
-done
+ done
declare dec_inv_1.simps[simp del]
declare inv_locate_n_b.simps [simp del]
-
-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"
-apply(simp add: at_begin_fst_bwtn.simps inv_locate_n_b.simps )
-done
-lemma Suc_minus:"length am + tn = n
- \<Longrightarrow> Suc tn = Suc n - length am "
-apply(arith)
-done
-
lemma 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))
@@ -3037,10 +2843,6 @@
apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps)
done
-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>
@@ -3376,14 +3178,6 @@
done
qed
-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)"
-apply(case_tac b)
-apply(simp_all add: start_of.simps fetch.simps nth_append)
-done
-
lemma length_tp:
"\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow>
start_of ly (length ap) = Suc (length tp div 2)"
@@ -3511,7 +3305,7 @@
by(rule_tac tm_append_first_steps_eq, simp_all add: crsp.simps)
from b have d: "s' > 0 \<and> stpa \<ge> stp"
by(simp add: crsp.simps)
- then obtain diff where e: "stpa = stp + diff" by (metis le_iff_add)
+ then obtain diff where e: "stpa = stp + diff" by (metis le_iff_add)
obtain s'' l'' r'' where f:
"steps (1, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')"
using h