--- 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";