src/HOL/Bali/DeclConcepts.thy
changeset 34915 7894c7dab132
parent 32960 69916a850301
child 34990 81e8fdfeb849
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Sun Jan 10 18:41:07 2010 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Sun Jan 10 18:43:45 2010 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Bali/DeclConcepts.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Norbert Schirmer
     1.7  *)
     1.8  header {* Advanced concepts on Java declarations like overriding, inheritance,
     1.9 @@ -2282,74 +2281,47 @@
    1.10  done
    1.11  
    1.12  lemma superclasses_mono:
    1.13 -"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c;
    1.14 -  \<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc;
    1.15 -  x\<in>superclasses G D 
    1.16 -\<rbrakk> \<Longrightarrow> x\<in>superclasses G C" 
    1.17 -proof -
    1.18 -  
    1.19 -  assume     ws: "ws_prog G"          and 
    1.20 -          cls_C: "class G C = Some c" and
    1.21 -             wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
    1.22 -                  \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
    1.23 -  assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D"           
    1.24 -  thus "\<And> c. \<lbrakk>class G C = Some c; x\<in>superclasses G D\<rbrakk>\<Longrightarrow>
    1.25 -        x\<in>superclasses G C" (is "PROP ?P C"  
    1.26 -                             is "\<And> c. ?CLS C c \<Longrightarrow> ?SUP D \<Longrightarrow> ?SUP C")
    1.27 -  proof (induct ?P C  rule: converse_trancl_induct)
    1.28 -    fix C c
    1.29 -    assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1D" "class G C = Some c" "x \<in> superclasses G D"
    1.30 -    with wf ws show "?SUP C"
    1.31 -      by (auto    intro: no_subcls1_Object 
    1.32 -               simp add: superclasses_rec subcls1_def)
    1.33 -  next
    1.34 -    fix C S c
    1.35 -    assume clsrel': "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S \<prec>\<^sub>C D"
    1.36 -       and    hyp : "\<And> s. \<lbrakk>class G S = Some s; x \<in> superclasses G D\<rbrakk>
    1.37 -                           \<Longrightarrow> x \<in> superclasses G S"
    1.38 -       and  cls_C': "class G C = Some c"
    1.39 -       and       x: "x \<in> superclasses G D"
    1.40 -    moreover note wf ws
    1.41 -    moreover from calculation 
    1.42 -    have "?SUP S" 
    1.43 -      by (force intro: no_subcls1_Object simp add: subcls1_def)
    1.44 -    moreover from calculation 
    1.45 -    have "super c = S" 
    1.46 -      by (auto intro: no_subcls1_Object simp add: subcls1_def)
    1.47 -    ultimately show "?SUP C" 
    1.48 -      by (auto intro: no_subcls1_Object simp add: superclasses_rec)
    1.49 -  qed
    1.50 +  assumes clsrel: "G\<turnstile>C\<prec>\<^sub>C D"
    1.51 +  and ws: "ws_prog G"
    1.52 +  and cls_C: "class G C = Some c"
    1.53 +  and wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
    1.54 +    \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
    1.55 +  and x: "x\<in>superclasses G D"
    1.56 +  shows "x\<in>superclasses G C" using clsrel cls_C x
    1.57 +proof (induct arbitrary: c rule: converse_trancl_induct)
    1.58 +  case (base C)
    1.59 +  with wf ws show ?case
    1.60 +    by (auto    intro: no_subcls1_Object 
    1.61 +             simp add: superclasses_rec subcls1_def)
    1.62 +next
    1.63 +  case (step C S)
    1.64 +  moreover note wf ws
    1.65 +  moreover from calculation 
    1.66 +  have "x\<in>superclasses G S"
    1.67 +    by (force intro: no_subcls1_Object simp add: subcls1_def)
    1.68 +  moreover from calculation 
    1.69 +  have "super c = S" 
    1.70 +    by (auto intro: no_subcls1_Object simp add: subcls1_def)
    1.71 +  ultimately show ?case 
    1.72 +    by (auto intro: no_subcls1_Object simp add: superclasses_rec)
    1.73  qed
    1.74  
    1.75  lemma subclsEval:
    1.76 -"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c;
    1.77 -  \<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc 
    1.78 - \<rbrakk> \<Longrightarrow> D\<in>superclasses G C" 
    1.79 -proof -
    1.80 -  note converse_trancl_induct 
    1.81 -       = converse_trancl_induct [consumes 1,case_names Single Step]
    1.82 -  assume 
    1.83 -             ws: "ws_prog G"          and 
    1.84 -          cls_C: "class G C = Some c" and
    1.85 -             wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
    1.86 -                  \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
    1.87 -  assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D"           
    1.88 -  thus "\<And> c. class G C = Some c\<Longrightarrow> D\<in>superclasses G C" 
    1.89 -    (is "PROP ?P C"  is "\<And> c. ?CLS C c  \<Longrightarrow> ?SUP C")
    1.90 -  proof (induct ?P C  rule: converse_trancl_induct)
    1.91 -    fix C c
    1.92 -    assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" "class G C = Some c"
    1.93 -    with ws wf show "?SUP C"
    1.94 -      by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def)
    1.95 -  next
    1.96 -    fix C S c
    1.97 -    assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S\<prec>\<^sub>C D" 
    1.98 -           "\<And>s. class G S = Some s \<Longrightarrow> D \<in> superclasses G S"
    1.99 -           "class G C = Some c" 
   1.100 -    with ws wf show "?SUP C"
   1.101 -      by - (rule superclasses_mono,
   1.102 -            auto dest: no_subcls1_Object simp add: subcls1_def )
   1.103 -  qed
   1.104 +  assumes clsrel: "G\<turnstile>C\<prec>\<^sub>C D"
   1.105 +  and ws: "ws_prog G"
   1.106 +  and cls_C: "class G C = Some c"
   1.107 +  and wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
   1.108 +    \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
   1.109 +  shows "D\<in>superclasses G C" using clsrel cls_C
   1.110 +proof (induct arbitrary: c rule: converse_trancl_induct)
   1.111 +  case (base C)
   1.112 +  with ws wf show ?case
   1.113 +    by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def)
   1.114 +next
   1.115 +  case (step C S)
   1.116 +  with ws wf show ?case
   1.117 +    by - (rule superclasses_mono,
   1.118 +          auto dest: no_subcls1_Object simp add: subcls1_def )
   1.119  qed
   1.120  
   1.121  end