Theory Lightweight_Java_Definition

(*  Title:       Lightweight Java, the definition
    Authors:     Rok Strnisa <rok@strnisa.com>, 2006
                 Matthew Parkinson <matt@matthewp.com>, 2006
    Maintainer:
    Note:        This file should _not_ be modified directly. Please see the
                 accompanying README file.
*)

(* generated by Ott 0.20.3 from: lj_common.ott lj_base.ott lj.ott *)
theory Lightweight_Java_Definition
imports Main "HOL-Library.Multiset"
begin

(** warning: the backend selected ignores the file structure informations *)
(** syntax *)
type_synonym "j" = "nat"
type_synonym "f" = "string"
type_synonym "meth" = "string"
type_synonym "var" = "string"
type_synonym "dcl" = "string"
type_synonym "oid" = "nat"
datatype "fqn" =
   fqn_def "dcl"

datatype "cl" =
   cl_object
 | cl_fqn "fqn"

datatype "x" =
   x_var "var"
 | x_this

datatype "vd" =
   vd_def "cl" "var"

type_synonym "X" = "x list"
datatype "ctx" =
   ctx_def

type_synonym "vds" = "vd list"
datatype "s" =
   s_block "s list"
 | s_ass "var" "x"
 | s_read "var" "x" "f"
 | s_write "x" "f" "x"
 | s_if "x" "x" "s" "s"
 | s_new "var" "ctx" "cl"
 | s_call "var" "x" "meth" "X"

datatype "meth_sig" =
   meth_sig_def "cl" "meth" "vds"

datatype "meth_body" =
   meth_body_def "s list" "x"

datatype "fd" =
   fd_def "cl" "f"

datatype "meth_def" =
   meth_def_def "meth_sig" "meth_body"

type_synonym "fds" = "fd list"
type_synonym "meth_defs" = "meth_def list"
datatype "cld" =
   cld_def "dcl" "cl" "fds" "meth_defs"

type_synonym "ctxcld" = "(ctx × cld)"
datatype "ty" =
   ty_top
 | ty_def "ctx" "dcl"

datatype "v" =
   v_null
 | v_oid "oid"

type_synonym "clds" = "cld list"
type_synonym "ctxclds" = "ctxcld list"
type_synonym "fs" = "f list"
type_synonym "ty_opt" = "ty option"
type_synonym "tys" = "ty list"
type_synonym "L" = "x ⇀ v"
type_synonym "H" = "oid ⇀ (ty × (f ⇀ v))"
datatype "Exception" =
   ex_npe

type_synonym "P" = "clds"
type_synonym "ctxcld_opt" = "ctxcld option"
type_synonym "nn" = "nat"
type_synonym "ctxclds_opt" = "ctxclds option"
type_synonym "fs_opt" = "fs option"
type_synonym "meths" = "meth list"
datatype "ty_opt_bot" =
   ty_opt_bot_opt "ty_opt"
 | ty_opt_bot_bot

type_synonym "meth_def_opt" = "meth_def option"
type_synonym "ctxmeth_def_opt" = "(ctx × meth_def) option"
datatype "mty" =
   mty_def "tys" "ty"

type_synonym "Γ" = "x ⇀ ty"
type_synonym "v_opt" = "v option"
datatype "config" =
   config_normal "P" "L" "H" "s list"
 | config_ex "P" "L" "H" "Exception"

type_synonym "T" = "x ⇀ x"


(** library functions *)
lemma [mono]:"
         (!! x. f x --> g x) ==> list_all (%b. b) (map f foo_list)-->
                    list_all (%b. b) (map g foo_list) "
   apply(induct_tac foo_list, auto) done

lemma [mono]: "case_prod f p = f (fst p) (snd p)" by (simp add: split_def)

(** definitions *)
(*defns class_name_def *)
inductive class_name :: "cld ⇒ dcl ⇒ bool"
where
(* defn class_name *)

class_nameI: "class_name ((cld_def dcl cl fds meth_defs)) (dcl)"

(*defns superclass_name_def *)
inductive superclass_name :: "cld ⇒ cl ⇒ bool"
where
(* defn superclass_name *)

superclass_nameI: "superclass_name ((cld_def dcl cl fds meth_defs)) (cl)"

(*defns class_fields_def *)
inductive class_fields :: "cld ⇒ fds ⇒ bool"
where
(* defn class_fields *)

class_fieldsI: "class_fields ((cld_def dcl cl fds meth_defs)) (fds)"

(*defns class_methods_def *)
inductive class_methods :: "cld ⇒ meth_defs ⇒ bool"
where
(* defn class_methods *)

class_methodsI: "class_methods ((cld_def dcl cl fds meth_defs)) (meth_defs)"

(*defns method_name_def *)
inductive method_name :: "meth_def ⇒ meth ⇒ bool"
where
(* defn method_name *)

method_nameI: "method_name ((meth_def_def (meth_sig_def cl meth vds) meth_body)) (meth)"

(*defns distinct_names_def *)
inductive distinct_names :: "P ⇒ bool"
where
(* defn distinct_names *)

dn_defI: "⟦ P  =    ((List.map (%((cld_XXX::cld),(dcl_XXX::dcl)).cld_XXX) cld_dcl_list))    ;
 list_all (λf. f)  ((List.map (%((cld_XXX::cld),(dcl_XXX::dcl)).class_name (cld_XXX) (dcl_XXX)) cld_dcl_list))  ;
 distinct ( ((List.map (%((cld_XXX::cld),(dcl_XXX::dcl)).dcl_XXX) cld_dcl_list)) ) ⟧ ⟹
