285 | s_not (@{const True}) = @{const False} |
285 | s_not (@{const True}) = @{const False} |
286 | s_not (@{const Not} $ t) = t |
286 | s_not (@{const Not} $ t) = t |
287 | s_not t = @{const Not} $ t |
287 | s_not t = @{const Not} $ t |
288 fun s_conj (@{const True}, t2) = t2 |
288 fun s_conj (@{const True}, t2) = t2 |
289 | s_conj (t1, @{const True}) = t1 |
289 | s_conj (t1, @{const True}) = t1 |
|
290 | s_conj (@{const False}, _) = @{const False} |
|
291 | s_conj (_, @{const False}) = @{const False} |
290 | s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2) |
292 | s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2) |
291 fun s_disj (@{const False}, t2) = t2 |
293 fun s_disj (@{const False}, t2) = t2 |
292 | s_disj (t1, @{const False}) = t1 |
294 | s_disj (t1, @{const False}) = t1 |
|
295 | s_disj (@{const True}, _) = @{const True} |
|
296 | s_disj (_, @{const True}) = @{const True} |
293 | s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2) |
297 | s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2) |
294 fun s_imp (@{const True}, t2) = t2 |
298 fun s_imp (@{const True}, t2) = t2 |
295 | s_imp (t1, @{const False}) = s_not t1 |
299 | s_imp (t1, @{const False}) = s_not t1 |
|
300 | s_imp (@{const False}, _) = @{const True} |
|
301 | s_imp (_, @{const True}) = @{const True} |
296 | s_imp p = HOLogic.mk_imp p |
302 | s_imp p = HOLogic.mk_imp p |
297 fun s_iff (@{const True}, t2) = t2 |
303 fun s_iff (@{const True}, t2) = t2 |
298 | s_iff (t1, @{const True}) = t1 |
304 | s_iff (t1, @{const True}) = t1 |
|
305 | s_iff (@{const False}, t2) = s_not t2 |
|
306 | s_iff (t1, @{const False}) = s_not t1 |
299 | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2 |
307 | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2 |
300 |
308 |
301 (* cf. "close_form" in "refute.ML" *) |
309 (* cf. "close_form" in "refute.ML" *) |
302 fun close_form t = |
310 fun close_form t = |
303 fold (fn ((s, i), T) => fn t' => |
311 fold (fn ((s, i), T) => fn t' => |