# HG changeset patch # User kleing # Date 976480834 -3600 # Node ID 17063aee1d8627cd447c0da749ddec71b275fda2 # Parent 41d309b48afe6e0de3af7a32f47f91838d44e7d2 moved method lemma to BVSpec diff -r 41d309b48afe -r 17063aee1d86 src/HOL/MicroJava/BV/BVSpec.thy --- a/src/HOL/MicroJava/BV/BVSpec.thy Sun Dec 10 21:40:14 2000 +0100 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Sun Dec 10 21:40:34 2000 +0100 @@ -58,6 +58,46 @@ (app i G mxs rT (phi!pc) \ pc+1 < max_pc \ (G \ step i G (phi!pc) <=' phi!(pc+1)))" by (simp add: wt_instr_def) + +(* move to WellForm *) + +lemma methd: + "[| wf_prog wf_mb G; (C,S,fs,mdecls) \ set G; (sig,rT,code) \ set mdecls |] + ==> method (G,C) sig = Some(C,rT,code) \ is_class G C" +proof - + assume wf: "wf_prog wf_mb G" + assume C: "(C,S,fs,mdecls) \ set G" + + assume m: "(sig,rT,code) \ set mdecls" + moreover + from wf + have "class G Object = Some (arbitrary, [], [])" + by simp + moreover + from wf C + have c: "class G C = Some (S,fs,mdecls)" + by (auto simp add: wf_prog_def intro: map_of_SomeI) + ultimately + have O: "C \ Object" + by auto + + from wf C + have "unique mdecls" + by (unfold wf_prog_def wf_cdecl_def) auto + + hence "unique (map (\(s,m). (s,C,m)) mdecls)" + by - (induct mdecls, auto) + + with m + have "map_of (map (\(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)" + by (force intro: map_of_SomeI) + + with wf C m c O + show ?thesis + by (auto dest: method_rec [of _ _ C]) +qed + + end diff -r 41d309b48afe -r 17063aee1d86 src/HOL/MicroJava/BV/LBVSpec.thy --- a/src/HOL/MicroJava/BV/LBVSpec.thy Sun Dec 10 21:40:14 2000 +0100 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy Sun Dec 10 21:40:34 2000 +0100 @@ -191,40 +191,4 @@ qed -lemma methd: - "[| wf_prog wf_mb G; (C,S,fs,mdecls) \ set G; (sig,rT,code) \ set mdecls |] - ==> method (G,C) sig = Some(C,rT,code) \ is_class G C" -proof - - assume wf: "wf_prog wf_mb G" - assume C: "(C,S,fs,mdecls) \ set G" - - assume m: "(sig,rT,code) \ set mdecls" - moreover - from wf - have "class G Object = Some (arbitrary, [], [])" - by simp - moreover - from wf C - have c: "class G C = Some (S,fs,mdecls)" - by (auto simp add: wf_prog_def intro: map_of_SomeI) - ultimately - have O: "C \ Object" - by auto - - from wf C - have "unique mdecls" - by (unfold wf_prog_def wf_cdecl_def) auto - - hence "unique (map (\(s,m). (s,C,m)) mdecls)" - by - (induct mdecls, auto) - - with m - have "map_of (map (\(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)" - by (force intro: map_of_SomeI) - - with wf C m c O - show ?thesis - by (auto dest: method_rec [of _ _ C]) -qed - end