Theory BDD
theory BDD
imports
Evasive
ROBDD.Level_Collapse
ListLexorder
begin
section‹Executably converting Simplicial Complexes to BDDs›
text‹We already know how to convert a simplicial complex to a boolean function, and that to a BDT.
We could trivially convert convert boolean functions to BDDs the same way they are converted to BDTs,
but the conversion to BDTs necessarily takes an amount of steps exponential in the number of variables (vertices).
The following method avoids this exponential method.›
text‹This theory does not include a proof on the run-time complexity of the conversion.›
text ‹The basic idea is that each vertex in a simplicial complex corresponds to one
@{term True} line in the truth table of the inducing Boolean function.
This is captured by the following definition, which is part of the correctness assumptions of the final theorem.›
definition bf_from_sc :: "nat set set => (bool vec ⇒ bool)"
where "bf_from_sc K ≡ (λv. {i. i < dim_vec v ∧ ¬ (vec_index v i)} ∈ K)"
lemma bf_from_sc:
assumes sc: "simplicial_complex.simplicial_complex n K"
shows "simplicial_complex_induced_by_monotone_boolean_function n (bf_from_sc K) = K"
unfolding bf_from_sc_def simplicial_complex_induced_by_monotone_boolean_function_def
using sc
unfolding simplicial_complex.simplicial_complex_def
unfolding simplicial_complex.simplices_def
unfolding ceros_of_boolean_input_def
by auto (metis ceros_of_boolean_input_def dim_vec sc
simplicial_complex.ceros_of_boolean_input_in_set simplicial_complex.simplicial_complex_def)
definition boolfunc_from_sc :: "nat => nat set set ⇒ nat boolfunc"
where "boolfunc_from_sc n K ≡ λp. {i. i < n ∧ ¬ p i} ∈ K"
text‹The conversion proven correct in two major steps:
\begin{itemize}
\item Prove that we can convert the list form of simplicial complexes to boolean functions instead of the set form (@{text boolfunc_from_sc_list})
\item Prove that we can convert the list form of simplicial complexes to BDDs (@{text boolfunc_bdd_from_sc_list})
\end{itemize}
›
definition "sc_threshold_2_3 ≡ {{},{0::nat},{1},{2},{3},{0,1},{0,2},{0,3},{1,2},{1,3},{2,3}}"
text‹Example: The truth table (as separate lemmas) for @{const sc_threshold_2_3}:›
lemma hlp1: "{i. i < 4 ∧ ¬ (f(0 := a0, 1 := a1, 2 := a2, 3 := a3)) i} =
(if a0 then {} else {0::nat})
∪ (if a1 then {} else {1})
∪ (if a2 then {} else {2})
∪ (if a3 then {} else {3})"
by auto
lemma sc_threshold_2_3_ffff:
"boolfunc_from_sc 4 sc_threshold_2_3 (a (0:=False,1:=False,2:=False,3:=False)) = False"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def
by simp (smt (z3) Suc_eq_numeral insert_absorb insert_commute insert_ident
insert_not_empty numeral_2_eq_2 singleton_inject zero_neq_numeral)
lemma sc_threshold_2_3_ffft:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=False,1:=False,2:=False,3:=True)) = False"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def
by simp (smt (z3) Suc_eq_numeral insertI1 insert_absorb insert_commute
insert_ident insert_not_empty numeral_2_eq_2 singleton_inject zero_neq_numeral)
lemma sc_threshold_2_3_fftf:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=False,1:=False,2:=True,3:=False)) = False"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def
by simp (smt (z3) insertI1 insert_iff numeral_1_eq_Suc_0
numeral_2_eq_2 numeral_eq_iff semiring_norm(86) singleton_iff zero_neq_numeral)
lemma sc_threshold_2_3_ftff:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=False,1:=True,2:=False,3:=False)) = False"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def
by simp (smt (verit, ccfv_SIG) insert_absorb insert_iff insert_not_empty
numeral_eq_iff semiring_norm(89) zero_neq_numeral)
lemma sc_threshold_2_3_tfff:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=True,1:=False,2:=False,3:=False)) = False"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def
by simp (smt (z3) eval_nat_numeral(3) insertI1 insert_commute insert_iff
n_not_Suc_n numeral_1_eq_Suc_0 numeral_2_eq_2
numeral_eq_iff singletonD verit_eq_simplify(12))
lemma sc_threshold_2_3_fftt:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=False,1:=False,2:=True,3:=True)) = True"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def by auto
lemma sc_threshold_2_3_ftft:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=False,1:=True,2:=False,3:=True)) = True"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def by auto
lemma sc_threshold_2_3_fttf:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=False,1:=True,2:=True,3:=False)) = True"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def by auto
lemma sc_threshold_2_3_fttt:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=False,1:=True,2:=True,3:=True)) = True"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def by auto
lemma sc_threshold_2_3_tfft:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=True,1:=False,2:=False,3:=True)) = True"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def by auto
lemma sc_threshold_2_3_tftf:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=True,1:=False,2:=True,3:=False)) = True"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def by auto
lemma sc_threshold_2_3_tftt:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=True,1:=False,2:=True,3:=True)) = True"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def by auto
lemma sc_threshold_2_3_ttff:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=True,1:=True,2:=False,3:=False)) = True"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def by auto
lemma sc_threshold_2_3_ttft:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=True,1:=True,2:=False,3:=True)) = True"
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def by auto
lemma sc_threshold_2_3_tttf:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=True,1:=True,2:=True,3:=False)) = True "
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def by auto
lemma sc_threshold_2_3_tttt:
"boolfunc_from_sc 4 sc_threshold_2_3 (a(0:=True,1:=True,2:=True,3:=True)) = True "
unfolding hlp1 boolfunc_from_sc_def sc_threshold_2_3_def by auto
lemma "boolfunc_from_sc n UNIV = bf_True"
unfolding boolfunc_from_sc_def by simp
lemma "boolfunc_from_sc n {} = bf_False"
unfolding boolfunc_from_sc_def by simp
text‹This may seem like an extra step, but effectively, it means:
require that all the atoms outside the vertex are true,
but don't care about what's in the vertex.›
lemma boolfunc_from_sc_lazy:
"simplicial_complex.simplicial_complex n K
⟹ boolfunc_from_sc n K = (λp. Pow {i. i < n ∧ ¬ p i} ⊆ K)"
unfolding simplicial_complex.simplicial_complex_def boolfunc_from_sc_def
by auto
primrec boolfunc_from_vertex_list :: "nat list ⇒ nat list ⇒ (nat ⇒ bool) ⇒ bool"
where
"boolfunc_from_vertex_list n [] = bf_True" |
"boolfunc_from_vertex_list n (f#fs) =
bf_and (boolfunc_from_vertex_list n fs) (if f ∈ set n then bf_True else bf_lit f)"
lemma boolfunc_from_vertex_list_Cons:
"boolfunc_from_vertex_list (a # as) lUNIV =
(λv. (boolfunc_from_vertex_list as lUNIV) (v(a:=True)))"
by (induction lUNIV; simp add: bf_lit_def)
lemma boolfunc_from_vertex_list_Empty:
"boolfunc_from_vertex_list [] lUNIV = Ball (set lUNIV)"
by(induction lUNIV) (auto simp add: bf_lit_def)
lemma boolfunc_from_vertex_list:
"set lUNIV = {..<n} ⟹ boolfunc_from_vertex_list a lUNIV = (λp. {i. i < n ∧ ¬ p i} ⊆ set a)"
by (induction a; fastforce
simp add: boolfunc_from_vertex_list_Empty boolfunc_from_vertex_list_Cons)
primrec boolfunc_from_sc_list :: "nat list ⇒ nat list list ⇒ (nat ⇒ bool) ⇒ bool"
where
"boolfunc_from_sc_list lUNIV [] = bf_False" |
"boolfunc_from_sc_list lUNIV (l#L) =
bf_or (boolfunc_from_sc_list lUNIV L) (boolfunc_from_vertex_list l lUNIV)"
lemma boolfunc_from_sc_un:
"boolfunc_from_sc n (a∪b) = bf_or (boolfunc_from_sc n a) (boolfunc_from_sc n b)"
unfolding boolfunc_from_sc_def unfolding bf_or_def bf_ite_def by force
lemma bf_ite_const[simp]: "bf_ite bf_True a b = a" "bf_ite bf_False a b = b"
by (simp_all)
lemma Pow_subset_Pow: "Pow a ⊆ Pow b = (a ⊆ b)"
by blast
lemma boolfunc_from_sc_list_concat:
"boolfunc_from_sc_list lUNIV (a @ b) =
bf_or (boolfunc_from_sc_list lUNIV a) (boolfunc_from_sc_list lUNIV b)"
by (induction a; auto)
lemma boolfunc_from_sc_list_existing_useless:
"a ∈ set as ⟹ boolfunc_from_sc_list l (a # as) = boolfunc_from_sc_list l as"
proof(induction as)
case (Cons a1s as) then show ?case by (cases "a1s = a"; simp) metis
qed simp
primrec remove :: "'a ⇒ 'a list ⇒ 'a list"
where
"remove a [] = []" |
"remove a (a1 # as) = (if a = a1 then [] else [a1]) @ remove a as"
lemma set_remove[simp]: "set (remove a as) = set as - {a}"
by(induction as; auto)
lemma remove_concat[simp]: "remove a (a1 @ a2) = remove a a1 @ remove a a2"
by(induction a1; simp)
lemma boolfunc_from_sc_list_dedup1:
"boolfunc_from_sc_list l (a # as) = boolfunc_from_sc_list l (a # remove a as)"
proof(induction as)
case (Cons a1s as) then show ?case by(cases "a1s = a"; simp) metis
qed simp
lemma boolfunc_from_sc_list_reorder:
"set a = set b ⟹ boolfunc_from_sc_list l a = boolfunc_from_sc_list l b"
proof(induction a arbitrary: b)
next
case (Cons a1 a2)
then obtain b1 b2 where b: "b = b1 @ a1 # b2" by (metis list.set_intros(1) split_list)
have cons_concat: "⋀a as. a # as = [a] @ as" by simp
have bb: "boolfunc_from_sc_list l b =
bf_or (boolfunc_from_vertex_list a1 l)
(bf_or (boolfunc_from_sc_list l b1) (boolfunc_from_sc_list l b2))"
apply(subst b)
apply(subst boolfunc_from_sc_list_concat)
apply(subst cons_concat)
apply(subst boolfunc_from_sc_list_concat)
apply(auto)
done
have bbb: "boolfunc_from_sc_list l b = boolfunc_from_sc_list l (a1 # (remove a1 (b1 @ b2)))"
unfolding bb boolfunc_from_sc_list_dedup1[symmetric]
by (auto simp add: boolfunc_from_sc_list_concat)
show ?case proof(cases "a1 ∈ set a2")
case True
then show ?thesis using Cons by (metis insert_absorb list.set(2))
next
case False
then have a2: "set a2 = set (remove a1 (b1 @ b2))"
using Cons.prems b by fastforce
show ?thesis using Cons.IH[OF a2] bbb by simp
qed
qed simp
lemma boolfunc_from_sc_list:
"set lUNIV = {..<n::nat}
⟹ simplicial_complex.simplicial_complex n (set ` set L)
⟹ boolfunc_from_sc_list lUNIV L = boolfunc_from_sc n (set ` set L)"
proof -
assume lUNIV: "set lUNIV = {..<n::nat}"
assume sc: "simplicial_complex.simplicial_complex n (set ` set L)"
define sorted where "sorted ≡ sorted_wrt (λa b :: nat list. card (set b) ≤ card (set a))"
have i: "sorted L
⟹ simplicial_complex.simplicial_complex n (set ` set L)
⟹ boolfunc_from_sc_list lUNIV L = boolfunc_from_sc n (set ` set L)" for L
proof(induction L)
case Nil
show ?case by (simp add: boolfunc_from_sc_def)
next
case (Cons a L)
from Cons.prems(2) have p: "Pow (set a) ⊆ (set ` set (a # L))"
unfolding simplicial_complex.simplicial_complex_def by simp
hence pun: "insert (set a) (set ` set L) = Pow (set a) ∪ (set ` set L)" by auto
from p and Cons.prems(2)
have sp: "simplicial_complex.simplicial_complex n (Pow (set a))"
by (meson PowD Pow_subset_Pow simplicial_complex.simplicial_complex_def subsetD)
have bfSing: "boolfunc_from_sc_list lUNIV [a] = boolfunc_from_sc n (Pow (set a))"
unfolding boolfunc_from_sc_lazy [OF sp]
by (simp add: Pow_subset_Pow boolfunc_from_vertex_list [OF lUNIV])
have bflCons: "boolfunc_from_sc_list lUNIV (a # L) =
bf_or (boolfunc_from_sc_list lUNIV [a]) (boolfunc_from_sc_list lUNIV L)"
unfolding boolfunc_from_sc_list.simps(2) [of _ a L] by auto
from Cons.prems have "simplicial_complex.simplicial_complex n (set ` set L)"
unfolding simplicial_complex.simplicial_complex_def sorted_def
by simp (metis List.finite_set PowD card_seteq insert_image subset_insert)
from Cons.IH[OF _ this] Cons.prems(1)
have "boolfunc_from_sc_list lUNIV L = boolfunc_from_sc n (set ` set L)"
unfolding sorted_def by simp
thus ?case
apply(subst bflCons)
apply(simp del: boolfunc_from_sc_list.simps)
apply(subst pun)
apply(subst boolfunc_from_sc_un)
apply(subst bfSing)
apply(simp)
done
qed
define sort where "sort ≡ rev (sort_key (λl. card (set l)) L)"
have sc: "simplicial_complex.simplicial_complex n (set ` set sort)"
unfolding sort_def using sc by simp
have sorted: "sorted sort"
by(simp add: sorted_def sort_def sorted_wrt_rev) (metis sorted_map sorted_sort_key)
have set: "set sort = set L" unfolding sort_def by simp
from boolfunc_from_sc_list_reorder[OF set] i[OF sorted sc] set
show ?thesis by presburger
qed
lemma boolfunc_from_sc_alt: "boolfunc_from_sc n K = vec_to_boolfunc n (bf_from_sc K)"
unfolding boolfunc_from_sc_def vec_to_boolfunc_def bf_from_sc_def
unfolding dim_vec by(fastforce intro!: eqelem_imp_iff)
primrec bdd_from_vertex_list :: "nat list ⇒ nat list ⇒ bddi ⇒ (nat × bddi) Heap"
where
"bdd_from_vertex_list n [] s = tci s" |
"bdd_from_vertex_list n (f#fs) s = do {
(f, s) ← if f ∈ set n then tci s else litci f s;
(fs, s) ← bdd_from_vertex_list n fs s;
andci fs f s
}"
primrec bdd_from_sc_list :: "nat list ⇒ nat list list ⇒ bddi ⇒ (nat × bddi) Heap"
where
"bdd_from_sc_list lUNIV [] s = fci s" |
"bdd_from_sc_list lUNIV (l#L) s = do {
(l, s) ← bdd_from_vertex_list l lUNIV s;
(L, s) ← bdd_from_sc_list lUNIV L s;
orci L l s
}"
definition "nat_list_from_vertex v ≡ sorted_list_of_set v"
definition "nat_list_from_sc K ≡ sorted_list_of_list_set (nat_list_from_vertex ` K)"
definition "ex_2_3 ≡ do {
s ← emptyci;
(ex, s) ← bdd_from_sc_list [0, 1, 2, 3] (nat_list_from_sc sc_threshold_2_3) s;
graphifyci ''threshold_two_three'' ex s
}"
lemma nat_list_from_vertex:
assumes "finite l"
shows "set (nat_list_from_vertex l) = {i . i ∈ l}"
unfolding nat_list_from_vertex_def sorted_list_of_set_def
by auto (metis assms set_sorted_list_of_set sorted_list_of_set_def)+
lemma
finite_sorted_list_of_set:
assumes "finite L"
shows "finite (sorted_list_of_set ` L)"
using finite_imageI [OF assms, of sorted_list_of_set] .
lemma nat_list_from_sc:
assumes L: "finite L"
and l: "∀l∈L. finite l"
shows "set ` set (nat_list_from_sc (L :: nat set set)) = {{i . i ∈ l} | l. l ∈ L}"
unfolding nat_list_from_sc_def
unfolding nat_list_from_vertex_def
unfolding set_sorted_list_of_list_set [OF finite_sorted_list_of_set [OF L]]
proof (safe)
fix x :: "nat set"
assume xl: "x ∈ L"
hence fx: "finite x" using l by simp
show exl: "∃l. set (sorted_list_of_set x) = {i. i ∈ l} ∧ l ∈ L"
by (rule exI [of _ x], auto simp add: xl fx)
show "{i. i ∈ x} ∈ set ` sorted_list_of_set ` L"
by (metis Collect_mem_eq exl fx image_iff set_sorted_list_of_set)
qed
definition "ex_false ≡ do {
s ← emptyci;
(ex, s) ← bdd_from_sc_list [0, 1, 2, 3] (nat_list_from_sc {}) s;
graphifyci ''false'' ex s
}"
definition "ex_true ≡ do {
s ← emptyci;
(ex, s) ← bdd_from_sc_list [0, 1, 2, 3]
(nat_list_from_sc
{{},{0},{1},{2},{3},
{0,1},{0,2},{0,3},{1,2},{1,3},{2,3},
{0,1,2},{0,1,3},{0,2,3},{1,2,3},{0,1,2,3}}) s;
graphifyci ''true'' ex s
}"
definition "another_ex ≡ do {
s ← emptyci;
(ex, s) ← bdd_from_sc_list [0, 1, 2, 3]
(nat_list_from_sc
{{},{0},{1},{2},{3},
{0,1},{0,2},{0,3},{1,2},{1,3},{2,3},
{0,1,2},{0,1,3},{0,2,3},{1,2,3}}) s;
graphifyci ''another_ex'' ex s
}"
definition "one_another_ex ≡ do {
s ← emptyci;
(ex, s) ← bdd_from_sc_list [0, 1, 2, 3]
(nat_list_from_sc
{{},{0},{1},{2},{3},
{0,1},{0,2},{0,3},{1,2},{1,3},{2,3},
{0,1,2},{0,1,3},{1,2,3}}) s;
graphifyci ''one_another_ex'' ex s
}"
lemma bf_ite_direct[simp]: "bf_ite i bf_True bf_False = i" by simp
lemma andciI: "node_relator (tb, tc) rp ⟹ node_relator (eb, ec) rp ⟹ rq ⊆ rp ⟹
<bdd_relator rp s> andci tc ec s <λ(r,s'). bdd_relator (insert (bf_and tb eb,r) rq) s'>"
by sep_auto
lemma bdd_from_vertex_list[sep_heap_rules]:
shows "<bdd_relator rp s>
bdd_from_vertex_list n l s
<λ(r,s'). bdd_relator (insert (boolfunc_from_vertex_list n l, r) rp) s'>"
proof(induction l arbitrary: rp s)
case Nil then show ?case by (sep_auto)
next
case (Cons a l)
show ?case proof(cases "a ∈ set n")
case True
show ?thesis
apply(simp only: bdd_from_vertex_list.simps list.map
boolfunc_from_vertex_list.simps True if_True)
apply(sep_auto simp only:)
apply(rule Cons.IH)
apply(clarsimp simp del: bf_ite_def)
apply(sep_auto)
done
next
case False
show ?thesis
apply(simp only: bdd_from_vertex_list.simps list.map
boolfunc_from_vertex_list.simps False if_False)
apply(sep_auto simp only:)
apply(rule Cons.IH)
apply(sep_auto simp del: bf_ite_def bf_and_def)
done
qed
qed
lemma boolfunc_bdd_from_sc_list:
shows "<bdd_relator rp s>
bdd_from_sc_list lUNIV K s
<λ(r,s'). bdd_relator (insert (boolfunc_from_sc_list lUNIV K, r) rp) s'>"
proof(induction K arbitrary: rp s)
case Nil
then show ?case by sep_auto
next
case (Cons a K)
show ?case by(sep_auto heap add: Cons.IH simp del: bf_ite_def bf_or_def)
qed
lemma map_map_idI: "(⋀x. x ∈ ⋃(set ` set l) ⟹ f x = x) ⟹ map (map f) l = l"
by(induct l; simp; meson map_idI)
definition
"bdd_from_sc K n ≡ bdd_from_sc_list (nat_list_from_vertex {..<n}) (nat_list_from_sc K)"
theorem bdd_from_sc:
assumes "simplicial_complex.simplicial_complex n (K :: nat set set)"
shows "<bdd_relator rp s>
bdd_from_sc K n s
<λ(r,s'). bdd_relator (insert (vec_to_boolfunc n (bf_from_sc K), r) rp) s'>"
proof -
have fK: "finite K"
using simplicial_complex.finite_simplicial_complex [OF assms] .
have fv: "∀v∈K. finite v"
using simplicial_complex.finite_simplices [OF assms] ..
define lUNIV where lUNIV_def: "lUNIV = nat_list_from_vertex {..<n}"
hence set_lUNIV: "set lUNIV = {..<n}"
unfolding nat_list_from_vertex_def
using sorted_list_of_set(1) [OF finite_lessThan [of n]] by simp
define Klist where "Klist ≡ (nat_list_from_sc K)"
have Klist_set: "set ` set Klist = K"
using nat_list_from_sc [OF fK fv]
unfolding Klist_def nat_list_from_sc_def nat_list_from_vertex_def by simp
have Klist_map: "Klist = nat_list_from_sc K"
unfolding Klist_def ..
have sc_Klist: "simplicial_complex.simplicial_complex n (set ` set Klist)"
unfolding Klist_set using assms .
show ?thesis
apply (insert boolfunc_bdd_from_sc_list[of rp s lUNIV Klist])
unfolding bdd_from_sc_def unfolding Klist_def [symmetric]
unfolding lUNIV_def [symmetric]
unfolding boolfunc_from_sc_list [OF set_lUNIV sc_Klist]
unfolding Klist_set
unfolding boolfunc_from_sc_alt by simp
qed
code_identifier
code_module Product_Type ⇀ (SML) IBDD
and (OCaml) IBDD and (Haskell) IBDD
| code_module Typerep ⇀ (SML) IBDD
and (OCaml) IBDD and (Haskell) IBDD
| code_module String ⇀ (SML) IBDD
and (OCaml) IBDD and (Haskell) IBDD
export_code open bdd_from_sc ex_2_3 ex_false ex_true another_ex one_another_ex
in Haskell module_name IBDD file BDD
export_code bdd_from_sc ex_2_3
in SML module_name IBDD file SMLBDD
end