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)" |
"cyclerec i j fs = 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 simp
lemma cyclerecD: fixes xs :: "'a :: dlo list" shows
"[| cyclerec i j as; xs!i < xs!j|] ==> ∃a∈set as. ¬ Idlo a xs"
apply(induct as arbitrary: j)
apply (simp)
apply(case_tac a)
apply(auto split:split_if_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 fastsimp
apply fastsimp
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_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 auto
done
end