open HolKernel boolLib bossLib Parse; val _ = new_theory "improved_gc";

open pred_setTheory arithmeticTheory pairTheory listTheory combinTheory;
open finite_mapTheory sumTheory relationTheory;

infix \\
val op \\ = op THEN;
val RW = REWRITE_RULE;
val RW1 = ONCE_REWRITE_RULE;
fun SUBGOAL q = REVERSE (sg q)
fun ALPHA_TAC s = let
  fun my_alpha_conv tm =
    ALPHA_CONV (mk_var(s,type_of (fst(dest_abs tm)))) tm
  in CONV_TAC (RAND_CONV my_alpha_conv) end;



val _ = Hol_datatype `heap_address = H_ADDR of num | H_DATA of 'a`;
val heap_address_11 = fetch "-" "heap_address_11";
val heap_address_distinct = fetch "-" "heap_address_distinct";

val _ = type_abbrev("abs_heap",``:(num |-> ('b heap_address) list # 'a) #
          (num set) # (num set) # (num set) # (num -> num)``);

val ADDR_MAP_def = Define `
  (ADDR_MAP f [] = []) /\
  (ADDR_MAP f (H_ADDR x::xs) = H_ADDR (f x) :: ADDR_MAP f xs) /\
  (ADDR_MAP f (H_DATA y::xs) = H_DATA y :: ADDR_MAP f xs)`;

val IN_THM = SIMP_RULE std_ss [EXTENSION,GSPECIFICATION]
val ADDR_SET_def = (IN_THM o Define) `ADDR_SET s = { x | MEM (H_ADDR x) s }`;

val (gc_reachable_rules,gc_reachable_ind,gc_reachable_cases) = Hol_reln `
  (!h roots x.
    x IN ADDR_SET roots ==> gc_reachable (h,roots) x) /\
  (!h roots x a xs d.
    a IN FDOM h /\ (h ' a = (xs,d)) /\ x IN ADDR_SET xs /\ gc_reachable (h,roots) a ==>
    gc_reachable (h,roots) x)`;

val PAIR_TRANSLATE_def = Define `PAIR_TRANSLATE f (xs,a) = (ADDR_MAP f xs,a)`;
val SET_TRANSLATE_def = (IN_THM o Define) `SET_TRANSLATE f s = { x | (f x) IN s }`;
val HAS_CHANGED_def = (IN_THM o Define) `HAS_CHANGED f = { x | ~(f x = x) }`;
val POINTERS_def = (IN_THM o Define) `POINTERS h y =
  { a | ?b zs d. b IN y /\ b IN FDOM h /\ (h ' b = (zs,d)) /\ a IN ADDR_SET zs }`;

val gc_filter_def = Define `
  gc_filter (h,roots) = (DRESTRICT h (gc_reachable (h,roots)),roots)`;

val gc_copy_def = Define `
  gc_copy (h1,roots1) (h2,roots2) =
    ?f. (f o f = I) /\ (FDOM h1 = SET_TRANSLATE f (FDOM h2)) /\
        (roots2 = ADDR_MAP f roots1) /\
        !x. x IN FDOM h1 ==> (h1 ' x = PAIR_TRANSLATE f (h2 ' (f x)))`;

val gc_exec_def = Define `gc_exec x y = gc_copy (gc_filter x) y`;

val (abs_step_rules,abs_step_ind,abs_step_cases) = Hol_reln `
  (!h x y z f a.
    a IN z /\ ~(f a = a) ==>
    abs_step (h,x,y,z,f) (h,x,y,z DELETE a,f)) /\
  (!h x y z f a xs d.
    a IN y /\ (h ' a = (xs,d)) /\ (!b. b IN ADDR_SET xs ==> ~(f b = b)) ==>
    abs_step (h,x,y,z,f) (h |+ (a,ADDR_MAP f xs,d),a INSERT x,y DELETE a,z,f)) /\
  (!h x y z f a b xs d.
    a IN z /\ (f a = a) /\ (f b = b) /\ ~(b IN FDOM h) /\ a IN FDOM h /\ (h ' a = (xs,d)) ==>
    abs_step (h,x,y,z,f) (h |+ (b,xs,d) \\ a,x,b INSERT y,z UNION (ADDR_SET xs),(a =+ b) ((b =+ a) f)))`;

val abs_steps_def = Define `abs_steps = RTC abs_step`;

val abs_steps_TRANS = store_thm("abs_steps_TRANS",
  ``!x y z. abs_steps x y /\ abs_steps y z ==> abs_steps x z``,
  METIS_TAC [abs_steps_def,RTC_RTC]);

val (abs_gc_rules,abs_gc_ind,abs_gc_cases) = Hol_reln `
  (!h roots h2 f x.
    abs_steps (h,{},{},ADDR_SET roots,I) (h2,x,{},{},f) ==>
    abs_gc (h,roots) (DRESTRICT h2 x,ADDR_MAP f roots))`;

val abs_gc_inv_def = Define `
  abs_gc_inv (h1,roots1) (h,x,y,z,f) =
    let old = FDOM h UNION HAS_CHANGED f DIFF (x UNION y) in
      DISJOINT x y /\
      POINTERS h x SUBSET (x UNION y) /\
      POINTERS h (UNIV DIFF x) SUBSET old /\
      POINTERS h y UNION ADDR_SET roots1 SUBSET SET_TRANSLATE f (x UNION y) UNION z /\
      SET_TRANSLATE f (x UNION y) UNION z SUBSET gc_reachable (h1,roots1) /\
      (!a. a IN z ==> if f a = a then a IN old else f a IN x UNION y) /\
      (!a. ~(f a = a) ==> ~(a IN x UNION y = f a IN x UNION y)) /\
      (!a. a IN y \/ a IN x = ~(f a = a) /\ a IN FDOM h) /\ (f o f = I) /\
      (SET_TRANSLATE f (FDOM h) = FDOM h1) /\
      (!d. d IN FDOM h1 ==>
          (h1 ' d = if (f d) IN x then PAIR_TRANSLATE f (h ' (f d)) else h ' (f d)))`;

val SET_TAC =
  FULL_SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_UNION,IN_DELETE,SUBSET_DEF,
    DISJOINT_DEF,NOT_IN_EMPTY,EXTENSION,IN_INSERT,IN_INTER,IN_DIFF,IN_UNIV]
  \\ METIS_TAC [PAIR_EQ];

val SET2_TAC =
  FULL_SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_UNION,IN_DELETE,SUBSET_DEF,
    DISJOINT_DEF,NOT_IN_EMPTY,EXTENSION,IN_INSERT,IN_INTER,IN_DIFF,IN_UNIV,
    POINTERS_def,HAS_CHANGED_def,SET_TRANSLATE_def,FDOM_FUPDATE,
    FDOM_DOMSUB,FAPPLY_FUPDATE_THM,DOMSUB_FAPPLY_THM] \\ SET_TAC;

val POINTERS_IGNORE = prove(
  ``~(a IN x) ==> (POINTERS (h |+ (a,xs,d)) x = POINTERS h x) /\
                  (POINTERS (h \\ a) x = POINTERS h x)``,
  SET2_TAC);

