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.88 +apply (simp add: surj_if_then_else)
    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