header {* \isaheader{Completeness of the LBV} *}
theory LBVComplete
imports LBVSpec Typing_Framework
begin
definition is_target :: "'s step_type => 's list => nat => bool" where
"is_target step τs pc' <-> (∃pc s'. pc' ≠ pc+1 ∧ pc < size τs ∧ (pc',s') ∈ set (step pc (τs!pc)))"
definition make_cert :: "'s step_type => 's list => 's => 's certificate" where
"make_cert step τs B = map (λpc. if is_target step τs pc then τs!pc else B) [0..<size τs] @ [B]"
lemma [code]:
"is_target step τs pc' =
list_ex (λpc. pc' ≠ pc+1 ∧ List.member (map fst (step pc (τs!pc))) pc') [0..<size τs]"
apply (simp add: list_ex_iff is_target_def member_def)
apply force
done
locale lbvc = lbv +
fixes τs :: "'a list"
fixes c :: "'a list"
defines cert_def: "c ≡ make_cert step τs ⊥"
assumes mono: "mono r step (size τs) A"
assumes pres: "pres_type step (size τs) A"
assumes τs: "∀pc < size τs. τs!pc ∈ A ∧ τs!pc ≠ \<top>"
assumes bounded: "bounded step (size τs)"
assumes B_neq_T: "⊥ ≠ \<top>"
lemma (in lbvc) cert: "cert_ok c (size τs) \<top> ⊥ A"
proof (unfold cert_ok_def, intro strip conjI)
note [simp] = make_cert_def cert_def nth_append
show "c!size τs = ⊥" by simp
fix pc assume pc: "pc < size τs"
from pc τs B_A show "c!pc ∈ A" by simp
from pc τs B_neq_T show "c!pc ≠ \<top>" by simp
qed
lemmas [simp del] = split_paired_Ex
lemma (in lbvc) cert_target [intro?]:
"[| (pc',s') ∈ set (step pc (τs!pc));
pc' ≠ pc+1; pc < size τs; pc' < size τs |]
==> c!pc' = τs!pc'"
by (auto simp add: cert_def make_cert_def nth_append is_target_def)
lemma (in lbvc) cert_approx [intro?]:
"[| pc < size τs; c!pc ≠ ⊥ |] ==> c!pc = τs!pc"
by (auto simp add: cert_def make_cert_def nth_append)
lemma (in lbv) le_top [simp, intro]: "x <=_r \<top>"
by (insert top) simp
lemma (in lbv) merge_mono:
assumes less: "set ss⇣2 {\<sqsubseteq>⇘r⇙} set ss⇣1"
assumes x: "x ∈ A"
assumes ss⇣1: "snd`set ss⇣1 ⊆ A"
assumes ss⇣2: "snd`set ss⇣2 ⊆ A"
shows "merge c pc ss⇣2 x \<sqsubseteq>⇩r merge c pc ss⇣1 x" (is "?s⇣2 \<sqsubseteq>⇩r ?s⇣1")
proof-
have "?s⇣1 = \<top> ==> ?thesis" by simp
moreover {
assume merge: "?s⇣1 ≠ T"
from x ss⇣1 have "?s⇣1 =
(if ∀(pc',s')∈set ss⇣1. pc' ≠ pc + 1 --> s' \<sqsubseteq>⇩r c!pc'
then (map snd [(p', t') \<leftarrow> ss⇣1 . p'=pc+1]) \<Squnion>⇘f⇙ x
else \<top>)" by (rule merge_def)
with merge obtain
app: "∀(pc',s')∈set ss⇣1. pc' ≠ pc+1 --> s' \<sqsubseteq>⇩r c!pc'"
(is "?app ss⇣1") and
sum: "(map snd [(p',t') \<leftarrow> ss⇣1 . p' = pc+1] \<Squnion>⇘f⇙ x) = ?s⇣1"
(is "?map ss⇣1 \<Squnion>⇘f⇙ x = _" is "?sum ss⇣1 = _")
by (simp split: split_if_asm)
from app less have "?app ss⇣2" by (blast dest: trans_r lesub_step_typeD)
moreover {
from ss⇣1 have map1: "set (?map ss⇣1) ⊆ A" by auto
with x and semilat Semilat_axioms have "?sum ss⇣1 ∈ A" by (auto intro!: plusplus_closed)
with sum have "?s⇣1 ∈ A" by simp
moreover
have mapD: "!!x ss. x ∈ set (?map ss) ==> ∃p. (p,x) ∈ set ss ∧ p=pc+1" by auto
from x map1 have "∀x ∈ set (?map ss⇣1). x \<sqsubseteq>⇩r ?sum ss⇣1" by clarify (rule pp_ub1)
with sum have "∀x ∈ set (?map ss⇣1). x \<sqsubseteq>⇩r ?s⇣1" by simp
with less have "∀x ∈ set (?map ss⇣2). x \<sqsubseteq>⇩r ?s⇣1"
by (fastforce dest!: mapD lesub_step_typeD intro: trans_r)
moreover from map1 x have "x \<sqsubseteq>⇩r (?sum ss⇣1)" by (rule pp_ub2)
with sum have "x \<sqsubseteq>⇩r ?s⇣1" by simp
moreover from ss⇣2 have "set (?map ss⇣2) ⊆ A" by auto
ultimately have "?sum ss⇣2 \<sqsubseteq>⇩r ?s⇣1" using x by - (rule pp_lub)
}
moreover from x ss⇣2 have "?s⇣2 =
(if ∀(pc', s')∈set ss⇣2. pc' ≠ pc + 1 --> s' \<sqsubseteq>⇩r c!pc'
then map snd [(p', t') \<leftarrow> ss⇣2 . p' = pc + 1] \<Squnion>⇘f⇙ x
else \<top>)" by (rule merge_def)
ultimately have ?thesis by simp
}
ultimately show ?thesis by (cases "?s⇣1 = \<top>") auto
qed
lemma (in lbvc) wti_mono:
assumes less: "s⇣2 \<sqsubseteq>⇩r s⇣1"
assumes pc: "pc < size τs" and s⇣1: "s⇣1 ∈ A" and s⇣2: "s⇣2 ∈ A"
shows "wti c pc s⇣2 \<sqsubseteq>⇩r wti c pc s⇣1" (is "?s⇣2' \<sqsubseteq>⇩r ?s⇣1'")
proof -
from mono pc s⇣2 less have "set (step pc s⇣2) {\<sqsubseteq>⇘r⇙} set (step pc s⇣1)" by (rule monoD)
moreover from cert B_A pc have "c!Suc pc ∈ A" by (rule cert_okD3)
moreover from pres s⇣1 pc have "snd`set (step pc s⇣1) ⊆ A" by (rule pres_typeD2)
moreover from pres s⇣2 pc have "snd`set (step pc s⇣2) ⊆ A" by (rule pres_typeD2)
ultimately show ?thesis by (simp add: wti merge_mono)
qed
lemma (in lbvc) wtc_mono:
assumes less: "s⇣2 \<sqsubseteq>⇩r s⇣1"
assumes pc: "pc < size τs" and s⇣1: "s⇣1 ∈ A" and s⇣2: "s⇣2 ∈ A"
shows "wtc c pc s⇣2 \<sqsubseteq>⇩r wtc c pc s⇣1" (is "?s⇣2' \<sqsubseteq>⇩r ?s⇣1'")
proof (cases "c!pc = ⊥")
case True
moreover from less pc s⇣1 s⇣2 have "wti c pc s⇣2 \<sqsubseteq>⇩r wti c pc s⇣1" by (rule wti_mono)
ultimately show ?thesis by (simp add: wtc)
next
case False
have "?s⇣1' = \<top> ==> ?thesis" by simp
moreover {
assume "?s⇣1' ≠ \<top>"
with False have c: "s⇣1 \<sqsubseteq>⇩r c!pc" by (simp add: wtc split: split_if_asm)
with less have "s⇣2 \<sqsubseteq>⇩r c!pc" ..
with False c have ?thesis by (simp add: wtc)
}
ultimately show ?thesis by (cases "?s⇣1' = \<top>") auto
qed
lemma (in lbv) top_le_conv [simp]: "\<top> \<sqsubseteq>⇩r x = (x = \<top>)"
by (insert semilat) (simp add: top top_le_conv)
lemma (in lbv) neq_top [simp, elim]: "[| x \<sqsubseteq>⇩r y; y ≠ \<top> |] ==> x ≠ \<top>"
by (cases "x = T") auto
lemma (in lbvc) stable_wti:
assumes stable: "stable r step τs pc" and pc: "pc < size τs"
shows "wti c pc (τs!pc) ≠ \<top>"
proof -
let ?step = "step pc (τs!pc)"
from stable
have less: "∀(q,s')∈set ?step. s' \<sqsubseteq>⇩r τs!q" by (simp add: stable_def)
from cert B_A pc have cert_suc: "c!Suc pc ∈ A" by (rule cert_okD3)
moreover from τs pc have "τs!pc ∈ A" by simp
with pres pc have stepA: "snd`set ?step ⊆ A" by - (rule pres_typeD2)
ultimately
have "merge c pc ?step (c!Suc pc) =
(if ∀(pc',s')∈set ?step. pc'≠pc+1 --> s' \<sqsubseteq>⇩r c!pc'
then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] \<Squnion>⇘f⇙ c!Suc pc
else \<top>)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
moreover {
fix pc' s' assume s': "(pc',s') ∈ set ?step" and suc_pc: "pc' ≠ pc+1"
with less have "s' \<sqsubseteq>⇩r τs!pc'" by auto
also from bounded pc s' have "pc' < size τs" by (rule boundedD)
with s' suc_pc pc have "c!pc' = τs!pc'" ..
hence "τs!pc' = c!pc'" ..
finally have "s' \<sqsubseteq>⇩r c!pc'" .
} hence "∀(pc',s')∈set ?step. pc'≠pc+1 --> s' \<sqsubseteq>⇩r c!pc'" by auto
moreover from pc have "Suc pc = size τs ∨ Suc pc < size τs" by auto
hence "map snd [(p',t') \<leftarrow> ?step.p'=pc+1] \<Squnion>⇘f⇙ c!Suc pc ≠ \<top>" (is "?map \<Squnion>⇘f⇙ _ ≠ _")
proof (rule disjE)
assume pc': "Suc pc = size τs"
with cert have "c!Suc pc = ⊥" by (simp add: cert_okD2)
moreover
from pc' bounded pc
have "∀(p',t')∈set ?step. p'≠pc+1" by clarify (drule boundedD, auto)
hence "[(p',t') \<leftarrow> ?step. p'=pc+1] = []" by (blast intro: filter_False)
hence "?map = []" by simp
ultimately show ?thesis by (simp add: B_neq_T)
next
assume pc': "Suc pc < size τs"
from pc' τs have "τs!Suc pc ∈ A" by simp
moreover note cert_suc
moreover from stepA have "set ?map ⊆ A" by auto
moreover have "!!s. s ∈ set ?map ==> ∃t. (Suc pc, t) ∈ set ?step" by auto
with less have "∀s' ∈ set ?map. s' \<sqsubseteq>⇩r τs!Suc pc" by auto
moreover from pc' have "c!Suc pc \<sqsubseteq>⇩r τs!Suc pc"
by (cases "c!Suc pc = ⊥") (auto dest: cert_approx)
ultimately have "?map \<Squnion>⇘f⇙ c!Suc pc \<sqsubseteq>⇩r τs!Suc pc" by (rule pp_lub)
moreover from pc' τs have "τs!Suc pc ≠ \<top>" by simp
ultimately show ?thesis by auto
qed
ultimately have "merge c pc ?step (c!Suc pc) ≠ \<top>" by simp
thus ?thesis by (simp add: wti)
qed
lemma (in lbvc) wti_less:
assumes stable: "stable r step τs pc" and suc_pc: "Suc pc < size τs"
shows "wti c pc (τs!pc) \<sqsubseteq>⇩r τs!Suc pc" (is "?wti \<sqsubseteq>⇩r _")
proof -
let ?step = "step pc (τs!pc)"
from stable
have less: "∀(q,s')∈set ?step. s' \<sqsubseteq>⇩r τs!q" by (simp add: stable_def)
from suc_pc have pc: "pc < size τs" by simp
with cert B_A have cert_suc: "c!Suc pc ∈ A" by (rule cert_okD3)
moreover from τs pc have "τs!pc ∈ A" by simp
with pres pc have stepA: "snd`set ?step ⊆ A" by - (rule pres_typeD2)
moreover from stable pc have "?wti ≠ \<top>" by (rule stable_wti)
hence "merge c pc ?step (c!Suc pc) ≠ \<top>" by (simp add: wti)
ultimately
have "merge c pc ?step (c!Suc pc) =
map snd [(p',t') \<leftarrow> ?step.p'=pc+1] \<Squnion>⇘f⇙ c!Suc pc" by (rule merge_not_top_s)
hence "?wti = …" (is "_ = (?map \<Squnion>⇘f⇙ _)" is "_ = ?sum") by (simp add: wti)
also {
from suc_pc τs have "τs!Suc pc ∈ A" by simp
moreover note cert_suc
moreover from stepA have "set ?map ⊆ A" by auto
moreover have "!!s. s ∈ set ?map ==> ∃t. (Suc pc, t) ∈ set ?step" by auto
with less have "∀s' ∈ set ?map. s' \<sqsubseteq>⇩r τs!Suc pc" by auto
moreover from suc_pc have "c!Suc pc \<sqsubseteq>⇩r τs!Suc pc"
by (cases "c!Suc pc = ⊥") (auto dest: cert_approx)
ultimately have "?sum \<sqsubseteq>⇩r τs!Suc pc" by (rule pp_lub)
}
finally show ?thesis .
qed
lemma (in lbvc) stable_wtc:
assumes stable: "stable r step τs pc" and pc: "pc < size τs"
shows "wtc c pc (τs!pc) ≠ \<top>"
proof -
from stable pc have wti: "wti c pc (τs!pc) ≠ \<top>" by (rule stable_wti)
show ?thesis
proof (cases "c!pc = ⊥")
case True with wti show ?thesis by (simp add: wtc)
next
case False
with pc have "c!pc = τs!pc" ..
with False wti show ?thesis by (simp add: wtc)
qed
qed
lemma (in lbvc) wtc_less:
assumes stable: "stable r step τs pc" and suc_pc: "Suc pc < size τs"
shows "wtc c pc (τs!pc) \<sqsubseteq>⇩r τs!Suc pc" (is "?wtc \<sqsubseteq>⇩r _")
proof (cases "c!pc = ⊥")
case True
moreover from stable suc_pc have "wti c pc (τs!pc) \<sqsubseteq>⇩r τs!Suc pc" by (rule wti_less)
ultimately show ?thesis by (simp add: wtc)
next
case False
from suc_pc have pc: "pc < size τs" by simp
with stable have "?wtc ≠ \<top>" by (rule stable_wtc)
with False have "?wtc = wti c pc (c!pc)"
by (unfold wtc) (simp split: split_if_asm)
also from pc False have "c!pc = τs!pc" ..
finally have "?wtc = wti c pc (τs!pc)" .
also from stable suc_pc have "wti c pc (τs!pc) \<sqsubseteq>⇩r τs!Suc pc" by (rule wti_less)
finally show ?thesis .
qed
lemma (in lbvc) wt_step_wtl_lemma:
assumes wt_step: "wt_step r \<top> step τs"
shows "!!pc s. pc+size ls = size τs ==> s \<sqsubseteq>⇩r τs!pc ==> s ∈ A ==> s≠\<top> ==>
wtl ls c pc s ≠ \<top>"
(is "!!pc s. _ ==> _ ==> _ ==> _ ==> ?wtl ls pc s ≠ _")
proof (induct ls)
fix pc s assume "s≠\<top>" thus "?wtl [] pc s ≠ \<top>" by simp
next
fix pc s i ls
assume "!!pc s. pc+size ls=size τs ==> s \<sqsubseteq>⇩r τs!pc ==> s ∈ A ==> s≠\<top> ==>
?wtl ls pc s ≠ \<top>"
moreover
assume pc_l: "pc + size (i#ls) = size τs"
hence suc_pc_l: "Suc pc + size ls = size τs" by simp
ultimately
have IH: "!!s. s \<sqsubseteq>⇩r τs!Suc pc ==> s ∈ A ==> s ≠ \<top> ==> ?wtl ls (Suc pc) s ≠ \<top>" .
from pc_l obtain pc: "pc < size τs" by simp
with wt_step have stable: "stable r step τs pc" by (simp add: wt_step_def)
moreover note pc
ultimately have wt_τs: "wtc c pc (τs!pc) ≠ \<top>" by (rule stable_wtc)
assume s_τs: "s \<sqsubseteq>⇩r τs!pc"
assume sA: "s ∈ A"
from τs pc have τs_pc: "τs!pc ∈ A" by simp
from s_τs pc τs_pc sA have wt_s_τs: "wtc c pc s \<sqsubseteq>⇩r wtc c pc (τs!pc)" by (rule wtc_mono)
with wt_τs have wt_s: "wtc c pc s ≠ \<top>" by simp
moreover assume s: "s ≠ \<top>"
ultimately have "ls = [] ==> ?wtl (i#ls) pc s ≠ \<top>" by simp
moreover {
assume "ls ≠ []"
with pc_l have suc_pc: "Suc pc < size τs" by (auto simp add: neq_Nil_conv)
with stable have "wtc c pc (τs!pc) \<sqsubseteq>⇩r τs!Suc pc" by (rule wtc_less)
with wt_s_τs have "wtc c pc s \<sqsubseteq>⇩r τs!Suc pc" by (rule trans_r)
moreover from cert suc_pc have "c!pc ∈ A" "c!(pc+1) ∈ A"
by (auto simp add: cert_ok_def)
from pres this sA pc have "wtc c pc s ∈ A" by (rule wtc_pres)
ultimately have "?wtl ls (Suc pc) (wtc c pc s) ≠ \<top>" using IH wt_s by blast
with s wt_s have "?wtl (i#ls) pc s ≠ \<top>" by simp
}
ultimately show "?wtl (i#ls) pc s ≠ \<top>" by (cases ls) blast+
qed
theorem (in lbvc) wtl_complete:
assumes wt: "wt_step r \<top> step τs"
assumes s: "s \<sqsubseteq>⇩r τs!0" "s ∈ A" "s ≠ \<top>" and eq: "size ins = size τs"
shows "wtl ins c 0 s ≠ \<top>"
proof -
from eq have "0+size ins = size τs" by simp
from wt this s show ?thesis by (rule wt_step_wtl_lemma)
qed
end