symbolized
authorkleing
Sun Mar 03 16:59:08 2002 +0100 (2002-03-03)
changeset 1300651c5f3f11d16
parent 13005 42a54d6cec15
child 13007 0940d19b2e2b
symbolized
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/MicroJava/BV/BVSpec.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/BV/Effect.thy
src/HOL/MicroJava/BV/EffectMono.thy
src/HOL/MicroJava/BV/Err.thy
src/HOL/MicroJava/BV/JType.thy
src/HOL/MicroJava/BV/JVM.thy
src/HOL/MicroJava/BV/JVMType.thy
src/HOL/MicroJava/BV/Kildall.thy
src/HOL/MicroJava/BV/LBVComplete.thy
src/HOL/MicroJava/BV/LBVCorrect.thy
src/HOL/MicroJava/BV/LBVSpec.thy
src/HOL/MicroJava/BV/Listn.thy
src/HOL/MicroJava/BV/Opt.thy
src/HOL/MicroJava/BV/Product.thy
src/HOL/MicroJava/BV/Semilat.thy
src/HOL/MicroJava/BV/Typing_Framework.thy
src/HOL/MicroJava/BV/Typing_Framework_err.thy
src/HOL/MicroJava/JVM/JVMExec.thy
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Sat Mar 02 12:09:23 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Sun Mar 03 16:59:08 2002 +0100
     1.3 @@ -276,8 +276,7 @@
     1.4    apply simp
     1.5    done
     1.6  
     1.7 -text {* Some shorthands to make the welltyping of method @{term
     1.8 -makelist_name} easier to read *} 
     1.9 +text {* Some abbreviations for readability *} 
    1.10  syntax
    1.11    list :: ty 
    1.12    test :: ty
    1.13 @@ -382,4 +381,4 @@
    1.14    apply (simp add: conf_def start_heap_def)
    1.15    done
    1.16  
    1.17 -end
    1.18 \ No newline at end of file
    1.19 +end
     2.1 --- a/src/HOL/MicroJava/BV/BVSpec.thy	Sat Mar 02 12:09:23 2002 +0100
     2.2 +++ b/src/HOL/MicroJava/BV/BVSpec.thy	Sun Mar 03 16:59:08 2002 +0100
     2.3 @@ -17,42 +17,42 @@
     2.4  
     2.5  constdefs
     2.6    wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
     2.7 -                exception_table,p_count] => bool"
     2.8 +                exception_table,p_count] \<Rightarrow> bool"
     2.9    "wt_instr i G rT phi mxs max_pc et pc == 
    2.10    app i G mxs rT pc et (phi!pc) \<and>
    2.11    (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
    2.12  
    2.13 -  wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
    2.14 +  wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
    2.15    "wt_start G C pTs mxl phi == 
    2.16    G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
    2.17  
    2.18    wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
    2.19 -                 exception_table,method_type] => bool"
    2.20 +                 exception_table,method_type] \<Rightarrow> bool"
    2.21    "wt_method G C pTs rT mxs mxl ins et phi ==
    2.22    let max_pc = length ins in
    2.23    0 < max_pc \<and> wt_start G C pTs mxl phi \<and> 
    2.24 -  (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc et pc)"
    2.25 +  (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins ! pc) G rT phi mxs max_pc et pc)"
    2.26  
    2.27 -  wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
    2.28 +  wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
    2.29    "wt_jvm_prog G phi ==
    2.30    wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
    2.31             wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"
    2.32  
    2.33  
    2.34  lemma wt_jvm_progD:
    2.35 -  "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
    2.36 +  "wt_jvm_prog G phi \<Longrightarrow> (\<exists>wt. wf_prog wt G)"
    2.37    by (unfold wt_jvm_prog_def, blast)
    2.38  
    2.39  lemma wt_jvm_prog_impl_wt_instr:
    2.40 -  "[| wt_jvm_prog G phi; is_class G C;
    2.41 -      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins |] 
    2.42 -  ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc";
    2.43 +  "\<lbrakk> wt_jvm_prog G phi; is_class G C;
    2.44 +      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins \<rbrakk> 
    2.45 +  \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc";
    2.46    by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
    2.47        simp, simp, simp add: wf_mdecl_def wt_method_def)
    2.48  
    2.49  lemma wt_jvm_prog_impl_wt_start:
    2.50 -  "[| wt_jvm_prog G phi; is_class G C;
    2.51 -      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) |] ==> 
    2.52 +  "\<lbrakk> wt_jvm_prog G phi; is_class G C;
    2.53 +      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) \<rbrakk> \<Longrightarrow> 
    2.54    0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
    2.55    by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
    2.56        simp, simp, simp add: wf_mdecl_def wt_method_def)
     3.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sat Mar 02 12:09:23 2002 +0100
     3.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sun Mar 03 16:59:08 2002 +0100
     3.3 @@ -31,9 +31,9 @@
     3.4    can directly infer that the current instruction is well typed:
     3.5  *}
     3.6  lemma wt_jvm_prog_impl_wt_instr_cor:
     3.7 -  "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
     3.8 -      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
     3.9 -  ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
    3.10 +  "\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
    3.11 +      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
    3.12 +  \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
    3.13  apply (unfold correct_state_def Let_def correct_frame_def)
    3.14  apply simp
    3.15  apply (blast intro: wt_jvm_prog_impl_wt_instr)
    3.16 @@ -57,10 +57,10 @@
    3.17    @{text match_exception_table} from the operational semantics:
    3.18  *}
    3.19  lemma in_match_any:
    3.20 -  "match_exception_table G xcpt pc et = Some pc' ==> 
    3.21 +  "match_exception_table G xcpt pc et = Some pc' \<Longrightarrow> 
    3.22    \<exists>C. C \<in> set (match_any G pc et) \<and> G \<turnstile> xcpt \<preceq>C C \<and> 
    3.23        match_exception_table G C pc et = Some pc'"
    3.24 -  (is "PROP ?P et" is "?match et ==> ?match_any et")
    3.25 +  (is "PROP ?P et" is "?match et \<Longrightarrow> ?match_any et")
    3.26  proof (induct et)  
    3.27    show "PROP ?P []" 
    3.28      by simp
    3.29 @@ -131,10 +131,10 @@
    3.30    conforms. 
    3.31  *}
    3.32  lemma uncaught_xcpt_correct:
    3.33 -  "!!f. [| wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T;
    3.34 -      G,phi \<turnstile>JVM (None, hp, f#frs)\<surd> |]
    3.35 -  ==> G,phi \<turnstile>JVM (find_handler G (Some xcp) hp frs)\<surd>" 
    3.36 -  (is "!!f. [| ?wt; ?adr; ?hp; ?correct (None, hp, f#frs) |] ==> ?correct (?find frs)")
    3.37 +  "\<And>f. \<lbrakk> wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T;
    3.38 +      G,phi \<turnstile>JVM (None, hp, f#frs)\<surd> \<rbrakk>
    3.39 +  \<Longrightarrow> G,phi \<turnstile>JVM (find_handler G (Some xcp) hp frs)\<surd>" 
    3.40 +  (is "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?correct (None, hp, f#frs) \<rbrakk> \<Longrightarrow> ?correct (?find frs)")
    3.41  proof (induct frs) 
    3.42    -- "the base case is trivial, as it should be"
    3.43    show "?correct (?find [])" by (simp add: correct_state_def)
    3.44 @@ -153,9 +153,9 @@
    3.45  
    3.46    -- "the induction hypothesis as produced by Isabelle, immediatly simplified
    3.47      with the fixed assumptions above"
    3.48 -  assume "\<And>f. [| ?wt; ?adr; ?hp; ?correct (None, hp, f#frs') |] ==> ?correct (?find frs')"  
    3.49 +  assume "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?correct (None, hp, f#frs') \<rbrakk> \<Longrightarrow> ?correct (?find frs')"  
    3.50    with wt adr hp 
    3.51 -  have IH: "\<And>f. ?correct (None, hp, f#frs') ==> ?correct (?find frs')" by blast
    3.52 +  have IH: "\<And>f. ?correct (None, hp, f#frs') \<Longrightarrow> ?correct (?find frs')" by blast
    3.53  
    3.54    from cr
    3.55    have cr': "?correct (None, hp, f'#frs')" by (auto simp add: correct_state_def)
    3.56 @@ -249,11 +249,11 @@
    3.57    for welltyped instructions and conformant states:
    3.58  *}
    3.59  lemma exec_instr_xcpt_hp:
    3.60 -  "[|  fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp;
    3.61 +  "\<lbrakk>  fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp;
    3.62         wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
    3.63 -       G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
    3.64 -  ==> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T" 
    3.65 -  (is "[| ?xcpt; ?wt; ?correct |] ==> ?thesis")
    3.66 +       G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
    3.67 +  \<Longrightarrow> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T" 
    3.68 +  (is "\<lbrakk> ?xcpt; ?wt; ?correct \<rbrakk> \<Longrightarrow> ?thesis")
    3.69  proof -
    3.70    note [simp] = split_beta raise_system_xcpt_def
    3.71    note [split] = split_if_asm option.split_asm 
    3.72 @@ -279,13 +279,13 @@
    3.73    resulting next state always conforms:
    3.74  *}
    3.75  lemma xcpt_correct:
    3.76 -  "[| wt_jvm_prog G phi;
    3.77 +  "\<lbrakk> wt_jvm_prog G phi;
    3.78        method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
    3.79        wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
    3.80        fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp; 
    3.81        Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
    3.82 -      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
    3.83 -  ==> G,phi \<turnstile>JVM state'\<surd>"
    3.84 +      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
    3.85 +  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    3.86  proof -
    3.87    assume wtp: "wt_jvm_prog G phi"
    3.88    assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
    3.89 @@ -588,47 +588,47 @@
    3.90  lemmas [iff] = not_Err_eq
    3.91  
    3.92  lemma Load_correct:
    3.93 -"[| wf_prog wt G;
    3.94 +"\<lbrakk> wf_prog wt G;
    3.95      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
    3.96      ins!pc = Load idx; 
    3.97      wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
    3.98      Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
    3.99 -    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
   3.100 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.101 +    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
   3.102 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.103  apply (clarsimp simp add: defs1 map_eq_Cons)
   3.104  apply (blast intro: approx_loc_imp_approx_val_sup)
   3.105  done
   3.106  
   3.107  lemma Store_correct:
   3.108 -"[| wf_prog wt G;
   3.109 +"\<lbrakk> wf_prog wt G;
   3.110    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
   3.111    ins!pc = Store idx;
   3.112    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
   3.113    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
   3.114 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
   3.115 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.116 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
   3.117 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.118  apply (clarsimp simp add: defs1 map_eq_Cons)
   3.119  apply (blast intro: approx_loc_subst)
   3.120  done
   3.121  
   3.122  
   3.123  lemma LitPush_correct:
   3.124 -"[| wf_prog wt G;
   3.125 +"\<lbrakk> wf_prog wt G;
   3.126      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.127      ins!pc = LitPush v;
   3.128      wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.129      Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
   3.130 -    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
   3.131 -==> G,phi \<turnstile>JVM state'\<surd>" 
   3.132 +    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
   3.133 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
   3.134  apply (clarsimp simp add: defs1 sup_PTS_eq map_eq_Cons)
   3.135  apply (blast dest: conf_litval intro: conf_widen)
   3.136  done
   3.137  
   3.138  
   3.139  lemma Cast_conf2:
   3.140 -  "[| wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; 
   3.141 -      G\<turnstile>Class C\<preceq>T; is_class G C|] 
   3.142 -  ==> G,h\<turnstile>v::\<preceq>T"
   3.143 +  "\<lbrakk> wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; 
   3.144 +      G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk> 
   3.145 +  \<Longrightarrow> G,h\<turnstile>v::\<preceq>T"
   3.146  apply (unfold cast_ok_def)
   3.147  apply (frule widen_Class)
   3.148  apply (elim exE disjE) 
   3.149 @@ -641,28 +641,28 @@
   3.150  lemmas defs1 = defs1 raise_system_xcpt_def
   3.151  
   3.152  lemma Checkcast_correct:
   3.153 -"[| wt_jvm_prog G phi;
   3.154 +"\<lbrakk> wt_jvm_prog G phi;
   3.155      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.156      ins!pc = Checkcast D; 
   3.157      wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.158      Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.159      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   3.160 -    fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] 
   3.161 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.162 +    fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   3.163 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.164  apply (clarsimp simp add: defs1 wt_jvm_prog_def map_eq_Cons split: split_if_asm)
   3.165  apply (blast intro: Cast_conf2)
   3.166  done
   3.167  
   3.168  
   3.169  lemma Getfield_correct:
   3.170 -"[| wt_jvm_prog G phi;
   3.171 +"\<lbrakk> wt_jvm_prog G phi;
   3.172    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.173    ins!pc = Getfield F D; 
   3.174    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.175    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.176    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   3.177 -  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] 
   3.178 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.179 +  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   3.180 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.181  apply (clarsimp simp add: defs1 map_eq_Cons wt_jvm_prog_def 
   3.182                  split: option.split split_if_asm)
   3.183  apply (frule conf_widen)
   3.184 @@ -687,14 +687,14 @@
   3.185  
   3.186  
   3.187  lemma Putfield_correct:
   3.188 -"[| wf_prog wt G;
   3.189 +"\<lbrakk> wf_prog wt G;
   3.190    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.191    ins!pc = Putfield F D; 
   3.192    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.193    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.194    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   3.195 -  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] 
   3.196 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.197 +  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   3.198 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.199  apply (clarsimp simp add: defs1 split_beta split: option.split List.split split_if_asm)
   3.200  apply (frule conf_widen)
   3.201  prefer 2
   3.202 @@ -715,14 +715,14 @@
   3.203      
   3.204  
   3.205  lemma New_correct:
   3.206 -"[| wf_prog wt G;
   3.207 +"\<lbrakk> wf_prog wt G;
   3.208    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.209    ins!pc = New X; 
   3.210    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.211    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.212    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   3.213 -  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] 
   3.214 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.215 +  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   3.216 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.217  proof -
   3.218    assume wf:   "wf_prog wt G"
   3.219    assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
   3.220 @@ -793,14 +793,14 @@
   3.221  
   3.222  
   3.223  lemma Invoke_correct: 
   3.224 -"[| wt_jvm_prog G phi; 
   3.225 +"\<lbrakk> wt_jvm_prog G phi; 
   3.226    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.227    ins ! pc = Invoke C' mn pTs; 
   3.228    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.229    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.230    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   3.231 -  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] 
   3.232 -==> G,phi \<turnstile>JVM state'\<surd>" 
   3.233 +  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   3.234 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
   3.235  proof -
   3.236    assume wtprog: "wt_jvm_prog G phi"
   3.237    assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
   3.238 @@ -972,13 +972,13 @@
   3.239  lemmas [simp del] = map_append
   3.240  
   3.241  lemma Return_correct:
   3.242 -"[| wt_jvm_prog G phi; 
   3.243 +"\<lbrakk> wt_jvm_prog G phi; 
   3.244    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.245    ins ! pc = Return; 
   3.246    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.247    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.248 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
   3.249 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.250 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
   3.251 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.252  proof -
   3.253    assume wt_prog: "wt_jvm_prog G phi"
   3.254    assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
   3.255 @@ -1098,110 +1098,110 @@
   3.256  lemmas [simp] = map_append
   3.257  
   3.258  lemma Goto_correct:
   3.259 -"[| wf_prog wt G; 
   3.260 +"\<lbrakk> wf_prog wt G; 
   3.261    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.262    ins ! pc = Goto branch; 
   3.263    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.264    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.265 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   3.266 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.267 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   3.268 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.269  apply (clarsimp simp add: defs1)
   3.270  apply fast
   3.271  done
   3.272  
   3.273  
   3.274  lemma Ifcmpeq_correct:
   3.275 -"[| wf_prog wt G; 
   3.276 +"\<lbrakk> wf_prog wt G; 
   3.277    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.278    ins ! pc = Ifcmpeq branch; 
   3.279    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.280    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.281 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   3.282 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.283 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   3.284 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.285  apply (clarsimp simp add: defs1)
   3.286  apply fast
   3.287  done
   3.288  
   3.289  lemma Pop_correct:
   3.290 -"[| wf_prog wt G; 
   3.291 +"\<lbrakk> wf_prog wt G; 
   3.292    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.293    ins ! pc = Pop;
   3.294    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.295    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.296 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   3.297 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.298 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   3.299 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.300  apply (clarsimp simp add: defs1)
   3.301  apply fast
   3.302  done
   3.303  
   3.304  lemma Dup_correct:
   3.305 -"[| wf_prog wt G; 
   3.306 +"\<lbrakk> wf_prog wt G; 
   3.307    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.308    ins ! pc = Dup;
   3.309    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.310    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.311 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   3.312 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.313 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   3.314 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.315  apply (clarsimp simp add: defs1 map_eq_Cons)
   3.316  apply (blast intro: conf_widen)
   3.317  done
   3.318  
   3.319  lemma Dup_x1_correct:
   3.320 -"[| wf_prog wt G; 
   3.321 +"\<lbrakk> wf_prog wt G; 
   3.322    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.323    ins ! pc = Dup_x1;
   3.324    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.325    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.326 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   3.327 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.328 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   3.329 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.330  apply (clarsimp simp add: defs1 map_eq_Cons)
   3.331  apply (blast intro: conf_widen)
   3.332  done
   3.333  
   3.334  lemma Dup_x2_correct:
   3.335 -"[| wf_prog wt G; 
   3.336 +"\<lbrakk> wf_prog wt G; 
   3.337    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.338    ins ! pc = Dup_x2;
   3.339    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.340    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.341 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   3.342 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.343 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   3.344 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.345  apply (clarsimp simp add: defs1 map_eq_Cons)
   3.346  apply (blast intro: conf_widen)
   3.347  done
   3.348  
   3.349  lemma Swap_correct:
   3.350 -"[| wf_prog wt G; 
   3.351 +"\<lbrakk> wf_prog wt G; 
   3.352    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.353    ins ! pc = Swap;
   3.354    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.355    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.356 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   3.357 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.358 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   3.359 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.360  apply (clarsimp simp add: defs1 map_eq_Cons)
   3.361  apply (blast intro: conf_widen)
   3.362  done
   3.363  
   3.364  lemma IAdd_correct:
   3.365 -"[| wf_prog wt G; 
   3.366 +"\<lbrakk> wf_prog wt G; 
   3.367    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.368    ins ! pc = IAdd; 
   3.369    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   3.370    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.371 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   3.372 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.373 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   3.374 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.375  apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
   3.376  apply blast
   3.377  done
   3.378  
   3.379  lemma Throw_correct:
   3.380 -"[| wf_prog wt G; 
   3.381 +"\<lbrakk> wf_prog wt G; 
   3.382    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   3.383    ins ! pc = Throw; 
   3.384    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   3.385    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   3.386 -  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] 
   3.387 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.388 +  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   3.389 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.390    by simp
   3.391  
   3.392  
   3.393 @@ -1213,11 +1213,11 @@
   3.394    into another conforming state when one instruction is executed.
   3.395  *}
   3.396  theorem instr_correct:
   3.397 -"[| wt_jvm_prog G phi;
   3.398 +"\<lbrakk> wt_jvm_prog G phi;
   3.399    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
   3.400    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
   3.401 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   3.402 -==> G,phi \<turnstile>JVM state'\<surd>"
   3.403 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   3.404 +\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.405  apply (frule wt_jvm_prog_impl_wt_instr_cor)
   3.406  apply assumption+
   3.407  apply (cases "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs)")
   3.408 @@ -1254,13 +1254,13 @@
   3.409  
   3.410  lemma correct_state_impl_Some_method:
   3.411    "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
   3.412 -  ==> \<exists>meth. method (G,C) sig = Some(C,meth)"
   3.413 +  \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
   3.414  by (auto simp add: correct_state_def Let_def)
   3.415  
   3.416  
   3.417  lemma BV_correct_1 [rule_format]:
   3.418 -"!!state. [| wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>|] 
   3.419 - ==> exec (G,state) = Some state' --> G,phi \<turnstile>JVM state'\<surd>"
   3.420 +"\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> 
   3.421 + \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   3.422  apply (simp only: split_tupled_all)
   3.423  apply (rename_tac xp hp frs)
   3.424  apply (case_tac xp)
   3.425 @@ -1277,19 +1277,19 @@
   3.426  
   3.427  
   3.428  lemma L0:
   3.429 -  "[| xp=None; frs\<noteq>[] |] ==> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
   3.430 +  "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
   3.431  by (clarsimp simp add: neq_Nil_conv split_beta)
   3.432  
   3.433  lemma L1:
   3.434 -  "[|wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]|] 
   3.435 -  ==> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
   3.436 +  "\<lbrakk>wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]\<rbrakk> 
   3.437 +  \<Longrightarrow> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
   3.438  apply (drule L0)
   3.439  apply assumption
   3.440  apply (fast intro: BV_correct_1)
   3.441  done
   3.442  
   3.443  theorem BV_correct [rule_format]:
   3.444 -"[| wt_jvm_prog G phi; G \<turnstile> s -jvm-> t |] ==> G,phi \<turnstile>JVM s\<surd> --> G,phi \<turnstile>JVM t\<surd>"
   3.445 +"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>"
   3.446  apply (unfold exec_all_def)
   3.447  apply (erule rtrancl_induct)
   3.448   apply simp
   3.449 @@ -1297,9 +1297,9 @@
   3.450  done
   3.451  
   3.452  theorem BV_correct_implies_approx:
   3.453 -"[| wt_jvm_prog G phi; 
   3.454 -    G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|] 
   3.455 -==> approx_stk G hp stk (fst (the (phi C sig ! pc))) \<and> 
   3.456 +"\<lbrakk> wt_jvm_prog G phi; 
   3.457 +    G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> 
   3.458 +\<Longrightarrow> approx_stk G hp stk (fst (the (phi C sig ! pc))) \<and> 
   3.459      approx_loc G hp loc (snd (the (phi C sig ! pc)))"
   3.460  apply (drule BV_correct)
   3.461  apply assumption+
     4.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Sat Mar 02 12:09:23 2002 +0100
     4.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Sun Mar 03 16:59:08 2002 +0100
     4.3 @@ -12,23 +12,23 @@
     4.4  theory Correct = BVSpec + JVMExec:
     4.5  
     4.6  constdefs
     4.7 -  approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
     4.8 -  "approx_val G h v any == case any of Err => True | OK T => G,h\<turnstile>v::\<preceq>T"
     4.9 +  approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
    4.10 +  "approx_val G h v any == case any of Err \<Rightarrow> True | OK T \<Rightarrow> G,h\<turnstile>v::\<preceq>T"
    4.11  
    4.12 -  approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
    4.13 +  approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool"
    4.14    "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
    4.15  
    4.16 -  approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
    4.17 +  approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool"
    4.18    "approx_stk G hp stk ST == approx_loc G hp stk (map OK ST)"
    4.19  
    4.20 -  correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool"
    4.21 +  correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
    4.22    "correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
    4.23                           approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
    4.24                           pc < length ins \<and> length loc=length(snd sig)+maxl+1"
    4.25  
    4.26  
    4.27  consts
    4.28 - correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool"
    4.29 + correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool"
    4.30  primrec
    4.31  "correct_frames G hp phi rT0 sig0 [] = True"
    4.32  
    4.33 @@ -50,13 +50,13 @@
    4.34  
    4.35  
    4.36  constdefs
    4.37 - correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
    4.38 + correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
    4.39                    ("_,_ |-JVM _ [ok]"  [51,51] 50)
    4.40  "correct_state G phi == \<lambda>(xp,hp,frs).
    4.41     case xp of
    4.42 -     None => (case frs of
    4.43 -             [] => True
    4.44 -             | (f#fs) => G\<turnstile>h hp\<surd> \<and> preallocated hp \<and> 
    4.45 +     None \<Rightarrow> (case frs of
    4.46 +             [] \<Rightarrow> True
    4.47 +             | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and> preallocated hp \<and> 
    4.48        (let (stk,loc,C,sig,pc) = f
    4.49               in
    4.50                           \<exists>rT maxs maxl ins et s.
    4.51 @@ -65,11 +65,11 @@
    4.52                           phi C sig ! pc = Some s \<and>
    4.53         correct_frame G hp s maxl ins f \<and> 
    4.54               correct_frames G hp phi rT sig fs))
    4.55 -   | Some x => frs = []" 
    4.56 +   | Some x \<Rightarrow> frs = []" 
    4.57  
    4.58  
    4.59  syntax (xsymbols)
    4.60 - correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
    4.61 + correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
    4.62                    ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
    4.63  
    4.64  
    4.65 @@ -99,8 +99,8 @@
    4.66    by (cases T) (blast intro: conf_hext)+
    4.67  
    4.68  lemma approx_val_heap_update:
    4.69 -  "[| hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|] 
    4.70 -  ==> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
    4.71 +  "\<lbrakk> hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> 
    4.72 +  \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
    4.73    by (cases v, auto simp add: obj_ty_def conf_def)
    4.74  
    4.75  lemma approx_val_widen:
    4.76 @@ -228,8 +228,8 @@
    4.77  section {* oconf *}
    4.78  
    4.79  lemma oconf_field_update:
    4.80 -  "[|map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> |]
    4.81 -  ==> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
    4.82 +  "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
    4.83 +  \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
    4.84    by (simp add: oconf_def lconf_def)
    4.85  
    4.86  lemma oconf_newref:
    4.87 @@ -290,11 +290,11 @@
    4.88  
    4.89  lemma correct_frames_field_update [rule_format]:
    4.90    "\<forall>rT C sig. 
    4.91 -  correct_frames G hp phi rT sig frs --> 
    4.92 -  hp a = Some (C,fs) --> 
    4.93 -  map_of (fields (G, C)) fl = Some fd --> 
    4.94 +  correct_frames G hp phi rT sig frs \<longrightarrow> 
    4.95 +  hp a = Some (C,fs) \<longrightarrow> 
    4.96 +  map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
    4.97    G,hp\<turnstile>v::\<preceq>fd 
    4.98 -  --> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs";
    4.99 +  \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs";
   4.100  apply (induct frs)
   4.101   apply simp
   4.102  apply clarify
     5.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Sat Mar 02 12:09:23 2002 +0100
     5.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Sun Mar 03 16:59:08 2002 +0100
     5.3 @@ -13,7 +13,7 @@
     5.4  
     5.5  text {* Program counter of successor instructions: *}
     5.6  consts
     5.7 -  succs :: "instr => p_count => p_count list"
     5.8 +  succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list"
     5.9  primrec 
    5.10    "succs (Load idx) pc         = [pc+1]"
    5.11    "succs (Store idx) pc        = [pc+1]"
    5.12 @@ -36,7 +36,7 @@
    5.13  
    5.14  text "Effect of instruction on the state type:"
    5.15  consts 
    5.16 -eff' :: "instr \<times> jvm_prog \<times> state_type => state_type"
    5.17 +eff' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
    5.18  
    5.19  recdef eff' "{}"
    5.20  "eff' (Load idx,  G, (ST, LT))          = (ok_val (LT ! idx) # ST, LT)"
    5.21 @@ -84,7 +84,7 @@
    5.22    by (induct et) auto
    5.23  
    5.24  consts
    5.25 -  xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table => cname list" 
    5.26 +  xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table \<Rightarrow> cname list" 
    5.27  recdef xcpt_names "{}"
    5.28    "xcpt_names (Getfield F C, G, pc, et) = match G (Xcpt NullPointer) pc et" 
    5.29    "xcpt_names (Putfield F C, G, pc, et) = match G (Xcpt NullPointer) pc et" 
    5.30 @@ -104,7 +104,7 @@
    5.31    norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"
    5.32    "norm_eff i G == option_map (\<lambda>s. eff' (i,G,s))"
    5.33  
    5.34 -  eff :: "instr => jvm_prog => p_count => exception_table => state_type option => succ_type"
    5.35 +  eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> succ_type"
    5.36    "eff i G pc et s == (map (\<lambda>pc'. (pc',norm_eff i G s)) (succs i pc)) @ (xcpt_eff i G pc s et)"
    5.37  
    5.38  constdefs
    5.39 @@ -127,7 +127,7 @@
    5.40  
    5.41  text "Conditions under which eff is applicable:"
    5.42  consts
    5.43 -app' :: "instr \<times> jvm_prog \<times> p_count \<times> nat \<times> ty \<times> state_type => bool"
    5.44 +app' :: "instr \<times> jvm_prog \<times> p_count \<times> nat \<times> ty \<times> state_type \<Rightarrow> bool"
    5.45  
    5.46  recdef app' "{}"
    5.47  "app' (Load idx, G, pc, maxs, rT, s) = 
    5.48 @@ -180,17 +180,17 @@
    5.49    xcpt_app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> bool"
    5.50    "xcpt_app i G pc et \<equiv> \<forall>C\<in>set(xcpt_names (i,G,pc,et)). is_class G C"
    5.51  
    5.52 -  app :: "instr => jvm_prog => nat => ty => nat => exception_table => state_type option => bool"
    5.53 -  "app i G maxs rT pc et s == case s of None => True | Some t => app' (i,G,pc,maxs,rT,t) \<and> xcpt_app i G pc et"
    5.54 +  app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> bool"
    5.55 +  "app i G maxs rT pc et s == case s of None \<Rightarrow> True | Some t \<Rightarrow> app' (i,G,pc,maxs,rT,t) \<and> xcpt_app i G pc et"
    5.56  
    5.57  
    5.58 -lemma 1: "2 < length a ==> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
    5.59 +lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
    5.60  proof (cases a)
    5.61    fix x xs assume "a = x#xs" "2 < length a"
    5.62    thus ?thesis by - (cases xs, simp, cases "tl xs", auto)
    5.63  qed auto
    5.64  
    5.65 -lemma 2: "\<not>(2 < length a) ==> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
    5.66 +lemma 2: "\<not>(2 < length a) \<Longrightarrow> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
    5.67  proof -;
    5.68    assume "\<not>(2 < length a)"
    5.69    hence "length a < (Suc (Suc (Suc 0)))" by simp
    5.70 @@ -203,7 +203,7 @@
    5.71      hence "\<exists> l. x = [l]"  by - (cases x, auto)
    5.72    } note 0 = this
    5.73  
    5.74 -  have "length a = Suc (Suc 0) ==> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
    5.75 +  have "length a = Suc (Suc 0) \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
    5.76    with * show ?thesis by (auto dest: 0)
    5.77  qed
    5.78  
    5.79 @@ -337,7 +337,7 @@
    5.80  proof (cases (open) s)
    5.81    note list_all2_def [simp]
    5.82    case Pair
    5.83 -  have "?app (a,b) ==> ?P (a,b)"
    5.84 +  have "?app (a,b) \<Longrightarrow> ?P (a,b)"
    5.85    proof -
    5.86      assume app: "?app (a,b)"
    5.87      hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> 
     6.1 --- a/src/HOL/MicroJava/BV/EffectMono.thy	Sat Mar 02 12:09:23 2002 +0100
     6.2 +++ b/src/HOL/MicroJava/BV/EffectMono.thy	Sun Mar 03 16:59:08 2002 +0100
     6.3 @@ -14,7 +14,7 @@
     6.4  
     6.5  
     6.6  lemma sup_loc_some [rule_format]:
     6.7 -"\<forall>y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = OK t --> 
     6.8 +"\<forall>y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = OK t \<longrightarrow> 
     6.9    (\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
    6.10  proof (induct (open) ?P b)
    6.11    show "?P []" by simp
    6.12 @@ -41,9 +41,9 @@
    6.13     
    6.14  
    6.15  lemma all_widen_is_sup_loc:
    6.16 -"\<forall>b. length a = length b --> 
    6.17 +"\<forall>b. length a = length b \<longrightarrow> 
    6.18       (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map OK a) <=l (map OK b))" 
    6.19 - (is "\<forall>b. length a = length b --> ?Q a b" is "?P a")
    6.20 + (is "\<forall>b. length a = length b \<longrightarrow> ?Q a b" is "?P a")
    6.21  proof (induct "a")
    6.22    show "?P []" by simp
    6.23  
    6.24 @@ -60,7 +60,7 @@
    6.25   
    6.26  
    6.27  lemma append_length_n [rule_format]: 
    6.28 -"\<forall>n. n \<le> length x --> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
    6.29 +"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
    6.30  proof (induct (open) ?P x)
    6.31    show "?P []" by simp
    6.32  
    6.33 @@ -86,7 +86,7 @@
    6.34  qed
    6.35  
    6.36  lemma rev_append_cons:
    6.37 -"n < length x ==> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
    6.38 +"n < length x \<Longrightarrow> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
    6.39  proof -
    6.40    assume n: "n < length x"
    6.41    hence "n \<le> length x" by simp
    6.42 @@ -109,7 +109,7 @@
    6.43  lemmas [iff] = not_Err_eq
    6.44  
    6.45  lemma app_mono: 
    6.46 -"[|G \<turnstile> s <=' s'; app i G m rT pc et s'|] ==> app i G m rT pc et s"
    6.47 +"\<lbrakk>G \<turnstile> s <=' s'; app i G m rT pc et s'\<rbrakk> \<Longrightarrow> app i G m rT pc et s"
    6.48  proof -
    6.49  
    6.50    { fix s1 s2
    6.51 @@ -281,7 +281,7 @@
    6.52  lemmas [simp del] = split_paired_Ex
    6.53  
    6.54  lemma eff'_mono:
    6.55 -"[| app i G m rT pc et (Some s2); G \<turnstile> s1 <=s s2 |] ==>
    6.56 +"\<lbrakk> app i G m rT pc et (Some s2); G \<turnstile> s1 <=s s2 \<rbrakk> \<Longrightarrow>
    6.57    G \<turnstile> eff' (i,G,s1) <=s eff' (i,G,s2)"
    6.58  proof (cases s1, cases s2)
    6.59    fix a1 b1 a2 b2
     7.1 --- a/src/HOL/MicroJava/BV/Err.thy	Sat Mar 02 12:09:23 2002 +0100
     7.2 +++ b/src/HOL/MicroJava/BV/Err.thy	Sun Mar 03 16:59:08 2002 +0100
     7.3 @@ -12,48 +12,48 @@
     7.4  
     7.5  datatype 'a err = Err | OK 'a
     7.6  
     7.7 -types 'a ebinop = "'a => 'a => 'a err"
     7.8 +types 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
     7.9        'a esl =    "'a set * 'a ord * 'a ebinop"
    7.10  
    7.11  consts
    7.12 -  ok_val :: "'a err => 'a"
    7.13 +  ok_val :: "'a err \<Rightarrow> 'a"
    7.14  primrec
    7.15    "ok_val (OK x) = x"
    7.16  
    7.17  constdefs
    7.18 - lift :: "('a => 'b err) => ('a err => 'b err)"
    7.19 -"lift f e == case e of Err => Err | OK x => f x"
    7.20 + lift :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
    7.21 +"lift f e == case e of Err \<Rightarrow> Err | OK x \<Rightarrow> f x"
    7.22  
    7.23 - lift2 :: "('a => 'b => 'c err) => 'a err => 'b err => 'c err"
    7.24 + lift2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a err \<Rightarrow> 'b err \<Rightarrow> 'c err"
    7.25  "lift2 f e1 e2 ==
    7.26 - case e1 of Err  => Err
    7.27 -          | OK x => (case e2 of Err => Err | OK y => f x y)"
    7.28 + case e1 of Err  \<Rightarrow> Err
    7.29 +          | OK x \<Rightarrow> (case e2 of Err \<Rightarrow> Err | OK y \<Rightarrow> f x y)"
    7.30  
    7.31 - le :: "'a ord => 'a err ord"
    7.32 + le :: "'a ord \<Rightarrow> 'a err ord"
    7.33  "le r e1 e2 ==
    7.34 -        case e2 of Err => True |
    7.35 -                   OK y => (case e1 of Err => False | OK x => x <=_r y)"
    7.36 +        case e2 of Err \<Rightarrow> True |
    7.37 +                   OK y \<Rightarrow> (case e1 of Err \<Rightarrow> False | OK x \<Rightarrow> x <=_r y)"
    7.38  
    7.39 - sup :: "('a => 'b => 'c) => ('a err => 'b err => 'c err)"
    7.40 + sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> 'c err)"
    7.41  "sup f == lift2(%x y. OK(x +_f y))"
    7.42  
    7.43 - err :: "'a set => 'a err set"
    7.44 + err :: "'a set \<Rightarrow> 'a err set"
    7.45  "err A == insert Err {x . ? y:A. x = OK y}"
    7.46  
    7.47 - esl :: "'a sl => 'a esl"
    7.48 + esl :: "'a sl \<Rightarrow> 'a esl"
    7.49  "esl == %(A,r,f). (A,r, %x y. OK(f x y))"
    7.50  
    7.51 - sl :: "'a esl => 'a err sl"
    7.52 + sl :: "'a esl \<Rightarrow> 'a err sl"
    7.53  "sl == %(A,r,f). (err A, le r, lift2 f)"
    7.54  
    7.55  syntax
    7.56 - err_semilat :: "'a esl => bool"
    7.57 + err_semilat :: "'a esl \<Rightarrow> bool"
    7.58  translations
    7.59  "err_semilat L" == "semilat(Err.sl L)"
    7.60  
    7.61  
    7.62  consts
    7.63 -  strict  :: "('a => 'b err) => ('a err => 'b err)"
    7.64 +  strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
    7.65  primrec
    7.66    "strict f Err    = Err"
    7.67    "strict f (OK x) = f x"
    7.68 @@ -75,20 +75,20 @@
    7.69    by (simp add: lesub_def)
    7.70  
    7.71  lemma le_err_refl:
    7.72 -  "!x. x <=_r x ==> e <=_(Err.le r) e"
    7.73 +  "!x. x <=_r x \<Longrightarrow> e <=_(Err.le r) e"
    7.74  apply (unfold lesub_def Err.le_def)
    7.75  apply (simp split: err.split)
    7.76  done 
    7.77  
    7.78  lemma le_err_trans [rule_format]:
    7.79 -  "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e3 --> e1 <=_(le r) e3"
    7.80 +  "order r \<Longrightarrow> e1 <=_(le r) e2 \<longrightarrow> e2 <=_(le r) e3 \<longrightarrow> e1 <=_(le r) e3"
    7.81  apply (unfold unfold_lesub_err le_def)
    7.82  apply (simp split: err.split)
    7.83  apply (blast intro: order_trans)
    7.84  done
    7.85  
    7.86  lemma le_err_antisym [rule_format]:
    7.87 -  "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e1 --> e1=e2"
    7.88 +  "order r \<Longrightarrow> e1 <=_(le r) e2 \<longrightarrow> e2 <=_(le r) e1 \<longrightarrow> e1=e2"
    7.89  apply (unfold unfold_lesub_err le_def)
    7.90  apply (simp split: err.split)
    7.91  apply (blast intro: order_antisym)
    7.92 @@ -136,20 +136,20 @@
    7.93    by (simp add: lesssub_def lesub_def le_def split: err.split)
    7.94  
    7.95  lemma semilat_errI:
    7.96 -  "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
    7.97 +  "semilat(A,r,f) \<Longrightarrow> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
    7.98  apply (unfold semilat_Def closed_def plussub_def lesub_def 
    7.99                lift2_def Err.le_def err_def)
   7.100  apply (simp split: err.split)
   7.101  done
   7.102  
   7.103  lemma err_semilat_eslI: 
   7.104 -  "!!L. semilat L ==> err_semilat(esl L)"
   7.105 +  "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
   7.106  apply (unfold sl_def esl_def)
   7.107  apply (simp (no_asm_simp) only: split_tupled_all)
   7.108  apply (simp add: semilat_errI)
   7.109  done
   7.110  
   7.111 -lemma acc_err [simp, intro!]:  "acc r ==> acc(le r)"
   7.112 +lemma acc_err [simp, intro!]:  "acc r \<Longrightarrow> acc(le r)"
   7.113  apply (unfold acc_def lesub_def le_def lesssub_def)
   7.114  apply (simp add: wf_eq_minimal split: err.split)
   7.115  apply clarify
   7.116 @@ -170,7 +170,7 @@
   7.117  section {* lift *}
   7.118  
   7.119  lemma lift_in_errI:
   7.120 -  "[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S"
   7.121 +  "\<lbrakk> e : err S; !x:S. e = OK x \<longrightarrow> f x : err S \<rbrakk> \<Longrightarrow> lift f e : err S"
   7.122  apply (unfold lift_def)
   7.123  apply (simp split: err.split)
   7.124  apply blast
   7.125 @@ -221,42 +221,42 @@
   7.126  section {* semilat (err A) (le r) f *}
   7.127  
   7.128  lemma semilat_le_err_Err_plus [simp]:
   7.129 -  "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err"
   7.130 +  "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> Err +_f x = Err"
   7.131    by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
   7.132  
   7.133  lemma semilat_le_err_plus_Err [simp]:
   7.134 -  "[| x: err A; semilat(err A, le r, f) |] ==> x +_f Err = Err"
   7.135 +  "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> x +_f Err = Err"
   7.136    by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
   7.137  
   7.138  lemma semilat_le_err_OK1:
   7.139 -  "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] 
   7.140 -  ==> x <=_r z";
   7.141 +  "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk> 
   7.142 +  \<Longrightarrow> x <=_r z";
   7.143  apply (rule OK_le_err_OK [THEN iffD1])
   7.144  apply (erule subst)
   7.145  apply simp
   7.146  done 
   7.147  
   7.148  lemma semilat_le_err_OK2:
   7.149 -  "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] 
   7.150 -  ==> y <=_r z"
   7.151 +  "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk> 
   7.152 +  \<Longrightarrow> y <=_r z"
   7.153  apply (rule OK_le_err_OK [THEN iffD1])
   7.154  apply (erule subst)
   7.155  apply simp
   7.156  done 
   7.157  
   7.158  lemma eq_order_le:
   7.159 -  "[| x=y; order r |] ==> x <=_r y"
   7.160 +  "\<lbrakk> x=y; order r \<rbrakk> \<Longrightarrow> x <=_r y"
   7.161  apply (unfold order_def)
   7.162  apply blast
   7.163  done
   7.164  
   7.165  lemma OK_plus_OK_eq_Err_conv [simp]:
   7.166 -  "[| x:A; y:A; semilat(err A, le r, fe) |] ==> 
   7.167 +  "\<lbrakk> x:A; y:A; semilat(err A, le r, fe) \<rbrakk> \<Longrightarrow> 
   7.168    ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
   7.169  proof -
   7.170 -  have plus_le_conv3: "!!A x y z f r. 
   7.171 -    [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |] 
   7.172 -    ==> x <=_r z \<and> y <=_r z"
   7.173 +  have plus_le_conv3: "\<And>A x y z f r. 
   7.174 +    \<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk> 
   7.175 +    \<Longrightarrow> x <=_r z \<and> y <=_r z"
   7.176      by (rule plus_le_conv [THEN iffD1])
   7.177    case rule_context
   7.178    thus ?thesis
   7.179 @@ -287,13 +287,13 @@
   7.180  
   7.181  (* FIXME? *)
   7.182  lemma all_bex_swap_lemma [iff]:
   7.183 -  "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))"
   7.184 +  "(!x. (? y:A. x = f y) \<longrightarrow> P x) = (!y:A. P(f y))"
   7.185    by blast
   7.186  
   7.187  lemma closed_err_Union_lift2I: 
   7.188 -  "[| !A:AS. closed (err A) (lift2 f); AS ~= {}; 
   7.189 -      !A:AS.!B:AS. A~=B --> (!a:A.!b:B. a +_f b = Err) |] 
   7.190 -  ==> closed (err(Union AS)) (lift2 f)"
   7.191 +  "\<lbrakk> !A:AS. closed (err A) (lift2 f); AS ~= {}; 
   7.192 +      !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. a +_f b = Err) \<rbrakk> 
   7.193 +  \<Longrightarrow> closed (err(Union AS)) (lift2 f)"
   7.194  apply (unfold closed_def err_def)
   7.195  apply simp
   7.196  apply clarify
   7.197 @@ -307,9 +307,9 @@
   7.198    which may not hold 
   7.199  *}
   7.200  lemma err_semilat_UnionI:
   7.201 -  "[| !A:AS. err_semilat(A, r, f); AS ~= {}; 
   7.202 -      !A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |] 
   7.203 -  ==> err_semilat(Union AS, r, f)"
   7.204 +  "\<lbrakk> !A:AS. err_semilat(A, r, f); AS ~= {}; 
   7.205 +      !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) \<rbrakk> 
   7.206 +  \<Longrightarrow> err_semilat(Union AS, r, f)"
   7.207  apply (unfold semilat_def sl_def)
   7.208  apply (simp add: closed_err_Union_lift2I)
   7.209  apply (rule conjI)
     8.1 --- a/src/HOL/MicroJava/BV/JType.thy	Sat Mar 02 12:09:23 2002 +0100
     8.2 +++ b/src/HOL/MicroJava/BV/JType.thy	Sun Mar 03 16:59:08 2002 +0100
     8.3 @@ -17,31 +17,31 @@
     8.4    by (unfold super_def) (auto dest: subcls1D)
     8.5  
     8.6  constdefs
     8.7 -  is_ref :: "ty => bool"
     8.8 -  "is_ref T == case T of PrimT t => False | RefT r => True"
     8.9 +  is_ref :: "ty \<Rightarrow> bool"
    8.10 +  "is_ref T == case T of PrimT t \<Rightarrow> False | RefT r \<Rightarrow> True"
    8.11  
    8.12 -  sup :: "'c prog => ty => ty => ty err"
    8.13 +  sup :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty err"
    8.14    "sup G T1 T2 ==
    8.15 -  case T1 of PrimT P1 => (case T2 of PrimT P2 => 
    8.16 -                         (if P1 = P2 then OK (PrimT P1) else Err) | RefT R => Err)
    8.17 -           | RefT R1 => (case T2 of PrimT P => Err | RefT R2 => 
    8.18 -  (case R1 of NullT => (case R2 of NullT => OK NT | ClassT C => OK (Class C))
    8.19 -            | ClassT C => (case R2 of NullT => OK (Class C) 
    8.20 -                           | ClassT D => OK (Class (exec_lub (subcls1 G) (super G) C D)))))"
    8.21 +  case T1 of PrimT P1 \<Rightarrow> (case T2 of PrimT P2 \<Rightarrow> 
    8.22 +                         (if P1 = P2 then OK (PrimT P1) else Err) | RefT R \<Rightarrow> Err)
    8.23 +           | RefT R1 \<Rightarrow> (case T2 of PrimT P \<Rightarrow> Err | RefT R2 \<Rightarrow> 
    8.24 +  (case R1 of NullT \<Rightarrow> (case R2 of NullT \<Rightarrow> OK NT | ClassT C \<Rightarrow> OK (Class C))
    8.25 +            | ClassT C \<Rightarrow> (case R2 of NullT \<Rightarrow> OK (Class C) 
    8.26 +                           | ClassT D \<Rightarrow> OK (Class (exec_lub (subcls1 G) (super G) C D)))))"
    8.27  
    8.28 -  subtype :: "'c prog => ty => ty => bool"
    8.29 +  subtype :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
    8.30    "subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2"
    8.31  
    8.32 -  is_ty :: "'c prog => ty => bool"
    8.33 -  "is_ty G T == case T of PrimT P => True | RefT R =>
    8.34 -               (case R of NullT => True | ClassT C => (C,Object):(subcls1 G)^*)"
    8.35 +  is_ty :: "'c prog \<Rightarrow> ty \<Rightarrow> bool"
    8.36 +  "is_ty G T == case T of PrimT P \<Rightarrow> True | RefT R \<Rightarrow>
    8.37 +               (case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (C,Object):(subcls1 G)^*)"
    8.38  
    8.39  
    8.40  translations
    8.41    "types G" == "Collect (is_type G)"
    8.42  
    8.43  constdefs
    8.44 -  esl :: "'c prog => ty esl"
    8.45 +  esl :: "'c prog \<Rightarrow> ty esl"
    8.46    "esl G == (types G, subtype G, sup G)"
    8.47  
    8.48  lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
    8.49 @@ -51,12 +51,12 @@
    8.50    by (auto elim: widen.elims)
    8.51  
    8.52  lemma is_tyI:
    8.53 -  "[| is_type G T; wf_prog wf_mb G |] ==> is_ty G T"
    8.54 +  "\<lbrakk> is_type G T; wf_prog wf_mb G \<rbrakk> \<Longrightarrow> is_ty G T"
    8.55    by (auto simp add: is_ty_def intro: subcls_C_Object 
    8.56             split: ty.splits ref_ty.splits)
    8.57  
    8.58  lemma is_type_conv: 
    8.59 -  "wf_prog wf_mb G ==> is_type G T = is_ty G T"
    8.60 +  "wf_prog wf_mb G \<Longrightarrow> is_type G T = is_ty G T"
    8.61  proof
    8.62    assume "is_type G T" "wf_prog wf_mb G" 
    8.63    thus "is_ty G T"
    8.64 @@ -86,7 +86,7 @@
    8.65  qed
    8.66  
    8.67  lemma order_widen:
    8.68 -  "acyclic (subcls1 G) ==> order (subtype G)"
    8.69 +  "acyclic (subcls1 G) \<Longrightarrow> order (subtype G)"
    8.70    apply (unfold order_def lesub_def subtype_def)
    8.71    apply (auto intro: widen_trans)
    8.72    apply (case_tac x)
    8.73 @@ -106,7 +106,7 @@
    8.74    done
    8.75  
    8.76  lemma wf_converse_subcls1_impl_acc_subtype:
    8.77 -  "wf ((subcls1 G)^-1) ==> acc (subtype G)"
    8.78 +  "wf ((subcls1 G)^-1) \<Longrightarrow> acc (subtype G)"
    8.79  apply (unfold acc_def lesssub_def)
    8.80  apply (drule_tac p = "(subcls1 G)^-1 - Id" in wf_subset)
    8.81   apply blast
    8.82 @@ -159,8 +159,8 @@
    8.83  done 
    8.84  
    8.85  lemma closed_err_types:
    8.86 -  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] 
    8.87 -  ==> closed (err (types G)) (lift2 (sup G))"
    8.88 +  "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk> 
    8.89 +  \<Longrightarrow> closed (err (types G)) (lift2 (sup G))"
    8.90    apply (unfold closed_def plussub_def lift2_def sup_def)
    8.91    apply (auto split: err.split)
    8.92    apply (drule is_tyI, assumption)
    8.93 @@ -171,9 +171,9 @@
    8.94  
    8.95  
    8.96  lemma sup_subtype_greater:
    8.97 -  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
    8.98 -      is_type G t1; is_type G t2; sup G t1 t2 = OK s |] 
    8.99 -  ==> subtype G t1 s \<and> subtype G t2 s"
   8.100 +  "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
   8.101 +      is_type G t1; is_type G t2; sup G t1 t2 = OK s \<rbrakk> 
   8.102 +  \<Longrightarrow> subtype G t1 s \<and> subtype G t2 s"
   8.103  proof -
   8.104    assume wf_prog:       "wf_prog wf_mb G"
   8.105    assume single_valued: "single_valued (subcls1 G)" 
   8.106 @@ -210,10 +210,10 @@
   8.107  qed
   8.108  
   8.109  lemma sup_subtype_smallest:
   8.110 -  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
   8.111 +  "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
   8.112        is_type G a; is_type G b; is_type G c; 
   8.113 -      subtype G a c; subtype G b c; sup G a b = OK d |]
   8.114 -  ==> subtype G d c"
   8.115 +      subtype G a c; subtype G b c; sup G a b = OK d \<rbrakk>
   8.116 +  \<Longrightarrow> subtype G d c"
   8.117  proof -
   8.118    assume wf_prog:       "wf_prog wf_mb G"
   8.119    assume single_valued: "single_valued (subcls1 G)" 
   8.120 @@ -244,7 +244,7 @@
   8.121    } note this [intro]
   8.122  
   8.123    have [dest!]:
   8.124 -    "!!C T. G \<turnstile> Class C \<preceq> T ==> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
   8.125 +    "\<And>C T. G \<turnstile> Class C \<preceq> T \<Longrightarrow> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
   8.126      by (frule widen_Class, auto)
   8.127  
   8.128    assume "is_type G a" "is_type G b" "is_type G c"
   8.129 @@ -255,13 +255,13 @@
   8.130  qed
   8.131  
   8.132  lemma sup_exists:
   8.133 -  "[| subtype G a c; subtype G b c; sup G a b = Err |] ==> False"
   8.134 +  "\<lbrakk> subtype G a c; subtype G b c; sup G a b = Err \<rbrakk> \<Longrightarrow> False"
   8.135    by (auto simp add: PrimT_PrimT PrimT_PrimT2 sup_def subtype_def
   8.136             split: ty.splits ref_ty.splits)
   8.137  
   8.138  lemma err_semilat_JType_esl_lemma:
   8.139 -  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] 
   8.140 -  ==> err_semilat (esl G)"
   8.141 +  "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk> 
   8.142 +  \<Longrightarrow> err_semilat (esl G)"
   8.143  proof -
   8.144    assume wf_prog:   "wf_prog wf_mb G"
   8.145    assume single_valued: "single_valued (subcls1 G)" 
   8.146 @@ -297,12 +297,12 @@
   8.147  qed
   8.148  
   8.149  lemma single_valued_subcls1:
   8.150 -  "wf_prog wf_mb G ==> single_valued (subcls1 G)"
   8.151 +  "wf_prog wf_mb G \<Longrightarrow> single_valued (subcls1 G)"
   8.152    by (auto simp add: wf_prog_def unique_def single_valued_def
   8.153      intro: subcls1I elim!: subcls1.elims)
   8.154  
   8.155  theorem err_semilat_JType_esl:
   8.156 -  "wf_prog wf_mb G ==> err_semilat (esl G)"
   8.157 +  "wf_prog wf_mb G \<Longrightarrow> err_semilat (esl G)"
   8.158    by (frule acyclic_subcls1, frule single_valued_subcls1, rule err_semilat_JType_esl_lemma)
   8.159  
   8.160  end
     9.1 --- a/src/HOL/MicroJava/BV/JVM.thy	Sat Mar 02 12:09:23 2002 +0100
     9.2 +++ b/src/HOL/MicroJava/BV/JVM.thy	Sun Mar 03 16:59:08 2002 +0100
     9.3 @@ -14,8 +14,8 @@
     9.4    "exec G maxs rT et bs == 
     9.5    err_step (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
     9.6  
     9.7 -  kiljvm :: "jvm_prog => nat => nat => ty => exception_table => 
     9.8 -             instr list => state list => state list"
     9.9 +  kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
    9.10 +             instr list \<Rightarrow> state list \<Rightarrow> state list"
    9.11    "kiljvm G maxs maxr rT et bs ==
    9.12    kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)"
    9.13  
    9.14 @@ -28,7 +28,7 @@
    9.15          result = kiljvm G mxs (1+size pTs+mxl) rT et ins start
    9.16      in \<forall>n < size ins. result!n \<noteq> Err)"
    9.17  
    9.18 -  wt_jvm_prog_kildall :: "jvm_prog => bool"
    9.19 +  wt_jvm_prog_kildall :: "jvm_prog \<Rightarrow> bool"
    9.20    "wt_jvm_prog_kildall G ==
    9.21    wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"
    9.22  
    9.23 @@ -77,7 +77,7 @@
    9.24  
    9.25  
    9.26  theorem exec_pres_type:
    9.27 -  "wf_prog wf_mb S ==> 
    9.28 +  "wf_prog wf_mb S \<Longrightarrow> 
    9.29    pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
    9.30    apply (unfold exec_def JVM_states_unfold)
    9.31    apply (rule pres_type_lift)
    9.32 @@ -243,7 +243,7 @@
    9.33    by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
    9.34  
    9.35  theorem exec_mono:
    9.36 -  "wf_prog wf_mb G ==>
    9.37 +  "wf_prog wf_mb G \<Longrightarrow>
    9.38    mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"  
    9.39    apply (unfold exec_def JVM_le_unfold JVM_states_unfold)  
    9.40    apply (rule mono_lift)
    9.41 @@ -257,7 +257,7 @@
    9.42    done
    9.43  
    9.44  theorem semilat_JVM_slI:
    9.45 -  "wf_prog wf_mb G ==> semilat (JVMType.sl G maxs maxr)"
    9.46 +  "wf_prog wf_mb G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
    9.47    apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
    9.48    apply (rule semilat_opt)
    9.49    apply (rule err_semilat_Product_esl)
    9.50 @@ -275,7 +275,7 @@
    9.51  
    9.52  
    9.53  theorem is_bcv_kiljvm:
    9.54 -  "[| wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) |] ==> 
    9.55 +  "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow> 
    9.56        is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
    9.57               (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
    9.58    apply (unfold kiljvm_def sl_triple_conv)
    9.59 @@ -293,9 +293,9 @@
    9.60  
    9.61  
    9.62  theorem wt_kil_correct:
    9.63 -  "[| wt_kil G C pTs rT maxs mxl et bs; wf_prog wf_mb G; 
    9.64 -      is_class G C; \<forall>x \<in> set pTs. is_type G x |]
    9.65 -  ==> \<exists>phi. wt_method G C pTs rT maxs mxl bs et phi"
    9.66 +  "\<lbrakk> wt_kil G C pTs rT maxs mxl et bs; wf_prog wf_mb G; 
    9.67 +      is_class G C; \<forall>x \<in> set pTs. is_type G x \<rbrakk>
    9.68 +  \<Longrightarrow> \<exists>phi. wt_method G C pTs rT maxs mxl bs et phi"
    9.69  proof -
    9.70    let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
    9.71                  #(replicate (size bs - 1) (OK None))"
    9.72 @@ -386,10 +386,10 @@
    9.73  
    9.74  
    9.75  theorem wt_kil_complete:
    9.76 -  "[| wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G; 
    9.77 +  "\<lbrakk> wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G; 
    9.78        length phi = length bs; is_class G C; \<forall>x \<in> set pTs. is_type G x;
    9.79 -      map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl)) |]
    9.80 -  ==> wt_kil G C pTs rT maxs mxl et bs"
    9.81 +      map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl)) \<rbrakk>
    9.82 +  \<Longrightarrow> wt_kil G C pTs rT maxs mxl et bs"
    9.83  proof -
    9.84    assume wf: "wf_prog wf_mb G"  
    9.85    assume isclass: "is_class G C"
    9.86 @@ -490,12 +490,12 @@
    9.87          have "JVMType.le G maxs ?maxr (OK None) (?phi!n)"
    9.88            by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def 
    9.89              split: err.splits)        
    9.90 -        hence "[| n = Suc n'; n < length ?start |] 
    9.91 -          ==> JVMType.le G maxs ?maxr (?start!n) (?phi!n)"
    9.92 +        hence "\<lbrakk> n = Suc n'; n < length ?start \<rbrakk> 
    9.93 +          \<Longrightarrow> JVMType.le G maxs ?maxr (?start!n) (?phi!n)"
    9.94            by simp
    9.95        }
    9.96        ultimately
    9.97 -      have "n < length ?start ==> (?start!n) <=_(JVMType.le G maxs ?maxr) (?phi!n)"
    9.98 +      have "n < length ?start \<Longrightarrow> (?start!n) <=_(JVMType.le G maxs ?maxr) (?phi!n)"
    9.99          by (unfold lesub_def) (cases n, blast+)
   9.100      } 
   9.101      ultimately show ?thesis by (rule le_listI)
   9.102 @@ -540,9 +540,9 @@
   9.103    programs without problems:
   9.104  *}
   9.105  lemma is_type_pTs:
   9.106 -  "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls; 
   9.107 -      t \<in> set (snd sig) |]
   9.108 -  ==> is_type G t"
   9.109 +  "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls; 
   9.110 +      t \<in> set (snd sig) \<rbrakk>
   9.111 +  \<Longrightarrow> is_type G t"
   9.112  proof -
   9.113    assume "wf_prog wf_mb G" 
   9.114           "(C,S,fs,mdecls) \<in> set G"
   9.115 @@ -559,7 +559,7 @@
   9.116  
   9.117  
   9.118  theorem jvm_kildall_correct:
   9.119 -  "wt_jvm_prog_kildall G ==> \<exists>Phi. wt_jvm_prog G Phi"
   9.120 +  "wt_jvm_prog_kildall G \<Longrightarrow> \<exists>Phi. wt_jvm_prog G Phi"
   9.121  proof -  
   9.122    assume wtk: "wt_jvm_prog_kildall G"
   9.123  
    10.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Sat Mar 02 12:09:23 2002 +0100
    10.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Sun Mar 03 16:59:08 2002 +0100
    10.3 @@ -15,58 +15,58 @@
    10.4    state_type   = "opstack_type \<times> locvars_type"
    10.5    state        = "state_type option err"    -- "for Kildall"
    10.6    method_type  = "state_type option list"   -- "for BVSpec"
    10.7 -  class_type   = "sig => method_type"
    10.8 -  prog_type    = "cname => class_type"
    10.9 +  class_type   = "sig \<Rightarrow> method_type"
   10.10 +  prog_type    = "cname \<Rightarrow> class_type"
   10.11  
   10.12  
   10.13  constdefs
   10.14 -  stk_esl :: "'c prog => nat => ty list esl"
   10.15 +  stk_esl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty list esl"
   10.16    "stk_esl S maxs == upto_esl maxs (JType.esl S)"
   10.17  
   10.18 -  reg_sl :: "'c prog => nat => ty err list sl"
   10.19 +  reg_sl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty err list sl"
   10.20    "reg_sl S maxr == Listn.sl maxr (Err.sl (JType.esl S))"
   10.21  
   10.22 -  sl :: "'c prog => nat => nat => state sl"
   10.23 +  sl :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state sl"
   10.24    "sl S maxs maxr ==
   10.25    Err.sl(Opt.esl(Product.esl (stk_esl S maxs) (Err.esl(reg_sl S maxr))))"
   10.26  
   10.27  constdefs
   10.28 -  states :: "'c prog => nat => nat => state set"
   10.29 +  states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state set"
   10.30    "states S maxs maxr == fst(sl S maxs maxr)"
   10.31  
   10.32 -  le :: "'c prog => nat => nat => state ord"
   10.33 +  le :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state ord"
   10.34    "le S maxs maxr == fst(snd(sl S maxs maxr))"
   10.35  
   10.36 -  sup :: "'c prog => nat => nat => state binop"
   10.37 +  sup :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state binop"
   10.38    "sup S maxs maxr == snd(snd(sl S maxs maxr))"
   10.39  
   10.40  
   10.41  constdefs
   10.42 -  sup_ty_opt :: "['code prog,ty err,ty err] => bool" 
   10.43 +  sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool" 
   10.44                   ("_ |- _ <=o _" [71,71] 70)
   10.45    "sup_ty_opt G == Err.le (subtype G)"
   10.46  
   10.47 -  sup_loc :: "['code prog,locvars_type,locvars_type] => bool" 
   10.48 +  sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
   10.49                ("_ |- _ <=l _"  [71,71] 70)
   10.50    "sup_loc G == Listn.le (sup_ty_opt G)"
   10.51  
   10.52 -  sup_state :: "['code prog,state_type,state_type] => bool"   
   10.53 +  sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"   
   10.54                 ("_ |- _ <=s _"  [71,71] 70)
   10.55    "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
   10.56  
   10.57 -  sup_state_opt :: "['code prog,state_type option,state_type option] => bool" 
   10.58 +  sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool" 
   10.59                     ("_ |- _ <=' _"  [71,71] 70)
   10.60    "sup_state_opt G == Opt.le (sup_state G)"
   10.61  
   10.62  
   10.63  syntax (xsymbols)
   10.64 -  sup_ty_opt    :: "['code prog,ty err,ty err] => bool" 
   10.65 +  sup_ty_opt    :: "['code prog,ty err,ty err] \<Rightarrow> bool" 
   10.66                     ("_ \<turnstile> _ <=o _" [71,71] 70)
   10.67 -  sup_loc       :: "['code prog,locvars_type,locvars_type] => bool" 
   10.68 +  sup_loc       :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
   10.69                     ("_ \<turnstile> _ <=l _" [71,71] 70)
   10.70 -  sup_state     :: "['code prog,state_type,state_type] => bool" 
   10.71 +  sup_state     :: "['code prog,state_type,state_type] \<Rightarrow> bool" 
   10.72                     ("_ \<turnstile> _ <=s _" [71,71] 70)
   10.73 -  sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
   10.74 +  sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
   10.75                     ("_ \<turnstile> _ <=' _" [71,71] 70)
   10.76                     
   10.77  
   10.78 @@ -98,7 +98,7 @@
   10.79               sup_ty_opt_def JVM_le_unfold) simp
   10.80  
   10.81  lemma zip_map [rule_format]:
   10.82 -  "\<forall>a. length a = length b --> 
   10.83 +  "\<forall>a. length a = length b \<longrightarrow> 
   10.84    zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)"
   10.85    apply (induct b) 
   10.86     apply simp
   10.87 @@ -188,11 +188,11 @@
   10.88    by (simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def)
   10.89  
   10.90  theorem sup_ty_opt_OK:
   10.91 -  "G \<turnstile> a <=o (OK b) ==> \<exists> x. a = OK x"
   10.92 +  "G \<turnstile> a <=o (OK b) \<Longrightarrow> \<exists> x. a = OK x"
   10.93    by (clarsimp simp add: sup_ty_opt_def Err.le_def split: err.splits)
   10.94  
   10.95  lemma widen_PrimT_conv1 [simp]:
   10.96 -  "[| G \<turnstile> S \<preceq> T; S = PrimT x|] ==> T = PrimT x"
   10.97 +  "\<lbrakk> G \<turnstile> S \<preceq> T; S = PrimT x\<rbrakk> \<Longrightarrow> T = PrimT x"
   10.98    by (auto elim: widen.elims)
   10.99  
  10.100  theorem sup_PTS_eq:
  10.101 @@ -214,20 +214,20 @@
  10.102  
  10.103  
  10.104  theorem sup_loc_length:
  10.105 -  "G \<turnstile> a <=l b ==> length a = length b"
  10.106 +  "G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
  10.107  proof -
  10.108    assume G: "G \<turnstile> a <=l b"
  10.109 -  have "\<forall>b. (G \<turnstile> a <=l b) --> length a = length b"
  10.110 +  have "\<forall>b. (G \<turnstile> a <=l b) \<longrightarrow> length a = length b"
  10.111      by (induct a, auto)
  10.112    with G
  10.113    show ?thesis by blast
  10.114  qed
  10.115  
  10.116  theorem sup_loc_nth:
  10.117 -  "[| G \<turnstile> a <=l b; n < length a |] ==> G \<turnstile> (a!n) <=o (b!n)"
  10.118 +  "\<lbrakk> G \<turnstile> a <=l b; n < length a \<rbrakk> \<Longrightarrow> G \<turnstile> (a!n) <=o (b!n)"
  10.119  proof -
  10.120    assume a: "G \<turnstile> a <=l b" "n < length a"
  10.121 -  have "\<forall> n b. (G \<turnstile> a <=l b) --> n < length a --> (G \<turnstile> (a!n) <=o (b!n))"
  10.122 +  have "\<forall> n b. (G \<turnstile> a <=l b) \<longrightarrow> n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))"
  10.123      (is "?P a")
  10.124    proof (induct a)
  10.125      show "?P []" by simp
  10.126 @@ -248,8 +248,8 @@
  10.127  qed
  10.128  
  10.129  theorem all_nth_sup_loc:
  10.130 -  "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n))) 
  10.131 -  --> (G \<turnstile> a <=l b)" (is "?P a")
  10.132 +  "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) 
  10.133 +  \<longrightarrow> (G \<turnstile> a <=l b)" (is "?P a")
  10.134  proof (induct a)
  10.135    show "?P []" by simp
  10.136  
  10.137 @@ -258,14 +258,14 @@
  10.138    show "?P (l#ls)"
  10.139    proof (intro strip)
  10.140      fix b
  10.141 -    assume f: "\<forall>n. n < length (l # ls) --> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
  10.142 +    assume f: "\<forall>n. n < length (l # ls) \<longrightarrow> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
  10.143      assume l: "length (l#ls) = length b"
  10.144      
  10.145      then obtain b' bs where b: "b = b'#bs"
  10.146        by - (cases b, simp, simp add: neq_Nil_conv, rule that)
  10.147  
  10.148      with f
  10.149 -    have "\<forall>n. n < length ls --> (G \<turnstile> (ls!n) <=o (bs!n))"
  10.150 +    have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
  10.151        by auto
  10.152  
  10.153      with f b l IH
  10.154 @@ -276,12 +276,12 @@
  10.155  
  10.156  
  10.157  theorem sup_loc_append:
  10.158 -  "length a = length b ==> 
  10.159 +  "length a = length b \<Longrightarrow> 
  10.160     (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
  10.161  proof -
  10.162    assume l: "length a = length b"
  10.163  
  10.164 -  have "\<forall>b. length a = length b --> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
  10.165 +  have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
  10.166              (G \<turnstile> x <=l y))" (is "?P a") 
  10.167    proof (induct a)
  10.168      show "?P []" by simp
  10.169 @@ -347,7 +347,7 @@
  10.170  
  10.171  
  10.172  theorem sup_loc_update [rule_format]:
  10.173 -  "\<forall> n y. (G \<turnstile> a <=o b) --> n < length y --> (G \<turnstile> x <=l y) --> 
  10.174 +  "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
  10.175            (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
  10.176  proof (induct x)
  10.177    show "?P []" by simp
  10.178 @@ -365,17 +365,17 @@
  10.179  
  10.180  
  10.181  theorem sup_state_length [simp]:
  10.182 -  "G \<turnstile> s2 <=s s1 ==> 
  10.183 +  "G \<turnstile> s2 <=s s1 \<Longrightarrow> 
  10.184     length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
  10.185    by (auto dest: sup_loc_length simp add: sup_state_def stk_convert lesub_def Product.le_def);
  10.186  
  10.187  theorem sup_state_append_snd:
  10.188 -  "length a = length b ==> 
  10.189 +  "length a = length b \<Longrightarrow> 
  10.190    (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
  10.191    by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append)
  10.192  
  10.193  theorem sup_state_append_fst:
  10.194 -  "length a = length b ==> 
  10.195 +  "length a = length b \<Longrightarrow> 
  10.196    (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
  10.197    by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append)
  10.198  
  10.199 @@ -390,13 +390,13 @@
  10.200    by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def map_eq_Cons sup_loc_Cons2)
  10.201  
  10.202  theorem sup_state_ignore_fst:  
  10.203 -  "G \<turnstile> (a, x) <=s (b, y) ==> G \<turnstile> (c, x) <=s (c, y)"
  10.204 +  "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
  10.205    by (simp add: sup_state_def lesub_def Product.le_def)
  10.206  
  10.207  theorem sup_state_rev_fst:
  10.208    "(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))"
  10.209  proof -
  10.210 -  have m: "!!f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
  10.211 +  have m: "\<And>f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
  10.212    show ?thesis by (simp add: m sup_state_def stk_convert lesub_def Product.le_def)
  10.213  qed
  10.214    
  10.215 @@ -423,17 +423,17 @@
  10.216  
  10.217  
  10.218  theorem sup_ty_opt_trans [trans]:
  10.219 -  "[|G \<turnstile> a <=o b; G \<turnstile> b <=o c|] ==> G \<turnstile> a <=o c"
  10.220 +  "\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
  10.221    by (auto intro: widen_trans 
  10.222             simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def 
  10.223             split: err.splits)
  10.224  
  10.225  theorem sup_loc_trans [trans]:
  10.226 -  "[|G \<turnstile> a <=l b; G \<turnstile> b <=l c|] ==> G \<turnstile> a <=l c"
  10.227 +  "\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
  10.228  proof -
  10.229    assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
  10.230   
  10.231 -  hence "\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (c!n))"
  10.232 +  hence "\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (c!n))"
  10.233    proof (intro strip)
  10.234      fix n 
  10.235      assume n: "n < length a"
  10.236 @@ -442,7 +442,7 @@
  10.237        by - (rule sup_loc_nth)
  10.238      also 
  10.239      from n G
  10.240 -    have "G \<turnstile> ... <=o (c!n)"
  10.241 +    have "G \<turnstile> \<dots> <=o (c!n)"
  10.242        by - (rule sup_loc_nth, auto dest: sup_loc_length)
  10.243      finally
  10.244      show "G \<turnstile> (a!n) <=o (c!n)" .
  10.245 @@ -455,11 +455,11 @@
  10.246    
  10.247  
  10.248  theorem sup_state_trans [trans]:
  10.249 -  "[|G \<turnstile> a <=s b; G \<turnstile> b <=s c|] ==> G \<turnstile> a <=s c"
  10.250 +  "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
  10.251    by (auto intro: sup_loc_trans simp add: sup_state_def stk_convert Product.le_def lesub_def)
  10.252  
  10.253  theorem sup_state_opt_trans [trans]:
  10.254 -  "[|G \<turnstile> a <=' b; G \<turnstile> b <=' c|] ==> G \<turnstile> a <=' c"
  10.255 +  "\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
  10.256    by (auto intro: sup_state_trans 
  10.257             simp add: sup_state_opt_def Opt.le_def lesub_def 
  10.258             split: option.splits)
    11.1 --- a/src/HOL/MicroJava/BV/Kildall.thy	Sat Mar 02 12:09:23 2002 +0100
    11.2 +++ b/src/HOL/MicroJava/BV/Kildall.thy	Sun Mar 03 16:59:08 2002 +0100
    11.3 @@ -11,24 +11,24 @@
    11.4  theory Kildall = Typing_Framework + While_Combinator + Product:
    11.5  
    11.6  
    11.7 -syntax "@lesubstep_type" :: "(nat \<times> 's) list => 's ord => (nat \<times> 's) list => bool"
    11.8 +syntax "@lesubstep_type" :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
    11.9         ("(_ /<=|_| _)" [50, 0, 51] 50)
   11.10  translations
   11.11   "x <=|r| y" == "x <=[(Product.le (op =) r)] y"
   11.12   
   11.13  
   11.14  constdefs
   11.15 - pres_type :: "'s step_type => nat => 's set => bool"
   11.16 + pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
   11.17  "pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A"
   11.18  
   11.19 - mono :: "'s ord => 's step_type => nat => 's set => bool"
   11.20 + mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
   11.21  "mono r step n A ==
   11.22 - \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t --> step p s <=|r| step p t"
   11.23 + \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t"
   11.24  
   11.25  consts
   11.26   iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow>
   11.27            's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set"
   11.28 - propa :: "'s binop => (nat \<times> 's) list => 's list => nat set => 's list * nat set"
   11.29 + propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set"
   11.30  
   11.31  primrec
   11.32  "propa f []      ss w = (ss,w)"
   11.33 @@ -45,13 +45,13 @@
   11.34         (ss,w)"
   11.35  
   11.36  constdefs
   11.37 - unstables :: "'s ord => 's step_type => 's list => nat set"
   11.38 + unstables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat set"
   11.39  "unstables r step ss == {p. p < size ss \<and> \<not>stable r step ss p}"
   11.40  
   11.41 - kildall :: "'s ord => 's binop => 's step_type => 's list => 's list"
   11.42 + kildall :: "'s ord \<Rightarrow> 's binop \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> 's list"
   11.43  "kildall r f step ss == fst(iter f step ss (unstables r step ss))"
   11.44  
   11.45 -consts merges :: "'s binop => (nat \<times> 's) list => 's list => 's list"
   11.46 +consts merges :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> 's list"
   11.47  primrec
   11.48  "merges f []      ss = ss"
   11.49  "merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"
   11.50 @@ -61,16 +61,16 @@
   11.51  
   11.52  
   11.53  consts
   11.54 - "@plusplussub" :: "'a list => ('a => 'a => 'a) => 'a => 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
   11.55 + "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
   11.56  primrec
   11.57    "[] ++_f y = y"
   11.58    "(x#xs) ++_f y = xs ++_f (x +_f y)"
   11.59  
   11.60  lemma nth_merges:
   11.61 -  "!!ss. [| semilat (A, r, f); p < length ss; ss \<in> list n A; 
   11.62 -            \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A |] ==>
   11.63 +  "\<And>ss. \<lbrakk> semilat (A, r, f); p < length ss; ss \<in> list n A; 
   11.64 +            \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
   11.65    (merges f ps ss)!p = map snd [(p',t') \<in> ps. p'=p] ++_f ss!p"
   11.66 -  (is "!!ss. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?steptype ps \<Longrightarrow> ?P ss ps")
   11.67 +  (is "\<And>ss. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?steptype ps \<Longrightarrow> ?P ss ps")
   11.68  proof (induct ps)
   11.69    show "\<And>ss. ?P ss []" by simp
   11.70  
   11.71 @@ -98,15 +98,15 @@
   11.72  
   11.73  
   11.74  lemma pres_typeD:
   11.75 -  "[| pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) |] ==> s' \<in> A"
   11.76 +  "\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A"
   11.77    by (unfold pres_type_def, blast)
   11.78  
   11.79  lemma boundedD: 
   11.80 -  "[| bounded step n; p < n; (q,t) : set (step p xs) |] ==> q < n" 
   11.81 +  "\<lbrakk> bounded step n; p < n; (q,t) : set (step p xs) \<rbrakk> \<Longrightarrow> q < n" 
   11.82    by (unfold bounded_def, blast)
   11.83  
   11.84  lemma monoD:
   11.85 -  "[| mono r step n A; p < n; s\<in>A; s <=_r t |] ==> step p s <=|r| step p t"
   11.86 +  "\<lbrakk> mono r step n A; p < n; s\<in>A; s <=_r t \<rbrakk> \<Longrightarrow> step p s <=|r| step p t"
   11.87    by (unfold mono_def, blast)
   11.88  
   11.89  (** merges **)
   11.90 @@ -117,9 +117,9 @@
   11.91  
   11.92  
   11.93  lemma merges_preserves_type_lemma: 
   11.94 -  "[| semilat(A,r,f) |] ==>
   11.95 -     \<forall>xs. xs \<in> list n A --> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
   11.96 -          --> merges f ps xs \<in> list n A" 
   11.97 +  "semilat(A,r,f) \<Longrightarrow>
   11.98 +     \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
   11.99 +          \<longrightarrow> merges f ps xs \<in> list n A" 
  11.100    apply (frule semilatDclosedI) 
  11.101    apply (unfold closed_def) 
  11.102    apply (induct_tac ps)
  11.103 @@ -128,13 +128,13 @@
  11.104    done
  11.105  
  11.106  lemma merges_preserves_type [simp]:
  11.107 -  "[| semilat(A,r,f); xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A |]
  11.108 -  ==> merges f ps xs \<in> list n A"
  11.109 +  "\<lbrakk> semilat(A,r,f); xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
  11.110 +  \<Longrightarrow> merges f ps xs \<in> list n A"
  11.111    by (simp add: merges_preserves_type_lemma)
  11.112    
  11.113  lemma merges_incr_lemma:
  11.114 -  "[| semilat(A,r,f) |] ==> 
  11.115 -     \<forall>xs. xs \<in> list n A --> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) --> xs <=[r] merges f ps xs"
  11.116 +  "semilat(A,r,f) \<Longrightarrow> 
  11.117 +     \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs <=[r] merges f ps xs"
  11.118    apply (induct_tac ps)
  11.119     apply simp
  11.120    apply simp
  11.121 @@ -149,14 +149,14 @@
  11.122    done
  11.123  
  11.124  lemma merges_incr:
  11.125 -  "[| semilat(A,r,f); xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A |] 
  11.126 -  ==> xs <=[r] merges f ps xs"
  11.127 +  "\<lbrakk> semilat(A,r,f); xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk> 
  11.128 +  \<Longrightarrow> xs <=[r] merges f ps xs"
  11.129    by (simp add: merges_incr_lemma)
  11.130  
  11.131  
  11.132  lemma merges_same_conv [rule_format]:
  11.133 -  "[| semilat(A,r,f) |] ==> 
  11.134 -     (\<forall>xs. xs \<in> list n A --> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) --> 
  11.135 +  "semilat(A,r,f) \<Longrightarrow> 
  11.136 +     (\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow> 
  11.137       (merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))"
  11.138    apply (induct_tac ps)
  11.139     apply simp
  11.140 @@ -191,25 +191,25 @@
  11.141  
  11.142  
  11.143  lemma list_update_le_listI [rule_format]:
  11.144 -  "set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs -->  
  11.145 -   x <=_r ys!p --> semilat(A,r,f) --> x\<in>A --> 
  11.146 +  "set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>  
  11.147 +   x <=_r ys!p \<longrightarrow> semilat(A,r,f) \<longrightarrow> x\<in>A \<longrightarrow> 
  11.148     xs[p := x +_f xs!p] <=[r] ys"
  11.149    apply (unfold Listn.le_def lesub_def semilat_def)
  11.150    apply (simp add: list_all2_conv_all_nth nth_list_update)
  11.151    done
  11.152  
  11.153  lemma merges_pres_le_ub:
  11.154 -  "[| semilat(A,r,f); set ts <= A; set ss <= A; 
  11.155 +  "\<lbrakk> semilat(A,r,f); set ts <= A; set ss <= A; 
  11.156       \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts; 
  11.157 -     ss <=[r] ts |] 
  11.158 -  ==> merges f ps ss <=[r] ts"
  11.159 +     ss <=[r] ts \<rbrakk> 
  11.160 +  \<Longrightarrow> merges f ps ss <=[r] ts"
  11.161  proof -
  11.162    { fix A r f t ts ps
  11.163      have
  11.164 -    "!!qs. [| semilat(A,r,f); set ts <= A; 
  11.165 -              \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts |] ==> 
  11.166 -    set qs <= set ps  --> 
  11.167 -    (\<forall>ss. set ss <= A --> ss <=[r] ts --> merges f qs ss <=[r] ts)"
  11.168 +    "\<And>qs. \<lbrakk> semilat(A,r,f); set ts <= A; 
  11.169 +              \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts \<rbrakk> \<Longrightarrow> 
  11.170 +    set qs <= set ps  \<longrightarrow> 
  11.171 +    (\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)"
  11.172      apply (induct_tac qs)
  11.173       apply simp
  11.174      apply (simp (no_asm_simp))
  11.175 @@ -233,7 +233,7 @@
  11.176  
  11.177  
  11.178  lemma decomp_propa:
  11.179 -  "!!ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow> 
  11.180 +  "\<And>ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow> 
  11.181     propa f qs ss w = 
  11.182     (merges f qs ss, {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un w)"
  11.183    apply (induct qs)
  11.184 @@ -263,7 +263,7 @@
  11.185    thus "(x#xs) ++_f y \<in> A" by simp
  11.186  qed
  11.187  
  11.188 -lemma ub2: "!!y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
  11.189 +lemma ub2: "\<And>y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
  11.190  proof (induct x)
  11.191    show "\<And>y. semilat(A, r, f) \<Longrightarrow> y <=_r [] ++_f y" by simp 
  11.192    
  11.193 @@ -287,7 +287,8 @@
  11.194  qed
  11.195  
  11.196  
  11.197 -lemma ub1: "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
  11.198 +lemma ub1: 
  11.199 +  "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
  11.200  proof (induct ls)
  11.201    show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
  11.202    
  11.203 @@ -298,7 +299,8 @@
  11.204    then obtain s: "s \<in> A" and ls: "set ls \<subseteq> A" by simp
  11.205    assume y: "y \<in> A" 
  11.206  
  11.207 -  assume "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
  11.208 +  assume 
  11.209 +    "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
  11.210    hence IH: "\<And>y. x \<in> set ls \<Longrightarrow> y \<in> A \<Longrightarrow> x <=_r ls ++_f y" .
  11.211  
  11.212    assume "x \<in> set (s#ls)"
  11.213 @@ -356,12 +358,12 @@
  11.214  
  11.215  
  11.216  lemma stable_pres_lemma:
  11.217 -  "[| semilat (A,r,f); pres_type step n A; bounded step n; 
  11.218 +  "\<lbrakk> semilat (A,r,f); pres_type step n A; bounded step n; 
  11.219       ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n; 
  11.220       \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n; 
  11.221       \<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q; 
  11.222 -     q \<notin> w \<or> q = p |] 
  11.223 -  ==> stable r step (merges f (step p (ss!p)) ss) q"
  11.224 +     q \<notin> w \<or> q = p \<rbrakk> 
  11.225 +  \<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q"
  11.226    apply (unfold stable_def)
  11.227    apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A")
  11.228     prefer 2
  11.229 @@ -434,7 +436,7 @@
  11.230   
  11.231    
  11.232  lemma lesub_step_type:
  11.233 -  "!!b x y. a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
  11.234 +  "\<And>b x y. a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
  11.235  apply (induct a)
  11.236   apply simp
  11.237  apply simp
  11.238 @@ -451,10 +453,10 @@
  11.239  
  11.240  
  11.241  lemma merges_bounded_lemma:
  11.242 -  "[| semilat (A,r,f); mono r step n A; bounded step n; 
  11.243 +  "\<lbrakk> semilat (A,r,f); mono r step n A; bounded step n; 
  11.244       \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; 
  11.245 -     ss <=[r] ts; ! p. p < n --> stable r step ts p |] 
  11.246 -  ==> merges f (step p (ss!p)) ss <=[r] ts"
  11.247 +     ss <=[r] ts; ! p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
  11.248 +  \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts"
  11.249    apply (unfold stable_def)
  11.250    apply (rule merges_pres_le_ub)
  11.251        apply assumption
  11.252 @@ -481,7 +483,7 @@
  11.253    done
  11.254  
  11.255  lemma termination_lemma:  
  11.256 -  "[| semilat(A,r,f); ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w |] ==> 
  11.257 +  "\<lbrakk> semilat(A,r,f); ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> 
  11.258        ss <[r] merges f qs ss \<or> 
  11.259    merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w"
  11.260    apply (unfold lesssub_def)
  11.261 @@ -617,10 +619,10 @@
  11.262  done
  11.263  
  11.264  lemma is_bcv_kildall:
  11.265 -  "[| semilat(A,r,f); acc r; top r T; 
  11.266 +  "\<lbrakk> semilat(A,r,f); acc r; top r T; 
  11.267        pres_type step n A; bounded step n; 
  11.268 -      mono r step n A |]
  11.269 -  ==> is_bcv r T step n A (kildall r f step)"
  11.270 +      mono r step n A \<rbrakk>
  11.271 +  \<Longrightarrow> is_bcv r T step n A (kildall r f step)"
  11.272  apply(unfold is_bcv_def wt_step_def)
  11.273  apply(insert kildall_properties[of A])
  11.274  apply(simp add:stables_def)
    12.1 --- a/src/HOL/MicroJava/BV/LBVComplete.thy	Sat Mar 02 12:09:23 2002 +0100
    12.2 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Sun Mar 03 16:59:08 2002 +0100
    12.3 @@ -14,43 +14,43 @@
    12.4  theory LBVComplete = BVSpec + LBVSpec + EffectMono:
    12.5  
    12.6  constdefs
    12.7 -  contains_targets :: "[instr list, certificate, method_type, p_count] => bool"
    12.8 +  contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
    12.9    "contains_targets ins cert phi pc == 
   12.10       \<forall>pc' \<in> set (succs (ins!pc) pc). 
   12.11 -      pc' \<noteq> pc+1 \<and> pc' < length ins --> cert!pc' = phi!pc'"
   12.12 +      pc' \<noteq> pc+1 \<and> pc' < length ins \<longrightarrow> cert!pc' = phi!pc'"
   12.13  
   12.14 -  fits :: "[instr list, certificate, method_type] => bool"
   12.15 -  "fits ins cert phi == \<forall>pc. pc < length ins --> 
   12.16 +  fits :: "[instr list, certificate, method_type] \<Rightarrow> bool"
   12.17 +  "fits ins cert phi == \<forall>pc. pc < length ins \<longrightarrow> 
   12.18                         contains_targets ins cert phi pc \<and>
   12.19                         (cert!pc = None \<or> cert!pc = phi!pc)"
   12.20  
   12.21 -  is_target :: "[instr list, p_count] => bool" 
   12.22 +  is_target :: "[instr list, p_count] \<Rightarrow> bool" 
   12.23    "is_target ins pc == 
   12.24       \<exists>pc'. pc \<noteq> pc'+1 \<and> pc' < length ins \<and> pc \<in> set (succs (ins!pc') pc')"
   12.25  
   12.26  
   12.27  constdefs 
   12.28 -  make_cert :: "[instr list, method_type] => certificate"
   12.29 +  make_cert :: "[instr list, method_type] \<Rightarrow> certificate"
   12.30    "make_cert ins phi == 
   12.31       map (\<lambda>pc. if is_target ins pc then phi!pc else None) [0..length ins(]"
   12.32  
   12.33 -  make_Cert :: "[jvm_prog, prog_type] => prog_certificate"
   12.34 +  make_Cert :: "[jvm_prog, prog_type] \<Rightarrow> prog_certificate"
   12.35    "make_Cert G Phi ==  \<lambda> C sig. let (C,rT,(maxs,maxl,b)) = the (method (G,C) sig)
   12.36                                  in make_cert b (Phi C sig)"
   12.37    
   12.38  lemmas [simp del] = split_paired_Ex
   12.39  
   12.40  lemma make_cert_target:
   12.41 -  "[| pc < length ins; is_target ins pc |] ==> make_cert ins phi ! pc = phi!pc"
   12.42 +  "\<lbrakk> pc < length ins; is_target ins pc \<rbrakk> \<Longrightarrow> make_cert ins phi ! pc = phi!pc"
   12.43    by (simp add: make_cert_def)
   12.44  
   12.45  lemma make_cert_approx:
   12.46 -  "[| pc < length ins; make_cert ins phi ! pc \<noteq> phi ! pc |] ==> 
   12.47 +  "\<lbrakk> pc < length ins; make_cert ins phi ! pc \<noteq> phi ! pc \<rbrakk> \<Longrightarrow> 
   12.48     make_cert ins phi ! pc = None"
   12.49    by (auto simp add: make_cert_def)
   12.50  
   12.51  lemma make_cert_contains_targets:
   12.52 -  "pc < length ins ==> contains_targets ins (make_cert ins phi) phi pc"
   12.53 +  "pc < length ins \<Longrightarrow> contains_targets ins (make_cert ins phi) phi pc"
   12.54  proof (unfold contains_targets_def, intro strip, elim conjE) 
   12.55    fix pc'
   12.56    assume "pc < length ins" 
   12.57 @@ -71,19 +71,19 @@
   12.58    by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets)
   12.59  
   12.60  lemma fitsD: 
   12.61 -  "[| fits ins cert phi; pc' \<in> set (succs (ins!pc) pc); 
   12.62 -      pc' \<noteq> Suc pc; pc < length ins; pc' < length ins |]
   12.63 -  ==> cert!pc' = phi!pc'"
   12.64 +  "\<lbrakk> fits ins cert phi; pc' \<in> set (succs (ins!pc) pc); 
   12.65 +      pc' \<noteq> Suc pc; pc < length ins; pc' < length ins \<rbrakk>
   12.66 +  \<Longrightarrow> cert!pc' = phi!pc'"
   12.67    by (clarsimp simp add: fits_def contains_targets_def)
   12.68  
   12.69  lemma fitsD2:
   12.70 -   "[| fits ins cert phi; pc < length ins; cert!pc = Some s |]
   12.71 -  ==> cert!pc = phi!pc"
   12.72 +   "\<lbrakk> fits ins cert phi; pc < length ins; cert!pc = Some s \<rbrakk>
   12.73 +  \<Longrightarrow> cert!pc = phi!pc"
   12.74    by (auto simp add: fits_def)
   12.75                             
   12.76  lemma wtl_inst_mono:
   12.77 -  "[| wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; 
   12.78 -      pc < length ins;  G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
   12.79 +  "\<lbrakk> wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; 
   12.80 +      pc < length ins;  G \<turnstile> s2 <=' s1; i = ins!pc \<rbrakk> \<Longrightarrow>
   12.81    \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
   12.82  proof -
   12.83    assume pc:   "pc < length ins" "i = ins!pc"
   12.84 @@ -144,8 +144,8 @@
   12.85  
   12.86  
   12.87  lemma wtl_cert_mono:
   12.88 -  "[| wtl_cert i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; 
   12.89 -      pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
   12.90 +  "\<lbrakk> wtl_cert i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; 
   12.91 +      pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc \<rbrakk> \<Longrightarrow>
   12.92    \<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
   12.93  proof -
   12.94    assume wtl:  "wtl_cert i G rT s1 cert mxs mpc pc = OK s1'" and
   12.95 @@ -181,8 +181,8 @@
   12.96  
   12.97   
   12.98  lemma wt_instr_imp_wtl_inst:
   12.99 -  "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
  12.100 -      pc < length ins; length ins = max_pc |] ==> 
  12.101 +  "\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
  12.102 +      pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow> 
  12.103    wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
  12.104   proof -
  12.105    assume wt:   "wt_instr (ins!pc) G rT phi mxs max_pc pc" 
  12.106 @@ -193,14 +193,14 @@
  12.107    have app: "app (ins!pc) G mxs rT (phi!pc)" by (simp add: wt_instr_def)
  12.108  
  12.109    from wt pc
  12.110 -  have pc': "!!pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
  12.111 +  have pc': "\<And>pc'. pc' \<in> set (succs (ins!pc) pc) \<Longrightarrow> pc' < length ins"
  12.112      by (simp add: wt_instr_def)
  12.113  
  12.114    let ?s' = "eff (ins!pc) G (phi!pc)"
  12.115  
  12.116    from wt fits pc
  12.117 -  have cert: "!!pc'. [|pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1|] 
  12.118 -    ==> G \<turnstile> ?s' <=' cert!pc'"
  12.119 +  have cert: "\<And>pc'. \<lbrakk>pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1\<rbrakk> 
  12.120 +    \<Longrightarrow> G \<turnstile> ?s' <=' cert!pc'"
  12.121      by (auto dest: fitsD simp add: wt_instr_def)     
  12.122  
  12.123    from app pc cert pc'
  12.124 @@ -209,9 +209,9 @@
  12.125  qed
  12.126  
  12.127  lemma wt_less_wtl:
  12.128 -  "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; 
  12.129 +  "\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; 
  12.130        wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s;
  12.131 -      fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> 
  12.132 +      fits ins cert phi; Suc pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow> 
  12.133    G \<turnstile> s <=' phi ! Suc pc"
  12.134  proof -
  12.135    assume wt:   "wt_instr (ins!pc) G rT phi mxs max_pc pc" 
  12.136 @@ -222,7 +222,7 @@
  12.137    { assume suc: "Suc pc \<in> set (succs (ins ! pc) pc)"
  12.138      with wtl have "s = eff (ins!pc) G (phi!pc)"
  12.139        by (simp add: wtl_inst_OK)
  12.140 -    also from suc wt have "G \<turnstile> ... <=' phi!Suc pc"
  12.141 +    also from suc wt have "G \<turnstile> \<dots> <=' phi!Suc pc"
  12.142        by (simp add: wt_instr_def)
  12.143      finally have ?thesis .
  12.144    }
  12.145 @@ -244,8 +244,8 @@
  12.146    
  12.147  
  12.148  lemma wt_instr_imp_wtl_cert:
  12.149 -  "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
  12.150 -      pc < length ins; length ins = max_pc |] ==> 
  12.151 +  "\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
  12.152 +      pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow> 
  12.153    wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
  12.154  proof -
  12.155    assume "wt_instr (ins!pc) G rT phi mxs max_pc pc" and 
  12.156 @@ -256,7 +256,7 @@
  12.157    hence wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
  12.158      by (rule wt_instr_imp_wtl_inst)
  12.159  
  12.160 -  hence "cert!pc = None ==> ?thesis"
  12.161 +  hence "cert!pc = None \<Longrightarrow> ?thesis"
  12.162      by (simp add: wtl_cert_def)
  12.163  
  12.164    moreover
  12.165 @@ -276,9 +276,9 @@
  12.166    
  12.167  
  12.168  lemma wt_less_wtl_cert:
  12.169 -  "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; 
  12.170 +  "\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; 
  12.171        wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s;
  12.172 -      fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> 
  12.173 +      fits ins cert phi; Suc pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow> 
  12.174    G \<turnstile> s <=' phi ! Suc pc"
  12.175  proof -
  12.176    assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s"
  12.177 @@ -319,14 +319,14 @@
  12.178  *}
  12.179  
  12.180  theorem wt_imp_wtl_inst_list:
  12.181 -"\<forall> pc. (\<forall>pc'. pc' < length all_ins --> 
  12.182 -        wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc') -->
  12.183 -       fits all_ins cert phi --> 
  12.184 -       (\<exists>l. pc = length l \<and> all_ins = l@ins) -->  
  12.185 -       pc < length all_ins -->      
  12.186 -       (\<forall> s. (G \<turnstile> s <=' (phi!pc)) --> 
  12.187 +"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow> 
  12.188 +        wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc') \<longrightarrow>
  12.189 +       fits all_ins cert phi \<longrightarrow> 
  12.190 +       (\<exists>l. pc = length l \<and> all_ins = l@ins) \<longrightarrow>  
  12.191 +       pc < length all_ins \<longrightarrow>      
  12.192 +       (\<forall> s. (G \<turnstile> s <=' (phi!pc)) \<longrightarrow> 
  12.193               wtl_inst_list ins G rT cert mxs (length all_ins) pc s \<noteq> Err)" 
  12.194 -(is "\<forall>pc. ?wt --> ?fits --> ?l pc ins --> ?len pc --> ?wtl pc ins"  
  12.195 +(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins"  
  12.196   is "\<forall>pc. ?C pc ins" is "?P ins") 
  12.197  proof (induct "?P" "ins")
  12.198    case Nil
  12.199 @@ -338,7 +338,7 @@
  12.200    show "?P (i#ins')" 
  12.201    proof (intro allI impI, elim exE conjE)
  12.202      fix pc s l
  12.203 -    assume wt  : "\<forall>pc'. pc' < length all_ins --> 
  12.204 +    assume wt  : "\<forall>pc'. pc' < length all_ins \<longrightarrow> 
  12.205                          wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc'"
  12.206      assume fits: "fits all_ins cert phi"
  12.207      assume l   : "pc < length all_ins"
  12.208 @@ -357,7 +357,7 @@
  12.209      from Cons
  12.210      have "?C (Suc pc) ins'" by blast
  12.211      with wt fits pc
  12.212 -    have IH: "?len (Suc pc) --> ?wtl (Suc pc) ins'" by auto
  12.213 +    have IH: "?len (Suc pc) \<longrightarrow> ?wtl (Suc pc) ins'" by auto
  12.214  
  12.215      show "wtl_inst_list (i#ins') G rT cert mxs (length all_ins) pc s \<noteq> Err" 
  12.216      proof (cases "?len (Suc pc)")
  12.217 @@ -398,15 +398,15 @@
  12.218    
  12.219  
  12.220  lemma fits_imp_wtl_method_complete:
  12.221 -  "[| wt_method G C pTs rT mxs mxl ins phi; fits ins cert phi |] 
  12.222 -  ==> wtl_method G C pTs rT mxs mxl ins cert"
  12.223 +  "\<lbrakk> wt_method G C pTs rT mxs mxl ins phi; fits ins cert phi \<rbrakk> 
  12.224 +  \<Longrightarrow> wtl_method G C pTs rT mxs mxl ins cert"
  12.225  by (simp add: wt_method_def wtl_method_def)
  12.226     (rule wt_imp_wtl_inst_list [rule_format, elim_format], auto simp add: wt_start_def) 
  12.227  
  12.228  
  12.229  lemma wtl_method_complete:
  12.230    "wt_method G C pTs rT mxs mxl ins phi 
  12.231 -  ==> wtl_method G C pTs rT mxs mxl ins (make_cert ins phi)"
  12.232 +  \<Longrightarrow> wtl_method G C pTs rT mxs mxl ins (make_cert ins phi)"
  12.233  proof -
  12.234    assume "wt_method G C pTs rT mxs mxl ins phi" 
  12.235    moreover
  12.236 @@ -419,7 +419,7 @@
  12.237  
  12.238  
  12.239  theorem wtl_complete:
  12.240 -  "wt_jvm_prog G Phi ==> wtl_jvm_prog G (make_Cert G Phi)"
  12.241 +  "wt_jvm_prog G Phi \<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)"
  12.242  proof -
  12.243    assume wt: "wt_jvm_prog G Phi"
  12.244     
    13.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Sat Mar 02 12:09:23 2002 +0100
    13.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Sun Mar 03 16:59:08 2002 +0100
    13.3 @@ -17,40 +17,40 @@
    13.4  lemmas [simp del] = split_paired_Ex split_paired_All
    13.5  
    13.6  constdefs
    13.7 -fits :: "[method_type,instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] => bool"
    13.8 +fits :: "[method_type,instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] \<Rightarrow> bool"
    13.9  "fits phi is G rT s0 maxs maxr et cert == 
   13.10 -  (\<forall>pc s1. pc < length is -->
   13.11 -    (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0 = OK s1 -->
   13.12 -    (case cert!pc of None   => phi!pc = s1
   13.13 -                   | Some t => phi!pc = Some t)))"
   13.14 +  (\<forall>pc s1. pc < length is \<longrightarrow>
   13.15 +    (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0 = OK s1 \<longrightarrow>
   13.16 +    (case cert!pc of None   \<Rightarrow> phi!pc = s1
   13.17 +                   | Some t \<Rightarrow> phi!pc = Some t)))"
   13.18  
   13.19  constdefs
   13.20 -make_phi :: "[instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] => method_type"
   13.21 +make_phi :: "[instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] \<Rightarrow> method_type"
   13.22  "make_phi is G rT s0 maxs maxr et cert == 
   13.23     map (\<lambda>pc. case cert!pc of 
   13.24 -               None   => ok_val (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0) 
   13.25 -             | Some t => Some t) [0..length is(]"
   13.26 +               None   \<Rightarrow> ok_val (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0) 
   13.27 +             | Some t \<Rightarrow> Some t) [0..length is(]"
   13.28  
   13.29  
   13.30  lemma fitsD_None:
   13.31 -  "[|fits phi is G rT s0 mxs mxr et cert; pc < length is;
   13.32 +  "\<lbrakk>fits phi is G rT s0 mxs mxr et cert; pc < length is;
   13.33      wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0 = OK s1; 
   13.34 -    cert ! pc = None|] ==> phi!pc = s1"
   13.35 +    cert ! pc = None\<rbrakk> \<Longrightarrow> phi!pc = s1"
   13.36    by (auto simp add: fits_def)
   13.37  
   13.38  lemma fitsD_Some:
   13.39 -  "[|fits phi is G rT s0 mxs mxr et cert; pc < length is;
   13.40 +  "\<lbrakk>fits phi is G rT s0 mxs mxr et cert; pc < length is;
   13.41      wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0 = OK s1; 
   13.42 -    cert ! pc = Some t|] ==> phi!pc = Some t"
   13.43 +    cert ! pc = Some t\<rbrakk> \<Longrightarrow> phi!pc = Some t"
   13.44    by (auto simp add: fits_def)
   13.45  
   13.46  lemma make_phi_Some:
   13.47 -  "[| pc < length is; cert!pc = Some t |] ==> 
   13.48 +  "\<lbrakk> pc < length is; cert!pc = Some t \<rbrakk> \<Longrightarrow> 
   13.49    make_phi is G rT s0 mxs mxr et cert ! pc = Some t"
   13.50    by (simp add: make_phi_def)
   13.51  
   13.52  lemma make_phi_None:
   13.53 -  "[| pc < length is; cert!pc = None |] ==> 
   13.54 +  "\<lbrakk> pc < length is; cert!pc = None \<rbrakk> \<Longrightarrow> 
   13.55    make_phi is G rT s0 mxs mxr et cert ! pc = 
   13.56    ok_val (wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0)"
   13.57    by (simp add: make_phi_def)
   13.58 @@ -65,8 +65,8 @@
   13.59  qed
   13.60    
   13.61  lemma fits_lemma1:
   13.62 -  "[| wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'; fits phi is G rT s mxs mxr et cert |]
   13.63 -  ==> \<forall>pc t. pc < length is --> cert!pc = Some t --> phi!pc = Some t"
   13.64 +  "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'; fits phi is G rT s mxs mxr et cert \<rbrakk>
   13.65 +  \<Longrightarrow> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t"
   13.66  proof (intro strip)
   13.67    fix pc t 
   13.68    assume "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'"
   13.69 @@ -83,10 +83,10 @@
   13.70  
   13.71  
   13.72  lemma wtl_suc_pc:
   13.73 - "[| wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
   13.74 + "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
   13.75       wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s';
   13.76       wtl_cert (is!pc) G rT s' cert mxs mxr (length is) et pc = OK s'';
   13.77 -     fits phi is G rT s mxs mxr et cert; Suc pc < length is |] ==>
   13.78 +     fits phi is G rT s mxs mxr et cert; Suc pc < length is \<rbrakk> \<Longrightarrow>
   13.79    G \<turnstile> s'' <=' phi ! Suc pc"
   13.80  proof -
   13.81    
   13.82 @@ -117,15 +117,15 @@
   13.83      "wtl_cert l G rT s'' cert mxs mxr (length is) et (Suc pc) = OK x"
   13.84      by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
   13.85  
   13.86 -  hence c1: "!!t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
   13.87 +  hence c1: "\<And>t. cert!Suc pc = Some t \<Longrightarrow> G \<turnstile> s'' <=' cert!Suc pc"
   13.88      by (simp add: wtl_cert_def split: split_if_asm)
   13.89    moreover
   13.90    from fits pc wts
   13.91 -  have c2: "!!t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
   13.92 +  have c2: "\<And>t. cert!Suc pc = Some t \<Longrightarrow> phi!Suc pc = cert!Suc pc"
   13.93      by - (drule fitsD_Some, auto)
   13.94    moreover
   13.95    from fits pc wts
   13.96 -  have c3: "cert!Suc pc = None ==> phi!Suc pc = s''"
   13.97 +  have c3: "cert!Suc pc = None \<Longrightarrow> phi!Suc pc = s''"
   13.98      by (rule fitsD_None)
   13.99    ultimately
  13.100    show ?thesis by (cases "cert!Suc pc", auto)
  13.101 @@ -133,8 +133,8 @@
  13.102  
  13.103  
  13.104  lemma wtl_fits_wt:
  13.105 -  "[| wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err; 
  13.106 -      fits phi is G rT s mxs mxr et cert; pc < length is |] ==>
  13.107 +  "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err; 
  13.108 +      fits phi is G rT s mxs mxr et cert; pc < length is \<rbrakk> \<Longrightarrow>
  13.109     wt_instr (is!pc) G rT phi mxs (length is) et pc"
  13.110  proof -
  13.111    assume fits: "fits phi is G rT s mxs mxr et cert"
  13.112 @@ -146,10 +146,10 @@
  13.113      by - (drule wtl_all, auto)
  13.114  
  13.115    from fits wtl pc have cert_Some: 
  13.116 -    "!!t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
  13.117 +    "\<And>t pc. \<lbrakk> pc < length is; cert!pc = Some t \<rbrakk> \<Longrightarrow> phi!pc = Some t"
  13.118      by (auto dest: fits_lemma1)
  13.119    
  13.120 -  from fits wtl pc have cert_None: "cert!pc = None ==> phi!pc = s'"
  13.121 +  from fits wtl pc have cert_None: "cert!pc = None \<Longrightarrow> phi!pc = s'"
  13.122      by - (drule fitsD_None)
  13.123    
  13.124    from pc c cert_None cert_Some
  13.125 @@ -169,8 +169,8 @@
  13.126        case False          
  13.127        with wti pc'
  13.128        have G: "G \<turnstile> r <=' cert ! pc'" by (simp add: wtl_inst_OK) blast
  13.129 -      hence "cert!pc' = None ==> r = None" by simp
  13.130 -      hence "cert!pc' = None ==> ?thesis" by simp
  13.131 +      hence "cert!pc' = None \<Longrightarrow> r = None" by simp
  13.132 +      hence "cert!pc' = None \<Longrightarrow> ?thesis" by simp
  13.133        moreover {
  13.134          fix t assume "cert!pc' = Some t"
  13.135          with less have "phi!pc' = cert!pc'" by (simp add: cert_Some)
  13.136 @@ -183,7 +183,7 @@
  13.137        have "G \<turnstile> r <=' s''"  sorry
  13.138        also
  13.139        from wtl w fits c pc 
  13.140 -      have "Suc pc < length is ==> G \<turnstile> s'' <=' phi ! Suc pc" 
  13.141 +      have "Suc pc < length is \<Longrightarrow> G \<turnstile> s'' <=' phi ! Suc pc" 
  13.142          by - (rule wtl_suc_pc)
  13.143        with True less
  13.144        have "G \<turnstile> s'' <=' phi ! Suc pc" by blast
  13.145 @@ -197,8 +197,8 @@
  13.146  
  13.147      
  13.148  lemma fits_first:
  13.149 -  "[| 0 < length is; wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err; 
  13.150 -      fits phi is G rT s mxs mxr et cert |] ==> 
  13.151 +  "\<lbrakk> 0 < length is; wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err; 
  13.152 +      fits phi is G rT s mxs mxr et cert \<rbrakk> \<Longrightarrow> 
  13.153    G \<turnstile> s <=' phi ! 0"
  13.154  proof -
  13.155    assume wtl:  "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
  13.156 @@ -210,11 +210,11 @@
  13.157      by simp
  13.158    
  13.159    with fits pc
  13.160 -  have "cert!0 = None ==> phi!0 = s"
  13.161 +  have "cert!0 = None \<Longrightarrow> phi!0 = s"
  13.162      by (rule fitsD_None)
  13.163    moreover    
  13.164    from fits pc wt0
  13.165 -  have "!!t. cert!0 = Some t ==> phi!0 = cert!0"
  13.166 +  have "\<And>t. cert!0 = Some t \<Longrightarrow> phi!0 = cert!0"
  13.167      by - (drule fitsD_Some, auto)
  13.168    moreover
  13.169    from pc
  13.170 @@ -225,7 +225,7 @@
  13.171      "wtl_cert x G rT s cert mxs mxr (length is) et 0 = OK s'"
  13.172      by auto
  13.173    hence 
  13.174 -    "!!t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
  13.175 +    "\<And>t. cert!0 = Some t \<Longrightarrow> G \<turnstile> s <=' cert!0"
  13.176      by (simp add: wtl_cert_def split: split_if_asm)
  13.177  
  13.178    ultimately
  13.179 @@ -235,7 +235,7 @@
  13.180  
  13.181    
  13.182  lemma wtl_method_correct:
  13.183 -"wtl_method G C pTs rT mxs mxl et ins cert ==> \<exists> phi. wt_method G C pTs rT mxs mxl ins et phi"
  13.184 +"wtl_method G C pTs rT mxs mxl et ins cert \<Longrightarrow> \<exists> phi. wt_method G C pTs rT mxs mxl ins et phi"
  13.185  proof (unfold wtl_method_def, simp only: Let_def, elim conjE)
  13.186    let "?s0" = "Some ([], OK (Class C) # map OK pTs @ replicate mxl Err)"
  13.187    assume pc:  "0 < length ins"
  13.188 @@ -246,7 +246,7 @@
  13.189  
  13.190    with wtl
  13.191    have allpc:
  13.192 -    "\<forall>pc. pc < length ins --> wt_instr (ins ! pc) G rT phi mxs (length ins) et pc"
  13.193 +    "\<forall>pc. pc < length ins \<longrightarrow> wt_instr (ins ! pc) G rT phi mxs (length ins) et pc"
  13.194      by (blast intro: wtl_fits_wt)
  13.195  
  13.196    from pc wtl fits
  13.197 @@ -259,7 +259,7 @@
  13.198  
  13.199  
  13.200  theorem wtl_correct:
  13.201 -  "wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
  13.202 +  "wtl_jvm_prog G cert \<Longrightarrow> \<exists> Phi. wt_jvm_prog G Phi"
  13.203  proof -  
  13.204    assume wtl: "wtl_jvm_prog G cert"
  13.205  
    14.1 --- a/src/HOL/MicroJava/BV/LBVSpec.thy	Sat Mar 02 12:09:23 2002 +0100
    14.2 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Sun Mar 03 16:59:08 2002 +0100
    14.3 @@ -22,8 +22,8 @@
    14.4  
    14.5  types
    14.6    certificate       = "state_type option list" 
    14.7 -  class_certificate = "sig => certificate"
    14.8 -  prog_certificate  = "cname => class_certificate"
    14.9 +  class_certificate = "sig \<Rightarrow> certificate"
   14.10 +  prog_certificate  = "cname \<Rightarrow> class_certificate"
   14.11  
   14.12  consts
   14.13    merge :: "[jvm_prog, p_count, nat, nat, p_count, certificate, (nat \<times> (state_type option)) list, state] \<Rightarrow> state"
   14.14 @@ -38,24 +38,24 @@
   14.15  
   14.16  constdefs 
   14.17    wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count] 
   14.18 -               => state_type option err" 
   14.19 +               \<Rightarrow> state_type option err" 
   14.20    "wtl_inst i G rT s cert maxs maxr max_pc et pc == 
   14.21       if app i G maxs rT pc et s then 
   14.22         merge G pc maxs maxr max_pc cert (eff i G pc et s) (OK (cert!(pc+1)))
   14.23       else Err"
   14.24  
   14.25    wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count] 
   14.26 -               => state_type option err"  
   14.27 +               \<Rightarrow> state_type option err"  
   14.28    "wtl_cert i G rT s cert maxs maxr max_pc et pc ==
   14.29       case cert!pc of
   14.30 -        None    => wtl_inst i G rT s cert maxs maxr max_pc et pc
   14.31 -      | Some s' => if G \<turnstile> s <=' (Some s') then 
   14.32 +        None    \<Rightarrow> wtl_inst i G rT s cert maxs maxr max_pc et pc
   14.33 +      | Some s' \<Rightarrow> if G \<turnstile> s <=' (Some s') then 
   14.34                      wtl_inst i G rT (Some s') cert maxs maxr max_pc et pc 
   14.35                    else Err"
   14.36  
   14.37  consts 
   14.38    wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,nat,p_count,exception_table,p_count,
   14.39 -                     state_type option] => state_type option err"
   14.40 +                     state_type option] \<Rightarrow> state_type option err"
   14.41  primrec
   14.42    "wtl_inst_list []     G rT cert maxs maxr max_pc et pc s = OK s"
   14.43    "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s = 
   14.44 @@ -64,7 +64,7 @@
   14.45                
   14.46  
   14.47  constdefs
   14.48 - wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,exception_table,instr list,certificate] => bool"  
   14.49 + wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,exception_table,instr list,certificate] \<Rightarrow> bool"  
   14.50   "wtl_method G C pTs rT mxs mxl et ins cert ==  
   14.51  	let max_pc = length ins  
   14.52    in 
   14.53 @@ -72,7 +72,7 @@
   14.54    wtl_inst_list ins G rT cert mxs mxl max_pc et 0 
   14.55                  (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \<noteq> Err"
   14.56  
   14.57 - wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool" 
   14.58 + wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool" 
   14.59   "wtl_jvm_prog G cert ==  
   14.60    wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b,et). wtl_method G C (snd sig) rT maxs maxl et b (cert C sig)) G"
   14.61  
   14.62 @@ -84,12 +84,12 @@
   14.63    by simp
   14.64  
   14.65  lemma merge_def:
   14.66 -  "!!x. merge G pc mxs mxr max_pc cert ss x = 
   14.67 +  "\<And>x. merge G pc mxs mxr max_pc cert ss x = 
   14.68    (if \<forall>(pc',s') \<in> set ss. pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> s' <=' cert!pc') then
   14.69      map (OK \<circ> snd) [(p',t') \<in> ss. p'=pc+1] ++_(sup G mxs mxr) x
   14.70 -  else Err)" (is "!!x. ?merge ss x = ?if ss x" is "!!x. ?P ss x")
   14.71 +  else Err)" (is "\<And>x. ?merge ss x = ?if ss x" is "\<And>x. ?P ss x")
   14.72  proof (induct ss)
   14.73 -  show "!!x. ?P [] x" by simp
   14.74 +  show "\<And>x. ?P [] x" by simp
   14.75  next
   14.76    have OK_snd: "(\<lambda>u. OK (snd u)) = OK \<circ> snd" by (rule ext) auto
   14.77    fix x ss and s::"nat \<times> (state_type option)"
   14.78 @@ -173,7 +173,7 @@
   14.79  qed
   14.80  
   14.81  lemma wtl_take:
   14.82 -  "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s'' ==>
   14.83 +  "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s'' \<Longrightarrow>
   14.84     \<exists>s'. wtl_inst_list (take pc' is) G rT cert mxs mxr mpc et pc s = OK s'"
   14.85  proof -
   14.86    assume "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s''"
   14.87 @@ -183,7 +183,7 @@
   14.88  qed
   14.89  
   14.90  lemma take_Suc:
   14.91 -  "\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
   14.92 +  "\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
   14.93  proof (induct l)
   14.94    show "?P []" by simp
   14.95  next
   14.96 @@ -197,9 +197,9 @@
   14.97  qed
   14.98  
   14.99  lemma wtl_Suc:
  14.100 - "[| wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'; 
  14.101 + "\<lbrakk> wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'; 
  14.102       wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s'';
  14.103 -     Suc pc < length is |] ==>
  14.104 +     Suc pc < length is \<rbrakk> \<Longrightarrow>
  14.105    wtl_inst_list (take (Suc pc) is) G rT cert maxs maxr (length is) et 0 s = OK s''" 
  14.106  proof -
  14.107    assume "wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'"
  14.108 @@ -210,8 +210,8 @@
  14.109  qed
  14.110  
  14.111  lemma wtl_all:
  14.112 -  "[| wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err;
  14.113 -      pc < length is |] ==> 
  14.114 +  "\<lbrakk> wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err;
  14.115 +      pc < length is \<rbrakk> \<Longrightarrow> 
  14.116     \<exists>s' s''. wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s' \<and> 
  14.117              wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
  14.118  proof -
    15.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Sat Mar 02 12:09:23 2002 +0100
    15.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Sun Mar 03 16:59:08 2002 +0100
    15.3 @@ -12,41 +12,41 @@
    15.4  
    15.5  constdefs
    15.6  
    15.7 - list :: "nat => 'a set => 'a list set"
    15.8 + list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set"
    15.9  "list n A == {xs. length xs = n & set xs <= A}"
   15.10  
   15.11 - le :: "'a ord => ('a list)ord"
   15.12 + le :: "'a ord \<Rightarrow> ('a list)ord"
   15.13  "le r == list_all2 (%x y. x <=_r y)"
   15.14  
   15.15 -syntax "@lesublist" :: "'a list => 'a ord => 'a list => bool"
   15.16 +syntax "@lesublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
   15.17         ("(_ /<=[_] _)" [50, 0, 51] 50)
   15.18 -syntax "@lesssublist" :: "'a list => 'a ord => 'a list => bool"
   15.19 +syntax "@lesssublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
   15.20         ("(_ /<[_] _)" [50, 0, 51] 50)
   15.21  translations
   15.22   "x <=[r] y" == "x <=_(Listn.le r) y"
   15.23   "x <[r] y"  == "x <_(Listn.le r) y"
   15.24  
   15.25  constdefs
   15.26 - map2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
   15.27 + map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
   15.28  "map2 f == (%xs ys. map (split f) (zip xs ys))"
   15.29  
   15.30 -syntax "@plussublist" :: "'a list => ('a => 'b => 'c) => 'b list => 'c list"
   15.31 +syntax "@plussublist" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
   15.32         ("(_ /+[_] _)" [65, 0, 66] 65)
   15.33  translations  "x +[f] y" == "x +_(map2 f) y"
   15.34  
   15.35 -consts coalesce :: "'a err list => 'a list err"
   15.36 +consts coalesce :: "'a err list \<Rightarrow> 'a list err"
   15.37  primrec
   15.38  "coalesce [] = OK[]"
   15.39  "coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"
   15.40  
   15.41  constdefs
   15.42 - sl :: "nat => 'a sl => 'a list sl"
   15.43 + sl :: "nat \<Rightarrow> 'a sl \<Rightarrow> 'a list sl"
   15.44  "sl n == %(A,r,f). (list n A, le r, map2 f)"
   15.45  
   15.46 - sup :: "('a => 'b => 'c err) => 'a list => 'b list => 'c list err"
   15.47 + sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list err"
   15.48  "sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
   15.49  
   15.50 - upto_esl :: "nat => 'a esl => 'a list esl"
   15.51 + upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl"
   15.52  "upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"
   15.53  
   15.54  lemmas [simp] = set_update_subsetI
   15.55 @@ -75,7 +75,7 @@
   15.56  done
   15.57  
   15.58  lemma Cons_less_Conss [simp]:
   15.59 -  "order r ==> 
   15.60 +  "order r \<Longrightarrow> 
   15.61    x#xs <_(Listn.le r) y#ys = 
   15.62    (x <_r y & xs <=[r] ys  |  x = y & xs <_(Listn.le r) ys)"
   15.63  apply (unfold lesssub_def)
   15.64 @@ -83,7 +83,7 @@
   15.65  done  
   15.66  
   15.67  lemma list_update_le_cong:
   15.68 -  "[| i<size xs; xs <=[r] ys; x <=_r y |] ==> xs[i:=x] <=[r] ys[i:=y]";
   15.69 +  "\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]";
   15.70  apply (unfold unfold_lesub_list)
   15.71  apply (unfold Listn.le_def)
   15.72  apply (simp add: list_all2_conv_all_nth nth_list_update)
   15.73 @@ -91,19 +91,19 @@
   15.74  
   15.75  
   15.76  lemma le_listD:
   15.77 -  "[| xs <=[r] ys; p < size xs |] ==> xs!p <=_r ys!p"
   15.78 +  "\<lbrakk> xs <=[r] ys; p < size xs \<rbrakk> \<Longrightarrow> xs!p <=_r ys!p"
   15.79  apply (unfold Listn.le_def lesub_def)
   15.80  apply (simp add: list_all2_conv_all_nth)
   15.81  done
   15.82  
   15.83  lemma le_list_refl:
   15.84 -  "!x. x <=_r x ==> xs <=[r] xs"
   15.85 +  "!x. x <=_r x \<Longrightarrow> xs <=[r] xs"
   15.86  apply (unfold unfold_lesub_list)
   15.87  apply (simp add: Listn.le_def list_all2_conv_all_nth)
   15.88  done
   15.89  
   15.90  lemma le_list_trans:
   15.91 -  "[| order r; xs <=[r] ys; ys <=[r] zs |] ==> xs <=[r] zs"
   15.92 +  "\<lbrakk> order r; xs <=[r] ys; ys <=[r] zs \<rbrakk> \<Longrightarrow> xs <=[r] zs"
   15.93  apply (unfold unfold_lesub_list)
   15.94  apply (simp add: Listn.le_def list_all2_conv_all_nth)
   15.95  apply clarify
   15.96 @@ -112,7 +112,7 @@
   15.97  done
   15.98  
   15.99  lemma le_list_antisym:
  15.100 -  "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys"
  15.101 +  "\<lbrakk> order r; xs <=[r] ys; ys <=[r] xs \<rbrakk> \<Longrightarrow> xs = ys"
  15.102  apply (unfold unfold_lesub_list)
  15.103  apply (simp add: Listn.le_def list_all2_conv_all_nth)
  15.104  apply (rule nth_equalityI)
  15.105 @@ -123,7 +123,7 @@
  15.106  done
  15.107  
  15.108  lemma order_listI [simp, intro!]:
  15.109 -  "order r ==> order(Listn.le r)"
  15.110 +  "order r \<Longrightarrow> order(Listn.le r)"
  15.111  apply (subst order_def)
  15.112  apply (blast intro: le_list_refl le_list_trans le_list_antisym
  15.113               dest: order_refl)
  15.114 @@ -131,35 +131,35 @@
  15.115  
  15.116  
  15.117  lemma lesub_list_impl_same_size [simp]:
  15.118 -  "xs <=[r] ys ==> size ys = size xs"  
  15.119 +  "xs <=[r] ys \<Longrightarrow> size ys = size xs"  
  15.120  apply (unfold Listn.le_def lesub_def)
  15.121  apply (simp add: list_all2_conv_all_nth)
  15.122  done 
  15.123  
  15.124  lemma lesssub_list_impl_same_size:
  15.125 -  "xs <_(Listn.le r) ys ==> size ys = size xs"
  15.126 +  "xs <_(Listn.le r) ys \<Longrightarrow> size ys = size xs"
  15.127  apply (unfold lesssub_def)
  15.128  apply auto
  15.129  done  
  15.130  
  15.131  lemma listI:
  15.132 -  "[| length xs = n; set xs <= A |] ==> xs : list n A"
  15.133 +  "\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A"
  15.134  apply (unfold list_def)
  15.135  apply blast
  15.136  done
  15.137  
  15.138  lemma listE_length [simp]:
  15.139 -   "xs : list n A ==> length xs = n"
  15.140 +   "xs : list n A \<Longrightarrow> length xs = n"
  15.141  apply (unfold list_def)
  15.142  apply blast
  15.143  done 
  15.144  
  15.145  lemma less_lengthI:
  15.146 -  "[| xs : list n A; p < n |] ==> p < length xs"
  15.147 +  "\<lbrakk> xs : list n A; p < n \<rbrakk> \<Longrightarrow> p < length xs"
  15.148    by simp
  15.149  
  15.150  lemma listE_set [simp]:
  15.151 -  "xs : list n A ==> set xs <= A"
  15.152 +  "xs : list n A \<Longrightarrow> set xs <= A"
  15.153  apply (unfold list_def)
  15.154  apply blast
  15.155  done 
  15.156 @@ -183,7 +183,7 @@
  15.157  done 
  15.158  
  15.159  lemma list_not_empty:
  15.160 -  "? a. a:A ==> ? xs. xs : list n A";
  15.161 +  "? a. a:A \<Longrightarrow> ? xs. xs : list n A";
  15.162  apply (induct "n")
  15.163   apply simp
  15.164  apply (simp add: in_list_Suc_iff)
  15.165 @@ -192,18 +192,18 @@
  15.166  
  15.167  
  15.168  lemma nth_in [rule_format, simp]:
  15.169 -  "!i n. length xs = n --> set xs <= A --> i < n --> (xs!i) : A"
  15.170 +  "!i n. length xs = n \<longrightarrow> set xs <= A \<longrightarrow> i < n \<longrightarrow> (xs!i) : A"
  15.171  apply (induct "xs")
  15.172   apply simp
  15.173  apply (simp add: nth_Cons split: nat.split)
  15.174  done
  15.175  
  15.176  lemma listE_nth_in:
  15.177 -  "[| xs : list n A; i < n |] ==> (xs!i) : A"
  15.178 +  "\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A"
  15.179    by auto
  15.180  
  15.181  lemma listt_update_in_list [simp, intro!]:
  15.182 -  "[| xs : list n A; x:A |] ==> xs[i := x] : list n A"
  15.183 +  "\<lbrakk> xs : list n A; x:A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
  15.184  apply (unfold list_def)
  15.185  apply simp
  15.186  done 
  15.187 @@ -215,7 +215,7 @@
  15.188  done 
  15.189  
  15.190  lemma plus_list_Cons [simp]:
  15.191 -  "(x#xs) +[f] ys = (case ys of [] => [] | y#ys => (x +_f y)#(xs +[f] ys))"
  15.192 +  "(x#xs) +[f] ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x +_f y)#(xs +[f] ys))"
  15.193    by (simp add: plussub_def map2_def split: list.split)
  15.194  
  15.195  lemma length_plus_list [rule_format, simp]:
  15.196 @@ -227,7 +227,7 @@
  15.197  done
  15.198  
  15.199  lemma nth_plus_list [rule_format, simp]:
  15.200 -  "!xs ys i. length xs = n --> length ys = n --> i<n --> 
  15.201 +  "!xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i<n \<longrightarrow> 
  15.202    (xs +[f] ys)!i = (xs!i) +_f (ys!i)"
  15.203  apply (induct n)
  15.204   apply simp
  15.205 @@ -239,30 +239,30 @@
  15.206  
  15.207  
  15.208  lemma plus_list_ub1 [rule_format]:
  15.209 -  "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |] 
  15.210 -  ==> xs <=[r] xs +[f] ys"
  15.211 +  "\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk> 
  15.212 +  \<Longrightarrow> xs <=[r] xs +[f] ys"
  15.213  apply (unfold unfold_lesub_list)
  15.214  apply (simp add: Listn.le_def list_all2_conv_all_nth)
  15.215  done
  15.216  
  15.217  lemma plus_list_ub2:
  15.218 -  "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |]
  15.219 -  ==> ys <=[r] xs +[f] ys"
  15.220 +  "\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
  15.221 +  \<Longrightarrow> ys <=[r] xs +[f] ys"
  15.222  apply (unfold unfold_lesub_list)
  15.223  apply (simp add: Listn.le_def list_all2_conv_all_nth)
  15.224  done 
  15.225  
  15.226  lemma plus_list_lub [rule_format]:
  15.227 -  "semilat(A,r,f) ==> !xs ys zs. set xs <= A --> set ys <= A --> set zs <= A 
  15.228 -  --> size xs = n & size ys = n --> 
  15.229 -  xs <=[r] zs & ys <=[r] zs --> xs +[f] ys <=[r] zs"
  15.230 +  "semilat(A,r,f) \<Longrightarrow> !xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A 
  15.231 +  \<longrightarrow> size xs = n & size ys = n \<longrightarrow> 
  15.232 +  xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs"
  15.233  apply (unfold unfold_lesub_list)
  15.234  apply (simp add: Listn.le_def list_all2_conv_all_nth)
  15.235  done 
  15.236  
  15.237  lemma list_update_incr [rule_format]:
  15.238 -  "[| semilat(A,r,f); x:A |] ==> set xs <= A --> 
  15.239 -  (!i. i<size xs --> xs <=[r] xs[i := x +_f xs!i])"
  15.240 +  "\<lbrakk> semilat(A,r,f); x:A \<rbrakk> \<Longrightarrow> set xs <= A \<longrightarrow> 
  15.241 +  (!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
  15.242  apply (unfold unfold_lesub_list)
  15.243  apply (simp add: Listn.le_def list_all2_conv_all_nth)
  15.244  apply (induct xs)
  15.245 @@ -273,7 +273,7 @@
  15.246  done 
  15.247  
  15.248  lemma acc_le_listI [intro!]:
  15.249 -  "[| order r; acc r |] ==> acc(Listn.le r)"
  15.250 +  "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
  15.251  apply (unfold acc_def)
  15.252  apply (subgoal_tac
  15.253   "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})")
  15.254 @@ -323,7 +323,7 @@
  15.255  done 
  15.256  
  15.257  lemma closed_listI:
  15.258 -  "closed S f ==> closed (list n S) (map2 f)"
  15.259 +  "closed S f \<Longrightarrow> closed (list n S) (map2 f)"
  15.260  apply (unfold closed_def)
  15.261  apply (induct n)
  15.262   apply simp
  15.263 @@ -335,7 +335,7 @@
  15.264  
  15.265  
  15.266  lemma semilat_Listn_sl:
  15.267 -  "!!L. semilat L ==> semilat (Listn.sl n L)"
  15.268 +  "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
  15.269  apply (unfold Listn.sl_def)
  15.270  apply (simp (no_asm_simp) only: split_tupled_all)
  15.271  apply (simp (no_asm) only: semilat_Def split_conv)
  15.272 @@ -349,7 +349,7 @@
  15.273  
  15.274  
  15.275  lemma coalesce_in_err_list [rule_format]:
  15.276 -  "!xes. xes : list n (err A) --> coalesce xes : err(list n A)"
  15.277 +  "!xes. xes : list n (err A) \<longrightarrow> coalesce xes : err(list n A)"
  15.278  apply (induct n)
  15.279   apply simp
  15.280  apply clarify
  15.281 @@ -359,13 +359,13 @@
  15.282  apply force
  15.283  done 
  15.284  
  15.285 -lemma lem: "!!x xs. x +_(op #) xs = x#xs"
  15.286 +lemma lem: "\<And>x xs. x +_(op #) xs = x#xs"
  15.287    by (simp add: plussub_def)
  15.288  
  15.289  lemma coalesce_eq_OK1_D [rule_format]:
  15.290 -  "semilat(err A, Err.le r, lift2 f) ==> 
  15.291 -  !xs. xs : list n A --> (!ys. ys : list n A --> 
  15.292 -  (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))"
  15.293 +  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
  15.294 +  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
  15.295 +  (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> xs <=[r] zs))"
  15.296  apply (induct n)
  15.297    apply simp
  15.298  apply clarify
  15.299 @@ -376,9 +376,9 @@
  15.300  done
  15.301  
  15.302  lemma coalesce_eq_OK2_D [rule_format]:
  15.303 -  "semilat(err A, Err.le r, lift2 f) ==> 
  15.304 -  !xs. xs : list n A --> (!ys. ys : list n A --> 
  15.305 -  (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))"
  15.306 +  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
  15.307 +  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
  15.308 +  (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> ys <=[r] zs))"
  15.309  apply (induct n)
  15.310   apply simp
  15.311  apply clarify
  15.312 @@ -389,8 +389,8 @@
  15.313  done 
  15.314  
  15.315  lemma lift2_le_ub:
  15.316 -  "[| semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; 
  15.317 -      u:A; x <=_r u; y <=_r u |] ==> z <=_r u"
  15.318 +  "\<lbrakk> semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; 
  15.319 +      u:A; x <=_r u; y <=_r u \<rbrakk> \<Longrightarrow> z <=_r u"
  15.320  apply (unfold semilat_Def plussub_def err_def)
  15.321  apply (simp add: lift2_def)
  15.322  apply clarify
  15.323 @@ -401,10 +401,10 @@
  15.324  done 
  15.325  
  15.326  lemma coalesce_eq_OK_ub_D [rule_format]:
  15.327 -  "semilat(err A, Err.le r, lift2 f) ==> 
  15.328 -  !xs. xs : list n A --> (!ys. ys : list n A --> 
  15.329 +  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
  15.330 +  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
  15.331    (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us 
  15.332 -           & us : list n A --> zs <=[r] us))"
  15.333 +           & us : list n A \<longrightarrow> zs <=[r] us))"
  15.334  apply (induct n)
  15.335   apply simp
  15.336  apply clarify
  15.337 @@ -418,15 +418,15 @@
  15.338  done 
  15.339  
  15.340  lemma lift2_eq_ErrD:
  15.341 -  "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A |] 
  15.342 -  ==> ~(? u:A. x <=_r u & y <=_r u)"
  15.343 +  "\<lbrakk> x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A \<rbrakk> 
  15.344 +  \<Longrightarrow> ~(? u:A. x <=_r u & y <=_r u)"
  15.345    by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])
  15.346  
  15.347  
  15.348  lemma coalesce_eq_Err_D [rule_format]:
  15.349 -  "[| semilat(err A, Err.le r, lift2 f) |] 
  15.350 -  ==> !xs. xs:list n A --> (!ys. ys:list n A --> 
  15.351 -      coalesce (xs +[f] ys) = Err --> 
  15.352 +  "\<lbrakk> semilat(err A, Err.le r, lift2 f) \<rbrakk> 
  15.353 +  \<Longrightarrow> !xs. xs:list n A \<longrightarrow> (!ys. ys:list n A \<longrightarrow> 
  15.354 +      coalesce (xs +[f] ys) = Err \<longrightarrow> 
  15.355        ~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))"
  15.356  apply (induct n)
  15.357   apply simp
  15.358 @@ -445,8 +445,8 @@
  15.359  done 
  15.360  
  15.361  lemma closed_map2_list [rule_format]:
  15.362 -  "closed (err A) (lift2 f) ==> 
  15.363 -  !xs. xs : list n A --> (!ys. ys : list n A --> 
  15.364 +  "closed (err A) (lift2 f) \<Longrightarrow> 
  15.365 +  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
  15.366    map2 f xs ys : list n (err A))"
  15.367  apply (unfold map2_def)
  15.368  apply (induct n)
  15.369 @@ -458,14 +458,14 @@
  15.370  done 
  15.371  
  15.372  lemma closed_lift2_sup:
  15.373 -  "closed (err A) (lift2 f) ==> 
  15.374 +  "closed (err A) (lift2 f) \<Longrightarrow> 
  15.375    closed (err (list n A)) (lift2 (sup f))"
  15.376    by (fastsimp  simp add: closed_def plussub_def sup_def lift2_def
  15.377                            coalesce_in_err_list closed_map2_list
  15.378                  split: err.split)
  15.379  
  15.380  lemma err_semilat_sup:
  15.381 -  "err_semilat (A,r,f) ==> 
  15.382 +  "err_semilat (A,r,f) \<Longrightarrow> 
  15.383    err_semilat (list n A, Listn.le r, sup f)"
  15.384  apply (unfold Err.sl_def)
  15.385  apply (simp only: split_conv)
  15.386 @@ -480,7 +480,7 @@
  15.387  done 
  15.388  
  15.389  lemma err_semilat_upto_esl:
  15.390 -  "!!L. err_semilat L ==> err_semilat(upto_esl m L)"
  15.391 +  "\<And>L. err_semilat L \<Longrightarrow> err_semilat(upto_esl m L)"
  15.392  apply (unfold Listn.upto_esl_def)
  15.393  apply (simp (no_asm_simp) only: split_tupled_all)
  15.394  apply simp
    16.1 --- a/src/HOL/MicroJava/BV/Opt.thy	Sat Mar 02 12:09:23 2002 +0100
    16.2 +++ b/src/HOL/MicroJava/BV/Opt.thy	Sun Mar 03 16:59:08 2002 +0100
    16.3 @@ -11,49 +11,49 @@
    16.4  theory Opt = Err:
    16.5  
    16.6  constdefs
    16.7 - le :: "'a ord => 'a option ord"
    16.8 -"le r o1 o2 == case o2 of None => o1=None |
    16.9 -                              Some y => (case o1 of None => True
   16.10 -                                                  | Some x => x <=_r y)"
   16.11 + le :: "'a ord \<Rightarrow> 'a option ord"
   16.12 +"le r o1 o2 == case o2 of None \<Rightarrow> o1=None |
   16.13 +                              Some y \<Rightarrow> (case o1 of None \<Rightarrow> True
   16.14 +                                                  | Some x \<Rightarrow> x <=_r y)"
   16.15  
   16.16 - opt :: "'a set => 'a option set"
   16.17 + opt :: "'a set \<Rightarrow> 'a option set"
   16.18  "opt A == insert None {x . ? y:A. x = Some y}"
   16.19  
   16.20 - sup :: "'a ebinop => 'a option ebinop"
   16.21 + sup :: "'a ebinop \<Rightarrow> 'a option ebinop"
   16.22  "sup f o1 o2 ==  
   16.23 - case o1 of None => OK o2 | Some x => (case o2 of None => OK o1
   16.24 -     | Some y => (case f x y of Err => Err | OK z => OK (Some z)))"
   16.25 + case o1 of None \<Rightarrow> OK o2 | Some x \<Rightarrow> (case o2 of None \<Rightarrow> OK o1
   16.26 +     | Some y \<Rightarrow> (case f x y of Err \<Rightarrow> Err | OK z \<Rightarrow> OK (Some z)))"
   16.27  
   16.28 - esl :: "'a esl => 'a option esl"
   16.29 + esl :: "'a esl \<Rightarrow> 'a option esl"
   16.30  "esl == %(A,r,f). (opt A, le r, sup f)"
   16.31  
   16.32  lemma unfold_le_opt:
   16.33    "o1 <=_(le r) o2 = 
   16.34 -  (case o2 of None => o1=None | 
   16.35 -              Some y => (case o1 of None => True | Some x => x <=_r y))"
   16.36 +  (case o2 of None \<Rightarrow> o1=None | 
   16.37 +              Some y \<Rightarrow> (case o1 of None \<Rightarrow> True | Some x \<Rightarrow> x <=_r y))"
   16.38  apply (unfold lesub_def le_def)
   16.39  apply (rule refl)
   16.40  done
   16.41  
   16.42  lemma le_opt_refl:
   16.43 -  "order r ==> o1 <=_(le r) o1"
   16.44 +  "order r \<Longrightarrow> o1 <=_(le r) o1"
   16.45  by (simp add: unfold_le_opt split: option.split)
   16.46  
   16.47  lemma le_opt_trans [rule_format]:
   16.48 -  "order r ==> 
   16.49 -   o1 <=_(le r) o2 --> o2 <=_(le r) o3 --> o1 <=_(le r) o3"
   16.50 +  "order r \<Longrightarrow> 
   16.51 +   o1 <=_(le r) o2 \<longrightarrow> o2 <=_(le r) o3 \<longrightarrow> o1 <=_(le r) o3"
   16.52  apply (simp add: unfold_le_opt split: option.split)
   16.53  apply (blast intro: order_trans)
   16.54  done
   16.55  
   16.56  lemma le_opt_antisym [rule_format]:
   16.57 -  "order r ==> o1 <=_(le r) o2 --> o2 <=_(le r) o1 --> o1=o2"
   16.58 +  "order r \<Longrightarrow> o1 <=_(le r) o2 \<longrightarrow> o2 <=_(le r) o1 \<longrightarrow> o1=o2"
   16.59  apply (simp add: unfold_le_opt split: option.split)
   16.60  apply (blast intro: order_antisym)
   16.61  done
   16.62  
   16.63  lemma order_le_opt [intro!,simp]:
   16.64 -  "order r ==> order(le r)"
   16.65 +  "order r \<Longrightarrow> order(le r)"
   16.66  apply (subst order_def)
   16.67  apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
   16.68  done 
   16.69 @@ -102,7 +102,7 @@
   16.70  
   16.71  
   16.72  lemma semilat_opt:
   16.73 -  "!!L. err_semilat L ==> err_semilat (Opt.esl L)"
   16.74 +  "\<And>L. err_semilat L \<Longrightarrow> err_semilat (Opt.esl L)"
   16.75  proof (unfold Opt.esl_def Err.sl_def, simp add: split_tupled_all)
   16.76    
   16.77    fix A r f
   16.78 @@ -141,11 +141,11 @@
   16.79        assume ab: "x = OK a" "y = OK b"
   16.80        
   16.81        with x 
   16.82 -      have a: "!!c. a = Some c ==> c : A"
   16.83 +      have a: "\<And>c. a = Some c \<Longrightarrow> c : A"
   16.84          by (clarsimp simp add: opt_def)
   16.85  
   16.86        from ab y
   16.87 -      have b: "!!d. b = Some d ==> d : A"
   16.88 +      have b: "\<And>d. b = Some d \<Longrightarrow> d : A"
   16.89          by (clarsimp simp add: opt_def)
   16.90        
   16.91        { fix c d assume "a = Some c" "b = Some d"
   16.92 @@ -225,10 +225,10 @@
   16.93          obtain "OK d:err A" "OK e:err A" "OK g:err A"
   16.94            by simp
   16.95          with lub
   16.96 -        have "[| (OK d) <=_(Err.le r) (OK g); (OK e) <=_(Err.le r) (OK g) |]
   16.97 -          ==> (OK d) +_(lift2 f) (OK e) <=_(Err.le r) (OK g)"
   16.98 +        have "\<lbrakk> (OK d) <=_(Err.le r) (OK g); (OK e) <=_(Err.le r) (OK g) \<rbrakk>
   16.99 +          \<Longrightarrow> (OK d) +_(lift2 f) (OK e) <=_(Err.le r) (OK g)"
  16.100            by blast
  16.101 -        hence "[| d <=_r g; e <=_r g |] ==> \<exists>y. d +_f e = OK y \<and> y <=_r g"
  16.102 +        hence "\<lbrakk> d <=_r g; e <=_r g \<rbrakk> \<Longrightarrow> \<exists>y. d +_f e = OK y \<and> y <=_r g"
  16.103            by simp
  16.104  
  16.105          with ok some xyz xz yz
  16.106 @@ -263,14 +263,14 @@
  16.107  done 
  16.108  
  16.109  lemma Top_le_conv:
  16.110 -  "[| order r; top r T |] ==> (T <=_r x) = (x = T)"
  16.111 +  "\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T <=_r x) = (x = T)"
  16.112  apply (unfold top_def)
  16.113  apply (blast intro: order_antisym)
  16.114  done 
  16.115  
  16.116  
  16.117  lemma acc_le_optI [intro!]:
  16.118 -  "acc r ==> acc(le r)"
  16.119 +  "acc r \<Longrightarrow> acc(le r)"
  16.120  apply (unfold acc_def lesub_def le_def lesssub_def)
  16.121  apply (simp add: wf_eq_minimal split: option.split)
  16.122  apply clarify
  16.123 @@ -283,8 +283,8 @@
  16.124  done 
  16.125  
  16.126  lemma option_map_in_optionI:
  16.127 -  "[| ox : opt S; !x:S. ox = Some x --> f x : S |] 
  16.128 -  ==> option_map f ox : opt S";
  16.129 +  "\<lbrakk> ox : opt S; !x:S. ox = Some x \<longrightarrow> f x : S \<rbrakk> 
  16.130 +  \<Longrightarrow> option_map f ox : opt S";
  16.131  apply (unfold option_map_def)
  16.132  apply (simp split: option.split)
  16.133  apply blast
    17.1 --- a/src/HOL/MicroJava/BV/Product.thy	Sat Mar 02 12:09:23 2002 +0100
    17.2 +++ b/src/HOL/MicroJava/BV/Product.thy	Sun Mar 03 16:59:08 2002 +0100
    17.3 @@ -11,16 +11,16 @@
    17.4  theory Product = Err:
    17.5  
    17.6  constdefs
    17.7 - le :: "'a ord => 'b ord => ('a * 'b) ord"
    17.8 + le :: "'a ord \<Rightarrow> 'b ord \<Rightarrow> ('a * 'b) ord"
    17.9  "le rA rB == %(a,b) (a',b'). a <=_rA a' & b <=_rB b'"
   17.10  
   17.11 - sup :: "'a ebinop => 'b ebinop => ('a * 'b)ebinop"
   17.12 + sup :: "'a ebinop \<Rightarrow> 'b ebinop \<Rightarrow> ('a * 'b)ebinop"
   17.13  "sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)"
   17.14  
   17.15 - esl :: "'a esl => 'b esl => ('a * 'b ) esl"
   17.16 + esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl"
   17.17  "esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
   17.18  
   17.19 -syntax "@lesubprod" :: "'a*'b => 'a ord => 'b ord => 'b => bool"
   17.20 +syntax "@lesubprod" :: "'a*'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'b \<Rightarrow> bool"
   17.21         ("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
   17.22  translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
   17.23  
   17.24 @@ -49,7 +49,7 @@
   17.25  
   17.26  
   17.27  lemma acc_le_prodI [intro!]:
   17.28 -  "[| acc rA; acc rB |] ==> acc(Product.le rA rB)"
   17.29 +  "\<lbrakk> acc rA; acc rB \<rbrakk> \<Longrightarrow> acc(Product.le rA rB)"
   17.30  apply (unfold acc_def)
   17.31  apply (rule wf_subset)
   17.32   apply (erule wf_lex_prod)
   17.33 @@ -59,7 +59,7 @@
   17.34  
   17.35  
   17.36  lemma closed_lift2_sup:
   17.37 -  "[| closed (err A) (lift2 f); closed (err B) (lift2 g) |] ==> 
   17.38 +  "\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow> 
   17.39    closed (err(A<*>B)) (lift2(sup f g))";
   17.40  apply (unfold closed_def plussub_def lift2_def err_def sup_def)
   17.41  apply (simp split: err.split)
   17.42 @@ -72,12 +72,12 @@
   17.43  
   17.44  
   17.45  lemma plus_eq_Err_conv [simp]:
   17.46 -  "[| x:A; y:A; semilat(err A, Err.le r, lift2 f) |] 
   17.47 -  ==> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
   17.48 +  "\<lbrakk> x:A; y:A; semilat(err A, Err.le r, lift2 f) \<rbrakk> 
   17.49 +  \<Longrightarrow> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
   17.50  proof -
   17.51    have plus_le_conv2:
   17.52 -    "!!r f z. [| z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
   17.53 -                 OK x +_f OK y <=_r z|] ==> OK x <=_r z \<and> OK y <=_r z"
   17.54 +    "\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
   17.55 +                 OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
   17.56      by (rule plus_le_conv [THEN iffD1])
   17.57    case rule_context
   17.58    thus ?thesis
   17.59 @@ -110,7 +110,7 @@
   17.60  qed
   17.61  
   17.62  lemma err_semilat_Product_esl:
   17.63 -  "!!L1 L2. [| err_semilat L1; err_semilat L2 |] ==> err_semilat(Product.esl L1 L2)"
   17.64 +  "\<And>L1 L2. \<lbrakk> err_semilat L1; err_semilat L2 \<rbrakk> \<Longrightarrow> err_semilat(Product.esl L1 L2)"
   17.65  apply (unfold esl_def Err.sl_def)
   17.66  apply (simp (no_asm_simp) only: split_tupled_all)
   17.67  apply simp
    18.1 --- a/src/HOL/MicroJava/BV/Semilat.thy	Sat Mar 02 12:09:23 2002 +0100
    18.2 +++ b/src/HOL/MicroJava/BV/Semilat.thy	Sun Mar 03 16:59:08 2002 +0100
    18.3 @@ -13,134 +13,134 @@
    18.4  
    18.5  theory Semilat = While_Combinator:
    18.6  
    18.7 -types 'a ord    = "'a => 'a => bool"
    18.8 -      'a binop  = "'a => 'a => 'a"
    18.9 +types 'a ord    = "'a \<Rightarrow> 'a \<Rightarrow> bool"
   18.10 +      'a binop  = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   18.11        'a sl     = "'a set * 'a ord * 'a binop"
   18.12  
   18.13  consts
   18.14 - "@lesub"   :: "'a => 'a ord => 'a => bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
   18.15 - "@lesssub" :: "'a => 'a ord => 'a => bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
   18.16 + "@lesub"   :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
   18.17 + "@lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
   18.18  defs
   18.19  lesub_def:   "x <=_r y == r x y"
   18.20  lesssub_def: "x <_r y  == x <=_r y & x ~= y"
   18.21  
   18.22  consts
   18.23 - "@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
   18.24 + "@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
   18.25  defs
   18.26  plussub_def: "x +_f y == f x y"
   18.27  
   18.28  
   18.29  constdefs
   18.30 - ord :: "('a*'a)set => 'a ord"
   18.31 + ord :: "('a*'a)set \<Rightarrow> 'a ord"
   18.32  "ord r == %x y. (x,y):r"
   18.33  
   18.34 - order :: "'a ord => bool"
   18.35 + order :: "'a ord \<Rightarrow> bool"
   18.36  "order r == (!x. x <=_r x) &
   18.37 -            (!x y. x <=_r y & y <=_r x --> x=y) &
   18.38 -            (!x y z. x <=_r y & y <=_r z --> x <=_r z)"
   18.39 +            (!x y. x <=_r y & y <=_r x \<longrightarrow> x=y) &
   18.40 +            (!x y z. x <=_r y & y <=_r z \<longrightarrow> x <=_r z)"
   18.41  
   18.42 - acc :: "'a ord => bool"
   18.43 + acc :: "'a ord \<Rightarrow> bool"
   18.44  "acc r == wf{(y,x) . x <_r y}"
   18.45  
   18.46 - top :: "'a ord => 'a => bool"
   18.47 + top :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool"
   18.48  "top r T == !x. x <=_r T"
   18.49  
   18.50 - closed :: "'a set => 'a binop => bool"
   18.51 + closed :: "'a set \<Rightarrow> 'a binop \<Rightarrow> bool"
   18.52  "closed A f == !x:A. !y:A. x +_f y : A"
   18.53  
   18.54 - semilat :: "'a sl => bool"
   18.55 + semilat :: "'a sl \<Rightarrow> bool"
   18.56  "semilat == %(A,r,f). order r & closed A f &
   18.57                  (!x:A. !y:A. x <=_r x +_f y)  &
   18.58                  (!x:A. !y:A. y <=_r x +_f y)  &
   18.59 -                (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
   18.60 +                (!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)"
   18.61  
   18.62 - is_ub :: "('a*'a)set => 'a => 'a => 'a => bool"
   18.63 + is_ub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   18.64  "is_ub r x y u == (x,u):r & (y,u):r"
   18.65  
   18.66 - is_lub :: "('a*'a)set => 'a => 'a => 'a => bool"
   18.67 -"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
   18.68 + is_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   18.69 +"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
   18.70  
   18.71 - some_lub :: "('a*'a)set => 'a => 'a => 'a"
   18.72 + some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   18.73  "some_lub r x y == SOME z. is_lub r x y z"
   18.74  
   18.75  
   18.76  lemma order_refl [simp, intro]:
   18.77 -  "order r ==> x <=_r x";
   18.78 +  "order r \<Longrightarrow> x <=_r x";
   18.79    by (simp add: order_def)
   18.80  
   18.81  lemma order_antisym:
   18.82 -  "[| order r; x <=_r y; y <=_r x |] ==> x = y"
   18.83 +  "\<lbrakk> order r; x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y"
   18.84  apply (unfold order_def)
   18.85  apply (simp (no_asm_simp))  
   18.86  done
   18.87  
   18.88  lemma order_trans:
   18.89 -   "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z"
   18.90 +   "\<lbrakk> order r; x <=_r y; y <=_r z \<rbrakk> \<Longrightarrow> x <=_r z"
   18.91  apply (unfold order_def)
   18.92  apply blast
   18.93  done 
   18.94  
   18.95  lemma order_less_irrefl [intro, simp]:
   18.96 -   "order r ==> ~ x <_r x"
   18.97 +   "order r \<Longrightarrow> ~ x <_r x"
   18.98  apply (unfold order_def lesssub_def)
   18.99  apply blast
  18.100  done 
  18.101  
  18.102  lemma order_less_trans:
  18.103 -  "[| order r; x <_r y; y <_r z |] ==> x <_r z"
  18.104 +  "\<lbrakk> order r; x <_r y; y <_r z \<rbrakk> \<Longrightarrow> x <_r z"
  18.105  apply (unfold order_def lesssub_def)
  18.106  apply blast
  18.107  done 
  18.108  
  18.109  lemma topD [simp, intro]:
  18.110 -  "top r T ==> x <=_r T"
  18.111 +  "top r T \<Longrightarrow> x <=_r T"
  18.112    by (simp add: top_def)
  18.113  
  18.114  lemma top_le_conv [simp]:
  18.115 -  "[| order r; top r T |] ==> (T <=_r x) = (x = T)"
  18.116 +  "\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T <=_r x) = (x = T)"
  18.117    by (blast intro: order_antisym)
  18.118  
  18.119  lemma semilat_Def:
  18.120  "semilat(A,r,f) == order r & closed A f & 
  18.121                   (!x:A. !y:A. x <=_r x +_f y) & 
  18.122                   (!x:A. !y:A. y <=_r x +_f y) & 
  18.123 -                 (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
  18.124 +                 (!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)"
  18.125  apply (unfold semilat_def split_conv [THEN eq_reflection])
  18.126  apply (rule refl [THEN eq_reflection])
  18.127  done
  18.128  
  18.129  lemma semilatDorderI [simp, intro]:
  18.130 -  "semilat(A,r,f) ==> order r"
  18.131 +  "semilat(A,r,f) \<Longrightarrow> order r"
  18.132    by (simp add: semilat_Def)
  18.133  
  18.134  lemma semilatDclosedI [simp, intro]:
  18.135 -  "semilat(A,r,f) ==> closed A f"
  18.136 +  "semilat(A,r,f) \<Longrightarrow> closed A f"
  18.137  apply (unfold semilat_Def)
  18.138  apply simp
  18.139  done
  18.140  
  18.141  lemma semilat_ub1 [simp]:
  18.142 -  "[| semilat(A,r,f); x:A; y:A |] ==> x <=_r x +_f y"
  18.143 +  "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
  18.144    by (unfold semilat_Def, simp)
  18.145  
  18.146  lemma semilat_ub2 [simp]:
  18.147 -  "[| semilat(A,r,f); x:A; y:A |] ==> y <=_r x +_f y"
  18.148 +  "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
  18.149    by (unfold semilat_Def, simp)
  18.150  
  18.151  lemma semilat_lub [simp]:
  18.152 - "[| x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A |] ==> x +_f y <=_r z";
  18.153 + "\<lbrakk> x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z";
  18.154    by (unfold semilat_Def, simp)
  18.155  
  18.156  
  18.157  lemma plus_le_conv [simp]:
  18.158 -  "[| x:A; y:A; z:A; semilat(A,r,f) |] 
  18.159 -  ==> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
  18.160 +  "\<lbrakk> x:A; y:A; z:A; semilat(A,r,f) \<rbrakk> 
  18.161 +  \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
  18.162  apply (unfold semilat_Def)
  18.163  apply (blast intro: semilat_ub1 semilat_ub2 semilat_lub order_trans)
  18.164  done
  18.165  
  18.166  lemma le_iff_plus_unchanged:
  18.167 -  "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (x +_f y = y)"
  18.168 +  "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)"
  18.169  apply (rule iffI)
  18.170   apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub2, assumption+)
  18.171  apply (erule subst)
  18.172 @@ -148,7 +148,7 @@
  18.173  done 
  18.174  
  18.175  lemma le_iff_plus_unchanged2:
  18.176 -  "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (y +_f x = y)"
  18.177 +  "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)"
  18.178  apply (rule iffI)
  18.179   apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub1, assumption+)
  18.180  apply (erule subst)
  18.181 @@ -157,7 +157,7 @@
  18.182  
  18.183  
  18.184  lemma closedD:
  18.185 -  "[| closed A f; x:A; y:A |] ==> x +_f y : A"
  18.186 +  "\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A"
  18.187  apply (unfold closed_def)
  18.188  apply blast
  18.189  done 
  18.190 @@ -167,15 +167,15 @@
  18.191  
  18.192  
  18.193  lemma is_lubD:
  18.194 -  "is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
  18.195 +  "is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
  18.196    by (simp add: is_lub_def)
  18.197  
  18.198  lemma is_ubI:
  18.199 -  "[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u"
  18.200 +  "\<lbrakk> (x,u) : r; (y,u) : r \<rbrakk> \<Longrightarrow> is_ub r x y u"
  18.201    by (simp add: is_ub_def)
  18.202  
  18.203  lemma is_ubD:
  18.204 -  "is_ub r x y u ==> (x,u) : r & (y,u) : r"
  18.205 +  "is_ub r x y u \<Longrightarrow> (x,u) : r & (y,u) : r"
  18.206    by (simp add: is_ub_def)
  18.207  
  18.208  
  18.209 @@ -192,8 +192,8 @@
  18.210  done
  18.211  
  18.212  lemma extend_lub:
  18.213 -  "[| single_valued r; is_lub (r^* ) x y u; (x',x) : r |] 
  18.214 -  ==> EX v. is_lub (r^* ) x' y v"
  18.215 +  "\<lbrakk> single_valued r; is_lub (r^* ) x y u; (x',x) : r \<rbrakk> 
  18.216 +  \<Longrightarrow> EX v. is_lub (r^* ) x' y v"
  18.217  apply (unfold is_lub_def is_ub_def)
  18.218  apply (case_tac "(y,x) : r^*")
  18.219   apply (case_tac "(y,x') : r^*")
  18.220 @@ -207,7 +207,7 @@
  18.221  done
  18.222  
  18.223  lemma single_valued_has_lubs [rule_format]:
  18.224 -  "[| single_valued r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> 
  18.225 +  "\<lbrakk> single_valued r; (x,u) : r^* \<rbrakk> \<Longrightarrow> (!y. (y,u) : r^* \<longrightarrow> 
  18.226    (EX z. is_lub (r^* ) x y z))"
  18.227  apply (erule converse_rtrancl_induct)
  18.228   apply clarify
  18.229 @@ -218,7 +218,7 @@
  18.230  done
  18.231  
  18.232  lemma some_lub_conv:
  18.233 -  "[| acyclic r; is_lub (r^* ) x y u |] ==> some_lub (r^* ) x y = u"
  18.234 +  "\<lbrakk> acyclic r; is_lub (r^* ) x y u \<rbrakk> \<Longrightarrow> some_lub (r^* ) x y = u"
  18.235  apply (unfold some_lub_def is_lub_def)
  18.236  apply (rule someI2)
  18.237   apply assumption
  18.238 @@ -226,8 +226,8 @@
  18.239  done
  18.240  
  18.241  lemma is_lub_some_lub:
  18.242 -  "[| single_valued r; acyclic r; (x,u):r^*; (y,u):r^* |] 
  18.243 -  ==> is_lub (r^* ) x y (some_lub (r^* ) x y)";
  18.244 +  "\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^* \<rbrakk> 
  18.245 +  \<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)";
  18.246    by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv)
  18.247  
  18.248  subsection{*An executable lub-finder*}
    19.1 --- a/src/HOL/MicroJava/BV/Typing_Framework.thy	Sat Mar 02 12:09:23 2002 +0100
    19.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework.thy	Sun Mar 03 16:59:08 2002 +0100
    19.3 @@ -15,23 +15,23 @@
    19.4    's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
    19.5  
    19.6  constdefs
    19.7 - bounded :: "'s step_type => nat => bool"
    19.8 + bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
    19.9  "bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"  
   19.10  
   19.11 - stable :: "'s ord => 's step_type => 's list => nat => bool"
   19.12 + stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool"
   19.13  "stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"
   19.14  
   19.15 - stables :: "'s ord => 's step_type => 's list => bool"
   19.16 + stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
   19.17  "stables r step ss == !p<size ss. stable r step ss p"
   19.18  
   19.19 - is_bcv :: "'s ord => 's => 's step_type 
   19.20 -           => nat => 's set => ('s list => 's list) => bool"  
   19.21 + is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type 
   19.22 +           \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool"  
   19.23  "is_bcv r T step n A bcv == !ss : list n A.
   19.24     (!p<n. (bcv ss)!p ~= T) =
   19.25     (? ts: list n A. ss <=[r] ts & wt_step r T step ts)"
   19.26  
   19.27   wt_step ::
   19.28 -"'s ord => 's => 's step_type => 's list => bool"
   19.29 +"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
   19.30  "wt_step r T step ts ==
   19.31   !p<size(ts). ts!p ~= T & stable r step ts p"
   19.32  
    20.1 --- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Sat Mar 02 12:09:23 2002 +0100
    20.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Sun Mar 03 16:59:08 2002 +0100
    20.3 @@ -11,10 +11,10 @@
    20.4  
    20.5  constdefs
    20.6  
    20.7 -dynamic_wt :: "'s ord => 's err step_type => 's err list => bool"
    20.8 +dynamic_wt :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool"
    20.9  "dynamic_wt r step ts == wt_step (Err.le r) Err step ts"
   20.10  
   20.11 -static_wt :: "'s ord => (nat => 's => bool) => 's step_type => 's list => bool"
   20.12 +static_wt :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
   20.13  "static_wt r app step ts == 
   20.14    \<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)"
   20.15  
   20.16 @@ -28,14 +28,14 @@
   20.17  "err_step app step p t == case t of Err \<Rightarrow> map_err (step p arbitrary) | OK t' \<Rightarrow> 
   20.18    if app p t' then map_snd OK (step p t') else map_err (step p t')"
   20.19  
   20.20 -non_empty :: "'s step_type => bool"
   20.21 +non_empty :: "'s step_type \<Rightarrow> bool"
   20.22  "non_empty step == \<forall>p t. step p t \<noteq> []"
   20.23  
   20.24  
   20.25  lemmas err_step_defs = err_step_def map_snd_def map_err_def
   20.26  
   20.27  lemma non_emptyD:
   20.28 -  "non_empty step ==> \<exists>q t'. (q,t') \<in> set(step p t)"
   20.29 +  "non_empty step \<Longrightarrow> \<exists>q t'. (q,t') \<in> set(step p t)"
   20.30  proof (unfold non_empty_def)
   20.31    assume "\<forall>p t. step p t \<noteq> []"
   20.32    hence "step p t \<noteq> []" by blast
   20.33 @@ -47,9 +47,9 @@
   20.34  
   20.35  
   20.36  lemma dynamic_imp_static:
   20.37 -  "[| bounded step (size ts); non_empty step;
   20.38 -      dynamic_wt r (err_step app step) ts |] 
   20.39 -  ==> static_wt r app step (map ok_val ts)"
   20.40 +  "\<lbrakk> bounded step (size ts); non_empty step;
   20.41 +      dynamic_wt r (err_step app step) ts \<rbrakk> 
   20.42 +  \<Longrightarrow> static_wt r app step (map ok_val ts)"
   20.43  proof (unfold static_wt_def, intro strip, rule conjI)
   20.44  
   20.45    assume b:  "bounded step (size ts)"
   20.46 @@ -112,8 +112,8 @@
   20.47  
   20.48  
   20.49  lemma static_imp_dynamic:
   20.50 -  "[| static_wt r app step ts; bounded step (size ts) |] 
   20.51 -  ==> dynamic_wt r (err_step app step) (map OK ts)"
   20.52 +  "\<lbrakk> static_wt r app step ts; bounded step (size ts) \<rbrakk> 
   20.53 +  \<Longrightarrow> dynamic_wt r (err_step app step) (map OK ts)"
   20.54  proof (unfold dynamic_wt_def wt_step_def, intro strip, rule conjI)
   20.55    assume bounded: "bounded step (size ts)"
   20.56    assume static:  "static_wt r app step ts"
    21.1 --- a/src/HOL/MicroJava/JVM/JVMExec.thy	Sat Mar 02 12:09:23 2002 +0100
    21.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Sun Mar 03 16:59:08 2002 +0100
    21.3 @@ -34,6 +34,6 @@
    21.4  
    21.5  syntax (xsymbols)
    21.6    exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
    21.7 -              ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
    21.8 +              ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
    21.9  
   21.10  end