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 (xA. f x) = (xA. Some (f x))"
  by (simp add: Some_Inf image_comp)

lemma Some_SUP:
  "A  {}  Some (xA. f x) = (xA. Some (f x))"
  by (simp add: Some_Sup image_comp)

lemma option_Inf_Sup: "(Sup ` A)  (Inf ` {f ` A |f. YA. 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. yA})"
      by (auto simp add: image_def)

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

    have [simp]: "y. y  A 
         (ya. y - {None} = ya - {None}  ya  A)  {ya. xy - {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. xy - {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. xy - {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 . YA. 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 "xA. F x", simp_all)

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

    from this have " x . x  None  x  Inf ` {f ` A |f. YA. f Y  Y}"
      by blast
  
    from this have E:" Inf ` {f ` A |f. YA. f Y  Y} = {None}  False"
      by blast

    have [simp]: "((x{f ` A |f. YA. f Y  Y}. x) = None) = False"
      by (metis (no_types, lifting) E Sup_option_def x. x  None  x  Inf ` {f ` A |f. YA. 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. axa - {None}. y = the a} = f (the ` (xa - {None}))"
        by  (simp add: image_def)
      from this have [simp]: "xa. xa  A  xA. f {y. axa - {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. ax - {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]: "(xA. Some (f {y. xx - {None}. y = the x})) = {Some (f {y. ax - {None}. y = the a}) |x. x  A}"
        by (simp add: Setcompr_eq_image)
      
      have [simp]: "x. (f. x = {y. xA. y = f x}  (YA. f Y  Y))  {Some (f {y. ax - {None}. y = the a}) |x. x  A} = x"
        apply (rule exI [of _ "{Some (f {y. ax - {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. xy - {None}. ya = the x} |y. y  A}. f x)  f {y. xxb - {None}. y = the x}"
          apply (rule INF_lower2 [of "{y. xxb - {None}. y = the x}"])
          by blast+
      }
      from this have [simp]: "(x{the ` (y - {None}) |y. y  A}. f x)  the (YA. Some (f (the ` (Y - {None}))))"
        apply (simp add: Inf_option_def image_def Option.these_def)
        by (rule Inf_greatest, clarsimp)
      have [simp]: "the (YA. Some (f (the ` (Y - {None}))))  Option.these (Inf ` {f ` A |f. YA. 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. YA. 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. YA. 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. yA}))"
      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. YA. f Y  Y})"
    proof (cases " (Inf ` {f ` A |f. YA. 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. YA. f Y  Y)  Inf ` {f ` A |f. YA. 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