Theory Containers.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  (xset 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