Theory CertDlo

(*  Author:     Tobias Nipkow, 2007

A simple certificate based checker for q-free dlo formulae.
Certificate is cycle.
*)

theory CertDlo
imports QEdlo
begin

fun 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 = (∃iss. list_all2 cycle ass iss)"

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

lemma 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:if_split_asm)
done

lemma cycleD: fixes xs :: "'a :: dlo list" shows
 "cycle as is ⟹ ¬ DLO.I (list_conj (map Atom as)) xs"
apply rule
apply (simp add:cycle_def map_eq_Cons_conv split:list.splits atom.splits)
apply auto
apply(drule_tac xs = xs in cyclerecD)
apply(drule_tac x = "as!z" in bspec)
apply (erule nth_mem)
apply fastforce
apply fastforce
done

lemma 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_iff 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 auto
done

end