Theory Prelims

(* Author: Alexander Maletzky *)

section ‹Preliminaries›

theory Prelims
  imports Polynomials.Utils Groebner_Bases.General
begin

subsection ‹Lists›

subsubsection ‹Sequences of Lists›

lemma list_seq_length_mono:
  fixes seq :: "nat ⇒ 'a list"
  assumes "⋀i. (∃x. seq (Suc i) = x # seq i)" and "i < j"
  shows "length (seq i) < length (seq j)"
proof -
  from assms(2) obtain k where "j = Suc (i + k)" using less_iff_Suc_add by auto
  show ?thesis unfolding ‹j = Suc (i + k)›
  proof (induct k)
    case 0
    from assms(1) obtain x where eq: "seq (Suc i) = x # seq i" ..
    show ?case by (simp add: eq)
  next
    case (Suc k)
    from assms(1) obtain x where "seq (Suc (i + Suc k)) = x # seq (i + Suc k)" ..
    hence eq: "seq (Suc (Suc (i + k))) = x # seq (Suc (i + k))" by simp
    note Suc
    also have "length (seq (Suc (i + k))) < length (seq (Suc (i + Suc k)))" by (simp add: eq)
    finally show ?case .
  qed
qed

corollary list_seq_length_mono_weak:
  fixes seq :: "nat ⇒ 'a list"
  assumes "⋀i. (∃x. seq (Suc i) = x # seq i)" and "i ≤ j"
  shows "length (seq i) ≤ length (seq j)"
proof (cases "i = j")
  case True
  thus ?thesis by simp
next
  case False
  with assms(2) have "i < j" by simp
  with assms(1) have "length (seq i) < length (seq j)" by (rule list_seq_length_mono)
  thus ?thesis by simp
qed

lemma list_seq_indexE_length:
  fixes seq :: "nat ⇒ 'a list"
  assumes "⋀i. (∃x. seq (Suc i) = x # seq i)"
  obtains j where "i < length (seq j)"
proof (induct i arbitrary: thesis)
  case 0
  have "0 ≤ length (seq 0)" by simp
  also from assms lessI have "... < length (seq (Suc 0))" by (rule list_seq_length_mono)
  finally show ?case by (rule 0)
next
  case (Suc i)
  obtain j where "i < length (seq j)" by (rule Suc(1))
  hence "Suc i ≤ length (seq j)" by simp
  also from assms lessI have "... < length (seq (Suc j))" by (rule list_seq_length_mono)
  finally show ?case by (rule Suc(2))
qed

lemma list_seq_nth:
  fixes seq :: "nat ⇒ 'a list"
  assumes "⋀i. (∃x. seq (Suc i) = x # seq i)" and "i < length (seq j)" and "j ≤ k"
  shows "rev (seq k) ! i = rev (seq j) ! i"
proof -
  from assms(3) obtain l where "k = j + l" using nat_le_iff_add by blast
  show ?thesis unfolding ‹k = j + l›
  proof (induct l)
    case 0
    show ?case by simp
  next
    case (Suc l)
    note assms(2)
    also from assms(1) le_add1 have "length (seq j) ≤ length (seq (j + l))"
      by (rule list_seq_length_mono_weak)
    finally have i: "i < length (seq (j + l))" .
    from assms(1) obtain x where "seq (Suc (j + l)) = x # seq (j + l)" ..
    thus ?case by (simp add: nth_append i Suc)
  qed
qed

corollary list_seq_nth':
  fixes seq :: "nat ⇒ 'a list"
  assumes "⋀i. (∃x. seq (Suc i) = x # seq i)" and "i < length (seq j)" and "i < length (seq k)"
  shows "rev (seq k) ! i = rev (seq j) ! i"
proof (rule linorder_cases)
  assume "j < k"
  hence "j ≤ k" by simp
  with assms(1, 2) show ?thesis by (rule list_seq_nth)
