# HG changeset patch
# User blanchet
# Date 1283788286 -7200
# Node ID 70fd4a3c41ed88bb8d1b0365b9b9fde55d53aab6
# Parent  8420a873f534b6a7bc442315c4c197de7f7293e9
remove "minipick" (the toy version of Nitpick) and some tests;
a small step towards making the Nitpick tests take less time

diff -r 8420a873f534 -r 70fd4a3c41ed src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Sep 06 16:50:29 2010 +0200
+++ b/src/HOL/IsaMakefile	Mon Sep 06 17:51:26 2010 +0200
@@ -277,7 +277,6 @@
   Tools/nat_numeral_simprocs.ML \
   Tools/Nitpick/kodkod.ML \
   Tools/Nitpick/kodkod_sat.ML \
-  Tools/Nitpick/minipick.ML \
   Tools/Nitpick/nitpick.ML \
   Tools/Nitpick/nitpick_hol.ML \
   Tools/Nitpick/nitpick_isar.ML \
@@ -670,11 +669,10 @@
   Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
   Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \
   Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
-  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
-  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
-  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
-  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
-  Nitpick_Examples/Typedef_Nits.thy
+  Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \
+  Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
+  Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
+  Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
 
 
diff -r 8420a873f534 -r 70fd4a3c41ed src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Mon Sep 06 16:50:29 2010 +0200
+++ b/src/HOL/Nitpick.thy	Mon Sep 06 17:51:26 2010 +0200
@@ -24,7 +24,6 @@
      ("Tools/Nitpick/nitpick.ML")
      ("Tools/Nitpick/nitpick_isar.ML")
      ("Tools/Nitpick/nitpick_tests.ML")
-     ("Tools/Nitpick/minipick.ML")
 begin
 
 typedecl bisim_iterator
@@ -237,7 +236,6 @@
 use "Tools/Nitpick/nitpick.ML"
 use "Tools/Nitpick/nitpick_isar.ML"
 use "Tools/Nitpick/nitpick_tests.ML"
-use "Tools/Nitpick/minipick.ML"
 
 setup {* Nitpick_Isar.setup *}
 
diff -r 8420a873f534 -r 70fd4a3c41ed src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Sep 06 16:50:29 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Sep 06 17:51:26 2010 +0200
@@ -32,44 +32,6 @@
 nitpick [card = 1\<midarrow>12, expect = none]
 by auto
 
-lemma "(split o curry) f = f"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "(curry o split) f = f"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "(split o curry) f = (\<lambda>x. x) f"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "(curry o split) f = (\<lambda>x. x) f"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "split o curry = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = none]
-apply (rule ext)+
-by auto
-
-lemma "curry o split = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = none]
-apply (rule ext)+
-by auto
-
 lemma "split (\<lambda>x y. f (x, y)) = f"
 nitpick [card = 1\<midarrow>12, expect = none]
 by auto
@@ -150,31 +112,31 @@
 oops
 
 lemma "{a, b} = {b}"
-nitpick [card = 100, expect = genuine]
+nitpick [card = 50, expect = genuine]
 oops
 
 lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
 nitpick [card = 1, expect = genuine]
-nitpick [card = 20, expect = genuine]
+nitpick [card = 10, expect = genuine]
 nitpick [card = 5, dont_box, expect = genuine]
 oops
 
 lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
 nitpick [card = 3, expect = genuine]
 nitpick [card = 3, dont_box, expect = genuine]
-nitpick [card = 10, expect = genuine]
+nitpick [card = 8, expect = genuine]
 oops
 
 lemma "f (a, b) = x"
-nitpick [card = 12, expect = genuine]
+nitpick [card = 10, expect = genuine]
 oops
 
 lemma "f (a, a) = f (c, d)"
-nitpick [card = 12, expect = genuine]
+nitpick [card = 10, expect = genuine]
 oops
 
 lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>10, expect = none]
 by auto
 
 lemma "\<exists>F. F a b = G a b"
@@ -187,7 +149,7 @@
 oops
 
 lemma "(A\<Colon>'a\<times>'a, B\<Colon>'a\<times>'a) \<in> R \<Longrightarrow> (A, B) \<in> R"
-nitpick [card = 20, expect = none]
+nitpick [card = 15, expect = none]
 by auto
 
 lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
