wfenv.art
notation syntax rels ; import syntax wf wfenv ;// Reflexivity results for widening relations. //
thm simpty_widens_to-refl TE |- st1 simpty_widens_to st1 qed by structural cases on st1; thm varty_widens_to-refl TE |- vt1 varty_widens_to vt1 qed by simpty_widens_to-refl; thm expty_widens_to-refl TE |- et1 expty_widens_to et1 qed by structural cases on et1,EXPTY_WIDENS__elim,varty_widens_to-refl;
// Transitivity results for widening relations.
thm Object-implements if TE wf_tyenv then ~(TE |- Object implements i); consider methods st Cdec(TE,Object) = SOME(CLASS(NONE,EMPTY,PEMPTY,methods)) [rw,auto] by WF_TYENV__Object_declared [TE]; qed by IMPLEMENTS__elim,agro-grind; thm Object-subclass if TE wf_tyenv then TE |- Object subclass_of C <=> C = Object g; consider methods st Cdec(TE,Object) = SOME(CLASS(NONE,EMPTY,PEMPTY,methods)) [rw,auto] by WF_TYENV__Object_declared [TE]; per cases case + TE |- Object subclass_of C a - C = Object; then qed by rule cases on a; end by IFF,g; // <-- got by auto rule thm Object-simpty if TE wf_tyenv then TE |- Class(Object) simpty_widens_to st <=> st = Class(Object) g; per cases case + TE |- Class(Object) simpty_widens_to st a - st = Class(Object); then qed by rule cases on a, Object-subclass [TE], Object-implements [TE]; end by IFF,g,PEXISTS_SPLIT; // <-- got by auto rule //thm subclass-Object // if TE wf_tyenv // TE |- C reachable_class a // then TE |- C subclass_of Object; // proceed by rule induction on a with C variable; // case Base; qed by WF_TYENV__only_Object_has_no_superclass [TE,C]; // case Step; qed by subclass_of__Step [TE]; // end; thm simpty_widens_to-trans if TE wf_tyenv TE |- st0 simpty_widens_to st1 a1 TE |- st1 simpty_widens_to st2 a2 then TE |- st0 simpty_widens_to st2 then qed by rule cases on a1,rule cases on a2, subclass-trans [TE],subinterface-trans [TE],wellfounded_interface-trans [TE], Object-subclass [TE],Object-simpty [TE], Object-implements [TE]; thm varty_widens_to-trans if TE wf_tyenv TE |- C0 varty_widens_to C1 TE |- C1 varty_widens_to C2 then TE |- C0 varty_widens_to C2 qed by VARTY_WIDENS__elim,simpty_widens_to-trans [TE],Object-simpty [TE],PEXISTS_SPLIT; thm expty_widens_to-trans if TE wf_tyenv TE |- C0 expty_widens_to C1 TE |- C1 expty_widens_to C2 then TE |- C0 expty_widens_to C2 qed by EXPTY_WIDENS__elim,varty_widens_to-trans [TE],PEXISTS_SPLIT;
// Decomposition results for widening
thm array-widens-lemma TE |- expty expty_widens_to SOME(VT(simpty0,dim)) & 0 < dim --> ?simpty1. expty = SOME(VT(simpty1,dim)) & TE |- simpty1 simpty_widens_to simpty0 qed by EXPTY_WIDENS__elim,VARTY_WIDENS__elim thm prim-widens-lemma TE |- expty expty_widens_to SOME(VT(PrimT(primty),0)) <=> expty = SOME(VT(PrimT(primty),0)); qed by IFF,EXPTY_WIDENS__elim,VARTY_WIDENS__elim,SIMPTY_WIDENS__elim,PEXISTS_SPLIT thm var-prim-widens-lemma TE |- varty varty_widens_to VT(PrimT(primty),0) --> varty = VT(PrimT(primty),0) qed by VARTY_WIDENS__elim,SIMPTY_WIDENS__elim thm class-widens-lemma TE wf_tyenv & TE |- expty expty_widens_to SOME(VT(Class(C),0)) & C <> Object --> ?C'. TE |- C' subclass_of C & expty = SOME(VT(Class(C'),0)) qed by EXPTY_WIDENS__elim,VARTY_WIDENS__elim,SIMPTY_WIDENS__elim;
// widening preserves field visibility
thm inherited-fields-exist if TE wf_tyenv TE_wF TE |- C1 subclass_of C0 C1_subclass ((C',f),var0_ty) :: FDecs(TE,C0) search then ((C',f),var0_ty) :: FDecs(TE,C1) proceed by rule induction on C1_subclass with C1 variable; case Refl; qed by search; case Step; qed by FDecs__Super,search,IN_ELIM; end;
// widening preserves method visibility up to narrowing of return type.
thm class-inherited-class-methods-are-narrower if TE wf_tyenv TE_wf TE |- C1 subclass_of C0 C1_subclass MSigsC(TE,C0)(m,MT(AT,rt0)) search then ?rt1. MSigsC(TE,C1)(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0 g proceed by rule induction on C1_subclass with C1 variable; case Refl; qed by expty_widens_to-refl,search; case Step Cdec(TE,C1) = SOME(CLASS(SOME(Ca),Is,fields,methods)) [rw,auto] ?rt1. MSigsC(TE,Ca)(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0 ihyp TE |- Ca subclass_of C0; consider rt1 st MSigsC(TE,Ca)(m,MT(AT,rt1)) ma TE |- rt1 expty_widens_to rt0 miss_narrower by ihyp; then qed by WF_TYENV__class_return_types_wider [TE,methods,fields,Is,C1/C], TE_wf,PDOM,IN_ELIM,Cdec,expty_widens_to-trans [TE],TE_wf,PEXISTS_SPLIT; end;
//
thm interface-inherited-interface-methods-are-narrower if TE wf_tyenv TE_wf TE |- i1 subinterface_of i0 i1_subclass MSigsI(TE,i0)(m,MT(AT,rt0)) search then ?rt1. MSigsI(TE,i1)(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0 g proceed by rule induction on i1_subclass with i1 variable; case Refl; qed by expty_widens_to-refl,search; case Step Idec(TE,i1) = SOME(INTERFACE(Is,methods)) [rw,auto] ia :: Is ?rt1. MSigsI(TE,ia)(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0 ihyp TE |- ia subinterface_of i0; consider rt1 st MSigsI(TE,ia)(m,MT(AT,rt1)) ma TE |- rt1 expty_widens_to rt0 miss_narrower by ihyp; then qed by WF_TYENV__interface_return_types_wider [TE,methods,Is,i1/i,ia/i',AT], expty_widens_to-trans [TE], TE_wf,PDOM,IN_ELIM,Idec,ma,PEXISTS_SPLIT; end;
//
thm class-inherited-interface-methods-are-narrower if TE wf_tyenv TE_wf TE |- C implements i imp MSigsI(TE,i)(m,MT(AT,rt0)) search then ?rt1. MSigsC(TE,C)(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0 g consider Csupo,Is,fields,methods st Cdec(TE,C) = SOME(CLASS(Csupo,Is,fields,methods)) [rw,auto] i :: Is by IMPLEMENTS__elim,imp; qed by WF_TYENV__interfaces_implemented [TE,C/C],search,TE_wf,PDOM,Cdec,IN_ELIM,PEXISTS_SPLIT;
// The base case (where interfaces support all methods in the Object class) // needs careful attention. An ommission was discovered in the language // spec and rule for well-formed environments with respect to this.
thm interface-inherited-Object-methods-are-narrower if TE wf_tyenv TE_wf TE |- i wellfounded_interface i_reachable MSigsC(TE,Object)(m,MT(AT,rt0)) base then ?rt1. MSigsI(TE,i)(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0 g proceed by rule induction on i_reachable with i variable; // the cases are: // - the method occurs in the methods of the new interface (easy) // - the method doesn't occur, and there are no superinterfaces (easy by WF) // - the method doesn't occur in the new methods but does in // some superinterface, and by wf. some most narrow interfaces // exists amongst the superinterfaces. case Base Idec(TE,i) = SOME(INTERFACE(EMPTY,methods)) [rw,auto]; per cases case (m,MT(AT,rt')) :: methods hit; have TE |- rt' expty_widens_to rt0 by WF_TYENV__interface_return_types_wider_than_Object [TE,methods,i/i], TE_wf,PDOM,IN_ELIM,Idec,base,hit,PEXISTS_SPLIT; then qed by MSigsI__Hit,g [rt'],hit; case !AT' rt'. (m,MT(AT',rt')) :: methods --> AT' <> AT; then qed by MSigsI__Miss [methods,TE,m/m,i/i,AT], base,g [rt0],expty_widens_to-refl,Args; end by hard IN_ELIM,EMPTY_ELIM,FUN_EQ; // soeme sort of bug with EMPTY_ELIM case Step Idec(TE,i) = SOME(INTERFACE(Is,methods)) [rw,auto] i' :: Is witness ?rt1. MSigsI(TE,i')(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0 ihyp TE |- i' wellfounded_interface; qed by expty_widens_to-trans [TE], WF_TYENV__interface_return_types_wider [TE,methods,Is,i/i,i'/i'],Idec, witness,ihyp,TE_wf,PDOM,IN_ELIM,PEXISTS_SPLIT; end;
//
thm array-inherited-Object-methods-are-identical MSigsC(TE,Object)(m,MT(AT,rt)) --> MSigsA(TE)(m,MT(AT,rt)) qed by MSigsA__elim,PEXISTS_SPLIT;
// put it all together!!
thm inherited-methods-exist if TE wf_tyenv TE_wf MSigs(TE,VT(st0,dim0))(m,MT(AT,rt0)) search TE |- vt1 varty_widens_to VT(st0,dim0) rel then ?rt1. MSigs(TE,vt1)(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0 g qed by VARTY_WIDENS__elim,SIMPTY_WIDENS__elim,rel,g,TE_wf,search,ZERO_CASES [dim0], MSigs, expty_widens_to-trans [TE], array-inherited-Object-methods-are-identical [TE,rt0,AT], interface-inherited-Object-methods-are-narrower [TE,rt0,AT], class-inherited-interface-methods-are-narrower [TE,rt0,AT], interface-inherited-interface-methods-are-narrower [TE,rt0,AT], class-inherited-class-methods-are-narrower [TE,rt0,AT];
// This is an interesting little proof - it shows that for a well // formed environment FDecs does not find more than one field type // for a given field/class pair.
thm FDecs-finds-subclasses if FDecs(TE,C)((Cf,f),vt) deriv then TE |- C subclass_of Cf; proceed by rule induction on deriv with C variable; case Hit; qed; case Super; qed by subclass_of__Step; end; thm object-fields-unique if TE wf_tyenv FDecs(TE,C)((Cf,f),vt1) deriv1 FDecs(TE,C)((Cf,f),vt2) deriv2 then vt1 = vt2; have TE |- C subclass_of Cf C_subclass by FDecs-finds-subclasses,deriv1; proceed by rule induction on C_subclass with C variable; case Refl Cf = C ; consider methods1,Is1,fields1,Csup st Cdec(TE,C) = SOME(CLASS(Csup,Is1,fields1,methods1)) [rw,auto] fields1 f = SOME(vt1) [rw,auto] by rule cases on deriv1, FDecs-finds-subclasses [TE,C/Cf,f/f,vt1], WF_TYENV__no_circular_classes [TE,C/C],PDOM,IN_ELIM,Cdec; qed by rule cases on deriv2, FDecs-finds-subclasses [TE,C/Cf,f/f,vt2], WF_TYENV__no_circular_classes [TE,C/C,Is1,fields1,methods1], PDOM,IN_ELIM,Cdec,PEXISTS_SPLIT; case Step Cdec(TE,C) = SOME(CLASS(SOME(C1'),Is1,fields1,methods1)) [rw,auto] FDecs(TE,C1')((Cf,f),vt1) & FDecs(TE,C1')((Cf,f),vt2) --> vt1 = vt2 ihyp TE |- C1' subclass_of Cf s2; qed by rule cases on deriv1,rule cases on deriv2,ihyp,s2,PFORALL_SPLIT, FDecs-finds-subclasses [TE,C/Cf,C1'/C,f/f,vt1], FDecs-finds-subclasses [TE,C/Cf,C1'/C,f/f,vt2], WF_TYENV__no_circular_classes [TE,C/C,Is1,fields1,methods1], PDOM,IN_ELIM,Cdec; end;
// And thus the graph found by FDecs form a partial function.
thm object-fields-form-graph TE wf_tyenv --> IS_GRAPH {fspec | FDecs(TE,C)(fspec)}; qed by object-fields-unique [TE], IS_GRAPH_ELIM,GSPEC_ELIM,VT_11,VT_splits,PFORALL_SPLIT;
