1(*---------------------------------------------------------------------------* 2 * * 3 * Mutual recursion * 4 * * 5 *---------------------------------------------------------------------------*) 6 7app load ["bossLib"]; open bossLib; 8 9(*--------------------------------------------------------------------------- 10 Start with something simple: even and odd 11 ---------------------------------------------------------------------------*) 12 13val eo_def = 14 xDefine "eo" `(even 0 = T) /\ 15 (odd 0 = F) /\ 16 (even (SUC x) = odd x) /\ 17 (odd (SUC x) = even x)`; 18 19 20val APART = prove(Term `!n. even n = ~odd n`, 21 Induct 22 THEN RW_TAC std_ss [eo_def]); 23 24 25(*--------------------------------------------------------------------------- 26 Taking an implication out of the equality makes the proof 27 harder, since the inductive hypothesis is not in shape to be used. 28 Fortunately, some propositional reasoning puts things right. 29 ---------------------------------------------------------------------------*) 30 31val APART_IMP = prove(Term `!n. even n ==> ~odd n`, 32 Induct 33 THEN RW_TAC std_ss [eo_def] 34 THEN PROVE_TAC[]); 35 36 37(*--------------------------------------------------------------------------- 38 Something a little more complex: dealing with nested 39 datatypes. First we define a type of arbitrarily branching 40 trees. Some fiddling needs to be done to deliver the proper 41 size equation and insert it into the TypeBase. 42 ---------------------------------------------------------------------------*) 43 44val _ = Hol_datatype `ltree = Node of 'a => ltree list`; 45 46val (size_tm,ltree_size_def_0) = TypeBase.size_of ``:'a ltree``; 47 48val ltree_size_def = Q.prove 49(`!x f l. ltree_size f (Node x l) = list_size (ltree_size f) l + f x + 1`, 50 NTAC 2 GEN_TAC THEN Induct 51 THEN RW_TAC list_ss [ltree_size_def_0,listTheory.list_size_def] 52 THEN POP_ASSUM MP_TAC 53 THEN Cases_on `l` 54 THEN RW_TAC list_ss [ltree_size_def_0,listTheory.list_size_def]); 55 56val _ = TypeBase.write 57 [TypeBasePure.put_size (size_tm,TypeBasePure.ORIG ltree_size_def) 58 (valOf (TypeBase.read {Tyop="ltree",Thy="scratch"}))]; 59 60val fringe_fns_def = 61 xDefine "fringe_fns" 62 `(fringe (Node v []) = [v]) 63 /\ (fringe (Node v l) = fringes l) 64 65 /\ (fringes [] = []) 66 /\ (fringes (h::t) = (fringe h) ++ (fringes t))`; 67 68 69(*--------------------------------------------------------------------------- 70 This can also be handled with higher-order recursion, but some 71 extra mucking around is needed to prove termination. Can 72 this be automated? 73 ---------------------------------------------------------------------------*) 74 75val Fringe_defn = 76 Defn.Hol_defn "Fringe" 77 `(Fringe (Node v []) = [v]) /\ 78 (Fringe (Node v l) = FLAT (MAP Fringe l))`; 79 80 81(*--------------------------------------------------------------------------- 82 Required lemma in termination proof 83 ---------------------------------------------------------------------------*) 84 85val list_contains_ltree_lem = Q.prove 86(`!ltr l f. MEM ltr l ==> ltree_size f ltr <= list_size (ltree_size f) l`, 87 Induct_on `l` 88 THEN RW_TAC list_ss [listTheory.MEM,listTheory.list_size_def] 89 THENL [DECIDE_TAC, PROVE_TAC [DECIDE ``x:num <= y ==> x <= y+z``]]); 90 91(*--------------------------------------------------------------------------- 92 Termination proof for Fringe 93 ---------------------------------------------------------------------------*) 94 95local val [_,guess] = TotalDefn.guessR Fringe_defn 96 open listTheory 97in 98val (Fringe_eqns,Fringe_ind) = 99 Defn.tprove(Fringe_defn, 100 WF_REL_TAC `^guess` 101 THEN RW_TAC list_ss [MEM,ltree_size_def,list_size_def] 102 THENL [numLib.ARITH_TAC, 103 PROVE_TAC [list_contains_ltree_lem, 104 DECIDE ``x:num <= y ==> x < y + (w+2)``]]) 105end; 106 107 108(*--------------------------------------------------------------------------- 109 So far, only the domain of the mutual function has had 110 to be a sum. Here's a situation where the range is also a sum. 111 The example is an evaluation function for a simple first order 112 mutually recursive type of expressions. 113 114 In ML: 115 116 datatype 117 ('a,'b)exp = VAR of 'a 118 | IF of ('a,'b)bexp * ('a,'b)exp * ('a,'b)exp 119 | APP of 'b * ('a,'b)exp list 120 and 121 ('a,'b)bexp = EQ of ('a,'b)exp * ('a,'b)exp 122 | LEQ of ('a,'b)exp * ('a,'b)exp 123 | AND of ('a,'b)bexp * ('a,'b)bexp 124 | OR of ('a,'b)bexp * ('a,'b)bexp 125 | NOT of ('a,'b)bexp; 126 127 128 fun E env (VAR x) = fst env x 129 | E env (IF (b,e1,e2)) = if EB env b then E env e1 else E env e2 130 | E env (APP (f,l)) = (snd env f) (EL env l) 131 and 132 EL env [] = [] 133 | EL env (a::t) = E env a :: EL env t 134 and 135 EB env (EQ (e1,e2)) = (E env e1 = E env e2) 136 | EB env (LEQ (e1,e2)) = E env e1 <= E env e2 137 | EB env (AND (b1,b2)) = EB env b1 andalso EB env b2 138 | EB env (OR (b1,b2)) = EB env b1 orelse EB env b2 139 | EB env (NOT b) = not(EB env b); 140 141 ---------------------------------------------------------------------------*) 142 143val _ = Hol_datatype 144 `exp = VAR of 'a 145 | IF of bexp => exp => exp 146 | APP of 'b => exp list 147 ; 148 bexp = EQ of exp => exp 149 | LEQ of exp => exp 150 | AND of bexp => bexp 151 | OR of bexp => bexp 152 | NOT of bexp`; 153 154 155val (_,size_def) = TypeBase.size_of ``:('a,'b)exp``; 156 157val exp = ty_antiq ``:('a,'b)exp``; 158val bexp = ty_antiq ``:('a,'b)bexp``; 159 160 161(*--------------------------------------------------------------------------- 162 The argument "env" comprises two maps: one for variables, and one 163 for functions. Termination should be proved automatically, but it's 164 not (currently), so we have to do a manual proof. 165 ---------------------------------------------------------------------------*) 166 167val ELBdefn = 168 Count.apply (Hol_defn "ELB") 169 `(E (env, VAR x:^exp) = FST env x) 170 /\ (E (env, IF b e1 e2) = if EB (env,b) then E (env,e1) else E (env,e2)) 171 /\ (E (env, APP f l) = (SND env f) (ELL (env, l))) 172 173 /\ (ELL (env, []) = []) 174 /\ (ELL (env, a::t) = E (env, a) :: ELL (env, t)) 175 176 /\ (EB (env, EQ e1 e2) = (E (env, e1) = E (env, e2))) 177 /\ (EB (env, LEQ e1 e2) = E (env, e1) <= E (env, e2)) 178 /\ (EB (env, NOT b:^bexp) = ~EB (env, b)) 179 /\ (EB (env, OR b1 b2) = EB (env, b1) \/ EB (env, b2)) 180 /\ (EB (env, AND b1 b2) = EB (env, b1) /\ EB (env, b2))`; 181 182 183val [_,guess] = TotalDefn.guessR ELBdefn; 184Defn.tgoal ELBdefn; 185e (WF_REL_TAC `^guess` THEN RW_TAC arith_ss [size_def]); 186e (Induct_on `l` THEN RW_TAC list_ss [size_def,listTheory.list_size_def]); 187 188 189(*--------------------------------------------------------------------------- 190 A version of the same functions, featuring higher-order 191 recursion and schema variables. The definition process 192 actually helps write the function, by threading the environment 193 through all the calls. 194 ---------------------------------------------------------------------------*) 195 196val Evals_defn = 197 Count.apply 198 (Defn.Hol_defn "Evals") 199 `(Eval (VAR x) = vEnv x) 200 /\ (Eval (IF b e1 e2) = if Bval b then Eval e1 else Eval e2) 201 /\ (Eval (APP f l) = fEnv (MAP Eval l)) 202 203 /\ (Bval (EQ e1 e2) = (Eval e1 = Eval e2)) 204 /\ (Bval (LEQ e1 e2) = Eval e1 <= Eval e2) 205 /\ (Bval (NOT b) = ~Bval (b:^bexp)) 206 /\ (Bval (OR b1 b2) = Bval b1 \/ Bval b2) 207 /\ (Bval (AND b1 b2) = Bval b1 /\ Bval b2)`; 208 209 210val (Evals_def,Evals_ind) = 211 let val [_,guess] = TotalDefn.guessR Evals_defn 212 in Defn.tprove(Evals_defn, 213 WF_REL_TAC `^guess` 214 THEN RW_TAC arith_ss [size_def] 215 THEN Induct_on `l` 216 THEN RW_TAC list_ss [size_def,listTheory.MEM] 217 THENL [PROVE_TAC [DECIDE ``x < y+(x+2n)``], 218 PROVE_TAC [DECIDE ``x < y+1n ==> x < y+(z+2)``]]) 219 end; 220