(* $Header: /users/lal/black/hol/Disser/RCS/wellformed.sml,v 1.16 1997/07/09 23:46:57 black Exp $ *)
(* *created  "Mon Dec 23 09:21:17 1996" *by "Paul E. Black" *)
(* *modified "Tue Jul  8 15:15:10 1997" *by "Paul E. Black" *)

(*-----------------------------------------------------------------------
		 Definition of Well Formed conditions
			after Peter Homeier
 -----------------------------------------------------------------------*)

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

new_parent "c_ast";

add_theorems_to_sml "c_ast";

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

load_library {lib = find_library "ind_def", theory = "-"};

(* it is bothersome to fully declare this every time *)
val CONS_Term = (--`CONS:Cvar->Cvar list->Cvar list`--);

(*-----------------------------------------------------------------------
	Define what we mean by the first set (list) is a subset of the 
	second set (list).
 -----------------------------------------------------------------------*)

val IS_SUBSET = new_list_rec_definition("IS_SUBSET",
    (--`(!(a:'a list). IS_SUBSET [] a = T) /\
	      (!a h l. IS_SUBSET (CONS h l) a =
			(IS_EL h a) /\ (IS_SUBSET l a))`--));


(*-----------------------------------------------------------------------
	Define that the two C types are conforming types.
 -----------------------------------------------------------------------*)

(* type predicates *)
rec_define "CType_AX"
	`(is_Ptr Char = F) /\
	 (is_Ptr Int = F) /\
	 (is_Ptr Void = F) /\
	 (is_Ptr (Ptr t) = T) /\
	 (is_Ptr (Array t1 sz) = F) /\
	 (is_Ptr (Struct s) = F) /\
	 (is_Ptr (Funty t2 t3) = F)`;

rec_define "CType_AX"
	`(is_Array Char = F) /\
	 (is_Array Int = F) /\
	 (is_Array Void = F) /\
	 (is_Array (Ptr t) = F) /\
	 (is_Array (Array t1 sz) = T) /\
	 (is_Array (Struct s) = F) /\
	 (is_Array (Funty t2 t3) = F)`;

rec_define "CType_AX"
	`(is_Struct Char = F) /\
	 (is_Struct Int = F) /\
	 (is_Struct Void = F) /\
	 (is_Struct (Ptr t) = F) /\
	 (is_Struct (Array t1 sz) = F) /\
	 (is_Struct (Struct s) = T) /\
	 (is_Struct (Funty t2 t3) = F)`;

rec_define "CType_AX"
	`(is_Funty Char = F) /\
	 (is_Funty Int = F) /\
	 (is_Funty Void = F) /\
	 (is_Funty (Ptr t) = F) /\
	 (is_Funty (Array t1 sz) = F) /\
	 (is_Funty (Struct s) = F) /\
	 (is_Funty (Funty t2 t3) = T)`;

(* subtype accessors *)
rec_define "CType_AX" `(CTy_subty (Ptr st) = st) /\
		       (CTy_subty (Array st1 sz) = st1)`;

rec_define "CType_AX" `Struct_subty (Struct s) = s`;

rec_define "CType_AX" `Funty_frmty (Funty ft tt) = ft`;

rec_define "CType_AX" `Funty_toty  (Funty ft tt) = tt`;

rec_define "CType_AX"
	`(Ctypes_conform Char t = (Char = t)) /\
	 (Ctypes_conform Int t = (Int = t)) /\
	 (Ctypes_conform Void t = (Void = t)) /\
	 (Ctypes_conform (Ptr st) t =
		((is_Ptr t \/ is_Array t) =>
			(Ctypes_conform st (CTy_subty t)) | F)) /\
	 (Ctypes_conform (Array st1 sz) t =
		((is_Ptr t \/ is_Array t) =>
			(Ctypes_conform st1 (CTy_subty t)) | F)) /\
	 (Ctypes_conform (Struct s1) t =
		(is_Struct t => (s1 = Struct_subty t) | F)) /\
	 (Ctypes_conform (Funty it ot) t =
		(is_Funty t => Ctypes_conform it (Funty_frmty t) /\
			      (Ctypes_conform ot (Funty_toty t)) | F))`;

