# HG changeset patch
# User webertj
# Date 1169240662 -3600
# Node ID 98e3e9f001924d36f70a0d900111c9b4a8226e4e
# Parent  ab3dfcef6489907f911e069aba460a5a599e993a
interpreter for Finite_Set.finite added

diff -r ab3dfcef6489 -r 98e3e9f00192 src/HOL/Tools/refute.ML
--- 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 #>
diff -r ab3dfcef6489 -r 98e3e9f00192 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Fri Jan 19 21:20:10 2007 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Fri Jan 19 22:04:22 2007 +0100
@@ -980,6 +980,10 @@
   refute
 oops
 
+lemma "x \<in> Finites"
+  refute  -- {* no finite countermodel exists *}
+oops
+
 lemma "finite x"
   refute  -- {* no finite countermodel exists *}
 oops