Theory FOR_Preliminaries

section‹Preliminaries›
text‹This theory contains some auxiliary results previously located in Auxx.Util of IsaFoR.›
theory FOR_Preliminaries
  imports
    Polynomial_Factorization.Missing_List 
    First_Order_Terms.Fun_More
begin

lemma finite_imp_eq [simp]:
  "finite {x. P x ⟶ Q x} ⟷ finite {x. ¬ P x} ∧ finite {x. Q x}"
  by (auto simp: Collect_imp_eq Collect_neg_eq)

definition const :: "'a ⇒ 'b ⇒ 'a" where
  "const ≡ (λx y. x)"

definition flip :: "('a ⇒ 'b ⇒ 'c) ⇒ ('b ⇒ 'a ⇒ 'c)" where
  "flip f ≡ (λx y. f y x)"
declare flip_def[simp]

lemma const_apply[simp]: "const x y = x"
  by (simp add: const_def)

lemma foldr_Cons_append_conv [simp]:
  "foldr (#) xs ys = xs @ ys"
  by (induct xs) simp_all

lemma foldl_flip_Cons[simp]:
  "foldl (flip (#)) xs ys = rev ys @ xs"
  by (induct ys arbitrary: xs) simp_all

text ‹already present as @{thm [source] foldr_conv_foldl}, but
  direction seems odd›
lemma foldr_flip_rev[simp]:
  "foldr (flip f) (rev xs) a = foldl f a xs"
  by (simp add: foldr_conv_foldl)

text ‹already present as @{thm [source] foldl_conv_foldr}, but
  direction seems odd›
lemma foldl_flip_rev[simp]:
  "foldl (flip f) a (rev xs) = foldr f xs a"
  by (simp add: foldl_conv_foldr)

fun debug :: "(String.literal ⇒ String.literal) ⇒ String.literal ⇒ 'a ⇒ 'a" where "debug i t x = x"


end