# Theory ExportProofs

```subsection "Top-Level Algorithm Proofs"
theory ExportProofs
imports HeuristicProofs Exports
(*"HOL-Library.Code_Real_Approx_By_Float"*)
HOL.String "HOL-Library.Code_Target_Int" "HOL-Library.Code_Target_Nat" PrettyPrinting Show.Show_Real
begin

theorem "eval (Unpower f) L = eval f L" unfolding unpower_eval Unpower_def by auto

theorem VSLuckiest: "∀xs. eval (VSLuckiest φ) xs = eval φ xs"
unfolding VSLuckiest_def Unpower_def opt_def
using QE_dnf_eval[OF luckiestFind_eval' opt_no_group] opt_no_group
by fastforce

theorem VSLuckiestBlocks : "∀xs. eval (VSLuckiestBlocks φ) xs = eval φ xs"
unfolding VSLuckiestBlocks_def Unpower_def opt_group_def
using QE_dnf'_eval[OF the_real_step_augment[OF luckiestFind_eval, of "λx _ _. x"] opt]
using opt
by fastforce

theorem VSEquality : "∀xs. eval (VSEquality φ) xs = eval φ xs"
unfolding VSEquality_def Unpower_def opt_def
using QE_dnf_eval[OF qe_eq_repeat_eval' opt_no_group]
using  opt_no_group VSLuckiest
by fastforce

theorem VSEqualityBlocks : "∀xs. eval (VSEqualityBlocks φ) xs = eval φ xs"
unfolding VSEqualityBlocks_def Unpower_def opt_group_def
using QE_dnf'_eval[OF the_real_step_augment[OF qe_eq_repeat_eval, of "λx _ _. x"] opt]
using opt VSLuckiestBlocks
by fastforce

theorem VSGeneralBlocks : "∀xs. eval (VSGeneralBlocks φ) xs = eval φ xs"
unfolding VSGeneralBlocks_def Unpower_def opt_group_def
using QE_dnf'_eval[OF the_real_step_augment[OF gen_qe_eval, of "λx _ _. x"] opt]
using opt VSLuckiestBlocks
by fastforce

theorem VSLuckyBlocks : "∀xs. eval (VSLuckyBlocks φ) xs = eval φ xs"
unfolding VSLuckyBlocks_def Unpower_def opt_group_def
using QE_dnf'_eval[OF the_real_step_augment[OF luckyFind'_eval, of "λx _ _. x"] opt]
using opt VSLuckiestBlocks
by fastforce

theorem VSLEGBlocks : "∀xs. eval (VSLEGBlocks φ) xs = eval φ xs"
unfolding VSLEGBlocks_def opt_group_def
using VSEqualityBlocks VSGeneralBlocks VSLuckyBlocks
by fastforce

theorem VSEqualityBlocksLimited : "∀xs. eval (VSEqualityBlocksLimited φ) xs = eval φ xs"
unfolding VSEqualityBlocksLimited_def Unpower_def opt_group_def
using QE_dnf_eval[OF qe_eq_repeat_eval_augment opt] opt VSLuckiestBlocks
by fastforce

theorem VSEquality_3_times : "∀xs. eval (VSEquality_3_times φ) xs = eval φ xs"
using VSEquality unfolding VSEquality_3_times_def by auto

theorem VSGeneral:  "∀xs. eval (VSGeneral φ) xs = eval φ xs"
unfolding VSGeneral_def Unpower_def Unpower_def opt_def
using QE_dnf_eval[OF gen_qe_eval' opt_no_group]
using  opt_no_group VSLuckiest
by fastforce

theorem VSGeneralBlocksLimited:  "∀xs. eval (VSGeneralBlocksLimited φ) xs = eval φ xs"
unfolding VSGeneralBlocksLimited_def Unpower_def opt_group_def
using QE_dnf_eval[OF gen_qe_eval_augment opt] opt VSLuckiestBlocks
by fastforce

theorem VSBrowns:  "∀xs. eval (VSBrowns φ) xs = eval φ xs"
unfolding VSBrowns_def Unpower_def opt_group_def
using QE_dnf_eval[OF step_augmenter_eval[of gen_qe brownsHeuristic, OF gen_qe_eval brownHueristic_less_than] opt] opt VSLuckiestBlocks
by fastforce

theorem VSGeneral_3_times : "∀xs. eval (VSGeneral_3_times φ) xs = eval φ xs"
unfolding  VSGeneral_3_times_def  using VSGeneral
by auto

theorem VSLucky: "∀xs. eval (VSLucky φ) xs = eval φ xs"
unfolding VSLucky_def Unpower_def opt_def
using QE_dnf_eval[OF luckyFind_eval' opt_no_group] opt_no_group VSLuckiest
by fastforce

theorem VSLuckyBlocksLimited: "∀xs. eval (VSLuckyBlocksLimited φ) xs = eval φ xs"
unfolding VSLuckyBlocksLimited_def Unpower_def opt_group_def
using QE_dnf_eval[OF luckyFind_eval_augment opt] opt VSLuckiestBlocks
by fastforce

theorem VSLEG: "∀xs. eval (VSLEG φ) xs = eval φ xs"
unfolding VSLEG_def
using VSLucky VSEquality VSGeneral by auto

theorem VSHeuristic : "∀xs. eval(VSHeuristic φ) xs = eval φ xs"
unfolding VSHeuristic_def Unpower_def opt_group_def
using QE_dnf_eval[OF superPicker_eval opt] opt VSLuckiestBlocks
by fastforce

theorem VSLuckiestRepeat : "∀xs. eval (VSLuckiestRepeat φ) xs = eval φ xs"
unfolding VSLuckiestRepeat_def using repeatAmountOfQuantifiers_eval[OF] using VSLuckiest
by blast

export_code
print_mpoly
VSGeneral VSEquality VSLucky VSLEG VSLuckiest
VSGeneralBlocksLimited VSEqualityBlocksLimited VSLuckyBlocksLimited
VSGeneralBlocks VSEqualityBlocks VSLuckyBlocks VSLEGBlocks VSLuckiestBlocks
QE_dnf
gen_qe qe_eq_repeat
simpfm push_forall nnf Unpower
is_quantifier_free is_solved
add mult C V pow minus
Eq Or is_quantifier_free

real_of_int real_mult real_div real_plus real_minus

VSGeneral_3_times VSEquality_3_times VSHeuristic VSLuckiestRepeat VSBrowns
in SML module_name VS

end```