diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -6,7 +6,7 @@
 
 header {* \isaheader{Well-formedness of Java programs} *}
 
-theory WellForm = TypeRel:
+theory WellForm = TypeRel + SystemClasses:
 
 text {*
 for static checks on expressions and statements, see WellType.
@@ -45,9 +45,12 @@
                    (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'.
                       method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))"
 
+ wf_syscls :: "'c prog => bool"
+"wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"
+
  wf_prog :: "'c wf_mb => 'c prog => bool"
-"wf_prog wf_mb G ==
-   let cs = set G in ObjectC \<in> cs \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G"
+"wf_prog wf_mb G == 
+   let cs = set G in wf_syscls G \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G"
 
 lemma class_wf: 
  "[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)"
@@ -57,9 +60,9 @@
 done
 
 lemma class_Object [simp]: 
-  "wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])"
-apply (unfold wf_prog_def ObjectC_def class_def)
-apply (auto intro: map_of_SomeI)
+  "wf_prog wf_mb G ==> \<exists>X fs ms. class G Object = Some (X,fs,ms)"
+apply (unfold wf_prog_def wf_syscls_def class_def)
+apply (auto simp: map_of_SomeI)
 done
 
 lemma is_class_Object [simp]: "wf_prog wf_mb G ==> is_class G Object"
@@ -158,20 +161,12 @@
 
 lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma];
 
-lemma method_Object [simp]: "wf_prog wf_mb G ==> method (G,Object) = empty"
-apply(subst method_rec)
-apply auto
-done
-
-lemma fields_Object [simp]: "wf_prog wf_mb G ==> fields (G,Object) = []"
-apply(subst fields_rec)
-apply auto
-done
-
-lemma field_Object [simp]: "wf_prog wf_mb G ==> field (G,Object) = empty"
-apply (unfold field_def)
-apply(simp (no_asm_simp))
-done
+lemma method_Object [simp]:
+  "method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> wf_prog wf_mb G \<Longrightarrow> D = Object"  
+  apply (frule class_Object, clarify)
+  apply (drule method_rec, assumption)
+  apply (auto dest: map_of_SomeD)
+  done
 
 lemma subcls_C_Object: "[|is_class G C; wf_prog wf_mb G|] ==> G\<turnstile>C\<preceq>C Object"
 apply(erule subcls1_induct)
@@ -190,7 +185,10 @@
   \<forall>((fn,fd),fT)\<in>set (fields (G,C)). G\<turnstile>C\<preceq>C fd"
 apply( erule subcls1_induct)
 apply(   assumption)
-apply(  simp (no_asm_simp))
+apply(  frule class_Object)
+apply(  clarify)
+apply(  frule fields_rec, assumption)
+apply(  fastsimp)
 apply( tactic "safe_tac HOL_cs")
 apply( subst fields_rec)
 apply(   assumption)
@@ -216,8 +214,16 @@
   "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
 apply( erule subcls1_induct)
 apply(   assumption)
-apply(  safe dest!: wf_cdecl_supD)
-apply(  simp (no_asm_simp))
+apply(  frule class_Object)
+apply(  clarify)
+apply(  frule fields_rec, assumption)
+apply(  drule class_wf, assumption)
+apply(  simp add: wf_cdecl_def)
+apply(  rule unique_map_inj)
+apply(   simp)
+apply(  rule injI)
+apply(  simp)
+apply( safe dest!: wf_cdecl_supD)
 apply( drule subcls1_wfD)
 apply(  assumption)
 apply( subst fields_rec)
@@ -269,7 +275,16 @@
    --> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))"
 apply( erule subcls1_induct)
 apply(   assumption)
-apply(  force)
+apply(  clarify) 
+apply(  frule class_Object)
+apply(  clarify)
+apply(  frule method_rec, assumption)
+apply(  drule class_wf, assumption)
+apply(  simp add: wf_cdecl_def)
+apply(  drule map_of_SomeD)
+apply(  subgoal_tac "md = Object")
+apply(   fastsimp)
+apply(  fastsimp)
 apply( clarify)
 apply( frule_tac C = C in method_rec)
 apply(  assumption)
@@ -334,7 +349,10 @@
   "wf_prog wf_mb G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) 
   --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
 apply (erule (1) subcls1_induct)
- apply (simp)
+ apply clarify
+ apply (frule method_Object, assumption)
+ apply hypsubst
+ apply simp
 apply (erule conjE)
 apply (subst method_rec)
   apply (assumption)
@@ -377,7 +395,12 @@
   "[|is_class G C; wf_prog wf_mb G|] ==>  
   \<forall>f\<in>set (fields (G,C)). is_type G (snd f)"
 apply( erule (1) subcls1_induct)
-apply(  simp (no_asm_simp))
+apply(  frule class_Object)
+apply(  clarify)
+apply(  frule fields_rec, assumption)
+apply(  drule class_wf, assumption)
+apply(  simp add: wf_cdecl_def wf_fdecl_def)
+apply(  fastsimp)
 apply( subst fields_rec)
 apply(   fast)
 apply(  assumption)
@@ -405,24 +428,52 @@
   "[| 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"
+  assume wf: "wf_prog wf_mb G" and C:  "(C,S,fs,mdecls) \<in> set G" and
+         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)"
+  from wf C have "class G C = Some (S,fs,mdecls)"
     by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
+  moreover
+  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)
   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 simp add: is_class_def dest: method_rec)
 qed
 
+
+lemma wf_mb'E:
+  "\<lbrakk> wf_prog wf_mb G; \<And>C S fs ms m.\<lbrakk>(C,S,fs,ms) \<in> set G; m \<in> set ms\<rbrakk> \<Longrightarrow> wf_mb' G C m \<rbrakk>
+  \<Longrightarrow> wf_prog wf_mb' G"
+  apply (simp add: wf_prog_def)
+  apply auto
+  apply (simp add: wf_cdecl_def wf_mdecl_def)
+  apply safe
+  apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply clarify apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply clarify apply (drule bspec, assumption)+ apply simp
+  done
+
+
+lemma fst_mono: "A \<subseteq> B \<Longrightarrow> fst ` A \<subseteq> fst ` B" by fast
+
+lemma wf_syscls:
+  "set SystemClasses \<subseteq> set G \<Longrightarrow> wf_syscls G"
+  apply (drule fst_mono)
+  apply (simp add: SystemClasses_def wf_syscls_def)
+  apply (simp add: ObjectC_def) 
+  apply (rule allI, case_tac x)
+  apply (auto simp add: NullPointerC_def ClassCastC_def OutOfMemoryC_def)
+  done
+
 end