# HG changeset patch
# User haftmann
# Date 1253523699 -7200
# Node ID 29e4e567b5f48ca1ec1bcaff8c4f7a3ec6a926c4
# Parent  1392578231336fdaf6bb4a4221f290eb3897f1f0
tuned proofs

diff -r 139257823133 -r 29e4e567b5f4 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Sat Sep 19 07:38:11 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Mon Sep 21 11:01:39 2009 +0200
@@ -3649,10 +3649,7 @@
     from setsum_restrict_set[OF fS, of "\<lambda>v. u v *s v" S', symmetric] SS'
     have "setsum (\<lambda>v. ?u v *s v) S = setsum (\<lambda>v. u v *s v) S'"
       unfolding cond_value_iff cond_application_beta
-      apply (simp add: cond_value_iff cong del: if_weak_cong)
-      apply (rule setsum_cong)
-      apply auto
-      done
+      by (simp add: cond_value_iff cong del: if_weak_cong)
     hence "setsum (\<lambda>v. ?u v *s v) S = y" by (metis u)
     hence "y \<in> ?rhs" by auto}
   moreover
diff -r 139257823133 -r 29e4e567b5f4 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Sep 19 07:38:11 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Sep 21 11:01:39 2009 +0200
@@ -99,11 +99,9 @@
 
 lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast
 lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
-  apply (auto simp add: closedin_def)
+  apply (auto simp add: closedin_def Diff_Diff_Int)
   apply (metis openin_subset subset_eq)
-  apply (auto simp add: Diff_Diff_Int)
-  apply (subgoal_tac "topspace U \<inter> S = S")
-  by auto
+  done
 
 lemma openin_closedin:  "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
   by (simp add: openin_closedin_eq)
diff -r 139257823133 -r 29e4e567b5f4 src/HOL/MetisExamples/Message.thy
--- a/src/HOL/MetisExamples/Message.thy	Sat Sep 19 07:38:11 2009 +0200
+++ b/src/HOL/MetisExamples/Message.thy	Mon Sep 21 11:01:39 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MetisTest/Message.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Testing the metis method
@@ -711,17 +710,17 @@
 proof (neg_clausify)
 assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
 have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
-  by (metis analz_synth_Un sup_set_eq sup_set_eq sup_set_eq)
+  by (metis analz_synth_Un)
 have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
-  by (metis 0 sup_set_eq)
+  by (metis 0)
 have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
-  by (metis 1 Un_commute sup_set_eq sup_set_eq)
+  by (metis 1 Un_commute)
 have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
-  by (metis 3 Un_empty_right sup_set_eq)
+  by (metis 3 Un_empty_right)
 have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
-  by (metis 4 Un_empty_right sup_set_eq)
+  by (metis 4 Un_empty_right)
 have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
-  by (metis 5 Un_commute sup_set_eq sup_set_eq)
+  by (metis 5 Un_commute)
 show "False"
   by (metis 2 6)
 qed
diff -r 139257823133 -r 29e4e567b5f4 src/HOL/MetisExamples/set.thy
--- a/src/HOL/MetisExamples/set.thy	Sat Sep 19 07:38:11 2009 +0200
+++ b/src/HOL/MetisExamples/set.thy	Mon Sep 21 11:01:39 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MetisExamples/set.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Testing the metis method
@@ -36,23 +35,23 @@
 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
 have 6: "sup Y Z = X \<or> Y \<subseteq> X"
-  by (metis 0 sup_set_eq)
+  by (metis 0)
 have 7: "sup Y Z = X \<or> Z \<subseteq> X"
-  by (metis 1 sup_set_eq)
+  by (metis 1)
 have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3"
-  by (metis 5 sup_set_eq)
+  by (metis 5)
 have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 2 sup_set_eq)
+  by (metis 2)
 have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 3 sup_set_eq)
+  by (metis 3)
 have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 4 sup_set_eq)
+  by (metis 4)
 have 12: "Z \<subseteq> X"
-  by (metis Un_upper2 sup_set_eq 7)
+  by (metis Un_upper2 7)
 have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
-  by (metis 8 Un_upper2 sup_set_eq)
+  by (metis 8 Un_upper2)
 have 14: "Y \<subseteq> X"
-  by (metis Un_upper1 sup_set_eq 6)
+  by (metis Un_upper1 6)
 have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   by (metis 10 12)
 have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
@@ -66,17 +65,17 @@
 have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X"
   by (metis 16 14)
 have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
-  by (metis 13 Un_upper1 sup_set_eq)
+  by (metis 13 Un_upper1)
 have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
   by (metis equalityI 21)
 have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 22 Un_least sup_set_eq)
