Some simple properties of dynamic accessibility added.
authorschirmer
Wed Feb 27 15:23:42 2002 +0100 (2002-02-27)
changeset 1296373fb6a200e36
parent 12962 a24ffe84a06a
child 12964 2ac9265b2cd5
Some simple properties of dynamic accessibility added.
src/HOL/Bali/WellForm.thy
     1.1 --- a/src/HOL/Bali/WellForm.thy	Wed Feb 27 08:52:09 2002 +0100
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Wed Feb 27 15:23:42 2002 +0100
     1.3 @@ -2872,6 +2872,27 @@
     1.4                                     dest: acc_modi_le_Dests)
     1.5  qed
     1.6  
     1.7 +subsubsection {* Properties of dynamic accessibility *}
     1.8 +
     1.9 +lemma dyn_accessible_Private:
    1.10 + assumes dyn_acc: "G \<turnstile> m in C dyn_accessible_from accC" and
    1.11 +            priv: "accmodi m = Private"
    1.12 +   shows "accC = declclass m"
    1.13 +proof -
    1.14 +  from dyn_acc priv
    1.15 +  show ?thesis
    1.16 +  proof (induct)
    1.17 +    case (Immediate C m)
    1.18 +    have "G \<turnstile> m in C permits_acc_to accC" and "accmodi m = Private" .
    1.19 +    then show ?case
    1.20 +      by (simp add: permits_acc_def)
    1.21 +  next
    1.22 +    case Overriding
    1.23 +    then show ?case
    1.24 +      by (auto dest!: overrides_commonD)
    1.25 +  qed
    1.26 +qed
    1.27 +
    1.28  text {* @{text dyn_accessible_Package} only works with the @{text wf_prog} assumption. 
    1.29  Without it. it is easy to leaf the Package!
    1.30  *}
    1.31 @@ -2915,6 +2936,26 @@
    1.32    qed
    1.33  qed
    1.34  
    1.35 +text {* For fields we don't need the wellformedness of the program, since
    1.36 +there is no overriding *}
    1.37 +lemma dyn_accessible_field_Package:
    1.38 + assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
    1.39 +            pack: "accmodi f = Package" and
    1.40 +           field: "is_field f"
    1.41 +   shows "pid accC = pid (declclass f)"
    1.42 +proof -
    1.43 +  from dyn_acc pack field
    1.44 +  show ?thesis
    1.45 +  proof (induct)
    1.46 +    case (Immediate C f)
    1.47 +    have "G \<turnstile> f in C permits_acc_to accC" and "accmodi f = Package" .
    1.48 +    then show ?case
    1.49 +      by (simp add: permits_acc_def)
    1.50 +  next
    1.51 +    case Overriding
    1.52 +    then show ?case by (simp add: is_field_def)
    1.53 +  qed
    1.54 +qed
    1.55  
    1.56  text {* @{text dyn_accessible_instance_field_Protected} only works for fields
    1.57  since methods can break the package bounds due to overriding