--- a/src/HOL/Library/Lattice_Constructions.thy Wed Jun 17 18:58:46 2015 +0200
+++ b/src/HOL/Library/Lattice_Constructions.thy Wed Jun 17 20:05:21 2015 +0200
@@ -50,33 +50,28 @@
lemma less_bot_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
by (simp add: less_bot_def)
-instance proof
-qed (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
+instance
+ by default
+ (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
-end
+end
-instance bot :: (order) order proof
-qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
+instance bot :: (order) order
+ by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
-instance bot :: (linorder) linorder proof
-qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
+instance bot :: (linorder) linorder
+ by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
instantiation bot :: (order) bot
begin
-
-definition "bot = Bot"
-
-instance ..
-
+ definition "bot = Bot"
+ instance ..
end
instantiation bot :: (top) top
begin
-
-definition "top = Value top"
-
-instance ..
-
+ definition "top = Value top"
+ instance ..
end
instantiation bot :: (semilattice_inf) semilattice_inf
@@ -84,10 +79,16 @@
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')))"
+ "inf x y =
+ (case x of
+ Bot \<Rightarrow> Bot
+ | Value v \<Rightarrow>
+ (case y of
+ Bot \<Rightarrow> Bot
+ | Value v' \<Rightarrow> Value (inf v v')))"
-instance proof
-qed (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
+instance
+ by default (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
end
@@ -96,17 +97,24 @@
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')))"
+ "sup x y =
+ (case x of
+ Bot \<Rightarrow> y
+ | Value v \<Rightarrow>
+ (case y of
+ Bot \<Rightarrow> x
+ | Value v' \<Rightarrow> Value (sup v v')))"
-instance proof
-qed (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
+instance
+ by default (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)
+ by intro_classes (simp add: bot_bot_def)
-section \<open>Values extended by a top element\<close>
+
+subsection \<open>Values extended by a top element\<close>
datatype 'a top = Value 'a | Top
@@ -119,7 +127,7 @@
definition less_top where
"x < y \<longleftrightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> x < y))"
-lemma less_eq_top_Top [simp]: "x <= Top"
+lemma less_eq_top_Top [simp]: "x \<le> Top"
by (simp add: less_eq_top_def)
lemma less_eq_top_Top_code [code]: "x \<le> Top \<longleftrightarrow> True"
@@ -149,33 +157,28 @@
lemma less_top_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
by (simp add: less_top_def)
-instance proof
-qed (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
+instance
+ by default
+ (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
-end
+end
-instance top :: (order) order proof
-qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
+instance top :: (order) order
+ by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
-instance top :: (linorder) linorder proof
-qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
+instance top :: (linorder) linorder
+ by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
instantiation top :: (order) top
begin
-
-definition "top = Top"
-
-instance ..
-
+ definition "top = Top"
+ instance ..
end
instantiation top :: (bot) bot
begin
-
-definition "bot = Value bot"
-
-instance ..
-
+ definition "bot = Value bot"
+ instance ..
end
instantiation top :: (semilattice_inf) semilattice_inf
@@ -183,10 +186,16 @@
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')))"
+ "inf x y =
+ (case x of
+ Top \<Rightarrow> y
+ | Value v \<Rightarrow>
+ (case y of
+ Top \<Rightarrow> x
+ | Value v' \<Rightarrow> Value (inf v v')))"
-instance proof
-qed (auto simp add: inf_top_def less_eq_top_def split: top.splits)
+instance
+ by default (auto simp add: inf_top_def less_eq_top_def split: top.splits)
end
@@ -195,15 +204,22 @@
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')))"
+ "sup x y =
+ (case x of
+ Top \<Rightarrow> Top
+ | Value v \<Rightarrow>
+ (case y of
+ Top \<Rightarrow> Top
+ | Value v' \<Rightarrow> Value (sup v v')))"
-instance proof
-qed (auto simp add: sup_top_def less_eq_top_def split: top.splits)
+instance
+ by default (auto simp add: sup_top_def less_eq_top_def split: top.splits)
end
instance top :: (lattice) bounded_lattice_top
-by(intro_classes)(simp add: top_top_def)
+ by default (simp add: top_top_def)
+
subsection \<open>Values extended by a top and a bottom element\<close>
@@ -212,51 +228,61 @@
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)"
+definition less_eq_flat_complete_lattice
+where
+ "x \<le> y \<equiv>
+ (case x of
+ Bot \<Rightarrow> True
+ | Value v1 \<Rightarrow>
+ (case y of
+ Bot \<Rightarrow> False
+ | Value v2 \<Rightarrow> v1 = v2
+ | Top \<Rightarrow> True)
+ | Top \<Rightarrow> y = Top)"
-lemma [simp]: "Bot <= y"
-unfolding less_eq_flat_complete_lattice_def by auto
+definition less_flat_complete_lattice
+where
+ "x < y =
+ (case x of
+ Bot \<Rightarrow> y \<noteq> Bot
+ | Value v1 \<Rightarrow> y = Top
+ | Top \<Rightarrow> False)"
-lemma [simp]: "y <= Top"
-unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
+lemma [simp]: "Bot \<le> y"
+ unfolding less_eq_flat_complete_lattice_def by auto
+
+lemma [simp]: "y \<le> 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"
+ assumes "a \<noteq> aa" "Value a \<le> z" "Value aa \<le> z"
shows "z = Top"
-using assms
-by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
+ 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"
+ assumes "a \<noteq> aa" "z \<le> Value a" "z \<le> Value aa"
shows "z = Bot"
-using assms
-by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
+ 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)
+instance
+ by default
+ (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 ..
-
+ definition "bot = Bot"
+ instance ..
end
instantiation flat_complete_lattice :: (type) top
begin
-
-definition "top = Top"
-
-instance ..
-
+ definition "top = Top"
+ instance ..
end
instantiation flat_complete_lattice :: (type) lattice
@@ -264,14 +290,32 @@
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)"
+ "inf x y =
+ (case x of
+ Bot \<Rightarrow> Bot
+ | Value v1 \<Rightarrow>
+ (case y of
+ Bot \<Rightarrow> Bot
+ | Value v2 \<Rightarrow> if v1 = v2 then x else Bot
+ | Top \<Rightarrow> x)
+ | Top \<Rightarrow> 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)"
+ "sup x y =
+ (case x of
+ Bot \<Rightarrow> y
+ | Value v1 \<Rightarrow>
+ (case y of
+ Bot \<Rightarrow> x
+ | Value v2 \<Rightarrow> if v1 = v2 then x else Top
+ | Top \<Rightarrow> Top)
+ | Top \<Rightarrow> 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)
+instance
+ by default
+ (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
@@ -280,60 +324,65 @@
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))"
+ "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))"
-
+ "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 x :: "'a flat_complete_lattice"
+ fix A
+ assume "x \<in> A"
{
fix v
assume "A - {Top} = {Value v}"
- from this have "(THE v. A - {Top} = {Value v}) = v"
+ then have "(THE v. A - {Top} = {Value v}) = v"
by (auto intro!: the1_equality)
moreover
- from \<open>x : A\<close> \<open>A - {Top} = {Value v}\<close> have "x = Top \<or> x = Value v"
+ from \<open>x \<in> A\<close> \<open>A - {Top} = {Value v}\<close> have "x = Top \<or> x = Value v"
by auto
- ultimately have "Value (THE v. A - {Top} = {Value v}) <= x"
+ ultimately have "Value (THE v. A - {Top} = {Value v}) \<le> x"
by auto
}
- from \<open>x : A\<close> this show "Inf A <= x"
+ with \<open>x \<in> A\<close> show "Inf A \<le> x"
unfolding Inf_flat_complete_lattice_def
by fastforce
next
- fix z A
- assume z: "\<And>x. x : A ==> z <= (x :: 'a flat_complete_lattice)"
+ fix z :: "'a flat_complete_lattice"
+ fix A
+ assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
{
fix v
- assume "A - {Top} = {Value v}"
- moreover
- from this have "(THE v. A - {Top} = {Value v}) = v"
+ assume *: "A - {Top} = {Value v}"
+ then 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
+ with * have "z \<le> Value (THE v::'a. A - {Top} = {Value v})"
+ using z by auto
+ }
+ moreover
{
- assume not_one_value: "A ~= {}" "A ~= {Top}" "~ (EX v::'a. A - {Top} = {Value v})"
- have "z <= Bot"
+ assume not_one_value: "A \<noteq> {}" "A \<noteq> {Top}" "\<not> (\<exists>v::'a. A - {Top} = {Value v})"
+ have "z \<le> Bot"
proof (cases "A - {Top} = {Bot}")
case True
- from this z show ?thesis
+ with z show ?thesis
by auto
next
case False
from not_one_value
- obtain a1 where a1: "a1 : A - {Top}" by auto
+ obtain a1 where a1: "a1 \<in> A - {Top}" by auto
from not_one_value False a1
- obtain a2 where "a2 : A - {Top} \<and> a1 \<noteq> a2"
+ obtain a2 where "a2 \<in> A - {Top} \<and> a1 \<noteq> a2"
by (cases a1) auto
- from this a1 z[of "a1"] z[of "a2"] show ?thesis
+ with a1 z[of "a1"] z[of "a2"] show ?thesis
apply (cases a1)
apply auto
apply (cases a2)
@@ -341,75 +390,69 @@
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
+ }
+ ultimately show "z \<le> Inf A"
+ using z unfolding Inf_flat_complete_lattice_def by auto -- slow
next
- fix x A
- assume "(x :: 'a flat_complete_lattice) : A"
+ fix x :: "'a flat_complete_lattice"
+ fix A
+ assume "x \<in> A"
{
fix v
assume "A - {Bot} = {Value v}"
- from this have "(THE v. A - {Bot} = {Value v}) = v"
+ then have "(THE v. A - {Bot} = {Value v}) = v"
by (auto intro!: the1_equality)
moreover
- from \<open>x : A\<close> \<open>A - {Bot} = {Value v}\<close> have "x = Bot \<or> x = Value v"
+ from \<open>x \<in> A\<close> \<open>A - {Bot} = {Value v}\<close> have "x = Bot \<or> x = Value v"
by auto
- ultimately have "x <= Value (THE v. A - {Bot} = {Value v})"
+ ultimately have "x \<le> Value (THE v. A - {Bot} = {Value v})"
by auto
}
- from \<open>x : A\<close> this show "x <= Sup A"
+ with \<open>x \<in> A\<close> show "x \<le> Sup A"
unfolding Sup_flat_complete_lattice_def
by fastforce
next
- fix z A
- assume z: "\<And>x. x : A ==> x <= (z :: 'a flat_complete_lattice)"
+ fix z :: "'a flat_complete_lattice"
+ fix A
+ assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
{
fix v
assume "A - {Bot} = {Value v}"
moreover
- from this have "(THE v. A - {Bot} = {Value v}) = v"
+ then 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
+ ultimately have "Value (THE v::'a. A - {Bot} = {Value v}) \<le> z"
+ using z by auto
+ }
+ moreover
{
- assume not_one_value: "A ~= {}" "A ~= {Bot}" "~ (EX v::'a. A - {Bot} = {Value v})"
- have "Top <= z"
+ assume not_one_value: "A \<noteq> {}" "A \<noteq> {Bot}" "\<not> (\<exists>v::'a. A - {Bot} = {Value v})"
+ have "Top \<le> z"
proof (cases "A - {Bot} = {Top}")
case True
- from this z show ?thesis
+ with 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"
+ from not_one_value obtain a1 where a1: "a1 \<in> A - {Bot}"
+ by auto
+ from not_one_value False a1 obtain a2 where "a2 \<in> A - {Bot} \<and> a1 \<noteq> a2"
by (cases a1) auto
- from this a1 z[of "a1"] z[of "a2"] show ?thesis
+ 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
- } moreover
- note z moreover
- ultimately show "Sup A <= z"
- unfolding Sup_flat_complete_lattice_def
- by auto
+ }
+ ultimately show "Sup A \<le> z"
+ using z unfolding Sup_flat_complete_lattice_def by auto -- slow
next
show "Inf {} = (top :: 'a flat_complete_lattice)"
- by(simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
-next
+ 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)
+ by (simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
qed
end