merged

--- a/src/HOL/Int.thy	Tue Feb 17 20:45:23 2009 -0800
+++ b/src/HOL/Int.thy	Wed Feb 18 10:26:48 2009 +0100
@@ -1627,7 +1627,7 @@
 context ring_1
 begin
 
-lemma of_int_of_nat:
+lemma of_int_of_nat [nitpick_const_simp]:
   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
 proof (cases "k < 0")
   case True then have "0 \<le> - k" by simp

--- a/src/HOL/Tools/refute.ML	Tue Feb 17 20:45:23 2009 -0800
+++ b/src/HOL/Tools/refute.ML	Wed Feb 18 10:26:48 2009 +0100
@@ -2662,6 +2662,34 @@
   (* theory -> model -> arguments -> Term.term ->
     (interpretation * model * arguments) option *)
 
+  fun set_interpreter thy model args t =
+  let
+    val (typs, terms) = model
+  in
+    case AList.lookup (op =) terms t of
+      SOME intr =>
+      (* return an existing interpretation *)
+      SOME (intr, model, args)
+    | NONE =>
+      (case t of
+      (* 'Collect' == identity *)
+        Const (@{const_name Collect}, _) $ t1 =>
+        SOME (interpret thy model args t1)
+      | Const (@{const_name Collect}, _) =>
+        SOME (interpret thy model args (eta_expand t 1))
+      (* 'op :' == application *)
+      | Const (@{const_name "op :"}, _) $ t1 $ t2 =>
+        SOME (interpret thy model args (t2 $ t1))
+      | Const (@{const_name "op :"}, _) $ t1 =>
+        SOME (interpret thy model args (eta_expand t 1))
+      | Const (@{const_name "op :"}, _) =>
+        SOME (interpret thy model args (eta_expand t 2))
+      | _ => NONE)
+  end;
+
+  (* theory -> model -> arguments -> Term.term ->
+    (interpretation * model * arguments) option *)
+
   (* only an optimization: 'card' could in principle be interpreted with *)
   (* interpreters available already (using its definition), but the code *)
   (* below is more efficient                                             *)
@@ -3271,6 +3299,7 @@
      add_interpreter "stlc"    stlc_interpreter #>
      add_interpreter "Pure"    Pure_interpreter #>
      add_interpreter "HOLogic" HOLogic_interpreter #>
+     add_interpreter "set"     set_interpreter #>
      add_interpreter "IDT"             IDT_interpreter #>
      add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
      add_interpreter "IDT_recursion"   IDT_recursion_interpreter #>