Theory ROBDD.Conc_Impl
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
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])
apply(simp only: star_aci(2)[symmetric])
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)
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
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]
lemma iteci_lu_code[code_unfold]: "iteci_lu i t e s = iteci_lu_code i t e s"
oops
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
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]
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
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