diff -r 3cae30b60577 -r 63112be4a469 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:26:27 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:29:23 2010 +0100
@@ -32,7 +32,7 @@
 datatype annotation = Gen | New | Fls | Tru
 datatype annotation_atom = A of annotation | V of var
 
-type assign_literal = var * annotation
+type assign_literal = var * (sign * annotation)
 
 datatype mtyp =
   MAlpha |
@@ -82,8 +82,9 @@
 fun string_for_annotation_atom (A a) = string_for_annotation a
   | string_for_annotation_atom (V x) = string_for_var x
 
-fun string_for_assign_literal (x, a) =
-  string_for_var x ^ " = " ^ string_for_annotation a
+fun string_for_assign_literal (x, (sn, a)) =
+  string_for_var x ^ (case sn of Plus => " = " | Minus => " \<noteq> ") ^
+  string_for_annotation a
 
 val bool_M = MType (@{type_name bool}, [])
 val dummy_M = MType (nitpick_prefix ^ "dummy", [])
@@ -346,7 +347,7 @@
       | aux (MRec z) = MRec z
   in aux end
 
-datatype comp_op = Eq | Leq
+datatype comp_op = Eq | Neq | Leq
 
 type comp = annotation_atom * annotation_atom * comp_op * var list
 type assign_clause = assign_literal list
@@ -354,6 +355,7 @@
 type constraint_set = comp list * assign_clause list
 
 fun string_for_comp_op Eq = "="
+  | string_for_comp_op Neq = "\<noteq>"
   | string_for_comp_op Leq = "\<le>"
 
 fun string_for_comp (aa1, aa2, cmp, xs) =
@@ -364,28 +366,39 @@
   | string_for_assign_clause asgs =
     space_implode " \<or> " (map string_for_assign_literal asgs)
 
-fun add_assign_literal (x, a) clauses =
-  if exists (fn [(x', a')] => x = x' andalso a <> a' | _ => false) clauses then
+fun add_assign_literal (x, (sn, a)) clauses =
+  if exists (fn [(x', (sn', a'))] =>
+                x = x' andalso ((sn = sn' andalso a <> a') orelse
+                                (sn <> sn' andalso a = a'))
+              | _ => false) clauses then
     NONE
   else
-    SOME ([(x, a)] :: clauses)fun add_assign_conjunct _ NONE = NONE
+    SOME ([(x, a)] :: clauses)
 
 fun add_assign_disjunct _ NONE = NONE
   | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs)
 
-fun do_annotation_atom_comp Eq [] aa1 aa2 (cset as (comps, clauses)) =
+fun annotation_comp Eq a1 a2 = (a1 = a2)
+  | annotation_comp Neq a1 a2 = (a1 <> a2)
+  | annotation_comp Leq a1 a2 = (a1 = a2 orelse a2 = Gen)
+
+fun comp_op_sign Eq = Plus
+  | comp_op_sign Neq = Minus
+  | comp_op_sign Leq =
+    raise BAD ("Nitpick_Mono.comp_op_sign", "unexpected \"Leq\"")
+
+fun do_annotation_atom_comp Leq [] aa1 aa2 (cset as (comps, clauses)) =
     (case (aa1, aa2) of
-       (A a1, A a2) => if a1 = a2 then SOME cset else NONE
+       (A a1, A a2) => if annotation_comp Leq a1 a2 then SOME cset else NONE
+     | _ => SOME (insert (op =) (aa1, aa2, Leq, []) comps, clauses))
+  | do_annotation_atom_comp cmp [] aa1 aa2 (cset as (comps, clauses)) =
+    (case (aa1, aa2) of
+       (A a1, A a2) => if annotation_comp cmp a1 a2 then SOME cset else NONE
      | (V x1, A a2) =>
-       clauses |> add_assign_literal (x1, a2) |> Option.map (pair comps)
-     | (V _, V _) => SOME (insert (op =) (aa1, aa2, Eq, []) comps, clauses)
-     | _ => do_annotation_atom_comp Eq [] aa2 aa1 cset)
-  | do_annotation_atom_comp Leq [] aa1 aa2 (cset as (comps, clauses)) =
-    (case (aa1, aa2) of
-       (_, A Gen) => SOME cset
-     | (A Gen, A _) => NONE
-     | (A a1, A a2) => if a1 = a2 then SOME cset else NONE
-     | _ => SOME (insert (op =) (aa1, aa2, Leq, []) comps, clauses))
+       clauses |> add_assign_literal (x1, (comp_op_sign cmp, a2))
+               |> Option.map (pair comps)
+     | (A _, V _) => do_annotation_atom_comp cmp [] aa2 aa1 cset
+     | (V _, V _) => SOME (insert (op =) (aa1, aa2, cmp, []) comps, clauses))
   | do_annotation_atom_comp cmp xs aa1 aa2 (comps, clauses) =
     SOME (insert (op =) (aa1, aa2, cmp, xs) comps, clauses)
 
