machine-code/garbage-collectors/cheney_gcScript.sml

52 val D1 = Define `D1 m x = ?k y z. (m (k:num) = DATA(x,y,z)) \/ (m k = DATA(y,x,z))`;
56 val DR1 = Define `DR1 m k = D1 m k \/ R1 m k`
94     (D1(CUT(b,i)m) SUBSET0 RANGE(b,j)) /\                (* b-i links only to b-j and nil *)
95     (RANGE(i,j') SUBSET (r UNION D1(CUT(b,i)m))) /\      (* every i-j is linked to by some b-i *)
96     (D1(CUT(i,j)m) SUBSET0 DR0(ICUT(b,e)m)) /\           (* i-j links only outside of b-e *)
97     (D1(ICUT(b,e)m) SUBSET0 DR0(ICUT(b,e)m)) /\          (* outside of b-e links only to outside b-e *)
181   ``D1 (CUT(j,j+1)m) SUBSET0 s /\ D1 (CUT(i,j)m) SUBSET0 s ==>
182     D1 (CUT(i,j+1)m) SUBSET0 s``,
184   \\ SIMP_TAC std_ss [IN_DEF,D1,CUT_def,RANGE_def,DECIDE ``k<n+1=k<=n``]
226   ``D1 (CUT (b,i) m) j ==>
228   SIMP_TAC std_ss [D1,CUT_def] \\ REPEAT STRIP_TAC
233   ``k IN D1 m /\ ~(j = x) /\ IRANGE(b,e)x /\ ~(j = e) /\
239     \\ `{j} SUBSET D1 m` by METIS_TAC [IN_EQ_SUBSET] \\ FULL_SIMP_TAC std_ss [cheney_inv_def]
240     \\ `{j} SUBSET (D1 (ICUT (b,e) m)) \/ {j} SUBSET (D1 (CUT (b,i) m)) \/
241         {j} SUBSET (D1 (CUT (i,j) m)) \/ {j} SUBSET (D1 (CUT (j,e) m))` by
242      (FULL_SIMP_TAC std_ss [GSYM IN_EQ_SUBSET,IN_DEF,D1,GSYM RANGE_def]
262       FULL_SIMP_TAC bool_ss [GSYM IN_EQ_SUBSET,IN_INSERT,IN_DEF,D1,CUT_def,RANGE_def]
303   \\ `k IN D1 m /\ k' IN D1 m` by (SIMP_TAC std_ss [IN_DEF,D1] \\ METIS_TAC [])
430         \\ SIMP_TAC std_ss [RANGE_def,DECIDE ``j <= k /\ k < j+1 = (j = k)``,D1]
434       \\ MATCH_MP_TAC SUBSET0_TRANS \\ Q.EXISTS_TAC `D1 (ICUT (b,e) m)` \\ STRIP_TAC THEN1
437         \\ SIMP_TAC std_ss [IN_DEF,D1,ICUT_def] \\ METIS_TAC [])
440      (MATCH_MP_TAC SUBSET0_TRANS \\ Q.EXISTS_TAC `D1 (ICUT (b,e) m)` \\ STRIP_TAC THEN1
441        (REWRITE_TAC [DR0,SUBSET0_DEF,SUBSET_DEF,IN_INSERT,CUT_def,D1]
442         \\ SIMP_TAC std_ss [IN_DEF,DR0,UPDATE_def,ICUT_def,FUN_EQ_THM,D0,R0,D1]
446       \\ REWRITE_TAC [DR0,SUBSET0_DEF,SUBSET_DEF,IN_INSERT,CUT_def,D1]
581       RANGE (i,j) SUBSET (r UNION D1 (CUT (b,i) m)) /\
583       RANGE (i + 1,j2) SUBSET (r UNION D1 (CUT (b,i + 1) ((i =+ DATA (x,y,d)) m)))``,
585   \\ SIMP_TAC bool_ss [IN_DEF,D1,CUT_def] \\ REPEAT STRIP_TAC
656   \\ `{x;y} SUBSET0 D1 (CUT(i,j)m)` by
658     \\ FULL_SIMP_TAC bool_ss [IN_DEF,D1,RANGE_def,cheney_inv_def,CUT_def]
695     \\ sg `D1 (CUT (i,i + 1) ((i =+ DATA (x',y',d))m'')) = {x';y'}` THENL [
696       ASM_SIMP_TAC std_ss [D1,EXTENSION,IN_INSERT,NOT_IN_EMPTY]
697       \\ ASM_SIMP_TAC std_ss [D1,IN_DEF,CUT_def,RANGE_def,DECIDE ``i<=k/\k<i+1 = (k = i)``]
718     \\ Q.EXISTS_TAC `D1 (CUT (i,j'') m'')` \\ ASM_SIMP_TAC bool_ss []
719     \\ SIMP_TAC std_ss [D1,SUBSET_DEF,SUBSET0_DEF,IN_INSERT]
720     \\ SIMP_TAC std_ss [D1,IN_DEF,CUT_def,RANGE_def]
742       \\ `(r i) \/ D1 (CUT (b,i) m'') i` by METIS_TAC []
861     \\ SIMP_TAC std_ss [IN_DEF,D1,heap_type_distinct])
863     \\ SIMP_TAC std_ss [IN_DEF,D1,heap_type_distinct])
865     \\ SIMP_TAC std_ss [IN_DEF,D1,heap_type_distinct])
868     \\ FULL_SIMP_TAC std_ss [IN_DEF,DR0,D1,D0,ICUT_def] \\ REPEAT STRIP_TAC
955       RANGE (b,e) ax /\ (D1 (CUT (b,j) m) SUBSET0 RANGE (b,j)) /\ (m 0 = EMP) /\
962     \\ `D1 (CUT (b,j) m) k` by (ASM_SIMP_TAC std_ss [D1,CUT_def] \\ METIS_TAC [])
971     \\ `D1 (CUT (b,j) m) k'` by (ASM_SIMP_TAC std_ss [D1,CUT_def] \\ METIS_TAC [])
984       (D1 (CUT (i,j) m) SUBSET0 RANGE (i,j)) /\ (D0 (CUT (i,j) m) = RANGE (i,j)) /\ (m 0 = EMP) /\
992   \\ `D1 (CUT (i,j) m) k /\ D1 (CUT (i,j) m) k'` by
993       (SIMP_TAC std_ss [D1,CUT_def] \\ METIS_TAC [heap_type_distinct])
1004      (D1 (CUT (i,j) m) SUBSET0 RANGE (i,j)) /\ (D0 (CUT (i,j) m) = RANGE (i,j)) /\ (m 0 = EMP) /\
1126       \\ MATCH_MP_TAC SUBSET0_TRANS \\ Q.EXISTS_TAC `D1 (CUT (b,j'') m'')`
1129       \\ ASM_SIMP_TAC std_ss [IN_DEF,D1,CUT_def] \\ METIS_TAC []])
1155           \\ `D1 (CUT (b,j'') m'') k /\ D1 (CUT (b,j'') m'') k'` by
1156            (FULL_SIMP_TAC std_ss [D1,CUT_def] \\ METIS_TAC [])
1186           `D1 (CUT (b,j'') m'') y` by (SIMP_TAC bool_ss [CUT_def,D1] \\ METIS_TAC [])
1193           `D1 (CUT (b,j'') m'') z` by (SIMP_TAC bool_ss [CUT_def,D1] \\ METIS_TAC [])