src/HOL/Bali/DeclConcepts.thy
changeset 12937 0c4fd7529467
parent 12925 99131847fb93
child 12962 a24ffe84a06a
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Feb 25 20:46:09 2002 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Mon Feb 25 20:48:14 2002 +0100
     1.3 @@ -1007,10 +1007,10 @@
     1.4              split: memberdecl.splits)
     1.5  
     1.6  lemma unique_member_of: 
     1.7 - (assumes n: "G\<turnstile>n member_of C" and  
     1.8 +  assumes n: "G\<turnstile>n member_of C" and  
     1.9            m: "G\<turnstile>m member_of C" and
    1.10         eqid: "memberid n = memberid m"
    1.11 - ) "n=m"
    1.12 +  shows "n=m"
    1.13  proof -
    1.14    from n m eqid  
    1.15    show "n=m"
    1.16 @@ -1173,9 +1173,9 @@
    1.17  by (cases "accmodi m") (auto simp add: permits_acc_def)
    1.18  
    1.19  lemma dyn_accessible_from_static_declC: 
    1.20 -  (assumes  acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and
    1.21 +  assumes  acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and
    1.22             static: "is_static m"
    1.23 -  ) "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
    1.24 +  shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
    1.25  proof -
    1.26    from acc_C static
    1.27    show "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
    1.28 @@ -1304,11 +1304,11 @@
    1.29  by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans)
    1.30  
    1.31  lemma member_of_inheritance:
    1.32 -  (assumes    m: "G\<turnstile>m member_of D" and 
    1.33 +  assumes       m: "G\<turnstile>m member_of D" and
    1.34       subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and
    1.35       subclseq_C_m: "G\<turnstile>C \<preceq>\<^sub>C declclass m" and
    1.36                 ws: "ws_prog G" 
    1.37 -  ) "G\<turnstile>m member_of C"
    1.38 +  shows "G\<turnstile>m member_of C"
    1.39  proof -
    1.40    from m subclseq_D_C subclseq_C_m
    1.41    show ?thesis
    1.42 @@ -1352,13 +1352,13 @@
    1.43  qed
    1.44  
    1.45  lemma member_of_subcls:
    1.46 -  (assumes    old: "G\<turnstile>old member_of C" and 
    1.47 +  assumes     old: "G\<turnstile>old member_of C" and 
    1.48                new: "G\<turnstile>new member_of D" and
    1.49               eqid: "memberid new = memberid old" and
    1.50       subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and 
    1.51     subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" and
    1.52                 ws: "ws_prog G"
    1.53 -  ) "G\<turnstile>D \<prec>\<^sub>C C"
    1.54 +  shows "G\<turnstile>D \<prec>\<^sub>C C"
    1.55  proof -
    1.56    from old 
    1.57    have subclseq_C_old: "G\<turnstile>C \<preceq>\<^sub>C declclass old"
    1.58 @@ -1423,10 +1423,10 @@
    1.59  
    1.60  
    1.61  lemma inherited_field_access: 
    1.62 - (assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and
    1.63 +  assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and
    1.64            is_field: "is_field membr" and 
    1.65            subclseq: "G \<turnstile> dynC \<preceq>\<^sub>C statC"
    1.66 - ) "G\<turnstile>membr in dynC dyn_accessible_from accC"
    1.67 +  shows "G\<turnstile>membr in dynC dyn_accessible_from accC"
    1.68  proof -
    1.69    from stat_acc is_field subclseq 
    1.70    show ?thesis
    1.71 @@ -1437,11 +1437,11 @@
    1.72  qed
    1.73  
    1.74  lemma accessible_inheritance:
    1.75 - (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
    1.76 +  assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
    1.77            subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
    1.78         member_dynC: "G\<turnstile>m member_of dynC" and
    1.79            dynC_acc: "G\<turnstile>(Class dynC) accessible_in (pid accC)"
    1.80 - ) "G\<turnstile>m of dynC accessible_from accC"
    1.81 +  shows "G\<turnstile>m of dynC accessible_from accC"
    1.82  proof -
    1.83    from stat_acc
    1.84    have member_statC: "G\<turnstile>m member_of statC" 
    1.85 @@ -1664,13 +1664,13 @@
    1.86  done
    1.87  
    1.88  lemma imethds_cases [consumes 3, case_names NewMethod InheritedMethod]:
    1.89 - (assumes im: "im \<in> imethds G I sig" and  
    1.90 +  assumes im: "im \<in> imethds G I sig" and  
    1.91           ifI: "iface G I = Some i" and
    1.92            ws: "ws_prog G" and
    1.93       hyp_new:  "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig 
    1.94                  = Some im \<Longrightarrow> P" and
    1.95       hyp_inh: "\<And> J. \<lbrakk>J \<in> set (isuperIfs i); im \<in> imethds G J sig\<rbrakk> \<Longrightarrow> P"
    1.96 -  ) "P"
    1.97 +  shows P
    1.98  proof -
    1.99    from ifI ws im hyp_new hyp_inh
   1.100    show "P"
   1.101 @@ -1756,9 +1756,9 @@
   1.102  by (auto dest: methd_declC method_declared_inI)
   1.103  
   1.104  lemma member_methd:
   1.105 - (assumes member_of: "G\<turnstile>Methd sig m member_of C" and
   1.106 +  assumes member_of: "G\<turnstile>Methd sig m member_of C" and
   1.107                   ws: "ws_prog G"
   1.108 - ) "methd G C sig = Some m"
   1.109 +  shows "methd G C sig = Some m"
   1.110  proof -
   1.111    from member_of 
   1.112    have iscls_C: "is_class G C" 
   1.113 @@ -2013,13 +2013,13 @@
   1.114  by (auto simp add: dynmethd_rec)
   1.115   
   1.116  lemma dynmethd_Some_cases [consumes 3, case_names Static Overrides]:
   1.117 -  (assumes dynM: "dynmethd G statC dynC sig = Some dynM" and
   1.118 +  assumes      dynM: "dynmethd G statC dynC sig = Some dynM" and
   1.119          is_cls_dynC: "is_class G dynC" and
   1.120                   ws: "ws_prog G" and
   1.121           hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
   1.122         hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;dynM\<noteq>statM;
   1.123                         G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
   1.124 -   ) "P"
   1.125 +  shows P
   1.126  proof -
   1.127    from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
   1.128    from clsDynC ws dynM hyp_static hyp_override
   1.129 @@ -2037,13 +2037,12 @@
   1.130  qed
   1.131  
   1.132  lemma no_override_in_Object:
   1.133 -  (assumes     dynM: "dynmethd G statC dynC sig = Some dynM" and
   1.134 +  assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
   1.135              is_cls_dynC: "is_class G dynC" and
   1.136                       ws: "ws_prog G" and
   1.137                    statM: "methd G statC sig = Some statM" and
   1.138           neq_dynM_statM: "dynM\<noteq>statM"
   1.139 -   )
   1.140 -   "dynC \<noteq> Object"
   1.141 +  shows "dynC \<noteq> Object"
   1.142  proof -
   1.143    from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
   1.144    from clsDynC ws dynM statM neq_dynM_statM 
   1.145 @@ -2063,7 +2062,7 @@
   1.146  
   1.147  lemma dynmethd_Some_rec_cases [consumes 3, 
   1.148                                 case_names Static Override  Recursion]:
   1.149 -(assumes     dynM: "dynmethd G statC dynC sig = Some dynM" and
   1.150 +  assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
   1.151                  clsDynC: "class G dynC = Some c" and
   1.152                       ws: "ws_prog G" and
   1.153               hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
   1.154 @@ -2072,8 +2071,8 @@
   1.155                                       G,sig\<turnstile> dynM overrides statM\<rbrakk> \<Longrightarrow> P" and
   1.156  
   1.157            hyp_recursion: "\<lbrakk>dynC\<noteq>Object;
   1.158 -                           dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P" 
   1.159 -  ) "P"
   1.160 +                           dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P"
   1.161 +  shows P
   1.162  proof -
   1.163    from clsDynC have "is_class G dynC" by simp
   1.164    note no_override_in_Object' = no_override_in_Object [OF dynM this ws]
   1.165 @@ -2139,12 +2138,12 @@
   1.166  qed
   1.167  
   1.168  lemma methd_Some_dynmethd_Some:
   1.169 -  (assumes    statM: "methd G statC sig = Some statM" and 
   1.170 +  assumes     statM: "methd G statC sig = Some statM" and
   1.171             subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   1.172         is_cls_statC: "is_class G statC" and
   1.173                   ws: "ws_prog G"
   1.174 -   ) "\<exists> dynM. dynmethd G statC dynC sig = Some dynM"
   1.175 -   (is "?P dynC")
   1.176 +  shows "\<exists> dynM. dynmethd G statC dynC sig = Some dynM"
   1.177 +    (is "?P dynC")
   1.178  proof -
   1.179    from subclseq is_cls_statC 
   1.180    have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
   1.181 @@ -2185,7 +2184,7 @@
   1.182  qed
   1.183  
   1.184  lemma dynmethd_cases [consumes 4, case_names Static Overrides]:
   1.185 -  (assumes    statM: "methd G statC sig = Some statM" and 
   1.186 +  assumes     statM: "methd G statC sig = Some statM" and 
   1.187             subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   1.188         is_cls_statC: "is_class G statC" and
   1.189                   ws: "ws_prog G" and
   1.190 @@ -2193,7 +2192,7 @@
   1.191         hyp_override: "\<And> dynM. \<lbrakk>dynmethd G statC dynC sig = Some dynM;
   1.192                                   dynM\<noteq>statM;
   1.193                             G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
   1.194 -   ) "P"
   1.195 +  shows P
   1.196  proof -
   1.197    from subclseq is_cls_statC 
   1.198    have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
   1.199 @@ -2215,13 +2214,13 @@
   1.200  qed
   1.201  
   1.202  lemma ws_dynmethd:
   1.203 -  (assumes statM: "methd G statC sig = Some statM" and
   1.204 +  assumes  statM: "methd G statC sig = Some statM" and
   1.205          subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   1.206      is_cls_statC: "is_class G statC" and
   1.207                ws: "ws_prog G"
   1.208 -   )
   1.209 -   "\<exists> dynM. dynmethd G statC dynC sig = Some dynM \<and>
   1.210 -            is_static dynM = is_static statM \<and> G\<turnstile>resTy dynM\<preceq>resTy statM"
   1.211 +  shows
   1.212 +    "\<exists> dynM. dynmethd G statC dynC sig = Some dynM \<and>
   1.213 +             is_static dynM = is_static statM \<and> G\<turnstile>resTy dynM\<preceq>resTy statM"
   1.214  proof - 
   1.215    from statM subclseq is_cls_statC ws
   1.216    show ?thesis