# HG changeset patch
# User blanchet
# Date 1263980299 -3600
# Node ID fb90752a92713de79610f54ee719118d72749cdb
# Parent  c4f04bee79f3c93944ecf5e613f11ed0d3574afc# Parent  440605046777b668745aa2b599bd25a5ad224f00
merged

diff -r 440605046777 -r fb90752a9271 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Wed Jan 20 10:38:19 2010 +0100
@@ -496,14 +496,14 @@
 
 (* problem -> problem -> bool *)
 fun problems_equivalent (p1 : problem) (p2 : problem) =
-  #univ_card p1 = #univ_card p2
-  andalso #formula p1 = #formula p2
-  andalso #bounds p1 = #bounds p2
-  andalso #expr_assigns p1 = #expr_assigns p2
-  andalso #tuple_assigns p1 = #tuple_assigns p2
-  andalso #int_bounds p1 = #int_bounds p2
-  andalso filter (is_relevant_setting o fst) (#settings p1)
-          = filter (is_relevant_setting o fst) (#settings p2)
+  #univ_card p1 = #univ_card p2 andalso
+  #formula p1 = #formula p2 andalso
+  #bounds p1 = #bounds p2 andalso
+  #expr_assigns p1 = #expr_assigns p2 andalso
+  #tuple_assigns p1 = #tuple_assigns p2 andalso
+  #int_bounds p1 = #int_bounds p2 andalso
+  filter (is_relevant_setting o fst) (#settings p1)
+  = filter (is_relevant_setting o fst) (#settings p2)
 
 (* int -> string *)
 fun base_name j =
@@ -883,8 +883,8 @@
 
 (* string -> bool *)
 fun is_ident_char s =
-  Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
-  orelse s = "_" orelse s = "'" orelse s = "$"
+  Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse
+  s = "_" orelse s = "'" orelse s = "$"
 
 (* string list -> string list *)
 fun strip_blanks [] = []
@@ -950,9 +950,9 @@
    -> substring * (int * raw_bound list) list * int list *)
 fun read_next_outcomes j (s, ps, js) =
   let val (s1, s2) = Substring.position outcome_marker s in
-    if Substring.isEmpty s2
-       orelse not (Substring.isEmpty (Substring.position problem_marker s1
-                                      |> snd)) then
+    if Substring.isEmpty s2 orelse
+       not (Substring.isEmpty (Substring.position problem_marker s1
+                               |> snd)) then
       (s, ps, js)
     else
       let
diff -r 440605046777 -r fb90752a9271 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Jan 20 10:38:19 2010 +0100
@@ -188,17 +188,11 @@
                            orig_t =
   let
     val timer = Timer.startRealTimer ()
-    val user_thy = Proof.theory_of state
+    val thy = Proof.theory_of state
+    val ctxt = Proof.context_of state
     val nitpick_thy = ThyInfo.get_theory "Nitpick"
-    val nitpick_thy_missing = not (Theory.subthy (nitpick_thy, user_thy))
-    val thy = if nitpick_thy_missing then
-                Theory.begin_theory "Nitpick_Internal_Name_Do_Not_Use_XYZZY"
-                                    [nitpick_thy, user_thy]
-                |> Theory.checkpoint
-              else
-                user_thy
-    val ctxt = Proof.context_of state
-               |> nitpick_thy_missing ? Context.raw_transfer thy
+    val _ = Theory.subthy (nitpick_thy, thy) orelse
+            error "You must import the theory \"Nitpick\" to use Nitpick"
     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
          boxes, monos, wfs, sat_solver, blocking, falsify, debug, verbose,
          overlord, user_axioms, assms, merge_type_vars, binary_ints,
@@ -280,8 +274,8 @@
        unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
        constr_cache = Unsynchronized.ref []}
     val frees = Term.add_frees assms_t []
-    val _ = null (Term.add_tvars assms_t [])
-            orelse raise NOT_SUPPORTED "schematic type variables"
+    val _ = null (Term.add_tvars assms_t []) orelse
+            raise NOT_SUPPORTED "schematic type variables"
     val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
          core_t) = preprocess_term ext_ctxt assms_t
     val got_all_user_axioms =
@@ -325,77 +319,65 @@
 
     val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
     (* typ -> bool *)
-    fun is_free_type_monotonic T =
-      unique_scope orelse
-      case triple_lookup (type_match thy) monos T of
-        SOME (SOME b) => b
-      | _ => is_bit_type T
-             orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
-    fun is_datatype_monotonic T =
+    fun is_type_always_monotonic T =
+      ((not (is_pure_typedef thy T) orelse is_univ_typedef thy T) andalso
+       not (is_quot_type thy T)) orelse
+      is_number_type thy T orelse is_bit_type T
+    fun is_type_monotonic T =
       unique_scope orelse
       case triple_lookup (type_match thy) monos T of
         SOME (SOME b) => b
-      | _ => not (is_pure_typedef thy T) orelse is_univ_typedef thy T
-             orelse is_number_type thy T
-             orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
-    fun is_datatype_deep T =
-      is_word_type T
-      orelse exists (curry (op =) T o domain_type o type_of) sel_names
+      | _ => is_type_always_monotonic T orelse
+             formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
+    fun is_deep_datatype T =
+      is_datatype thy T andalso
+      (is_word_type T orelse
+       exists (curry (op =) T o domain_type o type_of) sel_names)
     val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
              |> sort TermOrd.typ_ord
-    val _ = if verbose andalso binary_ints = SOME true
-               andalso exists (member (op =) [nat_T, int_T]) Ts then
+    val _ = if verbose andalso binary_ints = SOME true andalso
+               exists (member (op =) [nat_T, int_T]) Ts then
               print_v (K "The option \"binary_ints\" will be ignored because \
                          \of the presence of rationals, reals, \"Suc\", \
                          \\"gcd\", or \"lcm\" in the problem.")
             else
               ()
-    val (all_dataTs, all_free_Ts) =
-      List.partition (is_integer_type orf is_datatype thy) Ts
-    val (mono_dataTs, nonmono_dataTs) =
-      List.partition is_datatype_monotonic all_dataTs
-    val (mono_free_Ts, nonmono_free_Ts) =
-      List.partition is_free_type_monotonic all_free_Ts
-
-    val interesting_mono_free_Ts = filter_out is_bit_type mono_free_Ts
+    val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic Ts
     val _ =
-      if not unique_scope andalso not (null interesting_mono_free_Ts) then
-        print_v (fn () =>
-                    let
-                      val ss = map (quote o string_for_type ctxt)
-                                   interesting_mono_free_Ts
-                    in
-                      "The type" ^ plural_s_for_list ss ^ " " ^
-                      space_implode " " (serial_commas "and" ss) ^ " " ^
-                      (if none_true monos then
-                         "passed the monotonicity test"
-                       else
-                         (if length ss = 1 then "is" else "are") ^
-                         " considered monotonic") ^
-                      ". Nitpick might be able to skip some scopes."
-                    end)
+      if verbose andalso not unique_scope then
+        case filter_out is_type_always_monotonic mono_Ts of
+          [] => ()
+        | interesting_mono_Ts =>
+          print_v (fn () =>
+                      let
+                        val ss = map (quote o string_for_type ctxt)
+                                     interesting_mono_Ts
+                      in
+                        "The type" ^ plural_s_for_list ss ^ " " ^
+                        space_implode " " (serial_commas "and" ss) ^ " " ^
+                        (if none_true monos then
+                           "passed the monotonicity test"
+                         else
+                           (if length ss = 1 then "is" else "are") ^
+                           " considered monotonic") ^
+                        ". Nitpick might be able to skip some scopes."
+                      end)
       else
         ()
-    val mono_Ts = mono_dataTs @ mono_free_Ts
-    val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts
-    val shallow_dataTs = filter_out is_datatype_deep mono_dataTs
+    val shallow_dataTs = filter_out is_deep_datatype Ts
 (*
-    val _ = priority "Monotonic datatypes:"
-    val _ = List.app (priority o string_for_type ctxt) mono_dataTs
-    val _ = priority "Nonmonotonic datatypes:"
-    val _ = List.app (priority o string_for_type ctxt) nonmono_dataTs
-    val _ = priority "Monotonic free types:"
-    val _ = List.app (priority o string_for_type ctxt) mono_free_Ts
-    val _ = priority "Nonmonotonic free types:"
-    val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts
+    val _ = priority "Monotonic types:"
+    val _ = List.app (priority o string_for_type ctxt) mono_Ts
+    val _ = priority "Nonmonotonic types:"
+    val _ = List.app (priority o string_for_type ctxt) nonmono_Ts
 *)
 
     val need_incremental = Int.max (max_potential, max_genuine) >= 2
     val effective_sat_solver =
       if sat_solver <> "smart" then
-        if need_incremental
-           andalso not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
-                               sat_solver) then
+        if need_incremental andalso
+           not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
+                      sat_solver) then
           (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
                        \be used instead of " ^ quote sat_solver ^ "."));
            "SAT4J")
