1(*--------------------------------------------------------------------------- 2 An example from Larry Paulson's book "ML for the Working 3 Programmer" (first edition, p. 225): 4 5 "Our approach to program schemes is simpler than resorting 6 to domain theory, but is less general. In domain theory 7 it is simple to prove that any ML function of the form 8 9 fun h x = if p x then x else h(h(g x)) 10 11 satisfies 12 13 h (h x) = h x 14 15 for all x -- regardless of whether the function terminates. Our 16 approach cannot easily handle this. What well-founded relation 17 should we use to demonstrate the termination of the nested 18 recursive call in h?" 19 20 Under our approach, the answer is that the goal should be made 21 contingent on the existence of a termination relation. Then 22 recursion induction is valid, and the desired theorem thereby 23 proved, provided that "h" has been defined by a recursive schema 24 (note that h is schematic in p and g). 25 ---------------------------------------------------------------------------*) 26 27load "bossLib"; open bossLib; 28 29show_assums := true; 30 31 32(*--------------------------------------------------------------------------- 33 The variables p and g are parameters. 34 ---------------------------------------------------------------------------*) 35 36val H_def = TotalDefn.DefineSchema `H x = if p x then x else H (H (g x))`; 37 38 39(*--------------------------------------------------------------------------- 40 H_fact = 41 [!x. ~p x ==> R (H_aux R g p (g x)) x, 42 !x. ~p x ==> R (g x) x, 43 WF R ] 44 |- 45 !x. H g p (H g p x) = H g p x 46 ---------------------------------------------------------------------------*) 47 48val H_fact = TAC_PROOF 49((hyp H_def, Term`!x. H g p (H g p x) = H g p x`), 50 recInduct (fetch "-" "H_ind") 51 THEN RW_TAC std_ss [] 52 THEN ONCE_REWRITE_TAC [H_def] 53 THEN PROVE_TAC [H_def]); 54 55 56(*--------------------------------------------------------------------------- 57 P.S. Notice that, since H is a nested function, the termination 58 conditions of H are really those of an auxiliary function 59 H_aux. In an invocation of Define, the system derives 60 the recursion equations for H_aux but doesn't keep them, 61 since it can derive the recursion equations for H. 62 63 If you want more information, the functions in the Defn 64 structure help: 65 66 val H_defn = 67 Defn.Hol_defn "H" 68 `H x = if p x then x else H (H (g x))`; 69 70 - Defn.eqns_of H_defn; 71 > val it = 72 > [WF R, !x. ~p x ==> R (g x) x, 73 > !x. ~p x ==> R (H_aux R g p (g x)) x] 74 > |- H g p x = (if p x then x else H g p (H g p (g x))) : thm 75 76 val SOME aux_defn = Defn.aux_defn H_defn; 77 > val aux_defn = <defn> : Defn.defn 78 79 Defn.eqns_of aux_defn; 80 > val it = 81 > |- WF R ==> 82 > (~p x ==> R (g x) x) ==> 83 > (~p x ==> R (H_aux R g p (g x)) x) 84 > ==> 85 > (H_aux R g p x = 86 > (if p x then x else H_aux R g p (H_aux R g p (g x)))) :thm 87 88 Defn.ind_of aux_defn;; 89 > val it = 90 > SOME [WF R, !x. ~p x ==> R (g x) x] 91 > |- !P. 92 > (!x. (~p x ==> P (g x)) /\ 93 > (~p x ==> 94 > R (H_aux R g p (g x)) x ==> 95 > P (H_aux R g p (g x))) ==> P x) 96 > ==> 97 > !v. P v : thm option 98 99 100 ---------------------------------------------------------------------------*) 101