# Theory Multiset_Ordering_in_NP

section ‹Deciding the Generalized Multiset Ordering is in NP›

text ‹We first define a SAT-encoding for the comparison of two multisets w.r.t. two relations S and NS,
then show soundness of the encoding and finally show that the size of the encoding is quadratic in the input.›

theory
Multiset_Ordering_in_NP
imports
Multiset_Ordering_More
Propositional_Formula
begin

subsection ‹Locale for Generic Encoding›

text ‹We first define a generic encoding which may be instantiated for both propositional formulas
and for CNFs. Here, we require some encoding primitives with the semantics specified in the
enc-sound assumptions.›

locale encoder =
fixes eval :: "('a ⇒ bool) ⇒ 'f ⇒ bool"
and enc_False :: "'f"
and enc_True :: 'f
and enc_pos :: "'a ⇒ 'f"
and enc_neg :: "'a ⇒ 'f"
and enc_different :: "'a ⇒ 'a ⇒ 'f"
and enc_equiv_and_not :: "'a ⇒ 'a ⇒ 'a ⇒ 'f"
and enc_equiv_ite :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'f"
and enc_ite :: "'a ⇒ 'a ⇒ 'a ⇒ 'f"
and enc_impl :: "'a ⇒ 'f ⇒ 'f"
and enc_var_impl :: "'a ⇒ 'a ⇒ 'f"
and enc_not_and :: "'a ⇒ 'a ⇒ 'f"
and enc_not_all :: "'a list ⇒ 'f"
and enc_conj :: "'f list ⇒ 'f"
assumes enc_sound[simp]:
"eval α (enc_False) = False"
"eval α (enc_True) = True"
"eval α (enc_pos x) = α x"
"eval α (enc_neg x) = (¬ α x)"
"eval α (enc_different x y) = (α x ≠ α y)"
"eval α (enc_equiv_and_not x y z) = (α x ⟷ α y ∧ ¬ α z)"
"eval α (enc_equiv_ite x y z u) = (α x ⟷ (if α y then α z else α u))"
"eval α (enc_ite x y z) = (if α x then α y else α z)"
"eval α (enc_impl x f) = (α x ⟶ eval α f)"
"eval α (enc_var_impl x y) = (α x ⟶ α y)"
"eval α (enc_not_and x y) = (¬ (α x ∧ α y))"
"eval α (enc_not_all xs) = (¬ (Ball (set xs) α))"
"eval α (enc_conj fs) = (Ball (set fs) (eval α))"
begin

subsection ‹Definition of the Encoding›

text ‹We need to encode formulas of the shape that exactly one variable
is evaluated to true. Here, we use the linear encoding of
\<^cite>‹‹Section~5.3› in "DBLP:journals/jsat/EenS06"›
that requires some auxiliary variables. More precisely, for each
propositional variable that we want to count we require two auxiliary variables.›

fun encode_sum_0_1_main :: "('a × 'a × 'a) list ⇒ 'f list × 'a × 'a" where
"encode_sum_0_1_main [(x, zero, one)] = ([enc_different zero x], zero, x)"
| "encode_sum_0_1_main ((x, zero, one) # rest) = (case encode_sum_0_1_main rest of
(conds, fzero, fone) ⇒ let
czero = enc_equiv_and_not zero fzero x;
cone  = enc_equiv_ite one x fzero fone
in (czero # cone # conds, zero, one))"

definition encode_exactly_one :: "('a × 'a × 'a) list ⇒ 'f × 'f list" where
"encode_exactly_one vars = (case vars of [] ⇒ (enc_False, [])
| [(x,_,_)] ⇒ (enc_pos x, [])
| ((x,_,_) # vars) ⇒ (case encode_sum_0_1_main vars of (conds, zero, one)
⇒ (enc_ite x zero one, conds)))"

fun encodeGammaCond :: "'a ⇒ 'a ⇒ bool ⇒ bool ⇒ 'f" where
"encodeGammaCond gam eps True True = enc_True"
| "encodeGammaCond gam eps False False = enc_neg gam"
| "encodeGammaCond gam eps False True = enc_var_impl gam eps"
| "encodeGammaCond gam eps True False = enc_not_and gam eps"
end

text ‹The encoding of the multiset comparisons is based on \<^cite>‹‹Sections~3.6 and 3.7› in "RPO_NP"›.
It uses propositional variables $\gamma_{ij}$ and $\epsilon_i$.
We further add auxiliary variables that are required for the exactly-one-encoding.›

datatype PropVar = Gamma nat nat | Epsilon nat
| AuxZeroJI nat nat | AuxOneJI nat nat
| AuxZeroIJ nat nat | AuxOneIJ nat nat

text ‹At this point we define a new locale as an instance of @{locale encoder} where the
type of propositional variables is fixed to @{typ PropVar}.›

locale ms_encoder = encoder eval for eval :: "(PropVar ⇒ bool) ⇒ 'f ⇒ bool"
begin

definition formula14 :: "nat ⇒ nat ⇒ 'f list" where
"formula14 n m = (let
inner_left = λ j. case encode_exactly_one (map (λ i. (Gamma i j, AuxZeroJI i j, AuxOneJI i j)) [0 ..< n])
of (one, cands) ⇒ one # cands;
left = List.maps inner_left [0 ..< m];
inner_right = λ i. encode_exactly_one (map (λ j. (Gamma i j, AuxZeroIJ i j, AuxOneIJ i j)) [0 ..< m]);
right = List.maps (λ i. case inner_right i of (one, cands) ⇒ enc_impl (Epsilon i) one # cands) [0 ..< n]
in left @ right)"

definition formula15 :: "(nat ⇒ nat ⇒ bool) ⇒ (nat ⇒ nat ⇒ bool) ⇒ nat ⇒ nat ⇒ 'f list" where
"formula15 cs cns n m = (let
conjs = List.maps (λ i. List.maps (λ j. let s = cs i j; ns = cns i j in
if s ∧ ns then [] else [encodeGammaCond (Gamma i j) (Epsilon i) s ns]) [0 ..< m]) [0 ..< n]
in conjs @ formula14 n m)"

definition formula16 :: "(nat ⇒ nat ⇒ bool) ⇒ (nat ⇒ nat ⇒ bool) ⇒ nat ⇒ nat ⇒ 'f list" where
"formula16 cs cns n m = (enc_not_all (map Epsilon [0 ..< n]) # formula15 cs cns n m)"

text ‹The main encoding function. It takes a function as input
that returns for each pair of elements a pair of Booleans, and
these indicate whether the elements are strictly or weakly decreasing. Moreover, two input lists are given.
Finally two formulas are returned, where the first is satisfiable iff the two lists are strictly decreasing w.r.t.
the multiset ordering, and second is satisfiable iff there is a weak decrease w.r.t. the multiset ordering.›

definition encode_mul_ext :: "('a ⇒ 'a ⇒ bool × bool) ⇒ 'a list ⇒ 'a list ⇒ 'f × 'f" where
"encode_mul_ext s_ns xs ys = (let
n = length xs;
m = length ys;
cs = (λ i j. fst (s_ns (xs ! i) (ys ! j)));
cns = (λ i j. snd (s_ns (xs ! i) (ys ! j)));
f15 = formula15 cs cns n m;
f16 = enc_not_all (map Epsilon [0 ..< n]) # f15
in (enc_conj f16, enc_conj f15))"
end

subsection ‹Soundness of the Encoding›

context encoder
begin

abbreviation eval_all :: "('a ⇒ bool) ⇒ 'f list ⇒ bool" where
"eval_all α fs ≡ (Ball (set fs) (eval α))"

