first step towards extending Minipick with more translations
authorblanchet
Fri Sep 23 14:25:53 2011 +0200 (2011-09-23)
changeset 450629598cada31b3
parent 45061 39519609abe0
child 45063 b3b50d8b535a
first step towards extending Minipick with more translations
src/HOL/Nitpick_Examples/Mini_Nits.thy
src/HOL/Nitpick_Examples/minipick.ML
     1.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Fri Sep 23 14:08:50 2011 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Fri Sep 23 14:25:53 2011 +0200
     1.3 @@ -12,22 +12,16 @@
     1.4  uses "minipick.ML"
     1.5  begin
     1.6  
     1.7 -ML {*
     1.8 -exception FAIL
     1.9 +nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1]
    1.10  
    1.11 -val has_kodkodi = (getenv "KODKODI" <> "")
    1.12 +nitpick_params [total_consts = smart]
    1.13  
    1.14 -fun minipick n t =
    1.15 -  map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n)
    1.16 -  |> Minipick.solve_any_kodkod_problem @{theory}
    1.17 -fun minipick_expect expect n t =
    1.18 -  if has_kodkodi then
    1.19 -    if minipick n t = expect then () else raise FAIL
    1.20 -  else
    1.21 -    ()
    1.22 -val none = minipick_expect "none"
    1.23 -val genuine = minipick_expect "genuine"
    1.24 -val unknown = minipick_expect "unknown"
    1.25 +ML {*
    1.26 +val check = Minipick.minipick @{context}
    1.27 +val expect = Minipick.minipick_expect @{context}
    1.28 +val none = expect "none"
    1.29 +val genuine = expect "genuine"
    1.30 +val unknown = expect "unknown"
    1.31  *}
    1.32  
    1.33  ML {* genuine 1 @{prop "x = Not"} *}
    1.34 @@ -43,7 +37,6 @@
    1.35  ML {* none 5 @{prop "\<exists>x. x = x"} *}
    1.36  ML {* none 1 @{prop "\<forall>x. x = y"} *}
    1.37  ML {* genuine 2 @{prop "\<forall>x. x = y"} *}
    1.38 -ML {* none 1 @{prop "\<exists>x. x = y"} *}
    1.39  ML {* none 2 @{prop "\<exists>x. x = y"} *}
    1.40  ML {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
    1.41  ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
    1.42 @@ -74,6 +67,9 @@
    1.43  ML {* genuine 2 @{prop "{a} = {a, b}"} *}
    1.44  ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
    1.45  ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
    1.46 +ML {* none 5 @{prop "UNIV\<^sup>+ = UNIV"} *}
    1.47 +ML {* none 5 @{prop "(UNIV\<Colon>'a \<times> 'b \<Rightarrow> bool) - {} = UNIV"} *}
    1.48 +ML {* none 5 @{prop "{} - (UNIV\<Colon>'a \<times> 'b \<Rightarrow> bool) = {}"} *}
    1.49  ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.50  ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.51  ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.52 @@ -93,6 +89,8 @@
    1.53  ML {* none 1 @{prop "fst (a, b) = b"} *}
    1.54  ML {* genuine 2 @{prop "fst (a, b) = b"} *}
    1.55  ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
    1.56 +ML {* genuine 2 @{prop "f ((x, z), y) = (x, z)"} *}
    1.57 +ML {* none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"} *}
    1.58  ML {* none 5 @{prop "snd (a, b) = b"} *}
    1.59  ML {* none 1 @{prop "snd (a, b) = a"} *}
    1.60  ML {* genuine 2 @{prop "snd (a, b) = a"} *}
    1.61 @@ -105,5 +103,9 @@
    1.62  ML {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
    1.63  ML {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
    1.64  ML {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
    1.65 +ML {* none 5 @{prop "f = (\<lambda>x. f x)"} *}
    1.66 +ML {* none 5 @{prop "f = (\<lambda>x. f x\<Colon>'a \<Rightarrow> bool)"} *}
    1.67 +ML {* none 5 @{prop "f = (\<lambda>x y. f x y)"} *}
    1.68 +ML {* none 5 @{prop "f = (\<lambda>x y. f x y\<Colon>'a \<Rightarrow> bool)"} *}
    1.69  
    1.70  end
     2.1 --- a/src/HOL/Nitpick_Examples/minipick.ML	Fri Sep 23 14:08:50 2011 +0200
     2.2 +++ b/src/HOL/Nitpick_Examples/minipick.ML	Fri Sep 23 14:25:53 2011 +0200
     2.3 @@ -7,21 +7,8 @@
     2.4  
     2.5  signature MINIPICK =
     2.6  sig
     2.7 -  datatype rep = S_Rep | R_Rep
     2.8 -  type styp = Nitpick_Util.styp
     2.9 -
    2.10 -  val vars_for_bound_var :
    2.11 -    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
    2.12 -  val rel_expr_for_bound_var :
    2.13 -    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
    2.14 -  val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
    2.15 -  val false_atom : Kodkod.rel_expr
    2.16 -  val true_atom : Kodkod.rel_expr
    2.17 -  val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
    2.18 -  val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
    2.19 -  val kodkod_problem_from_term :
    2.20 -    Proof.context -> (typ -> int) -> term -> Kodkod.problem
    2.21 -  val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
    2.22 +  val minipick : Proof.context -> int -> term -> string
    2.23 +  val minipick_expect : Proof.context -> string -> int -> term -> unit
    2.24  end;
    2.25  
    2.26  structure Minipick : MINIPICK =
    2.27 @@ -33,28 +20,34 @@
    2.28  open Nitpick_Peephole
    2.29  open Nitpick_Kodkod
    2.30  
    2.31 -datatype rep = S_Rep | R_Rep
    2.32 +datatype rep =
    2.33 +  S_Rep |
    2.34 +  R_Rep of bool
    2.35  
    2.36 -fun check_type ctxt (Type (@{type_name fun}, Ts)) =
    2.37 -    List.app (check_type ctxt) Ts
    2.38 -  | check_type ctxt (Type (@{type_name prod}, Ts)) =
    2.39 -    List.app (check_type ctxt) Ts
    2.40 -  | check_type _ @{typ bool} = ()
    2.41 -  | check_type _ (TFree (_, @{sort "{}"})) = ()
    2.42 -  | check_type _ (TFree (_, @{sort HOL.type})) = ()
    2.43 -  | check_type ctxt T =
    2.44 -    raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
    2.45 +fun check_type ctxt raw_infinite (Type (@{type_name fun}, Ts)) =
    2.46 +    List.app (check_type ctxt raw_infinite) Ts
    2.47 +  | check_type ctxt raw_infinite (Type (@{type_name prod}, Ts)) =
    2.48 +    List.app (check_type ctxt raw_infinite) Ts
    2.49 +  | check_type _ _ @{typ bool} = ()
    2.50 +  | check_type _ _ (TFree (_, @{sort "{}"})) = ()
    2.51 +  | check_type _ _ (TFree (_, @{sort HOL.type})) = ()
    2.52 +  | check_type ctxt raw_infinite T =
    2.53 +    if raw_infinite T then ()
    2.54 +    else raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
    2.55  
    2.56  fun atom_schema_of S_Rep card (Type (@{type_name fun}, [T1, T2])) =
    2.57      replicate_list (card T1) (atom_schema_of S_Rep card T2)
    2.58 -  | atom_schema_of R_Rep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
    2.59 +  | atom_schema_of (R_Rep true) card
    2.60 +                   (Type (@{type_name fun}, [T1, @{typ bool}])) =
    2.61      atom_schema_of S_Rep card T1
    2.62 -  | atom_schema_of R_Rep card (Type (@{type_name fun}, [T1, T2])) =
    2.63 -    atom_schema_of S_Rep card T1 @ atom_schema_of R_Rep card T2
    2.64 +  | atom_schema_of (rep as R_Rep _) card (Type (@{type_name fun}, [T1, T2])) =
    2.65 +    atom_schema_of S_Rep card T1 @ atom_schema_of rep card T2
    2.66    | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
    2.67      maps (atom_schema_of S_Rep card) Ts
    2.68    | atom_schema_of _ card T = [card T]
    2.69  val arity_of = length ooo atom_schema_of
    2.70 +val atom_seqs_of = map (AtomSeq o rpair 0) ooo atom_schema_of
    2.71 +val atom_seq_product_of = foldl1 Product ooo atom_seqs_of
    2.72  
    2.73  fun index_for_bound_var _ [_] 0 = 0
    2.74    | index_for_bound_var card (_ :: Ts) 0 =
    2.75 @@ -68,78 +61,121 @@
    2.76    map2 (curry DeclOne o pair 1)
    2.77         (index_seq (index_for_bound_var card (T :: Ts) 0)
    2.78                    (arity_of R card (nth (T :: Ts) 0)))
    2.79 -       (map (AtomSeq o rpair 0) (atom_schema_of R card T))
    2.80 +       (atom_seqs_of R card T)
    2.81  
    2.82  val atom_product = foldl1 Product o map Atom
    2.83  
    2.84 -val false_atom = Atom 0
    2.85 -val true_atom = Atom 1
    2.86 +val false_atom_num = 0
    2.87 +val true_atom_num = 1
    2.88 +val false_atom = Atom false_atom_num
    2.89 +val true_atom = Atom true_atom_num
    2.90  
    2.91 -fun formula_from_atom r = RelEq (r, true_atom)
    2.92 -fun atom_from_formula f = RelIf (f, true_atom, false_atom)
    2.93 -
    2.94 -fun kodkod_formula_from_term ctxt card frees =
    2.95 +fun kodkod_formula_from_term ctxt total card complete concrete frees =
    2.96    let
    2.97 -    fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
    2.98 -        let
    2.99 -          val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
   2.100 -                    |> all_combinations
   2.101 -        in
   2.102 -          map2 (fn i => fn js =>
   2.103 -                   RelIf (formula_from_atom (Project (r, [Num i])),
   2.104 -                          atom_product js, empty_n_ary_rel (length js)))
   2.105 -               (index_seq 0 (length jss)) jss
   2.106 -          |> foldl1 Union
   2.107 -        end
   2.108 -      | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
   2.109 -        let
   2.110 -          val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
   2.111 -                    |> all_combinations
   2.112 -          val arity2 = arity_of S_Rep card T2
   2.113 -        in
   2.114 -          map2 (fn i => fn js =>
   2.115 -                   Product (atom_product js,
   2.116 -                            Project (r, num_seq (i * arity2) arity2)
   2.117 -                            |> R_rep_from_S_rep T2))
   2.118 -               (index_seq 0 (length jss)) jss
   2.119 -          |> foldl1 Union
   2.120 -        end
   2.121 +    fun F_from_S_rep (SOME false) r = Not (RelEq (r, false_atom))
   2.122 +      | F_from_S_rep _ r = RelEq (r, true_atom)
   2.123 +    fun S_rep_from_F NONE f = RelIf (f, true_atom, false_atom)
   2.124 +      | S_rep_from_F (SOME true) f = RelIf (f, true_atom, None)
   2.125 +      | S_rep_from_F (SOME false) f = RelIf (Not f, false_atom, None)
   2.126 +    fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
   2.127 +        if total andalso T2 = bool_T then
   2.128 +          let
   2.129 +            val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
   2.130 +                      |> all_combinations
   2.131 +          in
   2.132 +            map2 (fn i => fn js =>
   2.133 +(*
   2.134 +                     RelIf (F_from_S_rep NONE (Project (r, [Num i])),
   2.135 +                            atom_product js, empty_n_ary_rel (length js))
   2.136 +*)
   2.137 +                     Join (Project (r, [Num i]),
   2.138 +                           atom_product (false_atom_num :: js))
   2.139 +                 ) (index_seq 0 (length jss)) jss
   2.140 +            |> foldl1 Union
   2.141 +          end
   2.142 +        else
   2.143 +          let
   2.144 +            val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
   2.145 +                      |> all_combinations
   2.146 +            val arity2 = arity_of S_Rep card T2
   2.147 +          in
   2.148 +            map2 (fn i => fn js =>
   2.149 +                     Product (atom_product js,
   2.150 +                              Project (r, num_seq (i * arity2) arity2)
   2.151 +                              |> R_rep_from_S_rep T2))
   2.152 +                 (index_seq 0 (length jss)) jss
   2.153 +            |> foldl1 Union
   2.154 +          end
   2.155        | R_rep_from_S_rep _ r = r
   2.156      fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
   2.157          Comprehension (decls_for S_Rep card Ts T,
   2.158              RelEq (R_rep_from_S_rep T
   2.159                         (rel_expr_for_bound_var card S_Rep (T :: Ts) 0), r))
   2.160        | S_rep_from_R_rep _ _ r = r
   2.161 -    fun to_F Ts t =
   2.162 +    fun partial_eq pos Ts (Type (@{type_name fun}, [T1, T2])) t1 t2 =
   2.163 +        HOLogic.mk_all ("x", T1,
   2.164 +                        HOLogic.eq_const T2 $ (incr_boundvars 1 t1 $ Bound 0)
   2.165 +                        $ (incr_boundvars 1 t2 $ Bound 0))
   2.166 +        |> to_F (SOME pos) Ts
   2.167 +      | partial_eq pos Ts T t1 t2 =
   2.168 +        if pos andalso not (concrete T) then
   2.169 +          False
   2.170 +        else
   2.171 +          (t1, t2) |> pairself (to_R_rep Ts)
   2.172 +                   |> (if pos then Some o Intersect else Lone o Union)
   2.173 +    and to_F pos Ts t =
   2.174        (case t of
   2.175 -         @{const Not} $ t1 => Not (to_F Ts t1)
   2.176 +         @{const Not} $ t1 => Not (to_F (Option.map not pos) Ts t1)
   2.177         | @{const False} => False
   2.178         | @{const True} => True
   2.179         | Const (@{const_name All}, _) $ Abs (_, T, t') =>
   2.180 -         All (decls_for S_Rep card Ts T, to_F (T :: Ts) t')
   2.181 +         if pos = SOME true andalso not (complete T) then False
   2.182 +         else All (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')
   2.183         | (t0 as Const (@{const_name All}, _)) $ t1 =>
   2.184 -         to_F Ts (t0 $ eta_expand Ts t1 1)
   2.185 +         to_F pos Ts (t0 $ eta_expand Ts t1 1)
   2.186         | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
   2.187 -         Exist (decls_for S_Rep card Ts T, to_F (T :: Ts) t')
   2.188 +         if pos = SOME false andalso not (complete T) then True
   2.189 +         else Exist (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')
   2.190         | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   2.191 -         to_F Ts (t0 $ eta_expand Ts t1 1)
   2.192 -       | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
   2.193 -         RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
   2.194 +         to_F pos Ts (t0 $ eta_expand Ts t1 1)
   2.195 +       | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
   2.196 +         (case pos of
   2.197 +            NONE => RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
   2.198 +          | SOME pos => partial_eq pos Ts T t1 t2)
   2.199         | Const (@{const_name ord_class.less_eq},
   2.200                  Type (@{type_name fun},
   2.201 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   2.202 +                      [Type (@{type_name fun}, [T', @{typ bool}]), _]))
   2.203           $ t1 $ t2 =>
   2.204 -         Subset (to_R_rep Ts t1, to_R_rep Ts t2)
   2.205 -       | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
   2.206 -       | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
   2.207 -       | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
   2.208 -       | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
   2.209 -       | Free _ => raise SAME ()
   2.210 -       | Term.Var _ => raise SAME ()
   2.211 -       | Bound _ => raise SAME ()
   2.212 -       | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
   2.213 -       | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
   2.214 -      handle SAME () => formula_from_atom (to_R_rep Ts t)
   2.215 +         (case pos of
   2.216 +            NONE => Subset (to_R_rep Ts t1, to_R_rep Ts t2)
   2.217 +          | SOME true =>
   2.218 +            Subset (Difference (atom_seq_product_of S_Rep card T',
   2.219 +                                Join (to_R_rep Ts t1, false_atom)),
   2.220 +                    Join (to_R_rep Ts t2, true_atom))
   2.221 +          | SOME false =>
   2.222 +            Subset (Join (to_R_rep Ts t1, true_atom),
   2.223 +                    Difference (atom_seq_product_of S_Rep card T',
   2.224 +                                Join (to_R_rep Ts t2, false_atom))))
   2.225 +       | @{const HOL.conj} $ t1 $ t2 => And (to_F pos Ts t1, to_F pos Ts t2)
   2.226 +       | @{const HOL.disj} $ t1 $ t2 => Or (to_F pos Ts t1, to_F pos Ts t2)
   2.227 +       | @{const HOL.implies} $ t1 $ t2 =>
   2.228 +         Implies (to_F (Option.map not pos) Ts t1, to_F pos Ts t2)
   2.229 +       | t1 $ t2 =>
   2.230 +         (case pos of
   2.231 +            NONE => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
   2.232 +          | SOME pos =>
   2.233 +            let
   2.234 +              val kt1 = to_R_rep Ts t1
   2.235 +              val kt2 = to_S_rep Ts t2
   2.236 +              val kT = atom_seq_product_of S_Rep card (fastype_of1 (Ts, t2))
   2.237 +            in
   2.238 +              if pos then
   2.239 +                Not (Subset (kt2, Difference (kT, Join (kt1, true_atom))))
   2.240 +              else
   2.241 +                Subset (kt2, Difference (kT, Join (kt1, false_atom)))
   2.242 +            end)
   2.243 +       | _ => raise SAME ())
   2.244 +      handle SAME () => F_from_S_rep pos (to_R_rep Ts t)
   2.245      and to_S_rep Ts t =
   2.246        case t of
   2.247          Const (@{const_name Pair}, _) $ t1 $ t2 =>
   2.248 @@ -160,6 +196,16 @@
   2.249        | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
   2.250        | Bound j => rel_expr_for_bound_var card S_Rep Ts j
   2.251        | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
   2.252 +    and partial_set_op swap1 swap2 op1 op2 Ts t1 t2 =
   2.253 +      let
   2.254 +        val kt1 = to_R_rep Ts t1
   2.255 +        val kt2 = to_R_rep Ts t2
   2.256 +        val (a11, a21) = (false_atom, true_atom) |> swap1 ? swap
   2.257 +        val (a12, a22) = (false_atom, true_atom) |> swap2 ? swap
   2.258 +      in
   2.259 +        Union (Product (op1 (Join (kt1, a11), Join (kt2, a12)), true_atom),
   2.260 +               Product (op2 (Join (kt1, a21), Join (kt2, a22)), false_atom))
   2.261 +      end
   2.262      and to_R_rep Ts t =
   2.263        (case t of
   2.264           @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
   2.265 @@ -180,15 +226,51 @@
   2.266         | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   2.267         | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
   2.268         | Const (@{const_name bot_class.bot},
   2.269 -                T as Type (@{type_name fun}, [_, @{typ bool}])) =>
   2.270 -         empty_n_ary_rel (arity_of R_Rep card T)
   2.271 -       | Const (@{const_name insert}, _) $ t1 $ t2 =>
   2.272 -         Union (to_S_rep Ts t1, to_R_rep Ts t2)
   2.273 +                T as Type (@{type_name fun}, [T', @{typ bool}])) =>
   2.274 +         if total then empty_n_ary_rel (arity_of (R_Rep total) card T)
   2.275 +         else Product (atom_seq_product_of (R_Rep total) card T', false_atom)
   2.276 +       | Const (@{const_name top_class.top},
   2.277 +                T as Type (@{type_name fun}, [T', @{typ bool}])) =>
   2.278 +         if total then atom_seq_product_of (R_Rep total) card T
   2.279 +         else Product (atom_seq_product_of (R_Rep total) card T', true_atom)
   2.280 +       | Const (@{const_name insert}, Type (_, [T, _])) $ t1 $ t2 =>
   2.281 +         if total then
   2.282 +           Union (to_S_rep Ts t1, to_R_rep Ts t2)
   2.283 +         else
   2.284 +           let
   2.285 +             val kt1 = to_S_rep Ts t1
   2.286 +             val kt2 = to_R_rep Ts t2
   2.287 +           in
   2.288 +             RelIf (Some kt1,
   2.289 +                    if arity_of S_Rep card T = 1 then
   2.290 +                      Override (kt2, Product (kt1, true_atom))
   2.291 +                    else
   2.292 +                      Union (Difference (kt2, Product (kt1, false_atom)),
   2.293 +                             Product (kt1, true_atom)),
   2.294 +                    Difference (kt2, Product (atom_seq_product_of S_Rep card T,
   2.295 +                                              false_atom)))
   2.296 +           end
   2.297         | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   2.298         | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
   2.299 -       | Const (@{const_name trancl}, _) $ t1 =>
   2.300 -         if arity_of R_Rep card (fastype_of1 (Ts, t1)) = 2 then
   2.301 -           Closure (to_R_rep Ts t1)
   2.302 +       | Const (@{const_name trancl},
   2.303 +                Type (_, [Type (_, [Type (_, [T', _]), _]), _])) $ t1 =>
   2.304 +         if arity_of S_Rep card T' = 1 then
   2.305 +           if total then
   2.306 +             Closure (to_R_rep Ts t1)
   2.307 +           else
   2.308 +             let
   2.309 +               val kt1 = to_R_rep Ts t1
   2.310 +               val true_core_kt = Closure (Join (kt1, true_atom))
   2.311 +               val kTx =
   2.312 +                 atom_seq_product_of S_Rep card (HOLogic.mk_prodT (`I T'))
   2.313 +               val false_mantle_kt =
   2.314 +                 Difference (kTx,
   2.315 +                     Closure (Difference (kTx, Join (kt1, false_atom))))
   2.316 +             in
   2.317 +               Union (Product (Difference (false_mantle_kt, true_core_kt),
   2.318 +                               false_atom),
   2.319 +                      Product (true_core_kt, true_atom))
   2.320 +             end
   2.321           else
   2.322             raise NOT_SUPPORTED "transitive closure for function or pair type"
   2.323         | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
   2.324 @@ -196,7 +278,8 @@
   2.325                  Type (@{type_name fun},
   2.326                        [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   2.327           $ t1 $ t2 =>
   2.328 -         Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
   2.329 +         if total then Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
   2.330 +         else partial_set_op true true Intersect Union Ts t1 t2
   2.331         | Const (@{const_name inf_class.inf}, _) $ _ =>
   2.332           to_R_rep Ts (eta_expand Ts t 1)
   2.333         | Const (@{const_name inf_class.inf}, _) =>
   2.334 @@ -205,7 +288,8 @@
   2.335                  Type (@{type_name fun},
   2.336                        [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   2.337           $ t1 $ t2 =>
   2.338 -         Union (to_R_rep Ts t1, to_R_rep Ts t2)
   2.339 +         if total then Union (to_R_rep Ts t1, to_R_rep Ts t2)
   2.340 +         else partial_set_op true true Union Intersect Ts t1 t2
   2.341         | Const (@{const_name sup_class.sup}, _) $ _ =>
   2.342           to_R_rep Ts (eta_expand Ts t 1)
   2.343         | Const (@{const_name sup_class.sup}, _) =>
   2.344 @@ -214,7 +298,8 @@
   2.345                  Type (@{type_name fun},
   2.346                        [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   2.347           $ t1 $ t2 =>
   2.348 -         Difference (to_R_rep Ts t1, to_R_rep Ts t2)
   2.349 +         if total then Difference (to_R_rep Ts t1, to_R_rep Ts t2)
   2.350 +         else partial_set_op true false Intersect Union Ts t1 t2
   2.351         | Const (@{const_name minus_class.minus},
   2.352                  Type (@{type_name fun},
   2.353                        [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   2.354 @@ -223,40 +308,47 @@
   2.355                  Type (@{type_name fun},
   2.356                        [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
   2.357           to_R_rep Ts (eta_expand Ts t 2)
   2.358 -       | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
   2.359 -       | Const (@{const_name Pair}, _) $ _ => raise SAME ()
   2.360 -       | Const (@{const_name Pair}, _) => raise SAME ()
   2.361 +       | Const (@{const_name Pair}, _) $ _ $ _ => to_S_rep Ts t
   2.362 +       | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts t
   2.363 +       | Const (@{const_name Pair}, _) => to_S_rep Ts t
   2.364         | Const (@{const_name fst}, _) $ _ => raise SAME ()
   2.365         | Const (@{const_name fst}, _) => raise SAME ()
   2.366         | Const (@{const_name snd}, _) $ _ => raise SAME ()
   2.367         | Const (@{const_name snd}, _) => raise SAME ()
   2.368 -       | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
   2.369 +       | @{const False} => false_atom
   2.370 +       | @{const True} => true_atom
   2.371         | Free (x as (_, T)) =>
   2.372 -         Rel (arity_of R_Rep card T, find_index (curry (op =) x) frees)
   2.373 +         Rel (arity_of (R_Rep total) card T, find_index (curry (op =) x) frees)
   2.374         | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
   2.375         | Bound _ => raise SAME ()
   2.376         | Abs (_, T, t') =>
   2.377 -         (case fastype_of1 (T :: Ts, t') of
   2.378 -            @{typ bool} => Comprehension (decls_for S_Rep card Ts T,
   2.379 -                                          to_F (T :: Ts) t')
   2.380 -          | T' => Comprehension (decls_for S_Rep card Ts T @
   2.381 -                                 decls_for R_Rep card (T :: Ts) T',
   2.382 -                                 Subset (rel_expr_for_bound_var card R_Rep
   2.383 -                                                              (T' :: T :: Ts) 0,
   2.384 -                                         to_R_rep (T :: Ts) t')))
   2.385 +         (case (total, fastype_of1 (T :: Ts, t')) of
   2.386 +            (true, @{typ bool}) =>
   2.387 +            Comprehension (decls_for S_Rep card Ts T, to_F NONE (T :: Ts) t')
   2.388 +          | (_, T') =>
   2.389 +            Comprehension (decls_for S_Rep card Ts T @
   2.390 +                           decls_for (R_Rep total) card (T :: Ts) T',
   2.391 +                           Subset (rel_expr_for_bound_var card (R_Rep total)
   2.392 +                                                          (T' :: T :: Ts) 0,
   2.393 +                                   to_R_rep (T :: Ts) t')))
   2.394         | t1 $ t2 =>
   2.395           (case fastype_of1 (Ts, t) of
   2.396 -            @{typ bool} => atom_from_formula (to_F Ts t)
   2.397 +            @{typ bool} =>
   2.398 +            if total then
   2.399 +              S_rep_from_F NONE (to_F NONE Ts t)
   2.400 +            else
   2.401 +              RelIf (to_F (SOME true) Ts t, true_atom,
   2.402 +                     RelIf (Not (to_F (SOME false) Ts t), false_atom,
   2.403 +                     None))
   2.404            | T =>
   2.405              let val T2 = fastype_of1 (Ts, t2) in
   2.406                case arity_of S_Rep card T2 of
   2.407                  1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
   2.408                | arity2 =>
   2.409 -                let val res_arity = arity_of R_Rep card T in
   2.410 +                let val res_arity = arity_of (R_Rep total) card T in
   2.411                    Project (Intersect
   2.412                        (Product (to_S_rep Ts t2,
   2.413 -                                atom_schema_of R_Rep card T
   2.414 -                                |> map (AtomSeq o rpair 0) |> foldl1 Product),
   2.415 +                                atom_seq_product_of (R_Rep total) card T),
   2.416                         to_R_rep Ts t1),
   2.417                        num_seq arity2 res_arity)
   2.418                  end
   2.419 @@ -264,28 +356,30 @@
   2.420         | _ => raise NOT_SUPPORTED ("term " ^
   2.421                                     quote (Syntax.string_of_term ctxt t)))
   2.422        handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
   2.423 -  in to_F [] end
   2.424 +  in to_F (if total then NONE else SOME true) [] end
   2.425  
   2.426 -fun bound_for_free card i (s, T) =
   2.427 -  let val js = atom_schema_of R_Rep card T in
   2.428 +fun bound_for_free total card i (s, T) =
   2.429 +  let val js = atom_schema_of (R_Rep total) card T in
   2.430      ([((length js, i), s)],
   2.431 -     [TupleSet [], atom_schema_of R_Rep card T |> map (rpair 0)
   2.432 +     [TupleSet [], atom_schema_of (R_Rep total) card T |> map (rpair 0)
   2.433                     |> tuple_set_from_atom_schema])
   2.434    end
   2.435  
   2.436 -fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
   2.437 -                                   r =
   2.438 -    if body_type T2 = bool_T then
   2.439 +fun declarative_axiom_for_rel_expr total card Ts
   2.440 +                                   (Type (@{type_name fun}, [T1, T2])) r =
   2.441 +    if total andalso body_type T2 = bool_T then
   2.442        True
   2.443      else
   2.444        All (decls_for S_Rep card Ts T1,
   2.445 -           declarative_axiom_for_rel_expr card (T1 :: Ts) T2
   2.446 +           declarative_axiom_for_rel_expr total card (T1 :: Ts) T2
   2.447                 (List.foldl Join r (vars_for_bound_var card S_Rep (T1 :: Ts) 0)))
   2.448 -  | declarative_axiom_for_rel_expr _ _ _ r = One r
   2.449 -fun declarative_axiom_for_free card i (_, T) =
   2.450 -  declarative_axiom_for_rel_expr card [] T (Rel (arity_of R_Rep card T, i))
   2.451 +  | declarative_axiom_for_rel_expr total _ _ _ r =
   2.452 +    (if total then One else Lone) r
   2.453 +fun declarative_axiom_for_free total card i (_, T) =
   2.454 +  declarative_axiom_for_rel_expr total card [] T
   2.455 +      (Rel (arity_of (R_Rep total) card T, i))
   2.456  
   2.457 -fun kodkod_problem_from_term ctxt raw_card t =
   2.458 +fun kodkod_problem_from_term ctxt total raw_card raw_infinite t =
   2.459    let
   2.460      val thy = ProofContext.theory_of ctxt
   2.461      fun card (Type (@{type_name fun}, [T1, T2])) =
   2.462 @@ -293,14 +387,25 @@
   2.463        | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
   2.464        | card @{typ bool} = 2
   2.465        | card T = Int.max (1, raw_card T)
   2.466 +    fun complete (Type (@{type_name fun}, [T1, T2])) =
   2.467 +        concrete T1 andalso complete T2
   2.468 +      | complete (Type (@{type_name prod}, Ts)) = forall complete Ts
   2.469 +      | complete T = not (raw_infinite T)
   2.470 +    and concrete (Type (@{type_name fun}, [T1, T2])) =
   2.471 +        complete T1 andalso concrete T2
   2.472 +      | concrete (Type (@{type_name prod}, Ts)) = forall concrete Ts
   2.473 +      | concrete _ = true
   2.474      val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
   2.475 -    val _ = fold_types (K o check_type ctxt) neg_t ()
   2.476 +    val _ = fold_types (K o check_type ctxt raw_infinite) neg_t ()
   2.477      val frees = Term.add_frees neg_t []
   2.478 -    val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
   2.479 +    val bounds =
   2.480 +      map2 (bound_for_free total card) (index_seq 0 (length frees)) frees
   2.481      val declarative_axioms =
   2.482 -      map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
   2.483 -    val formula = kodkod_formula_from_term ctxt card frees neg_t
   2.484 -                  |> fold_rev (curry And) declarative_axioms
   2.485 +      map2 (declarative_axiom_for_free total card)
   2.486 +           (index_seq 0 (length frees)) frees
   2.487 +    val formula =
   2.488 +      neg_t |> kodkod_formula_from_term ctxt total card complete concrete frees 
   2.489 +            |> fold_rev (curry And) declarative_axioms
   2.490      val univ_card = univ_card 0 0 0 bounds formula
   2.491    in
   2.492      {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
   2.493 @@ -324,4 +429,28 @@
   2.494      | Error (s, _) => error ("Kodkod error: " ^ s)
   2.495    end
   2.496  
   2.497 +val default_raw_infinite = member (op =) [@{typ nat}, @{typ int}]
   2.498 +
   2.499 +fun minipick ctxt n t =
   2.500 +  let
   2.501 +    val thy = ProofContext.theory_of ctxt
   2.502 +    val {total_consts, ...} = Nitpick_Isar.default_params thy []
   2.503 +    val totals =
   2.504 +      total_consts |> Option.map single |> the_default [true, false]
   2.505 +    fun problem_for (total, k) =
   2.506 +      kodkod_problem_from_term ctxt total (K k) default_raw_infinite t
   2.507 +  in
   2.508 +    (totals, 1 upto n)
   2.509 +    |-> map_product pair
   2.510 +    |> map problem_for
   2.511 +    |> solve_any_kodkod_problem (Proof_Context.theory_of ctxt)
   2.512 +  end
   2.513 +
   2.514 +fun minipick_expect ctxt expect n t =
   2.515 +  if getenv "KODKODI" <> "" then
   2.516 +    if minipick ctxt n t = expect then ()
   2.517 +    else error ("\"minipick_expect\" expected " ^ quote expect)
   2.518 +  else
   2.519 +    ()
   2.520 +
   2.521  end;