(* generated by Ott 0.10.14 from: lj.ott *)

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import Natmap.
Require Import FMaps.
Require Import EqNat.
(** syntax *)
Definition f := nat.
Definition m := nat.
Definition var := nat.
Definition dcl := nat.
Definition oid := nat.
Definition j := nat.

Inductive 
cl : Set := 
   cl_dcl : dcl -> cl
 | cl_object : cl
.

Inductive 
x : Set := 
   x_var : var -> x
 | x_this : x
.

Inductive 
ty : Set := 
   ty_def : cl -> ty
.

Module XOrd <: OrderedType.
  Definition t := x.
  Definition eq (t1 t2 : t) : Prop:= match t1, t2 with
                                       x_this, x_this => True
                                       | x_var n1, x_var n2 => eq_nat n1 n2
                                       | _, _ => False
                                     end.
  Definition lt (t1 t2 : t) : Prop:= match t1, t2 with
                                       | x_var n1, x_var n2 => lt n1 n2
                                       | x_var _, x_this => True
                                       | _, _ => False
                                     end.
  Theorem eq_refl : forall y : t, eq y y. 
    intro y; case y; intros; simpl.
    apply eq_nat_refl.
    auto.
  Qed.
  Theorem eq_sym : forall (y z: t), eq y z-> eq z y.
    intros y z; case y; case z; simpl; auto.
    clear y z; induction v.
    intro v; case v; intros.
    exact H.
    simpl in H; elimtype False; exact H.
    intros v0; case v0; intros.
    simpl in H; elimtype False; exact H.
    simpl in *|-*; apply IHv; exact H.
  Qed.
  Theorem eq_trans : forall (w y z: t), eq w y -> eq y z -> eq w z.
    intros w y z; case w; case y; case z; simpl ; try (intros; elimtype False; auto; fail).
    clear w y z.
    intros w y z; generalize w y z; clear w y z.
    induction w; induction y; induction z; simpl; intros; auto.
    elimtype False; exact H.
    apply (IHw _ _ H H0).
    auto.
  Qed.
  Theorem lt_trans : forall w y z : t, lt w y -> lt y z -> lt w z.
    intros w y z; case w; case y; case z; try (simpl; auto; fail); clear w y z.
    intros w y z; simpl; auto.
    intros H H0; apply (lt_trans _ _ _ H H0).
    intros.
    simpl in H0; elimtype False; exact H0.
  Qed.
  Theorem lt_not_eq : forall (y z : t), lt y z ->~ eq y z.
    intros y z; case y; case z; try( simpl; auto).
    induction v; induction v; unfold not; simpl; auto; intros.
    apply (lt_irrefl 0 H). 
    destruct v; try omega.
    simpl in H0; exact H0.
    rewrite (eq_nat_eq _ _ H0) in H.
    apply (lt_irrefl _ H).
  Qed.
  Lemma compare : forall y z : t, Compare lt eq y z.
    intros.
    destruct y; destruct z.
    elim (le_lt_dec v v0); intros.
    elim (eq_nat_dec v v0); intros.
    rewrite a0.
    exact (EQ _ (eq_refl (x_var v0))).
    assert (v < v0).
    omega.
    assert (lt (x_var v) (x_var v0)).
    simpl; exact H.
    exact (LT _ H0).
    assert (lt (x_var v0) (x_var v)).
    simpl; exact b.
    exact (GT _ H).
    assert (lt (x_var v) x_this).
    simpl; auto.
    exact (LT _ H).
    assert (lt (x_var v) x_this).
    simpl; auto.
    exact (GT _ H).
    exact (EQ _ (eq_refl x_this)).
  Qed.
End XOrd.

Module XMap := FMapList.Make (XOrd).

Inductive 
vd : Set := 
   vd_def : ty -> var -> vd
.


Inductive 
list_s : Set := 
   Nil_list_s : list_s
 | Cons_list_s : s -> list_s -> list_s

with s : Set := 
   s_new : var -> cl -> s
 | s_ass : var -> x -> s
 | s_read : var -> x -> f -> s
 | s_write : x -> f -> x -> s
 | s_call : var -> x -> m -> list x -> s
 | s_if : x -> x -> s -> s -> s
 | s_block : list_s -> s
.

Definition 
  Ss : Set := list s
  .

(**** Induction principle for statements ****)
Section s_rect.

Variables
   (P : s -> Type)
   (Q : list_s -> Type).

