Commit c0789d50 by Lawrence Paulson

### new entry ROBDD

parent 4e2a27a6d0a7
This diff is collapsed.
 section\Array List\ text\Most of this has been contributed by Peter Lammich.\ theory Array_List imports "../Separation_Logic_Imperative_HOL/Examples/Array_Blit" begin text\ This implements a datastructure that efficiently supports two operations: appending an element and looking up the nth element. The implementation is straightforward. \ text\ As underlying data structure an array is used. Since changing the length of an array requires copying, we double the size whenever the array needs to be expanded. We use a counter for the current length to track which elements are used and which are spares. \ type_synonym 'a array_list = "'a array \ nat" definition "is_array_list l \ \(a,n). \\<^sub>Al'. a \\<^sub>a l' * \(n \ length l' \ l = take n l' \ length l'>0)" definition "initial_capacity \ 16::nat" definition "arl_empty \ do { a \ Array.new initial_capacity default; return (a,0) }" lemma [sep_heap_rules]: "< emp > arl_empty " by (sep_auto simp: arl_empty_def is_array_list_def initial_capacity_def) definition "arl_nth \ \(a,n) i. do { Array.nth a i }" lemma [sep_heap_rules]: "i < is_array_list l a > arl_nth a i <\x. is_array_list l a * \(x = l!i) >" by (sep_auto simp: arl_nth_def is_array_list_def split: prod.splits) definition "arl_append \ \(a,n) x. do { len \ Array.len a; if n Array.upd n x a; return (a,n+1) } else do { let newcap = 2 * len; a \ array_grow a newcap default; a \ Array.upd n x a; return (a,n+1) } }" lemma [sep_heap_rules]: " < is_array_list l a > arl_append a x <\a. is_array_list (l@[x]) a >\<^sub>t" by (sep_auto simp: arl_append_def is_array_list_def take_update_last neq_Nil_conv split: prod.splits nat.split) lemma is_array_list_prec: "precise is_array_list" unfolding is_array_list_def[abs_def] apply(rule preciseI) apply(simp split: prod.splits) using preciseD snga_prec by fastforce lemma is_array_list_lengthIA: "is_array_list l li \\<^sub>A \(snd li = length l) * true" by(sep_auto simp: is_array_list_def split: prod.splits) find_consts "assn \ bool" lemma is_array_list_lengthI: "x \ is_array_list l li \ snd li = length l" using is_array_list_lengthIA by (metis (full_types) ent_pure_post_iff star_aci(2)) end
 section\Code export\ theory BDD_Code imports Level_Collapse begin text\For convenience reasons, the code export is in a separate theory. For Haskell, we only have to reactivate the original equation for @{term blit}. Other languages might need an implementation for it.\ lemma [code del]: "blit src si dst di len = blit' src (integer_of_nat si) dst (integer_of_nat di) (integer_of_nat len)" by (simp add: blit'_def) declare blit_def[code] export_code open iteci_lu notci andci orci nandci norci biimpci xorci ifci tci fci tautci emptyci graphifyci litci eqci checking Haskell end
 section\Tests and examples\ theory BDD_Examples imports Level_Collapse begin text\Just two simple examples:\ lemma " do { s \ emptyci; (t,s) \ tci s; tautci t s } <\r. \(r = True)>\<^sub>t" by sep_auto lemma " do { s \ emptyci; (a,s) \ litci 0 s; (b,s) \ litci 1 s; (c,s) \ litci 2 s; (t1i,s) \ orci a b s; (t1,s) \ andci t1i c s; (t2i1,s) \ andci a c s; (t2i2,s) \ andci b c s; (t2,s) \ orci t2i1 t2i2 s; eqci t1 t2 } <\>\<^sub>t" by sep_auto end \ No newline at end of file
This diff is collapsed.
 section\Boolean functions\ theory Bool_Func imports Main begin text\ The end result of our implementation is verified against these functions: \ type_synonym 'a boolfunc = "('a \ bool) \ bool" text\if-then-else on boolean functions.\ definition "bf_ite i t e \ (\l. if i l then t l else e l)" text\if-then-else is interesting because we can, together with constant true and false, represent all binary boolean functions using maximally two applications of it.\ abbreviation "bf_True \ (\l. True)" abbreviation "bf_False \ (\l. False)" text\A quick demonstration:\ definition "bf_and a b \ bf_ite a b bf_False" lemma "(bf_and a b) as \ a as \ b as" unfolding bf_and_def bf_ite_def by meson definition "bf_not b \ bf_ite b bf_False bf_True" lemma bf_not_alt: "bf_not a as \ \a as" unfolding bf_not_def bf_ite_def by meson text\For convenience, we want a few functions more:\ definition "bf_or a b \ bf_ite a bf_True b" definition "bf_lit v \ (\l. l v)" definition "bf_if v t e \ bf_ite (bf_lit v) t e" lemma bf_if_alt: "bf_if v t e = (\l. if l v then t l else e l)" unfolding bf_if_def bf_ite_def bf_lit_def .. definition "bf_nand a b = bf_not (bf_and a b)" definition "bf_nor a b = bf_not (bf_or a b)" definition "bf_biimp a b = (bf_ite a b (bf_not b))" lemma bf_biimp_alt: "bf_biimp a b = (\l. a l \ b l)" unfolding bf_biimp_def bf_not_def bf_ite_def by(simp add: fun_eq_iff) definition "bf_xor a b = bf_not (bf_biimp a b)" lemma bf_xor_alt: "bf_xor a b = (bf_ite a (bf_not b) b)" (* two application version *) unfolding bf_xor_def bf_biimp_def bf_not_def unfolding bf_ite_def by simp text\All of these are implemented and had their implementation verified.\ definition "bf_imp a b = bf_ite a b bf_True" lemma bf_imp_alt: "bf_imp a b = bf_or (bf_not a) b" unfolding bf_or_def bf_not_def bf_imp_def unfolding bf_ite_def unfolding fun_eq_iff by simp lemma [dest!,elim!]: "bf_False = bf_True \ False" "bf_True = bf_False \ False" unfolding fun_eq_iff by simp_all (* Occurs here and there as goal for sep_auto *) lemmas [simp] = bf_and_def bf_or_def bf_nand_def bf_biimp_def bf_xor_alt bf_nor_def bf_not_def subsection\Shannon decomposition\ text\ A restriction of a boolean function on a variable is creating the boolean function that evaluates as if that variable was set to a fixed value: \ definition "bf_restrict (i::'a) (val::bool) (f::'a boolfunc) \ (\v. f (v(i:=val)))" text \ Restrictions are useful, because they remove variables from the set of significant variables: \ definition "bf_vars bf = {v. \as. bf_restrict v True bf as \ bf_restrict v False bf as}" lemma "var \ bf_vars (bf_restrict var val ex)" unfolding bf_vars_def bf_restrict_def by(simp) text\ We can decompose calculating if-then-else into computing if-then-else of two triples of functions with one variable restricted to true / false. Given that the functions have finite arity, we can use this to construct a recursive definition. \ lemma brace90shannon: "bf_ite F G H ass = bf_ite (\l. l i) (bf_ite (bf_restrict i True F) (bf_restrict i True G) (bf_restrict i True H)) (bf_ite (bf_restrict i False F) (bf_restrict i False G) (bf_restrict i False H)) ass" unfolding bf_ite_def bf_restrict_def by (auto simp add: fun_upd_idem) end
 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(unfold star_aci(2)[symmetric]) apply(unfold star_aci(1)[symmetric]) (* black unfold magic *) apply(unfold star_aci(2)[symmetric]) apply blast (* 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]: " emptyci \<^sub>t" by(sep_auto simp: is_bdd_impl_def emptyci_def emptymi_def) lemma [sep_heap_rules]: "tmi' bdd = Some (p,bdd') \ 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') \ 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') \ ifci v t e bddi <\(pi,bddi'). is_bdd_impl bdd' bddi' * \(pi = p)>\<^sub>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 \ 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 \ ftci " "destrmi' ni bdd = Some FD \ ffi bdd = Some r \ ffci " "\v t e. destrmi' ni bdd = Some (IFD v t e) \ fii v t e bdd = Some r \ fici v t e " shows " case_ifexici ftci ffci fici ni bddi " 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 " 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 " 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 ''Cannot happen'') i s } }" declare iteci.simps[code] lemma iteci_rule: " ( mi.ite_impl i t e bdd = Some (p,bdd')) \ iteci i t e bddi <\(pi,bddi'). is_bdd_impl bdd' bddi' * \(pi=p )>\<^sub>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. iteci x1 x2 x3 bddi <\r. case r of (pi, bddi') \ is_bdd_impl r2 bddi' * \ (pi = r1)>\<^sub>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')) \ param_optci i t e bddi <\(pi,bddi'). is_bdd_impl bdd' bddi' * \(pi=p)>\<^sub>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) \ hm_lookup (i, t, e) (dcli bddi) <\(pi). is_bdd_impl bdd bddi * \(pi = p)>\<^sub>t" unfolding is_bdd_impl_def by (sep_auto) lemma bdd_hm_update_rule'[sep_heap_rules]: " 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 ''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')) \ iteci_lu i t e bddi <\(pi,bddi'). is_bdd_impl bdd' bddi' * \(pi=p )>\<^sub>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. iteci_lu x1 x2 x3 bddi <\r. case r of (pi, bddi') \ is_bdd_impl r2 bddi' * \ (pi = r1)>\<^sub>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