machine-code/garbage-collectors/improved_gcScript.sml

351 val D0 = Define `D0 m k = ?x y z. m (k:num) = H_BLOCK (x,y,z)`;
355 val DR0 = Define `DR0 m k = D0 m k \/ R0 m k`
442     abs_steps (h1,{},{},ADDR_SET roots1,I) (h,D0(CUT(b,i)m),D0(CUT(i,j)m),z,f)`;
450     abs_gc_inv (h1,roots1) (h,D0(CUT(b,i)m),D0(CUT(i,j)m),z,f)``,
456     abs_gc_inv (h1,roots1) (h,D0(CUT(b,i)m),D0(CUT(i,j)m),z,f)``,
624   \\ FULL_SIMP_TAC std_ss [gc_inv_def] \\ FULL_SIMP_TAC std_ss [DR0,R0,D0,CUT_EQ]
634        \\ `n IN D0 (CUT (i,j) m) \/ n IN D0 (CUT (b,i) m)` by METIS_TAC []
635        \\ FULL_SIMP_TAC std_ss [D0,CUT_EQ,IN_DEF] \\ RANGE_TAC)
647   ``(D0(CUT(j,j)m) = {}) /\ (D1(CUT(j,j)m) = {}) /\
651   \\ ASM_SIMP_TAC std_ss [IN_DEF,D0,R0,D1,R1,CUT_EQ]);
706       (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [IN_DEF,R0,D0,DR0,EMP_RANGE_def,
716     \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,DR0,IN_DEF,D0,R0,CUT_EQ,APPLY_UPDATE_THM]
748   \\ `D0 (CUT (i,j + y + 1) ((j =+ H_BLOCK (x,y,d)) m)) =
749        j INSERT D0 (CUT (i,j) m)` by
751       \\ FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,APPLY_UPDATE_THM,EMP_RANGE_def,IN_DEF]
765   \\ Q.EXISTS_TAC `(h,D0 (CUT (b,i) m),D0 (CUT (i,j) m),z UNION {n},f)`
768   \\ Q.EXISTS_TAC `(h |+ (j,x,y,d) \\ n,D0 (CUT (b,i) m),j INSERT D0 (CUT (i,j) m),
789                          (D0(CUT(b,j)m) = D0(CUT(b,i)m) UNION D0(CUT(i,j)m))``,
790   SIMP_TAC std_ss [EXTENSION,IN_UNION] \\ SIMP_TAC std_ss [IN_DEF,D1,CUT_EQ,D0]
881   ``!i x m. i IN D0 m ==> (D0 ((i =+ H_BLOCK x) m) = D0 m)``,
882   SIMP_TAC std_ss [FORALL_PROD,FUN_EQ_THM,IN_DEF,D0,CUT_EQ,APPLY_UPDATE_THM]
903     \\ `i IN (UNIV DIFF D0 (CUT (b,i) m))` by
905        \\ FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11] \\ RANGE_TAC)
906     \\ `ADDR_SET xs SUBSET POINTERS h (UNIV DIFF D0 (CUT (b,i) m))`
908     \\ `D0 (CUT (b,i) m) UNION D0 (CUT (i,j) m) = D0 (CUT(b,j)m)`
910     \\ `ADDR_SET xs SUBSET (FDOM h UNION HAS_CHANGED f DIFF (D0 (CUT (b,j) m)))` by
913     \\ `x IN (FDOM h UNION HAS_CHANGED f DIFF D0 (CUT (b,j) m))` by SET_TAC
915      (`~(x IN D0 (CUT (b,j) m))` by SET_TAC
916       \\ POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ]
919       \\ FULL_SIMP_TAC std_ss [heap_element_11,DR0,D0,R0,CUT_EQ,
924     \\ Q.PAT_X_ASSUM `~(x IN D0 (CUT (b,j) m))` MP_TAC
925     \\ SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ]
929     \\ FULL_SIMP_TAC std_ss [heap_element_distinct,DR0,D0,R0,CUT_EQ,heap_element_11]
964   \\ `i IN D0 (CUT (b,i + n + 1) m3) /\
972       \\ FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11])
981    (FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11]
992   \\ Q.EXISTS_TAC `(h3,D0 (CUT (b,i) m3),D0 (CUT (i,j3) m3),
1007   \\ ASM_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11]
1062   \\ SIMP_TAC std_ss [DR0,D0,R0,CUT_EQ,IN_DEF] \\ DISJ1_TAC
1103   \\ Q.EXISTS_TAC `DRESTRICT h4 (D0 (CUT (b,i4) m4))`
1105   \\ `gc_exec (h,roots) (DRESTRICT h4 (D0 (CUT (b,i4) m4)),ADDR_MAP f3 roots)` by
1108        \\ Q.LIST_EXISTS_TAC [`h4`,`f4`,`(D0 (CUT (b,i4) m4))`]
1120   \\ ASM_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ]
1126       \\ FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11])