diff options
author | Son Ho | 2023-05-12 21:19:28 +0200 |
---|---|---|
committer | Son HO | 2023-06-04 21:54:38 +0200 |
commit | a15a029d9b885906495a63c0b37dbfe59ec5c065 (patch) | |
tree | e3ba2b7afd23b1c257c3bf58fb6a705743c55867 /backends/hol4/divDefLibTestScript.sml | |
parent | 62699c2ebb2d10301f437ca06961a82c30913405 (diff) |
Fix minor issues
Diffstat (limited to '')
-rw-r--r-- | backends/hol4/divDefLibTestScript.sml | 65 |
1 files changed, 61 insertions, 4 deletions
diff --git a/backends/hol4/divDefLibTestScript.sml b/backends/hol4/divDefLibTestScript.sml index b1243065..80170b24 100644 --- a/backends/hol4/divDefLibTestScript.sml +++ b/backends/hol4/divDefLibTestScript.sml @@ -7,10 +7,9 @@ open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory open primitivesLib open divDefTheory divDefLib -val [even_def, odd_def] = DefineDiv ‘ - (even (i : int) : bool result = if i = 0 then Return T else odd (i - 1)) /\ - (odd (i : int) : bool result = if i = 0 then Return F else even (i - 1)) -’ +val _ = new_theory "divDefLibTest" + +(* nth *) Datatype: list_t = @@ -31,3 +30,61 @@ val [nth_def] = DefineDiv ‘ od | ListNil => Fail Failure ’ + +(* even, odd *) + +val [even_def, odd_def] = DefineDiv ‘ + (even (i : int) : bool result = if i = 0 then Return T else odd (i - 1)) /\ + (odd (i : int) : bool result = if i = 0 then Return F else even (i - 1)) +’ + +(* btree *) + +Datatype: + btree = + BLeaf 'a + | BNode btree btree +End + +val [btree_height_def] = DefineDiv ‘ + btree_height (tree : 'a btree) : int result = + case tree of + | BLeaf _ => Return 1 + | BNode l r => + do + hl <- btree_height l; + hr <- btree_height r; + Return (hl + hr) + od +’ + +(* tree 2 *) + +Datatype: + tree = + TLeaf 'a + | TNode node ; + + node = + Node (tree list) +End + +val [tree_height_def, tree_nodes_height_def] = DefineDiv ‘ + (tree_height (tree : 'a tree) : int result = + case tree of + TLeaf _ => Return 1 + | TNode n => + case n of Node ls => tree_nodes_height ls) ∧ + + (tree_nodes_height (ls : ('a tree) list) : int result = + case ls of + [] => Return 0 + | t :: tl => + do + h1 <- tree_height t; + h2 <- tree_nodes_height tl; + Return (h1 + h2) + od) +’ + +val _ = export_theory () |