Hypotheses
   (H1 : forall var cl, P (s_new var cl))
   (H2 : forall var x, P (s_ass var x))
   (H3 : forall var x f, P (s_read var x f))
   (H4 : forall x y f, P (s_write x f y))
   (H5 : forall var x m l, P (s_call var x m l))
   (H6 : forall x y s1 s2, P (s1 ) -> P (s2) -> P (s_if x y s1 s2))
   (H7 : forall l, Q l -> P (s_block l))
   (H8 : Q Nil_list_s)
   (H9 : forall l s, P s -> Q l -> Q (Cons_list_s s l)).

Fixpoint s_rect' s : P s :=
   match s as s return P s with
     | s_new var' cl' => H1 var' cl'
     | s_ass var' x' => H2 var' x'
     | s_read var' x' f' => H3 var' x' f'
     | s_write x' f' y => H4 x' y f'
     | s_call var' x' m' l => H5 var' x' m' l
     | s_if x' y' s1 s2 => H6 x' y' s1 s2 (s_rect' s1) (s_rect' s2)
     | s_block l => H7 l 
       ((fix list_s_rect' (l : list_s) : Q l :=
         match l as l return Q l with
           | Nil_list_s => H8
           | Cons_list_s s' l' => H9 l' s' (s_rect' s') (list_s_rect' l')
         end) l)
   end.

