Theory 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
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 ⇀ (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
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
definition Method :: "'m prog ⇒ cname ⇒ mname ⇒ ty list ⇒ ty ⇒ 'm ⇒ 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)"
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 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:
assumes sub: "P ⊢ C' ≼⇧* C" and
C_sees: "P ⊢ C sees M:Ts→T=m in D" and
C'_sees: "P ⊢ C' sees M: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 = ⌊((Ts', T', m'), D')⌋"
using C'_sees sees_methods_fun[OF Ms'] Ms'_def by(clarsimp simp: Method_def)
then have "Ms2 M = ⌊((Ts', T', m'), D')⌋ ∨
Ms2 M = None ∧ 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 = ⌊((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_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.induct)
subsection‹Field lookup›
inductive
Fields :: "['m prog, cname, ((vname × cname) × 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,T). ((F,C),T)) 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 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,T). ((F,C),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,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 ⊢ C has_fields FDTs"
shows "⟦ P ⊢ C ≼⇧* D; class P D = Some(D',fs,ms); (F,T) ∈ set fs ⟧
⟹ ((F,D),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),T) ∈ set FDTs ⟹ P ⊢ C ≼⇧* D"
using fields proof(induct)
case (has_fields_rec C D' fs ms FDTs FDTs')
then have "((F, D), T) ∈ (λx. case x of (F, x) ⇒ ((F, C), x)) ` set fs ∨
((F, D), T) ∈ set FDTs" by clarsimp
then show ?case proof(rule disjE)
assume "((F, D), 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), 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),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), T) ∈ (λx. case x of (F, x) ⇒ ((F, C), x)) ` set fs
∨ ((F, D), T) ∈ set FDTs" by clarsimp
then show ?case proof(rule disjE)
assume "((F, D), T) ∈ (λx. case x of (F, x) ⇒ ((F, C), x)) ` set fs"
then have CD[simp]: "C = D" and fs: "(F, 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), 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), 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 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,T). ((F,D'),T)) fs @ pre" in exI) simp
qed
definition has_field :: "'m prog ⇒ cname ⇒ vname ⇒ ty ⇒ cname ⇒ bool"
("_ ⊢ _ has _:_ in _" [51,51,51,51,51] 50)
where
"P ⊢ C has F:T in D ≡
∃FDTs. P ⊢ C has_fields FDTs ∧ map_of FDTs (F,D) = Some T"
lemma has_field_mono:
assumes has: " P ⊢ C has F:T in D" and sub: "P ⊢ C' ≼⇧* C"
shows "P ⊢ C' has F:T in D"
proof -
obtain FDTs where FDTs:"P ⊢ C has_fields FDTs" and "map_of FDTs (F, D) = ⌊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
definition sees_field :: "'m prog ⇒ cname ⇒ vname ⇒ ty ⇒ cname ⇒ bool"
("_ ⊢ _ sees _:_ in _" [51,51,51,51,51] 50)
where
"P ⊢ C sees F:T in D ≡
∃FDTs. P ⊢ 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: if_split_asm)
lemma has_visible_field:
"P ⊢ C sees F:T in D ⟹ P ⊢ 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 ⊢ C sees F:T in D; P ⊢ C sees F:T' in D'⟧ ⟹ T' = T ∧ D' = D"
by(fastforce simp:sees_field_def dest:has_fields_fun)
lemma sees_field_decl_above:
"P ⊢ C sees F:T in D ⟹ P ⊢ C ≼⇧* D"
by(auto simp:sees_field_def
intro: has_fields_decl_above map_of_SomeD map_of_remap_SomeD)
lemma sees_field_idemp:
assumes sees: "P ⊢ C sees F:T in D"
shows "P ⊢ D sees F:T in D"
proof -
obtain FDTs where C_flds: "P ⊢ C has_fields FDTs"
and FDTs: "map_of (map (λ((F, D), T). (F, D, T)) FDTs) F = ⌊(D, 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, T)⌋ ⟹ C' = D ∧ (F, T) ∈ set fs"
by(frule map_of_SomeD) clarsimp
have "?FDTs ⟶ P ⊢ D sees F:T in D"
using C_flds proof induct
case NObj: has_fields_rec
then show ?case using map by (fastforce intro: has_fields_rec simp: sees_field_def)
next
case Obj: has_fields_Object
then show ?case using map by(fastforce intro: has_fields_Object simp: sees_field_def)
qed
then show ?thesis using FDTs by(rule mp)
qed
subsection "Functional lookup"
definition "method" :: "'m prog ⇒ cname ⇒ mname ⇒ cname × ty list × ty × 'm"
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"
where
"field P C F ≡ THE (D,T). P ⊢ C sees F:T in D"
definition fields :: "'m prog ⇒ cname ⇒ ((vname × cname) × 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:T in D ⟹ field P C F = (D,T)"
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)
subsection "Code generator setup"
code_pred
(modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
subcls1p
.
declare subcls1_def [code_pred_def]
code_pred
(modes: i ⇒ i × o ⇒ bool, i ⇒ i × i ⇒ bool)
[inductify]
subcls1
.
definition subcls' where "subcls' G = (subcls1p G)^**"
code_pred
(modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
[inductify]
subcls'
.
lemma subcls_conv_subcls' [code_unfold]:
"(subcls1 G)^* = {(C, D). subcls' G C D}"
by (simp add: subcls'_def subcls1_def rtrancl_def)
code_pred
(modes: i ⇒ i ⇒ i ⇒ bool)
widen
.
code_pred
(modes: i ⇒ i ⇒ o ⇒ bool)
Fields
.
lemma has_field_code [code_pred_intro]:
"⟦ P ⊢ C has_fields FDTs; map_of FDTs (F, D) = ⌊T⌋ ⟧
⟹ P ⊢ C has F:T in D"
by(auto simp add: has_field_def)
code_pred
(modes: i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
has_field
by(auto simp add: has_field_def)
lemma sees_field_code [code_pred_intro]:
"⟦ P ⊢ C has_fields FDTs; map_of (map (λ((F, D), T). (F, D, T)) FDTs) F = ⌊(D, T)⌋ ⟧
⟹ P ⊢ C sees F:T in D"
by(auto simp add: sees_field_def)
code_pred
(modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ bool,
i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
sees_field
by(auto simp add: sees_field_def)
code_pred
(modes: i ⇒ i ⇒ o ⇒ bool)
Methods
.
lemma Method_code [code_pred_intro]:
"⟦ P ⊢ C sees_methods Mm; Mm M = ⌊((Ts, T, m), D)⌋ ⟧
⟹ P ⊢ C sees M: Ts→T = m in D"
by(auto simp add: Method_def)
code_pred
(modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ o ⇒ bool,
i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
Method
by(auto simp add: Method_def)
lemma eval_Method_i_i_i_o_o_o_o_conv:
"Predicate.eval (Method_i_i_i_o_o_o_o P C M) = (λ(Ts, T, m, D). P ⊢ C sees M:Ts→T=m in D)"
by(auto intro: Method_i_i_i_o_o_o_oI elim: Method_i_i_i_o_o_o_oE intro!: ext)
lemma method_code [code]:
"method P C M =
Predicate.the (Predicate.bind (Method_i_i_i_o_o_o_o P C M) (λ(Ts, T, m, D). Predicate.single (D, Ts, T, m)))"
apply (rule sym, rule the_eqI)
apply (simp add: method_def eval_Method_i_i_i_o_o_o_o_conv)
apply (rule arg_cong [where f=The])
apply (auto simp add: Sup_fun_def Sup_bool_def fun_eq_iff)
done
lemma eval_Fields_conv:
"Predicate.eval (Fields_i_i_o P C) = (λFDTs. P ⊢ C has_fields FDTs)"
by(auto intro: Fields_i_i_oI elim: Fields_i_i_oE intro!: ext)
lemma fields_code [code]:
"fields P C = Predicate.the (Fields_i_i_o P C)"
by(simp add: fields_def Predicate.the_def eval_Fields_conv)
lemma eval_sees_field_i_i_i_o_o_conv:
"Predicate.eval (sees_field_i_i_i_o_o P C F) = (λ(T, D). P ⊢ C sees F:T in D)"
by(auto intro!: ext intro: sees_field_i_i_i_o_oI elim: sees_field_i_i_i_o_oE)
lemma eval_sees_field_i_i_i_o_i_conv:
"Predicate.eval (sees_field_i_i_i_o_i P C F D) = (λT. P ⊢ C sees F:T in D)"
by(auto intro!: ext intro: sees_field_i_i_i_o_iI elim: sees_field_i_i_i_o_iE)
lemma field_code [code]:
"field P C F = Predicate.the (Predicate.bind (sees_field_i_i_i_o_o P C F) (λ(T, D). Predicate.single (D, T)))"
apply (rule sym, rule the_eqI)
apply (simp add: field_def eval_sees_field_i_i_i_o_o_conv)
apply (rule arg_cong [where f=The])
apply (auto simp add: Sup_fun_def Sup_bool_def fun_eq_iff)
done
end