From df03890491fc9c549376d26262b0be3707c00f59 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 23 May 2023 14:47:26 +0200
Subject: Add the generated HOL4 files

---
 tests/hol4/hashmap/Holmakefile             |   5 +
 tests/hol4/hashmap/hashmap_FunsScript.sml  | 567 +++++++++++++++++++++++++++++
 tests/hol4/hashmap/hashmap_FunsTheory.sig  | 550 ++++++++++++++++++++++++++++
 tests/hol4/hashmap/hashmap_TypesScript.sml |  24 ++
 tests/hol4/hashmap/hashmap_TypesTheory.sig | 494 +++++++++++++++++++++++++
 5 files changed, 1640 insertions(+)
 create mode 100644 tests/hol4/hashmap/Holmakefile
 create mode 100644 tests/hol4/hashmap/hashmap_FunsScript.sml
 create mode 100644 tests/hol4/hashmap/hashmap_FunsTheory.sig
 create mode 100644 tests/hol4/hashmap/hashmap_TypesScript.sml
 create mode 100644 tests/hol4/hashmap/hashmap_TypesTheory.sig

(limited to 'tests/hol4/hashmap')

diff --git a/tests/hol4/hashmap/Holmakefile b/tests/hol4/hashmap/Holmakefile
new file mode 100644
index 00000000..3c4b8973
--- /dev/null
+++ b/tests/hol4/hashmap/Holmakefile
@@ -0,0 +1,5 @@
+# This file was automatically generated - modify ../Holmakefile.template instead
+INCLUDES =  ../../../backends/hol4
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/tests/hol4/hashmap/hashmap_FunsScript.sml b/tests/hol4/hashmap/hashmap_FunsScript.sml
new file mode 100644
index 00000000..9ad497f5
--- /dev/null
+++ b/tests/hol4/hashmap/hashmap_FunsScript.sml
@@ -0,0 +1,567 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap]: function definitions *)
+open primitivesLib divDefLib
+open hashmap_TypesTheory
+
+val _ = new_theory "hashmap_Funs"
+
+
+val hash_key_fwd_def = Define ‘
+  (** [hashmap::hash_key] *)
+  hash_key_fwd (k : usize) : usize result =
+    Return k
+’
+
+val [hash_map_allocate_slots_loop_fwd_def] = DefineDiv ‘
+  (** [hashmap::HashMap::{0}::allocate_slots] *)
+  hash_map_allocate_slots_loop_fwd
+    (slots : 't list_t vec) (n : usize) : 't list_t vec result =
+    if usize_gt n (int_to_usize 0)
+    then (
+      do
+      slots0 <- vec_push_back slots ListNil;
+      n0 <- usize_sub n (int_to_usize 1);
+      hash_map_allocate_slots_loop_fwd slots0 n0
+      od)
+    else Return slots
+’
+
+val hash_map_allocate_slots_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::allocate_slots] *)
+  hash_map_allocate_slots_fwd
+    (slots : 't list_t vec) (n : usize) : 't list_t vec result =
+    hash_map_allocate_slots_loop_fwd slots n
+’
+
+val hash_map_new_with_capacity_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::new_with_capacity] *)
+  hash_map_new_with_capacity_fwd
+    (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) :
+    't hash_map_t result
+    =
+    let v = vec_new in
+    do
+    slots <- hash_map_allocate_slots_fwd v capacity;
+    i <- usize_mul capacity max_load_dividend;
+    i0 <- usize_div i max_load_divisor;
+    Return
+      (<|
+         hash_map_num_entries := (int_to_usize 0);
+         hash_map_max_load_factor := (max_load_dividend, max_load_divisor);
+         hash_map_max_load := i0;
+         hash_map_slots := slots
+         |>)
+    od
+’
+
+val hash_map_new_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::new] *)
+  hash_map_new_fwd : 't hash_map_t result =
+    hash_map_new_with_capacity_fwd (int_to_usize 32) (int_to_usize 4)
+      (int_to_usize 5)
+’
+
+val [hash_map_clear_loop_fwd_back_def] = DefineDiv ‘
+  (** [hashmap::HashMap::{0}::clear] *)
+  hash_map_clear_loop_fwd_back
+    (slots : 't list_t vec) (i : usize) : 't list_t vec result =
+    let i0 = vec_len slots in
+    if usize_lt i i0
+    then (
+      do
+      i1 <- usize_add i (int_to_usize 1);
+      slots0 <- vec_index_mut_back slots i ListNil;
+      hash_map_clear_loop_fwd_back slots0 i1
+      od)
+    else Return slots
+’
+
+val hash_map_clear_fwd_back_def = Define ‘
+  (** [hashmap::HashMap::{0}::clear] *)
+  hash_map_clear_fwd_back (self : 't hash_map_t) : 't hash_map_t result =
+    do
+    v <- hash_map_clear_loop_fwd_back self.hash_map_slots (int_to_usize 0);
+    Return
+      (self
+         with
+         <|
+         hash_map_num_entries := (int_to_usize 0); hash_map_slots := v
+         |>)
+    od
+’
+
+val hash_map_len_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::len] *)
+  hash_map_len_fwd (self : 't hash_map_t) : usize result =
+    Return self.hash_map_num_entries
+’
+
+val [hash_map_insert_in_list_loop_fwd_def] = DefineDiv ‘
+  (** [hashmap::HashMap::{0}::insert_in_list] *)
+  hash_map_insert_in_list_loop_fwd
+    (key : usize) (value : 't) (ls : 't list_t) : bool result =
+    (case ls of
+    | ListCons ckey cvalue tl =>
+      if ckey = key
+      then Return F
+      else hash_map_insert_in_list_loop_fwd key value tl
+    | ListNil => Return T)
+’
+
+val hash_map_insert_in_list_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::insert_in_list] *)
+  hash_map_insert_in_list_fwd
+    (key : usize) (value : 't) (ls : 't list_t) : bool result =
+    hash_map_insert_in_list_loop_fwd key value ls
+’
+
+val [hash_map_insert_in_list_loop_back_def] = DefineDiv ‘
+  (** [hashmap::HashMap::{0}::insert_in_list] *)
+  hash_map_insert_in_list_loop_back
+    (key : usize) (value : 't) (ls : 't list_t) : 't list_t result =
+    (case ls of
+    | ListCons ckey cvalue tl =>
+      if ckey = key
+      then Return (ListCons ckey value tl)
+      else (
+        do
+        tl0 <- hash_map_insert_in_list_loop_back key value tl;
+        Return (ListCons ckey cvalue tl0)
+        od)
+    | ListNil => let l = ListNil in Return (ListCons key value l))
+’
+
+val hash_map_insert_in_list_back_def = Define ‘
+  (** [hashmap::HashMap::{0}::insert_in_list] *)
+  hash_map_insert_in_list_back
+    (key : usize) (value : 't) (ls : 't list_t) : 't list_t result =
+    hash_map_insert_in_list_loop_back key value ls
+’
+
+val hash_map_insert_no_resize_fwd_back_def = Define ‘
+  (** [hashmap::HashMap::{0}::insert_no_resize] *)
+  hash_map_insert_no_resize_fwd_back
+    (self : 't hash_map_t) (key : usize) (value : 't) : 't hash_map_t result =
+    do
+    hash <- hash_key_fwd key;
+    let i = vec_len self.hash_map_slots in
+    do
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+    inserted <- hash_map_insert_in_list_fwd key value l;
+    if inserted
+    then (
+      do
+      i0 <- usize_add self.hash_map_num_entries (int_to_usize 1);
+      l0 <- hash_map_insert_in_list_back key value l;
+      v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+      Return (self with <| hash_map_num_entries := i0; hash_map_slots := v |>)
+      od)
+    else (
+      do
+      l0 <- hash_map_insert_in_list_back key value l;
+      v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+      Return (self with <| hash_map_slots := v |>)
+      od)
+    od
+    od
+’
+
+(** [core::num::u32::{9}::MAX] *)
+Definition core_num_u32_max_body_def:
+  core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
+End
+Definition core_num_u32_max_c_def:
+  core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
+End
+
+val [hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘
+  (** [hashmap::HashMap::{0}::move_elements_from_list] *)
+  hash_map_move_elements_from_list_loop_fwd_back
+    (ntable : 't hash_map_t) (ls : 't list_t) : 't hash_map_t result =
+    (case ls of
+    | ListCons k v tl =>
+      do
+      ntable0 <- hash_map_insert_no_resize_fwd_back ntable k v;
+      hash_map_move_elements_from_list_loop_fwd_back ntable0 tl
+      od
+    | ListNil => Return ntable)
+’
+
+val hash_map_move_elements_from_list_fwd_back_def = Define ‘
+  (** [hashmap::HashMap::{0}::move_elements_from_list] *)
+  hash_map_move_elements_from_list_fwd_back
+    (ntable : 't hash_map_t) (ls : 't list_t) : 't hash_map_t result =
+    hash_map_move_elements_from_list_loop_fwd_back ntable ls
+’
+
+val [hash_map_move_elements_loop_fwd_back_def] = DefineDiv ‘
+  (** [hashmap::HashMap::{0}::move_elements] *)
+  hash_map_move_elements_loop_fwd_back
+    (ntable : 't hash_map_t) (slots : 't list_t vec) (i : usize) :
+    ('t hash_map_t # 't list_t vec) result
+    =
+    let i0 = vec_len slots in
+    if usize_lt i i0
+    then (
+      do
+      l <- vec_index_mut_fwd slots i;
+      let ls = mem_replace_fwd l ListNil in
+      do
+      ntable0 <- hash_map_move_elements_from_list_fwd_back ntable ls;
+      i1 <- usize_add i (int_to_usize 1);
+      let l0 = mem_replace_back l ListNil in
+      do
+      slots0 <- vec_index_mut_back slots i l0;
+      hash_map_move_elements_loop_fwd_back ntable0 slots0 i1
+      od
+      od
+      od)
+    else Return (ntable, slots)
+’
+
+val hash_map_move_elements_fwd_back_def = Define ‘
+  (** [hashmap::HashMap::{0}::move_elements] *)
+  hash_map_move_elements_fwd_back
+    (ntable : 't hash_map_t) (slots : 't list_t vec) (i : usize) :
+    ('t hash_map_t # 't list_t vec) result
+    =
+    hash_map_move_elements_loop_fwd_back ntable slots i
+’
+
+val hash_map_try_resize_fwd_back_def = Define ‘
+  (** [hashmap::HashMap::{0}::try_resize] *)
+  hash_map_try_resize_fwd_back (self : 't hash_map_t) : 't hash_map_t result =
+    do
+    max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+    let capacity = vec_len self.hash_map_slots in
+    do
+    n1 <- usize_div max_usize (int_to_usize 2);
+    let (i, i0) = self.hash_map_max_load_factor in
+    do
+    i1 <- usize_div n1 i;
+    if usize_le capacity i1
+    then (
+      do
+      i2 <- usize_mul capacity (int_to_usize 2);
+      ntable <- hash_map_new_with_capacity_fwd i2 i i0;
+      (ntable0, _) <-
+        hash_map_move_elements_fwd_back ntable self.hash_map_slots
+          (int_to_usize 0);
+      Return
+        (ntable0
+           with
+           <|
+           hash_map_num_entries := self.hash_map_num_entries;
+           hash_map_max_load_factor := (i, i0)
+           |>)
+      od)
+    else Return (self with <| hash_map_max_load_factor := (i, i0) |>)
+    od
+    od
+    od
+’
+
+val hash_map_insert_fwd_back_def = Define ‘
+  (** [hashmap::HashMap::{0}::insert] *)
+  hash_map_insert_fwd_back
+    (self : 't hash_map_t) (key : usize) (value : 't) : 't hash_map_t result =
+    do
+    self0 <- hash_map_insert_no_resize_fwd_back self key value;
+    i <- hash_map_len_fwd self0;
+    if usize_gt i self0.hash_map_max_load
+    then hash_map_try_resize_fwd_back self0
+    else Return self0
+    od
+’
+
+val [hash_map_contains_key_in_list_loop_fwd_def] = DefineDiv ‘
+  (** [hashmap::HashMap::{0}::contains_key_in_list] *)
+  hash_map_contains_key_in_list_loop_fwd
+    (key : usize) (ls : 't list_t) : bool result =
+    (case ls of
+    | ListCons ckey t tl =>
+      if ckey = key
+      then Return T
+      else hash_map_contains_key_in_list_loop_fwd key tl
+    | ListNil => Return F)
+’
+
+val hash_map_contains_key_in_list_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::contains_key_in_list] *)
+  hash_map_contains_key_in_list_fwd
+    (key : usize) (ls : 't list_t) : bool result =
+    hash_map_contains_key_in_list_loop_fwd key ls
+’
+
+val hash_map_contains_key_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::contains_key] *)
+  hash_map_contains_key_fwd
+    (self : 't hash_map_t) (key : usize) : bool result =
+    do
+    hash <- hash_key_fwd key;
+    let i = vec_len self.hash_map_slots in
+    do
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_fwd self.hash_map_slots hash_mod;
+    hash_map_contains_key_in_list_fwd key l
+    od
+    od
+’
+
+val [hash_map_get_in_list_loop_fwd_def] = DefineDiv ‘
+  (** [hashmap::HashMap::{0}::get_in_list] *)
+  hash_map_get_in_list_loop_fwd (key : usize) (ls : 't list_t) : 't result =
+    (case ls of
+    | ListCons ckey cvalue tl =>
+      if ckey = key
+      then Return cvalue
+      else hash_map_get_in_list_loop_fwd key tl
+    | ListNil => Fail Failure)
+’
+
+val hash_map_get_in_list_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::get_in_list] *)
+  hash_map_get_in_list_fwd (key : usize) (ls : 't list_t) : 't result =
+    hash_map_get_in_list_loop_fwd key ls
+’
+
+val hash_map_get_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::get] *)
+  hash_map_get_fwd (self : 't hash_map_t) (key : usize) : 't result =
+    do
+    hash <- hash_key_fwd key;
+    let i = vec_len self.hash_map_slots in
+    do
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_fwd self.hash_map_slots hash_mod;
+    hash_map_get_in_list_fwd key l
+    od
+    od
+’
+
+val [hash_map_get_mut_in_list_loop_fwd_def] = DefineDiv ‘
+  (** [hashmap::HashMap::{0}::get_mut_in_list] *)
+  hash_map_get_mut_in_list_loop_fwd
+    (ls : 't list_t) (key : usize) : 't result =
+    (case ls of
+    | ListCons ckey cvalue tl =>
+      if ckey = key
+      then Return cvalue
+      else hash_map_get_mut_in_list_loop_fwd tl key
+    | ListNil => Fail Failure)
+’
+
+val hash_map_get_mut_in_list_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::get_mut_in_list] *)
+  hash_map_get_mut_in_list_fwd (ls : 't list_t) (key : usize) : 't result =
+    hash_map_get_mut_in_list_loop_fwd ls key
+’
+
+val [hash_map_get_mut_in_list_loop_back_def] = DefineDiv ‘
+  (** [hashmap::HashMap::{0}::get_mut_in_list] *)
+  hash_map_get_mut_in_list_loop_back
+    (ls : 't list_t) (key : usize) (ret : 't) : 't list_t result =
+    (case ls of
+    | ListCons ckey cvalue tl =>
+      if ckey = key
+      then Return (ListCons ckey ret tl)
+      else (
+        do
+        tl0 <- hash_map_get_mut_in_list_loop_back tl key ret;
+        Return (ListCons ckey cvalue tl0)
+        od)
+    | ListNil => Fail Failure)
+’
+
+val hash_map_get_mut_in_list_back_def = Define ‘
+  (** [hashmap::HashMap::{0}::get_mut_in_list] *)
+  hash_map_get_mut_in_list_back
+    (ls : 't list_t) (key : usize) (ret : 't) : 't list_t result =
+    hash_map_get_mut_in_list_loop_back ls key ret
+’
+
+val hash_map_get_mut_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::get_mut] *)
+  hash_map_get_mut_fwd (self : 't hash_map_t) (key : usize) : 't result =
+    do
+    hash <- hash_key_fwd key;
+    let i = vec_len self.hash_map_slots in
+    do
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+    hash_map_get_mut_in_list_fwd l key
+    od
+    od
+’
+
+val hash_map_get_mut_back_def = Define ‘
+  (** [hashmap::HashMap::{0}::get_mut] *)
+  hash_map_get_mut_back
+    (self : 't hash_map_t) (key : usize) (ret : 't) : 't hash_map_t result =
+    do
+    hash <- hash_key_fwd key;
+    let i = vec_len self.hash_map_slots in
+    do
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+    l0 <- hash_map_get_mut_in_list_back l key ret;
+    v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+    Return (self with <| hash_map_slots := v |>)
+    od
+    od
+’
+
+val [hash_map_remove_from_list_loop_fwd_def] = DefineDiv ‘
+  (** [hashmap::HashMap::{0}::remove_from_list] *)
+  hash_map_remove_from_list_loop_fwd
+    (key : usize) (ls : 't list_t) : 't option result =
+    (case ls of
+    | ListCons ckey t tl =>
+      if ckey = key
+      then
+        let mv_ls = mem_replace_fwd (ListCons ckey t tl) ListNil in
+        (case mv_ls of
+        | ListCons i cvalue tl0 => Return (SOME cvalue)
+        | ListNil => Fail Failure)
+      else hash_map_remove_from_list_loop_fwd key tl
+    | ListNil => Return NONE)
+’
+
+val hash_map_remove_from_list_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::remove_from_list] *)
+  hash_map_remove_from_list_fwd
+    (key : usize) (ls : 't list_t) : 't option result =
+    hash_map_remove_from_list_loop_fwd key ls
+’
+
+val [hash_map_remove_from_list_loop_back_def] = DefineDiv ‘
+  (** [hashmap::HashMap::{0}::remove_from_list] *)
+  hash_map_remove_from_list_loop_back
+    (key : usize) (ls : 't list_t) : 't list_t result =
+    (case ls of
+    | ListCons ckey t tl =>
+      if ckey = key
+      then
+        let mv_ls = mem_replace_fwd (ListCons ckey t tl) ListNil in
+        (case mv_ls of
+        | ListCons i cvalue tl0 => Return tl0
+        | ListNil => Fail Failure)
+      else (
+        do
+        tl0 <- hash_map_remove_from_list_loop_back key tl;
+        Return (ListCons ckey t tl0)
+        od)
+    | ListNil => Return ListNil)
+’
+
+val hash_map_remove_from_list_back_def = Define ‘
+  (** [hashmap::HashMap::{0}::remove_from_list] *)
+  hash_map_remove_from_list_back
+    (key : usize) (ls : 't list_t) : 't list_t result =
+    hash_map_remove_from_list_loop_back key ls
+’
+
+val hash_map_remove_fwd_def = Define ‘
+  (** [hashmap::HashMap::{0}::remove] *)
+  hash_map_remove_fwd (self : 't hash_map_t) (key : usize) : 't option result =
+    do
+    hash <- hash_key_fwd key;
+    let i = vec_len self.hash_map_slots in
+    do
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+    x <- hash_map_remove_from_list_fwd key l;
+    (case x of
+    | NONE => Return NONE
+    | SOME x0 =>
+      do
+      _ <- usize_sub self.hash_map_num_entries (int_to_usize 1);
+      Return (SOME x0)
+      od)
+    od
+    od
+’
+
+val hash_map_remove_back_def = Define ‘
+  (** [hashmap::HashMap::{0}::remove] *)
+  hash_map_remove_back
+    (self : 't hash_map_t) (key : usize) : 't hash_map_t result =
+    do
+    hash <- hash_key_fwd key;
+    let i = vec_len self.hash_map_slots in
+    do
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+    x <- hash_map_remove_from_list_fwd key l;
+    (case x of
+    | NONE =>
+      do
+      l0 <- hash_map_remove_from_list_back key l;
+      v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+      Return (self with <| hash_map_slots := v |>)
+      od
+    | SOME x0 =>
+      do
+      i0 <- usize_sub self.hash_map_num_entries (int_to_usize 1);
+      l0 <- hash_map_remove_from_list_back key l;
+      v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+      Return (self with <| hash_map_num_entries := i0; hash_map_slots := v |>)
+      od)
+    od
+    od
+’
+
+val test1_fwd_def = Define ‘
+  (** [hashmap::test1] *)
+  test1_fwd : unit result =
+    do
+    hm <- hash_map_new_fwd;
+    hm0 <- hash_map_insert_fwd_back hm (int_to_usize 0) (int_to_u64 42);
+    hm1 <- hash_map_insert_fwd_back hm0 (int_to_usize 128) (int_to_u64 18);
+    hm2 <- hash_map_insert_fwd_back hm1 (int_to_usize 1024) (int_to_u64 138);
+    hm3 <- hash_map_insert_fwd_back hm2 (int_to_usize 1056) (int_to_u64 256);
+    i <- hash_map_get_fwd hm3 (int_to_usize 128);
+    if ~ (i = int_to_u64 18)
+    then Fail Failure
+    else (
+      do
+      hm4 <- hash_map_get_mut_back hm3 (int_to_usize 1024) (int_to_u64 56);
+      i0 <- hash_map_get_fwd hm4 (int_to_usize 1024);
+      if ~ (i0 = int_to_u64 56)
+      then Fail Failure
+      else (
+        do
+        x <- hash_map_remove_fwd hm4 (int_to_usize 1024);
+        (case x of
+        | NONE => Fail Failure
+        | SOME x0 =>
+          if ~ (x0 = int_to_u64 56)
+          then Fail Failure
+          else (
+            do
+            hm5 <- hash_map_remove_back hm4 (int_to_usize 1024);
+            i1 <- hash_map_get_fwd hm5 (int_to_usize 0);
+            if ~ (i1 = int_to_u64 42)
+            then Fail Failure
+            else (
+              do
+              i2 <- hash_map_get_fwd hm5 (int_to_usize 128);
+              if ~ (i2 = int_to_u64 18)
+              then Fail Failure
+              else (
+                do
+                i3 <- hash_map_get_fwd hm5 (int_to_usize 1056);
+                if ~ (i3 = int_to_u64 256) then Fail Failure else Return ()
+                od)
+              od)
+            od))
+        od)
+      od)
+    od
+’
+
+(** Unit test for [hashmap::test1] *)
+val _ = assert_return (“test1_fwd”)
+
+val _ = export_theory ()
diff --git a/tests/hol4/hashmap/hashmap_FunsTheory.sig b/tests/hol4/hashmap/hashmap_FunsTheory.sig
new file mode 100644
index 00000000..50482547
--- /dev/null
+++ b/tests/hol4/hashmap/hashmap_FunsTheory.sig
@@ -0,0 +1,550 @@
+signature hashmap_FunsTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val core_num_u32_max_body_def : thm
+    val core_num_u32_max_c_def : thm
+    val hash_key_fwd_def : thm
+    val hash_map_allocate_slots_fwd_def : thm
+    val hash_map_allocate_slots_loop_fwd_def : thm
+    val hash_map_clear_fwd_back_def : thm
+    val hash_map_clear_loop_fwd_back_def : thm
+    val hash_map_contains_key_fwd_def : thm
+    val hash_map_contains_key_in_list_fwd_def : thm
+    val hash_map_contains_key_in_list_loop_fwd_def : thm
+    val hash_map_get_fwd_def : thm
+    val hash_map_get_in_list_fwd_def : thm
+    val hash_map_get_in_list_loop_fwd_def : thm
+    val hash_map_get_mut_back_def : thm
+    val hash_map_get_mut_fwd_def : thm
+    val hash_map_get_mut_in_list_back_def : thm
+    val hash_map_get_mut_in_list_fwd_def : thm
+    val hash_map_get_mut_in_list_loop_back_def : thm
+    val hash_map_get_mut_in_list_loop_fwd_def : thm
+    val hash_map_insert_fwd_back_def : thm
+    val hash_map_insert_in_list_back_def : thm
+    val hash_map_insert_in_list_fwd_def : thm
+    val hash_map_insert_in_list_loop_back_def : thm
+    val hash_map_insert_in_list_loop_fwd_def : thm
+    val hash_map_insert_no_resize_fwd_back_def : thm
+    val hash_map_len_fwd_def : thm
+    val hash_map_move_elements_from_list_fwd_back_def : thm
+    val hash_map_move_elements_from_list_loop_fwd_back_def : thm
+    val hash_map_move_elements_fwd_back_def : thm
+    val hash_map_move_elements_loop_fwd_back_def : thm
+    val hash_map_new_fwd_def : thm
+    val hash_map_new_with_capacity_fwd_def : thm
+    val hash_map_remove_back_def : thm
+    val hash_map_remove_from_list_back_def : thm
+    val hash_map_remove_from_list_fwd_def : thm
+    val hash_map_remove_from_list_loop_back_def : thm
+    val hash_map_remove_from_list_loop_fwd_def : thm
+    val hash_map_remove_fwd_def : thm
+    val hash_map_try_resize_fwd_back_def : thm
+    val test1_fwd_def : thm
+  
+  val hashmap_Funs_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [hashmap_Types] Parent theory of "hashmap_Funs"
+   
+   [core_num_u32_max_body_def]  Definition
+      
+      ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
+   
+   [core_num_u32_max_c_def]  Definition
+      
+      ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
+   
+   [hash_key_fwd_def]  Definition
+      
+      ⊢ ∀k. hash_key_fwd k = Return k
+   
+   [hash_map_allocate_slots_fwd_def]  Definition
+      
+      ⊢ ∀slots n.
+          hash_map_allocate_slots_fwd slots n =
+          hash_map_allocate_slots_loop_fwd slots n
+   
+   [hash_map_allocate_slots_loop_fwd_def]  Definition
+      
+      ⊢ ∀slots n.
+          hash_map_allocate_slots_loop_fwd slots n =
+          if usize_gt n (int_to_usize 0) then
+            do
+              slots0 <- vec_push_back slots ListNil;
+              n0 <- usize_sub n (int_to_usize 1);
+              hash_map_allocate_slots_loop_fwd slots0 n0
+            od
+          else Return slots
+   
+   [hash_map_clear_fwd_back_def]  Definition
+      
+      ⊢ ∀self.
+          hash_map_clear_fwd_back self =
+          do
+            v <-
+              hash_map_clear_loop_fwd_back self.hash_map_slots
+                (int_to_usize 0);
+            Return
+              (self with
+               <|hash_map_num_entries := int_to_usize 0;
+                 hash_map_slots := v|>)
+          od
+   
+   [hash_map_clear_loop_fwd_back_def]  Definition
+      
+      ⊢ ∀slots i.
+          hash_map_clear_loop_fwd_back slots i =
+          (let
+             i0 = vec_len slots
+           in
+             if usize_lt i i0 then
+               do
+                 i1 <- usize_add i (int_to_usize 1);
+                 slots0 <- vec_index_mut_back slots i ListNil;
+                 hash_map_clear_loop_fwd_back slots0 i1
+               od
+             else Return slots)
+   
+   [hash_map_contains_key_fwd_def]  Definition
+      
+      ⊢ ∀self key.
+          hash_map_contains_key_fwd self key =
+          do
+            hash <- hash_key_fwd key;
+            i <<- vec_len self.hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_fwd self.hash_map_slots hash_mod;
+            hash_map_contains_key_in_list_fwd key l
+          od
+   
+   [hash_map_contains_key_in_list_fwd_def]  Definition
+      
+      ⊢ ∀key ls.
+          hash_map_contains_key_in_list_fwd key ls =
+          hash_map_contains_key_in_list_loop_fwd key ls
+   
+   [hash_map_contains_key_in_list_loop_fwd_def]  Definition
+      
+      ⊢ ∀key ls.
+          hash_map_contains_key_in_list_loop_fwd key ls =
+          case ls of
+            ListCons ckey t tl =>
+              if ckey = key then Return T
+              else hash_map_contains_key_in_list_loop_fwd key tl
+          | ListNil => Return F
+   
+   [hash_map_get_fwd_def]  Definition
+      
+      ⊢ ∀self key.
+          hash_map_get_fwd self key =
+          do
+            hash <- hash_key_fwd key;
+            i <<- vec_len self.hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_fwd self.hash_map_slots hash_mod;
+            hash_map_get_in_list_fwd key l
+          od
+   
+   [hash_map_get_in_list_fwd_def]  Definition
+      
+      ⊢ ∀key ls.
+          hash_map_get_in_list_fwd key ls =
+          hash_map_get_in_list_loop_fwd key ls
+   
+   [hash_map_get_in_list_loop_fwd_def]  Definition
+      
+      ⊢ ∀key ls.
+          hash_map_get_in_list_loop_fwd key ls =
+          case ls of
+            ListCons ckey cvalue tl =>
+              if ckey = key then Return cvalue
+              else hash_map_get_in_list_loop_fwd key tl
+          | ListNil => Fail Failure
+   
+   [hash_map_get_mut_back_def]  Definition
+      
+      ⊢ ∀self key ret.
+          hash_map_get_mut_back self key ret =
+          do
+            hash <- hash_key_fwd key;
+            i <<- vec_len self.hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+            l0 <- hash_map_get_mut_in_list_back l key ret;
+            v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+            Return (self with hash_map_slots := v)
+          od
+   
+   [hash_map_get_mut_fwd_def]  Definition
+      
+      ⊢ ∀self key.
+          hash_map_get_mut_fwd self key =
+          do
+            hash <- hash_key_fwd key;
+            i <<- vec_len self.hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+            hash_map_get_mut_in_list_fwd l key
+          od
+   
+   [hash_map_get_mut_in_list_back_def]  Definition
+      
+      ⊢ ∀ls key ret.
+          hash_map_get_mut_in_list_back ls key ret =
+          hash_map_get_mut_in_list_loop_back ls key ret
+   
+   [hash_map_get_mut_in_list_fwd_def]  Definition
+      
+      ⊢ ∀ls key.
+          hash_map_get_mut_in_list_fwd ls key =
+          hash_map_get_mut_in_list_loop_fwd ls key
+   
+   [hash_map_get_mut_in_list_loop_back_def]  Definition
+      
+      ⊢ ∀ls key ret.
+          hash_map_get_mut_in_list_loop_back ls key ret =
+          case ls of
+            ListCons ckey cvalue tl =>
+              if ckey = key then Return (ListCons ckey ret tl)
+              else
+                do
+                  tl0 <- hash_map_get_mut_in_list_loop_back tl key ret;
+                  Return (ListCons ckey cvalue tl0)
+                od
+          | ListNil => Fail Failure
+   
+   [hash_map_get_mut_in_list_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls key.
+          hash_map_get_mut_in_list_loop_fwd ls key =
+          case ls of
+            ListCons ckey cvalue tl =>
+              if ckey = key then Return cvalue
+              else hash_map_get_mut_in_list_loop_fwd tl key
+          | ListNil => Fail Failure
+   
+   [hash_map_insert_fwd_back_def]  Definition
+      
+      ⊢ ∀self key value.
+          hash_map_insert_fwd_back self key value =
+          do
+            self0 <- hash_map_insert_no_resize_fwd_back self key value;
+            i <- hash_map_len_fwd self0;
+            if usize_gt i self0.hash_map_max_load then
+              hash_map_try_resize_fwd_back self0
+            else Return self0
+          od
+   
+   [hash_map_insert_in_list_back_def]  Definition
+      
+      ⊢ ∀key value ls.
+          hash_map_insert_in_list_back key value ls =
+          hash_map_insert_in_list_loop_back key value ls
+   
+   [hash_map_insert_in_list_fwd_def]  Definition
+      
+      ⊢ ∀key value ls.
+          hash_map_insert_in_list_fwd key value ls =
+          hash_map_insert_in_list_loop_fwd key value ls
+   
+   [hash_map_insert_in_list_loop_back_def]  Definition
+      
+      ⊢ ∀key value ls.
+          hash_map_insert_in_list_loop_back key value ls =
+          case ls of
+            ListCons ckey cvalue tl =>
+              if ckey = key then Return (ListCons ckey value tl)
+              else
+                do
+                  tl0 <- hash_map_insert_in_list_loop_back key value tl;
+                  Return (ListCons ckey cvalue tl0)
+                od
+          | ListNil => (let l = ListNil in Return (ListCons key value l))
+   
+   [hash_map_insert_in_list_loop_fwd_def]  Definition
+      
+      ⊢ ∀key value ls.
+          hash_map_insert_in_list_loop_fwd key value ls =
+          case ls of
+            ListCons ckey cvalue tl =>
+              if ckey = key then Return F
+              else hash_map_insert_in_list_loop_fwd key value tl
+          | ListNil => Return T
+   
+   [hash_map_insert_no_resize_fwd_back_def]  Definition
+      
+      ⊢ ∀self key value.
+          hash_map_insert_no_resize_fwd_back self key value =
+          do
+            hash <- hash_key_fwd key;
+            i <<- vec_len self.hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+            inserted <- hash_map_insert_in_list_fwd key value l;
+            if inserted then
+              do
+                i0 <- usize_add self.hash_map_num_entries (int_to_usize 1);
+                l0 <- hash_map_insert_in_list_back key value l;
+                v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+                Return
+                  (self with
+                   <|hash_map_num_entries := i0; hash_map_slots := v|>)
+              od
+            else
+              do
+                l0 <- hash_map_insert_in_list_back key value l;
+                v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+                Return (self with hash_map_slots := v)
+              od
+          od
+   
+   [hash_map_len_fwd_def]  Definition
+      
+      ⊢ ∀self. hash_map_len_fwd self = Return self.hash_map_num_entries
+   
+   [hash_map_move_elements_from_list_fwd_back_def]  Definition
+      
+      ⊢ ∀ntable ls.
+          hash_map_move_elements_from_list_fwd_back ntable ls =
+          hash_map_move_elements_from_list_loop_fwd_back ntable ls
+   
+   [hash_map_move_elements_from_list_loop_fwd_back_def]  Definition
+      
+      ⊢ ∀ntable ls.
+          hash_map_move_elements_from_list_loop_fwd_back ntable ls =
+          case ls of
+            ListCons k v tl =>
+              do
+                ntable0 <- hash_map_insert_no_resize_fwd_back ntable k v;
+                hash_map_move_elements_from_list_loop_fwd_back ntable0 tl
+              od
+          | ListNil => Return ntable
+   
+   [hash_map_move_elements_fwd_back_def]  Definition
+      
+      ⊢ ∀ntable slots i.
+          hash_map_move_elements_fwd_back ntable slots i =
+          hash_map_move_elements_loop_fwd_back ntable slots i
+   
+   [hash_map_move_elements_loop_fwd_back_def]  Definition
+      
+      ⊢ ∀ntable slots i.
+          hash_map_move_elements_loop_fwd_back ntable slots i =
+          (let
+             i0 = vec_len slots
+           in
+             if usize_lt i i0 then
+               do
+                 l <- vec_index_mut_fwd slots i;
+                 ls <<- mem_replace_fwd l ListNil;
+                 ntable0 <-
+                   hash_map_move_elements_from_list_fwd_back ntable ls;
+                 i1 <- usize_add i (int_to_usize 1);
+                 l0 <<- mem_replace_back l ListNil;
+                 slots0 <- vec_index_mut_back slots i l0;
+                 hash_map_move_elements_loop_fwd_back ntable0 slots0 i1
+               od
+             else Return (ntable,slots))
+   
+   [hash_map_new_fwd_def]  Definition
+      
+      ⊢ hash_map_new_fwd =
+        hash_map_new_with_capacity_fwd (int_to_usize 32) (int_to_usize 4)
+          (int_to_usize 5)
+   
+   [hash_map_new_with_capacity_fwd_def]  Definition
+      
+      ⊢ ∀capacity max_load_dividend max_load_divisor.
+          hash_map_new_with_capacity_fwd capacity max_load_dividend
+            max_load_divisor =
+          (let
+             v = vec_new
+           in
+             do
+               slots <- hash_map_allocate_slots_fwd v capacity;
+               i <- usize_mul capacity max_load_dividend;
+               i0 <- usize_div i max_load_divisor;
+               Return
+                 <|hash_map_num_entries := int_to_usize 0;
+                   hash_map_max_load_factor :=
+                     (max_load_dividend,max_load_divisor);
+                   hash_map_max_load := i0; hash_map_slots := slots|>
+             od)
+   
+   [hash_map_remove_back_def]  Definition
+      
+      ⊢ ∀self key.
+          hash_map_remove_back self key =
+          do
+            hash <- hash_key_fwd key;
+            i <<- vec_len self.hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+            x <- hash_map_remove_from_list_fwd key l;
+            case x of
+              NONE =>
+                do
+                  l0 <- hash_map_remove_from_list_back key l;
+                  v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+                  Return (self with hash_map_slots := v)
+                od
+            | SOME x0 =>
+              do
+                i0 <- usize_sub self.hash_map_num_entries (int_to_usize 1);
+                l0 <- hash_map_remove_from_list_back key l;
+                v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+                Return
+                  (self with
+                   <|hash_map_num_entries := i0; hash_map_slots := v|>)
+              od
+          od
+   
+   [hash_map_remove_from_list_back_def]  Definition
+      
+      ⊢ ∀key ls.
+          hash_map_remove_from_list_back key ls =
+          hash_map_remove_from_list_loop_back key ls
+   
+   [hash_map_remove_from_list_fwd_def]  Definition
+      
+      ⊢ ∀key ls.
+          hash_map_remove_from_list_fwd key ls =
+          hash_map_remove_from_list_loop_fwd key ls
+   
+   [hash_map_remove_from_list_loop_back_def]  Definition
+      
+      ⊢ ∀key ls.
+          hash_map_remove_from_list_loop_back key ls =
+          case ls of
+            ListCons ckey t tl =>
+              if ckey = key then
+                (let
+                   mv_ls = mem_replace_fwd (ListCons ckey t tl) ListNil
+                 in
+                   case mv_ls of
+                     ListCons i cvalue tl0 => Return tl0
+                   | ListNil => Fail Failure)
+              else
+                do
+                  tl0 <- hash_map_remove_from_list_loop_back key tl;
+                  Return (ListCons ckey t tl0)
+                od
+          | ListNil => Return ListNil
+   
+   [hash_map_remove_from_list_loop_fwd_def]  Definition
+      
+      ⊢ ∀key ls.
+          hash_map_remove_from_list_loop_fwd key ls =
+          case ls of
+            ListCons ckey t tl =>
+              if ckey = key then
+                (let
+                   mv_ls = mem_replace_fwd (ListCons ckey t tl) ListNil
+                 in
+                   case mv_ls of
+                     ListCons i cvalue tl0 => Return (SOME cvalue)
+                   | ListNil => Fail Failure)
+              else hash_map_remove_from_list_loop_fwd key tl
+          | ListNil => Return NONE
+   
+   [hash_map_remove_fwd_def]  Definition
+      
+      ⊢ ∀self key.
+          hash_map_remove_fwd self key =
+          do
+            hash <- hash_key_fwd key;
+            i <<- vec_len self.hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+            x <- hash_map_remove_from_list_fwd key l;
+            case x of
+              NONE => Return NONE
+            | SOME x0 =>
+              monad_ignore_bind
+                (usize_sub self.hash_map_num_entries (int_to_usize 1))
+                (Return (SOME x0))
+          od
+   
+   [hash_map_try_resize_fwd_back_def]  Definition
+      
+      ⊢ ∀self.
+          hash_map_try_resize_fwd_back self =
+          do
+            max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+            capacity <<- vec_len self.hash_map_slots;
+            n1 <- usize_div max_usize (int_to_usize 2);
+            (i,i0) <<- self.hash_map_max_load_factor;
+            i1 <- usize_div n1 i;
+            if usize_le capacity i1 then
+              do
+                i2 <- usize_mul capacity (int_to_usize 2);
+                ntable <- hash_map_new_with_capacity_fwd i2 i i0;
+                (ntable0,_) <-
+                  hash_map_move_elements_fwd_back ntable
+                    self.hash_map_slots (int_to_usize 0);
+                Return
+                  (ntable0 with
+                   <|hash_map_num_entries := self.hash_map_num_entries;
+                     hash_map_max_load_factor := (i,i0)|>)
+              od
+            else Return (self with hash_map_max_load_factor := (i,i0))
+          od
+   
+   [test1_fwd_def]  Definition
+      
+      ⊢ test1_fwd =
+        do
+          hm <- hash_map_new_fwd;
+          hm0 <-
+            hash_map_insert_fwd_back hm (int_to_usize 0) (int_to_u64 42);
+          hm1 <-
+            hash_map_insert_fwd_back hm0 (int_to_usize 128) (int_to_u64 18);
+          hm2 <-
+            hash_map_insert_fwd_back hm1 (int_to_usize 1024)
+              (int_to_u64 138);
+          hm3 <-
+            hash_map_insert_fwd_back hm2 (int_to_usize 1056)
+              (int_to_u64 256);
+          i <- hash_map_get_fwd hm3 (int_to_usize 128);
+          if i ≠ int_to_u64 18 then Fail Failure
+          else
+            do
+              hm4 <-
+                hash_map_get_mut_back hm3 (int_to_usize 1024)
+                  (int_to_u64 56);
+              i0 <- hash_map_get_fwd hm4 (int_to_usize 1024);
+              if i0 ≠ int_to_u64 56 then Fail Failure
+              else
+                do
+                  x <- hash_map_remove_fwd hm4 (int_to_usize 1024);
+                  case x of
+                    NONE => Fail Failure
+                  | SOME x0 =>
+                    if x0 ≠ int_to_u64 56 then Fail Failure
+                    else
+                      do
+                        hm5 <- hash_map_remove_back hm4 (int_to_usize 1024);
+                        i1 <- hash_map_get_fwd hm5 (int_to_usize 0);
+                        if i1 ≠ int_to_u64 42 then Fail Failure
+                        else
+                          do
+                            i2 <- hash_map_get_fwd hm5 (int_to_usize 128);
+                            if i2 ≠ int_to_u64 18 then Fail Failure
+                            else
+                              do
+                                i3 <-
+                                  hash_map_get_fwd hm5 (int_to_usize 1056);
+                                if i3 ≠ int_to_u64 256 then Fail Failure
+                                else Return ()
+                              od
+                          od
+                      od
+                od
+            od
+        od
+   
+   
+*)
+end
diff --git a/tests/hol4/hashmap/hashmap_TypesScript.sml b/tests/hol4/hashmap/hashmap_TypesScript.sml
new file mode 100644
index 00000000..a0865956
--- /dev/null
+++ b/tests/hol4/hashmap/hashmap_TypesScript.sml
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap]: type definitions *)
+open primitivesLib divDefLib
+
+val _ = new_theory "hashmap_Types"
+
+
+Datatype:
+  (** [hashmap::List] *)
+  list_t = | ListCons usize 't list_t | ListNil
+End
+
+Datatype:
+  (** [hashmap::HashMap] *)
+  hash_map_t =
+  <|
+    hash_map_num_entries : usize;
+    hash_map_max_load_factor : (usize # usize);
+    hash_map_max_load : usize;
+    hash_map_slots : 't list_t vec;
+  |>
+End
+
+val _ = export_theory ()
diff --git a/tests/hol4/hashmap/hashmap_TypesTheory.sig b/tests/hol4/hashmap/hashmap_TypesTheory.sig
new file mode 100644
index 00000000..4ad77ac5
--- /dev/null
+++ b/tests/hol4/hashmap/hashmap_TypesTheory.sig
@@ -0,0 +1,494 @@
+signature hashmap_TypesTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val hash_map_t_TY_DEF : thm
+    val hash_map_t_case_def : thm
+    val hash_map_t_size_def : thm
+    val list_t_TY_DEF : thm
+    val list_t_case_def : thm
+    val list_t_size_def : thm
+    val recordtype_hash_map_t_seldef_hash_map_max_load_def : thm
+    val recordtype_hash_map_t_seldef_hash_map_max_load_factor_def : thm
+    val recordtype_hash_map_t_seldef_hash_map_max_load_factor_fupd_def : thm
+    val recordtype_hash_map_t_seldef_hash_map_max_load_fupd_def : thm
+    val recordtype_hash_map_t_seldef_hash_map_num_entries_def : thm
+    val recordtype_hash_map_t_seldef_hash_map_num_entries_fupd_def : thm
+    val recordtype_hash_map_t_seldef_hash_map_slots_def : thm
+    val recordtype_hash_map_t_seldef_hash_map_slots_fupd_def : thm
+  
+  (*  Theorems  *)
+    val EXISTS_hash_map_t : thm
+    val FORALL_hash_map_t : thm
+    val datatype_hash_map_t : thm
+    val datatype_list_t : thm
+    val hash_map_t_11 : thm
+    val hash_map_t_Axiom : thm
+    val hash_map_t_accessors : thm
+    val hash_map_t_accfupds : thm
+    val hash_map_t_case_cong : thm
+    val hash_map_t_case_eq : thm
+    val hash_map_t_component_equality : thm
+    val hash_map_t_fn_updates : thm
+    val hash_map_t_fupdcanon : thm
+    val hash_map_t_fupdcanon_comp : thm
+    val hash_map_t_fupdfupds : thm
+    val hash_map_t_fupdfupds_comp : thm
+    val hash_map_t_induction : thm
+    val hash_map_t_literal_11 : thm
+    val hash_map_t_literal_nchotomy : thm
+    val hash_map_t_nchotomy : thm
+    val hash_map_t_updates_eq_literal : thm
+    val list_t_11 : thm
+    val list_t_Axiom : thm
+    val list_t_case_cong : thm
+    val list_t_case_eq : thm
+    val list_t_distinct : thm
+    val list_t_induction : thm
+    val list_t_nchotomy : thm
+  
+  val hashmap_Types_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [divDef] Parent theory of "hashmap_Types"
+   
+   [hash_map_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('hash_map_t').
+                   (∀a0'.
+                      (∃a0 a1 a2 a3.
+                         a0' =
+                         (λa0 a1 a2 a3.
+                              ind_type$CONSTR 0 (a0,a1,a2,a3)
+                                (λn. ind_type$BOTTOM)) a0 a1 a2 a3) ⇒
+                      $var$('hash_map_t') a0') ⇒
+                   $var$('hash_map_t') a0') rep
+   
+   [hash_map_t_case_def]  Definition
+      
+      ⊢ ∀a0 a1 a2 a3 f.
+          hash_map_t_CASE (hash_map_t a0 a1 a2 a3) f = f a0 a1 a2 a3
+   
+   [hash_map_t_size_def]  Definition
+      
+      ⊢ ∀f a0 a1 a2 a3.
+          hash_map_t_size f (hash_map_t a0 a1 a2 a3) =
+          1 + pair_size (λv. 0) (λv. 0) a1
+   
+   [list_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('list_t').
+                   (∀a0'.
+                      (∃a0 a1 a2.
+                         a0' =
+                         (λa0 a1 a2.
+                              ind_type$CONSTR 0 (a0,a1)
+                                (ind_type$FCONS a2 (λn. ind_type$BOTTOM)))
+                           a0 a1 a2 ∧ $var$('list_t') a2) ∨
+                      a0' =
+                      ind_type$CONSTR (SUC 0) (ARB,ARB)
+                        (λn. ind_type$BOTTOM) ⇒
+                      $var$('list_t') a0') ⇒
+                   $var$('list_t') a0') rep
+   
+   [list_t_case_def]  Definition
+      
+      ⊢ (∀a0 a1 a2 f v. list_t_CASE (ListCons a0 a1 a2) f v = f a0 a1 a2) ∧
+        ∀f v. list_t_CASE ListNil f v = v
+   
+   [list_t_size_def]  Definition
+      
+      ⊢ (∀f a0 a1 a2.
+           list_t_size f (ListCons a0 a1 a2) =
+           1 + (f a1 + list_t_size f a2)) ∧ ∀f. list_t_size f ListNil = 0
+   
+   [recordtype_hash_map_t_seldef_hash_map_max_load_def]  Definition
+      
+      ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load = u0
+   
+   [recordtype_hash_map_t_seldef_hash_map_max_load_factor_def]  Definition
+      
+      ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load_factor = p
+   
+   [recordtype_hash_map_t_seldef_hash_map_max_load_factor_fupd_def]  Definition
+      
+      ⊢ ∀f u p u0 v.
+          hash_map_t u p u0 v with hash_map_max_load_factor updated_by f =
+          hash_map_t u (f p) u0 v
+   
+   [recordtype_hash_map_t_seldef_hash_map_max_load_fupd_def]  Definition
+      
+      ⊢ ∀f u p u0 v.
+          hash_map_t u p u0 v with hash_map_max_load updated_by f =
+          hash_map_t u p (f u0) v
+   
+   [recordtype_hash_map_t_seldef_hash_map_num_entries_def]  Definition
+      
+      ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_num_entries = u
+   
+   [recordtype_hash_map_t_seldef_hash_map_num_entries_fupd_def]  Definition
+      
+      ⊢ ∀f u p u0 v.
+          hash_map_t u p u0 v with hash_map_num_entries updated_by f =
+          hash_map_t (f u) p u0 v
+   
+   [recordtype_hash_map_t_seldef_hash_map_slots_def]  Definition
+      
+      ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_slots = v
+   
+   [recordtype_hash_map_t_seldef_hash_map_slots_fupd_def]  Definition
+      
+      ⊢ ∀f u p u0 v.
+          hash_map_t u p u0 v with hash_map_slots updated_by f =
+          hash_map_t u p u0 (f v)
+   
+   [EXISTS_hash_map_t]  Theorem
+      
+      ⊢ ∀P. (∃h. P h) ⇔
+            ∃u0 p u v.
+              P
+                <|hash_map_num_entries := u0;
+                  hash_map_max_load_factor := p; hash_map_max_load := u;
+                  hash_map_slots := v|>
+   
+   [FORALL_hash_map_t]  Theorem
+      
+      ⊢ ∀P. (∀h. P h) ⇔
+            ∀u0 p u v.
+              P
+                <|hash_map_num_entries := u0;
+                  hash_map_max_load_factor := p; hash_map_max_load := u;
+                  hash_map_slots := v|>
+   
+   [datatype_hash_map_t]  Theorem
+      
+      ⊢ DATATYPE
+          (record hash_map_t hash_map_num_entries hash_map_max_load_factor
+             hash_map_max_load hash_map_slots)
+   
+   [datatype_list_t]  Theorem
+      
+      ⊢ DATATYPE (list_t ListCons ListNil)
+   
+   [hash_map_t_11]  Theorem
+      
+      ⊢ ∀a0 a1 a2 a3 a0' a1' a2' a3'.
+          hash_map_t a0 a1 a2 a3 = hash_map_t a0' a1' a2' a3' ⇔
+          a0 = a0' ∧ a1 = a1' ∧ a2 = a2' ∧ a3 = a3'
+   
+   [hash_map_t_Axiom]  Theorem
+      
+      ⊢ ∀f. ∃fn. ∀a0 a1 a2 a3. fn (hash_map_t a0 a1 a2 a3) = f a0 a1 a2 a3
+   
+   [hash_map_t_accessors]  Theorem
+      
+      ⊢ (∀u p u0 v. (hash_map_t u p u0 v).hash_map_num_entries = u) ∧
+        (∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load_factor = p) ∧
+        (∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load = u0) ∧
+        ∀u p u0 v. (hash_map_t u p u0 v).hash_map_slots = v
+   
+   [hash_map_t_accfupds]  Theorem
+      
+      ⊢ (∀h f.
+           (h with hash_map_max_load_factor updated_by f).
+           hash_map_num_entries =
+           h.hash_map_num_entries) ∧
+        (∀h f.
+           (h with hash_map_max_load updated_by f).hash_map_num_entries =
+           h.hash_map_num_entries) ∧
+        (∀h f.
+           (h with hash_map_slots updated_by f).hash_map_num_entries =
+           h.hash_map_num_entries) ∧
+        (∀h f.
+           (h with hash_map_num_entries updated_by f).
+           hash_map_max_load_factor =
+           h.hash_map_max_load_factor) ∧
+        (∀h f.
+           (h with hash_map_max_load updated_by f).hash_map_max_load_factor =
+           h.hash_map_max_load_factor) ∧
+        (∀h f.
+           (h with hash_map_slots updated_by f).hash_map_max_load_factor =
+           h.hash_map_max_load_factor) ∧
+        (∀h f.
+           (h with hash_map_num_entries updated_by f).hash_map_max_load =
+           h.hash_map_max_load) ∧
+        (∀h f.
+           (h with hash_map_max_load_factor updated_by f).hash_map_max_load =
+           h.hash_map_max_load) ∧
+        (∀h f.
+           (h with hash_map_slots updated_by f).hash_map_max_load =
+           h.hash_map_max_load) ∧
+        (∀h f.
+           (h with hash_map_num_entries updated_by f).hash_map_slots =
+           h.hash_map_slots) ∧
+        (∀h f.
+           (h with hash_map_max_load_factor updated_by f).hash_map_slots =
+           h.hash_map_slots) ∧
+        (∀h f.
+           (h with hash_map_max_load updated_by f).hash_map_slots =
+           h.hash_map_slots) ∧
+        (∀h f.
+           (h with hash_map_num_entries updated_by f).hash_map_num_entries =
+           f h.hash_map_num_entries) ∧
+        (∀h f.
+           (h with hash_map_max_load_factor updated_by f).
+           hash_map_max_load_factor =
+           f h.hash_map_max_load_factor) ∧
+        (∀h f.
+           (h with hash_map_max_load updated_by f).hash_map_max_load =
+           f h.hash_map_max_load) ∧
+        ∀h f.
+          (h with hash_map_slots updated_by f).hash_map_slots =
+          f h.hash_map_slots
+   
+   [hash_map_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f.
+          M = M' ∧
+          (∀a0 a1 a2 a3.
+             M' = hash_map_t a0 a1 a2 a3 ⇒ f a0 a1 a2 a3 = f' a0 a1 a2 a3) ⇒
+          hash_map_t_CASE M f = hash_map_t_CASE M' f'
+   
+   [hash_map_t_case_eq]  Theorem
+      
+      ⊢ hash_map_t_CASE x f = v ⇔
+        ∃u p u0 v'. x = hash_map_t u p u0 v' ∧ f u p u0 v' = v
+   
+   [hash_map_t_component_equality]  Theorem
+      
+      ⊢ ∀h1 h2.
+          h1 = h2 ⇔
+          h1.hash_map_num_entries = h2.hash_map_num_entries ∧
+          h1.hash_map_max_load_factor = h2.hash_map_max_load_factor ∧
+          h1.hash_map_max_load = h2.hash_map_max_load ∧
+          h1.hash_map_slots = h2.hash_map_slots
+   
+   [hash_map_t_fn_updates]  Theorem
+      
+      ⊢ (∀f u p u0 v.
+           hash_map_t u p u0 v with hash_map_num_entries updated_by f =
+           hash_map_t (f u) p u0 v) ∧
+        (∀f u p u0 v.
+           hash_map_t u p u0 v with hash_map_max_load_factor updated_by f =
+           hash_map_t u (f p) u0 v) ∧
+        (∀f u p u0 v.
+           hash_map_t u p u0 v with hash_map_max_load updated_by f =
+           hash_map_t u p (f u0) v) ∧
+        ∀f u p u0 v.
+          hash_map_t u p u0 v with hash_map_slots updated_by f =
+          hash_map_t u p u0 (f v)
+   
+   [hash_map_t_fupdcanon]  Theorem
+      
+      ⊢ (∀h g f.
+           h with
+           <|hash_map_max_load_factor updated_by f;
+             hash_map_num_entries updated_by g|> =
+           h with
+           <|hash_map_num_entries updated_by g;
+             hash_map_max_load_factor updated_by f|>) ∧
+        (∀h g f.
+           h with
+           <|hash_map_max_load updated_by f;
+             hash_map_num_entries updated_by g|> =
+           h with
+           <|hash_map_num_entries updated_by g;
+             hash_map_max_load updated_by f|>) ∧
+        (∀h g f.
+           h with
+           <|hash_map_max_load updated_by f;
+             hash_map_max_load_factor updated_by g|> =
+           h with
+           <|hash_map_max_load_factor updated_by g;
+             hash_map_max_load updated_by f|>) ∧
+        (∀h g f.
+           h with
+           <|hash_map_slots updated_by f;
+             hash_map_num_entries updated_by g|> =
+           h with
+           <|hash_map_num_entries updated_by g;
+             hash_map_slots updated_by f|>) ∧
+        (∀h g f.
+           h with
+           <|hash_map_slots updated_by f;
+             hash_map_max_load_factor updated_by g|> =
+           h with
+           <|hash_map_max_load_factor updated_by g;
+             hash_map_slots updated_by f|>) ∧
+        ∀h g f.
+          h with
+          <|hash_map_slots updated_by f; hash_map_max_load updated_by g|> =
+          h with
+          <|hash_map_max_load updated_by g; hash_map_slots updated_by f|>
+   
+   [hash_map_t_fupdcanon_comp]  Theorem
+      
+      ⊢ ((∀g f.
+            hash_map_max_load_factor_fupd f ∘ hash_map_num_entries_fupd g =
+            hash_map_num_entries_fupd g ∘ hash_map_max_load_factor_fupd f) ∧
+         ∀h g f.
+           hash_map_max_load_factor_fupd f ∘ hash_map_num_entries_fupd g ∘
+           h =
+           hash_map_num_entries_fupd g ∘ hash_map_max_load_factor_fupd f ∘
+           h) ∧
+        ((∀g f.
+            hash_map_max_load_fupd f ∘ hash_map_num_entries_fupd g =
+            hash_map_num_entries_fupd g ∘ hash_map_max_load_fupd f) ∧
+         ∀h g f.
+           hash_map_max_load_fupd f ∘ hash_map_num_entries_fupd g ∘ h =
+           hash_map_num_entries_fupd g ∘ hash_map_max_load_fupd f ∘ h) ∧
+        ((∀g f.
+            hash_map_max_load_fupd f ∘ hash_map_max_load_factor_fupd g =
+            hash_map_max_load_factor_fupd g ∘ hash_map_max_load_fupd f) ∧
+         ∀h g f.
+           hash_map_max_load_fupd f ∘ hash_map_max_load_factor_fupd g ∘ h =
+           hash_map_max_load_factor_fupd g ∘ hash_map_max_load_fupd f ∘ h) ∧
+        ((∀g f.
+            hash_map_slots_fupd f ∘ hash_map_num_entries_fupd g =
+            hash_map_num_entries_fupd g ∘ hash_map_slots_fupd f) ∧
+         ∀h g f.
+           hash_map_slots_fupd f ∘ hash_map_num_entries_fupd g ∘ h =
+           hash_map_num_entries_fupd g ∘ hash_map_slots_fupd f ∘ h) ∧
+        ((∀g f.
+            hash_map_slots_fupd f ∘ hash_map_max_load_factor_fupd g =
+            hash_map_max_load_factor_fupd g ∘ hash_map_slots_fupd f) ∧
+         ∀h g f.
+           hash_map_slots_fupd f ∘ hash_map_max_load_factor_fupd g ∘ h =
+           hash_map_max_load_factor_fupd g ∘ hash_map_slots_fupd f ∘ h) ∧
+        (∀g f.
+           hash_map_slots_fupd f ∘ hash_map_max_load_fupd g =
+           hash_map_max_load_fupd g ∘ hash_map_slots_fupd f) ∧
+        ∀h g f.
+          hash_map_slots_fupd f ∘ hash_map_max_load_fupd g ∘ h =
+          hash_map_max_load_fupd g ∘ hash_map_slots_fupd f ∘ h
+   
+   [hash_map_t_fupdfupds]  Theorem
+      
+      ⊢ (∀h g f.
+           h with
+           <|hash_map_num_entries updated_by f;
+             hash_map_num_entries updated_by g|> =
+           h with hash_map_num_entries updated_by f ∘ g) ∧
+        (∀h g f.
+           h with
+           <|hash_map_max_load_factor updated_by f;
+             hash_map_max_load_factor updated_by g|> =
+           h with hash_map_max_load_factor updated_by f ∘ g) ∧
+        (∀h g f.
+           h with
+           <|hash_map_max_load updated_by f;
+             hash_map_max_load updated_by g|> =
+           h with hash_map_max_load updated_by f ∘ g) ∧
+        ∀h g f.
+          h with
+          <|hash_map_slots updated_by f; hash_map_slots updated_by g|> =
+          h with hash_map_slots updated_by f ∘ g
+   
+   [hash_map_t_fupdfupds_comp]  Theorem
+      
+      ⊢ ((∀g f.
+            hash_map_num_entries_fupd f ∘ hash_map_num_entries_fupd g =
+            hash_map_num_entries_fupd (f ∘ g)) ∧
+         ∀h g f.
+           hash_map_num_entries_fupd f ∘ hash_map_num_entries_fupd g ∘ h =
+           hash_map_num_entries_fupd (f ∘ g) ∘ h) ∧
+        ((∀g f.
+            hash_map_max_load_factor_fupd f ∘
+            hash_map_max_load_factor_fupd g =
+            hash_map_max_load_factor_fupd (f ∘ g)) ∧
+         ∀h g f.
+           hash_map_max_load_factor_fupd f ∘
+           hash_map_max_load_factor_fupd g ∘ h =
+           hash_map_max_load_factor_fupd (f ∘ g) ∘ h) ∧
+        ((∀g f.
+            hash_map_max_load_fupd f ∘ hash_map_max_load_fupd g =
+            hash_map_max_load_fupd (f ∘ g)) ∧
+         ∀h g f.
+           hash_map_max_load_fupd f ∘ hash_map_max_load_fupd g ∘ h =
+           hash_map_max_load_fupd (f ∘ g) ∘ h) ∧
+        (∀g f.
+           hash_map_slots_fupd f ∘ hash_map_slots_fupd g =
+           hash_map_slots_fupd (f ∘ g)) ∧
+        ∀h g f.
+          hash_map_slots_fupd f ∘ hash_map_slots_fupd g ∘ h =
+          hash_map_slots_fupd (f ∘ g) ∘ h
+   
+   [hash_map_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀u p u0 v. P (hash_map_t u p u0 v)) ⇒ ∀h. P h
+   
+   [hash_map_t_literal_11]  Theorem
+      
+      ⊢ ∀u01 p1 u1 v1 u02 p2 u2 v2.
+          <|hash_map_num_entries := u01; hash_map_max_load_factor := p1;
+            hash_map_max_load := u1; hash_map_slots := v1|> =
+          <|hash_map_num_entries := u02; hash_map_max_load_factor := p2;
+            hash_map_max_load := u2; hash_map_slots := v2|> ⇔
+          u01 = u02 ∧ p1 = p2 ∧ u1 = u2 ∧ v1 = v2
+   
+   [hash_map_t_literal_nchotomy]  Theorem
+      
+      ⊢ ∀h. ∃u0 p u v.
+          h =
+          <|hash_map_num_entries := u0; hash_map_max_load_factor := p;
+            hash_map_max_load := u; hash_map_slots := v|>
+   
+   [hash_map_t_nchotomy]  Theorem
+      
+      ⊢ ∀hh. ∃u p u0 v. hh = hash_map_t u p u0 v
+   
+   [hash_map_t_updates_eq_literal]  Theorem
+      
+      ⊢ ∀h u0 p u v.
+          h with
+          <|hash_map_num_entries := u0; hash_map_max_load_factor := p;
+            hash_map_max_load := u; hash_map_slots := v|> =
+          <|hash_map_num_entries := u0; hash_map_max_load_factor := p;
+            hash_map_max_load := u; hash_map_slots := v|>
+   
+   [list_t_11]  Theorem
+      
+      ⊢ ∀a0 a1 a2 a0' a1' a2'.
+          ListCons a0 a1 a2 = ListCons a0' a1' a2' ⇔
+          a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
+   
+   [list_t_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1. ∃fn.
+          (∀a0 a1 a2. fn (ListCons a0 a1 a2) = f0 a0 a1 a2 (fn a2)) ∧
+          fn ListNil = f1
+   
+   [list_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f v.
+          M = M' ∧
+          (∀a0 a1 a2. M' = ListCons a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ∧
+          (M' = ListNil ⇒ v = v') ⇒
+          list_t_CASE M f v = list_t_CASE M' f' v'
+   
+   [list_t_case_eq]  Theorem
+      
+      ⊢ list_t_CASE x f v = v' ⇔
+        (∃u t l. x = ListCons u t l ∧ f u t l = v') ∨ x = ListNil ∧ v = v'
+   
+   [list_t_distinct]  Theorem
+      
+      ⊢ ∀a2 a1 a0. ListCons a0 a1 a2 ≠ ListNil
+   
+   [list_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀l. P l ⇒ ∀t u. P (ListCons u t l)) ∧ P ListNil ⇒ ∀l. P l
+   
+   [list_t_nchotomy]  Theorem
+      
+      ⊢ ∀ll. (∃u t l. ll = ListCons u t l) ∨ ll = ListNil
+   
+   
+*)
+end
-- 
cgit v1.2.3