#|
Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Computational Logic, Inc. PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT
IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Computational Logic, Inc. BE LIABLE TO YOU FOR ANY DAMAGES,
ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#
;; Matt Kaufmann
;; Koenig Tree Lemma events supporting ``An Extension of the
;; Boyer-Moore Theorem Prover to Support First-Order Quantification,''
;; to appear in JAR (1992?).  The DEFN-SK events have been replaced by
;; DCLs and ADD-AXIOMs, as shown.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Koenig's Lemma Events List
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; All this initial stuff is just to get the CONSTRAIN below accepted.

Event: Start with the initial nqthm theory.

Definition: ones (n) = if n ≃ 0 then nil

else cons (1, ones (n − 1)) endif Definition: all-ones (s) = if listp (s) then (car (s) = 1) ∧ all-ones (cdr (s))

else s = nil endif

Definition: length (s) = if listp (s) then 1 + length (cdr (s))

else 0 endif

Definition: subseq (s1 , s2 ) = if s1 = s2 then t

elseif s2 ≃ nil then f

else subseq (s1 , cdr (s2 )) endif

Theorem: subseq-all-ones (all-ones (s1 ) ∧ subseq (s2 , s1 )) → all-ones (s2 )

Definition: plistp (s) = if listp (s) then plistp (cdr (s))

else s = nil endif

Theorem: plistp-all-ones all-ones (s) → plistp (s)

Theorem: all-ones-ones all-ones (ones (n))

Theorem: ones-is-injective ((i ∈ N) ∧ (j ∈ N) ∧ (i ≠ j )) → (ones (i) ≠ ones (j ))

Conservative Axiom: koenig-intro node-p (nil) ∧ (truep (node-p (s)) ∨ falsep (node-p (s))) ∧ (node-p (s)

→ (node-p (cons (n, s)) = ((0 < n) ∧ (succard (s) ≮ n)))) ∧ ((node-p (s1 ) ∧ subseq (s, s1 )) → node-p (s)) ∧ node-p (s-n (n)) ∧ (((i ∈ N) ∧ (j ∈ N) ∧ (i ≠ j )) → (s-n (i) ≠ s-n (j ))) ∧ ((¬ plistp (s)) → (¬ node-p (s)))

Simultaneously, we introduce the new function symbols node-p, succard, and s-n.

;; We want to define a function s-height which returns an element of a given height.
;; The next several events culminate in the following lemma:
;; (prove-lemma length-s-height (rewrite)
;;   (equal (length (s-height n)) (fix n)))

Definition: succ-aux (s, n) = if n ≃ 0 then nil

else cons (cons (n, s), succ-aux (s, n − 1)) endif

Definition: successors (s) = succ-aux (s, succard (s))

Definition: successors-list (ss) = if listp (ss)

then append (successors (car (ss)), successors-list (cdr (ss)))

else nil endif

Definition: level (n) = if n ≃ 0 then list (nil)

else successors-list (level (n − 1)) endif

Definition: init-tree (n) = if n ≃ 0 then list (nil)

else append (level (n), init-tree (n − 1)) endif

Definition: remove1 (a, x) = if listp (x)

then if a = car (x) then cdr (x)

else cons (car (x), remove1 (a, cdr (x))) endif else x endif

Theorem: length-remove1 (a ∈ x) → (length (remove1 (a, x)) < length (x))

Definition: first-non-member-index (i, x) = if s-n (i) ∈ x then first-non-member-index (1 + i, remove1 (s-n (i), x))

else i endif Definition: nthcdr (n, s) = if n ≃ 0 then s

else nthcdr (n − 1, cdr (s)) endif

Definition: s-height (n) = nthcdr (length (s-n (first-non-member-index (0, init-tree (n)))) − n,

s-n (first-non-member-index (0, init-tree (n))))

Theorem: nthcdr-subseq (length (s) ≮ n) → subseq (nthcdr (n, s), s)

