src/ZF/ex/misc.ML
 changeset 8266 4bc79ed1233b parent 5431 d50c2783f941 child 9061 144b06e6729e
equal inserted replaced
8265:187cada50e19 8266:4bc79ed1233b
`     6 Miscellaneous examples for Zermelo-Fraenkel Set Theory `
`     6 Miscellaneous examples for Zermelo-Fraenkel Set Theory `
`     7 Composition of homomorphisms, Pastre's examples, ...`
`     7 Composition of homomorphisms, Pastre's examples, ...`
`     8 *)`
`     8 *)`
`     9 `
`     9 `
`    10 writeln"ZF/ex/misc";`
`    10 writeln"ZF/ex/misc";`
`       `
`    11 `
`       `
`    12 (*These two are cited in Benzmueller and Kohlhash's system description of LEO,`
`       `
`    13   CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*)`
`       `
`    14 `
`       `
`    15 Goal "(X = Y Un Z) <-> (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))";`
`       `
`    16 by (blast_tac (claset() addSIs [equalityI]) 1);`
`       `
`    17 result();`
`       `
`    18 `
`       `
`    19 (*the dual of the previous one*)`
`       `
`    20 Goal "(X = Y Int Z) <-> (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))";`
`       `
`    21 by (blast_tac (claset() addSIs [equalityI]) 1);`
`       `
`    22 result();`
`    11 `
`    23 `
`    12 (*trivial example of term synthesis: apparently hard for some provers!*)`
`    24 (*trivial example of term synthesis: apparently hard for some provers!*)`
`    13 Goal "a ~= b ==> a:?X & b ~: ?X";`
`    25 Goal "a ~= b ==> a:?X & b ~: ?X";`
`    14 by (Blast_tac 1);`
`    26 by (Blast_tac 1);`
`    15 result();`
`    27 result();`