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