Definition of Substitutions |
Require Import Calculus.
Require Import Arith.
Require Import MatchCompNat.
Require Import List.
Module SetProgram(My_Program: Program).
Import My_Program.
Require Subclassing.
Module My_Subclassing := Subclassing.SetProgram(My_Program).
Import My_Subclassing.
Function: substitutes q for this in path p
|
Definition thisSubst_in_path (p: Path) (q: Path): Path :=
match p with
| (Path_this) => q
| _ => p
end
.
Function: substitutes q for this in type T
|
Definition thisSubst_in_type (T: type) (q: Path): type :=
match T with
| (type_virtual p L) => (type_virtual (thisSubst_in_path p q) L)
| (type_class C) => (type_class C)
end
.
Function: substitutes q for this in term t
|
Fixpoint thisSubst_in_term (t: Term) (q: Path) {struct t}: Term :=
match t with
| (Term_this) => (path_to_term q)
| (Term_param x) => (Term_param x)
| (Term_var n) => (Term_var n)
| (Term_select p f) => (Term_select (thisSubst_in_path p q) f)
| (Term_new C fts) => (Term_new C (thisSubst_in_fieldTermList fts q))
| (Term_call p m xts) => (Term_call (thisSubst_in_path p q) m (thisSubst_in_paramTermList xts q))
| (Term_loc T u u') => (Term_loc (thisSubst_in_type T q) (thisSubst_in_term u q) (thisSubst_in_term u' q))
end
Function: substitutes q for this in bindings fts
|
with thisSubst_in_fieldTermList (fts: FieldTermList) (q: Path) {struct fts}: FieldTermList :=
match fts with
| FieldTerm_nil => FieldTerm_nil
| (FieldTerm_cons f t fts') => (FieldTerm_cons f (thisSubst_in_term t q) (thisSubst_in_fieldTermList fts' q))
end
Function: substitutes q for this in bindings xts
|
with thisSubst_in_paramTermList (xts: ParamTermList) (q: Path) {struct xts}: ParamTermList :=
match xts with
| ParamTerm_nil => ParamTerm_nil
| (ParamTerm_cons x t xts') => (ParamTerm_cons x (thisSubst_in_term t q) (thisSubst_in_paramTermList xts' q))
end
.
Function: substitutes v for the variable n in path p
|
Definition varSubst_in_path (p: Path) (n: VarSym) (v: Value): Path :=
match p with
| (Path_this) => (Path_this)
| (Path_param x) => (Path_param x)
| (Path_var i) =>
(match_comp_nat3 i n Path
(Path_var i)
(Path_value v)
(Path_var (pred i))
)
| (Path_value v) => (Path_value v)
end
.
Function: substitutes v for the variable n in type T
|
Definition varSubst_in_type (T: type) (n: VarSym) (v: Value): type :=
match T with
| (type_virtual p L) => (type_virtual (varSubst_in_path p n v) L)
| (type_class C) => (type_class C)
end
.
Function: substitutes v for the variable n in term t
|
Fixpoint varSubst_in_term (t: Term) (n: VarSym) (v: Value) {struct t}: Term :=
match t with
| (Term_this) => (Term_this)
| (Term_param x) => (Term_param x)
| (Term_var i) =>
(match_comp_nat3 i n Term
(Term_var i)
(value_to_term v)
(Term_var (pred i))
)
| (Term_select p f) => (Term_select (varSubst_in_path p n v) f)
| (Term_new C fts) => (Term_new C (varSubst_in_fieldTermList fts n v))
| (Term_call p m xts) => (Term_call (varSubst_in_path p n v) m (varSubst_in_paramTermList xts n v))
| (Term_loc T u u') => (Term_loc (varSubst_in_type T n v) (varSubst_in_term u n v) (varSubst_in_term u' (S n) v))
end
Function: substitutes v for the variable n in bindings xts
|
with varSubst_in_paramTermList (xts: ParamTermList) (n: VarSym) (v: Value) {struct xts}: ParamTermList :=
match xts with
| (ParamTerm_nil) => (ParamTerm_nil)
| (ParamTerm_cons x t xts') => (ParamTerm_cons x (varSubst_in_term t n v) (varSubst_in_paramTermList xts' n v))
end
Function: substitutes v for the variable n in bindings fts
|
with varSubst_in_fieldTermList (fts: FieldTermList) (n: VarSym) (v: Value) {struct fts}: FieldTermList :=
match fts with
| (FieldTerm_nil) => (FieldTerm_nil)
| (FieldTerm_cons f t fts') => (FieldTerm_cons f (varSubst_in_term t n v) (varSubst_in_fieldTermList fts' n v))
end
.
Function: substitutes v for the parameter x in path p
|
Definition paramSubst_in_path (p: Path) (x: ParamSym) (v: Value): Path :=
match p with
| (Path_param y) => if (ParamSym_eq x y) then (Path_value v) else p
| _ => p
end
.
Function: substitutes v for the parameter x in type T
|
Definition paramSubst_in_type (T: type) (x: ParamSym) (v: Value): type :=
match T with
| (type_virtual p L) => (type_virtual (paramSubst_in_path p x v) L)
| (type_class C) => (type_class C)
end
.
Function: substitutes v for the parameter x in term t
|
Fixpoint paramSubst_in_term (t: Term) (x: ParamSym) (v: Value) {struct t}: Term :=
match t with
| (Term_this) => (Term_this)
| (Term_param y) => if (ParamSym_eq x y) then (value_to_term v) else (Term_param y)
| (Term_var n) => (Term_var n)
| (Term_select p f) => (Term_select (paramSubst_in_path p x v) f)
| (Term_new C fts) => (Term_new C (paramSubst_in_fieldTermList fts x v))
| (Term_call p m xts) => (Term_call (paramSubst_in_path p x v) m (paramSubst_in_paramTermList xts x v))
| (Term_loc T u u') => (Term_loc (paramSubst_in_type T x v) (paramSubst_in_term u x v) (paramSubst_in_term u' x v))
end
Function: substitutes v for the parameter x in bindings fts
|
with paramSubst_in_fieldTermList (fts: FieldTermList) (x: ParamSym) (v: Value) {struct fts}: FieldTermList :=
match fts with
| FieldTerm_nil => FieldTerm_nil
| (FieldTerm_cons f t fts') => (FieldTerm_cons f (paramSubst_in_term t x v) (paramSubst_in_fieldTermList fts' x v))
end
Function: substitutes v for the parameter x in bindings xts
|
with paramSubst_in_paramTermList (xts: ParamTermList) (x: ParamSym) (v: Value) {struct xts}: ParamTermList :=
match xts with
| ParamTerm_nil => ParamTerm_nil
| (ParamTerm_cons y t xts') => (ParamTerm_cons y (paramSubst_in_term t x v) (paramSubst_in_paramTermList xts' x v))
end
.
| Function: converts a list of values to a list of terms |
Fixpoint paramValueList_to_ParamTermList (xvs: list (ParamSym * Value)) {struct xvs}: ParamTermList :=
match xvs with
| nil => (ParamTerm_nil)
| (x,v) :: xvs' => (ParamTerm_cons x (value_to_term v) (paramValueList_to_ParamTermList xvs'))
end
.
Function: substitutes values vs for the parameter xs in term t when xvs = (xs,vs)
|
Definition map_paramSubst_in_term (t: Term) (xvs: list (ParamSym * Value)): Term :=
(fold_left
(fun t' (xv: (ParamSym * Value)) => let (x,v) := xv in (paramSubst_in_term t' x v))
xvs
t
)
.
Definition map_paramSubst_in_path (p: Path) (xvs: list (ParamSym * Value)): Path :=
(fold_left
(fun p' (xv: (ParamSym * Value)) => let (x,v) := xv in (paramSubst_in_path p' x v))
xvs
p
)
.
Definition map_paramSubst_in_type (T: type) (xvs: list (ParamSym * Value)): type :=
(fold_left
(fun T' (xv: (ParamSym * Value)) => let (x,v) := xv in (paramSubst_in_type T' x v))
xvs
T
)
.
Definition map_paramSubst_in_fieldTermList (fts: FieldTermList) (xvs: list (ParamSym * Value)): FieldTermList :=
(fold_left
(fun fts' (xv: (ParamSym * Value)) => let (x,v) := xv in (paramSubst_in_fieldTermList fts' x v))
xvs
fts
)
.
Definition map_paramSubst_in_paramTermList (xts: ParamTermList) (xvs: list (ParamSym * Value)): ParamTermList :=
(fold_left
(fun xts' (xv: (ParamSym * Value)) => let (x,v) := xv in (paramSubst_in_paramTermList xts' x v))
xvs
xts
)
.
Lemma polySubst_in_pathThis:
forall (xvs: list (ParamSym * Value)),
(map_paramSubst_in_path Path_this xvs) = Path_this
.
Lemma polySubst_in_pathVar:
forall (xvs: list (ParamSym * Value)),
forall (i: VarSym),
(map_paramSubst_in_path (Path_var i) xvs) = (Path_var i)
.
Lemma polySubst_in_pathValue:
forall (xvs: list (ParamSym * Value)),
forall (v: Value),
(map_paramSubst_in_path (Path_value v) xvs) = (Path_value v)
.
Lemma polySubst_in_pathParam:
forall (xvs: list (ParamSym * Value)) (x: ParamSym),
(
(forall (v: Value), ~(In (x, v) xvs)) /\
(map_paramSubst_in_path (Path_param x) xvs) = (Path_param x)
) \/
exists v: Value,
(In (x, v) xvs) /\
(map_paramSubst_in_path (Path_param x) xvs) = (Path_value v)
.
Lemma polySubst_in_pathParam_corollary:
forall (xvs: list (ParamSym * Value)),
forall (x: ParamSym),
(map_paramSubst_in_path (Path_param x) xvs) = (Path_param x) \/
exists v: Value,
(map_paramSubst_in_path (Path_param x) xvs) = (Path_value v)
.
Lemma polySubst_in_fieldTermNil:
forall (xvs : list (ParamSym * Value)),
(map_paramSubst_in_fieldTermList FieldTerm_nil xvs) = FieldTerm_nil
.
Lemma polySubst_in_fieldTermCons:
forall (xvs : list (ParamSym * Value)),
forall (f: FieldSym) (t: Term) (fts: FieldTermList),
(map_paramSubst_in_fieldTermList (FieldTerm_cons f t fts) xvs) =
(FieldTerm_cons f (map_paramSubst_in_term t xvs) (map_paramSubst_in_fieldTermList fts xvs))
.
Lemma polySubst_in_paramTermNil:
forall (xvs : list (ParamSym * Value)),
(map_paramSubst_in_paramTermList ParamTerm_nil xvs) = ParamTerm_nil
.
Lemma polySubst_in_paramTermCons:
forall (xvs : list (ParamSym * Value)),
forall (x: ParamSym) (t: Term) (xts: ParamTermList),
(map_paramSubst_in_paramTermList (ParamTerm_cons x t xts) xvs) =
(ParamTerm_cons x (map_paramSubst_in_term t xvs) (map_paramSubst_in_paramTermList xts xvs))
.
Lemma polySubst_in_termThis:
forall (xvs: list (ParamSym * Value)),
(map_paramSubst_in_term Term_this xvs) = Term_this
.
Lemma polySubst_in_termVar:
forall (i: VarSym) (xvs: list (ParamSym * Value)),
(map_paramSubst_in_term (Term_var i) xvs) = (Term_var i)
.
Lemma polySubst_in_termSelect:
forall (xvs: list (ParamSym * Value)),
forall (p: Path) (f: FieldSym),
(map_paramSubst_in_term (Term_select p f) xvs) =
(Term_select (map_paramSubst_in_path p xvs) f)
.
Lemma polySubst_in_termNew:
forall (xvs: (list (ParamSym * Value))),
forall (C: ClassSym) (fts: FieldTermList),
(map_paramSubst_in_term (Term_new C fts) xvs) =
(Term_new C (map_paramSubst_in_fieldTermList fts xvs))
.
Lemma polySubst_in_termCall:
forall (xvs: (list (ParamSym * Value))),
forall (p: Path) (m: MethodSym) (xts: ParamTermList),
(map_paramSubst_in_term (Term_call p m xts) xvs) =
(Term_call (map_paramSubst_in_path p xvs) m (map_paramSubst_in_paramTermList xts xvs))
.
Lemma polySubst_in_termLet:
forall (xvs: (list (ParamSym * Value))),
forall (T: type) (t u: Term),
(map_paramSubst_in_term (Term_loc T t u) xvs) =
(Term_loc (map_paramSubst_in_type T xvs) (map_paramSubst_in_term t xvs) (map_paramSubst_in_term u xvs))
.
Lemma polySubst_in_typeVirtual:
forall (xvs: list (ParamSym * Value)),
forall (p: Path) (L: TypeSym),
(map_paramSubst_in_type (type_virtual p L) xvs) =
(type_virtual (map_paramSubst_in_path p xvs) L)
.
Lemma polySubst_in_typeClass:
forall (xvs: list (ParamSym * Value)),
forall (C: ClassSym),
(map_paramSubst_in_type (type_class C) xvs) =
(type_class C)
.
Definition polySubst_in_termValue_prop1 (v: Value): Prop :=
forall (xvs: (list (ParamSym * Value))),
(map_paramSubst_in_term (value_to_term v) xvs) = (value_to_term v)
.
Definition polySubst_in_termValue_prop2 (fvs: FieldValueList): Prop :=
forall (xvs: (list (ParamSym * Value))),
(map_paramSubst_in_fieldTermList (fieldValueList_to_fieldTermList fvs) xvs) =
(fieldValueList_to_fieldTermList fvs)
.
| Values are invariant by repeated substitutions for parameters |
Lemma polySubst_in_termValue:
forall (v: Value) (xvs: (list (ParamSym * Value))),
(map_paramSubst_in_term (value_to_term v) xvs) = (value_to_term v)
.
Lemma polySubst_in_termParam:
forall (xvs: list (ParamSym * Value)) (x: ParamSym),
(
(forall (v: Value), ~(In (x, v) xvs)) /\
(map_paramSubst_in_term (Term_param x) xvs) = (Term_param x)
) \/
exists v: Value,
(In (x, v) xvs) /\
(map_paramSubst_in_term (Term_param x) xvs) = (value_to_term v)
.
Lemma polySubst_in_termParam_corollary:
forall (xvs: list (ParamSym * Value)),
forall (x: ParamSym),
(map_paramSubst_in_term (Term_param x) xvs) = (Term_param x) \/
exists v: Value,
(map_paramSubst_in_term (Term_param x) xvs) = (value_to_term v)
.
End SetProgram.