# 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) \<and> pc+1 < max_pc \<and> (G \<turnstile> 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) \<in> set G; (sig,rT,code) \<in> set mdecls |]
+  ==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C"
+proof -
+  assume wf: "wf_prog wf_mb G" 
+  assume C:  "(C,S,fs,mdecls) \<in> set G"
+
+  assume m: "(sig,rT,code) \<in> 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 \<noteq> Object"
+    by auto
+      
+  from wf C
+  have "unique mdecls"
+    by (unfold wf_prog_def wf_cdecl_def) auto
+
+  hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)"
+    by - (induct mdecls, auto)
+
+  with m
+  have "map_of (map (\<lambda>(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) \<in> set G; (sig,rT,code) \<in> set mdecls |]
-  ==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C"
-proof -
-  assume wf: "wf_prog wf_mb G" 
-  assume C:  "(C,S,fs,mdecls) \<in> set G"
-
-  assume m: "(sig,rT,code) \<in> 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 \<noteq> Object"
-    by auto
-      
-  from wf C
-  have "unique mdecls"
-    by (unfold wf_prog_def wf_cdecl_def) auto
-
-  hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)"
-    by - (induct mdecls, auto)
-
-  with m
-  have "map_of (map (\<lambda>(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