@@ -440,8 +453,8 @@
 fun do_notin_mtype_fv _ _ _ NONE = NONE
   | do_notin_mtype_fv Minus _ MAlpha cset = cset
   | do_notin_mtype_fv Plus [] MAlpha _ = NONE
-  | do_notin_mtype_fv Plus [(x, a)] MAlpha (SOME clauses) =
-    clauses |> add_assign_literal (x, a)
+  | do_notin_mtype_fv Plus [asg] MAlpha (SOME clauses) =
+    clauses |> add_assign_literal asg
   | do_notin_mtype_fv Plus clause MAlpha (SOME clauses) =
     SOME (insert (op =) clause clauses)
   | do_notin_mtype_fv sn clause (MFun (M1, A a, M2)) cset =
@@ -451,13 +464,13 @@
              else I)
          |> do_notin_mtype_fv sn clause M2
   | do_notin_mtype_fv Plus clause (MFun (M1, V x, M2)) cset =
-    cset |> (case add_assign_disjunct (x, Gen) (SOME clause) of
+    cset |> (case add_assign_disjunct (x, (Plus, Gen)) (SOME clause) of
                NONE => I
              | SOME clause' => do_notin_mtype_fv Plus clause' M1)
          |> do_notin_mtype_fv Minus clause M1
          |> do_notin_mtype_fv Plus clause M2
   | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) cset =
-    cset |> (case fold (fn a => add_assign_disjunct (x, a)) [Fls, Tru]
+    cset |> (case fold (fn a => add_assign_disjunct (x, (Plus, a))) [Fls, Tru]
                        (SOME clause) of
                NONE => I
              | SOME clause' => do_notin_mtype_fv Plus clause' M1)
@@ -495,13 +508,15 @@
 fun prop_for_bool_var_equality (v1, v2) =
   PL.And (PL.Or (PL.BoolVar v1, PL.Not (PL.BoolVar v2)),
           PL.Or (PL.Not (PL.BoolVar v1), PL.BoolVar v2))
-fun prop_for_assign_literal (x, a) =
+fun prop_for_assign (x, a) =
   let val (b1, b2) = bools_from_annotation a in
     PL.And (PL.BoolVar (fst_var x) |> not b1 ? PL.Not,
             PL.BoolVar (snd_var x) |> not b2 ? PL.Not)
   end
+fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a)
+  | prop_for_assign_literal (x, (Minus, a)) = PL.Not (prop_for_assign (x, a))
 fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a')
-  | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, a)
+  | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a))
 fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2)
   | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1)
   | prop_for_atom_equality (V x1, V x2) =
@@ -509,10 +524,12 @@
             prop_for_bool_var_equality (pairself snd_var (x1, x2)))
 val prop_for_assign_clause = PL.exists o map prop_for_assign_literal
 fun prop_for_exists_var_assign_literal xs a =
-  PL.exists (map (fn x => prop_for_assign_literal (x, a)) xs)
+  PL.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs)
 fun prop_for_comp (aa1, aa2, Eq, []) =
     PL.SAnd (prop_for_comp (aa1, aa2, Leq, []),
              prop_for_comp (aa2, aa1, Leq, []))
+  | prop_for_comp (aa1, aa2, Neq, []) =
+    PL.Not (prop_for_comp (aa1, aa2, Eq, []))
   | prop_for_comp (aa1, aa2, Leq, []) =
     PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
   | prop_for_comp (aa1, aa2, cmp, xs) =
@@ -526,7 +543,8 @@
   @ (if calculus > 2 then [New, Tru] else [])
 
 fun prop_for_variable_domain calculus x =
-  PL.exists (map (curry prop_for_assign_literal x) (variable_domain calculus))
+  PL.exists (map (fn a => prop_for_assign_literal (x, (Plus, a)))
+                 (variable_domain calculus))
 
 fun extract_assigns max_var assigns asgs =
   fold (fn x => fn accum =>
@@ -555,7 +573,7 @@
 
 fun solve calculus max_var (comps, clauses) =
   let
-    val asgs = map_filter (fn [asg] => SOME asg | _ => NONE) clauses
+    val asgs = map_filter (fn [(x, (_, a))] => SOME (x, a) | _ => NONE) clauses
     fun do_assigns assigns =
       SOME (extract_assigns max_var assigns asgs |> tap print_solution)
     val _ = print_problem calculus comps clauses