header {* \isaheader{Relations between Jinja Types} *}
theory TypeRel imports Decl begin
subsection{* The subclass relations *}
inductive_set
subcls1 :: "'m prog => (cname × cname) set"
and subcls1' :: "'m prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>1 _" [71,71,71] 70)
for P :: "'m prog"
where
"P \<turnstile> C \<prec>1 D ≡ (C,D) ∈ subcls1 P"
| subcls1I: "[|class P C = Some (D,rest); C ≠ Object|] ==> P \<turnstile> C \<prec>1 D"
abbreviation
subcls :: "'m prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>* _" [71,71,71] 70)
where "P \<turnstile> C \<preceq>* D ≡ (C,D) ∈ (subcls1 P)*"
lemma subcls1D: "P \<turnstile> C \<prec>1 D ==> C ≠ Object ∧ (∃fs ms. class P C = Some (D,fs,ms))"
by(erule subcls1.induct)(fastsimp simp add:is_class_def)
lemma [iff]: "¬ P \<turnstile> Object \<prec>1 C"
by(fastsimp dest:subcls1D)
lemma [iff]: "(P \<turnstile> Object \<preceq>* C) = (C = Object)"
apply(rule iffI)
apply(erule converse_rtranclE)
apply simp_all
done
lemma subcls1_def2:
"subcls1 P =
(SIGMA C:{C. is_class P C}. {D. C≠Object ∧ fst (the (class P C))=D})"
by (fastsimp simp:is_class_def dest: subcls1D elim: subcls1I)
lemma finite_subcls1: "finite (subcls1 P)"
apply (simp add: subcls1_def2)
apply(rule finite_SigmaI [OF finite_is_class])
apply(rule_tac B = "{fst (the (class P C))}" in finite_subset)
apply auto
done
subsection{* The subtype relations *}
inductive
widen :: "'m prog => ty => ty => bool" ("_ \<turnstile> _ ≤ _" [71,71,71] 70)
for P :: "'m prog"
where
widen_refl[iff]: "P \<turnstile> T ≤ T"
| widen_subcls: "P \<turnstile> C \<preceq>* D ==> P \<turnstile> Class C ≤ Class D"
| widen_null[iff]: "P \<turnstile> NT ≤ Class C"
abbreviation (xsymbols)
widens :: "'m prog => ty list => ty list => bool"
("_ \<turnstile> _ [≤] _" [71,71,71] 70) where
"widens P Ts Ts' ≡ list_all2 (widen P) Ts Ts'"
lemma [iff]: "(P \<turnstile> T ≤ Void) = (T = Void)"
by (auto elim: widen.cases)
lemma [iff]: "(P \<turnstile> T ≤ Boolean) = (T = Boolean)"
by (auto elim: widen.cases)
lemma [iff]: "(P \<turnstile> T ≤ Integer) = (T = Integer)"
by (auto elim: widen.cases)
lemma [iff]: "(P \<turnstile> Void ≤ T) = (T = Void)"
by (auto elim: widen.cases)
lemma [iff]: "(P \<turnstile> Boolean ≤ T) = (T = Boolean)"
by (auto elim: widen.cases)
lemma [iff]: "(P \<turnstile> Integer ≤ T) = (T = Integer)"
by (auto elim: widen.cases)
lemma Class_widen: "P \<turnstile> Class C ≤ T ==> ∃D. T = Class D"
apply (ind_cases "P \<turnstile> Class C ≤ T")
apply auto
done
lemma [iff]: "(P \<turnstile> T ≤ NT) = (T = NT)"
apply(cases T)
apply(auto dest:Class_widen)
done
lemma Class_widen_Class [iff]: "(P \<turnstile> Class C ≤ Class D) = (P \<turnstile> C \<preceq>* D)"
apply (rule iffI)
apply (ind_cases "P \<turnstile> Class C ≤ Class D")
apply (auto elim: widen_subcls)
done
lemma widen_Class: "(P \<turnstile> T ≤ Class C) = (T = NT ∨ (∃D. T = Class D ∧ P \<turnstile> D \<preceq>* C))"
by(induct T, auto)
lemma widen_trans[trans]: "[|P \<turnstile> S ≤ U; P \<turnstile> U ≤ T|] ==> P \<turnstile> S ≤ T"
proof -
assume "P\<turnstile>S ≤ U" thus "!!T. P \<turnstile> U ≤ T ==> P \<turnstile> S ≤ T"
proof induct
case (widen_refl T T') thus "P \<turnstile> 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 \<turnstile> 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 \<turnstile> NT ≤ RT" by auto
qed
qed
lemma widens_trans [trans]: "[|P \<turnstile> Ss [≤] Ts; P \<turnstile> Ts [≤] Us|] ==> P \<turnstile> Ss [≤] Us"
by (rule list_all2_trans, rule widen_trans)
lemmas widens_refl [iff] = list_all2_refl [of "widen P", OF widen_refl, standard]
lemmas widens_Cons [iff] = list_all2_Cons1 [of "widen P", standard]
subsection{* Method lookup *}
inductive
Methods :: "['m prog, cname, mname \<rightharpoonup> (ty list × ty × 'm) × cname] => bool"
("_ \<turnstile> _ sees'_methods _" [51,51,51] 50)
for P :: "'m prog"
where
sees_methods_Object:
"[| class P Object = Some(D,fs,ms); Mm = Option.map (λm. (m,Object)) o map_of ms |]
==> P \<turnstile> Object sees_methods Mm"
| sees_methods_rec:
"[| class P C = Some(D,fs,ms); C ≠ Object; P \<turnstile> D sees_methods Mm;
Mm' = Mm ++ (Option.map (λm. (m,C)) o map_of ms) |]
==> P \<turnstile> C sees_methods Mm'";
lemma sees_methods_fun:
assumes 1: "P \<turnstile> C sees_methods Mm"
shows "!!Mm'. P \<turnstile> 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 \<turnstile> D sees_methods Dres"
and IH: "!!Dres'. P \<turnstile> D sees_methods Dres' ==> Dres' = Dres"
and Cres: "Cres = Dres ++ (Option.map (λm. (m,C)) o map_of ms)"
and Cmethods': "P \<turnstile> C sees_methods Cres'" by fact+
from Cmethods' notObj "class" obtain Dres'
where Dmethods': "P \<turnstile> D sees_methods Dres'"
and Cres': "Cres' = Dres' ++ (Option.map (λm. (m,C)) o 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 \<turnstile> 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 \<turnstile> C sees_methods Mm"
shows "Mm M = Some(m,D) ==> P \<turnstile> C \<preceq>* D"
using Csees
proof induct
case sees_methods_Object thus ?case by auto
next
case sees_methods_rec thus ?case
by(fastsimp simp:Option.map_def split:option.splits
elim:converse_rtrancl_into_rtrancl[OF subcls1I])
qed
lemma sees_methods_idemp:
assumes Cmethods: "P \<turnstile> C sees_methods Mm"
shows "!!m D. Mm M = Some(m,D) ==>
∃Mm'. (P \<turnstile> D sees_methods Mm') ∧ Mm' M = Some(m,D)"
using Cmethods
proof induct
case sees_methods_Object thus ?case
by(fastsimp dest: Methods.sees_methods_Object)
next
case sees_methods_rec thus ?case
by(fastsimp split:option.splits dest: Methods.sees_methods_rec)
qed
lemma sees_methods_decl_mono:
assumes sub: "P \<turnstile> C' \<preceq>* C"
shows "P \<turnstile> C sees_methods Mm ==>
∃Mm' Mm2. P \<turnstile> C' sees_methods Mm' ∧ Mm' = Mm ++ Mm2 ∧
(∀M m D. Mm2 M = Some(m,D) --> P \<turnstile> D \<preceq>* C)"
(is "_ ==> ∃Mm' Mm2. ?Q C' C Mm' Mm2")
using sub
proof (induct rule:converse_rtrancl_induct)
assume "P \<turnstile> C sees_methods Mm"
hence "?Q C C Mm empty" by simp
thus "∃Mm' Mm2. ?Q C C Mm' Mm2" by blast
next
fix C'' C'
assume sub1: "P \<turnstile> C'' \<prec>1 C'" and sub: "P \<turnstile> C' \<preceq>* C"
and IH: "P \<turnstile> C sees_methods Mm ==>
∃Mm' Mm2. P \<turnstile> C' sees_methods Mm' ∧
Mm' = Mm ++ Mm2 ∧ (∀M m D. Mm2 M = Some(m,D) --> P \<turnstile> D \<preceq>* C)"
and Csees: "P \<turnstile> C sees_methods Mm"
from IH[OF Csees] obtain Mm' Mm2 where C'sees: "P \<turnstile> C' sees_methods Mm'"
and Mm': "Mm' = Mm ++ Mm2"
and subC:"∀M m D. Mm2 M = Some(m,D) --> P \<turnstile> D \<preceq>* 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 = "Option.map (λm. (m,C'')) o map_of ms"
have "P \<turnstile> 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
constdefs
Method :: "'m prog => cname => mname => ty list => ty => 'm => cname => bool"
("_ \<turnstile> _ sees _: _->_ = _ in _" [51,51,51,51,51,51,51] 50)
"P \<turnstile> C sees M: Ts->T = m in D ≡
∃Mm. P \<turnstile> C sees_methods Mm ∧ Mm M = Some((Ts,T,m),D)"
has_method :: "'m prog => cname => mname => bool" ("_ \<turnstile> _ has _" [51,0,51] 50)
"P \<turnstile> C has M ≡ ∃Ts T m D. P \<turnstile> C sees M:Ts->T = m in D"
lemma sees_method_fun:
"[|P \<turnstile> C sees M:TS->T = m in D; P \<turnstile> C sees M:TS'->T' = m' in D' |]
==> TS' = TS ∧ T' = T ∧ m' = m ∧ D' = D"
by(fastsimp dest: sees_methods_fun simp:Method_def)
lemma sees_method_decl_above:
"P \<turnstile> C sees M:Ts->T = m in D ==> P \<turnstile> C \<preceq>* D"
by(clarsimp simp:Method_def sees_methods_decl_above)
lemma visible_method_exists:
"P \<turnstile> 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(fastsimp simp:Method_def dest!: visible_methods_exist)
lemma sees_method_idemp:
"P \<turnstile> C sees M:Ts->T=m in D ==> P \<turnstile> D sees M:Ts->T=m in D"
by(fastsimp simp: Method_def intro:sees_methods_idemp)
lemma sees_method_decl_mono:
"[| P \<turnstile> C' \<preceq>* C; P \<turnstile> C sees M:Ts->T = m in D;
P \<turnstile> C' sees M:Ts'->T' = m' in D' |] ==> P \<turnstile> D' \<preceq>* 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:rtrancl_trans)
done
lemma sees_method_is_class:
"[| P \<turnstile> C sees M:Ts->T = m in D |] ==> is_class P C"
by (auto simp add: is_class_def Method_def elim: Methods.induct)
subsection{* Field lookup *}
inductive
Fields :: "['m prog, cname, ((vname × cname) × ty) list] => bool"
("_ \<turnstile> _ has'_fields _" [51,51,51] 50)
for P :: "'m prog"
where
has_fields_rec:
"[| class P C = Some(D,fs,ms); C ≠ Object; P \<turnstile> D has_fields FDTs;
FDTs' = map (λ(F,T). ((F,C),T)) fs @ FDTs |]
==> P \<turnstile> C has_fields FDTs'"
| has_fields_Object:
"[| class P Object = Some(D,fs,ms); FDTs = map (λ(F,T). ((F,Object),T)) fs |]
==> P \<turnstile> Object has_fields FDTs"
lemma has_fields_fun:
assumes 1: "P \<turnstile> C has_fields FDTs"
shows "!!FDTs'. P \<turnstile> 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 \<turnstile> D has_fields Dres"
and IH: "!!Dres'. P \<turnstile> D has_fields Dres' ==> Dres' = Dres"
and Cres: "Cres = map (λ(F,T). ((F,C),T)) fs @ Dres"
and CFields': "P \<turnstile> C has_fields Cres'" by fact+
from CFields' notObj "class" obtain Dres'
where DFields': "P \<turnstile> D has_fields Dres'"
and Cres': "Cres' = map (λ(F,T). ((F,C),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 \<turnstile> C has_fields FDTs"
shows "[| P \<turnstile> C \<preceq>* D; class P D = Some(D',fs,ms); (F,T) ∈ set fs |]
==> ((F,D),T) ∈ set FDTs"
using sub apply(induct)
apply(simp add:image_def)
apply(erule converse_rtranclE)
apply(force)
apply(drule subcls1D)
apply fastsimp
apply(force simp:image_def)
done
lemma has_fields_decl_above:
assumes fields: "P \<turnstile> C has_fields FDTs"
shows "((F,D),T) ∈ set FDTs ==> P \<turnstile> C \<preceq>* D"
using fields apply(induct)
prefer 2 apply fastsimp
apply clarsimp
apply(erule disjE)
apply(clarsimp simp add:image_def)
apply simp
apply(blast dest:subcls1I converse_rtrancl_into_rtrancl)
done
lemma subcls_notin_has_fields:
assumes fields: "P \<turnstile> C has_fields FDTs"
shows "((F,D),T) ∈ set FDTs ==> (D,C) ∉ (subcls1 P)+"
using fields apply(induct)
prefer 2 apply(fastsimp dest: tranclD)
apply clarsimp
apply(erule disjE)
apply(clarsimp simp add:image_def)
apply(drule tranclD)
apply clarify
apply(frule subcls1D)
apply(fastsimp dest:all_fields_in_has_fields)
apply simp
apply(blast dest:subcls1I trancl_into_trancl)
done
lemma has_fields_mono_lem:
assumes sub: "P \<turnstile> D \<preceq>* C"
shows "P \<turnstile> C has_fields FDTs
==> ∃pre. P \<turnstile> D has_fields pre@FDTs ∧ dom(map_of pre) ∩ dom(map_of FDTs) = {}"
using sub apply(induct rule:converse_rtrancl_induct)
apply(rule_tac x = "[]" in exI)
apply simp
apply clarsimp
apply(rename_tac D' D pre)
apply(subgoal_tac "(D',C) : (subcls1 P)^+")
prefer 2 apply(erule (1) rtrancl_into_trancl2)
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,T). ((F,D'),T)) 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 image_def)
done
constdefs
has_field :: "'m prog => cname => vname => ty => cname => bool"
("_ \<turnstile> _ has _:_ in _" [51,51,51,51,51] 50)
"P \<turnstile> C has F:T in D ≡
∃FDTs. P \<turnstile> C has_fields FDTs ∧ map_of FDTs (F,D) = Some T"
lemma has_field_mono:
"[| P \<turnstile> C has F:T in D; P \<turnstile> C' \<preceq>* C |] ==> P \<turnstile> C' has F:T in D"
apply(clarsimp simp:has_field_def)
apply(drule (1) has_fields_mono_lem)
apply(fastsimp simp: map_add_def split:option.splits)
done
constdefs
sees_field :: "'m prog => cname => vname => ty => cname => bool"
("_ \<turnstile> _ sees _:_ in _" [51,51,51,51,51] 50)
"P \<turnstile> C sees F:T in D ≡
∃FDTs. P \<turnstile> C has_fields FDTs ∧
map_of (map (λ((F,D),T). (F,(D,T))) FDTs) F = Some(D,T)"
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: split_if_asm)
lemma has_visible_field:
"P \<turnstile> C sees F:T in D ==> P \<turnstile> C has F:T in D"
by(auto simp add:has_field_def sees_field_def map_of_remap_SomeD)
lemma sees_field_fun:
"[|P \<turnstile> C sees F:T in D; P \<turnstile> C sees F:T' in D'|] ==> T' = T ∧ D' = D"
by(fastsimp simp:sees_field_def dest:has_fields_fun)
lemma sees_field_decl_above:
"P \<turnstile> C sees F:T in D ==> P \<turnstile> C \<preceq>* D"
apply(auto simp:sees_field_def)
apply(blast intro: has_fields_decl_above map_of_SomeD map_of_remap_SomeD)
done
lemma sees_field_idemp:
"P \<turnstile> C sees F:T in D ==> P \<turnstile> D sees F:T in D"
apply (unfold sees_field_def)
apply clarsimp
apply (rule_tac P = "map_of ?xs F = ?y" in mp)
prefer 2
apply assumption
apply (thin_tac "map_of ?xs F = ?y")
apply (erule Fields.induct)
apply clarsimp
apply (frule map_of_SomeD)
apply clarsimp
apply (fastsimp intro: has_fields_rec)
apply clarsimp
apply (frule map_of_SomeD)
apply clarsimp
apply (fastsimp intro: has_fields_Object)
done
subsection "Functional lookup"
constdefs
method :: "'m prog => cname => mname => cname × ty list × ty × 'm"
"method P C M ≡ THE (D,Ts,T,m). P \<turnstile> C sees M:Ts -> T = m in D"
field :: "'m prog => cname => vname => cname × ty"
"field P C F ≡ THE (D,T). P \<turnstile> C sees F:T in D"
fields :: "'m prog => cname => ((vname × cname) × ty) list"
"fields P C ≡ THE FDTs. P \<turnstile> C has_fields FDTs"
lemma fields_def2 [simp]: "P \<turnstile> C has_fields FDTs ==> fields P C = FDTs"
by (unfold fields_def) (auto dest: has_fields_fun)
lemma field_def2 [simp]: "P \<turnstile> C sees F:T in D ==> field P C F = (D,T)"
by (unfold field_def) (auto dest: sees_field_fun)
lemma method_def2 [simp]: "P \<turnstile> 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)
end