Theory Basic_Utils

text ‹Trivialities›
theory Basic_Utils
  imports TRS.Trs Deriving.Compare_Order_Instances TRS.Multihole_Context
begin

(********************************* TO MOVE SECTION **************************)
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 sum_list_drop:
  assumes "sum_list (x # xs) = length ys"
  shows "sum_list xs = length (drop x ys)"
  using assms by (induct xs arbitrary: ys) auto

lemma sum_list_relativ_idx_length:
  assumes "sum_list xs = length ys"
      and "i < length xs" and "sum_list (drop i xs) > 0"
    shows "sum_list (take i xs) < length ys"
  using assms
proof (induction xs arbitrary: ys)
  case (Cons x xs)
  then show ?case
    by (cases i, auto) (metis add_strict_left_mono append_take_drop_id less_add_same_cancel1 sum_list.append)
qed auto

lemma sum_list_drop_greater_nth:
  assumes "i < length (xs :: nat list)"
  shows "xs ! i ≤ sum_list (drop i xs)"
  using assms
proof (induct xs arbitrary: i)
  case (Cons a xs)
  then show ?case by (cases i) auto
qed auto

lemma take1_drop [simp]:
  assumes "sum_list (take i ys) < length xs"
  shows "take (Suc 0) (drop (sum_list (take i ys)) xs) = [xs ! (sum_list (take i ys))]"
  using assms by (metis Cons_nth_drop_Suc take0 take_Suc_Cons)

lemma fill_holes_MHole2 [simp]:
  assumes "sum_list (map num_holes cs) = length ss" and "i < length cs" and "cs ! i = MHole"
  shows "fill_holes (cs ! i) (partition_holes ss cs ! i) = ss ! (sum_list (take i (map num_holes cs)))"
  using assms sum_list_drop_greater_nth[of i "map num_holes cs"] partition_by_nth[of i "map num_holes cs" ss]
  using sum_list_relativ_idx_length[OF assms(1), of i]
  by auto

lemma fill_holes_MHole_length:
  assumes "sum_list (map num_holes cs) = length ss" and "i < length cs" and "cs ! i = MHole"
  shows "sum_list (take i (map num_holes cs)) < length ss"
  using assms sum_list_drop_greater_nth[of i "map num_holes cs"]
  using sum_list_relativ_idx_length[OF assms(1)]
  by auto

lemma gmctxt_no_holes_gterm:
  assumes "num_holes C = 0" and "ground_mctxt C"
  shows "ground (term_of_mctxt C)"
  using assms by (induct C) auto

lemma fill_holes_empty_id [simp]:
  assumes "num_holes C = 0"
  shows "fill_holes C [] = term_of_mctxt C"
  using assms by (metis mctxt_of_term_fill_holes mctxt_of_term_term_of_mctxt_id)

lemma map_append_Cons_nth:
  assumes "i < Suc (length xs + length ys)"
  shows "(map f xs @ f x # map f ys) ! i = f ((xs @ x # ys) ! i)"
  using assms by (auto simp: nth_append_Cons)

(********************************* FINISHED THE TO MOVE SECTION **************************)

