summaryrefslogtreecommitdiff
path: root/tests/hol4/hashmap
diff options
context:
space:
mode:
authorSon Ho2023-06-02 17:23:29 +0200
committerSon HO2023-06-04 21:54:38 +0200
commitdc46dbb9a01329c39673fedc195006745c365030 (patch)
treedf1c93fbb2cb6a0e4e7b534d2b624a3e2b999ad5 /tests/hol4/hashmap
parent54afbf3a8b71ee729641ee3024d19aaf8fa92a67 (diff)
Update the HOL4 proofs for the last *release* version of HOL4
Diffstat (limited to '')
-rw-r--r--tests/hol4/hashmap/hashmap_PropertiesScript.sml10
-rw-r--r--tests/hol4/hashmap/hashmap_TypesTheory.sig96
-rw-r--r--tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig108
3 files changed, 108 insertions, 106 deletions
diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
index c8e87f07..7259f2f5 100644
--- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml
+++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
@@ -1040,7 +1040,7 @@ QED
(* TODO: the names introduced by progress are random, which is confusing.
It also makes the proofs less stable.
- Try to use the names given by the let-bindings. *)
+ Update the progress tactic to use the names given by the let-bindings. *)
Theorem hash_map_move_elements_loop_fwd_back_spec_aux:
∀ hm slots i n.
@@ -1138,16 +1138,17 @@ Proof
fs [])
>-(
(* Prove that index j (update slots i) = index j slots *)
- pop_assum (qspec_assume ‘int_to_usize j’) >> gvs [] >> massage >> gvs [] >>
+ first_x_assum (qspec_assume ‘int_to_usize j’) >> gvs [] >> massage >> gvs [] >>
fs [vec_len_def] >>
massage >> gvs [] >>
sg ‘j ≠ usize_to_int i’ >- int_tac >> gvs [vec_index_def, vec_update_def] >>
massage >>
(* Use the fact that slot_t_lookup k (index i ... slots) = NONE *)
- last_x_assum (qspec_assume ‘k’) >>
+ first_x_assum (qspec_assume ‘k’) >>
first_assum sg_premise_tac
>- (
sg ‘usize_to_int i < j’ >- int_tac >> fs [] >>
+ sg ‘usize_to_int i ≤ j’ >- int_tac >> fs [] >>
(* TODO: we have to rewrite key_MEM_j_lookup_i_is_NONE before applying
metis_tac *)
assume_tac key_MEM_j_lookup_i_is_NONE >> fs [] >>
@@ -1156,7 +1157,8 @@ Proof
(* Use the fact that as the key is in the slots after i, it can't be in “hm” (yet) *)
last_x_assum (qspec_assume ‘j’) >> gvs [] >>
first_x_assum sg_premise_tac >- (int_tac) >> gvs [] >>
- first_x_assum imp_res_tac) >>
+ first_x_assum imp_res_tac >>
+ metis_tac []) >>
(* The conclusion of the theorem (the post-condition) *)
conj_tac
>-(
diff --git a/tests/hol4/hashmap/hashmap_TypesTheory.sig b/tests/hol4/hashmap/hashmap_TypesTheory.sig
index 4ad77ac5..a8839fa4 100644
--- a/tests/hol4/hashmap/hashmap_TypesTheory.sig
+++ b/tests/hol4/hashmap/hashmap_TypesTheory.sig
@@ -5,18 +5,18 @@ sig
(* Definitions *)
val hash_map_t_TY_DEF : thm
val hash_map_t_case_def : thm
+ val hash_map_t_hash_map_max_load : thm
+ val hash_map_t_hash_map_max_load_factor : thm
+ val hash_map_t_hash_map_max_load_factor_fupd : thm
+ val hash_map_t_hash_map_max_load_fupd : thm
+ val hash_map_t_hash_map_num_entries : thm
+ val hash_map_t_hash_map_num_entries_fupd : thm
+ val hash_map_t_hash_map_slots : thm
+ val hash_map_t_hash_map_slots_fupd : 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
@@ -72,6 +72,46 @@ sig
⊢ ∀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_hash_map_max_load] Definition
+
+ ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load = u0
+
+ [hash_map_t_hash_map_max_load_factor] Definition
+
+ ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load_factor = p
+
+ [hash_map_t_hash_map_max_load_factor_fupd] 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
+
+ [hash_map_t_hash_map_max_load_fupd] 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
+
+ [hash_map_t_hash_map_num_entries] Definition
+
+ ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_num_entries = u
+
+ [hash_map_t_hash_map_num_entries_fupd] 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
+
+ [hash_map_t_hash_map_slots] Definition
+
+ ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_slots = v
+
+ [hash_map_t_hash_map_slots_fupd] 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)
+
[hash_map_t_size_def] Definition
⊢ ∀f a0 a1 a2 a3.
@@ -108,46 +148,6 @@ sig
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) ⇔
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig b/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
index bea7eb76..a3e770ea 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
+++ b/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
@@ -5,18 +5,18 @@ sig
(* Definitions *)
val hashmap_hash_map_t_TY_DEF : thm
val hashmap_hash_map_t_case_def : thm
+ val hashmap_hash_map_t_hashmap_hash_map_max_load : thm
+ val hashmap_hash_map_t_hashmap_hash_map_max_load_factor : thm
+ val hashmap_hash_map_t_hashmap_hash_map_max_load_factor_fupd : thm
+ val hashmap_hash_map_t_hashmap_hash_map_max_load_fupd : thm
+ val hashmap_hash_map_t_hashmap_hash_map_num_entries : thm
+ val hashmap_hash_map_t_hashmap_hash_map_num_entries_fupd : thm
+ val hashmap_hash_map_t_hashmap_hash_map_slots : thm
+ val hashmap_hash_map_t_hashmap_hash_map_slots_fupd : thm
val hashmap_hash_map_t_size_def : thm
val hashmap_list_t_TY_DEF : thm
val hashmap_list_t_case_def : thm
val hashmap_list_t_size_def : thm
- val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_def : thm
- val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_factor_def : thm
- val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_factor_fupd_def : thm
- val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_fupd_def : thm
- val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_num_entries_def : thm
- val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_num_entries_fupd_def : thm
- val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_slots_def : thm
- val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_slots_fupd_def : thm
(* Theorems *)
val EXISTS_hashmap_hash_map_t : thm
@@ -73,92 +73,92 @@ sig
hashmap_hash_map_t_CASE (hashmap_hash_map_t a0 a1 a2 a3) f =
f a0 a1 a2 a3
- [hashmap_hash_map_t_size_def] Definition
-
- ⊢ ∀f a0 a1 a2 a3.
- hashmap_hash_map_t_size f (hashmap_hash_map_t a0 a1 a2 a3) =
- 1 + pair_size (λv. 0) (λv. 0) a1
-
- [hashmap_list_t_TY_DEF] Definition
-
- ⊢ ∃rep.
- TYPE_DEFINITION
- (λa0'.
- ∀ $var$('hashmap_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$('hashmap_list_t') a2) ∨
- a0' =
- ind_type$CONSTR (SUC 0) (ARB,ARB)
- (λn. ind_type$BOTTOM) ⇒
- $var$('hashmap_list_t') a0') ⇒
- $var$('hashmap_list_t') a0') rep
-
- [hashmap_list_t_case_def] Definition
-
- ⊢ (∀a0 a1 a2 f v.
- hashmap_list_t_CASE (HashmapListCons a0 a1 a2) f v = f a0 a1 a2) ∧
- ∀f v. hashmap_list_t_CASE HashmapListNil f v = v
-
- [hashmap_list_t_size_def] Definition
-
- ⊢ (∀f a0 a1 a2.
- hashmap_list_t_size f (HashmapListCons a0 a1 a2) =
- 1 + (f a1 + hashmap_list_t_size f a2)) ∧
- ∀f. hashmap_list_t_size f HashmapListNil = 0
-
- [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_def] Definition
+ [hashmap_hash_map_t_hashmap_hash_map_max_load] Definition
⊢ ∀u p u0 v.
(hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load = u0
- [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_factor_def] Definition
+ [hashmap_hash_map_t_hashmap_hash_map_max_load_factor] Definition
⊢ ∀u p u0 v.
(hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load_factor =
p
- [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_factor_fupd_def] Definition
+ [hashmap_hash_map_t_hashmap_hash_map_max_load_factor_fupd] Definition
⊢ ∀f u p u0 v.
hashmap_hash_map_t u p u0 v with
hashmap_hash_map_max_load_factor updated_by f =
hashmap_hash_map_t u (f p) u0 v
- [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_fupd_def] Definition
+ [hashmap_hash_map_t_hashmap_hash_map_max_load_fupd] Definition
⊢ ∀f u p u0 v.
hashmap_hash_map_t u p u0 v with
hashmap_hash_map_max_load updated_by f =
hashmap_hash_map_t u p (f u0) v
- [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_num_entries_def] Definition
+ [hashmap_hash_map_t_hashmap_hash_map_num_entries] Definition
⊢ ∀u p u0 v.
(hashmap_hash_map_t u p u0 v).hashmap_hash_map_num_entries = u
- [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_num_entries_fupd_def] Definition
+ [hashmap_hash_map_t_hashmap_hash_map_num_entries_fupd] Definition
⊢ ∀f u p u0 v.
hashmap_hash_map_t u p u0 v with
hashmap_hash_map_num_entries updated_by f =
hashmap_hash_map_t (f u) p u0 v
- [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_slots_def] Definition
+ [hashmap_hash_map_t_hashmap_hash_map_slots] Definition
⊢ ∀u p u0 v. (hashmap_hash_map_t u p u0 v).hashmap_hash_map_slots = v
- [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_slots_fupd_def] Definition
+ [hashmap_hash_map_t_hashmap_hash_map_slots_fupd] Definition
⊢ ∀f u p u0 v.
hashmap_hash_map_t u p u0 v with
hashmap_hash_map_slots updated_by f =
hashmap_hash_map_t u p u0 (f v)
+ [hashmap_hash_map_t_size_def] Definition
+
+ ⊢ ∀f a0 a1 a2 a3.
+ hashmap_hash_map_t_size f (hashmap_hash_map_t a0 a1 a2 a3) =
+ 1 + pair_size (λv. 0) (λv. 0) a1
+
+ [hashmap_list_t_TY_DEF] Definition
+
+ ⊢ ∃rep.
+ TYPE_DEFINITION
+ (λa0'.
+ ∀ $var$('hashmap_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$('hashmap_list_t') a2) ∨
+ a0' =
+ ind_type$CONSTR (SUC 0) (ARB,ARB)
+ (λn. ind_type$BOTTOM) ⇒
+ $var$('hashmap_list_t') a0') ⇒
+ $var$('hashmap_list_t') a0') rep
+
+ [hashmap_list_t_case_def] Definition
+
+ ⊢ (∀a0 a1 a2 f v.
+ hashmap_list_t_CASE (HashmapListCons a0 a1 a2) f v = f a0 a1 a2) ∧
+ ∀f v. hashmap_list_t_CASE HashmapListNil f v = v
+
+ [hashmap_list_t_size_def] Definition
+
+ ⊢ (∀f a0 a1 a2.
+ hashmap_list_t_size f (HashmapListCons a0 a1 a2) =
+ 1 + (f a1 + hashmap_list_t_size f a2)) ∧
+ ∀f. hashmap_list_t_size f HashmapListNil = 0
+
[EXISTS_hashmap_hash_map_t] Theorem
⊢ ∀P. (∃h. P h) ⇔