(* Author: Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
*)
section \<open>Correctness of the LBV\<close>
theory LBVCorrect
imports LBVSpec Typing_Framework
begin
locale lbvs = lbv +
fixes s0 :: 'a ("s\<^sub>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) \ \ 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\<^sub>0 \ \"
assumes pc: "pc+1 < length ins"
shows "wtl (take (pc+1) ins) c 0 s0 \\<^sub>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: if_split_asm)
qed
lemma (in lbvs) wtl_stable:
assumes wtl: "wtl ins c 0 s0 \ \"
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 \ \" (is "?s1 \ _") by (rule wtl_take)
from wtl have s2: "wtl (take (pc+1) ins) c 0 s0 \ \" (is "?s2 \ _") by (rule wtl_take)
from wtl pc have wt_s1: "wtc c pc ?s1 \ \" 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: if_split_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 "\ \ \" (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 ?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)) \ \" 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 \ \"
assumes pc: "pc < length ins"
shows "\!pc \ \"
proof (cases "c!pc = \")
case False with pc
have "\!pc = c!pc" ..
also from cert pc have "\ \ \" 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 "\ \ \" by (rule wtl_take)
finally show ?thesis .
qed
lemma (in lbvs) phi_in_A:
assumes wtl: "wtl ins c 0 s0 \ \"
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 \ \"
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 \ \" by (rule wtl_take)
with 0 False
have "s0 <=_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 s0 \ \"
assumes s0: "s0 \ A"
shows "\ts. wt_step r \ step ts"
proof -
have "wt_step r \ 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 \ \" 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 \ \"
assumes s0: "s0 \ A"
assumes nz: "0 < length ins"
shows "\ts \ list (length ins) A. wt_step r \ 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 \ 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 \ \" 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
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
