src/ZF/Coind/Language.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.

(*  Title:      ZF/Coind/Language.ML
    ID:         $Id$
    Author:     Jacob Frost, Cambridge University Computer Laboratory
    Copyright   1995  University of Cambridge
*)

(* ############################################################ *)
(* General lemmas                                               *)
(* ############################################################ *)

goal ZF.thy "!!a.~a=b ==> ~a:{b}";
by (fast_tac ZF_cs 1);    
qed "notsingletonI";

goal ZF.thy "!!a.~a:{b} ==> ~a=b";
by (fast_tac ZF_cs 1);    
qed "notsingletonD";

val prems = goal ZF.thy "[| a~:{b}; a~=b ==> P |] ==> P";
by (cut_facts_tac prems 1);
by (resolve_tac prems 1);
by (fast_tac ZF_cs 1);    
qed "notsingletonE";

goal ZF.thy "!!x. x : A Un B ==> x: B Un A";
by (fast_tac ZF_cs 1);
qed "lem_fix";

goal ZF.thy "!!A.[| x~:A; x=y |] ==> y~:A";
by (fast_tac ZF_cs 1);
qed "map_lem1";


open Language;