machine-code/garbage-collectors/cheney_gcScript.sml

51 val D0 = Define `D0 m k = ?x y z. m (k:num) = DATA(x,y,z)`;
55 val DR0 = Define `DR0 m k = D0 m k \/ R0 m k`
93     (D0(CUT(b,j)m) = RANGE(b,j)) /\                      (* all DATA between b and j *)
100     (CARD(D0(ICUT(b,e)m)) <= e-j) /\                     (* num of elements outside b-e fit into e-j *)
101     FINITE (D0(ICUT(b,e)m)) /\                           (* the set is finite *)
146   SIMP_TAC std_ss [cheney_inv_def,FUN_EQ_THM,D0,IN_DEF,RANGE_def,CUT_def]
219   SIMP_TAC std_ss [DR0,D0,R0,ICUT_def,IRANGE_def,RANGE_def,heap_type_distinct]);
222   ``D0 (CUT (b,j) m) i ==> ?h g dd. RANGE(b,j)i /\ (m i = DATA(h,g,dd))``,
223   SIMP_TAC std_ss [D0,CUT_def] \\ METIS_TAC [heap_type_distinct]);
343     (if x = 0 then x2 = 0 else (m2 x = REF x2) /\ D0 (CUT(b,j2)m2) x2) /\
351    (Cases_on `IRANGE (b,e) x` \\ FULL_SIMP_TAC bool_ss [IN_DEF,DR0,D0,R0,
370     (FULL_SIMP_TAC bool_ss [IN_DEF,DR0,isREF_def,D0,R0,ICUT_def]
375      \\ `x IN D0 (ICUT(b,e)m)`
376           by (FULL_SIMP_TAC bool_ss [IN_DEF,D0,ICUT_def] \\ METIS_TAC[])
408      (ASM_SIMP_TAC std_ss [FUN_EQ_THM,D0,CUT_def,RANGE_def,IN_DEF]
414       \\ FULL_SIMP_TAC bool_ss [D0,FUN_EQ_THM,CUT_def] \\ METIS_TAC [])
422         \\ SIMP_TAC std_ss [IN_DEF,DR0,UPDATE_def,ICUT_def,FUN_EQ_THM,D0,R0]
429         \\ SIMP_TAC std_ss [IN_DEF,DR0,UPDATE_def,ICUT_def,FUN_EQ_THM,D0,R0]
442         \\ SIMP_TAC std_ss [IN_DEF,DR0,UPDATE_def,ICUT_def,FUN_EQ_THM,D0,R0,D1]
447       \\ SIMP_TAC std_ss [IN_DEF,DR0,UPDATE_def,ICUT_def,FUN_EQ_THM,D0,R0]
479       \\ `D0 (ICUT (b,e) ((x =+ REF j) m)) = D0 (ICUT (b,e) m) DELETE x` by
481         \\ SIMP_TAC std_ss [IN_DEF,ICUT_def,D0,UPDATE_def] \\ STRIP_TAC
486       \\ `x IN D0 (ICUT (b,e) m)` by
487         (ASM_SIMP_TAC std_ss [IN_DEF,D0,ICUT_def] \\ METIS_TAC [])
490      (`D0 (ICUT (b,e) ((x =+ REF j) m)) = D0 (ICUT (b,e) m) DELETE x` by
492         \\ SIMP_TAC std_ss [IN_DEF,ICUT_def,D0,UPDATE_def] \\ STRIP_TAC
539      (ASM_SIMP_TAC std_ss [DR0,D0,R0,ICUT_def,FUN_EQ_THM,UPDATE_def] \\ STRIP_TAC
544          \\ ASM_SIMP_TAC std_ss [D0,CUT_def,RANGE_def,UPDATE_def] \\ METIS_TAC [])
556       (if x = 0 then x' = 0 else (m x = REF x') /\ D0 m x') /\
557       (if y = 0 then y' = 0 else (m y = REF y') /\ D0 m y') ==>
559   REWRITE_TAC [FUN_EQ_THM,D0] \\ REPEAT STRIP_TAC
560   \\ `?a0 x0 y0 D0. x'' = (a0,x0,y0,D0)` by METIS_TAC [PAIR]
619   SIMP_TAC std_ss [D0,CUT_def] \\ METIS_TAC []);
681    (sg `D0 (CUT (b,j'') ((i =+ DATA (x',y',d)) m'')) =
682      i INSERT D0 (CUT (b,j'') m'')` THENL [
683       SIMP_TAC std_ss [EXTENSION,D0,CUT_def,IN_INSERT]
684       \\ SIMP_TAC std_ss [IN_DEF,D0,UPDATE_def] \\ STRIP_TAC
763     \\ `D0 (CUT (b,j'') m'') i` by METIS_TAC [] \\ IMP_RES_TAC D0_IMP
766    (`!x i j m. D0 (CUT (i,j) m) x ==> D0 m x` by
767       (SIMP_TAC bool_ss [D0,CUT_def] \\ METIS_TAC [heap_type_distinct])
859   THEN1 (SIMP_TAC std_ss [FUN_EQ_THM,D0,heap_type_distinct])
868     \\ FULL_SIMP_TAC std_ss [IN_DEF,DR0,D1,D0,ICUT_def] \\ REPEAT STRIP_TAC
880     \\ FULL_SIMP_TAC std_ss [FINITE_RANGE2,SUBSET_DEF,IN_DEF,D0]
885     \\ Q.EXISTS_TAC `RANGE(b,i)` \\ FULL_SIMP_TAC std_ss [D0,SUBSET_DEF,IN_DEF,ICUT_def,FINITE_RANGE2]
897     \\ RES_TAC \\ RES_TAC \\ FULL_SIMP_TAC std_ss [IN_DEF,DR0,D0,heap_type_11] \\ METIS_TAC []));
956       (D0 (CUT (b,j) m) = RANGE (b,j)) ==>
966     \\ `D0 (CUT (b,j) m) k` by METIS_TAC []
975     \\ `D0 (CUT (b,j) m) k'` by METIS_TAC []
984       (D1 (CUT (i,j) m) SUBSET0 RANGE (i,j)) /\ (D0 (CUT (i,j) m) = RANGE (i,j)) /\ (m 0 = EMP) /\
994   \\ `~(k = 0) ==> D0 (CUT (i,j) m) k` by METIS_TAC []
995   \\ `~(k' = 0) ==> D0 (CUT (i,j) m) k'` by METIS_TAC []
1004      (D1 (CUT (i,j) m) SUBSET0 RANGE (i,j)) /\ (D0 (CUT (i,j) m) = RANGE (i,j)) /\ (m 0 = EMP) /\
1122       `D0 (CUT (b,j'') m'') k` by METIS_TAC [] \\ IMP_RES_TAC D0_IMP
1166             \\ `D0 (CUT (b,j'') m'') k` by METIS_TAC []
1170             \\ `D0 (CUT (b,j'') m'') k'` by METIS_TAC []
1191           \\ `D0 (CUT (b,j'') m'') y` by METIS_TAC []
1198           \\ `D0 (CUT (b,j'') m'') z` by METIS_TAC []
1208           \\ `D0 (CUT (b,j'') m'') k` by METIS_TAC []