--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Hoare_tm_basis.thy Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,2857 @@
+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
\ No newline at end of file