66 fun simplify_prop (@{const Not} $ t) = s_not (simplify_prop t) |
66 fun simplify_prop (@{const Not} $ t) = s_not (simplify_prop t) |
67 | simplify_prop (@{const conj} $ t $ u) = s_conj (simplify_prop t, simplify_prop u) |
67 | simplify_prop (@{const conj} $ t $ u) = s_conj (simplify_prop t, simplify_prop u) |
68 | simplify_prop (@{const disj} $ t $ u) = s_disj (simplify_prop t, simplify_prop u) |
68 | simplify_prop (@{const disj} $ t $ u) = s_disj (simplify_prop t, simplify_prop u) |
69 | simplify_prop (@{const implies} $ t $ u) = s_imp (simplify_prop t, simplify_prop u) |
69 | simplify_prop (@{const implies} $ t $ u) = s_imp (simplify_prop t, simplify_prop u) |
70 | simplify_prop (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_prop t, simplify_prop u) |
70 | simplify_prop (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_prop t, simplify_prop u) |
|
71 | simplify_prop (t as Const (@{const_name HOL.eq}, _) $ u $ v) = |
|
72 if u aconv v then @{const True} else t |
71 | simplify_prop (t $ u) = simplify_prop t $ simplify_prop u |
73 | simplify_prop (t $ u) = simplify_prop t $ simplify_prop u |
72 | simplify_prop (Abs (s, T, t)) = Abs (s, T, simplify_prop t) |
74 | simplify_prop (Abs (s, T, t)) = Abs (s, T, simplify_prop t) |
73 | simplify_prop t = t |
75 | simplify_prop t = t |
74 |
76 |
75 fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps) |
77 fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps) |