(* Title: HOL/MicroJava/J/TypeRel.thy ID: $Id$ Author: David von Oheimb Copyright 1999 Technische Universitaet Muenchen The relations between Java types *) theory TypeRel = Decl: consts subcls1 :: "'c prog => (cname \ cname) set" (* subclass *) widen :: "'c prog => (ty \ ty ) set" (* widening *) cast :: "'c prog => (cname \ cname) set" (* casting *) 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) syntax (HTML) 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) translations "G\C \C1 D" == "(C,D) \ subcls1 G" "G\C \C D" == "(C,D) \ (subcls1 G)^*" "G\S \ T" == "(S,T) \ widen G" "G\C \? D" == "(C,D) \ cast G" defs (* direct subclass, cf. 8.1.3 *) subcls1_def: "subcls1 G \ {(C,D). C\Object \ (\c. class G C=Some c \ fst c=D)}" lemma subcls1D: "G\C\C1D \ C \ Object \ (\fs ms. class G C = Some (D,fs,ms))" apply (unfold subcls1_def) apply auto done lemma subcls1I: "\class G C = Some (D,rest); C \ Object\ \ G\C\C1D" apply (unfold subcls1_def) apply auto done lemma subcls1_def2: "subcls1 G = (\C\{C. is_class G C} . {D. C\Object \ fst (the (class G C))=D})" apply (unfold subcls1_def is_class_def) apply auto done lemma finite_subcls1: "finite (subcls1 G)" apply(subst subcls1_def2) apply(rule finite_SigmaI [OF finite_is_class]) apply(rule_tac B = "{fst (the (class G C))}" in finite_subset) apply auto done lemma subcls_is_class: "(C,D) \ (subcls1 G)^+ ==> is_class G C" apply (unfold is_class_def) apply(erule trancl_trans_induct) apply (auto dest!: subcls1D) done lemma subcls_is_class2 [rule_format (no_asm)]: "G\C\C D \ is_class G D \ is_class G C" apply (unfold is_class_def) apply (erule rtrancl_induct) apply (drule_tac [2] subcls1D) apply auto done consts class_rec ::"'c prog \ cname \ 'a \ (cname \ fdecl list \ 'c mdecl list \ 'a \ 'a) \ 'a" recdef class_rec "same_fst (\G. wf ((subcls1 G)^-1)) (\G. (subcls1 G)^-1)" "class_rec (G,C) = (\t f. case class G C of None \ arbitrary | Some (D,fs,ms) \ if wf ((subcls1 G)^-1) then f C fs ms (if C = Object then t else class_rec (G,D) t f) else arbitrary)" recdef_tc class_rec_tc: class_rec apply (unfold same_fst_def) apply (auto intro: subcls1I) done lemma class_rec_lemma: "\ wf ((subcls1 G)^-1); class G C = Some (D,fs,ms)\ \ class_rec (G,C) t f = f C fs ms (if C=Object then t else class_rec (G,D) t f)"; apply (rule class_rec_tc [THEN class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]]]) apply (rule ext, rule ext) apply auto done consts method :: "'c prog \ cname => ( sig \ cname \ ty \ 'c)" (* ###curry *) field :: "'c prog \ cname => ( vname \ cname \ ty )" (* ###curry *) fields :: "'c prog \ cname => ((vname \ cname) \ ty) list" (* ###curry *) (* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *) defs method_def: "method \ \(G,C). class_rec (G,C) empty (\C fs ms ts. ts ++ map_of (map (\(s,m). (s,(C,m))) ms))" lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==> method (G,C) = (if C = Object then empty else method (G,D)) ++ map_of (map (\(s,m). (s,(C,m))) ms)" apply (unfold method_def) apply (simp split del: split_if) apply (erule (1) class_rec_lemma [THEN trans]); apply auto done (* list of fields of a class, including inherited and hidden ones *) defs fields_def: "fields \ \(G,C). class_rec (G,C) [] (\C fs ms ts. map (\(fn,ft). ((fn,C),ft)) fs @ ts)" lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==> fields (G,C) = map (\(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))" apply (unfold fields_def) apply (simp split del: split_if) apply (erule (1) class_rec_lemma [THEN trans]); apply auto done defs field_def: "field == map_of o (map (\((fn,fd),ft). (fn,(fd,ft)))) o fields" lemma field_fields: "field (G,C) fn = Some (fd, fT) \ map_of (fields (G,C)) (fn, fd) = Some fT" apply (unfold field_def) apply (rule table_of_remap_SomeD) apply simp done inductive "widen G" intros (*widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping *) refl [intro!, simp]: "G\ T \ T" (* identity conv., cf. 5.1.1 *) subcls : "G\C\C D ==> G\Class C \ Class D" null [intro!]: "G\ NT \ RefT R" inductive "cast G" intros (* casting conversion, cf. 5.5 / 5.1.5 *) (* left out casts on primitve types *) widen: "G\C\C D ==> G\C \? D" subcls: "G\D\C C ==> G\C \? D" lemma widen_PrimT_RefT [iff]: "(G\PrimT pT\RefT rT) = False" apply (rule iffI) apply (erule widen.elims) apply auto done lemma widen_RefT: "G\RefT R\T ==> \t. T=RefT t" apply (ind_cases "G\S\T") apply auto done lemma widen_RefT2: "G\S\RefT R ==> \t. S=RefT t" apply (ind_cases "G\S\T") apply auto done lemma widen_Class: "G\Class C\T ==> \D. T=Class D" apply (ind_cases "G\S\T") apply auto done lemma widen_Class_NullT [iff]: "(G\Class C\NT) = False" apply (rule iffI) apply (ind_cases "G\S\T") apply auto done lemma widen_Class_Class [iff]: "(G\Class C\ Class D) = (G\C\C D)" apply (rule iffI) apply (ind_cases "G\S\T") apply (auto elim: widen.subcls) done lemma widen_trans [rule_format (no_asm)]: "G\S\U ==> \T. G\U\T --> G\S\T" apply (erule widen.induct) apply safe apply (frule widen_Class) apply (frule_tac [2] widen_RefT) apply safe apply(erule (1) rtrancl_trans) done ML {* InductAttrib.print_global_rules(the_context()) *} ML {* set show_tags *} (*####theorem widen_trans: "\G\S\U; G\U\T\ \ G\S\T" proof - assume "G\S\U" thus "\T. G\U\T \ G\S\T" (*(is "PROP ?P S U")*) proof (induct (*cases*) (open) (*?P S U*) rule: widen.induct [consumes 1]) case refl fix T' assume "G\T\T'" thus "G\T\T'". (* fix T' show "PROP ?P T T".*) next case subcls fix T assume "G\Class D\T" then obtain E where "T = Class E" by (blast dest: widen_Class) from prems show "G\Class C\T" proof (auto elim: rtrancl_trans) qed next case null fix RT assume "G\RefT R\RT" then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT) thus "G\NT\RT" by auto qed qed *) theorem widen_trans: "\G\S\U; G\U\T\ \ G\S\T" proof - assume "G\S\U" thus "\T. G\U\T \ G\S\T" (*(is "PROP ?P S U")*) proof (induct (*cases*) (open) (*?P S U*)) (* rule: widen.induct *) case refl fix T' assume "G\T\T'" thus "G\T\T'". (* fix T' show "PROP ?P T T".*) next case subcls fix T assume "G\Class D\T" then obtain E where "T = Class E" by (blast dest: widen_Class) from prems show "G\Class C\T" proof (auto elim: rtrancl_trans) qed next case null fix RT assume "G\RefT R\RT" then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT) thus "G\NT\RT" by auto qed qed end