--- a/src/HOL/MicroJava/BV/BVExample.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Sun Mar 03 16:59:08 2002 +0100
@@ -276,8 +276,7 @@
apply simp
done
-text {* Some shorthands to make the welltyping of method @{term
-makelist_name} easier to read *}
+text {* Some abbreviations for readability *}
syntax
list :: ty
test :: ty
@@ -382,4 +381,4 @@
apply (simp add: conf_def start_heap_def)
done
-end
\ No newline at end of file
+end
--- a/src/HOL/MicroJava/BV/BVSpec.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Sun Mar 03 16:59:08 2002 +0100
@@ -17,42 +17,42 @@
constdefs
wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
- exception_table,p_count] => bool"
+ exception_table,p_count] \<Rightarrow> bool"
"wt_instr i G rT phi mxs max_pc et pc ==
app i G mxs rT pc et (phi!pc) \<and>
(\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
- wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
+ wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
"wt_start G C pTs mxl phi ==
G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
- exception_table,method_type] => bool"
+ exception_table,method_type] \<Rightarrow> bool"
"wt_method G C pTs rT mxs mxl ins et phi ==
let max_pc = length ins in
0 < max_pc \<and> wt_start G C pTs mxl phi \<and>
- (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc et pc)"
+ (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins ! pc) G rT phi mxs max_pc et pc)"
- wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
+ wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
"wt_jvm_prog G phi ==
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"
lemma wt_jvm_progD:
- "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
+ "wt_jvm_prog G phi \<Longrightarrow> (\<exists>wt. wf_prog wt G)"
by (unfold wt_jvm_prog_def, blast)
lemma wt_jvm_prog_impl_wt_instr:
- "[| wt_jvm_prog G phi; is_class G C;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins |]
- ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc";
+ "\<lbrakk> wt_jvm_prog G phi; is_class G C;
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins \<rbrakk>
+ \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc";
by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
simp, simp, simp add: wf_mdecl_def wt_method_def)
lemma wt_jvm_prog_impl_wt_start:
- "[| wt_jvm_prog G phi; is_class G C;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) |] ==>
+ "\<lbrakk> wt_jvm_prog G phi; is_class G C;
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) \<rbrakk> \<Longrightarrow>
0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
simp, simp, simp add: wf_mdecl_def wt_method_def)
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sun Mar 03 16:59:08 2002 +0100
@@ -31,9 +31,9 @@
can directly infer that the current instruction is well typed:
*}
lemma wt_jvm_prog_impl_wt_instr_cor:
- "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
- ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
+ "\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+ \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
apply (unfold correct_state_def Let_def correct_frame_def)
apply simp
apply (blast intro: wt_jvm_prog_impl_wt_instr)
@@ -57,10 +57,10 @@
@{text match_exception_table} from the operational semantics:
*}
lemma in_match_any:
- "match_exception_table G xcpt pc et = Some pc' ==>
+ "match_exception_table G xcpt pc et = Some pc' \<Longrightarrow>
\<exists>C. C \<in> set (match_any G pc et) \<and> G \<turnstile> xcpt \<preceq>C C \<and>
match_exception_table G C pc et = Some pc'"
- (is "PROP ?P et" is "?match et ==> ?match_any et")
+ (is "PROP ?P et" is "?match et \<Longrightarrow> ?match_any et")
proof (induct et)
show "PROP ?P []"
by simp
@@ -131,10 +131,10 @@
conforms.
*}
lemma uncaught_xcpt_correct:
- "!!f. [| wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T;
- G,phi \<turnstile>JVM (None, hp, f#frs)\<surd> |]
- ==> G,phi \<turnstile>JVM (find_handler G (Some xcp) hp frs)\<surd>"
- (is "!!f. [| ?wt; ?adr; ?hp; ?correct (None, hp, f#frs) |] ==> ?correct (?find frs)")
+ "\<And>f. \<lbrakk> wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T;
+ G,phi \<turnstile>JVM (None, hp, f#frs)\<surd> \<rbrakk>
+ \<Longrightarrow> G,phi \<turnstile>JVM (find_handler G (Some xcp) hp frs)\<surd>"
+ (is "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?correct (None, hp, f#frs) \<rbrakk> \<Longrightarrow> ?correct (?find frs)")
proof (induct frs)
-- "the base case is trivial, as it should be"
show "?correct (?find [])" by (simp add: correct_state_def)
@@ -153,9 +153,9 @@
-- "the induction hypothesis as produced by Isabelle, immediatly simplified
with the fixed assumptions above"
- assume "\<And>f. [| ?wt; ?adr; ?hp; ?correct (None, hp, f#frs') |] ==> ?correct (?find frs')"
+ assume "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?correct (None, hp, f#frs') \<rbrakk> \<Longrightarrow> ?correct (?find frs')"
with wt adr hp
- have IH: "\<And>f. ?correct (None, hp, f#frs') ==> ?correct (?find frs')" by blast
+ have IH: "\<And>f. ?correct (None, hp, f#frs') \<Longrightarrow> ?correct (?find frs')" by blast
from cr
have cr': "?correct (None, hp, f'#frs')" by (auto simp add: correct_state_def)
@@ -249,11 +249,11 @@
for welltyped instructions and conformant states:
*}
lemma exec_instr_xcpt_hp:
- "[| fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp;
+ "\<lbrakk> fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
- ==> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T"
- (is "[| ?xcpt; ?wt; ?correct |] ==> ?thesis")
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+ \<Longrightarrow> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T"
+ (is "\<lbrakk> ?xcpt; ?wt; ?correct \<rbrakk> \<Longrightarrow> ?thesis")
proof -
note [simp] = split_beta raise_system_xcpt_def
note [split] = split_if_asm option.split_asm
@@ -279,13 +279,13 @@
resulting next state always conforms:
*}
lemma xcpt_correct:
- "[| wt_jvm_prog G phi;
+ "\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
- ==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+ \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wtp: "wt_jvm_prog G phi"
assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
@@ -588,47 +588,47 @@
lemmas [iff] = not_Err_eq
lemma Load_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Load idx;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (blast intro: approx_loc_imp_approx_val_sup)
done
lemma Store_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Store idx;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (blast intro: approx_loc_subst)
done
lemma LitPush_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = LitPush v;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 sup_PTS_eq map_eq_Cons)
apply (blast dest: conf_litval intro: conf_widen)
done
lemma Cast_conf2:
- "[| wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v;
- G\<turnstile>Class C\<preceq>T; is_class G C|]
- ==> G,h\<turnstile>v::\<preceq>T"
+ "\<lbrakk> wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v;
+ G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk>
+ \<Longrightarrow> G,h\<turnstile>v::\<preceq>T"
apply (unfold cast_ok_def)
apply (frule widen_Class)
apply (elim exE disjE)
@@ -641,28 +641,28 @@
lemmas defs1 = defs1 raise_system_xcpt_def
lemma Checkcast_correct:
-"[| wt_jvm_prog G phi;
+"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Checkcast D;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
- fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 wt_jvm_prog_def map_eq_Cons split: split_if_asm)
apply (blast intro: Cast_conf2)
done
lemma Getfield_correct:
-"[| wt_jvm_prog G phi;
+"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Getfield F D;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
- fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons wt_jvm_prog_def
split: option.split split_if_asm)
apply (frule conf_widen)
@@ -687,14 +687,14 @@
lemma Putfield_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Putfield F D;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
- fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 split_beta split: option.split List.split split_if_asm)
apply (frule conf_widen)
prefer 2
@@ -715,14 +715,14 @@
lemma New_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = New X;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
- fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wf: "wf_prog wt G"
assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
@@ -793,14 +793,14 @@
lemma Invoke_correct:
-"[| wt_jvm_prog G phi;
+"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Invoke C' mn pTs;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
- fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wtprog: "wt_jvm_prog G phi"
assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
@@ -972,13 +972,13 @@
lemmas [simp del] = map_append
lemma Return_correct:
-"[| wt_jvm_prog G phi;
+"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Return;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wt_prog: "wt_jvm_prog G phi"
assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
@@ -1098,110 +1098,110 @@
lemmas [simp] = map_append
lemma Goto_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Goto branch;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1)
apply fast
done
lemma Ifcmpeq_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Ifcmpeq branch;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1)
apply fast
done
lemma Pop_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Pop;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1)
apply fast
done
lemma Dup_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Dup;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (blast intro: conf_widen)
done
lemma Dup_x1_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Dup_x1;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (blast intro: conf_widen)
done
lemma Dup_x2_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Dup_x2;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (blast intro: conf_widen)
done
lemma Swap_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Swap;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (blast intro: conf_widen)
done
lemma IAdd_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = IAdd;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
apply blast
done
lemma Throw_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Throw;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
- fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
by simp
@@ -1213,11 +1213,11 @@
into another conforming state when one instruction is executed.
*}
theorem instr_correct:
-"[| wt_jvm_prog G phi;
+"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (frule wt_jvm_prog_impl_wt_instr_cor)
apply assumption+
apply (cases "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs)")
@@ -1254,13 +1254,13 @@
lemma correct_state_impl_Some_method:
"G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>
- ==> \<exists>meth. method (G,C) sig = Some(C,meth)"
+ \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
by (auto simp add: correct_state_def Let_def)
lemma BV_correct_1 [rule_format]:
-"!!state. [| wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>|]
- ==> exec (G,state) = Some state' --> G,phi \<turnstile>JVM state'\<surd>"
+"\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk>
+ \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (simp only: split_tupled_all)
apply (rename_tac xp hp frs)
apply (case_tac xp)
@@ -1277,19 +1277,19 @@
lemma L0:
- "[| xp=None; frs\<noteq>[] |] ==> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
+ "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
by (clarsimp simp add: neq_Nil_conv split_beta)
lemma L1:
- "[|wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]|]
- ==> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
+ "\<lbrakk>wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]\<rbrakk>
+ \<Longrightarrow> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
apply (drule L0)
apply assumption
apply (fast intro: BV_correct_1)
done
theorem BV_correct [rule_format]:
-"[| wt_jvm_prog G phi; G \<turnstile> s -jvm-> t |] ==> G,phi \<turnstile>JVM s\<surd> --> G,phi \<turnstile>JVM t\<surd>"
+"\<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>"
apply (unfold exec_all_def)
apply (erule rtrancl_induct)
apply simp
@@ -1297,9 +1297,9 @@
done
theorem BV_correct_implies_approx:
-"[| wt_jvm_prog G phi;
- G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|]
-==> approx_stk G hp stk (fst (the (phi C sig ! pc))) \<and>
+"\<lbrakk> wt_jvm_prog G phi;
+ G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk>
+\<Longrightarrow> approx_stk G hp stk (fst (the (phi C sig ! pc))) \<and>
approx_loc G hp loc (snd (the (phi C sig ! pc)))"
apply (drule BV_correct)
apply assumption+
--- a/src/HOL/MicroJava/BV/Correct.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Sun Mar 03 16:59:08 2002 +0100
@@ -12,23 +12,23 @@
theory Correct = BVSpec + JVMExec:
constdefs
- approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
- "approx_val G h v any == case any of Err => True | OK T => G,h\<turnstile>v::\<preceq>T"
+ approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
+ "approx_val G h v any == case any of Err \<Rightarrow> True | OK T \<Rightarrow> G,h\<turnstile>v::\<preceq>T"
- approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
+ approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool"
"approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
- approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
+ approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool"
"approx_stk G hp stk ST == approx_loc G hp stk (map OK ST)"
- correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool"
+ correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
"correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
approx_stk G hp stk ST \<and> approx_loc G hp loc LT \<and>
pc < length ins \<and> length loc=length(snd sig)+maxl+1"
consts
- correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool"
+ correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool"
primrec
"correct_frames G hp phi rT0 sig0 [] = True"
@@ -50,13 +50,13 @@
constdefs
- correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
+ correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
("_,_ |-JVM _ [ok]" [51,51] 50)
"correct_state G phi == \<lambda>(xp,hp,frs).
case xp of
- None => (case frs of
- [] => True
- | (f#fs) => G\<turnstile>h hp\<surd> \<and> preallocated hp \<and>
+ None \<Rightarrow> (case frs of
+ [] \<Rightarrow> True
+ | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and> preallocated hp \<and>
(let (stk,loc,C,sig,pc) = f
in
\<exists>rT maxs maxl ins et s.
@@ -65,11 +65,11 @@
phi C sig ! pc = Some s \<and>
correct_frame G hp s maxl ins f \<and>
correct_frames G hp phi rT sig fs))
- | Some x => frs = []"
+ | Some x \<Rightarrow> frs = []"
syntax (xsymbols)
- correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
+ correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50)
@@ -99,8 +99,8 @@
by (cases T) (blast intro: conf_hext)+
lemma approx_val_heap_update:
- "[| hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|]
- ==> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
+ "\<lbrakk> hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk>
+ \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
by (cases v, auto simp add: obj_ty_def conf_def)
lemma approx_val_widen:
@@ -228,8 +228,8 @@
section {* oconf *}
lemma oconf_field_update:
- "[|map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> |]
- ==> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
+ "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
+ \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
by (simp add: oconf_def lconf_def)
lemma oconf_newref:
@@ -290,11 +290,11 @@
lemma correct_frames_field_update [rule_format]:
"\<forall>rT C sig.
- correct_frames G hp phi rT sig frs -->
- hp a = Some (C,fs) -->
- map_of (fields (G, C)) fl = Some fd -->
+ correct_frames G hp phi rT sig frs \<longrightarrow>
+ hp a = Some (C,fs) \<longrightarrow>
+ map_of (fields (G, C)) fl = Some fd \<longrightarrow>
G,hp\<turnstile>v::\<preceq>fd
- --> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs";
+ \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs";
apply (induct frs)
apply simp
apply clarify
--- a/src/HOL/MicroJava/BV/Effect.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Sun Mar 03 16:59:08 2002 +0100
@@ -13,7 +13,7 @@
text {* Program counter of successor instructions: *}
consts
- succs :: "instr => p_count => p_count list"
+ succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list"
primrec
"succs (Load idx) pc = [pc+1]"
"succs (Store idx) pc = [pc+1]"
@@ -36,7 +36,7 @@
text "Effect of instruction on the state type:"
consts
-eff' :: "instr \<times> jvm_prog \<times> state_type => state_type"
+eff' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
recdef eff' "{}"
"eff' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)"
@@ -84,7 +84,7 @@
by (induct et) auto
consts
- xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table => cname list"
+ xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table \<Rightarrow> cname list"
recdef xcpt_names "{}"
"xcpt_names (Getfield F C, G, pc, et) = match G (Xcpt NullPointer) pc et"
"xcpt_names (Putfield F C, G, pc, et) = match G (Xcpt NullPointer) pc et"
@@ -104,7 +104,7 @@
norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"
"norm_eff i G == option_map (\<lambda>s. eff' (i,G,s))"
- eff :: "instr => jvm_prog => p_count => exception_table => state_type option => succ_type"
+ eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> succ_type"
"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)"
constdefs
@@ -127,7 +127,7 @@
text "Conditions under which eff is applicable:"
consts
-app' :: "instr \<times> jvm_prog \<times> p_count \<times> nat \<times> ty \<times> state_type => bool"
+app' :: "instr \<times> jvm_prog \<times> p_count \<times> nat \<times> ty \<times> state_type \<Rightarrow> bool"
recdef app' "{}"
"app' (Load idx, G, pc, maxs, rT, s) =
@@ -180,17 +180,17 @@
xcpt_app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> bool"
"xcpt_app i G pc et \<equiv> \<forall>C\<in>set(xcpt_names (i,G,pc,et)). is_class G C"
- app :: "instr => jvm_prog => nat => ty => nat => exception_table => state_type option => bool"
- "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"
+ app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> bool"
+ "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"
-lemma 1: "2 < length a ==> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
+lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
proof (cases a)
fix x xs assume "a = x#xs" "2 < length a"
thus ?thesis by - (cases xs, simp, cases "tl xs", auto)
qed auto
-lemma 2: "\<not>(2 < length a) ==> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
+lemma 2: "\<not>(2 < length a) \<Longrightarrow> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
proof -;
assume "\<not>(2 < length a)"
hence "length a < (Suc (Suc (Suc 0)))" by simp
@@ -203,7 +203,7 @@
hence "\<exists> l. x = [l]" by - (cases x, auto)
} note 0 = this
- have "length a = Suc (Suc 0) ==> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
+ have "length a = Suc (Suc 0) \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
with * show ?thesis by (auto dest: 0)
qed
@@ -337,7 +337,7 @@
proof (cases (open) s)
note list_all2_def [simp]
case Pair
- have "?app (a,b) ==> ?P (a,b)"
+ have "?app (a,b) \<Longrightarrow> ?P (a,b)"
proof -
assume app: "?app (a,b)"
hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and>
--- a/src/HOL/MicroJava/BV/EffectMono.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy Sun Mar 03 16:59:08 2002 +0100
@@ -14,7 +14,7 @@
lemma sup_loc_some [rule_format]:
-"\<forall>y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = OK t -->
+"\<forall>y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = OK t \<longrightarrow>
(\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
proof (induct (open) ?P b)
show "?P []" by simp
@@ -41,9 +41,9 @@
lemma all_widen_is_sup_loc:
-"\<forall>b. length a = length b -->
+"\<forall>b. length a = length b \<longrightarrow>
(\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map OK a) <=l (map OK b))"
- (is "\<forall>b. length a = length b --> ?Q a b" is "?P a")
+ (is "\<forall>b. length a = length b \<longrightarrow> ?Q a b" is "?P a")
proof (induct "a")
show "?P []" by simp
@@ -60,7 +60,7 @@
lemma append_length_n [rule_format]:
-"\<forall>n. n \<le> length x --> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
+"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
proof (induct (open) ?P x)
show "?P []" by simp
@@ -86,7 +86,7 @@
qed
lemma rev_append_cons:
-"n < length x ==> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
+"n < length x \<Longrightarrow> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
proof -
assume n: "n < length x"
hence "n \<le> length x" by simp
@@ -109,7 +109,7 @@
lemmas [iff] = not_Err_eq
lemma app_mono:
-"[|G \<turnstile> s <=' s'; app i G m rT pc et s'|] ==> app i G m rT pc et s"
+"\<lbrakk>G \<turnstile> s <=' s'; app i G m rT pc et s'\<rbrakk> \<Longrightarrow> app i G m rT pc et s"
proof -
{ fix s1 s2
@@ -281,7 +281,7 @@
lemmas [simp del] = split_paired_Ex
lemma eff'_mono:
-"[| app i G m rT pc et (Some s2); G \<turnstile> s1 <=s s2 |] ==>
+"\<lbrakk> app i G m rT pc et (Some s2); G \<turnstile> s1 <=s s2 \<rbrakk> \<Longrightarrow>
G \<turnstile> eff' (i,G,s1) <=s eff' (i,G,s2)"
proof (cases s1, cases s2)
fix a1 b1 a2 b2
--- a/src/HOL/MicroJava/BV/Err.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy Sun Mar 03 16:59:08 2002 +0100
@@ -12,48 +12,48 @@
datatype 'a err = Err | OK 'a
-types 'a ebinop = "'a => 'a => 'a err"
+types 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
'a esl = "'a set * 'a ord * 'a ebinop"
consts
- ok_val :: "'a err => 'a"
+ ok_val :: "'a err \<Rightarrow> 'a"
primrec
"ok_val (OK x) = x"
constdefs
- lift :: "('a => 'b err) => ('a err => 'b err)"
-"lift f e == case e of Err => Err | OK x => f x"
+ lift :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
+"lift f e == case e of Err \<Rightarrow> Err | OK x \<Rightarrow> f x"
- lift2 :: "('a => 'b => 'c err) => 'a err => 'b err => 'c err"
+ lift2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a err \<Rightarrow> 'b err \<Rightarrow> 'c err"
"lift2 f e1 e2 ==
- case e1 of Err => Err
- | OK x => (case e2 of Err => Err | OK y => f x y)"
+ case e1 of Err \<Rightarrow> Err
+ | OK x \<Rightarrow> (case e2 of Err \<Rightarrow> Err | OK y \<Rightarrow> f x y)"
- le :: "'a ord => 'a err ord"
+ le :: "'a ord \<Rightarrow> 'a err ord"
"le r e1 e2 ==
- case e2 of Err => True |
- OK y => (case e1 of Err => False | OK x => x <=_r y)"
+ case e2 of Err \<Rightarrow> True |
+ OK y \<Rightarrow> (case e1 of Err \<Rightarrow> False | OK x \<Rightarrow> x <=_r y)"
- sup :: "('a => 'b => 'c) => ('a err => 'b err => 'c err)"
+ sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> 'c err)"
"sup f == lift2(%x y. OK(x +_f y))"
- err :: "'a set => 'a err set"
+ err :: "'a set \<Rightarrow> 'a err set"
"err A == insert Err {x . ? y:A. x = OK y}"
- esl :: "'a sl => 'a esl"
+ esl :: "'a sl \<Rightarrow> 'a esl"
"esl == %(A,r,f). (A,r, %x y. OK(f x y))"
- sl :: "'a esl => 'a err sl"
+ sl :: "'a esl \<Rightarrow> 'a err sl"
"sl == %(A,r,f). (err A, le r, lift2 f)"
syntax
- err_semilat :: "'a esl => bool"
+ err_semilat :: "'a esl \<Rightarrow> bool"
translations
"err_semilat L" == "semilat(Err.sl L)"
consts
- strict :: "('a => 'b err) => ('a err => 'b err)"
+ strict :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
primrec
"strict f Err = Err"
"strict f (OK x) = f x"
@@ -75,20 +75,20 @@
by (simp add: lesub_def)
lemma le_err_refl:
- "!x. x <=_r x ==> e <=_(Err.le r) e"
+ "!x. x <=_r x \<Longrightarrow> e <=_(Err.le r) e"
apply (unfold lesub_def Err.le_def)
apply (simp split: err.split)
done
lemma le_err_trans [rule_format]:
- "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e3 --> e1 <=_(le r) e3"
+ "order r \<Longrightarrow> e1 <=_(le r) e2 \<longrightarrow> e2 <=_(le r) e3 \<longrightarrow> e1 <=_(le r) e3"
apply (unfold unfold_lesub_err le_def)
apply (simp split: err.split)
apply (blast intro: order_trans)
done
lemma le_err_antisym [rule_format]:
- "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e1 --> e1=e2"
+ "order r \<Longrightarrow> e1 <=_(le r) e2 \<longrightarrow> e2 <=_(le r) e1 \<longrightarrow> e1=e2"
apply (unfold unfold_lesub_err le_def)
apply (simp split: err.split)
apply (blast intro: order_antisym)
@@ -136,20 +136,20 @@
by (simp add: lesssub_def lesub_def le_def split: err.split)
lemma semilat_errI:
- "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
+ "semilat(A,r,f) \<Longrightarrow> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
apply (unfold semilat_Def closed_def plussub_def lesub_def
lift2_def Err.le_def err_def)
apply (simp split: err.split)
done
lemma err_semilat_eslI:
- "!!L. semilat L ==> err_semilat(esl L)"
+ "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
apply (unfold sl_def esl_def)
apply (simp (no_asm_simp) only: split_tupled_all)
apply (simp add: semilat_errI)
done
-lemma acc_err [simp, intro!]: "acc r ==> acc(le r)"
+lemma acc_err [simp, intro!]: "acc r \<Longrightarrow> acc(le r)"
apply (unfold acc_def lesub_def le_def lesssub_def)
apply (simp add: wf_eq_minimal split: err.split)
apply clarify
@@ -170,7 +170,7 @@
section {* lift *}
lemma lift_in_errI:
- "[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S"
+ "\<lbrakk> e : err S; !x:S. e = OK x \<longrightarrow> f x : err S \<rbrakk> \<Longrightarrow> lift f e : err S"
apply (unfold lift_def)
apply (simp split: err.split)
apply blast
@@ -221,42 +221,42 @@
section {* semilat (err A) (le r) f *}
lemma semilat_le_err_Err_plus [simp]:
- "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err"
+ "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> Err +_f x = Err"
by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
lemma semilat_le_err_plus_Err [simp]:
- "[| x: err A; semilat(err A, le r, f) |] ==> x +_f Err = Err"
+ "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> x +_f Err = Err"
by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
lemma semilat_le_err_OK1:
- "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |]
- ==> x <=_r z";
+ "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk>
+ \<Longrightarrow> x <=_r z";
apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst)
apply simp
done
lemma semilat_le_err_OK2:
- "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |]
- ==> y <=_r z"
+ "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk>
+ \<Longrightarrow> y <=_r z"
apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst)
apply simp
done
lemma eq_order_le:
- "[| x=y; order r |] ==> x <=_r y"
+ "\<lbrakk> x=y; order r \<rbrakk> \<Longrightarrow> x <=_r y"
apply (unfold order_def)
apply blast
done
lemma OK_plus_OK_eq_Err_conv [simp]:
- "[| x:A; y:A; semilat(err A, le r, fe) |] ==>
+ "\<lbrakk> x:A; y:A; semilat(err A, le r, fe) \<rbrakk> \<Longrightarrow>
((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
proof -
- have plus_le_conv3: "!!A x y z f r.
- [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |]
- ==> x <=_r z \<and> y <=_r z"
+ have plus_le_conv3: "\<And>A x y z f r.
+ \<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk>
+ \<Longrightarrow> x <=_r z \<and> y <=_r z"
by (rule plus_le_conv [THEN iffD1])
case rule_context
thus ?thesis
@@ -287,13 +287,13 @@
(* FIXME? *)
lemma all_bex_swap_lemma [iff]:
- "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))"
+ "(!x. (? y:A. x = f y) \<longrightarrow> P x) = (!y:A. P(f y))"
by blast
lemma closed_err_Union_lift2I:
- "[| !A:AS. closed (err A) (lift2 f); AS ~= {};
- !A:AS.!B:AS. A~=B --> (!a:A.!b:B. a +_f b = Err) |]
- ==> closed (err(Union AS)) (lift2 f)"
+ "\<lbrakk> !A:AS. closed (err A) (lift2 f); AS ~= {};
+ !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. a +_f b = Err) \<rbrakk>
+ \<Longrightarrow> closed (err(Union AS)) (lift2 f)"
apply (unfold closed_def err_def)
apply simp
apply clarify
@@ -307,9 +307,9 @@
which may not hold
*}
lemma err_semilat_UnionI:
- "[| !A:AS. err_semilat(A, r, f); AS ~= {};
- !A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |]
- ==> err_semilat(Union AS, r, f)"
+ "\<lbrakk> !A:AS. err_semilat(A, r, f); AS ~= {};
+ !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) \<rbrakk>
+ \<Longrightarrow> err_semilat(Union AS, r, f)"
apply (unfold semilat_def sl_def)
apply (simp add: closed_err_Union_lift2I)
apply (rule conjI)
--- a/src/HOL/MicroJava/BV/JType.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Sun Mar 03 16:59:08 2002 +0100
@@ -17,31 +17,31 @@
by (unfold super_def) (auto dest: subcls1D)
constdefs
- is_ref :: "ty => bool"
- "is_ref T == case T of PrimT t => False | RefT r => True"
+ is_ref :: "ty \<Rightarrow> bool"
+ "is_ref T == case T of PrimT t \<Rightarrow> False | RefT r \<Rightarrow> True"
- sup :: "'c prog => ty => ty => ty err"
+ sup :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty err"
"sup G T1 T2 ==
- case T1 of PrimT P1 => (case T2 of PrimT P2 =>
- (if P1 = P2 then OK (PrimT P1) else Err) | RefT R => Err)
- | RefT R1 => (case T2 of PrimT P => Err | RefT R2 =>
- (case R1 of NullT => (case R2 of NullT => OK NT | ClassT C => OK (Class C))
- | ClassT C => (case R2 of NullT => OK (Class C)
- | ClassT D => OK (Class (exec_lub (subcls1 G) (super G) C D)))))"
+ case T1 of PrimT P1 \<Rightarrow> (case T2 of PrimT P2 \<Rightarrow>
+ (if P1 = P2 then OK (PrimT P1) else Err) | RefT R \<Rightarrow> Err)
+ | RefT R1 \<Rightarrow> (case T2 of PrimT P \<Rightarrow> Err | RefT R2 \<Rightarrow>
+ (case R1 of NullT \<Rightarrow> (case R2 of NullT \<Rightarrow> OK NT | ClassT C \<Rightarrow> OK (Class C))
+ | ClassT C \<Rightarrow> (case R2 of NullT \<Rightarrow> OK (Class C)
+ | ClassT D \<Rightarrow> OK (Class (exec_lub (subcls1 G) (super G) C D)))))"
- subtype :: "'c prog => ty => ty => bool"
+ subtype :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
"subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2"
- is_ty :: "'c prog => ty => bool"
- "is_ty G T == case T of PrimT P => True | RefT R =>
- (case R of NullT => True | ClassT C => (C,Object):(subcls1 G)^*)"
+ is_ty :: "'c prog \<Rightarrow> ty \<Rightarrow> bool"
+ "is_ty G T == case T of PrimT P \<Rightarrow> True | RefT R \<Rightarrow>
+ (case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (C,Object):(subcls1 G)^*)"
translations
"types G" == "Collect (is_type G)"
constdefs
- esl :: "'c prog => ty esl"
+ esl :: "'c prog \<Rightarrow> ty esl"
"esl G == (types G, subtype G, sup G)"
lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
@@ -51,12 +51,12 @@
by (auto elim: widen.elims)
lemma is_tyI:
- "[| is_type G T; wf_prog wf_mb G |] ==> is_ty G T"
+ "\<lbrakk> is_type G T; wf_prog wf_mb G \<rbrakk> \<Longrightarrow> is_ty G T"
by (auto simp add: is_ty_def intro: subcls_C_Object
split: ty.splits ref_ty.splits)
lemma is_type_conv:
- "wf_prog wf_mb G ==> is_type G T = is_ty G T"
+ "wf_prog wf_mb G \<Longrightarrow> is_type G T = is_ty G T"
proof
assume "is_type G T" "wf_prog wf_mb G"
thus "is_ty G T"
@@ -86,7 +86,7 @@
qed
lemma order_widen:
- "acyclic (subcls1 G) ==> order (subtype G)"
+ "acyclic (subcls1 G) \<Longrightarrow> order (subtype G)"
apply (unfold order_def lesub_def subtype_def)
apply (auto intro: widen_trans)
apply (case_tac x)
@@ -106,7 +106,7 @@
done
lemma wf_converse_subcls1_impl_acc_subtype:
- "wf ((subcls1 G)^-1) ==> acc (subtype G)"
+ "wf ((subcls1 G)^-1) \<Longrightarrow> acc (subtype G)"
apply (unfold acc_def lesssub_def)
apply (drule_tac p = "(subcls1 G)^-1 - Id" in wf_subset)
apply blast
@@ -159,8 +159,8 @@
done
lemma closed_err_types:
- "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |]
- ==> closed (err (types G)) (lift2 (sup G))"
+ "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk>
+ \<Longrightarrow> closed (err (types G)) (lift2 (sup G))"
apply (unfold closed_def plussub_def lift2_def sup_def)
apply (auto split: err.split)
apply (drule is_tyI, assumption)
@@ -171,9 +171,9 @@
lemma sup_subtype_greater:
- "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
- is_type G t1; is_type G t2; sup G t1 t2 = OK s |]
- ==> subtype G t1 s \<and> subtype G t2 s"
+ "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
+ is_type G t1; is_type G t2; sup G t1 t2 = OK s \<rbrakk>
+ \<Longrightarrow> subtype G t1 s \<and> subtype G t2 s"
proof -
assume wf_prog: "wf_prog wf_mb G"
assume single_valued: "single_valued (subcls1 G)"
@@ -210,10 +210,10 @@
qed
lemma sup_subtype_smallest:
- "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
+ "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
is_type G a; is_type G b; is_type G c;
- subtype G a c; subtype G b c; sup G a b = OK d |]
- ==> subtype G d c"
+ subtype G a c; subtype G b c; sup G a b = OK d \<rbrakk>
+ \<Longrightarrow> subtype G d c"
proof -
assume wf_prog: "wf_prog wf_mb G"
assume single_valued: "single_valued (subcls1 G)"
@@ -244,7 +244,7 @@
} note this [intro]
have [dest!]:
- "!!C T. G \<turnstile> Class C \<preceq> T ==> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
+ "\<And>C T. G \<turnstile> Class C \<preceq> T \<Longrightarrow> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
by (frule widen_Class, auto)
assume "is_type G a" "is_type G b" "is_type G c"
@@ -255,13 +255,13 @@
qed
lemma sup_exists:
- "[| subtype G a c; subtype G b c; sup G a b = Err |] ==> False"
+ "\<lbrakk> subtype G a c; subtype G b c; sup G a b = Err \<rbrakk> \<Longrightarrow> False"
by (auto simp add: PrimT_PrimT PrimT_PrimT2 sup_def subtype_def
split: ty.splits ref_ty.splits)
lemma err_semilat_JType_esl_lemma:
- "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |]
- ==> err_semilat (esl G)"
+ "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk>
+ \<Longrightarrow> err_semilat (esl G)"
proof -
assume wf_prog: "wf_prog wf_mb G"
assume single_valued: "single_valued (subcls1 G)"
@@ -297,12 +297,12 @@
qed
lemma single_valued_subcls1:
- "wf_prog wf_mb G ==> single_valued (subcls1 G)"
+ "wf_prog wf_mb G \<Longrightarrow> single_valued (subcls1 G)"
by (auto simp add: wf_prog_def unique_def single_valued_def
intro: subcls1I elim!: subcls1.elims)
theorem err_semilat_JType_esl:
- "wf_prog wf_mb G ==> err_semilat (esl G)"
+ "wf_prog wf_mb G \<Longrightarrow> err_semilat (esl G)"
by (frule acyclic_subcls1, frule single_valued_subcls1, rule err_semilat_JType_esl_lemma)
end
--- a/src/HOL/MicroJava/BV/JVM.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Sun Mar 03 16:59:08 2002 +0100
@@ -14,8 +14,8 @@
"exec G maxs rT et bs ==
err_step (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
- kiljvm :: "jvm_prog => nat => nat => ty => exception_table =>
- instr list => state list => state list"
+ kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow>
+ instr list \<Rightarrow> state list \<Rightarrow> state list"
"kiljvm G maxs maxr rT et bs ==
kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)"
@@ -28,7 +28,7 @@
result = kiljvm G mxs (1+size pTs+mxl) rT et ins start
in \<forall>n < size ins. result!n \<noteq> Err)"
- wt_jvm_prog_kildall :: "jvm_prog => bool"
+ wt_jvm_prog_kildall :: "jvm_prog \<Rightarrow> bool"
"wt_jvm_prog_kildall G ==
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"
@@ -77,7 +77,7 @@
theorem exec_pres_type:
- "wf_prog wf_mb S ==>
+ "wf_prog wf_mb S \<Longrightarrow>
pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
apply (unfold exec_def JVM_states_unfold)
apply (rule pres_type_lift)
@@ -243,7 +243,7 @@
by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
theorem exec_mono:
- "wf_prog wf_mb G ==>
+ "wf_prog wf_mb G \<Longrightarrow>
mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"
apply (unfold exec_def JVM_le_unfold JVM_states_unfold)
apply (rule mono_lift)
@@ -257,7 +257,7 @@
done
theorem semilat_JVM_slI:
- "wf_prog wf_mb G ==> semilat (JVMType.sl G maxs maxr)"
+ "wf_prog wf_mb G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
apply (rule semilat_opt)
apply (rule err_semilat_Product_esl)
@@ -275,7 +275,7 @@
theorem is_bcv_kiljvm:
- "[| wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) |] ==>
+ "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow>
is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
(size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
apply (unfold kiljvm_def sl_triple_conv)
@@ -293,9 +293,9 @@
theorem wt_kil_correct:
- "[| wt_kil G C pTs rT maxs mxl et bs; wf_prog wf_mb G;
- is_class G C; \<forall>x \<in> set pTs. is_type G x |]
- ==> \<exists>phi. wt_method G C pTs rT maxs mxl bs et phi"
+ "\<lbrakk> wt_kil G C pTs rT maxs mxl et bs; wf_prog wf_mb G;
+ is_class G C; \<forall>x \<in> set pTs. is_type G x \<rbrakk>
+ \<Longrightarrow> \<exists>phi. wt_method G C pTs rT maxs mxl bs et phi"
proof -
let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
#(replicate (size bs - 1) (OK None))"
@@ -386,10 +386,10 @@
theorem wt_kil_complete:
- "[| wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G;
+ "\<lbrakk> wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G;
length phi = length bs; is_class G C; \<forall>x \<in> set pTs. is_type G x;
- map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl)) |]
- ==> wt_kil G C pTs rT maxs mxl et bs"
+ map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl)) \<rbrakk>
+ \<Longrightarrow> wt_kil G C pTs rT maxs mxl et bs"
proof -
assume wf: "wf_prog wf_mb G"
assume isclass: "is_class G C"
@@ -490,12 +490,12 @@
have "JVMType.le G maxs ?maxr (OK None) (?phi!n)"
by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def
split: err.splits)
- hence "[| n = Suc n'; n < length ?start |]
- ==> JVMType.le G maxs ?maxr (?start!n) (?phi!n)"
+ hence "\<lbrakk> n = Suc n'; n < length ?start \<rbrakk>
+ \<Longrightarrow> JVMType.le G maxs ?maxr (?start!n) (?phi!n)"
by simp
}
ultimately
- have "n < length ?start ==> (?start!n) <=_(JVMType.le G maxs ?maxr) (?phi!n)"
+ have "n < length ?start \<Longrightarrow> (?start!n) <=_(JVMType.le G maxs ?maxr) (?phi!n)"
by (unfold lesub_def) (cases n, blast+)
}
ultimately show ?thesis by (rule le_listI)
@@ -540,9 +540,9 @@
programs without problems:
*}
lemma is_type_pTs:
- "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls;
- t \<in> set (snd sig) |]
- ==> is_type G t"
+ "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls;
+ t \<in> set (snd sig) \<rbrakk>
+ \<Longrightarrow> is_type G t"
proof -
assume "wf_prog wf_mb G"
"(C,S,fs,mdecls) \<in> set G"
@@ -559,7 +559,7 @@
theorem jvm_kildall_correct:
- "wt_jvm_prog_kildall G ==> \<exists>Phi. wt_jvm_prog G Phi"
+ "wt_jvm_prog_kildall G \<Longrightarrow> \<exists>Phi. wt_jvm_prog G Phi"
proof -
assume wtk: "wt_jvm_prog_kildall G"
--- a/src/HOL/MicroJava/BV/JVMType.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Sun Mar 03 16:59:08 2002 +0100
@@ -15,58 +15,58 @@
state_type = "opstack_type \<times> locvars_type"
state = "state_type option err" -- "for Kildall"
method_type = "state_type option list" -- "for BVSpec"
- class_type = "sig => method_type"
- prog_type = "cname => class_type"
+ class_type = "sig \<Rightarrow> method_type"
+ prog_type = "cname \<Rightarrow> class_type"
constdefs
- stk_esl :: "'c prog => nat => ty list esl"
+ stk_esl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty list esl"
"stk_esl S maxs == upto_esl maxs (JType.esl S)"
- reg_sl :: "'c prog => nat => ty err list sl"
+ reg_sl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty err list sl"
"reg_sl S maxr == Listn.sl maxr (Err.sl (JType.esl S))"
- sl :: "'c prog => nat => nat => state sl"
+ sl :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state sl"
"sl S maxs maxr ==
Err.sl(Opt.esl(Product.esl (stk_esl S maxs) (Err.esl(reg_sl S maxr))))"
constdefs
- states :: "'c prog => nat => nat => state set"
+ states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state set"
"states S maxs maxr == fst(sl S maxs maxr)"
- le :: "'c prog => nat => nat => state ord"
+ le :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state ord"
"le S maxs maxr == fst(snd(sl S maxs maxr))"
- sup :: "'c prog => nat => nat => state binop"
+ sup :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state binop"
"sup S maxs maxr == snd(snd(sl S maxs maxr))"
constdefs
- sup_ty_opt :: "['code prog,ty err,ty err] => bool"
+ sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool"
("_ |- _ <=o _" [71,71] 70)
"sup_ty_opt G == Err.le (subtype G)"
- sup_loc :: "['code prog,locvars_type,locvars_type] => bool"
+ sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool"
("_ |- _ <=l _" [71,71] 70)
"sup_loc G == Listn.le (sup_ty_opt G)"
- sup_state :: "['code prog,state_type,state_type] => bool"
+ sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"
("_ |- _ <=s _" [71,71] 70)
"sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
- sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
+ sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
("_ |- _ <=' _" [71,71] 70)
"sup_state_opt G == Opt.le (sup_state G)"
syntax (xsymbols)
- sup_ty_opt :: "['code prog,ty err,ty err] => bool"
+ sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool"
("_ \<turnstile> _ <=o _" [71,71] 70)
- sup_loc :: "['code prog,locvars_type,locvars_type] => bool"
+ sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool"
("_ \<turnstile> _ <=l _" [71,71] 70)
- sup_state :: "['code prog,state_type,state_type] => bool"
+ sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"
("_ \<turnstile> _ <=s _" [71,71] 70)
- sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
+ sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
("_ \<turnstile> _ <=' _" [71,71] 70)
@@ -98,7 +98,7 @@
sup_ty_opt_def JVM_le_unfold) simp
lemma zip_map [rule_format]:
- "\<forall>a. length a = length b -->
+ "\<forall>a. length a = length b \<longrightarrow>
zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)"
apply (induct b)
apply simp
@@ -188,11 +188,11 @@
by (simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def)
theorem sup_ty_opt_OK:
- "G \<turnstile> a <=o (OK b) ==> \<exists> x. a = OK x"
+ "G \<turnstile> a <=o (OK b) \<Longrightarrow> \<exists> x. a = OK x"
by (clarsimp simp add: sup_ty_opt_def Err.le_def split: err.splits)
lemma widen_PrimT_conv1 [simp]:
- "[| G \<turnstile> S \<preceq> T; S = PrimT x|] ==> T = PrimT x"
+ "\<lbrakk> G \<turnstile> S \<preceq> T; S = PrimT x\<rbrakk> \<Longrightarrow> T = PrimT x"
by (auto elim: widen.elims)
theorem sup_PTS_eq:
@@ -214,20 +214,20 @@
theorem sup_loc_length:
- "G \<turnstile> a <=l b ==> length a = length b"
+ "G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
proof -
assume G: "G \<turnstile> a <=l b"
- have "\<forall>b. (G \<turnstile> a <=l b) --> length a = length b"
+ have "\<forall>b. (G \<turnstile> a <=l b) \<longrightarrow> length a = length b"
by (induct a, auto)
with G
show ?thesis by blast
qed
theorem sup_loc_nth:
- "[| G \<turnstile> a <=l b; n < length a |] ==> G \<turnstile> (a!n) <=o (b!n)"
+ "\<lbrakk> G \<turnstile> a <=l b; n < length a \<rbrakk> \<Longrightarrow> G \<turnstile> (a!n) <=o (b!n)"
proof -
assume a: "G \<turnstile> a <=l b" "n < length a"
- have "\<forall> n b. (G \<turnstile> a <=l b) --> n < length a --> (G \<turnstile> (a!n) <=o (b!n))"
+ have "\<forall> n b. (G \<turnstile> a <=l b) \<longrightarrow> n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))"
(is "?P a")
proof (induct a)
show "?P []" by simp
@@ -248,8 +248,8 @@
qed
theorem all_nth_sup_loc:
- "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n)))
- --> (G \<turnstile> a <=l b)" (is "?P a")
+ "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n)))
+ \<longrightarrow> (G \<turnstile> a <=l b)" (is "?P a")
proof (induct a)
show "?P []" by simp
@@ -258,14 +258,14 @@
show "?P (l#ls)"
proof (intro strip)
fix b
- assume f: "\<forall>n. n < length (l # ls) --> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
+ assume f: "\<forall>n. n < length (l # ls) \<longrightarrow> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
assume l: "length (l#ls) = length b"
then obtain b' bs where b: "b = b'#bs"
by - (cases b, simp, simp add: neq_Nil_conv, rule that)
with f
- have "\<forall>n. n < length ls --> (G \<turnstile> (ls!n) <=o (bs!n))"
+ have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
by auto
with f b l IH
@@ -276,12 +276,12 @@
theorem sup_loc_append:
- "length a = length b ==>
+ "length a = length b \<Longrightarrow>
(G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
proof -
assume l: "length a = length b"
- have "\<forall>b. length a = length b --> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and>
+ have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and>
(G \<turnstile> x <=l y))" (is "?P a")
proof (induct a)
show "?P []" by simp
@@ -347,7 +347,7 @@
theorem sup_loc_update [rule_format]:
- "\<forall> n y. (G \<turnstile> a <=o b) --> n < length y --> (G \<turnstile> x <=l y) -->
+ "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow>
(G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
proof (induct x)
show "?P []" by simp
@@ -365,17 +365,17 @@
theorem sup_state_length [simp]:
- "G \<turnstile> s2 <=s s1 ==>
+ "G \<turnstile> s2 <=s s1 \<Longrightarrow>
length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
by (auto dest: sup_loc_length simp add: sup_state_def stk_convert lesub_def Product.le_def);
theorem sup_state_append_snd:
- "length a = length b ==>
+ "length a = length b \<Longrightarrow>
(G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append)
theorem sup_state_append_fst:
- "length a = length b ==>
+ "length a = length b \<Longrightarrow>
(G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append)
@@ -390,13 +390,13 @@
by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def map_eq_Cons sup_loc_Cons2)
theorem sup_state_ignore_fst:
- "G \<turnstile> (a, x) <=s (b, y) ==> G \<turnstile> (c, x) <=s (c, y)"
+ "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
by (simp add: sup_state_def lesub_def Product.le_def)
theorem sup_state_rev_fst:
"(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))"
proof -
- have m: "!!f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
+ have m: "\<And>f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
show ?thesis by (simp add: m sup_state_def stk_convert lesub_def Product.le_def)
qed
@@ -423,17 +423,17 @@
theorem sup_ty_opt_trans [trans]:
- "[|G \<turnstile> a <=o b; G \<turnstile> b <=o c|] ==> G \<turnstile> a <=o c"
+ "\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
by (auto intro: widen_trans
simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def
split: err.splits)
theorem sup_loc_trans [trans]:
- "[|G \<turnstile> a <=l b; G \<turnstile> b <=l c|] ==> G \<turnstile> a <=l c"
+ "\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
proof -
assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
- hence "\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (c!n))"
+ hence "\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (c!n))"
proof (intro strip)
fix n
assume n: "n < length a"
@@ -442,7 +442,7 @@
by - (rule sup_loc_nth)
also
from n G
- have "G \<turnstile> ... <=o (c!n)"
+ have "G \<turnstile> \<dots> <=o (c!n)"
by - (rule sup_loc_nth, auto dest: sup_loc_length)
finally
show "G \<turnstile> (a!n) <=o (c!n)" .
@@ -455,11 +455,11 @@
theorem sup_state_trans [trans]:
- "[|G \<turnstile> a <=s b; G \<turnstile> b <=s c|] ==> G \<turnstile> a <=s c"
+ "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
by (auto intro: sup_loc_trans simp add: sup_state_def stk_convert Product.le_def lesub_def)
theorem sup_state_opt_trans [trans]:
- "[|G \<turnstile> a <=' b; G \<turnstile> b <=' c|] ==> G \<turnstile> a <=' c"
+ "\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
by (auto intro: sup_state_trans
simp add: sup_state_opt_def Opt.le_def lesub_def
split: option.splits)
--- a/src/HOL/MicroJava/BV/Kildall.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy Sun Mar 03 16:59:08 2002 +0100
@@ -11,24 +11,24 @@
theory Kildall = Typing_Framework + While_Combinator + Product:
-syntax "@lesubstep_type" :: "(nat \<times> 's) list => 's ord => (nat \<times> 's) list => bool"
+syntax "@lesubstep_type" :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
("(_ /<=|_| _)" [50, 0, 51] 50)
translations
"x <=|r| y" == "x <=[(Product.le (op =) r)] y"
constdefs
- pres_type :: "'s step_type => nat => 's set => bool"
+ pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
"pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A"
- mono :: "'s ord => 's step_type => nat => 's set => bool"
+ mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
"mono r step n A ==
- \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t --> step p s <=|r| step p t"
+ \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t"
consts
iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow>
's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set"
- propa :: "'s binop => (nat \<times> 's) list => 's list => nat set => 's list * nat set"
+ propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set"
primrec
"propa f [] ss w = (ss,w)"
@@ -45,13 +45,13 @@
(ss,w)"
constdefs
- unstables :: "'s ord => 's step_type => 's list => nat set"
+ unstables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat set"
"unstables r step ss == {p. p < size ss \<and> \<not>stable r step ss p}"
- kildall :: "'s ord => 's binop => 's step_type => 's list => 's list"
+ kildall :: "'s ord \<Rightarrow> 's binop \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> 's list"
"kildall r f step ss == fst(iter f step ss (unstables r step ss))"
-consts merges :: "'s binop => (nat \<times> 's) list => 's list => 's list"
+consts merges :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> 's list"
primrec
"merges f [] ss = ss"
"merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"
@@ -61,16 +61,16 @@
consts
- "@plusplussub" :: "'a list => ('a => 'a => 'a) => 'a => 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
+ "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
primrec
"[] ++_f y = y"
"(x#xs) ++_f y = xs ++_f (x +_f y)"
lemma nth_merges:
- "!!ss. [| semilat (A, r, f); p < length ss; ss \<in> list n A;
- \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A |] ==>
+ "\<And>ss. \<lbrakk> semilat (A, r, f); p < length ss; ss \<in> list n A;
+ \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
(merges f ps ss)!p = map snd [(p',t') \<in> ps. p'=p] ++_f ss!p"
- (is "!!ss. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?steptype ps \<Longrightarrow> ?P ss ps")
+ (is "\<And>ss. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?steptype ps \<Longrightarrow> ?P ss ps")
proof (induct ps)
show "\<And>ss. ?P ss []" by simp
@@ -98,15 +98,15 @@
lemma pres_typeD:
- "[| pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) |] ==> s' \<in> A"
+ "\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A"
by (unfold pres_type_def, blast)
lemma boundedD:
- "[| bounded step n; p < n; (q,t) : set (step p xs) |] ==> q < n"
+ "\<lbrakk> bounded step n; p < n; (q,t) : set (step p xs) \<rbrakk> \<Longrightarrow> q < n"
by (unfold bounded_def, blast)
lemma monoD:
- "[| mono r step n A; p < n; s\<in>A; s <=_r t |] ==> step p s <=|r| step p t"
+ "\<lbrakk> mono r step n A; p < n; s\<in>A; s <=_r t \<rbrakk> \<Longrightarrow> step p s <=|r| step p t"
by (unfold mono_def, blast)
(** merges **)
@@ -117,9 +117,9 @@
lemma merges_preserves_type_lemma:
- "[| semilat(A,r,f) |] ==>
- \<forall>xs. xs \<in> list n A --> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
- --> merges f ps xs \<in> list n A"
+ "semilat(A,r,f) \<Longrightarrow>
+ \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
+ \<longrightarrow> merges f ps xs \<in> list n A"
apply (frule semilatDclosedI)
apply (unfold closed_def)
apply (induct_tac ps)
@@ -128,13 +128,13 @@
done
lemma merges_preserves_type [simp]:
- "[| semilat(A,r,f); xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A |]
- ==> merges f ps xs \<in> list n A"
+ "\<lbrakk> semilat(A,r,f); xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
+ \<Longrightarrow> merges f ps xs \<in> list n A"
by (simp add: merges_preserves_type_lemma)
lemma merges_incr_lemma:
- "[| semilat(A,r,f) |] ==>
- \<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"
+ "semilat(A,r,f) \<Longrightarrow>
+ \<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"
apply (induct_tac ps)
apply simp
apply simp
@@ -149,14 +149,14 @@
done
lemma merges_incr:
- "[| semilat(A,r,f); xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A |]
- ==> xs <=[r] merges f ps xs"
+ "\<lbrakk> semilat(A,r,f); xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk>
+ \<Longrightarrow> xs <=[r] merges f ps xs"
by (simp add: merges_incr_lemma)
lemma merges_same_conv [rule_format]:
- "[| semilat(A,r,f) |] ==>
- (\<forall>xs. xs \<in> list n A --> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) -->
+ "semilat(A,r,f) \<Longrightarrow>
+ (\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow>
(merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))"
apply (induct_tac ps)
apply simp
@@ -191,25 +191,25 @@
lemma list_update_le_listI [rule_format]:
- "set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs -->
- x <=_r ys!p --> semilat(A,r,f) --> x\<in>A -->
+ "set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>
+ x <=_r ys!p \<longrightarrow> semilat(A,r,f) \<longrightarrow> x\<in>A \<longrightarrow>
xs[p := x +_f xs!p] <=[r] ys"
apply (unfold Listn.le_def lesub_def semilat_def)
apply (simp add: list_all2_conv_all_nth nth_list_update)
done
lemma merges_pres_le_ub:
- "[| semilat(A,r,f); set ts <= A; set ss <= A;
+ "\<lbrakk> semilat(A,r,f); set ts <= A; set ss <= A;
\<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts;
- ss <=[r] ts |]
- ==> merges f ps ss <=[r] ts"
+ ss <=[r] ts \<rbrakk>
+ \<Longrightarrow> merges f ps ss <=[r] ts"
proof -
{ fix A r f t ts ps
have
- "!!qs. [| semilat(A,r,f); set ts <= A;
- \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts |] ==>
- set qs <= set ps -->
- (\<forall>ss. set ss <= A --> ss <=[r] ts --> merges f qs ss <=[r] ts)"
+ "\<And>qs. \<lbrakk> semilat(A,r,f); set ts <= A;
+ \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts \<rbrakk> \<Longrightarrow>
+ set qs <= set ps \<longrightarrow>
+ (\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)"
apply (induct_tac qs)
apply simp
apply (simp (no_asm_simp))
@@ -233,7 +233,7 @@
lemma decomp_propa:
- "!!ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow>
+ "\<And>ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow>
propa f qs ss w =
(merges f qs ss, {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un w)"
apply (induct qs)
@@ -263,7 +263,7 @@
thus "(x#xs) ++_f y \<in> A" by simp
qed
-lemma ub2: "!!y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
+lemma ub2: "\<And>y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
proof (induct x)
show "\<And>y. semilat(A, r, f) \<Longrightarrow> y <=_r [] ++_f y" by simp
@@ -287,7 +287,8 @@
qed
-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"
+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"
proof (induct ls)
show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
@@ -298,7 +299,8 @@
then obtain s: "s \<in> A" and ls: "set ls \<subseteq> A" by simp
assume y: "y \<in> A"
- 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"
+ 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"
hence IH: "\<And>y. x \<in> set ls \<Longrightarrow> y \<in> A \<Longrightarrow> x <=_r ls ++_f y" .
assume "x \<in> set (s#ls)"
@@ -356,12 +358,12 @@
lemma stable_pres_lemma:
- "[| semilat (A,r,f); pres_type step n A; bounded step n;
+ "\<lbrakk> semilat (A,r,f); pres_type step n A; bounded step n;
ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n;
\<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n;
\<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q;
- q \<notin> w \<or> q = p |]
- ==> stable r step (merges f (step p (ss!p)) ss) q"
+ q \<notin> w \<or> q = p \<rbrakk>
+ \<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q"
apply (unfold stable_def)
apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A")
prefer 2
@@ -434,7 +436,7 @@
lemma lesub_step_type:
- "!!b x y. a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
+ "\<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'"
apply (induct a)
apply simp
apply simp
@@ -451,10 +453,10 @@
lemma merges_bounded_lemma:
- "[| semilat (A,r,f); mono r step n A; bounded step n;
+ "\<lbrakk> semilat (A,r,f); mono r step n A; bounded step n;
\<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n;
- ss <=[r] ts; ! p. p < n --> stable r step ts p |]
- ==> merges f (step p (ss!p)) ss <=[r] ts"
+ ss <=[r] ts; ! p. p < n \<longrightarrow> stable r step ts p \<rbrakk>
+ \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts"
apply (unfold stable_def)
apply (rule merges_pres_le_ub)
apply assumption
@@ -481,7 +483,7 @@
done
lemma termination_lemma:
- "[| semilat(A,r,f); ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w |] ==>
+ "\<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>
ss <[r] merges f qs ss \<or>
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"
apply (unfold lesssub_def)
@@ -617,10 +619,10 @@
done
lemma is_bcv_kildall:
- "[| semilat(A,r,f); acc r; top r T;
+ "\<lbrakk> semilat(A,r,f); acc r; top r T;
pres_type step n A; bounded step n;
- mono r step n A |]
- ==> is_bcv r T step n A (kildall r f step)"
+ mono r step n A \<rbrakk>
+ \<Longrightarrow> is_bcv r T step n A (kildall r f step)"
apply(unfold is_bcv_def wt_step_def)
apply(insert kildall_properties[of A])
apply(simp add:stables_def)
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Sun Mar 03 16:59:08 2002 +0100
@@ -14,43 +14,43 @@
theory LBVComplete = BVSpec + LBVSpec + EffectMono:
constdefs
- contains_targets :: "[instr list, certificate, method_type, p_count] => bool"
+ contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
"contains_targets ins cert phi pc ==
\<forall>pc' \<in> set (succs (ins!pc) pc).
- pc' \<noteq> pc+1 \<and> pc' < length ins --> cert!pc' = phi!pc'"
+ pc' \<noteq> pc+1 \<and> pc' < length ins \<longrightarrow> cert!pc' = phi!pc'"
- fits :: "[instr list, certificate, method_type] => bool"
- "fits ins cert phi == \<forall>pc. pc < length ins -->
+ fits :: "[instr list, certificate, method_type] \<Rightarrow> bool"
+ "fits ins cert phi == \<forall>pc. pc < length ins \<longrightarrow>
contains_targets ins cert phi pc \<and>
(cert!pc = None \<or> cert!pc = phi!pc)"
- is_target :: "[instr list, p_count] => bool"
+ is_target :: "[instr list, p_count] \<Rightarrow> bool"
"is_target ins pc ==
\<exists>pc'. pc \<noteq> pc'+1 \<and> pc' < length ins \<and> pc \<in> set (succs (ins!pc') pc')"
constdefs
- make_cert :: "[instr list, method_type] => certificate"
+ make_cert :: "[instr list, method_type] \<Rightarrow> certificate"
"make_cert ins phi ==
map (\<lambda>pc. if is_target ins pc then phi!pc else None) [0..length ins(]"
- make_Cert :: "[jvm_prog, prog_type] => prog_certificate"
+ make_Cert :: "[jvm_prog, prog_type] \<Rightarrow> prog_certificate"
"make_Cert G Phi == \<lambda> C sig. let (C,rT,(maxs,maxl,b)) = the (method (G,C) sig)
in make_cert b (Phi C sig)"
lemmas [simp del] = split_paired_Ex
lemma make_cert_target:
- "[| pc < length ins; is_target ins pc |] ==> make_cert ins phi ! pc = phi!pc"
+ "\<lbrakk> pc < length ins; is_target ins pc \<rbrakk> \<Longrightarrow> make_cert ins phi ! pc = phi!pc"
by (simp add: make_cert_def)
lemma make_cert_approx:
- "[| pc < length ins; make_cert ins phi ! pc \<noteq> phi ! pc |] ==>
+ "\<lbrakk> pc < length ins; make_cert ins phi ! pc \<noteq> phi ! pc \<rbrakk> \<Longrightarrow>
make_cert ins phi ! pc = None"
by (auto simp add: make_cert_def)
lemma make_cert_contains_targets:
- "pc < length ins ==> contains_targets ins (make_cert ins phi) phi pc"
+ "pc < length ins \<Longrightarrow> contains_targets ins (make_cert ins phi) phi pc"
proof (unfold contains_targets_def, intro strip, elim conjE)
fix pc'
assume "pc < length ins"
@@ -71,19 +71,19 @@
by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets)
lemma fitsD:
- "[| fits ins cert phi; pc' \<in> set (succs (ins!pc) pc);
- pc' \<noteq> Suc pc; pc < length ins; pc' < length ins |]
- ==> cert!pc' = phi!pc'"
+ "\<lbrakk> fits ins cert phi; pc' \<in> set (succs (ins!pc) pc);
+ pc' \<noteq> Suc pc; pc < length ins; pc' < length ins \<rbrakk>
+ \<Longrightarrow> cert!pc' = phi!pc'"
by (clarsimp simp add: fits_def contains_targets_def)
lemma fitsD2:
- "[| fits ins cert phi; pc < length ins; cert!pc = Some s |]
- ==> cert!pc = phi!pc"
+ "\<lbrakk> fits ins cert phi; pc < length ins; cert!pc = Some s \<rbrakk>
+ \<Longrightarrow> cert!pc = phi!pc"
by (auto simp add: fits_def)
lemma wtl_inst_mono:
- "[| wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi;
- pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
+ "\<lbrakk> wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi;
+ pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc \<rbrakk> \<Longrightarrow>
\<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
proof -
assume pc: "pc < length ins" "i = ins!pc"
@@ -144,8 +144,8 @@
lemma wtl_cert_mono:
- "[| wtl_cert i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi;
- pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
+ "\<lbrakk> wtl_cert i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi;
+ pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc \<rbrakk> \<Longrightarrow>
\<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
proof -
assume wtl: "wtl_cert i G rT s1 cert mxs mpc pc = OK s1'" and
@@ -181,8 +181,8 @@
lemma wt_instr_imp_wtl_inst:
- "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
- pc < length ins; length ins = max_pc |] ==>
+ "\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
+ pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow>
wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
proof -
assume wt: "wt_instr (ins!pc) G rT phi mxs max_pc pc"
@@ -193,14 +193,14 @@
have app: "app (ins!pc) G mxs rT (phi!pc)" by (simp add: wt_instr_def)
from wt pc
- have pc': "!!pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
+ have pc': "\<And>pc'. pc' \<in> set (succs (ins!pc) pc) \<Longrightarrow> pc' < length ins"
by (simp add: wt_instr_def)
let ?s' = "eff (ins!pc) G (phi!pc)"
from wt fits pc
- have cert: "!!pc'. [|pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1|]
- ==> G \<turnstile> ?s' <=' cert!pc'"
+ have cert: "\<And>pc'. \<lbrakk>pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1\<rbrakk>
+ \<Longrightarrow> G \<turnstile> ?s' <=' cert!pc'"
by (auto dest: fitsD simp add: wt_instr_def)
from app pc cert pc'
@@ -209,9 +209,9 @@
qed
lemma wt_less_wtl:
- "[| wt_instr (ins!pc) G rT phi mxs max_pc pc;
+ "\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc;
wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s;
- fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==>
+ fits ins cert phi; Suc pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow>
G \<turnstile> s <=' phi ! Suc pc"
proof -
assume wt: "wt_instr (ins!pc) G rT phi mxs max_pc pc"
@@ -222,7 +222,7 @@
{ assume suc: "Suc pc \<in> set (succs (ins ! pc) pc)"
with wtl have "s = eff (ins!pc) G (phi!pc)"
by (simp add: wtl_inst_OK)
- also from suc wt have "G \<turnstile> ... <=' phi!Suc pc"
+ also from suc wt have "G \<turnstile> \<dots> <=' phi!Suc pc"
by (simp add: wt_instr_def)
finally have ?thesis .
}
@@ -244,8 +244,8 @@
lemma wt_instr_imp_wtl_cert:
- "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
- pc < length ins; length ins = max_pc |] ==>
+ "\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
+ pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow>
wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
proof -
assume "wt_instr (ins!pc) G rT phi mxs max_pc pc" and
@@ -256,7 +256,7 @@
hence wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
by (rule wt_instr_imp_wtl_inst)
- hence "cert!pc = None ==> ?thesis"
+ hence "cert!pc = None \<Longrightarrow> ?thesis"
by (simp add: wtl_cert_def)
moreover
@@ -276,9 +276,9 @@
lemma wt_less_wtl_cert:
- "[| wt_instr (ins!pc) G rT phi mxs max_pc pc;
+ "\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc;
wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s;
- fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==>
+ fits ins cert phi; Suc pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow>
G \<turnstile> s <=' phi ! Suc pc"
proof -
assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s"
@@ -319,14 +319,14 @@
*}
theorem wt_imp_wtl_inst_list:
-"\<forall> pc. (\<forall>pc'. pc' < length all_ins -->
- wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc') -->
- fits all_ins cert phi -->
- (\<exists>l. pc = length l \<and> all_ins = l@ins) -->
- pc < length all_ins -->
- (\<forall> s. (G \<turnstile> s <=' (phi!pc)) -->
+"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow>
+ wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc') \<longrightarrow>
+ fits all_ins cert phi \<longrightarrow>
+ (\<exists>l. pc = length l \<and> all_ins = l@ins) \<longrightarrow>
+ pc < length all_ins \<longrightarrow>
+ (\<forall> s. (G \<turnstile> s <=' (phi!pc)) \<longrightarrow>
wtl_inst_list ins G rT cert mxs (length all_ins) pc s \<noteq> Err)"
-(is "\<forall>pc. ?wt --> ?fits --> ?l pc ins --> ?len pc --> ?wtl pc ins"
+(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins"
is "\<forall>pc. ?C pc ins" is "?P ins")
proof (induct "?P" "ins")
case Nil
@@ -338,7 +338,7 @@
show "?P (i#ins')"
proof (intro allI impI, elim exE conjE)
fix pc s l
- assume wt : "\<forall>pc'. pc' < length all_ins -->
+ assume wt : "\<forall>pc'. pc' < length all_ins \<longrightarrow>
wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc'"
assume fits: "fits all_ins cert phi"
assume l : "pc < length all_ins"
@@ -357,7 +357,7 @@
from Cons
have "?C (Suc pc) ins'" by blast
with wt fits pc
- have IH: "?len (Suc pc) --> ?wtl (Suc pc) ins'" by auto
+ have IH: "?len (Suc pc) \<longrightarrow> ?wtl (Suc pc) ins'" by auto
show "wtl_inst_list (i#ins') G rT cert mxs (length all_ins) pc s \<noteq> Err"
proof (cases "?len (Suc pc)")
@@ -398,15 +398,15 @@
lemma fits_imp_wtl_method_complete:
- "[| wt_method G C pTs rT mxs mxl ins phi; fits ins cert phi |]
- ==> wtl_method G C pTs rT mxs mxl ins cert"
+ "\<lbrakk> wt_method G C pTs rT mxs mxl ins phi; fits ins cert phi \<rbrakk>
+ \<Longrightarrow> wtl_method G C pTs rT mxs mxl ins cert"
by (simp add: wt_method_def wtl_method_def)
(rule wt_imp_wtl_inst_list [rule_format, elim_format], auto simp add: wt_start_def)
lemma wtl_method_complete:
"wt_method G C pTs rT mxs mxl ins phi
- ==> wtl_method G C pTs rT mxs mxl ins (make_cert ins phi)"
+ \<Longrightarrow> wtl_method G C pTs rT mxs mxl ins (make_cert ins phi)"
proof -
assume "wt_method G C pTs rT mxs mxl ins phi"
moreover
@@ -419,7 +419,7 @@
theorem wtl_complete:
- "wt_jvm_prog G Phi ==> wtl_jvm_prog G (make_Cert G Phi)"
+ "wt_jvm_prog G Phi \<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)"
proof -
assume wt: "wt_jvm_prog G Phi"
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Sun Mar 03 16:59:08 2002 +0100
@@ -17,40 +17,40 @@
lemmas [simp del] = split_paired_Ex split_paired_All
constdefs
-fits :: "[method_type,instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] => bool"
+fits :: "[method_type,instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] \<Rightarrow> bool"
"fits phi is G rT s0 maxs maxr et cert ==
- (\<forall>pc s1. pc < length is -->
- (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0 = OK s1 -->
- (case cert!pc of None => phi!pc = s1
- | Some t => phi!pc = Some t)))"
+ (\<forall>pc s1. pc < length is \<longrightarrow>
+ (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0 = OK s1 \<longrightarrow>
+ (case cert!pc of None \<Rightarrow> phi!pc = s1
+ | Some t \<Rightarrow> phi!pc = Some t)))"
constdefs
-make_phi :: "[instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] => method_type"
+make_phi :: "[instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] \<Rightarrow> method_type"
"make_phi is G rT s0 maxs maxr et cert ==
map (\<lambda>pc. case cert!pc of
- None => ok_val (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0)
- | Some t => Some t) [0..length is(]"
+ None \<Rightarrow> ok_val (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0)
+ | Some t \<Rightarrow> Some t) [0..length is(]"
lemma fitsD_None:
- "[|fits phi is G rT s0 mxs mxr et cert; pc < length is;
+ "\<lbrakk>fits phi is G rT s0 mxs mxr et cert; pc < length is;
wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0 = OK s1;
- cert ! pc = None|] ==> phi!pc = s1"
+ cert ! pc = None\<rbrakk> \<Longrightarrow> phi!pc = s1"
by (auto simp add: fits_def)
lemma fitsD_Some:
- "[|fits phi is G rT s0 mxs mxr et cert; pc < length is;
+ "\<lbrakk>fits phi is G rT s0 mxs mxr et cert; pc < length is;
wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0 = OK s1;
- cert ! pc = Some t|] ==> phi!pc = Some t"
+ cert ! pc = Some t\<rbrakk> \<Longrightarrow> phi!pc = Some t"
by (auto simp add: fits_def)
lemma make_phi_Some:
- "[| pc < length is; cert!pc = Some t |] ==>
+ "\<lbrakk> pc < length is; cert!pc = Some t \<rbrakk> \<Longrightarrow>
make_phi is G rT s0 mxs mxr et cert ! pc = Some t"
by (simp add: make_phi_def)
lemma make_phi_None:
- "[| pc < length is; cert!pc = None |] ==>
+ "\<lbrakk> pc < length is; cert!pc = None \<rbrakk> \<Longrightarrow>
make_phi is G rT s0 mxs mxr et cert ! pc =
ok_val (wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0)"
by (simp add: make_phi_def)
@@ -65,8 +65,8 @@
qed
lemma fits_lemma1:
- "[| 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 |]
- ==> \<forall>pc t. pc < length is --> cert!pc = Some t --> phi!pc = Some t"
+ "\<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>
+ \<Longrightarrow> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t"
proof (intro strip)
fix pc t
assume "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'"
@@ -83,10 +83,10 @@
lemma wtl_suc_pc:
- "[| wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
+ "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s';
wtl_cert (is!pc) G rT s' cert mxs mxr (length is) et pc = OK s'';
- fits phi is G rT s mxs mxr et cert; Suc pc < length is |] ==>
+ fits phi is G rT s mxs mxr et cert; Suc pc < length is \<rbrakk> \<Longrightarrow>
G \<turnstile> s'' <=' phi ! Suc pc"
proof -
@@ -117,15 +117,15 @@
"wtl_cert l G rT s'' cert mxs mxr (length is) et (Suc pc) = OK x"
by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
- hence c1: "!!t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
+ hence c1: "\<And>t. cert!Suc pc = Some t \<Longrightarrow> G \<turnstile> s'' <=' cert!Suc pc"
by (simp add: wtl_cert_def split: split_if_asm)
moreover
from fits pc wts
- have c2: "!!t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
+ have c2: "\<And>t. cert!Suc pc = Some t \<Longrightarrow> phi!Suc pc = cert!Suc pc"
by - (drule fitsD_Some, auto)
moreover
from fits pc wts
- have c3: "cert!Suc pc = None ==> phi!Suc pc = s''"
+ have c3: "cert!Suc pc = None \<Longrightarrow> phi!Suc pc = s''"
by (rule fitsD_None)
ultimately
show ?thesis by (cases "cert!Suc pc", auto)
@@ -133,8 +133,8 @@
lemma wtl_fits_wt:
- "[| wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
- fits phi is G rT s mxs mxr et cert; pc < length is |] ==>
+ "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
+ fits phi is G rT s mxs mxr et cert; pc < length is \<rbrakk> \<Longrightarrow>
wt_instr (is!pc) G rT phi mxs (length is) et pc"
proof -
assume fits: "fits phi is G rT s mxs mxr et cert"
@@ -146,10 +146,10 @@
by - (drule wtl_all, auto)
from fits wtl pc have cert_Some:
- "!!t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
+ "\<And>t pc. \<lbrakk> pc < length is; cert!pc = Some t \<rbrakk> \<Longrightarrow> phi!pc = Some t"
by (auto dest: fits_lemma1)
- from fits wtl pc have cert_None: "cert!pc = None ==> phi!pc = s'"
+ from fits wtl pc have cert_None: "cert!pc = None \<Longrightarrow> phi!pc = s'"
by - (drule fitsD_None)
from pc c cert_None cert_Some
@@ -169,8 +169,8 @@
case False
with wti pc'
have G: "G \<turnstile> r <=' cert ! pc'" by (simp add: wtl_inst_OK) blast
- hence "cert!pc' = None ==> r = None" by simp
- hence "cert!pc' = None ==> ?thesis" by simp
+ hence "cert!pc' = None \<Longrightarrow> r = None" by simp
+ hence "cert!pc' = None \<Longrightarrow> ?thesis" by simp
moreover {
fix t assume "cert!pc' = Some t"
with less have "phi!pc' = cert!pc'" by (simp add: cert_Some)
@@ -183,7 +183,7 @@
have "G \<turnstile> r <=' s''" sorry
also
from wtl w fits c pc
- have "Suc pc < length is ==> G \<turnstile> s'' <=' phi ! Suc pc"
+ have "Suc pc < length is \<Longrightarrow> G \<turnstile> s'' <=' phi ! Suc pc"
by - (rule wtl_suc_pc)
with True less
have "G \<turnstile> s'' <=' phi ! Suc pc" by blast
@@ -197,8 +197,8 @@
lemma fits_first:
- "[| 0 < length is; wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
- fits phi is G rT s mxs mxr et cert |] ==>
+ "\<lbrakk> 0 < length is; wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
+ fits phi is G rT s mxs mxr et cert \<rbrakk> \<Longrightarrow>
G \<turnstile> s <=' phi ! 0"
proof -
assume wtl: "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
@@ -210,11 +210,11 @@
by simp
with fits pc
- have "cert!0 = None ==> phi!0 = s"
+ have "cert!0 = None \<Longrightarrow> phi!0 = s"
by (rule fitsD_None)
moreover
from fits pc wt0
- have "!!t. cert!0 = Some t ==> phi!0 = cert!0"
+ have "\<And>t. cert!0 = Some t \<Longrightarrow> phi!0 = cert!0"
by - (drule fitsD_Some, auto)
moreover
from pc
@@ -225,7 +225,7 @@
"wtl_cert x G rT s cert mxs mxr (length is) et 0 = OK s'"
by auto
hence
- "!!t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
+ "\<And>t. cert!0 = Some t \<Longrightarrow> G \<turnstile> s <=' cert!0"
by (simp add: wtl_cert_def split: split_if_asm)
ultimately
@@ -235,7 +235,7 @@
lemma wtl_method_correct:
-"wtl_method G C pTs rT mxs mxl et ins cert ==> \<exists> phi. wt_method G C pTs rT mxs mxl ins et phi"
+"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"
proof (unfold wtl_method_def, simp only: Let_def, elim conjE)
let "?s0" = "Some ([], OK (Class C) # map OK pTs @ replicate mxl Err)"
assume pc: "0 < length ins"
@@ -246,7 +246,7 @@
with wtl
have allpc:
- "\<forall>pc. pc < length ins --> wt_instr (ins ! pc) G rT phi mxs (length ins) et pc"
+ "\<forall>pc. pc < length ins \<longrightarrow> wt_instr (ins ! pc) G rT phi mxs (length ins) et pc"
by (blast intro: wtl_fits_wt)
from pc wtl fits
@@ -259,7 +259,7 @@
theorem wtl_correct:
- "wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
+ "wtl_jvm_prog G cert \<Longrightarrow> \<exists> Phi. wt_jvm_prog G Phi"
proof -
assume wtl: "wtl_jvm_prog G cert"
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Sun Mar 03 16:59:08 2002 +0100
@@ -22,8 +22,8 @@
types
certificate = "state_type option list"
- class_certificate = "sig => certificate"
- prog_certificate = "cname => class_certificate"
+ class_certificate = "sig \<Rightarrow> certificate"
+ prog_certificate = "cname \<Rightarrow> class_certificate"
consts
merge :: "[jvm_prog, p_count, nat, nat, p_count, certificate, (nat \<times> (state_type option)) list, state] \<Rightarrow> state"
@@ -38,24 +38,24 @@
constdefs
wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count]
- => state_type option err"
+ \<Rightarrow> state_type option err"
"wtl_inst i G rT s cert maxs maxr max_pc et pc ==
if app i G maxs rT pc et s then
merge G pc maxs maxr max_pc cert (eff i G pc et s) (OK (cert!(pc+1)))
else Err"
wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count]
- => state_type option err"
+ \<Rightarrow> state_type option err"
"wtl_cert i G rT s cert maxs maxr max_pc et pc ==
case cert!pc of
- None => wtl_inst i G rT s cert maxs maxr max_pc et pc
- | Some s' => if G \<turnstile> s <=' (Some s') then
+ None \<Rightarrow> wtl_inst i G rT s cert maxs maxr max_pc et pc
+ | Some s' \<Rightarrow> if G \<turnstile> s <=' (Some s') then
wtl_inst i G rT (Some s') cert maxs maxr max_pc et pc
else Err"
consts
wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,nat,p_count,exception_table,p_count,
- state_type option] => state_type option err"
+ state_type option] \<Rightarrow> state_type option err"
primrec
"wtl_inst_list [] G rT cert maxs maxr max_pc et pc s = OK s"
"wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s =
@@ -64,7 +64,7 @@
constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,exception_table,instr list,certificate] => bool"
+ wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,exception_table,instr list,certificate] \<Rightarrow> bool"
"wtl_method G C pTs rT mxs mxl et ins cert ==
let max_pc = length ins
in
@@ -72,7 +72,7 @@
wtl_inst_list ins G rT cert mxs mxl max_pc et 0
(Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \<noteq> Err"
- wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool"
+ wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool"
"wtl_jvm_prog G cert ==
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"
@@ -84,12 +84,12 @@
by simp
lemma merge_def:
- "!!x. merge G pc mxs mxr max_pc cert ss x =
+ "\<And>x. merge G pc mxs mxr max_pc cert ss x =
(if \<forall>(pc',s') \<in> set ss. pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> s' <=' cert!pc') then
map (OK \<circ> snd) [(p',t') \<in> ss. p'=pc+1] ++_(sup G mxs mxr) x
- else Err)" (is "!!x. ?merge ss x = ?if ss x" is "!!x. ?P ss x")
+ else Err)" (is "\<And>x. ?merge ss x = ?if ss x" is "\<And>x. ?P ss x")
proof (induct ss)
- show "!!x. ?P [] x" by simp
+ show "\<And>x. ?P [] x" by simp
next
have OK_snd: "(\<lambda>u. OK (snd u)) = OK \<circ> snd" by (rule ext) auto
fix x ss and s::"nat \<times> (state_type option)"
@@ -173,7 +173,7 @@
qed
lemma wtl_take:
- "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s'' ==>
+ "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s'' \<Longrightarrow>
\<exists>s'. wtl_inst_list (take pc' is) G rT cert mxs mxr mpc et pc s = OK s'"
proof -
assume "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s''"
@@ -183,7 +183,7 @@
qed
lemma take_Suc:
- "\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
+ "\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
proof (induct l)
show "?P []" by simp
next
@@ -197,9 +197,9 @@
qed
lemma wtl_Suc:
- "[| wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s';
+ "\<lbrakk> wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s';
wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s'';
- Suc pc < length is |] ==>
+ Suc pc < length is \<rbrakk> \<Longrightarrow>
wtl_inst_list (take (Suc pc) is) G rT cert maxs maxr (length is) et 0 s = OK s''"
proof -
assume "wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'"
@@ -210,8 +210,8 @@
qed
lemma wtl_all:
- "[| wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err;
- pc < length is |] ==>
+ "\<lbrakk> wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err;
+ pc < length is \<rbrakk> \<Longrightarrow>
\<exists>s' s''. wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s' \<and>
wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
proof -
--- a/src/HOL/MicroJava/BV/Listn.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy Sun Mar 03 16:59:08 2002 +0100
@@ -12,41 +12,41 @@
constdefs
- list :: "nat => 'a set => 'a list set"
+ list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set"
"list n A == {xs. length xs = n & set xs <= A}"
- le :: "'a ord => ('a list)ord"
+ le :: "'a ord \<Rightarrow> ('a list)ord"
"le r == list_all2 (%x y. x <=_r y)"
-syntax "@lesublist" :: "'a list => 'a ord => 'a list => bool"
+syntax "@lesublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
("(_ /<=[_] _)" [50, 0, 51] 50)
-syntax "@lesssublist" :: "'a list => 'a ord => 'a list => bool"
+syntax "@lesssublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
("(_ /<[_] _)" [50, 0, 51] 50)
translations
"x <=[r] y" == "x <=_(Listn.le r) y"
"x <[r] y" == "x <_(Listn.le r) y"
constdefs
- map2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
+ map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
"map2 f == (%xs ys. map (split f) (zip xs ys))"
-syntax "@plussublist" :: "'a list => ('a => 'b => 'c) => 'b list => 'c list"
+syntax "@plussublist" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
("(_ /+[_] _)" [65, 0, 66] 65)
translations "x +[f] y" == "x +_(map2 f) y"
-consts coalesce :: "'a err list => 'a list err"
+consts coalesce :: "'a err list \<Rightarrow> 'a list err"
primrec
"coalesce [] = OK[]"
"coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"
constdefs
- sl :: "nat => 'a sl => 'a list sl"
+ sl :: "nat \<Rightarrow> 'a sl \<Rightarrow> 'a list sl"
"sl n == %(A,r,f). (list n A, le r, map2 f)"
- sup :: "('a => 'b => 'c err) => 'a list => 'b list => 'c list err"
+ sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list err"
"sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
- upto_esl :: "nat => 'a esl => 'a list esl"
+ upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl"
"upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"
lemmas [simp] = set_update_subsetI
@@ -75,7 +75,7 @@
done
lemma Cons_less_Conss [simp]:
- "order r ==>
+ "order r \<Longrightarrow>
x#xs <_(Listn.le r) y#ys =
(x <_r y & xs <=[r] ys | x = y & xs <_(Listn.le r) ys)"
apply (unfold lesssub_def)
@@ -83,7 +83,7 @@
done
lemma list_update_le_cong:
- "[| i<size xs; xs <=[r] ys; x <=_r y |] ==> xs[i:=x] <=[r] ys[i:=y]";
+ "\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]";
apply (unfold unfold_lesub_list)
apply (unfold Listn.le_def)
apply (simp add: list_all2_conv_all_nth nth_list_update)
@@ -91,19 +91,19 @@
lemma le_listD:
- "[| xs <=[r] ys; p < size xs |] ==> xs!p <=_r ys!p"
+ "\<lbrakk> xs <=[r] ys; p < size xs \<rbrakk> \<Longrightarrow> xs!p <=_r ys!p"
apply (unfold Listn.le_def lesub_def)
apply (simp add: list_all2_conv_all_nth)
done
lemma le_list_refl:
- "!x. x <=_r x ==> xs <=[r] xs"
+ "!x. x <=_r x \<Longrightarrow> xs <=[r] xs"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
done
lemma le_list_trans:
- "[| order r; xs <=[r] ys; ys <=[r] zs |] ==> xs <=[r] zs"
+ "\<lbrakk> order r; xs <=[r] ys; ys <=[r] zs \<rbrakk> \<Longrightarrow> xs <=[r] zs"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
apply clarify
@@ -112,7 +112,7 @@
done
lemma le_list_antisym:
- "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys"
+ "\<lbrakk> order r; xs <=[r] ys; ys <=[r] xs \<rbrakk> \<Longrightarrow> xs = ys"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
apply (rule nth_equalityI)
@@ -123,7 +123,7 @@
done
lemma order_listI [simp, intro!]:
- "order r ==> order(Listn.le r)"
+ "order r \<Longrightarrow> order(Listn.le r)"
apply (subst order_def)
apply (blast intro: le_list_refl le_list_trans le_list_antisym
dest: order_refl)
@@ -131,35 +131,35 @@
lemma lesub_list_impl_same_size [simp]:
- "xs <=[r] ys ==> size ys = size xs"
+ "xs <=[r] ys \<Longrightarrow> size ys = size xs"
apply (unfold Listn.le_def lesub_def)
apply (simp add: list_all2_conv_all_nth)
done
lemma lesssub_list_impl_same_size:
- "xs <_(Listn.le r) ys ==> size ys = size xs"
+ "xs <_(Listn.le r) ys \<Longrightarrow> size ys = size xs"
apply (unfold lesssub_def)
apply auto
done
lemma listI:
- "[| length xs = n; set xs <= A |] ==> xs : list n A"
+ "\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A"
apply (unfold list_def)
apply blast
done
lemma listE_length [simp]:
- "xs : list n A ==> length xs = n"
+ "xs : list n A \<Longrightarrow> length xs = n"
apply (unfold list_def)
apply blast
done
lemma less_lengthI:
- "[| xs : list n A; p < n |] ==> p < length xs"
+ "\<lbrakk> xs : list n A; p < n \<rbrakk> \<Longrightarrow> p < length xs"
by simp
lemma listE_set [simp]:
- "xs : list n A ==> set xs <= A"
+ "xs : list n A \<Longrightarrow> set xs <= A"
apply (unfold list_def)
apply blast
done
@@ -183,7 +183,7 @@
done
lemma list_not_empty:
- "? a. a:A ==> ? xs. xs : list n A";
+ "? a. a:A \<Longrightarrow> ? xs. xs : list n A";
apply (induct "n")
apply simp
apply (simp add: in_list_Suc_iff)
@@ -192,18 +192,18 @@
lemma nth_in [rule_format, simp]:
- "!i n. length xs = n --> set xs <= A --> i < n --> (xs!i) : A"
+ "!i n. length xs = n \<longrightarrow> set xs <= A \<longrightarrow> i < n \<longrightarrow> (xs!i) : A"
apply (induct "xs")
apply simp
apply (simp add: nth_Cons split: nat.split)
done
lemma listE_nth_in:
- "[| xs : list n A; i < n |] ==> (xs!i) : A"
+ "\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A"
by auto
lemma listt_update_in_list [simp, intro!]:
- "[| xs : list n A; x:A |] ==> xs[i := x] : list n A"
+ "\<lbrakk> xs : list n A; x:A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
apply (unfold list_def)
apply simp
done
@@ -215,7 +215,7 @@
done
lemma plus_list_Cons [simp]:
- "(x#xs) +[f] ys = (case ys of [] => [] | y#ys => (x +_f y)#(xs +[f] ys))"
+ "(x#xs) +[f] ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x +_f y)#(xs +[f] ys))"
by (simp add: plussub_def map2_def split: list.split)
lemma length_plus_list [rule_format, simp]:
@@ -227,7 +227,7 @@
done
lemma nth_plus_list [rule_format, simp]:
- "!xs ys i. length xs = n --> length ys = n --> i<n -->
+ "!xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i<n \<longrightarrow>
(xs +[f] ys)!i = (xs!i) +_f (ys!i)"
apply (induct n)
apply simp
@@ -239,30 +239,30 @@
lemma plus_list_ub1 [rule_format]:
- "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |]
- ==> xs <=[r] xs +[f] ys"
+ "\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
+ \<Longrightarrow> xs <=[r] xs +[f] ys"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
done
lemma plus_list_ub2:
- "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |]
- ==> ys <=[r] xs +[f] ys"
+ "\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
+ \<Longrightarrow> ys <=[r] xs +[f] ys"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
done
lemma plus_list_lub [rule_format]:
- "semilat(A,r,f) ==> !xs ys zs. set xs <= A --> set ys <= A --> set zs <= A
- --> size xs = n & size ys = n -->
- xs <=[r] zs & ys <=[r] zs --> xs +[f] ys <=[r] zs"
+ "semilat(A,r,f) \<Longrightarrow> !xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A
+ \<longrightarrow> size xs = n & size ys = n \<longrightarrow>
+ xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
done
lemma list_update_incr [rule_format]:
- "[| semilat(A,r,f); x:A |] ==> set xs <= A -->
- (!i. i<size xs --> xs <=[r] xs[i := x +_f xs!i])"
+ "\<lbrakk> semilat(A,r,f); x:A \<rbrakk> \<Longrightarrow> set xs <= A \<longrightarrow>
+ (!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
apply (induct xs)
@@ -273,7 +273,7 @@
done
lemma acc_le_listI [intro!]:
- "[| order r; acc r |] ==> acc(Listn.le r)"
+ "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
apply (unfold acc_def)
apply (subgoal_tac
"wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})")
@@ -323,7 +323,7 @@
done
lemma closed_listI:
- "closed S f ==> closed (list n S) (map2 f)"
+ "closed S f \<Longrightarrow> closed (list n S) (map2 f)"
apply (unfold closed_def)
apply (induct n)
apply simp
@@ -335,7 +335,7 @@
lemma semilat_Listn_sl:
- "!!L. semilat L ==> semilat (Listn.sl n L)"
+ "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
apply (unfold Listn.sl_def)
apply (simp (no_asm_simp) only: split_tupled_all)
apply (simp (no_asm) only: semilat_Def split_conv)
@@ -349,7 +349,7 @@
lemma coalesce_in_err_list [rule_format]:
- "!xes. xes : list n (err A) --> coalesce xes : err(list n A)"
+ "!xes. xes : list n (err A) \<longrightarrow> coalesce xes : err(list n A)"
apply (induct n)
apply simp
apply clarify
@@ -359,13 +359,13 @@
apply force
done
-lemma lem: "!!x xs. x +_(op #) xs = x#xs"
+lemma lem: "\<And>x xs. x +_(op #) xs = x#xs"
by (simp add: plussub_def)
lemma coalesce_eq_OK1_D [rule_format]:
- "semilat(err A, Err.le r, lift2 f) ==>
- !xs. xs : list n A --> (!ys. ys : list n A -->
- (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))"
+ "semilat(err A, Err.le r, lift2 f) \<Longrightarrow>
+ !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow>
+ (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> xs <=[r] zs))"
apply (induct n)
apply simp
apply clarify
@@ -376,9 +376,9 @@
done
lemma coalesce_eq_OK2_D [rule_format]:
- "semilat(err A, Err.le r, lift2 f) ==>
- !xs. xs : list n A --> (!ys. ys : list n A -->
- (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))"
+ "semilat(err A, Err.le r, lift2 f) \<Longrightarrow>
+ !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow>
+ (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> ys <=[r] zs))"
apply (induct n)
apply simp
apply clarify
@@ -389,8 +389,8 @@
done
lemma lift2_le_ub:
- "[| semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z;
- u:A; x <=_r u; y <=_r u |] ==> z <=_r u"
+ "\<lbrakk> semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z;
+ u:A; x <=_r u; y <=_r u \<rbrakk> \<Longrightarrow> z <=_r u"
apply (unfold semilat_Def plussub_def err_def)
apply (simp add: lift2_def)
apply clarify
@@ -401,10 +401,10 @@
done
lemma coalesce_eq_OK_ub_D [rule_format]:
- "semilat(err A, Err.le r, lift2 f) ==>
- !xs. xs : list n A --> (!ys. ys : list n A -->
+ "semilat(err A, Err.le r, lift2 f) \<Longrightarrow>
+ !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow>
(!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us
- & us : list n A --> zs <=[r] us))"
+ & us : list n A \<longrightarrow> zs <=[r] us))"
apply (induct n)
apply simp
apply clarify
@@ -418,15 +418,15 @@
done
lemma lift2_eq_ErrD:
- "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A |]
- ==> ~(? u:A. x <=_r u & y <=_r u)"
+ "\<lbrakk> x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A \<rbrakk>
+ \<Longrightarrow> ~(? u:A. x <=_r u & y <=_r u)"
by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])
lemma coalesce_eq_Err_D [rule_format]:
- "[| semilat(err A, Err.le r, lift2 f) |]
- ==> !xs. xs:list n A --> (!ys. ys:list n A -->
- coalesce (xs +[f] ys) = Err -->
+ "\<lbrakk> semilat(err A, Err.le r, lift2 f) \<rbrakk>
+ \<Longrightarrow> !xs. xs:list n A \<longrightarrow> (!ys. ys:list n A \<longrightarrow>
+ coalesce (xs +[f] ys) = Err \<longrightarrow>
~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))"
apply (induct n)
apply simp
@@ -445,8 +445,8 @@
done
lemma closed_map2_list [rule_format]:
- "closed (err A) (lift2 f) ==>
- !xs. xs : list n A --> (!ys. ys : list n A -->
+ "closed (err A) (lift2 f) \<Longrightarrow>
+ !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow>
map2 f xs ys : list n (err A))"
apply (unfold map2_def)
apply (induct n)
@@ -458,14 +458,14 @@
done
lemma closed_lift2_sup:
- "closed (err A) (lift2 f) ==>
+ "closed (err A) (lift2 f) \<Longrightarrow>
closed (err (list n A)) (lift2 (sup f))"
by (fastsimp simp add: closed_def plussub_def sup_def lift2_def
coalesce_in_err_list closed_map2_list
split: err.split)
lemma err_semilat_sup:
- "err_semilat (A,r,f) ==>
+ "err_semilat (A,r,f) \<Longrightarrow>
err_semilat (list n A, Listn.le r, sup f)"
apply (unfold Err.sl_def)
apply (simp only: split_conv)
@@ -480,7 +480,7 @@
done
lemma err_semilat_upto_esl:
- "!!L. err_semilat L ==> err_semilat(upto_esl m L)"
+ "\<And>L. err_semilat L \<Longrightarrow> err_semilat(upto_esl m L)"
apply (unfold Listn.upto_esl_def)
apply (simp (no_asm_simp) only: split_tupled_all)
apply simp
--- a/src/HOL/MicroJava/BV/Opt.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy Sun Mar 03 16:59:08 2002 +0100
@@ -11,49 +11,49 @@
theory Opt = Err:
constdefs
- le :: "'a ord => 'a option ord"
-"le r o1 o2 == case o2 of None => o1=None |
- Some y => (case o1 of None => True
- | Some x => x <=_r y)"
+ le :: "'a ord \<Rightarrow> 'a option ord"
+"le r o1 o2 == case o2 of None \<Rightarrow> o1=None |
+ Some y \<Rightarrow> (case o1 of None \<Rightarrow> True
+ | Some x \<Rightarrow> x <=_r y)"
- opt :: "'a set => 'a option set"
+ opt :: "'a set \<Rightarrow> 'a option set"
"opt A == insert None {x . ? y:A. x = Some y}"
- sup :: "'a ebinop => 'a option ebinop"
+ sup :: "'a ebinop \<Rightarrow> 'a option ebinop"
"sup f o1 o2 ==
- case o1 of None => OK o2 | Some x => (case o2 of None => OK o1
- | Some y => (case f x y of Err => Err | OK z => OK (Some z)))"
+ case o1 of None \<Rightarrow> OK o2 | Some x \<Rightarrow> (case o2 of None \<Rightarrow> OK o1
+ | Some y \<Rightarrow> (case f x y of Err \<Rightarrow> Err | OK z \<Rightarrow> OK (Some z)))"
- esl :: "'a esl => 'a option esl"
+ esl :: "'a esl \<Rightarrow> 'a option esl"
"esl == %(A,r,f). (opt A, le r, sup f)"
lemma unfold_le_opt:
"o1 <=_(le r) o2 =
- (case o2 of None => o1=None |
- Some y => (case o1 of None => True | Some x => x <=_r y))"
+ (case o2 of None \<Rightarrow> o1=None |
+ Some y \<Rightarrow> (case o1 of None \<Rightarrow> True | Some x \<Rightarrow> x <=_r y))"
apply (unfold lesub_def le_def)
apply (rule refl)
done
lemma le_opt_refl:
- "order r ==> o1 <=_(le r) o1"
+ "order r \<Longrightarrow> o1 <=_(le r) o1"
by (simp add: unfold_le_opt split: option.split)
lemma le_opt_trans [rule_format]:
- "order r ==>
- o1 <=_(le r) o2 --> o2 <=_(le r) o3 --> o1 <=_(le r) o3"
+ "order r \<Longrightarrow>
+ o1 <=_(le r) o2 \<longrightarrow> o2 <=_(le r) o3 \<longrightarrow> o1 <=_(le r) o3"
apply (simp add: unfold_le_opt split: option.split)
apply (blast intro: order_trans)
done
lemma le_opt_antisym [rule_format]:
- "order r ==> o1 <=_(le r) o2 --> o2 <=_(le r) o1 --> o1=o2"
+ "order r \<Longrightarrow> o1 <=_(le r) o2 \<longrightarrow> o2 <=_(le r) o1 \<longrightarrow> o1=o2"
apply (simp add: unfold_le_opt split: option.split)
apply (blast intro: order_antisym)
done
lemma order_le_opt [intro!,simp]:
- "order r ==> order(le r)"
+ "order r \<Longrightarrow> order(le r)"
apply (subst order_def)
apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
done
@@ -102,7 +102,7 @@
lemma semilat_opt:
- "!!L. err_semilat L ==> err_semilat (Opt.esl L)"
+ "\<And>L. err_semilat L \<Longrightarrow> err_semilat (Opt.esl L)"
proof (unfold Opt.esl_def Err.sl_def, simp add: split_tupled_all)
fix A r f
@@ -141,11 +141,11 @@
assume ab: "x = OK a" "y = OK b"
with x
- have a: "!!c. a = Some c ==> c : A"
+ have a: "\<And>c. a = Some c \<Longrightarrow> c : A"
by (clarsimp simp add: opt_def)
from ab y
- have b: "!!d. b = Some d ==> d : A"
+ have b: "\<And>d. b = Some d \<Longrightarrow> d : A"
by (clarsimp simp add: opt_def)
{ fix c d assume "a = Some c" "b = Some d"
@@ -225,10 +225,10 @@
obtain "OK d:err A" "OK e:err A" "OK g:err A"
by simp
with lub
- have "[| (OK d) <=_(Err.le r) (OK g); (OK e) <=_(Err.le r) (OK g) |]
- ==> (OK d) +_(lift2 f) (OK e) <=_(Err.le r) (OK g)"
+ have "\<lbrakk> (OK d) <=_(Err.le r) (OK g); (OK e) <=_(Err.le r) (OK g) \<rbrakk>
+ \<Longrightarrow> (OK d) +_(lift2 f) (OK e) <=_(Err.le r) (OK g)"
by blast
- hence "[| d <=_r g; e <=_r g |] ==> \<exists>y. d +_f e = OK y \<and> y <=_r g"
+ hence "\<lbrakk> d <=_r g; e <=_r g \<rbrakk> \<Longrightarrow> \<exists>y. d +_f e = OK y \<and> y <=_r g"
by simp
with ok some xyz xz yz
@@ -263,14 +263,14 @@
done
lemma Top_le_conv:
- "[| order r; top r T |] ==> (T <=_r x) = (x = T)"
+ "\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T <=_r x) = (x = T)"
apply (unfold top_def)
apply (blast intro: order_antisym)
done
lemma acc_le_optI [intro!]:
- "acc r ==> acc(le r)"
+ "acc r \<Longrightarrow> acc(le r)"
apply (unfold acc_def lesub_def le_def lesssub_def)
apply (simp add: wf_eq_minimal split: option.split)
apply clarify
@@ -283,8 +283,8 @@
done
lemma option_map_in_optionI:
- "[| ox : opt S; !x:S. ox = Some x --> f x : S |]
- ==> option_map f ox : opt S";
+ "\<lbrakk> ox : opt S; !x:S. ox = Some x \<longrightarrow> f x : S \<rbrakk>
+ \<Longrightarrow> option_map f ox : opt S";
apply (unfold option_map_def)
apply (simp split: option.split)
apply blast
--- a/src/HOL/MicroJava/BV/Product.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy Sun Mar 03 16:59:08 2002 +0100
@@ -11,16 +11,16 @@
theory Product = Err:
constdefs
- le :: "'a ord => 'b ord => ('a * 'b) ord"
+ le :: "'a ord \<Rightarrow> 'b ord \<Rightarrow> ('a * 'b) ord"
"le rA rB == %(a,b) (a',b'). a <=_rA a' & b <=_rB b'"
- sup :: "'a ebinop => 'b ebinop => ('a * 'b)ebinop"
+ sup :: "'a ebinop \<Rightarrow> 'b ebinop \<Rightarrow> ('a * 'b)ebinop"
"sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)"
- esl :: "'a esl => 'b esl => ('a * 'b ) esl"
+ esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl"
"esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
-syntax "@lesubprod" :: "'a*'b => 'a ord => 'b ord => 'b => bool"
+syntax "@lesubprod" :: "'a*'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'b \<Rightarrow> bool"
("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
@@ -49,7 +49,7 @@
lemma acc_le_prodI [intro!]:
- "[| acc rA; acc rB |] ==> acc(Product.le rA rB)"
+ "\<lbrakk> acc rA; acc rB \<rbrakk> \<Longrightarrow> acc(Product.le rA rB)"
apply (unfold acc_def)
apply (rule wf_subset)
apply (erule wf_lex_prod)
@@ -59,7 +59,7 @@
lemma closed_lift2_sup:
- "[| closed (err A) (lift2 f); closed (err B) (lift2 g) |] ==>
+ "\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow>
closed (err(A<*>B)) (lift2(sup f g))";
apply (unfold closed_def plussub_def lift2_def err_def sup_def)
apply (simp split: err.split)
@@ -72,12 +72,12 @@
lemma plus_eq_Err_conv [simp]:
- "[| x:A; y:A; semilat(err A, Err.le r, lift2 f) |]
- ==> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
+ "\<lbrakk> x:A; y:A; semilat(err A, Err.le r, lift2 f) \<rbrakk>
+ \<Longrightarrow> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
proof -
have plus_le_conv2:
- "!!r f z. [| z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
- OK x +_f OK y <=_r z|] ==> OK x <=_r z \<and> OK y <=_r z"
+ "\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
+ OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
by (rule plus_le_conv [THEN iffD1])
case rule_context
thus ?thesis
@@ -110,7 +110,7 @@
qed
lemma err_semilat_Product_esl:
- "!!L1 L2. [| err_semilat L1; err_semilat L2 |] ==> err_semilat(Product.esl L1 L2)"
+ "\<And>L1 L2. \<lbrakk> err_semilat L1; err_semilat L2 \<rbrakk> \<Longrightarrow> err_semilat(Product.esl L1 L2)"
apply (unfold esl_def Err.sl_def)
apply (simp (no_asm_simp) only: split_tupled_all)
apply simp
--- a/src/HOL/MicroJava/BV/Semilat.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy Sun Mar 03 16:59:08 2002 +0100
@@ -13,134 +13,134 @@
theory Semilat = While_Combinator:
-types 'a ord = "'a => 'a => bool"
- 'a binop = "'a => 'a => 'a"
+types 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
'a sl = "'a set * 'a ord * 'a binop"
consts
- "@lesub" :: "'a => 'a ord => 'a => bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
- "@lesssub" :: "'a => 'a ord => 'a => bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
+ "@lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
+ "@lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
defs
lesub_def: "x <=_r y == r x y"
lesssub_def: "x <_r y == x <=_r y & x ~= y"
consts
- "@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
+ "@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
defs
plussub_def: "x +_f y == f x y"
constdefs
- ord :: "('a*'a)set => 'a ord"
+ ord :: "('a*'a)set \<Rightarrow> 'a ord"
"ord r == %x y. (x,y):r"
- order :: "'a ord => bool"
+ order :: "'a ord \<Rightarrow> bool"
"order r == (!x. x <=_r x) &
- (!x y. x <=_r y & y <=_r x --> x=y) &
- (!x y z. x <=_r y & y <=_r z --> x <=_r z)"
+ (!x y. x <=_r y & y <=_r x \<longrightarrow> x=y) &
+ (!x y z. x <=_r y & y <=_r z \<longrightarrow> x <=_r z)"
- acc :: "'a ord => bool"
+ acc :: "'a ord \<Rightarrow> bool"
"acc r == wf{(y,x) . x <_r y}"
- top :: "'a ord => 'a => bool"
+ top :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool"
"top r T == !x. x <=_r T"
- closed :: "'a set => 'a binop => bool"
+ closed :: "'a set \<Rightarrow> 'a binop \<Rightarrow> bool"
"closed A f == !x:A. !y:A. x +_f y : A"
- semilat :: "'a sl => bool"
+ semilat :: "'a sl \<Rightarrow> bool"
"semilat == %(A,r,f). order r & closed A f &
(!x:A. !y:A. x <=_r x +_f y) &
(!x:A. !y:A. y <=_r x +_f y) &
- (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
+ (!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)"
- is_ub :: "('a*'a)set => 'a => 'a => 'a => bool"
+ is_ub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
"is_ub r x y u == (x,u):r & (y,u):r"
- is_lub :: "('a*'a)set => 'a => 'a => 'a => bool"
-"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
+ is_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
- some_lub :: "('a*'a)set => 'a => 'a => 'a"
+ some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
"some_lub r x y == SOME z. is_lub r x y z"
lemma order_refl [simp, intro]:
- "order r ==> x <=_r x";
+ "order r \<Longrightarrow> x <=_r x";
by (simp add: order_def)
lemma order_antisym:
- "[| order r; x <=_r y; y <=_r x |] ==> x = y"
+ "\<lbrakk> order r; x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y"
apply (unfold order_def)
apply (simp (no_asm_simp))
done
lemma order_trans:
- "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z"
+ "\<lbrakk> order r; x <=_r y; y <=_r z \<rbrakk> \<Longrightarrow> x <=_r z"
apply (unfold order_def)
apply blast
done
lemma order_less_irrefl [intro, simp]:
- "order r ==> ~ x <_r x"
+ "order r \<Longrightarrow> ~ x <_r x"
apply (unfold order_def lesssub_def)
apply blast
done
lemma order_less_trans:
- "[| order r; x <_r y; y <_r z |] ==> x <_r z"
+ "\<lbrakk> order r; x <_r y; y <_r z \<rbrakk> \<Longrightarrow> x <_r z"
apply (unfold order_def lesssub_def)
apply blast
done
lemma topD [simp, intro]:
- "top r T ==> x <=_r T"
+ "top r T \<Longrightarrow> x <=_r T"
by (simp add: top_def)
lemma top_le_conv [simp]:
- "[| order r; top r T |] ==> (T <=_r x) = (x = T)"
+ "\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T <=_r x) = (x = T)"
by (blast intro: order_antisym)
lemma semilat_Def:
"semilat(A,r,f) == order r & closed A f &
(!x:A. !y:A. x <=_r x +_f y) &
(!x:A. !y:A. y <=_r x +_f y) &
- (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
+ (!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)"
apply (unfold semilat_def split_conv [THEN eq_reflection])
apply (rule refl [THEN eq_reflection])
done
lemma semilatDorderI [simp, intro]:
- "semilat(A,r,f) ==> order r"
+ "semilat(A,r,f) \<Longrightarrow> order r"
by (simp add: semilat_Def)
lemma semilatDclosedI [simp, intro]:
- "semilat(A,r,f) ==> closed A f"
+ "semilat(A,r,f) \<Longrightarrow> closed A f"
apply (unfold semilat_Def)
apply simp
done
lemma semilat_ub1 [simp]:
- "[| semilat(A,r,f); x:A; y:A |] ==> x <=_r x +_f y"
+ "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
by (unfold semilat_Def, simp)
lemma semilat_ub2 [simp]:
- "[| semilat(A,r,f); x:A; y:A |] ==> y <=_r x +_f y"
+ "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
by (unfold semilat_Def, simp)
lemma semilat_lub [simp]:
- "[| x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A |] ==> x +_f y <=_r z";
+ "\<lbrakk> x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z";
by (unfold semilat_Def, simp)
lemma plus_le_conv [simp]:
- "[| x:A; y:A; z:A; semilat(A,r,f) |]
- ==> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
+ "\<lbrakk> x:A; y:A; z:A; semilat(A,r,f) \<rbrakk>
+ \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
apply (unfold semilat_Def)
apply (blast intro: semilat_ub1 semilat_ub2 semilat_lub order_trans)
done
lemma le_iff_plus_unchanged:
- "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (x +_f y = y)"
+ "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)"
apply (rule iffI)
apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub2, assumption+)
apply (erule subst)
@@ -148,7 +148,7 @@
done
lemma le_iff_plus_unchanged2:
- "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (y +_f x = y)"
+ "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)"
apply (rule iffI)
apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub1, assumption+)
apply (erule subst)
@@ -157,7 +157,7 @@
lemma closedD:
- "[| closed A f; x:A; y:A |] ==> x +_f y : A"
+ "\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A"
apply (unfold closed_def)
apply blast
done
@@ -167,15 +167,15 @@
lemma is_lubD:
- "is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
+ "is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
by (simp add: is_lub_def)
lemma is_ubI:
- "[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u"
+ "\<lbrakk> (x,u) : r; (y,u) : r \<rbrakk> \<Longrightarrow> is_ub r x y u"
by (simp add: is_ub_def)
lemma is_ubD:
- "is_ub r x y u ==> (x,u) : r & (y,u) : r"
+ "is_ub r x y u \<Longrightarrow> (x,u) : r & (y,u) : r"
by (simp add: is_ub_def)
@@ -192,8 +192,8 @@
done
lemma extend_lub:
- "[| single_valued r; is_lub (r^* ) x y u; (x',x) : r |]
- ==> EX v. is_lub (r^* ) x' y v"
+ "\<lbrakk> single_valued r; is_lub (r^* ) x y u; (x',x) : r \<rbrakk>
+ \<Longrightarrow> EX v. is_lub (r^* ) x' y v"
apply (unfold is_lub_def is_ub_def)
apply (case_tac "(y,x) : r^*")
apply (case_tac "(y,x') : r^*")
@@ -207,7 +207,7 @@
done
lemma single_valued_has_lubs [rule_format]:
- "[| single_valued r; (x,u) : r^* |] ==> (!y. (y,u) : r^* -->
+ "\<lbrakk> single_valued r; (x,u) : r^* \<rbrakk> \<Longrightarrow> (!y. (y,u) : r^* \<longrightarrow>
(EX z. is_lub (r^* ) x y z))"
apply (erule converse_rtrancl_induct)
apply clarify
@@ -218,7 +218,7 @@
done
lemma some_lub_conv:
- "[| acyclic r; is_lub (r^* ) x y u |] ==> some_lub (r^* ) x y = u"
+ "\<lbrakk> acyclic r; is_lub (r^* ) x y u \<rbrakk> \<Longrightarrow> some_lub (r^* ) x y = u"
apply (unfold some_lub_def is_lub_def)
apply (rule someI2)
apply assumption
@@ -226,8 +226,8 @@
done
lemma is_lub_some_lub:
- "[| single_valued r; acyclic r; (x,u):r^*; (y,u):r^* |]
- ==> is_lub (r^* ) x y (some_lub (r^* ) x y)";
+ "\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^* \<rbrakk>
+ \<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)";
by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv)
subsection{*An executable lub-finder*}
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy Sun Mar 03 16:59:08 2002 +0100
@@ -15,23 +15,23 @@
's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
constdefs
- bounded :: "'s step_type => nat => bool"
+ bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
"bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"
- stable :: "'s ord => 's step_type => 's list => nat => bool"
+ stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool"
"stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"
- stables :: "'s ord => 's step_type => 's list => bool"
+ stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
"stables r step ss == !p<size ss. stable r step ss p"
- is_bcv :: "'s ord => 's => 's step_type
- => nat => 's set => ('s list => 's list) => bool"
+ is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type
+ \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool"
"is_bcv r T step n A bcv == !ss : list n A.
(!p<n. (bcv ss)!p ~= T) =
(? ts: list n A. ss <=[r] ts & wt_step r T step ts)"
wt_step ::
-"'s ord => 's => 's step_type => 's list => bool"
+"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
"wt_step r T step ts ==
!p<size(ts). ts!p ~= T & stable r step ts p"
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy Sun Mar 03 16:59:08 2002 +0100
@@ -11,10 +11,10 @@
constdefs
-dynamic_wt :: "'s ord => 's err step_type => 's err list => bool"
+dynamic_wt :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool"
"dynamic_wt r step ts == wt_step (Err.le r) Err step ts"
-static_wt :: "'s ord => (nat => 's => bool) => 's step_type => 's list => bool"
+static_wt :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
"static_wt r app step ts ==
\<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)"
@@ -28,14 +28,14 @@
"err_step app step p t == case t of Err \<Rightarrow> map_err (step p arbitrary) | OK t' \<Rightarrow>
if app p t' then map_snd OK (step p t') else map_err (step p t')"
-non_empty :: "'s step_type => bool"
+non_empty :: "'s step_type \<Rightarrow> bool"
"non_empty step == \<forall>p t. step p t \<noteq> []"
lemmas err_step_defs = err_step_def map_snd_def map_err_def
lemma non_emptyD:
- "non_empty step ==> \<exists>q t'. (q,t') \<in> set(step p t)"
+ "non_empty step \<Longrightarrow> \<exists>q t'. (q,t') \<in> set(step p t)"
proof (unfold non_empty_def)
assume "\<forall>p t. step p t \<noteq> []"
hence "step p t \<noteq> []" by blast
@@ -47,9 +47,9 @@
lemma dynamic_imp_static:
- "[| bounded step (size ts); non_empty step;
- dynamic_wt r (err_step app step) ts |]
- ==> static_wt r app step (map ok_val ts)"
+ "\<lbrakk> bounded step (size ts); non_empty step;
+ dynamic_wt r (err_step app step) ts \<rbrakk>
+ \<Longrightarrow> static_wt r app step (map ok_val ts)"
proof (unfold static_wt_def, intro strip, rule conjI)
assume b: "bounded step (size ts)"
@@ -112,8 +112,8 @@
lemma static_imp_dynamic:
- "[| static_wt r app step ts; bounded step (size ts) |]
- ==> dynamic_wt r (err_step app step) (map OK ts)"
+ "\<lbrakk> static_wt r app step ts; bounded step (size ts) \<rbrakk>
+ \<Longrightarrow> dynamic_wt r (err_step app step) (map OK ts)"
proof (unfold dynamic_wt_def wt_step_def, intro strip, rule conjI)
assume bounded: "bounded step (size ts)"
assume static: "static_wt r app step ts"
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Sun Mar 03 16:59:08 2002 +0100
@@ -34,6 +34,6 @@
syntax (xsymbols)
exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
- ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
+ ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
end