Theory Basic_Utils

text ‹Trivialities›
theory Basic_Utils
  imports QTRS.Trs
begin

lemma finite_check:
  fixes M
  assumes "S ⊂ {x :: nat. x ≤ M}"
  shows "finite S"
  using assms Collect_cong atMost_def finite_atMost finite_subset less_le by fastforce

lemma finite_Max:
  fixes S :: "nat set"
  assumes "finite S" and "Max S > 0" and "S ≠ {}"
  shows "Max S ∈ S"
proof (rule ccontr)
  assume A: "(Max S) ∉ S"
  have C: "∀x ∈ S. x ≤ Max S - 1" using assms A by force
  then have "Max S - 1 < Max S" using assms(2) by linarith
  then have "∃x ∈ S. x > Max S - 1" using Max_gr_iff assms(1) assms(3) by auto
  then show  False using C by auto
qed

lemma finite_nat_subset:
  assumes "S ⊆  {x :: nat. x ≤ M}"
  shows "finite S"
  using assms
  by (simp add:  finite_Collect_le_nat finite_subset)

lemma max_attain:
fixes x s assumes "finite S" "x∈ S" and "x ≥ Max S" shows "x = Max S"
proof (rule ccontr)
  assume A:"x ≠ Max S"
  have loc: "x > Max S" using assms(3) A by auto
  moreover have "x ≤ Max S" using Max_ge assms(1) assms(2) by auto
  then show False using loc by simp
qed

lemma subs:
  fixes f M
  assumes "∀m n :: nat. n < m ⟶ f n ≤ f m"
    and  "∀n. f n ≤ (M :: nat)"
  shows "∃N. ∀n. n ≥ N ⟶ f n = Max (range f)"
proof -
  have "∀x ∈ range f. x ≤ M"
    using assms(2) by auto
  then have "range f ⊆ {x :: nat. x ≤ M}"
    by auto
  then have fin:"finite (range f)" using finite_nat_subset by auto
  show ?thesis
  proof (cases "Max (range f)")
    case  0
    show ?thesis using "0"
      by (metis Max.boundedE UNIV_not_empty fin image_is_empty le_0_eq rangeI)
  next
    case (Suc m)
    have "Max (range f) ∈ range f"  using fin  finite_Max by auto
    then obtain N where loc1: "f N = Max (range f)" by auto
    then have  loc2: "∀n. n > N ⟶ f n ≥ Max (range f)" using assms(1) by fastforce
    moreover have "∀n. n = N ⟶ f n ≥ Max (range f)" using loc1 by auto
    then have "∀n. n ≥ N ⟶ f n ≥ Max (range f)" using loc2
      by (simp add: dual_order.order_iff_strict)
    then show ?thesis  using max_attain fin rangeI by blast
  qed
qed

lemma inc_set_fixpoint:
  fixes f S
  assumes "∀m n :: nat. n < m ⟶ f n ⊆ f m"
  and " ∀n. f n ⊆ S ∧ finite S"
shows "∃n. ∀m. m > n ⟶ f m = f n"
  using assms 
proof -
  let ?M = "card S"
  have ub:"∀n. (card ∘ f) n ≤ ?M"
    using assms(2) Finite_Set.card_mono by auto
  have "∀m n. n < m ⟶ (card ∘ f) n ≤ (card ∘ f) m"
    using assms(1) by (metis assms(2) card_mono comp_apply finite_subset)
  then have "∃N. ∀n. n ≥ N ⟶ (card ∘ f) n = Max (range (card ∘ f))"
    using ub subs [of "card ∘ f"] by auto
  then obtain N where obt_loc:" ∀n. n ≥ N ⟶ ((card∘f) n) = Max (range (card ∘ f))"
    by auto
  then have "∀n. n ≥ N ⟶ card (f n) = Max (range (card ∘ f))"
    using comp_def by auto
  then have loc: "∀n. n > N ⟶ f N ⊆ f n" using assms(1) by auto
  also have "∀n. n = N ⟶ f N ⊆ f n" by auto
  then have "∀n. n ≥ N ⟶ f N ⊆ f n"
    using loc by (simp add: dual_order.order_iff_strict)
  then have "∀n. n ≥ N ⟶ card (f N) = card (f n)"
    using obt_loc by auto
  then have "∀n. n ≥ N ⟶ f N = f n" using ub Finite_Set.card_subset_eq
    by (metis ‹∀n ≥ N. f N ⊆ f n› assms(2) rev_finite_subset)
   then show ?thesis using less_imp_le_nat by blast
qed

lemma inc_set_fixpoint':
  fixes f S
  assumes "∀m n :: nat. n ≤ m ⟶ f n ⊆ f m"
  and " ∀n. f n ⊆ S ∧ finite S"
shows "∃n. ∀m. m ≥ n ⟶ f m = f n"
  using assms inc_set_fixpoint[of f S] le_neq_implies_less
  by (metis less_or_eq_imp_le)

lemma inc_set_fixpoint2:
  fixes f g S
  assumes "∀m n :: nat. n ≤ m ⟶ f n ⊆ f m ∧ g n ⊆ g m"
      and "∀n. f n ⊆ S ∧ g n ⊆ S"
      and "finite S"
    shows  "∃n. ∀m ≥ n. f m = f n ∧ g m = g n"
proof -
  obtain n⇩1 n⇩2 where fixpoints:
    "∀m. m ≥ n⇩1 ⟶ f m = f n⇩1" "∀m. m ≥ n⇩2 ⟶ g m = g n⇩2"
    using inc_set_fixpoint'[of f S] inc_set_fixpoint'[of g S] assms by blast+
  define n where "n = max n⇩1 n⇩2"
  have "∀m ≥ n. f m = f n ∧ g m = g n" using fixpoints n_def
    by (metis max.boundedE max.cobounded1 max.cobounded2)
  thus ?thesis by blast
qed

lemma construct_exI':
  assumes "∀i < n. ∃x. P x i"
  shows "∃xs. length xs = n ∧ (∀i < n. P (xs ! i) i)"
  using assms
proof (induction n)
  case (Suc n)
  then obtain x where x: "P x n" by blast
  obtain xs where "length xs = n ∧ (∀i < n. P (xs ! i) i)" using Suc by auto
  hence "length (xs @ [x]) = Suc n ∧ (∀i < Suc n. P ((xs @ [x]) ! i) i)"
    using x by (simp add: less_Suc_eq nth_append)
  thus ?case by blast
qed simp

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)"
  using assms
proof (induction n)
  case (Suc n)
  then obtain x y where x_y: "P x y n" by blast
  obtain xs ys where "length xs = n ∧ length ys = n ∧ (∀i<n. P (xs ! i) (ys ! i) i)" using Suc by auto
  hence "length (xs @ [x]) = Suc n ∧ length (ys @ [y]) = Suc n ∧
    (∀i<Suc n. P ((xs @ [x]) ! i) ((ys @ [y]) ! i) i)"
    using x_y by (simp add: less_Suc_eq nth_append)
  thus ?case by blast
qed simp

(* 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)"
  using assms
proof (induction n)
  case (Suc n)
  then obtain ys where ys_n: "P (ys ! n) n" by blast
  obtain xs where "length xs = n ∧ (∀i < n. P (xs ! i) i)" using Suc by auto
  hence "length (xs @ [ys ! n]) = Suc n ∧ (∀i < Suc n. P ((xs @ [ys ! n]) ! i) i)"
    using ys_n by (simp add: less_Suc_eq nth_append)
  thus ?case by blast
qed simp

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)

end