Fixpoint list_s_rect' (s_list : list_s) : Q s_list :=
  match s_list as s_list return Q s_list with 
    | Nil_list_s => H8
    | Cons_list_s s' l' => H9 l' s' 
      ((fix s_rect' (s' : s) : P s' :=
        match s' as s' return P s' with
          | s_new var' cl' => H1 var' cl'
          | s_ass var' x' => H2 var' x'
          | s_read var' x' f' => H3 var' x' f'
          | s_write x' f' y => H4 x' y f'
          | s_call var' x' m' l => H5 var' x' m' l
          | s_if x' y' s1 s2 => H6 x' y' s1 s2 (s_rect' s1) (s_rect' s2)
          | s_block l => H7 l (list_s_rect' l) 
        end) s')
      (list_s_rect' l')
  end.

End s_rect.

Definition s_list_ind (P : s -> Prop) (Q : list_s -> Prop) := list_s_rect' P Q.

Definition s_list_rec (P : s -> Set) (Q : list_s -> Set) := list_s_rect' P Q.


Inductive 
ms : Set := 
   ms_def : ty -> m -> list vd -> ms
.

Inductive 
mb : Set := 
   mb_def : Ss -> x -> mb
.

Inductive 
fd : Set := 
   fd_def : ty -> f -> fd
.

Inductive 
md : Set := 
   md_def : ms -> mb -> md
.

Definition
fds : Set := list fd
.

Inductive 
cld : Set := 
   cld_def : dcl -> cl -> fds -> list md -> cld
.

Inductive 
v : Set := 
   v_null : v
 | v_oid : oid -> v
.

Definition
L : Set := XMap.t v
.

Definition
H : Set := NatMap.t (cl * NatMap.t v).

Definition
P : Set := list cld
.

Definition
tyopt : Set := option ty
.

Definition
tys : Set := list ty
.

Definition
G : Set := XMap.t ty
.

Definition
vopt : Set := option v
.

Inductive 
config : Set := 
   config_normal : L -> H -> Ss -> config
 | config_npe : L -> H -> config
.

Definition
F : Set := list f
.

Inductive 
menv : Set := 
   menv_def : list var -> mb -> menv
.

Definition
M : Set := list m
.

Inductive 
mty : Set := 
   mty_def : tys -> ty -> mty
.

Definition
T : Set := XMap.t x
.

Definition
clopt : Set := option cl
.

(** auxiliary functions on the statement list types *)

Fixpoint map_list_s (A:Set) (f:s->A) (l:list_s) {struct l} : list A :=
  match l with
  | Nil_list_s => nil
  | Cons_list_s h tl_ => cons (f h) (map_list_s A f tl_)
  end.
Implicit Arguments map_list_s.

Fixpoint make_list_s (l:list s) : list_s :=
  match l with
  | nil  => Nil_list_s
  | cons h tl_ => Cons_list_s h (make_list_s tl_)
  end.

Fixpoint unmake_list_s (l:list_s) :  list s :=
  match l with
  | Nil_list_s => nil
  | Cons_list_s h tl_ =>  cons h (unmake_list_s tl_)
  end.

Fixpoint app_list_s (l m:list_s) {struct l} : list_s :=
  match l with
  | Nil_list_s => m
  | Cons_list_s h tl_ => Cons_list_s h (app_list_s tl_ m)
  end.

Fixpoint names ( p: P ) {struct p} : list cl :=
  match p with
    nil => cons cl_object nil
    | cons (cld_def dcl cl fds mds) clds => cons (cl_dcl dcl) (names clds)
  end.

Fixpoint names' ( pcl_list: list (P*cld) ) {struct pcl_list} : list cl :=
  match pcl_list with
    nil => cons cl_object nil
    | cons (_, (cld_def dcl cl fds mds)) clds => cons (cl_dcl dcl) (names' clds)
  end.


Fixpoint path (p : P) (cl' : cl) {struct p} : list cld :=
  match p, cl' with 
    | cons (cld_def dcl' cl'' fds' mds') clds, cl_dcl dcl => 
      if (eq_nat_dec dcl dcl') then (cons (cld_def dcl' cl'' fds' mds') (path clds cl'')) else (path clds (cl_dcl dcl))
    | _, _ => nil
  end.

Definition get_fs (fds : list fd) : list f :=
  map (fun (fd' : fd) => match fd' with fd_def ty' f' => f' end) fds.

Fixpoint concat (A : Set) (l: list (list A)) {struct l}: list A :=
  match l with 
    nil => nil
    | cons a l' => app a (concat A l')
  end.

Implicit Arguments concat [A].

Fixpoint get_parent (cld' : cld) : cl :=
  match cld' with cld_def dcl' cl' fds' mds' => cl' end.

Definition ext_fs (clds : list cld) : list f :=
   concat (map (fun (cld' : cld) => match cld' with cld_def dcl' cl' fds' mds' => get_fs fds' end) clds).

Definition fields (p : P) (cl' : cl) : F := ext_fs (path p cl').

Definition get_ms (mds : list md) : M :=
	   map (fun (md' : md) => match md' with md_def (ms_def ty' m' vds) mb => m' end) mds.

Definition ext_ms (clds : list cld) : M :=
	   concat (map (fun (cld' : cld) =>
					 match cld' with 
					   cld_def dcl' cl' fds' mds' => get_ms mds' end) 
			clds).

Definition inherited_methods (p : P) (cl' : cl) : M := 
  match (path p cl') with 
    nil => ext_ms nil
    | cons x cl' => ext_ms (app cl' nil)
  end.

Definition methods (p : P) (cl' : cl) : M := ext_ms (path p cl').

Fixpoint get_fty (fds : list fd) (f' : f) {struct fds} : option ty :=
	 match fds with
	       cons (fd_def ty' f'') fds' => if (eq_nat_dec f' f'') then (Some ty') else (get_fty fds' f')
	       | _ => None
	  end.

Fixpoint ext_fty (clds : list cld) (f' : f) {struct clds} : option ty :=
	 match clds with 
	       cons (cld_def dcl' cl' fds' mds') clds' =>
	       	    match (get_fty fds' f') with
		    	  Some ty' => Some ty'
			  | None => ext_fty clds' f'
                    end
		| nil => None
	  end.
	       
Definition ftype (p : P) (cl' : cl) (f' : f) : option ty :=  ext_fty (path p cl') f'.

Definition get_vdstys (vds : list vd) : tys :=
	  map (fun (vd' : vd) => match vd' with vd_def ty' var' => ty' end) vds.

Definition get_vdsvars (vds : list vd) : (list var) :=
	  map (fun (vd' : vd) => match vd' with vd_def ty' var' => var' end) vds.

Definition get_all_mds (clds : list cld) : (list md) :=
	   concat (map (fun (cld' : cld) => match cld' with cld_def dcl' cl' fds' mds' => (mds') end) clds).

Definition filter_mds (mds : list md) (m' : m) : (list md) :=
	   fold_right (fun (md' : md) (mds' : list md) => 
	   	     match md' with 
		     	   md_def (ms_def ty' m'' vds') mb' =>
			   if (eq_nat_dec m'' m') then cons md' mds' else mds' 
		     end) nil mds.

Definition ext_mty (md' : md) : mty :=
	   match md' with md_def (ms_def ty' m' vds') mb' => mty_def (get_vdstys ( vds')) ty' end.

Definition get_md (p : P) (cl' : cl) ( m' : m) : option md := head (filter_mds (get_all_mds (path p cl')) m').

Definition mtype (p : P) (cl' : cl) ( m' : m) : option mty := match (get_md p cl' m') with
                                                         Some x => Some (ext_mty x)
                                                         | None => None
                                                       end.

Definition ext_menv (md' : md) : menv :=
	   match md' with 
	   	 md_def (ms_def ty' m' vds') mb' => menv_def (get_vdsvars vds') mb'
           end.

 Definition find_menv (p : P) (cl' : cl) (m' : m) : option menv := match (get_md p cl' m') with
                                                                     None => None
                                                                     | Some md' => Some (ext_menv md')
                                                                   end. 

Definition tr_x (t : T) (x' : x) : x :=
	   match (XMap.find x' t) with
	      None => x'
	      | Some x'' => x''
	   end.

Definition tr_var (t' : T) ( v' : var ) : var :=
	   match (XMap.find (x_var v') t') with 
	   	 None => v' 
		 | Some (x_var v'') => v''
		 | Some (x_this) => v'
	   end.

Fixpoint
 tr_s ( t : T) (s' : s)  {struct s'}: s :=
 match s' with 
   s_new var' cl' => s_new (tr_var t var') cl'
   | s_ass var' x' => s_ass (tr_var t var')  (tr_x t x')
   | s_read var' x' f' => s_read (tr_var t var') (tr_x t x') f'
   | s_write x' f' y' => s_write (tr_x t x') f' (tr_x t y')
   | s_call var' x' m' xs' => s_call (tr_var t var') (tr_x t x') m' (map (tr_x t) xs')
   | s_if x' y' s' s'' => s_if (tr_x t x') (tr_x t y') (tr_s t s') (tr_s t s'')
   | s_block Ss' => s_block (tr_Ss t Ss')
 end
with
  tr_Ss (t' : T) (Ss' : list_s) {struct Ss'} : list_s :=
  match Ss' with
    Nil_list_s => Nil_list_s
    | Cons_list_s s' Ss'' => Cons_list_s (tr_s t' s' )  (tr_Ss t' Ss'')
  end.

Fixpoint in_nat_list (b : nat) (B : list nat) {struct B} : bool :=
  match B with 
    nil => false 
    | cons b' B' => if eq_nat_dec b' b then true else in_nat_list b B' 
  end.
	 
Fixpoint in_x_list (b : x) (B : list x) {struct B} : bool :=
  match B with 
    nil => false 
    | cons b' B' => match b', b with
                      x_this, x_this => true
                      | x_var n, x_var n' => if eq_nat_dec n n' then true else in_x_list b B'
                      | _, _ => in_x_list b B'
                    end
  end.

Fixpoint list_inter (A: Type) (a b : list A) (f : A -> list A -> bool) {struct a}: list A :=
	 match a with 
	       nil => nil
	      | cons el a' => if (f el b) then cons el (list_inter A a' b f) else (list_inter A a' b f)
	 end.

(* defns subtyping *)

Inductive
(* defn direct *)

sty_direct : P -> ty -> ty -> Prop :=
 | sty_dir : forall (md_list:list md) (P5:P) (dcl5:dcl) (cl5:cl) (fds5:fds),
      In  (cld_def dcl5 cl5 fds5 md_list) P5  ->
     sty_direct P5 (ty_def (cl_dcl dcl5)) (ty_def cl5).


Inductive
(* defn one *)

sty_one : P -> ty -> ty -> Prop :=
| sty_from_direct : forall (P5:P) (ty5:ty) (ty':ty),
  sty_direct P5 ty5 ty' ->
  sty_one P5 ty5 ty'
| sty_opt_refl : forall (P5:P),
  sty_one P5 (ty_def (cl_object)) (ty_def (cl_object))
| sty_reflexive : forall (P5:P) (dcl':dcl) (cl':cl) (fds' : fds) (mds : list md),
  In  (cld_def dcl' cl' fds' mds) P5  ->
  sty_one P5 (ty_def (cl_dcl dcl')) (ty_def (cl_dcl dcl'))
| sty_transitive : forall (P5:P) (ty5:ty) (ty'':ty) (ty':ty),
  sty_one P5 ty5 ty' ->
  sty_one P5 ty' ty'' ->
  sty_one P5 ty5 ty''.


(* defn many *)
Inductive
sty_many : P -> tys -> tys -> Prop :=
 | sty_man : forall (ty_ty'_list:list (ty*ty)) (P5:P),
     (sty_one_list (map (fun (ty' : ty*ty) => (P5,fst ty',snd ty')) ty_ty'_list)) ->
     sty_many P5  ( (map (fun (ty':ty*ty) => fst ty' ) ty_ty'_list))   
     (map (fun (ty':ty*ty) => snd ty') ty_ty'_list)
with
sty_one_list : list (P*ty*ty) -> Prop :=
 | Nil_sty_one_list : sty_one_list nil
 | Cons_sty_one_list : forall (P5:P) (ty5:ty) (ty':ty) (l':list (P*ty*ty)),
      (sty_one P5 ty5 ty') -> sty_one_list l' ->
      sty_one_list (cons (P5,ty5,ty') l')
.

Inductive
(* defn option *)

sty_option : P -> tyopt -> tyopt -> Prop :=
 | sty_opt : forall (P5:P) (tyopt5:tyopt) (tyopt':tyopt) (ty5:ty) (ty':ty),
      tyopt5  =   Some  ty5   ->
      tyopt'  =   Some  ty'   ->
     sty_one P5 ty5 ty' ->
     sty_option P5 tyopt5 tyopt'
with
sty_opt_list : list (P * tyopt*tyopt) -> Prop :=
 | Nil_sty_opt_list : sty_opt_list nil
 | Cons_sty_opt_list : forall (P5:P) (ty5 ty' : ty) (oty oty' :tyopt) (l':list (P* tyopt*tyopt)),
      (sty_option P5 oty oty') -> sty_opt_list l' ->
      sty_opt_list (cons (P5, oty, oty') l').

(* defns well_formedness *)

Inductive
(* defn type *)

wf_type : P -> ty -> Prop :=
 | wf_valid_dcl : forall (P5:P) (cl5:cl),
      In  cl5  (names P5  )  ->
     wf_type P5 (ty_def cl5).

(* defn stmt *)

Inductive
wf_stmt : P -> G -> s -> Prop :=
 | wf_new : forall (P5:P) (G5:G) (var5:var) (cl5:cl),
     sty_option P5  (Some  (ty_def cl5))   (XMap.find (x_var var5) G5)  ->
     wf_stmt P5 G5 (s_new var5 cl5)
 | wf_var_assign : forall (P5:P) (G5:G) (var5:var) (x5:x),
     sty_option P5  (XMap.find x5 G5)  (XMap.find (x_var var5) G5) ->
     wf_stmt P5 G5 (s_ass var5 x5)
 | wf_field_read : forall (P5:P) (G5:G) (var5:var) (x5:x) (f5:f) (cl5:cl) (ty5:ty),
       (XMap.find x5 G5)   =   Some  (ty_def cl5)   ->
       ftype  P5   cl5   f5   =   Some  ty5   ->
     sty_option P5  (Some  ty5)   (XMap.find (x_var var5) G5) ->
     wf_stmt P5 G5 (s_read var5 x5 f5)
 | wf_field_write : forall (P5:P) (G5:G) (x5:x) (f5:f) (y:x) (cl5:cl) (ty5:ty),
       (XMap.find x5 G5)  =   Some  (ty_def cl5)   ->
       ftype  P5   cl5   f5   =   Some  ty5   ->
     sty_option P5  (XMap.find y G5)   (Some ty5)  ->
     wf_stmt P5 G5 (s_write x5 f5 y)
 | wf_mcall : forall (y_ty_list:list (x*ty)) (P5:P) (G5:G) (var5:var) (x5:x) (m5:m) (cl5:cl) (ty':ty),
       XMap.find x5 G5 =   Some  (ty_def cl5)   ->
       mtype  P5   cl5   m5   =  Some (mty_def  ((map (fun (y: x*ty) => snd y) y_ty_list))  ty')  ->
     (sty_opt_list (map (fun (y:x*ty) => (P5,  (XMap.find (fst y) G5), Some  (snd y) )) y_ty_list)) ->
     sty_option P5  (Some  ty') (XMap.find (x_var var5) G5)  ->
     wf_stmt P5 G5 (s_call var5 x5 m5 (map (fun (y:x*ty) => fst y) y_ty_list))
 | wf_if : forall (P5:P) (G5:G) (x5:x) (y:x) (s1:s) (s2:s),
      sty_option P5  (XMap.find x5 G5) (XMap.find y G5) \/  sty_option P5 (XMap.find y G5) (XMap.find x5 G5) ->
     wf_stmt P5 G5 s1 ->
     wf_stmt P5 G5 s2 ->
     wf_stmt P5 G5 (s_if x5 y s1 s2)
 | wf_block : forall (s_list:list_s) (P5:P) (G5:G),
     (wf_stmt_list (map_list_s (fun (s_:s) => (P5,G5,s_)) s_list)) ->
     wf_stmt P5 G5 (s_block s_list)
with
wf_stmt_list : list (P*G*s) -> Prop :=
 | Nil_wf_stmt_list : wf_stmt_list nil
 | Cons_wf_stmt_list : forall (P5:P) (G5:G) (s_:s) (l':list (P*G*s)),
   (wf_stmt P5 G5 s_) -> wf_stmt_list l' ->
      wf_stmt_list (cons (P5, G5, s_) l').


Fixpoint distinct (A : Type) (l : list A) : Prop :=
  match l with 
    nil => True
    | cons a l' => (~ In a l') /\ distinct A l'
  end.

(* defn meth *)
Inductive 
wf_meth : P -> ty -> md -> Prop :=
 | wf_method : forall (s_list:list_s) (ty_var_list : list (ty*var)) (P5:P) (cl5:cl) (ty_5:ty) (m5:m) (x5:x) (G5:G),
     (wf_type_list  (map (fun (ty_var:(ty*var)) => (P5,fst ty_var)) ty_var_list)) ->
      (distinct _ (map (fun (ty_var:(ty*var)) => (P5,snd ty_var)) ty_var_list)) ->
     G5  =   (fold_left (fun (m : XMap.t ty) (p : x*ty) => XMap.add (fst p) (snd p) m) (cons (x_this, (ty_def cl5)) 
       (map (fun (ty_var : ty*var) => (x_var (snd ty_var), fst ty_var)) ty_var_list)) (XMap.empty ty)) ->
     (wf_stmt_list (map_list_s (fun (s_:s) => (P5,G5,s_)) s_list)) ->
     sty_option P5  (XMap.find x5 G5) (Some  ty_5)  ->
     wf_meth P5 (ty_def cl5) (md_def (ms_def ty_5 m5  (map (fun (ty_var:ty*var) => 
       (vd_def (fst ty_var) (snd ty_var))) ty_var_list)) (mb_def (unmake_list_s s_list) x5))
with
  wf_type_list : list (P*ty) -> Prop :=
| Nil_wf_type_list : wf_type_list nil
| Cons_wf_type_list : forall (P5:P) (ty_:ty) (l':list (P*ty)),
  (wf_type P5 ty_) -> wf_type_list l' ->
  wf_type_list (cons (P5,ty_) l').

(* defn class *)

Inductive
wf_class : P -> cld -> Prop :=
 | wf_cl : forall (ty_f_list:list (ty*f)) (md_list:list md) (P5:P) (dcl5:dcl) (cl5:cl) (fds5:fds),
     wf_type P5 (ty_def cl5) ->
     cl_dcl dcl5 <> cl5 ->
      fds5  =    (map (fun (tyf:ty*f) => (fd_def (fst tyf) (snd tyf) )) ty_f_list) ->
      distinct f (map (fun (tyf:ty*f) => snd tyf) ty_f_list)  ->
      list_inter _ (map (fun (tyf : ty*f) => snd tyf ) ty_f_list) (fields  P5   cl5) in_nat_list= nil  ->
     (wf_type_list (map (fun (tyf:ty*f) => (P5,fst tyf)) ty_f_list)) ->
     (wf_meth_list (map (fun (md':md) => (P5,(ty_def (cl_dcl dcl5)),md')) md_list)) ->
     distinct _ (map (fun (md' : md) => match md' with md_def (ms_def _ m' _) _=> m' end) md_list) ->
      (forall (m' : m) (ty' : ty) (vd_list : list vd) (mb' : mb),
        In (md_def (ms_def ty' m' vd_list) mb') md_list -> In  m' (methods P5 cl5)  ->
        Some (mty_def (get_vdstys vd_list) ty')
          = mtype  P5 cl5 m')  ->
     wf_class P5 (cld_def dcl5 cl5 fds5 md_list)
with
wf_meth_list : list (P*ty*md) -> Prop :=
 | Nil_wf_meth_list : wf_meth_list nil
 | Cons_wf_meth_list : forall (P5:P) (dcl5:dcl) (md':md) (l':list (P*ty*md)),
      (wf_meth P5 (ty_def (cl_dcl dcl5)) md') -> wf_meth_list l' ->
      wf_meth_list (cons (P5, (ty_def (cl_dcl dcl5)), md') l').

(* defn program *)

Inductive
wf_prog : P -> Prop :=
 | wf_program : forall (cld_list:list cld) (p:P),
      p = cld_list ->
      distinct _ (names p)  ->
      (wf_class_list  (map (fun (cld_:cld) => (p,cld_)) cld_list)) ->
      wf_prog p
with
wf_class_list : list (P*cld) -> Prop :=
| Nil_wf_class_list : wf_class_list nil
| Cons_wf_class_list : forall (P5:P) (cld_:cld) (l':list (P*cld)),
  (wf_class P5 cld_) -> wf_class_list l' ->
  (exists cl', get_parent cld_ = cl' /\ In cl' (names' l') ) ->
  wf_class_list (cons (P5,cld_) l').

(* defn object *)
Inductive
wf_obj : P -> H -> vopt -> tyopt -> Prop :=
 | wf_null : forall (P5:P) (H5:H) (tyopt5:tyopt) (ty5:ty),
      tyopt5  =   Some  ty5   ->
     wf_obj P5 H5  (Some  v_null)  tyopt5
 | wf_object : forall (P5:P) (H5:H) (oid5:oid) (tyopt5:tyopt),
   sty_option P5  (match NatMap.find oid5 H5 with
                     None => None
                     | Some tyfs => Some (ty_def (fst tyfs))
                                         end)  tyopt5 ->
                     wf_obj P5 H5  (Some (v_oid oid5)) tyopt5.

(* defn stack *)

Inductive
  wf_stck : P -> G -> H -> L -> Prop :=
| wf_stack : forall (P5:P) (G5:G) (H5:H) (L5:L),
   (forall  x5 , XMap.mem x5 G5 = true -> exists ty5 ,
     XMap.find x5 G5 = Some ty5 /\ wf_type P5 ty5 /\ wf_obj P5 H5 (XMap.find x5 L5) (Some ty5))  ->
   wf_stck P5 G5 H5 L5.

(* defn heap *)

Inductive
wf_hp : P -> H -> Prop :=
| wf_heap : forall (P5:P) (H5:H),
   (forall  (oid5 : oid), NatMap.mem oid5 H5 = true-> exists  cl5, (match (NatMap.find oid5 H5) with
                                                         None => None
                                                         | Some tyfs => Some (fst tyfs)
                                                       end) = Some cl5 /\ wf_type P5 (ty_def cl5)  /\ 
   (forall f5, In f5 (fields P5 cl5) -> exists ty5, ftype P5 cl5 f5 = Some  ty5 /\ 
  
     wf_obj P5 H5 ((match NatMap.find oid5 H5  with 
                                     None => None
	                             | Some tyfs => NatMap.find f5 (snd tyfs)
	                           end)) (Some ty5)))  ->
   wf_hp P5 H5.

(* defn config *)

Inductive
  wf_config : P -> G -> config -> Prop :=
| wf_all : forall (s_list : Ss) (P5:P) (G5:G) (L5:L) (H5:H),
  wf_prog P5 ->
  wf_hp P5 H5 ->
  wf_stck P5 G5 H5 L5 ->
  (wf_stmt_list (map (fun (s_:s) => (P5,G5,s_)) s_list)) ->
  wf_config P5 G5 (config_normal L5 H5 s_list)
| wf_all_npe : forall (P5:P) (G5:G) (L5:L) (H5:H),
  wf_config P5 G5 (config_npe L5 H5).
      

(* defns smallstep *)

Fixpoint init_field_map (fs: list f) : NatMap.t v :=
  match fs with
    nil => NatMap.empty v
    | cons f' fs' => NatMap.add f' v_null (init_field_map fs')
  end.

Inductive
(* defn reduce *)

reduce : config -> P -> config -> Prop :=
| field_read_npe : forall (L5:L) (H5:H) (var5:var) (x5:x) (f5:f) (Ss5:Ss) (P5:P),
  XMap.find x5 L5 = Some v_null ->
  reduce (config_normal L5 H5 ( (s_read var5 x5 f5) :: Ss5) ) P5 (config_npe L5 H5)

| field_write_npe : forall (L5:L) (H5:H) (x5:x) (f5:f) (y:x) (Ss5:Ss) (P5:P),
  XMap.find x5 L5 = Some v_null ->
  reduce (config_normal L5 H5 ( (s_write x5 f5 y) :: Ss5) ) P5 (config_npe L5 H5)

| mcall_npe : forall (y_list:list x) (L5:L) (H5:H) (var5:var) (x5:x) (m5:m) (Ss5:Ss) (P5:P),
  XMap.find x5 L5 = Some v_null ->
  reduce (config_normal L5 H5 ( (s_call var5 x5 m5 y_list) :: Ss5) ) P5 (config_npe L5 H5)

| new : forall (f_list : list f) (L5:L) (H5:H) (var5:var) (cl5:cl) (Ss5:Ss) (P5:P) (oid5:oid) (H':H),
  NatMap.mem oid5 H5 = false -> fields P5 cl5 = f_list ->
  H' = NatMap.add oid5 (cl5, init_field_map f_list) H5 -> 
  reduce (config_normal L5 H5 ( (s_new var5 cl5) :: Ss5)) P5 (config_normal (XMap.add (x_var var5) (v_oid oid5) L5) H' Ss5)

| var_assign : forall (L5:L) (H5:H) (var5:var) (x5:x) (Ss5:Ss) (P5:P) (v5:v),
  XMap.find x5 L5 = Some v5 ->
  reduce (config_normal L5 H5 ( (s_ass var5 x5) :: Ss5 )) P5 (config_normal (XMap.add (x_var var5) v5 L5) H5 Ss5)
    
| field_read : forall (L5:L) (H5:H) (var5:var) (x5:x) (f5:f) (Ss5:Ss) (P5:P) (v5:v) (oid5:oid),
  XMap.find x5 L5 = Some (v_oid oid5) ->
  (match (NatMap.find oid5 H5) with 
     None => None
     | Some cl_map => NatMap.find f5 (snd cl_map)
   end) = Some v5->
  reduce (config_normal L5 H5 ((s_read var5 x5 f5) ::  Ss5) ) P5 (config_normal (XMap.add (x_var var5) v5 L5) H5 Ss5)

| field_write : forall (L5:L) (H5:H) (x5:x) (f5:f) (y:x) (Ss5:Ss) (P5:P) (oid5:oid) (v5:v),
  XMap.find x5 L5 = Some (v_oid oid5) ->
  XMap.find y L5 = Some v5 ->
  reduce (config_normal L5 H5 ((s_write x5 f5 y) :: Ss5)) P5 (config_normal L5 (match (NatMap.find oid5 H5) with 
                                                                               None => H5 
						                               | Some tyfs => NatMap.add oid5 (fst tyfs,(NatMap.add f5 v5 (snd tyfs))) H5
						                                end) Ss5)
| mcall : forall (big_list : list (x*var*var*v)) (L5:L) (H5:H) (var_5:var)
  (x5:x) (m5:m) (Ss5:Ss) (P5:P) (L':L) (T5:T) (Ss':Ss) (y':x) (cl5:cl) (x' : var) (y:x) (o : oid) 
  (z : (cl * NatMap.t v)),

  XMap.find x5 L5 = Some (v_oid o) ->

  NatMap.find o H5 = Some z ->

  find_menv P5 (fst z) m5  = Some (menv_def (map (fun (yp : x*var*var*v) => snd (fst (fst yp) )) big_list) (mb_def Ss' y)) ->

  distinct _ (map (fun (yp :x*var*var*v) => (x_var (snd (fst yp)))) big_list) ->

 ( forall (x' : x), In x' (map (fun (yp :x*var*var*v) => (x_var (snd (fst yp)))) big_list) -> ~ XMap.In x' L5) ->
 
 ~ XMap.In (x_var x') L5 ->
 
 ~ In x' (map (fun (yp :x*var*var*v) =>  (snd (fst yp))) big_list) ->
  
  valid_lookup_list L5 (map (fun (yp:x*var*var*v) => (fst (fst (fst (yp))), snd yp)) big_list) ->
  
  L' =  XMap.add (x_var x') (v_oid o) (fold_right (fun (yp:x*var*var*v) m=> XMap.add (x_var (snd (fst yp))) (snd yp) m) L5 big_list) ->

  T5 =  XMap.add x_this (x_var x') (fold_right (fun (yp : x*var*var*v) m => XMap.add (x_var (snd (fst (fst yp)))) (x_var (snd (fst yp))) m)  (XMap.empty x) big_list)  ->

  tr_x T5 y = y' ->
  
  reduce (config_normal L5 H5 ((s_call var_5 x5 m5 (map (fun (yp:x*var*var*v) => (fst ( fst (fst yp)))) big_list)) :: Ss5)) P5 (config_normal L' H5 (app (unmake_list_s (tr_Ss T5 (make_list_s Ss'))) ((s_ass var_5 y') :: Ss5)))

| if_true : forall (L5:L) (H5:H) (x5:x) (y:x) (s1:s) (s2:s) (Ss5:Ss) (P5:P) (v5:v) (w:v),
  XMap.find x5 L5 = Some v5 ->
  XMap.find y L5 = Some w ->
  v5 = w ->
  reduce (config_normal L5 H5 ((s_if x5 y s1 s2) :: Ss5) ) P5 (config_normal L5 H5 (s1 :: Ss5))

| if_false : forall (L5:L) (H5:H) (x5:x) (y:x) (s1:s) (s2:s) (Ss5:Ss) (P5:P) (v5:v) (w:v),
  XMap.find x5 L5 = Some v5 ->
  XMap.find y L5 = Some w ->
  v5 <> w ->
  reduce (config_normal L5 H5 ((s_if x5 y s1 s2) :: Ss5) ) P5 (config_normal L5 H5 (s2 :: Ss5))
        
| block : forall (s_list:list_s) (L5:L) (H5:H) (Ss5:Ss) (P5:P),
  reduce (config_normal L5 H5 ( (s_block s_list) :: Ss5) ) P5 (config_normal L5 H5 (app (unmake_list_s s_list) Ss5))
            
    with
      valid_lookup_list : L -> list (x*v) -> Prop :=
      valid_lookup_nil : forall (L5 : L), valid_lookup_list L5 nil
    | valid_lookup_cons : forall (L5:L) (y:x) (v':v) (l':list (x*v)),
      XMap.find y L5  = Some v' -> valid_lookup_list L5  l' ->
         valid_lookup_list L5 (cons (y,v') l').