Promote HOL-Light's pairwise to pred_setTheory replacing the old one

[binghe]

Hi,

currently there are two versions of pairwise describing pairwise (binary) relation of set elements. The existing one in pred_setTheory allow pairs of two identical elements:

   [pairwise_def]  Definition (pred_setTheory)
      ⊢ ∀P s. pairwise P s ⇔ ∀e1 e2. e1 ∈ s ∧ e2 ∈ s ⇒ P e1 e2

While the version in topologyTheory was from HOL-Light, requiring pairs of distinct elements:

   [pairwise]  Definition (topologyTheory)
      ⊢ ∀r s. pairwise r s ⇔ ∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ⇒ r x y

The version in pred_setTheory is currently not used by any other proofs in the core theory (or basic examples, I didn't test all examples) and there are only two supporting simple lemmas. On the other hand, HOL-Light's pairwise was originally ported as part of real_topologyTheory and is used in various places. In particular, the following definition of disjoint (currently in util_probTheory) can be improved by re-defining it as an overload to pairwise DISJOINT:

   [disjoint_def]  Definition      
      ⊢ ∀A. disjoint A ⇔ ∀a b. a ∈ A ∧ b ∈ A ∧ a ≠ b ⇒ DISJOINT a b

For better compatibility with HOL-Light derived theories, I propose we merge the two pairwise definitions and use HOL-Light's version as the referenced version in core library. This looks like we added the distinct requirements into the existing definition and the existing two lemmas either remains or have slightly changed. The above disjoint_def and supporting theorems are refined and moved from util_prob to topology.

For other irrelevant small changes, there's a leftover in src/rational for the name changes of ring-related stuff. I also renamed the newly added theorem permutes_bijn to permutes_alt_bijns, mostly because bijn is not a constant but bijns is. The theory permutes is added into the OT theory hol-set.

Regards,

Chun Tian

[binghe]

In addition, due to old Slack discussions, I added a new theorem MIN_SET_THM' in pred_setTheory for doing inductions on MIN_SET of finite sets:

   [MIN_SET_THM']  Theorem (added)
      ⊢ (∀e. MIN_SET {e} = e) ∧
        ∀e s. s ≠ ∅ ⇒ MIN_SET (e INSERT s) = MIN e (MIN_SET s)

   [MIN_SET_THM]  Theorem (existing)
      ⊢ (∀e. MIN_SET {e} = e) ∧
        ∀s e1 e2.
          MIN_SET (e1 INSERT e2 INSERT s) = MIN e1 (MIN_SET (e2 INSERT s))

[binghe]

If any user code wants the "old" behavior of pairwise for a user-defined relation R, he can use pairwise (RC R) s instead, and in this way the distinctness of pair elements gets ignored. We can even define the following overload to have the old definition "back" but under a different name, e.g.:

Overload PAIRWISE = ``\R. pairwise (RC R)``

Thus the new definition seems more general than the old one. There seems no easy way to define the new pairwise on top of the old one.

[mn200]

Your last comment is backwards I think. If the HOL Light version with disjointness baked in is

pairwiseD R s <=> !x y. x IN s /\ y IN s /\ x <> y ==> R x y

and the other is

pairwiseN R s <=> !x y. x IN s /\ y IN s ==> R x y

Then we have

|- pairwiseD R = pairwiseN (RC R)

(the R on the right turns into the disjunction x = y \/ R x y; then negate the equality and move it to the left of the implication).

This suggests to me that we set up an overload for pairwiseD and keep the version in pred_set.

[binghe]

Hmmm… thanks for corrections. If the pairwise in topologyTheory were renamed to pairwiseD then there’s no need to move it to pred_setTheory. Let me close this PR for now.