# HG changeset patch # User Christian Urban # Date 1396530178 -3600 # Node ID 0352ad5ee9c5704d76d70515867c424abce5b6d6 # Parent e3ecf558aef254d512fdcc8709dfc676b2ff2955 added an attempt to change TMs to use FinFuns. diff -r e3ecf558aef2 -r 0352ad5ee9c5 thys/Hoare_tm2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/thys/Hoare_tm2.thy Thu Apr 03 14:02:58 2014 +0100 @@ -0,0 +1,5729 @@ +header {* + Separation logic for Turing Machines +*} + +theory Hoare_tm +imports Hoare_gen + My_block + Data_slot + "~~/src/HOL/Library/FinFun_Syntax" +begin + + +ML {* +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 simp + +lemma int_add_A : "(x + y) + z = x + (y + (z::int))" + by simp + +lemma int_add_LC: "x + (y + (z::int)) = y + (x + z)" + by simp + +lemmas int_add_ac = int_add_A int_add_C int_add_LC + + +section {* Operational Semantics of TM *} + +datatype taction = W0 | W1 | L | R + +type_synonym tstate = nat + +datatype Block = Oc | Bk + +(* the successor state when tape symbol is Bk or Oc, respectively *) +type_synonym tm_inst = "(taction \ tstate) \ (taction \ tstate)" + +(* - number of faults (nat) + - TM program (nat \ tm_inst) + - current state (nat) + - position of head (int) + - tape (int \ Block) +*) +type_synonym tconf = "nat \ (nat \f tm_inst option) \ nat \ int \ (int \f Block option)" + +(* updates the position/tape according to an action *) +fun + next_tape :: "taction \ (int \ (int \f Block option)) \ (int \ (int \f Block option))" +where + "next_tape W0 (pos, m) = (pos, m(pos $:= Some Bk))" | + "next_tape W1 (pos, m) = (pos, m(pos $:= Some Oc))" | + "next_tape L (pos, m) = (pos - 1, m)" | + "next_tape R (pos, m) = (pos + 1, m)" + +fun tstep :: "tconf \ tconf" + where "tstep (faults, prog, pc, pos, m) = + (case (prog $ pc) of + Some ((action0, pc0), (action1, pc1)) \ + case (m $ pos) of + Some Bk \ (faults, prog, pc0, next_tape action0 (pos, m)) | + Some Oc \ (faults, prog, pc1, next_tape action1 (pos, m)) | + None \ (faults + 1, prog, pc, pos, m) + | None \ (faults + 1, prog, pc, pos, m))" + +lemma tstep_splits: + "(P (tstep s)) = ((\ faults prog pc pos m action0 pc0 action1 pc1. + s = (faults, prog, pc, pos, m) \ + prog $ pc = Some ((action0, pc0), (action1, pc1)) \ + m $ pos = Some Bk \ P (faults, prog, pc0, next_tape action0 (pos, m))) \ + (\ faults prog pc pos m action0 pc0 action1 pc1. + s = (faults, prog, pc, pos, m) \ + prog $ pc = Some ((action0, pc0), (action1, pc1)) \ + m $ pos = Some Oc \ P (faults, prog, pc1, next_tape action1 (pos, m))) \ + (\ faults prog pc pos m action0 pc0 action1 pc1. + s = (faults, prog, pc, pos, m) \ + prog $ pc = Some ((action0, pc0), (action1, pc1)) \ + m $ pos = None \ P (faults + 1, prog, pc, pos, m)) \ + (\ faults prog pc pos m . + s = (faults, prog, pc, pos, m) \ + prog $ pc = None \ 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_def + +fun trset_of :: "tconf \ tresource set" + where "trset_of (faults, prog, pc, pos, m) = + tprog_set prog \ tpc_set pc \ tpos_set pos \ tmem_set m \ 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 \ tpg" + +notation TLocal (binder "TL " 10) + +abbreviation + tprog_instr :: "tm_inst \ tpg" ("\ _" [61] 61) +where "\ i \ TInstr i" + +abbreviation tprog_seq :: + "tpg \ tpg \ tpg" (infixr ";" 52) +where "c1 ; c2 \ TSeq c1 c2" + +definition "sg e = (\s. s = e)" + +type_synonym tassert = "tresource set \ bool" + +abbreviation + t_hoare :: "tassert \ tassert \ tassert \ bool" ("(\(1_)\/ (_)/ \(1_)\)" 50) +where + "\p\ c \q\ == sep_exec.Hoare_gen tstep trset_of p c q" + +abbreviation it_hoare :: + "('a::sep_algebra \ tresource set \ bool) \ ('a \ bool) \ (tresource set \ bool) \ ('a \ bool) \ bool" + ("(1_).(\(1_)\/ (_)/ \(1_)\)" 50) +where "I. \P\ c \Q\ == sep_exec.IHoare tstep trset_of I P c Q" + +(* +primrec tpg_len :: "tpg \ 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 \ nat \ nat \ 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 \ j = l)>" + +declare tassemble_to.simps [simp del] + +lemmas tasmp = tassemble_to.simps (2, 3, 4) + +abbreviation + tasmb_to :: "nat \ tpg \ nat \ tassert" ("_ :[ _ ]: _" [60, 60, 60] 60) + where + "i :[ tpg ]: j \ 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: "\ y s. \p y s\ \ y = x" + shows "p x = (EXS x. p x)" +proof + fix s + show "p x s = (EXS x. p x) s" + proof + assume "p x s" + thus "(EXS x. p x) s" by (auto simp:pred_ex_def) + next + assume "(EXS x. p x) s" + thus "p x s" + proof(rule EXS_elim) + fix y + assume "p y s" + from this[unfolded h1[OF this]] show "p x s" . + qed + qed +qed + +definition "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 \ []" + shows "tpg_fold (tpg#tpgs) = (tpg; (tpg_fold tpgs))" + using h +proof(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 + qed +qed auto + +lemmas tpg_fold_simps = tpg_fold_sg tpg_fold_cons + +lemma tpg_fold_app: + assumes h1: "tpgs1 \ []" + and h2: "tpgs2 \ []" + shows "i:[(tpg_fold (tpgs1 @ tpgs2))]:j = i:[(tpg_fold (tpgs1); tpg_fold tpgs2)]:j" + using h1 h2 +proof(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) \ []" + by (metis Cons.prems(2) Nil_is_append_conv) + have "?L = (i :[ tpg_fold (tpg1' # (tpgs1' @ tpgs2)) ]: j )" by simp + also have "\ = (i:[(tpg1'; (tpg_fold (tpgs1' @ tpgs2)))]:j )" + by (simp add:tpg_fold_cons[OF `(tpgs1' @ tpgs2) \ []`]) + also have "\ = ?R" + proof - + have "(EXS j'. i :[ tpg1' ]: j' \* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) = + (EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \* j'a :[ tpg_fold tpgs1' ]: j') \* + j' :[ tpg_fold tpgs2 ]: j)" + proof(default+) + fix s + assume "(EXS j'. i :[ tpg1' ]: j' \* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s" + thus "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \* j'a :[ tpg_fold tpgs1' ]: j') \* + j' :[ tpg_fold tpgs2 ]: j) s" + proof(elim EXS_elim) + fix j' + assume "(i :[ tpg1' ]: j' \* 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 \* j'a :[ tpg_fold tpgs1' ]: j') \* + 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 \* + j'a :[ tpg_fold tpgs1' ]: j') \* j' :[ tpg_fold tpgs2 ]: j) s" + (is "(EXS j'. (?P j' \* ?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' \* 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 \* ?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 \* j'a :[ tpg_fold tpgs1' ]: j') \* + j' :[ tpg_fold tpgs2 ]: j) s" + thus "(EXS j'. i :[ tpg1' ]: j' \* 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' \* 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' \* 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' \* + 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 \* 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 auto + + +subsection {* 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 \* q) s \ q (s - x) \ x \ 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 \* r) (trset_of (ft, prog, i', pos, mem)) \ i' = i" +proof - + assume "(st i \* r) (trset_of (ft, prog, i', pos, mem))" + from stimes_sgD [OF this[unfolded st_def], unfolded trset_of.simps] + have "tpc_set i \ tprog_set prog \ tpc_set i' \ tpos_set pos \ + tmem_set mem \ tfaults_set ft" by auto + thus ?thesis + by (unfold tpn_set_def, auto) +qed + +lemma psD: + "(ps p \* r) (trset_of (ft, prog, i', pos, mem)) \ 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 \ tprog_set prog \ tpc_set i' \ + tpos_set pos \ tmem_set mem \ tfaults_set ft" + by simp + thus ?thesis + by (unfold tpn_set_def, auto) +qed + +lemma codeD: "(st i ** sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem)) + \ 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 auto +qed + +lemma memD: "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem)) \ 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} \ {TC i inst |i inst. prog i = Some inst} \ {TAt i} \ + {TPos pos} \ {TM i n |i n. mem i = Some n} \ {TFaults ft}" by simp + thus ?thesis by auto +qed + +lemma t_hoare_seq: + assumes a1: "\ i j. \st i \* p\ i:[c1]:j \st j \* q\" + and a2: "\ j k. \st j ** q\ j:[c2]:k \st k ** r\" + shows "\st i \* p\ i:[(c1 ; c2)]:k \st k \* r\" +proof(subst tassemble_to.simps, rule tm.code_exI) + fix j' + show "\st i \* p\ i:[ c1 ]:j' \* j':[ c2 ]:k \st k \* r\" + proof(rule tm.composition) + from a1 show "\st i \* p\ i:[ c1 ]:j' \st j' \* q\" by auto + next + from a2 show "\st j' \* q\ j':[ c2 ]:k \st k \* r\" by auto + qed +qed + + +lemma t_hoare_seq1: + assumes a1: "\j'. \st i \* p\ i:[c1]:j' \st j' \* q\" + assumes a2: "\j'. \st j' \* q\ j':[c2]:k \st k' \* r\" + shows "\st i \* p\ i:[(c1 ; c2)]:k \st k' \* r\" +proof(subst tassemble_to.simps, rule tm.code_exI) + fix j' + show "\st i \* p\ i:[ c1 ]:j' \* j':[ c2 ]:k \st k' \* r\" + proof(rule tm.composition) + from a1 show "\st i \* p\ i:[ c1 ]:j' \st j' \* q\" by auto + next + from a2 show " \st j' \* q\ j':[ c2 ]:k \st k' \* r\" by auto + qed +qed + +lemma t_hoare_seq2: + assumes h: "\j. \st i ** p\ i:[c1]:j \st k' \* r\" + shows "\st i ** p\ i:[(c1 ; c2)]:j \st k' ** r\" + apply (unfold tassemble_to.simps, rule tm.code_exI) + by (rule tm.code_extension, rule h) + +lemma t_hoare_local: + assumes h: "(\l. \st i \* p\ i :[ c l ]: j \st k \* q\)" + shows "\st i ** p\ i:[TLocal c]:j \st k ** q\" using h + by (unfold tassemble_to.simps, intro tm.code_exI, simp) + +lemma t_hoare_label: + assumes "\l. l = i \ \st l \* p\ l:[ c l ]:j \st k \* q\" + shows "\st i \* p\ i:[(TLabel l; c l)]:j \st k \* q\" +using assms +by (unfold tassemble_to.simps, intro tm.code_exI tm.code_condI, clarify, auto) + +primrec t_split_cmd :: "tpg \ (tpg \ tpg option)" + where "t_split_cmd (\inst) = (\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) \ (TSeq c1 c21, Some c22) | + (c21, None) \ (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 simp + +lemma "t_blast_cmd (c1; c2; TLabel l) = (c1; c2)" + by simp + +lemma t_split_cmd_eq: + assumes "t_split_cmd c = (c1, Some c2)" + shows "i:[c]:j = i:[(c1; c2)]:j" + using assms +proof(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) + qed +qed auto + +lemma t_hoare_label_last_pre: + assumes h1: "t_split_cmd c = (c', Some (TLabel l))" + and h2: "l = j \ \p\ i:[c']:j \q\" + shows "\p\ i:[c]:j \q\" +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 \ \p\ i:[t_blast_cmd c]:j \q\" + shows "\p\ i:[c]:j \q\" +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 auto +qed + + +subsection {* Basic assertions for TM *} + +(* ones between tape position i and j *) +function ones :: "int \ int \ tassert" where + "ones i j = (if j < i then <(i = j + 1)> + else (one i) \* ones (i + 1) j)" +by auto + +termination + by (relation "measure(\ (i::int, j). nat (j - i + 1))") auto + +lemma ones_base_simp: + "j < i \ ones i j = <(i = j + 1)>" + by simp + +lemma ones_step_simp: + "\ j < i \ ones i j = ((one i) \* ones (i + 1) j)" + by simp + +lemmas ones_simps = ones_base_simp ones_step_simp + +declare ones.simps [simp del] ones_simps [simp] + +lemma ones_induct [case_names Base Step]: + assumes h1: "\ i j. j < i \ P i j (<(i = j + (1::int))>)" + and h2: "\ i j. \\ j < i; P (i + 1) j (ones (i + 1) j)\ \ P i j ((one i) \* ones (i + 1) j)" + shows "P i j (ones i j)" +proof(induct i j rule:ones.induct) + fix i j + assume ih: "(\ j < i \ 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 \* ones (i + 1) j)" by blast + with False show ?thesis by auto + qed +qed + +function ones' :: "int \ int \ tassert" where + "ones' i j = (if j < i then <(i = j + 1)> + else ones' i (j - 1) \* one j)" +by auto +termination by (relation "measure(\ (i::int, j). nat (j - i + 1))") auto + +lemma ones_rev: "\ j < i \ (ones i j) = ((ones i (j - 1)) ** one j)" +proof(induct i j rule:ones_induct) + case Base + thus ?case by auto +next + 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) + qed +qed + +lemma ones_rev_induct [case_names Base Step]: + assumes h1: "\ i j. j < i \ P i j (<(i = j + (1::int))>)" + and h2: "\ i j. \\ j < i; P i (j - 1) (ones i (j - 1))\ \ 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: "(\ j < i \ 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) \* one j)" by blast + with ones_rev and False + show ?thesis + by simp + qed +qed + +function zeros :: "int \ int \ tassert" where + "zeros i j = (if j < i then <(i = j + 1)> else + (zero i) ** zeros (i + 1) j)" +by auto +termination by (relation "measure(\ (i::int, j). nat (j - i + 1))") auto + +lemma zeros_base_simp: "j < i \ zeros i j = <(i = j + 1)>" + by simp + +lemma zeros_step_simp: "\ j < i \ zeros i j = ((zero i) ** zeros (i + 1) j)" + by simp + +declare zeros.simps [simp del] +lemmas zeros_simps [simp] = zeros_base_simp zeros_step_simp + +lemma zeros_induct [case_names Base Step]: + assumes h1: "\ i j. j < i \ P i j (<(i = j + (1::int))>)" + and h2: "\ i j. \\ j < i; P (i + 1) j (zeros (i + 1) j)\ \ + 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: "(\ j < i \ 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 \* zeros (i + 1) j)" by blast + with False show ?thesis by auto + qed +qed + +lemma zeros_rev: "\ j < i \ (zeros i j) = ((zeros i (j - 1)) \* zero j)" +proof(induct i j rule:zeros_induct) + case (Base i j) + thus ?case by auto +next + 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) + qed +qed + +lemma zeros_rev_induct [case_names Base Step]: + assumes h1: "\ i j. j < i \ P i j (<(i = j + (1::int))>)" + and h2: "\ i j. \\ j < i; P i (j - 1) (zeros i (j - 1))\ \ + 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: "(\ j < i \ 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) \* zero j)" by blast + with zeros_rev and False + show ?thesis by simp + qed +qed + +definition "rep i j k = ((ones i (i + (int k))) \* <(j = i + int k)>)" + +fun reps :: "int \ int \ nat list\ 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 \ [] \ + 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 \ 1 then 0 else (length ks) - 1)" + +definition "reps_ctnt_len ks = (\ k \ ks. (1 + k))" + +definition "reps_len ks = (reps_sep_len ks) + (reps_ctnt_len ks)" + +definition "splited xs ys zs = ((xs = ys @ zs) \ (ys \ []) \ (zs \ []))" + +lemma list_split: + assumes h: "k # ks = ys @ zs" + and h1: "ys \ []" + shows "(ys = [k] \ zs = ks) \ (\ ys'. ys' \ [] \ ys = k # ys' \ ks = ys' @ zs)" +proof(cases ys) + case Nil + with h1 show ?thesis by auto +next + 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 " \ys'. ys' \ [] \ ys = k # ys' \ ks = ys' @ zs" + proof(rule exI[where x = ys']) + from False hh Cons show "ys' \ [] \ ys = k # ys' \ ks = ys' @ zs" by auto + qed + qed + next + case True + show ?thesis + proof(rule disjI1) + from hh True Cons + show "ys = [k] \ zs = ks" by auto + qed + qed +qed + +lemma splited_cons[elim_format]: + assumes h: "splited (k # ks) ys zs" + shows "(ys = [k] \ zs = ks) \ (\ ys'. ys' \ [] \ ys = k # ys' \ splited ks ys' zs)" +proof - + from h have "k # ks = ys @ zs" "ys \ [] " unfolding splited_def by auto + from list_split[OF this] + have "ys = [k] \ zs = ks \ (\ys'. ys' \ [] \ ys = k # ys' \ ks = ys' @ zs)" . + thus ?thesis + proof + assume " ys = [k] \ zs = ks" thus ?thesis by auto + next + assume "\ys'. ys' \ [] \ ys = k # ys' \ ks = ys' @ zs" + then obtain ys' where hh: "ys' \ []" "ys = k # ys'" "ks = ys' @ zs" by auto + show ?thesis + proof(rule disjI2) + show "\ys'. ys' \ [] \ ys = k # ys' \ splited ks ys' zs" + proof(rule exI[where x = ys']) + from h have "zs \ []" 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' \ [] \ ys = k # ys' \ splited ks ys' zs" by auto + qed + qed + qed +qed + +lemma splited_cons_elim: + assumes h: "splited (k # ks) ys zs" + and h1: "\ys = [k]; zs = ks\ \ P" + and h2: "\ ys'. \ys' \ []; ys = k#ys'; splited ks ys' zs\ \ P" + shows P +proof(rule splited_cons[OF h]) + assume "ys = [k] \ zs = ks \ (\ys'. ys' \ [] \ ys = k # ys' \ splited ks ys' zs)" + thus P + proof + assume hh: "ys = [k] \ 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 "\ys'. ys' \ [] \ ys = k # ys' \ splited ks ys' zs" + then obtain ys' where hh: "ys' \ []" "ys = k # ys'" "splited ks ys' zs" by auto + from h2[OF this] + show P . + qed +qed + +lemma list_nth_expand: + "i < length xs \ 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 \ [] \ (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 auto + +lemma reps_len_correct: + assumes h: "(reps i j ks) s" + shows "j = i + int (reps_len ks) - 1" + using h +proof(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) + qed +qed + +lemma 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) +qed + +lemma reps_len_expand1: "(EXS j. (reps i j ks \* r)) = (reps i (i + int (reps_len ks) - 1) ks \* 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 \* + zero (i + int (reps_len ys)) \* + reps (i + int (reps_len ys) + 1) j zs)" + using h +proof(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' \ []" "ys = k # ys'" "splited ks ys' zs" + hence nnks: "ks \ []" + 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) + qed +qed + + +subsection {* 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 \ 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) +qed + +lemma 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 \ a \ (xs @ ys)!a = ys!(a - length xs)" + by (metis not_less nth_append) + + +lemma list_ext_tail: + assumes h1: "length xs \ a" + and h2: "length xs \ a'" + and h3: "a' \ 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 \ []" + 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) +qed + +lemmas list_ext_simps = list_ext_lt_get list_ext_lt list_ext_len list_ext_len_eq + +lemma listsum_upd_suc: + "a < length ks \ 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 \ 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) +qed + +lemma 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) +qed + +lemma ks_ext_len: + assumes h1: "(reps i j ks) s" + and h3: "length ks \ 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 auto +qed + +definition + "reps' i j ks = + (if ks = [] then (<(i = j + 1)>) else (reps i (j - 1) ks \* zero j))" + +lemma reps'_expand: + assumes h: "ks \ []" + 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 \* zero j) s" + by (simp add:reps'_def) + hence "(reps i (i + int (reps_len ks) - 1) ks \* zero (i + int (reps_len ks))) s" + proof(elim EXS_elim) + fix j + assume "(reps i (j - 1) ks \* 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 \* 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) + qed +qed + +lemma reps'_len_correct: + assumes h: "(reps' i j ks) s" + and h1: "ks \ []" + shows "(j = i + int (reps_len ks))" +proof - + from h1 have "reps' i j ks s = (reps i (j - 1) ks \* 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 simp +qed + +lemma reps'_append: + "reps' i j (ks1 @ ks2) = (EXS m. (reps' i (m - 1) ks1 \* 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 \ []` and `ks2 \ []` + 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 \* + zero (i + int (reps_len ks1)) \* + reps (i + int (reps_len ks1) + 1) (j - 1) ks2)" . + from `ks1 \ []` + have eq_2: "reps' i j (ks1 @ ks2) = (reps i (j - 1) (ks1 @ ks2) \* 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 \* 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 \ []` `ks2 \ []` + show "(reps' i (i + int (reps_len ks1) + 1 - 1) ks1 \* + 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 \* reps' m j ks2) s" + thus "reps' i j (ks1 @ ks2) s" + proof(elim EXS_elim) + fix m + assume "(reps' i (m - 1) ks1 \* 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 \ []`] + have eq_m: "m = i + int (reps_len ks1) + 1" by simp + have "((reps i (i + int (reps_len ks1) - 1) ks1 \* zero (i + int (reps_len ks1))) \* + ((reps (i + int (reps_len ks1) + 1) (j - 1) ks2) \* zero j)) s" + (is "(?P \* ?Q) s") + proof(rule sep_conjI) + from h(3) eq_m `ks1 \ []` show "?P s1" + by (simp add:reps'_def) + next + from h(4) eq_m `ks2 \ []` 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 \ []` 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) + qed +qed + +lemma reps'_sg: + "reps' i j [k] = + (<(j = i + int k + 1)> \* ones i (i + int k) \* 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. \((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 \ tpc_set i' \ tpos_set y \ tmem_set z \ tfaults_set f - tpc_set i')" + by blast + moreover have + "(tprog_set x \ tpc_set i' \ tpos_set y \ tmem_set z \ tfaults_set f - tpc_set i') = + (tprog_set x \ tpos_set y \ tmem_set z \ tfaults_set f)" + by (unfold tpn_set_def, auto) + ultimately have r_rest: "r (tprog_set x \ tpos_set y \ tmem_set z \ 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 \ tpos_set y \ tmem_set z \ 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 \ tpos_set y \ tmem_set z \ tfaults_set f)" + by (unfold trset_of.simps plus_set_def, auto) + qed +qed + +lemma 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 \ tpc_set y \ tpos_set i \ tmem_set z \ + tfaults_set f - tpos_set i)" (is "r ?xs") + by blast + moreover have + "?xs = tprog_set x \ tpc_set y \ tmem_set z \ tfaults_set f" + by (unfold tpn_set_def, auto) + ultimately have r_rest: "r \" + 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 \ tpc_set y \ tmem_set z \ 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 \ tpc_set y \ tmem_set z \ tfaults_set f)" + by (unfold trset_of.simps plus_set_def, auto) + qed +qed + +lemma TM_in_simp: "({TM a v} \ + tprog_set x \ tpc_set y \ tpos_set z \ tmem_set mem \ tfaults_set f) = + ({TM a v} \ tmem_set mem)" + by (unfold tpn_set_def, auto) + +lemma tmem_set_upd: + "{TM a v} \ tmem_set mem \ + tmem_set (mem(a:=Some v')) = ((tmem_set mem) - {TM a v}) \ {TM a v'}" + by (unfold tpn_set_def, auto) + +lemma tmem_set_disj: "{TM a v} \ tmem_set mem \ + {TM a v'} \ (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)) \ + ((tm a v') ** r) (trset_of (f, x, y, z, mem(a := Some v')))" +proof - + have eq_s: "(tprog_set x \ tpc_set y \ tpos_set z \ tmem_set mem \ tfaults_set f - {TM a v}) = + (tprog_set x \ tpc_set y \ tpos_set z \ (tmem_set mem - {TM a v}) \ tfaults_set f)" + by (unfold tpn_set_def, auto) + assume g: "(tm a v \* r) (trset_of (f, x, y, z, mem))" + from this[unfolded trset_of.simps tm_def] + have h: "(sg {TM a v} \* r) (tprog_set x \ tpc_set y \ tpos_set z \ tmem_set mem \ tfaults_set f)" . + hence h0: "r (tprog_set x \ tpc_set y \ tpos_set z \ (tmem_set mem - {TM a v}) \ tfaults_set f)" + by(sep_drule stimes_sgD, clarify, unfold eq_s, auto) + from h TM_in_simp have "{TM a v} \ 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 \ v')) = {TM a v'} \ (tmem_set mem - {TM a v})" + "{TM a v'} \ (tmem_set mem - {TM a v}) = {}" by auto + show ?thesis + proof - + have "(tm a v' ** r) (tmem_set (mem(a \ v')) \ tprog_set x \ tpc_set y \ tpos_set z \ 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 \ tpc_set y \ tpos_set z \ (tmem_set mem - {TM a v}) \ tfaults_set f)" . + next + show "{TM a v'} ## tprog_set x \ tpc_set y \ tpos_set z \ (tmem_set mem - {TM a v}) \ 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 \ v')) \ tprog_set x \ tpc_set y \ tpos_set z \ tfaults_set f = + {TM a v'} + (tprog_set x \ tpc_set y \ tpos_set z \ (tmem_set mem - {TM a v}) \ 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) + qed +qed + +lemma hoare_write_zero: + "\st i ** ps p ** tm p v\ + i:[write_zero]:j + \st j ** ps p ** tm p Bk\" +proof(unfold write_zero_def, intro t_hoare_local, rule t_hoare_label_last, simp, simp) + show "\st i \* ps p \* tm p v\ i :[ \ ((W0, j), W0, j) ]: j \st j \* ps p \* tm p Bk\" + proof(unfold tassemble_to.simps, simp only:sep_conj_cond, + intro tm.code_condI, simp) + assume eq_j: "j = Suc i" + show "\st i \* ps p \* tm p v\ sg {TC i ((W0, Suc i), W0, Suc i)} + \st (Suc i) \* ps p \* tm p Bk\" + 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 \* ps p \* st i \* tm p v \* 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 \* ps p \* 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'\ 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 \* ps p \* st j \* tm p Bk \* 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 "\k. (r \* ps p \* st j \* tm p Bk \* 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 + qed +qed + +lemma hoare_write_zero_gen[step]: + assumes "p = q" + shows "\st i ** ps p ** tm q v\ + i:[write_zero]:j + \st j ** ps p ** tm q Bk\" + by (unfold assms, rule hoare_write_zero) + +definition "write_one = (TL exit. \((W1, exit), (W1, exit)); TLabel exit)" + +lemma hoare_write_one: + "\st i ** ps p ** tm p v\ + i:[write_one]:j + \st j ** ps p ** tm p Oc\" +proof(unfold write_one_def, intro t_hoare_local, rule t_hoare_label_last, simp+) + fix l + show "\st i \* ps p \* tm p v\ i :[ \ ((W1, j), W1, j) ]: j \st j \* ps p \* tm p Oc\" + 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 "\ps p \* st i \* tm p v\ sg {TC i ((W1, ?j), W1, ?j)} + \ps p \* st ?j \* tm p Oc\" + proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) + fix ft prog cs i' mem r + assume h: "(r \* ps p \* st i \* tm p v \* 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 \* ps p \* 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'\ 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 \* ps p \* st ?j \* tm p Oc \* 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 "\k. (r \* ps p \* st ?j \* tm p Oc \* 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 + qed +qed + +lemma hoare_write_one_gen[step]: + assumes "p = q" + shows "\st i ** ps p ** tm q v\ + i:[write_one]:j + \st j ** ps p ** tm q Oc\" + by (unfold assms, rule hoare_write_one) + +definition "move_left = (TL exit . \((L, exit), (L, exit)); TLabel exit)" + +lemma hoare_move_left: + "\st i ** ps p ** tm p v2\ + i:[move_left]:j + \st j ** ps (p - 1) ** tm p v2\" +proof(unfold move_left_def, intro t_hoare_local, rule t_hoare_label_last, simp+) + fix l + show "\st i \* ps p \* tm p v2\ i :[ \ ((L, l), L, l) ]: l + \st l \* ps (p - 1) \* tm p v2\" + proof(unfold tassemble_to.simps, simp only:sep_conj_cond, + intro tm.code_condI, simp add: sep_conj_ac) + let ?j = "Suc i" + show "\ps p \* st i \* tm p v2\ sg {TC i ((L, ?j), L, ?j)} + \st ?j \* tm p v2 \* ps (p - 1)\" + proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) + fix ft prog cs i' mem r + assume h: "(r \* ps p \* st i \* tm p v2 \* 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 \* ps p \* 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 \* st ?j \* tm p v2 \* ps (p - 1) \* 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 \* ps (p - 1) \* r \* tm p v2 \* sg {TC i ((L, ?j), L, ?j)}) + (trset_of (ft, prog, ?j, p - 1, mem))" + thus "(r \* st ?j \* tm p v2 \* ps (p - 1) \* sg {TC i ((L, ?j), L, ?j)}) + (trset_of (ft, prog, ?j, p - 1, mem))" + by(simp add: sep_conj_ac) + qed + thus "\k. (r \* st ?j \* tm p v2 \* ps (p - 1) \* 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 + qed +qed + +lemma hoare_move_left_gen[step]: + assumes "p = q" + shows "\st i ** ps p ** tm q v2\ + i:[move_left]:j + \st j ** ps (p - 1) ** tm q v2\" + by (unfold assms, rule hoare_move_left) + +definition "move_right = (TL exit . \((R, exit), (R, exit)); TLabel exit)" + +lemma hoare_move_right: + "\st i ** ps p ** tm p v1 \ + i:[move_right]:j + \st j ** ps (p + 1) ** tm p v1 \" +proof(unfold move_right_def, intro t_hoare_local, rule t_hoare_label_last, simp+) + fix l + show "\st i \* ps p \* tm p v1\ i :[ \ ((R, l), R, l) ]: l + \st l \* ps (p + 1) \* tm p v1\" + proof(unfold tassemble_to.simps, simp only:sep_conj_cond, + intro tm.code_condI, simp add: sep_conj_ac) + let ?j = "Suc i" + show "\ps p \* st i \* tm p v1\ sg {TC i ((R, ?j), R, ?j)} + \st ?j \* tm p v1 \* ps (p + 1)\" + proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) + fix ft prog cs i' mem r + assume h: "(r \* ps p \* st i \* tm p v1 \* 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 \* ps p \* 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 \* st ?j \* tm p v1 \* ps (p + 1) \* + 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 \* ps (p + 1) \* r \* tm p v1 \* sg {TC i ((R, ?j), R, ?j)}) + (trset_of (ft, prog, ?j, p + 1, mem))" + thus "(r \* st ?j \* tm p v1 \* ps (p + 1) \* sg {TC i ((R, ?j), R, ?j)}) + (trset_of (ft, prog, ?j, p + 1, mem))" + by (simp add: sep_conj_ac) + qed + thus "\k. (r \* st ?j \* tm p v1 \* ps (p + 1) \* 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 + qed +qed + +lemma hoare_move_right_gen[step]: + assumes "p = q" + shows "\st i ** ps p ** tm q v1 \ + i:[move_right]:j + \st j ** ps (p + 1) ** tm q v1 \" + by (unfold assms, rule hoare_move_right) + +definition "if_one e = (TL exit . \((W0, exit), (W1, e)); TLabel exit)" + +lemma hoare_if_one_true: + "\st i ** ps p ** one p\ + i:[if_one e]:j + \st e ** ps p ** one p\" +proof(unfold if_one_def, intro t_hoare_local, rule t_hoare_label_last, simp+) + fix l + show " \st i \* ps p \* one p\ i :[ \ ((W0, l), W1, e) ]: l \st e \* ps p \* one p\" + proof(unfold tassemble_to.simps, simp only:sep_conj_cond, + intro tm.code_condI, simp add: sep_conj_ac) + let ?j = "Suc i" + show "\one p \* ps p \* st i\ sg {TC i ((W0, ?j), W1, e)} \one p \* ps p \* st e\" + proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) + fix ft prog cs pc mem r + assume h: "(r \* one p \* ps p \* st i \* 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 \* one p \* 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 \* one p \* ps p \* st e \* sg {TC i ((W0, ?j), W1, e)}) (trset_of ?x)" + apply(unfold stp) + by(sep_drule st_upd, simp add: sep_conj_ac) + thus "\k.(r \* one p \* ps p \* st e \* 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 + qed +qed + +text {* + The following problematic lemma is not provable now + lemma hoare_self: "\p\ i :[ap]: j \p\" + 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 + "\st i ** ps p ** one q\ + i:[if_one e]:j + \st e ** ps p ** one q\" + by (unfold assms, rule hoare_if_one_true) + +lemma hoare_if_one_true1: + "\st i ** ps p ** one p\ + i:[(if_one e; c)]:j + \st e ** ps p ** one p\" +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 \* one p \* ps p \* st i \* j' :[ c ]: j \* i :[ if_one e ]: j') + (trset_of (ft, prog, cs, pos, mem))" + from tm.frame_rule[OF hoare_if_one_true] + have "\ r. \st i \* ps p \* one p \* r\ i :[ if_one e ]: j' \st e \* ps p \* one p \* r\" + by(simp add: sep_conj_ac) + from this[unfolded tm.Hoare_gen_def tassemble_to.simps, rule_format, of "j' :[ c ]: j"] h + have "\ k. (r \* one p \* ps p \* st e \* i :[ if_one e ]: j' \* j' :[ c ]: j) + (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" + by(auto simp: sep_conj_ac) + thus "\k. (r \* one p \* ps p \* st e \* j' :[ c ]: j \* i :[ if_one e ]: j') + (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" + by(simp add: sep_conj_ac) +qed + +lemma hoare_if_one_true1_gen[step]: + assumes "p = q" + shows + "\st i ** ps p ** one q\ + i:[(if_one e; c)]:j + \st e ** ps p ** one q\" + by (unfold assms, rule hoare_if_one_true1) + +lemma hoare_if_one_false: + "\st i ** ps p ** zero p\ + i:[if_one e]:j + \st j ** ps p ** zero p\" +proof(unfold if_one_def, intro t_hoare_local, rule t_hoare_label_last, simp+) + show "\st i \* ps p \* zero p\ i :[ (\ ((W0, j), W1, e)) ]: j + \st j \* ps p \* zero p\" + proof(unfold tassemble_to.simps, simp only:sep_conj_cond, + intro tm.code_condI, simp add: sep_conj_ac) + let ?j = "Suc i" + show "\ps p \* st i \* zero p\ sg {TC i ((W0, ?j), W1, e)} \ps p \* zero p \* st ?j \" + proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) + fix ft prog cs pc mem r + assume h: "(r \* ps p \* st i \* zero p \* 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 \* zero p \* 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 \* zero p \* ps p \* st ?j \* 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 "\k. (r \* ps p \* zero p \* st ?j \* 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 + qed +qed + +lemma hoare_if_one_false_gen[step]: + assumes "p = q" + shows "\st i ** ps p ** zero q\ + i:[if_one e]:j + \st j ** ps p ** zero q\" + by (unfold assms, rule hoare_if_one_false) + +definition "if_zero e = (TL exit . \((W0, e), (W1, exit)); TLabel exit)" + +lemma hoare_if_zero_true: + "\st i ** ps p ** zero p\ + i:[if_zero e]:j + \st e ** ps p ** zero p\" +proof(unfold if_zero_def, intro t_hoare_local, rule t_hoare_label_last, simp+) + fix l + show "\st i \* ps p \* zero p\ i :[ \ ((W0, e), W1, l) ]: l \st e \* ps p \* zero p\" + proof(unfold tassemble_to.simps, simp only:sep_conj_cond, + intro tm.code_condI, simp add: sep_conj_ac) + let ?j = "Suc i" + show "\ps p \* st i \* zero p\ sg {TC i ((W0, e), W1, ?j)} \ps p \* st e \* zero p\" + proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) + fix ft prog cs pc mem r + assume h: "(r \* ps p \* st i \* zero p \* 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 \* zero p \* 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 \* zero p \* ps p \* st e \* sg {TC i ((W0, e), W1, ?j)}) (trset_of ?x)" + apply(unfold stp) + by(sep_drule st_upd, simp add: sep_conj_ac) + thus "\k. (r \* ps p \* st e \* zero p \* 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 + qed +qed + +lemma hoare_if_zero_true_gen[step]: + assumes "p = q" + shows + "\st i ** ps p ** zero q\ + i:[if_zero e]:j + \st e ** ps p ** zero q\" + by (unfold assms, rule hoare_if_zero_true) + +lemma hoare_if_zero_true1: + "\st i ** ps p ** zero p\ + i:[(if_zero e; c)]:j + \st e ** ps p ** zero p\" + 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 \* ps p \* st i \* zero p \* j' :[ c ]: j \* i :[ if_zero e ]: j') + (trset_of (ft, prog, cs, pos, mem))" + from tm.frame_rule[OF hoare_if_zero_true] + have "\ r. \st i \* ps p \* zero p \* r\ i :[ if_zero e ]: j' \st e \* ps p \* zero p \* r\" + by(simp add: sep_conj_ac) + from this[unfolded tm.Hoare_gen_def tassemble_to.simps, rule_format, of "j' :[ c ]: j"] h + have "\ k. (r \* zero p \* ps p \* st e \* i :[ if_zero e ]: j' \* j' :[ c ]: j) + (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" + by(auto simp: sep_conj_ac) + thus "\k. (r \* ps p \* st e \* zero p \* j' :[ c ]: j \* i :[ if_zero e ]: j') + (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" + by(simp add: sep_conj_ac) +qed + +lemma hoare_if_zero_true1_gen[step]: + assumes "p = q" + shows + "\st i ** ps p ** zero q\ + i:[(if_zero e; c)]:j + \st e ** ps p ** zero q\" + by (unfold assms, rule hoare_if_zero_true1) + +lemma hoare_if_zero_false: + "\st i ** ps p ** tm p Oc\ + i:[if_zero e]:j + \st j ** ps p ** tm p Oc\" +proof(unfold if_zero_def, intro t_hoare_local, rule t_hoare_label_last, simp, simp) + fix l + show "\st i \* ps p \* tm p Oc\ i :[ \ ((W0, e), W1, l) ]: l + \st l \* ps p \* tm p Oc\" + proof(unfold tassemble_to.simps, simp only:sep_conj_cond, + intro tm.code_condI, simp add: sep_conj_ac) + let ?j = "Suc i" + show "\ps p \* st i \* tm p Oc\ sg {TC i ((W0, e), W1, ?j)} + \ps p \* st ?j \* tm p Oc\" + proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify) + fix ft prog cs pc mem r + assume h: "(r \* ps p \* st i \* tm p Oc \* 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 \* tm p Oc \* 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 \* tm p Oc \* ps p \* st ?j \* sg {TC i ((W0, e), W1, ?j)}) (trset_of ?x)" + apply(unfold stp) + by(sep_drule st_upd, simp add: sep_conj_ac) + thus "\k. (r \* ps p \* st ?j \* tm p Oc \* 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 + qed +qed + +lemma hoare_if_zero_false_gen[step]: + assumes "p = q" + shows + "\st i ** ps p ** tm q Oc\ + i:[if_zero e]:j + \st j ** ps p ** tm q Oc\" + by (unfold assms, rule hoare_if_zero_false) + + +definition "jmp e = \((W0, e), (W1, e))" + +lemma hoare_jmp: + "\st i \* ps p \* tm p v\ i:[jmp e]:j \st e \* ps p \* tm p v\" +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 \* ps p \* st i \* tm p v \* <(j = i + 1)> \* 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 \* <(j = i + 1)> \* tm p v \* 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 \* ps p \* st e \* tm p v \* <(j = i + 1)> \* + sg {TC i ((W0, e), W1, e)}) (trset_of ?x)" + apply(unfold stp) + by(sep_drule st_upd, simp add: sep_conj_ac) + thus "\ k. (r \* ps p \* st e \* tm p v \* <(j = i + 1)> \* 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 auto +qed + +lemma hoare_jmp_gen[step]: + assumes "p = q" + shows "\st i \* ps p \* tm q v\ i:[jmp e]:j \st e \* ps p \* tm q v\" + by (unfold assms, rule hoare_jmp) + +lemma hoare_jmp1: + "\st i \* ps p \* tm p v\ + i:[(jmp e; c)]:j + \st e \* ps p \* tm p v\" +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 \* ps p \* st i \* tm p v \* j' :[ c ]: j \* i :[ jmp e ]: j') + (trset_of (ft, prog, cs, pos, mem))" + from tm.frame_rule[OF hoare_jmp] + have "\ r. \st i \* ps p \* tm p v \* r\ i :[ jmp e ]: j' \st e \* ps p \* tm p v \* r\" + by(simp add: sep_conj_ac) + from this[unfolded tm.Hoare_gen_def tassemble_to.simps, rule_format, of "j' :[ c ]: j"] h + have "\ k. (r \* tm p v \* ps p \* st e \* i :[ jmp e ]: j' \* j' :[ c ]: j) + (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" + by(auto simp: sep_conj_ac) + thus "\k. (r \* ps p \* st e \* tm p v \* j' :[ c ]: j \* i :[ jmp e ]: j') + (trset_of (tm.run (Suc k) (ft, prog, cs, pos, mem)))" + by(simp add: sep_conj_ac) +qed + + +lemma hoare_jmp1_gen[step]: + assumes "p = q" + shows "\st i \* ps p \* tm q v\ + i:[(jmp e; c)]:j + \st e \* ps p \* tm q v\" + by (unfold assms, rule hoare_jmp1) + + +lemma condI: + assumes h1: b + and h2: "b \ p s" + shows "( \* p) s" + by (metis (full_types) cond_true_eq1 h1 h2) + +lemma condE: + assumes "( \* p) s" + obtains "b" and "p s" +proof(atomize_elim) + from condD[OF assms] + show "b \ p s" . +qed + + +section {* 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 "\?P\ ?c \?Q\"} + val env = match ctxt pat t + in inst env (term_of @{cpat "?P::tresource set \ 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 "\?P\ ?c \?Q\"} + val env = match ctxt pat t + in inst env (term_of @{cpat "?Q::tresource set \ bool"}) end; + + fun get_mid ctxt t = + let val pat = term_of @{cpat "\?P\ ?c \?Q\"} + val env = match ctxt pat t + in inst env (term_of @{cpat "?c::tresource set \ 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 \ tresource set \ bool"}) $ Free (x, @{typ "nat"}) + + val sconj_term = term_of @{cterm "sep_conj::tassert \ tassert \ tassert"} + + fun mk_ps_term x = + Const (@{const_name ps}, @{typ "int \ tresource set \ 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'') end + +fun 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_context +in + rule +end +*} + +lemma fwd_rule: + assumes "\ s . U s \ V s" + shows "(U ** RR) s \ (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 state +end +*} + +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 \* 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: "\ x s. (ones (i + 1) j \* ones (j + 1) x) s \ ones (i + 1) x s" + by metis + hence "(ones (i + 1) x \* 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) +qed + +lemma one_abs: "(one m) s \ (ones m m) s" + by (smt cond_true_eq2 ones.simps) + +lemma ones_reps_abs: + assumes "ones m n s" + "m \ n" + shows "(reps m n [nat (n - m)]) s" + using assms + by simp + +lemma reps_reps'_abs: + assumes "(reps m n xs \* zero u) s" "u = n + 1" "xs \ []" + shows "(reps' m u xs) s" + unfolding assms using assms + by (unfold reps'_def, simp) + +lemma reps'_abs: + assumes "(reps' m n xs \* 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_abs + +lemmas abs_reps' = ones_reps_abs reps_reps'_abs reps'_abs + + +section {* 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 \ (ones i j) = sep_false" + by (simp add:pasrt_def) + +lemma hoare_right_until_zero: + "\st i ** ps u ** ones u (v - 1) ** zero v \ + i:[right_until_zero]:j + \st j ** ps v ** ones u (v - 1) ** zero v \" +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 "\st i \* ps u \* ones u (v - 1) \* zero v\ ?body + \st ?j \* ps v \* ones u (v - 1) \* zero v\" (is "?P u (v - 1) (ones u (v - 1))") + proof(induct "u" "v - 1" rule:ones_induct) + case (Base k) + moreover have "\st i \* ps v \* zero v\ ?body + \st ?j \* ps v \* zero v\" by hsteps + ultimately show ?case by (auto intro!:tm.pre_condI simp:sep_conj_cond) + next + case (Step k) + moreover have "\st i \* ps k \* (one k \* ones (k + 1) (v - 1)) \* zero v\ + i :[ (if_zero ?j ; move_right ; jmp i) ]: ?j + \st ?j \* ps v \* (one k \* ones (k + 1) (v - 1)) \* zero v\" + proof - + have s1: "\st i \* ps k \* (one k \* ones (k + 1) (v - 1)) \* zero v\ + ?body + \st i \* ps (k + 1) \* one k \* ones (k + 1) (v - 1) \* zero v\" + proof(cases "k + 1 \ 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) \* ones ((k + 1) + 1) (v - 1))" + by simp + show ?thesis + apply(simp only: eq_ones) + by hsteps + qed + note Step(2)[step] + have s2: "\st i \* ps (k + 1) \* one k \* ones (k + 1) (v - 1) \* zero v\ + ?body + \st ?j \* ps v \* one k \* ones (k + 1) (v - 1) \* zero v\" + by hsteps + from tm.sequencing [OF s1 s2, step] + show ?thesis + by (auto simp:sep_conj_ac) + qed + ultimately show ?case by simp + qed +qed + +lemma hoare_right_until_zero_gen[step]: + assumes "u = v" "w = x - 1" + shows "\st i ** ps u ** ones v w ** zero x \ + i:[right_until_zero]:j + \st j ** ps x ** ones v w ** zero x \" + 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: + "\st i ** ps v ** zero u ** ones (u + 1) v \ + i:[left_until_zero]:j + \st j ** ps u ** zero u ** ones (u + 1) v \" +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 "\st i \* ps v \* zero u \* ones (u + 1) v\ ?body + \st ?j \* ps u \* zero u \* ones (u + 1) v\" + 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 "\st i \* ps k \* zero u \* ones (u + 1) (k - 1) \* one k\ + ?body + \st ?j \* ps u \* zero u \* ones (u + 1) (k - 1) \* one k\" + proof(rule tm.sequencing[where q = + "st i \* ps (k - 1) \* zero u \* ones (u + 1) (k - 1) \* one k"]) + show "\st i \* ps k \* zero u \* ones (u + 1) (k - 1) \* one k\ + ?body + \st i \* ps (k - 1) \* zero u \* ones (u + 1) (k - 1) \* one k\" + 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 "\st i \* ps (k - 1) \* zero u \* ones (u + 1) (k - 1) \* one k\ + ?body + \st ?j \* ps u \* zero u \* ones (u + 1) (k - 1) \* one k\" by hsteps + qed + thus ?case by (unfold ones_rev[OF Step(1)], simp) + qed +qed + +lemma hoare_left_until_zero_gen[step]: + assumes "u = x" "w = v + 1" + shows "\st i ** ps u ** zero v ** ones w x \ + i:[left_until_zero]:j + \st j ** ps v ** zero v ** ones w x \" + 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: + "\st i ** ps u ** zeros u (v - 1) ** one v \ + i:[right_until_one]:j + \st j ** ps v ** zeros u (v - 1) ** one v \" +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 "\st i \* ps u \* zeros u (v - 1) \* one v\ ?body + \st ?j \* ps v \* zeros u (v - 1) \* one v\" + 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 "\st i \* ps k \* zero k \* zeros (k + 1) (v - 1) \* one v\ + ?body + \st ?j \* ps v \* zero k \* zeros (k + 1) (v - 1) \* one v\" + proof(rule tm.sequencing[where q = + "st i \* ps (k + 1) \* zero k \* zeros (k + 1) (v - 1) \* one v"]) + show "\st i \* ps k \* zero k \* zeros (k + 1) (v - 1) \* one v\ + ?body + \st i \* ps (k + 1) \* zero k \* zeros (k + 1) (v - 1) \* one v\" + 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 "\st i \* ps (k + 1) \* zero k \* zeros (k + 1) (v - 1) \* one v\ + ?body + \st ?j \* ps v \* zero k \* zeros (k + 1) (v - 1) \* one v\" + by hsteps + qed + thus ?case by (auto simp: sep_conj_ac Step(1)) + qed +qed + +lemma hoare_right_until_one_gen[step]: + assumes "u = v" "w = x - 1" + shows + "\st i ** ps u ** zeros v w ** one x \ + i:[right_until_one]:j + \st j ** ps x ** zeros v w ** one x \" + 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: + "\st i ** ps v ** one u ** zeros (u + 1) v \ + i:[left_until_one]:j + \st j ** ps u ** one u ** zeros (u + 1) v \" +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 "\st i \* ps v \* one u \* zeros (u + 1) v\ ?body + \st ?j \* ps u \* one u \* zeros (u + 1) v\" + proof(induct u v rule: ones'.induct) + fix ia ja + assume h: "\ ja < ia \ + \st i \* ps (ja - 1) \* one ia \* zeros (ia + 1) (ja - 1)\ ?body + \st ?j \* ps ia \* one ia \* zeros (ia + 1) (ja - 1)\" + show "\st i \* ps ja \* one ia \* zeros (ia + 1) ja\ ?body + \st ?j \* ps ia \* one ia \* zeros (ia + 1) ja\" + proof(cases "ja < ia") + case False + note lt = False + from h[OF this] have [step]: + "\st i \* ps (ja - 1) \* one ia \* zeros (ia + 1) (ja - 1)\ ?body + \st ?j \* ps ia \* one ia \* zeros (ia + 1) (ja - 1)\" . + show ?thesis + proof(cases "ja = ia") + case True + moreover + have "\st i \* ps ja \* one ja\ ?body \st ?j \* ps ja \* one ja\" + 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) \* zero ja)" + by simp + have s1: "\st i \* ps ja \* one ia \* zeros (ia + 1) (ja - 1) \* zero ja\ + ?body + \st i \* ps (ja - 1) \* one ia \* zeros (ia + 1) (ja - 1) \* zero ja\" + proof(cases "ia + 1 \ ja") + case True + from k1 True have "ja = ia + 1" by arith + moreover have "\st i \* ps (ia + 1) \* one (ia + 1 - 1) \* zero (ia + 1)\ + i :[ (if_one ?j ; move_left ; jmp i) ]: ?j + \st i \* ps (ia + 1 - 1) \* one (ia + 1 - 1) \* zero (ia + 1)\" + 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) \* zero (ja - 1))" + by auto + show ?thesis + apply (unfold k, simp) + by hsteps + qed + have s2: "\st i \* ps (ja - 1) \* one ia \* zeros (ia + 1) (ja - 1) \* zero ja\ + ?body + \st ?j \* ps ia \* one ia \* zeros (ia + 1) (ja - 1) \* zero ja\" + 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 + qed +qed + +lemma hoare_left_until_one_gen[step]: + assumes "u = x" "w = v + 1" + shows "\st i ** ps u ** one v ** zeros w x \ + i:[left_until_one]:j + \st j ** ps v ** one v ** zeros w x \" + 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 \ [] \ + 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 \ r = s" + shows "( ** r) = ( ** s)" +proof(cases b) + case True + from h[OF this] show ?thesis by simp +next + case False + thus ?thesis + by (unfold sep_conj_def set_ins_def pasrt_def, auto) +qed + +lemma reps_rev: "ks \ [] + \ reps i j (ks @ [k]) = (reps i (j - int (k + 1) - 1 ) ks \* + zero (j - int (k + 1)) \* ones (j - int k) j)" +proof(induct ks arbitrary: i j) + case Nil + thus ?case by simp +next + 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)> \* + one i \* ones (i + 1) (i + int a) \* + zero (i + int a + 1) \* one (i + int a + 2) \* ones (3 + (i + int a)) (i + int a + 2 + int k)) + = + (<(-2 + (j - int k) = i + int a)> \* one i \* ones (i + 1) (i + int a) \* + zero (j - (1 + int k)) \* one (j - int k) \* ones (j - int k + 1) j)" + (is "( \* ?L) = ( \* ?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) + qed +qed + +lemma hoare_if_one_reps: + assumes nn: "ks \ []" + shows "\st i ** ps v ** reps u v ks\ + i:[if_one e]:j + \st e ** ps v ** reps u v ks\" +proof(rule rev_exhaust[of ks]) + assume "ks = []" with nn show ?thesis by simp +next + fix y ys + assume eq_ks: "ks = ys @ [y]" + show " \st i \* ps v \* reps u v ks\ i :[ if_one e ]: j \st e \* ps v \* reps u v ks\" + proof(cases "ys = []") + case False + have "\st i \* ps v \* reps u v (ys @ [y])\ i :[ if_one e ]: j \st e \* ps v \* reps u v (ys @ [y])\" + 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 + qed +qed + +lemma hoare_if_one_reps_gen[step]: + assumes nn: "ks \ []" "u = w" + shows "\st i ** ps u ** reps v w ks\ + i:[if_one e]:j + \st e ** ps u ** reps v w ks\" + by (unfold `u = w`, rule hoare_if_one_reps[OF `ks \ []`]) + +lemma hoare_if_zero_ones_false[step]: + assumes "\ w < u" "v = w" + shows "\st i \* ps v \* ones u w\ + i :[if_zero e]: j + \st j \* ps v \* ones u w\" + by (unfold `v = w` ones_rev[OF `\ w < u`], hstep) + +lemma hoare_left_until_double_zero_nil[step]: + assumes "u = v" + shows "\st i ** ps u ** zero v\ + i:[left_until_double_zero]:j + \st j ** ps u ** zero v\" + 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 \ []" + shows "\st i ** ps v ** reps u v ks\ + i:[if_zero e]:j + \st j ** ps v ** reps u v ks\" +proof(rule rev_exhaust[of ks]) + assume "ks = []" with nn show ?thesis by simp +next + fix y ys + assume eq_ks: "ks = ys @ [y]" + show " \st i \* ps v \* reps u v ks\ i :[ if_zero e ]: j \st j \* ps v \* reps u v ks\" + proof(cases "ys = []") + case False + have "\st i \* ps v \* reps u v (ys @ [y])\ i :[ if_zero e ]: j \st j \* ps v \* reps u v (ys @ [y])\" + 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 + qed +qed + +lemma hoare_if_zero_reps_false_gen[step]: + assumes "ks \ []" "u = w" + shows "\st i ** ps u ** reps v w ks\ + i:[if_zero e]:j + \st j ** ps u ** reps v w ks\" + by (unfold `u = w`, rule hoare_if_zero_reps_false[OF `ks \ []`]) + + +lemma hoare_if_zero_reps_false1: + assumes nn: "ks \ []" + shows "\st i ** ps u ** reps u v ks\ + i:[if_zero e]:j + \st j ** ps u ** reps u v ks\" +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)+) +qed + +lemma hoare_if_zero_reps_false1_gen[step]: + assumes nn: "ks \ []" + and h: "u = w" + shows "\st i ** ps u ** reps w v ks\ + i:[if_zero e]:j + \st j ** ps u ** reps w v ks\" + by (unfold h, rule hoare_if_zero_reps_false1[OF `ks \ []`]) + +lemma hoare_left_until_double_zero: + assumes h: "ks \ []" + shows "\st i ** ps v ** zero u ** zero (u + 1) ** reps (u+2) v ks\ + i:[left_until_double_zero]:j + \st j ** ps u ** zero u ** zero (u + 1) ** reps (u+2) v ks\" +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 "\st i \* ps v \* zero u \* zero (u + 1) \* reps (u + 2) v ks\ + ?body + \st ?j \* ps u \* zero u \* zero (u + 1) \* reps (u + 2) v ks\" + 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) \* one (u + 2 + int k))" + by (smt ones_rev) + have eq_ones': "(one (u + 2) \* ones (3 + u) (u + 2 + int k)) = + (one (u + 2 + int k) \* 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' \* ps (u + 2 + int k) \* zero u \* + zero (u + 1) \* 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 \* + ps (1 + (u + int (reps_len ks))) \* + zero u \* + zero (u + 1) \* + reps (u + 2) (1 + (u + int (reps_len ks))) ks \* + zero (u + 2 + int (reps_len ks)) \* + 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 + qed +qed + +lemma hoare_left_until_double_zero_gen[step]: + assumes h1: "ks \ []" + and h: "u = y" "w = v + 1" "x = v + 2" + shows "\st i ** ps u ** zero v ** zero w ** reps x y ks\ + i:[left_until_double_zero]:j + \st j ** ps v ** zero v ** zero w ** reps x y ks\" + by (unfold h, rule hoare_left_until_double_zero[OF h1]) + +lemma hoare_jmp_reps1: + assumes "ks \ []" + shows "\ st i \* ps u \* reps u v ks\ + i:[jmp e]:j + \ st e \* ps u \* reps u v ks\" +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]) + qed +qed + +lemma hoare_jmp_reps1_gen[step]: + assumes "ks \ []" "u = v" + shows "\ st i \* ps u \* reps v w ks\ + i:[jmp e]:j + \ st e \* ps u \* reps v w ks\" + by (unfold assms, rule hoare_jmp_reps1[OF `ks \ []`]) + +lemma hoare_jmp_reps: + "\ st i \* ps u \* reps u v ks \* tm (v + 1) x \ + i:[(jmp e; c)]:j + \ st e \* ps u \* reps u v ks \* tm (v + 1) x \" +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]) + qed +qed + +definition "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 \ []" + shows "\st i \* ps u ** reps u v ks \* zero (v + 1) \* zero (v + 2) \ + i:[shift_right]:j + \st j ** ps (v + 2) ** zero u ** reps (u + 1) (v + 1) ks ** zero (v + 2) \" +proof(unfold shift_right_def, intro t_hoare_local t_hoare_label, clarify, + rule t_hoare_label_last, auto) + fix la + have eq_ones: "\ u k. (one (u + int k + 1) \* ones (u + 1) (u + int k)) = + (one (u + 1) \* 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 "\st i \* ps u \* reps u v ks \* zero (v + 1) \* zero (v + 2)\ + i :[ (if_zero la ; + write_zero ; move_right ; right_until_zero ; write_one ; move_right ; jmp i) ]: la + \st la \* ps (v + 2) \* zero u \* reps (u + 1) (v + 1) ks \* zero (v + 2)\" + 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: + "\st i \* ps u \* one u \* ones (u + 1) (u + int k) \* zero (u + int k + 1) \* + zero (u + int k + 2)\ + ?body + \st i \* + ps (u + int k + 2) \* + one (u + int k + 1) \* ones (u + 1) (u + int k) \* zero u \* zero (u + int k + 2)\" + apply (hsteps) + by (simp add:sep_conj_ac, sep_cancel+, smt) + hence "\st i \* ps u \* one u \* ones (u + 1) (u + int k) \* zero (u + int k + 1) \* + zero (u + int k + 2)\ + ?body + \st ?j \* ps (u + int k + 2) \* zero u \* one (u + 1) \* + ones (2 + u) (u + 1 + int k) \* zero (u + int k + 2)\" + proof(rule tm.sequencing) + show "\st i \* + ps (u + int k + 2) \* + one (u + int k + 1) \* ones (u + 1) (u + int k) \* zero u \* zero (u + int k + 2)\ + ?body + \st ?j \* + ps (u + int k + 2) \* + zero u \* one (u + 1) \* ones (2 + u) (u + 1 + int k) \* zero (u + int k + 2)\" + 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) \* + ones (u + 1) (u + int k) \* + zero u \* reps (u + int k + 2) v ks \* zero (v + 1) \* zero (v + 2)) + = + (zero u \* + ones (u + 1) (u + int k) \* + one (u + int k + 1) \* reps (u + int k + 2) v ks \* zero (v + 1) \* zero (v + 2))" + by (simp add:eq_ones sep_conj_ac) + have "\st i \* ps u \* one u \* ones (u + 1) (u + int k) \* zero (u + int k + 1) \* + reps (u + int k + 2) v ks \* zero (v + 1) \* zero (v + 2)\ + ?body + \st i \* ps (u + int k + 2) \* zero u \* ones (u + 1) (u + int k) \* + one (u + int k + 1) \* reps (u + int k + 2) v ks \* zero (v + 1) \* zero (v + 2)\" + apply (hsteps) + by (auto simp:sep_conj_ac, sep_cancel+, smt) + hence "\st i \* ps u \* one u \* ones (u + 1) (u + int k) \* zero (u + int k + 1) \* + reps (u + int k + 2) v ks \* zero (v + 1) \* zero (v + 2)\ + ?body + \st ?j \* ps (v + 2) \* zero u \* one (u + 1) \* ones (2 + u) (u + 1 + int k) \* + zero (2 + (u + int k)) \* reps (3 + (u + int k)) (v + 1) ks \* zero (v + 2)\" + proof(rule tm.sequencing) + have eq_ones': + "\ u k. (one (u + int k + 1) \* ones (u + 1) (u + int k) \* zero (u + int k + 2)) = + (one (u + 1) \* zero (2 + (u + int k)) \* ones (2 + u) (u + 1 + int k))" + by (smt eq_ones sep.mult_assoc sep_conj_commute) + show "\st i \* ps (u + int k + 2) \* zero u \* + ones (u + 1) (u + int k) \* one (u + int k + 1) \* reps (u + int k + 2) v ks \* + zero (v + 1) \* zero (v + 2)\ + ?body + \st ?j \* ps (v + 2) \* zero u \* one (u + 1) \* ones (2 + u) (u + 1 + int k) \* + zero (2 + (u + int k)) \* reps (3 + (u + int k)) (v + 1) ks \* zero (v + 2)\" + 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 auto +qed + +lemma hoare_shift_right_cons_gen[step]: + assumes h: "ks \ []" + and h1: "u = v" "x = w + 1" "y = w + 2" + shows "\st i \* ps u ** reps v w ks \* zero x \* zero y \ + i:[shift_right]:j + \st j ** ps y ** zero v ** reps (v + 1) x ks ** zero y\" + by (unfold h1, rule hoare_shift_right_cons[OF h]) + +lemma shift_right_nil [step]: + assumes "u = v" + shows + "\ st i \* ps u \* zero v \ + i:[shift_right]:j + \ st j \* ps u \* zero v \" + 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]: + "\st i ** ps u ** ones u v ** zero (v + 1)\ + i :[clear_until_zero]: j + \st j ** ps (v + 1) ** zeros u v ** zero (v + 1)\ " +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 "\st i \* ps u \* ones u v \* zero (v + 1)\ ?body + \st j \* ps (v + 1) \* zeros u v \* zero (v + 1)\" + proof(induct u v rule: zeros.induct) + fix ia ja + assume h: "\ ja < ia \ + \st i \* ps (ia + 1) \* ones (ia + 1) ja \* zero (ja + 1)\ ?body + \st j \* ps (ja + 1) \* zeros (ia + 1) ja \* zero (ja + 1)\" + show "\st i \* ps ia \* ones ia ja \* zero (ja + 1)\ ?body + \st j \* ps (ja + 1) \* zeros ia ja \* zero (ja + 1)\" + 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 \* ones (ia + 1) ja)" + by(simp add: ones.simps) + from False have zeros_eq: "zeros ia ja = (zero ia \* zeros (ia + 1) ja)" + by(simp add: zeros.simps) + have s1: "\st i \* ps ia \* one ia \* ones (ia + 1) ja \* zero (ja + 1)\ ?body + \st i \* ps (ia + 1) \* zero ia \* ones (ia + 1) ja \* zero (ja + 1)\" + 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) \* ones (ia + 1 + 1) ja)" + by(simp add: ones.simps) + thus ?thesis + by (simp, hsteps) + qed + have s2: "\st i \* ps (ia + 1) \* zero ia \* ones (ia + 1) ja \* zero (ja + 1)\ + ?body + \st j \* ps (ja + 1) \* zero ia \* zeros (ia + 1) ja \* zero (ja + 1)\" + by hsteps + from tm.sequencing[OF s1 s2] have + "\st i \* ps ia \* one ia \* ones (ia + 1) ja \* zero (ja + 1)\ ?body + \st j \* ps (ja + 1) \* zero ia \* zeros (ia + 1) ja \* zero (ja + 1)\" . + thus ?thesis + unfolding ones_eq zeros_eq by(simp add: sep_conj_ac) + qed + qed +qed + +lemma hoare_clear_until_zero_gen[step]: + assumes "u = v" "x = w + 1" + shows "\st i ** ps u ** ones v w ** zero x\ + i :[clear_until_zero]: j + \st j ** ps x ** zeros v w ** zero x\" + 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 \ []" "u = v" + shows + "\st i ** ps u ** reps v w ks\ + i:[move_left]:j + \st j ** ps (u - 1) ** reps v w ks\" +proof - + from `ks \ []` 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 \* ones (v + 1) (v + int y))" + by (smt ones_step_simp) + my_block_end + apply (unfold this, hsteps) + by (simp add:this, hsteps) +qed + +lemma hoare_shift_left_cons: + assumes h: "ks \ []" + shows "\st i \* ps u \* tm (u - 1) x \* reps u v ks \* zero (v + 1) \* zero (v + 2) \ + i:[shift_left]:j + \st j \* ps (v + 2) \* reps (u - 1) (v - 1) ks \* zero v \* zero (v + 1) \* zero (v + 2) \" +proof(unfold shift_left_def, intro t_hoare_local t_hoare_label, clarify, + rule t_hoare_label_last, simp+, clarify, prune) + show " \st i \* ps u \* tm (u - 1) x \* reps u v ks \* zero (v + 1) \* zero (v + 2)\ + i :[ (if_zero j ; + move_left ; + write_one ; + right_until_zero ; + move_left ; write_zero ; + move_right ; move_right ; jmp i) ]: j + \st j \* ps (v + 2) \* reps (u - 1) (v - 1) ks \* zero v \* zero (v + 1) \* zero (v + 2)\" + 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 "\st i \* ps u \* tm (u - 1) x \* (one u \* ones (u + 1) (u + int k)) \* + zero (u + int k + 1) \* zero (u + int k + 2)\ + ?body + \st j \* ps (u + int k + 2) \* (one (u - 1) \* ones u (u - 1 + int k)) \* + zero (u + int k) \* zero (u + int k + 1) \* zero (u + int k + 2)\" + apply(rule tm.sequencing [where q = "st i \* ps (u + int k + 2) \* + (one (u - 1) \* ones u (u - 1 + int k)) \* + zero (u + int k) \* zero (u + int k + 1) \* zero (u + int k + 2)"]) + apply (hsteps) + apply (rule_tac p = "st j' \* ps (u - 1) \* ones (u - 1) (u + int k) \* + zero (u + int k + 1) \* 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) \* 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 "\st i \* ps u \* tm (u - 1) x \* one u \* ones (u + 1) (u + int k) \* + zero (u + int k + 1) \* reps (u + int k + 2) v ks \* zero (v + 1) \* zero (v + 2)\ + ?body + \st j \* ps (v + 2) \* one (u - 1) \* ones u (u - 1 + int k) \* + zero (u + int k) \* reps (1 + (u + int k)) (v - 1) ks \* + zero v \* zero (v + 1) \* zero (v + 2)\" + apply (rule tm.sequencing[where q = "st i \* ps (u + int k + 2) \* + zero (u + int k + 1) \* reps (u + int k + 2) v ks \* zero (v + 1) \* + zero (v + 2) \* one (u - 1) \* ones u (u - 1 + int k) \* zero (u + int k)"]) + apply (hsteps) + apply (rule_tac p = "st j' \* ps (u - 1) \* + ones (u - 1) (u + int k) \* + zero (u + int k + 1) \* + reps (u + int k + 2) v ks \* zero (v + 1) \* 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) \* 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 \ []`, of i "u + int k + 2" Bk v, folded zero_def] + have "\st i \* ps (u + int k + 2) \* zero (u + int k + 1) \* + reps (u + int k + 2) v ks \* zero (v + 1) \* zero (v + 2)\ + ?body + \st j \* ps (v + 2) \* reps (1 + (u + int k)) (v - 1) ks \* + zero v \* zero (v + 1) \* zero (v + 2)\" + 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 auto +qed + +lemma hoare_shift_left_cons_gen[step]: + assumes h: "ks \ []" + "v = u - 1" "w = u" "y = x + 1" "z = x + 2" + shows "\st i \* ps u \* tm v vv \* reps w x ks \* tm y Bk \* tm z Bk\ + i:[shift_left]:j + \st j \* ps z \* reps v (x - 1) ks \* zero x \* zero y \* zero z \" + by (unfold assms, fold zero_def, rule hoare_shift_left_cons[OF `ks \ []`]) + +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: + "\ i j . \st i \* ps u \* zero u \* p \ + i:[c1]:j + \st e \* q \ + " + shows "\st i \* ps u \* zero u \* p \ + i:[(bone c1 c2)]:j + \st e \* q \ + " +apply (unfold bone_def, intro t_hoare_local) +apply hsteps +apply (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: + "\ i j . \st i \* ps u \* zero u \* p \ + i:[c1]:j + \st j \* ps v \* tm v x \* q \ + " + shows "\st i \* ps u \* zero u \* p \ + i:[(bone c1 c2)]:j + \st j \* ps v \* tm v x \* q \ + " +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 hsteps +qed + +lemma hoare_bone_2: + assumes h: + "\ i j . \st i \* ps u \* one u \* p \ + i:[c2]:j + \st j \* q \ + " + shows "\st i \* ps u \* one u \* p \ + i:[(bone c1 c2)]:j + \st j \* q \ + " +apply (unfold bone_def, intro t_hoare_local) +apply (rule_tac q = "st la \* ps u \* one u \* 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), 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: + "\ i j . \st i \* ps u \* one u \* p \ + i:[c2]:j + \st e \* q \ + " + shows "\st i \* ps u \* one u \* p \ + i:[(bone c1 c2)]:j + \st e \* q \ + " +apply (unfold bone_def, intro t_hoare_local) +apply (rule_tac q = "st la \* ps u \* one u \* p" in tm.sequencing) +apply hsteps +apply (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]: + "\ i j . \st i \* ps u \* one u \* p \ + i:[c1]:j + \st j \* ps v \* tm v x \* q \ + " + shows "\st i \* ps u \* one u \* p \ + i:[(bzero c1 c2)]:j + \st j \* ps v \* tm v x \* q \ + " +apply (unfold bzero_def, intro t_hoare_local) +apply hsteps +apply (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 hsteps + +lemma hoare_bzero_1_out: + assumes h[step]: + "\ i j . \st i \* ps u \* one u \* p \ + i:[c1]:j + \st e \* q \ + " + shows "\st i \* ps u \* one u \* p \ + i:[(bzero c1 c2)]:j + \st e \* q \ + " +apply (unfold bzero_def, intro t_hoare_local) +apply hsteps +apply (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: + "\ i j. \st i \* ps u \* zero u \* p \ + i:[c2]:j + \st j \* q \ + " + shows "\st i \* ps u \* zero u \* p \ + i:[(bzero c1 c2)]:j + \st j \* q \ + " + apply (unfold bzero_def, intro t_hoare_local) + apply (rule_tac q = "st la \* ps u \* zero u \* 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: + "\ i j . \st i \* ps u \* zero u \* p \ + i:[c2]:j + \st e \* q \ + " + shows "\st i \* ps u \* zero u \* p\ + i:[(bzero c1 c2)]:j + \st e \* q \ + " +apply (unfold bzero_def, intro t_hoare_local) +apply (rule_tac q = "st la \* ps u \* zero u \* p" in tm.sequencing) +apply hsteps +apply (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 \ []" "ys \ []" + shows "reps_len (xs @ ys) = reps_len xs + reps_len ys + 1" + using assms +proof(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 \ []`] reps_len_sg) + next + case False + hence " xs1 @ ys \ []" by simp + thus ?thesis + apply (simp add:reps_len_cons[OF `xs1@ys \ []`] reps_len_cons[OF `xs1 \ []`]) + by (simp add: Cons.hyps[OF `xs1 \ []` `ys \ []`]) + qed +qed auto + +lemma hoare_skip_or_set_set: + "\ st i \* ps u \* zero u \* zero (u + 1) \* tm (u + 2) x\ + i:[skip_or_set]:j + \ st j \* ps (u + 2) \* one u \* zero (u + 1) \* tm (u + 2) x\" + apply(unfold skip_or_set_def) + apply(rule_tac q = "st j \* ps (u + 2) \* tm (u + 2) x \* one u \* 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 "\st i \* ps u \* zero v \* zero w \* tm x xv\ + i:[skip_or_set]:j + \st j \* ps x \* one v \* zero w \* tm x xv\" + by (unfold assms, rule hoare_skip_or_set_set) + +lemma hoare_skip_or_set_skip: + "\ st i \* ps u \* reps u v [k] \* zero (v + 1)\ + i:[skip_or_set]:j + \ st j \* ps (v + 2) \* reps u v [k] \* zero (v + 1)\" +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 \* ps u \* one u \* ones (u + 1) (u + int k) \* + zero (u + int k + 1)" + in tm.pre_stren) + apply (rule_tac q = "st j \* ps (u + int k + 2) \* + one u \* ones (u + 1) (u + int k) \* zero (u + int k + 1) + " in tm.post_weaken) + apply (rule hoare_bone_2) + apply (rule_tac p = " st i \* ps u \* ones u (u + int k) \* 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) + qed + +lemma hoare_skip_or_set_skip_gen[step]: + assumes "u = v" "x = w + 1" + shows "\ st i \* ps u \* reps v w [k] \* zero x\ + i:[skip_or_set]:j + \ st j \* ps (w + 2) \* reps v w [k] \* zero x\" + 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 + "\st i \* ps u \* reps u v [k] \* zero (v + 1)\ + i:[if_reps_z e]:j + \st e \* ps u \* reps u v [k] \* zero (v + 1)\" + 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' \* ps (u + 1) \* zero (u + 1) \* 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 "\st i \* ps u \* reps v w [k] \* zero x\ + i:[if_reps_z e]:j + \st e \* ps u \* reps v w [k] \* zero x\" + by (unfold assms, rule hoare_if_reps_z_true, simp) + +lemma hoare_if_reps_z_false: + assumes h: "k \ 0" + shows + "\st i \* ps u \* reps u v [k]\ + i:[if_reps_z e]:j + \st j \* ps u \* reps u v [k]\" +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' \* ps (u + 1) \* one (u + 1) \* one u \* + ones (2 + u) (u + (1 + int k'))" in tm.pre_stren) + apply (rule_tac hoare_bone_2) + by (hsteps) +qed + +lemma hoare_if_reps_z_false_gen[step]: + assumes h: "k \ 0" "u = v" + shows + "\st i \* ps u \* reps v w [k]\ + i:[if_reps_z e]:j + \st j \* ps u \* reps v w [k]\" + by (unfold assms, rule hoare_if_reps_z_false[OF `k \ 0`]) + +definition "if_reps_nz e = (move_right; + bzero (move_left; jmp e) (move_left) + )" + +lemma EXS_postI: + assumes "\P\ + c + \Q x\" + shows "\P\ + c + \EXS x. Q x\" +by (metis EXS_intro assms tm.hoare_adjust) + +lemma hoare_if_reps_nz_true: + assumes h: "k \ 0" + shows + "\st i \* ps u \* reps u v [k]\ + i:[if_reps_nz e]:j + \st e \* ps u \* reps u v [k]\" +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' \* ps (u + 1) \* one (u + 1) \* one u \* + ones (2 + u) (u + (1 + int k'))" in tm.pre_stren) + apply (rule hoare_bzero_1_out) + by hsteps +qed + + +lemma hoare_if_reps_nz_true_gen[step]: + assumes h: "k \ 0" "u = v" + shows + "\st i \* ps u \* reps v w [k]\ + i:[if_reps_nz e]:j + \st e \* ps u \* reps v w [k]\" + by (unfold assms, rule hoare_if_reps_nz_true[OF `k\ 0`]) + +lemma hoare_if_reps_nz_false: + assumes h: "k = 0" + shows + "\st i \* ps u \* reps u v [k] \* zero (v + 1)\ + i:[if_reps_nz e]:j + \st j \* ps u \* reps u v [k] \* zero (v + 1)\" + 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' \* ps (u + 1) \* zero (u + 1) \* 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 + "\st i \* ps u \* reps v w [k] \* zero x\ + i:[if_reps_nz e]:j + \st j \* ps u \* reps v w [k] \* zero x\" + 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 "\st i \* ps u \* zeros u (u + int (reps_len (replicate (Suc n) 0))) \* + tm (u + int (reps_len (replicate (Suc n) 0)) + 1) x\ + i:[skip_or_sets (Suc n)]:j + \st j \* ps (u + int (reps_len (replicate (Suc n) 0)) + 1) \* + reps' u (u + int (reps_len (replicate (Suc n) 0))) (replicate (Suc n) 0) \* + tm (u + int (reps_len (replicate (Suc n) 0)) + 1) x \" +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: "\n. n \ 0 \ 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: "\ u v. (zeros u (u + int (v + 2))) = + (zeros u (u + (int v)) \* zero (u + (int v) + 1) \* 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))) \* + zero ((u + int (reps_len (replicate (Suc n) 0))) + 1) \* + zero ((u + int (reps_len (replicate (Suc n) 0))) + 2)) + " by (simp only:eq_len) + have hh: "\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 \ []" "[skip_or_set] \ []" 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 \ 0" by simp + show ?case + apply (unfold eq_z eq_code) + apply (hstep Suc(1)) + apply (unfold eq_len[OF `Suc n \ 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) + qed + +lemma hoare_skip_or_sets_set_gen[step]: + assumes h: "p2 = p1" + "p3 = p1 + int (reps_len (replicate (Suc n) 0))" + "p4 = p3 + 1" + shows "\st i \* ps p1 \* zeros p2 p3 \* tm p4 x\ + i:[skip_or_sets (Suc n)]:j + \st j \* ps p4 \* reps' p2 p3 (replicate (Suc n) 0) \* tm p4 x\" + 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 "\st i \* ps u \* reps' u v (take n ks) \* reps' (v + 1) w [ks!n] \ + i:[skip_or_sets (Suc n)]:j + \st j \* ps (w+1) \* reps' u v (take n ks) \* reps' (v + 1) w [ks!n]\" + using h +proof(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 \ []" "[skip_or_set] \ []" 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 "\st i \* ps u \* (reps' u (m - 1) (take n ks) \* reps' m v [ks ! n])\ + i :[ (skip_or_sets (Suc n)) ]: j + \st j \* ps (v + 1) \* (reps' u (m - 1) (take n ks) \* reps' m v [ks ! n])\" + 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 "\st j' \* ps (v + 1) \* reps' (v + 1) w [ks ! Suc n]\ + j' :[ skip_or_set ]: j + \st j \* ps (w + 1) \* reps' (v + 1) w [ks ! Suc n]\" + 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+) +qed + +lemma hoare_skip_or_sets_skip_gen[step]: + assumes h: "n < length ks" "u = v" "x = w + 1" + shows "\st i \* ps u \* reps' v w (take n ks) \* reps' x y [ks!n] \ + i:[skip_or_sets (Suc n)]:j + \st j \* ps (y+1) \* reps' v w (take n ks) \* reps' x y [ks!n]\" + 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)) \* 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 \ v" + shows "(zeros u v \* 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 \* fam_conj {v<..} zero) = fam_conj ({u - 1<..v} + {v<..}) zero" . + moreover + from `u \ 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 \ (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 \ j` have hh: "i + 1 \ j" by auto + hence eq_set: "{i..j} = (insert i {i + 1 .. j})" + by (smt simp_from_to) + have "i \ {i + 1 .. j}" by simp + from fam_conj_insert_simp[OF this, folded eq_set] + have "fam_conj {i..j} zero = (zero i \* fam_conj {i + 1..j} zero)" . + with Step(2)[OF hh] Step + show ?thesis by simp + qed + qed + } + moreover note this[OF `u \ v`] + ultimately show ?thesis by simp + qed + ultimately show ?thesis by smt +qed + +declare replicate.simps [simp del] + +lemma hoare_skip_or_sets_comb: + assumes "length ks \ n" + shows "\st i \* ps u \* reps u v ks \* fam_conj {v<..} zero\ + i:[skip_or_sets (Suc n)]:j + \st j \* ps ((v + int (reps_len (list_ext n ks)) - int (reps_len ks))+ 2) \* + reps' u (v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1) (list_ext n ks) \* + fam_conj {(v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1)<..} zero \" +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 \* ps (v + 1) \* + zeros (v + 1) (v + 1 + int (reps_len (replicate (Suc n) 0))) \* + tm (v + 2 + int (reps_len (replicate (Suc n) 0))) Bk \* + 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 \ (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)))) \* + 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 \ 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 \* fam_conj {v<..} zero) = + (reps' u (v + 1) ks \* 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 "\st i \* ps u \* reps' u (v + 1) ks \ + i :[ skip_or_sets (Suc (length ks - 1))]: j + \st j \* ps (v + 2) \* reps' u (v + 1) ks \" + 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) \* tm (u + int n + 2) Bk \* fam_conj {(u + int n + 2)<..} zero)" + my_block + have "u + 1 \ (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) \* 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) \* 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 \ 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 \ []" 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 \ 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) +qed + +lemma hoare_skip_or_sets_comb_gen: + assumes "length ks \ n" "u = v" "w = x" + shows "\st i \* ps u \* reps v w ks \* fam_conj {x<..} zero\ + i:[skip_or_sets (Suc n)]:j + \st j \* ps ((x + int (reps_len (list_ext n ks)) - int (reps_len ks))+ 2) \* + reps' u (x + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1) (list_ext n ks) \* + fam_conj {(x + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1)<..} zero \" + by (unfold assms, rule hoare_skip_or_sets_comb[OF `length ks \ 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 \ 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 \ []" 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 simp +qed + +lemma reps'_nn_expand: + assumes "xs \ []" + shows "(reps' u v xs) = (reps u (v - 1) xs \* zero v)" + by (metis assms reps'_def) + +lemma sep_conj_st1: "(p \* st t \* q) = (st t \* p \* q)" + by (simp only:sep_conj_ac) + +lemma sep_conj_st2: "(p \* st t) = (st t \* p)" + by (simp only:sep_conj_ac) + +lemma sep_conj_st3: "((st t \* p) \* r) = (st t \* p \* r)" + by (simp only:sep_conj_ac) + +lemma sep_conj_st4: "(EXS x. (st t \* r x)) = ((st t) \* (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_st4 + +lemma sep_conj_cond3 : "( \* ) = <(cond1 \ cond2)>" + by (smt cond_eqI cond_true_eq sep_conj_commute sep_conj_empty) + +lemma sep_conj_cond4 : "( \* \* r) = (<(cond1 \ cond2)> \* 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: + "\st i ** ps v ** zero u ** reps (u + 1) v [k]\ + i:[left_until_zero]:j + \st j ** ps u ** zero u ** reps (u + 1) v [k]\" + apply (unfold reps.simps, simp only:sep_conj_cond) + apply (rule tm.pre_condI, simp) + by hstep + +lemma hoare_left_until_zero_reps_gen[step]: + assumes "u = x" "w = v + 1" + shows "\st i ** ps u ** zero v ** reps w x [k]\ + i:[left_until_zero]:j + \st j ** ps v ** zero v ** reps w x [k]\" + 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)> \* 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" . +qed + +lemma condI1: + assumes "p s" "b" + shows "( \* p) s" +proof(rule condI[OF assms(2)]) + from assms(1) show "p s" . +qed + +lemma hoare_locate_set: + assumes "length ks \ n" + shows "\st i \* zero (u - 1) \* ps u \* reps u v ks \* fam_conj {v<..} zero\ + i:[locate n]:j + \st j \* zero (u - 1) \* + (EXS m w. ps m \* reps' u (m - 1) (take n (list_ext n ks)) \* + reps m w [(list_ext n ks)!n] \* fam_conj {w<..} zero)\" +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 \ 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' \* <(m = u + int (reps_len (take n (list_ext n ks))) + 1)> \* + ps (v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 2) \* + ((reps u (m - 1 - 1) (take n (list_ext n ks)) \* zero (m - 1)) \* + reps' m (v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1) + [list_ext n ks ! n]) \* + fam_conj + {v + int (reps_len (list_ext n ks)) - int (reps_len ks) + 1<..} + zero \* + zero (u - 1)" + in tm.pre_stren) + my_block + have "[list_ext n ks ! n] \ []" 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] \* + 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) \* + 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 \ 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] \ []" 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)> \* + 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 \ n`]) + apply (subst (1) reps'_append, simp add:sep_conj_exists) + apply (rule tm.precond_exI) + my_block + from True `length ks \ 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 smt +qed + +lemma hoare_locate_set_gen[step]: + assumes "length ks \ n" + "u = v - 1" "v = w" "x = y" + shows "\st i \* zero u \* ps v \* reps w x ks \* fam_conj {y<..} zero\ + i:[locate n]:j + \st j \* zero u \* + (EXS m w. ps m \* reps' v (m - 1) (take n (list_ext n ks)) \* + reps m w [(list_ext n ks)!n] \* fam_conj {w<..} zero)\" + by (unfold assms, rule hoare_locate_set[OF `length ks \ n`]) + +lemma hoare_locate_skip: + assumes h: "n < length ks" + shows + "\st i \* ps u \* zero (u - 1) \* reps' u (v - 1) (take n ks) \* reps' v w [ks!n] \* tm (w + 1) x\ + i:[locate n]:j + \st j \* ps v \* zero (u - 1) \* reps' u (v - 1) (take n ks) \* reps' v w [ks!n] \* tm (w + 1) x\" +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 hsteps +qed + + +lemma hoare_locate_skip_gen[step]: + assumes "n < length ks" + "v = u - 1" "w = u" "x = y - 1" "z' = z + 1" + shows + "\st i \* ps u \* tm v Bk \* reps' w x (take n ks) \* reps' y z [ks!n] \* tm z' vx\ + i:[locate n]:j + \st j \* ps y \* tm v Bk \* reps' w x (take n ks) \* reps' y z [ks!n] \* tm z' vx\" + 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 \* ones (m + 1) (m + int k))" + by (simp add:ones_simps) + +lemma reps_splitedI: + assumes h1: "(reps u v ks1 \* zero (v + 1) \* reps (v + 2) w ks2) s" + and h2: "ks1 \ []" + and h3: "ks2 \ []" + 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 \* + zero (u + int (reps_len ks1)) \* 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) +qed + +lemma reps_sucI: + assumes h: "(reps u v (xs@[x]) \* 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)) \* 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 \* zero (v - int (x + 1) - 1 + 1) \* + 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) \* 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 \ []" . + next + show "[Suc x] \ []" by simp + qed +qed + +lemma cond_expand: "( \* p) s = (cond \ (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 "\ (1 + n) < m" + shows "(ones m n \* one (1 + n)) = (ones m (1 + n))" + by (insert ones_rev[OF assms, simplified], simp) + +lemma reps_one_abs: + assumes "(reps u v [k] \* 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 \* reps w x ys) s" + "w = v + 1" "ys \ []" + 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) +qed + +lemma reps_one_abs1: + assumes "(reps u v (xs@[k]) \* 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 simp +next + 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) +qed + +lemma tm_hoare_inc00: + assumes h: "a < length ks \ ks ! a = v" + shows "\st i \* ps u \* zero (u - 2) \* zero (u - 1) \* reps u ia ks \* fam_conj {ia<..} zero\ + i :[ Inc a ]: j + \st j \* + ps u \* + zero (u - 2) \* + zero (u - 1) \* + reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1) (ks[a := Suc v]) \* + fam_conj {(ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1)<..} zero\" + (is "\ ?P \ ?code \ ?Q \") +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 \ []" by auto + hence "(reps u ia ks \* zero (ia + 1)) = reps' u (ia + 1) ks" + by (simp add:reps'_def) + also from eq_ks have "\ = reps' u (ia + 1) (take a ks @ [ks!a] @ drop (Suc a) ks)" by simp + also have "\ = (EXS m. reps' u (m - 1) (take a ks) \* + reps' m (ia + 1) (ks ! a # drop (Suc a) ks))" + by (simp add:reps'_append) + also have "\ = (EXS m. reps' u (m - 1) (take a ks) \* + reps' m (ia + 1) ([ks ! a] @ drop (Suc a) ks))" + by simp + also have "\ = (EXS m ma. reps' u (m - 1) (take a ks) \* + reps' m (ma - 1) [ks ! a] \* reps' ma (ia + 1) (drop (Suc a) ks))" + by (simp only:reps'_append sep_conj_exists) + finally have eq_s: "(reps u ia ks \* zero (ia + 1)) = \" . + { fix m ma + have eq_u: "-1 + u = u - 1" by smt + have " \st i \* + ps u \* + zero (u - 2) \* + zero (u - 1) \* + (reps' u (m - 1) (take a ks) \* + reps' m (ma - 1) [ks ! a] \* reps' ma (ia + 1) (drop (Suc a) ks)) \* + fam_conj {ia + 1<..} zero\ + i :[ Inc a ]: j + \st j \* + ps u \* + zero (u - 2) \* + zero (u - 1) \* + reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1) (ks[a := Suc v]) \* + fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1<..} zero\" + 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 \* + reps u (1 + (m + int (ks ! a))) (take a ks @ [Suc (ks ! a)])) hc" + hence "(fam_conj {m + int (ks ! a) + 1<..} zero \* 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' \* ps (1 + (m + int (ks ! a))) \* zero (u - 1) \* zero (u - 2) \* + reps u (1 + (m + int (ks ! a))) (take a ks @ [Suc (ks!a)]) + \* 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' \* + ps (2 + (m + int (ks ! a))) \* + reps (2 + (m + int (ks ! a))) ia (drop (Suc a) ks) \* zero (ia + 1) \* zero (ia + 2) \* + reps u (m + int (ks ! a)) (take a ks @ [ks!a]) \* zero (1 + (m + int (ks ! a))) \* + zero (u - 2) \* zero (u - 1) \* 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' \* ps (1 + (m + int (ks ! a))) \* + zero (u - 2) \* zero (u - 1) \* + reps u (1 + (m + int (ks ! a))) (take a ks @ [Suc (ks ! a)]) \* + zero (2 + (m + int (ks ! a))) \* + reps (3 + (m + int (ks ! a))) (ia + 1) (drop (Suc a) ks) \* 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 \* ps u \* zero (u - 2) \* zero (u - 1) \* + (reps u ia ks \* zero (ia + 1)) \* 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) +qed + +declare ones_simps [simp del] + +lemma tm_hoare_inc01: + assumes "length ks \ a \ v = 0" + shows + "\st i \* ps u \* zero (u - 2) \* zero (u - 1) \* reps u ia ks \* fam_conj {ia<..} zero\ + i :[ Inc a ]: j + \st j \* + ps u \* + zero (u - 2) \* + zero (u - 1) \* + reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1) ((list_ext a ks)[a := Suc v]) \* + fam_conj {(ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1)<..} zero\" +proof - + from assms have "length ks \ a" "v = 0" by auto + show ?thesis + apply (rule_tac p = " + st i \* ps u \* zero (u - 2) \* zero (u - 1) \* (reps u ia ks \* <(ia = u + int (reps_len ks) - 1)>) \* + 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 \ 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)) \* <(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' \* ps (m + int (list_ext a ks ! a) + 1) \* + zero (u - 2) \* zero (u - 1) \* + reps u (m + int (list_ext a ks ! a) + 1) + ((take a (list_ext a ks))@[Suc (list_ext a ks ! a)]) \* + 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 \ a` have "list_ext a ks ! a = 0" + by (metis le_refl list_ext_tail) + from `length ks \ 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 \* + 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 \* + 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+) +qed + +definition "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: "(( \* p) s) = (b \ (p s))" +proof + assume "( \* p) s" + from condD[OF this] show " b \ p s" . +next + assume "b \ p s" + hence b and "p s" by auto + from `b` have "() 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 "( \* p) s" by (auto intro!:sep_conjI) +qed + +lemma tm_hoare_dec_fail00: + assumes "a < length ks \ ks ! a = 0" + shows "\st i \* ps u \* zero (u - 2) \* zero (u - 1) \* reps u ia ks \* fam_conj {ia<..} zero\ + i :[ Dec a e ]: j + \st e \* ps u \* zero (u - 2) \* zero (u - 1) \* + reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks)) (list_ext a ks[a := 0]) \* + fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) <..} zero\" +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) \* fam_conj {ia<..} zero) = + (reps' u (ia + 1) ((take a ks @ [ks ! a]) @ drop (Suc a) ks) \* 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] \* 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 \* + ps mb \* + reps u mb ((take a ks)@[ks ! a]) \* <(m - 2 = mb)> \* + zero (m - 1) \* + zero (u - 1) \* + one m \* + zero (u - 2) \* + ones (m + 1) (m + int k') \* + <(-2 + ma = m + int k')> \* zero (ma - 1) \* reps' ma (ia + 1) ks' \* 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]) \* fam_conj {ia<..} zero) = + (reps' u (ia + 1) (take a ks @ [ks ! a]) \* 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] \* 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 \* ps m \* (reps u m ((take a ks)@[ks!a]) \* <(ia = m)>) + \* zero (ia + 1) \* zero (u - 1) \* + zero (2 + ia) \* zero (u - 2) \* 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) + qed +qed + +lemma tm_hoare_dec_fail01: + assumes "length ks \ a" + shows "\st i \* ps u \* zero (u - 2) \* zero (u - 1) \* reps u ia ks \* fam_conj {ia<..} zero\ + i :[ Dec a e ]: j + \st e \* ps u \* zero (u - 2) \* zero (u - 1) \* + reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks)) (list_ext a ks[a := 0]) \* + fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) <..} zero\" + 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 \* ps u \* zero (u - 2) \* + zero (u - 1) \* reps u ia ks \* fam_conj {ia<..} zero \* + <(ia = u + int (reps_len ks) - 1)>" in tm.pre_stren) + apply hstep + (* apply (hstep hoare_locate_set_gen[OF `length ks \ 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 \* ps m \* reps u m (take a (list_ext a ks) @ [0]) \* zero (w + 1) \* + <(w = m + int 0)> \* zero (u - 1) \* + fam_conj {w + 1<..} zero \* zero (u - 2) \* + <(ia = u + int (reps_len ks) - 1)>" in tm.pre_stren) + my_block + have "(take a (list_ext a ks)) @ [0] \ []" 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 \ ia = u + int (reps_len ks) - 1" + and h: "(ps u \* + st e \* + zero (u - 1) \* + zero (m + 1) \* + fam_conj {m + 1<..} zero \* zero (u - 2) \* 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 \* + st e \* + zero (u - 1) \* + zero (u - 2) \* + fam_conj {u + (-1 + int (reps_len (list_ext a ks)))<..} zero \* + 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 \ 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 \ 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)) \* ones m m \* 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 \* ps u \* zero (u - 2) \* zero (u - 1) \* + reps u ia ks \* 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 \* ps u \* zero (u - 2) \* zero (u - 1) \* reps u ia ks \* + fam_conj {ia<..} zero \* <(ia = u + int (reps_len ks) - 1)>) s" + by (unfold eq_ia, simp) + my_block_end + by (rule this, assumption) + +lemma t_hoare_label1: + "(\l. l = i \ \st l \* p\ l :[ c l ]: j \st k \* q\) \ + \st l \* p \ + i:[(TLabel l; c l)]:j + \st k \* q\" +by (unfold tassemble_to.simps, intro tm.code_exI tm.code_condI, clarify, auto) + +lemma tm_hoare_dec_fail1: + assumes "a < length ks \ ks ! a = 0 \ length ks \ a" + shows "\st i \* ps u \* zero (u - 2) \* zero (u - 1) \* reps u ia ks \* fam_conj {ia<..} zero\ + i :[ Dec a e ]: j + \st e \* ps u \* zero (u - 2) \* zero (u - 1) \* + reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks)) (list_ext a ks[a := 0]) \* + fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) <..} zero\" + using assms +proof + assume "a < length ks \ ks ! a = 0" + thus ?thesis + by (rule tm_hoare_dec_fail00) +next + assume "length ks \ a" + thus ?thesis + by (rule tm_hoare_dec_fail01) +qed + +lemma shift_left_nil_gen[step]: + assumes "u = v" + shows "\st i \* ps u \* zero v\ + i :[shift_left]:j + \st j \* ps u \* zero v\" + apply(unfold assms shift_left_def, intro t_hoare_local t_hoare_label, clarify, + rule t_hoare_label_last, simp, clarify, prune, simp) + by hstep + +lemma tm_hoare_dec_suc1: + assumes "a < length ks \ ks ! a = Suc v" + shows "\st i \* ps u \* zero (u - 2) \* zero (u - 1) \* reps u ia ks \* fam_conj {ia<..} zero\ + i :[ Dec a e ]: j + \st j \* ps u \* zero (u - 2) \* zero (u - 1) \* + reps u (ia - 1) (list_ext a ks[a := v]) \* + fam_conj {ia - 1<..} zero\" +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) \* fam_conj {ia<..} zero) = + (reps' u (ia + 1) ((take a ks @ [ks ! a]) @ drop (Suc a) ks) \* 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 \* + ps mb \* + zero (u - 1) \* + reps' u (mb - 1) (take a ks) \* + reps' mb (m - 1) [ks ! a] \* + one m \* + zero (u - 2) \* + ones (m + 1) (m + int k') \* + <(-2 + ma = m + int k')> \* zero (ma - 1) \* reps' ma (ia + 1) ks' \* 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 \ 0" by simp + from hoare_if_reps_nz_true[OF this, where u = mb and v = "m - 2"] + have "\st i \* ps mb \* reps mb (-2 + m) [ks ! a]\ + i :[ if_reps_nz l ]: j + \st l \* ps mb \* reps mb (-2 + m) [ks ! a]\" + 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' \* ps mb \* zero (u - 1) \* reps' u (mb - 1) (take a ks) \* + ((ones mb (mb + int (ks ! a)) \* <(-2 + m = mb + int (ks ! a))>) \* zero (mb + int (ks ! a) + 1)) \* + one (mb + int (ks ! a) + 2) \* zero (u - 2) \* + ones (mb + int (ks ! a) + 3) (mb + int (ks ! a) + int k' + 2) \* + <(-2 + ma = m + int k')> \* zero (ma - 1) \* reps' ma (ia + 1) ks' \* 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) \* 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 \* + ps (mb + int (Suc v) + 2) \* zero (mb + int (Suc v) + 1) \* + reps (mb + int (Suc v) + 2) ia (drop (Suc a) ks) \* zero (ia + 1) \* zero (ia + 2) \* + zero (mb + int (Suc v)) \* + ones mb (mb + int v) \* + zero (u - 1) \* + reps' u (mb - 1) (take a ks) \* + zero (u - 2) \* 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 \* ps (ia - 1) \* zero (u - 2) \* zero (u - 1) \* + reps u (ia - 1) (take a ks @ [v] @ drop (Suc a) ks) \* + zero ia \* zero (ia + 1) \* zero (ia + 2) \* + 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]) \* fam_conj {ia<..} zero) = + (reps' u (ia + 1) (take a ks @ [ks ! a]) \* 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 \* ps m \* zero (u - 1) \* reps' u (m - 1) (take a ks) \* + reps' m (ia + 1) [ks ! a] \* zero (2 + ia) \* zero (u - 2) \* 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] \* 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 \ 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) \* 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 \* ps (m + int v) \* zero (u - 2) \* zero (u - 1) \* + reps u (m + int v) (take a ks @ [v]) \* zero (m + (1 + int v)) \* + zero (2 + (m + int v)) \* zero (3 + (m + int v)) \* + 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) + qed +qed + +definition "cfill_until_one = (TL start exit. + TLabel start; + if_one exit; + write_one; + move_left; + jmp start; + TLabel exit + )" + +lemma hoare_cfill_until_one: + "\st i \* ps v \* one (u - 1) \* zeros u v\ + i :[ cfill_until_one ]: j + \st j \* ps (u - 1) \* ones (u - 1) v \" +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 hstep +next + case (Step x y) + show ?case + apply (rule_tac q = "st i \* ps (y - 1) \* one (x - 1) \* zeros x (y - 1) \* 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 "\st i \* ps (y - 1) \* one (x - 1) \* zeros x (y - 1)\ + i :[ jmp l ]: j + \st l \* ps (y - 1) \* one (x - 1) \* zeros x (y - 1)\" + 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) +qed + +definition "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 \ k" + shows "\st i \* ps (v + 2 + int w) \* zero (u - 1) \* + reps u (v - int w) [k - w] \* zeros (v - int w + 1) (v + 1) \* + one (v + 2) \* ones (v + 3) (v + 2 + int w) \* zeros (v + 3 + int w) (v + int(reps_len [k]) + 1)\ + i :[cmove]: j + \st j \* ps (u - 1) \* zero (u - 1) \* reps u u [0] \* zeros (u + 1) (v + 1) \* + reps (v + 2) (v + int (reps_len [k]) + 1) [k]\" + using assms +proof(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 \* ps (v + 2 + int k) \* zero (u - 1) \* + reps u u [0] \* zeros (u + 1) (v + 1) \* + ones (v + 2) (v + 2 + int k) \* zeros (v + 3 + int k) (2 + (v + int k)) \* + <(u = v - int k)>" + in tm.pre_stren) + my_block + fix i j + have "\st i \* ps (v + 2 + int k) \* zeros (u + 1) (v + 1) \* ones (v + 2) (v + 2 + int k) + \* <(u = v - int k)>\ + i :[ left_until_zero ]: j + \st j \* ps (v + 1) \* zeros (u + 1) (v + 1) \* ones (v + 2) (v + 2 + int k) + \* <(u = v - int k)>\" + 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 \* 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 "\st i \* ps (v + 1) \* reps u u [0] \* zeros (u + 1) (v + 1)\ + i :[left_until_one]:j + \st j \* ps u \* reps u u [0] \* zeros (u + 1) (v + 1)\" + 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 \ k` + have h: "k' = k - (Suc w)" "Suc w \ 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 "\st i \* ps (v + 2 + int w) \* zeros (v - int w + 1) (v + 1) \* + one (v + 2) \* ones (v + 3) (v + 2 + int w) \ + i :[left_until_zero]: j + \st j \* ps (v + 1) \* zeros (v - int w + 1) (v + 1) \* + one (v + 2) \* ones (v + 3) (v + 2 + int w) \" + my_block + have "(one (v + 2) \* 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 \* 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 "\st i \* ps (v + 1) \* reps u (v - int w) [k - w] \* zeros (v - int w + 1) (v + 1)\ + i :[left_until_one]: j + \st j \* ps (v - int w) \* reps u (v - int w) [k - w] \* zeros (v - int w + 1) (v + 1)\" + 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] \* 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 \ (p::tassert) = q)" + have "( \* p) = ( \* q)" + by (metis `b \ 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 "\ (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 "\st i \* ps (v - int w) \* + (reps u (v - (1 + int w)) [k - Suc w] \* one (v - int w))\ + i :[ move_left]: j + \st j \* ps (v - (1 + int w)) \* + (reps u (v - (1 + int w)) [k - Suc w] \* one (v - int w))\" + 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 "\st i' \* ps (v - (1 + int w)) \* reps u (v - (1 + int w)) [k - Suc w]\ + i' :[ if_zero j ]: j' + \st j' \* ps (v - (1 + int w)) \* reps u (v - (1 + int w)) [k - Suc w]\" + 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 "\st i \* ps (v - (1 + int w)) \* reps u (v - (1 + int w)) [k - Suc w]\ + i :[ move_right ]: j + \st j \* ps (v - int w) \* reps u (v - (1 + int w)) [k - Suc w] \" + 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 "\st i \* ps (v - int w) \* one (v + 2) \* + zero (v - int w) \* zeros (v - int w + 1) (v + 1)\ + i :[right_until_one]: j + \st j \* ps (v + 2) \* one (v + 2) \* zero (v - int w) \* zeros (v - int w + 1) (v + 1)\" + my_block + have "(zero (v - int w) \* 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) \* 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 "\st i \* ps (v + 2) \* zero (v + 3 + int w) \* zeros (4 + (v + int w)) (2 + (v + int k)) \* + one (v + 2) \* ones (v + 3) (v + 2 + int w)\ + i :[right_until_zero]: j + \st j \* ps (v + 3 + int w) \* zero (v + 3 + int w) \* zeros (4 + (v + int w)) (2 + (v + int k)) \* + one (v + 2) \* ones (v + 3) (v + 2 + int w)\" + my_block + have "(one (v + 2) \* 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) \* 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) \* 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) +qed + +definition "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 + "\st i \* ps u \* zero (u - 2) \* zero (u - 1) \* reps u v [k] \* zero (v + 1) \* + zeros (v + 2) (v + int(reps_len [k]) + 1)\ + i :[copy]: j + \st j \* ps u \* zero (u - 2) \* zero (u - 1) \* reps u v [k] \* zero (v + 1) \* + reps (v + 2) (v + int (reps_len [k]) + 1) [k]\" + apply (unfold copy_def) + my_block + fix i j + have + "\st i \* ps u \* reps u v [k] \* zero (v + 1) \* zeros (v + 2) (v + int(reps_len [k]) + 1)\ + i :[cinit]: j + \st j \* ps (v + 2) \* reps u v [k] \* zero (v + 1) \* + one (v + 2) \* zeros (v + 3) (v + int(reps_len [k]) + 1)\" + 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) \* 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' \* ps (v + 2) \* reps u v [k] \* zero (v + 1) \* + one (v + 2) \* zeros (v + 3) (v + int (reps_len [k]) + 1) \* zero (u - 2) \* zero (u - 1) \* + <(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 "\st i \* ps (v + 2) \* zero (u - 1) \* reps u v [k] \* zero (v + 1) \* + one (v + 2) \* zeros (v + 3) (v + int(reps_len [k]) + 1)\ + i :[cmove]: j + \st j \* ps (u - 1) \* zero (u - 1) \* reps u u [0] \* zeros (u + 1) (v + 1) \* + reps (v + 2) (v + int (reps_len [k]) + 1) [k]\" + 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 \ v = u + int (reps_len [k]) - 1") + my_block + have "(zeros (u + 1) (u + int k + 1)) = (zeros (u + 1) (u + int k) \* 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 "\st i \* ps (u + int k) \* one u \* zeros (u + 1) (u + int k)\ + i :[ cfill_until_one ]: j + \st j \* ps u \* ones u (u + int k) \" + 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