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
```