Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
To: windley@edu.uidaho.cs.panther
Cc: Tom.Melham@uk.ac.cam.cl, info-hol@edu.uidaho.cs.ted
Subject: Re: mutual recursion
In-Reply-To: Your message of Sat, 25 Apr 92 11:07:26 -0700. <199204251807.AA00418@panther.cs.uidaho.edu>
Date: Sun, 26 Apr 92 14:31:20 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.744:26.03.92.13.31.26"@cl.cam.ac.uk>


In a private message from Phil Windley, he said:

> On Thu, 23 Apr 92 12:54:51 BST, Tom.Melham@cl.cam.ac.uk wrote:
> +------------
> | If there's sufficient interest, I could post a little example of
> | how to do a quick-and-dirty mutual recursive data type definition
> | "by hand"...
> 
> Hi Tom,
> 
> I think that this would be nice.  Until there is a built-in mutually
> recursive data type package, a small tutorial would save some time for
> those of us who want to use them.  
> 
> Cheers,
> 
> --phil--

Ok, attached is a small example (runs in version 2).
See also the Aarhus report.

Tom

=============================================================================

% ===================================================================== %
% Definition of mutually recursive data types:				% 
%									%
%     A = A1 | A2 B   and   B = B1 | B2 A				%
%									%
% T. Melham, 26 April 1992.						%
% ===================================================================== %

% --------------------------------------------------------------------- %
% Open a new theory.							%
% --------------------------------------------------------------------- %
new_theory `mutual`;;

% --------------------------------------------------------------------- %
% Define a big type with everything in it.				%
% --------------------------------------------------------------------- %
let R_Axiom =
    define_type `R_Axiom` `R = RA1 | RA2 R | RB1 | RB2 R`;;

let R_Induct = prove_induction_thm R_Axiom;;

% --------------------------------------------------------------------- %
% Now, we want to carve R into two disjoint sets, representing A and B. %
% We define two predicates ISA and ISB, such that they are true of well %
% formed representations of A and B respectively.  Do this by defining 	%
% a mapping f from R to num such that					%
%									%
%    f x = 1 iff x represents something in A				%
%    f x = 2 iff x represents something in B				%
%    f x = 0 otherwise							%
%									%
% Then ISA = \x. f x = 1 and ISB = \x. f x = 2.				%
% --------------------------------------------------------------------- %

let f_lemma =
    prove_rec_fn_exists R_Axiom
    "(f RA1 = 1) /\
     (f (RA2 r) = ((f r = 2) => 1 | 0)) /\
     (f RB1 = 2) /\
     (f (RB2 r) = ((f r = 1) => 2 | 0))";;

let ISA_ISB_lemma =
    PROVE
    ("?ISA ISB.
       (ISA RA1) /\ ~(ISB RA1) /\ 
       (!r. ISA (RA2 r) = ISB r) /\ (!r. ~ISB (RA2 r)) /\
       (ISB RB1) /\ ~(ISA RB1) /\
       (!r. ISB (RB2 r) = ISA r) /\ (!r. ~ISA (RB2 r))",
     X_CHOOSE_THEN "code:R->num" STRIP_ASSUME_TAC f_lemma THEN
     MAP_EVERY EXISTS_TAC ["\x:R. code x = 1";"\x:R. code x = 2"] THEN
     CONV_TAC (ONCE_DEPTH_CONV BETA_CONV) THEN
     ASM_REWRITE_TAC (map num_EQ_CONV ["1 = 2";"2 = 1"]) THEN
     REPEAT (GEN_TAC ORELSE CONJ_TAC)THEN COND_CASES_TAC THEN
     CONV_TAC (ONCE_DEPTH_CONV num_EQ_CONV) THEN
     REWRITE_TAC []);;

let ISA_ISB =
    new_specification `ISA_ISB` 
    [`constant`,`ISA`;`constant`,`ISB`] ISA_ISB_lemma;;

% --------------------------------------------------------------------- %
% Now, define the types A and B.					%
% --------------------------------------------------------------------- %

let A_EXISTS =
    PROVE ("?r. ISA r", EXISTS_TAC "RA1" THEN REWRITE_TAC [ISA_ISB]);;

