header {*
Separation logic for TM
*}
theory Hoare_tm_basis
imports Hoare_gen My_block Data_slot MLs Term_pat (* BaseSS *) Subgoal Sort_ops
Thm_inst
begin
section {* Aux lemmas on seperation algebra *}
lemma cond_eq: "((<b> \<and>* p) s) = (b \<and> (p s))"
proof
assume "(<b> \<and>* p) s"
from condD[OF this] show " b \<and> p s" .
next
assume "b \<and> p s"
hence b and "p s" by auto
from `b` have "(<b>) 0" by (auto simp:pasrt_def)
moreover have "s = 0 + s" by auto
moreover have "0 ## s" by auto
moreover note `p s`
ultimately show "(<b> \<and>* p) s" by (auto intro!:sep_conjI)
qed
lemma cond_eqI:
assumes h: "b \<Longrightarrow> r = s"
shows "(<b> ** r) = (<b> ** s)"
proof(cases b)
case True
from h[OF this] show ?thesis by simp
next
case False
thus ?thesis
by (unfold sep_conj_def set_ins_def pasrt_def, auto)
qed
lemma EXS_intro:
assumes h: "(P x) s"
shows "((EXS x. P(x))) s"
by (smt h pred_ex_def sep_conj_impl)
lemma EXS_elim:
assumes "(EXS x. P x) s"
obtains x where "P x s"
by (metis assms pred_ex_def)
lemma EXS_eq:
fixes x
assumes h: "Q (p x)"
and h1: "\<And> y s. \<lbrakk>p y s\<rbrakk> \<Longrightarrow> y = x"
shows "p x = (EXS x. p x)"
proof
fix s
show "p x s = (EXS x. p x) s"
proof
assume "p x s"
thus "(EXS x. p x) s" by (auto simp:pred_ex_def)
next
assume "(EXS x. p x) s"
thus "p x s"
proof(rule EXS_elim)
fix y
assume "p y s"
from this[unfolded h1[OF this]] show "p x s" .
qed
qed
qed
section {* The TM assembly language *}
subsection {* The TM assembly language *}
datatype taction = W0 | W1 | L | R
datatype tstate = St nat
fun nat_of :: "tstate \<Rightarrow> nat"
where "nat_of (St n) = n"
declare [[coercion_enabled]]
declare [[coercion "St :: nat \<Rightarrow> tstate"]]
type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)"
datatype Block = Oc | Bk
datatype tpg =
TInstr tm_inst
| TLabel tstate
| TSeq tpg tpg
| TLocal "(tstate \<Rightarrow> tpg)"
notation TLocal (binder "TL " 10)
abbreviation tprog_instr :: "tm_inst \<Rightarrow> tpg" ("\<guillemotright> _" [61] 61)
where "\<guillemotright> i \<equiv> TInstr i"
abbreviation tprog_seq :: "tpg \<Rightarrow> tpg \<Rightarrow> tpg" (infixr ";" 52)
where "c1 ; c2 \<equiv> TSeq c1 c2"
subsection {* The notion of assembling *}
datatype tresource =
TM int Block
| TC nat tm_inst
| TAt nat
| TPos int
| TFaults nat
type_synonym tassert = "tresource set \<Rightarrow> bool"
definition "sg e = (\<lambda> s. s = e)"
primrec tassemble_to :: "tpg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> tassert"
where
"tassemble_to (TInstr ai) i j = (sg ({TC i ai}) ** <(j = i + 1)>)" |
"tassemble_to (TSeq p1 p2) i j = (EXS j'. (tassemble_to p1 i j') ** (tassemble_to p2 j' j))" |
"tassemble_to (TLocal fp) i j = (EXS l. (tassemble_to (fp l) i j))" |
"tassemble_to (TLabel l) i j = <(i = j \<and> j = nat_of l)>"
declare tassemble_to.simps [simp del]
lemmas tasmp = tassemble_to.simps (2, 3, 4)
abbreviation tasmb_to :: "nat \<Rightarrow> tpg \<Rightarrow> nat \<Rightarrow> tassert" ("_ :[ _ ]: _" [60, 60, 60] 60)
where "i :[ tpg ]: j \<equiv> tassemble_to tpg i j"
section {* Automatic checking of assemblility *}
subsection {* Basic theories *}
text {* @{text cpg} is the type for skeleton assembly language. Every constructor
corresponds to one in the definition of @{text tpg} *}
datatype cpg =
CInstr tm_inst
| CLabel nat
| CSeq cpg cpg
| CLocal cpg
text {* Conversion from @{text cpg} to @{text tpg}*}
fun c2t :: "tstate list \<Rightarrow> cpg \<Rightarrow> tpg" where
"c2t env (CInstr ((act0, St st0), (act1, St 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)"
text {* Well formedness checking of @{text cpg} *}
datatype status = Free | Bound
text {* @{text wf_cpg_test} is the checking function *}
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'))"
text {*
The meaning the following @{text "c2p"} has to be understood together with
the following lemma @{text "wf_cpg_test_correct"}. The intended use of @{text "c2p"}
is when the elements of @{text "sts"} are all @{text "Free"}, in which case,
the precondition on @{text "f"}, i.e.
@{text "\<forall> x. ((length x = length sts \<and>
(\<forall> k < length sts. sts!k = Bound \<longrightarrow> (x!k = f i k))"}
is trivially true.
*}
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)))"
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 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 less_eq_list_def)
moreover from h have "\<forall> i < length x. x!i \<le> z!i"
by (metis less_eq_list_def order_trans)
ultimately show "x \<le> z"
by (metis 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, St l0), (a1, St l1))"
by (metis surj_pair tstate.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)))"
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
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
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, St l0), (a1, St l1))"
by (metis surj_pair tstate.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. St 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. St 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 = nat_of (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 = St i"
from h1 h3 have p1: "l < length (sts' - sts)"
by (metis length_list_update min_max.inf.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 = nat_of (x ! l))>) 0"
by (simp add:set_ins_def)
thus "\<exists> s. (<(i = nat_of (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]
obtain b1 sts1
where LetE: "(let (b2, y) = wf_cpg_test sts1 cpg2 in (b1 \<and> b2, y)) = (True, sts')"
"(b1, sts1) = wf_cpg_test sts cpg1"
by (auto simp:Let_def split:prod.splits)
show "\<exists> j. c2p (sts' - sts) i (CSeq cpg1 cpg2) j"
proof -
from LetE(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::tstate" 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 nth_app: "length xs \<le> a \<Longrightarrow> (xs @ ys)!a = ys!(a - length xs)"
by (metis not_less nth_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
subsection {* Invariant under lifts and perms *}
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 (nat_of l0)),
(act1, lift_b t i (nat_of 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)"
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"
fun lift_es :: "(tstate list \<times> nat) list \<Rightarrow> tstate list \<Rightarrow> tstate list" where
"lift_es [] env = env"
| "lift_es ((env', t)#ops) env = lift_es ops (take t env @ env' @ drop t env)"
fun lift_ss :: "(tstate list \<times> nat) list \<Rightarrow> status list \<Rightarrow> status list" where
"lift_ss [] sts = sts"
| "lift_ss ((env', t)#ops) sts = lift_ss ops (take t sts @ map (\<lambda> x. Free) env' @ drop t sts)"
fun lift_ts :: "(nat \<times> nat) list \<Rightarrow> cpg \<Rightarrow> cpg" where
"lift_ts [] cpg = cpg"
| "lift_ts ((lenv, t)#ops) cpg = lift_ts ops (lift_t t lenv cpg)"
fun perm_ss :: "(nat \<times> nat) list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"perm_ss [] env = env"
| "perm_ss ((i, j)#ops) env = perm_ss ops (perm_s i j env)"
fun perms :: "nat => (nat \<times> nat) list \<Rightarrow> cpg \<Rightarrow> cpg" where
"perms n [] cpg = cpg"
| "perms n ((i, j)#ops) cpg = perms n ops (perm n i j cpg)"
definition
"adjust_cpg len sps lfs cpg = lift_ts lfs (perms len sps cpg)"
definition
"red_lfs lfs = map (apfst length) lfs"
definition
"adjust_env sps lfs env = lift_es lfs (perm_ss sps env)"
definition
"adjust_sts sps lfs sts = lift_ss lfs (perm_ss sps sts)"
fun sts_disj_test :: "status list \<Rightarrow> status list \<Rightarrow> bool" where
"sts_disj_test [] [] = True"
| "sts_disj_test [] (s#ss) = False"
| "sts_disj_test (s#ss) [] = False"
| "sts_disj_test (s1#ss1) (s2#ss2) = (case (s1, s2) of
(Bound, Bound) \<Rightarrow> False
| _ \<Rightarrow> sts_disj_test ss1 ss2)"
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
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, St l0), (a1, St l1))"
by (metis surj_pair tstate.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, St l0), (a1, St l1))"
by (metis nat_of.cases surj_pair)
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
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 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_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)
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, St l0), (a1, St l1))"
by (metis surj_pair tstate.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, St l0), (a1, St l1))"
by (metis surj_pair tstate.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_max.inf.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, St l0), (a1, St l1))"
by (metis nat_of.cases surj_pair)
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
lemma sts_disj_free:
assumes "list_all (op = Free) sts"
and "length sts' = length sts"
shows "sts_disj sts' sts"
by (metis (full_types) assms(1) assms(2) list_all_length
status.distinct(1) sts_disj_def)
lemma all_free_plus:
assumes "length sts' = length sts"
and "list_all (op = Free) sts"
shows "sts' + sts = sts'"
using assms
proof(induct sts' arbitrary:sts)
case (Cons s sts' sts)
note cs = Cons
thus ?case
proof(cases "sts")
case (Cons s1 sts1)
with cs
show ?thesis
by (smt list.size(4) list_all_simps(1)
plus_list.simps(3) plus_status.simps(1) sts_list_plus_commut)
qed auto
qed auto
lemma wf_cpg_test_extrapo:
assumes "wf_cpg_test sts cpg = (True, sts)"
and "list_all (op = Free) sts"
and "length sts' = length sts"
shows "wf_cpg_test sts' cpg = (True, sts')"
proof -
have "sts_disj sts' (sts - sts)"
proof(rule sts_disj_free)
from assms(2)
show "list_all (op = Free) (sts - sts)"
by (induct sts, auto)
next
from assms(3) show "length sts' = length (sts - sts)"
by (metis length_sts_plus minus_list_len plus_list_len)
qed
from wf_cpg_test_disj [OF assms(1) this]
have "wf_cpg_test (sts' + sts) cpg = (True, sts' + sts)" .
moreover from all_free_plus[OF assms(3, 2)] have "sts' + sts = sts'" .
finally show ?thesis by simp
qed
lemma perms_wf_cpg_test:
assumes "wf_cpg_test sts cpg = (True, sts')"
shows "wf_cpg_test (perm_ss ops sts) (perms (length sts) ops cpg) =
(True, perm_ss ops sts')"
using assms
proof(induct ops arbitrary:sts cpg sts')
case (Cons sp ops sts cpg sts')
show ?case
proof(cases "sp")
case (Pair i j)
show ?thesis
proof -
let ?sts = "(perm_s i j sts)" and ?cpg = "(perm (length sts) i j cpg)"
and ?sts' = "perm_s i j sts'"
have "wf_cpg_test (perm_ss ops ?sts) (perms (length ?sts) ops ?cpg) =
(True, perm_ss ops ?sts')"
proof(rule Cons(1))
show "wf_cpg_test (perm_s i j sts) (perm (length sts) i j cpg) = (True, perm_s i j sts')"
by (metis Cons.prems perm_wf_cpg_test)
qed
thus ?thesis
apply (unfold Pair)
apply simp
by (metis perm_s_len)
qed
qed
qed auto
lemma perm_ss_len: "length (perm_ss ops xs) = length xs"
proof(induct ops arbitrary:xs)
case (Cons sp ops xs)
show ?case
proof(cases "sp")
case (Pair i j)
show ?thesis
proof -
let ?xs = "(perm_s i j xs)"
have "length (perm_ss ops ?xs) = length ?xs"
by (metis Cons.hyps)
also have "\<dots> = length xs"
by (metis perm_s_len)
finally show ?thesis
by (unfold Pair, simp)
qed
qed
qed auto
lemma perms_c2t:
assumes "wf_cpg_test sts cpg = (True, sts')"
and "length env = length sts"
shows "c2t (perm_ss ops env) (perms (length env) ops cpg) = c2t env cpg"
using assms
proof(induct ops arbitrary:sts cpg sts' env)
case (Cons sp ops sts cpg sts' env)
show ?case
proof(cases "sp")
case (Pair i j)
show ?thesis
proof -
let ?env = "(perm_s i j env)" and ?cpg = "(perm (length env) i j cpg)"
have " c2t (perm_ss ops ?env) (perms (length ?env) ops ?cpg) = c2t ?env ?cpg"
proof(rule Cons(1))
from perm_wf_cpg_test[OF Cons(2), of i j, folded Cons(3)]
show "wf_cpg_test (perm_s i j sts) (perm (length env) i j cpg) = (True, perm_s i j sts')" .
next
show "length (perm_s i j env) = length (perm_s i j sts)"
by (metis Cons.prems(2) perm_s_len)
qed
also have "\<dots> = c2t env cpg"
by (metis Cons.prems(1) Cons.prems(2) perm_c2t)
finally show ?thesis
apply (unfold Pair)
apply simp
by (metis perm_s_len)
qed
qed
qed auto
lemma red_lfs_nil: "red_lfs [] = []"
by (simp add:red_lfs_def)
lemma red_lfs_cons: "red_lfs ((env, t)#lfs) = (length env, t)#(red_lfs lfs)"
by (simp add:red_lfs_def)
lemmas red_lfs_simps [simp] = red_lfs_nil red_lfs_cons
lemma lifts_wf_cpg_test:
assumes "wf_cpg_test sts cpg = (True, sts')"
shows "wf_cpg_test (lift_ss ops sts) (lift_ts (red_lfs ops) cpg)
= (True, lift_ss ops sts')"
using assms
proof(induct ops arbitrary:sts cpg sts')
case (Cons sp ops sts cpg sts')
show ?case
proof(cases "sp")
case (Pair env' t)
thus ?thesis
proof -
let ?sts = "(take t sts @ map (\<lambda>x. Free) env' @ drop t sts)"
and ?sts' = "(take t sts' @ map (\<lambda>x. Free) env' @ drop t sts')"
and ?cpg = "(lift_t t (length env') cpg)"
have "wf_cpg_test (lift_ss ops ?sts) (lift_ts (red_lfs ops) ?cpg) = (True, lift_ss ops ?sts')"
proof(induct rule: Cons(1))
case 1
show ?case
by (metis Cons.prems length_map lift_wf_cpg_test)
qed
thus ?thesis
by (unfold Pair, simp)
qed
qed
qed auto
lemma lifts_c2t:
assumes "wf_cpg_test sts cpg = (True, sts')"
and "length env = length sts"
shows "c2t (lift_es ops env) (lift_ts (red_lfs ops) cpg) = c2t env cpg"
using assms
proof(induct ops arbitrary:sts cpg sts' env)
case (Cons sp ops sts cpg sts' env)
show ?case
proof(cases "sp")
case (Pair env' t)
show ?thesis
proof -
let ?env = "(take t env @ env' @ drop t env)"
and ?cpg = "(lift_t t (length env') cpg)"
have "c2t (lift_es ops ?env) (lift_ts (red_lfs ops) ?cpg) = c2t ?env ?cpg"
proof(rule Cons(1))
from lift_wf_cpg_test[OF Cons(2), of t "map (\<lambda> x. Free) env'", simplified length_map]
show "wf_cpg_test (take t sts @ map (\<lambda>x. Free) env' @ drop t sts)
(lift_t t (length env') cpg) =
(True, take t sts' @ map (\<lambda>x. Free) env' @ drop t sts')" .
next
show "length (take t env @ env' @ drop t env) =
length (take t sts @ map (\<lambda>x. Free) env' @ drop t sts)"
by (metis (full_types) Cons.prems(2) Pair assms(2) length_append
length_drop length_map length_take)
qed
also have "\<dots> = c2t env cpg"
by (metis Cons.prems(1) Cons.prems(2) lift_c2t)
finally show ?thesis
by (unfold Pair, simp)
qed
qed
qed auto
lemma adjust_c2t:
assumes "wf_cpg_test sts cpg = (True, sts')"
and "length env = length sts"
shows "c2t (adjust_env sps lfs env) (adjust_cpg (length sts) sps (red_lfs lfs) cpg) = c2t env cpg"
proof -
let ?cpg = "(perms (length sts) sps cpg)"
and ?env = "(perm_ss sps env)"
have "c2t (lift_es lfs ?env)
(lift_ts (red_lfs lfs) ?cpg) = c2t ?env ?cpg"
proof (rule lifts_c2t)
from perms_wf_cpg_test[OF assms(1), of sps]
show "wf_cpg_test (perm_ss sps sts) (perms (length sts) sps cpg) = (True, perm_ss sps sts')" .
next
show "length (perm_ss sps env) = length (perm_ss sps sts)"
by (metis assms(2) perm_ss_len)
qed
also have "\<dots> = c2t env cpg"
proof(fold assms(2), rule perms_c2t)
from assms(1) show " wf_cpg_test sts cpg = (True, sts')" .
next
from assms(2) show "length env = length sts" .
qed
finally show ?thesis
by (unfold adjust_env_def adjust_cpg_def, simp)
qed
lemma adjust_wf_cpg_test:
assumes "wf_cpg_test sts cpg = (True, sts')"
shows "wf_cpg_test (adjust_sts sps lfs sts) (adjust_cpg (length sts) sps (red_lfs lfs) cpg) =
(True, adjust_sts sps lfs sts')"
proof -
have " wf_cpg_test (lift_ss lfs (perm_ss sps sts)) (lift_ts (red_lfs lfs) (perms (length sts) sps cpg)) =
(True, lift_ss lfs (perm_ss sps sts'))"
proof(rule lifts_wf_cpg_test)
show " wf_cpg_test (perm_ss sps sts) (perms (length sts) sps cpg) = (True, perm_ss sps sts')"
by (rule perms_wf_cpg_test[OF assms])
qed
thus ?thesis
by (unfold adjust_sts_def adjust_cpg_def, simp)
qed
lemma sts_disj_test_correct:
assumes "sts_disj_test sts1 sts2"
shows "sts_disj sts1 sts2"
using assms
proof(induct sts1 arbitrary:sts2)
case (Nil sts2)
note Nil_1 = Nil
show ?case
proof(cases sts2)
case Nil
with Nil_1
show ?thesis by (simp add:sts_disj_def)
next
case (Cons s2 ss2)
with Nil_1 show ?thesis by simp
qed
next
case (Cons s1 ss1 sts2)
note Cons_1 = Cons
show ?case
proof(cases "sts2")
case Nil
with Cons_1 show ?thesis by simp
next
case (Cons s2 ss2)
show ?thesis
proof(cases "s1 = Bound \<and> s2 = Bound")
case True
with Cons_1 Cons
show ?thesis by simp
next
case False
with Cons_1 Cons
have "sts_disj_test ss1 ss2" by (auto split:status.splits)
from Cons_1(1) [OF this] False
show ?thesis
apply (unfold Cons)
apply (unfold sts_disj_def)
by (smt False length_Suc_conv list.size(4) nth_Cons')
qed
qed
qed
lemma sts_minus_free:
assumes "length sts1 = length sts2"
and "list_all (op = Free) sts2"
shows "sts1 - sts2 = sts1"
using assms
proof(induct sts1 arbitrary:sts2)
case (Nil sts2)
thus ?case by simp
next
case (Cons s1 ss1 sts2)
note Cons_1 = Cons
thus ?case
proof(cases sts2)
case Nil
with Cons
show ?thesis by simp
next
case (Cons s2 ss2)
have "ss1 - ss2 = ss1"
proof(rule Cons_1(1))
show "length ss1 = length ss2"
by (metis Cons Cons_1(2) Suc_length_conv list.inject)
next
show "list_all (op = Free) ss2"
by (metis Cons Cons_1(3) list_all_simps(1))
qed
moreover from Cons_1(3) Cons have "s2 = Free"
by (metis (full_types) list_all_simps(1))
ultimately show ?thesis using Cons
apply simp
by (metis (hide_lams, mono_tags) minus_status.simps(2) minus_status.simps(3) status.exhaust)
qed
qed
lemma st_simp [simp]: "St (nat_of x) = x"
by (metis nat_of.simps tstate.exhaust)
lemma wf_cpg_test_len:
assumes "wf_cpg_test sts cpg = (b, sts')"
shows "length sts' = length sts"
using assms
proof(induct cpg arbitrary:sts sts' b)
case (CInstr instr sts sts' b)
then obtain a1 s1 a2 s2 where
eq_instr: "instr = ((a1, St s1), (a2, St s2))"
by (metis st_simp surj_pair)
with CInstr
show ?case by simp
qed (auto split:prod.splits)
lemma wf_cpg_test_seq:
assumes "wf_cpg_test sts1 c1 = (True, sts1')"
and "wf_cpg_test sts2 c2 = (True, sts2')"
and "length sts1 = length sts2"
and "list_all (op = Free) sts1"
and "list_all (op = Free) sts2"
and "sts_disj_test sts1' sts2'"
shows "wf_cpg_test sts1 (CSeq c1 c2) = (True, sts1' + sts2')"
proof -
have "wf_cpg_test (sts1' + sts2) c2 = (True, sts1' + sts2')"
by (metis add_imp_eq assms(2) assms(5) assms(6) length_sts_plus
plus_list_len sts_disj_test_correct sts_minus_free wf_cpg_test_disj wf_cpg_test_extrapo wf_cpg_test_len)
hence "wf_cpg_test sts1' c2 = (True, sts1' + sts2')"
by (metis all_free_plus assms(1) assms(3) assms(5) wf_cpg_test_len)
with assms(1)
show ?thesis by simp
qed
lemma c2t_seq:
assumes "c2t env c1 = t1"
and "c2t env c2 = t2"
shows "c2t env (CSeq c1 c2) = (t1; t2)"
using assms by simp
lemma c2t_local:
assumes "\<And>x. (c2t (x#xs) cpg = body x)"
shows "c2t xs (CLocal cpg) = (TL x. body x)"
using assms
by simp
lemma wf_cpg_test_local:
assumes "wf_cpg_test (Free#sts) cpg = (b, s'#sts')"
shows "wf_cpg_test sts (CLocal cpg) = (b, sts')"
by (simp add:assms)
lemma wf_c2t_combined:
assumes "wf_cpg_test sts cpg = (True, sts)"
and "c2t env cpg = tpg"
and "list_all (op = Free) sts"
and "length env = length sts"
shows "\<forall> i. \<exists> j s. ((i:[tpg]:j) s)"
proof
fix i
from wf_cpg_test_correct[OF assms(1), rule_format, of i]
obtain j where "c2p (sts - sts) i cpg j" by metis
from this[unfolded c2p_def]
obtain f where h: "\<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 (i :[ c2t x cpg ]: j)" by metis
have "\<exists> s. (i :[ c2t env cpg ]: j) s"
proof(rule h[rule_format], rule conjI)
show "length env = length (sts - sts)"
by (smt assms(4) minus_list_len)
next
show "\<forall>k<length (sts - sts). (sts - sts) ! k = Bound \<longrightarrow> env ! k = f i k"
by (metis assms(3) minus_status.simps(1) nth_sts_minus status.distinct(1) sts_minus_free)
qed
show "\<exists> j s. ((i:[tpg]:j) s)"
by (metis `\<exists>s. (i :[ c2t env cpg ]: j) s` assms(2))
qed
subsection {* The Checker *}
ML {*
print_depth 200
*}
subsubsection {* Auxilary functions *}
ML {*
local
fun clear_binds ctxt = (ctxt |> Variable.binds_of |> Vartab.keys |> map (fn xi => (xi, NONE))
|> fold Variable.bind_term) ctxt
fun get_binds ctxt = ctxt |> Variable.binds_of |> Vartab.dest |> map (fn (xi, (_, tm)) => (xi, SOME tm))
fun set_binds blist ctxt = (fold Variable.bind_term blist) (clear_binds ctxt)
in
fun blocalM f = liftM (m2M (fn ctxt => returnM (get_binds ctxt)))
:|-- (fn binds =>
f
:|-- (fn result =>
liftM (m2M (fn ctxt' => s2M (set_binds binds ctxt') |-- returnM result
)))
)
end
fun condM bf scan = (fn v => m0M (fn st => if (bf (v, st)) then scan v else returnM v))
local
val counter = Unsynchronized.ref 0
in
fun init_counter n = (counter := n)
fun counter_test x =
if !counter <= 1 then true
else (counter := !counter - 1; false)
end
(* break point monad *)
fun bpM v' = (fn v => m0M (fn st => raiseM (v', (v, st))))
fun the_theory () = ML_Context.the_local_context () |> Proof_Context.theory_of
fun the_context () = ML_Context.the_local_context ()
(* Calculating the numberal of integer [i] *)
fun nat_of i = if i = 0 then @{term "0::nat"} else
(Const ("Num.numeral_class.numeral", @{typ "num \<Rightarrow> nat"}) $
(Numeral.mk_cnumeral i |> term_of))
fun vfixM nm typ = (m2M' (fn ctxt => let
val ([x], ctxt') = Variable.variant_fixes [nm] ctxt
val tm_x = Free (x, typ)
in s2M ctxt' |-- returnM tm_x end))
fun fixM nm typ = (m2M' (fn ctxt => let
val ([x], ctxt') = Variable.add_fixes [nm] ctxt
val tm_x = Free (x, typ)
in s2M ctxt' |-- returnM tm_x end))
local
fun mk_listM l =
case l of
[] => @{fterm "[]"}
| (tm::tms) => localM (@{match "?x"} tm
|-- (mk_listM tms)
:|-- @{match "?xs"}
|-- @{fterm "?x#?xs"})
in
fun mk_list_term ctxt l = [((), ctxt)] |> mk_listM l |> normVal |> fst
end
fun term_name (Const (x, _)) = Long_Name.base_name x
| term_name (Free (x, _)) = x
| term_name (Var ((x, _), _)) = x
| term_name _ = Name.uu;
val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
fun simpl_conv ss thl ctm =
rew_conv (ss addsimps thl) ctm RS meta_eq_to_obj_eq;
fun find_thms ctxt pats =
Find_Theorems.find_theorems ctxt NONE NONE true
(map (fn pat =>(true, Find_Theorems.Pattern
(Proof_Context.read_term_pattern ctxt pat))) pats) |> snd |> map snd
fun local_on arg rhs = [((), @{context})] |>
@{match "?body"} (Term.lambda arg rhs) |--
@{fterm "TL x. ?body x"} |> normVal |> fst
fun find_idx vars l = (nat_of (find_index (equal l) vars))
local
fun mk_pair_term (i, j) = [((), @{context})] |>
@{match "?i"} (nat_of i)
|-- @{match "?j"} (nat_of j)
|-- @{fterm "(?i, ?j)"} |> normVal |> fst
in
fun mk_npair_list_term ctxt pair_list =
if pair_list = [] then @{term "[]::(nat \<times> nat) list"}
else pair_list |> map mk_pair_term |> mk_list_term ctxt
end
fun list_of_array ary = let
val len = Array.length ary
val idx = upto (0, len - 1)
in map (fn i => Array.sub (ary, i)) idx end
local
fun mk_env_term ctxt lst =
if lst = [] then @{term "[]::tstate list"} else (mk_list_term ctxt lst)
fun mk_pair_term ctxt (i, j) = [((), ctxt)] |>
@{match "?i"} (mk_env_term ctxt i)
|-- @{match "?j"} (nat_of j)
|-- @{fterm "(?i, ?j)"} |> normVal |> fst
in
fun mk_tpair_list_term ctxt pair_list =
if pair_list = [] then @{term "[] :: (tstate list \<times> nat) list"}
else pair_list |> map (mk_pair_term ctxt) |> mk_list_term ctxt
end
*}
subsubsection {* The reifier *}
ML {*
fun locM (c2t_thm, test_thm) = (m1M' (fn env =>
let
val Free (x, _) = hd env
val c2t_thm = Drule.generalize ([], [x]) c2t_thm
val c2t_thm = @{thm c2t_local} OF [c2t_thm]
val test_thm = @{thm wf_cpg_test_local} OF [test_thm]
in
s1M (tl env) |-- returnM (c2t_thm, test_thm)
end))
fun reify_local reify t =
( @{match "TL x . ?body (x::tstate)"} t
|-- vfixM "x" @{typ "tstate"}
:|-- @{match "?x"}
:|-- (fn tmx => m1M' (fn env => s1M (tmx::env)))
|-- @{fterm "?body ?x"}
:|-- reify
:|-- locM
(* :|-- condM counter_test (bpM ("local", t)) *)
)
fun labelM exp = m0M' (fn (env, ctxt) => let
(* The following three lines are used for debugging purpose
(* (* The following two lines are used to set breakpoint counter
and invoke the reifyer in debug mode *)
val _ = init_counter 3
val t = reify tpg_def_rhs [(rev tpg_def_largs_sufx, ctxt_tpg_def)] |> normExcp
*)
(* The following line is used to extract break point information and
establish the environment to execute body statements *)
val ((brc, exp), (_, (env, ctxt)::_)) = t
*)
val c2t_thm = [((), ctxt)] |>
@{match "?cpg"} exp
|-- @{match "?env"} (env |> mk_list_term ctxt)
|-- @{fterm "c2t ?env ?cpg"} |> normVal |> fst |> cterm_of (Proof_Context.theory_of ctxt)
|> simpl_conv (simpset_of ctxt) []
val test_thm = [((), ctxt)] |>
@{match "?cpg"} exp
|-- @{match "?sts"} (env |> map (fn _ => @{term "Free"}) |> mk_list_term ctxt)
|-- @{fterm "wf_cpg_test ?sts ?cpg"} |> normVal |> fst |> cterm_of (Proof_Context.theory_of ctxt)
|> simpl_conv (simpset_of ctxt) []
in returnM (c2t_thm, test_thm) end)
fun reify_label t =
@{match "TLabel ?L"} t
|-- @{fterm "?L"}
:|-- (fn l => m1M' (fn st => returnM (find_idx st l)))
:|-- @{match ?L1}
|-- @{fterm "CLabel ?L1"}
(* :|-- condM counter_test (bpM ("label", t)) *)
:|-- labelM
fun seqM ((c2t_thm1, test_thm1), (c2t_thm2, test_thm2)) =
m0M' (fn (env, ctxt) =>
let
val simp_trans = (simpset_of ctxt) delsimps @{thms wf_cpg_test.simps c2t.simps} |> full_simplify
val ct2_thm = (@{thm c2t_seq} OF [c2t_thm1, c2t_thm2]) |> simp_trans
val test_thm = (@{thm wf_cpg_test_seq} OF [test_thm1, test_thm2]) |> simp_trans
in returnM (ct2_thm, test_thm) end)
fun reify_seq reify t =
@{match "?c1; ?c2"} t
|-- ((@{fterm "?c1"} :|-- reify) --
(@{fterm "?c2"} :|-- reify))
(* :|-- condM counter_test (bpM ("seq", t)) *)
:|-- seqM
fun reify_instr t =
@{match "\<guillemotright> ((?A0, ?L0), (?A1, ?L1))"} t
|-- @{fterm "?L0"}
:|-- (fn l => m1M' (fn st => returnM (find_idx st l)))
:|-- @{match ?L0'}
|-- @{fterm "?L1"}
:|-- (fn l => m1M' (fn st => returnM (find_idx st l)))
:|-- @{match ?L1'}
|-- @{fterm "CInstr ((?A0, ?L0'), (?A1, St ?L1'))"}
:|-- labelM
(* :|-- condM counter_test (bpM ("instr", t)) *)
fun reify_var var =
(* condM counter_test (bpM ("var", var)) () |-- *)
(m0M' (fn (env, ctxt) => let
(* The following three lines are used for debugging purpose
(* (* The following two lines are used to set breakpoint counter
and invoke the reifyer in debug mode *)
val _ = init_counter 3
val t = reify tpg_def_rhs [(rev tpg_def_largs_sufx, ctxt_tpg_def)] |> normExcp
*)
(* The following line is used to extract break point information and
establish the environment to execute body statements *)
val ((brc, var), (_, (env, ctxt)::_)) = t
*)
val (var_hd, var_args) = Term.strip_comb var
val (var_args_prefx, var_args_sufx) =
take_suffix (fn tm => type_of tm = @{typ "tstate"}) var_args
val var_skel_hd_typ = var_args_prefx |> map type_of |> (fn typs => typs ---> @{typ "cpg"})
(* We discriminate two cases, one for tpg constants; the other for argument variable *)
val ([var_skel_hd_name], ctxt1) =
case var_hd of
(Const (nm, _)) => ([((nm |> Long_Name.base_name)^"_skel")], ctxt)
| _ => Variable.variant_fixes [(term_name var_hd^"_skel_")] ctxt
(* If [var_hd] is a constant, a corresponding skeleton constant is assumed to exist alrady *)
val var_skel_hd = if (Term.is_Const var_hd) then Syntax.read_term ctxt1 var_skel_hd_name
else Free (var_skel_hd_name, var_skel_hd_typ)
(* [skel_tm] is the skeleton object the properties of which will either be assumed (in case of
argument variable), or proved (in case of global constants ) *)
val skel_tm = Term.list_comb (var_skel_hd, var_args_prefx)
(* Start to prove or assume [c2t] property (named [c2t_thm]) of the skeleton object,
since the [c2t] property needs to be universally qantified, we
need to invent quantifier names: *)
val (var_skel_args_sufx_names, ctxt2) =
Variable.variant_fixes (var_args_sufx |> map term_name) ctxt1
val var_skel_args_sufx = var_skel_args_sufx_names |> map (fn nm => Free (nm, @{typ "tstate"}))
val c2t_rhs = Term.list_comb (var_hd, var_args_prefx@var_skel_args_sufx)
val c2t_env = mk_list_term ctxt2 (var_skel_args_sufx |> rev)
val eqn = [((), ctxt2)] |>
@{match ?env} c2t_env
|-- @{match ?skel_tm} skel_tm
|-- @{match ?c2t_rhs} c2t_rhs
|-- @{fterm "Trueprop (c2t ?env ?skel_tm = ?c2t_rhs)"} |> normVal |> fst
fun all_on ctxt arg body = Const ("all", dummyT) $ (Term.lambda arg body) |>
Syntax.check_term ctxt
val c2t_eqn = fold (all_on ctxt2) (rev var_skel_args_sufx) eqn |> cterm_of (Proof_Context.theory_of ctxt2)
val ([c2t_thm], ctxt3) =
if (Term.is_Const var_hd) then
(* if [var_hd] is an constant, try to prove [c2t_eqn] by searching
into the facts database *)
let
val pat_skel_args = fold (curry (op ^)) (map (K " _ ") var_args_prefx) ""
val pat_skel_str = "( "^ var_skel_hd_name ^ pat_skel_args ^" )"
val test_pat = ("wf_cpg_test _ "^ pat_skel_str ^" = (True, _)")
val c2t_pat = ("c2t _ "^ pat_skel_str ^" = _")
val (wf_test_thms, c2t_thms) = ([test_pat], [c2t_pat]) |> pairself (find_thms ctxt2)
in
([([((0, @{thm "refl"}), ctxt2)] |>
goalM (c2t_eqn |> term_of)
|-- tacM (fn ctxt => (Simplifier.simp_tac ((simpset_of ctxt) addsimps c2t_thms) 1))
>> Goal.conclude |> normVal |> fst |> Raw_Simplifier.norm_hhf)], ctxt2)
end
else (* Otherwise, make [c2t_eqn] an assumption *)
Assumption.add_assumes [c2t_eqn] ctxt2
(* Start to prove or assume [wf_cpg_test] property (named [wf_test_thm]) of the skeleton object. *)
val sts = map (fn tm => @{term "Free"}) var_args_sufx |> mk_list_term ctxt3
val wf_test_eqn = [((), ctxt3)] |>
@{match ?cpg} skel_tm
|-- @{match ?sts} sts
|-- @{fterm "Trueprop (wf_cpg_test ?sts ?cpg = (True, ?sts))"} |> normVal |> fst
|> cterm_of (Proof_Context.theory_of ctxt3)
val ([wf_test_thm], ctxt4) =
if (Term.is_Const var_hd) then
let
val pat_skel_args = fold (curry (op ^)) (map (K " _ ") var_args_prefx) ""
val pat_skel_str = "( "^ var_skel_hd_name ^ pat_skel_args ^ " )"
val test_pat = ("wf_cpg_test _ "^ pat_skel_str ^" = (True, _)")
val c2t_pat = ("c2t _ "^ pat_skel_str ^" = _")
val wf_test_thms = [test_pat] |> (find_thms ctxt2)
in
([([((0, @{thm "refl"}), ctxt2)] |>
goalM (wf_test_eqn |> term_of)
|-- tacM (fn ctxt => (Simplifier.simp_tac ((simpset_of ctxt) addsimps wf_test_thms) 1))
>> Goal.conclude |> normVal |> fst |> Raw_Simplifier.norm_hhf)], ctxt3)
end
else Assumption.add_assumes [wf_test_eqn] ctxt3
(* Start the derivation of the length theorem *)
val length_env = mk_list_term ctxt4 (var_args_sufx |> rev)
val length_thm = [((0, @{thm "init"}), ctxt4)] |>
@{match "(?env)"} length_env
|-- @{match "(?sts)"} sts
|-- @{fterm "Trueprop (length (?env::tstate list) = length (?sts::status list))"}
:|-- goalM
|-- tacM (fn ctxt => (Simplifier.simp_tac (simpset_of ctxt) 1))
>> Goal.conclude |> normVal |> fst
(* Start compute two adjust operations, namely [sps] and [lfs] *)
val locs = var_args_sufx |> map (fn arg => find_index (equal arg) env) |> rev
val swaps = swaps_of locs
val sps = swaps |> mk_npair_list_term @{context}
val locs' = sexec swaps (Array.fromList locs) |> list_of_array
val pairs = ((~1::locs') ~~ (locs' @ [length env]))
fun lfs_of (t, ops) [] = ops |> rev
| lfs_of (t, ops) ((i, j)::pairs) = let
val stuf = upto (i + 1, j - 1) |> map (fn idx => nth env idx)
in if (stuf <> []) then lfs_of (t + length stuf + 1, (stuf, t)::ops) pairs
else lfs_of (t + length stuf + 1, ops) pairs
end
val lfs = lfs_of (0, []) pairs |> mk_tpair_list_term @{context}
(* [simp_trans] is the simplification procedure used to simply the theorem after
instantiation.
*)
val simp_trans = full_simplify ((simpset_of @{context}) addsimps @{thms adjust_sts_def
adjust_env_def perm_s_def perm_b_def map_idx_len
map_idx_def upto_map upto_empty} @ [c2t_thm])
(* Instantiating adjust theorems *)
val adjust_c2t_thm = [((), ctxt4)] |>
@{match "?sps"} sps
|-- @{match "?lfs"} lfs
|-- thm_instM (@{thm adjust_c2t} OF [wf_test_thm, length_thm])
|> normVal |> fst |> simp_trans
val adjust_test_thm = [((), ctxt4)] |>
@{match "?sps"} sps
|-- @{match "?lfs"} lfs
|-- thm_instM (@{thm adjust_wf_cpg_test} OF [wf_test_thm])
|> normVal |> fst |> simp_trans
in
(* s2M ctxt4 |-- *) returnM (adjust_c2t_thm, adjust_test_thm)
end))
fun reify t =
localM (reify_seq reify t ||
reify_local reify t ||
reify_label t ||
reify_instr t ||
reify_var t
)
*}
subsubsection {* The Checker packed up as the asmb attribute *}
ML {*
fun asmb_attrib def_thm =
Context.cases (fn thy =>
(* val thy = @{theory} *) let
fun thy_exit ctxt =
Context.Theory (Local_Theory.exit_global (Local_Theory.assert_bottom true ctxt))
val ctxt0 = Named_Target.theory_init thy
val (((x, y), [tpg_def]), ctxt_tpg_def) = Variable.import true [def_thm] ctxt0
val (tpg_def_lhs, tpg_def_rhs) = [((), ctxt_tpg_def)] |>
@{match "Trueprop (?L = ?R)"} (prop_of tpg_def)
|-- @{fterm "?L"} -- @{fterm "?R"} |> normVal |> fst
val (tpg_def_lhd, tpg_def_largs) = Term.strip_comb tpg_def_lhs
val (tpg_def_largs_prefx, tpg_def_largs_sufx) =
take_suffix (fn tm => type_of tm = @{typ "tstate"}) tpg_def_largs
(* Invoking the reifyer in normal mode *)
val ((c2t_thm_1, test_thm_1), ((_, ctxt_r)::y)) =
reify tpg_def_rhs [(rev tpg_def_largs_sufx, ctxt_tpg_def)]
|> normVal
val asmb_thm_1 = (@{thm wf_c2t_combined} OF [test_thm_1, c2t_thm_1]) |> (full_simplify (simpset_of ctxt_r))
val (r_cpg, r_tpg) = [((), ctxt_r)] |>
@{match "Trueprop (c2t _ ?X = ?tpg)"} (c2t_thm_1 |> prop_of)
|-- (@{fterm "?X"} -- @{fterm "?tpg"}) |> normVal |> fst
val tpg_def_params = Variable.add_fixed ctxt_tpg_def (tpg_def_lhs) [] |> map fst
|> sort (Variable.fixed_ord ctxt_tpg_def)
val r_cpg_frees = Term.add_frees r_cpg []
local fun condense [] = []
| condense xs = [hd xs]
in
val skel_def_params =
tpg_def_params |> map (fn nm => condense
(filter (fn (tnm, _) => String.isPrefix nm tnm) r_cpg_frees))
|> flat |> map Free
end
val skel_def_rhs = fold Term.lambda (skel_def_params |> rev) r_cpg
local
val Const (nm, _) = tpg_def_lhs |> Term.head_of
in
val tpg_def_name = nm |> Long_Name.base_name
val skel_def_lhs = Free (tpg_def_name^"_skel", type_of skel_def_rhs)
end
val skel_def_eqn = [((), ctxt_r)] |>
@{match "?lhs"} skel_def_lhs
|-- @{match "?rhs"} skel_def_rhs
|-- @{fterm "Trueprop (?lhs = ?rhs)"} |> normVal |> fst
val ((skel_def_lhs, (skel_def_name, skel_def_thm)), lthy2) =
Specification.definition (NONE, (Attrib.empty_binding, skel_def_eqn)) ctxt_r
val c2t_thm_final = [((0, @{thm refl}), lthy2)] |>
@{match "?env"} (mk_list_term lthy2 (rev tpg_def_largs_sufx))
|-- @{match "?skel"} (Term.list_comb (skel_def_lhs, skel_def_params))
val c2t_thm_final = [((0, @{thm refl}), lthy2)] |>
@{match "?env"} (mk_list_term lthy2 (rev tpg_def_largs_sufx))
|-- @{match "?skel"} (Term.list_comb (skel_def_lhs, skel_def_params))
|-- @{match "?tpg"} tpg_def_lhs
|-- @{fterm "Trueprop (c2t ?env ?skel = ?tpg)"}
:|-- goalM
|-- tacM (fn ctxt => (Simplifier.simp_tac ((simpset_of ctxt |> Simplifier.clear_ss)
addsimps [skel_def_thm, c2t_thm_1]) 1))
|-- tacM (fn ctxt => (Simplifier.simp_tac ((simpset_of ctxt |> Simplifier.clear_ss)
addsimps [def_thm]) 1))
>> Goal.conclude |> normVal |> fst
val test_thm_final = [((0, @{thm refl}), lthy2)] |>
@{match "?sts"} (tpg_def_largs_sufx |> map (fn _ => @{term "Free"}) |> mk_list_term lthy2)
|-- @{match "?skel"} (Term.list_comb (skel_def_lhs, skel_def_params))
|-- @{fterm "Trueprop (wf_cpg_test ?sts ?skel = (True, ?sts))"}
:|-- goalM
|-- tacM (fn ctxt => (Simplifier.simp_tac ((simpset_of ctxt |> Simplifier.clear_ss)
addsimps [skel_def_thm, test_thm_1]) 1))
>> Goal.conclude |> normVal |> fst
val asmb_thm_final = [((0, @{thm refl}), lthy2)] |>
@{match "?tpg"} tpg_def_lhs
|-- @{fterm "Trueprop (\<forall> i. \<exists> j s. (i:[?tpg]:j) s)"}
:|-- goalM
|-- tacM (fn ctxt => (Simplifier.simp_tac ((simpset_of ctxt)
addsimps [tpg_def, asmb_thm_1]) 1))
>> Goal.conclude |> normVal |> fst
fun generalize thm = let
val hyps = (#hyps (thm |> Thm.crep_thm))
val thm' = if (length hyps = 0) then thm
else (fold Thm.implies_intr (#hyps (thm |> Thm.crep_thm) |> rev |> tl |> rev) thm)
in
thm' |> Thm.forall_intr_frees
end
val lthy3 =
Local_Theory.note ((Binding.name ("c2t_" ^ tpg_def_name ^ "_skel"), []),
[c2t_thm_final |> generalize]) lthy2 |> snd
val lthy4 =
Local_Theory.note ((Binding.name ("wf_" ^ tpg_def_name ^ "_skel"), []),
[test_thm_final |> generalize]) lthy3 |> snd
val lthy5 =
Local_Theory.note ((Binding.name ("asmb_" ^ tpg_def_name), []),
[asmb_thm_final |> Drule.export_without_context]) lthy4 |> snd
in
thy_exit lthy5
end) (fn ctxt => Context.Proof ctxt)
*}
setup {*
Attrib.setup @{binding asmb} (Scan.succeed (Thm.declaration_attribute asmb_attrib)) "asmb attribute"
*}
section {* Basic macros for TM *}
definition [asmb]: "write_zero = (TL exit. \<guillemotright>((W0, exit), (W0, exit)); TLabel exit)"
definition [asmb]: "write_one = (TL exit. \<guillemotright>((W1, exit), (W1, exit)); TLabel exit)"
definition [asmb]: "move_left = (TL exit . \<guillemotright>((L, exit), (L, exit)); TLabel exit)"
definition [asmb]: "move_right = (TL exit . \<guillemotright>((R, exit), (R, exit)); TLabel exit)"
definition [asmb]: "if_one e = (TL exit . \<guillemotright>((W0, exit), (W1, e)); TLabel exit)"
definition [asmb]: "if_zero e = (TL exit . \<guillemotright>((W0, e), (W1, exit)); TLabel exit)"
definition [asmb]: "jmp e = \<guillemotright>((W0, e), (W1, e))"
definition [asmb]:
"right_until_zero =
(TL start exit.
TLabel start;
if_zero exit;
move_right;
jmp start;
TLabel exit
)"
definition [asmb]:
"left_until_zero =
(TL start exit.
TLabel start;
if_zero exit;
move_left;
jmp start;
TLabel exit
)"
definition [asmb]:
"right_until_one =
(TL start exit.
TLabel start;
if_one exit;
move_right;
jmp start;
TLabel exit
)"
definition [asmb]:
"left_until_one =
(TL start exit.
TLabel start;
if_one exit;
move_left;
jmp start;
TLabel exit
)"
definition [asmb]:
"left_until_double_zero =
(TL start exit.
TLabel start;
if_zero exit;
left_until_zero;
move_left;
if_one start;
TLabel exit)"
definition [asmb]:
"shift_right =
(TL start exit.
TLabel start;
if_zero exit;
write_zero;
move_right;
right_until_zero;
write_one;
move_right;
jmp start;
TLabel exit
)"
definition [asmb]:
"clear_until_zero =
(TL start exit.
TLabel start;
if_zero exit;
write_zero;
move_right;
jmp start;
TLabel exit)"
definition [asmb]:
"shift_left =
(TL start exit.
TLabel start;
if_zero exit;
move_left;
write_one;
right_until_zero;
move_left;
write_zero;
move_right;
move_right;
jmp start;
TLabel exit)
"
definition [asmb]:
"bone c1 c2 = (TL exit l_one.
if_one l_one;
(c1;
jmp exit);
TLabel l_one;
c2;
TLabel exit
)"
definition [asmb]:
"cfill_until_one = (TL start exit.
TLabel start;
if_one exit;
write_one;
move_left;
jmp start;
TLabel exit
)"
definition [asmb]:
"cmove = (TL start exit.
TLabel start;
left_until_zero;
left_until_one;
move_left;
if_zero exit;
move_right;
write_zero;
right_until_one;
right_until_zero;
write_one;
jmp start;
TLabel exit
)"
definition [asmb]:
"cinit = (right_until_zero; move_right; write_one)"
definition [asmb]:
"copy = (cinit; cmove; move_right; move_right; right_until_one;
move_left; move_left; cfill_until_one)"
definition
"bzero c1 c2 = (TL exit l_zero.
if_zero l_zero;
(c1;
jmp exit);
TLabel l_zero;
c2;
TLabel exit
)"
definition "if_reps_nz e = (move_right;
bzero (move_left; jmp e) (move_left)
)"
declare if_reps_nz_def[unfolded bzero_def, asmb]
definition "if_reps_z e = (move_right;
bone (move_left; jmp e) (move_left)
)"
declare if_reps_z_def [unfolded bone_def, asmb]
definition
"skip_or_set = bone (write_one; move_right; move_right)
(right_until_zero; move_right)"
declare skip_or_set_def[unfolded bone_def, asmb]
definition "tpg_fold tpgs = foldr TSeq (butlast tpgs) (last tpgs)"
definition "cpg_fold cpgs = foldr CSeq (butlast cpgs) (last cpgs)"
definition "skip_or_sets n = tpg_fold (replicate n skip_or_set)"
definition "skip_or_sets_skel n = cpg_fold (replicate n skip_or_set_skel)"
lemma c2t_skip_or_sets_skel:
"c2t [] (skip_or_sets_skel (Suc n)) = skip_or_sets (Suc n)"
proof(induct n)
case (Suc k)
thus ?case
apply (unfold skip_or_sets_skel_def cpg_fold_def skip_or_sets_def tpg_fold_def)
my_block
fix x k
have "(last (replicate (Suc k) x)) = x"
by (metis Suc_neq_Zero last_replicate)
my_block_end
apply (unfold this)
my_block
fix x k
have "(butlast (replicate (Suc k) x)) = replicate k x"
by (metis butlast_snoc replicate_Suc replicate_append_same)
my_block_end
apply (unfold this)
my_block
fix x k f y
have "foldr f (replicate (Suc k) x) y = f x (foldr f (replicate k x) y)"
by simp
my_block_end
apply (unfold this)
by (simp add:c2t_skip_or_set_skel)
next
case 0
show ?case
by (simp add:skip_or_sets_skel_def cpg_fold_def skip_or_sets_def tpg_fold_def
c2t_skip_or_set_skel)
qed
lemma wf_skip_or_sets_skel:
"wf_cpg_test [] (skip_or_sets_skel (Suc n)) = (True, [])"
proof(induct n)
case (Suc k)
thus ?case
apply (unfold skip_or_sets_skel_def cpg_fold_def)
my_block
fix x k
have "(last (replicate (Suc k) x)) = x"
by (metis Suc_neq_Zero last_replicate)
my_block_end
apply (unfold this)
my_block
fix x k
have "(butlast (replicate (Suc k) x)) = replicate k x"
by (metis butlast_snoc replicate_Suc replicate_append_same)
my_block_end
apply (unfold this)
my_block
fix x k f y
have "foldr f (replicate (Suc k) x) y = f x (foldr f (replicate k x) y)"
by simp
my_block_end
apply (unfold this)
by (simp add:wf_skip_or_set_skel)
next
case 0
thus ?case
apply (unfold skip_or_sets_skel_def cpg_fold_def)
by (simp add:wf_skip_or_set_skel)
qed
lemma asmb_skip_or_sets:
"\<forall>i. \<exists>j s. (i :[ skip_or_sets (Suc n) ]: j) s"
by (rule wf_c2t_combined[OF wf_skip_or_sets_skel c2t_skip_or_sets_skel], auto)
definition [asmb]: "locate n = (skip_or_sets (Suc n);
move_left;
move_left;
left_until_zero;
move_right
)"
definition [asmb]: "Inc a = locate a;
right_until_zero;
move_right;
shift_right;
move_left;
left_until_double_zero;
write_one;
left_until_double_zero;
move_right;
move_right
"
definition [asmb]: "Dec a e = (TL continue.
(locate a;
if_reps_nz continue;
left_until_double_zero;
move_right;
move_right;
jmp e);
(TLabel continue;
right_until_zero;
move_left;
write_zero;
move_right;
move_right;
shift_left;
move_left;
move_left;
move_left;
left_until_double_zero;
move_right;
move_right))"
end