Theory CertLin

(*  Author:     Tobias Nipkow, 2007

A simple certificate checker for q-free linear arithmetic:
is linear combination of atoms and certificate contradictory?
*)

theory CertLin
imports LinArith
begin

declare list_add_assoc [simp]

instantiation atom :: monoid_add
begin

fun plus_atom :: "atom ⇒ atom ⇒ atom" where
  "(Eq r⇩1 cs⇩1) + (Eq r⇩2 cs⇩2) = Eq (r⇩1+r⇩2) (cs⇩1+cs⇩2)" |
  "(Eq r⇩1 cs⇩1) + (Less r⇩2 cs⇩2) = Less (r⇩1+r⇩2) (cs⇩1+cs⇩2)" |
  "(Less r⇩1 cs⇩1) + (Eq r⇩2 cs⇩2) = Less (r⇩1+r⇩2) (cs⇩1+cs⇩2)" |
  "(Less r⇩1 cs⇩1) + (Less r⇩2 cs⇩2) = Less (r⇩1+r⇩2) (cs⇩1+cs⇩2)"

definition
  "0 = Eq 0 []"

instance
apply intro_classes
apply(simp_all add: zero_atom_def)
apply(case_tac a)
apply(case_tac b)
apply(case_tac c)
apply simp_all
apply(case_tac c)
apply simp_all
apply(case_tac b)
apply(case_tac c)
apply simp_all
apply(case_tac c)
apply simp_all
apply(case_tac a)
apply simp_all
apply(case_tac a)
apply simp_all
done

end

lemma I_R_additive: "I⇩R a xs ⟹ I⇩R b xs ⟹ I⇩R(a+b) xs"
apply(case_tac a)
apply(case_tac b)
apply (simp_all add:iprod_left_add_distrib)
apply(case_tac b)
apply (simp_all add:iprod_left_add_distrib)
done

fun mult_atom :: "real ⇒ atom ⇒ atom" (infix ‹*⇩a› 70) where
"c *⇩a Eq r cs = Eq (c*r) (c *⇩s cs)" |
"c *⇩a Less r cs = (if c=0 then Eq 0 [] else Less (c*r) (c *⇩s cs))"

definition iprod_a :: "real list ⇒ atom list ⇒ atom" (infix ‹⊙⇩a› 70)
where "cs ⊙⇩a as = (∑(c,a) ← zip cs as. c *⇩a a)"

lemma iprod_a_Nil2[simp]: "cs ⊙⇩a [] = 0"
by(simp add:iprod_a_def)

lemma [simp]: "(c#cs) ⊙⇩a (a#as) = (c *⇩a a) + cs ⊙⇩a as"
by(simp add:iprod_a_def)

definition contradict :: "atom list ⇒ real list ⇒ bool" where
"contradict as cs ⟷ size cs = size as ∧ (∀c∈set cs. c≥0) ∧
  (case cs ⊙⇩a as of Eq r cs ⇒ r ≠ 0 ∧ (∀c∈set cs. c=0)
                  | Less r cs ⇒ r ≥ 0 ∧ (∀c∈set cs. c=0))"

definition
"contradict_dnf ass = (∃css. list_all2 contradict ass css)"

lemma refute_I:
  "¬ Logic.interpret h (Neg f) e ⟹ Logic.interpret h f e"
by simp

lemma I_R_mult_atom: "c ≥ 0 ⟹ I⇩R a xs ⟹ I⇩R (c *⇩a a) xs"
apply(cases a)
 apply(clarsimp)
apply(simp)
done

lemma I_R_iprod_a:
 "size cs = size as ⟹ ∀(c,a) ∈ set(zip cs as). I⇩R (c *⇩a a) xs
 ⟹ I⇩R (cs ⊙⇩a as) xs"
apply(induct cs as rule:list_induct2)
 apply (simp add:zero_atom_def)
apply(simp add:I_R_additive)
done

lemma contradictD:
 "contradict as cs ⟹ ∃a∈set as. ¬ I⇩R a xs"
proof -
  assume "contradict as cs"
  have "¬ I⇩R (cs ⊙⇩a as) xs"
  proof (cases "cs ⊙⇩a as")
    case Less thus ?thesis using ‹contradict as cs›
      by(simp add:contradict_def iprod0_if_coeffs0)
  next
    case Eq thus ?thesis using ‹contradict as cs›
      by(simp add:contradict_def iprod0_if_coeffs0)
  qed
  thus ?thesis using ‹contradict as cs›
    by(force simp add:contradict_def intro: I_R_iprod_a I_R_mult_atom
             elim:in_set_zipE)
qed

lemma cyclic_dnfD: "qfree f ⟹ contradict_dnf (dnf(R.nnf f)) ⟹ ¬R.I f xs"
apply(subst R.I_nnf[symmetric])
apply(subst R.I_dnf[symmetric])
apply(erule R.nqfree_nnf)
apply(auto simp add:contradict_dnf_def list_all2_iff in_set_conv_nth)
apply(drule_tac x="(dnf(R.nnf f) ! i, css!i)" in bspec)
apply (auto simp:set_zip)
apply(drule_tac xs=xs in contradictD)
apply auto
done

end