val set_SUBSET_POINTERS = prove(
  ``(h ' a = (xs,d)) /\ a IN FDOM h /\ a IN x ==> ADDR_SET xs SUBSET POINTERS h x``,
  SET2_TAC);

val POINTER_FUPDATE_EQ = store_thm("POINTER_FUPDATE_EQ",
  ``~(b IN FDOM h) /\ b IN x ==>
    (POINTERS (h |+ (b,xs,d)) x = POINTERS h x UNION ADDR_SET xs)``,
  SET2_TAC);

val POINTERS_FUPDATE = prove(
  ``POINTERS (h |+ (b,xs,d)) (b INSERT y) SUBSET POINTERS h y UNION ADDR_SET xs``,
  SET2_TAC);

val POINTERS_SUBSET = prove(
  ``!h x y. x SUBSET y ==> POINTERS h x SUBSET POINTERS h y``,
  SET2_TAC);

val POINTERS_DOMSUB = prove(
  ``!h y. POINTERS (h \\ a) y SUBSET POINTERS h y``,
  SET2_TAC);

val SET_TRANSLATE_SUBSET = prove(
  ``!f x y. (f o f = I) ==>
            (SET_TRANSLATE f x SUBSET y = x SUBSET SET_TRANSLATE f y)``,
  SIMP_TAC std_ss [FUN_EQ_THM] \\ SET2_TAC);

val SET_TRANSLATE_MAP = prove(
  ``!xs f. (f o f = I) ==> (ADDR_SET (ADDR_MAP f xs) = SET_TRANSLATE f (ADDR_SET xs))``,
  SIMP_TAC std_ss [EXTENSION,ADDR_SET_def,SET_TRANSLATE_def]
  \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ Induct
  \\ ASM_SIMP_TAC std_ss [ADDR_MAP_def,MEM] \\ Cases
  \\ ASM_SIMP_TAC std_ss [ADDR_MAP_def,MEM,heap_address_11,heap_address_distinct]
  \\ SET2_TAC);

val SET_TRANSLATE_THM = prove(
  ``(f o f = I) ==>
     (SET_TRANSLATE f (x UNION y) = (SET_TRANSLATE f x) UNION (SET_TRANSLATE f y)) /\
     (SET_TRANSLATE f (x INTER y) = (SET_TRANSLATE f x) INTER (SET_TRANSLATE f y)) /\
     (SET_TRANSLATE f (a INSERT x) = (f a) INSERT (SET_TRANSLATE f x)) /\
     (SET_TRANSLATE f (SET_TRANSLATE f x) = x)``,
  SIMP_TAC std_ss [EXTENSION] \\ SIMP_TAC std_ss [FUN_EQ_THM] \\ SET2_TAC);

val SET_TRANSLATE_IGNORE = prove(
  ``(f o f = I) /\ (f a = a) /\ (f b = b) /\ ~(a IN x) /\ ~(b IN x) ==>
      (SET_TRANSLATE ((a =+ b) ((b =+ a) f)) x = SET_TRANSLATE f x)``,
  SIMP_TAC std_ss [EXTENSION] \\ SIMP_TAC std_ss [FUN_EQ_THM,APPLY_UPDATE_THM,
    SET_TRANSLATE_def] \\ SET2_TAC);

val ADDR_MAP_ADDR_MAP = store_thm("ADDR_MAP_ADDR_MAP",
  ``!xs f. (f o f = I) ==> (ADDR_MAP f (ADDR_MAP f xs) = xs)``,
  Induct \\ SIMP_TAC std_ss [ADDR_MAP_def] \\ Cases
  \\ ASM_SIMP_TAC std_ss [ADDR_MAP_def,FUN_EQ_THM]);

val ADDR_MAP_EQ_ADDR_MAP = prove(
  ``!xs f g. (ADDR_MAP f xs = ADDR_MAP g xs) = !x. x IN ADDR_SET xs ==> (f x = g x)``,
  Induct \\ SIMP_TAC std_ss [ADDR_MAP_def,ADDR_SET_def,MEM]
  \\ Cases \\ FULL_SIMP_TAC std_ss [ADDR_MAP_def,ADDR_SET_def,MEM,CONS_11,
       heap_address_11,heap_address_distinct] \\ SET_TAC);

val abs_step_thm = prove(
  ``!s1 s2. abs_step s1 s2 /\ abs_gc_inv (h0,r0) s1 ==> abs_gc_inv (h0,r0) s2``,
  REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `abs_step s1 s1i` ASSUME_TAC
  \\ FULL_SIMP_TAC std_ss [abs_step_cases]
  THEN1 (FULL_SIMP_TAC std_ss [abs_gc_inv_def,IN_UNION,IN_DELETE,LET_DEF]
         \\ `f a IN x UNION y` by SET_TAC
         \\ SUBGOAL `a IN SET_TRANSLATE f (x UNION y)` THEN1 SET_TAC \\ SET2_TAC)
  THEN1
   (FULL_SIMP_TAC std_ss [abs_gc_inv_def,IN_UNION,IN_DELETE,FDOM_FUPDATE,LET_DEF]
    \\ `a INSERT FDOM h = FDOM h` by SET_TAC \\ ASM_SIMP_TAC std_ss [IN_INSERT]
    \\ `~(a IN x) /\ ~(a IN (FDOM h UNION HAS_CHANGED f DIFF (a INSERT x)))` by SET_TAC
    \\ ASM_SIMP_TAC std_ss [POINTERS_IGNORE] \\ STRIP_TAC THEN1 SET_TAC
    \\ `(a INSERT x) UNION (y DELETE a) UNION z = x UNION y UNION z` by SET_TAC
    \\ `(a INSERT x) UNION (y DELETE a) = x UNION y` by SET_TAC
    \\ ASM_SIMP_TAC std_ss []
    \\ REVERSE (REPEAT STRIP_TAC) THEN1
     (Cases_on `f d' = a` \\ ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM,IN_INSERT]
      \\ `~(a IN x)` by SET_TAC
      \\ ASM_SIMP_TAC std_ss [PAIR_TRANSLATE_def,ADDR_MAP_ADDR_MAP])
    THEN1 SET_TAC THEN1 SET_TAC THEN1 SET_TAC THEN1 SET2_TAC THEN1 SET2_TAC
    \\ MATCH_MP_TAC (MATCH_MP (RW [GSYM AND_IMP_INTRO] SUBSET_TRANS) (SPEC_ALL POINTERS_FUPDATE))
    \\ ASM_SIMP_TAC std_ss [UNION_SUBSET] \\ `a IN FDOM h` by SET_TAC
    \\ IMP_RES_TAC set_SUBSET_POINTERS \\ POP_ASSUM (K ALL_TAC)
    \\ ASM_SIMP_TAC std_ss [SET_TRANSLATE_MAP,SET_TRANSLATE_SUBSET] \\ SET2_TAC)
  THEN1
   (FULL_SIMP_TAC std_ss [abs_gc_inv_def,IN_UNION,IN_DELETE,FDOM_FUPDATE,IN_INSERT,LET_DEF]
    \\ `~(a IN x) /\ ~(b IN x) /\ ~(a = b) /\ a IN (UNIV DIFF x) /\ a IN (UNIV DIFF (x UNION y))` by SET_TAC
    \\ `ADDR_SET xs SUBSET POINTERS h (UNIV DIFF (x UNION y))` by METIS_TAC [set_SUBSET_POINTERS]
    \\ `((a =+ b) ((b =+ a) f) o (a =+ b) ((b =+ a) f) = I)` by
         (FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,FUN_EQ_THM] \\ SET_TAC)
    \\ STRIP_TAC THEN1 SET_TAC
    \\ ASM_SIMP_TAC std_ss [POINTERS_IGNORE] \\ STRIP_TAC THEN1 SET_TAC
    \\ `(HAS_CHANGED ((a =+ b) ((b =+ a) f)) = a INSERT b INSERT HAS_CHANGED f) /\
       ~(b IN HAS_CHANGED f)` by
        (FULL_SIMP_TAC std_ss [EXTENSION,HAS_CHANGED_def,APPLY_UPDATE_THM] \\ SET2_TAC)
    \\ STRIP_TAC THEN1 (FULL_SIMP_TAC std_ss [] \\ SET2_TAC)
    \\ `~(a IN y) /\ ~(b IN y)` by SET_TAC
    \\ FULL_SIMP_TAC std_ss [SET_TRANSLATE_THM,APPLY_UPDATE_THM,SET_TRANSLATE_IGNORE]
    \\ STRIP_TAC THEN1 SET2_TAC
    \\ STRIP_TAC THEN1
     (`a IN gc_reachable (h0,r0)` by SET_TAC
      \\ SUBGOAL `ADDR_SET xs SUBSET gc_reachable (h0,r0)` THEN1 SET_TAC
      \\ FULL_SIMP_TAC std_ss [SUBSET_DEF] \\ REPEAT STRIP_TAC
      \\ SIMP_TAC std_ss [IN_DEF] \\ ONCE_REWRITE_TAC [gc_reachable_cases]
      \\ DISJ2_TAC \\ Q.PAT_X_ASSUM `a IN gc_reachable hhh`
           (ASSUME_TAC o SIMP_RULE std_ss [IN_DEF]) \\ ASM_SIMP_TAC std_ss []
      \\ Q.LIST_EXISTS_TAC [`a`,`xs`,`d`] \\ ASM_SIMP_TAC std_ss [] \\ SET2_TAC)
    \\ STRIP_TAC THEN1
     (FULL_SIMP_TAC std_ss [FDOM_FUPDATE,FDOM_DOMSUB]
      \\ ALPHA_TAC "n" \\ REPEAT STRIP_TAC THEN1
       (Cases_on `a = n` \\ FULL_SIMP_TAC std_ss []
        \\ SUBGOAL `~(n = b)` THEN1 (FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ SET_TAC)
        \\ CCONTR_TAC \\ FULL_SIMP_TAC std_ss []
        \\ `~(b IN HAS_CHANGED f)` by (SIMP_TAC std_ss [HAS_CHANGED_def] \\ SET_TAC)
        \\ SET_TAC)
      \\ Cases_on `a = n` \\ FULL_SIMP_TAC std_ss []
      \\ `POINTERS h (UNIV DIFF (x UNION y)) SUBSET POINTERS h (UNIV DIFF x)` by
           (MATCH_MP_TAC POINTERS_SUBSET \\ SET_TAC)
      \\ `n IN FDOM h UNION HAS_CHANGED f DIFF (x UNION y)` by SET_TAC
      \\ FULL_SIMP_TAC std_ss [IN_INSERT,IN_UNION,IN_DELETE,IN_DIFF] \\ SET_TAC)
    \\ FULL_SIMP_TAC std_ss [FDOM_DOMSUB,FDOM_FUPDATE,IN_INSERT]
    \\ STRIP_TAC THEN1 (FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ SET_TAC)
    \\ STRIP_TAC THEN1 (FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ SET_TAC)
    \\ Q.PAT_X_ASSUM `gg = FDOM h0` (ASSUME_TAC o GSYM) \\ ASM_SIMP_TAC std_ss []
    \\ STRIP_TAC THEN1
     (FULL_SIMP_TAC std_ss [EXTENSION,SET_TRANSLATE_def,APPLY_UPDATE_THM]
      \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ SET_TAC)
    \\ ALPHA_TAC "i" \\ STRIP_TAC
    \\ Cases_on `(i = a) \/ (i = b)` \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,
        FUN_EQ_THM,DOMSUB_FAPPLY_THM,FAPPLY_FUPDATE_THM]
    THEN1 (FULL_SIMP_TAC std_ss [SET_TRANSLATE_def])
    \\ `~(f i = a) /\ ~(f i = b)` by METIS_TAC []
    \\ Cases_on `f i IN x` \\ FULL_SIMP_TAC std_ss []
    \\ `?xs d. h ' (f i) = (xs,d)` by METIS_TAC [PAIR]
    \\ ASM_SIMP_TAC std_ss [PAIR_TRANSLATE_def,IN_DEF,SET_TRANSLATE_def]
    \\ ASM_SIMP_TAC std_ss [ADDR_MAP_EQ_ADDR_MAP,APPLY_UPDATE_THM]
    \\ REPEAT STRIP_TAC
    \\ `ADDR_SET xs' SUBSET x UNION y` by METIS_TAC [set_SUBSET_POINTERS,SUBSET_TRANS]
    \\ SET_TAC));

val abs_steps_thm = prove(
  ``!s1 s2. abs_steps s1 s2 /\ abs_gc_inv (h0,r0) s1 ==> abs_gc_inv (h0,r0) s2``,
  SIMP_TAC std_ss [GSYM AND_IMP_INTRO,abs_steps_def]
  \\ HO_MATCH_MP_TAC RTC_INDUCT \\ SIMP_TAC std_ss [] \\ METIS_TAC [abs_step_thm]);

val ok_heap_def = Define `
  ok_heap (h,roots) = (POINTERS h UNIV UNION ADDR_SET roots SUBSET FDOM h)`;

val ok_heap_IMP = store_thm("ok_heap_IMP",
  ``ok_heap (h1,roots1) ==> abs_gc_inv (h1,roots1) (h1,{},{},ADDR_SET roots1,I)``,
  FULL_SIMP_TAC std_ss [abs_gc_inv_def,LET_DEF,ok_heap_def]
  \\ SUBGOAL `ADDR_SET roots1 SUBSET gc_reachable (h1,roots1)` THEN1 SET2_TAC
  \\ SIMP_TAC std_ss [SUBSET_DEF] \\ REPEAT STRIP_TAC \\ SIMP_TAC std_ss [IN_DEF]
  \\ ONCE_REWRITE_TAC [gc_reachable_cases] \\ ASM_SIMP_TAC std_ss []);

val abs_gc_thm = store_thm("abs_gc_thm",
  ``!h1 roots1 h2 roots2.
       ok_heap (h1,roots1) /\ abs_gc (h1,roots1) (h2,roots2) ==>
       gc_exec (h1,roots1) (h2,roots2)``,
  SIMP_TAC std_ss [abs_gc_cases,gc_exec_def,gc_filter_def,gc_copy_def]
  \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `f` \\ ASM_SIMP_TAC std_ss []
  \\ IMP_RES_TAC ok_heap_IMP \\ IMP_RES_TAC abs_steps_thm \\ POP_ASSUM MP_TAC
  \\ SIMP_TAC std_ss [abs_gc_inv_def,LET_DEF,NOT_IN_EMPTY,UNION_EMPTY]
  \\ STRIP_TAC \\ SIMP_TAC std_ss [FDOM_DRESTRICT,DRESTRICT_DEF]
  \\ SUBGOAL `gc_reachable (h1,roots1) = SET_TRANSLATE f x` THEN1 SET2_TAC
  \\ ASM_SIMP_TAC std_ss [SET_EQ_SUBSET] \\ SIMP_TAC std_ss [SUBSET_DEF]
  \\ `?tt. (h1,roots1) = tt` by METIS_TAC [PAIR] \\ ASM_SIMP_TAC std_ss []
  \\ REPEAT STRIP_TAC \\ REPEAT (POP_ASSUM MP_TAC)
  \\ SIMP_TAC std_ss [AND_IMP_INTRO] \\ ONCE_REWRITE_TAC [CONJ_COMM]
  \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO]
  \\ STRIP_TAC \\ POP_ASSUM (MP_TAC o SIMP_RULE std_ss [IN_DEF])
  \\ Q.SPEC_TAC (`x'`,`q`) \\ Q.SPEC_TAC (`tt`,`t`)
  \\ HO_MATCH_MP_TAC gc_reachable_ind \\ REPEAT STRIP_TAC THEN1 SET_TAC
  \\ FULL_SIMP_TAC std_ss [SET_TRANSLATE_def]
  \\ `h2' ' (f q') = (ADDR_MAP f xs,d)` by
    (Q.PAT_X_ASSUM `!d. d IN FDOM h ==> bb` (MP_TAC o GSYM o Q.SPEC `q'`)
     \\ `?xs2 d2. h2' ' (f q') = (xs2,d2)` by METIS_TAC [PAIR]
     \\ ASM_SIMP_TAC std_ss [PAIR_TRANSLATE_def]
     \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
     \\ ASM_SIMP_TAC std_ss [ADDR_MAP_ADDR_MAP])
  \\ `ADDR_SET (ADDR_MAP f xs) SUBSET POINTERS h2' x` by METIS_TAC [set_SUBSET_POINTERS]
  \\ `f q IN ADDR_SET (ADDR_MAP f xs)` by
      (FULL_SIMP_TAC std_ss [SET_TRANSLATE_MAP,SET_TRANSLATE_def]
       \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM]) \\ SET_TAC);