next
  assume "k < j"
  hence "k ≤ j" by simp
  with assms(1, 3) have "rev (seq j) ! i = rev (seq k) ! i" by (rule list_seq_nth)
  thus ?thesis by (rule HOL.sym)
next
  assume "j = k"
  thus ?thesis by simp
qed

subsubsection ‹@{const filter}›

lemma filter_merge_wrt_1:
  assumes "⋀y. y ∈ set ys ⟹ P y ⟹ False"
  shows "filter P (merge_wrt rel xs ys) = filter P xs"
  using assms
proof (induct rel xs ys rule: merge_wrt.induct)
  case (1 rel xs)
  show ?case by simp
next
  case (2 rel y ys)
  hence "P y ⟹ False" and "⋀z. z ∈ set ys ⟹ P z ⟹ False" by auto
  thus ?case by (auto simp: filter_empty_conv)
next
  case (3 rel x xs y ys)
  hence "¬ P y" and x: "⋀z. z ∈ set ys ⟹ P z ⟹ False" by auto
  have a: "filter P (merge_wrt rel xs ys) = filter P xs" if "x = y" using that x by (rule 3(1))
  have b: "filter P (merge_wrt rel xs (y # ys)) = filter P xs" if "x ≠ y" and "rel x y"
    using that 3(4) by (rule 3(2))
  have c: "filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs)" if "x ≠ y" and "¬ rel x y"
    using that x by (rule 3(3))
  show ?case by (simp add: a b c ‹¬ P y›)
qed

lemma filter_merge_wrt_2:
  assumes "⋀x. x ∈ set xs ⟹ P x ⟹ False"
  shows "filter P (merge_wrt rel xs ys) = filter P ys"
  using assms
proof (induct rel xs ys rule: merge_wrt.induct)
  case (1 rel xs)
  thus ?case by (auto simp: filter_empty_conv)
next
  case (2 rel y ys)
  show ?case by simp
next
  case (3 rel x xs y ys)
  hence "¬ P x" and x: "⋀z. z ∈ set xs ⟹ P z ⟹ False" by auto
  have a: "filter P (merge_wrt rel xs ys) = filter P ys" if "x = y" using that x by (rule 3(1))
  have b: "filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys)" if "x ≠ y" and "rel x y"
    using that x by (rule 3(2))
  have c: "filter P (merge_wrt rel (x # xs) ys) = filter P ys" if "x ≠ y" and "¬ rel x y"
    using that 3(4) by (rule 3(3))
  show ?case by (simp add: a b c ‹¬ P x›)
qed

lemma length_filter_le_1:
  assumes "length (filter P xs) ≤ 1" and "i < length xs" and "j < length xs"
    and "P (xs ! i)" and "P (xs ! j)"
  shows "i = j"
proof -
  have *: thesis if "a < b" and "b < length xs"
    and "⋀as bs cs. as @ ((xs ! a) # (bs @ ((xs ! b) # cs))) = xs ⟹ thesis" for a b thesis
  proof (rule that(3))
    from that(1, 2) have 1: "a < length xs" by simp
    with that(1, 2) have 2: "b - Suc a < length (drop (Suc a) xs)" by simp
    from that(1) ‹a < length xs› have eq: "xs ! b = drop (Suc a) xs ! (b - Suc a)" by simp
    show "(take a xs) @ ((xs ! a) # ((take (b - Suc a) (drop (Suc a) xs)) @ ((xs ! b) #
                  drop (Suc (b - Suc a)) (drop (Suc a) xs)))) = xs"
      by (simp only: eq id_take_nth_drop[OF 1, symmetric] id_take_nth_drop[OF 2, symmetric])
  qed
  show ?thesis
  proof (rule linorder_cases)
    assume "i < j"
    then obtain as bs cs where "as @ ((xs ! i) # (bs @ ((xs ! j) # cs))) = xs"
      using assms(3) by (rule *)
    hence "filter P xs = filter P (as @ ((xs ! i) # (bs @ ((xs ! j) # cs))))" by simp
    also from assms(4, 5) have "... = (filter P as) @ ((xs ! i) # ((filter P bs) @ ((xs ! j) # (filter P cs))))"
      by simp
    finally have "¬ length (filter P xs) ≤ 1" by simp
    thus ?thesis using assms(1) ..
  next
    assume "j < i"
    then obtain as bs cs where "as @ ((xs ! j) # (bs @ ((xs ! i) # cs))) = xs"
      using assms(2) by (rule *)
    hence "filter P xs = filter P (as @ ((xs ! j) # (bs @ ((xs ! i) # cs))))" by simp
    also from assms(4, 5) have "... = (filter P as) @ ((xs ! j) # ((filter P bs) @ ((xs ! i) # (filter P cs))))"
      by simp
    finally have "¬ length (filter P xs) ≤ 1" by simp
    thus ?thesis using assms(1) ..
  qed
