--- 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
--- a/thys/Abacus_Defs.thy Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Abacus_Defs.thy Fri Dec 21 15:30:24 2018 +0100
@@ -2,7 +2,7 @@
Author: Jian Xu, Xingyuan Zhang, and Christian Urban
*)
-header {* Alternative Definitions for Translating Abacus Machines to TMs *}
+chapter {* Alternative Definitions for Translating Abacus Machines to TMs *}
theory Abacus_Defs
imports Abacus
@@ -13,7 +13,7 @@
fun address :: "abc_prog \<Rightarrow> nat \<Rightarrow> nat"
where
- "address p x = (Suc (listsum (take x (layout p)))) "
+ "address p x = (Suc (sum_list (take x (layout p)))) "
abbreviation
"TMGoto \<equiv> [(Nop, 1), (Nop, 1)]"
--- a/thys/Abacus_Hoare.thy Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Abacus_Hoare.thy Fri Dec 21 15:30:24 2018 +0100
@@ -240,6 +240,7 @@
apply(rule_tac abc_comp_frist_steps_halt_eq', simp_all)
done
+
lemma abc_comp_second_step_eq:
assumes exec: "abc_step_l (s, lm) (abc_fetch s B) = (sa, lma)"
shows "abc_step_l (s + length A, lm) (abc_fetch (s + length A) (A [+] B))
--- a/thys/NatBijection.thy Fri Dec 21 12:31:36 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,274 +0,0 @@
-theory NatBijection
-imports Main Parity "~~/src/HOL/Library/Discrete"
-begin
-
-declare One_nat_def[simp del]
-
-fun oddfactor :: "nat \<Rightarrow> nat" where
- [simp del]: "oddfactor n = (if n = 0 then 0
- else if even n then oddfactor (n div 2) else ((n - 1) div 2))"
-
-fun evenfactor :: "nat \<Rightarrow> nat" where
- [simp del]: "evenfactor n = (if n = 0 then 0
- else if even n then 2 * evenfactor (n div 2) else 1)"
-
-lemma oddfactor [simp]:
- "oddfactor 0 = 0"
- "odd n \<Longrightarrow> oddfactor n = (n - 1) div 2"
- "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)"
-by (simp_all add: oddfactor.simps)
-
-lemma evenfactor [simp]:
- "evenfactor 0 = 0"
- "odd n \<Longrightarrow> evenfactor n = 1"
- "even n \<Longrightarrow> evenfactor n = 2 * evenfactor (n div 2)"
-apply(simp_all add: evenfactor.simps)
-apply(case_tac n)
-apply(simp_all)
-done
-
-fun penc :: "(nat \<times> nat) \<Rightarrow> nat" where
- "penc (m, n) = (2 ^ m) * (2 * n + 1) - 1"
-
-fun pdec :: "nat \<Rightarrow> nat \<times> nat" where
- "pdec z = (Discrete.log (evenfactor (Suc z)), oddfactor (Suc z))"
-
-lemma q2: "pdec (penc m) = m"
-apply(case_tac m)
-apply(simp)
-apply(simp only: penc.simps pdec.simps)
-apply(case_tac m)
-apply(simp only: penc.simps pdec.simps)
-apply(subst y1)
-apply(subst y2)
-apply(simp)
-done
-
-
-lemma oddfactor_odd:
- "oddfactor n = 0 \<or> odd (oddfactor n)"
-apply(induct n rule: nat_less_induct)
-apply(case_tac "n = 0")
-apply(simp)
-apply(case_tac "odd n")
-apply(auto)
-done
-
-lemma bigger: "oddfactor (Suc n) > 0"
-apply(induct n rule: nat_less_induct)
-apply(case_tac "n = 0")
-apply(simp)
-apply(case_tac "odd n")
-apply(auto)
-apply(drule_tac x="n div 2" in spec)
-apply(drule mp)
-apply(auto)
-by (smt numeral_2_eq_2 odd_nat_plus_one_div_two)
-
-fun pencode :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
- "pencode m n = (2 ^ m) * (2 * n + 1) - 1"
-
-fun pdecode2 :: "nat \<Rightarrow> nat" where
- "pdecode2 z = (oddfactor (Suc z) - 1) div 2"
-
-fun pdecode1 :: "nat \<Rightarrow> nat" where
- "pdecode1 z = Discrete.log ((Suc z) div (oddfactor (Suc z)))"
-
-lemma k:
- "odd n \<Longrightarrow> oddfactor (2 ^ m * n) = n"
-apply(induct m)
-apply(simp_all)
-done
-
-lemma ww: "\<exists>k. n = 2 ^ k * oddfactor n"
-apply(induct n rule: nat_less_induct)
-apply(case_tac "n=0")
-apply(simp)
-apply(case_tac "odd n")
-apply(simp)
-apply(rule_tac x="0" in exI)
-apply(simp)
-apply(simp)
-apply(drule_tac x="n div 2" in spec)
-apply(erule impE)
-apply(simp)
-apply(erule exE)
-apply(rule_tac x="Suc k" in exI)
-apply(simp)
-by (metis div_mult_self2_is_id even_mult_two_ex nat_mult_assoc nat_mult_commute zero_neq_numeral)
-
-
-lemma test: "x = y \<Longrightarrow> 2 * x = 2 * y"
-by simp
-
-lemma m: "0 < n ==> 2 ^ Discrete.log (n div (oddfactor n)) = n div (oddfactor n)"
-apply(induct n rule: nat_less_induct)
-apply(case_tac "n=0")
-apply(simp)
-apply(case_tac "odd n")
-apply(simp)
-apply(drule_tac x="n div 2" in spec)
-apply(drule mp)
-apply(auto)[1]
-apply(drule mp)
-apply (metis One_nat_def Suc_lessI div_2_gt_zero odd_1_nat)
-apply(subst (asm) oddfactor(3)[symmetric])
-apply(simp)
-apply(subst (asm) oddfactor(3)[symmetric])
-apply(simp)
-apply(subgoal_tac "n div 2 div oddfactor n = n div (oddfactor n) div 2")
-prefer 2
-apply (metis div_mult2_eq nat_mult_commute)
-apply(simp only: log_half)
-apply(case_tac "n div oddfactor n = 0")
-apply(simp)
-apply(simp del: oddfactor)
-apply(drule test)
-apply(subst (asm) power.simps(2)[symmetric])
-apply(subgoal_tac "Suc (Discrete.log (n div oddfactor n) - 1) = Discrete.log (n div oddfactor n)")
-prefer 2
-apply (smt log.simps Suc_1 div_less div_mult_self1_is_id log_half log_zero numeral_1_eq_Suc_0 numeral_One odd_1_nat odd_nat_plus_one_div_two one_less_numeral_iff power_one_right semiring_norm(76))
-apply(simp only: One_nat_def)
-apply(subst dvd_mult_div_cancel)
-apply (smt Suc_1 div_by_0 div_mult_self2_is_id oddfactor_odd dvd_power even_Suc even_numeral_nat even_product_nat nat_even_iff_2_dvd power_0 ww)
-apply(simp (no_asm))
-done
-
-lemma m1: "n div oddfactor n * oddfactor n = n"
-apply(induct n rule: nat_less_induct)
-apply(case_tac "n=0")
-apply(simp)
-apply(case_tac "odd n")
-apply(simp)
-apply(simp)
-apply(drule_tac x="n div 2" in spec)
-apply(drule mp)
-apply(auto)[1]
-by (metis add_eq_if diff_add_inverse oddfactor(3) mod_eq_0_iff mult_div_cancel nat_mult_commute ww)
-
-
-lemma m2: "0 < n ==> 2 ^ Discrete.log (n div (oddfactor n)) * (oddfactor n) = n"
-apply(subst m)
-apply(simp)
-apply(subst m1)
-apply(simp)
-done
-
-lemma y1:
- "pdecode2 (pencode m n) = n"
-apply(simp del: One_nat_def)
-apply(subst k)
-apply(auto)
-done
-
-lemma y2:
- "pdecode1 (pencode m n) = m"
-apply(simp only: pdecode1.simps pencode.simps)
-apply(subst Suc_diff_1)
-apply(auto)[1]
-apply(subst Suc_diff_1)
-apply(auto)[1]
-apply(subst k)
-apply(auto)[1]
-by (metis Suc_eq_plus1 Suc_neq_Zero comm_semiring_1_class.normalizing_semiring_rules(7) div_mult_self1_is_id log_exp)
-
-lemma yy:
- "pencode (pdecode1 m) (pdecode2 m) = m"
-apply(induct m rule: nat_less_induct)
-apply(simp (no_asm))
-apply(case_tac "n = 0")
-apply(simp)
-apply(subst dvd_mult_div_cancel)
-using oddfactor_odd
-apply -
-apply(drule_tac x="Suc n" in meta_spec)
-apply(erule disjE)
-apply(auto)[1]
-apply (metis One_nat_def even_num_iff nat_even_iff_2_dvd odd_pos)
-using bigger
-apply -
-apply(rotate_tac 3)
-apply(drule_tac x="n" in meta_spec)
-apply(simp del: pencode.simps pdecode2.simps pdecode1.simps One_nat_def add: One_nat_def[symmetric])
-apply(subst m2)
-apply(simp)
-apply(simp)
-done
-
-fun penc where
- "penc (m, n) = pencode m n"
-
-fun pdec where
- "pdec m = (pdecode1 m, pdecode2 m)"
-
-lemma q1: "penc (pdec m) = m"
-apply(simp only: penc.simps pdec.simps)
-apply(rule yy)
-done
-
-lemma q2: "pdec (penc m) = m"
-apply(simp only: penc.simps pdec.simps)
-apply(case_tac m)
-apply(simp only: penc.simps pdec.simps)
-apply(subst y1)
-apply(subst y2)
-apply(simp)
-done
-
-lemma inj_penc: "inj_on penc A"
-apply(rule inj_on_inverseI)
-apply(rule q2)
-done
-
-lemma inj_pdec: "inj_on pdec A"
-apply(rule inj_on_inverseI)
-apply(rule q1)
-done
-
-lemma surj_penc: "surj penc"
-apply(rule surjI)
-apply(rule q1)
-done
-
-lemma surj_pdec: "surj pdec"
-apply(rule surjI)
-apply(rule q2)
-done
-
-lemma
- "bij pdec"
-by(simp add: bij_def surj_pdec inj_pdec)
-
-lemma
- "bij penc"
-by(simp add: bij_def surj_penc inj_penc)
-
-lemma "a \<le> penc (a, 0)"
-apply(induct a)
-apply(simp)
-apply(simp)
-by (smt nat_one_le_power)
-
-lemma "penc(a, 0) \<le> penc (a, b)"
-apply(simp)
-by (metis diff_le_mono le_add1 mult_2_right mult_le_mono1 nat_add_commute nat_mult_1 nat_mult_commute)
-
-lemma "b \<le> penc (a, b)"
-apply(simp)
-proof -
- have f1: "(1\<Colon>nat) + 1 = 2"
- by (metis mult_2 nat_mult_1_right)
- have f2: "\<And>x\<^isub>1 x\<^isub>2. (x\<^isub>1\<Colon>nat) \<le> x\<^isub>1 * x\<^isub>2 \<or> \<not> 1 \<le> x\<^isub>2"
- by (metis mult_le_mono2 nat_mult_1_right)
- have "1 + (b + b) \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1"
- by (metis le_add1 le_trans nat_add_left_cancel_le)
- hence "(1 + (b + b)) * (1 + 1) ^ a \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1"
- using f2 by (metis le_add1 le_trans one_le_power)
- hence "b \<le> 2 ^ a * (b + b + 1) - 1"
- using f1 by (metis le_diff_conv nat_add_commute nat_le_linear nat_mult_commute)
- thus "b \<le> 2 ^ a * (2 * b + 1) - 1"
- by (metis mult_2)
-qed
-
-
-end
\ No newline at end of file
--- a/thys/Recursive.thy Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Recursive.thy Fri Dec 21 15:30:24 2018 +0100
@@ -170,33 +170,26 @@
declare addition_inv.simps[simp del]
+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 addition_inv_init:
"\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>
addition_inv (0, lm) m n p lm"
-apply(simp add: addition_inv.simps Let_def)
+apply(simp add: addition_inv.simps Let_def )
apply(rule_tac x = "lm ! m" in exI, simp)
done
-lemma abs_fetch_0[simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_1[simp]: "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_2[simp]: "abc_fetch 2 (addition m n p) = Some (Inc p)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_3[simp]: "abc_fetch 3 (addition m n p) = Some (Goto 0)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_4[simp]: "abc_fetch 4 (addition m n p) = Some (Dec p 7)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_5[simp]: "abc_fetch 5 (addition m n p) = Some (Inc m)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_6[simp]: "abc_fetch 6 (addition m n p) = Some (Goto 4)"
-by(simp add: abc_fetch.simps addition.simps)
+lemma abs_fetch[simp]:
+ "abc_fetch 0 (addition m n p) = Some (Dec m 4)"
+ "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)"
+ "abc_fetch 2 (addition m n p) = Some (Inc p)"
+ "abc_fetch 3 (addition m n p) = Some (Goto 0)"
+ "abc_fetch 4 (addition m n p) = Some (Dec p 7)"
+ "abc_fetch 5 (addition m n p) = Some (Inc m)"
+ "abc_fetch 6 (addition m n p) = Some (Goto 4)"
+by(simp_all add: abc_fetch.simps addition.simps)
lemma exists_small_list_elem1[simp]:
"\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x \<le> lm ! m; 0 < x\<rbrakk>
@@ -288,7 +281,7 @@
abc_step_l.simps addition_inv.simps
abc_lm_v.simps abc_lm_s.simps nth_append
split: if_splits)
-apply(rule_tac [!] x = x in exI, simp_all add: list_update_overwrite Suc_diff_Suc)
+apply(rule_tac [!] x = x in exI, simp_all add: list_update_overwrite Suc_diff_Suc )
by (metis list_update_overwrite list_update_swap nat_neq_iff)
lemma addition_correct':
@@ -479,21 +472,12 @@
rule_tac x = "initlm ! n" in exI, simp)
done
-lemma abc_fetch_0[simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)"
-apply(simp add: mv_box.simps abc_fetch.simps)
-done
-
-lemma abc_fetch_1[simp]: "abc_fetch (Suc 0) (mv_box m n) =
- Some (Inc n)"
-apply(simp add: mv_box.simps abc_fetch.simps)
-done
-
-lemma abc_fetch_2[simp]: "abc_fetch 2 (mv_box m n) = Some (Goto 0)"
-apply(simp add: mv_box.simps abc_fetch.simps)
-done
-
-lemma abc_fetch_3[simp]: "abc_fetch 3 (mv_box m n) = None"
-apply(simp add: mv_box.simps abc_fetch.simps)
+lemma abc_fetch[simp]:
+ "abc_fetch 0 (mv_box m n) = Some (Dec m 3)"
+ "abc_fetch (Suc 0) (mv_box m n) = Some (Inc n)"
+ "abc_fetch 2 (mv_box m n) = Some (Goto 0)"
+ "abc_fetch 3 (mv_box m n) = None"
+apply(simp_all add: mv_box.simps abc_fetch.simps)
done
lemma replicate_Suc_iff_anywhere: "x # x\<up>b @ ys = x\<up>(Suc b) @ ys"
@@ -2584,7 +2568,7 @@
apply(arith)
apply(case_tac "Suc k = length ap", simp)
apply(rule_tac start_of_less, simp)
-apply(auto simp: tinc_b_def shift.simps start_of_suc_inc length_of.simps startof_not0)
+apply(auto simp: tinc_b_def shift.simps start_of_suc_inc length_of.simps )
done
lemma findnth_le[elim]:
@@ -2607,7 +2591,7 @@
apply(rule_tac start_of_less, simp)
apply(subgoal_tac "b \<le> start_of (layout_of ap) k + 2*n + 1 \<and>
start_of (layout_of ap) k + 2*n + 1 \<le> start_of (layout_of ap) (Suc k)", auto)
-apply(auto simp: tinc_b_def shift.simps length_of.simps startof_not0 start_of_suc_inc)
+apply(auto simp: tinc_b_def shift.simps length_of.simps start_of_suc_inc)
done
lemma start_of_eq: "length ap < as \<Longrightarrow> start_of (layout_of ap) as = start_of (layout_of ap) (length ap)"
@@ -2646,7 +2630,7 @@
prefer 2
apply(subgoal_tac "start_of (layout_of ap) (Suc k) = start_of (layout_of ap) k + 2*n + 16
\<and> start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap)")
-apply(simp add: startof_not0, rule_tac conjI)
+apply(simp, rule_tac conjI)
apply(simp add: start_of_suc_dec)
apply(rule_tac start_of_all_le)
apply(auto simp: tdec_b_def shift.simps)
@@ -2795,6 +2779,4 @@
by simp
qed
-unused_thms
-
end
\ No newline at end of file
--- a/thys/Uncomputable.thy Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Uncomputable.thy Fri Dec 21 15:30:24 2018 +0100
@@ -77,7 +77,7 @@
if s = 4 then inv_begin4 n tp
else False)"
-lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow>
+lemma inv_begin_step_E: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow>
\<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
by (rule_tac x = "Suc i" in exI, simp)
@@ -88,7 +88,7 @@
using assms
unfolding tcopy_begin_def
apply(cases cf)
-apply(auto simp: numeral split: if_splits)
+apply(auto simp: numeral split: if_splits elim:inv_begin_step_E)
apply(case_tac "hd c")
apply(auto)
apply(case_tac c)
@@ -239,75 +239,52 @@
inv_loop4.simps[simp del] inv_loop5.simps[simp del]
inv_loop6.simps[simp del]
-lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
+lemma Bk_no_Oc_repeatE[elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
by (case_tac t, auto)
-lemma [simp]: "inv_loop1 x (b, []) = False"
-by (simp add: inv_loop1.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
+lemma inv_loop3_Bk_empty_via_2[elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
by (auto simp: inv_loop2.simps inv_loop3.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
+lemma inv_loop3_Bk_empty[elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
by (auto simp: inv_loop3.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
+lemma inv_loop5_Oc_empty_via_4[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
apply(auto simp: inv_loop4.simps inv_loop5.simps)
apply(rule_tac [!] x = i in exI,
rule_tac [!] x = "Suc j" in exI, simp_all)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"
-by (auto simp: inv_loop4.simps inv_loop5.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
-by (auto simp: inv_loop4.simps inv_loop5.simps)
-
-lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"
-by (auto simp: inv_loop6.simps)
-
-lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR"
-by (auto simp: inv_loop6.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
+lemma inv_loop1_Bk[elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
by (auto simp: inv_loop1.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
-by (auto simp: inv_loop1.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
+lemma inv_loop3_Bk_via_2[elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
apply(auto simp: inv_loop2.simps inv_loop3.simps)
apply(rule_tac [!] x = i in exI, rule_tac [!] x = j in exI, simp_all)
done
-lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"
-by (case_tac j, simp_all)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
+lemma inv_loop3_Bk_move[elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
apply(auto simp: inv_loop3.simps)
apply(rule_tac [!] x = i in exI,
rule_tac [!] x = j in exI, simp_all)
apply(case_tac [!] t, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
+lemma inv_loop5_Oc_via_4_Bk[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
by (auto simp: inv_loop4.simps inv_loop5.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
+lemma inv_loop6_Bk_via_5[elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
by (auto simp: inv_loop6.simps inv_loop5.simps)
-lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"
+lemma inv_loop5_loop_no_Bk[simp]: "inv_loop5_loop x (b, Bk # list) = False"
by (auto simp: inv_loop5.simps)
-lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
+lemma inv_loop6_exit_no_Bk[simp]: "inv_loop6_exit x (b, Bk # list) = False"
by (auto simp: inv_loop6.simps)
declare inv_loop5_loop.simps[simp del] inv_loop5_exit.simps[simp del]
inv_loop6_loop.simps[simp del] inv_loop6_exit.simps[simp del]
-lemma [elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
+lemma inv_loop6_loopBk_via_5[elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
\<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )
apply(erule_tac exE)+
@@ -319,10 +296,10 @@
apply(case_tac [!] nat, simp_all)
done
-lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
+lemma inv_loop6_loop_no_Oc_Bk[simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
by (auto simp: inv_loop6_loop.simps)
-lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
+lemma inv_loop6_exit_Oc_Bk_via_5[elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
inv_loop6_exit x (tl b, Oc # Bk # list)"
apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)
apply(erule_tac exE)+
@@ -331,24 +308,12 @@
apply(case_tac [!] nat, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
+lemma inv_loop6_Bk_tail_via_5[elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
apply(simp add: inv_loop5.simps inv_loop6.simps)
apply(case_tac "hd b", simp_all, auto)
done
-lemma [simp]: "inv_loop6 x ([], Bk # xs) = False"
-apply(simp add: inv_loop6.simps inv_loop6_loop.simps
- inv_loop6_exit.simps)
-apply(auto)
-done
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
-by (simp)
-
-lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
-by (simp add: inv_loop6_exit.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
+lemma inv_loop6_loop_Bk_Bk_drop[elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
\<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
apply(simp only: inv_loop6_loop.simps)
apply(erule_tac exE)+
@@ -357,7 +322,7 @@
apply(case_tac [!] k, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk>
+lemma inv_loop6_exit_Oc_Bk_via_loop6[elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk>
\<Longrightarrow> inv_loop6_exit x (tl b, Oc # Bk # list)"
apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)
apply(erule_tac exE)+
@@ -365,20 +330,20 @@
apply(case_tac [!] k, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
+lemma inv_loop6_Bk_tail[elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
apply(simp add: inv_loop6.simps)
apply(case_tac "hd b", simp_all, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"
+lemma inv_loop2_Oc_via_1[elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"
apply(auto simp: inv_loop1.simps inv_loop2.simps)
apply(rule_tac x = "Suc i" in exI, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
+lemma inv_loop2_Bk_via_Oc[elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
by (auto simp: inv_loop2.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
+lemma inv_loop4_Oc_via_3[elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
apply(auto simp: inv_loop3.simps inv_loop4.simps)
apply(rule_tac [!] x = i in exI, auto)
apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)
@@ -386,20 +351,17 @@
apply(case_tac [!] j, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
+lemma inv_loop4_Oc_move[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
apply(auto simp: inv_loop4.simps)
apply(rule_tac [!] x = "i" in exI, auto)
apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)
apply(case_tac [!] t, simp_all)
done
-lemma [simp]: "inv_loop5 x ([], list) = False"
-by (auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
-
-lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"
+lemma inv_loop5_exit_no_Oc[simp]: "inv_loop5_exit x (b, Oc # list) = False"
by (auto simp: inv_loop5_exit.simps)
-lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
+lemma inv_loop5_exit_Bk_Oc_via_loop[elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
\<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"
apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)
apply(erule_tac exE)+
@@ -407,7 +369,7 @@
apply(case_tac [!] k, auto)
done
-lemma [elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk>
+lemma inv_loop5_loop_Oc_Oc_drop[elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk>
\<Longrightarrow> inv_loop5_loop x (tl b, Oc # Oc # list)"
apply(simp only: inv_loop5_loop.simps)
apply(erule_tac exE)+
@@ -416,21 +378,43 @@
apply(case_tac [!] k, auto)
done
-lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop5 x (tl b, hd b # Oc # list)"
+lemma inv_loop5_Oc_tl[elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop5 x (tl b, hd b # Oc # list)"
apply(simp add: inv_loop5.simps)
apply(case_tac "hd b", simp_all, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_loop1 x ([], Bk # Oc # list)"
+lemma inv_loop1_Bk_Oc_via_6[elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_loop1 x ([], Bk # Oc # list)"
+apply(auto simp: inv_loop6.simps inv_loop1.simps
+ inv_loop6_loop.simps inv_loop6_exit.simps)
+done
+
+lemma inv_loop1_Oc_via_6[elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk>
+ \<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"
apply(auto simp: inv_loop6.simps inv_loop1.simps
inv_loop6_loop.simps inv_loop6_exit.simps)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk>
- \<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"
-apply(auto simp: inv_loop6.simps inv_loop1.simps
- inv_loop6_loop.simps inv_loop6_exit.simps)
-done
+
+lemma inv_loop_nonempty[simp]:
+ "inv_loop1 x (b, []) = False"
+ "inv_loop2 x ([], b) = False"
+ "inv_loop2 x (l', []) = False"
+ "inv_loop3 x (b, []) = False"
+ "inv_loop4 x ([], b) = False"
+ "inv_loop5 x ([], list) = False"
+ "inv_loop6 x ([], Bk # xs) = False"
+ by (auto simp: inv_loop1.simps inv_loop2.simps inv_loop3.simps inv_loop4.simps
+ inv_loop5.simps inv_loop6.simps inv_loop5_exit.simps inv_loop5_loop.simps
+ inv_loop6_loop.simps)
+
+lemma inv_loop_nonemptyE[elim]:
+ "\<lbrakk>inv_loop5 x (b, [])\<rbrakk> \<Longrightarrow> RR" "inv_loop6 x (b, []) \<Longrightarrow> RR"
+ "\<lbrakk>inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
+ by (auto simp: inv_loop4.simps inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps
+ inv_loop6.simps inv_loop6_exit.simps inv_loop6_loop.simps inv_loop1.simps)
+
+lemma inv_loop6_Bk_Bk_drop[elim]: "\<lbrakk>inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
+ by (simp)
lemma inv_loop_step:
"\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
@@ -476,39 +460,19 @@
using wf_measure_loop
by (metis wf_iff_no_infinite_down_chain)
-
-
-lemma [simp]: "inv_loop2 x ([], b) = False"
-by (auto simp: inv_loop2.simps)
-
-lemma [simp]: "inv_loop2 x (l', []) = False"
-by (auto simp: inv_loop2.simps)
-
-lemma [simp]: "inv_loop3 x (b, []) = False"
-by (auto simp: inv_loop3.simps)
-
-lemma [simp]: "inv_loop4 x ([], b) = False"
-by (auto simp: inv_loop4.simps)
-
-
-lemma [elim]:
- "\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;
+lemma inv_loop4_not_just_Oc[elim]:
+ "\<lbrakk>inv_loop4 x (l', []);
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l'))\<rbrakk>
- \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) < length (takeWhile (\<lambda>a. a = Oc) (rev l'))"
+ \<Longrightarrow> RR"
+ "\<lbrakk>inv_loop4 x (l', Bk # list);
+ length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq>
+ length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
+ \<Longrightarrow> RR"
apply(auto simp: inv_loop4.simps)
apply(case_tac [!] j, simp_all add: List.takeWhile_tail)
done
-
-lemma [elim]:
- "\<lbrakk>inv_loop4 x (l', Bk # list); l' \<noteq> []; 0 < x;
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq>
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
- \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) <
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
-by (auto simp: inv_loop4.simps)
-
lemma takeWhile_replicate_append:
"P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"
by (induct x, auto)
@@ -517,12 +481,11 @@
"P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"
by (induct x, auto)
-lemma [elim]:
- "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;
+lemma inv_loop5_Bk_E[elim]:
+ "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> [];
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
- \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) <
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
+ \<Longrightarrow> RR"
apply(auto simp: inv_loop5.simps inv_loop5_exit.simps)
apply(case_tac [!] j, simp_all)
apply(case_tac [!] "nat", simp_all)
@@ -531,21 +494,20 @@
apply(case_tac nata, simp_all add: List.takeWhile_tail)
done
-lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
+lemma inv_loop1_hd_Oc[elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
by (auto simp: inv_loop1.simps)
-lemma [elim]:
- "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;
+lemma inv_loop6_not_just_Bk[elim]:
+ "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> [];
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
- \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) <
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
+ \<Longrightarrow> RR"
apply(auto simp: inv_loop6.simps)
apply(case_tac l', simp_all)
done
-lemma [elim]:
- "\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []; 0 < x\<rbrakk> \<Longrightarrow>
+lemma inv_loop2_OcE[elim]:
+ "\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []\<rbrakk> \<Longrightarrow>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list)) <
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
apply(auto simp: inv_loop2.simps)
@@ -553,22 +515,20 @@
takeWhile_replicate)
done
-lemma [elim]:
- "\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> []; 0 < x;
+lemma inv_loop5_OcE[elim]:
+ "\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> [];
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
- \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) <
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
+ \<Longrightarrow> RR"
apply(auto simp: inv_loop5.simps)
apply(case_tac l', auto)
done
-lemma[elim]:
- "\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> []; 0 < x;
+lemma inv_loop6_OcE[elim]:
+ "\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> [];
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list))
\<noteq> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
- \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) <
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
+ \<Longrightarrow> RR"
apply(case_tac l')
apply(auto simp: inv_loop6.simps)
done
@@ -668,29 +628,21 @@
inv_end3.simps[simp del] inv_end4.simps[simp del]
inv_end5.simps[simp del]
-lemma [simp]: "inv_end1 x (b, []) = False"
-by (auto simp: inv_end1.simps)
-
-lemma [simp]: "inv_end2 x (b, []) = False"
-by (auto simp: inv_end2.simps)
-
-lemma [simp]: "inv_end3 x (b, []) = False"
-by (auto simp: inv_end3.simps)
+lemma inv_end_nonempty[simp]:
+ "inv_end1 x (b, []) = False"
+ "inv_end1 x ([], list) = False"
+ "inv_end2 x (b, []) = False"
+ "inv_end3 x (b, []) = False"
+ "inv_end4 x (b, []) = False"
+ "inv_end5 x (b, []) = False"
+ "inv_end5 x ([], Oc # list) = False"
+by (auto simp: inv_end1.simps inv_end2.simps inv_end3.simps inv_end4.simps inv_end5.simps)
-lemma [simp]: "inv_end4 x (b, []) = False"
-by (auto simp: inv_end4.simps)
-
-lemma [simp]: "inv_end5 x (b, []) = False"
-by (auto simp: inv_end5.simps)
-
-lemma [simp]: "inv_end1 x ([], list) = False"
-by (auto simp: inv_end1.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
+lemma inv_end0_Bk_via_1[elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
\<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
by (auto simp: inv_end1.simps inv_end0.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk>
+lemma inv_end3_Oc_via_2[elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk>
\<Longrightarrow> inv_end3 x (b, Oc # list)"
apply(auto simp: inv_end2.simps inv_end3.simps)
apply(rule_tac x = "j - 1" in exI)
@@ -698,65 +650,65 @@
apply(case_tac x, simp_all)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
+lemma inv_end2_Bk_via_3[elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
by (auto simp: inv_end2.simps inv_end3.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow>
+lemma inv_end5_Bk_via_4[elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow>
inv_end5 x ([], Bk # Bk # list)"
by (auto simp: inv_end4.simps inv_end5.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
+lemma inv_end5_Bk_tail_via_4[elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
inv_end5 x (tl b, hd b # Bk # list)"
apply(auto simp: inv_end4.simps inv_end5.simps)
apply(rule_tac x = 1 in exI, simp)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"
+lemma inv_end0_Bk_via_5[elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"
apply(auto simp: inv_end5.simps inv_end0.simps)
apply(case_tac [!] j, simp_all)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
+lemma inv_end2_Oc_via_1[elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
by (auto simp: inv_end1.simps inv_end2.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
+lemma inv_end4_Bk_Oc_via_2[elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
inv_end4 x ([], Bk # Oc # list)"
by (auto simp: inv_end2.simps inv_end4.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
+lemma inv_end4_Oc_via_2[elim]: "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
inv_end4 x (tl b, hd b # Oc # list)"
apply(auto simp: inv_end2.simps inv_end4.simps)
apply(case_tac [!] j, simp_all)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
+lemma inv_end2_Oc_via_3[elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
by (auto simp: inv_end2.simps inv_end3.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
+lemma inv_end4_Bk_via_Oc[elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
by (auto simp: inv_end2.simps inv_end4.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
+lemma inv_end5_Bk_drop_Oc[elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
by (auto simp: inv_end2.simps inv_end5.simps)
declare inv_end5_loop.simps[simp del]
inv_end5_exit.simps[simp del]
-lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"
+lemma inv_end5_exit_no_Oc[simp]: "inv_end5_exit x (b, Oc # list) = False"
by (auto simp: inv_end5_exit.simps)
-lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
+lemma inv_end5_loop_no_Bk_Oc[simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
apply(auto simp: inv_end5_loop.simps)
apply(case_tac [!] j, simp_all)
done
-lemma [elim]:
+lemma inv_end5_exit_Bk_Oc_via_loop[elim]:
"\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk> \<Longrightarrow>
inv_end5_exit x (tl b, Bk # Oc # list)"
apply(auto simp: inv_end5_loop.simps inv_end5_exit.simps)
apply(case_tac [!] i, simp_all)
done
-lemma [elim]:
+lemma inv_end5_loop_Oc_Oc_drop[elim]:
"\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
inv_end5_loop x (tl b, Oc # Oc # list)"
apply(simp only: inv_end5_loop.simps inv_end5_exit.simps)
@@ -766,7 +718,7 @@
apply(case_tac [!] i, simp_all)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
+lemma inv_end5_Oc_tail[elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
inv_end5 x (tl b, hd b # Oc # list)"
apply(simp add: inv_end2.simps inv_end5.simps)
apply(case_tac "hd b", simp_all, auto)
@@ -816,9 +768,6 @@
unfolding end_LE_def
by (auto)
-lemma [simp]: "inv_end5 x ([], Oc # list) = False"
-by (auto simp: inv_end5.simps inv_end5_loop.simps)
-
lemma halt_lemma:
"\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
by (metis wf_iff_no_infinite_down_chain)
@@ -878,14 +827,11 @@
(* tcopy *)
-lemma [intro]: "tm_wf (tcopy_begin, 0)"
-by (auto simp: tm_wf.simps tcopy_begin_def)
-
-lemma [intro]: "tm_wf (tcopy_loop, 0)"
-by (auto simp: tm_wf.simps tcopy_loop_def)
-
-lemma [intro]: "tm_wf (tcopy_end, 0)"
-by (auto simp: tm_wf.simps tcopy_end_def)
+lemma tm_wf_tcopy[intro]:
+ "tm_wf (tcopy_begin, 0)"
+ "tm_wf (tcopy_loop, 0)"
+ "tm_wf (tcopy_end, 0)"
+by (auto simp: tm_wf.simps tcopy_end_def tcopy_loop_def tcopy_begin_def)
lemma tcopy_correct1:
assumes "0 < x"
@@ -999,10 +945,10 @@
where
"halts p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k, <n::nat> @ Bk \<up> l)))}"
-lemma [intro, simp]: "tm_wf0 tcopy"
+lemma tm_wf0_tcopy[intro, simp]: "tm_wf0 tcopy"
by (auto simp: tcopy_def)
-lemma [intro, simp]: "tm_wf0 dither"
+lemma tm_wf0_dither[intro, simp]: "tm_wf0 dither"
by (auto simp: tm_wf.simps dither_def)
text {*