val gc_copy_thm = prove(
  ``ok_heap (h1,roots1) /\ gc_copy (h1,roots1) (h2,roots2) ==> ok_heap (h2,roots2)``,
  SIMP_TAC std_ss [gc_exec_def,gc_copy_def,gc_filter_def,ok_heap_def]
  \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_UNION,POINTERS_def]
  \\ `!k. f (f k) = k` by FULL_SIMP_TAC std_ss [FUN_EQ_THM]
  \\ REVERSE (REPEAT STRIP_TAC) THEN1
   (POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [SET_TRANSLATE_MAP,SET_TRANSLATE_def]
    \\ SET_TAC)
  \\ FULL_SIMP_TAC std_ss [IN_UNIV,SET_TRANSLATE_def,EXTENSION]
  \\ Q.PAT_X_ASSUM `!d. ff IN FDOM h1 <=> bb IN FDOM h2` ASSUME_TAC
  \\ FULL_SIMP_TAC std_ss []
  \\ `h1 ' (f b) = PAIR_TRANSLATE f (zs,d)` by METIS_TAC []
  \\ FULL_SIMP_TAC std_ss [PAIR_TRANSLATE_def]
  \\ SUBGOAL `f x IN ADDR_SET (ADDR_MAP f zs)` THEN1 METIS_TAC []
  \\ FULL_SIMP_TAC std_ss [SET_TRANSLATE_MAP,SET_TRANSLATE_def]);

val gc_filter_thm = prove(
  ``ok_heap (h1,roots1) ==> ok_heap (gc_filter(h1,roots1))``,
  SIMP_TAC std_ss [gc_exec_def,gc_copy_def,gc_filter_def,ok_heap_def]
  \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_UNION,POINTERS_def]
  \\ REVERSE (REPEAT STRIP_TAC) THEN1
   (RES_TAC \\ FULL_SIMP_TAC std_ss [FDOM_DRESTRICT,IN_INTER]
    \\ FULL_SIMP_TAC std_ss [IN_DEF] \\ ONCE_REWRITE_TAC [gc_reachable_cases]
    \\ ASM_SIMP_TAC std_ss [IN_DEF])
  \\ FULL_SIMP_TAC std_ss [FDOM_DRESTRICT,IN_INTER]
  \\ Q.PAT_X_ASSUM `DRESTRICT h1 (gc_reachable (h1,roots1)) ' b = (zs,d)` MP_TAC
  \\ ASM_SIMP_TAC std_ss [DRESTRICT_DEF,IN_INTER] \\ REPEAT STRIP_TAC THEN1 SET_TAC
  \\ FULL_SIMP_TAC std_ss [IN_DEF]
  \\ ONCE_REWRITE_TAC [gc_reachable_cases] \\ DISJ2_TAC
  \\ SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `b` \\ ASM_SIMP_TAC std_ss [IN_DEF]);

val gc_exec_thm = store_thm("gc_exec_thm",
  ``ok_heap (h1,roots1) /\ gc_exec (h1,roots1) (h2,roots2) ==> ok_heap (h2,roots2)``,
  METIS_TAC [gc_exec_def,gc_filter_thm,gc_copy_thm,PAIR]);

(* next level *)

val _ = Hol_datatype `heap_element =
    H_EMP | H_REF of num | H_BLOCK of ('a heap_address) list # (num # 'b)`;
val heap_element_distinct = fetch "-" "heap_element_distinct";
val heap_element_11 = fetch "-" "heap_element_11";

val isDATA_def = Define `isDATA x = ?i. x = H_DATA i`;
val isADDR_def = Define `isADDR x = ?i. x = H_ADDR i`;
val isREF_def = Define `isREF x = ?i. x = H_REF i`;
val isBLOCK_def = Define `isBLOCK x = ?i. x = H_BLOCK i`;
val getADDR_def = Define `getADDR (H_ADDR x) = x`;
val getREF_def = Define `getREF (H_REF x) = x`;
val getBLOCK_def = Define `getBLOCK (H_BLOCK y) = y`;
val getLENGTH_def = Define `
  (getLENGTH (H_BLOCK (m,l,n)) = l + 1) /\
  (getLENGTH (H_REF i) = 0) /\
  (getLENGTH (H_EMP) = 0)`;

val RANGE_def = Define `RANGE(i:num,j) k = i <= k /\ k < j`;
val CUT_def = Define `CUT (i,j) m = \k. if RANGE (i,j) k then m k else H_EMP`;

val D0 = Define `D0 m k = ?x y z. m (k:num) = H_BLOCK (x,y,z)`;
val D1 = Define `D1 m i = ?k x y z. (m (k:num) = H_BLOCK(x,y,z)) /\ i IN ADDR_SET x`;
val R0 = Define `R0 m k = ?a. m (k:num) = H_REF a`;
val R1 = Define `R1 m a = ?k. m (k:num) = H_REF a`;
val DR0 = Define `DR0 m k = D0 m k \/ R0 m k`
val DR1 = Define `DR1 m k = D1 m k \/ R1 m k`

val move_def = Define `
  (move (H_DATA x,j,m) = (H_DATA x,j,m)) /\
  (move (H_ADDR a,j,m) =
     case m a of
       H_REF i => (H_ADDR i,j,m)
     | H_BLOCK (xs,n,d) => let m = (a =+ H_REF j) m in
                           let m = (j =+ H_BLOCK (xs,n,d)) m in
                              (H_ADDR j,j + n + 1,m))`;

val move_list_def = Define `
  (move_list ([],j,m) = ([],j,m)) /\
  (move_list (x::xs,j,m) =
     let (x,j,m) = move (x,j,m) in
     let (xs,j,m) = move_list (xs,j,m) in
       (x::xs,j,m))`;

val gc_step_def = Define `
  gc_step (i,j,m) =
    let (xs,n,d) = getBLOCK (m i) in
    let (xs,j,m) = move_list (xs,j,m) in
    let m = (i =+ H_BLOCK (xs,n,d)) m in
    let i = i + n + 1 in
      (i,j,m)`;

val gc_loop_def = tailrecLib.tailrec_define ``
  gc_loop (i,j,m) = if i = j then (i,m) else
                      let (i,j,m) = gc_step (i,j,m) in
                        gc_loop (i,j,m)``;

val gc_def = Define `
  gc (b:num,e:num,b2:num,e2:num,roots,m) =
    let (b2,e2,b,e) = (b,e,b2,e2) in
    let (roots,j,m) = move_list (roots,b,m) in
    let (i,m) = gc_loop (b,j,m) in
    let m = CUT (b,i) m in
      (b,i,e,b2,e2,roots,m)`;

(* invariant *)

val EMP_RANGE_def = Define `
  EMP_RANGE (b,e) m = !k. k IN RANGE(b,e) ==> (m k = H_EMP)`;

val (full_heap_rules,full_heap_ind,full_heap_cases) =
  Hol_reln
  `(!b m. full_heap b b m) /\
   (!b e m n xs d.
      (m b = H_BLOCK (xs,n,d)) /\ EMP_RANGE (b+1,b+n+1) m /\
      full_heap (b+n+1) e m ==> full_heap b e m)`;

val full_heap_ind = IndDefLib.derive_strong_induction(full_heap_rules,full_heap_ind);
val _ = save_thm("full_heap_ind",full_heap_ind);

val (part_heap_rules,part_heap_ind,part_heap_cases) =
  Hol_reln
  `(!b m. part_heap b b m 0) /\
   (!b e m k.
      ~(isBLOCK (m b)) /\ part_heap (b+1) e m k ==> part_heap b e m k) /\
   (!b e m n xs d k.
      (m b = H_BLOCK (xs,n,d)) /\ EMP_RANGE (b+1,b+n+1) m /\
      part_heap (b+n+1) e m k ==> part_heap b e m (k+n+1))`;

val part_heap_ind = IndDefLib.derive_strong_induction(part_heap_rules,part_heap_ind);
val _ = save_thm("part_heap_ind",part_heap_ind);

val ref_mem_def = Define `
  ref_mem (h,f) m =
    !a. m a = if a IN FDOM h then H_BLOCK (h ' a) else
              if f a = a then H_EMP else H_REF (f a)`;

val gc_inv_def = Define `
  gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z) =
    (b <= i /\ i <= j /\ j <= e) /\
    (* semispaces are disjoint *)
    (~(e < b2) ==> e2 < b) /\
    (* EMP outside of b2-e2 and b-j *)
    (!k. ~(RANGE(b2,e2)k) /\ ~(RANGE(b,j)k) ==> (m k = H_EMP)) /\
    (* heap full of BLOCK elements between b-i, i-j *)
    full_heap b i m /\ full_heap i j m /\
    (* data elements from b2-e2 fit into j-e *)
    (?len. part_heap b2 e2 m len /\ len <= e-j) /\
    (* refinement *)
    ref_mem (h,f) m /\
    (* simulation *)
    ok_heap (h1,roots1) /\
    abs_steps (h1,{},{},ADDR_SET roots1,I) (h,D0(CUT(b,i)m),D0(CUT(i,j)m),z,f)`;

(* some lemmas *)

val RANGE_TAC = FULL_SIMP_TAC std_ss [RANGE_def,IN_DEF,gc_inv_def] \\ DECIDE_TAC

val gc_inv_IMP = store_thm("gc_inv_IMP",
  ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z) ==>
    abs_gc_inv (h1,roots1) (h,D0(CUT(b,i)m),D0(CUT(i,j)m),z,f)``,
  SIMP_TAC std_ss [gc_inv_def] \\ METIS_TAC [ok_heap_IMP,abs_steps_thm]);

val gc_inv_THM = store_thm("gc_inv_THM",
  ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z) =
    gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z) /\
    abs_gc_inv (h1,roots1) (h,D0(CUT(b,i)m),D0(CUT(i,j)m),z,f)``,
  METIS_TAC [gc_inv_IMP]);

val full_heap_REFL = store_thm("full_heap_REFL",
  ``!b m. full_heap b b m``,
  METIS_TAC [full_heap_cases]);

val full_heap_TRANS = store_thm("full_heap_TRANS",
  ``!j b i m. full_heap b i m /\ full_heap i j m ==> full_heap b j m``,
  STRIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ HO_MATCH_MP_TAC full_heap_ind
  \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ METIS_TAC [full_heap_cases]);

val full_heap_step = prove(
  ``!n xs d b e m. full_heap b e m ==>
            (m e = H_BLOCK (xs,n,d)) /\ EMP_RANGE (e+1,e+n+1) m ==>
            full_heap b (e+n+1) m``,
  NTAC 3 STRIP_TAC
  \\ HO_MATCH_MP_TAC full_heap_ind \\ STRIP_TAC THEN1 METIS_TAC [full_heap_cases]
  \\ REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [full_heap_cases]);

val CUT_EQ = store_thm("CUT_EQ",
  ``((CUT (b,e) m a = H_BLOCK x) = (a IN RANGE (b,e) /\ (m a = H_BLOCK x))) /\
    ((CUT (b,e) m a = H_REF i) = (a IN RANGE (b,e) /\ (m a = H_REF i)))``,
  SIMP_TAC std_ss [CUT_def,IN_DEF] \\ SRW_TAC [] []);

val CUT_update = prove(
  ``~RANGE (i,j) k ==> (CUT (i,j) ((k =+ x) m) = CUT (i,j) m)``,
  SIMP_TAC std_ss [CUT_def,UPDATE_def,FUN_EQ_THM] \\ METIS_TAC []);

val part_heap_LESS_EQ = store_thm("part_heap_LESS_EQ",
  ``!b e m k. part_heap b e m k ==> b <= e``,
  HO_MATCH_MP_TAC part_heap_ind \\ REPEAT STRIP_TAC \\ DECIDE_TAC);

