Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Fri, 22 Jan 1993 14:36:14 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA21719; Fri, 22 Jan 93 06:15:30 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA21714; Fri, 22 Jan 93 06:15:17 -0800 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Fri, 22 Jan 1993 14:14:31 +0000 To: info-hol@edu.uidaho.cs.ted Cc: Tom.Melham@uk.ac.cam.cl Subject: Mutually Inductive Definitions. Date: Fri, 22 Jan 93 14:14:24 +0000 From: Tom Melham Message-Id: <"swan.cl.ca.398:22.01.93.14.14.39"@cl.cam.ac.uk> How to do Mutually Inductively-defined Relations in HOL. ======================================================== I occasionally get asked about extending my tools for inductive relation definitions to handle sets of mutually defined relations. I'm afraid I will probably not get around to extending the tools myself, so I thought I'd post this little example to help anyone who might want to do such a construction "by hand". It should, in fact, be fairly straightforward to extend my current code to deal with mutually inductive definitions. Any volunteers? Tom % ===================================================================== % % EXAMPLE (runs in HOL88 version 2.01) % % ===================================================================== % new_theory `mut`;; % --------------------------------------------------------------------- % % We wish to define two predicates on the natural numbers, namely Even % % and Odd. These are defined inductively by the following rules: % % % % Odd n Even n % % -------- ------------- -------- ------------ % % Even 0 Even (n+1) Odd 1 Odd (n+1) % % % % In HOL, we can simply make the usual "impredicative" definitions of % % these predicates. We express the closure under these rules of an % % arbitrary pair of sets P and Q as follows: % % % % "P 0 /\ (!n. Q n ==> P (n+1)) /\ Q 1 /\ !n. P n ==> Q (n+1)" % % % % and then define Even to be the intersection of all sets P for which % % there is a Q such that P and Q are closed under the rules. The set % % Odd is defined in the analgous way. % % --------------------------------------------------------------------- % let PQclosed = "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:num->bool. (?Q:num->bool. ^PQclosed) ==> P n");; let Odd_DEF = new_definition (`Odd`, "Odd n = !Q:num->bool. (?P:num->bool. ^PQclosed) ==> Q n");; % --------------------------------------------------------------------- % % We can now prove from the impredicative definitions of Even and Odd % % that the rules do indeed hold of these sets. % % --------------------------------------------------------------------- % let Even0 = PROVE ("Even 0", PURE_ONCE_REWRITE_TAC [Even_DEF] THEN REPEAT STRIP_TAC);; let Even_Odd = PROVE ("!n. Even n ==> Odd (n+1)", PURE_ONCE_REWRITE_TAC [Even_DEF;Odd_DEF] THEN REPEAT STRIP_TAC THEN REPEAT (FIRST_ASSUM MATCH_MP_TAC) THEN EXISTS_TAC "Q:num->bool" THEN REPEAT CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC);; let Odd1 = PROVE ("Odd 1", PURE_ONCE_REWRITE_TAC [Odd_DEF] THEN REPEAT STRIP_TAC);; let Odd_Even = PROVE ("!n. Odd n ==> Even (n+1)", PURE_ONCE_REWRITE_TAC [Even_DEF;Odd_DEF] THEN REPEAT STRIP_TAC THEN REPEAT (FIRST_ASSUM MATCH_MP_TAC) THEN EXISTS_TAC "P:num->bool" THEN REPEAT CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC);; % --------------------------------------------------------------------- % % We also have a principle of Rule Induction for each of Even and Odd. % % We have that for any pair of sets P and Q closed under the rules: % % % % Q n P n % % -------- ---------- ------- --------- % % P 0 P (n+1) Q 1 Q (n+1) % % % % Even is a subset of P and Odd a subset of Q. We can express this % % by two seperate induction theorems, as well as a joint one. % % --------------------------------------------------------------------- % let Rule_Induction1 = PROVE ("!P. (?Q:num->bool. ^PQclosed) ==> !n. Even n ==> P n", PURE_ONCE_REWRITE_TAC [Even_DEF] THEN REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN EXISTS_TAC "Q:num->bool" THEN REPEAT CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC);; let Rule_Induction2 = PROVE ("!Q. (?P:num->bool. ^PQclosed) ==> !n. Odd n ==> Q n", PURE_ONCE_REWRITE_TAC [Odd_DEF] THEN REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN EXISTS_TAC "P:num->bool" THEN REPEAT CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC);; let Rule_Induction = PROVE ("!P Q. ^PQclosed ==> (!n. Even n ==> P n) /\ (!n. Odd n ==> Q n)", PURE_ONCE_REWRITE_TAC [Odd_DEF;Even_DEF] THEN REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THENL (map EXISTS_TAC ["Q:num->bool";"P:num->bool"]) THEN REPEAT CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC);;