1.1 --- a/doc-src/IsarRef/conversion.tex	Sun Sep 03 20:01:27 2000 +0200
     1.2 +++ b/doc-src/IsarRef/conversion.tex	Sun Sep 03 20:01:47 2000 +0200
     1.3 @@ -21,7 +21,9 @@
     1.4  %  \texttt{} & & \\
     1.5    \texttt{stac}~a~1 & & subst~a \\
     1.6    \texttt{strip_tac}~1 & & intro~strip & \Text{(HOL)} \\
     1.7 -  \texttt{split_all_tac} & \ll & clarify & \Text{(HOL)} \\
     1.8 +  \texttt{split_all_tac} & & simp~(no_asm_simp)~only: split_paired_all & \Text{(HOL)} \\
     1.9 +                         & \approx & simp~only: split_tupled_all & \Text{(HOL)} \\
    1.10 +                         & \ll & clarify & \Text{(HOL)} \\
    1.11  \end{matharray}
    1.12  
    1.13  

     2.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sun Sep 03 20:01:27 2000 +0200
     2.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sun Sep 03 20:01:47 2000 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4  apply (unfold correct_state_def Let_def correct_frame_def)
     2.5  apply simp
     2.6  apply (blast intro: wt_jvm_prog_impl_wt_instr)
     2.7 -.
     2.8 +done
     2.9  
    2.10  lemma Load_correct:
    2.11  "\<lbrakk> wf_prog wt G;
    2.12 @@ -36,7 +36,7 @@
    2.13   apply (rule approx_loc_imp_approx_val_sup)
    2.14   apply simp+
    2.15  apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
    2.16 -.
    2.17 +done
    2.18  
    2.19  lemma Store_correct:
    2.20  "\<lbrakk> wf_prog wt G;
    2.21 @@ -50,7 +50,7 @@
    2.22  apply (rule conjI)
    2.23   apply (blast intro: approx_stk_imp_approx_stk_sup)
    2.24  apply (blast intro: approx_loc_imp_approx_loc_subst approx_loc_imp_approx_loc_sup)
    2.25 -.
    2.26 +done
    2.27  
    2.28  
    2.29  lemma conf_Intg_Integer [iff]:
    2.30 @@ -65,10 +65,10 @@
    2.31    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    2.32    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
    2.33    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
    2.34 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
    2.35 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    2.36  apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
    2.37  apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
    2.38 -.
    2.39 +done
    2.40  
    2.41  lemma NT_subtype_conv:
    2.42    "G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))"
    2.43 @@ -78,7 +78,7 @@
    2.44      apply auto
    2.45      apply (case_tac R)
    2.46      apply auto
    2.47 -    .
    2.48 +    done
    2.49    note l = this
    2.50  
    2.51    show ?thesis 
    2.52 @@ -92,12 +92,12 @@
    2.53    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    2.54    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
    2.55    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
    2.56 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
    2.57 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    2.58  apply (clarsimp simp add: defs1 map_eq_Cons)
    2.59  apply (rule conjI)
    2.60   apply (force simp add: approx_val_Null NT_subtype_conv)
    2.61  apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
    2.62 -.
    2.63 +done
    2.64  
    2.65  
    2.66  lemma Cast_conf2:
    2.67 @@ -110,7 +110,7 @@
    2.68  apply (clarsimp simp add: conf_def obj_ty_def)
    2.69  apply (cases v)
    2.70  apply (auto intro: null rtrancl_trans)
    2.71 -.
    2.72 +done
    2.73  
    2.74  
    2.75  lemma Checkcast_correct:
    2.76 @@ -123,7 +123,7 @@
    2.77  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    2.78  apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
    2.79  apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2)
    2.80 -.
    2.81 +done
    2.82  
    2.83  
    2.84  lemma Getfield_correct:
    2.85 @@ -133,7 +133,7 @@
    2.86    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    2.87    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
    2.88    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
    2.89 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
    2.90 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    2.91  apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split)
    2.92  apply (frule conf_widen)
    2.93  apply assumption+
    2.94 @@ -144,7 +144,7 @@
    2.95   apply assumption+
    2.96   apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def)
    2.97  apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
    2.98 -.
    2.99 +done
   2.100  
   2.101  lemma Putfield_correct:
   2.102  "\<lbrakk> wf_prog wt G;
   2.103 @@ -153,7 +153,7 @@
   2.104    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   2.105    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   2.106    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   2.107 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
   2.108 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   2.109  apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split)
   2.110  apply (clarsimp simp add: approx_val_def)
   2.111  apply (frule conf_widen)
   2.112 @@ -162,11 +162,12 @@
   2.113  apply assumption
   2.114  apply (drule conf_RefTD)
   2.115  apply clarsimp
   2.116 -apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup
   2.117 -		approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
   2.118 -		hconf_imp_hconf_field_update
   2.119 -		correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields)
   2.120 -.
   2.121 +apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap
   2.122 +  approx_stk_imp_approx_stk_sup
   2.123 +  approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
   2.124 +  hconf_imp_hconf_field_update
   2.125 +  correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields)
   2.126 +done
   2.127  
   2.128  lemma collapse_paired_All:
   2.129    "(\<forall>x y. P(x,y)) = (\<forall>z. P z)"
   2.130 @@ -190,7 +191,7 @@
   2.131                     correct_init_obj simp add:  NT_subtype_conv approx_val_def conf_def
   2.132  		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
   2.133         split: option.split)
   2.134 -.
   2.135 +done
   2.136  
   2.137  
   2.138  (****** Method Invocation ******)
   2.139 @@ -442,14 +443,14 @@
   2.140  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   2.141  apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm)
   2.142  apply (frule wt_jvm_prog_impl_wt_instr)
   2.143 -apply (tactic "EVERY1[atac, etac Suc_lessD]")
   2.144 +apply (assumption, erule Suc_lessD)
   2.145  apply (unfold wt_jvm_prog_def)
   2.146 -apply (tactic {* fast_tac (claset()
   2.147 - addDs [thm "subcls_widen_methd"]
   2.148 - addEs [rotate_prems 1 widen_trans]
   2.149 - addIs [conf_widen]
   2.150 - addss (simpset() addsimps [thm "approx_val_def",thm "append_eq_conv_conj", map_eq_Cons]@thms "defs1")) 1 *})
   2.151 -.
   2.152 +apply (fastsimp
   2.153 +  dest: subcls_widen_methd
   2.154 +  elim: widen_trans [COMP swap_prems_rl]
   2.155 +  intro: conf_widen
   2.156 +  simp: approx_val_def append_eq_conv_conj map_eq_Cons defs1)
   2.157 +done
   2.158  
   2.159  lemmas [simp] = map_append
   2.160  
   2.161 @@ -463,7 +464,7 @@
   2.162  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   2.163  apply (clarsimp simp add: defs1)
   2.164  apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
   2.165 -.
   2.166 +done
   2.167  
   2.168  
   2.169  lemma Ifcmpeq_correct:
   2.170 @@ -476,7 +477,7 @@
   2.171  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   2.172  apply (clarsimp simp add: defs1)
   2.173  apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
   2.174 -.
   2.175 +done
   2.176  
   2.177  lemma Pop_correct:
   2.178  "\<lbrakk> wf_prog wt G; 
   2.179 @@ -488,7 +489,7 @@
   2.180  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   2.181  apply (clarsimp simp add: defs1)
   2.182  apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
   2.183 -.
   2.184 +done
   2.185  
   2.186  lemma Dup_correct:
   2.187  "\<lbrakk> wf_prog wt G; 
   2.188 @@ -501,7 +502,7 @@
   2.189  apply (clarsimp simp add: defs1 map_eq_Cons)
   2.190  apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   2.191               simp add: defs1 map_eq_Cons)
   2.192 -.
   2.193 +done
   2.194  
   2.195  lemma Dup_x1_correct:
   2.196  "\<lbrakk> wf_prog wt G; 
   2.197 @@ -514,7 +515,7 @@
   2.198  apply (clarsimp simp add: defs1 map_eq_Cons)
   2.199  apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   2.200               simp add: defs1 map_eq_Cons)
   2.201 -.
   2.202 +done
   2.203  
   2.204  lemma Dup_x2_correct:
   2.205  "\<lbrakk> wf_prog wt G; 
   2.206 @@ -527,7 +528,7 @@
   2.207  apply (clarsimp simp add: defs1 map_eq_Cons)
   2.208  apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   2.209               simp add: defs1 map_eq_Cons)
   2.210 -.
   2.211 +done
   2.212  
   2.213  lemma Swap_correct:
   2.214  "\<lbrakk> wf_prog wt G; 
   2.215 @@ -540,7 +541,7 @@
   2.216  apply (clarsimp simp add: defs1 map_eq_Cons)
   2.217  apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   2.218               simp add: defs1 map_eq_Cons)
   2.219 -.
   2.220 +done
   2.221  
   2.222  lemma IAdd_correct:
   2.223  "\<lbrakk> wf_prog wt G; 
   2.224 @@ -552,7 +553,7 @@
   2.225  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   2.226  apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
   2.227  apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup)
   2.228 -.
   2.229 +done
   2.230  
   2.231  
   2.232  (** instr correct **)
   2.233 @@ -575,7 +576,7 @@
   2.234         Checkcast_correct Getfield_correct Putfield_correct New_correct 
   2.235         Goto_correct Ifcmpeq_correct Pop_correct Dup_correct 
   2.236         Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+
   2.237 -.
   2.238 +done
   2.239  
   2.240  
   2.241  (** Main **)
   2.242 @@ -588,19 +589,19 @@
   2.243  
   2.244  lemma BV_correct_1 [rulify]:
   2.245  "\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> 
   2.246 - \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
   2.247 -apply (tactic "split_all_tac 1")
   2.248 + \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   2.249 +apply (simp only: split_tupled_all)
   2.250  apply (rename_tac xp hp frs)
   2.251  apply (case_tac xp)
   2.252   apply (case_tac frs)
   2.253    apply simp
   2.254 - apply (tactic "split_all_tac 1")
   2.255 - apply (tactic "hyp_subst_tac 1")
   2.256 + apply (simp only: split_tupled_all)
   2.257 + apply hypsubst
   2.258   apply (frule correct_state_impl_Some_method)
   2.259   apply (force intro: instr_correct)
   2.260  apply (case_tac frs)
   2.261 -apply simp+
   2.262 -.
   2.263 +apply simp_all
   2.264 +done
   2.265  
   2.266  
   2.267  lemma L0:
   2.268 @@ -613,7 +614,7 @@
   2.269  apply (drule L0)
   2.270  apply assumption
   2.271  apply (fast intro: BV_correct_1)
   2.272 -.
   2.273 +done
   2.274  
   2.275  
   2.276  theorem BV_correct [rulify]:
   2.277 @@ -622,7 +623,7 @@
   2.278  apply (erule rtrancl_induct)
   2.279   apply simp
   2.280  apply (auto intro: BV_correct_1)
   2.281 -.
   2.282 +done
   2.283  
   2.284  
   2.285  theorem BV_correct_initial:
   2.286 @@ -631,6 +632,6 @@
   2.287  apply (drule BV_correct)
   2.288  apply assumption+
   2.289  apply (simp add: correct_state_def correct_frame_def split_def split: option.splits)
   2.290 -.
   2.291 +done
   2.292  
   2.293  end