theory TM_Assemble
imports Hoare_tm StateMonad
"~~/src/HOL/Library/FinFun_Syntax"
"~~/src/HOL/Library/Sublist"
LetElim
begin
section {* The assembler based on Benton's x86 paper *}
text {*
The problem with the assembler is that it is too slow to be useful.
*}
primrec pass1 :: "tpg \<Rightarrow> (unit, (nat \<times> nat \<times> (nat \<rightharpoonup> nat))) SM"
where
"pass1 (TInstr ai) = sm_map (\<lambda> (pos, lno, lmap). (pos + 1, lno, lmap))" |
"pass1 (TSeq p1 p2) = do {pass1 p1; pass1 p2 }" |
"pass1 (TLocal fp) = do { lno \<leftarrow> tap (\<lambda> (pos, lno, lmap). lno);
sm_map (\<lambda> (pos, lno, lmap). (pos, lno+1, lmap));
pass1 (fp lno) }" |
"pass1 (TLabel l) = sm_map ((\<lambda> (pos, lno, lmap). (pos, lno, lmap(l \<mapsto> pos))))"
declare pass1.simps[simp del]
type_synonym ('a, 'b) alist = "('a \<times> 'b) list"
primrec pass2 :: "tpg \<Rightarrow> (nat \<rightharpoonup> nat) \<Rightarrow> (unit, (nat \<times> nat \<times> (nat, tm_inst) alist)) SM"
where
"pass2 (TInstr ai) lmap = sm_map (\<lambda> (pos, lno, prog). (pos + 1, lno, (pos, ai)#prog))" |
"pass2 (TSeq p1 p2) lmap = do {pass2 p1 lmap; pass2 p2 lmap}" |
"pass2 (TLocal fp) lmap = do { lno \<leftarrow> tap (\<lambda> (pos, lno, prog). lno);
sm_map (\<lambda> (pos, lno, prog). (pos, lno + 1, prog));
(case (lmap lno) of
Some l => pass2 (fp l) lmap |
None => (raise ''Undefined label''))} " |
"pass2 (TLabel l) lmap = do { pos \<leftarrow> tap (\<lambda> (pos, lno, prog). pos);
if (l = pos) then return ()
else (raise ''Label mismatch'') }"
declare pass2.simps[simp del]
definition "assembleM i tpg =
do {(x, (pos, lno, lmap)) \<leftarrow> execute (pass1 tpg) (i, 0, empty);
execute (pass2 tpg lmap) (i, 0, [])}"
definition
"assemble i tpg = Option.map (\<lambda> (x, (j, lno, prog)).(prog, j)) (assembleM i tpg)"
lemma tprog_set_union:
assumes "(fst ` set pg3) \<inter> (fst ` set pg2) = {}"
shows "tprog_set (map_of pg3 ++ map_of pg2) = tprog_set (map_of pg3) \<union> tprog_set (map_of pg2)"
proof -
from assms have "dom (map_of pg3) \<inter> dom (map_of pg2) = {}"
by (metis dom_map_of_conv_image_fst)
hence map_comm: "map_of pg3 ++ map_of pg2 = map_of pg2 ++ map_of pg3"
by (metis map_add_comm)
show ?thesis
proof
show "tprog_set (map_of pg3 ++ map_of pg2) \<subseteq> tprog_set (map_of pg3) \<union> tprog_set (map_of pg2)"
proof
fix x
assume " x \<in> tprog_set (map_of pg3 ++ map_of pg2)"
then obtain i inst where h:
"x = TC i inst"
"(map_of pg3 ++ map_of pg2) i = Some inst"
apply (unfold tprog_set_def)
by (smt mem_Collect_eq)
from map_add_SomeD[OF h(2)] h(1)
show " x \<in> tprog_set (map_of pg3) \<union> tprog_set (map_of pg2)"
apply (unfold tprog_set_def)
by (smt mem_Collect_eq sup1CI sup_Un_eq)
qed
next
show "tprog_set (map_of pg3) \<union> tprog_set (map_of pg2) \<subseteq> tprog_set (map_of pg3 ++ map_of pg2)"
proof
fix x
assume " x \<in> tprog_set (map_of pg3) \<union> tprog_set (map_of pg2)"
then obtain i inst
where h: "x = TC i inst" "map_of pg3 i = Some inst \<or> map_of pg2 i = Some inst"
apply (unfold tprog_set_def)
by (smt Un_iff mem_Collect_eq)
from h(2)
show "x \<in> tprog_set (map_of pg3 ++ map_of pg2)"
proof
assume "map_of pg2 i = Some inst"
hence "(map_of pg3 ++ map_of pg2) i = Some inst"
by (metis map_add_find_right)
with h(1) show ?thesis
apply (unfold tprog_set_def)
by (smt mem_Collect_eq)
next
assume "map_of pg3 i = Some inst"
hence "(map_of pg2 ++ map_of pg3) i = Some inst"
by (metis map_add_find_right)
with h(1) show ?thesis
apply (unfold map_comm)
apply (unfold tprog_set_def)
by (smt mem_Collect_eq)
qed
qed
qed
qed
lemma assumes "assemble i c = Some (prog, j)"
shows "(i:[c]:j) (tprog_set (map_of prog))"
proof -
from assms obtain x lno
where "(assembleM i c) = Some (x, (j, lno, prog))"
apply(unfold assemble_def)
by (cases "(assembleM i c)", auto)
then obtain y pos lno' lmap where
"execute (pass1 c) (i, 0, empty) = Some (y, (pos, lno', lmap))"
"execute (pass2 c lmap) (i, 0, []) = Some (x, (j, lno, prog))"
apply (unfold assembleM_def)
by (cases "execute (pass1 c) (i, 0, Map.empty)", auto simp:Option.bind.simps)
hence mid: "effect (pass1 c) (i, 0, empty) (pos, lno', lmap) y"
"effect (pass2 c lmap) (i, 0, []) (j, lno, prog) x"
by (auto intro:effectI)
{ fix lnos lmap lmap' prog1 prog2
assume "effect (pass2 c lmap') (i, lnos, prog1) (j, lno, prog2) x"
hence "\<exists> prog. (prog2 = prog@prog1 \<and> (i:[c]:j) (tprog_set (map_of prog)) \<and>
(\<forall> k \<in> fst ` (set prog). i \<le> k \<and> k < j) \<and> i \<le> j)"
proof(induct c arbitrary:lmap' i lnos prog1 j lno prog2 x)
case (TInstr instr lmap' i lnos prog1 j lno prog2 x)
thus ?case
apply (auto simp: effect_def assemble_def assembleM_def execute.simps sm_map_def sm_def
tprog_set_def tassemble_to.simps sg_def pass1.simps pass2.simps
split:if_splits)
by (cases instr, auto)
next
case (TLabel l lmap' i lnos prog1 j lno prog2 x)
thus ?case
apply (rule_tac x = "[]" in exI)
apply (unfold tassemble_to.simps)
by (auto simp: effect_def assemble_def assembleM_def execute.simps sm_map_def sm_def
tprog_set_def tassemble_to.simps sg_def pass1.simps pass2.simps tap_def bind_def
return_def raise_def sep_empty_def set_ins_def
split:if_splits)
next
case (TSeq c1 c2 lmap' i lnos prog1 j lno prog2 x)
from TSeq(3)
obtain h' r where
"effect (pass2 c1 lmap') (i, lnos, prog1) h' r"
"effect (pass2 c2 lmap') h' (j, lno, prog2) x"
apply (unfold pass2.simps)
by (auto elim!:effect_elims)
then obtain pos1 lno1 pg1
where h:
"effect (pass2 c1 lmap') (i, lnos, prog1) (pos1, lno1, pg1) r"
"effect (pass2 c2 lmap') (pos1, lno1, pg1) (j, lno, prog2) x"
by (cases h', auto)
from TSeq(1)[OF h(1)] TSeq(2)[OF h(2)]
obtain pg2 pg3
where hh: "pg1 = pg2 @ prog1 \<and> (i :[ c1 ]: pos1) (tprog_set (map_of pg2))"
"(\<forall>k\<in> fst ` (set pg2). i \<le> k \<and> k < pos1)"
"i \<le> pos1"
"prog2 = pg3 @ pg1 \<and> (pos1 :[ c2 ]: j) (tprog_set (map_of pg3))"
"(\<forall>k\<in>fst ` (set pg3). pos1 \<le> k \<and> k < j)"
"pos1 \<le> j"
by auto
thus ?case
apply (rule_tac x = "pg3 @ pg2" in exI, auto)
apply (unfold tassemble_to.simps)
apply (rule_tac x = pos1 in EXS_intro)
my_block have
"(tprog_set (map_of pg2 ++ map_of pg3)) = tprog_set (map_of pg2) \<union> tprog_set (map_of pg3)"
proof(rule tprog_set_union)
from hh(2, 5) show "fst ` set pg2 \<inter> fst ` set pg3 = {}"
by (smt disjoint_iff_not_equal)
qed
my_block_end
apply (unfold this, insert this)
my_block
have "tprog_set (map_of pg2) \<inter> tprog_set (map_of pg3) = {}"
proof -
{ fix x
assume h: "x \<in> tprog_set (map_of pg2)" "x \<in> tprog_set (map_of pg3)"
then obtain i inst where "x = TC i inst"
"map_of pg2 i = Some inst"
"map_of pg3 i = Some inst"
apply (unfold tprog_set_def)
by (smt mem_Collect_eq tresource.inject(2))
hence "(i, inst) \<in> set pg2" "(i, inst) \<in> set pg3"
by (metis map_of_SomeD)+
with hh(2, 5)
have "False"
by (smt rev_image_eqI)
} thus ?thesis by auto
qed
my_block_end
apply (insert this)
apply (fold set_ins_def)
by (rule sep_conjI, assumption+, simp)
next
case (TLocal body lmap' i lnos prog1 j lno prog2 x)
from TLocal(2)
obtain l where h:
"lmap' lnos = Some l"
"effect (pass2 (body l) lmap') (i, Suc lnos, prog1) (j, lno, prog2) ()"
apply (unfold pass2.simps)
by (auto elim!:effect_elims split:option.splits simp:sm_map_def)
from TLocal(1)[OF this(2)]
obtain pg where hh: "prog2 = pg @ prog1 \<and> (i :[ body l ]: j) (tprog_set (map_of pg))"
"(\<forall>k\<in> fst ` (set pg). i \<le> k \<and> k < j)"
"i \<le> j"
by auto
thus ?case
apply (rule_tac x = pg in exI, auto)
apply (unfold tassemble_to.simps)
by (rule_tac x = l in EXS_intro, auto)
qed
} from this[OF mid(2)] show ?thesis by auto
qed
definition "valid_tpg tpg = (\<forall> i. \<exists> j prog. assemble i tpg = Some (j, prog))"
section {* A new method based on DB indexing *}
text {*
In this section, we introduced a new method based on DB-indexing to provide a quick check of
assemblebility of TM assmbly programs in the format of @{text "tpg"}. The
lemma @{text "ct_left_until_zero"} at the end shows how the well-formedness of @{text "left_until_zero"}
is proved in a modular way.
*}
datatype cpg =
CInstr tm_inst
| CLabel nat
| CSeq cpg cpg
| CLocal cpg
datatype status = Free | Bound
definition "lift_b t i j = (if (j \<ge> t) then (j + i) else j)"
fun lift_t :: "nat \<Rightarrow> nat \<Rightarrow> cpg \<Rightarrow> cpg"
where "lift_t t i (CInstr ((act0, l0), (act1, l1))) =
(CInstr ((act0, lift_b t i l0), (act1, lift_b t i l1)))" |
"lift_t t i (CLabel l) = CLabel (lift_b t i l)" |
"lift_t t i (CSeq c1 c2) = CSeq (lift_t t i c1) (lift_t t i c2)" |
"lift_t t i (CLocal c) = CLocal (lift_t (t + 1) i c)"
definition "lift0 (i::nat) cpg = lift_t 0 i cpg"
definition "perm_b t i j k = (if ((k::nat) = i \<and> i < t \<and> j < t) then j else
if (k = j \<and> i < t \<and> j < t) then i else k)"
lemma inj_perm_b: "inj (perm_b t i j)"
proof(induct rule:injI)
case (1 x y)
thus ?case
by (unfold perm_b_def, auto split:if_splits)
qed
fun perm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> cpg \<Rightarrow> cpg"
where "perm t i j (CInstr ((act0, l0), (act1, l1))) =
(CInstr ((act0, perm_b t i j l0), (act1, perm_b t i j l1)))" |
"perm t i j (CLabel l) = CLabel (perm_b t i j l)" |
"perm t i j (CSeq c1 c2) = CSeq (perm t i j c1) (perm t i j c2)" |
"perm t i j (CLocal c) = CLocal (perm (t + 1) (i + 1) (j + 1) c)"
definition "map_idx f sts = map (\<lambda> k. sts!(f (nat k))) [0 .. int (length sts) - 1]"
definition "perm_s i j sts = map_idx (perm_b (length sts) i j) sts"
value "perm_s 2 5 [(0::int), 1, 2, 3, 4, 5, 6, 7, 8, 9, 10]"
lemma "perm_s 2 20 [(0::int), 1, 2, 3, 4, 5, 6, 7, 8, 9, 10] = x"
apply (unfold perm_s_def map_idx_def perm_b_def, simp add:upto.simps)
oops
lemma upto_len: "length [i .. j] = (if j < i then 0 else (nat (j - i + 1)))"
proof(induct i j rule:upto.induct)
case (1 i j)
show ?case
proof(cases "j < i")
case True
thus ?thesis by simp
next
case False
hence eq_ij: "[i..j] = i # [i + 1..j]" by (simp add:upto.simps)
from 1 False
show ?thesis
by (auto simp:eq_ij)
qed
qed
lemma perm_s_len: "length (perm_s i j sts') = length sts'"
apply (unfold perm_s_def map_idx_def)
by (smt Nil_is_map_conv length_0_conv length_greater_0_conv length_map neq_if_length_neq upto_len)
fun c2t :: "nat list \<Rightarrow> cpg \<Rightarrow> tpg" where
"c2t env (CInstr ((act0, st0), (act1, st1))) = TInstr ((act0, env!st0), (act1, env!st1))" |
"c2t env (CLabel l) = TLabel (env!l)" |
"c2t env (CSeq cpg1 cpg2) = TSeq (c2t env cpg1) (c2t env cpg2)" |
"c2t env (CLocal cpg) = TLocal (\<lambda> x. c2t (x#env) cpg)"
instantiation status :: minus
begin
fun minus_status :: "status \<Rightarrow> status \<Rightarrow> status" where
"minus_status Bound Bound = Free" |
"minus_status Bound Free = Bound" |
"minus_status Free x = Free "
instance ..
end
instantiation status :: plus
begin
fun plus_status :: "status \<Rightarrow> status \<Rightarrow> status" where
"plus_status Free x = x" |
"plus_status Bound x = Bound"
instance ..
end
instantiation list :: (plus)plus
begin
fun plus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"plus_list [] ys = []" |
"plus_list (x#xs) [] = []" |
"plus_list (x#xs) (y#ys) = ((x + y)#plus_list xs ys)"
instance ..
end
instantiation list :: (minus)minus
begin
fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"minus_list [] ys = []" |
"minus_list (x#xs) [] = []" |
"minus_list (x#xs) (y#ys) = ((x - y)#minus_list xs ys)"
instance ..
end
(* consts castr :: "nat list \<Rightarrow> nat \<Rightarrow> cpg \<Rightarrow> nat \<Rightarrow> tassert"
definition "castr env i cpg j = (i:[c2t env cpg]:j)" *)
(*
definition
"c2p sts i cpg j = (\<forall> x. ((length x = length sts \<and>
(\<forall> k < length sts. sts!k = Bound \<longrightarrow> (\<exists> f. x!k = f i)))
\<longrightarrow> (\<exists> s. (i:[(c2t x cpg)]:j) s)))"
*)
definition
"c2p sts i cpg j =
(\<exists> f. \<forall> x. ((length x = length sts \<and>
(\<forall> k < length sts. sts!k = Bound \<longrightarrow> (x!k = f i k)))
\<longrightarrow> (\<exists> s. (i:[(c2t x cpg)]:j) s)))"
fun wf_cpg_test :: "status list \<Rightarrow> cpg \<Rightarrow> (bool \<times> status list)" where
"wf_cpg_test sts (CInstr ((a0, l0), (a1, l1))) = ((l0 < length sts \<and> l1 < length sts), sts)" |
"wf_cpg_test sts (CLabel l) = ((l < length sts) \<and> sts!l = Free, sts[l:=Bound])" |
"wf_cpg_test sts (CSeq c1 c2) = (let (b1, sts1) = wf_cpg_test sts c1;
(b2, sts2) = wf_cpg_test sts1 c2 in
(b1 \<and> b2, sts2))" |
"wf_cpg_test sts (CLocal body) = (let (b, sts') = (wf_cpg_test (Free#sts) body) in
(b, tl sts'))"
instantiation status :: order
begin
definition less_eq_status_def: "((st1::status) \<le> st2) = (st1 = Free \<or> st2 = Bound)"
definition less_status_def: "((st1::status) < st2) = (st1 \<le> st2 \<and> st1 \<noteq> st2)"
instance
proof
fix x y
show "(x < (y::status)) = (x \<le> y \<and> \<not> y \<le> x)"
by (metis less_eq_status_def less_status_def status.distinct(1))
next
fix x show "x \<le> (x::status)"
by (metis (full_types) less_eq_status_def status.exhaust)
next
fix x y z
assume "x \<le> y" "y \<le> (z::status)" show "x \<le> (z::status)"
by (metis `x \<le> y` `y \<le> z` less_eq_status_def status.distinct(1))
next
fix x y
assume "x \<le> y" "y \<le> (x::status)" show "x = y"
by (metis `x \<le> y` `y \<le> x` less_eq_status_def status.distinct(1))
qed
end
instantiation list :: (order)order
begin
definition "((sts::('a::order) list) \<le> sts') =
((length sts = length sts') \<and> (\<forall> i < length sts. sts!i \<le> sts'!i))"
definition "((sts::('a::order) list) < sts') = ((sts \<le> sts') \<and> sts \<noteq> sts')"
lemma anti_sym: assumes h: "x \<le> (y::'a list)" "y \<le> x"
shows "x = y"
proof -
from h have "length x = length y"
by (metis less_eq_list_def)
moreover from h have " (\<forall> i < length x. x!i = y!i)"
by (metis (full_types) antisym_conv less_eq_list_def)
ultimately show ?thesis
by (metis nth_equalityI)
qed
lemma refl: "x \<le> (x::('a::order) list)"
apply (unfold less_eq_list_def)
by (metis order_refl)
instance
proof
fix x y
show "((x::('a::order) list) < y) = (x \<le> y \<and> \<not> y \<le> x)"
proof
assume h: "x \<le> y \<and> \<not> y \<le> x"
have "x \<noteq> y"
proof
assume "x = y" with h have "\<not> (x \<le> x)" by simp
with refl show False by auto
qed
moreover from h have "x \<le> y" by blast
ultimately show "x < y" by (auto simp:less_list_def)
next
assume h: "x < y"
hence hh: "x \<le> y"
by (metis TM_Assemble.less_list_def)
moreover have "\<not> y \<le> x"
proof
assume "y \<le> x"
from anti_sym[OF hh this] have "x = y" .
with h show False
by (metis less_list_def)
qed
ultimately show "x \<le> y \<and> \<not> y \<le> x" by auto
qed
next
fix x from refl show "(x::'a list) \<le> x" .
next
fix x y assume "(x::'a list) \<le> y" "y \<le> x"
from anti_sym[OF this] show "x = y" .
next
fix x y z
assume h: "(x::'a list) \<le> y" "y \<le> z"
show "x \<le> z"
proof -
from h have "length x = length z" by (metis TM_Assemble.less_eq_list_def)
moreover from h have "\<forall> i < length x. x!i \<le> z!i"
by (metis TM_Assemble.less_eq_list_def order_trans)
ultimately show "x \<le> z"
by (metis TM_Assemble.less_eq_list_def)
qed
qed
end
lemma sts_bound_le: "sts \<le> sts[l := Bound]"
proof -
have "length sts = length (sts[l := Bound])"
by (metis length_list_update)
moreover have "\<forall> i < length sts. sts!i \<le> (sts[l:=Bound])!i"
proof -
{ fix i
assume "i < length sts"
have "sts ! i \<le> sts[l := Bound] ! i"
proof(cases "l < length sts")
case True
note le_l = this
show ?thesis
proof(cases "l = i")
case True with le_l
have "sts[l := Bound] ! i = Bound" by auto
thus ?thesis by (metis less_eq_status_def)
next
case False
with le_l have "sts[l := Bound] ! i = sts!i" by auto
thus ?thesis by auto
qed
next
case False
hence "sts[l := Bound] = sts" by auto
thus ?thesis by auto
qed
} thus ?thesis by auto
qed
ultimately show ?thesis by (metis less_eq_list_def)
qed
lemma sts_tl_le:
assumes "sts \<le> sts'"
shows "tl sts \<le> tl sts'"
proof -
from assms have "length (tl sts) = length (tl sts')"
by (metis (hide_lams, no_types) length_tl less_eq_list_def)
moreover from assms have "\<forall> i < length (tl sts). (tl sts)!i \<le> (tl sts')!i"
by (smt calculation length_tl less_eq_list_def nth_tl)
ultimately show ?thesis
by (metis less_eq_list_def)
qed
lemma wf_cpg_test_le:
assumes "wf_cpg_test sts cpg = (True, sts')"
shows "sts \<le> sts'" using assms
proof(induct cpg arbitrary:sts sts')
case (CInstr instr sts sts')
obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))"
by (metis prod.exhaust)
from CInstr[unfolded this]
show ?case by simp
next
case (CLabel l sts sts')
thus ?case by (auto simp:sts_bound_le)
next
case (CLocal body sts sts')
from this(2)
obtain sts1 where h: "wf_cpg_test (Free # sts) body = (True, sts1)" "sts' = tl sts1"
by (auto split:prod.splits)
from CLocal(1)[OF this(1)] have "Free # sts \<le> sts1" .
from sts_tl_le[OF this]
have "sts \<le> tl sts1" by simp
from this[folded h(2)]
show ?case .
next
case (CSeq cpg1 cpg2 sts sts')
from this(3)
show ?case
by (auto split:prod.splits dest!:CSeq(1, 2))
qed
lemma c2p_assert:
assumes "(c2p [] i cpg j)"
shows "\<exists> s. (i :[(c2t [] cpg)]: j) s"
proof -
from assms obtain f where
h [rule_format]:
"\<forall> x. length x = length [] \<and> (\<forall>k<length []. [] ! k = Bound \<longrightarrow> (x ! k = f i k)) \<longrightarrow>
(\<exists> s. (i :[ c2t [] cpg ]: j) s)"
by (unfold c2p_def, auto)
have "length [] = length [] \<and> (\<forall>k<length []. [] ! k = Bound \<longrightarrow> ([] ! k = f i k))"
by auto
from h[OF this] obtain s where "(i :[ c2t [] cpg ]: j) s" by blast
thus ?thesis by auto
qed
definition "sts_disj sts sts' = ((length sts = length sts') \<and>
(\<forall> i < length sts. \<not>(sts!i = Bound \<and> sts'!i = Bound)))"
lemma length_sts_plus:
assumes "length (sts1 :: status list) = length sts2"
shows "length (sts1 + sts2) = length sts1"
using assms
proof(induct sts1 arbitrary: sts2)
case Nil
thus ?case
by (metis plus_list.simps(1))
next
case (Cons s' sts' sts2)
thus ?case
proof(cases "sts2 = []")
case True
with Cons show ?thesis by auto
next
case False
then obtain s'' sts'' where eq_sts2: "sts2 = s''#sts''"
by (metis neq_Nil_conv)
with Cons
show ?thesis
by (metis length_Suc_conv list.inject plus_list.simps(3))
qed
qed
lemma nth_sts_plus:
assumes "i < length ((sts1::status list) + sts2)"
shows "(sts1 + sts2)!i = sts1!i + sts2!i"
using assms
proof(induct sts1 arbitrary:i sts2)
case (Nil i sts2)
thus ?case by auto
next
case (Cons s' sts' i sts2)
show ?case
proof(cases "sts2 = []")
case True
with Cons show ?thesis by auto
next
case False
then obtain s'' sts'' where eq_sts2: "sts2 = s''#sts''"
by (metis neq_Nil_conv)
with Cons
show ?thesis
by (smt list.size(4) nth_Cons' plus_list.simps(3))
qed
qed
lemma nth_sts_minus:
assumes "i < length ((sts1::status list) - sts2)"
shows "(sts1 - sts2)!i = sts1!i - sts2!i"
using assms
proof(induct arbitrary:i rule:minus_list.induct)
case (3 x xs y ys i)
show ?case
proof(cases i)
case 0
thus ?thesis by simp
next
case (Suc k)
with 3(2) have "k < length (xs - ys)" by auto
from 3(1)[OF this] and Suc
show ?thesis
by auto
qed
qed auto
fun taddr :: "tresource \<Rightarrow> nat" where
"taddr (TC i instr) = i"
lemma tassemble_to_range:
assumes "(i :[tpg]: j) s"
shows "(i \<le> j) \<and> (\<forall> r \<in> s. i \<le> taddr r \<and> taddr r < j)"
using assms
proof(induct tpg arbitrary: i j s)
case (TInstr instr i j s)
obtain a0 l0 a1 l1 where "instr = ((a0, l0), (a1, l1))"
by (metis pair_collapse)
with TInstr
show ?case
apply (simp add:tassemble_to.simps sg_def)
by (smt `instr = ((a0, l0), a1, l1)` cond_eq cond_true_eq1
empty_iff insert_iff le_refl lessI sep.mult_commute taddr.simps)
next
case (TLabel l i j s)
thus ?case
apply (simp add:tassemble_to.simps)
by (smt equals0D pasrt_def set_zero_def)
next
case (TSeq c1 c2 i j s)
from TSeq(3) obtain s1 s2 j' where
h: "(i :[ c1 ]: j') s1" "(j' :[ c2 ]: j) s2" "s1 ## s2" "s = s1 + s2"
by (auto simp:tassemble_to.simps elim!:EXS_elim sep_conjE)
show ?case
proof -
{ fix r
assume "r \<in> s"
with h (3, 4) have "r \<in> s1 \<or> r \<in> s2"
by (auto simp:set_ins_def)
hence "i \<le> j \<and> i \<le> taddr r \<and> taddr r < j"
proof
assume " r \<in> s1"
from TSeq(1)[OF h(1)]
have "i \<le> j'" "(\<forall>r\<in>s1. i \<le> taddr r \<and> taddr r < j')" by auto
from this(2)[rule_format, OF `r \<in> s1`]
have "i \<le> taddr r" "taddr r < j'" by auto
with TSeq(2)[OF h(2)]
show ?thesis by auto
next
assume "r \<in> s2"
from TSeq(2)[OF h(2)]
have "j' \<le> j" "(\<forall>r\<in>s2. j' \<le> taddr r \<and> taddr r < j)" by auto
from this(2)[rule_format, OF `r \<in> s2`]
have "j' \<le> taddr r" "taddr r < j" by auto
with TSeq(1)[OF h(1)]
show ?thesis by auto
qed
} thus ?thesis
by (smt TSeq.hyps(1) TSeq.hyps(2) h(1) h(2))
qed
next
case (TLocal body i j s)
from this(2) obtain l s' where "(i :[ body l ]: j) s"
by (simp add:tassemble_to.simps, auto elim!:EXS_elim)
from TLocal(1)[OF this]
show ?case by auto
qed
lemma c2p_seq:
assumes "c2p sts1 i cpg1 j'"
"c2p sts2 j' cpg2 j"
"sts_disj sts1 sts2"
shows "(c2p (sts1 + sts2) i (CSeq cpg1 cpg2) j)"
proof -
from assms(1)[unfolded c2p_def]
obtain f1 where
h1[rule_format]:
"\<forall>x. length x = length sts1 \<and> (\<forall>k<length sts1. sts1 ! k = Bound \<longrightarrow> (x ! k = f1 i k)) \<longrightarrow>
Ex (i :[ c2t x cpg1 ]: j')" by blast
from assms(2)[unfolded c2p_def]
obtain f2 where h2[rule_format]:
"\<forall>x. length x = length sts2 \<and> (\<forall>k<length sts2. sts2 ! k = Bound \<longrightarrow> (x ! k = f2 j' k)) \<longrightarrow>
Ex (j' :[ c2t x cpg2 ]: j)" by blast
from assms(3)[unfolded sts_disj_def]
have h3: "length sts1 = length sts2"
and h4[rule_format]:
"(\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> sts2 ! i = Bound))" by auto
let ?f = "\<lambda> i k. if (sts1!k = Bound) then f1 i k else f2 j' k"
{ fix x
assume h5: "length x = length (sts1 + sts2)" and
h6[rule_format]: "(\<forall>k<length (sts1 + sts2). (sts1 + sts2) ! k = Bound \<longrightarrow> x ! k = ?f i k)"
obtain s1 where h_s1: "(i :[ c2t x cpg1 ]: j') s1"
proof(atomize_elim, rule h1)
from h3 h5 have "length x = length sts1"
by (metis length_sts_plus)
moreover {
fix k assume hh: "k<length sts1" "sts1 ! k = Bound"
from hh(1) h3 h5 have p1: "k < length (sts1 + sts2)"
by (metis calculation)
from h3 hh(2) have p2: "(sts1 + sts2)!k = Bound"
by (metis nth_sts_plus p1 plus_status.simps(2))
from h6[OF p1 p2] have "x ! k = (if sts1 ! k = Bound then f1 i k else f2 j' k)" .
with hh(2)
have "x ! k = f1 i k" by simp
} ultimately show "length x = length sts1 \<and>
(\<forall>k<length sts1. sts1 ! k = Bound \<longrightarrow> (x ! k = f1 i k))"
by blast
qed
obtain s2 where h_s2: "(j' :[ c2t x cpg2 ]: j) s2"
proof(atomize_elim, rule h2)
from h3 h5 have "length x = length sts2"
by (metis length_sts_plus)
moreover {
fix k
assume hh: "k<length sts2" "sts2 ! k = Bound"
from hh(1) h3 h5 have p1: "k < length (sts1 + sts2)"
by (metis calculation)
from hh(1) h3 h5 hh(2) have p2: "(sts1 + sts2)!k = Bound"
by (metis `length sts1 = length sts2 \<and>
(\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> sts2 ! i = Bound))`
calculation nth_sts_plus plus_status.simps(1) status.distinct(1) status.exhaust)
from h6[OF p1 p2] have "x ! k = (if sts1 ! k = Bound then f1 i k else f2 j' k)" .
moreover from h4[OF hh(1)[folded h3]] hh(2) have "sts1!k \<noteq> Bound" by auto
ultimately have "x!k = f2 j' k" by simp
} ultimately show "length x = length sts2 \<and>
(\<forall>k<length sts2. sts2 ! k = Bound \<longrightarrow> (x ! k = f2 j' k))"
by blast
qed
have h_s12: "s1 ## s2"
proof -
{ fix r assume h: "r \<in> s1" "r \<in> s2"
with h_s1 h_s2
have "False"by (smt tassemble_to_range)
} thus ?thesis by (auto simp:set_ins_def)
qed
have "(EXS j'. i :[ c2t x cpg1 ]: j' \<and>* j' :[ c2t x cpg2 ]: j) (s1 + s2)"
proof(rule_tac x = j' in EXS_intro)
from h_s1 h_s2 h_s12
show "(i :[ c2t x cpg1 ]: j' \<and>* j' :[ c2t x cpg2 ]: j) (s1 + s2)"
by (metis sep_conjI)
qed
hence "\<exists> s. (i :[ c2t x (CSeq cpg1 cpg2) ]: j) s"
by (auto simp:tassemble_to.simps)
}
hence "\<exists>f. \<forall>x. length x = length (sts1 + sts2) \<and>
(\<forall>k<length (sts1 + sts2). (sts1 + sts2) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>
Ex (i :[ c2t x (CSeq cpg1 cpg2) ]: j)"
by (rule_tac x = ?f in exI, auto)
thus ?thesis
by(unfold c2p_def, auto)
qed
lemma plus_list_len:
"length ((sts1::status list) + sts2) = min (length sts1) (length sts2)"
by(induct rule:plus_list.induct, auto)
lemma minus_list_len:
"length ((sts1::status list) - sts2) = min (length sts1) (length sts2)"
by(induct rule:minus_list.induct, auto)
lemma sts_le_comb:
assumes "sts1 \<le> sts2"
and "sts2 \<le> sts3"
shows "sts_disj (sts2 - sts1) (sts3 - sts2)" and
"(sts3 - sts1) = (sts2 - sts1) + (sts3 - sts2)"
proof -
from assms
have h1: "length sts1 = length sts2" "\<forall>i<length sts1. sts1 ! i \<le> sts2 ! i"
and h2: "length sts2 = length sts3" "\<forall>i<length sts1. sts2 ! i \<le> sts3 ! i"
by (unfold less_eq_list_def, auto)
have "sts_disj (sts2 - sts1) (sts3 - sts2)"
proof -
from h1(1) h2(1)
have "length (sts2 - sts1) = length (sts3 - sts2)"
by (metis minus_list_len)
moreover {
fix i
assume lt_i: "i<length (sts2 - sts1)"
from lt_i h1(1) h2(1) have "i < length sts1"
by (smt minus_list_len)
from h1(2)[rule_format, of i, OF this] h2(2)[rule_format, of i, OF this]
have "sts1 ! i \<le> sts2 ! i" "sts2 ! i \<le> sts3 ! i" .
moreover have "(sts2 - sts1) ! i = sts2!i - sts1!i"
by (metis lt_i nth_sts_minus)
moreover have "(sts3 - sts2)!i = sts3!i - sts2!i"
by (metis `length (sts2 - sts1) = length (sts3 - sts2)` lt_i nth_sts_minus)
ultimately have " \<not> ((sts2 - sts1) ! i = Bound \<and> (sts3 - sts2) ! i = Bound)"
apply (cases "sts2!i", cases "sts1!i", cases "sts3!i", simp, simp)
apply (cases "sts3!i", simp, simp)
apply (cases "sts1!i", cases "sts3!i", simp, simp)
by (cases "sts3!i", simp, simp)
} ultimately show ?thesis by (unfold sts_disj_def, auto)
qed
moreover have "(sts3 - sts1) = (sts2 - sts1) + (sts3 - sts2)"
proof(induct rule:nth_equalityI)
case 1
show ?case by (metis h1(1) h2(1) length_sts_plus minus_list_len)
next
case 2
{ fix i
assume lt_i: "i<length (sts3 - sts1)"
have "(sts3 - sts1) ! i = (sts2 - sts1 + (sts3 - sts2)) ! i" (is "?L = ?R")
proof -
have "?R = sts2!i - sts1!i + (sts3!i - sts2!i)"
by (smt `i < length (sts3 - sts1)` h2(1) minus_list_len nth_sts_minus
nth_sts_plus plus_list_len)
moreover have "?L = sts3!i - sts1!i"
by (metis `i < length (sts3 - sts1)` nth_sts_minus)
moreover
have "sts2!i - sts1!i + (sts3!i - sts2!i) = sts3!i - sts1!i"
proof -
from lt_i h1(1) h2(1) have "i < length sts1"
by (smt minus_list_len)
from h1(2)[rule_format, of i, OF this] h2(2)[rule_format, of i, OF this]
show ?thesis
apply (cases "sts2!i", cases "sts1!i", cases "sts3!i", simp, simp)
apply (cases "sts3!i", simp, simp)
apply (cases "sts1!i", cases "sts3!i", simp, simp)
by (cases "sts3!i", simp, simp)
qed
ultimately show ?thesis by simp
qed
} thus ?case by auto
qed
ultimately show "sts_disj (sts2 - sts1) (sts3 - sts2)" and
"(sts3 - sts1) = (sts2 - sts1) + (sts3 - sts2)" by auto
qed
lemma wf_cpg_test_correct:
assumes "wf_cpg_test sts cpg = (True, sts')"
shows "(\<forall> i. \<exists> j. (c2p (sts' - sts) i cpg j))"
using assms
proof(induct cpg arbitrary:sts sts')
case (CInstr instr sts sts')
obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))"
by (metis prod.exhaust)
show ?case
proof(unfold eq_instr c2p_def, clarsimp simp:tassemble_to.simps)
fix i
let ?a = "Suc i" and ?f = "\<lambda> i k. i"
show "\<exists>a f. \<forall>x. length x = length (sts' - sts) \<and>
(\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>
Ex (sg {TC i ((a0, x ! l0), a1, x ! l1)} \<and>* <(a = Suc i)>)"
proof(rule_tac x = ?a in exI, rule_tac x = ?f in exI, default, clarsimp)
fix x
let ?j = "Suc i"
let ?s = " {TC i ((a0, x ! l0), a1, x ! l1)}"
have "(sg {TC i ((a0, x ! l0), a1, x ! l1)} \<and>* <(Suc i = Suc i)>) ?s"
by (simp add:tassemble_to.simps sg_def)
thus "Ex (sg {TC i ((a0, x ! l0), a1, x ! l1)})" by auto
qed
qed
next
case (CLabel l sts sts')
show ?case
proof
fix i
from CLabel
have h1: "l < length sts"
and h2: "sts ! l = Free"
and h3: "sts[l := Bound] = sts'" by auto
let ?f = "\<lambda> i k. i"
have "\<exists>a f. \<forall>x. length x = length (sts' - sts) \<and>
(\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f (i::nat) k) \<longrightarrow>
Ex (<(i = a \<and> a = x ! l)>)"
proof(rule_tac x = i in exI, rule_tac x = ?f in exI, clarsimp)
fix x
assume h[rule_format]:
"\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = i"
from h1 h3 have p1: "l < length (sts' - sts)"
by (metis length_list_update min.idem minus_list_len)
from p1 h2 h3 have p2: "(sts' - sts)!l = Bound"
by (metis h1 minus_status.simps(2) nth_list_update_eq nth_sts_minus)
from h[OF p1 p2] have "(<(i = x ! l)>) 0"
by (simp add:set_ins_def)
thus "\<exists> s. (<(i = x ! l)>) s" by auto
qed
thus "\<exists>a. c2p (sts' - sts) i (CLabel l) a"
by (auto simp:c2p_def tassemble_to.simps)
qed
next
case (CSeq cpg1 cpg2 sts sts')
show ?case
proof
fix i
from CSeq(3)[unfolded wf_cpg_test.simps]
show "\<exists> j. c2p (sts' - sts) i (CSeq cpg1 cpg2) j"
proof(let_elim)
case (LetE b1 sts1)
from this(1)
obtain b2 where h: "(b2, sts') = wf_cpg_test sts1 cpg2" "b1=True" "b2=True"
by (atomize_elim, unfold Let_def, auto split:prod.splits)
from wf_cpg_test_le[OF LetE(2)[symmetric, unfolded h(2)]]
have sts_le1: "sts \<le> sts1" .
from CSeq(1)[OF LetE(2)[unfolded h(2), symmetric], rule_format, of i]
obtain j1 where h1: "(c2p (sts1 - sts) i cpg1 j1)" by blast
from wf_cpg_test_le[OF h(1)[symmetric, unfolded h(3)]]
have sts_le2: "sts1 \<le> sts'" .
from sts_le_comb[OF sts_le1 sts_le2]
have hh: "sts_disj (sts1 - sts) (sts' - sts1)"
"sts' - sts = (sts1 - sts) + (sts' - sts1)" .
from CSeq(2)[OF h(1)[symmetric, unfolded h(3)], rule_format, of j1]
obtain j2 where h2: "(c2p (sts' - sts1) j1 cpg2 j2)" by blast
have "c2p (sts' - sts) i (CSeq cpg1 cpg2) j2"
by(unfold hh(2), rule c2p_seq[OF h1 h2 hh(1)])
thus ?thesis by blast
qed
qed
next
case (CLocal body sts sts')
from this(2) obtain b sts1 s where
h: "wf_cpg_test (Free # sts) body = (True, sts1)"
"sts' = tl sts1"
by (unfold wf_cpg_test.simps, auto split:prod.splits)
from wf_cpg_test_le[OF h(1), unfolded less_eq_list_def] h(2)
obtain s where eq_sts1: "sts1 = s#sts'"
by (metis Suc_length_conv list.size(4) tl.simps(2))
from CLocal(1)[OF h(1)] have p1: "\<forall>i. \<exists>a. c2p (sts1 - (Free # sts)) i body a" .
show ?case
proof
fix i
from p1[rule_format, of i] obtain j where "(c2p (sts1 - (Free # sts)) i body) j" by blast
then obtain f where hh [rule_format]:
"\<forall>x. length x = length (sts1 - (Free # sts)) \<and>
(\<forall>k<length (sts1 - (Free # sts)). (sts1 - (Free # sts)) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>
(\<exists>s. (i :[ c2t x body ]: j) s)"
by (auto simp:c2p_def)
let ?f = "\<lambda> i k. f i (Suc k)"
have "\<exists>j f. \<forall>x. length x = length (sts' - sts) \<and>
(\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>
(\<exists>s. (i :[ (TL xa. c2t (xa # x) body) ]: j) s)"
proof(rule_tac x = j in exI, rule_tac x = ?f in exI, default, clarsimp)
fix x
assume h1: "length x = length (sts' - sts)"
and h2: "\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f i (Suc k)"
let ?l = "f i 0" let ?x = " ?l#x"
from wf_cpg_test_le[OF h(1)] have "length (Free#sts) = length sts1"
by (unfold less_eq_list_def, simp)
with h1 h(2) have q1: "length (?l # x) = length (sts1 - (Free # sts))"
by (smt Suc_length_conv length_Suc_conv list.inject list.size(4)
minus_list.simps(3) minus_list_len tl.simps(2))
have q2: "(\<forall>k<length (sts1 - (Free # sts)).
(sts1 - (Free # sts)) ! k = Bound \<longrightarrow> (f i 0 # x) ! k = f i k)"
proof -
{ fix k
assume lt_k: "k<length (sts1 - (Free # sts))"
and bd_k: "(sts1 - (Free # sts)) ! k = Bound"
have "(f i 0 # x) ! k = f i k"
proof(cases "k")
case (Suc k')
moreover have "x ! k' = f i (Suc k')"
proof(rule h2[rule_format])
from bd_k Suc eq_sts1 show "(sts' - sts) ! k' = Bound" by simp
next
from Suc lt_k eq_sts1 show "k' < length (sts' - sts)" by simp
qed
ultimately show ?thesis by simp
qed simp
} thus ?thesis by auto
qed
from conjI[THEN hh[of ?x], OF q1 q2] obtain s
where h_s: "(i :[ c2t (f i 0 # x) body ]: j) s" by blast
thus "\<exists>s. (i :[ (TL xa. c2t (xa # x) body) ]: j) s"
apply (simp add:tassemble_to.simps)
by (rule_tac x = s in exI, rule_tac x = ?l in EXS_intro, simp)
qed
thus "\<exists>j. c2p (sts' - sts) i (CLocal body) j"
by (auto simp:c2p_def)
qed
qed
lemma
assumes "wf_cpg_test [] cpg = (True, sts')"
and "tpg = c2t [] cpg"
shows "\<forall> i. \<exists> j s. ((i:[tpg]:j) s)"
proof
fix i
have eq_sts_minus: "(sts' - []) = []"
by (metis list.exhaust minus_list.simps(1) minus_list.simps(2))
from wf_cpg_test_correct[OF assms(1), rule_format, of i]
obtain j where "c2p (sts' - []) i cpg j" by auto
from c2p_assert [OF this[unfolded eq_sts_minus]]
obtain s where "(i :[ c2t [] cpg ]: j) s" by blast
from this[folded assms(2)]
show " \<exists> j s. ((i:[tpg]:j) s)" by blast
qed
lemma replicate_nth: "(replicate n x @ sts) ! (l + n) = sts!l"
by (smt length_replicate nth_append)
lemma replicate_update:
"(replicate n x @ sts)[l + n := v] = replicate n x @ sts[l := v]"
by (smt length_replicate list_update_append)
lemma l_n_v_orig:
assumes "l0 < length env"
and "t \<le> l0"
shows "(take t env @ es @ drop t env) ! (l0 + length es) = env ! l0"
proof -
from assms(1, 2) have "t < length env" by auto
hence h: "env = take t env @ drop t env"
"length (take t env) = t"
apply (metis append_take_drop_id)
by (smt `t < length env` length_take)
with assms(2) have eq_sts_l: "env!l0 = (drop t env)!(l0 - t)"
by (metis nth_app)
from h(2) have "length (take t env @ es) = t + length es"
by (metis length_append length_replicate nat_add_commute)
moreover from assms(2) have "t + (length es) \<le> l0 + (length es)" by auto
ultimately have "((take t env @ es) @ drop t env)!(l0 + length es) =
(drop t env)!(l0+ length es - (t + length es))"
by (smt length_replicate length_splice nth_append)
with eq_sts_l[symmetric, unfolded assms]
show ?thesis by auto
qed
lemma l_n_v:
assumes "l < length sts"
and "sts!l = v"
and "t \<le> l"
shows "(take t sts @ replicate n x @ drop t sts) ! (l + n) = v"
proof -
from l_n_v_orig[OF assms(1) assms(3), of "replicate n x"]
and assms(2)
show ?thesis by auto
qed
lemma l_n_v_s:
assumes "l < length sts"
and "t \<le> l"
shows "(take t sts @ sts0 @ drop t sts)[l + length sts0 := v] =
take t (sts[l:=v])@ sts0 @ drop t (sts[l:=v])"
proof -
let ?n = "length sts0"
from assms(1, 2) have "t < length sts" by auto
hence h: "sts = take t sts @ drop t sts"
"length (take t sts) = t"
apply (metis append_take_drop_id)
by (smt `t < length sts` length_take)
with assms(2) have eq_sts_l: "sts[l:=v] = take t sts @ drop t sts [(l - t) := v]"
by (smt list_update_append)
with h(2) have eq_take_drop_t: "take t (sts[l:=v]) = take t sts"
"drop t (sts[l:=v]) = (drop t sts)[l - t:=v]"
apply (metis append_eq_conv_conj)
by (metis append_eq_conv_conj eq_sts_l h(2))
from h(2) have "length (take t sts @ sts0) = t + ?n"
by (metis length_append length_replicate nat_add_commute)
moreover from assms(2) have "t + ?n \<le> l + ?n" by auto
ultimately have "((take t sts @ sts0) @ drop t sts)[l + ?n := v] =
(take t sts @ sts0) @ (drop t sts)[(l + ?n - (t + ?n)) := v]"
by (smt list_update_append replicate_nth)
with eq_take_drop_t
show ?thesis by auto
qed
lemma l_n_v_s1:
assumes "l < length sts"
and "\<not> t \<le> l"
shows "(take t sts @ sts0 @ drop t sts)[l := v] =
take t (sts[l := v]) @ sts0 @ drop t (sts[l := v])"
proof(cases "t < length sts")
case False
hence h: "take t sts = sts" "drop t sts = []"
"take t (sts[l:=v]) = sts [l:=v]"
"drop t (sts[l:=v]) = []"
by auto
with assms(1)
show ?thesis
by (metis list_update_append)
next
case True
with assms(2)
have h: "(take t sts)[l:=v] = take t (sts[l:=v])"
"(sts[l:=v]) = (take t sts)[l:=v]@drop t sts"
"length (take t sts) = t"
apply (smt length_list_update length_take nth_equalityI nth_list_update nth_take)
apply (smt True append_take_drop_id assms(2) length_take list_update_append1)
by (smt True length_take)
from h(2,3) have "drop t (sts[l := v]) = drop t sts"
by (metis append_eq_conv_conj length_list_update)
with h(1)
show ?thesis
apply simp
by (metis assms(2) h(3) list_update_append1 not_leE)
qed
lemma l_n_v_s2:
assumes "l0 < length env"
and "t \<le> l0"
and "\<not> t \<le> l1"
shows "(take t env @ es @ drop t env) ! l1 = env ! l1"
proof -
from assms(1, 2) have "t < length env" by auto
hence h: "env = take t env @ drop t env"
"length (take t env) = t"
apply (metis append_take_drop_id)
by (smt `t < length env` length_take)
with assms(3) show ?thesis
by (smt nth_append)
qed
lemma l_n_v_s3:
assumes "l0 < length env"
and "\<not> t \<le> l0"
shows "(take t env @ es @ drop t env) ! l0 = env ! l0"
proof(cases "t < length env")
case True
hence h: "env = take t env @ drop t env"
"length (take t env) = t"
apply (metis append_take_drop_id)
by (smt `t < length env` length_take)
with assms(2) show ?thesis
by (smt nth_append)
next
case False
hence "take t env = env" by auto
with assms(1) show ?thesis
by (metis nth_append)
qed
lemma lift_wf_cpg_test:
assumes "wf_cpg_test sts cpg = (True, sts')"
shows "wf_cpg_test (take t sts @ sts0 @ drop t sts) (lift_t t (length sts0) cpg) =
(True, take t sts' @ sts0 @ drop t sts')"
using assms
proof(induct cpg arbitrary:t sts0 sts sts')
case (CInstr instr t sts0 sts sts')
obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))"
by (metis prod.exhaust)
from CInstr
show ?case
by (auto simp:eq_instr lift_b_def)
next
case (CLabel l t sts0 sts sts')
thus ?case
apply (auto simp:lift_b_def
replicate_nth replicate_update l_n_v_orig l_n_v_s)
apply (metis (mono_tags) diff_diff_cancel length_drop length_rev
linear not_less nth_append nth_take rev_take take_all)
by (simp add:l_n_v_s1)
next
case (CSeq c1 c2 sts0 sts sts')
thus ?case
by (auto simp: lift0_def lift_b_def split:prod.splits)
next
case (CLocal body t sts0 sts sts')
from this(2) obtain sts1 where h: "wf_cpg_test (Free # sts) body = (True, sts1)" "tl sts1 = sts'"
by (auto simp:lift0_def lift_b_def split:prod.splits)
let ?lift_s = "\<lambda> t sts. take t sts @ sts0 @ drop t sts"
have eq_lift_1: "(?lift_s (Suc t) (Free # sts)) = Free#?lift_s t sts"
by (simp)
from wf_cpg_test_le[OF h(1)] have "length (Free#sts) = length sts1"
by (unfold less_eq_list_def, simp)
hence eq_sts1: "sts1 = hd sts1 # tl sts1"
by (metis append_Nil append_eq_conv_conj hd.simps list.exhaust tl.simps(2))
from CLocal(1)[OF h(1), of "Suc t", of "sts0", unfolded eq_lift_1]
show ?case
apply (simp, subst eq_sts1, simp)
apply (simp add:h(2))
by (subst eq_sts1, simp add:h(2))
qed
lemma lift_c2t:
assumes "wf_cpg_test sts cpg = (True, sts')"
and "length env = length sts"
shows "c2t (take t env @ es @ drop t env) (lift_t t (length es) cpg) =
c2t env cpg"
using assms
proof(induct cpg arbitrary: t env es sts sts')
case (CInstr instr t env es sts sts')
obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))"
by (metis prod.exhaust)
from CInstr have h: "l0 < length env" "l1 < length env"
by (auto simp:eq_instr)
with CInstr(2)
show ?case
by (auto simp:eq_instr lift_b_def l_n_v_orig l_n_v_s2 l_n_v_s3)
next
case (CLabel l t env es sts sts')
thus ?case
by (auto simp:lift_b_def
replicate_nth replicate_update l_n_v_orig l_n_v_s3)
next
case (CSeq c1 c2 t env es sts sts')
from CSeq(3) obtain sts1
where h: "wf_cpg_test sts c1 = (True, sts1)" "wf_cpg_test sts1 c2 = (True, sts')"
by (auto split:prod.splits)
from wf_cpg_test_le[OF h(1)] have "length sts = length sts1"
by (auto simp:less_eq_list_def)
from CSeq(4)[unfolded this] have eq_len_env: "length env = length sts1" .
from CSeq(1)[OF h(1) CSeq(4)]
CSeq(2)[OF h(2) eq_len_env]
show ?case
by (auto simp: lift0_def lift_b_def split:prod.splits)
next
case (CLocal body t env es sts sts')
{ fix x
from CLocal(2)
obtain sts1 where h1: "wf_cpg_test (Free # sts) body = (True, sts1)"
by (auto split:prod.splits)
from CLocal(3) have "length (x#env) = length (Free # sts)" by simp
from CLocal(1)[OF h1 this, of "Suc t"]
have "c2t (x # take t env @ es @ drop t env) (lift_t (Suc t) (length es) body) =
c2t (x # env) body"
by simp
} thus ?case by simp
qed
pr 20
lemma upto_append:
assumes "x \<le> y + 1"
shows "[x .. y + 1] = [x .. y]@[y + 1]"
using assms
by (induct x y rule:upto.induct, auto simp:upto.simps)
lemma nth_upto:
assumes "l < length sts"
shows "[0..(int (length sts)) - 1]!l = int l"
using assms
proof(induct sts arbitrary:l)
case Nil
thus ?case by simp
next
case (Cons s sts l)
from Cons(2)
have "0 \<le> (int (length sts) - 1) + 1" by auto
from upto_append[OF this]
have eq_upto: "[0..int (length sts)] = [0..int (length sts) - 1] @ [int (length sts)]"
by simp
show ?case
proof(cases "l < length sts")
case True
with Cons(1)[OF True] eq_upto
show ?thesis
apply simp
by (smt nth_append take_eq_Nil upto_len)
next
case False
with Cons(2) have eq_l: "l = length sts" by simp
show ?thesis
proof(cases sts)
case (Cons x xs)
have "[0..1 + int (length xs)] = [0 .. int (length xs)]@[1 + int (length xs)]"
by (smt upto_append)
moreover have "length [0 .. int (length xs)] = Suc (length xs)"
by (smt upto_len)
moreover note Cons
ultimately show ?thesis
apply (simp add:eq_l)
by (smt nth_Cons' nth_append)
qed (simp add:upto_len upto.simps eq_l)
qed
qed
lemma map_idx_idx:
assumes "l < length sts"
shows "(map_idx f sts)!l = sts!(f l)"
proof -
from assms have lt_l: "l < length [0..int (length sts) - 1]"
by (smt upto_len)
show ?thesis
apply (unfold map_idx_def nth_map[OF lt_l])
by (metis assms nat_int nth_upto)
qed
lemma map_idx_len: "length (map_idx f sts) = length sts"
apply (unfold map_idx_def)
by (smt length_map upto_len)
lemma map_idx_eq:
assumes "\<forall> l < length sts. f l = g l"
shows "map_idx f sts = map_idx g sts"
proof(induct rule: nth_equalityI)
case 1
show "length (map_idx f sts) = length (map_idx g sts)"
by (metis map_idx_len)
next
case 2
{ fix l
assume "l < length (map_idx f sts)"
hence "l < length sts"
by (metis map_idx_len)
from map_idx_idx[OF this] and assms and this
have "map_idx f sts ! l = map_idx g sts ! l"
by (smt list_eq_iff_nth_eq map_idx_idx map_idx_len)
} thus ?case by auto
qed
lemma perm_s_commut: "perm_s i j sts = perm_s j i sts"
apply (unfold perm_s_def, rule map_idx_eq, unfold perm_b_def)
by smt
lemma map_idx_id: "map_idx id sts = sts"
proof(induct rule:nth_equalityI)
case 1
from map_idx_len show "length (map_idx id sts) = length sts" .
next
case 2
{ fix l
assume "l < length (map_idx id sts)"
from map_idx_idx[OF this[unfolded map_idx_len]]
have "map_idx id sts ! l = sts ! l" by simp
} thus ?case by auto
qed
lemma perm_s_lt_i:
assumes "\<not> i < length sts"
shows "perm_s i j sts = sts"
proof -
have "map_idx (perm_b (length sts) i j) sts = map_idx id sts"
proof(rule map_idx_eq, default, clarsimp)
fix l
assume "l < length sts"
with assms
show "perm_b (length sts) i j l = l"
by (unfold perm_b_def, auto)
qed
with map_idx_id
have "map_idx (perm_b (length sts) i j) sts = sts" by simp
thus ?thesis by (simp add:perm_s_def)
qed
lemma perm_s_lt:
assumes "\<not> i < length sts \<or> \<not> j < length sts"
shows "perm_s i j sts = sts"
using assms
proof
assume "\<not> i < length sts"
from perm_s_lt_i[OF this] show ?thesis .
next
assume "\<not> j < length sts"
from perm_s_lt_i[OF this, of i, unfolded perm_s_commut]
show ?thesis .
qed
lemma perm_s_update_i:
assumes "i < length sts"
and "j < length sts"
shows "sts ! i = perm_s i j sts ! j"
proof -
from map_idx_idx[OF assms(2)]
have "map_idx (perm_b (length sts) i j) sts ! j = sts!(perm_b (length sts) i j j)" .
with assms
show ?thesis
by (auto simp:perm_s_def perm_b_def)
qed
lemma nth_perm_s_neq:
assumes "l \<noteq> j"
and "l \<noteq> i"
and "l < length sts"
shows "sts ! l = perm_s i j sts ! l"
proof -
have "map_idx (perm_b (length sts) i j) sts ! l = sts!(perm_b (length sts) i j l)"
by (metis assms(3) map_idx_def map_idx_idx)
with assms
show ?thesis
by (unfold perm_s_def perm_b_def, auto)
qed
lemma map_idx_update:
assumes "f j = i"
and "inj f"
and "i < length sts"
and "j < length sts"
shows "map_idx f (sts[i:=v]) = map_idx f sts[j := v]"
proof(induct rule:nth_equalityI)
case 1
show "length (map_idx f (sts[i := v])) = length (map_idx f sts[j := v])"
by (metis length_list_update map_idx_len)
next
case 2
{ fix l
assume lt_l: "l < length (map_idx f (sts[i := v]))"
have eq_nth: "sts[i := v] ! f l = map_idx f sts[j := v] ! l"
proof(cases "f l = i")
case False
from lt_l have "l < length sts"
by (metis length_list_update map_idx_len)
from map_idx_idx[OF this, of f] have " map_idx f sts ! l = sts ! f l" .
moreover from False assms have "l \<noteq> j" by auto
moreover note False
ultimately show ?thesis by simp
next
case True
with assms have eq_l: "l = j"
by (metis inj_eq)
moreover from lt_l eq_l
have "j < length (map_idx f sts[j := v])"
by (metis length_list_update map_idx_len)
moreover note True assms
ultimately show ?thesis by simp
qed
from lt_l have "l < length (sts[i := v])"
by (metis map_idx_len)
from map_idx_idx[OF this] eq_nth
have "map_idx f (sts[i := v]) ! l = map_idx f sts[j := v] ! l" by simp
} thus ?case by auto
qed
lemma perm_s_update:
assumes "i < length sts"
and "j < length sts"
shows "(perm_s i j sts)[i := v] = perm_s i j (sts[j := v])"
proof -
have "map_idx (perm_b (length (sts[j := v])) i j) (sts[j := v]) =
map_idx (perm_b (length (sts[j := v])) i j) sts[i := v]"
proof(rule map_idx_update[OF _ _ assms(2, 1)])
from inj_perm_b show "inj (perm_b (length (sts[j := v])) i j)" .
next
from assms show "perm_b (length (sts[j := v])) i j i = j"
by (auto simp:perm_b_def)
qed
hence "map_idx (perm_b (length sts) i j) sts[i := v] =
map_idx (perm_b (length (sts[j := v])) i j) (sts[j := v])"
by simp
thus ?thesis by (simp add:perm_s_def)
qed
lemma perm_s_update_neq:
assumes "l \<noteq> i"
and "l \<noteq> j"
shows "perm_s i j sts[l := v] = perm_s i j (sts[l := v])"
proof(cases "i < length sts \<and> j < length sts")
case False
with perm_s_lt have "perm_s i j sts = sts" by auto
moreover have "perm_s i j (sts[l:=v]) = sts[l:=v]"
proof -
have "length (sts[l:=v]) = length sts" by auto
from False[folded this] perm_s_lt
show ?thesis by metis
qed
ultimately show ?thesis by simp
next
case True
note lt_ij = this
show ?thesis
proof(cases "l < length sts")
case False
hence "sts[l:=v] = sts" by auto
moreover have "perm_s i j sts[l := v] = perm_s i j sts"
proof -
from False and perm_s_len
have "\<not> l < length (perm_s i j sts)" by metis
thus ?thesis by auto
qed
ultimately show ?thesis by simp
next
case True
show ?thesis
proof -
have "map_idx (perm_b (length (sts[l := v])) i j) (sts[l := v]) =
map_idx (perm_b (length (sts[l := v])) i j) sts[l := v]"
proof(induct rule:map_idx_update [OF _ inj_perm_b True True])
case 1
from assms lt_ij
show ?case
by (unfold perm_b_def, auto)
qed
thus ?thesis
by (unfold perm_s_def, simp)
qed
qed
qed
lemma perm_sb: "(perm_s i j sts)[perm_b (length sts) i j l := v] = perm_s i j (sts[l := v])"
apply(subst perm_b_def, auto simp:perm_s_len perm_s_lt perm_s_update)
apply (subst perm_s_commut, subst (2) perm_s_commut, rule_tac perm_s_update, auto)
by (rule_tac perm_s_update_neq, auto)
lemma perm_s_id: "perm_s i i sts = sts" (is "?L = ?R")
proof -
from map_idx_id have "?R = map_idx id sts" by metis
also have "\<dots> = ?L"
by (unfold perm_s_def, rule map_idx_eq, unfold perm_b_def, auto)
finally show ?thesis by simp
qed
lemma upto_map:
assumes "i \<le> j"
shows "[i .. j] = i # map (\<lambda> x. x + 1) [i .. (j - 1)]"
using assms
proof(induct i j rule:upto.induct)
case (1 i j)
show ?case (is "?L = ?R")
proof -
from 1(2)
have eq_l: "?L = i # [i+1 .. j]" by (simp add:upto.simps)
show ?thesis
proof(cases "i + 1 \<le> j")
case False
with eq_l show ?thesis by (auto simp:upto.simps)
next
case True
have "[i + 1..j] = map (\<lambda>x. x + 1) [i..j - 1]"
by (smt "1.hyps" Cons_eq_map_conv True upto.simps)
with eq_l
show ?thesis by simp
qed
qed
qed
lemma perm_s_cons: "(perm_s (Suc i) (Suc j) (s # sts)) = s#perm_s i j sts"
proof -
have le_0: "0 \<le> int (length (s # sts)) - 1" by simp
have "map (\<lambda>k. (s # sts) ! perm_b (length (s # sts)) (Suc i) (Suc j) (nat k))
[0..int (length (s # sts)) - 1] =
s # map (\<lambda>k. sts ! perm_b (length sts) i j (nat k)) [0..int (length sts) - 1]"
by (unfold upto_map[OF le_0], auto simp:perm_b_def, smt+)
thus ?thesis by (unfold perm_s_def map_idx_def, simp)
qed
lemma perm_wf_cpg_test:
assumes "wf_cpg_test sts cpg = (True, sts')"
shows "wf_cpg_test (perm_s i j sts) (perm (length sts) i j cpg) =
(True, perm_s i j sts')"
using assms
proof(induct cpg arbitrary:t i j sts sts')
case (CInstr instr i j sts sts')
obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))"
by (metis prod.exhaust)
from CInstr
show ?case
apply (unfold eq_instr, clarsimp)
by (unfold perm_s_len perm_b_def, clarsimp)
next
case (CLabel l i j sts sts')
have "(perm_s i j sts)[perm_b (length sts) i j l := Bound] = perm_s i j (sts[l := Bound])"
by (metis perm_sb)
with CLabel
show ?case
apply (auto simp:perm_s_len perm_sb)
apply (subst perm_b_def, auto simp:perm_sb)
apply (subst perm_b_def, auto simp:perm_s_lt perm_s_update_i)
apply (unfold perm_s_id, subst perm_s_commut, simp add: perm_s_update_i[symmetric])
apply (simp add:perm_s_update_i[symmetric])
by (simp add: nth_perm_s_neq[symmetric])
next
case (CSeq c1 c2 i j sts sts')
thus ?case
apply (auto split:prod.splits)
apply (metis (hide_lams, no_types) less_eq_list_def prod.inject wf_cpg_test_le)
by (metis (hide_lams, no_types) less_eq_list_def prod.inject wf_cpg_test_le)
next
case (CLocal body i j sts sts')
from this(2) obtain sts1 where h: "wf_cpg_test (Free # sts) body = (True, sts1)" "tl sts1 = sts'"
by (auto simp:lift0_def lift_b_def split:prod.splits)
from wf_cpg_test_le[OF h(1)] have "length (Free#sts) = length sts1"
by (unfold less_eq_list_def, simp)
hence eq_sts1: "sts1 = hd sts1 # tl sts1"
by (metis append_Nil append_eq_conv_conj hd.simps list.exhaust tl.simps(2))
from CLocal(1)[OF h(1), of "Suc i" "Suc j"] h(2) eq_sts1
show ?case
apply (auto split:prod.splits simp:perm_s_cons)
by (metis perm_s_cons tl.simps(2))
qed
lemma nth_perm_sb:
assumes "l0 < length env"
shows "perm_s i j env ! perm_b (length env) i j l0 = env ! l0"
by (metis assms nth_perm_s_neq perm_b_def perm_s_commut perm_s_lt perm_s_update_i)
lemma perm_c2t:
assumes "wf_cpg_test sts cpg = (True, sts')"
and "length env = length sts"
shows "c2t (perm_s i j env) (perm (length env) i j cpg) =
c2t env cpg"
using assms
proof(induct cpg arbitrary:i j env sts sts')
case (CInstr instr i j env sts sts')
obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))"
by (metis prod.exhaust)
from CInstr have h: "l0 < length env" "l1 < length env"
by (auto simp:eq_instr)
with CInstr(2)
show ?case
apply (auto simp:eq_instr)
by (metis nth_perm_sb)+
next
case (CLabel l t env es sts sts')
thus ?case
apply (auto)
by (metis nth_perm_sb)
next
case (CSeq c1 c2 i j env sts sts')
from CSeq(3) obtain sts1
where h: "wf_cpg_test sts c1 = (True, sts1)" "wf_cpg_test sts1 c2 = (True, sts')"
by (auto split:prod.splits)
from wf_cpg_test_le[OF h(1)] have "length sts = length sts1"
by (auto simp:less_eq_list_def)
from CSeq(4)[unfolded this] have eq_len_env: "length env = length sts1" .
from CSeq(1)[OF h(1) CSeq(4)]
CSeq(2)[OF h(2) eq_len_env]
show ?case by auto
next
case (CLocal body i j env sts sts')
{ fix x
from CLocal(2, 3)
obtain sts1 where "wf_cpg_test (Free # sts) body = (True, sts1)"
"length (x#env) = length (Free # sts)"
by (auto split:prod.splits)
from CLocal(1)[OF this]
have "(c2t (x # perm_s i j env) (perm (Suc (length env)) (Suc i) (Suc j) body)) =
(c2t (x # env) body)"
by (metis Suc_length_conv perm_s_cons)
} thus ?case by simp
qed
lemma wf_cpg_test_disj_aux1:
assumes "sts_disj sts1 (sts[l := Bound] - sts)"
"l < length sts"
"sts ! l = Free"
shows "(sts1 + sts) ! l = Free"
proof -
from assms(1)[unfolded sts_disj_def]
have h: "length sts1 = length (sts[l := Bound] - sts)"
"(\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> (sts[l := Bound] - sts) ! i = Bound))"
by auto
from h(1) assms(2)
have lt_l: "l < length sts1"
"l < length (sts[l := Bound] - sts)"
"l < length (sts1 + sts)"
apply (smt length_list_update minus_list_len)
apply (smt assms(2) length_list_update minus_list_len)
by (smt assms(2) h(1) length_list_update length_sts_plus minus_list_len)
from h(2)[rule_format, of l, OF this(1)]
have " \<not> (sts1 ! l = Bound \<and> (sts[l := Bound] - sts) ! l = Bound)" .
with assms(3) nth_sts_minus[OF lt_l(2)] nth_sts_plus[OF lt_l(3)] assms(2)
show ?thesis
by (cases "sts1!l", auto)
qed
lemma wf_cpg_test_disj_aux2:
assumes "sts_disj sts1 (sts[l := Bound] - sts)"
" l < length sts"
shows "(sts1 + sts)[l := Bound] = sts1 + sts[l := Bound]"
proof -
from assms have lt_l: "l < length (sts1 + sts[l:=Bound])"
"l < length (sts1 + sts)"
apply (smt length_list_update length_sts_plus minus_list_len sts_disj_def)
by (smt assms(1) assms(2) length_list_update length_sts_plus minus_list_len sts_disj_def)
show ?thesis
proof(induct rule:nth_equalityI)
case 1
show ?case
by (smt assms(1) length_list_update length_sts_plus minus_list_len sts_disj_def)
next
case 2
{ fix i
assume lt_i: "i < length ((sts1 + sts)[l := Bound])"
have " (sts1 + sts)[l := Bound] ! i = (sts1 + sts[l := Bound]) ! i"
proof(cases "i = l")
case True
with nth_sts_plus[OF lt_l(1)] assms(2) nth_sts_plus[OF lt_l(2)] lt_l
show ?thesis
by (cases "sts1 ! l", auto)
next
case False
from lt_i have "i < length (sts1 + sts)" "i < length (sts1 + sts[l := Bound])"
apply auto
by (metis length_list_update plus_list_len)
from nth_sts_plus[OF this(1)] nth_sts_plus[OF this(2)] lt_i lt_l False
show ?thesis
by simp
qed
} thus ?case by auto
qed
qed
lemma sts_list_plus_commut:
shows "sts1 + sts2 = sts2 + (sts1:: status list)"
proof(induct rule:nth_equalityI)
case 1
show ?case
by (metis min.commute plus_list_len)
next
case 2
{ fix i
assume lt_i1: "i<length (sts1 + sts2)"
hence lt_i2: "i < length (sts2 + sts1)"
by (smt plus_list_len)
from nth_sts_plus[OF this] nth_sts_plus[OF lt_i1]
have "(sts1 + sts2) ! i = (sts2 + sts1) ! i"
apply simp
apply (cases "sts1!i", cases "sts2!i", auto)
by (cases "sts2!i", auto)
} thus ?case by auto
qed
lemma sts_disj_cons:
assumes "sts_disj sts1 sts2"
shows "sts_disj (Free # sts1) (s # sts2)"
using assms
proof -
from assms
have h: "length sts1 = length sts2"
"(\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> sts2 ! i = Bound))"
by (unfold sts_disj_def, auto)
from h(1) have "length (Free # sts1) = length (s # sts2)" by simp
moreover {
fix i
assume lt_i: "i<length (Free # sts1)"
have "\<not> ((Free # sts1) ! i = Bound \<and> (s # sts2) ! i = Bound)"
proof(cases "i")
case 0
thus ?thesis by simp
next
case (Suc k)
from h(2)[rule_format, of k] lt_i[unfolded Suc] Suc
show ?thesis by auto
qed
}
ultimately show ?thesis by (auto simp:sts_disj_def)
qed
lemma sts_disj_uncomb:
assumes "sts_disj sts (sts1 + sts2)"
and "sts_disj sts1 sts2"
shows "sts_disj sts sts1" "sts_disj sts sts2"
using assms
apply (smt assms(1) assms(2) length_sts_plus nth_sts_plus plus_status.simps(2) sts_disj_def)
by (smt assms(1) assms(2) length_sts_plus nth_sts_plus
plus_status.simps(2) sts_disj_def sts_list_plus_commut)
lemma wf_cpg_test_disj:
assumes "wf_cpg_test sts cpg = (True, sts')"
and "sts_disj sts1 (sts' - sts)"
shows "wf_cpg_test (sts1 + sts) cpg = (True, sts1 + sts')"
using assms
proof(induct cpg arbitrary:sts sts1 sts')
case (CInstr instr sts sts1 sts')
obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))"
by (metis pair_collapse)
with CInstr(1) have h: "l0 < length sts" "l1 < length sts" "sts = sts'" by auto
with CInstr eq_instr
show ?case
apply (auto)
by (smt length_sts_plus minus_list_len sts_disj_def)+
next
case (CLabel l sts sts1 sts')
thus ?case
apply auto
apply (smt length_list_update length_sts_plus minus_list_len sts_disj_def)
by (auto simp: wf_cpg_test_disj_aux1 wf_cpg_test_disj_aux2)
next
case (CSeq c1 c2 sts sts1 sts')
from CSeq(3) obtain sts''
where h: "wf_cpg_test sts c1 = (True, sts'')" "wf_cpg_test sts'' c2 = (True, sts')"
by (auto split:prod.splits)
from wf_cpg_test_le[OF h(1)] have "length sts = length sts''"
by (auto simp:less_eq_list_def)
from sts_le_comb[OF wf_cpg_test_le[OF h(1)] wf_cpg_test_le[OF h(2)]]
have " sts' - sts = (sts'' - sts) + (sts' - sts'')" "sts_disj (sts'' - sts) (sts' - sts'')"
by auto
from sts_disj_uncomb[OF CSeq(4)[unfolded this(1)] this(2)]
have "sts_disj sts1 (sts'' - sts)" "sts_disj sts1 (sts' - sts'')" .
from CSeq(1)[OF h(1) this(1)] CSeq(2)[OF h(2) this(2)]
have "wf_cpg_test (sts1 + sts) c1 = (True, sts1 + sts'')"
"wf_cpg_test (sts1 + sts'') c2 = (True, sts1 + sts')" .
thus ?case
by simp
next
case (CLocal body sts sts1 sts')
from this(2)
obtain sts'' where h: "wf_cpg_test (Free # sts) body = (True, sts'')" "sts' = tl sts''"
by (auto split:prod.splits)
from wf_cpg_test_le[OF h(1), unfolded less_eq_list_def] h(2)
obtain s where eq_sts'': "sts'' = s#sts'"
by (metis Suc_length_conv list.size(4) tl.simps(2))
let ?sts = "Free#sts1"
from CLocal(3) have "sts_disj ?sts (sts'' - (Free # sts))"
apply (unfold eq_sts'', simp)
by (metis sts_disj_cons)
from CLocal(1)[OF h(1) this] eq_sts''
show ?case
by (auto split:prod.splits)
qed
section {* Application of the theory above *}
definition "move_left_skel = CLocal (CSeq (CInstr ((L, 0), (L, 0))) (CLabel 0))"
lemma wt_move_left: "wf_cpg_test [] move_left_skel = (True, [])"
by (unfold move_left_skel_def, simp)
lemma ct_move_left: "c2t [] move_left_skel = move_left"
by (unfold move_left_skel_def move_left_def, simp)
lemma wf_move_left: "\<forall> i. \<exists> s j. (i:[move_left]:j ) s"
proof -
from wf_cpg_test_correct[OF wt_move_left] ct_move_left
show ?thesis
by (unfold c2p_def, simp, metis)
qed
definition "jmp_skel = CInstr ((W0, 0), (W1, 0))"
lemma wt_jmp: "wf_cpg_test [Free] jmp_skel = (True, [Free])"
by (unfold jmp_skel_def, simp)
lemma ct_jmp: "c2t [l] jmp_skel = (jmp l)"
by (unfold jmp_skel_def jmp_def, simp)
lemma wf_jmp: "\<forall> i. \<exists> s j. (i:[jmp l]:j ) s"
proof -
from wf_cpg_test_correct[OF wt_jmp] ct_jmp
show ?thesis
apply (unfold c2p_def, simp)
by (metis One_nat_def Suc_eq_plus1 list.size(3) list.size(4))
qed
definition "label_skel = CLabel 0"
lemma wt_label: "wf_cpg_test [Free] label_skel = (True, [Bound])"
by (simp add:label_skel_def)
lemma ct_label: "c2t [l] label_skel = (TLabel l)"
by (simp add:label_skel_def)
thm if_zero_def
definition "if_zero_skel = CLocal (CSeq (CInstr ((W0, 1), (W1, 0))) (
CLabel 0
)
)"
lemma wt_if_zero: "wf_cpg_test [Free] if_zero_skel = (True, [Free])"
by (simp add:if_zero_skel_def)
definition "left_until_zero_skel = CLocal (CLocal (
CSeq (CLabel 1) (
CSeq if_zero_skel (
CSeq move_left_skel (
CSeq (lift_t 0 1 jmp_skel) (
label_skel
))))
))"
lemma w1: "wf_cpg_test [Free, Bound] if_zero_skel = (True, [Free, Bound])"
by (simp add:if_zero_skel_def)
lemma w2: "wf_cpg_test [Free, Bound] move_left_skel = (True, [Free, Bound])"
by (simp add:move_left_skel_def)
lemma w3: "wf_cpg_test [Free, Bound] (lift_t 0 (Suc 0) jmp_skel) =
(True, [Free, Bound])"
by (simp add:jmp_skel_def lift_b_def)
lemma w4: "wf_cpg_test [Free, Bound] label_skel = (True, [Bound, Bound])"
by (unfold label_skel_def, simp)
lemma wt_left_until_zero:
"wf_cpg_test [] left_until_zero_skel = (True, [])"
by (unfold left_until_zero_skel_def, simp add:w1 w2 w3 w4)
lemma c1: "c2t [xa, x] if_zero_skel = if_zero xa"
by (simp add:if_zero_skel_def if_zero_def)
lemma c2: "c2t [xa, x] move_left_skel = move_left"
by (simp add:move_left_skel_def move_left_def)
lemma c3: "c2t [xa, x] (lift_t 0 (Suc 0) jmp_skel) =
jmp x"
by (simp add:jmp_skel_def jmp_def lift_b_def)
lemma c4: "c2t [xa, x] label_skel = TLabel xa"
by (simp add:label_skel_def)
lemma ct_left_until_zero:
"c2t [] left_until_zero_skel = left_until_zero"
apply (unfold left_until_zero_def left_until_zero_skel_def)
by (simp add:c1 c2 c3 c4)
lemma wf_left_until_zero:
"\<forall> i. \<exists> s j. (i:[left_until_zero]:j) s"
proof -
from wf_cpg_test_correct[OF wt_left_until_zero] ct_left_until_zero
show ?thesis
apply (unfold c2p_def, simp)
by metis
qed
end