(* Title: thys/Abacus_Hoare.thy

   Author: Jian Xu, Xingyuan Zhang, and Christian Urban

   Modifications: Sebastiaan Joosten

*)

theory Abacus_Hoare

imports Abacus

begin

type_synonym abc_assert = "nat list \<Rightarrow> bool"

definition 

  assert_imp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100)

where

  "assert_imp P Q \<equiv> \<forall>xs. P xs \<longrightarrow> Q xs"

fun abc_holds_for :: "(nat list \<Rightarrow> bool) \<Rightarrow> (nat \<times> nat list) \<Rightarrow> bool" ("_ abc'_holds'_for _" [100, 99] 100)

where

  "P abc_holds_for (s, lm) = P lm"  

(* Hoare Rules *)

(* halting case *)

(*consts abc_Hoare_halt :: "abc_assert \<Rightarrow> abc_prog \<Rightarrow> abc_assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)*)

fun abc_final :: "(nat \<times> nat list) \<Rightarrow> abc_prog \<Rightarrow> bool"

  where 

  "abc_final (s, lm) p = (s = length p)"

fun abc_notfinal :: "abc_conf \<Rightarrow> abc_prog \<Rightarrow> bool"

  where

  "abc_notfinal (s, lm) p = (s < length p)"

definition 

  abc_Hoare_halt :: "abc_assert \<Rightarrow> abc_prog \<Rightarrow> abc_assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)

where

  "abc_Hoare_halt P p Q \<equiv> \<forall>lm. P lm \<longrightarrow> (\<exists>n. abc_final (abc_steps_l (0, lm) p n) p \<and> Q abc_holds_for (abc_steps_l (0, lm) p n))"

lemma abc_Hoare_haltI:

  assumes "\<And>lm. P lm \<Longrightarrow> \<exists>n. abc_final (abc_steps_l (0, lm) p n) p \<and> Q abc_holds_for (abc_steps_l (0, lm) p n)"

  shows "{P} (p::abc_prog) {Q}"

unfolding abc_Hoare_halt_def 

using assms by auto

text {*

  {P} A {Q}   {Q} B {S} 

  -----------------------------------------

  {P} A [+] B {S}

*}

definition

  abc_Hoare_unhalt :: "abc_assert \<Rightarrow> abc_prog \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" 50)

where

  "abc_Hoare_unhalt P p \<equiv> \<forall>args. P args \<longrightarrow> (\<forall> n .abc_notfinal (abc_steps_l (0, args) p n) p)"

lemma abc_Hoare_unhaltI:

  assumes "\<And>args n. P args \<Longrightarrow> abc_notfinal (abc_steps_l (0, args) p n) p"

  shows "{P} (p::abc_prog) \<up>"

unfolding abc_Hoare_unhalt_def 

using assms by auto

fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst"

  where

  "abc_inst_shift (Inc m) n = Inc m" |

  "abc_inst_shift (Dec m e) n = Dec m (e + n)" |

  "abc_inst_shift (Goto m) n = Goto (m + n)"

fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list" 

  where

  "abc_shift xs n = map (\<lambda> x. abc_inst_shift x n) xs" 

fun abc_comp :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow> 

                           abc_inst list" (infixl "[+]" 99)

  where

  "abc_comp al bl = (let al_len = length al in 

                           al @ abc_shift bl al_len)"

lemma abc_comp_first_step_eq_pre: 

  "s < length A

 \<Longrightarrow> abc_step_l (s, lm) (abc_fetch s (A [+] B)) = 

    abc_step_l (s, lm) (abc_fetch s A)"

by(simp add: abc_step_l.simps abc_fetch.simps nth_append)

