Theory Containers_Auxiliary

(*  Title:      Containers/Containers_Auxiliary.thy
    Author:     Andreas Lochbihler, KIT *)

theory Containers_Auxiliary imports
  "HOL-Library.Monad_Syntax"
begin

chapter ‹An executable linear order on sets›
text_raw ‹\label{chapter:linear:order:set}›

section ‹Auxiliary definitions›

lemma insert_bind_set: "insert a A ⤜ f = f a ∪ (A ⤜ f)"
by(auto simp add: Set.bind_def)

lemma set_bind_iff:
  "set (List.bind xs f) = Set.bind (set xs) (set ∘ f)"
by(induct xs)(simp_all add: insert_bind_set)

lemma set_bind_conv_fold: "set xs ⤜ f = fold ((∪) ∘ f) xs {}"
by(induct xs rule: rev_induct)(simp_all add: insert_bind_set)

lemma card_gt_1D:
  assumes "card A > 1"
  shows "∃x y. x ∈ A ∧ y ∈ A ∧ x ≠ y"
proof(rule ccontr)
  from assms have "A ≠ {}" by auto
  then obtain x where "x ∈ A" by auto
  moreover
  assume "¬ ?thesis"
  ultimately have "A = {x}" by auto
  with assms show False by simp
qed

lemma card_eq_1_iff: "card A = 1 ⟷ (∃x. A = {x})"
proof
  assume card: "card A = 1"
  hence [simp]: "finite A" using card_gt_0_iff[of A] by simp
  have "A = {THE x. x ∈ A}"
  proof(intro equalityI subsetI)
    fix x
    assume x: "x ∈ A"
    hence "(THE x. x ∈ A) = x"
    proof(rule the_equality)
      fix x'
      assume x': "x' ∈ A"
      show "x' = x"
      proof(rule ccontr)
        assume neq: "x' ≠ x"
        from x x' have eq: "A = insert x (insert x' (A - {x, x'}))" by auto
        have "card A = 2 + card (A - {x, x'})" using neq by(subst eq)(simp)
        with card show False by simp
      qed
    qed
    thus "x ∈ {THE x. x ∈ A}" by simp
  next
    fix x
    assume "x ∈ {THE x. x ∈ A}"
    hence x: "x = (THE x. x ∈ A)" by simp
    from card have "A ≠ {}" by auto
    then obtain x' where x': "x' ∈ A" by blast
    thus "x ∈ A" unfolding x
    proof(rule theI)
      fix x
      assume x: "x ∈ A"
      show "x = x'"
      proof(rule ccontr)
        assume neq: "x ≠ x'"
        from x x' have eq: "A = insert x (insert x' (A - {x, x'}))" by auto
        have "card A = 2 + card (A - {x, x'})" using neq by(subst eq)(simp)
        with card show False by simp
      qed
    qed
  qed
  thus "∃x. A = {x}" ..
qed auto

lemma card_eq_Suc_0_ex1: "card A = Suc 0 ⟷ (∃!x. x ∈ A)"
by(auto simp only: One_nat_def[symmetric] card_eq_1_iff)

context linorder begin

lemma sorted_last: "⟦ sorted xs; x ∈ set xs ⟧ ⟹ x ≤ last xs"
by(cases xs rule: rev_cases)(auto simp add: sorted_append)

end

lemma empty_filter_conv: "[] = filter P xs ⟷ (∀x∈set xs. ¬ P x)"
by(auto dest: sym simp add: filter_empty_conv)


definition ID :: "'a ⇒ 'a" where "ID = id"

lemma ID_code [code, code_unfold]: "ID = (λx. x)"
by(simp add: ID_def id_def)

lemma ID_Some: "ID (Some x) = Some x"
by(simp add: ID_def)

lemma ID_None: "ID None = None" 
by(simp add: ID_def)

text ‹lexicographic order on pairs›

context
  fixes leq_a :: "'a ⇒ 'a ⇒ bool" (infix "⊑⇩a" 50) 
  and less_a :: "'a ⇒ 'a ⇒ bool" (infix "⊏⇩a" 50) 
  and leq_b :: "'b ⇒ 'b ⇒ bool" (infix "⊑⇩b" 50) 
  and less_b :: "'b ⇒ 'b ⇒ bool" (infix "⊏⇩b" 50) 
begin

definition less_eq_prod :: "('a × 'b) ⇒ ('a × 'b) ⇒ bool" (infix "⊑" 50)
where "less_eq_prod = (λ(x1, x2) (y1, y2). x1 ⊏⇩a y1 ∨ x1 ⊑⇩a y1 ∧ x2 ⊑⇩b y2)"

definition less_prod :: "('a × 'b) ⇒ ('a × 'b) ⇒ bool" (infix "⊏" 50)
where "less_prod = (λ(x1, x2) (y1, y2). x1 ⊏⇩a y1 ∨ x1 ⊑⇩a y1 ∧ x2 ⊏⇩b y2)"

lemma less_eq_prod_simps [simp]:
  "(x1, x2) ⊑ (y1, y2) ⟷ x1 ⊏⇩a y1 ∨ x1 ⊑⇩a y1 ∧ x2 ⊑⇩b y2"
by(simp add: less_eq_prod_def)

lemma less_prod_simps [simp]:
  "(x1, x2) ⊏ (y1, y2) ⟷ x1 ⊏⇩a y1 ∨ x1 ⊑⇩a y1 ∧ x2 ⊏⇩b y2"
by(simp add: less_prod_def)

end

context
  fixes leq_a :: "'a ⇒ 'a ⇒ bool" (infix "⊑⇩a" 50) 
  and less_a :: "'a ⇒ 'a ⇒ bool" (infix "⊏⇩a" 50) 
  and leq_b :: "'b ⇒ 'b ⇒ bool" (infix "⊑⇩b" 50) 
  and less_b :: "'b ⇒ 'b ⇒ bool" (infix "⊏⇩b" 50) 
  assumes lin_a: "class.linorder leq_a less_a" 
  and lin_b: "class.linorder leq_b less_b"
begin

abbreviation (input) less_eq_prod' :: "('a × 'b) ⇒ ('a × 'b) ⇒ bool" (infix "⊑" 50)
where "less_eq_prod' ≡ less_eq_prod leq_a less_a leq_b"

abbreviation (input) less_prod' :: "('a × 'b) ⇒ ('a × 'b) ⇒ bool" (infix "⊏" 50)
where "less_prod' ≡ less_prod leq_a less_a less_b"

lemma linorder_prod:
  "class.linorder (⊑) (⊏)"
proof -
  interpret a: linorder "(⊑⇩a)" "(⊏⇩a)" by(fact lin_a)
  interpret b: linorder "(⊑⇩b)" "(⊏⇩b)" by(fact lin_b)
  show ?thesis by unfold_locales auto
qed

end

hide_const less_eq_prod' less_prod'

end