src/HOL/Bali/WellType.thy

 (*  Title:      HOL/Bali/WellType.thy
     Author:     David von Oheimb
 *)
-header {* Well-typedness of Java programs *}
+subsection {* Well-typedness of Java programs *}
 
 theory WellType
 imports DeclConcepts
 begin
 

 
 abbreviation
   pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
   where "pkg e == pid (cls e)"
 
-section "Static overloading: maximally specific methods "
+subsubsection "Static overloading: maximally specific methods "
 
 type_synonym
   emhead = "ref_ty \<times> mhead"
 
 --{* Some mnemotic selectors for emhead *}

 lemma Null_staticD: 
   "a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
 apply (clarsimp simp add: invmode_IntVir_eq)
 done
 
-section "Typing for unary operations"
+subsubsection "Typing for unary operations"
 
 primrec unop_type :: "unop \<Rightarrow> prim_ty"
 where
   "unop_type UPlus   = Integer"
 | "unop_type UMinus  = Integer"

   "wt_unop UPlus   t = (t = PrimT Integer)"
 | "wt_unop UMinus  t = (t = PrimT Integer)"
 | "wt_unop UBitNot t = (t = PrimT Integer)"
 | "wt_unop UNot    t = (t = PrimT Boolean)"
 
-section "Typing for binary operations"
+subsubsection "Typing for binary operations"
 
 primrec binop_type :: "binop \<Rightarrow> prim_ty"
 where
   "binop_type Mul      = Integer"     
 | "binop_type Div      = Integer"

 | "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
 | "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
 | "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
 | "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
 
-section "Typing for terms"
+subsubsection "Typing for terms"
 
 type_synonym tys  = "ty + ty list"
 translations
   (type) "tys" <= (type) "ty + ty list"