Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Thu, 28 Jan 1993 08:24:14 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11847;
          Wed, 27 Jan 93 20:25:10 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Killer.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA11842;
          Wed, 27 Jan 93 20:25:04 -0800
Received: by makaha.cs.ucla.edu (Sendmail 5.61a+YP/2.27) id AA26674;
          Wed, 27 Jan 93 20:24:38 -0800
Date: Wed, 27 Jan 93 20:24:38 -0800
From: toal@EDU.UCLA.CS (Ray J. Toal)
Message-Id: <9301280424.AA26674@makaha.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: More on mutually inductively defined relations



%<

Here is a slightly different formulation of the mutually inductively defined
relations example Tom Melham posted earlier.  Logically it is the same, of
course; the only difference is that here we define

  Even n = !P Q. Closed P Q ==> P n                           (1)
  Odd n  = !P Q. Closed P Q ==> Q n                         

instead of

  Even n = !P. (?Q. Closed P Q) ==> P n                       (2)
  Odd n  = !Q. (?P. Closed P Q) ==> Q n                     

which appears a bit more symmetric.  By the way it is trivial to prove
(1) = (2).

>%


new_theory `mut2`;;

let Closed_DEF =
  new_definition
    (`Closed`,
    "Closed P Q = 
      P 0 /\
      (!n. Q n ==> P (n+1)) /\
      Q 1 /\
      (!n. P n ==> Q (n+1))");;

let Even_DEF = 
  new_definition
    (`Even`,
    "Even n = !P Q. Closed P Q ==> P n");;

let Odd_DEF = 
  new_definition
    (`Odd`,
    "Odd n = !P Q. Closed P Q ==> Q n");;

let Even0 =
  PROVE
    ("Even 0",
    REWRITE_TAC [Even_DEF;Closed_DEF] THEN REPEAT STRIP_TAC);;

let Even_Odd =
  PROVE
    ("!n. Even n ==> Odd (n+1)",
     REWRITE_TAC [Closed_DEF;Even_DEF;Odd_DEF] THEN
     REPEAT STRIP_TAC THEN
     RES_TAC THEN
     RES_TAC);;
  
let Odd1 =
  PROVE
    ("Odd 1",
     REWRITE_TAC [Odd_DEF;Closed_DEF] THEN REPEAT STRIP_TAC);;

let Odd_Even =
  PROVE
    ("!n. Odd n ==> Even (n+1)",
     REWRITE_TAC [Even_DEF;Odd_DEF;Closed_DEF] THEN
     REPEAT STRIP_TAC THEN 
     RES_TAC THEN
     RES_TAC);;

let Rule_Induction1 =
  PROVE 
    ("!P Q. Closed P Q ==> !n. Even n ==> P n",
     REWRITE_TAC [Even_DEF;Closed_DEF] THEN
     REPEAT STRIP_TAC THEN
     RES_TAC);;

let Rule_Induction2 =
  PROVE
    ("!P Q. Closed P Q ==> !n. Odd n ==> Q n",
     REWRITE_TAC [Odd_DEF] THEN
     REPEAT STRIP_TAC THEN
     RES_TAC);;

let Rule_Induction =
  PROVE
    ("!P Q. Closed P Q ==> (!n. Even n ==> P n) /\ (!n. Odd n ==> Q n)",
     REWRITE_TAC [Closed_DEF;Odd_DEF;Even_DEF] THEN
     REPEAT STRIP_TAC THEN
     RES_TAC);;

%
Ray Toal
%