Theory TypeRel
section ‹Relations between Jinja Types›
theory TypeRel
imports
Decl
begin
subsection‹The subclass relations›
inductive subcls1 :: "'m prog ⇒ cname ⇒ cname ⇒ bool" ("_ ⊢ _ ≺⇧1 _" [71, 71, 71] 70)
for P :: "'m prog"
where 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 ≡ (subcls1 P)⇧*⇧* C D"
lemma subcls1D:
"P ⊢ C ≺⇧1 D ⟹ C ≠ Object ∧ (∃fs ms. class P C = Some (D,fs,ms))"
by(auto elim: subcls1.cases)
lemma Object_subcls1 [iff]: "¬ P ⊢ Object ≺⇧1 C"
by(simp add: subcls1.simps)
lemma Object_subcls_conv [iff]: "(P ⊢ Object ≼⇧* C) = (C = Object)"
by(auto elim: converse_rtranclpE)
lemma finite_subcls1: "finite {(C, D). P ⊢ C ≺⇧1 D}"
proof -
let ?A = "SIGMA C:{C. is_class P C}. {D. C≠Object ∧ fst (the (class P C))=D}"
have "finite ?A" by(rule finite_SigmaI [OF finite_is_class]) auto
also have "?A = {(C, D). P ⊢ C ≺⇧1 D}"
by(fastforce simp:is_class_def dest: subcls1D elim: subcls1I)
finally show ?thesis .
qed
lemma finite_subcls1':
"finite ({(D, C). P ⊢ C ≺⇧1 D})"
by(subst finite_converse[symmetric])
(simp add: converse_unfold finite_subcls1 del: finite_converse)
lemma subcls_is_class: "(subcls1 P)⇧+⇧+ C D ⟹ is_class P C"
by(auto elim: converse_tranclpE dest!: subcls1D simp add: is_class_def)
lemma subcls_is_class1: "⟦ P ⊢ C ≼⇧* D; is_class P D ⟧ ⟹ is_class P C"
by(auto elim: converse_rtranclpE dest!: subcls1D simp add: is_class_def)
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"
| widen_null_array[iff]: "P ⊢ NT ≤ Array A"
| widen_array_object: "P ⊢ Array A ≤ Class Object"
| widen_array_array: "P ⊢ A ≤ B ⟹ P ⊢ Array A ≤ Array B"
abbreviation
widens :: "'m prog ⇒ ty list ⇒ ty list ⇒ bool" ("_ ⊢ _ [≤] _" [71,71,71] 70)
where
"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(erule widen.cases, auto)
lemma Array_Array_widen:
"P ⊢ Array T ≤ Array U ⟹ P ⊢ T ≤ U"
by(auto elim: widen.cases)
lemma widen_Array: "(P ⊢ T ≤ U⌊⌉) ⟷ (T = NT ∨ (∃V. T = V⌊⌉ ∧ P ⊢ V ≤ U))"
by(induct T)(auto dest: Array_Array_widen elim: widen.cases intro: widen_array_array)
lemma Array_widen: "P ⊢ Array A ≤ T ⟹ (∃B. T = Array B ∧ P ⊢ A ≤ B) ∨ T = Class Object"
by(auto elim: widen.cases)
lemma [iff]: "(P ⊢ T ≤ NT) = (T = NT)"
by(induct T)(auto dest:Class_widen Array_widen)
lemma Class_widen_Class [iff]: "(P ⊢ Class C ≤ Class D) = (P ⊢ C ≼⇧* D)"
by (auto elim: widen_subcls widen.cases)
lemma widen_Class: "(P ⊢ T ≤ Class C) = (T = NT ∨ (∃D. T = Class D ∧ P ⊢ D ≼⇧* C) ∨ (C = Object ∧ (∃A. T = Array A)))"
by(induct T)(auto dest: Array_widen intro: widen_array_object)
lemma NT_widen:
"P ⊢ NT ≤ T = (T = NT ∨ (∃C. T = Class C) ∨ (∃U. T = U⌊⌉))"
by(cases T) auto
lemma Class_widen2: "P ⊢ Class C ≤ T = (∃D. T = Class D ∧ P ⊢ C ≼⇧* D)"
by (cases T, auto elim: widen.cases)
lemma Object_widen: "P ⊢ Class Object ≤ T ⟹ T = Class Object"
by(cases T, auto elim: widen.cases)
lemma NT_Array_widen_Object:
"is_NT_Array T ⟹ P ⊢ T ≤ Class Object"
by(induct T, auto intro: widen_array_object)
lemma widen_trans[trans]:
assumes "P ⊢ S ≤ U" "P ⊢ U ≤ T"
shows "P ⊢ S ≤ T"
using assms
proof(induct arbitrary: T)
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
next
case widen_null_array thus ?case by(auto dest: Array_widen)
next
case (widen_array_object A T)
hence "T = Class Object" by(rule Object_widen)
with widen_array_object show "P ⊢ A⌊⌉ ≤ T"
by(auto intro: widen.widen_array_object)
next
case widen_array_array thus ?case
by(auto dest!: Array_widen intro: widen.widen_array_array widen_array_object)
qed
lemma widens_trans: "⟦P ⊢ Ss [≤] Ts; P ⊢ Ts [≤] Us⟧ ⟹ P ⊢ Ss [≤] Us"
by (rule list_all2_trans)(rule widen_trans)
lemma class_type_of'_widenD:
"class_type_of' T = ⌊C⌋ ⟹ P ⊢ T ≤ Class C"
by(cases T)(auto intro: widen_array_object)
lemma widen_is_class_type_of:
assumes "class_type_of' T = ⌊C⌋" "P ⊢ T' ≤ T" "T' ≠ NT"
obtains C' where "class_type_of' T' = ⌊C'⌋" "P ⊢ C' ≼⇧* C"
using assms by(cases T)(auto simp add: widen_Class widen_Array)
lemma widens_refl: "P ⊢ Ts [≤] Ts"
by(rule list_all2_refl[OF widen_refl])
lemma widen_append1:
"P ⊢ (xs @ ys) [≤] Ts = (∃Ts1 Ts2. Ts = Ts1 @ Ts2 ∧ length xs = length Ts1 ∧ length ys = length Ts2 ∧ P ⊢ xs [≤] Ts1 ∧ P ⊢ ys [≤] Ts2)"
unfolding list_all2_append1 by fastforce
lemmas widens_Cons [iff] = list_all2_Cons1 [of "widen P"] for P
lemma widens_lengthD:
"P ⊢ xs [≤] ys ⟹ length xs = length ys"
by(rule list_all2_lengthD)
lemma widen_refT: "⟦ is_refT T; P ⊢ U ≤ T ⟧ ⟹ is_refT U"
by(erule refTE)(auto simp add: widen_Class widen_Array)
lemma refT_widen: "⟦ is_refT T; P ⊢ T ≤ U ⟧ ⟹ is_refT U"
by(erule widen.cases) auto
inductive is_lub :: "'m prog ⇒ ty ⇒ ty ⇒ ty ⇒ bool" ("_ ⊢ lub'((_,/ _)') = _" [51,51,51,51] 50)
for P :: "'m prog" and U :: ty and V :: ty and T :: ty
where
"⟦ P ⊢ U ≤ T; P ⊢ V ≤ T;
⋀T'. ⟦ P ⊢ U ≤ T'; P ⊢ V ≤ T' ⟧ ⟹ P ⊢ T ≤ T' ⟧
⟹ P ⊢ lub(U, V) = T"
lemma is_lub_upper:
"P ⊢ lub(U, V) = T ⟹ P ⊢ U ≤ T ∧ P ⊢ V ≤ T"
by(auto elim: is_lub.cases)
lemma is_lub_least:
"⟦ P ⊢ lub(U, V) = T; P ⊢ U ≤ T'; P ⊢ V ≤ T' ⟧ ⟹ P ⊢ T ≤ T'"
by(auto elim: is_lub.cases)
lemma is_lub_Void [iff]:
"P ⊢ lub(Void, Void) = T ⟷ T = Void"
by(auto intro: is_lub.intros elim: is_lub.cases)
lemma is_lubI [code_pred_intro]:
"⟦P ⊢ U ≤ T; P ⊢ V ≤ T; ∀T'. P ⊢ U ≤ T' ⟶ P ⊢ V ≤ T' ⟶ P ⊢ T ≤ T'⟧ ⟹ P ⊢ lub(U, V) = T"
by(blast intro: is_lub.intros)
subsection‹Method lookup›
inductive Methods :: "'m prog ⇒ cname ⇒ (mname ⇀ (ty list × ty × 'm option) × 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 "P ⊢ C sees_methods Mm"
shows "P ⊢ C sees_methods Mm' ⟹ Mm' = Mm"
using assms
proof(induction arbitrary: Mm')
case sees_methods_Object thus ?case by(auto elim: Methods.cases)
next
case (sees_methods_rec C D fs ms Dres Cres Cres')
from ‹P ⊢ C sees_methods Cres'› ‹C ≠ Object› ‹class P C = ⌊(D, fs, ms)⌋›
obtain Dres' where Dmethods': "P ⊢ D sees_methods Dres'"
and Cres': "Cres' = Dres' ++ (map_option (λm. (m,C)) ∘ map_of ms)"
by cases auto
from sees_methods_rec.IH[OF Dmethods'] ‹Cres = Dres ++ (map_option (λm. (m,C)) ∘ map_of ms)› Cres'
show ?case by simp
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 "P ⊢ C sees_methods Mm"
shows "Mm M = Some(m,D) ⟹ P ⊢ C ≼⇧* D"
using assms
by induct(auto elim: converse_rtranclp_into_rtranclp[where r = "subcls1 P", OF subcls1I])
lemma sees_methods_idemp:
assumes "P ⊢ C sees_methods Mm" and "Mm M = Some(m,D)"
shows "∃Mm'. (P ⊢ D sees_methods Mm') ∧ Mm' M = Some(m,D)"
using assms
by(induct arbitrary: m D)(fastforce dest: Methods.intros)+
lemma sees_methods_decl_mono:
assumes sub: "P ⊢ C' ≼⇧* C" and "P ⊢ C sees_methods Mm"
shows "∃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 assms
proof (induction rule: converse_rtranclp_induct)
case base
hence "?Q C C Mm Map.empty" by simp
thus "∃Mm' Mm2. ?Q C C Mm' Mm2" by blast
next
case (step C'' C')
note sub1 = ‹P ⊢ C'' ≺⇧1 C'› and sub = ‹P ⊢ C' ≼⇧* C›
and Csees = ‹P ⊢ C sees_methods Mm›
from step.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_rtranclp_into_rtranclp[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
definition Method :: "'m prog ⇒ cname ⇒ mname ⇒ ty list ⇒ ty ⇒ 'm option ⇒ cname ⇒ bool"
("_ ⊢ _ sees _: _→_ = _ in _" [51,51,51,51,51,51,51] 50)
where
"P ⊢ C sees M: Ts→T = m in D ≡
∃Mm. P ⊢ C sees_methods Mm ∧ Mm M = Some((Ts,T,m),D)"
text ‹
Output translation to replace @{term "None"} with its notation ‹Native›
when used as method body in @{term "Method"}.
›
abbreviation (output)
Method_native :: "'m prog ⇒ cname ⇒ mname ⇒ ty list ⇒ ty ⇒ cname ⇒ bool"
("_ ⊢ _ sees _: _→_ = Native in _" [51,51,51,51,51,51] 50)
where "Method_native P C M Ts T D ≡ Method P C M Ts T Native D"
definition has_method :: "'m prog ⇒ cname ⇒ mname ⇒ bool" ("_ ⊢ _ has _" [51,0,51] 50)
where
"P ⊢ C has M ≡ ∃Ts T m D. P ⊢ C sees M:Ts→T = m in D"
lemma has_methodI:
"P ⊢ C sees M:Ts→T = m in D ⟹ P ⊢ C has M"
by (unfold has_method_def) blast
lemma sees_method_fun:
"⟦P ⊢ C sees M:TS→T = m in D; P ⊢ C sees M:TS'→T' = m' in D' ⟧
⟹ 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: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:Ts→T = m in D ⟹
∃D' fs ms. class P D = Some(D',fs,ms) ∧ map_of ms M = Some(Ts,T,m)"
by(fastforce simp:Method_def dest!: visible_methods_exist)
lemma sees_method_idemp:
"P ⊢ C sees M:Ts→T=m in D ⟹ P ⊢ D sees M:Ts→T=m in D"
by(fastforce simp: Method_def intro:sees_methods_idemp)
lemma sees_method_decl_mono:
"⟦ P ⊢ C' ≼⇧* C; P ⊢ C sees M:Ts→T = m in D;
P ⊢ C' sees M:Ts'→T' = m' in D' ⟧ ⟹ P ⊢ D' ≼⇧* D"
apply(frule sees_method_decl_above)
apply(unfold Method_def)
apply clarsimp
apply(drule (1) sees_methods_decl_mono)
apply clarsimp
apply(drule (1) sees_methods_fun)
apply clarsimp
apply(blast intro:rtranclp_trans)
done
lemma sees_method_is_class:
"P ⊢ C sees M:Ts→T = m in D ⟹ is_class P C"
by (auto simp add: is_class_def Method_def elim: Methods.cases)
subsection‹Field lookup›
inductive Fields :: "'m prog ⇒ cname ⇒ ((vname × cname) × (ty × fmod)) 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,Tm). ((F,C),Tm)) fs @ FDTs ⟧
⟹ P ⊢ C has_fields FDTs'"
| has_fields_Object:
"⟦ class P Object = Some(D,fs,ms); FDTs = map (λ(F,T). ((F,Object),T)) fs ⟧
⟹ P ⊢ Object has_fields FDTs"
lemma has_fields_fun:
assumes "P ⊢ C has_fields FDTs" and "P ⊢ C has_fields FDTs'"
shows "FDTs' = FDTs"
using assms
proof(induction arbitrary: FDTs')
case has_fields_Object thus ?case by(auto elim: Fields.cases)
next
case (has_fields_rec C D fs ms Dres Cres Cres')
from ‹P ⊢ C has_fields Cres'› ‹C ≠ Object› ‹class P C = Some (D, fs, ms)›
obtain Dres' where DFields': "P ⊢ D has_fields Dres'"
and Cres': "Cres' = map (λ(F,Tm). ((F,C),Tm)) fs @ Dres'"
by cases auto
from has_fields_rec.IH[OF DFields'] ‹Cres = map (λ(F,Tm). ((F,C),Tm)) fs @ Dres› Cres'
show ?case by simp
qed
lemma all_fields_in_has_fields:
assumes "P ⊢ C has_fields FDTs"
and "P ⊢ C ≼⇧* D" "class P D = Some(D',fs,ms)" "(F,Tm) ∈ set fs"
shows "((F,D),Tm) ∈ set FDTs"
using assms
by induct (auto 4 3 elim: converse_rtranclpE dest: subcls1D)
lemma has_fields_decl_above:
assumes "P ⊢ C has_fields FDTs" "((F,D),Tm) ∈ set FDTs"
shows "P ⊢ C ≼⇧* D"
using assms
by induct (auto intro: converse_rtranclp_into_rtranclp subcls1I)
lemma subcls_notin_has_fields:
assumes "P ⊢ C has_fields FDTs" "((F,D),Tm) ∈ set FDTs"
shows "¬ (subcls1 P)⇧+⇧+ D C"
using assms apply(induct)
prefer 2 apply(fastforce dest: tranclpD)
apply clarsimp
apply(erule disjE)
apply(clarsimp simp add:image_def)
apply(drule tranclpD)
apply clarify
apply(frule subcls1D)
apply(fastforce dest:tranclpD all_fields_in_has_fields)
apply(blast dest:subcls1I tranclp.trancl_into_trancl)
done
lemma has_fields_mono_lem:
assumes "P ⊢ D ≼⇧* C" "P ⊢ C has_fields FDTs"
shows "∃pre. P ⊢ D has_fields pre@FDTs ∧ dom(map_of pre) ∩ dom(map_of FDTs) = {}"
using assms
apply(induct rule:converse_rtranclp_induct)
apply(rule_tac x = "[]" in exI)
apply simp
apply clarsimp
apply(rename_tac D' D pre)
apply(subgoal_tac "(subcls1 P)^++ D' C")
prefer 2 apply(erule (1) rtranclp_into_tranclp2)
apply(drule subcls1D)
apply clarsimp
apply(rename_tac fs ms)
apply(drule (2) has_fields_rec)
apply(rule refl)
apply(rule_tac x = "map (λ(F,Tm). ((F,D'),Tm)) fs @ pre" in exI)
apply simp
apply(simp add:Int_Un_distrib2)
apply(rule equals0I)
apply(auto dest: subcls_notin_has_fields simp:dom_map_of_conv_image_fst image_def)
done
lemma has_fields_is_class:
"P ⊢ C has_fields FDTs ⟹ is_class P C"
by (auto simp add: is_class_def elim: Fields.cases)
lemma Object_has_fields_Object:
assumes "P ⊢ Object has_fields FDTs"
shows "snd ` fst ` set FDTs ⊆ {Object}"
using assms by cases auto
definition
has_field :: "'m prog ⇒ cname ⇒ vname ⇒ ty ⇒ fmod ⇒ cname ⇒ bool"
("_ ⊢ _ has _:_ '(_') in _" [51,51,51,51,51,51] 50)
where
"P ⊢ C has F:T (fm) in D ≡
∃FDTs. P ⊢ C has_fields FDTs ∧ map_of FDTs (F,D) = Some (T, fm)"
lemma has_field_mono:
"⟦ P ⊢ C has F:T (fm) in D; P ⊢ C' ≼⇧* C ⟧ ⟹ P ⊢ C' has F:T (fm) in D"
by(fastforce simp:has_field_def map_add_def dest: has_fields_mono_lem)
lemma has_field_is_class:
"P ⊢ C has M:T (fm) in D ⟹ is_class P C"
by (auto simp add: is_class_def has_field_def elim: Fields.cases)
lemma has_field_decl_above:
"P ⊢ C has F:T (fm) in D ⟹ P ⊢ C ≼⇧* D"
unfolding has_field_def
by(auto dest: map_of_SomeD has_fields_decl_above)
lemma has_field_fun:
"⟦P ⊢ C has F:T (fm) in D; P ⊢ C has F:T' (fm') in D⟧ ⟹ T' = T ∧ fm = fm'"
by(auto simp:has_field_def dest:has_fields_fun)
definition
sees_field :: "'m prog ⇒ cname ⇒ vname ⇒ ty ⇒ fmod ⇒ cname ⇒ bool"
("_ ⊢ _ sees _:_ '(_') in _" [51,51,51,51,51,51] 50)
where
"P ⊢ C sees F:T (fm) in D ≡
∃FDTs. P ⊢ C has_fields FDTs ∧
map_of (map (λ((F,D),Tm). (F,(D,Tm))) FDTs) F = Some(D,T,fm)"
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 has_visible_field:
"P ⊢ C sees F:T (fm) in D ⟹ P ⊢ C has F:T (fm) in D"
by(auto simp add:has_field_def sees_field_def map_of_remap_SomeD)
lemma sees_field_fun:
"⟦P ⊢ C sees F:T (fm) in D; P ⊢ C sees F:T' (fm') in D'⟧ ⟹ T' = T ∧ D' = D ∧ fm = fm'"
by(fastforce simp:sees_field_def dest:has_fields_fun)
lemma sees_field_decl_above:
"P ⊢ C sees F:T (fm) in D ⟹ P ⊢ C ≼⇧* D"
by(clarsimp simp add: sees_field_def)
(blast intro: has_fields_decl_above map_of_SomeD map_of_remap_SomeD)
lemma sees_field_idemp:
assumes "P ⊢ C sees F:T (fm) in D"
shows "P ⊢ D sees F:T (fm) in D"
proof -
from assms obtain FDTs where has: "P ⊢ C has_fields FDTs"
and F: "map_of (map (λ((F, D), Tm). (F, D, Tm)) FDTs) F = ⌊(D, T, fm)⌋"
unfolding sees_field_def by blast
thus ?thesis
proof induct
case has_fields_rec thus ?case unfolding sees_field_def
by(auto)(fastforce dest: map_of_SomeD intro!: exI intro: Fields.has_fields_rec)
next
case has_fields_Object thus ?case unfolding sees_field_def
by(fastforce dest: map_of_SomeD intro: Fields.has_fields_Object intro!: exI)
qed
qed
subsection "Functional lookup"
definition "method" :: "'m prog ⇒ cname ⇒ mname ⇒ cname × ty list × ty × 'm option"
where "method P C M ≡ THE (D,Ts,T,m). P ⊢ C sees M:Ts → T = m in D"
definition field :: "'m prog ⇒ cname ⇒ vname ⇒ cname × ty × fmod"
where "field P C F ≡ THE (D,T,fm). P ⊢ C sees F:T (fm) in D"
definition fields :: "'m prog ⇒ cname ⇒ ((vname × cname) × (ty × fmod)) list"
where "fields P C ≡ THE FDTs. P ⊢ C has_fields FDTs"
lemma [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:T (fm) in D ⟹ field P C F = (D,T,fm)"
by (unfold field_def) (auto dest: sees_field_fun)
lemma method_def2 [simp]: "P ⊢ C sees M: Ts→T = m in D ⟹ method P C M = (D,Ts,T,m)"
by (unfold method_def) (auto dest: sees_method_fun)
lemma has_fields_b_fields:
"P ⊢ C has_fields FDTs ⟹ fields P C = FDTs"
unfolding fields_def
by (blast intro: the_equality has_fields_fun)
lemma has_field_map_of_fields [simp]:
"P ⊢ C has F:T (fm) in D ⟹ map_of (fields P C) (F, D) = ⌊(T, fm)⌋"
by(auto simp add: has_field_def)
subsection ‹Code generation›
text ‹New introduction rules for subcls1›
code_pred
(modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
subcls1
.
text ‹
Introduce proper constant ‹subcls'› for @{term "subcls"}
and generate executable equation for ‹subcls'›
›
definition subcls' where "subcls' = subcls"
code_pred
(modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
[inductify]
subcls'
.
lemma subcls_conv_subcls' [code_unfold]:
"(subcls1 P)^** = subcls' P"
by(simp add: subcls'_def)
text ‹
Change rule @{thm widen_array_object} such that predicate compiler
tests on class @{term Object} first. Otherwise ‹widen_i_o_i› never terminates.
›
lemma widen_array_object_code:
"C = Object ⟹ P ⊢ Array A ≤ Class C"
by(auto intro: widen.intros)
lemmas [code_pred_intro] =
widen_refl widen_subcls widen_null widen_null_array widen_array_object_code widen_array_array
code_pred
(modes: i ⇒ i ⇒ i ⇒ bool)
widen
by(erule widen.cases) auto
text ‹
Readjust the code equations for @{term widen} such that @{term widen_i_i_i} is guaranteed to
contain @{term "()"} at most once (even in the code representation!). This is important
for the scheduler and the small-step semantics because of the weaker code equations
for @{term "the"}.
A similar problem cannot hit the subclass relation because, for acyclic subclass hierarchies,
the paths in the hieararchy are unique and cycle-free.
›
definition widen_i_i_i' where "widen_i_i_i' = widen_i_i_i"
declare widen.equation [code del]
lemmas widen_i_i_i'_equation [code] = widen.equation[folded widen_i_i_i'_def]
lemma widen_i_i_i_code [code]:
"widen_i_i_i P T T' = (if P ⊢ T ≤ T' then Predicate.single () else bot)"
by(auto intro!: pred_eqI intro: widen_i_i_iI elim: widen_i_i_iE)
code_pred
(modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
Methods
.
code_pred
(modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ i ⇒ bool)
[inductify]
Method
.
code_pred
(modes: i ⇒ i ⇒ i ⇒ bool)
[inductify]
has_method
.
declare fun_upd_def [code_pred_inline]
code_pred
(modes: i ⇒ i ⇒ o ⇒ bool)
Fields
.
code_pred
(modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ i ⇒ bool)
[inductify, skip_proof]
has_field
.