@@ -421,9 +403,9 @@
             (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
       let
         val _ = not (exists (fn other => scope_less_eq other scope)
-                            (!too_big_scopes))
-                orelse raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\
-                                        \problem_for_scope", "too large scope")
+                            (!too_big_scopes)) orelse
+                raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\
+                                 \problem_for_scope", "too large scope")
 (*
         val _ = priority "Offsets:"
         val _ = List.app (fn (T, j0) =>
@@ -437,9 +419,9 @@
         val main_j0 = offset_of_type ofs bool_T
         val (nat_card, nat_j0) = spec_of_type scope nat_T
         val (int_card, int_j0) = spec_of_type scope int_T
-        val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0)
-                orelse raise BAD ("Nitpick.pick_them_nits_in_term.\
-                                  \problem_for_scope", "bad offsets")
+        val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0) orelse
+                raise BAD ("Nitpick.pick_them_nits_in_term.problem_for_scope",
+                           "bad offsets")
         val kk = kodkod_constrs peephole_optim nat_card int_card main_j0
         val (free_names, rep_table) =
           choose_reps_for_free_vars scope free_names NameTable.empty
@@ -527,8 +509,8 @@
                defs = nondef_fs @ def_fs @ declarative_axioms})
       end
       handle TOO_LARGE (loc, msg) =>
-             if loc = "Nitpick_KK.check_arity"
-                andalso not (Typtab.is_empty ofs) then
+             if loc = "Nitpick_Kodkod.check_arity" andalso
+                not (Typtab.is_empty ofs) then
                problem_for_scope liberal
                    {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
                     bits = bits, bisim_depth = bisim_depth,
diff -r 440605046777 -r fb90752a9271 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 20 10:38:19 2010 +0100
@@ -82,6 +82,7 @@
   val dest_n_tuple : int -> term -> term list
   val instantiate_type : theory -> typ -> typ -> typ -> typ
   val is_real_datatype : theory -> string -> bool
+  val is_quot_type : theory -> typ -> bool
   val is_codatatype : theory -> typ -> bool
   val is_pure_typedef : theory -> typ -> bool
   val is_univ_typedef : theory -> typ -> bool
@@ -91,6 +92,8 @@
   val is_record_update : theory -> styp -> bool
   val is_abs_fun : theory -> styp -> bool
   val is_rep_fun : theory -> styp -> bool
+  val is_quot_abs_fun : Proof.context -> styp -> bool
+  val is_quot_rep_fun : Proof.context -> styp -> bool
   val is_constr : theory -> styp -> bool
   val is_stale_constr : theory -> styp -> bool
   val is_sel : string -> bool
@@ -325,6 +328,8 @@
    (@{const_name uminus_int_inst.uminus_int}, 0),
    (@{const_name ord_int_inst.less_int}, 2),
    (@{const_name ord_int_inst.less_eq_int}, 2),
+   (@{const_name unknown}, 0),
+   (@{const_name is_unknown}, 1),
    (@{const_name Tha}, 1),
    (@{const_name Frac}, 0),
    (@{const_name norm_frac}, 0)]
@@ -506,8 +511,8 @@
     val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
     val (co_s, co_Ts) = dest_Type co_T
     val _ =
-      if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts)
-         andalso co_s <> "fun" andalso not (is_basic_datatype co_s) then
+      if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
+         co_s <> "fun" andalso not (is_basic_datatype co_s) then
         ()
       else
         raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
@@ -543,14 +548,16 @@
 val is_typedef = is_some oo typedef_info
 val is_real_datatype = is_some oo Datatype.get_info
 (* theory -> typ -> bool *)
+fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* ### *)
+  | is_quot_type _ _ = false
 fun is_codatatype thy (T as Type (s, _)) =
     not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
                |> Option.map snd |> these))
   | is_codatatype _ _ = false
 fun is_pure_typedef thy (T as Type (s, _)) =
     is_typedef thy s andalso
-    not (is_real_datatype thy s orelse is_codatatype thy T
-         orelse is_record_type T orelse is_integer_type T)
+    not (is_real_datatype thy s orelse is_quot_type thy T orelse
+         is_codatatype thy T orelse is_record_type T orelse is_integer_type T)
   | is_pure_typedef _ _ = false
 fun is_univ_typedef thy (Type (s, _)) =
     (case typedef_info thy s of
@@ -564,8 +571,9 @@
      | NONE => false)
   | is_univ_typedef _ _ = false
 fun is_datatype thy (T as Type (s, _)) =
-    (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind})
-    andalso not (is_basic_datatype s)
+    (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
+     is_quot_type thy T) andalso
+    not (is_basic_datatype s)
   | is_datatype _ _ = false
 
 (* theory -> typ -> (string * typ) list * (string * typ) *)
@@ -606,6 +614,11 @@
        SOME {Rep_name, ...} => s = Rep_name
      | NONE => false)
   | is_rep_fun _ _ = false
+(* Proof.context -> styp -> bool *)
+fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* ### *)
+  | is_quot_abs_fun _ _ = false
+fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* ### *)
+  | is_quot_rep_fun _ _ = false
 
 (* theory -> styp -> styp *)
 fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
