Quelle  Conc_Impl.thy

section‹Imparative implementation›
theory Conc_Impl
imports Pointer_Map_Impl Middle_Impl
begin

record bddi =
  dpmi :: "(nat × nat × nat) pointermap_impl"
  dcli :: "((nat × nat × nat),nat) hashtable"
lemma bdd_exhaust: "dpm a = dpm b ==> dcl a = dcl b ==> a = (b :: bdd)" by simp

instantiation prod :: (default, default) default
begin
  definition "default_prod :: ('a × 'b) ≡ (default, default)"
  instance ..
end
(* can be found in "~~/src/HOL/Proofs/Extraction/Greatest_Common_Divisor" or "~~/src/HOL/Proofs/Lambda/WeakNorm" *)
instantiation nat :: default
begin
  definition "default_nat ≡ 0 :: nat"
  instance ..
end

definition "is_bdd_impl (bdd::bdd) (bddi::bddi) = is_pointermap_impl (dpm bdd) (dpmi bddi) * is_hashmap (dcl bdd) (dcli bddi)"

lemma is_bdd_impl_prec: "precise is_bdd_impl"
  apply(rule preciseI)
  apply(unfold is_bdd_impl_def)
  apply(clarsimp)
  apply(rename_tac a a' x y p F F')
  apply(rule bdd_exhaust)
   apply(rule_tac p = "dpmi p" and h = "(x,y)" in preciseD[OF is_pointermap_impl_prec])
   apply(unfold star_aci(1))
   apply blast
  apply(rule_tac p = "dcli p" and h = "(x,y)" in preciseD[OF is_hashmap_prec])
  apply(simp only: star_aci(2)[symmetric])
  apply(simp only: star_aci(1)[symmetric]) (* black unfold magic *)
  apply(simp only: star_aci(2)[symmetric])
  (* This proof is exactly the same as for pointermap. One could make a rule from it. *)
done

definition "emptyci :: bddi Heap ≡ do { ep ← pointermap_empty; ehm ← hm_new; return (dpmi=ep, dcli=ehm) }"
definition "tci bdd ≡ return (1::nat,bdd::bddi)"
definition "fci bdd ≡ return (0::nat,bdd::bddi)"
definition "ifci v t e bdd ≡ (if t = e then return (t, bdd) else do {
                              (p,u) ← pointermap_getmki (v, t, e) (dpmi bdd);
                              return (Suc (Suc p), dpmi_update (const u) bdd)
})"
definition destrci :: "nat ==> bddi ==> (nat, nat) IFEXD Heap" where
"destrci n bdd ≡ (case n of
  0 ==> return FD |
  Suc 0 ==> return TD |
  Suc (Suc p) ==> pm_pthi (dpmi bdd) p 🍋 (λ(v,t,e). return (IFD v t e)))"

term "mi.les"

lemma emptyci_rule[sep_heap_rules]: "<emp> emptyci <is_bdd_impl emptymi>_t"
  by(sep_auto simp: is_bdd_impl_def emptyci_def emptymi_def)

