theory CertLin
imports LinArith
begin
declare list_add_assoc [simp]
instantiation atom :: monoid_add
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(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: "IR a xs ==> IR b xs ==> IR(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 "\<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"
by(simp add:iprod_a_def)
lemma [simp]: "(c#cs) \<odot>a (a#as) = (c *a a) + cs \<odot>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 \<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
"contradict_dnf ass = (EX 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 ==> IR a xs ==> IR (c *a a) xs"
apply(cases a)
apply(clarsimp)
apply(rule real_mult_less_mono2)
apply arith
apply simp
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)
apply (simp add:zero_atom_def)
apply(simp add:I_R_additive)
done
lemma contradictD:
"contradict as cs ==> ∃a∈set as. ¬ IR a xs"
proof -
assume "contradict as cs"
have "¬ IR (cs \<odot>a as) xs"
proof (cases "cs \<odot>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_def 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