Theory Phi_BI.Phi_Aug

theory Phi_Aug ― ‹Augmenting to the Standard Library›
  imports Main
begin

section ‹List›

subsection ‹Combinators›

lemma fun_comp_intr_left[no_atp]:
  ‹f = g ⟹ x o f = x o g›
  by simp

setup ‹Sign.mandatory_path "comb"›

definition ‹K x = (λ_. x)› ― ‹to improve the performance as any lambda expression ‹λ_. x› is not
  cached within the internal system of Isabelle.›

lemma K_app[simp]:
  ‹ comb.K x y = x ›
  unfolding comb.K_def ..

lemma K_comp[simp]:
  ‹ comb.K x o f = comb.K x ›
  unfolding fun_eq_iff comb.K_def
  by simp

lemmas K_comp'[simp] = comb.K_comp[THEN fun_comp_intr_left, folded comp_assoc]
  

setup ‹Sign.parent_path›

subsection ‹Length Preserving Map›

definition length_preserving_map :: ‹'a list set ⇒ ('a list ⇒ 'a list) ⇒ bool›
  where ‹length_preserving_map D f ⟷ (∀l ∈ D. length (f l) = length l)›

lemma length_preserving_map__map[simp, intro!]:
  ‹ length_preserving_map D (map f) ›
  unfolding length_preserving_map_def
  by simp 

lemma length_preserving_map__id[simp, intro!]:
  ‹ length_preserving_map D id ›
  unfolding length_preserving_map_def by simp

lemma length_preserving_map__id'[simp, intro!]:
  ‹ length_preserving_map D (λx. x) ›
  unfolding length_preserving_map_def by simp

lemma length_preserving_map__funcomp[simp, intro!]:
  ‹ length_preserving_map (g ` D) f
⟹ length_preserving_map D g
⟹ length_preserving_map D (f o g) ›
  unfolding length_preserving_map_def
  by clarsimp

lemma length_preserving_map_comb_K[simp, intro!]:
  ‹ length_preserving_map D (comb.K xs) = (∀x∈D. length xs = length x) › 
  unfolding length_preserving_map_def
  by clarsimp


subsection ‹Mapping at a single element›

definition list_upd_map :: ‹nat ⇒ ('a ⇒ 'a) ⇒ 'a list ⇒ 'a list›
  where ‹list_upd_map i f l = l[i := f (l ! i)]›

lemma length_preserving_map__list_upd_map [simp, intro!]:
  ‹ length_preserving_map D (list_upd_map i f) ›
  unfolding length_preserving_map_def list_upd_map_def
  by force

lemma list_upd_map_const_f[simp]:
  ‹ list_upd_map i (λx. v) xs = xs[i := v] ›
  unfolding list_upd_map_def ..

lemma list_upd_map_0_eval[simp]:
  ‹ list_upd_map 0 f (h # l) = (f h # l) ›
  unfolding list_upd_map_def
  by simp

lemma list_upd_map_N_eval[simp]:
  ‹ list_upd_map (numeral n) f (h # l) = (h # list_upd_map (numeral n - 1) f l) ›
  unfolding list_upd_map_def
  by simp

lemma list_upd_map_Suc_eval[simp]:
  ‹ list_upd_map (Suc n) f (h # l) = (h # list_upd_map n f l) ›
  unfolding list_upd_map_def
  by simp

lemma length_list_upd_map[iff]:
  ‹ length (list_upd_map i f l) = length l ›
  unfolding list_upd_map_def
  by clarsimp

lemma take_list_upd_map_le[simp]:
  ‹ i ≤ j
⟹ take j (list_upd_map i f l) = list_upd_map i f (take j l) ›
  unfolding list_upd_map_def
  by (metis nth_take order_le_imp_less_or_eq take_update_cancel take_update_swap)

lemma take_list_upd_map_gt[simp]:
  ‹ j < i
⟹ take j (list_upd_map i f l) = take j l ›
  unfolding list_upd_map_def
  by simp

lemma drop_list_upd_map_lt[simp]:
  ‹ i < j
⟹ drop j (list_upd_map i f l) = drop j l ›
  unfolding list_upd_map_def
  by simp

lemma drop_list_upd_map_ge[simp]:
  ‹ j ≤ i
⟹ drop j (list_upd_map i f l) = list_upd_map (i-j) f (drop j l) ›
  unfolding list_upd_map_def
  by (metis Nat.add_diff_assoc add_diff_cancel_left' drop_all drop_update_swap length_list_update less_imp_le_nat linorder_not_le nth_drop)
  
lemma list_upd_map_i[iff]:
  ‹ i < length l
⟹ list_upd_map i f l ! i = f (l ! i) ›
  unfolding list_upd_map_def
  by clarsimp

lemma list_upd_map_j[iff]:
  ‹ j ≠ i
⟹ list_upd_map i f l ! j = l ! j ›
  unfolding list_upd_map_def
  by clarsimp

lemma list_upd_map_ij:
  ‹ j < length l
⟹ list_upd_map i f l ! j = (if j = i then f (l ! i) else l ! j) ›
  unfolding list_upd_map_def
  by auto


subsection ‹Mapping Prefix / Suffix›

definition sublist_map_L :: ‹nat ⇒ ('a list ⇒ 'a list) ⇒ 'a list ⇒ 'a list›
  ― ‹applies on the left N elements›
  where ‹sublist_map_L N f l = f (take N l) @ drop N l›

definition sublist_map_R :: ‹nat ⇒ ('a list ⇒ 'a list) ⇒ 'a list ⇒ 'a list›
  ― ‹applies on the right (len-N) elements›
  where ‹sublist_map_R N f l = take N l @ f (drop N l)›

lemma length_preserving_map__sublist_map_R [simp, intro!]:
  ‹ length_preserving_map (drop N ` D) f
