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: "\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' \ tnam" wenzelm@22708: vnam' :: "vnam' \ vname" wenzelm@22708: label':: "label' \ 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': "\m. n = tnam' m" wenzelm@22708: surj_vnam': "\m. n = vnam' m" wenzelm@22708: surj_label':" \m. n = label' m" schirmer@12854: wenzelm@20769: abbreviation wenzelm@21404: HasFoo :: qtname where wenzelm@22708: "HasFoo == \pid=java_lang,tid=TName (tnam' HasFoo')\" wenzelm@20769: wenzelm@21404: abbreviation wenzelm@21404: Base :: qtname where wenzelm@22708: "Base == \pid=java_lang,tid=TName (tnam' Base')\" wenzelm@20769: wenzelm@21404: abbreviation wenzelm@21404: Ext :: qtname where wenzelm@22708: "Ext == \pid=java_lang,tid=TName (tnam' Ext')\" wenzelm@20769: wenzelm@21404: abbreviation wenzelm@21404: Main :: qtname where wenzelm@22708: "Main == \pid=java_lang,tid=TName (tnam' Main')\" 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\Object" schirmer@12854: by (simp add: Object_def) schirmer@12854: schirmer@12854: lemma neq_Ext_Object [simp]: "Ext\Object" schirmer@12854: by (simp add: Object_def) schirmer@12854: schirmer@12925: lemma neq_Main_Object [simp]: "Main\Object" schirmer@12925: by (simp add: Object_def) schirmer@12925: schirmer@12854: lemma neq_Base_SXcpt [simp]: "Base\SXcpt xn" schirmer@12854: by (simp add: SXcpt_def) schirmer@12854: schirmer@12854: lemma neq_Ext_SXcpt [simp]: "Ext\SXcpt xn" schirmer@12854: by (simp add: SXcpt_def) schirmer@12854: wenzelm@13524: lemma neq_Main_SXcpt [simp]: "Main\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 \ []" schirmer@12854: SXcpt_mdecls_def: "SXcpt_mdecls \ []" 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 \ \name=foo,parTs=[Class Base]\" schirmer@12854: schirmer@12854: foo_mhead :: mhead schirmer@12854: "foo_mhead \ \access=Public,static=False,pars=[z],resT=Class Base\" schirmer@12854: schirmer@12854: constdefs schirmer@12854: schirmer@12854: Base_foo :: mdecl schirmer@12854: "Base_foo \ (foo_sig, \access=Public,static=False,pars=[z],resT=Class Base, schirmer@12854: mbody=\lcls=[],stmt=Return (!!z)\\)" schirmer@12925: schirmer@12925: constdefs schirmer@12854: Ext_foo :: mdecl schirmer@12854: "Ext_foo \ (foo_sig, schirmer@12854: \access=Public,static=False,pars=[z],resT=Class Ext, schirmer@12854: mbody=\lcls=[] schirmer@12925: ,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := schirmer@13688: Lit (Intg 1)) ;; schirmer@13688: Return (Lit Null)\ schirmer@12854: \)" schirmer@12854: schirmer@12854: constdefs schirmer@12854: schirmer@12925: arr_viewed_from :: "qtname \ qtname \ var" schirmer@12925: "arr_viewed_from accC C \ {accC,Base,True}StatRef (ClassT C)..arr" schirmer@12854: haftmann@18551: BaseCl :: "class" schirmer@12854: "BaseCl \ \access=Public, schirmer@12854: cfields=[(arr, \access=Public,static=True ,type=PrimT Boolean.[]\), schirmer@12854: (vee, \access=Public,static=False,type=Iface HasFoo \)], 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]\" schirmer@12854: haftmann@18551: ExtCl :: "class" schirmer@12854: "ExtCl \ \access=Public, schirmer@12854: cfields=[(vee, \access=Public,static=False,type= PrimT Integer\)], schirmer@12854: methods=[Ext_foo], schirmer@12854: init=Skip, schirmer@12854: super=Base, schirmer@12854: superIfs=[]\" schirmer@12854: haftmann@18551: MainCl :: "class" schirmer@12925: "MainCl \ \access=Public, schirmer@12925: cfields=[], schirmer@12925: methods=[], schirmer@12925: init=Skip, schirmer@12925: super=Object, schirmer@12925: superIfs=[]\" schirmer@12925: (* The "main" method is modeled seperately (see tprg) *) schirmer@12925: schirmer@12854: constdefs schirmer@12854: schirmer@12854: HasFooInt :: iface schirmer@12854: "HasFooInt \ \access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\" schirmer@12854: schirmer@12854: Ifaces ::"idecl list" schirmer@12854: "Ifaces \ [(HasFoo,HasFooInt)]" schirmer@12854: schirmer@12854: "Classes" ::"cdecl list" schirmer@12925: "Classes \ [(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\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 \access=Public,cfields=[] schirmer@12854: ,methods=Object_mdecls haftmann@28524: ,init=Skip,super=undefined,superIfs=[]\" 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 \access=Public,cfields=[],methods=SXcpt_mdecls, schirmer@12854: init=Skip, schirmer@12854: super=if xn = Throwable then Object else SXcpt Throwable, schirmer@12854: superIfs=[]\" 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 == \ifaces=Ifaces,classes=Classes\" schirmer@12854: schirmer@12854: constdefs schirmer@12854: test :: "(ty)list \ stmt" schirmer@12854: "test pTs \ e:==NewC Ext;; schirmer@12925: \ Try Expr({Main,ClassT Base,IntVir}!!e\foo({pTs}[Lit Null])) schirmer@12854: \ Catch((SXcpt NullPointer) z) schirmer@12925: (lab1\ 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) \ (subcls1 tprg)^+ \ 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) \ (subcls1 tprg)^+ \ 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) \ (subcls1 tprg)^+ \ 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) \ (subcls1 tprg)^+ \ 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: "(\pid=java_lang,tid=TName tn\, \pid=java_lang,tid=TName tn\) schirmer@12854: \ (subcls1 tprg)^+ \ 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 \ (\(I,i)\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 \ (\(C,c)\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\SXcpt xn\\<^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\Ext \\<^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\Ext \\<^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), \access=Public,static=True ,type=PrimT Boolean.[]\), schirmer@12854: ((vee,Base), \access=Public,static=False,type=Iface HasFoo \)]" 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), \access=Public,static=False,type= PrimT Integer\)] 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 \ empty(foo_sig\(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 [(\(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\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: "\ tprg\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\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: "\ tprg\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: "\ tprg \ 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 (\sig m. tprg \ Ext inherits method sig m) schirmer@12854: (empty(fst ((\(s, m). (s, Base, m)) Base_foo)\ schirmer@12854: snd ((\(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 [(\(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: "\class tprg C = Some c; C\Object\ \ \ 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\(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\(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\(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 ((\(s, m). (s, a, m)) x) = (a,snd x)" schirmer@12854: by (cases x) (auto) schirmer@12854: schirmer@12854: lemma fst_special_simp: "fst ((\(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\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\ mdecl (sig, snd Base_foo) declared_in Base \ 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\(Base,(snd Base_foo)) overrides old \ 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\(Base,(snd Base_foo)) overrides\<^sub>S old \ 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\(Base,(snd Base_foo)) hides old \ 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\(Ext,(snd Ext_foo)) hides old \ 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\ mdecl (sig, snd Ext_foo) declared_in Ext \ 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\(Ext,(snd Ext_foo)) overrides old schirmer@12854: \ 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\(Ext,(snd Ext_foo)) overrides\<^sub>S old schirmer@12854: \ 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\(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\(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\(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\(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 \ (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\(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\(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 \ (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\(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\(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\(Ext,Ext_foo) overrides (Base,Base_foo)" schirmer@12854: proof (rule overridesR.Direct, simp_all) schirmer@12854: show "\ is_static Ext_foo" schirmer@12854: by (simp add: member_is_static_simp Ext_foo_def) schirmer@12854: show "\ is_static Base_foo" schirmer@12854: by (simp add: member_is_static_simp Base_foo_def) schirmer@12854: show "accmodi Ext_foo \ 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\mdecl Ext_foo declared_in Ext" schirmer@12854: by (auto intro: Ext_declares_foo) schirmer@12854: show "tprg\mdecl Base_foo declared_in Base" schirmer@12854: by (auto intro: Base_declares_foo) schirmer@12854: show "tprg \(Base, mdecl Base_foo) inheritable_in java_lang" schirmer@12854: by (simp add: inheritable_in_def Base_foo_def) schirmer@12854: show "tprg\resTy Ext_foo\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 \name = foo, parTs = [Class Base]\ schirmer@12854: = Some (Ext,snd Ext_foo)" schirmer@12854: proof - schirmer@12854: have "methd tprg Base \name = foo, parTs = [Class Base]\ schirmer@12854: = Some (Base,snd Base_foo)" and schirmer@12854: "methd tprg Ext \name = foo, parTs = [Class Base]\ 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 (\((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\(Base, fdecl (arr, schirmer@12854: \access = Public, static = True, type = PrimT Boolean.[]\)) 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\(Base, fdecl (arr, schirmer@12925: \access = Public, static = True, type = PrimT Boolean.[]\)) 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\(Base, fdecl (arr, schirmer@12854: \access = Public, static = True, type = PrimT Boolean.[]\)) 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\(Base, fdecl (arr, schirmer@12925: \access = Public, static = True, type = PrimT Boolean.[]\)) 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 (\((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\(Base, fdecl (arr, \access=Public,static=True ,type=PrimT Boolean.[]\)) 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\(Base, fdecl (arr, \access=Public,static=True ,type=PrimT Boolean.[]\)) 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 \ 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 \ 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) \name=foo, parTs=[NT]\ = schirmer@12854: {((ClassT Base, \access=Public,static=False,pars=[z],resT=Class Base\) schirmer@12854: ,[Class Base])}" schirmer@12854: apply (unfold appl_methds_def) schirmer@12854: apply (simp (no_asm)) schirmer@12854: apply (subgoal_tac "tprg\NT\ 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) \name=foo,parTs=[NT]\ = schirmer@12854: {((ClassT Base, \access=Public,static=False,pars=[z],resT=Class Base\) schirmer@12854: , [Class Base])}" nipkow@31197: by (simp add: max_spec_def appl_methds_Base_foo Collect_conv_if) schirmer@12854: schirmer@12854: section "well-typedness" schirmer@12854: schirmer@12925: lemma wt_test: "\prg=tprg,cls=Main,lcl=empty(VName e\Class Base)\\test ?pTs\\" 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: "\prg=tprg,cls=Main,lcl=empty(VName e\Class Base)\ schirmer@13688: \{} \\test ?pTs\\ \nrm={VName e},brk=\ l. UNIV\" 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 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: "\a obj. \the (new_Addr h) = a; atleast_free h (Suc n)\ \ schirmer@12854: new_Addr h = Some a \ atleast_free (h(a\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" <= "\tag=Arr (PrimT Boolean) (CONST two) wenzelm@20769: ,values=CONST empty(Inr 0\Bool False)(Inr (CONST one)\Bool False)\" wenzelm@20769: "obj_b" <= "\tag=CInst (CONST Ext) wenzelm@20769: ,values=(CONST empty(Inl (CONST vee, CONST Base)\Null ) wenzelm@20769: (Inl (CONST vee, CONST Ext )\Intg 0))\" wenzelm@20769: "obj_c" == "\tag=CInst (SXcpt NullPointer),values=CONST empty\" wenzelm@20769: "arr_N" == "CONST empty(Inl (CONST arr, CONST Base)\Null)" wenzelm@20769: "arr_a" == "CONST empty(Inl (CONST arr, CONST Base)\Addr a)" haftmann@28524: "globs1" == "CONST empty(Inr (CONST Ext) \\tag=CONST undefined, values=CONST empty\) haftmann@28524: (Inr (CONST Base) \\tag=CONST undefined, values=arr_N\) haftmann@28524: (Inr Object\\tag=CONST undefined, values=CONST empty\)" haftmann@28524: "globs2" == "CONST empty(Inr (CONST Ext) \\tag=CONST undefined, values=CONST empty\) haftmann@28524: (Inr Object\\tag=CONST undefined, values=CONST empty\) wenzelm@20769: (Inl a\obj_a) haftmann@28524: (Inr (CONST Base) \\tag=CONST undefined, values=arr_a\)" schirmer@12854: "globs3" == "globs2(Inl b\obj_b)" schirmer@12854: "globs8" == "globs3(Inl c\obj_c)" wenzelm@20769: "locs3" == "CONST empty(VName (CONST e)\Addr b)" wenzelm@20769: "locs4" == "CONST empty(VName (CONST z)\Null)(Inr()\Addr b)" wenzelm@20769: "locs8" == "locs3(VName (CONST z)\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: "\the (new_Addr (heap s1)) = a; schirmer@12854: the (new_Addr (heap ?s2)) = b; schirmer@12854: the (new_Addr (heap ?s3)) = c\ \ schirmer@12854: atleast_free (heap s0) four \ schirmer@12854: tprg\s0' \test [Class Base]\ ?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\(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