# HG changeset patch
# User nipkow
# Date 949494398 -3600
# Node ID 59b62e8804b454341baa7ff68d138db35e6ba3f8
# Parent  6b7ef9fc39da959ebd2636f5035f275adb14591b
Rduced Class C <= Class D to C <= D.

diff -r 6b7ef9fc39da -r 59b62e8804b4 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Wed Feb 02 12:46:57 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Wed Feb 02 13:26:38 2000 +0100
@@ -120,7 +120,7 @@
 by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [obj_ty_def]) 1);
 by (exhaust_tac "v" 1);
-by (ALLGOALS (fast_tac  (claset() addIs [widen_trans] addss (simpset() addsimps [widen.null]))));
+by (ALLGOALS (fast_tac  (claset() addIs [rtrancl_trans] addss (simpset() addsimps [widen.null]))));
 qed "Cast_conf2";
 
 Goal
@@ -283,31 +283,31 @@
 by (asm_full_simp_tac (simpset()addsimps[raise_xcpt_def]@defs1 
 	addsplits [option.split]) 1);
 by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
 bd approx_stk_append_lemma 1;   
 by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
 bd conf_RefTD 1;
 by (Clarify_tac 1);
 by(rename_tac "oloc oT ofs T'" 1);
-by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
 bd subtype_widen_methd 1;
   ba 1;
  ba 1;
 be exE 1;
 by(rename_tac "oT'" 1);
 by (Clarify_tac 1);
-by(subgoal_tac "G \\<turnstile> Class oT \\<preceq> Class oT'" 1);
+by(subgoal_tac "G \\<turnstile> oT \\<preceq>C oT'" 1);
  by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 method_wf_mdecl)) 2);
   ba 2;
  by(Blast_tac 2);
-by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
 by(forward_tac [method_in_md] 1);
  ba 1;
  back();
  back();
 by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
 by (forward_tac [wt_jvm_prog_impl_wt_start] 1);
  ba 1;
  back();
diff -r 6b7ef9fc39da -r 59b62e8804b4 src/HOL/MicroJava/J/Conform.ML
--- a/src/HOL/MicroJava/J/Conform.ML	Wed Feb 02 12:46:57 2000 +0100
+++ b/src/HOL/MicroJava/J/Conform.ML	Wed Feb 02 13:26:38 2000 +0100
@@ -55,7 +55,7 @@
 (K [Asm_full_simp_tac 1]);
 
 val conf_obj_AddrI = prove_goalw thy [conf_def]
- "\\<And>G. \\<lbrakk>h a = Some (C,fs); G\\<turnstile>Class C\\<preceq> Class D\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq> Class D" 
+ "\\<And>G. \\<lbrakk>h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq> Class D" 
 (K [Asm_full_simp_tac 1]);
 
 Goalw [conf_def] "is_type G T \\<longrightarrow> G,h\\<turnstile>default_val T\\<Colon>\\<preceq>T";
@@ -98,17 +98,17 @@
 	safe_tac HOL_cs,
 	Asm_full_simp_tac 1]);
 
-val conf_RefTD = prove_goalw thy [conf_def] "G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT T \\<longrightarrow> a' = Null |  \
-\ (\\<exists>a obj T'. a' = Addr a \\<and>  h a = Some obj \\<and>  obj_ty obj = T' \\<and>  G\\<turnstile>T'\\<preceq>RefT T)" (K [
-	induct_tac "a'" 1,
-	    Auto_tac,
-	    REPEAT (etac widen_PrimT_RefT 1)]) RS mp;
+Goalw [conf_def]
+ "G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT T \\<longrightarrow> a' = Null |  \
+\ (\\<exists>a obj T'. a' = Addr a \\<and>  h a = Some obj \\<and>  obj_ty obj = T' \\<and>  G\\<turnstile>T'\\<preceq>RefT T)";
+by(induct_tac "a'" 1);
+by(Auto_tac);
+qed_spec_mp "conf_RefTD";
 
 val conf_NullTD = prove_goal thy "\\<And>G. G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT NullT \\<Longrightarrow> a' = Null" (K [
 	dtac conf_RefTD 1,
 	Step_tac 1,
-	 Auto_tac,
-	 etac widen_Class_NullT 1]);
+	 Auto_tac]);
 
 val non_npD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t\\<rbrakk> \\<Longrightarrow> \
 \ \\<exists>a C fs. a' = Addr a \\<and>  h a = Some (C,fs) \\<and>  G\\<turnstile>Class C\\<preceq>RefT t" (K [
