src/HOL/ex/set.thy
author paulson
Thu Mar 14 16:48:34 2002 +0100 (2002-03-14)
changeset 13058 ad6106d7b4bb
parent 9100 9e081c812338
child 13107 8743cc847224
permissions -rw-r--r--
converted theory "set" to Isar and added some SET-VAR examples
paulson@13058
     1
(*  Title:      HOL/ex/set.thy
paulson@13058
     2
    ID:         $Id$
paulson@13058
     3
    Author:     Tobias Nipkow and Lawrence C Paulson
paulson@13058
     4
    Copyright   1991  University of Cambridge
paulson@13058
     5
paulson@13058
     6
Set Theory examples: Cantor's Theorem, Schroeder-Berstein Theorem, etc.
paulson@13058
     7
*)
wenzelm@9100
     8
wenzelm@9100
     9
theory set = Main:
wenzelm@9100
    10
paulson@13058
    11
text{*These two are cited in Benzmueller and Kohlhase's system description 
paulson@13058
    12
of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not prove.*}
paulson@13058
    13
paulson@13058
    14
lemma "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"
paulson@13058
    15
by blast
paulson@13058
    16
paulson@13058
    17
lemma "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"
paulson@13058
    18
by blast
paulson@13058
    19
paulson@13058
    20
text{*trivial example of term synthesis: apparently hard for some provers!*}
paulson@13058
    21
lemma "a ~= b ==> a:?X & b ~: ?X"
paulson@13058
    22
by blast
paulson@13058
    23
paulson@13058
    24
(** Examples for the Blast_tac paper **)
paulson@13058
    25
paulson@13058
    26
text{*Union-image, called Un_Union_image on equalities.ML*}
paulson@13058
    27
lemma "(UN x:C. f(x) Un g(x)) = Union(f`C)  Un  Union(g`C)"
paulson@13058
    28
by blast
paulson@13058
    29
paulson@13058
    30
text{*Inter-image, called Int_Inter_image on equalities.ML*}
paulson@13058
    31
lemma "(INT x:C. f(x) Int g(x)) = Inter(f`C) Int Inter(g`C)"
paulson@13058
    32
by blast
paulson@13058
    33
paulson@13058
    34
text{*Singleton I.  Nice demonstration of blast_tac--and its limitations.
paulson@13058
    35
For some unfathomable reason, UNIV_I increases the search space greatly*}
paulson@13058
    36
lemma "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"
paulson@13058
    37
by (blast del: UNIV_I)
paulson@13058
    38
paulson@13058
    39
text{*Singleton II.  variant of the benchmark above*}
paulson@13058
    40
lemma "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"
paulson@13058
    41
by (blast del: UNIV_I)
paulson@13058
    42
paulson@13058
    43
text{* A unique fixpoint theorem --- fast/best/meson all fail *}
paulson@13058
    44
paulson@13058
    45
lemma "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y"
paulson@13058
    46
apply (erule ex1E, rule ex1I, erule arg_cong)
paulson@13058
    47
apply (rule subst, assumption, erule allE, rule arg_cong, erule mp) 
paulson@13058
    48
apply (erule arg_cong) 
paulson@13058
    49
done
paulson@13058
    50
paulson@13058
    51
paulson@13058
    52
paulson@13058
    53
text{* Cantor's Theorem: There is no surjection from a set to its powerset. *}
paulson@13058
    54
paulson@13058
    55
text{*requires best-first search because it is undirectional*}
paulson@13058
    56
lemma cantor1: "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)"
paulson@13058
    57
by best
paulson@13058
    58
paulson@13058
    59
text{*This form displays the diagonal term*}
paulson@13058
    60
lemma "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)"
paulson@13058
    61
by best
paulson@13058
    62
paulson@13058
    63
text{*This form exploits the set constructs*}
paulson@13058
    64
lemma "?S ~: range(f :: 'a=>'a set)"
paulson@13058
    65
by (rule notI, erule rangeE, best)  
paulson@13058
    66
paulson@13058
    67
text{*Or just this!*}
paulson@13058
    68
lemma "?S ~: range(f :: 'a=>'a set)"
paulson@13058
    69
by best
paulson@13058
    70
paulson@13058
    71
text{* The Schroeder-Berstein Theorem *}
paulson@13058
    72
paulson@13058
    73
lemma disj_lemma: "[| -(f`X) = g`(-X);  f(a)=g(b);  a:X |] ==> b:X"
paulson@13058
    74
by blast
paulson@13058
    75
paulson@13058
    76
lemma surj_if_then_else:
paulson@13058
    77
     "-(f`X) = g`(-X) ==> surj(%z. if z:X then f(z) else g(z))"
paulson@13058
    78
by (simp add: surj_def, blast)
paulson@13058
    79
paulson@13058
    80
lemma bij_if_then_else: 
paulson@13058
    81
     "[| inj_on f X;  inj_on g (-X);  -(f`X) = g`(-X);  
paulson@13058
    82
         h = (%z. if z:X then f(z) else g(z)) |]        
paulson@13058
    83
      ==> inj(h) & surj(h)"
paulson@13058
    84
apply (unfold inj_on_def)
paulson@13058
    85
apply (simp add: surj_if_then_else)
paulson@13058
    86
apply (blast dest: disj_lemma sym)
paulson@13058
    87
done
paulson@13058
    88
paulson@13058
    89
lemma decomposition: "EX X. X = - (g`(- (f`X)))"
paulson@13058
    90