Theorem: node-p-nthcdr (node-p (s) ∧ (length (s) ≮ n)) → node-p (nthcdr (n, s))

Theorem: lessp-difference-1 (x < (x − n)) = f

Theorem: node-p-s-height node-p (s-height (n))

Theorem: length-nthcdr length (nthcdr (n, s)) = (length (s) − n)

Theorem: first-non-member-index-lessp first-non-member-index (i, x) ≮ i

Theorem: s-n-first-non-member-index-not-equal (i ∈ N) → (s-n (first-non-member-index (1 + i, remove1 (s-n (i), x))) ≠ s-n (i))

Theorem: member-remove1 (a ≠ b) → ((a ∈ remove1 (b, x)) = (a ∈ x))

Theorem: s-n-first-non-member-index (i ∈ N) → (s-n (first-non-member-index (i, x)) ∉ x)

Theorem: member-append (a ∈ append (x, y)) = ((a ∈ x) ∨ (a ∈ y))

Theorem: member-cons-succ-aux (cons (z, v) ∈ succ-aux (v, n)) = ((0 < z) ∧ (n ≮ z))

Theorem: node-p-cons-lemma (¬ node-p (s)) → (¬ node-p (cons (n, s)))

Theorem: node-p-cons node-p (cons (n, s)) = (node-p (s) ∧ (0 < n) ∧ (succard (s) ≮ n))

Definition: all-length-n (ss, n) = if listp (ss) then (length (car (ss)) = n)

∧ all-length-n (cdr (ss), n)

else t endif

Theorem: all-length-n-append all-length-n (append (ss1 , ss2 ), n) = (all-length-n (ss1 , n) ∧ all-length-n (ss2 , n))

Theorem: all-length-n-succ-aux (length (s) = n) → all-length-n (succ-aux (s, k), 1 + n)

Theorem: all-length-n-successors-list all-length-n (ss, n) → all-length-n (successors-list (ss), 1 + n)

Theorem: length-0 (length (s) = 0) = (s ≃ nil)

Definition: member-level-induction (s, n) = if n ≃ 0 then t

else member-level-induction (cdr (s), n − 1) endif

Theorem: succ-aux-listp (¬ listp (s)) → (s ∉ succ-aux (z, n))

Theorem: successors-list-listp (¬ listp (s)) → (s ∉ successors-list (ss))

Theorem: member-succ-aux (s ∈ succ-aux (x, n)) → (cdr (s) = x)

Theorem: member-successors-list-successors-list-witness (s ∈ successors-list (ss)) = ((cdr (s) ∈ ss) ∧ (s ∈ successors (cdr (s))))

Theorem: member-level ((n ∈ N) ∧ node-p (s)) → ((s ∈ level (n)) = (length (s) = n))

Theorem: member-init-tree node-p (s) → ((s ∈ init-tree (n)) = (n ≮ length (s)))

Theorem: length-s-non-member-index (i ∈ N) → (n < length (s-n (first-non-member-index (i, init-tree (n)))))

Theorem: length-s-height length (s-height (n)) = fix (n)

Event: Disable s-height.

;; End of s-height excursion.
;; Our goal:
;(prove-lemma konig-tree-lemma nil
;  (and (node-p (k n))
;       (implies (not (lessp j i))
;                (subseq (k i) (k j)))
;       (equal (length (k n)) (fix n))))
#| The original DEFN-SK event here was processed as follows:
>(defn-sk inf (s)
  ;; says that s has arbitrarily high successors
  (forall big-h (exists big-s
    (and (subseq s big-s)
         (node-p big-s)
         (lessp big-h (length big-s))))))

