(* a simplified programs script *)

(* one note: a lot of time is spent in this file chasing down redundant
type labels; typing tactics are needed for this theory *)

(* script new.quantifiers *)
(* script "natorder" *) (* this indicates what is needed *)

(* basic types needed *)

declareconstant "data";
declareconstant "address";
declareconstant "state";
declareconstant "command";

(* data includes naturals, boolean and error *)

axiom "NATDATA" "Nat:?n" "data:Nat:?n";

axiom "BOOLDATA" "bool:?b" "data:bool:?b";

declareconstant "error";

(* error is a data value *)

axiom "ERRORDATA" "error" "data:error";

(* error is not a natural number *)

axiom "ERRORNOTNAT" "error = Nat:error" "false";

s "error=Nat:?x";
ri "EQUATION"; ex();
right(); left();
initializecounter();
rri "REFLEX"; ex();
assign "?a_1" "error";
right(); ri "0|-|1"; rri "TYPES"; ri "RIGHT@ $0|-|1"; ex();
up(); ri "ERRORNOTNAT"; ex();
up();up(); rri "CASEINTRO"; ex();
p "ERRORNOTNAT2";

(* error is not a boolean *)

axiom "ERRORNOTBOOL" "error = bool:error" "false";

(* states are functions from addresses to data *)

axiom "STATEDEF" "state:?s" "[data:?s@address:?1]";

(* commands are functions from states to states which fix [error] *)

(* the idea is that [error] is the "crashed" state of our machine *)

(* this should prove that [error] is actually a state *)

(*

ERRORSTATE:

[error] = 

state : [error]

["ERRORDATA","STATEDEF"]

*)

s "[error]";
left(); ri "ERRORDATA"; ex();
right(); ri "BIND@address:?1"; ex();
top(); rri "STATEDEF"; ex();
p "ERRORSTATE";