+  by (metis 22 Un_least)
 have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X"
   by (metis 23 12)
 have 25: "sup Y Z = X"
   by (metis 24 14)
 have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3"
-  by (metis Un_least sup_set_eq 25)
+  by (metis Un_least 25)
 have 27: "Y \<subseteq> x"
   by (metis 20 25)
 have 28: "Z \<subseteq> x"
@@ -105,31 +104,31 @@
 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
 have 6: "sup Y Z = X \<or> Y \<subseteq> X"
-  by (metis 0 sup_set_eq)
+  by (metis 0)
 have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 2 sup_set_eq)
+  by (metis 2)
 have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 4 sup_set_eq)
+  by (metis 4)
 have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
-  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
+  by (metis 5 Un_upper2)
 have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
+  by (metis 3 Un_upper2)
 have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
-  by (metis 8 Un_upper2 sup_set_eq sup_set_eq)
+  by (metis 8 Un_upper2)
 have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
-  by (metis 10 Un_upper1 sup_set_eq)
+  by (metis 10 Un_upper1)
 have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
-  by (metis 9 Un_upper1 sup_set_eq)
+  by (metis 9 Un_upper1)
 have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis equalityI 13 Un_least sup_set_eq)
+  by (metis equalityI 13 Un_least)
 have 15: "sup Y Z = X"
-  by (metis 14 sup_set_eq 1 sup_set_eq sup_set_eq 6)
+  by (metis 14 1 6)
 have 16: "Y \<subseteq> x"
-  by (metis 7 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq 15)
+  by (metis 7 Un_upper2 Un_upper1 15)
 have 17: "\<not> X \<subseteq> x"
-  by (metis 11 Un_upper1 sup_set_eq 15)
+  by (metis 11 Un_upper1 15)
 have 18: "X \<subseteq> x"
-  by (metis Un_least sup_set_eq 15 12 15 16)
+  by (metis Un_least 15 12 15 16)
 show "False"
   by (metis 18 17)
 qed
@@ -148,23 +147,23 @@
 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
 have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 3 sup_set_eq)
+  by (metis 3)
 have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
-  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
+  by (metis 5 Un_upper2)
 have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 2 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
+  by (metis 2 Un_upper2)
 have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
-  by (metis 6 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq)
+  by (metis 6 Un_upper2 Un_upper1)
 have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
-  by (metis equalityI 7 Un_upper1 sup_set_eq)
+  by (metis equalityI 7 Un_upper1)
 have 11: "sup Y Z = X"
-  by (metis 10 Un_least sup_set_eq sup_set_eq 1 sup_set_eq sup_set_eq 0 sup_set_eq)
+  by (metis 10 Un_least 1 0)
 have 12: "Z \<subseteq> x"
   by (metis 9 11)
 have 13: "X \<subseteq> x"
-  by (metis Un_least sup_set_eq 11 12 8 Un_upper1 sup_set_eq sup_set_eq 11)
+  by (metis Un_least 11 12 8 Un_upper1 11)
 show "False"
-  by (metis 13 4 sup_set_eq Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq 11)
+  by (metis 13 4 Un_upper2 Un_upper1 11)
 qed
 
 (*Example included in TPHOLs paper*)
@@ -183,19 +182,19 @@
 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
 have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 4 sup_set_eq)
+  by (metis 4)
 have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
+  by (metis 3 Un_upper2)
 have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
-  by (metis 7 Un_upper1 sup_set_eq sup_set_eq)
+  by (metis 7 Un_upper1)
 have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis equalityI 5 sup_set_eq Un_upper2 sup_set_eq Un_upper1 sup_set_eq Un_least sup_set_eq)
+  by (metis equalityI 5 Un_upper2 Un_upper1 Un_least)
 have 10: "Y \<subseteq> x"
-  by (metis 2 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
+  by (metis 2 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
 have 11: "X \<subseteq> x"
-  by (metis Un_least sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 8 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 10)
+  by (metis Un_least 9 Un_upper2 1 Un_upper1 0 8 9 Un_upper2 1 Un_upper1 0 10)
 show "False"
-  by (metis 11 6 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
+  by (metis 11 6 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
 qed 
 
 ML {*AtpWrapper.problem_name := "set__equal_union"*}
@@ -238,7 +237,7 @@
 
 lemma (*singleton_example_2:*)
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-by (metis Set.subsetI Union_upper insert_code mem_def set_eq_subset)
+by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
 
 lemma singleton_example_2:
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"