(* $Header: /users/lal/black/hol/Disser/RCS/semeq.sml,v 1.22 1997/05/19 20:52:11 black Exp $ *)
(* *created  "Tue Dec 17 15:50:40 1996" *by "Paul E. Black" *)
(* *modified "Mon May 19 14:49:36 1997" *by "Paul E. Black" *)

(*-----------------------------------------------------------------------
	Definition of semantic equivalence of two C statements
 -----------------------------------------------------------------------*)

system "/bin/rm semeq.thms";
new_theory "semeq";

new_parent "c_ast";

use "utilities.sml"; (* for LIFT_QUANT_RULE *)

load_library {lib = Sys_lib.ind_def_lib , theory = "-"};

(*-----------------------------------------------------------------------
	C expression has No Side Effects.  Specifically, evaluating the
	expression doesn't change the state.
 -----------------------------------------------------------------------*)

local val NoSEType = (--`NoSE:CExpr->bool`--)
in
val {desc=NoSE_rules, induction_thm=NoSE_ind} =
    Inductive_def.new_inductive_definition {
    name = "NoSE",
    patt = ((--`^NoSEType expr`--), []),
    fixity = Prefix,
    rules = [
{(* integer constants don't have side effects *)
side_conditions = [],
hypotheses = [],
		(*----------------------------------------*)
conclusion =	(--`^NoSEType (Const c t)`--)},
	(*----------------------------------------------------------------
		Kludge - we should have a separate, mutually recursive
		definition of NoSE for Lvalues.
	 ----------------------------------------------------------------*)
{(* variable references don't change state *)
side_conditions = [],
hypotheses = [],
		(*----------------------------------------*)
conclusion =	(--`^NoSEType (Lval (Vref var))`--)},
{(* array references don't change state, if the index expression doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoSEType c`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoSEType (Lval (Aryref var c))`--)},
{(* dereference ("*") doesn't change state if the expression doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoSEType c`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoSEType (Lval (Deref c))`--)},
{(* structure field accesses don't change state if the Lvalue doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoSEType (Lval lv)`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoSEType (Lval (Field lv var))`--)},
(* Assignments change the state *)
{(* Binary operations don't change state if neither operand does *)
side_conditions = [],
hypotheses = [	(--`^NoSEType c1`--),
		(--`^NoSEType c2`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoSEType (Binary c1 opr c2)`--)},
{(* address-of ("&") doesn't change state if the Lvalue doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoSEType (Lval lv)`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoSEType (LUnary AdrOf lv)`--)},
{(* Unary operations don't change state if operand doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoSEType c`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoSEType (Unary opr c)`--)}
(* we'll be conservative and assume that function Calls change state *)
]}
end;

val c = ref 1;
save_thm("NoSE_Const",			el (!c) NoSE_rules); c:=(!c)+1;
save_thm("NoSE_LVvar",			el (!c) NoSE_rules); c:=(!c)+1;
save_thm("NoSE_LVarray", LIFT_QUANT_RULE (el (!c) NoSE_rules)); c:=(!c)+1;
save_thm("NoSE_LVderef",		el (!c) NoSE_rules); c:=(!c)+1;
save_thm("NoSE_LVfield", LIFT_QUANT_RULE (el (!c) NoSE_rules)); c:=(!c)+1;
save_thm("NoSE_Binary",  LIFT_QUANT_RULE (el (!c) NoSE_rules)); c:=(!c)+1;
save_thm("NoSE_LUadrOf",		el (!c) NoSE_rules); c:=(!c)+1;
save_thm("NoSE_Unary",   LIFT_QUANT_RULE (el (!c) NoSE_rules)); c:=(!c)+1;


(*-----------------------------------------------------------------------
	Define what it means for an expressions to have no
	postevaluation side effects.
 -----------------------------------------------------------------------*)

local val NoPostSEType = (--`NoPostSE:CExpr->bool`--)
in
val {desc=NoPostSE_rules, induction_thm=NoPostSE_ind} =
    Inductive_def.new_inductive_definition {
    name = "NoPostSE",
    patt = ((--`^NoPostSEType expr`--), []),
    fixity = Prefix,
    rules = [
{(* constants don't have postevaluation side effects *)
side_conditions = [],
hypotheses = [],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (Const c t)`--)},
	(*----------------------------------------------------------------
		Kludge - we should have a separate, mutually recursive
		definition of NoPostSE for Lvalues.
	 ----------------------------------------------------------------*)
{(* variable references don't have postevaluation side effects *)
side_conditions = [],
hypotheses = [],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (Lval (Vref var))`--)},
{(* array refs don't have post SE's if the index expression doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPostSEType c`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (Lval (Aryref var c))`--)},
{(* derefs ("*") don't have post SE's if the expression doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPostSEType c`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (Lval (Deref c))`--)},
{(* structure field accesses don't have post SE's if the Lvalue doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPostSEType (Lval lv)`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (Lval (Field lv var))`--)},
{(* assignments don't have post SE's if the lvalue and expr don't *)
side_conditions = [],
hypotheses = [	(--`^NoPostSEType (Lval lv)`--),
		(--`^NoPostSEType ce`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (Assign lv ce)`--)},
{(* binary operations don't have post SE's if neither operand does *)
side_conditions = [],
hypotheses = [	(--`^NoPostSEType c1`--),
		(--`^NoPostSEType c2`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (Binary c1 opr c2)`--)},
{(* address-of ("&") doesn't have post SE's if the Lvalue doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPostSEType (Lval lv)`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (LUnary AdrOf lv)`--)},
{(* preinc ("++lv") doesn't have post SE's if the Lvalue doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPostSEType (Lval lv)`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (LUnary PreInc lv)`--)},
{(* predec ("--lv") doesn't have post SE's if the Lvalue doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPostSEType (Lval lv)`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (LUnary PreDec lv)`--)},
{(* unary operations don't have post SE's if operand doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPostSEType c`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (Unary opr c)`--)},
	(*----------------------------------------------------------------
		Kludge - we should have a separate, mutually recursive
		definition of NoPostSE for ParamLists.
	 ----------------------------------------------------------------*)
{(* function calls don't have post SE's if param list is empty *)
side_conditions = [],
hypotheses = [],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (Call v PLnull)`--)},
{(* function calls don't have post SE's if first param and rest don't *)
side_conditions = [],
hypotheses = [	(--`^NoPostSEType ce`--),
		(--`^NoPostSEType (Call v prest)`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPostSEType (Call v (PL ce prest))`--)}
]}
end;

val c = ref 1;
save_thm("NoPostSE_Const",		el (!c) NoPostSE_rules); c:=(!c)+1;
save_thm("NoPostSE_LVvar",		el (!c) NoPostSE_rules); c:=(!c)+1;
save_thm("NoPostSE_LVarray", LIFT_QUANT_RULE (el (!c) NoPostSE_rules)); c:=(!c)+1;
save_thm("NoPostSE_LVderef",		el (!c) NoPostSE_rules); c:=(!c)+1;
save_thm("NoPostSE_LVfield", LIFT_QUANT_RULE (el (!c) NoPostSE_rules)); c:=(!c)+1;
save_thm("NoPostSE_Assign",  LIFT_QUANT_RULE (el (!c) NoPostSE_rules)); c:=(!c)+1;
save_thm("NoPostSE_Binary",  LIFT_QUANT_RULE (el (!c) NoPostSE_rules)); c:=(!c)+1;
save_thm("NoPostSE_LUadrOf",		el (!c) NoPostSE_rules); c:=(!c)+1;
save_thm("NoPostSE_LUPreInc",		el (!c) NoPostSE_rules); c:=(!c)+1;
save_thm("NoPostSE_LUPreDec",		el (!c) NoPostSE_rules); c:=(!c)+1;
save_thm("NoPostSE_Unary",   LIFT_QUANT_RULE (el (!c) NoPostSE_rules)); c:=(!c)+1;
save_thm("NoPostSE_CallNPL", LIFT_QUANT_RULE (el (!c) NoPostSE_rules)); c:=(!c)+1;
save_thm("NoPostSE_CallPL",  LIFT_QUANT_RULE (el (!c) NoPostSE_rules)); c:=(!c)+1;


(*-----------------------------------------------------------------------
	Define (at least the form of) semantic equivalence of
	preevaluation of subexpressions.
		PreEval lv e s1 s2
	means
		(Seq (Simple e) s1)
	has the same semantics as
			(s2)
	The term, lv, is the lvalue which holds the result of the
	expression, e.  The lvalue cannot have any side effects, and
	the expression cannot have any postevaluation side effects.

	SKIMP: these must be fully specified.
 -----------------------------------------------------------------------*)

local val PreEvalType = (--`PreEval:Lvalue->CExpr->CStmt->CStmt->bool`--)
in
val {desc=PreEval_rules, induction_thm=PreEval_ind} =
    Inductive_def.new_inductive_definition {
    name = "PreEval",
    patt = ((--`^PreEvalType lv e s1 s2`--), []),
    fixity = Prefix,
    rules = [
{(* preevaluation separation for simple statements *)
side_conditions = [(--`NoSE (Lval lv)`--)],
hypotheses = [	(--`NoPostSE e`--)],
		(*----------------------------------------*)
conclusion =	(--`^PreEvalType lv e (Simple cWOe) (Simple c)`--)},
{(* preevaluation separation for If statements *)
side_conditions = [(--`NoSE (Lval lv)`--)],
hypotheses = [	(--`NoPostSE e`--)],
		(*----------------------------------------*)
conclusion =	(--`^PreEvalType lv e (If cWOe s) (If c s)`--)},
{(* preevaluation separation for If/Then/Else statements *)
side_conditions = [(--`NoSE (Lval lv)`--)],
hypotheses = [	(--`NoPostSE e`--)],
		(*----------------------------------------*)
conclusion =	(--`^PreEvalType lv e (IfElse cWOe s1 s2)(IfElse c s1 s2)`--)},
{(* preevaluation separation for Return statements *)
side_conditions = [(--`NoSE (Lval lv)`--)],
hypotheses = [	(--`NoPostSE e`--)],
		(*----------------------------------------*)
conclusion =	(--`^PreEvalType lv e (Ret cWOe) (Ret c)`--)}
]}
end;

val c = ref 1;
save_thm("PreEval_simple", LIFT_QUANT_RULE (el (!c) PreEval_rules)); c:=(!c)+1;
save_thm("PreEval_if",	   LIFT_QUANT_RULE (el (!c) PreEval_rules)); c:=(!c)+1;
save_thm("PreEval_ifelse", LIFT_QUANT_RULE (el (!c) PreEval_rules)); c:=(!c)+1;
save_thm("PreEval_ret",	   LIFT_QUANT_RULE (el (!c) PreEval_rules)); c:=(!c)+1;


(*-----------------------------------------------------------------------
	Define what it means for an expressions to have no
	preevaluation side effects.
 -----------------------------------------------------------------------*)

local val NoPreSEType = (--`NoPreSE:CExpr->bool`--)
in
val {desc=NoPreSE_rules, induction_thm=NoPreSE_ind} =
    Inductive_def.new_inductive_definition {
    name = "NoPreSE",
    patt = ((--`^NoPreSEType expr`--), []),
    fixity = Prefix,
    rules = [
{(* constants don't have postevaluation side effects *)
side_conditions = [],
hypotheses = [],
		(*----------------------------------------*)
conclusion =	(--`^NoPreSEType (Const c t)`--)},
	(*----------------------------------------------------------------
		Kludge - we should have a separate, mutually recursive
		definition of NoPreSE for Lvalues.
	 ----------------------------------------------------------------*)
{(* variable references don't have preevaluation side effects *)
side_conditions = [],
hypotheses = [],
		(*----------------------------------------*)
conclusion =	(--`^NoPreSEType (Lval (Vref var))`--)},
{(* array refs don't have pre SE's if the index expression doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPreSEType c`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPreSEType (Lval (Aryref var c))`--)},
{(* derefs ("*") don't have pre SE's if the expression doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPreSEType c`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPreSEType (Lval (Deref c))`--)},
{(* structure field accesses don't have pre SE's if the Lvalue doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPreSEType (Lval lv)`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPreSEType (Lval (Field lv var))`--)},
(* assignment is a preeval side effect *)
{(* binary operations don't have pre SE's if neither operand does *)
side_conditions = [],
hypotheses = [	(--`^NoPreSEType c1`--),
		(--`^NoPreSEType c2`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPreSEType (Binary c1 opr c2)`--)},
{(* address-of ("&") doesn't have pre SE's if the Lvalue doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPreSEType (Lval lv)`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPreSEType (LUnary AdrOf lv)`--)},
{(* postinc ("lv++") doesn't have pre SE's if the Lvalue doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPreSEType (Lval lv)`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPreSEType (LUnary PostInc lv)`--)},
{(* postdec ("lv--") doesn't have pre SE's if the Lvalue doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPreSEType (Lval lv)`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPreSEType (LUnary PostDec lv)`--)},
{(* unary operations don't have pre SE's if operand doesn't *)
side_conditions = [],
hypotheses = [	(--`^NoPreSEType c`--)],
		(*----------------------------------------*)
conclusion =	(--`^NoPreSEType (Unary opr c)`--)}
(* we will be conservative and assume that function calls have preeval SE's *)
]}
end;

val c = ref 1;
save_thm("NoPreSE_Const",		el (!c) NoPreSE_rules); c:=(!c)+1;
save_thm("NoPreSE_LVvar",		el (!c) NoPreSE_rules); c:=(!c)+1;
save_thm("NoPreSE_LVarray", LIFT_QUANT_RULE (el (!c) NoPreSE_rules)); c:=(!c)+1;
save_thm("NoPreSE_LVderef",		el (!c) NoPreSE_rules); c:=(!c)+1;
save_thm("NoPreSE_LVfield", LIFT_QUANT_RULE (el (!c) NoPreSE_rules)); c:=(!c)+1;
save_thm("NoPreSE_Binary",  LIFT_QUANT_RULE (el (!c) NoPreSE_rules)); c:=(!c)+1;
save_thm("NoPreSE_LUadrOf",		el (!c) NoPreSE_rules); c:=(!c)+1;
save_thm("NoPreSE_LUPostInc",		el (!c) NoPreSE_rules); c:=(!c)+1;
save_thm("NoPreSE_LUPostDec",		el (!c) NoPreSE_rules); c:=(!c)+1;
save_thm("NoPreSE_Unary",   LIFT_QUANT_RULE (el (!c) NoPreSE_rules)); c:=(!c)+1;


(*-----------------------------------------------------------------------
	Define (at least the form of) semantic equivalence of
	postevaluation of subexpressions.
		PostEval s1 e s2
	means
		(Seq s1 (Simple e))
	has the same semantics as
			(s2)
	The expression cannot have any preevaluation side effects.

	SKIMP: these must be fully specified.
 -----------------------------------------------------------------------*)

(* SKIMP: this is just a beginning *)
local val PostEvalType = (--`PostEval:CStmt->CExpr->CStmt->bool`--)
in
val {desc=PostEval_rules, induction_thm=PostEval_ind} =
    Inductive_def.new_inductive_definition {
    name = "PostEval",
    patt = ((--`^PostEvalType s1 e s2`--), []),
    fixity = Prefix,
    rules = [
{(* Postevaluation separation for simple statements *)
side_conditions = [],
hypotheses = [	(--`NoPreSE e`--)],
		(*----------------------------------------*)
conclusion =	(--`^PostEvalType (Simple cWOe) e (Simple c)`--)}
]}
end;

val c = ref 1;
save_thm("PostEval_simple", LIFT_QUANT_RULE (el (!c)PostEval_rules));c:=(!c)+1;

		
(*-----------------------------------------------------------------------
	Semantic equivalence of two C statements
 -----------------------------------------------------------------------*)

local val SEM_EQType = (--`SEM_EQ:CStmt->CStmt->bool`--)
in
val {desc=SEM_EQ_rules, induction_thm=SEM_EQ_ind} =
    Inductive_def.new_inductive_definition {
    name = "SEM_EQ",
    patt = ((--`^SEM_EQType s1 s2`--), []),
    fixity = Prefix,
    rules = [
{(* semantic equivalence is reflexive *)
side_conditions = [],
hypotheses = [],
		(*----------------------------------------*)
conclusion =	(--`^SEM_EQType s1 s1`--)},
{(* semantic equivalence is symetric *)
side_conditions = [],
hypotheses = [	(--`^SEM_EQType s1 s2`--)],
		(*----------------------------------------*)
conclusion =	(--`^SEM_EQType s2 s1`--)},
{(* semantic equivalence is transitive *)
side_conditions = [],
hypotheses = [	(--`^SEM_EQType s1 s2`--),
		(--`^SEM_EQType s2 s3`--)],
		(*----------------------------------------*)
conclusion =	(--`^SEM_EQType s1 s3`--)},

{(* preevaluation separation equivalent to sequence *)
side_conditions = [],
hypotheses = [  (--`PreEval lv expr s1 s2`--)],
		(*----------------------------------------*)
conclusion =	(--`^SEM_EQType (Seq (Simple expr) s1) s2`--)},
{(* postevaluation separation equivalent to sequence *)
side_conditions = [],
hypotheses = [	(--`PostEval s1 expr s2`--)],
		(*----------------------------------------*)
conclusion =	(--`^SEM_EQType (Seq s1 (Simple expr)) s2`--)},

{(* associativity of sequence *)
side_conditions = [],
hypotheses = [],
		(*----------------------------------------*)
conclusion =	(--`^SEM_EQType (Seq (Seq s1 s2) s3) (Seq s1 (Seq s2 s3))`--)},
{(* composition of sequence *)
side_conditions = [],
hypotheses = [	(--`^SEM_EQType sf1 sf2`--),
		(--`^SEM_EQType ss1 ss2`--)],
		(*----------------------------------------*)
conclusion =	(--`^SEM_EQType (Seq sf1 ss1) (Seq sf2 ss2)`--)},
{(* null effect of EmptyStmt (left) *)
side_conditions = [],
hypotheses = [],
		(*----------------------------------------*)
conclusion =	(--`^SEM_EQType (Seq EmptyStmt s) s`--)},
{(* null effect of EmptyStmt (right) *)
side_conditions = [],
hypotheses = [],
		(*----------------------------------------*)
conclusion =	(--`^SEM_EQType (Seq s EmptyStmt) s`--)},

{(* one-armed If equiv to IfElse with Empty else *)
side_conditions = [],
hypotheses = [],
		(*----------------------------------------*)
conclusion =	(--`^SEM_EQType (IfElse t s EmptyStmt) (If t s)`--)}
]}
end;

val c = ref 1;
save_thm("SEM_EQ_REFL",		el (!c) SEM_EQ_rules); c:=(!c)+1;
val SEM_EQ_SYM_IMP =		el (!c) SEM_EQ_rules; c:=(!c)+1;
save_thm("SEM_EQ_SYM", prove((--`SEM_EQ s1 s2 = SEM_EQ s2 s1`--),
    EQ_TAC THENL [
	ACCEPT_TAC (SPEC_ALL SEM_EQ_SYM_IMP),
	ACCEPT_TAC (SPECL [(--`s2:CStmt`--),(--`s1:CStmt`--)] SEM_EQ_SYM_IMP)
    ]
));
save_thm("SEM_EQ_TRANS", LIFT_QUANT_RULE (el (!c) SEM_EQ_rules)); c:=(!c)+1;

save_thm("Preeval_seq_equiv",LIFT_QUANT_RULE (el (!c) SEM_EQ_rules));c:=(!c)+1;
save_thm("Posteval_seq_equiv",	el (!c) SEM_EQ_rules); c:=(!c)+1;

save_thm("Seq_semantic_assoc",	el (!c) SEM_EQ_rules); c:=(!c)+1;
save_thm("Seq_semantic_comp",	el (!c) SEM_EQ_rules); c:=(!c)+1;
save_thm("Empty_null_left",	el (!c) SEM_EQ_rules); c:=(!c)+1;
save_thm("Empty_null_right",	el (!c) SEM_EQ_rules); c:=(!c)+1;

save_thm("IfElse_EQ_If",	el (!c) SEM_EQ_rules); c:=(!c)+1;

close_theory();
export_theory();

(* end of $Source: /users/lal/black/hol/Disser/RCS/semeq.sml,v $ *)