diff options
Diffstat (limited to '')
| -rw-r--r-- | .gitignore | 4 | ||||
| -rw-r--r-- | backends/hol4/divDefLibTestTheory.sig | 5 | ||||
| -rw-r--r-- | backends/hol4/divDefNoFixLibTestTheory.sig | 51 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 226 | ||||
| -rw-r--r-- | tests/hol4/betree/betreeMain_TypesTheory.sig | 310 | ||||
| -rw-r--r-- | tests/hol4/hashmap/hashmap_PropertiesScript.sml | 10 | ||||
| -rw-r--r-- | tests/hol4/hashmap/hashmap_TypesTheory.sig | 96 | ||||
| -rw-r--r-- | tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig | 108 | ||||
| -rw-r--r-- | tests/hol4/misc-constants/constantsTheory.sig | 60 | ||||
| -rw-r--r-- | tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig | 68 |
10 files changed, 468 insertions, 470 deletions
@@ -61,6 +61,10 @@ tests/fstar/misc/obj/ .HOLMK .hollogs .holobjs +*.dat +*.ui +*.uo +*Theory.sml # Misc /fstar-tests diff --git a/backends/hol4/divDefLibTestTheory.sig b/backends/hol4/divDefLibTestTheory.sig index d8cc4ab5..2df28a2f 100644 --- a/backends/hol4/divDefLibTestTheory.sig +++ b/backends/hol4/divDefLibTestTheory.sig @@ -53,7 +53,6 @@ sig val tree_distinct : thm val tree_induction : thm val tree_nchotomy : thm - val tree_size_eq : thm val divDefLibTest_grammars : type_grammar.grammar * term_grammar.grammar (* @@ -434,10 +433,6 @@ sig ⊢ ∀tt. (∃a. tt = TLeaf a) ∨ ∃n. tt = TNode n - [tree_size_eq] Theorem - - ⊢ tree1_size f = list_size (tree_size f) - *) end diff --git a/backends/hol4/divDefNoFixLibTestTheory.sig b/backends/hol4/divDefNoFixLibTestTheory.sig index 999cf543..6c8f373c 100644 --- a/backends/hol4/divDefNoFixLibTestTheory.sig +++ b/backends/hol4/divDefNoFixLibTestTheory.sig @@ -5,12 +5,12 @@ sig (* Definitions *) val even___E_def : thm val even___P_def : thm - val even___fuel0_def_UNION_extract0 : thm - val even___fuel0_def_UNION_extract1 : thm - val even___fuel0_def_UNION_primitive : thm - val even___fuel_def_UNION_extract0 : thm - val even___fuel_def_UNION_extract1 : thm - val even___fuel_def_UNION_primitive : thm + val even___fuel0_UNION_extract0_def : thm + val even___fuel0_UNION_extract1_def : thm + val even___fuel0_UNION_primitive_def : thm + val even___fuel_UNION_extract0_def : thm + val even___fuel_UNION_extract1_def : thm + val even___fuel_UNION_primitive_def : thm val even_def : thm val list_t_TY_DEF : thm val list_t_case_def : thm @@ -56,17 +56,17 @@ sig ⊢ ∀i $var$($n). even___P i $var$($n) ⇔ ¬is_diverge (even___fuel0 $var$($n) i) - [even___fuel0_def_UNION_extract0] Definition + [even___fuel0_UNION_extract0_def] Definition - ⊢ ∀x x0. even___fuel0 x x0 = even___fuel0_def_UNION (INL (x,x0)) + ⊢ ∀x x0. even___fuel0 x x0 = even___fuel0_UNION (INL (x,x0)) - [even___fuel0_def_UNION_extract1] Definition + [even___fuel0_UNION_extract1_def] Definition - ⊢ ∀x x0. odd___fuel0 x x0 = even___fuel0_def_UNION (INR (x,x0)) + ⊢ ∀x x0. odd___fuel0 x x0 = even___fuel0_UNION (INR (x,x0)) - [even___fuel0_def_UNION_primitive] Definition + [even___fuel0_UNION_primitive_def] Definition - ⊢ even___fuel0_def_UNION = + ⊢ even___fuel0_UNION = WFREC (@R. WF R ∧ (∀i $var$($n) $var$($m). @@ -75,7 +75,7 @@ sig ∀i $var$($n) $var$($m). $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ R (INL ($var$($m),i − 1)) (INR ($var$($n),i))) - (λeven___fuel0_def_UNION a. + (λeven___fuel0_UNION a. case a of INL ($var$($n),i) => I @@ -85,9 +85,7 @@ sig if i = 0 then do b <- Return T; Return b od else do - b <- - even___fuel0_def_UNION - (INR ($var$($m),i − 1)); + b <- even___fuel0_UNION (INR ($var$($m),i − 1)); Return b od) | INR ($var$($n'),i') => @@ -98,22 +96,21 @@ sig if i' = 0 then do b <- Return F; Return b od else do - b <- - even___fuel0_def_UNION (INL ($var$($m),i' − 1)); + b <- even___fuel0_UNION (INL ($var$($m),i' − 1)); Return b od)) - [even___fuel_def_UNION_extract0] Definition + [even___fuel_UNION_extract0_def] Definition - ⊢ ∀x x0. even___fuel x x0 = even___fuel_def_UNION (INL (x,x0)) + ⊢ ∀x x0. even___fuel x x0 = even___fuel_UNION (INL (x,x0)) - [even___fuel_def_UNION_extract1] Definition + [even___fuel_UNION_extract1_def] Definition - ⊢ ∀x x0. odd___fuel x x0 = even___fuel_def_UNION (INR (x,x0)) + ⊢ ∀x x0. odd___fuel x x0 = even___fuel_UNION (INR (x,x0)) - [even___fuel_def_UNION_primitive] Definition + [even___fuel_UNION_primitive_def] Definition - ⊢ even___fuel_def_UNION = + ⊢ even___fuel_UNION = WFREC (@R. WF R ∧ (∀i $var$($n) $var$($m). @@ -122,7 +119,7 @@ sig ∀i $var$($n) $var$($m). $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ R (INL ($var$($m),i − 1)) (INR ($var$($n),i))) - (λeven___fuel_def_UNION a. + (λeven___fuel_UNION a. case a of INL ($var$($n),i) => I @@ -130,14 +127,14 @@ sig 0 => Diverge | SUC $var$($m) => if i = 0 then Return T - else even___fuel_def_UNION (INR ($var$($m),i − 1))) + else even___fuel_UNION (INR ($var$($m),i − 1))) | INR ($var$($n'),i') => I (case $var$($n') of 0 => Diverge | SUC $var$($m) => if i' = 0 then Return F - else even___fuel_def_UNION (INL ($var$($m),i' − 1)))) + else even___fuel_UNION (INL ($var$($m),i' − 1)))) [even_def] Definition diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index ae7f083d..6660b02d 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -359,195 +359,200 @@ sig [string] Parent theory of "primitives" - [isize_bounds] Axiom - - [oracles: ] [axioms: isize_bounds] [] - ⊢ isize_min ≤ i16_min ∧ i16_max ≤ isize_max - - [usize_bounds] Axiom - - [oracles: ] [axioms: usize_bounds] [] ⊢ u16_max ≤ usize_max - - [isize_to_int_bounds] Axiom + [i128_to_int_bounds] Axiom - [oracles: ] [axioms: isize_to_int_bounds] [] - ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max + [oracles: ] [axioms: i128_to_int_bounds] [] + ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max - [i8_to_int_bounds] Axiom + [i128_to_int_int_to_i128] Axiom - [oracles: ] [axioms: i8_to_int_bounds] [] - ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max + [oracles: ] [axioms: i128_to_int_int_to_i128] [] + ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n [i16_to_int_bounds] Axiom [oracles: ] [axioms: i16_to_int_bounds] [] ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max + [i16_to_int_int_to_i16] Axiom + + [oracles: ] [axioms: i16_to_int_int_to_i16] [] + ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n + [i32_to_int_bounds] Axiom [oracles: ] [axioms: i32_to_int_bounds] [] ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max + [i32_to_int_int_to_i32] Axiom + + [oracles: ] [axioms: i32_to_int_int_to_i32] [] + ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n + [i64_to_int_bounds] Axiom [oracles: ] [axioms: i64_to_int_bounds] [] ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max - [i128_to_int_bounds] Axiom + [i64_to_int_int_to_i64] Axiom - [oracles: ] [axioms: i128_to_int_bounds] [] - ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max + [oracles: ] [axioms: i64_to_int_int_to_i64] [] + ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n - [usize_to_int_bounds] Axiom + [i8_to_int_bounds] Axiom - [oracles: ] [axioms: usize_to_int_bounds] [] - ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max + [oracles: ] [axioms: i8_to_int_bounds] [] + ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max - [u8_to_int_bounds] Axiom + [i8_to_int_int_to_i8] Axiom - [oracles: ] [axioms: u8_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max + [oracles: ] [axioms: i8_to_int_int_to_i8] [] + ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n - [u16_to_int_bounds] Axiom + [int_to_i128_i128_to_int] Axiom - [oracles: ] [axioms: u16_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max + [oracles: ] [axioms: int_to_i128_i128_to_int] [] + ⊢ ∀i. int_to_i128 (i128_to_int i) = i - [u32_to_int_bounds] Axiom + [int_to_i16_i16_to_int] Axiom - [oracles: ] [axioms: u32_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max + [oracles: ] [axioms: int_to_i16_i16_to_int] [] + ⊢ ∀i. int_to_i16 (i16_to_int i) = i - [u64_to_int_bounds] Axiom + [int_to_i32_i32_to_int] Axiom - [oracles: ] [axioms: u64_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max + [oracles: ] [axioms: int_to_i32_i32_to_int] [] + ⊢ ∀i. int_to_i32 (i32_to_int i) = i - [u128_to_int_bounds] Axiom + [int_to_i64_i64_to_int] Axiom - [oracles: ] [axioms: u128_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max + [oracles: ] [axioms: int_to_i64_i64_to_int] [] + ⊢ ∀i. int_to_i64 (i64_to_int i) = i - [isize_to_int_int_to_isize] Axiom + [int_to_i8_i8_to_int] Axiom - [oracles: ] [axioms: isize_to_int_int_to_isize] [] - ⊢ ∀n. isize_min ≤ n ∧ n ≤ isize_max ⇒ - isize_to_int (int_to_isize n) = n + [oracles: ] [axioms: int_to_i8_i8_to_int] [] + ⊢ ∀i. int_to_i8 (i8_to_int i) = i - [i8_to_int_int_to_i8] Axiom + [int_to_isize_isize_to_int] Axiom - [oracles: ] [axioms: i8_to_int_int_to_i8] [] - ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n + [oracles: ] [axioms: int_to_isize_isize_to_int] [] + ⊢ ∀i. int_to_isize (isize_to_int i) = i - [i16_to_int_int_to_i16] Axiom + [int_to_u128_u128_to_int] Axiom - [oracles: ] [axioms: i16_to_int_int_to_i16] [] - ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n + [oracles: ] [axioms: int_to_u128_u128_to_int] [] + ⊢ ∀i. int_to_u128 (u128_to_int i) = i - [i32_to_int_int_to_i32] Axiom + [int_to_u16_u16_to_int] Axiom - [oracles: ] [axioms: i32_to_int_int_to_i32] [] - ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n + [oracles: ] [axioms: int_to_u16_u16_to_int] [] + ⊢ ∀i. int_to_u16 (u16_to_int i) = i - [i64_to_int_int_to_i64] Axiom + [int_to_u32_u32_to_int] Axiom - [oracles: ] [axioms: i64_to_int_int_to_i64] [] - ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n + [oracles: ] [axioms: int_to_u32_u32_to_int] [] + ⊢ ∀i. int_to_u32 (u32_to_int i) = i - [i128_to_int_int_to_i128] Axiom + [int_to_u64_u64_to_int] Axiom - [oracles: ] [axioms: i128_to_int_int_to_i128] [] - ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n + [oracles: ] [axioms: int_to_u64_u64_to_int] [] + ⊢ ∀i. int_to_u64 (u64_to_int i) = i - [usize_to_int_int_to_usize] Axiom + [int_to_u8_u8_to_int] Axiom - [oracles: ] [axioms: usize_to_int_int_to_usize] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ usize_max ⇒ usize_to_int (int_to_usize n) = n + [oracles: ] [axioms: int_to_u8_u8_to_int] [] + ⊢ ∀i. int_to_u8 (u8_to_int i) = i - [u8_to_int_int_to_u8] Axiom + [int_to_usize_usize_to_int] Axiom - [oracles: ] [axioms: u8_to_int_int_to_u8] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n + [oracles: ] [axioms: int_to_usize_usize_to_int] [] + ⊢ ∀i. int_to_usize (usize_to_int i) = i - [u16_to_int_int_to_u16] Axiom + [isize_bounds] Axiom - [oracles: ] [axioms: u16_to_int_int_to_u16] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n + [oracles: ] [axioms: isize_bounds] [] + ⊢ isize_min ≤ i16_min ∧ i16_max ≤ isize_max - [u32_to_int_int_to_u32] Axiom + [isize_to_int_bounds] Axiom - [oracles: ] [axioms: u32_to_int_int_to_u32] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n + [oracles: ] [axioms: isize_to_int_bounds] [] + ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max - [u64_to_int_int_to_u64] Axiom + [isize_to_int_int_to_isize] Axiom - [oracles: ] [axioms: u64_to_int_int_to_u64] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n + [oracles: ] [axioms: isize_to_int_int_to_isize] [] + ⊢ ∀n. isize_min ≤ n ∧ n ≤ isize_max ⇒ + isize_to_int (int_to_isize n) = n + + [mk_vec_axiom] Axiom + + [oracles: ] [axioms: mk_vec_axiom] [] + ⊢ ∀l. len l ≤ usize_max ⇒ vec_to_list (mk_vec l) = l + + [u128_to_int_bounds] Axiom + + [oracles: ] [axioms: u128_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max [u128_to_int_int_to_u128] Axiom [oracles: ] [axioms: u128_to_int_int_to_u128] [] ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n - [int_to_i8_i8_to_int] Axiom - - [oracles: ] [axioms: int_to_i8_i8_to_int] [] - ⊢ ∀i. int_to_i8 (i8_to_int i) = i - - [int_to_i16_i16_to_int] Axiom + [u16_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i16_i16_to_int] [] - ⊢ ∀i. int_to_i16 (i16_to_int i) = i + [oracles: ] [axioms: u16_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max - [int_to_i32_i32_to_int] Axiom + [u16_to_int_int_to_u16] Axiom - [oracles: ] [axioms: int_to_i32_i32_to_int] [] - ⊢ ∀i. int_to_i32 (i32_to_int i) = i + [oracles: ] [axioms: u16_to_int_int_to_u16] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n - [int_to_i64_i64_to_int] Axiom + [u32_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i64_i64_to_int] [] - ⊢ ∀i. int_to_i64 (i64_to_int i) = i + [oracles: ] [axioms: u32_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max - [int_to_i128_i128_to_int] Axiom + [u32_to_int_int_to_u32] Axiom - [oracles: ] [axioms: int_to_i128_i128_to_int] [] - ⊢ ∀i. int_to_i128 (i128_to_int i) = i + [oracles: ] [axioms: u32_to_int_int_to_u32] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n - [int_to_isize_isize_to_int] Axiom + [u64_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_isize_isize_to_int] [] - ⊢ ∀i. int_to_isize (isize_to_int i) = i + [oracles: ] [axioms: u64_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max - [int_to_u8_u8_to_int] Axiom + [u64_to_int_int_to_u64] Axiom - [oracles: ] [axioms: int_to_u8_u8_to_int] [] - ⊢ ∀i. int_to_u8 (u8_to_int i) = i + [oracles: ] [axioms: u64_to_int_int_to_u64] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n - [int_to_u16_u16_to_int] Axiom + [u8_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u16_u16_to_int] [] - ⊢ ∀i. int_to_u16 (u16_to_int i) = i + [oracles: ] [axioms: u8_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max - [int_to_u32_u32_to_int] Axiom + [u8_to_int_int_to_u8] Axiom - [oracles: ] [axioms: int_to_u32_u32_to_int] [] - ⊢ ∀i. int_to_u32 (u32_to_int i) = i + [oracles: ] [axioms: u8_to_int_int_to_u8] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n - [int_to_u64_u64_to_int] Axiom + [usize_bounds] Axiom - [oracles: ] [axioms: int_to_u64_u64_to_int] [] - ⊢ ∀i. int_to_u64 (u64_to_int i) = i + [oracles: ] [axioms: usize_bounds] [] ⊢ u16_max ≤ usize_max - [int_to_u128_u128_to_int] Axiom + [usize_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u128_u128_to_int] [] - ⊢ ∀i. int_to_u128 (u128_to_int i) = i + [oracles: ] [axioms: usize_to_int_bounds] [] + ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max - [int_to_usize_usize_to_int] Axiom + [usize_to_int_int_to_usize] Axiom - [oracles: ] [axioms: int_to_usize_usize_to_int] [] - ⊢ ∀i. int_to_usize (usize_to_int i) = i + [oracles: ] [axioms: usize_to_int_int_to_usize] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ usize_max ⇒ usize_to_int (int_to_usize n) = n [vec_to_list_num_bounds] Axiom @@ -555,11 +560,6 @@ sig ⊢ ∀v. 0 ≤ LENGTH (vec_to_list v) ∧ LENGTH (vec_to_list v) ≤ Num usize_max - [mk_vec_axiom] Axiom - - [oracles: ] [axioms: mk_vec_axiom] [] - ⊢ ∀l. len l ≤ usize_max ⇒ vec_to_list (mk_vec l) = l - [bind_def] Definition ⊢ ∀x f. diff --git a/tests/hol4/betree/betreeMain_TypesTheory.sig b/tests/hol4/betree/betreeMain_TypesTheory.sig index 5cbe4c6b..a451eae9 100644 --- a/tests/hol4/betree/betreeMain_TypesTheory.sig +++ b/tests/hol4/betree/betreeMain_TypesTheory.sig @@ -4,11 +4,29 @@ sig (* Definitions *) val betree_be_tree_t_TY_DEF : thm + val betree_be_tree_t_betree_be_tree_node_id_cnt : thm + val betree_be_tree_t_betree_be_tree_node_id_cnt_fupd : thm + val betree_be_tree_t_betree_be_tree_params : thm + val betree_be_tree_t_betree_be_tree_params_fupd : thm + val betree_be_tree_t_betree_be_tree_root : thm + val betree_be_tree_t_betree_be_tree_root_fupd : thm val betree_be_tree_t_case_def : thm val betree_be_tree_t_size_def : thm val betree_internal_t_TY_DEF : thm + val betree_internal_t_betree_internal_id : thm + val betree_internal_t_betree_internal_id_fupd : thm + val betree_internal_t_betree_internal_left : thm + val betree_internal_t_betree_internal_left_fupd : thm + val betree_internal_t_betree_internal_pivot : thm + val betree_internal_t_betree_internal_pivot_fupd : thm + val betree_internal_t_betree_internal_right : thm + val betree_internal_t_betree_internal_right_fupd : thm val betree_internal_t_case_def : thm val betree_leaf_t_TY_DEF : thm + val betree_leaf_t_betree_leaf_id : thm + val betree_leaf_t_betree_leaf_id_fupd : thm + val betree_leaf_t_betree_leaf_size : thm + val betree_leaf_t_betree_leaf_size_fupd : thm val betree_leaf_t_case_def : thm val betree_leaf_t_size_def : thm val betree_list_t_TY_DEF : thm @@ -18,41 +36,23 @@ sig val betree_message_t_case_def : thm val betree_message_t_size_def : thm val betree_node_id_counter_t_TY_DEF : thm + val betree_node_id_counter_t_betree_node_id_counter_next_node_id : thm + val betree_node_id_counter_t_betree_node_id_counter_next_node_id_fupd : thm val betree_node_id_counter_t_case_def : thm val betree_node_id_counter_t_size_def : thm val betree_node_t_TY_DEF : thm val betree_node_t_case_def : thm val betree_node_t_size_def : thm val betree_params_t_TY_DEF : thm + val betree_params_t_betree_params_min_flush_size : thm + val betree_params_t_betree_params_min_flush_size_fupd : thm + val betree_params_t_betree_params_split_size : thm + val betree_params_t_betree_params_split_size_fupd : thm val betree_params_t_case_def : thm val betree_params_t_size_def : thm val betree_upsert_fun_state_t_TY_DEF : thm val betree_upsert_fun_state_t_case_def : thm val betree_upsert_fun_state_t_size_def : thm - val recordtype_betree_be_tree_t_seldef_betree_be_tree_node_id_cnt_def : thm - val recordtype_betree_be_tree_t_seldef_betree_be_tree_node_id_cnt_fupd_def : thm - val recordtype_betree_be_tree_t_seldef_betree_be_tree_params_def : thm - val recordtype_betree_be_tree_t_seldef_betree_be_tree_params_fupd_def : thm - val recordtype_betree_be_tree_t_seldef_betree_be_tree_root_def : thm - val recordtype_betree_be_tree_t_seldef_betree_be_tree_root_fupd_def : thm - val recordtype_betree_internal_t_seldef_betree_internal_id_def : thm - val recordtype_betree_internal_t_seldef_betree_internal_id_fupd_def : thm - val recordtype_betree_internal_t_seldef_betree_internal_left_def : thm - val recordtype_betree_internal_t_seldef_betree_internal_left_fupd_def : thm - val recordtype_betree_internal_t_seldef_betree_internal_pivot_def : thm - val recordtype_betree_internal_t_seldef_betree_internal_pivot_fupd_def : thm - val recordtype_betree_internal_t_seldef_betree_internal_right_def : thm - val recordtype_betree_internal_t_seldef_betree_internal_right_fupd_def : thm - val recordtype_betree_leaf_t_seldef_betree_leaf_id_def : thm - val recordtype_betree_leaf_t_seldef_betree_leaf_id_fupd_def : thm - val recordtype_betree_leaf_t_seldef_betree_leaf_size_def : thm - val recordtype_betree_leaf_t_seldef_betree_leaf_size_fupd_def : thm - val recordtype_betree_node_id_counter_t_seldef_betree_node_id_counter_next_node_id_def : thm - val recordtype_betree_node_id_counter_t_seldef_betree_node_id_counter_next_node_id_fupd_def : thm - val recordtype_betree_params_t_seldef_betree_params_min_flush_size_def : thm - val recordtype_betree_params_t_seldef_betree_params_min_flush_size_fupd_def : thm - val recordtype_betree_params_t_seldef_betree_params_split_size_def : thm - val recordtype_betree_params_t_seldef_betree_params_split_size_fupd_def : thm (* Theorems *) val EXISTS_betree_be_tree_t : thm @@ -204,6 +204,38 @@ sig $var$('betree_be_tree_t') a0') ⇒ $var$('betree_be_tree_t') a0') rep + [betree_be_tree_t_betree_be_tree_node_id_cnt] Definition + + ⊢ ∀b b0 b1. + (betree_be_tree_t b b0 b1).betree_be_tree_node_id_cnt = b0 + + [betree_be_tree_t_betree_be_tree_node_id_cnt_fupd] Definition + + ⊢ ∀f b b0 b1. + betree_be_tree_t b b0 b1 with + betree_be_tree_node_id_cnt updated_by f = + betree_be_tree_t b (f b0) b1 + + [betree_be_tree_t_betree_be_tree_params] Definition + + ⊢ ∀b b0 b1. (betree_be_tree_t b b0 b1).betree_be_tree_params = b + + [betree_be_tree_t_betree_be_tree_params_fupd] Definition + + ⊢ ∀f b b0 b1. + betree_be_tree_t b b0 b1 with betree_be_tree_params updated_by f = + betree_be_tree_t (f b) b0 b1 + + [betree_be_tree_t_betree_be_tree_root] Definition + + ⊢ ∀b b0 b1. (betree_be_tree_t b b0 b1).betree_be_tree_root = b1 + + [betree_be_tree_t_betree_be_tree_root_fupd] Definition + + ⊢ ∀f b b0 b1. + betree_be_tree_t b b0 b1 with betree_be_tree_root updated_by f = + betree_be_tree_t b b0 (f b1) + [betree_be_tree_t_case_def] Definition ⊢ ∀a0 a1 a2 f. @@ -246,6 +278,51 @@ sig $var$('betree_internal_t') a1') ⇒ $var$('betree_internal_t') a1') rep + [betree_internal_t_betree_internal_id] Definition + + ⊢ ∀u u0 b b0. (betree_internal_t u u0 b b0).betree_internal_id = u + + [betree_internal_t_betree_internal_id_fupd] Definition + + ⊢ ∀f u u0 b b0. + betree_internal_t u u0 b b0 with betree_internal_id updated_by f = + betree_internal_t (f u) u0 b b0 + + [betree_internal_t_betree_internal_left] Definition + + ⊢ ∀u u0 b b0. (betree_internal_t u u0 b b0).betree_internal_left = b + + [betree_internal_t_betree_internal_left_fupd] Definition + + ⊢ ∀f u u0 b b0. + betree_internal_t u u0 b b0 with + betree_internal_left updated_by f = + betree_internal_t u u0 (f b) b0 + + [betree_internal_t_betree_internal_pivot] Definition + + ⊢ ∀u u0 b b0. + (betree_internal_t u u0 b b0).betree_internal_pivot = u0 + + [betree_internal_t_betree_internal_pivot_fupd] Definition + + ⊢ ∀f u u0 b b0. + betree_internal_t u u0 b b0 with + betree_internal_pivot updated_by f = + betree_internal_t u (f u0) b b0 + + [betree_internal_t_betree_internal_right] Definition + + ⊢ ∀u u0 b b0. + (betree_internal_t u u0 b b0).betree_internal_right = b0 + + [betree_internal_t_betree_internal_right_fupd] Definition + + ⊢ ∀f u u0 b b0. + betree_internal_t u u0 b b0 with + betree_internal_right updated_by f = + betree_internal_t u u0 b (f b0) + [betree_internal_t_case_def] Definition ⊢ ∀a0 a1 a2 a3 f. @@ -267,6 +344,26 @@ sig $var$('betree_leaf_t') a0') ⇒ $var$('betree_leaf_t') a0') rep + [betree_leaf_t_betree_leaf_id] Definition + + ⊢ ∀u u0. (betree_leaf_t u u0).betree_leaf_id = u + + [betree_leaf_t_betree_leaf_id_fupd] Definition + + ⊢ ∀f u u0. + betree_leaf_t u u0 with betree_leaf_id updated_by f = + betree_leaf_t (f u) u0 + + [betree_leaf_t_betree_leaf_size] Definition + + ⊢ ∀u u0. (betree_leaf_t u u0).betree_leaf_size = u0 + + [betree_leaf_t_betree_leaf_size_fupd] Definition + + ⊢ ∀f u u0. + betree_leaf_t u u0 with betree_leaf_size updated_by f = + betree_leaf_t u (f u0) + [betree_leaf_t_case_def] Definition ⊢ ∀a0 a1 f. betree_leaf_t_CASE (betree_leaf_t a0 a1) f = f a0 a1 @@ -355,6 +452,19 @@ sig $var$('betree_node_id_counter_t') a0) ⇒ $var$('betree_node_id_counter_t') a0) rep + [betree_node_id_counter_t_betree_node_id_counter_next_node_id] Definition + + ⊢ ∀u. (betree_node_id_counter_t u). + betree_node_id_counter_next_node_id = + u + + [betree_node_id_counter_t_betree_node_id_counter_next_node_id_fupd] Definition + + ⊢ ∀f u. + betree_node_id_counter_t u with + betree_node_id_counter_next_node_id updated_by f = + betree_node_id_counter_t (f u) + [betree_node_id_counter_t_case_def] Definition ⊢ ∀a f. @@ -424,6 +534,27 @@ sig $var$('betree_params_t') a0') ⇒ $var$('betree_params_t') a0') rep + [betree_params_t_betree_params_min_flush_size] Definition + + ⊢ ∀u u0. (betree_params_t u u0).betree_params_min_flush_size = u + + [betree_params_t_betree_params_min_flush_size_fupd] Definition + + ⊢ ∀f u u0. + betree_params_t u u0 with + betree_params_min_flush_size updated_by f = + betree_params_t (f u) u0 + + [betree_params_t_betree_params_split_size] Definition + + ⊢ ∀u u0. (betree_params_t u u0).betree_params_split_size = u0 + + [betree_params_t_betree_params_split_size_fupd] Definition + + ⊢ ∀f u u0. + betree_params_t u u0 with betree_params_split_size updated_by f = + betree_params_t u (f u0) + [betree_params_t_case_def] Definition ⊢ ∀a0 a1 f. betree_params_t_CASE (betree_params_t a0 a1) f = f a0 a1 @@ -463,137 +594,6 @@ sig ⊢ (∀a. betree_upsert_fun_state_t_size (BetreeUpsertFunStateAdd a) = 1) ∧ ∀a. betree_upsert_fun_state_t_size (BetreeUpsertFunStateSub a) = 1 - [recordtype_betree_be_tree_t_seldef_betree_be_tree_node_id_cnt_def] Definition - - ⊢ ∀b b0 b1. - (betree_be_tree_t b b0 b1).betree_be_tree_node_id_cnt = b0 - - [recordtype_betree_be_tree_t_seldef_betree_be_tree_node_id_cnt_fupd_def] Definition - - ⊢ ∀f b b0 b1. - betree_be_tree_t b b0 b1 with - betree_be_tree_node_id_cnt updated_by f = - betree_be_tree_t b (f b0) b1 - - [recordtype_betree_be_tree_t_seldef_betree_be_tree_params_def] Definition - - ⊢ ∀b b0 b1. (betree_be_tree_t b b0 b1).betree_be_tree_params = b - - [recordtype_betree_be_tree_t_seldef_betree_be_tree_params_fupd_def] Definition - - ⊢ ∀f b b0 b1. - betree_be_tree_t b b0 b1 with betree_be_tree_params updated_by f = - betree_be_tree_t (f b) b0 b1 - - [recordtype_betree_be_tree_t_seldef_betree_be_tree_root_def] Definition - - ⊢ ∀b b0 b1. (betree_be_tree_t b b0 b1).betree_be_tree_root = b1 - - [recordtype_betree_be_tree_t_seldef_betree_be_tree_root_fupd_def] Definition - - ⊢ ∀f b b0 b1. - betree_be_tree_t b b0 b1 with betree_be_tree_root updated_by f = - betree_be_tree_t b b0 (f b1) - - [recordtype_betree_internal_t_seldef_betree_internal_id_def] Definition - - ⊢ ∀u u0 b b0. (betree_internal_t u u0 b b0).betree_internal_id = u - - [recordtype_betree_internal_t_seldef_betree_internal_id_fupd_def] Definition - - ⊢ ∀f u u0 b b0. - betree_internal_t u u0 b b0 with betree_internal_id updated_by f = - betree_internal_t (f u) u0 b b0 - - [recordtype_betree_internal_t_seldef_betree_internal_left_def] Definition - - ⊢ ∀u u0 b b0. (betree_internal_t u u0 b b0).betree_internal_left = b - - [recordtype_betree_internal_t_seldef_betree_internal_left_fupd_def] Definition - - ⊢ ∀f u u0 b b0. - betree_internal_t u u0 b b0 with - betree_internal_left updated_by f = - betree_internal_t u u0 (f b) b0 - - [recordtype_betree_internal_t_seldef_betree_internal_pivot_def] Definition - - ⊢ ∀u u0 b b0. - (betree_internal_t u u0 b b0).betree_internal_pivot = u0 - - [recordtype_betree_internal_t_seldef_betree_internal_pivot_fupd_def] Definition - - ⊢ ∀f u u0 b b0. - betree_internal_t u u0 b b0 with - betree_internal_pivot updated_by f = - betree_internal_t u (f u0) b b0 - - [recordtype_betree_internal_t_seldef_betree_internal_right_def] Definition - - ⊢ ∀u u0 b b0. - (betree_internal_t u u0 b b0).betree_internal_right = b0 - - [recordtype_betree_internal_t_seldef_betree_internal_right_fupd_def] Definition - - ⊢ ∀f u u0 b b0. - betree_internal_t u u0 b b0 with - betree_internal_right updated_by f = - betree_internal_t u u0 b (f b0) - - [recordtype_betree_leaf_t_seldef_betree_leaf_id_def] Definition - - ⊢ ∀u u0. (betree_leaf_t u u0).betree_leaf_id = u - - [recordtype_betree_leaf_t_seldef_betree_leaf_id_fupd_def] Definition - - ⊢ ∀f u u0. - betree_leaf_t u u0 with betree_leaf_id updated_by f = - betree_leaf_t (f u) u0 - - [recordtype_betree_leaf_t_seldef_betree_leaf_size_def] Definition - - ⊢ ∀u u0. (betree_leaf_t u u0).betree_leaf_size = u0 - - [recordtype_betree_leaf_t_seldef_betree_leaf_size_fupd_def] Definition - - ⊢ ∀f u u0. - betree_leaf_t u u0 with betree_leaf_size updated_by f = - betree_leaf_t u (f u0) - - [recordtype_betree_node_id_counter_t_seldef_betree_node_id_counter_next_node_id_def] Definition - - ⊢ ∀u. (betree_node_id_counter_t u). - betree_node_id_counter_next_node_id = - u - - [recordtype_betree_node_id_counter_t_seldef_betree_node_id_counter_next_node_id_fupd_def] Definition - - ⊢ ∀f u. - betree_node_id_counter_t u with - betree_node_id_counter_next_node_id updated_by f = - betree_node_id_counter_t (f u) - - [recordtype_betree_params_t_seldef_betree_params_min_flush_size_def] Definition - - ⊢ ∀u u0. (betree_params_t u u0).betree_params_min_flush_size = u - - [recordtype_betree_params_t_seldef_betree_params_min_flush_size_fupd_def] Definition - - ⊢ ∀f u u0. - betree_params_t u u0 with - betree_params_min_flush_size updated_by f = - betree_params_t (f u) u0 - - [recordtype_betree_params_t_seldef_betree_params_split_size_def] Definition - - ⊢ ∀u u0. (betree_params_t u u0).betree_params_split_size = u0 - - [recordtype_betree_params_t_seldef_betree_params_split_size_fupd_def] Definition - - ⊢ ∀f u u0. - betree_params_t u u0 with betree_params_split_size updated_by f = - betree_params_t u (f u0) - [EXISTS_betree_be_tree_t] Theorem ⊢ ∀P. (∃b. P b) ⇔ 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) ⇔ diff --git a/tests/hol4/misc-constants/constantsTheory.sig b/tests/hol4/misc-constants/constantsTheory.sig index 6148221f..149d7e22 100644 --- a/tests/hol4/misc-constants/constantsTheory.sig +++ b/tests/hol4/misc-constants/constantsTheory.sig @@ -23,6 +23,10 @@ sig val p3_c_def : thm val pair_t_TY_DEF : thm val pair_t_case_def : thm + val pair_t_pair_x : thm + val pair_t_pair_x_fupd : thm + val pair_t_pair_y : thm + val pair_t_pair_y_fupd : thm val pair_t_size_def : thm val q1_body_def : thm val q1_c_def : thm @@ -30,12 +34,6 @@ sig val q2_c_def : thm val q3_body_def : thm val q3_c_def : thm - val recordtype_pair_t_seldef_pair_x_def : thm - val recordtype_pair_t_seldef_pair_x_fupd_def : thm - val recordtype_pair_t_seldef_pair_y_def : thm - val recordtype_pair_t_seldef_pair_y_fupd_def : thm - val recordtype_wrap_t_seldef_wrap_val_def : thm - val recordtype_wrap_t_seldef_wrap_val_fupd_def : thm val s1_body_def : thm val s1_c_def : thm val s2_body_def : thm @@ -49,6 +47,8 @@ sig val wrap_t_TY_DEF : thm val wrap_t_case_def : thm val wrap_t_size_def : thm + val wrap_t_wrap_val : thm + val wrap_t_wrap_val_fupd : thm val x0_body_def : thm val x0_c_def : thm val x1_body_def : thm @@ -198,6 +198,22 @@ sig ⊢ ∀a0 a1 f. pair_t_CASE (pair_t a0 a1) f = f a0 a1 + [pair_t_pair_x] Definition + + ⊢ ∀t t0. (pair_t t t0).pair_x = t + + [pair_t_pair_x_fupd] Definition + + ⊢ ∀f t t0. pair_t t t0 with pair_x updated_by f = pair_t (f t) t0 + + [pair_t_pair_y] Definition + + ⊢ ∀t t0. (pair_t t t0).pair_y = t0 + + [pair_t_pair_y_fupd] Definition + + ⊢ ∀f t t0. pair_t t t0 with pair_y updated_by f = pair_t t (f t0) + [pair_t_size_def] Definition ⊢ ∀f f1 a0 a1. pair_t_size f f1 (pair_t a0 a1) = 1 + (f a0 + f1 a1) @@ -226,30 +242,6 @@ sig ⊢ q3_c = get_return_value q3_body - [recordtype_pair_t_seldef_pair_x_def] Definition - - ⊢ ∀t t0. (pair_t t t0).pair_x = t - - [recordtype_pair_t_seldef_pair_x_fupd_def] Definition - - ⊢ ∀f t t0. pair_t t t0 with pair_x updated_by f = pair_t (f t) t0 - - [recordtype_pair_t_seldef_pair_y_def] Definition - - ⊢ ∀t t0. (pair_t t t0).pair_y = t0 - - [recordtype_pair_t_seldef_pair_y_fupd_def] Definition - - ⊢ ∀f t t0. pair_t t t0 with pair_y updated_by f = pair_t t (f t0) - - [recordtype_wrap_t_seldef_wrap_val_def] Definition - - ⊢ ∀t. (wrap_t t).wrap_val = t - - [recordtype_wrap_t_seldef_wrap_val_fupd_def] Definition - - ⊢ ∀f t. wrap_t t with wrap_val updated_by f = wrap_t (f t) - [s1_body_def] Definition ⊢ s1_body = Return (int_to_u32 6) @@ -311,6 +303,14 @@ sig ⊢ ∀f a. wrap_t_size f (wrap_t a) = 1 + f a + [wrap_t_wrap_val] Definition + + ⊢ ∀t. (wrap_t t).wrap_val = t + + [wrap_t_wrap_val_fupd] Definition + + ⊢ ∀f t. wrap_t t with wrap_val updated_by f = wrap_t (f t) + [x0_body_def] Definition ⊢ x0_body = Return (int_to_u32 0) diff --git a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig index 82c842be..c0ff4e09 100644 --- a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig +++ b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig @@ -53,15 +53,11 @@ sig val one_t_size_def : thm val pair_t_TY_DEF : thm val pair_t_case_def : thm + val pair_t_pair_x : thm + val pair_t_pair_x_fupd : thm + val pair_t_pair_y : thm + val pair_t_pair_y_fupd : thm val pair_t_size_def : thm - val recordtype_pair_t_seldef_pair_x_def : thm - val recordtype_pair_t_seldef_pair_x_fupd_def : thm - val recordtype_pair_t_seldef_pair_y_def : thm - val recordtype_pair_t_seldef_pair_y_fupd_def : thm - val recordtype_struct_with_pair_t_seldef_struct_with_pair_p_def : thm - val recordtype_struct_with_pair_t_seldef_struct_with_pair_p_fupd_def : thm - val recordtype_struct_with_tuple_t_seldef_struct_with_tuple_p_def : thm - val recordtype_struct_with_tuple_t_seldef_struct_with_tuple_p_fupd_def : thm val refs_test1_fwd_def : thm val refs_test2_fwd_def : thm val rem_test_fwd_def : thm @@ -69,9 +65,13 @@ sig val struct_with_pair_t_TY_DEF : thm val struct_with_pair_t_case_def : thm val struct_with_pair_t_size_def : thm + val struct_with_pair_t_struct_with_pair_p : thm + val struct_with_pair_t_struct_with_pair_p_fupd : thm val struct_with_tuple_t_TY_DEF : thm val struct_with_tuple_t_case_def : thm val struct_with_tuple_t_size_def : thm + val struct_with_tuple_t_struct_with_tuple_p : thm + val struct_with_tuple_t_struct_with_tuple_p_fupd : thm val subs_test_fwd_def : thm val sum_t_TY_DEF : thm val sum_t_case_def : thm @@ -577,45 +577,25 @@ sig ⊢ ∀a0 a1 f. pair_t_CASE (pair_t a0 a1) f = f a0 a1 - [pair_t_size_def] Definition - - ⊢ ∀f f1 a0 a1. pair_t_size f f1 (pair_t a0 a1) = 1 + (f a0 + f1 a1) - - [recordtype_pair_t_seldef_pair_x_def] Definition + [pair_t_pair_x] Definition ⊢ ∀t t0. (pair_t t t0).pair_x = t - [recordtype_pair_t_seldef_pair_x_fupd_def] Definition + [pair_t_pair_x_fupd] Definition ⊢ ∀f t t0. pair_t t t0 with pair_x updated_by f = pair_t (f t) t0 - [recordtype_pair_t_seldef_pair_y_def] Definition + [pair_t_pair_y] Definition ⊢ ∀t t0. (pair_t t t0).pair_y = t0 - [recordtype_pair_t_seldef_pair_y_fupd_def] Definition + [pair_t_pair_y_fupd] Definition ⊢ ∀f t t0. pair_t t t0 with pair_y updated_by f = pair_t t (f t0) - [recordtype_struct_with_pair_t_seldef_struct_with_pair_p_def] Definition - - ⊢ ∀p. (struct_with_pair_t p).struct_with_pair_p = p - - [recordtype_struct_with_pair_t_seldef_struct_with_pair_p_fupd_def] Definition - - ⊢ ∀f p. - struct_with_pair_t p with struct_with_pair_p updated_by f = - struct_with_pair_t (f p) - - [recordtype_struct_with_tuple_t_seldef_struct_with_tuple_p_def] Definition - - ⊢ ∀p. (struct_with_tuple_t p).struct_with_tuple_p = p - - [recordtype_struct_with_tuple_t_seldef_struct_with_tuple_p_fupd_def] Definition + [pair_t_size_def] Definition - ⊢ ∀f p. - struct_with_tuple_t p with struct_with_tuple_p updated_by f = - struct_with_tuple_t (f p) + ⊢ ∀f f1 a0 a1. pair_t_size f f1 (pair_t a0 a1) = 1 + (f a0 + f1 a1) [refs_test1_fwd_def] Definition @@ -665,6 +645,16 @@ sig struct_with_pair_t_size f f1 (struct_with_pair_t a) = 1 + pair_t_size f f1 a + [struct_with_pair_t_struct_with_pair_p] Definition + + ⊢ ∀p. (struct_with_pair_t p).struct_with_pair_p = p + + [struct_with_pair_t_struct_with_pair_p_fupd] Definition + + ⊢ ∀f p. + struct_with_pair_t p with struct_with_pair_p updated_by f = + struct_with_pair_t (f p) + [struct_with_tuple_t_TY_DEF] Definition ⊢ ∃rep. @@ -688,6 +678,16 @@ sig struct_with_tuple_t_size f f1 (struct_with_tuple_t a) = 1 + pair_size f f1 a + [struct_with_tuple_t_struct_with_tuple_p] Definition + + ⊢ ∀p. (struct_with_tuple_t p).struct_with_tuple_p = p + + [struct_with_tuple_t_struct_with_tuple_p_fupd] Definition + + ⊢ ∀f p. + struct_with_tuple_t p with struct_with_tuple_p updated_by f = + struct_with_tuple_t (f p) + [subs_test_fwd_def] Definition ⊢ ∀x y. subs_test_fwd x y = u32_sub x y |