Theory IsaSAT_Bump_Heuristics_Init_State
theory IsaSAT_Bump_Heuristics_Init_State
imports Watched_Literals_VMTF IsaSAT_ACIDS
Tuple4 IsaSAT_ACIDS Pairing_Heap_LLVM.Relational_Pairing_Heaps Pairing_Heap_LLVM.Pairing_Heaps_Impl
begin
type_synonym vmtf_remove_int_option_fst_As = ‹nat_vmtf_node list × nat × nat option × nat option × nat option›
definition isa_vmtf_init
:: ‹nat multiset ⇒ (nat, nat) ann_lits ⇒ vmtf_remove_int_option_fst_As set›
where
‹isa_vmtf_init 𝒜⇩i⇩n M = {(ns, m, fst_As, lst_As, next_search).
𝒜⇩i⇩n ≠ {#} ⟶ (fst_As ≠ None ∧ lst_As ≠ None ∧ (ns, m, the fst_As, the lst_As, next_search) ∈ vmtf 𝒜⇩i⇩n M)}›
type_synonym bump_heuristics_init = ‹((nat,nat)acids,vmtf_remove_int_option_fst_As, bool, nat list × bool list) tuple4›
abbreviation Bump_Heuristics_Init :: ‹_ ⇒ _ ⇒ _ ⇒ _ ⇒ bump_heuristics_init› where
‹Bump_Heuristics_Init a b c d ≡ Tuple4 a b c d›
lemmas bump_heuristics_init_splits = Tuple4.tuple4.splits
hide_fact tuple4.splits
abbreviation get_stable_heuristics :: ‹bump_heuristics_init ⇒ (nat,nat) acids› where
‹get_stable_heuristics ≡ Tuple4_a›
abbreviation get_focused_heuristics :: ‹bump_heuristics_init ⇒ vmtf_remove_int_option_fst_As› where
‹get_focused_heuristics ≡ Tuple4_b›
abbreviation is_focused_heuristics :: ‹bump_heuristics_init ⇒ bool› where
‹is_focused_heuristics ≡ Tuple4_c›
abbreviation is_stable_heuristics:: ‹bump_heuristics_init ⇒ bool› where
‹is_stable_heuristics x ≡ ¬is_focused_heuristics x›
abbreviation get_bumped_variables :: ‹bump_heuristics_init ⇒ nat list × bool list› where
‹get_bumped_variables ≡ Tuple4_d›
abbreviation set_stable_heuristics :: ‹(nat,nat)acids ⇒bump_heuristics_init ⇒ _› where
‹set_stable_heuristics ≡ Tuple4.set_a›
abbreviation set_focused_heuristics :: ‹vmtf_remove_int_option_fst_As ⇒bump_heuristics_init ⇒ _› where
‹set_focused_heuristics ≡ Tuple4.set_b›
abbreviation set_is_focused_heuristics :: ‹bool ⇒bump_heuristics_init ⇒ _› where
‹set_is_focused_heuristics ≡ Tuple4.set_c›
abbreviation set_bumped_variables :: ‹nat list × bool list ⇒bump_heuristics_init ⇒ _› where
‹set_bumped_variables ≡ Tuple4.set_d›
definition get_unit_trail where
‹get_unit_trail M = (rev (takeWhile (λx. ¬is_decided x) (rev M)))›
definition bump_heur_init :: ‹_ ⇒ _ ⇒ bump_heuristics_init set› where
‹bump_heur_init 𝒜 M = {x.
get_stable_heuristics x ∈ acids 𝒜 M ∧
get_focused_heuristics x ∈ isa_vmtf_init 𝒜 M ∧
(get_bumped_variables x, set (fst (get_bumped_variables x))) ∈ distinct_atoms_rel 𝒜 ∧
count_decided M = 0
}›
lemma get_unit_trail_count_decided_0[simp]: ‹count_decided M = 0 ⟹ get_unit_trail M = M›
by (auto simp: get_unit_trail_def count_decided_0_iff)
(metis rev_swap set_rev takeWhile_eq_all_conv)
subsection ‹Access Function›
definition vmtf_heur_import_variable :: ‹nat ⇒ vmtf_remove_int_option_fst_As ⇒ _› where
‹vmtf_heur_import_variable L = (λ(n, stmp, fst, last, cnext).
(vmtf_cons n L cnext stmp, stmp+1, fst, Some L, cnext))›
definition acids_heur_import_variable :: ‹nat ⇒ (nat, nat) acids ⇒ _› where
‹acids_heur_import_variable L = (λ(bw, m). do {
ASSERT (m ≤ unat32_max);
bw ← ACIDS.mop_prio_insert L m bw;
RETURN (bw, (m+1))
})›
definition initialise_VMTF :: ‹nat list ⇒ nat ⇒ vmtf_remove_int_option_fst_As nres› where
‹initialise_VMTF N n = do {
let A = replicate n (VMTF_Node 0 None None);
ASSERT(length N ≤ unat32_max);
(n, A, cnext) ← WHILE⇩T
(λ(i, A, cnext). i < length_uint32_nat N)
(λ(i, A, cnext). do {
ASSERT(i < length_uint32_nat N);
let L = (N ! (length N - 1 - i));
ASSERT(L < length A);
ASSERT(cnext ≠ None ⟶ the cnext < length A);
ASSERT(i + 1 ≤ unat32_max);
RETURN (i + 1, vmtf_cons A L cnext (i), Some L)
})
(0, A, None);
RETURN ((A, n, cnext, (if N = [] then None else Some ((N!(length N - 1)))), cnext))
}›
definition init_ACIDS0 :: ‹_ ⇒ nat ⇒ (nat multiset × nat multiset × (nat ⇒ nat)) nres› where
‹init_ACIDS0 𝒜 n = do {
ASSERT (𝒜 ≠ {#} ⟶ n > Max (insert 0 (set_mset 𝒜)));
RETURN ((𝒜, {#}, λ_. 0))
}›
definition hp_init_ACIDS0 where
‹hp_init_ACIDS0 _ n = do {
RETURN ((replicate n None, replicate n None, replicate n None, replicate n None, replicate n 0, None))
}›
lemma hp_acids_empty:
‹(hp_init_ACIDS0 𝒜, init_ACIDS0 𝒜) ∈
Id →⇩f ⟨((⟨⟨nat_rel⟩option_rel, ⟨nat_rel⟩option_rel⟩pairing_heaps_rel)) O
acids_encoded_hmrel⟩nres_rel›
proof -
have 1: ‹((𝒜, (λ_. None, λ_. None, λ_. None, λ_. None, λ_. Some 0), None), (𝒜, {#}, λ_. 0)) ∈ acids_encoded_hmrel›
by (auto simp: acids_encoded_hmrel_def pairing_heaps_rel_def map_fun_rel_def
ACIDS.hmrel_def encoded_hp_prop_list_conc_def encoded_hp_prop_def empty_outside_def
intro!: relcompI)
have H: ‹mset_nodes ya ≠ {#}› for ya
by (cases ya) auto
show ?thesis
unfolding uncurry0_def hp_init_ACIDS0_def init_ACIDS0_def
apply (intro frefI nres_relI)
apply refine_rcg
apply (rule relcompI[of])
defer
apply (rule 1)
by (auto simp add: acids_encoded_hmrel_def encoded_hp_prop_def hp_init_ACIDS0_def
ACIDS.hmrel_def encoded_hp_prop_list_conc_def pairing_heaps_rel_def H map_fun_rel_def
split: option.splits dest!: multi_member_split)
qed
definition init_ACIDS where
‹init_ACIDS 𝒜 n = do {
ac ← init_ACIDS0 𝒜 n;
RETURN (ac, 0)
}›
definition initialise_ACIDS :: ‹nat list ⇒ nat ⇒ (nat, nat) acids nres› where
‹initialise_ACIDS N n = do {
A ← init_ACIDS (mset N) n;
ASSERT(length N ≤ unat32_max);
(n, A) ← WHILE⇩T⇗ λ_. True⇖
(λ(i, A). i < length_uint32_nat N)
(λ(i, A). do {
ASSERT(i < length_uint32_nat N);
let L = (N ! i);
ASSERT (snd A = i);
ASSERT(i + 1 ≤ unat32_max);
A ← acids_heur_import_variable L A;
RETURN (i + 1, A)
})
(0, A);
RETURN A
}›
definition initialise_ACIDS_rev where
‹initialise_ACIDS_rev N = initialise_ACIDS (rev N)›
definition (in -) distinct_atms_empty where
‹distinct_atms_empty _ = {}›
definition (in -) distinct_atms_int_empty where
‹distinct_atms_int_empty n = RETURN ([], replicate n False)›
lemma distinct_atms_int_empty_distinct_atms_empty:
‹(distinct_atms_int_empty, RETURN o distinct_atms_empty) ∈
[λn. (∀L∈#ℒ⇩a⇩l⇩l 𝒜. atm_of L < n)]⇩f nat_rel → ⟨distinct_atoms_rel 𝒜⟩nres_rel›
apply (intro frefI nres_relI)
apply (auto simp: distinct_atoms_rel_alt_def distinct_atms_empty_def distinct_atms_int_empty_def)
by (metis atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n atms_of_def imageE)
lemma initialise_VMTF:
shows ‹(uncurry initialise_VMTF, uncurry (λN n. RES (isa_vmtf_init N []))) ∈
[λ(N,n). (∀L∈# N. L < n) ∧ (distinct_mset N) ∧ size N < unat32_max ∧ set_mset N = set_mset 𝒜]⇩f
(⟨nat_rel⟩list_rel_mset_rel) ×⇩f nat_rel → ⟨Id⟩nres_rel›
(is ‹(?init, ?R) ∈ _›)
proof -
have vmtf_ns_notin_empty: ‹vmtf_ns_notin [] 0 (replicate n (VMTF_Node 0 None None))› for n
unfolding vmtf_ns_notin_def
by auto
have K2: ‹distinct N ⟹ fst_As < length N ⟹ N!fst_As ∈ set (take fst_As N) ⟹ False›
for fst_As x N
by (metis (no_types, lifting) in_set_conv_nth length_take less_not_refl min_less_iff_conj
nth_eq_iff_index_eq nth_take)
have W_ref: ‹WHILE⇩T (λ(i, A, cnext). i < length_uint32_nat N')
(λ(i, A, cnext). do {
_ ← ASSERT (i < length_uint32_nat N');
let L = (N' ! (length N' - 1 - i));
_ ← ASSERT (L < length A);
_ ← ASSERT (cnext ≠ None ⟶ the cnext < length A);
_ ← ASSERT (i + 1 ≤ unat32_max);
RETURN
(i + 1,
vmtf_cons A L cnext (i), Some L)
})
(0, replicate n' (VMTF_Node 0 None None),
None)
≤ SPEC(λ(i, A', cnext).
vmtf_ns (rev ((take i (rev N')))) i A'
∧ cnext = (option_last (take i (rev N'))) ∧ i = length N' ∧
length A' = n ∧ vmtf_ns_notin (rev ((take i (rev N')))) i A'
)›
(is ‹_ ≤ SPEC ?P›)
if H: ‹case y of (N, n) ⇒(∀L∈# N. L < n) ∧ distinct_mset N ∧ size N < unat32_max ∧
set_mset N = set_mset 𝒜› and
ref: ‹(x, y) ∈ ⟨Id⟩list_rel_mset_rel ×⇩f nat_rel› and
st[simp]: ‹x = (N', n')› ‹y = (N, n)›
for N N' n n' A x y
proof -
have [simp]: ‹n = n'› and NN': ‹(N', N) ∈ ⟨Id⟩list_rel_mset_rel›
using ref unfolding st by auto
then have dist: ‹distinct N'›
using NN' H by (auto simp: list_rel_def br_def list_mset_rel_def list.rel_eq
list_all2_op_eq_map_right_iff' distinct_image_mset_inj list_rel_mset_rel_def)
have L_N: ‹L < n› if ‹L∈set N'› for L
using H ref that by (auto simp: list_rel_def br_def list_mset_rel_def
list_all2_op_eq_map_right_iff' list_rel_mset_rel_def list.rel_eq)
let ?Q = ‹λ(i, A', cnext).
vmtf_ns (rev ((take i (rev N')))) i A' ∧ i ≤ length N' ∧
cnext = (option_last (take i (rev N'))) ∧
length A' = n ∧ vmtf_ns_notin (rev ((take i (rev N')))) i A'›
have[simp]: ‹N' ! (length N' - Suc a) ∉ set (take a (rev N'))› if ‹a < length N'› for a
by (metis K2 dist distinct_rev length_rev rev_nth that)
show ?thesis
apply (refine_vcg WHILET_rule[where R = ‹measure (λ(i, _). length N' + 1 - i)› and I = ‹?Q›])
subgoal by auto
subgoal by (auto intro: vmtf_ns.intros)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for S N' x2 A'
unfolding assert_bind_spec_conv vmtf_ns_notin_def
using L_N dist
by (auto 5 5 simp: take_Suc_conv_app_nth hd_drop_conv_nth nat_shiftr_div2
option_last_def hd_rev last_map intro!: vmtf_cons dest: K2)
subgoal by auto
subgoal for s
using L_N[of ‹N' ! (length N' - 1 - fst s)›] dist nth_mem[of ‹length N' - 1 - fst s› N']
by (auto simp: take_Suc_conv_app_nth hd_drop_conv_nth nat_shiftr_div2
option_last_def hd_rev last_map simp del: nth_mem)
subgoal
using L_N dist
by (auto simp: last_take_nth_conv option_last_def nth_rev)
subgoal
using H dist ref
by (auto simp: last_take_nth_conv option_last_def list_rel_mset_rel_imp_same_length)
subgoal
using L_N dist
by (auto 5 5 simp: take_Suc_conv_app_nth option_last_def hd_rev nth_rev last_map intro!: vmtf_cons
dest: K2)
subgoal by (auto simp: take_Suc_conv_app_nth)
subgoal by (auto simp: take_Suc_conv_app_nth nth_rev)
subgoal by auto
subgoal
using L_N dist
by (auto 5 5 simp: take_Suc_conv_app_nth hd_rev last_map option_last_def nth_rev
intro!: vmtf_notin_vmtf_cons dest: K2 split: if_splits)
subgoal by auto
subgoal by (auto simp: nth_rev)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
have [simp]: ‹vmtf_ℒ⇩a⇩l⇩l n' [] ((set N, {}))›
if ‹(N, n') ∈ ⟨Id⟩list_rel_mset_rel› for N N' n'
using that unfolding vmtf_ℒ⇩a⇩l⇩l_def
by (auto simp: ℒ⇩a⇩l⇩l_def atms_of_def image_image image_Un list_rel_def
br_def list_mset_rel_def list_all2_op_eq_map_right_iff'
list_rel_mset_rel_def list.rel_eq)
have in_N_in_N1: ‹L ∈ set N' ⟹ L ∈ atms_of (ℒ⇩a⇩l⇩l N)›
if ‹(N', N) ∈ list_mset_rel› for L N N' y
using that by (auto simp: ℒ⇩a⇩l⇩l_def atms_of_def image_image image_Un list_rel_def
list.rel_eq br_def list_mset_rel_def list_all2_op_eq_map_right_iff')
have length_ba: ‹∀L∈# N. L < length ba ⟹ L ∈ atms_of (ℒ⇩a⇩l⇩l N) ⟹
L < length ba›
if ‹(N', y) ∈ ⟨Id⟩list_rel_mset_rel›
for L ba N N' y
using that
by (auto simp: ℒ⇩a⇩l⇩l_def nat_shiftr_div2 list.rel_eq
atms_of_def image_image image_Un split: if_splits)
show ?thesis
supply list.rel_eq[simp]
apply (intro frefI nres_relI)
unfolding initialise_VMTF_def uncurry_def conc_Id id_def isa_vmtf_init_def
distinct_atms_int_empty_def nres_monad1
apply (subst Let_def)
apply (refine_vcg)
subgoal by (auto dest: list_rel_mset_rel_imp_same_length)
apply (rule W_ref[THEN order_trans]; assumption?)
subgoal for N' N'n' n' Nn
apply (auto dest: list_rel_mset_rel_imp_same_length simp: vmtf_def)
apply (rule exI[of _ ‹((fst N'))›])
apply (rule_tac exI[of _ ‹[]›])
apply (auto dest: list_rel_mset_rel_imp_same_length simp: vmtf_def hd_rev last_conv_nth rev_nth
atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
apply (auto dest: list_rel_mset_rel_imp_same_length simp: vmtf_def hd_rev last_conv_nth rev_nth
atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n list_rel_mset_rel_def list_mset_rel_def br_def hd_conv_nth)
done
done
qed
lemma initialise_ACIDS:
shows ‹(uncurry initialise_ACIDS, uncurry (λN n. RES (acids N ([]::(nat,nat)ann_lits)))) ∈
[λ(N,n). (∀L∈# N. L < n) ∧ (distinct_mset N) ∧ size N < unat32_max ∧ set_mset N = set_mset 𝒜]⇩f
(⟨nat_rel⟩list_rel_mset_rel) ×⇩f nat_rel → ⟨Id⟩nres_rel›
(is ‹(?init, ?R) ∈ _›)
proof -
define I' where ‹I' x ≡ (λ(a,b::(nat,nat)acids). b ∈ acids 𝒜 (map (λa. (Decided (Pos a)) :: (nat,nat)ann_lit) (drop a (fst x))) ∧ a ≤ length (fst x) ∧
snd b = a ∧ fst (snd (fst b)) = mset (take a (fst x)))› for x :: ‹nat list × nat›
have I0: ‹(∀L∈#fst y. L < snd y) ∧
distinct_mset (fst y) ∧
size (fst y) < unat32_max ∧ set_mset (fst y) = set_mset 𝒜 ⟹
(x, y) ∈ ⟨nat_rel⟩list_rel_mset_rel ×⇩f nat_rel ⟹
length (fst x) ≤ unat32_max ⟹ I' x (0, (mset (fst x), {#}, λ_. 0), 0)› for x y
by (cases x, cases y)
(auto simp: I'_def acids_def list_rel_mset_rel_def list_mset_rel_def br_def defined_lit_map
dest!: multi_member_split)
have I'_Suc: ‹I' x (fst s + 1,
(fst (fst (snd s)), add_mset (fst x ! fst s) (fst (snd (fst (snd s)))),
(snd (snd (fst (snd s))))(fst x ! fst s := snd (snd s))),
snd (snd s) + 1)› and
pre: ‹fst x ! fst s ∉# fst (snd (fst (snd s)))›
if
‹(∀L∈#fst y. L < snd y) ∧
distinct_mset (fst y) ∧
size (fst y) < unat32_max ∧ set_mset (fst y) = set_mset 𝒜› and
‹(x, y) ∈ ⟨nat_rel⟩list_rel_mset_rel ×⇩f nat_rel› and
‹x = (a, b)› and
‹y = (aa, ba)› and
‹length (fst x) ≤ unat32_max› and
‹I' x s› and
‹fst s < length_uint32_nat (fst x)› and
‹fst s < length_uint32_nat (fst x)› and
‹snd (snd s) = fst s› and
‹fst s + 1 ≤ unat32_max›
for a b aa ba s x y
proof -
have ‹mset (take (Suc (fst s)) a) ⊆# 𝒜›
apply (rule subset_mset.trans[of _ ‹mset a›])
using that
apply (clarsimp_all simp: acids_def defined_lit_map list_rel_mset_rel_def br_def list_mset_rel_def
image_image acids_heur_import_variable_def I'_def mset_take_subseteq)
by (metis distinct_subseteq_iff fst_eqD le_refl set_take_subset take_all_iff that(1))
then show ‹I' x (fst s + 1,
(fst (fst (snd s)), add_mset (fst x ! fst s) (fst (snd (fst (snd s)))),
(snd (snd (fst (snd s))))(fst x ! fst s := snd (snd s))),
snd (snd s) + 1)› ‹fst x ! fst s ∉# fst (snd (fst (snd s)))›
using that
by (force simp: acids_def take_Suc_conv_app_nth defined_lit_map list_rel_mset_rel_def br_def list_mset_rel_def
image_image acids_heur_import_variable_def I'_def Cons_nth_drop_Suc[symmetric] distinct_in_set_take_iff
dest: multi_member_split)+
qed
show ?thesis
unfolding uncurry_def case_prod_beta initialise_ACIDS_def
acids_heur_import_variable_def ACIDS.mop_prio_insert_def nres_monad3
init_ACIDS_def nres_monad3 init_ACIDS0_def
bind_to_let_conv Let_def
apply (intro frefI nres_relI)
subgoal for x y
apply (cases x, cases y)
apply (refine_vcg specify_left[OF WHILEIT_rule_stronger_inv[where Φ = ‹λ(a::nat,b::(nat,nat)acids). b ∈ acids 𝒜 ([]::(nat,nat)ann_lits)› and
I' = ‹I' x› and
R = ‹measure (λ(a,b). length (fst x) - a)›]])
subgoal apply (auto simp: list_rel_mset_rel_def list_mset_rel_def br_def acids_def)
using gt_or_eq_0 by blast
subgoal by (auto simp: list_rel_mset_rel_def list_mset_rel_def br_def)
subgoal by auto
subgoal by auto
subgoal by (rule I0)
subgoal by (auto simp: I'_def)
subgoal by (auto simp:)
subgoal by auto
subgoal by (rule pre)
subgoal by (auto simp: I'_def list_rel_mset_rel_def list_mset_rel_def br_def
acids_def)
subgoal by (rule I'_Suc)
subgoal by (auto simp: I'_def)
subgoal
by (auto simp add: I'_def)
subgoal apply (auto simp: list_rel_mset_rel_def list_mset_rel_def br_def acids_def)
by (metis distinct_subseteq_iff set_mset_mset)
done
done
qed
lemma initialise_ACIDS_rev:
shows ‹(uncurry initialise_ACIDS_rev, uncurry (λN n. RES (acids N ([]::(nat,nat)ann_lits)))) ∈
[λ(N,n). (∀L∈# N. L < n) ∧ (distinct_mset N) ∧ size N < unat32_max ∧ set_mset N = set_mset 𝒜]⇩f
(⟨nat_rel⟩list_rel_mset_rel) ×⇩f nat_rel → ⟨Id⟩nres_rel›
unfolding initialise_ACIDS_rev_def
apply (intro frefI nres_relI)+
unfolding uncurry_def case_prod_beta
apply (rule initialise_ACIDS[where 𝒜=𝒜, THEN fref_to_Down_curry])
by (auto simp: list_mset_rel_def list_rel_mset_rel_def br_def)
definition initialize_Bump_Init :: ‹nat list ⇒ nat ⇒ bump_heuristics_init nres› where
‹initialize_Bump_Init A n = do {
focused ← initialise_VMTF A n;
hstable ← initialise_ACIDS_rev A n;
to_remove ← distinct_atms_int_empty n;
RETURN (Tuple4 hstable focused True to_remove)
}›
lemma specify_left_RES:
assumes "m ≤ RES Φ"
assumes "⋀x. x ∈ Φ ⟹ f x ≤ M"
shows "do { x ← m; f x } ≤ M"
using assms by (auto simp: pw_le_iff refine_pw_simps)
lemma initialize_Bump_Init:
shows ‹(uncurry initialize_Bump_Init, uncurry (λN n. RES (bump_heur_init N []))) ∈
[λ(N,n). (∀L∈# N. L < n) ∧ (distinct_mset N) ∧ size N < unat32_max ∧ set_mset N = set_mset 𝒜]⇩f
(⟨nat_rel⟩list_rel_mset_rel) ×⇩f nat_rel → ⟨Id⟩nres_rel›
(is ‹(?init, ?R) ∈ _›)
unfolding initialize_Bump_Init_def uncurry_def distinct_atms_int_empty_def nres_monad1
apply (intro frefI nres_relI)
apply (refine_rcg)
apply hypsubst
apply (rule specify_left_RES[OF initialise_VMTF[where 𝒜=𝒜, THEN fref_to_Down_curry, unfolded conc_fun_RES]])
apply assumption+
apply (rule specify_left_RES[OF initialise_ACIDS_rev[where 𝒜=𝒜, THEN fref_to_Down_curry, unfolded conc_fun_RES]])
apply assumption+
apply (auto simp: bump_heur_init_def distinct_atoms_rel_def distinct_hash_atoms_rel_def
atoms_hash_rel_def intro!: relcompI)
done
type_synonym bump_heuristics_option_fst_As = ‹vmtf_remove_int_option_fst_As›
lemma isa_vmtf_init_consD:
‹((ns, m, fst_As, lst_As, next_search)) ∈ isa_vmtf_init 𝒜 M ⟹
((ns, m, fst_As, lst_As, next_search)) ∈ isa_vmtf_init 𝒜 (L # M)›
by (auto simp: isa_vmtf_init_def dest: vmtf_consD)
lemma isa_vmtf_init_consD':
‹vm ∈ isa_vmtf_init 𝒜 M ⟹ vm ∈ isa_vmtf_init 𝒜 (L # M)›
by (auto simp: isa_vmtf_init_def dest: vmtf_consD)
lemma vmtf_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ vmtf 𝒜 M ⟹ L ∈ vmtf ℬ M›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
unfolding vmtf_def vmtf_ℒ⇩a⇩l⇩l_def
by auto
lemma isa_vmtf_init_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ isa_vmtf_init 𝒜 M =isa_vmtf_init ℬ M›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] vmtf_cong[of 𝒜 ℬ] vmtf_cong[of ℬ 𝒜]
unfolding isa_vmtf_init_def vmtf_ℒ⇩a⇩l⇩l_def
by auto
lemma isa_acids_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ acids 𝒜 = acids ℬ›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
unfolding acids_def
by (auto intro!: ext intro!: distinct_subseteq_iff[THEN iffD1])
lemma distinct_atoms_rel_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ distinct_atoms_rel 𝒜 = distinct_atoms_rel ℬ›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
unfolding vmtf_def vmtf_ℒ⇩a⇩l⇩l_def distinct_atoms_rel_def atoms_hash_rel_def distinct_hash_atoms_rel_def
by auto
lemma bump_heur_init_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ bump_heur_init 𝒜 M = bump_heur_init ℬ M›
using isa_vmtf_init_cong[of 𝒜 ℬ M]
ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] distinct_atoms_rel_cong[of 𝒜 ℬ] isa_acids_cong[of 𝒜 ℬ]
unfolding bump_heur_init_def isa_acids_cong[of 𝒜 ℬ]
by auto
lemma bump_heur_init_consD':
‹vm ∈ bump_heur_init 𝒜 M ⟹ vm ∈ bump_heur_init 𝒜 (Propagated L n # M)›
by (auto simp: bump_heur_init_def dest: isa_vmtf_init_consD' acids_prepend)
end