diff options
| author | Son Ho | 2023-01-31 18:24:47 +0100 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:54:38 +0200 |
| commit | bbe4a8b234d183e36c157dbc6b9900214e405a52 (patch) | |
| tree | 3894ae7606ae5f9aa5f6dc3d56007d40b94e6339 /backends/hol4/testHashmapScript.sml | |
| parent | bc2a51e89f198ab33549a59a59bcf418921f8529 (diff) | |
Start working on divDefLib for diverging definitions
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/testHashmapScript.sml | 14 |
1 files changed, 2 insertions, 12 deletions
diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml index 249bc0bf..77c97651 100644 --- a/backends/hol4/testHashmapScript.sml +++ b/backends/hol4/testHashmapScript.sml @@ -37,17 +37,6 @@ val list_t_v_def = Define ‘ list_t_v (ListCons x tl) = x :: list_t_v tl ’ -(* TODO: move *) -Theorem index_eq: - (∀x ls. index 0 (x :: ls) = x) ∧ - (∀i x ls. index i (x :: ls) = - if (0 < i) ∨ (0 ≤ i ∧ i ≠ 0) then index (i - 1) ls - else (if i = 0 then x else ARB)) -Proof - rw [index_def] >> fs [] >> - exfalso >> cooper_tac -QED - Theorem nth_mut_fwd_spec: !(ls : 't list_t) (i : u32). u32_to_int i < len (list_t_v ls) ==> @@ -57,7 +46,7 @@ Theorem nth_mut_fwd_spec: | Loop => F Proof Induct_on ‘ls’ >> rw [list_t_v_def, len_def] >~ [‘ListNil’] - >-(massage >> exfalso >> cooper_tac) >> + >-(massage >> int_tac) >> pure_once_rewrite_tac [nth_mut_fwd_def] >> rw [] >> fs [index_eq] >> progress >> progress @@ -108,6 +97,7 @@ Theorem insert_lem: lookup key ls1 = SOME value /\ (* The other bindings are left unchanged *) (!k. k <> key ==> lookup k ls = lookup k ls1) + (* TODO: invariant *) | Fail _ => F | Loop => F Proof |