equal
deleted
inserted
replaced
305 |
305 |
306 fun prove_antisym_le ss t = |
306 fun prove_antisym_le ss t = |
307 let |
307 let |
308 val (le, r, s) = dest_binop t |
308 val (le, r, s) = dest_binop t |
309 val less = Const (@{const_name less}, Term.fastype_of le) |
309 val less = Const (@{const_name less}, Term.fastype_of le) |
310 val prems = Simplifier.prems_of_ss ss |
310 val prems = Simplifier.prems_of ss |
311 in |
311 in |
312 (case find_first (eq_prop (le $ s $ r)) prems of |
312 (case find_first (eq_prop (le $ s $ r)) prems of |
313 NONE => |
313 NONE => |
314 find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems |
314 find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems |
315 |> Option.map (fn thm => thm RS antisym_less1) |
315 |> Option.map (fn thm => thm RS antisym_less1) |
319 |
319 |
320 fun prove_antisym_less ss t = |
320 fun prove_antisym_less ss t = |
321 let |
321 let |
322 val (less, r, s) = dest_binop (HOLogic.dest_not t) |
322 val (less, r, s) = dest_binop (HOLogic.dest_not t) |
323 val le = Const (@{const_name less_eq}, Term.fastype_of less) |
323 val le = Const (@{const_name less_eq}, Term.fastype_of less) |
324 val prems = prems_of_ss ss |
324 val prems = Simplifier.prems_of ss |
325 in |
325 in |
326 (case find_first (eq_prop (le $ r $ s)) prems of |
326 (case find_first (eq_prop (le $ r $ s)) prems of |
327 NONE => |
327 NONE => |
328 find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems |
328 find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems |
329 |> Option.map (fn thm => thm RS antisym_less2) |
329 |> Option.map (fn thm => thm RS antisym_less2) |