Theory SemiType
section ‹The Jinja Type System as a Semilattice›
theory SemiType
imports
WellForm
"../DFA/Semilattices"
begin
inductive_set
widen1 :: "'a prog ⇒ (ty × ty) set"
and widen1_syntax :: "'a prog ⇒ ty ⇒ ty ⇒ bool" (‹_ ⊢ _ <⇧1 _› [71,71,71] 70)
for P :: "'a prog"
where
"P ⊢ C <⇧1 D ≡ (C, D) ∈ widen1 P"
| widen1_Array_Object:
"P ⊢ Array (Class Object) <⇧1 Class Object"
| widen1_Array_Integer:
"P ⊢ Array Integer <⇧1 Class Object"
| widen1_Array_Boolean:
"P ⊢ Array Boolean <⇧1 Class Object"
| widen1_Array_Void:
"P ⊢ Array Void <⇧1 Class Object"
| widen1_Class:
"P ⊢ C ≺⇧1 D ⟹ P ⊢ Class C <⇧1 Class D"
| widen1_Array_Array:
"⟦ P ⊢ T <⇧1 U; ¬ is_NT_Array T ⟧ ⟹ P ⊢ Array T <⇧1 Array U"
abbreviation widen1_trancl :: "'a prog ⇒ ty ⇒ ty ⇒ bool" (‹_ ⊢ _ <⇧+ _› [71,71,71] 70) where
"P ⊢ T <⇧+ U ≡ (T, U) ∈ trancl (widen1 P)"
abbreviation widen1_rtrancl :: "'a prog ⇒ ty ⇒ ty ⇒ bool" (‹_ ⊢ _ <⇧* _› [71,71,71] 70) where
"P ⊢ T <⇧* U ≡ (T, U) ∈ rtrancl (widen1 P)"
inductive_simps widen1_simps1 [simp]:
"P ⊢ Integer <⇧1 T"
"P ⊢ Boolean <⇧1 T"
"P ⊢ Void <⇧1 T"
"P ⊢ Class Object <⇧1 T"
"P ⊢ NT <⇧1 U"
inductive_simps widen1_simps [simp]:
"P ⊢ Array (Class Object) <⇧1 T"
"P ⊢ Array Integer <⇧1 T"
"P ⊢ Array Boolean <⇧1 T"
"P ⊢ Array Void <⇧1 T"
"P ⊢ Class C <⇧1 T"
"P ⊢ T <⇧1 Array U"
lemma is_type_widen1:
assumes icO: "is_class P Object"
shows "P ⊢ T <⇧1 U ⟹ is_type P T"
by(induct rule: widen1.induct)(auto intro: subcls_is_class icO split: ty.split dest: is_type_ground_type)
lemma widen1_NT_Array:
assumes "is_NT_Array T"
shows "¬ P ⊢ T⌊⌉ <⇧1 U"
proof
assume "P ⊢ T⌊⌉ <⇧1 U" thus False using assms
by(induct "T⌊⌉" U arbitrary: T) auto
qed
lemma widen1_is_type:
assumes wfP: "wf_prog wfmd P"
shows "(A, B) ∈ widen1 P ⟹ is_type P B"
proof(induct rule: widen1.induct)
case (widen1_Class C D)
hence "is_class P C" "is_class P D"
by(auto intro: subcls_is_class converse_subcls_is_class[OF wfP])
thus ?case by simp
next
case (widen1_Array_Array T U)
thus ?case by(cases U)(auto elim: widen1.cases)
qed(insert wfP, auto)
lemma widen1_trancl_is_type:
assumes wfP: "wf_prog wfmd P"
shows "(A, B) ∈ (widen1 P)^+ ⟹ is_type P B"
apply(induct rule: trancl_induct)
apply(auto intro: widen1_is_type[OF wfP])
done
lemma single_valued_widen1:
assumes wf: "wf_prog wf_md P"
shows "single_valued (widen1 P)"
proof(rule single_valuedI)
fix x y z
assume "P ⊢ x <⇧1 y" "P ⊢ x <⇧1 z"
thus "y = z"
proof(induct arbitrary: z rule: widen1.induct)
case widen1_Class
with right_unique_subcls1[OF wf] show ?case
by (auto dest: right_uniqueD)
next
case (widen1_Array_Array T U z)
from ‹P ⊢ T⌊⌉ <⇧1 z› ‹P ⊢ T <⇧1 U› ‹¬ is_NT_Array T›
obtain z' where z': "z = z'⌊⌉" and Tz': "P ⊢ T <⇧1 z'"
by(auto elim: widen1.cases)
with ‹P ⊢ T <⇧1 z' ⟹ U = z'› have "U = z'" by blast
with z' show ?case by simp
qed simp_all
qed
function inheritance_level :: "'a prog ⇒ cname ⇒ nat" where
"inheritance_level P C =
(if acyclicP (subcls1 P) ∧ is_class P C ∧ C ≠ Object
then Suc (inheritance_level P (fst (the (class P C))))
else 0)"
by(pat_completeness, auto)
termination
proof(relation "same_fst (λP. acyclicP (subcls1 P)) (λP. {(C, C'). (subcls1 P)¯¯ C C'})")
show "wf (same_fst (λP. acyclicP (subcls1 P)) (λP. {(C, C'). (subcls1 P)¯¯ C C'}))"
by(rule wf_same_fst)(rule acyclicP_wf_subcls1[unfolded wfp_def])
qed(auto simp add: is_class_def intro: subcls1I)
fun subtype_measure :: "'a prog ⇒ ty ⇒ nat" where
"subtype_measure P (Class C) = inheritance_level P C"
| "subtype_measure P (Array T) = 1 + subtype_measure P T"
| "subtype_measure P T = 0"
lemma subtype_measure_measure:
assumes acyclic: "acyclicP (subcls1 P)"
and widen1: "P ⊢ x <⇧1 y"
shows "subtype_measure P y < subtype_measure P x"
using widen1
proof(induct rule: widen1.induct)
case (widen1_Class C D)
then obtain rest where "is_class P C" "C ≠ Object" "class P C = ⌊(D, rest)⌋"
by(auto elim!: subcls1.cases simp: is_class_def)
thus ?case using acyclic by(simp)
qed(simp_all)
lemma wf_converse_widen1:
assumes wfP: "wf_prog wfmc P"
shows "wf ((widen1 P)^-1)"
proof(rule wf_subset)
from wfP have "acyclicP (subcls1 P)" by(rule acyclic_subcls1)
thus "(widen1 P)¯ ⊆ measure (subtype_measure P)"
by(auto dest: subtype_measure_measure)
qed simp
fun super :: "'a prog ⇒ ty ⇒ ty"
where
"super P (Array Integer) = Class Object"
| "super P (Array Boolean) = Class Object"
| "super P (Array Void) = Class Object"
| "super P (Array (Class C)) = (if C = Object then Class Object else Array (super P (Class C)))"
| "super P (Array (Array T)) = Array (super P (Array T))"
| "super P (Class C) = Class (fst (the (class P C)))"
lemma superI:
"P ⊢ T <⇧1 U ⟹ super P T = U"
proof(induct rule: widen1.induct)
case (widen1_Array_Array T U)
thus ?case by(cases T) auto
qed(auto dest: subcls1D)
lemma Class_widen1_super:
"P ⊢ Class C' <⇧1 U' ⟷ is_class P C' ∧ C' ≠ Object ∧ U' = super P (Class C')"
(is "?lhs ⟷ ?rhs")
proof(rule iffI)
assume ?lhs thus ?rhs
by(auto intro: subcls_is_class simp add: superI simp del: super.simps)
next
assume ?rhs thus ?lhs
by(auto simp add: is_class_def intro: subcls1.intros)
qed
lemma super_widen1:
assumes icO: "is_class P Object"
shows "P ⊢ T <⇧1 U ⟷ is_type P T ∧ (case T of Class C ⇒ (C ≠ Object ∧ U = super P T)
| Array T' ⇒ U = super P T
| _ ⇒ False)"
proof(induct T arbitrary: U)
case Class thus ?case using Class_widen1_super by(simp)
next
case (Array T' U')
note IH = this
have "P ⊢ T'⌊⌉ <⇧1 U' = (is_type P (T'⌊⌉) ∧ U' = super P (T'⌊⌉))"
proof(rule iffI)
assume wd: "P ⊢ T'⌊⌉ <⇧1 U'"
with icO have "is_type P (T'⌊⌉)" by(rule is_type_widen1)
moreover from wd have "super P (T'⌊⌉) = U'" by(rule superI)
ultimately show "is_type P (T'⌊⌉) ∧ U' = super P (T'⌊⌉)" by simp
next
assume "is_type P (T'⌊⌉) ∧ U' = super P (T'⌊⌉)"
then obtain "is_type P (T'⌊⌉)" and U': "U' = super P (T'⌊⌉)" ..
thus "P ⊢ T'⌊⌉ <⇧1 U'"
proof(cases T')
case (Class D)
thus ?thesis using U' icO ‹is_type P (T'⌊⌉)›
by(cases "D = Object")(auto simp add: is_class_def intro: subcls1.intros)
next
case Array thus ?thesis
using IH ‹is_type P (T'⌊⌉)› U' by(auto simp add: ty.split_asm)
qed simp_all
qed
thus ?case by(simp)
qed(simp_all)
definition sup :: "'c prog ⇒ ty ⇒ ty ⇒ ty err" where
"sup P T U ≡
if is_refT T ∧ is_refT U
then OK (if U = NT then T
else if T = NT then U
else exec_lub (widen1 P) (super P) T U)
else if (T = U) then OK T else Err"
lemma sup_def':
"sup P = (λT U.
if is_refT T ∧ is_refT U
then OK (if U = NT then T
else if T = NT then U
else exec_lub (widen1 P) (super P) T U)
else if (T = U) then OK T else Err)"
by (simp add: fun_eq_iff sup_def)
definition esl :: "'m prog ⇒ ty esl"
where
"esl P = (types P, widen P, sup P)"
lemma order_widen [intro,simp]:
"wf_prog m P ⟹ order (widen P)"
unfolding Semilat.order_def lesub_def
by (auto intro: widen_trans widen_antisym)
lemma subcls1_trancl_widen1_trancl:
"(subcls1 P)^++ C D ⟹ P ⊢ Class C <⇧+ Class D"
by(induct rule: tranclp_induct[consumes 1, case_names base step])
(auto intro: trancl_into_trancl)
lemma subcls_into_widen1_rtrancl:
"P ⊢ C ≼⇧* D ⟹ P ⊢ Class C <⇧* Class D"
by(induct rule: rtranclp_induct)(auto intro: rtrancl_into_rtrancl)
lemma not_widen1_NT_Array:
"P ⊢ U <⇧1 T ⟹ ¬ is_NT_Array T"
by(induct rule: widen1.induct)(auto)
lemma widen1_trancl_into_Array_widen1_trancl:
"⟦ P ⊢ A <⇧+ B; ¬ is_NT_Array A ⟧ ⟹ P ⊢ A⌊⌉ <⇧+ B⌊⌉"
by(induct rule: converse_trancl_induct)
(auto intro: trancl_into_trancl2 widen1_Array_Array dest: not_widen1_NT_Array)
lemma widen1_rtrancl_into_Array_widen1_rtrancl:
"⟦ P ⊢ A <⇧* B; ¬ is_NT_Array A ⟧ ⟹ P ⊢ A⌊⌉ <⇧* B⌊⌉"
by(blast elim: rtranclE intro: trancl_into_rtrancl widen1_trancl_into_Array_widen1_trancl rtrancl_into_trancl1)
lemma Array_Object_widen1_trancl:
assumes wf: "wf_prog wmdc P"
and itA: "is_type P (A⌊⌉)"
shows "P ⊢ A⌊⌉ <⇧+ Class Object"
using itA
proof(induction A)
case (Class C)
hence "is_class P C" by simp
hence "P ⊢ C ≼⇧* Object" by(rule subcls_C_Object[OF _ wf])
hence "P ⊢ Class C <⇧* Class Object" by(rule subcls_into_widen1_rtrancl)
hence "P ⊢ Class C⌊⌉ <⇧* Class Object⌊⌉"
by(rule widen1_rtrancl_into_Array_widen1_rtrancl) simp
thus ?case by(rule rtrancl_into_trancl1) simp
next
case (Array A)
from ‹is_type P (A⌊⌉⌊⌉)› have "is_type P (A⌊⌉)" by(rule is_type_ArrayD)
hence "P ⊢ A⌊⌉ <⇧+ Class Object" by(rule Array.IH)
moreover from ‹is_type P (A⌊⌉⌊⌉)› have "¬ is_NT_Array (A⌊⌉)" by auto
ultimately have "P ⊢ A⌊⌉⌊⌉ <⇧+ Class Object⌊⌉"
by(rule widen1_trancl_into_Array_widen1_trancl)
thus ?case by(rule trancl_into_trancl) simp
qed auto
lemma widen_into_widen1_trancl:
assumes wf: "wf_prog wfmd P"
shows "⟦ P ⊢ A ≤ B; A ≠ B; A ≠ NT; is_type P A ⟧ ⟹ P ⊢ A <⇧+ B"
proof(induct rule: widen.induct)
case (widen_subcls C D)
from ‹Class C ≠ Class D› ‹P ⊢ C ≼⇧* D› have "(subcls1 P)⇧+⇧+ C D"
by(auto elim: rtranclp.cases intro: rtranclp_into_tranclp1)
thus ?case by(rule subcls1_trancl_widen1_trancl)
next
case widen_array_object thus ?case by(auto intro: Array_Object_widen1_trancl[OF wf])
next
case (widen_array_array A B)
hence "P ⊢ A <⇧+ B" by(cases A) auto
with ‹is_type P (A⌊⌉)› show ?case by(auto intro: widen1_trancl_into_Array_widen1_trancl)
qed(auto)
lemma wf_prog_impl_acc_widen:
assumes wfP: "wf_prog wfmd P"
shows "acc (types P) (widen P)"
proof -
from wf_converse_widen1[OF wfP]
have "wf (((widen1 P)^-1)^+)" by(rule wf_trancl)
hence wfw1t: "⋀M T. T ∈ M ⟹ (∃z∈M. ∀y. (y, z) ∈ ((widen1 P)¯)⇧+ ⟶ y ∉ M)"
by(auto simp only: wf_eq_minimal)
have "wf {(y, x). is_type P x ∧ is_type P y ∧ widen P x y ∧ x ≠ y}"
unfolding wf_eq_minimal
proof(intro strip)
fix M and T :: ty
assume TM: "T ∈ M"
show "∃z∈M. ∀y. (y, z) ∈ {(y, T). is_type P T ∧ is_type P y ∧ widen P T y ∧ T ≠ y} ⟶ y ∉ M"
proof(cases "(∃C. Class C ∈ M ∧ is_class P C) ∨ (∃U. U⌊⌉ ∈ M ∧ is_type P (U⌊⌉))")
case True
have BNTthesis: "⋀B. ⟦ B ∈ (M ∩ types P) - {NT} ⟧ ⟹ ?thesis"
proof -
fix B
assume BM: "B ∈ M ∩ types P - {NT}"
from wfw1t[OF BM] obtain z
where zM: "z ∈ M"
and znnt: "z ≠ NT"
and itz: "is_type P z"
and y: "⋀y. (y, z) ∈ ((widen1 P)¯)⇧+ ⟹ y ∉ M ∩ types P - {NT}" by blast
show "?thesis B"
proof(rule bexI[OF _ zM], rule allI, rule impI)
fix y
assume "(y, z) ∈ {(y, T). is_type P T ∧ is_type P y ∧ widen P T y ∧ T ≠ y}"
hence Pzy: "P ⊢ z ≤ y" and zy: "z ≠ y" and "is_type P y" by auto
hence "P ⊢ z <⇧+ y" using znnt itz
by -(rule widen_into_widen1_trancl[OF wfP])
hence ynM: "y ∉ M ∩ types P - {NT}"
by -(rule y, simp add: trancl_converse)
thus "y ∉ M" using Pzy znnt ‹is_type P y› by auto
qed
qed
from True show ?thesis by(fastforce intro: BNTthesis)
next
case False
hence not_is_class: "⋀C. Class C ∈ M ⟹ ¬ is_class P C"
and not_is_array: "⋀U. U⌊⌉ ∈ M ⟹ ¬ is_type P (U⌊⌉)" by simp_all
show ?thesis
proof(cases "∃C. Class C ∈ M")
case True
then obtain C where "Class C ∈ M" ..
with not_is_class[of C] show ?thesis
by(blast dest: rtranclpD subcls_is_class Class_widen)
next
case False
show ?thesis
proof(cases "∃T. Array T ∈ M")
case True
then obtain U where U: "Array U ∈ M" ..
hence "¬ is_type P (U⌊⌉)" by(rule not_is_array)
thus ?thesis using U by(auto simp del: is_type.simps)
next
case False
with ‹¬ (∃C. Class C ∈ M)› TM
have "∀y. P ⊢ T ≤ y ∧ T ≠ y ⟶ y ∉ M"
by(cases T)(fastforce simp add: NT_widen)+
thus ?thesis using TM by blast
qed
qed
qed
qed
thus ?thesis by(simp add: Semilat.acc_def lesssub_def lesub_def)
qed
lemmas wf_widen_acc = wf_prog_impl_acc_widen
declare wf_widen_acc [intro, simp]
lemma acyclic_widen1:
"wf_prog wfmc P ⟹ acyclic (widen1 P)"
by(auto dest: wf_converse_widen1 wf_acyclic simp add: acyclic_converse)
lemma widen1_into_widen:
"(A, B) ∈ widen1 P ⟹ P ⊢ A ≤ B"
by(induct rule: widen1.induct)(auto intro: widen.intros)
lemma widen1_rtrancl_into_widen:
"P ⊢ A <⇧* B ⟹ P ⊢ A ≤ B"
by(induct rule: rtrancl_induct)(auto dest!: widen1_into_widen elim: widen_trans)
lemma widen_eq_widen1_trancl:
"⟦ wf_prog wf_md P; T ≠ NT; T ≠ U; is_type P T ⟧ ⟹ P ⊢ T ≤ U ⟷ P ⊢ T <⇧+ U"
by(blast intro: widen_into_widen1_trancl widen1_rtrancl_into_widen trancl_into_rtrancl)
lemma sup_is_type:
assumes wf: "wf_prog wf_md P"
and itA: "is_type P A"
and itB: "is_type P B"
and sup: "sup P A B = OK T"
shows "is_type P T"
proof -
{ assume ANT: "A ≠ NT"
and BNT: "B ≠ NT"
and AnB: "A ≠ B"
and RTA: "is_refT A"
and RTB: "is_refT B"
with itA itB have AObject: "P ⊢ A ≤ Class Object"
and BObject: "P ⊢ B ≤ Class Object"
by(auto intro: is_refType_widen_Object[OF wf])
have "is_type P (exec_lub (widen1 P) (super P) A B)"
proof(cases "A = Class Object ∨ B = Class Object")
case True
hence "exec_lub (widen1 P) (super P) A B = Class Object"
proof(rule disjE)
assume A: "A = Class Object"
moreover
from BObject BNT itB have "P ⊢ B <⇧* Class Object"
by(cases "B = Class Object")(auto intro: trancl_into_rtrancl widen_into_widen1_trancl[OF wf])
hence "is_ub ((widen1 P)⇧*) (Class Object) B (Class Object)"
by(auto intro: is_ubI)
hence "is_lub ((widen1 P)⇧*) (Class Object) B (Class Object)"
by(auto simp add: is_lub_def dest: is_ubD)
with acyclic_widen1[OF wf]
have "exec_lub (widen1 P) (super P) (Class Object) B = Class Object"
by(auto intro: exec_lub_conv superI)
ultimately show "exec_lub (widen1 P) (super P) A B = Class Object" by simp
next
assume B: "B = Class Object"
moreover
from AObject ANT itA
have "(A, Class Object) ∈ (widen1 P)⇧*"
by(cases "A = Class Object", auto intro: trancl_into_rtrancl widen_into_widen1_trancl[OF wf])
hence "is_ub ((widen1 P)⇧*) (Class Object) A (Class Object)"
by(auto intro: is_ubI)
hence "is_lub ((widen1 P)⇧*) (Class Object) A (Class Object)"
by(auto simp add: is_lub_def dest: is_ubD)
with acyclic_widen1[OF wf]
have "exec_lub (widen1 P) (super P) A (Class Object) = Class Object"
by(auto intro: exec_lub_conv superI)
ultimately show "exec_lub (widen1 P) (super P) A B = Class Object" by simp
qed
with wf show ?thesis by(simp)
next
case False
hence AnObject: "A ≠ Class Object"
and BnObject: "B ≠ Class Object" by auto
from widen_into_widen1_trancl[OF wf AObject AnObject ANT itA]
have "P ⊢ A <⇧* Class Object" by(rule trancl_into_rtrancl)
moreover from widen_into_widen1_trancl[OF wf BObject BnObject BNT itB]
have "P ⊢ B <⇧* Class Object" by(rule trancl_into_rtrancl)
ultimately have "is_lub ((widen1 P)⇧*) A B (exec_lub (widen1 P) (super P) A B)"
by(rule is_lub_exec_lub[OF single_valued_widen1[OF wf] acyclic_widen1[OF wf]])(auto intro: superI)
hence Aew1: "P ⊢ A <⇧* exec_lub (widen1 P) (super P) A B"
by(auto simp add: is_lub_def dest!: is_ubD)
thus ?thesis
proof(rule rtranclE)
assume "A = exec_lub (widen1 P) (super P) A B"
with itA show ?thesis by simp
next
fix A'
assume "P ⊢ A' <⇧1 exec_lub (widen1 P) (super P) A B"
thus ?thesis by(rule widen1_is_type[OF wf])
qed
qed }
with is_class_Object[OF wf] sup itA itB show ?thesis unfolding sup_def
by(cases "A = B")(auto split: if_split_asm simp add: exec_lub_refl)
qed
lemma closed_err_types:
assumes wfP: "wf_prog wf_mb P"
shows "closed (err (types P)) (lift2 (sup P))"
proof -
{ fix A B
assume it: "is_type P A" "is_type P B"
and "A ≠ NT" "B ≠ NT" "A ≠ B"
and "is_refT A" "is_refT B"
hence "is_type P (exec_lub (widen1 P) (super P) A B)"
using sup_is_type[OF wfP it] by(simp add: sup_def) }
with is_class_Object[OF wfP] show ?thesis
unfolding closed_def plussub_def lift2_def sup_def'
by(auto split: err.split ty.splits)(auto simp add: exec_lub_refl)
qed
lemma widen_into_widen1_rtrancl:
"⟦wf_prog wfmd P; widen P A B; A ≠ NT; is_type P A ⟧ ⟹ (A, B) ∈ (widen1 P)⇧*"
by(cases "A = B")(auto intro: trancl_into_rtrancl widen_into_widen1_trancl)
lemma sup_widen_greater:
assumes wfP: "wf_prog wf_mb P"
and it1: "is_type P t1"
and it2: "is_type P t2"
and sup: "sup P t1 t2 = OK s"
shows "widen P t1 s ∧ widen P t2 s"
proof -
{ assume t1: "is_refT t1"
and t2: "is_refT t2"
and t1NT: "t1 ≠ NT"
and t2NT: "t2 ≠ NT"
with it1 it2 wfP have "P ⊢ t1 ≤ Class Object" "P ⊢ t2 ≤ Class Object"
by(auto intro: is_refType_widen_Object)
with t1NT t2NT it1 it2
have "P ⊢ t1 <⇧* Class Object" "P ⊢ t2 <⇧* Class Object"
by(auto intro: widen_into_widen1_rtrancl[OF wfP])
with single_valued_widen1[OF wfP]
obtain u where "is_lub ((widen1 P)^*) t1 t2 u"
by (blast dest: single_valued_has_lubs)
hence "P ⊢ t1 ≤ exec_lub (widen1 P) (super P) t1 t2 ∧
P ⊢ t2 ≤ exec_lub (widen1 P) (super P) t1 t2"
using acyclic_widen1[OF wfP] superI[of _ _ P]
by(simp add: exec_lub_conv)(blast dest: is_lubD is_ubD intro: widen1_rtrancl_into_widen) }
with it1 it2 sup show ?thesis
by (cases s) (auto simp add: sup_def split: if_split_asm elim: refTE)
qed
lemma sup_widen_smallest:
assumes wfP: "wf_prog wf_mb P"
and itT: "is_type P T"
and itU: "is_type P U"
and TwV: "P ⊢ T ≤ V"
and UwV: "P ⊢ U ≤ V"
and sup: "sup P T U = OK W"
shows "widen P W V"
proof -
{ assume rT: "is_refT T"
and rU: "is_refT U"
and UNT: "U ≠ NT"
and TNT: "T ≠ NT"
and W: "exec_lub (widen1 P) (super P) T U = W"
from itU itT rT rU UNT TNT have "P ⊢ T ≤ Class Object" "P ⊢ U ≤ Class Object"
by(auto intro:is_refType_widen_Object[OF wfP])
with UNT TNT itT itU
have "P ⊢ T <⇧* Class Object" "P ⊢ U <⇧* Class Object"
by(auto intro: widen_into_widen1_rtrancl[OF wfP])
with single_valued_widen1[OF wfP]
obtain X where lub: "is_lub ((widen1 P)^* ) T U X"
by (blast dest: single_valued_has_lubs)
with acyclic_widen1[OF wfP]
have "exec_lub (widen1 P) (super P) T U = X"
by (blast intro: superI exec_lub_conv)
also from TwV TNT UwV UNT itT itU have "P ⊢ T <⇧* V" "P ⊢ U <⇧* V"
by(auto intro: widen_into_widen1_rtrancl[OF wfP])
with lub have "P ⊢ X <⇧* V"
by (clarsimp simp add: is_lub_def is_ub_def)
finally have "P ⊢ exec_lub (widen1 P) (super P) T U ≤ V"
by(rule widen1_rtrancl_into_widen)
with W have "P ⊢ W ≤ V" by simp }
with sup itT itU TwV UwV show ?thesis
by(simp add: sup_def split: if_split_asm)
qed
lemma sup_exists:
"⟦ widen P a c; widen P b c ⟧ ⟹ ∃T. sup P a b = OK T"
by(cases b a rule: ty.exhaust[case_product ty.exhaust])(auto simp add: sup_def)
lemma err_semilat_JType_esl:
assumes wf_prog: "wf_prog wf_mb P"
shows "err_semilat (esl P)"
proof -
from wf_prog have "order (widen 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 ⊑⇘Err.le (widen P)⇙ x ⊔⇘lift2 (sup P)⇙ y) ∧
(∀x∈err (types P). ∀y∈err (types P). y ⊑⇘Err.le (widen P)⇙ x ⊔⇘lift2 (sup P)⇙ y)"
by(auto simp add: lesub_def plussub_def Err.le_def lift2_def sup_widen_greater split: err.split)
moreover from wf_prog have
"∀x∈err (types P). ∀y∈err (types P). ∀z∈err (types P).
x ⊑⇘Err.le (widen P)⇙ z ∧ y ⊑⇘Err.le (widen P)⇙ z ⟶ x ⊔⇘lift2 (sup P)⇙ y ⊑⇘Err.le (widen P)⇙ z"
unfolding lift2_def plussub_def lesub_def Err.le_def
by(auto intro: sup_widen_smallest dest:sup_exists simp add: split: err.split)
ultimately show ?thesis by (simp add: esl_def semilat_def sl_def Err.sl_def)
qed
subsection ‹Relation between @{term "sup P T U = OK V"} and @{term "P ⊢ lub(T, U) = V"}›
lemma sup_is_lubI:
assumes wf: "wf_prog wf_md P"
and it: "is_type P T" "is_type P U"
and sup: "sup P T U = OK V"
shows "P ⊢ lub(T, U) = V"
proof
from sup_widen_greater[OF wf it sup]
show "P ⊢ T ≤ V" "P ⊢ U ≤ V" by blast+
next
fix T'
assume "P ⊢ T ≤ T'" "P ⊢ U ≤ T'"
thus "P ⊢ V ≤ T'" using sup by(rule sup_widen_smallest[OF wf it])
qed
lemma is_lub_subD:
assumes wf: "wf_prog wf_md P"
and it: "is_type P T" "is_type P U"
and lub: "P ⊢ lub(T, U) = V"
shows "sup P T U = OK V"
proof -
from lub have "P ⊢ T ≤ V" "P ⊢ U ≤ V" by(blast dest: is_lub_upper)+
from sup_exists[OF this] obtain W where "sup P T U = OK W" by blast
moreover
with wf it have "P ⊢ lub(T, U) = W" by(rule sup_is_lubI)
with lub have "V = W" by(auto dest: is_lub_unique[OF wf])
ultimately show ?thesis by simp
qed
lemma is_lub_is_type:
"⟦ wf_prog wf_md P; is_type P T; is_type P U; P ⊢ lub(T, U) = V ⟧ ⟹ is_type P V"
by(frule (3) is_lub_subD)(erule (3) sup_is_type)
subsection ‹Code generator setup›
code_pred widen1p .
lemmas [code] = widen1_def
lemma eval_widen1p_i_i_o_conv:
"Predicate.eval (widen1p_i_i_o P T) = (λU. P ⊢ T <⇧1 U)"
by(auto elim: widen1p_i_i_oE intro: widen1p_i_i_oI simp add: widen1_def fun_eq_iff)
lemma rtrancl_widen1_code [code_unfold]:
"(widen1 P)^* = {(a, b). Predicate.holds (rtrancl_tab_FioB_i_i_i (widen1p_i_i_o P) [] a b)}"
by(auto simp add: fun_eq_iff Predicate.holds_eq widen1_def rtrancl_def rtranclp_eq_rtrancl_tab_nil eval_widen1p_i_i_o_conv intro!: rtrancl_tab_FioB_i_i_iI elim!: rtrancl_tab_FioB_i_i_iE)
declare exec_lub_def [code_unfold]
end