val EMP_RANGE_RANGE = store_thm("EMP_RANGE_RANGE",
  ``!b e i m.
      ~(RANGE(b,e)i) ==> (EMP_RANGE (b,e) ((i=+x)m) = EMP_RANGE (b,e) m)``,
  FULL_SIMP_TAC std_ss [EMP_RANGE_def,APPLY_UPDATE_THM,IN_DEF] \\ METIS_TAC []);

val part_heap_TRANS = store_thm("part_heap_TRANS",
  ``!j k2 b i m k1. part_heap b i m k1 /\ part_heap i j m k2 ==> part_heap b j m (k1+k2)``,
  NTAC 2 STRIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO]
  \\ HO_MATCH_MP_TAC part_heap_ind \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC
  THEN1 (REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [part_heap_cases])
  \\ REPEAT STRIP_TAC \\ RES_TAC \\ ONCE_REWRITE_TAC [part_heap_cases]
  \\ ASM_SIMP_TAC std_ss [heap_element_11] \\ DISJ2_TAC
  \\ Q.EXISTS_TAC `k1+k2` \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC);

val part_heap_IGNORE = store_thm("part_heap_IGNORE",
  ``!b e m k. part_heap b e m k /\ ~(RANGE(b,e)i) ==>
              part_heap b e ((i =+ x) m) k``,
  SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ HO_MATCH_MP_TAC part_heap_ind
  \\ STRIP_TAC THEN1 METIS_TAC [part_heap_cases]
  \\ STRIP_TAC THEN1
   (REPEAT STRIP_TAC \\ IMP_RES_TAC part_heap_LESS_EQ
    \\ `~(RANGE(b+1,e)i) /\ ~(i = b)` by RANGE_TAC \\ RES_TAC
    \\ METIS_TAC [APPLY_UPDATE_THM,part_heap_cases])
  \\ REPEAT STRIP_TAC \\ IMP_RES_TAC part_heap_LESS_EQ
  \\ `~RANGE (b + n + 1,e) i /\ ~(b = i) /\ ~(RANGE(b+1,b+n+1)i)` by RANGE_TAC
  \\ ONCE_REWRITE_TAC [part_heap_cases] \\ DISJ2_TAC \\ DISJ2_TAC
  \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,heap_element_11,EMP_RANGE_RANGE]);

val part_heap_EMP_RANGE = store_thm("part_heap_EMP_RANGE",
  ``!i m. b <= i /\ EMP_RANGE (b,i) m ==> part_heap b i m 0``,
  STRIP_TAC \\ completeInduct_on `i-b` \\ REPEAT STRIP_TAC \\ Cases_on `i = b`
  \\ FULL_SIMP_TAC std_ss [] THEN1 METIS_TAC [part_heap_cases]
  \\ `b+1 <= i /\ i - (b + 1) < i - b /\ (i - (b + 1) = i - (b + 1))` by DECIDE_TAC
  \\ ONCE_REWRITE_TAC [part_heap_cases] \\ DISJ2_TAC \\ DISJ1_TAC
  \\ SUBGOAL `(m b = H_EMP) /\ EMP_RANGE (b+1,i) m`
  THEN1 (RES_TAC \\ FULL_SIMP_TAC std_ss [isBLOCK_def,heap_element_distinct])
  \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF]
  \\ `RANGE(b,i)b` by RANGE_TAC \\ ASM_SIMP_TAC std_ss []
  \\ REPEAT STRIP_TAC \\ `RANGE(b,i)k` by RANGE_TAC \\ ASM_SIMP_TAC std_ss []);

val part_heap_REF = store_thm("part_heap_REF",
  ``!b e m k. part_heap b e m k /\ (m i = H_BLOCK (x,y,d)) /\ RANGE(b,e)i ==>
              y+1 <= k /\ part_heap b e ((i =+ H_REF t) m) (k - (y + 1))``,
  SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ HO_MATCH_MP_TAC part_heap_ind
  \\ STRIP_TAC THEN1 (REPEAT STRIP_TAC \\ `F` by RANGE_TAC)
  \\ STRIP_TAC THEN1
   (NTAC 7 STRIP_TAC \\ FULL_SIMP_TAC std_ss [] \\ Cases_on `i = b`
    THEN1 FULL_SIMP_TAC std_ss [isBLOCK_def,heap_element_11]
    \\ `RANGE (b + 1,e) i` by RANGE_TAC
    \\ METIS_TAC [APPLY_UPDATE_THM,part_heap_cases])
  \\ NTAC 10 STRIP_TAC \\ RES_TAC
  \\ Cases_on `RANGE (b + n + 1,e) i` THEN1
   (`~(i = b)` by RANGE_TAC \\ RES_TAC \\ STRIP_TAC THEN1 DECIDE_TAC
    \\ ONCE_REWRITE_TAC [part_heap_cases] \\ DISJ2_TAC \\ DISJ2_TAC
    \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM,heap_element_11]
    \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF,APPLY_UPDATE_THM]
    \\ Q.EXISTS_TAC `k-(y+1)` \\ STRIP_TAC THEN1 RANGE_TAC
    \\ ASM_SIMP_TAC std_ss [] \\ ALPHA_TAC "j" \\ REPEAT STRIP_TAC
    \\ Cases_on `i = j` \\ FULL_SIMP_TAC std_ss [heap_element_distinct] \\ RANGE_TAC)
  \\ Cases_on `RANGE (b + 1,b + n + 1) i` THEN1
   (FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF] \\ RES_TAC
    \\ FULL_SIMP_TAC std_ss [heap_element_distinct])
  \\ `i = b` by RANGE_TAC \\ FULL_SIMP_TAC std_ss [heap_element_11]
  \\ ONCE_REWRITE_TAC [part_heap_cases] \\ DISJ2_TAC \\ DISJ1_TAC
  \\ SIMP_TAC std_ss [isBLOCK_def,APPLY_UPDATE_THM,heap_element_distinct]
  \\ FULL_SIMP_TAC std_ss [DECIDE ``k+n+1-(n+1)=k``]
  \\ MATCH_MP_TAC part_heap_IGNORE \\ REVERSE STRIP_TAC THEN1 RANGE_TAC
  \\ ONCE_REWRITE_TAC [GSYM (RW1[ADD_COMM]ADD_0)]
  \\ MATCH_MP_TAC part_heap_TRANS \\ Q.EXISTS_TAC `b+n+1` \\ ASM_SIMP_TAC std_ss []
  \\ ASM_SIMP_TAC std_ss [part_heap_EMP_RANGE]);

val part_heap_LENGTH_LESS_EQ = store_thm("part_heap_LENGTH_LESS_EQ",
  ``!b e m k. part_heap b e m k ==> k <= e - b``,
  HO_MATCH_MP_TAC part_heap_ind \\ ASM_SIMP_TAC std_ss []
  \\ REPEAT STRIP_TAC \\ IMP_RES_TAC part_heap_LESS_EQ \\ DECIDE_TAC);

val CUT_UPDATE = store_thm("CUT_UPDATE",
  ``!b e a m x.
      (~(RANGE(b,e)a) ==> (CUT(b,e)((a=+x)m) = CUT(b,e)m)) /\
      (RANGE(b,e)a ==> (CUT(b,e)((a=+x)m) = (a=+x)(CUT(b,e)m)))``,
  FULL_SIMP_TAC std_ss [FUN_EQ_THM,CUT_def,APPLY_UPDATE_THM] \\ METIS_TAC []);

val ref_mem_IMP = prove(
  ``(ref_mem (h,f) m /\ (m n = H_BLOCK x) ==> n IN FDOM h /\ (h ' n = x)) /\
    (ref_mem (h,f) m /\ (m n = H_REF i) ==> ~(n IN FDOM h) /\ ~(f n = n) /\ (f n = i)) /\
    (ref_mem (h,f) m /\ (m n = H_EMP) ==> ~(n IN FDOM h) /\ (f n = n))``,
  SIMP_TAC std_ss [ref_mem_def,GSYM AND_IMP_INTRO]
  \\ METIS_TAC [heap_element_11,heap_element_distinct]);

val full_heap_LESS_EQ = store_thm("full_heap_LESS_EQ",
  ``!b e m. full_heap b e m ==> b <= e``,
  HO_MATCH_MP_TAC full_heap_ind \\ REPEAT STRIP_TAC \\ DECIDE_TAC);

val full_heap_IGNORE = prove(
  ``!m2 b e m. full_heap b e m /\ (!a. RANGE(b,e)a ==> (m2 a = m a)) ==>
               full_heap b e m2``,
  STRIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO]
  \\ HO_MATCH_MP_TAC full_heap_ind \\ REPEAT STRIP_TAC
  \\ ONCE_REWRITE_TAC [full_heap_cases] \\ SIMP_TAC std_ss [APPLY_UPDATE_THM]
  \\ IMP_RES_TAC full_heap_LESS_EQ
  \\ `RANGE (b,e) b` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC)
  \\ RES_TAC \\ DISJ2_TAC \\ ASM_SIMP_TAC std_ss [heap_element_11]
  \\ REPEAT STRIP_TAC THEN1
   (FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF]
    \\ REPEAT STRIP_TAC \\ RES_TAC
    \\ `RANGE (b,e) k` by RANGE_TAC \\ ASM_SIMP_TAC std_ss [])
  \\ Q.PAT_X_ASSUM `bbb ==> full_heap (b + n + 1) e m2` MATCH_MP_TAC
  \\ REPEAT STRIP_TAC \\ RES_TAC
  \\ `RANGE (b,e) a` by RANGE_TAC \\ ASM_SIMP_TAC std_ss []);

val full_heap_RANGE = store_thm("full_heap_RANGE",
  ``!i x b e m. full_heap b e m /\ ~(RANGE(b,e)i) ==> full_heap b e ((i =+ x) m)``,
  REPEAT STRIP_TAC \\ MATCH_MP_TAC full_heap_IGNORE \\ Q.EXISTS_TAC `m`
  \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM] \\ REPEAT STRIP_TAC
  \\ Cases_on `a = i` \\ FULL_SIMP_TAC std_ss [RANGE_def]);

val full_heap_R0 = prove(
  ``!b e m. full_heap b e m ==> !k. RANGE(b,e)k ==> ~(R0 m k)``,
  HO_MATCH_MP_TAC full_heap_ind \\ REPEAT STRIP_TAC
  THEN1 (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC)
  \\ Cases_on `b = k` \\ FULL_SIMP_TAC std_ss [R0,heap_element_distinct]
  \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF,heap_element_distinct]
  \\ Cases_on `RANGE (b + n + 1,e) k` THEN1 METIS_TAC []
  \\ `RANGE (b + 1,b + n + 1) k` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC)
  \\ RES_TAC \\ FULL_SIMP_TAC std_ss [R0,heap_element_distinct]);

(* proof *)

