src/HOL/ex/set.thy
 changeset 13058 ad6106d7b4bb parent 9100 9e081c812338 child 13107 8743cc847224
```     1.1 --- a/src/HOL/ex/set.thy	Thu Mar 14 16:00:29 2002 +0100
1.2 +++ b/src/HOL/ex/set.thy	Thu Mar 14 16:48:34 2002 +0100
1.3 @@ -1,4 +1,177 @@
1.4 +(*  Title:      HOL/ex/set.thy
1.5 +    ID:         \$Id\$
1.6 +    Author:     Tobias Nipkow and Lawrence C Paulson
1.7 +    Copyright   1991  University of Cambridge
1.8 +
1.9 +Set Theory examples: Cantor's Theorem, Schroeder-Berstein Theorem, etc.
1.10 +*)
1.11
1.12  theory set = Main:
1.13
1.14 +text{*These two are cited in Benzmueller and Kohlhase's system description
1.15 +of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not prove.*}
1.16 +
1.17 +lemma "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"
1.18 +by blast
1.19 +
1.20 +lemma "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"
1.21 +by blast
1.22 +
1.23 +text{*trivial example of term synthesis: apparently hard for some provers!*}
1.24 +lemma "a ~= b ==> a:?X & b ~: ?X"
1.25 +by blast
1.26 +
1.27 +(** Examples for the Blast_tac paper **)
1.28 +
1.29 +text{*Union-image, called Un_Union_image on equalities.ML*}
1.30 +lemma "(UN x:C. f(x) Un g(x)) = Union(f`C)  Un  Union(g`C)"
1.31 +by blast
1.32 +
1.33 +text{*Inter-image, called Int_Inter_image on equalities.ML*}
1.34 +lemma "(INT x:C. f(x) Int g(x)) = Inter(f`C) Int Inter(g`C)"
1.35 +by blast
1.36 +
1.37 +text{*Singleton I.  Nice demonstration of blast_tac--and its limitations.
1.38 +For some unfathomable reason, UNIV_I increases the search space greatly*}
1.39 +lemma "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"
1.40 +by (blast del: UNIV_I)
1.41 +
1.42 +text{*Singleton II.  variant of the benchmark above*}
1.43 +lemma "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"
1.44 +by (blast del: UNIV_I)
1.45 +
1.46 +text{* A unique fixpoint theorem --- fast/best/meson all fail *}
1.47 +
1.48 +lemma "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y"
1.49 +apply (erule ex1E, rule ex1I, erule arg_cong)
1.50 +apply (rule subst, assumption, erule allE, rule arg_cong, erule mp)
1.51 +apply (erule arg_cong)
1.52 +done
1.53 +
1.54 +
1.55 +
1.56 +text{* Cantor's Theorem: There is no surjection from a set to its powerset. *}
1.57 +
1.58 +text{*requires best-first search because it is undirectional*}
1.59 +lemma cantor1: "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)"
1.60 +by best
1.61 +
1.62 +text{*This form displays the diagonal term*}
1.63 +lemma "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)"
1.64 +by best
1.65 +
1.66 +text{*This form exploits the set constructs*}
1.67 +lemma "?S ~: range(f :: 'a=>'a set)"
1.68 +by (rule notI, erule rangeE, best)
1.69 +
1.70 +text{*Or just this!*}
1.71 +lemma "?S ~: range(f :: 'a=>'a set)"
1.72 +by best
1.73 +
1.74 +text{* The Schroeder-Berstein Theorem *}
1.75 +
1.76 +lemma disj_lemma: "[| -(f`X) = g`(-X);  f(a)=g(b);  a:X |] ==> b:X"
1.77 +by blast
1.78 +
1.79 +lemma surj_if_then_else:
1.80 +     "-(f`X) = g`(-X) ==> surj(%z. if z:X then f(z) else g(z))"
1.81 +by (simp add: surj_def, blast)
1.82 +
1.83 +lemma bij_if_then_else:
1.84 +     "[| inj_on f X;  inj_on g (-X);  -(f`X) = g`(-X);
1.85 +         h = (%z. if z:X then f(z) else g(z)) |]
1.86 +      ==> inj(h) & surj(h)"
1.87 +apply (unfold inj_on_def)
1.89 +apply (blast dest: disj_lemma sym)
1.90 +done
1.91 +
1.92 +lemma decomposition: "EX X. X = - (g`(- (f`X)))"
1.93 +apply (rule exI)
1.94 +apply (rule lfp_unfold)
1.95 +apply (rule monoI, blast)
1.96 +done
1.97 +
1.98 +text{*Schroeder-Bernstein Theorem*}
1.99 +lemma "[| inj (f:: 'a=>'b);  inj (g:: 'b=>'a) |]
1.100 +       ==> EX h:: 'a=>'b. inj(h) & surj(h)"
1.101 +apply (rule decomposition [THEN exE])
1.102 +apply (rule exI)
1.103 +apply (rule bij_if_then_else)
1.104 +   apply (rule_tac [4] refl)
1.105 +  apply (rule_tac [2] inj_on_inv)
1.106 +  apply (erule subset_inj_on [OF subset_UNIV])
1.107 +  txt{*tricky variable instantiations!*}
1.108 + apply (erule ssubst, subst double_complement)
1.109 + apply (rule subsetI, erule imageE, erule ssubst, rule rangeI)
1.110 +apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
1.111 +done
1.112 +
1.113 +
1.114 +text{*Set variable instantiation examples from
1.115 +W. W. Bledsoe and Guohui Feng, SET-VAR.
1.116 +JAR 11 (3), 1993, pages 293-314.
1.117 +
1.118 +Isabelle can prove the easy examples without any special mechanisms, but it
1.119 +can't prove the hard ones.
1.120 +*}
1.121 +
1.122 +text{*Example 1, page 295.*}
1.123 +lemma "(EX A. (ALL x:A. x <= (0::int)))"
1.124 +by force
1.125 +
1.126 +text{*Example 2*}
1.127 +lemma "D : F --> (EX G. (ALL A:G. EX B:F. A <= B))";
1.128 +by force
1.129 +
1.130 +text{*Example 3*}
1.131 +lemma "P(a) --> (EX A. (ALL x:A. P(x)) & (EX y. y:A))";
1.132 +by force
1.133 +
1.134 +text{*Example 4*}
1.135 +lemma "a<b & b<(c::int) --> (EX A. a~:A & b:A & c~: A)"
1.136 +by force
1.137 +
1.138 +text{*Example 5, page 298.*}
1.139 +lemma "P(f(b)) --> (EX s A. (ALL x:A. P(x)) & f(s):A)";
1.140 +by force
1.141 +
1.142 +text{*Example 6*}
1.143 +lemma "P(f(b)) --> (EX s A. (ALL x:A. P(x)) & f(s):A)";
1.144 +by force
1.145 +
1.146 +text{*Example 7*}
1.147 +lemma "EX A. a ~: A"
1.148 +by force
1.149 +
1.150 +text{*Example 8*}
1.151 +lemma "(ALL u v. u < (0::int) --> u ~= abs v) --> (EX A::int set. (ALL y. abs y ~: A) & -2 : A)"
1.152 +by force  text{*not blast, which can't simplify -2<0*}
1.153 +
1.154 +text{*Example 9 omitted (requires the reals)*}
1.155 +
1.156 +text{*The paper has no Example 10!*}
1.157 +
1.158 +text{*Example 11: needs a hint*}
1.159 +lemma "(ALL A. 0:A & (ALL x:A. Suc(x):A) --> n:A) &
1.160 +       P(0) & (ALL x. P(x) --> P(Suc(x))) --> P(n)"
1.161 +apply clarify
1.162 +apply (drule_tac x="{x. P x}" in spec)
1.163 +by force
1.164 +
1.165 +text{*Example 12*}
1.166 +lemma "(ALL A. (0,0):A & (ALL x y. (x,y):A --> (Suc(x),Suc(y)):A) --> (n,m):A)
1.167 +       & P(n) --> P(m)"
1.168 +by auto
1.169 +
1.170 +text{*Example EO1: typo in article, and with the obvious fix it seems
1.171 +      to require arithmetic reasoning.*}
1.172 +lemma "(ALL x. (EX u. x=2*u) = (~(EX v. Suc x = 2*v))) -->
1.173 +       (EX A. ALL x. (x : A) = (Suc x ~: A))"
1.174 +apply clarify
1.175 +apply (rule_tac x="{x. EX u. x = 2*u}" in exI, auto)
1.176 +apply (case_tac v, auto)
1.177 +apply (drule_tac x="Suc v" and P="%x. ?a(x) ~= ?b(x)" in spec, force)
1.178 +done
1.179 +
1.180  end
```