Introduced distinction wf_prog vs. ws_prog
--- a/src/HOL/MicroJava/BV/Altern.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/BV/Altern.thy Mon May 26 18:36:15 2003 +0200
@@ -1,3 +1,13 @@
+(* Title: HOL/MicroJava/BV/Altern.thy
+ ID: $Id$
+ Author: Martin Strecker
+ Copyright GPL 2003
+*)
+
+
+(* Alternative definition of well-typing of bytecode,
+ used in compiler type correctness proof *)
+
theory Altern = BVSpec:
--- a/src/HOL/MicroJava/BV/BVExample.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Mon May 26 18:36:15 2003 +0200
@@ -186,6 +186,7 @@
text {*
The program is structurally wellformed:
*}
+
lemma wf_struct:
"wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
proof -
@@ -223,7 +224,8 @@
apply (auto simp add: name_defs distinct_classes distinct_fields)
done
ultimately
- show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def)
+ show ?thesis
+ by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def)
qed
section "Welltypings"
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Mon May 26 18:36:15 2003 +0200
@@ -299,9 +299,10 @@
have "\<exists>D vs. hp (the_Addr v) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C"
by (auto dest!: non_np_objD)
}
- ultimately show ?thesis using Getfield field class stk hconf
+ ultimately show ?thesis using Getfield field class stk hconf wf
apply clarsimp
- apply (fastsimp dest!: hconfD widen_cfs_fields [OF _ _ wf] oconf_objD)
+ apply (fastsimp intro: wf_prog_ws_prog
+ dest!: hconfD widen_cfs_fields oconf_objD)
done
next
case (Putfield F C)
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Mon May 26 18:36:15 2003 +0200
@@ -677,6 +677,7 @@
apply (rule conjI)
apply (drule widen_cfs_fields)
apply assumption+
+ apply (erule wf_prog_ws_prog)
apply (erule conf_widen)
prefer 2
apply assumption
@@ -772,7 +773,8 @@
moreover
from wf hp heap_ok is_class_X
have hp': "G \<turnstile>h ?hp' \<surd>"
- by - (rule hconf_newref, auto simp add: oconf_def dest: fields_is_type)
+ by - (rule hconf_newref,
+ auto simp add: oconf_def dest: fields_is_type)
moreover
from hp
have sup: "hp \<le>| ?hp'" by (rule hext_new)
@@ -915,7 +917,7 @@
obtain mD'':
"method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')"
"is_class G D''"
- by (auto dest: method_in_md)
+ by (auto dest: wf_prog_ws_prog [THEN method_in_md])
from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def)
@@ -1319,7 +1321,9 @@
shows hconf_start: "\<Gamma> \<turnstile>h (start_heap \<Gamma>) \<surd>"
apply (unfold hconf_def start_heap_def)
apply (auto simp add: fun_upd_apply blank_def oconf_def split: split_if_asm)
- apply (simp add: fields_is_type [OF _ wf is_class_xcpt [OF wf]])+
+ apply (simp add: fields_is_type
+ [OF _ wf [THEN wf_prog_ws_prog]
+ is_class_xcpt [OF wf [THEN wf_prog_ws_prog]]])+
done
lemma
--- a/src/HOL/MicroJava/BV/JType.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/BV/JType.thy Mon May 26 18:36:15 2003 +0200
@@ -51,18 +51,18 @@
by (auto elim: widen.elims)
lemma is_tyI:
- "\<lbrakk> is_type G T; wf_prog wf_mb G \<rbrakk> \<Longrightarrow> is_ty G T"
+ "\<lbrakk> is_type G T; ws_prog G \<rbrakk> \<Longrightarrow> is_ty G T"
by (auto simp add: is_ty_def intro: subcls_C_Object
split: ty.splits ref_ty.splits)
lemma is_type_conv:
- "wf_prog wf_mb G \<Longrightarrow> is_type G T = is_ty G T"
+ "ws_prog G \<Longrightarrow> is_type G T = is_ty G T"
proof
- assume "is_type G T" "wf_prog wf_mb G"
+ assume "is_type G T" "ws_prog G"
thus "is_ty G T"
by (rule is_tyI)
next
- assume wf: "wf_prog wf_mb G" and
+ assume wf: "ws_prog G" and
ty: "is_ty G T"
show "is_type G T"
@@ -159,7 +159,7 @@
done
lemma closed_err_types:
- "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk>
+ "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk>
\<Longrightarrow> closed (err (types G)) (lift2 (sup G))"
apply (unfold closed_def plussub_def lift2_def sup_def)
apply (auto split: err.split)
@@ -171,22 +171,22 @@
lemma sup_subtype_greater:
- "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
+ "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G);
is_type G t1; is_type G t2; sup G t1 t2 = OK s \<rbrakk>
\<Longrightarrow> subtype G t1 s \<and> subtype G t2 s"
proof -
- assume wf_prog: "wf_prog wf_mb G"
+ assume ws_prog: "ws_prog G"
assume single_valued: "single_valued (subcls1 G)"
assume acyclic: "acyclic (subcls1 G)"
{ fix c1 c2
assume is_class: "is_class G c1" "is_class G c2"
- with wf_prog
+ with ws_prog
obtain
"G \<turnstile> c1 \<preceq>C Object"
"G \<turnstile> c2 \<preceq>C Object"
by (blast intro: subcls_C_Object)
- with wf_prog single_valued
+ with ws_prog single_valued
obtain u where
"is_lub ((subcls1 G)^* ) c1 c2 u"
by (blast dest: single_valued_has_lubs)
@@ -210,24 +210,24 @@
qed
lemma sup_subtype_smallest:
- "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
+ "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G);
is_type G a; is_type G b; is_type G c;
subtype G a c; subtype G b c; sup G a b = OK d \<rbrakk>
\<Longrightarrow> subtype G d c"
proof -
- assume wf_prog: "wf_prog wf_mb G"
+ assume ws_prog: "ws_prog G"
assume single_valued: "single_valued (subcls1 G)"
assume acyclic: "acyclic (subcls1 G)"
{ fix c1 c2 D
assume is_class: "is_class G c1" "is_class G c2"
assume le: "G \<turnstile> c1 \<preceq>C D" "G \<turnstile> c2 \<preceq>C D"
- from wf_prog is_class
+ from ws_prog is_class
obtain
"G \<turnstile> c1 \<preceq>C Object"
"G \<turnstile> c2 \<preceq>C Object"
by (blast intro: subcls_C_Object)
- with wf_prog single_valued
+ with ws_prog single_valued
obtain u where
lub: "is_lub ((subcls1 G)^* ) c1 c2 u"
by (blast dest: single_valued_has_lubs)
@@ -260,22 +260,22 @@
split: ty.splits ref_ty.splits)
lemma err_semilat_JType_esl_lemma:
- "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk>
+ "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk>
\<Longrightarrow> err_semilat (esl G)"
proof -
- assume wf_prog: "wf_prog wf_mb G"
+ assume ws_prog: "ws_prog G"
assume single_valued: "single_valued (subcls1 G)"
assume acyclic: "acyclic (subcls1 G)"
hence "order (subtype G)"
by (rule order_widen)
moreover
- from wf_prog single_valued acyclic
+ from ws_prog single_valued acyclic
have "closed (err (types G)) (lift2 (sup G))"
by (rule closed_err_types)
moreover
- from wf_prog single_valued acyclic
+ from ws_prog single_valued acyclic
have
"(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \<and>
(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)"
@@ -283,7 +283,7 @@
moreover
- from wf_prog single_valued acyclic
+ from ws_prog single_valued acyclic
have
"\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). \<forall>z\<in>err (types G).
x <=_(le (subtype G)) z \<and> y <=_(le (subtype G)) z \<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
@@ -297,12 +297,12 @@
qed
lemma single_valued_subcls1:
- "wf_prog wf_mb G \<Longrightarrow> single_valued (subcls1 G)"
- by (auto simp add: wf_prog_def unique_def single_valued_def
+ "ws_prog G \<Longrightarrow> single_valued (subcls1 G)"
+ by (auto simp add: ws_prog_def unique_def single_valued_def
intro: subcls1I elim!: subcls1.elims)
theorem err_semilat_JType_esl:
- "wf_prog wf_mb G \<Longrightarrow> err_semilat (esl G)"
+ "ws_prog G \<Longrightarrow> err_semilat (esl G)"
by (frule acyclic_subcls1, frule single_valued_subcls1, rule err_semilat_JType_esl_lemma)
end
--- a/src/HOL/MicroJava/BV/JVM.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/BV/JVM.thy Mon May 26 18:36:15 2003 +0200
@@ -29,7 +29,6 @@
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"
-
theorem is_bcv_kiljvm:
"\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow>
is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
@@ -37,14 +36,15 @@
apply (unfold kiljvm_def sl_triple_conv)
apply (rule is_bcv_kildall)
apply (simp (no_asm) add: sl_triple_conv [symmetric])
- apply (force intro!: semilat_JVM_slI dest: wf_acyclic simp add: symmetric sl_triple_conv)
+ apply (force intro!: semilat_JVM_slI dest: wf_acyclic
+ simp add: symmetric sl_triple_conv)
apply (simp (no_asm) add: JVM_le_unfold)
apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype
- dest: wf_subcls1 wf_acyclic)
+ dest: wf_subcls1 wf_acyclic wf_prog_ws_prog)
apply (simp add: JVM_le_unfold)
apply (erule exec_pres_type)
apply assumption
- apply (erule exec_mono, assumption)
+ apply (drule wf_prog_ws_prog, erule exec_mono, assumption)
done
lemma subset_replicate: "set (replicate n x) \<subseteq> {x}"
--- a/src/HOL/MicroJava/BV/LBVJVM.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy Mon May 26 18:36:15 2003 +0200
@@ -86,7 +86,8 @@
let ?f = "JVMType.sup G mxs mxr"
let ?A = "states G mxs mxr"
- have "semilat (JVMType.sl G mxs mxr)" by (rule semilat_JVM_slI)
+ have "semilat (JVMType.sl G mxs mxr)"
+ by (rule semilat_JVM_slI, rule wf_prog_ws_prog)
hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
moreover
have "top ?r Err" by (simp add: JVM_le_unfold)
@@ -217,7 +218,8 @@
app_eff: "wt_app_eff (sup_state_opt G) ?app ?eff phi"
by (simp (asm_lr) add: wt_method_def2)
- have "semilat (JVMType.sl G mxs ?mxr)" by (rule semilat_JVM_slI)
+ have "semilat (JVMType.sl G mxs ?mxr)"
+ by (rule semilat_JVM_slI, rule wf_prog_ws_prog)
hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
moreover
have "top ?r Err" by (simp add: JVM_le_unfold)
@@ -234,7 +236,8 @@
by (clarsimp simp add: exec_def)
(intro bounded_lift check_bounded_is_bounded)
with wf
- have "mono ?r ?step (length ins) ?A" by (rule exec_mono)
+ have "mono ?r ?step (length ins) ?A"
+ by (rule wf_prog_ws_prog [THEN exec_mono])
hence "mono ?r ?step (length ?phi) ?A" by (simp add: length)
moreover
have "pres_type ?step (length ins) ?A" by (rule exec_pres_type)
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Mon May 26 18:36:15 2003 +0200
@@ -239,11 +239,11 @@
done
lemma order_sup_state_opt:
- "wf_prog wf_mb G \<Longrightarrow> order (sup_state_opt G)"
+ "ws_prog G \<Longrightarrow> order (sup_state_opt G)"
by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
theorem exec_mono:
- "wf_prog wf_mb G \<Longrightarrow> bounded (exec G maxs rT et bs) (size bs) \<Longrightarrow>
+ "ws_prog G \<Longrightarrow> bounded (exec G maxs rT et bs) (size bs) \<Longrightarrow>
mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"
apply (unfold exec_def JVM_le_unfold JVM_states_unfold)
apply (rule mono_lift)
@@ -257,7 +257,7 @@
done
theorem semilat_JVM_slI:
- "wf_prog wf_mb G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
+ "ws_prog G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
apply (rule semilat_opt)
apply (rule err_semilat_Product_esl)
@@ -287,7 +287,7 @@
"(C,S,fs,mdecls) \<in> set G"
"((mn,pTs),rT,code) \<in> set mdecls"
hence "wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
- by (unfold wf_prog_def wf_cdecl_def) auto
+ by (rule wf_prog_wf_mdecl)
hence "\<forall>t \<in> set pTs. is_type G t"
by (unfold wf_mdecl_def wf_mhead_def) auto
moreover
@@ -319,11 +319,10 @@
apply (unfold wf_prog_def wf_cdecl_def)
apply clarsimp
apply (drule bspec, assumption)
- apply (unfold wf_mdecl_def)
+ apply (unfold wf_cdecl_mdecl_def)
apply clarsimp
apply (drule bspec, assumption)
- apply clarsimp
- apply (frule methd [OF wf], assumption+)
+ apply (frule methd [OF wf [THEN wf_prog_ws_prog]], assumption+)
apply (frule is_type_pTs [OF wf], assumption+)
apply clarify
apply (drule rule [OF wf], assumption+)
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Mon May 26 18:36:15 2003 +0200
@@ -8,7 +8,7 @@
theory CorrComp = JTypeSafe + LemmasComp:
-
+declare wf_prog_ws_prog [simp add]
(* If no exception is present after evaluation/execution,
none can have been present before *)
@@ -278,28 +278,27 @@
(**********************************************************************)
-(* ### to be moved to one of the J/* files *)
-
lemma method_preserves [rule_format (no_asm)]:
"\<lbrakk> wf_prog wf_mb G; is_class G C;
\<forall> S rT mb. \<forall> cn \<in> fst ` set G. wf_mdecl wf_mb G cn (S,rT,mb) \<longrightarrow> (P cn S (rT,mb))\<rbrakk>
\<Longrightarrow> \<forall> D.
method (G, C) S = Some (D, rT, mb) \<longrightarrow> (P D S (rT,mb))"
-apply (frule WellForm.wf_subcls1)
+apply (frule wf_prog_ws_prog [THEN wf_subcls1])
apply (rule subcls1_induct, assumption, assumption)
apply (intro strip)
apply ((drule spec)+, drule_tac x="Object" in bspec)
-apply (simp add: wf_prog_def wf_syscls_def)
+apply (simp add: wf_prog_def ws_prog_def wf_syscls_def)
apply (subgoal_tac "D=Object") apply simp
apply (drule mp)
apply (frule_tac C=Object in method_wf_mdecl)
- apply simp apply assumption apply simp apply assumption apply simp
+ apply simp
+ apply assumption apply simp apply assumption apply simp
apply (subst method_rec) apply simp
apply force
-apply assumption
+apply simp
apply (simp only: map_add_def)
apply (split option.split)
apply (rule conjI)
@@ -332,14 +331,6 @@
(**********************************************************************)
-(* required for lemma wtpd_expr_call *)
-lemma ty_exprs_length [simp]: "(E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts)"
-apply (subgoal_tac "(E\<turnstile>e::T \<longrightarrow> True) \<and> (E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts) \<and> (E\<turnstile>s\<surd> \<longrightarrow> True)")
-apply blast
-apply (rule ty_expr_ty_exprs_wt_stmt.induct)
-apply auto
-done
-
constdefs wtpd_expr :: "java_mb env \<Rightarrow> expr \<Rightarrow> bool"
"wtpd_expr E e == (\<exists> T. E\<turnstile>e :: T)"
wtpd_exprs :: "java_mb env \<Rightarrow> (expr list) \<Rightarrow> bool"
@@ -573,73 +564,43 @@
-
-
-
-
-
(**********************************************************************)
-constdefs
- state_ok :: "java_mb env \<Rightarrow> xstate \<Rightarrow> bool"
- "state_ok E xs == xs::\<preceq>E"
-
-
-lemma state_ok_eval: "\<lbrakk>state_ok E xs; wf_java_prog (prg E); wtpd_expr E e;
- (prg E)\<turnstile>xs -e\<succ>v -> xs'\<rbrakk> \<Longrightarrow> state_ok E xs'"
-apply (simp only: state_ok_def wtpd_expr_def)
+lemma state_ok_eval: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_expr E e;
+ (prg E)\<turnstile>xs -e\<succ>v -> xs'\<rbrakk> \<Longrightarrow> xs'::\<preceq>E"
+apply (simp only: wtpd_expr_def)
apply (erule exE)
-apply (case_tac xs', case_tac xs, simp only:)
-apply (rule eval_type_sound [THEN conjunct1])
-apply (rule HOL.refl)
-apply assumption
-apply (subgoal_tac "fst E \<turnstile> (gx xs, gs xs) -e\<succ>v-> (gx xs', gs xs')")
-apply assumption
-apply (auto simp: gx_def gs_def)
+apply (case_tac xs', case_tac xs)
+apply (auto intro: eval_type_sound [THEN conjunct1])
done
-(* to be moved into JTypeSafe.thy *)
-lemma evals_type_sound: "!!E s s'.
- [| G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); G=prg E; wf_java_prog G; (x,s)::\<preceq>E; E\<turnstile>es[::]Ts |]
- ==> (x',s')::\<preceq>E \<and> (x'=None --> list_all2 (conf G (heap s')) vs Ts)"
-apply( simp (no_asm_simp) only: split_tupled_all)
-apply (drule eval_evals_exec_type_sound
- [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp])
-apply auto
+lemma state_ok_evals: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_exprs E es;
+ (xs,es,vs,xs') \<in> Eval.evals (prg E)\<rbrakk> \<Longrightarrow> xs'::\<preceq>E"
+apply (simp only: wtpd_exprs_def)
+apply (erule exE)
+apply (case_tac xs) apply (case_tac xs')
+apply (auto intro: evals_type_sound [THEN conjunct1])
done
-lemma state_ok_evals: "\<lbrakk>state_ok E xs; wf_java_prog (prg E); wtpd_exprs E es;
- (xs,es,vs,xs') \<in> Eval.evals (prg E)\<rbrakk> \<Longrightarrow> state_ok E xs'"
-apply (simp only: state_ok_def wtpd_exprs_def)
-apply (erule exE)
-apply (case_tac xs) apply (case_tac xs') apply (simp only:)
-apply (rule evals_type_sound [THEN conjunct1])
-apply (auto simp: gx_def gs_def)
-done
-
-lemma state_ok_exec: "\<lbrakk>state_ok E xs; wf_java_prog (prg E); wtpd_stmt E st;
- (xs,st,xs') \<in> Eval.exec (prg E)\<rbrakk> \<Longrightarrow> state_ok E xs'"
-apply (simp only: state_ok_def wtpd_stmt_def)
-apply (case_tac xs', case_tac xs, simp only:)
-apply (rule exec_type_sound)
-apply (rule HOL.refl)
-apply assumption
-apply (subgoal_tac "((gx xs, gs xs), st, (gx xs', gs xs')) \<in> Eval.exec (fst E)")
-apply assumption
-apply (auto simp: gx_def gs_def)
+lemma state_ok_exec: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_stmt E st;
+ (xs,st,xs') \<in> Eval.exec (prg E)\<rbrakk> \<Longrightarrow> xs'::\<preceq>E"
+apply (simp only: wtpd_stmt_def)
+apply (case_tac xs', case_tac xs)
+apply (auto intro: exec_type_sound)
done
lemma state_ok_init:
- "\<lbrakk> wf_java_prog G; state_ok (env_of_jmb G C S) (x, h, l);
+ "\<lbrakk> wf_java_prog G; (x, h, l)::\<preceq>(env_of_jmb G C S);
is_class G dynT;
method (G, dynT) (mn, pTs) = Some (md, rT, pns, lvars, blk, res);
list_all2 (conf G h) pvs pTs; G,h \<turnstile> a' ::\<preceq> Class md\<rbrakk>
\<Longrightarrow>
-state_ok (env_of_jmb G md (mn, pTs)) (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))"
+(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs))"
+apply (frule wf_prog_ws_prog)
apply (frule method_in_md [THEN conjunct2], assumption+)
apply (frule method_yields_wf_java_mdecl, assumption, assumption)
-apply (simp add: state_ok_def env_of_jmb_def gs_def conforms_def split_beta)
+apply (simp add: env_of_jmb_def gs_def conforms_def split_beta)
apply (simp add: wf_java_mdecl_def)
apply (rule conjI)
apply (rule lconf_ext)
@@ -675,7 +636,7 @@
done
-lemma class_expr_is_class: "\<lbrakk>E \<turnstile> e :: Class C; wf_prog wf_mb (prg E)\<rbrakk>
+lemma class_expr_is_class: "\<lbrakk>E \<turnstile> e :: Class C; ws_prog (prg E)\<rbrakk>
\<Longrightarrow> is_class (prg E) C"
by (case_tac E, auto dest: ty_expr_is_type)
@@ -685,7 +646,7 @@
by (blast dest: singleton_in_set max_spec2appl_meths appl_methsD)
-lemma eval_conf: "\<lbrakk>G \<turnstile> s -e\<succ>v-> s'; wf_java_prog G; state_ok E s;
+lemma eval_conf: "\<lbrakk>G \<turnstile> s -e\<succ>v-> s'; wf_java_prog G; s::\<preceq>E;
E\<turnstile>e::T; gx s' = None; prg E = G \<rbrakk>
\<Longrightarrow> G,gh s'\<turnstile>v::\<preceq>T"
apply (simp add: gh_def)
@@ -694,15 +655,13 @@
apply (rule sym) apply assumption
apply assumption
apply (simp (no_asm_use) add: surjective_pairing [THEN sym])
-apply (simp only: state_ok_def gs_def)
-apply (case_tac s, simp)
-apply assumption
-apply (simp add: gx_def)
+apply (simp only: surjective_pairing [THEN sym])
+apply (auto simp add: gs_def gx_def)
done
lemma evals_preserves_conf:
"\<lbrakk> G\<turnstile> s -es[\<succ>]vs-> s'; G,gh s \<turnstile> t ::\<preceq> T; E \<turnstile>es[::]Ts;
- wf_java_prog G; state_ok E s;
+ wf_java_prog G; s::\<preceq>E;
prg E = G \<rbrakk> \<Longrightarrow> G,gh s' \<turnstile> t ::\<preceq> T"
apply (subgoal_tac "gh s\<le>| gh s'")
apply (frule conf_hext, assumption, assumption)
@@ -711,15 +670,14 @@
apply assumption
apply (simp add: gx_def gh_def gl_def surjective_pairing [THEN sym])
apply (case_tac E)
-apply (simp add: gx_def gs_def gh_def gl_def state_ok_def
- surjective_pairing [THEN sym])
+apply (simp add: gx_def gs_def gh_def gl_def surjective_pairing [THEN sym])
done
lemma eval_of_class: "\<lbrakk> G \<turnstile> s -e\<succ>a'-> s'; E \<turnstile> e :: Class C;
- wf_java_prog G; state_ok E s; gx s'=None; a' \<noteq> Null; G=prg E\<rbrakk>
+ wf_java_prog G; s::\<preceq>E; gx s'=None; a' \<noteq> Null; G=prg E\<rbrakk>
\<Longrightarrow> (\<exists> lc. a' = Addr lc)"
apply (case_tac s, case_tac s', simp)
-apply (frule eval_type_sound, (simp add: state_ok_def gs_def)+)
+apply (frule eval_type_sound, (simp add: gs_def)+)
apply (case_tac a')
apply (auto simp: conf_def)
done
@@ -727,9 +685,10 @@
lemma dynT_subcls:
"\<lbrakk> a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; dynT = fst (the (h (the_Addr a')));
- is_class G dynT; wf_prog wf_mb G \<rbrakk> \<Longrightarrow> G\<turnstile>dynT \<preceq>C C"
+ is_class G dynT; ws_prog G \<rbrakk> \<Longrightarrow> G\<turnstile>dynT \<preceq>C C"
apply (case_tac "C = Object")
apply (simp, rule subcls_C_Object, assumption+)
+apply simp
apply (frule non_np_objD, auto)
done
@@ -746,7 +705,7 @@
apply ((erule exE)+, (erule conjE)+, (erule exE)+)
apply (drule widen_methd)
apply assumption
-apply (rule dynT_subcls, assumption+, simp, assumption+)
+apply (rule dynT_subcls) apply assumption+ apply simp apply simp
apply (erule exE)+ apply simp
done
@@ -764,7 +723,7 @@
(\<forall> os CL S.
(class_sig_defined G CL S) \<longrightarrow>
(wtpd_expr (env_of_jmb G CL S) ex) \<longrightarrow>
- (state_ok (env_of_jmb G CL S) xs) \<longrightarrow>
+ (xs ::\<preceq> (env_of_jmb G CL S)) \<longrightarrow>
( {TranslComp.comp G, CL, S} \<turnstile>
{gh xs, os, (locvars_xstate G CL S xs)}
>- (compExpr (gmb G CL S) ex) \<rightarrow>
@@ -775,7 +734,7 @@
(\<forall> os CL S.
(class_sig_defined G CL S) \<longrightarrow>
(wtpd_exprs (env_of_jmb G CL S) exs) \<longrightarrow>
- (state_ok (env_of_jmb G CL S) xs) \<longrightarrow>
+ (xs::\<preceq>(env_of_jmb G CL S)) \<longrightarrow>
( {TranslComp.comp G, CL, S} \<turnstile>
{gh xs, os, (locvars_xstate G CL S xs)}
>- (compExprs (gmb G CL S) exs) \<rightarrow>
@@ -786,7 +745,7 @@
(\<forall> os CL S.
(class_sig_defined G CL S) \<longrightarrow>
(wtpd_stmt (env_of_jmb G CL S) st) \<longrightarrow>
- (state_ok (env_of_jmb G CL S) xs) \<longrightarrow>
+ (xs::\<preceq>(env_of_jmb G CL S)) \<longrightarrow>
( {TranslComp.comp G, CL, S} \<turnstile>
{gh xs, os, (locvars_xstate G CL S xs)}
>- (compStmt (gmb G CL S) st) \<rightarrow>
@@ -797,8 +756,8 @@
apply simp
(* case NewC *)
-apply clarify
-apply (frule wf_subcls1) (* establish wf ((subcls1 G)^-1) *)
+apply clarify
+apply (frule wf_prog_ws_prog [THEN wf_subcls1]) (* establish wf ((subcls1 G)^-1) *)
apply (simp add: c_hupd_hp_invariant)
apply (rule progression_one_step)
apply (rotate_tac 1, drule sym) (* reverse equation (a, None) = new_Addr (fst s) *)
@@ -828,7 +787,7 @@
apply (intro allI impI)
apply (frule_tac xs=s1 in eval_xcpt, assumption) (* establish (gx s1 = None) *)
apply (frule wtpd_expr_binop)
-(* establish (state_ok \<dots> s1) *)
+(* establish (s1::\<preceq> \<dots>) *)
apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp)) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
@@ -896,8 +855,9 @@
apply (simp only: gx_conv, simp only: gx_conv, frule np_NoneD, erule conjE)
- (* establish (state_ok \<dots> (Norm s1)) *)
-apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
+ (* establish ((Norm s1)::\<preceq> \<dots>) *)
+apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst)
+ apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
apply (simp only: compExpr_compExprs.simps)
@@ -936,7 +896,7 @@
apply (intro allI impI)
apply (frule_tac xs=s1 in evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *)
apply (frule wtpd_exprs_cons)
- (* establish (state_ok \<dots> (Norm s0)) *)
+ (* establish ((Norm s0)::\<preceq> \<dots>) *)
apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
apply simp
@@ -967,7 +927,7 @@
apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
apply (frule wtpd_stmt_comp)
- (* establish (state_ok \<dots> s1) *)
+ (* establish (s1::\<preceq> \<dots>) *)
apply (frule_tac st=c1 in state_ok_exec) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
apply simp
@@ -980,7 +940,7 @@
apply (intro allI impI)
apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
apply (frule wtpd_stmt_cond, (erule conjE)+)
-(* establish (state_ok \<dots> s1) *)
+(* establish (s1::\<preceq> \<dots>) *)
apply (frule_tac e=e in state_ok_eval)
apply (simp (no_asm_simp) only: env_of_jmb_fst)
apply assumption
@@ -1053,9 +1013,9 @@
apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
apply (frule wtpd_stmt_loop, (erule conjE)+)
-(* establish (state_ok \<dots> s1) *)
+(* establish (s1::\<preceq> \<dots>) *)
apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
-(* establish (state_ok \<dots> s2) *)
+(* establish (s2::\<preceq> \<dots>) *)
apply (frule_tac xs=s1 and st=c in state_ok_exec)
apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
@@ -1094,7 +1054,7 @@
apply blast
(*****)
-(* case method call *) defer (* !!! NEWC *)
+(* case method call *)
apply (intro allI impI)
@@ -1107,11 +1067,11 @@
(* assumptions about state_ok and is_class *)
-(* establish state_ok (env_of_jmb G CL S) s1 *)
+(* establish s1::\<preceq> (env_of_jmb G CL S) *)
apply (frule_tac xs="Norm s0" and e=e in state_ok_eval)
apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp (no_asm_use) only: env_of_jmb_fst)
-(* establish state_ok (env_of_jmb G CL S) (x, h, l) *)
+(* establish (x, h, l)::\<preceq>(env_of_jmb G CL S) *)
apply (frule_tac xs=s1 and xs'="(x, h, l)" in state_ok_evals)
apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp only: env_of_jmb_fst)
@@ -1130,7 +1090,7 @@
apply (subgoal_tac " method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res)")
apply (subgoal_tac "list_all2 (conf G h) pvs pTs")
-(* establish state_ok (env_of_jmb G md (mn, pTs)) (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a')) *)
+(* establish (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs)) *)
apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class dynT")
apply (frule (2) conf_widen)
apply (frule state_ok_init, assumption+)
@@ -1138,16 +1098,14 @@
apply (subgoal_tac "class_sig_defined G md (mn, pTs)")
apply (frule wtpd_blk, assumption, assumption)
apply (frule wtpd_res, assumption, assumption)
-apply (subgoal_tac "state_ok (env_of_jmb G md (mn, pTs)) s3")
+apply (subgoal_tac "s3::\<preceq>(env_of_jmb G md (mn, pTs))")
-(* establish method (TranslComp.comp G, md) (mn, pTs) =
- Some (md, rT, compMethod (pns, lvars, blk, res)) *)
-apply (frule_tac C=md and D=md in comp_method, assumption, assumption)
-
-(* establish
- method (TranslComp.comp G, dynT) (mn, pTs) =
- Some (md, rT, compMethod (pns, lvars, blk, res)) *)
- apply (frule_tac C=dynT and D=md in comp_method, assumption, assumption)
+apply (subgoal_tac "method (TranslComp.comp G, md) (mn, pTs) =
+ Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))")
+prefer 2 apply (simp add: wf_prog_ws_prog [THEN comp_method])
+apply (subgoal_tac "method (TranslComp.comp G, dynT) (mn, pTs) =
+ Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))")
+prefer 2 apply (simp add: wf_prog_ws_prog [THEN comp_method])
apply (simp only: fst_conv snd_conv)
(* establish length pns = length pTs *)
@@ -1209,7 +1167,7 @@
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
-(* show state_ok \<dots> s3 *)
+(* show s3::\<preceq>\<dots> *)
apply (rule_tac xs = "(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))" and st=blk in state_ok_exec)
apply assumption apply (simp (no_asm_simp) only: env_of_jmb_fst)
apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
@@ -1231,7 +1189,7 @@
apply (subgoal_tac "((gx s1, gs s1), ps, pvs, x, h, l) \<in> evals G")
apply (frule_tac E="env_of_jmb G CL S" in evals_type_sound)
apply (simp only: env_of_jmb_fst)
-apply assumption apply (simp only: state_ok_def)
+apply assumption
apply (simp add: conforms_def xconf_def gs_def)
apply simp
apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym])
@@ -1242,14 +1200,14 @@
(* show method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res) *)
-apply (frule method_in_md [THEN conjunct2], assumption+)
+apply (frule wf_prog_ws_prog [THEN method_in_md [THEN conjunct2]], assumption+)
(* show G\<turnstile>Class dynT \<preceq> Class md *)
apply (simp (no_asm_use) only: widen_Class_Class)
apply (rule method_wf_mdecl [THEN conjunct1], assumption+)
(* is_class G md *)
-apply (rule method_in_md [THEN conjunct1], assumption+)
+apply (rule wf_prog_ws_prog [THEN method_in_md [THEN conjunct1]], assumption+)
(* show is_class G dynT *)
apply (frule non_npD) apply assumption
@@ -1257,6 +1215,7 @@
apply simp
apply (rule subcls_is_class2) apply assumption
apply (frule class_expr_is_class) apply (simp only: env_of_jmb_fst)
+apply (rule wf_prog_ws_prog, assumption)
apply (simp only: env_of_jmb_fst)
(* show G,h \<turnstile> a' ::\<preceq> Class C *)
@@ -1280,7 +1239,7 @@
>- (compExpr (gmb G C S) ex) \<rightarrow>
{hp', val#os, (locvars_locals G C S loc')}"
apply (frule compiler_correctness [THEN conjunct1])
-apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def state_ok_def)
+apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def)
done
theorem compiler_correctness_exec: "
@@ -1294,7 +1253,7 @@
>- (compStmt (gmb G C S) st) \<rightarrow>
{hp', os, (locvars_locals G C S loc')}"
apply (frule compiler_correctness [THEN conjunct2 [THEN conjunct2]])
-apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def state_ok_def)
+apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def)
done
(**********************************************************************)
@@ -1306,4 +1265,6 @@
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
*}
+declare wf_prog_ws_prog [simp del]
+
end
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Mon May 26 18:36:15 2003 +0200
@@ -4,8 +4,7 @@
Copyright GPL 2002
*)
-theory CorrCompTp = LemmasComp + JVM + TypeInf + NatCanonify + Altern:
-
+theory CorrCompTp = LemmasComp + JVM + TypeInf + Altern:
declare split_paired_All [simp del]
declare split_paired_Ex [simp del]
@@ -27,7 +26,7 @@
by (simp add: local_env_def split_beta)
-lemma wt_class_expr_is_class: "\<lbrakk> wf_prog wf_mb G; E \<turnstile> expr :: Class cname;
+lemma wt_class_expr_is_class: "\<lbrakk> ws_prog G; E \<turnstile> expr :: Class cname;
E = local_env G C (mn, pTs) pns lvars\<rbrakk>
\<Longrightarrow> is_class G cname "
apply (subgoal_tac "((fst E), (snd E)) \<turnstile> expr :: Class cname")
@@ -308,7 +307,7 @@
(* show is_class G cname \<and> field (G, cname) vname = Some (cname, T) *)
apply (rule field_in_fd) apply assumption+
(* show is_class G Ca *)
- apply (rule wt_class_expr_is_class, assumption+, rule HOL.refl)
+ apply (fast intro: wt_class_expr_is_class)
(* FAss *)
apply (intro strip)
@@ -485,8 +484,8 @@
lemma states_mono: "\<lbrakk> mxs \<le> mxs' \<rbrakk>
\<Longrightarrow> states G mxs mxr \<subseteq> states G mxs' mxr"
apply (simp add: states_def JVMType.sl_def)
-apply (simp add: Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def
- JType.esl_def)
+apply (simp add: Product.esl_def stk_esl_def reg_sl_def
+ upto_esl_def Listn.sl_def Err.sl_def JType.esl_def)
apply (simp add: Err.esl_def Err.le_def Listn.le_def)
apply (simp add: Product.le_def Product.sup_def Err.sup_def)
apply (simp add: Opt.esl_def Listn.sup_def)
@@ -528,14 +527,12 @@
apply (induct i)
apply simp+
(* case Goto *)
-apply (simp only: nat_canonify)
-apply simp
+apply arith
(* case Ifcmpeq *)
apply simp
apply (erule disjE)
-apply simp
-apply (simp only: nat_canonify)
-apply simp
+apply arith
+apply arith
(* case Throw *)
apply simp
done
@@ -547,14 +544,12 @@
apply (induct i)
apply simp+
(* case Goto *)
-apply (simp only: nat_canonify)
-apply simp
+apply arith
(* case Ifcmpeq *)
apply simp
apply (erule disjE)
apply simp
-apply (simp only: nat_canonify)
-apply simp
+apply arith
(* case Throw *)
apply simp
done
@@ -1255,33 +1250,35 @@
\<Longrightarrow> bc_mt_corresp [Getfield vname cname]
(replST (Suc 0) (snd (the (field (G, cname) vname))))
(Class C # ST, LT) (comp G) rT mxr (Suc 0)"
- apply (frule wf_subcls1)
+ apply (frule wf_prog_ws_prog [THEN wf_subcls1])
apply (frule field_in_fd, assumption+)
apply (frule widen_field, assumption+)
apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
- apply (simp add: comp_field [THEN sym] comp_subcls1 [THEN sym] comp_widen [THEN sym] comp_is_class [THEN sym])
+ apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (intro strip)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp+
-apply (simp only: comp_is_type [THEN sym])
+apply (simp only: comp_is_type)
apply (rule_tac C=cname in fields_is_type)
apply (simp add: field_def)
apply (drule JBasis.table_of_remap_SomeD)+
apply assumption+
+apply (erule wf_prog_ws_prog)
+apply assumption
done
lemma bc_mt_corresp_Putfield: "\<lbrakk> wf_prog wf_mb G;
field (G, C) vname = Some (cname, Ta); G \<turnstile> T \<preceq> Ta; is_class G C \<rbrakk>
\<Longrightarrow> bc_mt_corresp [Putfield vname cname] (popST 2) (T # Class C # T # ST, LT)
(comp G) rT mxr (Suc 0)"
- apply (frule wf_subcls1)
+ apply (frule wf_prog_ws_prog [THEN wf_subcls1])
apply (frule field_in_fd, assumption+)
apply (frule widen_field, assumption+)
apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
- apply (simp add: comp_field [THEN sym] comp_subcls1 [THEN sym] comp_widen [THEN sym] comp_is_class [THEN sym])
+ apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
apply (intro strip)
@@ -1302,13 +1299,13 @@
apply (simp add: comp_is_class)
apply (rule_tac x=pTsa in exI)
apply (rule_tac x="Class cname" in exI)
- apply (simp add: max_spec_preserves_length comp_is_class [THEN sym])
+ apply (simp add: max_spec_preserves_length comp_is_class)
apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
- apply (simp add: comp_widen list_all2_def)
+ apply (simp add: split_paired_all comp_widen list_all2_def)
apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
apply (rule exI)+
- apply (rule comp_method)
- apply assumption+
+ apply (simp add: wf_prog_ws_prog [THEN comp_method])
+ apply auto
done
@@ -1329,7 +1326,7 @@
-- {* @{text "<=s"} *}
apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
- apply (frule comp_method, assumption+)
+ apply (simp add: wf_prog_ws_prog [THEN comp_method])
apply (simp add: max_spec_preserves_length [THEN sym])
-- "@{text check_type}"
@@ -1341,7 +1338,7 @@
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp+
-apply (simp only: comp_is_type [THEN sym])
+apply (simp only: comp_is_type)
apply (frule method_wf_mdecl) apply assumption apply assumption
apply (simp add: wf_mdecl_def wf_mhead_def)
apply (simp add: max_def)
@@ -1714,6 +1711,7 @@
apply (simp (no_asm_simp), rule bc_mt_corresp_Checkcast)
apply (simp add: comp_is_class)
apply (simp only: compTpExpr_LT_ST)
+apply (drule cast_RefT)
apply blast
apply (simp add: start_sttp_resp_def)
@@ -1885,7 +1883,7 @@
apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast)
apply (simp (no_asm_simp))
apply (rule bc_mt_corresp_Getfield) apply assumption+
- apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl)
+ apply (fast intro: wt_class_expr_is_class)
apply (simp (no_asm_simp) add: start_sttp_resp_def)
@@ -1905,7 +1903,7 @@
apply (rule bc_mt_corresp_Dup_x1)
apply (simp (no_asm_simp) add: dup_x1ST_def)
apply (rule bc_mt_corresp_Putfield) apply assumption+
- apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl)
+ apply (fast intro: wt_class_expr_is_class)
apply (simp (no_asm_simp) add: start_sttp_resp_def)
apply (simp (no_asm_simp) add: start_sttp_resp_def)
apply (simp (no_asm_simp) add: start_sttp_resp_def)
@@ -1922,7 +1920,7 @@
apply (simp only: compTpExprs_LT_ST)
apply (simp (no_asm_simp))
apply (rule bc_mt_corresp_Invoke) apply assumption+
- apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl)
+ apply (fast intro: wt_class_expr_is_class)
apply (simp (no_asm_simp) add: start_sttp_resp_def)
apply (rule start_sttp_resp_comb)
apply (simp (no_asm_simp))
@@ -2247,14 +2245,13 @@
apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+
apply (intro strip)
apply (rule wt_instr_Goto)
- apply (simp (no_asm_simp) add: nat_canonify)
- apply (simp (no_asm_simp) add: nat_canonify)
+ apply arith
+ apply arith
(* \<dots> ! nat (int pc + i) = \<dots> ! pc *)
- apply (simp (no_asm_simp) add: nat_canonify)
+ apply (simp (no_asm_simp))
apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
- apply (simp (no_asm_simp) only: int_outside_right nat_int)
apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
@@ -2592,52 +2589,56 @@
apply (simp only: split_paired_All, simp)
(* subgoal is_class / wf_mhead / wf_java_mdecl *)
-apply (rule methd [THEN conjunct2]) apply assumption+ apply (simp only:)
-apply (rule wf_prog_wf_mhead, assumption+) apply (simp only:)
+apply (blast intro: methd [THEN conjunct2])
+apply (frule wf_prog_wf_mdecl, assumption+) apply (simp only:) apply (simp add: wf_mdecl_def)
apply (rule wf_java_prog_wf_java_mdecl, assumption+)
-
done
- (**********************************************************************************)
-
-
-
lemma comp_set_ms: "(C, D, fs, cms)\<in>set (comp G)
\<Longrightarrow> \<exists> ms. (C, D, fs, ms) \<in>set G \<and> cms = map (compMethod G C) ms"
by (auto simp: comp_def compClass_def)
-lemma method_body_source: "\<lbrakk> wf_prog wf_mb G; is_class G C; method (comp G, C) sig = Some (D, rT, cmb) \<rbrakk>
- \<Longrightarrow> (\<exists> mb. method (G, C) sig = Some (D, rT, mb))"
-apply (simp add: comp_method_eq comp_method_result_def)
-apply (case_tac "method (G, C) sig")
-apply auto
-done
+
+ (* ---------------------------------------------------------------------- *)
section "Main Theorem"
(* MAIN THEOREM:
Methodtype computed by comp is correct for bytecode generated by compTp *)
theorem wt_prog_comp: "wf_java_prog G \<Longrightarrow> wt_jvm_prog (comp G) (compTp G)"
apply (simp add: wf_prog_def)
+
apply (subgoal_tac "wf_java_prog G") prefer 2 apply (simp add: wf_prog_def)
apply (simp (no_asm_simp) add: wf_prog_def wt_jvm_prog_def)
-apply (simp add: comp_unique comp_wf_syscls wf_cdecl_def)
+apply (simp add: comp_ws_prog)
+
+apply (intro strip)
+apply (subgoal_tac "\<exists> C D fs cms. c = (C, D, fs, cms)")
apply clarify
apply (frule comp_set_ms)
apply clarify
apply (drule bspec, assumption)
-apply (simp add: comp_wf_fdecl)
-apply (simp add: wf_mdecl_def)
-
apply (rule conjI)
-apply (rule ballI)
-apply (subgoal_tac "\<exists> sig rT mb. x = (sig, rT, mb)") prefer 2 apply (case_tac x, simp)
+
+ (* wf_mrT *)
+apply (case_tac "C = Object")
+apply (simp add: wf_mrT_def)
+apply (subgoal_tac "is_class G D")
+apply (simp add: comp_wf_mrT)
+apply (simp add: wf_prog_def ws_prog_def ws_cdecl_def)
+apply blast
+
+ (* wf_cdecl_mdecl *)
+apply (simp add: wf_cdecl_mdecl_def)
+apply (simp add: split_beta)
+apply (intro strip)
+
+ (* show wt_method \<dots> *)
+apply (subgoal_tac "\<exists> sig rT mb. x = (sig, rT, mb)")
apply (erule exE)+
apply (simp (no_asm_simp) add: compMethod_def split_beta)
apply (erule conjE)+
apply (drule_tac x="(sig, rT, mb)" in bspec) apply simp
-apply (rule conjI)
-apply (simp add: comp_wf_mhead)
apply (rule_tac mn="fst sig" and pTs="snd sig" in wt_method_comp)
apply assumption+
apply simp
@@ -2647,27 +2648,11 @@
apply simp
apply simp
apply (simp add: compMethod_def split_beta)
-
-apply (rule conjI)
-apply (rule unique_map_fst [THEN iffD1])
- apply (simp (no_asm_simp) add: compMethod_def split_beta) apply simp
-
-apply clarify
-apply (rule conjI) apply (simp add: comp_is_class)
-apply (rule conjI) apply (simp add: comp_subcls)
-apply (simp add: compMethod_def split_beta)
-apply (intro strip)
- apply (drule_tac x=x in bspec, assumption, drule_tac x="D'" in spec, drule_tac x="rT'" in spec)
- apply (erule exE)
-
-apply (frule method_body_source) apply assumption+
-apply (drule mp, assumption)
-apply (simp add: comp_widen)
+apply auto
done
-
(**********************************************************************************)
declare split_paired_All [simp add]
--- a/src/HOL/MicroJava/Comp/Index.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/Comp/Index.thy Mon May 26 18:36:15 2003 +0200
@@ -63,6 +63,10 @@
apply simp
done
+lemma lift_if: "(f (if b then t else e)) = (if b then (f t) else (f e))"
+apply auto
+done
+
lemma update_at_index: "
\<lbrakk> distinct (gjmb_plns (gmb G C S));
x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow>
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Mon May 26 18:36:15 2003 +0200
@@ -8,9 +8,16 @@
theory LemmasComp = TranslComp:
+
+declare split_paired_All [simp del]
+declare split_paired_Ex [simp del]
+
+
(**********************************************************************)
(* misc lemmas *)
+
+
lemma split_pairs: "(\<lambda>(a,b). (F a b)) (ab) = F (fst ab) (snd ab)"
proof -
have "(\<lambda>(a,b). (F a b)) (fst ab,snd ab) = F (fst ab) (snd ab)"
@@ -34,6 +41,44 @@
by (case_tac st, simp add: c_hupd_conv gh_def)
+lemma unique_map_fst [rule_format]: "(\<forall> x \<in> set xs. (fst x = fst (f x) )) \<longrightarrow>
+ unique (map f xs) = unique xs"
+proof (induct xs)
+ case Nil show ?case by simp
+next
+ case (Cons a list)
+ show ?case
+ proof
+ assume fst_eq: "\<forall>x\<in>set (a # list). fst x = fst (f x)"
+
+ have fst_set: "(fst a \<in> fst ` set list) = (fst (f a) \<in> fst ` f ` set list)"
+ proof
+ assume as: "fst a \<in> fst ` set list"
+ then obtain x where fst_a_x: "x\<in>set list \<and> fst a = fst x"
+ by (auto simp add: image_iff)
+ then have "fst (f a) = fst (f x)" by (simp add: fst_eq)
+ with as show "(fst (f a) \<in> fst ` f ` set list)" by (simp add: fst_a_x)
+ next
+ assume as: "fst (f a) \<in> fst ` f ` set list"
+ then obtain x where fst_a_x: "x\<in>set list \<and> fst (f a) = fst (f x)"
+ by (auto simp add: image_iff)
+ then have "fst a = fst x" by (simp add: fst_eq)
+ with as show "fst a \<in> fst ` set list" by (simp add: fst_a_x)
+ qed
+
+ with fst_eq Cons
+ show "unique (map f (a # list)) = unique (a # list)"
+ by (simp add: unique_def fst_set)
+ qed
+qed
+
+lemma comp_unique: "unique (comp G) = unique G"
+apply (simp add: comp_def)
+apply (rule unique_map_fst)
+apply (simp add: compClass_def split_beta)
+done
+
+
(**********************************************************************)
(* invariance of properties under compilation *)
@@ -53,75 +98,96 @@
apply (simp add: image_compose [THEN sym] o_def split_beta del: image_compose)
done
-lemma comp_is_class: "is_class G C = is_class (comp G) C"
+lemma comp_is_class: "is_class (comp G) C = is_class G C"
by (case_tac "class G C", auto simp: is_class_def comp_class_None dest: comp_class_imp)
-lemma comp_is_type: "is_type G T = is_type (comp G) T"
+lemma comp_is_type: "is_type (comp G) T = is_type G T"
by ((cases T),simp,(induct G)) ((simp),(simp only: comp_is_class),(simp add: comp_is_class),(simp only: comp_is_class))
-lemma SIGMA_cong: "\<lbrakk> A = B; !!x. x \<in> B \<Longrightarrow> C x = D x \<rbrakk> \<Longrightarrow> (\<Sigma> x \<in> A. C x) = (\<Sigma> x \<in> B. D x)"
+lemma SIGMA_cong: "\<lbrakk> A = B; !!x. x \<in> B \<Longrightarrow> C x = D x \<rbrakk>
+ \<Longrightarrow> (\<Sigma> x \<in> A. C x) = (\<Sigma> x \<in> B. D x)"
by auto
-lemma comp_classname: "is_class G C \<Longrightarrow> fst (the (class G C)) = fst (the (class (comp G) C))"
+lemma comp_classname: "is_class G C
+ \<Longrightarrow> fst (the (class G C)) = fst (the (class (comp G) C))"
by (case_tac "class G C", auto simp: is_class_def dest: comp_class_imp)
-lemma comp_subcls1: "subcls1 G = subcls1 (comp G)"
+lemma comp_subcls1: "subcls1 (comp G) = subcls1 G"
apply (simp add: subcls1_def2 comp_is_class)
apply (rule SIGMA_cong, simp)
-apply (simp add: comp_is_class [THEN sym])
+apply (simp add: comp_is_class)
apply (simp add: comp_classname)
done
-lemma comp_subcls: "(subcls1 G)^* = (subcls1 (comp G))^*"
- by (induct G) (simp_all add: comp_def comp_subcls1)
-
-lemma comp_widen: "((ty1,ty2) \<in> widen G) = ((ty1,ty2) \<in> widen (comp G))"
+lemma comp_widen: "((ty1,ty2) \<in> widen (comp G)) = ((ty1,ty2) \<in> widen G)"
apply rule
+ apply (cases "(ty1,ty2)" "comp G" rule: widen.cases)
+ apply (simp_all add: comp_subcls1 widen.null)
apply (cases "(ty1,ty2)" G rule: widen.cases)
- apply (simp_all add: comp_subcls widen.null)
- apply (cases "(ty1,ty2)" "comp G" rule: widen.cases)
- apply (simp_all add: comp_subcls widen.null)
+ apply (simp_all add: comp_subcls1 widen.null)
done
-lemma comp_cast: "((ty1,ty2) \<in> cast G) = ((ty1,ty2) \<in> cast (comp G))"
+lemma comp_cast: "((ty1,ty2) \<in> cast (comp G)) = ((ty1,ty2) \<in> cast G)"
apply rule
+ apply (cases "(ty1,ty2)" "comp G" rule: cast.cases)
+ apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
+ apply (rule cast.widen) apply (simp add: comp_widen)
apply (cases "(ty1,ty2)" G rule: cast.cases)
- apply (simp_all add: comp_subcls cast.widen cast.subcls)
- apply (cases "(ty1,ty2)" "comp G" rule: cast.cases)
- apply (simp_all add: comp_subcls cast.widen cast.subcls)
+ apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
+ apply (rule cast.widen) apply (simp add: comp_widen)
done
-lemma comp_cast_ok: "cast_ok G = cast_ok (comp G)"
+lemma comp_cast_ok: "cast_ok (comp G) = cast_ok G"
by (simp add: expand_fun_eq cast_ok_def comp_widen)
-lemma comp_wf_fdecl: "wf_fdecl G fd \<Longrightarrow> wf_fdecl (comp G) fd"
-apply (case_tac fd)
-apply (simp add: wf_fdecl_def comp_is_type)
+lemma compClass_fst [simp]: "(fst (compClass G C)) = (fst C)"
+by (simp add: compClass_def split_beta)
+
+lemma compClass_fst_snd [simp]: "(fst (snd (compClass G C))) = (fst (snd C))"
+by (simp add: compClass_def split_beta)
+
+lemma compClass_fst_snd_snd [simp]: "(fst (snd (snd (compClass G C)))) = (fst (snd (snd C)))"
+by (simp add: compClass_def split_beta)
+
+lemma comp_wf_fdecl [simp]: "wf_fdecl (comp G) fd = wf_fdecl G fd"
+by (case_tac fd, simp add: wf_fdecl_def comp_is_type)
+
+
+lemma compClass_forall [simp]: "
+ (\<forall>x\<in>set (snd (snd (snd (compClass G C)))). P (fst x) (fst (snd x))) =
+ (\<forall>x\<in>set (snd (snd (snd C))). P (fst x) (fst (snd x)))"
+by (simp add: compClass_def compMethod_def split_beta)
+
+lemma comp_wf_mhead: "wf_mhead (comp G) S rT = wf_mhead G S rT"
+by (simp add: wf_mhead_def split_beta comp_is_type)
+
+lemma comp_ws_cdecl: "
+ ws_cdecl (TranslComp.comp G) (compClass G C) = ws_cdecl G C"
+apply (simp add: ws_cdecl_def split_beta comp_is_class comp_subcls1)
+apply (simp (no_asm_simp) add: comp_wf_mhead)
+apply (simp add: compClass_def compMethod_def split_beta unique_map_fst)
done
-lemma comp_wf_syscls: "wf_syscls G = wf_syscls (comp G)"
+
+lemma comp_wf_syscls: "wf_syscls (comp G) = wf_syscls G"
apply (simp add: wf_syscls_def comp_def compClass_def split_beta)
apply (simp only: image_compose [THEN sym])
-apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls). (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
-(*
-apply (subgoal_tac "(fst o (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls). (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
-*)
+apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
+ (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
apply (simp del: image_compose)
apply (simp add: expand_fun_eq split_beta)
done
-lemma comp_wf_mhead: "wf_mhead G S rT = wf_mhead (comp G) S rT"
-by (simp add: wf_mhead_def split_beta comp_is_type)
-
-lemma comp_wf_mdecl: "\<lbrakk> wf_mdecl wf_mb G C jmdl;
- (wf_mb G C jmdl) \<longrightarrow> (wf_mb_comp (comp G) C (compMethod G C jmdl)) \<rbrakk>
- \<Longrightarrow>
- wf_mdecl wf_mb_comp (comp G) C (compMethod G C jmdl)"
-by (simp add: wf_mdecl_def wf_mhead_def comp_is_type split_beta compMethod_def)
+lemma comp_ws_prog: "ws_prog (comp G) = ws_prog G"
+apply (rule sym)
+apply (simp add: ws_prog_def comp_ws_cdecl comp_unique)
+apply (simp add: comp_wf_syscls)
+apply (auto simp add: comp_ws_cdecl [THEN sym] TranslComp.comp_def)
+done
lemma comp_class_rec: " wf ((subcls1 G)^-1) \<Longrightarrow>
@@ -159,16 +225,16 @@
done
lemma comp_fields: "wf ((subcls1 G)^-1) \<Longrightarrow>
- fields (G,C) = fields (comp G,C)"
+ fields (comp G,C) = fields (G,C)"
by (simp add: fields_def comp_class_rec)
lemma comp_field: "wf ((subcls1 G)^-1) \<Longrightarrow>
- field (G,C) = field (comp G,C)"
+ field (comp G,C) = field (G,C)"
by (simp add: field_def comp_fields)
-lemma class_rec_relation [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G;
+lemma class_rec_relation [rule_format (no_asm)]: "\<lbrakk> ws_prog G;
\<forall> fs ms. R (f1 Object fs ms t1) (f2 Object fs ms t2);
\<forall> C fs ms r1 r2. (R r1 r2) \<longrightarrow> (R (f1 C fs ms r1) (f2 C fs ms r2)) \<rbrakk>
\<Longrightarrow> ((class G C) \<noteq> None) \<longrightarrow>
@@ -194,10 +260,11 @@
(* subgoals *)
-apply (frule class_wf) apply assumption
-apply (simp add: wf_cdecl_def is_class_def)
+apply (frule class_wf_struct) apply assumption
+apply (simp add: ws_cdecl_def is_class_def)
apply (simp add: subcls1_def2 is_class_def)
+apply auto
done
@@ -206,189 +273,114 @@
translations
"mtd_mb" => "Fun.comp snd snd"
-
-lemma map_of_map_fst: "\<lbrakk> map_of (map f xs) k = Some e; inj f;
+lemma map_of_map_fst: "\<lbrakk> inj f;
\<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
- \<Longrightarrow> map_of (map g xs) k = Some (snd (g ((inv f) (k, e))))"
+ \<Longrightarrow> map_of (map g xs) k
+ = option_map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
apply (induct xs)
apply simp
apply (simp del: split_paired_All)
apply (case_tac "k = fst a")
apply (simp del: split_paired_All)
-apply (subgoal_tac "(fst a, e) = f a")
+apply (subgoal_tac "(inv f (fst a, snd (f a))) = a", simp)
+apply (subgoal_tac "(fst a, snd (f a)) = f a", simp)
+apply (erule conjE)+
+apply (drule_tac s ="fst (f a)" and t="fst a" in sym)
apply simp
-apply (rule_tac s= "(fst (f a), snd (f a))" in trans)
-apply simp
-apply (rule surjective_pairing [THEN sym])
-apply (simp del: split_paired_All)
+apply (simp add: surjective_pairing)
done
-lemma comp_method [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk> \<Longrightarrow>
- (method (G, C) S) = Some (D, rT, mb) \<longrightarrow>
- (method (comp G, C) S) = Some (D, rT, mtd_mb (compMethod G D (S, rT, mb)))"
+lemma comp_method [rule_format (no_asm)]: "\<lbrakk> ws_prog G; is_class G C\<rbrakk> \<Longrightarrow>
+ ((method (comp G, C) S) =
+ option_map (\<lambda> (D,rT,b). (D, rT, mtd_mb (compMethod G D (S, rT, b))))
+ (method (G, C) S))"
apply (simp add: method_def)
apply (frule wf_subcls1)
apply (simp add: comp_class_rec)
apply (simp add: map_compose [THEN sym] split_iter split_compose del: map_compose)
-apply (rule_tac R="%x y. (x S) = Some (D, rT, mb) \<longrightarrow> (y S) = Some (D, rT, snd (snd (compMethod G D (S, rT, mb))))" in class_rec_relation) apply assumption
+apply (rule_tac R="%x y. ((x S) = (option_map (\<lambda>(D, rT, b).
+ (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))"
+ in class_rec_relation)
+apply assumption
apply (intro strip)
apply simp
-apply (frule_tac f="(\<lambda>(s, m). (s, Object, m))"
- and g="(Fun.comp (\<lambda>(s, m). (s, Object, m)) (compMethod G Object))" in map_of_map_fst)
-(*
-apply (frule_tac f="(\<lambda>(s, m). (s, Object, m))"
- and g="((\<lambda>(s, m). (s, Object, m)) \<circ> compMethod G Object)" in map_of_map_fst)
-*)
-apply (simp add: inj_on_def)
+apply (rule trans)
+
+apply (rule_tac f="(\<lambda>(s, m). (s, Object, m))" and
+ g="(Fun.comp (\<lambda>(s, m). (s, Object, m)) (compMethod G Object))"
+ in map_of_map_fst)
+defer (* inj \<dots> *)
+apply (simp add: inj_on_def split_beta)
apply (simp add: split_beta compMethod_def)
-apply (simp add: split_beta compMethod_def)
+apply (simp add: map_of_map [THEN sym])
+apply (simp add: split_beta)
+apply (simp add: map_compose [THEN sym] Fun.comp_def split_beta)
+apply (subgoal_tac "(\<lambda>x\<Colon>(vname list \<times> fdecl list \<times> stmt \<times> expr) mdecl.
+ (fst x, Object,
+ snd (compMethod G Object
+ (inv (\<lambda>(s\<Colon>sig, m\<Colon>ty \<times> vname list \<times> fdecl list \<times> stmt \<times> expr).
+ (s, Object, m))
+ (S, Object, snd x)))))
+ = (\<lambda>x. (fst x, Object, fst (snd x),
+ snd (snd (compMethod G Object (S, snd x)))))")
apply (simp only:)
-apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, D, rT, mb)) = (S, rT, mb)")
+apply (simp add: expand_fun_eq)
+apply (intro strip)
+apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)")
apply (simp only:)
apply (simp add: compMethod_def split_beta)
-apply (simp add: map_of_map) apply (erule exE)+ apply simp
-apply (simp add: map_of_map) apply (erule exE)+ apply simp
-apply (rule inv_f_eq) apply (simp add: inj_on_def) apply simp
+apply (rule inv_f_eq)
+defer
+defer
apply (intro strip)
apply (simp add: map_add_Some_iff map_of_map del: split_paired_Ex)
+apply (simp add: map_add_def)
+apply (subgoal_tac "inj (\<lambda>(s, m). (s, Ca, m))")
+apply (drule_tac g="(Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca))" and xs=ms
+ and k=S in map_of_map_fst)
+apply (simp add: split_beta)
+apply (simp add: compMethod_def split_beta)
+apply (case_tac "(map_of (map (\<lambda>(s, m). (s, Ca, m)) ms) S)")
+apply simp
+apply simp apply (simp add: split_beta map_of_map) apply (erule exE) apply (erule conjE)+
+apply (drule_tac t=a in sym)
+apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Ca, m)) (S, a)) = (S, snd a)")
+apply simp
apply (subgoal_tac "\<forall>x\<in>set ms. fst ((Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x")
-(*
-apply (subgoal_tac "\<forall>x\<in>set ms. fst (((\<lambda>(s, m). (s, Ca, m)) \<circ> compMethod G Ca) x) = fst x")
-*)
-apply (erule disjE)
-apply (rule disjI1)
+ prefer 2 apply (simp (no_asm_simp) add: compMethod_def split_beta)
apply (simp add: map_of_map2)
apply (simp (no_asm_simp) add: compMethod_def split_beta)
-apply (rule disjI2)
-apply (simp add: map_of_map2)
-
- -- "subgoal"
-apply (simp (no_asm_simp) add: compMethod_def split_beta)
-
-apply (simp add: is_class_def)
+ -- "remaining subgoals"
+apply (auto intro: inv_f_eq simp add: inj_on_def is_class_def)
done
-constdefs comp_method_result :: "java_mb prog \<Rightarrow> sig \<Rightarrow>
- (cname \<times> ty \<times> java_mb) option \<Rightarrow> (cname \<times> ty \<times> jvm_method) option"
- "comp_method_result G S m == case m of
- None \<Rightarrow> None
- | Some (D, rT, mb) \<Rightarrow> Some (D, rT, mtd_mb (compMethod G D (S, rT, mb)))"
-
-lemma map_of_map_compMethod: "map_of (map (\<lambda>(s, m). (s, C, m)) (map (compMethod G C) ms)) S =
- (case map_of (map (\<lambda>(s, m). (s, C, m)) ms) S of None \<Rightarrow> None
- | Some (D, rT, mb) \<Rightarrow> Some (D, rT, mtd_mb (compMethod G D (S, rT, mb))))"
-apply (induct ms)
-apply simp
-apply (simp only: map_compose [THEN sym])
-apply (simp add: o_def split_beta del: map.simps)
-apply (simp (no_asm_simp) only: map.simps map_of.simps)
-apply (simp add: compMethod_def split_beta)
-done
-
- (* the following is more expressive than comp_method and should replace it *)
-lemma comp_method_eq [rule_format (no_asm)]: "wf_prog wf_mb G \<Longrightarrow> is_class G C \<longrightarrow>
-method (comp G, C) S = comp_method_result G S (method (G,C) S)"
-apply (subgoal_tac "wf ((subcls1 G)^-1)") prefer 2 apply (rule wf_subcls1, assumption)
-
-apply (rule subcls_induct)
-apply assumption
-apply (intro strip)
-apply (subgoal_tac "\<exists> D fs ms. class G C = Some (D, fs, ms)")
- prefer 2 apply (simp add: is_class_def)
-apply (erule exE)+
-
-apply (case_tac "C = Object")
-
- (* C = Object *)
-apply (subst method_rec_lemma) apply assumption+ apply simp
-apply (subst method_rec_lemma) apply (frule comp_class_imp) apply assumption+
- apply (simp add: comp_subcls1)
-apply (simp add: comp_method_result_def)
-apply (rule map_of_map_compMethod)
-
- (* C \<noteq> Object *)
-apply (subgoal_tac "(C, D) \<in> (subcls1 G)\<^sup>+")
- prefer 2 apply (frule subcls1I, assumption+) apply blast
-apply (subgoal_tac "is_class G D")
-apply (drule spec, drule mp, assumption, drule mp, assumption)
-apply (frule wf_subcls1)
-apply (subgoal_tac "wf ((subcls1 (comp G))\<inverse>)")
-apply (frule_tac G=G in method_rec_lemma, assumption)
-apply (frule comp_class_imp)
-apply (frule_tac G="comp G" in method_rec_lemma, assumption)
-apply (simp only:)
-apply (simp (no_asm_simp) add: comp_method_result_def expand_fun_eq)
-
-apply (case_tac "(method (G, D) ++ map_of (map (\<lambda>(s, m). (s, C, m)) ms)) S")
-
- (* case None *)
-apply (simp (no_asm_simp) add: map_add_None)
-apply (simp add: map_of_map_compMethod comp_method_result_def)
-
- (* case Some *)
-apply (simp add: map_add_Some_iff)
-apply (erule disjE)
- apply (simp add: split_beta map_of_map_compMethod)
- apply (simp add: map_add_def comp_method_result_def map_of_map_compMethod)
-
- (* show subgoals *)
-apply (simp add: comp_subcls1)
- (* show is_class G D *)
-apply (simp add: wf_prog_def wf_cdecl_def)
-apply (subgoal_tac "(C, D, fs, ms)\<in>set G")
-apply blast
-apply (simp add: class_def map_of_SomeD)
-done
-
- (* ### this proof is horrid and has to be redone *)
-lemma unique_map_fst [rule_format]: "(\<forall> x \<in> set xs. (fst x = fst (f x) )) \<longrightarrow>
- unique xs = unique (map f xs)"
-apply (induct_tac "xs")
-apply simp
+lemma comp_wf_mrT: "\<lbrakk> ws_prog G; is_class G D\<rbrakk> \<Longrightarrow>
+ wf_mrT (TranslComp.comp G) (C, D, fs, map (compMethod G a) ms) =
+ wf_mrT G (C, D, fs, ms)"
+apply (simp add: wf_mrT_def compMethod_def split_beta)
+apply (simp add: comp_widen)
+apply (rule iffI)
apply (intro strip)
apply simp
-apply (case_tac a, simp)
-apply (case_tac "f (aa, b)")
-apply (simp only:)
-apply (simp only: unique_Cons)
-
-apply simp
-apply (subgoal_tac "(\<exists>y. (ab, y) \<in> set list) = (\<exists>y. (ab, y) \<in> f ` set list)")
-apply blast
-apply (rule iffI)
-
-apply clarify
-apply (rule_tac x="(snd (f(ab, y)))" in exI)
-apply simp
-apply (subgoal_tac "(ab, snd (f (ab, y))) = (fst (f (ab, y)), snd (f (ab, y)))")
-apply (simp only:)
-apply (simp add: surjective_pairing [THEN sym])
-apply (subgoal_tac "fst (f (ab, y)) = fst (ab, y)")
-apply simp
-apply (drule bspec) apply assumption apply simp
-
-apply clarify
-apply (drule bspec) apply assumption apply simp
-apply (subgoal_tac "ac = ab")
-apply simp
-apply blast
-apply (drule sym)
-apply (drule sym)
-apply (drule_tac f=fst in arg_cong)
-apply simp
-done
-
-lemma comp_unique: "unique G = unique (comp G)"
-apply (simp add: comp_def)
-apply (rule unique_map_fst)
-apply (simp add: compClass_def split_beta)
+apply (drule bspec) apply assumption
+apply (drule_tac x=D' in spec) apply (drule_tac x=rT' in spec) apply (drule mp)
+prefer 2 apply assumption
+apply (simp add: comp_method [of G D])
+apply (erule exE)+
+apply (subgoal_tac "z =(fst z, fst (snd z), snd (snd z))")
+apply (rule exI)
+apply (simp)
+apply (simp add: split_paired_all)
+apply (intro strip)
+apply (simp add: comp_method)
+apply auto
done
@@ -396,9 +388,6 @@
(* DIVERSE OTHER LEMMAS *)
(**********************************************************************)
-
-(* already proved less elegantly in CorrComp.thy;
- to be moved into a common super-theory *)
lemma max_spec_preserves_length:
"max_spec G C (mn, pTs) = {((md,rT),pTs')}
\<Longrightarrow> length pTs = length pTs'"
@@ -408,7 +397,6 @@
done
-(* already proved in CorrComp.thy \<longrightarrow> into common supertheory *)
lemma ty_exprs_length [simp]: "(E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts)"
apply (subgoal_tac "(E\<turnstile>e::T \<longrightarrow> True) \<and> (E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts) \<and> (E\<turnstile>s\<surd> \<longrightarrow> True)")
apply blast
@@ -425,5 +413,13 @@
apply (simp add: method_rT_def)
done
+ (**********************************************************************************)
+
+declare compClass_fst [simp del]
+declare compClass_fst_snd [simp del]
+declare compClass_fst_snd_snd [simp del]
+
+declare split_paired_All [simp add]
+declare split_paired_Ex [simp add]
end
--- a/src/HOL/MicroJava/Comp/TypeInf.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/Comp/TypeInf.thy Mon May 26 18:36:15 2003 +0200
@@ -20,7 +20,7 @@
by (erule ty_expr.cases, auto)
lemma Cast_invers: "E\<turnstile>Cast D e::T
- \<Longrightarrow> \<exists> C. T = Class D \<and> E\<turnstile>e::Class C \<and> is_class (prg E) D \<and> prg E\<turnstile>C\<preceq>? D"
+ \<Longrightarrow> \<exists> C. T = Class D \<and> E\<turnstile>e::C \<and> is_class (prg E) D \<and> prg E\<turnstile>C\<preceq>? Class D"
by (erule ty_expr.cases, auto)
lemma Lit_invers: "E\<turnstile>Lit x::T
@@ -87,9 +87,10 @@
(* Uniqueness of types property *)
lemma uniqueness_of_types: "
- (\<forall> E T1 T2. E\<turnstile>e :: T1 \<longrightarrow> E\<turnstile>e :: T2 \<longrightarrow> T1 = T2) \<and>
- (\<forall> E Ts1 Ts2. E\<turnstile>es [::] Ts1 \<longrightarrow> E\<turnstile>es [::] Ts2 \<longrightarrow> Ts1 = Ts2)"
-
+ (\<forall> (E\<Colon>'a prog \<times> (vname \<Rightarrow> ty option)) T1 T2.
+ E\<turnstile>e :: T1 \<longrightarrow> E\<turnstile>e :: T2 \<longrightarrow> T1 = T2) \<and>
+ (\<forall> (E\<Colon>'a prog \<times> (vname \<Rightarrow> ty option)) Ts1 Ts2.
+ E\<turnstile>es [::] Ts1 \<longrightarrow> E\<turnstile>es [::] Ts2 \<longrightarrow> Ts1 = Ts2)"
apply (rule expr.induct)
(* NewC *)
--- a/src/HOL/MicroJava/J/Example.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Mon May 26 18:36:15 2003 +0200
@@ -293,60 +293,74 @@
done
lemma wf_ObjectC:
-"wf_cdecl wf_java_mdecl tprg ObjectC"
-apply (unfold wf_cdecl_def wf_fdecl_def ObjectC_def)
+"ws_cdecl tprg ObjectC \<and>
+ wf_cdecl_mdecl wf_java_mdecl tprg ObjectC \<and> wf_mrT tprg ObjectC"
+apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
+ wf_mrT_def wf_fdecl_def ObjectC_def)
apply (simp (no_asm))
done
lemma wf_NP:
-"wf_cdecl wf_java_mdecl tprg NullPointerC"
-apply (unfold wf_cdecl_def wf_fdecl_def NullPointerC_def)
+"ws_cdecl tprg NullPointerC \<and>
+ wf_cdecl_mdecl wf_java_mdecl tprg NullPointerC \<and> wf_mrT tprg NullPointerC"
+apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
+ wf_mrT_def wf_fdecl_def NullPointerC_def)
apply (simp add: class_def)
apply (fold NullPointerC_def class_def)
apply auto
done
lemma wf_OM:
-"wf_cdecl wf_java_mdecl tprg OutOfMemoryC"
-apply (unfold wf_cdecl_def wf_fdecl_def OutOfMemoryC_def)
+"ws_cdecl tprg OutOfMemoryC \<and>
+ wf_cdecl_mdecl wf_java_mdecl tprg OutOfMemoryC \<and> wf_mrT tprg OutOfMemoryC"
+apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
+ wf_mrT_def wf_fdecl_def OutOfMemoryC_def)
apply (simp add: class_def)
apply (fold OutOfMemoryC_def class_def)
apply auto
done
lemma wf_CC:
-"wf_cdecl wf_java_mdecl tprg ClassCastC"
-apply (unfold wf_cdecl_def wf_fdecl_def ClassCastC_def)
+"ws_cdecl tprg ClassCastC \<and>
+ wf_cdecl_mdecl wf_java_mdecl tprg ClassCastC \<and> wf_mrT tprg ClassCastC"
+apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
+ wf_mrT_def wf_fdecl_def ClassCastC_def)
apply (simp add: class_def)
apply (fold ClassCastC_def class_def)
apply auto
done
lemma wf_BaseC:
-"wf_cdecl wf_java_mdecl tprg BaseC"
-apply (unfold wf_cdecl_def wf_fdecl_def BaseC_def)
+"ws_cdecl tprg BaseC \<and>
+ wf_cdecl_mdecl wf_java_mdecl tprg BaseC \<and> wf_mrT tprg BaseC"
+apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
+ wf_mrT_def wf_fdecl_def BaseC_def)
apply (simp (no_asm))
apply (fold BaseC_def)
-apply (rule wf_foo_Base [THEN conjI])
+apply (rule mp) defer apply (rule wf_foo_Base)
+apply (auto simp add: wf_mdecl_def)
+done
+
+
+lemma wf_ExtC:
+"ws_cdecl tprg ExtC \<and>
+ wf_cdecl_mdecl wf_java_mdecl tprg ExtC \<and> wf_mrT tprg ExtC"
+apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
+ wf_mrT_def wf_fdecl_def ExtC_def)
+apply (simp (no_asm))
+apply (fold ExtC_def)
+apply (rule mp) defer apply (rule wf_foo_Ext)
+apply (auto simp add: wf_mdecl_def)
+apply (drule rtranclD)
apply auto
done
-lemma wf_ExtC:
-"wf_cdecl wf_java_mdecl tprg ExtC"
-apply (unfold wf_cdecl_def wf_fdecl_def ExtC_def)
-apply (simp (no_asm))
-apply (fold ExtC_def)
-apply (rule wf_foo_Ext [THEN conjI])
-apply auto
-apply (drule rtranclD)
-apply auto
-done
lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def)
lemma wf_tprg:
"wf_prog wf_java_mdecl tprg"
-apply (unfold wf_prog_def Let_def)
+apply (unfold wf_prog_def ws_prog_def Let_def)
apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes)
apply (rule wf_syscls)
apply (simp add: SystemClasses_def)
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Mon May 26 18:36:15 2003 +0200
@@ -15,23 +15,30 @@
(x,(h(a\<mapsto>(C,(init_vars (fields (G,C))))), l))::\<preceq>(G, lT)"
apply( erule conforms_upd_obj)
apply( unfold oconf_def)
-apply( auto dest!: fields_is_type)
+apply( auto dest!: fields_is_type simp add: wf_prog_ws_prog)
done
-
+
+
lemma Cast_conf:
- "[| wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>Class C; G\<turnstile>C\<preceq>? D; cast_ok G D h v|]
- ==> G,h\<turnstile>v::\<preceq>Class D"
+ "[| wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>CC; G\<turnstile>CC \<preceq>? Class D; cast_ok G D h v|]
+ ==> G,h\<turnstile>v::\<preceq>Class D"
+apply (case_tac "CC")
+apply simp
+apply (case_tac "ref_ty")
+apply (clarsimp simp add: conf_def)
+apply simp
+apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D", simp)
+apply (rule conf_widen, assumption+) apply (erule widen.subcls)
+
apply (unfold cast_ok_def)
apply( case_tac "v = Null")
apply( simp)
-apply( drule widen_RefT)
apply( clarify)
apply( drule (1) non_npD)
apply( auto intro!: conf_AddrI simp add: obj_ty_def)
done
-
lemma FAcc_type_sound:
"[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (x,(h,l))::\<preceq>(G,lT);
x' = None --> G,h\<turnstile>a'::\<preceq> Class C; np a' x' = None |] ==>
@@ -43,6 +50,7 @@
apply auto
apply( drule conforms_heapD [THEN hconfD])
apply( assumption)
+apply (frule wf_prog_ws_prog)
apply( drule (2) widen_cfs_fields)
apply( drule (1) oconf_objD)
apply auto
@@ -82,6 +90,7 @@
apply( force)
apply( rule oconf_hext)
apply( erule_tac [2] hext_upd_obj)
+apply (frule wf_prog_ws_prog)
apply( drule (2) widen_cfs_fields)
apply( rule oconf_obj [THEN iffD2])
apply( simp (no_asm))
@@ -157,7 +166,6 @@
apply( fast elim!: widen_trans)
apply (rule conforms_xcpt_change)
apply( rule conforms_hext) apply assumption
-(* apply( erule conforms_hext)*)
apply( erule (1) hext_trans)
apply( erule conforms_heapD)
apply (simp add: conforms_def)
@@ -168,6 +176,8 @@
declare split_if [split del]
declare fun_upd_apply [simp del]
declare fun_upd_same [simp]
+declare wf_prog_ws_prog [simp]
+
ML{*
val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
@@ -267,6 +277,7 @@
apply (rule Cast_conf)
apply assumption+
+
-- "7 LAss"
apply (fold fun_upd_def)
apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims")
@@ -342,7 +353,8 @@
apply( simp)
apply (rule conjI)
apply( fast elim: hext_trans)
- apply (rule conforms_xcpt_change, assumption) apply (simp (no_asm_simp) add: xconf_def)
+ apply (rule conforms_xcpt_change, assumption)
+ apply (simp (no_asm_simp) add: xconf_def)
apply(clarsimp)
apply( drule ty_expr_is_type, simp)
@@ -370,6 +382,15 @@
apply auto
done
+lemma evals_type_sound: "!!E s s'.
+ [| G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); G=prg E; wf_java_prog G; (x,s)::\<preceq>E; E\<turnstile>es[::]Ts |]
+ ==> (x',s')::\<preceq>E \<and> (x'=None --> list_all2 (conf G (heap s')) vs Ts)"
+apply( simp (no_asm_simp) only: split_tupled_all)
+apply (drule eval_evals_exec_type_sound
+ [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp])
+apply auto
+done
+
lemma exec_type_sound: "!!E s s'.
[| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd> |]
==> (x',s')::\<preceq>E"
@@ -395,6 +416,7 @@
declare split_beta [simp del]
declare fun_upd_apply [simp]
+declare wf_prog_ws_prog [simp del]
end
--- a/src/HOL/MicroJava/J/TypeRel.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Mon May 26 18:36:15 2003 +0200
@@ -11,19 +11,19 @@
consts
subcls1 :: "'c prog => (cname \<times> cname) set" -- "subclass"
widen :: "'c prog => (ty \<times> ty ) set" -- "widening"
- cast :: "'c prog => (cname \<times> cname) set" -- "casting"
+ cast :: "'c prog => (ty \<times> ty ) set" -- "casting"
syntax (xsymbols)
subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
- cast :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
+ cast :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
syntax
subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
subcls :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
widen :: "'c prog => [ty , ty ] => bool" ("_ |- _ <= _" [71,71,71] 70)
- cast :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
+ cast :: "'c prog => [ty , ty ] => bool" ("_ |- _ <=? _" [71,71,71] 70)
translations
"G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
@@ -132,8 +132,8 @@
-- "casting conversion, cf. 5.5 / 5.1.5"
-- "left out casts on primitve types"
inductive "cast G" intros
- widen: "G\<turnstile>C\<preceq>C D ==> G\<turnstile>C \<preceq>? D"
- subcls: "G\<turnstile>D\<preceq>C C ==> G\<turnstile>C \<preceq>? D"
+ widen: "G\<turnstile> C\<preceq> D ==> G\<turnstile>C \<preceq>? D"
+ subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D"
lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False"
apply (rule iffI)
@@ -168,6 +168,21 @@
apply (auto elim: widen.subcls)
done
+lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D"
+by (ind_cases "G \<turnstile> T \<preceq> NT", auto)
+
+lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False"
+apply (rule iffI)
+apply (erule cast.elims)
+apply auto
+done
+
+lemma cast_RefT: "G \<turnstile> C \<preceq>? Class D \<Longrightarrow> \<exists> rT. C = RefT rT"
+apply (erule cast.cases)
+apply simp apply (erule widen.cases)
+apply auto
+done
+
theorem widen_trans[trans]: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
proof -
assume "G\<turnstile>S\<preceq>U" thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
--- a/src/HOL/MicroJava/J/WellForm.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Mon May 26 18:36:15 2003 +0200
@@ -27,12 +27,40 @@
types 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
constdefs
+ wf_syscls :: "'c prog => bool"
+"wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"
+
wf_fdecl :: "'c prog => fdecl => bool"
"wf_fdecl G == \<lambda>(fn,ft). is_type G ft"
wf_mhead :: "'c prog => sig => ty => bool"
"wf_mhead G == \<lambda>(mn,pTs) rT. (\<forall>T\<in>set pTs. is_type G T) \<and> is_type G rT"
+ ws_cdecl :: "'c prog => 'c cdecl => bool"
+"ws_cdecl G ==
+ \<lambda>(C,(D,fs,ms)).
+ (\<forall>f\<in>set fs. wf_fdecl G f) \<and> unique fs \<and>
+ (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT) \<and> unique ms \<and>
+ (C \<noteq> Object \<longrightarrow> is_class G D \<and> \<not>G\<turnstile>D\<preceq>C C)"
+
+ ws_prog :: "'c prog => bool"
+"ws_prog G ==
+ wf_syscls G \<and> (\<forall>c\<in>set G. ws_cdecl G c) \<and> unique G"
+
+ wf_mrT :: "'c prog => 'c cdecl => bool"
+"wf_mrT G ==
+ \<lambda>(C,(D,fs,ms)).
+ (C \<noteq> Object \<longrightarrow> (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'.
+ method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))"
+
+ wf_cdecl_mdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
+"wf_cdecl_mdecl wf_mb G ==
+ \<lambda>(C,(D,fs,ms)). (\<forall>m\<in>set ms. wf_mb G C m)"
+
+ wf_prog :: "'c wf_mb => 'c prog => bool"
+"wf_prog wf_mb G ==
+ ws_prog G \<and> (\<forall>c\<in> set G. wf_mrT G c \<and> wf_cdecl_mdecl wf_mb G c)"
+
wf_mdecl :: "'c wf_mb => 'c wf_mb"
"wf_mdecl wf_mb G C == \<lambda>(sig,rT,mb). wf_mhead G sig rT \<and> wf_mb G C (sig,rT,mb)"
@@ -45,33 +73,62 @@
(\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'.
method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))"
- wf_syscls :: "'c prog => bool"
-"wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"
+lemma wf_cdecl_mrT_cdecl_mdecl:
+ "(wf_cdecl wf_mb G c) = (ws_cdecl G c \<and> wf_mrT G c \<and> wf_cdecl_mdecl wf_mb G c)"
+apply (rule iffI)
+apply (simp add: wf_cdecl_def ws_cdecl_def wf_mrT_def wf_cdecl_mdecl_def
+ wf_mdecl_def wf_mhead_def split_beta)+
+done
- wf_prog :: "'c wf_mb => 'c prog => bool"
-"wf_prog wf_mb G ==
- let cs = set G in wf_syscls G \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G"
+lemma wf_cdecl_ws_cdecl [intro]: "wf_cdecl wf_mb G cd \<Longrightarrow> ws_cdecl G cd"
+by (simp add: wf_cdecl_mrT_cdecl_mdecl)
+
+lemma wf_prog_ws_prog [intro]: "wf_prog wf_mb G \<Longrightarrow> ws_prog G"
+by (simp add: wf_prog_def ws_prog_def)
+
+lemma wf_prog_wf_mdecl:
+ "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; ((mn,pTs),rT,code) \<in> set mdecls\<rbrakk>
+ \<Longrightarrow> wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
+by (auto simp add: wf_prog_def ws_prog_def wf_mdecl_def
+ wf_cdecl_mdecl_def ws_cdecl_def)
lemma class_wf:
- "[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)"
-apply (unfold wf_prog_def class_def)
-apply (simp)
+ "[|class G C = Some c; wf_prog wf_mb G|]
+ ==> wf_cdecl wf_mb G (C,c) \<and> wf_mrT G (C,c)"
+apply (unfold wf_prog_def ws_prog_def wf_cdecl_def class_def)
+apply clarify
+apply (drule_tac x="(C,c)" in bspec, fast dest: map_of_SomeD)
+apply (drule_tac x="(C,c)" in bspec, fast dest: map_of_SomeD)
+apply (simp add: wf_cdecl_def ws_cdecl_def wf_mdecl_def
+ wf_cdecl_mdecl_def wf_mrT_def split_beta)
+done
+
+lemma class_wf_struct:
+ "[|class G C = Some c; ws_prog G|]
+ ==> ws_cdecl G (C,c)"
+apply (unfold ws_prog_def class_def)
apply (fast dest: map_of_SomeD)
done
lemma class_Object [simp]:
- "wf_prog wf_mb G ==> \<exists>X fs ms. class G Object = Some (X,fs,ms)"
-apply (unfold wf_prog_def wf_syscls_def class_def)
+ "ws_prog G ==> \<exists>X fs ms. class G Object = Some (X,fs,ms)"
+apply (unfold ws_prog_def wf_syscls_def class_def)
apply (auto simp: map_of_SomeI)
done
-lemma is_class_Object [simp]: "wf_prog wf_mb G ==> is_class G Object"
+lemma class_Object_syscls [simp]:
+ "wf_syscls G ==> unique G \<Longrightarrow> \<exists>X fs ms. class G Object = Some (X,fs,ms)"
+apply (unfold wf_syscls_def class_def)
+apply (auto simp: map_of_SomeI)
+done
+
+lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object"
apply (unfold is_class_def)
apply (simp (no_asm_simp))
done
-lemma is_class_xcpt [simp]: "wf_prog wf_mb G \<Longrightarrow> is_class G (Xcpt x)"
- apply (simp add: wf_prog_def wf_syscls_def)
+lemma is_class_xcpt [simp]: "ws_prog G \<Longrightarrow> is_class G (Xcpt x)"
+ apply (simp add: ws_prog_def wf_syscls_def)
apply (simp add: is_class_def class_def)
apply clarify
apply (erule_tac x = x in allE)
@@ -79,38 +136,38 @@
apply (auto intro!: map_of_SomeI)
done
-lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; wf_prog wf_mb G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+"
+lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+"
apply( frule r_into_trancl)
apply( drule subcls1D)
apply(clarify)
-apply( drule (1) class_wf)
-apply( unfold wf_cdecl_def)
+apply( drule (1) class_wf_struct)
+apply( unfold ws_cdecl_def)
apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
done
lemma wf_cdecl_supD:
-"!!r. \<lbrakk>wf_cdecl wf_mb G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D"
-apply (unfold wf_cdecl_def)
+"!!r. \<lbrakk>ws_cdecl G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D"
+apply (unfold ws_cdecl_def)
apply (auto split add: option.split_asm)
done
-lemma subcls_asym: "[|wf_prog wf_mb G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+"
+lemma subcls_asym: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+"
apply(erule tranclE)
apply(fast dest!: subcls1_wfD )
apply(fast dest!: subcls1_wfD intro: trancl_trans)
done
-lemma subcls_irrefl: "[|wf_prog wf_mb G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D"
+lemma subcls_irrefl: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D"
apply (erule trancl_trans_induct)
apply (auto dest: subcls1_wfD subcls_asym)
done
-lemma acyclic_subcls1: "wf_prog wf_mb G ==> acyclic (subcls1 G)"
+lemma acyclic_subcls1: "ws_prog G ==> acyclic (subcls1 G)"
apply (unfold acyclic_def)
apply (fast dest: subcls_irrefl)
done
-lemma wf_subcls1: "wf_prog wf_mb G ==> wf ((subcls1 G)^-1)"
+lemma wf_subcls1: "ws_prog G ==> wf ((subcls1 G)^-1)"
apply (rule finite_acyclic_wf)
apply ( subst finite_converse)
apply ( rule finite_subcls1)
@@ -118,12 +175,14 @@
apply (erule acyclic_subcls1)
done
+
lemma subcls_induct:
"[|wf_prog wf_mb G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
(is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
proof -
assume p: "PROP ?P"
assume ?A thus ?thesis apply -
+apply (drule wf_prog_ws_prog)
apply(drule wf_subcls1)
apply(drule wf_trancl)
apply(simp only: trancl_converse)
@@ -155,7 +214,57 @@
apply( case_tac "C = Object")
apply( fast)
apply safe
-apply( frule (1) class_wf)
+apply( frule (1) class_wf) apply (erule conjE)+
+apply (frule wf_cdecl_ws_cdecl)
+apply( frule (1) wf_cdecl_supD)
+
+apply( subgoal_tac "G\<turnstile>C\<prec>C1a")
+apply( erule_tac [2] subcls1I)
+apply( rule p)
+apply (unfold is_class_def)
+apply auto
+done
+qed
+
+lemma subcls_induct_struct:
+"[|ws_prog G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
+(is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
+proof -
+ assume p: "PROP ?P"
+ assume ?A thus ?thesis apply -
+apply(drule wf_subcls1)
+apply(drule wf_trancl)
+apply(simp only: trancl_converse)
+apply(erule_tac a = C in wf_induct)
+apply(rule p)
+apply(auto)
+done
+qed
+
+
+lemma subcls1_induct_struct:
+"[|is_class G C; ws_prog G; P Object;
+ !!C D fs ms. [|C \<noteq> Object; is_class G C; class G C = Some (D,fs,ms) \<and>
+ ws_cdecl G (C,D,fs,ms) \<and> G\<turnstile>C\<prec>C1D \<and> is_class G D \<and> P D|] ==> P C
+ |] ==> P C"
+(is "?A \<Longrightarrow> ?B \<Longrightarrow> ?C \<Longrightarrow> PROP ?P \<Longrightarrow> _")
+proof -
+ assume p: "PROP ?P"
+ assume ?A ?B ?C thus ?thesis apply -
+apply(unfold is_class_def)
+apply( rule impE)
+prefer 2
+apply( assumption)
+prefer 2
+apply( assumption)
+apply( erule thin_rl)
+apply( rule subcls_induct_struct)
+apply( assumption)
+apply( rule impI)
+apply( case_tac "C = Object")
+apply( fast)
+apply safe
+apply( frule (1) class_wf_struct)
apply( frule (1) wf_cdecl_supD)
apply( subgoal_tac "G\<turnstile>C\<prec>C1a")
@@ -170,7 +279,7 @@
lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma];
-lemma field_rec: "\<lbrakk>class G C = Some (D, fs, ms); wf_prog wf_mb G\<rbrakk>
+lemma field_rec: "\<lbrakk>class G C = Some (D, fs, ms); ws_prog G\<rbrakk>
\<Longrightarrow> field (G, C) =
(if C = Object then empty else field (G, D)) ++
map_of (map (\<lambda>(s, f). (s, C, f)) fs)"
@@ -183,14 +292,14 @@
done
lemma method_Object [simp]:
- "method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> wf_prog wf_mb G \<Longrightarrow> D = Object"
+ "method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> ws_prog G \<Longrightarrow> D = Object"
apply (frule class_Object, clarify)
apply (drule method_rec, assumption)
apply (auto dest: map_of_SomeD)
done
-lemma fields_Object [simp]: "\<lbrakk> ((vn, C), T) \<in> set (fields (G, Object)); wf_prog wf_mb G \<rbrakk>
+lemma fields_Object [simp]: "\<lbrakk> ((vn, C), T) \<in> set (fields (G, Object)); ws_prog G \<rbrakk>
\<Longrightarrow> C = Object"
apply (frule class_Object)
apply clarify
@@ -202,8 +311,8 @@
apply simp
done
-lemma subcls_C_Object: "[|is_class G C; wf_prog wf_mb G|] ==> G\<turnstile>C\<preceq>C Object"
-apply(erule subcls1_induct)
+lemma subcls_C_Object: "[|is_class G C; ws_prog G|] ==> G\<turnstile>C\<preceq>C Object"
+apply(erule subcls1_induct_struct)
apply( assumption)
apply( fast)
apply(auto dest!: wf_cdecl_supD)
@@ -215,9 +324,9 @@
apply auto
done
-lemma widen_fields_defpl': "[|is_class G C; wf_prog wf_mb G|] ==>
+lemma widen_fields_defpl': "[|is_class G C; ws_prog G|] ==>
\<forall>((fn,fd),fT)\<in>set (fields (G,C)). G\<turnstile>C\<preceq>C fd"
-apply( erule subcls1_induct)
+apply( erule subcls1_induct_struct)
apply( assumption)
apply( frule class_Object)
apply( clarify)
@@ -238,21 +347,21 @@
done
lemma widen_fields_defpl:
- "[|((fn,fd),fT) \<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==>
+ "[|((fn,fd),fT) \<in> set (fields (G,C)); ws_prog G; is_class G C|] ==>
G\<turnstile>C\<preceq>C fd"
apply( drule (1) widen_fields_defpl')
apply (fast)
done
lemma unique_fields:
- "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
-apply( erule subcls1_induct)
+ "[|is_class G C; ws_prog G|] ==> unique (fields (G,C))"
+apply( erule subcls1_induct_struct)
apply( assumption)
apply( frule class_Object)
apply( clarify)
apply( frule fields_rec, assumption)
-apply( drule class_wf, assumption)
-apply( simp add: wf_cdecl_def)
+apply( drule class_wf_struct, assumption)
+apply( simp add: ws_cdecl_def)
apply( rule unique_map_inj)
apply( simp)
apply( rule inj_onI)
@@ -263,9 +372,9 @@
apply( subst fields_rec)
apply auto
apply( rotate_tac -1)
-apply( frule class_wf)
+apply( frule class_wf_struct)
apply auto
-apply( simp add: wf_cdecl_def)
+apply( simp add: ws_cdecl_def)
apply( erule unique_append)
apply( rule unique_map_inj)
apply( clarsimp)
@@ -275,7 +384,7 @@
done
lemma fields_mono_lemma [rule_format (no_asm)]:
- "[|wf_prog wf_mb G; (C',C)\<in>(subcls1 G)^*|] ==>
+ "[|ws_prog G; (C',C)\<in>(subcls1 G)^*|] ==>
x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
apply(erule converse_rtrancl_induct)
apply( safe dest!: subcls1D)
@@ -284,7 +393,7 @@
done
lemma fields_mono:
-"\<lbrakk>map_of (fields (G,C)) fn = Some f; G\<turnstile>D\<preceq>C C; is_class G D; wf_prog wf_mb G\<rbrakk>
+"\<lbrakk>map_of (fields (G,C)) fn = Some f; G\<turnstile>D\<preceq>C C; is_class G D; ws_prog G\<rbrakk>
\<Longrightarrow> map_of (fields (G,D)) fn = Some f"
apply (rule map_of_SomeI)
apply (erule (1) unique_fields)
@@ -293,7 +402,7 @@
done
lemma widen_cfs_fields:
-"[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; wf_prog wf_mb G|]==>
+"[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; ws_prog G|]==>
map_of (fields (G,D)) (fn, fd) = Some fT"
apply (drule field_fields)
apply (drule rtranclD)
@@ -307,6 +416,7 @@
"wf_prog wf_mb G ==> is_class G C \<Longrightarrow>
method (G,C) sig = Some (md,mh,m)
--> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))"
+apply (frule wf_prog_ws_prog)
apply( erule subcls1_induct)
apply( assumption)
apply( clarify)
@@ -317,7 +427,7 @@
apply( simp add: wf_cdecl_def)
apply( drule map_of_SomeD)
apply( subgoal_tac "md = Object")
-apply( fastsimp)
+apply( fastsimp)
apply( fastsimp)
apply( clarify)
apply( frule_tac C = C in method_rec)
@@ -338,22 +448,45 @@
done
-lemma wf_prog_wf_mhead: "\<lbrakk> wf_prog wf_mb G; (C, D, fds, mths) \<in> set G;
- ((mn, pTs), rT, jmb) \<in> set mths \<rbrakk>
- \<Longrightarrow> wf_mhead G (mn, pTs) rT"
-apply (simp add: wf_prog_def wf_cdecl_def)
-apply (erule conjE)+
-apply (drule bspec, assumption)
-apply simp
-apply (erule conjE)+
-apply (drule bspec, assumption)
-apply (simp add: wf_mdecl_def)
+lemma method_wf_mhead [rule_format (no_asm)]:
+ "ws_prog G ==> is_class G C \<Longrightarrow>
+ method (G,C) sig = Some (md,rT,mb)
+ --> G\<turnstile>C\<preceq>C md \<and> wf_mhead G sig rT"
+apply( erule subcls1_induct_struct)
+apply( assumption)
+apply( clarify)
+apply( frule class_Object)
+apply( clarify)
+apply( frule method_rec, assumption)
+apply( drule class_wf_struct, assumption)
+apply( simp add: ws_cdecl_def)
+apply( drule map_of_SomeD)
+apply( subgoal_tac "md = Object")
+apply( fastsimp)
+apply( fastsimp)
+apply( clarify)
+apply( frule_tac C = C in method_rec)
+apply( assumption)
+apply( rotate_tac -1)
+apply( simp)
+apply( drule map_add_SomeD)
+apply( erule disjE)
+apply( erule_tac V = "?P --> ?Q" in thin_rl)
+apply (frule map_of_SomeD)
+apply (clarsimp simp add: ws_cdecl_def)
+apply blast
+apply clarify
+apply( rule rtrancl_trans)
+prefer 2
+apply( assumption)
+apply( rule r_into_rtrancl)
+apply( fast intro: subcls1I)
done
lemma subcls_widen_methd [rule_format (no_asm)]:
- "[|G\<turnstile>T\<preceq>C T'; wf_prog wf_mb G|] ==>
- \<forall>D rT b. method (G,T') sig = Some (D,rT ,b) -->
- (\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \<and> G\<turnstile>rT'\<preceq>rT)"
+ "[|G\<turnstile>T'\<preceq>C T; wf_prog wf_mb G|] ==>
+ \<forall>D rT b. method (G,T) sig = Some (D,rT ,b) -->
+ (\<exists>D' rT' b'. method (G,T') sig = Some (D',rT',b') \<and> G\<turnstile>D'\<preceq>C D \<and> G\<turnstile>rT'\<preceq>rT)"
apply( drule rtranclD)
apply( erule disjE)
apply( fast)
@@ -362,14 +495,14 @@
prefer 2
apply( clarify)
apply( drule spec, drule spec, drule spec, erule (1) impE)
-apply( fast elim: widen_trans)
+apply( fast elim: widen_trans rtrancl_trans)
apply( clarify)
apply( drule subcls1D)
apply( clarify)
apply( subst method_rec)
apply( assumption)
apply( unfold map_add_def)
-apply( simp (no_asm_simp) del: split_paired_Ex)
+apply( simp (no_asm_simp) add: wf_prog_ws_prog del: split_paired_Ex)
apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z")
apply( erule exE)
apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
@@ -377,25 +510,34 @@
apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
apply( tactic "asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1")
apply( simp_all (no_asm_simp) del: split_paired_Ex)
-apply( drule (1) class_wf)
+apply( frule (1) class_wf)
apply( simp (no_asm_simp) only: split_tupled_all)
apply( unfold wf_cdecl_def)
apply( drule map_of_SomeD)
-apply auto
+apply (auto simp add: wf_mrT_def)
+apply (rule rtrancl_trans)
+defer
+apply (rule method_wf_mhead [THEN conjunct1])
+apply (simp only: wf_prog_def)
+apply (simp add: is_class_def)
+apply assumption
+apply (auto intro: subcls1I)
done
+
lemma subtype_widen_methd:
"[| G\<turnstile> C\<preceq>C D; wf_prog wf_mb G;
method (G,D) sig = Some (md, rT, b) |]
==> \<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
-apply(auto dest: subcls_widen_methd method_wf_mdecl
+apply(auto dest: subcls_widen_methd
simp add: wf_mdecl_def wf_mhead_def split_def)
done
+
lemma method_in_md [rule_format (no_asm)]:
- "wf_prog wf_mb G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code)
+ "ws_prog G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code)
--> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
-apply (erule (1) subcls1_induct)
+apply (erule (1) subcls1_induct_struct)
apply clarify
apply (frule method_Object, assumption)
apply hypsubst
@@ -416,18 +558,42 @@
done
+lemma method_in_md_struct [rule_format (no_asm)]:
+ "ws_prog G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code)
+ --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
+apply (erule (1) subcls1_induct_struct)
+ apply clarify
+ apply (frule method_Object, assumption)
+ apply hypsubst
+ apply simp
+apply (erule conjE)
+apply (subst method_rec)
+ apply (assumption)
+ apply (assumption)
+apply (clarify)
+apply (erule_tac "x" = "Da" in allE)
+apply (clarsimp)
+ apply (simp add: map_of_map)
+ apply (clarify)
+ apply (subst method_rec)
+ apply (assumption)
+ apply (assumption)
+ apply (simp add: map_add_def map_of_map split add: option.split)
+done
+
lemma fields_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk>
\<Longrightarrow> \<forall> vn D T. (((vn,D),T) \<in> set (fields (G,C))
\<longrightarrow> (is_class G D \<and> ((vn,D),T) \<in> set (fields (G,D))))"
apply (erule (1) subcls1_induct)
apply clarify
+apply (frule wf_prog_ws_prog)
apply (frule fields_Object, assumption+)
apply (simp only: is_class_Object) apply simp
apply clarify
apply (frule fields_rec)
-apply assumption
+apply (simp (no_asm_simp) add: wf_prog_ws_prog)
apply (case_tac "Da=C")
apply blast (* case Da=C *)
@@ -448,6 +614,7 @@
apply clarify
apply (frule field_fields)
apply (drule map_of_SomeD)
+apply (frule wf_prog_ws_prog)
apply (drule fields_Object, assumption+)
apply simp
@@ -460,6 +627,7 @@
apply (rule trans [THEN sym], rule sym, assumption)
apply (rule_tac x=vn in fun_cong)
apply (rule trans, rule field_rec, assumption+)
+apply (simp (no_asm_simp) add: wf_prog_ws_prog)
apply (simp (no_asm_use)) apply blast
done
@@ -478,6 +646,7 @@
apply (rule map_of_SomeD)
apply (rule table_of_remap_SomeD)
apply assumption+
+apply (simp (no_asm_simp) add: wf_prog_ws_prog)+
done
lemma Call_lemma:
@@ -495,16 +664,15 @@
apply auto
done
-
lemma fields_is_type_lemma [rule_format (no_asm)]:
- "[|is_class G C; wf_prog wf_mb G|] ==>
+ "[|is_class G C; ws_prog G|] ==>
\<forall>f\<in>set (fields (G,C)). is_type G (snd f)"
-apply( erule (1) subcls1_induct)
+apply( erule (1) subcls1_induct_struct)
apply( frule class_Object)
apply( clarify)
apply( frule fields_rec, assumption)
-apply( drule class_wf, assumption)
-apply( simp add: wf_cdecl_def wf_fdecl_def)
+apply( drule class_wf_struct, assumption)
+apply( simp add: ws_cdecl_def wf_fdecl_def)
apply( fastsimp)
apply( subst fields_rec)
apply( fast)
@@ -513,34 +681,43 @@
apply( safe)
prefer 2
apply( force)
-apply( drule (1) class_wf)
-apply( unfold wf_cdecl_def)
+apply( drule (1) class_wf_struct)
+apply( unfold ws_cdecl_def)
apply( clarsimp)
apply( drule (1) bspec)
apply( unfold wf_fdecl_def)
apply auto
done
+
lemma fields_is_type:
- "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==>
+ "[|map_of (fields (G,C)) fn = Some f; ws_prog G; is_class G C|] ==>
is_type G f"
apply(drule map_of_SomeD)
apply(drule (2) fields_is_type_lemma)
apply(auto)
done
+
+lemma field_is_type: "\<lbrakk> ws_prog G; is_class G C; field (G, C) fn = Some (fd, fT) \<rbrakk>
+ \<Longrightarrow> is_type G fT"
+apply (frule_tac f="((fn, fd), fT)" in fields_is_type_lemma)
+apply (auto simp add: field_def dest: map_of_SomeD)
+done
+
+
lemma methd:
- "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |]
+ "[| ws_prog G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |]
==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C"
proof -
- assume wf: "wf_prog wf_mb G" and C: "(C,S,fs,mdecls) \<in> set G" and
+ assume wf: "ws_prog G" and C: "(C,S,fs,mdecls) \<in> set G" and
m: "(sig,rT,code) \<in> set mdecls"
moreover
from wf C have "class G C = Some (S,fs,mdecls)"
- by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
+ by (auto simp add: ws_prog_def class_def is_class_def intro: map_of_SomeI)
moreover
from wf C
- have "unique mdecls" by (unfold wf_prog_def wf_cdecl_def) auto
+ have "unique mdecls" by (unfold ws_prog_def ws_cdecl_def) auto
hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)" by (induct mdecls, auto)
with m
have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
@@ -553,20 +730,11 @@
lemma wf_mb'E:
"\<lbrakk> wf_prog wf_mb G; \<And>C S fs ms m.\<lbrakk>(C,S,fs,ms) \<in> set G; m \<in> set ms\<rbrakk> \<Longrightarrow> wf_mb' G C m \<rbrakk>
\<Longrightarrow> wf_prog wf_mb' G"
- apply (simp add: wf_prog_def)
+ apply (simp only: wf_prog_def)
apply auto
- apply (simp add: wf_cdecl_def wf_mdecl_def)
+ apply (simp add: wf_cdecl_mdecl_def)
apply safe
apply (drule bspec, assumption) apply simp
- apply (drule bspec, assumption) apply simp
- apply (drule bspec, assumption) apply simp
- apply clarify apply (drule bspec, assumption) apply simp
- apply (drule bspec, assumption) apply simp
- apply (drule bspec, assumption) apply simp
- apply (drule bspec, assumption) apply simp
- apply (drule bspec, assumption) apply simp
- apply (drule bspec, assumption) apply simp
- apply clarify apply (drule bspec, assumption)+ apply simp
done
--- a/src/HOL/MicroJava/J/WellType.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Mon May 26 18:36:15 2003 +0200
@@ -108,19 +108,19 @@
-- "local variables might include This, which is hidden anyway"
consts
- ty_expr :: "(java_mb env \<times> expr \<times> ty ) set"
- ty_exprs:: "(java_mb env \<times> expr list \<times> ty list) set"
- wt_stmt :: "(java_mb env \<times> stmt ) set"
+ ty_expr :: "('c env \<times> expr \<times> ty ) set"
+ ty_exprs:: "('c env \<times> expr list \<times> ty list) set"
+ wt_stmt :: "('c env \<times> stmt ) set"
syntax (xsymbols)
- ty_expr :: "java_mb env => [expr , ty ] => bool" ("_ \<turnstile> _ :: _" [51,51,51]50)
- ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
- wt_stmt :: "java_mb env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51,51 ]50)
+ ty_expr :: "'c env => [expr , ty ] => bool" ("_ \<turnstile> _ :: _" [51,51,51]50)
+ ty_exprs:: "'c env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
+ wt_stmt :: "'c env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51,51 ]50)
syntax
- ty_expr :: "java_mb env => [expr , ty ] => bool" ("_ |- _ :: _" [51,51,51]50)
- ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
- wt_stmt :: "java_mb env => stmt => bool" ("_ |- _ [ok]" [51,51 ]50)
+ ty_expr :: "'c env => [expr , ty ] => bool" ("_ |- _ :: _" [51,51,51]50)
+ ty_exprs:: "'c env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
+ wt_stmt :: "'c env => stmt => bool" ("_ |- _ [ok]" [51,51 ]50)
translations
@@ -134,9 +134,9 @@
E\<turnstile>NewC C::Class C" -- "cf. 15.8"
-- "cf. 15.15"
- Cast: "[| E\<turnstile>e::Class C; is_class (prg E) D;
- prg E\<turnstile>C\<preceq>? D |] ==>
- E\<turnstile>Cast D e::Class D"
+ Cast: "[| E\<turnstile>e::C; is_class (prg E) D;
+ prg E\<turnstile>C\<preceq>? Class D |] ==>
+ E\<turnstile>Cast D e:: Class D"
-- "cf. 15.7.1"
Lit: "[| typeof (\<lambda>v. None) x = Some T |] ==>
@@ -213,7 +213,7 @@
constdefs
- wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool"
+ wf_java_mdecl :: "'c prog => cname => java_mb mdecl => bool"
"wf_java_mdecl G C == \<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
length pTs = length pns \<and>
distinct pns \<and>
@@ -225,25 +225,22 @@
E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
syntax
- wf_java_prog :: "java_mb prog => bool"
+ wf_java_prog :: "'c prog => bool"
translations
"wf_java_prog" == "wf_prog wf_java_mdecl"
lemma wf_java_prog_wf_java_mdecl: "\<lbrakk>
wf_java_prog G; (C, D, fds, mths) \<in> set G; jmdcl \<in> set mths \<rbrakk>
\<Longrightarrow> wf_java_mdecl G C jmdcl"
-apply (simp add: wf_prog_def)
-apply (simp add: wf_cdecl_def)
+apply (simp only: wf_prog_def)
apply (erule conjE)+
apply (drule bspec, assumption)
-apply simp
-apply (erule conjE)+
-apply (drule bspec, assumption)
-apply (simp add: wf_mdecl_def split_beta)
+apply (simp add: wf_cdecl_mdecl_def split_beta)
done
-lemma wt_is_type: "(E\<turnstile>e::T \<longrightarrow> wf_prog wf_mb (prg E) \<longrightarrow> is_type (prg E) T) \<and>
- (E\<turnstile>es[::]Ts \<longrightarrow> wf_prog wf_mb (prg E) \<longrightarrow> Ball (set Ts) (is_type (prg E))) \<and>
+
+lemma wt_is_type: "(E\<turnstile>e::T \<longrightarrow> ws_prog (prg E) \<longrightarrow> is_type (prg E) T) \<and>
+ (E\<turnstile>es[::]Ts \<longrightarrow> ws_prog (prg E) \<longrightarrow> Ball (set Ts) (is_type (prg E))) \<and>
(E\<turnstile>c \<surd> \<longrightarrow> True)"
apply (rule ty_expr_ty_exprs_wt_stmt.induct)
apply auto
@@ -253,10 +250,15 @@
apply ( drule (1) fields_is_type)
apply ( simp (no_asm_simp))
apply (assumption)
-apply (auto dest!: max_spec2mheads method_wf_mdecl is_type_rTI
+apply (auto dest!: max_spec2mheads method_wf_mhead is_type_rTI
simp add: wf_mdecl_def)
done
lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, rule_format]
+lemma expr_class_is_class: "
+ \<lbrakk>ws_prog (prg E); E \<turnstile> e :: Class C\<rbrakk> \<Longrightarrow> is_class (prg E) C"
+ by (frule ty_expr_is_type, assumption, simp)
+
+
end