src/HOL/MicroJava/J/WellForm.thy

--- a/src/HOL/MicroJava/J/WellForm.thy	Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Sun Dec 16 00:18:17 2001 +0100
@@ -57,7 +57,7 @@
 done
 
 lemma class_Object [simp]: 
-	"wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])"
+  "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)
 done
@@ -205,13 +205,15 @@
 apply auto
 done
 
-lemma widen_fields_defpl: "[|((fn,fd),fT) \<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==>  
+lemma widen_fields_defpl: 
+  "[|((fn,fd),fT) \<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==>  
   G\<turnstile>C\<preceq>C fd"
 apply( drule (1) widen_fields_defpl')
 apply (fast)
 done
 
-lemma unique_fields: "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
+lemma unique_fields: 
+  "[|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)
@@ -232,7 +234,8 @@
 apply(auto dest!: widen_fields_defpl)
 done
 
-lemma fields_mono_lemma [rule_format (no_asm)]: "[|wf_prog wf_mb G; (C',C)\<in>(subcls1 G)^*|] ==>  
+lemma fields_mono_lemma [rule_format (no_asm)]: 
+  "[|wf_prog wf_mb G; (C',C)\<in>(subcls1 G)^*|] ==>  
   x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
 apply(erule converse_rtrancl_induct)
 apply( safe dest!: subcls1D)
@@ -260,7 +263,8 @@
 apply (fast dest: fields_mono)
 done
 
-lemma method_wf_mdecl [rule_format (no_asm)]: "wf_prog wf_mb G ==> is_class G C \<Longrightarrow>   
+lemma method_wf_mdecl [rule_format (no_asm)]: 
+  "wf_prog wf_mb G ==> is_class G C \<Longrightarrow>   
      method (G,C) sig = Some (md,mh,m) 
    --> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))"
 apply( erule subcls1_induct)
@@ -322,10 +326,13 @@
  "[| G\<turnstile> C\<preceq>C D; wf_prog wf_mb G;  
      method (G,D) sig = Some (md, rT, b) |]  
   ==> \<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
-apply(auto dest: subcls_widen_methd method_wf_mdecl simp add: wf_mdecl_def wf_mhead_def split_def)
+apply(auto dest: subcls_widen_methd method_wf_mdecl 
+           simp add: wf_mdecl_def wf_mhead_def split_def)
 done
 
-lemma method_in_md [rule_format (no_asm)]: "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)"
+lemma method_in_md [rule_format (no_asm)]: 
+  "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 (erule conjE)
@@ -366,7 +373,8 @@
 done
 
 
-lemma fields_is_type_lemma [rule_format (no_asm)]: "[|is_class G C; wf_prog wf_mb G|] ==>  
+lemma fields_is_type_lemma [rule_format (no_asm)]: 
+  "[|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))
@@ -385,7 +393,8 @@
 apply auto
 done
 
-lemma fields_is_type: "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==>  
+lemma fields_is_type: 
+  "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==>  
   is_type G f"
 apply(drule map_of_SomeD)
 apply(drule (2) fields_is_type_lemma)
@@ -401,31 +410,19 @@
 
   assume m: "(sig,rT,code) \<in> set mdecls"
   moreover
-  from wf
-  have "class G Object = Some (arbitrary, [], [])"
-    by simp 
+  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 c: "class G C = Some (S,fs,mdecls)"
     by (auto simp add: wf_prog_def class_def is_class_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
+  have O: "C \<noteq> Object" by 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)"
+  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)
+  show ?thesis by (auto simp add: is_class_def dest: method_rec)
 qed
 
 end