polished Nitpick's binary integer support etc.;
authorblanchet
Fri Dec 18 12:00:29 2009 +0100 (2009-12-18)
changeset 341268a2c5d7aff51
parent 34125 7aac4d74bb76
child 34127 85257fa296f6
polished Nitpick's binary integer support etc.;
etc. = improve inconsistent scope correction + sort values nicely in output
+ handle "mod" using the characterization "x mod y = x - x div y * y"
(instead of explicit code in Nitpick)
+ introduce KK = Kodkod as abbreviation
doc-src/Nitpick/nitpick.tex
src/HOL/Divides.thy
src/HOL/IsaMakefile
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Datatype_Nits.thy
src/HOL/Nitpick_Examples/Integer_Nits.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nitpick_Examples/Nitpick_Examples.thy
src/HOL/Nitpick_Examples/Special_Nits.thy
src/HOL/Nitpick_Examples/Typedef_Nits.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_peephole.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Dec 17 15:22:27 2009 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Fri Dec 18 12:00:29 2009 +0100
     1.3 @@ -740,7 +740,7 @@
     1.4  
     1.5  \prew
     1.6  \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
     1.7 -\textbf{nitpick}~[\textit{card nat}~= 100,\, \textit{verbose}] \\[2\smallskipamount]
     1.8 +\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
     1.9  \slshape The inductive predicate ``\textit{even}'' was proved well-founded.
    1.10  Nitpick can compute it efficiently. \\[2\smallskipamount]
    1.11  Trying 1 scope: \\
    1.12 @@ -758,7 +758,7 @@
    1.13  
    1.14  \prew
    1.15  \textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
    1.16 -\textbf{nitpick}~[\textit{card nat}~= 100] \\[2\smallskipamount]
    1.17 +\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount]
    1.18  \slshape Nitpick found a counterexample: \\[2\smallskipamount]
    1.19  \hbox{}\qquad Empty assignment
    1.20  \postw
    1.21 @@ -1752,7 +1752,7 @@
    1.22  
    1.23  \textbf{Warning:} For technical reasons, Nitpick always reverts to unary for
    1.24  problems that refer to the types \textit{rat} or \textit{real} or the constants
    1.25 -\textit{gcd} or \textit{lcm}.
    1.26 +\textit{Suc}, \textit{gcd}, or \textit{lcm}.
    1.27  
    1.28  {\small See also \textit{bits} (\S\ref{scope-of-search}) and
    1.29  \textit{show\_datatypes} (\S\ref{output-format}).}
     2.1 --- a/src/HOL/Divides.thy	Thu Dec 17 15:22:27 2009 +0100
     2.2 +++ b/src/HOL/Divides.thy	Fri Dec 18 12:00:29 2009 +0100
     2.3 @@ -2443,6 +2443,17 @@
     2.4  declare dvd_eq_mod_eq_0_number_of [simp]
     2.5  
     2.6  
     2.7 +subsubsection {* Nitpick *}
     2.8 +
     2.9 +lemma zmod_zdiv_equality':
    2.10 +"(m\<Colon>int) mod n = m - (m div n) * n"
    2.11 +by (rule_tac P="%x. m mod n = x - (m div n) * n"
    2.12 +    in subst [OF mod_div_equality [of _ n]])
    2.13 +   arith
    2.14 +
    2.15 +lemmas [nitpick_def] = mod_div_equality' [THEN eq_reflection]
    2.16 +                       zmod_zdiv_equality' [THEN eq_reflection]
    2.17 +
    2.18  subsubsection {* Code generation *}
    2.19  
    2.20  definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
     3.1 --- a/src/HOL/IsaMakefile	Thu Dec 17 15:22:27 2009 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Fri Dec 18 12:00:29 2009 +0100
     3.3 @@ -610,13 +610,13 @@
     3.4  
     3.5  HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
     3.6  
     3.7 -$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML	\
     3.8 -  Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy	\
     3.9 -  Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Manual_Nits.thy	\
    3.10 -  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy		\
    3.11 -  Nitpick_Examples/Nitpick_Examples.thy					\
    3.12 -  Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy	\
    3.13 -  Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy	\
    3.14 +$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
    3.15 +  Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
    3.16 +  Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Integer_Nits.thy \
    3.17 +  Nitpick_Examples/Manual_Nits.thy Nitpick_Examples/Mini_Nits.thy \
    3.18 +  Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \
    3.19 +  Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
    3.20 +  Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
    3.21    Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
    3.22  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
    3.23  
     4.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Thu Dec 17 15:22:27 2009 +0100
     4.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Dec 18 12:00:29 2009 +0100
     4.3 @@ -876,7 +876,7 @@
     4.4  by auto
     4.5  
     4.6  lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))"
     4.7 -nitpick [expect = none]
     4.8 +nitpick [card = 1\<midarrow>7, expect = none]
     4.9  by auto
    4.10  
    4.11  lemma "A \<union> - A = UNIV"
    4.12 @@ -892,7 +892,7 @@
    4.13  oops
    4.14  
    4.15  lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))"
    4.16 -nitpick [expect = none]
    4.17 +nitpick [card = 1\<midarrow>7, expect = none]
    4.18  oops
    4.19  
    4.20  lemma "finite A"
     5.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Thu Dec 17 15:22:27 2009 +0100
     5.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Dec 18 12:00:29 2009 +0100
     5.3 @@ -14,21 +14,11 @@
     5.4  nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
     5.5  
     5.6  primrec rot where
     5.7 -"rot Nibble0 = Nibble1" |
     5.8 -"rot Nibble1 = Nibble2" |
     5.9 -"rot Nibble2 = Nibble3" |
    5.10 -"rot Nibble3 = Nibble4" |
    5.11 -"rot Nibble4 = Nibble5" |
    5.12 -"rot Nibble5 = Nibble6" |
    5.13 -"rot Nibble6 = Nibble7" |
    5.14 -"rot Nibble7 = Nibble8" |
    5.15 -"rot Nibble8 = Nibble9" |
    5.16 -"rot Nibble9 = NibbleA" |
    5.17 -"rot NibbleA = NibbleB" |
    5.18 -"rot NibbleB = NibbleC" |
    5.19 -"rot NibbleC = NibbleD" |
    5.20 -"rot NibbleD = NibbleE" |
    5.21 -"rot NibbleE = NibbleF" |
    5.22 +"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
    5.23 +"rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" |
    5.24 +"rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" |
    5.25 +"rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" |
    5.26 +"rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" |
    5.27  "rot NibbleF = Nibble0"
    5.28  
    5.29  lemma "rot n \<noteq> n"
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Fri Dec 18 12:00:29 2009 +0100
     6.3 @@ -0,0 +1,209 @@
     6.4 +(*  Title:      HOL/Nitpick_Examples/Integer_Nits.thy
     6.5 +    Author:     Jasmin Blanchette, TU Muenchen
     6.6 +    Copyright   2009
     6.7 +
     6.8 +Examples featuring Nitpick applied to natural numbers and integers.
     6.9 +*)
    6.10 +
    6.11 +header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *} 
    6.12 +
    6.13 +theory Integer_Nits
    6.14 +imports Nitpick
    6.15 +begin
    6.16 +
    6.17 +nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
    6.18 +                card = 1\<midarrow>6, bits = 1,2,3,4,6,8]
    6.19 +
    6.20 +lemma "Suc x = x + 1"
    6.21 +nitpick [unary_ints, expect = none]
    6.22 +nitpick [binary_ints, expect = none]
    6.23 +sorry
    6.24 +
    6.25 +lemma "x < Suc x"
    6.26 +nitpick [unary_ints, expect = none]
    6.27 +nitpick [binary_ints, expect = none]
    6.28 +sorry
    6.29 +
    6.30 +lemma "x + y \<ge> (x::nat)"
    6.31 +nitpick [unary_ints, expect = none]
    6.32 +nitpick [binary_ints, expect = none]
    6.33 +sorry
    6.34 +
    6.35 +lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::nat)"
    6.36 +nitpick [unary_ints, expect = none]
    6.37 +nitpick [binary_ints, expect = none]
    6.38 +sorry
    6.39 +
    6.40 +lemma "x + y = y + (x::nat)"
    6.41 +nitpick [unary_ints, expect = none]
    6.42 +nitpick [binary_ints, expect = none]
    6.43 +sorry
    6.44 +
    6.45 +lemma "x > y \<Longrightarrow> x - y \<noteq> (0::nat)"
    6.46 +nitpick [unary_ints, expect = none]
    6.47 +nitpick [binary_ints, expect = none]
    6.48 +sorry
    6.49 +
    6.50 +lemma "x \<le> y \<Longrightarrow> x - y = (0::nat)"
    6.51 +nitpick [unary_ints, expect = none]
    6.52 +nitpick [binary_ints, expect = none]
    6.53 +sorry
    6.54 +
    6.55 +lemma "x - (0::nat) = x"
    6.56 +nitpick [unary_ints, expect = none]
    6.57 +nitpick [binary_ints, expect = none]
    6.58 +sorry
    6.59 +
    6.60 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::nat)"
    6.61 +nitpick [unary_ints, expect = none]
    6.62 +nitpick [binary_ints, expect = none]
    6.63 +sorry
    6.64 +
    6.65 +lemma "0 * y = (0::nat)"
    6.66 +nitpick [unary_ints, expect = none]
    6.67 +nitpick [binary_ints, expect = none]
    6.68 +sorry
    6.69 +
    6.70 +lemma "y * 0 = (0::nat)"
    6.71 +nitpick [unary_ints, expect = none]
    6.72 +nitpick [binary_ints, expect = none]
    6.73 +sorry
    6.74 +
    6.75 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::nat)"
    6.76 +nitpick [unary_ints, expect = none]
    6.77 +nitpick [binary_ints, expect = none]
    6.78 +sorry
    6.79 +
    6.80 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::nat)"
    6.81 +nitpick [unary_ints, expect = none]
    6.82 +nitpick [binary_ints, expect = none]
    6.83 +sorry
    6.84 +
    6.85 +lemma "x * y div y = (x::nat)"
    6.86 +nitpick [unary_ints, expect = genuine]
    6.87 +nitpick [binary_ints, expect = genuine]
    6.88 +oops
    6.89 +
    6.90 +lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::nat)"
    6.91 +nitpick [unary_ints, expect = none]
    6.92 +nitpick [binary_ints, expect = none]
    6.93 +sorry
    6.94 +
    6.95 +lemma "5 * 55 < (260::nat)"
    6.96 +nitpick [unary_ints, expect = none]
    6.97 +nitpick [binary_ints, expect = none]
    6.98 +nitpick [binary_ints, bits = 9, expect = genuine]
    6.99 +oops
   6.100 +
   6.101 +lemma "nat (of_nat n) = n"
   6.102 +nitpick [unary_ints, expect = none]
   6.103 +nitpick [binary_ints, expect = none]
   6.104 +sorry
   6.105 +
   6.106 +lemma "x + y \<ge> (x::int)"
   6.107 +nitpick [unary_ints, expect = genuine]
   6.108 +nitpick [binary_ints, expect = genuine]
   6.109 +oops
   6.110 +
   6.111 +lemma "\<lbrakk>x \<ge> 0; y \<ge> 0\<rbrakk> \<Longrightarrow> x + y \<ge> (0::int)"
   6.112 +nitpick [unary_ints, expect = none]
   6.113 +nitpick [binary_ints, expect = none]
   6.114 +sorry
   6.115 +
   6.116 +lemma "y \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)"
   6.117 +nitpick [unary_ints, expect = none]
   6.118 +nitpick [binary_ints, expect = none]
   6.119 +sorry
   6.120 +
   6.121 +lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (y::int)"
   6.122 +nitpick [unary_ints, expect = none]
   6.123 +nitpick [binary_ints, expect = none]
   6.124 +sorry
   6.125 +
   6.126 +lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)"
   6.127 +nitpick [unary_ints, expect = genuine]
   6.128 +nitpick [binary_ints, expect = genuine]
   6.129 +oops
   6.130 +
   6.131 +lemma "\<lbrakk>x \<le> 0; y \<le> 0\<rbrakk> \<Longrightarrow> x + y \<le> (0::int)"
   6.132 +nitpick [unary_ints, expect = none]
   6.133 +nitpick [binary_ints, expect = none]
   6.134 +sorry
   6.135 +
   6.136 +lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::int)"
   6.137 +nitpick [unary_ints, expect = genuine]
   6.138 +nitpick [binary_ints, expect = genuine]
   6.139 +oops
   6.140 +
   6.141 +lemma "x + y = y + (x::int)"
   6.142 +nitpick [unary_ints, expect = none]
   6.143 +nitpick [binary_ints, expect = none]
   6.144 +sorry
   6.145 +
   6.146 +lemma "x > y \<Longrightarrow> x - y \<noteq> (0::int)"
   6.147 +nitpick [unary_ints, expect = none]
   6.148 +nitpick [binary_ints, expect = none]
   6.149 +sorry
   6.150 +
   6.151 +lemma "x \<le> y \<Longrightarrow> x - y = (0::int)"
   6.152 +nitpick [unary_ints, expect = genuine]
   6.153 +nitpick [binary_ints, expect = genuine]
   6.154 +oops
   6.155 +
   6.156 +lemma "x - (0::int) = x"
   6.157 +nitpick [unary_ints, expect = none]
   6.158 +nitpick [binary_ints, expect = none]
   6.159 +sorry
   6.160 +
   6.161 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::int)"
   6.162 +nitpick [unary_ints, expect = none]
   6.163 +nitpick [binary_ints, expect = none]
   6.164 +sorry
   6.165 +
   6.166 +lemma "0 * y = (0::int)"
   6.167 +nitpick [unary_ints, expect = none]
   6.168 +nitpick [binary_ints, expect = none]
   6.169 +sorry
   6.170 +
   6.171 +lemma "y * 0 = (0::int)"
   6.172 +nitpick [unary_ints, expect = none]
   6.173 +nitpick [binary_ints, expect = none]
   6.174 +sorry
   6.175 +
   6.176 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::int)"
   6.177 +nitpick [unary_ints, expect = genuine]
   6.178 +nitpick [binary_ints, expect = genuine]
   6.179 +oops
   6.180 +
   6.181 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::int)"
   6.182 +nitpick [unary_ints, expect = genuine]
   6.183 +nitpick [binary_ints, expect = genuine]
   6.184 +oops
   6.185 +
   6.186 +lemma "x * y div y = (x::int)"
   6.187 +nitpick [unary_ints, expect = genuine]
   6.188 +nitpick [binary_ints, expect = genuine]
   6.189 +oops
   6.190 +
   6.191 +lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::int)"
   6.192 +nitpick [unary_ints, expect = none]
   6.193 +nitpick [binary_ints, expect = none, card = 1\<midarrow>5, bits = 1\<midarrow>5]
   6.194 +sorry
   6.195 +
   6.196 +lemma "(x * y < 0) \<longleftrightarrow> (x > 0 \<and> y < 0) \<or> (x < 0 \<and> y > (0::int))"
   6.197 +nitpick [unary_ints, expect = none]
   6.198 +nitpick [binary_ints, expect = none]
   6.199 +sorry
   6.200 +
   6.201 +lemma "-5 * 55 > (-260::int)"
   6.202 +nitpick [unary_ints, expect = none]
   6.203 +nitpick [binary_ints, expect = none]
   6.204 +nitpick [binary_ints, bits = 9, expect = genuine]
   6.205 +oops
   6.206 +
   6.207 +lemma "nat (of_nat n) = n"
   6.208 +nitpick [unary_ints, expect = none]
   6.209 +nitpick [binary_ints, expect = none]
   6.210 +sorry
   6.211 +
   6.212 +end
     7.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Dec 17 15:22:27 2009 +0100
     7.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Dec 18 12:00:29 2009 +0100
     7.3 @@ -59,7 +59,7 @@
     7.4  nitpick
     7.5  oops
     7.6  
     7.7 -subsection {* 3.5. Numbers *}
     7.8 +subsection {* 3.5. Natural Numbers and Integers *}
     7.9  
    7.10  lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
    7.11  nitpick
    7.12 @@ -121,11 +121,11 @@
    7.13  "even n \<Longrightarrow> even (Suc (Suc n))"
    7.14  
    7.15  lemma "\<exists>n. even n \<and> even (Suc n)"
    7.16 -nitpick [card nat = 100, verbose]
    7.17 +nitpick [card nat = 100, unary_ints, verbose]
    7.18  oops
    7.19  
    7.20  lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
    7.21 -nitpick [card nat = 100]
    7.22 +nitpick [card nat = 100, unary_ints, verbose]
    7.23  oops
    7.24  
    7.25  inductive even' where
    7.26 @@ -134,7 +134,7 @@
    7.27  "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
    7.28  
    7.29  lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
    7.30 -nitpick [card nat = 10, verbose, show_consts]
    7.31 +nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
    7.32  oops
    7.33  
    7.34  lemma "even' (n - 2) \<Longrightarrow> even' n"
     8.1 --- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Thu Dec 17 15:22:27 2009 +0100
     8.2 +++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Fri Dec 18 12:00:29 2009 +0100
     8.3 @@ -6,9 +6,8 @@
     8.4  *)
     8.5  
     8.6  theory Nitpick_Examples
     8.7 -imports Core_Nits Datatype_Nits Induct_Nits Manual_Nits Mini_Nits Mono_Nits
     8.8 -        Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
     8.9 +imports Core_Nits Datatype_Nits Induct_Nits Integer_Nits Manual_Nits Mini_Nits
    8.10 +        Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
    8.11          Typedef_Nits
    8.12  begin
    8.13 -
    8.14  end
     9.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Thu Dec 17 15:22:27 2009 +0100
     9.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Fri Dec 18 12:00:29 2009 +0100
     9.3 @@ -135,7 +135,7 @@
     9.4  lemma "\<forall>a. g a = a
     9.5         \<Longrightarrow> \<exists>b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\<Colon>nat).
     9.6             b\<^isub>1 < b\<^isub>11 \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 < b\<^isub>11 then a else h b\<^isub>2) x"
     9.7 -nitpick [expect = none]
     9.8 +nitpick [expect = potential]
     9.9  nitpick [dont_specialize, expect = none]
    9.10  nitpick [dont_box, expect = none]
    9.11  nitpick [dont_box, dont_specialize, expect = none]
    10.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Thu Dec 17 15:22:27 2009 +0100
    10.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Dec 18 12:00:29 2009 +0100
    10.3 @@ -11,7 +11,7 @@
    10.4  imports Main Rational
    10.5  begin
    10.6  
    10.7 -nitpick_params [card = 1\<midarrow>4, timeout = 5 s]
    10.8 +nitpick_params [card = 1\<midarrow>4, timeout = 30 s]
    10.9  
   10.10  typedef three = "{0\<Colon>nat, 1, 2}"
   10.11  by blast
   10.12 @@ -67,7 +67,7 @@
   10.13  sorry
   10.14  
   10.15  lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
   10.16 -nitpick [card = 1\<midarrow>5, timeout = 10 s, expect = genuine]
   10.17 +nitpick [card = 1\<midarrow>5, expect = genuine]
   10.18  oops
   10.19  
   10.20  lemma "True \<equiv> ((\<lambda>x\<Colon>bool. x) = (\<lambda>x. x))"
   10.21 @@ -157,15 +157,15 @@
   10.22  by (rule Rep_Nat_inverse)
   10.23  
   10.24  lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
   10.25 -nitpick [card = 1, timeout = 60 s, max_potential = 0, expect = none]
   10.26 +nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
   10.27  by (rule Zero_int_def_raw)
   10.28  
   10.29  lemma "Abs_Integ (Rep_Integ a) = a"
   10.30 -nitpick [card = 1, timeout = 60 s, max_potential = 0, expect = none]
   10.31 +nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
   10.32  by (rule Rep_Integ_inverse)
   10.33  
   10.34  lemma "Abs_list (Rep_list a) = a"
   10.35 -nitpick [card = 1\<midarrow>2, timeout = 60 s, expect = none]
   10.36 +nitpick [card = 1\<midarrow>2, expect = none]
   10.37  by (rule Rep_list_inverse)
   10.38  
   10.39  record point =
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Dec 17 15:22:27 2009 +0100
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Dec 18 12:00:29 2009 +0100
    11.3 @@ -75,6 +75,8 @@
    11.4  open Nitpick_Kodkod
    11.5  open Nitpick_Model
    11.6  
    11.7 +structure KK = Kodkod
    11.8 +
    11.9  type params = {
   11.10    cards_assigns: (typ option * int list) list,
   11.11    maxes_assigns: (styp option * int list) list,
   11.12 @@ -126,10 +128,10 @@
   11.13    rel_table: nut NameTable.table,
   11.14    liberal: bool,
   11.15    scope: scope,
   11.16 -  core: Kodkod.formula,
   11.17 -  defs: Kodkod.formula list}
   11.18 +  core: KK.formula,
   11.19 +  defs: KK.formula list}
   11.20  
   11.21 -type rich_problem = Kodkod.problem * problem_extension
   11.22 +type rich_problem = KK.problem * problem_extension
   11.23  
   11.24  (* Proof.context -> string -> term list -> Pretty.T list *)
   11.25  fun pretties_for_formulas _ _ [] = []
   11.26 @@ -344,8 +346,8 @@
   11.27      val _ = if verbose andalso binary_ints = SOME true
   11.28                 andalso exists (member (op =) [nat_T, int_T]) Ts then
   11.29                print_v (K "The option \"binary_ints\" will be ignored because \
   11.30 -                         \of the presence of rationals, reals, \"gcd\", or \
   11.31 -                         \\"lcm\" in the problem.")
   11.32 +                         \of the presence of rationals, reals, \"Suc\", \
   11.33 +                         \\"gcd\", or \"lcm\" in the problem.")
   11.34              else
   11.35                ()
   11.36      val (all_dataTs, all_free_Ts) =
   11.37 @@ -447,7 +449,7 @@
   11.38            NameTable.fold (curry Int.max o arity_of_rep o snd) rep_table 1
   11.39          val min_univ_card =
   11.40            NameTable.fold (curry Int.max o min_univ_card_of_rep o snd) rep_table
   11.41 -                         (univ_card nat_card int_card main_j0 [] Kodkod.True)
   11.42 +                         (univ_card nat_card int_card main_j0 [] KK.True)
   11.43          val _ = check_arity min_univ_card min_highest_arity
   11.44  
   11.45          val core_u = choose_reps_in_nut scope liberal rep_table false core_u
   11.46 @@ -469,7 +471,7 @@
   11.47          val core_u = rename_vars_in_nut pool rel_table core_u
   11.48          val def_us = map (rename_vars_in_nut pool rel_table) def_us
   11.49          val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
   11.50 -        (* nut -> Kodkod.formula *)
   11.51 +        (* nut -> KK.formula *)
   11.52          val to_f = kodkod_formula_from_nut bits ofs liberal kk
   11.53          val core_f = to_f core_u
   11.54          val def_fs = map to_f def_us
   11.55 @@ -510,7 +512,7 @@
   11.56            fold Integer.max (map (fst o fst) (maps fst bounds)) 0
   11.57          val formula = fold_rev s_and declarative_axioms formula
   11.58          val _ = if bits = 0 then () else check_bits bits formula
   11.59 -        val _ = if formula = Kodkod.False then ()
   11.60 +        val _ = if formula = KK.False then ()
   11.61                  else check_arity univ_card highest_arity
   11.62        in
   11.63          SOME ({comment = comment, settings = settings, univ_card = univ_card,
   11.64 @@ -525,7 +527,7 @@
   11.65                 defs = nondef_fs @ def_fs @ declarative_axioms})
   11.66        end
   11.67        handle TOO_LARGE (loc, msg) =>
   11.68 -             if loc = "Nitpick_Kodkod.check_arity"
   11.69 +             if loc = "Nitpick_KK.check_arity"
   11.70                  andalso not (Typtab.is_empty ofs) then
   11.71                 problem_for_scope liberal
   11.72                     {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
   11.73 @@ -548,10 +550,9 @@
   11.74                                   " component of scope."));
   11.75                NONE)
   11.76  
   11.77 -    (* int -> (''a * int list list) list -> ''a -> Kodkod.tuple_set *)
   11.78 +    (* int -> (''a * int list list) list -> ''a -> KK.tuple_set *)
   11.79      fun tuple_set_for_rel univ_card =
   11.80 -      Kodkod.TupleSet o map (kk_tuple debug univ_card) o the
   11.81 -      oo AList.lookup (op =)
   11.82 +      KK.TupleSet o map (kk_tuple debug univ_card) o the oo AList.lookup (op =)
   11.83  
   11.84      val word_model = if falsify then "counterexample" else "model"
   11.85  
   11.86 @@ -566,7 +567,7 @@
   11.87        List.app (Unsynchronized.change checked_problems o Option.map o cons
   11.88                  o nth problems)
   11.89  
   11.90 -    (* bool -> Kodkod.raw_bound list -> problem_extension -> bool option *)
   11.91 +    (* bool -> KK.raw_bound list -> problem_extension -> bool option *)
   11.92      fun print_and_check_model genuine bounds
   11.93              ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
   11.94               : problem_extension) =
   11.95 @@ -663,7 +664,7 @@
   11.96        let
   11.97          val max_potential = Int.max (0, max_potential)
   11.98          val max_genuine = Int.max (0, max_genuine)
   11.99 -        (* bool -> int * Kodkod.raw_bound list -> bool option *)
  11.100 +        (* bool -> int * KK.raw_bound list -> bool option *)
  11.101          fun print_and_check genuine (j, bounds) =
  11.102            print_and_check_model genuine bounds (snd (nth problems j))
  11.103          val max_solutions = max_potential + max_genuine
  11.104 @@ -672,15 +673,15 @@
  11.105          if max_solutions <= 0 then
  11.106            (0, 0, donno)
  11.107          else
  11.108 -          case Kodkod.solve_any_problem overlord deadline max_threads
  11.109 -                                        max_solutions (map fst problems) of
  11.110 -            Kodkod.NotInstalled =>
  11.111 +          case KK.solve_any_problem overlord deadline max_threads max_solutions
  11.112 +                                    (map fst problems) of
  11.113 +            KK.NotInstalled =>
  11.114              (print_m install_kodkodi_message;
  11.115               (max_potential, max_genuine, donno + 1))
  11.116 -          | Kodkod.Normal ([], unsat_js) =>
  11.117 +          | KK.Normal ([], unsat_js) =>
  11.118              (update_checked_problems problems unsat_js;
  11.119               (max_potential, max_genuine, donno))
  11.120 -          | Kodkod.Normal (sat_ps, unsat_js) =>
  11.121 +          | KK.Normal (sat_ps, unsat_js) =>
  11.122              let
  11.123                val (lib_ps, con_ps) =
  11.124                  List.partition (#liberal o snd o nth problems o fst) sat_ps
  11.125 @@ -739,13 +740,12 @@
  11.126                      in solve_any_problem 0 max_genuine donno false problems end
  11.127                  end
  11.128              end
  11.129 -          | Kodkod.TimedOut unsat_js =>
  11.130 +          | KK.TimedOut unsat_js =>
  11.131              (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
  11.132 -          | Kodkod.Interrupted NONE =>
  11.133 -            (checked_problems := NONE; do_interrupted ())
  11.134 -          | Kodkod.Interrupted (SOME unsat_js) =>
  11.135 +          | KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ())
  11.136 +          | KK.Interrupted (SOME unsat_js) =>
  11.137              (update_checked_problems problems unsat_js; do_interrupted ())
  11.138 -          | Kodkod.Error (s, unsat_js) =>
  11.139 +          | KK.Error (s, unsat_js) =>
  11.140              (update_checked_problems problems unsat_js;
  11.141               print_v (K ("Kodkod error: " ^ s ^ "."));
  11.142               (max_potential, max_genuine, donno + 1))
  11.143 @@ -787,8 +787,8 @@
  11.144               SOME problem =>
  11.145               (problems
  11.146                |> (null problems orelse
  11.147 -                  not (Kodkod.problems_equivalent (fst problem)
  11.148 -                                                  (fst (hd problems))))
  11.149 +                  not (KK.problems_equivalent (fst problem)
  11.150 +                                              (fst (hd problems))))
  11.151                    ? cons problem, donno)
  11.152             | NONE => (problems, donno + 1))
  11.153          val (problems, donno) =
  11.154 @@ -832,7 +832,7 @@
  11.155             "") ^ "."
  11.156        end
  11.157  
  11.158 -    (* int -> int -> scope list -> int * int * int -> Kodkod.outcome *)
  11.159 +    (* int -> int -> scope list -> int * int * int -> KK.outcome *)
  11.160      fun run_batches _ _ [] (max_potential, max_genuine, donno) =
  11.161          if donno > 0 andalso max_genuine > 0 then
  11.162            (print_m (fn () => excipit "ran out of some resource"); "unknown")
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Dec 17 15:22:27 2009 +0100
    12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Dec 18 12:00:29 2009 +0100
    12.3 @@ -968,7 +968,8 @@
    12.4         | @{typ unit} => 1
    12.5         | Type _ =>
    12.6           (case datatype_constrs ext_ctxt T of
    12.7 -            [] => if is_integer_type T then 0 else raise SAME ()
    12.8 +            [] => if is_integer_type T orelse is_bit_type T then 0
    12.9 +                  else raise SAME ()
   12.10            | constrs =>
   12.11              let
   12.12                val constr_cards =
   12.13 @@ -1220,7 +1221,7 @@
   12.14  
   12.15  (* Proof.context -> term list -> const_table *)
   12.16  fun const_def_table ctxt ts =
   12.17 -  table_for (rev o map prop_of o Nitpick_Defs.get) ctxt
   12.18 +  table_for (map prop_of o Nitpick_Defs.get) ctxt
   12.19    |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
   12.20            (map pair_for_prop ts)
   12.21  (* term list -> const_table *)
   12.22 @@ -3350,13 +3351,13 @@
   12.23  (* term -> bool *)
   12.24  fun may_use_binary_ints (t1 $ t2) =
   12.25      may_use_binary_ints t1 andalso may_use_binary_ints t2
   12.26 -  | may_use_binary_ints (Const (s, _)) =
   12.27 +  | may_use_binary_ints (t as Const (s, _)) =
   12.28 +    t <> @{const Suc} andalso
   12.29      not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
   12.30 -                        @{const_name Frac}, @{const_name norm_frac},
   12.31 -                        @{const_name nat_gcd}, @{const_name nat_lcm}] s)
   12.32 +                        @{const_name nat_gcd}, @{const_name nat_lcm},
   12.33 +                        @{const_name Frac}, @{const_name norm_frac}] s)
   12.34    | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
   12.35    | may_use_binary_ints _ = true
   12.36 -
   12.37  fun should_use_binary_ints (t1 $ t2) =
   12.38      should_use_binary_ints t1 orelse should_use_binary_ints t2
   12.39    | should_use_binary_ints (Const (s, _)) =
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Dec 17 15:22:27 2009 +0100
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Dec 18 12:00:29 2009 +0100
    13.3 @@ -49,44 +49,46 @@
    13.4  open Nitpick_Rep
    13.5  open Nitpick_Nut
    13.6  
    13.7 -type nfa_transition = Kodkod.rel_expr * typ
    13.8 +structure KK = Kodkod
    13.9 +
   13.10 +type nfa_transition = KK.rel_expr * typ
   13.11  type nfa_entry = typ * nfa_transition list
   13.12  type nfa_table = nfa_entry list
   13.13  
   13.14  structure NfaGraph = Graph(type key = typ val ord = TermOrd.typ_ord)
   13.15  
   13.16 -(* int -> Kodkod.int_expr list *)
   13.17 -fun flip_nums n = index_seq 1 n @ [0] |> map Kodkod.Num
   13.18 +(* int -> KK.int_expr list *)
   13.19 +fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
   13.20  
   13.21 -(* int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int *)
   13.22 +(* int -> int -> int -> KK.bound list -> KK.formula -> int *)
   13.23  fun univ_card nat_card int_card main_j0 bounds formula =
   13.24    let
   13.25 -    (* Kodkod.rel_expr -> int -> int *)
   13.26 +    (* KK.rel_expr -> int -> int *)
   13.27      fun rel_expr_func r k =
   13.28        Int.max (k, case r of
   13.29 -                    Kodkod.Atom j => j + 1
   13.30 -                  | Kodkod.AtomSeq (k', j0) => j0 + k'
   13.31 +                    KK.Atom j => j + 1
   13.32 +                  | KK.AtomSeq (k', j0) => j0 + k'
   13.33                    | _ => 0)
   13.34 -    (* Kodkod.tuple -> int -> int *)
   13.35 +    (* KK.tuple -> int -> int *)
   13.36      fun tuple_func t k =
   13.37        case t of
   13.38 -        Kodkod.Tuple js => fold Integer.max (map (Integer.add 1) js) k
   13.39 +        KK.Tuple js => fold Integer.max (map (Integer.add 1) js) k
   13.40        | _ => k
   13.41 -    (* Kodkod.tuple_set -> int -> int *)
   13.42 +    (* KK.tuple_set -> int -> int *)
   13.43      fun tuple_set_func ts k =
   13.44 -      Int.max (k, case ts of Kodkod.TupleAtomSeq (k', j0) => j0 + k' | _ => 0)
   13.45 +      Int.max (k, case ts of KK.TupleAtomSeq (k', j0) => j0 + k' | _ => 0)
   13.46      val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
   13.47                    int_expr_func = K I}
   13.48      val tuple_F = {tuple_func = tuple_func, tuple_set_func = tuple_set_func}
   13.49 -    val card = fold (Kodkod.fold_bound expr_F tuple_F) bounds 1
   13.50 -               |> Kodkod.fold_formula expr_F formula
   13.51 +    val card = fold (KK.fold_bound expr_F tuple_F) bounds 1
   13.52 +               |> KK.fold_formula expr_F formula
   13.53    in Int.max (main_j0 + fold Integer.max [2, nat_card, int_card] 0, card) end
   13.54  
   13.55 -(* int -> Kodkod.formula -> unit *)
   13.56 +(* int -> KK.formula -> unit *)
   13.57  fun check_bits bits formula =
   13.58    let
   13.59 -    (* Kodkod.int_expr -> unit -> unit *)
   13.60 -    fun int_expr_func (Kodkod.Num k) () =
   13.61 +    (* KK.int_expr -> unit -> unit *)
   13.62 +    fun int_expr_func (KK.Num k) () =
   13.63          if is_twos_complement_representable bits k then
   13.64            ()
   13.65          else
   13.66 @@ -96,39 +98,38 @@
   13.67        | int_expr_func _ () = ()
   13.68      val expr_F = {formula_func = K I, rel_expr_func = K I,
   13.69                    int_expr_func = int_expr_func}
   13.70 -  in Kodkod.fold_formula expr_F formula () end
   13.71 +  in KK.fold_formula expr_F formula () end
   13.72  
   13.73  (* int -> int -> unit *)
   13.74  fun check_arity univ_card n =
   13.75 -  if n > Kodkod.max_arity univ_card then
   13.76 +  if n > KK.max_arity univ_card then
   13.77      raise TOO_LARGE ("Nitpick_Kodkod.check_arity",
   13.78                       "arity " ^ string_of_int n ^ " too large for universe of \
   13.79                       \cardinality " ^ string_of_int univ_card)
   13.80    else
   13.81      ()
   13.82  
   13.83 -(* bool -> int -> int list -> Kodkod.tuple *)
   13.84 +(* bool -> int -> int list -> KK.tuple *)
   13.85  fun kk_tuple debug univ_card js =
   13.86    if debug then
   13.87 -    Kodkod.Tuple js
   13.88 +    KK.Tuple js
   13.89    else
   13.90 -    Kodkod.TupleIndex (length js,
   13.91 -                       fold (fn j => fn accum => accum * univ_card + j) js 0)
   13.92 +    KK.TupleIndex (length js,
   13.93 +                   fold (fn j => fn accum => accum * univ_card + j) js 0)
   13.94  
   13.95 -(* (int * int) list -> Kodkod.tuple_set *)
   13.96 -val tuple_set_from_atom_schema =
   13.97 -  foldl1 Kodkod.TupleProduct o map Kodkod.TupleAtomSeq
   13.98 -(* rep -> Kodkod.tuple_set *)
   13.99 +(* (int * int) list -> KK.tuple_set *)
  13.100 +val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq
  13.101 +(* rep -> KK.tuple_set *)
  13.102  val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep
  13.103  
  13.104 -(* int -> Kodkod.tuple_set *)
  13.105 -val single_atom = Kodkod.TupleSet o single o Kodkod.Tuple o single
  13.106 -(* int -> Kodkod.int_bound list *)
  13.107 +(* int -> KK.tuple_set *)
  13.108 +val single_atom = KK.TupleSet o single o KK.Tuple o single
  13.109 +(* int -> KK.int_bound list *)
  13.110  fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
  13.111 -(* int -> int -> Kodkod.int_bound list *)
  13.112 +(* int -> int -> KK.int_bound list *)
  13.113  fun pow_of_two_int_bounds bits j0 univ_card =
  13.114    let
  13.115 -    (* int -> int -> int -> Kodkod.int_bound list *)
  13.116 +    (* int -> int -> int -> KK.int_bound list *)
  13.117      fun aux 0  _ _ = []
  13.118        | aux 1 pow_of_two j =
  13.119          if j < univ_card then [(SOME (~ pow_of_two), [single_atom j])] else []
  13.120 @@ -137,11 +138,11 @@
  13.121          aux (iter - 1) (2 * pow_of_two) (j + 1)
  13.122    in aux (bits + 1) 1 j0 end
  13.123  
  13.124 -(* Kodkod.formula -> Kodkod.n_ary_index list *)
  13.125 +(* KK.formula -> KK.n_ary_index list *)
  13.126  fun built_in_rels_in_formula formula =
  13.127    let
  13.128 -    (* Kodkod.rel_expr -> Kodkod.n_ary_index list -> Kodkod.n_ary_index list *)
  13.129 -    fun rel_expr_func (r as Kodkod.Rel (x as (n, j))) =
  13.130 +    (* KK.rel_expr -> KK.n_ary_index list -> KK.n_ary_index list *)
  13.131 +    fun rel_expr_func (r as KK.Rel (x as (n, j))) =
  13.132          if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then
  13.133            I
  13.134          else
  13.135 @@ -151,7 +152,7 @@
  13.136        | rel_expr_func _ = I
  13.137      val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
  13.138                    int_expr_func = K I}
  13.139 -  in Kodkod.fold_formula expr_F formula [] end
  13.140 +  in KK.fold_formula expr_F formula [] end
  13.141  
  13.142  val max_table_size = 65536
  13.143  
  13.144 @@ -163,7 +164,7 @@
  13.145    else
  13.146      ()
  13.147  
  13.148 -(* bool -> int -> int * int -> (int -> int) -> Kodkod.tuple list *)
  13.149 +(* bool -> int -> int * int -> (int -> int) -> KK.tuple list *)
  13.150  fun tabulate_func1 debug univ_card (k, j0) f =
  13.151    (check_table_size k;
  13.152     map_filter (fn j1 => let val j2 = f j1 in
  13.153 @@ -172,7 +173,7 @@
  13.154                            else
  13.155                              NONE
  13.156                          end) (index_seq 0 k))
  13.157 -(* bool -> int -> int * int -> int -> (int * int -> int) -> Kodkod.tuple list *)
  13.158 +(* bool -> int -> int * int -> int -> (int * int -> int) -> KK.tuple list *)
  13.159  fun tabulate_op2 debug univ_card (k, j0) res_j0 f =
  13.160    (check_table_size (k * k);
  13.161     map_filter (fn j => let
  13.162 @@ -187,7 +188,7 @@
  13.163                             NONE
  13.164                         end) (index_seq 0 (k * k)))
  13.165  (* bool -> int -> int * int -> int -> (int * int -> int * int)
  13.166 -   -> Kodkod.tuple list *)
  13.167 +   -> KK.tuple list *)
  13.168  fun tabulate_op2_2 debug univ_card (k, j0) res_j0 f =
  13.169    (check_table_size (k * k);
  13.170     map_filter (fn j => let
  13.171 @@ -202,13 +203,13 @@
  13.172                           else
  13.173                             NONE
  13.174                         end) (index_seq 0 (k * k)))
  13.175 -(* bool -> int -> int * int -> (int * int -> int) -> Kodkod.tuple list *)
  13.176 +(* bool -> int -> int * int -> (int * int -> int) -> KK.tuple list *)
  13.177  fun tabulate_nat_op2 debug univ_card (k, j0) f =
  13.178    tabulate_op2 debug univ_card (k, j0) j0 (atom_for_nat (k, 0) o f)
  13.179  fun tabulate_int_op2 debug univ_card (k, j0) f =
  13.180    tabulate_op2 debug univ_card (k, j0) j0
  13.181                 (atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0)))
  13.182 -(* bool -> int -> int * int -> (int * int -> int * int) -> Kodkod.tuple list *)
  13.183 +(* bool -> int -> int * int -> (int * int -> int * int) -> KK.tuple list *)
  13.184  fun tabulate_int_op2_2 debug univ_card (k, j0) f =
  13.185    tabulate_op2_2 debug univ_card (k, j0) j0
  13.186                   (pairself (atom_for_int (k, 0)) o f
  13.187 @@ -228,7 +229,7 @@
  13.188    else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end
  13.189  
  13.190  (* bool -> int -> int -> int -> int -> int * int
  13.191 -   -> string * bool * Kodkod.tuple list *)
  13.192 +   -> string * bool * KK.tuple list *)
  13.193  fun tabulate_built_in_rel debug univ_card nat_card int_card j0 (x as (n, _)) =
  13.194    (check_arity univ_card n;
  13.195     if x = not3_rel then
  13.196 @@ -269,15 +270,14 @@
  13.197     else
  13.198       raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation"))
  13.199  
  13.200 -(* bool -> int -> int -> int -> int -> int * int -> Kodkod.rel_expr
  13.201 -   -> Kodkod.bound *)
  13.202 +(* bool -> int -> int -> int -> int -> int * int -> KK.rel_expr -> KK.bound *)
  13.203  fun bound_for_built_in_rel debug univ_card nat_card int_card j0 x =
  13.204    let
  13.205      val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card
  13.206                                             j0 x
  13.207 -  in ([(x, nick)], [Kodkod.TupleSet ts]) end
  13.208 +  in ([(x, nick)], [KK.TupleSet ts]) end
  13.209  
  13.210 -(* bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list *)
  13.211 +(* bool -> int -> int -> int -> int -> KK.formula -> KK.bound list *)
  13.212  fun bounds_for_built_in_rels_in_formula debug univ_card nat_card int_card j0 =
  13.213    map (bound_for_built_in_rel debug univ_card nat_card int_card j0)
  13.214    o built_in_rels_in_formula
  13.215 @@ -288,7 +288,7 @@
  13.216    (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
  13.217     else "") ^ " : " ^ string_for_rep R
  13.218  
  13.219 -(* Proof.context -> bool -> nut -> Kodkod.bound *)
  13.220 +(* Proof.context -> bool -> nut -> KK.bound *)
  13.221  fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
  13.222      ([(x, bound_comment ctxt debug nick T R)],
  13.223       if nick = @{const_name bisim_iterator_max} then
  13.224 @@ -296,11 +296,11 @@
  13.225           Atom (k, j0) => [single_atom (k - 1 + j0)]
  13.226         | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
  13.227       else
  13.228 -       [Kodkod.TupleSet [], upper_bound_for_rep R])
  13.229 +       [KK.TupleSet [], upper_bound_for_rep R])
  13.230    | bound_for_plain_rel _ _ u =
  13.231      raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
  13.232  
  13.233 -(* Proof.context -> bool -> dtype_spec list -> nut -> Kodkod.bound *)
  13.234 +(* Proof.context -> bool -> dtype_spec list -> nut -> KK.bound *)
  13.235  fun bound_for_sel_rel ctxt debug dtypes
  13.236          (FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2),
  13.237                    nick)) =
  13.238 @@ -310,26 +310,24 @@
  13.239      in
  13.240        ([(x, bound_comment ctxt debug nick T R)],
  13.241         if explicit_max = 0 then
  13.242 -         [Kodkod.TupleSet []]
  13.243 +         [KK.TupleSet []]
  13.244         else
  13.245 -         let val ts = Kodkod.TupleAtomSeq (epsilon - delta, delta + j0) in
  13.246 +         let val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0) in
  13.247             if R2 = Formula Neut then
  13.248 -             [ts] |> not exclusive ? cons (Kodkod.TupleSet [])
  13.249 +             [ts] |> not exclusive ? cons (KK.TupleSet [])
  13.250             else
  13.251 -             [Kodkod.TupleSet [],
  13.252 -              Kodkod.TupleProduct (ts, upper_bound_for_rep R2)]
  13.253 +             [KK.TupleSet [], KK.TupleProduct (ts, upper_bound_for_rep R2)]
  13.254           end)
  13.255      end
  13.256    | bound_for_sel_rel _ _ _ u =
  13.257      raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u])
  13.258  
  13.259 -(* Kodkod.bound list -> Kodkod.bound list *)
  13.260 +(* KK.bound list -> KK.bound list *)
  13.261  fun merge_bounds bs =
  13.262    let
  13.263 -    (* Kodkod.bound -> int *)
  13.264 +    (* KK.bound -> int *)
  13.265      fun arity (zs, _) = fst (fst (hd zs))
  13.266 -    (* Kodkod.bound list -> Kodkod.bound -> Kodkod.bound list
  13.267 -       -> Kodkod.bound list *)
  13.268 +    (* KK.bound list -> KK.bound -> KK.bound list -> KK.bound list *)
  13.269      fun add_bound ds b [] = List.revAppend (ds, [b])
  13.270        | add_bound ds b (c :: cs) =
  13.271          if arity b = arity c andalso snd b = snd c then
  13.272 @@ -338,40 +336,40 @@
  13.273            add_bound (c :: ds) b cs
  13.274    in fold (add_bound []) bs [] end
  13.275  
  13.276 -(* int -> int -> Kodkod.rel_expr list *)
  13.277 -fun unary_var_seq j0 n = map (curry Kodkod.Var 1) (index_seq j0 n)
  13.278 +(* int -> int -> KK.rel_expr list *)
  13.279 +fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n)
  13.280  
  13.281 -(* int list -> Kodkod.rel_expr *)
  13.282 -val singleton_from_combination = foldl1 Kodkod.Product o map Kodkod.Atom
  13.283 -(* rep -> Kodkod.rel_expr list *)
  13.284 +(* int list -> KK.rel_expr *)
  13.285 +val singleton_from_combination = foldl1 KK.Product o map KK.Atom
  13.286 +(* rep -> KK.rel_expr list *)
  13.287  fun all_singletons_for_rep R =
  13.288    if is_lone_rep R then
  13.289      all_combinations_for_rep R |> map singleton_from_combination
  13.290    else
  13.291      raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R])
  13.292  
  13.293 -(* Kodkod.rel_expr -> Kodkod.rel_expr list *)
  13.294 -fun unpack_products (Kodkod.Product (r1, r2)) =
  13.295 +(* KK.rel_expr -> KK.rel_expr list *)
  13.296 +fun unpack_products (KK.Product (r1, r2)) =
  13.297      unpack_products r1 @ unpack_products r2
  13.298    | unpack_products r = [r]
  13.299 -fun unpack_joins (Kodkod.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2
  13.300 +fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2
  13.301    | unpack_joins r = [r]
  13.302  
  13.303 -(* rep -> Kodkod.rel_expr *)
  13.304 +(* rep -> KK.rel_expr *)
  13.305  val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep
  13.306  fun full_rel_for_rep R =
  13.307    case atom_schema_of_rep R of
  13.308      [] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R])
  13.309 -  | schema => foldl1 Kodkod.Product (map Kodkod.AtomSeq schema)
  13.310 +  | schema => foldl1 KK.Product (map KK.AtomSeq schema)
  13.311  
  13.312 -(* int -> int list -> Kodkod.decl list *)
  13.313 +(* int -> int list -> KK.decl list *)
  13.314  fun decls_for_atom_schema j0 schema =
  13.315 -  map2 (fn j => fn x => Kodkod.DeclOne ((1, j), Kodkod.AtomSeq x))
  13.316 +  map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x))
  13.317         (index_seq j0 (length schema)) schema
  13.318  
  13.319  (* The type constraint below is a workaround for a Poly/ML bug. *)
  13.320  
  13.321 -(* kodkod_constrs -> rep -> Kodkod.rel_expr -> Kodkod.formula *)
  13.322 +(* kodkod_constrs -> rep -> KK.rel_expr -> KK.formula *)
  13.323  fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs)
  13.324                       R r =
  13.325    let val body_R = body_rep R in
  13.326 @@ -380,13 +378,13 @@
  13.327          val binder_schema = atom_schema_of_reps (binder_reps R)
  13.328          val body_schema = atom_schema_of_rep body_R
  13.329          val one = is_one_rep body_R
  13.330 -        val opt_x = case r of Kodkod.Rel x => SOME x | _ => NONE
  13.331 +        val opt_x = case r of KK.Rel x => SOME x | _ => NONE
  13.332        in
  13.333          if opt_x <> NONE andalso length binder_schema = 1
  13.334             andalso length body_schema = 1 then
  13.335 -          (if one then Kodkod.Function else Kodkod.Functional)
  13.336 -              (the opt_x, Kodkod.AtomSeq (hd binder_schema),
  13.337 -               Kodkod.AtomSeq (hd body_schema))
  13.338 +          (if one then KK.Function else KK.Functional)
  13.339 +              (the opt_x, KK.AtomSeq (hd binder_schema),
  13.340 +               KK.AtomSeq (hd body_schema))
  13.341          else
  13.342            let
  13.343              val decls = decls_for_atom_schema ~1 binder_schema
  13.344 @@ -395,12 +393,12 @@
  13.345            in kk_all decls (kk_xone (fold kk_join vars r)) end
  13.346        end
  13.347      else
  13.348 -      Kodkod.True
  13.349 +      KK.True
  13.350    end
  13.351 -fun kk_n_ary_function kk R (r as Kodkod.Rel x) =
  13.352 +fun kk_n_ary_function kk R (r as KK.Rel x) =
  13.353      if not (is_opt_rep R) then
  13.354        if x = suc_rel then
  13.355 -        Kodkod.False
  13.356 +        KK.False
  13.357        else if x = nat_add_rel then
  13.358          formula_for_bool (card_of_rep (body_rep R) = 1)
  13.359        else if x = nat_multiply_rel then
  13.360 @@ -408,58 +406,56 @@
  13.361        else
  13.362          d_n_ary_function kk R r
  13.363      else if x = nat_subtract_rel then
  13.364 -      Kodkod.True
  13.365 +      KK.True
  13.366      else
  13.367        d_n_ary_function kk R r
  13.368    | kk_n_ary_function kk R r = d_n_ary_function kk R r
  13.369  
  13.370 -(* kodkod_constrs -> Kodkod.rel_expr list -> Kodkod.formula *)
  13.371 -fun kk_disjoint_sets _ [] = Kodkod.True
  13.372 +(* kodkod_constrs -> KK.rel_expr list -> KK.formula *)
  13.373 +fun kk_disjoint_sets _ [] = KK.True
  13.374    | kk_disjoint_sets (kk as {kk_and, kk_no, kk_intersect, ...} : kodkod_constrs)
  13.375                       (r :: rs) =
  13.376      fold (kk_and o kk_no o kk_intersect r) rs (kk_disjoint_sets kk rs)
  13.377  
  13.378 -(* int -> kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr)
  13.379 -   -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.380 +(* int -> kodkod_constrs -> (KK.rel_expr -> KK.rel_expr) -> KK.rel_expr
  13.381 +   -> KK.rel_expr *)
  13.382  fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =
  13.383    if inline_rel_expr r then
  13.384      f r
  13.385    else
  13.386 -    let val x = (Kodkod.arity_of_rel_expr r, j) in
  13.387 -      kk_rel_let [Kodkod.AssignRelReg (x, r)] (f (Kodkod.RelReg x))
  13.388 +    let val x = (KK.arity_of_rel_expr r, j) in
  13.389 +      kk_rel_let [KK.AssignRelReg (x, r)] (f (KK.RelReg x))
  13.390      end
  13.391 -(* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr) -> Kodkod.rel_expr
  13.392 -   -> Kodkod.rel_expr *)
  13.393 +(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr) -> KK.rel_expr
  13.394 +   -> KK.rel_expr *)
  13.395  val single_rel_rel_let = basic_rel_rel_let 0
  13.396 -(* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
  13.397 -   -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.398 +(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr) -> KK.rel_expr
  13.399 +   -> KK.rel_expr -> KK.rel_expr *)
  13.400  fun double_rel_rel_let kk f r1 r2 =
  13.401    single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
  13.402 -(* kodkod_constrs
  13.403 -   -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
  13.404 -   -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr
  13.405 -   -> Kodkod.rel_expr *)
  13.406 +(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr)
  13.407 +   -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)
  13.408  fun tripl_rel_rel_let kk f r1 r2 r3 =
  13.409    double_rel_rel_let kk
  13.410        (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
  13.411  
  13.412 -(* kodkod_constrs -> int -> Kodkod.formula -> Kodkod.rel_expr *)
  13.413 +(* kodkod_constrs -> int -> KK.formula -> KK.rel_expr *)
  13.414  fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f =
  13.415 -  kk_rel_if f (Kodkod.Atom (j0 + 1)) (Kodkod.Atom j0)
  13.416 -(* kodkod_constrs -> rep -> Kodkod.formula -> Kodkod.rel_expr *)
  13.417 +  kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0)
  13.418 +(* kodkod_constrs -> rep -> KK.formula -> KK.rel_expr *)
  13.419  fun rel_expr_from_formula kk R f =
  13.420    case unopt_rep R of
  13.421      Atom (2, j0) => atom_from_formula kk j0 f
  13.422    | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R])
  13.423  
  13.424 -(* kodkod_cotrs -> int -> int -> Kodkod.rel_expr -> Kodkod.rel_expr list *)
  13.425 +(* kodkod_cotrs -> int -> int -> KK.rel_expr -> KK.rel_expr list *)
  13.426  fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity
  13.427                            num_chunks r =
  13.428    List.tabulate (num_chunks, fn j => kk_project_seq r (j * chunk_arity)
  13.429                                                      chunk_arity)
  13.430  
  13.431 -(* kodkod_constrs -> bool -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr
  13.432 -   -> Kodkod.rel_expr *)
  13.433 +(* kodkod_constrs -> bool -> rep -> rep -> KK.rel_expr -> KK.rel_expr
  13.434 +   -> KK.rel_expr *)
  13.435  fun kk_n_fold_join
  13.436          (kk as {kk_intersect, kk_product, kk_join, kk_project_seq, ...}) one R1
  13.437          res_R r1 r2 =
  13.438 @@ -479,8 +475,8 @@
  13.439              arity1 (arity_of_rep res_R)
  13.440      end
  13.441  
  13.442 -(* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr list
  13.443 -   -> Kodkod.rel_expr list -> Kodkod.rel_expr *)
  13.444 +(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr list
  13.445 +   -> KK.rel_expr list -> KK.rel_expr *)
  13.446  fun kk_case_switch (kk as {kk_union, kk_product, ...}) R1 R2 r rs1 rs2 =
  13.447    if rs1 = rs2 then r
  13.448    else kk_n_fold_join kk true R1 R2 r (fold1 kk_union (map2 kk_product rs1 rs2))
  13.449 @@ -488,7 +484,7 @@
  13.450  val lone_rep_fallback_max_card = 4096
  13.451  val some_j0 = 0
  13.452  
  13.453 -(* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.454 +(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
  13.455  fun lone_rep_fallback kk new_R old_R r =
  13.456    if old_R = new_R then
  13.457      r
  13.458 @@ -505,7 +501,7 @@
  13.459        else
  13.460          raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R])
  13.461      end
  13.462 -(* kodkod_constrs -> int * int -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.463 +(* kodkod_constrs -> int * int -> rep -> KK.rel_expr -> KK.rel_expr *)
  13.464  and atom_from_rel_expr kk (x as (k, j0)) old_R r =
  13.465    case old_R of
  13.466      Func (R1, R2) =>
  13.467 @@ -518,7 +514,7 @@
  13.468      end
  13.469    | Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R])
  13.470    | _ => lone_rep_fallback kk (Atom x) old_R r
  13.471 -(* kodkod_constrs -> rep list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.472 +(* kodkod_constrs -> rep list -> rep -> KK.rel_expr -> KK.rel_expr *)
  13.473  and struct_from_rel_expr kk Rs old_R r =
  13.474    case old_R of
  13.475      Atom _ => lone_rep_fallback kk (Struct Rs) old_R r
  13.476 @@ -542,7 +538,7 @@
  13.477          lone_rep_fallback kk (Struct Rs) old_R r
  13.478      end
  13.479    | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R])
  13.480 -(* kodkod_constrs -> int -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.481 +(* kodkod_constrs -> int -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
  13.482  and vect_from_rel_expr kk k R old_R r =
  13.483    case old_R of
  13.484      Atom _ => lone_rep_fallback kk (Vect (k, R)) old_R r
  13.485 @@ -565,7 +561,7 @@
  13.486                                           (kk_n_fold_join kk true R1 R2 arg_r r))
  13.487                 (all_singletons_for_rep R1))
  13.488    | _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
  13.489 -(* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.490 +(* kodkod_constrs -> rep -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
  13.491  and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r =
  13.492      let
  13.493        val dom_card = card_of_rep R1
  13.494 @@ -594,9 +590,9 @@
  13.495         let
  13.496           val args_rs = all_singletons_for_rep R1
  13.497           val vals_rs = unpack_vect_in_chunks kk 1 k r
  13.498 -         (* Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.499 +         (* KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)
  13.500           fun empty_or_singleton_set_for arg_r val_r =
  13.501 -           #kk_join kk val_r (#kk_product kk (Kodkod.Atom (j0 + 1)) arg_r)
  13.502 +           #kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r)
  13.503         in
  13.504           fold1 (#kk_union kk) (map2 empty_or_singleton_set_for args_rs vals_rs)
  13.505         end
  13.506 @@ -613,11 +609,11 @@
  13.507             #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r)
  13.508           end
  13.509       | Func (Unit, (Atom (2, j0))) =>
  13.510 -       #kk_rel_if kk (#kk_rel_eq kk r (Kodkod.Atom (j0 + 1)))
  13.511 +       #kk_rel_if kk (#kk_rel_eq kk r (KK.Atom (j0 + 1)))
  13.512                    (full_rel_for_rep R1) (empty_rel_for_rep R1)
  13.513       | Func (R1', Atom (2, j0)) =>
  13.514         func_from_no_opt_rel_expr kk R1 (Formula Neut)
  13.515 -           (Func (R1', Formula Neut)) (#kk_join kk r (Kodkod.Atom (j0 + 1)))
  13.516 +           (Func (R1', Formula Neut)) (#kk_join kk r (KK.Atom (j0 + 1)))
  13.517       | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
  13.518                         [old_R, Func (R1, Formula Neut)]))
  13.519    | func_from_no_opt_rel_expr kk R1 R2 old_R r =
  13.520 @@ -633,14 +629,14 @@
  13.521           Atom (x as (2, j0)) =>
  13.522           let val schema = atom_schema_of_rep R1 in
  13.523             if length schema = 1 then
  13.524 -             #kk_override kk (#kk_product kk (Kodkod.AtomSeq (hd schema))
  13.525 -                                             (Kodkod.Atom j0))
  13.526 -                             (#kk_product kk r (Kodkod.Atom (j0 + 1)))
  13.527 +             #kk_override kk (#kk_product kk (KK.AtomSeq (hd schema))
  13.528 +                                             (KK.Atom j0))
  13.529 +                             (#kk_product kk r (KK.Atom (j0 + 1)))
  13.530             else
  13.531               let
  13.532                 val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema))
  13.533                          |> rel_expr_from_rel_expr kk R1' R1
  13.534 -               val r2 = Kodkod.Var (1, ~(length schema) - 1)
  13.535 +               val r2 = KK.Var (1, ~(length schema) - 1)
  13.536                 val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r)
  13.537               in
  13.538                 #kk_comprehension kk (decls_for_atom_schema ~1 (schema @ [x]))
  13.539 @@ -652,7 +648,7 @@
  13.540      | Func (Unit, R2') =>
  13.541        let val j0 = some_j0 in
  13.542          func_from_no_opt_rel_expr kk R1 R2 (Func (Atom (1, j0), R2'))
  13.543 -                                  (#kk_product kk (Kodkod.Atom j0) r)
  13.544 +                                  (#kk_product kk (KK.Atom j0) r)
  13.545        end
  13.546      | Func (R1', R2') =>
  13.547        if R1 = R1' andalso R2 = R2' then
  13.548 @@ -677,7 +673,7 @@
  13.549          end
  13.550      | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
  13.551                        [old_R, Func (R1, R2)])
  13.552 -(* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.553 +(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
  13.554  and rel_expr_from_rel_expr kk new_R old_R r =
  13.555    let
  13.556      val unopt_old_R = unopt_rep old_R
  13.557 @@ -697,43 +693,43 @@
  13.558                           [old_R, new_R]))
  13.559            unopt_old_R r
  13.560    end
  13.561 -(* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.562 +(* kodkod_constrs -> rep -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
  13.563  and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2))
  13.564  
  13.565 -(* kodkod_constrs -> typ -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.566 +(* kodkod_constrs -> typ -> KK.rel_expr -> KK.rel_expr *)
  13.567  fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r =
  13.568 -  kk_join r (Kodkod.Rel (if T = @{typ "unsigned_bit word"} then
  13.569 -                           unsigned_bit_word_sel_rel
  13.570 -                         else
  13.571 -                           signed_bit_word_sel_rel))
  13.572 -(* kodkod_constrs -> typ -> Kodkod.rel_expr -> Kodkod.int_expr *)
  13.573 -val int_expr_from_atom = Kodkod.SetSum ooo bit_set_from_atom
  13.574 -(* kodkod_constrs -> typ -> rep -> Kodkod.int_expr -> Kodkod.rel_expr *)
  13.575 +  kk_join r (KK.Rel (if T = @{typ "unsigned_bit word"} then
  13.576 +                       unsigned_bit_word_sel_rel
  13.577 +                     else
  13.578 +                       signed_bit_word_sel_rel))
  13.579 +(* kodkod_constrs -> typ -> KK.rel_expr -> KK.int_expr *)
  13.580 +val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom
  13.581 +(* kodkod_constrs -> typ -> rep -> KK.int_expr -> KK.rel_expr *)
  13.582  fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...}
  13.583                          : kodkod_constrs) T R i =
  13.584    kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R))
  13.585 -                   (kk_rel_eq (bit_set_from_atom kk T (Kodkod.Var (1, ~1)))
  13.586 -                              (Kodkod.Bits i))
  13.587 +                   (kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1)))
  13.588 +                              (KK.Bits i))
  13.589  
  13.590 -(* kodkod_constrs -> nut -> Kodkod.formula *)
  13.591 +(* kodkod_constrs -> nut -> KK.formula *)
  13.592  fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =
  13.593      kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep)
  13.594 -                      (Kodkod.Rel x)
  13.595 +                      (KK.Rel x)
  13.596    | declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs)
  13.597                                      (FreeRel (x, _, R, _)) =
  13.598 -    if is_one_rep R then kk_one (Kodkod.Rel x)
  13.599 -    else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (Kodkod.Rel x)
  13.600 -    else Kodkod.True
  13.601 +    if is_one_rep R then kk_one (KK.Rel x)
  13.602 +    else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (KK.Rel x)
  13.603 +    else KK.True
  13.604    | declarative_axiom_for_plain_rel _ u =
  13.605      raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])
  13.606  
  13.607 -(* nut NameTable.table -> styp -> Kodkod.rel_expr * rep * int *)
  13.608 +(* nut NameTable.table -> styp -> KK.rel_expr * rep * int *)
  13.609  fun const_triple rel_table (x as (s, T)) =
  13.610    case the_name rel_table (ConstName (s, T, Any)) of
  13.611 -    FreeRel ((n, j), _, R, _) => (Kodkod.Rel (n, j), R, n)
  13.612 +    FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n)
  13.613    | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])
  13.614  
  13.615 -(* nut NameTable.table -> styp -> Kodkod.rel_expr *)
  13.616 +(* nut NameTable.table -> styp -> KK.rel_expr *)
  13.617  fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
  13.618  
  13.619  (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
  13.620 @@ -747,7 +743,7 @@
  13.621    in
  13.622      map_filter (fn (j, T) =>
  13.623                     if forall (not_equal T o #typ) dtypes then NONE
  13.624 -                   else SOME (kk_project r (map Kodkod.Num [0, j]), T))
  13.625 +                   else SOME (kk_project r (map KK.Num [0, j]), T))
  13.626                 (index_seq 1 (arity - 1) ~~ tl type_schema)
  13.627    end
  13.628  (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
  13.629 @@ -763,28 +759,28 @@
  13.630      SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
  13.631                       o #const) constrs)
  13.632  
  13.633 -val empty_rel = Kodkod.Product (Kodkod.None, Kodkod.None)
  13.634 +val empty_rel = KK.Product (KK.None, KK.None)
  13.635  
  13.636 -(* nfa_table -> typ -> typ -> Kodkod.rel_expr list *)
  13.637 +(* nfa_table -> typ -> typ -> KK.rel_expr list *)
  13.638  fun direct_path_rel_exprs nfa start final =
  13.639    case AList.lookup (op =) nfa final of
  13.640      SOME trans => map fst (filter (curry (op =) start o snd) trans)
  13.641    | NONE => []
  13.642 -(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> Kodkod.rel_expr *)
  13.643 +(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> KK.rel_expr *)
  13.644  and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final =
  13.645      fold kk_union (direct_path_rel_exprs nfa start final)
  13.646 -         (if start = final then Kodkod.Iden else empty_rel)
  13.647 +         (if start = final then KK.Iden else empty_rel)
  13.648    | any_path_rel_expr (kk as {kk_union, ...}) nfa (q :: qs) start final =
  13.649      kk_union (any_path_rel_expr kk nfa qs start final)
  13.650               (knot_path_rel_expr kk nfa qs start q final)
  13.651  (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> typ
  13.652 -   -> Kodkod.rel_expr *)
  13.653 +   -> KK.rel_expr *)
  13.654  and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa qs start
  13.655                         knot final =
  13.656    kk_join (kk_join (any_path_rel_expr kk nfa qs knot final)
  13.657                     (kk_reflexive_closure (loop_path_rel_expr kk nfa qs knot)))
  13.658            (any_path_rel_expr kk nfa qs start knot)
  13.659 -(* kodkod_constrs -> nfa_table -> typ list -> typ -> Kodkod.rel_expr *)
  13.660 +(* kodkod_constrs -> nfa_table -> typ list -> typ -> KK.rel_expr *)
  13.661  and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start =
  13.662      fold kk_union (direct_path_rel_exprs nfa start start) empty_rel
  13.663    | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (q :: qs) start =
  13.664 @@ -812,12 +808,12 @@
  13.665    nfa |> graph_for_nfa |> NfaGraph.strong_conn
  13.666        |> map (fn keys => filter (member (op =) keys o fst) nfa)
  13.667  
  13.668 -(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> Kodkod.formula *)
  13.669 +(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> KK.formula *)
  13.670  fun acyclicity_axiom_for_datatype dtypes kk nfa start =
  13.671    #kk_no kk (#kk_intersect kk
  13.672 -                 (loop_path_rel_expr kk nfa (map fst nfa) start) Kodkod.Iden)
  13.673 +                 (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden)
  13.674  (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
  13.675 -   -> Kodkod.formula list *)
  13.676 +   -> KK.formula list *)
  13.677  fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes =
  13.678    map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes
  13.679    |> strongly_connected_sub_nfas
  13.680 @@ -825,7 +821,7 @@
  13.681                           nfa)
  13.682  
  13.683  (* extended_context -> int -> kodkod_constrs -> nut NameTable.table
  13.684 -   -> Kodkod.rel_expr -> constr_spec -> int -> Kodkod.formula *)
  13.685 +   -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
  13.686  fun sel_axiom_for_sel ext_ctxt j0
  13.687          (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no,
  13.688                  kk_join, ...}) rel_table dom_r
  13.689 @@ -840,15 +836,14 @@
  13.690      if exclusive then
  13.691        kk_n_ary_function kk (Func (Atom z, R2)) r
  13.692      else
  13.693 -      let val r' = kk_join (Kodkod.Var (1, 0)) r in
  13.694 -        kk_all [Kodkod.DeclOne ((1, 0), Kodkod.AtomSeq z)]
  13.695 -               (kk_formula_if (kk_subset (Kodkod.Var (1, 0)) dom_r)
  13.696 -                              (kk_n_ary_function kk R2 r')
  13.697 -                              (kk_no r'))
  13.698 +      let val r' = kk_join (KK.Var (1, 0)) r in
  13.699 +        kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]
  13.700 +               (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r)
  13.701 +                              (kk_n_ary_function kk R2 r') (kk_no r'))
  13.702        end
  13.703    end
  13.704  (* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
  13.705 -   -> constr_spec -> Kodkod.formula list *)
  13.706 +   -> constr_spec -> KK.formula list *)
  13.707  fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table
  13.708          (constr as {const, delta, epsilon, explicit_max, ...}) =
  13.709    let
  13.710 @@ -862,9 +857,9 @@
  13.711          val ran_r = discr_rel_expr rel_table const
  13.712          val max_axiom =
  13.713            if honors_explicit_max then
  13.714 -            Kodkod.True
  13.715 +            KK.True
  13.716            else if is_twos_complement_representable bits (epsilon - delta) then
  13.717 -            Kodkod.LE (Kodkod.Cardinality ran_r, Kodkod.Num explicit_max)
  13.718 +            KK.LE (KK.Cardinality ran_r, KK.Num explicit_max)
  13.719            else
  13.720              raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
  13.721                               "\"bits\" value " ^ string_of_int bits ^
  13.722 @@ -876,21 +871,20 @@
  13.723        end
  13.724    end
  13.725  (* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
  13.726 -   -> dtype_spec -> Kodkod.formula list *)
  13.727 +   -> dtype_spec -> KK.formula list *)
  13.728  fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table
  13.729                              ({constrs, ...} : dtype_spec) =
  13.730    maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs
  13.731  
  13.732  (* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
  13.733 -   -> Kodkod.formula list *)
  13.734 +   -> KK.formula list *)
  13.735  fun uniqueness_axiom_for_constr ext_ctxt
  13.736          ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
  13.737           : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
  13.738    let
  13.739 -    (* Kodkod.rel_expr -> Kodkod.formula *)
  13.740 +    (* KK.rel_expr -> KK.formula *)
  13.741      fun conjunct_for_sel r =
  13.742 -      kk_rel_eq (kk_join (Kodkod.Var (1, 0)) r)
  13.743 -                (kk_join (Kodkod.Var (1, 1)) r)
  13.744 +      kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
  13.745      val num_sels = num_sels_for_constr_type (snd const)
  13.746      val triples = map (const_triple rel_table
  13.747                         o boxed_nth_sel_for_constr ext_ctxt const)
  13.748 @@ -904,13 +898,13 @@
  13.749      if num_sels = 0 then
  13.750        kk_lone set_r
  13.751      else
  13.752 -      kk_all (map (Kodkod.DeclOne o rpair set_r o pair 1) [0, 1])
  13.753 +      kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])
  13.754               (kk_implies
  13.755                    (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
  13.756 -                  (kk_rel_eq (Kodkod.Var (1, 0)) (Kodkod.Var (1, 1))))
  13.757 +                  (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
  13.758    end
  13.759  (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
  13.760 -   -> Kodkod.formula list *)
  13.761 +   -> KK.formula list *)
  13.762  fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table
  13.763                                     ({constrs, ...} : dtype_spec) =
  13.764    map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs
  13.765 @@ -918,7 +912,7 @@
  13.766  (* constr_spec -> int *)
  13.767  fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
  13.768  (* int -> kodkod_constrs -> nut NameTable.table -> dtype_spec
  13.769 -   -> Kodkod.formula list *)
  13.770 +   -> KK.formula list *)
  13.771  fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
  13.772                                    rel_table
  13.773                                    ({card, constrs, ...} : dtype_spec) =
  13.774 @@ -926,12 +920,12 @@
  13.775      [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
  13.776    else
  13.777      let val rs = map (discr_rel_expr rel_table o #const) constrs in
  13.778 -      [kk_rel_eq (fold1 kk_union rs) (Kodkod.AtomSeq (card, j0)),
  13.779 +      [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)),
  13.780         kk_disjoint_sets kk rs]
  13.781      end
  13.782  
  13.783  (* extended_context -> int -> int Typtab.table -> kodkod_constrs
  13.784 -   -> nut NameTable.table -> dtype_spec -> Kodkod.formula list *)
  13.785 +   -> nut NameTable.table -> dtype_spec -> KK.formula list *)
  13.786  fun other_axioms_for_datatype _ _ _ _ _ {shallow = true, ...} = []
  13.787    | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
  13.788                                (dtype as {typ, ...}) =
  13.789 @@ -942,12 +936,12 @@
  13.790      end
  13.791  
  13.792  (* extended_context -> int -> int Typtab.table -> kodkod_constrs
  13.793 -   -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list *)
  13.794 +   -> nut NameTable.table -> dtype_spec list -> KK.formula list *)
  13.795  fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes =
  13.796    acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @
  13.797    maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes
  13.798  
  13.799 -(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula *)
  13.800 +(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
  13.801  fun kodkod_formula_from_nut bits ofs liberal
  13.802          (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
  13.803                  kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one,
  13.804 @@ -959,20 +953,20 @@
  13.805      val main_j0 = offset_of_type ofs bool_T
  13.806      val bool_j0 = main_j0
  13.807      val bool_atom_R = Atom (2, main_j0)
  13.808 -    val false_atom = Kodkod.Atom bool_j0
  13.809 -    val true_atom = Kodkod.Atom (bool_j0 + 1)
  13.810 +    val false_atom = KK.Atom bool_j0
  13.811 +    val true_atom = KK.Atom (bool_j0 + 1)
  13.812  
  13.813 -    (* polarity -> int -> Kodkod.rel_expr -> Kodkod.formula *)
  13.814 +    (* polarity -> int -> KK.rel_expr -> KK.formula *)
  13.815      fun formula_from_opt_atom polar j0 r =
  13.816        case polar of
  13.817 -        Neg => kk_not (kk_rel_eq r (Kodkod.Atom j0))
  13.818 -      | _ => kk_rel_eq r (Kodkod.Atom (j0 + 1))
  13.819 -    (* int -> Kodkod.rel_expr -> Kodkod.formula *)
  13.820 +        Neg => kk_not (kk_rel_eq r (KK.Atom j0))
  13.821 +      | _ => kk_rel_eq r (KK.Atom (j0 + 1))
  13.822 +    (* int -> KK.rel_expr -> KK.formula *)
  13.823      val formula_from_atom = formula_from_opt_atom Pos
  13.824  
  13.825 -    (* Kodkod.formula -> Kodkod.formula -> Kodkod.formula *)
  13.826 +    (* KK.formula -> KK.formula -> KK.formula *)
  13.827      fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2)
  13.828 -    (* Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.829 +    (* KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)
  13.830      val kk_or3 =
  13.831        double_rel_rel_let kk
  13.832            (fn r1 => fn r2 =>
  13.833 @@ -985,27 +979,27 @@
  13.834                          (kk_intersect r1 r2))
  13.835      fun kk_notimplies3 r1 r2 = kk_and3 r1 (kk_not3 r2)
  13.836  
  13.837 -    (* int -> Kodkod.rel_expr -> Kodkod.formula list *)
  13.838 +    (* int -> KK.rel_expr -> KK.formula list *)
  13.839      val unpack_formulas =
  13.840        map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1
  13.841 -    (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) -> int
  13.842 -       -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  13.843 +    (* (KK.formula -> KK.formula -> KK.formula) -> int -> KK.rel_expr
  13.844 +       -> KK.rel_expr -> KK.rel_expr *)
  13.845      fun kk_vect_set_op connective k r1 r2 =
  13.846        fold1 kk_product (map2 (atom_from_formula kk bool_j0 oo connective)
  13.847                               (unpack_formulas k r1) (unpack_formulas k r2))
  13.848 -    (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) -> int
  13.849 -       -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula *)
  13.850 +    (* (KK.formula -> KK.formula -> KK.formula) -> int -> KK.rel_expr
  13.851 +       -> KK.rel_expr -> KK.formula *)
  13.852      fun kk_vect_set_bool_op connective k r1 r2 =
  13.853        fold1 kk_and (map2 connective (unpack_formulas k r1)
  13.854                           (unpack_formulas k r2))
  13.855  
  13.856 -    (* nut -> Kodkod.formula *)
  13.857 +    (* nut -> KK.formula *)
  13.858      fun to_f u =
  13.859        case rep_of u of
  13.860          Formula polar =>
  13.861          (case u of
  13.862 -           Cst (False, _, _) => Kodkod.False
  13.863 -         | Cst (True, _, _) => Kodkod.True
  13.864 +           Cst (False, _, _) => KK.False
  13.865 +         | Cst (True, _, _) => KK.True
  13.866           | Op1 (Not, _, _, u1) =>
  13.867             kk_not (to_f_with_polarity (flip_polarity polar) u1)
  13.868           | Op1 (Finite, _, _, u1) =>
  13.869 @@ -1014,9 +1008,9 @@
  13.870                 Neut => if opt1 then
  13.871                           raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
  13.872                         else
  13.873 -                         Kodkod.True
  13.874 +                         KK.True
  13.875               | Pos => formula_for_bool (not opt1)
  13.876 -             | Neg => Kodkod.True
  13.877 +             | Neg => KK.True
  13.878             end
  13.879           | Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1
  13.880           | Op2 (All, _, _, u1, u2) =>
  13.881 @@ -1052,7 +1046,7 @@
  13.882               else
  13.883                 let
  13.884                   (* FIXME: merge with similar code below *)
  13.885 -                 (* bool -> nut -> Kodkod.rel_expr *)
  13.886 +                 (* bool -> nut -> KK.rel_expr *)
  13.887                   fun set_to_r widen u =
  13.888                     if widen then
  13.889                       kk_difference (full_rel_for_rep dom_R)
  13.890 @@ -1065,7 +1059,7 @@
  13.891             end
  13.892           | Op2 (DefEq, _, _, u1, u2) =>
  13.893             (case min_rep (rep_of u1) (rep_of u2) of
  13.894 -              Unit => Kodkod.True
  13.895 +              Unit => KK.True
  13.896              | Formula polar =>
  13.897                kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
  13.898              | min_R =>
  13.899 @@ -1085,7 +1079,7 @@
  13.900                end)
  13.901           | Op2 (Eq, T, R, u1, u2) =>
  13.902             (case min_rep (rep_of u1) (rep_of u2) of
  13.903 -              Unit => Kodkod.True
  13.904 +              Unit => KK.True
  13.905              | Formula polar =>
  13.906                kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
  13.907              | min_R =>
  13.908 @@ -1114,7 +1108,7 @@
  13.909                       else
  13.910                         if is_lone_rep min_R then
  13.911                           if arity_of_rep min_R = 1 then
  13.912 -                           kk_subset (kk_product r1 r2) Kodkod.Iden
  13.913 +                           kk_subset (kk_product r1 r2) KK.Iden
  13.914                           else if not both_opt then
  13.915                             (r1, r2) |> is_opt_rep (rep_of u2) ? swap
  13.916                                      |-> kk_subset
  13.917 @@ -1139,8 +1133,8 @@
  13.918                        val rs2 = unpack_products r2
  13.919                      in
  13.920                        if length rs1 = length rs2
  13.921 -                         andalso map Kodkod.arity_of_rel_expr rs1
  13.922 -                                 = map Kodkod.arity_of_rel_expr rs2 then
  13.923 +                         andalso map KK.arity_of_rel_expr rs1
  13.924 +                                 = map KK.arity_of_rel_expr rs2 then
  13.925                          fold1 kk_and (map2 kk_subset rs1 rs2)
  13.926                        else
  13.927                          kk_subset r1 r2
  13.928 @@ -1165,26 +1159,25 @@
  13.929           | Op3 (If, _, _, u1, u2, u3) =>
  13.930             kk_formula_if (to_f u1) (to_f_with_polarity polar u2)
  13.931                           (to_f_with_polarity polar u3)
  13.932 -         | FormulaReg (j, _, _) => Kodkod.FormulaReg j
  13.933 +         | FormulaReg (j, _, _) => KK.FormulaReg j
  13.934           | _ => raise NUT ("Nitpick_Kodkod.to_f", [u]))
  13.935        | Atom (2, j0) => formula_from_atom j0 (to_r u)
  13.936        | _ => raise NUT ("Nitpick_Kodkod.to_f", [u])
  13.937 -    (* polarity -> nut -> Kodkod.formula *)
  13.938 +    (* polarity -> nut -> KK.formula *)
  13.939      and to_f_with_polarity polar u =
  13.940        case rep_of u of
  13.941          Formula _ => to_f u
  13.942        | Atom (2, j0) => formula_from_atom j0 (to_r u)
  13.943        | Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u)
  13.944        | _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u])
  13.945 -    (* nut -> Kodkod.rel_expr *)
  13.946 +    (* nut -> KK.rel_expr *)
  13.947      and to_r u =
  13.948        case u of
  13.949          Cst (False, _, Atom _) => false_atom
  13.950        | Cst (True, _, Atom _) => true_atom
  13.951        | Cst (Iden, T, Func (Struct [R1, R2], Formula Neut)) =>
  13.952          if R1 = R2 andalso arity_of_rep R1 = 1 then
  13.953 -          kk_intersect Kodkod.Iden (kk_product (full_rel_for_rep R1)
  13.954 -                                               Kodkod.Univ)
  13.955 +          kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ)
  13.956          else
  13.957            let
  13.958              val schema1 = atom_schema_of_rep R1
  13.959 @@ -1200,106 +1193,100 @@
  13.960                  (kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1)
  13.961                             (rel_expr_from_rel_expr kk min_R R2 r2))
  13.962            end
  13.963 -      | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => Kodkod.Atom j0
  13.964 +      | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
  13.965        | Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) =>
  13.966          to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
  13.967        | Cst (Num j, T, R) =>
  13.968          if is_word_type T then
  13.969 -          atom_from_int_expr kk T R (Kodkod.Num j)
  13.970 +          atom_from_int_expr kk T R (KK.Num j)
  13.971          else if T = int_T then
  13.972            case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
  13.973 -            ~1 => if is_opt_rep R then Kodkod.None
  13.974 +            ~1 => if is_opt_rep R then KK.None
  13.975                    else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
  13.976 -          | j' => Kodkod.Atom j'
  13.977 +          | j' => KK.Atom j'
  13.978          else
  13.979 -          if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T)
  13.980 -          else if is_opt_rep R then Kodkod.None
  13.981 +          if j < card_of_rep R then KK.Atom (j + offset_of_type ofs T)
  13.982 +          else if is_opt_rep R then KK.None
  13.983            else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
  13.984        | Cst (Unknown, _, R) => empty_rel_for_rep R
  13.985        | Cst (Unrep, _, R) => empty_rel_for_rep R
  13.986 -      | Cst (Suc, T, Func (Atom x, _)) =>
  13.987 -        if domain_type T <> nat_T then
  13.988 -          Kodkod.Rel suc_rel
  13.989 -        else
  13.990 -          kk_intersect (Kodkod.Rel suc_rel)
  13.991 -                       (kk_product Kodkod.Univ (Kodkod.AtomSeq x))
  13.992 -      | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => Kodkod.Rel nat_add_rel
  13.993 -      | Cst (Add, Type ("fun", [@{typ int}, _]), _) => Kodkod.Rel int_add_rel
  13.994 +      | Cst (Suc, T as @{typ "unsigned_bit word => unsigned_bit word"}, R) =>
  13.995 +        to_bit_word_unary_op T R (curry KK.Add (KK.Num 1))
  13.996 +      | Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) =>
  13.997 +        kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x))
  13.998 +      | Cst (Suc, _, Func (Atom x, _)) => KK.Rel suc_rel
  13.999 +      | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_add_rel
 13.1000 +      | Cst (Add, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_add_rel
 13.1001        | Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
 13.1002 -        to_bit_word_binary_op T R NONE (SOME (curry Kodkod.Add))
 13.1003 +        to_bit_word_binary_op T R NONE (SOME (curry KK.Add))
 13.1004        | Cst (Add, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
 13.1005          to_bit_word_binary_op T R
 13.1006              (SOME (fn i1 => fn i2 => fn i3 =>
 13.1007 -                 kk_implies (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i1, i2)))
 13.1008 -                            (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i2, i3)))))
 13.1009 -            (SOME (curry Kodkod.Add))
 13.1010 +                 kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2)))
 13.1011 +                            (KK.LE (KK.Num 0, KK.BitXor (i2, i3)))))
 13.1012 +            (SOME (curry KK.Add))
 13.1013        | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) =>
 13.1014 -        Kodkod.Rel nat_subtract_rel
 13.1015 +        KK.Rel nat_subtract_rel
 13.1016        | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) =>
 13.1017 -        Kodkod.Rel int_subtract_rel
 13.1018 +        KK.Rel int_subtract_rel
 13.1019        | Cst (Subtract, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
 13.1020          to_bit_word_binary_op T R NONE
 13.1021              (SOME (fn i1 => fn i2 =>
 13.1022 -                      Kodkod.IntIf (Kodkod.LE (i1, i2), Kodkod.Num 0,
 13.1023 -                                    Kodkod.Sub (i1, i2))))
 13.1024 +                      KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2))))
 13.1025        | Cst (Subtract, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
 13.1026          to_bit_word_binary_op T R
 13.1027              (SOME (fn i1 => fn i2 => fn i3 =>
 13.1028 -                 kk_implies (Kodkod.LT (Kodkod.BitXor (i1, i2), Kodkod.Num 0))
 13.1029 -                            (Kodkod.LT (Kodkod.BitXor (i2, i3), Kodkod.Num 0))))
 13.1030 -            (SOME (curry Kodkod.Sub))
 13.1031 +                 kk_implies (KK.LT (KK.BitXor (i1, i2), KK.Num 0))
 13.1032 +                            (KK.LT (KK.BitXor (i2, i3), KK.Num 0))))
 13.1033 +            (SOME (curry KK.Sub))
 13.1034        | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) =>
 13.1035 -        Kodkod.Rel nat_multiply_rel
 13.1036 +        KK.Rel nat_multiply_rel
 13.1037        | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) =>
 13.1038 -        Kodkod.Rel int_multiply_rel
 13.1039 +        KK.Rel int_multiply_rel
 13.1040        | Cst (Multiply,
 13.1041               T as Type ("fun", [Type (@{type_name word}, [bit_T]), _]), R) =>
 13.1042          to_bit_word_binary_op T R
 13.1043              (SOME (fn i1 => fn i2 => fn i3 =>
 13.1044 -                kk_or (Kodkod.IntEq (i2, Kodkod.Num 0))
 13.1045 -                      (Kodkod.IntEq (Kodkod.Div (i3, i2), i1)
 13.1046 +                kk_or (KK.IntEq (i2, KK.Num 0))
 13.1047 +                      (KK.IntEq (KK.Div (i3, i2), i1)
 13.1048                         |> bit_T = @{typ signed_bit}
 13.1049 -                          ? kk_and (Kodkod.LE (Kodkod.Num 0,
 13.1050 -                                          foldl1 Kodkod.BitAnd [i1, i2, i3])))))
 13.1051 -            (SOME (curry Kodkod.Mult))
 13.1052 -      | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) =>
 13.1053 -        Kodkod.Rel nat_divide_rel
 13.1054 -      | Cst (Divide, Type ("fun", [@{typ int}, _]), _) =>
 13.1055 -        Kodkod.Rel int_divide_rel
 13.1056 +                          ? kk_and (KK.LE (KK.Num 0,
 13.1057 +                                           foldl1 KK.BitAnd [i1, i2, i3])))))
 13.1058 +            (SOME (curry KK.Mult))
 13.1059 +      | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_divide_rel
 13.1060 +      | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_divide_rel
 13.1061        | Cst (Divide, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
 13.1062          to_bit_word_binary_op T R NONE
 13.1063              (SOME (fn i1 => fn i2 =>
 13.1064 -                      Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0),
 13.1065 -                                    Kodkod.Num 0, Kodkod.Div (i1, i2))))
 13.1066 +                      KK.IntIf (KK.IntEq (i2, KK.Num 0),
 13.1067 +                                KK.Num 0, KK.Div (i1, i2))))
 13.1068        | Cst (Divide, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
 13.1069          to_bit_word_binary_op T R
 13.1070              (SOME (fn i1 => fn i2 => fn i3 =>
 13.1071 -                Kodkod.LE (Kodkod.Num 0, foldl1 Kodkod.BitAnd [i1, i2, i3])))
 13.1072 +                      KK.LE (KK.Num 0, foldl1 KK.BitAnd [i1, i2, i3])))
 13.1073              (SOME (fn i1 => fn i2 =>
 13.1074 -                 Kodkod.IntIf (kk_and (Kodkod.LT (i1, Kodkod.Num 0))
 13.1075 -                                      (Kodkod.LT (Kodkod.Num 0, i2)),
 13.1076 -                     Kodkod.Sub (Kodkod.Div (Kodkod.Add (i1, Kodkod.Num 1), i2),
 13.1077 -                                 Kodkod.Num 1),
 13.1078 -                     Kodkod.IntIf (kk_and (Kodkod.LT (Kodkod.Num 0, i1))
 13.1079 -                                          (Kodkod.LT (i2, Kodkod.Num 0)),
 13.1080 -                         Kodkod.Sub (Kodkod.Div (Kodkod.Sub (i1, Kodkod.Num 1),
 13.1081 -                                                 i2), Kodkod.Num 1),
 13.1082 -                         Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0),
 13.1083 -                                       Kodkod.Num 0, Kodkod.Div (i1, i2))))))
 13.1084 -      | Cst (Gcd, _, _) => Kodkod.Rel gcd_rel
 13.1085 -      | Cst (Lcm, _, _) => Kodkod.Rel lcm_rel
 13.1086 -      | Cst (Fracs, _, Func (Atom (1, _), _)) => Kodkod.None
 13.1087 +                 KK.IntIf (kk_and (KK.LT (i1, KK.Num 0))
 13.1088 +                                  (KK.LT (KK.Num 0, i2)),
 13.1089 +                     KK.Sub (KK.Div (KK.Add (i1, KK.Num 1), i2), KK.Num 1),
 13.1090 +                     KK.IntIf (kk_and (KK.LT (KK.Num 0, i1))
 13.1091 +                                      (KK.LT (i2, KK.Num 0)),
 13.1092 +                         KK.Sub (KK.Div (KK.Sub (i1, KK.Num 1), i2), KK.Num 1),
 13.1093 +                         KK.IntIf (KK.IntEq (i2, KK.Num 0),
 13.1094 +                                   KK.Num 0, KK.Div (i1, i2))))))
 13.1095 +      | Cst (Gcd, _, _) => KK.Rel gcd_rel
 13.1096 +      | Cst (Lcm, _, _) => KK.Rel lcm_rel
 13.1097 +      | Cst (Fracs, _, Func (Atom (1, _), _)) => KK.None
 13.1098        | Cst (Fracs, _, Func (Struct _, _)) =>
 13.1099 -        kk_project_seq (Kodkod.Rel norm_frac_rel) 2 2
 13.1100 -      | Cst (NormFrac, _, _) => Kodkod.Rel norm_frac_rel
 13.1101 +        kk_project_seq (KK.Rel norm_frac_rel) 2 2
 13.1102 +      | Cst (NormFrac, _, _) => KK.Rel norm_frac_rel
 13.1103        | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) =>
 13.1104 -        Kodkod.Iden
 13.1105 +        KK.Iden
 13.1106        | Cst (NatToInt, Type ("fun", [@{typ nat}, _]),
 13.1107               Func (Atom (nat_k, nat_j0), Opt (Atom (int_k, int_j0)))) =>
 13.1108          if nat_j0 = int_j0 then
 13.1109 -          kk_intersect Kodkod.Iden
 13.1110 -              (kk_product (Kodkod.AtomSeq (max_int_for_card int_k + 1, nat_j0))
 13.1111 -                          Kodkod.Univ)
 13.1112 +          kk_intersect KK.Iden
 13.1113 +              (kk_product (KK.AtomSeq (max_int_for_card int_k + 1, nat_j0))
 13.1114 +                          KK.Univ)
 13.1115          else
 13.1116            raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
 13.1117        | Cst (NatToInt, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
 13.1118 @@ -1312,21 +1299,19 @@
 13.1119            val overlap = Int.min (nat_k, abs_card)
 13.1120          in
 13.1121            if nat_j0 = int_j0 then
 13.1122 -            kk_union (kk_product (Kodkod.AtomSeq (int_k - abs_card,
 13.1123 -                                                  int_j0 + abs_card))
 13.1124 -                                 (Kodkod.Atom nat_j0))
 13.1125 -                     (kk_intersect Kodkod.Iden
 13.1126 -                          (kk_product (Kodkod.AtomSeq (overlap, int_j0))
 13.1127 -                                      Kodkod.Univ))
 13.1128 +            kk_union (kk_product (KK.AtomSeq (int_k - abs_card,
 13.1129 +                                              int_j0 + abs_card))
 13.1130 +                                 (KK.Atom nat_j0))
 13.1131 +                     (kk_intersect KK.Iden
 13.1132 +                          (kk_product (KK.AtomSeq (overlap, int_j0)) KK.Univ))
 13.1133            else
 13.1134              raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
 13.1135          end
 13.1136        | Cst (IntToNat, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
 13.1137          to_bit_word_unary_op T R
 13.1138 -            (fn i => Kodkod.IntIf (Kodkod.LE (i, Kodkod.Num 0),
 13.1139 -                                   Kodkod.Num 0, i))
 13.1140 +            (fn i => KK.IntIf (KK.LE (i, KK.Num 0), KK.Num 0, i))
 13.1141        | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
 13.1142 -      | Op1 (Finite, _, Opt (Atom _), _) => Kodkod.None
 13.1143 +      | Op1 (Finite, _, Opt (Atom _), _) => KK.None
 13.1144        | Op1 (Converse, T, R, u1) =>
 13.1145          let
 13.1146            val (b_T, a_T) = HOLogic.dest_prodT (domain_type T)
 13.1147 @@ -1346,9 +1331,9 @@
 13.1148            val body_arity = arity_of_rep body_R
 13.1149          in
 13.1150            kk_project (to_rep (Func (Struct [a_R, b_R], body_R)) u1)
 13.1151 -                     (map Kodkod.Num (index_seq a_arity b_arity @
 13.1152 -                                      index_seq 0 a_arity @
 13.1153 -                                      index_seq ab_arity body_arity))
 13.1154 +                     (map KK.Num (index_seq a_arity b_arity @
 13.1155 +                                  index_seq 0 a_arity @
 13.1156 +                                  index_seq ab_arity body_arity))
 13.1157            |> rel_expr_from_rel_expr kk R (Func (Struct [b_R, a_R], body_R))
 13.1158          end
 13.1159        | Op1 (Closure, _, R, u1) =>
 13.1160 @@ -1410,13 +1395,13 @@
 13.1161        | Op2 (Exist, T, Opt _, u1, u2) =>
 13.1162          let val rs1 = untuple to_decl u1 in
 13.1163            if not (is_opt_rep (rep_of u2)) then
 13.1164 -            kk_rel_if (kk_exist rs1 (to_f u2)) true_atom Kodkod.None
 13.1165 +            kk_rel_if (kk_exist rs1 (to_f u2)) true_atom KK.None
 13.1166            else
 13.1167              let val r2 = to_r u2 in
 13.1168                kk_union (kk_rel_if (kk_exist rs1 (kk_rel_eq r2 true_atom))
 13.1169 -                                  true_atom Kodkod.None)
 13.1170 +                                  true_atom KK.None)
 13.1171                         (kk_rel_if (kk_all rs1 (kk_rel_eq r2 false_atom))
 13.1172 -                                  false_atom Kodkod.None)
 13.1173 +                                  false_atom KK.None)
 13.1174              end
 13.1175          end
 13.1176        | Op2 (Or, _, _, u1, u2) =>
 13.1177 @@ -1437,10 +1422,10 @@
 13.1178                          kk_rel_if
 13.1179                              (fold kk_and (map_filter (fn (u, r) =>
 13.1180                                   if is_opt_rep (rep_of u) then SOME (kk_some r)
 13.1181 -                                 else NONE) [(u1, r1), (u2, r2)]) Kodkod.True)
 13.1182 -                            (atom_from_formula kk bool_j0 (Kodkod.LT (pairself
 13.1183 +                                 else NONE) [(u1, r1), (u2, r2)]) KK.True)
 13.1184 +                            (atom_from_formula kk bool_j0 (KK.LT (pairself
 13.1185                                  (int_expr_from_atom kk (type_of u1)) (r1, r2))))
 13.1186 -                            Kodkod.None)
 13.1187 +                            KK.None)
 13.1188                      (to_r u1) (to_r u2))
 13.1189        | Op2 (The, T, R, u1, u2) =>
 13.1190          if is_opt_rep R then
 13.1191 @@ -1485,8 +1470,8 @@
 13.1192            if f1 = f2 then
 13.1193              atom_from_formula kk j0 f1
 13.1194            else
 13.1195 -            kk_union (kk_rel_if f1 true_atom Kodkod.None)
 13.1196 -                     (kk_rel_if f2 Kodkod.None false_atom)
 13.1197 +            kk_union (kk_rel_if f1 true_atom KK.None)
 13.1198 +                     (kk_rel_if f2 KK.None false_atom)
 13.1199          end
 13.1200        | Op2 (Union, _, R, u1, u2) =>
 13.1201          to_set_op kk_or kk_or3 kk_union kk_union kk_intersect false R u1 u2
 13.1202 @@ -1518,7 +1503,7 @@
 13.1203             | Opt (Atom (2, _)) =>
 13.1204               let
 13.1205                 (* FIXME: merge with similar code above *)
 13.1206 -               (* rep -> rep -> nut -> Kodkod.rel_expr *)
 13.1207 +               (* rep -> rep -> nut -> KK.rel_expr *)
 13.1208                 fun must R1 R2 u =
 13.1209                   kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) true_atom
 13.1210                 fun may R1 R2 u =
 13.1211 @@ -1553,9 +1538,9 @@
 13.1212                          (to_rep (Func (b_R, Formula Neut)) u2)
 13.1213             | Opt (Atom (2, _)) =>
 13.1214               let
 13.1215 -               (* Kodkod.rel_expr -> rep -> nut -> Kodkod.rel_expr *)
 13.1216 +               (* KK.rel_expr -> rep -> nut -> KK.rel_expr *)
 13.1217                 fun do_nut r R u = kk_join (to_rep (Func (R, body_R)) u) r
 13.1218 -               (* Kodkod.rel_expr -> Kodkod.rel_expr *)
 13.1219 +               (* KK.rel_expr -> KK.rel_expr *)
 13.1220                 fun do_term r =
 13.1221                   kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r
 13.1222               in kk_union (do_term true_atom) (do_term false_atom) end
 13.1223 @@ -1567,7 +1552,7 @@
 13.1224             (Func (R11, R12), Func (R21, Formula Neut)) =>
 13.1225             if R21 = R11 andalso is_lone_rep R12 then
 13.1226               let
 13.1227 -               (* Kodkod.rel_expr -> Kodkod.rel_expr *)
 13.1228 +               (* KK.rel_expr -> KK.rel_expr *)
 13.1229                 fun big_join r = kk_n_fold_join kk false R21 R12 r (to_r u1)
 13.1230                 val core_r = big_join (to_r u2)
 13.1231                 val core_R = Func (R12, Formula Neut)
 13.1232 @@ -1593,9 +1578,9 @@
 13.1233        | Op2 (Apply, @{typ nat}, _,
 13.1234               Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) =>
 13.1235          if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
 13.1236 -          Kodkod.Atom (offset_of_type ofs nat_T)
 13.1237 +          KK.Atom (offset_of_type ofs nat_T)
 13.1238          else
 13.1239 -          fold kk_join (map to_integer [u1, u2]) (Kodkod.Rel nat_subtract_rel)
 13.1240 +          fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel)
 13.1241        | Op2 (Apply, _, R, u1, u2) =>
 13.1242          if is_Cst Unrep u2 andalso is_set_type (type_of u1)
 13.1243             andalso is_FreeName u1 then
 13.1244 @@ -1603,7 +1588,7 @@
 13.1245          else
 13.1246            to_apply R u1 u2
 13.1247        | Op2 (Lambda, T, R as Opt (Atom (1, j0)), u1, u2) =>
 13.1248 -        to_guard [u1, u2] R (Kodkod.Atom j0)
 13.1249 +        to_guard [u1, u2] R (KK.Atom j0)
 13.1250        | Op2 (Lambda, T, Func (_, Formula Neut), u1, u2) =>
 13.1251          kk_comprehension (untuple to_decl u1) (to_f u2)
 13.1252        | Op2 (Lambda, T, Func (_, R2), u1, u2) =>
 13.1253 @@ -1639,10 +1624,9 @@
 13.1254           | Vect (k, R) => to_product (replicate k R) us
 13.1255           | Atom (1, j0) =>
 13.1256             (case filter (not_equal Unit o rep_of) us of
 13.1257 -              [] => Kodkod.Atom j0
 13.1258 -            | us' =>
 13.1259 -              kk_rel_if (kk_some (fold1 kk_product (map to_r us')))
 13.1260 -                        (Kodkod.Atom j0) Kodkod.None)
 13.1261 +              [] => KK.Atom j0
 13.1262 +            | us' => kk_rel_if (kk_some (fold1 kk_product (map to_r us')))
 13.1263 +                               (KK.Atom j0) KK.None)
 13.1264           | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))
 13.1265        | Construct ([u'], _, _, []) => to_r u'
 13.1266        | Construct (_ :: sel_us, T, R, arg_us) =>
 13.1267 @@ -1660,47 +1644,46 @@
 13.1268                         else
 13.1269                           kk_comprehension
 13.1270                               (decls_for_atom_schema ~1 (atom_schema_of_rep R1))
 13.1271 -                             (kk_rel_eq (kk_join (Kodkod.Var (1, ~1)) sel_r)
 13.1272 -                                        arg_r)
 13.1273 +                             (kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r)
 13.1274                       end) sel_us arg_us
 13.1275          in fold1 kk_intersect set_rs end
 13.1276 -      | BoundRel (x, _, _, _) => Kodkod.Var x
 13.1277 -      | FreeRel (x, _, _, _) => Kodkod.Rel x
 13.1278 -      | RelReg (j, _, R) => Kodkod.RelReg (arity_of_rep R, j)
 13.1279 +      | BoundRel (x, _, _, _) => KK.Var x
 13.1280 +      | FreeRel (x, _, _, _) => KK.Rel x
 13.1281 +      | RelReg (j, _, R) => KK.RelReg (arity_of_rep R, j)
 13.1282        | u => raise NUT ("Nitpick_Kodkod.to_r", [u])
 13.1283 -    (* nut -> Kodkod.decl *)
 13.1284 +    (* nut -> KK.decl *)
 13.1285      and to_decl (BoundRel (x, _, R, _)) =
 13.1286 -        Kodkod.DeclOne (x, Kodkod.AtomSeq (the_single (atom_schema_of_rep R)))
 13.1287 +        KK.DeclOne (x, KK.AtomSeq (the_single (atom_schema_of_rep R)))
 13.1288        | to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u])
 13.1289 -    (* nut -> Kodkod.expr_assign *)
 13.1290 +    (* nut -> KK.expr_assign *)
 13.1291      and to_expr_assign (FormulaReg (j, _, R)) u =
 13.1292 -        Kodkod.AssignFormulaReg (j, to_f u)
 13.1293 +        KK.AssignFormulaReg (j, to_f u)
 13.1294        | to_expr_assign (RelReg (j, _, R)) u =
 13.1295 -        Kodkod.AssignRelReg ((arity_of_rep R, j), to_r u)
 13.1296 +        KK.AssignRelReg ((arity_of_rep R, j), to_r u)
 13.1297        | to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1])
 13.1298 -    (* int * int -> nut -> Kodkod.rel_expr *)
 13.1299 +    (* int * int -> nut -> KK.rel_expr *)
 13.1300      and to_atom (x as (k, j0)) u =
 13.1301        case rep_of u of
 13.1302          Formula _ => atom_from_formula kk j0 (to_f u)
 13.1303 -      | Unit => if k = 1 then Kodkod.Atom j0
 13.1304 +      | Unit => if k = 1 then KK.Atom j0
 13.1305                  else raise NUT ("Nitpick_Kodkod.to_atom", [u])
 13.1306        | R => atom_from_rel_expr kk x R (to_r u)
 13.1307 -    (* rep list -> nut -> Kodkod.rel_expr *)
 13.1308 +    (* rep list -> nut -> KK.rel_expr *)
 13.1309      and to_struct Rs u =
 13.1310        case rep_of u of
 13.1311          Unit => full_rel_for_rep (Struct Rs)
 13.1312        | R' => struct_from_rel_expr kk Rs R' (to_r u)
 13.1313 -    (* int -> rep -> nut -> Kodkod.rel_expr *)
 13.1314 +    (* int -> rep -> nut -> KK.rel_expr *)
 13.1315      and to_vect k R u =
 13.1316        case rep_of u of
 13.1317          Unit => full_rel_for_rep (Vect (k, R))
 13.1318        | R' => vect_from_rel_expr kk k R R' (to_r u)
 13.1319 -    (* rep -> rep -> nut -> Kodkod.rel_expr *)
 13.1320 +    (* rep -> rep -> nut -> KK.rel_expr *)
 13.1321      and to_func R1 R2 u =
 13.1322        case rep_of u of
 13.1323          Unit => full_rel_for_rep (Func (R1, R2))
 13.1324        | R' => rel_expr_to_func kk R1 R2 R' (to_r u)
 13.1325 -    (* rep -> nut -> Kodkod.rel_expr *)
 13.1326 +    (* rep -> nut -> KK.rel_expr *)
 13.1327      and to_opt R u =
 13.1328        let val old_R = rep_of u in
 13.1329          if is_opt_rep old_R then
 13.1330 @@ -1708,16 +1691,16 @@
 13.1331          else
 13.1332            to_rep R u
 13.1333        end
 13.1334 -    (* rep -> nut -> Kodkod.rel_expr *)
 13.1335 +    (* rep -> nut -> KK.rel_expr *)
 13.1336      and to_rep (Atom x) u = to_atom x u
 13.1337        | to_rep (Struct Rs) u = to_struct Rs u
 13.1338        | to_rep (Vect (k, R)) u = to_vect k R u
 13.1339        | to_rep (Func (R1, R2)) u = to_func R1 R2 u
 13.1340        | to_rep (Opt R) u = to_opt R u
 13.1341        | to_rep R _ = raise REP ("Nitpick_Kodkod.to_rep", [R])
 13.1342 -    (* nut -> Kodkod.rel_expr *)
 13.1343 +    (* nut -> KK.rel_expr *)
 13.1344      and to_integer u = to_opt (one_rep ofs (type_of u) (rep_of u)) u
 13.1345 -    (* nut list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
 13.1346 +    (* nut list -> rep -> KK.rel_expr -> KK.rel_expr *)
 13.1347      and to_guard guard_us R r =
 13.1348        let
 13.1349          val unpacked_rs = unpack_joins r
 13.1350 @@ -1737,16 +1720,16 @@
 13.1351          else
 13.1352            kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r
 13.1353        end
 13.1354 -    (* rep -> rep -> Kodkod.rel_expr -> int -> Kodkod.rel_expr *)
 13.1355 +    (* rep -> rep -> KK.rel_expr -> int -> KK.rel_expr *)
 13.1356      and to_project new_R old_R r j0 =
 13.1357        rel_expr_from_rel_expr kk new_R old_R
 13.1358                               (kk_project_seq r j0 (arity_of_rep old_R))
 13.1359 -    (* rep list -> nut list -> Kodkod.rel_expr *)
 13.1360 +    (* rep list -> nut list -> KK.rel_expr *)
 13.1361      and to_product Rs us =
 13.1362        case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of
 13.1363          [] => raise REP ("Nitpick_Kodkod.to_product", Rs)
 13.1364        | rs => fold1 kk_product rs
 13.1365 -    (* int -> typ -> rep -> nut -> Kodkod.rel_expr *)
 13.1366 +    (* int -> typ -> rep -> nut -> KK.rel_expr *)
 13.1367      and to_nth_pair_sel n res_T res_R u =
 13.1368        case u of
 13.1369          Tuple (_, _, us) => to_rep res_R (nth us n)
 13.1370 @@ -1774,9 +1757,9 @@
 13.1371                                 (to_rep res_R (Cst (Unity, res_T, Unit)))
 13.1372                 | arity => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0
 13.1373               end
 13.1374 -    (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula)
 13.1375 -       -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula) -> nut -> nut
 13.1376 -       -> Kodkod.formula *)
 13.1377 +    (* (KK.formula -> KK.formula -> KK.formula)
 13.1378 +       -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> nut -> nut
 13.1379 +       -> KK.formula *)
 13.1380      and to_set_bool_op connective set_oper u1 u2 =
 13.1381        let
 13.1382          val min_R = min_rep (rep_of u1) (rep_of u2)
 13.1383 @@ -1792,12 +1775,12 @@
 13.1384                                          (kk_join r2 true_atom)
 13.1385          | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
 13.1386        end
 13.1387 -    (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula)
 13.1388 -       -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
 13.1389 -       -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula)
 13.1390 -       -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula)
 13.1391 -       -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula) -> bool -> rep
 13.1392 -       -> nut -> nut -> Kodkod.rel_expr *)
 13.1393 +    (* (KK.formula -> KK.formula -> KK.formula)
 13.1394 +       -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr)
 13.1395 +       -> (KK.rel_expr -> KK.rel_expr -> KK.formula)
 13.1396 +       -> (KK.rel_expr -> KK.rel_expr -> KK.formula)
 13.1397 +       -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> bool -> rep -> nut
 13.1398 +       -> nut -> KK.rel_expr *)
 13.1399      and to_set_op connective connective3 set_oper true_set_oper false_set_oper
 13.1400                    neg_second R u1 u2 =
 13.1401        let
 13.1402 @@ -1829,51 +1812,47 @@
 13.1403                     r1 r2
 13.1404               | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R]))
 13.1405        end
 13.1406 -    (* typ -> rep -> (Kodkod.int_expr -> Kodkod.int_expr) -> Kodkod.rel_expr *)
 13.1407 +    (* typ -> rep -> (KK.int_expr -> KK.int_expr) -> KK.rel_expr *)
 13.1408      and to_bit_word_unary_op T R oper =
 13.1409        let
 13.1410          val Ts = strip_type T ||> single |> op @
 13.1411 -        (* int -> Kodkod.int_expr *)
 13.1412 -        fun int_arg j = int_expr_from_atom kk (nth Ts j) (Kodkod.Var (1, j))
 13.1413 +        (* int -> KK.int_expr *)
 13.1414 +        fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j))
 13.1415        in
 13.1416          kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
 13.1417 -            (Kodkod.FormulaLet
 13.1418 -                 (map (fn j => Kodkod.AssignIntReg (j, int_arg j)) (0 upto 1),
 13.1419 -                  Kodkod.IntEq (Kodkod.IntReg 1, oper (Kodkod.IntReg 0))))
 13.1420 +            (KK.FormulaLet
 13.1421 +                 (map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 1),
 13.1422 +                  KK.IntEq (KK.IntReg 1, oper (KK.IntReg 0))))
 13.1423        end
 13.1424 -    (* typ -> rep
 13.1425 -       -> (Kodkod.int_expr -> Kodkod.int_expr -> Kodkod.int_expr -> bool) option
 13.1426 -       -> (Kodkod.int_expr -> Kodkod.int_expr -> Kodkod.int_expr) option
 13.1427 -       -> Kodkod.rel_expr *)
 13.1428 +    (* typ -> rep -> (KK.int_expr -> KK.int_expr -> KK.int_expr -> bool) option
 13.1429 +       -> (KK.int_expr -> KK.int_expr -> KK.int_expr) option -> KK.rel_expr *)
 13.1430      and to_bit_word_binary_op T R opt_guard opt_oper =
 13.1431        let
 13.1432          val Ts = strip_type T ||> single |> op @
 13.1433 -        (* int -> Kodkod.int_expr *)
 13.1434 -        fun int_arg j = int_expr_from_atom kk (nth Ts j) (Kodkod.Var (1, j))
 13.1435 +        (* int -> KK.int_expr *)
 13.1436 +        fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j))
 13.1437        in
 13.1438          kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
 13.1439 -            (Kodkod.FormulaLet
 13.1440 -                 (map (fn j => Kodkod.AssignIntReg (j, int_arg j)) (0 upto 2),
 13.1441 +            (KK.FormulaLet
 13.1442 +                 (map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 2),
 13.1443                    fold1 kk_and
 13.1444                          ((case opt_guard of
 13.1445                              NONE => []
 13.1446                            | SOME guard =>
 13.1447 -                            [guard (Kodkod.IntReg 0) (Kodkod.IntReg 1)
 13.1448 -                                   (Kodkod.IntReg 2)]) @
 13.1449 +                            [guard (KK.IntReg 0) (KK.IntReg 1) (KK.IntReg 2)]) @
 13.1450                           (case opt_oper of
 13.1451                              NONE => []
 13.1452                            | SOME oper =>
 13.1453 -                            [Kodkod.IntEq (Kodkod.IntReg 2,
 13.1454 -                                 oper (Kodkod.IntReg 0) (Kodkod.IntReg 1))]))))
 13.1455 +                            [KK.IntEq (KK.IntReg 2,
 13.1456 +                                       oper (KK.IntReg 0) (KK.IntReg 1))]))))
 13.1457        end
 13.1458 -    (* rep -> rep -> Kodkod.rel_expr -> nut -> Kodkod.rel_expr *)
 13.1459 +    (* rep -> rep -> KK.rel_expr -> nut -> KK.rel_expr *)
 13.1460      and to_apply res_R func_u arg_u =
 13.1461        case unopt_rep (rep_of func_u) of
 13.1462          Unit =>
 13.1463          let val j0 = offset_of_type ofs (type_of func_u) in
 13.1464            to_guard [arg_u] res_R
 13.1465 -                   (rel_expr_from_rel_expr kk res_R (Atom (1, j0))
 13.1466 -                                           (Kodkod.Atom j0))
 13.1467 +                   (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (KK.Atom j0))
 13.1468          end
 13.1469        | Atom (1, j0) =>
 13.1470          to_guard [arg_u] res_R
 13.1471 @@ -1902,7 +1881,7 @@
 13.1472              (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u))
 13.1473          |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R
 13.1474        | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u])
 13.1475 -    (* int -> rep -> rep -> Kodkod.rel_expr -> nut *)
 13.1476 +    (* int -> rep -> rep -> KK.rel_expr -> nut *)
 13.1477      and to_apply_vect k R' res_R func_r arg_u =
 13.1478        let
 13.1479          val arg_R = one_rep ofs (type_of arg_u) (unopt_rep (rep_of arg_u))
 13.1480 @@ -1912,11 +1891,10 @@
 13.1481          kk_case_switch kk arg_R res_R (to_opt arg_R arg_u)
 13.1482                         (all_singletons_for_rep arg_R) vect_rs
 13.1483        end
 13.1484 -    (* bool -> nut -> Kodkod.formula *)
 13.1485 +    (* bool -> nut -> KK.formula *)
 13.1486      and to_could_be_unrep neg u =
 13.1487 -      if neg andalso is_opt_rep (rep_of u) then kk_no (to_r u)
 13.1488 -      else Kodkod.False
 13.1489 -    (* nut -> Kodkod.rel_expr -> Kodkod.rel_expr *)
 13.1490 +      if neg andalso is_opt_rep (rep_of u) then kk_no (to_r u) else KK.False
 13.1491 +    (* nut -> KK.rel_expr -> KK.rel_expr *)
 13.1492      and to_compare_with_unrep u r =
 13.1493        if is_opt_rep (rep_of u) then
 13.1494          kk_rel_if (kk_some (to_r u)) r (empty_rel_for_rep (rep_of u))
    14.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Dec 17 15:22:27 2009 +0100
    14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Dec 18 12:00:29 2009 +0100
    14.3 @@ -40,6 +40,8 @@
    14.4  open Nitpick_Rep
    14.5  open Nitpick_Nut
    14.6  
    14.7 +structure KK = Kodkod
    14.8 +
    14.9  type params = {
   14.10    show_skolems: bool,
   14.11    show_datatypes: bool,
   14.12 @@ -71,19 +73,22 @@
   14.13    else
   14.14      Const (atom_name "" T j, T)
   14.15  
   14.16 +(* term -> real *)
   14.17 +fun extract_real_number (Const (@{const_name HOL.divide}, _) $ t1 $ t2) =
   14.18 +    real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
   14.19 +  | extract_real_number t = real (snd (HOLogic.dest_number t))
   14.20  (* term * term -> order *)
   14.21  fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2)
   14.22 -  | nice_term_ord (t1, t2) =
   14.23 -    int_ord (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
   14.24 +  | nice_term_ord tp = Real.compare (pairself extract_real_number tp)
   14.25      handle TERM ("dest_number", _) =>
   14.26 -           case (t1, t2) of
   14.27 +           case tp of
   14.28               (t11 $ t12, t21 $ t22) =>
   14.29               (case nice_term_ord (t11, t21) of
   14.30                  EQUAL => nice_term_ord (t12, t22)
   14.31                | ord => ord)
   14.32 -           | _ => TermOrd.term_ord (t1, t2)
   14.33 +           | _ => TermOrd.fast_term_ord tp
   14.34  
   14.35 -(* nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list *)
   14.36 +(* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *)
   14.37  fun tuple_list_for_name rel_table bounds name =
   14.38    the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
   14.39  
   14.40 @@ -240,8 +245,8 @@
   14.41    | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
   14.42  
   14.43  (* string * string * string * string -> scope -> nut list -> nut list
   14.44 -   -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> typ -> typ
   14.45 -   -> rep -> int list list -> term *)
   14.46 +   -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
   14.47 +   -> int list list -> term *)
   14.48  fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
   14.49          ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
   14.50           : scope) sel_names rel_table bounds =
   14.51 @@ -324,7 +329,7 @@
   14.52               | _ => t
   14.53      (* bool -> typ -> typ -> typ -> term list -> term list -> term *)
   14.54      fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
   14.55 -      ts1 ~~ ts2 |> T1 = @{typ bisim_iterator} ? rev
   14.56 +      ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
   14.57                   |> make_plain_fun (maybe_opt andalso not for_auto) T1 T2
   14.58                   |> unbit_and_unbox_term
   14.59                   |> typecast_fun (unbit_and_unbox_type T')
   14.60 @@ -506,7 +511,7 @@
   14.61      oooo term_for_rep []
   14.62    end
   14.63  
   14.64 -(* scope -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> nut
   14.65 +(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
   14.66     -> term *)
   14.67  fun term_for_name scope sel_names rel_table bounds name =
   14.68    let val T = type_of name in
   14.69 @@ -563,7 +568,7 @@
   14.70      end
   14.71  
   14.72  (* params -> scope -> (term option * int list) list -> styp list -> nut list
   14.73 -  -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
   14.74 +  -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
   14.75    -> Pretty.T * bool *)
   14.76  fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
   14.77          ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
   14.78 @@ -704,7 +709,7 @@
   14.79    end
   14.80  
   14.81  (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
   14.82 -   -> Kodkod.raw_bound list -> term -> bool option *)
   14.83 +   -> KK.raw_bound list -> term -> bool option *)
   14.84  fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns, ...})
   14.85                      auto_timeout free_names sel_names rel_table bounds prop =
   14.86    let
    15.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Dec 17 15:22:27 2009 +0100
    15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri Dec 18 12:00:29 2009 +0100
    15.3 @@ -130,6 +130,8 @@
    15.4  open Nitpick_Peephole
    15.5  open Nitpick_Rep
    15.6  
    15.7 +structure KK = Kodkod
    15.8 +
    15.9  datatype cst =
   15.10    Unity |
   15.11    False |
   15.12 @@ -196,8 +198,8 @@
   15.13    BoundName of int * typ * rep * string |
   15.14    FreeName of string * typ * rep |
   15.15    ConstName of string * typ * rep |
   15.16 -  BoundRel of Kodkod.n_ary_index * typ * rep * string |
   15.17 -  FreeRel of Kodkod.n_ary_index * typ * rep * string |
   15.18 +  BoundRel of KK.n_ary_index * typ * rep * string |
   15.19 +  FreeRel of KK.n_ary_index * typ * rep * string |
   15.20    RelReg of int * typ * rep |
   15.21    FormulaReg of int * typ * rep
   15.22  
   15.23 @@ -439,7 +441,7 @@
   15.24    case NameTable.lookup table name of
   15.25      SOME u => u
   15.26    | NONE => raise NUT ("Nitpick_Nut.the_name", [name])
   15.27 -(* nut NameTable.table -> nut -> Kodkod.n_ary_index *)
   15.28 +(* nut NameTable.table -> nut -> KK.n_ary_index *)
   15.29  fun the_rel table name =
   15.30    case the_name table name of
   15.31      FreeRel (x, _, _, _) => x
   15.32 @@ -915,10 +917,8 @@
   15.33          | Cst (True, T, _) => Cst (True, T, Formula Neut)
   15.34          | Cst (Num j, T, _) =>
   15.35            if is_word_type T then
   15.36 -            if is_twos_complement_representable bits j then
   15.37 -              Cst (Num j, T, best_non_opt_set_rep_for_type scope T)
   15.38 -            else
   15.39 -              Cst (Unrep, T, best_opt_set_rep_for_type scope T)
   15.40 +            Cst (if is_twos_complement_representable bits j then Num j
   15.41 +                 else Unrep, T, best_opt_set_rep_for_type scope T)
   15.42            else
   15.43              (case spec_of_type scope T of
   15.44                 (1, j0) => if j = 0 then Cst (Unity, T, Unit)
   15.45 @@ -1239,8 +1239,8 @@
   15.46        |> optimize_unit
   15.47    in aux table def Pos end
   15.48  
   15.49 -(* int -> Kodkod.n_ary_index list -> Kodkod.n_ary_index list
   15.50 -   -> int * Kodkod.n_ary_index list *)
   15.51 +(* int -> KK.n_ary_index list -> KK.n_ary_index list
   15.52 +   -> int * KK.n_ary_index list *)
   15.53  fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys)
   15.54    | fresh_n_ary_index n ((m, j) :: xs) ys =
   15.55      if m = n then (j, ys @ ((m, j + 1) :: xs))
    16.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Thu Dec 17 15:22:27 2009 +0100
    16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Fri Dec 18 12:00:29 2009 +0100
    16.3 @@ -266,7 +266,7 @@
    16.4  
    16.5      (* bool -> int *)
    16.6      val from_bool = atom_for_bool main_j0
    16.7 -    (* int -> Kodkod.rel_expr *)
    16.8 +    (* int -> rel_expr *)
    16.9      fun from_nat n = Atom (n + main_j0)
   16.10      val from_int = Atom o atom_for_int (int_card, main_j0)
   16.11      (* int -> int *)
   16.12 @@ -347,7 +347,7 @@
   16.13      (* rel_expr -> formula *)
   16.14      fun s_no None = True
   16.15        | s_no (Product (r1, r2)) = s_or (s_no r1) (s_no r2)
   16.16 -      | s_no (Intersect (Closure (Kodkod.Rel x), Kodkod.Iden)) = Acyclic x
   16.17 +      | s_no (Intersect (Closure (Rel x), Iden)) = Acyclic x
   16.18        | s_no r = if is_one_rel_expr r then False else No r
   16.19      fun s_lone None = True
   16.20        | s_lone r = if is_one_rel_expr r then True else Lone r
   16.21 @@ -409,8 +409,8 @@
   16.22                      s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2)
   16.23                    else
   16.24                      RelEq (r1, r2)
   16.25 -               | (_, Kodkod.None) => s_no r1
   16.26 -               | (Kodkod.None, _) => s_no r2
   16.27 +               | (_, None) => s_no r1
   16.28 +               | (None, _) => s_no r2
   16.29                 | _ => RelEq (r1, r2)
   16.30      fun s_subset (Atom j1) (Atom j2) = formula_for_bool (j1 = j2)
   16.31        | s_subset (Atom j) (AtomSeq (k, j0)) =
    17.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Dec 17 15:22:27 2009 +0100
    17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Dec 18 12:00:29 2009 +0100
    17.3 @@ -249,6 +249,10 @@
    17.4      [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
    17.5    else if T = @{typ signed_bit} then
    17.6      [(Card T, map (Integer.add 1 o Integer.min max_bits o Integer.max 1) bitss)]
    17.7 +  else if T = @{typ "unsigned_bit word"} then
    17.8 +    [(Card T, lookup_type_ints_assign thy cards_assigns nat_T)]
    17.9 +  else if T = @{typ "signed_bit word"} then
   17.10 +    [(Card T, lookup_type_ints_assign thy cards_assigns int_T)]
   17.11    else if T = @{typ bisim_iterator} then
   17.12      [(Card T, map (Integer.add 1 o Integer.max 0) bisim_depths)]
   17.13    else if is_fp_iterator_type T then
   17.14 @@ -316,32 +320,20 @@
   17.15      [] => false
   17.16    | xs =>
   17.17      let
   17.18 -      val exact_cards =
   17.19 -        map (Integer.prod
   17.20 -             o map (bounded_exact_card_of_type ext_ctxt k 0 card_assigns)
   17.21 +      val dom_cards =
   17.22 +        map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns)
   17.23               o binder_types o snd) xs
   17.24        val maxes = map (constr_max max_assigns) xs
   17.25        (* int -> int -> int *)
   17.26 -      fun effective_max 0 ~1 = k
   17.27 -        | effective_max 0 max = max
   17.28 -        | effective_max card ~1 = card
   17.29 +      fun effective_max card ~1 = card
   17.30          | effective_max card max = Int.min (card, max)
   17.31 -      val max = map2 effective_max exact_cards maxes |> Integer.sum
   17.32 -      (* unit -> int *)
   17.33 -      fun doms_card () =
   17.34 -        xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns)
   17.35 -                   o binder_types o snd)
   17.36 -           |> Integer.sum
   17.37 -    in
   17.38 -      max < k
   17.39 -      orelse (forall (not_equal 0) exact_cards andalso doms_card () < k)
   17.40 -    end
   17.41 -    handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false
   17.42 -
   17.43 -(* extended_context -> scope_desc -> bool *)
   17.44 -fun is_surely_inconsistent_scope_description ext_ctxt
   17.45 -                                             (desc as (card_assigns, _)) =
   17.46 -  exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_assigns
   17.47 +      val max = map2 effective_max dom_cards maxes |> Integer.sum
   17.48 +    in max < k end
   17.49 +(* extended_context -> (typ * int) list -> (typ * int) list
   17.50 +   -> (styp * int) list -> bool *)
   17.51 +fun is_surely_inconsistent_scope_description ext_ctxt seen rest max_assigns =
   17.52 +  exists (is_surely_inconsistent_card_assign ext_ctxt
   17.53 +                                             (seen @ rest, max_assigns)) seen
   17.54  
   17.55  (* extended_context -> scope_desc -> (typ * int) list option *)
   17.56  fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) =
   17.57 @@ -349,15 +341,15 @@
   17.58      (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
   17.59      fun aux seen [] = SOME seen
   17.60        | aux seen ((T, 0) :: _) = NONE
   17.61 -      | aux seen ((T, k) :: assigns) =
   17.62 -        (if is_surely_inconsistent_scope_description ext_ctxt
   17.63 -                ((T, k) :: seen, max_assigns) then
   17.64 +      | aux seen ((T, k) :: rest) =
   17.65 +        (if is_surely_inconsistent_scope_description ext_ctxt ((T, k) :: seen)
   17.66 +                                                     rest max_assigns then
   17.67             raise SAME ()
   17.68           else
   17.69 -           case aux ((T, k) :: seen) assigns of
   17.70 +           case aux ((T, k) :: seen) rest of
   17.71               SOME assigns => SOME assigns
   17.72             | NONE => raise SAME ())
   17.73 -        handle SAME () => aux seen ((T, k - 1) :: assigns)
   17.74 +        handle SAME () => aux seen ((T, k - 1) :: rest)
   17.75    in aux [] (rev card_assigns) end
   17.76  
   17.77  (* theory -> (typ * int) list -> typ * int -> typ * int *)