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