1 Proving Results from the paper Nachum Dershowitz: Tripartite Unions

The paper starts with Theorems 1 and 2, and then proves Theorem 3 which is a considerable improvement of Theorems 1 or 2. We start with Theorem 3, which we call wfp tri

It appears that all Dershowitz’s results in the paper assume that A, B and C are well-founded.

As a preliminary, it should be noted that

– in Isabelle, a relation R is well-founded if there is not an infinite decreasing sequence

… <_{R} x_{n} <_{R} x_{n−1} <_{R} … <_{R} x_{1} <_{R} x_{0}

where x <_{R} y means (x, y) ∈ R, and

– in Isabelle, the composition of relations R and S is defined by

R ◯ S = {(x, z).∃y.(x, y) ∈ S&(y, z) ∈ R}

rel_comp_def:
  "?r O ?s == {(x, z). EX y. (x, y) : ?s & (y, z) : ?r}"

Since both of these conventions are the opposite of those used by Dershowitz, which means that his theorems look the same as ours. If just one were different from his usage we would have to reverse the order of relation composition to make his theorems look like ours.

We use dvk cond R A, the condition from Doornbos & von Karger [1], that R ◯ A ⊆ (A ◯ (A ∪ R)^{∗}) ∪ R

dvk_cond_def':
  "dvk_cond ?s ?r == ?s O ?r <= (?r O (?r Un ?s)^*) Un ?s"

We next reproduce Dershowitz’s Theorem 3, [2, Thm 3]

Theorem 1 (wf tri', Dershowitz, Theorem 3). If A, B and C are well-founded, and the following hold:

(a) (B ∪ C) ◯ A ⊆ (A ◯ (A ∪ B ∪ C)^{∗}) ∪ (B ∪ C)

(b) C ◯ B ⊆ (A ◯ (A ∪ B ∪ C)^{∗}) ∪ (B ◯ B^{∗}) ∪ C

then A ∪ B ∪ C is well-founded.

wf_tri':
   "[| ?BC = ?B Un ?C; dvk_cond ?BC ?A;
    ?C O ?B <= (?A O (?A Un ?BC)^*) Un (?B O ?B^*) Un ?C;
    wf ?A; wf ?B; wf ?C |] ==> wf (?A Un ?BC)"

We separate Dershowitz’s proof into a number of lemmas. Note how, generally, statements in the proof of the form “there exists an infinite chain” have to be translated into a lemma with hypotheses and conclusion that certain relations are well-founded, or that something is in the wellfounded part or a relation.

The well-founded part (wfp in Isabelle) of a relation is the set whose elements are not the head of any infinite descending chain. So a relation is well-founded if and only if every member of the underlying set is in its well-founded part.

Following Dershowitz, we say an R-immortal element is the head of an infinite descending chain in R, and “immortal” means A∪R-immortal, or A ∪ B ∪ C-immortal, as the case may be.

NEW Define R^{−} to be R, but excluding steps of the form (w, z) where there exists some y such that (y, z) ∈ A and y is A ∪ R-immortal.

Lemma 1 (wfp tri lem ch). ORIGINAL If there is an infinite descending A∪R-chain then there is an infinite descending A∪R-chain where each step (w, z) ∈ R in that chain has the property that there is no (y, z) ∈ A such that y is the head of an infinite descending A ∪ R-chain.

CONTRAPOSITIVE If A ∪ R^{−} is well-founded then A ∪ R is wellfounded.

Proof. You construct an infinite descending A ∪ R-chain using A where possible and using R only where necessary.

The (forward) image r“s of a set s under a relation r is the containing those y such that x ∈ s and (x, y) ∈ r.

Image_def: "?r `` ?s == {y. EX x:?s. (x, y) : ?r}"
wfp_tri_lem_ch:
   "?x : wfp (?A Un ?R Int {(y, z). z ~: ?A `` (- wfp (?A Un ?R))})
      ==> ?x : wfp (?A Un ?R)"

