# HG changeset patch
# User bulwahn
# Date 1279728711 -7200
# Node ID eda5faaca9e2c4ebc56e7ab4ad073743272fc3f7
# Parent  67ccea8a47616cf73d3202779b287b0473ef22d2
adding a type for flat complete lattice to Quickcheck_Types

diff -r 67ccea8a4761 -r eda5faaca9e2 src/HOL/Library/Quickcheck_Types.thy
--- 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