Theory Regular_Tree_Relations.Basic_Utils

theory Basic_Utils
  imports Term_Context
begin

primrec is_Inl where
  "is_Inl (Inl q) ⟷ True"
| "is_Inl (Inr q) ⟷ False"

primrec is_Inr where
  "is_Inr (Inr q) ⟷ True"
| "is_Inr (Inl q) ⟷ False"

fun remove_sum where
  "remove_sum (Inl q) = q"
| "remove_sum (Inr q) = q"


text ‹List operations›

definition filter_rev_nth where
  "filter_rev_nth P xs i = length (filter P (take (Suc i) xs)) - 1"

lemma filter_rev_nth_butlast:
  "¬ P (last xs) ⟹ filter_rev_nth P xs i = filter_rev_nth P (butlast xs) i"
  unfolding filter_rev_nth_def
  by (induct xs arbitrary: i rule: rev_induct) (auto simp add: take_Cons')

lemma filter_rev_nth_idx:
  assumes "i < length xs" "P (xs ! i)" "ys = filter P xs"
  shows "xs ! i = ys ! (filter_rev_nth P xs i) ∧ filter_rev_nth P xs i < length ys"
  using assms unfolding filter_rev_nth_def
proof (induct xs arbitrary: ys i)
  case (Cons x xs) show ?case
  proof (cases "P x")
    case True
    then obtain ys' where *:"ys = x # ys'" using Cons(4) by auto
    show ?thesis using True Cons(1)[of "i - 1" ys'] Cons(2-)
      unfolding *
      by (cases i) (auto simp: nth_Cons' take_Suc_conv_app_nth)
  next
    case False
    then show ?thesis using Cons(1)[of "i - 1" ys] Cons(2-)
      by (auto simp: nth_Cons')
  qed
qed auto


(*replace list_of_permutation_n with n_lists *)

primrec add_elem_list_lists :: "'a ⇒ 'a list ⇒ 'a list list" where
  "add_elem_list_lists x [] = [[x]]"
| "add_elem_list_lists x (y # ys) = (x # y # ys) # (map ((#) y) (add_elem_list_lists x ys))"

lemma length_add_elem_list_lists:
  "ys ∈ set (add_elem_list_lists x xs) ⟹ length ys = Suc (length xs)"
  by (induct xs arbitrary: ys) auto

lemma add_elem_list_listsE:
  assumes "ys ∈ set (add_elem_list_lists x xs)"
  shows "∃ n ≤ length xs. ys = take n xs @ x # drop n xs" using assms
proof(induct xs arbitrary: ys)
  case (Cons a xs)
  then show ?case
    by auto fastforce
qed auto

lemma add_elem_list_listsI:
  assumes "n ≤ length xs" "ys = take n xs @ x # drop n xs"
  shows "ys ∈ set (add_elem_list_lists x xs)" using assms
proof  (induct xs arbitrary: ys n)
  case (Cons a xs)
  then show ?case
    by (cases n) (auto simp: image_iff) 
qed auto

lemma add_elem_list_lists_def':
  "set (add_elem_list_lists x xs) = {ys | ys n. n ≤ length xs ∧ ys = take n xs @ x # drop n xs}"
  using add_elem_list_listsI add_elem_list_listsE
  by fastforce

fun list_of_permutation_element_n :: "'a ⇒ nat ⇒ 'a list ⇒ 'a list list" where
  "list_of_permutation_element_n x 0 L = [[]]"
|  "list_of_permutation_element_n x (Suc n) L = concat (map (add_elem_list_lists x) (List.n_lists n L))"

lemma list_of_permutation_element_n_conv:
  assumes "n ≠ 0"
  shows "set (list_of_permutation_element_n x n L) =
    {xs | xs i. i < length xs ∧ (∀ j < length xs. j ≠ i ⟶ xs ! j ∈ set L) ∧ length xs = n ∧ xs ! i = x}" (is "?Ls = ?Rs")
proof (intro equalityI)
  from assms obtain j where [simp]: "n = Suc j" using assms by (cases n) auto
  {fix ys assume "ys ∈ ?Ls"
    then obtain xs i where wit: "xs ∈ set (List.n_lists j L)" "i ≤ length xs"
      "ys = take i xs @ x # drop i xs"
      by (auto dest: add_elem_list_listsE)
    then have "i < length ys" "length ys = Suc (length xs)" "ys ! i = x"
      by (auto simp: nth_append)
    moreover have "∀ j < length ys. j ≠ i ⟶ ys ! j ∈ set L" using wit(1, 2)
      by (auto simp: wit(3) min_def nth_append set_n_lists)
    ultimately have "ys ∈ ?Rs" using wit(1) unfolding set_n_lists
      by auto}
  then show "?Ls ⊆ ?Rs" by blast
next
  {fix xs assume "xs ∈ ?Rs"
    then obtain i where wit: "i < length xs" "∀ j < length xs. j ≠ i ⟶ xs ! j ∈ set L"
      "length xs = n" "xs ! i = x"
      by blast
    then have *: "xs ∈ set (add_elem_list_lists (xs ! i) (take i xs @ drop (Suc i) xs))"
      unfolding add_elem_list_lists_def'
      by (auto simp: min_def intro!: nth_equalityI)
         (metis Cons_nth_drop_Suc Suc_pred append_Nil append_take_drop_id assms diff_le_self diff_self_eq_0 drop_take less_Suc_eq_le nat_less_le take0)
    have [simp]: "x ∈ set (take i xs) ⟹ x ∈ set L" 
      "x ∈ set (drop (Suc i) xs) ⟹ x ∈ set L" for x using wit(2)
      by (auto simp: set_conv_nth)
    have "xs ∈ ?Ls" using wit
      by (cases "length xs")
         (auto simp: set_n_lists nth_append * min_def
               intro!: exI[of _ "take i xs @ drop (Suc i) xs"])}
  then show "?Rs ⊆ ?Ls" by blast
qed

lemma list_of_permutation_element_n_iff:
  "set (list_of_permutation_element_n x n L) =
    (if n = 0 then {[]} else {xs | xs i. i < length xs ∧ (∀ j < length xs. j ≠ i ⟶ xs ! j ∈ set L) ∧ length xs = n ∧ xs ! i = x})"
proof (cases n)
  case (Suc nat)
  then have [simp]: "Suc nat ≠ 0" by auto
  then show ?thesis
    by (auto simp: list_of_permutation_element_n_conv)
qed auto

lemma list_of_permutation_element_n_conv':
  assumes "x ∈ set L" "0 < n"
  shows "set (list_of_permutation_element_n x n L) =
      {xs. set xs ⊆ insert x (set L) ∧ length xs = n ∧ x ∈ set xs}"
proof -
  from assms(2) have *: "n ≠ 0" by simp
  show ?thesis using assms
    unfolding list_of_permutation_element_n_conv[OF *]
    by (auto simp: in_set_conv_nth) 
       (metis in_set_conv_nth insert_absorb subsetD)+
qed

text ‹Misc›

lemma in_set_idx:
  "x ∈ set xs ⟹ ∃ i < length xs. xs ! i = x"
  by (induct xs) force+

lemma set_list_subset_eq_nth_conv:
  "set xs ⊆ A ⟷ (∀ i < length xs. xs ! i ∈ A)"
  by (metis in_set_conv_nth subset_code(1))

lemma map_eq_nth_conv:
  "map f xs = map g ys ⟷ length xs = length ys ∧ (∀ i < length ys. f (xs ! i) = g (ys ! i))"
  using map_eq_imp_length_eq[of f xs g ys]
  by (auto intro: nth_equalityI) (metis nth_map)

lemma nth_append_Cons: "(xs @ y # zs) ! i =
  (if i < length xs then xs ! i else if i = length xs then y else zs ! (i - Suc (length xs)))"
  by (cases i "length xs" rule: linorder_cases, auto simp: nth_append)

lemma map_prod_times:
  "f ` A × g ` B = map_prod f g ` (A × B)"
  by auto

lemma trancl_full_on: "(X × X)⇧+ = X × X"
  using trancl_unfold_left[of "X × X"] trancl_unfold_right[of "X × X"] by auto

lemma trancl_map:
  assumes simu: "⋀x y. (x, y) ∈ r ⟹ (f x, f y) ∈ s"
    and steps: "(x, y) ∈ r⇧+"
  shows "(f x, f y) ∈ s⇧+" using steps
proof (induct)
  case (step y z) show ?case using step(3) simu[OF step(2)] 
    by auto
qed (auto simp: simu)

lemma trancl_map_prod_mono:
  "map_both f ` R⇧+ ⊆ (map_both f ` R)⇧+"
proof -
  have "(f x, f y) ∈ (map_both f ` R)⇧+" if "(x, y) ∈ R⇧+" for x y using that
    by (induct) (auto intro: trancl_into_trancl)
  then show ?thesis by auto
qed

lemma trancl_map_both_Restr:
  assumes "inj_on f X"
  shows "(map_both f ` Restr R X)⇧+ = map_both f ` (Restr R X)⇧+"
proof -
  have [simp]:
    "map_prod (inv_into X f ∘ f) (inv_into X f ∘ f) ` Restr R X = Restr R X"
    using inv_into_f_f[OF assms]
    by (intro equalityI subrelI)
       (force simp: comp_def map_prod_def image_def split: prod.splits)+
  have [simp]:
    "map_prod (f ∘ inv_into X f) (f ∘ inv_into X f) ` (map_both f ` Restr R X)⇧+ = (map_both f ` Restr R X)⇧+"
    using f_inv_into_f[of _ f X] subsetD[OF trancl_mono_set[OF image_mono[of "Restr R X" "X × X" "map_both f"]]]
    by (intro equalityI subrelI) (auto simp: map_prod_surj_on trancl_full_on comp_def rev_image_eqI)
  show ?thesis using assms trancl_map_prod_mono[of f "Restr R X"]
      image_mono[OF trancl_map_prod_mono[of "inv_into X f" "map_both f ` Restr R X"], of "map_both f"]
    by (intro equalityI) (simp_all add: image_comp map_prod.comp)
qed

lemma inj_on_trancl_map_both:
  assumes "inj_on f (fst ` R ∪ snd ` R)"
  shows "(map_both f ` R)⇧+ = map_both f ` R⇧+"
proof -
  have [simp]: "Restr R (fst ` R ∪ snd ` R) = R"
    by (force simp: image_def)
  then show ?thesis using assms
    using trancl_map_both_Restr[of f "fst ` R ∪ snd ` R" R]
    by simp
qed


lemma kleene_induct:
  "A ⊆ X ⟹ B O X ⊆ X ⟹ X O C ⊆ X ⟹ B⇧* O A O C⇧* ⊆ X"
  using relcomp_mono[OF compat_tr_compat[of B X] subset_refl, of "C⇧*"] compat_tr_compat[of "C¯" "X¯"]
    relcomp_mono[OF relcomp_mono, OF subset_refl _ subset_refl, of A X "B⇧*" "C⇧*"]
  unfolding rtrancl_converse converse_relcomp[symmetric] converse_mono by blast

lemma kleene_trancl_induct:
  "A ⊆ X ⟹ B O X ⊆ X ⟹ X O C ⊆ X ⟹ B⇧+ O A O C⇧+ ⊆ X"
  using kleene_induct[of A X B C]
  by (auto simp: rtrancl_eq_or_trancl)
     (meson relcomp.relcompI subsetD trancl_into_rtrancl)

lemma rtrancl_Un2_separatorE:
  "B O A = {} ⟹ (A ∪ B)⇧* = A⇧* ∪ A⇧* O B⇧*"
  by (metis R_O_Id empty_subsetI relcomp_distrib rtrancl_U_push rtrancl_reflcl_absorb sup_commute)

lemma trancl_Un2_separatorE:
  assumes "B O A = {}"
  shows "(A ∪ B)⇧+ = A⇧+ ∪ A⇧+ O B⇧+ ∪ B⇧+" (is "?Ls = ?Rs")
proof -
  {fix x y assume "(x, y) ∈ ?Ls"
    then have "(x, y) ∈ ?Rs" using assms
    proof (induct)
      case (step y z)
      then show ?case
        by (auto simp add: trancl_into_trancl relcomp_unfold dest: tranclD2)
    qed auto}
  then show ?thesis
    by (auto simp add: trancl_mono)
       (meson sup_ge1 sup_ge2 trancl_mono trancl_trans)
qed

text ‹Sum types where both components have the same type (to create copies)›

lemma is_InrE:
  assumes "is_Inr q"
  obtains p where "q = Inr p"
  using assms by (cases q) auto

lemma is_InlE:
  assumes "is_Inl q"
  obtains p where "q = Inl p"
  using assms by (cases q) auto

lemma not_is_Inr_is_Inl [simp]:
  "¬ is_Inl t ⟷ is_Inr t"
  "¬ is_Inr t ⟷ is_Inl t"
  by (cases t, auto)+

lemma [simp]: "remove_sum ∘ Inl = id" by auto

abbreviation CInl :: "'q ⇒ 'q + 'q" where "CInl ≡ Inl"
abbreviation CInr :: "'q ⇒ 'q + 'q" where "CInr ≡ Inr"

lemma inj_CInl: "inj CInl" "inj CInr" using inj_Inl inj_Inr by blast+

lemma map_prod_simp': "map_prod f g G = (f (fst G), g (snd G))"
  by (auto simp add: map_prod_def split!: prod.splits)

end