removed inj_eq from the default simpset again
authoroheimb
Mon Jan 03 14:07:08 2000 +0100 (2000-01-03)
changeset 8082381716a86fcb
parent 8081 1c8de414b45d
child 8083 f0d4165bc534
removed inj_eq from the default simpset again
src/HOL/MicroJava/J/Conform.ML
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/Eval.thy
src/HOL/MicroJava/J/JBasis.ML
src/HOL/MicroJava/J/JTypeSafe.ML
src/HOL/MicroJava/J/TypeRel.ML
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/WellForm.ML
src/HOL/MicroJava/J/WellForm.thy
src/HOL/MicroJava/J/WellType.ML
src/HOL/MicroJava/J/WellType.thy
     1.1 --- a/src/HOL/MicroJava/J/Conform.ML	Thu Dec 23 19:59:50 1999 +0100
     1.2 +++ b/src/HOL/MicroJava/J/Conform.ML	Mon Jan 03 14:07:08 2000 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4  	 ALLGOALS Asm_simp_tac]) RS mp;
     1.5  
     1.6  val conf_widen = prove_goalw thy [conf_def] 
     1.7 -"\\<And>G. wf_prog wtm G \\<Longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T \\<longrightarrow> G\\<turnstile>T\\<preceq>T' \\<longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T'" (K [
     1.8 +"\\<And>G. wf_prog wf_mb G \\<Longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T \\<longrightarrow> G\\<turnstile>T\\<preceq>T' \\<longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T'" (K [
     1.9  	rtac val_.induct 1,
    1.10  	    ALLGOALS Simp_tac,
    1.11  	    ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp;
    1.12 @@ -120,7 +120,7 @@
    1.13  \ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>Class C'\\<preceq>Class C)" 
    1.14  	(K[fast_tac (HOL_cs addDs [non_npD]) 1]);
    1.15  
    1.16 -Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wtm G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
    1.17 +Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wf_mb G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
    1.18  \ (\\<forall>C. t = ClassT C \\<longrightarrow> C \\<noteq> Object) \\<longrightarrow> \
    1.19  \ (\\<exists>a C fs. a' = Addr a \\<and>  h a = Some (C,fs) \\<and>  G\\<turnstile>Class C\\<preceq>RefT t)";
    1.20  by (rtac impI 1);
    1.21 @@ -134,7 +134,7 @@
    1.22  by  (Fast_tac 1);
    1.23  qed_spec_mp "non_np_objD'";
    1.24  
    1.25 -Goal "wf_prog wtm G \\<Longrightarrow> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts \\<longrightarrow> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' \\<longrightarrow>  list_all2 (conf G h) vs Ts'";
    1.26 +Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts \\<longrightarrow> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' \\<longrightarrow>  list_all2 (conf G h) vs Ts'";
    1.27  by( induct_tac "vs" 1);
    1.28  by(  ALLGOALS Clarsimp_tac);
    1.29  by(  ALLGOALS (forward_tac [list_all2_lengthD RS sym]));
     2.1 --- a/src/HOL/MicroJava/J/Conform.thy	Thu Dec 23 19:59:50 1999 +0100
     2.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Mon Jan 03 14:07:08 2000 +0100
     2.3 @@ -26,7 +26,7 @@
     2.4    hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool"             ("_\\<turnstile>h _\\<surd>"      [51,51]       50)
     2.5   "G\\<turnstile>h h\\<surd>    \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
     2.6  
     2.7 -  conforms :: "state \\<Rightarrow> javam env \\<Rightarrow> bool"	 ("_\\<Colon>\\<preceq>_"       [51,51]       50)
     2.8 +  conforms :: "state \\<Rightarrow> java_mb env \\<Rightarrow> bool"	 ("_\\<Colon>\\<preceq>_"       [51,51]       50)
     2.9   "s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
    2.10  
    2.11  end
     3.1 --- a/src/HOL/MicroJava/J/Eval.thy	Thu Dec 23 19:59:50 1999 +0100
     3.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Mon Jan 03 14:07:08 2000 +0100
     3.3 @@ -10,15 +10,15 @@
     3.4  Eval = State + 
     3.5  
     3.6  consts
     3.7 -  eval  :: "javam prog \\<Rightarrow> (xstate \\<times> expr      \\<times> val      \\<times> xstate) set"
     3.8 -  evals :: "javam prog \\<Rightarrow> (xstate \\<times> expr list \\<times> val list \\<times> xstate) set"
     3.9 -  exec  :: "javam prog \\<Rightarrow> (xstate \\<times> stmt                 \\<times> xstate) set"
    3.10 +  eval  :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr      \\<times> val      \\<times> xstate) set"
    3.11 +  evals :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr list \\<times> val list \\<times> xstate) set"
    3.12 +  exec  :: "java_mb prog \\<Rightarrow> (xstate \\<times> stmt                 \\<times> xstate) set"
    3.13  
    3.14  syntax
    3.15 -  eval :: "[javam prog,xstate,expr,val,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<succ>_\\<rightarrow> _"[51,82,82,82,82]81)
    3.16 -  evals:: "[javam prog,xstate,expr list,
    3.17 +  eval :: "[java_mb prog,xstate,expr,val,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<succ>_\\<rightarrow> _"[51,82,82,82,82]81)
    3.18 +  evals:: "[java_mb prog,xstate,expr list,
    3.19  	                      val list,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_[\\<succ>]_\\<rightarrow> _"[51,82,51,51,82]81)
    3.20 -  exec :: "[javam prog,xstate,stmt,    xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _"  [51,82,82,   82]81)
    3.21 +  exec :: "[java_mb prog,xstate,stmt,    xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _"  [51,82,82,   82]81)
    3.22  
    3.23  translations
    3.24    "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" == "(s, e, v, _args x s') \\<in> eval  G"
     4.1 --- a/src/HOL/MicroJava/J/JBasis.ML	Thu Dec 23 19:59:50 1999 +0100
     4.2 +++ b/src/HOL/MicroJava/J/JBasis.ML	Mon Jan 03 14:07:08 2000 +0100
     4.3 @@ -67,6 +67,10 @@
     4.4  		rotate_tac ~1,asm_full_simp_tac 
     4.5  	(simpset() delsimps [split_paired_All,split_paired_Ex])];
     4.6  
     4.7 +Goal "{y. x = Some y} \\<subseteq> {the x}";
     4.8 +by Auto_tac;
     4.9 +qed "some_subset_the";
    4.10 +
    4.11  fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1,
    4.12    asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];
    4.13  
    4.14 @@ -114,7 +118,7 @@
    4.15  
    4.16  Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)";
    4.17  by (induct_tac "l" 1);
    4.18 -by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
    4.19 +by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq]));
    4.20  qed_spec_mp "unique_map_inj";
    4.21  
    4.22  Goal "\\<And>l. unique l \\<Longrightarrow> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
     5.1 --- a/src/HOL/MicroJava/J/JTypeSafe.ML	Thu Dec 23 19:59:50 1999 +0100
     5.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Mon Jan 03 14:07:08 2000 +0100
     5.3 @@ -8,7 +8,7 @@
     5.4  
     5.5  Addsimps [split_beta];
     5.6  
     5.7 -Goal "\\<lbrakk>h a = None; (h, l)\\<Colon>\\<preceq>(G, lT); wf_prog wtm G; is_class G C\\<rbrakk> \\<Longrightarrow> \
     5.8 +Goal "\\<lbrakk>h a = None; (h, l)\\<Colon>\\<preceq>(G, lT); wf_prog wf_mb G; is_class G C\\<rbrakk> \\<Longrightarrow> \
     5.9  \ (h(a\\<mapsto>(C,(init_vars (fields (G,C))))), l)\\<Colon>\\<preceq>(G, lT)";
    5.10  by( etac conforms_upd_obj 1);
    5.11  by(  rewtac oconf_def);
    5.12 @@ -16,7 +16,7 @@
    5.13  qed "NewC_conforms";
    5.14  
    5.15  Goalw [cast_ok_def]
    5.16 - "\\<lbrakk> wf_prog wtm G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<Rightarrow>? T'; cast_ok G T' h v\\<rbrakk> \
    5.17 + "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<Rightarrow>? T'; cast_ok G T' h v\\<rbrakk> \
    5.18  \ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
    5.19  by( case_tac1 "v = Null" 1);
    5.20  by(  Asm_full_simp_tac 1);
    5.21 @@ -44,7 +44,7 @@
    5.22  by     Auto_tac;
    5.23  qed "Cast_conf";
    5.24  
    5.25 -Goal "\\<lbrakk> wf_prog wtm G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
    5.26 +Goal "\\<lbrakk> wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
    5.27  \    x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \
    5.28  \ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))\\<Colon>\\<preceq>ft";
    5.29  by( dtac np_NoneD 1);
    5.30 @@ -60,10 +60,10 @@
    5.31  by( dtac oconf_objD 1);
    5.32  by(  atac 1);
    5.33  by Auto_tac;
    5.34 -val FAcc_type_sound = result();
    5.35 +qed "FAcc_type_sound";
    5.36  
    5.37  Goal
    5.38 - "\\<lbrakk> wf_prog wtm G; a = the_Addr a'; (c, fs) = the (h a); \
    5.39 + "\\<lbrakk> wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); \
    5.40  \   (G, lT)\\<turnstile>v\\<Colon>T'; G\\<turnstile>T'\\<preceq>ft; \
    5.41  \   (G, lT)\\<turnstile>aa\\<Colon>Class C; \
    5.42  \   field (G,C) fn = Some (fd, ft); h''\\<le>|h'; \
    5.43 @@ -105,9 +105,9 @@
    5.44  by(  Asm_full_simp_tac 1);
    5.45  by(  fast_tac (HOL_cs addIs [conf_widen]) 1);
    5.46  by( fast_tac (HOL_cs addDs [conforms_heapD RS hconfD, oconf_objD]) 1);
    5.47 -val FAss_type_sound = result();
    5.48 +qed "FAss_type_sound";
    5.49  
    5.50 -Goalw [wf_mhead_def] "\\<lbrakk> wf_prog wtm G; list_all2 (conf G h) pvs pTs; \
    5.51 +Goalw [wf_mhead_def] "\\<lbrakk> wf_prog wf_mb G; list_all2 (conf G h) pvs pTs; \
    5.52   \ list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT; \
    5.53  \ length pTs' = length pns; nodups pns; \
    5.54  \ Ball (set lvars) (split (\\<lambda>vn. is_type G)) \
    5.55 @@ -145,7 +145,7 @@
    5.56  by( EVERY'[forward_tac [hext_objD], atac] 1);
    5.57  by( Clarsimp_tac 1);
    5.58  by( EVERY'[dtac Call_lemma, atac, atac] 1);
    5.59 -by( clarsimp_tac (claset(),simpset() addsimps [wt_java_mdecl_def])1);
    5.60 +by( clarsimp_tac (claset(),simpset() addsimps [wf_java_mdecl_def])1);
    5.61  by( thin_tac "method ?sig ?x = ?y" 1);
    5.62  by( EVERY'[dtac spec, etac impE] 1);
    5.63  by(  mp_tac 2);
     6.1 --- a/src/HOL/MicroJava/J/TypeRel.ML	Thu Dec 23 19:59:50 1999 +0100
     6.2 +++ b/src/HOL/MicroJava/J/TypeRel.ML	Mon Jan 03 14:07:08 2000 +0100
     6.3 @@ -14,12 +14,6 @@
     6.4  \ (SIGMA C:{C. is_class G C} . {D. fst (the (class G C)) = Some D})"
     6.5   (K [Auto_tac]);
     6.6  
     6.7 -context Option.thy;
     6.8 -Goal "{y. x = Some y} \\<subseteq> {the x}";
     6.9 -by Auto_tac;
    6.10 -val some_subset_the = result();
    6.11 -context thy;
    6.12 -
    6.13  Goal "finite (subcls1 G)";
    6.14  by(stac subcls1_def2 1);
    6.15  by( rtac finite_SigmaI 1);
    6.16 @@ -38,21 +32,11 @@
    6.17  	auto_tac (claset() addDs lemmata, simpset())]);
    6.18  
    6.19  
    6.20 -(*#### patch for Isabelle98-1*)
    6.21 -val major::prems = goal Trancl.thy
    6.22 - "\\<lbrakk> (x,y) \\<in> r^+; \
    6.23 -\    \\<And>x y. (x,y) \\<in> r \\<Longrightarrow> P x y; \
    6.24 -\    \\<And>x y z. \\<lbrakk> (x,y) \\<in> r^+; P x y; (y,z) \\<in> r^+; P y z \\<rbrakk> \\<Longrightarrow> P x z \
    6.25 -\ \\<rbrakk> \\<Longrightarrow> P x y";
    6.26 -by(blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
    6.27 -qed "trancl_trans_induct";
    6.28 -
    6.29 -Goalw [is_class_def] "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> is_class G C";
    6.30 +Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ \\<Longrightarrow> is_class G C";
    6.31  by(etac trancl_trans_induct 1);
    6.32  by (auto_tac (HOL_cs addSDs [subcls1D],simpset()));
    6.33  qed "subcls_is_class";
    6.34  
    6.35 -
    6.36  (* A particular thm about wf;
    6.37     looks like it is an odd instance of something more general
    6.38  *)
    6.39 @@ -66,7 +50,7 @@
    6.40  by (Fast_tac 1);
    6.41  by(rewrite_goals_tac [wf_def]);
    6.42  by(Blast_tac 1);
    6.43 -val wf_rel_lemma = result();
    6.44 +qed "wf_rel_lemma";
    6.45  
    6.46  
    6.47  (* Proving the termination conditions *)
    6.48 @@ -74,7 +58,7 @@
    6.49  goalw thy [subcls1_rel_def] "wf subcls1_rel";
    6.50  by(rtac (wf_rel_lemma RS wf_subset) 1);
    6.51  by(Force_tac 1);
    6.52 -val wf_subcls1_rel = result();
    6.53 +qed "wf_subcls1_rel";
    6.54  
    6.55  val method_TC = prove_goalw_cterm [subcls1_rel_def]
    6.56   (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (method.tcs)))))
    6.57 @@ -111,21 +95,19 @@
    6.58  val widen_Class_NullT = prove_typerel "G\\<turnstile>Class C\\<preceq>RefT NullT \\<Longrightarrow> R" 
    6.59   [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT NullT \\<longrightarrow> R"];
    6.60  
    6.61 -val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>Class cm \\<Longrightarrow> C=cm |  G\\<turnstile>C\\<prec>C cm"
    6.62 -[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> C=cm |  G\\<turnstile>C\\<prec>C cm"];
    6.63 +val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>Class cm \\<Longrightarrow> G\\<turnstile>C\\<prec>C cm"
    6.64 +[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> G\\<turnstile>C\\<prec>C cm"];
    6.65  
    6.66 -Goal "\\<lbrakk>G\\<turnstile>S\\<preceq>U; \\<forall>C. is_class G C \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object;\
    6.67 -\\\<forall>C. G\\<turnstile>Object\\<prec>C C \\<longrightarrow> False \\<rbrakk> \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
    6.68 +Goal "G\\<turnstile>S\\<preceq>U \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
    6.69  by( etac widen.induct 1);
    6.70  by   Safe_tac;
    6.71  by(  ALLGOALS (forward_tac [widen_Class, widen_RefT]));
    6.72  by  Safe_tac;
    6.73  by(  rtac widen.null 2);
    6.74 -by( forward_tac [widen_Class_Class] 1);
    6.75 -by Safe_tac;
    6.76 -by(  ALLGOALS(EVERY'[etac thin_rl,etac thin_rl,
    6.77 -	fast_tac (claset() addIs [widen.subcls,trancl_trans])]));
    6.78 -qed_spec_mp "widen_trans_lemma";
    6.79 +by(dtac widen_Class_Class 1);
    6.80 +by(rtac widen.subcls 1);
    6.81 +by(eatac rtrancl_trans 1 1);
    6.82 +qed_spec_mp "widen_trans";
    6.83  
    6.84  
    6.85  val prove_cast_lemma = prove_typerel_lemma [] cast.elim;
     7.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Thu Dec 23 19:59:50 1999 +0100
     7.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Jan 03 14:07:08 2000 +0100
     7.3 @@ -21,7 +21,7 @@
     7.4  
     7.5  translations
     7.6    	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
     7.7 -	"G\\<turnstile>C \\<prec>C  D" == "(C,D) \\<in> (subcls1 G)^+"
     7.8 +	"G\\<turnstile>C \\<prec>C  D" == "(C,D) \\<in> (subcls1 G)^*"
     7.9  	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    7.10  	"G\\<turnstile>S \\<Rightarrow>?  T" == "(S,T) \\<in> cast    G"
    7.11  
     8.1 --- a/src/HOL/MicroJava/J/WellForm.ML	Thu Dec 23 19:59:50 1999 +0100
     8.2 +++ b/src/HOL/MicroJava/J/WellForm.ML	Mon Jan 03 14:07:08 2000 +0100
     8.3 @@ -5,76 +5,63 @@
     8.4  *)
     8.5  
     8.6  val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def]
     8.7 - "\\<And>X. \\<lbrakk>class G C = Some c; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> wf_cdecl wtm G (C,c)" (K [
     8.8 + "\\<And>X. \\<lbrakk>class G C = Some c; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wf_cdecl wf_mb G (C,c)" (K [
     8.9  	Asm_full_simp_tac 1,
    8.10  	fast_tac (set_cs addDs [get_in_set]) 1]);
    8.11  
    8.12  val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def]
    8.13 -	"\\<And>X. wf_prog wtm G \\<Longrightarrow> class G Object = Some (None, [], [])" (K [
    8.14 +	"\\<And>X. wf_prog wf_mb G \\<Longrightarrow> class G Object = Some (None, [], [])" (K [
    8.15  	safe_tac set_cs,
    8.16  	dtac in_set_get 1,
    8.17  	 Auto_tac]);
    8.18  Addsimps [class_Object];
    8.19  
    8.20  val is_class_Object = prove_goalw thy [is_class_def] 
    8.21 -	"\\<And>X. wf_prog wtm G \\<Longrightarrow> is_class G Object" (K [Asm_simp_tac 1]);
    8.22 +	"\\<And>X. wf_prog wf_mb G \\<Longrightarrow> is_class G Object" (K [Asm_simp_tac 1]);
    8.23  Addsimps [is_class_Object];
    8.24  
    8.25 -Goal "\\<lbrakk>G\\<turnstile>C\\<prec>C1D; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> D \\<noteq> C \\<and> \\<not>  G\\<turnstile>D\\<prec>C C";
    8.26 +Goal "\\<lbrakk>G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> D \\<noteq> C \\<and> \\<not>(D,C)\\<in>(subcls1 G)^+";
    8.27  by( forward_tac [r_into_trancl] 1);
    8.28  by( dtac subcls1D 1);
    8.29  by( strip_tac1 1);
    8.30 -by( dtac class_wf 1);
    8.31 -by(  atac 1);
    8.32 +by( datac class_wf 1 1);
    8.33  by( rewtac wf_cdecl_def);
    8.34 -by( Clarsimp_tac 1);
    8.35 +by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
    8.36 +				  delsimps [reflcl_trancl]) 1);
    8.37  qed "subcls1_wfD";
    8.38  
    8.39  val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def] 
    8.40 -"\\<And>X. \\<lbrakk>wf_cdecl wtm G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
    8.41 +"\\<And>X. \\<lbrakk>wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
    8.42  	pair_tac "r" 1,
    8.43  	Asm_full_simp_tac 1,
    8.44  	strip_tac1 1,
    8.45  	option_case_tac 1,
    8.46  	Fast_tac 1]);
    8.47  
    8.48 -local
    8.49 -val lemma = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> C=Object \\<longrightarrow> R" (K [
    8.50 -	etac trancl_trans_induct 1,
    8.51 -	 atac 2,
    8.52 -	rewtac subcls1_def,
    8.53 -	Auto_tac]);
    8.54 -in
    8.55 -val subcls_Object = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>Object\\<prec>C C\\<rbrakk> \\<Longrightarrow> R" (K [
    8.56 -	etac (lemma RS mp) 1,
    8.57 -	Auto_tac]);
    8.58 -end;
    8.59 -
    8.60 -Goal "\\<lbrakk>wf_prog wt G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> \\<not>  G\\<turnstile>D\\<prec>C C";
    8.61 +Goal "\\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> \\<not>(D,C)\\<in>(subcls1 G)^+";
    8.62  by(etac tranclE 1);
    8.63 -by(ALLGOALS(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
    8.64 +by(TRYALL(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
    8.65  qed "subcls_asym";
    8.66  
    8.67 -val subcls_irrefl = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> C \\<noteq> D" (K [
    8.68 +val subcls_irrefl = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> C \\<noteq> D" (K [
    8.69  	etac trancl_trans_induct 1,
    8.70  	 fast_tac (HOL_cs addDs [subcls1_wfD]) 1,
    8.71  	fast_tac (HOL_cs addDs [subcls_asym]) 1]);
    8.72  
    8.73  val acyclic_subcls1 = prove_goalw thy [acyclic_def] 
    8.74 -	"\\<And>X. wf_prog wt G \\<Longrightarrow> acyclic (subcls1 G)" (K [
    8.75 +	"\\<And>X. wf_prog wf_mb G \\<Longrightarrow> acyclic (subcls1 G)" (K [
    8.76  	strip_tac1 1,
    8.77  	fast_tac (HOL_cs addDs [subcls_irrefl]) 1]);
    8.78  
    8.79 -val wf_subcls1 = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> wf ((subcls1 G)^-1)" (K [
    8.80 +val wf_subcls1 = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> wf ((subcls1 G)^-1)" (K [
    8.81  	rtac finite_acyclic_wf 1,
    8.82  	 stac finite_converse 1,
    8.83  	 rtac finite_subcls1 1,
    8.84  	stac acyclic_converse 1,
    8.85  	etac acyclic_subcls1 1]);
    8.86  
    8.87 -
    8.88  val major::prems = goal thy
    8.89 -  "\\<lbrakk>wf_prog wt G; \\<And>C. \\<forall>D. G\\<turnstile>C\\<prec>C D \\<longrightarrow> P D \\<Longrightarrow> P C\\<rbrakk> \\<Longrightarrow> P C";
    8.90 +  "\\<lbrakk>wf_prog wf_mb G; \\<And>C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ \\<longrightarrow> P D \\<Longrightarrow> P C\\<rbrakk> \\<Longrightarrow> P C";
    8.91  by(cut_facts_tac [major RS wf_subcls1] 1);
    8.92  by(dtac wf_trancl 1);
    8.93  by(asm_full_simp_tac (HOL_ss addsimps [trancl_converse]) 1);
    8.94 @@ -83,9 +70,9 @@
    8.95  by(Auto_tac);
    8.96  qed "subcls_induct";
    8.97  
    8.98 -val prems = goal thy "\\<lbrakk>is_class G C; wf_prog wtm G; P Object; \
    8.99 +val prems = goal thy "\\<lbrakk>is_class G C; wf_prog wf_mb G; P Object; \
   8.100  \\\<And>C D fs ms. \\<lbrakk>C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
   8.101 -\   wf_cdecl wtm G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D\\<rbrakk> \\<Longrightarrow> P C\
   8.102 +\   wf_cdecl wf_mb G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D\\<rbrakk> \\<Longrightarrow> P C\
   8.103  \ \\<rbrakk> \\<Longrightarrow> P C";
   8.104  by( cut_facts_tac prems 1);
   8.105  by( rtac impE 1);
   8.106 @@ -111,7 +98,7 @@
   8.107  by( etac subcls1I 1);
   8.108  qed "subcls1_induct";
   8.109  
   8.110 -Goal "wf_prog wtm G \\<Longrightarrow> method (G,C) = \
   8.111 +Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) = \
   8.112  \ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
   8.113  \ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
   8.114  \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
   8.115 @@ -125,9 +112,9 @@
   8.116  by( dtac wf_cdecl_supD 1);
   8.117  by(  atac 1);
   8.118  by( Asm_full_simp_tac 1);
   8.119 -val method_rec = result();
   8.120 +qed "method_rec";
   8.121  
   8.122 -Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wtm G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
   8.123 +Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
   8.124  \ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
   8.125  \ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
   8.126  by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.rules))) 1);
   8.127 @@ -142,57 +129,43 @@
   8.128  by( dtac wf_cdecl_supD 1);
   8.129  by(  atac 1);
   8.130  by( Asm_full_simp_tac 1);
   8.131 -val fields_rec = result();
   8.132 +qed "fields_rec";
   8.133  
   8.134 -val method_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> method (G,Object) = empty"
   8.135 +val method_Object = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> method (G,Object) = empty"
   8.136  	(K [stac method_rec 1,Auto_tac]);
   8.137 -val fields_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> fields (G,Object) = []"(K [
   8.138 +val fields_Object = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> fields (G,Object) = []"(K [
   8.139  	stac fields_rec 1,Auto_tac]);
   8.140  Addsimps [method_Object, fields_Object];
   8.141  val field_Object = prove_goalw thy [field_def]
   8.142 - "\\<And>X. wf_prog wtm G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);
   8.143 + "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);
   8.144  Addsimps [field_Object];
   8.145  
   8.146 -val subcls_C_Object = prove_goal thy 
   8.147 -	"\\<And>X. \\<lbrakk>is_class G C; wf_prog wtm G \\<rbrakk> \\<Longrightarrow> C \\<noteq> Object \\<longrightarrow> G\\<turnstile>C\\<prec>C Object" (K [
   8.148 -	etac subcls1_induct 1,
   8.149 -	  atac 1,
   8.150 -	 Fast_tac 1,
   8.151 -	safe_tac (HOL_cs addSDs [wf_cdecl_supD] addss (simpset())),
   8.152 -	 fast_tac (HOL_cs addIs [r_into_trancl]) 1,
   8.153 -	rtac trancl_trans 1,
   8.154 -	 atac 2,
   8.155 -	rtac r_into_trancl 1,
   8.156 -	rtac subcls1I 1,
   8.157 -	ALLGOALS Asm_simp_tac]) RS mp;
   8.158 +Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C Object";
   8.159 +by(etac subcls1_induct 1);
   8.160 +by(  atac 1);
   8.161 +by( Fast_tac 1);
   8.162 +by(auto_tac (HOL_cs addSDs [wf_cdecl_supD], simpset()));
   8.163 +by(eatac rtrancl_into_rtrancl2 1 1);
   8.164 +qed "subcls_C_Object";
   8.165  
   8.166  val is_type_rTI = prove_goalw thy [wf_mhead_def]
   8.167  	"\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"
   8.168  	(K [split_all_tac 1, Auto_tac]);
   8.169  
   8.170 -val widen_Class_Object = prove_goal thy 
   8.171 -	"\\<lbrakk>wf_prog wtm G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object" (fn prems => [
   8.172 -	cut_facts_tac prems 1,
   8.173 -	case_tac "C=Object" 1,
   8.174 -	 hyp_subst_tac 1,
   8.175 -	 Asm_simp_tac 1,
   8.176 -	rtac widen.subcls 1,
   8.177 -	fast_tac (HOL_cs addEs [subcls_C_Object]) 1]);
   8.178 +Goal "\\<lbrakk>wf_prog wf_mb G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object";
   8.179 +by(rtac widen.subcls 1);	
   8.180 +by(eatac subcls_C_Object 1 1);
   8.181 +qed "widen_Class_Object";
   8.182  
   8.183 -val widen_trans = prove_goal thy "\\<lbrakk>wf_prog wtm G; G\\<turnstile>S\\<preceq>U; G\\<turnstile>U\\<preceq>T\\<rbrakk> \\<Longrightarrow> G\\<turnstile>S\\<preceq>T"
   8.184 -(fn prems=> [cut_facts_tac prems 1, 
   8.185 -	fast_tac (HOL_cs addEs [widen_trans_lemma, widen_Class_Object, 
   8.186 -				subcls_Object]) 1]);
   8.187 +Goal "\\<lbrakk>(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
   8.188 +\ x \\<in> set (fields (G,C)) \\<longrightarrow> x \\<in> set (fields (G,C'))";
   8.189 +by(etac trancl_trans_induct 1);
   8.190 +by( safe_tac (HOL_cs addSDs [subcls1D]));
   8.191 +by(stac fields_rec 1);
   8.192 +by(  Auto_tac);
   8.193 +qed_spec_mp "fields_mono";
   8.194  
   8.195 -val fields_mono = prove_goal thy 
   8.196 -"\\<And>X. \\<lbrakk>G\\<turnstile>C'\\<prec>C C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
   8.197 -\ x \\<in> set (fields (G,C)) \\<longrightarrow> x \\<in> set (fields (G,C'))" (K [
   8.198 -	etac trancl_trans_induct 1,
   8.199 -	 safe_tac (HOL_cs addSDs [subcls1D]),
   8.200 -	stac fields_rec 1,
   8.201 -	  Auto_tac]) RS mp;
   8.202 -
   8.203 -Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
   8.204 +Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
   8.205  \ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>Class C\\<preceq>Class fd";
   8.206  by( etac subcls1_induct 1);
   8.207  by(   atac 1);
   8.208 @@ -209,24 +182,22 @@
   8.209  by(  dtac split_Pair_eq 1);
   8.210  by(  SELECT_GOAL (Auto_tac) 1);
   8.211  by( rtac widen_trans 1);
   8.212 -by(   atac 1);
   8.213 -by(  etac (r_into_trancl RS widen.subcls) 1);
   8.214 +by(  etac (r_into_rtrancl RS widen.subcls) 1);
   8.215  by( etac BallE 1);
   8.216  by(  contr_tac 1);
   8.217  by( Asm_full_simp_tac 1);
   8.218 -val widen_fields_defpl' = result();
   8.219 +qed "widen_fields_defpl'";
   8.220  
   8.221 -Goal "\\<lbrakk>is_class G C; wf_prog wtm G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
   8.222 +Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
   8.223  \ G\\<turnstile>Class C\\<preceq>Class fd";
   8.224 -by( dtac widen_fields_defpl' 1);
   8.225 -by(  atac 1);
   8.226 +by( datac widen_fields_defpl' 1 1);
   8.227  (*###################*)
   8.228  by( dtac bspec 1);
   8.229  auto();
   8.230 -val widen_fields_defpl = result();
   8.231 +qed "widen_fields_defpl";
   8.232  
   8.233  
   8.234 -Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> unique (fields (G,C))";
   8.235 +Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> unique (fields (G,C))";
   8.236  by( etac subcls1_induct 1);
   8.237  by(   atac 1);
   8.238  by(  safe_tac (HOL_cs addSDs [wf_cdecl_supD]));
   8.239 @@ -247,21 +218,27 @@
   8.240  by( Asm_full_simp_tac 1);
   8.241  by( dtac split_Pair_eq 1);
   8.242  by( fast_tac (HOL_cs addSDs [widen_Class_Class]) 1);
   8.243 -val unique_fields = result();
   8.244 +qed "unique_fields";
   8.245 +
   8.246 +(*####TO Trancl.ML*)
   8.247 +Goal "(a,b):r^* ==> a=b | a~=b & (a,b):r^+";
   8.248 +by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
   8.249 +				  delsimps [reflcl_trancl]) 1);
   8.250 +qed "rtranclD";
   8.251  
   8.252  Goal
   8.253 -"\\<lbrakk>wf_prog wtm G; G\\<turnstile>Class C'\\<preceq>Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
   8.254 +"\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>Class C'\\<preceq>Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
   8.255  \                          map_of (fields (G,C')) f = Some ft";
   8.256  by( dtac widen_Class_Class 1);
   8.257 -by( etac disjE 1);
   8.258 -by(  Asm_simp_tac 1);
   8.259 +by( dtac rtranclD 1);
   8.260 +by( Auto_tac);
   8.261  by( rtac table_mono 1);
   8.262  by(   atac 3);
   8.263  by(  rtac unique_fields 1);
   8.264  by(   etac subcls_is_class 1);
   8.265  by(  atac 1);
   8.266  by( fast_tac (HOL_cs addEs [fields_mono]) 1);
   8.267 -val widen_fields_mono = result();
   8.268 +qed "widen_fields_mono";
   8.269  
   8.270  
   8.271  val cfs_fields_lemma = prove_goalw thy [field_def] 
   8.272 @@ -269,11 +246,11 @@
   8.273  (K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
   8.274  
   8.275  val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\
   8.276 -\  G\\<turnstile>Class C'\\<preceq>Class C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
   8.277 +\  G\\<turnstile>Class C'\\<preceq>Class C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
   8.278  fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
   8.279  
   8.280 -Goal "wf_prog wtm G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
   8.281 -\  \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class md \\<and> wf_mdecl wtm G md (sig,(mh,m))";
   8.282 +Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
   8.283 +\  \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
   8.284  by( case_tac "is_class G C" 1);
   8.285  by(  forw_inst_tac [("C","C")] method_rec 2);
   8.286  by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
   8.287 @@ -290,21 +267,24 @@
   8.288  by(  thin_tac "?P \\<longrightarrow> ?Q" 1);
   8.289  by(  Clarify_tac 2);
   8.290  by(  rtac widen_trans 2);
   8.291 -by(    atac 2);
   8.292  by(   atac 3);
   8.293  by(  rtac widen.subcls 2);
   8.294 -by(  rtac r_into_trancl 2);
   8.295 +by(  rtac r_into_rtrancl 2);
   8.296  by(  fast_tac (HOL_cs addIs [subcls1I]) 2);
   8.297  by( forward_tac [table_mapf_SomeD] 1);
   8.298  by( strip_tac1 1);
   8.299  by( Asm_full_simp_tac 1);
   8.300  by( rewtac wf_cdecl_def);
   8.301  by( Asm_full_simp_tac 1);
   8.302 -val method_wf_mdecl = result() RS mp;
   8.303 +qed_spec_mp "method_wf_mdecl";
   8.304  
   8.305 -Goal "\\<lbrakk>G\\<turnstile>T\\<prec>C T'; wf_prog wt G\\<rbrakk> \\<Longrightarrow> \
   8.306 +Goal "\\<lbrakk>G\\<turnstile>T\\<prec>C T'; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
   8.307  \  \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
   8.308  \ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
   8.309 +by( dtac rtranclD 1);
   8.310 +by( etac disjE 1);
   8.311 +by(  Fast_tac 1);
   8.312 +by( etac conjE 1);
   8.313  by( etac trancl_trans_induct 1);
   8.314  by(  strip_tac1 2);
   8.315  by(  EVERY[dtac spec 2, dtac spec 2, dtac spec 2, mp_tac 2]);
   8.316 @@ -333,7 +313,7 @@
   8.317  
   8.318  
   8.319  Goal
   8.320 - "\\<lbrakk> G\\<turnstile>Class C\\<preceq>Class D; wf_prog wt G; \
   8.321 + "\\<lbrakk> G\\<turnstile>Class C\\<preceq>Class D; wf_prog wf_mb G; \
   8.322  \    method (G,D) sig = Some (md, rT, b) \\<rbrakk> \
   8.323  \ \\<Longrightarrow> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
   8.324  by(auto_tac (claset() addSDs [widen_Class_Class]
   8.325 @@ -342,7 +322,7 @@
   8.326  qed "subtype_widen_methd";
   8.327  
   8.328  
   8.329 -Goal "wf_prog wt G \\<Longrightarrow> \\<forall>D. method (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
   8.330 +Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>D. method (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
   8.331  by( case_tac "is_class G C" 1);
   8.332  by(  forw_inst_tac [("C","C")] method_rec 2);
   8.333  by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
   8.334 @@ -362,9 +342,8 @@
   8.335   by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);
   8.336  qed_spec_mp "method_in_md";
   8.337  
   8.338 -writeln"OK";
   8.339  
   8.340 -Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
   8.341 +Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
   8.342  \ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
   8.343  by( etac subcls1_induct 1);
   8.344  by(   atac 1);
   8.345 @@ -385,4 +364,4 @@
   8.346  by( rewtac wf_fdecl_def);
   8.347  by( split_all_tac 1);
   8.348  by( Asm_full_simp_tac 1);
   8.349 -val is_type_fields = result() RS bspec;
   8.350 +bind_thm ("is_type_fields", result() RS bspec);
     9.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Thu Dec 23 19:59:50 1999 +0100
     9.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Mon Jan 03 14:07:08 2000 +0100
     9.3 @@ -16,7 +16,7 @@
     9.4  
     9.5  WellForm = TypeRel +
     9.6  
     9.7 -types 'c wtm = 'c prog => cname => 'c mdecl => bool
     9.8 +types 'c wf_mb = 'c prog => cname => 'c mdecl => bool
     9.9  
    9.10  constdefs
    9.11  
    9.12 @@ -26,22 +26,22 @@
    9.13   wf_mhead	:: "'c prog \\<Rightarrow> sig   \\<Rightarrow> ty \\<Rightarrow> bool"
    9.14  "wf_mhead G \\<equiv> \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
    9.15  
    9.16 - wf_mdecl	:: "'c wtm \\<Rightarrow> 'c wtm"
    9.17 -"wf_mdecl wtm G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wtm G C (sig,rT,mb)"
    9.18 + wf_mdecl	:: "'c wf_mb \\<Rightarrow> 'c wf_mb"
    9.19 +"wf_mdecl wf_mb G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
    9.20  
    9.21 -  wf_cdecl	:: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
    9.22 -"wf_cdecl wtm G \\<equiv>
    9.23 +  wf_cdecl	:: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
    9.24 +"wf_cdecl wf_mb G \\<equiv>
    9.25     \\<lambda>(C,(sc,fs,ms)).
    9.26  	(\\<forall>f\\<in>set fs. wf_fdecl G   f    ) \\<and>  unique fs \\<and>
    9.27 -	(\\<forall>m\\<in>set ms. wf_mdecl wtm G C m) \\<and>  unique ms \\<and>
    9.28 +	(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and>  unique ms \\<and>
    9.29  	(case sc of None \\<Rightarrow> C = Object
    9.30           | Some D \\<Rightarrow>
    9.31               is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<prec>C C \\<and>
    9.32               (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
    9.33                   method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
    9.34  
    9.35 - wf_prog	:: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> bool"
    9.36 -"wf_prog wtm G \\<equiv>
    9.37 -   let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wtm G c) \\<and> unique G"
    9.38 + wf_prog	:: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> bool"
    9.39 +"wf_prog wf_mb G \\<equiv>
    9.40 +   let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
    9.41  
    9.42  end
    10.1 --- a/src/HOL/MicroJava/J/WellType.ML	Thu Dec 23 19:59:50 1999 +0100
    10.2 +++ b/src/HOL/MicroJava/J/WellType.ML	Mon Jan 03 14:07:08 2000 +0100
    10.3 @@ -5,8 +5,8 @@
    10.4  *)
    10.5  
    10.6  Goalw [m_head_def]
    10.7 -"\\<lbrakk> m_head G T sig = Some (md,rT); wf_prog wtm G; G\\<turnstile>Class T''\\<preceq>RefT T\\<rbrakk> \\<Longrightarrow> \
    10.8 -\\\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and>  G\\<turnstile>rT'\\<preceq>rT";
    10.9 +"\\<lbrakk> m_head G T sig = Some (md,rT); wf_prog wf_mb G; G\\<turnstile>Class T''\\<preceq>RefT T\\<rbrakk> \\<Longrightarrow> \
   10.10 +\\\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
   10.11  by( forward_tac [widen_Class_RefT] 1);
   10.12  by( etac exE 1);
   10.13  by( hyp_subst_tac 1);
   10.14 @@ -15,18 +15,15 @@
   10.15  by( strip_tac1 1);
   10.16  by( split_all_tac 1);
   10.17  by( dtac widen_Class_Class 1);
   10.18 -by( etac disjE 1);
   10.19 -by(  hyp_subst_tac 1);
   10.20 -by(  asm_full_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
   10.21  by( dtac subcls_widen_methd 1);
   10.22  by   Auto_tac;
   10.23  qed "widen_methd";
   10.24  
   10.25  
   10.26  Goal
   10.27 -"\\<lbrakk>m_head G T sig = Some (md,rT); G\\<turnstile>Class T''\\<preceq>RefT T; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
   10.28 +"\\<lbrakk>m_head G T sig = Some (md,rT); G\\<turnstile>Class T''\\<preceq>RefT T; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
   10.29  \ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
   10.30 -\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>Class T''\\<preceq>Class T' \\<and> wf_mhead G sig rT' \\<and> wtm G T' (sig,rT',b)";
   10.31 +\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>Class T''\\<preceq>Class T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
   10.32  by( dtac widen_methd 1);
   10.33  by(   atac 1);
   10.34  by(  atac 1);
   10.35 @@ -35,11 +32,11 @@
   10.36  by(  atac 1);
   10.37  by( rewtac wf_mdecl_def);
   10.38  by Auto_tac;
   10.39 -val Call_lemma = result();
   10.40 +qed "Call_lemma";
   10.41  
   10.42  
   10.43  val m_head_Object = prove_goalw thy [m_head_def]
   10.44 -"\\<And>x. wf_prog wtm G \\<Longrightarrow> m_head G (ClassT Object) sig = None" (K [Asm_simp_tac 1]);
   10.45 +"\\<And>x. wf_prog wf_mb G \\<Longrightarrow> m_head G (ClassT Object) sig = None" (K [Asm_simp_tac 1]);
   10.46  
   10.47  Addsimps [m_head_Object];
   10.48  
    11.1 --- a/src/HOL/MicroJava/J/WellType.thy	Thu Dec 23 19:59:50 1999 +0100
    11.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Mon Jan 03 14:07:08 2000 +0100
    11.3 @@ -69,20 +69,20 @@
    11.4  	"typeof dt (Addr a) = dt a"
    11.5  
    11.6  types
    11.7 -	javam = "vname list \\<times> (vname \\<times> ty) list \\<times> stmt \\<times> expr"
    11.8 +	java_mb = "vname list \\<times> (vname \\<times> ty) list \\<times> stmt \\<times> expr"
    11.9  	(* method body with parameter names, local variables, block, result expression *)
   11.10  
   11.11  consts
   11.12  
   11.13 -  ty_expr :: "javam env \\<Rightarrow> (expr      \\<times> ty     ) set"
   11.14 -  ty_exprs:: "javam env \\<Rightarrow> (expr list \\<times> ty list) set"
   11.15 -  wt_stmt :: "javam env \\<Rightarrow>  stmt                 set"
   11.16 +  ty_expr :: "java_mb env \\<Rightarrow> (expr      \\<times> ty     ) set"
   11.17 +  ty_exprs:: "java_mb env \\<Rightarrow> (expr list \\<times> ty list) set"
   11.18 +  wt_stmt :: "java_mb env \\<Rightarrow>  stmt                 set"
   11.19  
   11.20  syntax
   11.21  
   11.22 -ty_expr :: "javam env \\<Rightarrow> [expr     , ty     ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Colon>_"  [51,51,51]50)
   11.23 -ty_exprs:: "javam env \\<Rightarrow> [expr list, ty list] \\<Rightarrow> bool" ("_\\<turnstile>_[\\<Colon>]_"[51,51,51]50)
   11.24 -wt_stmt :: "javam env \\<Rightarrow>  stmt                \\<Rightarrow> bool" ("_\\<turnstile>_ \\<surd>" [51,51   ]50)
   11.25 +ty_expr :: "java_mb env \\<Rightarrow> [expr     , ty     ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Colon>_"  [51,51,51]50)
   11.26 +ty_exprs:: "java_mb env \\<Rightarrow> [expr list, ty list] \\<Rightarrow> bool" ("_\\<turnstile>_[\\<Colon>]_"[51,51,51]50)
   11.27 +wt_stmt :: "java_mb env \\<Rightarrow>  stmt                \\<Rightarrow> bool" ("_\\<turnstile>_ \\<surd>" [51,51   ]50)
   11.28  
   11.29  translations
   11.30  	"E\\<turnstile>e \\<Colon> T" == "(e,T) \\<in> ty_expr  E"
   11.31 @@ -168,8 +168,8 @@
   11.32  
   11.33  constdefs
   11.34  
   11.35 - wt_java_mdecl :: javam prog => cname => javam mdecl => bool
   11.36 -"wt_java_mdecl G C \\<equiv> \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
   11.37 + wf_java_mdecl :: java_mb prog => cname => java_mb mdecl => bool
   11.38 +"wf_java_mdecl G C \\<equiv> \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
   11.39  	length pTs = length pns \\<and>
   11.40  	nodups pns \\<and>
   11.41  	unique lvars \\<and>
   11.42 @@ -178,7 +178,7 @@
   11.43  	(let E = (G,map_of lvars(pns[\\<mapsto>]pTs)(This\\<mapsto>Class C)) in
   11.44  	 E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res\\<Colon>T \\<and> G\\<turnstile>T\\<preceq>rT))"
   11.45  
   11.46 - wf_java_prog :: javam prog => bool
   11.47 -"wf_java_prog G \\<equiv> wf_prog wt_java_mdecl G"
   11.48 + wf_java_prog :: java_mb prog => bool
   11.49 +"wf_java_prog G \\<equiv> wf_prog wf_java_mdecl G"
   11.50  
   11.51  end