bulwahn@37915: (*  Title:      HOL/Library/Quickcheck_Types.thy
bulwahn@37915:     Author:     Lukas Bulwahn
bulwahn@37915:     Copyright   2010 TU Muenchen
bulwahn@37915: *)
bulwahn@37915: 
bulwahn@37915: theory Quickcheck_Types
bulwahn@37915: imports Main
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: text {*
bulwahn@37915: This theory provides some default types for the quickcheck execution.
bulwahn@37915: In most cases, the default type @{typ "int"} meets the sort constraints
bulwahn@37915: of the proposition.
bulwahn@37915: But for the type classes bot and top, the type @{typ "int"} is insufficient.
bulwahn@37915: Hence, we provide other types than @{typ "int"} as further default types.  
bulwahn@37915: *}
bulwahn@37915: 
bulwahn@37915: subsection {* A non-distributive lattice *}
bulwahn@37915: 
bulwahn@37915: datatype non_distrib_lattice = Zero | A | B | C | One
bulwahn@37915: 
bulwahn@37915: instantiation non_distrib_lattice :: order
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: definition less_eq_non_distrib_lattice
bulwahn@37915: where
bulwahn@37915:   "a <= b = (case a of Zero => True | A => (b = A) \<or> (b = One) | B => (b = B) \<or> (b = One) | C => (b = C) \<or> (b = One) | One => (b = One))"
bulwahn@37915: 
bulwahn@37915: definition less_non_distrib_lattice
bulwahn@37915: where
bulwahn@37915:   "a < b = (case a of Zero => (b \<noteq> Zero) | A => (b = One) | B => (b = One) | C => (b = One) | One => False)"
bulwahn@37915: 
bulwahn@37915: instance proof
bulwahn@37915: qed (auto simp add: less_eq_non_distrib_lattice_def less_non_distrib_lattice_def split: non_distrib_lattice.split non_distrib_lattice.split_asm)
bulwahn@37915: 
bulwahn@37915: end
bulwahn@37915: 
bulwahn@37915: instantiation non_distrib_lattice :: lattice
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: 
bulwahn@37915: definition sup_non_distrib_lattice
bulwahn@37915: where
bulwahn@37915:   "sup a b = (if a = b then a else (if a = Zero then b else (if b = Zero then a else One)))"
bulwahn@37915: 
bulwahn@37915: definition inf_non_distrib_lattice
bulwahn@37915: where
bulwahn@37915:   "inf a b = (if a = b then a else (if a = One then b else (if b = One then a else Zero)))"
bulwahn@37915: 
bulwahn@37915: instance proof
bulwahn@37915: qed (auto simp add: inf_non_distrib_lattice_def sup_non_distrib_lattice_def less_eq_non_distrib_lattice_def split: split_if non_distrib_lattice.split non_distrib_lattice.split_asm)
bulwahn@37915: 
bulwahn@37915: end
bulwahn@37915: 
bulwahn@37919: hide_const Zero A B C One
bulwahn@37919: 
bulwahn@37915: subsection {* Values extended by a bottom element *}
bulwahn@37915: 
bulwahn@37915: datatype 'a bot = Value 'a | Bot
bulwahn@37915: 
bulwahn@37915: instantiation bot :: (preorder) preorder
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: definition less_eq_bot where
bulwahn@37915:   "x \<le> y \<longleftrightarrow> (case x of Bot \<Rightarrow> True | Value x \<Rightarrow> (case y of Bot \<Rightarrow> False | Value y \<Rightarrow> x \<le> y))"
bulwahn@37915: 
bulwahn@37915: definition less_bot where
bulwahn@37915:   "x < y \<longleftrightarrow> (case y of Bot \<Rightarrow> False | Value y \<Rightarrow> (case x of Bot \<Rightarrow> True | Value x \<Rightarrow> x < y))"
bulwahn@37915: 
bulwahn@37915: lemma less_eq_bot_Bot [simp]: "Bot \<le> x"
bulwahn@37915:   by (simp add: less_eq_bot_def)
bulwahn@37915: 
bulwahn@37915: lemma less_eq_bot_Bot_code [code]: "Bot \<le> x \<longleftrightarrow> True"
bulwahn@37915:   by simp
bulwahn@37915: 
bulwahn@37915: lemma less_eq_bot_Bot_is_Bot: "x \<le> Bot \<Longrightarrow> x = Bot"
bulwahn@37915:   by (cases x) (simp_all add: less_eq_bot_def)
bulwahn@37915: 
bulwahn@37915: lemma less_eq_bot_Value_Bot [simp, code]: "Value x \<le> Bot \<longleftrightarrow> False"
bulwahn@37915:   by (simp add: less_eq_bot_def)
bulwahn@37915: 
bulwahn@37915: lemma less_eq_bot_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
bulwahn@37915:   by (simp add: less_eq_bot_def)
bulwahn@37915: 
bulwahn@37915: lemma less_bot_Bot [simp, code]: "x < Bot \<longleftrightarrow> False"
bulwahn@37915:   by (simp add: less_bot_def)
bulwahn@37915: 
bulwahn@37915: lemma less_bot_Bot_is_Value: "Bot < x \<Longrightarrow> \<exists>z. x = Value z"
bulwahn@37915:   by (cases x) (simp_all add: less_bot_def)
bulwahn@37915: 
bulwahn@37915: lemma less_bot_Bot_Value [simp]: "Bot < Value x"
bulwahn@37915:   by (simp add: less_bot_def)
bulwahn@37915: 
bulwahn@37915: lemma less_bot_Bot_Value_code [code]: "Bot < Value x \<longleftrightarrow> True"
bulwahn@37915:   by simp
bulwahn@37915: 
bulwahn@37915: lemma less_bot_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
bulwahn@37915:   by (simp add: less_bot_def)
bulwahn@37915: 
bulwahn@37915: instance proof
bulwahn@37915: qed (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
bulwahn@37915: 
bulwahn@37915: end 
bulwahn@37915: 
bulwahn@37915: instance bot :: (order) order proof
bulwahn@37915: qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
bulwahn@37915: 
bulwahn@37915: instance bot :: (linorder) linorder proof
bulwahn@37915: qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
bulwahn@37915: 
haftmann@43815: instantiation bot :: (order) bot
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: definition "bot = Bot"
bulwahn@37915: 
bulwahn@37915: instance proof
bulwahn@37915: qed (simp add: bot_bot_def)
bulwahn@37915: 
bulwahn@37915: end
bulwahn@37915: 
bulwahn@37915: instantiation bot :: (top) top
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: definition "top = Value top"
bulwahn@37915: 
bulwahn@37915: instance proof
bulwahn@37915: qed (simp add: top_bot_def less_eq_bot_def split: bot.split)
bulwahn@37915: 
bulwahn@37915: end
bulwahn@37915: 
bulwahn@37915: instantiation bot :: (semilattice_inf) semilattice_inf
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: definition inf_bot
bulwahn@37915: where
bulwahn@37915:   "inf x y = (case x of Bot => Bot | Value v => (case y of Bot => Bot | Value v' => Value (inf v v')))"
bulwahn@37915: 
bulwahn@37915: instance proof
bulwahn@37915: qed (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
bulwahn@37915: 
bulwahn@37915: end
bulwahn@37915: 
bulwahn@37915: instantiation bot :: (semilattice_sup) semilattice_sup
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: definition sup_bot
bulwahn@37915: where
bulwahn@37915:   "sup x y = (case x of Bot => y | Value v => (case y of Bot => x | Value v' => Value (sup v v')))"
bulwahn@37915: 
bulwahn@37915: instance proof
bulwahn@37915: qed (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
bulwahn@37915: 
bulwahn@37915: end
bulwahn@37915: 
bulwahn@37915: instance bot :: (lattice) bounded_lattice_bot ..
bulwahn@37915: 
bulwahn@37915: section {* Values extended by a top element *}
bulwahn@37915: 
bulwahn@37915: datatype 'a top = Value 'a | Top
bulwahn@37915: 
bulwahn@37915: instantiation top :: (preorder) preorder
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: definition less_eq_top where
bulwahn@37915:   "x \<le> y \<longleftrightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> x \<le> y))"
bulwahn@37915: 
bulwahn@37915: definition less_top where
bulwahn@37915:   "x < y \<longleftrightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> x < y))"
bulwahn@37915: 
bulwahn@37915: lemma less_eq_top_Top [simp]: "x <= Top"
bulwahn@37915:   by (simp add: less_eq_top_def)
bulwahn@37915: 
bulwahn@37915: lemma less_eq_top_Top_code [code]: "x \<le> Top \<longleftrightarrow> True"
bulwahn@37915:   by simp
bulwahn@37915: 
bulwahn@37915: lemma less_eq_top_is_Top: "Top \<le> x \<Longrightarrow> x = Top"
bulwahn@37915:   by (cases x) (simp_all add: less_eq_top_def)
bulwahn@37915: 
bulwahn@37915: lemma less_eq_top_Top_Value [simp, code]: "Top \<le> Value x \<longleftrightarrow> False"
bulwahn@37915:   by (simp add: less_eq_top_def)
bulwahn@37915: 
bulwahn@37915: lemma less_eq_top_Value_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
bulwahn@37915:   by (simp add: less_eq_top_def)
bulwahn@37915: 
bulwahn@37915: lemma less_top_Top [simp, code]: "Top < x \<longleftrightarrow> False"
bulwahn@37915:   by (simp add: less_top_def)
bulwahn@37915: 
bulwahn@37915: lemma less_top_Top_is_Value: "x < Top \<Longrightarrow> \<exists>z. x = Value z"
bulwahn@37915:   by (cases x) (simp_all add: less_top_def)
bulwahn@37915: 
bulwahn@37915: lemma less_top_Value_Top [simp]: "Value x < Top"
bulwahn@37915:   by (simp add: less_top_def)
bulwahn@37915: 
bulwahn@37915: lemma less_top_Value_Top_code [code]: "Value x < Top \<longleftrightarrow> True"
bulwahn@37915:   by simp
bulwahn@37915: 
bulwahn@37915: lemma less_top_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
bulwahn@37915:   by (simp add: less_top_def)
bulwahn@37915: 
bulwahn@37915: instance proof
bulwahn@37915: qed (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
bulwahn@37915: 
bulwahn@37915: end 
bulwahn@37915: 
bulwahn@37915: instance top :: (order) order proof
bulwahn@37915: qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
bulwahn@37915: 
bulwahn@37915: instance top :: (linorder) linorder proof
bulwahn@37915: qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
bulwahn@37915: 
haftmann@43815: instantiation top :: (order) top
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: definition "top = Top"
bulwahn@37915: 
bulwahn@37915: instance proof
bulwahn@37915: qed (simp add: top_top_def)
bulwahn@37915: 
bulwahn@37915: end
bulwahn@37915: 
bulwahn@37915: instantiation top :: (bot) bot
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: definition "bot = Value bot"
bulwahn@37915: 
bulwahn@37915: instance proof
bulwahn@37915: qed (simp add: bot_top_def less_eq_top_def split: top.split)
bulwahn@37915: 
bulwahn@37915: end
bulwahn@37915: 
bulwahn@37915: instantiation top :: (semilattice_inf) semilattice_inf
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: definition inf_top
bulwahn@37915: where
bulwahn@37915:   "inf x y = (case x of Top => y | Value v => (case y of Top => x | Value v' => Value (inf v v')))"
bulwahn@37915: 
bulwahn@37915: instance proof
bulwahn@37915: qed (auto simp add: inf_top_def less_eq_top_def split: top.splits)
bulwahn@37915: 
bulwahn@37915: end
bulwahn@37915: 
bulwahn@37915: instantiation top :: (semilattice_sup) semilattice_sup
bulwahn@37915: begin
bulwahn@37915: 
bulwahn@37915: definition sup_top
bulwahn@37915: where
bulwahn@37915:   "sup x y = (case x of Top => Top | Value v => (case y of Top => Top | Value v' => Value (sup v v')))"
bulwahn@37915: 
bulwahn@37915: instance proof
bulwahn@37915: qed (auto simp add: sup_top_def less_eq_top_def split: top.splits)
bulwahn@37915: 
bulwahn@37915: end
bulwahn@37915: 
bulwahn@37915: instance top :: (lattice) bounded_lattice_top ..
bulwahn@37915: 
bulwahn@37918: 
bulwahn@37918: datatype 'a flat_complete_lattice = Value 'a | Bot | Top
bulwahn@37918: 
bulwahn@37918: instantiation flat_complete_lattice :: (type) order
bulwahn@37918: begin
bulwahn@37918: 
bulwahn@37918: definition less_eq_flat_complete_lattice where
bulwahn@37918:   "x \<le> y == (case x of Bot => True | Value v1 => (case y of Bot => False | Value v2 => (v1 = v2) | Top => True) | Top => (y = Top))"
bulwahn@37918: 
bulwahn@37918: definition less_flat_complete_lattice where
bulwahn@37918:   "x < y = (case x of Bot => \<not> (y = Bot) | Value v1 => (y = Top) | Top => False)"
bulwahn@37918: 
bulwahn@37918: lemma [simp]: "Bot <= y"
bulwahn@37918: unfolding less_eq_flat_complete_lattice_def by auto
bulwahn@37918: 
bulwahn@37918: lemma [simp]: "y <= Top"
bulwahn@37918: unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
bulwahn@37918: 
bulwahn@37918: lemma greater_than_two_values:
bulwahn@37918:   assumes "a ~= aa" "Value a <= z" "Value aa <= z"
bulwahn@37918:   shows "z = Top"
bulwahn@37918: using assms
bulwahn@37918: by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
bulwahn@37918: 
bulwahn@37918: lemma lesser_than_two_values:
bulwahn@37918:   assumes "a ~= aa" "z <= Value a" "z <= Value aa"
bulwahn@37918:   shows "z = Bot"
bulwahn@37918: using assms
bulwahn@37918: by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
bulwahn@37918: 
bulwahn@37918: instance proof
bulwahn@37918: qed (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def split: flat_complete_lattice.splits)
bulwahn@37918: 
bulwahn@37918: end
bulwahn@37918: 
bulwahn@37918: instantiation flat_complete_lattice :: (type) bot
bulwahn@37918: begin
bulwahn@37918: 
bulwahn@37918: definition "bot = Bot"
bulwahn@37918: 
bulwahn@37918: instance proof
bulwahn@37918: qed (simp add: bot_flat_complete_lattice_def)
bulwahn@37918: 
bulwahn@37918: end
bulwahn@37918: 
bulwahn@37918: instantiation flat_complete_lattice :: (type) top
bulwahn@37918: begin
bulwahn@37918: 
bulwahn@37918: definition "top = Top"
bulwahn@37918: 
bulwahn@37918: instance proof
bulwahn@37918: qed (auto simp add: less_eq_flat_complete_lattice_def top_flat_complete_lattice_def split: flat_complete_lattice.splits)
bulwahn@37918: 
bulwahn@37918: end
bulwahn@37918: 
bulwahn@37918: instantiation flat_complete_lattice :: (type) lattice
bulwahn@37918: begin
bulwahn@37918: 
bulwahn@37918: definition inf_flat_complete_lattice
bulwahn@37918: where
bulwahn@37918:   "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)"
bulwahn@37918: 
bulwahn@37918: definition sup_flat_complete_lattice
bulwahn@37918: where
bulwahn@37918:   "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)"
bulwahn@37918: 
bulwahn@37918: instance proof
bulwahn@37918: qed (auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)
bulwahn@37918: 
bulwahn@37918: end
bulwahn@37918: 
bulwahn@37918: instantiation flat_complete_lattice :: (type) complete_lattice
bulwahn@37918: begin
bulwahn@37918: 
bulwahn@37918: definition Sup_flat_complete_lattice
bulwahn@37918: where
bulwahn@37918:   "Sup A = (if (A = {} \<or> A = {Bot}) then Bot else (if (\<exists> v. A - {Bot} = {Value v}) then Value (THE v. A - {Bot} = {Value v}) else Top))"
bulwahn@37918: 
bulwahn@37918: definition Inf_flat_complete_lattice
bulwahn@37918: where
bulwahn@37918:   "Inf A = (if (A = {} \<or> A = {Top}) then Top else (if (\<exists> v. A - {Top} = {Value v}) then Value (THE v. A - {Top} = {Value v}) else Bot))"
bulwahn@37918:  
bulwahn@37918: instance
bulwahn@37918: proof
bulwahn@37918:   fix x A
bulwahn@37918:   assume "(x :: 'a flat_complete_lattice) : A"
bulwahn@37918:   {
bulwahn@37918:     fix v
bulwahn@37918:     assume "A - {Top} = {Value v}"
bulwahn@37918:     from this have "(THE v. A - {Top} = {Value v}) = v"
bulwahn@37918:       by (auto intro!: the1_equality)
bulwahn@37918:     moreover
bulwahn@37918:     from `x : A` `A - {Top} = {Value v}` have "x = Top \<or> x = Value v"
bulwahn@37918:       by auto
bulwahn@37918:     ultimately have "Value (THE v. A - {Top} = {Value v}) <= x"
bulwahn@37918:       by auto
bulwahn@37918:   }
bulwahn@37918:   from `x : A` this show "Inf A <= x"
bulwahn@37918:     unfolding Inf_flat_complete_lattice_def
nipkow@44890:     by fastforce
bulwahn@37918: next
bulwahn@37918:   fix z A
bulwahn@37918:   assume z: "\<And>x. x : A ==> z <= (x :: 'a flat_complete_lattice)"
bulwahn@37918:   {
bulwahn@37918:     fix v
bulwahn@37918:     assume "A - {Top} = {Value v}"
bulwahn@37918:     moreover
bulwahn@37918:     from this have "(THE v. A - {Top} = {Value v}) = v"
bulwahn@37918:       by (auto intro!: the1_equality)
bulwahn@37918:     moreover
bulwahn@37918:     note z
bulwahn@37918:     moreover
bulwahn@37918:     ultimately have "z <= Value (THE v::'a. A - {Top} = {Value v})"
bulwahn@37918:       by auto
bulwahn@37918:   } moreover
bulwahn@37918:   {
bulwahn@37918:     assume not_one_value: "A ~= {}" "A ~= {Top}" "~ (EX v::'a. A - {Top} = {Value v})"
bulwahn@37918:     have "z <= Bot"
bulwahn@37918:     proof (cases "A - {Top} = {Bot}")
bulwahn@37918:       case True
bulwahn@37918:       from this z show ?thesis
bulwahn@37918:         by auto
bulwahn@37918:     next
bulwahn@37918:       case False
bulwahn@37918:       from not_one_value
bulwahn@37918:       obtain a1 where a1: "a1 : A - {Top}" by auto
bulwahn@37918:       from not_one_value False a1
bulwahn@37918:       obtain a2 where "a2 : A - {Top} \<and> a1 \<noteq> a2"
bulwahn@37918:         by (cases a1) auto
bulwahn@37918:       from this a1 z[of "a1"] z[of "a2"] show ?thesis
bulwahn@37918:         apply (cases a1)
bulwahn@37918:         apply auto
bulwahn@37918:         apply (cases a2)
bulwahn@37918:         apply auto
bulwahn@37918:         apply (auto dest!: lesser_than_two_values)
bulwahn@37918:         done
bulwahn@37918:     qed
bulwahn@37918:   } moreover
bulwahn@37918:   note z moreover
bulwahn@37918:   ultimately show "z <= Inf A"
bulwahn@37918:     unfolding Inf_flat_complete_lattice_def
bulwahn@37918:     by auto
bulwahn@37918: next
bulwahn@37918:   fix x A
bulwahn@37918:   assume "(x :: 'a flat_complete_lattice) : A"
bulwahn@37918:   {
bulwahn@37918:     fix v
bulwahn@37918:     assume "A - {Bot} = {Value v}"
bulwahn@37918:     from this have "(THE v. A - {Bot} = {Value v}) = v"
bulwahn@37918:       by (auto intro!: the1_equality)
bulwahn@37918:     moreover
bulwahn@37918:     from `x : A` `A - {Bot} = {Value v}` have "x = Bot \<or> x = Value v"
bulwahn@37918:       by auto
bulwahn@37918:     ultimately have "x <= Value (THE v. A - {Bot} = {Value v})"
bulwahn@37918:       by auto
bulwahn@37918:   }
bulwahn@37918:   from `x : A` this show "x <= Sup A"
bulwahn@37918:     unfolding Sup_flat_complete_lattice_def
nipkow@44890:     by fastforce
bulwahn@37918: next
bulwahn@37918:   fix z A
bulwahn@37918:   assume z: "\<And>x. x : A ==> x <= (z :: 'a flat_complete_lattice)"
bulwahn@37918:   {
bulwahn@37918:     fix v
bulwahn@37918:     assume "A - {Bot} = {Value v}"
bulwahn@37918:     moreover
bulwahn@37918:     from this have "(THE v. A - {Bot} = {Value v}) = v"
bulwahn@37918:       by (auto intro!: the1_equality)
bulwahn@37918:     moreover
bulwahn@37918:     note z
bulwahn@37918:     moreover
bulwahn@37918:     ultimately have "Value (THE v::'a. A - {Bot} = {Value v}) <= z"
bulwahn@37918:       by auto
bulwahn@37918:   } moreover
bulwahn@37918:   {
bulwahn@37918:     assume not_one_value: "A ~= {}" "A ~= {Bot}" "~ (EX v::'a. A - {Bot} = {Value v})"
bulwahn@37918:     have "Top <= z"
bulwahn@37918:     proof (cases "A - {Bot} = {Top}")
bulwahn@37918:       case True
bulwahn@37918:       from this z show ?thesis
bulwahn@37918:         by auto
bulwahn@37918:     next
bulwahn@37918:       case False
bulwahn@37918:       from not_one_value
bulwahn@37918:       obtain a1 where a1: "a1 : A - {Bot}" by auto
bulwahn@37918:       from not_one_value False a1
bulwahn@37918:       obtain a2 where "a2 : A - {Bot} \<and> a1 \<noteq> a2"
bulwahn@37918:         by (cases a1) auto
bulwahn@37918:       from this a1 z[of "a1"] z[of "a2"] show ?thesis
bulwahn@37918:         apply (cases a1)
bulwahn@37918:         apply auto
bulwahn@37918:         apply (cases a2)
bulwahn@37918:         apply (auto dest!: greater_than_two_values)
bulwahn@37918:         done
bulwahn@37918:     qed
bulwahn@37918:   } moreover
bulwahn@37918:   note z moreover
bulwahn@37918:   ultimately show "Sup A <= z"
bulwahn@37918:     unfolding Sup_flat_complete_lattice_def
bulwahn@37918:     by auto
bulwahn@37918: qed
bulwahn@37918: 
bulwahn@37918: end
bulwahn@37918: 
bulwahn@37915: section {* Quickcheck configuration *}
bulwahn@37915: 
bulwahn@40654: quickcheck_params[finite_types = false, default_type = ["int", "non_distrib_lattice", "int bot", "int top", "int flat_complete_lattice"]]
bulwahn@37915: 
bulwahn@37918: hide_type non_distrib_lattice flat_complete_lattice bot top
bulwahn@37915: 
bulwahn@37915: end