@@ -613,6 +626,15 @@
        SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
      | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
   | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
+(* theory -> typ -> typ *)
+fun rep_type_for_quot_type _ (Type ("IntEx.my_int", [])) = @{typ "nat * nat"}
+  | rep_type_for_quot_type _ T =
+    raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
+(* theory -> typ -> term *)
+fun equiv_relation_for_quot_type _ (Type ("IntEx.my_int", [])) =
+    Const ("IntEx.intrel", @{typ "(nat * nat) => (nat * nat) => bool"})
+  | equiv_relation_for_quot_type _ T =
+    raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
 
 (* theory -> styp -> bool *)
 fun is_coconstr thy (s, T) =
@@ -628,19 +650,20 @@
 fun is_constr_like thy (s, T) =
   s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse
   let val (x as (s, T)) = (s, unbit_and_unbox_type T) in
-    Refute.is_IDT_constructor thy x orelse is_record_constr x
-    orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
-    orelse s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep}
-    orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
-    orelse is_coconstr thy x
+    Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
+    (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
+    s = @{const_name Quot} orelse
+    s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep} orelse
+    x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse
+    is_coconstr thy x
   end
 fun is_stale_constr thy (x as (_, T)) =
-  is_codatatype thy (body_type T) andalso is_constr_like thy x
-  andalso not (is_coconstr thy x)
+  is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
+  not (is_coconstr thy x)
 fun is_constr thy (x as (_, T)) =
-  is_constr_like thy x
-  andalso not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T)))))
-  andalso not (is_stale_constr thy x)
+  is_constr_like thy x andalso
+  not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) andalso
+  not (is_stale_constr thy x)
 (* string -> bool *)
 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
 val is_sel_like_and_no_discr =
@@ -662,13 +685,13 @@
 fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
   case T of
     Type ("fun", _) =>
-    (boxy = InPair orelse boxy = InFunLHS)
-    andalso not (is_boolean_type (body_type T))
+    (boxy = InPair orelse boxy = InFunLHS) andalso
+    not (is_boolean_type (body_type T))
   | Type ("*", Ts) =>
-    boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2
-    orelse ((boxy = InExpr orelse boxy = InFunLHS)
-            andalso exists (is_boxing_worth_it ext_ctxt InPair)
-                           (map (box_type ext_ctxt InPair) Ts))
+    boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
+    ((boxy = InExpr orelse boxy = InFunLHS) andalso
+     exists (is_boxing_worth_it ext_ctxt InPair)
+            (map (box_type ext_ctxt InPair) Ts))
   | _ => false
 (* extended_context -> boxability -> string * typ list -> string *)
 and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
@@ -679,8 +702,8 @@
 and box_type ext_ctxt boxy T =
   case T of
     Type (z as ("fun", [T1, T2])) =>
-    if boxy <> InConstr andalso boxy <> InSel
-       andalso should_box_type ext_ctxt boxy z then
+    if boxy <> InConstr andalso boxy <> InSel andalso
+       should_box_type ext_ctxt boxy z then
       Type (@{type_name fun_box},
             [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
     else
@@ -778,6 +801,8 @@
                val T' = (Record.get_extT_fields thy T
                         |> apsnd single |> uncurry append |> map snd) ---> T
              in [(s', T')] end
+           else if is_quot_type thy T then
+             [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
            else case typedef_info thy s of
              SOME {abs_type, rep_type, Abs_name, ...} =>
              [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
@@ -871,10 +896,10 @@
     let val args = map Envir.eta_contract args in
       case hd args of
         Const (x' as (s', _)) $ t =>
-        if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s
-           andalso forall (fn (n, t') =>
-                              select_nth_constr_arg thy x t n dummyT = t')
-                          (index_seq 0 (length args) ~~ args) then
+        if is_sel_like_and_no_discr s' andalso
+           constr_name_for_sel_like s' = s andalso
+           forall (fn (n, t') => select_nth_constr_arg thy x t n dummyT = t')
+                  (index_seq 0 (length args) ~~ args) then
           t
         else
           list_comb (Const x, args)
@@ -1011,8 +1036,8 @@
 (* theory -> string -> bool *)
 fun is_funky_typedef_name thy s =
   member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
-                 @{type_name int}] s
-  orelse is_frac_type thy (Type (s, []))
+                 @{type_name int}] s orelse
+  is_frac_type thy (Type (s, []))
 (* theory -> term -> bool *)
 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
   | is_funky_typedef _ _ = false
@@ -1055,8 +1080,8 @@
     (* term -> bool *)
     fun do_lhs t1 =
       case strip_comb t1 of
-        (Const _, args) => forall is_Var args
-                           andalso not (has_duplicates (op =) args)
+        (Const _, args) =>
+        forall is_Var args andalso not (has_duplicates (op =) args)
       | _ => false
     fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
       | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
@@ -1174,8 +1199,8 @@
     (* term -> bool *)
     fun is_good_arg (Bound _) = true
       | is_good_arg (Const (s, _)) =
-        s = @{const_name True} orelse s = @{const_name False}
-        orelse s = @{const_name undefined}
+        s = @{const_name True} orelse s = @{const_name False} orelse
+        s = @{const_name undefined}
       | is_good_arg _ = false
   in
     case t |> strip_abs_body |> strip_comb of
@@ -1289,9 +1314,17 @@
 fun nondef_props_for_const thy slack table (x as (s, _)) =
   these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
 
+(* theory -> styp -> term list *)
+fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
+  let val abs_T = domain_type T in
+    typedef_info thy (fst (dest_Type abs_T)) |> the
+    |> pairf #Abs_inverse #Rep_inverse
+    |> pairself (Refute.specialize_type thy x o prop_of o the)
+    ||> single |> op ::
+  end
 (* theory -> styp list -> term list *)
-fun optimized_typedef_axioms thy (abs_s, abs_Ts) =
-  let val abs_T = Type (abs_s, abs_Ts) in
+fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) =
+  let val abs_T = Type abs_z in
     if is_univ_typedef thy abs_T then
       []
     else case typedef_info thy abs_s of
@@ -1313,13 +1346,31 @@
       end
     | NONE => []
   end
-(* theory -> styp -> term list *)
-fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
-  let val abs_T = domain_type T in
-    typedef_info thy (fst (dest_Type abs_T)) |> the
-    |> pairf #Abs_inverse #Rep_inverse
-    |> pairself (Refute.specialize_type thy x o prop_of o the)
-    ||> single |> op ::
+fun optimized_quot_type_axioms thy abs_z =
+  let
+    val abs_T = Type abs_z
+    val rep_T = rep_type_for_quot_type thy abs_T
+    val equiv_rel = equiv_relation_for_quot_type thy abs_T
+    val a_var = Var (("a", 0), abs_T)
+    val x_var = Var (("x", 0), rep_T)
+    val y_var = Var (("y", 0), rep_T)
+    val x = (@{const_name Quot}, rep_T --> abs_T)
+    val sel_a_t = select_nth_constr_arg thy x a_var 0 rep_T
+    val normal_t = Const (@{const_name quot_normal}, rep_T --> rep_T)
+    val normal_x = normal_t $ x_var
+    val normal_y = normal_t $ y_var
+    val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
+  in
+    [Logic.mk_equals (sel_a_t, normal_t $ sel_a_t),
+     Logic.list_implies
+         ([@{const Not} $ (HOLogic.mk_eq (x_var, y_var)),
+           @{const Not} $ (is_unknown_t $ normal_x),
+           @{const Not} $ (is_unknown_t $ normal_y),
+           equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
+           Logic.mk_equals (normal_x, normal_y)),
+     @{const "==>"}
+         $ (HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)))
+         $ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
   end
 
 (* theory -> int * styp -> term *)
@@ -1402,8 +1453,8 @@
 (* extended_context -> styp -> bool *)
 fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
                             : extended_context) x =
-  not (null (def_props_for_const thy fast_descrs intro_table x))
-  andalso fixpoint_kind_of_const thy def_table x <> NoFp
+  not (null (def_props_for_const thy fast_descrs intro_table x)) andalso
+  fixpoint_kind_of_const thy def_table x <> NoFp
 fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
                             : extended_context) x =
   exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