Lemma 2 (wfp tri lem dvk). ORIGINAL If R and A satisfy the Doornbos & von Karger [1] condition dvk cond, and A is well-founded, and there is an infinite descending A ∪ R-chain, then there is an infinite descending R-chain whose members are not of the form z where (y, z) ∈ A and y is immortal, ie is the head of an infinite descending A ∪ R-chain.

CONTRAPOSITIVE If R and A satisfy the Doornbos & von Karger [1] condition dvk cond, and A and R^{−} (defined before Lemma 1) are well-founded, then A ∪ R is well-founded.

We first give a more intuitive proof, then a proof which more closely approximates the Isabelle proof.

Proof. Consider an infinite descending A∪R-chain. As A is well-founded, from any point in this chain there must be another R-step. Wherever possible replace a R-step z >_{R} v followed by an A-step v >_{A} u by an Astep (possibly followed by a number of A- or R-steps) in the given chain. (This relates to the part R ◯ A ⊆ (A ◯ (A ∪ R)^{∗}) ∪ … of dvk cond). Alternatively, if possible, replace the remainder of the chain from this point by any other infinite chain z >_{A} y >_{A∪R} . . .. Again, this will not always be possible since A is well-founded.

So, where this is not possible, we can replace a R-step followed by an A-step by a single R-step, which is possible using the part R◯A ⊆ …∪R

of dvk cond.

Doing this repeatedly could absorb any number of A-steps, but, again, as A is well-founded there cannot be infinitely many such A-steps, so eventually we reach another R-step. Repeating this gives the required infinite R-chain, with the given property.

This next proof approximates more closely to the Isabelle proof.

Proof. Assume that A is well-founded. Define R^{−} to be R, but excluding steps of the form (w, z) where there exists some y such that (y, z) ∈ A and y is immortal. Assume that R^{−} is well-founded.

Suppose that there is an infinite descending A ∪ R-chain. Choose a head z of such a chain, choosing z to be A-minimal, and also to be R^{−}- minimal among A-minimal immortal elements. As z is A-minimal, the first step of an infinite chain must be (say) (y, z) ∈ R, and also in fact (y, z) ∈ R^{−}. As A is well-founded, let y be A-minimal among possible choices for y. Then, by the R^{−}-minimality of z, although y is immortal, it is not A-minimal among immortal members. So we have (x, y) ∈ A, where x is immortal. So as R ◯ A ⊆ (A ◯ (A ∪ R)^{∗}) ∪ R, we could replace z >_{R} y >_{A} x in the infinite chain by

– (x, z) ∈ A ◯ (A ∪ R)^{∗}, say (x, y′) ∈ (A ∪ R)^{∗} and (y′, z) ∈ A (where x, y′ and z are immortal), but this would contradict the A-minimality of z (and our consequent inference that (y, z) ∉ A), or – (x, z) ∈ R, which would contradict our choice of y which was to be

A-minimal, since x could have been chosen instead of y.

Thus, either way we get a contradiction, so A ∪ R is well-founded.

wfp_tri_lem_dvk:
   "[| dvk_cond ?R ?A; wf ?A;
         wf (?R Int {(y, z). z ~: ?A `` (- wfp (?A Un ?R))}) |]
      ==> ?x : wfp (?A Un ?R)"

Define C^{−} to be C, but excluding steps of the form (w, z) where there exists some y such that (y, z) ∈ A and y is X ∪ B ∪ C-immortal.

For the purposes of Theorem 1 X will be A, but we will use the lemma with more general X when there are four or more relations.

Lemma 3 (wf tri lem BCm). If B and C^{−} (using the definition of C^{−} just above) are well-founded, and condition (b) of Theorem 1 is satisfied, then B ∪ C^{−} is well-founded.

Proof. Assume that B and C^{−} are well-founded.

