Theory Finite_IDL_Solver
theory Finite_IDL_Solver
imports
"HOL-Library.RBT_Mapping"
"HOL-Library.List_Lexorder"
"HOL-Library.Product_Lexorder"
Finite_IDL_Solver_Interface
Singleton_List
Polynomial_Factorization.Missing_List
begin
text ‹Delete all variables with (a sort that has) an upper bound of 0;
if some the clauses becomes empty, return a trivial unsat-problem.›
definition delete_trivial_sorts :: "('v,'s)fidl_input ⇒ ('v,'s)fidl_input option" where
"delete_trivial_sorts = (λ (bnds, diffs).
case partition ((=) 0 o snd) bnds of
([],_) ⇒ Some (bnds, diffs)
| (triv,non_triv) ⇒ let triv_sorts = set (map (snd o fst) triv);
newdiffs = map (filter (λ vw. snd (fst vw) ∉ triv_sorts)) diffs
in if [] ∈ set newdiffs then None else Some (non_triv, newdiffs))"
lemma delete_trivial_sorts: assumes inp: "fidl_input input"
and del: "delete_trivial_sorts input = ooutput"
shows "(ooutput = None ⟶ ¬ fidl_solvable input) ∧ (ooutput = Some output ⟶ fidl_input output ∧ fidl_solvable input = fidl_solvable output)"
proof -
obtain bnds diffs where input: "input = (bnds,diffs)" by force
obtain triv non_triv where part: "partition ((=) 0 o snd) bnds = (triv,non_triv)" (is "partition ?f _ = _") by force
define f where "f = ?f"
note del = del[unfolded delete_trivial_sorts_def input split part]
show ?thesis
proof (cases triv)
case Nil
thus ?thesis using inp del input by auto
next
case Cons
from part[unfolded partition_filter_conv, folded f_def]
have triv: "triv = filter f bnds" and non_triv: "non_triv = filter (Not ∘ f) bnds" by auto
define tsorts where "tsorts = set (map (snd ∘ fst) triv)"
define newdiffs where "newdiffs = map (filter (λvs. snd (fst vs) ∉ tsorts)) diffs"
let ?out = "(non_triv, newdiffs)"
note inp = inp[unfolded input fidl_input_def split]
from inp have dist: "distinct (map fst bnds)" by blast
have out_conds: "fidl_input ?out"
unfolding fidl_input_def split
proof (intro conjI allI impI)
show "distinct (map fst non_triv)" unfolding non_triv by (rule distinct_map_filter[OF dist])
{
fix v w
assume "(v, w) ∈ set (concat newdiffs)"
from this[unfolded newdiffs_def]
have vw: "(v, w) ∈ set (concat diffs)" and snd: "snd v ∉ tsorts" by auto
from vw inp show eq: "v ≠ w" by blast
from vw inp show eq: "snd v = snd w" by blast
from vw inp have "{v,w} ⊆ fst ` set bnds" by blast
with snd eq have "{v,w} ⊆ fst ` set non_triv" unfolding non_triv triv tsorts_def by force
thus "u ∈ {v, w} ⟹ u ∈ fst ` set non_triv" for u by auto
}
qed (insert inp, auto simp: non_triv)
let ?sat1 = "λ bnds α. (∀(v, b)∈set bnds. 0 ≤ α v ∧ α v ≤ b)"
let ?sat2 = "λ diffs α. (∀c∈set diffs. ∃(v, w)∈set c. α v ≠ α w)"
let ?sat = "λ bnds diffs α. ?sat1 bnds α ∧ ?sat2 diffs α"
have set_bnds: "set bnds = set triv ∪ set non_triv" using part by fastforce
have main: "fidl_solvable input = fidl_solvable ?out" unfolding input
proof
assume "fidl_solvable (non_triv, newdiffs)"
from this[unfolded fidl_solvable_def split] obtain α
where sat1: "?sat1 non_triv α" and sat2: "?sat2 newdiffs α" by blast
define β where "β v = (if snd v ∈ tsorts then 0 else α v)" for v
have αβ: "?sat2 newdiffs α = ?sat2 newdiffs β"
proof (intro ball_cong[OF refl] bex_cong[OF refl], clarsimp)
fix vsf v1 s1 v2 s2
assume *: "vsf ∈ set newdiffs" "((v1,s1),(v2,s2)) ∈ set vsf"
from *(1)[unfolded newdiffs_def]
obtain vs where vs: "vs ∈ set diffs" and vsf: "vsf = filter (λvs. snd (fst vs) ∉ tsorts) vs" by auto
from *(2)[unfolded vsf]
have vw: "((v1,s1),(v2,s2)) ∈ set vs" and s1: "s1 ∉ tsorts" by auto
from inp vw vs have "s1 = s2" by fastforce
with s1 show "(α (v1,s1) = α (v2,s2)) = (β (v1,s1) = β (v2,s2))" unfolding β_def by auto
qed
have "?sat1 bnds β" unfolding set_bnds using sat1
unfolding β_def triv non_triv tsorts_def f_def by force
moreover have "?sat2 diffs β" using sat2[unfolded αβ] unfolding newdiffs_def by auto
ultimately show "fidl_solvable (bnds, diffs)" unfolding fidl_solvable_def by auto
next
assume "fidl_solvable (bnds, diffs)"
from this[unfolded fidl_solvable_def split] obtain α
where sat1: "?sat1 bnds α" and sat2: "?sat2 diffs α" by blast
from sat1 have "?sat1 non_triv α" unfolding non_triv by auto
moreover have "?sat2 newdiffs α"
proof
fix vsf
assume "vsf ∈ set newdiffs"
from this[unfolded newdiffs_def]
obtain vs where vs: "vs ∈ set diffs" and vsf: "vsf = filter (λvs. snd (fst vs) ∉ tsorts) vs" by auto
from sat2[rule_format, OF vs] obtain v w where vw: "(v,w) ∈ set vs" and diff: "α v ≠ α w" by auto
from vs vw have vw': "(v,w) ∈ set (concat diffs)" by auto
from inp vw' have vw_sort: "snd v = snd w" by blast
from inp vw' have vw_bnds: "{v,w} ⊆ fst ` set bnds" by blast
then obtain b bw where "{(v,b),(w,bw)} ⊆ set bnds" by auto
with inp vw_sort have bnds: "{(v,b),(w,b)} ⊆ set bnds" by (metis insert_subset)
with sat1 have "0 ≤ α v" "α v ≤ b" "0 ≤ α w" "α w ≤ b" by auto
with diff have b0: "b ≠ 0" by auto
have "snd v ∉ tsorts"
proof
assume "snd v ∈ tsorts"
from this[unfolded tsorts_def triv f_def]
obtain u where u0: "(u,0) ∈ set bnds" and same_sort: "snd u = snd v" by auto
from bnds inp u0 same_sort have "b = 0" by blast
with b0 show False by auto
qed
with vw have "(v,w) ∈ set vsf" unfolding vsf by auto
with diff show "∃(v, w)∈set vsf. α v ≠ α w" by auto
qed
ultimately show "fidl_solvable (non_triv, newdiffs)"
by (auto simp: fidl_solvable_def)
qed
have outp: "ooutput = (if [] ∈ set newdiffs then None else Some ?out)"
using del by (auto simp: Cons tsorts_def newdiffs_def Let_def)
show ?thesis
proof (cases "[] ∈ set newdiffs")
case False
thus ?thesis using outp main out_conds by auto
next
case True
from split_list[OF this]
show ?thesis using outp unfolding main
by (auto simp: fidl_input_def fidl_solvable_def)
qed
qed
qed
fun assign_by_sort :: "('s, (int × ('v × int)list)) mapping ⇒ (('v × 's) × int) list
⇒ ('s, int × ('v × int)list) mapping" where
"assign_by_sort m [] = m"
| "assign_by_sort m (((v,s),b) # bnds) = (case Mapping.lookup m s of
None ⇒ assign_by_sort (Mapping.update s (b,[(v,b)]) m) bnds
| Some (b,vs) ⇒ assign_by_sort (Mapping.update s (b - 1, (v, b - 1) # vs) m) bnds)"
lemma assign_by_sort_computation: fixes bnds :: "(('v × 's) × int) list" and s :: 's
assumes filt: "filt = filter ((=) s ∘ snd ∘ fst) bnds"
shows "Mapping.lookup (assign_by_sort Mapping.empty bnds) s = (if filt = [] then None
else Some
(snd (hd filt) - int (length filt) + 1,
rev (map (λi. (fst (fst (filt ! i)), snd (hd filt) - int i)) [0..<length filt])))"
proof -
let ?f = "λ m ((v :: 'v,s :: 's),b :: int). case m of None ⇒ Some (b :: int,[(v,b)]) | Some (b :: int,vs) ⇒ Some (b - 1, (v, b - 1) # vs)"
let ?filt = filt
define f where "f = ?f"
define fi :: "(('v × 's) × int) ⇒ bool" where "fi = (((=) s) o snd o fst)"
{
fix a bnds' m
have "Mapping.lookup m s = foldl f a (filter fi bnds')
⟹ Mapping.lookup (assign_by_sort m bnds) s =
foldl f a (filter fi (bnds' @ bnds))"
proof (induct bnds arbitrary: m bnds')
case (Cons entry bnds m bnds')
obtain v s' b where entry: "entry = ((v,s'),b)" by (cases entry) auto
show ?case
proof (cases "s' = s")
case False
then obtain m' where
id: "assign_by_sort m (entry # bnds) = assign_by_sort m' bnds" and m': "Mapping.lookup m' s = Mapping.lookup m s"
unfolding entry by (cases "Mapping.lookup m s'", auto)
from False have False: "¬ fi entry" unfolding fi_def entry by auto
show ?thesis unfolding id
by (subst Cons(1), rule Cons(2)[folded m'], insert False, auto simp: entry)
next
case True
obtain m' where
id: "assign_by_sort m (entry # bnds) = assign_by_sort m' bnds"
and m': "Mapping.lookup m' s = f (Mapping.lookup m s) entry"
unfolding entry True by (cases "Mapping.lookup m s", auto simp: f_def)
from True have fi: "fi entry" unfolding entry fi_def by auto
have filt: "filter fi ((entry # bnds) @ bnds') = entry # filter fi (bnds @ bnds')"
unfolding entry True fi_def by auto
show ?thesis unfolding id filt
by (subst Cons(1)[where bnds' = "bnds' @ [entry]"], subst m'[unfolded Cons(2)], insert fi, auto)
qed
qed auto
}
from this[of Mapping.empty None Nil]
have impl: "Mapping.lookup (assign_by_sort Mapping.empty bnds) s = foldl f None (filter fi bnds)"
by auto
define filt where "filt = filter fi bnds"
{
assume "filt ≠ []"
then obtain x0 b0 s' bnds'
where filt: "filt = ((x0,s'),b0) # bnds'" by (cases filt, auto)
have fold: "foldl f (Some (b,xs)) bnds' =
Some (b - int (length bnds'),
rev (map2 (λi v. (fst (fst v), b - i)) [1.. int (length bnds')] bnds') @ xs)"
for b xs
proof (induct bnds' arbitrary: b xs)
case (Cons entry bnds)
obtain x s b' where entry: "entry = ((x,s),b')" by (cases entry) auto
have f_entry: "f (Some (b, xs)) entry = Some (b - 1, (x, b - 1) # xs)"
unfolding f_def entry by simp
have list: "[1..int (length bnds + Suc 0)] = 1 # map ((+) 1) [1..int (length bnds)]"
apply (intro nth_equalityI, force)
subgoal for i by (cases i, auto)
done
have map_eq: "map2 (λx y. (fst (fst y), b - 1 - x)) [1..int (length bnds)] bnds =
map2 (λx y. (fst (fst y), b - x)) (map ((+) 1) [1..int (length bnds)]) bnds"
by (intro nth_equalityI, auto)
show ?case unfolding foldl.simps list.size f_entry
unfolding Cons option.simps prod.simps unfolding list
by (intro conjI, force, insert map_eq, simp add: entry)
qed auto
have "Mapping.lookup (assign_by_sort Mapping.empty bnds) s = foldl f (Some (b0,[(x0,b0)])) bnds'"
unfolding impl filt_def[symmetric] filt by (simp add: f_def)
also have "… = Some
(b0 - int (length filt) + 1,
rev (map (λ i. (fst (fst (filt ! i)), b0 - int i)) [0 ..< length filt]))"
unfolding fold option.simps prod.simps rev.simps(2)[symmetric]
proof (intro conjI arg_cong[of _ _ rev])
show "(x0, b0) # map2 (λx y. (fst (fst y), b0 - x)) [1..int (length bnds')] bnds' =
map (λi. (fst (fst (filt ! i)), b0 - int i)) [0..<length filt]"
unfolding filt fst_conv list.size
apply (intro nth_equalityI, force)
subgoal for i apply (cases i, simp_all add: nth_append)
by (metis Suc_lessI nth_Cons_Suc)
done
qed (simp add: filt)
finally have "Mapping.lookup (assign_by_sort Mapping.empty bnds) s =
Some (snd (hd filt) - int (length filt) + 1, rev (map (λi. (fst (fst (filt ! i)), snd (hd filt) - int i)) [0..<length filt]))"
unfolding filt
by auto
} note ne_impl = this
have filt: "filt = ?filt" unfolding filt filt_def fi_def ..
show ?thesis
proof (cases "filt = []")
case False
thus ?thesis unfolding ne_impl[OF False] filt by auto
next
case True
thus ?thesis using filt unfolding impl filt_def[symmetric] by auto
qed
qed
definition find_large_sorts :: "(('v × 's) × int) list ⇒ 's set" where
"find_large_sorts bnds = (let
m = assign_by_sort Mapping.empty bnds;
mf = Mapping.filter (λ s (b,vs). b ≥ 0) m
in Mapping.keys mf)"
text ‹Delete all variables of a sort where the upper bound is large
enough to make all variables of this sort distinct.
Afterwards also delete all non-occurring variables from the bounds-list.›
definition delete_large_sorts_single :: "('v,'s)fidl_input ⇒ ('v,'s)fidl_input × bool" where
"delete_large_sorts_single = (λ (bnds, diffs).
let lsorts = find_large_sorts bnds
in if Set.is_empty lsorts then ((bnds,diffs), False)
else let newdiffs = filter (λ vs. ∀ vw ∈ set vs. snd (fst vw) ∉ lsorts) diffs;
remvars = set (List.maps (List.maps (λ (v,w). [v,w])) newdiffs);
newbnds = filter (λ vb. fst vb ∈ remvars) bnds
in ((newbnds, newdiffs),True))"
lemma delete_large_sorts_single: assumes inp: "fidl_input (input :: ('v,'s)fidl_input)"
and del: "delete_large_sorts_single input = (output,changed)"
shows "fidl_input output ∧
(fidl_solvable input = fidl_solvable output) ∧
(changed ⟶ length (fst input) > length (fst output))"
proof -
obtain bnds diffs where input: "input = (bnds,diffs)" by force
define lsorts where "lsorts = find_large_sorts bnds"
show ?thesis
proof (cases "Set.is_empty lsorts")
case True
with del inp show ?thesis
unfolding delete_large_sorts_single_def input split lsorts_def Let_def by auto
next
case False
define f where "f vs = (∀vw∈set vs. snd (fst vw) ∉ lsorts)" for vs :: "(('v × 's) × 'v × 's) list"
define newdiffs where "newdiffs = filter f diffs"
define remvars where "remvars = set (List.maps (List.maps (λ(v, w). [v, w])) newdiffs)"
define newbnds where "newbnds = filter (λvb. fst vb ∈ remvars) bnds"
let ?out = "(newbnds, newdiffs)"
from del[unfolded delete_large_sorts_single_def input split] False
have outp: "output = ?out"
by (simp add: Let_def lsorts_def newdiffs_def remvars_def newbnds_def f_def[abs_def])
note inp = inp[unfolded input fidl_input_def split]
from inp have dist: "distinct (map fst bnds)" by blast
have nd_sub: "set newdiffs ⊆ set diffs" unfolding newdiffs_def by auto
have nb_sub: "set newbnds ⊆ set bnds" unfolding newbnds_def by auto
have fidl_out': "fidl_input output"
unfolding fidl_input_def split outp
proof (intro conjI allI impI)
show "distinct (map fst newbnds)" unfolding newbnds_def by (rule distinct_map_filter[OF dist])
show "⋀v w b1 b2. (v, b1) ∈ set newbnds ⟹ (w, b2) ∈ set newbnds ⟹ snd v = snd w ⟹ b1 = b2"
using nb_sub inp by blast
show "⋀v b. (v, b) ∈ set newbnds ⟹ 0 ≤ b" using nb_sub inp by blast
from nd_sub have csub: "set (concat newdiffs) ⊆ set (concat diffs)" by auto
from csub show "⋀v w. (v, w) ∈ set (concat newdiffs) ⟹ snd v = snd w" using inp by (meson in_mono)
from csub show "⋀v w. (v, w) ∈ set (concat newdiffs) ⟹ v ≠ w" using inp by auto
fix v w u
assume vw: "(v, w) ∈ set (concat newdiffs)" and u: "u ∈ {v, w}"
with csub inp have ubnds: "u ∈ fst ` set bnds" by (meson in_mono)
from vw u have "u ∈ remvars" unfolding remvars_def List.maps_def
by (cases v; cases w; cases u; force)
with vw u ubnds show "u ∈ fst ` set newbnds" unfolding newbnds_def by force
qed
note fidl_out = fidl_out'[unfolded outp fidl_input_def split]
show ?thesis
proof (intro conjI impI fidl_out')
let ?sat1 = "λ bnds α. (∀(v, b)∈set bnds. 0 ≤ α v ∧ α v ≤ b)"
let ?sat2 = "λ diffs α. (∀c∈set diffs. ∃(v, w)∈set c. α v ≠ α w)"
let ?sat = "λ bnds diffs α. ?sat1 bnds α ∧ ?sat2 diffs α"
show "fidl_solvable input = fidl_solvable output"
proof
assume "fidl_solvable input"
then obtain α where "?sat bnds diffs α" unfolding fidl_solvable_def input by auto
hence "?sat newbnds newdiffs α" using nd_sub nb_sub by auto
thus "fidl_solvable output" unfolding fidl_solvable_def outp by auto
next
assume "fidl_solvable output"
from this[unfolded fidl_solvable_def outp] obtain α where
sat1: "?sat1 newbnds α" and sat2: "?sat2 newdiffs α" by auto
define m where "m = assign_by_sort Mapping.empty bnds"
define filt where "filt s = filter ((=) s ∘ snd ∘ fst) bnds" for s
define mf where "mf = Mapping.filter (λ s (b,vs). b ≥ 0) m"
{
fix s i vs
assume "Mapping.lookup mf s = Some (i,vs)"
from this[unfolded mf_def] have look_m: "Mapping.lookup m s = Some (i,vs)" and i0: "i ≥ 0"
by (transfer, auto split: option.splits if_splits)+
from look_m[unfolded m_def assign_by_sort_computation[OF filt_def]]
have i: "i = snd (hd (filt s)) - int (length (filt s)) + 1"
and vs: "vs = rev (map (λi. (fst (fst (filt s ! i)), snd (hd (filt s)) - int i)) [0..<length (filt s)])"
and ne: "filt s ≠ []" by (auto split: if_splits)
from ne obtain x b s' fs where "filt s = ((x,s'),b) # fs"
by (cases "filt s", auto)
with arg_cong[OF this, of set, unfolded filt_def]
have filt: "filt s = ((x,s),b) # fs" unfolding filt_def by (force simp: o_def)
from arg_cong[OF filt[unfolded filt_def], of set]
have in_bnds: "((x,s),b) ∈ set bnds" by auto
from filt have hd: "hd (filt s) = ((x,s),b)" by auto
note i = i[unfolded hd snd_conv]
note vs = vs[unfolded hd snd_conv]
from i0[unfolded i]
have bnd: "int (length (filt s)) ≤ b + 1" by simp
from arg_cong[OF vs, of "λ s. snd ` set s"] bnd
have bounded: "snd ` set vs ⊆ {0..b}" by auto
have dist: "distinct (map snd vs)"
unfolding vs rev_map[symmetric] distinct_rev
unfolding map_map o_def snd_conv
unfolding distinct_map by (auto simp: inj_on_def)
have image: "(fst o fst) ` set (filt s) ⊆ fst ` set vs"
unfolding vs set_map set_rev fst_conv image_comp o_def set_upt
unfolding set_conv_nth by auto
have "∃ x b. ((x,s),b) ∈ set bnds ∧ snd ` set vs ⊆ {0..b}" using bounded in_bnds by auto
note image dist this
} note mf_lookup = this
define β where "β = (λ (v,s).
case Mapping.lookup mf s of None ⇒ if (v,s) ∈ fst ` set newbnds then α (v,s) else 0 | Some (_,vs) ⇒ the (map_of vs v))"
have lsorts: "lsorts = Mapping.keys mf" unfolding mf_def m_def lsorts_def find_large_sorts_def Let_def ..
have "?sat1 bnds β"
proof (intro ballI, clarsimp)
fix v s b
assume vsb: "((v,s),b) ∈ set bnds"
with inp have b0: "b ≥ 0" by auto
show "0 ≤ β (v, s) ∧ β (v, s) ≤ b"
proof (cases "s ∈ lsorts")
case False
hence βα: "β (v,s) = (if (v,s) ∈ fst ` set newbnds then α (v,s) else 0)"
unfolding β_def split lsorts keys_dom_lookup by (cases "Mapping.lookup mf s", auto)
show ?thesis
proof (cases "(v,s) ∈ fst ` set newbnds")
case True
with vsb have mem: "((v,s),b) ∈ set newbnds" unfolding newbnds_def by auto
with βα have "β (v,s) = α (v,s)" by force
from sat1[rule_format, OF mem] this show ?thesis by auto
next
case False
with βα b0 show ?thesis by auto
qed
next
case True
from this[unfolded lsorts keys_dom_lookup]
obtain i vs where look_mf: "Mapping.lookup mf s = Some (i,vs)" by auto
from vsb have "v ∈ (fst ∘ fst) ` set (filt s)" unfolding filt_def by force
with mf_lookup[OF look_mf] obtain x b' where v: "v ∈ fst ` set vs"
and x: "((x, s), b') ∈ set bnds" and vs: "snd ` set vs ⊆ {0..b'}" by blast
from x vsb inp have "b' = b" by auto
note vs = vs[unfolded this]
from v have "map_of vs v ≠ None"
by (simp add: map_of_eq_None_iff)
then obtain i where map: "map_of vs v = Some i" by blast
from map_of_SomeD[OF this] vs have i: "i ∈ {0..b}" by auto
have β: "β (v,s) = the (map_of vs v)" unfolding β_def look_mf split by auto
thus ?thesis unfolding map using i by auto
qed
qed
moreover
have "?sat2 diffs β"
proof
fix c
assume c: "c ∈ set diffs"
show "∃(v, w)∈set c. β v ≠ β w"
proof (cases "c ∈ set newdiffs")
case True
from this[unfolded newdiffs_def] have fc: "f c" by auto
from True sat2 obtain v w where vw: "(v,w) ∈ set c" and diff: "α v ≠ α w" by auto
from fc[unfolded f_def] vw have sort: "snd v ∉ lsorts" by auto
from fidl_out True vw have vw_bnds: "{v,w} ⊆ fst ` set newbnds" unfolding set_concat
by (smt (verit, ccfv_SIG) UnionI image_iff subset_eq)
from fidl_out True vw have same_sort: "snd v = snd w" unfolding set_concat by blast
{
fix u
assume "u ∈ {v,w}"
with sort same_sort vw_bnds obtain x s where
u: "u = (x,s)" and s: "s ∉ lsorts" "(x,s) ∈ fst ` set newbnds" by force
have "β u = α u" unfolding β_def u split using s
by (cases "Mapping.lookup mf s", auto simp: lsorts keys_dom_lookup)
}
with vw diff show "∃(v, w)∈set c. β v ≠ β w"
by (intro bexI[of _ "(v,w)"], auto)
next
case False
from this[unfolded newdiffs_def] c have "¬ f c" by auto
from this[unfolded f_def] obtain v w where
vw: "(v,w) ∈ set c" and sort: "snd v ∈ lsorts" by force
from vw inp c have "snd v = snd w" unfolding set_concat by blast
with sort obtain x y s where v: "v = (x,s)" and w: "w = (y,s)" and s: "s ∈ lsorts"
by (cases v; cases w; auto)
from s[unfolded lsorts keys_dom_lookup]
obtain i vs where look_mf: "Mapping.lookup mf s = Some (i,vs)" by auto
from vw inp c have "v ≠ w" unfolding set_concat by blast
with v w have xy: "x ≠ y" by auto
have βv: "β v = the (map_of vs x)" unfolding β_def look_mf split v by auto
have βw: "β w = the (map_of vs y)" unfolding β_def look_mf split w by auto
show "∃(v, w)∈set c. β v ≠ β w"
proof (intro bexI[OF _ vw], unfold split βv βw)
from mf_lookup[OF look_mf]
have sub: "(fst ∘ fst) ` set (filt s) ⊆ fst ` set vs"
and dist: "distinct (map snd vs)" by auto
from vw c have "(v,w) ∈ set (concat diffs)" by auto
with inp have vw: "{v,w} ⊆ fst ` set bnds" by blast
{
fix z
assume "z ∈ {x,y}"
hence "(z,s) ∈ fst ` set bnds" using vw unfolding v w by auto
hence "z ∈ (fst ∘ fst) ` set (filt s)" unfolding filt_def by force
with sub have "z ∈ fst ` set vs" by auto
hence "map_of vs z ≠ None" by (simp add: map_of_eq_None_iff)
}
from this[of x] this[of y] obtain i j where
map: "map_of vs x = Some i" "map_of vs y = Some j"
by auto
hence mem: "(x,i) ∈ set vs" "(y,j) ∈ set vs" by (auto simp: map_of_SomeD)
then obtain k l where *: "k < length vs" "vs ! k = (x,i)" "l < length vs" "vs ! l = (y,j)"
unfolding set_conv_nth by auto
from * xy have "k ≠ l" by auto
with dist * have ij: "i ≠ j" unfolding distinct_conv_nth by force
thus "the (map_of vs x) ≠ the (map_of vs y)" unfolding map by auto
qed
qed
qed
ultimately show "fidl_solvable input" unfolding input fidl_solvable_def by auto
qed
next
define m where "m = assign_by_sort Mapping.empty bnds"
define filt where "filt s = filter ((=) s ∘ snd ∘ fst) bnds" for s
define mf where "mf = Mapping.filter (λ s (b,vs). b ≥ 0) m"
from False obtain s where sl: "s ∈ lsorts" by (auto simp: Set.is_empty_def)
from this[unfolded lsorts_def find_large_sorts_def Let_def, folded m_def]
have s: "s ∈ Mapping.keys m" using keys_filter by fastforce
let ?f = "((=) s ∘ snd ∘ fst)"
from s obtain b vs where "Mapping.lookup m s = Some (b,vs)"
by (metis in_keysD surj_pair)
with assign_by_sort_computation[OF filt_def, folded m_def, of s] have "set (filt s) ≠ {}"
by (auto split: if_splits)
from this[unfolded filt_def] obtain e where fe: "?f e" and e: "e ∈ set bnds" by auto
from fe obtain v b where e_id: "e = ((v,s),b)" by (cases e, auto)
let ?v = "(v,s)"
from split_list[OF e] obtain bef aft where bnds: "bnds = bef @ e # aft" by auto
have e: "fst e ∉ remvars"
proof
assume "fst e ∈ remvars"
from this[unfolded remvars_def e_id fst_conv] obtain w
where "(?v,w) ∈ set (concat newdiffs) ∨ (w,?v) ∈ set (concat newdiffs)"
unfolding List.maps_def by auto
from this[unfolded newdiffs_def] obtain vs where f: "f vs" and vs: "vs ∈ set diffs"
and "(?v,w) ∈ set vs ∨ (w,?v) ∈ set vs" by auto
from this(3) f[unfolded f_def] sl
have "(w,?v) ∈ set vs" and snd: "snd w ≠ s" by auto
from this(1) vs have "(w,?v) ∈ set (concat diffs)" by auto
with inp have "snd w = snd ?v" by blast
with snd show False by auto
qed
have "length (fst output) = length (filter (λvb. fst vb ∈ remvars) (bef @ aft))"
unfolding outp fst_conv newbnds_def bnds using e by auto
also have "… ≤ length (bef @ aft)" by (rule length_filter_le)
also have "… < length (fst input)" unfolding input bnds by auto
finally show "length (fst output) < length (fst input)" .
qed
qed
qed
partial_function (tailrec) delete_large_sorts :: "('v,'s)fidl_input ⇒ ('v,'s)fidl_input" where
[code]: "delete_large_sorts inp = (case delete_large_sorts_single inp of
(out,changed) ⇒ if changed then delete_large_sorts out else out)"
lemma delete_large_sorts: assumes "fidl_input inp"
and del: "delete_large_sorts inp = out"
shows "fidl_input out ∧ fidl_solvable inp = fidl_solvable out"
using assms
proof (induct inp rule: wf_induct[OF wf_measure, of "length o fst"])
case (1 inp)
obtain mid ch where single: "delete_large_sorts_single inp = (mid,ch)" (is "?e = _") by (cases ?e, auto)
from delete_large_sorts_single[OF 1(2) this]
have *: "fidl_input mid"
"fidl_solvable inp = fidl_solvable mid"
"ch ⟹ length (fst mid) < length (fst inp)"
by auto
note out = 1(3)[unfolded delete_large_sorts.simps[of inp, unfolded single split]]
show ?case
proof (cases ch)
case False
with out * show ?thesis by auto
next
case True
with out have out: "delete_large_sorts mid = out" by auto
from *(3)[OF True] have "(mid, inp) ∈ measure (length ∘ fst)" by auto
from 1(1)[rule_format, OF this *(1) out] * show ?thesis by auto
qed
qed
definition fidl_pre_processor where
"fidl_pre_processor solver input = (case delete_trivial_sorts input
of None ⇒ False
| Some mid ⇒ let (bnds',diffs') = delete_large_sorts mid
in if bnds' = [] ∧ diffs' = [] then True else solver (bnds', diffs'))"
lemma fidl_pre_processor: assumes "finite_idl_solver solver"
shows "finite_idl_solver (fidl_pre_processor solver)"
unfolding finite_idl_solver_def
proof (intro allI impI)
fix input :: "('a,'b)fidl_input"
assume bd: "fidl_input input"
note triv = delete_trivial_sorts[OF bd]
note res = fidl_pre_processor_def[of solver input]
show "fidl_pre_processor solver input = fidl_solvable input"
proof (cases "delete_trivial_sorts input")
case None
with triv res show ?thesis by auto
next
case (Some mid)
from triv[OF Some, of mid]
have mid: "fidl_input mid" and bd: "fidl_solvable input = fidl_solvable mid" by auto
note res = res[unfolded Some option.simps]
obtain ob od where large: "delete_large_sorts mid = (ob,od)" by force
note res = res[unfolded large Let_def split]
from delete_large_sorts[OF mid large]
have out: "fidl_input (ob, od)" and mid: "fidl_solvable mid = fidl_solvable (ob, od)" by auto
show ?thesis
proof (cases "ob = [] ∧ od = []")
case True
hence "fidl_solvable (ob,od)" unfolding fidl_solvable_def by auto
with True res show ?thesis unfolding bd mid by auto
next
case False
from assms[unfolded finite_idl_solver_def, rule_format, OF out]
show ?thesis using False unfolding bd mid res by auto
qed
qed
qed