@@ -1489,10 +1540,9 @@
         (t1 |> HOLogic.dest_list |> distinctness_formula T'
          handle TERM _ => do_const depth Ts t x [t1])
       | (t0 as Const (x as (@{const_name If}, _))) $ t1 $ t2 $ t3 =>
-        if is_ground_term t1
-           andalso exists (Pattern.matches thy o rpair t1)
-                          (Inttab.lookup_list ground_thm_table
-                                              (hash_term t1)) then
+        if is_ground_term t1 andalso
+           exists (Pattern.matches thy o rpair t1)
+                  (Inttab.lookup_list ground_thm_table (hash_term t1)) then
           do_term depth Ts t2
         else
           do_const depth Ts t x [t1, t2, t3]
@@ -1534,8 +1584,24 @@
               if is_constr thy x then
                 (Const x, ts)
               else if is_stale_constr thy x then
-                raise NOT_SUPPORTED ("(non-co-)constructors of codatatypes \
+                raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
                                      \(\"" ^ s ^ "\")")
+              else if is_quot_abs_fun thy x then
+                let
+                  val rep_T = domain_type T
+                  val abs_T = range_type T
+                in
+                  (Abs (Name.uu, rep_T,
+                        Const (@{const_name Quot}, rep_T --> abs_T)
+                               $ (Const (@{const_name quot_normal},
+                                         rep_T --> rep_T) $ Bound 0)), ts)
+                end
+              else if is_quot_rep_fun thy x then
+                let
+                  val abs_T = domain_type T
+                  val rep_T = range_type T
+                  val x' = (@{const_name Quot}, rep_T --> abs_T)
+                in select_nth_constr_arg_with_args depth Ts x' ts 0 rep_T end
               else if is_record_get thy x then
                 case length ts of
                   0 => (do_term depth Ts (eta_expand Ts t 1), [])
@@ -1691,8 +1757,8 @@
                  else
                    ()
        in
-         if tac_timeout = (!cached_timeout)
-            andalso length (!cached_wf_props) < max_cached_wfs then
+         if tac_timeout = (!cached_timeout) andalso
+            length (!cached_wf_props) < max_cached_wfs then
            ()
          else
            (cached_wf_props := []; cached_timeout := tac_timeout);
@@ -1716,8 +1782,8 @@
         (x as (s, _)) =
   case triple_lookup (const_match thy) wfs x of
     SOME (SOME b) => b
-  | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'}
-         orelse case AList.lookup (op =) (!wf_cache) x of
+  | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse
+         case AList.lookup (op =) (!wf_cache) x of
                   SOME (_, wf) => wf
                 | NONE =>
                   let
@@ -1859,8 +1925,8 @@
   in
     if is_equational_fun ext_ctxt x' then
       unrolled_const (* already done *)
-    else if not gfp andalso is_linear_inductive_pred_def def
-         andalso star_linear_preds then
+    else if not gfp andalso is_linear_inductive_pred_def def andalso
+         star_linear_preds then
       starred_linear_pred_const ext_ctxt x def
     else
       let
@@ -1980,10 +2046,10 @@
   let val t_comb = list_comb (t, args) in
     case t of
       Const x =>
-      if not relax andalso is_constr thy x
-         andalso not (is_fun_type (fastype_of1 (Ts, t_comb)))
-         andalso has_heavy_bounds_or_vars Ts level t_comb
-         andalso not (loose_bvar (t_comb, level)) then
+      if not relax andalso is_constr thy x andalso
+         not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
+         has_heavy_bounds_or_vars Ts level t_comb andalso
+         not (loose_bvar (t_comb, level)) then
         let
           val (j, seen) = case find_index (curry (op =) t_comb) seen of
                             ~1 => (0, t_comb :: seen)
@@ -2062,18 +2128,17 @@
     and aux_eq careful pass1 t0 t1 t2 =
       (if careful then
          raise SAME ()
-       else if axiom andalso is_Var t2
-               andalso num_occs_of_var (dest_Var t2) = 1 then
+       else if axiom andalso is_Var t2 andalso
+               num_occs_of_var (dest_Var t2) = 1 then
          @{const True}
        else case strip_comb t2 of
          (Const (x as (s, T)), args) =>
          let val arg_Ts = binder_types T in
-           if length arg_Ts = length args
-              andalso (is_constr thy x orelse s = @{const_name Pair}
-                       orelse x = (@{const_name Suc}, nat_T --> nat_T))
-              andalso (not careful orelse not (is_Var t1)
-                       orelse String.isPrefix val_var_prefix
-                                              (fst (fst (dest_Var t1)))) then
+           if length arg_Ts = length args andalso
+              (is_constr thy x orelse s = @{const_name Pair} orelse
+               x = (@{const_name Suc}, nat_T --> nat_T)) andalso
+              (not careful orelse not (is_Var t1) orelse
+               String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
              discriminate_value ext_ctxt x t1 ::
              map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
              |> foldr1 s_conj
@@ -2095,8 +2160,8 @@
   let
     (* term -> int -> term *)
     fun is_nth_sel_on t' n (Const (s, _) $ t) =
-        (t = t' andalso is_sel_like_and_no_discr s
-         andalso sel_no_from_name s = n)
+        (t = t' andalso is_sel_like_and_no_discr s andalso
+         sel_no_from_name s = n)
       | is_nth_sel_on _ _ _ = false
     (* term -> term list -> term *)
     fun do_term (Const (@{const_name Rep_Frac}, _)
@@ -2109,9 +2174,9 @@
             if length args = num_binder_types T then
               case hd args of
                 Const (x' as (_, T')) $ t' =>
-                if domain_type T' = body_type T
-                   andalso forall (uncurry (is_nth_sel_on t'))
-                                  (index_seq 0 (length args) ~~ args) then
+                if domain_type T' = body_type T andalso
+                   forall (uncurry (is_nth_sel_on t'))
+                          (index_seq 0 (length args) ~~ args) then
                   t'
                 else
                   raise SAME ()
@@ -2121,9 +2186,9 @@
           else if is_sel_like_and_no_discr s then
             case strip_comb (hd args) of
               (Const (x' as (s', T')), ts') =>
-              if is_constr_like thy x'
-                 andalso constr_name_for_sel_like s = s'
-                 andalso not (exists is_pair_type (binder_types T')) then
+              if is_constr_like thy x' andalso
+                 constr_name_for_sel_like s = s' andalso
+                 not (exists is_pair_type (binder_types T')) then
                 list_comb (nth ts' (sel_no_from_name s), tl args)
               else
                 raise SAME ()
@@ -2164,8 +2229,8 @@
     (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
        -> term -> term *)
     and aux_eq prems zs z t' t1 t2 =
-      if not (member (op =) zs z)
-         andalso not (exists_subterm (curry (op =) (Var z)) t') then
+      if not (member (op =) zs z) andalso
+         not (exists_subterm (curry (op =) (Var z)) t') then
         aux prems zs (subst_free [(Var z, t')] t2)
       else
         aux (t1 :: prems) (Term.add_vars t1 zs) t2
@@ -2323,8 +2388,8 @@
          (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
          if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then
            aux s0 (s1 :: ss) (T1 :: Ts) t1
-         else if quant_s = "" andalso (s0 = @{const_name All}
-                                       orelse s0 = @{const_name Ex}) then
+         else if quant_s = "" andalso
+                 (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
            aux s0 [s1] [T1] t1
          else
            raise SAME ()
@@ -2402,8 +2467,8 @@
 
 (* polarity -> string -> bool *)
 fun is_positive_existential polar quant_s =
-  (polar = Pos andalso quant_s = @{const_name Ex})
-  orelse (polar = Neg andalso quant_s <> @{const_name Ex})
+  (polar = Pos andalso quant_s = @{const_name Ex}) orelse
+  (polar = Neg andalso quant_s <> @{const_name Ex})
 
 (* extended_context -> int -> term -> term *)
 fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...})
@@ -2418,8 +2483,8 @@
         fun do_quantifier quant_s quant_T abs_s abs_T t =
           if not (loose_bvar1 (t, 0)) then
             aux ss Ts js depth polar (incr_boundvars ~1 t)
-          else if depth <= skolem_depth
-                  andalso is_positive_existential polar quant_s then
+          else if depth <= skolem_depth andalso
+                  is_positive_existential polar quant_s then
             let
               val j = length (!skolems) + 1
               val sko_s = skolem_prefix_for (length js) j ^ abs_s
@@ -2469,8 +2534,8 @@
         | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
           t0 $ t1 $ aux ss Ts js depth polar t2
         | Const (x as (s, T)) =>
-          if is_inductive_pred ext_ctxt x
-             andalso not (is_well_founded_inductive_pred ext_ctxt x) then
+          if is_inductive_pred ext_ctxt x andalso
+             not (is_well_founded_inductive_pred ext_ctxt x) then
             let
               val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
               val (pref, connective, set_oper) =
@@ -2582,9 +2647,9 @@
 (* typ list -> term -> bool *)
 fun is_eligible_arg Ts t =
   let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
-    null bad_Ts
-    orelse (is_higher_order_type (fastype_of1 (Ts, t))
-            andalso forall (not o is_higher_order_type) bad_Ts)
+    null bad_Ts orelse
+    (is_higher_order_type (fastype_of1 (Ts, t)) andalso
+     forall (not o is_higher_order_type) bad_Ts)
   end
 
 (* (int * term option) list -> (int * term) list -> int list *)
@@ -2608,9 +2673,9 @@
                       else case term_under_def t of Const x => [x] | _ => []
       (* term list -> typ list -> term -> term *)
       fun aux args Ts (Const (x as (s, T))) =
-          ((if not (member (op =) blacklist x) andalso not (null args)
-               andalso not (String.isPrefix special_prefix s)
-               andalso is_equational_fun ext_ctxt x then
+          ((if not (member (op =) blacklist x) andalso not (null args) andalso
+               not (String.isPrefix special_prefix s) andalso
+               is_equational_fun ext_ctxt x then
               let
                 val eligible_args = filter (is_eligible_arg Ts o snd)
                                            (index_seq 0 (length args) ~~ args)
@@ -2678,8 +2743,8 @@
         let val table = aux t2 [] table in aux t1 (t2 :: args) table end
       | aux (Abs (_, _, t')) _ table = aux t' [] table
       | aux (t as Const (x as (s, _))) args table =
-        if is_built_in_const true x orelse is_constr_like thy x orelse is_sel s
-           orelse s = @{const_name Sigma} then
+        if is_built_in_const true x orelse is_constr_like thy x orelse
+           is_sel s orelse s = @{const_name Sigma} then
           table
         else
           Termtab.map_default (t, 65536) (curry Int.min (length args)) table
@@ -2699,8 +2764,8 @@
              let
                val (arg_Ts, rest_T) = strip_n_binders n T
                val j =
-                 if hd arg_Ts = @{typ bisim_iterator}
-                    orelse is_fp_iterator_type (hd arg_Ts) then
+                 if hd arg_Ts = @{typ bisim_iterator} orelse
+                    is_fp_iterator_type (hd arg_Ts) then
                    1
                  else case find_index (not_equal bool_T) arg_Ts of
                    ~1 => n
@@ -2766,8 +2831,8 @@
                                \coerce_term", [t']))
         | (Type (new_s, new_Ts as [new_T1, new_T2]),
            Type (old_s, old_Ts as [old_T1, old_T2])) =>
-          if old_s = @{type_name fun_box} orelse old_s = @{type_name pair_box}
-             orelse old_s = "*" then
+          if old_s = @{type_name fun_box} orelse
+             old_s = @{type_name pair_box} orelse old_s = "*" then
             case constr_expand ext_ctxt old_T t of
               Const (@{const_name FunBox}, _) $ t1 =>
               if new_s = "fun" then
@@ -2881,13 +2946,17 @@
         $ do_term new_Ts old_Ts polar t2
       | Const (s as @{const_name The}, T) => do_description_operator s T
       | Const (s as @{const_name Eps}, T) => do_description_operator s T
+      | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
+        let val T' = box_type ext_ctxt InFunRHS1 T2 in
+          Const (@{const_name quot_normal}, T' --> T')
+        end
       | Const (s as @{const_name Tha}, T) => do_description_operator s T
       | Const (x as (s, T)) =>
-        Const (s, if s = @{const_name converse}
-                     orelse s = @{const_name trancl} then
+        Const (s, if s = @{const_name converse} orelse
+                     s = @{const_name trancl} then
                     box_relational_operator_type T
-                  else if is_built_in_const fast_descrs x
-                          orelse s = @{const_name Sigma} then
+                  else if is_built_in_const fast_descrs x orelse
+                          s = @{const_name Sigma} then
                     T
                   else if is_constr_like thy x then
                     box_type ext_ctxt InConstr T
@@ -2972,7 +3041,7 @@
                             |> map Logic.mk_equals,
                         Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
                                          list_comb (Const x2, bounds2 @ args2)))
-    |> Refute.close_form
+    |> Refute.close_form (* TODO: needed? *)
   end
 
 (* extended_context -> styp list -> term list *)
@@ -3078,23 +3147,29 @@
                fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
                     accum
              else if is_abs_fun thy x then
-               accum |> fold (add_nondef_axiom depth)
-                             (nondef_props_for_const thy false nondef_table x)
-                     |> is_funky_typedef thy (range_type T)
-                        ? fold (add_maybe_def_axiom depth)
-                               (nondef_props_for_const thy true
+               if is_quot_type thy (range_type T) then
+                 raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
+               else
+                 accum |> fold (add_nondef_axiom depth)
+                               (nondef_props_for_const thy false nondef_table x)
+                       |> is_funky_typedef thy (range_type T)
+                          ? fold (add_maybe_def_axiom depth)
+                                 (nondef_props_for_const thy true
                                                     (extra_table def_table s) x)
              else if is_rep_fun thy x then
-               accum |> fold (add_nondef_axiom depth)
-                             (nondef_props_for_const thy false nondef_table x)
-                     |> is_funky_typedef thy (range_type T)
-                        ? fold (add_maybe_def_axiom depth)
-                               (nondef_props_for_const thy true
+               if is_quot_type thy (domain_type T) then
+                 raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
+               else
+                 accum |> fold (add_nondef_axiom depth)
+                               (nondef_props_for_const thy false nondef_table x)
+                       |> is_funky_typedef thy (range_type T)
+                          ? fold (add_maybe_def_axiom depth)
+                                 (nondef_props_for_const thy true
                                                     (extra_table def_table s) x)
-                     |> add_axioms_for_term depth
-                                            (Const (mate_of_rep_fun thy x))
-                     |> fold (add_def_axiom depth)
-                             (inverse_axioms_for_rep_fun thy x)
+                       |> add_axioms_for_term depth
+                                              (Const (mate_of_rep_fun thy x))
+                       |> fold (add_def_axiom depth)
+                               (inverse_axioms_for_rep_fun thy x)
              else
                accum |> user_axioms <> SOME false
                         ? fold (add_nondef_axiom depth)
@@ -3116,10 +3191,12 @@
       | @{typ unit} => I
       | TFree (_, S) => add_axioms_for_sort depth T S
       | TVar (_, S) => add_axioms_for_sort depth T S
-      | Type (z as (_, Ts)) =>
+      | Type (z as (s, Ts)) =>
         fold (add_axioms_for_type depth) Ts
         #> (if is_pure_typedef thy T then
               fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
+            else if is_quot_type thy T then
+              fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
             else if max_bisim_depth >= 0 andalso is_codatatype thy T then
               fold (add_maybe_def_axiom depth)
                    (codatatype_bisim_axioms ext_ctxt T)
@@ -3364,11 +3441,11 @@
     member (op =) [@{const_name times_nat_inst.times_nat},
                    @{const_name div_nat_inst.div_nat},
                    @{const_name times_int_inst.times_int},
-                   @{const_name div_int_inst.div_int}] s
-    orelse (String.isPrefix numeral_prefix s andalso
-            let val n = the (Int.fromString (unprefix numeral_prefix s)) in
-              n <= ~ binary_int_threshold orelse n >= binary_int_threshold
-            end)
+                   @{const_name div_int_inst.div_int}] s orelse
+    (String.isPrefix numeral_prefix s andalso
+     let val n = the (Int.fromString (unprefix numeral_prefix s)) in
+       n <= ~ binary_int_threshold orelse n >= binary_int_threshold
+     end)
   | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
   | should_use_binary_ints _ = false
 
@@ -3398,8 +3475,8 @@
         SOME false => false
       | _ =>
         forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
-        (binary_ints = SOME true
-         orelse exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
+        (binary_ints = SOME true orelse
+         exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
     val box = exists (not_equal (SOME false) o snd) boxes
     val table =
       Termtab.empty |> uncurry
diff -r 440605046777 -r fb90752a9271 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Jan 20 10:38:19 2010 +0100
@@ -106,12 +106,12 @@
 
 (* string -> bool *)
 fun is_known_raw_param s =
-  AList.defined (op =) default_default_params s
-  orelse AList.defined (op =) negated_params s
-  orelse s = "max" orelse s = "eval" orelse s = "expect"
-  orelse exists (fn p => String.isPrefix (p ^ " ") s)
-                ["card", "max", "iter", "box", "dont_box", "mono", "non_mono",
-                 "wf", "non_wf", "format"]
+  AList.defined (op =) default_default_params s orelse
+  AList.defined (op =) negated_params s orelse
+  s = "max" orelse s = "eval" orelse s = "expect" orelse
+  exists (fn p => String.isPrefix (p ^ " ") s)
+         ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "wf",
+          "non_wf", "format"]
 
 (* string * 'a -> unit *)
 fun check_raw_param (s, _) =
diff -r 440605046777 -r fb90752a9271 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Jan 20 10:38:19 2010 +0100
@@ -380,8 +380,8 @@
         val one = is_one_rep body_R
         val opt_x = case r of KK.Rel x => SOME x | _ => NONE
       in
-        if opt_x <> NONE andalso length binder_schema = 1
-           andalso length body_schema = 1 then
+        if opt_x <> NONE andalso length binder_schema = 1 andalso
+           length body_schema = 1 then
           (if one then KK.Function else KK.Functional)
               (the opt_x, KK.AtomSeq (hd binder_schema),
                KK.AtomSeq (hd body_schema))
@@ -490,8 +490,8 @@
     r
   else
     let val card = card_of_rep old_R in
-      if is_lone_rep old_R andalso is_lone_rep new_R
-         andalso card = card_of_rep new_R then
+      if is_lone_rep old_R andalso is_lone_rep new_R andalso
+         card = card_of_rep new_R then
         if card >= lone_rep_fallback_max_card then
           raise TOO_LARGE ("Nitpick_Kodkod.lone_rep_fallback",
                            "too high cardinality (" ^ string_of_int card ^ ")")
@@ -1005,13 +1005,13 @@
          | Op1 (Finite, _, _, u1) =>
            let val opt1 = is_opt_rep (rep_of u1) in
              case polar of
-               Neut => if opt1 then
-                         raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
-                       else
-                         KK.True
+               Neut =>
+               if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
+               else KK.True
              | Pos => formula_for_bool (not opt1)
              | Neg => KK.True
            end
+         | Op1 (IsUnknown, _, _, u1) => kk_no (to_r u1)
          | Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1
          | Op2 (All, _, _, u1, u2) =>
            kk_all (untuple to_decl u1) (to_f_with_polarity polar u2)
@@ -1070,8 +1070,8 @@
                   | args _ = []
                 val opt_arg_us = filter (is_opt_rep o rep_of) (args u1)
               in
-                if null opt_arg_us orelse not (is_Opt min_R)
-                   orelse is_eval_name u1 then
+                if null opt_arg_us orelse not (is_Opt min_R) orelse
+                   is_eval_name u1 then
                   fold (kk_or o (kk_no o to_r)) opt_arg_us
                        (kk_rel_eq (to_rep min_R u1) (to_rep min_R u2))
                 else
@@ -1100,8 +1100,8 @@
                     (if polar = Pos then
                        if not both_opt then
                          kk_rel_eq r1 r2
-                       else if is_lone_rep min_R
-                               andalso arity_of_rep min_R = 1 then
+                       else if is_lone_rep min_R andalso
+                               arity_of_rep min_R = 1 then
                          kk_some (kk_intersect r1 r2)
                        else
                          raise SAME ()
@@ -1132,9 +1132,9 @@
                       val rs1 = unpack_products r1
                       val rs2 = unpack_products r2
                     in
-                      if length rs1 = length rs2
-                         andalso map KK.arity_of_rel_expr rs1
-                                 = map KK.arity_of_rel_expr rs2 then
+                      if length rs1 = length rs2 andalso
+                         map KK.arity_of_rel_expr rs1
+                         = map KK.arity_of_rel_expr rs2 then
                         fold1 kk_and (map2 kk_subset rs1 rs2)
                       else
                         kk_subset r1 r2
@@ -1582,8 +1582,8 @@
         else
           fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel)
       | Op2 (Apply, _, R, u1, u2) =>
-        if is_Cst Unrep u2 andalso is_set_type (type_of u1)
-           andalso is_FreeName u1 then
+        if is_Cst Unrep u2 andalso is_set_type (type_of u1) andalso
+           is_FreeName u1 then
           false_atom
         else
           to_apply R u1 u2
diff -r 440605046777 -r fb90752a9271 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jan 20 10:38:19 2010 +0100
@@ -440,7 +440,9 @@
                       | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
                                          \for_atom (Abs_Frac)", ts)
                     end
-                  else if not for_auto andalso is_abs_fun thy constr_x then
+                  else if not for_auto andalso
+                          (is_abs_fun thy constr_x orelse
+                           constr_s = @{const_name Quot}) then
                     Const (abs_name, constr_T) $ the_single ts
                   else
                     list_comb (Const constr_x, ts)
@@ -560,8 +562,8 @@
             pairself (strip_comb o unfold_outer_the_binders) (t1, t2)
           val max_depth = max_depth - (if member (op =) coTs T then 1 else 0)
         in
-          head1 = head2
-          andalso forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
+          head1 = head2 andalso
+          forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
         end
       else
         t1 = t2
@@ -704,8 +706,8 @@
   in
     (Pretty.chunks (if null chunks then [Pretty.str "Empty assignment"]
                     else chunks),
-     bisim_depth >= 0
-     orelse forall (is_codatatype_wellformed codatatypes) codatatypes)
+     bisim_depth >= 0 orelse
+     forall (is_codatatype_wellformed codatatypes) codatatypes)
   end
 
 (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
diff -r 440605046777 -r fb90752a9271 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Jan 20 10:38:19 2010 +0100
@@ -121,8 +121,8 @@
 
 (* typ -> typ -> bool *)
 fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
-    T = alpha_T orelse (not (is_fp_iterator_type T)
-                        andalso exists (could_exist_alpha_subtype alpha_T) Ts)
+    T = alpha_T orelse (not (is_fp_iterator_type T) andalso
+                        exists (could_exist_alpha_subtype alpha_T) Ts)
   | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
 (* theory -> typ -> typ -> bool *)
 fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
@@ -195,8 +195,8 @@
       let
         val C1 = do_type T1
         val C2 = do_type T2
-        val a = if is_boolean_type (body_type T2)
-                   andalso exists_alpha_sub_ctype_fresh C1 then
+        val a = if is_boolean_type (body_type T2) andalso
+                   exists_alpha_sub_ctype_fresh C1 then
                   V (Unsynchronized.inc max_fresh)
                 else
                   S Neg
diff -r 440605046777 -r fb90752a9271 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Jan 20 10:38:19 2010 +0100
@@ -39,6 +39,7 @@
     Converse |
     Closure |
     SingletonSet |
+    IsUnknown |
     Tha |
     First |
     Second |
@@ -158,6 +159,7 @@
   Converse |
   Closure |
   SingletonSet |
+  IsUnknown |
   Tha |
   First |
   Second |
@@ -231,6 +233,7 @@
   | string_for_op1 Converse = "Converse"
   | string_for_op1 Closure = "Closure"
   | string_for_op1 SingletonSet = "SingletonSet"
+  | string_for_op1 IsUnknown = "IsUnknown"
   | string_for_op1 Tha = "Tha"
   | string_for_op1 First = "First"
   | string_for_op1 Second = "Second"
@@ -567,7 +570,6 @@
                sub t1, sub_abs s T' t2)
         | (t0 as Const (@{const_name Let}, T), [t1, t2]) =>
           sub (t0 $ t1 $ eta_expand Ts t2 1)
-        | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
         | (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any)
         | (Const (@{const_name Pair}, T), [t1, t2]) =>
           Tuple (nth_range_type 2 T, Any, map sub [t1, t2])
@@ -641,6 +643,9 @@
           Op2 (Less, bool_T, Any, sub t1, sub t2)
         | (Const (@{const_name ord_int_inst.less_eq_int}, T), [t1, t2]) =>
           Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
+        | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
+        | (Const (@{const_name is_unknown}, T), [t1]) =>
+          Op1 (IsUnknown, bool_T, Any, sub t1)
         | (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>
           Op1 (Tha, T2, Any, sub t1)
         | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
@@ -715,12 +720,12 @@
                rep_for_abs_fun
              else if is_rep_fun thy x then
                Func oo best_non_opt_symmetric_reps_for_fun_type
-             else if all_exact orelse is_skolem_name v
-                     orelse member (op =) [@{const_name undefined_fast_The},
-                                           @{const_name undefined_fast_Eps},
-                                           @{const_name bisim},
-                                           @{const_name bisim_iterator_max}]
-                                          (original_name s) then
+             else if all_exact orelse is_skolem_name v orelse
+                    member (op =) [@{const_name undefined_fast_The},
+                                   @{const_name undefined_fast_Eps},
+                                   @{const_name bisim},
+                                   @{const_name bisim_iterator_max}]
+                           (original_name s) then
                best_non_opt_set_rep_for_type
              else if member (op =) [@{const_name set}, @{const_name distinct},
                                     @{const_name ord_class.less},
@@ -746,9 +751,9 @@
                                       (vs, table) =
   let
     val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n
-    val R' = if n = ~1 orelse is_word_type (body_type T)
-                orelse (is_fun_type (range_type T')
-                        andalso is_boolean_type (body_type T')) then
+    val R' = if n = ~1 orelse is_word_type (body_type T) orelse
+                (is_fun_type (range_type T') andalso
+                 is_boolean_type (body_type T')) then
                best_non_opt_set_rep_for_type scope T'
              else
                best_opt_set_rep_for_type scope T' |> unopt_rep
@@ -798,10 +803,8 @@
   if rep_of u = Unit then Cst (Unity, type_of u, Unit) else u
 (* typ -> rep -> nut *)
 fun unknown_boolean T R =
-  Cst (case R of
-         Formula Pos => False
-       | Formula Neg => True
-       | _ => Unknown, T, R)
+  Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
+       T, R)
 
 (* op1 -> typ -> rep -> nut -> nut *)
 fun s_op1 oper T R u1 =
@@ -954,19 +957,18 @@
             let
               val T1 = domain_type T
               val R1 = Atom (spec_of_type scope T1)
-              val total = T1 = nat_T
-                          andalso (cst = Subtract orelse cst = Divide
-                                   orelse cst = Gcd)
+              val total = T1 = nat_T andalso
+                          (cst = Subtract orelse cst = Divide orelse cst = Gcd)
             in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end
           else if cst = NatToInt orelse cst = IntToNat then
             let
               val (dom_card, dom_j0) = spec_of_type scope (domain_type T)
               val (ran_card, ran_j0) = spec_of_type scope (range_type T)
-              val total = not (is_word_type (domain_type T))
-                          andalso (if cst = NatToInt then
-                                    max_int_for_card ran_card >= dom_card + 1
-                                  else
-                                    max_int_for_card dom_card < ran_card)
+              val total = not (is_word_type (domain_type T)) andalso
+                          (if cst = NatToInt then
+                             max_int_for_card ran_card >= dom_card + 1
+                           else
+                             max_int_for_card dom_card < ran_card)
             in
               Cst (cst, T, Func (Atom (dom_card, dom_j0),
                                  Atom (ran_card, ran_j0) |> not total ? Opt))
@@ -979,6 +981,11 @@
              triad (s_op1 Not T (Formula Pos) u12)
                    (s_op1 Not T (Formula Neg) u11)
            | u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1')
+        | Op1 (IsUnknown, T, _, u1) =>
+          let val u1 = sub u1 in
+            if is_opt_rep (rep_of u1) then Op1 (IsUnknown, T, Formula Neut, u1)
+            else Cst (False, T, Formula Neut)
+          end
         | Op1 (oper, T, _, u1) =>
           let
             val u1 = sub u1
@@ -1029,8 +1036,8 @@
               if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
               else opt_opt_case ()
           in
-            if liberal orelse polar = Neg
-               orelse is_concrete_type datatypes (type_of u1) then
+            if liberal orelse polar = Neg orelse
+               is_concrete_type datatypes (type_of u1) then
               case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
                 (true, true) => opt_opt_case ()
               | (true, false) => hybrid_case u1'
@@ -1108,12 +1115,11 @@
                val u1' = aux table' false Neut u1
                val u2' = aux table' false Neut u2
                val R =
-                 if is_opt_rep (rep_of u2')
-                    orelse (range_type T = bool_T andalso
-                            not (is_Cst False
-                                        (unrepify_nut_in_nut table false Neut
-                                                             u1 u2
-                                         |> optimize_nut))) then
+                 if is_opt_rep (rep_of u2') orelse
+                    (range_type T = bool_T andalso
+                     not (is_Cst False (unrepify_nut_in_nut table false Neut
+                                                            u1 u2
+                                        |> optimize_nut))) then
                    opt_rep ofs T R
                  else
                    unopt_rep R
@@ -1131,9 +1137,9 @@
                 triad_fn (fn polar => gsub def polar u)
               else
                 let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
-                  if def
-                     orelse (liberal andalso (polar = Pos) = (oper = All))
-                     orelse is_complete_type datatypes (type_of u1) then
+                  if def orelse
+                     (liberal andalso (polar = Pos) = (oper = All)) orelse
+                     is_complete_type datatypes (type_of u1) then
                     quant_u
                   else
                     let
@@ -1231,8 +1237,8 @@
           in Construct (map sub us', T, R |> opt ? Opt, us) end
         | _ =>
           let val u = modify_name_rep u (the_name table u) in
-            if polar = Neut orelse not (is_boolean_type (type_of u))
-               orelse not (is_opt_rep (rep_of u)) then
+            if polar = Neut orelse not (is_boolean_type (type_of u)) orelse
+               not (is_opt_rep (rep_of u)) then
               u
             else
               s_op1 Cast (type_of u) (Formula polar) u
diff -r 440605046777 -r fb90752a9271 src/HOL/Tools/Nitpick/nitpick_peephole.ML
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Wed Jan 20 10:38:19 2010 +0100
@@ -421,8 +421,8 @@
         if is_one_rel_expr r1 then
           s_or (s_subset r1 r21) (s_subset r1 r22)
         else
-          if s_subset r1 r21 = True orelse s_subset r1 r22 = True
-             orelse r1 = r2 then
+          if s_subset r1 r21 = True orelse s_subset r1 r22 = True orelse
+             r1 = r2 then
             True
           else
             Subset (r1, r2)
diff -r 440605046777 -r fb90752a9271 src/HOL/Tools/Nitpick/nitpick_rep.ML
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Wed Jan 20 10:38:19 2010 +0100
@@ -274,8 +274,8 @@
      | (R1, R2) => Struct [R1, R2])
   | best_one_rep_for_type (scope as {card_assigns, datatypes, ofs, ...}) T =
     (case card_of_type card_assigns T of
-       1 => if is_some (datatype_spec datatypes T)
-               orelse is_fp_iterator_type T then
+       1 => if is_some (datatype_spec datatypes T) orelse
+               is_fp_iterator_type T then
               Atom (1, offset_of_type ofs T)
             else
               Unit
diff -r 440605046777 -r fb90752a9271 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Jan 20 10:38:19 2010 +0100
@@ -107,8 +107,8 @@
   | is_complete_type dtypes (Type ("*", Ts)) =
     forall (is_complete_type dtypes) Ts
   | is_complete_type dtypes T =
-    not (is_integer_type T) andalso not (is_bit_type T)
-    andalso #complete (the (datatype_spec dtypes T))
+    not (is_integer_type T) andalso not (is_bit_type T) andalso
+    #complete (the (datatype_spec dtypes T))
     handle Option.Option => true
 and is_concrete_type dtypes (Type ("fun", [T1, T2])) =
     is_complete_type dtypes T1 andalso is_concrete_type dtypes T2
@@ -427,8 +427,8 @@
           {delta = delta, epsilon = delta, exclusive = true, total = false}
         end
       else if not co andalso num_self_recs > 0 then
-        if not self_rec andalso num_non_self_recs = 1
-           andalso domain_card 2 card_assigns T = 1 then
+        if not self_rec andalso num_non_self_recs = 1 andalso
+           domain_card 2 card_assigns T = 1 then
           {delta = 0, epsilon = 1, exclusive = (s = @{const_name Nil}),
            total = true}
         else if s = @{const_name Cons} then
diff -r 440605046777 -r fb90752a9271 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Jan 20 10:38:19 2010 +0100
@@ -285,8 +285,8 @@
 (* string -> string *)
 fun maybe_quote y =
   let val s = plain_string_from_yxml y in
-    y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s))
-          orelse OuterKeyword.is_keyword s) ? quote
+    y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s)) orelse
+          OuterKeyword.is_keyword s) ? quote
   end
 
 end;