Re: [isabelle] Search in Isabelle



> In my work, I need a definition of dimension. It states
> dim V = (SOME n. EX B<=V. independent B & V<=span B & card B =n)   

Such definitions are notoriously tricky to work with. In particular,

dim V = m ==> (EX B<=V. independent B & V<=span B & card B =m) (3)

does not hold. What if V has no dimension? Then "dim V" is still
defined, but you don't know what it is. In it cannot possibly fulfill
the defining predicate. Another way to see that (3) is strange,
instantiate m with "dim V" in (3).

The rules for working with SOME are all in Hilbert_Choice. The closest
you can get to (3) is

lemma someI2: "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)"

This requires that you know that there is an "a" that satisfies P.
Some further hints:

- There is also THE and LEAST which may or may not be more convenient
than SOME.
- Look though the "What's in Main" manual (it's only 10 pages) to
discover what there is. You can also use the pdf search facility to
search for symbols in there.
- There is also THE and LEAST which may or may not be more convenient
than SOME.
- Sometimes it is convenient to set "undefined" values to a fixed value.
For example, card A = 0 if A is infinite. Maybe something similar makes
sense for dim.

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.