Athena Library (Version 1.3)
Konstantine Arkoudas and David Musser 
 
Proof Central
Athena

Overview

These Athena files constitute the Athena library, version 1.3. They are included in the distribution file.

lib/main files and listings

fast-power.ath  (listing)  Compute x +* n using lg n + operations
fast-power_unittest.ath  (listing)  
group.ath  (listing)  Semigroup, Identity, Monoid, Group algebraic theories
group_unittest.ath  (listing)  
integer-integral-domain.ath  (listing)  ZID, the integers as an integral domain
integer-plus.ath  (listing)  Integer addition
integer-times.ath  (listing)  Integer multiplication
integral-domain.ath  (listing)  Integral-Domain, an algebraic theory
integral-domain_unittest.ath  (listing)  
list-of.ath  (listing)  List datatype
nat-div.ath  (listing)  Natural number division
nat-fast-power.ath  (listing)  Natural number specialization of fast-power
nat-fast-power1.ath  (listing)  A variation
nat-gcd.ath  (listing)  Natural number gcd function (Euclid’s algorithm)
nat-half.ath  (listing)  Natural number floor of n/2 function; even, odd, parity
nat-less.ath  (listing)  Natural number orderings
nat-max.ath  (listing)  Natural number max function
nat-minus.ath  (listing)  Natural number subtraction
nat-plus.ath  (listing)  Natural number addition
nat-power.ath  (listing)  Natural number specialization of power
nat-times.ath  (listing)  Natural number multiplication
order.ath  (listing)  Binary-Relation, Irreflexive, Transitive, etc. relational theories
order_unittest.ath  (listing)  
ordered-list-nat.ath  (listing)  Natural number specialization of ordered-lists
ordered-list.ath  (listing)  Orderings of lists theory
ordered-list_unittest.ath  (listing)  
power.ath  (listing)  Compute x +* n using n-1 + operations
power_unittest.ath  (listing)  
ring.ath  (listing)  Ring, an algebraic theory
ring_unittest.ath  (listing)  
transitive-closure.ath  (listing)  Transitive closure, a relational theory
transitive-closure_unittest.ath  (listing)  

lib/algebra files and listings

function.ath  (listing)  Function theory
function_unittest.ath  (listing)  
permutation.ath  (listing)  Permutation theory
permutation_unittest.ath  (listing)  
Z-as-integral-domain.ath  (listing)  Integers as an integral doman
Z-poly-as-group.ath  (listing)  Integer power series as a group
Z-poly.ath  (listing)  Integer power series

lib/search files and listings

binary-search-nat.ath  (listing)  Binary search on BST with nat keys
binary-search-tree-nat.ath  (listing)  Binary search tree with nat keys
binary-search-tree.ath  (listing)  Binary search tree (BST) over Strict Weak Order (SWO)
binary-search-tree_unittest.ath  (listing)  
binary-search.ath  (listing)  Binary search on BST over SWO
binary-search1-nat.ath  (listing)  Binary search on BST with nat keys (alternate version)
binary-search_unittest.ath  (listing)  
binary-tree.ath  (listing)  Binary tree over T

lib/memory-range files and listings

bidirectional-iterator.ath  (listing)  Iterator with forward and backward movement
bidirectional-iterator_unittest.ath  (listing)  
binary-search-range.ath  (listing)  Binary search on a range
binary-search-range_unittest.ath  (listing)  
collect-locs.ath  (listing)  Collect memory locations into a list
collect-locs_unittest.ath  (listing)  
copy-range-backward.ath  (listing)  Copy starting at end
copy-range-backward_unittest.ath  (listing)  
copy-range.ath  (listing)  Copy starting at beginning
copy-range_unittest.ath  (listing)  
count-range.ath  (listing)  Count elements equal to a given value
count-range_unittest.ath  (listing)  
forward-iterator.ath  (listing)  Iterator with forward movement
forward-iterator_unittest.ath  (listing)  
memory.ath  (listing)  Basic memory access and modification
memory_unittest.ath  (listing)  
ordered-range.ath  (listing)  Operations on a range over a strict weak order
ordered-range_unittest.ath  (listing)  
random-access-iterator.ath  (listing)  Iterator with “big jump” movement
random-access-iterator_unittest.ath  (listing)  
range-length.ath  (listing)  Operations involving range lengths
range-length_unittest.ath  (listing)  
range.ath  (listing)  Range datatype and basic operations
range_unittest.ath  (listing)  
replace-range.ath  (listing)  Replace elements equal to x with a value y
replace-range_unittest.ath  (listing)  
reverse-range.ath  (listing)  Iterator adapter that reverses direction of movement
reverse-range_unittest.ath  (listing)  
swap-implementation.ath  (listing)  Implementation of swap operation on memory
swap-implementation_unittest.ath  (listing)  
trivial-iterator.ath  (listing)  Base of iterator refinements
trivial-iterator_unittest.ath  (listing)  

lib/basic

dmaps.ath  (listing)  DMap, default finite map structure
dmaps_unittest.ath  (listing)  
fmaps.ath  (listing)  Map, finite map structure
fmaps_unittest.ath  (listing)  
pairs.ath  (listing)  Pair, ordered pair datatype
sets.ath  (listing)  Set, finite set structure
sets_unittest.ath  (listing)  
st.ath  (listing)  ST, structured theory module