# HG changeset patch # User streckem # Date 1053966975 -7200 # Node ID a34d89ce6097adefbfb422fe6215e5f01c2c17bd # Parent bbd2f7b007364abf1a913025b242f20c8f400e54 Introduced distinction wf_prog vs. ws_prog diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/BV/Altern.thy --- a/src/HOL/MicroJava/BV/Altern.thy Mon May 26 11:42:41 2003 +0200 +++ b/src/HOL/MicroJava/BV/Altern.thy Mon May 26 18:36:15 2003 +0200 @@ -1,3 +1,13 @@ +(* Title: HOL/MicroJava/BV/Altern.thy + ID: $Id$ + Author: Martin Strecker + Copyright GPL 2003 +*) + + +(* Alternative definition of well-typing of bytecode, + used in compiler type correctness proof *) + theory Altern = BVSpec: diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/BV/BVExample.thy --- a/src/HOL/MicroJava/BV/BVExample.thy Mon May 26 11:42:41 2003 +0200 +++ b/src/HOL/MicroJava/BV/BVExample.thy Mon May 26 18:36:15 2003 +0200 @@ -186,6 +186,7 @@ text {* The program is structurally wellformed: *} + lemma wf_struct: "wf_prog (\G C mb. True) E" (is "wf_prog ?mb E") proof - @@ -223,7 +224,8 @@ apply (auto simp add: name_defs distinct_classes distinct_fields) done ultimately - show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def) + show ?thesis + by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def) qed section "Welltypings" diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/BV/BVNoTypeError.thy --- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Mon May 26 11:42:41 2003 +0200 +++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Mon May 26 18:36:15 2003 +0200 @@ -299,9 +299,10 @@ have "\D vs. hp (the_Addr v) = Some (D,vs) \ G \ D \C C" by (auto dest!: non_np_objD) } - ultimately show ?thesis using Getfield field class stk hconf + ultimately show ?thesis using Getfield field class stk hconf wf apply clarsimp - apply (fastsimp dest!: hconfD widen_cfs_fields [OF _ _ wf] oconf_objD) + apply (fastsimp intro: wf_prog_ws_prog + dest!: hconfD widen_cfs_fields oconf_objD) done next case (Putfield F C) diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Mon May 26 11:42:41 2003 +0200 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Mon May 26 18:36:15 2003 +0200 @@ -677,6 +677,7 @@ apply (rule conjI) apply (drule widen_cfs_fields) apply assumption+ + apply (erule wf_prog_ws_prog) apply (erule conf_widen) prefer 2 apply assumption @@ -772,7 +773,8 @@ moreover from wf hp heap_ok is_class_X have hp': "G \h ?hp' \" - by - (rule hconf_newref, auto simp add: oconf_def dest: fields_is_type) + by - (rule hconf_newref, + auto simp add: oconf_def dest: fields_is_type) moreover from hp have sup: "hp \| ?hp'" by (rule hext_new) @@ -915,7 +917,7 @@ obtain mD'': "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')" "is_class G D''" - by (auto dest: method_in_md) + by (auto dest: wf_prog_ws_prog [THEN method_in_md]) from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def) @@ -1319,7 +1321,9 @@ shows hconf_start: "\ \h (start_heap \) \" apply (unfold hconf_def start_heap_def) apply (auto simp add: fun_upd_apply blank_def oconf_def split: split_if_asm) - apply (simp add: fields_is_type [OF _ wf is_class_xcpt [OF wf]])+ + apply (simp add: fields_is_type + [OF _ wf [THEN wf_prog_ws_prog] + is_class_xcpt [OF wf [THEN wf_prog_ws_prog]]])+ done lemma diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/BV/JType.thy --- a/src/HOL/MicroJava/BV/JType.thy Mon May 26 11:42:41 2003 +0200 +++ b/src/HOL/MicroJava/BV/JType.thy Mon May 26 18:36:15 2003 +0200 @@ -51,18 +51,18 @@ by (auto elim: widen.elims) lemma is_tyI: - "\ is_type G T; wf_prog wf_mb G \ \ is_ty G T" + "\ is_type G T; ws_prog G \ \ is_ty G T" by (auto simp add: is_ty_def intro: subcls_C_Object split: ty.splits ref_ty.splits) lemma is_type_conv: - "wf_prog wf_mb G \ is_type G T = is_ty G T" + "ws_prog G \ is_type G T = is_ty G T" proof - assume "is_type G T" "wf_prog wf_mb G" + assume "is_type G T" "ws_prog G" thus "is_ty G T" by (rule is_tyI) next - assume wf: "wf_prog wf_mb G" and + assume wf: "ws_prog G" and ty: "is_ty G T" show "is_type G T" @@ -159,7 +159,7 @@ done lemma closed_err_types: - "\ wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) \ + "\ ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G) \ \ closed (err (types G)) (lift2 (sup G))" apply (unfold closed_def plussub_def lift2_def sup_def) apply (auto split: err.split) @@ -171,22 +171,22 @@ lemma sup_subtype_greater: - "\ wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G); + "\ ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G); is_type G t1; is_type G t2; sup G t1 t2 = OK s \ \ subtype G t1 s \ subtype G t2 s" proof - - assume wf_prog: "wf_prog wf_mb G" + assume ws_prog: "ws_prog G" assume single_valued: "single_valued (subcls1 G)" assume acyclic: "acyclic (subcls1 G)" { fix c1 c2 assume is_class: "is_class G c1" "is_class G c2" - with wf_prog + with ws_prog obtain "G \ c1 \C Object" "G \ c2 \C Object" by (blast intro: subcls_C_Object) - with wf_prog single_valued + with ws_prog single_valued obtain u where "is_lub ((subcls1 G)^* ) c1 c2 u" by (blast dest: single_valued_has_lubs) @@ -210,24 +210,24 @@ qed lemma sup_subtype_smallest: - "\ wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G); + "\ ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G); is_type G a; is_type G b; is_type G c; subtype G a c; subtype G b c; sup G a b = OK d \ \ subtype G d c" proof - - assume wf_prog: "wf_prog wf_mb G" + assume ws_prog: "ws_prog G" assume single_valued: "single_valued (subcls1 G)" assume acyclic: "acyclic (subcls1 G)" { fix c1 c2 D assume is_class: "is_class G c1" "is_class G c2" assume le: "G \ c1 \C D" "G \ c2 \C D" - from wf_prog is_class + from ws_prog is_class obtain "G \ c1 \C Object" "G \ c2 \C Object" by (blast intro: subcls_C_Object) - with wf_prog single_valued + with ws_prog single_valued obtain u where lub: "is_lub ((subcls1 G)^* ) c1 c2 u" by (blast dest: single_valued_has_lubs) @@ -260,22 +260,22 @@ split: ty.splits ref_ty.splits) lemma err_semilat_JType_esl_lemma: - "\ wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) \ + "\ ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G) \ \ err_semilat (esl G)" proof - - assume wf_prog: "wf_prog wf_mb G" + assume ws_prog: "ws_prog G" assume single_valued: "single_valued (subcls1 G)" assume acyclic: "acyclic (subcls1 G)" hence "order (subtype G)" by (rule order_widen) moreover - from wf_prog single_valued acyclic + from ws_prog single_valued acyclic have "closed (err (types G)) (lift2 (sup G))" by (rule closed_err_types) moreover - from wf_prog single_valued acyclic + from ws_prog single_valued acyclic have "(\x\err (types G). \y\err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \ (\x\err (types G). \y\err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)" @@ -283,7 +283,7 @@ moreover - from wf_prog single_valued acyclic + from ws_prog single_valued acyclic have "\x\err (types G). \y\err (types G). \z\err (types G). x <=_(le (subtype G)) z \ y <=_(le (subtype G)) z \ x +_(lift2 (sup G)) y <=_(le (subtype G)) z" @@ -297,12 +297,12 @@ qed lemma single_valued_subcls1: - "wf_prog wf_mb G \ single_valued (subcls1 G)" - by (auto simp add: wf_prog_def unique_def single_valued_def + "ws_prog G \ single_valued (subcls1 G)" + by (auto simp add: ws_prog_def unique_def single_valued_def intro: subcls1I elim!: subcls1.elims) theorem err_semilat_JType_esl: - "wf_prog wf_mb G \ err_semilat (esl G)" + "ws_prog G \ err_semilat (esl G)" by (frule acyclic_subcls1, frule single_valued_subcls1, rule err_semilat_JType_esl_lemma) end diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/BV/JVM.thy --- a/src/HOL/MicroJava/BV/JVM.thy Mon May 26 11:42:41 2003 +0200 +++ b/src/HOL/MicroJava/BV/JVM.thy Mon May 26 18:36:15 2003 +0200 @@ -29,7 +29,6 @@ wf_prog (\G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G" - theorem is_bcv_kiljvm: "\ wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \ \ is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) @@ -37,14 +36,15 @@ apply (unfold kiljvm_def sl_triple_conv) apply (rule is_bcv_kildall) apply (simp (no_asm) add: sl_triple_conv [symmetric]) - apply (force intro!: semilat_JVM_slI dest: wf_acyclic simp add: symmetric sl_triple_conv) + apply (force intro!: semilat_JVM_slI dest: wf_acyclic + simp add: symmetric sl_triple_conv) apply (simp (no_asm) add: JVM_le_unfold) apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype - dest: wf_subcls1 wf_acyclic) + dest: wf_subcls1 wf_acyclic wf_prog_ws_prog) apply (simp add: JVM_le_unfold) apply (erule exec_pres_type) apply assumption - apply (erule exec_mono, assumption) + apply (drule wf_prog_ws_prog, erule exec_mono, assumption) done lemma subset_replicate: "set (replicate n x) \ {x}" diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/BV/LBVJVM.thy --- a/src/HOL/MicroJava/BV/LBVJVM.thy Mon May 26 11:42:41 2003 +0200 +++ b/src/HOL/MicroJava/BV/LBVJVM.thy Mon May 26 18:36:15 2003 +0200 @@ -86,7 +86,8 @@ let ?f = "JVMType.sup G mxs mxr" let ?A = "states G mxs mxr" - have "semilat (JVMType.sl G mxs mxr)" by (rule semilat_JVM_slI) + have "semilat (JVMType.sl G mxs mxr)" + by (rule semilat_JVM_slI, rule wf_prog_ws_prog) hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv) moreover have "top ?r Err" by (simp add: JVM_le_unfold) @@ -217,7 +218,8 @@ app_eff: "wt_app_eff (sup_state_opt G) ?app ?eff phi" by (simp (asm_lr) add: wt_method_def2) - have "semilat (JVMType.sl G mxs ?mxr)" by (rule semilat_JVM_slI) + have "semilat (JVMType.sl G mxs ?mxr)" + by (rule semilat_JVM_slI, rule wf_prog_ws_prog) hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv) moreover have "top ?r Err" by (simp add: JVM_le_unfold) @@ -234,7 +236,8 @@ by (clarsimp simp add: exec_def) (intro bounded_lift check_bounded_is_bounded) with wf - have "mono ?r ?step (length ins) ?A" by (rule exec_mono) + have "mono ?r ?step (length ins) ?A" + by (rule wf_prog_ws_prog [THEN exec_mono]) hence "mono ?r ?step (length ?phi) ?A" by (simp add: length) moreover have "pres_type ?step (length ins) ?A" by (rule exec_pres_type) diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy --- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Mon May 26 11:42:41 2003 +0200 +++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Mon May 26 18:36:15 2003 +0200 @@ -239,11 +239,11 @@ done lemma order_sup_state_opt: - "wf_prog wf_mb G \ order (sup_state_opt G)" + "ws_prog G \ order (sup_state_opt G)" by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen) theorem exec_mono: - "wf_prog wf_mb G \ bounded (exec G maxs rT et bs) (size bs) \ + "ws_prog G \ bounded (exec G maxs rT et bs) (size bs) \ mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)" apply (unfold exec_def JVM_le_unfold JVM_states_unfold) apply (rule mono_lift) @@ -257,7 +257,7 @@ done theorem semilat_JVM_slI: - "wf_prog wf_mb G \ semilat (JVMType.sl G maxs maxr)" + "ws_prog G \ semilat (JVMType.sl G maxs maxr)" apply (unfold JVMType.sl_def stk_esl_def reg_sl_def) apply (rule semilat_opt) apply (rule err_semilat_Product_esl) @@ -287,7 +287,7 @@ "(C,S,fs,mdecls) \ set G" "((mn,pTs),rT,code) \ set mdecls" hence "wf_mdecl wf_mb G C ((mn,pTs),rT,code)" - by (unfold wf_prog_def wf_cdecl_def) auto + by (rule wf_prog_wf_mdecl) hence "\t \ set pTs. is_type G t" by (unfold wf_mdecl_def wf_mhead_def) auto moreover @@ -319,11 +319,10 @@ apply (unfold wf_prog_def wf_cdecl_def) apply clarsimp apply (drule bspec, assumption) - apply (unfold wf_mdecl_def) + apply (unfold wf_cdecl_mdecl_def) apply clarsimp apply (drule bspec, assumption) - apply clarsimp - apply (frule methd [OF wf], assumption+) + apply (frule methd [OF wf [THEN wf_prog_ws_prog]], assumption+) apply (frule is_type_pTs [OF wf], assumption+) apply clarify apply (drule rule [OF wf], assumption+) diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/Comp/CorrComp.thy --- a/src/HOL/MicroJava/Comp/CorrComp.thy Mon May 26 11:42:41 2003 +0200 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy Mon May 26 18:36:15 2003 +0200 @@ -8,7 +8,7 @@ theory CorrComp = JTypeSafe + LemmasComp: - +declare wf_prog_ws_prog [simp add] (* If no exception is present after evaluation/execution, none can have been present before *) @@ -278,28 +278,27 @@ (**********************************************************************) -(* ### to be moved to one of the J/* files *) - lemma method_preserves [rule_format (no_asm)]: "\ wf_prog wf_mb G; is_class G C; \ S rT mb. \ cn \ fst ` set G. wf_mdecl wf_mb G cn (S,rT,mb) \ (P cn S (rT,mb))\ \ \ D. method (G, C) S = Some (D, rT, mb) \ (P D S (rT,mb))" -apply (frule WellForm.wf_subcls1) +apply (frule wf_prog_ws_prog [THEN wf_subcls1]) apply (rule subcls1_induct, assumption, assumption) apply (intro strip) apply ((drule spec)+, drule_tac x="Object" in bspec) -apply (simp add: wf_prog_def wf_syscls_def) +apply (simp add: wf_prog_def ws_prog_def wf_syscls_def) apply (subgoal_tac "D=Object") apply simp apply (drule mp) apply (frule_tac C=Object in method_wf_mdecl) - apply simp apply assumption apply simp apply assumption apply simp + apply simp + apply assumption apply simp apply assumption apply simp apply (subst method_rec) apply simp apply force -apply assumption +apply simp apply (simp only: map_add_def) apply (split option.split) apply (rule conjI) @@ -332,14 +331,6 @@ (**********************************************************************) -(* required for lemma wtpd_expr_call *) -lemma ty_exprs_length [simp]: "(E\es[::]Ts \ length es = length Ts)" -apply (subgoal_tac "(E\e::T \ True) \ (E\es[::]Ts \ length es = length Ts) \ (E\s\ \ True)") -apply blast -apply (rule ty_expr_ty_exprs_wt_stmt.induct) -apply auto -done - constdefs wtpd_expr :: "java_mb env \ expr \ bool" "wtpd_expr E e == (\ T. E\e :: T)" wtpd_exprs :: "java_mb env \ (expr list) \ bool" @@ -573,73 +564,43 @@ - - - - - (**********************************************************************) -constdefs - state_ok :: "java_mb env \ xstate \ bool" - "state_ok E xs == xs::\E" - - -lemma state_ok_eval: "\state_ok E xs; wf_java_prog (prg E); wtpd_expr E e; - (prg E)\xs -e\v -> xs'\ \ state_ok E xs'" -apply (simp only: state_ok_def wtpd_expr_def) +lemma state_ok_eval: "\xs::\E; wf_java_prog (prg E); wtpd_expr E e; + (prg E)\xs -e\v -> xs'\ \ xs'::\E" +apply (simp only: wtpd_expr_def) apply (erule exE) -apply (case_tac xs', case_tac xs, simp only:) -apply (rule eval_type_sound [THEN conjunct1]) -apply (rule HOL.refl) -apply assumption -apply (subgoal_tac "fst E \ (gx xs, gs xs) -e\v-> (gx xs', gs xs')") -apply assumption -apply (auto simp: gx_def gs_def) +apply (case_tac xs', case_tac xs) +apply (auto intro: eval_type_sound [THEN conjunct1]) done -(* to be moved into JTypeSafe.thy *) -lemma evals_type_sound: "!!E s s'. - [| G\(x,s) -es[\]vs -> (x',s'); G=prg E; wf_java_prog G; (x,s)::\E; E\es[::]Ts |] - ==> (x',s')::\E \ (x'=None --> list_all2 (conf G (heap s')) vs Ts)" -apply( simp (no_asm_simp) only: split_tupled_all) -apply (drule eval_evals_exec_type_sound - [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp]) -apply auto +lemma state_ok_evals: "\xs::\E; wf_java_prog (prg E); wtpd_exprs E es; + (xs,es,vs,xs') \ Eval.evals (prg E)\ \ xs'::\E" +apply (simp only: wtpd_exprs_def) +apply (erule exE) +apply (case_tac xs) apply (case_tac xs') +apply (auto intro: evals_type_sound [THEN conjunct1]) done -lemma state_ok_evals: "\state_ok E xs; wf_java_prog (prg E); wtpd_exprs E es; - (xs,es,vs,xs') \ Eval.evals (prg E)\ \ state_ok E xs'" -apply (simp only: state_ok_def wtpd_exprs_def) -apply (erule exE) -apply (case_tac xs) apply (case_tac xs') apply (simp only:) -apply (rule evals_type_sound [THEN conjunct1]) -apply (auto simp: gx_def gs_def) -done - -lemma state_ok_exec: "\state_ok E xs; wf_java_prog (prg E); wtpd_stmt E st; - (xs,st,xs') \ Eval.exec (prg E)\ \ state_ok E xs'" -apply (simp only: state_ok_def wtpd_stmt_def) -apply (case_tac xs', case_tac xs, simp only:) -apply (rule exec_type_sound) -apply (rule HOL.refl) -apply assumption -apply (subgoal_tac "((gx xs, gs xs), st, (gx xs', gs xs')) \ Eval.exec (fst E)") -apply assumption -apply (auto simp: gx_def gs_def) +lemma state_ok_exec: "\xs::\E; wf_java_prog (prg E); wtpd_stmt E st; + (xs,st,xs') \ Eval.exec (prg E)\ \ xs'::\E" +apply (simp only: wtpd_stmt_def) +apply (case_tac xs', case_tac xs) +apply (auto intro: exec_type_sound) done lemma state_ok_init: - "\ wf_java_prog G; state_ok (env_of_jmb G C S) (x, h, l); + "\ wf_java_prog G; (x, h, l)::\(env_of_jmb G C S); is_class G dynT; method (G, dynT) (mn, pTs) = Some (md, rT, pns, lvars, blk, res); list_all2 (conf G h) pvs pTs; G,h \ a' ::\ Class md\ \ -state_ok (env_of_jmb G md (mn, pTs)) (np a' x, h, init_vars lvars(pns[\]pvs)(This\a'))" +(np a' x, h, init_vars lvars(pns[\]pvs)(This\a'))::\(env_of_jmb G md (mn, pTs))" +apply (frule wf_prog_ws_prog) apply (frule method_in_md [THEN conjunct2], assumption+) apply (frule method_yields_wf_java_mdecl, assumption, assumption) -apply (simp add: state_ok_def env_of_jmb_def gs_def conforms_def split_beta) +apply (simp add: env_of_jmb_def gs_def conforms_def split_beta) apply (simp add: wf_java_mdecl_def) apply (rule conjI) apply (rule lconf_ext) @@ -675,7 +636,7 @@ done -lemma class_expr_is_class: "\E \ e :: Class C; wf_prog wf_mb (prg E)\ +lemma class_expr_is_class: "\E \ e :: Class C; ws_prog (prg E)\ \ is_class (prg E) C" by (case_tac E, auto dest: ty_expr_is_type) @@ -685,7 +646,7 @@ by (blast dest: singleton_in_set max_spec2appl_meths appl_methsD) -lemma eval_conf: "\G \ s -e\v-> s'; wf_java_prog G; state_ok E s; +lemma eval_conf: "\G \ s -e\v-> s'; wf_java_prog G; s::\E; E\e::T; gx s' = None; prg E = G \ \ G,gh s'\v::\T" apply (simp add: gh_def) @@ -694,15 +655,13 @@ apply (rule sym) apply assumption apply assumption apply (simp (no_asm_use) add: surjective_pairing [THEN sym]) -apply (simp only: state_ok_def gs_def) -apply (case_tac s, simp) -apply assumption -apply (simp add: gx_def) +apply (simp only: surjective_pairing [THEN sym]) +apply (auto simp add: gs_def gx_def) done lemma evals_preserves_conf: "\ G\ s -es[\]vs-> s'; G,gh s \ t ::\ T; E \es[::]Ts; - wf_java_prog G; state_ok E s; + wf_java_prog G; s::\E; prg E = G \ \ G,gh s' \ t ::\ T" apply (subgoal_tac "gh s\| gh s'") apply (frule conf_hext, assumption, assumption) @@ -711,15 +670,14 @@ apply assumption apply (simp add: gx_def gh_def gl_def surjective_pairing [THEN sym]) apply (case_tac E) -apply (simp add: gx_def gs_def gh_def gl_def state_ok_def - surjective_pairing [THEN sym]) +apply (simp add: gx_def gs_def gh_def gl_def surjective_pairing [THEN sym]) done lemma eval_of_class: "\ G \ s -e\a'-> s'; E \ e :: Class C; - wf_java_prog G; state_ok E s; gx s'=None; a' \ Null; G=prg E\ + wf_java_prog G; s::\E; gx s'=None; a' \ Null; G=prg E\ \ (\ lc. a' = Addr lc)" apply (case_tac s, case_tac s', simp) -apply (frule eval_type_sound, (simp add: state_ok_def gs_def)+) +apply (frule eval_type_sound, (simp add: gs_def)+) apply (case_tac a') apply (auto simp: conf_def) done @@ -727,9 +685,10 @@ lemma dynT_subcls: "\ a' \ Null; G,h\a'::\ Class C; dynT = fst (the (h (the_Addr a'))); - is_class G dynT; wf_prog wf_mb G \ \ G\dynT \C C" + is_class G dynT; ws_prog G \ \ G\dynT \C C" apply (case_tac "C = Object") apply (simp, rule subcls_C_Object, assumption+) +apply simp apply (frule non_np_objD, auto) done @@ -746,7 +705,7 @@ apply ((erule exE)+, (erule conjE)+, (erule exE)+) apply (drule widen_methd) apply assumption -apply (rule dynT_subcls, assumption+, simp, assumption+) +apply (rule dynT_subcls) apply assumption+ apply simp apply simp apply (erule exE)+ apply simp done @@ -764,7 +723,7 @@ (\ os CL S. (class_sig_defined G CL S) \ (wtpd_expr (env_of_jmb G CL S) ex) \ - (state_ok (env_of_jmb G CL S) xs) \ + (xs ::\ (env_of_jmb G CL S)) \ ( {TranslComp.comp G, CL, S} \ {gh xs, os, (locvars_xstate G CL S xs)} >- (compExpr (gmb G CL S) ex) \ @@ -775,7 +734,7 @@ (\ os CL S. (class_sig_defined G CL S) \ (wtpd_exprs (env_of_jmb G CL S) exs) \ - (state_ok (env_of_jmb G CL S) xs) \ + (xs::$env_of_jmb G CL S)) \ ( {TranslComp.comp G, CL, S} \ {gh xs, os, (locvars_xstate G CL S xs)} >- (compExprs (gmb G CL S) exs) \ @@ -786,7 +745,7 @@ (\ os CL S. (class_sig_defined G CL S) \ (wtpd_stmt (env_of_jmb G CL S) st) \ - (state_ok (env_of_jmb G CL S) xs) \ + (xs::\(env_of_jmb G CL S)) \ ( {TranslComp.comp G, CL, S} \ {gh xs, os, (locvars_xstate G CL S xs)} >- (compStmt (gmb G CL S) st) \ @@ -797,8 +756,8 @@ apply simp (* case NewC *) -apply clarify -apply (frule wf_subcls1) (* establish wf ((subcls1 G)^-1) *) +apply clarify +apply (frule wf_prog_ws_prog [THEN wf_subcls1]) (* establish wf ((subcls1 G)^-1) *) apply (simp add: c_hupd_hp_invariant) apply (rule progression_one_step) apply (rotate_tac 1, drule sym) (* reverse equation (a, None) = new_Addr (fst s) *) @@ -828,7 +787,7 @@ apply (intro allI impI) apply (frule_tac xs=s1 in eval_xcpt, assumption) (* establish (gx s1 = None) *) apply (frule wtpd_expr_binop) -(* establish (state_ok \ s1) *) +(* establish (s1::\ $ *) apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp)) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) @@ -896,8 +855,9 @@ apply (simp only: gx_conv, simp only: gx_conv, frule np_NoneD, erule conjE) - (* establish (state_ok \ (Norm s1)) *) -apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) + (* establish ((Norm s1)::\ \) *) +apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) + apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) apply (simp only: compExpr_compExprs.simps) @@ -936,7 +896,7 @@ apply (intro allI impI) apply (frule_tac xs=s1 in evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *) apply (frule wtpd_exprs_cons) - (* establish (state_ok \ (Norm s0)) *) + (* establish ((Norm s0)::\ \) *) apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) apply simp @@ -967,7 +927,7 @@ apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *) apply (frule wtpd_stmt_comp) - (* establish (state_ok \ s1) *) + (* establish (s1::\ \) *) apply (frule_tac st=c1 in state_ok_exec) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) apply simp @@ -980,7 +940,7 @@ apply (intro allI impI) apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *) apply (frule wtpd_stmt_cond, (erule conjE)+) -(* establish (state_ok \ s1) *) +(* establish (s1::\ \) *) apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption @@ -1053,9 +1013,9 @@ apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *) apply (frule wtpd_stmt_loop, (erule conjE)+) -(* establish (state_ok \ s1) *) +(* establish (s1::\ \) *) apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) -(* establish (state_ok \ s2) *) +(* establish (s2::\ \) *) apply (frule_tac xs=s1 and st=c in state_ok_exec) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) @@ -1094,7 +1054,7 @@ apply blast (*****) -(* case method call *) defer (* !!! NEWC *) +(* case method call *) apply (intro allI impI) @@ -1107,11 +1067,11 @@ (* assumptions about state_ok and is_class *) -(* establish state_ok (env_of_jmb G CL S) s1 *) +(* establish s1::\ (env_of_jmb G CL S) *) apply (frule_tac xs="Norm s0" and e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp (no_asm_use) only: env_of_jmb_fst) -(* establish state_ok (env_of_jmb G CL S) (x, h, l) *) +(* establish (x, h, l)::\(env_of_jmb G CL S) *) apply (frule_tac xs=s1 and xs'="(x, h, l)" in state_ok_evals) apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp only: env_of_jmb_fst) @@ -1130,7 +1090,7 @@ apply (subgoal_tac " method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res)") apply (subgoal_tac "list_all2 (conf G h) pvs pTs") -(* establish state_ok (env_of_jmb G md (mn, pTs)) (np a' x, h, init_vars lvars(pns[\]pvs)(This\a')) *) +(* establish (np a' x, h, init_vars lvars(pns[\]pvs)(This\a'))::\(env_of_jmb G md (mn, pTs)) *) apply (subgoal_tac "G,h \ a' ::\ Class dynT") apply (frule (2) conf_widen) apply (frule state_ok_init, assumption+) @@ -1138,16 +1098,14 @@ apply (subgoal_tac "class_sig_defined G md (mn, pTs)") apply (frule wtpd_blk, assumption, assumption) apply (frule wtpd_res, assumption, assumption) -apply (subgoal_tac "state_ok (env_of_jmb G md (mn, pTs)) s3") +apply (subgoal_tac "s3::\(env_of_jmb G md (mn, pTs))") -(* establish method (TranslComp.comp G, md) (mn, pTs) = - Some (md, rT, compMethod (pns, lvars, blk, res)) *) -apply (frule_tac C=md and D=md in comp_method, assumption, assumption) - -(* establish - method (TranslComp.comp G, dynT) (mn, pTs) = - Some (md, rT, compMethod (pns, lvars, blk, res)) *) - apply (frule_tac C=dynT and D=md in comp_method, assumption, assumption) +apply (subgoal_tac "method (TranslComp.comp G, md) (mn, pTs) = + Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))") +prefer 2 apply (simp add: wf_prog_ws_prog [THEN comp_method]) +apply (subgoal_tac "method (TranslComp.comp G, dynT) (mn, pTs) = + Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))") +prefer 2 apply (simp add: wf_prog_ws_prog [THEN comp_method]) apply (simp only: fst_conv snd_conv) (* establish length pns = length pTs *) @@ -1209,7 +1167,7 @@ apply (simp (no_asm_simp)) apply (simp (no_asm_simp)) -(* show state_ok \ s3 *) +(* show s3::\\ *) apply (rule_tac xs = "(np a' x, h, init_vars lvars(pns[\]pvs)(This\a'))" and st=blk in state_ok_exec) apply assumption apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) @@ -1231,7 +1189,7 @@ apply (subgoal_tac "((gx s1, gs s1), ps, pvs, x, h, l) \ evals G") apply (frule_tac E="env_of_jmb G CL S" in evals_type_sound) apply (simp only: env_of_jmb_fst) -apply assumption apply (simp only: state_ok_def) +apply assumption apply (simp add: conforms_def xconf_def gs_def) apply simp apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym]) @@ -1242,14 +1200,14 @@ (* show method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res) *) -apply (frule method_in_md [THEN conjunct2], assumption+) +apply (frule wf_prog_ws_prog [THEN method_in_md [THEN conjunct2]], assumption+) (* show G\Class dynT \ Class md *) apply (simp (no_asm_use) only: widen_Class_Class) apply (rule method_wf_mdecl [THEN conjunct1], assumption+) (* is_class G md *) -apply (rule method_in_md [THEN conjunct1], assumption+) +apply (rule wf_prog_ws_prog [THEN method_in_md [THEN conjunct1]], assumption+) (* show is_class G dynT *) apply (frule non_npD) apply assumption @@ -1257,6 +1215,7 @@ apply simp apply (rule subcls_is_class2) apply assumption apply (frule class_expr_is_class) apply (simp only: env_of_jmb_fst) +apply (rule wf_prog_ws_prog, assumption) apply (simp only: env_of_jmb_fst) (* show G,h \ a' ::\ Class C *) @@ -1280,7 +1239,7 @@ >- (compExpr (gmb G C S) ex) \ {hp', val#os, (locvars_locals G C S loc')}" apply (frule compiler_correctness [THEN conjunct1]) -apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def state_ok_def) +apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def) done theorem compiler_correctness_exec: " @@ -1294,7 +1253,7 @@ >- (compStmt (gmb G C S) st) \ {hp', os, (locvars_locals G C S loc')}" apply (frule compiler_correctness [THEN conjunct2 [THEN conjunct2]]) -apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def state_ok_def) +apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def) done (**********************************************************************) @@ -1306,4 +1265,6 @@ simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) *} +declare wf_prog_ws_prog [simp del] + end diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/Comp/CorrCompTp.thy --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Mon May 26 11:42:41 2003 +0200 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Mon May 26 18:36:15 2003 +0200 @@ -4,8 +4,7 @@ Copyright GPL 2002 *) -theory CorrCompTp = LemmasComp + JVM + TypeInf + NatCanonify + Altern: - +theory CorrCompTp = LemmasComp + JVM + TypeInf + Altern: declare split_paired_All [simp del] declare split_paired_Ex [simp del] @@ -27,7 +26,7 @@ by (simp add: local_env_def split_beta) -lemma wt_class_expr_is_class: "\ wf_prog wf_mb G; E \ expr :: Class cname; +lemma wt_class_expr_is_class: "\ ws_prog G; E \ expr :: Class cname; E = local_env G C (mn, pTs) pns lvars\ \ is_class G cname " apply (subgoal_tac "((fst E), (snd E)) \ expr :: Class cname") @@ -308,7 +307,7 @@ (* show is_class G cname \ field (G, cname) vname = Some (cname, T) *) apply (rule field_in_fd) apply assumption+ (* show is_class G Ca *) - apply (rule wt_class_expr_is_class, assumption+, rule HOL.refl) + apply (fast intro: wt_class_expr_is_class) (* FAss *) apply (intro strip) @@ -485,8 +484,8 @@ lemma states_mono: "\ mxs \ mxs' \ \ states G mxs mxr \ states G mxs' mxr" apply (simp add: states_def JVMType.sl_def) -apply (simp add: Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def - JType.esl_def) +apply (simp add: Product.esl_def stk_esl_def reg_sl_def + upto_esl_def Listn.sl_def Err.sl_def JType.esl_def) apply (simp add: Err.esl_def Err.le_def Listn.le_def) apply (simp add: Product.le_def Product.sup_def Err.sup_def) apply (simp add: Opt.esl_def Listn.sup_def) @@ -528,14 +527,12 @@ apply (induct i) apply simp+ (* case Goto *) -apply (simp only: nat_canonify) -apply simp +apply arith (* case Ifcmpeq *) apply simp apply (erule disjE) -apply simp -apply (simp only: nat_canonify) -apply simp +apply arith +apply arith (* case Throw *) apply simp done @@ -547,14 +544,12 @@ apply (induct i) apply simp+ (* case Goto *) -apply (simp only: nat_canonify) -apply simp +apply arith (* case Ifcmpeq *) apply simp apply (erule disjE) apply simp -apply (simp only: nat_canonify) -apply simp +apply arith (* case Throw *) apply simp done @@ -1255,33 +1250,35 @@ \ bc_mt_corresp [Getfield vname cname] (replST (Suc 0) (snd (the (field (G, cname) vname)))) (Class C # ST, LT) (comp G) rT mxr (Suc 0)" - apply (frule wf_subcls1) + apply (frule wf_prog_ws_prog [THEN wf_subcls1]) apply (frule field_in_fd, assumption+) apply (frule widen_field, assumption+) apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def) - apply (simp add: comp_field [THEN sym] comp_subcls1 [THEN sym] comp_widen [THEN sym] comp_is_class [THEN sym]) + apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class) apply (simp add: max_ssize_def max_of_list_def ssize_sto_def) apply (intro strip) apply (simp add: check_type_simps) apply clarify apply (rule_tac x="Suc (length ST)" in exI) apply simp+ -apply (simp only: comp_is_type [THEN sym]) +apply (simp only: comp_is_type) apply (rule_tac C=cname in fields_is_type) apply (simp add: field_def) apply (drule JBasis.table_of_remap_SomeD)+ apply assumption+ +apply (erule wf_prog_ws_prog) +apply assumption done lemma bc_mt_corresp_Putfield: "\ wf_prog wf_mb G; field (G, C) vname = Some (cname, Ta); G \ T \ Ta; is_class G C \ \ bc_mt_corresp [Putfield vname cname] (popST 2) (T # Class C # T # ST, LT) (comp G) rT mxr (Suc 0)" - apply (frule wf_subcls1) + apply (frule wf_prog_ws_prog [THEN wf_subcls1]) apply (frule field_in_fd, assumption+) apply (frule widen_field, assumption+) apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def) - apply (simp add: comp_field [THEN sym] comp_subcls1 [THEN sym] comp_widen [THEN sym] comp_is_class [THEN sym]) + apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class) apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def) apply (intro strip) @@ -1302,13 +1299,13 @@ apply (simp add: comp_is_class) apply (rule_tac x=pTsa in exI) apply (rule_tac x="Class cname" in exI) - apply (simp add: max_spec_preserves_length comp_is_class [THEN sym]) + apply (simp add: max_spec_preserves_length comp_is_class) apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+) - apply (simp add: comp_widen list_all2_def) + apply (simp add: split_paired_all comp_widen list_all2_def) apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+) apply (rule exI)+ - apply (rule comp_method) - apply assumption+ + apply (simp add: wf_prog_ws_prog [THEN comp_method]) + apply auto done @@ -1329,7 +1326,7 @@ -- {* @{text "<=s"} *} apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+) - apply (frule comp_method, assumption+) + apply (simp add: wf_prog_ws_prog [THEN comp_method]) apply (simp add: max_spec_preserves_length [THEN sym]) -- "@{text check_type}" @@ -1341,7 +1338,7 @@ apply clarify apply (rule_tac x="Suc (length ST)" in exI) apply simp+ -apply (simp only: comp_is_type [THEN sym]) +apply (simp only: comp_is_type) apply (frule method_wf_mdecl) apply assumption apply assumption apply (simp add: wf_mdecl_def wf_mhead_def) apply (simp add: max_def) @@ -1714,6 +1711,7 @@ apply (simp (no_asm_simp), rule bc_mt_corresp_Checkcast) apply (simp add: comp_is_class) apply (simp only: compTpExpr_LT_ST) +apply (drule cast_RefT) apply blast apply (simp add: start_sttp_resp_def) @@ -1885,7 +1883,7 @@ apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast) apply (simp (no_asm_simp)) apply (rule bc_mt_corresp_Getfield) apply assumption+ - apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl) + apply (fast intro: wt_class_expr_is_class) apply (simp (no_asm_simp) add: start_sttp_resp_def) @@ -1905,7 +1903,7 @@ apply (rule bc_mt_corresp_Dup_x1) apply (simp (no_asm_simp) add: dup_x1ST_def) apply (rule bc_mt_corresp_Putfield) apply assumption+ - apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl) + apply (fast intro: wt_class_expr_is_class) apply (simp (no_asm_simp) add: start_sttp_resp_def) apply (simp (no_asm_simp) add: start_sttp_resp_def) apply (simp (no_asm_simp) add: start_sttp_resp_def) @@ -1922,7 +1920,7 @@ apply (simp only: compTpExprs_LT_ST) apply (simp (no_asm_simp)) apply (rule bc_mt_corresp_Invoke) apply assumption+ - apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl) + apply (fast intro: wt_class_expr_is_class) apply (simp (no_asm_simp) add: start_sttp_resp_def) apply (rule start_sttp_resp_comb) apply (simp (no_asm_simp)) @@ -2247,14 +2245,13 @@ apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+ apply (intro strip) apply (rule wt_instr_Goto) - apply (simp (no_asm_simp) add: nat_canonify) - apply (simp (no_asm_simp) add: nat_canonify) + apply arith + apply arith (* \ ! nat (int pc + i) = \ ! pc *) - apply (simp (no_asm_simp) add: nat_canonify) + apply (simp (no_asm_simp)) apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt) apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def) apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST) - apply (simp (no_asm_simp) only: int_outside_right nat_int) apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt) apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST) apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def) @@ -2592,52 +2589,56 @@ apply (simp only: split_paired_All, simp) (* subgoal is_class / wf_mhead / wf_java_mdecl *) -apply (rule methd [THEN conjunct2]) apply assumption+ apply (simp only:) -apply (rule wf_prog_wf_mhead, assumption+) apply (simp only:) +apply (blast intro: methd [THEN conjunct2]) +apply (frule wf_prog_wf_mdecl, assumption+) apply (simp only:) apply (simp add: wf_mdecl_def) apply (rule wf_java_prog_wf_java_mdecl, assumption+) - done - (**********************************************************************************) - - - lemma comp_set_ms: "(C, D, fs, cms)\set (comp G) \ \ ms. (C, D, fs, ms) \set G \ cms = map (compMethod G C) ms" by (auto simp: comp_def compClass_def) -lemma method_body_source: "\ wf_prog wf_mb G; is_class G C; method (comp G, C) sig = Some (D, rT, cmb) \ - \ (\ mb. method (G, C) sig = Some (D, rT, mb))" -apply (simp add: comp_method_eq comp_method_result_def) -apply (case_tac "method (G, C) sig") -apply auto -done + + (* ---------------------------------------------------------------------- *) section "Main Theorem" (* MAIN THEOREM: Methodtype computed by comp is correct for bytecode generated by compTp *) theorem wt_prog_comp: "wf_java_prog G \ wt_jvm_prog (comp G) (compTp G)" apply (simp add: wf_prog_def) + apply (subgoal_tac "wf_java_prog G") prefer 2 apply (simp add: wf_prog_def) apply (simp (no_asm_simp) add: wf_prog_def wt_jvm_prog_def) -apply (simp add: comp_unique comp_wf_syscls wf_cdecl_def) +apply (simp add: comp_ws_prog) + +apply (intro strip) +apply (subgoal_tac "\ C D fs cms. c = (C, D, fs, cms)") apply clarify apply (frule comp_set_ms) apply clarify apply (drule bspec, assumption) -apply (simp add: comp_wf_fdecl) -apply (simp add: wf_mdecl_def) - apply (rule conjI) -apply (rule ballI) -apply (subgoal_tac "\ sig rT mb. x = (sig, rT, mb)") prefer 2 apply (case_tac x, simp) + + (* wf_mrT *) +apply (case_tac "C = Object") +apply (simp add: wf_mrT_def) +apply (subgoal_tac "is_class G D") +apply (simp add: comp_wf_mrT) +apply (simp add: wf_prog_def ws_prog_def ws_cdecl_def) +apply blast + + (* wf_cdecl_mdecl *) +apply (simp add: wf_cdecl_mdecl_def) +apply (simp add: split_beta) +apply (intro strip) + + (* show wt_method \ *) +apply (subgoal_tac "\ sig rT mb. x = (sig, rT, mb)") apply (erule exE)+ apply (simp (no_asm_simp) add: compMethod_def split_beta) apply (erule conjE)+ apply (drule_tac x="(sig, rT, mb)" in bspec) apply simp -apply (rule conjI) -apply (simp add: comp_wf_mhead) apply (rule_tac mn="fst sig" and pTs="snd sig" in wt_method_comp) apply assumption+ apply simp @@ -2647,27 +2648,11 @@ apply simp apply simp apply (simp add: compMethod_def split_beta) - -apply (rule conjI) -apply (rule unique_map_fst [THEN iffD1]) - apply (simp (no_asm_simp) add: compMethod_def split_beta) apply simp - -apply clarify -apply (rule conjI) apply (simp add: comp_is_class) -apply (rule conjI) apply (simp add: comp_subcls) -apply (simp add: compMethod_def split_beta) -apply (intro strip) - apply (drule_tac x=x in bspec, assumption, drule_tac x="D'" in spec, drule_tac x="rT'" in spec) - apply (erule exE) - -apply (frule method_body_source) apply assumption+ -apply (drule mp, assumption) -apply (simp add: comp_widen) +apply auto done - (**********************************************************************************) declare split_paired_All [simp add] diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/Comp/Index.thy --- a/src/HOL/MicroJava/Comp/Index.thy Mon May 26 11:42:41 2003 +0200 +++ b/src/HOL/MicroJava/Comp/Index.thy Mon May 26 18:36:15 2003 +0200 @@ -63,6 +63,10 @@ apply simp done +lemma lift_if: "(f (if b then t else e)) = (if b then (f t) else (f e))" +apply auto +done + lemma update_at_index: " \ distinct (gjmb_plns (gmb G C S)); x \ set (gjmb_plns (gmb G C S)); x \ This \ \ diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/Comp/LemmasComp.thy --- a/src/HOL/MicroJava/Comp/LemmasComp.thy Mon May 26 11:42:41 2003 +0200 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Mon May 26 18:36:15 2003 +0200 @@ -8,9 +8,16 @@ theory LemmasComp = TranslComp: + +declare split_paired_All [simp del] +declare split_paired_Ex [simp del] + + (**********************************************************************) (* misc lemmas *) + + lemma split_pairs: "(\(a,b). (F a b)) (ab) = F (fst ab) (snd ab)" proof - have "(\(a,b). (F a b)) (fst ab,snd ab) = F (fst ab) (snd ab)" @@ -34,6 +41,44 @@ by (case_tac st, simp add: c_hupd_conv gh_def) +lemma unique_map_fst [rule_format]: "(\ x \ set xs. (fst x = fst (f x) )) \ + unique (map f xs) = unique xs" +proof (induct xs) + case Nil show ?case by simp +next + case (Cons a list) + show ?case + proof + assume fst_eq: "\x\set (a # list). fst x = fst (f x)" + + have fst_set: "(fst a \ fst ` set list) = (fst (f a) \ fst ` f ` set list)" + proof + assume as: "fst a \ fst ` set list" + then obtain x where fst_a_x: "x\set list \ fst a = fst x" + by (auto simp add: image_iff) + then have "fst (f a) = fst (f x)" by (simp add: fst_eq) + with as show "(fst (f a) \ fst ` f ` set list)" by (simp add: fst_a_x) + next + assume as: "fst (f a) \ fst ` f ` set list" + then obtain x where fst_a_x: "x\set list \ fst (f a) = fst (f x)" + by (auto simp add: image_iff) + then have "fst a = fst x" by (simp add: fst_eq) + with as show "fst a \ fst ` set list" by (simp add: fst_a_x) + qed + + with fst_eq Cons + show "unique (map f (a # list)) = unique (a # list)" + by (simp add: unique_def fst_set) + qed +qed + +lemma comp_unique: "unique (comp G) = unique G" +apply (simp add: comp_def) +apply (rule unique_map_fst) +apply (simp add: compClass_def split_beta) +done + + (**********************************************************************) (* invariance of properties under compilation *) @@ -53,75 +98,96 @@ apply (simp add: image_compose [THEN sym] o_def split_beta del: image_compose) done -lemma comp_is_class: "is_class G C = is_class (comp G) C" +lemma comp_is_class: "is_class (comp G) C = is_class G C" by (case_tac "class G C", auto simp: is_class_def comp_class_None dest: comp_class_imp) -lemma comp_is_type: "is_type G T = is_type (comp G) T" +lemma comp_is_type: "is_type (comp G) T = is_type G T" by ((cases T),simp,(induct G)) ((simp),(simp only: comp_is_class),(simp add: comp_is_class),(simp only: comp_is_class)) -lemma SIGMA_cong: "\ A = B; !!x. x \ B \ C x = D x \ \ (\ x \ A. C x) = (\ x \ B. D x)" +lemma SIGMA_cong: "\ A = B; !!x. x \ B \ C x = D x \ + \ (\ x \ A. C x) = (\ x \ B. D x)" by auto -lemma comp_classname: "is_class G C \ fst (the (class G C)) = fst (the (class (comp G) C))" +lemma comp_classname: "is_class G C + \ fst (the (class G C)) = fst (the (class (comp G) C))" by (case_tac "class G C", auto simp: is_class_def dest: comp_class_imp) -lemma comp_subcls1: "subcls1 G = subcls1 (comp G)" +lemma comp_subcls1: "subcls1 (comp G) = subcls1 G" apply (simp add: subcls1_def2 comp_is_class) apply (rule SIGMA_cong, simp) -apply (simp add: comp_is_class [THEN sym]) +apply (simp add: comp_is_class) apply (simp add: comp_classname) done -lemma comp_subcls: "(subcls1 G)^* = (subcls1 (comp G))^*" - by (induct G) (simp_all add: comp_def comp_subcls1) - -lemma comp_widen: "((ty1,ty2) \ widen G) = ((ty1,ty2) \ widen (comp G))" +lemma comp_widen: "((ty1,ty2) \ widen (comp G)) = ((ty1,ty2) \ widen G)" apply rule + apply (cases "(ty1,ty2)" "comp G" rule: widen.cases) + apply (simp_all add: comp_subcls1 widen.null) apply (cases "(ty1,ty2)" G rule: widen.cases) - apply (simp_all add: comp_subcls widen.null) - apply (cases "(ty1,ty2)" "comp G" rule: widen.cases) - apply (simp_all add: comp_subcls widen.null) + apply (simp_all add: comp_subcls1 widen.null) done -lemma comp_cast: "((ty1,ty2) \ cast G) = ((ty1,ty2) \ cast (comp G))" +lemma comp_cast: "((ty1,ty2) \ cast (comp G)) = ((ty1,ty2) \ cast G)" apply rule + apply (cases "(ty1,ty2)" "comp G" rule: cast.cases) + apply (simp_all add: comp_subcls1 cast.widen cast.subcls) + apply (rule cast.widen) apply (simp add: comp_widen) apply (cases "(ty1,ty2)" G rule: cast.cases) - apply (simp_all add: comp_subcls cast.widen cast.subcls) - apply (cases "(ty1,ty2)" "comp G" rule: cast.cases) - apply (simp_all add: comp_subcls cast.widen cast.subcls) + apply (simp_all add: comp_subcls1 cast.widen cast.subcls) + apply (rule cast.widen) apply (simp add: comp_widen) done -lemma comp_cast_ok: "cast_ok G = cast_ok (comp G)" +lemma comp_cast_ok: "cast_ok (comp G) = cast_ok G" by (simp add: expand_fun_eq cast_ok_def comp_widen) -lemma comp_wf_fdecl: "wf_fdecl G fd \ wf_fdecl (comp G) fd" -apply (case_tac fd) -apply (simp add: wf_fdecl_def comp_is_type) +lemma compClass_fst [simp]: "(fst (compClass G C)) = (fst C)" +by (simp add: compClass_def split_beta) + +lemma compClass_fst_snd [simp]: "(fst (snd (compClass G C))) = (fst (snd C))" +by (simp add: compClass_def split_beta) + +lemma compClass_fst_snd_snd [simp]: "(fst (snd (snd (compClass G C)))) = (fst (snd (snd C)))" +by (simp add: compClass_def split_beta) + +lemma comp_wf_fdecl [simp]: "wf_fdecl (comp G) fd = wf_fdecl G fd" +by (case_tac fd, simp add: wf_fdecl_def comp_is_type) + + +lemma compClass_forall [simp]: " + (\x\set (snd (snd (snd (compClass G C)))). P (fst x) (fst (snd x))) = + (\x\set (snd (snd (snd C))). P (fst x) (fst (snd x)))" +by (simp add: compClass_def compMethod_def split_beta) + +lemma comp_wf_mhead: "wf_mhead (comp G) S rT = wf_mhead G S rT" +by (simp add: wf_mhead_def split_beta comp_is_type) + +lemma comp_ws_cdecl: " + ws_cdecl (TranslComp.comp G) (compClass G C) = ws_cdecl G C" +apply (simp add: ws_cdecl_def split_beta comp_is_class comp_subcls1) +apply (simp (no_asm_simp) add: comp_wf_mhead) +apply (simp add: compClass_def compMethod_def split_beta unique_map_fst) done -lemma comp_wf_syscls: "wf_syscls G = wf_syscls (comp G)" + +lemma comp_wf_syscls: "wf_syscls (comp G) = wf_syscls G" apply (simp add: wf_syscls_def comp_def compClass_def split_beta) apply (simp only: image_compose [THEN sym]) -apply (subgoal_tac "(Fun.comp fst (\(C, cno::cname, fdls::fdecl list, jmdls). (C, cno, fdls, map (compMethod G C) jmdls))) = fst") -(* -apply (subgoal_tac "(fst o (\(C, cno::cname, fdls::fdecl list, jmdls). (C, cno, fdls, map (compMethod G C) jmdls))) = fst") -*) +apply (subgoal_tac "(Fun.comp fst (\(C, cno::cname, fdls::fdecl list, jmdls). + (C, cno, fdls, map (compMethod G C) jmdls))) = fst") apply (simp del: image_compose) apply (simp add: expand_fun_eq split_beta) done -lemma comp_wf_mhead: "wf_mhead G S rT = wf_mhead (comp G) S rT" -by (simp add: wf_mhead_def split_beta comp_is_type) - -lemma comp_wf_mdecl: "\ wf_mdecl wf_mb G C jmdl; - (wf_mb G C jmdl) \ (wf_mb_comp (comp G) C (compMethod G C jmdl)) \ - \ - wf_mdecl wf_mb_comp (comp G) C (compMethod G C jmdl)" -by (simp add: wf_mdecl_def wf_mhead_def comp_is_type split_beta compMethod_def) +lemma comp_ws_prog: "ws_prog (comp G) = ws_prog G" +apply (rule sym) +apply (simp add: ws_prog_def comp_ws_cdecl comp_unique) +apply (simp add: comp_wf_syscls) +apply (auto simp add: comp_ws_cdecl [THEN sym] TranslComp.comp_def) +done lemma comp_class_rec: " wf ((subcls1 G)^-1) \ @@ -159,16 +225,16 @@ done lemma comp_fields: "wf ((subcls1 G)^-1) \ - fields (G,C) = fields (comp G,C)" + fields (comp G,C) = fields (G,C)" by (simp add: fields_def comp_class_rec) lemma comp_field: "wf ((subcls1 G)^-1) \ - field (G,C) = field (comp G,C)" + field (comp G,C) = field (G,C)" by (simp add: field_def comp_fields) -lemma class_rec_relation [rule_format (no_asm)]: "\ wf_prog wf_mb G; +lemma class_rec_relation [rule_format (no_asm)]: "\ ws_prog G; \ fs ms. R (f1 Object fs ms t1) (f2 Object fs ms t2); \ C fs ms r1 r2. (R r1 r2) \ (R (f1 C fs ms r1) (f2 C fs ms r2)) \ \ ((class G C) \ None) \