equal
deleted
inserted
replaced
221 in SOME thm |
221 in SOME thm |
222 end handle Option => NONE) |
222 end handle Option => NONE) |
223 |
223 |
224 fun distinctTree_tac ctxt |
224 fun distinctTree_tac ctxt |
225 (Const (@{const_name Trueprop},_) $ |
225 (Const (@{const_name Trueprop},_) $ |
226 (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) = |
226 (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ (x as Free _)$ (y as Free _))), i) = |
227 (case (neq_x_y ctxt x y) of |
227 (case (neq_x_y ctxt x y) of |
228 SOME neq => rtac neq i |
228 SOME neq => rtac neq i |
229 | NONE => no_tac) |
229 | NONE => no_tac) |
230 | distinctTree_tac _ _ = no_tac; |
230 | distinctTree_tac _ _ = no_tac; |
231 |
231 |
234 SOME ctxt => SUBGOAL (distinctTree_tac ctxt) |
234 SOME ctxt => SUBGOAL (distinctTree_tac ctxt) |
235 | NONE => fn i => no_tac) |
235 | NONE => fn i => no_tac) |
236 |
236 |
237 val distinct_simproc = |
237 val distinct_simproc = |
238 Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"] |
238 Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"] |
239 (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) => |
239 (fn thy => fn ss => (fn (Const (@{const_name HOL.eq},_)$(x as Free _)$(y as Free _)) => |
240 (case try Simplifier.the_context ss of |
240 (case try Simplifier.the_context ss of |
241 SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) |
241 SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) |
242 (neq_x_y ctxt x y) |
242 (neq_x_y ctxt x y) |
243 | NONE => NONE) |
243 | NONE => NONE) |
244 | _ => NONE)) |
244 | _ => NONE)) |