lemma abc_before_final: 

  "\<lbrakk>abc_final (abc_steps_l (0, lm) p n) p; p \<noteq> []\<rbrakk>

  \<Longrightarrow> \<exists> n'. abc_notfinal (abc_steps_l (0, lm) p n') p \<and> 

            abc_final (abc_steps_l (0, lm) p (Suc n')) p"

proof(induct n)

  case 0

  thus "?thesis"

    by(simp add: abc_steps_l.simps)

next

  case (Suc n)

  have ind: " \<lbrakk>abc_final (abc_steps_l (0, lm) p n) p; p \<noteq> []\<rbrakk> \<Longrightarrow> 

    \<exists>n'. abc_notfinal (abc_steps_l (0, lm) p n') p \<and> abc_final (abc_steps_l (0, lm) p (Suc n')) p"

    by fact

  have final: "abc_final (abc_steps_l (0, lm) p (Suc n)) p" by fact

  have notnull: "p \<noteq> []" by fact

  show "?thesis"

  proof(cases "abc_final (abc_steps_l (0, lm) p n) p")

    case True

    have "abc_final (abc_steps_l (0, lm) p n) p" by fact

    then have "\<exists>n'. abc_notfinal (abc_steps_l (0, lm) p n') p \<and> abc_final (abc_steps_l (0, lm) p (Suc n')) p"

      using ind notnull

      by simp

    thus "?thesis"

      by simp

  next

    case False

    have "\<not> abc_final (abc_steps_l (0, lm) p n) p" by fact

    from final this have "abc_notfinal (abc_steps_l (0, lm) p n) p" 

      by(case_tac "abc_steps_l (0, lm) p n", simp add: abc_step_red2 

        abc_step_l.simps abc_fetch.simps split: if_splits)

    thus "?thesis"

      using final

      by(rule_tac x = n in exI, simp)

  qed

qed

lemma notfinal_Suc:

  "abc_notfinal (abc_steps_l (0, lm) A (Suc n)) A \<Longrightarrow>  

  abc_notfinal (abc_steps_l (0, lm) A n) A"

apply(case_tac "abc_steps_l (0, lm) A n")

apply(simp add: abc_step_red2 abc_fetch.simps abc_step_l.simps split: if_splits)

done

lemma abc_comp_frist_steps_eq_pre: 

  assumes notfinal: "abc_notfinal (abc_steps_l (0, lm)  A n) A"

  and notnull: "A \<noteq> []"

  shows "abc_steps_l (0, lm) (A [+] B) n = abc_steps_l (0, lm) A n"

using notfinal

proof(induct n)

  case 0

  thus "?case"

    by(simp add: abc_steps_l.simps)

next

  case (Suc n)

  have ind: "abc_notfinal (abc_steps_l (0, lm) A n) A \<Longrightarrow> abc_steps_l (0, lm) (A [+] B) n = abc_steps_l (0, lm) A n"

    by fact

  have h: "abc_notfinal (abc_steps_l (0, lm) A (Suc n)) A" by fact

  then have a: "abc_notfinal (abc_steps_l (0, lm) A n) A"

    by(simp add: notfinal_Suc)

  then have b: "abc_steps_l (0, lm) (A [+] B) n = abc_steps_l (0, lm) A n"

    using ind by simp

  obtain s lm' where c: "abc_steps_l (0, lm) A n = (s, lm')"

    by (metis prod.exhaust)

  then have d: "s < length A \<and> abc_steps_l (0, lm) (A [+] B) n = (s, lm')" 

    using a b by simp

  thus "?case"

    using c

    by(simp add: abc_step_red2 abc_fetch.simps abc_step_l.simps nth_append)

qed

declare abc_shift.simps[simp del] abc_comp.simps[simp del]

lemma halt_steps2: "st \<ge> length A \<Longrightarrow> abc_steps_l (st, lm) A stp = (st, lm)"

apply(induct stp)

by(simp_all add: abc_step_red2 abc_steps_l.simps abc_step_l.simps abc_fetch.simps)

lemma halt_steps: "abc_steps_l (length A, lm) A n = (length A, lm)"

apply(induct n, simp add: abc_steps_l.simps)

apply(simp add: abc_step_red2 abc_step_l.simps nth_append abc_fetch.simps)

done

lemma abc_steps_add: 

  "abc_steps_l (as, lm) ap (m + n) = 

         abc_steps_l (abc_steps_l (as, lm) ap m) ap n"

apply(induct m arbitrary: n as lm, simp add: abc_steps_l.simps)

proof -

  fix m n as lm

  assume ind: 

    "\<And>n as lm. abc_steps_l (as, lm) ap (m + n) = 

                   abc_steps_l (abc_steps_l (as, lm) ap m) ap n"

  show "abc_steps_l (as, lm) ap (Suc m + n) = 

             abc_steps_l (abc_steps_l (as, lm) ap (Suc m)) ap n"

    apply(insert ind[of as lm "Suc n"], simp)

    apply(insert ind[of as lm "Suc 0"], simp add: abc_steps_l.simps)

    apply(case_tac "(abc_steps_l (as, lm) ap m)", simp)

    apply(simp add: abc_steps_l.simps)

    apply(case_tac "abc_step_l (a, b) (abc_fetch a ap)", 

          simp add: abc_steps_l.simps)

    done

qed

lemma equal_when_halt: 

  assumes exc1: "abc_steps_l (s, lm) A na = (length A, lma)"

  and exc2: "abc_steps_l (s, lm) A nb = (length A, lmb)"

  shows "lma = lmb"

proof(cases "na > nb")

  case True

  then obtain d where "na = nb + d"

    by (metis add_Suc_right less_iff_Suc_add)

  thus "?thesis" using assms halt_steps

    by(simp add: abc_steps_add)

next

  case False

  then obtain d where "nb = na + d"

    by (metis add.comm_neutral less_imp_add_positive nat_neq_iff)

  thus "?thesis" using assms halt_steps

    by(simp add: abc_steps_add)

qed 

lemma abc_comp_frist_steps_halt_eq': 

  assumes final: "abc_steps_l (0, lm) A n = (length A, lm')"

    and notnull: "A \<noteq> []"

  shows "\<exists> n'. abc_steps_l (0, lm) (A [+] B) n' = (length A, lm')"

proof -

  have "\<exists> n'. abc_notfinal (abc_steps_l (0, lm) A n') A \<and> 

    abc_final (abc_steps_l (0, lm) A (Suc n')) A"

    using assms

    by(rule_tac n = n in abc_before_final, simp_all)

  then obtain na where a:

    "abc_notfinal (abc_steps_l (0, lm) A na) A \<and> 

            abc_final (abc_steps_l (0, lm) A (Suc na)) A" ..

  obtain sa lma where b: "abc_steps_l (0, lm) A na = (sa, lma)"

    by (metis prod.exhaust)

  then have c: "abc_steps_l (0, lm) (A [+] B) na = (sa, lma)"

    using a abc_comp_frist_steps_eq_pre[of lm A na B] assms 

    by simp

  have d: "sa < length A" using b a by simp

  then have e: "abc_step_l (sa, lma) (abc_fetch sa (A [+] B)) = 

    abc_step_l (sa, lma) (abc_fetch sa A)"

    by(rule_tac abc_comp_first_step_eq_pre)

  from a have "abc_steps_l (0, lm) A (Suc na) = (length A, lm')"

    using final equal_when_halt

    by(case_tac "abc_steps_l (0, lm) A (Suc na)" , simp)

  then have "abc_steps_l (0, lm) (A [+] B) (Suc na) = (length A, lm')"

    using a b c e

    by(simp add: abc_step_red2)

  thus "?thesis"

    by blast

qed

lemma abc_exec_null: "abc_steps_l sam [] n = sam"

apply(cases sam)

apply(induct n)

apply(auto simp: abc_step_red2)

apply(auto simp: abc_step_l.simps abc_steps_l.simps abc_fetch.simps)

done

lemma abc_comp_frist_steps_halt_eq: 

  assumes final: "abc_steps_l (0, lm) A n = (length A, lm')"

  shows "\<exists> n'. abc_steps_l (0, lm) (A [+] B) n' = (length A, lm')"

using final

apply(case_tac "A = []")

apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps abc_exec_null)

apply(rule_tac abc_comp_frist_steps_halt_eq', simp_all)

done

lemma abc_comp_second_step_eq: 

  assumes exec: "abc_step_l (s, lm) (abc_fetch s B) = (sa, lma)"

  shows "abc_step_l (s + length A, lm) (abc_fetch (s + length A) (A [+] B))

         = (sa + length A, lma)"

using assms

apply(auto simp: abc_step_l.simps abc_fetch.simps nth_append abc_comp.simps abc_shift.simps split : if_splits )

apply(case_tac [!] "B ! s", auto simp: Let_def)

done

lemma abc_comp_second_steps_eq:

  assumes exec: "abc_steps_l (0, lm) B n = (sa, lm')"

  shows "abc_steps_l (length A, lm) (A [+] B) n = (sa + length A, lm')"

using assms

proof(induct n arbitrary: sa lm')

  case 0

  thus "?case"

    by(simp add: abc_steps_l.simps)

next

  case (Suc n)

  have ind: "\<And>sa lm'. abc_steps_l (0, lm) B n = (sa, lm') \<Longrightarrow> 

    abc_steps_l (length A, lm) (A [+] B) n = (sa + length A, lm')" by fact

  have exec: "abc_steps_l (0, lm) B (Suc n) = (sa, lm')" by fact

  obtain sb lmb where a: " abc_steps_l (0, lm) B n = (sb, lmb)"

    by (metis prod.exhaust)

 then have "abc_steps_l (length A, lm) (A [+] B) n = (sb + length A, lmb)"

   using ind by simp

 moreover have "abc_step_l (sb + length A, lmb) (abc_fetch (sb + length A) (A [+] B)) = (sa + length A, lm') "

   using a exec abc_comp_second_step_eq

   by(simp add: abc_step_red2)    

 ultimately show "?case"

   by(simp add: abc_step_red2)

qed

lemma length_abc_comp[simp, intro]: 

  "length (A [+] B) = length A + length B"

by(auto simp: abc_comp.simps abc_shift.simps)   

lemma abc_Hoare_plus_halt : 

  assumes A_halt : "{P} (A::abc_prog) {Q}"

  and B_halt : "{Q} (B::abc_prog) {S}"

  shows "{P} (A [+] B) {S}"

proof(rule_tac abc_Hoare_haltI)

  fix lm

  assume a: "P lm"

  then obtain na lma where 

    "abc_final (abc_steps_l (0, lm) A na) A"

    and b: "abc_steps_l (0, lm) A na = (length A, lma)"

    and c: "Q abc_holds_for (length A, lma)"

    using A_halt unfolding abc_Hoare_halt_def

    by (metis (full_types) abc_final.simps abc_holds_for.simps prod.exhaust)

  have "\<exists> n. abc_steps_l (0, lm) (A [+] B) n = (length A, lma)"

    using abc_comp_frist_steps_halt_eq b

    by(simp)

  then obtain nx where h1: "abc_steps_l (0, lm) (A [+] B) nx = (length A, lma)" ..   

  from c have "Q lma"

    using c unfolding abc_holds_for.simps

    by simp

  then obtain nb lmb where

    "abc_final (abc_steps_l (0, lma) B nb) B"

    and d: "abc_steps_l (0, lma) B nb = (length B, lmb)"

    and e: "S abc_holds_for (length B, lmb)"

    using B_halt unfolding abc_Hoare_halt_def

    by (metis (full_types) abc_final.simps abc_holds_for.simps prod.exhaust)

  have h2: "abc_steps_l (length A, lma) (A [+] B) nb = (length B + length A, lmb)"

    using d abc_comp_second_steps_eq

    by simp

  thus "\<exists>n. abc_final (abc_steps_l (0, lm) (A [+] B) n) (A [+] B) \<and>

    S abc_holds_for abc_steps_l (0, lm) (A [+] B) n"

    using h1 e

    by(rule_tac x = "nx + nb" in exI, simp add: abc_steps_add)

qed

lemma abc_unhalt_append_eq:

  assumes unhalt: "{P} (A::abc_prog) \<up>"

  and P: "P args"

  shows "abc_steps_l (0, args) (A [+] B) stp = abc_steps_l (0, args) A stp"

proof(induct stp)

  case 0

  thus "?case"

    by(simp add: abc_steps_l.simps)

next

  case (Suc stp)

  have ind: "abc_steps_l (0, args) (A [+] B) stp = abc_steps_l (0, args) A stp"

    by fact

  obtain s nl where a: "abc_steps_l (0, args) A stp = (s, nl)"

    by (metis prod.exhaust)

  then have b: "s < length A"

    using unhalt P

    apply(auto simp: abc_Hoare_unhalt_def)

    by (metis abc_notfinal.simps)

  thus "?case"

    using a ind

    by(simp add: abc_step_red2 abc_step_l.simps abc_fetch.simps nth_append abc_comp.simps)

qed

lemma abc_Hoare_plus_unhalt1: 

  "{P} (A::abc_prog) \<up> \<Longrightarrow> {P} (A [+] B) \<up>"

apply(rule_tac abc_Hoare_unhaltI)

apply(frule_tac args = args and B = B and stp = n in abc_unhalt_append_eq)

apply(simp_all add: abc_Hoare_unhalt_def)

apply(erule_tac x = args in allE, simp)

apply(erule_tac x = n in allE)

apply(case_tac "(abc_steps_l (0, args) A n)", simp)

done

lemma notfinal_all_before:

  "\<lbrakk>abc_notfinal (abc_steps_l (0, args) A x) A; y\<le>x \<rbrakk>

  \<Longrightarrow> abc_notfinal (abc_steps_l (0, args) A y) A "

apply(subgoal_tac "\<exists> d. x = y + d", auto)

apply(case_tac "abc_steps_l (0, args) A y",simp)

apply(rule_tac classical, simp add: abc_steps_add leI halt_steps2)

by arith

lemma abc_Hoare_plus_unhalt2':

  assumes unhalt: "{Q} (B::abc_prog) \<up>"

   and halt: "{P} (A::abc_prog) {Q}"

   and notnull: "A \<noteq> []"

   and P: "P args" 

   shows "abc_notfinal (abc_steps_l (0, args) (A [+] B) n) (A [+] B)"

proof -

  obtain st nl stp where a: "abc_final (abc_steps_l (0, args) A stp) A"

    and b: "Q abc_holds_for (length A, nl)"

    and c: "abc_steps_l (0, args) A stp = (st, nl)"

    using halt P unfolding abc_Hoare_halt_def

    by (metis abc_holds_for.simps prod.exhaust)

  thm abc_before_final

  obtain stpa where d: 

    "abc_notfinal (abc_steps_l (0, args) A stpa) A \<and> abc_final (abc_steps_l (0, args) A (Suc stpa)) A"

    using a notnull abc_before_final[of args A stp]

    by(auto)

  thus "?thesis"

  proof(cases "n < Suc stpa")

    case True

    have h: "n < Suc stpa" by fact

    then have "abc_notfinal (abc_steps_l (0, args) A n) A"

      using d

      by(rule_tac notfinal_all_before, auto)

    moreover then have "abc_steps_l (0, args) (A [+] B) n = abc_steps_l (0, args) A n"

      using notnull

      by(rule_tac abc_comp_frist_steps_eq_pre, simp_all)

    ultimately show "?thesis"

      by(case_tac "abc_steps_l (0, args) A n", simp)

  next

    case False

    have "\<not> n < Suc stpa" by fact

    then obtain d where i1: "n = Suc stpa + d"

      by (metis add_Suc less_iff_Suc_add not_less_eq)

    have "abc_steps_l (0, args) A (Suc stpa) = (length A, nl)"

      using d a c

      apply(case_tac "abc_steps_l (0, args) A stp", simp add: equal_when_halt)

      by(case_tac "abc_steps_l (0, args) A (Suc stpa)", simp add: equal_when_halt)

    moreover have  "abc_steps_l (0, args) (A [+] B) stpa = abc_steps_l (0, args) A stpa"

      using notnull d

      by(rule_tac abc_comp_frist_steps_eq_pre, simp_all)

    ultimately have i2: "abc_steps_l (0, args) (A [+] B) (Suc stpa) = (length A, nl)"

      using d

      apply(case_tac "abc_steps_l (0, args) A stpa", simp)

      by(simp add: abc_step_red2 abc_steps_l.simps abc_fetch.simps abc_comp.simps nth_append)

    obtain s' nl' where i3:"abc_steps_l (0, nl) B d = (s', nl')"

      by (metis prod.exhaust)

    then have i4: "abc_steps_l (0, args) (A [+] B) (Suc stpa + d) = (length A + s', nl')"

      using i2  apply(simp only: abc_steps_add)

      using abc_comp_second_steps_eq[of nl B d s' nl']

      by simp

    moreover have "s' < length B"

      using unhalt b i3

      apply(simp add: abc_Hoare_unhalt_def)

      apply(erule_tac x = nl in allE, simp)

      by(erule_tac x = d in allE, simp)

    ultimately show "?thesis"

      using i1

      by(simp)

  qed

qed

lemma abc_comp_null_left[simp]: "[] [+] A = A"

apply(induct A)

apply(case_tac [2] a)

apply(auto simp: abc_comp.simps abc_shift.simps abc_inst_shift.simps)

done

lemma abc_comp_null_right[simp]: "A [+] [] = A"

apply(induct A)

apply(case_tac [2] a)

apply(auto simp: abc_comp.simps abc_shift.simps abc_inst_shift.simps)

done

lemma abc_Hoare_plus_unhalt2:

  "\<lbrakk>{Q} (B::abc_prog)\<up>; {P} (A::abc_prog) {Q}\<rbrakk>\<Longrightarrow> {P} (A [+] B) \<up>"

apply(case_tac "A = []")

apply(simp add: abc_Hoare_halt_def abc_Hoare_unhalt_def abc_exec_null)

apply(rule_tac abc_Hoare_unhaltI)

apply(erule_tac abc_Hoare_plus_unhalt2', simp)

apply(simp, simp)

done

end