.Open MATHS Model of Project
This is a formalization of a part of a project submitted by
Shenning Wen to the CSci Dept CSUSB as part of his Masters
Degree.  It solely my own work and does not reflect the extreme
usefulness of the Visual Basic and MS Access system that he produced.

. Conceptual Model of the Legacy Data Base
Address::$String.
Time_period::$linearly_ordered_set.
Customer::Finite_sets.
ac::$Customer->$Address.
This notation declares that `ac` is a map from Customers to addresses. See
$Maps.

Notice::Finite_sets.
tn::$Notice->$Time_period, time notice sent,
cn::$Notice->$Customer, customer to whom notice is sent.

Region::Finite_sets.
Store::Finite_sets.
rs::$Store->$Region, the store's region.

Bank::Finite_sets.

Account::Finite_sets.
	ca::$Account->$Customer
ba::$Account->$Bank

Check::Finite_sets.
Status::Finite_sets.
tc::$Check->$Time_period,
sc::$Check->$Store,
ac::$Check->$Account,
st::$Check->$Status, status of check.

bad::$Status.
Bad_check:: @ $Check,

 |-(1): For $Check x, x $in $Bad_check iff $st(x) = $bad.

The "|-" indicates an assertion without reason -- an axiom or assumption.

 (1)|-(2): $Bad_check= /$st($bad).

The "|-" above indicates an assertion with reason -- a theeorem.

Bad_customer::@$Customer,

 |-(3): for $Customer x, x  $in $Bad_customer iff for some $Bad_check y ( x = $ca( $ac( y  ) ) ).


 (3) |-(4): $Bad_customer= $ca ($ac ($Bad_check)).


 (2,4) |-(5): $Bad_customer= $ca $o $ac  $o /$st($bad).
. Proof of 5
Substitute in 4 the values of $Bad_check in 2.
. Proof of 4
$STANDARD overloading of functions from elements in domain to
subsets of domain.
. Proof of 2
$STANDARD overloading of functions from elements in domain to
substes of domain.

. The Datamart
A Datamart is a summarized user-friendly subset of a large database 
called a data warehouse.   A Data warehouse is a collection
of data for many possible purposes, some of which are not
known at the time of collection and storage.  A data mart is
focused on a few critical known user needs.

In this case the user only wants to
know about bad customers.  It is not worth wasting storage
in the datamart for information on `all` customers.


The datamart is also simplified by relating checks directly to
the customers that wrote them.
Data_Mart::=following,
.Net
No need to duplicate the global definitions.  Definitions for the Datamart
are prefixed with a DM.
DM_Customer::=$Bad_Customer.
DM_ac::$DM_Customer->$Address.
 |-(DM1): DM_ac = $ac o $DM_Customer. -- the $ac map limited to operate on $DM_Customer
only.

DM_Notice::Finite_sets=$Notice.
DM_tn::$DM_Notice->$Time_period, time notice sent,
 |-(DM2): DM_tn = $tn o $DM_Notice.
DM_cn::$DM_Notice->$DM_Customer, customer to whom notice is sent.
 |-(DM3): DM_cn = $cn o $DM_Notice.

DM_Account::@ $Account = { a:$Account || $cs(a) $in $DM_Customer }.
DM_ba::$DM_Account->$Bank = $ba o $DM_Account.
DM_ca::$DM_Account->$DM_Customer = $ca o $DM_Account.

I assume, below, that the executive is interested in all the checks
that a bad customer tends  whether they are good or bad. For an alternative
see
.See Exercise 1
below.
DM_Check::@ $Check = `Checks written by bad customers`.
 |-(DM4): DM_Check = { c: $Check || $ca($ac(c) $in DM_Customer }.
DM_bc::$DM_Check->$DM_Customer,
 |-(DM5): For $DM_Check c, bc(c) = $ca($ac(c)).

DM_Bad_Check::= $DM_Check & $Bad_check.
 (DM_customer, DM_checks,DM5)|- (DM6): For all $DM_Customer b, some $DM_Bad_check c, $DM_bc(c)=b.
. Proof of DM6
.Let
 ()|-DM_customers are customers with at least one bad check.
 ()|-DM_checks are all checks from DM_customers.
 ()|-All bad_checks are in the DM.
 ()|-The customer associated by the DM to a badcheck is by $DM5, the customer
in the main data base.
.Close.Let
.Close.Net
. Exercise 1
Shenning Wen's datamart only showed Bad_checks.  What do
you change $Data_Mart above to reflect this?
. Exercise 2
Shenning Wen's datamart also limited the number of Bad_Checks and
Notices in the Data Mart to 3 of each.  What do
you change in the result of Exercise 1 to reflect this?  There
are a number of ways to do this.  Choose one that might suit a
decision make and state why this is a good choice.
. Exercise 3
Suppose that the datamart has a map from each customer to a
account and each account to its bank.  Is this necessarily true
or does it add an assumption?  Either prove correctness or
state (and prove) a required axiom.
. References
For a summary of the notation see
.See http://www.csci.csusb.edu/dick/maths/math.syntax.html

linearly_ordered_set::=http://www/dick/maths/math_21_Order.html#toset.
Maps::=http://www.csci.csusb.edu/dick/maths/logic_5_Maps.html#Applying functions and maps.
o::=functional composition, see $Relations and $Maps.
/ ::=functional inversion, see $ConverseRelations.
in::=`is an element of set`, see $Sets
ConverseRelations::=http://www.csci.csusb.edu/dick/maths/logic_40_Relations.html#Converse Relations.
Relations::=http://www.csci.csusb.edu/dick/maths/logic_40_Relations.html.
Sets::=http://www/dick/maths/logic_30_Sets.html
STANDARD::=http://www/dick/maths/math_11_STANDARD.html.
String::=http://www/dick/maths/math_62_Strings.html.
.Close MATHS Model of Project