src/HOL/ex/set.thy
changeset 13107 8743cc847224
parent 13058 ad6106d7b4bb
child 14353 79f9fbef9106
     1.1 --- a/src/HOL/ex/set.thy	Tue May 07 14:27:07 2002 +0200
     1.2 +++ b/src/HOL/ex/set.thy	Tue May 07 14:27:39 2002 +0200
     1.3 @@ -2,176 +2,190 @@
     1.4      ID:         $Id$
     1.5      Author:     Tobias Nipkow and Lawrence C Paulson
     1.6      Copyright   1991  University of Cambridge
     1.7 +*)
     1.8  
     1.9 -Set Theory examples: Cantor's Theorem, Schroeder-Berstein Theorem, etc.
    1.10 -*)
    1.11 +header {* Set Theory examples: Cantor's Theorem, Schröder-Berstein Theorem, etc. *}
    1.12  
    1.13  theory set = Main:
    1.14  
    1.15 -text{*These two are cited in Benzmueller and Kohlhase's system description 
    1.16 -of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not prove.*}
    1.17 +text{*
    1.18 +  These two are cited in Benzmueller and Kohlhase's system description
    1.19 +  of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not
    1.20 +  prove.
    1.21 +*}
    1.22  
    1.23 -lemma "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"
    1.24 -by blast
    1.25 -
    1.26 -lemma "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"
    1.27 -by blast
    1.28 +lemma "(X = Y \<union> Z) =
    1.29 +    (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    1.30 +  by blast
    1.31  
    1.32 -text{*trivial example of term synthesis: apparently hard for some provers!*}
    1.33 -lemma "a ~= b ==> a:?X & b ~: ?X"
    1.34 -by blast
    1.35 +lemma "(X = Y \<inter> Z) =
    1.36 +    (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
    1.37 +  by blast
    1.38  
    1.39 -(** Examples for the Blast_tac paper **)
    1.40 +text {*
    1.41 +  Trivial example of term synthesis: apparently hard for some provers!
    1.42 +*}
    1.43  
    1.44 -text{*Union-image, called Un_Union_image on equalities.ML*}
    1.45 -lemma "(UN x:C. f(x) Un g(x)) = Union(f`C)  Un  Union(g`C)"
    1.46 -by blast
    1.47 +lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
    1.48 +  by blast
    1.49 +
    1.50 +
    1.51 +subsection {* Examples for the @{text blast} paper *}
    1.52  
    1.53 -text{*Inter-image, called Int_Inter_image on equalities.ML*}
    1.54 -lemma "(INT x:C. f(x) Int g(x)) = Inter(f`C) Int Inter(g`C)"
    1.55 -by blast
    1.56 +lemma "(\<Union>x \<in> C. f x \<union> g x) = \<Union>(f ` C)  \<union>  \<Union>(g ` C)"
    1.57 +  -- {* Union-image, called @{text Un_Union_image} in Main HOL *}
    1.58 +  by blast
    1.59  
    1.60 -text{*Singleton I.  Nice demonstration of blast_tac--and its limitations.
    1.61 -For some unfathomable reason, UNIV_I increases the search space greatly*}
    1.62 -lemma "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"
    1.63 -by (blast del: UNIV_I)
    1.64 +lemma "(\<Inter>x \<in> C. f x \<inter> g x) = \<Inter>(f ` C) \<inter> \<Inter>(g ` C)"
    1.65 +  -- {* Inter-image, called @{text Int_Inter_image} in Main HOL *}
    1.66 +  by blast
    1.67  
    1.68 -text{*Singleton II.  variant of the benchmark above*}
    1.69 -lemma "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"
    1.70 -by (blast del: UNIV_I)
    1.71 -
    1.72 -text{* A unique fixpoint theorem --- fast/best/meson all fail *}
    1.73 +lemma "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    1.74 +  -- {* Singleton I.  Nice demonstration of @{text blast}--and its limitations. *}
    1.75 +  -- {* For some unfathomable reason, @{text UNIV_I} increases the search space greatly. *}
    1.76 +  by (blast del: UNIV_I)
    1.77  
    1.78 -lemma "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y"
    1.79 -apply (erule ex1E, rule ex1I, erule arg_cong)
    1.80 -apply (rule subst, assumption, erule allE, rule arg_cong, erule mp) 
    1.81 -apply (erule arg_cong) 
    1.82 -done
    1.83 +lemma "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    1.84 +  -- {*Singleton II.  Variant of the benchmark above. *}
    1.85 +  by (blast del: UNIV_I)
    1.86 +
    1.87 +lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
    1.88 +  -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}
    1.89 +  apply (erule ex1E, rule ex1I, erule arg_cong)
    1.90 +  apply (rule subst, assumption, erule allE, rule arg_cong, erule mp)
    1.91 +  apply (erule arg_cong)
    1.92 +  done
    1.93  
    1.94  
    1.95  
    1.96 -text{* Cantor's Theorem: There is no surjection from a set to its powerset. *}
    1.97 +subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *}
    1.98  
    1.99 -text{*requires best-first search because it is undirectional*}
   1.100 -lemma cantor1: "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)"
   1.101 -by best
   1.102 +lemma cantor1: "\<not> (\<exists>f:: 'a \<Rightarrow> 'a set. \<forall>S. \<exists>x. f x = S)"
   1.103 +  -- {* Requires best-first search because it is undirectional. *}
   1.104 +  by best
   1.105  
   1.106 -text{*This form displays the diagonal term*}
   1.107 -lemma "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)"
   1.108 -by best
   1.109 +lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
   1.110 +  -- {*This form displays the diagonal term. *}
   1.111 +  by best
   1.112  
   1.113 -text{*This form exploits the set constructs*}
   1.114 -lemma "?S ~: range(f :: 'a=>'a set)"
   1.115 -by (rule notI, erule rangeE, best)  
   1.116 +lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
   1.117 +  -- {* This form exploits the set constructs. *}
   1.118 +  by (rule notI, erule rangeE, best)
   1.119  
   1.120 -text{*Or just this!*}
   1.121 -lemma "?S ~: range(f :: 'a=>'a set)"
   1.122 -by best
   1.123 +lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
   1.124 +  -- {* Or just this! *}
   1.125 +  by best
   1.126 +
   1.127  
   1.128 -text{* The Schroeder-Berstein Theorem *}
   1.129 +subsection {* The Schröder-Berstein Theorem *}
   1.130  
   1.131 -lemma disj_lemma: "[| -(f`X) = g`(-X);  f(a)=g(b);  a:X |] ==> b:X"
   1.132 -by blast
   1.133 +lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
   1.134 +  by blast
   1.135  
   1.136  lemma surj_if_then_else:
   1.137 -     "-(f`X) = g`(-X) ==> surj(%z. if z:X then f(z) else g(z))"
   1.138 -by (simp add: surj_def, blast)
   1.139 +  "-(f ` X) = g ` (-X) \<Longrightarrow> surj (\<lambda>z. if z \<in> X then f z else g z)"
   1.140 +  by (simp add: surj_def) blast
   1.141  
   1.142 -lemma bij_if_then_else: 
   1.143 -     "[| inj_on f X;  inj_on g (-X);  -(f`X) = g`(-X);  
   1.144 -         h = (%z. if z:X then f(z) else g(z)) |]        
   1.145 -      ==> inj(h) & surj(h)"
   1.146 -apply (unfold inj_on_def)
   1.147 -apply (simp add: surj_if_then_else)
   1.148 -apply (blast dest: disj_lemma sym)
   1.149 -done
   1.150 +lemma bij_if_then_else:
   1.151 +  "inj_on f X \<Longrightarrow> inj_on g (-X) \<Longrightarrow> -(f ` X) = g ` (-X) \<Longrightarrow>
   1.152 +    h = (\<lambda>z. if z \<in> X then f z else g z) \<Longrightarrow> inj h \<and> surj h"
   1.153 +  apply (unfold inj_on_def)
   1.154 +  apply (simp add: surj_if_then_else)
   1.155 +  apply (blast dest: disj_lemma sym)
   1.156 +  done
   1.157  
   1.158 -lemma decomposition: "EX X. X = - (g`(- (f`X)))"
   1.159 -apply (rule exI)
   1.160 -apply (rule lfp_unfold)
   1.161 -apply (rule monoI, blast) 
   1.162 -done
   1.163 +lemma decomposition: "\<exists>X. X = - (g ` (- (f ` X)))"
   1.164 +  apply (rule exI)
   1.165 +  apply (rule lfp_unfold)
   1.166 +  apply (rule monoI, blast)
   1.167 +  done
   1.168  
   1.169 -text{*Schroeder-Bernstein Theorem*}
   1.170 -lemma "[| inj (f:: 'a=>'b);  inj (g:: 'b=>'a) |]  
   1.171 -       ==> EX h:: 'a=>'b. inj(h) & surj(h)"
   1.172 -apply (rule decomposition [THEN exE])
   1.173 -apply (rule exI)
   1.174 -apply (rule bij_if_then_else)
   1.175 -   apply (rule_tac [4] refl)
   1.176 -  apply (rule_tac [2] inj_on_inv)
   1.177 -  apply (erule subset_inj_on [OF subset_UNIV]) 
   1.178 -  txt{*tricky variable instantiations!*}
   1.179 - apply (erule ssubst, subst double_complement)
   1.180 - apply (rule subsetI, erule imageE, erule ssubst, rule rangeI) 
   1.181 -apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
   1.182 -done
   1.183 +theorem Schroeder_Bernstein:
   1.184 +  "inj (f :: 'a \<Rightarrow> 'b) \<Longrightarrow> inj (g :: 'b \<Rightarrow> 'a)
   1.185 +    \<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
   1.186 +  apply (rule decomposition [THEN exE])
   1.187 +  apply (rule exI)
   1.188 +  apply (rule bij_if_then_else)
   1.189 +     apply (rule_tac [4] refl)
   1.190 +    apply (rule_tac [2] inj_on_inv)
   1.191 +    apply (erule subset_inj_on [OF subset_UNIV])
   1.192 +   txt {* Tricky variable instantiations! *}
   1.193 +   apply (erule ssubst, subst double_complement)
   1.194 +   apply (rule subsetI, erule imageE, erule ssubst, rule rangeI)
   1.195 +  apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
   1.196 +  done
   1.197  
   1.198  
   1.199 -text{*Set variable instantiation examples from 
   1.200 -W. W. Bledsoe and Guohui Feng, SET-VAR.
   1.201 -JAR 11 (3), 1993, pages 293-314.
   1.202 +subsection {* Set variable instantiation examples *}
   1.203  
   1.204 -Isabelle can prove the easy examples without any special mechanisms, but it
   1.205 -can't prove the hard ones.
   1.206 +text {*
   1.207 +  From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
   1.208 +  293-314.
   1.209 +
   1.210 +  Isabelle can prove the easy examples without any special mechanisms,
   1.211 +  but it can't prove the hard ones.
   1.212  *}
   1.213  
   1.214 -text{*Example 1, page 295.*}
   1.215 -lemma "(EX A. (ALL x:A. x <= (0::int)))"
   1.216 -by force 
   1.217 +lemma "\<exists>A. (\<forall>x \<in> A. x \<le> (0::int))"
   1.218 +  -- {* Example 1, page 295. *}
   1.219 +  by force
   1.220  
   1.221 -text{*Example 2*}
   1.222 -lemma "D : F --> (EX G. (ALL A:G. EX B:F. A <= B))";
   1.223 -by force 
   1.224 +lemma "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
   1.225 +  -- {* Example 2. *}
   1.226 +  by force
   1.227  
   1.228 -text{*Example 3*}
   1.229 -lemma "P(a) --> (EX A. (ALL x:A. P(x)) & (EX y. y:A))";
   1.230 -by force 
   1.231 +lemma "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
   1.232 +  -- {* Example 3. *}
   1.233 +  by force
   1.234  
   1.235 -text{*Example 4*}
   1.236 -lemma "a<b & b<(c::int) --> (EX A. a~:A & b:A & c~: A)"
   1.237 -by force 
   1.238 +lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
   1.239 +  -- {* Example 4. *}
   1.240 +  by force
   1.241  
   1.242 -text{*Example 5, page 298.*}
   1.243 -lemma "P(f(b)) --> (EX s A. (ALL x:A. P(x)) & f(s):A)";
   1.244 -by force 
   1.245 +lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
   1.246 +  -- {*Example 5, page 298. *}
   1.247 +  by force
   1.248  
   1.249 -text{*Example 6*}
   1.250 -lemma "P(f(b)) --> (EX s A. (ALL x:A. P(x)) & f(s):A)";
   1.251 -by force 
   1.252 +lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
   1.253 +  -- {* Example 6. *}
   1.254 +  by force
   1.255  
   1.256 -text{*Example 7*}
   1.257 -lemma "EX A. a ~: A"
   1.258 -by force 
   1.259 +lemma "\<exists>A. a \<notin> A"
   1.260 +  -- {* Example 7. *}
   1.261 +  by force
   1.262  
   1.263 -text{*Example 8*}
   1.264 -lemma "(ALL u v. u < (0::int) --> u ~= abs v) --> (EX A::int set. (ALL y. abs y ~: A) & -2 : A)"
   1.265 -by force  text{*not blast, which can't simplify -2<0*}
   1.266 +lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
   1.267 +    \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
   1.268 +  -- {* Example 8. *}
   1.269 +  by force  -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
   1.270  
   1.271 -text{*Example 9 omitted (requires the reals)*}
   1.272 +text {* Example 9 omitted (requires the reals). *}
   1.273  
   1.274 -text{*The paper has no Example 10!*}
   1.275 +text {* The paper has no Example 10! *}
   1.276  
   1.277 -text{*Example 11: needs a hint*}
   1.278 -lemma "(ALL A. 0:A & (ALL x:A. Suc(x):A) --> n:A) & 
   1.279 -       P(0) & (ALL x. P(x) --> P(Suc(x))) --> P(n)"
   1.280 -apply clarify
   1.281 -apply (drule_tac x="{x. P x}" in spec)
   1.282 -by force  
   1.283 +lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
   1.284 +  P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
   1.285 +  -- {* Example 11: needs a hint. *}
   1.286 +  apply clarify
   1.287 +  apply (drule_tac x = "{x. P x}" in spec)
   1.288 +  apply force
   1.289 +  done
   1.290  
   1.291 -text{*Example 12*}
   1.292 -lemma "(ALL A. (0,0):A & (ALL x y. (x,y):A --> (Suc(x),Suc(y)):A) --> (n,m):A)
   1.293 -       & P(n) --> P(m)"
   1.294 -by auto 
   1.295 +lemma
   1.296 +  "(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
   1.297 +    \<and> P n \<longrightarrow> P m"
   1.298 +  -- {* Example 12. *}
   1.299 +  by auto
   1.300  
   1.301 -text{*Example EO1: typo in article, and with the obvious fix it seems
   1.302 -      to require arithmetic reasoning.*}
   1.303 -lemma "(ALL x. (EX u. x=2*u) = (~(EX v. Suc x = 2*v))) --> 
   1.304 -       (EX A. ALL x. (x : A) = (Suc x ~: A))"
   1.305 -apply clarify 
   1.306 -apply (rule_tac x="{x. EX u. x = 2*u}" in exI, auto) 
   1.307 -apply (case_tac v, auto)
   1.308 -apply (drule_tac x="Suc v" and P="%x. ?a(x) ~= ?b(x)" in spec, force) 
   1.309 -done
   1.310 +lemma
   1.311 +  "(\<forall>x. (\<exists>u. x = 2 * u) = (\<not> (\<exists>v. Suc x = 2 * v))) \<longrightarrow>
   1.312 +    (\<exists>A. \<forall>x. (x \<in> A) = (Suc x \<notin> A))"
   1.313 +  -- {* Example EO1: typo in article, and with the obvious fix it seems
   1.314 +      to require arithmetic reasoning. *}
   1.315 +  apply clarify
   1.316 +  apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto)
   1.317 +   apply (case_tac v, auto)
   1.318 +  apply (drule_tac x = "Suc v" and P = "\<lambda>x. ?a x \<noteq> ?b x" in spec, force)
   1.319 +  done
   1.320  
   1.321  end