Suppose, contrary to the lemma, that B ∪ C^{−} is not well-founded. So there exists an B ∪ C^{−}-immortal z. Choose z to be B-minimal such, and also to be C^{−}-minimal among possible B-minimal choices.

As z is B-minimal, the first step of an infinite B ∪ C^{−}-chain must be (say) (y, z) ∈ C^{−}. As B is well-founded, let y be B-minimal among possible choices for y. Then, by the C^{−}-minimality of z, although y is B ∪C^{−}-immortal, it is not B-minimal among B ∪C^{−}-immortal members. So we have (x, y) ∈ B, where x is B ∪ C^{−}-immortal. So as C ◯ B ⊆ (A ◯ (X ∪ B ∪ C)^{∗}) ∪ (B ◯ B^{∗}) ∪ C, we could replace z >_{C} y >_{B} x in the infinite chain by

– (x, z) ∈ A◯(X ∪B ∪C)^{∗}, say (x, y′) ∈ (X ∪B ∪C)^{∗} and (y′, z) ∈ A — but x is B ∪C^{−}-immortal, and so is the head of an infinite descending X ∪ B ∪ C-chain, contradicting that (y, z) ∈ C^{−},

– (x, z) ∈ B ◯ B^{∗}, which would contradict our choice of z to be Bminimal

– (x, z) ∈ C (and so (x, z) ∈ C^{−}) which would contradict our choice of y to be B-minimal, since x could have been chosen instead of y.

Thus, in each case we get a contradiction, so B ∪ C^{−} is well-founded.

wf_tri_lem_BCm:
  "[| ?BC = ?B Un ?C; ?C O ?B <= (?A O (?X Un ?BC)^*) Un (?B O ?B^*) Un ?C;
     wf ?B; wf (?C Int {(y, z). z ~: ?A `` (- wfp (?X Un ?BC))}) |] ==>
   wf (?B Un ?C Int {(y, z). z ~: ?A `` (- wfp (?X Un ?BC))})"

Proof. (of Theorem 1) By Lemma 2 it is enough to prove that (B ∪ C)^{−} is well-founded. By Lemma 3 we have that B ∪ C^{−} is well-founded, and clearly (B ∪ C)^{−} ⊆ B ∪ C^{−}.

Now we show how to extend this result to four (or more) relations.

Theorem 2 (wf four). If A, B, C and D are well-founded, and the following hold:

(a) (B ∪ C ∪ D) ◯ A ⊆ (A ◯ (A ∪ B ∪ C ∪ D)^{∗}) ∪ (B ∪ C ∪ D)

(b) D ◯ C ⊆ (A ◯ (A ∪ B ∪ C ∪ D)^{∗}) ∪ (C ◯ C^{∗}) ∪ D

(c) (C ∪ D) ◯ B ⊆ (A ◯ (A ∪ B ∪ C ∪ D)^{∗}) ∪ (B ◯ B^{∗}) ∪ C ∪ D

then A ∪ B ∪ C ∪ D is well-founded.

val wf_four =
   "[| ?uall = ?A Un ?B Un ?C Un ?D; dvk_cond (?B Un ?C Un ?D) ?A;
       ?D O ?C <= (?A O ?uall^*) Un (?C O ?C^*) Un ?D;
       ?C Un ?D O ?B <= (?A O ?uall^*) Un (?B O ?B^*) Un (?C Un ?D);
       wf ?A; wf ?B; wf ?C; wf ?D |] ==> wf ?uall"

Proof. We adapt the previous definition of R^{−} for a relation R: R^{−} is R, but excluding steps of the form (w, z) where there exists some y such that (y, z) ∈ A and y is A ∪ B ∪ C ∪ D-immortal.

As D is well-founded, a fortiori D^{−} is well-founded.

Therefore by Lemma 3 (setting A, X, B, C to A, A ∪ B, C, D) and condition (b) C ∪ D^{−} is well-founded, and so a fortiori (C ∪ D)^{−} is wellfounded.

