2904
|
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 |
|
5069
|
9 |
Goalw [fun_per_def,per_def] "f===g=(!x y. x:D&y:D&x===y-->f x===g y)";
|
3457
|
10 |
by (rtac refl 1);
|
2904
|
11 |
qed "inst_fun_per";
|
|
12 |
|
|
13 |
(* Witness that quot is not empty *)
|
5069
|
14 |
Goal "?z:{s.? r.!y. y:s=y===r}";
|
2904
|
15 |
fr CollectI;
|
|
16 |
by (res_inst_tac [("x","x")] exI 1);
|
3457
|
17 |
by (rtac allI 1);
|
|
18 |
by (rtac mem_Collect_eq 1);
|
2904
|
19 |
qed "quotNE";
|