# HG changeset patch # User wenzelm # Date 1434564321 -7200 # Node ID 2127bee2069a358182258a0f36bce0f9fe3c2c10 # Parent 17741c71a731accaca8d1c44c3953a437af3e3b9 tuned proofs; diff -r 17741c71a731 -r 2127bee2069a src/HOL/Library/Lattice_Constructions.thy --- 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 \ 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 \ Bot + | Value v \ + (case y of + Bot \ Bot + | Value v' \ 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 \ y + | Value v \ + (case y of + Bot \ x + | Value v' \ 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 \Values extended by a top element\ + +subsection \Values extended by a top element\ datatype 'a top = Value 'a | Top @@ -119,7 +127,7 @@ 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" +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" @@ -149,33 +157,28 @@ lemma less_top_Value [simp, code]: "Value x < Value y \ 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 \ y + | Value v \ + (case y of + Top \ x + | Value v' \ 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 \ Top + | Value v \ + (case y of + Top \ Top + | Value v' \ 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 \Values extended by a top and a bottom element\ @@ -212,51 +228,61 @@ 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)" +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)" -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 \ y \ Bot + | Value v1 \ y = Top + | Top \ False)" -lemma [simp]: "y <= Top" -unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits) +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" + 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) + 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 \ aa" "z \ Value a" "z \ 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 \ 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)" + "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) +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 = {} \ A = {Bot}) then Bot else (if (\ v. A - {Bot} = {Value v}) then Value (THE v. A - {Bot} = {Value v}) else Top))" + "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))" - + "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 - assume "(x :: 'a flat_complete_lattice) : A" + fix x :: "'a flat_complete_lattice" + fix A + assume "x \ 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 \x : A\ \A - {Top} = {Value v}\ have "x = Top \ x = Value v" + 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" + ultimately have "Value (THE v. A - {Top} = {Value v}) \ x" by auto } - from \x : A\ this show "Inf A <= x" + with \x \ A\ show "Inf A \ x" unfolding Inf_flat_complete_lattice_def by fastforce next - fix z A - assume z: "\x. x : A ==> z <= (x :: 'a flat_complete_lattice)" + fix z :: "'a flat_complete_lattice" + fix A + assume z: "\x. x \ A \ z \ 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 \ 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 \ {}" "A \ {Top}" "\ (\v::'a. A - {Top} = {Value v})" + have "z \ 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 \ A - {Top}" by auto from not_one_value False a1 - obtain a2 where "a2 : A - {Top} \ a1 \ a2" + obtain a2 where "a2 \ A - {Top} \ a1 \ 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 \ 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 \ 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 \x : A\ \A - {Bot} = {Value v}\ have "x = Bot \ x = Value v" + 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})" + ultimately have "x \ Value (THE v. A - {Bot} = {Value v})" by auto } - from \x : A\ this show "x <= Sup A" + with \x \ A\ show "x \ Sup A" unfolding Sup_flat_complete_lattice_def by fastforce next - fix z A - assume z: "\x. x : A ==> x <= (z :: 'a flat_complete_lattice)" + fix z :: "'a flat_complete_lattice" + fix A + assume z: "\x. x \ A \ x \ 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}) \ 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 \ {}" "A \ {Bot}" "\ (\v::'a. A - {Bot} = {Value v})" + have "Top \ 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} \ a1 \ a2" + 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} \ a1 \ 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 \ 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