1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jun 01 14:14:02 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jun 01 14:54:35 2010 +0200
     1.3 @@ -319,7 +319,7 @@
     1.4      fun nth_value_of_type n =
     1.5        let
     1.6          fun term unfold =
     1.7 -          reconstruct_term unfold pool wacky_names scope atomss sel_names
     1.8 +          reconstruct_term true unfold pool wacky_names scope atomss sel_names
     1.9                             rel_table bounds T T (Atom (card, 0)) [[n]]
    1.10        in
    1.11          case term false of
    1.12 @@ -331,7 +331,8 @@
    1.13          | t => t
    1.14        end
    1.15    in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
    1.16 -and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
    1.17 +and reconstruct_term maybe_opt unfold pool
    1.18 +        (wacky_names as ((maybe_name, abs_name), _))
    1.19          (scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns,
    1.20                     bits, datatypes, ofs, ...})
    1.21          atomss sel_names rel_table bounds =
    1.22 @@ -607,6 +608,7 @@
    1.23        | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
    1.24                       (Func (R1, Formula Neut)) jss =
    1.25          let
    1.26 +val _ = priority ("HERE: " ^ (if maybe_opt then "y" else "n")) (* ### *)
    1.27            val jss1 = all_combinations_for_rep R1
    1.28            val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1
    1.29            val ts2 =
    1.30 @@ -633,7 +635,7 @@
    1.31                     string_of_int (length jss))
    1.32    in
    1.33      postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term
    1.34 -    oooo term_for_rep true []
    1.35 +    oooo term_for_rep maybe_opt []
    1.36    end
    1.37  
    1.38  (** Constant postprocessing **)
    1.39 @@ -830,13 +832,6 @@
    1.40  
    1.41  (** Model reconstruction **)
    1.42  
    1.43 -fun term_for_name pool scope atomss sel_names rel_table bounds name =
    1.44 -  let val T = type_of name in
    1.45 -    tuple_list_for_name rel_table bounds name
    1.46 -    |> reconstruct_term false pool (("", ""), ("", "")) scope atomss sel_names
    1.47 -                        rel_table bounds T T (rep_of name)
    1.48 -  end
    1.49 -
    1.50  fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
    1.51                                     $ Abs (s, T, Const (@{const_name "op ="}, _)
    1.52                                                  $ Bound 0 $ t')) =
    1.53 @@ -890,11 +885,13 @@
    1.54      val scope =
    1.55        {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
    1.56         bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
    1.57 -    fun term_for_rep unfold =
    1.58 -      reconstruct_term unfold pool wacky_names scope atomss sel_names rel_table
    1.59 -                       bounds
    1.60 +    fun term_for_rep maybe_opt unfold =
    1.61 +      reconstruct_term maybe_opt unfold pool wacky_names scope atomss
    1.62 +                       sel_names rel_table bounds
    1.63      fun nth_value_of_type card T n =
    1.64 -      let fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]] in
    1.65 +      let
    1.66 +        fun aux unfold = term_for_rep true unfold T T (Atom (card, 0)) [[n]]
    1.67 +      in
    1.68          case aux false of
    1.69            t as Const (s, _) =>
    1.70            if String.isPrefix (cyclic_const_prefix ()) s then
    1.71 @@ -932,7 +929,8 @@
    1.72                     Const (@{const_name undefined}, T')
    1.73                   else
    1.74                     tuple_list_for_name rel_table bounds name
    1.75 -                   |> term_for_rep false T T' (rep_of name)
    1.76 +                   |> term_for_rep (not (is_fully_representable_set name)) false
    1.77 +                                   T T' (rep_of name)
    1.78        in
    1.79          Pretty.block (Pretty.breaks
    1.80              [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
    1.81 @@ -1011,6 +1009,14 @@
    1.82       forall (is_codatatype_wellformed codatatypes) codatatypes)
    1.83    end
    1.84  
    1.85 +fun term_for_name pool scope atomss sel_names rel_table bounds name =
    1.86 +  let val T = type_of name in
    1.87 +    tuple_list_for_name rel_table bounds name
    1.88 +    |> reconstruct_term (not (is_fully_representable_set name)) false pool
    1.89 +                        (("", ""), ("", "")) scope atomss sel_names rel_table
    1.90 +                        bounds T T (rep_of name)
    1.91 +  end
    1.92 +
    1.93  fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
    1.94                                 card_assigns, ...})
    1.95                      auto_timeout free_names sel_names rel_table bounds prop =

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jun 01 14:14:02 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jun 01 14:54:35 2010 +0200
     2.3 @@ -105,6 +105,7 @@
     2.4    val the_name : 'a NameTable.table -> nut -> 'a
     2.5    val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
     2.6    val nut_from_term : hol_context -> op2 -> term -> nut
     2.7 +  val is_fully_representable_set : nut -> bool
     2.8    val choose_reps_for_free_vars :
     2.9      scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
    2.10    val choose_reps_for_consts :
    2.11 @@ -677,6 +678,23 @@
    2.12        end
    2.13    in aux eq [] [] end
    2.14  
    2.15 +fun is_fully_representable_set u =
    2.16 +  not (is_opt_rep (rep_of u)) andalso
    2.17 +  case u of
    2.18 +    FreeName _ => true
    2.19 +  | Op1 (SingletonSet, _, _, _) => true
    2.20 +  | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
    2.21 +  | Op2 (oper, _, _, u1, u2) =>
    2.22 +    if oper = Union orelse oper = SetDifference orelse oper = Intersect then
    2.23 +      forall is_fully_representable_set [u1, u2]
    2.24 +    else if oper = Apply then
    2.25 +      case u1 of
    2.26 +        ConstName (s, _, _) => is_sel_like_and_no_discr s
    2.27 +      | _ => false
    2.28 +    else
    2.29 +      false
    2.30 +  | _ => false
    2.31 +
    2.32  fun rep_for_abs_fun scope T =
    2.33    let val (R1, R2) = best_non_opt_symmetric_reps_for_fun_type scope T in
    2.34      Func (R1, (card_of_rep R1 <> card_of_rep R2 ? Opt) R2)
    2.35 @@ -766,22 +784,6 @@
    2.36  fun unknown_boolean T R =
    2.37    Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
    2.38         T, R)
    2.39 -fun is_fully_representable_set u =
    2.40 -  not (is_opt_rep (rep_of u)) andalso
    2.41 -  case u of
    2.42 -    FreeName _ => true
    2.43 -  | Op1 (SingletonSet, _, _, _) => true
    2.44 -  | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
    2.45 -  | Op2 (oper, _, _, u1, u2) =>
    2.46 -    if oper = Union orelse oper = SetDifference orelse oper = Intersect then
    2.47 -      forall is_fully_representable_set [u1, u2]
    2.48 -    else if oper = Apply then
    2.49 -      case u1 of
    2.50 -        ConstName (s, _, _) => is_sel_like_and_no_discr s
    2.51 -      | _ => false
    2.52 -    else
    2.53 -      false
    2.54 -  | _ => false
    2.55  
    2.56  fun s_op1 oper T R u1 =
    2.57    ((if oper = Not then