Theory JinjaDCI.TypeRel
section ‹ Relations between Jinja Types ›
theory TypeRel imports
"HOL-Library.Transitive_Closure_Table"
Decl
begin
subsection ‹ The subclass relations ›
inductive_set
subcls1 :: "'m prog ⇒ (cname × cname) set"
and subcls1' :: "'m prog ⇒ [cname, cname] ⇒ bool" ("_ ⊢ _ ≺⇧1 _" [71,71,71] 70)
for P :: "'m prog"
where
"P ⊢ C ≺⇧1 D ≡ (C,D) ∈ subcls1 P"
| subcls1I: "⟦class P C = Some (D,rest); C ≠ Object⟧ ⟹ P ⊢ C ≺⇧1 D"
abbreviation
subcls :: "'m prog ⇒ [cname, cname] ⇒ bool" ("_ ⊢ _ ≼⇧* _" [71,71,71] 70)
where "P ⊢ C ≼⇧* D ≡ (C,D) ∈ (subcls1 P)⇧*"
lemma subcls1D: "P ⊢ C ≺⇧1 D ⟹ C ≠ Object ∧ (∃fs ms. class P C = Some (D,fs,ms))"
by(erule subcls1.induct)(fastforce simp add:is_class_def)
lemma [iff]: "¬ P ⊢ Object ≺⇧1 C"
by(fastforce dest:subcls1D)
lemma [iff]: "(P ⊢ Object ≼⇧* C) = (C = Object)"
proof(rule iffI)
assume "P ⊢ Object ≼⇧* C" then show "C = Object"
by(auto elim: converse_rtranclE)
qed simp
lemma subcls1_def2:
"subcls1 P =
(SIGMA C:{C. is_class P C}. {D. C≠Object ∧ fst (the (class P C))=D})"
by (fastforce simp:is_class_def dest: subcls1D elim: subcls1I)
lemma finite_subcls1: "finite (subcls1 P)"
proof -
let ?SIG = "SIGMA C:{C. is_class P C}. {D. fst (the (class P C)) = D ∧ C ≠ Object}"
have "subcls1 P = ?SIG" by(simp add: subcls1_def2)
also have "finite ?SIG"
proof(rule finite_SigmaI [OF finite_is_class])
fix C assume C_in: "C ∈ {C. is_class P C}"
then show "finite {D. fst (the (class P C)) = D ∧ C ≠ Object}"
by(rule_tac finite_subset[where B = "{fst (the (class P C))}"]) auto
qed
ultimately show ?thesis by simp
qed
primrec supercls_lst :: "'m prog ⇒ cname list ⇒ bool" where
"supercls_lst P (C#Cs) = ((∀C' ∈ set Cs. P ⊢ C' ≼⇧* C) ∧ supercls_lst P Cs)" |
"supercls_lst P [] = True"
lemma supercls_lst_app:
"⟦ supercls_lst P (C#Cs); P ⊢ C ≼⇧* C' ⟧ ⟹ supercls_lst P (C'#C#Cs)"
by auto
subsection‹ The subtype relations ›
inductive
widen :: "'m prog ⇒ ty ⇒ ty ⇒ bool" ("_ ⊢ _ ≤ _" [71,71,71] 70)
for P :: "'m prog"
where
widen_refl[iff]: "P ⊢ T ≤ T"
| widen_subcls: "P ⊢ C ≼⇧* D ⟹ P ⊢ Class C ≤ Class D"
| widen_null[iff]: "P ⊢ NT ≤ Class C"
abbreviation
widens :: "'m prog ⇒ ty list ⇒ ty list ⇒ bool"
("_ ⊢ _ [≤] _" [71,71,71] 70) where
"widens P Ts Ts' ≡ list_all2 (widen P) Ts Ts'"
lemma [iff]: "(P ⊢ T ≤ Void) = (T = Void)"
by (auto elim: widen.cases)
lemma [iff]: "(P ⊢ T ≤ Boolean) = (T = Boolean)"
by (auto elim: widen.cases)
lemma [iff]: "(P ⊢ T ≤ Integer) = (T = Integer)"
by (auto elim: widen.cases)
lemma [iff]: "(P ⊢ Void ≤ T) = (T = Void)"
by (auto elim: widen.cases)
lemma [iff]: "(P ⊢ Boolean ≤ T) = (T = Boolean)"
by (auto elim: widen.cases)
lemma [iff]: "(P ⊢ Integer ≤ T) = (T = Integer)"
by (auto elim: widen.cases)
lemma Class_widen: "P ⊢ Class C ≤ T ⟹ ∃D. T = Class D"
by (ind_cases "P ⊢ Class C ≤ T") auto
lemma [iff]: "(P ⊢ T ≤ NT) = (T = NT)"
by(cases T) (auto dest:Class_widen)
lemma Class_widen_Class [iff]: "(P ⊢ Class C ≤ Class D) = (P ⊢ C ≼⇧* D)"
proof(rule iffI)
show "P ⊢ Class C ≤ Class D ⟹ P ⊢ C ≼⇧* D"
proof(ind_cases "P ⊢ Class C ≤ Class D") qed(auto)
qed(auto elim: widen_subcls)
lemma widen_Class: "(P ⊢ T ≤ Class C) = (T = NT ∨ (∃D. T = Class D ∧ P ⊢ D ≼⇧* C))"
by(induct T, auto)
lemma widen_trans[trans]: "⟦P ⊢ S ≤ U; P ⊢ U ≤ T⟧ ⟹ P ⊢ S ≤ T"
proof -
assume "P⊢S ≤ U" thus "⋀T. P ⊢ U ≤ T ⟹ P ⊢ S ≤ T"
proof induct
case (widen_refl T T') thus "P ⊢ T ≤ T'" .
next
case (widen_subcls C D T)
then obtain E where "T = Class E" by (blast dest: Class_widen)
with widen_subcls show "P ⊢ Class C ≤ T" by (auto elim: rtrancl_trans)
next
case (widen_null C RT)
then obtain D where "RT = Class D" by (blast dest: Class_widen)
thus "P ⊢ NT ≤ RT" by auto
qed
qed
lemma widens_trans [trans]: "⟦P ⊢ Ss [≤] Ts; P ⊢ Ts [≤] Us⟧ ⟹ P ⊢ Ss [≤] Us"
by (rule list_all2_trans, rule widen_trans)
lemmas widens_refl [iff] = list_all2_refl [of "widen P", OF widen_refl] for P
lemmas widens_Cons [iff] = list_all2_Cons1 [of "widen P"] for P
subsection‹ Method lookup ›
inductive
Methods :: "['m prog, cname, mname ⇀ (staticb × ty list × ty × 'm) × cname] ⇒ bool"
("_ ⊢ _ sees'_methods _" [51,51,51] 50)
for P :: "'m prog"
where
sees_methods_Object:
"⟦ class P Object = Some(D,fs,ms); Mm = map_option (λm. (m,Object)) ∘ map_of ms ⟧
⟹ P ⊢ Object sees_methods Mm"
| sees_methods_rec:
"⟦ class P C = Some(D,fs,ms); C ≠ Object; P ⊢ D sees_methods Mm;
Mm' = Mm ++ (map_option (λm. (m,C)) ∘ map_of ms) ⟧
⟹ P ⊢ C sees_methods Mm'"
lemma sees_methods_fun:
assumes 1: "P ⊢ C sees_methods Mm"
shows "⋀Mm'. P ⊢ C sees_methods Mm' ⟹ Mm' = Mm"
using 1
proof induct
case (sees_methods_rec C D fs ms Dres Cres Cres')
have "class": "class P C = Some (D, fs, ms)"
and notObj: "C ≠ Object" and Dmethods: "P ⊢ D sees_methods Dres"
and IH: "⋀Dres'. P ⊢ D sees_methods Dres' ⟹ Dres' = Dres"
and Cres: "Cres = Dres ++ (map_option (λm. (m,C)) ∘ map_of ms)"
and Cmethods': "P ⊢ C sees_methods Cres'" by fact+
from Cmethods' notObj "class" obtain Dres'
where Dmethods': "P ⊢ D sees_methods Dres'"
and Cres': "Cres' = Dres' ++ (map_option (λm. (m,C)) ∘ map_of ms)"
by(auto elim: Methods.cases)
from Cres Cres' IH[OF Dmethods'] show "Cres' = Cres" by simp
next
case sees_methods_Object thus ?case by(auto elim: Methods.cases)
qed
lemma visible_methods_exist:
"P ⊢ C sees_methods Mm ⟹ Mm M = Some(m,D) ⟹
(∃D' fs ms. class P D = Some(D',fs,ms) ∧ map_of ms M = Some m)"
by(induct rule:Methods.induct) auto
lemma sees_methods_decl_above:
assumes Csees: "P ⊢ C sees_methods Mm"
shows "Mm M = Some(m,D) ⟹ P ⊢ C ≼⇧* D"
using Csees
proof induct
next
case sees_methods_Object thus ?case by auto
next
case sees_methods_rec thus ?case
by(fastforce simp:map_option_case split:option.splits
elim:converse_rtrancl_into_rtrancl[OF subcls1I])
qed
lemma sees_methods_idemp:
assumes Cmethods: "P ⊢ C sees_methods Mm"
shows "⋀m D. Mm M = Some(m,D) ⟹
∃Mm'. (P ⊢ D sees_methods Mm') ∧ Mm' M = Some(m,D)"
using Cmethods
proof induct
case sees_methods_Object thus ?case
by(fastforce dest: Methods.sees_methods_Object)
next
case sees_methods_rec thus ?case
by(fastforce split:option.splits dest: Methods.sees_methods_rec)
qed
lemma sees_methods_decl_mono:
assumes sub: "P ⊢ C' ≼⇧* C"
shows "P ⊢ C sees_methods Mm ⟹
∃Mm' Mm⇩2. P ⊢ C' sees_methods Mm' ∧ Mm' = Mm ++ Mm⇩2 ∧
(∀M m D. Mm⇩2 M = Some(m,D) ⟶ P ⊢ D ≼⇧* C)"
(is "_ ⟹ ∃Mm' Mm2. ?Q C' C Mm' Mm2")
using sub
proof (induct rule:converse_rtrancl_induct)
assume "P ⊢ C sees_methods Mm"
hence "?Q C C Mm Map.empty" by simp
thus "∃Mm' Mm2. ?Q C C Mm' Mm2" by blast
next
fix C'' C'
assume sub1: "P ⊢ C'' ≺⇧1 C'" and sub: "P ⊢ C' ≼⇧* C"
and IH: "P ⊢ C sees_methods Mm ⟹
∃Mm' Mm2. P ⊢ C' sees_methods Mm' ∧
Mm' = Mm ++ Mm2 ∧ (∀M m D. Mm2 M = Some(m,D) ⟶ P ⊢ D ≼⇧* C)"
and Csees: "P ⊢ C sees_methods Mm"
from IH[OF Csees] obtain Mm' Mm2 where C'sees: "P ⊢ C' sees_methods Mm'"
and Mm': "Mm' = Mm ++ Mm2"
and subC:"∀M m D. Mm2 M = Some(m,D) ⟶ P ⊢ D ≼⇧* C" by blast
obtain fs ms where "class": "class P C'' = Some(C',fs,ms)" "C'' ≠ Object"
using subcls1D[OF sub1] by blast
let ?Mm3 = "map_option (λm. (m,C'')) ∘ map_of ms"
have "P ⊢ C'' sees_methods (Mm ++ Mm2) ++ ?Mm3"
using sees_methods_rec[OF "class" C'sees refl] Mm' by simp
hence "?Q C'' C ((Mm ++ Mm2) ++ ?Mm3) (Mm2++?Mm3)"
using converse_rtrancl_into_rtrancl[OF sub1 sub]
by simp (simp add:map_add_def subC split:option.split)
thus "∃Mm' Mm2. ?Q C'' C Mm' Mm2" by blast
qed
lemma sees_methods_is_class_Object:
"P ⊢ D sees_methods Mm ⟹ is_class P Object"
by(induct rule: Methods.induct; simp add: is_class_def)
lemma sees_methods_sub_Obj: "P ⊢ C sees_methods Mm ⟹ P ⊢ C ≼⇧* Object"
proof(induct rule: Methods.induct)
case (sees_methods_rec C D fs ms Mm Mm') show ?case
using subcls1I[OF sees_methods_rec.hyps(1,2)] sees_methods_rec.hyps(4)
by(rule converse_rtrancl_into_rtrancl)
qed(simp)
definition Method :: "'m prog ⇒ cname ⇒ mname ⇒ staticb ⇒ ty list ⇒ ty ⇒ 'm ⇒ cname ⇒ bool"
("_ ⊢ _ sees _, _ : _→_ = _ in _" [51,51,51,51,51,51,51,51] 50)
where
"P ⊢ C sees M, b: Ts→T = m in D ≡
∃Mm. P ⊢ C sees_methods Mm ∧ Mm M = Some((b,Ts,T,m),D)"
definition has_method :: "'m prog ⇒ cname ⇒ mname ⇒ staticb ⇒ bool"
("_ ⊢ _ has _, _" [51,0,0,51] 50)
where
"P ⊢ C has M, b ≡ ∃Ts T m D. P ⊢ C sees M,b:Ts→T = m in D"
lemma sees_method_fun:
"⟦P ⊢ C sees M,b:TS→T = m in D; P ⊢ C sees M,b':TS'→T' = m' in D' ⟧
⟹ b = b' ∧ TS' = TS ∧ T' = T ∧ m' = m ∧ D' = D"
by(fastforce dest: sees_methods_fun simp:Method_def)
lemma sees_method_decl_above:
"P ⊢ C sees M,b:Ts→T = m in D ⟹ P ⊢ C ≼⇧* D"
by(clarsimp simp:Method_def sees_methods_decl_above)
lemma visible_method_exists:
"P ⊢ C sees M,b:Ts→T = m in D ⟹
∃D' fs ms. class P D = Some(D',fs,ms) ∧ map_of ms M = Some(b,Ts,T,m)"
by(fastforce simp:Method_def dest!: visible_methods_exist)
lemma sees_method_idemp:
"P ⊢ C sees M,b:Ts→T=m in D ⟹ P ⊢ D sees M,b:Ts→T=m in D"
by(fastforce simp: Method_def intro:sees_methods_idemp)
lemma sees_method_decl_mono:
assumes sub: "P ⊢ C' ≼⇧* C" and
C_sees: "P ⊢ C sees M,b:Ts→T=m in D" and
C'_sees: "P ⊢ C' sees M,b':Ts'→T'=m' in D'"
shows "P ⊢ D' ≼⇧* D"
proof -
obtain Ms where Ms: "P ⊢ C sees_methods Ms"
using C_sees by(auto simp: Method_def)
obtain Ms' Ms2 where Ms': "P ⊢ C' sees_methods Ms'" and
Ms'_def: "Ms' = Ms ++ Ms2" and
Ms2_imp: "(∀M m D. Ms2 M = ⌊(m, D)⌋ ⟶ P ⊢ D ≼⇧* C)"
using sees_methods_decl_mono[OF sub Ms] by clarsimp
have "(Ms ++ Ms2) M = ⌊((b', Ts', T', m'), D')⌋"
using C'_sees sees_methods_fun[OF Ms'] Ms'_def by(clarsimp simp: Method_def)
then have "Ms2 M = ⌊((b', Ts', T', m'), D')⌋ ∨
Ms2 M = None ∧ b = b' ∧ Ts = Ts' ∧ T = T' ∧ m = m' ∧ D = D'"
using C_sees sees_methods_fun[OF Ms] by(clarsimp simp: Method_def)
also have "Ms2 M = ⌊((b', Ts', T', m'), D')⌋ ⟹ P ⊢ D' ≼⇧* C"
using Ms2_imp by simp
ultimately show ?thesis using sub sees_method_decl_above[OF C_sees] by auto
qed
lemma sees_methods_is_class: "P ⊢ C sees_methods Mm ⟹ is_class P C"
by (auto simp add: is_class_def elim: Methods.induct)
lemma sees_method_is_class:
"⟦ P ⊢ C sees M,b:Ts→T=m in D ⟧ ⟹ is_class P C"
by (auto simp add: is_class_def Method_def dest: sees_methods_is_class)
lemma sees_method_is_class':
"⟦ P ⊢ C sees M,b:Ts→T=m in D ⟧ ⟹ is_class P D"
by(drule sees_method_idemp, rule sees_method_is_class, assumption)
lemma sees_method_sub_Obj: "P ⊢ C sees M,b: Ts→T = m in D ⟹ P ⊢ C ≼⇧* Object"
by(auto simp: Method_def sees_methods_sub_Obj)
subsection‹ Field lookup ›
inductive
Fields :: "['m prog, cname, ((vname × cname) × staticb × ty) list] ⇒ bool"
("_ ⊢ _ has'_fields _" [51,51,51] 50)
for P :: "'m prog"
where
has_fields_rec:
"⟦ class P C = Some(D,fs,ms); C ≠ Object; P ⊢ D has_fields FDTs;
FDTs' = map (λ(F,b,T). ((F,C),b,T)) fs @ FDTs ⟧
⟹ P ⊢ C has_fields FDTs'"
| has_fields_Object:
"⟦ class P Object = Some(D,fs,ms); FDTs = map (λ(F,b,T). ((F,Object),b,T)) fs ⟧
⟹ P ⊢ Object has_fields FDTs"
lemma has_fields_is_class:
"P ⊢ C has_fields FDTs ⟹ is_class P C"
by (auto simp add: is_class_def elim: Fields.induct)
lemma has_fields_fun:
assumes 1: "P ⊢ C has_fields FDTs"
shows "⋀FDTs'. P ⊢ C has_fields FDTs' ⟹ FDTs' = FDTs"
using 1
proof induct
case (has_fields_rec C D fs ms Dres Cres Cres')
have "class": "class P C = Some (D, fs, ms)"
and notObj: "C ≠ Object" and DFields: "P ⊢ D has_fields Dres"
and IH: "⋀Dres'. P ⊢ D has_fields Dres' ⟹ Dres' = Dres"
and Cres: "Cres = map (λ(F,b,T). ((F,C),b,T)) fs @ Dres"
and CFields': "P ⊢ C has_fields Cres'" by fact+
from CFields' notObj "class" obtain Dres'
where DFields': "P ⊢ D has_fields Dres'"
and Cres': "Cres' = map (λ(F,b,T). ((F,C),b,T)) fs @ Dres'"
by(auto elim: Fields.cases)
from Cres Cres' IH[OF DFields'] show "Cres' = Cres" by simp
next
case has_fields_Object thus ?case by(auto elim: Fields.cases)
qed
lemma all_fields_in_has_fields:
assumes sub: "P ⊢ C has_fields FDTs"
shows "⟦ P ⊢ C ≼⇧* D; class P D = Some(D',fs,ms); (F,b,T) ∈ set fs ⟧
⟹ ((F,D),b,T) ∈ set FDTs"
using sub proof(induct)
case (has_fields_rec C D' fs ms FDTs FDTs')
then have C_D: "P ⊢ C ≼⇧* D" by simp
then show ?case proof(rule converse_rtranclE)
assume "C = D"
then show ?case using has_fields_rec by force
next
fix y assume sub1: "P ⊢ C ≺⇧1 y" and sub2: "P ⊢ y ≼⇧* D"
then show ?case using has_fields_rec subcls1D[OF sub1] by simp
qed
next
case (has_fields_Object D fs ms FDTs)
then show ?case by force
qed
lemma has_fields_decl_above:
assumes fields: "P ⊢ C has_fields FDTs"
shows "((F,D),b,T) ∈ set FDTs ⟹ P ⊢ C ≼⇧* D"
using fields proof(induct)
case (has_fields_rec C D' fs ms FDTs FDTs')
then have "((F, D), b, T) ∈ (λx. case x of (F, x) ⇒ ((F, C), x)) ` set fs ∨
((F, D), b, T) ∈ set FDTs" by clarsimp
then show ?case proof(rule disjE)
assume "((F, D), b, T) ∈ (λx. case x of (F, x) ⇒ ((F, C), x)) ` set fs"
then show ?case using has_fields_rec by clarsimp
next
assume "((F, D), b, T) ∈ set FDTs"
then show ?case using has_fields_rec
by(blast dest:subcls1I converse_rtrancl_into_rtrancl)
qed
next
case (has_fields_Object D fs ms FDTs)
then show ?case by fastforce
qed
lemma subcls_notin_has_fields:
assumes fields: "P ⊢ C has_fields FDTs"
shows "((F,D),b,T) ∈ set FDTs ⟹ (D,C) ∉ (subcls1 P)⇧+"
using fields proof(induct)
case (has_fields_rec C D' fs ms FDTs FDTs')
then have "((F, D), b, T) ∈ (λx. case x of (F, x) ⇒ ((F, C), x)) ` set fs
∨ ((F, D), b, T) ∈ set FDTs" by clarsimp
then show ?case proof(rule disjE)
assume "((F, D), b, T) ∈ (λx. case x of (F, x) ⇒ ((F, C), x)) ` set fs"
then have CD[simp]: "C = D" and fs: "(F, b, T) ∈ set fs" by clarsimp+
then have "(D, D) ∈ (subcls1 P)⇧+ ⟹ False" proof -
assume DD: "(D, D) ∈ (subcls1 P)⇧+"
obtain z where z1: "P ⊢ D ≺⇧1 z" and z_s: "P ⊢ z ≼⇧* D"
using tranclD[OF DD] by clarsimp
have [simp]: "z = D'" using subcls1D[OF z1] has_fields_rec.hyps(1) by clarsimp
then have "((F, D), b, T) ∈ set FDTs"
using z_s all_fields_in_has_fields[OF has_fields_rec.hyps(3) _ has_fields_rec.hyps(1) fs]
by simp
then have "(D, z) ∉ (subcls1 P)⇧+" using has_fields_rec.hyps(4) by simp
then show False using z1 by auto
qed
then show ?case by clarsimp
next
assume "((F, D), b, T) ∈ set FDTs"
then show ?case using has_fields_rec by(blast dest:subcls1I trancl_into_trancl)
qed
next
case (has_fields_Object D fs ms FDTs)
then show ?case by(fastforce dest: tranclD)
qed
lemma subcls_notin_has_fields2:
assumes fields: "P ⊢ C has_fields FDTs"
shows "⟦ C ≠ Object; P ⊢ C ≺⇧1 D ⟧ ⟹ (D,C) ∉ (subcls1 P)⇧*"
using fields proof(induct arbitrary: D)
case has_fields_rec
have "∀C C' P. (C, C') ∉ subcls1 P ∨ C ≠ Object ∧ (∃fs ms. class P C = ⌊(C', fs, ms)⌋)"
using subcls1D by blast
then have "(D, D) ∉ (subcls1 P)⇧+"
by (metis (no_types) Pair_inject has_fields_rec.hyps(1) has_fields_rec.hyps(4)
has_fields_rec.prems(2) option.inject tranclD)
then show ?case
by (meson has_fields_rec.prems(2) rtrancl_into_trancl1)
qed(fastforce dest: tranclD)
lemma has_fields_mono_lem:
assumes sub: "P ⊢ D ≼⇧* C"
shows "P ⊢ C has_fields FDTs
⟹ ∃pre. P ⊢ D has_fields pre@FDTs ∧ dom(map_of pre) ∩ dom(map_of FDTs) = {}"
using sub proof(induct rule:converse_rtrancl_induct)
case base
then show ?case by(rule_tac x = "[]" in exI) simp
next
case (step D' D)
then obtain pre where D_flds: "P ⊢ D has_fields pre @ FDTs" and
dom: "dom (map_of pre) ∩ dom (map_of FDTs) = {}" by clarsimp
have "(D',C) ∈ (subcls1 P)^+" by (rule rtrancl_into_trancl2[OF step.hyps(1,2)])
obtain fs ms where D'_cls: "class P D' = ⌊(D, fs, ms)⌋" "D' ≠ Object"
using subcls1D[OF step.hyps(1)] by clarsimp+
have "P ⊢ D' has_fields map (λ(F, T). ((F, D'), T)) fs @ pre @ FDTs"
using has_fields_rec[OF D'_cls D_flds] by simp
also have "dom (map_of (map (λ(F, T). ((F, D'), T)) fs @ pre))
∩ dom (map_of FDTs) = {}"
using dom subcls_notin_has_fields[OF D_flds, where D=D'] step.hyps(1)
by(auto simp:dom_map_of_conv_image_fst) fast
ultimately show ?case
by(rule_tac x = "map (λ(F,b,T). ((F,D'),b,T)) fs @ pre" in exI) simp
qed
lemma has_fields_declaring_classes:
shows "P ⊢ C has_fields FDTs
⟹ ∃pre FDTs'. FDTs = pre@FDTs'
∧ (C ≠ Object ⟶ (∃D fs ms. class P C = ⌊(D,fs,ms)⌋ ∧ P ⊢ D has_fields FDTs'))
∧ set(map (λt. snd(fst t)) pre) ⊆ {C}
∧ set(map (λt. snd(fst t)) FDTs') ⊆ {C'. C' ≠ C ∧ P ⊢ C ≼⇧* C'}"
proof(induct rule:Fields.induct)
case (has_fields_rec C D fs ms FDTs FDTs')
have sup1: "P ⊢ C ≺⇧1 D" using has_fields_rec.hyps(1,2) by (simp add: subcls1.subcls1I)
have "P ⊢ C has_fields FDTs'"
using Fields.has_fields_rec[OF has_fields_rec.hyps(1-3)] has_fields_rec by auto
then have nsup: "(D, C) ∉ (subcls1 P)⇧*" using subcls_notin_has_fields2 sup1 by auto
show ?case using has_fields_rec sup1 nsup
by(rule_tac x = "map (λ(F, y). ((F, C), y)) fs" in exI, clarsimp) auto
next
case has_fields_Object then show ?case by fastforce
qed
lemma has_fields_mono_lem2:
assumes hf: "P ⊢ C has_fields FDTs"
and cls: "class P C = Some(D,fs,ms)" and map_of: "map_of FDTs (F,C) = ⌊(b,T)⌋"
shows "∃FDTs'. FDTs = (map (λ(F,b,T). ((F,C),b,T)) fs) @ FDTs' ∧ map_of FDTs' (F,C) = None"
using assms
proof(cases "C = Object")
case False
let ?pre = "map (λ(F,b,T). ((F,C),b,T)) fs"
have sub: "P ⊢ C ≼⇧* D" using cls False by (simp add: r_into_rtrancl subcls1.subcls1I)
obtain FDTs' where fdts': "P ⊢ D has_fields FDTs'" "FDTs = ?pre @ FDTs'"
using False assms(1,2) Fields.simps[of P C FDTs] by clarsimp
then have int: "dom (map_of ?pre) ∩ dom (map_of FDTs') = {}"
using has_fields_mono_lem[OF sub, of FDTs'] has_fields_fun[OF hf] by fastforce
have "C ∉ (λt. snd (fst t)) ` set FDTs'"
using has_fields_declaring_classes[OF hf] cls False
has_fields_fun[OF fdts'(1)] fdts'(2)
by clarify auto
then have "map_of FDTs' (F,C) = None" by(rule map_of_set_pcs_notin)
then show ?thesis using fdts' int by simp
qed(auto dest: has_fields_Object has_fields_fun)
lemma has_fields_is_class_Object:
"P ⊢ D has_fields FDTs ⟹ is_class P Object"
by(induct rule: Fields.induct; simp add: is_class_def)
lemma Object_fields:
"⟦ P ⊢ Object has_fields FDTs; C ≠ Object ⟧ ⟹ map_of FDTs (F,C) = None"
by(drule Fields.cases, auto simp: map_of_reinsert_neq_None)
definition has_field :: "'m prog ⇒ cname ⇒ vname ⇒ staticb ⇒ ty ⇒ cname ⇒ bool"
("_ ⊢ _ has _,_:_ in _" [51,51,51,51,51,51] 50)
where
"P ⊢ C has F,b:T in D ≡
∃FDTs. P ⊢ C has_fields FDTs ∧ map_of FDTs (F,D) = Some (b,T)"
lemma has_field_mono:
assumes has: " P ⊢ C has F,b:T in D" and sub: "P ⊢ C' ≼⇧* C"
shows "P ⊢ C' has F,b:T in D"
proof -
obtain FDTs where FDTs:"P ⊢ C has_fields FDTs" and "map_of FDTs (F, D) = ⌊(b, T)⌋"
using has by(clarsimp simp: has_field_def)
also obtain pre where "P ⊢ C' has_fields pre @ FDTs"
and "dom (map_of pre) ∩ dom (map_of FDTs) = {}"
using has_fields_mono_lem[OF sub FDTs] by clarify
ultimately show ?thesis by(fastforce simp: has_field_def map_add_def split:option.splits)
qed
lemma has_field_fun:
"⟦P ⊢ C has F,b:T in D; P ⊢ C has F,b':T' in D⟧ ⟹ b = b' ∧ T' = T"
by(fastforce simp:has_field_def dest:has_fields_fun)
lemma has_field_idemp:
assumes has: "P ⊢ C has F,b:T in D"
shows "P ⊢ D has F,b:T in D"
proof -
obtain FDTs where C_flds: "P ⊢ C has_fields FDTs"
and FDTs: "map_of FDTs (F, D) = ⌊(b, T)⌋" (is "?FDTs")
using has by(clarsimp simp: has_field_def)
have map: "⋀C' fs. map_of (map (λ(F, y). ((F, C'), y)) fs) (F, D) = ⌊(b, T)⌋ ⟹ D = C'"
by(frule map_of_SomeD) clarsimp
have "?FDTs ⟶ P ⊢ D has F,b:T in D"
using C_flds proof induct
case NObj: (has_fields_rec C' D' fs ms FDTs FDTs')
then show ?case using map by (fastforce intro: has_fields_rec simp: has_field_def)
next
case Obj: (has_fields_Object D fs ms FDTs)
then show ?case using map by(fastforce intro: has_fields_Object simp: has_field_def)
qed
then show ?thesis using FDTs by(rule_tac mp)
qed
lemma visible_fields_exist:
assumes fields: "P ⊢ C has_fields FDTs" and
FDTs: "map_of FDTs (F,D) = Some (b, T)"
shows "∃D' fs ms. class P D = Some(D',fs,ms) ∧ map_of fs F = Some(b,T)"
proof -
have "map_of FDTs (F,D) = Some (b, T) ⟶
(∃D' fs ms. class P D = Some(D',fs,ms) ∧ map_of fs F = Some(b,T))"
using fields proof induct
case (has_fields_rec C' D' fs ms FDTs')
with assms map_of_reinsert_SomeD map_of_reinsert_neq_None[where D=D and F=F and fs=fs]
show ?case proof(cases "C' = D") qed auto
next
case (has_fields_Object D' fs ms FDTs)
with assms map_of_reinsert_SomeD map_of_reinsert_neq_None[where D=D and F=F and fs=fs]
show ?case proof(cases "Object = D") qed auto
qed
then show ?thesis using FDTs by simp
qed
lemma map_of_remap_SomeD:
"map_of (map (λ((k,k'),x). (k,(k',x))) t) k = Some (k',x) ⟹ map_of t (k, k') = Some x"
by (induct t) (auto simp:fun_upd_apply split: if_split_asm)
lemma map_of_remap_SomeD2:
"map_of (map (λ((k,k'),x,x'). (k,(k',x,x'))) t) k = Some (k',x,x') ⟹ map_of t (k, k') = Some (x, x')"
by (induct t) (auto simp:fun_upd_apply split: if_split_asm)
lemma has_field_decl_above:
"P ⊢ C has F,b:T in D ⟹ P ⊢ C ≼⇧* D"
by(auto simp: has_field_def
intro: has_fields_decl_above map_of_SomeD map_of_remap_SomeD2)
definition sees_field :: "'m prog ⇒ cname ⇒ vname ⇒ staticb ⇒ ty ⇒ cname ⇒ bool"
("_ ⊢ _ sees _,_:_ in _" [51,51,51,51,51,51] 50)
where
"P ⊢ C sees F,b:T in D ≡
∃FDTs. P ⊢ C has_fields FDTs ∧
map_of (map (λ((F,D),b,T). (F,(D,b,T))) FDTs) F = Some(D,b,T)"
lemma has_visible_field:
"P ⊢ C sees F,b:T in D ⟹ P ⊢ C has F,b:T in D"
by(auto simp add:has_field_def sees_field_def map_of_remap_SomeD2)
lemma sees_field_fun:
"⟦P ⊢ C sees F,b:T in D; P ⊢ C sees F,b':T' in D'⟧ ⟹ b = b' ∧ T' = T ∧ D' = D"
by(fastforce simp:sees_field_def dest:has_fields_fun)
lemma sees_field_decl_above:
"P ⊢ C sees F,b:T in D ⟹ P ⊢ C ≼⇧* D"
by(auto simp:sees_field_def
intro: has_fields_decl_above map_of_SomeD map_of_remap_SomeD2)
lemma sees_field_idemp:
assumes sees: "P ⊢ C sees F,b:T in D"
shows "P ⊢ D sees F,b:T in D"
proof -
obtain FDTs where C_flds: "P ⊢ C has_fields FDTs"
and FDTs: "map_of (map (λ((F, D), b, T). (F, D, b, T)) FDTs) F = ⌊(D, b, T)⌋"
(is "?FDTs")
using sees by(clarsimp simp: sees_field_def)
have map: "⋀C' fs. map_of (map ((λ((F, D), a). (F, D, a)) ∘ (λ(F, y). ((F, C'), y))) fs) F
= ⌊(D, b, T)⌋
⟹ D = C' ∧ (F, b, T) ∈ set fs"
by(frule map_of_SomeD) clarsimp
have "?FDTs ⟶ (∃FDTs. P ⊢ D has_fields FDTs
∧ map_of (map (λ((F, D), a). (F, D, a)) FDTs) F = ⌊(D, b, T)⌋)"
using C_flds proof induct
case NObj: (has_fields_rec C' D' fs ms FDTs FDTs')
then show ?case using map by (fastforce intro: has_fields_rec)
next
case Obj: (has_fields_Object D fs ms FDTs)
then show ?case using map by(fastforce intro: has_fields_Object)
qed
then show ?thesis using FDTs
by (smt map_eq_conv old.prod.case prod_cases3 sees_field_def split_cong)
qed
lemma has_field_sees_aux:
assumes hf: "P ⊢ C has_fields FDTs" and map: "map_of FDTs (F, C) = ⌊(b, T)⌋"
shows "map_of (map (λ((F, D), b, T). (F, D, b, T)) FDTs) F = ⌊(C, b, T)⌋"
proof -
obtain D fs ms where fs: "class P C = Some(D,fs,ms)"
using visible_fields_exist[OF assms] by clarsimp
then obtain FDTs' where
"FDTs = map (λ(F, b, T). ((F, C), b, T)) fs @ FDTs' ∧ map_of FDTs' (F, C) = None"
using has_fields_mono_lem2[OF hf fs map] by clarsimp
then show ?thesis using map_of_Some_None_split[OF _ _ map] by auto
qed
lemma has_field_sees: "P ⊢ C has F,b:T in C ⟹ P ⊢ C sees F,b:T in C"
by(auto simp:has_field_def sees_field_def has_field_sees_aux)
lemma has_field_is_class:
"P ⊢ C has F,b:T in D ⟹ is_class P C"
by (auto simp add: is_class_def has_field_def elim: Fields.induct)
lemma has_field_is_class':
"P ⊢ C has F,b:T in D ⟹ is_class P D"
by(drule has_field_idemp, rule has_field_is_class, assumption)
subsection "Functional lookup"
definition "method" :: "'m prog ⇒ cname ⇒ mname ⇒ cname × staticb × ty list × ty × 'm"
where
"method P C M ≡ THE (D,b,Ts,T,m). P ⊢ C sees M,b:Ts → T = m in D"
definition field :: "'m prog ⇒ cname ⇒ vname ⇒ cname × staticb × ty"
where
"field P C F ≡ THE (D,b,T). P ⊢ C sees F,b:T in D"
definition fields :: "'m prog ⇒ cname ⇒ ((vname × cname) × staticb × ty) list"
where
"fields P C ≡ THE FDTs. P ⊢ C has_fields FDTs"
lemma fields_def2 [simp]: "P ⊢ C has_fields FDTs ⟹ fields P C = FDTs"
by (unfold fields_def) (auto dest: has_fields_fun)
lemma field_def2 [simp]: "P ⊢ C sees F,b:T in D ⟹ field P C F = (D,b,T)"
by (unfold field_def) (auto dest: sees_field_fun)
lemma method_def2 [simp]: "P ⊢ C sees M,b: Ts→T = m in D ⟹ method P C M = (D,b,Ts,T,m)"
by (unfold method_def) (auto dest: sees_method_fun)
text ‹ The following are the fields for initializing an object (non-static fields)
and a class (just that class's static fields), respectively. ›
definition ifields :: "'m prog ⇒ cname ⇒ ((vname × cname) × staticb × ty) list"
where
"ifields P C ≡ filter (λ((F,D),b,T). b = NonStatic) (fields P C)"
definition isfields :: "'m prog ⇒ cname ⇒ ((vname × cname) × staticb × ty) list"
where
"isfields P C ≡ filter (λ((F,D),b,T). b = Static ∧ D = C) (fields P C)"
lemma ifields_def2[simp]: "⟦ P ⊢ C has_fields FDTs ⟧ ⟹ ifields P C = filter (λ((F,D),b,T). b = NonStatic) FDTs"
by (simp add: ifields_def)
lemma isfields_def2[simp]: "⟦ P ⊢ C has_fields FDTs ⟧ ⟹ isfields P C = filter (λ((F,D),b,T). b = Static ∧ D = C) FDTs"
by (simp add: isfields_def)
lemma ifields_def3: "⟦ P ⊢ C sees F,b:T in D; b = NonStatic ⟧ ⟹ (((F,D),b,T) ∈ set (ifields P C))"
by (unfold ifields_def) (auto simp: sees_field_def map_of_SomeD map_of_remap_SomeD2)
lemma isfields_def3: "⟦ P ⊢ C sees F,b:T in D; b = Static; D = C ⟧ ⟹ (((F,D),b,T) ∈ set (isfields P C))"
by (unfold isfields_def) (auto simp: sees_field_def map_of_SomeD map_of_remap_SomeD2)
definition seeing_class :: "'m prog ⇒ cname ⇒ mname ⇒ cname option" where
"seeing_class P C M =
(if ∃Ts T m D. P ⊢ C sees M,Static:Ts→T = m in D
then Some (fst(method P C M))
else None)"
lemma seeing_class_def2[simp]:
"P ⊢ C sees M,Static:Ts→T = m in D ⟹ seeing_class P C M = Some D"
by(fastforce simp: seeing_class_def)
end