Up to index of Isabelle/Bali5
theory Decl = Term + Table:(* Title: isabelle/Bali/Decl.thy
ID: $Id: Decl.thy,v 1.43 2001/05/11 14:41:56 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Field, method, interface, and class declarations, whole Java programs
simplifications:
* the only field and method modifier is static
* no constructors, which may be simulated by new + suitable methods
* there is just one global initializer per class, which can simulate all others
* no throws clause
* result statement replaced by result expression (evaluated at the end of the
execution of the body; transformation is always possible (with goto, while)
* a void method is replaced by one that returns Unit (of dummy type Void)
* no interface modifiers yet, i.e. every interface is public
* no interface fields
* no class modifiers yet, i.e. every class is public, non-final
* every class has an explicit superclass (unused for Object)
* the (standard) methods of Object and of standard exceptions are not specified
* no packages
* no main method
*)
(** order is significant, because of clash for "var" **)
theory Decl = Term + Table:
types modi = bool (* modifier: static *)
field
= "modi × ty"
fdecl (* field declaration, cf. 8.3 *)
= "ename × field"
translations
"field" <= (type) "bool × ty"
"fdecl" <= (type) "ename × field"
types (*sig: see Term.thy *)
mhead (* method head (excluding signature) *)
= "modi × ename list × ty"
(* modifier, parameter names, result type *)
mbody (* method body *)
= "(ename × ty) list × stmt × expr"
(* local variables, block+result expression *)
methd (* method in a class *)
= "mhead × mbody"
mdecl (* method declaration in a class *)
= "sig × methd"
translations
"mhead" <= (type) "bool × ename list × ty"
"mbody" <= (type) "(ename × ty) list × stmt × expr"
"methd" <= (type) "mhead × mbody"
"mdecl" <= (type) "sig × methd"
syntax
static :: "modi \<Rightarrow> bool"
mrt :: "mhead \<Rightarrow> ty"
translations
"static" => "id"
"mrt mh" => "snd (snd mh)"
types ibody (* interface body *)
= "(sig × mhead) list"
(* methods *)
iface (* interface *)
= "tname list × ibody"
(* superinterface list *)
idecl (* interface declaration, cf. 9.1 *)
= "tname × iface"
translations
"ibody" <= (type) "(sig × mhead) list"
"iface" <= (type) "tname list × ibody"
"idecl" <= (type) "tname × iface"
types cbody (* class body *)
= "fdecl list × mdecl list × stmt"
(* fields, methods, initializer *)
class (* class *)
= "tname × tname list × cbody"
(* superclass, implemented interfaces *)
cdecl (* class declaration, cf. 8.1 *)
= "tname × class"
translations
"cbody" <= (type) "fdecl list × mdecl list × stmt"
"class" <= (type) "tname × tname list × cbody"
"cdecl" <= (type) "tname × class"
section "standard classes"
consts
Object_mdecls :: "mdecl list" (* methods of Object *)
SXcpt_mdecls :: "mdecl list" (* methods of SXcpts *)
ObjectC :: "cdecl" (* declaration of root class *)
SXcptC ::"xname \<Rightarrow> cdecl" (* declarations of throwable classes *)
defs
ObjectC_def: "ObjectC \<equiv> (Object , (arbitrary ,[],[],Object_mdecls,Skip))"
SXcptC_def: "SXcptC xn\<equiv> (SXcpt xn, (if xn = Throwable then Object else
SXcpt Throwable,[],[],SXcpt_mdecls,Skip))"
lemma ObjectC_neq_SXcptC [simp]: "ObjectC \<noteq> SXcptC xn"
by (simp add: ObjectC_def SXcptC_def)
lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
apply (simp add: SXcptC_def)
apply auto
done
constdefs standard_classes :: "cdecl list"
"standard_classes \<equiv> [ObjectC, SXcptC Throwable,
SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
section "programs"
types prog = "idecl list × cdecl list"
translations
"prog"<= (type) "idecl list × cdecl list"
syntax
iface :: "prog \<Rightarrow> (tname, iface) table"
class :: "prog \<Rightarrow> (tname, class) table"
is_iface :: "prog \<Rightarrow> tname \<Rightarrow> bool"
is_class :: "prog \<Rightarrow> tname \<Rightarrow> bool"
translations
"iface G I" == "table_of (fst G) I"
"class G C" == "table_of (snd G) C"
"is_iface G I" == "iface G I \<noteq> None"
"is_class G C" == "class G C \<noteq> None"
section "is_type"
consts
is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
primrec "is_type G (PrimT pt) = True"
"is_type G (RefT rt) = isrtype G rt"
"isrtype G (NullT ) = True"
"isrtype G (IfaceT tn) = is_iface G tn"
"isrtype G (ClassT tn) = is_class G tn"
"isrtype G (ArrayT T ) = is_type G T"
lemma type_is_iface: "is_type G (Iface I) \<Longrightarrow> is_iface G I"
by auto
lemma type_is_class: "is_type G (Class C) \<Longrightarrow> is_class G C"
by auto
section "subinterface and subclass relation, in anticipation of TypeRel.thy"
consts
subint1 :: "prog \<Rightarrow> (tname × tname) set"
subcls1 :: "prog \<Rightarrow> (tname × tname) set"
defs
subint1_def: "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (fst i)}"
subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: fst c = D)}"
lemma subint1I: "\<lbrakk>iface G I = Some (si,ms); J \<in> set si\<rbrakk> \<Longrightarrow> (I,J) \<in> subint1 G"
apply (simp add: subint1_def)
done
lemma subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> (C,D) \<in> subcls1 G"
apply (simp add: subcls1_def)
done
lemma subint1D: "(I,J)\<in>subint1 G\<Longrightarrow> \<exists>(si,ms)\<in>iface G I: J\<in>set si"
apply (simp add: subint1_def)
apply auto
done
lemma subcls1D: "(C,D)\<in>subcls1 G \<Longrightarrow> C\<noteq>Object \<and> (\<exists>cb. class G C = Some (D,cb))"
apply (simp add: subcls1_def)
apply auto
done
lemma subint1_def2:
"subint1 G = (\<Sigma> I\<in>{I. is_iface G I}. set (fst (the (iface G I))))"
apply (unfold subint1_def)
apply auto
done
lemma subcls1_def2:
"subcls1 G = (\<Sigma>C\<in>{C. is_class G C}. {D. C\<noteq>Object \<and> fst(the(class G C))=D})"
apply (unfold subcls1_def)
apply auto
done
section "well-structured programs"
constdefs
ws_idecl :: "prog \<Rightarrow> tname \<Rightarrow> tname list \<Rightarrow> bool"
"ws_idecl G I si \<equiv> \<forall>J\<in>set si. is_iface G J \<and> (J,I)\<notin>(subint1 G)^+"
ws_cdecl :: "prog \<Rightarrow> tname \<Rightarrow> tname \<Rightarrow> bool"
"ws_cdecl G C sc \<equiv> C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+"
ws_prog :: "prog \<Rightarrow> bool"
"ws_prog G \<equiv> (\<forall>(I,(si,ib))\<in>set (fst G). ws_idecl G I si) \<and>
(\<forall>(C,(sc,cb))\<in>set (snd G). ws_cdecl G C sc)"
lemma ws_progI:
"\<lbrakk>\<forall>(I,si,ib)\<in>set (fst G). \<forall>J\<in>set si. is_iface G J \<and> (J,I) \<notin> (subint1 G)^+;
\<forall>(C,D ,cb)\<in>set (snd G). C\<noteq>Object \<longrightarrow> is_class G D \<and> (D,C) \<notin> (subcls1 G)^+
\<rbrakk> \<Longrightarrow> ws_prog G"
apply (unfold ws_prog_def ws_idecl_def ws_cdecl_def)
apply (erule_tac conjI)
apply blast
done
lemma ws_prog_ideclD:
"\<lbrakk>iface G I = Some (si,ib); J\<in>set si; ws_prog G\<rbrakk> \<Longrightarrow>
is_iface G J \<and> (J,I)\<notin>(subint1 G)^+"
apply (unfold ws_prog_def ws_idecl_def)
apply clarify
apply (drule_tac map_of_SomeD)
apply auto
done
lemma ws_prog_cdeclD:
"\<lbrakk>class G C = Some(sc,cb); C\<noteq>Object; ws_prog G\<rbrakk> \<Longrightarrow>
is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+"apply (unfold ws_prog_def ws_cdecl_def)
apply clarify
apply (drule_tac map_of_SomeD)
apply auto
done
section "well-foundedness"
lemma finite_is_iface: "finite {I. is_iface G I}"
apply (fold dom_def)
apply (rule_tac finite_dom_map_of)
done
lemma finite_is_class: "finite {C. is_class G C}"
apply (fold dom_def)
apply (rule_tac finite_dom_map_of)
done
lemma finite_subint1: "finite (subint1 G)"
apply (subst subint1_def2)
apply (rule finite_SigmaI)
apply (rule finite_is_iface)
apply (simp (no_asm))
done
lemma finite_subcls1: "finite (subcls1 G)"
apply (subst subcls1_def2)
apply (rule finite_SigmaI)
apply (rule finite_is_class)
apply (rule_tac B = "{fst (the (class G C))}" in finite_subset)
apply auto
done
lemma subint1_irrefl_lemma1: "ws_prog G \<Longrightarrow> (subint1 G)^-1 \<inter> (subint1 G)^+ = {}"
apply (force dest: subint1D ws_prog_ideclD conjunct2)
done
lemma subcls1_irrefl_lemma1: "ws_prog G \<Longrightarrow> (subcls1 G)^-1 \<inter> (subcls1 G)^+ = {}"
apply (force dest: subcls1D ws_prog_cdeclD conjunct2)
done
lemmas subint1_irrefl_lemma2 = subint1_irrefl_lemma1 [THEN irrefl_tranclI']
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
lemma subint1_irrefl: "\<lbrakk>(x, y) \<in> subint1 G; ws_prog G\<rbrakk> \<Longrightarrow> x \<noteq> y"
apply (rule irrefl_trancl_rD)
apply (rule subint1_irrefl_lemma2)
apply auto
done
lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1 G; ws_prog G\<rbrakk> \<Longrightarrow> x \<noteq> y"
apply (rule irrefl_trancl_rD)
apply (rule subcls1_irrefl_lemma2)
apply auto
done
lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI, standard]
lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
lemma wf_subint1: "ws_prog G \<Longrightarrow> wf ((subint1 G)¯)"
by (auto intro: finite_acyclic_wf_converse finite_subint1 subint1_acyclic)
lemma wf_subcls1: "ws_prog G \<Longrightarrow> wf ((subcls1 G)¯)"
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
lemma subint1_induct:
"\<lbrakk>ws_prog G; \<And>x. \<forall>y. (x, y) \<in> subint1 G \<longrightarrow> P y \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P a"
apply (frule wf_subint1)
apply (erule wf_induct)
apply (simp (no_asm_use) only: converse_iff)
apply blast
done
lemma subcls1_induct:
"\<lbrakk>ws_prog G; \<And>x. \<forall>y. (x, y) \<in> subcls1 G \<longrightarrow> P y \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P a"
apply (frule wf_subcls1)
apply (erule wf_induct)
apply (simp (no_asm_use) only: converse_iff)
apply blast
done
lemma ws_subint1_induct: "\<lbrakk>is_iface G I; ws_prog G;
\<And>I is ms. \<lbrakk>iface G I = Some (is, ms) \<and>
(\<forall>J \<in> set is. (I,J)\<in>subint1 G \<and> P J \<and> is_iface G J)\<rbrakk> \<Longrightarrow> P I\<rbrakk> \<Longrightarrow> P I"
apply (cut_tac)
apply (erule make_imp)
apply (rule subint1_induct)
apply assumption
apply safe
apply (fast dest: subint1I ws_prog_ideclD)
done
lemma ws_subcls1_induct: "\<lbrakk>is_class G C; ws_prog G;
\<And>C D si fs ms ini. \<lbrakk>class G C = Some (D,si,fs,ms,ini) \<and>
(C \<noteq> Object \<longrightarrow> (C,D)\<in>subcls1 G \<and> P D \<and> is_class G D)\<rbrakk> \<Longrightarrow> P C
\<rbrakk> \<Longrightarrow> P C"
apply (cut_tac)
apply (erule make_imp)
apply (rule subcls1_induct)
apply assumption
apply safe
apply (fast dest: subcls1I ws_prog_cdeclD)
done
section "general recursion operators for the interface and class hiearchies"
consts
iface_rec :: "prog × tname \<Rightarrow> (tname \<Rightarrow> ibody \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
class_rec :: "prog × tname \<Rightarrow> 'a \<Rightarrow> (tname \<Rightarrow> cbody \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
recdef iface_rec "same_fst ws_prog (\<lambda>G. (subint1 G)^-1)"
"iface_rec (G,I) = (\<lambda>f. case iface G I of None \<Rightarrow> arbitrary | Some (si,ib) \<Rightarrow>
if ws_prog G then f I ib ((\<lambda>J. iface_rec (G,J) f)`set si)
else arbitrary)"
(hints recdef_wf: wf_subint1 intro: subint1I)
declare iface_rec.simps [simp del]
lemma iface_rec: " \<lbrakk>iface G I = Some (si,ib); ws_prog G\<rbrakk> \<Longrightarrow>
iface_rec (G,I) f = f I ib ((\<lambda>J. iface_rec (G,J) f)`set si)"
apply (subst iface_rec.simps)
apply simp
done
recdef class_rec "same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)"
"class_rec(G,C) = (\<lambda>t f. case class G C of None\<Rightarrow> arbitrary | Some (sc,si,cb)\<Rightarrow>
if ws_prog G then f C cb (if C = Object then t else class_rec (G,sc) t f)
else arbitrary)"
(hints recdef_wf: wf_subcls1 intro: subcls1I)
declare class_rec.simps [simp del]
lemma class_rec: "\<lbrakk>class G C = Some (sc,si,cb); ws_prog G\<rbrakk> \<Longrightarrow>
class_rec (G,C) t f = f C cb (if C = Object then t else class_rec (G,sc) t f)"
apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])
apply simp
done
section "fields and methods"
types
fspec = "ename × tname"
consts
imethds :: "prog \<Rightarrow> tname \<Rightarrow> ( sig , tname × mhead) tables"
cmethd :: "prog \<Rightarrow> tname \<Rightarrow> ( sig , tname × methd) table"
fields :: "prog \<Rightarrow> tname \<Rightarrow> ((ename × tname) × field) list"
cfield :: "prog \<Rightarrow> tname \<Rightarrow> ( ename , tname × field) table"
defs
(* methods of an interface, with overriding and inheritance, cf. 9.2 *)
imeths_def: "imethds G I \<equiv> iface_rec (G,I) (\<lambda>I ms ts.
(Un_tables ts) \<oplus>\<oplus> (o2s \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) ms)))"
(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
cmethd_def: "cmethd G C \<equiv> class_rec (G,C) empty (\<lambda>C (fs,ms,ini) ts.
ts ++ table_of (map (\<lambda>(s,m). (s,C,m)) ms))"
(* list of fields of a class, including inherited and hidden ones *)
fields_def: "fields G C \<equiv> class_rec (G,C) [] (\<lambda>C (fs,ms,ini) ts.
map (\<lambda>(n,t). ((n,C),t)) fs @ ts)"
(* fields of a class, with inheritance and hiding, cf. 8.3 *)
cfield_def: "cfield G C \<equiv> table_of((map (\<lambda>((n,d),T).(n,(d,T)))) (fields G C))"
constdefs
is_methd :: "prog \<Rightarrow> tname \<Rightarrow> sig \<Rightarrow> bool"
"is_methd G \<equiv> \<lambda>C sig. is_class G C \<and> cmethd G C sig \<noteq> None"
subsection "imethds"
lemma imethds_rec: "\<lbrakk>iface G I = Some (is,ms); ws_prog G\<rbrakk> \<Longrightarrow>
imethds G I = Un_tables ((\<lambda>J. imethds G J)`set is) \<oplus>\<oplus>
(o2s \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) ms))"
apply (unfold imeths_def)
apply (rule iface_rec [THEN trans])
apply auto
done
(* local lemma *)
lemma imethds_norec:
"\<lbrakk>iface G md = Some (is, ms); ws_prog G; table_of ms sig = Some mh\<rbrakk> \<Longrightarrow>
(md, mh) \<in> imethds G md sig"
apply (subst imethds_rec)
apply assumption+
apply (rule iffD2)
apply (rule overrides_Some_iff)
apply (rule disjI1)
apply (auto elim: table_of_map_SomeI)
done
lemma imethds_defpl: "\<lbrakk>(md,mh) \<in> imethds G I sig; ws_prog G; is_iface G I\<rbrakk> \<Longrightarrow>
(\<exists>is ms. iface G md = Some (is, ms) \<and> table_of ms sig = Some mh) \<and>
(I,md) \<in> (subint1 G)^* \<and> (md,mh) \<in> imethds G md sig"
apply (erule make_imp)
apply (rule ws_subint1_induct, assumption, assumption)
apply (subst imethds_rec, erule conjunct1, assumption)
apply (force elim: imethds_norec intro: rtrancl_into_rtrancl2)
done
subsection "cmethd"
lemma cmethd_rec: "\<lbrakk>class G C = Some (sc,si,fs,ms,ini); ws_prog G\<rbrakk> \<Longrightarrow>
cmethd G C = (if C = Object then empty else cmethd G sc) ++
table_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
apply (unfold cmethd_def)
apply (erule class_rec [THEN trans], assumption)
apply clarsimp
done
(* local lemma *)
lemma cmethd_norec: "\<lbrakk>class G md = Some (D, si, fs, ms, ini); ws_prog G;
table_of ms sig = Some m\<rbrakk> \<Longrightarrow> cmethd G md sig = Some (md, m)"
apply (subst cmethd_rec)
apply assumption+
apply (rule disjI1 [THEN override_Some_iff [THEN iffD2]])
apply (auto elim: table_of_map_SomeI)
done
lemma cmethd_defpl: "\<lbrakk>cmethd G C sig = Some (md, m); ws_prog G; is_class G C\<rbrakk> \<Longrightarrow>
(\<exists>D si fs ms ini. class G md=Some (D,si,fs,ms,ini) \<and> table_of ms sig=Some m) \<and>
(C,md)\<in>(subcls1 G)^* \<and> cmethd G md sig = Some (md, m)"
apply (erule make_imp)
apply (rule ws_subcls1_induct, assumption, assumption)
apply (subst cmethd_rec, erule conjunct1, assumption)
apply (force elim: cmethd_norec intro: rtrancl_into_rtrancl2)
done
(*unused*)
lemma finite_cmethd:"ws_prog G \<Longrightarrow> finite {cmethd G C sig |sig C. is_class G C}"
apply (rule finite_is_class [THEN finite_SetCompr2])
apply (intro strip)
apply (erule_tac ws_subcls1_induct, assumption)
apply (subst cmethd_rec)
apply (erule_tac conjunct1, assumption)
apply (auto intro!: finite_range_map_of elim!: finite_range_map_of_override)
done
lemma finite_dom_cmethd:"\<lbrakk>ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> finite (dom (cmethd G C))"
apply (erule_tac ws_subcls1_induct)
apply assumption
apply (subst cmethd_rec)
apply (erule_tac conjunct1, assumption)
apply (auto intro!: finite_dom_map_of)
done
subsection "fields"
lemma fields_rec: "\<lbrakk>class G C = Some (sc,si,fs,ms,ini); ws_prog G\<rbrakk> \<Longrightarrow>
fields G C = map (\<lambda>(fn,ft). ((fn,C),ft)) fs @
(if C = Object then [] else fields G sc)"
apply (simp only: fields_def)
apply (erule class_rec [THEN trans])
apply assumption
apply clarsimp
done
(* local lemma *)
lemma fields_norec: "\<lbrakk>class G fd = Some (D, si, fs, ms, ini); ws_prog G;
table_of fs fn = Some f\<rbrakk> \<Longrightarrow> table_of (fields G fd) (fn,fd) = Some f"
apply (subst fields_rec)
apply assumption+
apply (subst map_of_override [symmetric])
apply (rule disjI1 [THEN override_Some_iff [THEN iffD2]])
apply (auto elim: table_of_map2_SomeI)
done
lemma fields_defpl:
"\<lbrakk>table_of (fields G C) (fn,fd) = Some f; ws_prog G; is_class G C\<rbrakk> \<Longrightarrow>
(\<exists>D si fs ms ini. class G fd=Some (D,si,fs,ms,ini) \<and> table_of fs fn=Some f) \<and>
(C,fd)\<in>(subcls1 G)^* \<and> table_of (fields G fd) (fn,fd) = Some f"
apply (erule make_imp)
apply (rule ws_subcls1_induct, assumption, assumption)
apply (subst fields_rec, erule conjunct1, assumption)
apply (auto elim: fields_norec intro: rtrancl_into_rtrancl2
simp add: map_of_override [symmetric] simp del: map_of_override)
done
lemma fields_emptyI: "\<And>y. \<lbrakk>ws_prog G; class G C = Some (sc, is, [], m, c);
C \<noteq> Object \<longrightarrow> class G sc = Some y \<and> fields G sc = []\<rbrakk> \<Longrightarrow>
fields G C = []"
apply (subst fields_rec)
apply assumption
apply auto
done
(* easier than with table_of *)
lemma fields_mono_lemma:
"\<lbrakk>x \<in> set (fields G C); (D,C)\<in>(subcls1 G)^*; ws_prog G\<rbrakk> \<Longrightarrow> x \<in> set (fields G D)"
apply (erule make_imp)
apply (erule converse_rtrancl_induct)
apply fast
apply (drule subcls1D)
apply clarsimp
apply (subst fields_rec)
apply auto
done
lemma ws_unique_fields_lemma:
"\<lbrakk>((fn, C), f1) \<in> set (fields G D); (fn, f2) \<in> set fs; ws_prog G;
class G C = Some (D, si, fs, m_i); C \<noteq> Object; class G D = Some c\<rbrakk> \<Longrightarrow> R"
apply (frule_tac ws_prog_cdeclD [THEN conjunct2], assumption, assumption)
apply (drule_tac weak_map_of_SomeI)
apply (frule_tac subcls1I [THEN subcls1_irrefl], assumption, assumption)
apply (auto dest: fields_defpl [THEN conjunct2 [THEN conjunct1[THEN rtranclD]]])
done
lemma ws_unique_fields: "\<lbrakk>is_class G C; ws_prog G;
\<And>C D s fs r. \<lbrakk>class G C = Some (D, s, fs, r)\<rbrakk> \<Longrightarrow> unique fs \<rbrakk> \<Longrightarrow>
unique (fields G C)"
apply cut_tac
apply (rule ws_subcls1_induct, assumption, assumption)
apply (subst fields_rec, erule conjunct1, assumption)
apply (auto intro!: unique_map_inj injI
elim!: unique_append ws_unique_fields_lemma fields_norec)
done
subsection "cfield"
lemma cfield_fields:
"cfield G C fn = Some (fd, fT) \<Longrightarrow> table_of (fields G C) (fn, fd) = Some fT"
apply (simp only: cfield_def)
apply (rule table_of_remap_SomeD)
apply simp
done
lemma cfield_defpl_is_class:
"\<lbrakk>is_class G C; cfield G C en = Some (fd, b, fT); ws_prog G\<rbrakk> \<Longrightarrow>
is_class G fd"
apply (drule cfield_fields)
apply (drule fields_defpl [THEN conjunct1], assumption)
apply auto
done
subsection "is_methd"
lemma is_methdI:
"\<lbrakk>class G C = Some y; cmethd G C sig = Some b\<rbrakk> \<Longrightarrow> is_methd G C sig"
apply (unfold is_methd_def)
apply auto
done
lemma is_methdD:
"is_methd G C sig \<Longrightarrow> class G C \<noteq> None \<and> cmethd G C sig \<noteq> None"
apply (unfold is_methd_def)
apply auto
done
lemma finite_is_methd: "ws_prog G \<Longrightarrow> finite (Collect (split (is_methd G)))"
apply (unfold is_methd_def)
apply (subst SetCompr_Sigma_eq)
apply (rule finite_is_class [THEN finite_SigmaI])
apply (simp only: mem_Collect_eq)
apply (fold dom_def)
apply (erule finite_dom_cmethd)
apply assumption
done
end
lemma ObjectC_neq_SXcptC:
ObjectC ~= SXcptC xn
lemma SXcptC_inject:
(SXcptC xn = SXcptC xm) = (xn = xm)
lemma type_is_iface:
is_type G (Iface I) ==> is_iface G I
lemma type_is_class:
is_type G (Class C) ==> is_class G C
lemma subint1I:
[| iface G I = Some (si, ms); J : set si |] ==> (I, J) : subint1 G
lemma subcls1I:
[| class G C = Some (D, rest); C ~= Object |] ==> (C, D) : subcls1 G
lemma subint1D:
(I, J) : subint1 G ==> ? (si, ms):iface G I: J : set si
lemma subcls1D:
(C, D) : subcls1 G ==> C ~= Object & (EX cb. class G C = Some (D, cb))
lemma subint1_def2:
subint1 G = (SIGMA I:{I. is_iface G I}. set (fst (the (iface G I))))
lemma subcls1_def2:
subcls1 G =
(SIGMA C:{C. is_class G C}. {D. C ~= Object & fst (the (class G C)) = D})
lemma ws_progI:
[| ALL (I, si, ib):set (fst G).
ALL J:set si. is_iface G J & (J, I) ~: (subint1 G)^+;
ALL (C, D, cb):set (snd G).
C ~= Object --> is_class G D & (D, C) ~: (subcls1 G)^+ |]
==> ws_prog G
lemma ws_prog_ideclD:
[| iface G I = Some (si, ib); J : set si; ws_prog G |] ==> is_iface G J & (J, I) ~: (subint1 G)^+
lemma ws_prog_cdeclD:
[| class G C = Some (sc, cb); C ~= Object; ws_prog G |] ==> is_class G sc & (sc, C) ~: (subcls1 G)^+
lemma finite_is_iface:
finite {I. is_iface G I}
lemma finite_is_class:
finite {C. is_class G C}
lemma finite_subint1:
finite (subint1 G)
lemma finite_subcls1:
finite (subcls1 G)
lemma subint1_irrefl_lemma1:
ws_prog G ==> (subint1 G)^-1 Int (subint1 G)^+ = {}
lemma subcls1_irrefl_lemma1:
ws_prog G ==> (subcls1 G)^-1 Int (subcls1 G)^+ = {}
lemmas subint1_irrefl_lemma2:
ws_prog G_1 ==> ALL x. (x, x) ~: (subint1 G_1)^+ [term]
lemmas subcls1_irrefl_lemma2:
ws_prog G_1 ==> ALL x. (x, x) ~: (subcls1 G_1)^+ [term]
lemma subint1_irrefl:
[| (x, y) : subint1 G; ws_prog G |] ==> x ~= y
lemma subcls1_irrefl:
[| (x, y) : subcls1 G; ws_prog G |] ==> x ~= y
lemmas subint1_acyclic:
ws_prog G ==> acyclic (subint1 G)
lemmas subcls1_acyclic:
ws_prog G ==> acyclic (subcls1 G)
lemma wf_subint1:
ws_prog G ==> wf ((subint1 G)^-1)
lemma wf_subcls1:
ws_prog G ==> wf ((subcls1 G)^-1)
lemma subint1_induct:
[| ws_prog G; !!x. ALL y. (x, y) : subint1 G --> P y ==> P x |] ==> P a
lemma subcls1_induct:
[| ws_prog G; !!x. ALL y. (x, y) : subcls1 G --> P y ==> P x |] ==> P a
lemma ws_subint1_induct:
[| is_iface G I; ws_prog G;
!!I is ms.
iface G I = Some (is, ms) &
(ALL J:set is. (I, J) : subint1 G & P J & is_iface G J)
==> P I |]
==> P I
lemma ws_subcls1_induct:
[| is_class G C; ws_prog G;
!!C D si fs ms ini.
class G C = Some (D, si, fs, ms, ini) &
(C ~= Object --> (C, D) : subcls1 G & P D & is_class G D)
==> P C |]
==> P C
lemma iface_rec:
[| iface G I = Some (si, ib); ws_prog G |] ==> iface_rec (G, I) f = f I ib ((%J. iface_rec (G, J) f) ` set si)
lemma class_rec:
[| class G C = Some (sc, si, cb); ws_prog G |]
==> class_rec (G, C) t f =
f C cb (if C = Object then t else class_rec (G, sc) t f)
lemma imethds_rec:
[| iface G I = Some (is, ms); ws_prog G |]
==> imethds G I =
Un_tables (imethds G ` set is) \<oplus>\<oplus>
(o2s o table_of (map (%(s, mh). (s, I, mh)) ms))
lemma imethds_norec:
[| iface G md = Some (is, ms); ws_prog G; table_of ms sig = Some mh |] ==> (md, mh) : imethds G md sig
lemma imethds_defpl:
[| (md, mh) : imethds G I sig; ws_prog G; is_iface G I |]
==> (EX is ms. iface G md = Some (is, ms) & table_of ms sig = Some mh) &
(I, md) : (subint1 G)^* & (md, mh) : imethds G md sig
lemma cmethd_rec:
[| class G C = Some (sc, si, fs, ms, ini); ws_prog G |]
==> cmethd G C =
(if C = Object then empty else cmethd G sc) ++
table_of (map (%(s, m). (s, C, m)) ms)
lemma cmethd_norec:
[| class G md = Some (D, si, fs, ms, ini); ws_prog G;
table_of ms sig = Some m |]
==> cmethd G md sig = Some (md, m)
lemma cmethd_defpl:
[| cmethd G C sig = Some (md, m); ws_prog G; is_class G C |]
==> (EX D si fs ms ini.
class G md = Some (D, si, fs, ms, ini) & table_of ms sig = Some m) &
(C, md) : (subcls1 G)^* & cmethd G md sig = Some (md, m)
lemma finite_cmethd:
ws_prog G ==> finite {cmethd G C sig |sig C. is_class G C}
lemma finite_dom_cmethd:
[| ws_prog G; is_class G C |] ==> finite (dom (cmethd G C))
lemma fields_rec:
[| class G C = Some (sc, si, fs, ms, ini); ws_prog G |]
==> fields G C =
map (split (%fn. Pair (fn, C))) fs @
(if C = Object then [] else fields G sc)
lemma fields_norec:
[| class G fd = Some (D, si, fs, ms, ini); ws_prog G; table_of fs fn = Some f |] ==> table_of (fields G fd) (fn, fd) = Some f
lemma fields_defpl:
[| table_of (fields G C) (fn, fd) = Some f; ws_prog G; is_class G C |]
==> (EX D si fs ms ini.
class G fd = Some (D, si, fs, ms, ini) & table_of fs fn = Some f) &
(C, fd) : (subcls1 G)^* & table_of (fields G fd) (fn, fd) = Some f
lemma fields_emptyI:
[| ws_prog G; class G C = Some (sc, is, [], m, c);
C ~= Object --> class G sc = Some y & fields G sc = [] |]
==> fields G C = []
lemma fields_mono_lemma:
[| x : set (fields G C); (D, C) : (subcls1 G)^*; ws_prog G |] ==> x : set (fields G D)
lemma ws_unique_fields_lemma:
[| ((fn, C), f1) : set (fields G D); (fn, f2) : set fs; ws_prog G;
class G C = Some (D, si, fs, m_i); C ~= Object; class G D = Some c |]
==> R
lemma ws_unique_fields:
[| is_class G C; ws_prog G;
!!C D s fs r. class G C = Some (D, s, fs, r) ==> unique fs |]
==> unique (fields G C)
lemma cfield_fields:
cfield G C fn = Some (fd, fT) ==> table_of (fields G C) (fn, fd) = Some fT
lemma cfield_defpl_is_class:
[| is_class G C; cfield G C en = Some (fd, b, fT); ws_prog G |] ==> is_class G fd
lemma is_methdI:
[| class G C = Some y; cmethd G C sig = Some b |] ==> is_methd G C sig
lemma is_methdD:
is_methd G C sig ==> is_class G C & cmethd G C sig ~= None
lemma finite_is_methd:
ws_prog G ==> finite (Collect (split (is_methd G)))