Theory Monadic_Language

subsection ‹A labeling VCG for a monadic language›

theory Monadic_Language
imports
  Complex_Main
  "../Case_Labeling"
  "HOL-Eisbach.Eisbach"
begin

ML_file ‹../util.ML›

ML ‹
  fun vcg_tac nt_rules nt_comb ctxt =
    let
      val rules = Named_Theorems.get ctxt nt_rules
      val comb = Named_Theorems.get ctxt nt_comb
    in REPEAT_ALL_NEW_FWD ( resolve_tac ctxt rules ORELSE' (resolve_tac ctxt comb THEN' resolve_tac ctxt rules)) end
›


text ‹This language is inspired by the languages used in AutoCorres \<^cite>‹greenaway_bridging_2012››

consts bind :: "'a option ⇒ ('a ⇒ 'b option) ⇒ 'b option" (infixr ‹|>>› 4)
consts return :: "'a ⇒ 'a option"
consts while :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ 'a option) ⇒ ('a ⇒ 'a option)"
consts valid :: "bool ⇒ 'a option ⇒ ('a ⇒ bool) ⇒ bool"

named_theorems vcg
named_theorems vcg_comb

method_setup vcg = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD (FIRSTGOAL (vcg_tac @{named_theorems "vcg"} @{named_theorems "vcg_comb"} ctxt)))
›


axiomatization where
   return[vcg]: "valid (Q x) (return x) Q" and
   bind[vcg]: "⟦⋀x. valid (R x) (c2 x) Q; valid P c1 R⟧ ⟹ valid P (bind c1 c2) Q" and
   while[vcg]: "⋀c. ⟦⋀x. valid (I x ∧ b x) (c x) I; ⋀x. I x ∧ ¬b x ⟹ Q x⟧ ⟹ valid (I x) (while b I c x) Q" and
   cond[vcg]: "⋀b c1 c2. valid P1 c1 Q ⟹ valid P2 c2 Q ⟹ valid (if b then P1 else P2) (if b then c1 else c2) Q" and
   case_prod[vcg]: "⋀P. ⟦⋀x y. v = (x,y) ⟹ valid (P x y) (B x y) Q⟧
    ⟹ valid (case v of (x,y) ⇒ P x y) (case v of (x,y) ⇒ B x y) Q" and
   conseq[vcg_comb]: "⟦valid P' c Q; P ⟹ P'⟧ ⟹ valid P c Q"


text ‹Labeled rules›

named_theorems vcg_l
named_theorems vcg_l_comb
named_theorems vcg_elim

method_setup vcg_l = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD (FIRSTGOAL (vcg_tac @{named_theorems "vcg_l"} @{named_theorems "vcg_l_comb"} ctxt)))
›

method vcg_l' = (vcg_l; (elim vcg_elim)?)

