# HG changeset patch # User huffman # Date 1316627995 25200 # Node ID 29b5ff81f709a79f4049f539f4ff00cb02da9036 # Parent ad016fc215f2487fc56f839d2c7cc766ee701d75# Parent 60d2c03d5c70cfac2d6fa691c46d0f47cf88031a merged diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/IsaMakefile Wed Sep 21 10:59:55 2011 -0700 @@ -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 diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Core_Nits.thy --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Datatype_Nits.thy --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Hotel_Nits.thy --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Induct_Nits.thy --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Integer_Nits.thy --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Mini_Nits.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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 "\x. x = Not"} *} +ML {* none 1 @{prop "\ False"} *} +ML {* genuine 1 @{prop "\ True"} *} +ML {* none 1 @{prop "\ \ b \ b"} *} +ML {* none 1 @{prop True} *} +ML {* genuine 1 @{prop False} *} +ML {* genuine 1 @{prop "True \ False"} *} +ML {* none 1 @{prop "True \ \ False"} *} +ML {* none 5 @{prop "\x. x = x"} *} +ML {* none 5 @{prop "\x. x = x"} *} +ML {* none 1 @{prop "\x. x = y"} *} +ML {* genuine 2 @{prop "\x. x = y"} *} +ML {* none 1 @{prop "\x. x = y"} *} +ML {* none 2 @{prop "\x. x = y"} *} +ML {* none 2 @{prop "\x\'a \ 'a. x = x"} *} +ML {* none 2 @{prop "\x\'a \ 'a. x = y"} *} +ML {* genuine 2 @{prop "\x\'a \ 'a. x = y"} *} +ML {* none 2 @{prop "\x\'a \ '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 \ P x = P y"} *} +ML {* none 5 @{prop "(x\'a \ 'a) = y \ P x = P y"} *} +ML {* none 2 @{prop "(x\'a \ 'a) = y \ P x y = P y x"} *} +ML {* none 5 @{prop "\x\'a \ 'a. x = y \ P x = P y"} *} +ML {* none 2 @{prop "(x\'a \ 'a) = y \ P x = P y"} *} +ML {* none 2 @{prop "\x\'a \ 'a. x = y \ P x = P y"} *} +ML {* genuine 1 @{prop "(op =) X = Ex"} *} +ML {* none 2 @{prop "\x::'a \ 'a. x = x"} *} +ML {* none 1 @{prop "x = y"} *} +ML {* genuine 1 @{prop "x \ y"} *} +ML {* genuine 2 @{prop "x = y"} *} +ML {* genuine 1 @{prop "X \ Y"} *} +ML {* none 1 @{prop "P \ Q \ Q \ P"} *} +ML {* none 1 @{prop "P \ Q \ P"} *} +ML {* none 1 @{prop "P \ Q \ Q \ P"} *} +ML {* genuine 1 @{prop "P \ Q \ P"} *} +ML {* none 1 @{prop "(P \ Q) \ (\ P \ Q)"} *} +ML {* none 5 @{prop "{a} = {a, a}"} *} +ML {* genuine 2 @{prop "{a} = {a, b}"} *} +ML {* genuine 1 @{prop "{a} \ {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 \ c \ {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *} +ML {* none 5 @{prop "A \ B = (\x. A x \ B x)"} *} +ML {* none 5 @{prop "A \ B = (\x. A x \ B x)"} *} +ML {* none 5 @{prop "A - B = (\x. A x \ \ B x)"} *} +ML {* none 5 @{prop "\a b. (a, b) = (b, a)"} *} +ML {* genuine 2 @{prop "(a, b) = (b, a)"} *} +ML {* genuine 2 @{prop "(a, b) \ (b, a)"} *} +ML {* none 5 @{prop "\a b\'a \ 'a. (a, b) = (b, a)"} *} +ML {* genuine 2 @{prop "(a\'a \ 'a, b) = (b, a)"} *} +ML {* none 5 @{prop "\a b\'a \ 'a \ 'a. (a, b) = (b, a)"} *} +ML {* genuine 2 @{prop "(a\'a \ 'a \ 'a, b) \ (b, a)"} *} +ML {* none 5 @{prop "\a b\'a \ 'a. (a, b) = (b, a)"} *} +ML {* genuine 1 @{prop "(a\'a \ 'a, b) \ (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) \ 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) \ a"} *} +ML {* genuine 1 @{prop P} *} +ML {* genuine 1 @{prop "(\x. P) a"} *} +ML {* genuine 1 @{prop "(\x y z. P y x z) a b c"} *} +ML {* none 5 @{prop "\f. f = (\x. x) \ f y = y"} *} +ML {* genuine 1 @{prop "\f. f p \ p \ (\a b. f (a, b) = (a, b))"} *} +ML {* none 2 @{prop "\f. \a b. f (a, b) = (a, b)"} *} +ML {* none 3 @{prop "f = (\a b. (b, a)) \ f x y = (y, x)"} *} +ML {* genuine 2 @{prop "f = (\a b. (b, a)) \ f x y = (x, y)"} *} + +end diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Nitpick_Examples.thy --- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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 diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Pattern_Nits.thy --- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Record_Nits.thy --- a/src/HOL/Nitpick_Examples/Record_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Special_Nits.thy --- a/src/HOL/Nitpick_Examples/Special_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Tests_Nits.thy --- a/src/HOL/Nitpick_Examples/Tests_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -1,6 +1,6 @@ (* Title: HOL/Nitpick_Examples/Tests_Nits.thy Author: Jasmin Blanchette, TU Muenchen - Copyright 2009, 2010 + Copyright 2009-2011 Nitpick tests. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Sep 21 10:59:55 2011 -0700 @@ -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. *) diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Nitpick_Examples/minipick.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nitpick_Examples/minipick.ML Wed Sep 21 10:59:55 2011 -0700 @@ -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; diff -r ad016fc215f2 -r 29b5ff81f709 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 21 08:28:53 2011 -0700 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 21 10:59:55 2011 -0700 @@ -149,13 +149,13 @@ |> snd end -(* This is a terrible hack. Free variables are sometimes code as "M__" when they - are displayed as "M" and we want to avoid clashes with these. But sometimes - it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all - free variables. In the worse case scenario, where the fact won't be resolved - correctly, the user can fix it manually, e.g., by naming the fact in - question. Ideally we would need nothing of it, but backticks just don't work - with schematic variables. *) +(* This is a terrible hack. Free variables are sometimes coded as "M__" when + they are displayed as "M" and we want to avoid clashes with these. But + sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all + prefixes of all free variables. In the worse case scenario, where the fact + won't be resolved correctly, the user can fix it manually, e.g., by naming + the fact in question. Ideally we would need nothing of it, but backticks + simply don't work with schematic variables. *) fun all_prefixes_of s = map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1) fun close_form t =