val move_lemma = store_thm("move_lemma",
  ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z UNION {n}) /\
    n IN (DR0(CUT(b2,e2)m)) ==>
    (m n = H_REF (f n)) /\ ~(f n = n) \/
    getLENGTH (m n) <= e - j /\ (m n = H_BLOCK (h ' n)) /\ n IN FDOM h /\ ~(n = j) /\
    n IN RANGE(b2,e2) /\ (f n = n) /\ EMP_RANGE (j,j+getLENGTH(H_BLOCK (h ' n))) m``,
  PURE_ONCE_REWRITE_TAC [gc_inv_THM] \\ ONCE_REWRITE_TAC [IN_DEF] \\ STRIP_TAC
  \\ FULL_SIMP_TAC std_ss [gc_inv_def] \\ FULL_SIMP_TAC std_ss [DR0,R0,D0,CUT_EQ]
  \\ IMP_RES_TAC ref_mem_IMP \\ ASM_SIMP_TAC std_ss [heap_element_11,heap_element_distinct]
  \\ SIMP_TAC std_ss [getLENGTH_def] \\ `n < e2` by RANGE_TAC
  \\ `(CUT(b2,e2)m) n = H_BLOCK (x,y,z')` by FULL_SIMP_TAC std_ss [CUT_EQ]
  \\ FULL_SIMP_TAC std_ss [IN_DEF]
  \\ IMP_RES_TAC part_heap_REF \\ STRIP_TAC THEN1 RANGE_TAC
  \\ FULL_SIMP_TAC std_ss [abs_gc_inv_def,LET_DEF]
  \\ STRIP_TAC THEN1 RANGE_TAC
  \\ STRIP_TAC THEN1
      (`n IN FDOM h` by FULL_SIMP_TAC std_ss [IN_DEF] \\ CCONTR_TAC
       \\ `n IN D0 (CUT (i,j) m) \/ n IN D0 (CUT (b,i) m)` by METIS_TAC []
       \\ FULL_SIMP_TAC std_ss [D0,CUT_EQ,IN_DEF] \\ RANGE_TAC)
   \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF]
   \\ REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `!k. bbb ==> (m k = H_EMP)` MATCH_MP_TAC
   \\ RANGE_TAC);

val ADDR_SET_THM = store_thm("ADDR_SET_THM",
  ``(ADDR_SET [] = {}) /\
    (ADDR_SET (H_DATA x :: xs) = ADDR_SET xs) /\
    (ADDR_SET (H_ADDR y :: xs) = y INSERT ADDR_SET xs)``,
  SRW_TAC [] [ADDR_SET_def,EXTENSION,MEM,NOT_IN_EMPTY,IN_INSERT]);

val CUT_EMPTY = store_thm("CUT_EMPTY",
  ``(D0(CUT(j,j)m) = {}) /\ (D1(CUT(j,j)m) = {}) /\
    (R0(CUT(j,j)m) = {}) /\ (R1(CUT(j,j)m) = {})``,
  SIMP_TAC std_ss [EXTENSION,NOT_IN_EMPTY]
  \\ `!j n. ~RANGE(j,j)n` by RANGE_TAC
  \\ ASM_SIMP_TAC std_ss [IN_DEF,D0,R0,D1,R1,CUT_EQ]);

val remove_from_z = prove(
  ``~(f n = n) ==> abs_steps (h,x,y,z UNION {n},f) (h,x,y,z,f)``,
  REPEAT STRIP_TAC \\ SIMP_TAC std_ss [abs_steps_def] \\ Cases_on `n IN z`
  THEN1 (`z UNION {n} = z` by SET_TAC \\ FULL_SIMP_TAC std_ss [RTC_REFL])
  \\ `(z,f) = ((z UNION {n}) DELETE n,f)` by SET_TAC
  \\ POP_ASSUM (fn th => ONCE_REWRITE_TAC [th]) \\ MATCH_MP_TAC RTC_SINGLE
  \\ SIMP_TAC std_ss [abs_step_cases] \\ SET_TAC);

val full_heap_BLOCK = prove(
  ``!b e m. full_heap b e m /\ (m i = H_BLOCK (x2,y,z2)) ==>
            full_heap b e ((i =+ H_BLOCK (x,y,z)) m)``,
  SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ HO_MATCH_MP_TAC full_heap_ind
  \\ SIMP_TAC std_ss [full_heap_REFL] \\ REPEAT STRIP_TAC \\ RES_TAC
  \\ ONCE_REWRITE_TAC [full_heap_cases]
  \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF,APPLY_UPDATE_THM]
  \\ METIS_TAC [heap_element_11,heap_element_distinct,PAIR_EQ]);

val move_thm = store_thm("move_thm",
  ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z UNION ADDR_SET [x]) /\
    ADDR_SET [x] SUBSET (DR0(CUT(b2,e2)m)) /\
    (move (x,j,m) = (x2,j2,m2)) ==>
      ?h2 f2. gc_inv (h1,roots1,h2,f2) (b,i,j2,e,b2,e2,m2,z UNION (D1(CUT(j,j2)m2))) /\ j <= j2 /\
              DR0 (CUT (b2,e2) m) SUBSET DR0 (CUT (b2,e2) m2) /\
              (CUT(b,j)m = CUT(b,j)m2) /\
              (!a. ~(f a = a) ==> (f2 a = f a)) /\
              (!a. a IN ADDR_SET [x2] ==> ~(f2 a = a)) /\
              ([x2] = ADDR_MAP f2 [x]) /\ full_heap j j2 m2``,
  CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [gc_inv_THM]))
  \\ REVERSE (Cases_on `x`) THEN1
   (SIMP_TAC std_ss [move_def] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
    \\ sg `ADDR_SET [H_DATA a] = {}` \\ ASM_SIMP_TAC std_ss [full_heap_REFL]
    \\ ASM_SIMP_TAC std_ss [ADDR_SET_def,SUBSET_DEF,MEM,NOT_IN_EMPTY,ADDR_MAP_def,
          heap_address_distinct,EXTENSION,UNION_EMPTY,CUT_EMPTY] \\ SET_TAC)
  \\ SIMP_TAC std_ss [ADDR_SET_THM,INSERT_SUBSET,EMPTY_SUBSET]
  \\ STRIP_TAC
  \\ IMP_RES_TAC move_lemma \\ FULL_SIMP_TAC std_ss [heap_element_distinct]
  THEN1
   (Q.LIST_EXISTS_TAC [`h`,`f`] \\ ASM_SIMP_TAC std_ss []
    \\ Q.PAT_X_ASSUM `move xx = fg` MP_TAC \\ ASM_SIMP_TAC (srw_ss()) [move_def]
    \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [ADDR_SET_THM,
         IN_INSERT,NOT_IN_EMPTY,CUT_EMPTY,UNION_EMPTY,full_heap_REFL]
    \\ FULL_SIMP_TAC std_ss [gc_inv_def,ADDR_MAP_def] \\ IMP_RES_TAC remove_from_z
    \\ `f o f = I` by METIS_TAC [abs_gc_inv_def] \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM]
    \\ METIS_TAC [abs_steps_thm,remove_from_z,abs_steps_TRANS])
  \\ `?x y d. h ' n = (x,y,d)` by METIS_TAC [PAIR]
  \\ Q.PAT_X_ASSUM `move xx = fg` MP_TAC \\ ASM_SIMP_TAC (srw_ss()) [move_def]
  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [LET_DEF,DECIDE ``j <= j + y + 1``]
  \\ STRIP_TAC
  \\ Q.LIST_EXISTS_TAC [`h |+ (j,h ' n) \\ n`,`(n =+ j) ((j =+ n) f)`] \\ ASM_SIMP_TAC std_ss []
  \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,ADDR_SET_THM,IN_INSERT,NOT_IN_EMPTY]
  \\ `full_heap j (j + y + 1) ((j =+ H_BLOCK (x,y,d)) ((n =+ H_REF j) m))` by
    (Q.PAT_X_ASSUM `~(n = j)` (fn th => REWRITE_TAC [MATCH_MP UPDATE_COMMUTES (GSYM th)])
     \\ `~(RANGE(j,j+y+1)n)` by
      (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [IN_DEF,R0,D0,DR0,EMP_RANGE_def,
         getLENGTH_def,ADD_ASSOC,heap_element_distinct])
     \\ MATCH_MP_TAC full_heap_RANGE \\ ASM_SIMP_TAC std_ss []
     \\ ONCE_REWRITE_TAC [full_heap_cases] \\ DISJ2_TAC
     \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,heap_element_11,full_heap_REFL,
          EMP_RANGE_def,getLENGTH_def,IN_DEF,ADD_ASSOC] \\ REPEAT STRIP_TAC
     \\ `~(j = k) /\ RANGE (j,j + y + 1) k` by RANGE_TAC \\ SET_TAC)
  \\ REVERSE STRIP_TAC THEN1
   (`~(RANGE(b,j)j) /\ ~(RANGE(b,j)n) /\ ~(RANGE(b2,e2)j)` by RANGE_TAC
    \\ ASM_SIMP_TAC std_ss [CUT_UPDATE,ADDR_MAP_def]
    \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,DR0,IN_DEF,D0,R0,CUT_EQ,APPLY_UPDATE_THM]
    \\ FULL_SIMP_TAC std_ss [getLENGTH_def,EMP_RANGE_def,ADD_ASSOC,IN_DEF]
    \\ `RANGE (j,j + y + 1) j` by RANGE_TAC
    \\ FULL_SIMP_TAC std_ss [gc_inv_def,FUN_EQ_THM,abs_gc_inv_def,LET_DEF]
    \\ `f j = j` by METIS_TAC [ref_mem_def,heap_element_distinct]
    \\ REPEAT STRIP_TAC \\ METIS_TAC [heap_element_11,heap_element_distinct,PAIR_EQ])
  \\ FULL_SIMP_TAC std_ss [gc_inv_def]
  \\ FULL_SIMP_TAC std_ss [getLENGTH_def]
  \\ `~(RANGE(b,i)j) /\ ~(RANGE(b,i)n) /\ ~(RANGE(i,j)j) /\
      ~(RANGE(i,j)n) /\ ~(RANGE(b2,e2)j)` by RANGE_TAC
  \\ REPEAT STRIP_TAC THEN1 RANGE_TAC THEN1 RANGE_TAC
  THEN1 (`~(j = k) /\ ~(n = k) /\ ~RANGE (b,j) k` by RANGE_TAC \\ METIS_TAC [APPLY_UPDATE_THM])
  THEN1 METIS_TAC [full_heap_RANGE]
  THEN1
   (MATCH_MP_TAC full_heap_TRANS \\ Q.EXISTS_TAC `j` \\ ASM_SIMP_TAC std_ss [full_heap_RANGE])
  THEN1
   (Q.EXISTS_TAC `len - (y+1)` \\ FULL_SIMP_TAC std_ss [IN_DEF]
    \\ IMP_RES_TAC (Q.INST [`t`|->`j`] part_heap_REF)
    \\ REVERSE STRIP_TAC THEN1 DECIDE_TAC
    \\ MATCH_MP_TAC part_heap_IGNORE \\ ASM_SIMP_TAC std_ss [])
  THEN1
   (SIMP_TAC std_ss [ref_mem_def,APPLY_UPDATE_THM,FDOM_FUPDATE,FDOM_DOMSUB,
      IN_INSERT,IN_DELETE,FAPPLY_FUPDATE_THM,DOMSUB_FAPPLY_THM]
    \\ ALPHA_TAC "k" \\ REPEAT STRIP_TAC
    \\ Cases_on `j = k` \\ FULL_SIMP_TAC std_ss []
    \\ Cases_on `k = n` \\ FULL_SIMP_TAC std_ss [ref_mem_def])
  \\ FULL_SIMP_TAC std_ss [CUT_UPDATE]
  \\ Q.PAT_X_ASSUM `~(n = j)` (fn th => REWRITE_TAC [MATCH_MP UPDATE_COMMUTES (GSYM th)] THEN ASSUME_TAC th)
  \\ `~(RANGE(j,j + y + 1)n) /\ ~(RANGE(i,j + y + 1)n)` by RANGE_TAC
  \\ FULL_SIMP_TAC std_ss [CUT_UPDATE]
  \\ REPEAT (Q.PAT_X_ASSUM `~(RANGE(xx,yy)df)` (K ALL_TAC))
  \\ `!k. RANGE (i,j + y + 1) k /\ ~RANGE (i,j) k  ==> RANGE (j,j + y + 1) k` by RANGE_TAC
  \\ `D0 (CUT (i,j + y + 1) ((j =+ H_BLOCK (x,y,d)) m)) =
       j INSERT D0 (CUT (i,j) m)` by
     (FULL_SIMP_TAC std_ss [EXTENSION,IN_INSERT]
      \\ FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,APPLY_UPDATE_THM,EMP_RANGE_def,IN_DEF]
      \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1
       (Cases_on `j = x'` \\ FULL_SIMP_TAC std_ss [heap_element_11]
        \\ CCONTR_TAC \\ `RANGE(j,j+y+1)x'` by RANGE_TAC
        \\ METIS_TAC [heap_element_distinct,ADD_ASSOC])
      \\ Cases_on `j = x'` \\ FULL_SIMP_TAC std_ss [heap_element_11] \\ RANGE_TAC)
  \\ `D1 (CUT (j,j + y + 1) ((j =+ H_BLOCK (x,y,d)) m)) = ADDR_SET x` by
     (FULL_SIMP_TAC std_ss [FUN_EQ_THM,D1,CUT_EQ,IN_DEF,APPLY_UPDATE_THM,EMP_RANGE_def]
      \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC
      THEN1 (Cases_on `j = k` \\ METIS_TAC
        [heap_element_11,heap_element_distinct,PAIR_EQ,ADD_ASSOC])
      \\ Q.EXISTS_TAC `j` \\ ASM_SIMP_TAC std_ss [heap_element_11] \\ RANGE_TAC)
  \\ ASM_SIMP_TAC std_ss []
  \\ MATCH_MP_TAC abs_steps_TRANS
  \\ Q.EXISTS_TAC `(h,D0 (CUT (b,i) m),D0 (CUT (i,j) m),z UNION {n},f)`
  \\ ASM_SIMP_TAC std_ss []
  \\ MATCH_MP_TAC abs_steps_TRANS
  \\ Q.EXISTS_TAC `(h |+ (j,x,y,d) \\ n,D0 (CUT (b,i) m),j INSERT D0 (CUT (i,j) m),
       (z UNION ADDR_SET x) UNION {n},(n =+ j) ((j =+ n) f))`
  \\ REVERSE STRIP_TAC
  THEN1 (MATCH_MP_TAC remove_from_z \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM])
  \\ `!xx. z UNION xx UNION {n} = z UNION {n} UNION xx` by SET_TAC
  \\ ASM_SIMP_TAC std_ss []
  \\ SIMP_TAC std_ss [abs_steps_def] \\ MATCH_MP_TAC RTC_SINGLE
  \\ SIMP_TAC std_ss [abs_step_cases] \\ DISJ2_TAC \\ DISJ2_TAC
  \\ Q.LIST_EXISTS_TAC [`n`,`j`,`x`,`(y,d)`] \\ ASM_SIMP_TAC std_ss []
  \\ STRIP_TAC THEN1 SET_TAC
  \\ `~RANGE (b2,e2) j /\ ~RANGE (b,j) j` by RANGE_TAC
  \\ `m j = H_EMP` by SET_TAC
  \\ Q.PAT_X_ASSUM `ref_mem (h,f) m` (fn th => FULL_SIMP_TAC std_ss [RW[ref_mem_def]th])
  \\ METIS_TAC [heap_element_distinct,IN_UNION,IN_INSERT]);

