diff options
Diffstat (limited to 'tests/hol4/betree')
| -rw-r--r-- | tests/hol4/betree/betreeMain_FunsScript.sml | 516 | ||||
| -rw-r--r-- | tests/hol4/betree/betreeMain_TypesScript.sml | 12 | ||||
| -rw-r--r-- | tests/hol4/betree/betreeMain_TypesTheory.sig | 140 |
3 files changed, 334 insertions, 334 deletions
diff --git a/tests/hol4/betree/betreeMain_FunsScript.sml b/tests/hol4/betree/betreeMain_FunsScript.sml index 03ff2671..b53c7b8d 100644 --- a/tests/hol4/betree/betreeMain_FunsScript.sml +++ b/tests/hol4/betree/betreeMain_FunsScript.sml @@ -279,22 +279,6 @@ val betree_leaf_split_back_def = Define ‘ od ’ -val [betree_node_lookup_in_bindings_fwd_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *) - betree_node_lookup_in_bindings_fwd - (key : u64) (bindings : (u64 # u64) betree_list_t) : u64 option result = - (case bindings of - | BetreeListCons hd tl => - let (i, i0) = hd in - if i = key - then Return (SOME i0) - else - if u64_gt i key - then Return NONE - else betree_node_lookup_in_bindings_fwd key tl - | BetreeListNil => Return NONE) -’ - val [betree_node_lookup_first_message_for_key_fwd_def] = DefineDiv ‘ (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *) betree_node_lookup_first_message_for_key_fwd @@ -396,7 +380,51 @@ val [betree_node_apply_upserts_back_def] = DefineDiv ‘ od ’ -val [betree_node_lookup_fwd_def, betree_node_lookup_back_def, betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_children_back_def] = DefineDiv ‘ +val [betree_node_lookup_in_bindings_fwd_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *) + betree_node_lookup_in_bindings_fwd + (key : u64) (bindings : (u64 # u64) betree_list_t) : u64 option result = + (case bindings of + | BetreeListCons hd tl => + let (i, i0) = hd in + if i = key + then Return (SOME i0) + else + if u64_gt i key + then Return NONE + else betree_node_lookup_in_bindings_fwd key tl + | BetreeListNil => Return NONE) +’ + +val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_children_back_def, betree_node_lookup_fwd_def, betree_node_lookup_back_def] = DefineDiv ‘ + (** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *) + (betree_internal_lookup_in_children_fwd + (self : betree_internal_t) (key : u64) (st : state) : + (state # u64 option) result + = + if u64_lt key self.betree_internal_pivot + then betree_node_lookup_fwd self.betree_internal_left key st + else betree_node_lookup_fwd self.betree_internal_right key st) + /\ + + (** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *) + (betree_internal_lookup_in_children_back + (self : betree_internal_t) (key : u64) (st : state) : + betree_internal_t result + = + if u64_lt key self.betree_internal_pivot + then ( + do + n <- betree_node_lookup_back self.betree_internal_left key st; + Return (self with <| betree_internal_left := n |>) + od) + else ( + do + n <- betree_node_lookup_back self.betree_internal_right key st; + Return (self with <| betree_internal_right := n |>) + od)) + /\ + (** [betree_main::betree::Node::{5}::lookup]: forward function *) (betree_node_lookup_fwd (self : betree_node_t) (key : u64) (st : state) : @@ -468,8 +496,8 @@ val [betree_node_lookup_fwd_def, betree_node_lookup_back_def, betree_internal_lo /\ (** [betree_main::betree::Node::{5}::lookup]: backward function 0 *) - (betree_node_lookup_back - (self : betree_node_t) (key : u64) (st : state) : betree_node_t result = + betree_node_lookup_back + (self : betree_node_t) (key : u64) (st : state) : betree_node_t result = (case self of | BetreeNodeInternal node => do @@ -532,142 +560,7 @@ val [betree_node_lookup_fwd_def, betree_node_lookup_back_def, betree_internal_lo (_, bindings) <- betree_load_leaf_node_fwd node.betree_leaf_id st; _ <- betree_node_lookup_in_bindings_fwd key bindings; Return (BetreeNodeLeaf node) - od)) - /\ - - (** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *) - (betree_internal_lookup_in_children_fwd - (self : betree_internal_t) (key : u64) (st : state) : - (state # u64 option) result - = - if u64_lt key self.betree_internal_pivot - then betree_node_lookup_fwd self.betree_internal_left key st - else betree_node_lookup_fwd self.betree_internal_right key st) - /\ - - (** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *) - betree_internal_lookup_in_children_back - (self : betree_internal_t) (key : u64) (st : state) : - betree_internal_t result - = - if u64_lt key self.betree_internal_pivot - then ( - do - n <- betree_node_lookup_back self.betree_internal_left key st; - Return (self with <| betree_internal_left := n |>) od) - else ( - do - n <- betree_node_lookup_back self.betree_internal_right key st; - Return (self with <| betree_internal_right := n |>) - od) -’ - -val [betree_node_lookup_mut_in_bindings_fwd_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *) - betree_node_lookup_mut_in_bindings_fwd - (key : u64) (bindings : (u64 # u64) betree_list_t) : - (u64 # u64) betree_list_t result - = - (case bindings of - | BetreeListCons hd tl => - let (i, i0) = hd in - if u64_ge i key - then Return (BetreeListCons (i, i0) tl) - else betree_node_lookup_mut_in_bindings_fwd key tl - | BetreeListNil => Return BetreeListNil) -’ - -val [betree_node_lookup_mut_in_bindings_back_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *) - betree_node_lookup_mut_in_bindings_back - (key : u64) (bindings : (u64 # u64) betree_list_t) - (ret : (u64 # u64) betree_list_t) : - (u64 # u64) betree_list_t result - = - (case bindings of - | BetreeListCons hd tl => - let (i, i0) = hd in - if u64_ge i key - then Return ret - else ( - do - tl0 <- betree_node_lookup_mut_in_bindings_back key tl ret; - Return (BetreeListCons (i, i0) tl0) - od) - | BetreeListNil => Return ret) -’ - -val betree_node_apply_to_leaf_fwd_back_def = Define ‘ - (** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) - betree_node_apply_to_leaf_fwd_back - (bindings : (u64 # u64) betree_list_t) (key : u64) - (new_msg : betree_message_t) : - (u64 # u64) betree_list_t result - = - do - bindings0 <- betree_node_lookup_mut_in_bindings_fwd key bindings; - b <- betree_list_head_has_key_fwd bindings0 key; - if b - then ( - do - hd <- betree_list_pop_front_fwd bindings0; - (case new_msg of - | BetreeMessageInsert v => - do - bindings1 <- betree_list_pop_front_back bindings0; - bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v); - betree_node_lookup_mut_in_bindings_back key bindings bindings2 - od - | BetreeMessageDelete => - do - bindings1 <- betree_list_pop_front_back bindings0; - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - od - | BetreeMessageUpsert s => - let (_, i) = hd in - do - v <- betree_upsert_update_fwd (SOME i) s; - bindings1 <- betree_list_pop_front_back bindings0; - bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v); - betree_node_lookup_mut_in_bindings_back key bindings bindings2 - od) - od) - else - (case new_msg of - | BetreeMessageInsert v => - do - bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v); - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - od - | BetreeMessageDelete => - betree_node_lookup_mut_in_bindings_back key bindings bindings0 - | BetreeMessageUpsert s => - do - v <- betree_upsert_update_fwd NONE s; - bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v); - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - od) - od -’ - -val [betree_node_apply_messages_to_leaf_fwd_back_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) - betree_node_apply_messages_to_leaf_fwd_back - (bindings : (u64 # u64) betree_list_t) - (new_msgs : (u64 # betree_message_t) betree_list_t) : - (u64 # u64) betree_list_t result - = - (case new_msgs of - | BetreeListCons new_msg new_msgs_tl => - let (i, m) = new_msg in - do - bindings0 <- betree_node_apply_to_leaf_fwd_back bindings i m; - betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl - od - | BetreeListNil => Return bindings) ’ val [betree_node_filter_messages_for_key_fwd_back_def] = DefineDiv ‘ @@ -811,7 +704,211 @@ val [betree_node_apply_messages_to_internal_fwd_back_def] = DefineDiv ‘ | BetreeListNil => Return msgs) ’ -val [betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def, betree_internal_flush_fwd_def, betree_internal_flush_back_def] = DefineDiv ‘ +val [betree_node_lookup_mut_in_bindings_fwd_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *) + betree_node_lookup_mut_in_bindings_fwd + (key : u64) (bindings : (u64 # u64) betree_list_t) : + (u64 # u64) betree_list_t result + = + (case bindings of + | BetreeListCons hd tl => + let (i, i0) = hd in + if u64_ge i key + then Return (BetreeListCons (i, i0) tl) + else betree_node_lookup_mut_in_bindings_fwd key tl + | BetreeListNil => Return BetreeListNil) +’ + +val [betree_node_lookup_mut_in_bindings_back_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *) + betree_node_lookup_mut_in_bindings_back + (key : u64) (bindings : (u64 # u64) betree_list_t) + (ret : (u64 # u64) betree_list_t) : + (u64 # u64) betree_list_t result + = + (case bindings of + | BetreeListCons hd tl => + let (i, i0) = hd in + if u64_ge i key + then Return ret + else ( + do + tl0 <- betree_node_lookup_mut_in_bindings_back key tl ret; + Return (BetreeListCons (i, i0) tl0) + od) + | BetreeListNil => Return ret) +’ + +val betree_node_apply_to_leaf_fwd_back_def = Define ‘ + (** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) + betree_node_apply_to_leaf_fwd_back + (bindings : (u64 # u64) betree_list_t) (key : u64) + (new_msg : betree_message_t) : + (u64 # u64) betree_list_t result + = + do + bindings0 <- betree_node_lookup_mut_in_bindings_fwd key bindings; + b <- betree_list_head_has_key_fwd bindings0 key; + if b + then ( + do + hd <- betree_list_pop_front_fwd bindings0; + (case new_msg of + | BetreeMessageInsert v => + do + bindings1 <- betree_list_pop_front_back bindings0; + bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v); + betree_node_lookup_mut_in_bindings_back key bindings bindings2 + od + | BetreeMessageDelete => + do + bindings1 <- betree_list_pop_front_back bindings0; + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + od + | BetreeMessageUpsert s => + let (_, i) = hd in + do + v <- betree_upsert_update_fwd (SOME i) s; + bindings1 <- betree_list_pop_front_back bindings0; + bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v); + betree_node_lookup_mut_in_bindings_back key bindings bindings2 + od) + od) + else + (case new_msg of + | BetreeMessageInsert v => + do + bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v); + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + od + | BetreeMessageDelete => + betree_node_lookup_mut_in_bindings_back key bindings bindings0 + | BetreeMessageUpsert s => + do + v <- betree_upsert_update_fwd NONE s; + bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v); + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + od) + od +’ + +val [betree_node_apply_messages_to_leaf_fwd_back_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) + betree_node_apply_messages_to_leaf_fwd_back + (bindings : (u64 # u64) betree_list_t) + (new_msgs : (u64 # betree_message_t) betree_list_t) : + (u64 # u64) betree_list_t result + = + (case new_msgs of + | BetreeListCons new_msg new_msgs_tl => + let (i, m) = new_msg in + do + bindings0 <- betree_node_apply_to_leaf_fwd_back bindings i m; + betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl + od + | BetreeListNil => Return bindings) +’ + +val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def] = DefineDiv ‘ + (** [betree_main::betree::Internal::{4}::flush]: forward function *) + (betree_internal_flush_fwd + (self : betree_internal_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (content : (u64 # betree_message_t) betree_list_t) (st : state) : + (state # (u64 # betree_message_t) betree_list_t) result + = + do + p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot; + let (msgs_left, msgs_right) = p in + do + len_left <- betree_list_len_fwd msgs_left; + if u64_ge len_left params.betree_params_min_flush_size + then ( + do + (st0, _) <- + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st; + (_, node_id_cnt0) <- + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st; + len_right <- betree_list_len_fwd msgs_right; + if u64_ge len_right params.betree_params_min_flush_size + then ( + do + (st1, _) <- + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt0 msgs_right st0; + _ <- + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt0 msgs_right st0; + Return (st1, BetreeListNil) + od) + else Return (st0, msgs_right) + od) + else ( + do + (st0, _) <- + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt msgs_right st; + _ <- + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st; + Return (st0, msgs_left) + od) + od + od) + /\ + + (** [betree_main::betree::Internal::{4}::flush]: backward function 0 *) + (betree_internal_flush_back + (self : betree_internal_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (content : (u64 # betree_message_t) betree_list_t) (st : state) : + (betree_internal_t # betree_node_id_counter_t) result + = + do + p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot; + let (msgs_left, msgs_right) = p in + do + len_left <- betree_list_len_fwd msgs_left; + if u64_ge len_left params.betree_params_min_flush_size + then ( + do + (st0, _) <- + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st; + (n, node_id_cnt0) <- + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st; + len_right <- betree_list_len_fwd msgs_right; + if u64_ge len_right params.betree_params_min_flush_size + then ( + do + (n0, node_id_cnt1) <- + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt0 msgs_right st0; + Return + (self + with + <| + betree_internal_left := n; betree_internal_right := n0 + |>, node_id_cnt1) + od) + else Return (self with <| betree_internal_left := n |>, node_id_cnt0) + od) + else ( + do + (n, node_id_cnt0) <- + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st; + Return (self with <| betree_internal_right := n |>, node_id_cnt0) + od) + od + od) + /\ + (** [betree_main::betree::Node::{5}::apply_messages]: forward function *) (betree_node_apply_messages_fwd (self : betree_node_t) (params : betree_params_t) @@ -868,12 +965,12 @@ val [betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def, be /\ (** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *) - (betree_node_apply_messages_back - (self : betree_node_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) - (msgs : (u64 # betree_message_t) betree_list_t) (st : state) : - (betree_node_t # betree_node_id_counter_t) result - = + betree_node_apply_messages_back + (self : betree_node_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (msgs : (u64 # betree_message_t) betree_list_t) (st : state) : + (betree_node_t # betree_node_id_counter_t) result + = (case self of | BetreeNodeInternal node => do @@ -921,104 +1018,7 @@ val [betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def, be Return (BetreeNodeLeaf (node with <| betree_leaf_size := len |>), node_id_cnt) od) - od)) - /\ - - (** [betree_main::betree::Internal::{4}::flush]: forward function *) - (betree_internal_flush_fwd - (self : betree_internal_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) - (content : (u64 # betree_message_t) betree_list_t) (st : state) : - (state # (u64 # betree_message_t) betree_list_t) result - = - do - p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot; - let (msgs_left, msgs_right) = p in - do - len_left <- betree_list_len_fwd msgs_left; - if u64_ge len_left params.betree_params_min_flush_size - then ( - do - (st0, _) <- - betree_node_apply_messages_fwd self.betree_internal_left params - node_id_cnt msgs_left st; - (_, node_id_cnt0) <- - betree_node_apply_messages_back self.betree_internal_left params - node_id_cnt msgs_left st; - len_right <- betree_list_len_fwd msgs_right; - if u64_ge len_right params.betree_params_min_flush_size - then ( - do - (st1, _) <- - betree_node_apply_messages_fwd self.betree_internal_right params - node_id_cnt0 msgs_right st0; - _ <- - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt0 msgs_right st0; - Return (st1, BetreeListNil) - od) - else Return (st0, msgs_right) - od) - else ( - do - (st0, _) <- - betree_node_apply_messages_fwd self.betree_internal_right params - node_id_cnt msgs_right st; - _ <- - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt msgs_right st; - Return (st0, msgs_left) od) - od - od) - /\ - - (** [betree_main::betree::Internal::{4}::flush]: backward function 0 *) - betree_internal_flush_back - (self : betree_internal_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) - (content : (u64 # betree_message_t) betree_list_t) (st : state) : - (betree_internal_t # betree_node_id_counter_t) result - = - do - p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot; - let (msgs_left, msgs_right) = p in - do - len_left <- betree_list_len_fwd msgs_left; - if u64_ge len_left params.betree_params_min_flush_size - then ( - do - (st0, _) <- - betree_node_apply_messages_fwd self.betree_internal_left params - node_id_cnt msgs_left st; - (n, node_id_cnt0) <- - betree_node_apply_messages_back self.betree_internal_left params - node_id_cnt msgs_left st; - len_right <- betree_list_len_fwd msgs_right; - if u64_ge len_right params.betree_params_min_flush_size - then ( - do - (n0, node_id_cnt1) <- - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt0 msgs_right st0; - Return - (self - with - <| - betree_internal_left := n; betree_internal_right := n0 - |>, node_id_cnt1) - od) - else Return (self with <| betree_internal_left := n |>, node_id_cnt0) - od) - else ( - do - (n, node_id_cnt0) <- - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt msgs_right st; - Return (self with <| betree_internal_right := n |>, node_id_cnt0) - od) - od - od ’ val betree_node_apply_fwd_def = Define ‘ diff --git a/tests/hol4/betree/betreeMain_TypesScript.sml b/tests/hol4/betree/betreeMain_TypesScript.sml index c43421c2..779f6abb 100644 --- a/tests/hol4/betree/betreeMain_TypesScript.sml +++ b/tests/hol4/betree/betreeMain_TypesScript.sml @@ -31,12 +31,6 @@ Datatype: End Datatype: - (** [betree_main::betree::Node] *) - betree_node_t = - | BetreeNodeInternal betree_internal_t - | BetreeNodeLeaf betree_leaf_t - ; - (** [betree_main::betree::Internal] *) betree_internal_t = <| @@ -45,6 +39,12 @@ Datatype: betree_internal_left : betree_node_t; betree_internal_right : betree_node_t; |> + ; + + (** [betree_main::betree::Node] *) + betree_node_t = + | BetreeNodeInternal betree_internal_t + | BetreeNodeLeaf betree_leaf_t End Datatype: diff --git a/tests/hol4/betree/betreeMain_TypesTheory.sig b/tests/hol4/betree/betreeMain_TypesTheory.sig index a451eae9..cffe6afb 100644 --- a/tests/hol4/betree/betreeMain_TypesTheory.sig +++ b/tests/hol4/betree/betreeMain_TypesTheory.sig @@ -22,6 +22,7 @@ sig 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_internal_t_size_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 @@ -42,7 +43,6 @@ sig 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 @@ -177,11 +177,11 @@ sig val betree_upsert_fun_state_t_induction : thm val betree_upsert_fun_state_t_nchotomy : thm val datatype_betree_be_tree_t : thm + val datatype_betree_internal_t : thm val datatype_betree_leaf_t : thm val datatype_betree_list_t : thm val datatype_betree_message_t : thm val datatype_betree_node_id_counter_t : thm - val datatype_betree_node_t : thm val datatype_betree_params_t : thm val datatype_betree_upsert_fun_state_t : thm @@ -253,30 +253,30 @@ sig ⊢ ∃rep. TYPE_DEFINITION - (λa1'. - ∀ $var$('betree_node_t') $var$('betree_internal_t'). + (λa0'. + ∀ $var$('betree_internal_t') $var$('betree_node_t'). (∀a0'. - (∃a. a0' = - (λa. - ind_type$CONSTR 0 (ARB,ARB,ARB) - (ind_type$FCONS a (λn. ind_type$BOTTOM))) - a ∧ $var$('betree_internal_t') a) ∨ - (∃a. a0' = - (λa. - ind_type$CONSTR (SUC 0) (a,ARB,ARB) - (λn. ind_type$BOTTOM)) a) ⇒ - $var$('betree_node_t') a0') ∧ - (∀a1'. (∃a0 a1 a2 a3. - a1' = + a0' = (λa0 a1 a2 a3. - ind_type$CONSTR (SUC (SUC 0)) (ARB,a0,a1) + ind_type$CONSTR 0 (a0,a1,ARB) (ind_type$FCONS a2 (ind_type$FCONS a3 (λn. ind_type$BOTTOM)))) a0 a1 a2 a3 ∧ $var$('betree_node_t') a2 ∧ $var$('betree_node_t') a3) ⇒ - $var$('betree_internal_t') a1') ⇒ - $var$('betree_internal_t') a1') rep + $var$('betree_internal_t') a0') ∧ + (∀a1'. + (∃a. a1' = + (λa. + ind_type$CONSTR (SUC 0) (ARB,ARB,ARB) + (ind_type$FCONS a (λn. ind_type$BOTTOM))) + a ∧ $var$('betree_internal_t') a) ∨ + (∃a. a1' = + (λa. + ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB,a) + (λn. ind_type$BOTTOM)) a) ⇒ + $var$('betree_node_t') a1') ⇒ + $var$('betree_internal_t') a0') rep [betree_internal_t_betree_internal_id] Definition @@ -329,6 +329,16 @@ sig betree_internal_t_CASE (betree_internal_t a0 a1 a2 a3) f = f a0 a1 a2 a3 + [betree_internal_t_size_def] Definition + + ⊢ (∀a0 a1 a2 a3. + betree_internal_t_size (betree_internal_t a0 a1 a2 a3) = + 1 + (betree_node_t_size a2 + betree_node_t_size a3)) ∧ + (∀a. betree_node_t_size (BetreeNodeInternal a) = + 1 + betree_internal_t_size a) ∧ + ∀a. betree_node_t_size (BetreeNodeLeaf a) = + 1 + betree_leaf_t_size a + [betree_leaf_t_TY_DEF] Definition ⊢ ∃rep. @@ -479,46 +489,36 @@ sig ⊢ ∃rep. TYPE_DEFINITION - (λa0'. - ∀ $var$('betree_node_t') $var$('betree_internal_t'). + (λa1'. + ∀ $var$('betree_internal_t') $var$('betree_node_t'). (∀a0'. - (∃a. a0' = - (λa. - ind_type$CONSTR 0 (ARB,ARB,ARB) - (ind_type$FCONS a (λn. ind_type$BOTTOM))) - a ∧ $var$('betree_internal_t') a) ∨ - (∃a. a0' = - (λa. - ind_type$CONSTR (SUC 0) (a,ARB,ARB) - (λn. ind_type$BOTTOM)) a) ⇒ - $var$('betree_node_t') a0') ∧ - (∀a1'. (∃a0 a1 a2 a3. - a1' = + a0' = (λa0 a1 a2 a3. - ind_type$CONSTR (SUC (SUC 0)) (ARB,a0,a1) + ind_type$CONSTR 0 (a0,a1,ARB) (ind_type$FCONS a2 (ind_type$FCONS a3 (λn. ind_type$BOTTOM)))) a0 a1 a2 a3 ∧ $var$('betree_node_t') a2 ∧ $var$('betree_node_t') a3) ⇒ - $var$('betree_internal_t') a1') ⇒ - $var$('betree_node_t') a0') rep + $var$('betree_internal_t') a0') ∧ + (∀a1'. + (∃a. a1' = + (λa. + ind_type$CONSTR (SUC 0) (ARB,ARB,ARB) + (ind_type$FCONS a (λn. ind_type$BOTTOM))) + a ∧ $var$('betree_internal_t') a) ∨ + (∃a. a1' = + (λa. + ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB,a) + (λn. ind_type$BOTTOM)) a) ⇒ + $var$('betree_node_t') a1') ⇒ + $var$('betree_node_t') a1') rep [betree_node_t_case_def] Definition ⊢ (∀a f f1. betree_node_t_CASE (BetreeNodeInternal a) f f1 = f a) ∧ ∀a f f1. betree_node_t_CASE (BetreeNodeLeaf a) f f1 = f1 a - [betree_node_t_size_def] Definition - - ⊢ (∀a. betree_node_t_size (BetreeNodeInternal a) = - 1 + betree_internal_t_size a) ∧ - (∀a. betree_node_t_size (BetreeNodeLeaf a) = - 1 + betree_leaf_t_size a) ∧ - ∀a0 a1 a2 a3. - betree_internal_t_size (betree_internal_t a0 a1 a2 a3) = - 1 + (betree_node_t_size a2 + betree_node_t_size a3) - [betree_params_t_TY_DEF] Definition ⊢ ∃rep. @@ -883,11 +883,11 @@ sig [betree_internal_t_Axiom] Theorem ⊢ ∀f0 f1 f2. ∃fn0 fn1. - (∀a. fn0 (BetreeNodeInternal a) = f0 a (fn1 a)) ∧ - (∀a. fn0 (BetreeNodeLeaf a) = f1 a) ∧ - ∀a0 a1 a2 a3. - fn1 (betree_internal_t a0 a1 a2 a3) = - f2 a0 a1 a2 a3 (fn0 a2) (fn0 a3) + (∀a0 a1 a2 a3. + fn0 (betree_internal_t a0 a1 a2 a3) = + f0 a0 a1 a2 a3 (fn1 a2) (fn1 a3)) ∧ + (∀a. fn1 (BetreeNodeInternal a) = f1 a (fn0 a)) ∧ + ∀a. fn1 (BetreeNodeLeaf a) = f2 a [betree_internal_t_accessors] Theorem @@ -1130,9 +1130,9 @@ sig [betree_internal_t_induction] Theorem ⊢ ∀P0 P1. - (∀b. P1 b ⇒ P0 (BetreeNodeInternal b)) ∧ - (∀b. P0 (BetreeNodeLeaf b)) ∧ - (∀b b0. P0 b ∧ P0 b0 ⇒ ∀u u0. P1 (betree_internal_t u0 u b b0)) ⇒ + (∀b b0. P1 b ∧ P1 b0 ⇒ ∀u u0. P0 (betree_internal_t u0 u b b0)) ∧ + (∀b. P0 b ⇒ P1 (BetreeNodeInternal b)) ∧ + (∀b. P1 (BetreeNodeLeaf b)) ⇒ (∀b. P0 b) ∧ ∀b. P1 b [betree_internal_t_literal_11] Theorem @@ -1472,11 +1472,11 @@ sig [betree_node_t_Axiom] Theorem ⊢ ∀f0 f1 f2. ∃fn0 fn1. - (∀a. fn0 (BetreeNodeInternal a) = f0 a (fn1 a)) ∧ - (∀a. fn0 (BetreeNodeLeaf a) = f1 a) ∧ - ∀a0 a1 a2 a3. - fn1 (betree_internal_t a0 a1 a2 a3) = - f2 a0 a1 a2 a3 (fn0 a2) (fn0 a3) + (∀a0 a1 a2 a3. + fn0 (betree_internal_t a0 a1 a2 a3) = + f0 a0 a1 a2 a3 (fn1 a2) (fn1 a3)) ∧ + (∀a. fn1 (BetreeNodeInternal a) = f1 a (fn0 a)) ∧ + ∀a. fn1 (BetreeNodeLeaf a) = f2 a [betree_node_t_case_cong] Theorem @@ -1498,9 +1498,9 @@ sig [betree_node_t_induction] Theorem ⊢ ∀P0 P1. - (∀b. P1 b ⇒ P0 (BetreeNodeInternal b)) ∧ - (∀b. P0 (BetreeNodeLeaf b)) ∧ - (∀b b0. P0 b ∧ P0 b0 ⇒ ∀u u0. P1 (betree_internal_t u0 u b b0)) ⇒ + (∀b b0. P1 b ∧ P1 b0 ⇒ ∀u u0. P0 (betree_internal_t u0 u b b0)) ∧ + (∀b. P0 b ⇒ P1 (BetreeNodeInternal b)) ∧ + (∀b. P1 (BetreeNodeLeaf b)) ⇒ (∀b. P0 b) ∧ ∀b. P1 b [betree_node_t_nchotomy] Theorem @@ -1706,6 +1706,14 @@ sig (record betree_be_tree_t betree_be_tree_params betree_be_tree_node_id_cnt betree_be_tree_root) + [datatype_betree_internal_t] Theorem + + ⊢ DATATYPE + (record betree_internal_t betree_internal_id + betree_internal_pivot betree_internal_left + betree_internal_right ∧ + betree_node_t BetreeNodeInternal BetreeNodeLeaf) + [datatype_betree_leaf_t] Theorem ⊢ DATATYPE (record betree_leaf_t betree_leaf_id betree_leaf_size) @@ -1726,14 +1734,6 @@ sig (record betree_node_id_counter_t betree_node_id_counter_next_node_id) - [datatype_betree_node_t] Theorem - - ⊢ DATATYPE - (betree_node_t BetreeNodeInternal BetreeNodeLeaf ∧ - record betree_internal_t betree_internal_id - betree_internal_pivot betree_internal_left - betree_internal_right) - [datatype_betree_params_t] Theorem ⊢ DATATYPE |