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