lemma linear_term_comb_subst:
  assumes "linear_term (Fun f ss)"
    and "length ss = length ts"
    and "⋀ i. i < length ts ⟹ ss ! i ⋅ σ i = ts ! i"
  shows "∃ σ. Fun f ss ⋅ σ = Fun f ts"
  using assms subst_merge[of ss "σ"]
  apply auto apply (rule_tac x = σ' in exI)
  apply (intro nth_equalityI) apply auto
  by (metis term_subst_eq)


lemmas construct_exI' = Ex_list_of_length_P

lemma construct_exI'_double:
  assumes "∀i < n. ∃x y. P x y i"
  shows "∃xs ys. length xs = n ∧ length ys = n ∧ (∀i < n. P (xs ! i) (ys ! i) i)"
proof -
  from assms obtain f g where "P (f i) (g i) i" if "i < n" for i using assms by metis
  then show ?thesis by (intro exI[of _ "map _ [0..<n]"]) auto
qed

lemma construct_exI'_quadraple:
  assumes "∀i < n. ∃x y z w. P x y z w i"
  shows "∃xs ys zs ws. length xs = n ∧ length ys = n ∧  length zs = n ∧  length ws = n 
  ∧ (∀i < n. P (xs ! i) (ys ! i) (zs!i) (ws!i) i)"
proof -
  from assms obtain f1 f2 f3 f4 where "P (f1 i) (f2 i) (f3 i) (f4 i) i" if "i < n" for i using assms 
    by metis
  then show ?thesis by (intro exI[of _ "map _ [0..<n]"]) auto
qed


(* TODO: check whether this is still needed *)
lemma construct_exI:
  assumes "∀i < n. ∃xs. P (xs ! i) i"
  shows "∃xs. length xs = n ∧ (∀i < n. P (xs ! i) i)"
proof -
  guess xss using construct_exI'[OF assms] by (elim exE)
  then show ?thesis by (intro exI[of _ "map (λi. xss ! i ! i) [0..<n]"]) auto
qed

definition right_ground_trs :: "('f, 'v) trs ⇒ bool" where
  "right_ground_trs R ≡ ∀(l, r) ∈ R. ground r"

definition ground_trs :: "('f, 'v) trs ⇒ bool" where
  "ground_trs R ≡ ∀(l, r) ∈ R. ground l ∧ ground r"

lemma ground_imp_right_ground_trs [simp]:
  "ground_trs R ⟹ right_ground_trs R"
  unfolding ground_trs_def right_ground_trs_def by fast

definition set_to_list :: "'a set ⇒ 'a list"
  where "set_to_list s = (SOME l. set l = s)"

lemma set_set_to_list:
  "finite s ⟹ set (set_to_list s) = s"
  unfolding set_to_list_def by (metis (mono_tags) finite_list some_eq_ex)

(*
lemma assumes "finite F"
"∀ls ∈ S. ∀i < length ls. (ls!i) ∈ F"
shows "finite S" using assms 
*)
thm "finite_lists_length_eq"


lemma assumes "(n::nat) ≥ 1" 
  shows "∀i < (n::nat). i ∈ {0..(n-1)}"
  using assms by auto


lemma 
  fixes n::"nat"
  assumes "n ≥ 1" "infinite S"
          "∀ls ∈ S. length ls = n"
  shows "∃i < n. infinite {(ls!i)|ls. ls ∈ S}"
proof(rule ccontr)
  assume " ¬ (∃i<n. infinite {ls ! i |ls. ls ∈ S})"
  hence fin_all:"∀i ∈  {(0::nat)..n - 1}. finite  {ls ! i |ls. ls ∈ S}"  using assms(1) by auto
  define F where "F = (⋃i∈{0..(n-1)}. {ls ! i |ls. ls ∈ S})" 
  hence F:"F =   (UNION {0..n - 1} (λ i.{ls ! i |ls. ls ∈ S}))" by auto
  have 0:"finite {0..(n-1)}" by auto
  have fin:"finite F" using finite_UN[OF 0] fin_all F by simp
  hence fin_ss:"finite  {xs. set xs ⊆ F ∧ length xs = n}"
    using finite_lists_length_eq[OF fin] by auto
  have "∀ls ∈ S.∀ i < length ls. ls!i ∈ F"  using F assms by fastforce
  hence "S ⊆  {xs. set xs ⊆ F ∧ length xs = n}" using assms(3) 
    using in_set_idx by force
  hence "finite S" using fin_ss 
    using finite_subset by auto
  thus False using assms(2) by simp
qed

lemma list_pigeonhole:
  fixes n::"nat"
  assumes "n ≥ 1" "infinite S"
          "∀ls ∈ S. length ls = n"
  shows "∃i < n. infinite {(ls!i)|ls. ls ∈ S}"
proof(rule ccontr)
  assume " ¬ (∃i<n. infinite {ls ! i |ls. ls ∈ S})"
  hence fin_all:"∀i ∈  {(0::nat)..n - 1}. finite  {ls ! i |ls. ls ∈ S}"  using assms(1) by auto
  define F where "F = (⋃i∈{0..(n-1)}. {ls ! i |ls. ls ∈ S})" 
  hence F:"F =   (UNION {0..n - 1} (λ i.{ls ! i |ls. ls ∈ S}))" by auto
  have 0:"finite {0..(n-1)}" by auto
  have fin:"finite F" using finite_UN[OF 0] fin_all F by simp
  hence fin_ss:"finite  {xs. set xs ⊆ F ∧ length xs = n}"
    using finite_lists_length_eq[OF fin] by auto
  have "∀ls ∈ S.∀ i < length ls. ls!i ∈ F"  using F assms by fastforce
  hence "S ⊆  {xs. set xs ⊆ F ∧ length xs = n}" using assms(3) 
    using in_set_idx by force
  hence "finite S" using fin_ss 
    using finite_subset by auto
  thus False using assms(2) by simp
qed

lemma tail_list_pigeonhole:
  assumes "n > m" "m ≥ 1"
  "∀ls ∈  S. length ls = n" 
  "∀i < m. finite {((ls::'a list)!i) | ls . ls ∈ (S::'a list set)}"
  "infinite S"
shows "∃i ≥ m. infinite {(ls!i)|ls . ls ∈ S}"
proof(rule ccontr)
  assume "¬(∃i ≥ m. infinite {(ls!i)|ls . ls ∈ S})"
  hence "∀i ≥ m. finite  {(ls!i)|ls . ls ∈ S}" by auto
  hence fin_all:"∀i < n.   finite  {(ls!i)|ls . ls ∈ S}" using assms(1,3,4) 
    by (meson not_le)
  hence fin_all:"∀i ∈ {0..(n-1)}.   finite  {(ls!i)|ls . ls ∈ S}" using assms(1,2) by auto
  define F where "F = (⋃i∈{0..(n-1)}. {ls ! i |ls. ls ∈ S})" 
  hence F:"F =   (UNION {0..n - 1} (λ i.{ls ! i |ls. ls ∈ S}))" by auto
  have 0:"finite {0..(n-1)}" by auto
  have fin:"finite F" using finite_UN[OF 0] fin_all F by simp
  hence fin_ss:"finite  {xs. set xs ⊆ F ∧ length xs = n}"
    using finite_lists_length_eq[OF fin] by auto
  have "∀ls ∈ S.∀ i < length ls. ls!i ∈ F"  using F assms by fastforce
  hence "S ⊆  {xs. set xs ⊆ F ∧ length xs = n}" using assms(3) 
    using in_set_idx by force
  hence "finite S" using fin_ss 
    using finite_subset by auto
  thus False using assms(5) by simp
qed

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

lemma Restr_simps:
  "R ⊆ X × X ⟹ Restr (R⇧+) X = R⇧+"
  "R ⊆ X × X ⟹ Restr Id X O R = R"
  "R ⊆ X × X ⟹ R O Restr Id X = R"
  "R ⊆ X × X ⟹ S ⊆ X × X ⟹ Restr (R O S) X = R O S"
  "R ⊆ X × X ⟹ R⇧+ ⊆ X × X"
  subgoal using trancl_mono_set[of R "X × X"] by (auto simp: trancl_full_on)
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal using trancl_subset_Sigma .
  done

lemma inj_on_by_inj:
  "inj f ⟹ inj_on f X"
  unfolding inj_on_def by auto

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 swap_trancl:
  "(prod.swap ` R)⇧+ = prod.swap ` (R⇧+)"
proof -
  have [simp]: "prod.swap ` X = X¯" for X by auto
  show ?thesis by (simp add: trancl_converse)
qed

lemma swap_rtrancl:
  "(prod.swap ` R)⇧* = prod.swap ` (R⇧*)"
proof -
  have [simp]: "prod.swap ` X = X¯" for X by auto
  show ?thesis by (simp add: rtrancl_converse)
qed

subsection ‹map finite set to natural numbers›

definition map_set_to_nat :: "('a :: linorder) set ⇒ 'a ⇒ nat" where
  "map_set_to_nat X = (λx. the (mem_idx x (sorted_list_of_set X)))"

lemma map_set_to_nat_inj:
  assumes "finite X"
  shows "inj_on (map_set_to_nat X) X"
proof -
  { fix x y assume "x ∈ X" "y ∈ X"
    then have "x ∈ set (sorted_list_of_set X)" "y ∈ set (sorted_list_of_set X)"
      using set_sorted_list_of_set[OF assms] by simp_all
    note this[unfolded mem_idx_sound]
    then have "x = y" if "map_set_to_nat X x = map_set_to_nat X y"
      using that nth_eq_iff_index_eq[OF distinct_sorted_list_of_set[of X]]
      by (force dest: mem_idx_sound_output simp: map_set_to_nat_def) }
  then show ?thesis by (simp add: inj_on_def)
qed

abbreviation map_both where
  "map_both f ≡ map_prod f f"

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]
    apply (intro equalityI subrelI)
     apply (auto simp: comp_def map_prod_def image_def)
    apply (metis (no_types, lifting) IntI SigmaI case_prod_conv)
    done
  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

lemmas trancl_map_both = trancl_map_both_Restr[of _ UNIV, unfolded UNIV_Times_UNIV Int_UNIV_right]

lemma map_both_relcomp:
  "inj_on f (snd ` A ∪ fst ` B) ⟹ map_both f ` A O map_both f ` B = map_both f ` (A O B)"
  by (force simp: inj_on_def intro: rev_image_eqI)

lemma subterm_set_finite:
  shows "finite {t . s ⊳ t}"
proof (induction s)
  case (Var x) have [simp]: "{t. Var x ⊳ t}  = {}" by auto
  then show ?case by auto
next
  case (Fun f ts)
  have "{t. Fun f ts ⊳ t} = (set ts) ∪ {t | s t. s ∈ set ts ∧ s ⊳ t}" by auto
  moreover have "finite {t | s t. s ∈ set ts ∧ s ⊳ t}" using Fun by auto
  ultimately show ?case by auto
qed

end