header {* \isaheader{The Jinja Type System as a Semilattice} *}
theory SemiType
imports "../Common/WellForm" "../DFA/Semilattices"
begin
definition super :: "'a prog => cname => cname"
where "super P C ≡ fst (the (class P C))"
lemma superI:
"(C,D) ∈ subcls1 P ==> super P C = D"
by (unfold super_def) (auto dest: subcls1D)
primrec the_Class :: "ty => cname"
where
"the_Class (Class C) = C"
definition sup :: "'c prog => ty => ty => ty err"
where
"sup P T⇣1 T⇣2 ≡
if is_refT T⇣1 ∧ is_refT T⇣2 then
OK (if T⇣1 = NT then T⇣2 else
if T⇣2 = NT then T⇣1 else
(Class (exec_lub (subcls1 P) (super P) (the_Class T⇣1) (the_Class T⇣2))))
else
(if T⇣1 = T⇣2 then OK T⇣1 else Err)"
lemma sup_def':
"sup P = (λT⇣1 T⇣2.
if is_refT T⇣1 ∧ is_refT T⇣2 then
OK (if T⇣1 = NT then T⇣2 else
if T⇣2 = NT then T⇣1 else
(Class (exec_lub (subcls1 P) (super P) (the_Class T⇣1) (the_Class T⇣2))))
else
(if T⇣1 = T⇣2 then OK T⇣1 else Err))"
by (simp add: sup_def fun_eq_iff)
abbreviation
subtype :: "'c prog => ty => ty => bool"
where "subtype P ≡ widen P"
definition esl :: "'c prog => ty esl"
where
"esl P ≡ (types P, subtype P, sup P)"
lemma is_class_is_subcls:
"wf_prog m P ==> is_class P C = P \<turnstile> C \<preceq>⇧* Object"
by (fastforce simp:is_class_def
elim: subcls_C_Object converse_rtranclE subcls1I
dest: subcls1D)
lemma subcls_antisym:
"[|wf_prog m P; P \<turnstile> C \<preceq>⇧* D; P \<turnstile> D \<preceq>⇧* C|] ==> C = D"
by (auto dest: acyclic_subcls1 acyclic_impl_antisym_rtrancl antisymD)
lemma widen_antisym:
"[| wf_prog m P; P \<turnstile> T ≤ U; P \<turnstile> U ≤ T |] ==> T = U"
apply (cases T)
apply (cases U)
apply auto
apply (cases U)
apply (auto elim!: subcls_antisym)
done
lemma order_widen [intro,simp]:
"wf_prog m P ==> order (subtype P)"
apply (unfold Semilat.order_def lesub_def)
apply (auto intro: widen_trans widen_antisym)
done
lemma NT_widen:
"P \<turnstile> NT ≤ T = (T = NT ∨ (∃C. T = Class C))"
by (cases T) auto
lemma Class_widen2: "P \<turnstile> Class C ≤ T = (∃D. T = Class D ∧ P \<turnstile> C \<preceq>⇧* D)"
by (cases T) auto
lemma wf_converse_subcls1_impl_acc_subtype:
"wf ((subcls1 P)^-1) ==> acc (subtype P)"
apply (unfold Semilat.acc_def lesssub_def)
apply (drule_tac p = "(subcls1 P)^-1 - Id" in wf_subset)
apply blast
apply (drule wf_trancl)
apply (simp add: wf_eq_minimal)
apply clarify
apply (unfold lesub_def)
apply (rename_tac M T)
apply (case_tac "EX C. Class C : M")
prefer 2
apply (case_tac T)
apply fastforce
apply fastforce
apply fastforce
apply simp
apply (rule_tac x = NT in bexI)
apply (rule allI)
apply (rule impI, erule conjE)
apply (clarsimp simp add: NT_widen)
apply simp
apply clarsimp
apply (erule_tac x = "{C. Class C : M}" in allE)
apply auto
apply (rename_tac D)
apply (rule_tac x = "Class D" in bexI)
prefer 2
apply assumption
apply clarify
apply (clarsimp simp: Class_widen2)
apply (insert rtrancl_r_diff_Id [symmetric, standard, of "subcls1 P"])
apply simp
apply (erule rtranclE)
apply blast
apply (drule rtrancl_converseI)
apply (subgoal_tac "((subcls1 P)-Id)^-1 = ((subcls1 P)^-1 - Id)")
prefer 2
apply blast
apply simp
apply (blast intro: rtrancl_into_trancl2)
done
lemma wf_subtype_acc [intro, simp]:
"wf_prog wf_mb P ==> acc (subtype P)"
by (rule wf_converse_subcls1_impl_acc_subtype, rule wf_subcls1)
lemma exec_lub_refl [simp]: "exec_lub r f T T = T"
by (simp add: exec_lub_def while_unfold)
lemma closed_err_types:
"wf_prog wf_mb P ==> closed (err (types P)) (lift2 (sup P))"
apply (unfold closed_def plussub_def lift2_def sup_def')
apply (frule acyclic_subcls1)
apply (frule single_valued_subcls1)
apply (auto simp: is_type_def is_refT_def is_class_is_subcls split: err.split ty.splits)
apply (blast dest!: is_lub_exec_lub is_lubD is_ubD intro!: is_ubI superI)
done
lemma sup_subtype_greater:
"[| wf_prog wf_mb P; is_type P t1; is_type P t2; sup P t1 t2 = OK s |]
==> subtype P t1 s ∧ subtype P t2 s"
proof -
assume wf_prog: "wf_prog wf_mb P"
{ fix c1 c2
assume is_class: "is_class P c1" "is_class P c2"
with wf_prog
obtain
"P \<turnstile> c1 \<preceq>⇧* Object"
"P \<turnstile> c2 \<preceq>⇧* Object"
by (blast intro: subcls_C_Object)
with single_valued_subcls1[OF wf_prog]
obtain u where
"is_lub ((subcls1 P)^* ) c1 c2 u"
by (blast dest: single_valued_has_lubs)
moreover
note acyclic_subcls1[OF wf_prog]
moreover
have "∀x y. (x, y) ∈ subcls1 P --> super P x = y"
by (blast intro: superI)
ultimately
have "P \<turnstile> c1 \<preceq>⇧* exec_lub (subcls1 P) (super P) c1 c2 ∧
P \<turnstile> c2 \<preceq>⇧* exec_lub (subcls1 P) (super P) c1 c2"
by (simp add: exec_lub_conv) (blast dest: is_lubD is_ubD)
} note this [simp]
assume "is_type P t1" "is_type P t2" "sup P t1 t2 = OK s"
thus ?thesis
apply (unfold sup_def)
apply (cases s)
apply (auto simp add: is_refT_def split: split_if_asm)
done
qed
lemma sup_subtype_smallest:
"[| wf_prog wf_mb P; is_type P a; is_type P b; is_type P c;
subtype P a c; subtype P b c; sup P a b = OK d |]
==> subtype P d c"
proof -
assume wf_prog: "wf_prog wf_mb P"
{ fix c1 c2 D
assume is_class: "is_class P c1" "is_class P c2"
assume le: "P \<turnstile> c1 \<preceq>⇧* D" "P \<turnstile> c2 \<preceq>⇧* D"
from wf_prog is_class
obtain
"P \<turnstile> c1 \<preceq>⇧* Object"
"P \<turnstile> c2 \<preceq>⇧* Object"
by (blast intro: subcls_C_Object)
with single_valued_subcls1[OF wf_prog]
obtain u where
lub: "is_lub ((subcls1 P)^* ) c1 c2 u"
by (blast dest: single_valued_has_lubs)
with acyclic_subcls1[OF wf_prog]
have "exec_lub (subcls1 P) (super P) c1 c2 = u"
by (blast intro: superI exec_lub_conv)
moreover
from lub le
have "P \<turnstile> u \<preceq>⇧* D"
by (simp add: is_lub_def is_ub_def)
ultimately
have "P \<turnstile> exec_lub (subcls1 P) (super P) c1 c2 \<preceq>⇧* D"
by blast
} note this [intro]
have [dest!]:
"!!C T. P \<turnstile> Class C ≤ T ==> ∃D. T=Class D ∧ P \<turnstile> C \<preceq>⇧* D"
by (frule Class_widen, auto)
assume "is_type P a" "is_type P b" "is_type P c"
"subtype P a c" "subtype P b c" "sup P a b = OK d"
thus ?thesis
by (auto simp add: sup_def is_refT_def
split: split_if_asm)
qed
lemma sup_exists:
"[| subtype P a c; subtype P b c |] ==> EX T. sup P a b = OK T"
apply (unfold sup_def)
apply (cases b)
apply auto
apply (cases a)
apply auto
apply (cases a)
apply auto
done
lemma err_semilat_JType_esl:
"wf_prog wf_mb P ==> err_semilat (esl P)"
proof -
assume wf_prog: "wf_prog wf_mb P"
hence "order (subtype P)"..
moreover from wf_prog
have "closed (err (types P)) (lift2 (sup P))"
by (rule closed_err_types)
moreover
from wf_prog have
"(∀x∈err (types P). ∀y∈err (types P). x \<sqsubseteq>⇘Err.le (subtype P)⇙ x \<squnion>⇘lift2 (sup P)⇙ y) ∧
(∀x∈err (types P). ∀y∈err (types P). y \<sqsubseteq>⇘Err.le (subtype P)⇙ x \<squnion>⇘lift2 (sup P)⇙ y)"
by (auto simp add: lesub_def plussub_def Err.le_def lift2_def sup_subtype_greater split: err.split)
moreover from wf_prog have
"∀x∈err (types P). ∀y∈err (types P). ∀z∈err (types P).
x \<sqsubseteq>⇘Err.le (subtype P)⇙ z ∧ y \<sqsubseteq>⇘Err.le (subtype P)⇙ z --> x \<squnion>⇘lift2 (sup P)⇙ y \<sqsubseteq>⇘Err.le (subtype P)⇙ z"
by (unfold lift2_def plussub_def lesub_def Err.le_def)
(auto intro: sup_subtype_smallest dest:sup_exists split: err.split)
ultimately show ?thesis by (simp add: esl_def semilat_def sl_def Err.sl_def)
qed
end