--- 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}"