Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 1 Feb 1994 21:05:19 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA11654; Tue, 1 Feb 1994 13:43:00 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA11650; Tue, 1 Feb 1994 13:42:31 -0700 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA08004; Tue, 1 Feb 1994 12:40:11 -0800 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 1 Feb 1994 20:40:02 +0000 To: info-hol@cs.uidaho.edu Subject: Recursion via induction for trees Date: Tue, 01 Feb 94 20:39:56 +0000 From: John Harrison Message-Id: <"swan.cl.cam.:244990:940201204005"@cl.cam.ac.uk> The discussion at HUG93 of the construction of infinitely-branching trees in hol90 reminded me that I had once started this in HOL88, but got discouraged at the prospect of proving the recursion (initiality) theorem. There are two standard ways of proving a theorem like this: * Prove by induction that you can define functions on any "initial segment", and that any two such agree on their common domain; hence the union of all these functions is what you want. * Define the graph of the desired function inductively (which here means over the clauses of the desired recursion) and then show by induction that it's the graph of a total function. As Elsa pointed out, it's not clear that one can come up with a satisfactory version of the former proof for infinitely branching trees, so I had to use the second. What struck me is that the second method is also *so* much easier! It's quite surprising to me that most books seem to prefer the first. (The second does appear in Jacobson "Basic Algebra I".) For example, the inbuilt proof of the primitive recursion theorem in HOL could be made a lot shorter using the second proof. This would apply especially if automatic inductive definitions as provided by the |ind_def| library were available at that stage, in the core. Finally, the present proof would have been simpler if the |ind_def| library allowed universal quantifiers in the hypotheses of rules. Conceivably it could be useful for more orthodox applications, e.g. a proof system for a logic with some sort of omega-rule. Anyway, enough chat. If anyone wants a HOL88 theory of infinitely branching trees, here it is. I think it's a bit weaker than Elsa's hol90 version because we don't allow partial functions at the nodes. But you could presumably construct something similar following the same pattern. John. %============================================================================% % Arbitrarily-branching (but wellfounded) trees. % % % % (*a,*b)Tree = Leaf(*b) | Branch(*a->(*a,*b)Tree) % %============================================================================% can unlink `TREE.th`;; new_theory `TREE`;; let LAND_CONV = RATOR_CONV o RAND_CONV;; %----------------------------------------------------------------------------% % Important general theorems for transforming between graphs and functions. % %----------------------------------------------------------------------------% let EXISTS_UNIQUE = prove_thm(`EXISTS_UNIQUE`, "!P:*->bool. (?!x. P(x)) = (!x. P(x) = (x = @x. P(x)))", REPEAT GEN_TAC THEN CONV_TAC(LAND_CONV EXISTS_UNIQUE_CONV) THEN EQ_TAC THENL [DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN GEN_TAC THEN EQ_TAC THENL [DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC] THEN CONV_TAC SELECT_CONV THEN ASM_REWRITE_TAC[]; DISCH_THEN(\th. ONCE_REWRITE_TAC[th]) THEN CONJ_TAC THENL [W(EXISTS_TAC o rhs o snd o dest_exists o snd) THEN REFL_TAC; REPEAT STRIP_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN REFL_TAC]]);; let FUN_GRAPH_GEN = prove_thm(`FUN_GRAPH_GEN`, "!(f:***->*) (P:*#**->bool) . (!x. ?!y. P(f(x),y)) = ?fn. !x y. P(f(x),y) = (y = fn(f(x)))", REPEAT GEN_TAC THEN EQ_TAC THENL [REWRITE_TAC[ONCE_REWRITE_RULE[ETA_AX] EXISTS_UNIQUE] THEN BETA_TAC THEN DISCH_THEN(\th. ONCE_REWRITE_TAC[th]) THEN EXISTS_TAC "\z:*. (@w:**. P(z,w))" THEN BETA_TAC THEN REWRITE_TAC[]; STRIP_TAC THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN CONV_TAC EXISTS_UNIQUE_CONV THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN W(EXISTS_TAC o rhs o snd o dest_exists o snd) THEN REFL_TAC]);; let FUN_GRAPH = prove_thm(`FUN_GRAPH`, "!P:*#**->bool. (!x. ?!y. P(x,y)) = ?f. !x y. P(x,y) = (y = f x)", MP_TAC(ISPEC "\x:*. x" FUN_GRAPH_GEN) THEN BETA_TAC THEN REWRITE_TAC[]);; %----------------------------------------------------------------------------% % Represent a tree as a set of elements ([a1;...;an],b), each imagined as % % a path chosen according to a1,...,an at successive branches and finishing % % in a leaf node labelled with b. % %----------------------------------------------------------------------------% let ty = ":*a list # *b -> bool";; let Leaf_REP = new_definition(`Leaf_REP`, "Leaf_REP (b:*b) = \(l,x). (l:(*a)list = []) /\ (x = b)");; let Branch_REP = new_definition(`Branch_REP`, "Branch_REP (f:*a->^ty) = \(l,x). ?a m. f(a)(m,x) /\ (l = CONS a m)");; %----------------------------------------------------------------------------% % Define inhabitation predicate. We can't use the inductive definitions % % package because of the universal quantifier in the antecedant of the % % implication, but we can easily prove the requisite theorems "by hand". % %----------------------------------------------------------------------------% let Typred = new_definition(`Typred`, "Typred (X:^ty) = !C. (!b. C(Leaf_REP b)) /\ (!f. (!a. C(f a)) ==> C(Branch_REP f)) ==> C(X)");; let Typred_thm = prove_thm(`Typred_thm`, "(!b. Typred(Leaf_REP b :^ty)) /\ (!f. (!a. Typred(f a)) ==> Typred(Branch_REP f :^ty))", REWRITE_TAC[Typred] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT(FIRST_ASSUM MATCH_MP_TAC THEN TRY GEN_TAC) THEN ASM_REWRITE_TAC[]);; let Typred_INDUCT = prove_thm(`Typred_INDUCT`, "!P x. (!b. P(Leaf_REP b)) /\ (!f. (!a. P(f a)) ==> P(Branch_REP f)) /\ Typred(x) ==> P(x:^ty)", REWRITE_TAC[Typred] THEN REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);; %----------------------------------------------------------------------------% % Prove type is inhabited, define it and define type bijections. % %----------------------------------------------------------------------------% let Tree = new_type_definition(`Tree`, "Typred:^ty->bool",PROVE("?x:^ty. Typred x", EXISTS_TAC "Leaf_REP b :^ty" THEN REWRITE_TAC[Typred_thm]));; let Tree_tybij = define_new_type_bijections `Tree_tybij` `mk_Tree` `dest_Tree` Tree;; let TYPRED_DEST = prove_thm(`TYPRED_DEST`, "!t:(*a,*b)Tree. Typred(dest_Tree t)", REWRITE_TAC[Tree_tybij]);; let MK_INJECTIVE = prove_thm(`MK_INJECTIVE`, "!(x:^ty) y. Typred x /\ Typred y /\ ~(x = y) ==> ~(mk_Tree x = mk_Tree y)", REPEAT GEN_TAC THEN REWRITE_TAC[Tree_tybij] THEN STRIP_TAC THEN DISCH_THEN(MP_TAC o AP_TERM "dest_Tree:(*a,*b)Tree->^ty") THEN ASM_REWRITE_TAC[]);; let abty = ":(*a,*b)Tree";; %----------------------------------------------------------------------------% % Now define the "true" version of our functions. % %----------------------------------------------------------------------------% let Leaf = new_definition(`Leaf`, "Leaf b = mk_Tree(Leaf_REP b :^ty)");; let Branch = new_definition(`Branch`, "Branch (f:*a->^abty) = mk_Tree(Branch_REP (\a. dest_Tree(f a)))");; %----------------------------------------------------------------------------% % Prove that induction holds. % %----------------------------------------------------------------------------% let Tree_INDUCT = prove_thm(`Tree_INDUCT`, "!P:^abty->bool. (!b. P(Leaf b)) /\ (!f. (!a. P(f a)) ==> P(Branch f)) ==> !x. P x", REWRITE_TAC[Leaf; Branch] THEN REPEAT STRIP_TAC THEN MP_TAC (SPECL ["\x:^ty. Typred x /\ P(mk_Tree x)"; "dest_Tree(x):^ty"] Typred_INDUCT) THEN BETA_TAC THEN REWRITE_TAC[Typred_thm; TYPRED_DEST; CONJUNCT1 Tree_tybij] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THENL [MATCH_MP_TAC(CONJUNCT2 Typred_thm) THEN ASM_REWRITE_TAC[]; RULE_ASSUM_TAC(REWRITE_RULE[Tree_tybij]) THEN FIRST_ASSUM(MP_TAC o SPEC "\a:*a. mk_Tree(f a :^ty)") THEN BETA_TAC THEN ASM_REWRITE_TAC[ETA_AX]]);; %----------------------------------------------------------------------------% % MATCH_MP_TAC won't allow |- ... ==> $! P, so define a little tactic. % %----------------------------------------------------------------------------% let Tree_INDUCT_TAC = W(MATCH_MP_TAC o BETA_RULE o C ISPEC Tree_INDUCT o rand o snd) THEN CONJ_TAC;; %----------------------------------------------------------------------------% % Prove that the constructors are distinct and injective. % %----------------------------------------------------------------------------% let Branch_Leaf = prove_thm(`Branch_Leaf`, "!(f:*a->^abty) (b:*b). ~(Branch f = Leaf b)", REPEAT GEN_TAC THEN REWRITE_TAC[Branch; Leaf] THEN MATCH_MP_TAC MK_INJECTIVE THEN REWRITE_TAC[Typred_thm] THEN CONJ_TAC THENL [MATCH_MP_TAC(CONJUNCT2 Typred_thm) THEN BETA_TAC THEN MATCH_ACCEPT_TAC TYPRED_DEST; REWRITE_TAC[Branch_REP; Leaf_REP] THEN DISCH_THEN(MP_TAC o C AP_THM "[]:*a list,(b:*b)") THEN CONV_TAC(ONCE_DEPTH_CONV PAIRED_BETA_CONV) THEN REWRITE_TAC[NOT_NIL_CONS]]);; let Leaf_INJ = prove_thm(`Leaf_INJ`, "!b1 b2. (Leaf(b1):^abty = Leaf(b2)) = (b1 = b2)", REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[Leaf] THEN CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN MATCH_MP_TAC MK_INJECTIVE THEN REWRITE_TAC[Typred_thm] THEN REWRITE_TAC[Leaf_REP] THEN DISCH_THEN(MP_TAC o C AP_THM "[]:*a list,b1:*b") THEN CONV_TAC(ONCE_DEPTH_CONV PAIRED_BETA_CONV) THEN ASM_REWRITE_TAC[]);; let Branch_INJ = prove_thm(`Branch_INJ`, "!f1 f2. (Branch(f1):^abty = Branch(f2)) = (f1 = f2)", let unwind_lemma = PROVE ("(?(x:*1) (y:*2). f(g x:*3)(y,z:*4) /\ (v = x) /\ (w = y)) = f(g v)(w,z)", EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MAP_EVERY EXISTS_TAC ["v:*1"; "w:*2"] THEN ASM_REWRITE_TAC[]) in REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[Branch] THEN CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN MATCH_MP_TAC MK_INJECTIVE THEN REWRITE_TAC[Typred_thm] THEN REPEAT CONJ_TAC THEN TRY(MATCH_MP_TAC(CONJUNCT2 Typred_thm)) THEN BETA_TAC THEN REWRITE_TAC[TYPRED_DEST] THEN REWRITE_TAC[Branch_REP] THEN POP_ASSUM MP_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN DISCH_TAC THEN CONV_TAC FUN_EQ_CONV THEN X_GEN_TAC "a:*a" THEN ONCE_REWRITE_TAC[GSYM(CONJUNCT1 Tree_tybij)] THEN AP_TERM_TAC THEN CONV_TAC FUN_EQ_CONV THEN X_GEN_TAC "p:*a list # *b" THEN POP_ASSUM(MP_TAC o C AP_THM "CONS (a:*a) (FST p),(SND p:*b)") THEN CONV_TAC(ONCE_DEPTH_CONV PAIRED_BETA_CONV) THEN BETA_TAC THEN REWRITE_TAC[CONS_11; unwind_lemma]);; %----------------------------------------------------------------------------% % Now prove the recursion (initiality) theorem. Make an inductive definition % % of the graph of the desired function (again we have to do it by hand owing % % to the universal quantifier). % %----------------------------------------------------------------------------% let PR_CLOSED = new_definition(`PR_CLOSED`, "PR_CLOSED (c:*b->*) (d:(*a->*)->(*a->^abty)->*) G = (!b. G(Leaf(b),c(b))) /\ (!f fn. (!a. G(f a,fn(f a))) ==> G(Branch f,d (fn o f) f))");; let PR_GRAPH = new_definition(`PR_GRAPH`, "PR_GRAPH (c:*b->*) (d:(*a->*)->(*a->^abty)->*) (x,y) = !G. PR_CLOSED c d G ==> G(x,y)");; let PR_RULES = prove_thm(`PR_RULES`, "!(c:*b->*) (d:(*a->*)->(*a->^abty)->*). (!b. PR_GRAPH c d (Leaf(b),c(b))) /\ (!f fn. (!a. PR_GRAPH c d (f a,fn(f a))) ==> PR_GRAPH c d (Branch f,d (fn o f) f))", REPEAT GEN_TAC THEN REWRITE_TAC[PR_GRAPH; PR_CLOSED] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT(FIRST_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);; let PR_INDUCT = prove_thm(`PR_INDUCT`, "!G (c:*b->*) (d:(*a->*)->(*a->^abty)->*). PR_CLOSED c d G ==> !x y. PR_GRAPH c d (x,y) ==> G(x,y)", REWRITE_TAC[PR_GRAPH] THEN REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC);; %----------------------------------------------------------------------------% % For the next stage, we need the cases theorem. % %----------------------------------------------------------------------------% let PR_CASES = prove_thm(`PR_CASES`, "!(c:*b->*) (d:(*a->*)->(*a->^abty)->*). PR_GRAPH c d (x,y) = (?b. (x = Leaf b) /\ (y = c b)) \/ (?f fn. (x = Branch f) /\ (y = d (fn o f) f) /\ (!a. PR_GRAPH c d (f a,fn(f a))))", REPEAT GEN_TAC THEN EQ_TAC THENL [W(MATCH_MP_TAC o CONV_RULE(ONCE_DEPTH_CONV PAIRED_BETA_CONV) o C ISPEC PR_INDUCT o curry mk_pabs "(x:^abty,y:*)" o rand o snd) THEN REWRITE_TAC[PR_CLOSED] THEN CONV_TAC(ONCE_DEPTH_CONV PAIRED_BETA_CONV) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[Branch_Leaf] THENL [DISJ1_TAC THEN EXISTS_TAC "b:*b" THEN REWRITE_TAC[]; MAP_EVERY EXISTS_TAC ["f:*a->^abty"; "fn:^abty->*"] THEN REWRITE_TAC[] THEN X_GEN_TAC "a:*a" THEN POP_ASSUM(STRIP_ASSUME_TAC o SPEC "a:*a") THEN ASM_REWRITE_TAC[PR_RULES] THEN MATCH_MP_TAC(CONJUNCT2(SPEC_ALL PR_RULES)) THEN ASM_REWRITE_TAC[]]; REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[PR_RULES] THEN MATCH_MP_TAC(CONJUNCT2(SPEC_ALL PR_RULES)) THEN ASM_REWRITE_TAC[]]);; %----------------------------------------------------------------------------% % Inductive proof that the relation is the graph of a total function. % %----------------------------------------------------------------------------% let PR_GTOTAL = prove_thm(`PR_GTOTAL`, "!c d (x:^abty). ?!y:*. PR_GRAPH c d (x,y)", GEN_TAC THEN GEN_TAC THEN Tree_INDUCT_TAC THENL [X_GEN_TAC "b:*b" THEN CONV_TAC EXISTS_UNIQUE_CONV THEN CONJ_TAC THENL [EXISTS_TAC "(c:*b->*) b" THEN REWRITE_TAC[PR_RULES]; REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[PR_CASES] THEN REWRITE_TAC[GSYM Branch_Leaf; Leaf_INJ] THEN DISCH_THEN(CONJUNCTS_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) SUBST1_TAC))) THEN ASM_REWRITE_TAC[]]; X_GEN_TAC "f:*a->^abty" THEN REWRITE_TAC[FUN_GRAPH_GEN] THEN DISCH_THEN(X_CHOOSE_TAC "fn:^abty->*") THEN CONV_TAC EXISTS_UNIQUE_CONV THEN CONJ_TAC THENL [POP_ASSUM(MP_TAC o GEN_ALL o SPECL ["x:*a"; "(fn:^abty->*)(f(x:*a))"]) THEN REWRITE_TAC[] THEN DISCH_THEN(ASSUME_TAC o MATCH_MP(CONJUNCT2(SPEC_ALL PR_RULES))) THEN W(EXISTS_TAC o rand o rand o hd o fst) THEN POP_ASSUM ACCEPT_TAC; REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[PR_CASES] THEN REWRITE_TAC[Branch_Leaf; Branch_INJ] THEN DISCH_THEN(CONJUNCTS_THEN(REPEAT_TCL CHOOSE_THEN (CONJUNCTS_THEN2 (ASSUME_TAC o SYM) (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)))) THEN ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN CONV_TAC FUN_EQ_CONV THEN ASM_REWRITE_TAC[o_THM]]]);; %----------------------------------------------------------------------------% % Convert from relational to functional form and include uniqueness. % %----------------------------------------------------------------------------% let Tree_Axiom = prove_thm(`Tree_Axiom`, "!c d. ?!fn:^abty->*. (!b. fn(Leaf b) = c(b)) /\ (!f. fn(Branch f) = d (fn o f) f)", REPEAT GEN_TAC THEN CONV_TAC EXISTS_UNIQUE_CONV THEN CONJ_TAC THENL [MP_TAC(SPECL ["c:*b->*"; "d:(*a->*)->(*a->^abty)->*"] PR_GTOTAL) THEN REWRITE_TAC[FUN_GRAPH] THEN DISCH_THEN(X_CHOOSE_TAC "gn:^abty->*") THEN EXISTS_TAC "gn:^abty->*" THEN MP_TAC(SPEC_ALL PR_RULES) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[]; REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN Tree_INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[o_DEF]]);; %----------------------------------------------------------------------------% % For completeness, prove the case analysis theorem for trees. % %----------------------------------------------------------------------------% let Tree_CASES = prove_thm(`Tree_CASES`, "!x:^abty. (?b. x = Leaf b) \/ (?f. x = Branch f)", Tree_INDUCT_TAC THEN REPEAT STRIP_TAC THENL [DISJ1_TAC; DISJ2_TAC] THEN W(EXISTS_TAC o rand o lhs o snd o dest_exists o snd) THEN REFL_TAC);; close_theory();;