(* this is really not what I want, because commands are more
than their execution behavior, but I'll use this definition for now *)

axiom "COMMANDDEF" "command:?c" 
"[((state:?1)=[error])||[error],state:?c@state:?1]";

(* now we look at some definitions of commands *)

defineconstant "abort" "[[error]]";

(* prove that abort is really a command *)

start "command:abort";
ri "COMMANDDEF"; ex();
dlls "abort"; ri "abort"; ex();
up(); ri "EVAL"; ex();
uptors "ERRORSTATE"; rri "ERRORSTATE"; ex();
uptors "CASEINTRO"; rri "CASEINTRO"; ex();
up(); rri "abort"; ex();
wb();

p "ABORTCOMMAND";


(* simplest approach is to start with command:abort and simplify *)

defineconstant "skip" "[state:?1]";

(* prove that skip is really a command (it obviously takes states to states,
and fixes [error]) *)

s "command:skip";
ri "COMMANDDEF"; ex();
right(); right(); right(); right();
ri "(LEFT@skip)**EVAL"; ex();
ri "TYPES"; ex();
up(); ri "TYPES"; ex();
top(); right(); right(); left(); rri "0|-|1";
up(); up(); rri "CASEINTRO"; ex();
up(); rri "skip"; ex();
wb();
p "SKIPCOMMAND";

(* now for the single assignment statement *)

(* can't use := because operators beginning with : have a special 
meaning; but this is not true in the new version of the prover, where
I will return to sensible notation! *)

(* right expressions are simply addresses for the moment *)
(* later we will want more complex right expressions -- as for
array assignment, for example, where the address chosen can depend
on the state *)

(* left expressions are functions from states to data *)

declareconstant "rexp";

axiom "REXPDEF" "rexp:?l" "[data:?l@state:?1]";

defineinfix "ASSIGNDEF" "(?x=:?y)" "command:[[((address:?x)=address:?2)||((rexp:?y)@(state:?1)),(state:?1)@?2]]";

(* ?x=:?y is clearly a command; the application of command: in the definition
helps us to avoid saying anything about the [error] state in the
definition *)

(* provide theorems to clarify what it is that =: actually does *)

(* the trivial proof that assignments are commands *)

s "?x=:?y";
ri "ASSIGNDEF"; rri "TYPES"; ex();
right(); rri "ASSIGNDEF"; ex();
p "ASSIGNCOMMAND";

(* an illustration of what this does *)

s "(?x=:?y)@?s";
ri "(LEFT@ASSIGNDEF)**EVAL"; ex();
left(); ri "COMMANDDEF"; ex();
right(); right(); right(); right(); ri "EVAL"; ex();
ri "EVERYWHERE2@TYPES"; ex();
up(); ri "STATEDEF"; ex();
ri "VALUE@[RIGHT@EVAL]"; ex();
ri "EVERYWHERE2@TYPES"; ex();
right(); ri "UNEVAL@[data:?3]"; ex();  (* UNEVAL;
					it's a new built-in tactic
					which converts its target to
					a value of the function given 
					as its parameter, if possible *)
					
ri "FNDIST**EVERYWHERE@EVAL"; ex();
right(); left(); right(); left();
ri "REXPDEF"; ex(); up(); ri "EVAL"; ex();
up(); ri "TYPES"; ex();
ri "BIND@state:?1"; ex();
ri "LEFT@ $REXPDEF"; ex();
up(); right(); dlls "STATEDEF"; ri "STATEDEF"; up(); ri "EVAL"; ex();
up(); ri "TYPES"; ri "BIND@address:?2"; ex();
ri "LEFT@ $STATEDEF"; ex();
top(); ri "EVAL"; ex();

(* this is a rather ugly expression; you might compare it with stuff
in the old programs.mk2 file *)

(* Here's something more concrete *)

(* take the state of the computer in which everything is 1 and 
assign the value 5 (we have [5] because a rexp depends on the state)
to the variable ?x; determine the value of a variable ?y in this state *)

s "((?x=:[5])@[1])@?y";
left(); left(); ri "ASSIGNDEF"; ex();
ri "COMMANDDEF"; ex();
up(); ri "EVERYWHERE2@EVAL"; ex();

(* first prove that [1] is not [error] *)

left(); left(); ri "STATEDEF"; ex();
right();right(); ri "EVAL"; ex();
ri "ONENAT"; up(); rri "NATDATA"; ex();
up(); up(); rri "UNIV_EQ"; ex();
right(); right(); ri "EQSYMM**ERRORNOTNAT2"; ex();
up(); up(); ri "FORALLDROP**AF"; up(); ex();
ri "STATEDEF**EVERYWHERE2@EVAL"; ex();
right(); ri "UNEVAL@[data:?2]"; ri "FNDIST**EVERYWHERE@EVAL"; ex();
ri "EVERYWHERE2@TYPES"; ex();
right(); left(); drls "REXPDEF"; ri "REXPDEF"; ex();
ri "EVERYWHERE2@EVAL"; ex();
right(); right(); ri "TYPENUMERAL"; ex();
up(); rri "NATDATA"; ex();
up(); up(); ri "EVAL"; ex();
up(); rri "NATDATA"; ex();
rri "BUILTIN"; ex();
up(); right(); drls "STATEDEF"; ri "STATEDEF"; ex();
ri "EVERYWHERE2@EVAL"; ex();
ri "EVERYWHERE2@TYPENUMERAL** $NATDATA"; ex();
up(); ri "EVAL"; ex();
up(); ri "($NATDATA)** $BUILTIN"; ex();
top(); ri "EVAL"; ex();
p "ASSIGN_EXAMPLE";

(* command sequencing *)

(* this is just a special case of composition of functions *)

defineinfix "SEQDEF" "?x;?y" "[(command:?y)@(command:?x)@?1]";

(* abort followed by any command is still an abort *)

s "abort;?c";
ri "SEQDEF"; ex();
right(); right(); left(); right(); rri "ABORTCOMMAND"; ri "abort"; ex();
up(); ri "EVAL"; ex();
up(); left(); ri "COMMANDDEF"; ex();
ri "EVERYWHERE2@EVAL"; ex();
ri "EVERYWHERE2@ $ERRORSTATE"; ex();
ri "VALUE@[$CASEINTRO]"; ex();
up(); ri "EVAL"; ex();
up(); left(); ri "COMMANDDEF"; ex();
up(); ri "EVAL"; ex();
ri "LEFT@(LEFT@ $ERRORSTATE)**REFLEX"; ex();
top(); rri "abort"; ex();
p "ABORTSEQ1";

(* any command followed by an abort is an abort *)

s "?c;abort";
ri "SEQDEF"; ex();
right(); left(); ri "COMMANDDEF"; ex();
up(); ri "EVAL"; ex();
downtoright "abort@?x";
ri "(LEFT@abort)**EVAL"; ex();
up(); rri "ERRORSTATE"; ex();
uptors "CASEINTRO"; rri "CASEINTRO"; ex();
top(); rri "abort"; ex();
p "ABORTSEQ2";

(* skip is the identity of command sequencing *)

s "?c;skip"; 
ri "SEQDEF"; ex();
right(); left(); ri "COMMANDDEF"; ex();
downtoright "skip@?x";
ri "(LEFT@skip)**EVAL**TYPES"; ex();
up(); ri "TYPES"; ex();
top(); right(); ri "EVAL"; ex();
right(); left(); rri "0|-|1"; ex();
uptors "CASEINTRO"; rri "CASEINTRO"; ex();
right(); left(); ri "COMMANDDEF"; ex();
up(); ri "EVAL"; ex();
up(); ri "UNEVAL@[state:?2]"; ri "FNDIST**EVERYWHERE@EVAL"; ex();
ri "(LEFT_CASE@ $ERRORSTATE)**RIGHT_CASE@TYPES"; ex();
uptors "COMMANDDEF"; rri "COMMANDDEF"; ex();
p "SKIPSEQ1"; 

(* another theorem about assignment, under construction *)

(* under what circumstances do two assignments of constant data values
to addresses commute? *)

s "((?x=:[?y]);(?z=:[?w]))=(?z=:[?w]);?x=:[?y]";

(* projected:  work on defining multiple assignment in terms of simple
assignment, using a refinement of the machine model to allow temporary
addresses? *)

(* here's a sketch of an implementation of multiple assignment using
single assignment and "private" temporary variables *)

(* this involves making explicit assumptions about the availability
of "hidden" memory in one's machine, so it is NOT good for a general theory
of programming! *)

declareconstant "private_address";
declareconstant "private_state";

(* definition of private state -- function from private addresses to states *)

axiom "PRIVSTATEDEF" "private_state:?s" "[data:?s@ private_address:?1]";

(* addresses are private addresses, too *)

axiom "ADDRESSES" "address:?v" "private_address:address:?v";

(* the relationship between states and private states *)

(*

STATES:

state : ?s = 

[(private_state : ?s) @ address : ?1]

["ADDRESSES","PRIVSTATEDEF","STATEDEF"]

*)

s "state:?s";
ri "STATEDEF"; ex();
drls "ADDRESSES"; ri "ADDRESSES"; ex();
top(); right(); ri "BIND@address:?1"; ex();
left(); rri "PRIVSTATEDEF"; ex();
p "STATES";

(* this ensures that the behavior of address and private_address
as retractions is convenient *)

(* this is an interesting phenomenon to look at when thinking
about subtyping *)

axiom "ADDRESSES2" "address:private_address:?x" "address:?x";

(* prove that states are also private states; ADDRESSES2 is needed for this *)

(*

STATES2:

private_state : state : ?s = 

state : ?s

["ADDRESSES2","PRIVSTATEDEF","STATEDEF","TYPES"]

*)

s "private_state:state:?s";
ri "PRIVSTATEDEF"; ex();
drls "STATEDEF"; ri "STATEDEF"; ex();
up(); ri "EVAL"; ex();
drls "ADDRESSES2"; ri "ADDRESSES2"; ex();
uptols "TYPES"; ri "TYPES"; ex();
uptors "STATEDEF"; rri "STATEDEF"; ex();
p "STATES2";

(*

STATES3:

state : private_state : ?s = 

state : ?s

["ADDRESSES","PRIVSTATEDEF","STATEDEF","TYPES"]

*)

s "state:private_state:?s";
ri "STATEDEF"; ex();
drls "PRIVSTATEDEF"; ri "PRIVSTATEDEF"; ex();
up(); ri "EVAL"; ex();
drrs "ADDRESSES"; rri "ADDRESSES"; ex();
uptols "TYPES"; ri "TYPES"; ex();
uptors "STATEDEF"; rri "STATEDEF"; ex();
p "STATES3";

(* axioms providing for private addresses which are not addresses *)
(* this gives us a strictly private address corresponding to each
public address *)

declareconstant "temp";
axiom "TEMPTYPE" "temp@?x" "private_address:temp@address:?x";
axiom "TEMPPRIVATE" "(temp@?x)=address:temp@?x" "false";

declareconstant "private_command";
axiom "PRIVCOMMANDDEF" "private_command:?c" 
"[((private_state:?s)=[error]) || [error] , private_state:?c@private_state:?1]";
declareconstant "private_rexp";

axiom "PRIVREXPDEF" "private_rexp:?l" "[data:?l@private_state:?1]";

defineinfix "PRIVASSIGNDEF" "(?x=:`priv ?y)" "private_command:[[((private_address:?x)=private_address:?2)||((private_rexp:?y)@(private_state:?1)),(private_state:?1)@?2]]";

defineinfix "PRIVSEQDEF" "?x;`priv ?y" "[(private_command:?y)@(private_command:?x)@?1]";

defineconstant "var@[?x]" "[(state:?1)@?x]";

defineconstant "private_var@[?x]" "[(private_state:?1)@?x]";

s "(address:?x)=:(rexp:?y)";
ri "ASSIGNDEF**(EVERYWHERE2@TYPES)** $ASSIGNDEF"; ex();
p "ASSIGNSCIN";
makescin "=:" "ASSIGNSCIN"; 

s "(private_address:?x)=:`priv (private_rexp:?y)";
ri "PRIVASSIGNDEF**(EVERYWHERE2@TYPES)** $PRIVASSIGNDEF"; ex();
p "PRIVASSIGNSCIN2";
makescin "=:`priv" "PRIVASSIGNSCIN2";

(* is this written correctly?  Exercise: prove that swap is a command *)

defineconstant "swap@?x,?y" 
"((temp@?x)=:`priv (private_var@[?y]));`priv(?y =: var@[?x]);`priv ?x =:`priv (private_var@[temp@?x])";

(* definition of weakest precondition *)

defineconstant "(wp@[?S])@?R"
"[(~[error]=(command:?S)@(state:?1))&?R@(command:?S)@(state:?1)]";

(* definition of Hoare triple in terms of wp *)

defineconstant "Htriple@?P,?Q,?R" "[?P@state:?1] |= (wp @ [?Q]) @ ?R";

(* prove a better version of the definition of Htriple given in the
old programs.mk2 file; the correction is that we do not allow Q
to crash when P is true *)

(*

Htriple2:  

Htriple @ ?P , ?Q , ?R  =  

(forall @ [(?P @ state : ?1) -> ~ [error] = (command 
         : ?Q) @ state : ?1]) & forall @ [(?P @ state 
      : ?1) -> ?R @ (command : ?Q) @ state : ?1]

AND , ASSERT , BOOLDEF , CASEINTRO , EQBOOL , EQUATION 
, FNDIST , Htriple , IF , IN , NONTRIV , NOT1 , ODDCHOICE 
, OR , REFLEX , Subset , TYPES , forall , wp , 0

*)

ae "Htriple";
ri "Subset2"; ex();
drls "wp"; ri "wp"; ex();
up(); ri "EVAL"; ex();
uptols "IDIS3"; ri "IDIS3"; ex();
top(); ri "FORALLDIST"; ex();
p "Htriple2";

quit();