Then, by Lemma 3 (setting A, X, B, C to A, A, B, C∪D) and condition

(c) B ∪ (C ∪ D)^{−} is well-founded and so a fortiori (B ∪ C ∪ D)^{−} is wellfounded.

Then, by Lemma 2 A ∪ B ∪ C ∪ D is well-founded.

We now extend this result to an arbitrary number of relations. The proof is straightforward but we need to set up some definitions.

First the condition we call tri cond, which is the condition satisfied by the list [B, C, D] in the case of four relations. It is defined recursively and gives (for example) conditions b and c of Theorem 2.

tri_cond_Nil : "tri_cond ?Auall [] = True"
tri_cond_Cons : "tri_cond ?Auall (?B # ?Bs) =
   ((let uBs = foldr op Un ?Bs {}
     in uBs O ?B <= ?Auall Un (?B O ?B^*) Un uBs) & tri_cond ?Auall ?Bs)"

We then need a separate lemma which is proved by structural induction on the list, say [B, C, D], of relations. For the general case we work with a list B_{1}, B_{2}, …, B_{n}.

Define U^{−} to be U, but excluding steps of the form (w, z) where there exists some y such that (y, z) ∈ A and y is X ∪ U-immortal.

Lemma 4. Suppose B_{1}, B_{2}, …, B_{n} are all well-founded, and let U = B_{1}∪B_{2}∪…∪B_{n}. Suppose the condition tri cond (A◯(X∪U)[B_{1}, B_{2}, …, B_{n}] holds. Then U^{−} is well-founded.

tri_n_lem : "[| ?uBs = foldr op Un ?Bs {}; ?Auall = ?A O (?X Un ?uBs)^*;
      tri_cond ?Auall ?Bs; Ball (set ?Bs) wf |] ==>
      wf (?uBs Int {(y, z). z ~: ?A `` (- wfp (?X Un ?uBs))})"

Proof. The proof is by structural induction on the list [B_{1}, B_{2}, …, B_{n}], and each step is proved using Lemma 3. The value used for X varies throughout, so if its final value is X_{f}, then the lemma is proved successively for

[]  X = X_{f} ∪ B_{1} ∪ B_{2} ∪ … ∪ B_{n}
[B_{n}]  X = X_{f} ∪ B_{1} ∪ B_{2} ∪ … ∪ B_{n−1}
⋮  ⋮
[B_{2}, …, B_{n}]  X = X_{f} ∪ B_{1}
[B_{1}, B_{2}, …, B_{n}]  X = X_{f}

Note that the value of X ∪ U (as used in the definition of U^{−} above) therefore remains unchanged, and that at each step we also use, in addition to Lemma 3, the fact that if B ∪ V^{−} is well-founded, then (B ∪ V)^{−} is well-founded.

Then we have the following theorem.

Theorem 3. Suppose A and B_{1}, B_{2}, …, B_{n} are all well-founded, and let U = B_{1} ∪ B_{2} ∪ … ∪ B_{n}. Suppose the condition tri cond (A ◯ (A ∪ U)[B_{1}, B_{2}, …, B_{n}] holds, and that U ◯ A ⊆ (A ◯ (A ∪ U)^{∗}) ∪ U Then A ∪ U is well-founded.

tri_n "[| ?uBs = foldr op Un ?Bs {}; ?Auall = ?A O (?A Un ?uBs)^*;
  dvk_cond ?uBs ?A; tri_cond ?Auall ?Bs; wf ?A; Ball (set ?Bs) wf |]
==> wf (?A Un ?uBs)"

Proof. By Lemma 4 we get that U^{−} is well-founded, where we use X = A in the definition of U^{−}. Then Lemma 2 gives the result.

References

1. Henk Doornbos & Burghard Von Karger. On the Union of Well-Founded Relations. L. J. of the IGPL 6 (1998), 195-201.

2. Nachum Dershowitz. Tripartite Unions. preprint