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

Overview

These Athena files constitute the Athena library, version 1.4. They are included in the Athena 1.4.1 (FPMICS) distribution files available on the GitHub Athena Foundation site.

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