isabelle: src/HOL/Quot/PER.ML@b55686a7b22c (annotated)

2904 fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	1	(* Title: HOL/Quot/PER.ML
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	2	ID: $Id$
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	3	Author: Oscar Slotosch
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	4	Copyright 1997 Technische Universitaet Muenchen
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	5
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	6	*)
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	7	open PER;
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	8
3842 b55686a7b22c fixed dots; wenzelm parents: 3457 diff changeset	9	goalw thy [fun_per_def,per_def] "f===g=(!x y. x:D&y:D&x===y-->f x===g y)";
3457 a8ab7c64817c Ran expandshort paulson parents: 2904 diff changeset	10	by (rtac refl 1);
2904 fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	11	qed "inst_fun_per";
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	12
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	13	(* Witness that quot is not empty *)
3842 b55686a7b22c fixed dots; wenzelm parents: 3457 diff changeset	14	goal thy "?z:{s.? r.!y. y:s=y===r}";
2904 fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	15	fr CollectI;
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	16	by (res_inst_tac [("x","x")] exI 1);
3457 a8ab7c64817c Ran expandshort paulson parents: 2904 diff changeset	17	by (rtac allI 1);
a8ab7c64817c Ran expandshort paulson parents: 2904 diff changeset	18	by (rtac mem_Collect_eq 1);
2904 fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	19	qed "quotNE";

author	wenzelm
	Fri, 10 Oct 1997 19:02:28 +0200
changeset 3842	b55686a7b22c
parent 3457	a8ab7c64817c
child 5069	3ea049f7979d
permissions	-rw-r--r--