Theory Option_ord

(*  Title:      HOL/Library/Option_ord.thy
    Author:     Florian Haftmann, TU Muenchen
*)

section ‹Canonical order on option type›

theory Option_ord
imports Main
begin

unbundle lattice_syntax

instantiation option :: (preorder) preorder
begin

definition less_eq_option where
  "x ≤ y ⟷ (case x of None ⇒ True | Some x ⇒ (case y of None ⇒ False | Some y ⇒ x ≤ y))"

definition less_option where
  "x < y ⟷ (case y of None ⇒ False | Some y ⇒ (case x of None ⇒ True | Some x ⇒ x < y))"

lemma less_eq_option_None [simp]: "None ≤ x"
  by (simp add: less_eq_option_def)

lemma less_eq_option_None_code [code]: "None ≤ x ⟷ True"
  by simp

lemma less_eq_option_None_is_None: "x ≤ None ⟹ x = None"
  by (cases x) (simp_all add: less_eq_option_def)

lemma less_eq_option_Some_None [simp, code]: "Some x ≤ None ⟷ False"
  by (simp add: less_eq_option_def)

lemma less_eq_option_Some [simp, code]: "Some x ≤ Some y ⟷ x ≤ y"
  by (simp add: less_eq_option_def)

lemma less_option_None [simp, code]: "x < None ⟷ False"
  by (simp add: less_option_def)

lemma less_option_None_is_Some: "None < x ⟹ ∃z. x = Some z"
  by (cases x) (simp_all add: less_option_def)

lemma less_option_None_Some [simp]: "None < Some x"
  by (simp add: less_option_def)

lemma less_option_None_Some_code [code]: "None < Some x ⟷ True"
  by simp

lemma less_option_Some [simp, code]: "Some x < Some y ⟷ x < y"
  by (simp add: less_option_def)

instance
  by standard
    (auto simp add: less_eq_option_def less_option_def less_le_not_le
      elim: order_trans split: option.splits)

end

instance option :: (order) order
  by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)

instance option :: (linorder) linorder
  by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)

instantiation option :: (order) order_bot
begin

definition bot_option where "⊥ = None"

instance
  by standard (simp add: bot_option_def)

end

instantiation option :: (order_top) order_top
begin

definition top_option where "⊤ = Some ⊤"

instance
  by standard (simp add: top_option_def less_eq_option_def split: option.split)

end

instance option :: (wellorder) wellorder
proof
  fix P :: "'a option ⇒ bool"
  fix z :: "'a option"
  assume H: "⋀x. (⋀y. y < x ⟹ P y) ⟹ P x"
  have "P None" by (rule H) simp
  then have P_Some [case_names Some]: "P z" if "⋀x. z = Some x ⟹ (P ∘ Some) x" for z
    using ‹P None› that by (cases z) simp_all
  show "P z"
  proof (cases z rule: P_Some)
    case (Some w)
    show "(P ∘ Some) w"
    proof (induct rule: less_induct)
      case (less x)
      have "P (Some x)"
      proof (rule H)
        fix y :: "'a option"
        assume "y < Some x"
        show "P y"
        proof (cases y rule: P_Some)
          case (Some v)
          with ‹y < Some x› have "v < x" by simp
          with less show "(P ∘ Some) v" .
        qed
      qed
      then show ?case by simp
    qed
  qed
qed

instantiation option :: (inf) inf
begin

definition inf_option where
  "x ⊓ y = (case x of None ⇒ None | Some x ⇒ (case y of None ⇒ None | Some y ⇒ Some (x ⊓ y)))"

lemma inf_None_1 [simp, code]: "None ⊓ y = None"
  by (simp add: inf_option_def)

lemma inf_None_2 [simp, code]: "x ⊓ None = None"
  by (cases x) (simp_all add: inf_option_def)

lemma inf_Some [simp, code]: "Some x ⊓ Some y = Some (x ⊓ y)"
  by (simp add: inf_option_def)

