Up to index of Isabelle/HOL/arrays
theory LBVCorrect = LBVSpec + Typing_Framework:(* Title: HOL/MicroJava/BV/LBVCorrect.thy
ID: $Id: LBVCorrect.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
Author: Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
*)
header {* \isaheader{Correctness of the LBV} *}
theory LBVCorrect = LBVSpec + Typing_Framework:
locale (open) lbvs = lbv +
fixes s0 :: 'a
fixes c :: "'a list"
fixes ins :: "'b list"
fixes phi :: "'a list" ("\<phi>")
defines phi_def:
"\<phi> \<equiv> map (\<lambda>pc. if c!pc = \<bottom> then wtl (take pc ins) c 0 s0 else c!pc)
[0..length ins(]"
assumes bounded: "bounded step (length ins) A"
assumes cert: "cert_ok c (length ins) \<top> \<bottom> A"
assumes pres: "pres_type step (length ins) A"
lemma (in lbvs) phi_None [intro?]:
"\<lbrakk> pc < length ins; c!pc = \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = wtl (take pc ins) c 0 s0"
by (simp add: phi_def)
lemma (in lbvs) phi_Some [intro?]:
"\<lbrakk> pc < length ins; c!pc \<noteq> \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = c ! pc"
by (simp add: phi_def)
lemma (in lbvs) phi_len [simp]:
"length \<phi> = length ins"
by (simp add: phi_def)
lemma (in lbvs) wtl_suc_pc:
assumes all: "wtl ins c 0 s0 \<noteq> \<top>"
assumes pc: "pc+1 < length ins"
shows "wtl (take (pc+1) ins) c 0 s0 <=_r \<phi>!(pc+1)"
proof -
from all pc
have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) \<noteq> 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 \<noteq> \<top>"
assumes s0: "s0 \<in> A"
assumes pc: "pc < length ins"
shows "stable r step \<phi> pc"
proof (unfold stable_def, clarify)
fix pc' s' assume step: "(pc',s') \<in> set (step pc (\<phi> ! pc))"
(is "(pc',s') \<in> set (?step pc)")
have tkpc: "wtl (take pc ins) c 0 s0 \<noteq> \<top>" (is "?s1 \<noteq> _") by (rule wtl_take)
have s2: "wtl (take (pc+1) ins) c 0 s0 \<noteq> \<top>" (is "?s2 \<noteq> _") by (rule wtl_take)
from wtl pc have wt_s1: "wtc c pc ?s1 \<noteq> \<top>" by (rule wtl_all)
have c_Some: "\<forall>pc t. pc < length ins \<longrightarrow> c!pc \<noteq> \<bottom> \<longrightarrow> \<phi>!pc = c!pc"
by (simp add: phi_def)
have c_None: "c!pc = \<bottom> \<Longrightarrow> \<phi>!pc = ?s1" ..
from wt_s1 pc c_None c_Some
have inst: "wtc c pc ?s1 = wti c pc (\<phi>!pc)"
by (simp add: wtc split: split_if_asm)
have "?s1 \<in> A" by (rule wtl_pres)
with pc c_Some cert c_None
have phi_in_A: "\<phi>!pc \<in> A" by (cases "c!pc = \<bottom>") (auto dest: cert_okD1)
with pc pres
have step_in_A: "snd`set (?step pc) \<subseteq> A" by (auto dest: pres_typeD2)
from bounded pc phi_in_A step have pc': "pc' < length ins" by (rule boundedD)
show "s' <=_r \<phi>!pc'"
proof (cases "pc' = pc+1")
case True
with pc' cert
have cert_in_A: "c!(pc+1) \<in> 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 "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp
with cert_in_A step_in_A
have "?merge = (map snd [(p',t')\<in>?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 \<phi>!(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)) \<noteq> \<top>" by (simp add: wti)
with step_in_A
have "\<forall>(pc', s')\<in>set (?step pc). pc'\<noteq>pc+1 \<longrightarrow> 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' = \<bottom> \<Longrightarrow> s' = \<bottom>" by simp
moreover
from c_Some pc'
have "c!pc' \<noteq> \<bottom> \<Longrightarrow> \<phi>!pc' = c!pc'" by auto
ultimately
show ?thesis by (cases "c!pc' = \<bottom>") auto
qed
qed
lemma (in lbvs) phi_not_top:
assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
assumes pc: "pc < length ins"
shows "\<phi>!pc \<noteq> \<top>"
proof (cases "c!pc = \<bottom>")
case False with pc
have "\<phi>!pc = c!pc" ..
also from cert pc have "\<dots> \<noteq> \<top>" by (rule cert_okD4)
finally show ?thesis .
next
case True with pc
have "\<phi>!pc = wtl (take pc ins) c 0 s0" ..
also from wtl have "\<dots> \<noteq> \<top>" by (rule wtl_take)
finally show ?thesis .
qed
lemma (in lbvs) phi_in_A:
assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
assumes s0: "s0 \<in> A"
shows "\<phi> \<in> list (length ins) A"
proof -
{ fix x assume "x \<in> set \<phi>"
then obtain xs ys where "\<phi> = xs @ x # ys"
by (auto simp add: in_set_conv_decomp)
then obtain pc where pc: "pc < length \<phi>" and x: "\<phi>!pc = x"
by (simp add: that [of "length xs"] nth_append)
from wtl s0 pc
have "wtl (take pc ins) c 0 s0 \<in> A" by (auto intro!: wtl_pres)
moreover
from pc have "pc < length ins" by simp
with cert have "c!pc \<in> A" ..
ultimately
have "\<phi>!pc \<in> A" using pc by (simp add: phi_def)
hence "x \<in> A" using x by simp
}
hence "set \<phi> \<subseteq> A" ..
thus ?thesis by (unfold list_def) simp
qed
lemma (in lbvs) phi0:
assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
assumes 0: "0 < length ins"
shows "s0 <=_r \<phi>!0"
proof (cases "c!0 = \<bottom>")
case True
with 0 have "\<phi>!0 = wtl (take 0 ins) c 0 s0" ..
moreover have "wtl (take 0 ins) c 0 s0 = s0" by simp
ultimately have "\<phi>!0 = s0" by simp
thus ?thesis by simp
next
case False
with 0 have "phi!0 = c!0" ..
moreover
have "wtl (take 1 ins) c 0 s0 \<noteq> \<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 ins c 0 s0 \<noteq> \<top>"
assumes "s0 \<in> A"
shows "\<exists>ts. wt_step r \<top> step ts"
proof -
have "wt_step r \<top> step \<phi>"
proof (unfold wt_step_def, intro strip conjI)
fix pc assume "pc < length \<phi>"
then obtain "pc < length ins" by simp
show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
show "stable r step \<phi> pc" by (rule wtl_stable)
qed
thus ?thesis ..
qed
theorem (in lbvs) wtl_sound_strong:
assumes "wtl ins c 0 s0 \<noteq> \<top>"
assumes "s0 \<in> A"
assumes "0 < length ins"
shows "\<exists>ts \<in> list (length ins) A. wt_step r \<top> step ts \<and> s0 <=_r ts!0"
proof -
have "\<phi> \<in> list (length ins) A" by (rule phi_in_A)
moreover
have "wt_step r \<top> step \<phi>"
proof (unfold wt_step_def, intro strip conjI)
fix pc assume "pc < length \<phi>"
then obtain "pc < length ins" by simp
show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
show "stable r step \<phi> pc" by (rule wtl_stable)
qed
moreover
have "s0 <=_r \<phi>!0" by (rule phi0)
ultimately
show ?thesis by fast
qed
end
lemma phi_None:
[| semilat (A, r, f); top r T; T : A; bottom r B; B : A;
bounded step (length ins) A; cert_ok c (length ins) T B A;
pres_type step (length ins) A; pc < length ins; c ! pc = B |]
==> map (%pc. if c ! pc = B then wtl_inst_list (take pc ins) c f r T B step 0 s0
else c ! pc)
[0..length ins(] !
pc =
wtl_inst_list (take pc ins) c f r T B step 0 s0
lemma phi_Some:
[| semilat (A, r, f); top r T; T : A; bottom r B; B : A;
bounded step (length ins) A; cert_ok c (length ins) T B A;
pres_type step (length ins) A; pc < length ins; c ! pc ~= B |]
==> map (%pc. if c ! pc = B then wtl_inst_list (take pc ins) c f r T B step 0 s0
else c ! pc)
[0..length ins(] !
pc =
c ! pc
lemma phi_len:
[| semilat (A, r, f); top r T; T : A; bottom r B; B : A;
bounded step (length ins) A; cert_ok c (length ins) T B A;
pres_type step (length ins) A |]
==> length
(map (%pc. if c ! pc = B
then wtl_inst_list (take pc ins) c f r T B step 0 s0
else c ! pc)
[0..length ins(]) =
length ins
lemma
[| semilat (A, r, f); top r T; T : A; bottom r B; B : A;
bounded step (length ins) A; cert_ok c (length ins) T B A;
pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0 ~= T;
pc + 1 < length ins |]
==> wtl_inst_list (take (pc + 1) ins) c f r T B step 0 s0
<=_r map (%pc. if c ! pc = B
then wtl_inst_list (take pc ins) c f r T B step 0 s0
else c ! pc)
[0..length ins(] !
(pc + 1)
lemma
[| semilat (A, r, f); top r T; T : A; bottom r B; B : A;
bounded step (length ins) A; cert_ok c (length ins) T B A;
pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0 ~= T;
s0 : A; pc < length ins |]
==> stable r step
(map (%pc. if c ! pc = B
then wtl_inst_list (take pc ins) c f r T B step 0 s0
else c ! pc)
[0..length ins(])
pc
lemma
[| semilat (A, r, f); top r T; T : A; bottom r B; B : A;
bounded step (length ins) A; cert_ok c (length ins) T B A;
pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0 ~= T;
pc < length ins |]
==> map (%pc. if c ! pc = B then wtl_inst_list (take pc ins) c f r T B step 0 s0
else c ! pc)
[0..length ins(] !
pc ~=
T
lemma
[| semilat (A, r, f); top r T; T : A; bottom r B; B : A;
bounded step (length ins) A; cert_ok c (length ins) T B A;
pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0 ~= T;
s0 : A |]
==> map (%pc. if c ! pc = B then wtl_inst_list (take pc ins) c f r T B step 0 s0
else c ! pc)
[0..length ins(]
: list (length ins) A
lemma
[| semilat (A, r, f); top r T; T : A; bottom r B; B : A;
bounded step (length ins) A; cert_ok c (length ins) T B A;
pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0 ~= T;
0 < length ins |]
==> s0 <=_r map (%pc. if c ! pc = B
then wtl_inst_list (take pc ins) c f r T B step 0 s0
else c ! pc)
[0..length ins(] !
0
theorem
[| semilat (A, r, f); top r T; T : A; bottom r B; B : A;
bounded step (length ins) A; cert_ok c (length ins) T B A;
pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0 ~= T;
s0 : A |]
==> EX ts. wt_step r T step ts
theorem
[| semilat (A, r, f); top r T; T : A; bottom r B; B : A;
bounded step (length ins) A; cert_ok c (length ins) T B A;
pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0 ~= T;
s0 : A; 0 < length ins |]
==> EX ts:list (length ins) A. wt_step r T step ts & s0 <=_r ts ! 0