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