summaryrefslogtreecommitdiff
path: root/tests/hol4/misc-no_nested_borrows
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hol4/misc-no_nested_borrows')
-rw-r--r--tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig68
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