Theory Lattice_Constructions

(*  Title:      HOL/Library/Lattice_Constructions.thy
    Author:     Lukas Bulwahn
    Copyright   2010 TU Muenchen
*)

section ‹Values extended by a bottom element›

theory Lattice_Constructions
imports Main
begin

datatype 'a bot = Value 'a | Bot

instantiation bot :: (preorder) preorder
begin

definition less_eq_bot where
  "x  y  (case x of Bot  True | Value x  (case y of Bot  False | Value y  x  y))"

definition less_bot where
  "x < y  (case y of Bot  False | Value y  (case x of Bot  True | Value x  x < y))"

lemma less_eq_bot_Bot [simp]: "Bot  x"
  by (simp add: less_eq_bot_def)

lemma less_eq_bot_Bot_code [code]: "Bot  x  True"
  by simp

lemma less_eq_bot_Bot_is_Bot: "x  Bot  x = Bot"
  by (cases x) (simp_all add: less_eq_bot_def)

lemma less_eq_bot_Value_Bot [simp, code]: "Value x  Bot  False"
  by (simp add: less_eq_bot_def)

lemma less_eq_bot_Value [simp, code]: "Value x  Value y  x  y"
  by (simp add: less_eq_bot_def)

lemma less_bot_Bot [simp, code]: "x < Bot  False"
  by (simp add: less_bot_def)

lemma less_bot_Bot_is_Value: "Bot < x  z. x = Value z"
  by (cases x) (simp_all add: less_bot_def)

lemma less_bot_Bot_Value [simp]: "Bot < Value x"
  by (simp add: less_bot_def)

lemma less_bot_Bot_Value_code [code]: "Bot < Value x  True"
  by simp

lemma less_bot_Value [simp, code]: "Value x < Value y  x < y"
  by (simp add: less_bot_def)

instance
  by standard
    (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)

end

instance bot :: (order) order
  by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)

instance bot :: (linorder) linorder
  by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)

instantiation bot :: (order) bot
begin
  definition "bot = Bot"
  instance ..
end

instantiation bot :: (top) top
begin
  definition "top = Value top"
  instance ..
end

instantiation bot :: (semilattice_inf) semilattice_inf
begin

definition inf_bot
where
  "inf x y =
    (case x of
      Bot  Bot
    | Value v 
        (case y of
          Bot  Bot
        | Value v'  Value (inf v v')))"

instance
  by standard (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)

end

instantiation bot :: (semilattice_sup) semilattice_sup
begin

definition sup_bot
where
  "sup x y =
    (case x of
      Bot  y
    | Value v 
        (case y of
          Bot  x
        | Value v'  Value (sup v v')))"

instance
  by standard (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)

end

instance bot :: (lattice) bounded_lattice_bot
  by intro_classes (simp add: bot_bot_def)


subsection ‹Values extended by a top element›

datatype 'a top = Value 'a | Top

instantiation top :: (preorder) preorder
begin

definition less_eq_top where
  "x  y  (case y of Top  True | Value y  (case x of Top  False | Value x  x  y))"

definition less_top where
  "x < y  (case x of Top  False | Value x  (case y of Top  True | Value y  x < y))"

lemma less_eq_top_Top [simp]: "x  Top"
  by (simp add: less_eq_top_def)

lemma less_eq_top_Top_code [code]: "x  Top  True"
  by simp

lemma less_eq_top_is_Top: "Top  x  x = Top"
  by (cases x) (simp_all add: less_eq_top_def)

lemma less_eq_top_Top_Value [simp, code]: "Top  Value x  False"
  by (simp add: less_eq_top_def)

lemma less_eq_top_Value_Value [simp, code]: "Value x  Value y  x  y"
  by (simp add: less_eq_top_def)

lemma less_top_Top [simp, code]: "Top < x  False"
  by (simp add: less_top_def)

lemma less_top_Top_is_Value: "x < Top  z. x = Value z"
  by (cases x) (simp_all add: less_top_def)

lemma less_top_Value_Top [simp]: "Value x < Top"
  by (simp add: less_top_def)

lemma less_top_Value_Top_code [code]: "Value x < Top  True"
  by simp

lemma less_top_Value [simp, code]: "Value x < Value y  x < y"
  by (simp add: less_top_def)