distinct_names (P)"

(*defns find_cld_def *)
inductive find_cld :: "P ⇒ ctx ⇒ fqn ⇒ ctxcld_opt ⇒ bool"
where
(* defn find_cld *)

fc_emptyI: "find_cld (  []  ) (ctx) (fqn) ( None )"

| fc_cons_trueI: "⟦ P  =    ([(cld)] @ cld_list)    ;
 cld  =  (cld_def dcl cl fds meth_defs) ⟧ ⟹
find_cld (P) (ctx) ((fqn_def dcl)) ( (Some (  ( ctx , cld )  )) )"

| fc_cons_falseI: "⟦ cld  =  (cld_def dcl' cl fds meth_defs)  ;
 (cl_fqn (fqn_def dcl))  ≠  (cl_fqn (fqn_def dcl'))  ;
find_cld (  (cld_list)  ) (ctx) ((fqn_def dcl)) (ctxcld_opt)⟧ ⟹
find_cld (  ([(cld)] @ cld_list)  ) (ctx) ((fqn_def dcl)) (ctxcld_opt)"

(*defns find_type_def *)
inductive find_type :: "P ⇒ ctx ⇒ cl ⇒ ty_opt ⇒ bool"
where
(* defn find_type *)

ft_objI: "find_type (P) (ctx) (cl_object) ( (Some ( ty_top )) )"

| ft_nullI: "⟦find_cld (P) (ctx) (fqn) ( None )⟧ ⟹
find_type (P) (ctx) ((cl_fqn fqn)) ( None )"

| ft_dclI: "⟦find_cld (P) (ctx) ((fqn_def dcl)) ( (Some (  ( ctx' , cld )  )) )⟧ ⟹
find_type (P) (ctx) ((cl_fqn (fqn_def dcl))) ( (Some ( (ty_def ctx' dcl) )) )"

(*defns path_length_def *)
inductive path_length :: "P ⇒ ctx ⇒ cl ⇒ nn ⇒ bool"
where
(* defn path_length *)

pl_objI: "path_length (P) (ctx) (cl_object) ( 0 )"

| pl_fqnI: "⟦find_cld (P) (ctx) (fqn) ( (Some (  ( ctx' , cld )  )) ) ;
superclass_name (cld) (cl) ;
path_length (P) (ctx') (cl) (nn)⟧ ⟹
path_length (P) (ctx) ((cl_fqn fqn)) ( ( nn +  1  ) )"

(*defns acyclic_clds_def *)
inductive acyclic_clds :: "P ⇒ bool"
where
(* defn acyclic_clds *)

ac_defI: "⟦ ∀  ctx   fqn .   (    (  (∃  ctx'   cld  .  find_cld (P) (ctx) (fqn) ( (Some (  ( ctx' , cld )  )) ) )  )   ⟶     (∃  nn  .  path_length (P) (ctx) ((cl_fqn fqn)) (nn) )      )  ⟧ ⟹
acyclic_clds (P)"

(*defns find_path_rec_def *)
inductive find_path_rec :: "P ⇒ ctx ⇒ cl ⇒ ctxclds ⇒ ctxclds_opt ⇒ bool"
where
(* defn find_path_rec *)

fpr_objI: "find_path_rec (P) (ctx) (cl_object) (ctxclds) ( Some ( ctxclds ) )"

| fpr_nullI: "⟦  (  ¬ ( acyclic_clds (P) )  )   ∨  find_cld (P) (ctx) (fqn) ( None ) ⟧ ⟹
find_path_rec (P) (ctx) ((cl_fqn fqn)) (ctxclds) ( None )"

| fpr_fqnI: "⟦ acyclic_clds (P)  ∧  find_cld (P) (ctx) (fqn) ( (Some (  ( ctx' , cld )  )) )  ;
superclass_name (cld) (cl) ;
find_path_rec (P) (ctx') (cl) ( ctxclds @[   ( ctx' , cld )   ] ) (ctxclds_opt)⟧ ⟹
find_path_rec (P) (ctx) ((cl_fqn fqn)) (ctxclds) (ctxclds_opt)"

(*defns find_path_def *)
inductive find_path :: "P ⇒ ctx ⇒ cl ⇒ ctxclds_opt ⇒ bool"
where
(* defn find_path *)

fp_defI: "⟦find_path_rec (P) (ctx) (cl) ( [] ) (ctxclds_opt)⟧ ⟹
find_path (P) (ctx) (cl) (ctxclds_opt)"

(*defns find_path_ty_def *)
inductive find_path_ty :: "P ⇒ ty ⇒ ctxclds_opt ⇒ bool"
where
(* defn find_path_ty *)

fpty_objI: "find_path_ty (P) (ty_top) ( Some (  []  ) )"

| fpty_dclI: "⟦find_path (P) (ctx) ((cl_fqn (fqn_def dcl))) (ctxclds_opt)⟧ ⟹
find_path_ty (P) ((ty_def ctx dcl)) (ctxclds_opt)"

(*defns fields_in_path_def *)
inductive fields_in_path :: "ctxclds ⇒ fs ⇒ bool"
where
(* defn fields_in_path *)

fip_emptyI: "fields_in_path ( [] ) ( [] )"

| fip_consI: "⟦class_fields (cld) ( ((List.map (%((cl_XXX::cl),(f_XXX::f)).(fd_def cl_XXX f_XXX)) cl_f_list)) ) ;
fields_in_path ( (ctxcld_list) ) (fs) ;
 fs'  =   (  ((List.map (%((cl_XXX::cl),(f_XXX::f)).f_XXX) cl_f_list))  @ fs )  ⟧ ⟹
fields_in_path ( ([( ( ctx , cld ) )] @ ctxcld_list) ) (fs')"

(*defns fields_def *)
inductive fields :: "P ⇒ ty ⇒ fs_opt ⇒ bool"
where
(* defn fields *)

fields_noneI: "⟦find_path_ty (P) (ty) ( None )⟧ ⟹
fields (P) (ty) ( None )"

| fields_someI: "⟦find_path_ty (P) (ty) ( Some ( ctxclds ) ) ;
fields_in_path (ctxclds) (fs)⟧ ⟹
fields (P) (ty) ( Some ( fs ) )"

(*defns methods_in_path_def *)
inductive methods_in_path :: "clds ⇒ meths ⇒ bool"
where
(* defn methods_in_path *)

mip_emptyI: "methods_in_path ( [] ) ( [] )"

| mip_consI: "⟦class_methods (cld) ( ((List.map (%((meth_def_XXX::meth_def),(cl_XXX::cl),(meth_XXX::meth),(vds_XXX::vds),(meth_body_XXX::meth_body)).meth_def_XXX) meth_def_cl_meth_vds_meth_body_list)) ) ;
 list_all (λf. f)  ((List.map (%((meth_def_XXX::meth_def),(cl_XXX::cl),(meth_XXX::meth),(vds_XXX::vds),(meth_body_XXX::meth_body)). meth_def_XXX  =  (meth_def_def (meth_sig_def cl_XXX meth_XXX vds_XXX) meth_body_XXX) ) meth_def_cl_meth_vds_meth_body_list))  ;
methods_in_path ( (cld_list) ) (meths') ;
 meths  =   (  ((List.map (%((meth_def_XXX::meth_def),(cl_XXX::cl),(meth_XXX::meth),(vds_XXX::vds),(meth_body_XXX::meth_body)).meth_XXX) meth_def_cl_meth_vds_meth_body_list))  @ meths' )  ⟧ ⟹
methods_in_path ( ([(cld)] @ cld_list) ) (meths)"

(*defns methods_def *)
inductive methods :: "P ⇒ ty ⇒ meths ⇒ bool"
where
(* defn methods *)

methods_methodsI: "⟦find_path_ty (P) (ty) ( Some (  ((List.map (%((ctx_XXX::ctx),(cld_XXX::cld)). ( ctx_XXX , cld_XXX ) ) ctx_cld_list))  ) ) ;
methods_in_path ( ((List.map (%((ctx_XXX::ctx),(cld_XXX::cld)).cld_XXX) ctx_cld_list)) ) (meths)⟧ ⟹
methods (P) (ty) (meths)"

(*defns ftype_in_fds_def *)
inductive ftype_in_fds :: "P ⇒ ctx ⇒ fds ⇒ f ⇒ ty_opt_bot ⇒ bool"
where
(* defn ftype_in_fds *)

ftif_emptyI: "ftype_in_fds (P) (ctx) ( [] ) (f) ((ty_opt_bot_opt  None ))"

| ftif_cons_botI: "⟦find_type (P) (ctx) (cl) ( None )⟧ ⟹
ftype_in_fds (P) (ctx) ( ([((fd_def cl f))] @ fd_list) ) (f) (ty_opt_bot_bot)"

| ftif_cons_trueI: "⟦find_type (P) (ctx) (cl) ( (Some ( ty )) )⟧ ⟹
ftype_in_fds (P) (ctx) ( ([((fd_def cl f))] @ fd_list) ) (f) ((ty_opt_bot_opt  (Some ( ty )) ))"

| ftif_cons_falseI: "⟦ f  ≠  f'  ;
ftype_in_fds (P) (ctx) ( (fd_list) ) (f') (ty_opt_bot)⟧ ⟹
ftype_in_fds (P) (ctx) ( ([((fd_def cl f))] @ fd_list) ) (f') (ty_opt_bot)"

(*defns ftype_in_path_def *)
inductive ftype_in_path :: "P ⇒ ctxclds ⇒ f ⇒ ty_opt ⇒ bool"
where
(* defn ftype_in_path *)

ftip_emptyI: "ftype_in_path (P) ( [] ) (f) ( None )"

| ftip_cons_botI: "⟦class_fields (cld) (fds) ;
ftype_in_fds (P) (ctx) (fds) (f) (ty_opt_bot_bot)⟧ ⟹
ftype_in_path (P) ( ([( ( ctx , cld ) )] @ ctxcld_list) ) (f) ( None )"

| ftip_cons_trueI: "⟦class_fields (cld) (fds) ;
ftype_in_fds (P) (ctx) (fds) (f) ((ty_opt_bot_opt  (Some ( ty )) ))⟧ ⟹
ftype_in_path (P) ( ([( ( ctx , cld ) )] @ ctxcld_list) ) (f) ( (Some ( ty )) )"

| ftip_cons_falseI: "⟦class_fields (cld) (fds) ;
ftype_in_fds (P) (ctx) (fds) (f) ((ty_opt_bot_opt  None )) ;
ftype_in_path (P) ( (ctxcld_list) ) (f) (ty_opt)⟧ ⟹
ftype_in_path (P) ( ([( ( ctx , cld ) )] @ ctxcld_list) ) (f) (ty_opt)"

(*defns ftype_def *)
inductive ftype :: "P ⇒ ty ⇒ f ⇒ ty ⇒ bool"
where
(* defn ftype *)

ftypeI: "⟦find_path_ty (P) (ty) ( Some ( ctxclds ) ) ;
ftype_in_path (P) (ctxclds) (f) ( (Some ( ty' )) )⟧ ⟹
ftype (P) (ty) (f) (ty')"

(*defns find_meth_def_in_list_def *)
inductive find_meth_def_in_list :: "meth_defs ⇒ meth ⇒ meth_def_opt ⇒ bool"
where
(* defn find_meth_def_in_list *)

fmdil_emptyI: "find_meth_def_in_list ( [] ) (meth) ( None )"

| fmdil_cons_trueI: "⟦ meth_def  =  (meth_def_def (meth_sig_def cl meth vds) meth_body) ⟧ ⟹
find_meth_def_in_list ( ([(meth_def)] @ meth_def_list) ) (meth) ( Some ( meth_def ) )"

| fmdil_cons_falseI: "⟦ meth_def  =  (meth_def_def (meth_sig_def cl meth' vds) meth_body)  ;
 meth  ≠  meth'  ;
find_meth_def_in_list ( (meth_def_list) ) (meth) (meth_def_opt)⟧ ⟹
find_meth_def_in_list ( ([(meth_def)] @ meth_def_list) ) (meth) (meth_def_opt)"

(*defns find_meth_def_in_path_def *)
inductive find_meth_def_in_path :: "ctxclds ⇒ meth ⇒ ctxmeth_def_opt ⇒ bool"
where
(* defn find_meth_def_in_path *)

fmdip_emptyI: "find_meth_def_in_path ( [] ) (meth) ( (None::ctxmeth_def_opt) )"

| fmdip_cons_trueI: "⟦class_methods (cld) (meth_defs) ;
find_meth_def_in_list (meth_defs) (meth) ( Some ( meth_def ) )⟧ ⟹
find_meth_def_in_path ( ([( ( ctx , cld ) )] @ ctxcld_list) ) (meth) ( (Some ( ctx , meth_def )::ctxmeth_def_opt) )"

| fmdip_cons_falseI: "⟦class_methods (cld) (meth_defs) ;
find_meth_def_in_list (meth_defs) (meth) ( None ) ;
find_meth_def_in_path ( (ctxcld_list) ) (meth) (ctxmeth_def_opt)⟧ ⟹
find_meth_def_in_path ( ([( ( ctx , cld ) )] @ ctxcld_list) ) (meth) (ctxmeth_def_opt)"

(*defns find_meth_def_def *)
inductive find_meth_def :: "P ⇒ ty ⇒ meth ⇒ ctxmeth_def_opt ⇒ bool"
where
(* defn find_meth_def *)

fmd_nullI: "⟦find_path_ty (P) (ty) ( None )⟧ ⟹
find_meth_def (P) (ty) (meth) ( (None::ctxmeth_def_opt) )"

| fmd_optI: "⟦find_path_ty (P) (ty) ( Some ( ctxclds ) ) ;
find_meth_def_in_path (ctxclds) (meth) (ctxmeth_def_opt)⟧ ⟹
find_meth_def (P) (ty) (meth) (ctxmeth_def_opt)"

(*defns mtype_def *)
inductive mtype :: "P ⇒ ty ⇒ meth ⇒ mty ⇒ bool"
where
(* defn mtype *)

mtypeI: "⟦find_meth_def (P) (ty) (meth) ( (Some ( ctx , meth_def )::ctxmeth_def_opt) ) ;
 meth_def  =  (meth_def_def (meth_sig_def cl meth  ((List.map (%((cl_XXX::cl),(var_XXX::var),(ty_XXX::ty)).(vd_def cl_XXX var_XXX)) cl_var_ty_list)) ) meth_body)  ;
find_type (P) (ctx) (cl) ( (Some ( ty' )) ) ;
 list_all (λf. f)  ((List.map (%((cl_XXX::cl),(var_XXX::var),(ty_XXX::ty)).find_type (P) (ctx) (cl_XXX) ( (Some ( ty_XXX )) )) cl_var_ty_list))  ;
 mty  =  (mty_def  ((List.map (%((cl_XXX::cl),(var_XXX::var),(ty_XXX::ty)).ty_XXX) cl_var_ty_list))  ty') ⟧ ⟹
mtype (P) (ty) (meth) (mty)"

(*defns sty_one_def *)
inductive sty_one :: "P ⇒ ty ⇒ ty ⇒ bool"
where
(* defn one *)

sty_objI: "⟦find_path_ty (P) (ty) ( Some ( ctxclds ) )⟧ ⟹
sty_one (P) (ty) (ty_top)"

| sty_dclI: "⟦find_path_ty (P) (ty) ( Some (  ((List.map (%((ctx_XXX::ctx),(cld_XXX::cld),(dcl_XXX::dcl)). ( ctx_XXX , cld_XXX ) ) ctx_cld_dcl_list))  ) ) ;
 list_all (λf. f)  ((List.map (%((ctx_XXX::ctx),(cld_XXX::cld),(dcl_XXX::dcl)).class_name (cld_XXX) (dcl_XXX)) ctx_cld_dcl_list))  ;
 ( ctx' , dcl' ) ∈ set  ((List.map (%((ctx_XXX::ctx),(cld_XXX::cld),(dcl_XXX::dcl)).(ctx_XXX,dcl_XXX)) ctx_cld_dcl_list)) ⟧ ⟹
sty_one (P) (ty) ((ty_def ctx' dcl'))"

(*defns sty_many_def *)
inductive sty_many :: "P ⇒ tys ⇒ tys ⇒ bool"
where
(* defn many *)

sty_manyI: "⟦ tys  =   ((List.map (%((ty_XXX::ty),(ty_'::ty)).ty_XXX) ty_ty'_list))   ;
 tys'  =   ((List.map (%((ty_XXX::ty),(ty_'::ty)).ty_') ty_ty'_list))   ;
 list_all (λf. f)  ((List.map (%((ty_XXX::ty),(ty_'::ty)).sty_one (P) (ty_XXX) (ty_')) ty_ty'_list)) ⟧ ⟹
sty_many (P) (tys) (tys')"

(*defns sty_option_def *)
inductive sty_option :: "P ⇒ ty_opt ⇒ ty_opt ⇒ bool"
where
(* defn option *)

sty_optionI: "⟦ ty_opt  =   (Some ( ty ))   ;
 ty_opt'  =   (Some ( ty' ))   ;
sty_one (P) (ty) (ty')⟧ ⟹
sty_option (P) (ty_opt) (ty_opt')"

(*defns well_formedness *)
inductive wf_object :: "P ⇒ H ⇒ v_opt ⇒ ty_opt ⇒ bool"
 and wf_varstate :: "P ⇒ Γ ⇒ H ⇒ L ⇒ bool"
 and wf_heap :: "P ⇒ H ⇒ bool"
 and wf_config :: "Γ ⇒ config ⇒ bool"
 and wf_stmt :: "P ⇒ Γ ⇒ s ⇒ bool"
 and wf_meth :: "P ⇒ ty ⇒ meth_def ⇒ bool"
 and wf_class_common :: "P ⇒ ctx ⇒ dcl ⇒ cl ⇒ fds ⇒ meth_defs ⇒ bool"
 and wf_class :: "P ⇒ cld ⇒ bool"
 and wf_program :: "P ⇒ bool"
where
(* defn object *)

wf_nullI: "⟦ ty_opt  =   (Some ( ty ))  ⟧ ⟹
wf_object (P) (H) ( Some  v_null ) (ty_opt)"

| wf_objectI: "⟦sty_option (P) ( (case  H   oid  of
                     None ⇒ None
                   | Some tyfs ⇒ Some (fst tyfs)) ) (ty_opt)⟧ ⟹
wf_object (P) (H) ( Some  (v_oid oid) ) (ty_opt)"

| (* defn varstate *)

wf_varstateI: "⟦ finite (dom ( L ))  ;
 ∀  x  ∈ dom  Γ .  wf_object (P) (H) ( L   x ) ( Γ   x ) ⟧ ⟹
wf_varstate (P) (Γ) (H) (L)"

| (* defn heap *)

wf_heapI: "⟦ finite (dom ( H ))  ;
 ∀  oid  ∈ dom  H .   (   ∃  ty  .     (case  H   oid  of
                     None ⇒ None
                   | Some tyfs ⇒ Some (fst tyfs))   =   (Some ( ty ))    ∧   (∃  fs  .   fields (P) (ty) ( Some ( fs ) )  ∧     (∀  f  ∈ set  fs .   ∃  ty'  .   (   ftype (P) (ty) (f) (ty')  ∧   wf_object (P) (H) ( (case  H   oid  of
                     None ⇒ None
                   | Some tyfs ⇒ (snd tyfs)  f ) ) ( (Some ( ty' )) )    )   )     )     )  ⟧ ⟹
wf_heap (P) (H)"

| (* defn config *)

wf_all_exI: "⟦wf_program (P) ;
wf_heap (P) (H) ;
wf_varstate (P) (Γ) (H) (L)⟧ ⟹
wf_config (Γ) ((config_ex P L H Exception))"

| wf_allI: "⟦wf_program (P) ;
wf_heap (P) (H) ;
wf_varstate (P) (Γ) (H) (L) ;
 list_all (λf. f)  ((List.map (%(s_XXX::s).wf_stmt (P) (Γ) (s_XXX)) s_list)) ⟧ ⟹
wf_config (Γ) ((config_normal P L H (s_list)))"

| (* defn stmt *)

wf_blockI: "⟦ list_all (λf. f)  ((List.map (%(s_XXX::s).wf_stmt (P) (Γ) (s_XXX)) s_list)) ⟧ ⟹
wf_stmt (P) (Γ) ((s_block (s_list)))"

| wf_var_assignI: "⟦sty_option (P) ( Γ   x ) ( Γ   (x_var var) )⟧ ⟹
wf_stmt (P) (Γ) ((s_ass var x))"

| wf_field_readI: "⟦  Γ   x   =   (Some ( ty ))   ;
ftype (P) (ty) (f) (ty') ;
sty_option (P) ( (Some ( ty' )) ) ( Γ   (x_var var) )⟧ ⟹
wf_stmt (P) (Γ) ((s_read var x f))"

| wf_field_writeI: "⟦  Γ   x   =   (Some ( ty ))   ;
ftype (P) (ty) (f) (ty') ;
sty_option (P) ( Γ   y ) ( (Some ( ty' )) )⟧ ⟹
wf_stmt (P) (Γ) ((s_write x f y))"

| wf_ifI: "⟦ sty_option (P) ( Γ   x ) ( Γ   y )  ∨  sty_option (P) ( Γ   y ) ( Γ   x )  ;
wf_stmt (P) (Γ) (s1) ;
wf_stmt (P) (Γ) (s2)⟧ ⟹
wf_stmt (P) (Γ) ((s_if x y s1 s2))"

| wf_newI: "⟦find_type (P) (ctx) (cl) ( (Some ( ty )) ) ;
sty_option (P) ( (Some ( ty )) ) ( Γ   (x_var var) )⟧ ⟹
wf_stmt (P) (Γ) ((s_new var ctx cl))"

| wf_mcallI: "⟦ Y  =   ((List.map (%((y_XXX::x),(ty_XXX::ty)).y_XXX) y_ty_list))   ;
  Γ   x   =   (Some ( ty ))   ;
mtype (P) (ty) (meth) ((mty_def  ((List.map (%((y_XXX::x),(ty_XXX::ty)).ty_XXX) y_ty_list))  ty')) ;
 list_all (λf. f)  ((List.map (%((y_XXX::x),(ty_XXX::ty)).sty_option (P) ( Γ   y_XXX ) ( (Some ( ty_XXX )) )) y_ty_list))  ;
sty_option (P) ( (Some ( ty' )) ) ( Γ   (x_var var) )⟧ ⟹
wf_stmt (P) (Γ) ((s_call var x meth Y))"

| (* defn meth *)

wf_methodI: "⟦ distinct ( ((List.map (%((cl_XXX::cl),(var_XXX::var),(ty_XXX::ty)).var_XXX) cl_var_ty_list)) )  ;
 list_all (λf. f)  ((List.map (%((cl_XXX::cl),(var_XXX::var),(ty_XXX::ty)).find_type (P) (ctx) (cl_XXX) ( (Some ( ty_XXX )) )) cl_var_ty_list))  ;
 Γ  =   (  (map_of ( ((List.map (%((cl_XXX::cl),(var_XXX::var),(ty_XXX::ty)).((x_var var_XXX),ty_XXX)) cl_var_ty_list)) ))   ( x_this   ↦   (ty_def ctx dcl) ))   ;
 list_all (λf. f)  ((List.map (%(s_XXX::s).wf_stmt (P) (Γ) (s_XXX)) s_list))  ;
find_type (P) (ctx) (cl) ( (Some ( ty )) ) ;
sty_option (P) ( Γ   y ) ( (Some ( ty )) )⟧ ⟹
wf_meth (P) ((ty_def ctx dcl)) ((meth_def_def (meth_sig_def cl meth  ((List.map (%((cl_XXX::cl),(var_XXX::var),(ty_XXX::ty)).(vd_def cl_XXX var_XXX)) cl_var_ty_list)) ) (meth_body_def (s_list) y)))"

| (* defn class_common *)

wf_class_commonI: "⟦find_type (P) (ctx) (cl) ( (Some ( ty )) ) ;
 (ty_def ctx dcl)  ≠  ty  ;
 distinct ( ((List.map (%((cl_XXX::cl),(f_XXX::f),(ty_XXX::ty)).f_XXX) cl_f_ty_list)) )  ;
fields (P) (ty) ( Some ( fs ) ) ;
 (set   ((List.map (%((cl_XXX::cl),(f_XXX::f),(ty_XXX::ty)).f_XXX) cl_f_ty_list))  ) ∩ (set  fs ) = {}  ;
 list_all (λf. f)  ((List.map (%((cl_XXX::cl),(f_XXX::f),(ty_XXX::ty)).find_type (P) (ctx) (cl_XXX) ( (Some ( ty_XXX )) )) cl_f_ty_list))  ;
 list_all (λf. f)  ((List.map (%((meth_def_XXX::meth_def),(meth_XXX::meth)).wf_meth (P) ((ty_def ctx dcl)) (meth_def_XXX)) meth_def_meth_list))  ;
 list_all (λf. f)  ((List.map (%((meth_def_XXX::meth_def),(meth_XXX::meth)).method_name (meth_def_XXX) (meth_XXX)) meth_def_meth_list))  ;
 distinct ( ((List.map (%((meth_def_XXX::meth_def),(meth_XXX::meth)).meth_XXX) meth_def_meth_list)) )  ;
methods (P) (ty) ( ((List.map (%((meth_'::meth),(mty_XXX::mty),(mty_'::mty)).meth_') meth'_mty_mty'_list)) ) ;
 list_all (λf. f)  ((List.map (%((meth_'::meth),(mty_XXX::mty),(mty_'::mty)).mtype (P) ((ty_def ctx dcl)) (meth_') (mty_XXX)) meth'_mty_mty'_list))  ;
 list_all (λf. f)  ((List.map (%((meth_'::meth),(mty_XXX::mty),(mty_'::mty)).mtype (P) (ty) (meth_') (mty_')) meth'_mty_mty'_list))  ;
 list_all (λf. f)  ((List.map (%((meth_'::meth),(mty_XXX::mty),(mty_'::mty)).  meth_'  ∈ set   ((List.map (%((meth_def_XXX::meth_def),(meth_XXX::meth)).meth_XXX) meth_def_meth_list))    ⟶   mty_XXX  =  mty_'  ) meth'_mty_mty'_list)) ⟧ ⟹
wf_class_common (P) (ctx) (dcl) (cl) ( ((List.map (%((cl_XXX::cl),(f_XXX::f),(ty_XXX::ty)).(fd_def cl_XXX f_XXX)) cl_f_ty_list)) ) ( ((List.map (%((meth_def_XXX::meth_def),(meth_XXX::meth)).meth_def_XXX) meth_def_meth_list)) )"

| (* defn class *)

wf_classI: "⟦ (cld_def dcl cl fds meth_defs)  ∈ set  P  ;
wf_class_common (P) (ctx_def) (dcl) (cl) (fds) (meth_defs)⟧ ⟹
wf_class (P) ((cld_def dcl cl fds meth_defs))"

| (* defn program *)

wf_programI: "⟦ P  =    (cld_list)    ;
distinct_names (P) ;
 list_all (λf. f)  ((List.map (%(cld_XXX::cld).wf_class (P) (cld_XXX)) cld_list))  ;
acyclic_clds (P)⟧ ⟹
wf_program (P)"

(*defns var_trans *)
inductive tr_s :: "T ⇒ s ⇒ s ⇒ bool"
where
(* defn tr_s *)

tr_s_blockI: "⟦ list_all (λf. f)  ((List.map (%((s_XXX::s),(s_'::s)).tr_s (T) (s_XXX) (s_')) s_s'_list)) ⟧ ⟹
tr_s (T) ((s_block ((List.map (%((s_XXX::s),(s_'::s)).s_XXX) s_s'_list)))) ((s_block ((List.map (%((s_XXX::s),(s_'::s)).s_') s_s'_list))))"

| tr_s_var_assignI: "⟦ (case  T  (x_var  var ) of
                    None ⇒  var  | Some x' ⇒
                 (case x' of x_this ⇒  var
                           | x_var var' ⇒ var')) =  var'  ;
 (case  T   x  of None ⇒  x
                                    | Some x' ⇒ x') =  x' ⟧ ⟹
tr_s (T) ((s_ass var x)) ((s_ass var' x'))"

| tr_s_field_readI: "⟦ (case  T  (x_var  var ) of
                    None ⇒  var  | Some x' ⇒
                 (case x' of x_this ⇒  var
                           | x_var var' ⇒ var')) =  var'  ;
 (case  T   x  of None ⇒  x
                                    | Some x' ⇒ x') =  x' ⟧ ⟹
tr_s (T) ((s_read var x f)) ((s_read var' x' f))"

| tr_s_field_writeI: "⟦ (case  T   x  of None ⇒  x
                                    | Some x' ⇒ x') =  x'  ;
 (case  T   y  of None ⇒  y
                                    | Some x' ⇒ x') =  y' ⟧ ⟹
tr_s (T) ((s_write x f y)) ((s_write x' f y'))"

| tr_s_ifI: "⟦ (case  T   x  of None ⇒  x
                                    | Some x' ⇒ x') =  x'  ;
 (case  T   y  of None ⇒  y
                                    | Some x' ⇒ x') =  y'  ;
tr_s (T) (s1) (s1') ;
tr_s (T) (s2) (s2')⟧ ⟹
tr_s (T) ((s_if x y s1 s2)) ((s_if x' y' s1' s2'))"

| tr_s_newI: "⟦ (case  T  (x_var  var ) of
                    None ⇒  var  | Some x' ⇒
                 (case x' of x_this ⇒  var
                           | x_var var' ⇒ var')) =  var' ⟧ ⟹
tr_s (T) ((s_new var ctx cl)) ((s_new var' ctx cl))"

| tr_s_mcallI: "⟦ (case  T  (x_var  var ) of
                    None ⇒  var  | Some x' ⇒
                 (case x' of x_this ⇒  var
                           | x_var var' ⇒ var')) =  var'  ;
 (case  T   x  of None ⇒  x
                                    | Some x' ⇒ x') =  x'  ;
 list_all (λf. f)  ((List.map (%((y_XXX::x),(y_'::x)). (case  T   y_XXX  of None ⇒  y_XXX
                                    | Some x' ⇒ x') =  y_' ) y_y'_list)) ⟧ ⟹
tr_s (T) ((s_call var x meth  ((List.map (%((y_XXX::x),(y_'::x)).y_XXX) y_y'_list)) )) ((s_call var' x' meth  ((List.map (%((y_XXX::x),(y_'::x)).y_') y_y'_list)) ))"

(*defns reduction *)
inductive r_stmt :: "config ⇒ config ⇒ bool"
where
(* defn stmt *)

r_blockI: "r_stmt ((config_normal P L H ([((s_block (s_list)))] @ s'_list))) ((config_normal P L H (s_list @ s'_list)))"

| r_var_assignI: "⟦  L   x   = Some  v ⟧ ⟹
r_stmt ((config_normal P L H ([((s_ass var x))] @ s_list))) ((config_normal P  ( L  ( (x_var var)   ↦   v ))  H (s_list)))"

| r_field_read_npeI: "⟦  L   x   = Some  v_null ⟧ ⟹
r_stmt ((config_normal P L H ([((s_read var x f))] @ s_list))) ((config_ex P L H ex_npe))"

| r_field_readI: "⟦  L   x   = Some  (v_oid oid)  ;
  (case  H   oid  of
                     None ⇒ None
                   | Some tyfs ⇒ (snd tyfs)  f )   = Some  v ⟧ ⟹
r_stmt ((config_normal P L H ([((s_read var x f))] @ s_list))) ((config_normal P  ( L  ( (x_var var)   ↦   v ))  H (s_list)))"

| r_field_write_npeI: "⟦  L   x   = Some  v_null ⟧ ⟹
r_stmt ((config_normal P L H ([((s_write x f y))] @ s_list))) ((config_ex P L H ex_npe))"

| r_field_writeI: "⟦  L   x   = Some  (v_oid oid)  ;
  L   y   = Some  v ⟧ ⟹
r_stmt ((config_normal P L H ([((s_write x f y))] @ s_list))) ((config_normal P L  (case  H   oid  of
                None ⇒ arbitrary
              | Some tyfs ⇒
                   (( H  ( oid   ↦
                       (fst tyfs, (snd tyfs) ( f   ↦   v ))))::H))  (s_list)))"

| r_if_trueI: "⟦  L   x   = Some  v  ;
  L   y   = Some  w  ;
 v  =  w ⟧ ⟹
r_stmt ((config_normal P L H ([((s_if x y s1 s2))] @ s'_list))) ((config_normal P L H ([(s1)] @ s'_list)))"

| r_if_falseI: "⟦  L   x   = Some  v  ;
  L   y   = Some  w  ;
 v  ≠  w ⟧ ⟹
r_stmt ((config_normal P L H ([((s_if x y s1 s2))] @ s'_list))) ((config_normal P L H ([(s2)] @ s'_list)))"

| r_newI: "⟦find_type (P) (ctx) (cl) ( (Some ( ty )) ) ;
fields (P) (ty) ( Some (  (f_list)  ) ) ;
 oid  ∉ dom  H  ;
 H'  =   (( H  ( oid   ↦  ( ty ,
                          map_of  ((List.map (%(f_XXX::f).(f_XXX,v_null)) f_list))  )))::H)  ⟧ ⟹
r_stmt ((config_normal P L H ([((s_new var ctx cl))] @ s_list))) ((config_normal P  ( L  ( (x_var var)   ↦   (v_oid oid) ))  H' (s_list)))"

| r_mcall_npeI: "⟦  L   x   = Some  v_null ⟧ ⟹
r_stmt ((config_normal P L H ([((s_call var x meth  (y_list) ))] @ s_list))) ((config_ex P L H ex_npe))"

| r_mcallI: "⟦  L   x   = Some  (v_oid oid)  ;
  (case  H   oid  of
                     None ⇒ None
                   | Some tyfs ⇒ Some (fst tyfs))   =   (Some ( ty ))   ;
find_meth_def (P) (ty) (meth) ( (Some ( ctx , (meth_def_def (meth_sig_def cl meth  ((List.map (%((y_XXX::x),(cl_XXX::cl),(var_XXX::var),(var_'::var),(v_XXX::v)).(vd_def cl_XXX var_XXX)) y_cl_var_var'_v_list)) ) (meth_body_def ((List.map (%((s_''::s),(s_'::s)).s_') s''_s'_list)) y)) )::ctxmeth_def_opt) ) ;
 (set  ((List.map (%((y_XXX::x),(cl_XXX::cl),(var_XXX::var),(var_'::var),(v_XXX::v)).(x_var var_')) y_cl_var_var'_v_list)) ) Int (dom  L ) = {}  ;
 distinct ( ((List.map (%((y_XXX::x),(cl_XXX::cl),(var_XXX::var),(var_'::var),(v_XXX::v)).var_') y_cl_var_var'_v_list)) )  ;
 x'  ∉ dom  L  ;
 x'  ∉ set  ((List.map (%((y_XXX::x),(cl_XXX::cl),(var_XXX::var),(var_'::var),(v_XXX::v)).(x_var var_')) y_cl_var_var'_v_list))  ;
 list_all (λf. f)  ((List.map (%((y_XXX::x),(cl_XXX::cl),(var_XXX::var),(var_'::var),(v_XXX::v)).  L   y_XXX   = Some  v_XXX ) y_cl_var_var'_v_list))  ;
 L'  =   (  ( L  ++ (map_of ( ((List.map (%((y_XXX::x),(cl_XXX::cl),(var_XXX::var),(var_'::var),(v_XXX::v)).((x_var var_'),v_XXX)) y_cl_var_var'_v_list)) )))   ( x'   ↦   (v_oid oid) ))   ;
 T  =   (  (map_of ( ((List.map (%((y_XXX::x),(cl_XXX::cl),(var_XXX::var),(var_'::var),(v_XXX::v)).((x_var var_XXX),(x_var var_'))) y_cl_var_var'_v_list)) ))   ( x_this   ↦   x' ))   ;
 list_all (λf. f)  ((List.map (%((s_''::s),(s_'::s)).tr_s (T) (s_') (s_'')) s''_s'_list))  ;
 (case  T   y  of None ⇒  y
                                    | Some x' ⇒ x') =  y' ⟧ ⟹
r_stmt ((config_normal P L H ([((s_call var x meth  ((List.map (%((y_XXX::x),(cl_XXX::cl),(var_XXX::var),(var_'::var),(v_XXX::v)).y_XXX) y_cl_var_var'_v_list)) ))] @ s_list))) ((config_normal P L' H ((List.map (%((s_''::s),(s_'::s)).s_'') s''_s'_list) @ [((s_ass var y'))] @ s_list)))"



end