``` ```

# Definition of Subclassing

``` Require Import Calculus. Require Import List. Module SetProgram(My_Program: Program). Import My_Program. ```
 Relation: subclass
``` Inductive Subclass: ClassSym -> ClassSym -> Prop :=      | SC_Class:     forall (C: ClassSym),       (Subclass C C)          | SC_Extends:     forall (A B C: ClassSym),       (classSuper A) = (Some B) ->       (Subclass B C) ->       (Subclass A C) . Definition ParamValueList := (list (ParamSym * Value)). Definition ValueList := (list Value). ```
 Predicate: check membership of a given binding in a list of bindings (field symbol, value)
``` Inductive FieldValueList_contains: FieldValueList -> FieldSym -> Value -> Prop :=   | FieldValueList_contains_head:     forall (f: FieldSym) (v: Value) (fvs: FieldValueList),       (FieldValueList_contains (FieldValue_cons f v fvs) f v)          | FieldValueList_contains_tail:     forall (f f': FieldSym) (v v': Value) (fvs: FieldValueList),       (FieldValueList_contains fvs f v) ->       (FieldValueList_contains (FieldValue_cons f' v' fvs) f v) . ```
 Equality on variable symbols is decidable
``` Lemma VarSym_eqdec:   forall (n m: VarSym), { n = m } + { n <> m } . ```
 Function: converts a value to a term
``` Fixpoint value_to_term (v: Value): Term :=   match v with     | (Value_mk C fvs) => (Term_new C (fieldValueList_to_fieldTermList fvs))   end   with fieldValueList_to_fieldTermList (fvs: FieldValueList): FieldTermList :=   match fvs with     | FieldValue_nil => FieldTerm_nil     | (FieldValue_cons f v fvs') =>       (FieldTerm_cons f (value_to_term v) (fieldValueList_to_fieldTermList fvs'))   end. ```
 Predicate: `t` is a value
``` Definition term_evaluated (t: Term): Prop :=   exists v: Value, (value_to_term v) = t. ```
 Function: promotes a path to a term
``` Definition path_to_term (p: Path): Term :=   match p with     | (Path_this) => Term_this     | (Path_param x) => (Term_param x)     | (Path_var n) => (Term_var n)     | (Path_value v) => (value_to_term v)   end . Lemma path_to_term_this:   forall (p: Path),     (path_to_term p) = Term_this ->     (p = Path_this) . Lemma path_to_term_param:   forall (p: Path) (x: ParamSym),     (path_to_term p) = (Term_param x) ->     (p = (Path_param x)) . Lemma path_to_term_var:   forall (p: Path) (n: VarSym),     (path_to_term p) = (Term_var n) ->     (p = (Path_var n)) . Lemma path_to_term_select:   forall (p: Path) (q: Path) (f: FieldSym),     (path_to_term p) = (Term_select q f) ->     False . Lemma path_to_term_call:   forall (p: Path) (q: Path) (m: MethodSym) (xts: ParamTermList),     (path_to_term p) = (Term_call q m xts) ->     False . Lemma path_to_term_let:   forall (p: Path) (T: type) (t u: Term),     (path_to_term p) = (Term_loc T t u) ->     False . Lemma path_to_term_new:   forall (p: Path) (C: ClassSym) (fts: FieldTermList),     (path_to_term p) = (Term_new C fts) ->     exists v: Value,       (p = (Path_value v)) /\ ((value_to_term v) = (Term_new C fts)) . End SetProgram. ```
Index