src/HOL/MetisExamples/set.thy
author nipkow
Wed Jun 24 09:41:14 2009 +0200 (2009-06-24)
changeset 31790 05c92381363c
parent 28592 824f8390aaa2
child 32519 e9644b497e1c
permissions -rw-r--r--
corrected and unified thm names
     1 (*  Title:      HOL/MetisExamples/set.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 
     5 Testing the metis method
     6 *)
     7 
     8 theory set imports Main
     9 
    10 begin
    11 
    12 lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
    13                (S(x,y) | ~S(y,z) | Q(Z,Z))  &
    14                (Q(X,y) | ~Q(y,Z) | S(X,X))" 
    15 by metis
    16 (*??But metis can't prove the single-step version...*)
    17 
    18 
    19 
    20 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
    21 by metis
    22 
    23 declare [[sledgehammer_modulus = 1]]
    24 
    25 
    26 (*multiple versions of this example*)
    27 lemma (*equal_union: *)
    28    "(X = Y \<union> Z) =
    29     (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    30 proof (neg_clausify)
    31 fix x
    32 assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
    33 assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
    34 assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    35 assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    36 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    37 assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
    38 have 6: "sup Y Z = X \<or> Y \<subseteq> X"
    39   by (metis 0 sup_set_eq)
    40 have 7: "sup Y Z = X \<or> Z \<subseteq> X"
    41   by (metis 1 sup_set_eq)
    42 have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3"
    43   by (metis 5 sup_set_eq)
    44 have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
    45   by (metis 2 sup_set_eq)
    46 have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
    47   by (metis 3 sup_set_eq)
    48 have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
    49   by (metis 4 sup_set_eq)
    50 have 12: "Z \<subseteq> X"
    51   by (metis Un_upper2 sup_set_eq 7)
    52 have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
    53   by (metis 8 Un_upper2 sup_set_eq)
    54 have 14: "Y \<subseteq> X"
    55   by (metis Un_upper1 sup_set_eq 6)
    56 have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
    57   by (metis 10 12)
    58 have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
    59   by (metis 9 12)
    60 have 17: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
    61   by (metis 11 12)
    62 have 18: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x"
    63   by (metis 17 14)
    64 have 19: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
    65   by (metis 15 14)
    66 have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X"
    67   by (metis 16 14)
    68 have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
    69   by (metis 13 Un_upper1 sup_set_eq)
    70 have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
    71   by (metis equalityI 21)
    72 have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
    73   by (metis 22 Un_least sup_set_eq)
    74 have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X"
    75   by (metis 23 12)
    76 have 25: "sup Y Z = X"
    77   by (metis 24 14)
    78 have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3"
    79   by (metis Un_least sup_set_eq 25)
    80 have 27: "Y \<subseteq> x"
    81   by (metis 20 25)
    82 have 28: "Z \<subseteq> x"
    83   by (metis 19 25)
    84 have 29: "\<not> X \<subseteq> x"
    85   by (metis 18 25)
    86 have 30: "X \<subseteq> x \<or> \<not> Y \<subseteq> x"
    87   by (metis 26 28)
    88 have 31: "X \<subseteq> x"
    89   by (metis 30 27)
    90 show "False"
    91   by (metis 31 29)
    92 qed
    93 
    94 declare [[sledgehammer_modulus = 2]]
    95 
    96 lemma (*equal_union: *)
    97    "(X = Y \<union> Z) =
    98     (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    99 proof (neg_clausify)
   100 fix x
   101 assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
   102 assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
   103 assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   104 assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   105 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   106 assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
   107 have 6: "sup Y Z = X \<or> Y \<subseteq> X"
   108   by (metis 0 sup_set_eq)
   109 have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   110   by (metis 2 sup_set_eq)
   111 have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   112   by (metis 4 sup_set_eq)
   113 have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
   114   by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
   115 have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   116   by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
   117 have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
   118   by (metis 8 Un_upper2 sup_set_eq sup_set_eq)
   119 have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
   120   by (metis 10 Un_upper1 sup_set_eq)
   121 have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
   122   by (metis 9 Un_upper1 sup_set_eq)
   123 have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
   124   by (metis equalityI 13 Un_least sup_set_eq)
   125 have 15: "sup Y Z = X"
   126   by (metis 14 sup_set_eq 1 sup_set_eq sup_set_eq 6)
   127 have 16: "Y \<subseteq> x"
   128   by (metis 7 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq 15)
   129 have 17: "\<not> X \<subseteq> x"
   130   by (metis 11 Un_upper1 sup_set_eq 15)
   131 have 18: "X \<subseteq> x"
   132   by (metis Un_least sup_set_eq 15 12 15 16)
   133 show "False"
   134   by (metis 18 17)
   135 qed
   136 
   137 declare [[sledgehammer_modulus = 3]]
   138 
   139 lemma (*equal_union: *)
   140    "(X = Y \<union> Z) =
   141     (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
   142 proof (neg_clausify)
   143 fix x
   144 assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
   145 assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
   146 assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   147 assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   148 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   149 assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
   150 have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   151   by (metis 3 sup_set_eq)
   152 have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
   153   by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
   154 have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   155   by (metis 2 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
   156 have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
   157   by (metis 6 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq)
   158 have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
   159   by (metis equalityI 7 Un_upper1 sup_set_eq)
   160 have 11: "sup Y Z = X"
   161   by (metis 10 Un_least sup_set_eq sup_set_eq 1 sup_set_eq sup_set_eq 0 sup_set_eq)
   162 have 12: "Z \<subseteq> x"
   163   by (metis 9 11)
   164 have 13: "X \<subseteq> x"
   165   by (metis Un_least sup_set_eq 11 12 8 Un_upper1 sup_set_eq sup_set_eq 11)
   166 show "False"
   167   by (metis 13 4 sup_set_eq Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq 11)
   168 qed
   169 
   170 (*Example included in TPHOLs paper*)
   171 
   172 declare [[sledgehammer_modulus = 4]]
   173 
   174 lemma (*equal_union: *)
   175    "(X = Y \<union> Z) =
   176     (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
   177 proof (neg_clausify)
   178 fix x
   179 assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
   180 assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
   181 assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   182 assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   183 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   184 assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
   185 have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   186   by (metis 4 sup_set_eq)
   187 have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   188   by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
   189 have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
   190   by (metis 7 Un_upper1 sup_set_eq sup_set_eq)
   191 have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
   192   by (metis equalityI 5 sup_set_eq Un_upper2 sup_set_eq Un_upper1 sup_set_eq Un_least sup_set_eq)
   193 have 10: "Y \<subseteq> x"
   194   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)
   195 have 11: "X \<subseteq> x"
   196   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)
   197 show "False"
   198   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)
   199 qed 
   200 
   201 ML {*AtpWrapper.problem_name := "set__equal_union"*}
   202 lemma (*equal_union: *)
   203    "(X = Y \<union> Z) =
   204     (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" 
   205 (*One shot proof: hand-reduced. Metis can't do the full proof any more.*)
   206 by (metis Un_least Un_upper1 Un_upper2 set_eq_subset)
   207 
   208 
   209 ML {*AtpWrapper.problem_name := "set__equal_inter"*}
   210 lemma "(X = Y \<inter> Z) =
   211     (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
   212 by (metis Int_greatest Int_lower1 Int_lower2 set_eq_subset)
   213 
   214 ML {*AtpWrapper.problem_name := "set__fixedpoint"*}
   215 lemma fixedpoint:
   216     "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
   217 by metis
   218 
   219 lemma (*fixedpoint:*)
   220     "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
   221 proof (neg_clausify)
   222 fix x xa
   223 assume 0: "f (g x) = x"
   224 assume 1: "\<And>y. y = x \<or> f (g y) \<noteq> y"
   225 assume 2: "\<And>x. g (f (xa x)) = xa x \<or> g (f x) \<noteq> x"
   226 assume 3: "\<And>x. g (f x) \<noteq> x \<or> xa x \<noteq> x"
   227 have 4: "\<And>X1. g (f X1) \<noteq> X1 \<or> g x \<noteq> X1"
   228   by (metis 3 1 2)
   229 show "False"
   230   by (metis 4 0)
   231 qed
   232 
   233 ML {*AtpWrapper.problem_name := "set__singleton_example"*}
   234 lemma (*singleton_example_2:*)
   235      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
   236 by (metis Set.subsetI Union_upper insertCI set_eq_subset)
   237   --{*found by SPASS*}
   238 
   239 lemma (*singleton_example_2:*)
   240      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
   241 by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_eq)
   242 
   243 lemma singleton_example_2:
   244      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
   245 proof (neg_clausify)
   246 assume 0: "\<And>x. \<not> S \<subseteq> {x}"
   247 assume 1: "\<And>x. x \<notin> S \<or> \<Union>S \<subseteq> x"
   248 have 2: "\<And>X3. X3 = \<Union>S \<or> \<not> X3 \<subseteq> \<Union>S \<or> X3 \<notin> S"
   249   by (metis set_eq_subset 1)
   250 have 3: "\<And>X3. S \<subseteq> insert (\<Union>S) X3"
   251   by (metis insert_iff Set.subsetI Union_upper 2 Set.subsetI)
   252 show "False"
   253   by (metis 3 0)
   254 qed
   255 
   256 
   257 
   258 text {*
   259   From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
   260   293-314.
   261 *}
   262 
   263 ML {*AtpWrapper.problem_name := "set__Bledsoe_Fung"*}
   264 (*Notes: 1, the numbering doesn't completely agree with the paper. 
   265 2, we must rename set variables to avoid type clashes.*)
   266 lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))"
   267       "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
   268       "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
   269       "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>B. a \<notin> B \<and> b \<in> B \<and> c \<notin> B"
   270       "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
   271       "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
   272       "\<exists>A. a \<notin> A"
   273       "(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m" 
   274 apply (metis atMost_iff)
   275 apply (metis emptyE)
   276 apply (metis insert_iff singletonE)
   277 apply (metis insertCI singletonE zless_le)
   278 apply (metis insert_iff singletonE)
   279 apply (metis insert_iff singletonE)
   280 apply (metis DiffE)
   281 apply (metis pair_in_Id_conv) 
   282 done
   283 
   284 end