# HG changeset patch
# User oheimb
# Date 947085185 -3600
# Node ID 2dda3e88d23f88c1b5f3df1ae2cff7a4d4901f24
# Parent  d9b3a224c0e6b1edc87ce938ca0b7c6a316000c0
simplified definition of appl_methds, removing m_head

diff -r d9b3a224c0e6 -r 2dda3e88d23f src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Jan 05 12:02:24 2000 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Jan 05 16:13:05 2000 +0100
@@ -135,10 +135,8 @@
 \ 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);
-by( etac conjE 1);
-by( dtac non_np_objD' 1);
-by(    atac 1);
-by(   atac 1);
+by( Clarify_tac 1);
+by( datac non_np_objD' 2 1);
 by(  strip_tac1 1);
 by(  Asm_full_simp_tac 1);
 by( Clarsimp_tac 1);
@@ -325,13 +323,9 @@
 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>Class C; m_head G C sig \\<noteq> None\\<rbrakk> \\<Longrightarrow> \
+\         s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>Class C; method (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);
-by(    atac 1);
-by(   atac 1);
-by(  atac 1);
+by( datac eval_type_sound 4 1);
 by( not_None_tac 1);
 by( split_all_tac 1);
 by(rewtac wf_java_prog_def);
diff -r d9b3a224c0e6 -r 2dda3e88d23f src/HOL/MicroJava/J/WellType.ML
--- a/src/HOL/MicroJava/J/WellType.ML	Wed Jan 05 12:02:24 2000 +0100
+++ b/src/HOL/MicroJava/J/WellType.ML	Wed Jan 05 16:13:05 2000 +0100
@@ -4,14 +4,13 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-Goalw [m_head_def]
-"\\<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";
+Goal
+"\\<lbrakk> method (G,C) sig = Some (md,rT,b); 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( asm_full_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
 by( strip_tac1 1);
-by( split_all_tac 1);
 by( dtac widen_Class_Class 1);
 by( dtac subcls_widen_methd 1);
 by   Auto_tac;
@@ -19,7 +18,7 @@
 
 
 Goal
-"\\<lbrakk>m_head G C sig = Some (md,rT); 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>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( datac widen_methd 2 1);
@@ -31,24 +30,26 @@
 qed "Call_lemma";
 
 
-val m_head_Object = prove_goalw thy [m_head_def]
-"\\<And>x. wf_prog wf_mb G \\<Longrightarrow> m_head G Object sig = None" (K [Asm_simp_tac 1]);
-
-Addsimps [m_head_Object];
+Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,Object) sig = None";
+by (Asm_simp_tac 1);
+qed "method_Object";
+Addsimps [method_Object];
 
-val max_spec2appl_meths = prove_goalw thy [max_spec_def] 
-	"x \\<in> max_spec G C sig \\<longrightarrow> x \\<in> appl_methds G C sig" 
-	(fn _ => [Fast_tac 1]) RS mp;
+Goalw [max_spec_def] 
+  "x \\<in> max_spec G C sig \\<Longrightarrow> x \\<in> appl_methds G C sig";
+by (Fast_tac 1);
+qed"max_spec2appl_meths";
 
-val appl_methsD = prove_goalw thy [appl_methds_def] 
-"(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;
+Goalw [appl_methds_def] 
+"((md,rT),pTs')\\<in>appl_methds G C (mn, pTs) \\<Longrightarrow> \
+\ \\<exists>D b. md = Class D \\<and> method (G,C) (mn, pTs') = Some (D,rT,b) \
+\ \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'";
+by (Fast_tac 1);
+qed "appl_methsD";
 
 val is_type_typeof = prove_goal thy 
 	"(\\<forall>a. v \\<noteq> Addr a) \\<longrightarrow> (\\<exists>T. typeof t v = Some T \\<and>  is_type G T)" (K [
 	rtac val_.induct 1,
 	    Fast_tac 5,
 	   ALLGOALS Simp_tac]) RS mp;
-
 Addsimps [is_type_typeof];
diff -r d9b3a224c0e6 -r 2dda3e88d23f src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Wed Jan 05 12:02:24 2000 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Wed Jan 05 16:13:05 2000 +0100
@@ -36,21 +36,18 @@
 
   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>  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 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 C \\<equiv> \\<lambda>(mn, pTs). {(mh,pTs') |mh pTs'.
-		                  m_head G C (mn, pTs') = Some mh \\<and>
+  appl_methds_def "appl_methds G C \\<equiv> \\<lambda>(mn, pTs).
+		                 {((Class md,rT),pTs') |md rT mb pTs'.
+		                  method (G,C)  (mn, pTs') = Some (md,rT,mb) \\<and>
 		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'}"
 
   (* maximally specific methods, cf. 15.11.2.2 *)