src/HOL/MicroJava/J/WellForm.ML

--- a/src/HOL/MicroJava/J/WellForm.ML	Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.ML	Fri Jul 14 16:32:51 2000 +0200
@@ -95,36 +95,50 @@
 by( etac subcls1I 1);
 qed "subcls1_induct";
 
-Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) = \
+Goal "\\<lbrakk>wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (Some D,fs,ms) \\<longrightarrow> is_class G D\\<rbrakk> \\<Longrightarrow> method (G,C) = \
 \ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
 \ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
 \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
 by( stac (method_TC RS (wf_subcls1_rel RS (hd method.simps))) 1);
+by( asm_simp_tac (simpset() addsplits[option.split]) 1);
+auto();
+qed "method_rec_lemma";
+
+Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) = \
+\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
+\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
+\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
+by(rtac method_rec_lemma 1);
 by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def] 
 		addsplits [option.split]) 1);
 by( case_tac "C = Object" 1);
-by(  Asm_full_simp_tac 1);
-by( dtac class_wf 1);
-by(  atac 1);
-by( dtac wf_cdecl_supD 1);
-by(  atac 1);
+by(  Force_tac 1);
+by Safe_tac;
+by( datac class_wf 1 1);
+by( datac wf_cdecl_supD 1 1);
 by( Asm_full_simp_tac 1);
 qed "method_rec";
 
+Goal "\\<lbrakk>wf ((subcls1 G)^-1); class G C = Some (sc,fs,ms); \\<forall>C. sc = Some C \\<longrightarrow> is_class G C\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
+\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
+\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
+by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
+by( asm_simp_tac (simpset() addsplits[option.split]) 1);
+qed "fields_rec_lemma";
+
 Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
 \ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
 \ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
-by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
-by( asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
+by(rtac fields_rec_lemma 1);
+by(   asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
+ba  1;
 by( option_case_tac2 "sc" 1);
 by(  Asm_simp_tac 1);
 by( case_tac "C = Object" 1);
 by(  rotate_tac 2 1);
 by(  Asm_full_simp_tac 1);
-by( dtac class_wf 1);
-by(  atac 1);
-by( dtac wf_cdecl_supD 1);
-by(  atac 1);
+by( datac class_wf 1 1);
+by( datac wf_cdecl_supD 1 1);
 by( Asm_full_simp_tac 1);
 qed "fields_rec";
 
@@ -211,12 +225,6 @@
 by( Asm_full_simp_tac 1);
 qed "unique_fields";
 
-(*####TO Trancl.ML*)
-Goal "(a,b):r^* ==> a=b | a~=b & (a,b):r^+";
-by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
-				  delsimps [reflcl_trancl]) 1);
-qed "rtranclD";
-
 Goal
 "\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
 \                          map_of (fields (G,C')) f = Some ft";