isabelle: src/HOL/Quot/PER.ML@8c9fadda81f4 (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
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 3842 diff changeset	9	Goalw [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 *)
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 3842 diff changeset	14	Goal "?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	paulson
	Tue, 18 Aug 1998 10:24:54 +0200
changeset 5330	8c9fadda81f4
parent 5069	3ea049f7979d
child 5858	beddc19c107a
permissions	-rw-r--r--