(*-----------------------------------------------------------------------
	Define that the first set (list) is a subset of the second
	set (list) given type conformance.
 -----------------------------------------------------------------------*)

rec_define "Cvar_AX" `Cvar_name (Var n d ty) = n`;

rec_define "Cvar_AX" `Cvar_disamb (Var n d ty) = d`;

rec_define "Cvar_AX" `Cvar_type (Var n d ty) = ty`;

rec_define "Cvar_AX"
	`TYPE_CONF (Var n d ty) v2 =
                (n = Cvar_name v2) /\ (d = Cvar_disamb v2)
                        /\ Ctypes_conform ty (Cvar_type v2)`;

(* this decomposes both Cvars at once, so is easier to use than TYPE_CONF *)
save_thm("TYPE_CONF_DEF",
    prove((--`TYPE_CONF (Var n d ty) (Var n2 d2 ty2) =
		(n = n2) /\ (d = d2) /\ Ctypes_conform ty ty2`--),
	  REWRITE_TAC [TYPE_CONF,Cvar_name,Cvar_disamb,Cvar_type]));

new_list_rec_definition("IS_SUBSET_TYCONF",
    (--`(!a. IS_SUBSET_TYCONF [] a = T) /\
	      (!a h l. IS_SUBSET_TYCONF (CONS h l) a =
		(SOME_EL (TYPE_CONF h) a) /\ (IS_SUBSET_TYCONF l a))`--));


(*-----------------------------------------------------------------------
	Define what we mean by the difference between two sets (lists).
	SETDIFF a b is a - b.
 -----------------------------------------------------------------------*)

val SETDIFF = new_list_rec_definition("SETDIFF",
    (--`(!(b:'a list). SETDIFF [] b = []) /\
	      (!b h l. SETDIFF (CONS h l) b =
		let diffTail = (SETDIFF l b) in
			(IS_EL h b) => diffTail |
			    (CONS h diffTail))`--));


(*-----------------------------------------------------------------------
	Generate unique variants of a set of variables with respect to
	a base set.  (Homeier Section 10.1, pp 231-234)
 -----------------------------------------------------------------------*)

new_constant{Name = "variants", Ty = ==`:Cvar list->Cvar list->Cvar list`==};

(*-----------------------------------------------------------------------
	A list of variables is piece-wise distinct if 
	no variable is repeated.  (Homeier, Section 10.1, p 234)
 -----------------------------------------------------------------------*)

val DL = new_list_rec_definition("DL",
    (--`(DL ([]:'a list) = T) /\
      (!h l. DL (CONS h l) = ~(IS_EL h l) /\ (DL l))`--));


(*-----------------------------------------------------------------------
	A list of variables is well-formed if every variable in the
	list is well-formed.  (Homeier, Section 10.4.2, p 256)
 -----------------------------------------------------------------------*)

(* SKIMP - formally define *)
val WF_xs = new_definition (
   "WF_xs",
    (--`! (x:Cvar list). WF_xs x = T`--)
);


(*-----------------------------------------------------------------------
	Define logical versions of program variables.  Logical variables
	are only used in assertions, and therefore represent the same
	value during execution.  They are used as "initial" values.
 -----------------------------------------------------------------------*)

new_constant{Name = "logicals", Ty = ==`:Cvar list->Cvar list`==};

(*-----------------------------------------------------------------------
	Return the global variables used by functions called in
	a statement.
 -----------------------------------------------------------------------*)

new_constant{Name = "GV_c", Ty = ==`:CStmt->Cvar list`==};

(*-----------------------------------------------------------------------
	Return the free variables of a statement.
 -----------------------------------------------------------------------*)

new_constant{Name = "FV_c", Ty = ==`:CStmt->Cvar list`==};

