(* Author: Gerwin Klein

Copyright 1999 Technische Universitaet Muenchen

*)

header {* \isaheader{Correctness of the LBV} *}

theory LBVCorrect

imports LBVSpec Typing_Framework

begin

locale lbvs = lbv +

fixes s0 :: 'a ("s⇩_{0}")

fixes c :: "'a list"

fixes ins :: "'b list"

fixes phi :: "'a list" ("φ")

defines phi_def:

"φ ≡ map (λpc. if c!pc = ⊥ then wtl (take pc ins) c 0 s0 else c!pc)

[0..<length ins]"

assumes bounded: "bounded step (length ins)"

assumes cert: "cert_ok c (length ins) \<top> ⊥ A"

assumes pres: "pres_type step (length ins) A"

lemma (in lbvs) phi_None [intro?]:

"[| pc < length ins; c!pc = ⊥ |] ==> φ ! pc = wtl (take pc ins) c 0 s0"

by (simp add: phi_def)

lemma (in lbvs) phi_Some [intro?]:

"[| pc < length ins; c!pc ≠ ⊥ |] ==> φ ! pc = c ! pc"

by (simp add: phi_def)

lemma (in lbvs) phi_len [simp]:

"length φ = length ins"

by (simp add: phi_def)

lemma (in lbvs) wtl_suc_pc:

assumes all: "wtl ins c 0 s⇩_{0}≠ \<top>"

assumes pc: "pc+1 < length ins"

shows "wtl (take (pc+1) ins) c 0 s0 \<sqsubseteq>⇩_{r}φ!(pc+1)"

proof -

from all pc

have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) ≠ T" by (rule wtl_all)

with pc show ?thesis by (simp add: phi_def wtc split: split_if_asm)

qed

lemma (in lbvs) wtl_stable:

assumes wtl: "wtl ins c 0 s0 ≠ \<top>"

assumes s0: "s0 ∈ A"

assumes pc: "pc < length ins"

shows "stable r step φ pc"

proof (unfold stable_def, clarify)

fix pc' s' assume step: "(pc',s') ∈ set (step pc (φ ! pc))"

(is "(pc',s') ∈ set (?step pc)")

from bounded pc step have pc': "pc' < length ins" by (rule boundedD)

from wtl have tkpc: "wtl (take pc ins) c 0 s0 ≠ \<top>" (is "?s1 ≠ _") by (rule wtl_take)

from wtl have s2: "wtl (take (pc+1) ins) c 0 s0 ≠ \<top>" (is "?s2 ≠ _") by (rule wtl_take)

from wtl pc have wt_s1: "wtc c pc ?s1 ≠ \<top>" by (rule wtl_all)

have c_Some: "∀pc t. pc < length ins --> c!pc ≠ ⊥ --> φ!pc = c!pc"

by (simp add: phi_def)

from pc have c_None: "c!pc = ⊥ ==> φ!pc = ?s1" ..

from wt_s1 pc c_None c_Some

have inst: "wtc c pc ?s1 = wti c pc (φ!pc)"

by (simp add: wtc split: split_if_asm)

from pres cert s0 wtl pc have "?s1 ∈ A" by (rule wtl_pres)

with pc c_Some cert c_None

have "φ!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)

show "s' <=_r φ!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 < length ins" by simp

with tkpc have "?s2 = wtc c pc ?s1" by - (rule wtl_Suc)

with inst

have merge: "?s2 = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti)

also

from s2 merge have "… ≠ \<top>" (is "?merge ≠ _") by simp

with cert_in_A step_in_A

have "?merge = (map snd [(p',t') \<leftarrow> ?step pc. p'=pc+1] ++_f (c!(pc+1)))"

by (rule merge_not_top_s)

finally

have "s' <=_r ?s2" using step_in_A cert_in_A True step

