# HG changeset patch
# User wenzelm
# Date 1434573022 -7200
# Node ID 5e67a223a141e68b6522a354485b34d5fc23bfd6
# Parent  16993a3f4967e35914855d7f51df0e2e1a5fb0db# Parent  64d27b9f00a0ce73475542de32c6fc535f774d03
merged

diff -r 16993a3f4967 -r 5e67a223a141 src/HOL/Library/Lattice_Constructions.thy
--- a/src/HOL/Library/Lattice_Constructions.thy	Wed Jun 17 22:06:56 2015 +0200
+++ b/src/HOL/Library/Lattice_Constructions.thy	Wed Jun 17 22:30:22 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> b" "Value a \<le> z" "Value b \<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> b" "z \<le> Value a" "z \<le> Value b"
   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,136 +324,163 @@
 
 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 v
-    assume "A - {Top} = {Value v}"
-    from this 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"
-      by auto
-    ultimately have "Value (THE v. A - {Top} = {Value v}) <= x"
-      by auto
-  }
-  from \<open>x : A\<close> this show "Inf A <= 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 x :: "'a flat_complete_lattice"
+  fix A
+  assume "x \<in> A"
   {
     fix v
     assume "A - {Top} = {Value v}"
-    moreover
-    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
-    note z
-    moreover
-    ultimately have "z <= Value (THE v::'a. A - {Top} = {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}) \<le> x"
       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
+  }
+  with \<open>x \<in> A\<close> show "Inf A \<le> x"
+    unfolding Inf_flat_complete_lattice_def
+    by fastforce
+next
+  fix z :: "'a flat_complete_lattice"
+  fix A
+  show "z \<le> Inf A" if z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
+  proof -
+    consider "A = {} \<or> A = {Top}"
+      | "A \<noteq> {}" "A \<noteq> {Top}" "\<exists>v. A - {Top} = {Value v}"
+      | "A \<noteq> {}" "A \<noteq> {Top}" "\<not> (\<exists>v. A - {Top} = {Value v})"
+      by blast
+    then show ?thesis
+    proof cases
+      case 1
+      then have "Inf A = Top"
+        unfolding Inf_flat_complete_lattice_def by auto
+      then show ?thesis by simp
     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
+      case 2
+      then obtain v where v1: "A - {Top} = {Value v}"
+        by auto
+      then have v2: "(THE v. A - {Top} = {Value v}) = v"
+        by (auto intro!: the1_equality)
+      from 2 v2 have Inf: "Inf A = Value v"
+        unfolding Inf_flat_complete_lattice_def by simp
+      from v1 have "Value v \<in> A" by blast
+      then have "z \<le> Value v" by (rule z)
+      with Inf show ?thesis by simp
+    next
+      case 3
+      then have Inf: "Inf A = Bot"
+        unfolding Inf_flat_complete_lattice_def by auto
+      have "z \<le> Bot"
+      proof (cases "A - {Top} = {Bot}")
+        case True
+        then have "Bot \<in> A" by blast
+        then show ?thesis by (rule z)
+      next
+        case False
+        from 3 obtain a1 where a1: "a1 \<in> A - {Top}"
+          by auto
+        from 3 False a1 obtain a2 where "a2 \<in> A - {Top} \<and> a1 \<noteq> a2"
+          by (cases a1) auto
+        with 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
+      with Inf show ?thesis by simp
     qed
-  } moreover
-  note z moreover
-  ultimately show "z <= Inf A"
-    unfolding Inf_flat_complete_lattice_def
-    by auto
+  qed
 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 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
+  fix z :: "'a flat_complete_lattice"
+  fix A
+  show "Sup A \<le> z" if z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
+  proof -
+    consider "A = {} \<or> A = {Bot}"
+      | "A \<noteq> {}" "A \<noteq> {Bot}" "\<exists>v. A - {Bot} = {Value v}"
+      | "A \<noteq> {}" "A \<noteq> {Bot}" "\<not> (\<exists>v. A - {Bot} = {Value v})"
+      by blast
+    then show ?thesis
+    proof cases
+      case 1
+      then have "Sup A = Bot"
+        unfolding Sup_flat_complete_lattice_def by auto
+      then show ?thesis by simp
+    next
+      case 2
+      then obtain v where v1: "A - {Bot} = {Value v}"
         by auto
+      then have v2: "(THE v. A - {Bot} = {Value v}) = v"
+        by (auto intro!: the1_equality)
+      from 2 v2 have Sup: "Sup A = Value v"
+        unfolding Sup_flat_complete_lattice_def by simp
+      from v1 have "Value v \<in> A" by blast
+      then have "Value v \<le> z" by (rule z)
+      with Sup show ?thesis by simp
     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
+      case 3
+      then have Sup: "Sup A = Top"
+        unfolding Sup_flat_complete_lattice_def by auto
+      have "Top \<le> z"
+      proof (cases "A - {Bot} = {Top}")
+        case True
+        then have "Top \<in> A" by blast
+        then show ?thesis by (rule z)
+      next
+        case False
+        from 3 obtain a1 where a1: "a1 \<in> A - {Bot}"
+          by auto
+        from 3 False a1 obtain a2 where "a2 \<in> A - {Bot} \<and> a1 \<noteq> a2"
+          by (cases a1) auto
+        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
+      with Sup show ?thesis by simp
     qed
-  } moreover
-  note z moreover
-  ultimately show "Sup A <= z"
-    unfolding Sup_flat_complete_lattice_def
-    by auto
+  qed
 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
diff -r 16993a3f4967 -r 5e67a223a141 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Wed Jun 17 22:06:56 2015 +0200
+++ b/src/HOL/Library/Ramsey.thy	Wed Jun 17 22:30:22 2015 +0200
@@ -86,7 +86,7 @@
            by(auto simp:clique_def insert_commute)
           moreover have "card(insert v R) = m"
             using \<open>?C\<close> \<open>finite R\<close> \<open>v ~: R\<close> \<open>m\<noteq>0\<close> by simp
-          ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by blast
+          ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by (metis insert_subset)
         } ultimately have "?EX V E m n" using CI by blast
       } moreover
       { assume "r2 \<le> card ?N"
@@ -106,7 +106,7 @@
             by(auto simp:indep_def insert_commute)
           moreover have "card(insert v R) = n"
             using \<open>?I\<close> \<open>finite R\<close> \<open>v ~: R\<close> \<open>n\<noteq>0\<close> by simp
-          ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by blast
+          ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by (metis insert_subset)
         } ultimately have "?EX V E m n" using CI by blast
       } ultimately show "?EX V E m n" by blast
     qed