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