let B_EXISTS =
    PROVE ("?r. ISB r", EXISTS_TAC "RB1" THEN REWRITE_TAC [ISA_ISB]);;

let A_DEF = 
    new_type_definition
    (`A`, "ISA", A_EXISTS);;

let B_DEF = 
    new_type_definition
    (`B`, "ISB", B_EXISTS);;

% --------------------------------------------------------------------- %
% Define representation and abstraction functions.			%
% --------------------------------------------------------------------- %

let REP_ABS_A =
    define_new_type_bijections
    `REP_ABS_A` `ABSA` `REPA` A_DEF;;

let REP_ABS_B =
    define_new_type_bijections
    `REP_ABS_B` `ABSB` `REPB` B_DEF;;

% --------------------------------------------------------------------- %
% We now define the constructors of A and B in the obvious way.		%
% --------------------------------------------------------------------- %

let A1_DEF =
    new_definition
    (`A1_DEF`, "A1 = ABSA RA1");;

let A2_DEF =
    new_definition
    (`A2_DEF`, "A2 b = ABSA (RA2(REPB b))");;

let B1_DEF =
    new_definition
    (`B1_DEF`, "B1 = ABSB RB1");;

let B2_DEF =
    new_definition
    (`B2_DEF`, "B2 a = ABSB (RB2(REPA a))");;

% --------------------------------------------------------------------- %
% Now to prove the characterizing theorem for A and B. For the 		%
% existence part, we define an auxiliary function on the underlying     %
% representation. It takes as arguments the things that will be 	%
% universally quantified outside the existential assertion in the final %
% theorem.  We return an element of the disjoint sum of the two types 	%
% in the final theorem.							%
% --------------------------------------------------------------------- %

let lemma =
    prove_rec_fn_exists R_Axiom
    "(fn x1 x2 f1 f2 RA1 = INL (x1:*)) /\ 
     (fn x1 x2 f1 f2 (RA2 x) = INL (f1 (OUTR(fn x1 x2 f1 f2 x)) (ABSB x))) /\ 
     (fn x1 x2 f1 f2 RB1 = INR (x2:**)) /\ 
     (fn x1 x2 f1 f2 (RB2 x) =  INR (f2 (OUTL(fn x1 x2 f1 f2 x)) (ABSA x)))";;

% --------------------------------------------------------------------- %
% A wee lemma for getting rid of quantifications over a pair-valued 	%
% variable.  This (or something like it) really ought to be built in.	%
% --------------------------------------------------------------------- %

let prod_Induct =
    PROVE
    ("!P. (!x:*. !y:**. P(x,y)) ==> !p. P p",
     REPEAT STRIP_TAC THEN
     PURE_ONCE_REWRITE_TAC [SYM (SPEC_ALL PAIR)] THEN
     FIRST_ASSUM MATCH_ACCEPT_TAC);;

% --------------------------------------------------------------------- %
% Important lemma: to prove 						%
%									%
%   |- (!a:A. P a) /\ (!b:B. Q b) 					%
%									%
% it suffices to prove							%
%									%
%   |- !r:R. (ISA r ==> P(ABSA r)) /\ (ISB r ==> Q(ABSB r))		%
%									%
% This lets us do a simultaneous induction over a:A and b:B via an 	%
% induction over r.							%
% --------------------------------------------------------------------- %

let re_lemma =
    PROVE
    ("!P Q. (!r:R. (ISA r ==> P(ABSA r)) /\ (ISB r ==> Q(ABSB r))) ==>
            ((!a:A. P a) /\ (!b:B. Q b))",
     REPEAT STRIP_TAC THENL
     [let thm1 = SPEC "a:A" (prove_abs_fn_onto REP_ABS_A) in
      CHOOSE_THEN (CONJUNCTS_THEN2 SUBST1_TAC MP_TAC) thm1;
      let thm2 = SPEC "b:B" (prove_abs_fn_onto REP_ABS_B) in
      CHOOSE_THEN (CONJUNCTS_THEN2 SUBST1_TAC MP_TAC) thm2] THEN
     ASM_REWRITE_TAC []);;


