Make more proofs about the hashmap proto

1 files changed, 55 insertions, 0 deletions

diff --git a/backends/hol4/testHashmapTheory.sig b/backends/hol4/testHashmapTheory.sig
index 16031716..1d304723 100644
--- a/backends/hol4/testHashmapTheory.sig
+++ b/backends/hol4/testHashmapTheory.sig
@@ -7,18 +7,25 @@ sig
   
   (*  Definitions  *)
     val distinct_keys_def : thm
+    val distinct_keys_f_def : thm
+    val for_all_def : thm
     val list_t_TY_DEF : thm
     val list_t_case_def : thm
     val list_t_size_def : thm
     val list_t_v_def : thm
     val lookup_def : thm
+    val pairwise_rel_def : thm
   
   (*  Theorems  *)
     val datatype_list_t : thm
     val distinct_keys_cons : thm
+    val distinct_keys_f_eq_distinct_keys : thm
+    val distinct_keys_f_insert : thm
+    val distinct_keys_f_insert_for_all : thm
     val distinct_keys_insert : thm
     val distinct_keys_insert_index_neq : thm
     val distinct_keys_tail : thm
+    val for_all_quant : thm
     val insert_index_neq : thm
     val insert_lem : thm
     val insert_lem_aux : thm
@@ -34,6 +41,7 @@ sig
     val nth_mut_fwd_def : thm
     val nth_mut_fwd_ind : thm
     val nth_mut_fwd_spec : thm
+    val pairwise_rel_quant : thm
   
   val testHashmap_grammars : type_grammar.grammar * term_grammar.grammar
 (*
@@ -63,6 +71,15 @@ sig
             j < len ls ⇒
             FST (index i ls) ≠ FST (index j ls)
    
+   [distinct_keys_f_def]  Definition
+      
+      ⊢ ∀ls. distinct_keys_f ls ⇔ pairwise_rel (λx y. FST x ≠ FST y) ls
+   
+   [for_all_def]  Definition
+      
+      ⊢ (∀p. for_all p [] ⇔ T) ∧
+        ∀p x ls. for_all p (x::ls) ⇔ p x ∧ for_all p ls
+   
    [list_t_TY_DEF]  Definition
       
       ⊢ ∃rep.
@@ -101,6 +118,12 @@ sig
       
       ⊢ ∀key ls. lookup key ls = lookup_raw key (list_t_v ls)
    
+   [pairwise_rel_def]  Definition
+      
+      ⊢ (∀p. pairwise_rel p [] ⇔ T) ∧
+        ∀p x ls.
+          pairwise_rel p (x::ls) ⇔ for_all (p x) ls ∧ pairwise_rel p ls
+   
    [datatype_list_t]  Theorem
       
       ⊢ DATATYPE (list_t ListCons ListNil)
@@ -112,6 +135,28 @@ sig
           distinct_keys ls ⇒
           distinct_keys ((k,v)::ls)
    
+   [distinct_keys_f_eq_distinct_keys]  Theorem
+      
+      ⊢ ∀ls. distinct_keys_f ls ⇔ distinct_keys ls
+   
+   [distinct_keys_f_insert]  Theorem
+      
+      [oracles: DISK_THM] [axioms: insert_def] []
+      ⊢ ∀k v ls0 ls1.
+          distinct_keys_f (list_t_v ls0) ⇒
+          insert k v ls0 = Return ls1 ⇒
+          distinct_keys_f (list_t_v ls1)
+   
+   [distinct_keys_f_insert_for_all]  Theorem
+      
+      [oracles: DISK_THM] [axioms: insert_def] []
+      ⊢ ∀k v k1 ls0 ls1.
+          k1 ≠ k ⇒
+          for_all (λy. k1 ≠ FST y) (list_t_v ls0) ⇒
+          pairwise_rel (λx y. FST x ≠ FST y) (list_t_v ls0) ⇒
+          insert k v ls0 = Return ls1 ⇒
+          for_all (λy. k1 ≠ FST y) (list_t_v ls1)
+   
    [distinct_keys_insert]  Theorem
       
       [oracles: DISK_THM] [axioms: insert_def] []
@@ -135,6 +180,10 @@ sig
       
       ⊢ ∀k v ls. distinct_keys ((k,v)::ls) ⇒ distinct_keys ls
    
+   [for_all_quant]  Theorem
+      
+      ⊢ ∀p ls. for_all p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls)
+   
    [insert_index_neq]  Theorem
       
       [oracles: DISK_THM] [axioms: insert_def] []
@@ -245,6 +294,12 @@ sig
           | Fail v1 => F
           | Diverge => F
    
+   [pairwise_rel_quant]  Theorem
+      
+      ⊢ ∀p ls.
+          pairwise_rel p ls ⇔
+          ∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls)
+   
    
 *)
 end