1(*---------------------------------------------------------------------------
2           McCarthy's 91 function.
3 ---------------------------------------------------------------------------*)
4
5quietdec := true;
6open TotalDefn numLib prim_recTheory arithmeticTheory;
7quietdec := false;
8
9(*---------------------------------------------------------------------------
10       Define the 91 function. We call it "N". We use Hol_defn to 
11       make the definition, since we have to tackle the termination 
12       proof ourselves.
13 ---------------------------------------------------------------------------*)
14
15val N_defn = Hol_defn "N" `N(x) = if x>100 then x-10 else N (N (x+11))`;
16
17val [Neqn] = Defn.eqns_of N_defn;
18val SOME Nind = Defn.ind_of N_defn;
19
20val SOME N_aux_defn = Defn.aux_defn N_defn;
21val SOME N_aux_ind = Defn.ind_of N_aux_defn;
22val [E] = map DISCH_ALL (Defn.eqns_of N_aux_defn);
23
24(*---------------------------------------------------------------------------
25      Prove partial correctness for N, to see how such a proof
26      works when the termination relation has not yet been supplied.
27 ---------------------------------------------------------------------------*)
28
29val Npartly_correct = Q.prove
30(`WF R /\ 
31  (!x. ~(x > 100) ==> R (N_aux R (x + 11)) x) /\
32  (!x. ~(x > 100) ==> R (x + 11) x)
33    ==>
34  !n. N(n) = if n>100 then n-10 else 91`,
35 STRIP_TAC THEN recInduct Nind
36   THEN RW_TAC arith_ss [] 
37   THEN ONCE_REWRITE_TAC [Neqn]
38   THEN RW_TAC arith_ss []);
39
40val N_aux_partial_correctness = Q.prove
41(`WF R /\ 
42  (!x. ~(x > 100) ==> R (N_aux R (x + 11)) x) /\
43  (!x. ~(x > 100) ==> R (x + 11) x)
44    ==>
45  !n. N_aux R n = if n>100 then n-10 else 91`,
46 STRIP_TAC THEN recInduct N_aux_ind
47   THEN RW_TAC arith_ss [] 
48   THEN RW_TAC arith_ss [E]);
49
50(*---------------------------------------------------------------------------*)
51(* Termination of 91 is a bit tricky.                                        *)
52(*---------------------------------------------------------------------------*)
53
54val lem = DECIDE ``~(x > 100) ==> (101-y < 101-x = x<y)``;
55
56val unexpand_measure = Q.prove
57(`(\x' x''. 101 < x' + (101 - x'') /\ x'' < 101) = measure \x. 101-x`,
58 RW_TAC arith_ss [FUN_EQ_THM, measure_thm]);
59
60(*---------------------------------------------------------------------------*)
61(* Get the auxiliary rec. eqns, instantiate with termination relation, and   *)
62(* do some simplifications.                                                  *)
63(*---------------------------------------------------------------------------*)
64
65val condE = 
66  SIMP_RULE arith_ss [AND_IMP_INTRO,WF_measure,measure_thm,SUB_LEFT_LESS] 
67        (Q.INST [`R` |-> `measure \x. 101-x`] E);
68
69val correctness' =
70  SIMP_RULE arith_ss [WF_measure,measure_thm,SUB_LEFT_LESS] 
71        (Q.INST [`R` |-> `measure \x. 101-x`] (N_aux_partial_correctness));
72
73val N_aux_ind' = (* takes ages, because of subtraction? *)
74  SIMP_RULE arith_ss [WF_measure,measure_thm,SUB_LEFT_LESS] 
75        (Q.INST [`R` |-> `measure \x. 101-x`] (DISCH_ALL N_aux_ind));
76
77(*---------------------------------------------------------------------------*)
78(* Termination. This is done the hard way, to prop up an obscure point.      *)
79(* We'll use NA to abbreviate the instantiated auxiliary function: thus      *)
80(* NA = N_aux(measure($- 101)). The proof goes as follows:                   *)
81(*                                                                           *)
82(* Induct on the termination relation, then tidy up the goal, obtaining the  *)
83(* goal "x < NA (x+11)". We now want to unroll NA(x+11). This requires       *)
84(* manually instantiating the auxiliary fn with `x+11`, and proving its      *)
85(* constraints. One of these is                                              *)
86(*                                                                           *)
87(*   x+11 < NA (x+22)           (%%)                                         *)
88(*                                                                           *)
89(* We will prove this by using the IH, by means of first doing a case split  *)
90(* on "x+11 > 100". Having (%%) allows NA(x+11) to be unrolled, but we will  *)
91(* also keep (%%) around for later use. Now  conditional rewriting will      *)
92(* unroll "NA(x+11)" yielding the goal "x < NA(NA(x+22))". Now we want to    *)
93(* unroll NA one more time, at its argument NA(x+22). Again we do a case     *)
94(* split, this time on "NA (x+22) > 100". Consider the two branches coming   *)
95(* from the case split.                                                      *)
96(* Case: NA (x+22) > 100. The goal is easy to prove by arithmetic            *)
97(*       from the assumptions and unrolling NA into the base case.           *)
98(* Case: ~(NA (x+22) > 100). Here the IH may be used with a somewhat clever  *)
99(*       witness to deliver                                                  *)
100(*       NA(x+22) -11 < NA(NA(x+22) -11+11)                                  *)
101(*                    = NA(NA(x+22))                                         *)
102(*       After that, the proof of this branch is also easy.                  *)
103(*---------------------------------------------------------------------------*)
104
105val (N_def,N_ind) = Defn.tprove
106 (N_defn,
107  WF_REL_TAC `measure \x. 101 - x` 
108    THEN RW_TAC arith_ss [SUB_LEFT_LESS,unexpand_measure]
109    THEN Q.ABBREV_TAC `NA = N_aux (measure (\x. 101 - x))`
110    THEN measureInduct_on `(\m. 101 - m) x`
111    THEN STRIP_TAC THEN FULL_SIMP_TAC arith_ss [lem]
112    THEN MP_TAC (Q.INST [`x` |-> `x+11`] condE)
113    THEN RW_TAC arith_ss []  (* implicit case split *)
114    THEN `x+11 < NA(x+22)` by METIS_TAC[DECIDE``x<x+11``,DECIDE``x+11+11=x+22``]
115    THEN RW_TAC std_ss [] THEN WEAKEN_TAC is_imp
116    THEN MP_TAC (Q.INST [`x` |-> `NA(x+22)`] condE) 
117    THEN RW_TAC arith_ss [] (* implicit case split *)
118    THEN `x < NA (x+22) - 11 /\ ~(NA (x + 22) - 11 > 100)` by DECIDE_TAC
119    THEN `NA(x+22) - 11 < NA(NA(x+22) - 11 + 11)` by METIS_TAC[]
120    THEN POP_ASSUM MP_TAC
121    THEN FULL_SIMP_TAC arith_ss [DECIDE ``x+y < p ==> ((p-y)+y = p)``]);
122
123(*---------------------------------------------------------------------------
124      Note that the above development is slightly cranky, since
125      the partial correctness theorem has constraints remaining. 
126      These were addressed by the termination proof, but the 
127      constraints were proved and then thrown away. 
128
129      Now try some computations with N.
130 ---------------------------------------------------------------------------*)
131
132EVAL ``N 0``;
133EVAL ``N 10``;
134EVAL ``N 11``;
135EVAL ``N 12``;
136EVAL ``N 40``;
137EVAL ``N 89``;
138EVAL ``N 90``;
139EVAL ``N 99``;
140EVAL ``N 100``;
141EVAL ``N 101``;
142EVAL ``N 102``;
143EVAL ``N 127``;
144