src/HOL/Tools/refute.ML
changeset 15283 f21466450330
parent 15280 e0e9bf44afad
child 15292 09e218879265
     1.1 --- a/src/HOL/Tools/refute.ML	Sat Nov 13 17:30:03 2004 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Sun Nov 14 01:40:27 2004 +0100
     1.3 @@ -1141,11 +1141,11 @@
     1.4  			(* unit -> (interpretation * model * arguments) option *)
     1.5  			fun interpret_groundtype () =
     1.6  			let
     1.7 -				val size = (if T = Term.propT then 2 else (the o assoc) (typs, T))  (* the model MUST specify a size for ground types *)
     1.8 -				val next = (if size=2 then next_idx+1 else next_idx+size)  (* optimization for types with size 2 *)
     1.9 -				val _    = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
    1.10 +				val size = (if T = Term.propT then 2 else (the o assoc) (typs, T))                      (* the model MUST specify a size for ground types *)
    1.11 +				val next = (if size=1 then next_idx else if size=2 then next_idx+1 else next_idx+size)  (* optimization for types with size 1 or 2 *)
    1.12 +				val _    = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ())    (* check if 'maxvars' is large enough *)
    1.13  				(* prop_formula list *)
    1.14 -				val fms  = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
    1.15 +				val fms  = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
    1.16  					else (map BoolVar (next_idx upto (next_idx+size-1))))
    1.17  				(* interpretation *)
    1.18  				val intr = Leaf fms
    1.19 @@ -1155,7 +1155,7 @@
    1.20  				(* prop_formula list -> prop_formula *)
    1.21  				fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
    1.22  				(* prop_formula *)
    1.23 -				val wf   = (if size=2 then True else exactly_one_true fms)
    1.24 +				val wf   = (if size=1 then True else if size=2 then True else exactly_one_true fms)
    1.25  			in
    1.26  				(* extend the model, increase 'next_idx', add well-formedness condition *)
    1.27  				Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
    1.28 @@ -1327,7 +1327,7 @@
    1.29  	in
    1.30  	(* ------------------------------------------------------------------------- *)
    1.31  	(* Providing interpretations directly is more efficient than unfolding the   *)
    1.32 -	(* logical constants.  IN HOL however, logical constants can themselves be   *)
    1.33 +	(* logical constants.  In HOL however, logical constants can themselves be   *)
    1.34  	(* arguments.  "All" and "Ex" are then translated just like any other        *)
    1.35  	(* constant, with the relevant axiom being added by 'collect_axioms'.        *)
    1.36  	(* ------------------------------------------------------------------------- *)
    1.37 @@ -1509,10 +1509,10 @@
    1.38  							(* recursively compute the size of the datatype *)
    1.39  							val size     = size_of_dtyp typs' descr typ_assoc constrs
    1.40  							val next_idx = #next_idx args
    1.41 -							val next     = (if size=2 then next_idx+1 else next_idx+size)  (* optimization for types with size 2 *)
    1.42 +							val next     = (if size=1 then next_idx else if size=2 then next_idx+1 else next_idx+size)  (* optimization for types with size 1 or size 2 *)
    1.43  							val _        = (if next-1>(#maxvars args) andalso (#maxvars args)>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
    1.44  							(* prop_formula list *)
    1.45 -							val fms      = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
    1.46 +							val fms      = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
    1.47  								else (map BoolVar (next_idx upto (next_idx+size-1))))
    1.48  							(* interpretation *)
    1.49  							val intr     = Leaf fms
    1.50 @@ -1522,7 +1522,7 @@
    1.51  							(* prop_formula list -> prop_formula *)
    1.52  							fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
    1.53  							(* prop_formula *)
    1.54 -							val wf       = (if size=2 then True else exactly_one_true fms)
    1.55 +							val wf       = (if size=1 then True else if size=2 then True else exactly_one_true fms)
    1.56  						in
    1.57  							(* extend the model, increase 'next_idx', add well-formedness condition *)
    1.58  							Some (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, next_idx = next, bounds = #bounds args, wellformed = SAnd (#wellformed args, wf)})