# HG changeset patch # User kleing # Date 974734885 -3600 # Node ID 7c6985b4de40d9b55d50e585544956a6a59039d3 # Parent f2d304bdf3ccbc391cd007d6160e1de16aaa982f BCV integration (type system is semilattice) diff -r f2d304bdf3cc -r 7c6985b4de40 src/HOL/MicroJava/BV/JType.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/MicroJava/BV/JType.thy Mon Nov 20 16:41:25 2000 +0100 @@ -0,0 +1,240 @@ +(* Title: HOL/BCV/JType.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 2000 TUM + +The type system of the JVM +*) + +header "JVM Type System as Semilattice" + +theory JType = WellForm + Err: + +constdefs + is_ref :: "ty => bool" + "is_ref T == case T of PrimT t => False | RefT r => True" + + sup :: "'c prog => ty => ty => ty err" + "sup G T1 T2 == + case T1 of PrimT P1 => (case T2 of PrimT P2 => (if P1 = P2 then OK (PrimT P1) else Err) | RefT R => Err) + | RefT R1 => (case T2 of PrimT P => Err | RefT R2 => + (case R1 of NullT => (case R2 of NullT => OK NT | ClassT C => OK (Class C)) + | ClassT C => (case R2 of NullT => OK (Class C) + | ClassT D => OK (Class (some_lub ((subcls1 G)^* ) C D)))))" + + subtype :: "'c prog => ty => ty => bool" + "subtype G T1 T2 == G \ T1 \ T2" + + is_ty :: "'c prog => ty => bool" + "is_ty G T == case T of PrimT P => True | RefT R => + (case R of NullT => True | ClassT C => (C,Object):(subcls1 G)^*)" + +translations + "types G" == "Collect (is_type G)" + +constdefs + esl :: "'c prog => ty esl" + "esl G == (types G, subtype G, sup G)" + +lemma PrimT_PrimT: "(G \ xb \ PrimT p) = (xb = PrimT p)" + by (auto elim: widen.elims) + +lemma PrimT_PrimT2: "(G \ PrimT p \ xb) = (xb = PrimT p)" + by (auto elim: widen.elims) + +lemma is_tyI: + "[| is_type G T; wf_prog wf_mb G |] ==> is_ty G T" + by (auto simp add: is_ty_def dest: subcls_C_Object + split: ty.splits ref_ty.splits) + +lemma is_type_conv: + "wf_prog wf_mb G ==> is_type G T = is_ty G T" +proof + assume "is_type G T" "wf_prog wf_mb G" + thus "is_ty G T" + by (rule is_tyI) +next + assume wf: "wf_prog wf_mb G" and + ty: "is_ty G T" + + show "is_type G T" + proof (cases T) + case PrimT + thus ?thesis by simp + next + fix R assume R: "T = RefT R" + with wf + have "R = ClassT Object \ ?thesis" by simp + moreover + from R wf ty + have "R \ ClassT Object \ ?thesis" + by (auto simp add: is_ty_def subcls1_def is_class_def class_def + elim: converse_rtranclE + split: ref_ty.splits) + ultimately + show ?thesis by blast + qed +qed + + +lemma order_widen: + "acyclic (subcls1 G) ==> order (subtype G)" + apply (unfold order_def lesub_def subtype_def) + apply (auto intro: widen_trans) + apply (case_tac x) + apply (case_tac y) + apply (auto simp add: PrimT_PrimT) + apply (case_tac y) + apply simp + apply simp + apply (case_tac ref_ty) + apply (case_tac ref_tya) + apply simp + apply simp + apply (case_tac ref_tya) + apply simp + apply simp + apply (auto dest: acyclic_impl_antisym_rtrancl antisymD) + done + +lemma closed_err_types: + "[| wf_prog wf_mb G; univalent (subcls1 G); acyclic (subcls1 G) |] + ==> closed (err (types G)) (lift2 (sup G))" + apply (unfold closed_def plussub_def lift2_def sup_def) + apply (auto split: err.split) + apply (drule is_tyI, assumption) + apply (auto simp add: is_ty_def is_type_conv simp del: is_type.simps + split: ty.split ref_ty.split) + apply (blast dest!: is_lub_some_lub is_lubD is_ubD intro!: is_ubI) + done + + +lemma err_semilat_JType_esl_lemma: + "[| wf_prog wf_mb G; univalent (subcls1 G); acyclic (subcls1 G) |] + ==> err_semilat (esl G)" +proof - + assume wf_prog: "wf_prog wf_mb G" + assume univalent: "univalent (subcls1 G)" + assume acyclic: "acyclic (subcls1 G)" + + hence "order (subtype G)" + by (rule order_widen) + moreover + from wf_prog univalent acyclic + have "closed (err (types G)) (lift2 (sup G))" + by (rule closed_err_types) + moreover + + { fix c1 c2 + assume is_class: "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 univalent + obtain u where + "is_lub ((subcls1 G)^* ) c1 c2 u" + by (blast dest: univalent_has_lubs) + with acyclic + have "G \ c1 \C some_lub ((subcls1 G)^* ) c1 c2" + by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD) + } note this [intro] + + { 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 + + { 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 univalent + obtain u where + "is_lub ((subcls1 G)^* ) c2 c1 u" + by (blast dest: univalent_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) + + { fix c1 c2 D + assume is_class: "is_class G c1" "is_class G c2" + assume le: "G \ c1 \C D" "G \ c2 \C D" + from wf_prog is_class + obtain + "G \ c1 \C Object" + "G \ c2 \C Object" + by (blast intro: subcls_C_Object) + with wf_prog univalent + obtain u where + lub: "is_lub ((subcls1 G)^* ) c1 c2 u" + by (blast dest: univalent_has_lubs) + with acyclic + have "some_lub ((subcls1 G)^* ) c1 c2 = u" + by (rule some_lub_conv) + moreover + from lub le + have "G \ u \C D" + by (simp add: is_lub_def is_ub_def) + ultimately + have "G \ some_lub ((subcls1 G)\<^sup>*) c1 c2 \C D" + by blast + } note this [intro] + + have [dest!]: + "!!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] + + 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 + + ultimately + + show ?thesis + by (unfold esl_def semilat_def sl_def) auto +qed + +lemma univalent_subcls1: + "wf_prog wf_mb G ==> univalent (subcls1 G)" + by (unfold wf_prog_def unique_def univalent_def subcls1_def) auto + +ML_setup {* bind_thm ("acyclic_subcls1", acyclic_subcls1) *} + +theorem "wf_prog wf_mb G ==> err_semilat (esl G)" + by (frule acyclic_subcls1, frule univalent_subcls1, rule err_semilat_JType_esl_lemma) + +end