src/HOL/MicroJava/J/TypeRel.thy
changeset 45970 b6d0cff57d96
parent 45231 d85a2fdc586c
child 53374 a14d2a854c02
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Sat Dec 24 15:53:10 2011 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Sat Dec 24 15:53:10 2011 +0100
     1.3 @@ -4,7 +4,9 @@
     1.4  
     1.5  header {* \isaheader{Relations between Java Types} *}
     1.6  
     1.7 -theory TypeRel imports Decl "~~/src/HOL/Library/Wfrec" begin
     1.8 +theory TypeRel
     1.9 +imports Decl "~~/src/HOL/Library/Wfrec"
    1.10 +begin
    1.11  
    1.12  -- "direct subclass, cf. 8.1.3"
    1.13  
    1.14 @@ -84,7 +86,9 @@
    1.15    (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
    1.16    subcls1p 
    1.17    .
    1.18 -declare subcls1_def[unfolded Collect_def, code_pred_def]
    1.19 +
    1.20 +declare subcls1_def [code_pred_def]
    1.21 +
    1.22  code_pred 
    1.23    (modes: i \<Rightarrow> i \<times> o \<Rightarrow> bool, i \<Rightarrow> i \<times> i \<Rightarrow> bool)
    1.24    [inductify]
    1.25 @@ -92,14 +96,16 @@
    1.26    .
    1.27  
    1.28  definition subcls' where "subcls' G = (subcls1p G)^**"
    1.29 +
    1.30  code_pred
    1.31    (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
    1.32    [inductify]
    1.33    subcls'
    1.34 -.
    1.35 +  .
    1.36 +
    1.37  lemma subcls_conv_subcls' [code_unfold]:
    1.38 -  "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)"
    1.39 -by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def)
    1.40 +  "(subcls1 G)^* = {(C, D). subcls' G C D}"
    1.41 +by(simp add: subcls'_def subcls1_def rtrancl_def)
    1.42  
    1.43  lemma class_rec_code [code]:
    1.44    "class_rec G C t f = 
    1.45 @@ -190,7 +196,7 @@
    1.46    map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
    1.47  apply (unfold method_def)
    1.48  apply (simp split del: split_if)
    1.49 -apply (erule (1) class_rec_lemma [THEN trans]);
    1.50 +apply (erule (1) class_rec_lemma [THEN trans])
    1.51  apply auto
    1.52  done
    1.53  
    1.54 @@ -204,7 +210,7 @@
    1.55    map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
    1.56  apply (unfold fields_def)
    1.57  apply (simp split del: split_if)
    1.58 -apply (erule (1) class_rec_lemma [THEN trans]);
    1.59 +apply (erule (1) class_rec_lemma [THEN trans])
    1.60  apply auto
    1.61  done
    1.62