isabelle: src/HOL/Quot/PER.ML@0b268cff9344 (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
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	9	goalw thy [fun_per_def,per_def] "f===g=(!x y.x:D&y:D&x===y-->f x===g y)";
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	10	br refl 1;
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 *)
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	14	goal thy "?z:{s.? r.!y.y:s=y===r}";
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);
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	17	br allI 1;
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	18	br mem_Collect_eq 1;
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	19	qed "quotNE";

author	wenzelm
	Tue, 27 May 1997 15:45:07 +0200
changeset 3362	0b268cff9344
parent 2904	fc10751254aa
child 3457	a8ab7c64817c
permissions	-rw-r--r--