context begin
  interpretation Labeling_Syntax .

  lemma L_return[vcg_l]: "CTXT inp ct (Suc inp) (valid (P x) (return x) P)"
    unfolding LABEL_simps by (rule return)

  lemma L_bind[vcg_l]:
    assumes "⋀x. CTXT (Suc outp') ((''bind'',outp', [VAR x]) # ct) outp (valid (R x) (c2 x) Q)"
    assumes "CTXT inp ct outp' (valid P c1 R)"
    shows "CTXT inp ct outp (valid P (bind c1 c2) Q)"
    using assms unfolding LABEL_simps by (rule bind)

  lemma L_while[vcg_l]:
    fixes inp ct defines "ct' ≡ λx. (''while'', inp, [VAR x])  # ct"
    assumes "⋀x. CTXT (Suc inp) (ct' x) outp'
      (valid (BIND ''inv_pre'' inp (I x) ∧ BIND ''lcond'' inp (b x)) (c x) (λx. BIND ''inv_post'' inp (I x)))"
    assumes "⋀x. B⟨''inv_pre'',inp: I x⟩ ∧ B⟨''lcond'',inp: ¬b x⟩ ⟹ VC (''post'',outp' , []) (ct' x) (P x)"
    shows "CTXT inp ct (Suc outp') (valid (I x) (while b I c x) P)"
    using assms(2-) unfolding LABEL_simps by (rule while)

  lemma L_cond[vcg_l]:
    fixes inp ct defines "ct' ≡ (''if'',inp,[]) # ct"
    assumes "C⟨Suc inp, (''then'',inp,[]) # ct',outp: valid P1 c1 Q⟩"
    assumes "C⟨Suc outp, (''else'',outp,[]) # ct',outp': valid P2 c2 Q⟩"
    shows "C⟨inp,ct,outp': valid (if B⟨''cond'',inp: b⟩ then B⟨''then'',inp: P1⟩ else B⟨''else'',inp: P2⟩) (if b then c1 else c2) Q⟩"
    using assms(2-) unfolding LABEL_simps by (rule cond)

  lemma L_case_prod[vcg_l]:
    assumes "⋀x y. v = (x,y) ⟹ CTXT inp ct outp (valid (P x y) (B x y) Q)"
    shows "CTXT inp ct outp (valid (case v of (x,y) ⇒ P x y) (case v of (x,y) ⇒ B x y) Q)"
    using assms unfolding LABEL_simps by (rule case_prod)

  lemma L_conseq[vcg_l_comb]:
    assumes "CTXT (Suc inp) ct outp (valid P' c Q)"
    assumes "P ⟹ VC (''conseq'',inp,[]) ct P'"
    shows "CTXT inp ct outp (valid P c Q)"
    using assms unfolding LABEL_simps by (rule conseq)

  lemma L_assm_conjE[vcg_elim]:
    assumes "BIND name inp (P ∧ Q)" obtains "BIND name inp P" "BIND name inp Q"
    using assms unfolding LABEL_simps by auto

  declare conjE[vcg_elim]

end



lemma dvd_div:
  fixes a b c :: int
  assumes "a dvd b" "c dvd b" "coprime a c"
  shows "a dvd (b div c)"
  using assms coprime_dvd_mult_left_iff by fastforce

lemma divides: "
valid
  (0 < (a :: int))
  (
    return a
    |>> (λn.
      while
        (λn. even n)
        (λn. 0 < n ∧ n dvd a ∧ (∀m. odd m ∧ m dvd a ⟶ m dvd n))
        (λn. return (n div 2))
        n
    )
  )
  (λr. odd r ∧ r dvd a ∧ (∀m. odd m ∧ m dvd a ⟶ m ≤ r))
"
  apply vcg
    apply (auto simp add: zdvd_imp_le dvd_div elim!:
      evenE intro: dvd_mult_right)
  done

lemma L_divides: "
valid
  (0 < (a :: int))
  (
    return a
    |>> (λn.
      while
        (λn. even n)
        (λn. 0 < n ∧ n dvd a ∧ (∀m. odd m ∧ m dvd a ⟶ m dvd n))
        (λn. return (n div 2))
        n
    )
  )
  (λr. odd r ∧ r dvd a ∧ (∀m. odd m ∧ m dvd a ⟶ m ≤ r))
"
  apply (rule Initial_Label)
  apply vcg_l'
proof casify
print_nested_cases
  case bind
  { case (while n)
    { case post then show ?case by (auto simp: zdvd_imp_le)
    next
      case conseq
      from ‹0 < n› ‹even n› have "0 < n div 2"
        by (simp add: pos_imp_zdiv_pos_iff zdvd_imp_le)
      moreover
      from ‹n dvd a› ‹even n› have "n div 2 dvd a"
        by (metis dvd_div_mult_self dvd_mult_left)
      moreover
      { fix m assume "odd m" "m dvd a"
        then have "m dvd n" using conseq.inv_pre(3) by simp
        moreover note ‹even n›
        moreover from ‹odd m› have "coprime m 2"
         by (metis dvd_eq_mod_eq_0 invertible_coprime mult_cancel_left2 not_mod_2_eq_1_eq_0)
        ultimately
        have "m dvd n div 2" by (rule dvd_div)
      }
      ultimately show ?case by auto
    }
  next
    case conseq then show ?case by auto
  }
qed



