Introduced distinction wf_prog vs. ws_prog
authorstreckem
Mon May 26 18:36:15 2003 +0200 (2003-05-26)
changeset 14045a34d89ce6097
parent 14044 bbd2f7b00736
child 14046 6616e6c53d48
Introduced distinction wf_prog vs. ws_prog
src/HOL/MicroJava/BV/Altern.thy
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/MicroJava/BV/BVNoTypeError.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/BV/JType.thy
src/HOL/MicroJava/BV/JVM.thy
src/HOL/MicroJava/BV/LBVJVM.thy
src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/MicroJava/Comp/Index.thy
src/HOL/MicroJava/Comp/LemmasComp.thy
src/HOL/MicroJava/Comp/TypeInf.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/MicroJava/J/WellType.thy
     1.1 --- a/src/HOL/MicroJava/BV/Altern.thy	Mon May 26 11:42:41 2003 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Altern.thy	Mon May 26 18:36:15 2003 +0200
     1.3 @@ -1,3 +1,13 @@
     1.4 +(*  Title:      HOL/MicroJava/BV/Altern.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Martin Strecker
     1.7 +    Copyright   GPL 2003
     1.8 +*)
     1.9 +
    1.10 +
    1.11 +(* Alternative definition of well-typing of bytecode, 
    1.12 +   used in compiler type correctness proof *)
    1.13 +
    1.14  
    1.15  theory Altern = BVSpec:
    1.16  
     2.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Mon May 26 11:42:41 2003 +0200
     2.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon May 26 18:36:15 2003 +0200
     2.3 @@ -186,6 +186,7 @@
     2.4  text {*
     2.5    The program is structurally wellformed:
     2.6  *}
     2.7 +
     2.8  lemma wf_struct:
     2.9    "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
    2.10  proof -
    2.11 @@ -223,7 +224,8 @@
    2.12      apply (auto simp add: name_defs distinct_classes distinct_fields)
    2.13      done       
    2.14    ultimately
    2.15 -  show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def)
    2.16 +  show ?thesis 
    2.17 +    by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def)
    2.18  qed
    2.19  
    2.20  section "Welltypings"
     3.1 --- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Mon May 26 11:42:41 2003 +0200
     3.2 +++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Mon May 26 18:36:15 2003 +0200
     3.3 @@ -299,9 +299,10 @@
     3.4          have "\<exists>D vs. hp (the_Addr v) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C" 
     3.5            by (auto dest!: non_np_objD)
     3.6        }
     3.7 -      ultimately show ?thesis using Getfield field class stk hconf
     3.8 +      ultimately show ?thesis using Getfield field class stk hconf wf
     3.9          apply clarsimp
    3.10 -        apply (fastsimp dest!: hconfD widen_cfs_fields [OF _ _ wf] oconf_objD)
    3.11 +        apply (fastsimp intro: wf_prog_ws_prog
    3.12 +	  dest!: hconfD widen_cfs_fields oconf_objD)
    3.13          done
    3.14      next
    3.15        case (Putfield F C)
     4.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Mon May 26 11:42:41 2003 +0200
     4.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Mon May 26 18:36:15 2003 +0200
     4.3 @@ -677,6 +677,7 @@
     4.4  apply (rule conjI)
     4.5   apply (drule widen_cfs_fields)
     4.6   apply assumption+
     4.7 + apply (erule wf_prog_ws_prog)
     4.8   apply (erule conf_widen)
     4.9   prefer 2
    4.10    apply assumption
    4.11 @@ -772,7 +773,8 @@
    4.12    moreover
    4.13    from wf hp heap_ok is_class_X
    4.14    have hp': "G \<turnstile>h ?hp' \<surd>"
    4.15 -    by - (rule hconf_newref, auto simp add: oconf_def dest: fields_is_type)
    4.16 +    by - (rule hconf_newref, 
    4.17 +          auto simp add: oconf_def dest: fields_is_type)
    4.18    moreover
    4.19    from hp
    4.20    have sup: "hp \<le>| ?hp'" by (rule hext_new)
    4.21 @@ -915,7 +917,7 @@
    4.22    obtain mD'': 
    4.23      "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')"
    4.24      "is_class G D''"
    4.25 -    by (auto dest: method_in_md)
    4.26 +    by (auto dest: wf_prog_ws_prog [THEN method_in_md])
    4.27        
    4.28    from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def)
    4.29  
    4.30 @@ -1319,7 +1321,9 @@
    4.31    shows hconf_start: "\<Gamma> \<turnstile>h (start_heap \<Gamma>) \<surd>"
    4.32    apply (unfold hconf_def start_heap_def)
    4.33    apply (auto simp add: fun_upd_apply blank_def oconf_def split: split_if_asm)
    4.34 -  apply (simp add: fields_is_type [OF _ wf is_class_xcpt [OF wf]])+
    4.35 +  apply (simp add: fields_is_type 
    4.36 +          [OF _ wf [THEN wf_prog_ws_prog] 
    4.37 +	        is_class_xcpt [OF wf [THEN wf_prog_ws_prog]]])+
    4.38    done
    4.39      
    4.40  lemma 
     5.1 --- a/src/HOL/MicroJava/BV/JType.thy	Mon May 26 11:42:41 2003 +0200
     5.2 +++ b/src/HOL/MicroJava/BV/JType.thy	Mon May 26 18:36:15 2003 +0200
     5.3 @@ -51,18 +51,18 @@
     5.4    by (auto elim: widen.elims)
     5.5  
     5.6  lemma is_tyI:
     5.7 -  "\<lbrakk> is_type G T; wf_prog wf_mb G \<rbrakk> \<Longrightarrow> is_ty G T"
     5.8 +  "\<lbrakk> is_type G T; ws_prog G \<rbrakk> \<Longrightarrow> is_ty G T"
     5.9    by (auto simp add: is_ty_def intro: subcls_C_Object 
    5.10             split: ty.splits ref_ty.splits)
    5.11  
    5.12  lemma is_type_conv: 
    5.13 -  "wf_prog wf_mb G \<Longrightarrow> is_type G T = is_ty G T"
    5.14 +  "ws_prog G \<Longrightarrow> is_type G T = is_ty G T"
    5.15  proof
    5.16 -  assume "is_type G T" "wf_prog wf_mb G" 
    5.17 +  assume "is_type G T" "ws_prog G" 
    5.18    thus "is_ty G T"
    5.19      by (rule is_tyI)
    5.20  next
    5.21 -  assume wf: "wf_prog wf_mb G" and
    5.22 +  assume wf: "ws_prog G" and
    5.23           ty: "is_ty G T"
    5.24  
    5.25    show "is_type G T"
    5.26 @@ -159,7 +159,7 @@
    5.27  done 
    5.28  
    5.29  lemma closed_err_types:
    5.30 -  "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk> 
    5.31 +  "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk> 
    5.32    \<Longrightarrow> closed (err (types G)) (lift2 (sup G))"
    5.33    apply (unfold closed_def plussub_def lift2_def sup_def)
    5.34    apply (auto split: err.split)
    5.35 @@ -171,22 +171,22 @@
    5.36  
    5.37  
    5.38  lemma sup_subtype_greater:
    5.39 -  "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
    5.40 +  "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G);
    5.41        is_type G t1; is_type G t2; sup G t1 t2 = OK s \<rbrakk> 
    5.42    \<Longrightarrow> subtype G t1 s \<and> subtype G t2 s"
    5.43  proof -
    5.44 -  assume wf_prog:       "wf_prog wf_mb G"
    5.45 +  assume ws_prog:       "ws_prog G"
    5.46    assume single_valued: "single_valued (subcls1 G)" 
    5.47    assume acyclic:       "acyclic (subcls1 G)"
    5.48   
    5.49    { fix c1 c2
    5.50      assume is_class: "is_class G c1" "is_class G c2"
    5.51 -    with wf_prog 
    5.52 +    with ws_prog 
    5.53      obtain 
    5.54        "G \<turnstile> c1 \<preceq>C Object"
    5.55        "G \<turnstile> c2 \<preceq>C Object"
    5.56        by (blast intro: subcls_C_Object)
    5.57 -    with wf_prog single_valued
    5.58 +    with ws_prog single_valued
    5.59      obtain u where
    5.60        "is_lub ((subcls1 G)^* ) c1 c2 u"      
    5.61        by (blast dest: single_valued_has_lubs)
    5.62 @@ -210,24 +210,24 @@
    5.63  qed
    5.64  
    5.65  lemma sup_subtype_smallest:
    5.66 -  "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
    5.67 +  "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G);
    5.68        is_type G a; is_type G b; is_type G c; 
    5.69        subtype G a c; subtype G b c; sup G a b = OK d \<rbrakk>
    5.70    \<Longrightarrow> subtype G d c"
    5.71  proof -
    5.72 -  assume wf_prog:       "wf_prog wf_mb G"
    5.73 +  assume ws_prog:       "ws_prog G"
    5.74    assume single_valued: "single_valued (subcls1 G)" 
    5.75    assume acyclic:       "acyclic (subcls1 G)"
    5.76  
    5.77    { fix c1 c2 D
    5.78      assume is_class: "is_class G c1" "is_class G c2"
    5.79      assume le: "G \<turnstile> c1 \<preceq>C D" "G \<turnstile> c2 \<preceq>C D"
    5.80 -    from wf_prog is_class
    5.81 +    from ws_prog is_class
    5.82      obtain 
    5.83        "G \<turnstile> c1 \<preceq>C Object"
    5.84        "G \<turnstile> c2 \<preceq>C Object"
    5.85        by (blast intro: subcls_C_Object)
    5.86 -    with wf_prog single_valued
    5.87 +    with ws_prog single_valued
    5.88      obtain u where
    5.89        lub: "is_lub ((subcls1 G)^* ) c1 c2 u"
    5.90        by (blast dest: single_valued_has_lubs)   
    5.91 @@ -260,22 +260,22 @@
    5.92             split: ty.splits ref_ty.splits)
    5.93  
    5.94  lemma err_semilat_JType_esl_lemma:
    5.95 -  "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk> 
    5.96 +  "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk> 
    5.97    \<Longrightarrow> err_semilat (esl G)"
    5.98  proof -
    5.99 -  assume wf_prog:   "wf_prog wf_mb G"
   5.100 +  assume ws_prog:   "ws_prog G"
   5.101    assume single_valued: "single_valued (subcls1 G)" 
   5.102    assume acyclic:   "acyclic (subcls1 G)"
   5.103    
   5.104    hence "order (subtype G)"
   5.105      by (rule order_widen)
   5.106    moreover
   5.107 -  from wf_prog single_valued acyclic
   5.108 +  from ws_prog single_valued acyclic
   5.109    have "closed (err (types G)) (lift2 (sup G))"
   5.110      by (rule closed_err_types)
   5.111    moreover
   5.112  
   5.113 -  from wf_prog single_valued acyclic 
   5.114 +  from ws_prog single_valued acyclic 
   5.115    have
   5.116      "(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \<and> 
   5.117       (\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)"
   5.118 @@ -283,7 +283,7 @@
   5.119  
   5.120    moreover
   5.121  
   5.122 -  from wf_prog single_valued acyclic 
   5.123 +  from ws_prog single_valued acyclic 
   5.124    have
   5.125      "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). \<forall>z\<in>err (types G). 
   5.126      x <=_(le (subtype G)) z \<and> y <=_(le (subtype G)) z \<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
   5.127 @@ -297,12 +297,12 @@
   5.128  qed
   5.129  
   5.130  lemma single_valued_subcls1:
   5.131 -  "wf_prog wf_mb G \<Longrightarrow> single_valued (subcls1 G)"
   5.132 -  by (auto simp add: wf_prog_def unique_def single_valued_def
   5.133 +  "ws_prog G \<Longrightarrow> single_valued (subcls1 G)"
   5.134 +  by (auto simp add: ws_prog_def unique_def single_valued_def
   5.135      intro: subcls1I elim!: subcls1.elims)
   5.136  
   5.137  theorem err_semilat_JType_esl:
   5.138 -  "wf_prog wf_mb G \<Longrightarrow> err_semilat (esl G)"
   5.139 +  "ws_prog G \<Longrightarrow> err_semilat (esl G)"
   5.140    by (frule acyclic_subcls1, frule single_valued_subcls1, rule err_semilat_JType_esl_lemma)
   5.141  
   5.142  end
     6.1 --- a/src/HOL/MicroJava/BV/JVM.thy	Mon May 26 11:42:41 2003 +0200
     6.2 +++ b/src/HOL/MicroJava/BV/JVM.thy	Mon May 26 18:36:15 2003 +0200
     6.3 @@ -29,7 +29,6 @@
     6.4    wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"
     6.5  
     6.6  
     6.7 -
     6.8  theorem is_bcv_kiljvm:
     6.9    "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow>
    6.10        is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
    6.11 @@ -37,14 +36,15 @@
    6.12    apply (unfold kiljvm_def sl_triple_conv)
    6.13    apply (rule is_bcv_kildall)
    6.14         apply (simp (no_asm) add: sl_triple_conv [symmetric]) 
    6.15 -       apply (force intro!: semilat_JVM_slI dest: wf_acyclic simp add: symmetric sl_triple_conv)
    6.16 +       apply (force intro!: semilat_JVM_slI dest: wf_acyclic 
    6.17 +	 simp add: symmetric sl_triple_conv)
    6.18        apply (simp (no_asm) add: JVM_le_unfold)
    6.19        apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype
    6.20 -                   dest: wf_subcls1 wf_acyclic) 
    6.21 +                   dest: wf_subcls1 wf_acyclic wf_prog_ws_prog)
    6.22       apply (simp add: JVM_le_unfold)
    6.23      apply (erule exec_pres_type)
    6.24     apply assumption
    6.25 -  apply (erule exec_mono, assumption)  
    6.26 +  apply (drule wf_prog_ws_prog, erule exec_mono, assumption)  
    6.27    done
    6.28  
    6.29  lemma subset_replicate: "set (replicate n x) \<subseteq> {x}"
     7.1 --- a/src/HOL/MicroJava/BV/LBVJVM.thy	Mon May 26 11:42:41 2003 +0200
     7.2 +++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Mon May 26 18:36:15 2003 +0200
     7.3 @@ -86,7 +86,8 @@
     7.4    let ?f    = "JVMType.sup G mxs mxr"
     7.5    let ?A    = "states G mxs mxr"
     7.6  
     7.7 -  have "semilat (JVMType.sl G mxs mxr)" by (rule semilat_JVM_slI)
     7.8 +  have "semilat (JVMType.sl G mxs mxr)" 
     7.9 +    by (rule semilat_JVM_slI, rule wf_prog_ws_prog)
    7.10    hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
    7.11    moreover
    7.12    have "top ?r Err"  by (simp add: JVM_le_unfold)
    7.13 @@ -217,7 +218,8 @@
    7.14      app_eff:    "wt_app_eff (sup_state_opt G) ?app ?eff phi"
    7.15      by (simp (asm_lr) add: wt_method_def2)
    7.16    
    7.17 -  have "semilat (JVMType.sl G mxs ?mxr)" by (rule semilat_JVM_slI)
    7.18 +  have "semilat (JVMType.sl G mxs ?mxr)" 
    7.19 +    by (rule semilat_JVM_slI, rule wf_prog_ws_prog)
    7.20    hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
    7.21    moreover
    7.22    have "top ?r Err"  by (simp add: JVM_le_unfold)
    7.23 @@ -234,7 +236,8 @@
    7.24      by (clarsimp simp add: exec_def) 
    7.25         (intro bounded_lift check_bounded_is_bounded)
    7.26    with wf
    7.27 -  have "mono ?r ?step (length ins) ?A" by (rule exec_mono)
    7.28 +  have "mono ?r ?step (length ins) ?A"
    7.29 +    by (rule wf_prog_ws_prog [THEN exec_mono])
    7.30    hence "mono ?r ?step (length ?phi) ?A" by (simp add: length)
    7.31    moreover
    7.32    have "pres_type ?step (length ins) ?A" by (rule exec_pres_type)
     8.1 --- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Mon May 26 11:42:41 2003 +0200
     8.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Mon May 26 18:36:15 2003 +0200
     8.3 @@ -239,11 +239,11 @@
     8.4    done
     8.5  
     8.6  lemma order_sup_state_opt:
     8.7 -  "wf_prog wf_mb G \<Longrightarrow> order (sup_state_opt G)"
     8.8 +  "ws_prog G \<Longrightarrow> order (sup_state_opt G)"
     8.9    by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
    8.10  
    8.11  theorem exec_mono:
    8.12 -  "wf_prog wf_mb G \<Longrightarrow> bounded (exec G maxs rT et bs) (size bs) \<Longrightarrow>
    8.13 +  "ws_prog G \<Longrightarrow> bounded (exec G maxs rT et bs) (size bs) \<Longrightarrow>
    8.14    mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"  
    8.15    apply (unfold exec_def JVM_le_unfold JVM_states_unfold)  
    8.16    apply (rule mono_lift)
    8.17 @@ -257,7 +257,7 @@
    8.18    done
    8.19  
    8.20  theorem semilat_JVM_slI:
    8.21 -  "wf_prog wf_mb G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
    8.22 +  "ws_prog G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
    8.23    apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
    8.24    apply (rule semilat_opt)
    8.25    apply (rule err_semilat_Product_esl)
    8.26 @@ -287,7 +287,7 @@
    8.27           "(C,S,fs,mdecls) \<in> set G"
    8.28           "((mn,pTs),rT,code) \<in> set mdecls"
    8.29    hence "wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
    8.30 -    by (unfold wf_prog_def wf_cdecl_def) auto  
    8.31 +    by (rule wf_prog_wf_mdecl)
    8.32    hence "\<forall>t \<in> set pTs. is_type G t" 
    8.33      by (unfold wf_mdecl_def wf_mhead_def) auto
    8.34    moreover
    8.35 @@ -319,11 +319,10 @@
    8.36      apply (unfold wf_prog_def wf_cdecl_def)
    8.37      apply clarsimp
    8.38      apply (drule bspec, assumption)
    8.39 -    apply (unfold wf_mdecl_def)
    8.40 +    apply (unfold wf_cdecl_mdecl_def)
    8.41      apply clarsimp
    8.42      apply (drule bspec, assumption)
    8.43 -    apply clarsimp
    8.44 -    apply (frule methd [OF wf], assumption+)
    8.45 +    apply (frule methd [OF wf [THEN wf_prog_ws_prog]], assumption+)
    8.46      apply (frule is_type_pTs [OF wf], assumption+)
    8.47      apply clarify
    8.48      apply (drule rule [OF wf], assumption+)
     9.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Mon May 26 11:42:41 2003 +0200
     9.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Mon May 26 18:36:15 2003 +0200
     9.3 @@ -8,7 +8,7 @@
     9.4  
     9.5  theory CorrComp =  JTypeSafe + LemmasComp:
     9.6  
     9.7 -
     9.8 +declare wf_prog_ws_prog [simp add]
     9.9  
    9.10  (* If no exception is present after evaluation/execution, 
    9.11    none can have been present before *)
    9.12 @@ -278,28 +278,27 @@
    9.13  (**********************************************************************)
    9.14  
    9.15  
    9.16 -(* ### to be moved to one of the J/* files *)
    9.17 -
    9.18  lemma method_preserves [rule_format (no_asm)]:
    9.19    "\<lbrakk> wf_prog wf_mb G; is_class G C; 
    9.20    \<forall> S rT mb. \<forall> cn \<in> fst ` set G. wf_mdecl wf_mb G cn (S,rT,mb)  \<longrightarrow> (P cn S (rT,mb))\<rbrakk>
    9.21   \<Longrightarrow> \<forall> D. 
    9.22    method (G, C) S = Some (D, rT, mb) \<longrightarrow> (P D S (rT,mb))"
    9.23  
    9.24 -apply (frule WellForm.wf_subcls1)
    9.25 +apply (frule wf_prog_ws_prog [THEN wf_subcls1])
    9.26  apply (rule subcls1_induct, assumption, assumption)
    9.27  
    9.28  apply (intro strip)
    9.29  apply ((drule spec)+, drule_tac x="Object" in bspec)
    9.30 -apply (simp add: wf_prog_def wf_syscls_def)
    9.31 +apply (simp add: wf_prog_def ws_prog_def wf_syscls_def)
    9.32  apply (subgoal_tac "D=Object") apply simp
    9.33  apply (drule mp)
    9.34  apply (frule_tac C=Object in method_wf_mdecl)
    9.35 - apply simp apply assumption apply simp apply assumption apply simp
    9.36 + apply simp
    9.37 + apply assumption apply simp apply assumption apply simp
    9.38  
    9.39  apply (subst method_rec) apply simp
    9.40  apply force
    9.41 -apply assumption
    9.42 +apply simp
    9.43  apply (simp only: map_add_def)
    9.44  apply (split option.split)
    9.45  apply (rule conjI)
    9.46 @@ -332,14 +331,6 @@
    9.47  
    9.48  (**********************************************************************)
    9.49  
    9.50 -(* required for lemma wtpd_expr_call *)
    9.51 -lemma ty_exprs_length [simp]: "(E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts)"
    9.52 -apply (subgoal_tac "(E\<turnstile>e::T \<longrightarrow> True) \<and> (E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts) \<and> (E\<turnstile>s\<surd> \<longrightarrow> True)")
    9.53 -apply blast
    9.54 -apply (rule ty_expr_ty_exprs_wt_stmt.induct)
    9.55 -apply auto
    9.56 -done
    9.57 -
    9.58  constdefs wtpd_expr :: "java_mb env \<Rightarrow> expr \<Rightarrow> bool"
    9.59    "wtpd_expr E e == (\<exists> T. E\<turnstile>e :: T)"
    9.60    wtpd_exprs :: "java_mb env \<Rightarrow> (expr list) \<Rightarrow> bool"
    9.61 @@ -573,73 +564,43 @@
    9.62  
    9.63  
    9.64  
    9.65 -
    9.66 -
    9.67 -
    9.68 -
    9.69 -
    9.70  (**********************************************************************)
    9.71  
    9.72 -constdefs
    9.73 -  state_ok :: "java_mb env \<Rightarrow> xstate \<Rightarrow> bool"
    9.74 -  "state_ok E xs == xs::\<preceq>E"
    9.75 -
    9.76 -
    9.77 -lemma state_ok_eval: "\<lbrakk>state_ok E xs; wf_java_prog (prg E); wtpd_expr E e;
    9.78 -  (prg E)\<turnstile>xs -e\<succ>v -> xs'\<rbrakk> \<Longrightarrow>  state_ok E xs'"
    9.79 -apply (simp only: state_ok_def wtpd_expr_def)
    9.80 +lemma state_ok_eval: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_expr E e;
    9.81 +  (prg E)\<turnstile>xs -e\<succ>v -> xs'\<rbrakk> \<Longrightarrow>  xs'::\<preceq>E"
    9.82 +apply (simp only: wtpd_expr_def)
    9.83  apply (erule exE)
    9.84 -apply (case_tac xs', case_tac xs, simp only:)
    9.85 -apply (rule eval_type_sound [THEN conjunct1])
    9.86 -apply (rule HOL.refl)
    9.87 -apply assumption
    9.88 -apply (subgoal_tac "fst E \<turnstile> (gx xs, gs xs) -e\<succ>v-> (gx xs', gs xs')")
    9.89 -apply assumption
    9.90 -apply (auto simp: gx_def gs_def)
    9.91 +apply (case_tac xs', case_tac xs)
    9.92 +apply (auto intro: eval_type_sound [THEN conjunct1])
    9.93  done
    9.94  
    9.95 -(* to be moved into JTypeSafe.thy *)
    9.96 -lemma evals_type_sound: "!!E s s'.  
    9.97 -  [| G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); G=prg E; wf_java_prog G; (x,s)::\<preceq>E; E\<turnstile>es[::]Ts |]  
    9.98 -  ==> (x',s')::\<preceq>E \<and> (x'=None --> list_all2 (conf G (heap s')) vs Ts)"
    9.99 -apply( simp (no_asm_simp) only: split_tupled_all)
   9.100 -apply (drule eval_evals_exec_type_sound 
   9.101 -             [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp])
   9.102 -apply auto
   9.103 +lemma state_ok_evals: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_exprs E es;
   9.104 +  (xs,es,vs,xs') \<in> Eval.evals (prg E)\<rbrakk> \<Longrightarrow> xs'::\<preceq>E"
   9.105 +apply (simp only: wtpd_exprs_def)
   9.106 +apply (erule exE)
   9.107 +apply (case_tac xs) apply (case_tac xs')
   9.108 +apply (auto intro: evals_type_sound [THEN conjunct1])
   9.109  done
   9.110  
   9.111 -lemma state_ok_evals: "\<lbrakk>state_ok E xs; wf_java_prog (prg E); wtpd_exprs E es;
   9.112 -  (xs,es,vs,xs') \<in> Eval.evals (prg E)\<rbrakk> \<Longrightarrow>  state_ok E xs'"
   9.113 -apply (simp only: state_ok_def wtpd_exprs_def)
   9.114 -apply (erule exE)
   9.115 -apply (case_tac xs) apply (case_tac xs') apply (simp only:)
   9.116 -apply (rule evals_type_sound [THEN conjunct1])
   9.117 -apply (auto simp: gx_def gs_def)
   9.118 -done
   9.119 -
   9.120 -lemma state_ok_exec: "\<lbrakk>state_ok E xs; wf_java_prog (prg E); wtpd_stmt E st;
   9.121 -  (xs,st,xs') \<in> Eval.exec (prg E)\<rbrakk> \<Longrightarrow>  state_ok E xs'"
   9.122 -apply (simp only: state_ok_def wtpd_stmt_def)
   9.123 -apply (case_tac xs', case_tac xs, simp only:)
   9.124 -apply (rule exec_type_sound)
   9.125 -apply (rule HOL.refl)
   9.126 -apply assumption
   9.127 -apply (subgoal_tac "((gx xs, gs xs), st, (gx xs', gs xs')) \<in> Eval.exec (fst E)")
   9.128 -apply assumption
   9.129 -apply (auto simp: gx_def gs_def)
   9.130 +lemma state_ok_exec: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_stmt E st;
   9.131 +  (xs,st,xs') \<in> Eval.exec (prg E)\<rbrakk> \<Longrightarrow>  xs'::\<preceq>E"
   9.132 +apply (simp only: wtpd_stmt_def)
   9.133 +apply (case_tac xs', case_tac xs)
   9.134 +apply (auto intro: exec_type_sound)
   9.135  done
   9.136  
   9.137  
   9.138  lemma state_ok_init: 
   9.139 -  "\<lbrakk> wf_java_prog G; state_ok (env_of_jmb G C S) (x, h, l); 
   9.140 +  "\<lbrakk> wf_java_prog G; (x, h, l)::\<preceq>(env_of_jmb G C S); 
   9.141    is_class G dynT;
   9.142    method (G, dynT) (mn, pTs) = Some (md, rT, pns, lvars, blk, res);
   9.143    list_all2 (conf G h) pvs pTs; G,h \<turnstile> a' ::\<preceq> Class md\<rbrakk>
   9.144  \<Longrightarrow>
   9.145 -state_ok (env_of_jmb G md (mn, pTs)) (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))"
   9.146 +(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs))"
   9.147 +apply (frule wf_prog_ws_prog)
   9.148  apply (frule method_in_md [THEN conjunct2], assumption+)
   9.149  apply (frule method_yields_wf_java_mdecl, assumption, assumption)
   9.150 -apply (simp add: state_ok_def env_of_jmb_def gs_def conforms_def split_beta)
   9.151 +apply (simp add: env_of_jmb_def gs_def conforms_def split_beta)
   9.152  apply (simp add: wf_java_mdecl_def)
   9.153  apply (rule conjI)
   9.154  apply (rule lconf_ext)
   9.155 @@ -675,7 +636,7 @@
   9.156  done
   9.157  
   9.158  
   9.159 -lemma class_expr_is_class: "\<lbrakk>E \<turnstile> e :: Class C; wf_prog wf_mb (prg E)\<rbrakk> 
   9.160 +lemma class_expr_is_class: "\<lbrakk>E \<turnstile> e :: Class C; ws_prog (prg E)\<rbrakk> 
   9.161    \<Longrightarrow> is_class (prg E) C"
   9.162  by (case_tac E, auto dest: ty_expr_is_type)
   9.163  
   9.164 @@ -685,7 +646,7 @@
   9.165  by (blast dest: singleton_in_set max_spec2appl_meths appl_methsD)
   9.166  
   9.167  
   9.168 -lemma eval_conf: "\<lbrakk>G \<turnstile> s -e\<succ>v-> s'; wf_java_prog G; state_ok E s;
   9.169 +lemma eval_conf: "\<lbrakk>G \<turnstile> s -e\<succ>v-> s'; wf_java_prog G; s::\<preceq>E;
   9.170    E\<turnstile>e::T; gx s' = None; prg E = G \<rbrakk> 
   9.171    \<Longrightarrow> G,gh s'\<turnstile>v::\<preceq>T"
   9.172  apply (simp add: gh_def)
   9.173 @@ -694,15 +655,13 @@
   9.174  apply (rule sym) apply assumption
   9.175  apply assumption
   9.176  apply (simp (no_asm_use) add: surjective_pairing [THEN sym])
   9.177 -apply (simp only: state_ok_def gs_def)
   9.178 -apply (case_tac s, simp)
   9.179 -apply assumption
   9.180 -apply (simp add: gx_def)
   9.181 +apply (simp only: surjective_pairing [THEN sym])
   9.182 +apply (auto simp add: gs_def gx_def)
   9.183  done
   9.184  
   9.185  lemma evals_preserves_conf:
   9.186    "\<lbrakk> G\<turnstile> s -es[\<succ>]vs-> s'; G,gh s \<turnstile> t ::\<preceq> T; E \<turnstile>es[::]Ts;
   9.187 -  wf_java_prog G; state_ok E s; 
   9.188 +  wf_java_prog G; s::\<preceq>E; 
   9.189    prg E = G \<rbrakk> \<Longrightarrow> G,gh s' \<turnstile> t ::\<preceq> T"
   9.190  apply (subgoal_tac "gh s\<le>| gh s'")
   9.191  apply (frule conf_hext, assumption, assumption)
   9.192 @@ -711,15 +670,14 @@
   9.193  apply assumption
   9.194  apply (simp add: gx_def gh_def gl_def surjective_pairing [THEN sym])
   9.195  apply (case_tac E)
   9.196 -apply (simp add: gx_def gs_def gh_def gl_def state_ok_def
   9.197 -  surjective_pairing [THEN sym])
   9.198 +apply (simp add: gx_def gs_def gh_def gl_def surjective_pairing [THEN sym])
   9.199  done
   9.200  
   9.201  lemma eval_of_class: "\<lbrakk> G \<turnstile> s -e\<succ>a'-> s'; E \<turnstile> e :: Class C; 
   9.202 -  wf_java_prog G; state_ok E s; gx s'=None; a' \<noteq> Null; G=prg E\<rbrakk>
   9.203 +  wf_java_prog G; s::\<preceq>E; gx s'=None; a' \<noteq> Null; G=prg E\<rbrakk>
   9.204    \<Longrightarrow> (\<exists> lc. a' = Addr lc)"
   9.205  apply (case_tac s, case_tac s', simp)
   9.206 -apply (frule eval_type_sound, (simp add: state_ok_def gs_def)+)
   9.207 +apply (frule eval_type_sound, (simp add: gs_def)+)
   9.208  apply (case_tac a')
   9.209  apply (auto simp: conf_def)
   9.210  done
   9.211 @@ -727,9 +685,10 @@
   9.212  
   9.213  lemma dynT_subcls: 
   9.214    "\<lbrakk> a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; dynT = fst (the (h (the_Addr a')));
   9.215 -  is_class G dynT; wf_prog wf_mb G \<rbrakk> \<Longrightarrow> G\<turnstile>dynT \<preceq>C C"
   9.216 +  is_class G dynT; ws_prog G \<rbrakk> \<Longrightarrow> G\<turnstile>dynT \<preceq>C C"
   9.217  apply (case_tac "C = Object")
   9.218  apply (simp, rule subcls_C_Object, assumption+)
   9.219 +apply simp
   9.220  apply (frule non_np_objD, auto)
   9.221  done
   9.222  
   9.223 @@ -746,7 +705,7 @@
   9.224  apply ((erule exE)+, (erule conjE)+, (erule exE)+)
   9.225  apply (drule widen_methd)
   9.226  apply assumption
   9.227 -apply (rule dynT_subcls, assumption+, simp, assumption+)
   9.228 +apply (rule dynT_subcls) apply assumption+ apply simp apply simp
   9.229  apply (erule exE)+ apply simp
   9.230  done
   9.231  
   9.232 @@ -764,7 +723,7 @@
   9.233    (\<forall> os CL S.
   9.234    (class_sig_defined G CL S) \<longrightarrow> 
   9.235    (wtpd_expr (env_of_jmb G CL S) ex) \<longrightarrow>
   9.236 -  (state_ok (env_of_jmb G CL S) xs) \<longrightarrow>
   9.237 +  (xs ::\<preceq> (env_of_jmb G CL S)) \<longrightarrow>
   9.238    ( {TranslComp.comp G, CL, S} \<turnstile>
   9.239      {gh xs, os, (locvars_xstate G CL S xs)}
   9.240      >- (compExpr (gmb G CL S) ex) \<rightarrow>
   9.241 @@ -775,7 +734,7 @@
   9.242    (\<forall> os CL S.
   9.243    (class_sig_defined G CL S) \<longrightarrow> 
   9.244    (wtpd_exprs (env_of_jmb G CL S) exs) \<longrightarrow>
   9.245 -  (state_ok (env_of_jmb G CL S) xs) \<longrightarrow>
   9.246 +  (xs::\<preceq>(env_of_jmb G CL S)) \<longrightarrow>
   9.247    ( {TranslComp.comp G, CL, S} \<turnstile>
   9.248      {gh xs, os, (locvars_xstate G CL S xs)}
   9.249      >- (compExprs (gmb G CL S) exs) \<rightarrow>
   9.250 @@ -786,7 +745,7 @@
   9.251    (\<forall> os CL S.
   9.252    (class_sig_defined G CL S) \<longrightarrow> 
   9.253    (wtpd_stmt (env_of_jmb G CL S) st) \<longrightarrow>
   9.254 -  (state_ok (env_of_jmb G CL S) xs) \<longrightarrow>
   9.255 +  (xs::\<preceq>(env_of_jmb G CL S)) \<longrightarrow>
   9.256    ( {TranslComp.comp G, CL, S} \<turnstile>
   9.257      {gh xs, os, (locvars_xstate G CL S xs)}
   9.258      >- (compStmt (gmb G CL S) st) \<rightarrow>
   9.259 @@ -797,8 +756,8 @@
   9.260  apply simp
   9.261  
   9.262  (* case NewC *) 
   9.263 -apply clarify
   9.264 -apply (frule wf_subcls1) (* establish  wf ((subcls1 G)^-1) *)
   9.265 +apply clarify 
   9.266 +apply (frule wf_prog_ws_prog [THEN wf_subcls1]) (* establish  wf ((subcls1 G)^-1) *)
   9.267  apply (simp add: c_hupd_hp_invariant)
   9.268  apply (rule progression_one_step)
   9.269  apply (rotate_tac 1, drule sym) (* reverse equation (a, None) = new_Addr (fst s) *)
   9.270 @@ -828,7 +787,7 @@
   9.271  apply (intro allI impI)
   9.272  apply (frule_tac xs=s1 in eval_xcpt, assumption) (* establish (gx s1 = None) *)
   9.273  apply (frule wtpd_expr_binop)
   9.274 -(* establish (state_ok \<dots> s1) *)
   9.275 +(* establish (s1::\<preceq> \<dots>) *)
   9.276  apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp)) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) 
   9.277  
   9.278  
   9.279 @@ -896,8 +855,9 @@
   9.280  apply (simp only: gx_conv, simp only: gx_conv, frule np_NoneD, erule conjE)
   9.281  
   9.282  
   9.283 -  (* establish (state_ok \<dots> (Norm s1)) *)
   9.284 -apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) 
   9.285 +  (* establish ((Norm s1)::\<preceq> \<dots>) *)
   9.286 +apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) 
   9.287 +   apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) 
   9.288  
   9.289  apply (simp only: compExpr_compExprs.simps)
   9.290  
   9.291 @@ -936,7 +896,7 @@
   9.292  apply (intro allI impI)
   9.293  apply (frule_tac xs=s1 in evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *)
   9.294  apply (frule wtpd_exprs_cons)
   9.295 -   (* establish (state_ok \<dots> (Norm s0)) *)
   9.296 +   (* establish ((Norm s0)::\<preceq> \<dots>) *)
   9.297  apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
   9.298  
   9.299  apply simp
   9.300 @@ -967,7 +927,7 @@
   9.301  apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
   9.302  apply (frule wtpd_stmt_comp)
   9.303  
   9.304 -  (* establish (state_ok \<dots>  s1) *)
   9.305 +  (* establish (s1::\<preceq> \<dots>) *)
   9.306  apply (frule_tac st=c1 in state_ok_exec) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
   9.307  
   9.308  apply simp
   9.309 @@ -980,7 +940,7 @@
   9.310  apply (intro allI impI)
   9.311  apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
   9.312  apply (frule wtpd_stmt_cond, (erule conjE)+)
   9.313 -(* establish (state_ok \<dots> s1) *)
   9.314 +(* establish (s1::\<preceq> \<dots>) *)
   9.315  apply (frule_tac e=e in state_ok_eval) 
   9.316  apply (simp (no_asm_simp) only: env_of_jmb_fst)
   9.317  apply assumption 
   9.318 @@ -1053,9 +1013,9 @@
   9.319  apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
   9.320  apply (frule wtpd_stmt_loop, (erule conjE)+)
   9.321  
   9.322 -(* establish (state_ok \<dots> s1) *)
   9.323 +(* establish (s1::\<preceq> \<dots>) *)
   9.324  apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
   9.325 -(* establish (state_ok \<dots> s2) *)
   9.326 +(* establish (s2::\<preceq> \<dots>) *)
   9.327  apply (frule_tac xs=s1 and st=c in state_ok_exec)
   9.328  apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
   9.329  
   9.330 @@ -1094,7 +1054,7 @@
   9.331  apply blast
   9.332  
   9.333  (*****)
   9.334 -(* case method call *) defer (* !!! NEWC *)
   9.335 +(* case method call *)
   9.336  
   9.337  apply (intro allI impI)
   9.338  
   9.339 @@ -1107,11 +1067,11 @@
   9.340  
   9.341  (* assumptions about state_ok and is_class *)
   9.342  
   9.343 -(* establish state_ok (env_of_jmb G CL S) s1 *)
   9.344 +(* establish s1::\<preceq> (env_of_jmb G CL S) *)
   9.345  apply (frule_tac xs="Norm s0" and e=e in state_ok_eval)
   9.346  apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp (no_asm_use) only: env_of_jmb_fst)
   9.347  
   9.348 -(* establish state_ok (env_of_jmb G CL S) (x, h, l) *)
   9.349 +(* establish (x, h, l)::\<preceq>(env_of_jmb G CL S) *)
   9.350  apply (frule_tac xs=s1 and xs'="(x, h, l)" in state_ok_evals)
   9.351  apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp only: env_of_jmb_fst)
   9.352  
   9.353 @@ -1130,7 +1090,7 @@
   9.354  apply (subgoal_tac " method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res)")
   9.355  apply (subgoal_tac "list_all2 (conf G h) pvs pTs")
   9.356  
   9.357 -(* establish state_ok (env_of_jmb G md (mn, pTs)) (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a')) *)
   9.358 +(* establish (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs)) *)
   9.359  apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class dynT")
   9.360  apply (frule (2) conf_widen)
   9.361  apply (frule state_ok_init, assumption+)
   9.362 @@ -1138,16 +1098,14 @@
   9.363  apply (subgoal_tac "class_sig_defined G md (mn, pTs)")
   9.364  apply (frule wtpd_blk, assumption, assumption)
   9.365  apply (frule wtpd_res, assumption, assumption)
   9.366 -apply (subgoal_tac "state_ok (env_of_jmb G md (mn, pTs)) s3")
   9.367 +apply (subgoal_tac "s3::\<preceq>(env_of_jmb G md (mn, pTs))")
   9.368  
   9.369 -(* establish method (TranslComp.comp G, md) (mn, pTs) =
   9.370 -          Some (md, rT, compMethod (pns, lvars, blk, res)) *)
   9.371 -apply (frule_tac C=md and D=md in comp_method, assumption, assumption)
   9.372 -
   9.373 -(* establish
   9.374 -   method (TranslComp.comp G, dynT) (mn, pTs) =
   9.375 -          Some (md, rT, compMethod (pns, lvars, blk, res)) *)
   9.376 - apply (frule_tac C=dynT and D=md in comp_method, assumption, assumption)
   9.377 +apply (subgoal_tac "method (TranslComp.comp G, md) (mn, pTs) =
   9.378 +          Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))")
   9.379 +prefer 2 apply (simp add: wf_prog_ws_prog [THEN comp_method])
   9.380 +apply (subgoal_tac "method (TranslComp.comp G, dynT) (mn, pTs) =
   9.381 +          Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))")
   9.382 +prefer 2 apply (simp add: wf_prog_ws_prog [THEN comp_method])
   9.383   apply (simp only: fst_conv snd_conv)
   9.384  
   9.385  (* establish length pns = length pTs *)
   9.386 @@ -1209,7 +1167,7 @@
   9.387  apply (simp (no_asm_simp))
   9.388  apply (simp (no_asm_simp))
   9.389  
   9.390 -(* show state_ok \<dots> s3 *)
   9.391 +(* show s3::\<preceq>\<dots> *)
   9.392  apply (rule_tac xs = "(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))" and st=blk in state_ok_exec)
   9.393  apply assumption apply (simp (no_asm_simp) only: env_of_jmb_fst) 
   9.394  apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
   9.395 @@ -1231,7 +1189,7 @@
   9.396  apply (subgoal_tac "((gx s1, gs s1), ps, pvs, x, h, l) \<in> evals G")
   9.397  apply (frule_tac E="env_of_jmb G CL S" in evals_type_sound)
   9.398  apply (simp only: env_of_jmb_fst) 
   9.399 -apply assumption apply (simp only: state_ok_def)
   9.400 +apply assumption
   9.401  apply (simp add: conforms_def xconf_def gs_def)
   9.402  apply simp
   9.403  apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym])
   9.404 @@ -1242,14 +1200,14 @@
   9.405  
   9.406  
   9.407  (* show method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res) *)
   9.408 -apply (frule method_in_md [THEN conjunct2], assumption+)
   9.409 +apply (frule wf_prog_ws_prog [THEN method_in_md [THEN conjunct2]], assumption+)
   9.410  
   9.411    (* show G\<turnstile>Class dynT \<preceq> Class md *)
   9.412  apply (simp (no_asm_use) only: widen_Class_Class)
   9.413  apply (rule method_wf_mdecl [THEN conjunct1], assumption+)
   9.414  
   9.415    (* is_class G md *)
   9.416 -apply (rule method_in_md [THEN conjunct1], assumption+)
   9.417 +apply (rule wf_prog_ws_prog [THEN method_in_md [THEN conjunct1]], assumption+)
   9.418  
   9.419    (* show is_class G dynT *)
   9.420  apply (frule non_npD) apply assumption
   9.421 @@ -1257,6 +1215,7 @@
   9.422  apply simp
   9.423  apply (rule subcls_is_class2) apply assumption
   9.424  apply (frule class_expr_is_class) apply (simp only: env_of_jmb_fst)
   9.425 +apply (rule wf_prog_ws_prog, assumption)
   9.426  apply (simp only: env_of_jmb_fst)
   9.427  
   9.428   (* show G,h \<turnstile> a' ::\<preceq> Class C *)
   9.429 @@ -1280,7 +1239,7 @@
   9.430        >- (compExpr (gmb G C S) ex) \<rightarrow> 
   9.431      {hp', val#os, (locvars_locals G C S loc')}"
   9.432  apply (frule compiler_correctness [THEN conjunct1])
   9.433 -apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def state_ok_def)
   9.434 +apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def)
   9.435  done
   9.436  
   9.437  theorem compiler_correctness_exec: "
   9.438 @@ -1294,7 +1253,7 @@
   9.439        >- (compStmt (gmb G C S) st) \<rightarrow>
   9.440      {hp', os, (locvars_locals G C S loc')}"
   9.441  apply (frule compiler_correctness [THEN conjunct2 [THEN conjunct2]])
   9.442 -apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def state_ok_def)
   9.443 +apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def)
   9.444  done
   9.445  
   9.446  (**********************************************************************)
   9.447 @@ -1306,4 +1265,6 @@
   9.448  simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   9.449  *}
   9.450  
   9.451 +declare wf_prog_ws_prog [simp del]
   9.452 +
   9.453  end
    10.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon May 26 11:42:41 2003 +0200
    10.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon May 26 18:36:15 2003 +0200
    10.3 @@ -4,8 +4,7 @@
    10.4      Copyright   GPL 2002
    10.5  *)
    10.6  
    10.7 -theory CorrCompTp =  LemmasComp + JVM + TypeInf + NatCanonify + Altern:
    10.8 -
    10.9 +theory CorrCompTp =  LemmasComp + JVM + TypeInf + Altern:
   10.10  
   10.11  declare split_paired_All [simp del]
   10.12  declare split_paired_Ex [simp del]
   10.13 @@ -27,7 +26,7 @@
   10.14  by (simp add: local_env_def split_beta)
   10.15  
   10.16  
   10.17 -lemma wt_class_expr_is_class: "\<lbrakk> wf_prog wf_mb G; E \<turnstile> expr :: Class cname;
   10.18 +lemma wt_class_expr_is_class: "\<lbrakk> ws_prog G; E \<turnstile> expr :: Class cname;
   10.19    E = local_env G C (mn, pTs) pns lvars\<rbrakk>
   10.20    \<Longrightarrow> is_class G cname "
   10.21  apply (subgoal_tac "((fst E), (snd E)) \<turnstile> expr :: Class cname")
   10.22 @@ -308,7 +307,7 @@
   10.23    (* show is_class G cname \<and> field (G, cname) vname = Some (cname, T) *)
   10.24    apply (rule field_in_fd) apply assumption+
   10.25    (* show is_class G Ca *)
   10.26 -  apply (rule wt_class_expr_is_class, assumption+, rule HOL.refl)
   10.27 +  apply (fast intro: wt_class_expr_is_class)
   10.28  
   10.29  (* FAss *)
   10.30  apply (intro strip)
   10.31 @@ -485,8 +484,8 @@
   10.32  lemma states_mono: "\<lbrakk> mxs \<le> mxs' \<rbrakk>
   10.33    \<Longrightarrow> states G mxs mxr \<subseteq> states G mxs' mxr"
   10.34  apply (simp add: states_def JVMType.sl_def)
   10.35 -apply (simp add: Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def
   10.36 -  JType.esl_def)
   10.37 +apply (simp add: Product.esl_def stk_esl_def reg_sl_def 
   10.38 +  upto_esl_def Listn.sl_def Err.sl_def  JType.esl_def)
   10.39  apply (simp add: Err.esl_def Err.le_def Listn.le_def)
   10.40  apply (simp add: Product.le_def Product.sup_def Err.sup_def)
   10.41  apply (simp add: Opt.esl_def Listn.sup_def)
   10.42 @@ -528,14 +527,12 @@
   10.43  apply (induct i)
   10.44  apply simp+
   10.45    (* case Goto *)
   10.46 -apply (simp only: nat_canonify)
   10.47 -apply simp
   10.48 +apply arith
   10.49    (* case Ifcmpeq *)
   10.50  apply simp
   10.51  apply (erule disjE)
   10.52 -apply simp
   10.53 -apply (simp only: nat_canonify)
   10.54 -apply simp
   10.55 +apply arith
   10.56 +apply arith
   10.57    (* case Throw *)
   10.58  apply simp
   10.59  done
   10.60 @@ -547,14 +544,12 @@
   10.61  apply (induct i)
   10.62  apply simp+
   10.63    (* case Goto *)
   10.64 -apply (simp only: nat_canonify)
   10.65 -apply simp
   10.66 +apply arith
   10.67    (* case Ifcmpeq *)
   10.68  apply simp
   10.69  apply (erule disjE)
   10.70  apply simp
   10.71 -apply (simp only: nat_canonify)
   10.72 -apply simp
   10.73 +apply arith
   10.74    (* case Throw *)
   10.75  apply simp
   10.76  done
   10.77 @@ -1255,33 +1250,35 @@
   10.78    \<Longrightarrow> bc_mt_corresp [Getfield vname cname] 
   10.79          (replST (Suc 0) (snd (the (field (G, cname) vname))))
   10.80          (Class C # ST, LT) (comp G) rT mxr (Suc 0)"
   10.81 -  apply (frule wf_subcls1)
   10.82 +  apply (frule wf_prog_ws_prog [THEN wf_subcls1])
   10.83    apply (frule field_in_fd, assumption+)
   10.84    apply (frule widen_field, assumption+)
   10.85    apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
   10.86 -  apply (simp add: comp_field [THEN sym] comp_subcls1 [THEN sym] comp_widen [THEN sym] comp_is_class [THEN sym])
   10.87 +  apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
   10.88    apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
   10.89    apply (intro strip)
   10.90  apply (simp add: check_type_simps)
   10.91  apply clarify
   10.92  apply (rule_tac x="Suc (length ST)" in exI)
   10.93  apply simp+
   10.94 -apply (simp only: comp_is_type [THEN sym])
   10.95 +apply (simp only: comp_is_type)
   10.96  apply (rule_tac C=cname in fields_is_type)
   10.97  apply (simp add: field_def)
   10.98  apply (drule JBasis.table_of_remap_SomeD)+
   10.99  apply assumption+
  10.100 +apply (erule wf_prog_ws_prog)
  10.101 +apply assumption
  10.102  done
  10.103  
  10.104  lemma bc_mt_corresp_Putfield: "\<lbrakk> wf_prog wf_mb G; 
  10.105    field (G, C) vname = Some (cname, Ta); G \<turnstile> T \<preceq> Ta; is_class G C \<rbrakk>
  10.106    \<Longrightarrow> bc_mt_corresp [Putfield vname cname] (popST 2) (T # Class C # T # ST, LT)
  10.107             (comp G) rT mxr (Suc 0)"
  10.108 -  apply (frule wf_subcls1)
  10.109 +  apply (frule wf_prog_ws_prog [THEN wf_subcls1])
  10.110    apply (frule field_in_fd, assumption+)
  10.111    apply (frule widen_field, assumption+)
  10.112    apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
  10.113 -  apply (simp add: comp_field [THEN sym] comp_subcls1 [THEN sym] comp_widen [THEN sym] comp_is_class [THEN sym])
  10.114 +  apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
  10.115    apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
  10.116  
  10.117    apply (intro strip)
  10.118 @@ -1302,13 +1299,13 @@
  10.119    apply (simp add: comp_is_class)
  10.120    apply (rule_tac x=pTsa in exI)
  10.121    apply (rule_tac x="Class cname" in exI)
  10.122 -  apply (simp add: max_spec_preserves_length comp_is_class [THEN sym])
  10.123 +  apply (simp add: max_spec_preserves_length comp_is_class)
  10.124    apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
  10.125 -  apply (simp add: comp_widen list_all2_def)
  10.126 +  apply (simp add: split_paired_all comp_widen list_all2_def)
  10.127    apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
  10.128    apply (rule exI)+
  10.129 -  apply (rule comp_method)
  10.130 -  apply assumption+
  10.131 +  apply (simp add: wf_prog_ws_prog [THEN comp_method])
  10.132 +  apply auto
  10.133    done
  10.134  
  10.135  
  10.136 @@ -1329,7 +1326,7 @@
  10.137  
  10.138    -- {* @{text "<=s"} *}
  10.139    apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
  10.140 -  apply (frule comp_method, assumption+)
  10.141 +  apply (simp add: wf_prog_ws_prog [THEN comp_method])
  10.142    apply (simp add: max_spec_preserves_length [THEN sym])
  10.143  
  10.144    -- "@{text check_type}"
  10.145 @@ -1341,7 +1338,7 @@
  10.146  apply clarify
  10.147  apply (rule_tac x="Suc (length ST)" in exI)
  10.148  apply simp+
  10.149 -apply (simp only: comp_is_type [THEN sym])
  10.150 +apply (simp only: comp_is_type)
  10.151  apply (frule method_wf_mdecl) apply assumption apply assumption
  10.152  apply (simp add: wf_mdecl_def wf_mhead_def)
  10.153  apply (simp add: max_def)
  10.154 @@ -1714,6 +1711,7 @@
  10.155  apply (simp (no_asm_simp), rule bc_mt_corresp_Checkcast)
  10.156  apply (simp add: comp_is_class)
  10.157  apply (simp only: compTpExpr_LT_ST)
  10.158 +apply (drule cast_RefT)
  10.159  apply blast
  10.160  apply (simp add: start_sttp_resp_def)
  10.161  
  10.162 @@ -1885,7 +1883,7 @@
  10.163  apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast) 
  10.164    apply (simp (no_asm_simp))
  10.165    apply (rule bc_mt_corresp_Getfield) apply assumption+
  10.166 -     apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl)
  10.167 +     apply (fast intro: wt_class_expr_is_class)
  10.168  apply (simp (no_asm_simp) add: start_sttp_resp_def)
  10.169  
  10.170  
  10.171 @@ -1905,7 +1903,7 @@
  10.172  apply (rule bc_mt_corresp_Dup_x1)
  10.173    apply (simp (no_asm_simp) add: dup_x1ST_def)
  10.174  apply (rule bc_mt_corresp_Putfield) apply assumption+
  10.175 -     apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl)
  10.176 +     apply (fast intro: wt_class_expr_is_class)
  10.177  apply (simp (no_asm_simp) add: start_sttp_resp_def)
  10.178  apply (simp (no_asm_simp) add: start_sttp_resp_def)
  10.179  apply (simp (no_asm_simp) add: start_sttp_resp_def)
  10.180 @@ -1922,7 +1920,7 @@
  10.181    apply (simp only: compTpExprs_LT_ST)
  10.182    apply (simp (no_asm_simp))
  10.183  apply (rule bc_mt_corresp_Invoke) apply assumption+
  10.184 -  apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl)
  10.185 +     apply (fast intro: wt_class_expr_is_class)
  10.186  apply (simp (no_asm_simp) add: start_sttp_resp_def)
  10.187  apply (rule start_sttp_resp_comb) 
  10.188    apply (simp (no_asm_simp))
  10.189 @@ -2247,14 +2245,13 @@
  10.190    apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+ 
  10.191    apply (intro strip)
  10.192    apply (rule wt_instr_Goto)
  10.193 -  apply (simp (no_asm_simp) add: nat_canonify)
  10.194 -  apply (simp (no_asm_simp) add: nat_canonify)
  10.195 +  apply arith
  10.196 +  apply arith
  10.197      (* \<dots> ! nat (int pc + i) = \<dots> ! pc *)
  10.198 -  apply (simp (no_asm_simp) add: nat_canonify)
  10.199 +  apply (simp (no_asm_simp))
  10.200    apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
  10.201    apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
  10.202    apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
  10.203 -  apply (simp (no_asm_simp) only: int_outside_right nat_int)
  10.204    apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
  10.205    apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
  10.206    apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
  10.207 @@ -2592,52 +2589,56 @@
  10.208  apply (simp only: split_paired_All, simp)
  10.209  
  10.210    (* subgoal is_class / wf_mhead / wf_java_mdecl *)
  10.211 -apply (rule methd [THEN conjunct2]) apply assumption+ apply (simp only:)
  10.212 -apply (rule wf_prog_wf_mhead, assumption+) apply (simp only:)
  10.213 +apply (blast intro: methd [THEN conjunct2])
  10.214 +apply (frule wf_prog_wf_mdecl, assumption+) apply (simp only:) apply (simp add: wf_mdecl_def)
  10.215  apply (rule wf_java_prog_wf_java_mdecl, assumption+)
  10.216 -
  10.217  done
  10.218  
  10.219  
  10.220 -  (**********************************************************************************)
  10.221 -
  10.222 -
  10.223 -
  10.224  lemma comp_set_ms: "(C, D, fs, cms)\<in>set (comp G) 
  10.225    \<Longrightarrow> \<exists> ms. (C, D, fs, ms) \<in>set G   \<and> cms = map (compMethod G C) ms"
  10.226  by (auto simp: comp_def compClass_def)
  10.227  
  10.228 -lemma method_body_source: "\<lbrakk> wf_prog wf_mb G; is_class G C;  method (comp G, C) sig = Some (D, rT, cmb) \<rbrakk>  
  10.229 -  \<Longrightarrow>  (\<exists> mb. method (G, C) sig = Some (D, rT, mb))"
  10.230 -apply (simp add: comp_method_eq comp_method_result_def)
  10.231 -apply (case_tac "method (G, C) sig")
  10.232 -apply auto
  10.233 -done
  10.234 +
  10.235 +  (* ---------------------------------------------------------------------- *)
  10.236  
  10.237  section "Main Theorem"
  10.238    (* MAIN THEOREM: 
  10.239    Methodtype computed by comp is correct for bytecode generated by compTp *)
  10.240  theorem wt_prog_comp: "wf_java_prog G  \<Longrightarrow> wt_jvm_prog (comp G) (compTp G)"
  10.241  apply (simp add: wf_prog_def)
  10.242 +
  10.243  apply (subgoal_tac "wf_java_prog G") prefer 2 apply (simp add: wf_prog_def)
  10.244  apply (simp (no_asm_simp) add: wf_prog_def wt_jvm_prog_def)
  10.245 -apply (simp add:  comp_unique comp_wf_syscls wf_cdecl_def)
  10.246 +apply (simp add: comp_ws_prog)
  10.247 +
  10.248 +apply (intro strip)
  10.249 +apply (subgoal_tac "\<exists> C D fs cms. c = (C, D, fs, cms)")
  10.250  apply clarify
  10.251  apply (frule comp_set_ms)
  10.252  apply clarify
  10.253  apply (drule bspec, assumption)
  10.254 -apply (simp add: comp_wf_fdecl)
  10.255 -apply (simp add: wf_mdecl_def)
  10.256 -
  10.257  apply (rule conjI)
  10.258 -apply (rule ballI)
  10.259 -apply (subgoal_tac "\<exists> sig rT mb. x = (sig, rT, mb)") prefer 2 apply (case_tac x, simp)
  10.260 +
  10.261 +  (* wf_mrT *)
  10.262 +apply (case_tac "C = Object")
  10.263 +apply (simp add: wf_mrT_def)
  10.264 +apply (subgoal_tac "is_class G D")
  10.265 +apply (simp add: comp_wf_mrT)
  10.266 +apply (simp add: wf_prog_def ws_prog_def ws_cdecl_def)
  10.267 +apply blast
  10.268 +
  10.269 +  (* wf_cdecl_mdecl *)
  10.270 +apply (simp add: wf_cdecl_mdecl_def)
  10.271 +apply (simp add: split_beta)
  10.272 +apply (intro strip)
  10.273 +
  10.274 +  (* show wt_method \<dots> *)
  10.275 +apply (subgoal_tac "\<exists> sig rT mb. x = (sig, rT, mb)") 
  10.276  apply (erule exE)+
  10.277  apply (simp (no_asm_simp) add: compMethod_def split_beta)
  10.278  apply (erule conjE)+
  10.279  apply (drule_tac x="(sig, rT, mb)" in bspec) apply simp
  10.280 -apply (rule conjI)
  10.281 -apply (simp add: comp_wf_mhead)
  10.282  apply (rule_tac mn="fst sig" and pTs="snd sig" in wt_method_comp)
  10.283    apply assumption+
  10.284    apply simp
  10.285 @@ -2647,27 +2648,11 @@
  10.286  apply simp
  10.287  apply simp
  10.288  apply (simp add: compMethod_def split_beta)
  10.289 -
  10.290 -apply (rule conjI)
  10.291 -apply (rule unique_map_fst [THEN iffD1]) 
  10.292 -  apply (simp (no_asm_simp) add: compMethod_def split_beta) apply simp
  10.293 -
  10.294 -apply clarify
  10.295 -apply (rule conjI) apply (simp add: comp_is_class)
  10.296 -apply (rule conjI) apply (simp add: comp_subcls)
  10.297 -apply (simp add: compMethod_def split_beta)
  10.298 -apply (intro strip) 
  10.299 -  apply (drule_tac x=x in bspec, assumption, drule_tac x="D'" in spec, drule_tac x="rT'" in spec)
  10.300 -  apply (erule exE)
  10.301 -
  10.302 -apply (frule method_body_source) apply assumption+
  10.303 -apply (drule mp, assumption)
  10.304 -apply (simp add: comp_widen)
  10.305 +apply auto
  10.306  done
  10.307  
  10.308  
  10.309  
  10.310 -
  10.311    (**********************************************************************************)
  10.312  
  10.313  declare split_paired_All [simp add]
    11.1 --- a/src/HOL/MicroJava/Comp/Index.thy	Mon May 26 11:42:41 2003 +0200
    11.2 +++ b/src/HOL/MicroJava/Comp/Index.thy	Mon May 26 18:36:15 2003 +0200
    11.3 @@ -63,6 +63,10 @@
    11.4  apply simp
    11.5  done
    11.6  
    11.7 +lemma lift_if: "(f (if b then t else e)) = (if b then (f t) else (f e))"
    11.8 +apply auto
    11.9 +done
   11.10 +
   11.11  lemma update_at_index: "
   11.12    \<lbrakk> distinct (gjmb_plns (gmb G C S)); 
   11.13    x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow> 
    12.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Mon May 26 11:42:41 2003 +0200
    12.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Mon May 26 18:36:15 2003 +0200
    12.3 @@ -8,9 +8,16 @@
    12.4  
    12.5  theory LemmasComp = TranslComp:
    12.6  
    12.7 +
    12.8 +declare split_paired_All [simp del]
    12.9 +declare split_paired_Ex [simp del]
   12.10 +
   12.11 +
   12.12  (**********************************************************************)
   12.13  (* misc lemmas *)
   12.14  
   12.15 +
   12.16 +
   12.17  lemma split_pairs: "(\<lambda>(a,b). (F a b)) (ab) = F (fst ab) (snd ab)"
   12.18  proof -
   12.19    have "(\<lambda>(a,b). (F a b)) (fst ab,snd ab) = F (fst ab) (snd ab)"
   12.20 @@ -34,6 +41,44 @@
   12.21  by (case_tac st, simp add: c_hupd_conv gh_def)
   12.22  
   12.23  
   12.24 +lemma unique_map_fst [rule_format]: "(\<forall> x \<in> set xs. (fst x = fst (f x) )) \<longrightarrow>
   12.25 +  unique (map f xs) = unique xs"
   12.26 +proof (induct xs)
   12.27 +  case Nil show ?case by simp
   12.28 +next
   12.29 +  case (Cons a list)
   12.30 +  show ?case
   12.31 +  proof
   12.32 +    assume fst_eq: "\<forall>x\<in>set (a # list). fst x = fst (f x)"
   12.33 +
   12.34 +    have fst_set: "(fst a \<in> fst ` set list) = (fst (f a) \<in> fst ` f ` set list)" 
   12.35 +    proof 
   12.36 +      assume as: "fst a \<in> fst ` set list" 
   12.37 +      then obtain x where fst_a_x: "x\<in>set list \<and> fst a = fst x" 
   12.38 +	by (auto simp add: image_iff)
   12.39 +      then have "fst (f a) = fst (f x)" by (simp add: fst_eq)
   12.40 +      with as show "(fst (f a) \<in> fst ` f ` set list)" by (simp add: fst_a_x)
   12.41 +    next
   12.42 +      assume as: "fst (f a) \<in> fst ` f ` set list"
   12.43 +      then obtain x where fst_a_x: "x\<in>set list \<and> fst (f a) = fst (f x)"
   12.44 +	by (auto simp add: image_iff)
   12.45 +      then have "fst a = fst x" by (simp add: fst_eq)
   12.46 +      with as show "fst a \<in> fst ` set list" by (simp add: fst_a_x)
   12.47 +    qed
   12.48 +
   12.49 +    with fst_eq Cons 
   12.50 +    show "unique (map f (a # list)) = unique (a # list)"
   12.51 +      by (simp add: unique_def fst_set)
   12.52 +  qed
   12.53 +qed
   12.54 +
   12.55 +lemma comp_unique: "unique (comp G) = unique G"
   12.56 +apply (simp add: comp_def)
   12.57 +apply (rule unique_map_fst)
   12.58 +apply (simp add: compClass_def split_beta)
   12.59 +done
   12.60 +
   12.61 +
   12.62  (**********************************************************************)
   12.63  (* invariance of properties under compilation *)
   12.64  
   12.65 @@ -53,75 +98,96 @@
   12.66  apply (simp add: image_compose [THEN sym] o_def split_beta del: image_compose)
   12.67  done
   12.68  
   12.69 -lemma comp_is_class: "is_class G C = is_class (comp G) C"
   12.70 +lemma comp_is_class: "is_class (comp G) C = is_class G C"
   12.71  by (case_tac "class G C", auto simp: is_class_def comp_class_None dest: comp_class_imp)
   12.72  
   12.73  
   12.74 -lemma comp_is_type: "is_type G T = is_type (comp G) T"
   12.75 +lemma comp_is_type: "is_type (comp G) T = is_type G T"
   12.76    by ((cases T),simp,(induct G)) ((simp),(simp only: comp_is_class),(simp add: comp_is_class),(simp only: comp_is_class))
   12.77  
   12.78 -lemma SIGMA_cong: "\<lbrakk> A = B; !!x. x \<in> B \<Longrightarrow> C x = D x \<rbrakk> \<Longrightarrow> (\<Sigma> x \<in> A. C x) = (\<Sigma> x \<in> B. D x)"
   12.79 +lemma SIGMA_cong: "\<lbrakk> A = B; !!x. x \<in> B \<Longrightarrow> C x = D x \<rbrakk> 
   12.80 +  \<Longrightarrow> (\<Sigma> x \<in> A. C x) = (\<Sigma> x \<in> B. D x)"
   12.81  by auto
   12.82  
   12.83 -lemma comp_classname: "is_class G C \<Longrightarrow> fst (the (class G C)) = fst (the (class (comp G) C))"
   12.84 +lemma comp_classname: "is_class G C 
   12.85 +  \<Longrightarrow> fst (the (class G C)) = fst (the (class (comp G) C))"
   12.86  by (case_tac "class G C", auto simp: is_class_def dest: comp_class_imp)
   12.87  
   12.88  
   12.89 -lemma comp_subcls1: "subcls1 G = subcls1 (comp G)"
   12.90 +lemma comp_subcls1: "subcls1 (comp G) = subcls1 G"
   12.91  apply (simp add: subcls1_def2 comp_is_class)
   12.92  apply (rule SIGMA_cong, simp)
   12.93 -apply (simp add: comp_is_class [THEN sym])
   12.94 +apply (simp add: comp_is_class)
   12.95  apply (simp add: comp_classname)
   12.96  done
   12.97  
   12.98 -lemma comp_subcls: "(subcls1 G)^* = (subcls1 (comp G))^*"
   12.99 -  by (induct G) (simp_all add: comp_def comp_subcls1)
  12.100 -
  12.101 -lemma comp_widen: "((ty1,ty2) \<in> widen G) = ((ty1,ty2) \<in> widen (comp G))"
  12.102 +lemma comp_widen: "((ty1,ty2) \<in> widen (comp G)) = ((ty1,ty2) \<in> widen G)"
  12.103    apply rule
  12.104 +  apply (cases "(ty1,ty2)" "comp G" rule: widen.cases) 
  12.105 +  apply (simp_all add: comp_subcls1 widen.null)
  12.106    apply (cases "(ty1,ty2)" G rule: widen.cases) 
  12.107 -  apply (simp_all add: comp_subcls widen.null)
  12.108 -  apply (cases "(ty1,ty2)" "comp G" rule: widen.cases) 
  12.109 -  apply (simp_all add: comp_subcls widen.null)
  12.110 +  apply (simp_all add: comp_subcls1 widen.null)
  12.111    done
  12.112  
  12.113 -lemma comp_cast: "((ty1,ty2) \<in> cast G) = ((ty1,ty2) \<in> cast (comp G))"
  12.114 +lemma comp_cast: "((ty1,ty2) \<in> cast (comp G)) = ((ty1,ty2) \<in> cast G)"
  12.115    apply rule
  12.116 +  apply (cases "(ty1,ty2)" "comp G" rule: cast.cases) 
  12.117 +  apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
  12.118 +  apply (rule cast.widen) apply (simp add: comp_widen)
  12.119    apply (cases "(ty1,ty2)" G rule: cast.cases)
  12.120 -  apply (simp_all add: comp_subcls cast.widen cast.subcls)
  12.121 -  apply (cases "(ty1,ty2)" "comp G" rule: cast.cases) 
  12.122 -  apply (simp_all add: comp_subcls cast.widen cast.subcls)
  12.123 +  apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
  12.124 +  apply (rule cast.widen) apply (simp add: comp_widen)
  12.125    done
  12.126  
  12.127 -lemma comp_cast_ok: "cast_ok G = cast_ok (comp G)"
  12.128 +lemma comp_cast_ok: "cast_ok (comp G) = cast_ok G"
  12.129    by (simp add: expand_fun_eq cast_ok_def comp_widen)
  12.130  
  12.131  
  12.132 -lemma comp_wf_fdecl: "wf_fdecl G fd  \<Longrightarrow> wf_fdecl (comp G) fd"
  12.133 -apply (case_tac fd)
  12.134 -apply (simp add: wf_fdecl_def comp_is_type)
  12.135 +lemma compClass_fst [simp]: "(fst (compClass G C)) = (fst C)"
  12.136 +by (simp add: compClass_def split_beta)
  12.137 +
  12.138 +lemma compClass_fst_snd [simp]: "(fst (snd (compClass G C))) = (fst (snd C))"
  12.139 +by (simp add: compClass_def split_beta)
  12.140 +
  12.141 +lemma compClass_fst_snd_snd [simp]: "(fst (snd (snd (compClass G C)))) = (fst (snd (snd C)))"
  12.142 +by (simp add: compClass_def split_beta)
  12.143 +
  12.144 +lemma comp_wf_fdecl [simp]: "wf_fdecl (comp G) fd = wf_fdecl G fd"
  12.145 +by (case_tac fd, simp add: wf_fdecl_def comp_is_type)
  12.146 +
  12.147 +
  12.148 +lemma compClass_forall [simp]: "
  12.149 +  (\<forall>x\<in>set (snd (snd (snd (compClass G C)))). P (fst x) (fst (snd x))) =
  12.150 +  (\<forall>x\<in>set (snd (snd (snd C))). P (fst x) (fst (snd x)))"
  12.151 +by (simp add: compClass_def compMethod_def split_beta)
  12.152 +
  12.153 +lemma comp_wf_mhead: "wf_mhead (comp G) S rT =  wf_mhead G S rT"
  12.154 +by (simp add: wf_mhead_def split_beta comp_is_type)
  12.155 +
  12.156 +lemma comp_ws_cdecl: "
  12.157 +  ws_cdecl (TranslComp.comp G) (compClass G C) = ws_cdecl G C"
  12.158 +apply (simp add: ws_cdecl_def split_beta comp_is_class comp_subcls1)
  12.159 +apply (simp (no_asm_simp) add: comp_wf_mhead)
  12.160 +apply (simp add: compClass_def compMethod_def split_beta unique_map_fst)
  12.161  done
  12.162  
  12.163 -lemma comp_wf_syscls: "wf_syscls G = wf_syscls (comp G)"
  12.164 +
  12.165 +lemma comp_wf_syscls: "wf_syscls (comp G) = wf_syscls G"
  12.166  apply (simp add: wf_syscls_def comp_def compClass_def split_beta)
  12.167  apply (simp only: image_compose [THEN sym])
  12.168 -apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls). (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
  12.169 -(*
  12.170 -apply (subgoal_tac "(fst o (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls). (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
  12.171 -*)
  12.172 +apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
  12.173 +  (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
  12.174  apply (simp del: image_compose)
  12.175  apply (simp add: expand_fun_eq split_beta)
  12.176  done
  12.177  
  12.178  
  12.179 -lemma comp_wf_mhead: "wf_mhead G S rT =  wf_mhead (comp G) S rT"
  12.180 -by (simp add: wf_mhead_def split_beta comp_is_type)
  12.181 -
  12.182 -lemma comp_wf_mdecl: "\<lbrakk> wf_mdecl wf_mb G C jmdl;
  12.183 -  (wf_mb G C jmdl) \<longrightarrow> (wf_mb_comp (comp G) C (compMethod G C jmdl)) \<rbrakk> 
  12.184 - \<Longrightarrow> 
  12.185 -  wf_mdecl wf_mb_comp (comp G) C (compMethod G C jmdl)"
  12.186 -by (simp add: wf_mdecl_def wf_mhead_def comp_is_type split_beta compMethod_def)
  12.187 +lemma comp_ws_prog: "ws_prog (comp G) = ws_prog G"
  12.188 +apply (rule sym)
  12.189 +apply (simp add: ws_prog_def comp_ws_cdecl comp_unique)
  12.190 +apply (simp add: comp_wf_syscls)
  12.191 +apply (auto simp add: comp_ws_cdecl [THEN sym] TranslComp.comp_def)
  12.192 +done
  12.193  
  12.194  
  12.195  lemma comp_class_rec: " wf ((subcls1 G)^-1) \<Longrightarrow> 
  12.196 @@ -159,16 +225,16 @@
  12.197  done
  12.198  
  12.199  lemma comp_fields: "wf ((subcls1 G)^-1) \<Longrightarrow> 
  12.200 -  fields (G,C) = fields (comp G,C)" 
  12.201 +  fields (comp G,C) = fields (G,C)" 
  12.202  by (simp add: fields_def comp_class_rec)
  12.203  
  12.204  lemma comp_field: "wf ((subcls1 G)^-1) \<Longrightarrow> 
  12.205 -  field (G,C) = field (comp G,C)" 
  12.206 +  field (comp G,C) = field (G,C)" 
  12.207  by (simp add: field_def comp_fields)
  12.208  
  12.209  
  12.210  
  12.211 -lemma class_rec_relation [rule_format (no_asm)]: "\<lbrakk>  wf_prog wf_mb G;
  12.212 +lemma class_rec_relation [rule_format (no_asm)]: "\<lbrakk>  ws_prog G;
  12.213    \<forall> fs ms. R (f1 Object fs ms t1) (f2 Object fs ms t2);
  12.214     \<forall> C fs ms r1 r2. (R r1 r2) \<longrightarrow> (R (f1 C fs ms r1) (f2 C fs ms r2)) \<rbrakk>
  12.215    \<Longrightarrow> ((class G C) \<noteq> None) \<longrightarrow> 
  12.216 @@ -194,10 +260,11 @@
  12.217  
  12.218    (* subgoals *)
  12.219  
  12.220 -apply (frule class_wf) apply assumption
  12.221 -apply (simp add: wf_cdecl_def is_class_def)
  12.222 +apply (frule class_wf_struct) apply assumption
  12.223 +apply (simp add: ws_cdecl_def is_class_def)
  12.224  
  12.225  apply (simp add: subcls1_def2 is_class_def)
  12.226 +apply auto
  12.227  done
  12.228  
  12.229  
  12.230 @@ -206,189 +273,114 @@
  12.231  translations
  12.232    "mtd_mb" => "Fun.comp snd snd"
  12.233  
  12.234 -
  12.235 -lemma map_of_map_fst: "\<lbrakk> map_of (map f xs) k = Some e; inj f;
  12.236 +lemma map_of_map_fst: "\<lbrakk> inj f;
  12.237    \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
  12.238 -  \<Longrightarrow>  map_of (map g xs) k = Some (snd (g ((inv f) (k, e))))"
  12.239 +  \<Longrightarrow>  map_of (map g xs) k 
  12.240 +  = option_map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
  12.241  apply (induct xs)
  12.242  apply simp
  12.243  apply (simp del: split_paired_All)
  12.244  apply (case_tac "k = fst a")
  12.245  apply (simp del: split_paired_All)
  12.246 -apply (subgoal_tac "(fst a, e)  = f a")
  12.247 +apply (subgoal_tac "(inv f (fst a, snd (f a))) = a", simp)
  12.248 +apply (subgoal_tac "(fst a, snd (f a)) = f a", simp)
  12.249 +apply (erule conjE)+
  12.250 +apply (drule_tac s ="fst (f a)" and t="fst a" in sym)
  12.251  apply simp
  12.252 -apply (rule_tac s= "(fst (f a), snd (f a))" in trans)
  12.253 -apply simp
  12.254 -apply (rule surjective_pairing [THEN sym])
  12.255 -apply (simp del: split_paired_All)
  12.256 +apply (simp add: surjective_pairing)
  12.257  done
  12.258  
  12.259  
  12.260 -lemma comp_method [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk> \<Longrightarrow> 
  12.261 -  (method (G, C) S) = Some (D, rT, mb) \<longrightarrow> 
  12.262 -  (method (comp G, C) S) = Some (D, rT, mtd_mb (compMethod G D (S, rT, mb)))"
  12.263 +lemma comp_method [rule_format (no_asm)]: "\<lbrakk> ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> 
  12.264 +  ((method (comp G, C) S) = 
  12.265 +  option_map (\<lambda> (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
  12.266 +             (method (G, C) S))"
  12.267  apply (simp add: method_def)
  12.268  apply (frule wf_subcls1)
  12.269  apply (simp add: comp_class_rec)
  12.270  apply (simp add: map_compose [THEN sym] split_iter split_compose del: map_compose)
  12.271 -apply (rule_tac R="%x y. (x S) = Some (D, rT, mb) \<longrightarrow> (y S) = Some (D, rT, snd (snd (compMethod G D (S, rT, mb))))" in  class_rec_relation) apply assumption
  12.272 +apply (rule_tac R="%x y. ((x S) = (option_map (\<lambda>(D, rT, b). 
  12.273 +  (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))" 
  12.274 +  in class_rec_relation)
  12.275 +apply assumption
  12.276  
  12.277  apply (intro strip)
  12.278  apply simp
  12.279  
  12.280 -apply (frule_tac f="(\<lambda>(s, m). (s, Object, m))" 
  12.281 -  and g="(Fun.comp (\<lambda>(s, m). (s, Object, m)) (compMethod G Object))" in map_of_map_fst)
  12.282 -(*
  12.283 -apply (frule_tac f="(\<lambda>(s, m). (s, Object, m))" 
  12.284 -  and g="((\<lambda>(s, m). (s, Object, m)) \<circ> compMethod G Object)" in map_of_map_fst)
  12.285 -*)
  12.286 -apply (simp add: inj_on_def)
  12.287 +apply (rule trans)
  12.288 +
  12.289 +apply (rule_tac f="(\<lambda>(s, m). (s, Object, m))" and
  12.290 +  g="(Fun.comp (\<lambda>(s, m). (s, Object, m)) (compMethod G Object))" 
  12.291 +  in map_of_map_fst)
  12.292 +defer				(* inj \<dots> *)
  12.293 +apply (simp add: inj_on_def split_beta) 
  12.294  apply (simp add: split_beta compMethod_def)
  12.295 -apply (simp add: split_beta compMethod_def)
  12.296 +apply (simp add: map_of_map [THEN sym])
  12.297 +apply (simp add: split_beta)
  12.298 +apply (simp add: map_compose [THEN sym] Fun.comp_def split_beta)
  12.299 +apply (subgoal_tac "(\<lambda>x\<Colon>(vname list \<times> fdecl list \<times> stmt \<times> expr) mdecl.
  12.300 +                    (fst x, Object,
  12.301 +                     snd (compMethod G Object
  12.302 +                           (inv (\<lambda>(s\<Colon>sig, m\<Colon>ty \<times> vname list \<times> fdecl list \<times> stmt \<times> expr).
  12.303 +                                    (s, Object, m))
  12.304 +                             (S, Object, snd x)))))
  12.305 +  = (\<lambda>x. (fst x, Object, fst (snd x),
  12.306 +                        snd (snd (compMethod G Object (S, snd x)))))")
  12.307  apply (simp only:)
  12.308 -apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, D, rT, mb)) = (S, rT, mb)")
  12.309 +apply (simp add: expand_fun_eq)
  12.310 +apply (intro strip)
  12.311 +apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)")
  12.312  apply (simp only:)
  12.313  apply (simp add: compMethod_def split_beta)
  12.314 -apply (simp add: map_of_map) apply (erule exE)+ apply simp
  12.315 -apply (simp add: map_of_map) apply (erule exE)+ apply simp
  12.316 -apply (rule inv_f_eq) apply (simp add: inj_on_def) apply simp
  12.317 +apply (rule inv_f_eq) 
  12.318 +defer
  12.319 +defer
  12.320  
  12.321  apply (intro strip)
  12.322  apply (simp add: map_add_Some_iff map_of_map del: split_paired_Ex)
  12.323 +apply (simp add: map_add_def)
  12.324 +apply (subgoal_tac "inj (\<lambda>(s, m). (s, Ca, m))")
  12.325 +apply (drule_tac g="(Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca))" and xs=ms
  12.326 +  and k=S in map_of_map_fst) 
  12.327 +apply (simp add: split_beta) 
  12.328 +apply (simp add: compMethod_def split_beta)
  12.329 +apply (case_tac "(map_of (map (\<lambda>(s, m). (s, Ca, m)) ms) S)")
  12.330 +apply simp
  12.331 +apply simp apply (simp add: split_beta map_of_map) apply (erule exE) apply (erule conjE)+
  12.332 +apply (drule_tac t=a in sym)
  12.333 +apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Ca, m)) (S, a)) = (S, snd a)")
  12.334 +apply simp
  12.335  apply (subgoal_tac "\<forall>x\<in>set ms. fst ((Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x")
  12.336 -(*
  12.337 -apply (subgoal_tac "\<forall>x\<in>set ms. fst (((\<lambda>(s, m). (s, Ca, m)) \<circ> compMethod G Ca) x) = fst x")
  12.338 -*)
  12.339 -apply (erule disjE)
  12.340 -apply (rule disjI1)
  12.341 +   prefer 2 apply (simp (no_asm_simp) add: compMethod_def split_beta)
  12.342  apply (simp add: map_of_map2)
  12.343  apply (simp (no_asm_simp) add: compMethod_def split_beta)
  12.344  
  12.345 -apply (rule disjI2)
  12.346 -apply (simp add: map_of_map2)
  12.347 -
  12.348 -  -- "subgoal"
  12.349 -apply (simp (no_asm_simp) add: compMethod_def split_beta)
  12.350 -
  12.351 -apply (simp add: is_class_def)
  12.352 +  -- "remaining subgoals"
  12.353 +apply (auto intro: inv_f_eq simp add: inj_on_def is_class_def)
  12.354  done
  12.355  
  12.356  
  12.357 -constdefs comp_method_result :: "java_mb prog \<Rightarrow> sig \<Rightarrow> 
  12.358 -  (cname \<times> ty \<times> java_mb) option \<Rightarrow> (cname \<times> ty \<times> jvm_method) option"
  12.359 -  "comp_method_result G S m ==  case m of 
  12.360 -    None \<Rightarrow> None
  12.361 -  | Some (D, rT, mb) \<Rightarrow> Some (D, rT, mtd_mb (compMethod G D (S, rT, mb)))"
  12.362  
  12.363 -
  12.364 -lemma map_of_map_compMethod: "map_of (map (\<lambda>(s, m). (s, C, m)) (map (compMethod G C) ms)) S =
  12.365 -          (case map_of (map (\<lambda>(s, m). (s, C, m)) ms) S of None \<Rightarrow> None
  12.366 -           | Some (D, rT, mb) \<Rightarrow> Some (D, rT, mtd_mb (compMethod G D (S, rT, mb))))"
  12.367 -apply (induct ms)
  12.368 -apply simp
  12.369 -apply (simp only: map_compose [THEN sym])
  12.370 -apply (simp add: o_def split_beta del: map.simps)
  12.371 -apply (simp (no_asm_simp) only: map.simps map_of.simps)
  12.372 -apply (simp add: compMethod_def split_beta)
  12.373 -done
  12.374 -
  12.375 -  (* the following is more expressive than comp_method and should replace it *)
  12.376 -lemma comp_method_eq [rule_format (no_asm)]: "wf_prog wf_mb G \<Longrightarrow> is_class G C \<longrightarrow>
  12.377 -method (comp G, C) S = comp_method_result G S (method (G,C) S)"
  12.378 -apply (subgoal_tac "wf ((subcls1 G)^-1)") prefer 2 apply (rule wf_subcls1, assumption) 
  12.379 -
  12.380 -apply (rule subcls_induct)
  12.381 -apply assumption
  12.382 -apply (intro strip)
  12.383 -apply (subgoal_tac "\<exists> D fs ms. class G C = Some (D, fs, ms)") 
  12.384 -   prefer 2 apply (simp add: is_class_def)
  12.385 -apply (erule exE)+
  12.386 -
  12.387 -apply (case_tac "C = Object")
  12.388 -
  12.389 -  (* C = Object *)
  12.390 -apply (subst method_rec_lemma) apply assumption+ apply simp 
  12.391 -apply (subst method_rec_lemma) apply (frule comp_class_imp) apply assumption+ 
  12.392 -   apply (simp add: comp_subcls1) 
  12.393 -apply (simp add: comp_method_result_def)
  12.394 -apply (rule map_of_map_compMethod) 
  12.395 -
  12.396 -  (* C \<noteq> Object *)
  12.397 -apply (subgoal_tac "(C, D) \<in> (subcls1 G)\<^sup>+") 
  12.398 -   prefer 2 apply (frule subcls1I, assumption+) apply blast
  12.399 -apply (subgoal_tac "is_class G D")
  12.400 -apply (drule spec, drule mp, assumption, drule mp, assumption)
  12.401 -apply (frule wf_subcls1) 
  12.402 -apply (subgoal_tac "wf ((subcls1 (comp G))\<inverse>)")
  12.403 -apply (frule_tac G=G in method_rec_lemma, assumption)
  12.404 -apply (frule comp_class_imp)
  12.405 -apply (frule_tac G="comp G" in method_rec_lemma, assumption)
  12.406 -apply (simp only:)
  12.407 -apply (simp (no_asm_simp) add: comp_method_result_def expand_fun_eq)
  12.408 -
  12.409 -apply (case_tac "(method (G, D) ++  map_of (map (\<lambda>(s, m). (s, C, m)) ms)) S")
  12.410 -
  12.411 -  (* case None *)
  12.412 -apply (simp (no_asm_simp) add: map_add_None)
  12.413 -apply (simp add: map_of_map_compMethod comp_method_result_def) 
  12.414 -
  12.415 -  (* case Some *)
  12.416 -apply (simp add: map_add_Some_iff)
  12.417 -apply (erule disjE)
  12.418 -  apply (simp add: split_beta map_of_map_compMethod)
  12.419 -  apply (simp add: map_add_def comp_method_result_def map_of_map_compMethod)
  12.420 -
  12.421 -  (* show subgoals *)
  12.422 -apply (simp add: comp_subcls1) 
  12.423 -  (* show is_class G D *)
  12.424 -apply (simp add: wf_prog_def wf_cdecl_def)
  12.425 -apply (subgoal_tac "(C, D, fs, ms)\<in>set G")
  12.426 -apply blast
  12.427 -apply (simp add: class_def map_of_SomeD)
  12.428 -done
  12.429 -
  12.430 -  (* ### this proof is horrid and has to be redone *)
  12.431 -lemma unique_map_fst [rule_format]: "(\<forall> x \<in> set xs. (fst x = fst (f x) )) \<longrightarrow>
  12.432 -  unique xs = unique (map f xs)"
  12.433 -apply (induct_tac "xs")
  12.434 -apply simp
  12.435 +lemma comp_wf_mrT: "\<lbrakk> ws_prog G; is_class G D\<rbrakk> \<Longrightarrow> 
  12.436 +  wf_mrT (TranslComp.comp G) (C, D, fs, map (compMethod G a) ms) =
  12.437 +  wf_mrT G (C, D, fs, ms)"
  12.438 +apply (simp add: wf_mrT_def compMethod_def split_beta)
  12.439 +apply (simp add: comp_widen)
  12.440 +apply (rule iffI)
  12.441  apply (intro strip)
  12.442  apply simp
  12.443 -apply (case_tac a, simp)
  12.444 -apply (case_tac "f (aa, b)")
  12.445 -apply (simp only:)
  12.446 -apply (simp only: unique_Cons)
  12.447 -
  12.448 -apply simp
  12.449 -apply (subgoal_tac "(\<exists>y. (ab, y) \<in> set list) = (\<exists>y. (ab, y) \<in> f ` set list)")
  12.450 -apply blast
  12.451 -apply (rule iffI)
  12.452 -
  12.453 -apply clarify
  12.454 -apply (rule_tac x="(snd (f(ab, y)))" in exI)
  12.455 -apply simp
  12.456 -apply (subgoal_tac "(ab, snd (f (ab, y))) = (fst (f (ab, y)), snd (f (ab, y)))")
  12.457 -apply (simp only:)
  12.458 -apply (simp add: surjective_pairing [THEN sym])
  12.459 -apply (subgoal_tac "fst (f (ab, y)) = fst (ab, y)")
  12.460 -apply simp
  12.461 -apply (drule bspec) apply assumption apply simp
  12.462 -
  12.463 -apply clarify
  12.464 -apply (drule bspec) apply assumption apply simp
  12.465 -apply (subgoal_tac "ac = ab")
  12.466 -apply simp
  12.467 -apply blast
  12.468 -apply (drule sym)
  12.469 -apply (drule sym)
  12.470 -apply (drule_tac f=fst in arg_cong)
  12.471 -apply simp
  12.472 -done
  12.473 -
  12.474 -lemma comp_unique: "unique G = unique (comp G)"
  12.475 -apply (simp add: comp_def)
  12.476 -apply (rule unique_map_fst)
  12.477 -apply (simp add: compClass_def split_beta)
  12.478 +apply (drule bspec) apply assumption
  12.479 +apply (drule_tac x=D' in spec) apply (drule_tac x=rT' in spec) apply (drule mp)
  12.480 +prefer 2 apply assumption
  12.481 +apply (simp add: comp_method [of G D])
  12.482 +apply (erule exE)+
  12.483 +apply (subgoal_tac "z =(fst z, fst (snd z), snd (snd z))")
  12.484 +apply (rule exI)
  12.485 +apply (simp)
  12.486 +apply (simp add: split_paired_all)
  12.487 +apply (intro strip)
  12.488 +apply (simp add: comp_method)
  12.489 +apply auto
  12.490  done
  12.491  
  12.492  
  12.493 @@ -396,9 +388,6 @@
  12.494    (* DIVERSE OTHER LEMMAS *)
  12.495  (**********************************************************************)
  12.496  
  12.497 -
  12.498 -(* already proved less elegantly in CorrComp.thy;
  12.499 -  to be moved into a common super-theory *)
  12.500  lemma max_spec_preserves_length:
  12.501    "max_spec G C (mn, pTs) = {((md,rT),pTs')} 
  12.502    \<Longrightarrow> length pTs = length pTs'"
  12.503 @@ -408,7 +397,6 @@
  12.504  done
  12.505  
  12.506  
  12.507 -(* already proved in CorrComp.thy \<longrightarrow> into common supertheory *)
  12.508  lemma ty_exprs_length [simp]: "(E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts)"
  12.509  apply (subgoal_tac "(E\<turnstile>e::T \<longrightarrow> True) \<and> (E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts) \<and> (E\<turnstile>s\<surd> \<longrightarrow> True)")
  12.510  apply blast
  12.511 @@ -425,5 +413,13 @@
  12.512  apply (simp add: method_rT_def)
  12.513  done
  12.514  
  12.515 +  (**********************************************************************************)
  12.516 +
  12.517 +declare compClass_fst [simp del]
  12.518 +declare compClass_fst_snd [simp del]
  12.519 +declare compClass_fst_snd_snd [simp del]
  12.520 +
  12.521 +declare split_paired_All [simp add]
  12.522 +declare split_paired_Ex [simp add]
  12.523  
  12.524  end
    13.1 --- a/src/HOL/MicroJava/Comp/TypeInf.thy	Mon May 26 11:42:41 2003 +0200
    13.2 +++ b/src/HOL/MicroJava/Comp/TypeInf.thy	Mon May 26 18:36:15 2003 +0200
    13.3 @@ -20,7 +20,7 @@
    13.4  by (erule ty_expr.cases, auto)
    13.5  
    13.6  lemma Cast_invers: "E\<turnstile>Cast D e::T
    13.7 -  \<Longrightarrow> \<exists> C. T = Class D \<and> E\<turnstile>e::Class C \<and> is_class (prg E) D \<and> prg E\<turnstile>C\<preceq>? D"
    13.8 +  \<Longrightarrow> \<exists> C. T = Class D \<and> E\<turnstile>e::C \<and> is_class (prg E) D \<and> prg E\<turnstile>C\<preceq>? Class D"
    13.9  by (erule ty_expr.cases, auto)
   13.10  
   13.11  lemma Lit_invers: "E\<turnstile>Lit x::T
   13.12 @@ -87,9 +87,10 @@
   13.13  (* Uniqueness of types property *)
   13.14  
   13.15  lemma uniqueness_of_types: "
   13.16 -  (\<forall> E T1 T2. E\<turnstile>e :: T1 \<longrightarrow> E\<turnstile>e :: T2 \<longrightarrow> T1 = T2) \<and>
   13.17 -  (\<forall> E Ts1 Ts2. E\<turnstile>es [::] Ts1 \<longrightarrow> E\<turnstile>es [::] Ts2 \<longrightarrow> Ts1 = Ts2)"
   13.18 -
   13.19 +  (\<forall> (E\<Colon>'a prog \<times> (vname \<Rightarrow> ty option)) T1 T2. 
   13.20 +  E\<turnstile>e :: T1 \<longrightarrow> E\<turnstile>e :: T2 \<longrightarrow> T1 = T2) \<and>
   13.21 +  (\<forall> (E\<Colon>'a prog \<times> (vname \<Rightarrow> ty option)) Ts1 Ts2. 
   13.22 +  E\<turnstile>es [::] Ts1 \<longrightarrow> E\<turnstile>es [::] Ts2 \<longrightarrow> Ts1 = Ts2)"
   13.23  apply (rule expr.induct)
   13.24  
   13.25  (* NewC *)
    14.1 --- a/src/HOL/MicroJava/J/Example.thy	Mon May 26 11:42:41 2003 +0200
    14.2 +++ b/src/HOL/MicroJava/J/Example.thy	Mon May 26 18:36:15 2003 +0200
    14.3 @@ -293,60 +293,74 @@
    14.4  done
    14.5  
    14.6  lemma wf_ObjectC: 
    14.7 -"wf_cdecl wf_java_mdecl tprg ObjectC"
    14.8 -apply (unfold wf_cdecl_def wf_fdecl_def ObjectC_def)
    14.9 +"ws_cdecl tprg ObjectC \<and> 
   14.10 +  wf_cdecl_mdecl wf_java_mdecl tprg ObjectC \<and> wf_mrT tprg ObjectC"
   14.11 +apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 
   14.12 +  wf_mrT_def wf_fdecl_def ObjectC_def)
   14.13  apply (simp (no_asm))
   14.14  done
   14.15  
   14.16  lemma wf_NP:
   14.17 -"wf_cdecl wf_java_mdecl tprg NullPointerC"
   14.18 -apply (unfold wf_cdecl_def wf_fdecl_def NullPointerC_def)
   14.19 +"ws_cdecl tprg NullPointerC \<and>
   14.20 +  wf_cdecl_mdecl wf_java_mdecl tprg NullPointerC \<and> wf_mrT tprg NullPointerC"
   14.21 +apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 
   14.22 +  wf_mrT_def wf_fdecl_def NullPointerC_def)
   14.23  apply (simp add: class_def)
   14.24  apply (fold NullPointerC_def class_def)
   14.25  apply auto
   14.26  done
   14.27  
   14.28  lemma wf_OM:
   14.29 -"wf_cdecl wf_java_mdecl tprg OutOfMemoryC"
   14.30 -apply (unfold wf_cdecl_def wf_fdecl_def OutOfMemoryC_def)
   14.31 +"ws_cdecl tprg OutOfMemoryC \<and>
   14.32 +  wf_cdecl_mdecl wf_java_mdecl tprg OutOfMemoryC \<and> wf_mrT tprg OutOfMemoryC"
   14.33 +apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 
   14.34 +  wf_mrT_def wf_fdecl_def OutOfMemoryC_def)
   14.35  apply (simp add: class_def)
   14.36  apply (fold OutOfMemoryC_def class_def)
   14.37  apply auto
   14.38  done
   14.39  
   14.40  lemma wf_CC:
   14.41 -"wf_cdecl wf_java_mdecl tprg ClassCastC"
   14.42 -apply (unfold wf_cdecl_def wf_fdecl_def ClassCastC_def)
   14.43 +"ws_cdecl tprg ClassCastC \<and>
   14.44 +  wf_cdecl_mdecl wf_java_mdecl tprg ClassCastC \<and> wf_mrT tprg ClassCastC"
   14.45 +apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 
   14.46 +  wf_mrT_def wf_fdecl_def ClassCastC_def)
   14.47  apply (simp add: class_def)
   14.48  apply (fold ClassCastC_def class_def)
   14.49  apply auto
   14.50  done
   14.51  
   14.52  lemma wf_BaseC: 
   14.53 -"wf_cdecl wf_java_mdecl tprg BaseC"
   14.54 -apply (unfold wf_cdecl_def wf_fdecl_def BaseC_def)
   14.55 +"ws_cdecl tprg BaseC \<and>
   14.56 +  wf_cdecl_mdecl wf_java_mdecl tprg BaseC \<and> wf_mrT tprg BaseC"
   14.57 +apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
   14.58 +  wf_mrT_def wf_fdecl_def BaseC_def)
   14.59  apply (simp (no_asm))
   14.60  apply (fold BaseC_def)
   14.61 -apply (rule wf_foo_Base [THEN conjI])
   14.62 +apply (rule mp) defer apply (rule wf_foo_Base)
   14.63 +apply (auto simp add: wf_mdecl_def)
   14.64 +done
   14.65 +
   14.66 +
   14.67 +lemma wf_ExtC: 
   14.68 +"ws_cdecl tprg ExtC \<and>
   14.69 +  wf_cdecl_mdecl wf_java_mdecl tprg ExtC \<and> wf_mrT tprg ExtC"
   14.70 +apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
   14.71 +  wf_mrT_def wf_fdecl_def ExtC_def)
   14.72 +apply (simp (no_asm))
   14.73 +apply (fold ExtC_def)
   14.74 +apply (rule mp) defer apply (rule wf_foo_Ext)
   14.75 +apply (auto simp add: wf_mdecl_def)
   14.76 +apply (drule rtranclD)
   14.77  apply auto
   14.78  done
   14.79  
   14.80 -lemma wf_ExtC: 
   14.81 -"wf_cdecl wf_java_mdecl tprg ExtC"
   14.82 -apply (unfold wf_cdecl_def wf_fdecl_def ExtC_def)
   14.83 -apply (simp (no_asm))
   14.84 -apply (fold ExtC_def)
   14.85 -apply (rule wf_foo_Ext [THEN conjI])
   14.86 -apply auto
   14.87 -apply (drule rtranclD)
   14.88 -apply auto
   14.89 -done
   14.90  
   14.91  lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def)
   14.92  
   14.93  lemma wf_tprg: 
   14.94  "wf_prog wf_java_mdecl tprg"
   14.95 -apply (unfold wf_prog_def Let_def)
   14.96 +apply (unfold wf_prog_def ws_prog_def Let_def)
   14.97  apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes)
   14.98  apply (rule wf_syscls)
   14.99  apply (simp add: SystemClasses_def)
    15.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Mon May 26 11:42:41 2003 +0200
    15.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Mon May 26 18:36:15 2003 +0200
    15.3 @@ -15,23 +15,30 @@
    15.4    (x,(h(a\<mapsto>(C,(init_vars (fields (G,C))))), l))::\<preceq>(G, lT)"
    15.5  apply( erule conforms_upd_obj)
    15.6  apply(  unfold oconf_def)
    15.7 -apply(  auto dest!: fields_is_type)
    15.8 +apply(  auto dest!: fields_is_type simp add: wf_prog_ws_prog)
    15.9  done
   15.10 - 
   15.11 +
   15.12 +
   15.13  lemma Cast_conf: 
   15.14 - "[| wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>Class C; G\<turnstile>C\<preceq>? D; cast_ok G D h v|]  
   15.15 -  ==> G,h\<turnstile>v::\<preceq>Class D" 
   15.16 + "[| wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>CC; G\<turnstile>CC \<preceq>? Class D; cast_ok G D h v|]  
   15.17 +  ==> G,h\<turnstile>v::\<preceq>Class D"
   15.18 +apply (case_tac "CC")
   15.19 +apply simp
   15.20 +apply (case_tac "ref_ty")
   15.21 +apply (clarsimp simp add: conf_def)
   15.22 +apply simp
   15.23 +apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D", simp) 
   15.24 +apply (rule conf_widen, assumption+) apply (erule widen.subcls)
   15.25 +
   15.26  apply (unfold cast_ok_def)
   15.27  apply( case_tac "v = Null")
   15.28  apply(  simp)
   15.29 -apply(  drule widen_RefT)
   15.30  apply(  clarify)
   15.31  apply( drule (1) non_npD)
   15.32  apply( auto intro!: conf_AddrI simp add: obj_ty_def)
   15.33  done
   15.34  
   15.35  
   15.36 -
   15.37  lemma FAcc_type_sound: 
   15.38  "[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (x,(h,l))::\<preceq>(G,lT);  
   15.39    x' = None --> G,h\<turnstile>a'::\<preceq> Class C; np a' x' = None |] ==>  
   15.40 @@ -43,6 +50,7 @@
   15.41  apply   auto
   15.42  apply( drule conforms_heapD [THEN hconfD])
   15.43  apply(  assumption)
   15.44 +apply (frule wf_prog_ws_prog)
   15.45  apply( drule (2) widen_cfs_fields)
   15.46  apply( drule (1) oconf_objD)
   15.47  apply auto
   15.48 @@ -82,6 +90,7 @@
   15.49  apply(  force)
   15.50  apply( rule oconf_hext)
   15.51  apply(  erule_tac [2] hext_upd_obj)
   15.52 +apply (frule wf_prog_ws_prog)
   15.53  apply( drule (2) widen_cfs_fields)
   15.54  apply( rule oconf_obj [THEN iffD2])
   15.55  apply( simp (no_asm))
   15.56 @@ -157,7 +166,6 @@
   15.57  apply(  fast elim!: widen_trans)
   15.58  apply (rule conforms_xcpt_change)
   15.59  apply( rule conforms_hext) apply assumption
   15.60 -(* apply( erule conforms_hext)*)
   15.61  apply(  erule (1) hext_trans)
   15.62  apply( erule conforms_heapD)
   15.63  apply (simp add: conforms_def)
   15.64 @@ -168,6 +176,8 @@
   15.65  declare split_if [split del]
   15.66  declare fun_upd_apply [simp del]
   15.67  declare fun_upd_same [simp]
   15.68 +declare wf_prog_ws_prog [simp]
   15.69 +
   15.70  ML{*
   15.71  val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
   15.72    (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
   15.73 @@ -267,6 +277,7 @@
   15.74    apply (rule Cast_conf)
   15.75    apply assumption+
   15.76  
   15.77 +
   15.78  -- "7 LAss"
   15.79  apply (fold fun_upd_def)
   15.80  apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
   15.81 @@ -342,7 +353,8 @@
   15.82  apply(  simp)
   15.83  apply (rule conjI)
   15.84    apply(  fast elim: hext_trans)
   15.85 -  apply (rule conforms_xcpt_change, assumption) apply (simp (no_asm_simp) add: xconf_def)
   15.86 +  apply (rule conforms_xcpt_change, assumption) 
   15.87 +  apply (simp (no_asm_simp) add: xconf_def)
   15.88  apply(clarsimp)
   15.89  
   15.90  apply( drule ty_expr_is_type, simp)
   15.91 @@ -370,6 +382,15 @@
   15.92  apply auto
   15.93  done
   15.94  
   15.95 +lemma evals_type_sound: "!!E s s'.  
   15.96 +  [| G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); G=prg E; wf_java_prog G; (x,s)::\<preceq>E; E\<turnstile>es[::]Ts |]  
   15.97 +  ==> (x',s')::\<preceq>E \<and> (x'=None --> list_all2 (conf G (heap s')) vs Ts)"
   15.98 +apply( simp (no_asm_simp) only: split_tupled_all)
   15.99 +apply (drule eval_evals_exec_type_sound 
  15.100 +             [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp])
  15.101 +apply auto
  15.102 +done
  15.103 +
  15.104  lemma exec_type_sound: "!!E s s'.  
  15.105    [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd> |]  
  15.106    ==> (x',s')::\<preceq>E"
  15.107 @@ -395,6 +416,7 @@
  15.108  
  15.109  declare split_beta [simp del]
  15.110  declare fun_upd_apply [simp]
  15.111 +declare wf_prog_ws_prog [simp del]
  15.112  
  15.113  end
  15.114  
    16.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Mon May 26 11:42:41 2003 +0200
    16.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon May 26 18:36:15 2003 +0200
    16.3 @@ -11,19 +11,19 @@
    16.4  consts
    16.5    subcls1 :: "'c prog => (cname \<times> cname) set"  -- "subclass"
    16.6    widen   :: "'c prog => (ty    \<times> ty   ) set"  -- "widening"
    16.7 -  cast    :: "'c prog => (cname \<times> cname) set"  -- "casting"
    16.8 +  cast    :: "'c prog => (ty    \<times> ty   ) set"  -- "casting"
    16.9  
   16.10  syntax (xsymbols)
   16.11    subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
   16.12    subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _"  [71,71,71] 70)
   16.13    widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
   16.14 -  cast    :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
   16.15 +  cast    :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
   16.16  
   16.17  syntax
   16.18    subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
   16.19    subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _"  [71,71,71] 70)
   16.20    widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _"   [71,71,71] 70)
   16.21 -  cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _"  [71,71,71] 70)
   16.22 +  cast    :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <=? _"  [71,71,71] 70)
   16.23  
   16.24  translations
   16.25    "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
   16.26 @@ -132,8 +132,8 @@
   16.27  -- "casting conversion, cf. 5.5 / 5.1.5"
   16.28  -- "left out casts on primitve types"
   16.29  inductive "cast G" intros
   16.30 -  widen:  "G\<turnstile>C\<preceq>C D ==> G\<turnstile>C \<preceq>? D"
   16.31 -  subcls: "G\<turnstile>D\<preceq>C C ==> G\<turnstile>C \<preceq>? D"
   16.32 +  widen:  "G\<turnstile> C\<preceq> D ==> G\<turnstile>C \<preceq>? D"
   16.33 +  subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D"
   16.34  
   16.35  lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False"
   16.36  apply (rule iffI)
   16.37 @@ -168,6 +168,21 @@
   16.38  apply (auto elim: widen.subcls)
   16.39  done
   16.40  
   16.41 +lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D"
   16.42 +by (ind_cases "G \<turnstile> T \<preceq> NT",  auto)
   16.43 +
   16.44 +lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False"
   16.45 +apply (rule iffI)
   16.46 +apply (erule cast.elims)
   16.47 +apply auto
   16.48 +done
   16.49 +
   16.50 +lemma cast_RefT: "G \<turnstile> C \<preceq>? Class D \<Longrightarrow> \<exists> rT. C = RefT rT"
   16.51 +apply (erule cast.cases)
   16.52 +apply simp apply (erule widen.cases) 
   16.53 +apply auto
   16.54 +done
   16.55 +
   16.56  theorem widen_trans[trans]: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
   16.57  proof -
   16.58    assume "G\<turnstile>S\<preceq>U" thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
    17.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Mon May 26 11:42:41 2003 +0200
    17.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Mon May 26 18:36:15 2003 +0200
    17.3 @@ -27,12 +27,40 @@
    17.4  types 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
    17.5  
    17.6  constdefs
    17.7 + wf_syscls :: "'c prog => bool"
    17.8 +"wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"
    17.9 +
   17.10   wf_fdecl :: "'c prog => fdecl => bool"
   17.11  "wf_fdecl G == \<lambda>(fn,ft). is_type G ft"
   17.12  
   17.13   wf_mhead :: "'c prog => sig => ty => bool"
   17.14  "wf_mhead G == \<lambda>(mn,pTs) rT. (\<forall>T\<in>set pTs. is_type G T) \<and> is_type G rT"
   17.15  
   17.16 + ws_cdecl :: "'c prog => 'c cdecl => bool"
   17.17 +"ws_cdecl G ==
   17.18 +   \<lambda>(C,(D,fs,ms)).
   17.19 +  (\<forall>f\<in>set fs. wf_fdecl G         f) \<and>  unique fs \<and>
   17.20 +  (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT) \<and> unique ms \<and>
   17.21 +  (C \<noteq> Object \<longrightarrow> is_class G D \<and>  \<not>G\<turnstile>D\<preceq>C C)"
   17.22 +
   17.23 + ws_prog :: "'c prog => bool"
   17.24 +"ws_prog G == 
   17.25 +  wf_syscls G \<and> (\<forall>c\<in>set G. ws_cdecl G c) \<and> unique G"
   17.26 +
   17.27 + wf_mrT   :: "'c prog => 'c cdecl => bool"
   17.28 +"wf_mrT G ==
   17.29 +   \<lambda>(C,(D,fs,ms)).
   17.30 +  (C \<noteq> Object \<longrightarrow> (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'.
   17.31 +                      method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))"
   17.32 +
   17.33 + wf_cdecl_mdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
   17.34 +"wf_cdecl_mdecl wf_mb G ==
   17.35 +   \<lambda>(C,(D,fs,ms)). (\<forall>m\<in>set ms. wf_mb G C m)"
   17.36 +
   17.37 + wf_prog :: "'c wf_mb => 'c prog => bool"
   17.38 +"wf_prog wf_mb G == 
   17.39 +     ws_prog G \<and> (\<forall>c\<in> set G. wf_mrT G c \<and> wf_cdecl_mdecl wf_mb G c)"
   17.40 +
   17.41   wf_mdecl :: "'c wf_mb => 'c wf_mb"
   17.42  "wf_mdecl wf_mb G C == \<lambda>(sig,rT,mb). wf_mhead G sig rT \<and> wf_mb G C (sig,rT,mb)"
   17.43  
   17.44 @@ -45,33 +73,62 @@
   17.45                     (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'.
   17.46                        method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))"
   17.47  
   17.48 - wf_syscls :: "'c prog => bool"
   17.49 -"wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"
   17.50 +lemma wf_cdecl_mrT_cdecl_mdecl:
   17.51 +  "(wf_cdecl wf_mb G c) = (ws_cdecl G c \<and> wf_mrT G c \<and> wf_cdecl_mdecl wf_mb G c)"
   17.52 +apply (rule iffI)
   17.53 +apply (simp add: wf_cdecl_def ws_cdecl_def wf_mrT_def wf_cdecl_mdecl_def 
   17.54 +  wf_mdecl_def wf_mhead_def split_beta)+
   17.55 +done
   17.56  
   17.57 - wf_prog :: "'c wf_mb => 'c prog => bool"
   17.58 -"wf_prog wf_mb G == 
   17.59 -   let cs = set G in wf_syscls G \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G"
   17.60 +lemma wf_cdecl_ws_cdecl [intro]: "wf_cdecl wf_mb G cd \<Longrightarrow> ws_cdecl G cd"
   17.61 +by (simp add: wf_cdecl_mrT_cdecl_mdecl)
   17.62 +
   17.63 +lemma wf_prog_ws_prog [intro]: "wf_prog wf_mb G \<Longrightarrow> ws_prog G"
   17.64 +by (simp add: wf_prog_def ws_prog_def)
   17.65 +
   17.66 +lemma wf_prog_wf_mdecl: 
   17.67 +  "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; ((mn,pTs),rT,code) \<in> set mdecls\<rbrakk>
   17.68 +  \<Longrightarrow> wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
   17.69 +by (auto simp add: wf_prog_def ws_prog_def wf_mdecl_def  
   17.70 +  wf_cdecl_mdecl_def ws_cdecl_def)
   17.71  
   17.72  lemma class_wf: 
   17.73 - "[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)"
   17.74 -apply (unfold wf_prog_def class_def)
   17.75 -apply (simp)
   17.76 + "[|class G C = Some c; wf_prog wf_mb G|] 
   17.77 +  ==> wf_cdecl wf_mb G (C,c) \<and> wf_mrT G (C,c)"
   17.78 +apply (unfold wf_prog_def ws_prog_def wf_cdecl_def class_def)
   17.79 +apply clarify
   17.80 +apply (drule_tac x="(C,c)" in bspec, fast dest: map_of_SomeD)
   17.81 +apply (drule_tac x="(C,c)" in bspec, fast dest: map_of_SomeD)
   17.82 +apply (simp add: wf_cdecl_def ws_cdecl_def wf_mdecl_def
   17.83 +  wf_cdecl_mdecl_def wf_mrT_def split_beta)
   17.84 +done
   17.85 +
   17.86 +lemma class_wf_struct: 
   17.87 + "[|class G C = Some c; ws_prog G|] 
   17.88 +  ==> ws_cdecl G (C,c)"
   17.89 +apply (unfold ws_prog_def class_def)
   17.90  apply (fast dest: map_of_SomeD)
   17.91  done
   17.92  
   17.93  lemma class_Object [simp]: 
   17.94 -  "wf_prog wf_mb G ==> \<exists>X fs ms. class G Object = Some (X,fs,ms)"
   17.95 -apply (unfold wf_prog_def wf_syscls_def class_def)
   17.96 +  "ws_prog G ==> \<exists>X fs ms. class G Object = Some (X,fs,ms)"
   17.97 +apply (unfold ws_prog_def wf_syscls_def class_def)
   17.98  apply (auto simp: map_of_SomeI)
   17.99  done
  17.100  
  17.101 -lemma is_class_Object [simp]: "wf_prog wf_mb G ==> is_class G Object"
  17.102 +lemma class_Object_syscls [simp]: 
  17.103 +  "wf_syscls G ==> unique G \<Longrightarrow> \<exists>X fs ms. class G Object = Some (X,fs,ms)"
  17.104 +apply (unfold wf_syscls_def class_def)
  17.105 +apply (auto simp: map_of_SomeI)
  17.106 +done
  17.107 +
  17.108 +lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object"
  17.109  apply (unfold is_class_def)
  17.110  apply (simp (no_asm_simp))
  17.111  done
  17.112  
  17.113 -lemma is_class_xcpt [simp]: "wf_prog wf_mb G \<Longrightarrow> is_class G (Xcpt x)"
  17.114 -  apply (simp add: wf_prog_def wf_syscls_def)
  17.115 +lemma is_class_xcpt [simp]: "ws_prog G \<Longrightarrow> is_class G (Xcpt x)"
  17.116 +  apply (simp add: ws_prog_def wf_syscls_def)
  17.117    apply (simp add: is_class_def class_def)
  17.118    apply clarify
  17.119    apply (erule_tac x = x in allE)
  17.120 @@ -79,38 +136,38 @@
  17.121    apply (auto intro!: map_of_SomeI)
  17.122    done
  17.123  
  17.124 -lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; wf_prog wf_mb G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+"
  17.125 +lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+"
  17.126  apply( frule r_into_trancl)
  17.127  apply( drule subcls1D)
  17.128  apply(clarify)
  17.129 -apply( drule (1) class_wf)
  17.130 -apply( unfold wf_cdecl_def)
  17.131 +apply( drule (1) class_wf_struct)
  17.132 +apply( unfold ws_cdecl_def)
  17.133  apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
  17.134  done
  17.135  
  17.136  lemma wf_cdecl_supD: 
  17.137 -"!!r. \<lbrakk>wf_cdecl wf_mb G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D"
  17.138 -apply (unfold wf_cdecl_def)
  17.139 +"!!r. \<lbrakk>ws_cdecl G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D"
  17.140 +apply (unfold ws_cdecl_def)
  17.141  apply (auto split add: option.split_asm)
  17.142  done
  17.143  
  17.144 -lemma subcls_asym: "[|wf_prog wf_mb G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+"
  17.145 +lemma subcls_asym: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+"
  17.146  apply(erule tranclE)
  17.147  apply(fast dest!: subcls1_wfD )
  17.148  apply(fast dest!: subcls1_wfD intro: trancl_trans)
  17.149  done
  17.150  
  17.151 -lemma subcls_irrefl: "[|wf_prog wf_mb G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D"
  17.152 +lemma subcls_irrefl: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D"
  17.153  apply (erule trancl_trans_induct)
  17.154  apply  (auto dest: subcls1_wfD subcls_asym)
  17.155  done
  17.156  
  17.157 -lemma acyclic_subcls1: "wf_prog wf_mb G ==> acyclic (subcls1 G)"
  17.158 +lemma acyclic_subcls1: "ws_prog G ==> acyclic (subcls1 G)"
  17.159  apply (unfold acyclic_def)
  17.160  apply (fast dest: subcls_irrefl)
  17.161  done
  17.162  
  17.163 -lemma wf_subcls1: "wf_prog wf_mb G ==> wf ((subcls1 G)^-1)"
  17.164 +lemma wf_subcls1: "ws_prog G ==> wf ((subcls1 G)^-1)"
  17.165  apply (rule finite_acyclic_wf)
  17.166  apply ( subst finite_converse)
  17.167  apply ( rule finite_subcls1)
  17.168 @@ -118,12 +175,14 @@
  17.169  apply (erule acyclic_subcls1)
  17.170  done
  17.171  
  17.172 +
  17.173  lemma subcls_induct: 
  17.174  "[|wf_prog wf_mb G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
  17.175  (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
  17.176  proof -
  17.177    assume p: "PROP ?P"
  17.178    assume ?A thus ?thesis apply -
  17.179 +apply (drule wf_prog_ws_prog)
  17.180  apply(drule wf_subcls1)
  17.181  apply(drule wf_trancl)
  17.182  apply(simp only: trancl_converse)
  17.183 @@ -155,7 +214,57 @@
  17.184  apply( case_tac "C = Object")
  17.185  apply(  fast)
  17.186  apply safe
  17.187 -apply( frule (1) class_wf)
  17.188 +apply( frule (1) class_wf) apply (erule conjE)+
  17.189 +apply (frule wf_cdecl_ws_cdecl)
  17.190 +apply( frule (1) wf_cdecl_supD)
  17.191 +
  17.192 +apply( subgoal_tac "G\<turnstile>C\<prec>C1a")
  17.193 +apply( erule_tac [2] subcls1I)
  17.194 +apply(  rule p)
  17.195 +apply (unfold is_class_def)
  17.196 +apply auto
  17.197 +done
  17.198 +qed
  17.199 +
  17.200 +lemma subcls_induct_struct: 
  17.201 +"[|ws_prog G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
  17.202 +(is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
  17.203 +proof -
  17.204 +  assume p: "PROP ?P"
  17.205 +  assume ?A thus ?thesis apply -
  17.206 +apply(drule wf_subcls1)
  17.207 +apply(drule wf_trancl)
  17.208 +apply(simp only: trancl_converse)
  17.209 +apply(erule_tac a = C in wf_induct)
  17.210 +apply(rule p)
  17.211 +apply(auto)
  17.212 +done
  17.213 +qed
  17.214 +
  17.215 +
  17.216 +lemma subcls1_induct_struct:
  17.217 +"[|is_class G C; ws_prog G; P Object;  
  17.218 +   !!C D fs ms. [|C \<noteq> Object; is_class G C; class G C = Some (D,fs,ms) \<and>  
  17.219 +    ws_cdecl G (C,D,fs,ms) \<and> G\<turnstile>C\<prec>C1D \<and> is_class G D \<and> P D|] ==> P C 
  17.220 + |] ==> P C"
  17.221 +(is "?A \<Longrightarrow> ?B \<Longrightarrow> ?C \<Longrightarrow> PROP ?P \<Longrightarrow> _")
  17.222 +proof -
  17.223 +  assume p: "PROP ?P"
  17.224 +  assume ?A ?B ?C thus ?thesis apply -
  17.225 +apply(unfold is_class_def)
  17.226 +apply( rule impE)
  17.227 +prefer 2
  17.228 +apply(   assumption)
  17.229 +prefer 2
  17.230 +apply(  assumption)
  17.231 +apply( erule thin_rl)
  17.232 +apply( rule subcls_induct_struct)
  17.233 +apply(  assumption)
  17.234 +apply( rule impI)
  17.235 +apply( case_tac "C = Object")
  17.236 +apply(  fast)
  17.237 +apply safe
  17.238 +apply( frule (1) class_wf_struct)
  17.239  apply( frule (1) wf_cdecl_supD)
  17.240  
  17.241  apply( subgoal_tac "G\<turnstile>C\<prec>C1a")
  17.242 @@ -170,7 +279,7 @@
  17.243  
  17.244  lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma];
  17.245  
  17.246 -lemma field_rec: "\<lbrakk>class G C = Some (D, fs, ms); wf_prog wf_mb G\<rbrakk>
  17.247 +lemma field_rec: "\<lbrakk>class G C = Some (D, fs, ms); ws_prog G\<rbrakk>
  17.248  \<Longrightarrow> field (G, C) =
  17.249     (if C = Object then empty else field (G, D)) ++
  17.250     map_of (map (\<lambda>(s, f). (s, C, f)) fs)"
  17.251 @@ -183,14 +292,14 @@
  17.252  done
  17.253  
  17.254  lemma method_Object [simp]:
  17.255 -  "method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> wf_prog wf_mb G \<Longrightarrow> D = Object"  
  17.256 +  "method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> ws_prog G \<Longrightarrow> D = Object"  
  17.257    apply (frule class_Object, clarify)
  17.258    apply (drule method_rec, assumption)
  17.259    apply (auto dest: map_of_SomeD)
  17.260    done
  17.261  
  17.262  
  17.263 -lemma fields_Object [simp]: "\<lbrakk> ((vn, C), T) \<in> set (fields (G, Object)); wf_prog wf_mb G \<rbrakk>
  17.264 +lemma fields_Object [simp]: "\<lbrakk> ((vn, C), T) \<in> set (fields (G, Object)); ws_prog G \<rbrakk>
  17.265    \<Longrightarrow> C = Object"
  17.266  apply (frule class_Object)
  17.267  apply clarify
  17.268 @@ -202,8 +311,8 @@
  17.269  apply simp
  17.270  done
  17.271  
  17.272 -lemma subcls_C_Object: "[|is_class G C; wf_prog wf_mb G|] ==> G\<turnstile>C\<preceq>C Object"
  17.273 -apply(erule subcls1_induct)
  17.274 +lemma subcls_C_Object: "[|is_class G C; ws_prog G|] ==> G\<turnstile>C\<preceq>C Object"
  17.275 +apply(erule subcls1_induct_struct)
  17.276  apply(  assumption)
  17.277  apply( fast)
  17.278  apply(auto dest!: wf_cdecl_supD)
  17.279 @@ -215,9 +324,9 @@
  17.280  apply auto
  17.281  done
  17.282  
  17.283 -lemma widen_fields_defpl': "[|is_class G C; wf_prog wf_mb G|] ==>  
  17.284 +lemma widen_fields_defpl': "[|is_class G C; ws_prog G|] ==>  
  17.285    \<forall>((fn,fd),fT)\<in>set (fields (G,C)). G\<turnstile>C\<preceq>C fd"
  17.286 -apply( erule subcls1_induct)
  17.287 +apply( erule subcls1_induct_struct)
  17.288  apply(   assumption)
  17.289  apply(  frule class_Object)
  17.290  apply(  clarify)
  17.291 @@ -238,21 +347,21 @@
  17.292  done
  17.293  
  17.294  lemma widen_fields_defpl: 
  17.295 -  "[|((fn,fd),fT) \<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==>  
  17.296 +  "[|((fn,fd),fT) \<in> set (fields (G,C)); ws_prog G; is_class G C|] ==>  
  17.297    G\<turnstile>C\<preceq>C fd"
  17.298  apply( drule (1) widen_fields_defpl')
  17.299  apply (fast)
  17.300  done
  17.301  
  17.302  lemma unique_fields: 
  17.303 -  "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
  17.304 -apply( erule subcls1_induct)
  17.305 +  "[|is_class G C; ws_prog G|] ==> unique (fields (G,C))"
  17.306 +apply( erule subcls1_induct_struct)
  17.307  apply(   assumption)
  17.308  apply(  frule class_Object)
  17.309  apply(  clarify)
  17.310  apply(  frule fields_rec, assumption)
  17.311 -apply(  drule class_wf, assumption)
  17.312 -apply(  simp add: wf_cdecl_def)
  17.313 +apply(  drule class_wf_struct, assumption)
  17.314 +apply(  simp add: ws_cdecl_def)
  17.315  apply(  rule unique_map_inj)
  17.316  apply(   simp)
  17.317  apply(  rule inj_onI)
  17.318 @@ -263,9 +372,9 @@
  17.319  apply( subst fields_rec)
  17.320  apply   auto
  17.321  apply( rotate_tac -1)
  17.322 -apply( frule class_wf)
  17.323 +apply( frule class_wf_struct)
  17.324  apply  auto
  17.325 -apply( simp add: wf_cdecl_def)
  17.326 +apply( simp add: ws_cdecl_def)
  17.327  apply( erule unique_append)
  17.328  apply(  rule unique_map_inj)
  17.329  apply(   clarsimp)
  17.330 @@ -275,7 +384,7 @@
  17.331  done
  17.332  
  17.333  lemma fields_mono_lemma [rule_format (no_asm)]: 
  17.334 -  "[|wf_prog wf_mb G; (C',C)\<in>(subcls1 G)^*|] ==>  
  17.335 +  "[|ws_prog G; (C',C)\<in>(subcls1 G)^*|] ==>  
  17.336    x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
  17.337  apply(erule converse_rtrancl_induct)
  17.338  apply( safe dest!: subcls1D)
  17.339 @@ -284,7 +393,7 @@
  17.340  done
  17.341  
  17.342  lemma fields_mono: 
  17.343 -"\<lbrakk>map_of (fields (G,C)) fn = Some f; G\<turnstile>D\<preceq>C C; is_class G D; wf_prog wf_mb G\<rbrakk> 
  17.344 +"\<lbrakk>map_of (fields (G,C)) fn = Some f; G\<turnstile>D\<preceq>C C; is_class G D; ws_prog G\<rbrakk> 
  17.345    \<Longrightarrow> map_of (fields (G,D)) fn = Some f"
  17.346  apply (rule map_of_SomeI)
  17.347  apply  (erule (1) unique_fields)
  17.348 @@ -293,7 +402,7 @@
  17.349  done
  17.350  
  17.351  lemma widen_cfs_fields: 
  17.352 -"[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; wf_prog wf_mb G|]==>  
  17.353 +"[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; ws_prog G|]==>  
  17.354    map_of (fields (G,D)) (fn, fd) = Some fT"
  17.355  apply (drule field_fields)
  17.356  apply (drule rtranclD)
  17.357 @@ -307,6 +416,7 @@
  17.358    "wf_prog wf_mb G ==> is_class G C \<Longrightarrow>   
  17.359       method (G,C) sig = Some (md,mh,m) 
  17.360     --> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))"
  17.361 +apply (frule wf_prog_ws_prog)
  17.362  apply( erule subcls1_induct)
  17.363  apply(   assumption)
  17.364  apply(  clarify) 
  17.365 @@ -317,7 +427,7 @@
  17.366  apply(  simp add: wf_cdecl_def)
  17.367  apply(  drule map_of_SomeD)
  17.368  apply(  subgoal_tac "md = Object")
  17.369 -apply(   fastsimp)
  17.370 +apply(   fastsimp) 
  17.371  apply(  fastsimp)
  17.372  apply( clarify)
  17.373  apply( frule_tac C = C in method_rec)
  17.374 @@ -338,22 +448,45 @@
  17.375  done
  17.376  
  17.377  
  17.378 -lemma wf_prog_wf_mhead: "\<lbrakk> wf_prog wf_mb G; (C, D, fds, mths) \<in> set G;
  17.379 -  ((mn, pTs), rT, jmb) \<in> set mths \<rbrakk>
  17.380 -  \<Longrightarrow> wf_mhead G (mn, pTs) rT"
  17.381 -apply (simp add: wf_prog_def wf_cdecl_def)
  17.382 -apply (erule conjE)+
  17.383 -apply (drule bspec, assumption)
  17.384 -apply simp
  17.385 -apply (erule conjE)+
  17.386 -apply (drule bspec, assumption)
  17.387 -apply (simp add: wf_mdecl_def)
  17.388 +lemma method_wf_mhead [rule_format (no_asm)]: 
  17.389 +  "ws_prog G ==> is_class G C \<Longrightarrow>   
  17.390 +     method (G,C) sig = Some (md,rT,mb) 
  17.391 +   --> G\<turnstile>C\<preceq>C md \<and> wf_mhead G sig rT"
  17.392 +apply( erule subcls1_induct_struct)
  17.393 +apply(   assumption)
  17.394 +apply(  clarify) 
  17.395 +apply(  frule class_Object)
  17.396 +apply(  clarify)
  17.397 +apply(  frule method_rec, assumption)
  17.398 +apply(  drule class_wf_struct, assumption)
  17.399 +apply(  simp add: ws_cdecl_def)
  17.400 +apply(  drule map_of_SomeD)
  17.401 +apply(  subgoal_tac "md = Object")
  17.402 +apply(   fastsimp)
  17.403 +apply(  fastsimp)
  17.404 +apply( clarify)
  17.405 +apply( frule_tac C = C in method_rec)
  17.406 +apply(  assumption)
  17.407 +apply( rotate_tac -1)
  17.408 +apply( simp)
  17.409 +apply( drule map_add_SomeD)
  17.410 +apply( erule disjE)
  17.411 +apply(  erule_tac V = "?P --> ?Q" in thin_rl)
  17.412 +apply (frule map_of_SomeD)
  17.413 +apply (clarsimp simp add: ws_cdecl_def)
  17.414 +apply blast
  17.415 +apply clarify
  17.416 +apply( rule rtrancl_trans)
  17.417 +prefer 2
  17.418 +apply(  assumption)
  17.419 +apply( rule r_into_rtrancl)
  17.420 +apply( fast intro: subcls1I)
  17.421  done
  17.422  
  17.423  lemma subcls_widen_methd [rule_format (no_asm)]: 
  17.424 -  "[|G\<turnstile>T\<preceq>C T'; wf_prog wf_mb G|] ==>  
  17.425 -   \<forall>D rT b. method (G,T') sig = Some (D,rT ,b) --> 
  17.426 -  (\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \<and> G\<turnstile>rT'\<preceq>rT)"
  17.427 +  "[|G\<turnstile>T'\<preceq>C T; wf_prog wf_mb G|] ==>  
  17.428 +   \<forall>D rT b. method (G,T) sig = Some (D,rT ,b) --> 
  17.429 +  (\<exists>D' rT' b'. method (G,T') sig = Some (D',rT',b') \<and> G\<turnstile>D'\<preceq>C D \<and> G\<turnstile>rT'\<preceq>rT)"
  17.430  apply( drule rtranclD)
  17.431  apply( erule disjE)
  17.432  apply(  fast)
  17.433 @@ -362,14 +495,14 @@
  17.434  prefer 2
  17.435  apply(  clarify)
  17.436  apply(  drule spec, drule spec, drule spec, erule (1) impE)
  17.437 -apply(  fast elim: widen_trans)
  17.438 +apply(  fast elim: widen_trans rtrancl_trans)
  17.439  apply( clarify)
  17.440  apply( drule subcls1D)
  17.441  apply( clarify)
  17.442  apply( subst method_rec)
  17.443  apply(  assumption)
  17.444  apply( unfold map_add_def)
  17.445 -apply( simp (no_asm_simp) del: split_paired_Ex)
  17.446 +apply( simp (no_asm_simp) add: wf_prog_ws_prog del: split_paired_Ex)
  17.447  apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z")
  17.448  apply(  erule exE)
  17.449  apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
  17.450 @@ -377,25 +510,34 @@
  17.451  apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
  17.452  apply(  tactic "asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1")
  17.453  apply(  simp_all (no_asm_simp) del: split_paired_Ex)
  17.454 -apply( drule (1) class_wf)
  17.455 +apply( frule (1) class_wf)
  17.456  apply( simp (no_asm_simp) only: split_tupled_all)
  17.457  apply( unfold wf_cdecl_def)
  17.458  apply( drule map_of_SomeD)
  17.459 -apply auto
  17.460 +apply (auto simp add: wf_mrT_def)
  17.461 +apply (rule rtrancl_trans)
  17.462 +defer
  17.463 +apply (rule method_wf_mhead [THEN conjunct1])
  17.464 +apply (simp only: wf_prog_def)
  17.465 +apply (simp add: is_class_def)
  17.466 +apply assumption
  17.467 +apply (auto intro: subcls1I)
  17.468  done
  17.469  
  17.470 +
  17.471  lemma subtype_widen_methd: 
  17.472   "[| G\<turnstile> C\<preceq>C D; wf_prog wf_mb G;  
  17.473       method (G,D) sig = Some (md, rT, b) |]  
  17.474    ==> \<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
  17.475 -apply(auto dest: subcls_widen_methd method_wf_mdecl 
  17.476 +apply(auto dest: subcls_widen_methd 
  17.477             simp add: wf_mdecl_def wf_mhead_def split_def)
  17.478  done
  17.479  
  17.480 +
  17.481  lemma method_in_md [rule_format (no_asm)]: 
  17.482 -  "wf_prog wf_mb G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) 
  17.483 +  "ws_prog G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) 
  17.484    --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
  17.485 -apply (erule (1) subcls1_induct)
  17.486 +apply (erule (1) subcls1_induct_struct)
  17.487   apply clarify
  17.488   apply (frule method_Object, assumption)
  17.489   apply hypsubst
  17.490 @@ -416,18 +558,42 @@
  17.491  done
  17.492  
  17.493  
  17.494 +lemma method_in_md_struct [rule_format (no_asm)]: 
  17.495 +  "ws_prog G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) 
  17.496 +  --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
  17.497 +apply (erule (1) subcls1_induct_struct)
  17.498 + apply clarify
  17.499 + apply (frule method_Object, assumption)
  17.500 + apply hypsubst
  17.501 + apply simp
  17.502 +apply (erule conjE)
  17.503 +apply (subst method_rec)
  17.504 +  apply (assumption)
  17.505 + apply (assumption)
  17.506 +apply (clarify)
  17.507 +apply (erule_tac "x" = "Da" in allE)
  17.508 +apply (clarsimp)
  17.509 + apply (simp add: map_of_map)
  17.510 + apply (clarify)
  17.511 + apply (subst method_rec)
  17.512 +   apply (assumption)
  17.513 +  apply (assumption)
  17.514 + apply (simp add: map_add_def map_of_map split add: option.split)
  17.515 +done
  17.516 +
  17.517  lemma fields_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk>
  17.518    \<Longrightarrow> \<forall> vn D T. (((vn,D),T) \<in> set (fields (G,C))
  17.519    \<longrightarrow> (is_class G D \<and> ((vn,D),T) \<in> set (fields (G,D))))"
  17.520  apply (erule (1) subcls1_induct)
  17.521  
  17.522  apply clarify
  17.523 +apply (frule wf_prog_ws_prog)
  17.524  apply (frule fields_Object, assumption+)
  17.525  apply (simp only: is_class_Object) apply simp
  17.526  
  17.527  apply clarify
  17.528  apply (frule fields_rec)
  17.529 -apply assumption
  17.530 +apply (simp (no_asm_simp) add: wf_prog_ws_prog)
  17.531  
  17.532  apply (case_tac "Da=C")
  17.533  apply blast			(* case Da=C *)
  17.534 @@ -448,6 +614,7 @@
  17.535  apply clarify
  17.536  apply (frule field_fields)
  17.537  apply (drule map_of_SomeD)
  17.538 +apply (frule wf_prog_ws_prog)
  17.539  apply (drule fields_Object, assumption+)
  17.540  apply simp
  17.541  
  17.542 @@ -460,6 +627,7 @@
  17.543  apply (rule trans [THEN sym], rule sym, assumption)
  17.544  apply (rule_tac x=vn in fun_cong)
  17.545  apply (rule trans, rule field_rec, assumption+)
  17.546 +apply (simp (no_asm_simp) add: wf_prog_ws_prog) 
  17.547  apply (simp (no_asm_use)) apply blast
  17.548  done
  17.549  
  17.550 @@ -478,6 +646,7 @@
  17.551  apply (rule map_of_SomeD)
  17.552  apply (rule table_of_remap_SomeD) 
  17.553  apply assumption+
  17.554 +apply (simp (no_asm_simp) add: wf_prog_ws_prog)+
  17.555  done
  17.556  
  17.557  lemma Call_lemma: 
  17.558 @@ -495,16 +664,15 @@
  17.559  apply auto
  17.560  done
  17.561  
  17.562 -
  17.563  lemma fields_is_type_lemma [rule_format (no_asm)]: 
  17.564 -  "[|is_class G C; wf_prog wf_mb G|] ==>  
  17.565 +  "[|is_class G C; ws_prog G|] ==>  
  17.566    \<forall>f\<in>set (fields (G,C)). is_type G (snd f)"
  17.567 -apply( erule (1) subcls1_induct)
  17.568 +apply( erule (1) subcls1_induct_struct)
  17.569  apply(  frule class_Object)
  17.570  apply(  clarify)
  17.571  apply(  frule fields_rec, assumption)
  17.572 -apply(  drule class_wf, assumption)
  17.573 -apply(  simp add: wf_cdecl_def wf_fdecl_def)
  17.574 +apply(  drule class_wf_struct, assumption)
  17.575 +apply(  simp add: ws_cdecl_def wf_fdecl_def)
  17.576  apply(  fastsimp)
  17.577  apply( subst fields_rec)
  17.578  apply(   fast)
  17.579 @@ -513,34 +681,43 @@
  17.580  apply( safe)
  17.581  prefer 2
  17.582  apply(  force)
  17.583 -apply( drule (1) class_wf)
  17.584 -apply( unfold wf_cdecl_def)
  17.585 +apply( drule (1) class_wf_struct)
  17.586 +apply( unfold ws_cdecl_def)
  17.587  apply( clarsimp)
  17.588  apply( drule (1) bspec)
  17.589  apply( unfold wf_fdecl_def)
  17.590  apply auto
  17.591  done
  17.592  
  17.593 +
  17.594  lemma fields_is_type: 
  17.595 -  "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==>  
  17.596 +  "[|map_of (fields (G,C)) fn = Some f; ws_prog G; is_class G C|] ==>  
  17.597    is_type G f"
  17.598  apply(drule map_of_SomeD)
  17.599  apply(drule (2) fields_is_type_lemma)
  17.600  apply(auto)
  17.601  done
  17.602  
  17.603 +
  17.604 +lemma field_is_type: "\<lbrakk> ws_prog G; is_class G C; field (G, C) fn = Some (fd, fT) \<rbrakk>
  17.605 +  \<Longrightarrow> is_type G fT"
  17.606 +apply (frule_tac f="((fn, fd), fT)" in fields_is_type_lemma)
  17.607 +apply (auto simp add: field_def dest: map_of_SomeD)
  17.608 +done
  17.609 +
  17.610 +
  17.611  lemma methd:
  17.612 -  "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |]
  17.613 +  "[| ws_prog G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |]
  17.614    ==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C"
  17.615  proof -
  17.616 -  assume wf: "wf_prog wf_mb G" and C:  "(C,S,fs,mdecls) \<in> set G" and
  17.617 +  assume wf: "ws_prog G" and C:  "(C,S,fs,mdecls) \<in> set G" and
  17.618           m: "(sig,rT,code) \<in> set mdecls"
  17.619    moreover
  17.620    from wf C have "class G C = Some (S,fs,mdecls)"
  17.621 -    by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
  17.622 +    by (auto simp add: ws_prog_def class_def is_class_def intro: map_of_SomeI)
  17.623    moreover
  17.624    from wf C 
  17.625 -  have "unique mdecls" by (unfold wf_prog_def wf_cdecl_def) auto
  17.626 +  have "unique mdecls" by (unfold ws_prog_def ws_cdecl_def) auto
  17.627    hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)" by (induct mdecls, auto)  
  17.628    with m 
  17.629    have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
  17.630 @@ -553,20 +730,11 @@
  17.631  lemma wf_mb'E:
  17.632    "\<lbrakk> wf_prog wf_mb G; \<And>C S fs ms m.\<lbrakk>(C,S,fs,ms) \<in> set G; m \<in> set ms\<rbrakk> \<Longrightarrow> wf_mb' G C m \<rbrakk>
  17.633    \<Longrightarrow> wf_prog wf_mb' G"
  17.634 -  apply (simp add: wf_prog_def)
  17.635 +  apply (simp only: wf_prog_def)
  17.636    apply auto
  17.637 -  apply (simp add: wf_cdecl_def wf_mdecl_def)
  17.638 +  apply (simp add: wf_cdecl_mdecl_def)
  17.639    apply safe
  17.640    apply (drule bspec, assumption) apply simp
  17.641 -  apply (drule bspec, assumption) apply simp
  17.642 -  apply (drule bspec, assumption) apply simp
  17.643 -  apply clarify apply (drule bspec, assumption) apply simp
  17.644 -  apply (drule bspec, assumption) apply simp
  17.645 -  apply (drule bspec, assumption) apply simp
  17.646 -  apply (drule bspec, assumption) apply simp
  17.647 -  apply (drule bspec, assumption) apply simp
  17.648 -  apply (drule bspec, assumption) apply simp
  17.649 -  apply clarify apply (drule bspec, assumption)+ apply simp
  17.650    done
  17.651  
  17.652  
    18.1 --- a/src/HOL/MicroJava/J/WellType.thy	Mon May 26 11:42:41 2003 +0200
    18.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Mon May 26 18:36:15 2003 +0200
    18.3 @@ -108,19 +108,19 @@
    18.4  -- "local variables might include This, which is hidden anyway"
    18.5  
    18.6  consts
    18.7 -  ty_expr :: "(java_mb env \<times> expr      \<times> ty     ) set"
    18.8 -  ty_exprs:: "(java_mb env \<times> expr list \<times> ty list) set"
    18.9 -  wt_stmt :: "(java_mb env \<times> stmt               ) set"
   18.10 +  ty_expr :: "('c env \<times> expr      \<times> ty     ) set"
   18.11 +  ty_exprs:: "('c env \<times> expr list \<times> ty list) set"
   18.12 +  wt_stmt :: "('c env \<times> stmt               ) set"
   18.13  
   18.14  syntax (xsymbols)
   18.15 -  ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ \<turnstile> _ :: _"   [51,51,51]50)
   18.16 -  ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
   18.17 -  wt_stmt :: "java_mb env =>  stmt                => bool" ("_ \<turnstile> _ \<surd>"      [51,51   ]50)
   18.18 +  ty_expr :: "'c env => [expr     , ty     ] => bool" ("_ \<turnstile> _ :: _"   [51,51,51]50)
   18.19 +  ty_exprs:: "'c env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
   18.20 +  wt_stmt :: "'c env =>  stmt                => bool" ("_ \<turnstile> _ \<surd>"      [51,51   ]50)
   18.21  
   18.22  syntax
   18.23 -  ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ |- _ :: _"   [51,51,51]50)
   18.24 -  ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
   18.25 -  wt_stmt :: "java_mb env =>  stmt                => bool" ("_ |- _ [ok]"   [51,51   ]50)
   18.26 +  ty_expr :: "'c env => [expr     , ty     ] => bool" ("_ |- _ :: _"   [51,51,51]50)
   18.27 +  ty_exprs:: "'c env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
   18.28 +  wt_stmt :: "'c env =>  stmt                => bool" ("_ |- _ [ok]"   [51,51   ]50)
   18.29  
   18.30  
   18.31  translations
   18.32 @@ -134,9 +134,9 @@
   18.33           E\<turnstile>NewC C::Class C"  -- "cf. 15.8"
   18.34  
   18.35    -- "cf. 15.15"
   18.36 -  Cast: "[| E\<turnstile>e::Class C; is_class (prg E) D;
   18.37 -            prg E\<turnstile>C\<preceq>? D |] ==>
   18.38 -         E\<turnstile>Cast D e::Class D"
   18.39 +  Cast: "[| E\<turnstile>e::C; is_class (prg E) D;
   18.40 +            prg E\<turnstile>C\<preceq>? Class D |] ==>
   18.41 +         E\<turnstile>Cast D e:: Class D"
   18.42  
   18.43    -- "cf. 15.7.1"
   18.44    Lit:    "[| typeof (\<lambda>v. None) x = Some T |] ==>
   18.45 @@ -213,7 +213,7 @@
   18.46  
   18.47  constdefs
   18.48  
   18.49 - wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool"
   18.50 + wf_java_mdecl :: "'c prog => cname => java_mb mdecl => bool"
   18.51  "wf_java_mdecl G C == \<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
   18.52    length pTs = length pns \<and>
   18.53    distinct pns \<and>
   18.54 @@ -225,25 +225,22 @@
   18.55     E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
   18.56  
   18.57  syntax 
   18.58 - wf_java_prog :: "java_mb prog => bool"
   18.59 + wf_java_prog :: "'c prog => bool"
   18.60  translations
   18.61    "wf_java_prog" == "wf_prog wf_java_mdecl"
   18.62  
   18.63  lemma wf_java_prog_wf_java_mdecl: "\<lbrakk> 
   18.64    wf_java_prog G; (C, D, fds, mths) \<in> set G; jmdcl \<in> set mths \<rbrakk>
   18.65    \<Longrightarrow> wf_java_mdecl G C jmdcl"
   18.66 -apply (simp add: wf_prog_def) 
   18.67 -apply (simp add: wf_cdecl_def)
   18.68 +apply (simp only: wf_prog_def) 
   18.69  apply (erule conjE)+
   18.70  apply (drule bspec, assumption)
   18.71 -apply simp
   18.72 -apply (erule conjE)+
   18.73 -apply (drule bspec, assumption)
   18.74 -apply (simp add: wf_mdecl_def split_beta)
   18.75 +apply (simp add: wf_cdecl_mdecl_def split_beta)
   18.76  done
   18.77  
   18.78 -lemma wt_is_type: "(E\<turnstile>e::T \<longrightarrow> wf_prog wf_mb (prg E) \<longrightarrow> is_type (prg E) T) \<and>  
   18.79 -       (E\<turnstile>es[::]Ts \<longrightarrow> wf_prog wf_mb (prg E) \<longrightarrow> Ball (set Ts) (is_type (prg E))) \<and> 
   18.80 +
   18.81 +lemma wt_is_type: "(E\<turnstile>e::T \<longrightarrow> ws_prog (prg E) \<longrightarrow> is_type (prg E) T) \<and>  
   18.82 +       (E\<turnstile>es[::]Ts \<longrightarrow> ws_prog (prg E) \<longrightarrow> Ball (set Ts) (is_type (prg E))) \<and> 
   18.83         (E\<turnstile>c \<surd> \<longrightarrow> True)"
   18.84  apply (rule ty_expr_ty_exprs_wt_stmt.induct)
   18.85  apply auto
   18.86 @@ -253,10 +250,15 @@
   18.87  apply ( drule (1) fields_is_type)
   18.88  apply (  simp (no_asm_simp))
   18.89  apply  (assumption)
   18.90 -apply (auto dest!: max_spec2mheads method_wf_mdecl is_type_rTI 
   18.91 +apply (auto dest!: max_spec2mheads method_wf_mhead is_type_rTI 
   18.92              simp add: wf_mdecl_def)
   18.93  done
   18.94  
   18.95  lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, rule_format]
   18.96  
   18.97 +lemma expr_class_is_class: "
   18.98 +  \<lbrakk>ws_prog (prg E); E \<turnstile> e :: Class C\<rbrakk> \<Longrightarrow> is_class (prg E) C"
   18.99 +  by (frule ty_expr_is_type, assumption, simp)
  18.100 +
  18.101 +
  18.102  end