qed

lemma length_filter_eq [simp]: "length (filter ((=) x) xs) = count_list xs x"
  by (induct xs, simp_all)

subsubsection ‹@{const drop}›

lemma nth_in_set_dropI:
  assumes "j ≤ i" and "i < length xs"
  shows "xs ! i ∈ set (drop j xs)"
  using assms
proof (induct xs arbitrary: i j)
  case Nil
  thus ?case by simp
next
  case (Cons x xs)
  show ?case
  proof (cases j)
    case 0
    with Cons(3) show ?thesis by (metis drop0 nth_mem)
  next
    case (Suc j0)
    with Cons(2) Suc_le_D obtain i0 where i: "i = Suc i0" by blast
    with Cons(2) have "j0 ≤ i0" by (simp add: ‹j = Suc j0›)
    moreover from Cons(3) have "i0 < length xs" by (simp add: i)
    ultimately have "xs ! i0 ∈ set (drop j0 xs)" by (rule Cons(1))
    thus ?thesis by (simp add: i ‹j = Suc j0›)
  qed
qed

subsubsection ‹@{const count_list}›

lemma count_list_upt [simp]: "count_list [a..<b] x = (if a ≤ x ∧ x < b then 1 else 0)"
proof (cases "a ≤ b")
  case True
  then obtain k where "b = a + k" using le_Suc_ex by blast
  show ?thesis unfolding ‹b = a + k› by (induct k, simp_all)
next
  case False
  thus ?thesis by simp
qed

subsubsection ‹@{const sorted_wrt}›

lemma sorted_wrt_upt_iff: "sorted_wrt rel [a..<b] ⟷ (∀i j. a ≤ i ⟶ i < j ⟶ j < b ⟶ rel i j)"
proof (cases "a ≤ b")
  case True
  then obtain k where "b = a + k" using le_Suc_ex by blast
  show ?thesis unfolding ‹b = a + k›
  proof (induct k)
    case 0
    show ?case by simp
  next
    case (Suc k)
    show ?case
    proof (simp add: sorted_wrt_append Suc, intro iffI allI ballI impI conjI)
      fix i j
      assume "(∀i≥a. ∀j>i. j < a + k ⟶ rel i j) ∧ (∀x∈{a..<a + k}. rel x (a + k))"
      hence 1: "⋀i' j'. a ≤ i' ⟹ i' < j' ⟹ j' < a + k ⟹ rel i' j'"
        and 2: "⋀x. a ≤ x ⟹ x < a + k ⟹ rel x (a + k)" by simp_all
      assume "a ≤ i" and "i < j"
      assume "j < Suc (a + k)"
      hence "j < a + k ∨ j = a + k" by auto
      thus "rel i j"
      proof
        assume "j < a + k"
        with ‹a ≤ i› ‹i < j› show ?thesis by (rule 1)
      next
        assume "j = a + k"
        from ‹a ≤ i› ‹i < j› show ?thesis unfolding ‹j = a + k› by (rule 2)
      qed
    next
      fix i j
      assume "∀i≥a. ∀j>i. j < Suc (a + k) ⟶ rel i j" and "a ≤ i" and "i < j" and "j < a + k"
      thus "rel i j" by simp
    next
      fix x
      assume "x ∈ {a..<a + k}"
      hence "a ≤ x" and "x < a + k" by simp_all
      moreover assume "∀i≥a. ∀j>i. j < Suc (a + k) ⟶ rel i j"
      ultimately show "rel x (a + k)" by simp
    qed
  qed
