tuned;
authorwenzelm
Tue Jun 13 18:36:06 2000 +0200 (2000-06-13)
changeset 9061144b06e6729e
parent 9060 b0dd884b1848
child 9062 7b34ffecaaa8
tuned;
src/ZF/ex/misc.ML
     1.1 --- a/src/ZF/ex/misc.ML	Tue Jun 13 18:34:59 2000 +0200
     1.2 +++ b/src/ZF/ex/misc.ML	Tue Jun 13 18:36:06 2000 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      ZF/ex/misc
     1.5 +(*  Title:      ZF/ex/misc.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9 @@ -7,34 +7,32 @@
    1.10  Composition of homomorphisms, Pastre's examples, ...
    1.11  *)
    1.12  
    1.13 -writeln"ZF/ex/misc";
    1.14 -
    1.15 -(*These two are cited in Benzmueller and Kohlhash's system description of LEO,
    1.16 +(*These two are cited in Benzmueller and Kohlhase's system description of LEO,
    1.17    CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*)
    1.18  
    1.19  Goal "(X = Y Un Z) <-> (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))";
    1.20  by (blast_tac (claset() addSIs [equalityI]) 1);
    1.21 -result();
    1.22 +qed "";
    1.23  
    1.24  (*the dual of the previous one*)
    1.25  Goal "(X = Y Int Z) <-> (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))";
    1.26  by (blast_tac (claset() addSIs [equalityI]) 1);
    1.27 -result();
    1.28 +qed "";
    1.29  
    1.30  (*trivial example of term synthesis: apparently hard for some provers!*)
    1.31  Goal "a ~= b ==> a:?X & b ~: ?X";
    1.32  by (Blast_tac 1);
    1.33 -result();
    1.34 +qed "";
    1.35  
    1.36  (*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
    1.37  Goal "ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
    1.38  by (Blast_tac 1);
    1.39 -result();
    1.40 +qed "";
    1.41  
    1.42  (*variant of the benchmark above*)
    1.43  Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
    1.44  by (Blast_tac 1);
    1.45 -result();
    1.46 +qed "";
    1.47  
    1.48  context Perm.thy;
    1.49  
    1.50 @@ -44,7 +42,7 @@
    1.51   Ellis Horwood, 53-100 (1979). *)
    1.52  Goal "(ALL F. {x}: F --> {y}:F) --> (ALL A. x:A --> y:A)";
    1.53  by (Best_tac 1);
    1.54 -result();
    1.55 +qed "";
    1.56  
    1.57  
    1.58  (*** Composition of homomorphisms is a homomorphism ***)
    1.59 @@ -68,7 +66,7 @@
    1.60  \    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
    1.61  \    (K O J) : hom(A,f,C,h)";
    1.62  by (asm_simp_tac (simpset() setloop (K Safe_tac)) 1);
    1.63 -val comp_homs = result();
    1.64 +qed "";
    1.65  
    1.66  (*This version uses meta-level rewriting, safe_tac and asm_simp_tac*)
    1.67  val [hom_def] = goal Perm.thy
    1.68 @@ -89,7 +87,7 @@
    1.69  Goalw [Pi_def, function_def]
    1.70      "r: domain(r)->B  <->  r <= domain(r)*B & (ALL X. r `` (r -`` X) <= X)";
    1.71  by (Best_tac 1);
    1.72 -result();
    1.73 +qed "";
    1.74  
    1.75  
    1.76  (**** From D Pastre.  Automatic theorem proving in set theory. 
    1.77 @@ -191,5 +189,3 @@
    1.78  by (Asm_simp_tac 1);
    1.79  by (Blast_tac 1);
    1.80  qed "Pow_Sigma_bij";
    1.81 -
    1.82 -writeln"Reached end of file.";