[opentheory-users] standard library requests

[Ramana Kumar]

In completing the HOL4 article writer's ability to log type
definitions, I find myself using the following assumptions in addition
to those in the standard library:

|- ∀t1 t2. (t1 ⇒ t2) ⇒ (t2 ⇒ t1) ⇒ (t1 ⇔ t2)

and

|- TYPE_DEFINITION =
   (λP rep.
      (∀x' x''. (rep x' = rep x'') ⇒ (x' = x'')) ∧
      ∀x. P x ⇔ ∃x'. x = rep x')

The first of these I think should simply be in the bool package. Is it
there already? It's hard to search the list of theorems. Arguably I
ought to make a new version of the bool package that proves that
theorem and .. submit it somewhere? Doing so would be a good test of
the tool chain. What do you imagine would be the easiest way to do
that, anyway?

The second theorem I wouldn't expect to go into the standard library
because it's basically an ad hoc constant definition to package up
type definitions in HOL4. However, it is the kind of theorem I imagine
being present in a "compatibility package" sitting between HOL4
theories and the standard library. Apart from a compatibility package,
or from simply defining TYPE_DEFINITION at the start of every HOL4
theory package, what other options are there for this theorem (and
others like it)?