fixed deps;
authorwenzelm
Wed Jun 21 15:58:23 2000 +0200 (2000-06-21)
changeset 91009e081c812338
parent 9099 f713ef362ad0
child 9101 b643f4d7b9e9
fixed deps;
src/HOL/ex/ROOT.ML
src/HOL/ex/set.ML
src/HOL/ex/set.thy
     1.1 --- a/src/HOL/ex/ROOT.ML	Wed Jun 21 10:34:33 2000 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Wed Jun 21 15:58:23 2000 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  time_use_thy "IntRing";
     1.6  
     1.7 -time_use     "set.ML";
     1.8 +time_use_thy "set";
     1.9  time_use_thy "MT";
    1.10  time_use_thy "Tarski";
    1.11  
     2.1 --- a/src/HOL/ex/set.ML	Wed Jun 21 10:34:33 2000 +0200
     2.2 +++ b/src/HOL/ex/set.ML	Wed Jun 21 15:58:23 2000 +0200
     2.3 @@ -6,72 +6,68 @@
     2.4  Cantor's Theorem; the Schroeder-Berstein Theorem.  
     2.5  *)
     2.6  
     2.7 -
     2.8 -writeln"File HOL/ex/set.";
     2.9 -
    2.10 -context Lfp.thy;
    2.11 -
    2.12 -(*These two are cited in Benzmueller and Kohlhash's system description of LEO,
    2.13 +(*These two are cited in Benzmueller and Kohlhase's system description of LEO,
    2.14    CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*)
    2.15  
    2.16  Goal "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))";
    2.17  by (Blast_tac 1);
    2.18 -result();
    2.19 +qed "";
    2.20  
    2.21  Goal "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))";
    2.22  by (Blast_tac 1);
    2.23 -result();
    2.24 +qed "";
    2.25  
    2.26  (*trivial example of term synthesis: apparently hard for some provers!*)
    2.27  Goal "a ~= b ==> a:?X & b ~: ?X";
    2.28  by (Blast_tac 1);
    2.29 -result();
    2.30 +qed "";
    2.31  
    2.32  (** Examples for the Blast_tac paper **)
    2.33  
    2.34  (*Union-image, called Un_Union_image on equalities.ML*)
    2.35  Goal "(UN x:C. f(x) Un g(x)) = Union(f``C)  Un  Union(g``C)";
    2.36  by (Blast_tac 1);
    2.37 -result();
    2.38 +qed "";
    2.39  
    2.40  (*Inter-image, called Int_Inter_image on equalities.ML*)
    2.41  Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)";
    2.42  by (Blast_tac 1);
    2.43 -result();
    2.44 +qed "";
    2.45  
    2.46  (*Singleton I.  Nice demonstration of blast_tac--and its limitations*)
    2.47  Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
    2.48  (*for some unfathomable reason, UNIV_I increases the search space greatly*)
    2.49  by (blast_tac (claset() delrules [UNIV_I]) 1);
    2.50 -result();
    2.51 +qed "";
    2.52  
    2.53  (*Singleton II.  variant of the benchmark above*)
    2.54  Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
    2.55  by (blast_tac (claset() delrules [UNIV_I]) 1);
    2.56  (*just Blast_tac takes 5 seconds instead of 1*)
    2.57 -result();
    2.58 +qed "";
    2.59  
    2.60  (*** A unique fixpoint theorem --- fast/best/meson all fail ***)
    2.61  
    2.62  Goal "?!x. f(g(x))=x ==> ?!y. g(f(y))=y";
    2.63  by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong,
    2.64            rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]);
    2.65 -result();
    2.66 +qed "";
    2.67 +
    2.68  
    2.69  (*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
    2.70  
    2.71 -goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)";
    2.72 +Goal "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)";
    2.73  (*requires best-first search because it is undirectional*)
    2.74  by (best_tac (claset() addSEs [equalityCE]) 1);
    2.75  qed "cantor1";
    2.76  
    2.77  (*This form displays the diagonal term*)
    2.78 -goal Set.thy "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)";
    2.79 +Goal "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)";
    2.80  by (best_tac (claset() addSEs [equalityCE]) 1);
    2.81  uresult();
    2.82  
    2.83  (*This form exploits the set constructs*)
    2.84 -goal Set.thy "?S ~: range(f :: 'a=>'a set)";
    2.85 +Goal "?S ~: range(f :: 'a=>'a set)";
    2.86  by (rtac notI 1);
    2.87  by (etac rangeE 1);
    2.88  by (etac equalityCE 1);
    2.89 @@ -82,6 +78,7 @@
    2.90  
    2.91  choplev 0;
    2.92  by (best_tac (claset() addSEs [equalityCE]) 1);
    2.93 +qed "";
    2.94  
    2.95  
    2.96  (*** The Schroder-Berstein Theorem ***)
    2.97 @@ -110,7 +107,7 @@
    2.98  by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));
    2.99  qed "decomposition";
   2.100  
   2.101 -val [injf,injg] = goal Lfp.thy 
   2.102 +val [injf,injg] = goal (the_context ())
   2.103     "[| inj (f:: 'a=>'b);  inj (g:: 'b=>'a) |] ==> \
   2.104  \   ? h:: 'a=>'b. inj(h) & surj(h)";
   2.105  by (rtac (decomposition RS exE) 1);
   2.106 @@ -125,5 +122,3 @@
   2.107  by (EVERY1 [etac ssubst, stac double_complement, 
   2.108              rtac (injg RS inv_image_comp RS sym)]);
   2.109  qed "schroeder_bernstein";
   2.110 -
   2.111 -writeln"Reached end of file.";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/set.thy	Wed Jun 21 15:58:23 2000 +0200
     3.3 @@ -0,0 +1,4 @@
     3.4 +
     3.5 +theory set = Main:
     3.6 +
     3.7 +end