Theory Jinja.LBVCorrect
section ‹Correctness of the LBV›
theory LBVCorrect
imports LBVSpec Typing_Framework_1
begin
locale lbvs = lbv +
fixes s⇩0 :: 'a
fixes c :: "'a list"
fixes ins :: "'b list"
fixes τs :: "'a list"
defines phi_def:
"τs ≡ map (λpc. if c!pc = ⊥ then wtl (take pc ins) c 0 s⇩0 else c!pc)
[0..<size ins]"
assumes bounded: "bounded step (size ins)"
assumes cert: "cert_ok c (size ins) ⊤ ⊥ A"
assumes pres: "pres_type step (size ins) A"
lemma (in lbvs) phi_None [intro?]:
"⟦ pc < size ins; c!pc = ⊥ ⟧ ⟹ τs!pc = wtl (take pc ins) c 0 s⇩0"
by (simp add: phi_def)
lemma (in lbvs) phi_Some [intro?]:
"⟦ pc < size ins; c!pc ≠ ⊥ ⟧ ⟹ τs!pc = c!pc"
by (simp add: phi_def)
lemma (in lbvs) phi_len [simp]: "size τs = size ins"
by (simp add: phi_def)
lemma (in lbvs) wtl_suc_pc:
assumes all: "wtl ins c 0 s⇩0 ≠ ⊤"
assumes pc: "pc+1 < size ins"
assumes sA: "s⇩0 ∈ A"
shows "wtl (take (pc+1) ins) c 0 s⇩0 ⊑⇩r τs!(pc+1)"
proof -
from all pc
have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s⇩0) ≠ T" by (rule wtl_all)
with pc show ?thesis using sA pres cert all wtl_pres by (simp add: phi_def wtc split: if_split_asm)
qed
lemma (in lbvs) wtl_stable:
assumes wtl: "wtl ins c 0 s⇩0 ≠ ⊤"
assumes s⇩0: "s⇩0 ∈ A" and pc: "pc < size ins"
shows "stable r step τs pc"
proof (unfold stable_def, clarify)
fix pc' s' assume step: "(pc',s') ∈ set (step pc (τs ! pc))"
(is "(pc',s') ∈ set (?step pc)")
from bounded pc step have pc': "pc' < size ins" by (rule boundedD)
have tkpc: "wtl (take pc ins) c 0 s⇩0 ≠ ⊤" (is "?s⇩1 ≠ _") using wtl by (rule wtl_take)
have s⇩2: "wtl (take (pc+1) ins) c 0 s⇩0 ≠ ⊤" (is "?s⇩2 ≠ _") using wtl by (rule wtl_take)
from wtl pc have wt_s⇩1: "wtc c pc ?s⇩1 ≠ ⊤" by (rule wtl_all)
have c_Some: "∀pc t. pc < size ins ⟶ c!pc ≠ ⊥ ⟶ τs!pc = c!pc"
by (simp add: phi_def)
have c_None: "c!pc = ⊥ ⟹ τs!pc = ?s⇩1" using pc ..
from wt_s⇩1 pc c_None c_Some
have inst: "wtc c pc ?s⇩1 = wti c pc (τs!pc)"
by (simp add: wtc split: if_split_asm)
have "?s⇩1 ∈ A" using pres cert s⇩0 wtl pc by (rule wtl_pres)
with pc c_Some cert c_None
have "τs!pc ∈ A" by (cases "c!pc = ⊥") (auto dest: cert_okD1)
with pc pres
have step_in_A: "snd`set (?step pc) ⊆ A" by (auto dest: pres_typeD2)
then have inA1: "s' ∈ A" using step by auto
show "s' ⊑⇩r τs!pc'"
proof (cases "pc' = pc+1")
case True
with pc' cert
have cert_in_A: "c!(pc+1) ∈ A" by (auto dest: cert_okD1)
from True pc' have pc1: "pc+1 < size ins" by simp
with pres cert s⇩0 wtl have inA2: "wtl (take (pc + 1) ins) c 0 s⇩0 ∈ A" by (auto dest:wtl_pres)
have c_None': "c!(pc +1)= ⊥ ⟹ τs!(pc + 1)= ?s⇩2" using pc1 ..
have "?s⇩2 ∈ A" using pres cert s⇩0 wtl pc1 by (rule wtl_pres)
with pc1 c_Some cert c_None'
have inA3: "τs!(pc+1) ∈ A" by (cases "c!(pc+1) = ⊥") (auto dest: cert_okD1)
from pc1 tkpc have "?s⇩2 = wtc c pc ?s⇩1" by - (rule wtl_Suc)
with inst
have merge: "?s⇩2 = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti)
also from s⇩2 merge have "… ≠ ⊤" (is "?merge ≠ _") by simp
with cert_in_A step_in_A
have "?merge = (map snd [(p',t') ← ?step pc. p'=pc+1] ⨆⇘f⇙ c!(pc+1))"
by (rule merge_not_top_s)
finally have "s' ⊑⇩r ?s⇩2" using step_in_A cert_in_A True step
by (auto intro: pp_ub1')
also from wtl pc1 have "?s⇩2 ⊑⇩r τs!(pc+1)" using s⇩0 by (auto dest: wtl_suc_pc)
also note True [symmetric]
finally show ?thesis using inA1 inA2 inA3 by simp
next
case False
from wt_s⇩1 inst
have "merge c pc (?step pc) (c!(pc+1)) ≠ ⊤" by (simp add: wti)
with step_in_A have "∀(pc', s')∈set (?step pc). pc'≠pc+1 ⟶ s' ⊑⇩r c!pc'"
by - (rule merge_not_top)
with step False have ok: "s' ⊑⇩r c!pc'" by blast
moreover from ok have "c!pc' = ⊥ ⟹ s' = ⊥" using inA1 by simp
moreover from c_Some pc' have "c!pc' ≠ ⊥ ⟹ τs!pc' = c!pc'" by auto
ultimately show ?thesis by (cases "c!pc' = ⊥") auto
qed
qed
lemma (in lbvs) phi_not_top:
assumes wtl: "wtl ins c 0 s⇩0 ≠ ⊤" and pc: "pc < size ins"
shows "τs!pc ≠ ⊤"
proof (cases "c!pc = ⊥")
case False with pc
have "τs!pc = c!pc" ..
also from cert pc have "… ≠ ⊤" by (rule cert_okD4)
finally show ?thesis .
next
case True with pc
have "τs!pc = wtl (take pc ins) c 0 s⇩0" ..
also from wtl have "… ≠ ⊤" by (rule wtl_take)
finally show ?thesis .
qed
lemma (in lbvs) phi_in_A:
assumes wtl: "wtl ins c 0 s⇩0 ≠ ⊤" and s⇩0: "s⇩0 ∈ A"
shows "τs ∈ nlists (size ins) A"
proof -
{ fix x assume "x ∈ set τs"
then obtain xs ys where "τs = xs @ x # ys"
by (auto simp add: in_set_conv_decomp)
then obtain pc where pc: "pc < size τs" and x: "τs!pc = x"
by (simp add: that [of "size xs"] nth_append)
from pres cert wtl s⇩0 pc
have "wtl (take pc ins) c 0 s⇩0 ∈ A" by (auto intro!: wtl_pres)
moreover
from pc have "pc < size ins" by simp
with cert have "c!pc ∈ A" ..
ultimately
have "τs!pc ∈ A" using pc by (simp add: phi_def)
hence "x ∈ A" using x by simp
}
hence "set τs ⊆ A" ..
thus ?thesis by (unfold nlists_def) simp
qed
lemma (in lbvs) phi0:
assumes wtl: "wtl ins c 0 s⇩0 ≠ ⊤" and 0: "0 < size ins" and s⇩0: "s⇩0 ∈ A"
shows "s⇩0 ⊑⇩r τs!0"
proof (cases "c!0 = ⊥")
case True
with 0 have "τs!0 = wtl (take 0 ins) c 0 s⇩0" ..
moreover have "wtl (take 0 ins) c 0 s⇩0 = s⇩0" by simp
ultimately have "τs!0 = s⇩0" by simp
thus ?thesis using s⇩0 by simp
next
case False
with 0 have "τs!0 = c!0" ..
moreover
have "wtl (take 1 ins) c 0 s⇩0 ≠ ⊤" using wtl by (rule wtl_take)
with 0 False
have "s⇩0 ⊑⇩r c!0" by (auto simp add: neq_Nil_conv wtc split: if_split_asm)
ultimately
show ?thesis by simp
qed
theorem (in lbvs) wtl_sound:
assumes wtl: "wtl ins c 0 s⇩0 ≠ ⊤" and s⇩0: "s⇩0 ∈ A"
shows "∃τs. wt_step r ⊤ step τs"
proof -
have "wt_step r ⊤ step τs"
proof (unfold wt_step_def, intro strip conjI)
fix pc assume "pc < size τs"
then obtain pc: "pc < size ins" by simp
with wtl show "τs!pc ≠ ⊤" by (rule phi_not_top)
from wtl s⇩0 pc show "stable r step τs pc" by (rule wtl_stable)
qed
thus ?thesis ..
qed
theorem (in lbvs) wtl_sound_strong:
assumes wtl: "wtl ins c 0 s⇩0 ≠ ⊤"
assumes s⇩0: "s⇩0 ∈ A" and ins: "0 < size ins"
shows "∃τs ∈ nlists (size ins) A. wt_step r ⊤ step τs ∧ s⇩0 ⊑⇩r τs!0"
proof -
have "τs ∈ nlists (size ins) A" using wtl s⇩0 by (rule phi_in_A)
moreover
have "wt_step r ⊤ step τs"
proof (unfold wt_step_def, intro strip conjI)
fix pc assume "pc < size τs"
then obtain pc: "pc < size ins" by simp
with wtl show "τs!pc ≠ ⊤" by (rule phi_not_top)
from wtl s⇩0 and pc show "stable r step τs pc" by (rule wtl_stable)
qed
moreover from wtl ins have "s⇩0 ⊑⇩r τs!0" using s⇩0 by (rule phi0)
ultimately show ?thesis by fast
qed
end