--- a/src/HOL/IsaMakefile Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/IsaMakefile Wed Oct 23 16:09:02 2002 +0200
@@ -487,6 +487,16 @@
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \
+ MicroJava/Comp/AuxLemmas.thy \
+ MicroJava/Comp/CorrComp.thy \
+ MicroJava/Comp/CorrCompTp.thy \
+ MicroJava/Comp/DefsComp.thy \
+ MicroJava/Comp/Index.thy \
+ MicroJava/Comp/LemmasComp.thy \
+ MicroJava/Comp/NatCanonify.thy \
+ MicroJava/Comp/TranslComp.thy \
+ MicroJava/Comp/TranslCompTp.thy \
+ MicroJava/Comp/TypeInf.thy \
MicroJava/J/Conform.thy MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \
MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \
MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Altern.thy Wed Oct 23 16:09:02 2002 +0200
@@ -0,0 +1,67 @@
+
+theory Altern = BVSpec:
+
+
+constdefs
+ check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"
+ "check_type G mxs mxr s \<equiv> s \<in> states G mxs mxr"
+
+ wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count,
+ exception_table,p_count] \<Rightarrow> bool"
+ "wt_instr_altern i G rT phi mxs mxr max_pc et pc \<equiv>
+ app i G mxs rT pc et (phi!pc) \<and>
+ check_type G mxs mxr (OK (phi!pc)) \<and>
+ (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
+
+ wt_method_altern :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
+ exception_table,method_type] \<Rightarrow> bool"
+ "wt_method_altern G C pTs rT mxs mxl ins et phi \<equiv>
+ let max_pc = length ins in
+ 0 < max_pc \<and>
+ length phi = length ins \<and>
+ check_bounded ins et \<and>
+ wt_start G C pTs mxl phi \<and>
+ (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr_altern (ins!pc) G rT phi mxs (1+length pTs+mxl) max_pc et pc)"
+
+
+lemma wt_method_wt_method_altern :
+ "wt_method G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method_altern G C pTs rT mxs mxl ins et phi"
+apply (simp add: wt_method_def wt_method_altern_def)
+apply (intro strip)
+apply clarify
+apply (drule spec, drule mp, assumption)
+apply (simp add: check_types_def wt_instr_def wt_instr_altern_def check_type_def)
+apply (auto intro: imageI)
+done
+
+
+lemma check_type_check_types [rule_format]:
+ "(\<forall>pc. pc < length phi \<longrightarrow> check_type G mxs mxr (OK (phi ! pc)))
+ \<longrightarrow> check_types G mxs mxr (map OK phi)"
+apply (induct phi)
+apply (simp add: check_types_def)
+apply (simp add: check_types_def)
+apply clarify
+apply (frule_tac x=0 in spec)
+apply (simp add: check_type_def)
+apply auto
+done
+
+lemma wt_method_altern_wt_method [rule_format]:
+ "wt_method_altern G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method G C pTs rT mxs mxl ins et phi"
+apply (simp add: wt_method_def wt_method_altern_def)
+apply (intro strip)
+apply clarify
+apply (rule conjI)
+ (* show check_types *)
+apply (rule check_type_check_types)
+apply (simp add: wt_instr_altern_def)
+
+ (* show wt_instr *)
+apply (intro strip)
+apply (drule spec, drule mp, assumption)
+apply (simp add: wt_instr_def wt_instr_altern_def)
+done
+
+
+end
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Oct 23 16:09:02 2002 +0200
@@ -242,7 +242,7 @@
qed
qed
-
+declare raise_if_def [simp]
text {*
The requirement of lemma @{text uncaught_xcpt_correct} (that
the exception is a valid reference on the heap) is always met
--- a/src/HOL/MicroJava/BV/JVMType.thy Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/BV/JVMType.thy Wed Oct 23 16:09:02 2002 +0200
@@ -212,6 +212,11 @@
"(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))"
by (simp add: sup_loc_def Listn.le_def lesub_def list_all2_Cons2)
+lemma sup_state_Cons:
+ "(G \<turnstile> (x#xt, a) <=s (y#yt, b)) =
+ ((G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt,b)))"
+ by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def)
+
theorem sup_loc_length:
"G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
--- a/src/HOL/MicroJava/J/Conform.thy Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Wed Oct 23 16:09:02 2002 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Conformity Relations for Type Soundness Proof} *}
-theory Conform = State + WellType:
+theory Conform = State + WellType + Exceptions:
types 'c env_ = "'c prog \<times> (vname \<leadsto> ty)" -- "same as @{text env} of @{text WellType.thy}"
@@ -28,9 +28,14 @@
hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50)
"G|-h h [ok] == \<forall>a obj. h a = Some obj --> G,h|-obj [ok]"
+
+ xconf :: "aheap \<Rightarrow> val option \<Rightarrow> bool"
+ "xconf hp vo == preallocated hp \<and> (\<forall> v. (vo = Some v) \<longrightarrow> (\<exists> xc. v = (Addr (XcptRef xc))))"
- conforms :: "state => java_mb env_ => bool" ("_ ::<= _" [51,51] 50)
- "s::<=E == prg E|-h heap s [ok] \<and> prg E,heap s|-locals s[::<=]localT E"
+ conforms :: "xstate => java_mb env_ => bool" ("_ ::<= _" [51,51] 50)
+ "s::<=E == prg E|-h heap (store s) [ok] \<and>
+ prg E,heap (store s)|-locals (store s)[::<=]localT E \<and>
+ xconf (heap (store s)) (abrupt s)"
syntax (xsymbols)
@@ -247,6 +252,12 @@
apply( auto simp add: length_Suc_conv)
done
+lemma lconf_restr: "\<lbrakk>lT vn = None; G, h \<turnstile> l [::\<preceq>] lT(vn\<mapsto>T)\<rbrakk> \<Longrightarrow> G, h \<turnstile> l [::\<preceq>] lT"
+apply (unfold lconf_def)
+apply (intro strip)
+apply (case_tac "n = vn")
+apply auto
+done
section "oconf"
@@ -277,29 +288,56 @@
done
+section "xconf"
+
+lemma xconf_raise_if: "xconf h x \<Longrightarrow> xconf h (raise_if b xcn x)"
+by (simp add: xconf_def raise_if_def)
+
+
+
section "conforms"
-lemma conforms_heapD: "(h, l)::\<preceq>(G, lT) ==> G\<turnstile>h h\<surd>"
+lemma conforms_heapD: "(x, (h, l))::\<preceq>(G, lT) ==> G\<turnstile>h h\<surd>"
apply (unfold conforms_def)
apply (simp)
done
-lemma conforms_localD: "(h, l)::\<preceq>(G, lT) ==> G,h\<turnstile>l[::\<preceq>]lT"
+lemma conforms_localD: "(x, (h, l))::\<preceq>(G, lT) ==> G,h\<turnstile>l[::\<preceq>]lT"
+apply (unfold conforms_def)
+apply (simp)
+done
+
+lemma conforms_xcptD: "(x, (h, l))::\<preceq>(G, lT) ==> xconf h x"
apply (unfold conforms_def)
apply (simp)
done
-lemma conformsI: "[|G\<turnstile>h h\<surd>; G,h\<turnstile>l[::\<preceq>]lT|] ==> (h, l)::\<preceq>(G, lT)"
+lemma conformsI: "[|G\<turnstile>h h\<surd>; G,h\<turnstile>l[::\<preceq>]lT; xconf h x|] ==> (x, (h, l))::\<preceq>(G, lT)"
apply (unfold conforms_def)
apply auto
done
-lemma conforms_hext: "[|(h,l)::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |] ==> (h',l)::\<preceq>(G,lT)"
-apply( fast dest: conforms_localD elim!: conformsI lconf_hext)
-done
+lemma conforms_restr: "\<lbrakk>lT vn = None; s ::\<preceq> (G, lT(vn\<mapsto>T)) \<rbrakk> \<Longrightarrow> s ::\<preceq> (G, lT)"
+by (simp add: conforms_def, fast intro: lconf_restr)
+
+lemma conforms_xcpt_change: "\<lbrakk> (x, (h,l))::\<preceq> (G, lT); xconf h x \<longrightarrow> xconf h x' \<rbrakk> \<Longrightarrow> (x', (h,l))::\<preceq> (G, lT)"
+by (simp add: conforms_def)
+
+
+lemma preallocated_hext: "\<lbrakk> preallocated h; h\<le>|h'\<rbrakk> \<Longrightarrow> preallocated h'"
+by (simp add: preallocated_def hext_def)
+
+lemma xconf_hext: "\<lbrakk> xconf h vo; h\<le>|h'\<rbrakk> \<Longrightarrow> xconf h' vo"
+by (simp add: xconf_def preallocated_def hext_def)
+
+lemma conforms_hext: "[|(x,(h,l))::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |]
+ ==> (x,(h',l))::\<preceq>(G,lT)"
+by( fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)
+
lemma conforms_upd_obj:
- "[|(h,l)::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|] ==> (h(a\<mapsto>obj),l)::\<preceq>(G, lT)"
+ "[|(x,(h,l))::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|]
+ ==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)"
apply(rule conforms_hext)
apply auto
apply(rule hconfI)
@@ -309,7 +347,8 @@
done
lemma conforms_upd_local:
-"[|(h, l)::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] ==> (h, l(va\<mapsto>v))::\<preceq>(G, lT)"
+"[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|]
+ ==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)"
apply (unfold conforms_def)
apply( auto elim: lconf_upd)
done
--- a/src/HOL/MicroJava/J/Eval.thy Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Wed Oct 23 16:09:02 2002 +0200
@@ -8,6 +8,30 @@
theory Eval = State + WellType:
+
+ -- "Auxiliary notions"
+
+constdefs
+ fits :: "java_mb prog \<Rightarrow> state \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
+ "G,s\<turnstile>a' fits T \<equiv> case T of PrimT T' \<Rightarrow> False | RefT T' \<Rightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T"
+
+constdefs
+ catch ::"java_mb prog \<Rightarrow> xstate \<Rightarrow> cname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60)
+ "G,s\<turnstile>catch C\<equiv> case abrupt s of None \<Rightarrow> False | Some a \<Rightarrow> G,store s\<turnstile> a fits Class C"
+
+
+
+constdefs
+ lupd :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_\<mapsto>_')"[10,10]1000)
+ "lupd vn v \<equiv> \<lambda> (hp,loc). (hp, (loc(vn\<mapsto>v)))"
+
+constdefs
+ new_xcpt_var :: "vname \<Rightarrow> xstate \<Rightarrow> xstate"
+ "new_xcpt_var vn \<equiv> \<lambda>(x,s). Norm (lupd(vn\<mapsto>the x) s)"
+
+
+ -- "Evaluation relations"
+
consts
eval :: "java_mb prog => (xstate \<times> expr \<times> val \<times> xstate) set"
evals :: "java_mb prog => (xstate \<times> expr list \<times> val list \<times> xstate) set"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Exceptions.thy Wed Oct 23 16:09:02 2002 +0200
@@ -0,0 +1,65 @@
+(* Title: HOL/MicroJava/J/Exceptions.thy
+ ID: $Id$
+ Author: Gerwin Klein, Martin Strecker
+ Copyright 2002 Technische Universitaet Muenchen
+*)
+
+theory Exceptions = State:
+
+text {* a new, blank object with default values in all fields: *}
+constdefs
+ blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj"
+ "blank G C \<equiv> (C,init_vars (fields(G,C)))"
+
+ start_heap :: "'c prog \<Rightarrow> aheap"
+ "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
+ (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
+ (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
+
+
+consts
+ cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname"
+
+translations
+ "cname_of hp v" == "fst (the (hp (the_Addr v)))"
+
+
+constdefs
+ preallocated :: "aheap \<Rightarrow> bool"
+ "preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
+
+lemma preallocatedD:
+ "preallocated hp \<Longrightarrow> \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
+ by (unfold preallocated_def) fast
+
+lemma preallocatedE [elim?]:
+ "preallocated hp \<Longrightarrow> (\<And>fs. hp (XcptRef x) = Some (Xcpt x, fs) \<Longrightarrow> P hp) \<Longrightarrow> P hp"
+ by (fast dest: preallocatedD)
+
+lemma cname_of_xcp:
+ "raise_if b x None = Some xcp \<Longrightarrow> preallocated hp
+ \<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x"
+proof -
+ assume "raise_if b x None = Some xcp"
+ hence "xcp = Addr (XcptRef x)"
+ by (simp add: raise_if_def split: split_if_asm)
+ moreover
+ assume "preallocated hp"
+ then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" ..
+ ultimately
+ show ?thesis by simp
+qed
+
+lemma preallocated_start:
+ "preallocated (start_heap G)"
+ apply (unfold preallocated_def)
+ apply (unfold start_heap_def)
+ apply (rule allI)
+ apply (case_tac x)
+ apply (auto simp add: blank_def)
+ done
+
+
+
+end
+
--- a/src/HOL/MicroJava/J/JListExample.thy Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Wed Oct 23 16:09:02 2002 +0200
@@ -62,10 +62,10 @@
cname ("string")
vnam ("string")
mname ("string")
- loc ("int")
+ loc_ ("int")
consts_code
- "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}")
+ "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}")
"arbitrary" ("(raise ERROR)")
"arbitrary" :: "val" ("{* Unit *}")
@@ -83,8 +83,8 @@
"l4_nam" ("\"l4\"")
ML {*
-fun new_addr p none hp =
- let fun nr i = if p (hp i) then (i, none) else nr (i+1);
+fun new_addr p none loc hp =
+ let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
in nr 0 end;
*}
@@ -114,14 +114,14 @@
locs l2_name;
locs l3_name;
locs l4_name;
-snd (the (heap 0)) (val_name, "list");
-snd (the (heap 0)) (next_name, "list");
-snd (the (heap 1)) (val_name, "list");
-snd (the (heap 1)) (next_name, "list");
-snd (the (heap 2)) (val_name, "list");
-snd (the (heap 2)) (next_name, "list");
-snd (the (heap 3)) (val_name, "list");
-snd (the (heap 3)) (next_name, "list");
+snd (the (heap (Loc 0))) (val_name, "list");
+snd (the (heap (Loc 0))) (next_name, "list");
+snd (the (heap (Loc 1))) (val_name, "list");
+snd (the (heap (Loc 1))) (next_name, "list");
+snd (the (heap (Loc 2))) (val_name, "list");
+snd (the (heap (Loc 2))) (next_name, "list");
+snd (the (heap (Loc 3))) (val_name, "list");
+snd (the (heap (Loc 3))) (next_name, "list");
*}
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Wed Oct 23 16:09:02 2002 +0200
@@ -11,8 +11,8 @@
declare split_beta [simp]
lemma NewC_conforms:
-"[|h a = None; (h, l)::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==>
- (h(a\<mapsto>(C,(init_vars (fields (G,C))))), l)::\<preceq>(G, lT)"
+"[|h a = None; (x,(h, l))::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==>
+ (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)
@@ -30,8 +30,10 @@
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); (h,l)::\<preceq>(G,lT);
+"[| 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 |] ==>
G,h\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\<preceq>ft"
apply( drule np_NoneD)
@@ -52,9 +54,9 @@
(G, lT)\<turnstile>aa::Class C;
field (G,C) fn = Some (fd, ft); h''\<le>|h';
x' = None --> G,h'\<turnstile>a'::\<preceq> Class C; h'\<le>|h;
- (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None|] ==>
+ Norm (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None|] ==>
h''\<le>|h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) \<and>
- (h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and>
+ Norm(h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and>
G,h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x))))\<turnstile>x::\<preceq>T'"
apply( drule np_NoneD)
apply( erule conjE)
@@ -90,6 +92,8 @@
apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD)
done
+
+
lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;
list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;
length pTs' = length pns; distinct pns;
@@ -106,17 +110,18 @@
done
lemma Call_type_sound:
- "[| wf_java_prog G; a' \<noteq> Null; (h, l)::\<preceq>(G, lT); class G C = Some y;
+ "[| wf_java_prog G; a' \<noteq> Null; Norm (h, l)::\<preceq>(G, lT); class G C = Some y;
max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\<le>|xh; xh\<le>|h;
list_all2 (conf G h) pvs pTsa;
(md, rT, pns, lvars, blk, res) =
the (method (G,fst (the (h (the_Addr a')))) (mn, pTs'));
- \<forall>lT. (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) -->
- (G, lT)\<turnstile>blk\<surd> --> h\<le>|xi \<and> (xi, xl)::\<preceq>(G, lT);
- \<forall>lT. (xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T -->
- xi\<le>|h' \<and> (h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T));
- G,xh\<turnstile>a'::\<preceq> Class C |] ==>
- xc\<le>|h' \<and> (h', l)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)"
+ \<forall>lT. (np a' None, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) -->
+ (G, lT)\<turnstile>blk\<surd> --> h\<le>|xi \<and> (xcptb, xi, xl)::\<preceq>(G, lT);
+ \<forall>lT. (xcptb,xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T -->
+ xi\<le>|h' \<and> (x',h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T));
+ G,xh\<turnstile>a'::\<preceq> Class C
+ |] ==>
+ xc\<le>|h' \<and> (x',(h', l))::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)"
apply( drule max_spec2mheads)
apply( clarify)
apply( drule (2) non_np_objD')
@@ -126,14 +131,15 @@
apply( drule (3) Call_lemma)
apply( clarsimp simp add: wf_java_mdecl_def)
apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
-apply( drule spec, erule impE)
-apply( erule_tac [2] notE impE, tactic "assume_tac 2")
+apply( drule spec, erule impE, erule_tac [2] notE impE, tactic "assume_tac 2")
apply( rule conformsI)
apply( erule conforms_heapD)
apply( rule lconf_ext)
apply( force elim!: Call_lemma2)
apply( erule conf_hext, erule (1) conf_obj_AddrI)
-apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl)
+apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl)
+apply (simp add: conforms_def)
+
apply( erule conjE)
apply( drule spec, erule (1) impE)
apply( drule spec, erule (1) impE)
@@ -149,11 +155,16 @@
apply( tactic "assume_tac 2")
prefer 2
apply( fast elim!: widen_trans)
-apply( erule conforms_hext)
+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)
done
+
+
declare split_if [split del]
declare fun_upd_apply [simp del]
declare fun_upd_same [simp]
@@ -165,17 +176,19 @@
Unify.search_bound := 40;
Unify.trace_bound := 40
*}
+
+
theorem eval_evals_exec_type_sound:
"wf_java_prog G ==>
(G\<turnstile>(x,(h,l)) -e \<succ>v -> (x', (h',l')) -->
- (\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e :: T -->
- h\<le>|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v ::\<preceq> T )))) \<and>
+ (\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e :: T -->
+ h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v ::\<preceq> T )))) \<and>
(G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) -->
- (\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts -->
- h\<le>|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and>
+ (\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts -->
+ h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None --> list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and>
(G\<turnstile>(x,(h,l)) -c -> (x', (h',l')) -->
- (\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (G,lT)\<turnstile>c \<surd> -->
- h\<le>|h' \<and> (h',l')::\<preceq>(G,lT)))"
+ (\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (G,lT)\<turnstile>c \<surd> -->
+ h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT)))"
apply( rule eval_evals_exec_induct)
apply( unfold c_hupd_def)
@@ -187,12 +200,14 @@
apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
-- "Level 7"
-
-- "15 NewC"
+apply (drule sym)
apply( drule new_AddrD)
apply( erule disjE)
prefer 2
apply( simp (no_asm_simp))
+apply (rule conforms_xcpt_change, assumption)
+apply (simp (no_asm_simp) add: xconf_def)
apply( clarsimp)
apply( rule conjI)
apply( force elim!: NewC_conforms)
@@ -216,6 +231,7 @@
apply( simp split add: binop.split)
-- "12 LAcc"
+apply simp
apply( fast elim: conforms_localD [THEN lconfD])
-- "for FAss"
@@ -234,7 +250,7 @@
apply( fast intro: hext_trans)
-- "10 Expr"
-prefer 6
+prefer 7
apply( fast)
-- "9 ???"
@@ -242,18 +258,28 @@
-- "8 Cast"
prefer 8
-apply (rule impI)
-apply (drule raise_if_NoneD)
-apply (clarsimp)
-apply (fast elim: Cast_conf)
+apply (rule conjI)
+ apply (fast intro: conforms_xcpt_change xconf_raise_if)
+
+ apply clarify
+ apply (drule raise_if_NoneD)
+ apply (clarsimp)
+ 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")
THEN_ALL_NEW Full_simp_tac) 1 *})
+apply (intro strip)
+apply (case_tac E)
+apply (simp)
apply( blast intro: conforms_upd_local conf_widen)
-- "6 FAcc"
+apply (rule conjI)
+ apply (simp add: np_def)
+ apply (fast intro: conforms_xcpt_change xconf_raise_if)
apply( fast elim!: FAcc_type_sound)
-- "5 While"
@@ -264,22 +290,34 @@
apply (tactic "forward_hyp_tac")
--- "4 Cons"
-prefer 3
+-- "4 Cond"
+prefer 4
+apply (case_tac "the_Bool v")
+apply simp
+apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
+apply simp
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
-- "3 ;;"
prefer 3
-apply( fast intro: hext_trans)
+apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
+
-- "2 FAss"
-apply( case_tac "x2 = None")
-prefer 2
-apply( simp (no_asm_simp))
-apply( fast intro: hext_trans)
-apply( simp)
-apply( drule eval_no_xcpt)
-apply( erule FAss_type_sound, rule HOL.refl, assumption+)
+apply (subgoal_tac "(np a' x1, ab, ba) ::\<preceq> (G, lT)")
+ prefer 2
+ apply (simp add: np_def)
+ apply (fast intro: conforms_xcpt_change xconf_raise_if)
+apply( case_tac "x2")
+ -- "x2 = None"
+ apply (simp)
+ apply (tactic forward_hyp_tac, clarify)
+ apply( drule eval_no_xcpt)
+ apply( erule FAss_type_sound, rule HOL.refl, assumption+)
+ -- "x2 = Some a"
+ apply ( simp (no_asm_simp))
+ apply( fast intro: hext_trans)
+
apply( tactic prune_params_tac)
-- "Level 52"
@@ -302,15 +340,21 @@
apply( simp)
apply( drule eval_xcpt)
apply( simp)
-apply( fast elim: hext_trans)
-apply( drule (1) ty_expr_is_type)
+apply (rule conjI)
+ apply( fast elim: hext_trans)
+ apply (rule conforms_xcpt_change, assumption) apply (simp (no_asm_simp) add: xconf_def)
+apply(clarsimp)
+
+apply( drule ty_expr_is_type, simp)
apply(clarsimp)
apply(unfold is_class_def)
apply(clarsimp)
+
apply(rule Call_type_sound);
prefer 11
apply blast
apply (simp (no_asm_simp))+
+
done
ML{*
Unify.search_bound := 20;
@@ -318,8 +362,8 @@
*}
lemma eval_type_sound: "!!E s s'.
- [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); s::\<preceq>E; E\<turnstile>e::T |]
- ==> s'::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)"
+ [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T |]
+ ==> (x',s')::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)"
apply( simp (no_asm_simp) only: split_tupled_all)
apply (drule eval_evals_exec_type_sound
[THEN conjunct1, THEN mp, THEN spec, THEN mp])
@@ -327,8 +371,8 @@
done
lemma exec_type_sound: "!!E s s'.
- [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); s::\<preceq>E; E\<turnstile>s0\<surd> |]
- ==> s'::\<preceq>E"
+ [| 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"
apply( simp (no_asm_simp) only: split_tupled_all)
apply (drule eval_evals_exec_type_sound
[THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp])
@@ -337,7 +381,7 @@
theorem all_methods_understood:
"[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null;
- s::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==>
+ (x,s)::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==>
method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None"
apply( drule (4) eval_type_sound)
apply(clarsimp)
--- a/src/HOL/MicroJava/J/State.thy Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/State.thy Wed Oct 23 16:09:02 2002 +0200
@@ -25,26 +25,33 @@
locals = "vname \<leadsto> val" -- "simple state, i.e. variable contents"
state = "aheap \<times> locals" -- "heap, local parameter including This"
- xstate = "xcpt option \<times> state" -- "state including exception information"
+ xstate = "val option \<times> state" -- "state including exception information"
syntax
heap :: "state => aheap"
locals :: "state => locals"
Norm :: "state => xstate"
+ abrupt :: "xstate \<Rightarrow> val option"
+ store :: "xstate \<Rightarrow> state"
+ lookup_obj :: "state \<Rightarrow> val \<Rightarrow> obj"
translations
"heap" => "fst"
"locals" => "snd"
"Norm s" == "(None,s)"
+ "abrupt" => "fst"
+ "store" => "snd"
+ "lookup_obj s a'" == "the (heap s (the_Addr a'))"
+
constdefs
- new_Addr :: "aheap => loc \<times> xcpt option"
- "new_Addr h == SOME (a,x). (h a = None \<and> x = None) | x = Some OutOfMemory"
+ raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option"
+ "raise_if b x xo \<equiv> if b \<and> (xo = None) then Some (Addr (XcptRef x)) else xo"
- raise_if :: "bool => xcpt => xcpt option => xcpt option"
- "raise_if c x xo == if c \<and> (xo = None) then Some x else xo"
+ new_Addr :: "aheap => loc \<times> val option"
+ "new_Addr h \<equiv> SOME (a,x). (h a = None \<and> x = None) | x = Some (Addr (XcptRef OutOfMemory))"
- np :: "val => xcpt option => xcpt option"
+ np :: "val => val option => val option"
"np v == raise_if (v = Null) NullPointer"
c_hupd :: "aheap => xstate => xstate"
@@ -58,17 +65,18 @@
apply (simp (no_asm))
done
-lemma new_AddrD:
-"(a,x) = new_Addr h ==> h a = None \<and> x = None | x = Some OutOfMemory"
+
+lemma new_AddrD: "new_Addr hp = (ref, xcp) \<Longrightarrow>
+ hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
+apply (drule sym)
apply (unfold new_Addr_def)
apply(simp add: Pair_fst_snd_eq Eps_split)
apply(rule someI)
apply(rule disjI2)
-apply(rule_tac "r" = "snd (?a,Some OutOfMemory)" in trans)
+apply(rule_tac "r" = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
apply auto
done
-
lemma raise_if_True [simp]: "raise_if True x y \<noteq> None"
apply (unfold raise_if_def)
apply auto
@@ -92,7 +100,7 @@
done
lemma raise_if_SomeD [rule_format (no_asm)]:
- "raise_if c x y = Some z \<longrightarrow> c \<and> Some z = Some x | y = Some z"
+ "raise_if c x y = Some z \<longrightarrow> c \<and> Some z = Some (Addr (XcptRef x)) | y = Some z"
apply (unfold raise_if_def)
apply auto
done
@@ -119,7 +127,7 @@
apply auto
done
-lemma np_Null [simp]: "np Null None = Some NullPointer"
+lemma np_Null [simp]: "np Null None = Some (Addr (XcptRef NullPointer))"
apply (unfold np_def raise_if_def)
apply auto
done
@@ -130,7 +138,7 @@
done
lemma np_raise_if [simp]: "(np Null (raise_if c xc None)) =
- Some (if c then xc else NullPointer)"
+ Some (Addr (XcptRef (if c then xc else NullPointer)))"
apply (unfold raise_if_def)
apply (simp (no_asm))
done
--- a/src/HOL/MicroJava/J/WellForm.thy Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Wed Oct 23 16:09:02 2002 +0200
@@ -170,6 +170,18 @@
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>
+\<Longrightarrow> field (G, C) =
+ (if C = Object then empty else field (G, D)) ++
+ map_of (map (\<lambda>(s, f). (s, C, f)) fs)"
+apply (simp only: field_def)
+apply (frule fields_rec, assumption)
+apply (rule HOL.trans)
+apply (simp add: o_def)
+apply (simp (no_asm_use)
+ add: split_beta split_def o_def map_compose [THEN sym] del: map_compose)
+done
+
lemma method_Object [simp]:
"method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> wf_prog wf_mb G \<Longrightarrow> D = Object"
apply (frule class_Object, clarify)
@@ -177,6 +189,19 @@
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>
+ \<Longrightarrow> C = Object"
+apply (frule class_Object)
+apply clarify
+apply (subgoal_tac "fields (G, Object) = map (\<lambda>(fn,ft). ((fn,Object),ft)) fs")
+apply (simp add: image_iff split_beta)
+apply auto
+apply (rule trans)
+apply (rule fields_rec, assumption+)
+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)
apply( assumption)
@@ -312,6 +337,19 @@
apply( fast intro: subcls1I)
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)
+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) -->
@@ -377,6 +415,55 @@
apply (simp add: override_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 fields_Object, assumption+)
+apply (simp only: is_class_Object) apply simp
+
+apply clarify
+apply (frule fields_rec)
+apply assumption
+
+apply (case_tac "Da=C")
+apply blast (* case Da=C *)
+
+apply (subgoal_tac "((vn, Da), T) \<in> set (fields (G, D))") apply blast
+apply (erule thin_rl)
+apply (rotate_tac 1)
+apply (erule thin_rl, erule thin_rl, erule thin_rl,
+ erule thin_rl, erule thin_rl, erule thin_rl)
+apply auto
+done
+
+lemma field_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk>
+ \<Longrightarrow> \<forall> vn D T. (field (G,C) vn = Some(D,T)
+ \<longrightarrow> is_class G D \<and> field (G,D) vn = Some(D,T))"
+apply (erule (1) subcls1_induct)
+
+apply clarify
+apply (frule field_fields)
+apply (drule map_of_SomeD)
+apply (drule fields_Object, assumption+)
+apply simp
+
+apply clarify
+apply (subgoal_tac "((field (G, D)) ++ map_of (map (\<lambda>(s, f). (s, C, f)) fs)) vn = Some (Da, T)")
+apply (simp (no_asm_use) only: override_Some_iff)
+apply (erule disjE)
+apply (simp (no_asm_use) add: map_of_map) apply blast
+apply blast
+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_use)) apply blast
+done
+
+
lemma widen_methd:
"[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\<turnstile>T''\<preceq>C C|]
==> \<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
@@ -384,6 +471,15 @@
apply auto
done
+lemma widen_field: "\<lbrakk> (field (G,C) fn) = Some (fd, fT); wf_prog wf_mb G; is_class G C \<rbrakk>
+ \<Longrightarrow> G\<turnstile>C\<preceq>C fd"
+apply (rule widen_fields_defpl)
+apply (simp add: field_def)
+apply (rule map_of_SomeD)
+apply (rule table_of_remap_SomeD)
+apply assumption+
+done
+
lemma Call_lemma:
"[|method (G,C) sig = Some (md,rT,b); G\<turnstile>T''\<preceq>C C; wf_prog wf_mb G;
class G C = Some y|] ==> \<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \<and>
--- a/src/HOL/MicroJava/J/WellType.thy Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Wed Oct 23 16:09:02 2002 +0200
@@ -96,15 +96,21 @@
apply auto
done
+lemma typeof_default_val: "\<exists>T. (typeof dt (default_val ty) = Some T) \<and> G\<turnstile> T \<preceq> ty"
+apply (case_tac ty)
+apply (case_tac prim_ty)
+apply auto
+done
+
types
java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
-- "method body with parameter names, local variables, block, result expression."
-- "local variables might include This, which is hidden anyway"
consts
- ty_expr :: "java_mb env => (expr \<times> ty ) set"
- ty_exprs:: "java_mb env => (expr list \<times> ty list) set"
- wt_stmt :: "java_mb env => stmt set"
+ 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"
syntax (xsymbols)
ty_expr :: "java_mb env => [expr , ty ] => bool" ("_ \<turnstile> _ :: _" [51,51,51]50)
@@ -118,11 +124,11 @@
translations
- "E\<turnstile>e :: T" == "(e,T) \<in> ty_expr E"
- "E\<turnstile>e[::]T" == "(e,T) \<in> ty_exprs E"
- "E\<turnstile>c \<surd>" == "c \<in> wt_stmt E"
+ "E\<turnstile>e :: T" == "(E,e,T) \<in> ty_expr"
+ "E\<turnstile>e[::]T" == "(E,e,T) \<in> ty_exprs"
+ "E\<turnstile>c \<surd>" == "(E,c) \<in> wt_stmt"
-inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intros
+inductive "ty_expr" "ty_exprs" "wt_stmt" intros
NewC: "[| is_class (prg E) C |] ==>
E\<turnstile>NewC C::Class C" -- "cf. 15.8"
@@ -150,7 +156,7 @@
-- "cf. 15.25, 15.25.1"
LAss: "[| v ~= This;
E\<turnstile>LAcc v::T;
- E\<turnstile>e::T';
+ E\<turnstile>e::T';
prg E\<turnstile>T'\<preceq>T |] ==>
E\<turnstile>v::=e::T'"
@@ -204,6 +210,7 @@
E\<turnstile>s\<surd> |] ==>
E\<turnstile>While(e) s\<surd>"
+
constdefs
wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool"
@@ -222,9 +229,22 @@
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 (erule conjE)+
+apply (drule bspec, assumption)
+apply simp
+apply (erule conjE)+
+apply (drule bspec, assumption)
+apply (simp add: wf_mdecl_def split_beta)
+done
-lemma wt_is_type: "wf_prog wf_mb G \<Longrightarrow> ((G,L)\<turnstile>e::T \<longrightarrow> is_type G T) \<and>
- ((G,L)\<turnstile>es[::]Ts \<longrightarrow> Ball (set Ts) (is_type G)) \<and> ((G,L)\<turnstile>c \<surd> \<longrightarrow> True)"
+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>
+ (E\<turnstile>c \<surd> \<longrightarrow> True)"
apply (rule ty_expr_ty_exprs_wt_stmt.induct)
apply auto
apply ( erule typeof_empty_is_type)
@@ -237,6 +257,6 @@
simp add: wf_mdecl_def)
done
-lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, COMP swap_prems_rl]
+lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, rule_format]
end
--- a/src/HOL/MicroJava/ROOT.ML Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/ROOT.ML Wed Oct 23 16:09:02 2002 +0200
@@ -3,6 +3,7 @@
add_path "J";
add_path "JVM";
add_path "BV";
+add_path "Comp";
no_document use_thy "While_Combinator";
@@ -14,3 +15,6 @@
use_thy "LBVJVM";
use_thy "BVNoTypeError";
use_thy "BVExample";
+
+use_thy "CorrComp";
+use_thy "CorrCompTp";