section ‹List representation›
theory List_Representation
imports Main
begin
lemma rev_take_Suc: assumes j: "j < length xs"
shows "rev (take (Suc j) xs) = xs ! j # rev (take j xs)"
proof -
from j have xs: "xs = take j xs @ xs ! j # drop (Suc j) xs" by (rule id_take_nth_drop)
show ?thesis unfolding arg_cong[OF xs, of "λ xs. rev (take (Suc j) xs)"]
by (simp add: min_def)
qed
type_synonym 'a list_repr = "'a list × 'a list"
definition list_repr :: "nat ⇒ 'a list_repr ⇒ 'a list ⇒ bool" where
"list_repr i ba xs = (i ≤ length xs ∧ fst ba = rev (take i xs) ∧ snd ba = drop i xs)"
definition of_list_repr :: "'a list_repr ⇒ 'a list" where
"of_list_repr ba = (rev (fst ba) @ snd ba)"
lemma of_list_repr: "list_repr i ba xs ⟹ of_list_repr ba = xs"
unfolding of_list_repr_def list_repr_def by auto
definition get_nth_i :: "'a list_repr ⇒ 'a" where
"get_nth_i ba = hd (snd ba)"
definition get_nth_im1 :: "'a list_repr ⇒ 'a" where
"get_nth_im1 ba = hd (fst ba)"
lemma get_nth_i: "list_repr i ba xs ⟹ i < length xs ⟹ get_nth_i ba = xs ! i"
unfolding list_repr_def get_nth_i_def
by (auto simp: hd_drop_conv_nth)
lemma get_nth_im1: "list_repr i ba xs ⟹ i ≠ 0 ⟹ get_nth_im1 ba = xs ! (i - 1)"
unfolding list_repr_def get_nth_im1_def
by (cases i, auto simp: rev_take_Suc)
definition update_i :: "'a list_repr ⇒ 'a ⇒ 'a list_repr" where
"update_i ba x = (fst ba, x # tl (snd ba))"
lemma Cons_tl_drop_update: "i < length xs ⟹ x # tl (drop i xs) = drop i (xs[i := x])"
proof (induct i arbitrary: xs)
case (0 xs)
thus ?case by (cases xs, auto)
next
case (Suc i xs)
thus ?case by (cases xs, auto)
qed
lemma update_i: "list_repr i ba xs ⟹ i < length xs ⟹ list_repr i (update_i ba x) (xs [i := x])"
unfolding update_i_def list_repr_def
by (auto simp: Cons_tl_drop_update)
definition update_im1 :: "'a list_repr ⇒ 'a ⇒ 'a list_repr" where
"update_im1 ba x = (x # tl (fst ba), snd ba)"
lemma update_im1: "list_repr i ba xs ⟹ i ≠ 0 ⟹ list_repr i (update_im1 ba x) (xs [i - 1 := x])"
unfolding update_im1_def list_repr_def
by (cases i, auto simp: rev_take_Suc)
lemma tl_drop_Suc: "tl (drop i xs) = drop (Suc i) xs"
proof (induct i arbitrary: xs)
case (0 xs) thus ?case by (cases xs, auto)
next
case (Suc i xs) thus ?case by (cases xs, auto)
qed
definition inc_i :: "'a list_repr ⇒ 'a list_repr" where
"inc_i ba = (case ba of (b,a) ⇒ (hd a # b, tl a))"
lemma inc_i: "list_repr i ba xs ⟹ i < length xs ⟹ list_repr (Suc i) (inc_i ba) xs"
unfolding list_repr_def inc_i_def by (cases ba, auto simp: rev_take_Suc hd_drop_conv_nth tl_drop_Suc)
definition dec_i :: "'a list_repr ⇒ 'a list_repr" where
"dec_i ba = (case ba of (b,a) ⇒ (tl b, hd b # a))"
lemma dec_i: "list_repr i ba xs ⟹ i ≠ 0 ⟹ list_repr (i - 1) (dec_i ba) xs"
unfolding list_repr_def dec_i_def
by (cases ba; cases i, auto simp: rev_take_Suc hd_drop_conv_nth Cons_nth_drop_Suc)
lemma dec_i_Suc: "list_repr (Suc i) ba xs ⟹ list_repr i (dec_i ba) xs"
using dec_i[of "Suc i" ba xs] by auto
end