src/HOL/MicroJava/J/WellForm.thy
changeset 10042 7164dc0d24d8
parent 8106 de9fae0cdfde
child 10061 fe82134773dc
equal deleted inserted replaced
10041:30693ebd16ae 10042:7164dc0d24d8
    18 
    18 
    19 types 'c wf_mb = 'c prog => cname => 'c mdecl => bool
    19 types 'c wf_mb = 'c prog => cname => 'c mdecl => bool
    20 
    20 
    21 constdefs
    21 constdefs
    22 
    22 
    23  wf_fdecl	:: "'c prog \\<Rightarrow>          fdecl \\<Rightarrow> bool"
    23  wf_fdecl	:: "'c prog =>          fdecl => bool"
    24 "wf_fdecl G \\<equiv> \\<lambda>(fn,ft). is_type G ft"
    24 "wf_fdecl G == \\<lambda>(fn,ft). is_type G ft"
    25 
    25 
    26  wf_mhead	:: "'c prog \\<Rightarrow> sig   \\<Rightarrow> ty \\<Rightarrow> bool"
    26  wf_mhead	:: "'c prog => sig   => ty => bool"
    27 "wf_mhead G \\<equiv> \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
    27 "wf_mhead G == \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
    28 
    28 
    29  wf_mdecl	:: "'c wf_mb \\<Rightarrow> 'c wf_mb"
    29  wf_mdecl	:: "'c wf_mb => 'c wf_mb"
    30 "wf_mdecl wf_mb G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
    30 "wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
    31 
    31 
    32   wf_cdecl	:: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
    32   wf_cdecl	:: "'c wf_mb => 'c prog => 'c cdecl => bool"
    33 "wf_cdecl wf_mb G \\<equiv>
    33 "wf_cdecl wf_mb G ==
    34    \\<lambda>(C,(sc,fs,ms)).
    34    \\<lambda>(C,(sc,fs,ms)).
    35 	(\\<forall>f\\<in>set fs. wf_fdecl G   f    ) \\<and>  unique fs \\<and>
    35 	(\\<forall>f\\<in>set fs. wf_fdecl G   f    ) \\<and>  unique fs \\<and>
    36 	(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and>  unique ms \\<and>
    36 	(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and>  unique ms \\<and>
    37 	(case sc of None \\<Rightarrow> C = Object
    37 	(case sc of None => C = Object
    38          | Some D \\<Rightarrow>
    38          | Some D =>
    39              is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<preceq>C C \\<and>
    39              is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<preceq>C C \\<and>
    40              (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
    40              (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
    41                  method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
    41                  method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
    42 
    42 
    43  wf_prog	:: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> bool"
    43  wf_prog	:: "'c wf_mb => 'c prog => bool"
    44 "wf_prog wf_mb G \\<equiv>
    44 "wf_prog wf_mb G ==
    45    let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
    45    let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
    46 
    46 
    47 end
    47 end