Adding the Skolem axiom:
      (AND (IMPLIES (AND (SUBSEQ S BIG-S)
                         (NODE-P BIG-S)
                         (LESSP (BIG-H S) (LENGTH BIG-S)))
                    (INF S))
           (IMPLIES (NOT (AND (SUBSEQ S (BIG-S BIG-H S))
                              (NODE-P (BIG-S BIG-H S))
                              (LESSP BIG-H
                                     (LENGTH (BIG-S BIG-H S)))))
                    (NOT (INF S)))).

     As this is a DEFN-SK we can conclude that:
      (OR (TRUEP (INF S)) (FALSEP (INF S)))
is a theorem.

[ 0.2 0.0 0.0 ]
INF
>
|#

Event: Introduce the function symbol inf of one argument.

Event: Introduce the function symbol big-h of one argument.

Event: Introduce the function symbol big-s of 2 arguments.

Axiom: inf-intro ((subseq (s, big-s) ∧ node-p (big-s) ∧ (big-h (s) < length (big-s))) → inf (s)) ∧ ((¬ (subseq (s, big-s (big-h, s))

∧ node-p (big-s (big-h, s))

∧ (big-h < length (big-s (big-h, s))))) → (¬ inf (s)))

Axiom: inf-boolean truep (inf (s)) ∨ falsep (inf (s))

;; The following three events were generated mechanically.  They are
;; useful especially for applying the Skolem axioms for INF inside the
;; proof-checker, via the macro command SK*.

Event: Disable inf-intro.

Theorem: inf-suff (subseq (s, big-s) ∧ node-p (big-s) ∧ (big-h (s) < length (big-s))) → inf (s)

Theorem: inf-necc (¬ (subseq (s, big-s (big-h, s))

∧ node-p (big-s (big-h, s))

∧ (big-h < length (big-s (big-h, s))))) → (¬ inf (s))

Definition: next (s, max) = if max ≃ 0 then cons (0, s)

elseif inf (cons (max, s)) then cons (max, s)

else next (s, max − 1) endif

;; We want to show that NEXT gives us a successor with infinitely many
;; successors.
; INF-IMPLIES-INF-NEXT:
;(implies (and (node-p s)
;             (inf s))
;        (inf (next s (succard s))))
;; Note that if some successor of s has infinitely many successors, so
;; does (NEXT S (SUCCARD S)).  This is the lemma
;; INF-CONS-IMPLIES-INF-NEXT below.  But first note:

Theorem: inf-implies-node-p inf (s) → node-p (s)

Theorem: not-inf-zerop (i ≃ 0) → (¬ inf (cons (i, s)))

Theorem: inf-cons-implies-inf-next (node-p (s) ∧ inf (cons (i, s)) ∧ (n ≮ i)) → inf (next (s, n))

;; Our goal now is to apply this lemma by proving that
;; (inf (cons i s)) for some i <= (succard s).

Definition: all-big-h (s, n) = if n ≃ 0 then 1 + length (s)

else big-h (cons (n, s)) + all-big-h (s, n − 1) endif

Theorem: all-big-h-length length (s) < all-big-h (s, n)

Theorem: all-big-h-lessp ((0 < i) ∧ (n ≮ i)) → ((big-h (cons (i, s)) < all-big-h (s, n)) = t)

;; Here's a function which tells us which way s first branches on its
;; way to extending to s1.

Definition: first-branch (s, s1 ) = if s = cdr (s1 ) then car (s1 )

elseif s1 ≃ nil then 0

else first-branch (s, cdr (s1 )) endif

Theorem: subseq-cons-first-branch (subseq (s, x) ∧ (s ≠ x)) → subseq (cons (first-branch (s, x), s), x)

Theorem: length-non-equal (length (x) < length (y)) → ((x = y) = f)

Theorem: first-branch-ok-for-succard (subseq (s, big-s) ∧ node-p (big-s) ∧ (s ≠ big-s)) → ((first-branch (s, big-s) ∈ N)

∧ (0 < first-branch (s, big-s))

∧ (succard (s) ≮ first-branch (s, big-s)))