next
  case False
  thus ?thesis by simp
qed

subsubsection ‹@{const insort_wrt} and @{const merge_wrt}›

lemma map_insort_wrt:
  assumes "⋀x. x ∈ set xs ⟹ r2 (f y) (f x) ⟷ r1 y x"
  shows "map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs)"
  using assms
proof (induct xs)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  have "x ∈ set (x # xs)" by simp
  hence "r2 (f y) (f x) = r1 y x" by (rule Cons(2))
  moreover have "map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs)"
  proof (rule Cons(1))
    fix x'
    assume "x' ∈ set xs"
    hence "x' ∈ set (x # xs)" by simp
    thus "r2 (f y) (f x') = r1 y x'" by (rule Cons(2))
  qed
  ultimately show ?case by simp
qed

lemma map_merge_wrt:
  assumes "f ` set xs ∩ f ` set ys = {}"
    and "⋀x y. x ∈ set xs ⟹ y ∈ set ys ⟹ r2 (f x) (f y) ⟷ r1 x y"
  shows "map f (merge_wrt r1 xs ys) = merge_wrt r2 (map f xs) (map f ys)"
  using assms
proof (induct r1 xs ys rule: merge_wrt.induct)
  case (1 uu xs)
  show ?case by simp
next
  case (2 r1 v va)
  show ?case by simp