% --------------------------------------------------------------------- %
% Now for the theorem.  Since there isn't much built in support for 	%
% tupled quantification, we prove it first in this lemma form.  Note 	%
% that a library for tupled quantification (due to Jim Grundy) is on	%
% the way in version 2.01.  Meanwhile, we do this.			%
% --------------------------------------------------------------------- %

let lemma =
    PROVE
    ("!x1:*. !x2:**. !f1 f2.
      ?! p. let fn1 = FST p and fn2 = SND p in
             ((fn1 A1 = x1) /\ 
              (!b. fn1 (A2 b) = f1 (fn2 b) b) /\ 
              (fn2 B1 = x2) /\ 
              (!a. fn2 (B2 a) = f2 (fn1 a) a))",
     REPEAT GEN_TAC THEN
     PURE_ONCE_REWRITE_TAC [A1_DEF;A2_DEF;B1_DEF;B2_DEF] THEN
     CONV_TAC EXISTS_UNIQUE_CONV THEN CONJ_TAC THENL
     [STRIP_ASSUME_TAC lemma THEN
      let fn = fst(dest_exists(concl lemma)) in
      EXISTS_TAC 
       "(OUTL o (^fn x1 x2 f1 f2) o REPA),
        (OUTR o (^fn x1 x2 f1 f2) o REPB)" THEN
      CONV_TAC (ONCE_DEPTH_CONV let_CONV) THEN
      let rew1 = REWRITE_RULE [ISA_ISB] in
      let th1 = rew1 (SPEC "RA1" (CONJUNCT2 REP_ABS_A)) and
          th2 = rew1 (SPEC "RB1" (CONJUNCT2 REP_ABS_B)) in
      let rew2 = REWRITE_RULE [ISA_ISB;REP_ABS_B] in
      let th3 = rew2 (SPEC "RA2(REPB b)" (CONJUNCT2 REP_ABS_A)) in
      let rew3 = REWRITE_RULE [ISA_ISB;REP_ABS_A] in
      let th4 = rew3 (SPEC "RB2(REPA a)" (CONJUNCT2 REP_ABS_B)) in
      ASM_REWRITE_TAC [o_THM;th1;th2;OUTL;OUTR;th3;th4] THEN
      REWRITE_TAC [REP_ABS_A;REP_ABS_B];
      let ind = INDUCT_THEN prod_Induct (K ALL_TAC) in
      REPEAT (ind THEN GEN_TAC THEN GEN_TAC) THEN
      REWRITE_TAC [PAIR_EQ] THEN
      CONV_TAC (ONCE_DEPTH_CONV let_CONV) THEN
      STRIP_TAC THEN CONV_TAC (ONCE_DEPTH_CONV FUN_EQ_CONV) THEN
      let thm = SPECL ["\a:A. x a:* = x' a";"\b:B. y b:** = y' b"] re_lemma in
      MATCH_MP_TAC (CONV_RULE (ONCE_DEPTH_CONV BETA_CONV) thm) THEN
      INDUCT_THEN (R_Induct) STRIP_ASSUME_TAC THEN
      ASM_REWRITE_TAC [ISA_ISB] THENL
      [DISCH_TAC THEN RES_TAC THEN
       IMP_RES_THEN (SUBST1_TAC o SYM) REP_ABS_B THEN
       ASM_REWRITE_TAC [];
       DISCH_TAC THEN RES_TAC THEN
       IMP_RES_THEN (SUBST1_TAC o SYM) REP_ABS_A THEN
       ASM_REWRITE_TAC []]]);;

% --------------------------------------------------------------------- %
% Exercise for the reader: convert the theorem into the following 	%
% nice form.  								%
%									%
% |- !x1:*. !x2:**. !f1 f2.						%
%      ?!(fn1,fn2).							%
%         ((fn1 A1 = x1) /\ 						%
%          (!b. fn1 (A2 b) = f1 (fn2 b) b) /\ 				%
%          (fn2 B1 = x2) /\ 						%
%          (!a. fn2 (B2 a) = f2 (fn1 a) a))				%
%									%
% Note: this will be MUCH easier when the tupled abstraction and 	%
% quantification library is installed.					%
% --------------------------------------------------------------------- %