# Theory HeuristicProofs

```subsection "Heuristic Proofs"
theory HeuristicProofs
begin

lemma the_real_step_augment:
assumes  steph : "⋀xs var L F Γ. length xs = var ⟹ (∃x. eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ)) = (∃x. eval (step var L F) (xs @ x # Γ))"
shows "(∃xs. (length xs = amount ∧ eval (list_disj (map(λ(L,F,n). ExN n (list_conj (map fm.Atom L @ F))) F))  (xs @ Γ))) = (eval (the_real_step_augment step amount F)  Γ)"
proof(induction amount arbitrary: F Γ)
case 0
then show ?case by auto
next
case (Suc amount)
have h1 : "⋀F. (∃x xs. length xs = amount ∧ F (xs @ x # Γ)) = (∃xs. length xs = Suc amount ∧ F (xs @  Γ))"
by (smt (z3) Suc_inject append.assoc append_Cons append_Nil2 append_eq_conv_conj length_append_singleton lessI self_append_conv2 take_hd_drop)

have h2: "⋀X x Γ. (∃f∈set (dnf_modified X).
eval (case f of (L, F, n) ⇒ ExN n (list_conj (map fm.Atom L @ F))) (x @ Γ)) = (∃(al, fl, n)∈set (dnf_modified X). ∃L. length L = n ∧ (∀a∈set al. aEval a (L @ (x @ Γ))) ∧ (∀f∈set fl. eval f (L @ (x @ Γ))))"
subgoal for X x Γ
apply(rule bex_cong)
apply simp_all
subgoal for f
apply(cases f)
by (metis Un_iff eval.simps(1) imageI)
done
done
have h3 : "⋀G. (∃x. ∃f∈set F. G x f) = (∃f∈set F. ∃x. G x f)"
by blast
show ?case
apply simp
unfolding Suc[symmetric]
unfolding eval_list_disj
apply simp
unfolding h1[symmetric, of "λx. (∃f∈set F. eval (case f of (L, F, n) ⇒ ExN n (list_conj (map fm.Atom L @ F))) x)"]
unfolding HOL.ex_comm[of "λx xs. length xs = amount ∧ (∃f∈set F. eval (case f of (L, F, n) ⇒ ExN n (list_conj (map fm.Atom L @ F))) (xs @ x # Γ))"]
unfolding HOL.ex_comm[of "λx xs. length xs = amount ∧
(∃f∈set (dnf_modified (push_forall
(nnf (unpower 0
(groupQuantifiers
(clearQuantifiers(list_disj (map (λ(L, F, n). ExN n (step (n + amount) L F)) F)))))))).
eval (case f of (L, F, n) ⇒ ExN n (list_conj (map fm.Atom L @ F))) (xs @ x # Γ))"]
apply(rule ex_cong1)
apply simp
subgoal for xs
unfolding h2
unfolding dnf_modified_eval
unfolding opt'
unfolding eval_list_disj
unfolding List.set_map Set.bex_simps(7)
unfolding h3
apply(cases "length xs = amount")
apply(rule bex_cong)
apply simp_all
subgoal for f
apply(cases f)
apply simp
subgoal for a b c
unfolding HOL.ex_comm[of "λx l. length l = c ∧ eval (list_conj (map fm.Atom a @ b)) (l @ xs @ x # Γ)"]
unfolding HOL.ex_comm[of "λx l. length l = c ∧ eval (step (c + amount) a b) (l @ xs @ x # Γ)"]
apply(rule ex_cong1)
apply simp
subgoal for l
apply(cases "length l = c")
apply simp_all
using steph[of "l @ xs" "c + amount" a b Γ]
by simp
done
done
done
done
qed

lemma step_converter :
assumes  steph : "⋀xs var L F Γ. length xs = var ⟹ (∃x. eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ)) = (∃x. eval (step var L F) (xs @ x # Γ))"
shows "⋀var L F Γ. (∃xs. length xs = var + 1 ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. (length xs = (var + 1)) ∧ eval (step var L F) (xs @ Γ))"
proof safe
fix var L F Γ xs
assume h : "length xs = var + 1"
"eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)"
have h1 : "length (take var xs) = var" using h by auto
have h2 : "(∃x. eval (step var L F) (take var xs @ x # Γ))"
using h steph[OF h1]
by (metis Cons_nth_drop_Suc One_nat_def add.right_neutral add_Suc_right append.assoc append_Cons append_Nil append_take_drop_id drop_all lessI order_refl)
then obtain x where h3: "eval (step var L F) (take var xs @ x # Γ)" by auto
show "∃xs. length xs = var + 1 ∧ eval (step var L F) (xs @ Γ)"
apply(rule exI[where x="take var xs @[x]"])
apply (auto)
using h(1) apply simp
using h3 by simp
next
fix var L F Γ xs
assume h: "length xs = var + 1"
"eval (step var L F) (xs @ Γ)"
have h1 : "length (take var xs) = var" using h by auto
have h2 : "(∃x. eval (list_conj (map fm.Atom L @ F)) (take var xs @ x # Γ))"
using h steph[OF h1]
by (metis Cons_nth_drop_Suc One_nat_def add.right_neutral add_Suc_right append.assoc append_Cons append_Nil append_take_drop_id drop_all lessI order_refl)
then obtain x where h3: "eval (list_conj (map fm.Atom L @ F)) (take var xs @ x # Γ)" by auto
show "∃xs. length xs = var + 1 ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)"
apply(rule exI[where x="take var xs @[x]"])
apply (auto)
using h(1) apply simp
using h3 by simp
qed

lemma step_augmenter_eval :
assumes  steph : "⋀xs var L F Γ. length xs = var ⟹ (∃x. eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ)) = (∃x. eval (step var L F) (xs @ x # Γ))"
assumes heuristic: "⋀n var L F. heuristic n L F = var ⟹ var ≤ n"
shows "⋀var amount L F Γ.
amount ≤ var + 1 ⟹
(∃xs. length xs = var + 1 ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. (length xs = (var + 1)) ∧ eval (step_augment step heuristic amount var L F) (xs @ Γ))"
subgoal for var amount L F Γ
proof(induction var arbitrary: L F Γ amount)
case 0
then have "amount = 0 ∨ amount = Suc 0" by auto
then show ?case apply simp using steph[of "[]" 0 L F Γ] apply auto
apply (metis append_Cons length_Cons list.size(3) self_append_conv2)
apply (metis append_Cons length_Cons list.size(3) self_append_conv2)
apply (metis Suc_length_conv append_Cons length_0_conv self_append_conv2)
by (metis Suc_length_conv append_Cons append_self_conv2 length_0_conv)
next
case (Suc var)
define heu where "heu = heuristic (Suc var) L F"
have heurange : "heu ≤ Suc var" unfolding heu_def
have lessThan1 : "1 ≤ var + 1" by auto

{
fix amount
assume amountLessThan: "amount ≤ var + 1"
have "(∃xs. length xs = Suc (Suc var) ∧
eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) = (∃xs. length xs = Suc (Suc var) ∧
eval
(step (Suc var) (map (swap_atom (Suc var) heu) L)
(map (swap_fm (Suc var) heu) F))
(xs @ Γ))"
proof(safe)
fix xs
assume h: "length (xs::real list) = Suc (Suc var)" "eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)"
then have length : "length (take (Suc var) (swap_list (Suc var) heu xs)) = Suc var" by auto
have take: "(take (Suc var) (swap_list (Suc var) heu xs) @ xs ! heu # Γ) = (swap_list (Suc var) heu (xs @ Γ)) " using h(1)
unfolding swap_list.simps
by (smt (verit, ccfv_threshold) Cons_nth_drop_Suc append.right_neutral append_Nil2 append_assoc append_eq_conv_conj append_self_conv2 append_take_drop_id drop0 heu_def heurange le_imp_less_Suc length_greater_0_conv length_list_update lessI list.sel(1) list.sel(3) list.simps(3) list.size(3) list_update_append nth_Cons_0 nth_append nth_append_length nth_list_update_eq take0 take_hd_drop)
have length1 : "Suc var < length (xs @ Γ)" using h by auto
have length2 : "heu < length (xs @ Γ)" using h heurange by auto
have h1: "(∃x. eval
(step (Suc var) (map (swap_atom (Suc var) heu) L)
(map (swap_fm (Suc var) heu) F))
(take (Suc var) (swap_list (Suc var) heu xs) @ x # Γ))"
unfolding steph[OF length, symmetric]
apply(rule exI[where x="nth xs heu"])
using h unfolding eval_list_conj take apply (auto simp del:swap_list.simps)
unfolding swap_fm[OF length1 length2,symmetric] swap_atom[OF length1 length2,symmetric]
by (meson UnCI eval.simps(1) imageI)+
then obtain x where heval: "eval
(step (Suc var) (map (swap_atom (Suc var) heu) L)
(map (swap_fm (Suc var) heu) F))
(take (Suc var) (swap_list (Suc var) heu xs) @ x # Γ)" by auto
show "∃xs. length xs = Suc (Suc var) ∧
eval
(step (Suc var) (map (swap_atom (Suc var) heu) L)
(map (swap_fm (Suc var) heu) F))
(xs @ Γ)"
apply(rule exI[where x="take (Suc var) (swap_list (Suc var) heu xs) @ [x]"])
apply auto
using h apply simp
using heval by auto
next
fix xs
assume h : "length xs = Suc (Suc var)""
eval
(step (Suc var) (map (swap_atom (Suc var) heu) L)
(map (swap_fm (Suc var) heu) F))
(xs @ Γ)"
define choppedXS where "choppedXS = take (Suc var) xs"
then have length : "length choppedXS = Suc var"
using h(1) by force
have "(∃x. eval (step (Suc var) (map (swap_atom (Suc var) heu) L) (map (swap_fm (Suc var) heu) F)) (choppedXS @ x # Γ))"
using h(2) choppedXS_def
by (metis append.assoc append_Cons append_Nil2 append_eq_conv_conj h(1) lessI take_hd_drop)
then have "∃x. (∀l∈ set L. aEval (swap_atom (Suc var) heu l) (choppedXS@x#Γ)) ∧ (∀f∈ set F. eval (swap_fm (Suc var) heu f) (choppedXS@x#Γ))"
unfolding steph[symmetric, OF length, of "(map (swap_atom (Suc var) heu) L)" "(map (swap_fm (Suc var) heu) F)" Γ] eval_list_conj apply auto
by (metis Un_iff eval.simps(1) imageI)
then obtain x where x : "(∀l∈set L. aEval (swap_atom (Suc var) heu l) (choppedXS @ x # Γ)) ∧
(∀f∈set F. eval (swap_fm (Suc var) heu f) (choppedXS @ x # Γ))" by auto
have length1 : "Suc var < length (swap_list (Suc var) heu (choppedXS @ [x]) @ Γ)"
have length2 : "heu < length (swap_list (Suc var) heu (choppedXS @ [x]) @ Γ)"
using ‹Suc var < length (swap_list (Suc var) heu (choppedXS @ [x]) @ Γ)› heurange by linarith
have swapswap : "(swap_list (Suc var) heu (swap_list (Suc var) heu (choppedXS @ [x]) @ Γ)) = (choppedXS @ [x]) @ Γ" apply auto
by (smt (z3) Cons_nth_drop_Suc append_eq_conv_conj append_same_eq heurange id_take_nth_drop le_neq_implies_less length length1 length_append_singleton lessI list.sel(1) list_update_append1 list_update_length list_update_swap nth_append nth_append_length nth_list_update_neq swap_list.simps take_hd_drop take_update_swap upd_conv_take_nth_drop)
show "∃xs. length xs = Suc (Suc var) ∧
eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)"
apply(rule exI[where x="swap_list (Suc var) heu (choppedXS @ [x])"])
apply(auto simp add: eval_list_conj simp del: swap_list.simps)
unfolding swap_atom[OF length1 length2] swap_fm[OF length1 length2] swapswap
using x by auto
qed
also have "... = (∃xs. length xs = Suc (Suc var) ∧
(∃f∈set (dnf ((push_forall ∘ nnf ∘ unpower 0 o groupQuantifiers o clearQuantifiers)(step (Suc var) (map (swap_atom (Suc var) heu) L)
(map (swap_fm (Suc var) heu) F)))).
eval (case f of (x, xa) ⇒ step_augment step heuristic amount var x xa)
(xs @ Γ)))"
unfolding opt[of "(step (Suc var) (map (swap_atom (Suc var) heu) L) (map (swap_fm (Suc var) heu) F))", symmetric]
unfolding dnf_eval[of "(push_forall ∘ nnf ∘ unpower 0 o groupQuantifiers o clearQuantifiers)(step (Suc var) (map (swap_atom (Suc var) heu) L)
(map (swap_fm (Suc var) heu) F))", symmetric]
proof(safe)
fix xs a b
assume h: "length xs = Suc (Suc var)""
(a, b)
∈ set (dnf ((push_forall ∘ nnf ∘ unpower 0 o groupQuantifiers o clearQuantifiers)(step (Suc var) (map (swap_atom (Suc var) heu) L)
(map (swap_fm (Suc var) heu) F)))) ""
∀a∈set a. aEval a (xs @ Γ) ""
∀f∈set b. eval f (xs @ Γ)"
have "(∃xs'. length xs' = var + 1 ∧
eval (step_augment step heuristic amount var a b) (xs' @ xs ! Suc var # Γ))"
unfolding Suc(1)[of amount a b "nth xs (Suc var)#Γ", OF amountLessThan, symmetric]
apply(rule exI[where x="take (Suc var) xs"])
using h(1) h(3-4) apply(auto simp add: eval_list_conj)
apply (metis Cons_nth_drop_Suc append_Cons append_eq_append_conv2 append_eq_conv_conj append_take_drop_id lessI)
by (metis Cons_nth_drop_Suc append_Cons append_eq_append_conv2 append_eq_conv_conj append_take_drop_id lessI)
then obtain xs' where xs': "length xs' = var + 1" "eval (step_augment step heuristic amount var a b) (xs' @ xs ! Suc var # Γ)"
by auto

show "∃xs. length xs = Suc (Suc var) ∧
(∃f∈set (dnf ((push_forall ∘ nnf ∘ unpower 0 o groupQuantifiers o clearQuantifiers)(step (Suc var) (map (swap_atom (Suc var) heu) L)
(map (swap_fm (Suc var) heu) F)))).
eval (case f of (x, xa) ⇒ step_augment step heuristic amount var x xa)
(xs @ Γ))"
apply(rule exI[where x="xs' @[ xs ! Suc var]"])
apply auto
using xs' apply simp
apply(rule bexI[where x="(a,b)"])
using xs' h apply(cases amount) apply (simp_all add:eval_list_conj)
using h(2) by auto
next
fix xs a b
assume h: "length xs = Suc (Suc var) ""
(a, b)
∈ set (dnf ((push_forall ∘ nnf ∘ unpower 0 o groupQuantifiers o clearQuantifiers)(step (Suc var) (map (swap_atom (Suc var) heu) L)
(map (swap_fm (Suc var) heu) F)))) ""
eval (step_augment step heuristic amount var a b) (xs @ Γ)"
have "(∃xs'. length xs' = var + 1 ∧
eval (list_conj (map fm.Atom a @ b)) (xs' @ xs ! Suc var # Γ))"
unfolding Suc(1)[of amount a b "nth xs (Suc var)#Γ", OF amountLessThan]
apply(rule exI[where x="take (Suc var) xs"])
using h(1) h(3) apply auto
by (metis Cons_nth_drop_Suc append.right_neutral append_Cons append_assoc append_eq_conv_conj append_self_conv2 append_take_drop_id lessI)
then obtain xs' where xs': "length xs' = var + 1" " eval (list_conj (map fm.Atom a @ b)) (xs' @ xs ! Suc var # Γ)"
by auto
show "∃xs. length xs = Suc (Suc var) ∧
(∃(al, fl)
∈set (dnf ((push_forall ∘ nnf ∘ unpower 0 o groupQuantifiers o clearQuantifiers)(step (Suc var) (map (swap_atom (Suc var) heu) L)
(map (swap_fm (Suc var) heu) F)))).
(∀a∈set al. aEval a (xs @ Γ)) ∧
(∀f∈set fl. eval f (xs @ Γ)))"
apply(rule exI[where x="xs' @[ xs ! Suc var]"])
apply auto
using xs' apply simp
apply(rule bexI[where x="(a,b)"])
using xs' h apply (simp_all add: eval_list_conj)
proof -
assume "∀f∈fm.Atom ` set a ∪ set b. eval f (xs' @ xs ! Suc var # Γ)"
then have "∀f. f ∈ fm.Atom ` set a ∪ set b ⟶ eval f (xs' @ xs ! Suc var # Γ)"
by meson
then have f1: "v ∉ set a ∨ eval (fm.Atom v) (xs' @ xs ! Suc var # Γ)" for v
by blast
obtain aa :: atom where
"(∃v0. v0 ∈ set a ∧ ¬ eval (fm.Atom v0) (xs' @ xs ! Suc var # Γ)) = (aa ∈ set a ∧ ¬ eval (fm.Atom aa) (xs' @ xs ! Suc var # Γ))"
by blast
then show "∀a∈set a. aEval a (xs' @ xs ! Suc var # Γ)"
using f1 eval.simps(1) by auto
qed

qed
finally have "(∃xs. length xs = Suc (Suc var) ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. length xs = Suc (Suc var) ∧
(∃f∈set (dnf ((push_forall ∘ nnf ∘ unpower 0 o groupQuantifiers o clearQuantifiers) (step (Suc var) (map (swap_atom (Suc var) heu) L) (map (swap_fm (Suc var) heu) F)))).
eval (case f of (x, xa) ⇒ step_augment step heuristic amount var x xa) (xs @ Γ)))"
by auto
}then show ?case apply(cases amount) using Suc(2)  by (simp_all add:eval_list_disj heu_def[symmetric])
qed
done

lemma qe_eq_repeat_eval_augment : "amount ≤ var+1 ⟹
(∃xs. (length xs = var + 1) ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. (length xs = var + 1) ∧ eval (step_augment qe_eq_repeat IdentityHeuristic amount var L F) (xs @ Γ))"
apply(rule step_augmenter_eval[of qe_eq_repeat IdentityHeuristic amount var L F Γ])
using qe_eq_repeat_eval apply blast by auto

lemma qe_eq_repeat_eval' : "
(∃xs. (length xs = var + 1) ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. (length xs = var + 1) ∧ eval (qe_eq_repeat var L F) (xs @ Γ))"
apply(rule step_converter[of qe_eq_repeat var L F Γ])
using qe_eq_repeat_eval by blast

lemma gen_qe_eval_augment : "amount ≤ var+1 ⟹
(∃xs. (length xs = var + 1) ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. (length xs = var + 1) ∧ eval (step_augment gen_qe IdentityHeuristic amount var L F) (xs @ Γ))"
apply(rule step_augmenter_eval[of gen_qe IdentityHeuristic amount var L F Γ])
using gen_qe_eval apply blast by auto

lemma gen_qe_eval' : "
(∃xs. (length xs = var + 1) ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. (length xs = var + 1) ∧ eval (gen_qe var L F) (xs @ Γ))"
apply(rule step_converter[of gen_qe var L F Γ])
using gen_qe_eval by blast

lemma luckyFind_eval_augment : "amount ≤ var+1 ⟹
(∃xs. (length xs = var + 1) ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. (length xs = var + 1) ∧ eval (step_augment luckyFind' IdentityHeuristic amount var L F) (xs @ Γ))"
apply(rule step_augmenter_eval[of luckyFind' IdentityHeuristic amount var L F Γ])
using luckyFind'_eval apply blast by auto

lemma luckyFind_eval' : "
(∃xs. (length xs = var + 1) ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. (length xs = var + 1) ∧ eval (luckyFind' var L F) (xs @ Γ))"
apply(rule step_converter[of luckyFind' var L F Γ])
using luckyFind'_eval by blast

lemma luckiestFind_eval' : "
(∃xs. (length xs = var + 1) ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. (length xs = var + 1) ∧ eval (luckiestFind var L F) (xs @ Γ))"
apply(rule step_converter[of luckiestFind var L F Γ])
using luckiestFind_eval by blast

lemma sortedListMember : "sorted_list_of_fset b = var # list ⟹ fmember var b "
by (metis fset_of_list_elem list.set_intros(1) sorted_list_of_fset_simps(2))

lemma rangeHeuristic :
assumes "heuristicPicker n L F = Some (var, step)"
shows "var≤n"
proof(cases "aquireData n L")
case (fields a b c)
then show ?thesis using assms apply(simp_all del: aquireData.simps getBest.simps)
apply(cases "getBest a L")
apply(simp_all del: aquireData.simps getBest.simps)
apply(cases F) apply(simp_all del: aquireData.simps getBest.simps)
apply(cases "getBest c L") apply(simp_all del: aquireData.simps getBest.simps)
apply(cases "getBest b L")apply(simp_all del: aquireData.simps getBest.simps)
apply (metis not_le_imp_less option.distinct(1) option.inject prod.inject)
apply (metis not_le_imp_less option.distinct(1) option.inject prod.inject)
apply(cases "getBest b L")apply(simp_all del: aquireData.simps getBest.simps)
by (metis not_le_imp_less option.distinct(1) option.inject prod.inject)+
qed

lemma pickedOneOfThem :
assumes "heuristicPicker n L F = Some (var, step)"
shows "step = qe_eq_repeat ∨ step = gen_qe ∨ step = luckyFind'"
using assms
apply(cases "aquireData n L")
subgoal for l e g
using assms apply(simp_all del: aquireData.simps getBest.simps)
apply(cases "getBest l L")
apply(simp_all del: aquireData.simps getBest.simps)
apply(cases F) apply(simp_all del: aquireData.simps getBest.simps)
apply(cases "getBest g L") apply(simp_all del: aquireData.simps getBest.simps)
apply(cases "getBest e L")apply(simp_all del: aquireData.simps getBest.simps)
apply (metis option.distinct(1) option.inject prod.inject)
apply (metis option.distinct(1) option.inject prod.inject)
apply(cases "getBest e L")apply(simp_all del: aquireData.simps getBest.simps)
by (metis  option.distinct(1) option.inject prod.inject)+
done

lemma superPicker_eval :
"amount≤ var+1 ⟹ (∃xs. length xs = var + 1 ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. (length xs = (var + 1)) ∧ eval (superPicker amount var L F) (xs @ Γ))"
proof(induction var arbitrary : L F Γ amount)
case 0
then show ?case apply(simp del:heuristicPicker.simps)
apply(cases "heuristicPicker 0 L F") apply(cases amount)
apply (simp_all del:heuristicPicker.simps)
subgoal for a
apply(cases a)
apply (simp_all del:heuristicPicker.simps)
subgoal for var step
apply(cases var) apply(cases amount)
apply(simp_all del:heuristicPicker.simps)
proof-
assume h: "heuristicPicker 0 L F = Some (0, step)"
show "(∃xs. length xs = Suc 0 ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. length xs = Suc 0 ∧ eval (step 0 L F) (xs @ Γ)) "
using pickedOneOfThem[OF h]
using  qe_eq_repeat_eval'[of 0 L F Γ] gen_qe_eval'[of 0 L F Γ] luckyFind_eval'[of 0 L F Γ]
by auto
next
show "⋀nat. amount ≤ Suc 0 ⟹
heuristicPicker 0 L F = Some (Suc nat, step) ⟹
a = (Suc nat, step) ⟹
var = Suc nat ⟹
(∃xs. length xs = Suc 0 ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. length xs = Suc 0 ∧ eval (superPicker amount 0 L F) (xs @ Γ)) "
apply(cases amount) by(simp_all del:heuristicPicker.simps)
qed
done
done
next
case (Suc i)
then show ?case apply(cases "heuristicPicker (Suc i) L F") apply(cases amount)
apply(simp_all del:heuristicPicker.simps)
subgoal for a
apply(cases a)
apply(simp_all del:heuristicPicker.simps) apply(cases amount) apply simp
apply(cases amount) apply(simp_all del:heuristicPicker.simps)
subgoal for var step amountPred amountPred'
proof-
assume amountPred : "amountPred ≤ Suc i"
assume ih: "(⋀amount L F Γ.
amount ≤ Suc i ⟹
(∃xs. length xs = Suc i ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)) =
(∃xs. length xs = Suc i ∧ eval (superPicker amount i L F) (xs @ Γ)))"
assume h0 : "heuristicPicker (Suc i) L F = Some (var, step)"
have h1: "⋀xs X F. (∃f∈set (map (λ(x, y). F x y)
(dnf X)).
eval f (xs)) = (∃(al,fl)∈set(dnf X).
eval (F al fl) (xs))"
subgoal for xs X F
apply auto
subgoal for a b
apply(rule bexI[where x="(a,b)"])
apply simp_all
done
done
done
have eval_map : "⋀al fl xs Γ.(∀f∈set (map fm.Atom al @ fl). eval f (xs @ Γ)) = ((∀a∈set al. aEval a (xs @ Γ)) ∧ (∀f∈set fl. eval f (xs @ Γ)))"
apply auto
by (meson Un_iff eval.simps(1) imageI)
have rearangeExists :  "⋀ X F.((∃xs. length xs = Suc (Suc i) ∧
(∃(al, fl)∈set (dnf X). F al fl xs)) =
(∃(al,fl)∈set (dnf X).(∃xs. length xs = Suc (Suc i) ∧
F al fl xs)))"
by blast
have dropTheEnd : "⋀F Γ.(∃xs. length xs = Suc (Suc i) ∧ F (xs @ Γ)) = (∃x. (∃xs. length xs = i+1 ∧ F (xs @ x#Γ)))"
apply(safe)
subgoal for F Γ xs
apply(rule exI[where x="nth xs (i+1)"])
apply(rule exI[where x="take (i+1) xs"]) apply auto
by (metis Cons_nth_drop_Suc append.right_neutral append_Cons append_assoc append_eq_conv_conj append_self_conv2 append_take_drop_id lessI)
subgoal for F Γ x xs
apply(rule exI[where x="xs@[x]"])
by auto
done
have h2 : "⋀X Γ amount. amount≤ Suc i ⟹((∃xs. length xs = Suc (Suc i) ∧
(∃(al, fl)∈set (dnf X).
eval (superPicker amount i al fl) (xs @ Γ)))
= (∃xs. length xs = Suc (Suc i) ∧
(∃(al, fl)∈set (dnf X).
(∀a∈set al. aEval a (xs@Γ))∧(∀f∈set fl. eval f (xs@Γ)))))"
subgoal for X Γ amount
unfolding rearangeExists
apply(rule bex_cong)
apply simp
subgoal for x
apply (cases x)
apply simp
subgoal for al fl
unfolding dropTheEnd
unfolding dropTheEnd[of"λxs. (∀a∈set al. aEval a xs) ∧ (∀f∈set fl. eval f xs)"]
apply simp
unfolding ih[of amount al fl "_#Γ",symmetric]
unfolding eval_list_conj
apply(rule ex_cong1)
subgoal for xa
apply(rule ex_cong1)
subgoal for xab apply auto
by (meson Un_iff eval.simps(1) image_eqI)
done
done
done
done
done
have h3 : "⋀L F. (∃xs. length xs = Suc (Suc i) ∧ eval (step (Suc i) L F) (xs@Γ)) = (∃xs. length xs = Suc (Suc i) ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ))"
subgoal for L F
using pickedOneOfThem[OF h0]
using  qe_eq_repeat_eval'[of "Suc i" L F Γ] gen_qe_eval'[of "Suc i" L F Γ] luckyFind_eval'[of "Suc i" L F Γ]
by auto
done
have heurange : "var≤ Suc i" using rangeHeuristic[OF h0] by auto
show ?thesis
unfolding eval_list_disj
unfolding h1
unfolding h2[OF amountPred]
unfolding dnf_eval
unfolding opt'
unfolding h3
proof(safe)
fix xs
assume h : "length xs = Suc (Suc i)" "eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)"
have h3 : "var < length (xs @ Γ)"  using h heurange by auto
have h1: "(swap_list (Suc i) var (xs @ Γ)) = (swap_list (Suc i) var xs @ Γ)"
using h(1) heurange apply simp
have h2 : "Suc i < length (xs @ Γ)" using h by auto

show "∃xs. length xs = Suc (Suc i) ∧
eval (list_conj (map fm.Atom (map (swap_atom (Suc i) var) L) @ map (swap_fm (Suc i) var) F)) (xs @ Γ)"
apply(rule exI[where x="swap_list (Suc i) var xs"])
apply(auto simp add:h eval_list_conj simp del:swap_list.simps)
using swap_fm[OF h2 h3] swap_atom[OF h2 h3] unfolding h1
using h(2) unfolding eval_list_conj
apply auto

by (meson Un_iff eval.simps(1) imageI)
next
fix xs
assume h : "length xs = Suc (Suc i)""eval (list_conj (map fm.Atom (map (swap_atom (Suc i) var) L) @ map (swap_fm (Suc i) var) F)) (xs @ Γ)"
have h3 : "var < length (swap_list (Suc i) var xs @ Γ)"  using h heurange by auto
have h1: "swap_list (Suc i) var (swap_list (Suc i) var xs @ Γ) = xs @ Γ"
apply auto
using h(1) heurange
by (smt (z3) le_imp_less_Suc length_list_update lessI list_update_append list_update_id list_update_overwrite list_update_swap nth_append nth_list_update_eq)
have h2 : "Suc i < length (swap_list (Suc i) var xs @ Γ)" using h by auto
show "∃xs. length xs = Suc (Suc i) ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ)"
apply(rule exI[where x="swap_list (Suc i) var xs"])
unfolding swap_fm[OF h2 h3] swap_atom[OF h2 h3]
unfolding h1
using h(2) unfolding eval_list_conj
apply auto
apply (meson Un_iff eval.simps(1) imageI)
done
qed
qed
done
done
qed

lemma brownHueristic_less_than: "brownsHeuristic n L F = var ⟹ var≤ n"
apply simp
apply(cases "sorted_list_of_fset
((λx. case foldl
(λ(maxdeg, totaldeg, appearancecount) l.
let deg = MPoly_Type.degree (case l of Less p ⇒ p | Eq p ⇒ p | Leq p ⇒ p | Neq p ⇒ p) x
in (max maxdeg deg, totaldeg + deg, appearancecount + (if 0 < deg then 1 else 0)))
(0, 0, 0) L of
(a, b, c) ⇒ Quad (a, b, c, x)) |`|
fset_of_list [0..<n])")
apply auto
subgoal for a apply(cases a)
by auto
done
end
```