lemma [sep_heap_rules]: "tmi' bdd = Some (p,bdd')
  ==> <is_bdd_impl bdd bddi>
        tci bddi
      <λ(pi,bddi'). is_bdd_impl bdd' bddi' * ↑(pi = p)>"
  by (sep_auto simp: tci_def tmi'_def split: Option.bind_splits)

lemma [sep_heap_rules]: "fmi' bdd = Some (p,bdd')
  ==> <is_bdd_impl bdd bddi>
        fci bddi
      <λ(pi,bddi'). is_bdd_impl bdd' bddi' * ↑(pi = p)>"
by(sep_auto simp: fci_def fmi'_def split: Option.bind_splits)

lemma [sep_heap_rules]: "ifmi' v t e bdd = Some (p, bdd') ==>
  <is_bdd_impl bdd bddi> ifci v t e bddi
  <λ(pi,bddi'). is_bdd_impl bdd' bddi' * ↑(pi = p)>_t"
  apply(clarsimp simp: is_bdd_impl_def ifmi'_def simp del: ifmi.simps)
  by (sep_auto simp: ifci_def apfst_def map_prod_def is_bdd_impl_def bdd_sane_def
               split: prod.splits if_splits Option.bind_splits)

lemma destrci_rule[sep_heap_rules]: "
  destrmi' n bdd = Some r ==>
  <is_bdd_impl bdd bddi> destrci n bddi
  <λr'. is_bdd_impl bdd bddi * ↑(r' = r)>" 
  unfolding destrmi'_def apply (clarsimp split: Option.bind_splits)
  apply(cases "(n, bdd)" rule: destrmi.cases)
    by (sep_auto simp: destrci_def bdd_node_valid_def is_bdd_impl_def ifexd_valid_def bdd_sane_def
                 dest: p_valid_RmiI)+

term mi.restrict_top_impl

thm mi.case_ifexi_def

definition "case_ifexici fti ffi fii ni bddi ≡ do {
  dest ← destrci ni bddi;
  case dest of TD ==> fti | FD ==> ffi | IFD v ti ei ==> fii v ti ei
}"

lemma [sep_decon_rules]:
  assumes S: "mi.case_ifexi fti ffi fii ni bdd = Some r"
  assumes [sep_heap_rules]: 
    "destrmi' ni bdd = Some TD ==> fti bdd = Some r ==> <is_bdd_impl bdd bddi> ftci <Q>"
    "destrmi' ni bdd = Some FD ==> ffi bdd = Some r ==> <is_bdd_impl bdd bddi> ffci <Q>"
    "∧v t e. destrmi' ni bdd = Some (IFD v t e) ==> fii v t e bdd = Some r
     ==> <is_bdd_impl bdd bddi> fici v t e <Q> "
  shows "<is_bdd_impl bdd bddi> case_ifexici ftci ffci fici ni bddi <Q>"
  using S unfolding mi.case_ifexi_def apply (clarsimp split: Option.bind_splits IFEXD.splits)
  by (sep_auto simp: case_ifexici_def)+


definition "restrict_topci p vr vl bdd =
  case_ifexici
    (return p)
    (return p)
    (λv te ee. return (if v = vr then (if vl then te else ee) else p))
    p bdd"

lemma [sep_heap_rules]:
  assumes "mi.restrict_top_impl p var val bdd = Some (r,bdd')"
  shows "<is_bdd_impl bdd bddi> restrict_topci p var val bddi
          <λri. is_bdd_impl bdd bddi * ↑(ri = r)>"
  using assms unfolding mi.restrict_top_impl_def restrict_topci_def by sep_auto

fun lowest_topsci where
"lowest_topsci [] s = return None" |
"lowest_topsci (e#es) s =
    case_ifexici
      (lowest_topsci es s)
      (lowest_topsci es s)
      (λv t e. do {
      (rec) ← lowest_topsci es s;
        (case rec of
          Some u ==> return ((Some (min u v))) |
          None ==> return ((Some v)))
       }) e s"

declare lowest_topsci.simps[simp del]

lemma [sep_heap_rules]:
  assumes "mi.lowest_tops_impl es bdd = Some (r,bdd')"
  shows "<is_bdd_impl bdd bddi> lowest_topsci es bddi
  <λ(ri). is_bdd_impl bdd bddi * ↑(ri = r ∧ bdd'=bdd)>"
proof -
  note [simp] = lowest_topsci.simps mi.lowest_tops_impl.simps
  show ?thesis using assms
    apply (induction es arbitrary: bdd r bdd' bddi)
     apply (sep_auto) 
    (* Unfortunately, we have to split on destrmi'-cases manually, else sep-aut introduces schematic before case-split is done *)
    apply (clarsimp simp: mi.case_ifexi_def split: Option.bind_splits IFEXD.splits)
      apply (sep_auto simp: mi.case_ifexi_def)
     apply (sep_auto simp: mi.case_ifexi_def)
    apply (sep_auto simp: mi.case_ifexi_def)
    done
qed

partial_function(heap) iteci where
"iteci i t e s = do {
  (lt) ← lowest_topsci [i, t, e] s;
  case lt of
    Some a ==> do {
      ti ← restrict_topci i a True s;
      tt ← restrict_topci t a True s;
      te ← restrict_topci e a True s;
      fi ← restrict_topci i a False s;
      ft ← restrict_topci t a False s;
      fe ← restrict_topci e a False s;
      (tb,s') ← iteci ti tt te s;
      (fb,s'') ← iteci fi ft fe s';
      (ifci a tb fb s'')
     }
  | None ==> do {
    case_ifexici (return (t,s)) (return (e,s)) (λ_ _ _. raise STR ''Cannot happen'') i s
   }
  }"
declare iteci.simps[code]

lemma iteci_rule: "
  ( mi.ite_impl i t e bdd = Some (p,bdd')) ⟶
  <is_bdd_impl bdd bddi>
    iteci i t e bddi
  <λ(pi,bddi'). is_bdd_impl bdd' bddi' * ↑(pi=p )>_t"
  apply (induction arbitrary: i t e bddi bdd p bdd' rule: mi.ite_impl.fixp_induct)
    subgoal
      apply simp  (* Warning: Dragons ahead! *)
      using option_admissible[where P=
             "λ(((x1,x2),x3),x4) (r1,r2). ∀bddi.
              <is_bdd_impl x4 bddi>
                iteci x1 x2 x3 bddi
              <λr. case r of (p_i, bddi') ==> is_bdd_impl r2 bddi' * ↑ (p_i = r1)>_t"]
      apply auto[1]
      apply (fo_rule subst[rotated])
       apply (assumption)
      by auto
    subgoal by simp
    subgoal
      apply clarify
      apply (clarsimp split: option.splits Option.bind_splits prod.splits)
       apply (subst iteci.simps)
       apply (sep_auto)
      apply (subst iteci.simps)
      apply (sep_auto)
       unfolding imp_to_meta apply rprems
       apply simp
      apply sep_auto
       apply (rule fi_rule)
        apply rprems
        apply simp
       apply frame_inference
      by sep_auto
  done

declare iteci_rule[THEN mp, sep_heap_rules]

definition param_optci where
  "param_optci i t e bdd = do {
    (tr, bdd) ← tci bdd;
    (fl, bdd) ← fci bdd;
    id ← destrci i bdd;
    td ← destrci t bdd;
    ed ← destrci e bdd;
              return (
              if id = TD then Some t else
                        if id = FD then Some e else
                        if td = TD ∧ ed = FD then Some i else
                        if t = e then Some t else
                        if ed = TD ∧ i = t then Some tr else
                        if td = FD ∧ i = e then Some fl else
                        None, bdd)
  }"

lemma param_optci_rule: "
  ( mi.param_opt_impl i t e bdd = Some (p,bdd')) ==>
  <is_bdd_impl bdd bddi>
    param_optci i t e bddi
  <λ(pi,bddi'). is_bdd_impl bdd' bddi' * ↑(pi=p)>_t"
by (sep_auto simp add: mi.param_opt_impl.simps param_optci_def tmi'_def fmi'_def
             split: Option.bind_splits)

lemma bdd_hm_lookup_rule: "
  (dcl bdd (i,t,e) = p) ==>
  <is_bdd_impl bdd bddi>
    hm_lookup (i, t, e) (dcli bddi)
  <λ(pi). is_bdd_impl bdd bddi * ↑(pi = p)>_t"
unfolding is_bdd_impl_def by (sep_auto)

lemma bdd_hm_update_rule'[sep_heap_rules]:
  "<is_bdd_impl bdd bddi>
    hm_update k v (dcli bddi)
  <λr. is_bdd_impl (updS bdd k v) (dcli_update (const r) bddi) * true>"
unfolding is_bdd_impl_def updS_def by (sep_auto)

partial_function(heap) iteci_lu where
"iteci_lu i t e s = do {
  lu ← ht_lookup (i,t,e) (dcli s);
  (case lu of Some b ==> return (b,s)
    | None ==> do {
      (po,s) ← param_optci i t e s;
      (case po of Some b ==> do {
        return (b,s)}
      | None ==> do {
        (lt) ← lowest_topsci [i, t, e] s;
        (case lt of Some a ==> do {
        ti ← restrict_topci i a True s;
        tt ← restrict_topci t a True s;
        te ← restrict_topci e a True s;
        fi ← restrict_topci i a False s;
        ft ← restrict_topci t a False s;
        fe ← restrict_topci e a False s;
        (tb,s) ← iteci_lu ti tt te s;
        (fb,s) ← iteci_lu fi ft fe s;
        (r,s) ← ifci a tb fb s;
        cl ← hm_update (i,t,e) r (dcli s);
        return (r,dcli_update (const cl) s)
       }
         | None ==> raise STR ''Cannot happen'' )})
  })}"
  
term ht_lookup
declare iteci_lu.simps[code]
thm iteci_lu.simps[unfolded restrict_topci_def case_ifexici_def  param_optci_def lowest_topsci.simps]
partial_function(heap) iteci_lu_code where "iteci_lu_code i t e s = do {
  lu ← hm_lookup (i, t, e) (dcli s);
  case lu of None ==> let po = if i = 1 then Some t
                              else if i = 0 then Some e else if t = 1 ∧ e = 0 then Some i else if t = e then Some t else if e = 1 ∧ i = t then Some 1 else if t = 0 ∧ i = e then Some 0 else None
                     in case po of None ==> do {
                                       id ← destrci i s;
                                       td ← destrci t s;
                                       ed ← destrci e s;
                                       let a = (case id of IFD v t e ==> v);
                                       let a = (case td of IFD v t e ==> min a v | _ ==> a);
                                       let a = (case ed of IFD v t e ==> min a v | _ ==> a);
                                       let ti = (case id of IFD v ti ei ==> if v = a then ti else i | _ ==> i);
                                       let tt = (case td of IFD v ti ei ==> if v = a then ti else t | _ ==> t);
                                       let te = (case ed of IFD v ti ei ==> if v = a then ti else e | _ ==> e);
                                       let fi = (case id of IFD v ti ei ==> if v = a then ei else i | _ ==> i);
                                       let ft = (case td of IFD v ti ei ==> if v = a then ei else t | _ ==> t);
                                       let fe = (case ed of IFD v ti ei ==> if v = a then ei else e | _ ==> e);
                                       (tb, s) ← iteci_lu_code ti tt te s;
                                       (fb, s) ← iteci_lu_code fi ft fe s;
                                       (r, s) ← ifci a tb fb s;
                                       cl ← hm_update (i, t, e) r (dcli s);
                                       return (r, dcli_update (const cl) s)
                                     }
                        | Some b ==> return (b, s)
  | Some b ==> return (b, s)
}"

declare iteci_lu_code.simps[code]
(* reduced the run-time of our examples by around 30%.
  But we would need some efficient automated machinery to show this,
  and I'm not even sure how to correctly use induction correctly for this.
  Thus: Future work.*)
lemma iteci_lu_code[code_unfold]: "iteci_lu i t e s = iteci_lu_code i t e s"
oops

(* Proof by copy-paste *)
lemma iteci_lu_rule: "
  ( mi.ite_impl_lu i t e bdd = Some (p,bdd')) ⟶
  <is_bdd_impl bdd bddi>
    iteci_lu i t e bddi
  <λ(pi,bddi'). is_bdd_impl bdd' bddi' * ↑(pi=p )>_t"
  apply (induction arbitrary: i t e bddi bdd p bdd' rule: mi.ite_impl_lu.fixp_induct)
    subgoal
      apply simp  (* More Dragons *)
      using option_admissible[where P=
             "λ(((x1,x2),x3),x4) (r1,r2). ∀bddi.
              <is_bdd_impl x4 bddi>
                iteci_lu x1 x2 x3 bddi
              <λr. case r of (p_i, bddi') ==> is_bdd_impl r2 bddi' * ↑ (p_i = r1)>_t"]
      apply auto[1]
      apply (fo_rule subst[rotated])
       apply (assumption)
      by auto
    subgoal by simp
    subgoal
      apply clarify
      apply (clarsimp split: option.splits Option.bind_splits prod.splits)
      subgoal
        unfolding updS_def
        apply (subst iteci_lu.simps)
        apply (sep_auto)
         using bdd_hm_lookup_rule apply(blast)
        apply(sep_auto)
         apply(rule fi_rule)
          apply(rule param_optci_rule)
          apply(sep_auto)
         apply(sep_auto)
        apply(sep_auto)
         unfolding imp_to_meta
         apply(rule fi_rule)
          apply(rprems)
          apply(simp; fail)
         apply(sep_auto)
        apply(sep_auto)
         apply(rule fi_rule)
          apply(rprems)
          apply(simp; fail)
         apply(sep_auto)
         apply(sep_auto)
        unfolding updS_def by (sep_auto)
      subgoal
        apply(subst iteci_lu.simps)
        apply(sep_auto)
         using bdd_hm_lookup_rule apply(blast)
        apply(sep_auto)
         apply(rule fi_rule)
          apply(rule param_optci_rule)
          apply(sep_auto)
         apply(sep_auto)
        by (sep_auto)
      subgoal
        apply(subst iteci_lu.simps)
        apply(sep_auto)
         using bdd_hm_lookup_rule apply(blast)
        by(sep_auto)
      done
  done

subsection‹A standard library of functions›

declare iteci_rule[THEN mp, sep_heap_rules]


definition "notci e s ≡ do {
  (f,s) ← fci s;
  (t,s) ← tci s;
  iteci_lu e f t s
}"
definition "orci e1 e2 s ≡ do {
  (t,s) ← tci s;
  iteci_lu e1 t e2 s
}"
definition "andci e1 e2 s ≡ do {
  (f,s) ← fci s;
  iteci_lu e1 e2 f s
}"
definition "norci e1 e2 s ≡ do {
  (r,s) ← orci e1 e2 s;
  notci r s
}"
definition "nandci e1 e2 s ≡ do {
  (r,s) ← andci e1 e2 s;
  notci r s
}"
definition "biimpci a b s ≡ do {
  (nb,s) ← notci b s;
  iteci_lu a b nb s
}"
definition "xorci a b s ≡ do {
  (nb,s) ← notci b s;
  iteci_lu a nb b s
}"
definition "litci v bdd ≡ do {
  (t,bdd) ← tci bdd;
  (f,bdd) ← fci bdd;
  ifci v t f bdd
}"
definition "tautci v bdd ≡ do {
  d ← destrci v bdd;
  return (d = TD)
}"

subsection‹Printing›
text‹The following functions are exported unverified. They are intended for BDD debugging purposes.›

partial_function(heap) serializeci :: "nat ==> bddi ==> ((nat × nat) × nat) list Heap" where
"serializeci p s = do {
  d ← destrci p s;
  (case d of
    IFD v t e ==> do {
      r ← serializeci t s;
      l ← serializeci e s;
      return (remdups ([((p,t),1),((p,e),0)] @ r @ l))
    } |
    _ ==> return []
  )
}"
declare serializeci.simps[code]
(* This snaps to heap as a Monad, which is not intended, but irrelevant. *)
fun mapM where
"mapM f [] = return []" |
"mapM f (a#as) = do {
  r ← f a;
  rs ← mapM f as;
  return (r#rs)
}"
definition "liftM f ma = do { a ← ma; return (f a) }"
definition "sequence = mapM id"
term "liftM (map f)"
lemma "liftM (map f) (sequence l) = sequence (map (liftM f) l)"
  apply(induction l)
   apply(simp add: sequence_def liftM_def)
  apply(simp)
oops

(*http://stackoverflow.com/questions/23864965/string-of-nat-in-isabelle*)
fun string_of_nat :: "nat ==> string" where
  "string_of_nat n = (if n < 10 then [char_of_nat (48 + n)]
                                else string_of_nat (n div 10) @ [char_of_nat (48 + (n mod 10))])"

definition labelci :: "bddi ==> nat ==> (string × string × string) Heap" where
"labelci s n = do {
   d ← destrci n s;
   let son = string_of_nat n;
   let label = (case d of
     TD ==> ''T'' |
     FD ==> ''F'' |
     (IFD v _ _) ==> string_of_nat v);
   return (label, son, son @ ''[label='' @ label @ ''];\010'')
}"

definition "graphifyci1 bdd a ≡ do {
  let ((f,t),y) = a;
  let c = (string_of_nat f @ '' -> '' @ string_of_nat t);
  return (c @ (case y of 0 ==> '' [style=dotted]'' | Suc _ ==> '''') @ '';\010'')
}"

definition "trd = snd ∘ snd"
definition "fstp = apsnd fst"

definition "the_thing_By f l = (let
  nub = remdups (map fst l) in
  map (λe. (e, map snd (filter (λg. (f e (fst g))) l))) nub)"
definition "the_thing = the_thing_By (=)"


definition graphifyci :: "string ==> nat ==> bddi ==> string Heap" where
"graphifyci name ep bdd ≡ do {
  s ← serializeci ep bdd;
  let e = map fst s;
  l ← mapM (labelci bdd) (rev (remdups (map fst e @ map snd e)));
  let grp = (map (λl. foldr (λa t. t @ a @ '';'') (snd l) ''{rank=same;'' @ ''}\010'') (the_thing (map fstp l)));
  e ← mapM (graphifyci1 bdd) s;
  let emptyhlp = (case ep of 0 ==> ''F;\010'' | Suc 0 ==> ''T;\010'' | _ ==> '''');
  return (''digraph '' @ name @ '' {\010'' @ concat (map trd l) @ concat grp @ concat e @ emptyhlp @ ''}'')
}"

end