1.1 --- a/src/HOL/Tools/refute.ML	Fri Jan 19 21:20:10 2007 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Jan 19 22:04:22 2007 +0100
     1.3 @@ -704,6 +704,7 @@
     1.4  			(* other optimizations *)
     1.5  			| Const ("Finite_Set.card", _)    => t
     1.6  			| Const ("Finite_Set.Finites", _) => t
     1.7 +			| Const ("Finite_Set.finite", _)  => t
     1.8  			| Const ("Orderings.less", Type ("fun", [Type ("nat", []),
     1.9  				Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
    1.10  			| Const ("HOL.plus", Type ("fun", [Type ("nat", []),
    1.11 @@ -890,6 +891,7 @@
    1.12  			(* other optimizations *)
    1.13  			| Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)
    1.14  			| Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
    1.15 +			| Const ("Finite_Set.finite", T)  => collect_type_axioms (axs, T)
    1.16  			| Const ("Orderings.less", T as Type ("fun", [Type ("nat", []),
    1.17  				Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
    1.18  					collect_type_axioms (axs, T)
    1.19 @@ -2580,6 +2582,35 @@
    1.20  	(* theory -> model -> arguments -> Term.term ->
    1.21  		(interpretation * model * arguments) option *)
    1.22  
    1.23 +	(* only an optimization: 'finite' could in principle be interpreted with  *)
    1.24 +	(* interpreters available already (using its definition), but the code    *)
    1.25 +	(* below is more efficient                                                *)
    1.26 +
    1.27 +	fun Finite_Set_finite_interpreter thy model args t =
    1.28 +		case t of
    1.29 +		  Const ("Finite_Set.finite",
    1.30 +				Type ("fun", [Type ("set", [T]), Type ("bool", [])])) $ _ =>
    1.31 +				(* we only consider finite models anyway, hence EVERY set is *)
    1.32 +				(* "finite"                                                  *)
    1.33 +				SOME (TT, model, args)
    1.34 +		| Const ("Finite_Set.finite",
    1.35 +				Type ("fun", [Type ("set", [T]), Type ("bool", [])])) =>
    1.36 +			let
    1.37 +				val (i_set, _, _) = interpret thy model
    1.38 +					{maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True}
    1.39 +					(Free ("dummy", Type ("set", [T])))
    1.40 +				val size_set      = size_of_type i_set
    1.41 +			in
    1.42 +				(* we only consider finite models anyway, hence EVERY set is *)
    1.43 +				(* "finite"                                                  *)
    1.44 +				SOME (Node (replicate size_set TT), model, args)
    1.45 +			end
    1.46 +		| _ =>
    1.47 +			NONE;
    1.48 +
    1.49 +	(* theory -> model -> arguments -> Term.term ->
    1.50 +		(interpretation * model * arguments) option *)
    1.51 +
    1.52  	(* only an optimization: 'Orderings.less' could in principle be            *)
    1.53  	(* interpreted with interpreters available already (using its definition), *)
    1.54  	(* but the code below is more efficient                                    *)
    1.55 @@ -3189,6 +3220,7 @@
    1.56  		 add_interpreter "IDT_recursion"   IDT_recursion_interpreter #>
    1.57  		 add_interpreter "Finite_Set.card"    Finite_Set_card_interpreter #>
    1.58  		 add_interpreter "Finite_Set.Finites" Finite_Set_Finites_interpreter #>
    1.59 +		 add_interpreter "Finite_Set.finite"  Finite_Set_finite_interpreter #>
    1.60  		 add_interpreter "Nat_Orderings.less" Nat_less_interpreter #>
    1.61  		 add_interpreter "Nat_HOL.plus"       Nat_plus_interpreter #>
    1.62  		 add_interpreter "Nat_HOL.minus"      Nat_minus_interpreter #>

     2.1 --- a/src/HOL/ex/Refute_Examples.thy	Fri Jan 19 21:20:10 2007 +0100
     2.2 +++ b/src/HOL/ex/Refute_Examples.thy	Fri Jan 19 22:04:22 2007 +0100
     2.3 @@ -980,6 +980,10 @@
     2.4    refute
     2.5  oops
     2.6  
     2.7 +lemma "x \<in> Finites"
     2.8 +  refute  -- {* no finite countermodel exists *}
     2.9 +oops
    2.10 +
    2.11  lemma "finite x"
    2.12    refute  -- {* no finite countermodel exists *}
    2.13  oops