next
  case (3 r1 x xs y ys)
  from 3(4) have "f x ≠ f y" and 1: "f ` set xs ∩ f ` set (y # ys) = {}"
    and 2: "f ` set (x # xs) ∩ f ` set ys = {}" by auto
  from this(1) have "x ≠ y" by auto
  have eq2: "map f (merge_wrt r1 xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys))"
    if "r1 x y" using ‹x ≠ y› that 1
  proof (rule 3(2))
    fix a b
    assume "a ∈ set xs"
    hence "a ∈ set (x # xs)" by simp
    moreover assume "b ∈ set (y # ys)"
    ultimately show "r2 (f a) (f b) ⟷ r1 a b" by (rule 3(5))
  qed
  have eq3: "map f (merge_wrt r1 (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys)"
    if "¬ r1 x y" using ‹x ≠ y› that 2
  proof (rule 3(3))
    fix a b
    assume "a ∈ set (x # xs)"
    assume "b ∈ set ys"
    hence "b ∈ set (y # ys)" by simp
    with ‹a ∈ set (x # xs)› show "r2 (f a) (f b) ⟷ r1 a b" by (rule 3(5))
  qed
  have eq4: "r2 (f x) (f y) ⟷ r1 x y" by (rule 3(5), simp_all)
  show ?case by (simp add: eq2 eq3 eq4 ‹f x ≠ f y› ‹x ≠ y›)
qed

subsection ‹Recursive Functions›

locale recursive =
  fixes h' :: "'b ⇒ 'b"
  fixes b :: 'b
  assumes b_fixpoint: "h' b = b"
begin

context
  fixes Q :: "'a ⇒ bool"
  fixes g :: "'a ⇒ 'b"
  fixes h :: "'a ⇒ 'a"
begin

function (domintros) recfun_aux :: "'a ⇒ 'b" where
  "recfun_aux x = (if Q x then g x else h' (recfun_aux (h x)))"
  by pat_completeness auto

lemmas [induct del] = recfun_aux.pinduct

definition dom :: "'a ⇒ bool"
  where "dom x ⟷ (∃k. Q ((h ^^ k) x))"

lemma domI:
  assumes "¬ Q x ⟹ dom (h x)"
  shows "dom x"
proof (cases "Q x")
  case True
  hence "Q ((h ^^ 0) x)" by simp
  thus ?thesis unfolding dom_def ..
next
  case False
  hence "dom (h x)" by (rule assms)
  then obtain k where "Q ((h ^^ k) (h x))" unfolding dom_def ..
  hence "Q ((h ^^ (Suc k)) x)" by (simp add: funpow_swap1)
  thus ?thesis unfolding dom_def ..
qed

lemma domD:
  assumes "dom x" and "¬ Q x"
  shows "dom (h x)"
proof -
  from assms(1) obtain k where *: "Q ((h ^^ k) x)" unfolding dom_def ..
  with assms(2) have "k ≠ 0" using funpow_0 by fastforce
  then obtain m where "k = Suc m" using nat.exhaust by blast
  with * have "Q ((h ^^ m) (h x))" by (simp add: funpow_swap1)
  thus ?thesis unfolding dom_def ..
qed

lemma recfun_aux_domI:
  assumes "dom x"
  shows "recfun_aux_dom x"
proof -
  from assms obtain k where "Q ((h ^^ k) x)" unfolding dom_def ..
  thus ?thesis
  proof (induct k arbitrary: x)
    case 0
    hence "Q x" by simp
    with recfun_aux.domintros show ?case by blast
  next
    case (Suc k)
    from Suc(2) have "Q ((h ^^ k) (h x))" by (simp add: funpow_swap1)
    hence "recfun_aux_dom (h x)" by (rule Suc(1))
    with recfun_aux.domintros show ?case by blast
  qed
qed

lemma recfun_aux_domD:
  assumes "recfun_aux_dom x"
  shows "dom x"
  using assms
proof (induct x rule: recfun_aux.pinduct)
  case (1 x)
  show ?case
  proof (cases "Q x")
    case True
    with domI show ?thesis by blast
  next
    case False
    hence "dom (h x)" by (rule 1(2))
    thus ?thesis using domI by blast
  qed
qed

corollary recfun_aux_dom_alt: "recfun_aux_dom = dom"
  by (auto dest: recfun_aux_domI recfun_aux_domD)

definition "fun" :: "'a ⇒ 'b"
  where "fun x = (if recfun_aux_dom x then recfun_aux x else b)"

lemma simps: "fun x = (if Q x then g x else h' (fun (h x)))"
proof (cases "dom x")
  case True
  hence dom: "recfun_aux_dom x" by (rule recfun_aux_domI)
  show ?thesis
  proof (cases "Q x")
    case True
    with dom show ?thesis by (simp add: fun_def recfun_aux.psimps)
  next
    case False
    have "recfun_aux_dom (h x)" by (rule recfun_aux_domI, rule domD, fact True, fact False)
    thus ?thesis by (simp add: fun_def dom False recfun_aux.psimps)
  qed
next
  case False
  moreover have "¬ Q x"
  proof
    assume "Q x"
    hence "dom x" using domI by blast
    with False show False ..
  qed
  moreover have "¬ dom (h x)"
  proof
    assume "dom (h x)"
    hence "dom x" using domI by blast
    with False show False ..
  qed
  ultimately show ?thesis by (simp add: recfun_aux_dom_alt fun_def b_fixpoint split del: if_split)
qed

lemma eq_fixpointI: "¬ dom x ⟹ fun x = b"
  by (simp add: fun_def recfun_aux_dom_alt)

lemma pinduct: "dom x ⟹ (⋀x. dom x ⟹ (¬ Q x ⟹ P (h x)) ⟹ P x) ⟹ P x"
  unfolding recfun_aux_dom_alt[symmetric] by (fact recfun_aux.pinduct)

end

end (* recursive *)

interpretation tailrec: recursive "λx. x" undefined
  by (standard, fact refl)

subsection ‹Binary Relations›

lemma almost_full_on_Int:
  assumes "almost_full_on P1 A1" and "almost_full_on P2 A2"
  shows "almost_full_on (λx y. P1 x y ∧ P2 x y) (A1 ∩ A2)" (is "almost_full_on ?P ?A")
proof (rule almost_full_onI)
  fix f :: "nat ⇒ 'a"
  assume a: "∀i. f i ∈ ?A"
  define g where "g = (λi. (f i, f i))"
  from assms have "almost_full_on (prod_le P1 P2) (A1 × A2)" by (rule almost_full_on_Sigma)
  moreover from a have "⋀i. g i ∈ A1 × A2" by (simp add: g_def)
  ultimately obtain i j where "i < j" and "prod_le P1 P2 (g i) (g j)" by (rule almost_full_onD)
  from this(2) have "?P (f i) (f j)" by (simp add: g_def prod_le_def)
  with ‹i < j› show "good ?P f" by (rule goodI)
qed

corollary almost_full_on_same:
  assumes "almost_full_on P1 A" and "almost_full_on P2 A"
  shows "almost_full_on (λx y. P1 x y ∧ P2 x y) A"
proof -
  from assms have "almost_full_on (λx y. P1 x y ∧ P2 x y) (A ∩ A)" by (rule almost_full_on_Int)
  thus ?thesis by simp
qed

context ord
begin

definition is_le_rel :: "('a ⇒ 'a ⇒ bool) ⇒ bool"
  where "is_le_rel rel = (rel = (=) ∨ rel = (≤) ∨ rel = (<))"

lemma is_le_relI [simp]: "is_le_rel (=)" "is_le_rel (≤)" "is_le_rel (<)"
  by (simp_all add: is_le_rel_def)

lemma is_le_relE:
  assumes "is_le_rel rel"
  obtains "rel = (=)" | "rel = (≤)" | "rel = (<)"
  using assms unfolding is_le_rel_def by blast

end (* ord *)

context preorder
begin

lemma is_le_rel_le:
  assumes "is_le_rel rel"
  shows "rel x y ⟹ x ≤ y"
  using assms by (rule is_le_relE, auto dest: less_imp_le)

lemma is_le_rel_trans:
  assumes "is_le_rel rel"
  shows "rel x y ⟹ rel y z ⟹ rel x z"
  using assms by (rule is_le_relE, auto dest: order_trans less_trans)

lemma is_le_rel_trans_le_left:
  assumes "is_le_rel rel"
  shows "x ≤ y ⟹ rel y z ⟹ x ≤ z"
  using assms by (rule is_le_relE, auto dest: order_trans le_less_trans less_imp_le)

lemma is_le_rel_trans_le_right:
  assumes "is_le_rel rel"
  shows "rel x y ⟹ y ≤ z ⟹ x ≤ z"
  using assms by (rule is_le_relE, auto dest: order_trans less_le_trans less_imp_le)

lemma is_le_rel_trans_less_left:
  assumes "is_le_rel rel"
  shows "x < y ⟹ rel y z ⟹ x < z"
  using assms by (rule is_le_relE, auto dest: less_le_trans less_imp_le)

lemma is_le_rel_trans_less_right:
  assumes "is_le_rel rel"
  shows "rel x y ⟹ y < z ⟹ x < z"
  using assms by (rule is_le_relE, auto dest: le_less_trans less_imp_le)

end (* preorder *)

context order
begin

lemma is_le_rel_distinct:
  assumes "is_le_rel rel"
  shows "rel x y ⟹ x ≠ y ⟹ x < y"
  using assms by (rule is_le_relE, auto)

lemma is_le_rel_antisym:
  assumes "is_le_rel rel"
  shows "rel x y ⟹ rel y x ⟹ x = y"
  using assms by (rule is_le_relE, auto)

end (* order *)

end (* theory *)