src/HOL/MicroJava/Comp/CorrCompTp.thy

 done
 
 
 
 (********************************************************************************)
-section "index"
+subsection "index"
 
 lemma local_env_snd: "
   snd (local_env G C (mn, pTs) pns lvars) = map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)"
 by (simp add: local_env_def)
 

 done
 
 
 (********************************************************************************)
 
-section "Preservation of ST and LT by compTpExpr / compTpStmt"
+subsection "Preservation of ST and LT by compTpExpr / compTpStmt"
 
 lemma sttp_of_comb_nil [simp]: "sttp_of (comb_nil sttp) = sttp"
 by (simp add: comb_nil_def)
 
 lemma mt_of_comb_nil [simp]: "mt_of (comb_nil sttp) = []"

 
 
 
 
   (* ********************************************************************** *)
-section "length of compExpr/ compTpExprs"
+subsection "length of compExpr/ compTpExprs"
   (* ********************************************************************** *)
 
 lemma length_comb [simp]:  "length (mt_of ((f1 \<box> f2) sttp)) = 
   length (mt_of (f1 sttp)) + length (mt_of (f2 (sttp_of (f1 sttp))))"
 by (simp add: comb_def split_beta)

   "\<forall> sttp. length (mt_of (compTpInitLvars jmb lvars sttp)) = length (compInitLvars jmb lvars)"
 by (induct lvars,  (simp add: compInitLvars_def length_compTpInit split_beta)+)
 
 
   (* ********************************************************************** *)
-section "Correspondence bytecode - method types"
+subsection "Correspondence bytecode - method types"
   (* ********************************************************************** *)
 
 abbreviation (input)
   ST_of :: "state_type \<Rightarrow> opstack_type"
   where "ST_of == fst"

 by (auto simp: comp_def compClass_def)
 
 
   (* ---------------------------------------------------------------------- *)
 
-section "Main Theorem"
+subsection "Main Theorem"
   (* MAIN THEOREM: 
   Methodtype computed by comp is correct for bytecode generated by compTp *)
 theorem wt_prog_comp: "wf_java_prog G  \<Longrightarrow> wt_jvm_prog (comp G) (compTp G)"
 apply (simp add: wf_prog_def)