@@ -204,30 +166,30 @@
 lemma "x = y"
 nitpick [card 'a = 1, expect = none]
 nitpick [card 'a = 2, expect = genuine]
-nitpick [card 'a = 200, expect = genuine]
+nitpick [card 'a = 100, expect = genuine]
 oops
 
 lemma "\<forall>x. x = y"
 nitpick [card 'a = 1, expect = none]
 nitpick [card 'a = 2, expect = genuine]
-nitpick [card 'a = 200, expect = genuine]
+nitpick [card 'a = 100, expect = genuine]
 oops
 
 lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
 nitpick [card 'a = 1, expect = genuine]
-nitpick [card 'a = 200, expect = genuine]
+nitpick [card 'a = 100, expect = genuine]
 oops
 
 lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
-nitpick [card 'a = 1\<midarrow>20, expect = none]
+nitpick [card 'a = 1\<midarrow>15, expect = none]
 by auto
 
 lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
-nitpick [card = 1\<midarrow>20, expect = none]
+nitpick [card = 1\<midarrow>15, expect = none]
 by auto
 
 lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<midarrow>4, expect = none]
 by auto
 
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
@@ -241,7 +203,6 @@
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
        f u v w x y z = f u (g u) w (h u w) y (k u w y)"
 nitpick [card = 1\<midarrow>2, expect = none]
-nitpick [card = 3, expect = none]
 sorry
 
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
@@ -288,18 +249,6 @@
 nitpick [expect = none]
 sorry
 
-lemma "\<forall>x\<Colon>'a\<times>'b. if (\<exists>y. x = y) then True else False"
-nitpick [expect = none]
-sorry
-
-lemma "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
-nitpick [expect = none]
-by auto
-
-lemma "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"
-nitpick [expect = none]
-by auto
-
 lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
 nitpick [card 'a = 1, expect = genuine]
 nitpick [card 'a = 5, expect = genuine]
@@ -383,10 +332,6 @@
 nitpick [card = 20, expect = genuine]
 oops
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
-nitpick [expect = none]
-by auto
-
 lemma "P x \<equiv> P x"
 nitpick [card = 1\<midarrow>10, expect = none]
 by auto
@@ -456,14 +401,12 @@
 oops
 
 lemma "\<exists>!x. x = undefined"
-nitpick [card = 30, expect = none]
+nitpick [card = 15, expect = none]
 by auto
 
 lemma "x = All \<Longrightarrow> False"
 nitpick [card = 1, dont_box, expect = genuine]
-nitpick [card = 2, dont_box, expect = genuine]
-nitpick [card = 8, dont_box, expect = genuine]
-nitpick [card = 10, dont_box, expect = unknown]
+nitpick [card = 5, dont_box, expect = genuine]
 oops
 
 lemma "\<forall>x. f x y = f x y"
@@ -482,15 +425,9 @@
 nitpick [expect = genuine]
 oops
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> All P = All (\<lambda>x. P (I x))"
-nitpick [expect = none]
-by auto
-
 lemma "x = Ex \<Longrightarrow> False"
 nitpick [card = 1, dont_box, expect = genuine]
-nitpick [card = 2, dont_box, expect = genuine]
-nitpick [card = 6, dont_box, expect = genuine]
-nitpick [card = 10, dont_box, expect = unknown]
+nitpick [card = 5, dont_box, expect = genuine]
 oops
 
 lemma "\<exists>x. f x y = f x y"
@@ -513,10 +450,6 @@
 nitpick [expect = genuine]
 oops
 
-lemma "Ex (\<lambda>x. f x y = f y x) = False"
-nitpick [expect = genuine]
-oops
-
 lemma "Ex (\<lambda>x. f x y \<noteq> f x y) = False"
 nitpick [expect = none]
 by auto
@@ -525,11 +458,6 @@
 nitpick [expect = none]
 by auto
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x. (op= (I x)))"
-      "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x y. x = (I y))"
-nitpick [expect = none]
-by auto
-
 lemma "x = y \<Longrightarrow> y = x"
 nitpick [expect = none]
 by auto
@@ -555,35 +483,10 @@
 nitpick [expect = none]
 by auto
 
-lemma "\<not> a \<Longrightarrow> \<not> (a \<and> b)" "\<not> b \<Longrightarrow> \<not> (a \<and> b)"
-nitpick [expect = none]
-by auto
-
-lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x. op \<or> (I x))"
-      "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x y. x \<or> (I y))"
-nitpick [expect = none]
-by auto
-
-lemma "a \<Longrightarrow> a \<or> b" "b \<Longrightarrow> a \<or> b"
-nitpick [expect = none]
-by auto
-
-lemma "\<not> (a \<or> b) \<Longrightarrow> \<not> a" "\<not> (a \<or> b) \<Longrightarrow> \<not> b"
-nitpick [expect = none]
-by auto
-
 lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)"
 nitpick [expect = none]
 by auto
 
-lemma "\<not>a \<Longrightarrow> a \<longrightarrow> b" "b \<Longrightarrow> a \<longrightarrow> b"
-nitpick [expect = none]
-by auto
-
-lemma "\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<not> (a \<longrightarrow> b)"
-nitpick [expect = none]
-by auto
-
 lemma "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))"
 nitpick [expect = none]
 by auto
@@ -592,12 +495,6 @@
 nitpick [expect = none]
 by auto
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x. If (I x))"
-      "J = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y. If x (J y))"
-      "K = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y z. If x y (K z))"
-nitpick [expect = none]
-by auto
-
 lemma "fst (x, y) = x"
 nitpick [expect = none]
 by (simp add: fst_def)
@@ -642,10 +539,6 @@
 nitpick [expect = none]
 by auto
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))"
-nitpick [expect = none]
-by auto
-
 lemma "fst (x, y) = snd (y, x)"
 nitpick [expect = none]
 by auto
@@ -662,10 +555,6 @@
 nitpick [expect = none]
 by auto
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> curry Id = (\<lambda>x y. Id (x, I y))"
-nitpick [expect = none]
-by (simp add: curry_def)
-
 lemma "{} = (\<lambda>x. False)"
 nitpick [expect = none]
 by (metis Collect_def empty_def)
@@ -722,10 +611,6 @@
 nitpick [expect = none]
 by (simp add: mem_def)
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> insert = (\<lambda>x. insert (I x))"
-nitpick [expect = none]
-by simp
-
 lemma "insert = (\<lambda>x y. insert x (y \<union> y))"
 nitpick [expect = none]
 by simp
@@ -743,10 +628,6 @@
 nitpick [expect = none]
 by auto
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))"
-nitpick [card = 1\<midarrow>2, expect = none]
-by auto
-
 lemma "((x, x), (x, x)) \<in> rtrancl {}"
 nitpick [card = 1\<midarrow>5, expect = none]
 by auto
@@ -755,42 +636,18 @@
 nitpick [card = 1\<midarrow>5, expect = none]
 by auto
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x y. op \<union> x (I y))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
 lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)"
 nitpick [expect = none]
 by auto
 
-lemma "a \<in> (A \<union> B) \<Longrightarrow> a \<in> A \<or> a \<in> B"
-nitpick [expect = none]
-by auto
-
 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))"
 nitpick [card = 1\<midarrow>5, expect = none]
 by auto
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x y. op \<inter> x (I y))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
 lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)"
 nitpick [card = 1\<midarrow>5, expect = none]
 by auto
 
