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