--- a/src/HOL/MicroJava/BV/BVSpec.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Thu Sep 21 10:42:49 2000 +0200
@@ -11,53 +11,53 @@
types
method_type = "state_type option list"
- class_type = "sig \<Rightarrow> method_type"
- prog_type = "cname \<Rightarrow> class_type"
+ class_type = "sig => method_type"
+ prog_type = "cname => class_type"
constdefs
-wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] \<Rightarrow> bool"
-"wt_instr i G rT phi max_pc pc \<equiv>
+wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] => bool"
+"wt_instr i G rT phi max_pc pc ==
app i G rT (phi!pc) \<and>
(\<forall> pc' \<in> set (succs i pc). pc' < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!pc'))"
-wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
-"wt_start G C pTs mxl phi \<equiv>
+wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => 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,instr list,method_type] \<Rightarrow> bool"
-"wt_method G C pTs rT mxl ins phi \<equiv>
+wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] => bool"
+"wt_method G C pTs rT mxl ins phi ==
let max_pc = length ins
in
0 < max_pc \<and> wt_start G C pTs mxl phi \<and>
- (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
+ (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi max_pc pc)"
-wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
-"wt_jvm_prog G phi \<equiv>
+wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
+"wt_jvm_prog G phi ==
wf_prog (\<lambda>G C (sig,rT,maxl,b).
wt_method G C (snd sig) rT maxl b (phi C sig)) G"
lemma wt_jvm_progD:
-"wt_jvm_prog G phi \<Longrightarrow> (\<exists>wt. wf_prog wt G)"
+"wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
by (unfold wt_jvm_prog_def, blast)
lemma wt_jvm_prog_impl_wt_instr:
-"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins \<rbrakk>
- \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
+"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins |]
+ ==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
simp, simp add: wf_mdecl_def wt_method_def)
lemma wt_jvm_prog_impl_wt_start:
-"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) \<rbrakk> \<Longrightarrow>
+"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) |] ==>
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 add: wf_mdecl_def wt_method_def)
(* for most instructions wt_instr collapses: *)
lemma
-"succs i pc = [pc+1] \<Longrightarrow> wt_instr i G rT phi max_pc pc =
+"succs i pc = [pc+1] ==> wt_instr i G rT phi max_pc pc =
(app i G rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
by (simp add: wt_instr_def)
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Sep 21 10:42:49 2000 +0200
@@ -24,13 +24,13 @@
done
lemma Load_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins!pc = Load idx;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (rule conjI)
apply (rule approx_loc_imp_approx_val_sup)
@@ -39,13 +39,13 @@
done
lemma Store_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins!pc = Store idx;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (rule conjI)
apply (blast intro: approx_stk_imp_approx_stk_sup)
@@ -54,18 +54,18 @@
lemma conf_Intg_Integer [iff]:
- "G,h \<turnstile> Intg i \<Colon>\<preceq> PrimT Integer"
+ "G,h \<turnstile> Intg i ::\<preceq> PrimT Integer"
by (simp add: conf_def)
lemma Bipush_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins!pc = Bipush i;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
done
@@ -73,7 +73,7 @@
lemma NT_subtype_conv:
"G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))"
proof -
- have "\<And>T T'. G \<turnstile> T' \<preceq> T \<Longrightarrow> T' = NT \<longrightarrow> (T=NT | (\<exists>C. T = Class C))"
+ have "!!T T'. G \<turnstile> T' \<preceq> T ==> T' = NT --> (T=NT | (\<exists>C. T = Class C))"
apply (erule widen.induct)
apply auto
apply (case_tac R)
@@ -86,13 +86,13 @@
qed
lemma Aconst_null_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins!pc = Aconst_null;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (rule conjI)
apply (force simp add: approx_val_Null NT_subtype_conv)
@@ -101,8 +101,8 @@
lemma Cast_conf2:
- "\<lbrakk>wf_prog ok G; G,h\<turnstile>v\<Colon>\<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\<Colon>\<preceq>T"
+ "[|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"
apply (unfold cast_ok_def)
apply (frule widen_Class)
apply (elim exE disjE)
@@ -114,26 +114,26 @@
lemma Checkcast_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins!pc = Checkcast D;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2)
done
lemma Getfield_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins!pc = Getfield F D;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split)
apply (frule conf_widen)
apply assumption+
@@ -147,13 +147,13 @@
done
lemma Putfield_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins!pc = Putfield F D;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split)
apply (clarsimp simp add: approx_val_def)
apply (frule conf_widen)
@@ -174,13 +174,13 @@
by fast
lemma New_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins!pc = New cl_idx;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def
fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1
split: option.split)
@@ -199,13 +199,13 @@
lemmas [simp del] = split_paired_Ex
lemma Invoke_correct:
-"\<lbrakk> wt_jvm_prog G phi;
+"[| wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxl,ins);
ins ! pc = Invoke C' mn pTs;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wtprog: "wt_jvm_prog G phi"
assume method: "method (G,C) sig = Some (C,rT,maxl,ins)"
@@ -282,7 +282,7 @@
by simp
with state' method ins
- have Null_ok: "oX = Null \<Longrightarrow> ?thesis"
+ have Null_ok: "oX = Null ==> ?thesis"
by (simp add: correct_state_def raise_xcpt_def)
{ fix ref
@@ -434,13 +434,13 @@
lemmas [simp del] = map_append
lemma Return_correct:
-"\<lbrakk> wt_jvm_prog G phi;
+"[| wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxl,ins);
ins ! pc = Return;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm)
apply (frule wt_jvm_prog_impl_wt_instr)
apply (assumption, erule Suc_lessD)
@@ -455,102 +455,102 @@
lemmas [simp] = map_append
lemma Goto_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins ! pc = Goto branch;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1)
apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
done
lemma Ifcmpeq_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins ! pc = Ifcmpeq branch;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1)
apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
done
lemma Pop_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins ! pc = Pop;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1)
apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
done
lemma Dup_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins ! pc = Dup;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
simp add: defs1 map_eq_Cons)
done
lemma Dup_x1_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins ! pc = Dup_x1;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
simp add: defs1 map_eq_Cons)
done
lemma Dup_x2_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins ! pc = Dup_x2;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
simp add: defs1 map_eq_Cons)
done
lemma Swap_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins ! pc = Swap;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
simp add: defs1 map_eq_Cons)
done
lemma IAdd_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxl,ins);
ins ! pc = IAdd;
wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup)
done
@@ -559,11 +559,11 @@
(** instr correct **)
lemma instr_correct:
-"\<lbrakk> wt_jvm_prog G phi;
+"[| wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxl,ins);
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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
apply (frule wt_jvm_prog_impl_wt_instr_cor)
apply assumption+
apply (cases "ins!pc")
@@ -583,13 +583,13 @@
lemma correct_state_impl_Some_method:
"G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>
- \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
+ ==> \<exists>meth. method (G,C) sig = Some(C,meth)"
by (auto simp add: correct_state_def Let_def)
lemma BV_correct_1 [rule_format]:
-"\<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>"
+"!!state. [| wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>|]
+ ==> exec (G,state) = Some state' --> G,phi \<turnstile>JVM state'\<surd>"
apply (simp only: split_tupled_all)
apply (rename_tac xp hp frs)
apply (case_tac xp)
@@ -605,12 +605,12 @@
lemma L0:
- "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
+ "[| xp=None; frs\<noteq>[] |] ==> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex)
lemma L1:
- "\<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>"
+ "[|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>"
apply (drule L0)
apply assumption
apply (fast intro: BV_correct_1)
@@ -618,7 +618,7 @@
theorem BV_correct [rule_format]:
-"\<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>"
+"[| wt_jvm_prog G phi; G \<turnstile> s -jvm-> t |] ==> G,phi \<turnstile>JVM s\<surd> --> G,phi \<turnstile>JVM t\<surd>"
apply (unfold exec_all_def)
apply (erule rtrancl_induct)
apply simp
@@ -627,8 +627,8 @@
theorem BV_correct_initial:
-"\<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)))"
+"[| 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> approx_loc G hp loc (snd (the (((phi C) sig) ! pc)))"
apply (drule BV_correct)
apply assumption+
apply (simp add: correct_state_def correct_frame_def split_def split: option.splits)
--- a/src/HOL/MicroJava/BV/Convert.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy Thu Sep 21 10:42:49 2000 +0200
@@ -19,51 +19,52 @@
consts
- strict :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
+ strict :: "('a => 'b err) => ('a err => 'b err)"
primrec
"strict f Err = Err"
"strict f (Ok x) = f x"
-consts
- opt_map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a option \<Rightarrow> 'b option)"
-primrec
- "opt_map f None = None"
- "opt_map f (Some x) = Some (f x)"
consts
- val :: "'a err \<Rightarrow> 'a"
+ val :: "'a err => 'a"
primrec
"val (Ok s) = s"
constdefs
(* lifts a relation to err with Err as top element *)
- lift_top :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> bool)"
- "lift_top P a' a \<equiv> case a of
- Err \<Rightarrow> True
- | Ok t \<Rightarrow> (case a' of Err \<Rightarrow> False | Ok t' \<Rightarrow> P t' t)"
+ lift_top :: "('a => 'b => bool) => ('a err => 'b err => bool)"
+ "lift_top P a' a == case a of
+ Err => True
+ | Ok t => (case a' of Err => False | Ok t' => P t' t)"
(* lifts a relation to option with None as bottom element *)
- lift_bottom :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a option \<Rightarrow> 'b option \<Rightarrow> bool)"
- "lift_bottom P a' a \<equiv> case a' of
- None \<Rightarrow> True
- | Some t' \<Rightarrow> (case a of None \<Rightarrow> False | Some t \<Rightarrow> P t' t)"
+ lift_bottom :: "('a => 'b => bool) => ('a option => 'b option => bool)"
+ "lift_bottom P a' a == case a' of
+ None => True
+ | Some t' => (case a of None => False | Some t => P t' t)"
- sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool" ("_ \<turnstile>_ <=o _")
- "sup_ty_opt G \<equiv> lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
+ sup_ty_opt :: "['code prog,ty err,ty err] => bool" ("_ \<turnstile> _ <=o _" [71,71] 70)
+ "sup_ty_opt G == lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
+
+ sup_loc :: "['code prog,locvars_type,locvars_type] => bool"
+ ("_ \<turnstile> _ <=l _" [71,71] 70)
+ "G \<turnstile> LT <=l LT' == list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
- sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=l _" [71,71] 70)
- "G \<turnstile> LT <=l LT' \<equiv> list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
-
- sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"
+ sup_state :: "['code prog,state_type,state_type] => bool"
("_ \<turnstile> _ <=s _" [71,71] 70)
- "G \<turnstile> s <=s s' \<equiv> (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+ "G \<turnstile> s <=s s' == (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+
+ sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
+ ("_ \<turnstile> _ <=' _" [71,71] 70)
+ "sup_state_opt G == lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
- sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=' _" [71,71] 70)
- "sup_state_opt G \<equiv> lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
-
+syntax (HTML output)
+ sup_ty_opt :: "['code prog,ty err,ty err] => bool" ("_ |- _ <=o _")
+ sup_loc :: "['code prog,locvars_type,locvars_type] => bool" ("_ |- _ <=l _" [71,71] 70)
+ sup_state :: "['code prog,state_type,state_type] => bool" ("_ |- _ <=s _" [71,71] 70)
+ sup_state_opt :: "['code prog,state_type option,state_type option] => bool" ("_ |- _ <=' _" [71,71] 70)
+
lemma not_Err_eq [iff]:
"(x \<noteq> Err) = (\<exists>a. x = Ok a)"
@@ -223,7 +224,7 @@
by (simp add: sup_ty_opt_def)
theorem sup_ty_opt_Ok:
- "G \<turnstile> a <=o (Ok b) \<Longrightarrow> \<exists> x. a = Ok x"
+ "G \<turnstile> a <=o (Ok b) ==> \<exists> x. a = Ok x"
by (clarsimp simp add: sup_ty_opt_def)
lemma widen_PrimT_conv1 [simp]:
@@ -250,10 +251,10 @@
theorem sup_loc_length:
- "G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
+ "G \<turnstile> a <=l b ==> length a = length b"
proof -
assume G: "G \<turnstile> a <=l b"
- have "\<forall> b. (G \<turnstile> a <=l b) \<longrightarrow> length a = length b"
+ have "\<forall> b. (G \<turnstile> a <=l b) --> length a = length b"
by (induct a, auto)
with G
show ?thesis by blast
@@ -263,7 +264,7 @@
"[| G \<turnstile> a <=l b; n < length a |] ==> 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) \<longrightarrow> n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))"
+ have "\<forall> n b. (G \<turnstile> a <=l b) --> n < length a --> (G \<turnstile> (a!n) <=o (b!n))"
(is "?P a")
proof (induct a)
show "?P []" by simp
@@ -285,7 +286,7 @@
theorem all_nth_sup_loc:
- "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) \<longrightarrow>
+ "\<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")
proof (induct a)
show "?P []" by simp
@@ -295,14 +296,14 @@
show "?P (l#ls)"
proof (intro strip)
fix b
- assume f: "\<forall>n. n < length (l # ls) \<longrightarrow> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
+ assume f: "\<forall>n. n < length (l # ls) --> (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 \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
+ have "\<forall>n. n < length ls --> (G \<turnstile> (ls!n) <=o (bs!n))"
by auto
with f b l IH
@@ -318,7 +319,7 @@
proof -
assume l: "length a = length b"
- have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and>
+ have "\<forall>b. length a = length b --> (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
@@ -384,7 +385,7 @@
theorem sup_loc_update [rule_format]:
- "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow>
+ "\<forall> n y. (G \<turnstile> a <=o b) --> n < length y --> (G \<turnstile> x <=l y) -->
(G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
proof (induct x)
show "?P []" by simp
@@ -427,7 +428,7 @@
by (auto simp add: sup_state_def map_eq_Cons sup_loc_Cons2)
theorem sup_state_ignore_fst:
- "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
+ "G \<turnstile> (a, x) <=s (b, y) ==> G \<turnstile> (c, x) <=s (c, y)"
by (simp add: sup_state_def)
theorem sup_state_rev_fst:
@@ -460,15 +461,15 @@
theorem sup_ty_opt_trans [trans]:
- "\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
+ "[|G \<turnstile> a <=o b; G \<turnstile> b <=o c|] ==> G \<turnstile> a <=o c"
by (auto intro: lift_top_trans widen_trans simp add: sup_ty_opt_def)
theorem sup_loc_trans [trans]:
- "\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
+ "[|G \<turnstile> a <=l b; G \<turnstile> b <=l c|] ==> G \<turnstile> a <=l c"
proof -
assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
- hence "\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (c!n))"
+ hence "\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (c!n))"
proof (intro strip)
fix n
assume n: "n < length a"
@@ -490,11 +491,11 @@
theorem sup_state_trans [trans]:
- "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
+ "[|G \<turnstile> a <=s b; G \<turnstile> b <=s c|] ==> G \<turnstile> a <=s c"
by (auto intro: sup_loc_trans simp add: sup_state_def)
theorem sup_state_opt_trans [trans]:
- "\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
+ "[|G \<turnstile> a <=' b; G \<turnstile> b <=' c|] ==> G \<turnstile> a <=' c"
by (auto intro: lift_bottom_trans sup_state_trans simp add: sup_state_opt_def)
--- a/src/HOL/MicroJava/BV/Correct.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Thu Sep 21 10:42:49 2000 +0200
@@ -11,26 +11,26 @@
theory Correct = BVSpec:
constdefs
- approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
-"approx_val G h v any \<equiv> case any of Err \<Rightarrow> True | Ok T \<Rightarrow> G,h\<turnstile>v\<Colon>\<preceq>T"
+ 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_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool"
-"approx_loc G hp loc LT \<equiv> list_all2 (approx_val G hp) loc LT"
+ approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
+"approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
- approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool"
-"approx_stk G hp stk ST \<equiv> approx_loc G hp stk (map Ok ST)"
+ approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
+"approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)"
- correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
-"correct_frame G hp \<equiv> \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
+ correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => 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"
- correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
-"correct_frame_opt G hp s \<equiv> case s of None \<Rightarrow> \<lambda>maxl ins f. False | Some t \<Rightarrow> correct_frame G hp t"
+ correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] => frame => bool"
+"correct_frame_opt G hp s == case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t"
consts
- correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool"
+ correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool"
primrec
"correct_frames G hp phi rT0 sig0 [] = True"
@@ -52,13 +52,13 @@
constdefs
- correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
+ correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
("_,_\<turnstile>JVM _\<surd>" [51,51] 50)
-"correct_state G phi \<equiv> \<lambda>(xp,hp,frs).
+"correct_state G phi == \<lambda>(xp,hp,frs).
case xp of
- None \<Rightarrow> (case frs of
- [] \<Rightarrow> True
- | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and>
+ None => (case frs of
+ [] => True
+ | (f#fs) => G\<turnstile>h hp\<surd> \<and>
(let (stk,loc,C,sig,pc) = f
in
\<exists>rT maxl ins s.
@@ -66,11 +66,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 \<Rightarrow> True"
+ | Some x => True"
lemma sup_heap_newref:
- "hp x = None \<Longrightarrow> hp \<le>| hp(newref hp \<mapsto> obj)"
+ "hp x = None ==> hp \<le>| hp(newref hp \<mapsto> obj)"
apply (unfold hext_def)
apply clarsimp
apply (drule newref_None 1) back
@@ -78,7 +78,7 @@
.
lemma sup_heap_update_value:
- "hp a = Some (C,od') \<Longrightarrow> hp \<le>| hp (a \<mapsto> (C,od))"
+ "hp a = Some (C,od') ==> hp \<le>| hp (a \<mapsto> (C,od))"
by (simp add: hext_def)
@@ -93,29 +93,29 @@
by (auto intro: null simp add: approx_val_def)
lemma approx_val_imp_approx_val_assConvertible [rule_format]:
- "wf_prog wt G \<Longrightarrow> approx_val G hp v (Ok T) \<longrightarrow> G\<turnstile> T\<preceq>T' \<longrightarrow> approx_val G hp v (Ok T')"
+ "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T' --> approx_val G hp v (Ok T')"
by (cases T) (auto intro: conf_widen simp add: approx_val_def)
lemma approx_val_imp_approx_val_sup_heap [rule_format]:
- "approx_val G hp v at \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_val G hp' v at"
+ "approx_val G hp v at --> hp \<le>| hp' --> approx_val G hp' v at"
apply (simp add: approx_val_def split: err.split)
apply (blast intro: conf_hext)
.
lemma approx_val_imp_approx_val_heap_update:
- "\<lbrakk>hp a = Some obj'; G,hp\<turnstile> v\<Colon>\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk>
- \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v\<Colon>\<preceq>T"
+ "[|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"
by (cases v, auto simp add: obj_ty_def conf_def)
lemma approx_val_imp_approx_val_sup [rule_format]:
- "wf_prog wt G \<Longrightarrow> (approx_val G h v us) \<longrightarrow> (G \<turnstile> us <=o us') \<longrightarrow> (approx_val G h v us')"
+ "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') --> (approx_val G h v us')"
apply (simp add: sup_PTS_eq approx_val_def split: err.split)
apply (blast intro: conf_widen)
.
lemma approx_loc_imp_approx_val_sup:
- "\<lbrakk>wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at\<rbrakk>
- \<Longrightarrow> approx_val G hp v at"
+ "[|wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at|]
+ ==> approx_val G hp v at"
apply (unfold approx_loc_def)
apply (unfold list_all2_def)
apply (auto intro: approx_val_imp_approx_val_sup simp add: split_def all_set_conv_all_nth)
@@ -129,8 +129,8 @@
by (simp add: approx_loc_def)
lemma assConv_approx_stk_imp_approx_loc [rule_format]:
- "wf_prog wt G \<Longrightarrow> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G)
- \<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp s tys_n \<longrightarrow>
+ "wf_prog wt G ==> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G)
+ --> length tys_n = length ts --> approx_stk G hp s tys_n -->
approx_loc G hp s (map Ok ts)"
apply (unfold approx_stk_def approx_loc_def list_all2_def)
apply (clarsimp simp add: all_set_conv_all_nth)
@@ -140,7 +140,7 @@
lemma approx_loc_imp_approx_loc_sup_heap [rule_format]:
- "\<forall>lvars. approx_loc G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_loc G hp' lvars lt"
+ "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' --> approx_loc G hp' lvars lt"
apply (unfold approx_loc_def list_all2_def)
apply (cases lt)
apply simp
@@ -150,7 +150,7 @@
.
lemma approx_loc_imp_approx_loc_sup [rule_format]:
- "wf_prog wt G \<Longrightarrow> approx_loc G hp lvars lt \<longrightarrow> G \<turnstile> lt <=l lt' \<longrightarrow> approx_loc G hp lvars lt'"
+ "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' --> approx_loc G hp lvars lt'"
apply (unfold sup_loc_def approx_loc_def list_all2_def)
apply (auto simp add: all_set_conv_all_nth)
apply (auto elim: approx_val_imp_approx_val_sup)
@@ -158,8 +158,8 @@
lemma approx_loc_imp_approx_loc_subst [rule_format]:
- "\<forall>loc idx x X. (approx_loc G hp loc LT) \<longrightarrow> (approx_val G hp x X)
- \<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
+ "\<forall>loc idx x X. (approx_loc G hp loc LT) --> (approx_val G hp x X)
+ --> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
apply (unfold approx_loc_def list_all2_def)
apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
.
@@ -168,7 +168,7 @@
lemmas [cong] = conj_cong
lemma approx_loc_append [rule_format]:
- "\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow>
+ "\<forall>L1 l2 L2. length l1=length L1 -->
approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
apply (unfold approx_loc_def list_all2_def)
apply simp
@@ -192,12 +192,12 @@
lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
- "\<forall>lvars. approx_stk G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_stk G hp' lvars lt"
+ "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' --> approx_stk G hp' lvars lt"
by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
lemma approx_stk_imp_approx_stk_sup [rule_format]:
- "wf_prog wt G \<Longrightarrow> approx_stk G hp lvars st \<longrightarrow> (G \<turnstile> map Ok st <=l (map Ok st'))
- \<longrightarrow> approx_stk G hp lvars st'"
+ "wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map Ok st <=l (map Ok st'))
+ --> approx_stk G hp lvars st'"
by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
lemma approx_stk_Nil [iff]:
@@ -215,7 +215,7 @@
by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
lemma approx_stk_append_lemma:
- "approx_stk G hp stk (S@ST') \<Longrightarrow>
+ "approx_stk G hp stk (S@ST') ==>
(\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length ST' \<and>
approx_stk G hp s S \<and> approx_stk G hp stk' ST')"
by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
@@ -224,7 +224,7 @@
(** oconf **)
lemma correct_init_obj:
- "\<lbrakk>is_class G C; wf_prog wt G\<rbrakk> \<Longrightarrow>
+ "[|is_class G C; wf_prog wt G|] ==>
G,h \<turnstile> (C, map_of (map (\<lambda>(f,fT).(f,default_val fT)) (fields(G,C)))) \<surd>"
apply (unfold oconf_def lconf_def)
apply (simp add: map_of_map)
@@ -233,13 +233,13 @@
lemma oconf_imp_oconf_field_update [rule_format]:
- "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v\<Colon>\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
- \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
+ "[|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>"
by (simp add: oconf_def lconf_def)
lemma oconf_imp_oconf_heap_newref [rule_format]:
-"hp x = None \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G,hp\<turnstile>obj'\<surd> \<longrightarrow> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>"
+"hp x = None --> G,hp\<turnstile>obj\<surd> --> G,hp\<turnstile>obj'\<surd> --> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>"
apply (unfold oconf_def lconf_def)
apply simp
apply (fast intro: conf_hext sup_heap_newref)
@@ -247,8 +247,8 @@
lemma oconf_imp_oconf_heap_update [rule_format]:
- "hp a = Some obj' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd>
- \<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
+ "hp a = Some obj' --> obj_ty obj' = obj_ty obj'' --> G,hp\<turnstile>obj\<surd>
+ --> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
apply (unfold oconf_def lconf_def)
apply simp
apply (force intro: approx_val_imp_approx_val_heap_update)
@@ -259,14 +259,14 @@
lemma hconf_imp_hconf_newref [rule_format]:
- "hp x = None \<longrightarrow> G\<turnstile>h hp\<surd> \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
+ "hp x = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
apply (simp add: hconf_def)
apply (fast intro: oconf_imp_oconf_heap_newref)
.
lemma hconf_imp_hconf_field_update [rule_format]:
"map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and>
- G,hp\<turnstile>v\<Colon>\<preceq>T \<and> G\<turnstile>h hp\<surd> \<longrightarrow> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>"
+ G,hp\<turnstile>v::\<preceq>T \<and> G\<turnstile>h hp\<surd> --> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>"
apply (simp add: hconf_def)
apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update
simp add: obj_ty_def)
@@ -277,10 +277,10 @@
lemmas [simp del] = fun_upd_apply
lemma correct_frames_imp_correct_frames_field_update [rule_format]:
- "\<forall>rT C sig. correct_frames G hp phi rT sig frs \<longrightarrow>
- hp a = Some (C,od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow>
- G,hp\<turnstile>v\<Colon>\<preceq>fd
- \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs";
+ "\<forall>rT C sig. correct_frames G hp phi rT sig frs -->
+ hp a = Some (C,od) --> map_of (fields (G, C)) fl = Some fd -->
+ G,hp\<turnstile>v::\<preceq>fd
+ --> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs";
apply (induct frs)
apply simp
apply (clarsimp simp add: correct_frame_def) (*takes long*)
@@ -300,8 +300,8 @@
.
lemma correct_frames_imp_correct_frames_newref [rule_format]:
- "\<forall>rT C sig. hp x = None \<longrightarrow> correct_frames G hp phi rT sig frs \<and> oconf G hp obj
- \<longrightarrow> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
+ "\<forall>rT C sig. hp x = None --> correct_frames G hp phi rT sig frs \<and> oconf G hp obj
+ --> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
apply (induct frs)
apply simp
apply (clarsimp simp add: correct_frame_def)
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Thu Sep 21 10:42:49 2000 +0200
@@ -9,30 +9,30 @@
theory LBVComplete = BVSpec + LBVSpec + StepMono:
constdefs
- contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
- "contains_targets ins cert phi pc \<equiv>
+ contains_targets :: "[instr list, certificate, method_type, p_count] => bool"
+ "contains_targets ins cert phi pc ==
\<forall>pc' \<in> set (succs (ins!pc) pc).
- pc' \<noteq> pc+1 \<and> pc' < length ins \<longrightarrow> cert!pc' = phi!pc'"
+ pc' \<noteq> pc+1 \<and> pc' < length ins --> cert!pc' = phi!pc'"
- fits :: "[instr list, certificate, method_type] \<Rightarrow> bool"
- "fits ins cert phi \<equiv> \<forall>pc. pc < length ins \<longrightarrow>
+ fits :: "[instr list, certificate, method_type] => bool"
+ "fits ins cert phi == \<forall>pc. pc < length ins -->
contains_targets ins cert phi pc \<and>
(cert!pc = None \<or> cert!pc = phi!pc)"
- is_target :: "[instr list, p_count] \<Rightarrow> bool"
- "is_target ins pc \<equiv>
+ is_target :: "[instr list, p_count] => 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] \<Rightarrow> certificate"
- "make_cert ins phi \<equiv>
+ make_cert :: "[instr list, method_type] => 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] \<Rightarrow> prog_certificate"
- "make_Cert G Phi \<equiv> \<lambda> C sig.
- let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
- (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
+ make_Cert :: "[jvm_prog, prog_type] => prog_certificate"
+ "make_Cert G Phi == \<lambda> C sig.
+ let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
+ (sig,rT,maxl,b) = SOME (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
in make_cert b (Phi C sig)"
@@ -197,14 +197,14 @@
have app: "app (ins!pc) G rT (phi!pc)" by (simp add: wt_instr_def)
from wt pc
- have pc': "\<And>pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
+ have pc': "!!pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
by (simp add: wt_instr_def)
let ?s' = "step (ins!pc) G (phi!pc)"
from wt fits pc
- have cert: "!!pc'. \<lbrakk>pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1\<rbrakk>
- \<Longrightarrow> G \<turnstile> ?s' <=' cert!pc'"
+ have cert: "!!pc'. [|pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1|]
+ ==> G \<turnstile> ?s' <=' cert!pc'"
by (auto dest: fitsD simp add: wt_instr_def)
from app pc cert pc'
@@ -324,14 +324,14 @@
*}
theorem wt_imp_wtl_inst_list:
-"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow>
- wt_instr (all_ins ! pc') G rT phi (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>
+"\<forall> pc. (\<forall>pc'. pc' < length all_ins -->
+ wt_instr (all_ins ! pc') G rT phi (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)) -->
wtl_inst_list ins G rT cert (length all_ins) pc s \<noteq> Err)"
-(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins"
+(is "\<forall>pc. ?wt --> ?fits --> ?l pc ins --> ?len pc --> ?wtl pc ins"
is "\<forall>pc. ?C pc ins" is "?P ins")
proof (induct "?P" "ins")
case Nil
@@ -343,7 +343,7 @@
show "?P (i#ins')"
proof (intro allI impI, elim exE conjE)
fix pc s l
- assume wt : "\<forall>pc'. pc' < length all_ins \<longrightarrow>
+ assume wt : "\<forall>pc'. pc' < length all_ins -->
wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'"
assume fits: "fits all_ins cert phi"
assume l : "pc < length all_ins"
@@ -362,7 +362,7 @@
from Cons
have "?C (Suc pc) ins'" by blast
with wt fits pc
- have IH: "?len (Suc pc) \<longrightarrow> ?wtl (Suc pc) ins'" by auto
+ have IH: "?len (Suc pc) --> ?wtl (Suc pc) ins'" by auto
show "wtl_inst_list (i#ins') G rT cert (length all_ins) pc s \<noteq> Err"
proof (cases "?len (Suc pc)")
@@ -422,20 +422,10 @@
by (rule fits_imp_wtl_method_complete)
qed
-lemma unique_set:
-"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow>
- a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
- by (induct "l") auto
-
-lemma unique_epsilon:
- "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow>
- (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
- by (auto simp add: unique_set)
-
theorem wtl_complete:
"wt_jvm_prog G Phi ==> wtl_jvm_prog G (make_Cert G Phi)"
-proof (simp only: wt_jvm_prog_def)
+proof (unfold wt_jvm_prog_def)
assume wfprog:
"wf_prog (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G"
@@ -449,12 +439,12 @@
(\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT \<and>
(\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \<and>
unique ms \<and>
- (case sc of None \<Rightarrow> C = Object
- | Some D \<Rightarrow>
+ (case sc of None => C = Object
+ | Some D =>
is_class G D \<and>
(D, C) \<notin> (subcls1 G)^* \<and>
(\<forall>(sig,rT,b)\<in>set ms.
- \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \<longrightarrow> G\<turnstile>rT\<preceq>rT'))"
+ \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') --> G\<turnstile>rT\<preceq>rT'))"
"(a, aa, ab, b) \<in> set G"
assume uG : "unique G"
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Sep 21 10:42:49 2000 +0200
@@ -11,31 +11,31 @@
lemmas [simp del] = split_paired_Ex split_paired_All
constdefs
-fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> bool"
-"fits phi is G rT s0 cert \<equiv>
- (\<forall>pc s1. pc < length is \<longrightarrow>
- (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 \<longrightarrow>
- (case cert!pc of None \<Rightarrow> phi!pc = s1
- | Some t \<Rightarrow> phi!pc = Some t)))"
+fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] => bool"
+"fits phi is G rT s0 cert ==
+ (\<forall>pc s1. pc < length is -->
+ (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 -->
+ (case cert!pc of None => phi!pc = s1
+ | Some t => phi!pc = Some t)))"
constdefs
-make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> method_type"
-"make_phi is G rT s0 cert \<equiv>
+make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] => method_type"
+"make_phi is G rT s0 cert ==
map (\<lambda>pc. case cert!pc of
- None \<Rightarrow> val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)
- | Some t \<Rightarrow> Some t) [0..length is(]"
+ None => val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)
+ | Some t => Some t) [0..length is(]"
lemma fitsD_None:
- "\<lbrakk>fits phi is G rT s0 cert; pc < length is;
+ "[|fits phi is G rT s0 cert; pc < length is;
wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1;
- cert ! pc = None\<rbrakk> \<Longrightarrow> phi!pc = s1"
+ cert ! pc = None|] ==> phi!pc = s1"
by (auto simp add: fits_def)
lemma fitsD_Some:
- "\<lbrakk>fits phi is G rT s0 cert; pc < length is;
+ "[|fits phi is G rT s0 cert; pc < length is;
wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1;
- cert ! pc = Some t\<rbrakk> \<Longrightarrow> phi!pc = Some t"
+ cert ! pc = Some t|] ==> phi!pc = Some t"
by (auto simp add: fits_def)
lemma make_phi_Some:
@@ -62,7 +62,7 @@
lemma fits_lemma1:
"[| wtl_inst_list is G rT cert (length is) 0 s = Ok s'; fits phi is G rT s cert |]
- ==> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t"
+ ==> \<forall>pc t. pc < length is --> cert!pc = Some t --> phi!pc = Some t"
proof (intro strip)
fix pc t
assume "wtl_inst_list is G rT cert (length is) 0 s = Ok s'"
@@ -114,11 +114,11 @@
"wtl_cert l G rT s'' cert (length is) (Suc pc) = Ok x"
by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
- hence c1: "\<And>t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
+ hence c1: "!!t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
by (simp add: wtl_cert_def split: if_splits)
moreover
from fits pc wts
- have c2: "\<And>t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
+ have c2: "!!t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
by - (drule fitsD_Some, auto)
moreover
from fits pc wts
@@ -150,7 +150,7 @@
from fits wtl pc
have cert_Some:
- "\<And>t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
+ "!!t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
by (auto dest: fits_lemma1)
from fits wtl pc
@@ -236,7 +236,7 @@
by (rule fitsD_None)
moreover
from fits pc wt0
- have "\<And>t. cert!0 = Some t ==> phi!0 = cert!0"
+ have "!!t. cert!0 = Some t ==> phi!0 = cert!0"
by - (drule fitsD_Some, auto)
moreover
from pc
@@ -247,7 +247,7 @@
"wtl_cert x G rT s cert (length is) 0 = Ok s'"
by simp (elim, rule that, simp)
hence
- "\<And>t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
+ "!!t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
by (simp add: wtl_cert_def split: if_splits)
ultimately
@@ -268,7 +268,7 @@
with wtl
have allpc:
- "\<forall>pc. pc < length ins \<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc"
+ "\<forall>pc. pc < length ins --> wt_instr (ins ! pc) G rT phi (length ins) pc"
by (blast intro: wtl_fits_wt)
from pc wtl fits
@@ -279,15 +279,6 @@
show ?thesis by (auto simp add: wt_method_def)
qed
-lemma unique_set:
- "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow>
- a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
- by (induct "l") auto
-
-lemma unique_epsilon:
- "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow>
- (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
- by (auto simp add: unique_set)
theorem wtl_correct:
"wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
@@ -304,9 +295,9 @@
(is "\<exists>Phi. ?Q Phi")
proof (intro exI)
let "?Phi" = "\<lambda> C sig.
- let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
- (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
- in \<epsilon> phi. wt_method G C (snd sig) rT maxl b phi"
+ let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
+ (sig,rT,maxl,b) = SOME (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
+ in SOME phi. wt_method G C (snd sig) rT maxl b phi"
from wtl_prog
show "?Q ?Phi"
proof (unfold wf_cdecl_def, intro)
@@ -328,8 +319,8 @@
wt_method G a (snd sig) rT maxl b
((\<lambda>(C,x,y,mdecls).
(\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
- (\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig))
- (\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
+ (SOME (sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig))
+ (SOME (Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
by - (drule bspec, assumption,
clarsimp dest!: wtl_method_correct,
clarsimp intro!: someI simp add: unique_epsilon)
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Thu Sep 21 10:42:49 2000 +0200
@@ -11,44 +11,36 @@
types
certificate = "state_type option list"
- class_certificate = "sig \<Rightarrow> certificate"
- prog_certificate = "cname \<Rightarrow> class_certificate"
+ class_certificate = "sig => certificate"
+ prog_certificate = "cname => class_certificate"
constdefs
check_cert :: "[instr, jvm_prog, state_type option, certificate, p_count, p_count]
- \<Rightarrow> bool"
- "check_cert i G s cert pc max_pc \<equiv> \<forall>pc' \<in> set (succs i pc). pc' < max_pc \<and>
- (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> step i G s <=' cert!pc')"
+ => bool"
+ "check_cert i G s cert pc max_pc == \<forall>pc' \<in> set (succs i pc). pc' < max_pc \<and>
+ (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')"
wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count]
- \<Rightarrow> state_type option err"
- "wtl_inst i G rT s cert max_pc pc \<equiv>
+ => state_type option err"
+ "wtl_inst i G rT s cert max_pc pc ==
if app i G rT s \<and> check_cert i G s cert pc max_pc then
if pc+1 mem (succs i pc) then Ok (step i G s) else Ok (cert!(pc+1))
else Err";
-lemma wtl_inst_Ok:
-"(wtl_inst i G rT s cert max_pc pc = Ok s') =
- (app i G rT s \<and> (\<forall>pc' \<in> set (succs i pc).
- pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> step i G s <=' cert!pc')) \<and>
- (if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))"
- by (auto simp add: wtl_inst_def check_cert_def set_mem_eq);
-
-
constdefs
wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count]
- \<Rightarrow> state_type option err"
- "wtl_cert i G rT s cert max_pc pc \<equiv>
+ => state_type option err"
+ "wtl_cert i G rT s cert max_pc pc ==
case cert!pc of
- None \<Rightarrow> wtl_inst i G rT s cert max_pc pc
- | Some s' \<Rightarrow> if G \<turnstile> s <=' (Some s') then
+ None => wtl_inst i G rT s cert max_pc pc
+ | Some s' => if G \<turnstile> s <=' (Some s') then
wtl_inst i G rT (Some s') cert max_pc pc
else Err"
consts
wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,p_count,p_count,
- state_type option] \<Rightarrow> state_type option err"
+ state_type option] => state_type option err"
primrec
"wtl_inst_list [] G rT cert max_pc pc s = Ok s"
"wtl_inst_list (i#is) G rT cert max_pc pc s =
@@ -57,19 +49,26 @@
constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \<Rightarrow> bool"
- "wtl_method G C pTs rT mxl ins cert \<equiv>
+ wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] => bool"
+ "wtl_method G C pTs rT mxl ins cert ==
let max_pc = length ins
in
0 < max_pc \<and>
wtl_inst_list ins G rT cert max_pc 0
(Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err))) \<noteq> Err"
- wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool"
- "wtl_jvm_prog G cert \<equiv>
+ wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool"
+ "wtl_jvm_prog G cert ==
wf_prog (\<lambda>G C (sig,rT,maxl,b). wtl_method G C (snd sig) rT maxl b (cert C sig)) G"
-text {* \medskip *}
+
+
+lemma wtl_inst_Ok:
+"(wtl_inst i G rT s cert max_pc pc = Ok s') =
+ (app i G rT s \<and> (\<forall>pc' \<in> set (succs i pc).
+ pc' < max_pc \<and> (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')) \<and>
+ (if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))"
+ by (auto simp add: wtl_inst_def check_cert_def set_mem_eq);
lemma strict_Some [simp]:
"(strict f x = Ok y) = (\<exists> z. x = Ok z \<and> f z = Ok y)"
@@ -127,7 +126,7 @@
qed
lemma take_Suc:
- "\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
+ "\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
proof (induct l)
show "?P []" by simp
@@ -191,4 +190,14 @@
by (auto simp add: wtl_append min_def)
qed
+lemma unique_set:
+"(a,b,c,d)\<in>set l --> unique l --> (a',b',c',d') \<in> set l -->
+ a = a' --> b=b' \<and> c=c' \<and> d=d'"
+ by (induct "l") auto
+
+lemma unique_epsilon:
+ "(a,b,c,d)\<in>set l --> unique l -->
+ (SOME (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
+ by (auto simp add: unique_set)
+
end
--- a/src/HOL/MicroJava/BV/Step.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/Step.thy Thu Sep 21 10:42:49 2000 +0200
@@ -12,7 +12,7 @@
text "Effect of instruction on the state type:"
consts
-step' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
+step' :: "instr \<times> jvm_prog \<times> state_type => state_type"
recdef step' "{}"
"step' (Load idx, G, (ST, LT)) = (val (LT ! idx) # ST, LT)"
@@ -40,13 +40,13 @@
(* "step' (i,G,s) = None" *)
constdefs
- step :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"
- "step i G \<equiv> opt_map (\<lambda>s. step' (i,G,s))"
+ step :: "instr => jvm_prog => state_type option => state_type option"
+ "step i G == option_map (\<lambda>s. step' (i,G,s))"
text "Conditions under which step is applicable:"
consts
-app' :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool"
+app' :: "instr \<times> jvm_prog \<times> ty \<times> state_type => bool"
recdef app' "{}"
"app' (Load idx, G, rT, s) = (idx < length (snd s) \<and>
@@ -88,13 +88,13 @@
constdefs
- app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> ty \<Rightarrow> state_type option \<Rightarrow> bool"
- "app i G rT s \<equiv> case s of None \<Rightarrow> True | Some t \<Rightarrow> app' (i,G,rT,t)"
+ app :: "instr => jvm_prog => ty => state_type option => bool"
+ "app i G rT s == case s of None => True | Some t => app' (i,G,rT,t)"
text {* program counter of successor instructions: *}
consts
-succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list"
+succs :: "instr => p_count => p_count list"
primrec
"succs (Load idx) pc = [pc+1]"
@@ -117,13 +117,13 @@
"succs (Invoke C mn fpTs) pc = [pc+1]"
-lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
+lemma 1: "2 < length a ==> (\<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) \<Longrightarrow> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
+lemma 2: "\<not>(2 < length a) ==> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
proof -;
assume "\<not>(2 < length a)"
hence "length a < (Suc 2)" by simp
@@ -136,7 +136,7 @@
hence "\<exists> l. x = [l]" by - (cases x, auto)
} note 0 = this
- have "length a = 2 \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
+ have "length a = 2 ==> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
with * show ?thesis by (auto dest: 0)
qed
@@ -149,7 +149,6 @@
by (simp add: app_def)
-
lemma appLoad[simp]:
"(app (Load idx) G rT (Some s)) = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err)"
by (simp add: app_def)
@@ -264,7 +263,7 @@
method (G,C) (mn,fpTs) = Some (mD', rT', b'))" (is "?app s = ?P s")
proof (cases (open) s)
case Pair
- have "?app (a,b) \<Longrightarrow> ?P (a,b)"
+ have "?app (a,b) ==> ?P (a,b)"
proof -
assume app: "?app (a,b)"
hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and>
@@ -286,7 +285,7 @@
with app
show ?thesis by (auto simp add: app_def) blast
qed
- with Pair have "?app s \<Longrightarrow> ?P s" by simp
+ with Pair have "?app s ==> ?P s" by simp
thus ?thesis by (auto simp add: app_def)
qed
--- a/src/HOL/MicroJava/BV/StepMono.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy Thu Sep 21 10:42:49 2000 +0200
@@ -14,7 +14,7 @@
lemma sup_loc_some [rule_format]:
-"\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Ok t \<longrightarrow>
+"\<forall> y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = Ok t -->
(\<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 \<longrightarrow>
+"\<forall>b. length a = length b -->
(\<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 \<longrightarrow> ?Q a b" is "?P a")
+ (is "\<forall>b. length a = length b --> ?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 \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
+"\<forall>n. n \<le> length x --> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
proof (induct (open) ?P x)
show "?P []" by simp
@@ -94,7 +94,7 @@
lemma rev_append_cons:
-"\<lbrakk>n < length x\<rbrakk> \<Longrightarrow> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
+"[|n < length x|] ==> \<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
@@ -118,7 +118,7 @@
lemma app_mono:
-"\<lbrakk>G \<turnstile> s <=' s'; app i G rT s'\<rbrakk> \<Longrightarrow> app i G rT s";
+"[|G \<turnstile> s <=' s'; app i G rT s'|] ==> app i G rT s";
proof -
{ fix s1 s2
--- a/src/HOL/MicroJava/J/Conform.ML Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Conform.ML Thu Sep 21 10:42:49 2000 +0200
@@ -6,25 +6,25 @@
section "hext";
-val hextI = prove_goalw thy [hext_def] "\\<And>h. \
-\ \\<forall>a C fs . h a = Some (C,fs) \\<longrightarrow> \
-\ (\\<exists>fs'. h' a = Some (C,fs')) \\<Longrightarrow> h\\<le>|h'" (K [Auto_tac ]);
+val hextI = prove_goalw thy [hext_def] "!!h. \
+\ \\<forall>a C fs . h a = Some (C,fs) --> \
+\ (\\<exists>fs'. h' a = Some (C,fs')) ==> h\\<le>|h'" (K [Auto_tac ]);
val hext_objD = prove_goalw thy [hext_def]
-"\\<And>h. \\<lbrakk>h\\<le>|h'; h a = Some (C,fs) \\<rbrakk> \\<Longrightarrow> \\<exists>fs'. h' a = Some (C,fs')"
+"!!h. [|h\\<le>|h'; h a = Some (C,fs) |] ==> \\<exists>fs'. h' a = Some (C,fs')"
(K [Force_tac 1]);
val hext_refl = prove_goal thy "h\\<le>|h" (K [
rtac hextI 1,
Fast_tac 1]);
-val hext_new = prove_goal thy "\\<And>h. h a = None \\<Longrightarrow> h\\<le>|h(a\\<mapsto>x)" (K [
+val hext_new = prove_goal thy "!!h. h a = None ==> h\\<le>|h(a\\<mapsto>x)" (K [
rtac hextI 1,
safe_tac HOL_cs,
ALLGOALS (case_tac "aa = a"),
Auto_tac]);
-val hext_trans = prove_goal thy "\\<And>h. \\<lbrakk>h\\<le>|h'; h'\\<le>|h''\\<rbrakk> \\<Longrightarrow> h\\<le>|h''" (K [
+val hext_trans = prove_goal thy "!!h. [|h\\<le>|h'; h'\\<le>|h''|] ==> h\\<le>|h''" (K [
rtac hextI 1,
safe_tac HOL_cs,
fast_tac (HOL_cs addDs [hext_objD]) 1]);
@@ -32,7 +32,7 @@
Addsimps [hext_refl, hext_new];
val hext_upd_obj = prove_goal thy
-"\\<And>h. h a = Some (C,fs) \\<Longrightarrow> h\\<le>|h(a\\<mapsto>(C,fs'))" (K [
+"!!h. h a = Some (C,fs) ==> h\\<le>|h(a\\<mapsto>(C,fs'))" (K [
rtac hextI 1,
safe_tac HOL_cs,
ALLGOALS (case_tac "aa = a"),
@@ -42,37 +42,37 @@
section "conf";
val conf_Null = prove_goalw thy [conf_def]
-"G,h\\<turnstile>Null\\<Colon>\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T" (K [Simp_tac 1]);
+"G,h\\<turnstile>Null::\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T" (K [Simp_tac 1]);
Addsimps [conf_Null];
val conf_litval = prove_goalw thy [conf_def]
-"typeof (\\<lambda>v. None) v = Some T \\<longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T" (K [
+"typeof (\\<lambda>v. None) v = Some T --> G,h\\<turnstile>v::\\<preceq>T" (K [
rtac val_.induct 1,
Auto_tac]) RS mp;
-Goalw [conf_def] "G,s\\<turnstile>Unit\\<Colon>\\<preceq>PrimT Void";
+Goalw [conf_def] "G,s\\<turnstile>Unit::\\<preceq>PrimT Void";
by( Simp_tac 1);
qed "conf_VoidI";
-Goalw [conf_def] "G,s\\<turnstile>Bool b\\<Colon>\\<preceq>PrimT Boolean";
+Goalw [conf_def] "G,s\\<turnstile>Bool b::\\<preceq>PrimT Boolean";
by( Simp_tac 1);
qed "conf_BooleanI";
-Goalw [conf_def] "G,s\\<turnstile>Intg i\\<Colon>\\<preceq>PrimT Integer";
+Goalw [conf_def] "G,s\\<turnstile>Intg i::\\<preceq>PrimT Integer";
by( Simp_tac 1);
qed "conf_IntegerI";
Addsimps [conf_VoidI, conf_BooleanI, conf_IntegerI];
val conf_AddrI = prove_goalw thy [conf_def]
-"\\<And>G. \\<lbrakk>h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq>T"
+"!!G. [|h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T|] ==> G,h\\<turnstile>Addr a::\\<preceq>T"
(K [Asm_full_simp_tac 1]);
val conf_obj_AddrI = prove_goalw thy [conf_def]
- "\\<And>G. \\<lbrakk>h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq> Class D"
+ "!!G. [|h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D|] ==> G,h\\<turnstile>Addr a::\\<preceq> Class D"
(K [Asm_full_simp_tac 1]);
-Goalw [conf_def] "is_type G T \\<longrightarrow> G,h\\<turnstile>default_val T\\<Colon>\\<preceq>T";
+Goalw [conf_def] "is_type G T --> G,h\\<turnstile>default_val T::\\<preceq>T";
by (res_inst_tac [("y","T")] ty.exhaust 1);
by (etac ssubst 1);
by (res_inst_tac [("y","prim_ty")] prim_ty.exhaust 1);
@@ -80,7 +80,7 @@
qed_spec_mp "defval_conf";
val conf_upd_obj = prove_goalw thy [conf_def]
-"h a = Some (C,fs) \\<longrightarrow> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x\\<Colon>\\<preceq>T) = (G,h\\<turnstile>x\\<Colon>\\<preceq>T)" (fn _ => [
+"h a = Some (C,fs) --> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x::\\<preceq>T) = (G,h\\<turnstile>x::\\<preceq>T)" (fn _ => [
rtac impI 1,
rtac val_.induct 1,
ALLGOALS Simp_tac,
@@ -88,14 +88,14 @@
ALLGOALS Asm_simp_tac]) RS mp;
val conf_widen = prove_goalw thy [conf_def]
-"\\<And>G. wf_prog wf_mb G \\<Longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T \\<longrightarrow> G\\<turnstile>T\\<preceq>T' \\<longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T'" (K [
+"!!G. wf_prog wf_mb G ==> G,h\\<turnstile>x::\\<preceq>T --> G\\<turnstile>T\\<preceq>T' --> G,h\\<turnstile>x::\\<preceq>T'" (K [
rtac val_.induct 1,
ALLGOALS Simp_tac,
ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp;
bind_thm ("conf_widen", conf_widen);
val conf_hext' = prove_goalw thy [conf_def]
- "\\<And>h. h\\<le>|h' \\<Longrightarrow> (\\<forall>v T. G,h\\<turnstile>v\\<Colon>\\<preceq>T \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>T)" (K [
+ "!!h. h\\<le>|h' ==> (\\<forall>v T. G,h\\<turnstile>v::\\<preceq>T --> G,h'\\<turnstile>v::\\<preceq>T)" (K [
REPEAT (rtac allI 1),
rtac val_.induct 1,
ALLGOALS Simp_tac,
@@ -107,36 +107,36 @@
bind_thm ("conf_hext", conf_hext);
val new_locD = prove_goalw thy [conf_def]
- "\\<lbrakk>h a = None; G,h\\<turnstile>Addr t\\<Colon>\\<preceq>T\\<rbrakk> \\<Longrightarrow> t\\<noteq>a" (fn prems => [
+ "[|h a = None; G,h\\<turnstile>Addr t::\\<preceq>T|] ==> t\\<noteq>a" (fn prems => [
cut_facts_tac prems 1,
Full_simp_tac 1,
safe_tac HOL_cs,
Asm_full_simp_tac 1]);
Goalw [conf_def]
- "G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT T \\<longrightarrow> a' = Null | \
+ "G,h\\<turnstile>a'::\\<preceq>RefT T --> a' = Null | \
\ (\\<exists>a obj T'. a' = Addr a \\<and> h a = Some obj \\<and> obj_ty obj = T' \\<and> G\\<turnstile>T'\\<preceq>RefT T)";
by(induct_tac "a'" 1);
by(Auto_tac);
qed_spec_mp "conf_RefTD";
-val conf_NullTD = prove_goal thy "\\<And>G. G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT NullT \\<Longrightarrow> a' = Null" (K [
+val conf_NullTD = prove_goal thy "!!G. G,h\\<turnstile>a'::\\<preceq>RefT NullT ==> a' = Null" (K [
dtac conf_RefTD 1,
Step_tac 1,
Auto_tac]);
-val non_npD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t\\<rbrakk> \\<Longrightarrow> \
+val non_npD = prove_goal thy "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq>RefT t|] ==> \
\ \\<exists>a C fs. a' = Addr a \\<and> h a = Some (C,fs) \\<and> G\\<turnstile>Class C\\<preceq>RefT t" (K [
dtac conf_RefTD 1,
Step_tac 1,
Auto_tac]);
-val non_np_objD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq> Class C; C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \
+val non_np_objD = prove_goal thy "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq> Class C; C \\<noteq> Object|] ==> \
\ (\\<exists>a C' fs. a' = Addr a \\<and> h a = Some (C',fs) \\<and> G\\<turnstile>C'\\<preceq>C C)"
(K[fast_tac (claset() addDs [non_npD]) 1]);
-Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wf_mb G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
-\ (\\<forall>C. t = ClassT C \\<longrightarrow> C \\<noteq> Object) \\<longrightarrow> \
+Goal "a' \\<noteq> Null --> wf_prog wf_mb G --> G,h\\<turnstile>a'::\\<preceq>RefT t -->\
+\ (\\<forall>C. t = ClassT C --> C \\<noteq> Object) --> \
\ (\\<exists>a C fs. a' = Addr a \\<and> h a = Some (C,fs) \\<and> G\\<turnstile>Class C\\<preceq>RefT t)";
by(rtac impI 1);
by(rtac impI 1);
@@ -150,7 +150,7 @@
by(Fast_tac 1);
qed_spec_mp "non_np_objD'";
-Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts \\<longrightarrow> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' \\<longrightarrow> list_all2 (conf G h) vs Ts'";
+Goal "wf_prog wf_mb G ==> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts --> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' --> list_all2 (conf G h) vs Ts'";
by(induct_tac "vs" 1);
by(ALLGOALS Clarsimp_tac);
by(forward_tac [list_all2_lengthD RS sym] 1);
@@ -166,30 +166,30 @@
section "lconf";
val lconfD = prove_goalw thy [lconf_def]
- "\\<And>X. \\<lbrakk> G,h\\<turnstile>vs[\\<Colon>\\<preceq>]Ts; Ts n = Some T \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>(the (vs n))\\<Colon>\\<preceq>T"
+ "!!X. [| G,h\\<turnstile>vs[::\\<preceq>]Ts; Ts n = Some T |] ==> G,h\\<turnstile>(the (vs n))::\\<preceq>T"
(K [Force_tac 1]);
val lconf_hext = prove_goalw thy [lconf_def]
- "\\<And>X. \\<lbrakk> G,h\\<turnstile>l[\\<Colon>\\<preceq>]L; h\\<le>|h' \\<rbrakk> \\<Longrightarrow> G,h'\\<turnstile>l[\\<Colon>\\<preceq>]L" (K [
+ "!!X. [| G,h\\<turnstile>l[::\\<preceq>]L; h\\<le>|h' |] ==> G,h'\\<turnstile>l[::\\<preceq>]L" (K [
fast_tac (claset() addEs [conf_hext]) 1]);
AddEs [lconf_hext];
-Goalw [lconf_def] "\\<And>X. \\<lbrakk> G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT; \
-\ G,h\\<turnstile>v\\<Colon>\\<preceq>T; lT va = Some T \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>l(va\\<mapsto>v)[\\<Colon>\\<preceq>]lT";
+Goalw [lconf_def] "!!X. [| G,h\\<turnstile>l[::\\<preceq>]lT; \
+\ G,h\\<turnstile>v::\\<preceq>T; lT va = Some T |] ==> G,h\\<turnstile>l(va\\<mapsto>v)[::\\<preceq>]lT";
by( Clarify_tac 1);
by( case_tac "n = va" 1);
by Auto_tac;
qed "lconf_upd";
-Goal "\\<forall>x. P x \\<longrightarrow> R (dv x) x \\<Longrightarrow> (\\<forall>x. map_of fs f = Some x \\<longrightarrow> P x) \\<longrightarrow> \
-\ (\\<forall>T. map_of fs f = Some T \\<longrightarrow> \
+Goal "\\<forall>x. P x --> R (dv x) x ==> (\\<forall>x. map_of fs f = Some x --> P x) --> \
+\ (\\<forall>T. map_of fs f = Some T --> \
\ (\\<exists>v. map_of (map (\\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \\<and> R v T))";
by( induct_tac "fs" 1);
by Auto_tac;
qed_spec_mp "lconf_init_vars_lemma";
Goalw [lconf_def, init_vars_def]
-"\\<forall>n. \\<forall>T. map_of fs n = Some T \\<longrightarrow> is_type G T \\<Longrightarrow> G,h\\<turnstile>init_vars fs[\\<Colon>\\<preceq>]map_of fs";
+"\\<forall>n. \\<forall>T. map_of fs n = Some T --> is_type G T ==> G,h\\<turnstile>init_vars fs[::\\<preceq>]map_of fs";
by Auto_tac;
by( rtac lconf_init_vars_lemma 1);
by( atac 3);
@@ -200,10 +200,10 @@
AddSIs [lconf_init_vars];
val lconf_ext = prove_goalw thy [lconf_def]
-"\\<And>X. \\<lbrakk>G,s\\<turnstile>l[\\<Colon>\\<preceq>]L; G,s\\<turnstile>v\\<Colon>\\<preceq>T\\<rbrakk> \\<Longrightarrow> G,s\\<turnstile>l(vn\\<mapsto>v)[\\<Colon>\\<preceq>]L(vn\\<mapsto>T)"
+"!!X. [|G,s\\<turnstile>l[::\\<preceq>]L; G,s\\<turnstile>v::\\<preceq>T|] ==> G,s\\<turnstile>l(vn\\<mapsto>v)[::\\<preceq>]L(vn\\<mapsto>T)"
(K [Auto_tac]);
-Goalw [lconf_def] "G,h\\<turnstile>l[\\<Colon>\\<preceq>]L \\<Longrightarrow> \\<forall>vs Ts. nodups vns \\<longrightarrow> length Ts = length vns \\<longrightarrow> list_all2 (\\<lambda>v T. G,h\\<turnstile>v\\<Colon>\\<preceq>T) vs Ts \\<longrightarrow> G,h\\<turnstile>l(vns[\\<mapsto>]vs)[\\<Colon>\\<preceq>]L(vns[\\<mapsto>]Ts)";
+Goalw [lconf_def] "G,h\\<turnstile>l[::\\<preceq>]L ==> \\<forall>vs Ts. nodups vns --> length Ts = length vns --> list_all2 (\\<lambda>v T. G,h\\<turnstile>v::\\<preceq>T) vs Ts --> G,h\\<turnstile>l(vns[\\<mapsto>]vs)[::\\<preceq>]L(vns[\\<mapsto>]Ts)";
by( induct_tac "vns" 1);
by( ALLGOALS Clarsimp_tac);
by( forward_tac [list_all2_lengthD] 1);
@@ -214,10 +214,10 @@
section "oconf";
val oconf_hext = prove_goalw thy [oconf_def]
-"\\<And>X. G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> h\\<le>|h' \\<Longrightarrow> G,h'\\<turnstile>obj\\<surd>" (K [Fast_tac 1]);
+"!!X. G,h\\<turnstile>obj\\<surd> ==> h\\<le>|h' ==> G,h'\\<turnstile>obj\\<surd>" (K [Fast_tac 1]);
val oconf_obj = prove_goalw thy [oconf_def,lconf_def] "G,h\\<turnstile>(C,fs)\\<surd> = \
-\ (\\<forall>T f. map_of(fields (G,C)) f = Some T \\<longrightarrow> (\\<exists>v. fs f = Some v \\<and> G,h\\<turnstile>v\\<Colon>\\<preceq>T))"(K [
+\ (\\<forall>T f. map_of(fields (G,C)) f = Some T --> (\\<exists>v. fs f = Some v \\<and> G,h\\<turnstile>v::\\<preceq>T))"(K [
Auto_tac]);
val oconf_objD = oconf_obj RS iffD1 RS spec RS spec RS mp;
@@ -225,11 +225,11 @@
section "hconf";
-Goalw [hconf_def] "\\<lbrakk>G\\<turnstile>h h\\<surd>; h a = Some obj\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>obj\\<surd>";
+Goalw [hconf_def] "[|G\\<turnstile>h h\\<surd>; h a = Some obj|] ==> G,h\\<turnstile>obj\\<surd>";
by (Fast_tac 1);
qed "hconfD";
-Goalw [hconf_def] "\\<forall>a obj. h a=Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> G\\<turnstile>h h\\<surd>";
+Goalw [hconf_def] "\\<forall>a obj. h a=Some obj --> G,h\\<turnstile>obj\\<surd> ==> G\\<turnstile>h h\\<surd>";
by (Fast_tac 1);
qed "hconfI";
@@ -237,25 +237,25 @@
section "conforms";
val conforms_heapD = prove_goalw thy [conforms_def]
- "(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G\\<turnstile>h h\\<surd>"
+ "(h, l)::\\<preceq>(G, lT) ==> G\\<turnstile>h h\\<surd>"
(fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1]);
val conforms_localD = prove_goalw thy [conforms_def]
- "(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT" (fn prems => [
+ "(h, l)::\\<preceq>(G, lT) ==> G,h\\<turnstile>l[::\\<preceq>]lT" (fn prems => [
cut_facts_tac prems 1, Asm_full_simp_tac 1]);
val conformsI = prove_goalw thy [conforms_def]
-"\\<lbrakk>G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT\\<rbrakk> \\<Longrightarrow> (h, l)\\<Colon>\\<preceq>(G, lT)" (fn prems => [
+"[|G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[::\\<preceq>]lT|] ==> (h, l)::\\<preceq>(G, lT)" (fn prems => [
cut_facts_tac prems 1,
Simp_tac 1,
Auto_tac]);
-Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> \\<rbrakk> \\<Longrightarrow> (h',l)\\<Colon>\\<preceq>(G,lT)";
+Goal "[|(h,l)::\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> |] ==> (h',l)::\\<preceq>(G,lT)";
by( fast_tac (HOL_cs addDs [conforms_localD]
addSEs [conformsI, lconf_hext]) 1);
qed "conforms_hext";
-Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G, lT); G,h(a\\<mapsto>obj)\\<turnstile>obj\\<surd>; h\\<le>|h(a\\<mapsto>obj)\\<rbrakk> \\<Longrightarrow> (h(a\\<mapsto>obj),l)\\<Colon>\\<preceq>(G, lT)";
+Goal "[|(h,l)::\\<preceq>(G, lT); G,h(a\\<mapsto>obj)\\<turnstile>obj\\<surd>; h\\<le>|h(a\\<mapsto>obj)|] ==> (h(a\\<mapsto>obj),l)::\\<preceq>(G, lT)";
by( rtac conforms_hext 1);
by Auto_tac;
by( rtac hconfI 1);
@@ -265,7 +265,7 @@
qed "conforms_upd_obj";
Goalw [conforms_def]
-"\\<lbrakk>(h, l)\\<Colon>\\<preceq>(G, lT); G,h\\<turnstile>v\\<Colon>\\<preceq>T; lT va = Some T\\<rbrakk> \\<Longrightarrow> \
-\ (h, l(va\\<mapsto>v))\\<Colon>\\<preceq>(G, lT)";
+"[|(h, l)::\\<preceq>(G, lT); G,h\\<turnstile>v::\\<preceq>T; lT va = Some T|] ==> \
+\ (h, l(va\\<mapsto>v))::\\<preceq>(G, lT)";
by( auto_tac (claset() addEs [lconf_upd], simpset()));
qed "conforms_upd_local";
--- a/src/HOL/MicroJava/J/Conform.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Thu Sep 21 10:42:49 2000 +0200
@@ -12,23 +12,23 @@
constdefs
- hext :: "aheap \\<Rightarrow> aheap \\<Rightarrow> bool" ( "_\\<le>|_" [51,51] 50)
- "h\\<le>|h' \\<equiv> \\<forall>a C fs. h a = Some(C,fs) \\<longrightarrow> (\\<exists>fs'. h' a = Some(C,fs'))"
+ hext :: "aheap => aheap => bool" ( "_\\<le>|_" [51,51] 50)
+ "h\\<le>|h' == \\<forall>a C fs. h a = Some(C,fs) --> (\\<exists>fs'. h' a = Some(C,fs'))"
- conf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> ty \\<Rightarrow> bool" ( "_,_\\<turnstile>_\\<Colon>\\<preceq>_" [51,51,51,51] 50)
- "G,h\\<turnstile>v\\<Colon>\\<preceq>T \\<equiv> \\<exists>T'. typeof (option_map obj_ty o h) v = Some T' \\<and> G\\<turnstile>T'\\<preceq>T"
+ conf :: "'c prog => aheap => val => ty => bool" ( "_,_\\<turnstile>_::\\<preceq>_" [51,51,51,51] 50)
+ "G,h\\<turnstile>v::\\<preceq>T == \\<exists>T'. typeof (option_map obj_ty o h) v = Some T' \\<and> G\\<turnstile>T'\\<preceq>T"
- lconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> ('a \\<leadsto> val) \\<Rightarrow> ('a \\<leadsto> ty) \\<Rightarrow> bool"
- ("_,_\\<turnstile>_[\\<Colon>\\<preceq>]_" [51,51,51,51] 50)
- "G,h\\<turnstile>vs[\\<Colon>\\<preceq>]Ts \\<equiv> \\<forall>n T. Ts n = Some T \\<longrightarrow> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v\\<Colon>\\<preceq>T)"
+ lconf :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
+ ("_,_\\<turnstile>_[::\\<preceq>]_" [51,51,51,51] 50)
+ "G,h\\<turnstile>vs[::\\<preceq>]Ts == \\<forall>n T. Ts n = Some T --> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v::\\<preceq>T)"
- oconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> obj \\<Rightarrow> bool" ("_,_\\<turnstile>_\\<surd>" [51,51,51] 50)
- "G,h\\<turnstile>obj\\<surd> \\<equiv> G,h\\<turnstile>snd obj[\\<Colon>\\<preceq>]map_of (fields (G,fst obj))"
+ oconf :: "'c prog => aheap => obj => bool" ("_,_\\<turnstile>_\\<surd>" [51,51,51] 50)
+ "G,h\\<turnstile>obj\\<surd> == G,h\\<turnstile>snd obj[::\\<preceq>]map_of (fields (G,fst obj))"
- hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool" ("_\\<turnstile>h _\\<surd>" [51,51] 50)
- "G\\<turnstile>h h\\<surd> \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
+ hconf :: "'c prog => aheap => bool" ("_\\<turnstile>h _\\<surd>" [51,51] 50)
+ "G\\<turnstile>h h\\<surd> == \\<forall>a obj. h a = Some obj --> G,h\\<turnstile>obj\\<surd>"
- conforms :: "state \\<Rightarrow> java_mb env_ \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50)
- "s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
+ conforms :: "state => java_mb env_ => bool" ("_::\\<preceq>_" [51,51] 50)
+ "s::\\<preceq>E == prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[::\\<preceq>]localT E"
end
--- a/src/HOL/MicroJava/J/Decl.ML Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Decl.ML Thu Sep 21 10:42:49 2000 +0200
@@ -8,8 +8,8 @@
rtac finite_map_of 1]);
val is_classI = prove_goalw thy [is_class_def]
-"\\<And>G. class G C = Some c \\<Longrightarrow> is_class G C" (K [Auto_tac]);
+"!!G. class G C = Some c ==> is_class G C" (K [Auto_tac]);
val is_classD = prove_goalw thy [is_class_def]
-"\\<And>G. is_class G C \\<Longrightarrow> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
+"!!G. is_class G C ==> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);
--- a/src/HOL/MicroJava/J/Decl.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy Thu Sep 21 10:42:49 2000 +0200
@@ -32,26 +32,26 @@
defs
- ObjectC_def "ObjectC \\<equiv> (Object, (None, [], []))"
+ ObjectC_def "ObjectC == (Object, (None, [], []))"
types 'c prog = "'c cdecl list"
consts
- class :: "'c prog \\<Rightarrow> (cname \\<leadsto> 'c class)"
+ class :: "'c prog => (cname \\<leadsto> 'c class)"
- is_class :: "'c prog \\<Rightarrow> cname \\<Rightarrow> bool"
- is_type :: "'c prog \\<Rightarrow> ty \\<Rightarrow> bool"
+ is_class :: "'c prog => cname => bool"
+ is_type :: "'c prog => ty => bool"
defs
- class_def "class \\<equiv> map_of"
+ class_def "class == map_of"
- is_class_def "is_class G C \\<equiv> class G C \\<noteq> None"
+ is_class_def "is_class G C == class G C \\<noteq> None"
primrec
"is_type G (PrimT pt) = True"
-"is_type G (RefT t) = (case t of NullT \\<Rightarrow> True | ClassT C \\<Rightarrow> is_class G C)"
+"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
end
--- a/src/HOL/MicroJava/J/Eval.ML Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.ML Thu Sep 21 10:42:49 2000 +0200
@@ -4,44 +4,44 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-Goal "\\<lbrakk>new_Addr (heap s) = (a,x); \
-\ s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)\\<rbrakk> \\<Longrightarrow> \
-\ G\\<turnstile>Norm s -NewC C\\<succ>Addr a\\<rightarrow> s'";
+Goal "[|new_Addr (heap s) = (a,x); \
+\ s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> \
+\ G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> s'";
by (hyp_subst_tac 1);
br eval_evals_exec.NewC 1;
by Auto_tac;
qed "NewCI";
-Goal "\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ> v \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
-\ (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
-\ (G\\<turnstile>(x,s) -c \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None)";
+Goal "!!s s'. (G\\<turnstile>(x,s) -e \\<succ> v -> (x',s') --> x'=None --> x=None) \\<and> \
+\ (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x'=None --> x=None) \\<and> \
+\ (G\\<turnstile>(x,s) -c -> (x',s') --> x'=None --> x=None)";
by(split_all_tac 1);
by(rtac eval_evals_exec.induct 1);
by(rewtac c_hupd_def);
by(ALLGOALS Asm_full_simp_tac);
qed "eval_evals_exec_no_xcpt";
-val eval_no_xcpt = prove_goal thy "\\<And>X. G\\<turnstile>(x,s) -e\\<succ>v\\<rightarrow> (None,s') \\<Longrightarrow> x=None" (K [
+val eval_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e\\<succ>v-> (None,s') ==> x=None" (K [
dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1,
Fast_tac 1]);
-val evals_no_xcpt = prove_goal thy "\\<And>X. G\\<turnstile>(x,s) -e[\\<succ>]v\\<rightarrow> (None,s') \\<Longrightarrow> x=None" (K [
+val evals_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e[\\<succ>]v-> (None,s') ==> x=None" (K [
dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1,
Fast_tac 1]);
val eval_evals_exec_xcpt = prove_goal thy
-"\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ> v \\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s) \\<and> \
-\ (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s) \\<and> \
-\ (G\\<turnstile>(x,s) -c \\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s)"
+"!!s s'. (G\\<turnstile>(x,s) -e \\<succ> v -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
+\ (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
+\ (G\\<turnstile>(x,s) -c -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s)"
(K [
split_all_tac 1,
rtac eval_evals_exec.induct 1,
rewtac c_hupd_def,
ALLGOALS Asm_full_simp_tac]);
val eval_xcpt = prove_goal thy
-"\\<And>X. G\\<turnstile>(Some xc,s) -e\\<succ>v\\<rightarrow> (x',s') \\<Longrightarrow> x'=Some xc \\<and> s'=s" (K [
+"!!X. G\\<turnstile>(Some xc,s) -e\\<succ>v-> (x',s') ==> x'=Some xc \\<and> s'=s" (K [
dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1,
Fast_tac 1]);
val exec_xcpt = prove_goal thy
-"\\<And>X. G\\<turnstile>(Some xc,s) -s0\\<rightarrow> (x',s') \\<Longrightarrow> x'=Some xc \\<and> s'=s" (K [
+"!!X. G\\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \\<and> s'=s" (K [
dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1,
Fast_tac 1]);
--- a/src/HOL/MicroJava/J/Eval.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Thu Sep 21 10:42:49 2000 +0200
@@ -10,118 +10,118 @@
Eval = State + WellType +
consts
- eval :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr \\<times> val \\<times> xstate) set"
- evals :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr list \\<times> val list \\<times> xstate) set"
- exec :: "java_mb prog \\<Rightarrow> (xstate \\<times> stmt \\<times> xstate) set"
+ eval :: "java_mb prog => (xstate \\<times> expr \\<times> val \\<times> xstate) set"
+ evals :: "java_mb prog => (xstate \\<times> expr list \\<times> val list \\<times> xstate) set"
+ exec :: "java_mb prog => (xstate \\<times> stmt \\<times> xstate) set"
syntax
- eval :: "[java_mb prog,xstate,expr,val,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<succ>_\\<rightarrow> _"[51,82,82,82,82]81)
+ eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "("_\\<turnstile>_ -_\\<succ>_-> _"[51,82,82,82,82]81)
evals:: "[java_mb prog,xstate,expr list,
- val list,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_[\\<succ>]_\\<rightarrow> _"[51,82,51,51,82]81)
- exec :: "[java_mb prog,xstate,stmt, xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _" [51,82,82, 82]81)
+ val list,xstate] => bool "("_\\<turnstile>_ -_[\\<succ>]_-> _"[51,82,51,51,82]81)
+ exec :: "[java_mb prog,xstate,stmt, xstate] => bool "("_\\<turnstile>_ -_-> _" [51,82,82, 82]81)
translations
- "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" <= "(s, e, v, x, s') \\<in> eval G"
- "G\\<turnstile>s -e \\<succ> v\\<rightarrow> s' " == "(s, e, v, s' ) \\<in> eval G"
- "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> (x,s')" <= "(s, e, v, x, s') \\<in> evals G"
- "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> s' " == "(s, e, v, s' ) \\<in> evals G"
- "G\\<turnstile>s -c \\<rightarrow> (x,s')" <= "(s, c, x, s') \\<in> exec G"
- "G\\<turnstile>s -c \\<rightarrow> s' " == "(s, c, s') \\<in> exec G"
+ "G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval G"
+ "G\\<turnstile>s -e \\<succ> v-> s' " == "(s, e, v, s' ) \\<in> eval G"
+ "G\\<turnstile>s -e[\\<succ>]v-> (x,s')" <= "(s, e, v, x, s') \\<in> evals G"
+ "G\\<turnstile>s -e[\\<succ>]v-> s' " == "(s, e, v, s' ) \\<in> evals G"
+ "G\\<turnstile>s -c -> (x,s')" <= "(s, c, x, s') \\<in> exec G"
+ "G\\<turnstile>s -c -> s' " == "(s, c, s') \\<in> exec G"
inductive "eval G" "evals G" "exec G" intrs
(* evaluation of expressions *)
(* cf. 15.5 *)
- XcptE "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary\\<rightarrow> (Some xc,s)"
+ XcptE "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary-> (Some xc,s)"
(* cf. 15.8.1 *)
- NewC "\\<lbrakk>h = heap s; (a,x) = new_Addr h;
- h'= h(a\\<mapsto>(C,init_vars (fields (G,C))))\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s -NewC C\\<succ>Addr a\\<rightarrow> c_hupd h' (x,s)"
+ NewC "[|h = heap s; (a,x) = new_Addr h;
+ h'= h(a\\<mapsto>(C,init_vars (fields (G,C))))|] ==>
+ G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> c_hupd h' (x,s)"
(* cf. 15.15 *)
- Cast "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>v\\<rightarrow> (x1,s1);
- x2=raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s0 -Cast C e\\<succ>v\\<rightarrow> (x2,s1)"
+ Cast "[|G\\<turnstile>Norm s0 -e\\<succ>v-> (x1,s1);
+ x2=raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1|] ==>
+ G\\<turnstile>Norm s0 -Cast C e\\<succ>v-> (x2,s1)"
(* cf. 15.7.1 *)
- Lit "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s"
+ Lit "G\\<turnstile>Norm s -Lit v\\<succ>v-> Norm s"
- BinOp "\\<lbrakk>G\\<turnstile>Norm s -e1\\<succ>v1\\<rightarrow> s1;
- G\\<turnstile>s1 -e2\\<succ>v2\\<rightarrow> s2;
- v = (case bop of Eq \\<Rightarrow> Bool (v1 = v2)
- | Add \\<Rightarrow> Intg (the_Intg v1 + the_Intg v2))\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v\\<rightarrow> s2"
+ BinOp "[|G\\<turnstile>Norm s -e1\\<succ>v1-> s1;
+ G\\<turnstile>s1 -e2\\<succ>v2-> s2;
+ v = (case bop of Eq => Bool (v1 = v2)
+ | Add => Intg (the_Intg v1 + the_Intg v2))|] ==>
+ G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v-> s2"
(* cf. 15.13.1, 15.2 *)
- LAcc "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)\\<rightarrow> Norm s"
+ LAcc "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)-> Norm s"
(* cf. 15.25.1 *)
- LAss "\\<lbrakk>G\\<turnstile>Norm s -e\\<succ>v\\<rightarrow> (x,(h,l));
- l' = (if x = None then l(va\\<mapsto>v) else l)\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s -va\\<Colon>=e\\<succ>v\\<rightarrow> (x,(h,l'))"
+ LAss "[|G\\<turnstile>Norm s -e\\<succ>v-> (x,(h,l));
+ l' = (if x = None then l(va\\<mapsto>v) else l)|] ==>
+ G\\<turnstile>Norm s -va::=e\\<succ>v-> (x,(h,l'))"
(* cf. 15.10.1, 15.2 *)
- FAcc "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> (x1,s1);
- v = the (snd (the (heap s1 (the_Addr a'))) (fn,T))\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v\\<rightarrow> (np a' x1,s1)"
+ FAcc "[|G\\<turnstile>Norm s0 -e\\<succ>a'-> (x1,s1);
+ v = the (snd (the (heap s1 (the_Addr a'))) (fn,T))|] ==>
+ G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v-> (np a' x1,s1)"
(* cf. 15.25.1 *)
- FAss "\\<lbrakk>G\\<turnstile> Norm s0 -e1\\<succ>a'\\<rightarrow> (x1,s1); a = the_Addr a';
- G\\<turnstile>(np a' x1,s1) -e2\\<succ>v \\<rightarrow> (x2,s2);
+ FAss "[|G\\<turnstile> Norm s0 -e1\\<succ>a'-> (x1,s1); a = the_Addr a';
+ G\\<turnstile>(np a' x1,s1) -e2\\<succ>v -> (x2,s2);
h = heap s2; (c,fs) = the (h a);
- h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v))))\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v\\<rightarrow> c_hupd h' (x2,s2)"
+ h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v))))|] ==>
+ G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v-> c_hupd h' (x2,s2)"
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
- Call "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> s1; a = the_Addr a';
- G\\<turnstile>s1 -ps[\\<succ>]pvs\\<rightarrow> (x,(h,l)); dynT = fst (the (h a));
+ Call "[|G\\<turnstile>Norm s0 -e\\<succ>a'-> s1; a = the_Addr a';
+ G\\<turnstile>s1 -ps[\\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
(md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
- G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk\\<rightarrow> s3;
- G\\<turnstile> s3 -res\\<succ>v \\<rightarrow> (x4,s4)\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v\\<rightarrow> (x4,(heap s4,l))"
+ G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk-> s3;
+ G\\<turnstile> s3 -res\\<succ>v -> (x4,s4)|] ==>
+ G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
(* evaluation of expression lists *)
(* cf. 15.5 *)
- XcptEs "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary\\<rightarrow> (Some xc,s)"
+ XcptEs "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary-> (Some xc,s)"
(* cf. 15.11.??? *)
Nil
- "G\\<turnstile>Norm s0 -[][\\<succ>][]\\<rightarrow> Norm s0"
+ "G\\<turnstile>Norm s0 -[][\\<succ>][]-> Norm s0"
(* cf. 15.6.4 *)
- Cons "\\<lbrakk>G\\<turnstile>Norm s0 -e \\<succ> v \\<rightarrow> s1;
- G\\<turnstile> s1 -es[\\<succ>]vs\\<rightarrow> s2\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs\\<rightarrow> s2"
+ Cons "[|G\\<turnstile>Norm s0 -e \\<succ> v -> s1;
+ G\\<turnstile> s1 -es[\\<succ>]vs-> s2|] ==>
+ G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs-> s2"
(* execution of statements *)
(* cf. 14.1 *)
- XcptS "G\\<turnstile>(Some xc,s) -s0\\<rightarrow> (Some xc,s)"
+ XcptS "G\\<turnstile>(Some xc,s) -s0-> (Some xc,s)"
(* cf. 14.5 *)
- Skip "G\\<turnstile>Norm s -Skip\\<rightarrow> Norm s"
+ Skip "G\\<turnstile>Norm s -Skip-> Norm s"
(* cf. 14.7 *)
- Expr "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>v\\<rightarrow> s1\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s0 -Expr e\\<rightarrow> s1"
+ Expr "[|G\\<turnstile>Norm s0 -e\\<succ>v-> s1|] ==>
+ G\\<turnstile>Norm s0 -Expr e-> s1"
(* cf. 14.2 *)
- Comp "\\<lbrakk>G\\<turnstile>Norm s0 -s \\<rightarrow> s1;
- G\\<turnstile> s1 -t \\<rightarrow> s2\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s0 -(s;; t)\\<rightarrow> s2"
+ Comp "[|G\\<turnstile>Norm s0 -s -> s1;
+ G\\<turnstile> s1 -t -> s2|] ==>
+ G\\<turnstile>Norm s0 -(s;; t)-> s2"
(* cf. 14.8.2 *)
- Cond "\\<lbrakk>G\\<turnstile>Norm s0 -e \\<succ>v\\<rightarrow> s1;
- G\\<turnstile> s1 -(if the_Bool v then s else t)\\<rightarrow> s2\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s0 -(If(e) s Else t)\\<rightarrow> s2"
+ Cond "[|G\\<turnstile>Norm s0 -e \\<succ>v-> s1;
+ G\\<turnstile> s1 -(if the_Bool v then s else t)-> s2|] ==>
+ G\\<turnstile>Norm s0 -(If(e) s Else t)-> s2"
(* cf. 14.10, 14.10.1 *)
- Loop "\\<lbrakk>G\\<turnstile>Norm s0 -(If(e) (s;; While(e) s) Else Skip)\\<rightarrow> s1\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s0 -(While(e) s)\\<rightarrow> s1"
+ Loop "[|G\\<turnstile>Norm s0 -(If(e) (s;; While(e) s) Else Skip)-> s1|] ==>
+ G\\<turnstile>Norm s0 -(While(e) s)-> s1"
end
--- a/src/HOL/MicroJava/J/Example.ML Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.ML Thu Sep 21 10:42:49 2000 +0200
@@ -11,7 +11,7 @@
val map_of_Cons1 = prove_goalw Map.thy [get_def thy "map_of_list"]
"map_of ((x,y)#ps) x = Some y" (K [Simp_tac 1]);
val map_of_Cons2 = prove_goalw Map.thy [get_def thy "map_of_list"]
-"\\<And>X. x\\<noteq>k \\<Longrightarrow> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]);
+"!!X. x\\<noteq>k ==> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]);
Delsimps[map_of_Cons]; (* sic! *)
Addsimps[map_of_Cons1, map_of_Cons2];
@@ -30,12 +30,12 @@
Simp_tac 1]);
Addsimps [class_tprg_Object, class_tprg_Base, class_tprg_Ext];
-Goal "\\<And>X. (Object,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
+Goal "!!X. (Object,C) \\<in> (subcls1 tprg)^+ ==> R";
by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
qed "not_Object_subcls";
AddSEs [not_Object_subcls];
-Goal "tprg\\<turnstile>Object\\<preceq>C C \\<Longrightarrow> C = Object";
+Goal "tprg\\<turnstile>Object\\<preceq>C C ==> C = Object";
be rtrancl_induct 1;
by Auto_tac;
bd subcls1D 1;
@@ -43,16 +43,16 @@
qed "subcls_ObjectD";
AddSDs[subcls_ObjectD];
-Goal "\\<And>X. (Base, Ext) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
+Goal "!!X. (Base, Ext) \\<in> (subcls1 tprg)^+ ==> R";
by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
qed "not_Base_subcls_Ext";
AddSEs [not_Base_subcls_Ext];
-Goalw [class_def, ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z \\<Longrightarrow> C=Object \\<or> C=Base \\<or> C=Ext";
+Goalw [class_def, ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=Ext";
by (auto_tac (claset(),simpset()addsimps[]addsplits[split_if_asm]));
qed "class_tprgD";
-Goal "(C,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
+Goal "(C,C) \\<in> (subcls1 tprg)^+ ==> R";
by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
by (ftac class_tprgD 1);
by (auto_tac (claset() addSDs [],simpset()));
@@ -196,7 +196,7 @@
fun t thm = resolve_tac ty_expr_ty_exprs_wt_stmt.intrs 1 thm;
Goalw [test_def] "(tprg, empty(e\\<mapsto>Class Base))\\<turnstile>\
-\ Expr(e\\<Colon>=NewC Ext);; Expr(LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
+\ Expr(e::=NewC Ext);; Expr(LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
(* ?pTs' = [Class Base] *)
by t; (* ;; *)
by t; (* Expr *)
@@ -225,8 +225,8 @@
Delsplits[split_if];
Addsimps[init_vars_def,c_hupd_def,cast_ok_def];
Goalw [test_def]
-" \\<lbrakk>new_Addr (heap (snd s0)) = (a, None)\\<rbrakk> \\<Longrightarrow> \
-\ tprg\\<turnstile>s0 -test\\<rightarrow> ?s";
+" [|new_Addr (heap (snd s0)) = (a, None)|] ==> \
+\ tprg\\<turnstile>s0 -test-> ?s";
(* ?s = s3 *)
by e; (* ;; *)
by e; (* Expr *)
--- a/src/HOL/MicroJava/J/Example.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Thu Sep 21 10:42:49 2000 +0200
@@ -35,8 +35,8 @@
consts
- cnam_ :: "cnam_ \\<Rightarrow> cname"
- vnam_ :: "vnam_ \\<Rightarrow> vnam"
+ cnam_ :: "cnam_ => cname"
+ vnam_ :: "vnam_ => vnam"
rules (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
@@ -74,18 +74,18 @@
defs
- foo_Base_def "foo_Base \\<equiv> ([x],[],Skip,LAcc x)"
- BaseC_def "BaseC \\<equiv> (Base, (Some Object,
+ foo_Base_def "foo_Base == ([x],[],Skip,LAcc x)"
+ BaseC_def "BaseC == (Base, (Some Object,
[(vee, PrimT Boolean)],
[((foo,[Class Base]),Class Base,foo_Base)]))"
- foo_Ext_def "foo_Ext \\<equiv> ([x],[],Expr( {Ext}Cast Ext
+ foo_Ext_def "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
(LAcc x)..vee:=Lit (Intg #1)),
Lit Null)"
- ExtC_def "ExtC \\<equiv> (Ext, (Some Base ,
+ ExtC_def "ExtC == (Ext, (Some Base ,
[(vee, PrimT Integer)],
[((foo,[Class Base]),Class Ext,foo_Ext)]))"
- test_def "test \\<equiv> Expr(e\\<Colon>=NewC Ext);;
+ test_def "test == Expr(e::=NewC Ext);;
Expr(LAcc e..foo({[Class Base]}[Lit Null]))"
--- a/src/HOL/MicroJava/J/JBasis.ML Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/JBasis.ML Thu Sep 21 10:42:49 2000 +0200
@@ -7,25 +7,25 @@
val strip_tac1 = SELECT_GOAL (safe_tac (HOL_cs delrules [conjI, disjE, impCE]));
Goalw [image_def]
- "x \\<in> f``A \\<Longrightarrow> \\<exists>y. y \\<in> A \\<and> x = f y";
+ "x \\<in> f``A ==> \\<exists>y. y \\<in> A \\<and> x = f y";
by(Auto_tac);
qed "image_rev";
fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
val select_split = prove_goalw Prod.thy [split_def]
- "(\\<epsilon>(x,y). P x y) = (\\<epsilon>xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
+ "(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
val split_beta = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
(fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
val split_beta2 = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
(fn _ => [Auto_tac]);
-val splitE2 = prove_goal Prod.thy "\\<lbrakk>Q (split P z); \\<And>x y. \\<lbrakk>z = (x, y); Q (P x y)\\<rbrakk> \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> R" (fn prems => [
+val splitE2 = prove_goal Prod.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
rtac (split_beta RS subst) 1,
rtac (hd prems) 1]);
-val splitE2' = prove_goal Prod.thy "\\<lbrakk>((\\<lambda>(x,y). P x y) z) w; \\<And>x y. \\<lbrakk>z = (x, y); (P x y) w\\<rbrakk> \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> R" (fn prems => [
+val splitE2' = prove_goal Prod.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [
REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
res_inst_tac [("P1","P")] (split_beta RS subst) 1,
rtac (hd prems) 1]);
@@ -33,7 +33,7 @@
fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
-val BallE = prove_goal thy "\\<lbrakk>Ball A P; x \\<notin> A \\<Longrightarrow> Q; P x \\<Longrightarrow> Q \\<rbrakk> \\<Longrightarrow> Q"
+val BallE = prove_goal thy "[|Ball A P; x \\<notin> A ==> Q; P x ==> Q |] ==> Q"
(fn prems => [rtac ballE 1, resolve_tac prems 1,
eresolve_tac prems 1, eresolve_tac prems 1]);
@@ -43,7 +43,7 @@
(* To HOL.ML *)
-val ex1_some_eq_trivial = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y"
+val ex1_some_eq_trivial = prove_goal HOL.thy "[| \\<exists>!x. P x; P y |] ==> Eps P = y"
(fn prems => [
cut_facts_tac prems 1,
rtac some_equality 1,
@@ -74,7 +74,7 @@
asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];
val optionE = prove_goal thy
- "\\<lbrakk> opt = None \\<Longrightarrow> P; \\<And>x. opt = Some x \\<Longrightarrow> P \\<rbrakk> \\<Longrightarrow> P"
+ "[| opt = None ==> P; !!x. opt = Some x ==> P |] ==> P"
(fn prems => [
case_tac "opt = None" 1,
eresolve_tac prems 1,
@@ -87,7 +87,7 @@
rotate_tac ~1 i , asm_full_simp_tac HOL_basic_ss i];
val option_map_SomeD = prove_goalw thy [option_map_def]
- "\\<And>x. option_map f x = Some y \\<Longrightarrow> \\<exists>z. x = Some z \\<and> f z = y" (K [
+ "!!x. option_map f x = Some y ==> \\<exists>z. x = Some z \\<and> f z = y" (K [
option_case_tac2 "x" 1,
Auto_tac]);
@@ -120,19 +120,19 @@
by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq]));
qed_spec_mp "unique_map_inj";
-Goal "\\<And>l. unique l \\<Longrightarrow> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
+Goal "!!l. unique l ==> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
by(etac unique_map_inj 1);
by(rtac injI 1);
by Auto_tac;
qed "unique_map_Pair";
-Goal "\\<lbrakk>M = N; \\<And>x. x\\<in>N \\<Longrightarrow> f x = g x\\<rbrakk> \\<Longrightarrow> f``M = g``N";
+Goal "[|M = N; !!x. x\\<in>N ==> f x = g x|] ==> f``M = g``N";
by(rtac set_ext 1);
by(simp_tac (simpset() addsimps image_def::premises()) 1);
qed "image_cong";
val split_Pair_eq = prove_goal Prod.thy
-"\\<And>X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A \\<Longrightarrow> y = Y" (K [
+"!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [
etac imageE 1,
split_all_tac 1,
auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]);
@@ -140,7 +140,7 @@
(* More about Maps *)
-val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x \\<Longrightarrow> \
+val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x ==> \
\ t k = Some x | t k = None \\<and> s k = Some x" (fn prems => [
cut_facts_tac prems 1,
case_tac "\\<exists>x. t k = Some x" 1,
@@ -153,7 +153,7 @@
Addsimps [fun_upd_same, fun_upd_other];
-Goal "unique xys \\<longrightarrow> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
+Goal "unique xys --> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
by(induct_tac "xys" 1);
by(Simp_tac 1);
by(force_tac (claset(), simpset() addsimps [unique_Cons]) 1);
@@ -162,7 +162,7 @@
val in_set_get = unique_map_of_Some_conv RS iffD2;
val get_in_set = unique_map_of_Some_conv RS iffD1;
-Goal "(\\<forall>(x,y)\\<in>set l. P x y) \\<longrightarrow> (\\<forall>x. \\<forall>y. map_of l x = Some y \\<longrightarrow> P x y)";
+Goal "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)";
by(induct_tac "l" 1);
by(ALLGOALS Simp_tac);
by Safe_tac;
@@ -170,37 +170,37 @@
bind_thm("Ball_set_table",result() RS mp);
val table_mono = prove_goal thy
-"unique l' \\<longrightarrow> (\\<forall>xy. (xy)\\<in>set l \\<longrightarrow> (xy)\\<in>set l') \\<longrightarrow>\
-\ (\\<forall>k y. map_of l k = Some y \\<longrightarrow> map_of l' k = Some y)" (fn _ => [
+"unique l' --> (\\<forall>xy. (xy)\\<in>set l --> (xy)\\<in>set l') -->\
+\ (\\<forall>k y. map_of l k = Some y --> map_of l' k = Some y)" (fn _ => [
induct_tac "l" 1,
Auto_tac,
fast_tac (HOL_cs addSIs [in_set_get]) 1])
RS mp RS mp RS spec RS spec RS mp;
-val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) \\<longrightarrow> \
+val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) --> \
\ map_of (map (\\<lambda>u. ((fst u, fst (snd u)), snd (snd u))) t) (k, k') = Some x" (K [
induct_tac "t" 1,
ALLGOALS Simp_tac,
case_tac1 "k = fst a" 1,
Auto_tac]) RS mp;
val table_map_Some = prove_goal thy
-"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \\<longrightarrow> \
+"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \
\map_of t (k, k') = Some x" (K [
induct_tac "t" 1,
Auto_tac]) RS mp;
-val table_mapf_Some = prove_goal thy "\\<And>f. \\<forall>x y. f x = f y \\<longrightarrow> x = y \\<Longrightarrow> \
-\ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) \\<longrightarrow> map_of t k = Some x" (K [
+val table_mapf_Some = prove_goal thy "!!f. \\<forall>x y. f x = f y --> x = y ==> \
+\ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) --> map_of t k = Some x" (K [
induct_tac "t" 1,
Auto_tac]) RS mp;
val table_mapf_SomeD = prove_goal thy
-"map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z \\<longrightarrow> (\\<exists>y. (k,y)\\<in>set t \\<and> z = f y)"(K [
+"map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z --> (\\<exists>y. (k,y)\\<in>set t \\<and> z = f y)"(K [
induct_tac "t" 1,
Auto_tac]) RS mp;
val table_mapf_Some2 = prove_goal thy
-"\\<And>k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) \\<Longrightarrow> C = D \\<and> map_of t k = Some x" (K [
+"!!k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) ==> C = D \\<and> map_of t k = Some x" (K [
forward_tac [table_mapf_SomeD] 1,
Auto_tac,
rtac table_mapf_Some 1,
--- a/src/HOL/MicroJava/J/JBasis.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/JBasis.thy Thu Sep 21 10:42:49 2000 +0200
@@ -10,7 +10,7 @@
constdefs
- unique :: "('a \\<times> 'b) list \\<Rightarrow> bool"
- "unique \\<equiv> nodups \\<circ> map fst"
+ unique :: "('a \\<times> 'b) list => bool"
+ "unique == nodups \\<circ> map fst"
end
--- a/src/HOL/MicroJava/J/JTypeSafe.ML Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML Thu Sep 21 10:42:49 2000 +0200
@@ -9,16 +9,16 @@
Addsimps [split_beta];
-Goal "\\<lbrakk>h a = None; (h, l)\\<Colon>\\<preceq>(G, lT); wf_prog wf_mb G; is_class G C\\<rbrakk> \\<Longrightarrow> \
-\ (h(a\\<mapsto>(C,(init_vars (fields (G,C))))), l)\\<Colon>\\<preceq>(G, lT)";
+Goal "[|h a = None; (h, l)::\\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> \
+\ (h(a\\<mapsto>(C,(init_vars (fields (G,C))))), l)::\\<preceq>(G, lT)";
by( etac conforms_upd_obj 1);
by( rewtac oconf_def);
by( auto_tac (claset() addSDs [is_type_fields, map_of_SomeD], simpset()));
qed "NewC_conforms";
Goalw [cast_ok_def]
- "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Class C; G\\<turnstile>C\\<preceq>? D; cast_ok G D h v\\<rbrakk> \
-\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>Class D";
+ "[| wf_prog wf_mb G; G,h\\<turnstile>v::\\<preceq>Class C; G\\<turnstile>C\\<preceq>? D; cast_ok G D h v|] \
+\ ==> G,h\\<turnstile>v::\\<preceq>Class D";
by( case_tac1 "v = Null" 1);
by( Asm_full_simp_tac 1);
by( dtac widen_RefT 1);
@@ -28,9 +28,9 @@
by( auto_tac (claset() addSIs [conf_AddrI], simpset() addsimps [obj_ty_def]));
qed "Cast_conf";
-Goal "\\<lbrakk> wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
-\ x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq> Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \
-\ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))\\<Colon>\\<preceq>ft";
+Goal "[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)::\\<preceq>(G,lT); \
+\ x' = None --> G,h\\<turnstile>a'::\\<preceq> Class C; np a' x' = None |] ==> \
+\ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\\<preceq>ft";
by( dtac np_NoneD 1);
by( etac conjE 1);
by( mp_tac 1);
@@ -47,15 +47,15 @@
qed "FAcc_type_sound";
Goal
- "\\<lbrakk> wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); \
-\ (G, lT)\\<turnstile>v\\<Colon>T'; G\\<turnstile>T'\\<preceq>ft; \
-\ (G, lT)\\<turnstile>aa\\<Colon>Class C; \
+ "[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); \
+\ (G, lT)\\<turnstile>v::T'; G\\<turnstile>T'\\<preceq>ft; \
+\ (G, lT)\\<turnstile>aa::Class C; \
\ field (G,C) fn = Some (fd, ft); h''\\<le>|h'; \
-\ x' = None \\<longrightarrow> G,h'\\<turnstile>a'\\<Colon>\\<preceq> Class C; h'\\<le>|h; \
-\ (h, l)\\<Colon>\\<preceq>(G, lT); G,h\\<turnstile>x\\<Colon>\\<preceq>T'; np a' x' = None\\<rbrakk> \\<Longrightarrow> \
+\ x' = None --> G,h'\\<turnstile>a'::\\<preceq> Class C; h'\\<le>|h; \
+\ (h, l)::\\<preceq>(G, lT); G,h\\<turnstile>x::\\<preceq>T'; np a' x' = None|] ==> \
\ h''\\<le>|h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))) \\<and> \
-\ (h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))), l)\\<Colon>\\<preceq>(G, lT) \\<and> \
-\ G,h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x))))\\<turnstile>x\\<Colon>\\<preceq>T'";
+\ (h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))), l)::\\<preceq>(G, lT) \\<and> \
+\ G,h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x))))\\<turnstile>x::\\<preceq>T'";
by( dtac np_NoneD 1);
by( etac conjE 1);
by( Asm_full_simp_tac 1);
@@ -91,11 +91,11 @@
by( fast_tac (HOL_cs addDs [conforms_heapD RS hconfD, oconf_objD]) 1);
qed "FAss_type_sound";
-Goalw [wf_mhead_def] "\\<lbrakk> wf_prog wf_mb G; list_all2 (conf G h) pvs pTs; \
+Goalw [wf_mhead_def] "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs; \
\ list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT; \
\ length pTs' = length pns; nodups pns; \
\ Ball (set lvars) (split (\\<lambda>vn. is_type G)) \
-\ \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>init_vars lvars(pns[\\<mapsto>]pvs)[\\<Colon>\\<preceq>]map_of lvars(pns[\\<mapsto>]pTs')";
+\ |] ==> G,h\\<turnstile>init_vars lvars(pns[\\<mapsto>]pvs)[::\\<preceq>]map_of lvars(pns[\\<mapsto>]pTs')";
by( Clarsimp_tac 1);
by( rtac lconf_ext_list 1);
by( rtac (Ball_set_table RS lconf_init_vars) 1);
@@ -106,17 +106,17 @@
qed "Call_lemma2";
Goalw [wf_java_prog_def]
- "\\<lbrakk> wf_java_prog G; a' \\<noteq> Null; (h, l)\\<Colon>\\<preceq>(G, lT); \
+ "[| wf_java_prog G; a' \\<noteq> Null; (h, l)::\\<preceq>(G, lT); \
\ max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\\<le>|xh; xh\\<le>|h; \
\ list_all2 (conf G h) pvs pTsa;\
\ (md, rT, pns, lvars, blk, res) = \
\ the (method (G,fst (the (h (the_Addr a')))) (mn, pTs'));\
-\ \\<forall>lT. (h, init_vars lvars(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> \
-\ (G, lT)\\<turnstile>blk\\<surd> \\<longrightarrow> h\\<le>|xi \\<and> (xi, xl)\\<Colon>\\<preceq>(G, lT); \
-\ \\<forall>lT. (xi, xl)\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> (\\<forall>T. (G, lT)\\<turnstile>res\\<Colon>T \\<longrightarrow> \
-\ xi\\<le>|h' \\<and> (h', xj)\\<Colon>\\<preceq>(G, lT) \\<and> (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>T)); \
-\ G,xh\\<turnstile>a'\\<Colon>\\<preceq> Class C \\<rbrakk> \\<Longrightarrow> \
-\ xc\\<le>|h' \\<and> (h', l)\\<Colon>\\<preceq>(G, lT) \\<and> (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>rTa)";
+\ \\<forall>lT. (h, init_vars lvars(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))::\\<preceq>(G, lT) --> \
+\ (G, lT)\\<turnstile>blk\\<surd> --> h\\<le>|xi \\<and> (xi, xl)::\\<preceq>(G, lT); \
+\ \\<forall>lT. (xi, xl)::\\<preceq>(G, lT) --> (\\<forall>T. (G, lT)\\<turnstile>res::T --> \
+\ xi\\<le>|h' \\<and> (h', xj)::\\<preceq>(G, lT) \\<and> (x' = None --> G,h'\\<turnstile>v::\\<preceq>T)); \
+\ G,xh\\<turnstile>a'::\\<preceq> Class C |] ==> \
+\ xc\\<le>|h' \\<and> (h', l)::\\<preceq>(G, lT) \\<and> (x' = None --> G,h'\\<turnstile>v::\\<preceq>rTa)";
by( dtac (insertI1 RSN (2,(equalityD2 RS subsetD))) 1);
by( dtac (max_spec2appl_meths RS appl_methsD) 1);
by( Clarify_tac 1);
@@ -139,9 +139,9 @@
by( thin_tac "?E\\<turnstile>?blk\\<surd>" 1);
by( etac conjE 1);
by( EVERY'[dtac spec, mp_tac] 1);
-(*by( thin_tac "?E\\<Colon>\\<preceq>(G, pT')" 1);*)
+(*by( thin_tac "?E::\\<preceq>(G, pT')" 1);*)
by( EVERY'[dtac spec, mp_tac] 1);
-by( thin_tac "?E\\<turnstile>res\\<Colon>?rT" 1);
+by( thin_tac "?E\\<turnstile>res::?rT" 1);
by( strip_tac1 1);
by( rtac conjI 1);
by( fast_tac (HOL_cs addIs [hext_trans]) 1);
@@ -167,16 +167,16 @@
val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]));
Goal
-"wf_java_prog G \\<Longrightarrow> \
-\ (G\\<turnstile>(x,(h,l)) -e \\<succ>v \\<rightarrow> (x', (h',l')) \\<longrightarrow> \
-\ (\\<forall>lT. (h ,l )\\<Colon>\\<preceq>(G,lT) \\<longrightarrow> (\\<forall>T . (G,lT)\\<turnstile>e \\<Colon> T \\<longrightarrow> \
-\ h\\<le>|h' \\<and> (h',l')\\<Colon>\\<preceq>(G,lT) \\<and> (x'=None \\<longrightarrow> G,h'\\<turnstile>v \\<Colon>\\<preceq> T )))) \\<and> \
-\ (G\\<turnstile>(x,(h,l)) -es[\\<succ>]vs\\<rightarrow> (x', (h',l')) \\<longrightarrow> \
-\ (\\<forall>lT. (h ,l )\\<Colon>\\<preceq>(G,lT) \\<longrightarrow> (\\<forall>Ts. (G,lT)\\<turnstile>es[\\<Colon>]Ts \\<longrightarrow> \
-\ h\\<le>|h' \\<and> (h',l')\\<Colon>\\<preceq>(G,lT) \\<and> (x'=None \\<longrightarrow> list_all2 (\\<lambda>v T. G,h'\\<turnstile>v\\<Colon>\\<preceq>T) vs Ts)))) \\<and> \
-\ (G\\<turnstile>(x,(h,l)) -c \\<rightarrow> (x', (h',l')) \\<longrightarrow> \
-\ (\\<forall>lT. (h ,l )\\<Colon>\\<preceq>(G,lT) \\<longrightarrow> (G,lT)\\<turnstile>c \\<surd> \\<longrightarrow> \
-\ h\\<le>|h' \\<and> (h',l')\\<Colon>\\<preceq>(G,lT)))";
+"wf_java_prog G ==> \
+\ (G\\<turnstile>(x,(h,l)) -e \\<succ>v -> (x', (h',l')) --> \
+\ (\\<forall>lT. (h ,l )::\\<preceq>(G,lT) --> (\\<forall>T . (G,lT)\\<turnstile>e :: T --> \
+\ h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT) \\<and> (x'=None --> G,h'\\<turnstile>v ::\\<preceq> T )))) \\<and> \
+\ (G\\<turnstile>(x,(h,l)) -es[\\<succ>]vs-> (x', (h',l')) --> \
+\ (\\<forall>lT. (h ,l )::\\<preceq>(G,lT) --> (\\<forall>Ts. (G,lT)\\<turnstile>es[::]Ts --> \
+\ h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT) \\<and> (x'=None --> list_all2 (\\<lambda>v T. G,h'\\<turnstile>v::\\<preceq>T) vs Ts)))) \\<and> \
+\ (G\\<turnstile>(x,(h,l)) -c -> (x', (h',l')) --> \
+\ (\\<forall>lT. (h ,l )::\\<preceq>(G,lT) --> (G,lT)\\<turnstile>c \\<surd> --> \
+\ h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT)))";
by( rtac eval_evals_exec.induct 1);
by( rewtac c_hupd_def);
@@ -298,24 +298,24 @@
THEN_ALL_NEW Asm_simp_tac) 1);
qed "eval_evals_exec_type_sound";
-Goal "\\<And>E s s'. \
-\ \\<lbrakk> G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>v \\<rightarrow> (x',s'); s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>T \\<rbrakk> \
-\ \\<Longrightarrow> s'\\<Colon>\\<preceq>E \\<and> (x'=None \\<longrightarrow> G,heap s'\\<turnstile>v\\<Colon>\\<preceq>T)";
+Goal "!!E s s'. \
+\ [| G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>v -> (x',s'); s::\\<preceq>E; E\\<turnstile>e::T |] \
+\ ==> s'::\\<preceq>E \\<and> (x'=None --> G,heap s'\\<turnstile>v::\\<preceq>T)";
by( split_all_tac 1);
bd (eval_evals_exec_type_sound RS conjunct1 RS mp RS spec RS mp) 1;
by Auto_tac;
qed "eval_type_sound";
-Goal "\\<And>E s s'. \
-\ \\<lbrakk> G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -s0\\<rightarrow> (x',s'); s\\<Colon>\\<preceq>E; E\\<turnstile>s0\\<surd> \\<rbrakk> \
-\ \\<Longrightarrow> s'\\<Colon>\\<preceq>E";
+Goal "!!E s s'. \
+\ [| G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -s0-> (x',s'); s::\\<preceq>E; E\\<turnstile>s0\\<surd> |] \
+\ ==> s'::\\<preceq>E";
by( split_all_tac 1);
bd (eval_evals_exec_type_sound RS conjunct2 RS conjunct2 RS mp RS spec RS mp) 1;
by Auto_tac;
qed "exec_type_sound";
-Goal "\\<lbrakk>G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>a'\\<rightarrow> Norm s'; a' \\<noteq> Null;\
-\ s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>Class C; method (G,C) sig \\<noteq> None\\<rbrakk> \\<Longrightarrow> \
+Goal "[|G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>a'-> Norm s'; a' \\<noteq> Null;\
+\ s::\\<preceq>E; E\\<turnstile>e::Class C; method (G,C) sig \\<noteq> None|] ==> \
\ method (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
by( datac eval_type_sound 4 1);
by( not_None_tac 1);
--- a/src/HOL/MicroJava/J/State.ML Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/State.ML Thu Sep 21 10:42:49 2000 +0200
@@ -10,7 +10,7 @@
Addsimps [obj_ty_def2];
val new_AddrD = prove_goalw thy [new_Addr_def]
-"\\<And>X. (a,x) = new_Addr h \\<Longrightarrow> h a = None \\<and> x = None | x = Some OutOfMemory" (K[
+"!!X. (a,x) = new_Addr h ==> h a = None \\<and> x = None | x = Some OutOfMemory" (K[
asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1,
rtac someI 1,
rtac disjI2 1,
@@ -40,20 +40,20 @@
Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2,if_None_eq];
val raise_if_SomeD = prove_goalw thy [raise_if_def]
- "raise_if c x y = Some z \\<longrightarrow> c \\<and> Some z = Some x | y = Some z"
+ "raise_if c x y = Some z --> c \\<and> Some z = Some x | y = Some z"
(K [split_tac [split_if] 1,Auto_tac]) RS mp;
val raise_if_NoneD = prove_goalw thy [raise_if_def]
- "raise_if c x y = None \\<longrightarrow> \\<not> c \\<and> y = None"
+ "raise_if c x y = None --> \\<not> c \\<and> y = None"
(K [split_tac [split_if] 1,Auto_tac]) RS mp;
val np_NoneD = (prove_goalw thy [np_def, raise_if_def]
- "np a' x' = None \\<longrightarrow> x' = None \\<and> a' \\<noteq> Null" (fn _ => [
+ "np a' x' = None --> x' = None \\<and> a' \\<noteq> Null" (fn _ => [
split_tac [split_if] 1,
Auto_tac ])) RS mp;
val np_None = (prove_goalw thy [np_def, raise_if_def]
- "a' \\<noteq> Null \\<longrightarrow> np a' x' = x'" (fn _ => [
+ "a' \\<noteq> Null --> np a' x' = x'" (fn _ => [
split_tac [split_if] 1,
Auto_tac ])) RS mp;
val np_Some = prove_goalw thy [np_def, raise_if_def] "np a' (Some xc) = Some xc"
--- a/src/HOL/MicroJava/J/State.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/State.thy Thu Sep 21 10:42:49 2000 +0200
@@ -15,11 +15,11 @@
constdefs
- obj_ty :: "obj \\<Rightarrow> ty"
- "obj_ty obj \\<equiv> Class (fst obj)"
+ obj_ty :: "obj => ty"
+ "obj_ty obj == Class (fst obj)"
- init_vars :: "('a \\<times> ty) list \\<Rightarrow> ('a \\<leadsto> val)"
- "init_vars \\<equiv> map_of o map (\\<lambda>(n,T). (n,default_val T))"
+ init_vars :: "('a \\<times> ty) list => ('a \\<leadsto> val)"
+ "init_vars == map_of o map (\\<lambda>(n,T). (n,default_val T))"
datatype xcpt (* exceptions *)
= NullPointer
@@ -37,9 +37,9 @@
= "xcpt option \\<times> state"
syntax
- heap :: "state \\<Rightarrow> aheap"
- locals :: "state \\<Rightarrow> locals"
- Norm :: "state \\<Rightarrow> xstate"
+ heap :: "state => aheap"
+ locals :: "state => locals"
+ Norm :: "state => xstate"
translations
"heap" => "fst"
@@ -48,19 +48,19 @@
constdefs
- new_Addr :: "aheap \\<Rightarrow> loc \\<times> xcpt option"
- "new_Addr h \\<equiv> \\<epsilon>(a,x). (h a = None \\<and> x = None) | x = Some OutOfMemory"
+ new_Addr :: "aheap => loc \\<times> xcpt option"
+ "new_Addr h == SOME (a,x). (h a = None \\<and> x = None) | x = Some OutOfMemory"
- raise_if :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option \\<Rightarrow> xcpt option"
- "raise_if c x xo \\<equiv> if c \\<and> (xo = None) then Some x else xo"
+ raise_if :: "bool => xcpt => xcpt option => xcpt option"
+ "raise_if c x xo == if c \\<and> (xo = None) then Some x else xo"
- np :: "val \\<Rightarrow> xcpt option \\<Rightarrow> xcpt option"
- "np v \\<equiv> raise_if (v = Null) NullPointer"
+ np :: "val => xcpt option => xcpt option"
+ "np v == raise_if (v = Null) NullPointer"
- c_hupd :: "aheap \\<Rightarrow> xstate \\<Rightarrow> xstate"
- "c_hupd h'\\<equiv> \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
+ c_hupd :: "aheap => xstate => xstate"
+ "c_hupd h'== \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
- cast_ok :: "'c prog \\<Rightarrow> cname \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> bool"
- "cast_ok G C h v \\<equiv> v = Null \\<or> G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq> Class C"
+ cast_ok :: "'c prog => cname => aheap => val => bool"
+ "cast_ok G C h v == v = Null \\<or> G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq> Class C"
end
--- a/src/HOL/MicroJava/J/Term.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy Thu Sep 21 10:42:49 2000 +0200
@@ -16,7 +16,7 @@
| Lit val (* literal value, also references *)
| BinOp binop expr expr (* binary operation *)
| LAcc vname (* local (incl. parameter) access *)
- | LAss vname expr (* local assign *) ("_\\<Colon>=_" [ 90,90]90)
+ | LAss vname expr (* local assign *) ("_::=_" [ 90,90]90)
| FAcc cname expr vname (* field access *) ("{_}_.._"[10,90,99 ]90)
| FAss cname expr vname
expr (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)
--- a/src/HOL/MicroJava/J/Type.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Type.thy Thu Sep 21 10:42:49 2000 +0200
@@ -31,7 +31,7 @@
syntax
NT :: " ty"
- Class :: "cname \\<Rightarrow> ty"
+ Class :: "cname => ty"
translations
"NT" == "RefT NullT"
"Class C" == "RefT (ClassT C)"
--- a/src/HOL/MicroJava/J/TypeRel.ML Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.ML Thu Sep 21 10:42:49 2000 +0200
@@ -4,11 +4,11 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-val subcls1D = prove_goalw thy [subcls1_def] "\\<And>G. G\\<turnstile>C\\<prec>C1D \\<Longrightarrow> \
+val subcls1D = prove_goalw thy [subcls1_def] "!!G. G\\<turnstile>C\\<prec>C1D ==> \
\ \\<exists>fs ms. class G C = Some (Some D,fs,ms)" (K [Auto_tac]);
val subcls1I = prove_goalw thy [subcls1_def]
-"\\<And>G. \\<lbrakk> class G C = Some (Some D,rest) \\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C1D" (K [Auto_tac]);
+"!!G. [| class G C = Some (Some D,rest) |] ==> G\\<turnstile>C\\<prec>C1D" (K [Auto_tac]);
val subcls1_def2 = prove_goalw thy [subcls1_def,is_class_def] "subcls1 G = \
\ (SIGMA C:{C. is_class G C} . {D. fst (the (class G C)) = Some D})"
@@ -32,7 +32,7 @@
auto_tac (claset() addDs lemmata, simpset())]);
-Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ \\<Longrightarrow> is_class G C";
+Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ ==> is_class G C";
by(etac trancl_trans_induct 1);
by (auto_tac (HOL_cs addSDs [subcls1D],simpset()));
qed "subcls_is_class";
@@ -81,16 +81,16 @@
qed "widen_PrimT_RefT";
AddIffs [widen_PrimT_RefT];
-val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T \\<Longrightarrow> \\<exists>t. T=RefT t"
- [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
+val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T ==> \\<exists>t. T=RefT t"
+ [prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> S=RefT R --> (\\<exists>t. T=RefT t)"];
bind_thm ("widen_RefT", widen_RefT);
-val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R \\<Longrightarrow> \\<exists>t. S=RefT t"
- [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
+val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R ==> \\<exists>t. S=RefT t"
+ [prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> T=RefT R --> (\\<exists>t. S=RefT t)"];
bind_thm ("widen_RefT2", widen_RefT2);
-val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T \\<Longrightarrow> \\<exists>D. T=Class D"
- [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> (\\<exists>D. T=Class D)"];
+val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T ==> \\<exists>D. T=Class D"
+ [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> S = Class C --> (\\<exists>D. T=Class D)"];
bind_thm ("widen_Class", widen_Class);
Goal "(G\\<turnstile>Class C\\<preceq>RefT NullT) = False";
@@ -108,7 +108,7 @@
qed "widen_Class_Class";
AddIffs [widen_Class_Class];
-Goal "G\\<turnstile>S\\<preceq>U \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
+Goal "G\\<turnstile>S\\<preceq>U ==> \\<forall>T. G\\<turnstile>U\\<preceq>T --> G\\<turnstile>S\\<preceq>T";
by( etac widen.induct 1);
by Safe_tac;
by( ALLGOALS (forward_tac [widen_Class, widen_RefT]));
--- a/src/HOL/MicroJava/J/TypeRel.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Thu Sep 21 10:42:49 2000 +0200
@@ -9,15 +9,15 @@
TypeRel = Decl +
consts
- subcls1 :: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (* subclass *)
- widen :: "'c prog \\<Rightarrow> (ty \\<times> ty ) set" (* widening *)
- cast :: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (* casting *)
+ subcls1 :: "'c prog => (cname \\<times> cname) set" (* subclass *)
+ widen :: "'c prog => (ty \\<times> ty ) set" (* widening *)
+ cast :: "'c prog => (cname \\<times> cname) set" (* casting *)
syntax
- subcls1 :: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_" [71,71,71] 70)
- subcls :: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _" [71,71,71] 70)
- widen :: "'c prog \\<Rightarrow> [ty , ty ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>_" [71,71,71] 70)
- cast :: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
+ subcls1 :: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<prec>C1_" [71,71,71] 70)
+ subcls :: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>C _" [71,71,71] 70)
+ widen :: "'c prog => [ty , ty ] => bool" ("_\\<turnstile>_\\<preceq>_" [71,71,71] 70)
+ cast :: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
translations
"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
@@ -28,23 +28,23 @@
defs
(* direct subclass, cf. 8.1.3 *)
- subcls1_def "subcls1 G \\<equiv> {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
+ subcls1_def "subcls1 G == {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
consts
- method :: "'c prog \\<times> cname \\<Rightarrow> ( sig \\<leadsto> cname \\<times> ty \\<times> 'c)"
- field :: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
- fields :: "'c prog \\<times> cname \\<Rightarrow> ((vname \\<times> cname) \\<times> ty) list"
+ method :: "'c prog \\<times> cname => ( sig \\<leadsto> cname \\<times> ty \\<times> 'c)"
+ field :: "'c prog \\<times> cname => ( vname \\<leadsto> cname \\<times> ty)"
+ fields :: "'c prog \\<times> cname => ((vname \\<times> cname) \\<times> ty) list"
constdefs (* auxiliary relations for recursive definitions below *)
subcls1_rel :: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set"
- "subcls1_rel \\<equiv> {((G,C),(G',C')). G = G' \\<and> wf ((subcls1 G)^-1) \\<and> G\\<turnstile>C'\\<prec>C1C}"
+ "subcls1_rel == {((G,C),(G',C')). G = G' \\<and> wf ((subcls1 G)^-1) \\<and> G\\<turnstile>C'\\<prec>C1C}"
(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
recdef method "subcls1_rel"
- "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty
- | Some (sc,fs,ms) \\<Rightarrow> (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow>
+ "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => empty
+ | Some (sc,fs,ms) => (case sc of None => empty | Some D =>
if is_class G D then method (G,D)
else arbitrary) \\<oplus>
map_of (map (\\<lambda>(s, m ).
@@ -53,25 +53,25 @@
(* list of fields of a class, including inherited and hidden ones *)
recdef fields "subcls1_rel"
- "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> arbitrary
- | Some (sc,fs,ms) \\<Rightarrow> map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
- (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow>
+ "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => arbitrary
+ | Some (sc,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
+ (case sc of None => [] | Some D =>
if is_class G D then fields (G,D)
else arbitrary))
else arbitrary)"
defs
- field_def "field \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
+ field_def "field == map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
i.e. sort of syntactic subtyping *)
refl "G\\<turnstile> T \\<preceq> T" (* identity conv., cf. 5.1.1 *)
- subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
+ subcls "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>Class C \\<preceq> Class D"
null "G\\<turnstile> NT \\<preceq> RefT R"
inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
(* left out casts on primitve types *)
- widen "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
- subcls "G\\<turnstile>D\\<preceq>C C \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
+ widen "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>C \\<preceq>? D"
+ subcls "G\\<turnstile>D\\<preceq>C C ==> G\\<turnstile>C \\<preceq>? D"
end
--- a/src/HOL/MicroJava/J/Value.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Value.thy Thu Sep 21 10:42:49 2000 +0200
@@ -22,9 +22,9 @@
translations "val" <= (type) "val_"
consts
- the_Bool :: "val \\<Rightarrow> bool"
- the_Intg :: "val \\<Rightarrow> int"
- the_Addr :: "val \\<Rightarrow> loc"
+ the_Bool :: "val => bool"
+ the_Intg :: "val => int"
+ the_Addr :: "val => loc"
primrec
"the_Bool (Bool b) = b"
@@ -36,8 +36,8 @@
"the_Addr (Addr a) = a"
consts
- defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *)
- default_val :: "ty \\<Rightarrow> val" (* default value for all types *)
+ defpval :: "prim_ty => val" (* default value for primitive types *)
+ default_val :: "ty => val" (* default value for all types *)
primrec
"defpval Void = Unit"
--- a/src/HOL/MicroJava/J/WellForm.ML Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.ML Thu Sep 21 10:42:49 2000 +0200
@@ -5,22 +5,22 @@
*)
val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def]
- "\\<And>X. \\<lbrakk>class G C = Some c; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wf_cdecl wf_mb G (C,c)" (K [
+ "!!X. [|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)" (K [
Asm_full_simp_tac 1,
fast_tac (set_cs addDs [get_in_set]) 1]);
val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def]
- "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> class G Object = Some (None, [], [])" (K [
+ "!!X. wf_prog wf_mb G ==> class G Object = Some (None, [], [])" (K [
safe_tac set_cs,
dtac in_set_get 1,
Auto_tac]);
Addsimps [class_Object];
val is_class_Object = prove_goalw thy [is_class_def]
- "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> is_class G Object" (K [Asm_simp_tac 1]);
+ "!!X. wf_prog wf_mb G ==> is_class G Object" (K [Asm_simp_tac 1]);
Addsimps [is_class_Object];
-Goal "\\<lbrakk>G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> D \\<noteq> C \\<and> \\<not>(D,C)\\<in>(subcls1 G)^+";
+Goal "[|G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G|] ==> D \\<noteq> C \\<and> \\<not>(D,C)\\<in>(subcls1 G)^+";
by( forward_tac [r_into_trancl] 1);
by( dtac subcls1D 1);
by( strip_tac1 1);
@@ -31,26 +31,26 @@
qed "subcls1_wfD";
val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def]
-"\\<And>X. \\<lbrakk>wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
+"!!X. [|wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object|] ==> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
pair_tac "r" 1,
asm_full_simp_tac (simpset() addsplits [option.split_asm]) 1]);
-Goal "\\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> \\<not>(D,C)\\<in>(subcls1 G)^+";
+Goal "[|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> \\<not>(D,C)\\<in>(subcls1 G)^+";
by(etac tranclE 1);
by(TRYALL(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
qed "subcls_asym";
-val subcls_irrefl = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> C \\<noteq> D" (K [
+val subcls_irrefl = prove_goal thy "!!X. [|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> C \\<noteq> D" (K [
etac trancl_trans_induct 1,
fast_tac (HOL_cs addDs [subcls1_wfD]) 1,
fast_tac (HOL_cs addDs [subcls_asym]) 1]);
val acyclic_subcls1 = prove_goalw thy [acyclic_def]
- "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> acyclic (subcls1 G)" (K [
+ "!!X. wf_prog wf_mb G ==> acyclic (subcls1 G)" (K [
strip_tac1 1,
fast_tac (HOL_cs addDs [subcls_irrefl]) 1]);
-val wf_subcls1 = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> wf ((subcls1 G)^-1)" (K [
+val wf_subcls1 = prove_goal thy "!!X. wf_prog wf_mb G ==> wf ((subcls1 G)^-1)" (K [
rtac finite_acyclic_wf 1,
stac finite_converse 1,
rtac finite_subcls1 1,
@@ -58,7 +58,7 @@
etac acyclic_subcls1 1]);
val major::prems = goal thy
- "\\<lbrakk>wf_prog wf_mb G; \\<And>C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ \\<longrightarrow> P D \\<Longrightarrow> P C\\<rbrakk> \\<Longrightarrow> P C";
+ "[|wf_prog wf_mb G; !!C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C";
by(cut_facts_tac [major RS wf_subcls1] 1);
by(dtac wf_trancl 1);
by(asm_full_simp_tac (HOL_ss addsimps [trancl_converse]) 1);
@@ -67,10 +67,10 @@
by(Auto_tac);
qed "subcls_induct";
-val prems = goal thy "\\<lbrakk>is_class G C; wf_prog wf_mb G; P Object; \
-\\\<And>C D fs ms. \\<lbrakk>C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
-\ wf_cdecl wf_mb G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D\\<rbrakk> \\<Longrightarrow> P C\
-\ \\<rbrakk> \\<Longrightarrow> P C";
+val prems = goal thy "[|is_class G C; wf_prog wf_mb G; P Object; \
+\!!C D fs ms. [|C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
+\ wf_cdecl wf_mb G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D|] ==> P C\
+\ |] ==> P C";
by( cut_facts_tac prems 1);
by( rtac impE 1);
by( atac 2);
@@ -95,18 +95,18 @@
by( etac subcls1I 1);
qed "subcls1_induct";
-Goal "\\<lbrakk>wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (Some D,fs,ms) \\<longrightarrow> is_class G D\\<rbrakk> \\<Longrightarrow> method (G,C) = \
-\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
-\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
+Goal "[|wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (Some D,fs,ms) --> is_class G D|] ==> method (G,C) = \
+\ (case class G C of None => empty | Some (sc,fs,ms) => \
+\ (case sc of None => empty | Some D => method (G,D)) \\<oplus> \
\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
by( stac (method_TC RS (wf_subcls1_rel RS (hd method.simps))) 1);
by( asm_simp_tac (simpset() addsplits[option.split]) 1);
auto();
qed "method_rec_lemma";
-Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) = \
-\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
-\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
+Goal "wf_prog wf_mb G ==> method (G,C) = \
+\ (case class G C of None => empty | Some (sc,fs,ms) => \
+\ (case sc of None => empty | Some D => method (G,D)) \\<oplus> \
\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
by(rtac method_rec_lemma 1);
by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]
@@ -119,16 +119,16 @@
by( Asm_full_simp_tac 1);
qed "method_rec";
-Goal "\\<lbrakk>wf ((subcls1 G)^-1); class G C = Some (sc,fs,ms); \\<forall>C. sc = Some C \\<longrightarrow> is_class G C\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
+Goal "[|wf ((subcls1 G)^-1); class G C = Some (sc,fs,ms); \\<forall>C. sc = Some C --> is_class G C|] ==> fields (G,C) = \
\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
-\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
+\ (case sc of None => [] | Some D => fields (G,D))";
by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
by( asm_simp_tac (simpset() addsplits[option.split]) 1);
qed "fields_rec_lemma";
-Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
+Goal "[|class G C = Some (sc,fs,ms); wf_prog wf_mb G|] ==> fields (G,C) = \
\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
-\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
+\ (case sc of None => [] | Some D => fields (G,D))";
by(rtac fields_rec_lemma 1);
by( asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
ba 1;
@@ -142,16 +142,16 @@
by( Asm_full_simp_tac 1);
qed "fields_rec";
-val method_Object = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> method (G,Object) = empty"
+val method_Object = prove_goal thy "!!X. wf_prog wf_mb G ==> method (G,Object) = empty"
(K [stac method_rec 1,Auto_tac]);
-val fields_Object = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> fields (G,Object) = []"(K [
+val fields_Object = prove_goal thy "!!X. wf_prog wf_mb G ==> fields (G,Object) = []"(K [
stac fields_rec 1,Auto_tac]);
Addsimps [method_Object, fields_Object];
val field_Object = prove_goalw thy [field_def]
- "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);
+ "!!X. wf_prog wf_mb G ==> field (G,Object) = empty" (K [Asm_simp_tac 1]);
Addsimps [field_Object];
-Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<preceq>C Object";
+Goal "[|is_class G C; wf_prog wf_mb G|] ==> G\\<turnstile>C\\<preceq>C Object";
by(etac subcls1_induct 1);
by( atac 1);
by( Fast_tac 1);
@@ -160,18 +160,18 @@
qed "subcls_C_Object";
val is_type_rTI = prove_goalw thy [wf_mhead_def]
- "\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"
+ "!!sig. wf_mhead G sig rT ==> is_type G rT"
(K [split_all_tac 1, Auto_tac]);
-Goal "\\<lbrakk>(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
-\ x \\<in> set (fields (G,C)) \\<longrightarrow> x \\<in> set (fields (G,C'))";
+Goal "[|(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G|] ==> \
+\ x \\<in> set (fields (G,C)) --> x \\<in> set (fields (G,C'))";
by(etac trancl_trans_induct 1);
by( safe_tac (HOL_cs addSDs [subcls1D]));
by(stac fields_rec 1);
by( Auto_tac);
qed_spec_mp "fields_mono";
-Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
+Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>C\\<preceq>C fd";
by( etac subcls1_induct 1);
by( atac 1);
@@ -193,7 +193,7 @@
by( Asm_full_simp_tac 1);
qed "widen_fields_defpl'";
-Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
+Goal "[|is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))|] ==> \
\ G\\<turnstile>C\\<preceq>C fd";
by( datac widen_fields_defpl' 1 1);
(*###################*)
@@ -202,7 +202,7 @@
qed "widen_fields_defpl";
-Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> unique (fields (G,C))";
+Goal "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))";
by( etac subcls1_induct 1);
by( atac 1);
by( safe_tac (HOL_cs addSDs [wf_cdecl_supD]));
@@ -226,7 +226,7 @@
qed "unique_fields";
Goal
-"\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
+"[|wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft|] ==> \
\ map_of (fields (G,C')) f = Some ft";
by( dtac rtranclD 1);
by( Auto_tac);
@@ -240,17 +240,17 @@
val cfs_fields_lemma = prove_goalw thy [field_def]
-"\\<And>X. field (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of(fields (G,C)) (fn, fd) = Some fT"
+"!!X. field (G,C) fn = Some (fd, fT) ==> map_of(fields (G,C)) (fn, fd) = Some fT"
(K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
-val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\
-\ G\\<turnstile>C'\\<preceq>C C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
+val widen_cfs_fields = prove_goal thy "!!X. [|field (G,C) fn = Some (fd, fT);\
+\ G\\<turnstile>C'\\<preceq>C C; wf_prog wf_mb G|] ==> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
bind_thm ("widen_cfs_fields",widen_cfs_fields);
-Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
-\ \\<longrightarrow> G\\<turnstile>C\\<preceq>C md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
+Goal "wf_prog wf_mb G ==> method (G,C) sig = Some (md,mh,m)\
+\ --> G\\<turnstile>C\\<preceq>C md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
by( case_tac "is_class G C" 1);
by( forw_inst_tac [("C","C")] method_rec 2);
by( asm_full_simp_tac (simpset() addsimps [is_class_def]
@@ -264,7 +264,7 @@
by( Asm_full_simp_tac 1);
by( dtac override_SomeD 1);
by( etac disjE 1);
-by( thin_tac "?P \\<longrightarrow> ?Q" 1);
+by( thin_tac "?P --> ?Q" 1);
by( Clarify_tac 2);
by( rtac rtrancl_trans 2);
by( atac 3);
@@ -277,8 +277,8 @@
by( Asm_full_simp_tac 1);
qed_spec_mp "method_wf_mdecl";
-Goal "\\<lbrakk>G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
-\ \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
+Goal "[|G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G|] ==> \
+\ \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) -->\
\ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
by( dtac rtranclD 1);
by( etac disjE 1);
@@ -312,15 +312,15 @@
Goal
- "\\<lbrakk> G\\<turnstile> C\\<preceq>C D; wf_prog wf_mb G; \
-\ method (G,D) sig = Some (md, rT, b) \\<rbrakk> \
-\ \\<Longrightarrow> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
+ "[| G\\<turnstile> C\\<preceq>C D; wf_prog wf_mb G; \
+\ method (G,D) sig = Some (md, rT, b) |] \
+\ ==> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
by(auto_tac (claset() addDs [subcls_widen_methd,method_wf_mdecl],
simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
qed "subtype_widen_methd";
-Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>D. method (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
+Goal "wf_prog wf_mb G ==> \\<forall>D. method (G,C) sig = Some(D,mh,code) --> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
by( case_tac "is_class G C" 1);
by( forw_inst_tac [("C","C")] method_rec 2);
by( asm_full_simp_tac (simpset() addsimps [is_class_def]
@@ -341,7 +341,7 @@
qed_spec_mp "method_in_md";
-Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
+Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
\ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
by( etac subcls1_induct 1);
by( atac 1);
--- a/src/HOL/MicroJava/J/WellForm.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Thu Sep 21 10:42:49 2000 +0200
@@ -20,28 +20,28 @@
constdefs
- wf_fdecl :: "'c prog \\<Rightarrow> fdecl \\<Rightarrow> bool"
-"wf_fdecl G \\<equiv> \\<lambda>(fn,ft). is_type G ft"
+ wf_fdecl :: "'c prog => fdecl => bool"
+"wf_fdecl G == \\<lambda>(fn,ft). is_type G ft"
- wf_mhead :: "'c prog \\<Rightarrow> sig \\<Rightarrow> ty \\<Rightarrow> bool"
-"wf_mhead G \\<equiv> \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
+ wf_mhead :: "'c prog => sig => ty => bool"
+"wf_mhead G == \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
- wf_mdecl :: "'c wf_mb \\<Rightarrow> 'c wf_mb"
-"wf_mdecl wf_mb G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
+ wf_mdecl :: "'c wf_mb => 'c wf_mb"
+"wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
- wf_cdecl :: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
-"wf_cdecl wf_mb G \\<equiv>
+ wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
+"wf_cdecl wf_mb G ==
\\<lambda>(C,(sc,fs,ms)).
(\\<forall>f\\<in>set fs. wf_fdecl G f ) \\<and> unique fs \\<and>
(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and> unique ms \\<and>
- (case sc of None \\<Rightarrow> C = Object
- | Some D \\<Rightarrow>
+ (case sc of None => C = Object
+ | Some D =>
is_class G D \\<and> \\<not> G\\<turnstile>D\\<preceq>C C \\<and>
(\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
- method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
+ method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
- wf_prog :: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> bool"
-"wf_prog wf_mb G \\<equiv>
+ wf_prog :: "'c wf_mb => 'c prog => bool"
+"wf_prog wf_mb G ==
let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
end
--- a/src/HOL/MicroJava/J/WellType.ML Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/WellType.ML Thu Sep 21 10:42:49 2000 +0200
@@ -5,15 +5,15 @@
*)
Goal
-"\\<lbrakk> method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>T''\\<preceq>C C\\<rbrakk>\
-\ \\<Longrightarrow> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
+"[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>T''\\<preceq>C C|]\
+\ ==> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
by( dtac subcls_widen_methd 1);
by Auto_tac;
qed "widen_methd";
Goal
-"\\<lbrakk>method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
+"[|method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G|] ==> \
\ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>T''\\<preceq>C T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
by( datac widen_methd 2 1);
@@ -25,25 +25,25 @@
qed "Call_lemma";
-Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,Object) sig = None";
+Goal "wf_prog wf_mb G ==> method (G,Object) sig = None";
by (Asm_simp_tac 1);
qed "method_Object";
Addsimps [method_Object];
Goalw [max_spec_def]
- "x \\<in> max_spec G C sig \\<Longrightarrow> x \\<in> appl_methds G C sig";
+ "x \\<in> max_spec G C sig ==> x \\<in> appl_methds G C sig";
by (Fast_tac 1);
qed"max_spec2appl_meths";
Goalw [appl_methds_def]
-"((md,rT),pTs')\\<in>appl_methds G C (mn, pTs) \\<Longrightarrow> \
+"((md,rT),pTs')\\<in>appl_methds G C (mn, pTs) ==> \
\ \\<exists>D b. md = Class D \\<and> method (G,C) (mn, pTs') = Some (D,rT,b) \
\ \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'";
by (Fast_tac 1);
qed "appl_methsD";
val is_type_typeof = prove_goal thy
- "(\\<forall>a. v \\<noteq> Addr a) \\<longrightarrow> (\\<exists>T. typeof t v = Some T \\<and> is_type G T)" (K [
+ "(\\<forall>a. v \\<noteq> Addr a) --> (\\<exists>T. typeof t v = Some T \\<and> is_type G T)" (K [
rtac val_.induct 1,
Fast_tac 5,
ALLGOALS Simp_tac]) RS mp;
--- a/src/HOL/MicroJava/J/WellType.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Thu Sep 21 10:42:49 2000 +0200
@@ -24,8 +24,8 @@
syntax
- prg :: "'c env \\<Rightarrow> 'c prog"
- localT :: "'c env \\<Rightarrow> (vname \\<leadsto> ty)"
+ prg :: "'c env => 'c prog"
+ localT :: "'c env => (vname \\<leadsto> ty)"
translations
@@ -34,29 +34,29 @@
consts
- more_spec :: "'c prog \\<Rightarrow> (ty \\<times> 'x) \\<times> ty list \\<Rightarrow>
- (ty \\<times> 'x) \\<times> ty list \\<Rightarrow> bool"
- appl_methds :: "'c prog \\<Rightarrow> cname \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
- max_spec :: "'c prog \\<Rightarrow> cname \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
+ more_spec :: "'c prog => (ty \\<times> 'x) \\<times> ty list =>
+ (ty \\<times> 'x) \\<times> ty list => bool"
+ appl_methds :: "'c prog => cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
+ max_spec :: "'c prog => cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
defs
- more_spec_def "more_spec G \\<equiv> \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
+ more_spec_def "more_spec G == \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
(* applicable methods, cf. 15.11.2.1 *)
- appl_methds_def "appl_methds G C \\<equiv> \\<lambda>(mn, pTs).
+ appl_methds_def "appl_methds G C == \\<lambda>(mn, pTs).
{((Class md,rT),pTs') |md rT mb pTs'.
method (G,C) (mn, pTs') = Some (md,rT,mb) \\<and>
list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'}"
(* maximally specific methods, cf. 15.11.2.2 *)
- max_spec_def "max_spec G C sig \\<equiv> {m. m \\<in>appl_methds G C sig \\<and>
+ max_spec_def "max_spec G C sig == {m. m \\<in>appl_methds G C sig \\<and>
(\\<forall>m'\\<in>appl_methds G C sig.
- more_spec G m' m \\<longrightarrow> m' = m)}"
+ more_spec G m' m --> m' = m)}"
consts
- typeof :: "(loc \\<Rightarrow> ty option) \\<Rightarrow> val \\<Rightarrow> ty option"
+ typeof :: "(loc => ty option) => val => ty option"
primrec
"typeof dt Unit = Some (PrimT Void)"
@@ -71,19 +71,19 @@
consts
- ty_expr :: "java_mb env \\<Rightarrow> (expr \\<times> ty ) set"
- ty_exprs:: "java_mb env \\<Rightarrow> (expr list \\<times> ty list) set"
- wt_stmt :: "java_mb env \\<Rightarrow> stmt set"
+ ty_expr :: "java_mb env => (expr \\<times> ty ) set"
+ ty_exprs:: "java_mb env => (expr list \\<times> ty list) set"
+ wt_stmt :: "java_mb env => stmt set"
syntax
-ty_expr :: "java_mb env \\<Rightarrow> [expr , ty ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Colon>_" [51,51,51]50)
-ty_exprs:: "java_mb env \\<Rightarrow> [expr list, ty list] \\<Rightarrow> bool" ("_\\<turnstile>_[\\<Colon>]_"[51,51,51]50)
-wt_stmt :: "java_mb env \\<Rightarrow> stmt \\<Rightarrow> bool" ("_\\<turnstile>_ \\<surd>" [51,51 ]50)
+ty_expr :: "java_mb env => [expr , ty ] => bool" ("_\\<turnstile>_::_" [51,51,51]50)
+ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_\\<turnstile>_[::]_"[51,51,51]50)
+wt_stmt :: "java_mb env => stmt => bool" ("_\\<turnstile>_ \\<surd>" [51,51 ]50)
translations
- "E\\<turnstile>e \\<Colon> T" == "(e,T) \\<in> ty_expr E"
- "E\\<turnstile>e[\\<Colon>]T" == "(e,T) \\<in> ty_exprs E"
+ "E\\<turnstile>e :: T" == "(e,T) \\<in> ty_expr E"
+ "E\\<turnstile>e[::]T" == "(e,T) \\<in> ty_exprs E"
"E\\<turnstile>c \\<surd>" == "c \\<in> wt_stmt E"
inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intrs
@@ -91,98 +91,98 @@
(* well-typed expressions *)
(* cf. 15.8 *)
- NewC "\\<lbrakk>is_class (prg E) C\\<rbrakk> \\<Longrightarrow>
- E\\<turnstile>NewC C\\<Colon>Class C"
+ NewC "[|is_class (prg E) C|] ==>
+ E\\<turnstile>NewC C::Class C"
(* cf. 15.15 *)
- Cast "\\<lbrakk>E\\<turnstile>e\\<Colon>Class C;
- prg E\\<turnstile>C\\<preceq>? D\\<rbrakk> \\<Longrightarrow>
- E\\<turnstile>Cast D e\\<Colon>Class D"
+ Cast "[|E\\<turnstile>e::Class C;
+ prg E\\<turnstile>C\\<preceq>? D|] ==>
+ E\\<turnstile>Cast D e::Class D"
(* cf. 15.7.1 *)
- Lit "\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow>
- E\\<turnstile>Lit x\\<Colon>T"
+ Lit "[|typeof (\\<lambda>v. None) x = Some T|] ==>
+ E\\<turnstile>Lit x::T"
(* cf. 15.13.1 *)
- LAcc "\\<lbrakk>localT E v = Some T; is_type (prg E) T\\<rbrakk> \\<Longrightarrow>
- E\\<turnstile>LAcc v\\<Colon>T"
+ LAcc "[|localT E v = Some T; is_type (prg E) T|] ==>
+ E\\<turnstile>LAcc v::T"
- BinOp "\\<lbrakk>E\\<turnstile>e1\\<Colon>T;
- E\\<turnstile>e2\\<Colon>T;
+ BinOp "[|E\\<turnstile>e1::T;
+ E\\<turnstile>e2::T;
if bop = Eq then T' = PrimT Boolean
- else T' = T \\<and> T = PrimT Integer\\<rbrakk> \\<Longrightarrow>
- E\\<turnstile>BinOp bop e1 e2\\<Colon>T'"
+ else T' = T \\<and> T = PrimT Integer|] ==>
+ E\\<turnstile>BinOp bop e1 e2::T'"
(* cf. 15.25, 15.25.1 *)
- LAss "\\<lbrakk>E\\<turnstile>LAcc v\\<Colon>T;
- E\\<turnstile>e\\<Colon>T';
- prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
- E\\<turnstile>v\\<Colon>=e\\<Colon>T'"
+ LAss "[|E\\<turnstile>LAcc v::T;
+ E\\<turnstile>e::T';
+ prg E\\<turnstile>T'\\<preceq>T|] ==>
+ E\\<turnstile>v::=e::T'"
(* cf. 15.10.1 *)
- FAcc "\\<lbrakk>E\\<turnstile>a\\<Colon>Class C;
- field (prg E,C) fn = Some (fd,fT)\\<rbrakk> \\<Longrightarrow>
- E\\<turnstile>{fd}a..fn\\<Colon>fT"
+ FAcc "[|E\\<turnstile>a::Class C;
+ field (prg E,C) fn = Some (fd,fT)|] ==>
+ E\\<turnstile>{fd}a..fn::fT"
(* cf. 15.25, 15.25.1 *)
- FAss "\\<lbrakk>E\\<turnstile>{fd}a..fn\\<Colon>T;
- E\\<turnstile>v \\<Colon>T';
- prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
- E\\<turnstile>{fd}a..fn:=v\\<Colon>T'"
+ FAss "[|E\\<turnstile>{fd}a..fn::T;
+ E\\<turnstile>v ::T';
+ prg E\\<turnstile>T'\\<preceq>T|] ==>
+ E\\<turnstile>{fd}a..fn:=v::T'"
(* cf. 15.11.1, 15.11.2, 15.11.3 *)
- Call "\\<lbrakk>E\\<turnstile>a\\<Colon>Class C;
- E\\<turnstile>ps[\\<Colon>]pTs;
- max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}\\<rbrakk> \\<Longrightarrow>
- E\\<turnstile>a..mn({pTs'}ps)\\<Colon>rT"
+ Call "[|E\\<turnstile>a::Class C;
+ E\\<turnstile>ps[::]pTs;
+ max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}|] ==>
+ E\\<turnstile>a..mn({pTs'}ps)::rT"
(* well-typed expression lists *)
(* cf. 15.11.??? *)
- Nil "E\\<turnstile>[][\\<Colon>][]"
+ Nil "E\\<turnstile>[][::][]"
(* cf. 15.11.??? *)
- Cons "\\<lbrakk>E\\<turnstile>e\\<Colon>T;
- E\\<turnstile>es[\\<Colon>]Ts\\<rbrakk> \\<Longrightarrow>
- E\\<turnstile>e#es[\\<Colon>]T#Ts"
+ Cons "[|E\\<turnstile>e::T;
+ E\\<turnstile>es[::]Ts|] ==>
+ E\\<turnstile>e#es[::]T#Ts"
(* well-typed statements *)
Skip "E\\<turnstile>Skip\\<surd>"
- Expr "\\<lbrakk>E\\<turnstile>e\\<Colon>T\\<rbrakk> \\<Longrightarrow>
+ Expr "[|E\\<turnstile>e::T|] ==>
E\\<turnstile>Expr e\\<surd>"
- Comp "\\<lbrakk>E\\<turnstile>s1\\<surd>;
- E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
+ Comp "[|E\\<turnstile>s1\\<surd>;
+ E\\<turnstile>s2\\<surd>|] ==>
E\\<turnstile>s1;; s2\\<surd>"
(* cf. 14.8 *)
- Cond "\\<lbrakk>E\\<turnstile>e\\<Colon>PrimT Boolean;
+ Cond "[|E\\<turnstile>e::PrimT Boolean;
E\\<turnstile>s1\\<surd>;
- E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
+ E\\<turnstile>s2\\<surd>|] ==>
E\\<turnstile>If(e) s1 Else s2\\<surd>"
(* cf. 14.10 *)
- Loop "\\<lbrakk>E\\<turnstile>e\\<Colon>PrimT Boolean;
- E\\<turnstile>s\\<surd>\\<rbrakk> \\<Longrightarrow>
+ Loop "[|E\\<turnstile>e::PrimT Boolean;
+ E\\<turnstile>s\\<surd>|] ==>
E\\<turnstile>While(e) s\\<surd>"
constdefs
wf_java_mdecl :: java_mb prog => cname => java_mb mdecl => bool
-"wf_java_mdecl G C \\<equiv> \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
+"wf_java_mdecl G C == \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
length pTs = length pns \\<and>
nodups pns \\<and>
unique lvars \\<and>
(\\<forall>pn\\<in>set pns. map_of lvars pn = None) \\<and>
(\\<forall>(vn,T)\\<in>set lvars. is_type G T) &
(let E = (G,map_of lvars(pns[\\<mapsto>]pTs)(This\\<mapsto>Class C)) in
- E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res\\<Colon>T \\<and> G\\<turnstile>T\\<preceq>rT))"
+ E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res::T \\<and> G\\<turnstile>T\\<preceq>rT))"
wf_java_prog :: java_mb prog => bool
-"wf_java_prog G \\<equiv> wf_prog wf_java_mdecl G"
+"wf_java_prog G == wf_prog wf_java_mdecl G"
end
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Thu Sep 21 10:42:49 2000 +0200
@@ -9,7 +9,7 @@
JVMExec = JVMExecInstr +
consts
- exec :: "jvm_prog \\<times> jvm_state \\<Rightarrow> jvm_state option"
+ exec :: "jvm_prog \\<times> jvm_state => jvm_state option"
(** exec is not recursive. recdef is just used for pattern matching **)
recdef exec "{}"
@@ -25,7 +25,7 @@
constdefs
- exec_all :: "[jvm_prog,jvm_state,jvm_state] \\<Rightarrow> bool" ("_ \\<turnstile> _ -jvm\\<rightarrow> _" [61,61,61]60)
- "G \\<turnstile> s -jvm\\<rightarrow> t \\<equiv> (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"
+ exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" ("_ \\<turnstile> _ -jvm-> _" [61,61,61]60)
+ "G \\<turnstile> s -jvm-> t == (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"
end
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Thu Sep 21 10:42:49 2000 +0200
@@ -9,7 +9,7 @@
JVMExecInstr = JVMInstructions + JVMState +
consts
-exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] \\<Rightarrow> jvm_state"
+exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state"
primrec
"exec_instr (Load idx) G hp stk vars Cl sig pc frs =
(None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"
--- a/src/HOL/MicroJava/JVM/JVMState.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMState.thy Thu Sep 21 10:42:49 2000 +0200
@@ -32,8 +32,8 @@
(** exceptions **)
constdefs
- raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option"
-"raise_xcpt c x \\<equiv> (if c then Some x else None)"
+ raise_xcpt :: "bool => xcpt => xcpt option"
+"raise_xcpt c x == (if c then Some x else None)"
(** runtime state **)
@@ -45,6 +45,6 @@
(** dynamic method lookup **)
constdefs
- dyn_class :: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname"
-"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
+ dyn_class :: "'code prog \\<times> sig \\<times> cname => cname"
+"dyn_class == \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
end
--- a/src/HOL/MicroJava/JVM/Store.ML Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Store.ML Thu Sep 21 10:42:49 2000 +0200
@@ -5,6 +5,6 @@
*)
Goalw [newref_def]
- "hp x = None \\<longrightarrow> hp (newref hp) = None";
+ "hp x = None --> hp (newref hp) = None";
by (fast_tac (claset() addIs [someI2_ex] addss (simpset())) 1);
qed_spec_mp "newref_None";
--- a/src/HOL/MicroJava/JVM/Store.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Store.thy Thu Sep 21 10:42:49 2000 +0200
@@ -12,7 +12,7 @@
Store = Conform +
constdefs
- newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"
- "newref s \\<equiv> \\<epsilon>v. s v = None"
+ newref :: "('a \\<leadsto> 'b) => 'a"
+ "newref s == SOME v. s v = None"
end