src/HOL/Bali/DeclConcepts.thy
changeset 34990 81e8fdfeb849
parent 34915 7894c7dab132
child 35067 af4c18c30593
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Sat Jan 30 17:01:01 2010 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Sat Jan 30 17:03:46 2010 +0100
     1.3 @@ -915,23 +915,15 @@
     1.4      assume "G \<turnstile> m member_of C"
     1.5      then show "n=m"
     1.6      proof (cases)
     1.7 -      case (Immediate m' _)
     1.8 -      with eqid 
     1.9 -      have "m=m'"
    1.10 -           "memberid n = memberid m" 
    1.11 -           "G\<turnstile> mbr m declared_in C" 
    1.12 -           "declclass m = C"
    1.13 -        by auto
    1.14 -      with member_n   
    1.15 +      case Immediate
    1.16 +      with eqid member_n
    1.17        show ?thesis
    1.18          by (cases n, cases m) 
    1.19             (auto simp add: declared_in_def 
    1.20                             cdeclaredmethd_def cdeclaredfield_def
    1.21                      split: memberdecl.splits)
    1.22      next
    1.23 -      case (Inherited m' _ _)
    1.24 -      then have "G\<turnstile> memberid m undeclared_in C"
    1.25 -        by simp
    1.26 +      case Inherited
    1.27        with eqid member_n
    1.28        show ?thesis
    1.29          by (cases n) (auto dest: declared_not_undeclared)
    1.30 @@ -1656,10 +1648,7 @@
    1.31      from member_of
    1.32      show "?Methd C"
    1.33      proof (cases)
    1.34 -      case (Immediate membr Ca)
    1.35 -      then have "Ca=C" "membr = method sig m" and 
    1.36 -                "G\<turnstile>Methd sig m declared_in C" "declclass m = C"
    1.37 -        by (cases m,auto)
    1.38 +      case Immediate
    1.39        with clsC 
    1.40        have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m"
    1.41          by (cases m)
    1.42 @@ -1669,13 +1658,12 @@
    1.43        show ?thesis
    1.44          by (simp add: methd_rec)
    1.45      next
    1.46 -      case (Inherited membr Ca S)
    1.47 +      case (Inherited S)
    1.48        with clsC
    1.49 -      have eq_Ca_C: "Ca=C" and
    1.50 -            undecl: "G\<turnstile>mid sig undeclared_in C" and
    1.51 +      have  undecl: "G\<turnstile>mid sig undeclared_in C" and
    1.52               super: "G \<turnstile>Methd sig m member_of (super c)"
    1.53          by (auto dest: subcls1D)
    1.54 -      from eq_Ca_C clsC undecl 
    1.55 +      from clsC undecl 
    1.56        have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = None"
    1.57          by (auto simp add: undeclared_in_def cdeclaredmethd_def
    1.58                      intro: table_of_mapconst_NoneI)