1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Feb 04 16:50:26 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Fri Feb 05 11:14:34 2010 +0100
     1.3 @@ -1694,7 +1694,7 @@
     1.4  ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
     1.5  ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
     1.6  \textbf{nitpick} \\[2\smallskipamount]
     1.7 -{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
     1.8 +{\slshape Nitpick found no counterexample.}
     1.9  \postw
    1.10  
    1.11  Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
    1.12 @@ -1756,7 +1756,7 @@
    1.13  \prew
    1.14  \textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
    1.15  \textbf{nitpick} \\[2\smallskipamount]
    1.16 -{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
    1.17 +{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
    1.18  \postw
    1.19  
    1.20  Insertion should transform the set of elements represented by the tree in the
    1.21 @@ -1766,14 +1766,14 @@
    1.22  \textbf{theorem} \textit{dataset\_insort}:\kern.4em
    1.23  ``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
    1.24  \textbf{nitpick} \\[2\smallskipamount]
    1.25 -{\slshape Nitpick ran out of time after checking 5 of 8 scopes.}
    1.26 +{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
    1.27  \postw
    1.28  
    1.29 -We could continue like this and sketch a complete theory of AA trees without
    1.30 -performing a single proof. Once the definitions and main theorems are in place
    1.31 -and have been thoroughly tested using Nitpick, we could start working on the
    1.32 -proofs. Developing theories this way usually saves time, because faulty theorems
    1.33 -and definitions are discovered much earlier in the process.
    1.34 +We could continue like this and sketch a complete theory of AA trees. Once the
    1.35 +definitions and main theorems are in place and have been thoroughly tested using
    1.36 +Nitpick, we could start working on the proofs. Developing theories this way
    1.37 +usually saves time, because faulty theorems and definitions are discovered much
    1.38 +earlier in the process.
    1.39  
    1.40  \section{Option Reference}
    1.41  \label{option-reference}

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Feb 04 16:50:26 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Feb 05 11:14:34 2010 +0100
     2.3 @@ -316,7 +316,15 @@
     2.4             if R2 = Formula Neut then
     2.5               [ts] |> not exclusive ? cons (KK.TupleSet [])
     2.6             else
     2.7 -             [KK.TupleSet [], KK.TupleProduct (ts, upper_bound_for_rep R2)]
     2.8 +             [KK.TupleSet [],
     2.9 +              if exclusive andalso T1 = T2 andalso epsilon > delta then
    2.10 +                index_seq delta (epsilon - delta)
    2.11 +                |> map (fn j =>
    2.12 +                           KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
    2.13 +                                            KK.TupleAtomSeq (j, j0)))
    2.14 +                |> foldl1 KK.TupleUnion
    2.15 +              else
    2.16 +                KK.TupleProduct (ts, upper_bound_for_rep R2)]
    2.17           end)
    2.18      end
    2.19    | bound_for_sel_rel _ _ _ u =
    2.20 @@ -944,11 +952,11 @@
    2.21  (* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
    2.22  fun kodkod_formula_from_nut bits ofs liberal
    2.23          (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
    2.24 -                kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one,
    2.25 -                kk_some, kk_rel_let, kk_rel_if, kk_union, kk_difference,
    2.26 -                kk_intersect, kk_product, kk_join, kk_closure, kk_comprehension,
    2.27 -                kk_project, kk_project_seq, kk_not3, kk_nat_less, kk_int_less,
    2.28 -                ...}) u =
    2.29 +                kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
    2.30 +                kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
    2.31 +                kk_difference, kk_intersect, kk_product, kk_join, kk_closure,
    2.32 +                kk_comprehension, kk_project, kk_project_seq, kk_not3,
    2.33 +                kk_nat_less, kk_int_less, ...}) u =
    2.34    let
    2.35      val main_j0 = offset_of_type ofs bool_T
    2.36      val bool_j0 = main_j0
    2.37 @@ -1108,7 +1116,7 @@
    2.38                       else
    2.39                         if is_lone_rep min_R then
    2.40                           if arity_of_rep min_R = 1 then
    2.41 -                           kk_subset (kk_product r1 r2) KK.Iden
    2.42 +                           kk_lone (kk_union r1 r2)
    2.43                           else if not both_opt then
    2.44                             (r1, r2) |> is_opt_rep (rep_of u2) ? swap
    2.45                                      |-> kk_subset

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 04 16:50:26 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Feb 05 11:14:34 2010 +0100
     3.3 @@ -426,16 +426,21 @@
     3.4            {delta = delta, epsilon = delta, exclusive = true, total = false}
     3.5          end
     3.6        else if not co andalso num_self_recs > 0 then
     3.7 -        if not self_rec andalso num_non_self_recs = 1 andalso
     3.8 -           domain_card 2 card_assigns T = 1 then
     3.9 -          {delta = 0, epsilon = 1,
    3.10 -           exclusive = (s = @{const_name Nil} andalso length constrs = 2),
    3.11 -           total = true}
    3.12 -        else if s = @{const_name Cons} andalso
    3.13 -                num_self_recs + num_non_self_recs = 2 then
    3.14 -          {delta = 1, epsilon = card, exclusive = true, total = false}
    3.15 -        else
    3.16 -          {delta = 0, epsilon = card, exclusive = false, total = false}
    3.17 +        (if num_self_recs = 1 andalso num_non_self_recs = 1 then
    3.18 +           if self_rec then
    3.19 +             case constrs of
    3.20 +               [{delta = 0, epsilon = 1, exclusive = true, ...}] =>
    3.21 +               {delta = 1, epsilon = card, exclusive = true, total = false}
    3.22 +             | _ => raise SAME ()
    3.23 +           else
    3.24 +             if domain_card 2 card_assigns T = 1 then
    3.25 +               {delta = 0, epsilon = 1, exclusive = true, total = true}
    3.26 +             else
    3.27 +               raise SAME ()
    3.28 +         else
    3.29 +           raise SAME ())
    3.30 +        handle SAME () =>
    3.31 +               {delta = 0, epsilon = card, exclusive = false, total = false}
    3.32        else if card = sum_dom_cards (card + 1) then
    3.33          let val delta = next_delta () in
    3.34            {delta = delta, epsilon = delta + domain_card card card_assigns T,
    3.35 @@ -473,7 +478,8 @@
    3.36        map (domain_card max card_assigns o snd) xs |> Integer.sum
    3.37      val constrs =
    3.38        fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
    3.39 -                                num_non_self_recs) (self_recs ~~ xs) []
    3.40 +                                num_non_self_recs)
    3.41 +               (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
    3.42    in
    3.43      {typ = T, card = card, co = co, complete = complete, concrete = concrete,
    3.44       deep = deep, constrs = constrs}