# Theory CertLin

Up to index of Isabelle/HOL/LinearQuantifierElim

theory CertLin
imports LinArith
(*  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

begin

fun plus_atom :: "atom => atom => atom" where
"(Eq r1 cs1) + (Eq r2 cs2) = Eq (r1+r2) (cs1+cs2)" |
"(Eq r1 cs1) + (Less r2 cs2) = Less (r1+r2) (cs1+cs2)" |
"(Less r1 cs1) + (Eq r2 cs2) = Less (r1+r2) (cs1+cs2)" |
"(Less r1 cs1) + (Less r2 cs2) = Less (r1+r2) (cs1+cs2)"

definition
"0 = Eq 0 []"

instance
apply intro_classes
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: "IR a xs ==> IR b xs ==> IR(a+b) xs"
apply(case_tac a)
apply(case_tac b)
apply(case_tac b)
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 "\<odot>a" 70)
where "cs \<odot>a as = (∑(c,a) \<leftarrow> zip cs as. c *a a)"

lemma iprod_a_Nil2[simp]: "cs \<odot>a [] = 0"

lemma [simp]: "(c#cs) \<odot>a (a#as) = (c *a a) + cs \<odot>a as"

definition contradict :: "atom list => real list => bool" where
"contradict as cs <-> size cs = size as ∧ (∀c∈set cs. c≥0) ∧
(case cs \<odot>a as of Eq r cs => r ≠ 0 ∧ (∀c∈set cs. c=0)
| Less r cs => r ≥ 0 ∧ (∀c∈set cs. c=0))"

definition

lemma refute_I:
"~ Logic.interpret h (Neg f) e ==> Logic.interpret h f e"
by simp

lemma I_R_mult_atom: "c ≥ 0 ==> IR a xs ==> IR (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). IR (c *a a) xs
==> IR (cs \<odot>a as) xs"

apply(induct cs as rule:list_induct2)
done

"contradict as cs ==> ∃a∈set as. ¬ IR a xs"
proof -
have "¬ IR (cs \<odot>a as) xs"
proof (cases "cs \<odot>a as")
case Less thus ?thesis using `contradict as cs`
next
case Eq thus ?thesis using `contradict as cs`
qed
thus ?thesis using `contradict as cs`
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)