Theory WellForm

Up to index of Isabelle/HOL/MicroJava

(*  Title:      HOL/MicroJava/J/WellForm.thy
    ID:         $Id: WellForm.thy,v 1.7 2000/09/25 10:08:52 kleing Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen

Well-formedness of Java programs
for static checks on expressions and statements, see WellType.thy

improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
* a method implementing or overwriting another method may have a result type 
  that widens to the result type of the other method (instead of identical type)

simplifications:
* for uniformity, Object is assumed to be declared like any other class
*)

WellForm = TypeRel +

types 'c wf_mb = 'c prog => cname => 'c mdecl => bool

constdefs
 wf_fdecl :: "'c prog => fdecl => bool"
"wf_fdecl G == \<lambda>(fn,ft). is_type G ft"

 wf_mhead :: "'c prog => sig => ty => bool"
"wf_mhead G == \<lambda>(mn,pTs) rT. (\<forall>T\<in>set pTs. is_type G T) \<and> is_type G rT"

 wf_mdecl :: "'c wf_mb => 'c wf_mb"
"wf_mdecl wf_mb G C == \<lambda>(sig,rT,mb). wf_mhead G sig rT \<and> wf_mb G C (sig,rT,mb)"

 wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
"wf_cdecl wf_mb G ==
   \<lambda>(C,(sc,fs,ms)).
  (\<forall>f\<in>set fs. wf_fdecl G   f    ) \<and>  unique fs \<and>
  (\<forall>m\<in>set ms. wf_mdecl wf_mb G C m) \<and>  unique ms \<and>
  (case sc of None => C = Object
         | Some D =>
             is_class G D \<and>  ¬  G\<turnstile>D\<preceq>C C \<and>
             (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'.
                 method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))"

 wf_prog :: "'c wf_mb => 'c prog => bool"
"wf_prog wf_mb G ==
   let cs = set G in ObjectC \<in> cs \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G"

end

theorem subcls1_wfD:

  [| G |- C <=C1 D; wf_prog wf_mb G |] ==> D ~= C & (D, C) ~: (subcls1 G)^+

theorem subcls_asym:

  [| wf_prog wf_mb G; (C, D) : (subcls1 G)^+ |] ==> (D, C) ~: (subcls1 G)^+

theorem subcls_induct:

  [| wf_prog wf_mb G; !!C. ALL D. (C, D) : (subcls1 G)^+ --> P D ==> P C |]
  ==> P C

theorem subcls1_induct:

  [| is_class G C; wf_prog wf_mb G; P Object;
     !!C D fs ms.
        [| C ~= Object; is_class G C;
           class G C = Some (Some D, fs, ms) &
           wf_cdecl wf_mb G (C, Some D, fs, ms) &
           G |- C <=C1 D & is_class G D & P D |]
        ==> P C |]
  ==> P C

theorem method_rec_lemma:

  [| wf ((subcls1 G)^-1);
     ALL D fs ms. class G C = Some (Some D, fs, ms) --> is_class G D |]
  ==> method (G, C) =
      (case class G C of None => empty
       | Some (sc, fs, ms) =>
           (case sc of None => empty | Some D => method (G, D)) ++
           map_of (map (%(s, m). (s, C, m)) ms))

theorem method_rec:

  wf_prog wf_mb G
  ==> method (G, C) =
      (case class G C of None => empty
       | Some (sc, fs, ms) =>
           (case sc of None => empty | Some D => method (G, D)) ++
           map_of (map (%(s, m). (s, C, m)) ms))

theorem fields_rec_lemma:

  [| wf ((subcls1 G)^-1); class G C = Some (sc, fs, ms);
     ALL C. sc = Some C --> is_class G C |]
  ==> fields (G, C) =
      map (split (%fn. Pair (fn, C))) fs @
      (case sc of None => [] | Some D => fields (G, D))

theorem fields_rec:

  [| class G C = Some (sc, fs, ms); wf_prog wf_mb G |]
  ==> fields (G, C) =
      map (split (%fn. Pair (fn, C))) fs @
      (case sc of None => [] | Some D => fields (G, D))

theorem subcls_C_Object:

  [| is_class G C; wf_prog wf_mb G |] ==> G |- C <=C Object

theorem fields_mono:

  [| (C', C) : (subcls1 G)^+; wf_prog wf_mb G; x : set (fields (G, C)) |]
  ==> x : set (fields (G, C'))

theorem widen_fields_defpl':

  [| is_class G C; wf_prog wf_mb G |]
  ==> ALL ((fn, fd), fT):set (fields (G, C)). G |- C <=C fd

theorem widen_fields_defpl:

  [| is_class G C; wf_prog wf_mb G; ((fn, fd), fT) : set (fields (G, C)) |]
  ==> G |- C <=C fd

theorem unique_fields:

  [| is_class G C; wf_prog wf_mb G |] ==> unique (fields (G, C))

theorem widen_fields_mono:

  [| wf_prog wf_mb G; G |- C' <=C C; map_of (fields (G, C)) f = Some ft |]
  ==> map_of (fields (G, C')) f = Some ft

theorem widen_cfs_fields:

  [| field (G, C) fn = Some (fd, fT); G |- C' <=C C; wf_prog wf_mb G |]
  ==> map_of (fields (G, C')) (fn, fd) = Some fT

theorem method_wf_mdecl:

  [| wf_prog wf_mb G; method (G, C) sig = Some (md, mh, m) |]
  ==> G |- C <=C md & wf_mdecl wf_mb G md (sig, mh, m)

theorem subcls_widen_methd:

  [| G |- T <=C T'; wf_prog wf_mb G; method (G, T') sig = Some (D, rT, b) |]
  ==> EX D' rT' b'. method (G, T) sig = Some (D', rT', b') & G |- rT' <= rT

theorem subtype_widen_methd:

  [| G |- C <=C D; wf_prog wf_mb G; method (G, D) sig = Some (md, rT, b) |]
  ==> EX mD' rT' b'. method (G, C) sig = Some (mD', rT', b') & G |- rT' <= rT

theorem method_in_md:

  [| wf_prog wf_mb G; method (G, C) sig = Some (D, mh, code) |]
  ==> is_class G D & method (G, D) sig = Some (D, mh, code)

theorem is_type_fields:

  [| is_class G C; wf_prog wf_mb G; x : set (fields (G, C)) |]
  ==> is_type G (snd x)