Option 2) is useful for resolving inverse functional properties in OWL, that is, if there is a property bf:isbn with the same literals asserted to two different subjects, the assumption can hold that the two subjects are equal under the presumption only one bf:isbn property can be asserted. This reminds me of the bf:Instance discussion that bf:isbn might identify a bf:Instance. Such ISBN literals can be arbitrary strings. It does not matter if they are ISBN-10, ISBN-13, with or without hyphens, correct or incorrect variants. It should not be expected that OWL resolution can normalize all forms of an ISBN intrinsically. The normalization would be an extra step in the preparation of Bibframe data, like we are used to it in the world of MARC today.
InverseFunctional is reserved for Object Properties (hences the syntax InverseFunctionalObjectProperty.
There is a roughly equivalent statement that also allows for datatype properties ; HasKey(<ClassExpression (<ObjectPropertyExpression>*) (<DataPropertyExpression>)).
Key axioms allow one to define sets of sufficient identity criteria, so that if, for the things referred to by two names, there is some matching value for each key property listed in a key axiom, the two names both refer to the same name.
Owl DataTypeRestrictions can be used to restrict the value of an ISBN property to one matching one of a specified set of regular expressions.
More powerful Knowledge Representation languages can represent more useful inferences; for example, that ISBN-9's and -12's might be missing a checksum; that ISBNs that fail their checksum might have been mistranscribed and that having certain prefixes makes it more likely that the associated manifestation is associated with some countries, publishers, imprints, etc.