26 add_atoms (not pos) x |
26 add_atoms (not pos) x |
27 | add_atoms pos x = cons (pos, x); |
27 | add_atoms pos x = cons (pos, x); |
28 |
28 |
29 fun atoms fml = add_atoms true fml []; |
29 fun atoms fml = add_atoms true fml []; |
30 |
30 |
31 fun zero1 pt (c as Const (@{const_name Groups.plus}, _) $ x $ y) = |
31 fun zero1 pt ((c as Const (@{const_name Groups.plus}, _)) $ x $ y) = |
32 (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE |
32 (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE |
33 | SOME z => SOME(c $ x $ z)) |
33 | SOME z => SOME (c $ x $ z)) |
34 | SOME z => SOME (c $ z $ y)) |
34 | SOME z => SOME (c $ z $ y)) |
35 | zero1 pt (c as Const (@{const_name Groups.minus}, _) $ x $ y) = |
35 | zero1 pt ((c as Const (@{const_name Groups.minus}, _)) $ x $ y) = |
36 (case zero1 pt x of |
36 (case zero1 pt x of |
37 NONE => (case zero1 (apfst not pt) y of NONE => NONE |
37 NONE => (case zero1 (apfst not pt) y of NONE => NONE |
38 | SOME z => SOME (c $ x $ z)) |
38 | SOME z => SOME (c $ x $ z)) |
39 | SOME z => SOME (c $ z $ y)) |
39 | SOME z => SOME (c $ z $ y)) |
40 | zero1 pt (c as Const (@{const_name Groups.uminus}, _) $ x) = |
40 | zero1 pt ((c as Const (@{const_name Groups.uminus}, _)) $ x) = |
41 (case zero1 (apfst not pt) x of NONE => NONE |
41 (case zero1 (apfst not pt) x of NONE => NONE |
42 | SOME z => SOME (c $ z)) |
42 | SOME z => SOME (c $ z)) |
43 | zero1 (pos, t) u = |
43 | zero1 (pos, t) u = |
44 if pos andalso (t aconv u) |
44 if pos andalso (t aconv u) |
45 then SOME (Const (@{const_name Groups.zero}, fastype_of t)) |
45 then SOME (Const (@{const_name Groups.zero}, fastype_of t)) |