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