-lemma "a \<notin> (A \<inter> B) \<Longrightarrow> a \<notin> A \<or> a \<notin> B"
-nitpick [expect = none]
-by auto
-
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x\<Colon>'a set. op - (I x))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x y\<Colon>'a set. op - x (I y))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
 lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B"
 nitpick [card = 1\<midarrow>5, expect = none]
 by auto
@@ -799,22 +656,10 @@
 nitpick [card = 1\<midarrow>5, expect = none]
 by auto
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x y. op \<subset> x (I y))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
 lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)"
 nitpick [card = 1\<midarrow>5, expect = none]
 by auto
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x. op \<subseteq> (I x))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x y. op \<subseteq> x (I y))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
 lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B"
 nitpick [card = 1\<midarrow>5, expect = none]
 by auto
@@ -843,10 +688,6 @@
 nitpick [card 'a = 10, expect = genuine]
 oops
 
-lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))"
-nitpick [card = 1\<midarrow>7, expect = none]
-oops
-
 lemma "finite A"
 nitpick [expect = none]
 oops
diff -r 8420a873f534 -r 70fd4a3c41ed src/HOL/Nitpick_Examples/Nitpick_Examples.thy
--- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Mon Sep 06 16:50:29 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Mon Sep 06 17:51:26 2010 +0200
@@ -7,7 +7,7 @@
 
 theory Nitpick_Examples
 imports Core_Nits Datatype_Nits Hotel_Nits Induct_Nits Integer_Nits Manual_Nits
-        Mini_Nits Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits
-        Tests_Nits Typedef_Nits
+        Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
+        Typedef_Nits
 begin
 end
