tuned
authorkleing
Fri Aug 11 14:52:52 2000 +0200 (2000-08-11)
changeset 9580d955914193e0
parent 9579 28e26f468f08
child 9581 b295382e1549
tuned
src/HOL/MicroJava/BV/LBVComplete.thy
src/HOL/MicroJava/BV/LBVCorrect.thy
src/HOL/MicroJava/BV/Step.thy
src/HOL/MicroJava/BV/StepMono.thy
     1.1 --- a/src/HOL/MicroJava/BV/LBVComplete.thy	Fri Aug 11 14:52:39 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Fri Aug 11 14:52:52 2000 +0200
     1.3 @@ -10,61 +10,61 @@
     1.4  
     1.5  
     1.6  constdefs
     1.7 -  is_approx :: "['a option list, 'a list] \\<Rightarrow> bool"
     1.8 -  "is_approx a b \\<equiv> length a = length b \\<and> (\\<forall> n. n < length a \\<longrightarrow>
     1.9 -                   (a!n = None \\<or> a!n = Some (b!n)))"
    1.10 +  is_approx :: "['a option list, 'a list] \<Rightarrow> bool"
    1.11 +  "is_approx a b \<equiv> length a = length b \<and> (\<forall> n. n < length a \<longrightarrow>
    1.12 +                   (a!n = None \<or> a!n = Some (b!n)))"
    1.13    
    1.14 -  contains_dead :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
    1.15 -  "contains_dead ins cert phi pc \\<equiv>
    1.16 -     Suc pc \\<notin> succs (ins!pc) pc \\<and> Suc pc < length phi \\<longrightarrow>
    1.17 +  contains_dead :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
    1.18 +  "contains_dead ins cert phi pc \<equiv>
    1.19 +     Suc pc \<notin> succs (ins!pc) pc \<and> Suc pc < length phi \<longrightarrow>
    1.20       cert ! (Suc pc) = Some (phi ! Suc pc)"
    1.21  
    1.22 -  contains_targets :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
    1.23 -  "contains_targets ins cert phi pc \\<equiv> (
    1.24 -     \\<forall> pc' \\<in> succs (ins!pc) pc. pc' \\<noteq> Suc pc \\<and> pc' < length phi \\<longrightarrow> 
    1.25 +  contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
    1.26 +  "contains_targets ins cert phi pc \<equiv> (
    1.27 +     \<forall> pc' \<in> succs (ins!pc) pc. pc' \<noteq> Suc pc \<and> pc' < length phi \<longrightarrow> 
    1.28       cert!pc' = Some (phi!pc'))" 
    1.29  
    1.30  
    1.31 -  fits :: "[instr list, certificate, method_type] \\<Rightarrow> bool"
    1.32 -  "fits ins cert phi \\<equiv> is_approx cert phi \\<and> length ins < length phi \\<and>
    1.33 -                            (\\<forall> pc. pc < length ins \\<longrightarrow>
    1.34 -                                   contains_dead ins cert phi pc \\<and> 
    1.35 +  fits :: "[instr list, certificate, method_type] \<Rightarrow> bool"
    1.36 +  "fits ins cert phi \<equiv> is_approx cert phi \<and> length ins < length phi \<and>
    1.37 +                            (\<forall> pc. pc < length ins \<longrightarrow>
    1.38 +                                   contains_dead ins cert phi pc \<and> 
    1.39                                     contains_targets ins cert phi pc)"
    1.40  
    1.41 -  is_target :: "[instr list, p_count] \\<Rightarrow> bool" 
    1.42 -  "is_target ins pc \\<equiv> \\<exists> pc'. pc' < length ins \\<and> pc \\<in> succs (ins!pc') pc'"
    1.43 +  is_target :: "[instr list, p_count] \<Rightarrow> bool" 
    1.44 +  "is_target ins pc \<equiv> \<exists> pc'. pc' < length ins \<and> pc \<in> succs (ins!pc') pc'"
    1.45  
    1.46 -  maybe_dead :: "[instr list, p_count] \\<Rightarrow> bool"
    1.47 -  "maybe_dead ins pc \\<equiv> \\<exists> pc'. pc = pc'+1 \\<and> pc \\<notin> succs (ins!pc') pc'"
    1.48 +  maybe_dead :: "[instr list, p_count] \<Rightarrow> bool"
    1.49 +  "maybe_dead ins pc \<equiv> \<exists> pc'. pc = pc'+1 \<and> pc \<notin> succs (ins!pc') pc'"
    1.50  
    1.51 -  mdot :: "[instr list, p_count] \\<Rightarrow> bool"
    1.52 -  "mdot ins pc \\<equiv> maybe_dead ins pc \\<or> is_target ins pc"
    1.53 +  mdot :: "[instr list, p_count] \<Rightarrow> bool"
    1.54 +  "mdot ins pc \<equiv> maybe_dead ins pc \<or> is_target ins pc"
    1.55  
    1.56  
    1.57  consts
    1.58 -  option_filter_n :: "['a list, nat \\<Rightarrow> bool, nat] \\<Rightarrow> 'a option list"
    1.59 +  option_filter_n :: "['a list, nat \<Rightarrow> bool, nat] \<Rightarrow> 'a option list"
    1.60  primrec 
    1.61    "option_filter_n []    P n = []"  
    1.62    "option_filter_n (h#t) P n = (if (P n) then Some h # option_filter_n t P (n+1) 
    1.63                                           else None   # option_filter_n t P (n+1))"  
    1.64    
    1.65  constdefs 
    1.66 -  option_filter :: "['a list, nat \\<Rightarrow> bool] \\<Rightarrow> 'a option list" 
    1.67 -  "option_filter l P \\<equiv> option_filter_n l P 0" 
    1.68 +  option_filter :: "['a list, nat \<Rightarrow> bool] \<Rightarrow> 'a option list" 
    1.69 +  "option_filter l P \<equiv> option_filter_n l P 0" 
    1.70    
    1.71 -  make_cert :: "[instr list, method_type] \\<Rightarrow> certificate"
    1.72 -  "make_cert ins phi \\<equiv> option_filter phi (mdot ins)"
    1.73 +  make_cert :: "[instr list, method_type] \<Rightarrow> certificate"
    1.74 +  "make_cert ins phi \<equiv> option_filter phi (mdot ins)"
    1.75    
    1.76 -  make_Cert :: "[jvm_prog, prog_type] \\<Rightarrow> prog_certificate"
    1.77 -  "make_Cert G Phi \\<equiv>  \\<lambda> C sig.
    1.78 -    let (C,x,y,mdecls) = \\<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\<in> set G \\<and> Cl = C in
    1.79 -      let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in
    1.80 +  make_Cert :: "[jvm_prog, prog_type] \<Rightarrow> prog_certificate"
    1.81 +  "make_Cert G Phi \<equiv>  \<lambda> C sig.
    1.82 +    let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C in
    1.83 +      let (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig in
    1.84          make_cert b (Phi C sig)"
    1.85    
    1.86  
    1.87  lemmas [simp del] = split_paired_Ex
    1.88  
    1.89 -lemma length_ofn [rulify]: "\\<forall>n. length (option_filter_n l P n) = length l"
    1.90 +lemma length_ofn [rulify]: "\<forall>n. length (option_filter_n l P n) = length l"
    1.91    by (induct l) auto
    1.92  
    1.93  
    1.94 @@ -72,7 +72,7 @@
    1.95  proof -
    1.96    {
    1.97      fix a n
    1.98 -    have "\\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a")
    1.99 +    have "\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a")
   1.100      proof (induct a)
   1.101        show "?P []" by (auto simp add: is_approx_def)
   1.102      
   1.103 @@ -89,7 +89,7 @@
   1.104          assume "m < length (option_filter_n (l # ls) P n)"
   1.105          hence m: "m < Suc (length ls)" by (simp only: length_ofn) simp
   1.106        
   1.107 -        show "option_filter_n (l # ls) P n ! m = None \\<or>
   1.108 +        show "option_filter_n (l # ls) P n ! m = None \<or>
   1.109                option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)" 
   1.110          proof (cases "m")
   1.111            assume "m = 0"
   1.112 @@ -102,7 +102,7 @@
   1.113              from m Suc
   1.114              show "m' < length (option_filter_n ls P (Suc n))" by (simp add: length_ofn)
   1.115            
   1.116 -            assume "option_filter_n ls P (Suc n) ! m' = None \\<or> 
   1.117 +            assume "option_filter_n ls P (Suc n) ! m' = None \<or> 
   1.118                      option_filter_n ls P (Suc n) ! m' = Some (ls ! m')"
   1.119              with m Suc
   1.120              show ?thesis by auto
   1.121 @@ -117,12 +117,12 @@
   1.122  qed
   1.123  
   1.124  lemma option_filter_Some:
   1.125 -"\\<lbrakk>n < length l; P n\\<rbrakk> \\<Longrightarrow> option_filter l P ! n = Some (l!n)"
   1.126 +"\<lbrakk>n < length l; P n\<rbrakk> \<Longrightarrow> option_filter l P ! n = Some (l!n)"
   1.127  proof -
   1.128    
   1.129    assume 1: "n < length l" "P n"
   1.130  
   1.131 -  have "\\<forall>n n'. n < length l \\<longrightarrow> P (n+n') \\<longrightarrow>  option_filter_n l P n' ! n = Some (l!n)"
   1.132 +  have "\<forall>n n'. n < length l \<longrightarrow> P (n+n') \<longrightarrow>  option_filter_n l P n' ! n = Some (l!n)"
   1.133      (is "?P l")
   1.134    proof (induct l)
   1.135      show "?P []" by simp
   1.136 @@ -154,13 +154,13 @@
   1.137    by (auto intro: option_filter_Some simp add: contains_dead_def mdot_def maybe_dead_def)
   1.138  
   1.139  lemma option_filter_contains_targets:
   1.140 -"pc < length ins \\<Longrightarrow> contains_targets ins (option_filter phi (mdot ins)) phi pc"
   1.141 +"pc < length ins \<Longrightarrow> contains_targets ins (option_filter phi (mdot ins)) phi pc"
   1.142  proof (unfold contains_targets_def, clarsimp)
   1.143   
   1.144    fix pc'
   1.145    assume "pc < length ins" 
   1.146 -         "pc' \\<in> succs (ins ! pc) pc" 
   1.147 -         "pc' \\<noteq> Suc pc" and
   1.148 +         "pc' \<in> succs (ins ! pc) pc" 
   1.149 +         "pc' \<noteq> Suc pc" and
   1.150      pc': "pc' < length phi"
   1.151  
   1.152    hence "is_target ins pc'" by (auto simp add: is_target_def)
   1.153 @@ -172,7 +172,7 @@
   1.154    
   1.155  
   1.156  lemma fits_make_cert:
   1.157 -  "length ins < length phi \\<Longrightarrow> fits ins (make_cert ins phi) phi"
   1.158 +  "length ins < length phi \<Longrightarrow> fits ins (make_cert ins phi) phi"
   1.159  proof -
   1.160    assume l: "length ins < length phi"
   1.161  
   1.162 @@ -194,25 +194,25 @@
   1.163  qed
   1.164  
   1.165  lemma fitsD: 
   1.166 -"\\<lbrakk>fits ins cert phi; pc' \\<in> succs (ins!pc) pc; pc' \\<noteq> Suc pc; pc < length ins; pc' < length ins\\<rbrakk> 
   1.167 -  \\<Longrightarrow> cert!pc' = Some (phi!pc')"
   1.168 +"\<lbrakk>fits ins cert phi; pc' \<in> succs (ins!pc) pc; pc' \<noteq> Suc pc; pc < length ins; pc' < length ins\<rbrakk> 
   1.169 +  \<Longrightarrow> cert!pc' = Some (phi!pc')"
   1.170  by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
   1.171  
   1.172  lemma fitsD2:
   1.173 -"\\<lbrakk>fits ins cert phi; Suc pc \\<notin> succs (ins!pc) pc;  pc < length ins\\<rbrakk> 
   1.174 -  \\<Longrightarrow> cert ! Suc pc = Some (phi ! Suc pc)"
   1.175 +"\<lbrakk>fits ins cert phi; Suc pc \<notin> succs (ins!pc) pc;  pc < length ins\<rbrakk> 
   1.176 +  \<Longrightarrow> cert ! Suc pc = Some (phi ! Suc pc)"
   1.177  by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
   1.178  
   1.179  
   1.180  lemma wtl_inst_mono:
   1.181 -"\\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; 
   1.182 -  G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow> 
   1.183 - \\<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')";
   1.184 +"\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; 
   1.185 +  G \<turnstile> s2 <=s s1; i = ins!pc\<rbrakk> \<Longrightarrow> 
   1.186 + \<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \<and> (G \<turnstile> s2' <=s s1')"
   1.187  proof -
   1.188    assume pc:   "pc < length ins" "i = ins!pc"
   1.189    assume wtl:  "wtl_inst i G rT s1 s1' cert mpc pc"
   1.190    assume fits: "fits ins cert phi"
   1.191 -  assume G:    "G \\<turnstile> s2 <=s s1"
   1.192 +  assume G:    "G \<turnstile> s2 <=s s1"
   1.193    
   1.194    let "?step s" = "step (i, G, s)"
   1.195  
   1.196 @@ -220,40 +220,40 @@
   1.197    have app: "app (i, G, rT, s2)" by (auto simp add: wtl_inst_def app_mono)
   1.198    
   1.199    from wtl G
   1.200 -  have step: "succs i pc \\<noteq> {} \\<Longrightarrow> G \\<turnstile> the (?step s2) <=s the (?step s1)" 
   1.201 +  have step: "succs i pc \<noteq> {} \<Longrightarrow> G \<turnstile> the (?step s2) <=s the (?step s1)" 
   1.202      by - (drule step_mono, auto simp add: wtl_inst_def)
   1.203    
   1.204    with app
   1.205 -  have some: "succs i pc \\<noteq> {} \\<Longrightarrow> ?step s2 \\<noteq> None" by (simp add: app_step_some)
   1.206 +  have some: "succs i pc \<noteq> {} \<Longrightarrow> ?step s2 \<noteq> None" by (simp add: app_step_some)
   1.207  
   1.208    {
   1.209      fix pc'
   1.210 -    assume 0: "pc' \\<in> succs i pc" "pc' \\<noteq> pc+1"
   1.211 -    hence "succs i pc \\<noteq> {}" by auto
   1.212 -    hence "G \\<turnstile> the (?step s2) <=s the (?step s1)" by (rule step)
   1.213 +    assume 0: "pc' \<in> succs i pc" "pc' \<noteq> pc+1"
   1.214 +    hence "succs i pc \<noteq> {}" by auto
   1.215 +    hence "G \<turnstile> the (?step s2) <=s the (?step s1)" by (rule step)
   1.216      also 
   1.217      from wtl 0
   1.218 -    have "G \\<turnstile> the (?step s1) <=s the (cert!pc')"
   1.219 +    have "G \<turnstile> the (?step s1) <=s the (cert!pc')"
   1.220        by (auto simp add: wtl_inst_def) 
   1.221      finally
   1.222 -    have "G\\<turnstile> the (?step s2) <=s the (cert!pc')" .
   1.223 +    have "G\<turnstile> the (?step s2) <=s the (cert!pc')" .
   1.224    } note cert = this
   1.225      
   1.226 -  have "\\<exists>s2'. wtl_inst i G rT s2 s2' cert mpc pc \\<and> G \\<turnstile> s2' <=s s1'"
   1.227 -  proof (cases "pc+1 \\<in> succs i pc")
   1.228 +  have "\<exists>s2'. wtl_inst i G rT s2 s2' cert mpc pc \<and> G \<turnstile> s2' <=s s1'"
   1.229 +  proof (cases "pc+1 \<in> succs i pc")
   1.230      case True
   1.231      with wtl
   1.232      have s1': "s1' = the (?step s1)" by (simp add: wtl_inst_def)
   1.233  
   1.234 -    have "wtl_inst i G rT s2 (the (?step s2)) cert mpc pc \\<and> G \\<turnstile> (the (?step s2)) <=s s1'" 
   1.235 -      (is "?wtl \\<and> ?G")
   1.236 +    have "wtl_inst i G rT s2 (the (?step s2)) cert mpc pc \<and> G \<turnstile> (the (?step s2)) <=s s1'" 
   1.237 +      (is "?wtl \<and> ?G")
   1.238      proof
   1.239        from True s1'
   1.240        show ?G by (auto intro: step)
   1.241  
   1.242        from True app wtl
   1.243        show ?wtl
   1.244 -        by (clarsimp intro: cert simp add: wtl_inst_def)
   1.245 +        by (clarsimp intro!: cert simp add: wtl_inst_def)
   1.246      qed
   1.247      thus ?thesis by blast
   1.248    next
   1.249 @@ -262,8 +262,8 @@
   1.250      have "s1' = the (cert ! Suc pc)" by (simp add: wtl_inst_def)
   1.251  
   1.252      with False app wtl
   1.253 -    have "wtl_inst i G rT s2 s1' cert mpc pc \\<and> G \\<turnstile> s1' <=s s1'"
   1.254 -      by (clarsimp intro: cert simp add: wtl_inst_def)
   1.255 +    have "wtl_inst i G rT s2 s1' cert mpc pc \<and> G \<turnstile> s1' <=s s1'"
   1.256 +      by (clarsimp intro!: cert simp add: wtl_inst_def)
   1.257  
   1.258      thus ?thesis by blast
   1.259    qed
   1.260 @@ -273,76 +273,76 @@
   1.261      
   1.262  
   1.263  lemma wtl_option_mono:
   1.264 -"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; 
   1.265 -  pc < length ins; G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow> 
   1.266 - \\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
   1.267 +"\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; 
   1.268 +  pc < length ins; G \<turnstile> s2 <=s s1; i = ins!pc\<rbrakk> \<Longrightarrow> 
   1.269 + \<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \<and> (G \<turnstile> s2' <=s s1')"
   1.270  proof -
   1.271    assume wtl:  "wtl_inst_option i G rT s1 s1' cert mpc pc" and
   1.272           fits: "fits ins cert phi" "pc < length ins"
   1.273 -               "G \\<turnstile> s2 <=s s1" "i = ins!pc"
   1.274 +               "G \<turnstile> s2 <=s s1" "i = ins!pc"
   1.275  
   1.276    show ?thesis
   1.277    proof (cases "cert!pc")
   1.278      case None
   1.279 -    with wtl fits;
   1.280 -    show ?thesis; 
   1.281 -      by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+);
   1.282 +    with wtl fits
   1.283 +    show ?thesis 
   1.284 +      by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+)
   1.285    next
   1.286      case Some
   1.287 -    with wtl fits;
   1.288 +    with wtl fits
   1.289  
   1.290 -    have G: "G \\<turnstile> s2 <=s a"
   1.291 +    have G: "G \<turnstile> s2 <=s a"
   1.292       by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+)
   1.293  
   1.294      from Some wtl
   1.295 -    have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def)
   1.296 +    have "wtl_inst i G rT a s1' cert mpc pc" by (simp add: wtl_inst_option_def)
   1.297  
   1.298      with G fits
   1.299 -    have "\\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
   1.300 -      by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+);
   1.301 +    have "\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \<and> (G \<turnstile> s2' <=s s1')"
   1.302 +      by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+)
   1.303      
   1.304 -    with Some G;
   1.305 -    show ?thesis; by (simp add: wtl_inst_option_def);
   1.306 +    with Some G
   1.307 +    show ?thesis by (simp add: wtl_inst_option_def)
   1.308    qed
   1.309  qed
   1.310  
   1.311  
   1.312      
   1.313  lemma wt_instr_imp_wtl_inst:
   1.314 -"\\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
   1.315 -  pc < length ins; length ins = max_pc\\<rbrakk> \\<Longrightarrow> 
   1.316 -  \\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
   1.317 +"\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
   1.318 +  pc < length ins; length ins = max_pc\<rbrakk> \<Longrightarrow> 
   1.319 +  \<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \<and> G \<turnstile> s <=s phi ! Suc pc"
   1.320  proof -
   1.321    assume wt:   "wt_instr (ins!pc) G rT phi max_pc pc" 
   1.322    assume fits: "fits ins cert phi"
   1.323    assume pc:   "pc < length ins" "length ins = max_pc"
   1.324  
   1.325    from wt 
   1.326 -  have app: "app (ins!pc, G, rT, phi!pc)" by (simp add: wt_instr_def);
   1.327 +  have app: "app (ins!pc, G, rT, phi!pc)" by (simp add: wt_instr_def)
   1.328  
   1.329    from wt pc
   1.330 -  have pc': "!!pc'. pc' \\<in> succs (ins!pc) pc \\<Longrightarrow> pc' < length ins"
   1.331 +  have pc': "!!pc'. pc' \<in> succs (ins!pc) pc \<Longrightarrow> pc' < length ins"
   1.332      by (simp add: wt_instr_def)
   1.333  
   1.334    let ?s' = "the (step (ins!pc,G, phi!pc))"
   1.335  
   1.336    from wt
   1.337 -  have G: "!!pc'. pc' \\<in> succs (ins!pc) pc \\<Longrightarrow> G \\<turnstile> ?s' <=s phi ! pc'"
   1.338 +  have G: "!!pc'. pc' \<in> succs (ins!pc) pc \<Longrightarrow> G \<turnstile> ?s' <=s phi ! pc'"
   1.339      by (simp add: wt_instr_def)
   1.340  
   1.341    from wt fits pc
   1.342 -  have cert: "!!pc'. \\<lbrakk>pc' \\<in> succs (ins!pc) pc; pc' < max_pc; pc' \\<noteq> pc+1\\<rbrakk> 
   1.343 -    \\<Longrightarrow> cert!pc' \\<noteq> None \\<and> G \\<turnstile> ?s' <=s the (cert!pc')"
   1.344 +  have cert: "!!pc'. \<lbrakk>pc' \<in> succs (ins!pc) pc; pc' < max_pc; pc' \<noteq> pc+1\<rbrakk> 
   1.345 +    \<Longrightarrow> cert!pc' \<noteq> None \<and> G \<turnstile> ?s' <=s the (cert!pc')"
   1.346      by (auto dest: fitsD simp add: wt_instr_def)
   1.347  
   1.348    show ?thesis
   1.349 -  proof (cases "pc+1 \\<in> succs (ins!pc) pc")
   1.350 +  proof (cases "pc+1 \<in> succs (ins!pc) pc")
   1.351      case True
   1.352  
   1.353 -    have "wtl_inst (ins!pc) G rT (phi!pc) ?s' cert max_pc pc \\<and> G \\<turnstile> ?s' <=s phi ! Suc pc" (is "?wtl \\<and> ?G")
   1.354 +    have "wtl_inst (ins!pc) G rT (phi!pc) ?s' cert max_pc pc \<and> G \<turnstile> ?s' <=s phi ! Suc pc" (is "?wtl \<and> ?G")
   1.355      proof 
   1.356        from True
   1.357 -      show "G \\<turnstile> ?s' <=s phi ! Suc pc"  by (simp add: G)
   1.358 +      show "G \<turnstile> ?s' <=s phi ! Suc pc"  by (simp add: G)
   1.359  
   1.360        from True fits app pc cert pc'
   1.361        show "?wtl"
   1.362 @@ -356,7 +356,7 @@
   1.363  
   1.364      case False
   1.365      with fits app pc cert pc'
   1.366 -    have "wtl_inst (ins ! pc) G rT (phi ! pc) ?s'' cert max_pc pc \\<and> G \\<turnstile> ?s'' <=s phi ! Suc pc" 
   1.367 +    have "wtl_inst (ins ! pc) G rT (phi ! pc) ?s'' cert max_pc pc \<and> G \<turnstile> ?s'' <=s phi ! Suc pc" 
   1.368        by (auto dest: fitsD2 simp add: wtl_inst_def)
   1.369  
   1.370      thus ?thesis by blast
   1.371 @@ -365,32 +365,32 @@
   1.372  
   1.373    
   1.374  lemma wt_instr_imp_wtl_option:
   1.375 -"\\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc;  max_pc = length ins\\<rbrakk> \\<Longrightarrow> 
   1.376 - \\<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
   1.377 +"\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc;  max_pc = length ins\<rbrakk> \<Longrightarrow> 
   1.378 + \<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \<and> G \<turnstile> s <=s phi ! Suc pc"
   1.379  proof -
   1.380    assume fits : "fits ins cert phi" "pc < length ins" 
   1.381           and "wt_instr (ins!pc) G rT phi max_pc pc" 
   1.382 -             "max_pc = length ins";
   1.383 +             "max_pc = length ins"
   1.384  
   1.385 -  hence * : "\\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
   1.386 -    by - (rule wt_instr_imp_wtl_inst, simp+);
   1.387 +  hence * : "\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \<and> G \<turnstile> s <=s phi ! Suc pc"
   1.388 +    by - (rule wt_instr_imp_wtl_inst, simp+)
   1.389    
   1.390 -  show ?thesis;
   1.391 -  proof (cases "cert ! pc");
   1.392 -    case None;
   1.393 -    with *;
   1.394 -    show ?thesis; by (simp add: wtl_inst_option_def);
   1.395 +  show ?thesis
   1.396 +  proof (cases "cert ! pc")
   1.397 +    case None
   1.398 +    with *
   1.399 +    show ?thesis by (simp add: wtl_inst_option_def)
   1.400  
   1.401 -  next;
   1.402 -    case Some;
   1.403 +  next
   1.404 +    case Some
   1.405  
   1.406 -    from fits; 
   1.407 -    have "pc < length phi"; by (clarsimp simp add: fits_def);
   1.408 -    with fits Some;
   1.409 -    have "cert ! pc = Some (phi!pc)"; by (auto simp add: fits_def is_approx_def);
   1.410 +    from fits 
   1.411 +    have "pc < length phi" by (clarsimp simp add: fits_def)
   1.412 +    with fits Some
   1.413 +    have "cert ! pc = Some (phi!pc)" by (auto simp add: fits_def is_approx_def)
   1.414       
   1.415 -    with *; 
   1.416 -    show ?thesis; by (simp add: wtl_inst_option_def);
   1.417 +    with * 
   1.418 +    show ?thesis by (simp add: wtl_inst_option_def)
   1.419    qed
   1.420  qed
   1.421  
   1.422 @@ -401,13 +401,13 @@
   1.423  *}
   1.424  
   1.425  theorem wt_imp_wtl_inst_list:
   1.426 -"\\<forall> pc. (\\<forall>pc'. pc' < length all_ins \\<longrightarrow> wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \\<longrightarrow>   
   1.427 -       fits all_ins cert phi \\<longrightarrow> 
   1.428 -       (\\<exists>l. pc = length l \\<and> all_ins = l@ins) \\<longrightarrow>  
   1.429 -       pc < length all_ins \\<longrightarrow>      
   1.430 -       (\\<forall> s. (G \\<turnstile> s <=s (phi!pc)) \\<longrightarrow> 
   1.431 -             (\\<exists>s'. wtl_inst_list ins G rT s s' cert (length all_ins) pc))" 
   1.432 -(is "\\<forall>pc. ?wt \\<longrightarrow> ?fits \\<longrightarrow> ?l pc ins \\<longrightarrow> ?len pc \\<longrightarrow> ?wtl pc ins" is "\\<forall>pc. ?C pc ins" is "?P ins") 
   1.433 +"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow> wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \<longrightarrow>   
   1.434 +       fits all_ins cert phi \<longrightarrow> 
   1.435 +       (\<exists>l. pc = length l \<and> all_ins = l@ins) \<longrightarrow>  
   1.436 +       pc < length all_ins \<longrightarrow>      
   1.437 +       (\<forall> s. (G \<turnstile> s <=s (phi!pc)) \<longrightarrow> 
   1.438 +             (\<exists>s'. wtl_inst_list ins G rT s s' cert (length all_ins) pc))" 
   1.439 +(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins" is "\<forall>pc. ?C pc ins" is "?P ins") 
   1.440  proof (induct "?P" "ins")
   1.441    case Nil
   1.442    show "?P []" by simp
   1.443 @@ -418,10 +418,10 @@
   1.444    show "?P (i#ins')" 
   1.445    proof (intro allI impI, elim exE conjE)
   1.446      fix pc s l
   1.447 -    assume wt  : "\\<forall>pc'. pc' < length all_ins \\<longrightarrow> 
   1.448 +    assume wt  : "\<forall>pc'. pc' < length all_ins \<longrightarrow> 
   1.449                          wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'"
   1.450      assume fits: "fits all_ins cert phi"
   1.451 -    assume G   : "G \\<turnstile> s <=s phi ! pc"
   1.452 +    assume G   : "G \<turnstile> s <=s phi ! pc"
   1.453      assume l   : "pc < length all_ins"
   1.454  
   1.455      assume pc  : "all_ins = l@i#ins'" "pc = length l"
   1.456 @@ -434,25 +434,25 @@
   1.457      with fits l 
   1.458      obtain s1 where
   1.459            "wtl_inst_option (all_ins!pc) G rT (phi!pc) s1 cert (length all_ins) pc" and
   1.460 -      s1: "G \\<turnstile> s1 <=s phi ! (Suc pc)"
   1.461 +      s1: "G \<turnstile> s1 <=s phi ! (Suc pc)"
   1.462        by - (drule wt_instr_imp_wtl_option, assumption+, simp, elim exE conjE, simp) 
   1.463      
   1.464      with fits l
   1.465      obtain s2 where
   1.466        o:  "wtl_inst_option (all_ins!pc) G rT s s2 cert (length all_ins) pc" 
   1.467 -      and "G \\<turnstile> s2 <=s s1"
   1.468 +      and "G \<turnstile> s2 <=s s1"
   1.469        by - (drule wtl_option_mono, assumption+, simp, elim exE conjE, rule that) 
   1.470  
   1.471      with s1
   1.472 -    have G': "G \\<turnstile> s2 <=s phi ! (Suc pc)"
   1.473 +    have G': "G \<turnstile> s2 <=s phi ! (Suc pc)"
   1.474        by - (rule sup_state_trans, auto)
   1.475  
   1.476      from Cons
   1.477      have "?C (Suc pc) ins'" by blast
   1.478      with wt fits pc
   1.479 -    have IH: "?len (Suc pc) \\<longrightarrow> ?wtl (Suc pc) ins'" by auto
   1.480 +    have IH: "?len (Suc pc) \<longrightarrow> ?wtl (Suc pc) ins'" by auto
   1.481  
   1.482 -    show "\\<exists>s'. wtl_inst_list (i#ins') G rT s s' cert (length all_ins) pc"
   1.483 +    show "\<exists>s'. wtl_inst_list (i#ins') G rT s s' cert (length all_ins) pc"
   1.484      proof (cases "?len (Suc pc)")
   1.485        case False
   1.486        with pc
   1.487 @@ -475,70 +475,70 @@
   1.488    
   1.489  
   1.490  lemma fits_imp_wtl_method_complete:
   1.491 -"\\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins cert"
   1.492 +"\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\<rbrakk> \<Longrightarrow> wtl_method G C pTs rT mxl ins cert"
   1.493  by (simp add: wt_method_def wtl_method_def del: split_paired_Ex)
   1.494 -   (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex); 
   1.495 +   (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex) 
   1.496  
   1.497  
   1.498  lemma wtl_method_complete:
   1.499 -"\\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)";
   1.500 -proof -;
   1.501 -  assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G";
   1.502 +"\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\<rbrakk> \<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)"
   1.503 +proof -
   1.504 +  assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G"
   1.505    
   1.506 -  hence "fits ins (make_cert ins phi) phi";
   1.507 -    by - (rule fits_make_cert, simp add: wt_method_def);
   1.508 +  hence "fits ins (make_cert ins phi) phi"
   1.509 +    by - (rule fits_make_cert, simp add: wt_method_def)
   1.510  
   1.511 -  with *;
   1.512 -  show ?thesis; by - (rule fits_imp_wtl_method_complete);
   1.513 -qed;
   1.514 +  with *
   1.515 +  show ?thesis by - (rule fits_imp_wtl_method_complete)
   1.516 +qed
   1.517  
   1.518  lemma unique_set:
   1.519 -"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (a',b',c',d') \\<in> set l \\<longrightarrow> a = a' \\<longrightarrow> b=b' \\<and> c=c' \\<and> d=d'";
   1.520 -  by (induct "l") auto;
   1.521 +"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
   1.522 +  by (induct "l") auto
   1.523  
   1.524  lemma unique_epsilon:
   1.525 -"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (\\<epsilon> (a',b',c',d'). (a',b',c',d') \\<in> set l \\<and> a'=a) = (a,b,c,d)";
   1.526 -  by (auto simp add: unique_set);
   1.527 +"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
   1.528 +  by (auto simp add: unique_set)
   1.529  
   1.530  
   1.531 -theorem wtl_complete: "\\<lbrakk>wt_jvm_prog G Phi\\<rbrakk> \\<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)";
   1.532 -proof (simp only: wt_jvm_prog_def);
   1.533 +theorem wtl_complete: "\<lbrakk>wt_jvm_prog G Phi\<rbrakk> \<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)"
   1.534 +proof (simp only: wt_jvm_prog_def)
   1.535  
   1.536 -  assume wfprog: "wf_prog (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G";
   1.537 +  assume wfprog: "wf_prog (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G"
   1.538  
   1.539 -  thus ?thesis; 
   1.540 -  proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto);
   1.541 -    fix a aa ab b ac ba ad ae bb; 
   1.542 -    assume 1 : "\\<forall>(C,sc,fs,ms)\\<in>set G.
   1.543 -             Ball (set fs) (wf_fdecl G) \\<and>
   1.544 -             unique fs \\<and>
   1.545 -             (\\<forall>(sig,rT,mb)\\<in>set ms. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \\<and>
   1.546 -             unique ms \\<and>
   1.547 -             (case sc of None \\<Rightarrow> C = Object
   1.548 -              | Some D \\<Rightarrow>
   1.549 -                  is_class G D \\<and>
   1.550 -                  (D, C) \\<notin> (subcls1 G)^* \\<and>
   1.551 -                  (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
   1.552 -             "(a, aa, ab, b) \\<in> set G";
   1.553 +  thus ?thesis 
   1.554 +  proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto)
   1.555 +    fix a aa ab b ac ba ad ae bb 
   1.556 +    assume 1 : "\<forall>(C,sc,fs,ms)\<in>set G.
   1.557 +             Ball (set fs) (wf_fdecl G) \<and>
   1.558 +             unique fs \<and>
   1.559 +             (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT \<and> (\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \<and>
   1.560 +             unique ms \<and>
   1.561 +             (case sc of None \<Rightarrow> C = Object
   1.562 +              | Some D \<Rightarrow>
   1.563 +                  is_class G D \<and>
   1.564 +                  (D, C) \<notin> (subcls1 G)^* \<and>
   1.565 +                  (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \<longrightarrow> G\<turnstile>rT\<preceq>rT'))"
   1.566 +             "(a, aa, ab, b) \<in> set G"
   1.567    
   1.568 -    assume uG : "unique G"; 
   1.569 -    assume b  : "((ac, ba), ad, ae, bb) \\<in> set b";
   1.570 +    assume uG : "unique G" 
   1.571 +    assume b  : "((ac, ba), ad, ae, bb) \<in> set b"
   1.572  
   1.573 -    from 1;
   1.574 -    show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))";
   1.575 -    proof (rule bspec [elimify], clarsimp);
   1.576 -      assume ub : "unique b";
   1.577 -      assume m: "\\<forall>(sig,rT,mb)\\<in>set b. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb"; 
   1.578 -      from m b;
   1.579 -      show ?thesis;
   1.580 -      proof (rule bspec [elimify], clarsimp);
   1.581 -        assume "wt_method G a ba ad ae bb (Phi a (ac, ba))";         
   1.582 -        with wfprog uG ub b 1;
   1.583 -        show ?thesis;
   1.584 -          by - (rule wtl_method_complete [elimify], assumption+, simp add: make_Cert_def unique_epsilon);
   1.585 -      qed; 
   1.586 -    qed;
   1.587 -  qed;
   1.588 +    from 1
   1.589 +    show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"
   1.590 +    proof (rule bspec [elimify], clarsimp)
   1.591 +      assume ub : "unique b"
   1.592 +      assume m: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and> (\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb" 
   1.593 +      from m b
   1.594 +      show ?thesis
   1.595 +      proof (rule bspec [elimify], clarsimp)
   1.596 +        assume "wt_method G a ba ad ae bb (Phi a (ac, ba))"         
   1.597 +        with wfprog uG ub b 1
   1.598 +        show ?thesis
   1.599 +          by - (rule wtl_method_complete [elimify], assumption+, simp add: make_Cert_def unique_epsilon)
   1.600 +      qed 
   1.601 +    qed
   1.602 +  qed
   1.603  qed
   1.604  
   1.605  lemmas [simp] = split_paired_Ex
     2.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Fri Aug 11 14:52:39 2000 +0200
     2.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Fri Aug 11 14:52:52 2000 +0200
     2.3 @@ -9,28 +9,28 @@
     2.4  theory LBVCorrect = BVSpec + LBVSpec:
     2.5  
     2.6  constdefs
     2.7 -fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool" 
     2.8 -"fits_partial phi pc is G rT s0 s2 cert \\<equiv> (\\<forall> a b i s1. (a@(i#b) = is) \\<longrightarrow> 
     2.9 -                   wtl_inst_list a G rT s0 s1 cert (pc+length is) pc \\<longrightarrow> 
    2.10 -                   wtl_inst_list (i#b) G rT s1 s2 cert (pc+length is) (pc+length a) \\<longrightarrow> 
    2.11 -                      ((cert!(pc+length a)      = None   \\<longrightarrow> phi!(pc+length a) = s1) \\<and> 
    2.12 -                       (\\<forall> t. cert!(pc+length a) = Some t \\<longrightarrow> phi!(pc+length a) = t)))"
    2.13 +fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \<Rightarrow> bool" 
    2.14 +"fits_partial phi pc is G rT s0 s2 cert \<equiv> (\<forall> a b i s1. (a@(i#b) = is) \<longrightarrow> 
    2.15 +                   wtl_inst_list a G rT s0 s1 cert (pc+length is) pc \<longrightarrow> 
    2.16 +                   wtl_inst_list (i#b) G rT s1 s2 cert (pc+length is) (pc+length a) \<longrightarrow> 
    2.17 +                      ((cert!(pc+length a)      = None   \<longrightarrow> phi!(pc+length a) = s1) \<and> 
    2.18 +                       (\<forall> t. cert!(pc+length a) = Some t \<longrightarrow> phi!(pc+length a) = t)))"
    2.19    
    2.20 -fits :: "[method_type,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
    2.21 -"fits phi is G rT s0 s2 cert \\<equiv> fits_partial phi 0 is G rT s0 s2 cert"
    2.22 +fits :: "[method_type,instr list,jvm_prog,ty,state_type,state_type,certificate] \<Rightarrow> bool"
    2.23 +"fits phi is G rT s0 s2 cert \<equiv> fits_partial phi 0 is G rT s0 s2 cert"
    2.24  
    2.25  lemma fitsD: 
    2.26 -"fits phi is G rT s0 s2 cert \\<Longrightarrow>
    2.27 - (a@(i#b) = is) \\<Longrightarrow>
    2.28 - wtl_inst_list a G rT s0 s1 cert (0+length is) 0 \\<Longrightarrow>
    2.29 - wtl_inst_list (i#b) G rT s1 s2 cert (0+length is) (0+length a) \\<Longrightarrow>
    2.30 - ((cert!(0+length a)     = None   \\<longrightarrow> phi!(0+length a) = s1) \\<and> 
    2.31 - (\\<forall> t. cert!(0+length a) = Some t \\<longrightarrow> phi!(0+length a) = t))"
    2.32 +"fits phi is G rT s0 s2 cert \<Longrightarrow>
    2.33 + (a@(i#b) = is) \<Longrightarrow>
    2.34 + wtl_inst_list a G rT s0 s1 cert (0+length is) 0 \<Longrightarrow>
    2.35 + wtl_inst_list (i#b) G rT s1 s2 cert (0+length is) (0+length a) \<Longrightarrow>
    2.36 + ((cert!(0+length a)     = None   \<longrightarrow> phi!(0+length a) = s1) \<and> 
    2.37 + (\<forall> t. cert!(0+length a) = Some t \<longrightarrow> phi!(0+length a) = t))"
    2.38  by (unfold fits_def fits_partial_def) blast
    2.39  
    2.40 -lemma exists_list: "\\<exists>l. n < length l" (is "?Q n")
    2.41 +lemma exists_list: "\<exists>l. n < length l" (is "?Q n")
    2.42  proof (induct "n")
    2.43 -  fix n;  assume "?Q n"
    2.44 +  fix n  assume "?Q n"
    2.45    thus "?Q (Suc n)"
    2.46    proof elim
    2.47      fix l assume "n < length (l::'a list)"
    2.48 @@ -40,12 +40,12 @@
    2.49  qed auto
    2.50  
    2.51  lemma exists_phi:
    2.52 -"wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow> 
    2.53 - \\<exists> phi. fits phi is G rT s0 s2 cert \\<and> length is < length phi"
    2.54 +"wtl_inst_list is G rT s0 s2 cert (length is) 0 \<Longrightarrow> 
    2.55 + \<exists> phi. fits phi is G rT s0 s2 cert \<and> length is < length phi"
    2.56  proof -
    2.57    assume all: "wtl_inst_list is G rT s0 s2 cert (length is) 0"
    2.58 -  have "\\<forall> s0 pc. wtl_inst_list is G rT s0 s2 cert (pc+length is) pc 
    2.59 -     \\<longrightarrow> (\\<exists> phi. pc + length is < length phi \\<and> fits_partial phi pc is G rT s0 s2 cert)"
    2.60 +  have "\<forall> s0 pc. wtl_inst_list is G rT s0 s2 cert (pc+length is) pc 
    2.61 +     \<longrightarrow> (\<exists> phi. pc + length is < length phi \<and> fits_partial phi pc is G rT s0 s2 cert)"
    2.62      (is "?P is")
    2.63    proof (induct "?P" "is")
    2.64      case Nil
    2.65 @@ -69,10 +69,10 @@
    2.66          by blast
    2.67  
    2.68        let "?A phi pc x s1'" = 
    2.69 -        "(cert ! (pc + length (x::instr list)) = None \\<longrightarrow> phi ! (pc + length x) = s1') \\<and>
    2.70 -         (\\<forall>t. cert ! (pc + length x) = Some t \\<longrightarrow> phi ! (pc + length x) = t)"
    2.71 +        "(cert ! (pc + length (x::instr list)) = None \<longrightarrow> phi ! (pc + length x) = s1') \<and>
    2.72 +         (\<forall>t. cert ! (pc + length x) = Some t \<longrightarrow> phi ! (pc + length x) = t)"
    2.73  
    2.74 -      show "\\<exists>phi. pc + length (a # list) < length phi \\<and> 
    2.75 +      show "\<exists>phi. pc + length (a # list) < length phi \<and> 
    2.76                    fits_partial phi pc (a # list) G rT s0 s2 cert" 
    2.77        proof (cases "cert!pc")
    2.78          case None            
    2.79 @@ -148,156 +148,156 @@
    2.80  
    2.81  
    2.82  lemma fits_lemma1:
    2.83 -"\\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\\<rbrakk> \\<Longrightarrow> 
    2.84 -  \\<forall> pc t. pc < length is \\<longrightarrow> (cert ! pc) = Some t \\<longrightarrow> (phi ! pc) = t";
    2.85 -proof intro;
    2.86 -  fix pc t;
    2.87 -  assume wtl:  "wtl_inst_list is G rT s0 s3 cert (length is) 0";
    2.88 -  assume fits: "fits phi is G rT s0 s3 cert";
    2.89 -  assume pc:   "pc < length is";
    2.90 -  assume cert: "cert ! pc = Some t";
    2.91 -  from pc;
    2.92 -  have "is \\<noteq> []"; by auto;
    2.93 -  hence cons: "\\<exists>i y. is = i#y"; by (simp add: neq_Nil_conv);
    2.94 -  from wtl pc;
    2.95 -  have "\\<exists>a b s1. a@b = is \\<and> length a = pc \\<and> 
    2.96 -                 wtl_inst_list a G rT s0 s1 cert (length is) 0 \\<and> 
    2.97 +"\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\<rbrakk> \<Longrightarrow> 
    2.98 +  \<forall> pc t. pc < length is \<longrightarrow> (cert ! pc) = Some t \<longrightarrow> (phi ! pc) = t"
    2.99 +proof intro
   2.100 +  fix pc t
   2.101 +  assume wtl:  "wtl_inst_list is G rT s0 s3 cert (length is) 0"
   2.102 +  assume fits: "fits phi is G rT s0 s3 cert"
   2.103 +  assume pc:   "pc < length is"
   2.104 +  assume cert: "cert ! pc = Some t"
   2.105 +  from pc
   2.106 +  have "is \<noteq> []" by auto
   2.107 +  hence cons: "\<exists>i y. is = i#y" by (simp add: neq_Nil_conv)
   2.108 +  from wtl pc
   2.109 +  have "\<exists>a b s1. a@b = is \<and> length a = pc \<and> 
   2.110 +                 wtl_inst_list a G rT s0 s1 cert (length is) 0 \<and> 
   2.111                   wtl_inst_list b G rT s1 s3 cert (length is) (0+length a)"
   2.112 -    (is "\\<exists>a b s1. ?A a b \\<and> ?L a \\<and> ?W1 a s1 \\<and> ?W2 a b s1");
   2.113 -  by (rule wtl_partial [rulify]);
   2.114 -  with cons;
   2.115 -  show "phi ! pc = t";
   2.116 -  proof (elim exE conjE);
   2.117 -    fix a b s1 i y;
   2.118 -    assume * :"?A a b" "?L a" "?W1 a s1" "?W2 a b s1" "is = i#y";
   2.119 -    with pc;
   2.120 -    have "b \\<noteq> []"; by auto;
   2.121 -    hence "\\<exists>b' bs. b = b'#bs"; by (simp add: neq_Nil_conv);
   2.122 -    thus ?thesis;
   2.123 -    proof (elim exE);
   2.124 -      fix b' bs; assume Cons: "b=b'#bs";
   2.125 -      with * fits cert;     
   2.126 -      show ?thesis; 
   2.127 -      proof (unfold fits_def fits_partial_def, elim allE impE); 
   2.128 -        from * Cons; show "a@b'#bs=is"; by simp;
   2.129 -      qed simp+;
   2.130 -    qed;
   2.131 -  qed;
   2.132 -qed;
   2.133 +    (is "\<exists>a b s1. ?A a b \<and> ?L a \<and> ?W1 a s1 \<and> ?W2 a b s1")
   2.134 +  by (rule wtl_partial [rulify])
   2.135 +  with cons
   2.136 +  show "phi ! pc = t"
   2.137 +  proof (elim exE conjE)
   2.138 +    fix a b s1 i y
   2.139 +    assume * :"?A a b" "?L a" "?W1 a s1" "?W2 a b s1" "is = i#y"
   2.140 +    with pc
   2.141 +    have "b \<noteq> []" by auto
   2.142 +    hence "\<exists>b' bs. b = b'#bs" by (simp add: neq_Nil_conv)
   2.143 +    thus ?thesis
   2.144 +    proof (elim exE)
   2.145 +      fix b' bs assume Cons: "b=b'#bs"
   2.146 +      with * fits cert     
   2.147 +      show ?thesis 
   2.148 +      proof (unfold fits_def fits_partial_def, elim allE impE) 
   2.149 +        from * Cons show "a@b'#bs=is" by simp
   2.150 +      qed simp+
   2.151 +    qed
   2.152 +  qed
   2.153 +qed
   2.154  
   2.155  lemma fits_lemma2:
   2.156 -"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; 
   2.157 +"\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; 
   2.158    wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); 
   2.159    fits phi (a@i#b) G rT s0 s3 cert; cert!(length a) = None; 
   2.160 -  wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> 
   2.161 - \\<Longrightarrow>  phi!(length a) = s1";
   2.162 -proof (unfold fits_def fits_partial_def, elim allE impE);
   2.163 -qed (auto simp del: split_paired_Ex);
   2.164 +  wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\<rbrakk> 
   2.165 + \<Longrightarrow>  phi!(length a) = s1"
   2.166 +proof (unfold fits_def fits_partial_def, elim allE impE)
   2.167 +qed (auto simp del: split_paired_Ex)
   2.168  
   2.169  
   2.170  
   2.171  lemma wtl_suc_pc:
   2.172 -"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; 
   2.173 +"\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; 
   2.174    wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); 
   2.175    wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a)); 
   2.176 -  fits phi (a@i#b) G rT s0 s3 cert \\<rbrakk> \\<Longrightarrow> 
   2.177 -  b \\<noteq> [] \\<longrightarrow> G \\<turnstile> s2 <=s (phi ! (Suc (length a)))";
   2.178 -proof;
   2.179 -  assume f: "fits phi (a@i#b) G rT s0 s3 cert";
   2.180 +  fits phi (a@i#b) G rT s0 s3 cert \<rbrakk> \<Longrightarrow> 
   2.181 +  b \<noteq> [] \<longrightarrow> G \<turnstile> s2 <=s (phi ! (Suc (length a)))"
   2.182 +proof
   2.183 +  assume f: "fits phi (a@i#b) G rT s0 s3 cert"
   2.184    assume "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
   2.185           "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)"
   2.186 -  and w: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))";
   2.187 -  hence a: "wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0"; by (rule wtl_append);
   2.188 -  assume "b \\<noteq> []"
   2.189 +  and w: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))"
   2.190 +  hence a: "wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0" by (rule wtl_append)
   2.191 +  assume "b \<noteq> []"
   2.192  
   2.193    from this
   2.194 -  obtain b' bs where Cons: "b = b' # bs"; by (simp add: neq_Nil_conv) (elim exE, rule that);
   2.195 -  hence "(a@[i]) @ b' # bs = a @ i # b"; by simp;
   2.196 +  obtain b' bs where Cons: "b = b' # bs" by (simp add: neq_Nil_conv) (elim exE, rule that)
   2.197 +  hence "(a@[i]) @ b' # bs = a @ i # b" by simp
   2.198    with f
   2.199 -  show "G \\<turnstile> s2 <=s phi ! Suc (length a)";
   2.200 -  proof (rule fitsD [elimify]); 
   2.201 -    from Cons w;       
   2.202 -    show "wtl_inst_list (b' # bs) G rT s2 s3 cert (0 + length (a @ i # b)) (0 + length (a @ [i]))";
   2.203 -      by simp;
   2.204 -    from a; 
   2.205 -    show "wtl_inst_list (a @ [i]) G rT s0 s2 cert (0 + length (a @ i # b)) 0"; by simp;
   2.206 +  show "G \<turnstile> s2 <=s phi ! Suc (length a)"
   2.207 +  proof (rule fitsD [elimify]) 
   2.208 +    from Cons w       
   2.209 +    show "wtl_inst_list (b' # bs) G rT s2 s3 cert (0 + length (a @ i # b)) (0 + length (a @ [i]))"
   2.210 +      by simp
   2.211 +    from a 
   2.212 +    show "wtl_inst_list (a @ [i]) G rT s0 s2 cert (0 + length (a @ i # b)) 0" by simp
   2.213      
   2.214      assume cert:
   2.215 -      "(cert ! (0 + length (a @ [i])) = None \\<longrightarrow> phi ! (0 + length (a @ [i])) = s2) \\<and>
   2.216 -      (\\<forall>t. cert ! (0 + length (a @ [i])) = Some t \\<longrightarrow> phi ! (0 + length (a @ [i])) = t)";
   2.217 -    show ?thesis;
   2.218 -    proof (cases "cert ! Suc (length a)");
   2.219 -      assume "cert ! Suc (length a) = None";
   2.220 -      with cert;
   2.221 -      have "s2 = phi ! Suc (length a)"; by simp; 
   2.222 -      thus ?thesis; by simp;
   2.223 -    next;
   2.224 -      fix t; assume "cert ! Suc (length a) = Some t";
   2.225 -      with cert;
   2.226 -      have "phi ! Suc (length a) = t"; by (simp del: split_paired_All);
   2.227 -      with cert Cons w;
   2.228 -      show ?thesis;  by (auto simp add: wtl_inst_option_def)
   2.229 +      "(cert ! (0 + length (a @ [i])) = None \<longrightarrow> phi ! (0 + length (a @ [i])) = s2) \<and>
   2.230 +      (\<forall>t. cert ! (0 + length (a @ [i])) = Some t \<longrightarrow> phi ! (0 + length (a @ [i])) = t)"
   2.231 +    show ?thesis
   2.232 +    proof (cases "cert ! Suc (length a)")
   2.233 +      assume "cert ! Suc (length a) = None"
   2.234 +      with cert
   2.235 +      have "s2 = phi ! Suc (length a)" by simp 
   2.236 +      thus ?thesis by simp
   2.237 +    next
   2.238 +      fix t assume "cert ! Suc (length a) = Some t"
   2.239 +      with cert
   2.240 +      have "phi ! Suc (length a) = t" by (simp del: split_paired_All)
   2.241 +      with cert Cons w
   2.242 +      show ?thesis  by (auto simp add: wtl_inst_option_def)
   2.243      qed
   2.244    qed
   2.245  qed
   2.246  
   2.247  lemma wtl_lemma: 
   2.248 -"\\<lbrakk>wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0;
   2.249 +"\<lbrakk>wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0;
   2.250    wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1);
   2.251    wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1));
   2.252 -  fits phi (i1@i#i2) G rT s0 s3 cert\\<rbrakk> \\<Longrightarrow>
   2.253 -  wt_instr i G rT phi (length (i1@i#i2)) (length i1)" (concl is "?P i");
   2.254 -proof -;
   2.255 -  assume w1: "wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0" (is ?w1);
   2.256 -  assume wo: "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)";
   2.257 -  assume w2: "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))";
   2.258 -  assume f:  "fits phi (i1@i#i2) G rT s0 s3 cert";
   2.259 +  fits phi (i1@i#i2) G rT s0 s3 cert\<rbrakk> \<Longrightarrow>
   2.260 +  wt_instr i G rT phi (length (i1@i#i2)) (length i1)" (concl is "?P i")
   2.261 +proof -
   2.262 +  assume w1: "wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0" (is ?w1)
   2.263 +  assume wo: "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)"
   2.264 +  assume w2: "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))"
   2.265 +  assume f:  "fits phi (i1@i#i2) G rT s0 s3 cert"
   2.266  
   2.267 -  from w1 wo w2;
   2.268 -  have wtl: "wtl_inst_list (i1@i#i2) G rT s0 s3 cert (length (i1@i#i2)) 0"; 
   2.269 -    by (rule wtl_cons_appendl);
   2.270 +  from w1 wo w2
   2.271 +  have wtl: "wtl_inst_list (i1@i#i2) G rT s0 s3 cert (length (i1@i#i2)) 0" 
   2.272 +    by (rule wtl_cons_appendl)
   2.273  
   2.274 -  with f;  
   2.275 -  have c1: "\\<forall>t. cert ! (length i1) = Some t \\<longrightarrow> phi ! (length i1) = t";
   2.276 -    by intro (rule fits_lemma1 [rulify], auto);
   2.277 +  with f  
   2.278 +  have c1: "\<forall>t. cert ! (length i1) = Some t \<longrightarrow> phi ! (length i1) = t"
   2.279 +    by intro (rule fits_lemma1 [rulify], auto)
   2.280  
   2.281 -  from w1 wo w2 f;
   2.282 -  have c2: "cert ! (length i1) = None \\<Longrightarrow> phi ! (length i1) = s1";
   2.283 -    by - (rule fits_lemma2);
   2.284 +  from w1 wo w2 f
   2.285 +  have c2: "cert ! (length i1) = None \<Longrightarrow> phi ! (length i1) = s1"
   2.286 +    by - (rule fits_lemma2)
   2.287  
   2.288 -  from wtl f;
   2.289 -  have c3: "\\<forall>pc t. pc < length(i1@i#i2) \\<longrightarrow> cert ! pc = Some t \\<longrightarrow> phi ! pc = t";
   2.290 -    by (rule fits_lemma1);
   2.291 +  from wtl f
   2.292 +  have c3: "\<forall>pc t. pc < length(i1@i#i2) \<longrightarrow> cert ! pc = Some t \<longrightarrow> phi ! pc = t"
   2.293 +    by (rule fits_lemma1)
   2.294  
   2.295 -  from w1 wo w2 f;
   2.296 -  have suc: "i2 \\<noteq> [] \\<Longrightarrow> G \\<turnstile> s2 <=s phi ! Suc (length i1)"; 
   2.297 -    by (rule wtl_suc_pc [rulify]); 
   2.298 +  from w1 wo w2 f
   2.299 +  have suc: "i2 \<noteq> [] \<Longrightarrow> G \<turnstile> s2 <=s phi ! Suc (length i1)" 
   2.300 +    by (rule wtl_suc_pc [rulify]) 
   2.301  
   2.302    with wo
   2.303 -  show ?thesis;
   2.304 +  show ?thesis
   2.305      by (auto simp add: c1 c2 c3 wt_instr_def wtl_inst_def wtl_inst_option_def split: option.split_asm)
   2.306  qed
   2.307  
   2.308  
   2.309  lemma wtl_fits_wt:
   2.310 -"\\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\\<rbrakk> 
   2.311 - \\<Longrightarrow> \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
   2.312 -proof intro;
   2.313 -  assume fits: "fits phi is G rT s0 s3 cert";
   2.314 +"\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\<rbrakk> 
   2.315 + \<Longrightarrow> \<forall>pc. pc < length is \<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc"
   2.316 +proof intro
   2.317 +  assume fits: "fits phi is G rT s0 s3 cert"
   2.318  
   2.319 -  fix pc;
   2.320 +  fix pc
   2.321    assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0"
   2.322 -     and pc:  "pc < length is";
   2.323 +     and pc:  "pc < length is"
   2.324    
   2.325    from this
   2.326    obtain i1 i2' s1 where 
   2.327      l:  "i1 @ i2' = is" "length i1 = pc" and
   2.328      w1: "wtl_inst_list i1 G rT s0 s1 cert (length is) 0" and 
   2.329 -    w2: "wtl_inst_list i2' G rT s1 s3 cert (length is) (0 + length i1)"; 
   2.330 -    by (rule wtl_partial [rulify, elimify]) (elim, rule that);
   2.331 +    w2: "wtl_inst_list i2' G rT s1 s3 cert (length is) (0 + length i1)" 
   2.332 +    by (rule wtl_partial [rulify, elimify]) (elim, rule that)
   2.333  
   2.334 -  from l pc;
   2.335 -  have "i2' \\<noteq> []"; by auto;
   2.336 +  from l pc
   2.337 +  have "i2' \<noteq> []" by auto
   2.338  
   2.339    from this
   2.340    obtain i i2 where c: "i2' = i#i2" 
   2.341 @@ -324,27 +324,27 @@
   2.342  qed
   2.343      
   2.344  lemma wtl_inst_list_correct:
   2.345 -"wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow> 
   2.346 - \\<exists> phi. \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
   2.347 -proof -;
   2.348 -  assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
   2.349 +"wtl_inst_list is G rT s0 s2 cert (length is) 0 \<Longrightarrow> 
   2.350 + \<exists> phi. \<forall>pc. pc < length is \<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc"
   2.351 +proof -
   2.352 +  assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0"
   2.353  
   2.354    from this
   2.355 -  obtain phi where "fits phi is G rT s0 s2 cert";
   2.356 +  obtain phi where "fits phi is G rT s0 s2 cert"
   2.357      by (rule exists_phi [elimify]) blast
   2.358  
   2.359    with wtl
   2.360    show ?thesis
   2.361 -    by (rule wtl_fits_wt [elimify]) blast;
   2.362 +    by (rule wtl_fits_wt [elimify]) blast
   2.363  qed
   2.364      
   2.365  lemma fits_first:
   2.366 -"\\<lbrakk>is \\<noteq> [];wtl_inst_list is G rT s0 s2 cert (length is) 0; 
   2.367 - fits phi is G rT s0 s2 cert\\<rbrakk> \\<Longrightarrow> G \\<turnstile> s0 <=s phi ! 0";
   2.368 -proof -;
   2.369 -  assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
   2.370 -  assume fits: "fits phi is G rT s0 s2 cert";
   2.371 -  assume "is \\<noteq> []"
   2.372 +"\<lbrakk>is \<noteq> [];wtl_inst_list is G rT s0 s2 cert (length is) 0; 
   2.373 + fits phi is G rT s0 s2 cert\<rbrakk> \<Longrightarrow> G \<turnstile> s0 <=s phi ! 0"
   2.374 +proof -
   2.375 +  assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0"
   2.376 +  assume fits: "fits phi is G rT s0 s2 cert"
   2.377 +  assume "is \<noteq> []"
   2.378    
   2.379    from this 
   2.380    obtain y ys where cons: "is = y#ys" 
   2.381 @@ -360,8 +360,8 @@
   2.382        by simp
   2.383  
   2.384      assume cert:
   2.385 -      "(cert ! (0 + length []) = None \\<longrightarrow> phi ! (0 + length []) = s0) \\<and>
   2.386 -       (\\<forall>t. cert ! (0 + length []) = Some t \\<longrightarrow> phi ! (0 + length []) = t)"
   2.387 +      "(cert ! (0 + length []) = None \<longrightarrow> phi ! (0 + length []) = s0) \<and>
   2.388 +       (\<forall>t. cert ! (0 + length []) = Some t \<longrightarrow> phi ! (0 + length []) = t)"
   2.389  
   2.390      show ?thesis
   2.391      proof (cases "cert!0")
   2.392 @@ -369,30 +369,30 @@
   2.393        with cert
   2.394        show ?thesis by simp
   2.395      next
   2.396 -      fix t; assume "cert!0 = Some t"
   2.397 +      fix t assume "cert!0 = Some t"
   2.398        with cert
   2.399 -      have "phi!0 = t"; by (simp del: split_paired_All);
   2.400 -      with cert cons wtl;
   2.401 -      show ?thesis; by (auto simp add: wtl_inst_option_def);
   2.402 +      have "phi!0 = t" by (simp del: split_paired_All)
   2.403 +      with cert cons wtl
   2.404 +      show ?thesis by (auto simp add: wtl_inst_option_def)
   2.405      qed
   2.406    qed simp
   2.407  qed
   2.408    
   2.409  lemma wtl_method_correct:
   2.410 -"wtl_method G C pTs rT mxl ins cert \\<Longrightarrow> \\<exists> phi. wt_method G C pTs rT mxl ins phi"
   2.411 +"wtl_method G C pTs rT mxl ins cert \<Longrightarrow> \<exists> phi. wt_method G C pTs rT mxl ins phi"
   2.412  proof (unfold wtl_method_def, simp del: split_paired_Ex, elim exE conjE)
   2.413    let "?s0" = "([], Some (Class C) # map Some pTs @ replicate mxl None)"
   2.414    fix s2
   2.415 -  assume neqNil: "ins \\<noteq> []"
   2.416 +  assume neqNil: "ins \<noteq> []"
   2.417    assume wtl: "wtl_inst_list ins G rT ?s0 s2 cert (length ins) 0"
   2.418  
   2.419    from this
   2.420 -  obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \\<and> length ins < length phi"
   2.421 -    by (rule exists_phi [elimify]) blast;
   2.422 +  obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \<and> length ins < length phi"
   2.423 +    by (rule exists_phi [elimify]) blast
   2.424  
   2.425    with wtl
   2.426    have allpc:
   2.427 -    "\\<forall>pc. pc < length ins \\<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc"
   2.428 +    "\<forall>pc. pc < length ins \<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc"
   2.429      by elim (rule wtl_fits_wt [elimify])
   2.430  
   2.431    from neqNil wtl fits
   2.432 @@ -404,58 +404,58 @@
   2.433  qed
   2.434  
   2.435  lemma unique_set:
   2.436 -"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (a',b',c',d') \\<in> set l \\<longrightarrow> a = a' \\<longrightarrow> b=b' \\<and> c=c' \\<and> d=d'";
   2.437 -  by (induct "l") auto;
   2.438 +"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
   2.439 +  by (induct "l") auto
   2.440  
   2.441  lemma unique_epsilon:
   2.442 -"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (\\<epsilon> (a',b',c',d'). (a',b',c',d') \\<in> set l \\<and> a'=a) = (a,b,c,d)";
   2.443 -  by (auto simp add: unique_set);
   2.444 +"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
   2.445 +  by (auto simp add: unique_set)
   2.446  
   2.447  theorem wtl_correct:
   2.448 -"wtl_jvm_prog G cert ==> \\<exists> Phi. wt_jvm_prog G Phi";
   2.449 -proof (clarsimp simp add: wt_jvm_prog_def wf_prog_def, intro conjI);
   2.450 +"wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
   2.451 +proof (clarsimp simp add: wt_jvm_prog_def wf_prog_def, intro conjI)
   2.452  
   2.453 -  assume wtl_prog: "wtl_jvm_prog G cert";
   2.454 -  thus "ObjectC \\<in> set G"; by (simp add: wtl_jvm_prog_def wf_prog_def);
   2.455 +  assume wtl_prog: "wtl_jvm_prog G cert"
   2.456 +  thus "ObjectC \<in> set G" by (simp add: wtl_jvm_prog_def wf_prog_def)
   2.457  
   2.458 -  from wtl_prog; 
   2.459 -  show uniqueG: "unique G"; by (simp add: wtl_jvm_prog_def wf_prog_def);
   2.460 +  from wtl_prog 
   2.461 +  show uniqueG: "unique G" by (simp add: wtl_jvm_prog_def wf_prog_def)
   2.462  
   2.463 -  show "\\<exists>Phi. Ball (set G) (wf_cdecl (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G)"
   2.464 -    (is "\\<exists>Phi. ?Q Phi");
   2.465 -  proof (intro exI);
   2.466 +  show "\<exists>Phi. Ball (set G) (wf_cdecl (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G)"
   2.467 +    (is "\<exists>Phi. ?Q Phi")
   2.468 +  proof (intro exI)
   2.469      let "?Phi" = 
   2.470 -        "\\<lambda> C sig. let (C,x,y,mdecls) = \\<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\<in> set G \\<and> Cl = C in
   2.471 -                   let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in\
   2.472 -                     \\<epsilon> phi. wt_method G C (snd sig) rT maxl b phi";
   2.473 -    from wtl_prog;
   2.474 -    show "?Q ?Phi";
   2.475 -    proof (unfold wf_cdecl_def, intro);
   2.476 -      fix x a b aa ba ab bb m;
   2.477 -      assume 1: "x \\<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \\<in> set bb";
   2.478 -      with wtl_prog;
   2.479 -      show "wf_mdecl (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (?Phi C sig)) G a m";
   2.480 -      proof (simp add: wf_mdecl_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def, elim conjE);
   2.481 -        apply_end (drule bspec, assumption, simp, elim conjE);
   2.482 -        assume "\\<forall>(sig,rT,mb)\\<in>set bb. wf_mhead G sig rT \\<and> 
   2.483 -                 (\\<lambda>(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb"
   2.484 -               "unique bb";
   2.485 -        with 1 uniqueG;
   2.486 -        show "(\\<lambda>(sig,rT,mb).
   2.487 -          wf_mhead G sig rT \\<and>
   2.488 -          (\\<lambda>(maxl,b).
   2.489 +        "\<lambda> C sig. let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C in
   2.490 +                   let (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig in\
   2.491 +                     \<epsilon> phi. wt_method G C (snd sig) rT maxl b phi"
   2.492 +    from wtl_prog
   2.493 +    show "?Q ?Phi"
   2.494 +    proof (unfold wf_cdecl_def, intro)
   2.495 +      fix x a b aa ba ab bb m
   2.496 +      assume 1: "x \<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \<in> set bb"
   2.497 +      with wtl_prog
   2.498 +      show "wf_mdecl (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (?Phi C sig)) G a m"
   2.499 +      proof (simp add: wf_mdecl_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def, elim conjE)
   2.500 +        apply_end (drule bspec, assumption, simp, elim conjE)
   2.501 +        assume "\<forall>(sig,rT,mb)\<in>set bb. wf_mhead G sig rT \<and> 
   2.502 +                 (\<lambda>(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb"
   2.503 +               "unique bb"
   2.504 +        with 1 uniqueG
   2.505 +        show "(\<lambda>(sig,rT,mb).
   2.506 +          wf_mhead G sig rT \<and>
   2.507 +          (\<lambda>(maxl,b).
   2.508                wt_method G a (snd sig) rT maxl b 
   2.509 -               ((\\<lambda>(C,x,y,mdecls).
   2.510 -                    (\\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
   2.511 -                     (\\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \\<in> set mdecls \\<and> sg = sig))
   2.512 -                 (\\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \\<in> set G \\<and> Cl = a))) mb) m";
   2.513 +               ((\<lambda>(C,x,y,mdecls).
   2.514 +                    (\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
   2.515 +                     (\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig))
   2.516 +                 (\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
   2.517            by - (drule bspec, assumption, 
   2.518 -                clarsimp elim: wtl_method_correct [elimify],
   2.519 -                clarsimp intro: selectI simp add: unique_epsilon); 
   2.520 -      qed;
   2.521 -    qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def);
   2.522 -  qed;
   2.523 -qed;
   2.524 +                clarsimp dest!: wtl_method_correct,
   2.525 +                clarsimp intro!: selectI simp add: unique_epsilon)
   2.526 +      qed
   2.527 +    qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
   2.528 +  qed
   2.529 +qed
   2.530      
   2.531  
   2.532 -end;
   2.533 +end
     3.1 --- a/src/HOL/MicroJava/BV/Step.thy	Fri Aug 11 14:52:39 2000 +0200
     3.2 +++ b/src/HOL/MicroJava/BV/Step.thy	Fri Aug 11 14:52:52 2000 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4  
     3.5  text "Effect of instruction on the state type"
     3.6  consts 
     3.7 -step :: "instr \\<times> jvm_prog \\<times> state_type \\<Rightarrow> state_type option"
     3.8 +step :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type option"
     3.9  
    3.10  recdef step "{}"
    3.11  "step (Load idx,  G, (ST, LT))          = Some (the (LT ! idx) # ST, LT)"
    3.12 @@ -41,22 +41,22 @@
    3.13  
    3.14  text "Conditions under which step is applicable"
    3.15  consts
    3.16 -app :: "instr \\<times> jvm_prog \\<times> ty \\<times> state_type \\<Rightarrow> bool"
    3.17 +app :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool"
    3.18  
    3.19  recdef app "{}"
    3.20 -"app (Load idx, G, rT, s)                  = (idx < length (snd s) \\<and> (snd s) ! idx \\<noteq> None)"
    3.21 +"app (Load idx, G, rT, s)                  = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> None)"
    3.22  "app (Store idx, G, rT, (ts#ST, LT))       = (idx < length LT)"
    3.23  "app (Bipush i, G, rT, s)                  = True"
    3.24  "app (Aconst_null, G, rT, s)               = True"
    3.25 -"app (Getfield F C, G, rT, (oT#ST, LT))    = (is_class G C \\<and> 
    3.26 -                                              field (G,C) F \\<noteq> None \\<and>
    3.27 -                                              fst (the (field (G,C) F)) = C \\<and>
    3.28 -                                              G \\<turnstile> oT \\<preceq> (Class C))"
    3.29 -"app (Putfield F C, G, rT, (vT#oT#ST, LT)) = (is_class G C \\<and> 
    3.30 -                                              field (G,C) F \\<noteq> None \\<and>
    3.31 -                                              fst (the (field (G,C) F)) = C \\<and>
    3.32 -                                              G \\<turnstile> oT \\<preceq> (Class C) \\<and>
    3.33 -                                              G \\<turnstile> vT \\<preceq> (snd (the (field (G,C) F))))" 
    3.34 +"app (Getfield F C, G, rT, (oT#ST, LT))    = (is_class G C \<and> 
    3.35 +                                              field (G,C) F \<noteq> None \<and>
    3.36 +                                              fst (the (field (G,C) F)) = C \<and>
    3.37 +                                              G \<turnstile> oT \<preceq> (Class C))"
    3.38 +"app (Putfield F C, G, rT, (vT#oT#ST, LT)) = (is_class G C \<and> 
    3.39 +                                              field (G,C) F \<noteq> None \<and>
    3.40 +                                              fst (the (field (G,C) F)) = C \<and>
    3.41 +                                              G \<turnstile> oT \<preceq> (Class C) \<and>
    3.42 +                                              G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" 
    3.43  "app (New C, G, rT, s)                     = (is_class G C)"
    3.44  "app (Checkcast C, G, rT, (RefT rt#ST,LT)) = (is_class G C)"
    3.45  "app (Pop, G, rT, (ts#ST,LT))              = True"
    3.46 @@ -66,19 +66,19 @@
    3.47  "app (Swap, G, rT, (ts1#ts2#ST,LT))        = True"
    3.48  "app (IAdd, G, rT, (PrimT Integer#PrimT Integer#ST,LT)) 
    3.49                                             = True"
    3.50 -"app (Ifcmpeq b, G, rT, (ts1#ts2#ST,LT))   = ((\\<exists> p. ts1 = PrimT p \\<and> ts1 = PrimT p) \\<or> 
    3.51 -                                              (\\<exists>r r'. ts1 = RefT r \\<and> ts2 = RefT r'))"
    3.52 +"app (Ifcmpeq b, G, rT, (ts1#ts2#ST,LT))   = ((\<exists> p. ts1 = PrimT p \<and> ts1 = PrimT p) \<or> 
    3.53 +                                              (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r'))"
    3.54  "app (Goto b, G, rT, s)                    = True"
    3.55 -"app (Return, G, rT, (T#ST,LT))            = (G \\<turnstile> T \\<preceq> rT)"
    3.56 +"app (Return, G, rT, (T#ST,LT))            = (G \<turnstile> T \<preceq> rT)"
    3.57  app_invoke:
    3.58 -"app (Invoke C mn fpTs, G, rT, s)          = (length fpTs < length (fst s) \\<and> 
    3.59 +"app (Invoke C mn fpTs, G, rT, s)          = (length fpTs < length (fst s) \<and> 
    3.60                                                (let 
    3.61                                                  apTs = rev (take (length fpTs) (fst s));
    3.62                                                  X    = hd (drop (length fpTs) (fst s)) 
    3.63                                                in
    3.64 -                                                G \\<turnstile> X \\<preceq> Class C \\<and> 
    3.65 -                                                (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
    3.66 -                                                method (G,C) (mn,fpTs) \\<noteq> None
    3.67 +                                                G \<turnstile> X \<preceq> Class C \<and> 
    3.68 +                                                (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and>
    3.69 +                                                method (G,C) (mn,fpTs) \<noteq> None
    3.70                                               ))"
    3.71  
    3.72  "app (i,G,rT,s)                            = False"
    3.73 @@ -87,7 +87,7 @@
    3.74  text {* \isa{p_count} of successor instructions *}
    3.75  
    3.76  consts
    3.77 -succs :: "instr \\<Rightarrow> p_count \\<Rightarrow> p_count set"
    3.78 +succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count set"
    3.79  
    3.80  primrec 
    3.81  "succs (Load idx) pc         = {pc+1}"
    3.82 @@ -110,25 +110,25 @@
    3.83  "succs (Invoke C mn fpTs) pc = {pc+1}"
    3.84  
    3.85  
    3.86 -lemma 1: "2 < length a \\<Longrightarrow> (\\<exists>l l' l'' ls. a = l#l'#l''#ls)"
    3.87 +lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
    3.88  proof (cases a)
    3.89    fix x xs assume "a = x#xs" "2 < length a"
    3.90    thus ?thesis by - (cases xs, simp, cases "tl xs", auto)
    3.91  qed auto
    3.92  
    3.93 -lemma 2: "\\<not>(2 < length a) \\<Longrightarrow> a = [] \\<or> (\\<exists> l. a = [l]) \\<or> (\\<exists> l l'. a = [l,l'])"
    3.94 +lemma 2: "\<not>(2 < length a) \<Longrightarrow> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
    3.95  proof -;
    3.96 -  assume "\\<not>(2 < length a)"
    3.97 +  assume "\<not>(2 < length a)"
    3.98    hence "length a < (Suc 2)" by simp
    3.99 -  hence * : "length a = 0 \\<or> length a = 1 \\<or> length a = 2" by (auto simp add: less_Suc_eq)
   3.100 +  hence * : "length a = 0 \<or> length a = 1 \<or> length a = 2" by (auto simp add: less_Suc_eq)
   3.101  
   3.102    { 
   3.103      fix x 
   3.104      assume "length x = 1"
   3.105 -    hence "\\<exists> l. x = [l]"  by - (cases x, auto)
   3.106 +    hence "\<exists> l. x = [l]"  by - (cases x, auto)
   3.107    } note 0 = this
   3.108  
   3.109 -  have "length a = 2 \\<Longrightarrow> \\<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
   3.110 +  have "length a = 2 \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
   3.111    with * show ?thesis by (auto dest: 0)
   3.112  qed
   3.113  
   3.114 @@ -139,56 +139,56 @@
   3.115  *}
   3.116  
   3.117  lemma appStore[simp]:
   3.118 -"app (Store idx, G, rT, s) = (\\<exists> ts ST LT. s = (ts#ST,LT) \\<and> idx < length LT)"
   3.119 +"app (Store idx, G, rT, s) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)"
   3.120  by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
   3.121  
   3.122  
   3.123  lemma appGetField[simp]:
   3.124 -"app (Getfield F C, G, rT, s) = (\\<exists> oT ST LT. s = (oT#ST, LT) \\<and> is_class G C \\<and> 
   3.125 -                                 fst (the (field (G,C) F)) = C \\<and>
   3.126 -                                 field (G,C) F \\<noteq> None \\<and> G \\<turnstile> oT \\<preceq> (Class C))"
   3.127 +"app (Getfield F C, G, rT, s) = (\<exists> oT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and> 
   3.128 +                                 fst (the (field (G,C) F)) = C \<and>
   3.129 +                                 field (G,C) F \<noteq> None \<and> G \<turnstile> oT \<preceq> (Class C))"
   3.130  by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
   3.131  
   3.132  
   3.133  lemma appPutField[simp]:
   3.134 -"app (Putfield F C, G, rT, s) = (\\<exists> vT oT ST LT. s = (vT#oT#ST, LT) \\<and> is_class G C \\<and> 
   3.135 -                                 field (G,C) F \\<noteq> None \\<and> fst (the (field (G,C) F)) = C \\<and>
   3.136 -                                 G \\<turnstile> oT \\<preceq> (Class C) \\<and>
   3.137 -                                 G \\<turnstile> vT \\<preceq> (snd (the (field (G,C) F))))" 
   3.138 +"app (Putfield F C, G, rT, s) = (\<exists> vT oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and> 
   3.139 +                                 field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
   3.140 +                                 G \<turnstile> oT \<preceq> (Class C) \<and>
   3.141 +                                 G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" 
   3.142  by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
   3.143  
   3.144  
   3.145  lemma appCheckcast[simp]:
   3.146 -"app (Checkcast C, G, rT, s) = (\\<exists>rT ST LT. s = (RefT rT#ST,LT) \\<and> is_class G C)"
   3.147 +"app (Checkcast C, G, rT, s) = (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C)"
   3.148  by (cases s, cases "fst s", simp, cases "hd (fst s)", auto)
   3.149  
   3.150  lemma appPop[simp]:
   3.151 -"app (Pop, G, rT, s) = (\\<exists>ts ST LT. s = (ts#ST,LT))" 
   3.152 +"app (Pop, G, rT, s) = (\<exists>ts ST LT. s = (ts#ST,LT))" 
   3.153  by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
   3.154  
   3.155  
   3.156  lemma appDup[simp]:
   3.157 -"app (Dup, G, rT, s) = (\\<exists>ts ST LT. s = (ts#ST,LT))" 
   3.158 +"app (Dup, G, rT, s) = (\<exists>ts ST LT. s = (ts#ST,LT))" 
   3.159  by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
   3.160  
   3.161  
   3.162  lemma appDup_x1[simp]:
   3.163 -"app (Dup_x1, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" 
   3.164 +"app (Dup_x1, G, rT, s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" 
   3.165  by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
   3.166  
   3.167  
   3.168  lemma appDup_x2[simp]:
   3.169 -"app (Dup_x2, G, rT, s) = (\\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))"
   3.170 +"app (Dup_x2, G, rT, s) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))"
   3.171  by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
   3.172  
   3.173  
   3.174  lemma appSwap[simp]:
   3.175 -"app (Swap, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" 
   3.176 +"app (Swap, G, rT, s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" 
   3.177  by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
   3.178  
   3.179  
   3.180  lemma appIAdd[simp]:
   3.181 -"app (IAdd, G, rT, s) = (\\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))"  (is "?app s = ?P s")
   3.182 +"app (IAdd, G, rT, s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))"  (is "?app s = ?P s")
   3.183  proof (cases s)
   3.184    case Pair
   3.185    have "?app (a,b) = ?P (a,b)"
   3.186 @@ -218,44 +218,49 @@
   3.187  
   3.188  
   3.189  lemma appIfcmpeq[simp]:
   3.190 -"app (Ifcmpeq b, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \\<and> 
   3.191 -                              ((\\<exists> p. ts1 = PrimT p \\<and> ts1 = PrimT p) \\<or>  
   3.192 -                               (\\<exists>r r'. ts1 = RefT r \\<and> ts2 = RefT r')))" 
   3.193 +"app (Ifcmpeq b, G, rT, s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> 
   3.194 +                              ((\<exists> p. ts1 = PrimT p \<and> ts1 = PrimT p) \<or>  
   3.195 +                               (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))" 
   3.196  by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
   3.197  
   3.198  
   3.199  lemma appReturn[simp]:
   3.200 -"app (Return, G, rT, s) = (\\<exists>T ST LT. s = (T#ST,LT) \\<and> (G \\<turnstile> T \\<preceq> rT))" 
   3.201 +"app (Return, G, rT, s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))" 
   3.202  by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
   3.203  
   3.204  
   3.205  lemma appInvoke[simp]:
   3.206 -"app (Invoke C mn fpTs, G, rT, s) = (\\<exists>apTs X ST LT.
   3.207 -                                       s = ((rev apTs) @ (X # ST), LT) \\<and> 
   3.208 -                                       length apTs = length fpTs \\<and> 
   3.209 -                                       G \\<turnstile> X \\<preceq> Class C \\<and>  
   3.210 -                                       (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and> 
   3.211 -                                       method (G,C) (mn,fpTs) \\<noteq> None)" (is "?app s = ?P s")
   3.212 +"app (Invoke C mn fpTs, G, rT, s) = (\<exists>apTs X ST LT.
   3.213 +                                       s = ((rev apTs) @ (X # ST), LT) \<and> 
   3.214 +                                       length apTs = length fpTs \<and> 
   3.215 +                                       G \<turnstile> X \<preceq> Class C \<and>  
   3.216 +                                       (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and> 
   3.217 +                                       method (G,C) (mn,fpTs) \<noteq> None)" (is "?app s = ?P s")
   3.218  proof (cases s)
   3.219    case Pair
   3.220 -  have "?app (a,b) \\<Longrightarrow> ?P (a,b)"
   3.221 +  have "?app (a,b) \<Longrightarrow> ?P (a,b)"
   3.222    proof -
   3.223      assume app: "?app (a,b)"
   3.224 -    hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \\<and> length fpTs < length a" 
   3.225 -      (is "?a \\<and> ?l") by auto    
   3.226 -    hence "?a \\<and> 0 < length (drop (length fpTs) a)" (is "?a \\<and> ?l") by auto
   3.227 -    hence "?a \\<and> ?l \\<and> length (rev (take (length fpTs) a)) = length fpTs" by (auto simp add: min_def)
   3.228 -    hence "\\<exists>apTs ST. a = rev apTs @ ST \\<and> length apTs = length fpTs \\<and> 0 < length ST" by blast
   3.229 -    hence "\\<exists>apTs ST. a = rev apTs @ ST \\<and> length apTs = length fpTs \\<and> ST \\<noteq> []" by blast        
   3.230 -    hence "\\<exists>apTs ST. a = rev apTs @ ST \\<and> length apTs = length fpTs \\<and> (\\<exists>X ST'. ST = X#ST')" by (simp add: neq_Nil_conv)
   3.231 -    hence "\\<exists>apTs X ST. a = rev apTs @ X # ST \\<and> length apTs = length fpTs" by blast
   3.232 +    hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> length fpTs < length a" 
   3.233 +      (is "?a \<and> ?l") by auto    
   3.234 +    hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l") by auto
   3.235 +    hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs" by (auto simp add: min_def)
   3.236 +    hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST" by blast
   3.237 +    hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []" by blast        
   3.238 +    hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> (\<exists>X ST'. ST = X#ST')" by (simp add: neq_Nil_conv)
   3.239 +    hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs" by blast
   3.240      with app
   3.241      show ?thesis by auto blast
   3.242    qed
   3.243 -  with Pair have "?app s \\<Longrightarrow> ?P s" by simp
   3.244 +  with Pair have "?app s \<Longrightarrow> ?P s" by simp
   3.245    thus ?thesis by auto
   3.246  qed 
   3.247  
   3.248  lemmas [simp del] = app_invoke
   3.249  
   3.250 +
   3.251 +lemma app_step_some:
   3.252 +  "\<lbrakk>app (i,G,rT,s); succs i pc \<noteq> {}\<rbrakk> \<Longrightarrow> step (i,G,s) \<noteq> None";
   3.253 +  by (cases s, cases i, auto)
   3.254 +
   3.255  end
     4.1 --- a/src/HOL/MicroJava/BV/StepMono.thy	Fri Aug 11 14:52:39 2000 +0200
     4.2 +++ b/src/HOL/MicroJava/BV/StepMono.thy	Fri Aug 11 14:52:52 2000 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/MicroJava/BV/Step.thy
     4.5 +(*  Title:      HOL/MicroJava/BV/StepMono.thy
     4.6      ID:         $Id$
     4.7      Author:     Gerwin Klein
     4.8      Copyright   2000 Technische Universitaet Muenchen
     4.9 @@ -11,39 +11,31 @@
    4.10  
    4.11  lemmas [trans] = sup_state_trans sup_loc_trans widen_trans
    4.12  
    4.13 -ML_setup {* bind_thm ("widen_RefT", widen_RefT) *}
    4.14 -ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *}
    4.15 -
    4.16 -
    4.17 -lemma app_step_some:
    4.18 -"\\<lbrakk>app (i,G,rT,s); succs i pc \\<noteq> {} \\<rbrakk> \\<Longrightarrow> step (i,G,s) \\<noteq> None";
    4.19 -by (cases s, cases i, auto)
    4.20 -
    4.21  
    4.22  lemma sup_state_length:
    4.23 -"G \\<turnstile> s2 <=s s1 \\<Longrightarrow> length (fst s2) = length (fst s1) \\<and> length (snd s2) = length (snd s1)"
    4.24 +"G \<turnstile> s2 <=s s1 \<Longrightarrow> length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
    4.25    by (cases s1, cases s2, simp add: sup_state_length_fst sup_state_length_snd)
    4.26    
    4.27  
    4.28 -lemma PrimT_PrimT: "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)"
    4.29 +lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
    4.30  proof
    4.31 -  show "xb = PrimT p \\<Longrightarrow> G \\<turnstile> xb \\<preceq> PrimT p" by blast
    4.32 +  show "xb = PrimT p \<Longrightarrow> G \<turnstile> xb \<preceq> PrimT p" by blast
    4.33  
    4.34 -  show "G\\<turnstile> xb \\<preceq> PrimT p \\<Longrightarrow> xb = PrimT p"
    4.35 +  show "G\<turnstile> xb \<preceq> PrimT p \<Longrightarrow> xb = PrimT p"
    4.36    proof (cases xb)
    4.37      fix prim
    4.38 -    assume "xb = PrimT prim" "G\\<turnstile>xb\\<preceq>PrimT p"
    4.39 +    assume "xb = PrimT prim" "G\<turnstile>xb\<preceq>PrimT p"
    4.40      thus ?thesis by simp
    4.41    next
    4.42      fix ref
    4.43 -    assume "G\\<turnstile>xb\\<preceq>PrimT p" "xb = RefT ref"
    4.44 +    assume "G\<turnstile>xb\<preceq>PrimT p" "xb = RefT ref"
    4.45      thus ?thesis by simp (rule widen_RefT [elimify], auto)
    4.46    qed
    4.47  qed
    4.48  
    4.49  
    4.50  lemma sup_loc_some [rulify]:
    4.51 -"\\<forall> y n. (G \\<turnstile> b <=l y) \\<longrightarrow> n < length y \\<longrightarrow> y!n = Some t \\<longrightarrow> (\\<exists>t. b!n = Some t \\<and> (G \\<turnstile> (b!n) <=o (y!n)))" (is "?P b")
    4.52 +"\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Some t \<longrightarrow> (\<exists>t. b!n = Some t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
    4.53  proof (induct "?P" b)
    4.54    show "?P []" by simp
    4.55  
    4.56 @@ -52,10 +44,10 @@
    4.57    proof (clarsimp simp add: list_all2_Cons1 sup_loc_def)
    4.58      fix z zs n
    4.59      assume * : 
    4.60 -      "G \\<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs" 
    4.61 +      "G \<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs" 
    4.62        "n < Suc (length zs)" "(z # zs) ! n = Some t"
    4.63  
    4.64 -    show "(\\<exists>t. (a # list) ! n = Some t) \\<and> G \\<turnstile>(a # list) ! n <=o Some t" 
    4.65 +    show "(\<exists>t. (a # list) ! n = Some t) \<and> G \<turnstile>(a # list) ! n <=o Some t" 
    4.66      proof (cases n) 
    4.67        case 0
    4.68        with * show ?thesis by (simp add: sup_ty_opt_some)
    4.69 @@ -69,8 +61,8 @@
    4.70     
    4.71  
    4.72  lemma all_widen_is_sup_loc:
    4.73 -"\\<forall>b. length a = length b \\<longrightarrow> (\\<forall>x\\<in>set (zip a b). x \\<in> widen G) = (G \\<turnstile> (map Some a) <=l (map Some b))" 
    4.74 - (is "\\<forall>b. length a = length b \\<longrightarrow> ?Q a b" is "?P a")
    4.75 +"\<forall>b. length a = length b \<longrightarrow> (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map Some a) <=l (map Some b))" 
    4.76 + (is "\<forall>b. length a = length b \<longrightarrow> ?Q a b" is "?P a")
    4.77  proof (induct "a")
    4.78    show "?P []" by simp
    4.79  
    4.80 @@ -87,7 +79,7 @@
    4.81   
    4.82  
    4.83  lemma append_length_n [rulify]: 
    4.84 -"\\<forall>n. n \\<le> length x \\<longrightarrow> (\\<exists>a b. x = a@b \\<and> length a = n)" (is "?P x")
    4.85 +"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
    4.86  proof (induct "?P" "x")
    4.87    show "?P []" by simp
    4.88  
    4.89 @@ -96,22 +88,22 @@
    4.90    show "?P (l#ls)"
    4.91    proof (intro allI impI)
    4.92      fix n
    4.93 -    assume l: "n \\<le> length (l # ls)"
    4.94 +    assume l: "n \<le> length (l # ls)"
    4.95  
    4.96 -    show "\\<exists>a b. l # ls = a @ b \\<and> length a = n" 
    4.97 +    show "\<exists>a b. l # ls = a @ b \<and> length a = n" 
    4.98      proof (cases n)
    4.99        assume "n=0" thus ?thesis by simp
   4.100      next
   4.101        fix "n'" assume s: "n = Suc n'"
   4.102        with l 
   4.103 -      have  "n' \\<le> length ls" by simp 
   4.104 -      hence "\\<exists>a b. ls = a @ b \\<and> length a = n'" by (rule Cons [rulify])
   4.105 +      have  "n' \<le> length ls" by simp 
   4.106 +      hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rulify])
   4.107        thus ?thesis
   4.108        proof elim
   4.109          fix a b 
   4.110          assume "ls = a @ b" "length a = n'"
   4.111          with s
   4.112 -        have "l # ls = (l#a) @ b \\<and> length (l#a) = n" by simp
   4.113 +        have "l # ls = (l#a) @ b \<and> length (l#a) = n" by simp
   4.114          thus ?thesis by blast
   4.115        qed
   4.116      qed
   4.117 @@ -121,23 +113,23 @@
   4.118  
   4.119  
   4.120  lemma rev_append_cons:
   4.121 -"\\<lbrakk>n < length x\\<rbrakk> \\<Longrightarrow> \\<exists>a b c. x = (rev a) @ b # c \\<and> length a = n"
   4.122 +"\<lbrakk>n < length x\<rbrakk> \<Longrightarrow> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
   4.123  proof -
   4.124    assume n: "n < length x"
   4.125 -  hence "n \\<le> length x" by simp
   4.126 -  hence "\\<exists>a b. x = a @ b \\<and> length a = n" by (rule append_length_n)
   4.127 +  hence "n \<le> length x" by simp
   4.128 +  hence "\<exists>a b. x = a @ b \<and> length a = n" by (rule append_length_n)
   4.129    thus ?thesis
   4.130    proof elim
   4.131      fix r d assume x: "x = r@d" "length r = n"
   4.132      with n
   4.133 -    have "\\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
   4.134 +    have "\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
   4.135      
   4.136      thus ?thesis 
   4.137      proof elim
   4.138        fix b c 
   4.139        assume "d = b#c"
   4.140        with x
   4.141 -      have "x = (rev (rev r)) @ b # c \\<and> length (rev r) = n" by simp
   4.142 +      have "x = (rev (rev r)) @ b # c \<and> length (rev r) = n" by simp
   4.143        thus ?thesis by blast
   4.144      qed
   4.145    qed
   4.146 @@ -145,9 +137,9 @@
   4.147  
   4.148  
   4.149  lemma app_mono: 
   4.150 -"\\<lbrakk>G \\<turnstile> s2 <=s s1; app (i, G, rT, s1)\\<rbrakk> \\<Longrightarrow> app (i, G, rT, s2)";
   4.151 +"\<lbrakk>G \<turnstile> s2 <=s s1; app (i, G, rT, s1)\<rbrakk> \<Longrightarrow> app (i, G, rT, s2)";
   4.152  proof -
   4.153 -  assume G:   "G \\<turnstile> s2 <=s s1"
   4.154 +  assume G:   "G \<turnstile> s2 <=s s1"
   4.155    assume app: "app (i, G, rT, s1)"
   4.156    
   4.157    show ?thesis
   4.158 @@ -158,7 +150,7 @@
   4.159      have l: "length (snd s1) = length (snd s2)" by (simp add: sup_state_length)
   4.160  
   4.161      from G Load app
   4.162 -    have "G \\<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_def)
   4.163 +    have "G \<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_def)
   4.164      
   4.165      with G Load app l
   4.166      show ?thesis by clarsimp (drule sup_loc_some, simp+)
   4.167 @@ -191,22 +183,22 @@
   4.168        where s1: "s1 = (vT # oT # ST, LT)" and
   4.169                  "field (G, cname) vname = Some (cname, b)" 
   4.170                  "is_class G cname" and
   4.171 -            oT: "G\\<turnstile> oT\\<preceq> (Class cname)" and
   4.172 -            vT: "G\\<turnstile> vT\\<preceq> b"
   4.173 +            oT: "G\<turnstile> oT\<preceq> (Class cname)" and
   4.174 +            vT: "G\<turnstile> vT\<preceq> b"
   4.175        by simp (elim exE conjE, simp, rule that)
   4.176      moreover
   4.177      from s1 G
   4.178      obtain vT' oT' ST' LT'
   4.179        where s2:  "s2 = (vT' # oT' # ST', LT')" and
   4.180 -            oT': "G\\<turnstile> oT' \\<preceq> oT" and
   4.181 -            vT': "G\\<turnstile> vT' \\<preceq> vT"
   4.182 +            oT': "G\<turnstile> oT' \<preceq> oT" and
   4.183 +            vT': "G\<turnstile> vT' \<preceq> vT"
   4.184        by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
   4.185      moreover
   4.186      from vT' vT
   4.187 -    have "G \\<turnstile> vT' \\<preceq> b" by (rule widen_trans)
   4.188 +    have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans)
   4.189      moreover
   4.190      from oT' oT
   4.191 -    have "G\\<turnstile> oT' \\<preceq> (Class cname)" by (rule widen_trans)
   4.192 +    have "G\<turnstile> oT' \<preceq> (Class cname)" by (rule widen_trans)
   4.193      ultimately
   4.194      show ?thesis
   4.195        by (auto simp add: Putfield)
   4.196 @@ -214,12 +206,12 @@
   4.197      case Checkcast
   4.198      with app G
   4.199      show ?thesis 
   4.200 -      by - (cases s2, auto intro: widen_RefT2 simp add: sup_state_Cons2)
   4.201 +      by - (cases s2, auto intro!: widen_RefT2 simp add: sup_state_Cons2)
   4.202    next
   4.203      case Return
   4.204      with app G
   4.205      show ?thesis
   4.206 -      by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans)
   4.207 +      by - (cases s2, auto simp add: sup_state_Cons2, rule widen_trans)
   4.208    next
   4.209      case Pop
   4.210      with app G
   4.211 @@ -266,9 +258,9 @@
   4.212      obtain apTs X ST LT where
   4.213        s1: "s1 = (rev apTs @ X # ST, LT)" and
   4.214        l:  "length apTs = length list" and
   4.215 -      C:  "G \\<turnstile> X \\<preceq> Class cname" and
   4.216 -      w:  "\\<forall>x \\<in> set (zip apTs list). x \\<in> widen G" and
   4.217 -      m:  "method (G, cname) (mname, list) \\<noteq> None"
   4.218 +      C:  "G \<turnstile> X \<preceq> Class cname" and
   4.219 +      w:  "\<forall>x \<in> set (zip apTs list). x \<in> widen G" and
   4.220 +      m:  "method (G, cname) (mname, list) \<noteq> None"
   4.221        by (simp del: not_None_eq, elim exE conjE) (rule that)
   4.222  
   4.223      obtain apTs' X' ST' LT' where
   4.224 @@ -278,7 +270,7 @@
   4.225        from l s1 G 
   4.226        have "length list < length (fst s2)" 
   4.227          by (simp add: sup_state_length)
   4.228 -      hence "\\<exists>a b c. (fst s2) = rev a @ b # c \\<and> length a = length list"
   4.229 +      hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
   4.230          by (rule rev_append_cons [rulify])
   4.231        thus ?thesis
   4.232          by -  (cases s2, elim exE conjE, simp, rule that) 
   4.233 @@ -289,26 +281,26 @@
   4.234      
   4.235      from this s1 s2 G 
   4.236      obtain
   4.237 -      G': "G \\<turnstile> (apTs',LT') <=s (apTs,LT)" and
   4.238 -      X : "G \\<turnstile>  X' \\<preceq> X" and "G \\<turnstile> (ST',LT') <=s (ST,LT)"
   4.239 +      G': "G \<turnstile> (apTs',LT') <=s (apTs,LT)" and
   4.240 +      X : "G \<turnstile>  X' \<preceq> X" and "G \<turnstile> (ST',LT') <=s (ST,LT)"
   4.241        by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1);
   4.242          
   4.243      with C
   4.244 -    have C': "G \\<turnstile> X' \\<preceq> Class cname"
   4.245 +    have C': "G \<turnstile> X' \<preceq> Class cname"
   4.246        by - (rule widen_trans, auto)
   4.247      
   4.248      from G'
   4.249 -    have "G \\<turnstile> map Some apTs' <=l map Some apTs"
   4.250 +    have "G \<turnstile> map Some apTs' <=l map Some apTs"
   4.251        by (simp add: sup_state_def)
   4.252      also
   4.253      from l w
   4.254 -    have "G \\<turnstile> map Some apTs <=l map Some list" 
   4.255 +    have "G \<turnstile> map Some apTs <=l map Some list" 
   4.256        by (simp add: all_widen_is_sup_loc)
   4.257      finally
   4.258 -    have "G \\<turnstile> map Some apTs' <=l map Some list" .
   4.259 +    have "G \<turnstile> map Some apTs' <=l map Some list" .
   4.260  
   4.261      with l'
   4.262 -    have w': "\\<forall>x \\<in> set (zip apTs' list). x \\<in> widen G"
   4.263 +    have w': "\<forall>x \<in> set (zip apTs' list). x \<in> widen G"
   4.264        by (simp add: all_widen_is_sup_loc)
   4.265  
   4.266      from Invoke s2 l' w' C' m
   4.267 @@ -319,14 +311,14 @@
   4.268      
   4.269  
   4.270  lemma step_mono:
   4.271 -"\\<lbrakk>succs i pc \\<noteq> {}; app (i,G,rT,s2); G \\<turnstile> s1 <=s s2\\<rbrakk> \\<Longrightarrow> 
   4.272 -  G \\<turnstile> the (step (i,G,s1)) <=s the (step (i,G,s2))"
   4.273 +"\<lbrakk>succs i pc \<noteq> {}; app (i,G,rT,s2); G \<turnstile> s1 <=s s2\<rbrakk> \<Longrightarrow> 
   4.274 +  G \<turnstile> the (step (i,G,s1)) <=s the (step (i,G,s2))"
   4.275  proof (cases s1, cases s2) 
   4.276    fix a1 b1 a2 b2
   4.277    assume s: "s1 = (a1,b1)" "s2 = (a2,b2)"
   4.278 -  assume succs: "succs i pc \\<noteq> {}"
   4.279 +  assume succs: "succs i pc \<noteq> {}"
   4.280    assume app2: "app (i,G,rT,s2)"
   4.281 -  assume G: "G \\<turnstile> s1 <=s s2"
   4.282 +  assume G: "G \<turnstile> s1 <=s s2"
   4.283  
   4.284    from G app2
   4.285    have app1: "app (i,G,rT,s1)" by (rule app_mono)
   4.286 @@ -334,9 +326,9 @@
   4.287    from app1 app2 succs
   4.288    obtain a1' b1' a2' b2'
   4.289      where step: "step (i,G,s1) = Some (a1',b1')" "step (i,G,s2) = Some (a2',b2')";
   4.290 -    by (auto dest: app_step_some);
   4.291 +    by (auto dest!: app_step_some);
   4.292  
   4.293 -  have "G \\<turnstile> (a1',b1') <=s (a2',b2')"
   4.294 +  have "G \<turnstile> (a1',b1') <=s (a2',b2')"
   4.295    proof (cases i)
   4.296      case Load
   4.297  
   4.298 @@ -349,10 +341,10 @@
   4.299         y': "nat < length b2" "b2 ! nat = Some y'" by clarsimp
   4.300  
   4.301      from G s 
   4.302 -    have "G \\<turnstile> b1 <=l b2" by (simp add: sup_state_def)
   4.303 +    have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_def)
   4.304  
   4.305      with y y'
   4.306 -    have "G \\<turnstile> y \\<preceq> y'" 
   4.307 +    have "G \<turnstile> y \<preceq> y'" 
   4.308        by - (drule sup_loc_some, simp+)
   4.309      
   4.310      with Load G y y' s step app1 app2 
   4.311 @@ -411,17 +403,17 @@
   4.312      have lr: "length a = length a'" by simp
   4.313        
   4.314      from lr G s s1 s2 
   4.315 -    have "G \\<turnstile> (ST, b1) <=s (ST', b2)"
   4.316 +    have "G \<turnstile> (ST, b1) <=s (ST', b2)"
   4.317        by (simp add: sup_state_append_fst sup_state_Cons1)
   4.318      
   4.319      moreover
   4.320      
   4.321      from Invoke G s step app1 app2
   4.322 -    have "b1 = b1' \\<and> b2 = b2'" by simp
   4.323 +    have "b1 = b1' \<and> b2 = b2'" by simp
   4.324  
   4.325      ultimately 
   4.326  
   4.327 -    have "G \\<turnstile> (ST, b1') <=s (ST', b2')" by simp
   4.328 +    have "G \<turnstile> (ST, b1') <=s (ST', b2')" by simp
   4.329  
   4.330      with Invoke G s step app1 app2 s1 s2 l l'
   4.331      show ?thesis