src/HOL/Bali/DeclConcepts.thy
changeset 45471 489f27dcc0f4
parent 41778 5f79a9e42507
child 46714 a7ca72710dfe
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Sat Nov 12 17:52:28 2011 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Sat Nov 12 17:53:48 2011 +0100
     1.3 @@ -1071,25 +1071,16 @@
     1.4  done
     1.5  
     1.6  lemma member_of_Package: 
     1.7 - "\<lbrakk>G\<turnstile>m member_of C; accmodi m = Package\<rbrakk> 
     1.8 -  \<Longrightarrow> pid (declclass m) = pid C" 
     1.9 -proof -
    1.10 -  assume   member: "G\<turnstile>m member_of C"
    1.11 -  then show " accmodi m = Package \<Longrightarrow> ?thesis" (is "PROP ?P m C")
    1.12 -  proof (induct rule: members.induct)
    1.13 -    fix C m
    1.14 -    assume     C: "declclass m = C"
    1.15 -    then show "pid (declclass m) = pid C"
    1.16 -      by simp
    1.17 -  next
    1.18 -    fix C S m  
    1.19 -    assume inheritable: "G \<turnstile> m inheritable_in pid C"
    1.20 -    assume         hyp: "PROP ?P m S" and
    1.21 -           package_acc: "accmodi m = Package" 
    1.22 -    with inheritable package_acc hyp
    1.23 -    show "pid (declclass m) = pid C" 
    1.24 -      by (auto simp add: inheritable_in_def)
    1.25 -  qed
    1.26 +  assumes "G\<turnstile>m member_of C"
    1.27 +    and "accmodi m = Package"
    1.28 +  shows "pid (declclass m) = pid C"
    1.29 +  using assms
    1.30 +proof induct
    1.31 +  case Immediate
    1.32 +  then show ?case by simp
    1.33 +next
    1.34 +  case Inherited
    1.35 +  then show ?case by (auto simp add: inheritable_in_def)
    1.36  qed
    1.37  
    1.38  lemma member_in_declC: "G\<turnstile>m member_in C\<Longrightarrow> G\<turnstile>m member_in (declclass m)"
    1.39 @@ -1581,19 +1572,14 @@
    1.40  apply (force elim: imethds_norec intro: rtrancl_into_rtrancl2)
    1.41  done
    1.42  
    1.43 -lemma imethds_cases [consumes 3, case_names NewMethod InheritedMethod]:
    1.44 -  assumes im: "im \<in> imethds G I sig" and  
    1.45 -         ifI: "iface G I = Some i" and
    1.46 -          ws: "ws_prog G" and
    1.47 -     hyp_new:  "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig 
    1.48 -                = Some im \<Longrightarrow> P" and
    1.49 -     hyp_inh: "\<And> J. \<lbrakk>J \<in> set (isuperIfs i); im \<in> imethds G J sig\<rbrakk> \<Longrightarrow> P"
    1.50 -  shows P
    1.51 -proof -
    1.52 -  from ifI ws im hyp_new hyp_inh
    1.53 -  show "P"
    1.54 -    by (auto simp add: imethds_rec)
    1.55 -qed
    1.56 +lemma imethds_cases:
    1.57 +  assumes im: "im \<in> imethds G I sig"
    1.58 +    and ifI: "iface G I = Some i"
    1.59 +    and ws: "ws_prog G"
    1.60 +  obtains (NewMethod) "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig = Some im"
    1.61 +    | (InheritedMethod) J where "J \<in> set (isuperIfs i)" and "im \<in> imethds G J sig"
    1.62 +using assms by (auto simp add: imethds_rec)
    1.63 +
    1.64  
    1.65  subsection "accimethd"
    1.66  
    1.67 @@ -1758,7 +1744,7 @@
    1.68  lemma accmethd_SomeD:
    1.69  "accmethd G S C sig = Some m
    1.70   \<Longrightarrow> methd G C sig = Some m \<and> G\<turnstile>method sig m of C accessible_from S"
    1.71 -by (auto simp add: accmethd_def dest: filter_tab_SomeD)
    1.72 +by (auto simp add: accmethd_def)
    1.73  
    1.74  lemma accmethd_SomeI:
    1.75  "\<lbrakk>methd G C sig = Some m; G\<turnstile>method sig m of C accessible_from S\<rbrakk> 
    1.76 @@ -1836,13 +1822,13 @@
    1.77        next
    1.78          case (Some statM)
    1.79          note statM = Some
    1.80 -        let "?filter C" = 
    1.81 -              "filter_tab
    1.82 +        let ?filter = 
    1.83 +              "\<lambda>C. filter_tab
    1.84                  (\<lambda>_ dynM. G,sig \<turnstile> dynM overrides statM \<or> dynM = statM)
    1.85                  (methd G C)"
    1.86 -        let "?class_rec C" =
    1.87 -              "(class_rec G C empty
    1.88 -                           (\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C)))"
    1.89 +        let ?class_rec =
    1.90 +              "\<lambda>C. class_rec G C empty
    1.91 +                           (\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C))"
    1.92          from statM Subcls ws subclseq_dynC_statC
    1.93          have dynmethd_dynC_def:
    1.94               "?Dynmethd_def dynC sig =
    1.95 @@ -1924,18 +1910,19 @@
    1.96    \<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C statC \<and> (\<exists> statM. methd G statC sig = Some statM)"
    1.97  by (auto simp add: dynmethd_rec)
    1.98   
    1.99 -lemma dynmethd_Some_cases [consumes 3, case_names Static Overrides]:
   1.100 -  assumes      dynM: "dynmethd G statC dynC sig = Some dynM" and
   1.101 -        is_cls_dynC: "is_class G dynC" and
   1.102 -                 ws: "ws_prog G" and
   1.103 -         hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
   1.104 -       hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;dynM\<noteq>statM;
   1.105 -                       G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
   1.106 -  shows P
   1.107 +lemma dynmethd_Some_cases:
   1.108 +  assumes dynM: "dynmethd G statC dynC sig = Some dynM"
   1.109 +    and is_cls_dynC: "is_class G dynC"
   1.110 +    and ws: "ws_prog G"
   1.111 +  obtains (Static) "methd G statC sig = Some dynM"
   1.112 +    | (Overrides) statM
   1.113 +      where "methd G statC sig = Some statM"
   1.114 +        and "dynM \<noteq> statM"
   1.115 +        and "G,sig\<turnstile>dynM overrides statM"
   1.116  proof -
   1.117    from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
   1.118 -  from clsDynC ws dynM hyp_static hyp_override
   1.119 -  show "P"
   1.120 +  from clsDynC ws dynM Static Overrides
   1.121 +  show ?thesis
   1.122    proof (induct rule: ws_class_induct)
   1.123      case (Object co)
   1.124      with ws  have "statC = Object" 
   1.125 @@ -1972,25 +1959,20 @@
   1.126  qed
   1.127  
   1.128  
   1.129 -lemma dynmethd_Some_rec_cases [consumes 3, 
   1.130 -                               case_names Static Override  Recursion]:
   1.131 -  assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
   1.132 -                clsDynC: "class G dynC = Some c" and
   1.133 -                     ws: "ws_prog G" and
   1.134 -             hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
   1.135 -           hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;
   1.136 -                                     methd G dynC sig = Some dynM; statM\<noteq>dynM;
   1.137 -                                     G,sig\<turnstile> dynM overrides statM\<rbrakk> \<Longrightarrow> P" and
   1.138 -
   1.139 -          hyp_recursion: "\<lbrakk>dynC\<noteq>Object;
   1.140 -                           dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P"
   1.141 -  shows P
   1.142 +lemma dynmethd_Some_rec_cases:
   1.143 +  assumes dynM: "dynmethd G statC dynC sig = Some dynM"
   1.144 +    and clsDynC: "class G dynC = Some c"
   1.145 +    and ws: "ws_prog G"
   1.146 +  obtains (Static) "methd G statC sig = Some dynM"
   1.147 +    | (Override) statM where "methd G statC sig = Some statM"
   1.148 +        and "methd G dynC sig = Some dynM" and "statM \<noteq> dynM"
   1.149 +        and "G,sig\<turnstile> dynM overrides statM"
   1.150 +    | (Recursion) "dynC \<noteq> Object" and "dynmethd G statC (super c) sig = Some dynM"
   1.151  proof -
   1.152 -  from clsDynC have "is_class G dynC" by simp
   1.153 -  note no_override_in_Object' = no_override_in_Object [OF dynM this ws]
   1.154 -  from ws clsDynC dynM hyp_static hyp_override hyp_recursion
   1.155 +  from clsDynC have *: "is_class G dynC" by simp
   1.156 +  from ws clsDynC dynM Static Override Recursion
   1.157    show ?thesis
   1.158 -    by (auto simp add: dynmethd_rec dest: no_override_in_Object')
   1.159 +    by (auto simp add: dynmethd_rec dest: no_override_in_Object [OF dynM * ws])
   1.160  qed
   1.161  
   1.162  lemma dynmethd_declC: 
   1.163 @@ -2095,24 +2077,22 @@
   1.164    qed
   1.165  qed
   1.166  
   1.167 -lemma dynmethd_cases [consumes 4, case_names Static Overrides]:
   1.168 -  assumes     statM: "methd G statC sig = Some statM" and 
   1.169 -           subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   1.170 -       is_cls_statC: "is_class G statC" and
   1.171 -                 ws: "ws_prog G" and
   1.172 -         hyp_static: "dynmethd G statC dynC sig = Some statM \<Longrightarrow> P" and
   1.173 -       hyp_override: "\<And> dynM. \<lbrakk>dynmethd G statC dynC sig = Some dynM;
   1.174 -                                 dynM\<noteq>statM;
   1.175 -                           G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
   1.176 -  shows P
   1.177 +lemma dynmethd_cases:
   1.178 +  assumes statM: "methd G statC sig = Some statM"
   1.179 +    and subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
   1.180 +    and is_cls_statC: "is_class G statC"
   1.181 +    and ws: "ws_prog G"
   1.182 +  obtains (Static) "dynmethd G statC dynC sig = Some statM"
   1.183 +    | (Overrides) dynM where "dynmethd G statC dynC sig = Some dynM"
   1.184 +        and "dynM \<noteq> statM" and "G,sig\<turnstile>dynM overrides statM"
   1.185  proof -
   1.186 +  note hyp_static = Static and hyp_override = Overrides
   1.187    from subclseq is_cls_statC 
   1.188    have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
   1.189    then obtain dc where
   1.190      clsDynC: "class G dynC = Some dc" by blast
   1.191    from statM subclseq is_cls_statC ws 
   1.192 -  obtain dynM
   1.193 -    where dynM: "dynmethd G statC dynC sig = Some dynM"
   1.194 +  obtain dynM where dynM: "dynmethd G statC dynC sig = Some dynM"
   1.195      by (blast dest: methd_Some_dynmethd_Some)
   1.196    from dynM is_cls_dynC ws 
   1.197    show ?thesis
   1.198 @@ -2151,14 +2131,13 @@
   1.199  
   1.200  subsection "dynlookup"
   1.201  
   1.202 -lemma dynlookup_cases [consumes 1, case_names NullT IfaceT ClassT ArrayT]:
   1.203 -"\<lbrakk>dynlookup G statT dynC sig = x;
   1.204 -           \<lbrakk>statT = NullT       ; empty sig = x                  \<rbrakk> \<Longrightarrow> P;
   1.205 -  \<And> I.    \<lbrakk>statT = IfaceT I    ; dynimethd G I      dynC sig = x\<rbrakk> \<Longrightarrow> P;
   1.206 -  \<And> statC.\<lbrakk>statT = ClassT statC; dynmethd  G statC  dynC sig = x\<rbrakk> \<Longrightarrow> P;
   1.207 -  \<And> ty.   \<lbrakk>statT = ArrayT ty   ; dynmethd  G Object dynC sig = x\<rbrakk> \<Longrightarrow> P
   1.208 - \<rbrakk> \<Longrightarrow> P"
   1.209 -by (cases statT) (auto simp add: dynlookup_def)
   1.210 +lemma dynlookup_cases:
   1.211 +  assumes "dynlookup G statT dynC sig = x"
   1.212 +  obtains (NullT) "statT = NullT" and "empty sig = x"
   1.213 +    | (IfaceT) I where "statT = IfaceT I" and "dynimethd G I dynC sig = x"
   1.214 +    | (ClassT) statC where "statT = ClassT statC" and "dynmethd G statC dynC sig = x"
   1.215 +    | (ArrayT) ty where "statT = ArrayT ty" and "dynmethd G Object dynC sig = x"
   1.216 +using assms by (cases statT) (auto simp add: dynlookup_def)
   1.217  
   1.218  subsection "fields"
   1.219