1(*---------------------------------------------------------------------------
2    Transformation of programs involving "unfold" : the fusion law. 
3 ---------------------------------------------------------------------------*)
4
5show_assums := true;
6open arithmeticTheory;
7
8(*---------------------------------------------------------------------------
9     Datatype of binary trees with data at each internal node.
10 ---------------------------------------------------------------------------*)
11
12Hol_datatype `btree = LEAF 
13                    | NODE of btree => 'a => btree`;
14
15
16(*---------------------------------------------------------------------------
17    Standard primitive recursor over btree.
18 ---------------------------------------------------------------------------*)
19
20val btreeRec_def = 
21 Define
22   `(btreeRec LEAF (v:'a) (f:'a->'b->'a->'a)  = v)
23 /\ (btreeRec (NODE t1 M t2) v f = f (btreeRec t1 v f) M (btreeRec t2 v f))`;
24
25
26
27(*---------------------------------------------------------------------------
28     "unfold" into a btree. The following is not correct, because "more" 
29     and "dest" are not arguments to the function (i.e. things that
30     are recursed on), but rather parameters that have to be filled in
31     before the definition makes sense in a logic of total functions
32     like HOL.
33
34         fun unfold more f x = 
35              if more x 
36               then let (y,a,z) = dest x
37                    in 
38                     NODE (unfold more dest y) a (unfold more dest z)
39               else LEAF
40
41     Following is the right way to define the unfold schema. Since dest 
42     and more are only free in the right hand side, they are treated
43     as parameters in a schematic definition.
44 ---------------------------------------------------------------------------*)
45
46val unfold_def = 
47 TotalDefn.DefineSchema
48     `unfold (x:'a) : 'b btree = 
49        if more x 
50          then let (y1,b,y2) = dest x 
51               in 
52                  NODE (unfold y1) b (unfold y2)
53          else LEAF`;
54
55
56
57(*---------------------------------------------------------------------------
58    val unfold_ind 
59      = 
60    [WF R, !x y1 b y2. more x /\ ((y1,b,y2) = dest x) ==> R y1 x,
61           !x y1 b y2. more x /\ ((y1,b,y2) = dest x) ==> R y2 x]
62    |- !P.
63         (!x.
64            (!y1 b y2. more x /\ ((y1,b,y2) = dest x) ==> P y1) /\
65            (!y1 b y2. more x /\ ((y1,b,y2) = dest x) ==> P y2) ==>
66            P x) ==>
67         !v. P v
68 ---------------------------------------------------------------------------*)
69
70val unfold_ind = theorem "unfold_ind";
71
72
73(*---------------------------------------------------------------------------
74        "fusion" is just a generalization of unfold.
75 ---------------------------------------------------------------------------*)
76
77val fusion_def = 
78 TotalDefn.DefineSchema
79     `fusion (x:'a) = 
80         if more x 
81           then let (y,i,z) = dest x
82                in 
83                   g (fusion y) (i:'b) (fusion z)
84           else (c:'c)`;
85
86
87(*---------------------------------------------------------------------------
88     Prove that unfolding and then reducing is the same as doing 
89     a fusion. 
90 ---------------------------------------------------------------------------*)
91
92val fusion_law = Q.prove
93(`!R dest more.
94     WF R
95     /\ (!x y1 b y2. more x /\ ((y1,b,y2) = dest x) ==> R y2 x) 
96     /\ (!x y1 b y2. more x /\ ((y1,b,y2) = dest x) ==> R y1 x) 
97     ==>
98        !x c g. 
99           btreeRec (unfold dest more x) c g = fusion c dest g more x`,
100REPEAT GEN_TAC THEN STRIP_TAC 
101  THEN recInduct unfold_ind 
102  THEN RW_TAC std_ss []
103  THEN RW_TAC std_ss [Once unfold_def, Once fusion_def]
104  THEN RW_TAC std_ss [btreeRec_def]);
105
106
107
108(*---------------------------------------------------------------------------
109   Now consider a different type: n-ary trees with data at each internal node.
110 ---------------------------------------------------------------------------*)
111
112Hol_datatype `tree = Nde of 'a => tree list`;
113
114val Root_def = Define `Root (Nde a tlist) = a`;
115val Kids_def = Define `Kids (Nde a tlist) = tlist`;
116
117val tree_size_def = snd (TypeBase.size_of "tree");
118
119(*---------------------------------------------------------------------------
120    Recursor over tree.
121 ---------------------------------------------------------------------------*)
122
123val treeRec_defn = Hol_defn
124   "treeRec"
125   `treeRec (Nde x tlist) = f x (MAP treeRec tlist)`;
126
127val (treeRec_def', treeRec_ind) = Defn.tprove
128(treeRec_defn,
129 WF_REL_TAC `^(Lib.el 2 (TotalDefn.guessR treeRec_defn))` THEN
130 Induct THEN RW_TAC list_ss [tree_size_def] THENL
131 [DECIDE_TAC, RES_TAC THEN DECIDE_TAC]);
132
133val treeRec_def = CONV_RULE (DEPTH_CONV ETA_CONV) treeRec_def';
134
135(*---------------------------------------------------------------------------
136     unfold into a list
137 ---------------------------------------------------------------------------*)
138
139val listUnfold_def = 
140 TotalDefn.DefineSchema
141     `listUnfold (x:'a) : 'b list = 
142        if done x then []
143         else f x :: listUnfold (g x)`;
144
145
146(*---------------------------------------------------------------------------
147    List a forest of trees out by levels. The nth element in the result 
148    is the concatentation of the nth levels in the trees.
149 ---------------------------------------------------------------------------*)
150
151val forestLevels_def = 
152 Define
153   `forestLevels = listUnfold NULL (MAP Root) (FLAT o MAP Kids)`;
154
155val tree_size_thm = Q.prove
156(`!t. tree1_size f (Kids t) < tree_size f t`,
157 recInduct treeRec_ind
158  THEN RW_TAC list_ss [tree_size_def, Kids_def]);
159
160
161val tree_size_thm1 = Q.prove
162(`!L1 L2. tree1_size f (L1 ++ L2) = tree1_size f L1 + tree1_size f L2`,
163 Induct THEN RW_TAC list_ss [tree_size_def]);
164
165
166val term_lem = Q.prove
167(`!x :'a tree list.
168      ~NULL x ==>
169          tree1_size (\v.0) (FLAT (MAP Kids x)) < tree1_size (\v.0) x`,
170 Induct THEN RW_TAC list_ss []
171   THEN FULL_SIMP_TAC list_ss [tree_size_def]
172   THEN Cases_on `x` THENL
173   [RW_TAC list_ss [tree_size_def]
174     THEN PROVE_TAC [tree_size_thm,LESS_TRANS,DECIDE (Term `x < x+1`)],
175   RW_TAC std_ss [tree_size_thm1] 
176     THEN FULL_SIMP_TAC std_ss [listTheory.NULL]
177     THEN MATCH_MP_TAC (DECIDE (Term`c<b /\ a<d ==> a+c < b+d`))
178     THEN PROVE_TAC [tree_size_thm,LESS_TRANS,DECIDE (Term `x < x+1`)]]);
179
180
181val listUnfold_def' = 
182 SIMP_RULE arith_ss [prim_recTheory.measure_thm,
183                     prim_recTheory.WF_measure,
184                     term_lem]
185   (Q.INST [`R`    |-> `measure (tree1_size (\v.0))`,
186            `done` |-> `NULL`,
187            `f`    |-> `MAP Root`,
188            `g`    |-> `FLAT o MAP Kids`] 
189         (INST_TYPE [alpha |-> Type `:'a tree list`,
190                     beta  |-> Type `:'a list`] 
191                   (DISCH_ALL listUnfold_def)));
192
193val forestLevels_eqns = Q.prove
194(`forestLevels tlist =
195    if NULL tlist then [] 
196     else MAP Root tlist::forestLevels (FLAT (MAP Kids tlist))`,
197 MATCH_ACCEPT_TAC (REWRITE_RULE [GSYM forestLevels_def] listUnfold_def'));
198
199val treeLevels_def = 
200 Define
201   `treeLevels tree = forestLevels [tree]`;
202
203
204(*---------------------------------------------------------------------------
205    Breadth-first traversal is just flattening the result of treeLevels.
206    But you could ask for more efficiency, and derive this by using
207    "deforestation", or fusion. See bfs in this directory.
208 ---------------------------------------------------------------------------*)
209
210
211