# HG changeset patch
# User oheimb
# Date 947001943 -3600
# Node ID dce06445aafdf3edbc2e2e1c62330c9845c21eb3
# Parent  c3790c6b4470a99712b9cbe611fd7655eb481d31
new arg type for max_spec etc.

diff -r c3790c6b4470 -r dce06445aafd src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Mon Jan 03 17:33:34 2000 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Tue Jan 04 17:05:43 2000 +0100
@@ -123,7 +123,7 @@
 
 Goalw [wf_java_prog_def]
  "\\<lbrakk> wf_java_prog G; a' \\<noteq> Null; (h, l)\\<Colon>\\<preceq>(G, lT); \
-\    max_spec G T (mn,pTsa) = {((mda,rTa),pTs')}; xc\\<le>|xh; xh\\<le>|h; \
+\    max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\\<le>|xh; xh\\<le>|h; \
 \    list_all2 (conf G h) pvs pTsa;\
 \    (md, rT, pns, lvars, blk, res) = \
 \              the (method (G,fst (the (h (the_Addr a')))) (mn, pTs'));\
@@ -131,7 +131,7 @@
 \ (G, lT)\\<turnstile>blk\\<surd> \\<longrightarrow>  h\\<le>|xi \\<and>  (xi, xl)\\<Colon>\\<preceq>(G, lT); \
 \ \\<forall>lT. (xi, xl)\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> (\\<forall>T. (G, lT)\\<turnstile>res\\<Colon>T \\<longrightarrow> \
 \         xi\\<le>|h' \\<and> (h', xj)\\<Colon>\\<preceq>(G, lT) \\<and> (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>T)); \
-\ G,xh\\<turnstile>a'\\<Colon>\\<preceq>RefT T \\<rbrakk> \\<Longrightarrow> \
+\ G,xh\\<turnstile>a'\\<Colon>\\<preceq>Class C \\<rbrakk> \\<Longrightarrow> \
 \ xc\\<le>|h' \\<and> (h', l)\\<Colon>\\<preceq>(G, lT) \\<and>  (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>rTa)";
 by( dtac (insertI1 RSN (2,(equalityD2 RS subsetD))) 1);
 by( dtac (max_spec2appl_meths RS appl_methsD) 1);
@@ -325,7 +325,7 @@
 qed "exec_type_sound";
 
 Goal "\\<lbrakk>G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>a'\\<rightarrow> Norm s'; a' \\<noteq> Null;\
-\         s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>RefT T; m_head G T sig \\<noteq> None\\<rbrakk> \\<Longrightarrow> \
+\         s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>Class C; m_head G C sig \\<noteq> None\\<rbrakk> \\<Longrightarrow> \
 \ method (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
 by( dtac eval_type_sound 1);
 by(     atac 1);
diff -r c3790c6b4470 -r dce06445aafd src/HOL/MicroJava/J/WellType.ML
--- a/src/HOL/MicroJava/J/WellType.ML	Mon Jan 03 17:33:34 2000 +0100
+++ b/src/HOL/MicroJava/J/WellType.ML	Tue Jan 04 17:05:43 2000 +0100
@@ -5,13 +5,11 @@
 *)
 
 Goalw [m_head_def]
