--- a/src/HOL/IsaMakefile Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/IsaMakefile Wed Sep 21 15:55:16 2011 +0200
@@ -709,10 +709,11 @@
Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \
Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
- Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \
- Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
- Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
- Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
+ Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
+ Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
+ Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
+ Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
+ Nitpick_Examples/Typedef_Nits.thy Nitpick_Examples/minipick.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Core_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Examples featuring Nitpick's functional core.
*)
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Datatype_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Examples featuring Nitpick applied to datatypes.
*)
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Hotel_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2010
+ Copyright 2010-2011
Nitpick example based on Tobias Nipkow's hotel key card formalization.
*)
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Induct_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Examples featuring Nitpick applied to (co)inductive definitions.
*)
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Integer_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Examples featuring Nitpick applied to natural numbers and integers.
*)
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Manual_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Examples from the Nitpick manual.
*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -0,0 +1,109 @@
+(* Title: HOL/Nitpick_Examples/Mini_Nits.thy
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2009-2011
+
+Examples featuring Minipick, the minimalistic version of Nitpick.
+*)
+
+header {* Examples Featuring Minipick, the Minimalistic Version of Nitpick *}
+
+theory Mini_Nits
+imports Main
+uses "minipick.ML"
+begin
+
+ML {*
+exception FAIL
+
+val has_kodkodi = (getenv "KODKODI" <> "")
+
+fun minipick n t =
+ map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n)
+ |> Minipick.solve_any_kodkod_problem @{theory}
+fun minipick_expect expect n t =
+ if has_kodkodi then
+ if minipick n t = expect then () else raise FAIL
+ else
+ ()
+val none = minipick_expect "none"
+val genuine = minipick_expect "genuine"
+val unknown = minipick_expect "unknown"
+*}
+
+ML {* genuine 1 @{prop "x = Not"} *}
+ML {* none 1 @{prop "\<exists>x. x = Not"} *}
+ML {* none 1 @{prop "\<not> False"} *}
+ML {* genuine 1 @{prop "\<not> True"} *}
+ML {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
+ML {* none 1 @{prop True} *}
+ML {* genuine 1 @{prop False} *}
+ML {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
+ML {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
+ML {* none 5 @{prop "\<forall>x. x = x"} *}
+ML {* none 5 @{prop "\<exists>x. x = x"} *}
+ML {* none 1 @{prop "\<forall>x. x = y"} *}
+ML {* genuine 2 @{prop "\<forall>x. x = y"} *}
+ML {* none 1 @{prop "\<exists>x. x = y"} *}
+ML {* none 2 @{prop "\<exists>x. x = y"} *}
+ML {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
+ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
+ML {* genuine 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = y"} *}
+ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
+ML {* none 1 @{prop "All = Ex"} *}
+ML {* genuine 2 @{prop "All = Ex"} *}
+ML {* none 1 @{prop "All P = Ex P"} *}
+ML {* genuine 2 @{prop "All P = Ex P"} *}
+ML {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
+ML {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
+ML {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
+ML {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
+ML {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
+ML {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
+ML {* genuine 1 @{prop "(op =) X = Ex"} *}
+ML {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
+ML {* none 1 @{prop "x = y"} *}
+ML {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
+ML {* genuine 2 @{prop "x = y"} *}
+ML {* genuine 1 @{prop "X \<subseteq> Y"} *}
+ML {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
+ML {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
+ML {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
+ML {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
+ML {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
+ML {* none 5 @{prop "{a} = {a, a}"} *}
+ML {* genuine 2 @{prop "{a} = {a, b}"} *}
+ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
+ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
+ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
+ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
+ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
+ML {* none 5 @{prop "A \<union> B = (\<lambda>x. A x \<or> B x)"} *}
+ML {* none 5 @{prop "A \<inter> B = (\<lambda>x. A x \<and> B x)"} *}
+ML {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
+ML {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
+ML {* genuine 2 @{prop "(a, b) = (b, a)"} *}
+ML {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
+ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
+ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
+ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
+ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
+ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
+ML {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
+ML {* none 5 @{prop "fst (a, b) = a"} *}
+ML {* none 1 @{prop "fst (a, b) = b"} *}
+ML {* genuine 2 @{prop "fst (a, b) = b"} *}
+ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
+ML {* none 5 @{prop "snd (a, b) = b"} *}
+ML {* none 1 @{prop "snd (a, b) = a"} *}
+ML {* genuine 2 @{prop "snd (a, b) = a"} *}
+ML {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
+ML {* genuine 1 @{prop P} *}
+ML {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
+ML {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
+ML {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
+ML {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
+ML {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
+ML {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
+ML {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
+
+end
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Mono_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Examples featuring Nitpick's monotonicity check.
*)
--- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,13 +1,13 @@
(* Title: HOL/Nitpick_Examples/Nitpick_Examples.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Nitpick examples.
*)
theory Nitpick_Examples
imports Core_Nits Datatype_Nits Hotel_Nits Induct_Nits Integer_Nits Manual_Nits
- Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
- Typedef_Nits
+ Mini_Nits Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits
+ Tests_Nits Typedef_Nits
begin
end
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Pattern_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Examples featuring Nitpick's "destroy_constrs" optimization.
*)
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Record_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Examples featuring Nitpick applied to records.
*)
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Refute_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Refute examples adapted to Nitpick.
*)
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Special_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Examples featuring Nitpick's "specialize" optimization.
*)
--- a/src/HOL/Nitpick_Examples/Tests_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Tests_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Nitpick tests.
*)
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Sep 21 15:55:15 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Sep 21 15:55:16 2011 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Typedef_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
+ Copyright 2009-2011
Examples featuring Nitpick applied to typedefs.
*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/minipick.ML Wed Sep 21 15:55:16 2011 +0200
@@ -0,0 +1,327 @@
+(* Title: HOL/Nitpick_Examples/minipick.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2009-2010
+
+Finite model generation for HOL formulas using Kodkod, minimalistic version.
+*)
+
+signature MINIPICK =
+sig
+ datatype rep = S_Rep | R_Rep
+ type styp = Nitpick_Util.styp
+
+ val vars_for_bound_var :
+ (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
+ val rel_expr_for_bound_var :
+ (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
+ val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
+ val false_atom : Kodkod.rel_expr
+ val true_atom : Kodkod.rel_expr
+ val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
+ val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
+ val kodkod_problem_from_term :
+ Proof.context -> (typ -> int) -> term -> Kodkod.problem
+ val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
+end;
+
+structure Minipick : MINIPICK =
+struct
+
+open Kodkod
+open Nitpick_Util
+open Nitpick_HOL
+open Nitpick_Peephole
+open Nitpick_Kodkod
+
+datatype rep = S_Rep | R_Rep
+
+fun check_type ctxt (Type (@{type_name fun}, Ts)) =
+ List.app (check_type ctxt) Ts
+ | check_type ctxt (Type (@{type_name prod}, Ts)) =
+ List.app (check_type ctxt) Ts
+ | check_type _ @{typ bool} = ()
+ | check_type _ (TFree (_, @{sort "{}"})) = ()
+ | check_type _ (TFree (_, @{sort HOL.type})) = ()
+ | check_type ctxt T =
+ raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
+
+fun atom_schema_of S_Rep card (Type (@{type_name fun}, [T1, T2])) =
+ replicate_list (card T1) (atom_schema_of S_Rep card T2)
+ | atom_schema_of R_Rep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
+ atom_schema_of S_Rep card T1
+ | atom_schema_of R_Rep card (Type (@{type_name fun}, [T1, T2])) =
+ atom_schema_of S_Rep card T1 @ atom_schema_of R_Rep card T2
+ | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
+ maps (atom_schema_of S_Rep card) Ts
+ | atom_schema_of _ card T = [card T]
+val arity_of = length ooo atom_schema_of
+
+fun index_for_bound_var _ [_] 0 = 0
+ | index_for_bound_var card (_ :: Ts) 0 =
+ index_for_bound_var card Ts 0 + arity_of S_Rep card (hd Ts)
+ | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
+fun vars_for_bound_var card R Ts j =
+ map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
+ (arity_of R card (nth Ts j)))
+val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
+fun decls_for R card Ts T =
+ map2 (curry DeclOne o pair 1)
+ (index_seq (index_for_bound_var card (T :: Ts) 0)
+ (arity_of R card (nth (T :: Ts) 0)))
+ (map (AtomSeq o rpair 0) (atom_schema_of R card T))
+
+val atom_product = foldl1 Product o map Atom
+
+val false_atom = Atom 0
+val true_atom = Atom 1
+
+fun formula_from_atom r = RelEq (r, true_atom)
+fun atom_from_formula f = RelIf (f, true_atom, false_atom)
+
+fun kodkod_formula_from_term ctxt card frees =
+ let
+ fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
+ let
+ val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
+ |> all_combinations
+ in
+ map2 (fn i => fn js =>
+ RelIf (formula_from_atom (Project (r, [Num i])),
+ atom_product js, empty_n_ary_rel (length js)))
+ (index_seq 0 (length jss)) jss
+ |> foldl1 Union
+ end
+ | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
+ let
+ val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
+ |> all_combinations
+ val arity2 = arity_of S_Rep card T2
+ in
+ map2 (fn i => fn js =>
+ Product (atom_product js,
+ Project (r, num_seq (i * arity2) arity2)
+ |> R_rep_from_S_rep T2))
+ (index_seq 0 (length jss)) jss
+ |> foldl1 Union
+ end
+ | R_rep_from_S_rep _ r = r
+ fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
+ Comprehension (decls_for S_Rep card Ts T,
+ RelEq (R_rep_from_S_rep T
+ (rel_expr_for_bound_var card S_Rep (T :: Ts) 0), r))
+ | S_rep_from_R_rep _ _ r = r
+ fun to_F Ts t =
+ (case t of
+ @{const Not} $ t1 => Not (to_F Ts t1)
+ | @{const False} => False
+ | @{const True} => True
+ | Const (@{const_name All}, _) $ Abs (_, T, t') =>
+ All (decls_for S_Rep card Ts T, to_F (T :: Ts) t')
+ | (t0 as Const (@{const_name All}, _)) $ t1 =>
+ to_F Ts (t0 $ eta_expand Ts t1 1)
+ | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
+ Exist (decls_for S_Rep card Ts T, to_F (T :: Ts) t')
+ | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
+ to_F Ts (t0 $ eta_expand Ts t1 1)
+ | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
+ RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
+ | Const (@{const_name ord_class.less_eq},
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+ $ t1 $ t2 =>
+ Subset (to_R_rep Ts t1, to_R_rep Ts t2)
+ | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
+ | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
+ | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
+ | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
+ | Free _ => raise SAME ()
+ | Term.Var _ => raise SAME ()
+ | Bound _ => raise SAME ()
+ | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
+ | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
+ handle SAME () => formula_from_atom (to_R_rep Ts t)
+ and to_S_rep Ts t =
+ case t of
+ Const (@{const_name Pair}, _) $ t1 $ t2 =>
+ Product (to_S_rep Ts t1, to_S_rep Ts t2)
+ | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
+ | Const (@{const_name fst}, _) $ t1 =>
+ let val fst_arity = arity_of S_Rep card (fastype_of1 (Ts, t)) in
+ Project (to_S_rep Ts t1, num_seq 0 fst_arity)
+ end
+ | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name snd}, _) $ t1 =>
+ let
+ val pair_arity = arity_of S_Rep card (fastype_of1 (Ts, t1))
+ val snd_arity = arity_of S_Rep card (fastype_of1 (Ts, t))
+ val fst_arity = pair_arity - snd_arity
+ in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
+ | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
+ | Bound j => rel_expr_for_bound_var card S_Rep Ts j
+ | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
+ and to_R_rep Ts t =
+ (case t of
+ @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
+ | Const (@{const_name ord_class.less_eq},
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
+ to_R_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name ord_class.less_eq}, _) =>
+ to_R_rep Ts (eta_expand Ts t 2)
+ | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
+ | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
+ | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
+ | Const (@{const_name bot_class.bot},
+ T as Type (@{type_name fun}, [_, @{typ bool}])) =>
+ empty_n_ary_rel (arity_of R_Rep card T)
+ | Const (@{const_name insert}, _) $ t1 $ t2 =>
+ Union (to_S_rep Ts t1, to_R_rep Ts t2)
+ | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
+ | Const (@{const_name trancl}, _) $ t1 =>
+ if arity_of R_Rep card (fastype_of1 (Ts, t1)) = 2 then
+ Closure (to_R_rep Ts t1)
+ else
+ raise NOT_SUPPORTED "transitive closure for function or pair type"
+ | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name inf_class.inf},
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+ $ t1 $ t2 =>
+ Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
+ | Const (@{const_name inf_class.inf}, _) $ _ =>
+ to_R_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name inf_class.inf}, _) =>
+ to_R_rep Ts (eta_expand Ts t 2)
+ | Const (@{const_name sup_class.sup},
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+ $ t1 $ t2 =>
+ Union (to_R_rep Ts t1, to_R_rep Ts t2)
+ | Const (@{const_name sup_class.sup}, _) $ _ =>
+ to_R_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name sup_class.sup}, _) =>
+ to_R_rep Ts (eta_expand Ts t 2)
+ | Const (@{const_name minus_class.minus},
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+ $ t1 $ t2 =>
+ Difference (to_R_rep Ts t1, to_R_rep Ts t2)
+ | Const (@{const_name minus_class.minus},
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
+ to_R_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name minus_class.minus},
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
+ to_R_rep Ts (eta_expand Ts t 2)
+ | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
+ | Const (@{const_name Pair}, _) $ _ => raise SAME ()
+ | Const (@{const_name Pair}, _) => raise SAME ()
+ | Const (@{const_name fst}, _) $ _ => raise SAME ()
+ | Const (@{const_name fst}, _) => raise SAME ()
+ | Const (@{const_name snd}, _) $ _ => raise SAME ()
+ | Const (@{const_name snd}, _) => raise SAME ()
+ | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
+ | Free (x as (_, T)) =>
+ Rel (arity_of R_Rep card T, find_index (curry (op =) x) frees)
+ | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
+ | Bound _ => raise SAME ()
+ | Abs (_, T, t') =>
+ (case fastype_of1 (T :: Ts, t') of
+ @{typ bool} => Comprehension (decls_for S_Rep card Ts T,
+ to_F (T :: Ts) t')
+ | T' => Comprehension (decls_for S_Rep card Ts T @
+ decls_for R_Rep card (T :: Ts) T',
+ Subset (rel_expr_for_bound_var card R_Rep
+ (T' :: T :: Ts) 0,
+ to_R_rep (T :: Ts) t')))
+ | t1 $ t2 =>
+ (case fastype_of1 (Ts, t) of
+ @{typ bool} => atom_from_formula (to_F Ts t)
+ | T =>
+ let val T2 = fastype_of1 (Ts, t2) in
+ case arity_of S_Rep card T2 of
+ 1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
+ | arity2 =>
+ let val res_arity = arity_of R_Rep card T in
+ Project (Intersect
+ (Product (to_S_rep Ts t2,
+ atom_schema_of R_Rep card T
+ |> map (AtomSeq o rpair 0) |> foldl1 Product),
+ to_R_rep Ts t1),
+ num_seq arity2 res_arity)
+ end
+ end)
+ | _ => raise NOT_SUPPORTED ("term " ^
+ quote (Syntax.string_of_term ctxt t)))
+ handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
+ in to_F [] end
+
+fun bound_for_free card i (s, T) =
+ let val js = atom_schema_of R_Rep card T in
+ ([((length js, i), s)],
+ [TupleSet [], atom_schema_of R_Rep card T |> map (rpair 0)
+ |> tuple_set_from_atom_schema])
+ end
+
+fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
+ r =
+ if body_type T2 = bool_T then
+ True
+ else
+ All (decls_for S_Rep card Ts T1,
+ declarative_axiom_for_rel_expr card (T1 :: Ts) T2
+ (List.foldl Join r (vars_for_bound_var card S_Rep (T1 :: Ts) 0)))
+ | declarative_axiom_for_rel_expr _ _ _ r = One r
+fun declarative_axiom_for_free card i (_, T) =
+ declarative_axiom_for_rel_expr card [] T (Rel (arity_of R_Rep card T, i))
+
+fun kodkod_problem_from_term ctxt raw_card t =
+ let
+ val thy = ProofContext.theory_of ctxt
+ fun card (Type (@{type_name fun}, [T1, T2])) =
+ reasonable_power (card T2) (card T1)
+ | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
+ | card @{typ bool} = 2
+ | card T = Int.max (1, raw_card T)
+ val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
+ val _ = fold_types (K o check_type ctxt) neg_t ()
+ val frees = Term.add_frees neg_t []
+ val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
+ val declarative_axioms =
+ map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
+ val formula = kodkod_formula_from_term ctxt card frees neg_t
+ |> fold_rev (curry And) declarative_axioms
+ val univ_card = univ_card 0 0 0 bounds formula
+ in
+ {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
+ bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
+ end
+
+fun solve_any_kodkod_problem thy problems =
+ let
+ val {debug, overlord, ...} = Nitpick_Isar.default_params thy []
+ val max_threads = 1
+ val max_solutions = 1
+ in
+ case solve_any_problem debug overlord NONE max_threads max_solutions
+ problems of
+ JavaNotInstalled => "unknown"
+ | JavaTooOld => "unknown"
+ | KodkodiNotInstalled => "unknown"
+ | Normal ([], _, _) => "none"
+ | Normal _ => "genuine"
+ | TimedOut _ => "unknown"
+ | Error (s, _) => error ("Kodkod error: " ^ s)
+ end
+
+end;