diff options
Diffstat (limited to 'tests/hol4/misc-no_nested_borrows')
| -rw-r--r-- | tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig | 68 |
1 files changed, 34 insertions, 34 deletions
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 |