isabelle: src/HOL/Fun.thy@0c7e97836e3c (annotated)

1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 923 diff changeset	1	(* Title: HOL/Fun.thy
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 923 diff changeset	3	Author: Tobias Nipkow, Cambridge University Computer Laboratory
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	4	Copyright 1994 University of Cambridge
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
2912 3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	6	Notions about functions.
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	8
2912 3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	9	Fun = Set +
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	10
4059 59c1422c9da5 New Blast_tac (and minor tidying...) paulson parents: 2912 diff changeset	11	instance set :: (term) order
59c1422c9da5 New Blast_tac (and minor tidying...) paulson parents: 2912 diff changeset	12	(subset_refl,subset_trans,subset_antisym,psubset_eq)
2912 3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	13	consts
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	14
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	15	inj, surj :: ('a => 'b) => bool (inj/surjective)
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	16	inj_onto :: ['a => 'b, 'a set] => bool
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	17	inv :: ('a => 'b) => ('b => 'a)
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	18
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	19	defs
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	20
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	21	inj_def "inj f == ! x y. f(x)=f(y) --> x=y"
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	22	inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	23	surj_def "surj f == ! y. ? x. y=f(x)"
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	24	inv_def "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	25
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv. nipkow parents: 1475 diff changeset	26	end

author	wenzelm
	Thu, 12 Feb 1998 17:53:05 +0100
changeset 4628	0c7e97836e3c
parent 4059	59c1422c9da5
child 4648	f04da668581c
permissions	-rw-r--r--