Theory Lists_Thms

(*
  File: Lists_Thms.thy
  Author: Bohua Zhan

  Setup for proof steps related to lists.
*)

section ‹Setup for lists›

theory Lists_Thms
  imports Set_Thms
begin

subsection ‹Definition of lists›

setup ‹add_resolve_prfstep @{thm list.distinct(2)}›
setup ‹add_forward_prfstep (equiv_forward_th @{thm list.simps(1)})›
setup ‹fold add_rewrite_rule @{thms List.list.sel}›
setup ‹add_rewrite_rule @{thm list.collapse}›
setup ‹add_var_induct_rule @{thm list.induct}›

subsection ‹Length›

setup ‹add_rewrite_rule @{thm List.list.size(3)}›
lemma length_one [rewrite]: "length [x] = 1" by simp
lemma length_Cons [rewrite]: "length (a # b) = length b + 1" by simp
lemma length_snoc [rewrite]: "length (xs @ [x]) = length xs + 1" by auto
lemma length_zero_is_nil [forward]: "length xs = 0 ⟹ xs = []" by simp
lemma length_gt_zero [forward]: "length xs > 0 ⟹ xs ≠ []" by simp

subsection ‹Append›

setup ‹add_rewrite_rule @{thm List.length_append}›
setup ‹add_rewrite_rule_cond @{thm List.append.simps(2)} [with_cond "?xs ≠ []"]›
setup ‹add_rewrite_rule @{thm List.hd_append2}›
lemma append_is_empty [forward]: "xs @ ys = [] ⟹ xs = [] ∧ ys = []" by simp

lemma cons_to_append [rewrite_back]: "a # b = [a] @ b" by simp

ML_file ‹list_ac.ML›
ML_file ‹list_ac_test.ML›

subsection ‹Showing two lists are equal›

setup ‹add_backward2_prfstep_cond @{thm nth_equalityI} [with_filt (order_filter "xs" "ys")]›

subsection ‹Set of elements of a list›

setup ‹add_rewrite_rule @{thm List.set_simps(1)}›
lemma set_one [rewrite]: "set [u] = {u}" by simp
lemma set_two [rewrite]: "set [u, v] = {u, v}" by simp
lemma set_simps2: "set (x # xs) = {x} ∪ set xs" by simp
setup ‹add_rewrite_rule_cond @{thm set_simps2} [with_cond "?xs ≠ []", with_cond "?xs ≠ [?y]"]›
setup ‹add_rewrite_rule @{thm List.set_append}›
setup ‹add_rewrite_rule @{thm List.set_rev}›
setup ‹add_resolve_prfstep @{thm List.finite_set}›
setup ‹add_backward_prfstep (equiv_forward_th @{thm in_set_conv_nth})›

subsection ‹hd›

setup ‹register_wellform_data ("hd xs", ["xs ≠ []"])›
setup ‹add_forward_prfstep_cond @{thm List.hd_in_set} [with_term "hd ?xs"]›

subsection ‹tl›

setup ‹add_rewrite_rule @{thm length_tl}›
lemma nth_tl' [rewrite]: "i < length (tl xs) ⟹ tl xs ! i = xs ! (i + 1)"
  by (simp add: nth_tl)
lemma set_tl_subset [forward_arg1]: "set (tl xs) ⊆ set xs"
  by (metis list.set_sel(2) subsetI tl_Nil)

subsection ‹nth›

