src/HOL/Bali/WellForm.thy
changeset 35440 bdf8ad377877
parent 35416 d8d7d1b785af
child 37678 0040bafffdef
     1.1 --- a/src/HOL/Bali/WellForm.thy	Mon Mar 01 18:49:55 2010 +0100
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Tue Mar 02 12:26:50 2010 +0100
     1.3 @@ -730,13 +730,15 @@
     1.4   \<Longrightarrow> \<not>is_static im \<and> accmodi im = Public"
     1.5  proof -
     1.6    assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
     1.7 +
     1.8 +  note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard]
     1.9    have "wf_prog G \<longrightarrow> 
    1.10           (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
    1.11                    \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
    1.12 -  proof (rule iface_rec.induct,intro allI impI)
    1.13 +  proof (induct G I rule: iface_rec_induct', intro allI impI)
    1.14      fix G I i im
    1.15 -    assume hyp: "\<forall> J i. J \<in> set (isuperIfs i) \<and> ws_prog G \<and> iface G I = Some i
    1.16 -                 \<longrightarrow> ?P G J"
    1.17 +    assume hyp: "\<And> i J. iface G I = Some i \<Longrightarrow> ws_prog G \<Longrightarrow> J \<in> set (isuperIfs i)
    1.18 +                 \<Longrightarrow> ?P G J"
    1.19      assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 
    1.20             im: "im \<in> imethds G I sig" 
    1.21      show "\<not>is_static im \<and> accmodi im = Public" 
    1.22 @@ -1345,14 +1347,16 @@
    1.23    qed
    1.24  qed
    1.25  
    1.26 +lemmas class_rec_induct' = class_rec.induct[of "%x y z w. P x y", standard]
    1.27 +
    1.28  lemma declclass_widen[rule_format]: 
    1.29   "wf_prog G 
    1.30   \<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 
    1.31   \<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C")
    1.32 -proof (rule class_rec.induct,intro allI impI)
    1.33 +proof (induct G C rule: class_rec_induct', intro allI impI)
    1.34    fix G C c m
    1.35 -  assume Hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c 
    1.36 -               \<longrightarrow> ?P G (super c)"
    1.37 +  assume Hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object
    1.38 +               \<Longrightarrow> ?P G (super c)"
    1.39    assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
    1.40           m:  "methd G C sig = Some m"
    1.41    show "G\<turnstile>C\<preceq>\<^sub>C declclass m" 
    1.42 @@ -1976,27 +1980,6 @@
    1.43    qed
    1.44  qed
    1.45  
    1.46 -(* Tactical version *)
    1.47 -(*
    1.48 -lemma declclassD[rule_format]:
    1.49 - "wf_prog G \<longrightarrow>  
    1.50 - (\<forall> c d m. class G C = Some c \<longrightarrow> methd G C sig = Some m \<longrightarrow> 
    1.51 -  class G (declclass m) = Some d
    1.52 - \<longrightarrow> table_of (methods d) sig  = Some (mthd m))"
    1.53 -apply (rule class_rec.induct)
    1.54 -apply (rule impI)
    1.55 -apply (rule allI)+
    1.56 -apply (rule impI)
    1.57 -apply (case_tac "C=Object")
    1.58 -apply   (force simp add: methd_rec)
    1.59 -
    1.60 -apply   (subst methd_rec)
    1.61 -apply     (blast dest: wf_ws_prog)+
    1.62 -apply   (case_tac "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig")
    1.63 -apply     (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
    1.64 -done
    1.65 -*)
    1.66 -
    1.67  lemma dynmethd_Object:
    1.68    assumes statM: "methd G Object sig = Some statM" and
    1.69          private: "accmodi statM = Private" and 
    1.70 @@ -2355,9 +2338,9 @@
    1.71    have "wf_prog G  \<longrightarrow> 
    1.72             (\<forall> c m. class G C = Some c \<longrightarrow>  methd G C sig = Some m 
    1.73                     \<longrightarrow>  methd G (declclass m) sig = Some m)"      (is "?P G C") 
    1.74 -  proof (rule class_rec.induct,intro allI impI)
    1.75 +  proof (induct G C rule: class_rec_induct', intro allI impI)
    1.76      fix G C c m
    1.77 -    assume hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c \<longrightarrow>
    1.78 +    assume hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object \<Longrightarrow>
    1.79                       ?P G (super c)"
    1.80      assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
    1.81              m: "methd G C sig = Some m"