Lines Matching refs:interpret
357 (interpret f [] = T) /\
358 (interpret f (c::cs) = interpret_clause f c /\ interpret f cs)
364 ``!cs. MEM [] cs ==> ~interpret f cs``,
377 ``!cs v b. (f v = b) /\ interpret f cs ==>
378 interpret f (rewrite v b cs)``,
383 ``(find_uprop cs = SOME (q,r)) ==> ~interpret f (rewrite q (~r) cs)``,
396 ``!cs f. (dpll cs = NONE) ==> (interpret f cs = F)``,
409 `~interpret f (rewrite q (~r) cs)` by METIS_TAC [interpret_uprop] THEN
437 val th1 = SIMP_CONV (srw_ss()) [] ``interpret ^f ^clauses``