examples/dev/composeScript.sml

37 (* Function used with PAT_X_ASSUM:   PAT_X_ASSUM <term> kill                     *)
40 val kill = (fn theorem => K ALL_TAC theorem);
995       THEN (Q.PAT_X_ASSUM `~(start t)` kill) THEN (Q.PAT_X_ASSUM `start (t+1)` kill)
1006       THEN (Q.PAT_X_ASSUM `te > 0` kill)
1026                !t. t0 < t /\ t <= t1 - 1 ==> ~s t` kill
1027       THEN Q.PAT_X_ASSUM `t < tte` kill
1028       THEN REPEAT (Q.PAT_X_ASSUM `tte <= tte ==> X tte` kill)
1032       THEN Q.PAT_X_ASSUM `done t`   kill THEN Q.PAT_X_ASSUM `POSEDGE load (t + 1)` kill
1033       THEN Q.PAT_X_ASSUM `done_e t` kill (* THEN Q.PAT_X_ASSUM `done_e te` kill *)
1034       THEN Q.PAT_X_ASSUM `done_f t` kill THEN Q.PAT_X_ASSUM `done_g t` kill
1046          THEN REPEAT (Q.PAT_X_ASSUM `POSEDGE start_f X` kill)
1064          THEN REPEAT (Q.PAT_X_ASSUM `HOLDF (tte+1+1,tf+1) Z` kill)
1065          THEN Q.PAT_X_ASSUM `!tt. tte+1+1 <= tt /\ tt < tf+1 ==> ~(POSEDGE start tt)` kill
1066          THEN Q.PAT_X_ASSUM `te < tf` kill
1087          THEN REPEAT (Q.PAT_X_ASSUM `!tt. X ==> ~start_g tt` kill)
1088          THEN REPEAT (Q.PAT_X_ASSUM `!tt. X ==> ~(POSEDGE start_g tt)` kill)
1089          THEN REPEAT (Q.PAT_X_ASSUM `tte < tf` kill)
1101          THEN Q.PAT_X_ASSUM `HOLDF (tte+1,tf) done` kill
1102          THEN Q.PAT_X_ASSUM `HOLDF (te,tf) done` kill
1103          THEN TRY (Q.PAT_X_ASSUM `(done:(num->bool)) (t:num)` kill)
1104          THEN TRY (Q.PAT_X_ASSUM `(done_e:(num->bool)) (t:num)` kill)
1105          THEN Q.PAT_X_ASSUM `HOLDF (t + 1,te) done_e` kill
1106          THEN Q.PAT_X_ASSUM `(done_e:(num->bool)) (te:num)` kill
1107          THEN Q.PAT_X_ASSUM `POSEDGE start' te` kill
1108          THEN TRY (Q.PAT_X_ASSUM `(done_f:(num->bool)) (t:num)` kill)
1109          THEN Q.PAT_X_ASSUM `(done_f:(num->bool)) (tte:num)` kill
1110          THEN Q.PAT_X_ASSUM `(done_g:(num->bool)) (tte:num)` kill
1111          THEN Q.PAT_X_ASSUM `(start_f:(num->bool)) (te:num)` kill
1112          THEN Q.PAT_X_ASSUM `HOLDF (tte + 1,tf) done_f` kill
1113          THEN Q.PAT_X_ASSUM `(done_f:(num->bool)) (tf:num)` kill
1114          THEN Q.PAT_X_ASSUM `!tt. te < tt /\ tt <= tf ==> ~POSEDGE start tt` kill
1115          THEN Q.PAT_X_ASSUM `(done_e:(num->bool)) (tf:num)` kill
1116          THEN Q.PAT_X_ASSUM `!tt. te <= tt /\ tt <= tf ==> done_e tt` kill
1117          THEN Q.PAT_X_ASSUM `!tt. te < tt /\ tt <= tf ==> ~POSEDGE done_e tt` kill
1118          THEN Q.PAT_X_ASSUM `!tt. te < tt /\ tt <= tf ==> ~start' tt` kill
1119          THEN Q.PAT_X_ASSUM ` ~((start_g:(num->bool)) (te:num))` kill
1120          THEN Q.PAT_X_ASSUM `tf <= tf ==> (done_g:(num->bool)) (tf:num)` kill
1121          THEN Q.PAT_X_ASSUM `(done_g:(num->bool)) (tf:num)` kill
1132          THEN Q.PAT_X_ASSUM `!tt. (t+1+1) <= tt /\ tt < (te+1) ==> ~(c1 tt)` kill
1133          THEN Q.PAT_X_ASSUM `!tt. 0 < (t+1) /\ (t+1) < tt /\ tt <= te ==> ~(c1 tt)` kill
1134          THEN Q.PAT_X_ASSUM `HOLDF (t+1,te) done` kill
1140          THEN Q.PAT_X_ASSUM `!tt. 0 < (t+1) /\ (t+1) < tt /\ tt <= te ==> ~(start tt)` kill
1142                (q tt = inp (t+1))` kill
1151          THEN Q.PAT_X_ASSUM `!tt. 0 < te /\ te < tt /\ tt <= tf ==> done_e tt` kill
1153                    (sel t = data_e te)` kill
1166          THEN REPEAT (Q.PAT_X_ASSUM `POSEDGE start_f X` kill)
1180          THEN REPEAT (Q.PAT_X_ASSUM `HOLDF (tte+1+1,tg+1) Z` kill)
1181          THEN Q.PAT_X_ASSUM `!tt. tte+1+1 <= tt /\ tt < tg+1 ==> ~(POSEDGE start tt)` kill
1182          THEN Q.PAT_X_ASSUM `te < tg` kill
1203          THEN REPEAT (Q.PAT_X_ASSUM `!tt. X ==> ~start_f tt` kill)
1204          THEN REPEAT (Q.PAT_X_ASSUM `!tt. X ==> ~(POSEDGE start_f tt)` kill)
1205          THEN REPEAT (Q.PAT_X_ASSUM `tte < tg` kill)
1217          THEN Q.PAT_X_ASSUM `HOLDF (tte+1,tg) done` kill
1218          THEN Q.PAT_X_ASSUM `HOLDF (te,tg) done` kill
1219          THEN TRY (Q.PAT_X_ASSUM `(done:(num->bool)) (t:num)` kill)
1220          THEN TRY (Q.PAT_X_ASSUM `(done_e:(num->bool)) (t:num)` kill)
1221          THEN Q.PAT_X_ASSUM `HOLDF (t + 1,te) done_e` kill
1222          THEN Q.PAT_X_ASSUM `(done_e:(num->bool)) (te:num)` kill
1223          THEN Q.PAT_X_ASSUM `POSEDGE start' te` kill
1224          THEN TRY(Q.PAT_X_ASSUM `(done_f:(num->bool)) (t:num)` kill)
1225          THEN Q.PAT_X_ASSUM `(done_f:(num->bool)) (tte:num)` kill
1226          THEN Q.PAT_X_ASSUM `(done_g:(num->bool)) (tte:num)` kill
1227          THEN Q.PAT_X_ASSUM `(start_g:(num->bool)) (te:num)` kill
1228          THEN Q.PAT_X_ASSUM `HOLDF (tte + 1,tg) done_g` kill
1229          THEN Q.PAT_X_ASSUM `(done_g:(num->bool)) (tg:num)` kill
1230          THEN Q.PAT_X_ASSUM `!tt. te < tt /\ tt <= tg ==> ~POSEDGE start tt` kill
1231          THEN Q.PAT_X_ASSUM `(done_e:(num->bool)) (tg:num)` kill
1232          THEN Q.PAT_X_ASSUM `!tt. te <= tt /\ tt <= tg ==> done_e tt` kill
1233          THEN Q.PAT_X_ASSUM `!tt. te < tt /\ tt <= tg ==> ~POSEDGE done_e tt` kill
1234          THEN Q.PAT_X_ASSUM `!tt. te < tt /\ tt <= tg ==> ~start' tt` kill
1235          THEN Q.PAT_X_ASSUM ` ~((start_f:(num->bool)) (te:num))` kill
1236          THEN Q.PAT_X_ASSUM `tg <= tg ==> (done_f:(num->bool)) (tg:num)` kill
1237          THEN Q.PAT_X_ASSUM `(done_f:(num->bool)) (tg:num)` kill
1247          THEN Q.PAT_X_ASSUM `!tt. (t+1+1) <= tt /\ tt < (te+1) ==> ~(c1 tt)` kill
1248          THEN Q.PAT_X_ASSUM `!tt. 0 < (t+1) /\ (t+1) < tt /\ tt <= te ==> ~(c1 tt)` kill
1249          THEN Q.PAT_X_ASSUM `HOLDF (t+1,te) done` kill
1255          THEN Q.PAT_X_ASSUM `!tt. 0 < (t+1) /\ (t+1) < tt /\ tt <= te ==> ~(start tt)` kill
1257                           (q tt = inp (t+1))` kill
1265          THEN Q.PAT_X_ASSUM `!tt. 0 < te /\ te < tt /\ tt <= tg ==> done_e tt` kill
1267                    (sel t = data_e te)` kill
1464      Q.PAT_X_ASSUM `!(m:num). (m:num) < v ==> X` kill (* delete the ind hyp *)
1615      Q.PAT_X_ASSUM `done_e (t:num)` kill
1616      THEN Q.PAT_X_ASSUM `done_f ((t:num) + 1)` kill
1617      THEN Q.PAT_X_ASSUM `done_g ((t:num) + 1)` kill
1618      THEN Q.PAT_X_ASSUM `POSEDGE start_e ((t:num) + 1)` kill
1619      THEN Q.PAT_X_ASSUM `HOLDF ((t:num) + 1,te) done_e` kill
1620      THEN Q.PAT_X_ASSUM `data_e (te:num) = X` kill
1621      THEN Q.PAT_X_ASSUM `data_e (te:num)` kill
1622      THEN Q.PAT_X_ASSUM `POSEDGE start_f (te:num)` kill
1623      THEN Q.PAT_X_ASSUM `done_f ((te:num) - 1)` kill
1624      THEN Q.PAT_X_ASSUM `done_f (tf:num)` kill
1625      THEN Q.PAT_X_ASSUM `(tf:num) > t + 1` kill
1626      THEN Q.PAT_X_ASSUM `out (tf:num) = X` kill
1627      THEN Q.PAT_X_ASSUM `HOLDF ((t:num) + 1,tf) done` kill
1628      THEN Q.PAT_X_ASSUM `(te:num) > t+1` kill
1630      THEN Q.PAT_X_ASSUM `HOLDF ((tte:num)+1,tf) done_f` kill
1633      THEN Q.PAT_X_ASSUM `(tte:num) = te - 1` kill
1634      THEN Q.PAT_X_ASSUM `(tte:num)+1 = te` kill
1635      THEN Q.PAT_X_ASSUM `(tf:num) > tte + 1` kill
1640      THEN REPEAT (Q.PAT_X_ASSUM `POSEDGE_IMP X` kill)
1641      THEN REPEAT (Q.PAT_X_ASSUM `DEL X` kill)
1642      THEN REPEAT (Q.PAT_X_ASSUM `AND X` kill)
1643      THEN Q.PAT_X_ASSUM `OR ((start:num->bool),sel,start_e)` kill
1644      THEN Q.PAT_X_ASSUM `MUX X` kill
1645      THEN Q.PAT_X_ASSUM `NOT X` kill
1652      THEN REPEAT (Q.PAT_X_ASSUM `!(t:num). X` kill)
1653      THEN TRY (Q.PAT_X_ASSUM `data_e (te:num) = X` kill)
1654      THEN Q.PAT_X_ASSUM `!(x:'a). ~f1 x ==> X` kill
1655      THEN Q.PAT_X_ASSUM `out (tf:num) = X` kill
1656      THEN Q.PAT_X_ASSUM `(v:num) = variant (inp_e (t + 1))` kill
1721      Q.PAT_X_ASSUM `!(m:num). m < X ==> Y` kill
1734      Q.PAT_X_ASSUM `!(m:num). m < X ==> Y` kill
1752      Q.PAT_X_ASSUM `!(m:num). m < X ==> Y` kill
1829      Q.PAT_X_ASSUM `!(m:num). m < X ==> Y` kill
1849      Q.PAT_X_ASSUM `!(m:num). m < X ==> Y` kill
1875      Q.PAT_X_ASSUM `!(m:num). m < X ==> Y` kill
1988      Q.PAT_X_ASSUM `!(m:num). m < X ==> Y` kill
1996      THEN Q.PAT_X_ASSUM `variant X < Y ==> Z` kill
2022      THEN Q.PAT_X_ASSUM `(variant (f3 (inp_e (t+1))) = variant (inp_e (ttg+1))) ==> X` kill
2101                          ~POSEDGE start_e (t + 1) ==> done_e (t + 1)` kill
2103                        COMPUTE (t,f1,inp_e,done_e,data_e)` kill
2105                          COMPUTE (t,f2,q,done_f,out)` kill
2107                          COMPUTE (t,f3,q,done_g,data_g)` kill
2109                          done_f (t + 1)` kill
2111                          done_g (t + 1)` kill
2115      THEN (REPEAT (Q.PAT_X_ASSUM `HOLDF Y X ==> Z` kill))