new arg type for max_spec etc.
--- 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);
--- 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
--- 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 *)