@@ -117,21 +117,22 @@
 	 Auto_tac]);
 
 val non_np_objD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq> Class C; C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \
-\ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>Class C'\\<preceq> Class C)" 
-	(K[fast_tac (HOL_cs addDs [non_npD]) 1]);
+\ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>C'\\<preceq>C C)" 
+	(K[fast_tac (claset() addDs [non_npD]) 1]);
 
 Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wf_mb G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
 \ (\\<forall>C. t = ClassT C \\<longrightarrow> C \\<noteq> Object) \\<longrightarrow> \
 \ (\\<exists>a C fs. a' = Addr a \\<and>  h a = Some (C,fs) \\<and>  G\\<turnstile>Class C\\<preceq>RefT t)";
-by (rtac impI 1);
-by (rtac impI 1);
-by (res_inst_tac [("y","t")] ref_ty.exhaust 1);
-by    (safe_tac HOL_cs);
-by   (dtac conf_NullTD 1);
-by   (contr_tac 1);
-by  (etac non_np_objD 1);
-by   (atac 1);
-by  (Fast_tac 1);
+by(rtac impI 1);
+by(rtac impI 1);
+by(res_inst_tac [("y","t")] ref_ty.exhaust 1);
+ by(Safe_tac);
+ by(dtac conf_NullTD 1);
+ by(contr_tac 1);
+by(dtac non_np_objD 1);
+  by(atac 1);
+ by(Fast_tac 1);
+by(Fast_tac 1);
 qed_spec_mp "non_np_objD'";
 
 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'";
diff -r 6b7ef9fc39da -r 59b62e8804b4 src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Feb 02 12:46:57 2000 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Feb 02 13:26:38 2000 +0100
@@ -204,7 +204,7 @@
 
 (* Level 7 *)
 
-(* 14 NewC *)
+(* 13 NewC *)
 by( dtac new_AddrD 1);
 by( etac disjE 1);
 by(  Asm_simp_tac 2);
@@ -213,20 +213,19 @@
 by( rtac conjI 1);
 by(  fast_tac (HOL_cs addSEs [NewC_conforms]) 1);
 by( rtac conf_obj_AddrI 1);
-by(  rtac widen.refl 2);
-by(  Asm_simp_tac 2);
+by(  rtac rtrancl_refl 2);
 by( Simp_tac 1);
 
 (* for Cast *)
 by( defer_tac 1);
 
-(* 13 Lit *)
+(* 12 Lit *)
 by( etac conf_litval 1);
 
-(* 12 LAcc *)
+(* 11 LAcc *)
 by( fast_tac (claset() addEs [conforms_localD RS lconfD]) 1);
 
-(* 11 Nil *)
+(* 10 Nil *)
 by( Simp_tac 5);
 
 (* for FAss *)
@@ -285,8 +284,7 @@
 (* Level 45 *)
 
 (* 1 Call *)
-by( case_tac1 "x = None" 1);
-by(  dtac (not_None_eq RS iffD1) 2);
+by( exhaust_tac "x" 1);
 by(  Clarsimp_tac 2);
 by(  dtac exec_xcpt 2);
 by(  Asm_full_simp_tac 2);
diff -r 6b7ef9fc39da -r 59b62e8804b4 src/HOL/MicroJava/J/TypeRel.ML
--- a/src/HOL/MicroJava/J/TypeRel.ML	Wed Feb 02 12:46:57 2000 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.ML	Wed Feb 02 13:26:38 2000 +0100
@@ -74,9 +74,12 @@
 
 val prove_widen_lemma = prove_typerel_lemma [] widen.elim;
 
-val widen_PrimT_RefT = prove_typerel "G\\<turnstile>PrimT x\\<preceq>RefT tname \\<Longrightarrow> R"
- [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = RefT tname \\<longrightarrow> R"];
-
+Goal "(G\\<turnstile>PrimT pT\\<preceq>RefT rT) = False";
+br iffI 1;
+be widen.elim 1;
+by(Auto_tac);
+qed "widen_PrimT_RefT";
+AddIffs [widen_PrimT_RefT];
 
 val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T \\<Longrightarrow> \\<exists>t. T=RefT t" 
 	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
@@ -87,16 +90,20 @@
 val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T \\<Longrightarrow> \\<exists>D. T=Class D"
  [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> (\\<exists>D. T=Class D)"];
 
-val widen_Class_RefT = prove_typerel 
-	"G\\<turnstile>Class C\\<preceq>RefT t \\<Longrightarrow> (\\<exists>tname. t=ClassT tname)" 
- [prove_widen_lemma 
- "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT t \\<longrightarrow> (\\<exists>tname. t=ClassT tname)"];
+Goal "(G\\<turnstile>Class C\\<preceq>RefT NullT) = False"; 
+br iffI 1;
+be widen.elim 1;
+by(Auto_tac);
+qed "widen_Class_NullT";
+AddIffs [widen_Class_NullT];
 
-val widen_Class_NullT = prove_typerel "G\\<turnstile>Class C\\<preceq>RefT NullT \\<Longrightarrow> R" 
- [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT NullT \\<longrightarrow> R"];
-
-val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq> Class cm \\<Longrightarrow> G\\<turnstile>C\\<preceq>C cm"
-[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> G\\<turnstile>C\\<preceq>C cm"];
+Goal "(G\\<turnstile>Class C\\<preceq> Class D) = (G\\<turnstile>C\\<preceq>C D)";
+br iffI 1;
+be widen.elim 1;
+by(Auto_tac);
+bes widen.intrs 1;
+qed "widen_Class_Class";
+AddIffs [widen_Class_Class];
 
 Goal "G\\<turnstile>S\\<preceq>U \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
 by( etac widen.induct 1);
@@ -104,8 +111,6 @@
 by(  ALLGOALS (forward_tac [widen_Class, widen_RefT]));
 by  Safe_tac;
 by(  rtac widen.null 2);
-by(dtac widen_Class_Class 1);
-by(rtac widen.subcls 1);
 by(eatac rtrancl_trans 1 1);
 qed_spec_mp "widen_trans";
 
diff -r 6b7ef9fc39da -r 59b62e8804b4 src/HOL/MicroJava/J/WellForm.ML
--- a/src/HOL/MicroJava/J/WellForm.ML	Wed Feb 02 12:46:57 2000 +0100
+++ b/src/HOL/MicroJava/J/WellForm.ML	Wed Feb 02 13:26:38 2000 +0100
@@ -152,11 +152,6 @@
 	"\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"
 	(K [split_all_tac 1, Auto_tac]);
 
-Goal "\\<lbrakk>wf_prog wf_mb G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq> Class Object";
-by(rtac widen.subcls 1);	
-by(eatac subcls_C_Object 1 1);
-qed "widen_Class_Object";
-
 Goal "\\<lbrakk>(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
 \ x \\<in> set (fields (G,C)) \\<longrightarrow> x \\<in> set (fields (G,C'))";
 by(etac trancl_trans_induct 1);
@@ -166,7 +161,7 @@
 qed_spec_mp "fields_mono";
 
 Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
-\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>Class C\\<preceq> Class fd";
+\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>C\\<preceq>C fd";
 by( etac subcls1_induct 1);
 by(   atac 1);
 by(  Asm_simp_tac 1);
@@ -181,15 +176,14 @@
 by( etac UnE 1);
 by(  dtac split_Pair_eq 1);
 by(  SELECT_GOAL (Auto_tac) 1);
-by( rtac widen_trans 1);
-by(  etac (r_into_rtrancl RS widen.subcls) 1);
+by( etac (r_into_rtrancl RS rtrancl_trans) 1);
 by( etac BallE 1);
 by(  contr_tac 1);
 by( Asm_full_simp_tac 1);
 qed "widen_fields_defpl'";
 
 Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
-\ G\\<turnstile>Class C\\<preceq> Class fd";
+\ G\\<turnstile>C\\<preceq>C fd";
 by( datac widen_fields_defpl' 1 1);
 (*###################*)
 by( dtac bspec 1);
@@ -217,7 +211,7 @@
 by (EVERY1[dtac widen_fields_defpl, atac, atac]);
 by( Asm_full_simp_tac 1);
 by( dtac split_Pair_eq 1);
-by( fast_tac (HOL_cs addSDs [widen_Class_Class]) 1);
+by( Asm_full_simp_tac 1);
 qed "unique_fields";
 
 (*####TO Trancl.ML*)
@@ -227,9 +221,8 @@
 qed "rtranclD";
 
 Goal
-"\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>Class C'\\<preceq> Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
+"\\<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";
-by( dtac widen_Class_Class 1);
 by( dtac rtranclD 1);
 by( Auto_tac);
 by( rtac table_mono 1);
@@ -246,11 +239,11 @@
 (K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
 
 val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\
-\  G\\<turnstile>Class C'\\<preceq> Class C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
+\  G\\<turnstile>C'\\<preceq>C C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
 fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
 
 Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
-\  \\<longrightarrow> G\\<turnstile>Class C\\<preceq> Class md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
+\  \\<longrightarrow> G\\<turnstile>C\\<preceq>C md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
 by( case_tac "is_class G C" 1);
 by(  forw_inst_tac [("C","C")] method_rec 2);
 by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
@@ -266,9 +259,8 @@
 by( etac disjE 1);
 by(  thin_tac "?P \\<longrightarrow> ?Q" 1);
 by(  Clarify_tac 2);
-by(  rtac widen_trans 2);
+by(  rtac rtrancl_trans 2);
 by(   atac 3);
-by(  rtac widen.subcls 2);
 by(  rtac r_into_rtrancl 2);
 by(  fast_tac (HOL_cs addIs [subcls1I]) 2);
 by( forward_tac [table_mapf_SomeD] 1);
@@ -313,11 +305,10 @@
 
 
 Goal
- "\\<lbrakk> G\\<turnstile>Class C\\<preceq> Class D; wf_prog wf_mb G; \
+ "\\<lbrakk> G\\<turnstile> C\\<preceq>C D; wf_prog wf_mb G; \
 \    method (G,D) sig = Some (md, rT, b) \\<rbrakk> \
 \ \\<Longrightarrow> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
-by(auto_tac (claset() addSDs [widen_Class_Class]
-                      addDs [subcls_widen_methd,method_wf_mdecl],
+by(auto_tac (claset() addDs [subcls_widen_methd,method_wf_mdecl],
              simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
 qed "subtype_widen_methd";
 
diff -r 6b7ef9fc39da -r 59b62e8804b4 src/HOL/MicroJava/J/WellType.ML
--- a/src/HOL/MicroJava/J/WellType.ML	Wed Feb 02 12:46:57 2000 +0100
+++ b/src/HOL/MicroJava/J/WellType.ML	Wed Feb 02 13:26:38 2000 +0100
@@ -5,22 +5,17 @@
 *)
 
 Goal
-"\\<lbrakk> method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>Class T''\\<preceq> Class C\\<rbrakk>\
+"\\<lbrakk> method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>T''\\<preceq>C C\\<rbrakk>\
 \ \\<Longrightarrow> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
-by( forward_tac [widen_Class_RefT] 1);
-by( etac exE 1);
-by( asm_full_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
-by( strip_tac1 1);
-by( dtac widen_Class_Class 1);
 by( dtac subcls_widen_methd 1);
 by   Auto_tac;
 qed "widen_methd";
 
 
 Goal
-"\\<lbrakk>method (G,C) sig = Some (md,rT,b); G\\<turnstile>Class T''\\<preceq> Class C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
+"\\<lbrakk>method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
 \ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
-\ 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)";
+\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>T''\\<preceq>C T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
 by( datac widen_methd 2 1);
 by( Clarsimp_tac 1);
 by( dtac method_wf_mdecl 1);