instance
  by standard
    (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)

end

instance top :: (order) order
  by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)

instance top :: (linorder) linorder
  by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)

instantiation top :: (order) top
begin
  definition "top = Top"
  instance ..
end

instantiation top :: (bot) bot
begin
  definition "bot = Value bot"
  instance ..
end

instantiation top :: (semilattice_inf) semilattice_inf
begin

definition inf_top
where
  "inf x y =
    (case x of
      Top  y
    | Value v 
        (case y of
          Top  x
        | Value v'  Value (inf v v')))"

instance
  by standard (auto simp add: inf_top_def less_eq_top_def split: top.splits)

end

instantiation top :: (semilattice_sup) semilattice_sup
begin

definition sup_top
where
  "sup x y =
    (case x of
      Top  Top
    | Value v 
        (case y of
          Top  Top
        | Value v'  Value (sup v v')))"

instance
  by standard (auto simp add: sup_top_def less_eq_top_def split: top.splits)

end

instance top :: (lattice) bounded_lattice_top
  by standard (simp add: top_top_def)


subsection ‹Values extended by a top and a bottom element›

datatype 'a flat_complete_lattice = Value 'a | Bot | Top

instantiation flat_complete_lattice :: (type) order
begin

definition less_eq_flat_complete_lattice
where
  "x  y 
    (case x of
      Bot  True
    | Value v1 
        (case y of
          Bot  False
        | Value v2  v1 = v2
        | Top  True)
    | Top  y = Top)"

definition less_flat_complete_lattice
where
  "x < y =
    (case x of
      Bot  y  Bot
    | Value v1  y = Top
    | Top  False)"

lemma [simp]: "Bot  y"
  unfolding less_eq_flat_complete_lattice_def by auto

lemma [simp]: "y  Top"
  unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)

lemma greater_than_two_values:
  assumes "a  b" "Value a  z" "Value b  z"
  shows "z = Top"
  using assms
  by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)

lemma lesser_than_two_values:
  assumes "a  b" "z  Value a" "z  Value b"
  shows "z = Bot"
  using assms
  by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)

instance
  by standard
    (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def
      split: flat_complete_lattice.splits)

end

instantiation flat_complete_lattice :: (type) bot
begin
  definition "bot = Bot"
  instance ..
end

instantiation flat_complete_lattice :: (type) top
begin
  definition "top = Top"
  instance ..
end

instantiation flat_complete_lattice :: (type) lattice
begin

definition inf_flat_complete_lattice
where
  "inf x y =
    (case x of
      Bot  Bot
    | Value v1 
        (case y of
          Bot  Bot
        | Value v2  if v1 = v2 then x else Bot
        | Top  x)
    | Top  y)"

definition sup_flat_complete_lattice
where
  "sup x y =
    (case x of
      Bot  y
    | Value v1 
        (case y of
          Bot  x
        | Value v2  if v1 = v2 then x else Top
        | Top  Top)
    | Top  Top)"

instance
  by standard
    (auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def
      less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)

end

instantiation flat_complete_lattice :: (type) complete_lattice
begin

definition Sup_flat_complete_lattice
where
  "Sup A =
    (if A = {}  A = {Bot} then Bot
     else if v. A - {Bot} = {Value v} then Value (THE v. A - {Bot} = {Value v})
     else Top)"

definition Inf_flat_complete_lattice
where
  "Inf A =
    (if A = {}  A = {Top} then Top
     else if v. A - {Top} = {Value v} then Value (THE v. A - {Top} = {Value v})
     else Bot)"

instance
proof
  fix x :: "'a flat_complete_lattice"
  fix A
  assume "x  A"
  {
    fix v
    assume "A - {Top} = {Value v}"
    then have "(THE v. A - {Top} = {Value v}) = v"
      by (auto intro!: the1_equality)
    moreover
    from x  A A - {Top} = {Value v} have "x = Top  x = Value v"
      by auto
    ultimately have "Value (THE v. A - {Top} = {Value v})  x"
      by auto
  }
  with x  A show "Inf A  x"
    unfolding Inf_flat_complete_lattice_def
    by fastforce
