# HG changeset patch
# User schirmer
# Date 1014796329 -3600
# Node ID a24ffe84a06a5bfd6e4639c705e882649753169a
# Parent  cd4f8d5c645088e1b51bb07bada2e853a67e4d44
Cleaning up the definition of static overriding.

diff -r cd4f8d5c6450 -r a24ffe84a06a src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Tue Feb 26 21:57:13 2002 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Wed Feb 27 08:52:09 2002 +0100
@@ -689,7 +689,6 @@
 inductive "stat_overridesR G" intros
 
 Direct: "\<lbrakk>\<not> is_static new; msig new = msig old; 
-         G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old);
          G\<turnstile>Method new declared_in (declclass new);  
          G\<turnstile>Method old declared_in (declclass old); 
          G\<turnstile>Method old inheritable_in pid (declclass new);
@@ -792,14 +791,6 @@
   G\<turnstile>Method old declared_in (declclass old)"
 by (induct set: overridesR) (auto intro: trancl_trans ws_widen_trans)
 
-lemma stat_overrides_commonD:
-"\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow>  
-  declclass new \<noteq> Object \<and> \<not> is_static new \<and> msig new = msig old \<and> 
-  G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
-  G\<turnstile>Method new declared_in (declclass new) \<and>   
-  G\<turnstile>Method old declared_in (declclass old)"
-by (induct set: stat_overridesR) (auto intro: trancl_trans)
-
 lemma overrides_eq_sigD: 
  "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> msig old=msig new"
 by (auto dest: overrides_commonD)
@@ -1107,6 +1098,26 @@
 by (auto dest: member_inD member_of_class_relation
         intro: rtrancl_trans)
 
+lemma stat_override_declclasses_relation: 
+"\<lbrakk>G\<turnstile>(declclass new) \<prec>\<^sub>C\<^sub>1 superNew; G \<turnstile>Method old member_of superNew \<rbrakk>
+\<Longrightarrow> G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old)"
+apply (rule trancl_rtrancl_trancl)
+apply (erule r_into_trancl)
+apply (cases old)
+apply (auto dest: member_of_class_relation)
+done
+
+lemma stat_overrides_commonD:
+"\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow>  
+  declclass new \<noteq> Object \<and> \<not> is_static new \<and> msig new = msig old \<and> 
+  G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
+  G\<turnstile>Method new declared_in (declclass new) \<and>   
+  G\<turnstile>Method old declared_in (declclass old)"
+apply (induct set: stat_overridesR) 
+apply (frule (1) stat_override_declclasses_relation) 
+apply (auto intro: trancl_trans)
+done
+
 lemma member_of_Package: 
  "\<lbrakk>G\<turnstile>m member_of C; accmodi m = Package\<rbrakk> 
   \<Longrightarrow> pid (declclass m) = pid C" 
diff -r cd4f8d5c6450 -r a24ffe84a06a src/HOL/Bali/ROOT.ML
--- a/src/HOL/Bali/ROOT.ML	Tue Feb 26 21:57:13 2002 +0100
+++ b/src/HOL/Bali/ROOT.ML	Wed Feb 27 08:52:09 2002 +0100
@@ -1,4 +1,3 @@
-
 use_thy "AxExample";
 use_thy "AxSound";
 use_thy "AxCompl";
diff -r cd4f8d5c6450 -r a24ffe84a06a src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Tue Feb 26 21:57:13 2002 +0100
+++ b/src/HOL/Bali/WellForm.thy	Wed Feb 27 08:52:09 2002 +0100
@@ -820,7 +820,7 @@
     qed
     with Direct resTy_widen not_static_old 
     show "?Overrides new old" 
-      by (auto intro: overridesR.Direct) 
+      by (auto intro: overridesR.Direct stat_override_declclasses_relation) 
   next
     case (Indirect inter new old)
     then show "?Overrides new old"