src/HOL/MicroJava/J/WellForm.thy
changeset 10042 7164dc0d24d8
parent 8106 de9fae0cdfde
child 10061 fe82134773dc
     1.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -20,28 +20,28 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 - wf_fdecl	:: "'c prog \\<Rightarrow>          fdecl \\<Rightarrow> bool"
     1.8 -"wf_fdecl G \\<equiv> \\<lambda>(fn,ft). is_type G ft"
     1.9 + wf_fdecl	:: "'c prog =>          fdecl => bool"
    1.10 +"wf_fdecl G == \\<lambda>(fn,ft). is_type G ft"
    1.11  
    1.12 - wf_mhead	:: "'c prog \\<Rightarrow> sig   \\<Rightarrow> ty \\<Rightarrow> bool"
    1.13 -"wf_mhead G \\<equiv> \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
    1.14 + wf_mhead	:: "'c prog => sig   => ty => bool"
    1.15 +"wf_mhead G == \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
    1.16  
    1.17 - wf_mdecl	:: "'c wf_mb \\<Rightarrow> 'c wf_mb"
    1.18 -"wf_mdecl wf_mb G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
    1.19 + wf_mdecl	:: "'c wf_mb => 'c wf_mb"
    1.20 +"wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
    1.21  
    1.22 -  wf_cdecl	:: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
    1.23 -"wf_cdecl wf_mb G \\<equiv>
    1.24 +  wf_cdecl	:: "'c wf_mb => 'c prog => 'c cdecl => bool"
    1.25 +"wf_cdecl wf_mb G ==
    1.26     \\<lambda>(C,(sc,fs,ms)).
    1.27  	(\\<forall>f\\<in>set fs. wf_fdecl G   f    ) \\<and>  unique fs \\<and>
    1.28  	(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and>  unique ms \\<and>
    1.29 -	(case sc of None \\<Rightarrow> C = Object
    1.30 -         | Some D \\<Rightarrow>
    1.31 +	(case sc of None => C = Object
    1.32 +         | Some D =>
    1.33               is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<preceq>C C \\<and>
    1.34               (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
    1.35 -                 method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
    1.36 +                 method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
    1.37  
    1.38 - wf_prog	:: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> bool"
    1.39 -"wf_prog wf_mb G \\<equiv>
    1.40 + wf_prog	:: "'c wf_mb => 'c prog => bool"
    1.41 +"wf_prog wf_mb G ==
    1.42     let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
    1.43  
    1.44  end