⟹ length_preserving_map D (sublist_map_R N f) ›
  unfolding length_preserving_map_def sublist_map_R_def
  by (clarify, simp)

lemma length_preserving_map__sublist_map_L [simp, intro!]:
  ‹ length_preserving_map (take N ` D) f
⟹ length_preserving_map D (sublist_map_L N f) ›
  unfolding length_preserving_map_def
  by (clarify, simp add: sublist_map_L_def)

lemma sublist_map_L_id[simp]:
  ‹ sublist_map_L N id = id ›
  unfolding fun_eq_iff sublist_map_L_def
  by clarsimp

lemma sublist_map_L_id'[simp]:
  ‹ sublist_map_L N (λx. x) = (λx. x) ›
  unfolding fun_eq_iff sublist_map_L_def
  by clarsimp

lemma sublist_map_R_id[simp]:
  ‹ sublist_map_R N id = id ›
  unfolding sublist_map_R_def fun_eq_iff
  by clarsimp

lemma sublist_map_R_id'[simp]:
  ‹ sublist_map_R N (λx. x) = (λx. x) ›
  unfolding sublist_map_R_def fun_eq_iff
  by clarsimp

lemma sublist_map_L_sublist_map_L[simp]:
  ‹ M ≤ N
⟹ sublist_map_L N (sublist_map_L M f) = sublist_map_L M f ›
  unfolding sublist_map_L_def
  by (clarsimp, metis (no_types, opaque_lifting) append_take_drop_id diff_add drop_drop take_drop)

lemma sublist_map_L_funcomp[simp]:
  ‹ length_preserving_map UNIV f
⟹ length_preserving_map UNIV g
⟹ sublist_map_L N (f o g) = sublist_map_L N f o sublist_map_L N g ›
  unfolding sublist_map_L_def fun_eq_iff length_preserving_map_def
  by (clarsimp simp add: min_def)

lemma sublist_map_R_sublist_map_R[simp]:
  ‹ sublist_map_R N (sublist_map_R M f) = sublist_map_R (N+M) f ›
  unfolding sublist_map_R_def
  by (clarsimp, metis add.commute append_assoc take_add)

lemma sublist_map_R_funcomp[simp]:
  ‹ length_preserving_map UNIV f
⟹ length_preserving_map UNIV g
⟹ sublist_map_R N (f o g) = sublist_map_R N f o sublist_map_R N g ›
  unfolding sublist_map_R_def length_preserving_map_def fun_eq_iff
  by (clarsimp, metis (no_types, opaque_lifting) append_Nil append_take_drop_id cancel_comm_monoid_add_class.diff_cancel diff_le_self drop_all list.size(3) min_def take0)

lemma sublist_map_L_at_i[simp]:
  ‹ i < N
⟹ sublist_map_L N (list_upd_map i f) = list_upd_map i f›
  unfolding fun_eq_iff sublist_map_L_def list_upd_map_def
  by (clarsimp, metis append_take_drop_id drop_update_cancel take_update_swap)

lemma sublist_map_R_at_i[simp]:
  ‹ sublist_map_R N (list_upd_map i f) = list_upd_map (N+i) f›
  unfolding fun_eq_iff sublist_map_R_def list_upd_map_def
  by (clarsimp,
      smt (verit) add_diff_cancel_left' append_take_drop_id drop_all length_take less_or_eq_imp_le linorder_not_less list_update_append list_update_nonempty min.absorb4 min_less_iff_conj not_add_less1 nth_drop)



section ‹Option›

definition zip_option :: ‹'a option × 'b option ⇒ ('a × 'b) option›
  where ‹zip_option xy = (case xy of (Some x, Some y) ⇒ Some (x,y)
                                   | _ ⇒ None)›

definition ‹unzip_option x = (map_option fst x, map_option snd x)›

lemma zip_option_simps[iff]:
  ‹ zip_option (Some a, Some b) = Some (a,b) ›
  ‹ zip_option (x, None) = None ›
  ‹ zip_option (None, y) = None ›
  unfolding zip_option_def
  by (simp_all, cases x, simp+)

lemma unzip_option_simps[iff]:
  ‹ unzip_option None = (None, None) ›
  ‹ unzip_option (Some (a,b)) = (Some a, Some b) ›
  unfolding unzip_option_def
  by simp_all

lemma unzip_zip_option[iff]:
  ‹ case_prod (rel_option (λ_ _. True)) x
⟹ unzip_option (zip_option x) = x ›
  by (cases x; case_tac a; case_tac b; simp)

lemma zip_option_prj[simp]:
  ‹ fst (unzip_option x) = map_option fst x ›
  ‹ snd (unzip_option x) = map_option snd x ›
  unfolding unzip_option_def
  by simp_all


section ‹Partial Map›

definition zip_partial_map :: ‹('a ⇀ 'b) × ('a ⇀ 'c) ⇒ ('a ⇀ 'b × 'c)›
  where ‹zip_partial_map x = (case x of (f,g) ⇒ (λk. zip_option (f k, g k)))›

definition unzip_partial_map :: ‹('a ⇀ 'b × 'c) ⇒ ('a ⇀ 'b) × ('a ⇀ 'c)›
  where ‹unzip_partial_map x = (map_option fst o x, map_option snd o x)›

lemma unzip_zip_partial_map[iff]:
  ‹ dom (fst x) = dom (snd x)
⟹ unzip_partial_map (zip_partial_map x) = x ›
  unfolding unzip_partial_map_def zip_partial_map_def
  by (cases x; clarsimp simp: fun_eq_iff zip_option_def split: option.split; metis domIff)

end