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