apply (rule exI)
paulson@13058
    91
apply (rule lfp_unfold)
paulson@13058
    92
apply (rule monoI, blast) 
paulson@13058
    93
done
paulson@13058
    94
paulson@13058
    95
text{*Schroeder-Bernstein Theorem*}
paulson@13058
    96
lemma "[| inj (f:: 'a=>'b);  inj (g:: 'b=>'a) |]  
paulson@13058
    97
       ==> EX h:: 'a=>'b. inj(h) & surj(h)"
paulson@13058
    98
apply (rule decomposition [THEN exE])
paulson@13058
    99
apply (rule exI)
paulson@13058
   100
apply (rule bij_if_then_else)
paulson@13058
   101
   apply (rule_tac [4] refl)
paulson@13058
   102
  apply (rule_tac [2] inj_on_inv)
paulson@13058
   103
  apply (erule subset_inj_on [OF subset_UNIV]) 
paulson@13058
   104
  txt{*tricky variable instantiations!*}
paulson@13058
   105
 apply (erule ssubst, subst double_complement)
paulson@13058
   106
 apply (rule subsetI, erule imageE, erule ssubst, rule rangeI) 
paulson@13058
   107
apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
paulson@13058
   108
done
paulson@13058
   109
paulson@13058
   110
paulson@13058
   111
text{*Set variable instantiation examples from 
paulson@13058
   112
W. W. Bledsoe and Guohui Feng, SET-VAR.
paulson@13058
   113
JAR 11 (3), 1993, pages 293-314.
paulson@13058
   114
paulson@13058
   115
Isabelle can prove the easy examples without any special mechanisms, but it
paulson@13058
   116
can't prove the hard ones.
paulson@13058
   117
*}
paulson@13058
   118
paulson@13058
   119
text{*Example 1, page 295.*}
paulson@13058
   120
lemma "(EX A. (ALL x:A. x <= (0::int)))"
paulson@13058
   121
by force 
paulson@13058
   122
paulson@13058
   123
text{*Example 2*}
paulson@13058
   124
lemma "D : F --> (EX G. (ALL A:G. EX B:F. A <= B))";
paulson@13058
   125
by force 
paulson@13058
   126
paulson@13058
   127
text{*Example 3*}
paulson@13058
   128
lemma "P(a) --> (EX A. (ALL x:A. P(x)) & (EX y. y:A))";
paulson@13058
   129
by force 
paulson@13058
   130
paulson@13058
   131
text{*Example 4*}
paulson@13058
   132
lemma "a<b & b<(c::int) --> (EX A. a~:A & b:A & c~: A)"
paulson@13058
   133
by force 
paulson@13058
   134
paulson@13058
   135
text{*Example 5, page 298.*}
paulson@13058
   136
lemma "P(f(b)) --> (EX s A. (ALL x:A. P(x)) & f(s):A)";
paulson@13058
   137
by force 
paulson@13058
   138
paulson@13058
   139
text{*Example 6*}
paulson@13058
   140
lemma "P(f(b)) --> (EX s A. (ALL x:A. P(x)) & f(s):A)";
paulson@13058
   141
by force 
paulson@13058
   142
paulson@13058
   143
text{*Example 7*}
paulson@13058
   144
lemma "EX A. a ~: A"
paulson@13058
   145
by force 
paulson@13058
   146
paulson@13058
   147
text{*Example 8*}
paulson@13058
   148
lemma "(ALL u v. u < (0::int) --> u ~= abs v) --> (EX A::int set. (ALL y. abs y ~: A) & -2 : A)"
paulson@13058
   149
by force  text{*not blast, which can't simplify -2<0*}
paulson@13058
   150
paulson@13058
   151
text{*Example 9 omitted (requires the reals)*}
paulson@13058
   152
paulson@13058
   153
text{*The paper has no Example 10!*}
paulson@13058
   154
paulson@13058
   155
text{*Example 11: needs a hint*}
paulson@13058
   156
lemma "(ALL A. 0:A & (ALL x:A. Suc(x):A) --> n:A) & 
paulson@13058
   157
       P(0) & (ALL x. P(x) --> P(Suc(x))) --> P(n)"
paulson@13058
   158
apply clarify
paulson@13058
   159
apply (drule_tac x="{x. P x}" in spec)
paulson@13058
   160
by force  
paulson@13058
   161
paulson@13058
   162
text{*Example 12*}
paulson@13058
   163
lemma "(ALL A. (0,0):A & (ALL x y. (x,y):A --> (Suc(x),Suc(y)):A) --> (n,m):A)
paulson@13058
   164
       & P(n) --> P(m)"
paulson@13058
   165
by auto 
paulson@13058
   166
paulson@13058
   167
text{*Example EO1: typo in article, and with the obvious fix it seems
paulson@13058
   168
      to require arithmetic reasoning.*}
paulson@13058
   169
lemma "(ALL x. (EX u. x=2*u) = (~(EX v. Suc x = 2*v))) --> 
paulson@13058
   170
       (EX A. ALL x. (x : A) = (Suc x ~: A))"
paulson@13058
   171
apply clarify 
paulson@13058
   172
apply (rule_tac x="{x. EX u. x = 2*u}" in exI, auto) 
paulson@13058
   173
apply (case_tac v, auto)
paulson@13058
   174
apply (drule_tac x="Suc v" and P="%x. ?a(x) ~= ?b(x)" in spec, force) 
paulson@13058
   175
done
paulson@13058
   176
wenzelm@9100
   177
end