src/HOL/MicroJava/J/TypeRel.thy

     Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
 header {* \isaheader{Relations between Java Types} *}
 
-theory TypeRel imports Decl "~~/src/HOL/Library/Wfrec" begin
+theory TypeRel
+imports Decl "~~/src/HOL/Library/Wfrec"
+begin
 
 -- "direct subclass, cf. 8.1.3"
 
 inductive_set
   subcls1 :: "'c prog => (cname \<times> cname) set"

 
 code_pred 
   (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
   subcls1p 
   .
-declare subcls1_def[unfolded Collect_def, code_pred_def]
+
+declare subcls1_def [code_pred_def]
+
 code_pred 
   (modes: i \<Rightarrow> i \<times> o \<Rightarrow> bool, i \<Rightarrow> i \<times> i \<Rightarrow> bool)
   [inductify]
   subcls1 
   .
 
 definition subcls' where "subcls' G = (subcls1p G)^**"
+
 code_pred
   (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
   [inductify]
   subcls'
-.
+  .
+
 lemma subcls_conv_subcls' [code_unfold]:
-  "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)"
-by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def)
+  "(subcls1 G)^* = {(C, D). subcls' G C D}"
+by(simp add: subcls'_def subcls1_def rtrancl_def)
 
 lemma class_rec_code [code]:
   "class_rec G C t f = 
   (if wf_class G then 
     (case class G C of

 lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
   method (G,C) = (if C = Object then empty else method (G,D)) ++  
   map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
 apply (unfold method_def)
 apply (simp split del: split_if)
-apply (erule (1) class_rec_lemma [THEN trans]);
+apply (erule (1) class_rec_lemma [THEN trans])
 apply auto
 done
 
 
 -- "list of fields of a class, including inherited and hidden ones"

 lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
  fields (G,C) = 
   map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
 apply (unfold fields_def)
 apply (simp split del: split_if)
-apply (erule (1) class_rec_lemma [THEN trans]);
+apply (erule (1) class_rec_lemma [THEN trans])
 apply auto
 done
 
 
 defs field_def [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"