diff -r 8420a873f534 -r 70fd4a3c41ed src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Sep 06 16:50:29 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Sep 06 17:51:26 2010 +0200
@@ -71,7 +71,7 @@
                      [if null markers then "External" else "ExternalV2",
                       dir ^ dir_sep ^ exec, base ^ ".cnf",
                       if dev = ToFile then out_file else ""] @ markers @
-                      (if dev = ToFile then [out_file] else []) @ args
+                     (if dev = ToFile then [out_file] else []) @ args
                    end)
 fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
     if incremental andalso mode = Batch then NONE else SOME (name, K ss)
diff -r 8420a873f534 -r 70fd4a3c41ed src/HOL/Tools/Nitpick/minipick.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Mon Sep 06 16:50:29 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,327 +0,0 @@
-(*  Title:      HOL/Tools/Nitpick/minipick.ML
-    Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009, 2010
-
-Finite model generation for HOL formulas using Kodkod, minimalistic version.
-*)
-
-signature MINIPICK =
-sig
-  datatype rep = SRep | RRep
-  type styp = Nitpick_Util.styp
-
-  val vars_for_bound_var :
-    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
-  val rel_expr_for_bound_var :
-    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
-  val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
-  val false_atom : Kodkod.rel_expr
-  val true_atom : Kodkod.rel_expr
-  val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
-  val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
-  val kodkod_problem_from_term :
-    Proof.context -> (typ -> int) -> term -> Kodkod.problem
-  val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
-end;
-
-structure Minipick : MINIPICK =
-struct
-
-open Kodkod
-open Nitpick_Util
-open Nitpick_HOL
-open Nitpick_Peephole
-open Nitpick_Kodkod
-
-datatype rep = SRep | RRep
-
-fun check_type ctxt (Type (@{type_name fun}, Ts)) =
-    List.app (check_type ctxt) Ts
-  | check_type ctxt (Type (@{type_name prod}, Ts)) =
-    List.app (check_type ctxt) Ts
-  | check_type _ @{typ bool} = ()
-  | check_type _ (TFree (_, @{sort "{}"})) = ()
-  | check_type _ (TFree (_, @{sort HOL.type})) = ()
-  | check_type ctxt T =
-    raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
-
-fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) =
-    replicate_list (card T1) (atom_schema_of SRep card T2)
-  | atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
-    atom_schema_of SRep card T1
-  | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
-    atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
-  | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
-    maps (atom_schema_of SRep card) Ts
-  | atom_schema_of _ card T = [card T]
-val arity_of = length ooo atom_schema_of
-
-fun index_for_bound_var _ [_] 0 = 0
-  | index_for_bound_var card (_ :: Ts) 0 =
-    index_for_bound_var card Ts 0 + arity_of SRep card (hd Ts)
-  | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
-fun vars_for_bound_var card R Ts j =
-  map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
-                               (arity_of R card (nth Ts j)))
-val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
-fun decls_for R card Ts T =
-  map2 (curry DeclOne o pair 1)
-       (index_seq (index_for_bound_var card (T :: Ts) 0)
-                  (arity_of R card (nth (T :: Ts) 0)))
-       (map (AtomSeq o rpair 0) (atom_schema_of R card T))
-
-val atom_product = foldl1 Product o map Atom
-
-val false_atom = Atom 0
-val true_atom = Atom 1
-
-fun formula_from_atom r = RelEq (r, true_atom)
-fun atom_from_formula f = RelIf (f, true_atom, false_atom)
-
-fun kodkod_formula_from_term ctxt card frees =
-  let
-    fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
-        let
-          val jss = atom_schema_of SRep card T1 |> map (rpair 0)
-                    |> all_combinations
-        in
-          map2 (fn i => fn js =>
-                   RelIf (formula_from_atom (Project (r, [Num i])),
-                          atom_product js, empty_n_ary_rel (length js)))
-               (index_seq 0 (length jss)) jss
-          |> foldl1 Union
-        end
-      | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
-        let
-          val jss = atom_schema_of SRep card T1 |> map (rpair 0)
-                    |> all_combinations
-          val arity2 = arity_of SRep card T2
-        in
-          map2 (fn i => fn js =>
-                   Product (atom_product js,
-                            Project (r, num_seq (i * arity2) arity2)
-                            |> R_rep_from_S_rep T2))
-               (index_seq 0 (length jss)) jss
-          |> foldl1 Union
-        end
-      | R_rep_from_S_rep _ r = r
-    fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
-        Comprehension (decls_for SRep card Ts T,
-            RelEq (R_rep_from_S_rep T
-                       (rel_expr_for_bound_var card SRep (T :: Ts) 0), r))
-      | S_rep_from_R_rep _ _ r = r
-    fun to_F Ts t =
-      (case t of
-         @{const Not} $ t1 => Not (to_F Ts t1)
-       | @{const False} => False
-       | @{const True} => True
-       | Const (@{const_name All}, _) $ Abs (_, T, t') =>
-         All (decls_for SRep card Ts T, to_F (T :: Ts) t')
-       | (t0 as Const (@{const_name All}, _)) $ t1 =>
-         to_F Ts (t0 $ eta_expand Ts t1 1)
-       | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
-         Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
-       | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
-         to_F Ts (t0 $ eta_expand Ts t1 1)
-       | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
-         RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
-       | Const (@{const_name ord_class.less_eq},
-                Type (@{type_name fun},
-                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
-         $ t1 $ t2 =>
-         Subset (to_R_rep Ts t1, to_R_rep Ts t2)
-       | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
-       | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
-       | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
-       | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
-       | Free _ => raise SAME ()
-       | Term.Var _ => raise SAME ()
-       | Bound _ => raise SAME ()
-       | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
-       | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
-      handle SAME () => formula_from_atom (to_R_rep Ts t)
-    and to_S_rep Ts t =
-      case t of
-        Const (@{const_name Pair}, _) $ t1 $ t2 =>
-        Product (to_S_rep Ts t1, to_S_rep Ts t2)
-      | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
-      | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
-      | Const (@{const_name fst}, _) $ t1 =>
-        let val fst_arity = arity_of SRep card (fastype_of1 (Ts, t)) in
-          Project (to_S_rep Ts t1, num_seq 0 fst_arity)
-        end
-      | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
-      | Const (@{const_name snd}, _) $ t1 =>
-        let
-          val pair_arity = arity_of SRep card (fastype_of1 (Ts, t1))
-          val snd_arity = arity_of SRep card (fastype_of1 (Ts, t))
-          val fst_arity = pair_arity - snd_arity
-        in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
-      | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
-      | Bound j => rel_expr_for_bound_var card SRep Ts j
-      | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
-    and to_R_rep Ts t =
-      (case t of
-         @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
-       | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
-       | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
-       | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
-       | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
-       | Const (@{const_name ord_class.less_eq},
-                Type (@{type_name fun},
-                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
-         to_R_rep Ts (eta_expand Ts t 1)
-       | Const (@{const_name ord_class.less_eq}, _) =>
-         to_R_rep Ts (eta_expand Ts t 2)
-       | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
-       | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
-       | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
-       | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
-       | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
-       | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
-       | Const (@{const_name bot_class.bot},
-                T as Type (@{type_name fun}, [_, @{typ bool}])) =>
-         empty_n_ary_rel (arity_of RRep card T)
-       | Const (@{const_name insert}, _) $ t1 $ t2 =>
-         Union (to_S_rep Ts t1, to_R_rep Ts t2)
-       | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
-       | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
-       | Const (@{const_name trancl}, _) $ t1 =>
-         if arity_of RRep card (fastype_of1 (Ts, t1)) = 2 then
-           Closure (to_R_rep Ts t1)
-         else
-           raise NOT_SUPPORTED "transitive closure for function or pair type"
-       | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
-       | Const (@{const_name semilattice_inf_class.inf},
-                Type (@{type_name fun},
-                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
-         $ t1 $ t2 =>
-         Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
-       | Const (@{const_name semilattice_inf_class.inf}, _) $ _ =>
-         to_R_rep Ts (eta_expand Ts t 1)
-       | Const (@{const_name semilattice_inf_class.inf}, _) =>
-         to_R_rep Ts (eta_expand Ts t 2)
-       | Const (@{const_name semilattice_sup_class.sup},
-                Type (@{type_name fun},
-                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
-         $ t1 $ t2 =>
-         Union (to_R_rep Ts t1, to_R_rep Ts t2)
-       | Const (@{const_name semilattice_sup_class.sup}, _) $ _ =>
-         to_R_rep Ts (eta_expand Ts t 1)
-       | Const (@{const_name semilattice_sup_class.sup}, _) =>
-         to_R_rep Ts (eta_expand Ts t 2)
-       | Const (@{const_name minus_class.minus},
-                Type (@{type_name fun},
-                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
-         $ t1 $ t2 =>
-         Difference (to_R_rep Ts t1, to_R_rep Ts t2)
-       | Const (@{const_name minus_class.minus},
-                Type (@{type_name fun},
-                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
-         to_R_rep Ts (eta_expand Ts t 1)
-       | Const (@{const_name minus_class.minus},
-                Type (@{type_name fun},
-                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
-         to_R_rep Ts (eta_expand Ts t 2)
-       | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
-       | Const (@{const_name Pair}, _) $ _ => raise SAME ()
-       | Const (@{const_name Pair}, _) => raise SAME ()
-       | Const (@{const_name fst}, _) $ _ => raise SAME ()
-       | Const (@{const_name fst}, _) => raise SAME ()
-       | Const (@{const_name snd}, _) $ _ => raise SAME ()
-       | Const (@{const_name snd}, _) => raise SAME ()
-       | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
-       | Free (x as (_, T)) =>
-         Rel (arity_of RRep card T, find_index (curry (op =) x) frees)
-       | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
-       | Bound _ => raise SAME ()
-       | Abs (_, T, t') =>
-         (case fastype_of1 (T :: Ts, t') of
-            @{typ bool} => Comprehension (decls_for SRep card Ts T,
-                                          to_F (T :: Ts) t')
-          | T' => Comprehension (decls_for SRep card Ts T @
-                                 decls_for RRep card (T :: Ts) T',
-                                 Subset (rel_expr_for_bound_var card RRep
-                                                              (T' :: T :: Ts) 0,
-                                         to_R_rep (T :: Ts) t')))
-       | t1 $ t2 =>
-         (case fastype_of1 (Ts, t) of
-            @{typ bool} => atom_from_formula (to_F Ts t)
-          | T =>
-            let val T2 = fastype_of1 (Ts, t2) in
-              case arity_of SRep card T2 of
-                1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
-              | arity2 =>
-                let val res_arity = arity_of RRep card T in
-                  Project (Intersect
-                      (Product (to_S_rep Ts t2,
-                                atom_schema_of RRep card T
-                                |> map (AtomSeq o rpair 0) |> foldl1 Product),
-                       to_R_rep Ts t1),
-                      num_seq arity2 res_arity)
-                end
-            end)
-       | _ => raise NOT_SUPPORTED ("term " ^
-                                   quote (Syntax.string_of_term ctxt t)))
-      handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
-  in to_F [] end
-
-fun bound_for_free card i (s, T) =
-  let val js = atom_schema_of RRep card T in
-    ([((length js, i), s)],
-     [TupleSet [], atom_schema_of RRep card T |> map (rpair 0)
-                   |> tuple_set_from_atom_schema])
-  end
-
-fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
-                                   r =
-    if body_type T2 = bool_T then
-      True
-    else
-      All (decls_for SRep card Ts T1,
-           declarative_axiom_for_rel_expr card (T1 :: Ts) T2
-               (List.foldl Join r (vars_for_bound_var card SRep (T1 :: Ts) 0)))
-  | declarative_axiom_for_rel_expr _ _ _ r = One r
-fun declarative_axiom_for_free card i (_, T) =
-  declarative_axiom_for_rel_expr card [] T (Rel (arity_of RRep card T, i))
-
-fun kodkod_problem_from_term ctxt raw_card t =
-  let
-    val thy = ProofContext.theory_of ctxt
-    fun card (Type (@{type_name fun}, [T1, T2])) =
-        reasonable_power (card T2) (card T1)
-      | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
-      | card @{typ bool} = 2
-      | card T = Int.max (1, raw_card T)
-    val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
-    val _ = fold_types (K o check_type ctxt) neg_t ()
-    val frees = Term.add_frees neg_t []
-    val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
-    val declarative_axioms =
-      map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
-    val formula = kodkod_formula_from_term ctxt card frees neg_t
-                  |> fold_rev (curry And) declarative_axioms
-    val univ_card = univ_card 0 0 0 bounds formula
-  in
-    {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
-     bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
-  end
-
-fun solve_any_kodkod_problem thy problems =
-  let
-    val {overlord, ...} = Nitpick_Isar.default_params thy []
-    val max_threads = 1
-    val max_solutions = 1
-  in
-    case solve_any_problem overlord NONE max_threads max_solutions problems of
-      JavaNotInstalled => "unknown"
-    | JavaTooOld => "unknown"
-    | KodkodiNotInstalled => "unknown"
-    | Normal ([], _, _) => "none"
-    | Normal _ => "genuine"
-    | TimedOut _ => "unknown"
-    | Interrupted _ => "unknown"
-    | Error (s, _) => error ("Kodkod error: " ^ s)
-  end
-
-end;