
wenzelm@12857: (*  Title:      HOL/Bali/Example.thy
schirmer@12854:     ID:         $Id$
schirmer@12854:     Author:     David von Oheimb
schirmer@12854: *)
schirmer@12854: header {* Example Bali program *}
schirmer@12854: 
haftmann@16417: theory Example imports Eval WellForm begin
schirmer@12854: 
schirmer@12854: text {*
schirmer@12854: The following example Bali program includes:
schirmer@12854: \begin{itemize}
schirmer@12854: \item class and interface declarations with inheritance, hiding of fields,
schirmer@12854:     overriding of methods (with refined result type), array type,
schirmer@12854: \item method call (with dynamic binding), parameter access, return expressions,
schirmer@12854: \item expression statements, sequential composition, literal values, 
schirmer@12854:     local assignment, local access, field assignment, type cast,
schirmer@12854: \item exception generation and propagation, try and catch statement, throw 
schirmer@12854:       statement
schirmer@12854: \item instance creation and (default) static initialization
schirmer@12854: \end{itemize}
schirmer@12854: \begin{verbatim}
schirmer@12854: package java_lang
schirmer@12854: 
schirmer@12854: public interface HasFoo {
schirmer@12854:   public Base foo(Base z);
schirmer@12854: }
schirmer@12854: 
schirmer@12854: public class Base implements HasFoo {
schirmer@12854:   static boolean arr[] = new boolean[2];
schirmer@12854:   public HasFoo vee;
schirmer@12854:   public Base foo(Base z) {
schirmer@12854:     return z;
schirmer@12854:   }
schirmer@12854: }
schirmer@12854: 
schirmer@12854: public class Ext extends Base {
schirmer@12854:   public int vee;
schirmer@12854:   public Ext foo(Base z) {
schirmer@12854:     ((Ext)z).vee = 1;
schirmer@12854:     return null;
schirmer@12854:   }
schirmer@12854: }
schirmer@12854: 
schirmer@12925: public class Main {
schirmer@12854:   public static void main(String args[]) throws Throwable {
schirmer@12854:     Base e = new Ext();
schirmer@12854:     try {e.foo(null); }
schirmer@12854:     catch(NullPointerException z) { 
schirmer@12854:       while(Ext.arr[2]) ;
schirmer@12854:     }
schirmer@12854:   }
schirmer@12854: }
schirmer@12854: \end{verbatim}
schirmer@12854: *}
schirmer@12854: declare widen.null [intro]
schirmer@12854: 
schirmer@12854: lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
schirmer@12854: apply (unfold wf_fdecl_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: declare wf_fdecl_def2 [iff]
schirmer@12854: 
schirmer@12854: 
schirmer@12854: section "type and expression names"
schirmer@12854: 
schirmer@12854: (** unfortunately cannot simply instantiate tnam **)
wenzelm@22708: datatype tnam'  = HasFoo' | Base' | Ext' | Main'
wenzelm@22708: datatype vnam'  = arr' | vee' | z' | e'
wenzelm@22708: datatype label' = lab1'
schirmer@12854: 
schirmer@12854: consts
schirmer@12854: 
wenzelm@22708:   tnam' :: "tnam'  \<Rightarrow> tnam"
wenzelm@22708:   vnam' :: "vnam'  \<Rightarrow> vname"
wenzelm@22708:   label':: "label' \<Rightarrow> label"
wenzelm@22708: axioms  (** tnam', vnam' and label are intended to be isomorphic 
schirmer@12854:             to tnam, vname and label **)
schirmer@12854: 
wenzelm@22708:   inj_tnam'  [simp]: "(tnam'  x = tnam'  y) = (x = y)"
wenzelm@22708:   inj_vnam'  [simp]: "(vnam'  x = vnam'  y) = (x = y)"
wenzelm@22708:   inj_label' [simp]: "(label' x = label' y) = (x = y)"
schirmer@12854:   
schirmer@12854:   
wenzelm@22708:   surj_tnam':  "\<exists>m. n = tnam'  m"
wenzelm@22708:   surj_vnam':  "\<exists>m. n = vnam'  m"
wenzelm@22708:   surj_label':" \<exists>m. n = label' m"
schirmer@12854: 
wenzelm@20769: abbreviation
wenzelm@21404:   HasFoo :: qtname where
wenzelm@22708:   "HasFoo == \<lparr>pid=java_lang,tid=TName (tnam' HasFoo')\<rparr>"
wenzelm@20769: 
wenzelm@21404: abbreviation
wenzelm@21404:   Base :: qtname where
wenzelm@22708:   "Base == \<lparr>pid=java_lang,tid=TName (tnam' Base')\<rparr>"
wenzelm@20769: 
wenzelm@21404: abbreviation
wenzelm@21404:   Ext :: qtname where
wenzelm@22708:   "Ext == \<lparr>pid=java_lang,tid=TName (tnam' Ext')\<rparr>"
wenzelm@20769: 
wenzelm@21404: abbreviation
wenzelm@21404:   Main :: qtname where
wenzelm@22708:   "Main == \<lparr>pid=java_lang,tid=TName (tnam' Main')\<rparr>"
wenzelm@20769: 
wenzelm@21404: abbreviation
wenzelm@21404:   arr :: vname where
wenzelm@22708:   "arr == (vnam' arr')"
wenzelm@20769: 
wenzelm@21404: abbreviation
wenzelm@21404:   vee :: vname where
wenzelm@22708:   "vee == (vnam' vee')"
wenzelm@20769: 
wenzelm@21404: abbreviation
wenzelm@21404:   z :: vname where
wenzelm@22708:   "z == (vnam' z')"
wenzelm@20769: 
wenzelm@21404: abbreviation
wenzelm@21404:   e :: vname where
wenzelm@22708:   "e == (vnam' e')"
wenzelm@20769: 
wenzelm@21404: abbreviation
wenzelm@21404:   lab1:: label where
wenzelm@22708:   "lab1 == label' lab1'"
schirmer@12854: 
schirmer@12854: 
schirmer@12854: lemma neq_Base_Object [simp]: "Base\<noteq>Object"
schirmer@12854: by (simp add: Object_def)
schirmer@12854: 
schirmer@12854: lemma neq_Ext_Object [simp]: "Ext\<noteq>Object"
schirmer@12854: by (simp add: Object_def)
schirmer@12854: 
schirmer@12925: lemma neq_Main_Object [simp]: "Main\<noteq>Object"
schirmer@12925: by (simp add: Object_def)
schirmer@12925: 
schirmer@12854: lemma neq_Base_SXcpt [simp]: "Base\<noteq>SXcpt xn"
schirmer@12854: by (simp add: SXcpt_def)
schirmer@12854: 
schirmer@12854: lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn"
schirmer@12854: by (simp add: SXcpt_def)
schirmer@12854: 
wenzelm@13524: lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
schirmer@12925: by (simp add: SXcpt_def)
schirmer@12925: 
schirmer@12854: section "classes and interfaces"
schirmer@12854: 
schirmer@12854: defs
schirmer@12854: 
schirmer@12854:   Object_mdecls_def: "Object_mdecls \<equiv> []"
schirmer@12854:   SXcpt_mdecls_def:  "SXcpt_mdecls  \<equiv> []"
schirmer@12854: 
schirmer@12854: consts
schirmer@12854:   
schirmer@12854:   foo    :: mname
schirmer@12854: 
schirmer@12854: constdefs
schirmer@12854:   
schirmer@12854:   foo_sig   :: sig
schirmer@12854:  "foo_sig   \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>"
schirmer@12854:   
schirmer@12854:   foo_mhead :: mhead
schirmer@12854:  "foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
schirmer@12854: 
schirmer@12854: constdefs
schirmer@12854:   
schirmer@12854:   Base_foo :: mdecl
schirmer@12854:  "Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
schirmer@12854:                         mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)"
schirmer@12925: 
schirmer@12925: constdefs
schirmer@12854:   Ext_foo  :: mdecl
schirmer@12854:  "Ext_foo  \<equiv> (foo_sig, 
schirmer@12854:               \<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
schirmer@12854: 	       mbody=\<lparr>lcls=[]
schirmer@12925:                      ,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := 
schirmer@13688:        	                                                     Lit (Intg 1)) ;;
schirmer@13688:                                 Return (Lit Null)\<rparr>
schirmer@12854: 	      \<rparr>)"
schirmer@12854: 
schirmer@12854: constdefs
schirmer@12854:   
schirmer@12925: arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var"
schirmer@12925: "arr_viewed_from accC C \<equiv> {accC,Base,True}StatRef (ClassT C)..arr"
schirmer@12854: 
haftmann@18551: BaseCl :: "class"
schirmer@12854: "BaseCl \<equiv> \<lparr>access=Public,
schirmer@12854:            cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
schirmer@12854: 	            (vee, \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)],
schirmer@12854:            methods=[Base_foo],
schirmer@12925:            init=Expr(arr_viewed_from Base Base 
schirmer@12925:                      :=New (PrimT Boolean)[Lit (Intg 2)]),
schirmer@12854:            super=Object,
schirmer@12854:            superIfs=[HasFoo]\<rparr>"
schirmer@12854:   
haftmann@18551: ExtCl  :: "class"
schirmer@12854: "ExtCl  \<equiv> \<lparr>access=Public,
schirmer@12854:            cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], 
schirmer@12854:            methods=[Ext_foo],
schirmer@12854:            init=Skip,
schirmer@12854:            super=Base,
schirmer@12854:            superIfs=[]\<rparr>"
schirmer@12854: 
haftmann@18551: MainCl :: "class"
schirmer@12925: "MainCl \<equiv> \<lparr>access=Public,
schirmer@12925:            cfields=[], 
schirmer@12925:            methods=[], 
schirmer@12925:            init=Skip,
schirmer@12925:            super=Object,
schirmer@12925:            superIfs=[]\<rparr>"
schirmer@12925: (* The "main" method is modeled seperately (see tprg) *)
schirmer@12925: 
schirmer@12854: constdefs
schirmer@12854:   
schirmer@12854:   HasFooInt :: iface
schirmer@12854:  "HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
schirmer@12854: 
schirmer@12854:   Ifaces ::"idecl list"
schirmer@12854:  "Ifaces \<equiv> [(HasFoo,HasFooInt)]"
schirmer@12854: 
schirmer@12854:  "Classes" ::"cdecl list"
schirmer@12925:  "Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
schirmer@12854: 
schirmer@12854: lemmas table_classes_defs = 
schirmer@12854:      Classes_def standard_classes_def ObjectC_def SXcptC_def
schirmer@12854: 
schirmer@12854: lemma table_ifaces [simp]: "table_of Ifaces = empty(HasFoo\<mapsto>HasFooInt)"
schirmer@12854: apply (unfold Ifaces_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_classes_Object [simp]: 
schirmer@12854:  "table_of Classes Object = Some \<lparr>access=Public,cfields=[]
schirmer@12854:                                  ,methods=Object_mdecls
haftmann@28524:                                  ,init=Skip,super=undefined,superIfs=[]\<rparr>"
schirmer@12854: apply (unfold table_classes_defs)
schirmer@12854: apply (simp (no_asm) add:Object_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_classes_SXcpt [simp]: 
schirmer@12854:   "table_of Classes (SXcpt xn) 
schirmer@12854:     = Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
schirmer@12854:             init=Skip,
schirmer@12854:             super=if xn = Throwable then Object else SXcpt Throwable,
schirmer@12854:             superIfs=[]\<rparr>"
schirmer@12854: apply (unfold table_classes_defs)
schirmer@12854: apply (induct_tac xn)
schirmer@12854: apply (simp add: Object_def SXcpt_def)+
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_classes_HasFoo [simp]: "table_of Classes HasFoo = None"
schirmer@12854: apply (unfold table_classes_defs)
schirmer@12854: apply (simp (no_asm) add: Object_def SXcpt_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_classes_Base [simp]: "table_of Classes Base = Some BaseCl"
schirmer@12854: apply (unfold table_classes_defs )
schirmer@12854: apply (simp (no_asm) add: Object_def SXcpt_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_classes_Ext [simp]: "table_of Classes Ext = Some ExtCl"
schirmer@12854: apply (unfold table_classes_defs )
schirmer@12854: apply (simp (no_asm) add: Object_def SXcpt_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12925: lemma table_classes_Main [simp]: "table_of Classes Main = Some MainCl"
schirmer@12925: apply (unfold table_classes_defs )
schirmer@12925: apply (simp (no_asm) add: Object_def SXcpt_def)
schirmer@12925: done
schirmer@12854: 
schirmer@12854: section "program"
schirmer@12854: 
wenzelm@20769: abbreviation
wenzelm@21404:   tprg :: prog where
wenzelm@20769:   "tprg == \<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
schirmer@12854: 
schirmer@12854: constdefs
schirmer@12854:   test    :: "(ty)list \<Rightarrow> stmt"
schirmer@12854:  "test pTs \<equiv> e:==NewC Ext;; 
schirmer@12925:            \<spacespace> Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
schirmer@12854:            \<spacespace> Catch((SXcpt NullPointer) z)
schirmer@12925:            (lab1\<bullet> While(Acc 
schirmer@12925:                         (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip)"
schirmer@12854: 
schirmer@12854: 
schirmer@12854: section "well-structuredness"
schirmer@12854: 
schirmer@12854: lemma not_Object_subcls_any [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
schirmer@12854: apply (auto dest!: tranclD subcls1D)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma not_Throwable_subcls_SXcpt [elim!]: 
schirmer@12854:   "(SXcpt Throwable, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
schirmer@12854: apply (auto dest!: tranclD subcls1D) 
schirmer@12854: apply (simp add: Object_def SXcpt_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma not_SXcpt_n_subcls_SXcpt_n [elim!]: 
schirmer@12854:   "(SXcpt xn, SXcpt xn)  \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
schirmer@12854: apply (auto dest!: tranclD subcls1D)
schirmer@12854: apply (drule rtranclD)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+  \<Longrightarrow> R"
schirmer@12854: apply (auto dest!: tranclD subcls1D simp add: BaseCl_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma not_TName_n_subcls_TName_n [rule_format (no_asm), elim!]: 
schirmer@12854:   "(\<lparr>pid=java_lang,tid=TName tn\<rparr>, \<lparr>pid=java_lang,tid=TName tn\<rparr>) 
schirmer@12854:    \<in> (subcls1 tprg)^+ \<longrightarrow> R"
wenzelm@22708: apply (rule_tac n1 = "tn" in surj_tnam' [THEN exE])
schirmer@12854: apply (erule ssubst)
wenzelm@22708: apply (rule tnam'.induct)
schirmer@12854: apply  safe
schirmer@12925: apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def MainCl_def)
schirmer@12854: apply (drule rtranclD)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
schirmer@12854: lemma ws_idecl_HasFoo: "ws_idecl tprg HasFoo []"
schirmer@12854: apply (unfold ws_idecl_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma ws_cdecl_Object: "ws_cdecl tprg Object any"
schirmer@12854: apply (unfold ws_cdecl_def)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma ws_cdecl_Throwable: "ws_cdecl tprg (SXcpt Throwable) Object"
schirmer@12854: apply (unfold ws_cdecl_def)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma ws_cdecl_SXcpt: "ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)"
schirmer@12854: apply (unfold ws_cdecl_def)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma ws_cdecl_Base: "ws_cdecl tprg Base Object"
schirmer@12854: apply (unfold ws_cdecl_def)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma ws_cdecl_Ext: "ws_cdecl tprg Ext Base"
schirmer@12854: apply (unfold ws_cdecl_def)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12925: lemma ws_cdecl_Main: "ws_cdecl tprg Main Object"
schirmer@12925: apply (unfold ws_cdecl_def)
schirmer@12925: apply auto
schirmer@12925: done
schirmer@12925: 
schirmer@12854: lemmas ws_cdecls = ws_cdecl_SXcpt ws_cdecl_Object ws_cdecl_Throwable
schirmer@12925:                    ws_cdecl_Base ws_cdecl_Ext ws_cdecl_Main
schirmer@12854: 
schirmer@12854: declare not_Object_subcls_any [rule del]
schirmer@12854:           not_Throwable_subcls_SXcpt [rule del] 
schirmer@12854:           not_SXcpt_n_subcls_SXcpt_n [rule del] 
schirmer@12854:           not_Base_subcls_Ext [rule del] not_TName_n_subcls_TName_n [rule del]
schirmer@12854: 
schirmer@12854: lemma ws_idecl_all: 
schirmer@12854:  "G=tprg \<Longrightarrow> (\<forall>(I,i)\<in>set Ifaces. ws_idecl G I (isuperIfs i))"
schirmer@12854: apply (simp (no_asm) add: Ifaces_def HasFooInt_def)
schirmer@12854: apply (auto intro!: ws_idecl_HasFoo)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma ws_cdecl_all: "G=tprg \<Longrightarrow> (\<forall>(C,c)\<in>set Classes. ws_cdecl G C (super c))"
schirmer@12925: apply (simp (no_asm) add: Classes_def BaseCl_def ExtCl_def MainCl_def)
schirmer@12854: apply (auto intro!: ws_cdecls simp add: standard_classes_def ObjectC_def 
schirmer@12854:         SXcptC_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma ws_tprg: "ws_prog tprg"
schirmer@12854: apply (unfold ws_prog_def)
schirmer@12854: apply (auto intro!: ws_idecl_all ws_cdecl_all)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
schirmer@12854: section "misc program properties (independent of well-structuredness)"
schirmer@12854: 
schirmer@12854: lemma single_iface [simp]: "is_iface tprg I = (I = HasFoo)"
schirmer@12854: apply (unfold Ifaces_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma empty_subint1 [simp]: "subint1 tprg = {}"
schirmer@12854: apply (unfold subint1_def Ifaces_def HasFooInt_def)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma unique_ifaces: "unique Ifaces"
schirmer@12854: apply (unfold Ifaces_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma unique_classes: "unique Classes"
schirmer@12854: apply (unfold table_classes_defs )
schirmer@12854: apply (simp )
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma SXcpt_subcls_Throwable [simp]: "tprg\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable"
schirmer@12854: apply (rule SXcpt_subcls_Throwable_lemma)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma Ext_subclseq_Base [simp]: "tprg\<turnstile>Ext \<preceq>\<^sub>C Base"
schirmer@12854: apply (rule subcls_direct1)
schirmer@12854: apply  (simp (no_asm) add: ExtCl_def)
schirmer@12854: apply  (simp add: Object_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext \<prec>\<^sub>C Base"
schirmer@12854: apply (rule subcls_direct2)
schirmer@12854: apply  (simp (no_asm) add: ExtCl_def)
schirmer@12854: apply  (simp add: Object_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
schirmer@12854: 
schirmer@12854: section "fields and method lookup"
schirmer@12854: 
schirmer@12854: lemma fields_tprg_Object [simp]: "DeclConcepts.fields tprg Object = []"
schirmer@12854: by (rule ws_tprg [THEN fields_emptyI], force+)
schirmer@12854: 
schirmer@12854: lemma fields_tprg_Throwable [simp]: 
schirmer@12854:   "DeclConcepts.fields tprg (SXcpt Throwable) = []"
schirmer@12854: by (rule ws_tprg [THEN fields_emptyI], force+)
schirmer@12854: 
schirmer@12854: lemma fields_tprg_SXcpt [simp]: "DeclConcepts.fields tprg (SXcpt xn) = []"
schirmer@12854: apply (case_tac "xn = Throwable")
schirmer@12854: apply  (simp (no_asm_simp))
schirmer@12854: by (rule ws_tprg [THEN fields_emptyI], force+)
schirmer@12854: 
wenzelm@22708: lemmas fields_rec' = fields_rec [OF _ ws_tprg]
schirmer@12854: 
schirmer@12854: lemma fields_Base [simp]: 
schirmer@12854: "DeclConcepts.fields tprg Base 
schirmer@12854:   = [((arr,Base), \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
schirmer@12854:      ((vee,Base), \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)]"
wenzelm@22708: apply (subst fields_rec')
schirmer@12854: apply   (auto simp add: BaseCl_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma fields_Ext [simp]: 
schirmer@12854:  "DeclConcepts.fields tprg Ext  
schirmer@12854:   = [((vee,Ext), \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)] 
schirmer@12854:     @ DeclConcepts.fields tprg Base"
schirmer@12854: apply (rule trans)
wenzelm@22708: apply (rule fields_rec')
schirmer@12854: apply   (auto simp add: ExtCl_def Object_def)
schirmer@12854: done
schirmer@12854: 
wenzelm@22708: lemmas imethds_rec' = imethds_rec [OF _ ws_tprg]
wenzelm@22708: lemmas methd_rec'  = methd_rec  [OF _ ws_tprg]
schirmer@12854: 
schirmer@12854: lemma imethds_HasFoo [simp]: 
nipkow@30235:   "imethds tprg HasFoo = Option.set \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
schirmer@12854: apply (rule trans)
wenzelm@22708: apply (rule imethds_rec')
schirmer@12854: apply  (auto simp add: HasFooInt_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma methd_tprg_Object [simp]: "methd tprg Object = empty"
wenzelm@22708: apply (subst methd_rec')
schirmer@12854: apply (auto simp add: Object_mdecls_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma methd_Base [simp]: 
schirmer@12854:   "methd tprg Base = table_of [(\<lambda>(s,m). (s, Base, m)) Base_foo]"
schirmer@12854: apply (rule trans)
wenzelm@22708: apply (rule methd_rec')
schirmer@12854: apply   (auto simp add: BaseCl_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma memberid_Base_foo_simp [simp]:
schirmer@12854:  "memberid (mdecl Base_foo) = mid foo_sig"
schirmer@12854: by (simp add: Base_foo_def)
schirmer@12854: 
schirmer@12854: lemma memberid_Ext_foo_simp [simp]:
schirmer@12854:  "memberid (mdecl Ext_foo) = mid foo_sig"
schirmer@12854: by (simp add: Ext_foo_def)
schirmer@12854: 
schirmer@12854: lemma Base_declares_foo:
schirmer@12854:   "tprg\<turnstile>mdecl Base_foo declared_in Base"
schirmer@12854: by (auto simp add: declared_in_def cdeclaredmethd_def BaseCl_def Base_foo_def)
schirmer@12854: 
schirmer@12854: lemma foo_sig_not_undeclared_in_Base:
schirmer@12854:   "\<not> tprg\<turnstile>mid foo_sig undeclared_in Base"
schirmer@12854: proof -
schirmer@12854:   from Base_declares_foo
schirmer@12854:   show ?thesis
schirmer@12854:     by (auto dest!: declared_not_undeclared )
schirmer@12854: qed
schirmer@12854: 
schirmer@12854: lemma Ext_declares_foo:
schirmer@12854:   "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
schirmer@12854: by (auto simp add: declared_in_def cdeclaredmethd_def ExtCl_def Ext_foo_def)
schirmer@12854: 
schirmer@12854: lemma foo_sig_not_undeclared_in_Ext:
schirmer@12854:   "\<not> tprg\<turnstile>mid foo_sig undeclared_in Ext"
schirmer@12854: proof -
schirmer@12854:   from Ext_declares_foo
schirmer@12854:   show ?thesis
schirmer@12854:     by (auto dest!: declared_not_undeclared )
schirmer@12854: qed
schirmer@12854: 
schirmer@12854: lemma Base_foo_not_inherited_in_Ext:
schirmer@12854:  "\<not> tprg \<turnstile> Ext inherits (Base,mdecl Base_foo)"
schirmer@12854: by (auto simp add: inherits_def foo_sig_not_undeclared_in_Ext)
schirmer@12854: 
schirmer@12854: lemma Ext_method_inheritance:
schirmer@12854:  "filter_tab (\<lambda>sig m. tprg \<turnstile> Ext inherits method sig m)
schirmer@12854:      (empty(fst ((\<lambda>(s, m). (s, Base, m)) Base_foo)\<mapsto>
schirmer@12854:       snd ((\<lambda>(s, m). (s, Base, m)) Base_foo)))
schirmer@12854:   = empty"
schirmer@12854: proof -
schirmer@12854:   from Base_foo_not_inherited_in_Ext
schirmer@12854:   show ?thesis
schirmer@12854:     by (auto intro: filter_tab_all_False simp add: Base_foo_def)
schirmer@12854: qed
schirmer@12854: 
schirmer@12854: 
schirmer@12854: lemma methd_Ext [simp]: "methd tprg Ext =   
schirmer@12854:   table_of [(\<lambda>(s,m). (s, Ext, m)) Ext_foo]"
schirmer@12854: apply (rule trans)
wenzelm@22708: apply (rule methd_rec')
schirmer@12854: apply   (auto simp add: ExtCl_def Object_def Ext_method_inheritance)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: section "accessibility"
schirmer@12854: 
schirmer@12854: lemma classesDefined: 
schirmer@12854:  "\<lbrakk>class tprg C = Some c; C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class tprg (super c) = Some sc"
schirmer@12854: apply (auto simp add: Classes_def standard_classes_def 
schirmer@12925:                       BaseCl_def ExtCl_def MainCl_def
schirmer@12854:                       SXcptC_def ObjectC_def) 
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma superclassesBase [simp]: "superclasses tprg Base={Object}"
schirmer@12854: proof -
schirmer@12854:   have ws: "ws_prog tprg" by (rule ws_tprg)
schirmer@12854:   then show ?thesis
schirmer@12854:     by (auto simp add: superclasses_rec  BaseCl_def)
schirmer@12854: qed
schirmer@12854: 
schirmer@12854: lemma superclassesExt [simp]: "superclasses tprg Ext={Base,Object}"
schirmer@12854: proof -
schirmer@12854:   have ws: "ws_prog tprg" by (rule ws_tprg)
schirmer@12854:   then show ?thesis
schirmer@12854:     by (auto simp add: superclasses_rec  ExtCl_def BaseCl_def)
schirmer@12854: qed
schirmer@12854: 
schirmer@12925: lemma superclassesMain [simp]: "superclasses tprg Main={Object}"
schirmer@12925: proof -
schirmer@12925:   have ws: "ws_prog tprg" by (rule ws_tprg)
schirmer@12925:   then show ?thesis
schirmer@12925:     by (auto simp add: superclasses_rec  MainCl_def)
schirmer@12925: qed
schirmer@12925: 
schirmer@12854: lemma HasFoo_accessible[simp]:"tprg\<turnstile>(Iface HasFoo) accessible_in P" 
schirmer@12854: by (simp add: accessible_in_RefT_simp is_public_def HasFooInt_def)
schirmer@12854: 
schirmer@12854: lemma HasFoo_is_acc_iface[simp]: "is_acc_iface tprg P HasFoo"
schirmer@12854: by (simp add: is_acc_iface_def)
schirmer@12854: 
schirmer@12854: lemma HasFoo_is_acc_type[simp]: "is_acc_type tprg P (Iface HasFoo)"
schirmer@12854: by (simp add: is_acc_type_def)
schirmer@12854: 
schirmer@12854: lemma Base_accessible[simp]:"tprg\<turnstile>(Class Base) accessible_in P" 
schirmer@12854: by (simp add: accessible_in_RefT_simp is_public_def BaseCl_def)
schirmer@12854: 
schirmer@12854: lemma Base_is_acc_class[simp]: "is_acc_class tprg P Base"
schirmer@12854: by (simp add: is_acc_class_def)
schirmer@12854: 
schirmer@12854: lemma Base_is_acc_type[simp]: "is_acc_type tprg P (Class Base)"
schirmer@12854: by (simp add: is_acc_type_def)
schirmer@12854: 
schirmer@12854: lemma Ext_accessible[simp]:"tprg\<turnstile>(Class Ext) accessible_in P" 
schirmer@12854: by (simp add: accessible_in_RefT_simp is_public_def ExtCl_def)
schirmer@12854: 
schirmer@12854: lemma Ext_is_acc_class[simp]: "is_acc_class tprg P Ext"
schirmer@12854: by (simp add: is_acc_class_def)
schirmer@12854: 
schirmer@12854: lemma Ext_is_acc_type[simp]: "is_acc_type tprg P (Class Ext)"
schirmer@12854: by (simp add: is_acc_type_def)
schirmer@12854: 
schirmer@12854: lemma accmethd_tprg_Object [simp]: "accmethd tprg S Object = empty"
schirmer@12854: apply (unfold accmethd_def)
schirmer@12854: apply (simp)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma  snd_special_simp: "snd ((\<lambda>(s, m). (s, a, m)) x) = (a,snd x)"
schirmer@12854: by (cases x) (auto)
schirmer@12854: 
schirmer@12854: lemma  fst_special_simp: "fst ((\<lambda>(s, m). (s, a, m)) x) = fst x"
schirmer@12854: by (cases x) (auto)
schirmer@12854: 
schirmer@12854: lemma foo_sig_undeclared_in_Object:
schirmer@12854:   "tprg\<turnstile>mid foo_sig undeclared_in Object"
schirmer@12854: by (auto simp add: undeclared_in_def cdeclaredmethd_def Object_mdecls_def)
schirmer@12854: 
schirmer@12854: lemma unique_sig_Base_foo:
schirmer@12854:  "tprg\<turnstile> mdecl (sig, snd Base_foo) declared_in Base \<Longrightarrow> sig=foo_sig"
schirmer@12854: by (auto simp add: declared_in_def cdeclaredmethd_def 
schirmer@12854:                    Base_foo_def BaseCl_def)
schirmer@12854: 
schirmer@12854: lemma Base_foo_no_override:
schirmer@12854:  "tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides old \<Longrightarrow> P"
schirmer@12854: apply (drule overrides_commonD)
schirmer@12854: apply (clarsimp)
schirmer@12854: apply (frule subclsEval)
schirmer@12854: apply    (rule ws_tprg)
schirmer@12854: apply    (simp)
schirmer@12854: apply    (rule classesDefined) 
schirmer@12854: apply    assumption+
schirmer@12854: apply (frule unique_sig_Base_foo) 
schirmer@12854: apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
schirmer@12854:             dest: unique_sig_Base_foo)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma Base_foo_no_stat_override:
schirmer@12854:  "tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides\<^sub>S old \<Longrightarrow> P"
schirmer@12854: apply (drule stat_overrides_commonD)
schirmer@12854: apply (clarsimp)
schirmer@12854: apply (frule subclsEval)
schirmer@12854: apply    (rule ws_tprg)
schirmer@12854: apply    (simp)
schirmer@12854: apply    (rule classesDefined) 
schirmer@12854: apply    assumption+
schirmer@12854: apply (frule unique_sig_Base_foo) 
schirmer@12854: apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
schirmer@12854:             dest: unique_sig_Base_foo)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
schirmer@12854: lemma Base_foo_no_hide:
schirmer@12854:  "tprg,sig\<turnstile>(Base,(snd Base_foo)) hides old \<Longrightarrow> P"
schirmer@12854: by (auto dest: hidesD simp add: Base_foo_def member_is_static_simp)
schirmer@12854: 
schirmer@12854: lemma Ext_foo_no_hide:
schirmer@12854:  "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) hides old \<Longrightarrow> P"
schirmer@12854: by (auto dest: hidesD simp add: Ext_foo_def member_is_static_simp)
schirmer@12854: 
schirmer@12854: lemma unique_sig_Ext_foo:
schirmer@12854:  "tprg\<turnstile> mdecl (sig, snd Ext_foo) declared_in Ext \<Longrightarrow> sig=foo_sig"
schirmer@12854: by (auto simp add: declared_in_def cdeclaredmethd_def 
schirmer@12854:                    Ext_foo_def ExtCl_def)
schirmer@12854: 
schirmer@12854: lemma Ext_foo_override:
schirmer@12854:  "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides old 
schirmer@12854:   \<Longrightarrow> old = (Base,(snd Base_foo))"
schirmer@12854: apply (drule overrides_commonD)
schirmer@12854: apply (clarsimp)
schirmer@12854: apply (frule subclsEval)
schirmer@12854: apply    (rule ws_tprg)
schirmer@12854: apply    (simp)
schirmer@12854: apply    (rule classesDefined) 
schirmer@12854: apply    assumption+
schirmer@12854: apply (frule unique_sig_Ext_foo) 
schirmer@12854: apply (case_tac "old")
schirmer@12854: apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 
schirmer@12854: apply (auto simp add: ExtCl_def Ext_foo_def
schirmer@12854:                       BaseCl_def Base_foo_def Object_mdecls_def
schirmer@12854:                       split_paired_all
schirmer@12854:                       member_is_static_simp
schirmer@12854:            dest: declared_not_undeclared unique_declaration)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma Ext_foo_stat_override:
schirmer@12854:  "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides\<^sub>S old 
schirmer@12854:   \<Longrightarrow> old = (Base,(snd Base_foo))"
schirmer@12854: apply (drule stat_overrides_commonD)
schirmer@12854: apply (clarsimp)
schirmer@12854: apply (frule subclsEval)
schirmer@12854: apply    (rule ws_tprg)
schirmer@12854: apply    (simp)
schirmer@12854: apply    (rule classesDefined) 
schirmer@12854: apply    assumption+
schirmer@12854: apply (frule unique_sig_Ext_foo) 
schirmer@12854: apply (case_tac "old")
schirmer@12854: apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 
schirmer@12854: apply (auto simp add: ExtCl_def Ext_foo_def
schirmer@12854:                       BaseCl_def Base_foo_def Object_mdecls_def
schirmer@12854:                       split_paired_all
schirmer@12854:                       member_is_static_simp
schirmer@12854:            dest: declared_not_undeclared unique_declaration)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma Base_foo_member_of_Base: 
schirmer@12854:   "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
schirmer@12854: by (auto intro!: members.Immediate Base_declares_foo)
schirmer@12854: 
schirmer@12925: lemma Base_foo_member_in_Base: 
schirmer@12925:   "tprg\<turnstile>(Base,mdecl Base_foo) member_in Base"
schirmer@12925: by (rule member_of_to_member_in [OF Base_foo_member_of_Base])
schirmer@12925: 
schirmer@12854: lemma Ext_foo_member_of_Ext: 
schirmer@12854:   "tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
schirmer@12854: by (auto intro!: members.Immediate Ext_declares_foo)
schirmer@12854: 
schirmer@12925: lemma Ext_foo_member_in_Ext: 
schirmer@12925:   "tprg\<turnstile>(Ext,mdecl Ext_foo) member_in Ext"
schirmer@12925: by (rule member_of_to_member_in [OF Ext_foo_member_of_Ext])
schirmer@12925: 
schirmer@12854: lemma Base_foo_permits_acc:
schirmer@14030:  "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_from S"
schirmer@12854: by ( simp add: permits_acc_def Base_foo_def)
schirmer@12854: 
schirmer@12854: lemma Base_foo_accessible [simp]:
schirmer@12854:  "tprg\<turnstile>(Base,mdecl Base_foo) of Base accessible_from S"
schirmer@12925: by (auto intro: accessible_fromR.Immediate 
schirmer@12854:                 Base_foo_member_of_Base Base_foo_permits_acc)
schirmer@12854: 
schirmer@12925: lemma Base_foo_dyn_accessible [simp]:
schirmer@12925:  "tprg\<turnstile>(Base,mdecl Base_foo) in Base dyn_accessible_from S"
schirmer@12925: apply (rule dyn_accessible_fromR.Immediate)
schirmer@12925: apply   (rule Base_foo_member_in_Base)
schirmer@12925: apply   (rule Base_foo_permits_acc)
schirmer@12925: done
schirmer@12925: 
schirmer@12854: lemma accmethd_Base [simp]: 
schirmer@12854:   "accmethd tprg S Base = methd tprg Base"
schirmer@12854: apply (simp add: accmethd_def)
schirmer@12854: apply (rule filter_tab_all_True)
schirmer@12854: apply (simp add: snd_special_simp fst_special_simp)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma Ext_foo_permits_acc:
schirmer@14030:  "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_from S"
schirmer@12854: by ( simp add: permits_acc_def Ext_foo_def)
schirmer@12854: 
schirmer@12854: lemma Ext_foo_accessible [simp]:
schirmer@12854:  "tprg\<turnstile>(Ext,mdecl Ext_foo) of Ext accessible_from S"
schirmer@12925: by (auto intro: accessible_fromR.Immediate 
schirmer@12854:                 Ext_foo_member_of_Ext Ext_foo_permits_acc)
schirmer@12854: 
schirmer@12925: lemma Ext_foo_dyn_accessible [simp]:
schirmer@12925:  "tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from S"
schirmer@12925: apply (rule dyn_accessible_fromR.Immediate) 
schirmer@12925: apply   (rule Ext_foo_member_in_Ext)
schirmer@12925: apply   (rule Ext_foo_permits_acc)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma Ext_foo_overrides_Base_foo:
schirmer@12854:  "tprg\<turnstile>(Ext,Ext_foo) overrides (Base,Base_foo)"
schirmer@12854: proof (rule overridesR.Direct, simp_all)
schirmer@12854:   show "\<not> is_static Ext_foo" 
schirmer@12854:     by (simp add: member_is_static_simp Ext_foo_def)
schirmer@12854:   show "\<not> is_static Base_foo"
schirmer@12854:     by (simp add: member_is_static_simp Base_foo_def)
schirmer@12854:   show "accmodi Ext_foo \<noteq> Private"
schirmer@12854:     by (simp add: Ext_foo_def)
schirmer@12854:   show "msig (Ext, Ext_foo) = msig (Base, Base_foo)"
schirmer@12854:     by (simp add: Ext_foo_def Base_foo_def)
schirmer@12854:   show "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
schirmer@12854:     by (auto intro: Ext_declares_foo)
schirmer@12854:   show "tprg\<turnstile>mdecl Base_foo declared_in Base"
schirmer@12854:     by (auto intro: Base_declares_foo)
schirmer@12854:   show "tprg \<turnstile>(Base, mdecl Base_foo) inheritable_in java_lang"
schirmer@12854:     by (simp add: inheritable_in_def Base_foo_def)
schirmer@12854:   show "tprg\<turnstile>resTy Ext_foo\<preceq>resTy Base_foo"
schirmer@12854:     by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp)
schirmer@12854: qed
schirmer@12854: 
schirmer@12854: lemma accmethd_Ext [simp]: 
schirmer@12854:   "accmethd tprg S Ext = methd tprg Ext"
schirmer@12854: apply (simp add: accmethd_def)
schirmer@12854: apply (rule filter_tab_all_True)
schirmer@12854: apply (auto simp add: snd_special_simp fst_special_simp)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma cls_Ext: "class tprg Ext = Some ExtCl"
schirmer@12854: by simp
schirmer@12854: lemma dynmethd_Ext_foo:
schirmer@12854:  "dynmethd tprg Base Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 
schirmer@12854:   = Some (Ext,snd Ext_foo)"
schirmer@12854: proof -
schirmer@12854:   have "methd tprg Base \<lparr>name = foo, parTs = [Class Base]\<rparr> 
schirmer@12854:           = Some (Base,snd Base_foo)" and
schirmer@12854:        "methd tprg Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 
schirmer@12854:           = Some (Ext,snd Ext_foo)" 
schirmer@12854:     by (auto simp add: Ext_foo_def Base_foo_def foo_sig_def)
schirmer@12854:   with cls_Ext ws_tprg Ext_foo_overrides_Base_foo
schirmer@12854:   show ?thesis
schirmer@12854:     by (auto simp add: dynmethd_rec simp add: Ext_foo_def Base_foo_def)
schirmer@12854: qed
schirmer@12854: 
schirmer@12854: lemma Base_fields_accessible[simp]:
schirmer@12854:  "accfield tprg S Base 
schirmer@12854:   = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))"
schirmer@12854: apply (auto simp add: accfield_def expand_fun_eq Let_def 
schirmer@12854:                       accessible_in_RefT_simp
schirmer@12854:                       is_public_def
schirmer@12854:                       BaseCl_def
schirmer@12854:                       permits_acc_def
schirmer@12854:                       declared_in_def 
schirmer@12854:                       cdeclaredfield_def
schirmer@12854:                intro!: filter_tab_all_True_Some filter_tab_None
schirmer@12925:                        accessible_fromR.Immediate
schirmer@12854:                intro: members.Immediate)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
schirmer@12854: lemma arr_member_of_Base:
schirmer@12854:   "tprg\<turnstile>(Base, fdecl (arr, 
schirmer@12854:                  \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
schirmer@12854:           member_of Base"
schirmer@12854: by (auto intro: members.Immediate 
schirmer@12854:        simp add: declared_in_def cdeclaredfield_def BaseCl_def)
schirmer@12854:  
schirmer@12925: lemma arr_member_in_Base:
schirmer@12925:   "tprg\<turnstile>(Base, fdecl (arr, 
schirmer@12925:                  \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
schirmer@12925:           member_in Base"
schirmer@12925: by (rule member_of_to_member_in [OF arr_member_of_Base])
schirmer@12925: 
schirmer@12854: lemma arr_member_of_Ext:
schirmer@12854:   "tprg\<turnstile>(Base, fdecl (arr, 
schirmer@12854:                     \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
schirmer@12854:              member_of Ext"
schirmer@12854: apply (rule members.Inherited)
schirmer@12854: apply   (simp add: inheritable_in_def)
schirmer@12854: apply   (simp add: undeclared_in_def cdeclaredfield_def ExtCl_def)
schirmer@12854: apply   (auto intro: arr_member_of_Base simp add: subcls1_def ExtCl_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12925: lemma arr_member_in_Ext:
schirmer@12925:   "tprg\<turnstile>(Base, fdecl (arr, 
schirmer@12925:                  \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
schirmer@12925:           member_in Ext"
schirmer@12925: by (rule member_of_to_member_in [OF arr_member_of_Ext])
schirmer@12925: 
schirmer@12854: lemma Ext_fields_accessible[simp]:
schirmer@12854: "accfield tprg S Ext 
schirmer@12854:   = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))"
schirmer@12854: apply (auto simp add: accfield_def expand_fun_eq Let_def 
schirmer@12854:                       accessible_in_RefT_simp
schirmer@12854:                       is_public_def
schirmer@12854:                       BaseCl_def
schirmer@12854:                       ExtCl_def
schirmer@12854:                       permits_acc_def
schirmer@12854:                intro!: filter_tab_all_True_Some filter_tab_None
schirmer@12925:                        accessible_fromR.Immediate)
schirmer@12854: apply (auto intro: members.Immediate arr_member_of_Ext
schirmer@12854:             simp add: declared_in_def cdeclaredfield_def ExtCl_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12925: lemma arr_Base_dyn_accessible [simp]:
schirmer@12925: "tprg\<turnstile>(Base, fdecl (arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>)) 
schirmer@12925:        in Base dyn_accessible_from S"
schirmer@12925: apply (rule dyn_accessible_fromR.Immediate)
schirmer@12925: apply   (rule arr_member_in_Base)
schirmer@12925: apply   (simp add: permits_acc_def)
schirmer@12925: done
schirmer@12925: 
schirmer@12925: lemma arr_Ext_dyn_accessible[simp]:
schirmer@12925: "tprg\<turnstile>(Base, fdecl (arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>)) 
schirmer@12925:        in Ext dyn_accessible_from S"
schirmer@12925: apply (rule dyn_accessible_fromR.Immediate)
schirmer@12925: apply   (rule arr_member_in_Ext)
schirmer@12925: apply   (simp add: permits_acc_def)
schirmer@12925: done
schirmer@12925: 
schirmer@12854: lemma array_of_PrimT_acc [simp]:
schirmer@12854:  "is_acc_type tprg java_lang (PrimT t.[])"
schirmer@12854: apply (simp add: is_acc_type_def accessible_in_RefT_simp)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma PrimT_acc [simp]: 
schirmer@12854:  "is_acc_type tprg java_lang (PrimT t)"
schirmer@12854: apply (simp add: is_acc_type_def accessible_in_RefT_simp)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma Object_acc [simp]:
schirmer@12854:  "is_acc_class tprg java_lang Object"
schirmer@12854: apply (auto simp add: is_acc_class_def accessible_in_RefT_simp is_public_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
schirmer@12854: section "well-formedness"
schirmer@12854: 
schirmer@12854: 
schirmer@12854: lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)"
schirmer@12854: apply (unfold wf_idecl_def HasFooInt_def)
schirmer@12854: apply (auto intro!: wf_mheadI ws_idecl_HasFoo 
schirmer@12854:             simp add: foo_sig_def foo_mhead_def mhead_resTy_simp
schirmer@12854:                       member_is_static_simp )
schirmer@12854: done
schirmer@12854: 
schirmer@12925: 
schirmer@12925: declare member_is_static_simp [simp]
schirmer@12854: declare wt.Skip [rule del] wt.Init [rule del]
wenzelm@26480: ML {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
schirmer@13688: lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
schirmer@13688: lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
schirmer@13688: 
schirmer@12854: lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
schirmer@12854: lemmas Ext_foo_defs  = Ext_foo_def  foo_sig_def
schirmer@13688: 
schirmer@13688: 
schirmer@13688: 
schirmer@12854: 
schirmer@12854: lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo"
schirmer@12854: apply (unfold Base_foo_defs )
schirmer@13688: apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs 
schirmer@12854:             simp add: mhead_resTy_simp)
schirmer@13688: (* for definite assignment *)
schirmer@13688: apply (rule exI)
schirmer@13688: apply (simp add: parameters_def)
schirmer@13688: apply (rule conjI)
schirmer@13688: apply  (rule da.Comp)
schirmer@13688: apply     (rule da.Expr)
schirmer@13688: apply     (rule da.AssLVar)
schirmer@13688: apply       (rule da.AccLVar)
schirmer@13688: apply         (simp)
schirmer@13688: apply        (rule assigned.select_convs)
schirmer@13688: apply       (simp)
schirmer@13688: apply      (rule assigned.select_convs)
schirmer@13688: apply     (simp)
schirmer@13688: apply    (simp)
schirmer@13688: apply    (rule da.Jmp)
schirmer@13688: apply      (simp)
schirmer@13688: apply     (rule assigned.select_convs)
schirmer@13688: apply    (simp)
schirmer@13688: apply   (rule assigned.select_convs)
schirmer@13688: apply  (simp)
schirmer@13688: apply (simp)
schirmer@12854: done
schirmer@12854: 
schirmer@13688: 
schirmer@12854: lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo"
schirmer@12854: apply (unfold Ext_foo_defs )
schirmer@12854: apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs 
schirmer@12854:             simp add: mhead_resTy_simp )
schirmer@12854: apply  (rule wt.Cast)
schirmer@12854: prefer 2
schirmer@12854: apply    simp
schirmer@12854: apply   (rule_tac [2] narrow.subcls [THEN cast.narrow])
schirmer@12854: apply   (auto intro!: wtIs)
schirmer@13688: (* for definite assignment *)
schirmer@13688: apply (rule exI)
schirmer@13688: apply (simp add: parameters_def)
schirmer@13688: apply (rule conjI)
schirmer@13688: apply  (rule da.Comp)
schirmer@13688: apply     (rule da.Expr)
schirmer@13688: apply     (rule da.Ass)   
schirmer@13688: apply       simp
schirmer@13688: apply      (rule da.FVar)
schirmer@13688: apply      (rule da.Cast)
schirmer@13688: apply      (rule da.AccLVar)
schirmer@13688: apply        simp
schirmer@13688: apply       (rule assigned.select_convs)
schirmer@13688: apply      simp
schirmer@13688: apply     (rule da_Lit)
schirmer@13688: apply     (simp)
schirmer@13688: apply    (rule da.Comp)
schirmer@13688: apply       (rule da.Expr)
schirmer@13688: apply       (rule da.AssLVar)
schirmer@13688: apply         (rule da.Lit)                  
schirmer@13688: apply        (rule assigned.select_convs)
schirmer@13688: apply       simp
schirmer@13688: apply      (rule da.Jmp)
schirmer@13688: apply        simp
schirmer@13688: apply       (rule assigned.select_convs)
schirmer@13688: apply      simp
schirmer@13688: apply     (rule assigned.select_convs)
schirmer@13688: apply    (simp)
schirmer@13688: apply   (rule assigned.select_convs)
schirmer@13688: apply  simp
schirmer@13688: apply simp
schirmer@12854: done
schirmer@12854: 
schirmer@12854: declare mhead_resTy_simp [simp add]
schirmer@12854: declare member_is_static_simp [simp add]
schirmer@12854: 
schirmer@12854: lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
schirmer@12854: apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
schirmer@12854: apply (auto intro!: wf_Base_foo)
schirmer@13688: apply        (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def)
schirmer@13688: apply   (auto intro!: wtIs)
schirmer@13688: (* for definite assignment *)
schirmer@13688: apply   (rule exI)
schirmer@13688: apply   (rule da.Expr)
schirmer@13688: apply  (rule da.Ass)
schirmer@13688: apply    (simp)
schirmer@13688: apply   (rule da.FVar)
schirmer@13688: apply   (rule da.Cast)
schirmer@13688: apply   (rule da_Lit)
schirmer@13688: apply   simp
schirmer@13688: apply  (rule da.NewA)
schirmer@13688: apply  (rule da.Lit)
schirmer@12854: apply (auto simp add: Base_foo_defs entails_def Let_def)
schirmer@12854: apply   (insert Base_foo_no_stat_override, simp add: Base_foo_def,blast)+
schirmer@13688: apply (insert Base_foo_no_hide         , simp add: Base_foo_def,blast)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
schirmer@12854: lemma wf_ExtC: "wf_cdecl tprg (Ext,ExtCl)"
schirmer@12854: apply (unfold wf_cdecl_def ExtCl_def)
schirmer@12854: apply (auto intro!: wf_Ext_foo ws_cdecl_Ext)
schirmer@13688: apply  (auto simp add: entails_def snd_special_simp)
schirmer@13688: apply      (insert Ext_foo_stat_override)
schirmer@13688: apply      (rule exI,rule da.Skip)      
schirmer@13688: apply     (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
schirmer@13688: apply    (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
schirmer@13688: apply   (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
schirmer@13688: apply  (insert Ext_foo_no_hide)
schirmer@12854: apply  (simp_all add: qmdecl_def)
schirmer@12854: apply  blast+
schirmer@12854: done
schirmer@12854: 
schirmer@12925: lemma wf_MainC: "wf_cdecl tprg (Main,MainCl)"
schirmer@12925: apply (unfold wf_cdecl_def MainCl_def)
schirmer@12925: apply (auto intro: ws_cdecl_Main)
schirmer@13688: apply (rule exI,rule da.Skip)
schirmer@12925: done
schirmer@12925: 
schirmer@12854: lemma wf_idecl_all: "p=tprg \<Longrightarrow> Ball (set Ifaces) (wf_idecl p)"
schirmer@12854: apply (simp (no_asm) add: Ifaces_def)
schirmer@12854: apply (simp (no_asm_simp))
schirmer@12854: apply (rule wf_HasFoo)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma wf_cdecl_all_standard_classes: 
schirmer@12854:   "Ball (set standard_classes) (wf_cdecl tprg)"
schirmer@12854: apply (unfold standard_classes_def Let_def 
schirmer@12854:        ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
nipkow@18576: apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
schirmer@13688: apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def 
schirmer@13688:             intro: da.Skip)
schirmer@12854: apply (auto simp add: Object_def Classes_def standard_classes_def 
schirmer@12854:                       SXcptC_def SXcpt_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma wf_cdecl_all: "p=tprg \<Longrightarrow> Ball (set Classes) (wf_cdecl p)"
schirmer@12854: apply (simp (no_asm) add: Classes_def)
schirmer@12854: apply (simp (no_asm_simp))
schirmer@12925: apply    (rule wf_BaseC [THEN conjI])
schirmer@12925: apply   (rule wf_ExtC [THEN conjI])
schirmer@12925: apply  (rule wf_MainC [THEN conjI])
schirmer@12854: apply (rule wf_cdecl_all_standard_classes)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: theorem wf_tprg: "wf_prog tprg"
schirmer@12854: apply (unfold wf_prog_def Let_def)
schirmer@12854: apply (simp (no_asm) add: unique_ifaces unique_classes)
schirmer@12854: apply (rule conjI)
schirmer@12854: apply  ((simp (no_asm) add: Classes_def standard_classes_def))
schirmer@12854: apply (rule conjI)
schirmer@12854: apply (simp add: Object_mdecls_def)
schirmer@12854: apply safe
schirmer@13688: apply  (cut_tac xn_cases)   
schirmer@12854: apply  (simp (no_asm_simp) add: Classes_def standard_classes_def)
schirmer@12854: apply  (insert wf_idecl_all)
schirmer@12854: apply  (insert wf_cdecl_all)
schirmer@12854: apply  auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: section "max spec"
schirmer@12854: 
schirmer@12854: lemma appl_methds_Base_foo: 
schirmer@12854: "appl_methds tprg S (ClassT Base) \<lparr>name=foo, parTs=[NT]\<rparr> =  
schirmer@12854:   {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
schirmer@12854:     ,[Class Base])}"
schirmer@12854: apply (unfold appl_methds_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
schirmer@12854: apply  (auto simp add: cmheads_def Base_foo_defs)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = 
schirmer@12854:   {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
schirmer@12854:    , [Class Base])}"
schirmer@12854: apply (unfold max_spec_def)
schirmer@12854: apply (simp (no_asm) add: appl_methds_Base_foo)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: section "well-typedness"
schirmer@12854: 
schirmer@12925: lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
schirmer@12854: apply (unfold test_def arr_viewed_from_def)
schirmer@12854: (* ?pTs = [Class Base] *)
schirmer@12854: apply (rule wtIs (* ;; *))
schirmer@12854: apply  (rule wtIs (* Ass *))
schirmer@12854: apply  (rule wtIs (* NewC *))
schirmer@12854: apply     (rule wtIs (* LVar *))
schirmer@12854: apply      (simp)
schirmer@12854: apply     (simp)
schirmer@12854: apply    (simp)
schirmer@12854: apply   (rule wtIs (* NewC *))
schirmer@12854: apply   (simp)
schirmer@12854: apply  (simp)
schirmer@12854: apply (rule wtIs (* Try *))
schirmer@12854: prefer 4
schirmer@12854: apply    (simp)
schirmer@12854: defer
schirmer@12854: apply    (rule wtIs (* Expr *))
schirmer@12854: apply    (rule wtIs (* Call *))
schirmer@12854: apply       (rule wtIs (* Acc *))
schirmer@12854: apply       (rule wtIs (* LVar *))
schirmer@12854: apply        (simp)
schirmer@12854: apply       (simp)
schirmer@12854: apply      (rule wtIs (* Cons *))
schirmer@12854: apply       (rule wtIs (* Lit *))
schirmer@12854: apply       (simp)
schirmer@12854: apply      (rule wtIs (* Nil *))
schirmer@12854: apply     (simp)
schirmer@12854: apply     (rule max_spec_Base_foo)
schirmer@12854: apply    (simp)
schirmer@12854: apply   (simp)
schirmer@12854: apply  (simp)
schirmer@12854: apply  (simp)
schirmer@12925: apply  (simp)
schirmer@12854: apply (rule wtIs (* While *))
schirmer@12854: apply  (rule wtIs (* Acc *))
schirmer@12854: apply   (rule wtIs (* AVar *))
schirmer@12854: apply   (rule wtIs (* Acc *))
schirmer@12854: apply   (rule wtIs (* FVar *))
schirmer@12854: apply    (rule wtIs (* StatRef *))
schirmer@12854: apply    (simp)
schirmer@12854: apply   (simp)
schirmer@12854: apply   (simp )
schirmer@12854: apply   (simp)
schirmer@12925: apply   (simp)
schirmer@12854: apply  (rule wtIs (* LVar *))
schirmer@12854: apply  (simp)
schirmer@12854: apply (rule wtIs (* Skip *))
schirmer@12854: done
schirmer@12854: 
schirmer@13688: section "definite assignment"
schirmer@13688: 
schirmer@13688: lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
schirmer@13688:                   \<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
schirmer@13688: apply (unfold test_def arr_viewed_from_def)
schirmer@13688: apply (rule da.Comp)
schirmer@13688: apply    (rule da.Expr)
schirmer@13688: apply    (rule da.AssLVar)
schirmer@13688: apply      (rule da.NewC)
schirmer@13688: apply     (rule assigned.select_convs)
schirmer@13688: apply    (simp)
schirmer@13688: apply   (rule da.Try)
schirmer@13688: apply      (rule da.Expr)
schirmer@13688: apply      (rule da.Call)
schirmer@13688: apply       (rule da.AccLVar)
schirmer@13688: apply         (simp)   
schirmer@13688: apply        (rule assigned.select_convs)
schirmer@13688: apply       (simp)
schirmer@13688: apply      (rule da.Cons)
schirmer@13688: apply       (rule da.Lit)
schirmer@13688: apply      (rule da.Nil)
schirmer@13688: apply     (rule da.Loop)
schirmer@13688: apply        (rule da.Acc)
schirmer@13688: apply         (simp)
schirmer@13688: apply        (rule da.AVar)
schirmer@13688: apply         (rule da.Acc)
schirmer@13688: apply          simp
schirmer@13688: apply         (rule da.FVar)
schirmer@13688: apply         (rule da.Cast)
schirmer@13688: apply         (rule da.Lit)
schirmer@13688: apply        (rule da.Lit)
schirmer@13688: apply       (rule da_Skip)
schirmer@13688: apply       (simp)
schirmer@13688: apply      (simp,rule assigned.select_convs)
schirmer@13688: apply     (simp)
schirmer@13688: apply    (simp,rule assigned.select_convs)
schirmer@13688: apply   (simp)
schirmer@13688: apply  simp
schirmer@13688: apply  blast
schirmer@13688: apply simp
schirmer@13688: apply (simp add: intersect_ts_def)
schirmer@13688: done
schirmer@13688: 
schirmer@12854: 
schirmer@12854: section "execution"
schirmer@12854: 
schirmer@12854: lemma alloc_one: "\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow>  
schirmer@12854:   new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n"
schirmer@12854: apply (frule atleast_free_SucD)
schirmer@12854: apply (drule atleast_free_Suc [THEN iffD1])
schirmer@12854: apply clarsimp
schirmer@12854: apply (frule new_Addr_SomeI)
schirmer@12854: apply force
schirmer@12854: done
schirmer@12854: 
schirmer@12854: declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp]
schirmer@12854: declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp]
schirmer@12854: declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
schirmer@12854:         Base_foo_defs  [simp]
schirmer@12854: 
wenzelm@26480: ML {* bind_thms ("eval_intros", map 
wenzelm@26342:         (simplify (@{simpset} delsimps @{thms Skip_eq}
wenzelm@24019:                              addsimps @{thms lvar_def}) o 
wenzelm@24019:          rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
schirmer@12854: lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
schirmer@12854: 
schirmer@12854: consts
schirmer@12854:   a :: loc
schirmer@12854:   b :: loc
schirmer@12854:   c :: loc
schirmer@12854: 
wenzelm@21404: abbreviation "one == Suc 0"
wenzelm@21404: abbreviation "two == Suc one"
wenzelm@21404: abbreviation "tree == Suc two"
wenzelm@21404: abbreviation "four == Suc tree"
schirmer@12854: 
wenzelm@20769: syntax
schirmer@12854:   obj_a :: obj
schirmer@12854:   obj_b :: obj
schirmer@12854:   obj_c :: obj
schirmer@12854:   arr_N :: "(vn, val) table"
schirmer@12854:   arr_a :: "(vn, val) table"
schirmer@12854:   globs1 :: globs
schirmer@12854:   globs2 :: globs
schirmer@12854:   globs3 :: globs
schirmer@12854:   globs8 :: globs
schirmer@12854:   locs3 :: locals
schirmer@12854:   locs4 :: locals
schirmer@12854:   locs8 :: locals
schirmer@12854:   s0  :: state
schirmer@12854:   s0' :: state
schirmer@12854:   s9' :: state
schirmer@12854:   s1  :: state
schirmer@12854:   s1' :: state
schirmer@12854:   s2  :: state
schirmer@12854:   s2' :: state
schirmer@12854:   s3  :: state
schirmer@12854:   s3' :: state
schirmer@12854:   s4  :: state
schirmer@12854:   s4' :: state
schirmer@12854:   s6' :: state
schirmer@12854:   s7' :: state
schirmer@12854:   s8  :: state
schirmer@12854:   s8' :: state
schirmer@12854: 
schirmer@12854: translations
wenzelm@20769:   "obj_a"   <= "\<lparr>tag=Arr (PrimT Boolean) (CONST two)
wenzelm@20769:                 ,values=CONST empty(Inr 0\<mapsto>Bool False)(Inr (CONST one)\<mapsto>Bool False)\<rparr>"
wenzelm@20769:   "obj_b"   <= "\<lparr>tag=CInst (CONST Ext)
wenzelm@20769:                 ,values=(CONST empty(Inl (CONST vee, CONST Base)\<mapsto>Null   ) 
wenzelm@20769:                               (Inl (CONST vee, CONST Ext )\<mapsto>Intg 0))\<rparr>"
wenzelm@20769:   "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
wenzelm@20769:   "arr_N"   == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Null)"
wenzelm@20769:   "arr_a"   == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Addr a)"
haftmann@28524:   "globs1"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
haftmann@28524:                      (Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_N\<rparr>)
haftmann@28524:                      (Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)"
haftmann@28524:   "globs2"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
haftmann@28524:                      (Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
wenzelm@20769:                      (Inl a\<mapsto>obj_a)
haftmann@28524:                      (Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_a\<rparr>)"
schirmer@12854:   "globs3"  == "globs2(Inl b\<mapsto>obj_b)"
schirmer@12854:   "globs8"  == "globs3(Inl c\<mapsto>obj_c)"
wenzelm@20769:   "locs3"   == "CONST empty(VName (CONST e)\<mapsto>Addr b)"
wenzelm@20769:   "locs4"   == "CONST empty(VName (CONST z)\<mapsto>Null)(Inr()\<mapsto>Addr b)"
wenzelm@20769:   "locs8"   == "locs3(VName (CONST z)\<mapsto>Addr c)"
wenzelm@20769:   "s0"  == "       st (CONST empty) (CONST empty)"
schirmer@12854:   "s0'" == " Norm  s0"
wenzelm@20769:   "s1"  == "       st globs1 (CONST empty)"
schirmer@12854:   "s1'" == " Norm  s1"
wenzelm@20769:   "s2"  == "       st globs2 (CONST empty)"
schirmer@12854:   "s2'" == " Norm  s2"
schirmer@12854:   "s3"  == "       st globs3 locs3 "
schirmer@12854:   "s3'" == " Norm  s3"
schirmer@12854:   "s4"  == "       st globs3 locs4"
schirmer@12854:   "s4'" == " Norm  s4"
schirmer@12854:   "s6'" == "(Some (Xcpt (Std NullPointer)), s4)"
schirmer@12854:   "s7'" == "(Some (Xcpt (Std NullPointer)), s3)"
schirmer@12854:   "s8"  == "       st globs8 locs8"
schirmer@12854:   "s8'" == " Norm  s8"
schirmer@12854:   "s9'" == "(Some (Xcpt (Std IndOutBound)), s8)"
schirmer@12854: 
schirmer@12854: 
schirmer@12854: declare Pair_eq [simp del]
schirmer@12854: lemma exec_test: 
schirmer@12854: "\<lbrakk>the (new_Addr (heap  s1)) = a;  
schirmer@12854:   the (new_Addr (heap ?s2)) = b;  
schirmer@12854:   the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>  
schirmer@12854:   atleast_free  (heap s0) four \<Longrightarrow>  
schirmer@12854:   tprg\<turnstile>s0' \<midarrow>test [Class Base]\<rightarrow> ?s9'"
schirmer@12854: apply (unfold test_def arr_viewed_from_def)
schirmer@12854: (* ?s9' = s9' *)
schirmer@12854: apply (simp (no_asm_use))
schirmer@12854: apply (drule (1) alloc_one,clarsimp)
schirmer@12854: apply (rule eval_Is (* ;; *))
schirmer@12854: apply  (erule_tac V = "the (new_Addr ?h) = c" in thin_rl)
schirmer@12854: apply  (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
schirmer@12854: apply  (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
schirmer@12854: apply  (rule eval_Is (* Expr *))
schirmer@12854: apply  (rule eval_Is (* Ass *))
schirmer@12854: apply   (rule eval_Is (* LVar *))
schirmer@12854: apply  (rule eval_Is (* NewC *))
schirmer@12854:       (* begin init Ext *)
schirmer@12854: apply   (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
schirmer@12854: apply   (erule_tac V = "atleast_free ?h tree" in thin_rl)
schirmer@12854: apply   (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
schirmer@12854: apply   (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
schirmer@12854: apply   (rule eval_Is (* Init Ext *))
schirmer@12854: apply   (simp)
schirmer@12854: apply   (rule conjI)
schirmer@12854: prefer 2 apply (rule conjI HOL.refl)+
schirmer@12854: apply   (rule eval_Is (* Init Base *))
schirmer@12854: apply   (simp add: arr_viewed_from_def)
schirmer@12854: apply   (rule conjI)
schirmer@12854: apply    (rule eval_Is (* Init Object *))
schirmer@12854: apply    (simp)
schirmer@12854: apply    (rule conjI, rule HOL.refl)+
schirmer@12854: apply    (rule HOL.refl)
schirmer@12854: apply   (simp)
schirmer@12854: apply   (rule conjI, rule_tac [2] HOL.refl)
schirmer@12854: apply   (rule eval_Is (* Expr *))
schirmer@12854: apply   (rule eval_Is (* Ass *))
schirmer@12854: apply    (rule eval_Is (* FVar *))
schirmer@12925: apply         (rule init_done, simp)
schirmer@12925: apply        (rule eval_Is (* StatRef *))
schirmer@12925: apply       (simp)
schirmer@12925: apply     (simp add: check_field_access_def Let_def) 
schirmer@12854: apply   (rule eval_Is (* NewA *))
schirmer@12854: apply     (simp)
schirmer@12854: apply    (rule eval_Is (* Lit *))
schirmer@12854: apply   (simp)
schirmer@12854: apply   (rule halloc.New)
schirmer@12854: apply    (simp (no_asm_simp))
schirmer@13688: apply   (drule atleast_free_weaken,drule atleast_free_weaken)
schirmer@12854: apply   (simp (no_asm_simp))
schirmer@12854: apply  (simp add: upd_gobj_def)
schirmer@12854:       (* end init Ext *)
schirmer@12854: apply  (rule halloc.New)
schirmer@12854: apply   (drule alloc_one)
schirmer@12854: prefer 2 apply fast
schirmer@12854: apply   (simp (no_asm_simp))
schirmer@12854: apply  (drule atleast_free_weaken)
schirmer@12854: apply  force
schirmer@12854: apply (simp)
schirmer@12854: apply (drule alloc_one)
schirmer@12854: apply  (simp (no_asm_simp))
schirmer@12854: apply clarsimp
schirmer@12854: apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
schirmer@12854: apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
schirmer@12854: apply (simp (no_asm_use))
schirmer@12854: apply (rule eval_Is (* Try *))
schirmer@12854: apply   (rule eval_Is (* Expr *))
schirmer@12854:       (* begin method call *)
schirmer@12854: apply   (rule eval_Is (* Call *))
schirmer@12854: apply      (rule eval_Is (* Acc *))
schirmer@12854: apply      (rule eval_Is (* LVar *))
schirmer@12854: apply     (rule eval_Is (* Cons *))
schirmer@12854: apply      (rule eval_Is (* Lit *))
schirmer@12854: apply     (rule eval_Is (* Nil *))
schirmer@12854: apply    (simp)
schirmer@12925: apply    (simp)
schirmer@12925: apply    (subgoal_tac
schirmer@12925:              "tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from Main")
schirmer@12925: apply      (simp add: check_method_access_def Let_def
schirmer@12925:                       invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
schirmer@12925: apply      (rule Ext_foo_dyn_accessible)
schirmer@12854: apply   (rule eval_Is (* Methd *))
schirmer@12854: apply   (simp add: body_def Let_def)
schirmer@12854: apply   (rule eval_Is (* Body *))
schirmer@12854: apply     (rule init_done, simp)
schirmer@12854: apply       (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
schirmer@12854: apply    (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
schirmer@13688: apply    (rule eval_Is (* Comp *))
schirmer@13688: apply     (rule eval_Is (* Expr *))
schirmer@13688: apply     (rule eval_Is (* Ass *))
schirmer@13688: apply      (rule eval_Is (* FVar *))
schirmer@13688: apply         (rule init_done, simp)
schirmer@13688: apply        (rule eval_Is (* Cast *))
schirmer@13688: apply         (rule eval_Is (* Acc *))
schirmer@13688: apply         (rule eval_Is (* LVar *))
schirmer@13688: apply        (simp)
schirmer@13688: apply       (simp split del: split_if)
schirmer@12925: apply      (simp add: check_field_access_def Let_def)
schirmer@13688: apply     (rule eval_Is (* XcptE *))
schirmer@13688: apply    (simp)
schirmer@13688: apply    (rule conjI)
schirmer@13688: apply     (simp)
schirmer@13688: apply    (rule eval_Is (* Comp *))
schirmer@12854: apply   (simp)
schirmer@12854:       (* end method call *)
schirmer@13688: apply  simp
schirmer@12854: apply  (rule sxalloc.intros)
schirmer@12854: apply  (rule halloc.New)
schirmer@12854: apply   (erule alloc_one [THEN conjunct1])
schirmer@12854: apply   (simp (no_asm_simp))
schirmer@12854: apply  (simp (no_asm_simp))
schirmer@12854: apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
schirmer@12854: apply (drule alloc_one [THEN conjunct1])
schirmer@12854: apply  (simp (no_asm_simp))
schirmer@12854: apply (erule_tac V = "atleast_free ?h two" in thin_rl)
schirmer@12854: apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
schirmer@12854: apply simp
schirmer@12854: apply (rule eval_Is (* While *))
schirmer@12854: apply  (rule eval_Is (* Acc *))
schirmer@12854: apply  (rule eval_Is (* AVar *))
schirmer@12854: apply    (rule eval_Is (* Acc *))
schirmer@12854: apply    (rule eval_Is (* FVar *))
schirmer@12854: apply      (rule init_done, simp)
schirmer@12854: apply     (rule eval_Is (* StatRef *))
schirmer@12854: apply    (simp)
schirmer@12925: apply    (simp add: check_field_access_def Let_def)
schirmer@12854: apply   (rule eval_Is (* Lit *))
schirmer@12854: apply  (simp (no_asm_simp))
schirmer@12854: apply (auto simp add: in_bounds_def)
schirmer@12854: done
schirmer@12854: declare Pair_eq [simp]
schirmer@12854: 
schirmer@12854: end