val ADDR_SET_CONS = store_thm("ADDR_SET_CONS",
  ``!h xs. ADDR_SET (h::xs) = ADDR_SET xs UNION ADDR_SET [h]``,
  Cases \\ FULL_SIMP_TAC std_ss [ADDR_SET_THM,EXTENSION,IN_UNION] \\ SET_TAC);

val D1_UNION = store_thm("D1_UNION",
  ``b <= i /\ i <= j ==> (D1(CUT(b,j)m) = D1(CUT(b,i)m) UNION D1(CUT(i,j)m)) /\
                         (D0(CUT(b,j)m) = D0(CUT(b,i)m) UNION D0(CUT(i,j)m))``,
  SIMP_TAC std_ss [EXTENSION,IN_UNION] \\ SIMP_TAC std_ss [IN_DEF,D1,CUT_EQ,D0]
  \\ REPEAT STRIP_TAC \\ `!k. RANGE(b,j)k = RANGE(b,i)k \/ RANGE(i,j)k` by RANGE_TAC
  \\ SET_TAC);

val D1_CUT_EQ_ADDR_SET_THM = prove(
  ``(m j = H_BLOCK (x,y,d)) /\ EMP_RANGE (j+1,j+y+1) m ==>
    (D1 (CUT (j,j + y + 1) m) = ADDR_SET x)``,
  FULL_SIMP_TAC std_ss [FUN_EQ_THM,D1,CUT_EQ,IN_DEF,APPLY_UPDATE_THM,EMP_RANGE_def]
  \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC
  THEN1 (Cases_on `j = k` \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF]
         THEN1 METIS_TAC [heap_element_11,heap_element_distinct,PAIR_EQ,ADD_ASSOC]
         \\ `RANGE (j + 1,j + y + 1) k` by RANGE_TAC
         \\ METIS_TAC [heap_element_distinct])
  \\ Q.EXISTS_TAC `j` \\ ASM_SIMP_TAC std_ss [heap_element_11] \\ RANGE_TAC);

val EQ_RANGE_def = Define `
  EQ_RANGE (b,e) m m2 = !k. k IN RANGE (b,e) ==> (m k = m2 k)`;

val EQ_RANGE_IMP_EQ_RANGE = store_thm("EQ_RANGE_IMP_EQ_RANGE",
  ``!b e i j m m2. EQ_RANGE (b,e) m m2 /\ b <= i /\ j <= e ==> EQ_RANGE (i,j) m m2``,
  SIMP_TAC std_ss [EQ_RANGE_def,IN_DEF,RANGE_def] \\ REPEAT STRIP_TAC
  \\ Q.PAT_X_ASSUM `!k.bbb` MATCH_MP_TAC \\ DECIDE_TAC);

val EQ_RANGE_full_heap = store_thm("EQ_RANGE_full_heap",
  ``!m2 b e m. full_heap b e m /\ EQ_RANGE (b,e) m m2 ==> full_heap b e m2``,
  STRIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ HO_MATCH_MP_TAC full_heap_ind
  \\ REPEAT STRIP_TAC THEN1 METIS_TAC [full_heap_cases]
  \\ ONCE_REWRITE_TAC [full_heap_cases] \\ IMP_RES_TAC full_heap_LESS_EQ
  \\ `~(e = b)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss []
  \\ `b IN RANGE (b,e)` by (SIMP_TAC std_ss [RANGE_def,IN_DEF] \\ DECIDE_TAC)
  \\ `m2 b = m b` by METIS_TAC [EQ_RANGE_def]
  \\ ASM_SIMP_TAC std_ss [heap_element_11]
  \\ `b <= b + n + 1 /\ e <= e` by DECIDE_TAC \\ REVERSE STRIP_TAC
  THEN1 (IMP_RES_TAC EQ_RANGE_IMP_EQ_RANGE \\ RES_TAC \\ ASM_SIMP_TAC std_ss [])
  \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF]
  \\ REPEAT STRIP_TAC \\ RES_TAC
  \\ `k IN RANGE (b,e)` suffices_by METIS_TAC [EQ_RANGE_def]
  \\ FULL_SIMP_TAC std_ss [RANGE_def,IN_DEF] \\ DECIDE_TAC);

val EQ_RANGE_CUT = store_thm("EQ_RANGE_CUT",
  ``EQ_RANGE (b,i) m (CUT (b,i) m)``,
  SIMP_TAC std_ss [EQ_RANGE_def,CUT_def,IN_DEF]);

val EQ_RANGE_THM = store_thm("EQ_RANGE_THM",
  ``(CUT (b,e) m1 = CUT (b,e) m2) ==> EQ_RANGE (b,e) m1 m2``,
  FULL_SIMP_TAC std_ss [CUT_def,FUN_EQ_THM,EQ_RANGE_def,IN_DEF] \\ SET_TAC);

val move_list_thm = store_thm("move_list_thm",
  ``!xs z h f m j xs2 j2 (m2:num -> ('a,'b) heap_element).
      gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z UNION ADDR_SET xs) /\
      ADDR_SET xs SUBSET (DR0(CUT(b2,e2)m)) /\
      (move_list (xs,j,m) = (xs2,j2,m2)) ==>
        ?h3 f3. gc_inv (h1,roots1,h3,f3) (b,i,j2,e,b2,e2,m2,z UNION (D1(CUT(j,j2)m2))) /\ j <= j2 /\
                DR0 (CUT (b2,e2) m) SUBSET DR0 (CUT (b2,e2) m2) /\
                (CUT(b,j)m = CUT(b,j)m2) /\
                (!a. ~(f a = a) ==> (f3 a = f a)) /\
                (!a. a IN ADDR_SET xs2 ==> ~(f3 a = a)) /\
                (xs2 = ADDR_MAP f3 xs) /\ full_heap j j2 m2``,
  Induct \\ SIMP_TAC std_ss [ADDR_SET_THM,UNION_EMPTY,move_list_def,ADDR_MAP_def,
    NOT_IN_EMPTY,CUT_EMPTY,LET_DEF,full_heap_REFL] THEN1 SET_TAC
  \\ ONCE_REWRITE_TAC [ADDR_SET_CONS]
  \\ NTAC 6 STRIP_TAC \\ FULL_SIMP_TAC std_ss [UNION_SUBSET]
  \\ `?x3 j3 m3. move (h,j,m) = (x3,j3,m3)` by METIS_TAC [PAIR]
  \\ `?xs4 j4 m4. move_list (xs,j3,m3) = (xs4,j4,m4)` by METIS_TAC [PAIR]
  \\ FULL_SIMP_TAC std_ss [UNION_ASSOC] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
  \\ REPEAT STRIP_TAC
  \\ IMP_RES_TAC move_thm \\ Q.PAT_X_ASSUM `!z roots1 i. bb` (K ALL_TAC)
  \\ Q.PAT_X_ASSUM `!z h f.bbb` (MP_TAC o Q.SPECL [
       `z UNION D1(CUT(j,j3)(m3:num -> ('a,'b) heap_element))`,
       `h2`,`f2`,`m3`,`j3`,`xs4`,`j4`,`m4`])
  \\ `ADDR_SET xs SUBSET DR0 (CUT (b2,e2) m3)` by SET_TAC
  \\ FULL_SIMP_TAC std_ss [AC UNION_ASSOC UNION_COMM]
  \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [IN_UNION]
  \\ Q.LIST_EXISTS_TAC [`h3`,`f3`] \\ `j <= j4` by DECIDE_TAC
  \\ ONCE_REWRITE_TAC [ADDR_SET_CONS] \\ ASM_SIMP_TAC std_ss []
  \\ `(CUT (b,j) m3 = CUT (b,j) m4) /\ (CUT (j,j3) m3 = CUT (j,j3) m4)` by
      (`!k. k < j ==> k < j3` by DECIDE_TAC
       \\ `!k. j <= k ==> b <= k` by RANGE_TAC
       \\ FULL_SIMP_TAC std_ss [CUT_def,RANGE_def,FUN_EQ_THM] \\ SET_TAC)
  \\ IMP_RES_TAC EQ_RANGE_THM \\ IMP_RES_TAC EQ_RANGE_full_heap
  \\ IMP_RES_TAC full_heap_TRANS \\ ASM_SIMP_TAC std_ss []
  \\ REVERSE STRIP_TAC THEN1
   (ASM_SIMP_TAC std_ss [] \\ STRIP_TAC THEN1 SET_TAC \\ STRIP_TAC THEN1 SET_TAC
    \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [ADDR_MAP_def,CONS_11,
      ADDR_SET_def,MEM,heap_address_11] \\ IMP_RES_TAC gc_inv_IMP
    \\ `f2 (f2 n) = n` by FULL_SIMP_TAC std_ss [gc_inv_def,FUN_EQ_THM,abs_gc_inv_def,LET_DEF]
    \\ FULL_SIMP_TAC std_ss [])
  \\ `D1 (CUT (j,j4) m4) = D1 (CUT (j,j3) m4) UNION D1 (CUT (j3,j4) m4)`
       by METIS_TAC [D1_UNION] \\ FULL_SIMP_TAC std_ss [AC UNION_ASSOC UNION_COMM]);

val D0_UPDATE = store_thm("D0_UPDATE",
  ``!i x m. i IN D0 m ==> (D0 ((i =+ H_BLOCK x) m) = D0 m)``,
  SIMP_TAC std_ss [FORALL_PROD,FUN_EQ_THM,IN_DEF,D0,CUT_EQ,APPLY_UPDATE_THM]
  \\ METIS_TAC []);

val gc_step_lemma = store_thm("gc_step_lemma",
  ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,D1(CUT(i,j)m)) ==> ~(i = j) ==>
    ?xs n d. (m i = H_BLOCK (xs,n,d)) /\
             EMP_RANGE (i + 1,i + n + 1) m /\
             full_heap (i + n + 1) j m /\
             ADDR_SET xs SUBSET DR0 (CUT (b2,e2) m) /\
             (D1 (CUT (i,j) m) = D1 (CUT (i+n+1,j) m) UNION ADDR_SET xs)``,
  SIMP_TAC std_ss [gc_step_def,LET_DEF] \\ REPEAT STRIP_TAC \\ IMP_RES_TAC gc_inv_IMP
  \\ `full_heap i j m` by METIS_TAC [gc_inv_def] \\ POP_ASSUM MP_TAC
  \\ ONCE_REWRITE_TAC [full_heap_cases] \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC
  \\ ASM_SIMP_TAC std_ss [heap_element_11] \\ STRIP_TAC THEN1 METIS_TAC [full_heap_cases]
  \\ IMP_RES_TAC full_heap_LESS_EQ
  \\ `i < i + n + 1 /\ i <= i + n + 1` by DECIDE_TAC
  \\ `D1 (CUT (i,j) m) = D1 (CUT (i+n+1,j) m) UNION ADDR_SET xs`
       by METIS_TAC [D1_UNION,D1_CUT_EQ_ADDR_SET_THM,UNION_COMM]
  \\ ASM_SIMP_TAC std_ss []
  \\ `i IN FDOM h /\ (h ' i = (xs,n,d))` by METIS_TAC [gc_inv_def,
       ref_mem_def, heap_element_distinct,heap_element_11,PAIR_EQ]
    \\ `i IN (UNIV DIFF D0 (CUT (b,i) m))` by
      (FULL_SIMP_TAC std_ss [IN_DIFF,IN_UNIV]
       \\ FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11] \\ RANGE_TAC)
    \\ `ADDR_SET xs SUBSET POINTERS h (UNIV DIFF D0 (CUT (b,i) m))`
         by METIS_TAC [set_SUBSET_POINTERS]
    \\ `D0 (CUT (b,i) m) UNION D0 (CUT (i,j) m) = D0 (CUT(b,j)m)`
         by METIS_TAC [D1_UNION,gc_inv_def,abs_gc_inv_def]
    \\ `ADDR_SET xs SUBSET (FDOM h UNION HAS_CHANGED f DIFF (D0 (CUT (b,j) m)))` by
         (FULL_SIMP_TAC std_ss [gc_inv_def,abs_gc_inv_def,LET_DEF] \\ SET_TAC)
    \\ SIMP_TAC std_ss [SUBSET_DEF] \\ REPEAT STRIP_TAC
    \\ `x IN (FDOM h UNION HAS_CHANGED f DIFF D0 (CUT (b,j) m))` by SET_TAC
    \\ Cases_on `x IN FDOM h` THEN1
     (`~(x IN D0 (CUT (b,j) m))` by SET_TAC
      \\ POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ]
      \\ `?x1 y1 d1. h ' x = (x1,y1,d1)` by METIS_TAC [PAIR]
      \\ `m x = H_BLOCK (x1,y1,d1)` by METIS_TAC [ref_mem_def,gc_inv_def]
      \\ FULL_SIMP_TAC std_ss [heap_element_11,DR0,D0,R0,CUT_EQ,
           heap_element_distinct,IN_DEF] \\ CCONTR_TAC
      \\ FULL_SIMP_TAC std_ss [gc_inv_def,abs_gc_inv_def,LET_DEF]
      \\ METIS_TAC [heap_element_distinct])
    \\ FULL_SIMP_TAC std_ss [IN_DIFF,IN_UNION]
    \\ Q.PAT_X_ASSUM `~(x IN D0 (CUT (b,j) m))` MP_TAC
    \\ SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ]
    \\ FULL_SIMP_TAC std_ss [HAS_CHANGED_def]
    \\ FULL_SIMP_TAC std_ss [gc_inv_def,abs_gc_inv_def,LET_DEF]
    \\ `m x = H_REF (f x)` by METIS_TAC [ref_mem_def]
    \\ FULL_SIMP_TAC std_ss [heap_element_distinct,DR0,D0,R0,CUT_EQ,heap_element_11]
    \\ SIMP_TAC std_ss [IN_DEF]
    \\ `full_heap b j m` by METIS_TAC [full_heap_TRANS]
    \\ `R0 m x` by FULL_SIMP_TAC std_ss [R0,heap_element_11]
    \\ CCONTR_TAC \\ METIS_TAC [full_heap_R0,heap_element_distinct]);

