# HG changeset patch # User blanchet # Date 1236356477 -3600 # Node ID 0e0cb7ac02813a949826acceeceaf4c66781f99b # Parent 66a57e4f043e64ce6311bcb3064a3cfab7aa1558 Fix remaining occurrences of "'a set" in Refute, by using "'a => bool" instead. I tested the affected symbols (card, finite, lfp, and gfp), and Refute now works better than before (i.e., more precision and more speed). diff -r 66a57e4f043e -r 0e0cb7ac0281 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Fri Mar 06 15:54:33 2009 +0100 +++ b/src/HOL/Tools/refute.ML Fri Mar 06 17:21:17 2009 +0100 @@ -2662,8 +2662,6 @@ | _ => (* head of term is not a constant *) NONE; - (* TODO: Fix all occurrences of Type ("set", _). *) - (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) @@ -2702,7 +2700,8 @@ fun Finite_Set_card_interpreter thy model args t = case t of Const (@{const_name Finite_Set.card}, - Type ("fun", [Type ("set", [T]), Type ("nat", [])])) => + Type ("fun", [Type ("fun", [T, Type ("bool", [])]), + Type ("nat", [])])) => let (* interpretation -> int *) fun number_of_elements (Node xs) = @@ -2732,7 +2731,8 @@ else Leaf (replicate size_of_nat False) end - val set_constants = make_constants thy model (Type ("set", [T])) + val set_constants = + make_constants thy model (Type ("fun", [T, Type ("bool", [])])) in SOME (Node (map card set_constants), model, args) end @@ -2749,14 +2749,17 @@ fun Finite_Set_finite_interpreter thy model args t = case t of Const (@{const_name Finite_Set.finite}, - Type ("fun", [Type ("set", [T]), Type ("bool", [])])) $ _ => + Type ("fun", [Type ("fun", [T, Type ("bool", [])]), + Type ("bool", [])])) $ _ => (* we only consider finite models anyway, hence EVERY set is *) (* "finite" *) SOME (TT, model, args) | Const (@{const_name Finite_Set.finite}, - Type ("fun", [Type ("set", [T]), Type ("bool", [])])) => + Type ("fun", [Type ("fun", [T, Type ("bool", [])]), + Type ("bool", [])])) => let - val size_of_set = size_of_type thy model (Type ("set", [T])) + val size_of_set = + size_of_type thy model (Type ("fun", [T, Type ("bool", [])])) in (* we only consider finite models anyway, hence EVERY set is *) (* "finite" *) @@ -2982,16 +2985,20 @@ fun lfp_interpreter thy model args t = case t of Const (@{const_name lfp}, Type ("fun", [Type ("fun", - [Type ("set", [T]), Type ("set", [_])]), Type ("set", [_])])) => + [Type ("fun", [T, Type ("bool", [])]), + Type ("fun", [_, Type ("bool", [])])]), + Type ("fun", [_, Type ("bool", [])])])) => let val size_elem = size_of_type thy model T (* the universe (i.e. the set that contains every element) *) val i_univ = Node (replicate size_elem TT) (* all sets with elements from type 'T' *) - val i_sets = make_constants thy model (Type ("set", [T])) + val i_sets = + make_constants thy model (Type ("fun", [T, Type ("bool", [])])) (* all functions that map sets to sets *) val i_funs = make_constants thy model (Type ("fun", - [Type ("set", [T]), Type ("set", [T])])) + [Type ("fun", [T, Type ("bool", [])]), + Type ("fun", [T, Type ("bool", [])])])) (* "lfp(f) == Inter({u. f(u) <= u})" *) (* interpretation * interpretation -> bool *) fun is_subset (Node subs, Node sups) = @@ -3033,16 +3040,20 @@ fun gfp_interpreter thy model args t = case t of Const (@{const_name gfp}, Type ("fun", [Type ("fun", - [Type ("set", [T]), Type ("set", [_])]), Type ("set", [_])])) => + [Type ("fun", [T, Type ("bool", [])]), + Type ("fun", [_, Type ("bool", [])])]), + Type ("fun", [_, Type ("bool", [])])])) => let nonfix union (* because "union" is used below *) val size_elem = size_of_type thy model T (* the universe (i.e. the set that contains every element) *) val i_univ = Node (replicate size_elem TT) (* all sets with elements from type 'T' *) - val i_sets = make_constants thy model (Type ("set", [T])) + val i_sets = + make_constants thy model (Type ("fun", [T, Type ("bool", [])])) (* all functions that map sets to sets *) val i_funs = make_constants thy model (Type ("fun", - [Type ("set", [T]), Type ("set", [T])])) + [Type ("fun", [T, Type ("bool", [])]), + Type ("fun", [T, Type ("bool", [])])])) (* "gfp(f) == Union({u. u <= f(u)})" *) (* interpretation * interpretation -> bool *) fun is_subset (Node subs, Node sups) =