Theory Option_ord

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

header {* Canonical order on option type *}

theory Option_ord
imports Option Main
begin

notation
  bot ("⊥") and
  top ("\<top>") and
  inf  (infixl "\<sqinter>" 70) and
  sup  (infixl "\<squnion>" 65) and
  Inf  ("\<Sqinter>_" [900] 900) and
  Sup  ("\<Squnion>_" [900] 900)

syntax (xsymbols)
  "_INF1"     :: "pttrns => 'b => 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3\<Sqinter>_∈_./ _)" [0, 0, 10] 10)
  "_SUP1"     :: "pttrns => 'b => 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3\<Squnion>_∈_./ _)" [0, 0, 10] 10)


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 proof
qed (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 proof
qed (auto simp add: less_eq_option_def less_option_def split: option.splits)

instance option :: (linorder) linorder proof
qed (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 proof
qed (simp add: bot_option_def)

end

instantiation option :: (order_top) order_top
begin

definition top_option where
  "\<top> = Some \<top>"

instance proof
qed (simp add: top_option_def less_eq_option_def split: option.split)

end

instance option :: (wellorder) wellorder proof
  fix P :: "'a option => bool" and 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]:
    "!!z. (!!x. z = Some x ==> (P o Some) x) ==> P z"
  proof -
    fix z
    assume "!!x. z = Some x ==> (P o Some) x"
    with `P None` show "P z" by (cases z) simp_all
  qed
  show "P z" proof (cases z rule: P_Some)
    case (Some w)
    show "(P o 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 o Some) v" .
        qed
      qed
      then show ?case by simp
    qed
  qed
qed

instantiation option :: (inf) inf
begin

definition inf_option where
  "x \<sqinter> y = (case x of None => None | Some x => (case y of None => None | Some y => Some (x \<sqinter> y)))"

lemma inf_None_1 [simp, code]:
  "None \<sqinter> y = None"
  by (simp add: inf_option_def)

lemma inf_None_2 [simp, code]:
  "x \<sqinter> None = None"
  by (cases x) (simp_all add: inf_option_def)

lemma inf_Some [simp, code]:
  "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
  by (simp add: inf_option_def)

instance ..

end

instantiation option :: (sup) sup
begin

definition sup_option where
  "x \<squnion> y = (case x of None => y | Some x' => (case y of None => x | Some y => Some (x' \<squnion> y)))"

lemma sup_None_1 [simp, code]:
  "None \<squnion> y = y"
  by (simp add: sup_option_def)

lemma sup_None_2 [simp, code]:
  "x \<squnion> None = x"
  by (cases x) (simp_all add: sup_option_def)

lemma sup_Some [simp, code]:
  "Some x \<squnion> Some y = Some (x \<squnion> y)"
  by (simp add: sup_option_def)

instance ..

end

instantiation option :: (semilattice_inf) semilattice_inf
begin

instance proof
  fix x y z :: "'a option"
  show "x \<sqinter> y ≤ x"
    by - (cases x, simp_all, cases y, simp_all)
  show "x \<sqinter> y ≤ y"
    by - (cases x, simp_all, cases y, simp_all)
  show "x ≤ y ==> x ≤ z ==> x ≤ y \<sqinter> z"
    by - (cases x, simp_all, cases y, simp_all, cases z, simp_all)
qed
  
end

instantiation option :: (semilattice_sup) semilattice_sup
begin

instance proof
  fix x y z :: "'a option"
  show "x ≤ x \<squnion> y"
    by - (cases x, simp_all, cases y, simp_all)
  show "y ≤ x \<squnion> y"
    by - (cases x, simp_all, cases y, simp_all)
  fix x y z :: "'a option"
  show "y ≤ x ==> z ≤ x ==> y \<squnion> z ≤ x"
    by - (cases y, simp_all, cases z, simp_all, cases x, simp_all)
qed

end

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 \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> 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
  "\<Sqinter>A = (if None ∈ A then None else Some (\<Sqinter>Option.these A))"

lemma None_in_Inf [simp]:
  "None ∈ A ==> \<Sqinter>A = None"
  by (simp add: Inf_option_def)

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

lemma empty_Sup [simp]:
  "\<Squnion>{} = None"
  by (simp add: Sup_option_def)

lemma singleton_None_Sup [simp]:
  "\<Squnion>{None} = None"
  by (simp add: Sup_option_def)

instance proof
  fix x :: "'a option" and A
  assume "x ∈ A"
  then show "\<Sqinter>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 ≤ \<Sqinter>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 ≤ \<Squnion>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 "\<Squnion>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 "\<Squnion>Option.these A ≤ y" by (rule Sup_least)
    with Some show ?thesis by (simp add: Sup_option_def)
  qed
next
  show "\<Squnion>{} = (⊥::'a option)"
  by (auto simp: bot_option_def)
next
  show "\<Sqinter>{} = (\<top>::'a option)"
  by (auto simp: top_option_def Inf_option_def)
qed

end

lemma Some_Inf:
  "Some (\<Sqinter>A) = \<Sqinter>(Some ` A)"
  by (auto simp add: Inf_option_def)

lemma Some_Sup:
  "A ≠ {} ==> Some (\<Squnion>A) = \<Squnion>(Some ` A)"
  by (auto simp add: Sup_option_def)

lemma Some_INF:
  "Some (\<Sqinter>x∈A. f x) = (\<Sqinter>x∈A. Some (f x))"
  using Some_Inf [of "f ` A"] by (simp add: comp_def)

lemma Some_SUP:
  "A ≠ {} ==> Some (\<Squnion>x∈A. f x) = (\<Squnion>x∈A. Some (f x))"
  using Some_Sup [of "f ` A"] by (simp add: comp_def)

instantiation option :: (complete_distrib_lattice) complete_distrib_lattice
begin

instance proof
  fix a :: "'a option" and B
  show "a \<squnion> \<Sqinter>B = (\<Sqinter>b∈B. a \<squnion> b)"
  proof (cases a)
    case None
    then show ?thesis by (simp add: INF_def)
  next
    case (Some c)
    show ?thesis
    proof (cases "None ∈ B")
      case True
      then have "Some c = (\<Sqinter>b∈B. Some c \<squnion> b)"
        by (auto intro!: antisym INF_lower2 INF_greatest)
      with True Some show ?thesis by simp
    next
      case False then have B: "{x ∈ B. ∃y. x = Some y} = B" by auto (metis not_Some_eq)
      from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b∈Option.these B. c \<squnion> b)" by simp
      then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x∈Some ` Option.these B. Some c \<squnion> x)"
        by (simp add: Some_INF Some_Inf comp_def)
      with Some B show ?thesis by (simp add: Some_image_these_eq)
    qed
  qed
  show "a \<sqinter> \<Squnion>B = (\<Squnion>b∈B. a \<sqinter> b)"
  proof (cases a)
    case None
    then show ?thesis by (simp add: SUP_def image_constant_conv bot_option_def)
  next
    case (Some c)
    show ?thesis
    proof (cases "B = {} ∨ B = {None}")
      case True
      then show ?thesis by auto
    next
      have B: "B = {x ∈ B. ∃y. x = Some y} ∪ {x ∈ B. x = None}"
        by auto
      then have Sup_B: "\<Squnion>B = \<Squnion>({x ∈ B. ∃y. x = Some y} ∪ {x ∈ B. x = None})"
        and SUP_B: "!!f. (\<Squnion>x ∈ B. f x) = (\<Squnion>x ∈ {x ∈ B. ∃y. x = Some y} ∪ {x ∈ B. x = None}. f x)"
        by simp_all
      have Sup_None: "\<Squnion>{x. x = None ∧ x ∈ B} = None"
        by (simp add: bot_option_def [symmetric])
      have SUP_None: "(\<Squnion>x∈{x. x = None ∧ x ∈ B}. Some c \<sqinter> x) = None"
        by (simp add: bot_option_def [symmetric])
      case False then have "Option.these B ≠ {}" by (simp add: these_not_empty_eq)
      moreover from inf_Sup have "Some c \<sqinter> Some (\<Squnion>Option.these B) = Some (\<Squnion>b∈Option.these B. c \<sqinter> b)"
        by simp
      ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x∈Some ` Option.these B. Some c \<sqinter> x)"
        by (simp add: Some_SUP Some_Sup comp_def)
      with Some show ?thesis
        by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib)
    qed
  qed
qed

end

instantiation option :: (complete_linorder) complete_linorder
begin

instance ..

end


no_notation
  bot ("⊥") and
  top ("\<top>") and
  inf  (infixl "\<sqinter>" 70) and
  sup  (infixl "\<squnion>" 65) and
  Inf  ("\<Sqinter>_" [900] 900) and
  Sup  ("\<Squnion>_" [900] 900)

no_syntax (xsymbols)
  "_INF1"     :: "pttrns => 'b => 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3\<Sqinter>_∈_./ _)" [0, 0, 10] 10)
  "_SUP1"     :: "pttrns => 'b => 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3\<Squnion>_∈_./ _)" [0, 0, 10] 10)

end