# Theory CertDlo

Up to index of Isabelle/HOL/LinearQuantifierElim

theory CertDlo
imports QEdlo
`(*  Author:     Tobias Nipkow, 2007A simple certificate based checker for q-free dlo formulae.Certificate is cycle.*)theory CertDloimports QEdlobeginfun cyclerec :: "nat => nat => atom list => bool" where"cyclerec i j [] = (i=j)" |"cyclerec i j (Less m n # fs) = (j=m & cyclerec i n fs)" |"cyclerec i j (Eq m n # fs) = (if j=m then cyclerec i n fs                               else if j=n then cyclerec i m fs else False)"definition cycle :: "atom list => nat list => bool" where"cycle fs is = ((∀i∈set is. i < length fs) ∧  (case map (nth fs) is of Less i j # fs' => cyclerec i j fs' | _ => False))"definition"cyclic_dnf ass = (EX iss. list_all2 cycle ass iss)"lemma refute_I:  "~ Logic.interpret h (Neg f) e ==> Logic.interpret h f e"by simplemma cyclerecD: fixes xs :: "'a :: dlo list" shows "[| cyclerec i j as; xs!i < xs!j|] ==> ∃a∈set as. ¬ I⇣d⇣l⇣o a xs"apply(induct as arbitrary: j) apply (simp)apply(case_tac a)apply(auto split:split_if_asm)donelemma cycleD: fixes xs :: "'a :: dlo list" shows "cycle as is ==> ¬ DLO.I (list_conj (map Atom as)) xs"apply ruleapply (simp add:cycle_def map_eq_Cons_conv split:list.splits atom.splits)apply autoapply(drule_tac xs = xs in cyclerecD)apply(drule_tac x = "as!z" in bspec)apply (erule nth_mem)apply fastforceapply fastforcedonelemma cyclic_dnfD: "qfree f ==> cyclic_dnf (dnf(DLO.nnf f)) ==> ~DLO.I f xs"apply(subst DLO.I_nnf[unfolded nnf_def, symmetric])apply(subst DLO.I_dnf[symmetric])apply(erule DLO.nqfree_nnf[unfolded nnf_def])apply(auto simp add:cyclic_dnf_def list_all2_def in_set_conv_nth)apply(drule_tac x="(dnf(DLO.nnf f) ! i, iss!i)" in bspec)apply (auto simp:set_zip)apply(drule_tac xs=xs in cycleD)apply autodoneend`