Theory ArchComp

(*  Author:  Tobias Nipkow  *)

section "Comparing Enumeration and Archive"

theory ArchComp
imports "Flyspeck-Tame.ArchCompProps" "HOL-Library.Code_Target_Numeral"
begin

subsection ‹Proofs by evaluation using generated code›

lemma pre_iso_test3: "∀g ∈ set Tri. pre_iso_test g"
by eval

lemma pre_iso_test4: "∀g ∈ set Quad. pre_iso_test g"
by eval

lemma pre_iso_test5: "∀g ∈ set Pent. pre_iso_test g"
by eval

lemma pre_iso_test6: "∀g ∈ set Hex. pre_iso_test g"
by eval

lemma same3: "samet (tameEnumFilter 0) Tri"
by eval

lemma same4: "samet (tameEnumFilter 1) Quad"
by eval

lemma same5: "samet (tameEnumFilter 2) Pent"
by eval

lemma same6: "samet (tameEnumFilter 3) Hex"
by eval

end