# HG changeset patch # User oheimb # Date 976126174 -3600 # Node ID 779af7c5874354f9cc9dbe2b2d202e157f2a2c4b # Parent e460c53c1c9b9722f87fda491625b36709e20cc2 improved superclass entry for classes and definition status of is_class, class corrected recursive definitions of "method" and "fields" Beware: some proofs are incomplete (sorry, oops), preliminary comments with DvO: diff -r e460c53c1c9b -r 779af7c58743 src/HOL/MicroJava/BV/BVSpec.thy --- a/src/HOL/MicroJava/BV/BVSpec.thy Wed Dec 06 19:05:50 2000 +0100 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Wed Dec 06 19:09:34 2000 +0100 @@ -38,17 +38,19 @@ "wt_jvm_prog G phi ==> (\wt. wf_prog wt G)" by (unfold wt_jvm_prog_def, blast) -lemma wt_jvm_prog_impl_wt_instr: -"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] +lemma wt_jvm_prog_impl_wt_instr: (* DvO: is_class G C eingefügt *) +"[| wt_jvm_prog G phi; is_class G C; + method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"; by (unfold wt_jvm_prog_def, drule method_wf_mdecl, - simp, simp add: wf_mdecl_def wt_method_def) + simp, simp, simp add: wf_mdecl_def wt_method_def) -lemma wt_jvm_prog_impl_wt_start: -"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> +lemma wt_jvm_prog_impl_wt_start: (* DvO: is_class G C eingefügt *) +"[| wt_jvm_prog G phi; is_class G C; + method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> 0 < (length ins) \ wt_start G C (snd sig) maxl (phi C sig)" by (unfold wt_jvm_prog_def, drule method_wf_mdecl, - simp, simp add: wf_mdecl_def wt_method_def) + simp, simp, simp add: wf_mdecl_def wt_method_def) text {* for most instructions wt\_instr collapses: *} lemma diff -r e460c53c1c9b -r 779af7c58743 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Dec 06 19:05:50 2000 +0100 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Dec 06 19:09:34 2000 +0100 @@ -17,7 +17,7 @@ lemmas [simp del] = split_paired_All lemma wt_jvm_prog_impl_wt_instr_cor: - "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); + "[| wt_jvm_prog G phi;is_class G C; method (G,C) sig = Some (C,rT,maxs,maxl,ins); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" apply (unfold correct_state_def Let_def correct_frame_def) @@ -195,7 +195,7 @@ G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def defs1 - fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def + fun_upd_apply map_eq_Cons raise_xcpt_def init_vars_def split: option.split) apply (force dest!: iffD1 [OF collapse_paired_All] intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap @@ -205,7 +205,7 @@ hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref correct_init_obj simp add: NT_subtype_conv approx_val_def conf_def defs1 - fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def + fun_upd_apply map_eq_Cons raise_xcpt_def init_vars_def split: option.split) done @@ -214,8 +214,8 @@ lemmas [simp del] = split_paired_Ex -lemma Invoke_correct: -"[| wt_jvm_prog G phi; +lemma Invoke_correct: (* DvO: is_class G C' eingefügt *) +"[| wt_jvm_prog G phi; is_class G C'; method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins ! pc = Invoke C' mn pTs; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; @@ -224,6 +224,7 @@ ==> G,phi \JVM state'\" proof - assume wtprog: "wt_jvm_prog G phi" + assume is_class: "is_class G C'" assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)" assume ins: "ins ! pc = Invoke C' mn pTs" assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" @@ -324,7 +325,7 @@ by - (drule widen_Class, elim, rule that) with X - have "G \ X' \C C'" + have X'_subcls: "G \ X' \C C'" by simp with mC' wfprog @@ -333,7 +334,7 @@ by (auto dest: subtype_widen_methd intro: that) from X' D - have "G \ D \C X'" + have D_subcls: "G \ D \C X'" by simp with wfprog mX @@ -346,10 +347,14 @@ have rT': "G \ rT' \ rT" by - (rule widen_trans) - from mD wfprog + from is_class X'_subcls D_subcls + have is_class_D: "is_class G D" + by (auto dest: subcls_is_class2) + + with mD wfprog obtain mD'': "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins')" - "is_class G D''" + "is_class G D''" by (auto dest: method_in_md) from loc obj_ty @@ -385,7 +390,7 @@ by (simp add: approx_loc_def approx_val_Err list_all2_def set_replicate_conv_if) - from wfprog mD + from wfprog mD is_class_D have "G \ Class D \ Class D''" by (auto dest: method_wf_mdecl) with obj_ty loc @@ -460,6 +465,8 @@ ==> G,phi \JVM state'\" apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm) apply (frule wt_jvm_prog_impl_wt_instr) +sorry +(* apply (assumption, erule Suc_lessD) apply (unfold wt_jvm_prog_def) apply (fastsimp @@ -468,6 +475,7 @@ intro: conf_widen simp: approx_val_def append_eq_conv_conj map_eq_Cons defs1) done +*) lemmas [simp] = map_append @@ -595,9 +603,12 @@ G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" apply (frule wt_jvm_prog_impl_wt_instr_cor) +sorry +(* apply assumption+ apply (cases "ins!pc") prefer 9 + apply (blast intro: Invoke_correct) prefer 9 apply (blast intro: Return_correct) @@ -608,7 +619,7 @@ Goto_correct Ifcmpeq_correct Pop_correct Dup_correct Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+ done - +*) (** Main **) diff -r e460c53c1c9b -r 779af7c58743 src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Wed Dec 06 19:05:50 2000 +0100 +++ b/src/HOL/MicroJava/BV/Correct.thy Wed Dec 06 19:09:34 2000 +0100 @@ -244,7 +244,7 @@ G,h \ (C, map_of (map (\(f,fT).(f,default_val fT)) (fields(G,C)))) \" apply (unfold oconf_def lconf_def) apply (simp add: map_of_map) -apply (force intro: defval_conf dest: map_of_SomeD is_type_fields) +apply (force intro: defval_conf dest: map_of_SomeD fields_is_type) done diff -r e460c53c1c9b -r 779af7c58743 src/HOL/MicroJava/BV/JType.thy --- a/src/HOL/MicroJava/BV/JType.thy Wed Dec 06 19:05:50 2000 +0100 +++ b/src/HOL/MicroJava/BV/JType.thy Wed Dec 06 19:09:34 2000 +0100 @@ -68,7 +68,7 @@ moreover from R wf ty have "R \ ClassT Object \ ?thesis" - by (auto simp add: is_ty_def subcls1_def is_class_def class_def + by (auto simp add: is_ty_def subcls1_def elim: converse_rtranclE split: ref_ty.splits) ultimately diff -r e460c53c1c9b -r 779af7c58743 src/HOL/MicroJava/BV/JVM.thy --- a/src/HOL/MicroJava/BV/JVM.thy Wed Dec 06 19:05:50 2000 +0100 +++ b/src/HOL/MicroJava/BV/JVM.thy Wed Dec 06 19:09:34 2000 +0100 @@ -179,7 +179,7 @@ apply (drule method_wf_mdecl, assumption) apply (simp add: wf_mdecl_def wf_mhead_def) - apply (drule is_type_fields) + apply (drule fields_is_type) apply assumption apply (subgoal_tac "((vname, cname), vT) \ set (fields (S, cname))") apply assumption diff -r e460c53c1c9b -r 779af7c58743 src/HOL/MicroJava/BV/LBVComplete.thy --- a/src/HOL/MicroJava/BV/LBVComplete.thy Wed Dec 06 19:05:50 2000 +0100 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy Wed Dec 06 19:09:34 2000 +0100 @@ -427,17 +427,15 @@ assume wfprog: "wf_prog (\G C (sig,rT,mxs,mxl,b). wt_method G C (snd sig) rT mxs mxl b (Phi C sig)) G" - thus ?thesis + thus ?thesis (* DvO: braucht ewig :-( *) proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto) fix a aa ab b ac ba ad ae af bb - assume 1 : "\(C,sc,fs,ms)\set G. - Ball (set fs) (wf_fdecl G) \ - unique fs \ + assume 1 : "\(C,D,fs,ms)\set G. + Ball (set fs) (wf_fdecl G) \ unique fs \ (\(sig,rT,mb)\set ms. wf_mhead G sig rT \ (\(mxs,mxl,b). wt_method G C (snd sig) rT mxs mxl b (Phi C sig)) mb) \ unique ms \ - (case sc of None => C = Object - | Some D => + (C \ Object \ is_class G D \ (D, C) \ (subcls1 G)^* \ (\(sig,rT,b)\set ms. @@ -456,15 +454,18 @@ from m b show ?thesis proof (rule bspec [elim_format], clarsimp) - assume "wt_method G a ba ad ae af bb (Phi a (ac, ba))" + assume "wt_method G a ba ad ae af bb (Phi a (ac, ba))" with wfprog uG ub b 1 show ?thesis by - (rule wtl_method_complete [elim_format], assumption+, simp add: make_Cert_def unique_epsilon unique_epsilon') qed +oops +(* qed qed qed +*) lemmas [simp] = split_paired_Ex diff -r e460c53c1c9b -r 779af7c58743 src/HOL/MicroJava/BV/LBVCorrect.thy --- a/src/HOL/MicroJava/BV/LBVCorrect.thy Wed Dec 06 19:05:50 2000 +0100 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Wed Dec 06 19:09:34 2000 +0100 @@ -282,6 +282,7 @@ theorem wtl_correct: "wtl_jvm_prog G cert ==> \ Phi. wt_jvm_prog G Phi" +(* proof (clarsimp simp add: wt_jvm_prog_def wf_prog_def, intro conjI) assume wtl_prog: "wtl_jvm_prog G cert" @@ -300,6 +301,10 @@ in SOME phi. wt_method G C (snd sig) rT maxs maxl b phi" from wtl_prog show "?Q ?Phi" +*) +sorry +(* +DvO: hier beginnt die Maschine wie blöd zu swappen proof (unfold wf_cdecl_def, intro) fix x a b aa ba ab bb m assume 1: "x \ set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \ set bb" @@ -328,6 +333,6 @@ qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def) qed qed - +*) end diff -r e460c53c1c9b -r 779af7c58743 src/HOL/MicroJava/BV/StepMono.thy --- a/src/HOL/MicroJava/BV/StepMono.thy Wed Dec 06 19:05:50 2000 +0100 +++ b/src/HOL/MicroJava/BV/StepMono.thy Wed Dec 06 19:09:34 2000 +0100 @@ -174,7 +174,7 @@ "is_class G cname" and oT: "G\ oT\ (Class cname)" and vT: "G\ vT\ b" - by simp (elim exE conjE, rule that) + by force moreover from s1 G obtain vT' oT' ST' LT'