next
  fix z :: "'a flat_complete_lattice"
  fix A
  show "z  Inf A" if z: "x. x  A  z  x"
  proof -
    consider "A = {}  A = {Top}"
      | "A  {}" "A  {Top}" "v. A - {Top} = {Value v}"
      | "A  {}" "A  {Top}" "¬ (v. A - {Top} = {Value v})"
      by blast
    then show ?thesis
    proof cases
      case 1
      then have "Inf A = Top"
        unfolding Inf_flat_complete_lattice_def by auto
      then show ?thesis by simp
    next
      case 2
      then obtain v where v1: "A - {Top} = {Value v}"
        by auto
      then have v2: "(THE v. A - {Top} = {Value v}) = v"
        by (auto intro!: the1_equality)
      from 2 v2 have Inf: "Inf A = Value v"
        unfolding Inf_flat_complete_lattice_def by simp
      from v1 have "Value v  A" by blast
      then have "z  Value v" by (rule z)
      with Inf show ?thesis by simp
    next
      case 3
      then have Inf: "Inf A = Bot"
        unfolding Inf_flat_complete_lattice_def by auto
      have "z  Bot"
      proof (cases "A - {Top} = {Bot}")
        case True
        then have "Bot  A" by blast
        then show ?thesis by (rule z)
      next
        case False
        from 3 obtain a1 where a1: "a1  A - {Top}"
          by auto
        from 3 False a1 obtain a2 where "a2  A - {Top}  a1  a2"
          by (cases a1) auto
        with a1 z[of "a1"] z[of "a2"] show ?thesis
          apply (cases a1)
          apply auto
          apply (cases a2)
          apply auto
          apply (auto dest!: lesser_than_two_values)
          done
      qed
      with Inf show ?thesis by simp
    qed
  qed
next
  fix x :: "'a flat_complete_lattice"
  fix A
  assume "x  A"
  {
    fix v
    assume "A - {Bot} = {Value v}"
    then have "(THE v. A - {Bot} = {Value v}) = v"
      by (auto intro!: the1_equality)
    moreover
    from x  A A - {Bot} = {Value v} have "x = Bot  x = Value v"
      by auto
    ultimately have "x  Value (THE v. A - {Bot} = {Value v})"
      by auto
  }
  with x  A show "x  Sup A"
    unfolding Sup_flat_complete_lattice_def
    by fastforce
next
  fix z :: "'a flat_complete_lattice"
  fix A
  show "Sup A  z" if z: "x. x  A  x  z"
  proof -
    consider "A = {}  A = {Bot}"
      | "A  {}" "A  {Bot}" "v. A - {Bot} = {Value v}"
      | "A  {}" "A  {Bot}" "¬ (v. A - {Bot} = {Value v})"
      by blast
    then show ?thesis
    proof cases
      case 1
      then have "Sup A = Bot"
        unfolding Sup_flat_complete_lattice_def by auto
      then show ?thesis by simp
    next
      case 2
      then obtain v where v1: "A - {Bot} = {Value v}"
        by auto
      then have v2: "(THE v. A - {Bot} = {Value v}) = v"
        by (auto intro!: the1_equality)
      from 2 v2 have Sup: "Sup A = Value v"
        unfolding Sup_flat_complete_lattice_def by simp
      from v1 have "Value v  A" by blast
      then have "Value v  z" by (rule z)
      with Sup show ?thesis by simp
    next
      case 3
      then have Sup: "Sup A = Top"
        unfolding Sup_flat_complete_lattice_def by auto
      have "Top  z"
      proof (cases "A - {Bot} = {Top}")
        case True
        then have "Top  A" by blast
        then show ?thesis by (rule z)
      next
        case False
        from 3 obtain a1 where a1: "a1  A - {Bot}"
          by auto
        from 3 False a1 obtain a2 where "a2  A - {Bot}  a1  a2"
          by (cases a1) auto
        with a1 z[of "a1"] z[of "a2"] show ?thesis
          apply (cases a1)
          apply auto
          apply (cases a2)
          apply (auto dest!: greater_than_two_values)
          done
      qed
      with Sup show ?thesis by simp
    qed
  qed
next
  show "Inf {} = (top :: 'a flat_complete_lattice)"
    by (simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
  show "Sup {} = (bot :: 'a flat_complete_lattice)"
    by (simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
qed

end

end