machine-code/garbage-collectors/lisp_gcScript.sml

167   ``!a. ref_cheney (m,e) (a,d,xs,ys) /\ x <= e ==> ~(ref_field a (x,xx) = 0w)``,
169   \\ Cases_on `xx` \\ Cases_on `r`
267     (arm_move(ref_addr a j,ref_field a (x,xx),r7,r8,d,xs) = (j2,x2,r7_2,r8_2,d2,xs2)) ==>
268     ref_cheney (m1,e) (a,d,xs2,ys) /\ (x2 = ref_field a (x1,xx)) /\ (j2 = ref_addr a j1) /\ (d2 = d) /\
269     arm_move_pre(ref_addr a j,ref_field a (x,xx),r7,r8, d, xs)``,
275   THEN1 (Cases_on `xx` \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [])
337   ``!a b b' i j j2 j3 e m m2 w ww r x xj2 xx2 xs xs2 d x2 xx  r7 r8 r7_2 r8_2 d2.
340     (arm_move(ref_addr a j,ref_field a (x,xx),r7,r8, d, xs) = (xj2,xx2,r7_2,r8_2,d2,xs2)) ==>
344     (ref_field a (x2,xx) = xx2) /\ (ref_addr a j2 = xj2) /\ (d = d2) /\
345     arm_move_pre(ref_addr a j,ref_field a (x,xx), r7,r8, d, xs)``,
370   ``ref_cheney_inv (b,i,j,j,e,f,m,x,xx,r) (a,r3,r4,d,xs,ys) /\ ~(i = j) /\
373     ref_cheney_inv (b,i',j',j',e',f,m',x,xx,r) (a,r3',r4',d,xs',ys) /\ (d = d') /\
376   \\ `cheney_inv (b,b,i',j',j',e',f,m',x,xx,r)` by METIS_TAC [cheney_inv_step]
419        Q.SPECL [`a`,`b`,`b`,`i`,`j`,`j2`,`j`,`e`,`m`,`m2`,`x`,`xx`,`r`,`ax`,`r41`,`r52`,`xs`,`xs1`,`d`,`x2`,`ad`,`r7`,`r8`,`r71`,`r81`,`d1`]) ref_cheney_move
423        Q.SPECL [`a`,`b`,`b`,`i`,`j2`,`j3`,`j`,`e`,`m2`,`m3`,`x`,`xx`,`r`,`ay`,`r42`,`r62`,`xs1`,`xs2`,`d1`,`y3`,`ad1`,`r71`,`r81`,`r72`,`r82`,`d2`]) ref_cheney_move
425   \\ REPEAT (Q.PAT_X_ASSUM `!xx.bb` (K ALL_TAC))
426   \\ REPEAT (Q.PAT_X_ASSUM `ccc ==> !xx.bb` (K ALL_TAC))
457       ref_cheney_inv (b,i,j,j,e,f,m,x,xx,r) (a,r3,r4,d,xs,ys) /\
460       ref_cheney_inv (b,i',i',i',e,f,m',x,xx,r) (a,r3',r4',d,xs',ys) /\ (d2 = d) /\
470   \\ Q.PAT_X_ASSUM `ref_cheney_inv (b,i,j,j,e,f,m,x,xx,r) (a,r3,r4,d,xs,ys)`
486   \\ `ref_cheney_inv (b,i2,j2,j2,e2,f,m2,x,xx,r) (a,r31,r41,d,xs1,ys) /\ (d = d1) /\
737       Q.INST [`xx`|->`m`,`ys`|->`xs3`,`f`|->`l+l+1`,`d`|->`x`])
1606      (REPEAT (Q.PAT_X_ASSUM `!xx.yy` (K ALL_TAC))
1623       \\ REPEAT (Q.PAT_X_ASSUM `!xx.yy` (K ALL_TAC))
1630      (REPEAT (Q.PAT_X_ASSUM `!xx.yy` (K ALL_TAC))
1646      (REPEAT (Q.PAT_X_ASSUM `!xx.yy` (K ALL_TAC))
1652     \\ REPEAT (Q.PAT_X_ASSUM `!xx.yy` (K ALL_TAC))
2110     \\ REPEAT (Q.PAT_X_ASSUM `ww = ref_field a (xx,yy)` (K ALL_TAC))
2159   \\ Q.ABBREV_TAC `xx = (FST (heap_el a v1),FST (heap_el a v2),SND (heap_el a v1),
2161   \\ Q.ABBREV_TAC `hh = build_heap (k,b,a,m) |+ (f,xx)`
2163       (hh ' (FST (f,SND (heap_el a v1))) = xx)` by
2166   \\ Q.UNABBREV_TAC `xx`