Theory Diophantine_Eqs_and_Ineqs

section ‹Linear Diophantine Equations and Inequalities›

text ‹We just represent equations and inequalities as polynomials, i.e., 
  ‹p = 0› or ‹p ≤ 0›. There is no need for strict inequalities ‹p < 0› 
  since for integers this is equivalent to ‹p + 1 ≤ 0›.›

theory Diophantine_Eqs_and_Ineqs
  imports Linear_Polynomial
begin

type_synonym 'v dleq = "(int,'v) lpoly"
type_synonym 'v dlineq = "(int,'v) lpoly"

definition satisfies_dleq :: "(int,'v) assign ⇒ 'v dleq ⇒ bool" where
  "satisfies_dleq α p = (eval_l α p = 0)" 

definition satisfies_dlineq :: "(int,'v) assign ⇒ 'v dlineq ⇒ bool" where
  "satisfies_dlineq α p = (eval_l α p ≤ 0)" 

abbreviation satisfies_eq_ineqs :: "(int,'v) assign ⇒ 'v dleq set ⇒ 'v dlineq set ⇒ bool" (‹_ ⊨⇩d⇩i⇩o '(_,_')›) where
  "satisfies_eq_ineqs α eqs ineqs ≡ Ball eqs (satisfies_dleq α) ∧ Ball ineqs (satisfies_dlineq α)" 
 
definition trivial_ineq :: "(int,'v :: linorder)lpoly ⇒ bool option" where
  "trivial_ineq c = (if vars_l_list c = [] then Some (constant_l c ≤ 0) else None)" 

lemma trivial_ineq_None: "trivial_ineq c = None ⟹ vars_l c ≠ {}" 
  unfolding trivial_ineq_def unfolding vars_l_list[symmetric] by fastforce

lemma trivial_ineq_Some: assumes "trivial_ineq c = Some b"
  shows "b = satisfies_dlineq α c" 
proof -
  from assms[unfolded trivial_ineq_def] have vars: "vars_l c = {}" and b: "b = (constant_l c ≤ 0)" 
    by (auto split: if_splits simp: vars_l_list_def)
  show ?thesis unfolding satisfies_dlineq_def eval_l_def vars using b by auto
qed

fun trivial_ineq_filter :: "'v :: linorder dlineq list ⇒ 'v dlineq list option" 
  where "trivial_ineq_filter [] = Some []" 
  | "trivial_ineq_filter (c # cs) = (case trivial_ineq c of Some True ⇒ trivial_ineq_filter cs
      | Some False ⇒ None
      | None ⇒ map_option ((#) c) (trivial_ineq_filter cs))" 

lemma trivial_ineq_filter: "trivial_ineq_filter cs = None ⟹ (∄ α. α ⊨⇩d⇩i⇩o ({}, set cs))" 
  "trivial_ineq_filter cs = Some ds ⟹ 
     Ball (set ds) (λ c. vars_l c ≠ {}) ∧ 
     (α ⊨⇩d⇩i⇩o ({}, set cs) ⟷ α ⊨⇩d⇩i⇩o ({}, set ds)) ∧ 
     length ds ≤ length cs" 
proof (atomize(full), induct cs arbitrary: ds)
  case IH: (Cons c cs)
  let ?t = "trivial_ineq c" 
  consider (T) "?t = Some True" | (F) "?t = Some False" | (V) "?t = None" by (cases ?t, auto)
  thus ?case
  proof cases
    case F
    from trivial_ineq_Some[OF F] F show ?thesis by auto
  next
    case T
    from trivial_ineq_Some[OF T] T IH show ?thesis by force
  next
    case V
    from trivial_ineq_None[OF V] V IH show ?thesis by auto
  qed
qed simp

lemma trivial_lhe: assumes "vars_l p = {}" 
  shows "eval_l α p = constant_l p"  
    "satisfies_dleq α p ⟷ p = 0" 
proof -
  show id: "eval_l α p = constant_l p" 
    by (subst eval_l_mono[of "{}"], insert assms, auto)
  show "satisfies_dleq α p ⟷ p = 0" 
    unfolding satisfies_dleq_def id using assms
    apply (transfer)
    by (metis (mono_tags, lifting) Collect_empty_eq not_None_eq)
qed


end