equal
deleted
inserted
replaced
4 Copyright 1997 Technische Universitaet Muenchen |
4 Copyright 1997 Technische Universitaet Muenchen |
5 |
5 |
6 *) |
6 *) |
7 open PER; |
7 open PER; |
8 |
8 |
9 goalw thy [fun_per_def,per_def] "f===g=(!x y.x:D&y:D&x===y-->f x===g y)"; |
9 goalw thy [fun_per_def,per_def] "f===g=(!x y. x:D&y:D&x===y-->f x===g y)"; |
10 by (rtac refl 1); |
10 by (rtac refl 1); |
11 qed "inst_fun_per"; |
11 qed "inst_fun_per"; |
12 |
12 |
13 (* Witness that quot is not empty *) |
13 (* Witness that quot is not empty *) |
14 goal thy "?z:{s.? r.!y.y:s=y===r}"; |
14 goal thy "?z:{s.? r.!y. y:s=y===r}"; |
15 fr CollectI; |
15 fr CollectI; |
16 by (res_inst_tac [("x","x")] exI 1); |
16 by (res_inst_tac [("x","x")] exI 1); |
17 by (rtac allI 1); |
17 by (rtac allI 1); |
18 by (rtac mem_Collect_eq 1); |
18 by (rtac mem_Collect_eq 1); |
19 qed "quotNE"; |
19 qed "quotNE"; |