# HG changeset patch # User kleing # Date 979492657 -3600 # Node ID 23386a5b63eb12022cbe6fe4027503ef989b48e3 # Parent 79194f07d3568ca23b3808fc9689232c9a6b0c5e tuned diff -r 79194f07d356 -r 23386a5b63eb src/HOL/MicroJava/BV/JType.thy --- a/src/HOL/MicroJava/BV/JType.thy Sun Jan 14 14:12:42 2001 +0100 +++ b/src/HOL/MicroJava/BV/JType.thy Sun Jan 14 18:17:37 2001 +0100 @@ -160,22 +160,15 @@ done -lemma err_semilat_JType_esl_lemma: - "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] - ==> err_semilat (esl G)" +lemma sup_subtype_greater: + "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G); + is_type G t1; is_type G t2; sup G t1 t2 = OK s |] + ==> subtype G t1 s \ subtype G t2 s" proof - - assume wf_prog: "wf_prog wf_mb G" + assume wf_prog: "wf_prog wf_mb 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 - have "closed (err (types G)) (lift2 (sup G))" - by (rule closed_err_types) - moreover - + assume acyclic: "acyclic (subcls1 G)" + { fix c1 c2 assume is_class: "is_class G c1" "is_class G c2" with wf_prog @@ -185,53 +178,31 @@ by (blast intro: subcls_C_Object) with wf_prog single_valued obtain u where - "is_lub ((subcls1 G)^* ) c1 c2 u" + "is_lub ((subcls1 G)^* ) c1 c2 u" by (blast dest: single_valued_has_lubs) with acyclic - have "G \ c1 \C some_lub ((subcls1 G)^* ) c1 c2" + have "G \ c1 \C some_lub ((subcls1 G)^* ) c1 c2 \ + G \ c2 \C some_lub ((subcls1 G)^* ) c1 c2" by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD) - } note this [intro] + } note this [simp] - { fix t1 t2 s - assume "is_type G t1" "is_type G t2" "sup G t1 t2 = OK s" - hence "subtype G t1 s" - by (unfold sup_def subtype_def) - (cases s, auto intro: widen.null - split: ty.splits ref_ty.splits if_splits) - } note this [intro] - - have - "\x\err (types G). \y\err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y" - by (auto simp add: lesub_def plussub_def le_def lift2_def split: err.split) - - moreover + assume "is_type G t1" "is_type G t2" "sup G t1 t2 = OK s" + thus ?thesis + apply (unfold sup_def subtype_def) + apply (cases s) + apply (auto split: ty.split_asm ref_ty.split_asm split_if_asm) + done +qed - { fix c1 c2 - assume "is_class G c1" "is_class G c2" - with wf_prog - obtain - "G \ c1 \C Object" - "G \ c2 \C Object" - by (blast intro: subcls_C_Object) - with wf_prog single_valued - obtain u where - "is_lub ((subcls1 G)^* ) c2 c1 u" - by (blast dest: single_valued_has_lubs) - with acyclic - have "G \ c1 \C some_lub ((subcls1 G)^* ) c2 c1" - by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD) - } note this [intro] - - have "\x\err (types G). \y\err (types G). - y <=_(le (subtype G)) x +_(lift2 (sup G)) y" - by (auto simp add: lesub_def plussub_def le_def sup_def subtype_def lift2_def - split: err.split ty.splits ref_ty.splits if_splits intro: widen.null) - moreover - - have [intro]: - "!!a b c. [| G \ a \ c; G \ b \ c; sup G a b = Err |] ==> False" - by (auto simp add: PrimT_PrimT PrimT_PrimT2 sup_def - split: ty.splits ref_ty.splits) +lemma sup_subtype_smallest: + "[| wf_prog wf_mb 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 |] + ==> subtype G d c" +proof - + assume wf_prog: "wf_prog wf_mb 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" @@ -261,18 +232,48 @@ "!!C T. G \ Class C \ T ==> \D. T=Class D \ G \ C \C D" by (frule widen_Class, auto) - { fix a b c d - assume "is_type G a" "is_type G b" "is_type G c" and - "G \ a \ c" "G \ b \ c" and - "sup G a b = OK d" - hence "G \ d \ c" - by (auto simp add: sup_def split: ty.splits ref_ty.splits if_splits) - } note this [intro] + assume "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" + thus ?thesis + by (auto simp add: subtype_def sup_def + split: ty.split_asm ref_ty.split_asm split_if_asm) +qed + +lemma sup_exists: + "[| subtype G a c; subtype G b c; sup G a b = Err |] ==> False" + by (auto simp add: PrimT_PrimT PrimT_PrimT2 sup_def subtype_def + split: ty.splits ref_ty.splits) +lemma err_semilat_JType_esl_lemma: + "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] + ==> err_semilat (esl G)" +proof - + assume wf_prog: "wf_prog wf_mb 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 + have "closed (err (types G)) (lift2 (sup G))" + by (rule closed_err_types) + moreover + + from wf_prog single_valued acyclic + have + "(\x\err (types G). \y\err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \ + (\x\err (types G). \y\err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)" + by (auto simp add: lesub_def plussub_def le_def lift2_def sup_subtype_greater split: err.split) + + moreover + + from wf_prog single_valued acyclic have "\x\err (types G). \y\err (types G). \z\err (types G). x <=_(le (subtype G)) z \ y <=_(le (subtype G)) z \ x +_(lift2 (sup G)) y <=_(le (subtype G)) z" - by (simp add: lift2_def plussub_def lesub_def subtype_def le_def split: err.splits) blast + by (unfold lift2_def plussub_def lesub_def le_def) + (auto intro: sup_subtype_smallest sup_exists split: err.split) ultimately