# Theory Containers.Containers_Auxiliary

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

theory Containers_Auxiliary imports
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)"

lemma set_bind_iff:
"set (List.bind xs f) = Set.bind (set xs) (set ∘ f)"

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)"

lemma ID_Some: "ID (Some x) = Some x"

lemma ID_None: "ID None = None"

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"

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

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