# Structure QbfConv

signature QbfConv = sig
type conv = Abbrev.conv
(* put an arbitrary QBF into the required form *)
(* specifically,
input term:
- has type bool
- is closed
- contains only:
- first order connectives (/\,\/,==>,~)
(TODO: allow equality?)
- quantifiers (!,?)
- variables
output term:
- of the form Q_1 x_1. ... Q_n x_n. phi
- each Q_i is either ! or ?
- Q_n is ?
- each x_i appears in phi
- phi is closed and in CNF
alternatively, the output term might simply be 'T' or 'F'
*)
val qbf_prenex_conv : conv
(* simplifies clauses (specialisation of SIMP_CONV). In particular, does the following rewrites:
(∀x. x ∨ P) = P, (∀x. ¬x ∨ P) = P, (∀x. x) = F, (∀x. ¬x) = F, (UOK)
and associativity/commutativity normalisation for conjunction and disjunction *)
val simp_clauses : conv
(* conversion that takes [!x:bool. t] where t is in CNF and may contain x and
removes the quantifier and all occurrences of x. also simplifies clauses (as above). *)
val remove_forall : conv
(* [last_quant_conv c] strips a quantifier (! and ? only) prefix down
to the last quantifier then applies c to the (singly quantified) body *)
val last_quant_conv : conv -> conv
(* applies a conversion under a quantifier prefix of foralls and exists *)
val strip_prefix_conv : conv -> conv
(* [last_quant_seq_conv cq cb] applies cb under the quantifier prefix and
then cq before each quantifier. That is:
Q1 x1. Q2 x2. ... Qn xn. P --> cq (Q1 x1. cq (Q2 x2. ... cq (Qn. xn. cb P))))
*)
val last_quant_seq_conv : conv -> conv -> conv
(* applies cb under the quantifier prefix, and then, if the innermost
quantifiers are all universal, applies cq before each of them *)
val last_forall_seq_conv : conv -> conv -> conv
end

*HOL 4, Kananaskis-13*