--- a/src/HOL/Tools/refute.ML Fri Jan 19 21:20:10 2007 +0100
+++ b/src/HOL/Tools/refute.ML Fri Jan 19 22:04:22 2007 +0100
@@ -704,6 +704,7 @@
(* other optimizations *)
| Const ("Finite_Set.card", _) => t
| Const ("Finite_Set.Finites", _) => t
+ | Const ("Finite_Set.finite", _) => t
| Const ("Orderings.less", Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
| Const ("HOL.plus", Type ("fun", [Type ("nat", []),
@@ -890,6 +891,7 @@
(* other optimizations *)
| Const ("Finite_Set.card", T) => collect_type_axioms (axs, T)
| Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
+ | Const ("Finite_Set.finite", T) => collect_type_axioms (axs, T)
| Const ("Orderings.less", T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
collect_type_axioms (axs, T)
@@ -2580,6 +2582,35 @@
(* theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option *)
+ (* only an optimization: 'finite' could in principle be interpreted with *)
+ (* interpreters available already (using its definition), but the code *)
+ (* below is more efficient *)
+
+ fun Finite_Set_finite_interpreter thy model args t =
+ case t of
+ Const ("Finite_Set.finite",
+ Type ("fun", [Type ("set", [T]), Type ("bool", [])])) $ _ =>
+ (* we only consider finite models anyway, hence EVERY set is *)
+ (* "finite" *)
+ SOME (TT, model, args)
+ | Const ("Finite_Set.finite",
+ Type ("fun", [Type ("set", [T]), Type ("bool", [])])) =>
+ let
+ val (i_set, _, _) = interpret thy model
+ {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True}
+ (Free ("dummy", Type ("set", [T])))
+ val size_set = size_of_type i_set
+ in
+ (* we only consider finite models anyway, hence EVERY set is *)
+ (* "finite" *)
+ SOME (Node (replicate size_set TT), model, args)
+ end
+ | _ =>
+ NONE;
+
+ (* theory -> model -> arguments -> Term.term ->
+ (interpretation * model * arguments) option *)
+
(* only an optimization: 'Orderings.less' could in principle be *)
(* interpreted with interpreters available already (using its definition), *)
(* but the code below is more efficient *)
@@ -3189,6 +3220,7 @@
add_interpreter "IDT_recursion" IDT_recursion_interpreter #>
add_interpreter "Finite_Set.card" Finite_Set_card_interpreter #>
add_interpreter "Finite_Set.Finites" Finite_Set_Finites_interpreter #>
+ add_interpreter "Finite_Set.finite" Finite_Set_finite_interpreter #>
add_interpreter "Nat_Orderings.less" Nat_less_interpreter #>
add_interpreter "Nat_HOL.plus" Nat_plus_interpreter #>
add_interpreter "Nat_HOL.minus" Nat_minus_interpreter #>