val gc_step_thm = store_thm("gc_step_thm",
  ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,D1(CUT(i,j)m)) /\ ~(i = j) ==>
    (gc_step (i,j,m) = (i2,j2,m2)) ==>
    ?h3 f3. gc_inv (h1,roots1,h3,f3) (b,i2,j2,e,b2,e2,m2,D1(CUT(i2,j2)m2)) /\
            i < i2 /\ j <= j2 /\ !a. ~(f a = a) ==> (f3 a = f a)``,
  STRIP_TAC \\ IMP_RES_TAC gc_inv_IMP \\ STRIP_ASSUME_TAC (UNDISCH_ALL gc_step_lemma)
  \\ ASM_SIMP_TAC std_ss [gc_step_def,LET_DEF,getBLOCK_def]
  \\ `?xs3 j3 m3. move_list (xs,j,m) = (xs3,j3,m3)` by METIS_TAC [PAIR]
  \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ helperLib.EXPAND_TAC
  \\ `~RANGE(i + n + 1,j3)i` by RANGE_TAC \\ FULL_SIMP_TAC std_ss [CUT_UPDATE]
  \\ IMP_RES_TAC full_heap_LESS_EQ
  \\ `i < i + n + 1 /\ i <= i + n + 1` by DECIDE_TAC
  \\ FULL_SIMP_TAC std_ss []
  \\ Q.PAT_X_ASSUM `gc_inv (h1,roots1,h,f) xxx` (fn th => ASSUME_TAC th THEN
       MP_TAC (Q.INST [`xs2`|->`xs3`,`j2`|->`j3`,`m2`|->`m3`]
               (helperLib.MATCH_INST (SPEC_ALL move_list_thm) (concl th))))
  \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC
  \\ `CUT (i + n + 1,j) m = CUT (i + n + 1,j) m3` by
    (FULL_SIMP_TAC std_ss [gc_inv_def,abs_gc_inv_def,LET_DEF]
     \\ `!k. i + n + 1 <= k ==> b <= k` by DECIDE_TAC
     \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM,CUT_def,RANGE_def] \\ SET_TAC)
  \\ `i + n + 1 <= j` by RANGE_TAC
  \\ `D1 (CUT (i + n + 1,j) m3) UNION D1 (CUT (j,j3) m3) = D1 (CUT (i + n + 1,j3) m3)`
         by METIS_TAC [D1_UNION,gc_inv_def,abs_gc_inv_def]
  \\ FULL_SIMP_TAC std_ss [] \\ Q.LIST_EXISTS_TAC [`h3 |+ (i,ADDR_MAP f3 xs,n,d)`,`f3`]
  \\ `~RANGE(b2,e2)i /\ RANGE(b,j3)i /\ RANGE(b,i+n+1)i` by RANGE_TAC
  \\ FULL_SIMP_TAC std_ss [gc_inv_def,CUT_UPDATE]
  \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM]
  \\ STRIP_TAC THEN1 RANGE_TAC \\ STRIP_TAC THEN1 METIS_TAC []
  \\ `i IN D0 (CUT (b,i + n + 1) m3) /\
      (m3 i = H_BLOCK (xs,n,d))` by
     (`!k. k < i + n + 1 ==> k < j` by DECIDE_TAC
      \\ FULL_SIMP_TAC std_ss []
      \\ `CUT (b,i+n+1) m3 = CUT (b,i+n+1) m` by
          (FULL_SIMP_TAC std_ss [CUT_def,RANGE_def] \\ SET_TAC)
      \\ `(CUT(b,i+n+1)m3) i = H_BLOCK (xs,n,d)` by
             (FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [CUT_EQ,IN_DEF])
      \\ FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11])
  \\ FULL_SIMP_TAC std_ss [D0_UPDATE]
  \\ STRIP_TAC THEN1
   (MATCH_MP_TAC (RW[AND_IMP_INTRO]full_heap_step)
    \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,heap_element_11,EMP_RANGE_def,IN_DEF]
    \\ STRIP_TAC THEN1 METIS_TAC [full_heap_BLOCK]
    \\ FULL_SIMP_TAC std_ss [CUT_def,FUN_EQ_THM] \\ REPEAT STRIP_TAC
    \\ `RANGE (b,j) k /\ ~(RANGE (i + 1,i + n + 1) i)` by RANGE_TAC \\ SET_TAC)
  \\ STRIP_TAC THEN1
   (FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11]
    \\ `~(i = j3)` by RANGE_TAC
    \\ METIS_TAC [full_heap_BLOCK,full_heap_cases,heap_element_11,PAIR_EQ])
  \\ STRIP_TAC THEN1
   (Q.EXISTS_TAC `len'` \\ ASM_SIMP_TAC std_ss []
    \\ MATCH_MP_TAC part_heap_IGNORE \\ ASM_SIMP_TAC std_ss [])
  \\ REPEAT STRIP_TAC THEN1
   (FULL_SIMP_TAC std_ss [ref_mem_def,APPLY_UPDATE_THM,FDOM_FUPDATE,IN_INSERT]
    \\ REPEAT STRIP_TAC \\ Cases_on `i = a`
    \\ FULL_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM])
  \\ MATCH_MP_TAC abs_steps_TRANS
  \\ Q.EXISTS_TAC `(h3,D0 (CUT (b,i) m3),D0 (CUT (i,j3) m3),
          D1 (CUT (i + n + 1,j3) m3),f3)` \\ ASM_SIMP_TAC std_ss []
  \\ SIMP_TAC std_ss [abs_steps_def]
  \\ MATCH_MP_TAC RTC_SINGLE
  \\ SIMP_TAC std_ss [abs_step_cases] \\ DISJ2_TAC \\ DISJ1_TAC
  \\ Q.LIST_EXISTS_TAC [`i`,`xs`,`(n,d)`] \\ ASM_SIMP_TAC std_ss []
  \\ IMP_RES_TAC ok_heap_IMP \\ IMP_RES_TAC abs_steps_thm \\ POP_ASSUM (K ALL_TAC)
  \\ `f3 o f3 = I` by FULL_SIMP_TAC std_ss [gc_inv_def,abs_gc_inv_def,LET_DEF]
  \\ FULL_SIMP_TAC std_ss [SET_TRANSLATE_MAP,SET_TRANSLATE_def]
  \\ Q.PAT_X_ASSUM `!a. bbb` (MP_TAC o Q.GEN `a` o Q.SPEC `(f3:num->num) a`)
  \\ `!k. f3 (f3 k) = (k:num)` by FULL_SIMP_TAC std_ss [FUN_EQ_THM]
  \\ FULL_SIMP_TAC std_ss [] \\ STRIP_TAC
  \\ FULL_SIMP_TAC std_ss [SET_EQ_SUBSET,GSYM SUBSET_INSERT_DELETE,INSERT_SUBSET]
  \\ SIMP_TAC std_ss [SUBSET_DEF,IN_INSERT,IN_DELETE]
  \\ `RANGE (i,j3) i` by RANGE_TAC
  \\ ASM_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11]
  \\ REVERSE (REPEAT STRIP_TAC)
  THEN1 METIS_TAC [heap_element_distinct,ref_mem_def,heap_element_11,PAIR_EQ]
  THEN1
   (FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF,heap_element_11]
    \\ CCONTR_TAC \\ FULL_SIMP_TAC std_ss []
    \\ `RANGE(i+1,i+n+1)x /\ RANGE(b,j)x` by RANGE_TAC \\ RES_TAC
    \\ FULL_SIMP_TAC std_ss [CUT_def,FUN_EQ_THM] \\ METIS_TAC [heap_element_distinct])
  THEN1 (FULL_SIMP_TAC std_ss [heap_element_11] \\ RANGE_TAC)
  THEN1 (FULL_SIMP_TAC std_ss [heap_element_11] \\ RANGE_TAC)
  THEN1 (FULL_SIMP_TAC std_ss [heap_element_11] \\ RANGE_TAC)
  THEN1
   (FULL_SIMP_TAC std_ss [heap_element_11]
    \\ REVERSE (Cases_on `RANGE(i+1,i+n+1)x`) THEN1 RANGE_TAC
    \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF,heap_element_11]
    \\ FULL_SIMP_TAC std_ss [CUT_def,FUN_EQ_THM]
    \\ `m x = H_EMP` by SET_TAC
    \\ `RANGE(b,j)x` by RANGE_TAC \\ RES_TAC
    \\ FULL_SIMP_TAC std_ss [CUT_def,FUN_EQ_THM] \\ METIS_TAC [heap_element_distinct]));