(*-----------------------------------------------------------------------
	Return the free variables of a HOL expression (an assertion).
 -----------------------------------------------------------------------*)

new_constant{Name = "FV_a", Ty = ==`:bool->Cvar list`==};

(*-----------------------------------------------------------------------
	A command is well-formed if While statements have well-formed
	termination conditions, Call statements use variables reasonably
	(eg, don't pass a global as a reference), and logical variables
	aren't used in expressions.  (Homeier, Section 10.4.2, p 258)
 -----------------------------------------------------------------------*)

(* SKIMP - formally define *)
val WF_c = new_definition (
   "WF_c",
    (--`! (s:CStmt). WF_c s = T`--)
);


(*-----------------------------------------------------------------------
	A function specification is well-formed syntactically, eg, all
	variables used in the body are either parameters or globals.
	This corresponds to Homeier's WF_proc_syntax (p 259).
 -----------------------------------------------------------------------*)

local val WF_fn_synType = (--`WF_fn_syntax:bool->Cfunction->bool->bool`--)
in
val {desc=WF_fn_syn_rules, induction_thm=WF_fn_syn_ind} =
    Inductive_def.new_inductive_definition {
    name = "WF_fn_syntax",
    patt = ((--`^WF_fn_synType pre func post`--), []),
    fixity = Prefix,
    rules = [
{
side_conditions = [],
hypotheses = [  (--`x = APPEND (formls:Cvar list) globls`--),
		(--`x0 = logicals x`--),
		(--`WF_xs x`--),
		(--`DL (x:Cvar list)`--),
		(--`WF_c body`--),
		(--`IS_SUBSET (GV_c body) globls`--),
		(--`IS_SUBSET (FV_c body) x`--),
		(--`IS_SUBSET_TYCONF (FV_a pre) x`--),
		(--`IS_SUBSET_TYCONF (FV_a post) (APPEND x x0)`--)
		(* SKIMP - no recursive call checks for now *)],
		(*----------------------------------------*)
conclusion =	(--`^WF_fn_synType pre (Func name formls globls
						(SOMEBody body)) post`--)}
]}
end;

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

(*-----------------------------------------------------------------------
	Create AND's of pairwise equivalency of two lists of Cvars.
	For instance, given (--`pairwiseEqual [a;b] [c;d]`--), return
		|- pairwiseEqual [a;b] [c;d] = (a=c) /\ (b=d)
	where a, b, c, and d are Var's.
 -----------------------------------------------------------------------*)

new_constant{Name = "pairwiseEqual", Ty = ==`:Cvar list->Cvar list->bool`==};

(*-----------------------------------------------------------------------
	Partial correctness conditions for C functions with pre- and
	postconditions.  This is a "template" for function calls.
	This corresponds to Homeier's WF_proc (p 260).  Any return
	value is indicated by a predicate on C_Result in the post-
	condition.
 -----------------------------------------------------------------------*)

local val WF_fnpType = (--`WF_fnp:bool->Cfunction->bool->bool`--)
in
val {desc=WF_fnp_rules, induction_thm=WF_fnp_ind} =
    Inductive_def.new_inductive_definition {
    name = "WF_fnp",
    patt = ((--`^WF_fnpType pre func post`--), []),
    fixity = Prefix,
    rules = [
{(* A function with pre- and postconditions is partially correct if the body
    can be proved partially correct. *)
side_conditions = [],
hypotheses = [	(--`(x:Cvar list) = APPEND formls globls`--),
		(--`x0 = logicals x`--),
		(--`WF_fn_syntax pre (Func name formls globls (SOMEBody body))
								post`--),
		(--`(Partial:bool->CStmt->bool->bool) ((pairwiseEqual x x0)
							/\ pre) body post`--)],
		(*----------------------------------------*)
conclusion =	(--`^WF_fnpType pre (Func name formls globls (SOMEBody body))
								post`--)}
]}
end;

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

close_theory();
export_theory();

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