isabelle: src/HOL/Fun.thy@01cbf154d926 (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
4648 f04da668581c New theory of the inverse image of a function paulson parents: 4059 diff changeset	9	Fun = Vimage +
2912 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
4830 bd73675adbed Added a few lemmas. nipkow parents: 4648 diff changeset	15	inj, surj :: ('a => 'b) => bool (inj/surjective)
bd73675adbed Added a few lemmas. nipkow parents: 4648 diff changeset	16	inj_on :: ['a => 'b, 'a set] => bool
bd73675adbed Added a few lemmas. nipkow parents: 4648 diff changeset	17	inv :: ('a => 'b) => ('b => 'a)
2912 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
4830 bd73675adbed Added a few lemmas. nipkow parents: 4648 diff changeset	21	inj_def "inj f == ! x y. f(x)=f(y) --> x=y"
bd73675adbed Added a few lemmas. nipkow parents: 4648 diff changeset	22	inj_on_def "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
bd73675adbed Added a few lemmas. nipkow parents: 4648 diff changeset	23	surj_def "surj f == ! y. ? x. y=f(x)"
bd73675adbed Added a few lemmas. nipkow parents: 4648 diff changeset	24	inv_def "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
2912 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
	Fri, 03 Jul 1998 18:05:03 +0200
changeset 5126	01cbf154d926
parent 4830	bd73675adbed
child 5305	513925de8962
permissions	-rw-r--r--