setup ‹register_wellform_data ("xs ! i", ["i < length xs"])›
setup ‹add_prfstep_check_req ("xs ! i", "i < length xs")›
setup ‹add_rewrite_rule_back @{thm hd_conv_nth}›
setup ‹add_rewrite_rule @{thm List.nth_Cons'}›
setup ‹add_rewrite_rule @{thm List.nth_append}›
setup ‹add_forward_prfstep_cond @{thm nth_mem} [with_term "?xs ! ?n"]›

subsection ‹sorted› (*TEMPORARY VERSION BY BOHUA pending a treatment of sorted_wrt*)

definition sorted :: "'a::linorder list ⇒ bool" where
 "sorted = List.sorted"
declare sorted_def[simp]

lemma sorted_Nil [resolve]: "sorted []" by simp
lemma sorted_single [resolve]: "sorted [x]" by simp

lemma sorted_simps2: "sorted (x # ys) = (Ball (set ys) ((≤) x) ∧ sorted ys)" by simp
setup ‹add_backward_prfstep (equiv_backward_th @{thm sorted_simps2})›

lemma sorted_ConsD1 [forward]: "sorted (x # xs) ⟹ sorted xs"
 using sorted_simps(2) by simp
lemma sorted_ConsD2 [forward, backward2]: "sorted (x # xs) ⟹ y ∈ set xs ⟹ x ≤ y"
 using sorted_simps(2) by auto

lemma sorted_appendI [backward]:
 "sorted xs ∧ sorted ys ∧ (∀x∈set xs. ∀y∈set ys. x ≤ y) ⟹ sorted (xs @ ys)"
 by (simp add: sorted_append)

lemma sorted_appendE [forward]: "sorted (xs @ ys) ⟹ sorted xs ∧ sorted ys"
 by (simp add: sorted_append)

lemma sorted_appendE2 [forward]:
 "sorted (xs @ ys) ⟹ x ∈ set xs ⟹ ∀y∈set ys. x ≤ y"
 using sorted_append by (auto simp add: sorted_append)

lemma sorted_nth_mono' [backward]:
 "sorted xs ⟹ j < length xs ⟹ i ≤ j ⟹ xs ! i ≤ xs ! j"
 using sorted_nth_mono by auto

lemma sorted_nth_mono_less [forward]:
 "sorted xs ⟹ i < length xs ⟹ xs ! i < xs ! j ⟹ i < j"
 by (meson leD not_le_imp_less sorted_nth_mono')

subsection ‹sort›

lemma sorted_sort: "sorted (sort xs)" by simp
setup ‹add_forward_prfstep_cond @{thm sorted_sort} [with_term "sort ?xs"]›
setup ‹add_rewrite_rule @{thm length_sort}›
setup ‹add_rewrite_rule @{thm mset_sort}›
setup ‹add_rewrite_rule @{thm set_sort}›

lemma properties_for_sort:
 "mset ys = mset xs ⟹ sorted ys ⟹ sort xs = ys" using properties_for_sort by simp
setup ‹add_backward_prfstep @{thm properties_for_sort}›
lemma sort_Nil [rewrite]: "sort [] = []" by auto
lemma sort_singleton [rewrite]: "sort [a] = [a]" by auto

subsection ‹distinct›

lemma distinct_Nil [resolve]: "distinct []" by simp
setup ‹add_resolve_prfstep @{thm List.distinct_singleton}›
setup ‹add_rewrite_rule_cond @{thm distinct.simps(2)} [with_cond "?xs ≠ []"]›
setup ‹add_rewrite_rule @{thm distinct_append}›
setup ‹add_rewrite_rule @{thm distinct_rev}›
setup ‹add_rewrite_rule @{thm distinct_sort}›
setup ‹add_resolve_prfstep (equiv_backward_th @{thm distinct_conv_nth})›

lemma distinct_nthE [forward]:
  "distinct xs ⟹ i < length xs ⟹ j < length xs ⟹ xs ! i = xs ! j ⟹ i = j"
  using nth_eq_iff_index_eq by blast

subsection ‹map function›

setup ‹fold add_rewrite_rule @{thms List.list.map}›
setup ‹add_rewrite_rule @{thm List.length_map}›
setup ‹add_rewrite_rule @{thm List.nth_map}›
setup ‹add_rewrite_rule @{thm List.map_append}›

subsection ‹Replicate›

setup ‹add_rewrite_arg_rule @{thm length_replicate}›
setup ‹add_rewrite_rule @{thm List.nth_replicate}›

subsection ‹last›

setup ‹register_wellform_data ("last xs", ["xs ≠ []"])›
lemma last_eval1 [rewrite]: "last [x] = x" by simp
lemma last_eval2 [rewrite]: "last [u, v] = v" by simp
setup ‹add_rewrite_rule @{thm List.last_ConsR}›
setup ‹add_rewrite_rule @{thm List.last_appendR}›
setup ‹add_rewrite_rule @{thm List.last_snoc}›
setup ‹add_rewrite_rule_back @{thm last_conv_nth}›
setup ‹add_forward_prfstep_cond @{thm List.last_in_set} [with_term "last ?as"]›

subsection ‹butlast›

setup ‹add_rewrite_arg_rule @{thm List.length_butlast}›
setup ‹add_rewrite_rule @{thm List.nth_butlast}›
setup ‹add_rewrite_rule_back @{thm List.butlast_conv_take}›
setup ‹add_rewrite_rule @{thm List.butlast_snoc}›
lemma butlast_eval1 [rewrite]: "butlast [x] = []" by simp
lemma butlast_eval2 [rewrite]: "butlast [x, y] = [x]" by simp
lemma butlast_cons [rewrite]: "as ≠ [] ⟹ butlast (a # as) = a # butlast as" by simp
lemma butlast_append' [rewrite]: "bs ≠ [] ⟹ butlast (as @ bs) = as @ butlast bs"
  by (simp add: butlast_append)

setup ‹add_rewrite_rule @{thm List.append_butlast_last_id}›
lemma set_butlast_is_subset: "set (butlast xs) ⊆ set xs" by (simp add: in_set_butlastD subsetI)
setup ‹add_forward_arg1_prfstep @{thm set_butlast_is_subset}›

subsection ‹List update›

setup ‹register_wellform_data ("xs[i := x]", ["i < length xs"])›
setup ‹add_rewrite_arg_rule @{thm List.length_list_update}›
setup ‹add_rewrite_rule @{thm List.nth_list_update_eq}›
setup ‹add_rewrite_rule @{thm List.nth_list_update_neq}›
setup ‹add_rewrite_rule @{thm List.nth_list_update}›

subsection ‹take›

setup ‹register_wellform_data ("take n xs", ["n ≤ length xs"])›
setup ‹add_prfstep_check_req ("take n xs", "n ≤ length xs")›

lemma length_take [rewrite_arg]: "n ≤ length xs ⟹ length (take n xs) = n" by simp
lemma nth_take [rewrite]: "i < length (take n xs) ⟹ take n xs ! i = xs ! i" by simp

setup ‹add_rewrite_rule @{thm List.take_0}›
setup ‹add_rewrite_rule @{thm List.take_Suc_conv_app_nth}›
lemma take_length [rewrite]: "take (length xs) xs = xs" by simp

setup ‹add_forward_arg1_prfstep @{thm List.set_take_subset}›

lemma take_Suc [rewrite]: "Suc n ≤ length xs ⟹ take (Suc n) xs = take n xs @ [nth xs n]"
  using Suc_le_lessD take_Suc_conv_app_nth by blast

setup ‹add_rewrite_rule @{thm List.take_update_cancel}›
setup ‹add_rewrite_rule @{thm List.append_take_drop_id}›
setup ‹add_rewrite_rule @{thm List.take_all}›

subsection ‹drop›

setup ‹add_rewrite_arg_rule @{thm List.length_drop}›
lemma nth_drop [rewrite]:
  "i < length (drop n xs) ⟹ drop n xs ! i = xs ! (n + i)" by simp

setup ‹add_rewrite_rule @{thm List.drop_0}›
setup ‹add_rewrite_rule @{thm List.drop_all}›
setup ‹add_rewrite_rule_back @{thm List.take_drop}›
setup ‹add_rewrite_rule @{thm List.drop_drop}›

subsection ‹rev›

setup ‹add_rewrite_arg_rule @{thm List.length_rev}›
setup ‹fold add_rewrite_rule @{thms List.rev.simps}›
setup ‹add_rewrite_rule @{thm List.rev_append}›
setup ‹add_rewrite_rule @{thm List.rev_rev_ident}›

subsection ‹filter›

setup ‹fold add_rewrite_rule @{thms filter.simps}›
setup ‹add_rewrite_rule @{thm filter_append}›
setup ‹add_rewrite_rule_bidir @{thm rev_filter}›

subsection ‹concat›

setup ‹fold add_rewrite_rule @{thms concat.simps}›

subsection ‹mset›

setup ‹add_rewrite_rule @{thm mset.simps(1)}›
lemma mset_simps_2 [rewrite]: "mset (a # x) = mset x + {#a#}" by simp
setup ‹add_rewrite_rule @{thm mset_append}›

setup ‹add_rewrite_rule @{thm mset_eq_setD}›
setup ‹add_rewrite_rule_cond @{thm in_multiset_in_set} [with_term "set ?xs"]›
setup ‹add_rewrite_rule_back_cond @{thm in_multiset_in_set} [with_term "mset ?xs"]›
setup ‹add_backward_prfstep @{thm Multiset.nth_mem_mset}›

lemma in_mset_conv_nth [resolve]: "x ∈# mset xs ⟹ ∃i<length xs. x = xs ! i"
  by (metis in_multiset_in_set in_set_conv_nth)

lemma hd_in_mset: "xs ≠ [] ⟹ hd xs ∈# mset xs" by simp
setup ‹add_forward_prfstep_cond @{thm hd_in_mset} [with_term "hd ?xs", with_term "mset ?xs"]›

lemma last_in_mset: "xs ≠ [] ⟹ last xs ∈# mset xs" by simp
setup ‹add_forward_prfstep_cond @{thm last_in_mset} [with_term "last ?xs", with_term "mset ?xs"]›

subsection ‹Relationship between mset and set of lists›

lemma mset_butlast [rewrite]: "xs ≠ [] ⟹ mset (butlast xs) = mset xs - {# last xs #}"
  by (metis add_diff_cancel_right' append_butlast_last_id mset.simps(1) mset.simps(2) union_code)

lemma insert_mset_to_set [rewrite]: "mset xs' = mset xs + {# x #} ⟹ set xs' = set xs ∪ {x}"
  by (metis set_mset_mset set_mset_single set_mset_union)

lemma delete_mset_to_set [rewrite]:
  "distinct xs ⟹ mset xs' = mset xs - {# x #} ⟹ set xs' = set xs - {x}"
  by (metis mset_eq_setD mset_remove1 set_remove1_eq)

lemma update_mset_to_set [rewrite]:
  "distinct xs ⟹ mset xs' = {# y #} + (mset xs - {# x #}) ⟹ set xs' = (set xs - {x}) ∪ {y}"
  by (metis insert_mset_to_set mset_remove1 set_remove1_eq union_commute)

lemma mset_update' [rewrite]:
  "i < length ls ⟹ mset (ls[i := v]) = {#v#} + (mset ls - {# ls ! i #})"
  using mset_update by fastforce

subsection ‹swap›

setup ‹add_rewrite_rule @{thm mset_swap}›
setup ‹add_rewrite_rule @{thm set_swap}›

subsection ‹upto lists›

lemma upt_zero_length [rewrite]: "length [0..<n] = n" by simp
lemma nth_upt_zero [rewrite]: "i < length [0..<n] ⟹ [0..<n] ! i = i" by simp

subsection ‹Lambda lists›

definition list :: "(nat ⇒ 'a) ⇒ nat ⇒ 'a list" where
  "list s n = map s [0 ..< n]"

lemma list_length [rewrite_arg]: "length (list s n) = n" by (simp add: list_def)
lemma list_nth [rewrite]: "i < length (list s n) ⟹ (list s n) ! i = s i" by (simp add: list_def)

subsection ‹Splitting of lists›

setup ‹add_resolve_prfstep @{thm split_list}›
setup ‹add_backward_prfstep @{thm not_distinct_decomp}›

subsection ‹Finiteness›

setup ‹add_resolve_prfstep @{thm finite_lists_length_le}›

subsection ‹Cardinality›

setup ‹add_rewrite_rule @{thm distinct_card}›

end