src/HOL/Tools/refute.ML
changeset 15611 c01f11cd08f9
parent 15574 b1d1b5bfc464
child 15767 8ed9fcc004fe
     1.1 --- a/src/HOL/Tools/refute.ML	Tue Mar 15 17:07:41 2005 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Mar 17 01:40:18 2005 +0100
     1.3 @@ -100,7 +100,7 @@
     1.4  
     1.5  	(* 'a tree * 'b tree -> ('a * 'b) tree *)
     1.6  
     1.7 -	fun tree_pair (t1,t2) =
     1.8 +	fun tree_pair (t1, t2) =
     1.9  		case t1 of
    1.10  		  Leaf x =>
    1.11  			(case t2 of
    1.12 @@ -240,7 +240,7 @@
    1.13  			if null typs then
    1.14  				"empty universe (no type variables in term)\n"
    1.15  			else
    1.16 -				"Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs) ^ "\n"
    1.17 +				"Size of types: " ^ commas (map (fn (T, i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs) ^ "\n"
    1.18  		val show_consts_msg =
    1.19  			if not (!show_consts) andalso Library.exists (is_Const o fst) terms then
    1.20  				"set \"show_consts\" to show the interpretation of constants\n"
    1.21 @@ -250,7 +250,7 @@
    1.22  			if null terms then
    1.23  				"empty interpretation (no free variables in term)\n"
    1.24  			else
    1.25 -				space_implode "\n" (List.mapPartial (fn (t,intr) =>
    1.26 +				space_implode "\n" (List.mapPartial (fn (t, intr) =>
    1.27  					(* print constants only if 'show_consts' is true *)
    1.28  					if (!show_consts) orelse not (is_Const t) then
    1.29  						SOME (Sign.string_of_term (sign_of thy) t ^ ": " ^ Sign.string_of_term (sign_of thy) (print thy model t intr assignment))
    1.30 @@ -1055,7 +1055,7 @@
    1.31  		val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
    1.32  		(* Term.term *)
    1.33  		val ex_closure = Library.foldl
    1.34 -			(fn (t', ((x,i),T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
    1.35 +			(fn (t', ((x, i), T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
    1.36  			(t, vars)
    1.37  		(* If 't' is of type 'propT' (rather than 'boolT'), applying  *)
    1.38  		(* 'HOLogic.exists_const' is not type-correct.  However, this *)
    1.39 @@ -1117,7 +1117,7 @@
    1.40  			map (fn x => [x]) xs
    1.41  		  | pick_all n xs =
    1.42  			let val rec_pick = pick_all (n-1) xs in
    1.43 -				Library.foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
    1.44 +				Library.foldl (fn (acc, x) => (cons_list x rec_pick) @ acc) ([], xs)
    1.45  			end
    1.46  	in
    1.47  		case intr of
    1.48 @@ -1134,11 +1134,11 @@
    1.49  
    1.50  	fun size_of_type intr =
    1.51  	let
    1.52 -		(* power(a,b) computes a^b, for a>=0, b>=0 *)
    1.53 +		(* power (a, b) computes a^b, for a>=0, b>=0 *)
    1.54  		(* int * int -> int *)
    1.55 -		fun power (a,0) = 1
    1.56 -		  | power (a,1) = a
    1.57 -		  | power (a,b) = let val ab = power(a, b div 2) in ab * ab * power(a, b mod 2) end
    1.58 +		fun power (a, 0) = 1
    1.59 +		  | power (a, 1) = a
    1.60 +		  | power (a, b) = let val ab = power(a, b div 2) in ab * ab * power(a, b mod 2) end
    1.61  	in
    1.62  		case intr of
    1.63  		  Leaf xs => length xs
    1.64 @@ -1270,7 +1270,7 @@
    1.65  			map (fn x => [x]) xs
    1.66  		  | pick_all (xs::xss) =
    1.67  			let val rec_pick = pick_all xss in
    1.68 -				Library.foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
    1.69 +				Library.foldl (fn (acc, x) => (cons_list x rec_pick) @ acc) ([], xs)
    1.70  			end
    1.71  		  | pick_all _ =
    1.72  			raise REFUTE ("interpretation_apply", "empty list (in pick_all)")
    1.73 @@ -1307,7 +1307,7 @@
    1.74  
    1.75  	(* int list -> int *)
    1.76  
    1.77 -	fun sum xs = Library.foldl op+ (0, xs);
    1.78 +	fun sum xs = foldl op+ 0 xs;
    1.79  
    1.80  (* ------------------------------------------------------------------------- *)
    1.81  (* product: returns the product of a list 'xs' of integers                   *)
    1.82 @@ -1315,7 +1315,7 @@
    1.83  
    1.84  	(* int list -> int *)
    1.85  
    1.86 -	fun product xs = Library.foldl op* (1, xs);
    1.87 +	fun product xs = foldl op* 1 xs;
    1.88  
    1.89  (* ------------------------------------------------------------------------- *)
    1.90  (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *)
    1.91 @@ -1750,6 +1750,7 @@
    1.92  									(* int option -- only recursive IDTs have an associated depth *)
    1.93  									val depth = assoc (typs, Type (s', Ts'))
    1.94  									val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s', Ts'), n-1)))
    1.95 +									(* returns an interpretation where everything is mapped to "undefined" *)
    1.96  									(* DatatypeAux.dtyp list -> interpretation *)
    1.97  									fun make_undef [] =
    1.98  										Leaf (replicate total False)
    1.99 @@ -1782,14 +1783,14 @@
   1.100  													raise REFUTE ("IDT_constructor_interpreter", "current size is less than old size")
   1.101  												else
   1.102  													()
   1.103 -											(* elements that exist at the previous depth are mapped to a defined *)
   1.104 -											(* value, while new elements are mapped to "undefined" by the        *)
   1.105 -											(* recursive constructor                                             *)
   1.106  											(* int * interpretation list *)
   1.107  											val (new_offset, intrs) = foldl_map make_constr (offset, replicate size' ds)
   1.108  											(* interpretation list *)
   1.109  											val undefs              = replicate (size - size') (make_undef ds)
   1.110  										in
   1.111 +											(* elements that exist at the previous depth are mapped to a defined *)
   1.112 +											(* value, while new elements are mapped to "undefined" by the        *)
   1.113 +											(* recursive constructor                                             *)
   1.114  											(new_offset, Node (intrs @ undefs))
   1.115  										end
   1.116  									(* extends the interpretation for a constructor (both recursive *)
   1.117 @@ -1799,7 +1800,7 @@
   1.118  										let
   1.119  											(* returns the k-th unit vector of length n *)
   1.120  											(* int * int -> interpretation *)
   1.121 -											fun unit_vector (k,n) =
   1.122 +											fun unit_vector (k, n) =
   1.123  												Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
   1.124  											(* int *)
   1.125  											val k = find_index_eq True xs
   1.126 @@ -1812,7 +1813,7 @@
   1.127  											else
   1.128  												(* if the element was already mapped to a defined value, map it *)
   1.129  												(* to the same value again, just extend the length of the leaf, *)
   1.130 -												(* do not increment offset                                      *)
   1.131 +												(* do not increment the 'offset'                                *)
   1.132  												(offset, unit_vector (k+1, total))
   1.133  										end
   1.134  									  | extend_constr (_, [], Node _) =
   1.135 @@ -1842,14 +1843,8 @@
   1.136  									(* DatatypeAux.dtyp list -> bool *)
   1.137  									fun is_rec_constr ds =
   1.138  										Library.exists DatatypeAux.is_rec_type ds
   1.139 -									(* constructors before 'Const (s, T)' generate elements of the datatype, *)
   1.140 -									(* and if the constructor is recursive, then non-recursive constructors  *)
   1.141 -									(* after it generate further elements                                    *)
   1.142 -									val offset = size_of_dtyp thy typs' descr typ_assoc constrs1 +
   1.143 -										(if is_rec_constr ctypes then
   1.144 -											size_of_dtyp thy typs' descr typ_assoc (List.filter (not o is_rec_constr o snd) cs)
   1.145 -										else
   1.146 -											0)
   1.147 +									(* constructors before 'Const (s, T)' generate elements of the datatype *)
   1.148 +									val offset = size_of_dtyp thy typs' descr typ_assoc constrs1
   1.149  								in
   1.150  									case depth of
   1.151  									  NONE =>  (* equivalent to a depth of 1 *)
   1.152 @@ -2011,7 +2006,6 @@
   1.153  									fun toList arr =
   1.154  										Array.foldr op:: [] arr
   1.155  								in
   1.156 -									(* TODO writeln ("REC-OP: " ^ makestring (Node (toList INTRS))); *)
   1.157  									SOME (Node (toList INTRS), model', args')
   1.158  								end
   1.159  						end
   1.160 @@ -2343,9 +2337,7 @@
   1.161  						fun get_constr_args (cname, cargs) =
   1.162  							let
   1.163  								val cTerm      = Const (cname, (map (typ_of_dtyp descr typ_assoc) cargs) ---> Type (s, Ts))
   1.164 -								(*TODO val _          = writeln ("cTerm: " ^ makestring cTerm) *)
   1.165  								val (iC, _, _) = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
   1.166 -								(*TODO val _          = writeln ("iC: " ^ makestring iC) *)
   1.167  								(* interpretation -> int list option *)
   1.168  								fun get_args (Leaf xs) =
   1.169  									if find_index_eq True xs = element then