--- 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);
--- 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];
--- 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 *)