src/CCL/Set.ML

- Installed specific code generator for equality enforcing that
arguments do not have function types, which would result in
an error message during compilation.

- Added test case generators for basic types.

(*  Title:      set/set
    ID:         $Id$

For set.thy.

Modified version of
    Title:      HOL/set
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

For set.thy.  Set theory for higher-order logic.  A set is simply a predicate.
*)

open Set;

val [prem] = goal Set.thy "[| P(a) |] ==> a : {x. P(x)}";
by (rtac (mem_Collect_iff RS iffD2) 1);
by (rtac prem 1);
qed "CollectI";

val prems = goal Set.thy "[| a : {x. P(x)} |] ==> P(a)";
by (resolve_tac (prems RL [mem_Collect_iff  RS iffD1]) 1);
qed "CollectD";

val CollectE = make_elim CollectD;

val [prem] = goal Set.thy "[| !!x. x:A <-> x:B |] ==> A = B";
by (rtac (set_extension RS iffD2) 1);
by (rtac (prem RS allI) 1);
qed "set_ext";

(*** Bounded quantifiers ***)

val prems = goalw Set.thy [Ball_def]
    "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)";
by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
qed "ballI";

val [major,minor] = goalw Set.thy [Ball_def]
    "[| ALL x:A. P(x);  x:A |] ==> P(x)";