lemma encode_sum_0_1_main: assumes "encode_sum_0_1_main vars = (conds, zero, one)"
and "⋀ i x ze on re. prop ⟹ i < length vars ⟹ drop i vars = ((x,ze,on) # re) ⟹
(α ze ⟷ ¬ (∃ y ∈ insert x (fst  set re). α y))
∧ (α on ⟷ (∃! y ∈ insert x (fst  set re). α y))"
and "¬ prop ⟹ eval_all α conds"
and "distinct (map fst vars)"
and "vars ≠ []"
shows "eval_all α conds
∧ (α zero ⟷ ¬ (∃ x ∈ fst  set vars. α x))
∧ (α one ⟷ (∃! x ∈ fst  set vars. α x))"
using assms
proof (induct vars arbitrary: conds zero one rule: encode_sum_0_1_main.induct)
case (1 x zero' one' conds zero one)
from 1(1,3-) 1(2)[of 0] show ?case by (cases "prop", auto)
next
case Cons: (2 x zero one r rr conds' zero' one')
let ?triple = "(x,zero,one)"
let ?rest = "r # rr"
obtain conds fzero fone where res: "encode_sum_0_1_main ?rest = (conds, fzero, fone)"
by (cases "encode_sum_0_1_main ?rest", auto)
from Cons(2)[unfolded encode_sum_0_1_main.simps res split Let_def]
have zero: "zero' = zero" and one: "one' = one" and
conds': "conds' = enc_equiv_and_not zero fzero x # enc_equiv_ite one x fzero fone # conds"
by auto
from Cons(5) have x: "x ∉ fst  set ?rest"
and dist: "distinct (map fst ?rest)" by auto
have "eval_all α conds ∧ α fzero = (¬ (∃a∈fst  set ?rest. α a)) ∧ α fone = (∃!x. x ∈ fst  set ?rest ∧ α x)"
apply (rule Cons(1)[OF res _ _ dist])
subgoal for i x ze on re using Cons(3)[of "Suc i" x ze on re] by auto
subgoal using Cons(4) unfolding conds' by auto
subgoal by auto
done
hence IH: "eval_all α conds" "α fzero = (¬ (∃a∈fst  set ?rest. α a))"
"α fone = (∃!x. x ∈ fst  set ?rest ∧ α x)" by auto
show ?case
proof (cases "prop")
case True
from Cons(3)[of 0 x zero one ?rest, OF True]
have id: "α zero = (∀y∈ insert x (fst  set ?rest). ¬ α y)"
"α one = (∃!y. y ∈ insert x (fst  set ?rest) ∧ α y)"  by auto
show ?thesis unfolding zero one conds' eval.simps using x IH(1)
apply (simp add: IH id)
by blast
next
case False
from Cons(4)[OF False, unfolded conds']
have id: "α zero = (¬ α x ∧ α fzero)"
"α one = (α x ∧ α fzero ∨ ¬ α x ∧ α fone)" by auto
show ?thesis unfolding zero one conds' eval.simps using x IH(1)
apply (simp add: IH id)
by blast
qed
qed auto

lemma encode_exactly_one_complete: assumes "encode_exactly_one vars = (one, conds)"
and "⋀ i x ze on. i < length vars ⟹
vars ! i = (x,ze,on) ⟹
(α ze ⟷ ¬ (∃ y ∈ fst  set (drop i vars). α y))
∧ (α on ⟷ (∃! y ∈ fst  set (drop i vars). α y))"
and "distinct (map fst vars)"
shows "eval_all α conds ∧ (eval α one ⟷ (∃! x ∈ fst  set vars. α x))"
proof -
consider (empty) "vars = []" | (single) x ze on where "vars = [(x,ze,on)]"
| (other) x ze on v vs where "vars = (x,ze,on) # v # vs"
by (cases vars; cases "tl vars"; auto)
thus ?thesis
proof cases
case (other x ze' on' v vs)
obtain on zero where res: "encode_sum_0_1_main (v # vs) = (conds, zero, on)"
and one: "one = enc_ite x zero on"
using assms(1) unfolding encode_exactly_one_def other split list.simps
by (cases "encode_sum_0_1_main (v # vs)", auto)
let ?vars = "v # vs"
define vars' where "vars' = ?vars"
from assms(3) other have dist: "distinct (map fst ?vars)" by auto
have main: "eval_all α conds  ∧ (α zero ⟷ ¬ (∃ x ∈ fst  set ?vars. α x))
∧ (α on ⟷ (∃! x ∈ fst  set ?vars. α x))"
apply (rule encode_sum_0_1_main[OF res _ _ dist, of True])
subgoal for i x ze on re using assms(2)[of "Suc i" x ze on] unfolding other
by (simp add: nth_via_drop)
by auto
hence conds: "eval_all α conds" and zero: "α zero ⟷ ¬ (∃ x ∈ fst  set ?vars. α x)"
and on: "α on ⟷ (∃! x ∈ fst  set ?vars. α x)" by auto
have one: "eval α one ⟷ (∃! x ∈ fst  set vars. α x)"
unfolding one
apply (simp)
using assms(3)
unfolding zero on other vars'_def[symmetric] by simp blast
show ?thesis using one conds by auto
next
case empty
with assms have "one = enc_False" by (auto simp: encode_exactly_one_def)
hence "eval α one = False" by auto
with assms empty show ?thesis by (auto simp: encode_exactly_one_def)
qed (insert assms, auto simp: encode_exactly_one_def)
qed

lemma encode_exactly_one_sound: assumes "encode_exactly_one vars = (one, conds)"
and "distinct (map fst vars)"
and "eval α one"
and "eval_all α conds"
shows "∃! x ∈ fst  set vars. α x"
proof -
consider (empty) "vars = []" | (single) x ze on where "vars = [(x,ze,on)]"
| (other) x ze on v vs where "vars = (x,ze,on) # v # vs"
by (cases vars; cases "tl vars"; auto)
thus ?thesis
proof cases
case (other x ze' on' v vs)
obtain on zero where res: "encode_sum_0_1_main (v # vs) = (conds, zero, on)"
and one: "one = enc_ite x zero on"
using assms(1) unfolding encode_exactly_one_def other split list.simps
by (cases "encode_sum_0_1_main (v # vs)", auto)
let ?vars = "v # vs"
define vars' where "vars' = ?vars"
from assms(2) other have dist: "distinct (map fst ?vars)" by auto
have main: "eval_all α conds  ∧ (α zero ⟷ ¬ (∃ x ∈ fst  set ?vars. α x))
∧ (α on ⟷ (∃! x ∈ fst  set ?vars. α x))"
by (rule encode_sum_0_1_main[OF res _ assms(4) dist, of False], auto)
hence conds: "eval_all α conds" and zero: "α zero ⟷ ¬ (∃ x ∈ fst  set ?vars. α x)"
and on: "α on ⟷ (∃! x ∈ fst  set ?vars. α x)" by auto
have one: "eval α one ⟷ (∃! x ∈ fst  set vars. α x)"
unfolding one
apply (simp)
using assms(2)
unfolding zero on other vars'_def[symmetric] by simp blast
with assms show ?thesis by auto
next
case empty
with assms have "one = enc_False" by (auto simp: encode_exactly_one_def)
hence "eval α one = False" by auto
with assms empty show ?thesis by (auto simp: encode_exactly_one_def)
qed (insert assms, auto simp: encode_exactly_one_def)
qed

lemma encodeGammaCond[simp]: "eval α (encodeGammaCond gam eps s ns) =
(α gam ⟶ (α eps ⟶ ns) ∧ (¬ α eps ⟶ s))"
by (cases ns; cases s, auto)

lemma eval_all_append[simp]: "eval_all α (fs @ gs) = (eval_all α fs ∧ eval_all α gs)"
by auto

lemma eval_all_Cons[simp]: "eval_all α (f # gs) = (eval α f ∧ eval_all α gs)"
by auto

lemma eval_all_concat[simp]: "eval_all α (concat fs) = (∀ f ∈ set fs. eval_all α f)"
by auto

lemma eval_all_maps[simp]: "eval_all α (List.maps f fs) = (∀ g ∈ set fs. eval_all α (f g))"
unfolding List.maps_def eval_all_concat by auto
end

context ms_encoder
begin

context
fixes s t :: "nat ⇒ 'a"
and n m :: nat
and S NS :: "'a rel"
and cs cns
assumes cs: "⋀ i j. cs i j = ((s i, t j) ∈ S)"
and cns:  "⋀ i j. cns i j = ((s i, t j) ∈ NS)"
begin

lemma encoding_sound:
assumes eval15: "eval_all v (formula15 cs cns n m)"
shows "(mset (map s [0 ..< n]), mset (map t [0 ..< m])) ∈ ns_mul_ext NS S"
"eval_all v (formula16 cs cns n m) ⟹ (mset (map s [0 ..< n]), mset (map t [0 ..< m])) ∈ s_mul_ext NS S"
proof -
from eval15[unfolded formula15_def]
have eval14: "eval_all v (formula14 n m)" by auto
define property where "property i = v (Epsilon i)" for i
define j_of_i :: "nat ⇒ nat"
where "j_of_i i = (THE j. j < m ∧ v (Gamma i j))" for i
define i_of_j :: "nat ⇒ nat"
where "i_of_j j = (THE i. i < n ∧ v (Gamma i j))" for j
define xs1 where "xs1 = filter (λ i. property i) [0 ..< n]"
define xs2 where "xs2 = filter (λ i. ¬ property i) [0 ..< n]"
define ys1 where "ys1 = map j_of_i xs1"
define ys2 where "ys2 = filter (λ j. j ∉ set ys1) [0 ..< m]"
let ?xs1 = "map s xs1"
let ?xs2 = "map s xs2"
let ?ys1 = "map t ys1"
let ?ys2 = "map t ys2"
{
fix i
assume *: "i < n" "v (Epsilon i)"
let ?vars = "map (λj. (Gamma i j, AuxZeroIJ i j, AuxOneIJ i j)) [0..<m]"
obtain one conds where enc: "encode_exactly_one ?vars = (one,conds)" by force
have dist: "distinct (map fst ?vars)" unfolding map_map o_def fst_conv
unfolding distinct_map by (auto simp: inj_on_def)
have "eval_all v (enc_impl (Epsilon i) one # conds)"
using eval14[unfolded formula14_def Let_def eval_all_append, unfolded eval_all_maps, THEN conjunct2] *(1) enc by force
with * have "eval v one" "eval_all v conds" by auto
from encode_exactly_one_sound[OF enc dist this]
have 1: "∃!x. x ∈ set (map (λj. Gamma i j) [0..<m]) ∧ v x"
by (simp add: image_comp)
have 2: "(∃!x. x ∈ set (map (λj. Gamma i j) [0..<m]) ∧ v x) =
(∃! j. j < m ∧ v (Gamma i j))" by fastforce
have 3: "∃! j. j < m ∧ v (Gamma i j)" using 1 2 by auto
have "j_of_i i < m ∧ v (Gamma i (j_of_i i))"
using 3 unfolding j_of_i_def
by (metis (no_types, lifting) the_equality)
note this 3
} note j_of_i = this
{
fix j
assume *: "j < m"
let ?vars = "map (λi. (Gamma i j, AuxZeroJI i j, AuxOneJI i j)) [0..<n]"
have dist: "distinct (map fst ?vars)" unfolding map_map o_def fst_conv
unfolding distinct_map by (auto simp: inj_on_def)
obtain one conds where enc: "encode_exactly_one ?vars = (one,conds)" by force
have "eval_all v (one # conds)"
using eval14[unfolded formula14_def Let_def eval_all_append, unfolded eval_all_maps, THEN conjunct1] *(1) enc by force
hence "eval v one" "eval_all v conds" by auto
from encode_exactly_one_sound[OF enc dist this]
have 1: "∃!x. x ∈ set (map (λi. Gamma i j) [0..<n]) ∧ v x"
by (simp add: image_comp)
have 2: "(∃!x. x ∈ set (map (λi. Gamma i j) [0..<n]) ∧ v x) =
(∃! i. i < n ∧ v (Gamma i j))" by fastforce
have 3: "∃! i. i < n ∧ v (Gamma i j)" using 1 2 by auto
have "i_of_j j < n ∧ v (Gamma (i_of_j j) j)"
using 3 unfolding i_of_j_def
by (metis (no_types, lifting) the_equality)
note this 3
} note i_of_j = this

have len: "length ?xs1 = length ?ys1"
unfolding ys1_def by simp
note goals = len
{
fix k
define i where "i = xs1 ! k"
assume "k < length ?ys1"
hence k: "k < length xs1" using len by auto
hence "i ∈ set xs1" using i_def by simp
hence ir: "i < n" "v (Epsilon i)"
unfolding xs1_def property_def by auto
from j_of_i this
have **: "j_of_i i < m ∧ v (Gamma i (j_of_i i))" by auto
have ys1k: "?ys1 ! k = t (j_of_i i)" unfolding i_def ys1_def using k by auto
have xs1k: "?xs1 ! k = s i" unfolding i_def using k by auto
from eval15 have "∀i∈{0..<n}.
∀j∈{0..<m}. v (Gamma i j) ⟶ (v (Epsilon i) ⟶ cns i j)"
unfolding formula15_def Let_def eval_all_append eval_all_maps
by (auto split: if_splits)
hence "cns i (j_of_i i)" using ** ir by auto
then have "(?xs1 ! k, ?ys1 ! k) ∈ NS"
unfolding xs1k ys1k using cns[of i "(j_of_i i)"] by (auto split: if_splits)
} note step2 = this
note goals = goals this
have xexp : "mset (map s [0..<n]) = mset ?xs1 + mset ?xs2"
unfolding xs1_def xs2_def
using mset_map_filter
by metis
note goals = goals this
{
fix i
assume "i < n" "property i"
hence "i_of_j (j_of_i i) = i"
using i_of_j j_of_i[of i] unfolding property_def by auto
} note i_of_j_of_i = this
have "mset ys1 = mset (filter (λj. j ∈ set (map j_of_i xs1)) [0..<m])"
(is "mset ?l = mset ?r")
proof -
have dl: "distinct ?l" unfolding ys1_def xs1_def distinct_map
proof
show "distinct (filter property [0..<n])" by auto
show "inj_on j_of_i (set (filter property [0..<n]))"
by (intro inj_on_inverseI[of _ i_of_j], insert i_of_j_of_i, auto)
qed
have dr: "distinct ?r" by simp
have id: "set ?l = set ?r" unfolding ys1_def xs1_def using j_of_i i_of_j
by (auto simp: property_def)
from dl dr id show ?thesis using set_eq_iff_mset_eq_distinct by blast
qed
hence ys1: "mset (map t ys1) = mset (map t ?r)" by simp
have yeyp: "mset (map t [0..<m]) = mset ?ys1 + mset ?ys2"
unfolding ys1 ys2_def unfolding ys1_def mset_map_filter ..
note goals = goals this
{
fix y
assume "y ∈ set ?ys2"
then obtain j where j: "j ∈ set ys2" and y: "y = t j" by auto
from j[unfolded ys2_def ys1_def]
have j: "j < m" and nmem: "j ∉ set (map j_of_i xs1)" by auto
let ?i = "i_of_j j"
from i_of_j[OF j] have i: "?i < n" and gamm: "v (Gamma ?i j)" by auto
from eval15[unfolded formula15_def Let_def eval_all_append eval_all_maps] i j gamm
have "¬ v (Epsilon ?i) ⟹ cs ?i j" by (force split: if_splits)
moreover have not: "¬ v (Epsilon ?i)" using nmem i j i_of_j j_of_i
unfolding xs1_def property_def
by (metis atLeast0LessThan filter_set imageI lessThan_iff list.set_map member_filter set_upt)
ultimately have "cs ?i j" by simp
hence sy: "(s ?i,y) ∈ S" unfolding y using cs[of ?i j] by (auto split: if_splits)
from not i have "?i ∈ set xs2" unfolding xs2_def property_def by auto
hence "s ?i ∈ set ?xs2" by simp
hence "∃ x ∈ set ?xs2. (x,y) ∈ S" using sy by auto
}
note goals = goals this

show "(mset (map s [0 ..< n]), mset (map t [0 ..< m])) ∈ ns_mul_ext NS S"
by (rule ns_mul_ext_intro[OF goals(3,4,1,2,5)])

assume "eval_all v (formula16 cs cns n m)"
from this[unfolded formula16_def Let_def]
obtain i where i: "i < n" and v: "¬ v (Epsilon i)" by auto
hence "i ∈ set xs2" unfolding xs2_def property_def by auto
hence "?xs2 ≠ []" by auto
note goals = goals this
show "(mset (map s [0 ..< n]), mset (map t [0 ..< m])) ∈ s_mul_ext NS S"
by (rule s_mul_ext_intro[OF goals(3,4,1,2,6,5)])
qed

lemma bex1_cong: "X = Y ⟹ (⋀ x. x ∈ Y ⟹ P x = Q x) ⟹ (∃!x. x ∈ X ∧ P x) = (∃!x. x ∈ Y ∧ Q x)"
by auto

lemma encoding_complete:
assumes "(mset (map s [0 ..< n]), mset (map t [0 ..< m])) ∈ ns_mul_ext NS S"
shows "(∃ v. eval_all v (formula15 cs cns n m) ∧
((mset (map s [0 ..< n]), mset (map t [0 ..< m])) ∈ s_mul_ext NS S ⟶ eval_all v (formula16 cs cns n m)))"
proof -
let ?S = "(mset (map s [0 ..< n]), mset (map t [0 ..< m])) ∈ s_mul_ext NS S"
from ns_mul_ext_elim[OF assms] s_mul_ext_elim[of "mset (map s [0..<n])" "mset (map t [0..<m])" NS S]
obtain Xs1 Xs2 Ys1 Ys2 where
eq1: "mset (map s [0..<n]) = mset Xs1 + mset Xs2" and
eq2: "mset (map t [0..<m]) = mset Ys1 + mset Ys2" and
len: "length Xs1 = length Ys1" and
ne: "?S ⟹ Xs2 ≠ []" and
NS: "⋀ i. i<length Ys1 ⟹ (Xs1 ! i, Ys1 ! i) ∈ NS" and
S: "⋀  y. y∈set Ys2 ⟹ ∃x∈set Xs2. (x, y) ∈ S"
by blast
from mset_map_split[OF eq1] obtain xs1 xs2 where
xs: "mset [0..<n] = mset xs1 + mset xs2"
and xs1: "Xs1 = map s xs1"
and xs2: "Xs2 = map s xs2" by auto
from mset_map_split[OF eq2] obtain ys1 ys2 where
ys: "mset [0..<m] = mset ys1 + mset ys2"
and ys1: "Ys1 = map t ys1"
and ys2: "Ys2 = map t ys2" by auto
from xs have dist_xs: "distinct (xs1 @ xs2)"
by (metis distinct_upt mset_append mset_eq_imp_distinct_iff)
from xs have un_xs: "set xs1 ∪ set xs2 = {..<n}"
by (metis atLeast_upt set_mset_mset set_mset_union)
from ys have dist_ys: "distinct (ys1 @ ys2)"
by (metis distinct_upt mset_append mset_eq_imp_distinct_iff)
from ys have un_ys: "set ys1 ∪ set ys2 = {..<m}"
by (metis atLeast_upt set_mset_mset set_mset_union)
define pos_of where "pos_of xs i = (THE p. p < length xs ∧ xs ! p = i)" for i and xs :: "nat list"
from dist_xs dist_ys have "distinct xs1" "distinct ys1" by auto
{
fix xs :: "nat list" and x
assume dist: "distinct xs" and x: "x ∈ set xs"
hence one: "∃! i. i < length xs ∧ xs ! i = x" by (rule distinct_Ex1)
from theI'[OF this, folded pos_of_def]
have "pos_of xs x < length xs" "xs ! pos_of xs x = x" by auto
note this one
} note pos = this
note p_xs = pos[OF ‹distinct xs1›]
note p_ys = pos[OF ‹distinct ys1›]
define i_of_j2 where "i_of_j2 j = (SOME i. i ∈ set xs2 ∧ cs i j)" for j
define v' :: "PropVar ⇒ bool" where
"v' x = (case x of
Epsilon i ⇒ i ∈ set xs1
| Gamma i j ⇒ (i ∈ set xs1 ∧ j ∈ set ys1 ∧ i = xs1 ! pos_of ys1 j
∨ i ∈ set xs2 ∧ j ∈ set ys2 ∧ i = i_of_j2 j))" for x
define v :: "PropVar ⇒ bool" where
"v x = (case x of
AuxZeroJI i j ⇒ (¬ Bex (set (drop i (map (λi. (Gamma i j)) [0..<n]))) v')
| AuxOneJI i j ⇒ (∃!y. y ∈ set (drop i (map (λi. (Gamma i j)) [0..<n])) ∧ v' y)
| AuxZeroIJ i j ⇒ (¬ Bex (set (drop j (map (λj. (Gamma i j)) [0..<m]))) v')
| AuxOneIJ i j ⇒ (∃!y. y ∈ set (drop j (map (λj. (Gamma i j)) [0..<m])) ∧ v' y)
| _ ⇒ v' x)" for x
note v_defs = v_def v'_def
{
fix j
assume j2: "j ∈ set ys2"
from j2 have "t j ∈ set Ys2" unfolding ys2 by auto
from S[OF this, unfolded xs2] have "∃ i. i ∈ set xs2 ∧ cs i j"
by (auto simp: cs)
from someI_ex[OF this, folded i_of_j2_def]
have *: "i_of_j2 j ∈ set xs2" "cs (i_of_j2 j) j" by auto
hence "v (Gamma (i_of_j2 j) j)" unfolding v_defs using j2 by auto
note * this
} note j_ys2 = this
{
fix j
assume j1: "j ∈ set ys1"
let ?pj = "pos_of ys1 j"
from p_ys[OF j1] have pj: "?pj < length Ys1" and yj: "ys1 ! ?pj = j"
unfolding ys1 by auto
have pj': "?pj < length Xs1" using len pj by auto
from NS[OF pj] have "(Xs1 ! ?pj, Ys1 ! ?pj) ∈ NS" .
also have "Ys1 ! ?pj = t j" using pj unfolding ys1 using yj by auto
also have "Xs1 ! ?pj = s (xs1 ! ?pj)" using pj' unfolding xs1 by auto
finally have cns: "cns (xs1 ! ?pj) j" unfolding cns .
have mem: "xs1 ! ?pj ∈ set xs1" using pj' unfolding xs1 by auto
have v: "v (Gamma (xs1 ! ?pj) j)"
unfolding v_defs using j1 mem by auto
note mem cns v
} note j_ys1 = this
have 14: "eval_all v (formula14 n m)"
unfolding formula14_def Let_def eval_all_append eval_all_maps
proof (intro conjI ballI, goal_cases)
case (1 j f)
then obtain one cands where j: "j < m" and f: "f ∈ set (one # cands)"
and enc: "encode_exactly_one (map (λi. (Gamma i j, AuxZeroJI i j, AuxOneJI i j)) [0..<n]) = (one, cands)" (is "?e = _")
by (cases ?e, auto)
have "eval_all v cands ∧
eval v one = (∃!x. x ∈ fst  set (map (λi. (Gamma i j, AuxZeroJI i j, AuxOneJI i j)) [0..<n]) ∧ v x)"
apply (rule encode_exactly_one_complete[OF enc])
subgoal for i y ze on
proof (goal_cases)
case 1
hence ze: "ze = AuxZeroJI i j" and on: "on = AuxOneJI i j" by auto
have id: "fst  set (drop i (map (λi. (Gamma i j, AuxZeroJI i j, AuxOneJI i j)) [0..<n]))
= set (drop i (map (λi. (Gamma i j)) [0..<n]))"
unfolding set_map[symmetric] drop_map by simp
show ?thesis unfolding ze on id unfolding v_def drop_map
by (intro conjI, force, simp, intro bex1_cong refl, auto)
qed
subgoal by (auto simp: distinct_map intro: inj_onI)
done
also have "fst  set (map (λi. (Gamma i j, AuxZeroJI i j, AuxOneJI i j)) [0..<n])
= (λi. Gamma i j)  set [0..<n]" unfolding set_map image_comp o_def by auto
also have "(∃!x. x ∈ … ∧ v x) = True" unfolding eq_True
proof -
from j un_ys have "j ∈ set ys1 ∨ j ∈ set ys2" by auto
thus "∃!x. x ∈ (λi. Gamma i j)  set [0..<n] ∧ v x"
proof
assume j: "j ∈ set ys2"
from j_ys2[OF j] un_xs have "i_of_j2 j ∈ {0..<n}" by auto
from this j_ys2[OF j] dist_ys j
show ?thesis
by (intro ex1I[of _ "(Gamma (i_of_j2 j) j)"], force, auto simp: v_defs)
next
assume j: "j ∈ set ys1"
from j_ys1[OF j] un_xs have "xs1 ! pos_of ys1 j ∈ {0..<n}" by auto
from this j_ys1[OF j] dist_ys j
show ?thesis
by (intro ex1I[of _ "(Gamma (xs1 ! pos_of ys1 j) j)"], force, auto simp: v_defs)
qed
qed
finally show ?case using 1 f by auto
next
case (2 i f)
then obtain one cands where i: "i < n" and f: "f ∈ set (enc_impl (Epsilon i) one # cands)"
and enc: "encode_exactly_one (map (λj. (Gamma i j, AuxZeroIJ i j, AuxOneIJ i j)) [0..<m]) = (one, cands)" (is "?e = _")
by (cases ?e, auto)
have "eval_all v cands ∧
eval v one = (∃!x. x ∈ fst  set (map (λj. (Gamma i j, AuxZeroIJ i j, AuxOneIJ i j)) [0..<m]) ∧ v x)"
apply (rule encode_exactly_one_complete[OF enc])
subgoal for j y ze on
proof (goal_cases)
case 1
hence ze: "ze = AuxZeroIJ i j" and on: "on = AuxOneIJ i j" by auto
have id: "fst  set (drop j (map (λj. (Gamma i j, AuxZeroIJ i j, AuxOneIJ i j)) [0..<m]))
= set (drop j (map (λj. (Gamma i j)) [0..<m]))"
unfolding set_map[symmetric] drop_map by simp
show ?thesis unfolding ze on id unfolding v_def drop_map
by (intro conjI, force, simp, intro bex1_cong refl, auto)
qed
subgoal by (auto simp: distinct_map intro: inj_onI)
done
also have "fst  set (map (λj. (Gamma i j, AuxZeroIJ i j, AuxOneIJ i j)) [0..<m])
= (λj. Gamma i j)  set [0..<m]" unfolding set_map image_comp o_def by auto
finally have cands: "eval_all v cands"
and "eval v one = (∃!x. x ∈ Gamma i  set [0..<m] ∧ v x)" by auto
note this(2)
also have "v (Epsilon i) ⟹ … = True" unfolding eq_True
proof -
assume v: "v (Epsilon i)"
hence i_xs: "i ∈ set xs1" "i ∉ set xs2" unfolding v_defs using dist_xs by auto
from this[unfolded set_conv_nth] obtain p where p1: "p < length xs1"
and xpi: "xs1 ! p = i" by auto
define j where "j = ys1 ! p"
from p1 len have p2: "p < length ys1" unfolding xs1 ys1 by auto
hence j: "j ∈ set ys1" unfolding j_def by auto
from p_ys[OF j] p2 have pp: "pos_of ys1 j = p" by (auto simp: j_def)
from j un_ys have jm: "j < m" by auto
have v: "v (Gamma i j)" unfolding v_defs using j pp xpi i_xs by simp
{
fix k
assume vk: "v (Gamma i k)"
from vk[unfolded v_defs] i_xs
have k: "k ∈ set ys1" and ik: "i = xs1 ! pos_of ys1 k" by auto
from p_ys[OF k] ik xpi have id: "pos_of ys1 k = p"
by (metis ‹distinct xs1› len length_map nth_eq_iff_index_eq p1 xs1 ys1)
have "k = ys1 ! pos_of ys1 k" using p_ys[OF k] by auto
also have "… = j" unfolding id j_def ..
finally have "k = j" .
} note unique = this
show "∃!j. j ∈ Gamma i  set [0..<m] ∧ v j"
by (intro ex1I[of _ "Gamma i j"], use jm v in force, use unique in auto)
qed
finally show ?case using 2 f cands enc by auto
qed
{
fix i j
assume i: "i < n" and j: "j < m"
assume v: "v (Gamma i j)"
have strict: "¬ v (Epsilon i) ⟹ cs i j" using i j v j_ys2[of j] unfolding v_defs by auto
{
assume "v (Epsilon i)"
hence i': "i ∈ set xs1" "i ∉ set xs2" unfolding v_defs using dist_xs by auto
with v have j': "j ∈ set ys1" unfolding v_defs using dist_ys by auto
from v[unfolded v_defs] i' have ii: "i = xs1 ! pos_of ys1 j" by auto
from j_ys1[OF j', folded ii] have "cns i j" by auto
}
note strict this
} note compare = this
have 15: "eval_all v (formula15 cs cns n m)"
unfolding formula15_def Let_def eval_all_maps eval_all_append using 14 compare by auto
{
assume ?S
have 16: "∃x∈{0..<n}. ¬ v (Epsilon x)"
by (rule bexI[of _ "hd xs2"]; insert ne[OF ‹?S›] xs2 un_xs dist_xs; cases xs2, auto simp: v_defs)
have "eval_all v (formula16 cs cns n m)"
unfolding formula16_def Let_def using 15 16 by simp
}
with 15 show ?thesis by blast
qed

lemma formula15: "(mset (map s [0 ..< n]), mset (map t [0 ..< m])) ∈ ns_mul_ext NS S
⟷ (∃ v. eval_all v (formula15 cs cns n m))"
using encoding_sound encoding_complete by blast

lemma formula16: "(mset (map s [0 ..< n]), mset (map t [0 ..< m])) ∈ s_mul_ext NS S
⟷ (∃ v. eval_all v (formula16 cs cns n m))"
using encoding_sound encoding_complete s_ns_mul_ext[of _ _ NS S]
unfolding formula16_def Let_def eval_all_Cons by blast
end

lemma encode_mul_ext: assumes "encode_mul_ext f xs ys = (φ⇩S, φ⇩N⇩S)"
shows "mul_ext f xs ys = ((∃ v. eval v φ⇩S), (∃ v. eval v φ⇩N⇩S))"
proof -
have xs: "mset xs = mset (map (λ i. xs ! i) [0 ..< length xs])" by (simp add: map_nth)
have ys: "mset ys = mset (map (λ i. ys ! i) [0 ..< length ys])" by (simp add: map_nth)
from assms[unfolded encode_mul_ext_def Let_def, simplified]
have phis: "φ⇩N⇩S = enc_conj (formula15 (λi j. fst (f (xs ! i) (ys ! j))) (λi j. snd (f (xs ! i) (ys ! j))) (length xs) (length ys))"
"φ⇩S = enc_conj (formula16 (λi j. fst (f (xs ! i) (ys ! j))) (λi j. snd (f (xs ! i) (ys ! j))) (length xs) (length ys))"
by (auto simp: formula16_def)
show ?thesis unfolding mul_ext_def Let_def unfolding xs ys prod.inject phis enc_sound
by (intro conjI; rule formula15 formula16, auto)
qed
end

subsection ‹Encoding into Propositional Formulas›

global_interpretation pf_encoder: ms_encoder
"Disj []"
"Conj []"
"λ x. Prop x"
"λ x. Neg (Prop x)"
"λ x y. Equiv (Prop x) (Neg (Prop y))"
"λ x y z. Equiv (Prop x) (Conj [Prop y, Neg (Prop z)])"
"λ x y z u. Equiv (Prop x) (Disj [Conj [Prop y, Prop z], Conj [Neg (Prop y), Prop u]])"
"λ x y z. Disj [Conj [Prop x, Prop y], Conj [Neg (Prop x), Prop z]]"
"λ x f. Impl (Prop x) f"
"λ x y. Impl (Prop x) (Prop y)"
"λ x y. Neg (Conj [Prop x, Prop y])"
"λ xs. Neg (Conj (map Prop xs))"
Conj
eval
defines
pf_encode_sum_0_1_main = pf_encoder.encode_sum_0_1_main and
pf_encode_exactly_one = pf_encoder.encode_exactly_one and
pf_encodeGammaCond = pf_encoder.encodeGammaCond and
pf_formula14 = pf_encoder.formula14 and
pf_formula15 = pf_encoder.formula15 and
pf_formula16 = pf_encoder.formula16 and
pf_encode_mul_ext = pf_encoder.encode_mul_ext
by (unfold_locales, auto)

text ‹The soundness theorem of the propositional formula encoder›

thm pf_encoder.encode_mul_ext

subsection ‹Size of Propositional Formula Encoding is Quadratic›

lemma size_pf_encode_sum_0_1_main: assumes "pf_encode_sum_0_1_main vars = (conds, one, zero)"
and "vars ≠ []"
shows "sum_list (map size_pf conds) = 16 * length vars - 12"
using assms
proof (induct vars arbitrary: conds one zero rule: pf_encoder.encode_sum_0_1_main.induct)
case (1 x zero' one' conds zero one)
hence "conds = [Equiv (Prop zero) (Neg (Prop x))]" by auto
thus ?case by simp
next
case Cons: (2 x zero one r rr conds' zero' one')
let ?triple = "(x,zero,one)"
let ?rest = "r # rr"
obtain conds fzero fone where res: "pf_encode_sum_0_1_main ?rest = (conds, fzero, fone)"
by (cases "pf_encode_sum_0_1_main ?rest", auto)
from Cons(2)[unfolded pf_encoder.encode_sum_0_1_main.simps res split Let_def]
have conds': "conds' = Equiv (Prop zero) (Conj [Prop fzero, Neg (Prop x)]) #
Equiv (Prop one) (Disj [Conj [Prop x, Prop fzero], Conj [Neg (Prop x), Prop fone]]) # conds"
by auto
have "sum_list (map size_pf conds') = 16 + sum_list (map size_pf conds)"
unfolding conds' by simp
with Cons(1)[OF res]
show ?case by simp
qed auto

lemma size_pf_encode_exactly_one: assumes "pf_encode_exactly_one vars = (one, conds)"
shows "size_pf one + sum_list (map size_pf conds) = 1 + (16 * length vars - 21)"
proof (cases "vars = []")
case True
with assms have "size_pf one = 1" "conds = []"
by (auto simp add: pf_encoder.encode_exactly_one_def)
thus ?thesis unfolding True by simp
next
case False
then obtain x ze' on' vs where vars: "vars = (x,ze',on') # vs" by (cases vars; auto)
show ?thesis
proof (cases vs)
case Nil
have "size_pf one = 1" "conds = []" using assms unfolding vars Nil
by (auto simp add: pf_encoder.encode_exactly_one_def)
thus ?thesis unfolding vars Nil by simp
next
case (Cons v vs')
obtain on zero where res: "pf_encode_sum_0_1_main vs = (conds, zero, on)"
and one: "one = Disj [Conj [Prop x, Prop zero], Conj [Neg (Prop x), Prop on]]"
using assms(1) False Cons unfolding pf_encoder.encode_exactly_one_def vars
by (cases "pf_encode_sum_0_1_main vs", auto)
from size_pf_encode_sum_0_1_main[OF res]
have sum: "sum_list (map size_pf conds) = (16 * length vars - 28)" using Cons vars by auto
have one: "size_pf one = 8" unfolding one by simp
show ?thesis unfolding one sum vars Cons by simp
qed
qed

lemma sum_list_concat: "sum_list (concat xs) = sum_list (map sum_list xs)"
by (induct xs, auto)

lemma sum_list_triv_cong: assumes "length xs = n"
and "⋀ x. x ∈ set xs ⟹ f x = c"
shows "sum_list (map f xs) = n * c"
by (subst map_cong[OF refl, of _ _ "λ _ . c"], insert assms, auto simp: sum_list_triv)

lemma size_pf_formula14: "sum_list (map size_pf (pf_formula14 n m)) = m + 3 * n + m * (n * 16 - 21) + n * (m * 16 - 21)"
proof -
have "sum_list (map size_pf (pf_formula14 n m)) = m * (1 + (16 * n - 21)) + n * (3 + (16 * m - 21))"
unfolding pf_encoder.formula14_def Let_def sum_list_append map_append map_concat List.maps_def sum_list_concat map_map o_def
proof (intro arg_cong2[of _ _ _ _ "(+)"], goal_cases)
case 1
show ?case
apply (rule sum_list_triv_cong, force)
subgoal for j
by (cases "pf_encode_exactly_one (map (λi. (Gamma i j, AuxZeroJI i j, AuxOneJI i j)) [0..<n])",
auto simp: size_pf_encode_exactly_one)
done
next
case 2
show ?case
apply (rule sum_list_triv_cong, force)
subgoal for i
by (cases "pf_encode_exactly_one (map (λj. (Gamma i j, AuxZeroIJ i j, AuxOneIJ i j)) [0..<m])",
auto simp: size_pf_encode_exactly_one)
done
qed
also have "… = m + 3 * n + m * (n * 16 - 21) + n * (m * 16 - 21)"
by (simp add: algebra_simps)
finally show ?thesis .
qed

lemma size_pf_encodeGammaCond: "size_pf (pf_encodeGammaCond gam eps ns s) ≤ 4"
by (cases ns; cases s, auto)

lemma size_pf_formula15: "sum_list (map size_pf (pf_formula15 cs cns n m)) ≤ m + 3 * n + m * (n * 16 - 21) + n * (m * 16 - 21) + 4 * m * n"
proof -
have "sum_list (map size_pf (pf_formula15 cs cns n m)) ≤ sum_list (map size_pf (pf_formula14 n m)) + 4 * m * n"
unfolding pf_encoder.formula15_def Let_def
apply (simp add: size_list_conv_sum_list List.maps_def map_concat o_def length_concat sum_list_triv sum_list_concat algebra_simps)
apply (rule le_trans, rule sum_list_mono, rule sum_list_mono[of _ _ "λ _. 4"])
by (auto simp: size_pf_encodeGammaCond sum_list_triv)
also have "… = m + 3 * n + m * (n * 16 - 21) + n * (m * 16 - 21) + 4 * m * n"
unfolding size_pf_formula14 by auto
finally show ?thesis .
qed

lemma size_pf_formula16: "sum_list (map size_pf (pf_formula16 cs cns n m)) ≤ 2 + m + 4 * n + m * (n * 16 - 21) + n * (m * 16 - 21) + 4 * m * n"
proof -
have "sum_list (map size_pf (pf_formula16 cs cns n m)) = sum_list (map size_pf (pf_formula15 cs cns n m)) + (n + 2)"
unfolding pf_encoder.formula16_def Let_def by (simp add: o_def size_list_conv_sum_list sum_list_triv)
also have "… ≤ (m + 3 * n + m * (n * 16 - 21) + n * (m * 16 - 21) + 4 * m * n) + (n + 2)"
by (rule add_right_mono[OF size_pf_formula15])
also have "… = 2 + m + 4 * n + m * (n * 16 - 21) + n * (m * 16 - 21) + 4 * m * n" by simp
finally show ?thesis .
qed

lemma size_pf_encode_mul_ext: assumes "pf_encode_mul_ext f xs ys = (φ⇩S, φ⇩N⇩S)"
and n: "n = max (length xs) (length ys)"
and n0: "n ≠ 0"
shows "size_pf φ⇩S ≤ 36 * n⇧2"
"size_pf φ⇩N⇩S ≤ 36 * n⇧2"
proof -
from assms[unfolded pf_encoder.encode_mul_ext_def Let_def, simplified]
have phis: "φ⇩N⇩S = Conj (pf_formula15 (λi j. fst (f (xs ! i) (ys ! j))) (λi j. snd (f (xs ! i) (ys ! j))) (length xs) (length ys))"
"φ⇩S = Conj (pf_formula16 (λi j. fst (f (xs ! i) (ys ! j))) (λi j. snd (f (xs ! i) (ys ! j))) (length xs) (length ys))"
by (auto simp: pf_encoder.formula16_def)
have "size_pf φ⇩S ≤ 1 + (2 + n + 4 * n + n * (n * 16 - 21) + n * (n * 16 - 21) + 4 * n * n)"
unfolding phis unfolding n size_pf.simps
by (rule add_left_mono, rule le_trans[OF size_pf_formula16], intro add_mono mult_mono le_refl, auto)
also have "… ≤ 36 * n^2 - 24 * n" using n0 by (cases n; auto simp: power2_eq_square algebra_simps)
finally show "size_pf φ⇩S ≤ 36 * n^2" by simp

have "size_pf φ⇩N⇩S ≤ 1 + (n + 4 * n + n * (n * 16 - 21) + n * (n * 16 - 21) + 4 * n * n)"
unfolding phis unfolding n size_pf.simps
apply (rule le_trans[OF size_pf_formula15])
by (intro max.mono add_mono mult_mono le_refl, auto)
also have "… ≤ 36 * n^2 - 25 * n" using n0 by (cases n; auto simp: power2_eq_square algebra_simps)
finally show "size_pf φ⇩N⇩S ≤ 36 * n^2" by simp
qed

subsection ‹Encoding into Conjunctive Normal Form›

global_interpretation cnf_encoder: ms_encoder
"[[]]"
"[]"
"λ x. [[(x, True)]]"
"λ x. [[(x, False)]]"
"λ x y. [[(x, True), (y, True)], [(x, False), (y, False)]]"
"λ x y z. [[(x,False),(y,True)],[(x,False),(z,False)],[(x,True),(y,False),(z,True)]]"
"λ x y z u. [[(x,True),(y,True),(u,False)],[(x,True),(y,False),(z,False)],[(x,False),(y,False),(z,True)],[(x,False),(y,True),(u,True)]]"
"λ x y z. [[(x,True),(z,True)],[(x,False),(y,True)]]"
"λ x xs. map (λ c. (x,False) # c) xs"
"λ x y. [[(x,False), (y, True)]]"
"λ x y. [[(x,False), (y, False)]]"
"λ xs. [map (λ x. (x, False)) xs]"
concat
eval_cnf
defines
cnf_encode_sum_0_1_main = cnf_encoder.encode_sum_0_1_main and
cnf_encode_exactly_one = cnf_encoder.encode_exactly_one and
cnf_encodeGammaCond = cnf_encoder.encodeGammaCond and
cnf_formula14 = cnf_encoder.formula14 and
cnf_formula15 = cnf_encoder.formula15 and
cnf_formula16 = cnf_encoder.formula16 and
cnf_encode_mul_ext = cnf_encoder.encode_mul_ext
by unfold_locales (force simp: eval_cnf_alt_def)+

text ‹The soundness theorem of the CNF-encoder›

thm cnf_encoder.encode_mul_ext

subsection ‹Size of CNF-Encoding is Quadratic›

lemma size_cnf_encode_sum_0_1_main: assumes "cnf_encode_sum_0_1_main vars = (conds, one, zero)"
and "vars ≠ []"
shows "sum_list (map size_cnf conds) = 26 * length vars - 20"
using assms
proof (induct vars arbitrary: conds one zero rule: cnf_encoder.encode_sum_0_1_main.induct)
case (1 x zero' one' conds zero one)
hence "conds =  [[[(zero, True), (one, True)], [(zero, False), (one, False)]]]" by auto
hence "sum_list (map size_cnf conds) = 6" by (simp add: size_cnf_def)
thus ?case by simp
next
case Cons: (2 x zero one r rr conds' zero' one')
let ?triple = "(x,zero,one)"
let ?rest = "r # rr"
obtain conds fzero fone where res: "cnf_encode_sum_0_1_main ?rest = (conds, fzero, fone)"
by (cases "cnf_encode_sum_0_1_main ?rest", auto)
from Cons(2)[unfolded cnf_encoder.encode_sum_0_1_main.simps res split Let_def]
have conds': "conds' = [[(zero, False), (fzero, True)], [(zero, False), (x, False)], [(zero, True), (fzero, False), (x, True)]] #
[[(one, True), (x, True), (fone, False)], [(one, True), (x, False), (fzero, False)], [(one, False), (x, False), (fzero, True)],
[(one, False), (x, True), (fone, True)]] #
conds"
by auto
have "sum_list (map size_cnf conds') = 26 + sum_list (map size_cnf conds)"
unfolding conds' by (simp add: size_cnf_def)
with Cons(1)[OF res]
show ?case by simp
qed auto

lemma size_cnf_encode_exactly_one: assumes "cnf_encode_exactly_one vars = (one, conds)"
shows "size_cnf one + sum_list (map size_cnf conds) ≤ 2 + (26 * length vars - 42) ∧ length one ≤ 2"
proof (cases "vars = []")
case True
with assms have "size_cnf one = 1" "length one = 1" "conds = []"
by (auto simp add: cnf_encoder.encode_exactly_one_def size_cnf_def)
thus ?thesis unfolding True by simp
next
case False
then obtain x ze' on' vs where vars: "vars = (x,ze',on') # vs" by (cases vars; auto)
show ?thesis
proof (cases vs)
case Nil
have "size_cnf one = 2" "length one = 1" "conds = []" using assms unfolding vars Nil
by (auto simp add: cnf_encoder.encode_exactly_one_def size_cnf_def)
thus ?thesis unfolding vars Nil by simp
next
case (Cons v vs')
obtain on zero where res: "cnf_encode_sum_0_1_main vs = (conds, zero, on)"
and one: "one = [[(x, True), (on, True)], [(x, False), (zero, True)]]"
using assms(1) False Cons unfolding cnf_encoder.encode_exactly_one_def vars
by (cases "cnf_encode_sum_0_1_main vs", auto)
from size_cnf_encode_sum_0_1_main[OF res]
have sum: "sum_list (map size_cnf conds) = 26 * length vars - 46" using Cons vars by auto
have one: "size_cnf one = 6" "length one = 2" unfolding one by (auto simp add: size_cnf_def)
show ?thesis unfolding one sum vars Cons by simp
qed
qed

lemma sum_list_mono_const: assumes "⋀ x. x ∈ set xs ⟹ f x ≤ c"
and "n = length xs"
shows "sum_list (map f xs) ≤ n * c"
unfolding assms(2) using assms(1)
by (induct xs; force)

lemma size_cnf_formula14: "sum_list (map size_cnf (cnf_formula14 n m)) ≤ 2 * m + 4 * n + m * (26 * n - 42) + n * (26 * m - 42)"
proof -
have "sum_list (map size_cnf (cnf_formula14 n m)) ≤ m * (2 + (26 * n - 42)) + n * (4 + (26 * m - 42))"
unfolding cnf_encoder.formula14_def Let_def sum_list_append map_append map_concat List.maps_def sum_list_concat map_map o_def
proof ((intro add_mono; intro sum_list_mono_const), goal_cases)
case (1 j)
obtain one conds where cnf: "cnf_encode_exactly_one (map (λi. (Gamma i j, AuxZeroJI i j, AuxOneJI i j)) [0..<n]) = (one, conds)" (is "?e = _")
by (cases ?e, auto)
show ?case unfolding cnf split using size_cnf_encode_exactly_one[OF cnf] by auto
next
case (3 i)
obtain one conds where cnf: "cnf_encode_exactly_one (map (λj. (Gamma i j, AuxZeroIJ i j, AuxOneIJ i j)) [0..<m]) = (one, conds)" (is "?e = _")
by (cases ?e, auto)
have id: "size_cnf (map ((#) (Epsilon i, False)) one) = size_cnf one + length one" unfolding size_cnf_def by (induct one, auto simp: o_def)
show ?case unfolding cnf split using size_cnf_encode_exactly_one[OF cnf] by (simp add: id)
qed auto
also have "… = 2 * m + 4 * n + m * (26 * n - 42) + n * (26 * m - 42)"
by (simp add: algebra_simps)
finally show ?thesis .
qed

lemma size_cnf_encodeGammaCond: "size_cnf (cnf_encodeGammaCond gam eps ns s) ≤ 3"
by (cases ns; cases s, auto simp: size_cnf_def)

lemma size_cnf_formula15: "sum_list (map size_cnf (cnf_formula15 cs cns n m)) ≤ 2 * m + 4 * n + m * (26 * n - 42) + n * (26 * m - 42) + 3 * n * m"
proof -
have "sum_list (map size_cnf (cnf_formula15 cs cns n m)) ≤ sum_list (map size_cnf (cnf_formula14 n m)) + 3 * n * m"
unfolding cnf_encoder.formula15_def Let_def
apply (simp add: size_list_conv_sum_list List.maps_def map_concat o_def length_concat sum_list_triv sum_list_concat algebra_simps)
apply (rule le_trans, rule sum_list_mono_const[OF _ refl], rule sum_list_mono_const[OF _ refl, of _ _ 3])
by (auto simp: size_cnf_encodeGammaCond)
also have "… ≤ (2 * m + 4 * n + m * (26 * n - 42) + n * (26 * m - 42)) + 3 * n * m"
by (rule add_right_mono[OF size_cnf_formula14])
finally show ?thesis .
qed

lemma size_cnf_formula16: "sum_list (map size_cnf (cnf_formula16 cs cns n m)) ≤ 1 + 2 * m + 5 * n + m * (26 * n - 42) + n * (26 * m - 42) + 3 * n * m"
proof -
have "sum_list (map size_cnf (cnf_formula16 cs cns n m)) = sum_list (map size_cnf (cnf_formula15 cs cns n m)) + (n + 1)"
unfolding cnf_encoder.formula16_def Let_def by (simp add: o_def size_list_conv_sum_list sum_list_triv size_cnf_def)
also have "… ≤ (2 * m + 4 * n + m * (26 * n - 42) + n * (26 * m - 42) + 3 * n * m) + (n + 1)"
by (rule add_right_mono[OF size_cnf_formula15])
also have "… = 1 + 2 * m + 5 * n + m * (26 * n - 42) + n * (26 * m - 42) + 3 * n * m" by simp
finally show ?thesis .
qed

lemma size_cnf_concat: "size_cnf (concat xs) = sum_list (map size_cnf xs)" unfolding size_cnf_def
by (induct xs, auto)

lemma size_cnf_encode_mul_ext: assumes "cnf_encode_mul_ext f xs ys = (φ⇩S, φ⇩N⇩S)"
and n: "n = max (length xs) (length ys)"
and n0: "n ≠ 0"
shows "size_cnf φ⇩S ≤ 55 * n⇧2"
"size_cnf φ⇩N⇩S ≤ 55 * n⇧2"
proof -
let ?fns = "cnf_formula15 (λi j. fst (f (xs ! i) (ys ! j))) (λi j. snd (f (xs ! i) (ys ! j))) (length xs) (length ys)"
let ?fs = "cnf_formula16 (λi j. fst (f (xs ! i) (ys ! j))) (λi j. snd (f (xs ! i) (ys ! j))) (length xs) (length ys)"
from assms[unfolded cnf_encoder.encode_mul_ext_def Let_def, simplified]
have phis: "φ⇩N⇩S = concat ?fns" "φ⇩S = concat ?fs"
by (auto simp: cnf_encoder.formula16_def)
have le_s: "sum_list (map size_cnf ?fs) ≤ 1 + 2 * n + 5 * n + n * (26 * n - 42) + n * (26 * n - 42) + 3 * n * n"
by (rule le_trans[OF size_cnf_formula16], intro add_mono mult_mono le_refl, insert n, auto)
have le_ns: "sum_list (map size_cnf ?fns) ≤ 2 * n + 4 * n + n * (26 * n - 42) + n * (26 * n - 42) + 3 * n * n"
by (rule le_trans[OF size_cnf_formula15], intro add_mono mult_mono le_refl, insert n, auto)
{
fix φ
assume "φ ∈ {φ⇩N⇩S, φ⇩S}"
then obtain f where "f ∈ {?fs,?fns}" and phi: "