--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/BVSpec.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,31 @@
+(* Title: HOL/MicroJava/BV/BVSpec.ML
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+Addsimps [wt_MR_def];
+
+Goalw [wt_jvm_prog_def] "wt_jvm_prog G phi \\<Longrightarrow> (\\<exists>wt. wf_prog wt G)";
+by(Blast_tac 1);
+qed "wt_jvm_progD";
+
+
+Goalw [wt_jvm_prog_def]
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (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";
+by(forward_tac [rotate_prems 2 cmethd_wf_mdecl] 1);
+ by (Asm_full_simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1);
+qed "wt_jvm_prog_impl_wt_instr";
+
+Goalw [wt_jvm_prog_def]
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (G,C) sig = Some (C,rT,maxl,ins) \\<rbrakk> \\<Longrightarrow> \
+\ 0 < (length ins) \\<and> wt_start G C (snd sig) maxl (phi C sig)";
+by(forward_tac [rotate_prems 2 cmethd_wf_mdecl] 1);
+ by (Asm_full_simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1);
+qed "wt_jvm_prog_impl_wt_start";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,201 @@
+(* Title: HOL/MicroJava/BV/BVSpec.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+
+Specification of bytecode verifier
+*)
+
+BVSpec = Convert +
+
+types
+ method_type = "state_type list"
+ class_type = "sig \\<Rightarrow> method_type"
+ prog_type = "cname \\<Rightarrow> class_type"
+
+consts
+ wt_LS :: "[load_and_store,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
+primrec
+"wt_LS (Load idx) G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ idx < length LT \\<and>
+ (\\<exists>ts. (LT ! idx) = Some ts \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (ts # ST , LT)))"
+
+"wt_LS (Store idx) G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ idx < length LT \\<and>
+ (\\<exists>ts ST'. ST = ts # ST' \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT[idx:=Some ts])))"
+
+"wt_LS (Bipush i) G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= ((PrimT Integer) # ST , LT))"
+
+"wt_LS (Aconst_null) G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (NT # ST , LT))"
+
+consts
+ wt_MO :: "[manipulate_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
+primrec
+"wt_MO (Getfield F C) G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ is_class G C \\<and>
+ (\\<exists>T oT ST'. cfield (G,C) F = Some(C,T) \\<and>
+ ST = oT # ST' \\<and>
+ G \\<turnstile> oT \\<preceq> (Class C) \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (T # ST' , LT)))"
+
+"wt_MO (Putfield F C) G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ is_class G C \\<and>
+ (\\<exists>T vT oT ST'.
+ cfield (G,C) F = Some(C,T) \\<and>
+ ST = vT # oT # ST' \\<and>
+ G \\<turnstile> oT \\<preceq> (Class C) \\<and>
+ G \\<turnstile> vT \\<preceq> T \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT)))"
+
+
+consts
+ wt_CO :: "[create_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
+primrec
+"wt_CO (New C) G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ is_class G C \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= ((Class C) # ST , LT))"
+
+consts
+ wt_CH :: "[check_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
+primrec
+"wt_CH (Checkcast C) G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ is_class G C \\<and>
+ (\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (Class C # ST' , LT)))"
+
+consts
+ wt_OS :: "[op_stack,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
+primrec
+"wt_OS Pop G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ \\<exists>ts ST'. pc+1 < max_pc \\<and>
+ ST = ts # ST' \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT))"
+
+"wt_OS Dup G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ (\\<exists>ts ST'. ST = ts # ST' \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (ts # ts # ST' , LT)))"
+
+"wt_OS Dup_x1 G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ (\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts1 # ST' , LT)))"
+
+"wt_OS Dup_x2 G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ (\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts3 # ts1 # ST' , LT)))"
+
+"wt_OS Swap G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (ts # ts' # ST' , LT)))"
+
+consts
+ wt_BR :: "[branch,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
+primrec
+"wt_BR (Ifcmpeq branch) G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and>
+ (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and> ts = ts' \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT) \\<and>
+ G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST' , LT)))"
+"wt_BR (Goto branch) G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ (nat(int pc+branch)) < max_pc \\<and>
+ G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST , LT))"
+
+consts
+ wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
+primrec
+"wt_MI (Invokevirtual mn fpTs) G phi max_pc pc =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ (\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\<and>
+ length apTs = length fpTs \\<and>
+ (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
+ (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
+ G \\<turnstile> phi ! (pc+1) >>>= (rT # ST' , LT))))"
+
+constdefs
+ wt_MR :: "[jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
+"wt_MR G rT phi pc \\<equiv>
+ (let (ST,LT) = phi ! pc
+ in
+ (\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))"
+
+
+constdefs
+ wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\<Rightarrow> bool"
+ "wt_instr instr G rT phi max_pc pc \\<equiv>
+ case instr of
+ LS ins \\<Rightarrow> wt_LS ins G phi max_pc pc
+ | CO ins \\<Rightarrow> wt_CO ins G phi max_pc pc
+ | MO ins \\<Rightarrow> wt_MO ins G phi max_pc pc
+ | CH ins \\<Rightarrow> wt_CH ins G phi max_pc pc
+ | MI ins \\<Rightarrow> wt_MI ins G phi max_pc pc
+ | MR \\<Rightarrow> wt_MR G rT phi pc
+ | OS ins \\<Rightarrow> wt_OS ins G phi max_pc pc
+ | BR ins \\<Rightarrow> wt_BR ins G phi max_pc pc"
+
+
+constdefs
+ wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool"
+ "wt_start G C pTs mxl phi \\<equiv>
+ G \\<turnstile> phi!0 >>>= ([],(Some(Class C))#((map Some pTs))@(replicate mxl None))"
+
+
+ wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool"
+ "wt_method G cn pTs rT mxl ins phi \\<equiv>
+ let max_pc = length ins
+ in
+ 0 < max_pc \\<and> wt_start G cn pTs mxl phi \\<and>
+ (\\<forall>pc. pc<max_pc \\<longrightarrow> 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>
+ wf_prog (\\<lambda>G C (sig,rT,maxl,b).
+ wt_method G C (snd sig) rT maxl b (phi C sig)) G"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,625 @@
+(* Title: HOL/MicroJava/BV/BVSpecTypeSafe.ML
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+val defs1 = exec.rules@[split_def,sup_state_def,correct_state_def,
+ correct_frame_def,wt_instr_def];
+
+Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
+\ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
+by (Asm_full_simp_tac 1);
+by(blast_tac (claset() addIs [wt_jvm_prog_impl_wt_instr]) 1);
+qed "wt_jvm_prog_impl_wt_instr_cor";
+
+
+Delsimps [split_paired_All];
+
+
+(******* LS *******)
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = LS(Load idx); \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup,
+ approx_loc_imp_approx_loc_sup]
+ addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
+qed "Load_correct";
+
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = LS(Store idx); \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
+ addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RSN(2, approx_loc_imp_approx_loc_sup)]
+ addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1)) 1);
+qed "Store_correct";
+
+Goalw [conf_def] "G,h \\<turnstile> Intg i \\<Colon>\\<preceq> PrimT Integer";
+by(Simp_tac 1);
+qed "conf_Intg_Integer";
+AddIffs [conf_Intg_Integer];
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = LS(Bipush i); \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
+ addss (simpset() addsimps [approx_val_def,sup_PTS_eq,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
+qed "Bipush_correct";
+
+Goal "G \\<turnstile> T' \\<preceq> T \\<Longrightarrow> T' = NT \\<longrightarrow> (T=NT | (\\<exists>C. T = Class C))";
+be widen.induct 1;
+by(Auto_tac);
+by(rename_tac "R" 1);
+by(exhaust_tac "R" 1);
+by(Auto_tac);
+val lemma = result();
+
+Goal "G \\<turnstile> NT \\<preceq> T = (T=NT | (\\<exists>C. T = Class C))";
+by(force_tac (claset() addIs widen.intrs addDs [lemma],simpset()) 1);
+qed "NT_subtype_conv";
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = LS Aconst_null; \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
+ addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
+qed "Aconst_null_correct";
+
+
+Goal
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = LS ls_com; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
+ ba 1;
+ ba 1;
+by(rewtac wt_jvm_prog_def);
+by (exhaust_tac "ls_com" 1);
+by (ALLGOALS (fast_tac (claset() addIs [Load_correct,Store_correct,Bipush_correct,Aconst_null_correct])));
+qed "LS_correct";
+
+
+(**** CH ****)
+
+Goalw [cast_ok_def]
+ "\\<lbrakk> wf_prog ok G; G,h\\<turnstile>v\\<Colon>\\<preceq>RefT rt; cast_ok G (Class C) h v ; G\\<turnstile>(Class C)\\<preceq>T'; is_class G C \\<rbrakk> \
+\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
+be disjE 1;
+ by (Clarify_tac 1);
+by (forward_tac [widen_Class] 1);
+by (Clarify_tac 1);
+be disjE 1;
+ by (asm_full_simp_tac (simpset() addsimps [widen.null]) 1);
+by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [obj_ty_def]) 1);
+by (exhaust_tac "v" 1);
+by (ALLGOALS (fast_tac (claset() addIs [widen_trans] addss (simpset() addsimps [widen.null]))));
+qed "Cast_conf2";
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = CH (Checkcast D); \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,
+ xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
+by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
+ addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup,Cast_conf2]
+ addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,approx_val_def])) 1);
+qed "Checkcast_correct";
+
+
+Goal
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = CH ch_com; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
+ ba 1;
+ ba 1;
+by(rewtac wt_jvm_prog_def);
+by (exhaust_tac "ch_com" 1);
+by (ALLGOALS (fast_tac (claset() addIs [Checkcast_correct])));
+qed "CH_correct";
+
+
+(******* MO *******)
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = MO (Getfield F D); \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
+by (Clarify_tac 1);
+bd approx_stk_Cons_lemma 1;
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
+
+by (forward_tac [conf_widen] 1);
+ ba 1;
+ ba 1;
+bd conf_RefTD 1;
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+
+(* approx_stk *)
+br conjI 1;
+by (asm_full_simp_tac (simpset() addsimps [approx_stk_Cons]) 1);
+br conjI 1;
+by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup]) 1);
+by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
+bd widen_cfs_fields 1;
+ ba 1;
+ ba 1;
+by (fast_tac (claset() addIs [conf_widen] addss (simpset() addsimps [hconf_def,oconf_def,lconf_def])) 1);
+
+(* approx_loc *)
+by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup]) 1);
+qed "Getfield_correct";
+
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = MO (Putfield F D); \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
+by (Clarify_tac 1);
+bd approx_stk_Cons_lemma 1;
+by (Clarify_tac 1);
+bd approx_stk_Cons_lemma 1;
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
+
+by (forward_tac [conf_widen] 1);
+ ba 2;
+ ba 1;
+by (fast_tac (claset() addDs [conf_RefTD,widen_cfs_fields]
+ addIs [sup_heap_update_value,approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup),
+ approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup),
+ hconf_imp_hconf_field_update,
+ correct_frames_imp_correct_frames_field_update,conf_widen] addss (simpset())) 1);
+qed "Putfield_correct";
+
+
+Goal
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = MO mo_com; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
+ ba 1;
+ ba 1;
+by(rewtac wt_jvm_prog_def);
+by (exhaust_tac "mo_com" 1);
+by (ALLGOALS (fast_tac (claset() addIs [Getfield_correct,Putfield_correct])));
+qed "MO_correct";
+
+
+(****** CO ******)
+
+Goal "(\\<forall>x y. P(x,y)) = (\\<forall>z. P z)";
+by(Fast_tac 1);
+qed "collapse_paired_All";
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
+\ ins!pc = CO(New cl_idx); \
+\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (fast_tac (claset() addSDs [collapse_paired_All RS iffD1]addIs [sup_heap_newref,
+ approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup),
+ approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup),
+ hconf_imp_hconf_newref,correct_frames_imp_correct_frames_newref,
+ rewrite_rule [split_def] correct_init_obj]
+ addss (simpset() addsimps [NT_subtype_conv,approx_stk_Cons,approx_val_def,conf_def,
+ fun_upd_apply,sup_loc_Cons,map_eq_Cons,is_class_def,xcpt_update_def,raise_xcpt_def,init_vars_def]@defs1
+ addsplits [option.split])) 1);
+qed "New_correct";
+
+Goal
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = CO co_com; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
+ ba 1;
+ ba 1;
+by(rewtac wt_jvm_prog_def);
+by (exhaust_tac "co_com" 1);
+by (ALLGOALS (fast_tac (claset() addIs [New_correct])));
+qed "CO_correct";
+
+
+(****** MI ******)
+
+Goal
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins ! pc = MI(Invokevirtual mn pTs); \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by(forward_tac [wt_jvm_progD] 1);
+by(etac exE 1);
+by (asm_full_simp_tac (simpset()addsimps[xcpt_update_def,raise_xcpt_def]@defs1
+ addsplits [option.split]) 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
+bd approx_stk_append_lemma 1;
+by (Clarify_tac 1);
+bd approx_stk_Cons_lemma 1;
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
+bd conf_RefTD 1;
+by (Clarify_tac 1);
+by(rename_tac "oloc oT ofs T'" 1);
+by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
+bd subtype_widen_methd 1;
+ ba 1;
+ ba 1;
+be exE 1;
+by(rename_tac "oT'" 1);
+by (Clarify_tac 1);
+by(subgoal_tac "G \\<turnstile> Class oT \\<preceq> Class oT'" 1);
+ by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 cmethd_wf_mdecl)) 2);
+ ba 2;
+ by(Blast_tac 2);
+by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
+by(forward_tac [cmethd_in_md] 1);
+ ba 1;
+ back();
+ back();
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
+by (forward_tac [wt_jvm_prog_impl_wt_start] 1);
+ ba 1;
+ back();
+by (asm_full_simp_tac (simpset() addsimps [wt_start_def,sup_state_def]) 1);
+by (Clarify_tac 1);
+
+(** approx_stk **)
+br conjI 1;
+ by (asm_full_simp_tac (simpset() addsimps [sup_loc_Nil,approx_stk_Nil]) 1);
+
+
+(** approx_loc **)
+br conjI 1;
+ br approx_loc_imp_approx_loc_sup 1;
+ ba 1;
+ by (Fast_tac 2);
+ by (asm_full_simp_tac (simpset() addsimps [split_def,approx_loc_Cons,approx_val_def,approx_loc_append]) 1);
+ br conjI 1;
+ br conf_widen 1;
+ ba 1;
+ by (Fast_tac 2);
+ by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
+ br conjI 1;
+ by (fast_tac (claset() addIs [approx_stk_rev RS iffD2 RSN(4,assConv_approx_stk_imp_approx_loc)]
+ addss (simpset() addsimps [split_def,approx_loc_Cons,approx_val_def])) 1);
+ by (asm_simp_tac (simpset() addsimps [split_def,approx_loc_def,zip_replicate,approx_val_None,set_replicate_conv_if]) 1);
+
+br conjI 1;
+ by (asm_simp_tac (simpset() addsimps [min_def]) 1);
+br exI 1;
+br exI 1;
+br conjI 1;
+ by(Blast_tac 1);
+by (fast_tac (claset()
+ addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
+ addss (simpset()addsimps [map_eq_Cons,sup_loc_Cons])) 1);
+qed "Invokevirtual_correct";
+
+Goal
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = MI mi_com; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
+ ba 1;
+ ba 1;
+by (exhaust_tac "mi_com" 1);
+by (ALLGOALS (fast_tac (claset() addIs [Invokevirtual_correct])));
+qed "MI_correct";
+
+(****** MR ******)
+
+Goal
+ "\\<forall>zs. (xs@ys = zs) = (xs = take (length xs) zs \\<and> ys = drop (length xs) zs)";
+by(induct_tac "xs" 1);
+by(Simp_tac 1);
+by(Asm_full_simp_tac 1);
+by(Clarify_tac 1);
+by(exhaust_tac "zs" 1);
+by(Auto_tac);
+qed_spec_mp "append_eq_conv_conj";
+
+
+
+Delsimps [map_append];
+Goal
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins ! pc = MR; \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
+by (exhaust_tac "frs" 1);
+ by (asm_full_simp_tac (simpset() addsimps defs1) 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1) 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
+by (forward_tac [wt_jvm_prog_impl_wt_instr] 1);
+ by(EVERY1[atac, etac Suc_lessD]);
+by(rewtac wt_jvm_prog_def);
+by (fast_tac (claset()
+ addDs [approx_stk_Cons_lemma,subcls_widen_methd]
+ addEs [rotate_prems 1 widen_trans]
+ addIs [conf_widen]
+ addss (simpset()
+ addsimps [approx_val_def,append_eq_conv_conj,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
+qed "Return_correct";
+Addsimps [map_append];
+
+Goal
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = MR; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
+ ba 1;
+ ba 1;
+by (ALLGOALS (fast_tac (claset() addIs [Return_correct])));
+qed "MR_correct";
+
+(****** BR ******)
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins ! pc = BR(Goto branch); \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup]
+ addss (simpset() addsimps defs1)) 1);
+qed "Goto_correct";
+
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = BR(Ifcmpeq branch); \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
+ addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
+qed "Ifiacmpeq_correct";
+
+
+Goal
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = BR br_com; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
+ ba 1;
+ ba 1;
+by(rewtac wt_jvm_prog_def);
+by (exhaust_tac "br_com" 1);
+by (ALLGOALS (fast_tac (claset() addIs [Goto_correct,Ifiacmpeq_correct])));
+qed "BR_correct";
+
+
+(****** OS ******)
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins ! pc = OS Pop; \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
+ addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
+qed "Pop_correct";
+
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins ! pc = OS Dup; \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
+ addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
+ addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
+qed "Dup_correct";
+
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins ! pc = OS Dup_x1; \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
+ addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
+ addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
+qed "Dup_x1_correct";
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins ! pc = OS Dup_x2; \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
+ addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
+ addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
+qed "Dup_x2_correct";
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins ! pc = OS Swap; \
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
+ addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
+ addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
+qed "Swap_correct";
+
+Goal
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ ins!pc = OS os_com; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
+\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
+ ba 1;
+ ba 1;
+by(rewtac wt_jvm_prog_def);
+by (exhaust_tac "os_com" 1);
+by (ALLGOALS (fast_tac (claset() addIs [Pop_correct,Dup_correct,Dup_x1_correct,Dup_x2_correct,Swap_correct])));
+qed "OS_correct";
+
+(** Main **)
+
+Goalw [correct_state_def,Let_def]
+ "correct_state G phi (None,hp,(stk,loc,C,sig,pc)#fs) \
+\ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) sig = Some(C,meth)";
+by(Asm_full_simp_tac 1);
+by(Blast_tac 1);
+qed "correct_state_impl_Some_cmethd";
+
+Goal
+"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; correct_state G phi state\\<rbrakk> \
+\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> correct_state G phi state'";
+by(split_all_tac 1);
+by(rename_tac "xp hp frs" 1);
+by (exhaust_tac "xp" 1);
+ by (exhaust_tac "frs" 1);
+ by (asm_full_simp_tac (simpset() addsimps exec.rules) 1);
+ by(split_all_tac 1);
+ by(hyp_subst_tac 1);
+ by(forward_tac [correct_state_impl_Some_cmethd] 1);
+ by (force_tac (claset() addIs [LS_correct,CO_correct,MO_correct,CH_correct,MI_correct,MR_correct,OS_correct,
+ BR_correct], simpset() addsplits [instr.split,instr.split_asm] addsimps exec.rules@[split_def]) 1);
+by (exhaust_tac "frs" 1);
+ by (asm_full_simp_tac (simpset() addsimps exec.rules) 1);
+by (force_tac (claset(), simpset() addsimps exec.rules@[correct_state_def]) 1);
+qed_spec_mp "BV_correct_1";
+
+
+(*******)
+Goal
+"xp=None \\<longrightarrow> frs\\<noteq>[] \\<longrightarrow> (\\<exists>xp' hp' frs'. exec (G,xp,hp,frs) = Some (xp',hp',frs'))";
+by (fast_tac (claset() addIs [BV_correct_1]
+ addss (simpset() addsplits [instr.split] addsimps [neq_Nil_conv]@defs1)) 1);
+qed_spec_mp "exec_lemma";
+
+Goal
+"\\<lbrakk> wt_jvm_prog G phi; \
+\ correct_state G phi (xp,hp,frs); xp=None; frs\\<noteq>[] \\<rbrakk> \
+\ \\<Longrightarrow> \\<exists>xp' hp' frs'. exec (G,xp,hp,frs) = Some (xp',hp',frs') \\<and> correct_state G phi (xp',hp',frs')";
+by (dres_inst_tac [("G","G"),("hp","hp")] exec_lemma 1);
+ba 1;
+by (fast_tac (claset() addIs [BV_correct_1]) 1);
+qed "L1";
+(*******)
+
+Goalw [exec_all_def]
+"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s -jvm\\<rightarrow> t \\<rbrakk> \
+\ \\<Longrightarrow> correct_state G phi s \\<longrightarrow> correct_state G phi t";
+be rtrancl_induct 1;
+ by (Simp_tac 1);
+by (fast_tac (claset() addIs [BV_correct_1] addss (simpset())) 1);
+qed_spec_mp "BV_correct";
+
+
+Goal
+"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s0 -jvm\\<rightarrow> (None,hp,(stk,loc,cn,ml,pc)#frs); correct_state G phi s0 \\<rbrakk> \
+\ \\<Longrightarrow> approx_stk G hp stk (fst (((phi cn) ml) ! pc)) \\<and> approx_loc G hp loc (snd (((phi cn) ml) ! pc)) ";
+bd BV_correct 1;
+ba 1;
+ba 1;
+by (asm_full_simp_tac (simpset() addsimps [correct_state_def,correct_frame_def,split_def]
+ addsplits [option.split_asm]) 1);
+qed_spec_mp "BV_correct_initial";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,10 @@
+(* Title: HOL/MicroJava/BV/BVSpecTypeSafe.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+
+Proof that the specification of the bytecode verifier only admits type safe
+programs.
+*)
+
+BVSpecTypeSafe = Correct
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Convert.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,41 @@
+(* Title: HOL/MicroJava/BV/Convert.ML
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+val widen_PrimT_conv1 =
+ prove_typerel "(G \\<turnstile> PrimT x \\<preceq> T) = (T = PrimT x)"
+ [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = PrimT x"];
+Addsimps [widen_PrimT_conv1];
+
+Goalw [sup_ty_opt_def] "(G \\<turnstile> any >= None) = (any = None)";
+by(simp_tac (simpset() addsplits [option.split]) 1);
+qed "anyConvNone";
+Addsimps [anyConvNone];
+
+Goalw [sup_ty_opt_def] "(G \\<turnstile> Some ty >= Some ty') = (G \\<turnstile> ty' \\<preceq> ty)";
+by(Simp_tac 1);
+qed "SomeanyConvSome";
+Addsimps [SomeanyConvSome];
+
+Goal
+"(G \\<turnstile> X >= Some(PrimT Integer)) = (X=None \\<or> (X=Some(PrimT Integer)))";
+by (simp_tac (simpset() setloop (split_tac [ty.split,option.split]) addsimps [sup_ty_opt_def]) 1);
+qed "sup_PTS_eq";
+
+
+
+Goal
+"CFS \\<turnstile> XT >>= [] = (XT=[])";
+by (case_tac "XT=[]" 1);
+by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1);
+by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1);
+qed "sup_loc_Nil";
+
+Goal
+"CFS \\<turnstile> XT >>= (Y#YT) = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> X>=Y \\<and> CFS \\<turnstile> XT'>>=YT)";
+by (case_tac "XT=[]" 1);
+by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1);
+by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1);
+qed "sup_loc_Cons";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Convert.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,33 @@
+(* Title: HOL/MicroJava/BV/Convert.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+
+The supertype relation lifted to type options, type lists and state types.
+*)
+
+Convert = JVMExec +
+
+types
+ locvars_type = ty option list
+ opstack_type = ty list
+ state_type = "opstack_type \\<times> locvars_type"
+
+constdefs
+
+ sup_ty_opt :: "['code prog,ty option,ty option] \\<Rightarrow> bool" ("_ \\<turnstile>_ >= _")
+ "G \\<turnstile> a >= a' \\<equiv>
+ case a of
+ None \\<Rightarrow> True
+ | Some t \\<Rightarrow> case a' of
+ None \\<Rightarrow> False
+ | Some t' \\<Rightarrow> G \\<turnstile> t' \\<preceq> t"
+
+ sup_loc :: "['code prog,locvars_type,locvars_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ >>= _" [71,71] 70)
+ "G \\<turnstile> LT >>= LT' \\<equiv> (length LT=length LT') \\<and> (\\<forall>(t,t')\\<in>set (zip LT LT'). G \\<turnstile> t >= t')"
+
+
+ sup_state :: "['code prog,state_type,state_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ >>>= _" [71,71] 70)
+ "G \\<turnstile> s >>>= s' \\<equiv> G \\<turnstile> map Some (fst s) >>= map Some (fst s') \\<and> G \\<turnstile> snd s >>= snd s'"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Correct.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,281 @@
+(* Title: HOL/MicroJava/BV/Correct.ML
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+(** sup_heap **)
+
+Goalw [hext_def]
+ "hp x = None \\<longrightarrow> hp \\<le>| (hp((newref hp) \\<mapsto> obj))";
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (Clarify_tac 1);
+bd newref_None 1;
+back();
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+qed_spec_mp "sup_heap_newref";
+
+
+Goalw [hext_def]
+"hp a = Some (cn,od') \\<longrightarrow> hp \\<le>| (hp(a \\<mapsto> (cn,od)))";
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+qed_spec_mp "sup_heap_update_value";
+
+
+(** approx_val **)
+
+Goalw [approx_val_def]
+"approx_val G hp x None";
+by (Asm_full_simp_tac 1);
+qed_spec_mp "approx_val_None";
+
+
+Goalw [approx_val_def]
+"approx_val G hp Null (Some(RefT x))";
+by(Simp_tac 1);
+by (fast_tac (claset() addIs widen.intrs) 1);
+qed_spec_mp "approx_val_Null";
+
+
+Goal
+"\\<lbrakk> wf_prog wt G \\<rbrakk> \
+\\\<Longrightarrow> approx_val G hp v (Some T) \\<longrightarrow> G\\<turnstile> T\\<preceq>T' \\<longrightarrow> approx_val G hp v (Some T')";
+by (exhaust_tac "T" 1);
+ by (Asm_simp_tac 1);
+by (fast_tac (claset() addIs [conf_widen] addss (simpset()addsimps[approx_val_def])) 1);
+qed_spec_mp "approx_val_imp_approx_val_assConvertible";
+
+
+Goal
+"approx_val G hp val at \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> approx_val G hp' val at";
+by (asm_full_simp_tac (simpset() setloop (split_tac [option.split])
+ addsimps [approx_val_def]) 1);
+by(blast_tac (claset() addIs [conf_hext]) 1);
+qed_spec_mp "approx_val_imp_approx_val_sup_heap";
+
+Goal
+"\\<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";
+by (exhaust_tac "v" 1);
+by (auto_tac (claset() , simpset() addsimps [obj_ty_def,conf_def] addsplits [option.split]));
+qed_spec_mp "approx_val_imp_approx_val_heap_update";
+
+
+Goal
+"wf_prog wt G \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us' >= us \\<longrightarrow> approx_val G h val us'";
+by (asm_simp_tac (simpset() addsimps [sup_PTS_eq,approx_val_def] addsplits [option.split,val_.split,ty.split]) 1);
+by(blast_tac (claset() addIs [conf_widen]) 1);
+qed_spec_mp "approx_val_imp_approx_val_sup";
+
+
+Goal
+"\\<lbrakk> wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\<turnstile> at >= LT ! idx \\<rbrakk> \
+\\\<Longrightarrow> approx_val G hp val at";
+by (fast_tac (claset() addIs [approx_val_imp_approx_val_sup] addss (simpset() addsimps
+ [split_def,approx_loc_def,all_set_conv_all_nth])) 1);
+qed "approx_loc_imp_approx_val_sup";
+
+
+(** approx_loc **)
+
+Goal
+"approx_loc G hp (s#xs) (l#ls) = \
+\ ((length xs = length ls) \\<and> (approx_val G hp s l) \\<and> (approx_loc G hp xs ls))";
+by (fast_tac (claset() addss (simpset() addsimps [approx_loc_def])) 1);
+qed "approx_loc_Cons";
+
+
+Goalw [approx_stk_def,approx_loc_def]
+"\\<lbrakk> wf_prog wt G \\<rbrakk> \
+\\\<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> approx_loc G hp s (map Some ts)";
+by (force_tac (claset() addIs [approx_val_imp_approx_val_assConvertible], simpset()
+ addsimps [all_set_conv_all_nth,split_def]) 1);
+qed_spec_mp "assConv_approx_stk_imp_approx_loc";
+
+
+Goalw [approx_loc_def]
+"\\<forall> lvars. approx_loc G hp lvars lt \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> approx_loc G hp' lvars lt";
+by (exhaust_tac "lt" 1);
+ by (Asm_simp_tac 1);
+by (force_tac (claset() addIs [approx_val_imp_approx_val_sup_heap],
+ simpset() addsimps [neq_Nil_conv]) 1);
+qed_spec_mp "approx_loc_imp_approx_loc_sup_heap";
+
+
+Goalw [sup_loc_def,approx_loc_def]
+"wf_prog wt G \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt' >>= lt \\<longrightarrow> approx_loc G hp lvars lt'";
+by (auto_tac (claset() , simpset() addsimps [all_set_conv_all_nth,split_def]));
+by (auto_tac (claset() addEs [approx_val_imp_approx_val_sup] , simpset()));
+qed_spec_mp "approx_loc_imp_approx_loc_sup";
+
+
+Goalw [approx_loc_def]
+"\\<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]))";
+by (fast_tac (claset() addDs [set_update_subset RS subsetD]
+ addss (simpset() addsimps [zip_update])) 1);
+qed_spec_mp "approx_loc_imp_approx_loc_subst";
+
+
+Goal
+"\\<forall>L1 l2 L2. length l1=length L1 \
+\ \\<longrightarrow> approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \\<and> approx_loc G hp l2 L2)";
+by (induct_tac "l1" 1);
+ by (fast_tac (claset() addDs [] addss (simpset() addsimps [approx_loc_def])) 1);
+br allI 1;
+by (exhaust_tac "L1" 1);
+ by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [approx_loc_Cons]) 1);
+by (case_tac "length l2 = length L2" 1);
+ by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (asm_full_simp_tac (simpset() addsimps [approx_loc_def]) 1);
+qed_spec_mp "approx_loc_append";
+
+
+(** approx_stk **)
+
+Goalw [approx_stk_def,approx_loc_def]
+"approx_stk G hp (rev s) (rev t) = approx_stk G hp s t";
+by (fast_tac (claset() addss (simpset() addsimps [zip_rev,rev_map RS sym])) 1);
+qed_spec_mp "approx_stk_rev_lem";
+
+Goal
+"approx_stk G hp (rev s) t = approx_stk G hp s (rev t)";
+by (fast_tac (claset() addIs [approx_stk_rev_lem RS subst] addss (simpset())) 1);
+qed_spec_mp "approx_stk_rev";
+
+Goalw [approx_stk_def]
+"\\<forall> lvars. approx_stk G hp lvars lt \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> approx_stk G hp' lvars lt";
+by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup_heap]) 1);
+qed_spec_mp "approx_stk_imp_approx_stk_sup_heap";
+
+
+Goalw [approx_stk_def]
+"wf_prog wt G \\<Longrightarrow> approx_stk G hp lvars st \\<longrightarrow> G \\<turnstile> (map Some st') >>= (map Some st) \\<longrightarrow> approx_stk G hp lvars st'";
+by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup]) 1);
+qed_spec_mp "approx_stk_imp_approx_stk_sup";
+
+Goalw [approx_stk_def,approx_loc_def]
+"approx_stk G hp [] []";
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+qed "approx_stk_Nil";
+
+
+Goalw [approx_stk_def,approx_loc_def]
+"approx_stk G hp (x # stk) (S#ST) = (approx_stk G hp stk ST \\<and> approx_val G hp x (Some S))";
+by (fast_tac (claset() addss (simpset())) 1);
+qed "approx_stk_Cons";
+
+Goal
+"\\<lbrakk> approx_stk G hp stk (S#ST') \\<rbrakk> \
+\ \\<Longrightarrow> \\<exists>s stk'. stk = s#stk' \\<and> approx_stk G hp stk' ST' \\<and> approx_val G hp s (Some S)";
+by (exhaust_tac "stk" 1);
+ by (fast_tac (claset() addss (simpset() addsimps [approx_stk_def,approx_loc_def])) 1);
+by (fast_tac (claset() addss (simpset() addsimps [approx_stk_Cons])) 1);
+qed "approx_stk_Cons_lemma";
+
+Goal
+"\\<forall>ST' stk. approx_stk G hp stk (S@ST') \
+\ \\<longrightarrow> (\\<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 (induct_tac "S" 1);
+ by (fast_tac (claset() addDs [] addss (simpset() addsimps [approx_stk_def,approx_loc_def])) 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+bd approx_stk_Cons_lemma 1;
+by (Clarify_tac 1);
+by (eres_inst_tac [("x","ST'")] allE 1);
+by (eres_inst_tac [("x","stk'")] allE 1);
+by (Clarify_tac 1);
+by (res_inst_tac [("x","s#sa")] exI 1);
+by (res_inst_tac [("x","stk'a")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps [approx_stk_Cons]) 1);
+qed_spec_mp "approx_stk_append_lemma";
+
+
+(** oconf **)
+
+Goalw [oconf_def,lconf_def]
+"\\<lbrakk> is_class G C; wf_prog wt G \\<rbrakk> \\<Longrightarrow> \
+\G,h\\<turnstile> (C, map_of (map (\\<lambda>(f,fT).(f,default_val fT)) (fields(G,C))))\\<surd>";
+by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);
+by (force_tac (claset() addIs [defval_conf]
+ addDs [map_of_SomeD,is_type_fields],simpset()) 1);
+qed "correct_init_obj";
+
+
+Goalw [oconf_def,lconf_def]
+"\\<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>";
+by (asm_full_simp_tac (simpset() addsplits [ty.split]) 1);
+qed_spec_mp "oconf_imp_oconf_field_update";
+
+
+Goalw [oconf_def,lconf_def]
+"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>";
+by (Asm_full_simp_tac 1);
+by (fast_tac (claset() addIs [conf_hext,sup_heap_newref]) 1);
+qed_spec_mp "oconf_imp_oconf_heap_newref";
+
+Goalw [oconf_def,lconf_def]
+"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>";
+by (Asm_full_simp_tac 1);
+by (fast_tac (claset() addIs [approx_val_imp_approx_val_heap_update] addss (simpset())) 1);
+qed_spec_mp "oconf_imp_oconf_heap_update";
+
+
+(** hconf **)
+
+
+Goal "hp x = None \\<longrightarrow> G,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G,hp(newref hp\\<mapsto>obj)\\<turnstile>\\<surd>";
+by (asm_full_simp_tac (simpset() addsplits [split_split]
+ addsimps [hconf_def]) 1);
+ by (fast_tac (claset()addIs[oconf_imp_oconf_heap_newref] addss (simpset())) 1);
+qed_spec_mp "hconf_imp_hconf_newref";
+
+
+Goal "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,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp(oloc \\<mapsto> (oT, fs((F,D)\\<mapsto>v)))\\<turnstile>\\<surd>";
+by (asm_full_simp_tac (simpset() addsimps [hconf_def]) 1);
+by (fast_tac (claset() addIs
+ [oconf_imp_oconf_heap_update, oconf_imp_oconf_field_update]
+ addss (simpset() addsimps [obj_ty_def])) 1);
+qed_spec_mp "hconf_imp_hconf_field_update";
+
+
+(** correct_frames **)
+
+Delsimps [fun_upd_apply];
+Goal
+"\\<forall>rT C ml. correct_frames G hp phi rT C ml frs \\<longrightarrow> \
+\ hp a = Some (cn,od) \\<longrightarrow> map_of (fields (G, cn)) fl = Some fd \\<longrightarrow> \
+\ G,hp\\<turnstile>v\\<Colon>\\<preceq>fd \
+\ \\<longrightarrow> correct_frames G (hp(a \\<mapsto> (cn, od(fl\\<mapsto>v)))) phi rT C ml frs";
+by (induct_tac "frs" 1);
+ by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1);
+by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap,
+ approx_loc_imp_approx_loc_sup_heap,
+ sup_heap_update_value] addss (simpset())) 1);
+qed_spec_mp "correct_frames_imp_correct_frames_field_update";
+
+
+Goal
+"\\<forall>rT C ml. hp x = None \\<longrightarrow> correct_frames G hp phi rT C ml frs \\<and> \
+\ oconf G hp obj \
+\ \\<longrightarrow> correct_frames G (hp(newref hp \\<mapsto> obj)) phi rT C ml frs";
+by (induct_tac "frs" 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1);
+by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap,
+ approx_loc_imp_approx_loc_sup_heap,
+ hconf_imp_hconf_newref,
+ sup_heap_newref] addss (simpset())) 1);
+qed_spec_mp "correct_frames_imp_correct_frames_newref";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Correct.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,65 @@
+(* Title: HOL/MicroJava/BV/Correct.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+
+The invariant for the type safety proof.
+*)
+
+Correct = BVSpec +
+
+constdefs
+ approx_val :: "[jvm_prog,aheap,val,ty option] \\<Rightarrow> bool"
+"approx_val G h v any \\<equiv> case any of None \\<Rightarrow> True | Some T \\<Rightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T"
+
+ approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \\<Rightarrow> bool"
+"approx_loc G hp loc LT \\<equiv>
+ length loc=length LT \\<and> (\\<forall>(val,any)\\<in>set (zip loc LT). approx_val G hp val any)"
+
+ approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \\<Rightarrow> bool"
+"approx_stk G hp stk ST \\<equiv> approx_loc G hp stk (map Some 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,ml,pc).
+ approx_stk G hp stk ST \\<and> approx_loc G hp loc LT \\<and>
+ pc < length ins \\<and> length loc=length(snd ml)+maxl+1"
+
+consts
+ correct_frames :: "[jvm_prog,aheap,prog_type,ty,cname,sig,frame list] \\<Rightarrow> bool"
+primrec
+"correct_frames G hp phi rT0 C0 ml0 [] = False"
+
+"correct_frames G hp phi rT0 C0 ml0 (f#frs) =
+ (let (stk,loc,C,ml,pc) = f;
+ (ST,LT) = (phi C ml) ! pc
+ in
+ (\\<exists>rT maxl ins.
+ cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
+ (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invokevirtual mn pTs) \\<and>
+ (mn,pTs) = ml0 \\<and>
+ (\\<exists>apTs D ST'.
+ fst((phi C ml)!k) = (rev apTs) @ (Class D) # ST' \\<and>
+ length apTs = length pTs \\<and>
+ (\\<exists>D' rT' maxl' ins'.
+ cmethd (G,D) (mn,pTs) = Some(D',rT',(maxl',ins')) \\<and>
+ G \\<turnstile> rT0 \\<preceq> rT') \\<and>
+ correct_frame G hp (tl ST, LT) maxl ins f \\<and>
+ correct_frames G hp phi rT C ml frs))))"
+
+
+constdefs
+ correct_state :: "[jvm_prog,prog_type,jvm_state] \\<Rightarrow> bool"
+"correct_state G phi \\<equiv> \\<lambda>(xp,hp,frs).
+ case xp of
+ None \\<Rightarrow> (case frs of
+ [] \\<Rightarrow> True
+ | (f#fs) \\<Rightarrow> (let (stk,loc,C,ml,pc) = f
+ in
+ \\<exists>rT maxl ins.
+ cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
+ G,hp\\<turnstile>\\<surd> \\<and>
+ correct_frame G hp ((phi C ml) ! pc) maxl ins f \\<and>
+ correct_frames G hp phi rT C ml fs))
+ | Some x \\<Rightarrow> True"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Conform.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,256 @@
+(* Title: HOL/MicroJava/J/Conform.ML
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+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 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')"
+ (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 [
+ 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 [
+ rtac hextI 1,
+ safe_tac HOL_cs,
+ fast_tac (HOL_cs addDs [hext_objD]) 1]);
+
+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 [
+ rtac hextI 1,
+ safe_tac HOL_cs,
+ ALLGOALS (case_tac "aa = a"),
+ Auto_tac]);
+
+
+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]);
+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 [
+ rtac val_.induct 1,
+ Auto_tac]) RS mp;
+
+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"
+(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>Class C\\<preceq>Class D\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<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";
+by (Simp_tac 1);
+by (res_inst_tac [("y","T")] ty.exhaust 1);
+by (etac ssubst 1);
+by (res_inst_tac [("y","prim_ty")] prim_ty.exhaust 1);
+by (auto_tac (claset(), simpset() addsimps [widen.null]));
+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 _ => [
+ rtac impI 1,
+ rtac val_.induct 1,
+ ALLGOALS Simp_tac,
+ case_tac "loc = a" 1,
+ ALLGOALS Asm_simp_tac]) RS mp;
+
+val conf_widen = prove_goalw thy [conf_def]
+"\\<And>G. wf_prog wtm G \\<Longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T \\<longrightarrow> G\\<turnstile>T\\<preceq>T' \\<longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T'" (K [
+ rtac val_.induct 1,
+ ALLGOALS Simp_tac,
+ ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp;
+
+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 [
+ REPEAT (rtac allI 1),
+ rtac val_.induct 1,
+ ALLGOALS Simp_tac,
+ safe_tac (HOL_cs addSDs [option_map_SomeD]),
+ rewtac option_map_def,
+ dtac hext_objD 1,
+ Auto_tac]);
+val conf_hext = conf_hext' RS spec RS spec RS mp;
+
+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 => [
+ cut_facts_tac prems 1,
+ Full_simp_tac 1,
+ safe_tac HOL_cs,
+ Asm_full_simp_tac 1]);
+
+val conf_RefTD = prove_goalw thy [conf_def] "G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT T \\<longrightarrow> 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)" (K [
+ induct_tac "a'" 1,
+ Auto_tac,
+ REPEAT (etac widen_PrimT_RefT 1)]) RS mp;
+
+val conf_NullTD = prove_goal thy "\\<And>G. G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT NullT \\<Longrightarrow> a' = Null" (K [
+ dtac conf_RefTD 1,
+ Step_tac 1,
+ Auto_tac,
+ etac widen_Class_NullT 1]);
+
+val non_npD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t\\<rbrakk> \\<Longrightarrow> \
+\ \\<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> \
+\ (\\<exists>a C' fs. a' = Addr a \\<and> h a = Some (C',fs) \\<and> G\\<turnstile>Class C'\\<preceq>Class C)"
+ (K[fast_tac (HOL_cs addDs [non_npD]) 1]);
+
+Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wtm G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
+\ (\\<forall>C. t = ClassT C \\<longrightarrow> C \\<noteq> Object) \\<longrightarrow> \
+\ (\\<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);
+by (res_inst_tac [("y","t")] ref_ty.exhaust 1);
+by (safe_tac HOL_cs);
+by (dtac conf_NullTD 1);
+by (contr_tac 1);
+by (etac non_np_objD 1);
+by (atac 1);
+by (Fast_tac 1);
+qed_spec_mp "non_np_objD'";
+
+Goal "wf_prog wtm 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'";
+by( induct_tac "vs" 1);
+by( ALLGOALS Clarsimp_tac);
+by( ALLGOALS (forward_tac [list_all2_lengthD RS sym]));
+by( ALLGOALS (full_simp_tac (simpset()addsimps[length_Suc_conv])));
+by( Safe_tac);
+by( rotate_tac ~1 1);
+by( ALLGOALS (forward_tac [list_all2_lengthD RS sym]));
+by( ALLGOALS (full_simp_tac (simpset()addsimps[length_Suc_conv])));
+by( ALLGOALS Clarify_tac);
+by( fast_tac (claset() addEs [conf_widen]) 1);
+qed_spec_mp "conf_list_gext_widen";
+
+
+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"
+ (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 [
+ 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";
+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> \
+\ (\\<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";
+by Auto_tac;
+by( rtac lconf_init_vars_lemma 1);
+by( atac 3);
+by( strip_tac 1);
+by( etac defval_conf 1);
+by Auto_tac;
+qed "lconf_init_vars";
+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)"
+ (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)";
+by( induct_tac "vns" 1);
+by( ALLGOALS Clarsimp_tac);
+by( forward_tac [list_all2_lengthD] 1);
+by( auto_tac (claset(), simpset() addsimps [length_Suc_conv]));
+qed_spec_mp "lconf_ext_list";
+
+
+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]);
+
+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 [
+ Auto_tac]);
+
+val oconf_objD = oconf_obj RS iffD1 RS spec RS spec RS mp;
+
+
+section "hconf";
+
+Goalw [hconf_def] "\\<lbrakk>G,h\\<turnstile>\\<surd>; h a = Some obj\\<rbrakk> \\<Longrightarrow> 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,h\\<turnstile>\\<surd>";
+by (Fast_tac 1);
+qed "hconfI";
+
+
+section "conforms";
+
+val conforms_heapD = prove_goalw thy [conforms_def]
+ "(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G,h\\<turnstile>\\<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 => [
+ cut_facts_tac prems 1, Asm_full_simp_tac 1]);
+
+val conformsI = prove_goalw thy [conforms_def]
+"\\<lbrakk>G,h\\<turnstile>\\<surd>; G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT\\<rbrakk> \\<Longrightarrow> (h, l)\\<Colon>\\<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,h'\\<turnstile>\\<surd> \\<rbrakk> \\<Longrightarrow> (h',l)\\<Colon>\\<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)";
+by( rtac conforms_hext 1);
+by Auto_tac;
+by( rtac hconfI 1);
+by( dtac conforms_heapD 1);
+by( (auto_tac (HOL_cs addEs [oconf_hext] addDs [hconfD],
+ simpset()delsimps[split_paired_All])));
+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)";
+by( auto_tac (claset() addEs [lconf_upd], simpset()));
+qed "conforms_upd_local";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Conform.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,32 @@
+(* Title: HOL/MicroJava/J/Conform.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+
+Conformity relations for type safety of Java
+*)
+
+Conform = State +
+
+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'))"
+
+ 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"
+
+ 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)"
+
+ 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))"
+
+ hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool" ("_,_\\<turnstile>\\<surd>" [51,51] 50)
+ "G,h\\<turnstile>\\<surd> \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
+
+ conforms :: "state \\<Rightarrow> javam env \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50)
+ "s\\<Colon>\\<preceq>E \\<equiv> prg E,heap s\\<turnstile>\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Decl.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,37 @@
+(* Title: HOL/MicroJava/J/Decl.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1997 Technische Universitaet Muenchen
+
+Class declarations
+*)
+
+Decl = Type +
+
+types fdecl (* field declaration, cf. 8.3 (, 9.3) *)
+ = "vname \\<times> ty"
+
+
+types sig (* signature of a method, cf. 8.4.2 *)
+ = "mname \\<times> ty list"
+
+ 'c mdecl (* method declaration in a class *)
+ = "sig \\<times> ty \\<times> 'c"
+
+types 'c class (* class *)
+ = "cname option \\<times> fdecl list \\<times> 'c mdecl list"
+ (* superclass, fields, methods*)
+
+ 'c cdecl (* class declaration, cf. 8.1 *)
+ = "cname \\<times> 'c class"
+
+consts
+
+ Object :: cname (* name of root class *)
+ ObjectC :: 'c cdecl (* decl of root class *)
+
+defs
+
+ ObjectC_def "ObjectC \\<equiv> (Object, (None, [], []))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Eval.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,39 @@
+(* Title: HOL/MicroJava/J/Eval.ML
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+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)";
+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 [
+ 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 [
+ 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)"
+ (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 [
+ 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 [
+ dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1,
+ Fast_tac 1]);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Eval.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,121 @@
+(* Title: HOL/MicroJava/J/Eval.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+
+Operational evaluation (big-step) semantics of the
+execution of Java expressions and statements
+*)
+
+Eval = State +
+
+consts
+ eval :: "javam prog \\<Rightarrow> (xstate \\<times> expr \\<times> val \\<times> xstate) set"
+ evals :: "javam prog \\<Rightarrow> (xstate \\<times> expr list \\<times> val list \\<times> xstate) set"
+ exec :: "javam prog \\<Rightarrow> (xstate \\<times> stmt \\<times> xstate) set"
+
+syntax
+ eval :: "[javam prog,xstate,expr,val,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<succ>_\\<rightarrow> _"[51,82,82,82,82]81)
+ evals:: "[javam prog,xstate,expr list,
+ val list,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_[\\<succ>]_\\<rightarrow> _"[51,82,51,51,82]81)
+ exec :: "[javam prog,xstate,stmt, xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _" [51,82,82, 82]81)
+
+translations
+ "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" == "(s, e, v, _args 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, _args 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, _args x s') \\<in> exec G"
+ "G\\<turnstile>s -c \\<rightarrow> 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)"
+
+ (* 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)"
+
+ (* cf. 15.15 *)
+ Cast "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>v\\<rightarrow> (x1,s1);
+ x2=raise_if (\\<not> cast_ok G T (heap s1) v) ClassCast x1\\<rbrakk> \\<Longrightarrow>
+ G\\<turnstile>Norm s0 -Cast T e\\<succ>v\\<rightarrow> (x2,s1)"
+
+ (* cf. 15.7.1 *)
+ Lit "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s"
+
+ (* cf. 15.13.1, 15.2 *)
+ LAcc "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)\\<rightarrow> 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'))"
+
+
+ (* 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)"
+
+ (* 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);
+ 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\\<in>=e2\\<succ>v\\<rightarrow> 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));
+ (md,rT,pns,lvars,blk,res) = the (cmethd (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))"
+
+
+(* evaluation of expression lists *)
+
+ (* cf. 15.5 *)
+ XcptEs "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary\\<rightarrow> (Some xc,s)"
+
+ (* cf. 15.11.??? *)
+ Nil
+ "G\\<turnstile>Norm s0 -[][\\<succ>][]\\<rightarrow> 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"
+
+(* execution of statements *)
+
+ (* cf. 14.1 *)
+ XcptS "G\\<turnstile>(Some xc,s) -s0\\<rightarrow> (Some xc,s)"
+
+ (* cf. 14.5 *)
+ Skip "G\\<turnstile>Norm s -Skip\\<rightarrow> 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"
+
+ (* 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"
+
+ (* 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"
+
+ (* 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"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/JBasis.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,230 @@
+(* Title: HOL/MicroJava/J/JBasis.ML
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 TU Muenchen
+*)
+
+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";
+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]);
+
+
+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 => [
+ 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 => [
+ REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
+ res_inst_tac [("P1","P")] (split_beta RS subst) 1,
+ rtac (hd prems) 1]);
+
+
+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"
+ (fn prems => [rtac ballE 1, resolve_tac prems 1,
+ eresolve_tac prems 1, eresolve_tac prems 1]);
+
+val set_cs2 = set_cs delrules [ballE] addSEs [BallE];
+
+Addsimps [Let_def];
+Addsimps [surjective_pairing RS sym];
+
+(* To HOL.ML *)
+
+val ex1_Eps_eq = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y"
+ (fn prems => [
+ cut_facts_tac prems 1,
+ rtac select_equality 1,
+ atac 1,
+ etac ex1E 1,
+ etac all_dupE 1,
+ fast_tac HOL_cs 1]);
+
+
+val ball_insert = prove_goalw equalities.thy [Ball_def]
+ "Ball (insert x A) P = (P x \\<and> Ball A P)" (fn _ => [
+ fast_tac set_cs 1]);
+
+fun option_case_tac i = EVERY [
+ etac option_caseE i,
+ rotate_tac ~2 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
+ rotate_tac ~2 i , asm_full_simp_tac HOL_basic_ss i];
+
+val not_None_tac = EVERY' [dtac (not_None_eq RS iffD1),rotate_tac ~1,etac exE,
+ rotate_tac ~1,asm_full_simp_tac
+ (simpset() delsimps [split_paired_All,split_paired_Ex])];
+
+fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1,
+ 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"
+ (fn prems => [
+ case_tac "opt = None" 1,
+ eresolve_tac prems 1,
+ not_None_tac 1,
+ eresolve_tac prems 1]);
+
+fun option_case_tac2 s i = EVERY [
+ exhaust_tac s i,
+ rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
+ 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 [
+ option_case_tac2 "x" 1,
+ Auto_tac]);
+
+
+section "unique";
+
+Goal "(x, y) : set l --> x : fst `` set l";
+by (induct_tac "l" 1);
+by Auto_tac;
+qed_spec_mp "fst_in_set_lemma";
+
+Goalw [unique_def] "unique []";
+by (Simp_tac 1);
+qed "unique_Nil";
+
+Goalw [unique_def] "unique ((x,y)#l) = (unique l \\<and> (!y. (x,y) ~: set l))";
+by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
+qed "unique_Cons";
+
+Addsimps [unique_Nil,unique_Cons];
+
+Goal "unique l' ==> unique l --> \
+\ (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')";
+by (induct_tac "l" 1);
+by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
+qed_spec_mp "unique_append";
+
+Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)";
+by (induct_tac "l" 1);
+by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
+qed_spec_mp "unique_map_inj";
+
+Goal "\\<And>l. unique l \\<Longrightarrow> 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";
+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 [
+ etac imageE 1,
+ split_all_tac 1,
+ auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]);
+
+
+section "list_all2";
+
+val list_all2_lengthD = prove_goalw thy [list_all2_def]
+ "\\<And>X. list_all2 P as bs \\<Longrightarrow> length as = length bs" (K [Auto_tac]);
+
+val list_all2_Nil = prove_goalw thy [list_all2_def]
+ "list_all2 P [] []" (K [Auto_tac]);
+Addsimps[list_all2_Nil];
+AddSIs[list_all2_Nil];
+
+val list_all2_Cons = prove_goalw thy [list_all2_def]
+ "\\<And>X. list_all2 P (a#as) (b#bs) = (P a b \\<and> list_all2 P as bs)" (K [Auto_tac]);
+AddIffs[list_all2_Cons];
+
+
+(* More about Maps *)
+
+val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x \\<Longrightarrow> \
+\ 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,
+ etac exE 1,
+ rotate_tac ~1 1,
+ Asm_full_simp_tac 1,
+ asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1,
+ rotate_tac ~1 1,
+ Asm_full_simp_tac 1]);
+
+Addsimps [fun_upd_same, fun_upd_other];
+
+Goal "unique xys \\<longrightarrow> (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);
+qed_spec_mp "unique_map_of_Some_conv";
+
+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)";
+by(induct_tac "l" 1);
+by(ALLGOALS Simp_tac);
+by Safe_tac;
+by Auto_tac;
+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 _ => [
+ 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> \
+\ 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 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 [
+ 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 [
+ 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 [
+ forward_tac [table_mapf_SomeD] 1,
+ Auto_tac,
+ rtac table_mapf_Some 1,
+ atac 2,
+ Fast_tac 1]);
+
+val finite_map_of = rewrite_rule [dom_def] finite_dom_map_of;
+
+Goal
+"map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
+by (induct_tac "xs" 1);
+auto();
+qed "map_of_map";
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/JBasis.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,19 @@
+(* Title: HOL/MicroJava/J/JBasis.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 TU Muenchen
+
+Some auxiliary definitions.
+*)
+
+JBasis = Main +
+
+constdefs
+
+ unique :: "('a \\<times> 'b) list \\<Rightarrow> bool"
+ "unique \\<equiv> nodups \\<circ> map fst"
+
+ list_all2 :: "('a \\<Rightarrow> 'b \\<Rightarrow> bool) \\<Rightarrow> ('a list \\<Rightarrow> 'b list \\<Rightarrow> bool)"
+ "list_all2 P xs ys \\<equiv> length xs = length ys \\<and> (\\<forall> (x,y)\\<in>set (zip xs ys). P x y)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,349 @@
+(* Title: HOL/MicroJava/J/JTypeSafe.ML
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+
+Type safety proof
+*)
+
+Addsimps [split_beta];
+
+Goal "\\<lbrakk>h a = None; (h, l)\\<Colon>\\<preceq>(G, lT); wf_prog wtm G; is_class G C\\<rbrakk> \\<Longrightarrow> \
+\ (h(a\\<mapsto>(C,(init_vars (fields (G,C))))), l)\\<Colon>\\<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 wtm G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<Rightarrow>? T'; cast_ok G T' h v\\<rbrakk> \
+\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
+by( case_tac1 "v = Null" 1);
+by( Asm_full_simp_tac 1);
+by( dtac widen_RefT 1);
+by( Clarify_tac 1);
+by( forward_tac [cast_RefT] 1);
+by( Clarify_tac 1);
+by( rtac widen.null 1);
+by( case_tac1 "\\<exists>pt. T' = PrimT pt" 1);
+by( strip_tac1 1);
+by( dtac cast_PrimT2 1);
+by( etac conf_widen 1);
+by( atac 1);
+by( atac 1);
+by( Asm_full_simp_tac 1);
+by( dtac (non_PrimT RS iffD1) 1);
+by( strip_tac1 1);
+by( forward_tac [cast_RefT2] 1);
+by( strip_tac1 1);
+by( dtac non_npD 1);
+by( atac 1);
+by( rewrite_goals_tac [the_Addr_def,obj_ty_def]);
+by Auto_tac ;
+by( ALLGOALS (rtac conf_AddrI));
+by Auto_tac;
+qed "Cast_conf";
+
+Goal "\\<lbrakk> wf_prog wtm G; cfield (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";
+by( dtac np_NoneD 1);
+by( etac conjE 1);
+by( mp_tac 1);
+by( dtac non_np_objD 1);
+by Auto_tac;
+by( dtac (conforms_heapD RS hconfD) 1);
+by( atac 1);
+by( dtac widen_cfs_fields 1);
+by( atac 1);
+by( atac 1);
+by( dtac oconf_objD 1);
+by( atac 1);
+by Auto_tac;
+val FAcc_type_sound = result();
+
+Goal
+ "\\<lbrakk> wf_prog wtm 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; \
+\ cfield (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> \
+\ 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'";
+by( dtac np_NoneD 1);
+by( etac conjE 1);
+by( Asm_full_simp_tac 1);
+by( dtac non_np_objD 1);
+by( atac 1);
+by( SELECT_GOAL Auto_tac 1);
+by( strip_tac1 1);
+by( Full_simp_tac 1);
+by( EVERY [forward_tac [hext_objD] 1, atac 1]);
+by( etac exE 1);
+by( Asm_full_simp_tac 1);
+by( strip_tac1 1);
+by( rtac conjI 1);
+by( fast_tac (HOL_cs addEs [hext_trans, hext_upd_obj]) 1);
+by( rtac conjI 1);
+by( fast_tac (HOL_cs addEs [conf_upd_obj RS iffD2]) 2);
+
+by( rtac conforms_upd_obj 1);
+by Auto_tac;
+by( rtac hextI 2);
+by( Force_tac 2);
+by( rtac oconf_hext 1);
+by( etac hext_upd_obj 2);
+by( dtac widen_cfs_fields 1);
+by( atac 1);
+by( atac 1);
+by( rtac (oconf_obj RS iffD2) 1);
+by( Simp_tac 1);
+by( strip_tac 1);
+by( case_tac1 "(aaa, b) = (fn, fd)" 1);
+by( Asm_full_simp_tac 1);
+by( fast_tac (HOL_cs addIs [conf_widen]) 1);
+by( fast_tac (HOL_cs addDs [conforms_heapD RS hconfD, oconf_objD]) 1);
+val FAss_type_sound = result();
+
+Goalw [wf_mhead_def] "\\<lbrakk> wf_prog wtm 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')";
+by( Clarsimp_tac 1);
+by( rtac lconf_ext_list 1);
+by( rtac (Ball_set_table RS lconf_init_vars) 1);
+by( Force_tac 1);
+by( atac 1);
+by( atac 1);
+by( (etac conf_list_gext_widen THEN_ALL_NEW atac) 1);
+qed "Call_lemma2";
+
+Goalw [wf_java_prog_def]
+ "\\<lbrakk> wf_java_prog G; a' \\<noteq> Null; (h, l)\\<Colon>\\<preceq>(G, lT); \
+\ max_spec G T (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 (cmethd (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>RefT T \\<rbrakk> \\<Longrightarrow> \
+\ xc\\<le>|h' \\<and> (h', l)\\<Colon>\\<preceq>(G, lT) \\<and> (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>rTa)";
+by( dtac (insertI1 RSN (2,(equalityD2 RS subsetD))) 1);
+by( dtac (max_spec2appl_meths RS appl_methsD) 1);
+by( etac conjE 1);
+by( dtac non_np_objD' 1);
+by( atac 1);
+by( atac 1);
+by( strip_tac1 1);
+by( Asm_full_simp_tac 1);
+by( Clarsimp_tac 1);
+by( EVERY'[forward_tac [hext_objD], atac] 1);
+by( Clarsimp_tac 1);
+by( EVERY'[dtac Call_lemma, atac, atac] 1);
+by( clarsimp_tac (claset(),simpset() addsimps [wt_java_mdecl_def])1);
+by( thin_tac "cmethd ?sig ?x = ?y" 1);
+by( EVERY'[dtac spec, etac impE] 1);
+by( mp_tac 2);
+by( rtac conformsI 1);
+by( etac conforms_heapD 1);
+by( rtac lconf_ext 1);
+by( force_tac (claset() addSEs [Call_lemma2],simpset()) 1);
+by( EVERY'[etac conf_hext, etac conf_obj_AddrI, atac] 1);
+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( EVERY'[dtac spec, mp_tac] 1);
+by( thin_tac "?E\\<turnstile>res\\<Colon>?rT" 1);
+by( strip_tac1 1);
+by( rtac conjI 1);
+by( fast_tac (HOL_cs addIs [hext_trans]) 1);
+by( rtac conjI 1);
+by( rtac impI 2);
+by( mp_tac 2);
+by( forward_tac [conf_widen] 2);
+by( atac 4);
+by( atac 2);
+by( fast_tac (HOL_cs addSEs [widen_trans]) 2);
+by( etac conforms_hext 1);
+by( etac hext_trans 1);
+by( atac 1);
+by( etac conforms_heapD 1);
+qed "Call_type_sound";
+
+
+
+Unify.search_bound := 40;
+Unify.trace_bound := 40;
+Delsplits[split_if];
+Delsimps[fun_upd_apply];(*###*)
+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)))";
+by( rtac eval_evals_exec.induct 1);
+by( rewtac c_hupd_def);
+
+(* several simplifications, XcptE, XcptEs, XcptS, Skip *)
+by( ALLGOALS Asm_full_simp_tac);
+by( ALLGOALS strip_tac);
+by( ALLGOALS (eresolve_tac ty_expr_ty_exprs_wt_stmt.elims
+ THEN_ALL_NEW Full_simp_tac));
+by( ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac]));
+by( rewtac wf_java_prog_def);
+
+(* Level 7 *)
+
+(* 14 NewC *)
+by( dtac new_AddrD 1);
+by( etac disjE 1);
+by( Asm_simp_tac 2);
+by( etac conjE 1);
+by( Asm_simp_tac 1);
+by( rtac conjI 1);
+by( fast_tac (HOL_cs addSEs [NewC_conforms]) 1);
+by( rtac conf_obj_AddrI 1);
+by( rtac widen.refl 2);
+by( Asm_simp_tac 2);
+by( Simp_tac 1);
+
+(* for Cast *)
+by( defer_tac 1);
+
+(* 13 Lit *)
+by( etac conf_litval 1);
+
+(* 12 LAcc *)
+by( fast_tac (claset() addEs [conforms_localD RS lconfD]) 1);
+
+(* 11 Nil *)
+by( Simp_tac 5);
+
+(* for FAss *)
+by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac,
+ REPEAT o (etac conjE), hyp_subst_tac] 3);
+
+(* for if *)
+by( (case_tac1 "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);
+
+val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
+ (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]));
+by forward_hyp_tac;
+
+(* 10+1 if *)
+by( fast_tac (HOL_cs addIs [hext_trans]) 8);
+by( fast_tac (HOL_cs addIs [hext_trans]) 8);
+
+(* 9 Expr *)
+by( Fast_tac 6);
+
+by( ALLGOALS Asm_full_simp_tac);
+
+(* 8 Cast *)
+by( EVERY'[rtac impI, dtac raise_if_NoneD, Clarsimp_tac,
+ fast_tac (claset() addEs [Cast_conf])] 8);
+
+(* 7 LAss *)
+by( asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac] 1);
+by( blast_tac (claset() addIs [conforms_upd_local, conf_widen]) 1);
+
+(* 6 FAcc *)
+by( fast_tac (claset() addSEs [FAcc_type_sound]) 1);
+
+(* 5 While *)
+by( fast_tac (claset() addIs [ty_expr_ty_exprs_wt_stmt.Cond, ty_expr_ty_exprs_wt_stmt.Comp, ty_expr_ty_exprs_wt_stmt.Skip]
+ addEs [ty_expr_ty_exprs_wt_stmt.Loop]) 5);
+
+by forward_hyp_tac;
+
+(* 4 Cons *)
+by( fast_tac (claset() addDs [evals_no_xcpt] addIs [conf_hext,hext_trans]) 3);
+
+(* 3 ;; *)
+by( fast_tac (claset() addIs [hext_trans]) 3);
+
+(* 2 FAss *)
+by( case_tac1 "x2 = None" 1);
+by( Asm_simp_tac 2);
+by( fast_tac (claset() addIs [hext_trans]) 2);
+by( Asm_full_simp_tac 1);
+by( dtac eval_no_xcpt 1);
+by( SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1);
+
+by prune_params_tac;
+(* Level 45 *)
+
+(* 1 Call *)
+by( case_tac1 "x = None" 1);
+by( dtac (not_None_eq RS iffD1) 2);
+by( Clarsimp_tac 2);
+by( dtac exec_xcpt 2);
+by( Asm_full_simp_tac 2);
+by( dtac eval_xcpt 2);
+by( Asm_full_simp_tac 2);
+by( fast_tac (HOL_cs addEs [hext_trans]) 2);
+by( Clarify_tac 1);
+by( dtac evals_no_xcpt 1);
+by( Asm_full_simp_tac 1);
+by( case_tac1 "a' = Null" 1);
+by( Asm_full_simp_tac 1);
+by( dtac exec_xcpt 1);
+by( Asm_full_simp_tac 1);
+by( dtac eval_xcpt 1);
+by( Asm_full_simp_tac 1);
+by( fast_tac (HOL_cs addEs [hext_trans]) 1);
+by( (rtac (rewrite_rule[wf_java_prog_def]Call_type_sound) 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)";
+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";
+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>RefT T; m_head G T sig \\<noteq> None\\<rbrakk> \\<Longrightarrow> \
+\ cmethd (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
+by( dtac eval_type_sound 1);
+by( atac 1);
+by( atac 1);
+by( atac 1);
+by( atac 1);
+by( not_None_tac 1);
+by( split_all_tac 1);
+by(rewtac wf_java_prog_def);
+by( forward_tac [widen_methd] 1);
+by( atac 1);
+by( rtac (not_None_eq RS iffD1) 2);
+by( Fast_tac 2);
+by( etac conjE 1);
+by( dtac non_npD 1);
+by Auto_tac;
+qed "all_methods_understood";
+
+Delsimps [split_beta];
+Addsimps[fun_upd_apply];(*###*)
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,9 @@
+(* Title: HOL/MicroJava/J/JTypeSafe.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+
+Type Safety of Java
+*)
+
+JTypeSafe = Eval + Conform
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Prog.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,15 @@
+(* Title: HOL/MicroJava/J/Prog.ML
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+val finite_is_class = prove_goalw thy [is_class_def,class_def,o_def] "finite {C. is_class G C}" (K [
+ 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]);
+
+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 [
+ not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Prog.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,30 @@
+(* Title: HOL/MicroJava/J/Prog.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+
+Java program = list of class declarations
+*)
+
+Prog = Decl +
+
+types 'c prog = "'c cdecl list"
+
+consts
+
+ class :: "'c prog \\<Rightarrow> (cname \\<leadsto> 'c class)"
+
+ is_class :: "'c prog \\<Rightarrow> cname \\<Rightarrow> bool"
+ is_type :: "'c prog \\<Rightarrow> ty \\<Rightarrow> bool"
+
+defs
+
+ class_def "class \\<equiv> map_of"
+
+ is_class_def "is_class G C \\<equiv> 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)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/State.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,77 @@
+(* Title: HOL/MicroJava/J/State.ML
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+val the_Addr_Addr = prove_goalw thy [the_Addr_def]
+ "the_Addr (Addr a) = a" (K [Auto_tac]);
+
+Addsimps [the_Addr_Addr];
+
+val obj_ty_def2 = prove_goalw thy [obj_ty_def] "obj_ty (C,fs) = Class C"
+ (K [Simp_tac 1]);
+
+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[
+ asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1,
+ rtac selectI 1,
+ rtac disjI2 1,
+ res_inst_tac [("r","snd (a,Some OutOfMemory)")] trans 1,
+ Auto_tac ]);
+
+val raise_if_True = prove_goalw thy [raise_if_def]
+ "raise_if True x y \\<noteq> None"
+(K [split_tac [expand_if] 1,Auto_tac]);
+
+val raise_if_False = prove_goalw thy [raise_if_def]
+ "raise_if False x y = y"
+(K [Auto_tac]);
+
+val raise_if_Some = prove_goalw thy [raise_if_def]
+ "raise_if c x (Some y) \\<noteq> None" (K [Auto_tac]);
+
+val raise_if_Some2 = prove_goalw thy [raise_if_def]
+"raise_if c z (if x = None then Some y else x) \\<noteq> None" (K[
+ induct_tac "x" 1,
+ Auto_tac]);
+val if_None_eq = prove_goal thy
+"(if x = None then None else x) = x" (K[
+ induct_tac "x" 1,
+ Auto_tac]);
+
+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"
+(K [split_tac [expand_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"
+(K [split_tac [expand_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 _ => [
+ split_tac [expand_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 _ => [
+ split_tac [expand_if] 1,
+ Auto_tac ])) RS mp;
+val np_Some = prove_goalw thy [np_def, raise_if_def] "np a' (Some xc) = Some xc"
+ (fn _ => [Auto_tac ]);
+val np_Null = prove_goalw thy [np_def, raise_if_def]
+ "np Null None = Some NullPointer" (fn _ => [
+ Auto_tac ]);
+val np_Addr = prove_goalw thy [np_def, raise_if_def] "np (Addr a) None = None"
+ (fn _ => [Auto_tac ]);
+Addsimps[np_None, np_Some,np_Null,np_Addr];
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/State.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,91 @@
+(* Title: HOL/MicroJava/J/State.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+
+State for evaluation of Java expressions and statements
+*)
+
+State = WellType +
+
+constdefs
+
+ the_Bool :: "val \\<Rightarrow> bool"
+ "the_Bool v \\<equiv> \\<epsilon>b. v = Bool b"
+
+ the_Int :: "val \\<Rightarrow> int"
+ "the_Int v \\<equiv> \\<epsilon>i. v = Intg i"
+
+ the_Addr :: "val \\<Rightarrow> loc"
+ "the_Addr v \\<equiv> \\<epsilon>a. v = Addr a"
+
+consts
+
+ defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *)
+ default_val :: "ty \\<Rightarrow> val" (* default value for all types *)
+
+primrec
+ "defpval Void = Unit"
+ "defpval Boolean = Bool False"
+ "defpval Integer = Intg (#0)"
+
+primrec
+ "default_val (PrimT pt) = defpval pt"
+ "default_val (RefT r ) = Null"
+
+types fields_
+ = "(vname \\<times> cname \\<leadsto> val)" (* field name, defining class, value *)
+
+types obj = "cname \\<times> fields_" (* class instance with class name and fields *)
+
+constdefs
+
+ obj_ty :: "obj \\<Rightarrow> ty"
+ "obj_ty obj \\<equiv> 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))"
+
+datatype xcpt (* exceptions *)
+ = NullPointer
+ | ClassCast
+ | OutOfMemory
+
+types aheap = "loc \\<leadsto> obj" (* "heap" used in a translation below *)
+ locals = "vname \\<leadsto> val"
+
+ state (* simple state, i.e. variable contents *)
+ = "aheap \\<times> locals"
+ (* heap, local parameter including This *)
+
+ xstate (* state including exception information *)
+ = "xcpt option \\<times> state"
+
+syntax
+ heap :: "state \\<Rightarrow> aheap"
+ locals :: "state \\<Rightarrow> locals"
+ Norm :: "state \\<Rightarrow> xstate"
+
+translations
+ "heap" => "fst"
+ "locals" => "snd"
+ "Norm s" == "(None,s)"
+
+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"
+
+ 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"
+
+ np :: "val \\<Rightarrow> xcpt option \\<Rightarrow> xcpt option"
+ "np v \\<equiv> 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))"
+
+ cast_ok :: "'c prog \\<Rightarrow> ty \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> bool"
+ "cast_ok G T h v \\<equiv> ((\\<exists>pt. T = PrimT pt) | (v=Null) | G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq>T)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Term.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,41 @@
+(* Title: HOL/MicroJava/J/Term.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+
+Java expressions and statements
+*)
+
+Term = Type +
+
+types loc (* locations, i.e. abstract references on objects *)
+arities loc :: term
+
+datatype val_ (* name non 'val' because of clash with ML token *)
+ = Unit (* dummy result value of void methods *)
+ | Null (* null reference *)
+ | Bool bool (* Boolean value *)
+ | Intg int (* integer value *) (* Name Intg instead of Int because
+ of clash with HOL/Set.thy *)
+ | Addr loc (* addresses, i.e. locations of objects *)
+types val = val_
+translations "val" <= (type) "val_"
+
+datatype expr
+ = NewC cname (* class instance creation *)
+ | Cast ty expr (* type cast *)
+ | Lit val (* literal value, also references *)
+ | LAcc vname (* local (incl. parameter) access *)
+ | LAss vname expr (* local assign *) ("_\\<Colon>=_" [ 90,90]90)
+ | FAcc cname expr vname (* field access *) ("{_}_.._"[10,90,99 ]90)
+ | FAss cname expr vname
+ expr (* field ass. *)("{_}_.._\\<in>=_"[10,90,99,90]90)
+ | Call expr mname (ty list) (expr list)(* method call*)
+ ("_.._'({_}_')" [90,99,10,10] 90)
+and stmt
+ = Skip (* empty statement *)
+ | Expr expr (* expression statement *)
+ | Comp stmt stmt ("_;; _" [ 61,60]60)
+ | Cond expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70)
+ | Loop expr stmt ("While'(_') _" [ 80,79]70)
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Type.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,10 @@
+(* Title: HOL/MicroJava/J/Type.ML
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+Goal "(\\<forall>pt. T \\<noteq> PrimT pt) = (\\<exists>t. T = RefT t)";
+by(exhaust_tac "T" 1);
+by Auto_tac;
+qed "non_PrimT";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Type.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,39 @@
+(* Title: HOL/MicroJava/J/Type.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+
+Java types
+*)
+
+Type = JBasis +
+
+types cname (* class name *)
+ vnam (* variable or field name *)
+ mname (* method name *)
+arities cname, vnam, mname :: term
+
+datatype vname (* names for This pointer and local/field variables *)
+ = This
+ | VName vnam
+
+datatype prim_ty (* primitive type, cf. 4.2 *)
+ = Void (* 'result type' of void methods *)
+ | Boolean
+ | Integer
+
+datatype ref_ty (* reference type, cf. 4.3 *)
+ = NullT (* null type, cf. 4.1 *)
+ | ClassT cname (* class type *)
+and ty (* any type, cf. 4.1 *)
+ = PrimT prim_ty (* primitive type *)
+ | RefT ref_ty (* reference type *)
+
+syntax
+ NT :: " ty"
+ Class :: "cname \\<Rightarrow> ty"
+translations
+ "NT" == "RefT NullT"
+ "Class C" == "RefT (ClassT C)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/TypeRel.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,143 @@
+(* Title: HOL/MicroJava/J/TypeRel.ML
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+val subcls1D = prove_goalw thy [subcls1_def] "\\<And>G. G\\<turnstile>C\\<prec>C1D \\<Longrightarrow> \
+\ \\<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]);
+
+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})"
+ (K [Auto_tac]);
+
+context Option.thy;
+Goal "{y. x = Some y} \\<subseteq> {the x}";
+by Auto_tac;
+val some_subset_the = result();
+context thy;
+
+Goal "finite (subcls1 G)";
+by(stac subcls1_def2 1);
+by( rtac finite_SigmaI 1);
+by( rtac finite_is_class 1);
+by( rtac finite_subset 1);
+by( rtac some_subset_the 1);
+by( Simp_tac 1);
+qed "finite_subcls1";
+
+fun prove_typerel_lemma drules indrule s = prove_goal thy s (fn prems => [
+ rtac (hd prems RS indrule) 1,
+ auto_tac (claset() addDs drules, simpset())]);
+
+fun prove_typerel s lemmata = prove_goal thy s (fn prems => [
+ cut_facts_tac prems 1,
+ auto_tac (claset() addDs lemmata, simpset())]);
+
+
+(*#### patch for Isabelle98-1*)
+val major::prems = goal Trancl.thy
+ "\\<lbrakk> (x,y) \\<in> r^+; \
+\ \\<And>x y. (x,y) \\<in> r \\<Longrightarrow> P x y; \
+\ \\<And>x y z. \\<lbrakk> (x,y) \\<in> r^+; P x y; (y,z) \\<in> r^+; P y z \\<rbrakk> \\<Longrightarrow> P x z \
+\ \\<rbrakk> \\<Longrightarrow> P x y";
+by(blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
+qed "trancl_trans_induct";
+
+Goalw [is_class_def] "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> is_class G C";
+by(etac trancl_trans_induct 1);
+by (auto_tac (HOL_cs addSDs [subcls1D],simpset()));
+qed "subcls_is_class";
+
+
+(* A particular thm about wf;
+ looks like it is an odd instance of something more general
+*)
+Goalw [wf_def] "wf{((A,x),(B,y)) . A=B \\<and> wf(R(A)) \\<and> (x,y)\\<in>R(A)}";
+by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [split_paired_All]) 1);
+by(strip_tac 1);
+by(rename_tac "A x" 1);
+by(case_tac "wf(R A)" 1);
+by (eres_inst_tac [("a","x")] wf_induct 1);
+by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
+by (Fast_tac 1);
+by(rewrite_goals_tac [wf_def]);
+by(Blast_tac 1);
+val wf_rel_lemma = result();
+
+
+(* Proving the termination conditions *)
+
+goalw thy [subcls1_rel_def] "wf subcls1_rel";
+by(rtac (wf_rel_lemma RS wf_subset) 1);
+by(Force_tac 1);
+val wf_subcls1_rel = result();
+
+val cmethd_TC = prove_goalw_cterm [subcls1_rel_def]
+ (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (cmethd.tcs)))))
+ (K [auto_tac (claset() addIs [subcls1I], simpset())]);
+
+val fields_TC = prove_goalw_cterm [subcls1_rel_def]
+ (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (fields.tcs)))))
+ (K [auto_tac (claset() addIs [subcls1I], simpset())]);
+
+
+AddSIs [widen.refl];
+Addsimps [widen.refl];
+
+val prove_widen_lemma = prove_typerel_lemma [] widen.elim;
+
+val widen_PrimT_RefT = prove_typerel "G\\<turnstile>PrimT x\\<preceq>RefT tname \\<Longrightarrow> R"
+ [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = RefT tname \\<longrightarrow> R"];
+
+
+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_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_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_RefT = prove_typerel
+ "G\\<turnstile>Class C\\<preceq>RefT t \\<Longrightarrow> (\\<exists>tname. t=ClassT tname)"
+ [prove_widen_lemma
+ "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT t \\<longrightarrow> (\\<exists>tname. t=ClassT tname)"];
+
+val widen_Class_NullT = prove_typerel "G\\<turnstile>Class C\\<preceq>RefT NullT \\<Longrightarrow> R"
+ [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT NullT \\<longrightarrow> R"];
+
+val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>Class cm \\<Longrightarrow> C=cm | G\\<turnstile>C\\<prec>C cm"
+[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> C=cm | G\\<turnstile>C\\<prec>C cm"];
+
+Goal "\\<lbrakk>G\\<turnstile>S\\<preceq>U; \\<forall>C. is_class G C \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object;\
+\\\<forall>C. G\\<turnstile>Object\\<prec>C C \\<longrightarrow> False \\<rbrakk> \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
+by( etac widen.induct 1);
+by Safe_tac;
+by( ALLGOALS (forward_tac [widen_Class, widen_RefT]));
+by Safe_tac;
+by( rtac widen.null 2);
+by( forward_tac [widen_Class_Class] 1);
+by Safe_tac;
+by( ALLGOALS(EVERY'[etac thin_rl,etac thin_rl,
+ fast_tac (claset() addIs [widen.subcls,trancl_trans])]));
+qed_spec_mp "widen_trans_lemma";
+
+
+val prove_cast_lemma = prove_typerel_lemma [] cast.elim;
+
+val cast_RefT = prove_typerel "G\\<turnstile>RefT R\\<Rightarrow>? T \\<Longrightarrow> \\<exists>t. T=RefT t"
+ [prove_typerel_lemma [widen_RefT] cast.elim
+ "G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
+
+val cast_RefT2 = prove_typerel "G\\<turnstile>S\\<Rightarrow>? RefT R \\<Longrightarrow> \\<exists>t. S=RefT t"
+ [prove_typerel_lemma [widen_RefT2] cast.elim
+ "G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
+
+val cast_PrimT2 = prove_typerel "G\\<turnstile>S\\<Rightarrow>? PrimT pt \\<Longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"
+ [prove_cast_lemma "G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> T=PrimT pt \\<longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"];
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/TypeRel.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,76 @@
+(* Title: HOL/MicroJava/J/TypeRel.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+
+The relations between Java types
+*)
+
+TypeRel = Prog +
+
+consts
+ subcls1 :: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (* subclass *)
+ widen, (* widening *)
+ cast :: "'c prog \\<Rightarrow> (ty \\<times> ty) 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>_\\<prec>C _" [71,71,71] 70)
+ widen :: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>_" [71,71,71] 70)
+ cast :: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70)
+
+translations
+ "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
+ "G\\<turnstile>C \\<prec>C D" == "(C,D) \\<in> (subcls1 G)^+"
+ "G\\<turnstile>S \\<preceq> T" == "(S,T) \\<in> widen G"
+ "G\\<turnstile>S \\<Rightarrow>? T" == "(S,T) \\<in> cast G"
+
+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}"
+
+consts
+
+ cmethd :: "'c prog \\<times> cname \\<Rightarrow> ( sig \\<leadsto> cname \\<times> ty \\<times> 'c)"
+ cfield :: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
+ fields :: "'c prog \\<times> cname \\<Rightarrow> ((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}"
+
+(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
+recdef cmethd "subcls1_rel"
+ "cmethd (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>
+ if is_class G D then cmethd (G,D)
+ else arbitrary) \\<oplus>
+ map_of (map (\\<lambda>(s, m ).
+ (s,(C,m))) ms))
+ else arbitrary)"
+
+(* 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>
+ if is_class G D then fields (G,D)
+ else arbitrary))
+ else arbitrary)"
+defs
+
+ cfield_def "cfield \\<equiv> 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\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
+ null "G\\<turnstile> NT \\<preceq> RefT R"
+
+inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *)
+ widen "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> G\\<turnstile> S \\<Rightarrow>? T"
+ subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/WellForm.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,388 @@
+(* Title: HOL/MicroJava/J/WellForm.ML
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def]
+ "\\<And>X. \\<lbrakk>class G C = Some c; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> wf_cdecl wtm 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 wtm G \\<Longrightarrow> 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 wtm G \\<Longrightarrow> is_class G Object" (K [Asm_simp_tac 1]);
+Addsimps [is_class_Object];
+
+Goal "\\<lbrakk>G\\<turnstile>C\\<prec>C1D; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> D \\<noteq> C \\<and> \\<not> G\\<turnstile>D\\<prec>C C";
+by( forward_tac [r_into_trancl] 1);
+by( dtac subcls1D 1);
+by( strip_tac1 1);
+by( dtac class_wf 1);
+by( atac 1);
+by( rewtac wf_cdecl_def);
+by( Clarsimp_tac 1);
+qed "subcls1_wfD";
+
+val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def]
+"\\<And>X. \\<lbrakk>wf_cdecl wtm G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
+ pair_tac "r" 1,
+ Asm_full_simp_tac 1,
+ strip_tac1 1,
+ option_case_tac 1,
+ Fast_tac 1]);
+
+local
+val lemma = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> C=Object \\<longrightarrow> R" (K [
+ etac trancl_trans_induct 1,
+ atac 2,
+ rewtac subcls1_def,
+ Auto_tac]);
+in
+val subcls_Object = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>Object\\<prec>C C\\<rbrakk> \\<Longrightarrow> R" (K [
+ etac (lemma RS mp) 1,
+ Auto_tac]);
+end;
+
+Goal "\\<lbrakk>wf_prog wt G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> \\<not> G\\<turnstile>D\\<prec>C C";
+by(etac tranclE 1);
+by(ALLGOALS(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
+qed "subcls_asym";
+
+val subcls_irrefl = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> 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 wt G \\<Longrightarrow> 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 wtm G \\<Longrightarrow> wf ((subcls1 G)^-1)" (K [
+ rtac finite_acyclic_wf 1,
+ stac finite_converse 1,
+ rtac finite_subcls1 1,
+ stac acyclic_converse 1,
+ etac acyclic_subcls1 1]);
+
+
+val major::prems = goal thy
+ "\\<lbrakk>wf_prog wt G; \\<And>C. \\<forall>D. G\\<turnstile>C\\<prec>C D \\<longrightarrow> P D \\<Longrightarrow> P C\\<rbrakk> \\<Longrightarrow> 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);
+by(eres_inst_tac [("a","C")] wf_induct 1);
+by(resolve_tac prems 1);
+by(Auto_tac);
+qed "subcls_induct";
+
+val prems = goal thy "\\<lbrakk>is_class G C; wf_prog wtm 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 wtm 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";
+by( cut_facts_tac prems 1);
+by( rtac impE 1);
+by( atac 2);
+by( atac 2);
+by( etac thin_rl 1);
+by( rtac subcls_induct 1);
+by( atac 1);
+by( rtac impI 1);
+by( case_tac "C = Object" 1);
+by( Fast_tac 1);
+by( ex_ftac is_classD 1);
+by( forward_tac [class_wf] 1);
+by( atac 1);
+by( forward_tac [wf_cdecl_supD] 1);
+by( atac 1);
+by( strip_tac1 1);
+by( rtac (hd (tl (tl (tl prems)))) 1);
+by( atac 1);
+by( atac 1);
+by( subgoal_tac "G\\<turnstile>C\\<prec>C1D" 1);
+by( fast_tac (HOL_cs addIs [r_into_trancl]) 1);
+by( etac subcls1I 1);
+qed "subcls1_induct";
+
+Goal "wf_prog wtm G \\<Longrightarrow> cmethd (G,C) = \
+\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
+\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> cmethd (G,D)) \\<oplus> \
+\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
+by( stac (cmethd_TC RS (wf_subcls1_rel RS (hd cmethd.rules))) 1);
+by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]
+ addsplits [option.split]) 1);
+by( case_tac "C = Object" 1);
+by( Asm_full_simp_tac 1);
+by( dtac class_wf 1);
+by( atac 1);
+by( dtac wf_cdecl_supD 1);
+by( atac 1);
+by( Asm_full_simp_tac 1);
+val cmethd_rec = result();
+
+Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wtm G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
+\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
+\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
+by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.rules))) 1);
+by( asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
+by( option_case_tac2 "sc" 1);
+by( Asm_simp_tac 1);
+by( case_tac "C = Object" 1);
+by( rotate_tac 2 1);
+by( Asm_full_simp_tac 1);
+by( dtac class_wf 1);
+by( atac 1);
+by( dtac wf_cdecl_supD 1);
+by( atac 1);
+by( Asm_full_simp_tac 1);
+val fields_rec = result();
+
+val cmethd_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> cmethd (G,Object) = empty"
+ (K [stac cmethd_rec 1,Auto_tac]);
+val fields_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> fields (G,Object) = []"(K [
+ stac fields_rec 1,Auto_tac]);
+Addsimps [cmethd_Object, fields_Object];
+val cfield_Object = prove_goalw thy [cfield_def]
+ "\\<And>X. wf_prog wtm G \\<Longrightarrow> cfield (G,Object) = empty" (K [Asm_simp_tac 1]);
+Addsimps [cfield_Object];
+
+val subcls_C_Object = prove_goal thy
+ "\\<And>X. \\<lbrakk>is_class G C; wf_prog wtm G \\<rbrakk> \\<Longrightarrow> C \\<noteq> Object \\<longrightarrow> G\\<turnstile>C\\<prec>C Object" (K [
+ etac subcls1_induct 1,
+ atac 1,
+ Fast_tac 1,
+ safe_tac (HOL_cs addSDs [wf_cdecl_supD] addss (simpset())),
+ fast_tac (HOL_cs addIs [r_into_trancl]) 1,
+ rtac trancl_trans 1,
+ atac 2,
+ rtac r_into_trancl 1,
+ rtac subcls1I 1,
+ ALLGOALS Asm_simp_tac]) RS mp;
+
+val is_type_rTI = prove_goalw thy [wf_mhead_def]
+ "\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"
+ (K [split_all_tac 1, Auto_tac]);
+
+val widen_Class_Object = prove_goal thy
+ "\\<lbrakk>wf_prog wtm G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object" (fn prems => [
+ cut_facts_tac prems 1,
+ case_tac "C=Object" 1,
+ hyp_subst_tac 1,
+ Asm_simp_tac 1,
+ rtac widen.subcls 1,
+ fast_tac (HOL_cs addEs [subcls_C_Object]) 1]);
+
+val widen_trans = prove_goal thy "\\<lbrakk>wf_prog wtm G; G\\<turnstile>S\\<preceq>U; G\\<turnstile>U\\<preceq>T\\<rbrakk> \\<Longrightarrow> G\\<turnstile>S\\<preceq>T"
+(fn prems=> [cut_facts_tac prems 1,
+ fast_tac (HOL_cs addEs [widen_trans_lemma, widen_Class_Object,
+ subcls_Object]) 1]);
+
+val fields_mono = prove_goal thy
+"\\<And>X. \\<lbrakk>G\\<turnstile>C'\\<prec>C C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
+\ x \\<in> set (fields (G,C)) \\<longrightarrow> x \\<in> set (fields (G,C'))" (K [
+ etac trancl_trans_induct 1,
+ safe_tac (HOL_cs addSDs [subcls1D]),
+ stac fields_rec 1,
+ Auto_tac]) RS mp;
+
+Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
+\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>Class C\\<preceq>Class fd";
+by( etac subcls1_induct 1);
+by( atac 1);
+by( Asm_simp_tac 1);
+by( safe_tac HOL_cs);
+by( stac fields_rec 1);
+by( atac 1);
+by( atac 1);
+by( Simp_tac 1);
+by( rtac ballI 1);
+by( split_all_tac 1);
+by( Simp_tac 1);
+by( etac UnE 1);
+by( dtac split_Pair_eq 1);
+by( SELECT_GOAL (Auto_tac) 1);
+by( rtac widen_trans 1);
+by( atac 1);
+by( etac (r_into_trancl RS widen.subcls) 1);
+by( etac BallE 1);
+by( contr_tac 1);
+by( Asm_full_simp_tac 1);
+val widen_fields_defpl' = result();
+
+Goal "\\<lbrakk>is_class G C; wf_prog wtm G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
+\ G\\<turnstile>Class C\\<preceq>Class fd";
+by( dtac widen_fields_defpl' 1);
+by( atac 1);
+(*###################*)
+by( dtac bspec 1);
+auto();
+val widen_fields_defpl = result();
+
+
+Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> unique (fields (G,C))";
+by( etac subcls1_induct 1);
+by( atac 1);
+by( safe_tac (HOL_cs addSDs [wf_cdecl_supD]));
+by( Asm_simp_tac 1);
+by( dtac subcls1_wfD 1);
+by( atac 1);
+by( stac fields_rec 1);
+by Auto_tac;
+by( rotate_tac ~1 1);
+by( ex_ftac is_classD 1);
+by( forward_tac [class_wf] 1);
+by Auto_tac;
+by( asm_full_simp_tac (simpset() addsimps [wf_cdecl_def]) 1);
+by( etac unique_append 1);
+by( rtac unique_map_Pair 1);
+by( Step_tac 1);
+by (EVERY1[dtac widen_fields_defpl, atac, atac]);
+by( Asm_full_simp_tac 1);
+by( dtac split_Pair_eq 1);
+by( fast_tac (HOL_cs addSDs [widen_Class_Class]) 1);
+val unique_fields = result();
+
+Goal
+"\\<lbrakk>wf_prog wtm G; G\\<turnstile>Class C'\\<preceq>Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
+\ map_of (fields (G,C')) f = Some ft";
+by( dtac widen_Class_Class 1);
+by( etac disjE 1);
+by( Asm_simp_tac 1);
+by( rtac table_mono 1);
+by( atac 3);
+by( rtac unique_fields 1);
+by( etac subcls_is_class 1);
+by( atac 1);
+by( fast_tac (HOL_cs addEs [fields_mono]) 1);
+val widen_fields_mono = result();
+
+
+val cfs_fields_lemma = prove_goalw thy [cfield_def]
+"\\<And>X. cfield (G,C) fn = Some (fd, fT) \\<Longrightarrow> 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>cfield (G,C) fn = Some (fd, fT);\
+\ G\\<turnstile>Class C'\\<preceq>Class C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
+fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
+
+Goal "wf_prog wtm G \\<Longrightarrow> cmethd (G,C) sig = Some (md,mh,m)\
+\ \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class md \\<and> wf_mdecl wtm G md (sig,(mh,m))";
+by( case_tac "is_class G C" 1);
+by( forw_inst_tac [("C","C")] cmethd_rec 2);
+by( asm_full_simp_tac (simpset() addsimps [is_class_def]
+ delsimps [not_None_eq]) 2);
+by( etac subcls1_induct 1);
+by( atac 1);
+by( Force_tac 1);
+by( forw_inst_tac [("C","C")] cmethd_rec 1);
+by( strip_tac1 1);
+by( rotate_tac ~1 1);
+by( Asm_full_simp_tac 1);
+by( dtac override_SomeD 1);
+by( etac disjE 1);
+by( thin_tac "?P \\<longrightarrow> ?Q" 1);
+by( Clarify_tac 2);
+by( rtac widen_trans 2);
+by( atac 2);
+by( atac 3);
+by( rtac widen.subcls 2);
+by( rtac r_into_trancl 2);
+by( fast_tac (HOL_cs addIs [subcls1I]) 2);
+by( forward_tac [table_mapf_SomeD] 1);
+by( strip_tac1 1);
+by( Asm_full_simp_tac 1);
+by( rewtac wf_cdecl_def);
+by( Asm_full_simp_tac 1);
+val cmethd_wf_mdecl = result() RS mp;
+
+Goal "\\<lbrakk>G\\<turnstile>T\\<prec>C T'; wf_prog wt G\\<rbrakk> \\<Longrightarrow> \
+\ \\<forall>D rT b. cmethd (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
+\ (\\<exists>D' rT' b'. cmethd (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
+by( etac trancl_trans_induct 1);
+by( strip_tac1 2);
+by( EVERY[dtac spec 2, dtac spec 2, dtac spec 2, mp_tac 2]);
+by( fast_tac (HOL_cs addEs [widen_trans]) 2);
+by( strip_tac1 1);
+by( dtac subcls1D 1);
+by( strip_tac1 1);
+by( stac cmethd_rec 1);
+by( atac 1);
+by( rewtac override_def);
+by( asm_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
+by( case_tac "\\<exists>z. map_of(map (\\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z" 1);
+by( etac exE 1);
+by( asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 2);
+by( ALLGOALS (rotate_tac ~1 THEN' forward_tac[ssubst] THEN' (fn n=>atac(n+1))));
+by( ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex])));
+by( dtac class_wf 1);
+by( atac 1);
+by( split_all_tac 1);
+by( rewtac wf_cdecl_def);
+by( dtac table_mapf_Some2 1);
+by( Clarsimp_tac 1);
+by( dres_inst_tac [("xys1","ms")] get_in_set 1);
+by Auto_tac;
+qed_spec_mp "subcls_widen_methd";
+
+
+Goal
+ "\\<lbrakk> G\\<turnstile>Class C\\<preceq>Class D; wf_prog wt G; \
+\ cmethd (G,D) sig = Some (md, rT, b) \\<rbrakk> \
+\ \\<Longrightarrow> \\<exists>mD' rT' b'. cmethd (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
+by(auto_tac (claset() addSDs [widen_Class_Class]
+ addDs [subcls_widen_methd,cmethd_wf_mdecl],
+ simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
+qed "subtype_widen_methd";
+
+
+Goal "wf_prog wt G \\<Longrightarrow> \\<forall>D. cmethd (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> cmethd (G,D) sig = Some(D,mh,code)";
+by( case_tac "is_class G C" 1);
+by( forw_inst_tac [("C","C")] cmethd_rec 2);
+by( asm_full_simp_tac (simpset() addsimps [is_class_def]
+ delsimps [not_None_eq]) 2);
+by (etac subcls1_induct 1);
+ ba 1;
+ by (Asm_full_simp_tac 1);
+by (stac cmethd_rec 1);
+ ba 1;
+by (Clarify_tac 1);
+by (eres_inst_tac [("x","Da")] allE 1);
+by (Clarsimp_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);
+ by (Clarify_tac 1);
+ by (stac cmethd_rec 1);
+ ba 1;
+ by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);
+qed_spec_mp "cmethd_in_md";
+
+writeln"OK";
+
+Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
+\ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
+by( etac subcls1_induct 1);
+by( atac 1);
+by( Asm_simp_tac 1);
+by( strip_tac1 1);
+by( stac fields_rec 1);
+by( atac 1);
+by( atac 1);
+by( Asm_simp_tac 1);
+by( safe_tac set_cs);
+by( Fast_tac 2);
+by( dtac class_wf 1);
+by( atac 1);
+by( rewtac wf_cdecl_def);
+by( Asm_full_simp_tac 1);
+by( strip_tac1 1);
+by( EVERY[dtac bspec 1, atac 1]);
+by( rewtac wf_fdecl_def);
+by( split_all_tac 1);
+by( Asm_full_simp_tac 1);
+val is_type_fields = result() RS bspec;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/WellForm.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,47 @@
+(* Title: HOL/MicroJava/J/WellForm.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+
+Well-formedness of Java programs
+for static checks on expressions and statements, see WellType.thy
+
+improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
+* a method implementing or overwriting another method may have a result type
+ that widens to the result type of the other method (instead of identical type)
+
+simplifications:
+* for uniformity, Object is assumed to be declared like any other class
+*)
+
+WellForm = TypeRel +
+
+types 'c wtm = 'c prog => cname => 'c mdecl => bool
+
+constdefs
+
+ wf_fdecl :: "'c prog \\<Rightarrow> fdecl \\<Rightarrow> bool"
+"wf_fdecl G \\<equiv> \\<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_mdecl :: "'c wtm \\<Rightarrow> 'c wtm"
+"wf_mdecl wtm G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wtm G C (sig,rT,mb)"
+
+ wf_cdecl :: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
+"wf_cdecl wtm G \\<equiv>
+ \\<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 wtm G C m) \\<and> unique ms \\<and>
+ (case sc of None \\<Rightarrow> C = Object
+ | Some D \\<Rightarrow>
+ is_class G D \\<and> \\<not> G\\<turnstile>D\\<prec>C C \\<and>
+ (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
+ cmethd(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
+
+ wf_prog :: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> bool"
+"wf_prog wtm G \\<equiv>
+ let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wtm G c) \\<and> unique G"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/WellType.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,61 @@
+(* Title: HOL/MicroJava/J/WellType.ML
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+Goalw [m_head_def]
+"\\<lbrakk> m_head G T sig = Some (md,rT); wf_prog wtm G; G\\<turnstile>Class T''\\<preceq>RefT T\\<rbrakk> \\<Longrightarrow> \
+\\\<exists>md' rT' b'. cmethd (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
+by( forward_tac [widen_Class_RefT] 1);
+by( etac exE 1);
+by( hyp_subst_tac 1);
+by( asm_full_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
+by( rewtac option_map_def);
+by( strip_tac1 1);
+by( split_all_tac 1);
+by( dtac widen_Class_Class 1);
+by( etac disjE 1);
+by( hyp_subst_tac 1);
+by( asm_full_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
+by( dtac subcls_widen_methd 1);
+by Auto_tac;
+qed "widen_methd";
+
+
+Goal
+"\\<lbrakk>m_head G T sig = Some (md,rT); G\\<turnstile>Class T''\\<preceq>RefT T; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
+\ \\<exists>T' rT' b. cmethd (G,T'') sig = Some (T',rT',b) \\<and> \
+\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>Class T''\\<preceq>Class T' \\<and> wf_mhead G sig rT' \\<and> wtm G T' (sig,rT',b)";
+by( dtac widen_methd 1);
+by( atac 1);
+by( atac 1);
+by( Clarsimp_tac 1);
+by( dtac cmethd_wf_mdecl 1);
+by( atac 1);
+by( rewtac wf_mdecl_def);
+by Auto_tac;
+val Call_lemma = result();
+
+
+val m_head_Object = prove_goalw thy [m_head_def]
+"\\<And>x. wf_prog wtm G \\<Longrightarrow> m_head G (ClassT Object) sig = None" (K [Asm_simp_tac 1]);
+
+Addsimps [m_head_Object];
+
+val max_spec2appl_meths = prove_goalw thy [max_spec_def]
+ "x \\<in> max_spec G rT sig \\<longrightarrow> x \\<in> appl_methds G rT sig"
+ (fn _ => [Fast_tac 1]) RS mp;
+
+val appl_methsD = prove_goalw thy [appl_methds_def]
+"(mh,pTs')\\<in>appl_methds G rT (mn, pTs) \\<longrightarrow> \
+\ m_head G rT (mn, pTs') = Some mh \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
+ (K [Fast_tac 1]) RS mp;
+
+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 [
+ rtac val_.induct 1,
+ Fast_tac 5,
+ ALLGOALS Simp_tac]) RS mp;
+
+Addsimps [is_type_typeof];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/WellType.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,184 @@
+(* Title: HOL/MicroJava/J/WellType.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+
+Well-typedness of Java programs
+
+the formulation of well-typedness of method calls given below (as well as
+the Java Specification 1.0) is a little too restrictive: Is does not allow
+methods of class Object to be called upon references of interface type.
+
+simplifications:
+* the type rules include all static checks on expressions and statements, e.g.
+ definedness of names (of parameters, locals, fields, methods)
+
+*)
+
+WellType = Term + WellForm +
+
+types lenv (* local variables, including method parameters and This *)
+ = "vname \\<leadsto> ty"
+ 'c env
+ = "'c prog \\<times> lenv"
+
+syntax
+
+ prg :: "'c env \\<Rightarrow> 'c prog"
+ localT :: "'c env \\<Rightarrow> (vname \\<leadsto> ty)"
+
+translations
+
+ "prg" => "fst"
+ "localT" => "snd"
+
+consts
+
+ more_spec :: "'c prog \\<Rightarrow> (ty \\<times> 'x) \\<times> ty list \\<Rightarrow>
+ (ty \\<times> 'x) \\<times> ty list \\<Rightarrow> bool"
+ m_head :: "'c prog \\<Rightarrow> ref_ty \\<Rightarrow> sig \\<Rightarrow> (ty \\<times> ty) option"
+ appl_methds :: "'c prog \\<Rightarrow> ref_ty \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
+ max_spec :: "'c prog \\<Rightarrow> ref_ty \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
+
+defs
+
+ m_head_def "m_head G t sig \\<equiv> case t of NullT \\<Rightarrow> None | ClassT C \\<Rightarrow>
+ option_map (\\<lambda>(md,(rT,mb)). (Class md,rT)) (cmethd (G,C) sig)"
+
+ more_spec_def "more_spec G \\<equiv> \\<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 T \\<equiv> \\<lambda>(mn, pTs). {(mh,pTs') |mh pTs'.
+ m_head G T (mn, pTs') = Some mh \\<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 rT sig \\<equiv> {m. m \\<in>appl_methds G rT sig \\<and>
+ (\\<forall>m'\\<in>appl_methds G rT sig.
+ more_spec G m' m \\<longrightarrow> m' = m)}"
+consts
+
+ typeof :: "(loc \\<Rightarrow> ty option) \\<Rightarrow> val \\<Rightarrow> ty option"
+
+primrec
+ "typeof dt Unit = Some (PrimT Void)"
+ "typeof dt Null = Some NT"
+ "typeof dt (Bool b) = Some (PrimT Boolean)"
+ "typeof dt (Intg i) = Some (PrimT Integer)"
+ "typeof dt (Addr a) = dt a"
+
+types
+ javam = "vname list \\<times> (vname \\<times> ty) list \\<times> stmt \\<times> expr"
+ (* method body with parameter names, local variables, block, result expression *)
+
+consts
+
+ ty_expr :: "javam env \\<Rightarrow> (expr \\<times> ty ) set"
+ ty_exprs:: "javam env \\<Rightarrow> (expr list \\<times> ty list) set"
+ wt_stmt :: "javam env \\<Rightarrow> stmt set"
+
+syntax
+
+ty_expr :: "javam env \\<Rightarrow> [expr , ty ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Colon>_" [51,51,51]50)
+ty_exprs:: "javam env \\<Rightarrow> [expr list, ty list] \\<Rightarrow> bool" ("_\\<turnstile>_[\\<Colon>]_"[51,51,51]50)
+wt_stmt :: "javam env \\<Rightarrow> stmt \\<Rightarrow> 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>c \\<surd>" == "c \\<in> wt_stmt E"
+
+inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intrs
+
+(* well-typed expressions *)
+
+ (* cf. 15.8 *)
+ NewC "\\<lbrakk>is_class (prg E) C\\<rbrakk> \\<Longrightarrow>
+ E\\<turnstile>NewC C\\<Colon>Class C"
+
+ (* cf. 15.15 *)
+ Cast "\\<lbrakk>E\\<turnstile>e\\<Colon>T;
+ prg E\\<turnstile>T\\<Rightarrow>? T'\\<rbrakk> \\<Longrightarrow>
+ E\\<turnstile>Cast T' e\\<Colon>T'"
+
+ (* cf. 15.7.1 *)
+ Lit "\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow>
+ E\\<turnstile>Lit x\\<Colon>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"
+
+ (* 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'"
+
+ (* cf. 15.10.1 *)
+ FAcc "\\<lbrakk>E\\<turnstile>a\\<Colon>Class C;
+ cfield (prg E,C) fn = Some (fd,fT)\\<rbrakk> \\<Longrightarrow>
+ E\\<turnstile>{fd}a..fn\\<Colon>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\\<in>=v\\<Colon>T'"
+
+
+ (* cf. 15.11.1, 15.11.2, 15.11.3 *)
+ Call "\\<lbrakk>E\\<turnstile>a\\<Colon>RefT t;
+ E\\<turnstile>ps[\\<Colon>]pTs;
+ max_spec (prg E) t (mn, pTs) = {((md,rT),pTs')}\\<rbrakk> \\<Longrightarrow>
+ E\\<turnstile>a..mn({pTs'}ps)\\<Colon>rT"
+
+(* well-typed expression lists *)
+
+ (* cf. 15.11.??? *)
+ Nil "E\\<turnstile>[][\\<Colon>][]"
+
+ (* cf. 15.11.??? *)
+ Cons "\\<lbrakk>E\\<turnstile>e\\<Colon>T;
+ E\\<turnstile>es[\\<Colon>]Ts\\<rbrakk> \\<Longrightarrow>
+ E\\<turnstile>e#es[\\<Colon>]T#Ts"
+
+(* well-typed statements *)
+
+ Skip "E\\<turnstile>Skip\\<surd>"
+
+ Expr "\\<lbrakk>E\\<turnstile>e\\<Colon>T\\<rbrakk> \\<Longrightarrow>
+ E\\<turnstile>Expr e\\<surd>"
+
+ Comp "\\<lbrakk>E\\<turnstile>s1\\<surd>;
+ E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
+ E\\<turnstile>s1;; s2\\<surd>"
+
+ (* cf. 14.8 *)
+ Cond "\\<lbrakk>E\\<turnstile>e\\<Colon>PrimT Boolean;
+ E\\<turnstile>s1\\<surd>;
+ E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
+ 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>
+ E\\<turnstile>While(e) s\\<surd>"
+
+constdefs
+
+ wt_java_mdecl :: javam prog => cname => javam mdecl => bool
+"wt_java_mdecl G C \\<equiv> \\<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))"
+
+ wf_java_prog :: javam prog => bool
+"wf_java_prog G \\<equiv> wf_prog wt_java_mdecl G"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/Control.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,26 @@
+(* Title: HOL/MicroJava/JVM/Control.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+
+(Un)conditional branch instructions
+*)
+
+Control = JVMState +
+
+datatype branch = Goto int
+ | Ifcmpeq int (** Branch if int/ref comparison succeeds **)
+
+
+consts
+ exec_br :: "[branch,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)"
+
+primrec
+ "exec_br (Ifcmpeq i) stk pc =
+ (let (val1,val2) = (hd stk, hd (tl stk));
+ pc' = if val1 = val2 then nat(int pc+i) else pc+1
+ in
+ (tl (tl stk),pc'))"
+ "exec_br (Goto i) stk pc = (stk, nat(int pc+i))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,72 @@
+(* Title: HOL/MicroJava/JVM/JVMExec.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+
+Execution of the JVM
+*)
+
+JVMExec = LoadAndStore + Object + Method + Opstack + Control +
+
+datatype
+ instr = LS load_and_store
+ | CO create_object
+ | MO manipulate_object
+ | CH check_object
+ | MI meth_inv
+ | MR
+ | OS op_stack
+ | BR branch
+
+types
+ bytecode = instr list
+ jvm_prog = "(nat \\<times> bytecode)prog"
+
+consts
+ exec :: "jvm_prog \\<times> jvm_state \\<Rightarrow> jvm_state option"
+
+(** exec is not recursive. recdef is just used because for pattern matching **)
+recdef exec "{}"
+ "exec (G, xp, hp, []) = None"
+
+ "exec (G, None, hp, (stk,loc,cn,ml,pc)#frs) =
+ Some (case snd(snd(snd(the(cmethd (G,cn) ml)))) ! pc of
+ LS ins \\<Rightarrow> (let (stk',loc',pc') = exec_las ins stk loc pc
+ in
+ (None,hp,(stk',loc',cn,ml,pc')#frs))
+
+ | CO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_co ins G hp stk pc
+ in
+ (xp',hp',(stk',loc,cn,ml,pc')#frs))
+
+ | MO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_mo ins hp stk pc
+ in
+ (xp',hp',(stk',loc,cn,ml,pc')#frs))
+
+ | CH ins \\<Rightarrow> (let (xp',stk',pc') = exec_ch ins G hp stk pc
+ in
+ (xp',hp,(stk',loc,cn,ml,pc')#frs))
+
+ | MI ins \\<Rightarrow> (let (xp',frs',stk',pc') = exec_mi ins G hp stk pc
+ in
+ (xp',hp,frs'@(stk',loc,cn,ml,pc')#frs))
+
+ | MR \\<Rightarrow> (let frs' = exec_mr stk frs in
+ (None,hp,frs'))
+
+ | OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc
+ in
+ (None,hp,(stk',loc,cn,ml,pc')#frs))
+
+ | BR ins \\<Rightarrow> (let (stk',pc') = exec_br ins stk pc
+ in
+ (None,hp,(stk',loc,cn,ml,pc')#frs)))"
+
+ "exec (G, Some xp, hp, f#frs) = Some (Some xp, hp, [])"
+
+
+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}^*"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/JVMState.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,61 @@
+(* Title: HOL/MicroJava/JVM/JVMState.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+
+State of the JVM
+*)
+
+JVMState = Store +
+
+
+(** frame stack **)
+
+types
+ opstack = "val list"
+ locvars = "val list"
+ p_count = nat
+
+ frame = "opstack \\<times>
+ locvars \\<times>
+ cname \\<times>
+ sig \\<times>
+ p_count"
+
+ (* operand stack *)
+ (* local variables *)
+ (* name of def. class defined *)
+ (* meth name+param_desc *)
+ (* program counter within frame *)
+
+
+(** exceptions **)
+
+constdefs
+ raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option"
+"raise_xcpt c x \\<equiv> (if c then Some x else None)"
+
+ heap_update :: "[xcpt option,aheap,aheap] \\<Rightarrow> aheap"
+"heap_update xp hp' hp \\<equiv> if xp=None then hp' else hp"
+
+ stk_update :: "[xcpt option,opstack,opstack] \\<Rightarrow> opstack"
+"stk_update xp stk' stk \\<equiv> if xp=None then stk' else stk"
+
+ xcpt_update :: "[xcpt option,'a,'a] \\<Rightarrow> 'a"
+"xcpt_update xp y' y \\<equiv> if xp=None then y' else y"
+
+(** runtime state **)
+
+types
+ jvm_state = "xcpt option \\<times>
+ aheap \\<times>
+ frame list"
+
+
+
+(** dynamic method lookup **)
+
+constdefs
+ dyn_class :: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname"
+"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(cmethd(G,C) sig))"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/LoadAndStore.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,32 @@
+(* Title: HOL/MicroJava/JVM/LoadAndStore.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+
+Load and store instructions
+*)
+
+LoadAndStore = JVMState +
+
+(** load and store instructions transfer values between local variables
+ and operand stack. Values must all be of the same size (or tagged) **)
+
+datatype load_and_store =
+ Load nat (* load from local variable *)
+| Store nat (* store into local variable *)
+| Bipush int (* push int *)
+| Aconst_null (* push null *)
+
+
+consts
+ exec_las :: "[load_and_store,opstack,locvars,p_count] \\<Rightarrow> (opstack \\<times> locvars \\<times> p_count)"
+primrec
+ "exec_las (Load idx) stk vars pc = ((vars ! idx) # stk , vars , pc+1)"
+
+ "exec_las (Store idx) stk vars pc = (tl stk , vars[idx:=hd stk] , pc+1)"
+
+ "exec_las (Bipush ival) stk vars pc = (Intg ival # stk , vars , pc+1)"
+
+ "exec_las Aconst_null stk vars pc = (Null # stk , vars , pc+1)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/Method.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,7 @@
+(* Title: HOL/MicroJava/JVM/Method.ML
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+Addsimps [exec_mr_def];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/Method.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,41 @@
+(* Title: HOL/MicroJava/JVM/Method.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+
+Method invocation
+*)
+
+Method = JVMState +
+
+(** method invocation and return instructions **)
+
+datatype
+ meth_inv =
+ Invokevirtual mname (ty list) (** inv. instance meth of an object **)
+
+consts
+ exec_mi :: "[meth_inv,(nat \\<times> 'c)prog,aheap,opstack,p_count]
+ \\<Rightarrow> (xcpt option \\<times> frame list \\<times> opstack \\<times> p_count)"
+primrec
+ "exec_mi (Invokevirtual mn ps) G hp stk pc =
+ (let n = length ps;
+ argsoref = take (n+1) stk;
+ oref = last argsoref;
+ xp' = raise_xcpt (oref=Null) NullPointer;
+ dynT = fst(hp \\<And> (the_Addr oref));
+ (dc,mh,mxl,c)= the (cmethd (G,dynT) (mn,ps));
+ frs' = xcpt_update xp' [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] []
+ in
+ (xp' , frs' , drop (n+1) stk , pc+1))"
+
+
+constdefs
+ exec_mr :: "[opstack,frame list] \\<Rightarrow> frame list"
+"exec_mr stk0 frs \\<equiv>
+ (let val = hd stk0;
+ (stk,loc,cn,met,pc) = hd frs
+ in
+ (val#stk,loc,cn,met,pc)#tl frs)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/Object.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,73 @@
+(* Title: HOL/MicroJava/JVM/Object.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+
+Get and putfield instructions
+*)
+
+Object = JVMState +
+
+datatype
+ create_object = New cname
+
+consts
+ exec_co :: "[create_object,'code prog,aheap,opstack,p_count] \\<Rightarrow>
+ (xcpt option \\<times> aheap \\<times> opstack \\<times> p_count)"
+
+
+primrec
+ "exec_co (New C) G hp stk pc =
+ (let xp' = raise_xcpt (\\<forall>x. hp x \\<noteq> None) OutOfMemory;
+ oref = newref hp;
+ fs = init_vars (fields(G,C));
+ hp' = xcpt_update xp' (hp(oref \\<mapsto> (C,fs))) hp;
+ stk' = xcpt_update xp' ((Addr oref)#stk) stk
+ in (xp' , hp' , stk' , pc+1))"
+
+
+datatype
+ manipulate_object =
+ Getfield vname cname (* Fetch field from object *)
+ | Putfield vname cname (* Set field in object *)
+
+consts
+ exec_mo :: "[manipulate_object,aheap,opstack,p_count] \\<Rightarrow>
+ (xcpt option \\<times> aheap \\<times> opstack \\<times> p_count)"
+
+primrec
+ "exec_mo (Getfield F C) hp stk pc =
+ (let oref = hd stk;
+ xp' = raise_xcpt (oref=Null) NullPointer;
+ (oc,fs) = hp \\<And> (the_Addr oref);
+ stk' = xcpt_update xp' ((fs\\<And>(F,C))#(tl stk)) (tl stk)
+ in
+ (xp' , hp , stk' , pc+1))"
+
+ "exec_mo (Putfield F C) hp stk pc =
+ (let (fval,oref)= (hd stk, hd(tl stk));
+ xp' = raise_xcpt (oref=Null) NullPointer;
+ a = the_Addr oref;
+ (oc,fs) = hp \\<And> a;
+ hp' = xcpt_update xp' (hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval)))) hp
+ in
+ (xp' , hp' , tl (tl stk), pc+1))"
+
+
+datatype
+ check_object =
+ Checkcast cname (* Check whether object is of given type *)
+
+consts
+ exec_ch :: "[check_object,'code prog,aheap,opstack,p_count]
+ \\<Rightarrow> (xcpt option \\<times> opstack \\<times> p_count)"
+
+primrec
+ "exec_ch (Checkcast C) G hp stk pc =
+ (let oref = hd stk;
+ xp' = raise_xcpt (\\<not> cast_ok G (Class C) hp oref) ClassCast;
+ stk' = xcpt_update xp' stk (tl stk)
+ in
+ (xp' , stk' , pc+1))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/Opstack.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,38 @@
+(* Title: HOL/MicroJava/JVM/Opstack.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+
+Manipulation of operand stack
+*)
+
+Opstack = JVMState +
+
+(** instructions for the direct manipulation of the operand stack **)
+
+datatype
+ op_stack =
+ Pop
+ | Dup
+ | Dup_x1
+ | Dup_x2
+ | Swap
+
+consts
+ exec_os :: "[op_stack,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)"
+
+primrec
+ "exec_os Pop stk pc = (tl stk , pc+1)"
+
+ "exec_os Dup stk pc = (hd stk # stk , pc+1)"
+
+ "exec_os Dup_x1 stk pc = (hd stk # hd (tl stk) # hd stk # (tl (tl stk)) , pc+1)"
+
+ "exec_os Dup_x2 stk pc = (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))) , pc+1)"
+
+ "exec_os Swap stk pc =
+ (let (val1,val2) = (hd stk,hd (tl stk))
+ in
+ (val2#val1#(tl (tl stk)) , pc+1))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/Store.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,10 @@
+(* Title: HOL/MicroJava/JVM/Store.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+Goalw [newref_def]
+ "hp x = None \\<longrightarrow> hp (newref hp) = None";
+by (fast_tac (claset() addIs [selectI2EX] addss (simpset())) 1);
+qed_spec_mp "newref_None";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/Store.thy Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,23 @@
+(* Title: HOL/MicroJava/JVM/Store.thy
+ ID: $Id$
+ Author: Cornelia Pusch
+ Copyright 1999 Technische Universitaet Muenchen
+
+The store.
+
+The JVM builds on many notions already defined in Java.
+Conform provides notions for the type safety proof of the Bytecode Verifier.
+*)
+
+Store = Conform +
+
+syntax
+ value :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ \\<And> _")
+translations
+ "t \\<And> x" == "the (t x)"
+
+constdefs
+ newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"
+ "newref s \\<equiv> \\<epsilon>v. s v = None"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/ROOT.ML Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,12 @@
+goals_limit:=1;
+
+Unify.search_bound := 40;
+Unify.trace_bound := 40;
+
+add_path "J";
+add_path "JVM";
+add_path "BV";
+
+
+use_thy "JTypeSafe";
+use_thy "BVSpecTypeSafe";