--- a/src/HOL/Library/Quickcheck_Types.thy Wed Jul 21 18:11:51 2010 +0200
+++ b/src/HOL/Library/Quickcheck_Types.thy Wed Jul 21 18:11:51 2010 +0200
@@ -252,10 +252,214 @@
instance top :: (lattice) bounded_lattice_top ..
+
+datatype 'a flat_complete_lattice = Value 'a | Bot | Top
+
+instantiation flat_complete_lattice :: (type) order
+begin
+
+definition less_eq_flat_complete_lattice where
+ "x \<le> 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 => \<not> (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 ~= aa" "Value a <= z" "Value aa <= 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 ~= aa" "z <= Value a" "z <= Value aa"
+ shows "z = Bot"
+using assms
+by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
+
+instance proof
+qed (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 proof
+qed (simp add: bot_flat_complete_lattice_def)
+
+end
+
+instantiation flat_complete_lattice :: (type) top
+begin
+
+definition "top = Top"
+
+instance proof
+qed (auto simp add: less_eq_flat_complete_lattice_def top_flat_complete_lattice_def split: flat_complete_lattice.splits)
+
+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 proof
+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)
+
+end
+
+instantiation flat_complete_lattice :: (type) complete_lattice
+begin
+
+definition Sup_flat_complete_lattice
+where
+ "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))"
+
+definition Inf_flat_complete_lattice
+where
+ "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))"
+
+instance
+proof
+ fix x A
+ assume "(x :: 'a flat_complete_lattice) : A"
+ {
+ fix v
+ assume "A - {Top} = {Value v}"
+ from this have "(THE v. A - {Top} = {Value v}) = v"
+ by (auto intro!: the1_equality)
+ moreover
+ from `x : A` `A - {Top} = {Value v}` have "x = Top \<or> x = Value v"
+ by auto
+ ultimately have "Value (THE v. A - {Top} = {Value v}) <= x"
+ by auto
+ }
+ from `x : A` this show "Inf A <= x"
+ unfolding Inf_flat_complete_lattice_def
+ by fastsimp
+next
+ fix z A
+ assume z: "\<And>x. x : A ==> z <= (x :: 'a flat_complete_lattice)"
+ {
+ fix v
+ assume "A - {Top} = {Value v}"
+ moreover
+ from this have "(THE v. A - {Top} = {Value v}) = v"
+ by (auto intro!: the1_equality)
+ moreover
+ note z
+ moreover
+ ultimately have "z <= Value (THE v::'a. A - {Top} = {Value v})"
+ by auto
+ } moreover
+ {
+ assume not_one_value: "A ~= {}" "A ~= {Top}" "~ (EX v::'a. A - {Top} = {Value v})"
+ have "z <= Bot"
+ proof (cases "A - {Top} = {Bot}")
+ case True
+ from this z show ?thesis
+ by auto
+ next
+ case False
+ from not_one_value
+ obtain a1 where a1: "a1 : A - {Top}" by auto
+ from not_one_value False a1
+ obtain a2 where "a2 : A - {Top} \<and> a1 \<noteq> a2"
+ by (cases a1) auto
+ from this 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
+ } moreover
+ note z moreover
+ ultimately show "z <= Inf A"
+ unfolding Inf_flat_complete_lattice_def
+ by auto
+next
+ fix x A
+ assume "(x :: 'a flat_complete_lattice) : A"
+ {
+ fix v
+ assume "A - {Bot} = {Value v}"
+ from this have "(THE v. A - {Bot} = {Value v}) = v"
+ by (auto intro!: the1_equality)
+ moreover
+ from `x : A` `A - {Bot} = {Value v}` have "x = Bot \<or> x = Value v"
+ by auto
+ ultimately have "x <= Value (THE v. A - {Bot} = {Value v})"
+ by auto
+ }
+ from `x : A` this show "x <= Sup A"
+ unfolding Sup_flat_complete_lattice_def
+ by fastsimp
+next
+ fix z A
+ assume z: "\<And>x. x : A ==> x <= (z :: 'a flat_complete_lattice)"
+ {
+ fix v
+ assume "A - {Bot} = {Value v}"
+ moreover
+ from this have "(THE v. A - {Bot} = {Value v}) = v"
+ by (auto intro!: the1_equality)
+ moreover
+ note z
+ moreover
+ ultimately have "Value (THE v::'a. A - {Bot} = {Value v}) <= z"
+ by auto
+ } moreover
+ {
+ assume not_one_value: "A ~= {}" "A ~= {Bot}" "~ (EX v::'a. A - {Bot} = {Value v})"
+ have "Top <= z"
+ proof (cases "A - {Bot} = {Top}")
+ case True
+ from this z show ?thesis
+ by auto
+ next
+ case False
+ from not_one_value
+ obtain a1 where a1: "a1 : A - {Bot}" by auto
+ from not_one_value False a1
+ obtain a2 where "a2 : A - {Bot} \<and> a1 \<noteq> a2"
+ by (cases a1) auto
+ from this 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
+ } moreover
+ note z moreover
+ ultimately show "Sup A <= z"
+ unfolding Sup_flat_complete_lattice_def
+ by auto
+qed
+
+end
+
section {* Quickcheck configuration *}
-quickcheck_params[default_type = ["int", "non_distrib_lattice", "int bot", "int top"]]
+quickcheck_params[default_type = ["int", "non_distrib_lattice", "int bot", "int top", "int flat_complete_lattice"]]
-hide_type non_distrib_lattice bot top
+hide_type non_distrib_lattice flat_complete_lattice bot top
end
\ No newline at end of file