new library for binary trees

parent f86d8cf2
(* Polymorphic binary trees with elements at nodes *)
theory Tree
type tree 'a = Empty | Node (tree 'a) 'a (tree 'a)
end
theory Size
use export Tree
use export int.Int
(* number of nodes *)
function size (t: tree 'a) : int = match t with
| Empty -> 0
| Node l _ r -> 1 + size l + size r
end
lemma size_nonneg: forall t: tree 'a. 0 <= size t
end
theory Inorder "inorder traversal"
use export Tree
use export list.Append
function inorder (t: tree 'a) : list 'a = match t with
| Empty -> Nil
| Node l x r -> inorder l ++ Cons x (inorder r)
end
end
theory InorderLength
use import Size
use import Inorder
use import list.Length
lemma inorder_length: forall t: tree 'a. length (inorder t) = size t
end
theory Zipper "Huet's zipper"
use export Tree
type zipper 'a =
| Top
| Left (zipper 'a) 'a (tree 'a)
| Right (tree 'a) 'a (zipper 'a)
function zip (t: tree 'a) (z: zipper 'a) : tree 'a = match z with
| Top -> t
| Left z x r -> zip (Node t x r) z
| Right l x z -> zip (Node l x t) z
end
(* navigating in a tree using a zipper *)
type pointer 'a = (tree 'a, zipper 'a)
function start (t: tree 'a) : pointer 'a = (t, Top)
function up (p: pointer 'a) : pointer 'a = match p with
| _, Top -> p (* do nothing *)
| l, Left z x r | r, Right l x z -> (Node l x r, z)
end
function top (p: pointer 'a) : tree 'a = let t, z = p in zip t z
function down_left (p: pointer 'a) : pointer 'a = match p with
| Empty, _ -> p (* do nothing *)
| Node l x r, z -> (l, Left z x r)
end
function down_right (p: pointer 'a) : pointer 'a = match p with
| Empty, _ -> p (* do nothing *)
| Node l x r, z -> (r, Right l x z)
end
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/jcf/why3/share/why3session.dtd">
<why3session
name="bintree/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<file
name="../bintree.why"
verified="true"
expanded="true">
<theory
name="Tree"
locfile="bintree/../bintree.why"
loclnum="4" loccnumb="7" loccnume="11"
verified="true"
expanded="false">
</theory>
<theory
name="Size"
locfile="bintree/../bintree.why"
loclnum="10" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="size_nonneg"
locfile="bintree/../bintree.why"
loclnum="21" loccnumb="8" loccnume="19"
sum="c1e5f3c86f46cbc2b49f66569a612b62"
proved="true"
expanded="true"
shape="ainfix &lt;=c0asizeV0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
<goal
name="size_nonneg.1"
locfile="bintree/../bintree.why"
loclnum="21" loccnumb="8" loccnume="19"
sum="76f33fc5fb40c8de9764fff0ecc30fc4"
proved="true"
expanded="true"
shape="CV0aEmptyainfix &lt;=c0asizeV0aNodeVVVainfix &lt;=c0asizeV0Iainfix &lt;=c0asizeV1Iainfix &lt;=c0asizeV3F">
<transf
name="split_goal_wp"
proved="true"
expanded="true">
<goal
name="size_nonneg.1.1"
locfile="bintree/../bintree.why"
loclnum="21" loccnumb="8" loccnume="19"
sum="fd2074b121c07cb9a3b66e8b49e50a79"
proved="true"
expanded="true"
shape="CV0aEmptyainfix &lt;=c0asizeV0aNodeVVVtF">
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="size_nonneg.1.2"
locfile="bintree/../bintree.why"
loclnum="21" loccnumb="8" loccnume="19"
sum="efa29176d54e8840510dd6f7eee5df39"
proved="true"
expanded="true"
shape="CV0aEmptytaNodeVVVainfix &lt;=c0asizeV0Iainfix &lt;=c0asizeV1Iainfix &lt;=c0asizeV3F">
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
<theory
name="Inorder"
locfile="bintree/../bintree.why"
loclnum="25" loccnumb="7" loccnume="14"
verified="true"
expanded="false">
<label
name="inorder traversal"/>
</theory>
<theory
name="InorderLength"
locfile="bintree/../bintree.why"
loclnum="37" loccnumb="7" loccnume="20"
verified="true"
expanded="true">
<goal
name="inorder_length"
locfile="bintree/../bintree.why"
loclnum="43" loccnumb="8" loccnume="22"
sum="1bc5feeae3944538d03f37ec709c26c5"
proved="true"
expanded="true"
shape="ainfix =alengthainorderV0asizeV0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
<goal
name="inorder_length.0"
locfile="bintree/../bintree.why"
loclnum="43" loccnumb="8" loccnume="22"
sum="d2f91049042927cd5d7fb026985d1a7e"
proved="true"
expanded="true"
shape="CV0aEmptyainfix =alengthainorderV0asizeV0aNodeVVVainfix =alengthainorderV0asizeV0Iainfix =alengthainorderV1asizeV1Iainfix =alengthainorderV3asizeV3F">
<transf
name="split_goal_wp"
proved="true"
expanded="true">
<goal
name="inorder_length.0.0"
locfile="bintree/../bintree.why"
loclnum="43" loccnumb="8" loccnume="22"
sum="e39439bd48e1fdbe19b829c2591c85ea"
proved="true"
expanded="false"
shape="CV0aEmptyainfix =alengthainorderV0asizeV0aNodeVVVtF">
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="inorder_length.0.1"
locfile="bintree/../bintree.why"
loclnum="43" loccnumb="8" loccnume="22"
sum="bd22d649f8c6dfdce33a3d42dfdbd275"
proved="true"
expanded="false"
shape="CV0aEmptytaNodeVVVainfix =alengthainorderV0asizeV0Iainfix =alengthainorderV1asizeV1Iainfix =alengthainorderV3asizeV3F">
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment