Theory Virtual_Substitution.HeuristicProofs

subsection "Heuristic Proofs"
theory HeuristicProofs
  imports VSQuad Heuristic OptimizationProofs
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)
        apply(auto simp add:eval_list_conj)
        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 (simp_all add:opt)
      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
      by (simp add: heuristic)
    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]) @ Γ)"
          by (simp add: length)
        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)
          apply(simp add :length)
          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
            by (simp add: list_update_append nth_append)
          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)
            apply(simp add: h)
            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"])
            apply(auto simp add:eval_list_conj simp del:swap_list.simps)
            apply(simp add: h)
            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