tm2: comparison thys2/Hoare_tm

equal deleted inserted replaced

-:77daf1b85cf0
+:a5f5b9336007
+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