lisp-runtime/garbage-collector/stop_and_copyScript.sml

352 val D1 = Define `D1 m i = ?k x y z. (m (k:num) = H_BLOCK(x,y,z)) /\ i IN ADDR_SET x`;
356 val DR1 = Define `DR1 m k = D1 m k \/ R1 m k`
665   ``(D0(CUT(j,j)m) = {}) /\ (D1(CUT(j,j)m) = {}) /\
669   \\ ASM_SIMP_TAC std_ss [IN_DEF,D0,R0,D1,R1,CUT_EQ]);
692       ?h2 f2. gc_inv (h1,roots1,h2,f2) (b,i,j2,e,b2,e2,m2,z UNION (D1(CUT(j,j2)m2))) /\ j <= j2 /\
779   \\ `D1 (CUT (j,j + y + 1) ((j =+ H_BLOCK (x,y,d)) m)) = ADDR_SET x` by
780      (FULL_SIMP_TAC std_ss [FUN_EQ_THM,D1,CUT_EQ,IN_DEF,APPLY_UPDATE_THM,EMP_RANGE_def]
810   ``b <= i /\ i <= j ==> (D1(CUT(b,j)m) = D1(CUT(b,i)m) UNION D1(CUT(i,j)m)) /\
812   SIMP_TAC std_ss [EXTENSION,IN_UNION] \\ SIMP_TAC std_ss [IN_DEF,D1,CUT_EQ,D0]
818     (D1 (CUT (j,j + y + 1) m) = ADDR_SET x)``,
819   FULL_SIMP_TAC std_ss [FUN_EQ_THM,D1,CUT_EQ,IN_DEF,APPLY_UPDATE_THM,EMP_RANGE_def]
864         ?h3 f3. gc_inv (h1,roots1,h3,f3) (b,i,j2,e,b2,e2,m2,z UNION (D1(CUT(j,j2)m2))) /\ j <= j2 /\
880        `z UNION D1(CUT(j,j3)(m3:num -> ('a,'b) heap_element))`,
899   \\ `D1 (CUT (j,j4) m4) = D1 (CUT (j,j3) m4) UNION D1 (CUT (j3,j4) m4)`
908   ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,D1(CUT(i,j)m)) ==> ~(i = j) ==>
913              (D1 (CUT (i,j) m) = D1 (CUT (i+n+1,j) m) UNION ADDR_SET xs)``,
920   \\ `D1 (CUT (i,j) m) = D1 (CUT (i+n+1,j) m) UNION ADDR_SET xs`
958   ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,D1(CUT(i,j)m)) /\ ~(i = j) ==>
960     ?h3 f3. gc_inv (h1,roots1,h3,f3) (b,i2,j2,e,b2,e2,m2,D1(CUT(i2,j2)m2)) /\
979   \\ `D1 (CUT (i + n + 1,j) m3) UNION D1 (CUT (j,j3) m3) = D1 (CUT (i + n + 1,j3) m3)`
1022           D1 (CUT (i + n + 1,j3) m3),f3)` \\ ASM_SIMP_TAC std_ss []
1058       gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,D1(CUT(i,j)m)) ==>