src/HOL/Tools/refute.ML
changeset 21267 5294ecae6708
parent 21098 d0d8a48ae4e6
child 21556 e0ffb2d13f9f
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Nov 09 16:14:43 2006 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Nov 09 18:48:45 2006 +0100
     1.3 @@ -628,6 +628,8 @@
     1.4  			| Const ("List.op @", T)          => collect_type_axioms (axs, T)
     1.5  			| Const ("Lfp.lfp", T)            => collect_type_axioms (axs, T)
     1.6  			| Const ("Gfp.gfp", T)            => collect_type_axioms (axs, T)
     1.7 +			| Const ("fst", T)                => collect_type_axioms (axs, T)
     1.8 +			| Const ("snd", T)                => collect_type_axioms (axs, T)
     1.9  			(* simply-typed lambda calculus *)
    1.10  			| Const (s, T)                    =>
    1.11  				let
    1.12 @@ -2376,6 +2378,46 @@
    1.13  		| _ =>
    1.14  			NONE;
    1.15  
    1.16 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
    1.17 +
    1.18 +	(* only an optimization: 'fst' could in principle be interpreted with     *)
    1.19 +	(* interpreters available already (using its definition), but the code    *)
    1.20 +	(* below is more efficient                                                *)
    1.21 +
    1.22 +	fun Product_Type_fst_interpreter thy model args t =
    1.23 +		case t of
    1.24 +		  Const ("fst", Type ("fun", [Type ("*", [T, U]), _])) =>
    1.25 +			let
    1.26 +				val (iT, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
    1.27 +				val is_T       = make_constants iT
    1.28 +				val (iU, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", U))
    1.29 +				val size_U     = size_of_type iU
    1.30 +			in
    1.31 +				SOME (Node (List.concat (map (replicate size_U) is_T)), model, args)
    1.32 +			end
    1.33 +		| _ =>
    1.34 +			NONE;
    1.35 +
    1.36 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
    1.37 +
    1.38 +	(* only an optimization: 'snd' could in principle be interpreted with     *)
    1.39 +	(* interpreters available already (using its definition), but the code    *)
    1.40 +	(* below is more efficient                                                *)
    1.41 +
    1.42 +	fun Product_Type_snd_interpreter thy model args t =
    1.43 +		case t of
    1.44 +		  Const ("snd", Type ("fun", [Type ("*", [T, U]), _])) =>
    1.45 +			let
    1.46 +				val (iT, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
    1.47 +				val size_T     = size_of_type iT
    1.48 +				val (iU, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", U))
    1.49 +				val is_U       = make_constants iU
    1.50 +			in
    1.51 +				SOME (Node (List.concat (replicate size_T is_U)), model, args)
    1.52 +			end
    1.53 +		| _ =>
    1.54 +			NONE;
    1.55 +
    1.56  
    1.57  (* ------------------------------------------------------------------------- *)
    1.58  (* PRINTERS                                                                  *)
    1.59 @@ -2616,6 +2658,8 @@
    1.60  		 add_interpreter "List.op @" List_append_interpreter #>
    1.61  		 add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #>
    1.62  		 add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #>
    1.63 +		 add_interpreter "fst" Product_Type_fst_interpreter #>
    1.64 +		 add_interpreter "snd" Product_Type_snd_interpreter #>
    1.65  		 add_printer "stlc" stlc_printer #>
    1.66  		 add_printer "set"  set_printer #>
    1.67  		 add_printer "IDT"  IDT_printer;