converted theory "set" to Isar and added some SET-VAR examples
authorpaulson
Thu Mar 14 16:48:34 2002 +0100 (2002-03-14)
changeset 13058ad6106d7b4bb
parent 13057 805de10ca485
child 13059 d78d2089e163
converted theory "set" to Isar and added some SET-VAR examples
src/HOL/ex/set.ML
src/HOL/ex/set.thy
     1.1 --- a/src/HOL/ex/set.ML	Thu Mar 14 16:00:29 2002 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,123 +0,0 @@
     1.4 -(*  Title:      HOL/ex/set.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8 -
     1.9 -Cantor's Theorem; the Schroeder-Berstein Theorem.  
    1.10 -*)
    1.11 -
    1.12 -(*These two are cited in Benzmueller and Kohlhase's system description of LEO,
    1.13 -  CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*)
    1.14 -
    1.15 -Goal "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))";
    1.16 -by (Blast_tac 1);
    1.17 -qed "";
    1.18 -
    1.19 -Goal "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))";
    1.20 -by (Blast_tac 1);
    1.21 -qed "";
    1.22 -
    1.23 -(*trivial example of term synthesis: apparently hard for some provers!*)
    1.24 -Goal "a ~= b ==> a:?X & b ~: ?X";
    1.25 -by (Blast_tac 1);
    1.26 -qed "";
    1.27 -
    1.28 -(** Examples for the Blast_tac paper **)
    1.29 -
    1.30 -(*Union-image, called Un_Union_image on equalities.ML*)
    1.31 -Goal "(UN x:C. f(x) Un g(x)) = Union(f`C)  Un  Union(g`C)";
    1.32 -by (Blast_tac 1);
    1.33 -qed "";
    1.34 -
    1.35 -(*Inter-image, called Int_Inter_image on equalities.ML*)
    1.36 -Goal "(INT x:C. f(x) Int g(x)) = Inter(f`C) Int Inter(g`C)";
    1.37 -by (Blast_tac 1);
    1.38 -qed "";
    1.39 -
    1.40 -(*Singleton I.  Nice demonstration of blast_tac--and its limitations*)
    1.41 -Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
    1.42 -(*for some unfathomable reason, UNIV_I increases the search space greatly*)
    1.43 -by (blast_tac (claset() delrules [UNIV_I]) 1);
    1.44 -qed "";
    1.45 -
    1.46 -(*Singleton II.  variant of the benchmark above*)
    1.47 -Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
    1.48 -by (blast_tac (claset() delrules [UNIV_I]) 1);
    1.49 -(*just Blast_tac takes 5 seconds instead of 1*)
    1.50 -qed "";
    1.51 -
    1.52 -(*** A unique fixpoint theorem --- fast/best/meson all fail ***)
    1.53 -
    1.54 -Goal "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y";
    1.55 -by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong,
    1.56 -          rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]);
    1.57 -qed "";
    1.58 -
    1.59 -
    1.60 -(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
    1.61 -
    1.62 -Goal "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)";
    1.63 -(*requires best-first search because it is undirectional*)
    1.64 -by (Best_tac 1);
    1.65 -qed "cantor1";
    1.66 -
    1.67 -(*This form displays the diagonal term*)
    1.68 -Goal "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)";
    1.69 -by (Best_tac 1);
    1.70 -uresult();
    1.71 -
    1.72 -(*This form exploits the set constructs*)
    1.73 -Goal "?S ~: range(f :: 'a=>'a set)";
    1.74 -by (rtac notI 1);
    1.75 -by (etac rangeE 1);
    1.76 -by (etac equalityCE 1);
    1.77 -by (dtac CollectD 1);
    1.78 -by (contr_tac 1);
    1.79 -by (swap_res_tac [CollectI] 1);
    1.80 -by (assume_tac 1);
    1.81 -
    1.82 -choplev 0;
    1.83 -by (Best_tac 1);
    1.84 -qed "";
    1.85 -
    1.86 -
    1.87 -(*** The Schroeder-Berstein Theorem ***)
    1.88 -
    1.89 -Goal "[| -(f`X) = g`(-X);  f(a)=g(b);  a:X |] ==> b:X";
    1.90 -by (Blast_tac 1);
    1.91 -qed "disj_lemma";
    1.92 -
    1.93 -Goal "-(f`X) = g`(-X) ==> surj(%z. if z:X then f(z) else g(z))";
    1.94 -by (asm_simp_tac (simpset() addsimps [surj_def]) 1);
    1.95 -by (Blast_tac 1);
    1.96 -qed "surj_if_then_else";
    1.97 -
    1.98 -Goalw [inj_on_def]
    1.99 -     "[| inj_on f X;  inj_on g (-X);  -(f`X) = g`(-X); \
   1.100 -\        h = (%z. if z:X then f(z) else g(z)) |]       \
   1.101 -\     ==> inj(h) & surj(h)";
   1.102 -by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1);
   1.103 -by (blast_tac (claset() addDs [disj_lemma, sym]) 1);
   1.104 -qed "bij_if_then_else";
   1.105 -
   1.106 -Goal "EX X. X = - (g`(- (f`X)))";
   1.107 -by (rtac exI 1);
   1.108 -by (rtac lfp_unfold 1);
   1.109 -by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));
   1.110 -qed "decomposition";
   1.111 -
   1.112 -val [injf,injg] = goal (the_context ())
   1.113 -   "[| inj (f:: 'a=>'b);  inj (g:: 'b=>'a) |] \
   1.114 -\   ==> EX h:: 'a=>'b. inj(h) & surj(h)";
   1.115 -by (rtac (decomposition RS exE) 1);
   1.116 -by (rtac exI 1);
   1.117 -by (rtac bij_if_then_else 1);
   1.118 -by (rtac refl 4);
   1.119 -by (rtac inj_on_inv 2);
   1.120 -by (rtac ([subset_UNIV, injf] MRS subset_inj_on) 1);
   1.121 -  (**tricky variable instantiations!**)
   1.122 -by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI,
   1.123 -            etac imageE, etac ssubst, rtac rangeI]);
   1.124 -by (EVERY1 [etac ssubst, stac double_complement, 
   1.125 -            rtac (injg RS inv_image_comp RS sym)]);
   1.126 -qed "schroeder_bernstein";
     2.1 --- a/src/HOL/ex/set.thy	Thu Mar 14 16:00:29 2002 +0100
     2.2 +++ b/src/HOL/ex/set.thy	Thu Mar 14 16:48:34 2002 +0100
     2.3 @@ -1,4 +1,177 @@
     2.4 +(*  Title:      HOL/ex/set.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow and Lawrence C Paulson
     2.7 +    Copyright   1991  University of Cambridge
     2.8 +
     2.9 +Set Theory examples: Cantor's Theorem, Schroeder-Berstein Theorem, etc.
    2.10 +*)
    2.11  
    2.12  theory set = Main:
    2.13  
    2.14 +text{*These two are cited in Benzmueller and Kohlhase's system description 
    2.15 +of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not prove.*}
    2.16 +
    2.17 +lemma "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"
    2.18 +by blast
    2.19 +
    2.20 +lemma "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"
    2.21 +by blast
    2.22 +
    2.23 +text{*trivial example of term synthesis: apparently hard for some provers!*}
    2.24 +lemma "a ~= b ==> a:?X & b ~: ?X"
    2.25 +by blast
    2.26 +
    2.27 +(** Examples for the Blast_tac paper **)
    2.28 +
    2.29 +text{*Union-image, called Un_Union_image on equalities.ML*}
    2.30 +lemma "(UN x:C. f(x) Un g(x)) = Union(f`C)  Un  Union(g`C)"
    2.31 +by blast
    2.32 +
    2.33 +text{*Inter-image, called Int_Inter_image on equalities.ML*}
    2.34 +lemma "(INT x:C. f(x) Int g(x)) = Inter(f`C) Int Inter(g`C)"
    2.35 +by blast
    2.36 +
    2.37 +text{*Singleton I.  Nice demonstration of blast_tac--and its limitations.
    2.38 +For some unfathomable reason, UNIV_I increases the search space greatly*}
    2.39 +lemma "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"
    2.40 +by (blast del: UNIV_I)
    2.41 +
    2.42 +text{*Singleton II.  variant of the benchmark above*}
    2.43 +lemma "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"
    2.44 +by (blast del: UNIV_I)
    2.45 +
    2.46 +text{* A unique fixpoint theorem --- fast/best/meson all fail *}
    2.47 +
    2.48 +lemma "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y"
    2.49 +apply (erule ex1E, rule ex1I, erule arg_cong)
    2.50 +apply (rule subst, assumption, erule allE, rule arg_cong, erule mp) 
    2.51 +apply (erule arg_cong) 
    2.52 +done
    2.53 +
    2.54 +
    2.55 +
    2.56 +text{* Cantor's Theorem: There is no surjection from a set to its powerset. *}
    2.57 +
    2.58 +text{*requires best-first search because it is undirectional*}
    2.59 +lemma cantor1: "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)"
    2.60 +by best
    2.61 +
    2.62 +text{*This form displays the diagonal term*}
    2.63 +lemma "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)"
    2.64 +by best
    2.65 +
    2.66 +text{*This form exploits the set constructs*}
    2.67 +lemma "?S ~: range(f :: 'a=>'a set)"
    2.68 +by (rule notI, erule rangeE, best)  
    2.69 +
    2.70 +text{*Or just this!*}
    2.71 +lemma "?S ~: range(f :: 'a=>'a set)"
    2.72 +by best
    2.73 +
    2.74 +text{* The Schroeder-Berstein Theorem *}
    2.75 +
    2.76 +lemma disj_lemma: "[| -(f`X) = g`(-X);  f(a)=g(b);  a:X |] ==> b:X"
    2.77 +by blast
    2.78 +
    2.79 +lemma surj_if_then_else:
    2.80 +     "-(f`X) = g`(-X) ==> surj(%z. if z:X then f(z) else g(z))"
    2.81 +by (simp add: surj_def, blast)
    2.82 +
    2.83 +lemma bij_if_then_else: 
    2.84 +     "[| inj_on f X;  inj_on g (-X);  -(f`X) = g`(-X);  
    2.85 +         h = (%z. if z:X then f(z) else g(z)) |]        
    2.86 +      ==> inj(h) & surj(h)"
    2.87 +apply (unfold inj_on_def)
    2.88 +apply (simp add: surj_if_then_else)
    2.89 +apply (blast dest: disj_lemma sym)
    2.90 +done
    2.91 +
    2.92 +lemma decomposition: "EX X. X = - (g`(- (f`X)))"
    2.93 +apply (rule exI)
    2.94 +apply (rule lfp_unfold)
    2.95 +apply (rule monoI, blast) 
    2.96 +done
    2.97 +
    2.98 +text{*Schroeder-Bernstein Theorem*}
    2.99 +lemma "[| inj (f:: 'a=>'b);  inj (g:: 'b=>'a) |]  
   2.100 +       ==> EX h:: 'a=>'b. inj(h) & surj(h)"
   2.101 +apply (rule decomposition [THEN exE])
   2.102 +apply (rule exI)
   2.103 +apply (rule bij_if_then_else)
   2.104 +   apply (rule_tac [4] refl)
   2.105 +  apply (rule_tac [2] inj_on_inv)
   2.106 +  apply (erule subset_inj_on [OF subset_UNIV]) 
   2.107 +  txt{*tricky variable instantiations!*}
   2.108 + apply (erule ssubst, subst double_complement)
   2.109 + apply (rule subsetI, erule imageE, erule ssubst, rule rangeI) 
   2.110 +apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
   2.111 +done
   2.112 +
   2.113 +
   2.114 +text{*Set variable instantiation examples from 
   2.115 +W. W. Bledsoe and Guohui Feng, SET-VAR.
   2.116 +JAR 11 (3), 1993, pages 293-314.
   2.117 +
   2.118 +Isabelle can prove the easy examples without any special mechanisms, but it
   2.119 +can't prove the hard ones.
   2.120 +*}
   2.121 +
   2.122 +text{*Example 1, page 295.*}
   2.123 +lemma "(EX A. (ALL x:A. x <= (0::int)))"
   2.124 +by force 
   2.125 +
   2.126 +text{*Example 2*}
   2.127 +lemma "D : F --> (EX G. (ALL A:G. EX B:F. A <= B))";
   2.128 +by force 
   2.129 +
   2.130 +text{*Example 3*}
   2.131 +lemma "P(a) --> (EX A. (ALL x:A. P(x)) & (EX y. y:A))";
   2.132 +by force 
   2.133 +
   2.134 +text{*Example 4*}
   2.135 +lemma "a<b & b<(c::int) --> (EX A. a~:A & b:A & c~: A)"
   2.136 +by force 
   2.137 +
   2.138 +text{*Example 5, page 298.*}
   2.139 +lemma "P(f(b)) --> (EX s A. (ALL x:A. P(x)) & f(s):A)";
   2.140 +by force 
   2.141 +
   2.142 +text{*Example 6*}
   2.143 +lemma "P(f(b)) --> (EX s A. (ALL x:A. P(x)) & f(s):A)";
   2.144 +by force 
   2.145 +
   2.146 +text{*Example 7*}
   2.147 +lemma "EX A. a ~: A"
   2.148 +by force 
   2.149 +
   2.150 +text{*Example 8*}
   2.151 +lemma "(ALL u v. u < (0::int) --> u ~= abs v) --> (EX A::int set. (ALL y. abs y ~: A) & -2 : A)"
   2.152 +by force  text{*not blast, which can't simplify -2<0*}
   2.153 +
   2.154 +text{*Example 9 omitted (requires the reals)*}
   2.155 +
   2.156 +text{*The paper has no Example 10!*}
   2.157 +
   2.158 +text{*Example 11: needs a hint*}
   2.159 +lemma "(ALL A. 0:A & (ALL x:A. Suc(x):A) --> n:A) & 
   2.160 +       P(0) & (ALL x. P(x) --> P(Suc(x))) --> P(n)"
   2.161 +apply clarify
   2.162 +apply (drule_tac x="{x. P x}" in spec)
   2.163 +by force  
   2.164 +
   2.165 +text{*Example 12*}
   2.166 +lemma "(ALL A. (0,0):A & (ALL x y. (x,y):A --> (Suc(x),Suc(y)):A) --> (n,m):A)
   2.167 +       & P(n) --> P(m)"
   2.168 +by auto 
   2.169 +
   2.170 +text{*Example EO1: typo in article, and with the obvious fix it seems
   2.171 +      to require arithmetic reasoning.*}
   2.172 +lemma "(ALL x. (EX u. x=2*u) = (~(EX v. Suc x = 2*v))) --> 
   2.173 +       (EX A. ALL x. (x : A) = (Suc x ~: A))"
   2.174 +apply clarify 
   2.175 +apply (rule_tac x="{x. EX u. x = 2*u}" in exI, auto) 
   2.176 +apply (case_tac v, auto)
   2.177 +apply (drule_tac x="Suc v" and P="%x. ?a(x) ~= ?b(x)" in spec, force) 
   2.178 +done
   2.179 +
   2.180  end