equal
deleted
inserted
replaced
1584 by iprover |
1584 by iprover |
1585 |
1585 |
1586 |
1586 |
1587 subsubsection {* Inverse image of a function *} |
1587 subsubsection {* Inverse image of a function *} |
1588 |
1588 |
1589 constdefs |
1589 definition vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90) where |
1590 vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90) |
|
1591 [code del]: "f -` B == {x. f x : B}" |
1590 [code del]: "f -` B == {x. f x : B}" |
1592 |
1591 |
1593 lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)" |
1592 lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)" |
1594 by (unfold vimage_def) blast |
1593 by (unfold vimage_def) blast |
1595 |
1594 |