by (auto intro: pp_ub1')

also

from wtl pc1 have "?s2 <=_r φ!(pc+1)" by (rule wtl_suc_pc)

also note True [symmetric]

finally show ?thesis by simp

next

case False

from wt_s1 inst

have "merge c pc (?step pc) (c!(pc+1)) ≠ \<top>" 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' = ⊥" by simp

moreover

from c_Some pc'

have "c!pc' ≠ ⊥ ==> φ!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 s0 ≠ \<top>"

assumes pc: "pc < length ins"

shows "φ!pc ≠ \<top>"

proof (cases "c!pc = ⊥")

case False with pc

have "φ!pc = c!pc" ..

also from cert pc have "… ≠ \<top>" by (rule cert_okD4)

finally show ?thesis .

next

case True with pc

have "φ!pc = wtl (take pc ins) c 0 s0" ..

also from wtl have "… ≠ \<top>" by (rule wtl_take)

finally show ?thesis .

qed

lemma (in lbvs) phi_in_A:

assumes wtl: "wtl ins c 0 s0 ≠ \<top>"

assumes s0: "s0 ∈ A"

shows "φ ∈ list (length ins) A"

proof -

{ fix x assume "x ∈ set φ"

then obtain xs ys where "φ = xs @ x # ys"

by (auto simp add: in_set_conv_decomp)

then obtain pc where pc: "pc < length φ" and x: "φ!pc = x"

by (simp add: that [of "length xs"] nth_append)

from pres cert wtl s0 pc

have "wtl (take pc ins) c 0 s0 ∈ A" by (auto intro!: wtl_pres)

moreover

from pc have "pc < length ins" by simp

with cert have "c!pc ∈ A" ..

ultimately

have "φ!pc ∈ A" using pc by (simp add: phi_def)

hence "x ∈ A" using x by simp

}

hence "set φ ⊆ A" ..

thus ?thesis by (unfold list_def) simp

qed

lemma (in lbvs) phi0:

assumes wtl: "wtl ins c 0 s0 ≠ \<top>"

assumes 0: "0 < length ins"

shows "s0 <=_r φ!0"

proof (cases "c!0 = ⊥")

case True

with 0 have "φ!0 = wtl (take 0 ins) c 0 s0" ..

moreover have "wtl (take 0 ins) c 0 s0 = s0" by simp

ultimately have "φ!0 = s0" by simp

thus ?thesis by simp

next

case False

with 0 have "phi!0 = c!0" ..

moreover

from wtl have "wtl (take 1 ins) c 0 s0 ≠ \<top>" by (rule wtl_take)

with 0 False

have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: split_if_asm)

ultimately

show ?thesis by simp

qed

theorem (in lbvs) wtl_sound:

assumes wtl: "wtl ins c 0 s0 ≠ \<top>"

assumes s0: "s0 ∈ A"

shows "∃ts. wt_step r \<top> step ts"

proof -

have "wt_step r \<top> step φ"

proof (unfold wt_step_def, intro strip conjI)

fix pc assume "pc < length φ"

then have pc: "pc < length ins" by simp

with wtl show "φ!pc ≠ \<top>" by (rule phi_not_top)

from wtl s0 pc show "stable r step φ pc" by (rule wtl_stable)

qed

thus ?thesis ..

qed

theorem (in lbvs) wtl_sound_strong:

assumes wtl: "wtl ins c 0 s0 ≠ \<top>"

assumes s0: "s0 ∈ A"

assumes nz: "0 < length ins"

shows "∃ts ∈ list (length ins) A. wt_step r \<top> step ts ∧ s0 <=_r ts!0"

proof -

from wtl s0 have "φ ∈ list (length ins) A" by (rule phi_in_A)

moreover

have "wt_step r \<top> step φ"

proof (unfold wt_step_def, intro strip conjI)

fix pc assume "pc < length φ"

then have pc: "pc < length ins" by simp

with wtl show "φ!pc ≠ \<top>" by (rule phi_not_top)

from wtl s0 pc show "stable r step φ pc" by (rule wtl_stable)

qed

moreover

from wtl nz have "s0 <=_r φ!0" by (rule phi0)

ultimately

show ?thesis by fast

qed

end