# HG changeset patch # User paulson # Date 951128143 -3600 # Node ID 4bc79ed1233bda7cdfc27e7e4a0bea148167ee57 # Parent 187cada50e19f66da3b831386d9a0da1066f21f0 new examples that cannot be done in LEO diff -r 187cada50e19 -r 4bc79ed1233b src/HOL/ex/set.ML --- a/src/HOL/ex/set.ML Mon Feb 21 10:20:38 2000 +0100 +++ b/src/HOL/ex/set.ML Mon Feb 21 11:15:43 2000 +0100 @@ -11,6 +11,17 @@ context Lfp.thy; +(*These two are cited in Benzmueller and Kohlhash's system description of LEO, + CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*) + +Goal "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"; +by (Blast_tac 1); +result(); + +Goal "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"; +by (Blast_tac 1); +result(); + (*trivial example of term synthesis: apparently hard for some provers!*) Goal "a ~= b ==> a:?X & b ~: ?X"; by (Blast_tac 1); diff -r 187cada50e19 -r 4bc79ed1233b src/ZF/ex/misc.ML --- a/src/ZF/ex/misc.ML Mon Feb 21 10:20:38 2000 +0100 +++ b/src/ZF/ex/misc.ML Mon Feb 21 11:15:43 2000 +0100 @@ -9,6 +9,18 @@ writeln"ZF/ex/misc"; +(*These two are cited in Benzmueller and Kohlhash's system description of LEO, + CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*) + +Goal "(X = Y Un Z) <-> (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"; +by (blast_tac (claset() addSIs [equalityI]) 1); +result(); + +(*the dual of the previous one*) +Goal "(X = Y Int Z) <-> (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"; +by (blast_tac (claset() addSIs [equalityI]) 1); +result(); + (*trivial example of term synthesis: apparently hard for some provers!*) Goal "a ~= b ==> a:?X & b ~: ?X"; by (Blast_tac 1);