-"\\<lbrakk> m_head G T sig = Some (md,rT); wf_prog wf_mb G; G\\<turnstile>Class T''\\<preceq>RefT T\\<rbrakk> \\<Longrightarrow> \
+"\\<lbrakk> m_head G C sig = Some (md,rT); wf_prog wf_mb G; G\\<turnstile>Class T''\\<preceq>Class 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( hyp_subst_tac 1);
 by( asm_full_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
-by( rewtac option_map_def);
 by( strip_tac1 1);
 by( split_all_tac 1);
 by( dtac widen_Class_Class 1);
@@ -21,12 +19,10 @@
 
 
 Goal
-"\\<lbrakk>m_head G T sig = Some (md,rT); G\\<turnstile>Class T''\\<preceq>RefT T; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
+"\\<lbrakk>m_head G C sig = Some (md,rT); G\\<turnstile>Class T''\\<preceq>Class 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)";
-by( dtac widen_methd 1);
-by(   atac 1);
-by(  atac 1);
+by( datac widen_methd 2 1);
 by( Clarsimp_tac 1);
 by( dtac method_wf_mdecl 1);
 by(  atac 1);
@@ -36,17 +32,17 @@
 
 
 val m_head_Object = prove_goalw thy [m_head_def]
-"\\<And>x. wf_prog wf_mb G \\<Longrightarrow> m_head G (ClassT Object) sig = None" (K [Asm_simp_tac 1]);
+"\\<And>x. wf_prog wf_mb G \\<Longrightarrow> m_head G Object sig = None" (K [Asm_simp_tac 1]);
 
 Addsimps [m_head_Object];
 
 val max_spec2appl_meths = prove_goalw thy [max_spec_def] 
-	"x \\<in> max_spec G rT sig \\<longrightarrow> x \\<in> appl_methds G rT sig" 
+	"x \\<in> max_spec G C sig \\<longrightarrow> x \\<in> appl_methds G C sig" 
 	(fn _ => [Fast_tac 1]) RS mp;
 
 val appl_methsD = prove_goalw thy [appl_methds_def] 
-"(mh,pTs')\\<in>appl_methds G rT (mn, pTs) \\<longrightarrow> \
-\      m_head G rT (mn, pTs') = Some mh \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
+"(mh,pTs')\\<in>appl_methds G C (mn, pTs) \\<longrightarrow> \
+\      m_head G C (mn, pTs') = Some mh \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
 	(K [Fast_tac 1]) RS mp;
 
 val is_type_typeof = prove_goal thy 
diff -r c3790c6b4470 -r dce06445aafd src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Mon Jan 03 17:33:34 2000 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Tue Jan 04 17:05:43 2000 +0100
@@ -36,26 +36,26 @@
 
   more_spec	:: "'c prog \\<Rightarrow> (ty \\<times> 'x) \\<times> ty list \\<Rightarrow>
 		               (ty \\<times> 'x) \\<times> ty list \\<Rightarrow> bool"
-  m_head	:: "'c prog \\<Rightarrow>  ref_ty \\<Rightarrow> sig \\<Rightarrow>  (ty \\<times> ty) option"
-  appl_methds	:: "'c prog \\<Rightarrow>  ref_ty \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
-  max_spec	:: "'c prog \\<Rightarrow>  ref_ty \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
+  m_head	:: "'c prog \\<Rightarrow>  cname \\<Rightarrow> sig \\<Rightarrow>  (ty \\<times> ty) option"
+  appl_methds	:: "'c prog \\<Rightarrow>  cname \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
+  max_spec	:: "'c prog \\<Rightarrow>  cname \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
 
 defs
 
-  m_head_def  "m_head G t sig \\<equiv> case t of NullT \\<Rightarrow> None | ClassT C \\<Rightarrow>
+  m_head_def  "m_head G C sig \\<equiv> 
 		 option_map (\\<lambda>(md,(rT,mb)). (Class md,rT)) (method (G,C) sig)"
                                                                
   more_spec_def	  "more_spec G \\<equiv> \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
 		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
   
   (* applicable methods, cf. 15.11.2.1 *)
-  appl_methds_def "appl_methds G T \\<equiv> \\<lambda>(mn, pTs). {(mh,pTs') |mh pTs'.
-		                  m_head G T (mn, pTs') = Some mh \\<and>
+  appl_methds_def "appl_methds G C \\<equiv> \\<lambda>(mn, pTs). {(mh,pTs') |mh pTs'.
+		                  m_head G C (mn, pTs') = Some mh \\<and>
 		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'}"
 
   (* maximally specific methods, cf. 15.11.2.2 *)
-   max_spec_def	  "max_spec G rT sig \\<equiv> {m. m \\<in>appl_methds G rT sig \\<and> 
-				          (\\<forall>m'\\<in>appl_methds G rT sig.
+   max_spec_def	  "max_spec G C sig \\<equiv> {m. m \\<in>appl_methds G C sig \\<and> 
+				          (\\<forall>m'\\<in>appl_methds G C sig.
 				                   more_spec G m' m \\<longrightarrow> m' = m)}"
 consts
 
@@ -129,9 +129,9 @@
 
 
   (* cf. 15.11.1, 15.11.2, 15.11.3 *)
-  Call	"\\<lbrakk>E\\<turnstile>a\\<Colon>RefT t;
+  Call	"\\<lbrakk>E\\<turnstile>a\\<Colon>Class C;
 	  E\\<turnstile>ps[\\<Colon>]pTs;
-	  max_spec (prg E) t (mn, pTs) = {((md,rT),pTs')}\\<rbrakk> \\<Longrightarrow>
+	  max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}\\<rbrakk> \\<Longrightarrow>
 						 E\\<turnstile>a..mn({pTs'}ps)\\<Colon>rT"
 
 (* well-typed expression lists *)