Theorem: all-big-h-lessp-linear ((0 < i) ∧ (succard (s) ≮ i)) → (big-h (cons (i, s)) < all-big-h (s, succard (s)))

Event: Disable all-big-h-lessp.

Theorem: inf-implies-inf-next (node-p (s) ∧ inf (s)) → inf (next (s, succard (s)))

Definition: k (n) = if n ≃ 0 then nil

else next (k (n − 1), succard (k (n − 1))) endif

Theorem: subseq-nil subseq (nil, x) = plistp (x)

Theorem: node-p-implies-plistp node-p (s) → plistp (s)

Theorem: inf-nil inf (nil)

Event: Disable node-p-implies-plistp.

Theorem: konig-tree-lemma-1 inf (k (n))

Theorem: length-next inf (x) → (length (next (s, n)) = (1 + length (s)))

Theorem: konig-tree-lemma-2 length (k (n)) = fix (n)

Theorem: subseq-next subseq (s1 , s2 ) → subseq (s1 , next (s2 , n))

Theorem: konig-tree-lemma-3 (j ≮ i) → subseq (k (i), k (j ))

Theorem: konig-tree-lemma node-p (k (n)) ∧ ((j ≮ i) → subseq (k (i), k (j ))) ∧ (length (k (n)) = fix (n))

;; or, if one prefers:

Theorem: konig-tree-lemma-again (n ∈ N) → (node-p (k (n))

∧ ((j ≮ i) → subseq (k (i), k (j ))) ∧ (length (k (n)) = n))

Index

all-big-h, 8, 9 all-big-h-length, 8 all-big-h-lessp, 8 all-big-h-lessp-linear, 9 all-length-n, 5 all-length-n-append, 5 all-length-n-succ-aux, 5 all-length-n-successors-list, 5 all-ones, 2 all-ones-ones, 2

big-h, 7–9 big-s, 7

first-branch, 9 first-branch-ok-for-succard, 9 first-non-member-index, 3, 4, 6 first-non-member-index-lessp, 4

inf, 7–10 inf-boolean, 7 inf-cons-implies-inf-next, 8 inf-implies-inf-next, 9 inf-implies-node-p, 8 inf-intro, 7 inf-necc, 7 inf-nil, 9 inf-suff, 7 init-tree, 3–6

k, 9, 10 koenig-intro, 2 konig-tree-lemma, 10 konig-tree-lemma-1, 9 konig-tree-lemma-2, 10 konig-tree-lemma-3, 10 konig-tree-lemma-again, 10

length, 2–10 length-0, 5 length-next, 10 length-non-equal, 9 length-nthcdr, 4 length-remove1, 3 length-s-height, 6 length-s-non-member-index, 6 lessp-difference-1, 4 level, 3, 5

member-append, 4

member-cons-succ-aux, 4

member-init-tree, 5 member-level, 5 member-level-induction, 5 member-remove1, 4 member-succ-aux, 5 member-successors-list-successo

rs-list-witness, 5

next, 8–10

node-p, 2, 4, 5, 7–10

node-p-cons, 5

node-p-cons-lemma, 4 node-p-implies-plistp, 9 node-p-nthcdr, 4 node-p-s-height, 4 not-inf-zerop, 8 nthcdr, 4 nthcdr-subseq, 4

ones, 1, 2

ones-is-injective, 2

plistp, 2, 9

plistp-all-ones, 2

remove1, 3, 4

s-height, 4, 6 s-n, 2–4, 6 s-n-first-non-member-index, 4 s-n-first-non-member-index-not-eq

ual, 4 subseq, 2, 4, 7, 9, 10 subseq-all-ones, 2 subseq-cons-first-branch, 9 subseq-next, 10 subseq-nil, 9 succ-aux, 3–5 succ-aux-listp, 5 succard, 2, 3, 5, 9 successors, 3, 5 successors-list, 3, 5 successors-list-listp, 5