instance ..

end

instantiation option :: (sup) sup
begin

definition sup_option where
  "x ⊔ y = (case x of None ⇒ y | Some x' ⇒ (case y of None ⇒ x | Some y ⇒ Some (x' ⊔ y)))"

lemma sup_None_1 [simp, code]: "None ⊔ y = y"
  by (simp add: sup_option_def)

lemma sup_None_2 [simp, code]: "x ⊔ None = x"
  by (cases x) (simp_all add: sup_option_def)

lemma sup_Some [simp, code]: "Some x ⊔ Some y = Some (x ⊔ y)"
  by (simp add: sup_option_def)

instance ..

end

instance option :: (semilattice_inf) semilattice_inf
proof
  fix x y z :: "'a option"
  show "x ⊓ y ≤ x"
    by (cases x, simp_all, cases y, simp_all)
  show "x ⊓ y ≤ y"
    by (cases x, simp_all, cases y, simp_all)
  show "x ≤ y ⟹ x ≤ z ⟹ x ≤ y ⊓ z"
    by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
qed

instance option :: (semilattice_sup) semilattice_sup
proof
  fix x y z :: "'a option"
  show "x ≤ x ⊔ y"
    by (cases x, simp_all, cases y, simp_all)
  show "y ≤ x ⊔ y"
    by (cases x, simp_all, cases y, simp_all)
  fix x y z :: "'a option"
  show "y ≤ x ⟹ z ≤ x ⟹ y ⊔ z ≤ x"
    by (cases y, simp_all, cases z, simp_all, cases x, simp_all)
qed

instance option :: (lattice) lattice ..

instance option :: (lattice) bounded_lattice_bot ..

instance option :: (bounded_lattice_top) bounded_lattice_top ..

instance option :: (bounded_lattice_top) bounded_lattice ..