lemma add: "
valid
  True
  (
    while
      ― ‹COND:› (λ(r,j). j < (b :: nat))
      ― ‹INV:› (λ(r,j). j ≤ b ∧ r = a + j)
      ― ‹BODY:› (λ(r,j). return (r + 1, j + 1))
      ― ‹START:› (a,0)
    |>> (λ(r,_). return r)
  )
  (λr. r = a + b)
"
  by vcg auto


lemma mult: "
valid
  True
  (
    while
      ― ‹COND:› (λ(r,i). i < (a :: nat))
      ― ‹INV:› (λ(r,i). i ≤ a ∧ r = i * b)
      ― ‹BODY:› (λ(r,i).
        while
          ― ‹COND:› (λ(r,j). j < b)
          ― ‹INV:› (λ(r,j). i < a ∧ j ≤ b ∧ r = i * b + j)
          ― ‹BODY:› (λ(r,j). return (r + 1, j + 1))
          ― ‹START:› (r,0)
        |>> (λ(r,_). return (r, i + 1))
      )
      ― ‹START:› (0,0)
    |>> (λ(r,_). return r)
  )
  (λr. r = a * b)
"
  by vcg auto


section ‹Labeled›

lemma L_mult: "
valid
  True
  (
    while
      ― ‹COND:› (λ(r,i). i < (a :: nat))
      ― ‹INV:› (λ(r,i). i ≤ a ∧ r = i * b)
      ― ‹BODY:› (λ(r,i).
        while
          ― ‹COND:› (λ(r,j). j < b)
          ― ‹INV:› (λ(r,j). i < a ∧ j ≤ b ∧ r = i * b + j)
          ― ‹BODY:› (λ(r,j). return (r + 1, j + 1))
          ― ‹START:› (r,0)
        |>> (λ(r,_). return (r, i + 1))
      )
      ― ‹START:› (0,0)
    |>> (λ(r,_). return r)
  )
  (λr. r = a * b)
"
  apply (rule Initial_Label)
  apply vcg_l'
proof casify
  case while
  { case while
    { case post then show ?case by auto
    next
      case conseq then show ?case by auto
    }
  next
    case post then show ?case by auto
  next
    case conseq then show ?case by auto
  }
next
  case conseq then show ?case by auto
qed

lemma L_paths: "
valid
  (path ≠ [])
  ( while
      ― ‹COND:› (λ(p,r). p ≠ [])
      ― ‹INV:› (λ(p,r). distinct r ∧ hd (r @ p) = hd path ∧ last (r @ p) = last path)
      ― ‹BODY:› (λ(p,r).
        return (hd p)
        |>> (λx.
          if (r ≠ [] ∧ x = hd r)
          then return []
          else (if x ∈ set r
            then return (takeWhile (λy. y ≠ x) r)
            else return (r))
        |>> (λr'. return (tl p, r' @ [x])
        )
        )
        )
      ― ‹START:› (path, [])
    |>> (λ(_,r). return r)
  )
  (λr. distinct r ∧ hd r = hd path ∧ last r = last path)
"
  apply (rule Initial_Label)
  apply vcg_l'
proof casify
  case conseq then show ?case by auto
next
  case (while p r)
  { case conseq
    from conseq have "r = [] ⟹ ?case" by (cases p) auto
    moreover
    from conseq have "r ≠ [] ⟹ hd p = hd r ⟹ ?case" by (cases p) auto
    moreover
    { assume A: "r ≠ []" "hd p ≠ hd r"
      have "hd (takeWhile (λy. y ≠ hd p) r @ hd p # tl p) = hd r"
        using A by (cases r) auto
      moreover
      have "last (takeWhile (λy. y ≠ hd p) r @ hd p # tl p) = last (r @ p)"
        using A ‹p ≠ []› by auto
      moreover
      have "distinct (takeWhile (λy. y ≠ hd p) r @ [hd p])"
        using conseq by (auto dest: set_takeWhileD)
      ultimately
      have ?case using A conseq by auto
    }
    ultimately show ?case by blast
  next
    case post then show ?case by auto
  }
qed

end