1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 12 21:27:06 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 13 11:56:06 2010 +0100
     1.3 @@ -53,6 +53,8 @@
     1.4  val base_mixfix = "_\<^bsub>base\<^esub>"
     1.5  val step_mixfix = "_\<^bsub>step\<^esub>"
     1.6  val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
     1.7 +val cyclic_co_val_name = "\<omega>"
     1.8 +val cyclic_non_std_type_name = "\<xi>"
     1.9  val opt_flag = nitpick_prefix ^ "opt"
    1.10  val non_opt_flag = nitpick_prefix ^ "non_opt"
    1.11  
    1.12 @@ -397,7 +399,7 @@
    1.13          else case datatype_spec datatypes T of
    1.14            NONE => nth_atom pool for_auto T j k
    1.15          | SOME {deep = false, ...} => nth_atom pool for_auto T j k
    1.16 -        | SOME {co, constrs, ...} =>
    1.17 +        | SOME {co, standard, constrs, ...} =>
    1.18            let
    1.19              (* styp -> int list *)
    1.20              fun tuples_for_const (s, T) =
    1.21 @@ -428,8 +430,9 @@
    1.22                map (map_filter (fn js => if hd js = real_j then SOME (tl js)
    1.23                                          else NONE)) sel_jsss
    1.24              val uncur_arg_Ts = binder_types constr_T
    1.25 +            val maybe_cyclic = co orelse not standard
    1.26            in
    1.27 -            if co andalso member (op =) seen (T, j) then
    1.28 +            if maybe_cyclic andalso member (op =) seen (T, j) then
    1.29                Var (var ())
    1.30              else if constr_s = @{const_name Word} then
    1.31                HOLogic.mk_number
    1.32 @@ -437,7 +440,7 @@
    1.33                    (value_of_bits (the_single arg_jsss))
    1.34              else
    1.35                let
    1.36 -                val seen = seen |> co ? cons (T, j)
    1.37 +                val seen = seen |> maybe_cyclic ? cons (T, j)
    1.38                  val ts =
    1.39                    if length arg_Ts = 0 then
    1.40                      []
    1.41 @@ -469,19 +472,20 @@
    1.42                            (is_abs_fun thy constr_x orelse
    1.43                             constr_s = @{const_name Quot}) then
    1.44                      Const (abs_name, constr_T) $ the_single ts
    1.45 -                  else if not for_auto andalso
    1.46 -                          constr_s = @{const_name Silly} then
    1.47 -                    Const (fst (dest_Const (the_single ts)), T)
    1.48                    else
    1.49                      list_comb (Const constr_x, ts)
    1.50                in
    1.51 -                if co then
    1.52 +                if maybe_cyclic then
    1.53                    let val var = var () in
    1.54                      if exists_subterm (curry (op =) (Var var)) t then
    1.55 -                      Const (@{const_name The}, (T --> bool_T) --> T)
    1.56 -                      $ Abs ("\<omega>", T,
    1.57 -                             Const (@{const_name "op ="}, T --> T --> bool_T)
    1.58 -                             $ Bound 0 $ abstract_over (Var var, t))
    1.59 +                      if co then
    1.60 +                        Const (@{const_name The}, (T --> bool_T) --> T)
    1.61 +                        $ Abs (cyclic_co_val_name, T,
    1.62 +                               Const (@{const_name "op ="}, T --> T --> bool_T)
    1.63 +                               $ Bound 0 $ abstract_over (Var var, t))
    1.64 +                      else
    1.65 +                        nth_atom pool for_auto
    1.66 +                                 (Type (cyclic_non_std_type_name, [])) j k
    1.67                      else
    1.68                        t
    1.69                    end
    1.70 @@ -682,7 +686,8 @@
    1.71      (* typ -> dtype_spec list *)
    1.72      fun integer_datatype T =
    1.73        [{typ = T, card = card_of_type card_assigns T, co = false,
    1.74 -        complete = false, concrete = true, deep = true, constrs = []}]
    1.75 +        standard = true, complete = false, concrete = true, deep = true,
    1.76 +        constrs = []}]
    1.77        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
    1.78      val (codatatypes, datatypes) =
    1.79        datatypes |> filter #deep |> List.partition #co