1(*---------------------------------------------------------------------------
2
3    An example taken from
4
5        "Automating induction over mutually recursive functions",
6        Deepak Kapur and M. Subramaniam, Proceedings of AMAST'96,
7        Springer LNCS 1101.
8
9    The example displays the equivalence of call-by-name and 
10    call-by-value evaluation strategies for a type of simple arithmetic 
11    terms. The evaluation functions feature mutual and nested recursions.
12
13 ---------------------------------------------------------------------------*)
14
15load "bossLib"; open bossLib;
16
17
18Hol_datatype `arith = Con of num                   (* constant *)
19                    | Var of 'a                    (* variable *)
20                    | Add of arith => arith        (* addition *)
21                    | App of arith => 'a => arith  (* func. application *)`;
22
23
24(*---------------------------------------------------------------------------
25                     Call-by-name evaluation
26 ---------------------------------------------------------------------------*)
27
28val CBN_defn = 
29 Hol_defn 
30  "CBN"
31    `(CBN (Con n, y, N)     = Con n)
32 /\  (CBN (Var x, y, N)     = if x=y then CBNh N else Var x)
33 /\  (CBN (Add a1 a2, y, N) = Add (CBN(a1,y,N)) (CBN(a2,y,N)))
34 /\  (CBN (App B v M, y, N) = CBN (CBN(B,v,M), y, N))
35
36 /\  (CBNh (Con n) = Con n)
37 /\  (CBNh (Var x) = Var x)
38 /\  (CBNh (Add a1 a2) = Add (CBNh a1) (CBNh a2))
39 /\  (CBNh (App B v M) = CBN (B,v,M))`;
40
41
42val CBN_eqns     = Defn.eqns_of CBN_defn;
43val SOME CBN_ind = Defn.ind_of CBN_defn;
44
45
46(*---------------------------------------------------------------------------
47                     Environment lookup
48 ---------------------------------------------------------------------------*)
49
50val lookup_def = 
51 Define
52     `(lookup x [] = 0)
53  /\  (lookup x ((y,N)::rst) = if x=y then N else lookup x rst)`;
54
55
56(*---------------------------------------------------------------------------
57                     Call-by-value evaluation
58 ---------------------------------------------------------------------------*)
59
60val CBV_defn = Hol_defn "CBV"
61    `(CBV (Con n, env)  = n)
62 /\  (CBV (Var x, env)  = lookup x env)
63 /\  (CBV (Add a1 a2, env) = CBV(a1,env) + CBV(a2,env))
64 /\  (CBV (App B v M, env) = CBV(B, (v,CBV(M,env))::env))`;
65
66
67val CBV_eqns      = Defn.eqns_of CBV_defn;
68val SOME CBV_ind  = Defn.ind_of CBV_defn;
69
70
71(*---------------------------------------------------------------------------
72          Some munging to get tidier defns and induction thms.
73 ---------------------------------------------------------------------------*)
74
75val SOME R  = Defn.reln_of CBN_defn;
76val SOME R1 = Defn.reln_of CBV_defn;
77
78val CBNTerminates_def =
79 Define
80    `CBNTerminates ^R = ^(list_mk_conj (Defn.tcs_of CBN_defn))`;
81
82val CBVTerminates_def =
83 Define
84    `CBVTerminates ^R1 = ^(list_mk_conj (Defn.tcs_of CBV_defn))`;
85
86val TC0thms = 
87 CONJUNCTS 
88   (EQ_MP (SPEC_ALL CBNTerminates_def)
89        (ASSUME (lhs(concl(SPEC_ALL CBNTerminates_def)))));
90
91val TC1thms = 
92 CONJUNCTS 
93   (EQ_MP (SPEC_ALL CBVTerminates_def)
94        (ASSUME (lhs(concl(SPEC_ALL CBVTerminates_def)))));
95
96val CBN_eqns' = itlist PROVE_HYP TC0thms (LIST_CONJ CBN_eqns);
97val CBN_ind'  = itlist PROVE_HYP TC0thms CBN_ind;
98val CBV_eqns' = itlist PROVE_HYP TC1thms (LIST_CONJ CBV_eqns);
99
100
101(*---------------------------------------------------------------------------
102    Partial correctness is phrased as the following:
103
104       CBNTerminates R /\ CBVTerminates R1 
105           ==>
106       !x y N env. 
107           CBV (CBN(x,y,N),env) 
108              = 
109           CBV (x, (y,CBV(N,env))::env)
110
111    We build an induction theorem first, by instantiating the 
112    induction theorem for CBN to the predicates suggested by the 
113    method of Richard Boulton.
114 ---------------------------------------------------------------------------*)
115
116val tm = Term
117 `\(x,y,N). 
118    !env. CBV (CBN (x,y,N), env) 
119               = 
120          CBV(x, (y, CBV(N,env))::env)`;
121
122val tm1 = Term `\N. !env. CBV (CBNh N, env) = CBV(N,env)`;
123
124val [P0,P1] = fst(strip_forall(concl CBN_ind'));
125val ind0 = SPEC_ALL CBN_ind';
126val ind1 = CONV_RULE (DEPTH_CONV pairLib.GEN_BETA_CONV)
127              (INST [P0 |-> tm, P1 |-> tm1] ind0);
128val [ind2a, _] = CONJUNCTS (UNDISCH ind1);
129val ind3 = REWRITE_RULE pairTheory.pair_rws
130             (SPEC (Term`(x,y,N):'a arith#'a#'a arith`) ind2a);
131val ind4 = DISCH (fst(dest_imp(concl ind1)))
132                 (SPEC_ALL ind3);
133
134
135(*---------------------------------------------------------------------------
136      We distinguish the names "R" and "R1" of the termination 
137      relations; otherwise, the termination relations for both 
138      CBN and CBV would have the same name, which is confusing.
139 ---------------------------------------------------------------------------*)
140
141val R1' = mk_var("R1", type_of R1);;
142
143val CBV_eqns'' = UNDISCH (INST [R1 |-> R1'] (DISCH_ALL CBV_eqns'));
144
145
146(*---------------------------------------------------------------------------
147           Given ind4, the correctness proof is easy!
148 ---------------------------------------------------------------------------*)
149
150val KapurSubra = store_thm("KapurSubra",
151 Term`!R R1.
152        CBNTerminates ^R /\ CBVTerminates ^R1'
153            ==>
154        !x (y:'a) N env. 
155                CBV (CBN(x,y,N),env) 
156                   = 
157                CBV (x, (y, CBV(N,env))::env)`,
158REPEAT GEN_TAC THEN STRIP_TAC
159 THEN MATCH_MP_TAC ind4
160 THEN RW_TAC std_ss [CBN_eqns',CBV_eqns'',lookup_def]);
161
162
163(*---------------------------------------------------------------------------
164       Remaining task: supply R and R1 such that 
165
166          CBNTerminates R /\ CBVTerminates R1
167
168       This will require reasoning about the auxiliary functions
169       used in defining CBN and CBV. Since CBN is mutual recursive 
170       with CBNh and also a nested recursion, this makes things 
171       not completely obvious. We tackle CBV first, since it's
172       easier.
173 ---------------------------------------------------------------------------*)
174
175local val [guess1,_] = TotalDefn.guessR CBV_defn
176in
177val CBVTerminates = Q.prove
178(`CBVTerminates ^guess1`,
179 TotalDefn.TC_SIMP_TAC [] [prim_recTheory.WF_measure,CBVTerminates_def])
180end;
181
182
183(*---------------------------------------------------------------------------
184    Termination of CBN is much harder! First there's the problem of 
185    seeing why it terminates, then there's the task of expressing
186    termination formally, and finally, the proof of termination is 
187    also a little bit challenging.
188
189    1. Why it terminates. CBN eliminates all "App" nodes in an
190       expression. Thus, we can simply count the Apply nodes. 
191       However, the case where there are no App nodes in the 
192       expression must also be dealt with; in this case, the 
193       recursion is always on smaller arguments.
194
195    2. Formal expression. The specification of CBN leads to several 
196       background definitions: a "union" function is constructed to 
197       handle the mutual recursion, and an "auxiliary" function is
198       built to handle the nested recursion. The termination constraints
199       that we have to eliminate are those of the union function, and
200       these contain occurrences of the auxiliary function.
201
202       The way the analysis of (1) is formalized starts by defining 
203       a count of the App nodes in an expression. This measure will 
204       be put together in a lexicographic combination with the normal
205       size functions. We just have to fiddle to make sure that 
206       different size functions are applied in the different injections
207       into the sum.
208      
209 ---------------------------------------------------------------------------*)
210
211val AppCount_def =
212  Define
213    `(AppCount (App B _ M) = 1 + AppCount B + AppCount M)
214 /\  (AppCount (Add M N)   = AppCount M + AppCount N)
215 /\  (AppCount   _____     = 0)`;
216
217val JointAppCount_def =
218  Define
219    `(JointAppCount (INL(P,_,Q)) = AppCount P + AppCount Q)
220 /\  (JointAppCount (INR P)      = AppCount P)`;
221
222val JointStdSize_def =
223  Define 
224   `(JointStdSize (INL(P,_,Q)) = arith_size (\v.0) P + arith_size (\v.0) Q)
225 /\ (JointStdSize (INR P)      = arith_size (\v.0) P)`;
226
227
228val R = Term 
229`inv_image ($< LEX $<)
230  (\x:'a arith#'a#'a arith + 'a arith. (JointAppCount x, JointStdSize x))`;
231
232(*---------------------------------------------------------------------------
233     Set the termination relation of CBN_defn
234 ---------------------------------------------------------------------------*)
235
236val defnR = Defn.set_reln CBN_defn R;
237val tcs as [tc1,tc2,nested,tc3,tc4,tc5,tc6,tc7,tc8] = Defn.tcs_of defnR;
238
239(*---------------------------------------------------------------------------
240    Prove the easy termination conditions
241 ---------------------------------------------------------------------------*)
242
243val easy_tcs = prove(list_mk_conj [tc1,tc2,tc3,tc4,tc5,tc6,tc7,tc8],
244 TotalDefn.TC_SIMP_TAC [] 
245    [JointAppCount_def,JointStdSize_def,
246     AppCount_def,fetch "-" "arith_size_def"]);
247
248(*---------------------------------------------------------------------------
249       And eliminate them from the definition
250 ---------------------------------------------------------------------------*)
251
252val defnR_1 = Defn.elim_tcs defnR (CONJUNCTS easy_tcs);
253
254(*---------------------------------------------------------------------------
255    Fetch the equations for the auxiliary definition
256 ---------------------------------------------------------------------------*)
257
258val SOME Un = Defn.union_defn defnR_1;
259val SOME Aux_defn = Defn.aux_defn Un;
260
261(*---------------------------------------------------------------------------
262    Remove the easy termination constraints from the equations and
263    the provisional induction theorem.
264 ---------------------------------------------------------------------------*)
265
266val eqns = map (REWRITE_RULE [easy_tcs]) (Defn.eqns_of Aux_defn);
267val ind = REWRITE_RULE [easy_tcs] (valOf (Defn.ind_of Aux_defn));
268
269(*---------------------------------------------------------------------------
270     An abbreviation to make the goal more readable.
271 ---------------------------------------------------------------------------*)
272
273val Fn_def = Define `Fn = CBN_UNION_aux ^R`;
274
275(*---------------------------------------------------------------------------
276    Apply the abbreviation to the equations and provisional ind. thm.
277 ---------------------------------------------------------------------------*)
278
279val [e1,e2,e3,e4,e5,e6,e7,e8] = map (REWRITE_RULE [GSYM Fn_def]) eqns;
280val Fn_ind = REWRITE_RULE [GSYM Fn_def] ind;
281
282(*---------------------------------------------------------------------------
283     e4 is the nested equation and has a remaining tc on its assumptions
284 ---------------------------------------------------------------------------*)
285
286val eqn4 = REWRITE_RULE [GSYM Fn_def] (DISCH_ALL e4);
287
288(*---------------------------------------------------------------------------
289   CBN_UNION_aux, and therefore CBN, removes all App nodes from a term
290 ---------------------------------------------------------------------------*)
291
292val AppCountLem = Q.prove
293(`!e. AppCount (Fn e) = 0`,
294 recInduct Fn_ind
295   THEN RW_TAC arith_ss (AppCount_def::[e1,e2,e3,e5,e6,e7,e8]) THEN 
296   Q.SUBGOAL_THEN 
297     `inv_image ($< LEX $<) (\x. (JointAppCount x,JointStdSize x))
298        (INL (Fn (INL (B,v,M)),y,N)) (INL (App B v M,y,N))` ASSUME_TAC THENL 
299   [WEAKEN_TAC is_imp THEN 
300    TotalDefn.TC_SIMP_TAC [] [JointAppCount_def,JointStdSize_def,AppCount_def],
301    PROVE_TAC [eqn4]]);
302
303(*---------------------------------------------------------------------------
304     Termination of CBN
305 ---------------------------------------------------------------------------*)
306
307val (CBN_eqns, CBN_ind) = 
308Defn.tprove(CBN_defn,
309  EXISTS_TAC R THEN REWRITE_TAC [SYM Fn_def, easy_tcs]
310   THEN TotalDefn.TC_SIMP_TAC [] 
311          [JointAppCount_def,JointStdSize_def, AppCount_def,AppCountLem]);
312