src/HOL/ex/set.ML
changeset 6146 00f3324048a7
parent 5786 9a2c90bdadfe
child 6171 cd237a10cbf8
equal deleted inserted replaced
6145:dea357e84ac9 6146:00f3324048a7
    17 result();
    17 result();
    18 
    18 
    19 (** Examples for the Blast_tac paper **)
    19 (** Examples for the Blast_tac paper **)
    20 
    20 
    21 (*Union-image, called Un_Union_image on equalities.ML*)
    21 (*Union-image, called Un_Union_image on equalities.ML*)
    22 Goal "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
    22 Goal "(UN x:C. f(x) Un g(x)) = Union(f``C)  Un  Union(g``C)";
    23 by (Blast_tac 1);
    23 by (Blast_tac 1);
    24 result();
    24 result();
    25 
    25 
    26 (*Inter-image, called Int_Inter_image on equalities.ML*)
    26 (*Inter-image, called Int_Inter_image on equalities.ML*)
    27 Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
    27 Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)";
    28 by (Blast_tac 1);
    28 by (Blast_tac 1);
    29 result();
    29 result();
    30 
    30 
    31 (*Singleton I.  Nice demonstration of blast_tac--and its limitations*)
    31 (*Singleton I.  Nice demonstration of blast_tac--and its limitations*)
    32 Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
    32 Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";