src/HOL/Quot/PER.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 6162 484adda70b65
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Quot/PER.ML
     2     ID:         $Id$
     3     Author:     Oscar Slotosch
     4     Copyright   1997 Technische Universitaet Muenchen
     5 
     6 *)
     7 open PER;
     8 
     9 Goalw [fun_per_def,per_def] "f===g=(!x y. x:D&y:D&x===y-->f x===g y)";
    10 by (rtac refl 1);
    11 qed "inst_fun_per";
    12 
    13 (* Witness that quot is not empty *)
    14 Goal "?z:{s.? r.!y. y:s=y===r}";
    15 by (rtac CollectI 1);
    16 by (res_inst_tac [("x","x")] exI 1);
    17 by (rtac allI 1);
    18 by (rtac mem_Collect_eq 1);
    19 qed "quotNE";