src/HOL/Bali/WellForm.thy
changeset 34915 7894c7dab132
parent 32960 69916a850301
child 35067 af4c18c30593
     1.1 --- a/src/HOL/Bali/WellForm.thy	Sun Jan 10 18:41:07 2010 +0100
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Sun Jan 10 18:43:45 2010 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Bali/WellForm.thy
     1.5 -    ID:         $Id$
     1.6      Author:     David von Oheimb and Norbert Schirmer
     1.7  *)
     1.8  
     1.9 @@ -1409,8 +1408,7 @@
    1.10    from clsC ws 
    1.11    show "methd G C sig = Some m 
    1.12          \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
    1.13 -    (is "PROP ?P C") 
    1.14 -  proof (induct ?P C rule: ws_class_induct')
    1.15 +  proof (induct C rule: ws_class_induct')
    1.16      case Object
    1.17      assume "methd G Object sig = Some m" 
    1.18      with wf show ?thesis
    1.19 @@ -1755,28 +1753,20 @@
    1.20  lemma ballE': "\<forall>x\<in>A. P x \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> Q" by blast
    1.21  
    1.22  lemma subint_widen_imethds: 
    1.23 - "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J; jm \<in> imethds G J sig\<rbrakk> \<Longrightarrow>   
    1.24 -  \<exists> im \<in> imethds G I sig. is_static im = is_static jm \<and> 
    1.25 +  assumes irel: "G\<turnstile>I\<preceq>I J"
    1.26 +  and wf: "wf_prog G"
    1.27 +  and is_iface: "is_iface G J"
    1.28 +  and jm: "jm \<in> imethds G J sig"
    1.29 +  shows "\<exists>im \<in> imethds G I sig. is_static im = is_static jm \<and> 
    1.30                            accmodi im = accmodi jm \<and>
    1.31                            G\<turnstile>resTy im\<preceq>resTy jm"
    1.32 -proof -
    1.33 -  assume irel: "G\<turnstile>I\<preceq>I J" and
    1.34 -           wf: "wf_prog G" and
    1.35 -     is_iface: "is_iface G J"
    1.36 -  from irel show "jm \<in> imethds G J sig \<Longrightarrow> ?thesis" 
    1.37 -               (is "PROP ?P I" is "PROP ?Prem J \<Longrightarrow> ?Concl I")
    1.38 -  proof (induct ?P I rule: converse_rtrancl_induct) 
    1.39 -    case Id
    1.40 -    assume "jm \<in> imethds G J sig"
    1.41 -    then show "?Concl J" by  (blast elim: bexI')
    1.42 +  using irel jm
    1.43 +proof (induct rule: converse_rtrancl_induct)
    1.44 +    case base
    1.45 +    then show ?case by  (blast elim: bexI')
    1.46    next
    1.47 -    case Step
    1.48 -    fix I SI
    1.49 -    assume subint1_I_SI: "G\<turnstile>I \<prec>I1 SI" and 
    1.50 -            subint_SI_J: "G\<turnstile>SI \<preceq>I J" and
    1.51 -                    hyp: "PROP ?P SI" and
    1.52 -                     jm: "jm \<in> imethds G J sig"
    1.53 -    from subint1_I_SI 
    1.54 +    case (step I SI)
    1.55 +    from `G\<turnstile>I \<prec>I1 SI`
    1.56      obtain i where
    1.57        ifI: "iface G I = Some i" and
    1.58         SI: "SI \<in> set (isuperIfs i)"
    1.59 @@ -1784,10 +1774,10 @@
    1.60  
    1.61      let ?newMethods 
    1.62            = "(Option.set \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
    1.63 -    show "?Concl I"
    1.64 +    show ?case
    1.65      proof (cases "?newMethods sig = {}")
    1.66        case True
    1.67 -      with ifI SI hyp wf jm 
    1.68 +      with ifI SI step wf
    1.69        show "?thesis" 
    1.70          by (auto simp add: imethds_rec) 
    1.71      next
    1.72 @@ -1816,7 +1806,7 @@
    1.73          wf_SI: "wf_idecl G (SI,si)" 
    1.74          by (auto dest!: wf_idecl_supD is_acc_ifaceD
    1.75                    dest: wf_prog_idecl)
    1.76 -      from jm hyp 
    1.77 +      from step
    1.78        obtain sim::"qtname \<times> mhead"  where
    1.79                        sim: "sim \<in> imethds G SI sig" and
    1.80           eq_static_sim_jm: "is_static sim = is_static jm" and 
    1.81 @@ -1841,7 +1831,6 @@
    1.82        show ?thesis 
    1.83          by auto 
    1.84      qed
    1.85 -  qed
    1.86  qed
    1.87       
    1.88  (* Tactical version *)
    1.89 @@ -1974,30 +1963,20 @@
    1.90    from clsC ws 
    1.91    show "\<And> m d. \<lbrakk>methd G C sig = Some m; class G (declclass m) = Some d\<rbrakk>
    1.92          \<Longrightarrow> table_of (methods d) sig  = Some (mthd m)" 
    1.93 -         (is "PROP ?P C") 
    1.94 -  proof (induct ?P C rule: ws_class_induct)
    1.95 +  proof (induct rule: ws_class_induct)
    1.96      case Object
    1.97 -    fix m d
    1.98 -    assume "methd G Object sig = Some m" 
    1.99 -           "class G (declclass m) = Some d"
   1.100      with wf show "?thesis m d" by auto
   1.101    next
   1.102 -    case Subcls
   1.103 -    fix C c m d
   1.104 -    assume hyp: "PROP ?P (super c)"
   1.105 -    and      m: "methd G C sig = Some m"
   1.106 -    and  declC: "class G (declclass m) = Some d"
   1.107 -    and   clsC: "class G C = Some c"
   1.108 -    and   nObj: "C \<noteq> Object"
   1.109 +    case (Subcls C c)
   1.110      let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig"
   1.111      show "?thesis m d" 
   1.112      proof (cases "?newMethods")
   1.113        case None
   1.114 -      from None clsC nObj ws m declC
   1.115 -      show "?thesis" by (auto simp add: methd_rec) (rule hyp)
   1.116 +      from None ws Subcls
   1.117 +      show "?thesis" by (auto simp add: methd_rec) (rule Subcls)
   1.118      next
   1.119        case Some
   1.120 -      from Some clsC nObj ws m declC
   1.121 +      from Some ws Subcls
   1.122        show "?thesis" 
   1.123          by (auto simp add: methd_rec
   1.124                       dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)