val gc_loop_thm = store_thm("gc_loop_thm",
  ``!j h f m i2 m2.
      gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,D1(CUT(i,j)m)) ==>
      (gc_loop (i,j,m) = (i2,m2)) ==>
        ?h4 f4. gc_inv (h1,roots1,h4,f4) (b,i2,i2,e,b2,e2,m2,{}) /\ j <= i2 /\
                !a. f a <> a ==> (f4 a = f a)``,
  completeInduct_on `e - i` \\ NTAC 4 STRIP_TAC \\ Cases_on `i = j`
  \\ ONCE_REWRITE_TAC [gc_loop_def] \\ ASM_SIMP_TAC std_ss [CUT_EMPTY] THEN1 SET_TAC
  \\ NTAC 6 STRIP_TAC \\ `?i3 j3 m3. gc_step (i,j,m) = (i3,j3,m3)` by METIS_TAC [PAIR]
  \\ FULL_SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC \\ IMP_RES_TAC gc_step_thm
  \\ `(e - i3 < e - i) /\ (e - i3 = e - i3)`  by RANGE_TAC
  \\ RES_TAC \\ IMP_RES_TAC LESS_EQ_TRANS \\ ASM_SIMP_TAC std_ss [] \\ SET_TAC);

val ok_full_heap_def = Define `
  ok_full_heap (h,roots) (b,i,e,b2,e2,m) =
     b <= i /\ i <= e /\ b2 <= e2 /\ (e2 - b2 = e - b) /\ (~(e < b2) ==> e2 < b) /\
     (!k. ~RANGE (b,i) k ==> (m k = H_EMP)) /\
     (?t. part_heap b i m t) /\ ref_mem (h,I) m /\ ok_heap (h,roots)`;

val ok_full_heap_IMP = store_thm("ok_full_heap_IMP",
  ``ok_full_heap (h,roots) (b2,i,e2,b,e,m) ==>
    gc_inv (h,roots,h,I) (b,b,b,e,b2,e2,m,ADDR_SET roots) /\
    ADDR_SET roots SUBSET DR0 (CUT (b2,e2) m)``,
  STRIP_TAC \\ FULL_SIMP_TAC std_ss [gc_inv_def,ok_full_heap_def,full_heap_REFL]
  \\ IMP_RES_TAC ok_heap_IMP \\ REPEAT STRIP_TAC THEN1 RANGE_TAC
  \\ FULL_SIMP_TAC std_ss [CUT_EMPTY]
  THEN1 (Q.PAT_X_ASSUM `!k.bb` MATCH_MP_TAC \\ RANGE_TAC)
  THEN1 (`part_heap i e2 m 0` by
        (MATCH_MP_TAC part_heap_EMP_RANGE \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF]
         \\ REPEAT STRIP_TAC \\ `~RANGE (b2,i) k` by RANGE_TAC \\ RES_TAC)
      \\ IMP_RES_TAC part_heap_TRANS \\ Q.EXISTS_TAC `t` \\ FULL_SIMP_TAC std_ss []
      \\ IMP_RES_TAC part_heap_LENGTH_LESS_EQ)
  \\ SIMP_TAC std_ss [abs_steps_def,RTC_REFL]
  \\ FULL_SIMP_TAC std_ss [ok_heap_def,UNION_SUBSET]
  \\ FULL_SIMP_TAC std_ss [SUBSET_DEF] \\ REPEAT STRIP_TAC \\ RES_TAC
  \\ SIMP_TAC std_ss [DR0,D0,R0,CUT_EQ,IN_DEF] \\ DISJ1_TAC
  \\ `?x1 x2 x3. h ' x = (x1,x2,x3)` by METIS_TAC [PAIR]
  \\ Cases_on `m x` \\ POP_ASSUM MP_TAC
  \\ FULL_SIMP_TAC std_ss [ref_mem_def,heap_element_distinct]
  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [heap_element_11]
  \\ `RANGE (b2,i) x` by METIS_TAC [heap_element_distinct]
  \\ REPEAT STRIP_TAC \\ RANGE_TAC);

val full_heap_IMP_part_heap = store_thm("full_heap_IMP_part_heap",
  ``!b e m. full_heap b e m ==> part_heap b e m (e-b)``,
  HO_MATCH_MP_TAC full_heap_ind \\ REPEAT STRIP_TAC
  THEN1 (SIMP_TAC std_ss [] \\ METIS_TAC [part_heap_cases])
  \\ ONCE_REWRITE_TAC [part_heap_cases] \\ DISJ2_TAC \\ DISJ2_TAC
  \\ ASM_SIMP_TAC std_ss [CUT_EQ,heap_element_11]
  \\ Q.EXISTS_TAC `e - (b + n + 1)` \\ ASM_SIMP_TAC std_ss []
  \\ IMP_RES_TAC full_heap_LESS_EQ \\ DECIDE_TAC);

val gc_thm = store_thm("gc_thm",
  ``ok_full_heap (h,roots) (b2,i,e2,b,e,m) ==>
    (gc (b2,e2,b,e,roots,m) = (b,i2,e,b2,e2,roots2,m2)) ==>
    ?h2. ok_full_heap (h2,roots2) (b,i2,e,b2,e2,m2) /\
         gc_exec (h,roots) (h2,roots2) /\ full_heap b i2 m2``,
  STRIP_TAC \\ IMP_RES_TAC ok_full_heap_IMP
  \\ SIMP_TAC std_ss [gc_def,LET_DEF]
  \\ `?r3 b3 m3. move_list (roots,b,m) = (r3,b3,m3)` by METIS_TAC [PAIR]
  \\ `?i4 m4. gc_loop (b,b3,m3) = (i4,m4)` by METIS_TAC [PAIR]
  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC
  \\ IMP_RES_TAC (RW [UNION_EMPTY] (helperLib.SUBST_INST [``z:num set``|->``{}:num set``] move_list_thm))
  \\ Q.PAT_X_ASSUM `gc_inv (h,roots,h3,f3) ttt` MP_TAC
  \\ REPEAT (Q.PAT_X_ASSUM `gc_inv xxx yyy` (K ALL_TAC)) \\ STRIP_TAC
  \\ IMP_RES_TAC gc_loop_thm
  \\ Q.PAT_X_ASSUM `r3 = ADDR_MAP f3 roots` MP_TAC
  \\ REPEAT (Q.PAT_X_ASSUM `r3 = ADDR_MAP xx roots` (K ALL_TAC)) \\ STRIP_TAC
  \\ FULL_SIMP_TAC std_ss []
  \\ `f3 o f3 = I` by
      (FULL_SIMP_TAC std_ss [gc_inv_def]
       \\ IMP_RES_TAC ok_heap_IMP \\ IMP_RES_TAC abs_steps_thm
       \\ FULL_SIMP_TAC std_ss [abs_gc_inv_def,LET_DEF,gc_inv_def])
  \\ Q.PAT_X_ASSUM `gc_inv (h,roots,h4,f4) ttt` MP_TAC
  \\ REPEAT (Q.PAT_X_ASSUM `gc_inv xxx yyy` (K ALL_TAC))
  \\ SIMP_TAC std_ss [gc_inv_def] \\ REPEAT STRIP_TAC
  \\ Q.EXISTS_TAC `DRESTRICT h4 (D0 (CUT (b,i4) m4))`
  \\ FULL_SIMP_TAC std_ss [CUT_EMPTY] \\ helperLib.CLEAN_TAC
  \\ `gc_exec (h,roots) (DRESTRICT h4 (D0 (CUT (b,i4) m4)),ADDR_MAP f3 roots)` by
      (MATCH_MP_TAC abs_gc_thm \\ ASM_SIMP_TAC std_ss []
       \\ SIMP_TAC std_ss [abs_gc_cases]
       \\ Q.LIST_EXISTS_TAC [`h4`,`f4`,`(D0 (CUT (b,i4) m4))`]
       \\ ASM_SIMP_TAC std_ss [ADDR_MAP_EQ_ADDR_MAP]
       \\ FULL_SIMP_TAC std_ss [SET_TRANSLATE_MAP,SET_TRANSLATE_def]
       \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ SET_TAC)
  \\ IMP_RES_TAC gc_exec_thm \\ ASM_SIMP_TAC std_ss []
  \\ `full_heap b i4 (CUT (b,i4) m4)` by
    (MATCH_MP_TAC full_heap_IGNORE \\ Q.EXISTS_TAC `m4`
     \\ ASM_SIMP_TAC std_ss [CUT_def])
  \\ FULL_SIMP_TAC std_ss [ok_full_heap_def] \\ REPEAT STRIP_TAC
  THEN1 RANGE_TAC THEN1 FULL_SIMP_TAC std_ss [CUT_def,IN_DEF]
  THEN1 METIS_TAC [full_heap_IMP_part_heap,EQ_RANGE_full_heap,EQ_RANGE_CUT]
  \\ FULL_SIMP_TAC std_ss [ref_mem_def,FUN_EQ_THM,FDOM_DRESTRICT,IN_INTER]
  \\ ASM_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ]
  \\ REPEAT STRIP_TAC \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [CUT_def]))
  \\ Cases_on `RANGE (b,i4) a` \\ ASM_SIMP_TAC std_ss [IN_DEF]
  \\ Cases_on `FDOM h4 a` \\ ASM_SIMP_TAC std_ss [IN_DEF] THEN1
     (`?x1 x2 x3. h4 ' a = (x1,x2,x3)` by METIS_TAC [PAIR]
      \\ ASM_SIMP_TAC std_ss [heap_element_11,DRESTRICT_DEF,IN_INTER]
      \\ FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11])
  \\ Cases_on `f4 a = a` \\ ASM_SIMP_TAC std_ss [heap_element_distinct]
  \\ FULL_SIMP_TAC std_ss [abs_gc_inv_def,LET_DEF,NOT_IN_EMPTY,IN_UNION]
  \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM]
  \\ `R0 m4 a` by FULL_SIMP_TAC std_ss [R0,IN_DEF,heap_element_11]
  \\ METIS_TAC [full_heap_R0]);

val _ = export_theory();