instance option :: (distrib_lattice) distrib_lattice
proof
  fix x y z :: "'a option"
  show "x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)"
    by (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
qed

instantiation option :: (complete_lattice) complete_lattice
begin

definition Inf_option :: "'a option set ⇒ 'a option" where
  "⨅A = (if None ∈ A then None else Some (⨅Option.these A))"

lemma None_in_Inf [simp]: "None ∈ A ⟹ ⨅A = None"
  by (simp add: Inf_option_def)

definition Sup_option :: "'a option set ⇒ 'a option" where
  "⨆A = (if A = {} ∨ A = {None} then None else Some (⨆Option.these A))"

lemma empty_Sup [simp]: "⨆{} = None"
  by (simp add: Sup_option_def)

lemma singleton_None_Sup [simp]: "⨆{None} = None"
  by (simp add: Sup_option_def)

instance
proof
  fix x :: "'a option" and A
  assume "x ∈ A"
  then show "⨅A ≤ x"
    by (cases x) (auto simp add: Inf_option_def in_these_eq intro: Inf_lower)
next
  fix z :: "'a option" and A
  assume *: "⋀x. x ∈ A ⟹ z ≤ x"
  show "z ≤ ⨅A"
  proof (cases z)
    case None then show ?thesis by simp
  next
    case (Some y)
    show ?thesis
      by (auto simp add: Inf_option_def in_these_eq Some intro!: Inf_greatest dest!: *)
  qed
next
  fix x :: "'a option" and A
  assume "x ∈ A"
  then show "x ≤ ⨆A"
    by (cases x) (auto simp add: Sup_option_def in_these_eq intro: Sup_upper)
next
  fix z :: "'a option" and A
  assume *: "⋀x. x ∈ A ⟹ x ≤ z"
  show "⨆A ≤ z "
  proof (cases z)
    case None
    with * have "⋀x. x ∈ A ⟹ x = None" by (auto dest: less_eq_option_None_is_None)
    then have "A = {} ∨ A = {None}" by blast
    then show ?thesis by (simp add: Sup_option_def)
  next
    case (Some y)
    from * have "⋀w. Some w ∈ A ⟹ Some w ≤ z" .
    with Some have "⋀w. w ∈ Option.these A ⟹ w ≤ y"
      by (simp add: in_these_eq)
    then have "⨆Option.these A ≤ y" by (rule Sup_least)
    with Some show ?thesis by (simp add: Sup_option_def)
  qed
next
  show "⨆{} = (⊥::'a option)"
    by (auto simp: bot_option_def)
  show "⨅{} = (⊤::'a option)"
    by (auto simp: top_option_def Inf_option_def)
qed

end

lemma Some_Inf:
  "Some (⨅A) = ⨅(Some ` A)"
  by (auto simp add: Inf_option_def)

lemma Some_Sup:
  "A ≠ {} ⟹ Some (⨆A) = ⨆(Some ` A)"
  by (auto simp add: Sup_option_def)

lemma Some_INF:
  "Some (⨅x∈A. f x) = (⨅x∈A. Some (f x))"
  by (simp add: Some_Inf image_comp)

lemma Some_SUP:
  "A ≠ {} ⟹ Some (⨆x∈A. f x) = (⨆x∈A. Some (f x))"
  by (simp add: Some_Sup image_comp)

lemma option_Inf_Sup: "⨅(Sup ` A) ≤ ⨆(Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y})"
  for A :: "('a::complete_distrib_lattice option) set set"
proof (cases "{} ∈ A")
  case True
  then show ?thesis
    by (rule INF_lower2, simp_all)
next
  case False
  from this have X: "{} ∉ A"
    by simp
  then show ?thesis
  proof (cases "{None} ∈ A")
    case True
    then show ?thesis
      by (rule INF_lower2, simp_all)
  next
    case False

    {fix y
      assume A: "y ∈ A"
      have "Sup (y - {None}) = Sup y"
        by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq)
      from A and this have "(∃z. y - {None} = z - {None} ∧ z ∈ A) ∧ ⨆y = ⨆(y - {None})"
        by auto
    }
    from this have A: "Sup ` A = (Sup ` {y - {None} | y. y∈A})"
      by (auto simp add: image_def)

    have [simp]: "⋀y. y ∈ A ⟹ ∃ya. {ya. ∃x. x ∈ y ∧ (∃y. x = Some y) ∧ ya = the x} 
          = {y. ∃x∈ya - {None}. y = the x} ∧ ya ∈ A"
      by (rule exI, auto)

    have [simp]: "⋀y. y ∈ A ⟹
         (∃ya. y - {None} = ya - {None} ∧ ya ∈ A) ∧ ⨆{ya. ∃x∈y - {None}. ya = the x} 
          = ⨆{ya. ∃x. x ∈ y ∧ (∃y. x = Some y) ∧ ya = the x}"
      apply (safe, blast)
      by (rule arg_cong [of _ _ Sup], auto)
    {fix y
      assume [simp]: "y ∈ A"
      have "∃x. (∃y. x = {ya. ∃x∈y - {None}. ya = the x} ∧ y ∈ A) ∧ ⨆{ya. ∃x. x ∈ y ∧ (∃y. x = Some y) ∧ ya = the x} = ⨆x"
      and "∃x. (∃y. x = y - {None} ∧ y ∈ A) ∧ ⨆{ya. ∃x∈y - {None}. ya = the x} = ⨆{y. ∃xa. xa ∈ x ∧ (∃y. xa = Some y) ∧ y = the xa}"
         apply (rule exI [of _ "{ya. ∃x. x ∈ y ∧ (∃y. x = Some y) ∧ ya = the x}"], simp)
        by (rule exI [of _ "y - {None}"], simp)
    }
    from this have C: "(λx.  (⨆Option.these x)) ` {y - {None} |y. y ∈ A} =  (Sup ` {the ` (y - {None}) |y. y ∈ A})"
      by (simp add: image_def Option.these_def, safe, simp_all)
  
    have D: "∀ f . ∃Y∈A. f Y ∉ Y ⟹ False"
      by (drule spec [of _ "λ Y . SOME x . x ∈ Y"], simp add: X some_in_eq)
  
    define F where "F = (λ Y . SOME x::'a option . x ∈ (Y - {None}))"
  
    have G: "⋀ Y . Y ∈ A ⟹ ∃ x . x ∈ Y - {None}"
      by (metis False X all_not_in_conv insert_Diff_single these_insert_None these_not_empty_eq)
  
    have F: "⋀ Y . Y ∈ A ⟹ F Y ∈ (Y - {None})"
      by (metis F_def G empty_iff some_in_eq)
  
    have "Some ⊥ ≤ Inf (F ` A)"
      by (metis (no_types, lifting) Diff_iff F Inf_option_def bot.extremum image_iff 
          less_eq_option_Some singletonI)
      
    from this have "Inf (F ` A) ≠ None"
      by (cases "⨅x∈A. F x", simp_all)

    from this have "Inf (F ` A) ≠ None ∧ Inf (F ` A) ∈ Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y}"
      using F by auto

    from this have "∃ x . x ≠ None ∧ x ∈ Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y}"
      by blast
  
    from this have E:" Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y} = {None} ⟹ False"
      by blast

    have [simp]: "((⨆x∈{f ` A |f. ∀Y∈A. f Y ∈ Y}. ⨅x) = None) = False"
      by (metis (no_types, lifting) E Sup_option_def ‹∃x. x ≠ None ∧ x ∈ Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y}› 
          ex_in_conv option.simps(3))
  
    have B: "Option.these ((λx. Some (⨆Option.these x)) ` {y - {None} |y. y ∈ A}) 
        = ((λx. (⨆ Option.these x)) ` {y - {None} |y. y ∈ A})"
      by (metis image_image these_image_Some_eq)
    {
      fix f
      assume A: "⋀ Y . (∃y. Y = the ` (y - {None}) ∧ y ∈ A) ⟹ f Y ∈ Y"

      have "⋀xa. xa ∈ A ⟹ f {y. ∃a∈xa - {None}. y = the a} = f (the ` (xa - {None}))"
        by  (simp add: image_def)
      from this have [simp]: "⋀xa. xa ∈ A ⟹ ∃x∈A. f {y. ∃a∈xa - {None}. y = the a} = f (the ` (x - {None}))"
        by blast
      have "⋀xa. xa ∈ A ⟹ f (the ` (xa - {None})) = f {y. ∃a ∈ xa - {None}. y = the a} ∧ xa ∈ A"
        by (simp add: image_def)
      from this have [simp]: "⋀xa. xa ∈ A ⟹ ∃x. f (the ` (xa - {None})) = f {y. ∃a∈x - {None}. y = the a} ∧ x ∈ A"
        by blast

      {
        fix Y
        have "Y ∈ A ⟹ Some (f (the ` (Y - {None}))) ∈ Y"
          using A [of "the ` (Y - {None})"] apply (simp add: image_def)
          using option.collapse by fastforce
      }
      from this have [simp]: "⋀ Y . Y ∈ A ⟹ Some (f (the ` (Y - {None}))) ∈ Y"
        by blast
      have [simp]: "(⨅x∈A. Some (f {y. ∃x∈x - {None}. y = the x})) = ⨅{Some (f {y. ∃a∈x - {None}. y = the a}) |x. x ∈ A}"
        by (simp add: Setcompr_eq_image)
      
      have [simp]: "∃x. (∃f. x = {y. ∃x∈A. y = f x} ∧ (∀Y∈A. f Y ∈ Y)) ∧ ⨅{Some (f {y. ∃a∈x - {None}. y = the a}) |x. x ∈ A} = ⨅x"
        apply (rule exI [of _ "{Some (f {y. ∃a∈x - {None}. y = the a}) | x . x∈ A}"], safe)
        by (rule exI [of _ "(λ Y . Some (f (the ` (Y - {None})))) "], safe, simp_all)

      {
        fix xb
        have "xb ∈ A ⟹ (⨅x∈{{ya. ∃x∈y - {None}. ya = the x} |y. y ∈ A}. f x) ≤ f {y. ∃x∈xb - {None}. y = the x}"
          apply (rule INF_lower2 [of "{y. ∃x∈xb - {None}. y = the x}"])
          by blast+
      }
      from this have [simp]: "(⨅x∈{the ` (y - {None}) |y. y ∈ A}. f x) ≤ the (⨅Y∈A. Some (f (the ` (Y - {None}))))"
        apply (simp add: Inf_option_def image_def Option.these_def)
        by (rule Inf_greatest, clarsimp)
      have [simp]: "the (⨅Y∈A. Some (f (the ` (Y - {None})))) ∈ Option.these (Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y})"
        apply (auto simp add: Option.these_def)
        apply (rule imageI)
        apply auto
        using ‹⋀Y. Y ∈ A ⟹ Some (f (the ` (Y - {None}))) ∈ Y› apply blast
        apply (auto simp add: Some_INF [symmetric])
        done
      have "(⨅x∈{the ` (y - {None}) |y. y ∈ A}. f x) ≤ ⨆Option.these (Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y})"
        by (rule Sup_upper2 [of "the (Inf ((λ Y . Some (f (the ` (Y - {None})) )) ` A))"], simp_all)
    }
    from this have X: "⋀ f . ∀Y. (∃y. Y = the ` (y - {None}) ∧ y ∈ A) ⟶ f Y ∈ Y ⟹
      (⨅x∈{the ` (y - {None}) |y. y ∈ A}. f x) ≤ ⨆Option.these (Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y})"
      by blast
    

    have [simp]: "⋀ x . x∈{y - {None} |y. y ∈ A} ⟹  x ≠ {} ∧ x ≠ {None}"
      using F by fastforce

    have "(Inf (Sup `A)) = (Inf (Sup ` {y - {None} | y. y∈A}))"
      by (subst A, simp)

    also have "... = (⨅x∈{y - {None} |y. y ∈ A}. if x = {} ∨ x = {None} then None else Some (⨆Option.these x))"
      by (simp add: Sup_option_def)

    also have "... = (⨅x∈{y - {None} |y. y ∈ A}. Some (⨆Option.these x))"
      using G by fastforce
  
    also have "... = Some (⨅Option.these ((λx. Some (⨆Option.these x)) ` {y - {None} |y. y ∈ A}))"
      by (simp add: Inf_option_def, safe)
  
    also have "... =  Some (⨅ ((λx.  (⨆Option.these x)) ` {y - {None} |y. y ∈ A}))"
      by (simp add: B)
  
    also have "... = Some (Inf (Sup ` {the ` (y - {None}) |y. y ∈ A}))"
      by (unfold C, simp)
    thm Inf_Sup
    also have "... = Some (⨆x∈{f ` {the ` (y - {None}) |y. y ∈ A} |f. ∀Y. (∃y. Y = the ` (y - {None}) ∧ y ∈ A) ⟶ f Y ∈ Y}. ⨅x) "
      by (simp add: Inf_Sup)
  
    also have "... ≤ ⨆ (Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y})"
    proof (cases "⨆ (Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y})")
      case None
      then show ?thesis by (simp add: less_eq_option_def)
    next
      case (Some a)
      then show ?thesis
        apply simp
        apply (rule Sup_least, safe)
        apply (simp add: Sup_option_def)
        apply (cases "(∀f. ∃Y∈A. f Y ∉ Y) ∨ Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y} = {None}", simp_all)
        by (drule X, simp)
    qed
    finally show ?thesis by simp
  qed
qed

instance option :: (complete_distrib_lattice) complete_distrib_lattice
  by (standard, simp add: option_Inf_Sup)

instance option :: (complete_linorder) complete_linorder ..

unbundle no lattice_syntax

end