# HG changeset patch
# User schirmer
# Date 1014819822 -3600
# Node ID 73fb6a200e3610b88e9361871d970f8593e09cd2
# Parent  a24ffe84a06a5bfd6e4639c705e882649753169a
Some simple properties of dynamic accessibility added.

diff -r a24ffe84a06a -r 73fb6a200e36 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Wed Feb 27 08:52:09 2002 +0100
+++ b/src/HOL/Bali/WellForm.thy	Wed Feb 27 15:23:42 2002 +0100
@@ -2872,6 +2872,27 @@
                                    dest: acc_modi_le_Dests)
 qed
 
+subsubsection {* Properties of dynamic accessibility *}
+
+lemma dyn_accessible_Private:
+ assumes dyn_acc: "G \<turnstile> m in C dyn_accessible_from accC" and
+            priv: "accmodi m = Private"
+   shows "accC = declclass m"
+proof -
+  from dyn_acc priv
+  show ?thesis
+  proof (induct)
+    case (Immediate C m)
+    have "G \<turnstile> m in C permits_acc_to accC" and "accmodi m = Private" .
+    then show ?case
+      by (simp add: permits_acc_def)
+  next
+    case Overriding
+    then show ?case
+      by (auto dest!: overrides_commonD)
+  qed
+qed
+
 text {* @{text dyn_accessible_Package} only works with the @{text wf_prog} assumption. 
 Without it. it is easy to leaf the Package!
 *}
@@ -2915,6 +2936,26 @@
   qed
 qed
 
+text {* For fields we don't need the wellformedness of the program, since
+there is no overriding *}
+lemma dyn_accessible_field_Package:
+ assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
+            pack: "accmodi f = Package" and
+           field: "is_field f"
+   shows "pid accC = pid (declclass f)"
+proof -
+  from dyn_acc pack field
+  show ?thesis
+  proof (induct)
+    case (Immediate C f)
+    have "G \<turnstile> f in C permits_acc_to accC" and "accmodi f = Package" .
+    then show ?case
+      by (simp add: permits_acc_def)
+  next
+    case Overriding
+    then show ?case by (simp add: is_field_def)
+  qed
+qed
 
 text {* @{text dyn_accessible_instance_field_Protected} only works for fields
 since methods can break the package bounds due to overriding