Documentation

Std.Tactic.BVDecide.Normalize.Bool

This module contains the Bool simplifying part of the bv_normalize simp set.

theorem Std.Tactic.BVDecide.Normalize.if_eq_cond {α : Sort u_1} {b : Bool} {x y : α} :
(if b = true then x else y) = bif b then x else y
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_same_then (c t e : Bool) :
((bif c then t else e) == t) = (c || t == e)
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_same_then' (c t e : Bool) :
(t == bif c then t else e) = (c || t == e)
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_same_else (c t e : Bool) :
((bif c then t else e) == e) = (!c || t == e)
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_same_else' (c t e : Bool) :
(e == bif c then t else e) = (!c || t == e)
theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_same_then {w : Nat} (c : Bool) (t e : BitVec w) :
((bif c then t else e) == t) = (c || t == e)
theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_same_then' {w : Nat} (c : Bool) (t e : BitVec w) :
(t == bif c then t else e) = (c || t == e)
theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_same_else {w : Nat} (c : Bool) (t e : BitVec w) :
((bif c then t else e) == e) = (!c || t == e)
theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_same_else' {w : Nat} (c : Bool) (t e : BitVec w) :
(e == bif c then t else e) = (!c || t == e)
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_then_ite {α : Sort u_1} (cond : Bool) {a b c : α} :
(bif cond then bif cond then a else b else c) = bif cond then a else c
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_then_not_ite (cond : Bool) {a b c : Bool} :
(bif cond then !bif cond then a else b else c) = bif cond then !a else c
theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_then_not_ite {w : Nat} (cond : Bool) {a b c : BitVec w} :
(bif cond then ~~~bif cond then a else b else c) = bif cond then ~~~a else c
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_else_ite {α : Sort u_1} (cond : Bool) {a b c : α} :
(bif cond then a else bif cond then b else c) = bif cond then a else c
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_else_not_ite (cond : Bool) {a b c : Bool} :
(bif cond then a else !bif cond then b else c) = bif cond then a else !c
theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_else_not_ite {w : Nat} (cond : Bool) {a b c : BitVec w} :
(bif cond then a else ~~~bif cond then b else c) = bif cond then a else ~~~c
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_then_ite' {α : Sort u_1} (c0 c1 : Bool) {a b : α} :
(bif c0 then bif c1 then a else b else a) = bif c0 && !c1 then b else a
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_then_not_ite' (c0 c1 : Bool) {a b : Bool} :
(bif c0 then !bif c1 then !a else b else a) = bif c0 && !c1 then !b else a
theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_then_not_ite' {w : Nat} (c0 c1 : Bool) {a b : BitVec w} :
(bif c0 then ~~~bif c1 then ~~~a else b else a) = bif c0 && !c1 then ~~~b else a
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_else_ite' {α : Sort u_1} (c0 c1 : Bool) {a b : α} :
(bif c0 then a else bif c1 then a else b) = bif !c0 && !c1 then b else a
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_else_not_ite' (c0 c1 : Bool) {a b : Bool} :
(bif c0 then a else !bif c1 then !a else b) = bif !c0 && !c1 then !b else a
theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_else_not_ite' {w : Nat} (c0 c1 : Bool) {a b : BitVec w} :
(bif c0 then a else ~~~bif c1 then ~~~a else b) = bif !c0 && !c1 then ~~~b else a
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_then_ite'' {α : Sort u_1} (c0 c1 : Bool) {a b : α} :
(bif c0 then bif c1 then b else a else a) = bif c0 && c1 then b else a
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_then_not_ite'' (c0 c1 : Bool) {a b : Bool} :
(bif c0 then !bif c1 then b else !a else a) = bif c0 && c1 then !b else a
theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_then_not_ite'' {w : Nat} (c0 c1 : Bool) {a b : BitVec w} :
(bif c0 then ~~~bif c1 then b else ~~~a else a) = bif c0 && c1 then ~~~b else a
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_else_ite'' {α : Sort u_1} (c0 c1 : Bool) {a b : α} :
(bif c0 then a else bif c1 then b else a) = bif !c0 && c1 then b else a
theorem Std.Tactic.BVDecide.Normalize.Bool.ite_else_not_ite'' (c0 c1 : Bool) {a b : Bool} :
(bif c0 then a else !bif c1 then b else !a) = bif !c0 && c1 then !b else a
theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_else_not_ite'' {w : Nat} (c0 c1 : Bool) {a b : BitVec w} :
(bif c0 then a else ~~~bif c1 then b else ~~~a) = bif !c0 && c1 then ~~~b else a
theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_ite_zero {w : Nat} {c : Bool} {a e : BitVec w} :
(a * bif c then 0#w else e) = bif c then 0#w else a * e
theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_ite_zero' {w : Nat} {c : Bool} {a t : BitVec w} :
(a * bif c then t else 0#w) = bif c then a * t else 0#w
theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_ite_zero'' {w : Nat} {c : Bool} {a e : BitVec w} :
(bif c then 0#w else e) * a = bif c then 0#w else e * a
theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_ite_zero''' {w : Nat} {c : Bool} {a t : BitVec w} :
(bif c then t else 0#w) * a = bif c then t * a else 0#w
theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_one_eq_ite {b : Bool} {a : BitVec 1} :
((a == 1#1) == b) = (a == bif b then 1#1 else 0#1)
theorem Std.Tactic.BVDecide.Normalize.BitVec.one_beq_eq_ite {b : Bool} {a : BitVec 1} :
((1#1 == a) == b) = (a == bif b then 1#1 else 0#1)
theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_one_eq_ite' {b : Bool} {a : BitVec 1} :
(b == (a == 1#1)) = (a == bif b then 1#1 else 0#1)
theorem Std.Tactic.BVDecide.Normalize.BitVec.one_beq_eq_ite' {b : Bool} {a : BitVec 1} :
(b == (1#1 == a)) = (a == bif b then 1#1 else 0#1)
theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_zero_eq_ite {b : Bool} {a : BitVec 1} :
((a == 0#1) == b) = (a == bif b then 0#1 else 1#1)
theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_beq_eq_ite {b : Bool} {a : BitVec 1} :
((0#1 == a) == b) = (a == bif b then 0#1 else 1#1)
theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_zero_eq_ite' {b : Bool} {a : BitVec 1} :
(b == (a == 0#1)) = (a == bif b then 0#1 else 1#1)
theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_beq_eq_ite' {b : Bool} {a : BitVec 1} :
(b == (0#1 == a)) = (a == bif b then 0#1 else 1#1)
theorem Std.Tactic.BVDecide.Normalize.Bool.beq_not_ite {a b c : Bool} :
(a == !bif c then a else b) = (!c && a == !b)
theorem Std.Tactic.BVDecide.Normalize.Bool.beq_not_ite' {a b c : Bool} :
(a == !bif c then b else a) = (c && a == !b)
theorem Std.Tactic.BVDecide.Normalize.Bool.not_ite_beq {a b c : Bool} :
((!bif c then a else b) == a) = (!c && a == !b)
theorem Std.Tactic.BVDecide.Normalize.Bool.not_ite_beq' {a b c : Bool} :
((!bif c then b else a) == a) = (c && a == !b)
theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_not_ite {w : Nat} {a b : BitVec (w + 1)} {c : Bool} :
(a == ~~~bif c then a else b) = (!c && a == ~~~b)
theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_not_ite' {w : Nat} {a b : BitVec (w + 1)} {c : Bool} :
(a == ~~~bif c then b else a) = (c && a == ~~~b)
theorem Std.Tactic.BVDecide.Normalize.BitVec.not_ite_beq {w : Nat} {a b : BitVec (w + 1)} {c : Bool} :
((~~~bif c then a else b) == a) = (!c && ~~~b == a)
theorem Std.Tactic.BVDecide.Normalize.BitVec.not_ite_beq' {w : Nat} {a b : BitVec (w + 1)} {c : Bool} :
((~~~bif c then b else a) == a) = (c && ~~~b == a)
theorem Std.Tactic.BVDecide.Normalize.Bool.and_left (lhs rhs : Bool) (h : (lhs && rhs) = true) :
lhs = true
theorem Std.Tactic.BVDecide.Normalize.Bool.and_right (lhs rhs : Bool) (h : (lhs && rhs) = true) :
rhs = true