1(*---------------------------------------------------------------------------
2           Transformations for linear recursion.
3 ---------------------------------------------------------------------------*)
4
5open TotalDefn;
6
7show_assums := true;
8
9(*---------------------------------------------------------------------------
10       Definitions of schemas for linear recursion, 
11       continuation-passing style, and accumulator style.
12 ---------------------------------------------------------------------------*)
13
14val linRec_eqn = 
15 DefineSchema
16    `linRec (x:'a) = if atomic x then A x 
17                     else join (linRec (dest x)) (D x:'b)`;
18
19val cpRec_def0 = 
20 DefineSchema
21    `cpRec (x:'a, (f:'b -> 'c)) = 
22        if atomic x then f (A x) 
23        else cpRec (dest x, \u:'b. f (join u (D x:'b)))`;
24
25val accRec_def0 = 
26 DefineSchema
27    `accRec (x:'a, u:'b) = 
28        if atomic x then join (A x) u
29        else accRec (dest x, join (D x:'b) u)`;
30
31
32(*---------------------------------------------------------------------------
33      Minor massaging of definitions in order to clean up the TCs.
34 ---------------------------------------------------------------------------*)
35
36fun ID_SPEC thm = SPEC (#Bvar(Rsyntax.dest_forall(concl thm))) thm;
37
38val [cpRec_eqn, cpRec_ind] = CONJUNCTS
39(UNDISCH
40 (REWRITE_RULE pairTheory.pair_rws
41   (BETA_RULE (REWRITE_RULE[relationTheory.inv_image_def]
42      (REWRITE_RULE[UNDISCH (ISPEC (Term`FST:'a#('b->'c)->'a`)
43                              (ID_SPEC relationTheory.WF_inv_image))]
44        (INST [Term`R :'a # ('b -> 'c) -> 'a # ('b -> 'c) -> bool`
45                |->
46               Term`inv_image R (FST :'a # ('b -> 'c) -> 'a)`]
47         (DISCH_ALL (CONJ cpRec_def0 (fetch "-" "cpRec_ind")))))))));
48
49val [accRec_eqn, accRec_ind] = CONJUNCTS
50(UNDISCH
51 (REWRITE_RULE pairTheory.pair_rws
52   (BETA_RULE (REWRITE_RULE[relationTheory.inv_image_def]
53      (REWRITE_RULE[UNDISCH (ISPEC (Term`FST:'a#'b->'a`)
54                              (ID_SPEC relationTheory.WF_inv_image))]
55        (INST [Term`R :'a#'b -> 'a#'b -> bool`
56                 |->
57               Term`inv_image R (FST :'a#'b -> 'a)`]
58         (DISCH_ALL (CONJ accRec_def0 (theorem "accRec_ind")))))))));
59
60
61(* To overwrite old theorems
62
63    save_thm("cpRec_def", cpRec_eqn);
64    save_thm("cpRec_ind", cpRec_ind);
65    save_thm("accRec_def", accRec_eqn);
66    save_thm("accRec_ind", accRec_ind);
67*)
68
69val cpRec_eq_linRec = Q.prove
70(`!R atomic A join dest D.
71    WF R 
72     /\ (!x. ~(atomic x) ==> R (dest x) x)
73     ==> 
74      !x f. cpRec A D atomic dest join (x, f) 
75              = 
76            f (linRec A D atomic dest join x)`,
77REPEAT GEN_TAC THEN STRIP_TAC
78  THEN recInduct (theorem "linRec_ind")
79  THEN RW_TAC std_ss [] 
80  THEN ONCE_REWRITE_TAC[linRec_eqn] THEN ONCE_REWRITE_TAC[cpRec_eqn] 
81  THEN RW_TAC std_ss []);
82
83
84val accRec_eq_cpRec = Q.prove
85(`!R atomic A join dest D.
86    WF R 
87    /\ (!x. ~atomic x ==> R (dest x) x) 
88    /\ (!p q r:'b. join p (join q r) = join (join p q) r)
89     ==> 
90      !x u. accRec A D atomic dest join (x,u) 
91              = 
92            cpRec A D atomic dest join (x, \w. join w u)`,
93REPEAT GEN_TAC THEN STRIP_TAC
94  THEN recInduct accRec_ind THEN RW_TAC std_ss []
95  THEN ONCE_REWRITE_TAC[cpRec_eqn] THEN ONCE_REWRITE_TAC[accRec_eqn] 
96  THEN RW_TAC std_ss []);
97
98
99(*---------------------------------------------------------------------------
100     Ergo, we have the following equality between linear and 
101     accumulator recursions ... this can also be proved directly
102     via an equally easy proof.
103 ---------------------------------------------------------------------------*)
104
105val linRec_eq_accRec = Q.prove
106(`!R atomic A join dest D.
107    WF R 
108    /\ (!x. ~(atomic x) ==> R (dest x) x)
109    /\ (!p q r:'b. join p (join q r) = join (join p q) r)
110     ==> 
111      !x u. join (linRec A D atomic dest join x) u 
112              = 
113            accRec A D atomic dest join (x,u)`,
114REPEAT STRIP_TAC   (* weakness in solver forces use of IMP_RES_THEN *)
115  THEN IMP_RES_THEN (fn th => RW_TAC std_ss [th]) accRec_eq_cpRec
116  THEN IMP_RES_THEN (fn th => RW_TAC std_ss [th]) cpRec_eq_linRec);
117
118
119(*---------------------------------------------------------------------------
120              Two versions of reverse.
121 ---------------------------------------------------------------------------*)
122
123val rev_def = 
124 Define
125    `rev = linRec (*  A  *)    (\x.x)       
126                  (*  D  *)    (\l. [HD l]) 
127                  (* atomic *) NULL
128                  (*  dest  *) TL           
129                  (*  join  *) APPEND`;
130
131
132val frev_def = 
133 Define
134    `frev l a = accRec (*  A  *)    (\x.x)
135                       (*  D  *)    (\l. [HD l])
136                       (* atomic *)  NULL
137                       (*  dest  *)  TL
138                       (*  join  *)  APPEND
139                       (l,a)`;
140
141
142(*---------------------------------------------------------------------------
143      Equivalence of the two forms of reverse. First, instantiate
144      the program transformation "sufficiently".
145 ---------------------------------------------------------------------------*)
146
147val lem0 = GEN_ALL (DISCH_ALL (GSYM 
148             (UNDISCH_ALL (SPEC_ALL 
149               (Q.ISPEC `measure LENGTH` linRec_eq_accRec)))));
150
151val lem1 = Q.prove
152(`!x. ~NULL x ==> measure LENGTH (TL x) x`,
153Cases 
154  THEN RW_TAC list_ss [prim_recTheory.measure_def,
155                       relationTheory.inv_image_def]);
156
157
158val rev_eq_frev = Q.prove
159(`!l x. rev l = frev l []`,
160RW_TAC list_ss [rev_def, frev_def, lem0, lem1, prim_recTheory.WF_measure]);
161
162
163(*---------------------------------------------------------------------------
164    The natural way to apply these rewrites seems to be to let the
165    user write something in a simple style and then let the
166    system do some waily higher-order matching in order to choose
167    and apply a transformation. Even after the transformation has 
168    been applied, the new recursion equations may have to be simplified
169    in order to be intelligible to the user.
170 ---------------------------------------------------------------------------*)
171