interpreter for Finite_Set.Finites added
authorwebertj
Thu Mar 03 17:22:46 2005 +0100 (2005-03-03)
changeset 15571c166086feace
parent 15570 8d8c70b41bab
child 15572 9c89b1adf573
interpreter for Finite_Set.Finites added
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Mar 03 12:43:01 2005 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Mar 03 17:22:46 2005 +0100
     1.3 @@ -619,6 +619,7 @@
     1.4  			| Const ("op :", T)               => collect_type_axioms (axs, T)
     1.5  			(* other optimizations *)
     1.6  			| Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)
     1.7 +			| Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
     1.8  			| Const ("op <", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T)
     1.9  			| Const ("op +", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    1.10  			| Const ("op -", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    1.11 @@ -2064,6 +2065,25 @@
    1.12  
    1.13  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
    1.14  
    1.15 +	(* only an optimization: 'Finites' could in principle be interpreted with *)
    1.16 +	(* interpreters available already (using its definition), but the code    *)
    1.17 +	(* below is more efficient                                                *)
    1.18 +
    1.19 +	fun Finite_Set_Finites_interpreter thy model args t =
    1.20 +		case t of
    1.21 +		  Const ("Finite_Set.Finites", Type ("set", [Type ("set", [T])])) =>
    1.22 +			let
    1.23 +				val (i_set, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("set", [T])))
    1.24 +				val size_set      = size_of_type i_set
    1.25 +			in
    1.26 +				(* we only consider finite models anyway, hence EVERY set is in "Finites" *)
    1.27 +				SOME (Node (replicate size_set TT), model, args)
    1.28 +			end
    1.29 +		| _ =>
    1.30 +			NONE;
    1.31 +
    1.32 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
    1.33 +
    1.34  	(* only an optimization: 'op <' could in principle be interpreted with    *)
    1.35  	(* interpreters available already (using its definition), but the code    *)
    1.36  	(* below is more efficient                                                *)
    1.37 @@ -2388,18 +2408,19 @@
    1.38  
    1.39  	val setup =
    1.40  		[RefuteData.init,
    1.41 -		 add_interpreter "stlc"            stlc_interpreter,
    1.42 -		 add_interpreter "Pure"            Pure_interpreter,
    1.43 -		 add_interpreter "HOLogic"         HOLogic_interpreter,
    1.44 -		 add_interpreter "set"             set_interpreter,
    1.45 +		 add_interpreter "stlc"    stlc_interpreter,
    1.46 +		 add_interpreter "Pure"    Pure_interpreter,
    1.47 +		 add_interpreter "HOLogic" HOLogic_interpreter,
    1.48 +		 add_interpreter "set"     set_interpreter,
    1.49  		 add_interpreter "IDT"             IDT_interpreter,
    1.50  		 add_interpreter "IDT_constructor" IDT_constructor_interpreter,
    1.51  		 add_interpreter "IDT_recursion"   IDT_recursion_interpreter,
    1.52 -		 add_interpreter "Finite_Set.card" Finite_Set_card_interpreter,
    1.53 -		 add_interpreter "Nat.op <"        Nat_less_interpreter,
    1.54 -		 add_interpreter "Nat.op +"        Nat_plus_interpreter,
    1.55 -		 add_interpreter "Nat.op -"        Nat_minus_interpreter,
    1.56 -		 add_interpreter "Nat.op *"        Nat_mult_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 "Nat.op <" Nat_less_interpreter,
    1.60 +		 add_interpreter "Nat.op +" Nat_plus_interpreter,
    1.61 +		 add_interpreter "Nat.op -" Nat_minus_interpreter,
    1.62 +		 add_interpreter "Nat.op *" Nat_mult_interpreter,
    1.63  		 add_printer "stlc" stlc_printer,
    1.64  		 add_printer "set"  set_printer,
    1.65  		 add_printer "IDT"  IDT_printer];