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
slotosch@2904
     1
(*  Title:      HOL/Quot/PER.ML
slotosch@2904
     2
    ID:         $Id$
slotosch@2904
     3
    Author:     Oscar Slotosch
slotosch@2904
     4
    Copyright   1997 Technische Universitaet Muenchen
slotosch@2904
     5
slotosch@2904
     6
*)
slotosch@2904
     7
open PER;
slotosch@2904
     8
wenzelm@5069
     9
Goalw [fun_per_def,per_def] "f===g=(!x y. x:D&y:D&x===y-->f x===g y)";
paulson@3457
    10
by (rtac refl 1);
slotosch@2904
    11
qed "inst_fun_per";
slotosch@2904
    12
slotosch@2904
    13
(* Witness that quot is not empty *)
wenzelm@5069
    14
Goal "?z:{s.? r.!y. y:s=y===r}";
paulson@6162
    15
by (rtac CollectI 1);
slotosch@2904
    16
by (res_inst_tac [("x","x")] exI 1);
paulson@3457
    17
by (rtac allI 1);
paulson@3457
    18
by (rtac mem_Collect_eq 1);
slotosch@2904
    19
qed "quotNE";