recursive function theories / UF_rec still need coding of tapes and programs
header {* Separation logic for Turing Machines*}theory Hoare_tmimports Hoare_gen My_block Data_slotbeginML {*fun pretty_terms ctxt trms = Pretty.block (Pretty.commas (map (Syntax.pretty_term ctxt) trms))*}ML {*structure StepRules = Named_Thms (val name = @{binding "step"} val description = "Theorems for hoare rules for every step")*}ML {*structure FwdRules = Named_Thms (val name = @{binding "fwd"} val description = "Theorems for fwd derivation of seperation implication")*}setup {* StepRules.setup *}setup {* FwdRules.setup *}method_setup prune = {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} "pruning parameters"lemma int_add_C: "x + (y::int) = y + x" by simplemma int_add_A : "(x + y) + z = x + (y + (z::int))" by simplemma int_add_LC: "x + (y + (z::int)) = y + (x + z)" by simplemmas int_add_ac = int_add_A int_add_C int_add_LCsection {* Operational Semantics of TM *}datatype taction = W0 | W1 | L | Rtype_synonym tstate = natdatatype Block = Oc | Bk(* the successor state when tape symbol is Bk or Oc, respectively *)type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)"(* - number of faults (nat) - TM program (nat \<rightharpoonup> tm_inst) - current state (nat) - position of head (int) - tape (int \<rightharpoonup> Block)*)type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)"(* updates the position/tape according to an action *)fun next_tape :: "taction \<Rightarrow> (int \<times> (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int \<rightharpoonup> Block))"where "next_tape W0 (pos, m) = (pos, m(pos \<mapsto> Bk))" | "next_tape W1 (pos, m) = (pos, m(pos \<mapsto> Oc))" | "next_tape L (pos, m) = (pos - 1, m)" | "next_tape R (pos, m) = (pos + 1, m)"fun tstep :: "tconf \<Rightarrow> tconf" where "tstep (faults, prog, pc, pos, m) = (case (prog pc) of Some ((action0, pc0), (action1, pc1)) \<Rightarrow> case (m pos) of Some Bk \<Rightarrow> (faults, prog, pc0, next_tape action0 (pos, m)) | Some Oc \<Rightarrow> (faults, prog, pc1, next_tape action1 (pos, m)) | None \<Rightarrow> (faults + 1, prog, pc, pos, m) | None \<Rightarrow> (faults + 1, prog, pc, pos, m))"lemma tstep_splits: "(P (tstep s)) = ((\<forall> faults prog pc pos m action0 pc0 action1 pc1. s = (faults, prog, pc, pos, m) \<longrightarrow> prog pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow> m pos = Some Bk \<longrightarrow> P (faults, prog, pc0, next_tape action0 (pos, m))) \<and> (\<forall> faults prog pc pos m action0 pc0 action1 pc1. s = (faults, prog, pc, pos, m) \<longrightarrow> prog pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow> m pos = Some Oc \<longrightarrow> P (faults, prog, pc1, next_tape action1 (pos, m))) \<and> (\<forall> faults prog pc pos m action0 pc0 action1 pc1. s = (faults, prog, pc, pos, m) \<longrightarrow> prog pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow> m pos = None \<longrightarrow> P (faults + 1, prog, pc, pos, m)) \<and> (\<forall> faults prog pc pos m . s = (faults, prog, pc, pos, m) \<longrightarrow> prog pc = None \<longrightarrow> P (faults + 1, prog, pc, pos, m)) )" by (cases s) (auto split: option.splits Block.splits)datatype tresource = TM int Block (* at the position int of the tape is a Bl or Oc *) | TC nat tm_inst (* at the address nat is a certain instruction *) | TAt nat (* TM is at state nat*) | TPos int (* head of TM is at position int *) | TFaults nat (* there are nat faults *)definition "tprog_set prog = {TC i inst | i inst. prog i = Some inst}"definition "tpc_set pc = {TAt pc}"definition "tmem_set m = {TM i n | i n. m (i) = Some n}"definition "tpos_set pos = {TPos pos}"definition "tfaults_set faults = {TFaults faults}"lemmas tpn_set_def = tprog_set_def tpc_set_def tmem_set_def tfaults_set_def tpos_set_deffun trset_of :: "tconf \<Rightarrow> tresource set" where "trset_of (faults, prog, pc, pos, m) = tprog_set prog \<union> tpc_set pc \<union> tpos_set pos \<union> tmem_set m \<union> tfaults_set faults"interpretation tm: sep_exec tstep trset_of .section {* Assembly language for TMs and its program logic *}subsection {* The assembly language *}datatype tpg = TInstr tm_inst | TLabel nat | TSeq tpg tpg | TLocal "nat \<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"definition "sg e = (\<lambda>s. s = e)"type_synonym tassert = "tresource set \<Rightarrow> bool"abbreviation t_hoare :: "tassert \<Rightarrow> tassert \<Rightarrow> tassert \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)where "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> == sep_exec.Hoare_gen tstep trset_of p c q"abbreviation it_hoare :: "('a::sep_algebra \<Rightarrow> tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> (tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)where "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> == sep_exec.IHoare tstep trset_of I P c Q"(*primrec tpg_len :: "tpg \<Rightarrow> nat" where "tpg_len (TInstr ai) = 1" | "tpg_len (TSeq p1 p2) = tpg_len p1 + tpg_len " | "tpg_len (TLocal fp) = tpg_len (fp 0)" | "tpg_len (TLabel l) = 0" *)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 = 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"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 qedqeddefinition "tpg_fold tpgs = foldr TSeq (butlast tpgs) (last tpgs)"lemma tpg_fold_sg: "tpg_fold [tpg] = tpg" by (simp add:tpg_fold_def)lemma tpg_fold_cons: assumes h: "tpgs \<noteq> []" shows "tpg_fold (tpg#tpgs) = (tpg; (tpg_fold tpgs))" using hproof(induct tpgs arbitrary:tpg) case (Cons tpg1 tpgs1) thus ?case proof(cases "tpgs1 = []") case True thus ?thesis by (simp add:tpg_fold_def) next case False show ?thesis proof - have eq_1: "butlast (tpg # tpg1 # tpgs1) = tpg # (butlast (tpg1 # tpgs1))" by simp from False have eq_2: "last (tpg # tpg1 # tpgs1) = last (tpg1 # tpgs1)" by simp have eq_3: "foldr (op ;) (tpg # butlast (tpg1 # tpgs1)) (last (tpg1 # tpgs1)) = (tpg ; (foldr (op ;) (butlast (tpg1 # tpgs1)) (last (tpg1 # tpgs1))))" by simp show ?thesis apply (subst (1) tpg_fold_def, unfold eq_1 eq_2 eq_3) by (fold tpg_fold_def, simp) qed qedqed autolemmas tpg_fold_simps = tpg_fold_sg tpg_fold_conslemma tpg_fold_app: assumes h1: "tpgs1 \<noteq> []" and h2: "tpgs2 \<noteq> []" shows "i:[(tpg_fold (tpgs1 @ tpgs2))]:j = i:[(tpg_fold (tpgs1); tpg_fold tpgs2)]:j" using h1 h2proof(induct tpgs1 arbitrary: i j tpgs2) case (Cons tpg1' tpgs1') thus ?case (is "?L = ?R") proof(cases "tpgs1' = []") case False from h2 have "(tpgs1' @ tpgs2) \<noteq> []" by (metis Cons.prems(2) Nil_is_append_conv) have "?L = (i :[ tpg_fold (tpg1' # (tpgs1' @ tpgs2)) ]: j )" by simp also have "\<dots> = (i:[(tpg1'; (tpg_fold (tpgs1' @ tpgs2)))]:j )" by (simp add:tpg_fold_cons[OF `(tpgs1' @ tpgs2) \<noteq> []`]) also have "\<dots> = ?R" proof - have "(EXS j'. i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) = (EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>* j' :[ tpg_fold tpgs2 ]: j)" proof(default+) fix s assume "(EXS j'. i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s" thus "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>* j' :[ tpg_fold tpgs2 ]: j) s" proof(elim EXS_elim) fix j' assume "(i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s" from this[unfolded Cons(1)[OF False Cons(3)] tassemble_to.simps] show "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>* j' :[ tpg_fold tpgs2 ]: j) s" proof(elim sep_conjE EXS_elim) fix x y j'a xa ya assume h: "(i :[ tpg1' ]: j') x" "x ## y" "s = x + y" "(j' :[ tpg_fold tpgs1' ]: j'a) xa" "(j'a :[ tpg_fold tpgs2 ]: j) ya" " xa ## ya" "y = xa + ya" show "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>* j' :[ tpg_fold tpgs2 ]: j) s" (is "(EXS j'. (?P j' \<and>* ?Q j')) s") proof(rule EXS_intro[where x = "j'a"]) from `(j'a :[ tpg_fold tpgs2 ]: j) ya` have "(?Q j'a) ya" . moreover have "(?P j'a) (x + xa)" proof(rule EXS_intro[where x = j']) have "x + xa = x + xa" by simp moreover from `x ## y` `y = xa + ya` `xa ## ya` have "x ## xa" by (metis sep_disj_addD) moreover note `(i :[ tpg1' ]: j') x` `(j' :[ tpg_fold tpgs1' ]: j'a) xa` ultimately show "(i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold tpgs1' ]: j'a) (x + xa)" by (auto intro!:sep_conjI) qed moreover from `x##y` `y = xa + ya` `xa ## ya` have "(x + xa) ## ya" by (metis sep_disj_addI1 sep_disj_commuteI) moreover from `s = x + y` `y = xa + ya` have "s = (x + xa) + ya" by (metis h(2) h(6) sep_add_assoc sep_disj_addD1 sep_disj_addD2) ultimately show "(?P j'a \<and>* ?Q j'a) s" by (auto intro!:sep_conjI) qed qed qed next fix s assume "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>* j' :[ tpg_fold tpgs2 ]: j) s" thus "(EXS j'. i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s" proof(elim EXS_elim sep_conjE) fix j' x y j'a xa ya assume h: "(j' :[ tpg_fold tpgs2 ]: j) y" "x ## y" "s = x + y" "(i :[ tpg1' ]: j'a) xa" "(j'a :[ tpg_fold tpgs1' ]: j') ya" "xa ## ya" "x = xa + ya" show "(EXS j'. i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s" proof(rule EXS_intro[where x = j'a]) from `(i :[ tpg1' ]: j'a) xa` have "(i :[ tpg1' ]: j'a) xa" . moreover have "(j'a :[ tpg_fold (tpgs1' @ tpgs2) ]: j) (ya + y)" proof(unfold Cons(1)[OF False Cons(3)] tassemble_to.simps) show "(EXS j'. j'a :[ tpg_fold tpgs1' ]: j' \<and>* j' :[ tpg_fold tpgs2 ]: j) (ya + y)" proof(rule EXS_intro[where x = "j'"]) from `x ## y` `x = xa + ya` `xa ## ya` have "ya ## y" by (metis sep_add_disjD) moreover have "ya + y = ya + y" by simp moreover note `(j'a :[ tpg_fold tpgs1' ]: j') ya` `(j' :[ tpg_fold tpgs2 ]: j) y` ultimately show "(j'a :[ tpg_fold tpgs1' ]: j' \<and>* j' :[ tpg_fold tpgs2 ]: j) (ya + y)" by (auto intro!:sep_conjI) qed qed moreover from `s = x + y` `x = xa + ya` have "s = xa + (ya + y)" by (metis h(2) h(6) sep_add_assoc sep_add_disjD) moreover from `xa ## ya` `x ## y` `x = xa + ya` have "xa ## (ya + y)" by (metis sep_disj_addI3) ultimately show "(i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s" by (auto intro!:sep_conjI) qed qed qed thus ?thesis by (simp add:tassemble_to.simps, unfold tpg_fold_cons[OF False], unfold tassemble_to.simps, simp) qed finally show ?thesis . next case True thus ?thesis by (simp add:tpg_fold_cons[OF Cons(3)] tpg_fold_sg) qed qed autosubsection {* Assertions and program logic for this assembly language *}definition "st l = sg (tpc_set l)"definition "ps p = sg (tpos_set p)" definition "tm a v = sg ({TM a v})"definition "one i = tm i Oc"definition "zero i= tm i Bk"definition "any i = (EXS v. tm i v)"declare trset_of.simps[simp del]lemma stimes_sgD: "(sg x \<and>* q) s \<Longrightarrow> q (s - x) \<and> x \<subseteq> s" apply(erule_tac sep_conjE) apply(unfold set_ins_def sg_def) by (metis Diff_Int Diff_cancel Diff_empty Un_Diff sup.cobounded1 sup_bot.left_neutral sup_commute)lemma stD: "(st i \<and>* r) (trset_of (ft, prog, i', pos, mem)) \<Longrightarrow> i' = i"proof - assume "(st i \<and>* r) (trset_of (ft, prog, i', pos, mem))" from stimes_sgD [OF this[unfolded st_def], unfolded trset_of.simps] have "tpc_set i \<subseteq> tprog_set prog \<union> tpc_set i' \<union> tpos_set pos \<union> tmem_set mem \<union> tfaults_set ft" by auto thus ?thesis by (unfold tpn_set_def, auto)qedlemma psD: "(ps p \<and>* r) (trset_of (ft, prog, i', pos, mem)) \<Longrightarrow> pos = p"proof - assume "(ps p ** r) (trset_of (ft, prog, i', pos, mem))" from stimes_sgD [OF this[unfolded ps_def], unfolded trset_of.simps] have "tpos_set p \<subseteq> tprog_set prog \<union> tpc_set i' \<union> tpos_set pos \<union> tmem_set mem \<union> tfaults_set ft" by simp thus ?thesis by (unfold tpn_set_def, auto)qedlemma codeD: "(st i ** sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem)) \<Longrightarrow> prog i = Some inst"proof - assume "(st i ** sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem))" thus ?thesis apply(unfold sep_conj_def set_ins_def sg_def trset_of.simps tpn_set_def) by autoqedlemma memD: "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem)) \<Longrightarrow> mem a = Some v"proof - assume "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem))" from stimes_sgD[OF this[unfolded trset_of.simps tpn_set_def tm_def]] have "{TM a v} \<subseteq> {TC i inst |i inst. prog i = Some inst} \<union> {TAt i} \<union> {TPos pos} \<union> {TM i n |i n. mem i = Some n} \<union> {TFaults ft}" by simp thus ?thesis by autoqedlemma t_hoare_seq: assumes a1: "\<And> i j. \<lbrace>st i \<and>* p\<rbrace> i:[c1]:j \<lbrace>st j \<and>* q\<rbrace>" and a2: "\<And> j k. \<lbrace>st j ** q\<rbrace> j:[c2]:k \<lbrace>st k ** r\<rbrace>" shows "\<lbrace>st i \<and>* p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k \<and>* r\<rbrace>"proof(subst tassemble_to.simps, rule tm.code_exI) fix j' show "\<lbrace>st i \<and>* p\<rbrace> i:[ c1 ]:j' \<and>* j':[ c2 ]:k \<lbrace>st k \<and>* r\<rbrace>" proof(rule tm.composition) from a1 show "\<lbrace>st i \<and>* p\<rbrace> i:[ c1 ]:j' \<lbrace>st j' \<and>* q\<rbrace>" by auto next from a2 show "\<lbrace>st j' \<and>* q\<rbrace> j':[ c2 ]:k \<lbrace>st k \<and>* r\<rbrace>" by auto qedqedlemma t_hoare_seq1: assumes a1: "\<And>j'. \<lbrace>st i \<and>* p\<rbrace> i:[c1]:j' \<lbrace>st j' \<and>* q\<rbrace>" assumes a2: "\<And>j'. \<lbrace>st j' \<and>* q\<rbrace> j':[c2]:k \<lbrace>st k' \<and>* r\<rbrace>" shows "\<lbrace>st i \<and>* p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k' \<and>* r\<rbrace>"proof(subst tassemble_to.simps, rule tm.code_exI) fix j' show "\<lbrace>st i \<and>* p\<rbrace> i:[ c1 ]:j' \<and>* j':[ c2 ]:k \<lbrace>st k' \<and>* r\<rbrace>" proof(rule tm.composition) from a1 show "\<lbrace>st i \<and>* p\<rbrace> i:[ c1 ]:j' \<lbrace>st j' \<and>* q\<rbrace>" by auto next from a2 show " \<lbrace>st j' \<and>* q\<rbrace> j':[ c2 ]:k \<lbrace>st k' \<and>* r\<rbrace>" by auto qedqedlemma t_hoare_seq2: assumes h: "\<And>j. \<lbrace>st i ** p\<rbrace> i:[c1]:j \<lbrace>st k' \<and>* r\<rbrace>" shows "\<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:j \<lbrace>st k' ** r\<rbrace>" apply (unfold tassemble_to.simps, rule tm.code_exI) by (rule tm.code_extension, rule h)lemma t_hoare_local: assumes h: "(\<And>l. \<lbrace>st i \<and>* p\<rbrace> i :[ c l ]: j \<lbrace>st k \<and>* q\<rbrace>)" shows "\<lbrace>st i ** p\<rbrace> i:[TLocal c]:j \<lbrace>st k ** q\<rbrace>" using h by (unfold tassemble_to.simps, intro tm.code_exI, simp)lemma t_hoare_label: assumes "\<And>l. l = i \<Longrightarrow> \<lbrace>st l \<and>* p\<rbrace> l:[ c l ]:j \<lbrace>st k \<and>* q\<rbrace>" shows "\<lbrace>st i \<and>* p\<rbrace> i:[(TLabel l; c l)]:j \<lbrace>st k \<and>* q\<rbrace>"using assmsby (unfold tassemble_to.simps, intro tm.code_exI tm.code_condI, clarify, auto)primrec t_split_cmd :: "tpg \<Rightarrow> (tpg \<times> tpg option)" where "t_split_cmd (\<guillemotright>inst) = (\<guillemotright>inst, None)" | "t_split_cmd (TLabel l) = (TLabel l, None)" | "t_split_cmd (TSeq c1 c2) = (case (t_split_cmd c2) of (c21, Some c22) \<Rightarrow> (TSeq c1 c21, Some c22) | (c21, None) \<Rightarrow> (c1, Some c21))" | "t_split_cmd (TLocal c) = (TLocal c, None)"definition "t_last_cmd tpg = snd (t_split_cmd tpg)"declare t_last_cmd_def [simp]definition "t_blast_cmd tpg = fst (t_split_cmd tpg)"declare t_blast_cmd_def [simp]lemma "t_last_cmd (c1; c2; TLabel l) = Some (TLabel l)" by simplemma "t_blast_cmd (c1; c2; TLabel l) = (c1; c2)" by simplemma t_split_cmd_eq: assumes "t_split_cmd c = (c1, Some c2)" shows "i:[c]:j = i:[(c1; c2)]:j" using assmsproof(induct c arbitrary: c1 c2 i j) case (TSeq cx cy) from `t_split_cmd (cx ; cy) = (c1, Some c2)` show ?case apply (simp split:prod.splits option.splits) apply (cases cy, auto split:prod.splits option.splits) proof - fix a assume h: "t_split_cmd cy = (a, Some c2)" show "i :[ (cx ; cy) ]: j = i :[ ((cx ; a) ; c2) ]: j" apply (simp only: tassemble_to.simps(2) TSeq(2)[OF h] sep_conj_exists) apply (simp add:sep_conj_ac) by (simp add:pred_ex_def, default, auto) qedqed autolemma t_hoare_label_last_pre: assumes h1: "t_split_cmd c = (c', Some (TLabel l))" and h2: "l = j \<Longrightarrow> \<lbrace>p\<rbrace> i:[c']:j \<lbrace>q\<rbrace>" shows "\<lbrace>p\<rbrace> i:[c]:j \<lbrace>q\<rbrace>"by (unfold t_split_cmd_eq[OF h1], simp only:tassemble_to.simps sep_conj_cond, intro tm.code_exI tm.code_condI, insert h2, auto)lemma t_hoare_label_last: assumes h1: "t_last_cmd c = Some (TLabel l)" and h2: "l = j \<Longrightarrow> \<lbrace>p\<rbrace> i:[t_blast_cmd c]:j \<lbrace>q\<rbrace>" shows "\<lbrace>p\<rbrace> i:[c]:j \<lbrace>q\<rbrace>"proof - have "t_split_cmd c = (t_blast_cmd c, t_last_cmd c)" by simp from t_hoare_label_last_pre[OF this[unfolded h1]] h2 show ?thesis by autoqedsubsection {* Basic assertions for TM *}(* ones between tape position i and j *)function ones :: "int \<Rightarrow> int \<Rightarrow> tassert" where "ones i j = (if j < i then <(i = j + 1)> else (one i) \<and>* ones (i + 1) j)"by autotermination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") autolemma ones_base_simp: "j < i \<Longrightarrow> ones i j = <(i = j + 1)>" by simplemma ones_step_simp: "\<not> j < i \<Longrightarrow> ones i j = ((one i) \<and>* ones (i + 1) j)" by simplemmas ones_simps = ones_base_simp ones_step_simpdeclare ones.simps [simp del] ones_simps [simp]lemma ones_induct [case_names Base Step]: assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)" and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (ones (i + 1) j)\<rbrakk> \<Longrightarrow> P i j ((one i) \<and>* ones (i + 1) j)" shows "P i j (ones i j)"proof(induct i j rule:ones.induct) fix i j assume ih: "(\<not> j < i \<Longrightarrow> P (i + 1) j (ones (i + 1) j))" show "P i j (ones i j)" proof(cases "j < i") case True with h1 [OF True] show ?thesis by auto next case False from h2 [OF False] and ih[OF False] have "P i j (one i \<and>* ones (i + 1) j)" by blast with False show ?thesis by auto qedqedfunction ones' :: "int \<Rightarrow> int \<Rightarrow> tassert" where "ones' i j = (if j < i then <(i = j + 1)> else ones' i (j - 1) \<and>* one j)"by autotermination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") autolemma ones_rev: "\<not> j < i \<Longrightarrow> (ones i j) = ((ones i (j - 1)) ** one j)"proof(induct i j rule:ones_induct) case Base thus ?case by autonext case (Step i j) show ?case proof(cases "j < i + 1") case True with Step show ?thesis by simp next case False with Step show ?thesis by (auto simp:sep_conj_ac) qedqedlemma ones_rev_induct [case_names Base Step]: assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)" and h2: "\<And> i j. \<lbrakk>\<not> j < i; P i (j - 1) (ones i (j - 1))\<rbrakk> \<Longrightarrow> P i j ((ones i (j - 1)) ** one j)" shows "P i j (ones i j)"proof(induct i j rule:ones'.induct) fix i j assume ih: "(\<not> j < i \<Longrightarrow> P i (j - 1) (ones i (j - 1)))" show "P i j (ones i j)" proof(cases "j < i") case True with h1 [OF True] show ?thesis by auto next case False from h2 [OF False] and ih[OF False] have "P i j (ones i (j - 1) \<and>* one j)" by blast with ones_rev and False show ?thesis by simp qedqedfunction zeros :: "int \<Rightarrow> int \<Rightarrow> tassert" where "zeros i j = (if j < i then <(i = j + 1)> else (zero i) ** zeros (i + 1) j)"by autotermination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") autolemma zeros_base_simp: "j < i \<Longrightarrow> zeros i j = <(i = j + 1)>" by simplemma zeros_step_simp: "\<not> j < i \<Longrightarrow> zeros i j = ((zero i) ** zeros (i + 1) j)" by simpdeclare zeros.simps [simp del]lemmas zeros_simps [simp] = zeros_base_simp zeros_step_simplemma zeros_induct [case_names Base Step]: assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)" and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (zeros (i + 1) j)\<rbrakk> \<Longrightarrow> P i j ((zero i) ** zeros (i + 1) j)" shows "P i j (zeros i j)"proof(induct i j rule:zeros.induct) fix i j assume ih: "(\<not> j < i \<Longrightarrow> P (i + 1) j (zeros (i + 1) j))" show "P i j (zeros i j)" proof(cases "j < i") case True with h1 [OF True] show ?thesis by auto next case False from h2 [OF False] and ih[OF False] have "P i j (zero i \<and>* zeros (i + 1) j)" by blast with False show ?thesis by auto qedqedlemma zeros_rev: "\<not> j < i \<Longrightarrow> (zeros i j) = ((zeros i (j - 1)) \<and>* zero j)"proof(induct i j rule:zeros_induct) case (Base i j) thus ?case by autonext case (Step i j) show ?case proof(cases "j < i + 1") case True with Step show ?thesis by auto next case False with Step show ?thesis by (auto simp:sep_conj_ac) qedqedlemma zeros_rev_induct [case_names Base Step]: assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)" and h2: "\<And> i j. \<lbrakk>\<not> j < i; P i (j - 1) (zeros i (j - 1))\<rbrakk> \<Longrightarrow> P i j ((zeros i (j - 1)) ** zero j)" shows "P i j (zeros i j)"proof(induct i j rule:ones'.induct) fix i j assume ih: "(\<not> j < i \<Longrightarrow> P i (j - 1) (zeros i (j - 1)))" show "P i j (zeros i j)" proof(cases "j < i") case True with h1 [OF True] show ?thesis by auto next case False from h2 [OF False] and ih[OF False] have "P i j (zeros i (j - 1) \<and>* zero j)" by blast with zeros_rev and False show ?thesis by simp qedqeddefinition "rep i j k = ((ones i (i + (int k))) \<and>* <(j = i + int k)>)"fun reps :: "int \<Rightarrow> int \<Rightarrow> nat list\<Rightarrow> tassert" where "reps i j [] = <(i = j + 1)>" | "reps i j [k] = (ones i (i + int k) ** <(j = i + int k)>)" | "reps i j (k # ks) = (ones i (i + int k) ** zero (i + int k + 1) ** reps (i + int k + 2) j ks)"lemma reps_simp3: "ks \<noteq> [] \<Longrightarrow> reps i j (k # ks) = (ones i (i + int k) ** zero (i + int k + 1) ** reps (i + int k + 2) j ks)" by (cases ks, auto)definition "reps_sep_len ks = (if length ks \<le> 1 then 0 else (length ks) - 1)"definition "reps_ctnt_len ks = (\<Sum> k \<leftarrow> ks. (1 + k))"definition "reps_len ks = (reps_sep_len ks) + (reps_ctnt_len ks)"definition "splited xs ys zs = ((xs = ys @ zs) \<and> (ys \<noteq> []) \<and> (zs \<noteq> []))"lemma list_split: assumes h: "k # ks = ys @ zs" and h1: "ys \<noteq> []" shows "(ys = [k] \<and> zs = ks) \<or> (\<exists> ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> ks = ys' @ zs)"proof(cases ys) case Nil with h1 show ?thesis by autonext case (Cons y' ys') with h have "k#ks = y'#(ys' @ zs)" by simp hence hh: "y' = k" "ks = ys' @ zs" by auto show ?thesis proof(cases "ys' = []") case False show ?thesis proof(rule disjI2) show " \<exists>ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> ks = ys' @ zs" proof(rule exI[where x = ys']) from False hh Cons show "ys' \<noteq> [] \<and> ys = k # ys' \<and> ks = ys' @ zs" by auto qed qed next case True show ?thesis proof(rule disjI1) from hh True Cons show "ys = [k] \<and> zs = ks" by auto qed qedqedlemma splited_cons[elim_format]: assumes h: "splited (k # ks) ys zs" shows "(ys = [k] \<and> zs = ks) \<or> (\<exists> ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> splited ks ys' zs)"proof - from h have "k # ks = ys @ zs" "ys \<noteq> [] " unfolding splited_def by auto from list_split[OF this] have "ys = [k] \<and> zs = ks \<or> (\<exists>ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> ks = ys' @ zs)" . thus ?thesis proof assume " ys = [k] \<and> zs = ks" thus ?thesis by auto next assume "\<exists>ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> ks = ys' @ zs" then obtain ys' where hh: "ys' \<noteq> []" "ys = k # ys'" "ks = ys' @ zs" by auto show ?thesis proof(rule disjI2) show "\<exists>ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> splited ks ys' zs" proof(rule exI[where x = ys']) from h have "zs \<noteq> []" by (unfold splited_def, simp) with hh(1) hh(3) have "splited ks ys' zs" by (unfold splited_def, auto) with hh(1) hh(2) show "ys' \<noteq> [] \<and> ys = k # ys' \<and> splited ks ys' zs" by auto qed qed qedqedlemma splited_cons_elim: assumes h: "splited (k # ks) ys zs" and h1: "\<lbrakk>ys = [k]; zs = ks\<rbrakk> \<Longrightarrow> P" and h2: "\<And> ys'. \<lbrakk>ys' \<noteq> []; ys = k#ys'; splited ks ys' zs\<rbrakk> \<Longrightarrow> P" shows Pproof(rule splited_cons[OF h]) assume "ys = [k] \<and> zs = ks \<or> (\<exists>ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> splited ks ys' zs)" thus P proof assume hh: "ys = [k] \<and> zs = ks" show P proof(rule h1) from hh show "ys = [k]" by simp next from hh show "zs = ks" by simp qed next assume "\<exists>ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> splited ks ys' zs" then obtain ys' where hh: "ys' \<noteq> []" "ys = k # ys'" "splited ks ys' zs" by auto from h2[OF this] show P . qedqedlemma list_nth_expand: "i < length xs \<Longrightarrow> xs = take i xs @ [xs!i] @ drop (Suc i) xs" by (metis Cons_eq_appendI append_take_drop_id drop_Suc_conv_tl eq_Nil_appendI)lemma reps_len_nil: "reps_len [] = 0" by (auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)lemma reps_len_sg: "reps_len [k] = 1 + k" by (auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)lemma reps_len_cons: "ks \<noteq> [] \<Longrightarrow> (reps_len (k # ks)) = 2 + k + reps_len ks "proof(induct ks arbitrary:k) case (Cons n ns) thus ?case by(cases "ns = []", auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)qed autolemma reps_len_correct: assumes h: "(reps i j ks) s" shows "j = i + int (reps_len ks) - 1" using hproof(induct ks arbitrary:i j s) case Nil thus ?case by (auto simp:reps_len_nil pasrt_def)next case (Cons n ns) thus ?case proof(cases "ns = []") case False from Cons(2)[unfolded reps_simp3[OF False]] obtain s' where "(reps (i + int n + 2) j ns) s'" by (auto elim!:sep_conjE) from Cons.hyps[OF this] show ?thesis by (unfold reps_len_cons[OF False], simp) next case True with Cons(2) show ?thesis by (auto simp:reps_len_sg pasrt_def) qedqedlemma reps_len_expand: shows "(EXS j. (reps i j ks)) = (reps i (i + int (reps_len ks) - 1) ks)"proof(default+) fix s assume "(EXS j. reps i j ks) s" with reps_len_correct show "reps i (i + int (reps_len ks) - 1) ks s" by (auto simp:pred_ex_def)next fix s assume "reps i (i + int (reps_len ks) - 1) ks s" thus "(EXS j. reps i j ks) s" by (auto simp:pred_ex_def)qedlemma reps_len_expand1: "(EXS j. (reps i j ks \<and>* r)) = (reps i (i + int (reps_len ks) - 1) ks \<and>* r)"by (metis reps_len_def reps_len_expand sep.mult_commute sep_conj_exists1)lemma reps_splited: assumes h: "splited xs ys zs" shows "reps i j xs = (reps i (i + int (reps_len ys) - 1) ys \<and>* zero (i + int (reps_len ys)) \<and>* reps (i + int (reps_len ys) + 1) j zs)" using hproof(induct xs arbitrary: i j ys zs) case Nil thus ?case by (unfold splited_def, auto)next case (Cons k ks) from Cons(2) show ?case proof(rule splited_cons_elim) assume h: "ys = [k]" "zs = ks" with Cons(2) show ?thesis proof(cases "ks = []") case True with Cons(2) have False by (simp add:splited_def, cases ys, auto) thus ?thesis by auto next case False have ss: "i + int k + 1 = i + (1 + int k)" "i + int k + 2 = 2 + (i + int k)" by auto show ?thesis by (unfold h(1), unfold reps_simp3[OF False] reps.simps(2) reps_len_sg, auto simp:sep_conj_ac, unfold ss h(2), simp) qed next fix ys' assume h: "ys' \<noteq> []" "ys = k # ys'" "splited ks ys' zs" hence nnks: "ks \<noteq> []" by (unfold splited_def, auto) have ss: "i + int k + 2 + int (reps_len ys') = i + (2 + (int k + int (reps_len ys')))" by auto show ?thesis by (simp add: reps_simp3[OF nnks] reps_simp3[OF h(1)] Cons(1)[OF h(3)] h(2) reps_len_cons[OF h(1)] sep_conj_ac, subst ss, simp) qedqedsubsection {* A theory of list extension *}definition "list_ext n xs = xs @ replicate ((Suc n) - length xs) 0"lemma list_ext_len_eq: "length (list_ext a xs) = length xs + (Suc a - length xs)" by (metis length_append length_replicate list_ext_def)lemma list_ext_len: "a < length (list_ext a xs)" by (unfold list_ext_len_eq, auto)lemma list_ext_lt: "a < length xs \<Longrightarrow> list_ext a xs = xs" by (smt append_Nil2 list_ext_def replicate_0)lemma list_ext_lt_get: assumes h: "a' < length xs" shows "(list_ext a xs)!a' = xs!a'"proof(cases "a < length xs") case True with h show ?thesis by (auto simp:list_ext_lt)next case False with h show ?thesis apply (unfold list_ext_def) by (metis nth_append)qedlemma list_ext_get_upd: "((list_ext a xs)[a:=v])!a = v" by (metis list_ext_len nth_list_update_eq)lemma nth_app: "length xs \<le> a \<Longrightarrow> (xs @ ys)!a = ys!(a - length xs)" by (metis not_less nth_append)lemma list_ext_tail: assumes h1: "length xs \<le> a" and h2: "length xs \<le> a'" and h3: "a' \<le> a" shows "(list_ext a xs)!a' = 0"proof - from h1 h2 have "a' - length xs < length (replicate (Suc a - length xs) 0)" by (metis diff_less_mono h3 le_imp_less_Suc length_replicate) moreover from h1 have "replicate (Suc a - length xs) 0 \<noteq> []" by (smt empty_replicate) ultimately have "(replicate (Suc a - length xs) 0)!(a' - length xs) = 0" by (metis length_replicate nth_replicate) moreover have "(xs @ (replicate (Suc a - length xs) 0))!a' = (replicate (Suc a - length xs) 0)!(a' - length xs)" by (rule nth_app[OF h2]) ultimately show ?thesis by (auto simp:list_ext_def)qedlemmas list_ext_simps = list_ext_lt_get list_ext_lt list_ext_len list_ext_len_eqlemma listsum_upd_suc: "a < length ks \<Longrightarrow> listsum (map Suc (ks[a := Suc (ks ! a)]))= (Suc (listsum (map Suc ks)))"by (smt elem_le_listsum_nat length_list_update list_ext_get_upd list_update_overwrite listsum_update_nat map_update nth_equalityI nth_list_update nth_map)lemma reps_len_suc: assumes "a < length ks" shows "reps_len (ks[a:=Suc(ks!a)]) = 1 + reps_len ks"proof(cases "length ks \<le> 1") case True with `a < length ks` obtain k where "ks = [k]" "a = 0" by (smt length_0_conv length_Suc_conv) thus ?thesis apply (unfold `ks = [k]` `a = 0`) by (unfold reps_len_def reps_sep_len_def reps_ctnt_len_def, auto)next case False have "Suc = (op + (Suc 0))" by (default, auto) with listsum_upd_suc[OF `a < length ks`] False show ?thesis by (unfold reps_len_def reps_sep_len_def reps_ctnt_len_def, simp)qedlemma ks_suc_len: assumes h1: "(reps i j ks) s" and h2: "ks!a = v" and h3: "a < length ks" and h4: "(reps i j' (ks[a:=Suc v])) s'" shows "j' = j + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1"proof - from reps_len_correct[OF h1, unfolded list_ext_len_eq] reps_len_correct[OF h4, unfolded list_ext_len_eq] reps_len_suc[OF `a < length ks`] h2 h3 show ?thesis by (unfold list_ext_lt[OF `a < length ks`], auto)qedlemma ks_ext_len: assumes h1: "(reps i j ks) s" and h3: "length ks \<le> a" and h4: "reps i j' (list_ext a ks) s'" shows "j' = j + int (reps_len (list_ext a ks)) - int (reps_len ks)"proof - from reps_len_correct[OF h1, unfolded list_ext_len_eq] and reps_len_correct[OF h4, unfolded list_ext_len_eq] h3 show ?thesis by autoqeddefinition "reps' i j ks = (if ks = [] then (<(i = j + 1)>) else (reps i (j - 1) ks \<and>* zero j))"lemma reps'_expand: assumes h: "ks \<noteq> []" shows "(EXS j. reps' i j ks) = reps' i (i + int (reps_len ks)) ks"proof - show ?thesis proof(default+) fix s assume "(EXS j. reps' i j ks) s" with h have "(EXS j. reps i (j - 1) ks \<and>* zero j) s" by (simp add:reps'_def) hence "(reps i (i + int (reps_len ks) - 1) ks \<and>* zero (i + int (reps_len ks))) s" proof(elim EXS_elim) fix j assume "(reps i (j - 1) ks \<and>* zero j) s" then obtain s1 s2 where "s = s1 + s2" "s1 ## s2" "reps i (j - 1) ks s1" "zero j s2" by (auto elim!:sep_conjE) from reps_len_correct[OF this(3)] have "j = i + int (reps_len ks)" by auto with `reps i (j - 1) ks s1` have "reps i (i + int (reps_len ks) - 1) ks s1" by simp moreover from `j = i + int (reps_len ks)` and `zero j s2` have "zero (i + int (reps_len ks)) s2" by auto ultimately show "(reps i (i + int (reps_len ks) - 1) ks \<and>* zero (i + int (reps_len ks))) s" using `s = s1 + s2` `s1 ## s2` by (auto intro!:sep_conjI) qed thus "reps' i (i + int (reps_len ks)) ks s" by (simp add:h reps'_def) next fix s assume "reps' i (i + int (reps_len ks)) ks s" thus "(EXS j. reps' i j ks) s" by (auto intro!:EXS_intro) qedqedlemma reps'_len_correct: assumes h: "(reps' i j ks) s" and h1: "ks \<noteq> []" shows "(j = i + int (reps_len ks))"proof - from h1 have "reps' i j ks s = (reps i (j - 1) ks \<and>* zero j) s" by (simp add:reps'_def) from h[unfolded this] obtain s' where "reps i (j - 1) ks s'" by (auto elim!:sep_conjE) from reps_len_correct[OF this] show ?thesis by simpqedlemma reps'_append: "reps' i j (ks1 @ ks2) = (EXS m. (reps' i (m - 1) ks1 \<and>* reps' m j ks2))"proof(cases "ks1 = []") case True thus ?thesis by (auto simp:reps'_def pred_ex_def pasrt_def set_ins_def sep_conj_def)next case False show ?thesis proof(cases "ks2 = []") case False from `ks1 \<noteq> []` and `ks2 \<noteq> []` have "splited (ks1 @ ks2) ks1 ks2" by (auto simp:splited_def) from reps_splited[OF this, of i "j - 1"] have eq_1: "reps i (j - 1) (ks1 @ ks2) = (reps i (i + int (reps_len ks1) - 1) ks1 \<and>* zero (i + int (reps_len ks1)) \<and>* reps (i + int (reps_len ks1) + 1) (j - 1) ks2)" . from `ks1 \<noteq> []` have eq_2: "reps' i j (ks1 @ ks2) = (reps i (j - 1) (ks1 @ ks2) \<and>* zero j)" by (unfold reps'_def, simp) show ?thesis proof(default+) fix s assume "reps' i j (ks1 @ ks2) s" show "(EXS m. reps' i (m - 1) ks1 \<and>* reps' m j ks2) s" proof(rule EXS_intro[where x = "i + int(reps_len ks1) + 1"]) from `reps' i j (ks1 @ ks2) s`[unfolded eq_2 eq_1] and `ks1 \<noteq> []` `ks2 \<noteq> []` show "(reps' i (i + int (reps_len ks1) + 1 - 1) ks1 \<and>* reps' (i + int (reps_len ks1) + 1) j ks2) s" by (unfold reps'_def, simp, sep_cancel+) qed next fix s assume "(EXS m. reps' i (m - 1) ks1 \<and>* reps' m j ks2) s" thus "reps' i j (ks1 @ ks2) s" proof(elim EXS_elim) fix m assume "(reps' i (m - 1) ks1 \<and>* reps' m j ks2) s" then obtain s1 s2 where h: "s = s1 + s2" "s1 ## s2" "reps' i (m - 1) ks1 s1" " reps' m j ks2 s2" by (auto elim!:sep_conjE) from reps'_len_correct[OF this(3) `ks1 \<noteq> []`] have eq_m: "m = i + int (reps_len ks1) + 1" by simp have "((reps i (i + int (reps_len ks1) - 1) ks1 \<and>* zero (i + int (reps_len ks1))) \<and>* ((reps (i + int (reps_len ks1) + 1) (j - 1) ks2) \<and>* zero j)) s" (is "(?P \<and>* ?Q) s") proof(rule sep_conjI) from h(3) eq_m `ks1 \<noteq> []` show "?P s1" by (simp add:reps'_def) next from h(4) eq_m `ks2 \<noteq> []` show "?Q s2" by (simp add:reps'_def) next from h(2) show "s1 ## s2" . next from h(1) show "s = s1 + s2" . qed thus "reps' i j (ks1 @ ks2) s" by (unfold eq_2 eq_1, auto simp:sep_conj_ac) qed qed next case True have "-1 + j = j - 1" by auto with `ks1 \<noteq> []` True show ?thesis apply (auto simp:reps'_def pred_ex_def pasrt_def) apply (unfold `-1 + j = j - 1`) by (fold sep_empty_def, simp only:sep_conj_empty) qedqedlemma reps'_sg: "reps' i j [k] = (<(j = i + int k + 1)> \<and>* ones i (i + int k) \<and>* zero j)" apply (unfold reps'_def, default, auto simp:sep_conj_ac) by (sep_cancel+, simp add:pasrt_def)+section {* Basic macros for TM *}definition "write_zero = (TL exit. \<guillemotright>((W0, exit), (W0, exit)); TLabel exit)"lemma st_upd: assumes pre: "(st i' ** r) (trset_of (f, x, i, y, z))" shows "(st i'' ** r) (trset_of (f, x, i'', y, z))"proof - from stimes_sgD[OF pre[unfolded st_def], unfolded trset_of.simps, unfolded stD[OF pre]] have "r (tprog_set x \<union> tpc_set i' \<union> tpos_set y \<union> tmem_set z \<union> tfaults_set f - tpc_set i')" by blast moreover have "(tprog_set x \<union> tpc_set i' \<union> tpos_set y \<union> tmem_set z \<union> tfaults_set f - tpc_set i') = (tprog_set x \<union> tpos_set y \<union> tmem_set z \<union> tfaults_set f)" by (unfold tpn_set_def, auto) ultimately have r_rest: "r (tprog_set x \<union> tpos_set y \<union> tmem_set z \<union> tfaults_set f)" by auto show ?thesis proof(rule sep_conjI[where Q = r, OF _ r_rest]) show "st i'' (tpc_set i'')" by (unfold st_def sg_def, simp) next show "tpc_set i'' ## tprog_set x \<union> tpos_set y \<union> tmem_set z \<union> tfaults_set f" by (unfold tpn_set_def sep_disj_set_def, auto) next show "trset_of (f, x, i'', y, z) = tpc_set i'' + (tprog_set x \<union> tpos_set y \<union> tmem_set z \<union> tfaults_set f)" by (unfold trset_of.simps plus_set_def, auto) qedqedlemma pos_upd: assumes pre: "(ps i ** r) (trset_of (f, x, y, i', z))" shows "(ps j ** r) (trset_of (f, x, y, j, z))"proof - from stimes_sgD[OF pre[unfolded ps_def], unfolded trset_of.simps, unfolded psD[OF pre]] have "r (tprog_set x \<union> tpc_set y \<union> tpos_set i \<union> tmem_set z \<union> tfaults_set f - tpos_set i)" (is "r ?xs") by blast moreover have "?xs = tprog_set x \<union> tpc_set y \<union> tmem_set z \<union> tfaults_set f" by (unfold tpn_set_def, auto) ultimately have r_rest: "r \<dots>" by auto show ?thesis proof(rule sep_conjI[where Q = r, OF _ r_rest]) show "ps j (tpos_set j)" by (unfold ps_def sg_def, simp) next show "tpos_set j ## tprog_set x \<union> tpc_set y \<union> tmem_set z \<union> tfaults_set f" by (unfold tpn_set_def sep_disj_set_def, auto) next show "trset_of (f, x, y, j, z) = tpos_set j + (tprog_set x \<union> tpc_set y \<union> tmem_set z \<union> tfaults_set f)" by (unfold trset_of.simps plus_set_def, auto) qedqedlemma TM_in_simp: "({TM a v} \<subseteq> tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tmem_set mem \<union> tfaults_set f) = ({TM a v} \<subseteq> tmem_set mem)" by (unfold tpn_set_def, auto)lemma tmem_set_upd: "{TM a v} \<subseteq> tmem_set mem \<Longrightarrow> tmem_set (mem(a:=Some v')) = ((tmem_set mem) - {TM a v}) \<union> {TM a v'}" by (unfold tpn_set_def, auto)lemma tmem_set_disj: "{TM a v} \<subseteq> tmem_set mem \<Longrightarrow> {TM a v'} \<inter> (tmem_set mem - {TM a v}) = {}" by (unfold tpn_set_def, auto)lemma smem_upd: "((tm a v) ** r) (trset_of (f, x, y, z, mem)) \<Longrightarrow> ((tm a v') ** r) (trset_of (f, x, y, z, mem(a := Some v')))"proof - have eq_s: "(tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tmem_set mem \<union> tfaults_set f - {TM a v}) = (tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f)" by (unfold tpn_set_def, auto) assume g: "(tm a v \<and>* r) (trset_of (f, x, y, z, mem))" from this[unfolded trset_of.simps tm_def] have h: "(sg {TM a v} \<and>* r) (tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tmem_set mem \<union> tfaults_set f)" . hence h0: "r (tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f)" by(sep_drule stimes_sgD, clarify, unfold eq_s, auto) from h TM_in_simp have "{TM a v} \<subseteq> tmem_set mem" by(sep_drule stimes_sgD, auto) from tmem_set_upd [OF this] tmem_set_disj[OF this] have h2: "tmem_set (mem(a \<mapsto> v')) = {TM a v'} \<union> (tmem_set mem - {TM a v})" "{TM a v'} \<inter> (tmem_set mem - {TM a v}) = {}" by auto show ?thesis proof - have "(tm a v' ** r) (tmem_set (mem(a \<mapsto> v')) \<union> tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tfaults_set f)" proof(rule sep_conjI) show "tm a v' ({TM a v'})" by (unfold tm_def sg_def, simp) next from h0 show "r (tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f)" . next show "{TM a v'} ## tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f" proof - from g have " mem a = Some v" by(sep_frule memD, simp) thus "?thesis" by(unfold tpn_set_def set_ins_def, auto) qed next show "tmem_set (mem(a \<mapsto> v')) \<union> tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tfaults_set f = {TM a v'} + (tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f)" by (unfold h2(1) set_ins_def eq_s, auto) qed thus ?thesis apply (unfold trset_of.simps) by (metis sup_commute sup_left_commute) qedqedlemma hoare_write_zero: "\<lbrace>st i ** ps p ** tm p v\<rbrace> i:[write_zero]:j \<lbrace>st j ** ps p ** tm p Bk\<rbrace>"proof(unfold write_zero_def, intro t_hoare_local, rule t_hoare_label_last, simp, simp) show "\<lbrace>st i \<and>* ps p \<and>* tm p v\<rbrace> i :[ \<guillemotright> ((W0, j), W0, j) ]: j \<lbrace>st j \<and>* ps p \<and>* tm p Bk\<rbrace>" proof(unfold tassemble_to.simps, simp only:sep_conj_cond, intro tm.code_condI, simp) assume eq_j: "j = Suc i" show "\<lbrace>st i \<and>* ps p \<and>* tm p v\<rbrace> sg {TC i ((W0, Suc i), W0, Suc i)} \<lbrace>st (Suc i) \<and>* ps p \<and>* tm p Bk\<rbrace>" proof(fold eq_j, unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) fix ft prog cs i' mem r assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v \<and>* sg {TC i ((W0, j), W0, j)}) (trset_of (ft, prog, cs, i', mem))" from h have "prog i = Some ((W0, j), W0, j)" apply(rule_tac r = "r \<and>* ps p \<and>* tm p v" in codeD) by(simp add: sep_conj_ac) from h and this have stp: "tm.run 1 (ft, prog, cs, i', mem) = (ft, prog, j, i', mem(i'\<mapsto> Bk))" (is "?x = ?y") apply(sep_frule psD) apply(sep_frule stD) apply(sep_frule memD, simp) by(cases v, unfold tm.run_def, auto) from h have "i' = p" by(sep_drule psD, simp) with h have "(r \<and>* ps p \<and>* st j \<and>* tm p Bk \<and>* sg {TC i ((W0, j), W0, j)}) (trset_of ?x)" apply(unfold stp) apply(sep_drule pos_upd, sep_drule st_upd, sep_drule smem_upd) apply(auto simp: sep_conj_ac) done thus "\<exists>k. (r \<and>* ps p \<and>* st j \<and>* tm p Bk \<and>* sg {TC i ((W0, j), W0, j)}) (trset_of (tm.run (Suc k) (ft, prog, cs, i', mem)))" apply (rule_tac x = 0 in exI) by auto qed qedqedlemma hoare_write_zero_gen[step]: assumes "p = q" shows "\<lbrace>st i ** ps p ** tm q v\<rbrace> i:[write_zero]:j \<lbrace>st j ** ps p ** tm q Bk\<rbrace>" by (unfold assms, rule hoare_write_zero)definition "write_one = (TL exit. \<guillemotright>((W1, exit), (W1, exit)); TLabel exit)"lemma hoare_write_one: "\<lbrace>st i ** ps p ** tm p v\<rbrace> i:[write_one]:j \<lbrace>st j ** ps p ** tm p Oc\<rbrace>"proof(unfold write_one_def, intro t_hoare_local, rule t_hoare_label_last, simp+) fix l show "\<lbrace>st i \<and>* ps p \<and>* tm p v\<rbrace> i :[ \<guillemotright> ((W1, j), W1, j) ]: j \<lbrace>st j \<and>* ps p \<and>* tm p Oc\<rbrace>" proof(unfold tassemble_to.simps, simp only:sep_conj_cond, rule_tac tm.code_condI, simp add: sep_conj_ac) let ?j = "Suc i" show "\<lbrace>ps p \<and>* st i \<and>* tm p v\<rbrace> sg {TC i ((W1, ?j), W1, ?j)} \<lbrace>ps p \<and>* st ?j \<and>* tm p Oc\<rbrace>" proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) fix ft prog cs i' mem r assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v \<and>* sg {TC i ((W1, ?j), W1, ?j)}) (trset_of (ft, prog, cs, i', mem))" from h have "prog i = Some ((W1, ?j), W1, ?j)" apply(rule_tac r = "r \<and>* ps p \<and>* tm p v" in codeD) by(simp add: sep_conj_ac) from h and this have stp: "tm.run 1 (ft, prog, cs, i', mem) = (ft, prog, ?j, i', mem(i'\<mapsto> Oc))" (is "?x = ?y") apply(sep_frule psD) apply(sep_frule stD) apply(sep_frule memD, simp) by(cases v, unfold tm.run_def, auto) from h have "i' = p" by(sep_drule psD, simp) with h have "(r \<and>* ps p \<and>* st ?j \<and>* tm p Oc \<and>* sg {TC i ((W1, ?j), W1, ?j)}) (trset_of ?x)" apply(unfold stp) apply(sep_drule pos_upd, sep_drule st_upd, sep_drule smem_upd) apply(auto simp: sep_conj_ac) done thus "\<exists>k. (r \<and>* ps p \<and>* st ?j \<and>* tm p Oc \<and>* sg {TC i ((W1, ?j), W1, ?j)}) (trset_of (tm.run (Suc k) (ft, prog, cs, i', mem)))" apply (rule_tac x = 0 in exI) by auto qed qedqedlemma hoare_write_one_gen[step]: assumes "p = q" shows "\<lbrace>st i ** ps p ** tm q v\<rbrace> i:[write_one]:j \<lbrace>st j ** ps p ** tm q Oc\<rbrace>" by (unfold assms, rule hoare_write_one)definition "move_left = (TL exit . \<guillemotright>((L, exit), (L, exit)); TLabel exit)"lemma hoare_move_left: "\<lbrace>st i ** ps p ** tm p v2\<rbrace> i:[move_left]:j \<lbrace>st j ** ps (p - 1) ** tm p v2\<rbrace>"proof(unfold move_left_def, intro t_hoare_local, rule t_hoare_label_last, simp+) fix l show "\<lbrace>st i \<and>* ps p \<and>* tm p v2\<rbrace> i :[ \<guillemotright> ((L, l), L, l) ]: l \<lbrace>st l \<and>* ps (p - 1) \<and>* tm p v2\<rbrace>" proof(unfold tassemble_to.simps, simp only:sep_conj_cond, intro tm.code_condI, simp add: sep_conj_ac) let ?j = "Suc i" show "\<lbrace>ps p \<and>* st i \<and>* tm p v2\<rbrace> sg {TC i ((L, ?j), L, ?j)} \<lbrace>st ?j \<and>* tm p v2 \<and>* ps (p - 1)\<rbrace>" proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) fix ft prog cs i' mem r assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v2 \<and>* sg {TC i ((L, ?j), L, ?j)}) (trset_of (ft, prog, cs, i', mem))" from h have "prog i = Some ((L, ?j), L, ?j)" apply(rule_tac r = "r \<and>* ps p \<and>* tm p v2" in codeD) by(simp add: sep_conj_ac) from h and this have stp: "tm.run 1 (ft, prog, cs, i', mem) = (ft, prog, ?j, i' - 1, mem)" (is "?x = ?y") apply(sep_frule psD) apply(sep_frule stD) apply(sep_frule memD, simp) apply(unfold tm.run_def, case_tac v2, auto) done from h have "i' = p" by(sep_drule psD, simp) with h have "(r \<and>* st ?j \<and>* tm p v2 \<and>* ps (p - 1) \<and>* sg {TC i ((L, ?j), L, ?j)}) (trset_of ?x)" apply(unfold stp) apply(sep_drule pos_upd, sep_drule st_upd, simp) proof - assume "(st ?j \<and>* ps (p - 1) \<and>* r \<and>* tm p v2 \<and>* sg {TC i ((L, ?j), L, ?j)}) (trset_of (ft, prog, ?j, p - 1, mem))" thus "(r \<and>* st ?j \<and>* tm p v2 \<and>* ps (p - 1) \<and>* sg {TC i ((L, ?j), L, ?j)}) (trset_of (ft, prog, ?j, p - 1, mem))" by(simp add: sep_conj_ac) qed thus "\<exists>k. (r \<and>* st ?j \<and>* tm p v2 \<and>* ps (p - 1) \<and>* sg {TC i ((L, ?j), L, ?j)}) (trset_of (tm.run (Suc k) (ft, prog, cs, i', mem)))" apply (rule_tac x = 0 in exI) by auto qed qedqedlemma hoare_move_left_gen[step]: assumes "p = q" shows "\<lbrace>st i ** ps p ** tm q v2\<rbrace> i:[move_left]:j \<lbrace>st j ** ps (p - 1) ** tm q v2\<rbrace>" by (unfold assms, rule hoare_move_left)definition "move_right = (TL exit . \<guillemotright>((R, exit), (R, exit)); TLabel exit)"lemma hoare_move_right: "\<lbrace>st i ** ps p ** tm p v1 \<rbrace> i:[move_right]:j \<lbrace>st j ** ps (p + 1) ** tm p v1 \<rbrace>"proof(unfold move_right_def, intro t_hoare_local, rule t_hoare_label_last, simp+) fix l show "\<lbrace>st i \<and>* ps p \<and>* tm p v1\<rbrace> i :[ \<guillemotright> ((R, l), R, l) ]: l \<lbrace>st l \<and>* ps (p + 1) \<and>* tm p v1\<rbrace>" proof(unfold tassemble_to.simps, simp only:sep_conj_cond, intro tm.code_condI, simp add: sep_conj_ac) let ?j = "Suc i" show "\<lbrace>ps p \<and>* st i \<and>* tm p v1\<rbrace> sg {TC i ((R, ?j), R, ?j)} \<lbrace>st ?j \<and>* tm p v1 \<and>* ps (p + 1)\<rbrace>" proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) fix ft prog cs i' mem r assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v1 \<and>* sg {TC i ((R, ?j), R, ?j)}) (trset_of (ft, prog, cs, i', mem))" from h have "prog i = Some ((R, ?j), R, ?j)" apply(rule_tac r = "r \<and>* ps p \<and>* tm p v1" in codeD) by(simp add: sep_conj_ac) from h and this have stp: "tm.run 1 (ft, prog, cs, i', mem) = (ft, prog, ?j, i'+ 1, mem)" (is "?x = ?y") apply(sep_frule psD) apply(sep_frule stD) apply(sep_frule memD, simp) apply(unfold tm.run_def, case_tac v1, auto) done from h have "i' = p" by(sep_drule psD, simp) with h have "(r \<and>* st ?j \<and>* tm p v1 \<and>* ps (p + 1) \<and>* sg {TC i ((R, ?j), R, ?j)}) (trset_of ?x)" apply(unfold stp) apply(sep_drule pos_upd, sep_drule st_upd, simp) proof - assume "(st ?j \<and>* ps (p + 1) \<and>* r \<and>* tm p v1 \<and>* sg {TC i ((R, ?j), R, ?j)}) (trset_of (ft, prog, ?j, p + 1, mem))" thus "(r \<and>* st ?j \<and>* tm p v1 \<and>* ps (p + 1) \<and>* sg {TC i ((R, ?j), R, ?j)}) (trset_of (ft, prog, ?j, p + 1, mem))" by (simp add: sep_conj_ac) qed thus "\<exists>k. (r \<and>* st ?j \<and>* tm p v1 \<and>* ps (p + 1) \<and>* sg {TC i ((R, ?j), R, ?j)}) (trset_of (tm.run (Suc k) (ft, prog, cs, i', mem)))" apply (rule_tac x = 0 in exI) by auto qed qedqedlemma hoare_move_right_gen[step]: assumes "p = q" shows "\<lbrace>st i ** ps p ** tm q v1 \<rbrace> i:[move_right]:j \<lbrace>st j ** ps (p + 1) ** tm q v1 \<rbrace>" by (unfold assms, rule hoare_move_right)definition "if_one e = (TL exit . \<guillemotright>((W0, exit), (W1, e)); TLabel exit)"lemma hoare_if_one_true: "\<lbrace>st i ** ps p ** one p\<rbrace> i:[if_one e]:j \<lbrace>st e ** ps p ** one p\<rbrace>"proof(unfold if_one_def, intro t_hoare_local, rule t_hoare_label_last, simp+) fix l show " \<lbrace>st i \<and>* ps p \<and>* one p\<rbrace> i :[ \<guillemotright> ((W0, l), W1, e) ]: l \<lbrace>st e \<and>* ps p \<and>* one p\<rbrace>" proof(unfold tassemble_to.simps, simp only:sep_conj_cond, intro tm.code_condI, simp add: sep_conj_ac) let ?j = "Suc i" show "\<lbrace>one p \<and>* ps p \<and>* st i\<rbrace> sg {TC i ((W0, ?j), W1, e)} \<lbrace>one p \<and>* ps p \<and>* st e\<rbrace>" proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) fix ft prog cs pc mem r assume h: "(r \<and>* one p \<and>* ps p \<and>* st i \<and>* sg {TC i ((W0, ?j), W1, e)}) (trset_of (ft, prog, cs, pc, mem))" from h have k1: "prog i = Some ((W0, ?j), W1, e)" apply(rule_tac r = "r \<and>* one p \<and>* ps p" in codeD) by(simp add: sep_conj_ac) from h have k2: "pc = p" by(sep_drule psD, simp) from h and this have k3: "mem pc = Some Oc" apply(unfold one_def) by(sep_drule memD, simp) from h k1 k2 k3 have stp: "tm.run 1 (ft, prog, cs, pc, mem) = (ft, prog, e, pc, mem)" (is "?x = ?y") apply(sep_drule stD) by(unfold tm.run_def, auto) from h k2 have "(r \<and>* one p \<and>* ps p \<and>* st e \<and>* sg {TC i ((W0, ?j), W1, e)}) (trset_of ?x)" apply(unfold stp) by(sep_drule st_upd, simp add: sep_conj_ac) thus "\<exists>k.(r \<and>* one p \<and>* ps p \<and>* st e \<and>* sg {TC i ((W0, ?j), W1, e)}) (trset_of (tm.run (Suc k) (ft, prog, cs, pc, mem)))" apply (rule_tac x = 0 in exI) by auto qed qedqedtext {* The following problematic lemma is not provable now lemma hoare_self: "\<lbrace>p\<rbrace> i :[ap]: j \<lbrace>p\<rbrace>" apply(simp add: tm.Hoare_gen_def, clarify) apply(rule_tac x = 0 in exI, simp add: tm.run_def) done*}lemma hoare_if_one_true_gen[step]: assumes "p = q" shows "\<lbrace>st i ** ps p ** one q\<rbrace> i:[if_one e]:j \<lbrace>st e ** ps p ** one q\<rbrace>" by (unfold assms, rule hoare_if_one_true)lemma hoare_if_one_true1: "\<lbrace>st i ** ps p ** one p\<rbrace> i:[(if_one e; c)]:j \<lbrace>st e ** ps p ** one p\<rbrace>"proof(unfold tassemble_to.simps, rule tm.code_exI, simp add: sep_conj_ac tm.Hoare_gen_def, clarify) fix j' ft prog cs pos mem r assume h: "(r \<and>* one p \<and>* ps p \<and>* st i \<and>* j' :[ c ]: j \<and>* i :[ if_one e ]: j') (trset_of (ft, prog, cs, pos, mem))" from tm.frame_rule[OF hoare_if_one_true] have "\<And> r. \<lbrace>st i \<and>* ps p \<and>* one p \<and>* r\<rbrace> i :[ if_one e ]: j' \<lbrace>st e \<and>* ps p \<and>* one p \<and>* r\<rbrace>" by(simp add: sep_conj_ac) from this[unfolded tm.Hoare_gen_def tassemble_to.simps, rule_format, of "j' :[ c ]: j"] h have "\<exists> k. (r \<and>* one p \<and>* ps p \<and>* st e \<and>* i :[ if_one e ]: j' \<and>* j' :[ c ]: j) (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" by(auto simp: sep_conj_ac) thus "\<exists>k. (r \<and>* one p \<and>* ps p \<and>* st e \<and>* j' :[ c ]: j \<and>* i :[ if_one e ]: j') (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" by(simp add: sep_conj_ac)qedlemma hoare_if_one_true1_gen[step]: assumes "p = q" shows "\<lbrace>st i ** ps p ** one q\<rbrace> i:[(if_one e; c)]:j \<lbrace>st e ** ps p ** one q\<rbrace>" by (unfold assms, rule hoare_if_one_true1)lemma hoare_if_one_false: "\<lbrace>st i ** ps p ** zero p\<rbrace> i:[if_one e]:j \<lbrace>st j ** ps p ** zero p\<rbrace>"proof(unfold if_one_def, intro t_hoare_local, rule t_hoare_label_last, simp+) show "\<lbrace>st i \<and>* ps p \<and>* zero p\<rbrace> i :[ (\<guillemotright> ((W0, j), W1, e)) ]: j \<lbrace>st j \<and>* ps p \<and>* zero p\<rbrace>" proof(unfold tassemble_to.simps, simp only:sep_conj_cond, intro tm.code_condI, simp add: sep_conj_ac) let ?j = "Suc i" show "\<lbrace>ps p \<and>* st i \<and>* zero p\<rbrace> sg {TC i ((W0, ?j), W1, e)} \<lbrace>ps p \<and>* zero p \<and>* st ?j \<rbrace>" proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) fix ft prog cs pc mem r assume h: "(r \<and>* ps p \<and>* st i \<and>* zero p \<and>* sg {TC i ((W0, ?j), W1, e)}) (trset_of (ft, prog, cs, pc, mem))" from h have k1: "prog i = Some ((W0, ?j), W1, e)" apply(rule_tac r = "r \<and>* zero p \<and>* ps p" in codeD) by(simp add: sep_conj_ac) from h have k2: "pc = p" by(sep_drule psD, simp) from h and this have k3: "mem pc = Some Bk" apply(unfold zero_def) by(sep_drule memD, simp) from h k1 k2 k3 have stp: "tm.run 1 (ft, prog, cs, pc, mem) = (ft, prog, ?j, pc, mem)" (is "?x = ?y") apply(sep_drule stD) by(unfold tm.run_def, auto) from h k2 have "(r \<and>* zero p \<and>* ps p \<and>* st ?j \<and>* sg {TC i ((W0, ?j), W1, e)}) (trset_of ?x)" apply (unfold stp) by (sep_drule st_upd[where i''="?j"], auto simp:sep_conj_ac) thus "\<exists>k. (r \<and>* ps p \<and>* zero p \<and>* st ?j \<and>* sg {TC i ((W0, ?j), W1, e)}) (trset_of (tm.run (Suc k) (ft, prog, cs, pc, mem)))" by(auto simp: sep_conj_ac) qed qedqedlemma hoare_if_one_false_gen[step]: assumes "p = q" shows "\<lbrace>st i ** ps p ** zero q\<rbrace> i:[if_one e]:j \<lbrace>st j ** ps p ** zero q\<rbrace>" by (unfold assms, rule hoare_if_one_false)definition "if_zero e = (TL exit . \<guillemotright>((W0, e), (W1, exit)); TLabel exit)"lemma hoare_if_zero_true: "\<lbrace>st i ** ps p ** zero p\<rbrace> i:[if_zero e]:j \<lbrace>st e ** ps p ** zero p\<rbrace>"proof(unfold if_zero_def, intro t_hoare_local, rule t_hoare_label_last, simp+) fix l show "\<lbrace>st i \<and>* ps p \<and>* zero p\<rbrace> i :[ \<guillemotright> ((W0, e), W1, l) ]: l \<lbrace>st e \<and>* ps p \<and>* zero p\<rbrace>" proof(unfold tassemble_to.simps, simp only:sep_conj_cond, intro tm.code_condI, simp add: sep_conj_ac) let ?j = "Suc i" show "\<lbrace>ps p \<and>* st i \<and>* zero p\<rbrace> sg {TC i ((W0, e), W1, ?j)} \<lbrace>ps p \<and>* st e \<and>* zero p\<rbrace>" proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) fix ft prog cs pc mem r assume h: "(r \<and>* ps p \<and>* st i \<and>* zero p \<and>* sg {TC i ((W0, e), W1, ?j)}) (trset_of (ft, prog, cs, pc, mem))" from h have k1: "prog i = Some ((W0, e), W1, ?j)" apply(rule_tac r = "r \<and>* zero p \<and>* ps p" in codeD) by(simp add: sep_conj_ac) from h have k2: "pc = p" by(sep_drule psD, simp) from h and this have k3: "mem pc = Some Bk" apply(unfold zero_def) by(sep_drule memD, simp) from h k1 k2 k3 have stp: "tm.run 1 (ft, prog, cs, pc, mem) = (ft, prog, e, pc, mem)" (is "?x = ?y") apply(sep_drule stD) by(unfold tm.run_def, auto) from h k2 have "(r \<and>* zero p \<and>* ps p \<and>* st e \<and>* sg {TC i ((W0, e), W1, ?j)}) (trset_of ?x)" apply(unfold stp) by(sep_drule st_upd, simp add: sep_conj_ac) thus "\<exists>k. (r \<and>* ps p \<and>* st e \<and>* zero p \<and>* sg {TC i ((W0, e), W1, ?j)}) (trset_of (tm.run (Suc k) (ft, prog, cs, pc, mem)))" by(auto simp: sep_conj_ac) qed qedqedlemma hoare_if_zero_true_gen[step]: assumes "p = q" shows "\<lbrace>st i ** ps p ** zero q\<rbrace> i:[if_zero e]:j \<lbrace>st e ** ps p ** zero q\<rbrace>" by (unfold assms, rule hoare_if_zero_true)lemma hoare_if_zero_true1: "\<lbrace>st i ** ps p ** zero p\<rbrace> i:[(if_zero e; c)]:j \<lbrace>st e ** ps p ** zero p\<rbrace>" proof(unfold tassemble_to.simps, rule tm.code_exI, simp add: sep_conj_ac tm.Hoare_gen_def, clarify) fix j' ft prog cs pos mem r assume h: "(r \<and>* ps p \<and>* st i \<and>* zero p \<and>* j' :[ c ]: j \<and>* i :[ if_zero e ]: j') (trset_of (ft, prog, cs, pos, mem))" from tm.frame_rule[OF hoare_if_zero_true] have "\<And> r. \<lbrace>st i \<and>* ps p \<and>* zero p \<and>* r\<rbrace> i :[ if_zero e ]: j' \<lbrace>st e \<and>* ps p \<and>* zero p \<and>* r\<rbrace>" by(simp add: sep_conj_ac) from this[unfolded tm.Hoare_gen_def tassemble_to.simps, rule_format, of "j' :[ c ]: j"] h have "\<exists> k. (r \<and>* zero p \<and>* ps p \<and>* st e \<and>* i :[ if_zero e ]: j' \<and>* j' :[ c ]: j) (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" by(auto simp: sep_conj_ac) thus "\<exists>k. (r \<and>* ps p \<and>* st e \<and>* zero p \<and>* j' :[ c ]: j \<and>* i :[ if_zero e ]: j') (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" by(simp add: sep_conj_ac)qedlemma hoare_if_zero_true1_gen[step]: assumes "p = q" shows "\<lbrace>st i ** ps p ** zero q\<rbrace> i:[(if_zero e; c)]:j \<lbrace>st e ** ps p ** zero q\<rbrace>" by (unfold assms, rule hoare_if_zero_true1)lemma hoare_if_zero_false: "\<lbrace>st i ** ps p ** tm p Oc\<rbrace> i:[if_zero e]:j \<lbrace>st j ** ps p ** tm p Oc\<rbrace>"proof(unfold if_zero_def, intro t_hoare_local, rule t_hoare_label_last, simp, simp) fix l show "\<lbrace>st i \<and>* ps p \<and>* tm p Oc\<rbrace> i :[ \<guillemotright> ((W0, e), W1, l) ]: l \<lbrace>st l \<and>* ps p \<and>* tm p Oc\<rbrace>" proof(unfold tassemble_to.simps, simp only:sep_conj_cond, intro tm.code_condI, simp add: sep_conj_ac) let ?j = "Suc i" show "\<lbrace>ps p \<and>* st i \<and>* tm p Oc\<rbrace> sg {TC i ((W0, e), W1, ?j)} \<lbrace>ps p \<and>* st ?j \<and>* tm p Oc\<rbrace>" proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) fix ft prog cs pc mem r assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p Oc \<and>* sg {TC i ((W0, e), W1, ?j)}) (trset_of (ft, prog, cs, pc, mem))" from h have k1: "prog i = Some ((W0, e), W1, ?j)" apply(rule_tac r = "r \<and>* tm p Oc \<and>* ps p" in codeD) by(simp add: sep_conj_ac) from h have k2: "pc = p" by(sep_drule psD, simp) from h and this have k3: "mem pc = Some Oc" by(sep_drule memD, simp) from h k1 k2 k3 have stp: "tm.run 1 (ft, prog, cs, pc, mem) = (ft, prog, ?j, pc, mem)" (is "?x = ?y") apply(sep_drule stD) by(unfold tm.run_def, auto) from h k2 have "(r \<and>* tm p Oc \<and>* ps p \<and>* st ?j \<and>* sg {TC i ((W0, e), W1, ?j)}) (trset_of ?x)" apply(unfold stp) by(sep_drule st_upd, simp add: sep_conj_ac) thus "\<exists>k. (r \<and>* ps p \<and>* st ?j \<and>* tm p Oc \<and>* sg {TC i ((W0, e), W1, ?j)}) (trset_of (tm.run (Suc k) (ft, prog, cs, pc, mem)))" by(auto simp: sep_conj_ac) qed qedqedlemma hoare_if_zero_false_gen[step]: assumes "p = q" shows "\<lbrace>st i ** ps p ** tm q Oc\<rbrace> i:[if_zero e]:j \<lbrace>st j ** ps p ** tm q Oc\<rbrace>" by (unfold assms, rule hoare_if_zero_false)definition "jmp e = \<guillemotright>((W0, e), (W1, e))"lemma hoare_jmp: "\<lbrace>st i \<and>* ps p \<and>* tm p v\<rbrace> i:[jmp e]:j \<lbrace>st e \<and>* ps p \<and>* tm p v\<rbrace>"proof(unfold jmp_def tm.Hoare_gen_def tassemble_to.simps sep_conj_ac, clarify) fix ft prog cs pos mem r assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v \<and>* <(j = i + 1)> \<and>* sg {TC i ((W0, e), W1, e)}) (trset_of (ft, prog, cs, pos, mem))" from h have k1: "prog i = Some ((W0, e), W1, e)" apply(rule_tac r = "r \<and>* <(j = i + 1)> \<and>* tm p v \<and>* ps p" in codeD) by(simp add: sep_conj_ac) from h have k2: "p = pos" by(sep_drule psD, simp) from h k2 have k3: "mem pos = Some v" by(sep_drule memD, simp) from h k1 k2 k3 have stp: "tm.run 1 (ft, prog, cs, pos, mem) = (ft, prog, e, pos, mem)" (is "?x = ?y") apply(sep_drule stD) by(unfold tm.run_def, cases "mem pos", simp, cases v, auto) from h k2 have "(r \<and>* ps p \<and>* st e \<and>* tm p v \<and>* <(j = i + 1)> \<and>* sg {TC i ((W0, e), W1, e)}) (trset_of ?x)" apply(unfold stp) by(sep_drule st_upd, simp add: sep_conj_ac) thus "\<exists> k. (r \<and>* ps p \<and>* st e \<and>* tm p v \<and>* <(j = i + 1)> \<and>* sg {TC i ((W0, e), W1, e)}) (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" apply (rule_tac x = 0 in exI) by autoqedlemma hoare_jmp_gen[step]: assumes "p = q" shows "\<lbrace>st i \<and>* ps p \<and>* tm q v\<rbrace> i:[jmp e]:j \<lbrace>st e \<and>* ps p \<and>* tm q v\<rbrace>" by (unfold assms, rule hoare_jmp)lemma hoare_jmp1: "\<lbrace>st i \<and>* ps p \<and>* tm p v\<rbrace> i:[(jmp e; c)]:j \<lbrace>st e \<and>* ps p \<and>* tm p v\<rbrace>"proof(unfold tassemble_to.simps, rule tm.code_exI, simp add: sep_conj_ac tm.Hoare_gen_def, clarify) fix j' ft prog cs pos mem r assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v \<and>* j' :[ c ]: j \<and>* i :[ jmp e ]: j') (trset_of (ft, prog, cs, pos, mem))" from tm.frame_rule[OF hoare_jmp] have "\<And> r. \<lbrace>st i \<and>* ps p \<and>* tm p v \<and>* r\<rbrace> i :[ jmp e ]: j' \<lbrace>st e \<and>* ps p \<and>* tm p v \<and>* r\<rbrace>" by(simp add: sep_conj_ac) from this[unfolded tm.Hoare_gen_def tassemble_to.simps, rule_format, of "j' :[ c ]: j"] h have "\<exists> k. (r \<and>* tm p v \<and>* ps p \<and>* st e \<and>* i :[ jmp e ]: j' \<and>* j' :[ c ]: j) (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" by(auto simp: sep_conj_ac) thus "\<exists>k. (r \<and>* ps p \<and>* st e \<and>* tm p v \<and>* j' :[ c ]: j \<and>* i :[ jmp e ]: j') (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" by(simp add: sep_conj_ac)qedlemma hoare_jmp1_gen[step]: assumes "p = q" shows "\<lbrace>st i \<and>* ps p \<and>* tm q v\<rbrace> i:[(jmp e; c)]:j \<lbrace>st e \<and>* ps p \<and>* tm q v\<rbrace>" by (unfold assms, rule hoare_jmp1)lemma condI: assumes h1: b and h2: "b \<Longrightarrow> p s" shows "(<b> \<and>* p) s" by (metis (full_types) cond_true_eq1 h1 h2)lemma condE: assumes "(<b> \<and>* p) s" obtains "b" and "p s"proof(atomize_elim) from condD[OF assms] show "b \<and> p s" .qedsection {* Tactics *}ML {* val trace_step = Attrib.setup_config_bool @{binding trace_step} (K false) val trace_fwd = Attrib.setup_config_bool @{binding trace_fwd} (K false)*}ML {* val tracing = (fn ctxt => fn str => if (Config.get ctxt trace_step) then tracing str else ()) fun not_pred p = fn s => not (p s) fun break_sep_conj (Const (@{const_name sep_conj},_) $ t1 $ t2 $ _) = (break_sep_conj t1) @ (break_sep_conj t2) | break_sep_conj (Const (@{const_name sep_conj},_) $ t1 $ t2) = (break_sep_conj t1) @ (break_sep_conj t2) (* dig through eta exanded terms: *) | break_sep_conj (Abs (_, _, t $ Bound 0)) = break_sep_conj t | break_sep_conj t = [t]; val empty_env = (Vartab.empty, Vartab.empty) fun match_env ctxt pat trm env = Pattern.match (ctxt |> Proof_Context.theory_of) (pat, trm) env fun match ctxt pat trm = match_env ctxt pat trm empty_env; val inst = Envir.subst_term; fun term_of_thm thm = thm |> prop_of |> HOLogic.dest_Trueprop fun get_cmd ctxt code = let val pat = term_of @{cpat "_:[(?cmd)]:_"} val pat1 = term_of @{cpat "?cmd::tpg"} val env = match ctxt pat code in inst env pat1 end fun is_seq_term (Const (@{const_name TSeq}, _) $ _ $ _) = true | is_seq_term _ = false fun get_hcmd (Const (@{const_name TSeq}, _) $ hcmd $ _) = hcmd | get_hcmd hcmd = hcmd fun last [a] = a | last (a::b) = last b fun but_last [a] = [] | but_last (a::b) = a::(but_last b) fun foldr f [] = (fn x => x) | foldr f (x :: xs) = (f x) o (foldr f xs) fun concat [] = [] | concat (x :: xs) = x @ concat xs fun match_any ctxt pats tm = fold (fn pat => fn b => (b orelse Pattern.matches (ctxt |> Proof_Context.theory_of) (pat, tm))) pats false fun is_ps_term (Const (@{const_name ps}, _) $ _) = true | is_ps_term _ = false fun string_of_term ctxt t = t |> Syntax.pretty_term ctxt |> Pretty.str_of fun string_of_cterm ctxt ct = ct |> term_of |> string_of_term ctxt fun pterm ctxt t = t |> string_of_term ctxt |> tracing ctxt fun pcterm ctxt ct = ct |> string_of_cterm ctxt |> tracing ctxt fun string_for_term ctxt t = Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) (Syntax.string_of_term ctxt) t |> String.translate (fn c => if Char.isPrint c then str c else "") |> Sledgehammer_Util.simplify_spaces fun string_for_cterm ctxt ct = ct |> term_of |> string_for_term ctxt fun attemp tac = fn i => fn st => (tac i st) handle exn => Seq.empty fun try_tac tac = fn i => fn st => (tac i st) handle exn => (Seq.single st) (* aux end *) *}ML {* (* Functions specific to Hoare triples *) fun get_pre ctxt t = let val pat = term_of @{cpat "\<lbrace>?P\<rbrace> ?c \<lbrace>?Q\<rbrace>"} val env = match ctxt pat t in inst env (term_of @{cpat "?P::tresource set \<Rightarrow> bool"}) end fun can_process ctxt t = ((get_pre ctxt t; true) handle _ => false) fun get_post ctxt t = let val pat = term_of @{cpat "\<lbrace>?P\<rbrace> ?c \<lbrace>?Q\<rbrace>"} val env = match ctxt pat t in inst env (term_of @{cpat "?Q::tresource set \<Rightarrow> bool"}) end; fun get_mid ctxt t = let val pat = term_of @{cpat "\<lbrace>?P\<rbrace> ?c \<lbrace>?Q\<rbrace>"} val env = match ctxt pat t in inst env (term_of @{cpat "?c::tresource set \<Rightarrow> bool"}) end; fun is_pc_term (Const (@{const_name st}, _) $ _) = true | is_pc_term _ = false fun mk_pc_term x = Const (@{const_name st}, @{typ "nat \<Rightarrow> tresource set \<Rightarrow> bool"}) $ Free (x, @{typ "nat"}) val sconj_term = term_of @{cterm "sep_conj::tassert \<Rightarrow> tassert \<Rightarrow> tassert"} fun mk_ps_term x = Const (@{const_name ps}, @{typ "int \<Rightarrow> tresource set \<Rightarrow> bool"}) $ Free (x, @{typ "int"}) fun atomic tac = ((SOLVED' tac) ORELSE' (K all_tac)) fun map_simpset f = Context.proof_map (Simplifier.map_ss f) fun pure_sep_conj_ac_tac ctxt = (auto_tac (map_simpset (fn ss => ss addsimps @{thms sep_conj_ac}) ctxt) |> SELECT_GOAL) fun potential_facts ctxt prop = Facts.could_unify (Proof_Context.facts_of ctxt) ((Term.strip_all_body prop) |> Logic.strip_imp_concl); fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => (Method.insert_tac (potential_facts ctxt goal) i) THEN (pure_sep_conj_ac_tac ctxt i)); fun sep_conj_ac_tac ctxt = (SOLVED' (auto_tac (ctxt |> map_simpset (fn ss => ss addsimps @{thms sep_conj_ac})) |> SELECT_GOAL)) ORELSE' (atomic (some_fact_tac ctxt))*}ML {*type HoareTriple = { binding: binding, can_process: Proof.context -> term -> bool, get_pre: Proof.context -> term -> term, get_mid: Proof.context -> term -> term, get_post: Proof.context -> term -> term, is_pc_term: term -> bool, mk_pc_term: string -> term, sconj_term: term, sep_conj_ac_tac: Proof.context -> int -> tactic, hoare_seq1: thm, hoare_seq2: thm, pre_stren: thm, post_weaken: thm, frame_rule: thm} val tm_triple = {binding = @{binding "tm_triple"}, can_process = can_process, get_pre = get_pre, get_mid = get_mid, get_post = get_post, is_pc_term = is_pc_term, mk_pc_term = mk_pc_term, sconj_term = sconj_term, sep_conj_ac_tac = sep_conj_ac_tac, hoare_seq1 = @{thm t_hoare_seq1}, hoare_seq2 = @{thm t_hoare_seq2}, pre_stren = @{thm tm.pre_stren}, post_weaken = @{thm tm.post_weaken}, frame_rule = @{thm tm.frame_rule} }:HoareTriple*}ML {* val _ = data_slot "HoareTriples" "HoareTriple list" "[]"*}ML {* val _ = HoareTriples_store [tm_triple]*}ML {* (* aux1 functions *)fun focus_params t ctxt = let val (xs, Ts) = split_list (Term.variant_frees t (Term.strip_all_vars t)); (*as they are printed :-*) (* val (xs', ctxt') = variant_fixes xs ctxt; *) (* val ps = xs' ~~ Ts; *) val ps = xs ~~ Ts val (_, ctxt'') = ctxt |> Variable.add_fixes xs in ((xs, ps), ctxt'') endfun focus_concl ctxt t = let val ((xs, ps), ctxt') = focus_params t ctxt val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t); in (t' |> Logic.strip_imp_concl, ctxt') end fun get_concl ctxt (i, state) = nth (Thm.prems_of state) (i - 1) |> focus_concl ctxt |> (fn (x, _) => x |> HOLogic.dest_Trueprop) (* aux1 end *)*}ML {* fun indexing xs = upto (0, length xs - 1) ~~ xs fun select_idxs idxs ps = map_index (fn (i, e) => if (member (op =) idxs i) then [e] else []) ps |> flat fun select_out_idxs idxs ps = map_index (fn (i, e) => if (member (op =) idxs i) then [] else [e]) ps |> flat fun match_pres ctxt mf env ps qs = let fun sel_match mf env [] qs = [(env, [])] | sel_match mf env (p::ps) qs = let val pm = map (fn (i, q) => [(i, let val _ = tracing ctxt "Matching:" val _ = [p, q] |> (pretty_terms ctxt) |> Pretty.str_of |> tracing ctxt val r = mf p q env in r end)] handle _ => ( let val _ = tracing ctxt "Failed matching:" val _ = [p, q] |> (pretty_terms ctxt) |> Pretty.str_of |> tracing ctxt in [] end)) qs |> flat val r = pm |> map (fn (i, env') => let val qs' = filter_out (fn (j, q) => j = i) qs in sel_match mf env' ps qs' |> map (fn (env'', idxs) => (env'', i::idxs)) end) |> flat in r end in sel_match mf env ps (indexing qs) end fun provable tac ctxt goal = let val _ = tracing ctxt "Provable trying to prove:" val _ = [goal] |> (pretty_terms ctxt) |> Pretty.str_of |> tracing ctxt in (Goal.prove ctxt [] [] goal (fn {context, ...} => tac context 1); true) handle exn => false end fun make_sense tac ctxt thm_assms env = thm_assms |> map (inst env) |> forall (provable tac ctxt)*}ML {* fun triple_for ctxt goal = filter (fn trpl => (#can_process trpl) ctxt goal) (HoareTriples.get (Proof_Context.theory_of ctxt)) |> hd fun step_terms_for thm goal ctxt = let val _ = tracing ctxt "This is the new version of step_terms_for!" val _ = tracing ctxt "Tring to find triple processor: TP" val TP = triple_for ctxt goal val _ = #binding TP |> Binding.name_of |> tracing ctxt fun mk_sep_conj tms = foldr (fn tm => fn rtm => ((#sconj_term TP)$tm$rtm)) (but_last tms) (last tms) val thm_concl = thm |> prop_of |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop val thm_assms = thm |> prop_of |> Logic.strip_imp_prems val cmd_pat = thm_concl |> #get_mid TP ctxt |> get_cmd ctxt val cmd = goal |> #get_mid TP ctxt |> get_cmd ctxt val _ = tracing ctxt "matching command ... " val _ = tracing ctxt "cmd_pat = " val _ = pterm ctxt cmd_pat val (hcmd, env1, is_last) = (cmd, match ctxt cmd_pat cmd, true) handle exn => (cmd |> get_hcmd, match ctxt cmd_pat (cmd |> get_hcmd), false) val _ = tracing ctxt "hcmd =" val _ = pterm ctxt hcmd val _ = tracing ctxt "match command succeed! " val _ = tracing ctxt "pres =" val pres = goal |> #get_pre TP ctxt |> break_sep_conj val _ = pres |> (pretty_terms ctxt) |> Pretty.str_of |> tracing ctxt val _ = tracing ctxt "pre_pats =" val pre_pats = thm_concl |> #get_pre TP ctxt |> inst env1 |> break_sep_conj val _ = pre_pats |> (pretty_terms ctxt) |> Pretty.str_of |> tracing ctxt val _ = tracing ctxt "post_pats =" val post_pats = thm_concl |> #get_post TP ctxt |> inst env1 |> break_sep_conj val _ = post_pats |> (pretty_terms ctxt) |> Pretty.str_of |> tracing ctxt val _ = tracing ctxt "Calculating sols" val sols = match_pres ctxt (match_env ctxt) env1 pre_pats pres val _ = tracing ctxt "End calculating sols, sols =" val _ = tracing ctxt (@{make_string} sols) val _ = tracing ctxt "Calulating env2 and idxs" val (env2, idxs) = filter (fn (env, idxs) => make_sense (#sep_conj_ac_tac TP) ctxt thm_assms env) sols |> hd val _ = tracing ctxt "End calculating env2 and idxs" val _ = tracing ctxt "mterms =" val mterms = select_idxs idxs pres |> map (inst env2) val _ = mterms |> (pretty_terms ctxt) |> Pretty.str_of |> tracing ctxt val _ = tracing ctxt "nmterms = " val nmterms = select_out_idxs idxs pres |> map (inst env2) val _ = nmterms |> (pretty_terms ctxt) |> Pretty.str_of |> tracing ctxt val pre_cond = pre_pats |> map (inst env2) |> mk_sep_conj val post_cond = post_pats |> map (inst env2) |> mk_sep_conj val post_cond_npc = post_cond |> break_sep_conj |> filter (not_pred (#is_pc_term TP)) |> (fn x => x @ nmterms) |> mk_sep_conj |> cterm_of (Proof_Context.theory_of ctxt) fun mk_frame cond rest = if rest = [] then cond else ((#sconj_term TP)$ cond) $ (mk_sep_conj rest) val pre_cond_frame = mk_frame pre_cond nmterms |> cterm_of (Proof_Context.theory_of ctxt) fun post_cond_frame j' = post_cond |> break_sep_conj |> filter (not_pred (#is_pc_term TP)) |> (fn x => [#mk_pc_term TP j']@x) |> mk_sep_conj |> (fn x => mk_frame x nmterms) |> cterm_of (Proof_Context.theory_of ctxt) val need_frame = (nmterms <> []) in (post_cond_npc, pre_cond_frame, post_cond_frame, need_frame, is_last) end*}ML {* fun step_tac ctxt thm i state = let val _ = tracing ctxt "This is the new version of step_tac" val (goal, ctxt) = nth (Thm.prems_of state) (i - 1) |> focus_concl ctxt |> (apfst HOLogic.dest_Trueprop) val _ = tracing ctxt "step_tac: goal = " val _ = goal |> pterm ctxt val _ = tracing ctxt "Start to calculate intermediate terms ... " val (post_cond_npc, pre_cond_frame, post_cond_frame, need_frame, is_last) = step_terms_for thm goal ctxt val _ = tracing ctxt "Tring to find triple processor: TP" val TP = triple_for ctxt goal val _ = #binding TP |> Binding.name_of |> tracing ctxt fun mk_sep_conj tms = foldr (fn tm => fn rtm => ((#sconj_term TP)$tm$rtm)) (but_last tms) (last tms) val _ = tracing ctxt "Calculate intermediate terms finished! " val post_cond_npc_str = post_cond_npc |> string_for_cterm ctxt val pre_cond_frame_str = pre_cond_frame |> string_for_cterm ctxt val _ = tracing ctxt "step_tac: post_cond_npc = " val _ = post_cond_npc |> pcterm ctxt val _ = tracing ctxt "step_tac: pre_cond_frame = " val _ = pre_cond_frame |> pcterm ctxt fun tac1 i state = if is_last then (K all_tac) i state else res_inst_tac ctxt [(("q", 0), post_cond_npc_str)] (#hoare_seq1 TP) i state fun tac2 i state = res_inst_tac ctxt [(("p", 0), pre_cond_frame_str)] (#pre_stren TP) i state fun foc_tac post_cond_frame ctxt i state = let val goal = get_concl ctxt (i, state) val pc_term = goal |> #get_post TP ctxt |> break_sep_conj |> filter (#is_pc_term TP) |> hd val (_$Free(j', _)) = pc_term val psd = post_cond_frame j' val str_psd = psd |> string_for_cterm ctxt val _ = tracing ctxt "foc_tac: psd = " val _ = psd |> pcterm ctxt in res_inst_tac ctxt [(("q", 0), str_psd)] (#post_weaken TP) i state end val frame_tac = if need_frame then (rtac (#frame_rule TP)) else (K all_tac) val print_tac = if (Config.get ctxt trace_step) then Tactical.print_tac else (K all_tac) val tac = (tac1 THEN' (K (print_tac "tac1 success"))) THEN' (tac2 THEN' (K (print_tac "tac2 success"))) THEN' ((foc_tac post_cond_frame ctxt) THEN' (K (print_tac "foc_tac success"))) THEN' (frame_tac THEN' (K (print_tac "frame_tac success"))) THEN' (((rtac thm) THEN_ALL_NEW (#sep_conj_ac_tac TP ctxt)) THEN' (K (print_tac "rtac thm success"))) THEN' (K (ALLGOALS (atomic (#sep_conj_ac_tac TP ctxt)))) THEN' (* (#sep_conj_ac_tac TP ctxt) THEN' (#sep_conj_ac_tac TP ctxt) THEN' *) (K prune_params_tac) in tac i state end fun unfold_cell_tac ctxt = (Local_Defs.unfold_tac ctxt @{thms one_def zero_def}) fun fold_cell_tac ctxt = (Local_Defs.fold_tac ctxt @{thms one_def zero_def})*}ML {* fun sg_step_tac thms ctxt = let val sg_step_tac' = (map (fn thm => attemp (step_tac ctxt thm)) thms) (* @ [attemp (goto_tac ctxt)] *) |> FIRST' val sg_step_tac'' = (K (unfold_cell_tac ctxt)) THEN' sg_step_tac' THEN' (K (fold_cell_tac ctxt)) in sg_step_tac' ORELSE' sg_step_tac'' end fun steps_tac thms ctxt i = REPEAT (sg_step_tac thms ctxt i) THEN (prune_params_tac)*}method_setup hstep = {* Attrib.thms >> (fn thms => fn ctxt => (SIMPLE_METHOD' (fn i => sg_step_tac (thms@(StepRules.get ctxt)) ctxt i))) *} "One step symbolic execution using step theorems."method_setup hsteps = {* Attrib.thms >> (fn thms => fn ctxt => (SIMPLE_METHOD' (fn i => steps_tac (thms@(StepRules.get ctxt)) ctxt i))) *} "Sequential symbolic execution using step theorems."ML {* fun goto_tac ctxt thm i state = let val (goal, ctxt) = nth (Thm.prems_of state) (i - 1) |> focus_concl ctxt |> (apfst HOLogic.dest_Trueprop) val _ = tracing ctxt "goto_tac: goal = " val _ = goal |> string_of_term ctxt |> tracing ctxt val (post_cond_npc, pre_cond_frame, post_cond_frame, need_frame, is_last) = step_terms_for thm goal ctxt val _ = tracing ctxt "Tring to find triple processor: TP" val TP = triple_for ctxt goal val _ = #binding TP |> Binding.name_of |> tracing ctxt val _ = tracing ctxt "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" val post_cond_npc_str = post_cond_npc |> string_for_cterm ctxt val pre_cond_frame_str = pre_cond_frame |> string_for_cterm ctxt val _ = tracing ctxt "goto_tac: post_cond_npc = " val _ = post_cond_npc_str |> tracing ctxt val _ = tracing ctxt "goto_tac: pre_cond_frame = " val _ = pre_cond_frame_str |> tracing ctxt fun tac1 i state = if is_last then (K all_tac) i state else res_inst_tac ctxt [] (#hoare_seq2 TP) i state fun tac2 i state = res_inst_tac ctxt [(("p", 0), pre_cond_frame_str)] (#pre_stren TP) i state fun foc_tac post_cond_frame ctxt i state = let val goal = get_concl ctxt (i, state) val pc_term = goal |> #get_post TP ctxt |> break_sep_conj |> filter (#is_pc_term TP) |> hd val (_$Free(j', _)) = pc_term val psd = post_cond_frame j' val str_psd = psd |> string_for_cterm ctxt val _ = tracing ctxt "goto_tac: psd = " val _ = str_psd |> tracing ctxt in res_inst_tac ctxt [(("q", 0), str_psd)] (#post_weaken TP) i state end val frame_tac = if need_frame then (rtac (#frame_rule TP)) else (K all_tac) val _ = tracing ctxt "goto_tac: starting to apply tacs" val print_tac = if (Config.get ctxt trace_step) then Tactical.print_tac else (K all_tac) val tac = (tac1 THEN' (K (print_tac "tac1 success"))) THEN' (tac2 THEN' (K (print_tac "tac2 success"))) THEN' ((foc_tac post_cond_frame ctxt) THEN' (K (print_tac "foc_tac success"))) THEN' (frame_tac THEN' (K (print_tac "frame_tac success"))) THEN' ((((rtac thm) THEN_ALL_NEW (#sep_conj_ac_tac TP ctxt))) THEN' (K (print_tac "rtac success")) ) THEN' (K (ALLGOALS (atomic (#sep_conj_ac_tac TP ctxt)))) THEN' (K prune_params_tac) in tac i state end*}ML {* fun sg_goto_tac thms ctxt = let val sg_goto_tac' = (map (fn thm => attemp (goto_tac ctxt thm)) thms) |> FIRST' val sg_goto_tac'' = (K (unfold_cell_tac ctxt)) THEN' sg_goto_tac' THEN' (K (fold_cell_tac ctxt)) in sg_goto_tac' ORELSE' sg_goto_tac'' end fun gotos_tac thms ctxt i = REPEAT (sg_goto_tac thms ctxt i) THEN (prune_params_tac)*}method_setup hgoto = {* Attrib.thms >> (fn thms => fn ctxt => (SIMPLE_METHOD' (fn i => sg_goto_tac (thms@(StepRules.get ctxt)) ctxt i))) *} "One step symbolic execution using goto theorems."subsection {* Tactic for forward reasoning *}ML {*fun mk_msel_rule ctxt conclusion idx term =let val cjt_count = term |> break_sep_conj |> length fun variants nctxt names = fold_map Name.variant names nctxt; val (state, nctxt0) = Name.variant "s" (Variable.names_of ctxt); fun sep_conj_prop cjts = FunApp.fun_app_free (FunApp.fun_app_foldr SepConj.sep_conj_term cjts) state |> HOLogic.mk_Trueprop; (* concatenate string and string of an int *) fun conc_str_int str int = str ^ Int.toString int; (* make the conjunct names *) val (cjts, _) = ListExtra.range 1 cjt_count |> map (conc_str_int "a") |> variants nctxt0; fun skel_sep_conj names (Const (@{const_name sep_conj}, _) $ t1 $ t2 $ y) = (let val nm1 = take (length (break_sep_conj t1)) names val nm2 = drop (length (break_sep_conj t1)) names val t1' = skel_sep_conj nm1 t1 val t2' = skel_sep_conj nm2 t2 in (SepConj.sep_conj_term $ t1' $ t2' $ y) end) | skel_sep_conj names (Const (@{const_name sep_conj}, _) $ t1 $ t2) = (let val nm1 = take (length (break_sep_conj t1)) names val nm2 = drop (length (break_sep_conj t1)) names val t1' = skel_sep_conj nm1 t1 val t2' = skel_sep_conj nm2 t2 in (SepConj.sep_conj_term $ t1' $ t2') end) | skel_sep_conj names (Abs (x, y, t $ Bound 0)) = let val t' = (skel_sep_conj names t) val ty' = t' |> type_of |> domain_type in (Abs (x, ty', (t' $ Bound 0))) end | skel_sep_conj names t = Free (hd names, SepConj.sep_conj_term |> type_of |> domain_type); val _ = tracing ctxt "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx" val oskel = skel_sep_conj cjts term; val _ = tracing ctxt "yyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyy" val ttt = oskel |> type_of val _ = tracing ctxt "zzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzz" val orig = FunApp.fun_app_free oskel state |> HOLogic.mk_Trueprop val _ = tracing ctxt "uuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuu" val is_selected = member (fn (x, y) => x = y) idx val all_idx = ListExtra.range 0 cjt_count val selected_idx = idx val unselected_idx = filter_out is_selected all_idx val selected = map (nth cjts) selected_idx val unselected = map (nth cjts) unselected_idx fun fun_app_foldr f [a,b] = FunApp.fun_app_free (FunApp.fun_app_free f a) b | fun_app_foldr f [a] = Free (a, SepConj.sep_conj_term |> type_of |> domain_type) | fun_app_foldr f (x::xs) = (FunApp.fun_app_free f x) $ (fun_app_foldr f xs) | fun_app_foldr _ _ = raise Fail "fun_app_foldr"; val reordered_skel = if unselected = [] then (fun_app_foldr SepConj.sep_conj_term selected) else (SepConj.sep_conj_term $ (fun_app_foldr SepConj.sep_conj_term selected) $ (fun_app_foldr SepConj.sep_conj_term unselected)) val reordered = FunApp.fun_app_free reordered_skel state |> HOLogic.mk_Trueprop val goal = Logic.mk_implies (if conclusion then (orig, reordered) else (reordered, orig)); val rule = Goal.prove ctxt [] [] goal (fn _ => auto_tac (ctxt |> map_simpset (fn ss => ss addsimps @{thms sep_conj_ac}))) |> Drule.export_without_contextin ruleend*}lemma fwd_rule: assumes "\<And> s . U s \<longrightarrow> V s" shows "(U ** RR) s \<Longrightarrow> (V ** RR) s" by (metis assms sep_globalise)ML {* fun sg_sg_fwd_tac ctxt thm pos i state = let val tracing = (fn str => if (Config.get ctxt trace_fwd) then Output.tracing str else ()) fun pterm t = t |> string_of_term ctxt |> tracing fun pcterm ct = ct |> string_of_cterm ctxt |> tracing fun atm thm = let (* val thm = thm |> Drule.forall_intr_vars *) val res = thm |> cprop_of |> Object_Logic.atomize val res' = Raw_Simplifier.rewrite_rule [res] thm in res' end fun find_idx ctxt pats terms = let val result = map (fn pat => (find_index (fn trm => ((match ctxt pat trm; true) handle _ => false)) terms)) pats in (assert_all (fn x => x >= 0) result (K "match of precondition failed")); result end val goal = nth (Drule.cprems_of state) (i - 1) |> term_of val _ = tracing "goal = " val _ = goal |> pterm val ctxt_orig = ctxt val ((ps, goal), ctxt) = Variable.focus goal ctxt_orig val prems = goal |> Logic.strip_imp_prems val cprem = nth prems (pos - 1) val (_ $ (the_prem $ _)) = cprem val cjts = the_prem |> break_sep_conj val thm_prems = thm |> cprems_of |> hd |> Thm.dest_arg |> Thm.dest_fun val thm_assms = thm |> cprems_of |> tl |> map term_of val thm_cjts = thm_prems |> term_of |> break_sep_conj val thm_trm = thm |> prop_of val _ = tracing "cjts = " val _ = cjts |> map pterm val _ = tracing "thm_cjts = " val _ = thm_cjts |> map pterm val _ = tracing "Calculating sols" val sols = match_pres ctxt (match_env ctxt) empty_env thm_cjts cjts val _ = tracing "End calculating sols, sols =" val _ = tracing (@{make_string} sols) val _ = tracing "Calulating env2 and idxs" val (env2, idx) = filter (fn (env, idxs) => make_sense sep_conj_ac_tac ctxt thm_assms env) sols |> hd val ([thm'_trm], ctxt') = thm_trm |> inst env2 |> single |> (fn trms => Variable.import_terms true trms ctxt) val thm'_prem = Logic.strip_imp_prems thm'_trm |> hd val thm'_concl = Logic.strip_imp_concl thm'_trm val thm'_prem = (Goal.prove ctxt' [] [thm'_prem] thm'_concl (fn {context, prems = [prem]} => (rtac (prem RS thm) THEN_ALL_NEW (sep_conj_ac_tac ctxt)) 1)) val [thm'] = Variable.export ctxt' ctxt_orig [thm'_prem] val trans_rule = mk_msel_rule ctxt true idx the_prem val _ = tracing "trans_rule = " val _ = trans_rule |> cprop_of |> pcterm val app_rule = if (length cjts = length thm_cjts) then thm' else ((thm' |> atm) RS @{thm fwd_rule}) val _ = tracing "app_rule = " val _ = app_rule |> cprop_of |> pcterm val print_tac = if (Config.get ctxt trace_fwd) then Tactical.print_tac else (K all_tac) val the_tac = (dtac trans_rule THEN' (K (print_tac "dtac1 success"))) THEN' ((dtac app_rule THEN' (K (print_tac "dtac2 success"))))in (the_tac i state) handle _ => no_tac stateend*}ML {* fun sg_fwd_tac ctxt thm i state = let val goal = nth (Drule.cprems_of state) (i - 1) val prems = goal |> term_of |> Term.strip_all_body |> Logic.strip_imp_prems val posx = ListExtra.range 1 (length prems) in ((map (fn pos => attemp (sg_sg_fwd_tac ctxt thm pos)) posx) |> FIRST') i state end fun fwd_tac ctxt thms i state = ((map (fn thm => sg_fwd_tac ctxt thm) thms) |> FIRST') i state*}method_setup fwd = {* Attrib.thms >> (fn thms => fn ctxt => (SIMPLE_METHOD' (fn i => fwd_tac ctxt (thms@(FwdRules.get ctxt)) i))) *} "Forward derivation of separation implication"text {* Testing the fwd tactic *}lemma ones_abs: assumes "(ones u v \<and>* ones w x) s" "w = v + 1" shows "ones u x s" using assms(1) unfolding assms(2)proof(induct u v arbitrary: x s rule:ones_induct) case (Base i j x s) thus ?case by (auto elim!:condE)next case (Step i j x s) hence h: "\<And> x s. (ones (i + 1) j \<and>* ones (j + 1) x) s \<longrightarrow> ones (i + 1) x s" by metis hence "(ones (i + 1) x \<and>* one i) s" by (rule fwd_rule, insert Step(3), auto simp:sep_conj_ac) thus ?case by (smt condD ones.simps sep_conj_commute)qedlemma one_abs: "(one m) s \<Longrightarrow> (ones m m) s" by (smt cond_true_eq2 ones.simps)lemma ones_reps_abs: assumes "ones m n s" "m \<le> n" shows "(reps m n [nat (n - m)]) s" using assms by simplemma reps_reps'_abs: assumes "(reps m n xs \<and>* zero u) s" "u = n + 1" "xs \<noteq> []" shows "(reps' m u xs) s" unfolding assms using assms by (unfold reps'_def, simp)lemma reps'_abs: assumes "(reps' m n xs \<and>* reps' u v ys) s" "u = n + 1" shows "(reps' m v (xs @ ys)) s" apply (unfold reps'_append, rule_tac x = u in EXS_intro) by (insert assms, simp)lemmas abs_ones = one_abs ones_abslemmas abs_reps' = ones_reps_abs reps_reps'_abs reps'_abssection {* Modular TM programming and verification *}definition "right_until_zero = (TL start exit. TLabel start; if_zero exit; move_right; jmp start; TLabel exit )"lemma ones_false [simp]: "j < i - 1 \<Longrightarrow> (ones i j) = sep_false" by (simp add:pasrt_def)lemma hoare_right_until_zero: "\<lbrace>st i ** ps u ** ones u (v - 1) ** zero v \<rbrace> i:[right_until_zero]:j \<lbrace>st j ** ps v ** ones u (v - 1) ** zero v \<rbrace>"proof(unfold right_until_zero_def, intro t_hoare_local t_hoare_label, clarify, rule t_hoare_label_last, simp, simp) fix la let ?body = "i :[ (if_zero la ; move_right ; jmp i) ]: la" let ?j = la show "\<lbrace>st i \<and>* ps u \<and>* ones u (v - 1) \<and>* zero v\<rbrace> ?body \<lbrace>st ?j \<and>* ps v \<and>* ones u (v - 1) \<and>* zero v\<rbrace>" (is "?P u (v - 1) (ones u (v - 1))") proof(induct "u" "v - 1" rule:ones_induct) case (Base k) moreover have "\<lbrace>st i \<and>* ps v \<and>* zero v\<rbrace> ?body \<lbrace>st ?j \<and>* ps v \<and>* zero v\<rbrace>" by hsteps ultimately show ?case by (auto intro!:tm.pre_condI simp:sep_conj_cond) next case (Step k) moreover have "\<lbrace>st i \<and>* ps k \<and>* (one k \<and>* ones (k + 1) (v - 1)) \<and>* zero v\<rbrace> i :[ (if_zero ?j ; move_right ; jmp i) ]: ?j \<lbrace>st ?j \<and>* ps v \<and>* (one k \<and>* ones (k + 1) (v - 1)) \<and>* zero v\<rbrace>" proof - have s1: "\<lbrace>st i \<and>* ps k \<and>* (one k \<and>* ones (k + 1) (v - 1)) \<and>* zero v\<rbrace> ?body \<lbrace>st i \<and>* ps (k + 1) \<and>* one k \<and>* ones (k + 1) (v - 1) \<and>* zero v\<rbrace>" proof(cases "k + 1 \<ge> v") case True with Step(1) have "v = k + 1" by arith thus ?thesis apply(simp add: one_def) by hsteps next case False hence eq_ones: "ones (k + 1) (v - 1) = (one (k + 1) \<and>* ones ((k + 1) + 1) (v - 1))" by simp show ?thesis apply(simp only: eq_ones) by hsteps qed note Step(2)[step] have s2: "\<lbrace>st i \<and>* ps (k + 1) \<and>* one k \<and>* ones (k + 1) (v - 1) \<and>* zero v\<rbrace> ?body \<lbrace>st ?j \<and>* ps v \<and>* one k \<and>* ones (k + 1) (v - 1) \<and>* zero v\<rbrace>" by hsteps from tm.sequencing [OF s1 s2, step] show ?thesis by (auto simp:sep_conj_ac) qed ultimately show ?case by simp qedqedlemma hoare_right_until_zero_gen[step]: assumes "u = v" "w = x - 1" shows "\<lbrace>st i ** ps u ** ones v w ** zero x \<rbrace> i:[right_until_zero]:j \<lbrace>st j ** ps x ** ones v w ** zero x \<rbrace>" by (unfold assms, rule hoare_right_until_zero)definition "left_until_zero = (TL start exit. TLabel start; if_zero exit; move_left; jmp start; TLabel exit )"lemma hoare_left_until_zero: "\<lbrace>st i ** ps v ** zero u ** ones (u + 1) v \<rbrace> i:[left_until_zero]:j \<lbrace>st j ** ps u ** zero u ** ones (u + 1) v \<rbrace>"proof(unfold left_until_zero_def, intro t_hoare_local t_hoare_label, clarify, rule t_hoare_label_last, simp+) fix la let ?body = "i :[ (if_zero la ; move_left ; jmp i) ]: la" let ?j = la show "\<lbrace>st i \<and>* ps v \<and>* zero u \<and>* ones (u + 1) v\<rbrace> ?body \<lbrace>st ?j \<and>* ps u \<and>* zero u \<and>* ones (u + 1) v\<rbrace>" proof(induct "u+1" v rule:ones_rev_induct) case (Base k) thus ?case by (simp add:sep_conj_cond, intro tm.pre_condI, simp, hstep) next case (Step k) have "\<lbrace>st i \<and>* ps k \<and>* zero u \<and>* ones (u + 1) (k - 1) \<and>* one k\<rbrace> ?body \<lbrace>st ?j \<and>* ps u \<and>* zero u \<and>* ones (u + 1) (k - 1) \<and>* one k\<rbrace>" proof(rule tm.sequencing[where q = "st i \<and>* ps (k - 1) \<and>* zero u \<and>* ones (u + 1) (k - 1) \<and>* one k"]) show "\<lbrace>st i \<and>* ps k \<and>* zero u \<and>* ones (u + 1) (k - 1) \<and>* one k\<rbrace> ?body \<lbrace>st i \<and>* ps (k - 1) \<and>* zero u \<and>* ones (u + 1) (k - 1) \<and>* one k\<rbrace>" proof(induct "u + 1" "k - 1" rule:ones_rev_induct) case Base with Step(1) have "k = u + 1" by arith thus ?thesis by (simp, hsteps) next case Step show ?thesis apply (unfold ones_rev[OF Step(1)], simp) apply (unfold one_def) by hsteps qed next note Step(2) [step] show "\<lbrace>st i \<and>* ps (k - 1) \<and>* zero u \<and>* ones (u + 1) (k - 1) \<and>* one k\<rbrace> ?body \<lbrace>st ?j \<and>* ps u \<and>* zero u \<and>* ones (u + 1) (k - 1) \<and>* one k\<rbrace>" by hsteps qed thus ?case by (unfold ones_rev[OF Step(1)], simp) qedqedlemma hoare_left_until_zero_gen[step]: assumes "u = x" "w = v + 1" shows "\<lbrace>st i ** ps u ** zero v ** ones w x \<rbrace> i:[left_until_zero]:j \<lbrace>st j ** ps v ** zero v ** ones w x \<rbrace>" by (unfold assms, rule hoare_left_until_zero)definition "right_until_one = (TL start exit. TLabel start; if_one exit; move_right; jmp start; TLabel exit )"lemma hoare_right_until_one: "\<lbrace>st i ** ps u ** zeros u (v - 1) ** one v \<rbrace> i:[right_until_one]:j \<lbrace>st j ** ps v ** zeros u (v - 1) ** one v \<rbrace>"proof(unfold right_until_one_def, intro t_hoare_local t_hoare_label, clarify, rule t_hoare_label_last, simp+) fix la let ?body = "i :[ (if_one la ; move_right ; jmp i) ]: la" let ?j = la show "\<lbrace>st i \<and>* ps u \<and>* zeros u (v - 1) \<and>* one v\<rbrace> ?body \<lbrace>st ?j \<and>* ps v \<and>* zeros u (v - 1) \<and>* one v\<rbrace>" proof(induct u "v - 1" rule:zeros_induct) case (Base k) thus ?case by (simp add:sep_conj_cond, intro tm.pre_condI, simp, hsteps) next case (Step k) have "\<lbrace>st i \<and>* ps k \<and>* zero k \<and>* zeros (k + 1) (v - 1) \<and>* one v\<rbrace> ?body \<lbrace>st ?j \<and>* ps v \<and>* zero k \<and>* zeros (k + 1) (v - 1) \<and>* one v\<rbrace>" proof(rule tm.sequencing[where q = "st i \<and>* ps (k + 1) \<and>* zero k \<and>* zeros (k + 1) (v - 1) \<and>* one v"]) show "\<lbrace>st i \<and>* ps k \<and>* zero k \<and>* zeros (k + 1) (v - 1) \<and>* one v\<rbrace> ?body \<lbrace>st i \<and>* ps (k + 1) \<and>* zero k \<and>* zeros (k + 1) (v - 1) \<and>* one v\<rbrace>" proof(induct "k + 1" "v - 1" rule:zeros_induct) case Base with Step(1) have eq_v: "k + 1 = v" by arith from Base show ?thesis apply (simp add:sep_conj_cond, intro tm.pre_condI, simp) apply (hstep, clarsimp) by hsteps next case Step thus ?thesis by (simp, hsteps) qed next note Step(2)[step] show "\<lbrace>st i \<and>* ps (k + 1) \<and>* zero k \<and>* zeros (k + 1) (v - 1) \<and>* one v\<rbrace> ?body \<lbrace>st ?j \<and>* ps v \<and>* zero k \<and>* zeros (k + 1) (v - 1) \<and>* one v\<rbrace>" by hsteps qed thus ?case by (auto simp: sep_conj_ac Step(1)) qedqedlemma hoare_right_until_one_gen[step]: assumes "u = v" "w = x - 1" shows "\<lbrace>st i ** ps u ** zeros v w ** one x \<rbrace> i:[right_until_one]:j \<lbrace>st j ** ps x ** zeros v w ** one x \<rbrace>" by (unfold assms, rule hoare_right_until_one)definition "left_until_one = (TL start exit. TLabel start; if_one exit; move_left; jmp start; TLabel exit )"lemma hoare_left_until_one: "\<lbrace>st i ** ps v ** one u ** zeros (u + 1) v \<rbrace> i:[left_until_one]:j \<lbrace>st j ** ps u ** one u ** zeros (u + 1) v \<rbrace>"proof(unfold left_until_one_def, intro t_hoare_local t_hoare_label, clarify, rule t_hoare_label_last, simp+) fix la let ?body = "i :[ (if_one la ; move_left ; jmp i) ]: la" let ?j = la show "\<lbrace>st i \<and>* ps v \<and>* one u \<and>* zeros (u + 1) v\<rbrace> ?body \<lbrace>st ?j \<and>* ps u \<and>* one u \<and>* zeros (u + 1) v\<rbrace>" proof(induct u v rule: ones'.induct) fix ia ja assume h: "\<not> ja < ia \<Longrightarrow> \<lbrace>st i \<and>* ps (ja - 1) \<and>* one ia \<and>* zeros (ia + 1) (ja - 1)\<rbrace> ?body \<lbrace>st ?j \<and>* ps ia \<and>* one ia \<and>* zeros (ia + 1) (ja - 1)\<rbrace>" show "\<lbrace>st i \<and>* ps ja \<and>* one ia \<and>* zeros (ia + 1) ja\<rbrace> ?body \<lbrace>st ?j \<and>* ps ia \<and>* one ia \<and>* zeros (ia + 1) ja\<rbrace>" proof(cases "ja < ia") case False note lt = False from h[OF this] have [step]: "\<lbrace>st i \<and>* ps (ja - 1) \<and>* one ia \<and>* zeros (ia + 1) (ja - 1)\<rbrace> ?body \<lbrace>st ?j \<and>* ps ia \<and>* one ia \<and>* zeros (ia + 1) (ja - 1)\<rbrace>" . show ?thesis proof(cases "ja = ia") case True moreover have "\<lbrace>st i \<and>* ps ja \<and>* one ja\<rbrace> ?body \<lbrace>st ?j \<and>* ps ja \<and>* one ja\<rbrace>" by hsteps ultimately show ?thesis by auto next case False with lt have k1: "ia < ja" by auto from zeros_rev[of "ja" "ia + 1"] this have eq_zeros: "zeros (ia + 1) ja = (zeros (ia + 1) (ja - 1) \<and>* zero ja)" by simp have s1: "\<lbrace>st i \<and>* ps ja \<and>* one ia \<and>* zeros (ia + 1) (ja - 1) \<and>* zero ja\<rbrace> ?body \<lbrace>st i \<and>* ps (ja - 1) \<and>* one ia \<and>* zeros (ia + 1) (ja - 1) \<and>* zero ja\<rbrace>" proof(cases "ia + 1 \<ge> ja") case True from k1 True have "ja = ia + 1" by arith moreover have "\<lbrace>st i \<and>* ps (ia + 1) \<and>* one (ia + 1 - 1) \<and>* zero (ia + 1)\<rbrace> i :[ (if_one ?j ; move_left ; jmp i) ]: ?j \<lbrace>st i \<and>* ps (ia + 1 - 1) \<and>* one (ia + 1 - 1) \<and>* zero (ia + 1)\<rbrace>" by (hsteps) ultimately show ?thesis by (simp) next case False from zeros_rev[of "ja - 1" "ia + 1"] False have k: "zeros (ia + 1) (ja - 1) = (zeros (ia + 1) (ja - 1 - 1) \<and>* zero (ja - 1))" by auto show ?thesis apply (unfold k, simp) by hsteps qed have s2: "\<lbrace>st i \<and>* ps (ja - 1) \<and>* one ia \<and>* zeros (ia + 1) (ja - 1) \<and>* zero ja\<rbrace> ?body \<lbrace>st ?j \<and>* ps ia \<and>* one ia \<and>* zeros (ia + 1) (ja - 1) \<and>* zero ja\<rbrace>" by hsteps from tm.sequencing[OF s1 s2, step] show ?thesis apply (unfold eq_zeros) by hstep qed (* ccc *) next case True thus ?thesis by (auto intro:tm.hoare_sep_false) qed qedqedlemma hoare_left_until_one_gen[step]: assumes "u = x" "w = v + 1" shows "\<lbrace>st i ** ps u ** one v ** zeros w x \<rbrace> i:[left_until_one]:j \<lbrace>st j ** ps v ** one v ** zeros w x \<rbrace>" by (unfold assms, rule hoare_left_until_one)definition "left_until_double_zero = (TL start exit. TLabel start; if_zero exit; left_until_zero; move_left; if_one start; TLabel exit)"declare ones.simps[simp del]lemma reps_simps3: "ks \<noteq> [] \<Longrightarrow> reps i j (k # ks) = (ones i (i + int k) ** zero (i + int k + 1) ** reps (i + int k + 2) j ks)"by(case_tac ks, simp, simp add: reps.simps)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 simpnext case False thus ?thesis by (unfold sep_conj_def set_ins_def pasrt_def, auto)qedlemma reps_rev: "ks \<noteq> [] \<Longrightarrow> reps i j (ks @ [k]) = (reps i (j - int (k + 1) - 1 ) ks \<and>* zero (j - int (k + 1)) \<and>* ones (j - int k) j)"proof(induct ks arbitrary: i j) case Nil thus ?case by simpnext case (Cons a ks) show ?case proof(cases "ks = []") case True thus ?thesis proof - have eq_cond: "(j = i + int a + 2 + int k) = (-2 + (j - int k) = i + int a)" by auto have "(<(-2 + (j - int k) = i + int a)> \<and>* one i \<and>* ones (i + 1) (i + int a) \<and>* zero (i + int a + 1) \<and>* one (i + int a + 2) \<and>* ones (3 + (i + int a)) (i + int a + 2 + int k)) = (<(-2 + (j - int k) = i + int a)> \<and>* one i \<and>* ones (i + 1) (i + int a) \<and>* zero (j - (1 + int k)) \<and>* one (j - int k) \<and>* ones (j - int k + 1) j)" (is "(<?X> \<and>* ?L) = (<?X> \<and>* ?R)") proof(rule cond_eqI) assume h: "-2 + (j - int k) = i + int a" hence eqs: "i + int a + 1 = j - (1 + int k)" "i + int a + 2 = j - int k" "3 + (i + int a) = j - int k + 1" "(i + int a + 2 + int k) = j" by auto show "?L = ?R" by (unfold eqs, auto simp:sep_conj_ac) qed with True show ?thesis apply (simp del:ones_simps reps.simps) apply (simp add:sep_conj_cond eq_cond) by (auto simp:sep_conj_ac) qed next case False from Cons(1)[OF False, of "i + int a + 2" j] this show ?thesis by(simp add: reps_simps3 sep_conj_ac) qedqedlemma hoare_if_one_reps: assumes nn: "ks \<noteq> []" shows "\<lbrace>st i ** ps v ** reps u v ks\<rbrace> i:[if_one e]:j \<lbrace>st e ** ps v ** reps u v ks\<rbrace>"proof(rule rev_exhaust[of ks]) assume "ks = []" with nn show ?thesis by simpnext fix y ys assume eq_ks: "ks = ys @ [y]" show " \<lbrace>st i \<and>* ps v \<and>* reps u v ks\<rbrace> i :[ if_one e ]: j \<lbrace>st e \<and>* ps v \<and>* reps u v ks\<rbrace>" proof(cases "ys = []") case False have "\<lbrace>st i \<and>* ps v \<and>* reps u v (ys @ [y])\<rbrace> i :[ if_one e ]: j \<lbrace>st e \<and>* ps v \<and>* reps u v (ys @ [y])\<rbrace>" apply(unfold reps_rev[OF False], simp del:ones_simps add:ones_rev) by hstep thus ?thesis by (simp add:eq_ks) next case True with eq_ks show ?thesis apply (simp del:ones_simps add:ones_rev sep_conj_cond, intro tm.pre_condI, simp) by hstep qedqedlemma hoare_if_one_reps_gen[step]: assumes nn: "ks \<noteq> []" "u = w" shows "\<lbrace>st i ** ps u ** reps v w ks\<rbrace> i:[if_one e]:j \<lbrace>st e ** ps u ** reps v w ks\<rbrace>" by (unfold `u = w`, rule hoare_if_one_reps[OF `ks \<noteq> []`])lemma hoare_if_zero_ones_false[step]: assumes "\<not> w < u" "v = w" shows "\<lbrace>st i \<and>* ps v \<and>* ones u w\<rbrace> i :[if_zero e]: j \<lbrace>st j \<and>* ps v \<and>* ones u w\<rbrace>" by (unfold `v = w` ones_rev[OF `\<not> w < u`], hstep)lemma hoare_left_until_double_zero_nil[step]: assumes "u = v" shows "\<lbrace>st i ** ps u ** zero v\<rbrace> i:[left_until_double_zero]:j \<lbrace>st j ** ps u ** zero v\<rbrace>" apply (unfold `u = v` left_until_double_zero_def, intro t_hoare_local t_hoare_label, clarsimp, rule t_hoare_label_last, simp+) by (hsteps)lemma hoare_if_zero_reps_false: assumes nn: "ks \<noteq> []" shows "\<lbrace>st i ** ps v ** reps u v ks\<rbrace> i:[if_zero e]:j \<lbrace>st j ** ps v ** reps u v ks\<rbrace>"proof(rule rev_exhaust[of ks]) assume "ks = []" with nn show ?thesis by simpnext fix y ys assume eq_ks: "ks = ys @ [y]" show " \<lbrace>st i \<and>* ps v \<and>* reps u v ks\<rbrace> i :[ if_zero e ]: j \<lbrace>st j \<and>* ps v \<and>* reps u v ks\<rbrace>" proof(cases "ys = []") case False have "\<lbrace>st i \<and>* ps v \<and>* reps u v (ys @ [y])\<rbrace> i :[ if_zero e ]: j \<lbrace>st j \<and>* ps v \<and>* reps u v (ys @ [y])\<rbrace>" apply(unfold reps_rev[OF False], simp del:ones_simps add:ones_rev) by hstep thus ?thesis by (simp add:eq_ks) next case True with eq_ks show ?thesis apply (simp del:ones_simps add:ones_rev sep_conj_cond, intro tm.pre_condI, simp) by hstep qedqedlemma hoare_if_zero_reps_false_gen[step]: assumes "ks \<noteq> []" "u = w" shows "\<lbrace>st i ** ps u ** reps v w ks\<rbrace> i:[if_zero e]:j \<lbrace>st j ** ps u ** reps v w ks\<rbrace>" by (unfold `u = w`, rule hoare_if_zero_reps_false[OF `ks \<noteq> []`])lemma hoare_if_zero_reps_false1: assumes nn: "ks \<noteq> []" shows "\<lbrace>st i ** ps u ** reps u v ks\<rbrace> i:[if_zero e]:j \<lbrace>st j ** ps u ** reps u v ks\<rbrace>"proof - from nn obtain y ys where eq_ys: "ks = y#ys" by (metis neq_Nil_conv) show ?thesis apply (unfold eq_ys) by (case_tac ys, (simp, hsteps)+)qedlemma hoare_if_zero_reps_false1_gen[step]: assumes nn: "ks \<noteq> []" and h: "u = w" shows "\<lbrace>st i ** ps u ** reps w v ks\<rbrace> i:[if_zero e]:j \<lbrace>st j ** ps u ** reps w v ks\<rbrace>" by (unfold h, rule hoare_if_zero_reps_false1[OF `ks \<noteq> []`])lemma hoare_left_until_double_zero: assumes h: "ks \<noteq> []" shows "\<lbrace>st i ** ps v ** zero u ** zero (u + 1) ** reps (u+2) v ks\<rbrace> i:[left_until_double_zero]:j \<lbrace>st j ** ps u ** zero u ** zero (u + 1) ** reps (u+2) v ks\<rbrace>"proof(unfold left_until_double_zero_def, intro t_hoare_local t_hoare_label, clarsimp, rule t_hoare_label_last, simp+) fix la let ?body = "i :[ (if_zero la ; left_until_zero ; move_left ; if_one i) ]: j" let ?j = j show "\<lbrace>st i \<and>* ps v \<and>* zero u \<and>* zero (u + 1) \<and>* reps (u + 2) v ks\<rbrace> ?body \<lbrace>st ?j \<and>* ps u \<and>* zero u \<and>* zero (u + 1) \<and>* reps (u + 2) v ks\<rbrace>" using h proof(induct ks arbitrary: v rule:rev_induct) case Nil with h show ?case by auto next case (snoc k ks) show ?case proof(cases "ks = []") case True have eq_ones: "ones (u + 2) (u + 2 + int k) = (ones (u + 2) (u + 1 + int k) \<and>* one (u + 2 + int k))" by (smt ones_rev) have eq_ones': "(one (u + 2) \<and>* ones (3 + u) (u + 2 + int k)) = (one (u + 2 + int k) \<and>* ones (u + 2) (u + 1 + int k))" by (smt eq_ones ones.simps sep.mult_commute) thus ?thesis apply (insert True, simp del:ones_simps add:sep_conj_cond) apply (rule tm.pre_condI, simp del:ones_simps, unfold eq_ones) apply hsteps apply (rule_tac p = "st j' \<and>* ps (u + 2 + int k) \<and>* zero u \<and>* zero (u + 1) \<and>* ones (u + 2) (u + 2 + int k)" in tm.pre_stren) by (hsteps) next case False from False have spt: "splited (ks @ [k]) ks [k]" by (unfold splited_def, auto) show ?thesis apply (unfold reps_splited[OF spt], simp del:ones_simps add:sep_conj_cond) apply (rule tm.pre_condI, simp del:ones_simps) apply (rule_tac q = "st i \<and>* ps (1 + (u + int (reps_len ks))) \<and>* zero u \<and>* zero (u + 1) \<and>* reps (u + 2) (1 + (u + int (reps_len ks))) ks \<and>* zero (u + 2 + int (reps_len ks)) \<and>* ones (3 + (u + int (reps_len ks))) (3 + (u + int (reps_len ks)) + int k)" in tm.sequencing) apply hsteps[1] by (hstep snoc(1)) qed qedqedlemma hoare_left_until_double_zero_gen[step]: assumes h1: "ks \<noteq> []" and h: "u = y" "w = v + 1" "x = v + 2" shows "\<lbrace>st i ** ps u ** zero v ** zero w ** reps x y ks\<rbrace> i:[left_until_double_zero]:j \<lbrace>st j ** ps v ** zero v ** zero w ** reps x y ks\<rbrace>" by (unfold h, rule hoare_left_until_double_zero[OF h1])lemma hoare_jmp_reps1: assumes "ks \<noteq> []" shows "\<lbrace> st i \<and>* ps u \<and>* reps u v ks\<rbrace> i:[jmp e]:j \<lbrace> st e \<and>* ps u \<and>* reps u v ks\<rbrace>"proof - from assms obtain k ks' where Cons:"ks = k#ks'" by (metis neq_Nil_conv) thus ?thesis proof(cases "ks' = []") case True with Cons show ?thesis apply(simp add:sep_conj_cond reps.simps, intro tm.pre_condI, simp add:ones_simps) by (hgoto hoare_jmp_gen) next case False show ?thesis apply (unfold `ks = k#ks'` reps_simp3[OF False], simp add:ones_simps) by (hgoto hoare_jmp[where p = u]) qedqedlemma hoare_jmp_reps1_gen[step]: assumes "ks \<noteq> []" "u = v" shows "\<lbrace> st i \<and>* ps u \<and>* reps v w ks\<rbrace> i:[jmp e]:j \<lbrace> st e \<and>* ps u \<and>* reps v w ks\<rbrace>" by (unfold assms, rule hoare_jmp_reps1[OF `ks \<noteq> []`])lemma hoare_jmp_reps: "\<lbrace> st i \<and>* ps u \<and>* reps u v ks \<and>* tm (v + 1) x \<rbrace> i:[(jmp e; c)]:j \<lbrace> st e \<and>* ps u \<and>* reps u v ks \<and>* tm (v + 1) x \<rbrace>"proof(cases "ks") case Nil thus ?thesis by (simp add:sep_conj_cond, intro tm.pre_condI, simp, hsteps)next case (Cons k ks') thus ?thesis proof(cases "ks' = []") case True with Cons show ?thesis apply(simp add:sep_conj_cond, intro tm.pre_condI, simp) by (hgoto hoare_jmp[where p = u]) next case False show ?thesis apply (unfold `ks = k#ks'` reps_simp3[OF False], simp) by (hgoto hoare_jmp[where p = u]) qedqeddefinition "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 )"lemma hoare_shift_right_cons: assumes h: "ks \<noteq> []" shows "\<lbrace>st i \<and>* ps u ** reps u v ks \<and>* zero (v + 1) \<and>* zero (v + 2) \<rbrace> i:[shift_right]:j \<lbrace>st j ** ps (v + 2) ** zero u ** reps (u + 1) (v + 1) ks ** zero (v + 2) \<rbrace>"proof(unfold shift_right_def, intro t_hoare_local t_hoare_label, clarify, rule t_hoare_label_last, auto) fix la have eq_ones: "\<And> u k. (one (u + int k + 1) \<and>* ones (u + 1) (u + int k)) = (one (u + 1) \<and>* ones (2 + u) (u + 1 + int k))" by (smt cond_true_eq2 ones.simps ones_rev sep.mult_assoc sep.mult_commute sep.mult_left_commute sep_conj_assoc sep_conj_commute sep_conj_cond1 sep_conj_cond2 sep_conj_cond3 sep_conj_left_commute sep_conj_trivial_strip2) show "\<lbrace>st i \<and>* ps u \<and>* reps u v ks \<and>* zero (v + 1) \<and>* zero (v + 2)\<rbrace> i :[ (if_zero la ; write_zero ; move_right ; right_until_zero ; write_one ; move_right ; jmp i) ]: la \<lbrace>st la \<and>* ps (v + 2) \<and>* zero u \<and>* reps (u + 1) (v + 1) ks \<and>* zero (v + 2)\<rbrace>" using h proof(induct ks arbitrary:i u v) case (Cons k ks) thus ?case proof(cases "ks = []") let ?j = la case True let ?body = "i :[ (if_zero ?j ; write_zero ; move_right ; right_until_zero ; write_one ; move_right ; jmp i) ]: ?j" have first_interation: "\<lbrace>st i \<and>* ps u \<and>* one u \<and>* ones (u + 1) (u + int k) \<and>* zero (u + int k + 1) \<and>* zero (u + int k + 2)\<rbrace> ?body \<lbrace>st i \<and>* ps (u + int k + 2) \<and>* one (u + int k + 1) \<and>* ones (u + 1) (u + int k) \<and>* zero u \<and>* zero (u + int k + 2)\<rbrace>" apply (hsteps) by (simp add:sep_conj_ac, sep_cancel+, smt) hence "\<lbrace>st i \<and>* ps u \<and>* one u \<and>* ones (u + 1) (u + int k) \<and>* zero (u + int k + 1) \<and>* zero (u + int k + 2)\<rbrace> ?body \<lbrace>st ?j \<and>* ps (u + int k + 2) \<and>* zero u \<and>* one (u + 1) \<and>* ones (2 + u) (u + 1 + int k) \<and>* zero (u + int k + 2)\<rbrace>" proof(rule tm.sequencing) show "\<lbrace>st i \<and>* ps (u + int k + 2) \<and>* one (u + int k + 1) \<and>* ones (u + 1) (u + int k) \<and>* zero u \<and>* zero (u + int k + 2)\<rbrace> ?body \<lbrace>st ?j \<and>* ps (u + int k + 2) \<and>* zero u \<and>* one (u + 1) \<and>* ones (2 + u) (u + 1 + int k) \<and>* zero (u + int k + 2)\<rbrace>" apply (hgoto hoare_if_zero_true_gen) by (simp add:sep_conj_ac eq_ones) qed with True show ?thesis by (simp, simp only:sep_conj_cond, intro tm.pre_condI, auto simp:sep_conj_ac) next case False let ?j = la let ?body = "i :[ (if_zero ?j ; write_zero ; move_right ; right_until_zero ; write_one ; move_right ; jmp i) ]: ?j" have eq_ones': "(one (u + int k + 1) \<and>* ones (u + 1) (u + int k) \<and>* zero u \<and>* reps (u + int k + 2) v ks \<and>* zero (v + 1) \<and>* zero (v + 2)) = (zero u \<and>* ones (u + 1) (u + int k) \<and>* one (u + int k + 1) \<and>* reps (u + int k + 2) v ks \<and>* zero (v + 1) \<and>* zero (v + 2))" by (simp add:eq_ones sep_conj_ac) have "\<lbrace>st i \<and>* ps u \<and>* one u \<and>* ones (u + 1) (u + int k) \<and>* zero (u + int k + 1) \<and>* reps (u + int k + 2) v ks \<and>* zero (v + 1) \<and>* zero (v + 2)\<rbrace> ?body \<lbrace>st i \<and>* ps (u + int k + 2) \<and>* zero u \<and>* ones (u + 1) (u + int k) \<and>* one (u + int k + 1) \<and>* reps (u + int k + 2) v ks \<and>* zero (v + 1) \<and>* zero (v + 2)\<rbrace>" apply (hsteps) by (auto simp:sep_conj_ac, sep_cancel+, smt) hence "\<lbrace>st i \<and>* ps u \<and>* one u \<and>* ones (u + 1) (u + int k) \<and>* zero (u + int k + 1) \<and>* reps (u + int k + 2) v ks \<and>* zero (v + 1) \<and>* zero (v + 2)\<rbrace> ?body \<lbrace>st ?j \<and>* ps (v + 2) \<and>* zero u \<and>* one (u + 1) \<and>* ones (2 + u) (u + 1 + int k) \<and>* zero (2 + (u + int k)) \<and>* reps (3 + (u + int k)) (v + 1) ks \<and>* zero (v + 2)\<rbrace>" proof(rule tm.sequencing) have eq_ones': "\<And> u k. (one (u + int k + 1) \<and>* ones (u + 1) (u + int k) \<and>* zero (u + int k + 2)) = (one (u + 1) \<and>* zero (2 + (u + int k)) \<and>* ones (2 + u) (u + 1 + int k))" by (smt eq_ones sep.mult_assoc sep_conj_commute) show "\<lbrace>st i \<and>* ps (u + int k + 2) \<and>* zero u \<and>* ones (u + 1) (u + int k) \<and>* one (u + int k + 1) \<and>* reps (u + int k + 2) v ks \<and>* zero (v + 1) \<and>* zero (v + 2)\<rbrace> ?body \<lbrace>st ?j \<and>* ps (v + 2) \<and>* zero u \<and>* one (u + 1) \<and>* ones (2 + u) (u + 1 + int k) \<and>* zero (2 + (u + int k)) \<and>* reps (3 + (u + int k)) (v + 1) ks \<and>* zero (v + 2)\<rbrace>" apply (hsteps Cons.hyps) by (simp add:sep_conj_ac eq_ones, sep_cancel+, smt) qed thus ?thesis by (unfold reps_simp3[OF False], auto simp:sep_conj_ac) qed qed autoqedlemma hoare_shift_right_cons_gen[step]: assumes h: "ks \<noteq> []" and h1: "u = v" "x = w + 1" "y = w + 2" shows "\<lbrace>st i \<and>* ps u ** reps v w ks \<and>* zero x \<and>* zero y \<rbrace> i:[shift_right]:j \<lbrace>st j ** ps y ** zero v ** reps (v + 1) x ks ** zero y\<rbrace>" by (unfold h1, rule hoare_shift_right_cons[OF h])lemma shift_right_nil [step]: assumes "u = v" shows "\<lbrace> st i \<and>* ps u \<and>* zero v \<rbrace> i:[shift_right]:j \<lbrace> st j \<and>* ps u \<and>* zero v \<rbrace>" by (unfold assms shift_right_def, intro t_hoare_local t_hoare_label, clarify, rule t_hoare_label_last, simp+, hstep)text {* @{text "clear_until_zero"} is useful to implement @{text "drag"}.*}definition "clear_until_zero = (TL start exit. TLabel start; if_zero exit; write_zero; move_right; jmp start; TLabel exit)"lemma hoare_clear_until_zero[step]: "\<lbrace>st i ** ps u ** ones u v ** zero (v + 1)\<rbrace> i :[clear_until_zero]: j \<lbrace>st j ** ps (v + 1) ** zeros u v ** zero (v + 1)\<rbrace> "proof(unfold clear_until_zero_def, intro t_hoare_local, rule t_hoare_label, rule t_hoare_label_last, simp+) let ?body = "i :[ (if_zero j ; write_zero ; move_right ; jmp i) ]: j" show "\<lbrace>st i \<and>* ps u \<and>* ones u v \<and>* zero (v + 1)\<rbrace> ?body \<lbrace>st j \<and>* ps (v + 1) \<and>* zeros u v \<and>* zero (v + 1)\<rbrace>" proof(induct u v rule: zeros.induct) fix ia ja assume h: "\<not> ja < ia \<Longrightarrow> \<lbrace>st i \<and>* ps (ia + 1) \<and>* ones (ia + 1) ja \<and>* zero (ja + 1)\<rbrace> ?body \<lbrace>st j \<and>* ps (ja + 1) \<and>* zeros (ia + 1) ja \<and>* zero (ja + 1)\<rbrace>" show "\<lbrace>st i \<and>* ps ia \<and>* ones ia ja \<and>* zero (ja + 1)\<rbrace> ?body \<lbrace>st j \<and>* ps (ja + 1) \<and>* zeros ia ja \<and>* zero (ja + 1)\<rbrace>" proof(cases "ja < ia") case True thus ?thesis by (simp add: ones.simps zeros.simps sep_conj_ac, simp only:sep_conj_cond, intro tm.pre_condI, simp, hsteps) next case False note h[OF False, step] from False have ones_eq: "ones ia ja = (one ia \<and>* ones (ia + 1) ja)" by(simp add: ones.simps) from False have zeros_eq: "zeros ia ja = (zero ia \<and>* zeros (ia + 1) ja)" by(simp add: zeros.simps) have s1: "\<lbrace>st i \<and>* ps ia \<and>* one ia \<and>* ones (ia + 1) ja \<and>* zero (ja + 1)\<rbrace> ?body \<lbrace>st i \<and>* ps (ia + 1) \<and>* zero ia \<and>* ones (ia + 1) ja \<and>* zero (ja + 1)\<rbrace>" proof(cases "ja < ia + 1") case True from True False have "ja = ia" by auto thus ?thesis apply(simp add: ones.simps) by (hsteps) next case False from False have "ones (ia + 1) ja = (one (ia + 1) \<and>* ones (ia + 1 + 1) ja)" by(simp add: ones.simps) thus ?thesis by (simp, hsteps) qed have s2: "\<lbrace>st i \<and>* ps (ia + 1) \<and>* zero ia \<and>* ones (ia + 1) ja \<and>* zero (ja + 1)\<rbrace> ?body \<lbrace>st j \<and>* ps (ja + 1) \<and>* zero ia \<and>* zeros (ia + 1) ja \<and>* zero (ja + 1)\<rbrace>" by hsteps from tm.sequencing[OF s1 s2] have "\<lbrace>st i \<and>* ps ia \<and>* one ia \<and>* ones (ia + 1) ja \<and>* zero (ja + 1)\<rbrace> ?body \<lbrace>st j \<and>* ps (ja + 1) \<and>* zero ia \<and>* zeros (ia + 1) ja \<and>* zero (ja + 1)\<rbrace>" . thus ?thesis unfolding ones_eq zeros_eq by(simp add: sep_conj_ac) qed qedqedlemma hoare_clear_until_zero_gen[step]: assumes "u = v" "x = w + 1" shows "\<lbrace>st i ** ps u ** ones v w ** zero x\<rbrace> i :[clear_until_zero]: j \<lbrace>st j ** ps x ** zeros v w ** zero x\<rbrace>" by (unfold assms, rule hoare_clear_until_zero)definition "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) "declare ones_simps[simp del]lemma hoare_move_left_reps[step]: assumes "ks \<noteq> []" "u = v" shows "\<lbrace>st i ** ps u ** reps v w ks\<rbrace> i:[move_left]:j \<lbrace>st j ** ps (u - 1) ** reps v w ks\<rbrace>"proof - from `ks \<noteq> []` obtain y ys where eq_ks: "ks = y#ys" by (metis neq_Nil_conv) show ?thesis apply (unfold assms eq_ks) apply (case_tac ys, simp) my_block have "(ones v (v + int y)) = (one v \<and>* ones (v + 1) (v + int y))" by (smt ones_step_simp) my_block_end apply (unfold this, hsteps) by (simp add:this, hsteps)qedlemma hoare_shift_left_cons: assumes h: "ks \<noteq> []" shows "\<lbrace>st i \<and>* ps u \<and>* tm (u - 1) x \<and>* reps u v ks \<and>* zero (v + 1) \<and>* zero (v + 2) \<rbrace> i:[shift_left]:j \<lbrace>st j \<and>* ps (v + 2) \<and>* reps (u - 1) (v - 1) ks \<and>* zero v \<and>* zero (v + 1) \<and>* zero (v + 2) \<rbrace>"proof(unfold shift_left_def, intro t_hoare_local t_hoare_label, clarify, rule t_hoare_label_last, simp+, clarify, prune) show " \<lbrace>st i \<and>* ps u \<and>* tm (u - 1) x \<and>* reps u v ks \<and>* zero (v + 1) \<and>* zero (v + 2)\<rbrace> i :[ (if_zero j ; move_left ; write_one ; right_until_zero ; move_left ; write_zero ; move_right ; move_right ; jmp i) ]: j \<lbrace>st j \<and>* ps (v + 2) \<and>* reps (u - 1) (v - 1) ks \<and>* zero v \<and>* zero (v + 1) \<and>* zero (v + 2)\<rbrace>" using h proof(induct ks arbitrary:i u v x) case (Cons k ks) thus ?case proof(cases "ks = []") let ?body = "i :[ (if_zero j ; move_left ; write_one ; right_until_zero ; move_left ; write_zero ; move_right ; move_right ; jmp i) ]: j" case True have "\<lbrace>st i \<and>* ps u \<and>* tm (u - 1) x \<and>* (one u \<and>* ones (u + 1) (u + int k)) \<and>* zero (u + int k + 1) \<and>* zero (u + int k + 2)\<rbrace> ?body \<lbrace>st j \<and>* ps (u + int k + 2) \<and>* (one (u - 1) \<and>* ones u (u - 1 + int k)) \<and>* zero (u + int k) \<and>* zero (u + int k + 1) \<and>* zero (u + int k + 2)\<rbrace>" apply(rule tm.sequencing [where q = "st i \<and>* ps (u + int k + 2) \<and>* (one (u - 1) \<and>* ones u (u - 1 + int k)) \<and>* zero (u + int k) \<and>* zero (u + int k + 1) \<and>* zero (u + int k + 2)"]) apply (hsteps) apply (rule_tac p = "st j' \<and>* ps (u - 1) \<and>* ones (u - 1) (u + int k) \<and>* zero (u + int k + 1) \<and>* zero (u + int k + 2)" in tm.pre_stren) apply (hsteps) my_block have "(ones (u - 1) (u + int k)) = (ones (u - 1) (u + int k - 1) \<and>* one (u + int k))" by (smt ones_rev) my_block_end apply (unfold this) apply hsteps apply (simp add:sep_conj_ac, sep_cancel+) apply (smt ones.simps sep.mult_assoc sep_conj_commuteI) apply (simp add:sep_conj_ac)+ apply (sep_cancel+) apply (smt ones.simps sep.mult_left_commute sep_conj_commuteI this) by hstep with True show ?thesis by (simp add:ones_simps, simp only:sep_conj_cond, intro tm.pre_condI, simp) next case False let ?body = "i :[ (if_zero j ; move_left ; write_one ;right_until_zero ; move_left ; write_zero ; move_right ; move_right ; jmp i) ]: j" have "\<lbrace>st i \<and>* ps u \<and>* tm (u - 1) x \<and>* one u \<and>* ones (u + 1) (u + int k) \<and>* zero (u + int k + 1) \<and>* reps (u + int k + 2) v ks \<and>* zero (v + 1) \<and>* zero (v + 2)\<rbrace> ?body \<lbrace>st j \<and>* ps (v + 2) \<and>* one (u - 1) \<and>* ones u (u - 1 + int k) \<and>* zero (u + int k) \<and>* reps (1 + (u + int k)) (v - 1) ks \<and>* zero v \<and>* zero (v + 1) \<and>* zero (v + 2)\<rbrace>" apply (rule tm.sequencing[where q = "st i \<and>* ps (u + int k + 2) \<and>* zero (u + int k + 1) \<and>* reps (u + int k + 2) v ks \<and>* zero (v + 1) \<and>* zero (v + 2) \<and>* one (u - 1) \<and>* ones u (u - 1 + int k) \<and>* zero (u + int k)"]) apply (hsteps) apply (rule_tac p = "st j' \<and>* ps (u - 1) \<and>* ones (u - 1) (u + int k) \<and>* zero (u + int k + 1) \<and>* reps (u + int k + 2) v ks \<and>* zero (v + 1) \<and>* zero (v + 2) " in tm.pre_stren) apply hsteps my_block have "(ones (u - 1) (u + int k)) = (ones (u - 1) (u + int k - 1) \<and>* one (u + int k))" by (smt ones_rev) my_block_end apply (unfold this) apply (hsteps) apply (sep_cancel+) apply (smt ones.simps sep.mult_assoc sep_conj_commuteI) apply (sep_cancel+) apply (smt ones.simps this) my_block have eq_u: "1 + (u + int k) = u + int k + 1" by simp from Cons.hyps[OF `ks \<noteq> []`, of i "u + int k + 2" Bk v, folded zero_def] have "\<lbrace>st i \<and>* ps (u + int k + 2) \<and>* zero (u + int k + 1) \<and>* reps (u + int k + 2) v ks \<and>* zero (v + 1) \<and>* zero (v + 2)\<rbrace> ?body \<lbrace>st j \<and>* ps (v + 2) \<and>* reps (1 + (u + int k)) (v - 1) ks \<and>* zero v \<and>* zero (v + 1) \<and>* zero (v + 2)\<rbrace>" by (simp add:eq_u) my_block_end my_note hh[step] = this by hsteps thus ?thesis by (unfold reps_simp3[OF False], auto simp:sep_conj_ac ones_simps) qed qed autoqedlemma hoare_shift_left_cons_gen[step]: assumes h: "ks \<noteq> []" "v = u - 1" "w = u" "y = x + 1" "z = x + 2" shows "\<lbrace>st i \<and>* ps u \<and>* tm v vv \<and>* reps w x ks \<and>* tm y Bk \<and>* tm z Bk\<rbrace> i:[shift_left]:j \<lbrace>st j \<and>* ps z \<and>* reps v (x - 1) ks \<and>* zero x \<and>* zero y \<and>* zero z \<rbrace>" by (unfold assms, fold zero_def, rule hoare_shift_left_cons[OF `ks \<noteq> []`])definition "bone c1 c2 = (TL exit l_one. if_one l_one; (c1; jmp exit); TLabel l_one; c2; TLabel exit )"lemma hoare_bone_1_out: assumes h: "\<And> i j . \<lbrace>st i \<and>* ps u \<and>* zero u \<and>* p \<rbrace> i:[c1]:j \<lbrace>st e \<and>* q \<rbrace> " shows "\<lbrace>st i \<and>* ps u \<and>* zero u \<and>* p \<rbrace> i:[(bone c1 c2)]:j \<lbrace>st e \<and>* q \<rbrace> "apply (unfold bone_def, intro t_hoare_local)apply hstepsapply (subst tassemble_to.simps(2), intro tm.code_exI, rule tm.code_extension)apply (subst tassemble_to.simps(2), intro tm.code_exI, rule tm.code_extension)by (rule h)lemma hoare_bone_1: assumes h: "\<And> i j . \<lbrace>st i \<and>* ps u \<and>* zero u \<and>* p \<rbrace> i:[c1]:j \<lbrace>st j \<and>* ps v \<and>* tm v x \<and>* q \<rbrace> " shows "\<lbrace>st i \<and>* ps u \<and>* zero u \<and>* p \<rbrace> i:[(bone c1 c2)]:j \<lbrace>st j \<and>* ps v \<and>* tm v x \<and>* q \<rbrace> "proof - note h[step] show ?thesis apply (unfold bone_def, intro t_hoare_local) apply (rule t_hoare_label_last, auto) apply hsteps apply (subst tassemble_to.simps(2), intro tm.code_exI, rule tm.code_extension) by hstepsqedlemma hoare_bone_2: assumes h: "\<And> i j . \<lbrace>st i \<and>* ps u \<and>* one u \<and>* p \<rbrace> i:[c2]:j \<lbrace>st j \<and>* q \<rbrace> " shows "\<lbrace>st i \<and>* ps u \<and>* one u \<and>* p \<rbrace> i:[(bone c1 c2)]:j \<lbrace>st j \<and>* q \<rbrace> "apply (unfold bone_def, intro t_hoare_local)apply (rule_tac q = "st la \<and>* ps u \<and>* one u \<and>* p" in tm.sequencing)apply hstepsapply (subst tassemble_to.simps(2), intro tm.code_exI, intro tm.code_extension1)apply (subst tassemble_to.simps(2), intro tm.code_exI, intro tm.code_extension1)apply (subst tassemble_to.simps(2), intro tm.code_exI)apply (subst tassemble_to.simps(4), intro tm.code_condI, simp)apply (subst tassemble_to.simps(2), intro tm.code_exI)apply (subst tassemble_to.simps(4), simp add:sep_conj_cond, rule tm.code_condI, simp)by (rule h)lemma hoare_bone_2_out: assumes h: "\<And> i j . \<lbrace>st i \<and>* ps u \<and>* one u \<and>* p \<rbrace> i:[c2]:j \<lbrace>st e \<and>* q \<rbrace> " shows "\<lbrace>st i \<and>* ps u \<and>* one u \<and>* p \<rbrace> i:[(bone c1 c2)]:j \<lbrace>st e \<and>* q \<rbrace> "apply (unfold bone_def, intro t_hoare_local)apply (rule_tac q = "st la \<and>* ps u \<and>* one u \<and>* p" in tm.sequencing)apply hstepsapply (subst tassemble_to.simps(2), intro tm.code_exI, rule tm.code_extension1)apply (subst tassemble_to.simps(2), intro tm.code_exI, rule tm.code_extension1)apply (subst tassemble_to.simps(2), intro tm.code_exI)apply (subst tassemble_to.simps(4), rule tm.code_condI, simp)apply (subst tassemble_to.simps(2), intro tm.code_exI, rule tm.code_extension)by (rule h)definition "bzero c1 c2 = (TL exit l_zero. if_zero l_zero; (c1; jmp exit); TLabel l_zero; c2; TLabel exit )"lemma hoare_bzero_1: assumes h[step]: "\<And> i j . \<lbrace>st i \<and>* ps u \<and>* one u \<and>* p \<rbrace> i:[c1]:j \<lbrace>st j \<and>* ps v \<and>* tm v x \<and>* q \<rbrace> " shows "\<lbrace>st i \<and>* ps u \<and>* one u \<and>* p \<rbrace> i:[(bzero c1 c2)]:j \<lbrace>st j \<and>* ps v \<and>* tm v x \<and>* q \<rbrace> "apply (unfold bzero_def, intro t_hoare_local)apply hstepsapply (rule_tac c = " ((c1 ; jmp l) ; TLabel la ; c2 ; TLabel l)" in t_hoare_label_last, auto)apply (subst tassemble_to.simps(2), intro tm.code_exI, intro tm.code_extension)by hstepslemma hoare_bzero_1_out: assumes h[step]: "\<And> i j . \<lbrace>st i \<and>* ps u \<and>* one u \<and>* p \<rbrace> i:[c1]:j \<lbrace>st e \<and>* q \<rbrace> " shows "\<lbrace>st i \<and>* ps u \<and>* one u \<and>* p \<rbrace> i:[(bzero c1 c2)]:j \<lbrace>st e \<and>* q \<rbrace> "apply (unfold bzero_def, intro t_hoare_local)apply hstepsapply (subst tassemble_to.simps(2), intro tm.code_exI, rule tm.code_extension)apply (subst tassemble_to.simps(2), intro tm.code_exI, rule tm.code_extension)by (rule h)lemma hoare_bzero_2: assumes h: "\<And> i j. \<lbrace>st i \<and>* ps u \<and>* zero u \<and>* p \<rbrace> i:[c2]:j \<lbrace>st j \<and>* q \<rbrace> " shows "\<lbrace>st i \<and>* ps u \<and>* zero u \<and>* p \<rbrace> i:[(bzero c1 c2)]:j \<lbrace>st j \<and>* q \<rbrace> " apply (unfold bzero_def, intro t_hoare_local) apply (rule_tac q = "st la \<and>* ps u \<and>* zero u \<and>* p" in tm.sequencing) apply hsteps apply (subst tassemble_to.simps(2), intro tm.code_exI, intro tm.code_extension1) apply (subst tassemble_to.simps(2), intro tm.code_exI, intro tm.code_extension1) apply (subst tassemble_to.simps(2), intro tm.code_exI) apply (subst tassemble_to.simps(4)) apply (rule tm.code_condI, simp) apply (subst tassemble_to.simps(2)) apply (rule tm.code_exI) apply (subst tassemble_to.simps(4), simp add:sep_conj_cond) apply (rule tm.code_condI, simp) by (rule h)lemma hoare_bzero_2_out: assumes h: "\<And> i j . \<lbrace>st i \<and>* ps u \<and>* zero u \<and>* p \<rbrace> i:[c2]:j \<lbrace>st e \<and>* q \<rbrace> " shows "\<lbrace>st i \<and>* ps u \<and>* zero u \<and>* p\<rbrace> i:[(bzero c1 c2)]:j \<lbrace>st e \<and>* q \<rbrace> "apply (unfold bzero_def, intro t_hoare_local)apply (rule_tac q = "st la \<and>* ps u \<and>* zero u \<and>* p" in tm.sequencing)apply hstepsapply (subst tassemble_to.simps(2), intro tm.code_exI, rule tm.code_extension1)apply (subst tassemble_to.simps(2), intro tm.code_exI, rule tm.code_extension1)apply (subst tassemble_to.simps(2), intro tm.code_exI)apply (subst tassemble_to.simps(4), rule tm.code_condI, simp)apply (subst tassemble_to.simps(2), intro tm.code_exI, rule tm.code_extension)by (rule h)definition "skip_or_set = bone (write_one; move_right; move_right) (right_until_zero; move_right)"lemma reps_len_split: assumes "xs \<noteq> []" "ys \<noteq> []" shows "reps_len (xs @ ys) = reps_len xs + reps_len ys + 1" using assmsproof(induct xs arbitrary:ys) case (Cons x1 xs1) show ?case proof(cases "xs1 = []") case True thus ?thesis by (simp add:reps_len_cons[OF `ys \<noteq> []`] reps_len_sg) next case False hence " xs1 @ ys \<noteq> []" by simp thus ?thesis apply (simp add:reps_len_cons[OF `xs1@ys \<noteq> []`] reps_len_cons[OF `xs1 \<noteq> []`]) by (simp add: Cons.hyps[OF `xs1 \<noteq> []` `ys \<noteq> []`]) qedqed autolemma hoare_skip_or_set_set: "\<lbrace> st i \<and>* ps u \<and>* zero u \<and>* zero (u + 1) \<and>* tm (u + 2) x\<rbrace> i:[skip_or_set]:j \<lbrace> st j \<and>* ps (u + 2) \<and>* one u \<and>* zero (u + 1) \<and>* tm (u + 2) x\<rbrace>" apply(unfold skip_or_set_def) apply(rule_tac q = "st j \<and>* ps (u + 2) \<and>* tm (u + 2) x \<and>* one u \<and>* zero (u + 1)" in tm.post_weaken) apply(rule hoare_bone_1) apply hsteps by (auto simp:sep_conj_ac, sep_cancel+, smt)lemma hoare_skip_or_set_set_gen[step]: assumes "u = v" "w = v + 1" "x = v + 2" shows "\<lbrace>st i \<and>* ps u \<and>* zero v \<and>* zero w \<and>* tm x xv\<rbrace> i:[skip_or_set]:j \<lbrace>st j \<and>* ps x \<and>* one v \<and>* zero w \<and>* tm x xv\<rbrace>" by (unfold assms, rule hoare_skip_or_set_set)lemma hoare_skip_or_set_skip: "\<lbrace> st i \<and>* ps u \<and>* reps u v [k] \<and>* zero (v + 1)\<rbrace> i:[skip_or_set]:j \<lbrace> st j \<and>* ps (v + 2) \<and>* reps u v [k] \<and>* zero (v + 1)\<rbrace>"proof - show ?thesis apply(unfold skip_or_set_def, unfold reps.simps, simp add:sep_conj_cond) apply(rule tm.pre_condI, simp) apply(rule_tac p = "st i \<and>* ps u \<and>* one u \<and>* ones (u + 1) (u + int k) \<and>* zero (u + int k + 1)" in tm.pre_stren) apply (rule_tac q = "st j \<and>* ps (u + int k + 2) \<and>* one u \<and>* ones (u + 1) (u + int k) \<and>* zero (u + int k + 1) " in tm.post_weaken) apply (rule hoare_bone_2) apply (rule_tac p = " st i \<and>* ps u \<and>* ones u (u + int k) \<and>* zero (u + int k + 1) " in tm.pre_stren) apply hsteps apply (simp add:sep_conj_ac, sep_cancel+, auto simp:sep_conj_ac ones_simps) by (sep_cancel+, smt) qedlemma hoare_skip_or_set_skip_gen[step]: assumes "u = v" "x = w + 1" shows "\<lbrace> st i \<and>* ps u \<and>* reps v w [k] \<and>* zero x\<rbrace> i:[skip_or_set]:j \<lbrace> st j \<and>* ps (w + 2) \<and>* reps v w [k] \<and>* zero x\<rbrace>" by (unfold assms, rule hoare_skip_or_set_skip)definition "if_reps_z e = (move_right; bone (move_left; jmp e) (move_left) )"lemma hoare_if_reps_z_true: assumes h: "k = 0" shows "\<lbrace>st i \<and>* ps u \<and>* reps u v [k] \<and>* zero (v + 1)\<rbrace> i:[if_reps_z e]:j \<lbrace>st e \<and>* ps u \<and>* reps u v [k] \<and>* zero (v + 1)\<rbrace>" apply (unfold reps.simps, simp add:sep_conj_cond) apply (rule tm.pre_condI, simp add:h) apply (unfold if_reps_z_def) apply (simp add:ones_simps) apply (hsteps) apply (rule_tac p = "st j' \<and>* ps (u + 1) \<and>* zero (u + 1) \<and>* one u" in tm.pre_stren) apply (rule hoare_bone_1_out) by (hsteps)lemma hoare_if_reps_z_true_gen[step]: assumes "k = 0" "u = v" "x = w + 1" shows "\<lbrace>st i \<and>* ps u \<and>* reps v w [k] \<and>* zero x\<rbrace> i:[if_reps_z e]:j \<lbrace>st e \<and>* ps u \<and>* reps v w [k] \<and>* zero x\<rbrace>" by (unfold assms, rule hoare_if_reps_z_true, simp)lemma hoare_if_reps_z_false: assumes h: "k \<noteq> 0" shows "\<lbrace>st i \<and>* ps u \<and>* reps u v [k]\<rbrace> i:[if_reps_z e]:j \<lbrace>st j \<and>* ps u \<and>* reps u v [k]\<rbrace>"proof - from h obtain k' where "k = Suc k'" by (metis not0_implies_Suc) show ?thesis apply (unfold `k = Suc k'`) apply (simp add:sep_conj_cond, rule tm.pre_condI, simp) apply (unfold if_reps_z_def) apply (simp add:ones_simps) apply hsteps apply (rule_tac p = "st j' \<and>* ps (u + 1) \<and>* one (u + 1) \<and>* one u \<and>* ones (2 + u) (u + (1 + int k'))" in tm.pre_stren) apply (rule_tac hoare_bone_2) by (hsteps)qedlemma hoare_if_reps_z_false_gen[step]: assumes h: "k \<noteq> 0" "u = v" shows "\<lbrace>st i \<and>* ps u \<and>* reps v w [k]\<rbrace> i:[if_reps_z e]:j \<lbrace>st j \<and>* ps u \<and>* reps v w [k]\<rbrace>" by (unfold assms, rule hoare_if_reps_z_false[OF `k \<noteq> 0`])definition "if_reps_nz e = (move_right; bzero (move_left; jmp e) (move_left) )"lemma EXS_postI: assumes "\<lbrace>P\<rbrace> c \<lbrace>Q x\<rbrace>" shows "\<lbrace>P\<rbrace> c \<lbrace>EXS x. Q x\<rbrace>"by (metis EXS_intro assms tm.hoare_adjust)lemma hoare_if_reps_nz_true: assumes h: "k \<noteq> 0" shows "\<lbrace>st i \<and>* ps u \<and>* reps u v [k]\<rbrace> i:[if_reps_nz e]:j \<lbrace>st e \<and>* ps u \<and>* reps u v [k]\<rbrace>"proof - from h obtain k' where "k = Suc k'" by (metis not0_implies_Suc) show ?thesis apply (unfold `k = Suc k'`) apply (unfold reps.simps, simp add:sep_conj_cond, rule tm.pre_condI, simp) apply (unfold if_reps_nz_def) apply (simp add:ones_simps) apply hsteps apply (rule_tac p = "st j' \<and>* ps (u + 1) \<and>* one (u + 1) \<and>* one u \<and>* ones (2 + u) (u + (1 + int k'))" in tm.pre_stren) apply (rule hoare_bzero_1_out) by hstepsqedlemma hoare_if_reps_nz_true_gen[step]: assumes h: "k \<noteq> 0" "u = v" shows "\<lbrace>st i \<and>* ps u \<and>* reps v w [k]\<rbrace> i:[if_reps_nz e]:j \<lbrace>st e \<and>* ps u \<and>* reps v w [k]\<rbrace>" by (unfold assms, rule hoare_if_reps_nz_true[OF `k\<noteq> 0`])lemma hoare_if_reps_nz_false: assumes h: "k = 0" shows "\<lbrace>st i \<and>* ps u \<and>* reps u v [k] \<and>* zero (v + 1)\<rbrace> i:[if_reps_nz e]:j \<lbrace>st j \<and>* ps u \<and>* reps u v [k] \<and>* zero (v + 1)\<rbrace>" apply (simp add:h sep_conj_cond) apply (rule tm.pre_condI, simp) apply (unfold if_reps_nz_def) apply (simp add:ones_simps) apply (hsteps) apply (rule_tac p = "st j' \<and>* ps (u + 1) \<and>* zero (u + 1) \<and>* one u" in tm.pre_stren) apply (rule hoare_bzero_2) by (hsteps)lemma hoare_if_reps_nz_false_gen[step]: assumes h: "k = 0" "u = v" "x = w + 1" shows "\<lbrace>st i \<and>* ps u \<and>* reps v w [k] \<and>* zero x\<rbrace> i:[if_reps_nz e]:j \<lbrace>st j \<and>* ps u \<and>* reps v w [k] \<and>* zero x\<rbrace>" by (unfold assms, rule hoare_if_reps_nz_false, simp)definition "skip_or_sets n = tpg_fold (replicate n skip_or_set)"lemma hoare_skip_or_sets_set: shows "\<lbrace>st i \<and>* ps u \<and>* zeros u (u + int (reps_len (replicate (Suc n) 0))) \<and>* tm (u + int (reps_len (replicate (Suc n) 0)) + 1) x\<rbrace> i:[skip_or_sets (Suc n)]:j \<lbrace>st j \<and>* ps (u + int (reps_len (replicate (Suc n) 0)) + 1) \<and>* reps' u (u + int (reps_len (replicate (Suc n) 0))) (replicate (Suc n) 0) \<and>* tm (u + int (reps_len (replicate (Suc n) 0)) + 1) x \<rbrace>"proof(induct n arbitrary:i j u x) case 0 from 0 show ?case apply (simp add:reps'_def reps_len_def reps_ctnt_len_def reps_sep_len_def reps.simps) apply (unfold skip_or_sets_def, simp add:tpg_fold_sg) apply hsteps by (auto simp:sep_conj_ac, smt cond_true_eq2 ones.simps sep_conj_left_commute)next case (Suc n) { fix n have "listsum (replicate n (Suc 0)) = n" by (induct n, auto) } note eq_sum = this have eq_len: "\<And>n. n \<noteq> 0 \<Longrightarrow> reps_len (replicate (Suc n) 0) = reps_len (replicate n 0) + 2" by (simp add:reps_len_def reps_sep_len_def reps_ctnt_len_def) have eq_zero: "\<And> u v. (zeros u (u + int (v + 2))) = (zeros u (u + (int v)) \<and>* zero (u + (int v) + 1) \<and>* zero (u + (int v) + 2))" by (smt sep.mult_assoc zeros_rev) hence eq_z: "zeros u (u + int (reps_len (replicate (Suc (Suc n)) 0))) = (zeros u (u + int (reps_len (replicate (Suc n) 0))) \<and>* zero ((u + int (reps_len (replicate (Suc n) 0))) + 1) \<and>* zero ((u + int (reps_len (replicate (Suc n) 0))) + 2)) " by (simp only:eq_len) have hh: "\<And>x. (replicate (Suc (Suc n)) x) = (replicate (Suc n) x) @ [x]" by (metis replicate_Suc replicate_append_same) have hhh: "replicate (Suc n) skip_or_set \<noteq> []" "[skip_or_set] \<noteq> []" by auto have eq_code: "(i :[ skip_or_sets (Suc (Suc n)) ]: j) = (i :[ (skip_or_sets (Suc n); skip_or_set) ]: j)" proof(unfold skip_or_sets_def) show "i :[ tpg_fold (replicate (Suc (Suc n)) skip_or_set) ]: j = i :[ (tpg_fold (replicate (Suc n) skip_or_set) ; skip_or_set) ]: j" apply (insert tpg_fold_app[OF hhh, of i j], unfold hh) by (simp only:tpg_fold_sg) qed have "Suc n \<noteq> 0" by simp show ?case apply (unfold eq_z eq_code) apply (hstep Suc(1)) apply (unfold eq_len[OF `Suc n \<noteq> 0`]) apply hstep apply (auto simp:sep_conj_ac)[1] apply (sep_cancel+, prune) apply (fwd abs_ones) apply ((fwd abs_reps')+, simp add:int_add_ac) by (metis replicate_append_same) qedlemma hoare_skip_or_sets_set_gen[step]: assumes h: "p2 = p1" "p3 = p1 + int (reps_len (replicate (Suc n) 0))" "p4 = p3 + 1" shows "\<lbrace>st i \<and>* ps p1 \<and>* zeros p2 p3 \<and>* tm p4 x\<rbrace> i:[skip_or_sets (Suc n)]:j \<lbrace>st j \<and>* ps p4 \<and>* reps' p2 p3 (replicate (Suc n) 0) \<and>* tm p4 x\<rbrace>" apply (unfold h) by (rule hoare_skip_or_sets_set)declare reps.simps[simp del]lemma hoare_skip_or_sets_skip: assumes h: "n < length ks" shows "\<lbrace>st i \<and>* ps u \<and>* reps' u v (take n ks) \<and>* reps' (v + 1) w [ks!n] \<rbrace> i:[skip_or_sets (Suc n)]:j \<lbrace>st j \<and>* ps (w+1) \<and>* reps' u v (take n ks) \<and>* reps' (v + 1) w [ks!n]\<rbrace>" using hproof(induct n arbitrary: i j u v w ks) case 0 show ?case apply (subst (1 5) reps'_def, simp add:sep_conj_cond, intro tm.pre_condI, simp) apply (unfold skip_or_sets_def, simp add:tpg_fold_sg) apply (unfold reps'_def, simp del:reps.simps) apply hsteps by (sep_cancel+, smt+)next case (Suc n) from `Suc n < length ks` have "n < length ks" by auto note h = Suc(1) [OF this] show ?case my_block from `Suc n < length ks` have eq_take: "take (Suc n) ks = take n ks @ [ks!n]" by (metis not_less_eq not_less_iff_gr_or_eq take_Suc_conv_app_nth) my_block_end apply (unfold this) apply (subst reps'_append, simp add:sep_conj_exists, rule tm.precond_exI) my_block have "(i :[ skip_or_sets (Suc (Suc n)) ]: j) = (i :[ (skip_or_sets (Suc n); skip_or_set )]: j)" proof - have eq_rep: "(replicate (Suc (Suc n)) skip_or_set) = ((replicate (Suc n) skip_or_set) @ [skip_or_set])" by (metis replicate_Suc replicate_append_same) have "replicate (Suc n) skip_or_set \<noteq> []" "[skip_or_set] \<noteq> []" by auto from tpg_fold_app[OF this] show ?thesis by (unfold skip_or_sets_def eq_rep, simp del:replicate.simps add:tpg_fold_sg) qed my_block_end apply (unfold this) my_block fix i j m have "\<lbrace>st i \<and>* ps u \<and>* (reps' u (m - 1) (take n ks) \<and>* reps' m v [ks ! n])\<rbrace> i :[ (skip_or_sets (Suc n)) ]: j \<lbrace>st j \<and>* ps (v + 1) \<and>* (reps' u (m - 1) (take n ks) \<and>* reps' m v [ks ! n])\<rbrace>" apply (rule h[THEN tm.hoare_adjust]) by (sep_cancel+, auto) my_block_end my_note h_c1 = this my_block fix j' j m have "\<lbrace>st j' \<and>* ps (v + 1) \<and>* reps' (v + 1) w [ks ! Suc n]\<rbrace> j' :[ skip_or_set ]: j \<lbrace>st j \<and>* ps (w + 1) \<and>* reps' (v + 1) w [ks ! Suc n]\<rbrace>" apply (unfold reps'_def, simp) apply (rule hoare_skip_or_set_skip[THEN tm.hoare_adjust]) by (sep_cancel+, smt)+ my_block_end apply (hstep h_c1 this)+ by ((fwd abs_reps'), simp, sep_cancel+)qedlemma hoare_skip_or_sets_skip_gen[step]: assumes h: "n < length ks" "u = v" "x = w + 1" shows "\<lbrace>st i \<and>* ps u \<and>* reps' v w (take n ks) \<and>* reps' x y [ks!n] \<rbrace> i:[skip_or_sets (Suc n)]:j \<lbrace>st j \<and>* ps (y+1) \<and>* reps' v w (take n ks) \<and>* reps' x y [ks!n]\<rbrace>" by (unfold assms, rule hoare_skip_or_sets_skip[OF `n < length ks`])lemma fam_conj_interv_simp: "(fam_conj {(ia::int)<..} p) = ((p (ia + 1)) \<and>* fam_conj {ia + 1 <..} p)"by (smt Collect_cong fam_conj_insert_simp greaterThan_def greaterThan_eq_iff greaterThan_iff insertI1 insert_compr lessThan_iff mem_Collect_eq)lemma zeros_fam_conj: assumes "u \<le> v" shows "(zeros u v \<and>* fam_conj {v<..} zero) = fam_conj {u - 1<..} zero"proof - have "{u - 1<..v} ## {v <..}" by (auto simp:set_ins_def) from fam_conj_disj_simp[OF this, symmetric] have "(fam_conj {u - 1<..v} zero \<and>* fam_conj {v<..} zero) = fam_conj ({u - 1<..v} + {v<..}) zero" . moreover from `u \<le> v` have eq_set: "{u - 1 <..} = {u - 1 <..v} + {v <..}" by (auto simp:set_ins_def) moreover have "fam_conj {u - 1<..v} zero = zeros u v" proof - have "({u - 1<..v}) = ({u .. v})" by auto moreover { fix u v assume "u \<le> (v::int)" hence "fam_conj {u .. v} zero = zeros u v" proof(induct rule:ones_induct) case (Base i j) thus ?case by auto next case (Step i j) thus ?case proof(cases "i = j") case True show ?thesis by (unfold True, simp add:fam_conj_simps) next case False with `i \<le> j` have hh: "i + 1 \<le> j" by auto hence eq_set: "{i..j} = (insert i {i + 1 .. j})" by (smt simp_from_to) have "i \<notin> {i + 1 .. j}" by simp from fam_conj_insert_simp[OF this, folded eq_set] have "fam_conj {i..j} zero = (zero i \<and>* fam_conj {i + 1..j} zero)" . with Step(2)[OF hh] Step show ?thesis by simp qed qed } moreover note this[OF `u \<le> v`] ultimately show ?thesis by simp qed ultimately show ?thesis by smtqeddeclare replicate.simps [simp del]lemma hoare_skip_or_sets_comb: assumes "length ks \<le> n" shows "\<lbrace>st i \<and>* ps u \<and>* reps u v ks \<and>* fam_conj {v<..} zero\<rbrace> i:[skip_or_sets (Suc n)]:j \<lbrace>st j \<and>* ps ((v + int (reps_len (list_ext n ks)) - int (reps_len ks))+ 2) \<and>* reps' u (v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1) (list_ext n ks) \<and>* fam_conj {(v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1)<..} zero \<rbrace>"proof(cases "ks = []") case True show ?thesis apply (subst True, simp only:reps.simps sep_conj_cond) apply (rule tm.pre_condI, simp) apply (rule_tac p = "st i \<and>* ps (v + 1) \<and>* zeros (v + 1) (v + 1 + int (reps_len (replicate (Suc n) 0))) \<and>* tm (v + 2 + int (reps_len (replicate (Suc n) 0))) Bk \<and>* fam_conj {(v + 2 + int (reps_len (replicate (Suc n) 0)))<..} zero " in tm.pre_stren) apply hsteps apply (auto simp:sep_conj_ac)[1] apply (auto simp:sep_conj_ac)[2] my_block from True have "(list_ext n ks) = (replicate (Suc n) 0)" by (metis append_Nil diff_zero list.size(3) list_ext_def) my_block_end my_note le_red = this my_block from True have "(reps_len ks) = 0" by (metis reps_len_nil) my_block_end apply (unfold this le_red, simp) my_block have "v + 2 + int (reps_len (replicate (Suc n) 0)) = v + int (reps_len (replicate (Suc n) 0)) + 2" by smt my_block_end my_note eq_len = this apply (unfold this) apply (sep_cancel+) apply (fold zero_def) apply (subst fam_conj_interv_simp, simp) apply (simp only:int_add_ac) apply (simp only:sep_conj_ac, sep_cancel+) my_block have "v + 1 \<le> (2 + (v + int (reps_len (replicate (Suc n) 0))))" by simp from zeros_fam_conj[OF this] have "(fam_conj {v<..} zero) = (zeros (v + 1) (2 + (v + int (reps_len (replicate (Suc n) 0)))) \<and>* fam_conj {2 + (v + int (reps_len (replicate (Suc n) 0)))<..} zero)" by simp my_block_end apply (subst (asm) this, simp only:int_add_ac, sep_cancel+) by (smt cond_true_eq2 sep.mult_assoc sep.mult_commute sep.mult_left_commute sep_conj_assoc sep_conj_commute sep_conj_left_commute zeros.simps zeros_rev)next case False show ?thesis my_block have "(i:[skip_or_sets (Suc n)]:j) = (i:[(skip_or_sets (length ks); skip_or_sets (Suc n - length ks))]:j)" apply (unfold skip_or_sets_def) my_block have "(replicate (Suc n) skip_or_set) = (replicate (length ks) skip_or_set @ (replicate (Suc n - length ks) skip_or_set))" by (smt assms replicate_add) my_block_end apply (unfold this, rule tpg_fold_app, simp add:False) by (insert `length ks \<le> n`, simp) my_block_end apply (unfold this) my_block from False have "length ks = (Suc (length ks - 1))" by simp my_block_end apply (subst (1) this) my_block from False have "(reps u v ks \<and>* fam_conj {v<..} zero) = (reps' u (v + 1) ks \<and>* fam_conj {v+1<..} zero)" apply (unfold reps'_def, simp) by (subst fam_conj_interv_simp, simp add:sep_conj_ac) my_block_end apply (unfold this) my_block fix i j have "\<lbrace>st i \<and>* ps u \<and>* reps' u (v + 1) ks \<rbrace> i :[ skip_or_sets (Suc (length ks - 1))]: j \<lbrace>st j \<and>* ps (v + 2) \<and>* reps' u (v + 1) ks \<rbrace>" my_block have "ks = take (length ks - 1) ks @ [ks!(length ks - 1)]" by (smt False drop_0 drop_eq_Nil id_take_nth_drop) my_block_end my_note eq_ks = this apply (subst (1) this) apply (unfold reps'_append, simp add:sep_conj_exists, rule tm.precond_exI) my_block from False have "(length ks - Suc 0) < length ks" by (smt `length ks = Suc (length ks - 1)`) my_block_end apply hsteps apply (subst eq_ks, unfold reps'_append, simp only:sep_conj_exists) by (rule_tac x = m in EXS_intro, simp add:sep_conj_ac, sep_cancel+, smt) my_block_end apply (hstep this) my_block fix u n have "(fam_conj {u <..} zero) = (zeros (u + 1) (u + int n + 1) \<and>* tm (u + int n + 2) Bk \<and>* fam_conj {(u + int n + 2)<..} zero)" my_block have "u + 1 \<le> (u + int n + 2)" by auto from zeros_fam_conj[OF this, symmetric] have "fam_conj {u<..} zero = (zeros (u + 1) (u + int n + 2) \<and>* fam_conj {u + int n + 2<..} zero)" by simp my_block_end apply (subst this) my_block have "(zeros (u + 1) (u + int n + 2)) = ((zeros (u + 1) (u + int n + 1) \<and>* tm (u + int n + 2) Bk))" by (smt zero_def zeros_rev) my_block_end by (unfold this, auto simp:sep_conj_ac) my_block_end apply (subst (1) this[of _ "(reps_len (replicate (Suc (n - length ks)) 0))"]) my_block from `length ks \<le> n` have "Suc n - length ks = Suc (n - length ks)" by auto my_block_end my_note eq_suc = this apply (subst this) apply hsteps apply (simp add: sep_conj_ac this, sep_cancel+) apply (fwd abs_reps')+ my_block have "(int (reps_len (replicate (Suc (n - length ks)) 0))) = (int (reps_len (list_ext n ks)) - int (reps_len ks) - 1)" apply (unfold list_ext_def eq_suc) my_block have "replicate (Suc (n - length ks)) 0 \<noteq> []" by simp my_block_end by (unfold reps_len_split[OF False this], simp) my_block_end apply (unfold this) my_block from `length ks \<le> n` have "(ks @ replicate (Suc (n - length ks)) 0) = (list_ext n ks)" by (unfold list_ext_def, simp) my_block_end apply (unfold this, simp) apply (subst fam_conj_interv_simp, unfold zero_def, simp, simp add:int_add_ac sep_conj_ac) by (sep_cancel+, smt)qedlemma hoare_skip_or_sets_comb_gen: assumes "length ks \<le> n" "u = v" "w = x" shows "\<lbrace>st i \<and>* ps u \<and>* reps v w ks \<and>* fam_conj {x<..} zero\<rbrace> i:[skip_or_sets (Suc n)]:j \<lbrace>st j \<and>* ps ((x + int (reps_len (list_ext n ks)) - int (reps_len ks))+ 2) \<and>* reps' u (x + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1) (list_ext n ks) \<and>* fam_conj {(x + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1)<..} zero \<rbrace>" by (unfold assms, rule hoare_skip_or_sets_comb[OF `length ks \<le> n`])definition "locate n = (skip_or_sets (Suc n); move_left; move_left; left_until_zero; move_right )"lemma list_ext_tail_expand: assumes h: "length ks \<le> a" shows "list_ext a ks = take a (list_ext a ks) @ [(list_ext a ks)!a]"proof - let ?l = "list_ext a ks" from h have eq_len: "length ?l = Suc a" by (smt list_ext_len_eq) hence "?l \<noteq> []" by auto hence "?l = take (length ?l - 1) ?l @ [?l!(length ?l - 1)]" by (metis `length (list_ext a ks) = Suc a` diff_Suc_1 le_refl lessI take_Suc_conv_app_nth take_all) from this[unfolded eq_len] show ?thesis by simpqedlemma reps'_nn_expand: assumes "xs \<noteq> []" shows "(reps' u v xs) = (reps u (v - 1) xs \<and>* zero v)" by (metis assms reps'_def)lemma sep_conj_st1: "(p \<and>* st t \<and>* q) = (st t \<and>* p \<and>* q)" by (simp only:sep_conj_ac)lemma sep_conj_st2: "(p \<and>* st t) = (st t \<and>* p)" by (simp only:sep_conj_ac)lemma sep_conj_st3: "((st t \<and>* p) \<and>* r) = (st t \<and>* p \<and>* r)" by (simp only:sep_conj_ac)lemma sep_conj_st4: "(EXS x. (st t \<and>* r x)) = ((st t) \<and>* (EXS x. r x))" apply (unfold pred_ex_def, default+) apply (safe) apply (sep_cancel, auto) by (auto elim!: sep_conjE intro!:sep_conjI)lemmas sep_conj_st = sep_conj_st1 sep_conj_st2 sep_conj_st3 sep_conj_st4lemma sep_conj_cond3 : "(<cond1> \<and>* <cond2>) = <(cond1 \<and> cond2)>" by (smt cond_eqI cond_true_eq sep_conj_commute sep_conj_empty)lemma sep_conj_cond4 : "(<cond1> \<and>* <cond2> \<and>* r) = (<(cond1 \<and> cond2)> \<and>* r)" by (metis Hoare_gen.sep_conj_cond3 Hoare_tm.sep_conj_cond3)lemmas sep_conj_cond = sep_conj_cond3 sep_conj_cond4 sep_conj_cond lemma hoare_left_until_zero_reps: "\<lbrace>st i ** ps v ** zero u ** reps (u + 1) v [k]\<rbrace> i:[left_until_zero]:j \<lbrace>st j ** ps u ** zero u ** reps (u + 1) v [k]\<rbrace>" apply (unfold reps.simps, simp only:sep_conj_cond) apply (rule tm.pre_condI, simp) by hsteplemma hoare_left_until_zero_reps_gen[step]: assumes "u = x" "w = v + 1" shows "\<lbrace>st i ** ps u ** zero v ** reps w x [k]\<rbrace> i:[left_until_zero]:j \<lbrace>st j ** ps v ** zero v ** reps w x [k]\<rbrace>" by (unfold assms, rule hoare_left_until_zero_reps)lemma reps_lenE: assumes "reps u v ks s" shows "( <(v = u + int (reps_len ks) - 1)> \<and>* reps u v ks ) s"proof(rule condI) from reps_len_correct[OF assms] show "v = u + int (reps_len ks) - 1" .next from assms show "reps u v ks s" .qedlemma condI1: assumes "p s" "b" shows "(<b> \<and>* p) s"proof(rule condI[OF assms(2)]) from assms(1) show "p s" .qedlemma hoare_locate_set: assumes "length ks \<le> n" shows "\<lbrace>st i \<and>* zero (u - 1) \<and>* ps u \<and>* reps u v ks \<and>* fam_conj {v<..} zero\<rbrace> i:[locate n]:j \<lbrace>st j \<and>* zero (u - 1) \<and>* (EXS m w. ps m \<and>* reps' u (m - 1) (take n (list_ext n ks)) \<and>* reps m w [(list_ext n ks)!n] \<and>* fam_conj {w<..} zero)\<rbrace>"proof(cases "take n (list_ext n ks) = []") case False show ?thesis apply (unfold locate_def) apply (hstep hoare_skip_or_sets_comb_gen) apply (subst (3) list_ext_tail_expand[OF `length ks \<le> n`]) apply (subst (1) reps'_append, simp add:sep_conj_exists) apply (rule tm.precond_exI) apply (subst (1) reps'_nn_expand[OF False]) apply (rule_tac p = "st j' \<and>* <(m = u + int (reps_len (take n (list_ext n ks))) + 1)> \<and>* ps (v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 2) \<and>* ((reps u (m - 1 - 1) (take n (list_ext n ks)) \<and>* zero (m - 1)) \<and>* reps' m (v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1) [list_ext n ks ! n]) \<and>* fam_conj {v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1<..} zero \<and>* zero (u - 1)" in tm.pre_stren) my_block have "[list_ext n ks ! n] \<noteq> []" by simp from reps'_nn_expand[OF this] have "(reps' m (v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1) [list_ext n ks ! n]) = (reps m (v + (int (reps_len (list_ext n ks)) - int (reps_len ks))) [list_ext n ks ! n] \<and>* zero (v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1))" by simp my_block_end apply (subst this) my_block have "(fam_conj {v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1<..} zero) = (zero (v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 2) \<and>* fam_conj {v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 2<..} zero)" by (subst fam_conj_interv_simp, smt) my_block_end apply (unfold this) apply (simp only:sep_conj_st) apply hsteps apply (auto simp:sep_conj_ac)[1] apply (sep_cancel+) apply (rule_tac x = m in EXS_intro) apply (rule_tac x = "m + int (list_ext n ks ! n)" in EXS_intro) apply (simp add:sep_conj_ac del:ones_simps, sep_cancel+) apply (subst (asm) sep_conj_cond)+ apply (erule_tac condE, clarsimp, simp add:sep_conj_ac int_add_ac) apply (fwd abs_reps') apply (fwd abs_reps') apply (simp add:sep_conj_ac int_add_ac) apply (sep_cancel+) apply (subst (asm) reps'_def, subst fam_conj_interv_simp, subst fam_conj_interv_simp, simp add:sep_conj_ac int_add_ac) my_block fix s assume h: "(reps (1 + (u + int (reps_len (take n (list_ext n ks))))) (v + (- int (reps_len ks) + int (reps_len (list_ext n ks)))) [list_ext n ks ! n]) s" (is "?P s") from reps_len_correct[OF this] list_ext_tail_expand[OF `length ks \<le> n`] have hh: "v + (- int (reps_len ks) + int (reps_len (take n (list_ext n ks) @ [list_ext n ks ! n]))) = 1 + (u + int (reps_len (take n (list_ext n ks)))) + int (reps_len [list_ext n ks ! n]) - 1" by metis have "[list_ext n ks ! n] \<noteq> []" by simp from hh[unfolded reps_len_split[OF False this]] have "v = u + (int (reps_len ks)) - 1" by simp from condI1[where p = ?P, OF h this] have "(<(v = u + int (reps_len ks) - 1)> \<and>* reps (1 + (u + int (reps_len (take n (list_ext n ks))))) (v + (- int (reps_len ks) + int (reps_len (list_ext n ks)))) [list_ext n ks ! n]) s" . my_block_end apply (fwd this, (subst (asm) sep_conj_cond)+, erule condE, simp add:sep_conj_ac int_add_ac reps_len_sg) apply (fwd reps_lenE, (subst (asm) sep_conj_cond)+, erule condE, simp add:sep_conj_ac int_add_ac reps_len_sg) by (fwd reps_lenE, (subst (asm) sep_conj_cond)+, erule condE, simp add:sep_conj_ac)next case True show ?thesis apply (unfold locate_def) apply (hstep hoare_skip_or_sets_comb) apply (subst (3) list_ext_tail_expand[OF `length ks \<le> n`]) apply (subst (1) reps'_append, simp add:sep_conj_exists) apply (rule tm.precond_exI) my_block from True `length ks \<le> n` have "ks = []" "n = 0" apply (metis le0 le_antisym length_0_conv less_nat_zero_code list_ext_len take_eq_Nil) by (smt True length_take list.size(3) list_ext_len) my_block_end apply (unfold True this) apply (simp add:reps'_def list_ext_def reps.simps reps_len_def reps_sep_len_def reps_ctnt_len_def del:ones_simps) apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, simp del:ones_simps) apply (subst fam_conj_interv_simp, simp add:sep_conj_st del:ones_simps) apply (hsteps) apply (auto simp:sep_conj_ac)[1] apply (sep_cancel+) apply (rule_tac x = "(v + int (listsum (replicate (Suc 0) (Suc 0))))" in EXS_intro)+ apply (simp only:sep_conj_ac, sep_cancel+) apply (auto) apply (subst fam_conj_interv_simp) apply (subst fam_conj_interv_simp) by smtqedlemma hoare_locate_set_gen[step]: assumes "length ks \<le> n" "u = v - 1" "v = w" "x = y" shows "\<lbrace>st i \<and>* zero u \<and>* ps v \<and>* reps w x ks \<and>* fam_conj {y<..} zero\<rbrace> i:[locate n]:j \<lbrace>st j \<and>* zero u \<and>* (EXS m w. ps m \<and>* reps' v (m - 1) (take n (list_ext n ks)) \<and>* reps m w [(list_ext n ks)!n] \<and>* fam_conj {w<..} zero)\<rbrace>" by (unfold assms, rule hoare_locate_set[OF `length ks \<le> n`])lemma hoare_locate_skip: assumes h: "n < length ks" shows "\<lbrace>st i \<and>* ps u \<and>* zero (u - 1) \<and>* reps' u (v - 1) (take n ks) \<and>* reps' v w [ks!n] \<and>* tm (w + 1) x\<rbrace> i:[locate n]:j \<lbrace>st j \<and>* ps v \<and>* zero (u - 1) \<and>* reps' u (v - 1) (take n ks) \<and>* reps' v w [ks!n] \<and>* tm (w + 1) x\<rbrace>"proof - show ?thesis apply (unfold locate_def) apply hsteps apply (subst (2 4) reps'_def, simp add:reps.simps sep_conj_cond del:ones_simps) apply (intro tm.pre_condI, simp del:ones_simps) apply hsteps apply (case_tac "(take n ks) = []", simp add:reps'_def sep_conj_cond del:ones_simps) apply (rule tm.pre_condI, simp del:ones_simps) apply hsteps apply (simp del:ones_simps add:reps'_def) by hstepsqedlemma hoare_locate_skip_gen[step]: assumes "n < length ks" "v = u - 1" "w = u" "x = y - 1" "z' = z + 1" shows "\<lbrace>st i \<and>* ps u \<and>* tm v Bk \<and>* reps' w x (take n ks) \<and>* reps' y z [ks!n] \<and>* tm z' vx\<rbrace> i:[locate n]:j \<lbrace>st j \<and>* ps y \<and>* tm v Bk \<and>* reps' w x (take n ks) \<and>* reps' y z [ks!n] \<and>* tm z' vx\<rbrace>" by (unfold assms, fold zero_def, rule hoare_locate_skip[OF `n < length ks`])definition "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 "lemma ones_int_expand: "(ones m (m + int k)) = (one m \<and>* ones (m + 1) (m + int k))" by (simp add:ones_simps)lemma reps_splitedI: assumes h1: "(reps u v ks1 \<and>* zero (v + 1) \<and>* reps (v + 2) w ks2) s" and h2: "ks1 \<noteq> []" and h3: "ks2 \<noteq> []" shows "(reps u w (ks1 @ ks2)) s"proof - from h2 h3 have "splited (ks1 @ ks2) ks1 ks2" by (auto simp:splited_def) from h1 obtain s1 where "(reps u v ks1) s1" by (auto elim:sep_conjE) from h1 obtain s2 where "(reps (v + 2) w ks2) s2" by (auto elim:sep_conjE) from reps_len_correct[OF `(reps u v ks1) s1`] have eq_v: "v = u + int (reps_len ks1) - 1" . from reps_len_correct[OF `(reps (v + 2) w ks2) s2`] have eq_w: "w = v + 2 + int (reps_len ks2) - 1" . from h1 have "(reps u (u + int (reps_len ks1) - 1) ks1 \<and>* zero (u + int (reps_len ks1)) \<and>* reps (u + int (reps_len ks1) + 1) w ks2) s" apply (unfold eq_v eq_w[unfolded eq_v]) by (sep_cancel+, smt) thus ?thesis by(unfold reps_splited[OF `splited (ks1 @ ks2) ks1 ks2`], simp)qedlemma reps_sucI: assumes h: "(reps u v (xs@[x]) \<and>* one (1 + v)) s" shows "(reps u (1 + v) (xs@[Suc x])) s"proof(cases "xs = []") case True from h obtain s' where "(reps u v (xs@[x])) s'" by (auto elim:sep_conjE) from reps_len_correct[OF this] have " v = u + int (reps_len (xs @ [x])) - 1" . with True have eq_v: "v = u + int x" by (simp add:reps_len_sg) have eq_one1: "(one (1 + (u + int x)) \<and>* ones (u + 1) (u + int x)) = ones (u + 1) (1 + (u + int x))" by (smt ones_rev sep.mult_commute) from h show ?thesis apply (unfold True, simp add:eq_v reps.simps sep_conj_cond sep_conj_ac ones_rev) by (sep_cancel+, simp add: eq_one1, smt)next case False from h obtain s1 s2 where hh: "(reps u v (xs@[x])) s1" "s = s1 + s2" "s1 ## s2" "one (1 + v) s2" by (auto elim:sep_conjE) from hh(1)[unfolded reps_rev[OF False]] obtain s11 s12 s13 where hhh: "(reps u (v - int (x + 1) - 1) xs) s11" "(zero (v - int (x + 1))) s12" "(ones (v - int x) v) s13" "s11 ## (s12 + s13)" "s12 ## s13" "s1 = s11 + s12 + s13" apply (atomize_elim) apply(elim sep_conjE)+ apply (rule_tac x = xa in exI) apply (rule_tac x = xaa in exI) apply (rule_tac x = ya in exI) apply (intro conjI, assumption+) by (auto simp:set_ins_def) show ?thesis proof(rule reps_splitedI[where v = "(v - int (x + 1) - 1)"]) show "(reps u (v - int (x + 1) - 1) xs \<and>* zero (v - int (x + 1) - 1 + 1) \<and>* reps (v - int (x + 1) - 1 + 2) (1 + v) [Suc x]) s" proof(rule sep_conjI) from hhh(1) show "reps u (v - int (x + 1) - 1) xs s11" . next show "(zero (v - int (x + 1) - 1 + 1) \<and>* reps (v - int (x + 1) - 1 + 2) (1 + v) [Suc x]) (s12 + (s13 + s2))" proof(rule sep_conjI) from hhh(2) show "zero (v - int (x + 1) - 1 + 1) s12" by smt next from hh(4) hhh(3) show "reps (v - int (x + 1) - 1 + 2) (1 + v) [Suc x] (s13 + s2)" apply (simp add:reps.simps del:ones_simps add:ones_rev) by (smt hh(3) hh(4) hhh(4) hhh(5) hhh(6) sep_add_disjD sep_conjI sep_disj_addI1) next show "s12 ## s13 + s2" by (metis hh(3) hhh(4) hhh(5) hhh(6) sep_add_commute sep_add_disjD sep_add_disjI2 sep_disj_addD sep_disj_addD1 sep_disj_addI1 sep_disj_commuteI) next show "s12 + (s13 + s2) = s12 + (s13 + s2)" by metis qed next show "s11 ## s12 + (s13 + s2)" by (metis hh(3) hhh(4) hhh(5) hhh(6) sep_disj_addD1 sep_disj_addI1 sep_disj_addI3) next show "s = s11 + (s12 + (s13 + s2))" by (smt hh(2) hh(3) hhh(4) hhh(5) hhh(6) sep_add_assoc sep_add_commute sep_add_disjD sep_add_disjI2 sep_disj_addD1 sep_disj_addD2 sep_disj_addI1 sep_disj_addI3 sep_disj_commuteI) qed next from False show "xs \<noteq> []" . next show "[Suc x] \<noteq> []" by simp qedqedlemma cond_expand: "(<cond> \<and>* p) s = (cond \<and> (p s))" by (metis (full_types) condD pasrt_def sep_conj_commuteI sep_conj_sep_emptyI sep_empty_def sep_globalise)lemma ones_rev1: assumes "\<not> (1 + n) < m" shows "(ones m n \<and>* one (1 + n)) = (ones m (1 + n))" by (insert ones_rev[OF assms, simplified], simp)lemma reps_one_abs: assumes "(reps u v [k] \<and>* one w) s" "w = v + 1" shows "(reps u w [Suc k]) s" using assms unfolding assms apply (simp add:reps.simps sep_conj_ac) apply (subst (asm) sep_conj_cond)+ apply (erule condE, simp) by (simp add:ones_rev sep_conj_ac, sep_cancel+, smt)lemma reps'_reps_abs: assumes "(reps' u v xs \<and>* reps w x ys) s" "w = v + 1" "ys \<noteq> []" shows "(reps u x (xs@ys)) s"proof(cases "xs = []") case False with assms have h: "splited (xs@ys) xs ys" by (simp add:splited_def) from assms(1)[unfolded assms(2)] show ?thesis apply (unfold reps_splited[OF h]) apply (insert False, unfold reps'_def, simp) apply (fwd reps_lenE, (subst (asm) sep_conj_cond)+) by (erule condE, simp)next case True with assms show ?thesis apply (simp add:reps'_def) by (erule condE, simp)qedlemma reps_one_abs1: assumes "(reps u v (xs@[k]) \<and>* one w) s" "w = v + 1" shows "(reps u w (xs@[Suc k])) s"proof(cases "xs = []") case True with assms reps_one_abs show ?thesis by simpnext case False hence "splited (xs@[k]) xs [k]" by (simp add:splited_def) from assms(1)[unfolded reps_splited[OF this] assms(2)] show ?thesis apply (fwd reps_one_abs) apply (fwd reps_reps'_abs) apply (fwd reps'_reps_abs) by (simp add:assms)qedlemma tm_hoare_inc00: assumes h: "a < length ks \<and> ks ! a = v" shows "\<lbrace>st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u ia ks \<and>* fam_conj {ia<..} zero\<rbrace> i :[ Inc a ]: j \<lbrace>st j \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1) (ks[a := Suc v]) \<and>* fam_conj {(ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1)<..} zero\<rbrace>" (is "\<lbrace> ?P \<rbrace> ?code \<lbrace> ?Q \<rbrace>")proof - from h have "a < length ks" "ks ! a = v" by auto from list_nth_expand[OF `a < length ks`] have eq_ks: "ks = take a ks @ [ks!a] @ drop (Suc a) ks" . from `a < length ks` have "ks \<noteq> []" by auto hence "(reps u ia ks \<and>* zero (ia + 1)) = reps' u (ia + 1) ks" by (simp add:reps'_def) also from eq_ks have "\<dots> = reps' u (ia + 1) (take a ks @ [ks!a] @ drop (Suc a) ks)" by simp also have "\<dots> = (EXS m. reps' u (m - 1) (take a ks) \<and>* reps' m (ia + 1) (ks ! a # drop (Suc a) ks))" by (simp add:reps'_append) also have "\<dots> = (EXS m. reps' u (m - 1) (take a ks) \<and>* reps' m (ia + 1) ([ks ! a] @ drop (Suc a) ks))" by simp also have "\<dots> = (EXS m ma. reps' u (m - 1) (take a ks) \<and>* reps' m (ma - 1) [ks ! a] \<and>* reps' ma (ia + 1) (drop (Suc a) ks))" by (simp only:reps'_append sep_conj_exists) finally have eq_s: "(reps u ia ks \<and>* zero (ia + 1)) = \<dots>" . { fix m ma have eq_u: "-1 + u = u - 1" by smt have " \<lbrace>st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* (reps' u (m - 1) (take a ks) \<and>* reps' m (ma - 1) [ks ! a] \<and>* reps' ma (ia + 1) (drop (Suc a) ks)) \<and>* fam_conj {ia + 1<..} zero\<rbrace> i :[ Inc a ]: j \<lbrace>st j \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1) (ks[a := Suc v]) \<and>* fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1<..} zero\<rbrace>" proof(cases "(drop (Suc a) ks) = []") case True { fix hc have eq_1: "(1 + (m + int (ks ! a))) = (m + int (ks ! a) + 1)" by simp have eq_2: "take a ks @ [Suc (ks ! a)] = ks[a := Suc v]" apply (subst (3) eq_ks, unfold True, simp) by (metis True append_Nil2 eq_ks h upd_conv_take_nth_drop) assume h: "(fam_conj {1 + (m + int (ks ! a))<..} zero \<and>* reps u (1 + (m + int (ks ! a))) (take a ks @ [Suc (ks ! a)])) hc" hence "(fam_conj {m + int (ks ! a) + 1<..} zero \<and>* reps u (m + int (ks ! a) + 1) (ks[a := Suc v])) hc" by (unfold eq_1 eq_2 , sep_cancel+) } note eq_fam = this show ?thesis apply (unfold Inc_def, subst (3) reps'_def, simp add:True sep_conj_cond) apply (intro tm.pre_condI, simp) apply (subst fam_conj_interv_simp, simp, subst (3) zero_def) apply hsteps apply (subst reps'_sg, simp add:sep_conj_cond del:ones_simps) apply (rule tm.pre_condI, simp del:ones_simps) apply hsteps apply (rule_tac p = " st j' \<and>* ps (1 + (m + int (ks ! a))) \<and>* zero (u - 1) \<and>* zero (u - 2) \<and>* reps u (1 + (m + int (ks ! a))) (take a ks @ [Suc (ks!a)]) \<and>* fam_conj {1 + (m + int (ks ! a))<..} zero " in tm.pre_stren) apply (hsteps) apply (simp add:sep_conj_ac list_ext_lt[OF `a < length ks`], sep_cancel+) apply (fwd eq_fam, sep_cancel+) apply (simp del:ones_simps add:sep_conj_ac) apply (sep_cancel+, prune) apply ((fwd abs_reps')+, simp) apply (fwd reps_one_abs abs_reps')+ apply (subst (asm) reps'_def, simp) by (subst fam_conj_interv_simp, simp add:sep_conj_ac) next case False then obtain k' ks' where eq_drop: "drop (Suc a) ks = [k']@ks'" by (metis append_Cons append_Nil list.exhaust) from `a < length ks` have eq_ks: "ks[a := Suc v] = (take a ks @ [Suc (ks ! a)]) @ (drop (Suc a) ks)" apply (fold `ks!a = v`) by (metis append_Cons append_Nil append_assoc upd_conv_take_nth_drop) show ?thesis apply (unfold Inc_def) apply (unfold Inc_def eq_drop reps'_append, simp add:sep_conj_exists del:ones_simps) apply (rule tm.precond_exI, subst (2) reps'_sg) apply (subst sep_conj_cond)+ apply (subst (1) ones_int_expand) apply (rule tm.pre_condI, simp del:ones_simps) apply hsteps (* apply (hsteps hoare_locate_skip_gen[OF `a < length ks`]) *) apply (subst reps'_sg, simp add:sep_conj_cond del:ones_simps) apply (rule tm.pre_condI, simp del:ones_simps) apply hsteps apply (rule_tac p = "st j' \<and>* ps (2 + (m + int (ks ! a))) \<and>* reps (2 + (m + int (ks ! a))) ia (drop (Suc a) ks) \<and>* zero (ia + 1) \<and>* zero (ia + 2) \<and>* reps u (m + int (ks ! a)) (take a ks @ [ks!a]) \<and>* zero (1 + (m + int (ks ! a))) \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* fam_conj {ia + 2<..} zero " in tm.pre_stren) apply (hsteps hoare_shift_right_cons_gen[OF False] hoare_left_until_double_zero_gen[OF False]) apply (rule_tac p = "st j' \<and>* ps (1 + (m + int (ks ! a))) \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u (1 + (m + int (ks ! a))) (take a ks @ [Suc (ks ! a)]) \<and>* zero (2 + (m + int (ks ! a))) \<and>* reps (3 + (m + int (ks ! a))) (ia + 1) (drop (Suc a) ks) \<and>* fam_conj {ia + 1<..} zero " in tm.pre_stren) apply (hsteps) apply (simp add:sep_conj_ac, sep_cancel+) apply (unfold list_ext_lt[OF `a < length ks`], simp) apply (fwd abs_reps')+ apply(fwd reps'_reps_abs) apply (subst eq_ks, simp) apply (sep_cancel+) apply (thin_tac "mb = 4 + (m + (int (ks ! a) + int k'))") apply (thin_tac "ma = 2 + (m + int (ks ! a))", prune) apply (simp add: int_add_ac sep_conj_ac, sep_cancel+) apply (fwd reps_one_abs1, subst fam_conj_interv_simp, simp, sep_cancel+, smt) apply (fwd abs_ones)+ apply (fwd abs_reps') apply (fwd abs_reps') apply (fwd abs_reps') apply (fwd abs_reps') apply (unfold eq_drop, simp add:int_add_ac sep_conj_ac) apply (sep_cancel+) apply (fwd reps'_abs[where xs = "take a ks"]) apply (fwd reps'_abs[where xs = "[k']"]) apply (unfold reps'_def, simp add:int_add_ac sep_conj_ac) apply (sep_cancel+) by (subst (asm) fam_conj_interv_simp, simp, smt) qed } note h = this show ?thesis apply (subst fam_conj_interv_simp) apply (rule_tac p = "st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* (reps u ia ks \<and>* zero (ia + 1)) \<and>* fam_conj {ia + 1<..} zero" in tm.pre_stren) apply (unfold eq_s, simp only:sep_conj_exists) apply (intro tm.precond_exI h) by (sep_cancel+, unfold eq_s, simp)qeddeclare ones_simps [simp del]lemma tm_hoare_inc01: assumes "length ks \<le> a \<and> v = 0" shows "\<lbrace>st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u ia ks \<and>* fam_conj {ia<..} zero\<rbrace> i :[ Inc a ]: j \<lbrace>st j \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1) ((list_ext a ks)[a := Suc v]) \<and>* fam_conj {(ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1)<..} zero\<rbrace>"proof - from assms have "length ks \<le> a" "v = 0" by auto show ?thesis apply (rule_tac p = " st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* (reps u ia ks \<and>* <(ia = u + int (reps_len ks) - 1)>) \<and>* fam_conj {ia<..} zero " in tm.pre_stren) apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, simp) apply (unfold Inc_def) apply hstep (* apply (hstep hoare_locate_set_gen[OF `length ks \<le> a`]) *) apply (simp only:sep_conj_exists) apply (intro tm.precond_exI) my_block fix m w have "reps m w [list_ext a ks ! a] = (ones m (m + int (list_ext a ks ! a)) \<and>* <(w = m + int (list_ext a ks ! a))>)" by (simp add:reps.simps) my_block_end apply (unfold this) apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, simp) apply (subst fam_conj_interv_simp) apply (hsteps) apply (subst fam_conj_interv_simp, simp) apply (hsteps) apply (rule_tac p = "st j' \<and>* ps (m + int (list_ext a ks ! a) + 1) \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u (m + int (list_ext a ks ! a) + 1) ((take a (list_ext a ks))@[Suc (list_ext a ks ! a)]) \<and>* fam_conj {(m + int (list_ext a ks ! a) + 1)<..} zero " in tm.pre_stren) apply (hsteps) apply (simp add:sep_conj_ac, sep_cancel+) apply (unfold `v = 0`, prune) my_block from `length ks \<le> a` have "list_ext a ks ! a = 0" by (metis le_refl list_ext_tail) from `length ks \<le> a` have "a < length (list_ext a ks)" by (metis list_ext_len) from reps_len_suc[OF this] have eq_len: "int (reps_len (list_ext a ks)) = int (reps_len (list_ext a ks[a := Suc (list_ext a ks ! a)])) - 1" by smt fix m w hc assume h: "(fam_conj {m + int (list_ext a ks ! a) + 1<..} zero \<and>* reps u (m + int (list_ext a ks ! a) + 1) (take a (list_ext a ks) @ [Suc (list_ext a ks ! a)])) hc" then obtain s where "(reps u (m + int (list_ext a ks ! a) + 1) (take a (list_ext a ks) @ [Suc (list_ext a ks ! a)])) s" by (auto dest!:sep_conjD) from reps_len_correct[OF this] have "m = u + int (reps_len (take a (list_ext a ks) @ [Suc (list_ext a ks ! a)])) - int (list_ext a ks ! a) - 2" by smt from h [unfolded this] have "(fam_conj {u + int (reps_len (list_ext a ks))<..} zero \<and>* reps u (u + int (reps_len (list_ext a ks))) (list_ext a ks[a := Suc 0])) hc" apply (unfold eq_len, simp) my_block from `a < length (list_ext a ks)` have "take a (list_ext a ks) @ [Suc (list_ext a ks ! a)] = list_ext a ks[a := Suc (list_ext a ks ! a)]" by (smt `list_ext a ks ! a = 0` assms length_take list_ext_tail_expand list_update_length) my_block_end apply (unfold this) my_block have "-1 + (u + int (reps_len (list_ext a ks[a := Suc (list_ext a ks ! a)]))) = u + (int (reps_len (list_ext a ks[a := Suc (list_ext a ks ! a)])) - 1)" by simp my_block_end apply (unfold this) apply (sep_cancel+) by (unfold `(list_ext a ks ! a) = 0`, simp) my_block_end apply (rule this, assumption) apply (simp only:sep_conj_ac, sep_cancel+)+ apply (fwd abs_reps')+ apply (fwd reps_one_abs) apply (fwd reps'_reps_abs) apply (simp add:int_add_ac sep_conj_ac) apply (sep_cancel+) apply (subst fam_conj_interv_simp, simp add:sep_conj_ac, smt) apply (fwd reps_lenE, (subst (asm) sep_conj_cond)+, erule condE, simp) by (sep_cancel+)qeddefinition "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))"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)qedlemma tm_hoare_dec_fail00: assumes "a < length ks \<and> ks ! a = 0" shows "\<lbrace>st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u ia ks \<and>* fam_conj {ia<..} zero\<rbrace> i :[ Dec a e ]: j \<lbrace>st e \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks)) (list_ext a ks[a := 0]) \<and>* fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) <..} zero\<rbrace>"proof - from assms have "a < length ks" "ks!a = 0" by auto from list_nth_expand[OF `a < length ks`] have eq_ks: "ks = take a ks @ [ks ! a] @ drop (Suc a) ks" . show ?thesis proof(cases " drop (Suc a) ks = []") case False then obtain k' ks' where eq_drop: "drop (Suc a) ks = [k']@ks'" by (metis append_Cons append_Nil list.exhaust) show ?thesis apply (unfold Dec_def, intro t_hoare_local) apply (subst tassemble_to.simps(2), rule tm.code_exI, rule tm.code_extension) apply (subst (1) eq_ks) my_block have "(reps u ia (take a ks @ [ks ! a] @ drop (Suc a) ks) \<and>* fam_conj {ia<..} zero) = (reps' u (ia + 1) ((take a ks @ [ks ! a]) @ drop (Suc a) ks) \<and>* fam_conj {ia + 1<..} zero)" apply (subst fam_conj_interv_simp) by (unfold reps'_def, simp add:sep_conj_ac) my_block_end apply (unfold this) apply (subst reps'_append) apply (unfold eq_drop) apply (subst (2) reps'_append) apply (simp only:sep_conj_exists, intro tm.precond_exI) apply (subst (2) reps'_def, simp add:reps.simps ones_simps) apply (subst reps'_append, simp only:sep_conj_exists, intro tm.precond_exI) apply hstep (* apply (hstep hoare_locate_skip_gen[OF `a < length ks`]) *) my_block fix m mb have "(reps' mb (m - 1) [ks ! a]) = (reps mb (m - 2) [ks!a] \<and>* zero (m - 1))" by (simp add:reps'_def, smt) my_block_end apply (unfold this) apply hstep (* apply (hstep hoare_if_reps_nz_false_gen[OF `ks!a = 0`]) *) apply (simp only:reps.simps(2), simp add:`ks!a = 0`) apply (rule_tac p = "st j'b \<and>* ps mb \<and>* reps u mb ((take a ks)@[ks ! a]) \<and>* <(m - 2 = mb)> \<and>* zero (m - 1) \<and>* zero (u - 1) \<and>* one m \<and>* zero (u - 2) \<and>* ones (m + 1) (m + int k') \<and>* <(-2 + ma = m + int k')> \<and>* zero (ma - 1) \<and>* reps' ma (ia + 1) ks' \<and>* fam_conj {ia + 1<..} zero" in tm.pre_stren) apply hsteps apply (simp add:sep_conj_ac, sep_cancel+) apply (subgoal_tac "m + int k' = ma - 2", simp) apply (fwd abs_ones)+ apply (subst (asm) sep_conj_cond)+ apply (erule condE, auto) apply (fwd abs_reps')+ apply (subgoal_tac "ma = m + int k' + 2", simp) apply (fwd abs_reps')+ my_block from `a < length ks` have "list_ext a ks = ks" by (auto simp:list_ext_def) my_block_end apply (simp add:this) apply (subst eq_ks, simp add:eq_drop `ks!a = 0`) apply (subst (asm) reps'_def, simp) apply (subst fam_conj_interv_simp, simp add:sep_conj_ac, sep_cancel+) apply (metis append_Cons assms eq_Nil_appendI eq_drop eq_ks list_update_id) apply (clarsimp) apply (subst (asm) sep_conj_cond)+ apply (erule condE, clarsimp) apply (subst (asm) sep_conj_cond)+ apply (erule condE, clarsimp) apply (simp add:sep_conj_ac, sep_cancel+) apply (fwd abs_reps')+ by (fwd reps'_reps_abs, simp add:`ks!a = 0`) next case True show ?thesis apply (unfold Dec_def, intro t_hoare_local) apply (subst tassemble_to.simps(2), rule tm.code_exI, rule tm.code_extension) apply (subst (1) eq_ks, unfold True, simp) my_block have "(reps u ia (take a ks @ [ks ! a]) \<and>* fam_conj {ia<..} zero) = (reps' u (ia + 1) (take a ks @ [ks ! a]) \<and>* fam_conj {ia + 1<..} zero)" apply (unfold reps'_def, subst fam_conj_interv_simp) by (simp add:sep_conj_ac) my_block_end apply (subst (1) this) apply (subst reps'_append) apply (simp only:sep_conj_exists, intro tm.precond_exI) apply (subst fam_conj_interv_simp, simp) my_block have "(zero (2 + ia)) = (tm (2 + ia) Bk)" by (simp add:zero_def) my_block_end my_note eq_z = this apply hstep (* apply (hstep hoare_locate_skip_gen[OF `a < length ks`]) *) my_block fix m have "(reps' m (ia + 1) [ks ! a]) = (reps m ia [ks!a] \<and>* zero (ia + 1))" by (simp add:reps'_def) my_block_end apply (unfold this, prune) apply hstep (* apply (hstep hoare_if_reps_nz_false_gen[OF `ks!a = 0`]) *) apply (simp only:reps.simps(2), simp add:`ks!a = 0`) apply (rule_tac p = "st j'b \<and>* ps m \<and>* (reps u m ((take a ks)@[ks!a]) \<and>* <(ia = m)>) \<and>* zero (ia + 1) \<and>* zero (u - 1) \<and>* zero (2 + ia) \<and>* zero (u - 2) \<and>* fam_conj {2 + ia<..} zero" in tm.pre_stren) apply hsteps apply (simp add:sep_conj_ac) apply ((subst (asm) sep_conj_cond)+, erule condE, simp) my_block from `a < length ks` have "list_ext a ks = ks" by (metis list_ext_lt) my_block_end apply (unfold this, simp) apply (subst fam_conj_interv_simp) apply (subst fam_conj_interv_simp, simp) apply (simp only:sep_conj_ac, sep_cancel+) apply (subst eq_ks, unfold True `ks!a = 0`, simp) apply (metis True append_Nil2 assms eq_ks list_update_same_conv) apply (simp add:sep_conj_ac) apply (subst (asm) sep_conj_cond)+ apply (erule condE, simp, thin_tac "ia = m") apply (fwd abs_reps')+ apply (simp add:sep_conj_ac int_add_ac, sep_cancel+) apply (unfold reps'_def, simp) by (metis sep.mult_commute) qedqedlemma tm_hoare_dec_fail01: assumes "length ks \<le> a" shows "\<lbrace>st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u ia ks \<and>* fam_conj {ia<..} zero\<rbrace> i :[ Dec a e ]: j \<lbrace>st e \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks)) (list_ext a ks[a := 0]) \<and>* fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) <..} zero\<rbrace>" apply (unfold Dec_def, intro t_hoare_local) apply (subst tassemble_to.simps(2), rule tm.code_exI, rule tm.code_extension) apply (rule_tac p = "st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u ia ks \<and>* fam_conj {ia<..} zero \<and>* <(ia = u + int (reps_len ks) - 1)>" in tm.pre_stren) apply hstep (* apply (hstep hoare_locate_set_gen[OF `length ks \<le> a`]) *) apply (simp only:sep_conj_exists, intro tm.precond_exI) my_block from assms have "list_ext a ks ! a = 0" by (metis le_refl list_ext_tail) my_block_end my_note is_z = this apply (subst fam_conj_interv_simp) apply hstep (* apply (hstep hoare_if_reps_nz_false_gen[OF is_z]) *) apply (unfold is_z) apply (subst (1) reps.simps) apply (rule_tac p = "st j'b \<and>* ps m \<and>* reps u m (take a (list_ext a ks) @ [0]) \<and>* zero (w + 1) \<and>* <(w = m + int 0)> \<and>* zero (u - 1) \<and>* fam_conj {w + 1<..} zero \<and>* zero (u - 2) \<and>* <(ia = u + int (reps_len ks) - 1)>" in tm.pre_stren) my_block have "(take a (list_ext a ks)) @ [0] \<noteq> []" by simp my_block_end apply hsteps (* apply (hsteps hoare_left_until_double_zero_gen[OF this]) *) apply (simp add:sep_conj_ac) apply prune apply (subst (asm) sep_conj_cond)+ apply (elim condE, simp add:sep_conj_ac, prune) my_block fix m w ha assume h1: "w = m \<and> ia = u + int (reps_len ks) - 1" and h: "(ps u \<and>* st e \<and>* zero (u - 1) \<and>* zero (m + 1) \<and>* fam_conj {m + 1<..} zero \<and>* zero (u - 2) \<and>* reps u m (take a (list_ext a ks) @ [0])) ha" from h1 have eq_w: "w = m" and eq_ia: "ia = u + int (reps_len ks) - 1" by auto from h obtain s' where "reps u m (take a (list_ext a ks) @ [0]) s'" by (auto dest!:sep_conjD) from reps_len_correct[OF this] have eq_m: "m = u + int (reps_len (take a (list_ext a ks) @ [0])) - 1" . from h[unfolded eq_m, simplified] have "(ps u \<and>* st e \<and>* zero (u - 1) \<and>* zero (u - 2) \<and>* fam_conj {u + (-1 + int (reps_len (list_ext a ks)))<..} zero \<and>* reps u (u + (-1 + int (reps_len (list_ext a ks)))) (list_ext a ks[a := 0])) ha" apply (sep_cancel+) apply (subst fam_conj_interv_simp, simp) my_block from `length ks \<le> a` have "list_ext a ks[a := 0] = list_ext a ks" by (metis is_z list_update_id) my_block_end apply (unfold this) my_block from `length ks \<le> a` is_z have "take a (list_ext a ks) @ [0] = list_ext a ks" by (metis list_ext_tail_expand) my_block_end apply (unfold this) by (simp add:sep_conj_ac, sep_cancel+, smt) my_block_end apply (rule this, assumption) apply (sep_cancel+)[1] apply (subst (asm) sep_conj_cond)+ apply (erule condE, prune, simp) my_block fix s m assume "(reps' u (m - 1) (take a (list_ext a ks)) \<and>* ones m m \<and>* zero (m + 1)) s" hence "reps' u (m + 1) (take a (list_ext a ks) @ [0]) s" apply (unfold reps'_append) apply (rule_tac x = m in EXS_intro) by (subst (2) reps'_def, simp add:reps.simps) my_block_end apply (rotate_tac 1, fwd this) apply (subst (asm) reps'_def, simp add:sep_conj_ac) my_block fix s assume h: "(st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u ia ks \<and>* fam_conj {ia<..} zero) s" then obtain s' where "reps u ia ks s'" by (auto dest!:sep_conjD) from reps_len_correct[OF this] have eq_ia: "ia = u + int (reps_len ks) - 1" . from h have "(st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u ia ks \<and>* fam_conj {ia<..} zero \<and>* <(ia = u + int (reps_len ks) - 1)>) s" by (unfold eq_ia, simp) my_block_end by (rule this, assumption)lemma t_hoare_label1: "(\<And>l. l = i \<Longrightarrow> \<lbrace>st l \<and>* p\<rbrace> l :[ c l ]: j \<lbrace>st k \<and>* q\<rbrace>) \<Longrightarrow> \<lbrace>st l \<and>* p \<rbrace> i:[(TLabel l; c l)]:j \<lbrace>st k \<and>* q\<rbrace>"by (unfold tassemble_to.simps, intro tm.code_exI tm.code_condI, clarify, auto)lemma tm_hoare_dec_fail1: assumes "a < length ks \<and> ks ! a = 0 \<or> length ks \<le> a" shows "\<lbrace>st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u ia ks \<and>* fam_conj {ia<..} zero\<rbrace> i :[ Dec a e ]: j \<lbrace>st e \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks)) (list_ext a ks[a := 0]) \<and>* fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) <..} zero\<rbrace>" using assmsproof assume "a < length ks \<and> ks ! a = 0" thus ?thesis by (rule tm_hoare_dec_fail00)next assume "length ks \<le> a" thus ?thesis by (rule tm_hoare_dec_fail01)qedlemma shift_left_nil_gen[step]: assumes "u = v" shows "\<lbrace>st i \<and>* ps u \<and>* zero v\<rbrace> i :[shift_left]:j \<lbrace>st j \<and>* ps u \<and>* zero v\<rbrace>" apply(unfold assms shift_left_def, intro t_hoare_local t_hoare_label, clarify, rule t_hoare_label_last, simp, clarify, prune, simp) by hsteplemma tm_hoare_dec_suc1: assumes "a < length ks \<and> ks ! a = Suc v" shows "\<lbrace>st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u ia ks \<and>* fam_conj {ia<..} zero\<rbrace> i :[ Dec a e ]: j \<lbrace>st j \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u (ia - 1) (list_ext a ks[a := v]) \<and>* fam_conj {ia - 1<..} zero\<rbrace>"proof - from assms have "a < length ks" " ks ! a = Suc v" by auto from list_nth_expand[OF `a < length ks`] have eq_ks: "ks = take a ks @ [ks ! a] @ drop (Suc a) ks" . show ?thesis proof(cases " drop (Suc a) ks = []") case False then obtain k' ks' where eq_drop: "drop (Suc a) ks = [k']@ks'" by (metis append_Cons append_Nil list.exhaust) show ?thesis apply (unfold Dec_def, intro t_hoare_local) apply (subst tassemble_to.simps(2), rule tm.code_exI) apply (subst (1) eq_ks) my_block have "(reps u ia (take a ks @ [ks ! a] @ drop (Suc a) ks) \<and>* fam_conj {ia<..} zero) = (reps' u (ia + 1) ((take a ks @ [ks ! a]) @ drop (Suc a) ks) \<and>* fam_conj {ia + 1<..} zero)" apply (subst fam_conj_interv_simp) by (unfold reps'_def, simp add:sep_conj_ac) my_block_end apply (unfold this) apply (subst reps'_append) apply (unfold eq_drop) apply (subst (2) reps'_append) apply (simp only:sep_conj_exists, intro tm.precond_exI) apply (subst (2) reps'_def, simp add:reps.simps ones_simps) apply (subst reps'_append, simp only:sep_conj_exists, intro tm.precond_exI) apply (rule_tac q = "st l \<and>* ps mb \<and>* zero (u - 1) \<and>* reps' u (mb - 1) (take a ks) \<and>* reps' mb (m - 1) [ks ! a] \<and>* one m \<and>* zero (u - 2) \<and>* ones (m + 1) (m + int k') \<and>* <(-2 + ma = m + int k')> \<and>* zero (ma - 1) \<and>* reps' ma (ia + 1) ks' \<and>* fam_conj {ia + 1<..} zero" in tm.sequencing) apply (rule tm.code_extension) apply hstep (* apply (hstep hoare_locate_skip_gen[OF `a < length ks`]) *) apply (subst (2) reps'_def, simp) my_block fix i j l m mb from `ks!a = (Suc v)` have "ks!a \<noteq> 0" by simp from hoare_if_reps_nz_true[OF this, where u = mb and v = "m - 2"] have "\<lbrace>st i \<and>* ps mb \<and>* reps mb (-2 + m) [ks ! a]\<rbrace> i :[ if_reps_nz l ]: j \<lbrace>st l \<and>* ps mb \<and>* reps mb (-2 + m) [ks ! a]\<rbrace>" by smt my_block_end apply (hgoto this) apply (simp add:sep_conj_ac, sep_cancel+) apply (subst reps'_def, simp add:sep_conj_ac) apply (rule tm.code_extension1) apply (rule t_hoare_label1, simp, prune) apply (subst (2) reps'_def, simp add:reps.simps) apply (rule_tac p = "st j' \<and>* ps mb \<and>* zero (u - 1) \<and>* reps' u (mb - 1) (take a ks) \<and>* ((ones mb (mb + int (ks ! a)) \<and>* <(-2 + m = mb + int (ks ! a))>) \<and>* zero (mb + int (ks ! a) + 1)) \<and>* one (mb + int (ks ! a) + 2) \<and>* zero (u - 2) \<and>* ones (mb + int (ks ! a) + 3) (mb + int (ks ! a) + int k' + 2) \<and>* <(-2 + ma = m + int k')> \<and>* zero (ma - 1) \<and>* reps' ma (ia + 1) ks' \<and>* fam_conj {ia + 1<..} zero " in tm.pre_stren) apply hsteps (* apply (simp add:sep_conj_ac) *) apply (unfold `ks!a = Suc v`) my_block fix mb have "(ones mb (mb + int (Suc v))) = (ones mb (mb + int v) \<and>* one (mb + int (Suc v)))" by (simp add:ones_rev) my_block_end apply (unfold this, prune) apply hsteps apply (rule_tac p = "st j'a \<and>* ps (mb + int (Suc v) + 2) \<and>* zero (mb + int (Suc v) + 1) \<and>* reps (mb + int (Suc v) + 2) ia (drop (Suc a) ks) \<and>* zero (ia + 1) \<and>* zero (ia + 2) \<and>* zero (mb + int (Suc v)) \<and>* ones mb (mb + int v) \<and>* zero (u - 1) \<and>* reps' u (mb - 1) (take a ks) \<and>* zero (u - 2) \<and>* fam_conj {ia + 2<..} zero " in tm.pre_stren) apply hsteps (* apply (hsteps hoare_shift_left_cons_gen[OF False]) *) apply (rule_tac p = "st j'a \<and>* ps (ia - 1) \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u (ia - 1) (take a ks @ [v] @ drop (Suc a) ks) \<and>* zero ia \<and>* zero (ia + 1) \<and>* zero (ia + 2) \<and>* fam_conj {ia + 2<..} zero " in tm.pre_stren) apply hsteps apply (simp add:sep_conj_ac) apply (subst fam_conj_interv_simp) apply (subst fam_conj_interv_simp) apply (subst fam_conj_interv_simp) apply (simp add:sep_conj_ac) apply (sep_cancel+) my_block have "take a ks @ v # drop (Suc a) ks = list_ext a ks[a := v]" proof - from `a < length ks` have "list_ext a ks = ks" by (metis list_ext_lt) hence "list_ext a ks[a:=v] = ks[a:=v]" by simp moreover from `a < length ks` have "ks[a:=v] = take a ks @ v # drop (Suc a) ks" by (metis upd_conv_take_nth_drop) ultimately show ?thesis by metis qed my_block_end apply (unfold this, sep_cancel+, smt) apply (simp add:sep_conj_ac) apply (fwd abs_reps')+ apply (simp add:sep_conj_ac int_add_ac) apply (sep_cancel+) apply (subst (asm) reps'_def, simp add:sep_conj_ac) apply (subst (asm) sep_conj_cond)+ apply (erule condE, clarsimp) apply (simp add:sep_conj_ac, sep_cancel+) apply (fwd abs_ones)+ apply (fwd abs_reps')+ apply (subst (asm) reps'_def, simp) apply (subst (asm) fam_conj_interv_simp) apply (simp add:sep_conj_ac int_add_ac eq_drop reps'_def) apply (subst (asm) sep_conj_cond)+ apply (erule condE, clarsimp) by (simp add:sep_conj_ac int_add_ac) next case True show ?thesis apply (unfold Dec_def, intro t_hoare_local) apply (subst tassemble_to.simps(2), rule tm.code_exI) apply (subst (1) eq_ks, simp add:True) my_block have "(reps u ia (take a ks @ [ks ! a]) \<and>* fam_conj {ia<..} zero) = (reps' u (ia + 1) (take a ks @ [ks ! a]) \<and>* fam_conj {ia + 1<..} zero)" apply (subst fam_conj_interv_simp) by (unfold reps'_def, simp add:sep_conj_ac) my_block_end apply (unfold this) apply (subst reps'_append) apply (simp only:sep_conj_exists, intro tm.precond_exI) apply (rule_tac q = "st l \<and>* ps m \<and>* zero (u - 1) \<and>* reps' u (m - 1) (take a ks) \<and>* reps' m (ia + 1) [ks ! a] \<and>* zero (2 + ia) \<and>* zero (u - 2) \<and>* fam_conj {2 + ia<..} zero" in tm.sequencing) apply (rule tm.code_extension) apply (subst fam_conj_interv_simp, simp) apply hsteps (* apply (hstep hoare_locate_skip_gen[OF `a < length ks`]) *) my_block fix m have "(reps' m (ia + 1) [ks ! a]) = (reps m ia [ks!a] \<and>* zero (ia + 1))" by (unfold reps'_def, simp) my_block_end apply (unfold this) my_block fix i j l m from `ks!a = (Suc v)` have "ks!a \<noteq> 0" by simp my_block_end apply (hgoto hoare_if_reps_nz_true_gen) apply (rule tm.code_extension1) apply (rule t_hoare_label1, simp) apply (thin_tac "la = j'", prune) apply (subst (1) reps.simps) apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, simp) apply hsteps apply (unfold `ks!a = Suc v`) my_block fix m have "(ones m (m + int (Suc v))) = (ones m (m + int v) \<and>* one (m + int (Suc v)))" by (simp add:ones_rev) my_block_end apply (unfold this) apply hsteps apply (rule_tac p = "st j'a \<and>* ps (m + int v) \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u (m + int v) (take a ks @ [v]) \<and>* zero (m + (1 + int v)) \<and>* zero (2 + (m + int v)) \<and>* zero (3 + (m + int v)) \<and>* fam_conj {3 + (m + int v)<..} zero " in tm.pre_stren) apply hsteps apply (simp add:sep_conj_ac, sep_cancel+) my_block have "take a ks @ [v] = list_ext a ks[a := v]" proof - from True `a < length ks` have "ks = take a ks @ [ks!a]" by (metis append_Nil2 eq_ks) hence "ks[a:=v] = take a ks @ [v]" by (metis True `a < length ks` upd_conv_take_nth_drop) moreover from `a < length ks` have "list_ext a ks = ks" by (metis list_ext_lt) ultimately show ?thesis by simp qed my_block_end my_note eq_l = this apply (unfold this) apply (subst fam_conj_interv_simp) apply (subst fam_conj_interv_simp) apply (subst fam_conj_interv_simp) apply (simp add:sep_conj_ac, sep_cancel, smt) apply (simp add:sep_conj_ac int_add_ac)+ apply (sep_cancel+) apply (fwd abs_reps')+ apply (fwd reps'_reps_abs) by (simp add:eq_l) qedqeddefinition "cfill_until_one = (TL start exit. TLabel start; if_one exit; write_one; move_left; jmp start; TLabel exit )"lemma hoare_cfill_until_one: "\<lbrace>st i \<and>* ps v \<and>* one (u - 1) \<and>* zeros u v\<rbrace> i :[ cfill_until_one ]: j \<lbrace>st j \<and>* ps (u - 1) \<and>* ones (u - 1) v \<rbrace>"proof(induct u v rule:zeros_rev_induct) case (Base x y) thus ?case apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, simp add:ones_simps) apply (unfold cfill_until_one_def, intro t_hoare_local t_hoare_label, rule t_hoare_label_last, simp+) by hstepnext case (Step x y) show ?case apply (rule_tac q = "st i \<and>* ps (y - 1) \<and>* one (x - 1) \<and>* zeros x (y - 1) \<and>* one y" in tm.sequencing) apply (subst cfill_until_one_def, intro t_hoare_local t_hoare_label, rule t_hoare_label_last, simp+) apply hsteps my_block fix i j l have "\<lbrace>st i \<and>* ps (y - 1) \<and>* one (x - 1) \<and>* zeros x (y - 1)\<rbrace> i :[ jmp l ]: j \<lbrace>st l \<and>* ps (y - 1) \<and>* one (x - 1) \<and>* zeros x (y - 1)\<rbrace>" apply (case_tac "(y - 1) < x", simp add:zeros_simps) apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, simp) apply hstep apply (drule_tac zeros_rev, simp) by hstep my_block_end apply (hstep this) (* The next half *) apply (hstep Step(2), simp add:sep_conj_ac, sep_cancel+) by (insert Step(1), simp add:ones_rev sep_conj_ac)qeddefinition "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 )"declare zeros.simps [simp del] zeros_simps[simp del]lemma hoare_cmove: assumes "w \<le> k" shows "\<lbrace>st i \<and>* ps (v + 2 + int w) \<and>* zero (u - 1) \<and>* reps u (v - int w) [k - w] \<and>* zeros (v - int w + 1) (v + 1) \<and>* one (v + 2) \<and>* ones (v + 3) (v + 2 + int w) \<and>* zeros (v + 3 + int w) (v + int(reps_len [k]) + 1)\<rbrace> i :[cmove]: j \<lbrace>st j \<and>* ps (u - 1) \<and>* zero (u - 1) \<and>* reps u u [0] \<and>* zeros (u + 1) (v + 1) \<and>* reps (v + 2) (v + int (reps_len [k]) + 1) [k]\<rbrace>" using assmsproof(induct "k - w" arbitrary: w) case (0 w) hence "w = k" by auto show ?case apply (simp add: `w = k` del:zeros.simps zeros_simps) apply (unfold cmove_def, intro t_hoare_local t_hoare_label, rule t_hoare_label_last, simp+) apply (simp add:reps_len_def reps_sep_len_def reps_ctnt_len_def del:zeros_simps zeros.simps) apply (rule_tac p = "st i \<and>* ps (v + 2 + int k) \<and>* zero (u - 1) \<and>* reps u u [0] \<and>* zeros (u + 1) (v + 1) \<and>* ones (v + 2) (v + 2 + int k) \<and>* zeros (v + 3 + int k) (2 + (v + int k)) \<and>* <(u = v - int k)>" in tm.pre_stren) my_block fix i j have "\<lbrace>st i \<and>* ps (v + 2 + int k) \<and>* zeros (u + 1) (v + 1) \<and>* ones (v + 2) (v + 2 + int k) \<and>* <(u = v - int k)>\<rbrace> i :[ left_until_zero ]: j \<lbrace>st j \<and>* ps (v + 1) \<and>* zeros (u + 1) (v + 1) \<and>* ones (v + 2) (v + 2 + int k) \<and>* <(u = v - int k)>\<rbrace>" apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, simp) my_block have "(zeros (v - int k + 1) (v + 1)) = (zeros (v - int k + 1) v \<and>* zero (v + 1))" by (simp only:zeros_rev, smt) my_block_end apply (unfold this) by hsteps my_block_end apply (hstep this) my_block fix i j have "\<lbrace>st i \<and>* ps (v + 1) \<and>* reps u u [0] \<and>* zeros (u + 1) (v + 1)\<rbrace> i :[left_until_one]:j \<lbrace>st j \<and>* ps u \<and>* reps u u [0] \<and>* zeros (u + 1) (v + 1)\<rbrace>" apply (simp add:reps.simps ones_simps) by hsteps my_block_end apply (hsteps this) apply ((subst (asm) sep_conj_cond)+, erule condE, clarsimp) apply (fwd abs_reps')+ apply (simp only:sep_conj_ac int_add_ac, sep_cancel+) apply (simp add:int_add_ac sep_conj_ac zeros_simps) apply (simp add:sep_conj_ac int_add_ac, sep_cancel+) apply (fwd reps_lenE) apply (subst (asm) sep_conj_cond)+ apply (erule condE, clarsimp) apply (subgoal_tac "v = u + int k + int (reps_len [0]) - 1", clarsimp) apply (simp add:reps_len_sg) apply (fwd abs_ones)+ apply (fwd abs_reps')+ apply (simp add:sep_conj_ac int_add_ac) apply (sep_cancel+) apply (simp add:reps.simps, smt) by (clarsimp)next case (Suc k' w) from `Suc k' = k - w` `w \<le> k` have h: "k' = k - (Suc w)" "Suc w \<le> k" by auto show ?case apply (rule tm.sequencing[OF _ Suc(1)[OF h(1, 2)]]) apply (unfold cmove_def, intro t_hoare_local t_hoare_label, rule t_hoare_label_last, simp+) apply (simp add:reps_len_def reps_sep_len_def reps_ctnt_len_def del:zeros_simps zeros.simps) my_block fix i j have "\<lbrace>st i \<and>* ps (v + 2 + int w) \<and>* zeros (v - int w + 1) (v + 1) \<and>* one (v + 2) \<and>* ones (v + 3) (v + 2 + int w) \<rbrace> i :[left_until_zero]: j \<lbrace>st j \<and>* ps (v + 1) \<and>* zeros (v - int w + 1) (v + 1) \<and>* one (v + 2) \<and>* ones (v + 3) (v + 2 + int w) \<rbrace>" my_block have "(one (v + 2) \<and>* ones (v + 3) (v + 2 + int w)) = ones (v + 2) (v + 2 + int w)" by (simp only:ones_simps, smt) my_block_end apply (unfold this) my_block have "(zeros (v - int w + 1) (v + 1)) = (zeros (v - int w + 1) v \<and>* zero (v + 1))" by (simp only:zeros_rev, simp) my_block_end apply (unfold this) by hsteps my_block_end apply (hstep this) my_block fix i j have "\<lbrace>st i \<and>* ps (v + 1) \<and>* reps u (v - int w) [k - w] \<and>* zeros (v - int w + 1) (v + 1)\<rbrace> i :[left_until_one]: j \<lbrace>st j \<and>* ps (v - int w) \<and>* reps u (v - int w) [k - w] \<and>* zeros (v - int w + 1) (v + 1)\<rbrace>" apply (simp add:reps.simps ones_rev) apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, clarsimp) apply (subgoal_tac "u + int (k - w) = v - int w", simp) defer apply simp by hsteps my_block_end apply (hstep this) my_block have "(reps u (v - int w) [k - w]) = (reps u (v - (1 + int w)) [k - Suc w] \<and>* one (v - int w))" apply (subst (1 2) reps.simps) apply (subst sep_conj_cond)+ my_block have "((v - int w = u + int (k - w))) = (v - (1 + int w) = u + int (k - Suc w))" apply auto apply (smt Suc.prems h(2)) by (smt Suc.prems h(2)) my_block_end apply (simp add:this) my_block fix b p q assume "(b \<Longrightarrow> (p::tassert) = q)" have "(<b> \<and>* p) = (<b> \<and>* q)" by (metis `b \<Longrightarrow> p = q` cond_eqI) my_block_end apply (rule this) my_block assume "v - (1 + int w) = u + int (k - Suc w)" hence "v = 1 + int w + u + int (k - Suc w)" by auto my_block_end apply (simp add:this) my_block have "\<not> (u + int (k - w)) < u" by auto my_block_end apply (unfold ones_rev[OF this]) my_block from Suc (2, 3) have "(u + int (k - w) - 1) = (u + int (k - Suc w))" by auto my_block_end apply (unfold this) my_block from Suc (2, 3) have "(u + int (k - w)) = (1 + (u + int (k - Suc w)))" by auto my_block_end by (unfold this, simp) my_block_end apply (unfold this) my_block fix i j have "\<lbrace>st i \<and>* ps (v - int w) \<and>* (reps u (v - (1 + int w)) [k - Suc w] \<and>* one (v - int w))\<rbrace> i :[ move_left]: j \<lbrace>st j \<and>* ps (v - (1 + int w)) \<and>* (reps u (v - (1 + int w)) [k - Suc w] \<and>* one (v - int w))\<rbrace>" apply (simp add:reps.simps ones_rev) apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, clarsimp) apply (subgoal_tac " u + int (k - Suc w) = v - (1 + int w)", simp) defer apply simp apply hsteps by (simp add:sep_conj_ac, sep_cancel+, smt) my_block_end apply (hstep this) my_block fix i' j' have "\<lbrace>st i' \<and>* ps (v - (1 + int w)) \<and>* reps u (v - (1 + int w)) [k - Suc w]\<rbrace> i' :[ if_zero j ]: j' \<lbrace>st j' \<and>* ps (v - (1 + int w)) \<and>* reps u (v - (1 + int w)) [k - Suc w]\<rbrace>" apply (simp add:reps.simps ones_rev) apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, clarsimp) apply (subgoal_tac " u + int (k - Suc w) = v - (1 + int w)", simp) defer apply simp by hstep my_block_end apply (hstep this) my_block fix i j have "\<lbrace>st i \<and>* ps (v - (1 + int w)) \<and>* reps u (v - (1 + int w)) [k - Suc w]\<rbrace> i :[ move_right ]: j \<lbrace>st j \<and>* ps (v - int w) \<and>* reps u (v - (1 + int w)) [k - Suc w] \<rbrace>" apply (simp add:reps.simps ones_rev) apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, clarsimp) apply (subgoal_tac " u + int (k - Suc w) = v - (1 + int w)", simp) defer apply simp by hstep my_block_end apply (hsteps this) my_block fix i j have "\<lbrace>st i \<and>* ps (v - int w) \<and>* one (v + 2) \<and>* zero (v - int w) \<and>* zeros (v - int w + 1) (v + 1)\<rbrace> i :[right_until_one]: j \<lbrace>st j \<and>* ps (v + 2) \<and>* one (v + 2) \<and>* zero (v - int w) \<and>* zeros (v - int w + 1) (v + 1)\<rbrace>" my_block have "(zero (v - int w) \<and>* zeros (v - int w + 1) (v + 1)) = (zeros (v - int w) (v + 1))" by (simp add:zeros_simps) my_block_end apply (unfold this) by hsteps my_block_end apply (hstep this) my_block from Suc(2, 3) have "w < k" by auto hence "(zeros (v + 3 + int w) (2 + (v + int k))) = (zero (v + 3 + int w) \<and>* zeros (4 + (v + int w)) (2 + (v + int k)))" by (simp add:zeros_simps) my_block_end apply (unfold this) my_block fix i j have "\<lbrace>st i \<and>* ps (v + 2) \<and>* zero (v + 3 + int w) \<and>* zeros (4 + (v + int w)) (2 + (v + int k)) \<and>* one (v + 2) \<and>* ones (v + 3) (v + 2 + int w)\<rbrace> i :[right_until_zero]: j \<lbrace>st j \<and>* ps (v + 3 + int w) \<and>* zero (v + 3 + int w) \<and>* zeros (4 + (v + int w)) (2 + (v + int k)) \<and>* one (v + 2) \<and>* ones (v + 3) (v + 2 + int w)\<rbrace>" my_block have "(one (v + 2) \<and>* ones (v + 3) (v + 2 + int w)) = (ones (v + 2) (v + 2 + int w))" by (simp add:ones_simps, smt) my_block_end apply (unfold this) by hsteps my_block_end apply (hsteps this, simp only:sep_conj_ac) apply (sep_cancel+, simp add:sep_conj_ac) my_block fix s assume "(zero (v - int w) \<and>* zeros (v - int w + 1) (v + 1)) s" hence "zeros (v - int w) (v + 1) s" by (simp add:zeros_simps) my_block_end apply (fwd this) my_block fix s assume "(one (v + 3 + int w) \<and>* ones (v + 3) (v + 2 + int w)) s" hence "ones (v + 3) (3 + (v + int w)) s" by (simp add:ones_rev sep_conj_ac, smt) my_block_end apply (fwd this) by (simp add:sep_conj_ac, smt)qeddefinition "cinit = (right_until_zero; move_right; write_one)"definition "copy = (cinit; cmove; move_right; move_right; right_until_one; move_left; move_left; cfill_until_one)"lemma hoare_copy: shows "\<lbrace>st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u v [k] \<and>* zero (v + 1) \<and>* zeros (v + 2) (v + int(reps_len [k]) + 1)\<rbrace> i :[copy]: j \<lbrace>st j \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u v [k] \<and>* zero (v + 1) \<and>* reps (v + 2) (v + int (reps_len [k]) + 1) [k]\<rbrace>" apply (unfold copy_def) my_block fix i j have "\<lbrace>st i \<and>* ps u \<and>* reps u v [k] \<and>* zero (v + 1) \<and>* zeros (v + 2) (v + int(reps_len [k]) + 1)\<rbrace> i :[cinit]: j \<lbrace>st j \<and>* ps (v + 2) \<and>* reps u v [k] \<and>* zero (v + 1) \<and>* one (v + 2) \<and>* zeros (v + 3) (v + int(reps_len [k]) + 1)\<rbrace>" apply (unfold cinit_def) apply (simp add:reps.simps) apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, simp) apply hsteps apply (simp add:sep_conj_ac) my_block have "(zeros (u + int k + 2) (u + int k + int (reps_len [k]) + 1)) = (zero (u + int k + 2) \<and>* zeros (u + int k + 3) (u + int k + int (reps_len [k]) + 1))" by (smt reps_len_sg zeros_step_simp) my_block_end apply (unfold this) apply hstep by (simp add:sep_conj_ac, sep_cancel+, smt) my_block_end apply (hstep this) apply (rule_tac p = "st j' \<and>* ps (v + 2) \<and>* reps u v [k] \<and>* zero (v + 1) \<and>* one (v + 2) \<and>* zeros (v + 3) (v + int (reps_len [k]) + 1) \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* <(v = u + int (reps_len [k]) - 1)> " in tm.pre_stren) my_block fix i j from hoare_cmove[where w = 0 and k = k and i = i and j = j and v = v and u = u] have "\<lbrace>st i \<and>* ps (v + 2) \<and>* zero (u - 1) \<and>* reps u v [k] \<and>* zero (v + 1) \<and>* one (v + 2) \<and>* zeros (v + 3) (v + int(reps_len [k]) + 1)\<rbrace> i :[cmove]: j \<lbrace>st j \<and>* ps (u - 1) \<and>* zero (u - 1) \<and>* reps u u [0] \<and>* zeros (u + 1) (v + 1) \<and>* reps (v + 2) (v + int (reps_len [k]) + 1) [k]\<rbrace>" by (auto simp:ones_simps zeros_simps) my_block_end apply (hstep this) apply (hstep, simp) my_block have "reps u u [0] = one u" by (simp add:reps.simps ones_simps) my_block_end my_note eq_repsz = this apply (unfold this) apply (hstep) apply (subst reps.simps, simp add: ones_simps) apply hsteps apply (subst sep_conj_cond)+ apply (rule tm.pre_condI, simp del:zeros.simps zeros_simps) apply (thin_tac "int (reps_len [k]) = 1 + int k \<and> v = u + int (reps_len [k]) - 1") my_block have "(zeros (u + 1) (u + int k + 1)) = (zeros (u + 1) (u + int k) \<and>* zero (u + int k + 1))" by (simp only:zeros_rev, smt) my_block_end apply (unfold this) apply (hstep, simp) my_block fix i j from hoare_cfill_until_one[where v = "u + int k" and u = "u + 1"] have "\<lbrace>st i \<and>* ps (u + int k) \<and>* one u \<and>* zeros (u + 1) (u + int k)\<rbrace> i :[ cfill_until_one ]: j \<lbrace>st j \<and>* ps u \<and>* ones u (u + int k) \<rbrace>" by simp my_block_end apply (hstep this, simp add:sep_conj_ac reps.simps ones_simps) apply (simp add:sep_conj_ac reps.simps ones_simps) apply (subst sep_conj_cond)+ apply (subst (asm) sep_conj_cond)+ apply (rule condI) apply (erule condE, simp) apply (simp add: reps_len_def reps_sep_len_def reps_ctnt_len_def) apply (sep_cancel+) by (erule condE, simp)end