src/HOL/Tools/refute.ML
author webertj
Sat Jan 10 13:35:10 2004 +0100 (2004-01-10)
changeset 14350 41b32020d0b3
child 14351 cd3ef10d02be
permissions -rw-r--r--
Adding 'refute' to HOL.
webertj@14350
     1
(*  Title:      HOL/Tools/refute.ML
webertj@14350
     2
    ID:         $Id$
webertj@14350
     3
    Author:     Tjark Weber
webertj@14350
     4
    Copyright   2003-2004
webertj@14350
     5
webertj@14350
     6
Finite model generation for HOL formulae, using an external SAT solver.
webertj@14350
     7
*)
webertj@14350
     8
webertj@14350
     9
(* ------------------------------------------------------------------------- *)
webertj@14350
    10
(* Declares the 'REFUTE' signature as well as a structure 'Refute'.  See     *)
webertj@14350
    11
(* 'find_model' below for a description of the implemented algorithm, and    *)
webertj@14350
    12
(* the Isabelle/Isar theories 'HOL/Refute.thy' and 'HOL/Main.thy' on how to  *)
webertj@14350
    13
(* set things up.                                                            *)
webertj@14350
    14
(* ------------------------------------------------------------------------- *)
webertj@14350
    15
webertj@14350
    16
signature REFUTE =
webertj@14350
    17
sig
webertj@14350
    18
webertj@14350
    19
	(* We use 'REFUTE' only for internal error conditions that should    *)
webertj@14350
    20
	(* never occur in the first place (i.e. errors caused by bugs in our *)
webertj@14350
    21
	(* code).  Otherwise (e.g. to indicate invalid input data) we use    *)
webertj@14350
    22
	(* 'error'.                                                          *)
webertj@14350
    23
webertj@14350
    24
	exception REFUTE of string * string;	(* ("in function", "cause") *)
webertj@14350
    25
webertj@14350
    26
	val setup : (theory -> theory) list
webertj@14350
    27
webertj@14350
    28
	val set_default_param : (string * string) -> theory -> theory
webertj@14350
    29
	val get_default_param : theory -> string -> string option
webertj@14350
    30
	val get_default_params : theory -> (string * string) list
webertj@14350
    31
webertj@14350
    32
	val find_model : theory -> (string * string) list -> Term.term -> unit
webertj@14350
    33
webertj@14350
    34
	val refute_term : theory -> (string * string) list -> Term.term -> unit
webertj@14350
    35
	val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
webertj@14350
    36
end;
webertj@14350
    37
webertj@14350
    38
webertj@14350
    39
structure Refute : REFUTE =
webertj@14350
    40
struct
webertj@14350
    41
	exception REFUTE of string * string;
webertj@14350
    42
webertj@14350
    43
	exception EMPTY_DATATYPE;
webertj@14350
    44
webertj@14350
    45
	structure RefuteDataArgs =
webertj@14350
    46
	struct
webertj@14350
    47
		val name = "Refute/refute";
webertj@14350
    48
		type T = string Symtab.table;
webertj@14350
    49
		val empty = Symtab.empty;
webertj@14350
    50
		val copy = I;
webertj@14350
    51
		val prep_ext = I;
webertj@14350
    52
		val merge =
webertj@14350
    53
			fn (symTable1, symTable2) =>
webertj@14350
    54
				(Symtab.merge (op =) (symTable1, symTable2));
webertj@14350
    55
		fun print sg symTable =
webertj@14350
    56
			writeln
webertj@14350
    57
				("'refute', default parameters:\n" ^
webertj@14350
    58
				(space_implode "\n" (map (fn (name,value) => name ^ " = " ^ value) (Symtab.dest symTable))))
webertj@14350
    59
	end;
webertj@14350
    60
webertj@14350
    61
	structure RefuteData = TheoryDataFun(RefuteDataArgs);
webertj@14350
    62
webertj@14350
    63
webertj@14350
    64
(* ------------------------------------------------------------------------- *)
webertj@14350
    65
(* INTERFACE, PART 1: INITIALIZATION, PARAMETER MANAGEMENT                   *)
webertj@14350
    66
(* ------------------------------------------------------------------------- *)
webertj@14350
    67
webertj@14350
    68
(* ------------------------------------------------------------------------- *)
webertj@14350
    69
(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
webertj@14350
    70
(* structure                                                                 *)
webertj@14350
    71
(* ------------------------------------------------------------------------- *)
webertj@14350
    72
webertj@14350
    73
	val setup = [RefuteData.init];
webertj@14350
    74
webertj@14350
    75
(* ------------------------------------------------------------------------- *)
webertj@14350
    76
(* set_default_param: stores the '(name, value)' pair in RefuteData's symbol *)
webertj@14350
    77
(*                    table                                                  *)
webertj@14350
    78
(* ------------------------------------------------------------------------- *)
webertj@14350
    79
webertj@14350
    80
	fun set_default_param (name, value) thy =
webertj@14350
    81
	let
webertj@14350
    82
		val symTable = RefuteData.get thy
webertj@14350
    83
	in
webertj@14350
    84
		case Symtab.lookup (symTable, name) of
webertj@14350
    85
			None   => RefuteData.put (Symtab.extend (symTable, [(name, value)])) thy
webertj@14350
    86
		|	Some _ => RefuteData.put (Symtab.update ((name, value), symTable)) thy
webertj@14350
    87
	end;
webertj@14350
    88
webertj@14350
    89
(* ------------------------------------------------------------------------- *)
webertj@14350
    90
(* get_default_param: retrieves the value associated with 'name' from        *)
webertj@14350
    91
(*                    RefuteData's symbol table                              *)
webertj@14350
    92
(* ------------------------------------------------------------------------- *)
webertj@14350
    93
webertj@14350
    94
	fun get_default_param thy name = Symtab.lookup (RefuteData.get thy, name);
webertj@14350
    95
webertj@14350
    96
(* ------------------------------------------------------------------------- *)
webertj@14350
    97
(* get_default_params: returns a list of all '(name, value)' pairs that are  *)
webertj@14350
    98
(*                     stored in RefuteData's symbol table                   *)
webertj@14350
    99
(* ------------------------------------------------------------------------- *)
webertj@14350
   100
webertj@14350
   101
	fun get_default_params thy = Symtab.dest (RefuteData.get thy);
webertj@14350
   102
webertj@14350
   103
webertj@14350
   104
(* ------------------------------------------------------------------------- *)
webertj@14350
   105
(* PROPOSITIONAL FORMULAS                                                    *)
webertj@14350
   106
(* ------------------------------------------------------------------------- *)
webertj@14350
   107
webertj@14350
   108
(* ------------------------------------------------------------------------- *)
webertj@14350
   109
(* prop_formula: formulas of propositional logic, built from boolean         *)
webertj@14350
   110
(*               variables (referred to by index) and True/False using       *)
webertj@14350
   111
(*               not/or/and                                                  *)
webertj@14350
   112
(* ------------------------------------------------------------------------- *)
webertj@14350
   113
webertj@14350
   114
	datatype prop_formula =
webertj@14350
   115
		  True
webertj@14350
   116
		| False
webertj@14350
   117
		| BoolVar of int
webertj@14350
   118
		| Not of prop_formula
webertj@14350
   119
		| Or of prop_formula * prop_formula
webertj@14350
   120
		| And of prop_formula * prop_formula;
webertj@14350
   121
webertj@14350
   122
	(* the following constructor functions make sure that True and False do *)
webertj@14350
   123
	(* not occur within any of the other connectives (i.e. Not, Or, And)    *)
webertj@14350
   124
webertj@14350
   125
	(* prop_formula -> prop_formula *)
webertj@14350
   126
webertj@14350
   127
	fun SNot True  = False
webertj@14350
   128
	  | SNot False = True
webertj@14350
   129
	  | SNot fm    = Not fm;
webertj@14350
   130
webertj@14350
   131
	(* prop_formula * prop_formula -> prop_formula *)
webertj@14350
   132
webertj@14350
   133
	fun SOr (True, _)   = True
webertj@14350
   134
	  | SOr (_, True)   = True
webertj@14350
   135
	  | SOr (False, fm) = fm
webertj@14350
   136
	  | SOr (fm, False) = fm
webertj@14350
   137
	  | SOr (fm1, fm2)  = Or (fm1, fm2);
webertj@14350
   138
webertj@14350
   139
	(* prop_formula * prop_formula -> prop_formula *)
webertj@14350
   140
webertj@14350
   141
	fun SAnd (True, fm) = fm
webertj@14350
   142
	  | SAnd (fm, True) = fm
webertj@14350
   143
	  | SAnd (False, _) = False
webertj@14350
   144
	  | SAnd (_, False) = False
webertj@14350
   145
	  | SAnd (fm1, fm2) = And (fm1, fm2);
webertj@14350
   146
webertj@14350
   147
(* ------------------------------------------------------------------------- *)
webertj@14350
   148
(* list_disjunction: computes the disjunction of a list of propositional     *)
webertj@14350
   149
(*                   formulas                                                *)
webertj@14350
   150
(* ------------------------------------------------------------------------- *)
webertj@14350
   151
webertj@14350
   152
	(* prop_formula list -> prop_formula *)
webertj@14350
   153
webertj@14350
   154
	fun list_disjunction []      = False
webertj@14350
   155
	  | list_disjunction (x::xs) = SOr (x, list_disjunction xs);
webertj@14350
   156
webertj@14350
   157
(* ------------------------------------------------------------------------- *)
webertj@14350
   158
(* list_conjunction: computes the conjunction of a list of propositional     *)
webertj@14350
   159
(*                   formulas                                                *)
webertj@14350
   160
(* ------------------------------------------------------------------------- *)
webertj@14350
   161
webertj@14350
   162
	(* prop_formula list -> prop_formula *)
webertj@14350
   163
webertj@14350
   164
	fun list_conjunction []      = True
webertj@14350
   165
	  | list_conjunction (x::xs) = SAnd (x, list_conjunction xs);
webertj@14350
   166
webertj@14350
   167
(* ------------------------------------------------------------------------- *)
webertj@14350
   168
(* prop_formula_dot_product: [x1,...,xn] * [y1,...,yn] -> x1*y1+...+xn*yn    *)
webertj@14350
   169
(* ------------------------------------------------------------------------- *)
webertj@14350
   170
webertj@14350
   171
	(* prop_formula list * prop_formula list -> prop_formula *)
webertj@14350
   172
webertj@14350
   173
	fun prop_formula_dot_product ([],[])       = False
webertj@14350
   174
	  | prop_formula_dot_product (x::xs,y::ys) = SOr (SAnd (x,y), prop_formula_dot_product (xs,ys))
webertj@14350
   175
	  | prop_formula_dot_product (_,_)         = raise REFUTE ("prop_formula_dot_product", "lists are of different length");
webertj@14350
   176
webertj@14350
   177
(* ------------------------------------------------------------------------- *)
webertj@14350
   178
(* prop_formula_to_nnf: computes the negation normal form of a formula 'fm'  *)
webertj@14350
   179
(*                      of propositional logic (i.e. only variables may be   *)
webertj@14350
   180
(*                      negated, but not subformulas)                        *)
webertj@14350
   181
(* ------------------------------------------------------------------------- *)
webertj@14350
   182
webertj@14350
   183
	(* prop_formula -> prop_formula *)
webertj@14350
   184
webertj@14350
   185
	fun prop_formula_to_nnf fm =
webertj@14350
   186
		case fm of
webertj@14350
   187
		(* constants *)
webertj@14350
   188
		  True                => True
webertj@14350
   189
		| False               => False
webertj@14350
   190
		(* literals *)
webertj@14350
   191
		| BoolVar i           => BoolVar i
webertj@14350
   192
		| Not (BoolVar i)     => Not (BoolVar i)
webertj@14350
   193
		(* double-negation elimination *)
webertj@14350
   194
		| Not (Not fm)        => prop_formula_to_nnf fm
webertj@14350
   195
		(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
webertj@14350
   196
		| Not (Or  (fm1,fm2)) => SAnd (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
webertj@14350
   197
		| Not (And (fm1,fm2)) => SOr  (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
webertj@14350
   198
		(* 'or' and 'and' as outermost connectives are left untouched *)
webertj@14350
   199
		| Or  (fm1,fm2)       => SOr  (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
webertj@14350
   200
		| And (fm1,fm2)       => SAnd (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
webertj@14350
   201
		(* 'not' + constant *)
webertj@14350
   202
		| Not _               => raise REFUTE ("prop_formula_to_nnf", "'True'/'False' not allowed inside of 'Not'");
webertj@14350
   203
webertj@14350
   204
(* ------------------------------------------------------------------------- *)
webertj@14350
   205
(* prop_formula_nnf_to_cnf: computes the conjunctive normal form of a        *)
webertj@14350
   206
(*      formula 'fm' of propositional logic that is given in negation normal *)
webertj@14350
   207
(*      form.  Note that there may occur an exponential blowup of the        *)
webertj@14350
   208
(*      formula.                                                             *)
webertj@14350
   209
(* ------------------------------------------------------------------------- *)
webertj@14350
   210
webertj@14350
   211
	(* prop_formula -> prop_formula *)
webertj@14350
   212
webertj@14350
   213
	fun prop_formula_nnf_to_cnf fm =
webertj@14350
   214
		case fm of
webertj@14350
   215
		(* constants *)
webertj@14350
   216
		  True            => True
webertj@14350
   217
		| False           => False
webertj@14350
   218
		(* literals *)
webertj@14350
   219
		| BoolVar i       => BoolVar i
webertj@14350
   220
		| Not (BoolVar i) => Not (BoolVar i)
webertj@14350
   221
		(* pushing 'or' inside of 'and' using distributive laws *)
webertj@14350
   222
		| Or (fm1,fm2)    =>
webertj@14350
   223
			let
webertj@14350
   224
				val fm1' = prop_formula_nnf_to_cnf fm1
webertj@14350
   225
				val fm2' = prop_formula_nnf_to_cnf fm2
webertj@14350
   226
			in
webertj@14350
   227
				case fm1' of
webertj@14350
   228
				  And (fm11,fm12) => prop_formula_nnf_to_cnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2')))
webertj@14350
   229
				| _               =>
webertj@14350
   230
					(case fm2' of
webertj@14350
   231
					  And (fm21,fm22) => prop_formula_nnf_to_cnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22)))
webertj@14350
   232
					(* neither subformula contains 'and' *)
webertj@14350
   233
					| _               => fm)
webertj@14350
   234
			end
webertj@14350
   235
		(* 'and' as outermost connective is left untouched *)
webertj@14350
   236
		| And (fm1,fm2)   => SAnd (prop_formula_nnf_to_cnf fm1, prop_formula_nnf_to_cnf fm2)
webertj@14350
   237
		(* error *)
webertj@14350
   238
		| _               => raise REFUTE ("prop_formula_nnf_to_cnf", "formula is not in negation normal form");
webertj@14350
   239
webertj@14350
   240
(* ------------------------------------------------------------------------- *)
webertj@14350
   241
(* max: computes the maximum of two integer values 'i' and 'j'               *)
webertj@14350
   242
(* ------------------------------------------------------------------------- *)
webertj@14350
   243
webertj@14350
   244
	(* int * int -> int *)
webertj@14350
   245
webertj@14350
   246
	fun max (i,j) =
webertj@14350
   247
		if (i>j) then i else j;
webertj@14350
   248
webertj@14350
   249
(* ------------------------------------------------------------------------- *)
webertj@14350
   250
(* max_var_index: computes the maximal variable index occuring in 'fm',      *)
webertj@14350
   251
(*      where 'fm' is a formula of propositional logic                       *)
webertj@14350
   252
(* ------------------------------------------------------------------------- *)
webertj@14350
   253
webertj@14350
   254
	(* prop_formula -> int *)
webertj@14350
   255
webertj@14350
   256
	fun max_var_index fm =
webertj@14350
   257
		case fm of
webertj@14350
   258
		  True          => 0
webertj@14350
   259
		| False         => 0
webertj@14350
   260
		| BoolVar i     => i
webertj@14350
   261
		| Not fm1       => max_var_index fm1
webertj@14350
   262
		| And (fm1,fm2) => max (max_var_index fm1, max_var_index fm2)
webertj@14350
   263
		| Or (fm1,fm2)  => max (max_var_index fm1, max_var_index fm2);
webertj@14350
   264
webertj@14350
   265
(* ------------------------------------------------------------------------- *)
webertj@14350
   266
(* prop_formula_nnf_to_def_cnf: computes the definitional conjunctive normal *)
webertj@14350
   267
(*      form of a formula 'fm' of propositional logic that is given in       *)
webertj@14350
   268
(*      negation normal form.  To avoid an exponential blowup of the         *)
webertj@14350
   269
(*      formula, auxiliary variables may be introduced.  The result formula  *)
webertj@14350
   270
(*      is SAT-equivalent to 'fm' (i.e. it is satisfiable if and only if     *)
webertj@14350
   271
(*      'fm' is satisfiable).                                                *)
webertj@14350
   272
(* ------------------------------------------------------------------------- *)
webertj@14350
   273
webertj@14350
   274
	(* prop_formula -> prop_formula *)
webertj@14350
   275
webertj@14350
   276
	fun prop_formula_nnf_to_def_cnf fm =
webertj@14350
   277
	let
webertj@14350
   278
		(* prop_formula * int -> prop_formula * int *)
webertj@14350
   279
		fun prop_formula_nnf_to_def_cnf_new (fm,new) =
webertj@14350
   280
		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
webertj@14350
   281
			case fm of
webertj@14350
   282
			(* constants *)
webertj@14350
   283
			  True            => (True, new)
webertj@14350
   284
			| False           => (False, new)
webertj@14350
   285
			(* literals *)
webertj@14350
   286
			| BoolVar i       => (BoolVar i, new)
webertj@14350
   287
			| Not (BoolVar i) => (Not (BoolVar i), new)
webertj@14350
   288
			(* pushing 'or' inside of 'and' using distributive laws *)
webertj@14350
   289
			| Or (fm1,fm2)    =>
webertj@14350
   290
				let
webertj@14350
   291
					val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
webertj@14350
   292
					val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
webertj@14350
   293
				in
webertj@14350
   294
					case fst fm1' of
webertj@14350
   295
					  And (fm11,fm12) =>
webertj@14350
   296
						let
webertj@14350
   297
							val aux = BoolVar (snd fm2')
webertj@14350
   298
						in
webertj@14350
   299
							(* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *)
webertj@14350
   300
							prop_formula_nnf_to_def_cnf_new (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fst fm2', Not aux)), (snd fm2')+1)
webertj@14350
   301
						end
webertj@14350
   302
					| _               =>
webertj@14350
   303
						(case fst fm2' of
webertj@14350
   304
						  And (fm21,fm22) =>
webertj@14350
   305
							let
webertj@14350
   306
								val aux = BoolVar (snd fm2')
webertj@14350
   307
							in
webertj@14350
   308
								(* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *)
webertj@14350
   309
								prop_formula_nnf_to_def_cnf_new (SAnd (SOr (fst fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), (snd fm2')+1)
webertj@14350
   310
							end
webertj@14350
   311
						(* neither subformula contains 'and' *)
webertj@14350
   312
						| _               => (fm, new))
webertj@14350
   313
				end
webertj@14350
   314
			(* 'and' as outermost connective is left untouched *)
webertj@14350
   315
			| And (fm1,fm2)   =>
webertj@14350
   316
				let
webertj@14350
   317
					val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
webertj@14350
   318
					val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
webertj@14350
   319
				in
webertj@14350
   320
					(SAnd (fst fm1', fst fm2'), snd fm2')
webertj@14350
   321
				end
webertj@14350
   322
			(* error *)
webertj@14350
   323
			| _               => raise REFUTE ("prop_formula_nnf_to_def_cnf", "formula is not in negation normal form")
webertj@14350
   324
	in
webertj@14350
   325
		fst (prop_formula_nnf_to_def_cnf_new (fm, (max_var_index fm)+1))
webertj@14350
   326
	end;
webertj@14350
   327
webertj@14350
   328
(* ------------------------------------------------------------------------- *)
webertj@14350
   329
(* prop_formula_to_cnf: computes the conjunctive normal form of a formula    *)
webertj@14350
   330
(*                      'fm' of propositional logic                          *)
webertj@14350
   331
(* ------------------------------------------------------------------------- *)
webertj@14350
   332
webertj@14350
   333
	(* prop_formula -> prop_formula *)
webertj@14350
   334
webertj@14350
   335
	fun prop_formula_to_cnf fm =
webertj@14350
   336
		prop_formula_nnf_to_cnf (prop_formula_to_nnf fm);
webertj@14350
   337
webertj@14350
   338
(* ------------------------------------------------------------------------- *)
webertj@14350
   339
(* prop_formula_to_def_cnf: computes the definitional conjunctive normal     *)
webertj@14350
   340
(*      form of a formula 'fm' of propositional logic, introducing auxiliary *)
webertj@14350
   341
(*      variables if necessary to avoid an exponential blowup of the formula *)
webertj@14350
   342
(* ------------------------------------------------------------------------- *)
webertj@14350
   343
webertj@14350
   344
	(* prop_formula -> prop_formula *)
webertj@14350
   345
webertj@14350
   346
	fun prop_formula_to_def_cnf fm =
webertj@14350
   347
		prop_formula_nnf_to_def_cnf (prop_formula_to_nnf fm);
webertj@14350
   348
webertj@14350
   349
(* ------------------------------------------------------------------------- *)
webertj@14350
   350
(* prop_formula_to_dimacs_cnf_format: serializes a formula of propositional  *)
webertj@14350
   351
(*      logic to a file in DIMACS CNF format (see "Satisfiability Suggested  *)
webertj@14350
   352
(*      Format", May 8 1993, Section 2.1)                                    *)
webertj@14350
   353
(* fm  : formula to be serialized.  Note: 'fm' must not contain a variable   *)
webertj@14350
   354
(*       index less than 1.                                                  *)
webertj@14350
   355
(* def : If true, translate 'fm' into definitional CNF.  Otherwise translate *)
webertj@14350
   356
(*       'fm' into CNF.                                                      *)
webertj@14350
   357
(* path: path of the file to be created                                      *)
webertj@14350
   358
(* ------------------------------------------------------------------------- *)
webertj@14350
   359
webertj@14350
   360
	(* prop_formula -> bool -> Path.T -> unit *)
webertj@14350
   361
webertj@14350
   362
	fun prop_formula_to_dimacs_cnf_format fm def path =
webertj@14350
   363
	let
webertj@14350
   364
		(* prop_formula *)
webertj@14350
   365
		val cnf =
webertj@14350
   366
			if def then
webertj@14350
   367
				prop_formula_to_def_cnf fm
webertj@14350
   368
			else
webertj@14350
   369
				prop_formula_to_cnf fm
webertj@14350
   370
		val fm' =
webertj@14350
   371
			case cnf of
webertj@14350
   372
			  True  => Or (BoolVar 1, Not (BoolVar 1))
webertj@14350
   373
			| False => And (BoolVar 1, Not (BoolVar 1))
webertj@14350
   374
			| _     => cnf (* either 'cnf'=True/False, or 'cnf' does not contain True/False at all *)
webertj@14350
   375
		(* prop_formula -> int *)
webertj@14350
   376
		fun cnf_number_of_clauses (And (fm1,fm2)) =
webertj@14350
   377
			(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
webertj@14350
   378
		  | cnf_number_of_clauses _ =
webertj@14350
   379
			1
webertj@14350
   380
		(* prop_formula -> string *)
webertj@14350
   381
		fun cnf_prop_formula_to_string (BoolVar i) =
webertj@14350
   382
			if (i<1) then
webertj@14350
   383
				raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains a variable index less than 1")
webertj@14350
   384
			else
webertj@14350
   385
				(string_of_int i)
webertj@14350
   386
		  | cnf_prop_formula_to_string (Not fm1) =
webertj@14350
   387
			"-" ^ (cnf_prop_formula_to_string fm1)
webertj@14350
   388
		  | cnf_prop_formula_to_string (Or (fm1,fm2)) =
webertj@14350
   389
			(cnf_prop_formula_to_string fm1) ^ " " ^ (cnf_prop_formula_to_string fm2)
webertj@14350
   390
		  | cnf_prop_formula_to_string (And (fm1,fm2)) =
webertj@14350
   391
			(cnf_prop_formula_to_string fm1) ^ " 0\n" ^ (cnf_prop_formula_to_string fm2)
webertj@14350
   392
		  | cnf_prop_formula_to_string _ =
webertj@14350
   393
			raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains True/False")
webertj@14350
   394
	in
webertj@14350
   395
		File.write path ("c This file was generated by prop_formula_to_dimacs_cnf_format\n"
webertj@14350
   396
			^ "c (c) Tjark Weber\n"
webertj@14350
   397
			^ "p cnf " ^ (string_of_int (max_var_index fm')) ^ " " ^ (string_of_int (cnf_number_of_clauses fm')) ^ "\n"
webertj@14350
   398
			^ (cnf_prop_formula_to_string fm') ^ "\n")
webertj@14350
   399
	end;
webertj@14350
   400
webertj@14350
   401
(* ------------------------------------------------------------------------- *)
webertj@14350
   402
(* prop_formula_to_dimacs_sat_format: serializes a formula of propositional  *)
webertj@14350
   403
(*      logic to a file in DIMACS SAT format (see "Satisfiability Suggested  *)
webertj@14350
   404
(*      Format", May 8 1993, Section 2.2)                                    *)
webertj@14350
   405
(* fm  : formula to be serialized.  Note: 'fm' must not contain a variable   *)
webertj@14350
   406
(*       index less than 1.                                                  *)
webertj@14350
   407
(* path: path of the file to be created                                      *)
webertj@14350
   408
(* ------------------------------------------------------------------------- *)
webertj@14350
   409
webertj@14350
   410
	(* prop_formula -> Path.T -> unit *)
webertj@14350
   411
webertj@14350
   412
	fun prop_formula_to_dimacs_sat_format fm path =
webertj@14350
   413
	let
webertj@14350
   414
		fun prop_formula_to_string True =
webertj@14350
   415
			"*()"
webertj@14350
   416
		  | prop_formula_to_string False =
webertj@14350
   417
			"+()"
webertj@14350
   418
		  | prop_formula_to_string (BoolVar i) =
webertj@14350
   419
			if (i<1) then
webertj@14350
   420
				raise REFUTE ("prop_formula_to_dimacs_sat_format", "formula contains a variable index less than 1")
webertj@14350
   421
			else
webertj@14350
   422
				(string_of_int i)
webertj@14350
   423
		  | prop_formula_to_string (Not fm1) =
webertj@14350
   424
			"-(" ^ (prop_formula_to_string fm1) ^ ")"
webertj@14350
   425
		  | prop_formula_to_string (Or (fm1,fm2)) =
webertj@14350
   426
			"+(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
webertj@14350
   427
		  | prop_formula_to_string (And (fm1,fm2)) =
webertj@14350
   428
			"*(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
webertj@14350
   429
	in
webertj@14350
   430
		File.write path ("c This file was generated by prop_formula_to_dimacs_sat_format\n"
webertj@14350
   431
			^ "c (c) Tjark Weber\n"
webertj@14350
   432
			^ "p sat " ^ (string_of_int (max (max_var_index fm, 1))) ^ "\n"
webertj@14350
   433
			^ "(" ^ (prop_formula_to_string fm) ^ ")\n")
webertj@14350
   434
	end;
webertj@14350
   435
webertj@14350
   436
(* ------------------------------------------------------------------------- *)
webertj@14350
   437
(* prop_formula_sat_solver: try to find a satisfying assignment for the      *)
webertj@14350
   438
(*      boolean variables in a propositional formula, using an external SAT  *)
webertj@14350
   439
(*      solver.  If the SAT solver did not find an assignment, 'None' is     *)
webertj@14350
   440
(*      returned.  Otherwise 'Some (list of integers)' is returned, where    *)
webertj@14350
   441
(*      i>0 means that the boolean variable i is set to TRUE, and i<0 means  *)
webertj@14350
   442
(*      that the boolean variable i is set to FALSE.  Note that if           *)
webertj@14350
   443
(*      'satformat' is 'defcnf', then the assignment returned may contain    *)
webertj@14350
   444
(*      auxiliary variables that were not present in the original formula    *)
webertj@14350
   445
(*      'fm'.                                                                *)
webertj@14350
   446
(* fm        : formula that is passed to the SAT solver                      *) 
webertj@14350
   447
(* satpath   : path of the file used to store the propositional formula,     *)
webertj@14350
   448
(*             i.e. the input to the SAT solver                              *)
webertj@14350
   449
(* satformat : format of the SAT solver's input file.  Must be either "cnf", *)
webertj@14350
   450
(*             "defcnf", or "sat".                                           *)
webertj@14350
   451
(* resultpath: path of the file containing the SAT solver's output           *)
webertj@14350
   452
(* success   : part of the line in the SAT solver's output that is followed  *)
webertj@14350
   453
(*             by a line consisting of a list of integers representing the   *)
webertj@14350
   454
(*             satisfying assignment                                         *)
webertj@14350
   455
(* command   : system command used to execute the SAT solver                 *)
webertj@14350
   456
(* ------------------------------------------------------------------------- *)
webertj@14350
   457
webertj@14350
   458
	(* prop_formula -> Path.T -> string -> Path.T -> string -> string -> int list option *)
webertj@14350
   459
webertj@14350
   460
	fun prop_formula_sat_solver fm satpath satformat resultpath success command =
webertj@14350
   461
		if File.exists satpath then
webertj@14350
   462
			error ("file '" ^ (Path.pack satpath) ^ "' exists, please delete (will not overwrite)")
webertj@14350
   463
		else if File.exists resultpath then
webertj@14350
   464
			error ("file '" ^ (Path.pack resultpath) ^ "' exists, please delete (will not overwrite)")
webertj@14350
   465
		else
webertj@14350
   466
		(
webertj@14350
   467
			(* serialize the formula 'fm' to a file *)
webertj@14350
   468
			if satformat="cnf" then
webertj@14350
   469
				prop_formula_to_dimacs_cnf_format fm false satpath
webertj@14350
   470
			else if satformat="defcnf" then
webertj@14350
   471
				prop_formula_to_dimacs_cnf_format fm true satpath
webertj@14350
   472
			else if satformat="sat" then
webertj@14350
   473
				prop_formula_to_dimacs_sat_format fm satpath
webertj@14350
   474
			else
webertj@14350
   475
				error ("invalid argument: satformat='" ^ satformat ^ "' (must be either 'cnf', 'defcnf', or 'sat')");
webertj@14350
   476
			(* execute SAT solver *)
webertj@14350
   477
			if (system command)<>0 then
webertj@14350
   478
			(
webertj@14350
   479
				(* error executing SAT solver *)
webertj@14350
   480
				File.rm satpath;
webertj@14350
   481
				File.rm resultpath;
webertj@14350
   482
				error ("system command '" ^ command ^ "' failed (make sure a SAT solver is installed)")
webertj@14350
   483
			)
webertj@14350
   484
			else
webertj@14350
   485
			(
webertj@14350
   486
				(* read assignment from the result file *)
webertj@14350
   487
				File.rm satpath;
webertj@14350
   488
				let
webertj@14350
   489
					(* 'a option -> 'a Library.option *)
webertj@14350
   490
					fun option (SOME a) =
webertj@14350
   491
						Some a
webertj@14350
   492
					  | option NONE =
webertj@14350
   493
						None
webertj@14350
   494
					(* string -> int list *)
webertj@14350
   495
					fun string_to_int_list s =
webertj@14350
   496
						mapfilter (option o LargeInt.fromString) (space_explode " " s)
webertj@14350
   497
					(* string -> string -> bool *)
webertj@14350
   498
					fun is_substring s1 s2 =
webertj@14350
   499
					let
webertj@14350
   500
						val length1 = String.size s1
webertj@14350
   501
						val length2 = String.size s2
webertj@14350
   502
					in
webertj@14350
   503
						if length2 < length1 then
webertj@14350
   504
							false
webertj@14350
   505
						else if s1 = String.substring (s2, 0, length1) then
webertj@14350
   506
							true
webertj@14350
   507
						else is_substring s1 (String.substring (s2, 1, length2-1))
webertj@14350
   508
					end
webertj@14350
   509
					(* string list -> int list option *)
webertj@14350
   510
					fun extract_solution [] =
webertj@14350
   511
						None
webertj@14350
   512
					  | extract_solution (line::lines) =
webertj@14350
   513
						if is_substring success line then
webertj@14350
   514
							(* the next line must be a list of integers *)
webertj@14350
   515
							Some (string_to_int_list (hd lines))
webertj@14350
   516
						else
webertj@14350
   517
							extract_solution lines
webertj@14350
   518
					val sat_result = File.read resultpath
webertj@14350
   519
				in
webertj@14350
   520
					File.rm resultpath;
webertj@14350
   521
					extract_solution (split_lines sat_result)
webertj@14350
   522
				end
webertj@14350
   523
			)
webertj@14350
   524
		);
webertj@14350
   525
webertj@14350
   526
webertj@14350
   527
(* ------------------------------------------------------------------------- *)
webertj@14350
   528
(* TREES                                                                     *)
webertj@14350
   529
(* ------------------------------------------------------------------------- *)
webertj@14350
   530
webertj@14350
   531
(* ------------------------------------------------------------------------- *)
webertj@14350
   532
(* tree: implements an arbitrarily (but finitely) branching tree as a list   *)
webertj@14350
   533
(*       of (lists of ...) elements                                          *)
webertj@14350
   534
(* ------------------------------------------------------------------------- *)
webertj@14350
   535
webertj@14350
   536
	datatype 'a tree =
webertj@14350
   537
		  Leaf of 'a
webertj@14350
   538
		| Node of ('a tree) list;
webertj@14350
   539
webertj@14350
   540
	type prop_tree =
webertj@14350
   541
		prop_formula list tree;
webertj@14350
   542
webertj@14350
   543
	(* ('a -> 'b) -> 'a tree -> 'b tree *)
webertj@14350
   544
webertj@14350
   545
	fun tree_map f tr =
webertj@14350
   546
		case tr of
webertj@14350
   547
		  Leaf x  => Leaf (f x)
webertj@14350
   548
		| Node xs => Node (map (tree_map f) xs);
webertj@14350
   549
webertj@14350
   550
	(* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)
webertj@14350
   551
webertj@14350
   552
	fun tree_foldl f =
webertj@14350
   553
	let
webertj@14350
   554
		fun itl (e, Leaf x)  = f(e,x)
webertj@14350
   555
		  | itl (e, Node xs) = foldl (tree_foldl f) (e,xs)
webertj@14350
   556
	in
webertj@14350
   557
		itl
webertj@14350
   558
	end;
webertj@14350
   559
webertj@14350
   560
	(* 'a tree * 'b tree -> ('a * 'b) tree *)
webertj@14350
   561
webertj@14350
   562
	fun tree_pair (t1,t2) =
webertj@14350
   563
		case t1 of
webertj@14350
   564
		  Leaf x =>
webertj@14350
   565
			(case t2 of
webertj@14350
   566
				  Leaf y => Leaf (x,y)
webertj@14350
   567
				| Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)"))
webertj@14350
   568
		| Node xs =>
webertj@14350
   569
			(case t2 of
webertj@14350
   570
				  (* '~~' will raise an exception if the number of branches in both trees is different at the current node *)
webertj@14350
   571
				  Node ys => Node (map tree_pair (xs ~~ ys))
webertj@14350
   572
				| Leaf _  => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
webertj@14350
   573
webertj@14350
   574
(* ------------------------------------------------------------------------- *)
webertj@14350
   575
(* prop_tree_to_true: returns a propositional formula that is true iff the   *)
webertj@14350
   576
(*      tree denotes the boolean value TRUE                                  *)
webertj@14350
   577
(* ------------------------------------------------------------------------- *)
webertj@14350
   578
webertj@14350
   579
	(* prop_tree -> prop_formula *)
webertj@14350
   580
webertj@14350
   581
	(* a term of type 'bool' is represented as a 2-element leaf, where *)
webertj@14350
   582
	(* the term is true iff the leaf's first element is true           *)
webertj@14350
   583
webertj@14350
   584
	fun prop_tree_to_true (Leaf [fm,_]) =
webertj@14350
   585
		fm
webertj@14350
   586
	  | prop_tree_to_true _ =
webertj@14350
   587
		raise REFUTE ("prop_tree_to_true", "tree is not a 2-element leaf");
webertj@14350
   588
webertj@14350
   589
(* ------------------------------------------------------------------------- *)
webertj@14350
   590
(* prop_tree_to_false: returns a propositional formula that is true iff the  *)
webertj@14350
   591
(*      tree denotes the boolean value FALSE                                 *)
webertj@14350
   592
(* ------------------------------------------------------------------------- *)
webertj@14350
   593
webertj@14350
   594
	(* prop_tree -> prop_formula *)
webertj@14350
   595
webertj@14350
   596
	(* a term of type 'bool' is represented as a 2-element leaf, where *)
webertj@14350
   597
	(* the term is false iff the leaf's second element is true         *)
webertj@14350
   598
webertj@14350
   599
	fun prop_tree_to_false (Leaf [_,fm]) =
webertj@14350
   600
		fm
webertj@14350
   601
	  | prop_tree_to_false _ =
webertj@14350
   602
		raise REFUTE ("prop_tree_to_false", "tree is not a 2-element leaf");
webertj@14350
   603
webertj@14350
   604
(* ------------------------------------------------------------------------- *)
webertj@14350
   605
(* restrict_to_single_element: returns a propositional formula which is true *)
webertj@14350
   606
(*      iff the tree 'tr' describes a single element of its corresponding    *)
webertj@14350
   607
(*      type, i.e. iff at each leaf, one and only one formula is true        *)
webertj@14350
   608
(* ------------------------------------------------------------------------- *)
webertj@14350
   609
webertj@14350
   610
	(* prop_tree -> prop_formula *)
webertj@14350
   611
webertj@14350
   612
	fun restrict_to_single_element tr =
webertj@14350
   613
	let
webertj@14350
   614
		(* prop_formula list -> prop_formula *)
webertj@14350
   615
		fun allfalse []      = True
webertj@14350
   616
		  | allfalse (x::xs) = SAnd (SNot x, allfalse xs)
webertj@14350
   617
		(* prop_formula list -> prop_formula *)
webertj@14350
   618
		fun exactly1true []      = False
webertj@14350
   619
		  | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
webertj@14350
   620
	in
webertj@14350
   621
		case tr of
webertj@14350
   622
		  Leaf [BoolVar _, Not (BoolVar _)] => True (* optimization for boolean variables *)
webertj@14350
   623
		| Leaf xs                           => exactly1true xs
webertj@14350
   624
		| Node trees                        => list_conjunction (map restrict_to_single_element trees)
webertj@14350
   625
	end;
webertj@14350
   626
webertj@14350
   627
(* ------------------------------------------------------------------------- *)
webertj@14350
   628
(* HOL FORMULAS                                                              *)
webertj@14350
   629
(* ------------------------------------------------------------------------- *)
webertj@14350
   630
webertj@14350
   631
(* ------------------------------------------------------------------------- *)
webertj@14350
   632
(* absvar: form an abstraction over a schematic variable                     *)
webertj@14350
   633
(* ------------------------------------------------------------------------- *)
webertj@14350
   634
webertj@14350
   635
	(* Term.indexname * Term.typ * Term.term -> Term.term *)
webertj@14350
   636
webertj@14350
   637
	(* this function is similar to Term.absfree, but for schematic       *)
webertj@14350
   638
	(* variables (rather than free variables)                            *)
webertj@14350
   639
	fun absvar ((x,i),T,body) =
webertj@14350
   640
		Abs(x, T, abstract_over (Var((x,i),T), body));
webertj@14350
   641
webertj@14350
   642
(* ------------------------------------------------------------------------- *)
webertj@14350
   643
(* list_all_var: quantification over a list of schematic variables           *)
webertj@14350
   644
(* ------------------------------------------------------------------------- *)
webertj@14350
   645
webertj@14350
   646
	(* (Term.indexname * Term.typ) list * Term.term -> Term.term *)
webertj@14350
   647
webertj@14350
   648
	(* this function is similar to Term.list_all_free, but for schematic *)
webertj@14350
   649
	(* variables (rather than free variables)                            *)
webertj@14350
   650
	fun list_all_var ([], t) =
webertj@14350
   651
		t
webertj@14350
   652
	  | list_all_var ((idx,T)::vars, t) =
webertj@14350
   653
		(all T) $ (absvar(idx, T, list_all_var(vars,t)));
webertj@14350
   654
webertj@14350
   655
(* ------------------------------------------------------------------------- *)
webertj@14350
   656
(* close_vars: close up a formula over all schematic variables by            *)
webertj@14350
   657
(*             quantification (note that the result term may still contain   *)
webertj@14350
   658
(*             (non-schematic) free variables)                               *)
webertj@14350
   659
(* ------------------------------------------------------------------------- *)
webertj@14350
   660
webertj@14350
   661
	(* Term.term -> Term.term *)
webertj@14350
   662
webertj@14350
   663
	(* this function is similar to Logic.close_form, but for schematic   *)
webertj@14350
   664
	(* variables (rather than free variables)                            *)
webertj@14350
   665
	fun close_vars A =
webertj@14350
   666
		list_all_var (sort_wrt (fst o fst) (map dest_Var (term_vars A)), A);
webertj@14350
   667
webertj@14350
   668
(* ------------------------------------------------------------------------- *)
webertj@14350
   669
(* make_universes: given a list 'xs' of "types" and a universe size 'size',  *)
webertj@14350
   670
(*      this function returns all possible partitions of the universe into   *)
webertj@14350
   671
(*      the "types" in 'xs' such that no "type" is empty.  If 'size' is less *)
webertj@14350
   672
(*      than 'length xs', the returned list of partitions is empty.          *)
webertj@14350
   673
(*      Otherwise, if the list 'xs' is empty, then the returned list of      *)
webertj@14350
   674
(*      partitions contains only the empty list, regardless of 'size'.       *)
webertj@14350
   675
(* ------------------------------------------------------------------------- *)
webertj@14350
   676
webertj@14350
   677
	(* 'a list -> int -> ('a * int) list list *)
webertj@14350
   678
webertj@14350
   679
	fun make_universes xs size =
webertj@14350
   680
	let
webertj@14350
   681
		(* 'a list -> int -> int -> ('a * int) list list *)
webertj@14350
   682
		fun make_partitions_loop (x::xs) 0 total =
webertj@14350
   683
			map (fn us => ((x,0)::us)) (make_partitions xs total)
webertj@14350
   684
		  | make_partitions_loop (x::xs) first total =
webertj@14350
   685
			(map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
webertj@14350
   686
		  | make_partitions_loop _ _ _ =
webertj@14350
   687
			raise REFUTE ("make_universes::make_partitions_loop", "empty list")
webertj@14350
   688
		and
webertj@14350
   689
		(* 'a list -> int -> ('a * int) list list *)
webertj@14350
   690
		make_partitions [x] size =
webertj@14350
   691
			(* we must use all remaining elements on the type 'x', so there is only one partition *)
webertj@14350
   692
			[[(x,size)]]
webertj@14350
   693
		  | make_partitions (x::xs) 0 =
webertj@14350
   694
			(* there are no elements left in the universe, so there is only one partition *)
webertj@14350
   695
			[map (fn t => (t,0)) (x::xs)]
webertj@14350
   696
		  | make_partitions (x::xs) size =
webertj@14350
   697
			(* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
webertj@14350
   698
			make_partitions_loop (x::xs) size size
webertj@14350
   699
		  | make_partitions _ _ =
webertj@14350
   700
			raise REFUTE ("make_universes::make_partitions", "empty list")
webertj@14350
   701
		val len = length xs
webertj@14350
   702
	in
webertj@14350
   703
		if size<len then
webertj@14350
   704
			(* the universe isn't big enough to make every type non-empty *)
webertj@14350
   705
			[]
webertj@14350
   706
		else if xs=[] then
webertj@14350
   707
			(* no types: return one universe, regardless of the size *)
webertj@14350
   708
			[[]]
webertj@14350
   709
		else
webertj@14350
   710
			(* partition into possibly empty types, then add 1 element to each type *)
webertj@14350
   711
			map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
webertj@14350
   712
	end;
webertj@14350
   713
webertj@14350
   714
(* ------------------------------------------------------------------------- *)
webertj@14350
   715
(* sum: computes the sum of a list of integers; sum [] = 0                   *)
webertj@14350
   716
(* ------------------------------------------------------------------------- *)
webertj@14350
   717
webertj@14350
   718
	(* int list -> int *)
webertj@14350
   719
webertj@14350
   720
	fun sum xs = foldl (op +) (0, xs);
webertj@14350
   721
webertj@14350
   722
(* ------------------------------------------------------------------------- *)
webertj@14350
   723
(* product: computes the product of a list of integers; product [] = 1       *)
webertj@14350
   724
(* ------------------------------------------------------------------------- *)
webertj@14350
   725
webertj@14350
   726
	(* int list -> int *)
webertj@14350
   727
webertj@14350
   728
	fun product xs = foldl (op *) (1, xs);
webertj@14350
   729
webertj@14350
   730
(* ------------------------------------------------------------------------- *)
webertj@14350
   731
(* power: power(a,b) computes a^b, for a>=0, b>=0                            *)
webertj@14350
   732
(* ------------------------------------------------------------------------- *)
webertj@14350
   733
webertj@14350
   734
	(* int * int -> int *)
webertj@14350
   735
webertj@14350
   736
	fun power (a,0) = 1
webertj@14350
   737
	  | power (a,1) = a
webertj@14350
   738
	  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end;
webertj@14350
   739
webertj@14350
   740
(* ------------------------------------------------------------------------- *)
webertj@14350
   741
(* size_of_type: returns the size of a type, where 'us' specifies the size   *)
webertj@14350
   742
(*      of each basic type (i.e. each type variable), and 'cdepth' specifies *)
webertj@14350
   743
(*      the maximal constructor depth for inductive datatypes                *)
webertj@14350
   744
(* ------------------------------------------------------------------------- *)
webertj@14350
   745
webertj@14350
   746
	(* Term.typ -> (Term.typ * int) list -> theory -> int -> int *)
webertj@14350
   747
webertj@14350
   748
	fun size_of_type T us thy cdepth =
webertj@14350
   749
	let
webertj@14350
   750
		(* Term.typ -> (Term.typ * int) -> int *)
webertj@14350
   751
		fun lookup_size T [] =
webertj@14350
   752
			raise REFUTE ("size_of_type", "no size specified for type variable '" ^ (Sign.string_of_typ (sign_of thy) T) ^ "'")
webertj@14350
   753
		  | lookup_size T ((typ,size)::pairs) =
webertj@14350
   754
			if T=typ then size else lookup_size T pairs
webertj@14350
   755
	in
webertj@14350
   756
		case T of
webertj@14350
   757
		  Type ("prop", [])     => 2
webertj@14350
   758
		| Type ("bool", [])     => 2
webertj@14350
   759
		| Type ("Product_Type.unit", []) => 1
webertj@14350
   760
		| Type ("+", [T1,T2])   => (size_of_type T1 us thy cdepth) + (size_of_type T2 us thy cdepth)
webertj@14350
   761
		| Type ("*", [T1,T2])   => (size_of_type T1 us thy cdepth) * (size_of_type T2 us thy cdepth)
webertj@14350
   762
		| Type ("fun", [T1,T2]) => power (size_of_type T2 us thy cdepth, size_of_type T1 us thy cdepth)
webertj@14350
   763
		| Type ("set", [T1])    => size_of_type (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
webertj@14350
   764
		| Type (s, Ts)          =>
webertj@14350
   765
			(case DatatypePackage.datatype_info thy s of
webertj@14350
   766
			  Some info => (* inductive datatype *)
webertj@14350
   767
				if cdepth>0 then
webertj@14350
   768
					let
webertj@14350
   769
						val index               = #index info
webertj@14350
   770
						val descr               = #descr info
webertj@14350
   771
						val (_, dtyps, constrs) = the (assoc (descr, index))
webertj@14350
   772
						val Typs                = dtyps ~~ Ts
webertj@14350
   773
						(* DatatypeAux.dtyp -> Term.typ *)
webertj@14350
   774
						fun typ_of_dtyp (DatatypeAux.DtTFree a) =
webertj@14350
   775
							the (assoc (Typs, DatatypeAux.DtTFree a))
webertj@14350
   776
						  | typ_of_dtyp (DatatypeAux.DtRec i) =
webertj@14350
   777
							let
webertj@14350
   778
								val (s, ds, _) = the (assoc (descr, i))
webertj@14350
   779
							in
webertj@14350
   780
								Type (s, map typ_of_dtyp ds)
webertj@14350
   781
							end
webertj@14350
   782
						  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
webertj@14350
   783
							Type (s, map typ_of_dtyp ds)
webertj@14350
   784
					in
webertj@14350
   785
						sum (map (fn (_,ds) => product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)) constrs)
webertj@14350
   786
					end
webertj@14350
   787
				else 0
webertj@14350
   788
			| None      => error ("size_of_type: type contains an unknown type constructor: '" ^ s ^ "'"))
webertj@14350
   789
		| TFree _               => lookup_size T us
webertj@14350
   790
		| TVar _                => lookup_size T us
webertj@14350
   791
	end;
webertj@14350
   792
webertj@14350
   793
(* ------------------------------------------------------------------------- *)
webertj@14350
   794
(* type_to_prop_tree: creates a tree of boolean variables that denotes an    *)
webertj@14350
   795
(*      element of the type 'T'.  The height and branching factor of the     *)
webertj@14350
   796
(*      tree depend on the size and "structure" of 'T'.                      *)
webertj@14350
   797
(* 'us' : a "universe" specifying the number of elements for each basic type *)
webertj@14350
   798
(*        (i.e. each type variable) in 'T'                                   *)
webertj@14350
   799
(* 'cdepth': maximum constructor depth to be used for inductive datatypes    *)
webertj@14350
   800
(* 'idx': the next index to be used for a boolean variable                   *)
webertj@14350
   801
(* ------------------------------------------------------------------------- *)
webertj@14350
   802
webertj@14350
   803
	(* Term.typ -> (Term.typ * int) list -> theory -> int -> int -> prop_tree * int *)
webertj@14350
   804
webertj@14350
   805
	fun type_to_prop_tree T us thy cdepth idx =
webertj@14350
   806
	let
webertj@14350
   807
		(* int -> Term.typ -> int -> prop_tree list * int *)
webertj@14350
   808
		fun type_to_prop_tree_list 1 T' idx' =
webertj@14350
   809
			let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
webertj@14350
   810
				([tr], newidx)
webertj@14350
   811
			end
webertj@14350
   812
		  | type_to_prop_tree_list n T' idx' =
webertj@14350
   813
			let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
webertj@14350
   814
				let val (trees, lastidx) = type_to_prop_tree_list (n-1) T' newidx in
webertj@14350
   815
					(tr::trees, lastidx)
webertj@14350
   816
				end
webertj@14350
   817
			end
webertj@14350
   818
	in
webertj@14350
   819
		case T of
webertj@14350
   820
		  Type ("prop", []) =>
webertj@14350
   821
			(Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
webertj@14350
   822
		| Type ("bool", []) =>
webertj@14350
   823
			(Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
webertj@14350
   824
		| Type ("Product_Type.unit", []) =>
webertj@14350
   825
			(Leaf [True], idx)
webertj@14350
   826
		| Type ("+", [T1,T2]) =>
webertj@14350
   827
			let
webertj@14350
   828
				val s1 = size_of_type T1 us thy cdepth
webertj@14350
   829
				val s2 = size_of_type T2 us thy cdepth
webertj@14350
   830
				val s  = s1 + s2
webertj@14350
   831
			in
webertj@14350
   832
				if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
webertj@14350
   833
					raise EMPTY_DATATYPE
webertj@14350
   834
				else
webertj@14350
   835
					error "sum types (+) not implemented yet (TODO)"
webertj@14350
   836
			end
webertj@14350
   837
		| Type ("*", [T1,T2]) =>
webertj@14350
   838
			let
webertj@14350
   839
				val s1 = size_of_type T1 us thy cdepth
webertj@14350
   840
				val s2 = size_of_type T2 us thy cdepth
webertj@14350
   841
				val s  = s1 * s2
webertj@14350
   842
			in
webertj@14350
   843
				if s1=0 orelse s2=0 then
webertj@14350
   844
					raise EMPTY_DATATYPE
webertj@14350
   845
				else
webertj@14350
   846
					error "product types (*) not implemented yet (TODO)"
webertj@14350
   847
			end
webertj@14350
   848
		| Type ("fun", [T1,T2]) =>
webertj@14350
   849
			(* we create 'size_of_type T1' different copies of the tree for 'T2', *)
webertj@14350
   850
			(* which are then combined into a single new tree                     *)
webertj@14350
   851
			let
webertj@14350
   852
				val s = size_of_type T1 us thy cdepth
webertj@14350
   853
			in
webertj@14350
   854
				if s=0 then
webertj@14350
   855
					raise EMPTY_DATATYPE
webertj@14350
   856
				else
webertj@14350
   857
					let val (trees, newidx) = type_to_prop_tree_list s T2 idx in
webertj@14350
   858
						(Node trees, newidx)
webertj@14350
   859
					end
webertj@14350
   860
			end
webertj@14350
   861
		| Type ("set", [T1]) =>
webertj@14350
   862
			type_to_prop_tree (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth idx
webertj@14350
   863
		| Type (s, _) =>
webertj@14350
   864
			(case DatatypePackage.constrs_of thy s of
webertj@14350
   865
			   Some _ => (* inductive datatype *)
webertj@14350
   866
					let
webertj@14350
   867
						val s = size_of_type T us thy cdepth
webertj@14350
   868
					in
webertj@14350
   869
						if s=0 then
webertj@14350
   870
							raise EMPTY_DATATYPE
webertj@14350
   871
						else
webertj@14350
   872
							(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
webertj@14350
   873
					end
webertj@14350
   874
			 | None   => error ("type_to_prop_tree: type contains an unknown type constructor: '" ^ s ^ "'"))
webertj@14350
   875
		| TFree _ =>
webertj@14350
   876
			let val s = size_of_type T us thy cdepth in
webertj@14350
   877
				(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
webertj@14350
   878
			end
webertj@14350
   879
		| TVar _  =>
webertj@14350
   880
			let val s = size_of_type T us thy cdepth in
webertj@14350
   881
				(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
webertj@14350
   882
			end
webertj@14350
   883
	end;
webertj@14350
   884
webertj@14350
   885
(* ------------------------------------------------------------------------- *)
webertj@14350
   886
(* type_to_constants: creates a list of prop_trees with constants (True,     *)
webertj@14350
   887
(*      False) rather than boolean variables, one for every element in the   *)
webertj@14350
   888
(*      type 'T'; c.f. type_to_prop_tree                                     *)
webertj@14350
   889
(* ------------------------------------------------------------------------- *)
webertj@14350
   890
webertj@14350
   891
	(* Term.typ -> (Term.typ * int) list -> theory -> int -> prop_tree list *)
webertj@14350
   892
webertj@14350
   893
	fun type_to_constants T us thy cdepth =
webertj@14350
   894
	let
webertj@14350
   895
		(* returns a list with all unit vectors of length n *)
webertj@14350
   896
		(* int -> prop_tree list *)
webertj@14350
   897
		fun unit_vectors n =
webertj@14350
   898
		let
webertj@14350
   899
			(* returns the k-th unit vector of length n *)
webertj@14350
   900
			(* int * int -> prop_tree *)
webertj@14350
   901
			fun unit_vector (k,n) =
webertj@14350
   902
				Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
webertj@14350
   903
			(* int -> prop_tree list -> prop_tree list *)
webertj@14350
   904
			fun unit_vectors_acc k vs =
webertj@14350
   905
				if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
webertj@14350
   906
		in
webertj@14350
   907
			unit_vectors_acc 1 []
webertj@14350
   908
		end
webertj@14350
   909
		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
webertj@14350
   910
		(* 'a -> 'a list list -> 'a list list *)
webertj@14350
   911
		fun cons_list x xss =
webertj@14350
   912
			map (fn xs => x::xs) xss
webertj@14350
   913
		(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
webertj@14350
   914
		(* int -> 'a list -> 'a list list *)
webertj@14350
   915
		fun pick_all 1 xs =
webertj@14350
   916
			map (fn x => [x]) xs
webertj@14350
   917
		  | pick_all n xs =
webertj@14350
   918
			let val rec_pick = pick_all (n-1) xs in
webertj@14350
   919
				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
webertj@14350
   920
			end
webertj@14350
   921
	in
webertj@14350
   922
		case T of
webertj@14350
   923
		  Type ("prop", [])     => unit_vectors 2
webertj@14350
   924
		| Type ("bool", [])     => unit_vectors 2
webertj@14350
   925
		| Type ("Product_Type.unit", []) => unit_vectors 1
webertj@14350
   926
                | Type ("+", [T1,T2])   =>
webertj@14350
   927
			let
webertj@14350
   928
				val s1 = size_of_type T1 us thy cdepth
webertj@14350
   929
				val s2 = size_of_type T2 us thy cdepth
webertj@14350
   930
			in
webertj@14350
   931
				if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
webertj@14350
   932
					raise EMPTY_DATATYPE
webertj@14350
   933
				else
webertj@14350
   934
					error "sum types (+) not implemented yet (TODO)"
webertj@14350
   935
			end
webertj@14350
   936
                | Type ("*", [T1,T2])   =>
webertj@14350
   937
			let
webertj@14350
   938
				val s1 = size_of_type T1 us thy cdepth
webertj@14350
   939
				val s2 = size_of_type T2 us thy cdepth
webertj@14350
   940
			in
webertj@14350
   941
				if s1=0 orelse s2=0 then
webertj@14350
   942
					raise EMPTY_DATATYPE
webertj@14350
   943
				else
webertj@14350
   944
					error "product types (*) not implemented yet (TODO)"
webertj@14350
   945
			end
webertj@14350
   946
		| Type ("fun", [T1,T2]) =>
webertj@14350
   947
			let
webertj@14350
   948
				val s = size_of_type T1 us thy cdepth
webertj@14350
   949
			in
webertj@14350
   950
				if s=0 then
webertj@14350
   951
					raise EMPTY_DATATYPE
webertj@14350
   952
				else
webertj@14350
   953
					map (fn xs => Node xs) (pick_all s (type_to_constants T2 us thy cdepth))
webertj@14350
   954
			end
webertj@14350
   955
		| Type ("set", [T1])    => type_to_constants (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
webertj@14350
   956
		| Type (s, _)           =>
webertj@14350
   957
			(case DatatypePackage.constrs_of thy s of
webertj@14350
   958
			   Some _ => (* inductive datatype *)
webertj@14350
   959
					let
webertj@14350
   960
						val s = size_of_type T us thy cdepth
webertj@14350
   961
					in
webertj@14350
   962
						if s=0 then
webertj@14350
   963
							raise EMPTY_DATATYPE
webertj@14350
   964
						else
webertj@14350
   965
							unit_vectors s
webertj@14350
   966
					end
webertj@14350
   967
			 | None   => error ("type_to_constants: type contains an unknown type constructor: '" ^ s ^ "'"))
webertj@14350
   968
		| TFree _               => unit_vectors (size_of_type T us thy cdepth)
webertj@14350
   969
		| TVar _                => unit_vectors (size_of_type T us thy cdepth)
webertj@14350
   970
	end;
webertj@14350
   971
webertj@14350
   972
(* ------------------------------------------------------------------------- *)
webertj@14350
   973
(* prop_tree_equal: returns a propositional formula that is true iff 'tr1'   *)
webertj@14350
   974
(*      and 'tr2' both denote the same element                               *)
webertj@14350
   975
(* ------------------------------------------------------------------------- *)
webertj@14350
   976
webertj@14350
   977
	(* prop_tree * prop_tree -> prop_formula *)
webertj@14350
   978
webertj@14350
   979
	fun prop_tree_equal (tr1,tr2) =
webertj@14350
   980
		case tr1 of
webertj@14350
   981
		  Leaf x =>
webertj@14350
   982
			(case tr2 of
webertj@14350
   983
			  Leaf y => prop_formula_dot_product (x,y)
webertj@14350
   984
			| _      => raise REFUTE ("prop_tree_equal", "second tree is higher"))
webertj@14350
   985
		| Node xs =>
webertj@14350
   986
			(case tr2 of
webertj@14350
   987
			  Leaf _  => raise REFUTE ("prop_tree_equal", "first tree is higher")
webertj@14350
   988
			(* extensionality: two functions are equal iff they are equal for every element *)
webertj@14350
   989
			| Node ys => list_conjunction (map prop_tree_equal (xs ~~ ys)));
webertj@14350
   990
webertj@14350
   991
(* ------------------------------------------------------------------------- *)
webertj@14350
   992
(* prop_tree_apply: returns a tree that denotes the element obtained by      *)
webertj@14350
   993
(*      applying the function which is denoted by the tree 't1' to the       *)
webertj@14350
   994
(*      element which is denoted by the tree 't2'                            *)
webertj@14350
   995
(* ------------------------------------------------------------------------- *)
webertj@14350
   996
webertj@14350
   997
	(* prop_tree * prop_tree -> prop_tree *)
webertj@14350
   998
webertj@14350
   999
	fun prop_tree_apply (tr1,tr2) =
webertj@14350
  1000
	let
webertj@14350
  1001
		(* prop_tree * prop_tree -> prop_tree *)
webertj@14350
  1002
		fun prop_tree_disjunction (tr1,tr2) =
webertj@14350
  1003
			tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
webertj@14350
  1004
		(* prop_formula * prop_tree -> prop_tree *)
webertj@14350
  1005
		fun prop_formula_times_prop_tree (fm,tr) =
webertj@14350
  1006
			tree_map (map (fn x => SAnd (fm,x))) tr
webertj@14350
  1007
		(* prop_formula list * prop_tree list -> prop_tree *)
webertj@14350
  1008
		fun prop_formula_list_dot_product_prop_tree_list ([fm],[tr]) =
webertj@14350
  1009
			prop_formula_times_prop_tree (fm,tr)
webertj@14350
  1010
		  | prop_formula_list_dot_product_prop_tree_list (fm::fms,tr::trees) =
webertj@14350
  1011
			prop_tree_disjunction (prop_formula_times_prop_tree (fm,tr), prop_formula_list_dot_product_prop_tree_list (fms,trees))
webertj@14350
  1012
		  | prop_formula_list_dot_product_prop_tree_list (_,_) =
webertj@14350
  1013
			raise REFUTE ("prop_tree_apply::prop_formula_list_dot_product_prop_tree_list", "empty list")
webertj@14350
  1014
		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
webertj@14350
  1015
		(* 'a -> 'a list list -> 'a list list *)
webertj@14350
  1016
		fun cons_list x xss =
webertj@14350
  1017
			map (fn xs => x::xs) xss
webertj@14350
  1018
		(* returns a list of lists, each one consisting of one element from each element of 'xss' *)
webertj@14350
  1019
		(* 'a list list -> 'a list list *)
webertj@14350
  1020
		fun pick_all [xs] =
webertj@14350
  1021
			map (fn x => [x]) xs
webertj@14350
  1022
		  | pick_all (xs::xss) =
webertj@14350
  1023
			let val rec_pick = pick_all xss in
webertj@14350
  1024
				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
webertj@14350
  1025
			end
webertj@14350
  1026
		  | pick_all _ =
webertj@14350
  1027
			raise REFUTE ("prop_tree_apply::pick_all", "empty list")
webertj@14350
  1028
		(* prop_tree -> prop_formula list *)
webertj@14350
  1029
		fun prop_tree_to_prop_formula_list (Leaf xs) =
webertj@14350
  1030
			xs
webertj@14350
  1031
		  | prop_tree_to_prop_formula_list (Node trees) =
webertj@14350
  1032
			map list_conjunction (pick_all (map prop_tree_to_prop_formula_list trees))
webertj@14350
  1033
	in
webertj@14350
  1034
		case tr1 of
webertj@14350
  1035
		  Leaf _ =>
webertj@14350
  1036
			raise REFUTE ("prop_tree_apply", "first tree is a leaf")
webertj@14350
  1037
		| Node xs =>
webertj@14350
  1038
			prop_formula_list_dot_product_prop_tree_list (prop_tree_to_prop_formula_list tr2, xs)
webertj@14350
  1039
	end
webertj@14350
  1040
webertj@14350
  1041
(* ------------------------------------------------------------------------- *)
webertj@14350
  1042
(* term_to_prop_tree: translates a HOL term 't' into a tree of propositional *)
webertj@14350
  1043
(*      formulas; 'us' specifies the number of elements for each type        *)
webertj@14350
  1044
(*      variable in 't'; 'cdepth' specifies the maximal constructor depth    *)
webertj@14350
  1045
(*      for inductive datatypes.  Also returns the lowest index that was not *)
webertj@14350
  1046
(*      used for a boolean variable, and a substitution of terms (free/      *)
webertj@14350
  1047
(*      schematic variables) by prop_trees.                                  *)
webertj@14350
  1048
(* ------------------------------------------------------------------------- *)
webertj@14350
  1049
webertj@14350
  1050
	(* Term.term -> (Term.typ * int) list -> theory -> int -> prop_tree * (int * (Term.term * prop_tree) list) *)
webertj@14350
  1051
webertj@14350
  1052
	fun term_to_prop_tree t us thy cdepth =
webertj@14350
  1053
	let
webertj@14350
  1054
		(* Term.term -> int * (Term.term * prop_tree) list -> prop_tree * (int * (Term.term * prop_tree) list) *)
webertj@14350
  1055
		fun variable_to_prop_tree_subst t' (idx,subs) =
webertj@14350
  1056
			case assoc (subs,t') of
webertj@14350
  1057
			  Some tr =>
webertj@14350
  1058
				(* return the previously associated tree; the substitution remains unchanged *)
webertj@14350
  1059
				(tr, (idx,subs))
webertj@14350
  1060
			| None =>
webertj@14350
  1061
				(* generate a new tree; update the index; extend the substitution *)
webertj@14350
  1062
				let
webertj@14350
  1063
					val T = case t' of
webertj@14350
  1064
						  Free (_,T) => T
webertj@14350
  1065
						| Var (_,T)  => T
webertj@14350
  1066
						| _          => raise REFUTE ("variable_to_prop_tree_subst", "term is not a (free or schematic) variable")
webertj@14350
  1067
					val (tr,newidx) = type_to_prop_tree T us thy cdepth idx
webertj@14350
  1068
				in
webertj@14350
  1069
					(tr, (newidx, (t',tr)::subs))
webertj@14350
  1070
				end
webertj@14350
  1071
		(* Term.term -> int * (Term.term * prop_tree) list -> prop_tree list -> prop_tree * (int * (Term.term * prop_tree) list) *)
webertj@14350
  1072
		fun term_to_prop_tree_subst t' (idx,subs) bsubs =
webertj@14350
  1073
			case t' of
webertj@14350
  1074
			(* meta-logical constants *)
webertj@14350
  1075
			  Const ("Goal", _) $ t1 =>
webertj@14350
  1076
				term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1077
			| Const ("all", _) $ t1 =>
webertj@14350
  1078
				let
webertj@14350
  1079
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1080
				in
webertj@14350
  1081
					case tree1 of
webertj@14350
  1082
					  Node xs =>
webertj@14350
  1083
						let
webertj@14350
  1084
							val fmTrue  = list_conjunction (map prop_tree_to_true xs)
webertj@14350
  1085
							val fmFalse = list_disjunction (map prop_tree_to_false xs)
webertj@14350
  1086
						in
webertj@14350
  1087
							(Leaf [fmTrue, fmFalse], (i1,s1))
webertj@14350
  1088
						end
webertj@14350
  1089
					| _ =>
webertj@14350
  1090
						raise REFUTE ("term_to_prop_tree_subst", "'all' is not followed by a function")
webertj@14350
  1091
				end
webertj@14350
  1092
			| Const ("==", _) $ t1 $ t2 =>
webertj@14350
  1093
				let
webertj@14350
  1094
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1095
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
webertj@14350
  1096
					val fmTrue          = prop_tree_equal (tree1,tree2)
webertj@14350
  1097
					val fmFalse         = SNot fmTrue
webertj@14350
  1098
				in
webertj@14350
  1099
					(Leaf [fmTrue, fmFalse], (i2,s2))
webertj@14350
  1100
				end
webertj@14350
  1101
			| Const ("==>", _) $ t1 $ t2 =>
webertj@14350
  1102
				let
webertj@14350
  1103
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1104
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
webertj@14350
  1105
					val fmTrue          = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
webertj@14350
  1106
					val fmFalse         = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
webertj@14350
  1107
				in
webertj@14350
  1108
					(Leaf [fmTrue, fmFalse], (i2,s2))
webertj@14350
  1109
				end
webertj@14350
  1110
			(* HOL constants *)
webertj@14350
  1111
			| Const ("Trueprop", _) $ t1 =>
webertj@14350
  1112
				term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1113
			| Const ("Not", _) $ t1 =>
webertj@14350
  1114
				let
webertj@14350
  1115
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1116
					val fmTrue          = prop_tree_to_false tree1
webertj@14350
  1117
					val fmFalse         = prop_tree_to_true tree1
webertj@14350
  1118
				in
webertj@14350
  1119
					(Leaf [fmTrue, fmFalse], (i1,s1))
webertj@14350
  1120
				end
webertj@14350
  1121
			| Const ("True", _) =>
webertj@14350
  1122
				(Leaf [True, False], (idx,subs))
webertj@14350
  1123
			| Const ("False", _) =>
webertj@14350
  1124
				(Leaf [False, True], (idx,subs))
webertj@14350
  1125
			| Const ("All", _) $ t1 =>
webertj@14350
  1126
				let
webertj@14350
  1127
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1128
				in
webertj@14350
  1129
					case tree1 of
webertj@14350
  1130
					  Node xs =>
webertj@14350
  1131
						let
webertj@14350
  1132
							val fmTrue  = list_conjunction (map prop_tree_to_true xs)
webertj@14350
  1133
							val fmFalse = list_disjunction (map prop_tree_to_false xs)
webertj@14350
  1134
						in
webertj@14350
  1135
							(Leaf [fmTrue, fmFalse], (i1,s1))
webertj@14350
  1136
						end
webertj@14350
  1137
					| _ =>
webertj@14350
  1138
						raise REFUTE ("term_to_prop_tree_subst", "'All' is not followed by a function")
webertj@14350
  1139
				end
webertj@14350
  1140
			| Const ("Ex", _) $ t1 =>
webertj@14350
  1141
				let
webertj@14350
  1142
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1143
				in
webertj@14350
  1144
					case tree1 of
webertj@14350
  1145
					  Node xs =>
webertj@14350
  1146
						let
webertj@14350
  1147
							val fmTrue  = list_disjunction (map prop_tree_to_true xs)
webertj@14350
  1148
							val fmFalse = list_conjunction (map prop_tree_to_false xs)
webertj@14350
  1149
						in
webertj@14350
  1150
							(Leaf [fmTrue, fmFalse], (i1,s1))
webertj@14350
  1151
						end
webertj@14350
  1152
					| _ =>
webertj@14350
  1153
						raise REFUTE ("term_to_prop_tree_subst", "'Ex' is not followed by a function")
webertj@14350
  1154
				end
webertj@14350
  1155
			| Const ("Ex1", Type ("fun", [Type ("fun", [T, Type ("bool",[])]), Type ("bool",[])])) $ t1 =>
webertj@14350
  1156
				(* 'Ex1 t1' is equivalent to 'Ex Abs(x,T,t1' x & All Abs(y,T,t1'' y --> x=y))' *)
webertj@14350
  1157
				let
webertj@14350
  1158
					val t1'      = Term.incr_bv (1, 0, t1)
webertj@14350
  1159
					val t1''     = Term.incr_bv (2, 0, t1)
webertj@14350
  1160
					val t_equal  = (HOLogic.eq_const T) $ (Bound 1) $ (Bound 0)
webertj@14350
  1161
					val t_unique = (HOLogic.all_const T) $ Abs("y",T,HOLogic.mk_imp (t1'' $ (Bound 0),t_equal))
webertj@14350
  1162
					val t_ex1    = (HOLogic.exists_const T) $ Abs("x",T,HOLogic.mk_conj (t1' $ (Bound 0),t_unique))
webertj@14350
  1163
				in
webertj@14350
  1164
					term_to_prop_tree_subst t_ex1 (idx,subs) bsubs
webertj@14350
  1165
				end
webertj@14350
  1166
			| Const ("op =", _) $ t1 $ t2 =>
webertj@14350
  1167
				let
webertj@14350
  1168
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1169
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
webertj@14350
  1170
					val fmTrue          = prop_tree_equal (tree1,tree2)
webertj@14350
  1171
					val fmFalse         = SNot fmTrue
webertj@14350
  1172
				in
webertj@14350
  1173
					(Leaf [fmTrue, fmFalse], (i2,s2))
webertj@14350
  1174
				end
webertj@14350
  1175
			| Const ("op &", _) $ t1 $ t2 =>
webertj@14350
  1176
				let
webertj@14350
  1177
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1178
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
webertj@14350
  1179
					val fmTrue          = SAnd (prop_tree_to_true tree1, prop_tree_to_true tree2)
webertj@14350
  1180
					val fmFalse         = SOr (prop_tree_to_false tree1, prop_tree_to_false tree2)
webertj@14350
  1181
				in
webertj@14350
  1182
					(Leaf [fmTrue, fmFalse], (i2,s2))
webertj@14350
  1183
				end
webertj@14350
  1184
			| Const ("op |", _) $ t1 $ t2 =>
webertj@14350
  1185
				let
webertj@14350
  1186
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1187
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
webertj@14350
  1188
					val fmTrue          = SOr (prop_tree_to_true tree1, prop_tree_to_true tree2)
webertj@14350
  1189
					val fmFalse         = SAnd (prop_tree_to_false tree1, prop_tree_to_false tree2)
webertj@14350
  1190
				in
webertj@14350
  1191
					(Leaf [fmTrue, fmFalse], (i2,s2))
webertj@14350
  1192
				end
webertj@14350
  1193
			| Const ("op -->", _) $ t1 $ t2 =>
webertj@14350
  1194
				let
webertj@14350
  1195
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1196
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
webertj@14350
  1197
					val fmTrue          = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
webertj@14350
  1198
					val fmFalse         = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
webertj@14350
  1199
				in
webertj@14350
  1200
					(Leaf [fmTrue, fmFalse], (i2,s2))
webertj@14350
  1201
				end
webertj@14350
  1202
			(* set constants *)
webertj@14350
  1203
			| Const ("Collect", _) $ t1 =>
webertj@14350
  1204
				term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1205
			| Const ("op :", _) $ t1 $ t2 =>
webertj@14350
  1206
				term_to_prop_tree_subst (t2 $ t1) (idx,subs) bsubs
webertj@14350
  1207
			(* datatype constants *)
webertj@14350
  1208
			| Const ("Product_Type.Unity", _) =>
webertj@14350
  1209
				(Leaf [True], (idx,subs))
webertj@14350
  1210
			(* unknown constants *)
webertj@14350
  1211
			| Const (c, _) =>
webertj@14350
  1212
				error ("term contains an unknown constant: '" ^ c ^ "'")
webertj@14350
  1213
			(* abstractions *)
webertj@14350
  1214
			| Abs (_,T,body) =>
webertj@14350
  1215
				let
webertj@14350
  1216
					val constants       = type_to_constants T us thy cdepth
webertj@14350
  1217
					val (trees, substs) = split_list (map (fn c => term_to_prop_tree_subst body (idx,subs) (c::bsubs)) constants)
webertj@14350
  1218
				in
webertj@14350
  1219
					(* the substitutions in 'substs' are all identical *)
webertj@14350
  1220
					(Node trees, hd substs)
webertj@14350
  1221
				end
webertj@14350
  1222
			(* (free/schematic) variables *)
webertj@14350
  1223
			| Free _ =>
webertj@14350
  1224
				variable_to_prop_tree_subst t' (idx,subs)
webertj@14350
  1225
			| Var _ =>
webertj@14350
  1226
				variable_to_prop_tree_subst t' (idx,subs)
webertj@14350
  1227
			(* bound variables *)
webertj@14350
  1228
			| Bound i =>
webertj@14350
  1229
				if (length bsubs) <= i then
webertj@14350
  1230
					raise REFUTE ("term_to_prop_tree_subst", "term contains a loose bound variable (with index " ^ (string_of_int i) ^ ")")
webertj@14350
  1231
				else
webertj@14350
  1232
					(nth_elem (i,bsubs), (idx,subs))
webertj@14350
  1233
			(* application *)
webertj@14350
  1234
			| t1 $ t2 =>
webertj@14350
  1235
				let
webertj@14350
  1236
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
webertj@14350
  1237
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
webertj@14350
  1238
				in
webertj@14350
  1239
					(prop_tree_apply (tree1,tree2), (i2,s2))
webertj@14350
  1240
				end
webertj@14350
  1241
	in
webertj@14350
  1242
		term_to_prop_tree_subst t (1,[]) []
webertj@14350
  1243
	end;
webertj@14350
  1244
webertj@14350
  1245
(* ------------------------------------------------------------------------- *)
webertj@14350
  1246
(* term_to_prop_formula: translates a HOL formula 't' into a propositional   *)
webertj@14350
  1247
(*      formula that is satisfiable if and only if 't' has a model of "size" *)
webertj@14350
  1248
(*      'us' (where 'us' specifies the number of elements for each free type *)
webertj@14350
  1249
(*      variable in 't') and maximal constructor depth 'cdepth'.             *)
webertj@14350
  1250
(* ------------------------------------------------------------------------- *)
webertj@14350
  1251
webertj@14350
  1252
	(* TODO: shouldn't 'us' also specify the number of elements for schematic type variables? (if so, modify the comment above) *)
webertj@14350
  1253
webertj@14350
  1254
	(* Term.term -> (Term.typ * int) list -> theory -> int -> prop_formula * (int * (Term.term * prop_tree) list) *)
webertj@14350
  1255
webertj@14350
  1256
	fun term_to_prop_formula t us thy cdepth =
webertj@14350
  1257
	let
webertj@14350
  1258
		val (tr, (idx,subs)) = term_to_prop_tree t us thy cdepth
webertj@14350
  1259
		val fm               = prop_tree_to_true tr
webertj@14350
  1260
	in
webertj@14350
  1261
		if subs=[] then
webertj@14350
  1262
			(fm, (idx,subs))
webertj@14350
  1263
		else
webertj@14350
  1264
			(* make sure every tree that is substituted for a term describes a single element *)
webertj@14350
  1265
			(SAnd (list_conjunction (map (fn (_,tr) => restrict_to_single_element tr) subs), fm), (idx,subs))
webertj@14350
  1266
	end;
webertj@14350
  1267
webertj@14350
  1268
webertj@14350
  1269
(* ------------------------------------------------------------------------- *)
webertj@14350
  1270
(* INTERFACE, PART 2: FINDING A MODEL                                        *)
webertj@14350
  1271
(* ------------------------------------------------------------------------- *)
webertj@14350
  1272
webertj@14350
  1273
(* ------------------------------------------------------------------------- *)
webertj@14350
  1274
(* string_of_universe: prints a universe, i.e. an assignment of sizes for    *)
webertj@14350
  1275
(*                     types                                                 *)
webertj@14350
  1276
(* thy: the current theory                                                   *)
webertj@14350
  1277
(* us : a list containing types together with their size                     *)
webertj@14350
  1278
(* ------------------------------------------------------------------------- *)
webertj@14350
  1279
webertj@14350
  1280
	(* theory -> (Term.typ * int) list -> string *)
webertj@14350
  1281
webertj@14350
  1282
	fun string_of_universe thy [] =
webertj@14350
  1283
		"empty universe (no type variables in term)"
webertj@14350
  1284
	  | string_of_universe thy us =
webertj@14350
  1285
		space_implode ", " (map (fn (T,i) => (Sign.string_of_typ (sign_of thy) T) ^ ": " ^ (string_of_int i)) us);
webertj@14350
  1286
webertj@14350
  1287
(* ------------------------------------------------------------------------- *)
webertj@14350
  1288
(* string_of_model: prints a model, given by a substitution 'subs' of trees  *)
webertj@14350
  1289
(*      of propositional variables and an assignment 'ass' of truth values   *)
webertj@14350
  1290
(*      for these variables.                                                 *)
webertj@14350
  1291
(* thy   : the current theory                                                *)
webertj@14350
  1292
(* us    : universe, specifies the "size" of each type (i.e. type variable)  *)
webertj@14350
  1293
(* cdepth: maximal constructor depth for inductive datatypes                 *)
webertj@14350
  1294
(* subs  : substitution of trees of propositional formulas (for variables)   *)
webertj@14350
  1295
(* ass   : assignment of truth values for boolean variables; see function    *)
webertj@14350
  1296
(*         'truth_value' below for its meaning                               *)
webertj@14350
  1297
(* ------------------------------------------------------------------------- *)
webertj@14350
  1298
webertj@14350
  1299
	(* theory -> (Term.typ * int) list -> int -> (Term.term * prop_formula tree) list -> int list -> string *)
webertj@14350
  1300
webertj@14350
  1301
	fun string_of_model thy us cdepth [] ass =
webertj@14350
  1302
		"empty interpretation (no free variables in term)"
webertj@14350
  1303
	  | string_of_model thy us cdepth subs ass =
webertj@14350
  1304
		let
webertj@14350
  1305
			(* Sign.sg *)
webertj@14350
  1306
			val sg = sign_of thy
webertj@14350
  1307
			(* int -> bool *)
webertj@14350
  1308
			fun truth_value i =
webertj@14350
  1309
				if i mem ass then true
webertj@14350
  1310
				else if ~i mem ass then false
webertj@14350
  1311
				else error ("SAT solver assignment does not specify a value for variable " ^ (string_of_int i))
webertj@14350
  1312
			(* string -> string *)
webertj@14350
  1313
			fun strip_leading_quote str =
webertj@14350
  1314
				if nth_elem_string(0,str)="'" then
webertj@14350
  1315
					String.substring (str, 1, size str - 1)
webertj@14350
  1316
				else
webertj@14350
  1317
					str;
webertj@14350
  1318
			(* prop_formula list -> int *)
webertj@14350
  1319
			fun true_index xs =
webertj@14350
  1320
				(* returns the (0-based) index of the first true formula in xs *)
webertj@14350
  1321
				let fun true_index_acc [] _ =
webertj@14350
  1322
					raise REFUTE ("string_of_model::true_index", "no variable was set to true")
webertj@14350
  1323
				      | true_index_acc (x::xs) n =
webertj@14350
  1324
					case x of
webertj@14350
  1325
					  BoolVar i =>
webertj@14350
  1326
						if truth_value i then n else true_index_acc xs (n+1)
webertj@14350
  1327
					| True =>
webertj@14350
  1328
						n
webertj@14350
  1329
					| False =>
webertj@14350
  1330
						true_index_acc xs (n+1)
webertj@14350
  1331
					| _ =>
webertj@14350
  1332
						raise REFUTE ("string_of_model::true_index", "formula is not a boolean variable/true/false")
webertj@14350
  1333
				in
webertj@14350
  1334
					true_index_acc xs 0
webertj@14350
  1335
				end
webertj@14350
  1336
			(* Term.typ -> int -> prop_tree -> string *)
webertj@14350
  1337
			(* prop *)
webertj@14350
  1338
			fun string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
webertj@14350
  1339
				if truth_value i then "true" else "false"
webertj@14350
  1340
			  | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [True, False]) =
webertj@14350
  1341
				"true"
webertj@14350
  1342
			  | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [False, True]) =
webertj@14350
  1343
				"false"
webertj@14350
  1344
			(* bool *)
webertj@14350
  1345
			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
webertj@14350
  1346
				if truth_value i then "true" else "false"
webertj@14350
  1347
			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [True, False]) =
webertj@14350
  1348
				"true"
webertj@14350
  1349
			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [False, True]) =
webertj@14350
  1350
				"false"
webertj@14350
  1351
			(* unit *)
webertj@14350
  1352
			  | string_of_prop_tree (Type ("Product_Type.unit",[])) cdepth (Leaf [True]) =
webertj@14350
  1353
				"()"
webertj@14350
  1354
			  | string_of_prop_tree (Type (s,Ts)) cdepth (Leaf xs) =
webertj@14350
  1355
				(case DatatypePackage.datatype_info thy s of
webertj@14350
  1356
				   Some info => (* inductive datatype *)
webertj@14350
  1357
					let
webertj@14350
  1358
						val index               = #index info
webertj@14350
  1359
						val descr               = #descr info
webertj@14350
  1360
						val (_, dtyps, constrs) = the (assoc (descr, index))
webertj@14350
  1361
						val Typs                = dtyps ~~ Ts
webertj@14350
  1362
						(* string -> string *)
webertj@14350
  1363
						fun unqualify s =
webertj@14350
  1364
							implode (snd (take_suffix (fn c => c <> ".") (explode s)))
webertj@14350
  1365
						(* DatatypeAux.dtyp -> Term.typ *)
webertj@14350
  1366
						fun typ_of_dtyp (DatatypeAux.DtTFree a) =
webertj@14350
  1367
							the (assoc (Typs, DatatypeAux.DtTFree a))
webertj@14350
  1368
						  | typ_of_dtyp (DatatypeAux.DtRec i) =
webertj@14350
  1369
							let
webertj@14350
  1370
								val (s, ds, _) = the (assoc (descr, i))
webertj@14350
  1371
							in
webertj@14350
  1372
								Type (s, map typ_of_dtyp ds)
webertj@14350
  1373
							end
webertj@14350
  1374
						  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
webertj@14350
  1375
							Type (s, map typ_of_dtyp ds)
webertj@14350
  1376
						(* DatatypeAux.dtyp list -> int -> string *)
webertj@14350
  1377
						fun string_of_inductive_type_cargs [] n =
webertj@14350
  1378
							if n<>0 then
webertj@14350
  1379
								raise REFUTE ("string_of_model", "internal error computing the element index for an inductive type")
webertj@14350
  1380
							else
webertj@14350
  1381
								""
webertj@14350
  1382
						  | string_of_inductive_type_cargs (d::ds) n =
webertj@14350
  1383
							let
webertj@14350
  1384
								val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
webertj@14350
  1385
							in
webertj@14350
  1386
								" " ^ (string_of_prop_tree (typ_of_dtyp d) (cdepth-1) (nth_elem (n div size_ds, type_to_constants (typ_of_dtyp d) us thy (cdepth-1)))) ^ (string_of_inductive_type_cargs ds (n mod size_ds))
webertj@14350
  1387
							end
webertj@14350
  1388
						(* (string * DatatypeAux.dtyp list) list -> int -> string *)
webertj@14350
  1389
						fun string_of_inductive_type_constrs [] n =
webertj@14350
  1390
							raise REFUTE ("string_of_model", "inductive type has fewer elements than needed")
webertj@14350
  1391
						  | string_of_inductive_type_constrs ((s,ds)::cs) n =
webertj@14350
  1392
							let
webertj@14350
  1393
								val size = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
webertj@14350
  1394
							in
webertj@14350
  1395
								if n < size then
webertj@14350
  1396
									(unqualify s) ^ (string_of_inductive_type_cargs ds n)
webertj@14350
  1397
								else
webertj@14350
  1398
									string_of_inductive_type_constrs cs (n - size)
webertj@14350
  1399
							end
webertj@14350
  1400
					in
webertj@14350
  1401
						string_of_inductive_type_constrs constrs (true_index xs)
webertj@14350
  1402
					end
webertj@14350
  1403
				 | None =>
webertj@14350
  1404
					raise REFUTE ("string_of_model", "type contains an unknown type constructor: '" ^ s ^ "'"))
webertj@14350
  1405
			(* type variable *)
webertj@14350
  1406
			  | string_of_prop_tree (TFree (s,_)) cdepth (Leaf xs) =
webertj@14350
  1407
					(strip_leading_quote s) ^ (string_of_int (true_index xs))
webertj@14350
  1408
			  | string_of_prop_tree (TVar ((s,_),_)) cdepth (Leaf xs) =
webertj@14350
  1409
					(strip_leading_quote s) ^ (string_of_int (true_index xs))
webertj@14350
  1410
			(* function or set type *)
webertj@14350
  1411
			  | string_of_prop_tree T cdepth (Node xs) =
webertj@14350
  1412
				case T of
webertj@14350
  1413
				  Type ("fun", [T1,T2]) =>
webertj@14350
  1414
					let
webertj@14350
  1415
						val strings = foldl (fn (ss,(c,x)) => ss @ [(string_of_prop_tree T1 cdepth c) ^ "\\<mapsto>" ^ (string_of_prop_tree T2 cdepth x)]) ([], (type_to_constants T1 us thy cdepth) ~~ xs)
webertj@14350
  1416
					in
webertj@14350
  1417
						"(" ^ (space_implode ", " strings) ^ ")"
webertj@14350
  1418
					end
webertj@14350
  1419
				| Type ("set", [T1]) =>
webertj@14350
  1420
					let
webertj@14350
  1421
						val strings = foldl (fn (ss,(c,x)) => if (string_of_prop_tree (Type ("bool",[])) cdepth x)="true" then ss @ [string_of_prop_tree T1 cdepth c] else ss) ([], (type_to_constants T1 us thy cdepth) ~~ xs)
webertj@14350
  1422
					in
webertj@14350
  1423
						"{" ^ (space_implode ", " strings) ^ "}"
webertj@14350
  1424
					end
webertj@14350
  1425
				| _ => raise REFUTE ("string_of_model::string_of_prop_tree", "not a function/set type")
webertj@14350
  1426
			(* Term.term * prop_formula tree -> string *)
webertj@14350
  1427
			fun string_of_term_assignment (t,tr) =
webertj@14350
  1428
			let
webertj@14350
  1429
				val T = case t of
webertj@14350
  1430
					  Free (_,T) => T
webertj@14350
  1431
					| Var (_,T)  => T
webertj@14350
  1432
					| _          => raise REFUTE ("string_of_model::string_of_term_assignment", "term is not a (free or schematic) variable")
webertj@14350
  1433
			in
webertj@14350
  1434
				(Sign.string_of_term sg t) ^ " = " ^ (string_of_prop_tree T cdepth tr)
webertj@14350
  1435
			end
webertj@14350
  1436
		in
webertj@14350
  1437
			space_implode "\n" (map string_of_term_assignment subs)
webertj@14350
  1438
		end;
webertj@14350
  1439
webertj@14350
  1440
(* ------------------------------------------------------------------------- *)
webertj@14350
  1441
(* find_model: repeatedly calls 'prop_formula_sat_solver' with appropriate   *)
webertj@14350
  1442
(*             parameters, and displays the results to the user              *)
webertj@14350
  1443
(* params    : list of '(name, value)' pairs used to override default        *)
webertj@14350
  1444
(*             parameters                                                    *)
webertj@14350
  1445
(*                                                                           *)
webertj@14350
  1446
(* This is a brief description of the algorithm implemented:                 *)
webertj@14350
  1447
(*                                                                           *)
webertj@14350
  1448
(* 1. Let k = max ('minsize',1).                                             *)
webertj@14350
  1449
(* 2. Let the universe have k elements.  Find all possible partitions of     *)
webertj@14350
  1450
(*    these elements into the basic types occuring in 't' such that no basic *)
webertj@14350
  1451
(*    type is empty.                                                         *)
webertj@14350
  1452
(* 3. Translate 't' into a propositional formula p s.t. 't' has a model wrt. *)
webertj@14350
  1453
(*    the partition chosen in step (2.) if (actually, if and only if) p is   *)
webertj@14350
  1454
(*    satisfiable.  To do this, replace quantification by conjunction/       *)
webertj@14350
  1455
(*    disjunction over all elements of the type being quantified over.  (If  *)
webertj@14350
  1456
(*    p contains more than 'maxvars' boolean variables, terminate.)          *)
webertj@14350
  1457
(* 4. Serialize p to a file, and try to find a satisfying assignment for p   *)
webertj@14350
  1458
(*    by invoking an external SAT solver.                                    *)
webertj@14350
  1459
(* 5. If the SAT solver finds a satisfying assignment for p, translate this  *)
webertj@14350
  1460
(*    assignment back into a model for 't'.  Present this model to the user, *)
webertj@14350
  1461
(*    then terminate.                                                        *)
webertj@14350
  1462
(* 6. As long as there is another partition left, pick it and go back to     *)
webertj@14350
  1463
(*    step (3.).                                                             *)
webertj@14350
  1464
(* 7. Increase k by 1.  As long as k does not exceed 'maxsize', go back to   *)
webertj@14350
  1465
(*    step (2.).                                                             *)
webertj@14350
  1466
(*                                                                           *)
webertj@14350
  1467
(* The following parameters are currently supported (and required!):         *)
webertj@14350
  1468
(*                                                                           *)
webertj@14350
  1469
(* Name          Type    Description                                         *)
webertj@14350
  1470
(*                                                                           *)
webertj@14350
  1471
(* "minsize"     int     Only search for models with size at least           *)
webertj@14350
  1472
(*                       'minsize'.                                          *)
webertj@14350
  1473
(* "maxsize"     int     If >0, only search for models with size at most     *)
webertj@14350
  1474
(*                       'maxsize'.                                          *)
webertj@14350
  1475
(* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
webertj@14350
  1476
(*                       when transforming the term into a propositional     *)
webertj@14350
  1477
(*                       formula.                                            *)
webertj@14350
  1478
(* "satfile"     string  Name of the file used to store the propositional    *)
webertj@14350
  1479
(*                       formula, i.e. the input to the SAT solver.          *)
webertj@14350
  1480
(* "satformat"   string  Format of the SAT solver's input file.  Must be     *)
webertj@14350
  1481
(*                       either "cnf", "defcnf", or "sat".  Since "sat" is   *)
webertj@14350
  1482
(*                       not supported by most SAT solvers, and "cnf" can    *)
webertj@14350
  1483
(*                       cause exponential blowup of the formula, "defcnf"   *)
webertj@14350
  1484
(*                       is recommended.                                     *)
webertj@14350
  1485
(* "resultfile"  string  Name of the file containing the SAT solver's        *)
webertj@14350
  1486
(*                       output.                                             *)
webertj@14350
  1487
(* "success"     string  Part of the line in the SAT solver's output that    *)
webertj@14350
  1488
(*                       precedes a list of integers representing the        *)
webertj@14350
  1489
(*                       satisfying assignment.                              *)
webertj@14350
  1490
(* "command"     string  System command used to execute the SAT solver.      *)
webertj@14350
  1491
(*                       Note that you if you change 'satfile' or            *)
webertj@14350
  1492
(*                       'resultfile', you will also need to change          *)
webertj@14350
  1493
(*                       'command'.                                          *)
webertj@14350
  1494
(*                                                                           *)
webertj@14350
  1495
(* See the Isabelle/Isar theory 'Refute.thy' for reasonable default values.  *)
webertj@14350
  1496
(* ------------------------------------------------------------------------- *)
webertj@14350
  1497
webertj@14350
  1498
	(* theory -> (string * string) list -> Term.term -> unit *)
webertj@14350
  1499
webertj@14350
  1500
	fun find_model thy params t =
webertj@14350
  1501
	let
webertj@14350
  1502
		(* (string * string) list * (string * string) list -> (string * string) list *)
webertj@14350
  1503
		fun add_params (parms, []) =
webertj@14350
  1504
			parms
webertj@14350
  1505
		  | add_params (parms, defparm::defparms) =
webertj@14350
  1506
			add_params (gen_ins (fn (a, b) => (fst a) = (fst b)) (defparm, parms), defparms)
webertj@14350
  1507
		(* (string * string) list * string -> int *)
webertj@14350
  1508
		fun read_int (parms, name) =
webertj@14350
  1509
			case assoc_string (parms, name) of
webertj@14350
  1510
			  Some s => (case LargeInt.fromString s of
webertj@14350
  1511
				  SOME i => i
webertj@14350
  1512
				| NONE   => error ("parameter '" ^ name ^ "' (value is '" ^ s ^ "') must be an integer value"))
webertj@14350
  1513
			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")
webertj@14350
  1514
		(* (string * string) list * string -> string *)
webertj@14350
  1515
		fun read_string (parms, name) =
webertj@14350
  1516
			case assoc_string (parms, name) of
webertj@14350
  1517
			  Some s => s
webertj@14350
  1518
			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")
webertj@14350
  1519
		(* (string * string) list *)
webertj@14350
  1520
		val allparams  = add_params (params, get_default_params thy)
webertj@14350
  1521
		(* int *)
webertj@14350
  1522
		val minsize    = read_int (allparams, "minsize")
webertj@14350
  1523
		val maxsize    = read_int (allparams, "maxsize")
webertj@14350
  1524
		val maxvars    = read_int (allparams, "maxvars")
webertj@14350
  1525
		(* string *)
webertj@14350
  1526
		val satfile    = read_string (allparams, "satfile")
webertj@14350
  1527
		val satformat  = read_string (allparams, "satformat")
webertj@14350
  1528
		val resultfile = read_string (allparams, "resultfile")
webertj@14350
  1529
		val success    = read_string (allparams, "success")
webertj@14350
  1530
		val command    = read_string (allparams, "command")
webertj@14350
  1531
		(* misc *)
webertj@14350
  1532
		val satpath    = Path.unpack satfile
webertj@14350
  1533
		val resultpath = Path.unpack resultfile
webertj@14350
  1534
		val sg         = sign_of thy
webertj@14350
  1535
		(* Term.typ list *)
webertj@14350
  1536
		val tvars      = map (fn (i,s) => TVar(i,s)) (term_tvars t)
webertj@14350
  1537
		val tfrees     = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
webertj@14350
  1538
		(* universe -> int -> bool *)
webertj@14350
  1539
		fun find_model_universe u cdepth =
webertj@14350
  1540
			let
webertj@14350
  1541
				(* given the universe 'u' and constructor depth 'cdepth', translate *)
webertj@14350
  1542
        	                (* the term 't' into a propositional formula 'fm'                   *)
webertj@14350
  1543
				val (fm,(idx,subs)) = term_to_prop_formula t u thy cdepth
webertj@14350
  1544
				val usedvars        = idx-1
webertj@14350
  1545
			in
webertj@14350
  1546
				(* 'maxvars=0' means "use as many variables as necessary" *)
webertj@14350
  1547
				if usedvars>maxvars andalso maxvars<>0 then
webertj@14350
  1548
					(
webertj@14350
  1549
						(* too many variables used: terminate *)
webertj@14350
  1550
						writeln ("\nSearch terminated: " ^ (string_of_int usedvars) ^ " boolean variables used (only " ^ (string_of_int maxvars) ^ " allowed).");
webertj@14350
  1551
						true
webertj@14350
  1552
					)
webertj@14350
  1553
				else
webertj@14350
  1554
					(* pass the formula 'fm' to an external SAT solver *)
webertj@14350
  1555
					case prop_formula_sat_solver fm satpath satformat resultpath success command of
webertj@14350
  1556
					  None =>
webertj@14350
  1557
						(* no model found *)
webertj@14350
  1558
						false
webertj@14350
  1559
					| Some assignment =>
webertj@14350
  1560
						(* model found: terminate *)
webertj@14350
  1561
						(
webertj@14350
  1562
							writeln ("\nModel found:\n" ^ (string_of_universe thy u) ^ "\n" ^ (string_of_model thy u cdepth subs assignment));
webertj@14350
  1563
							true
webertj@14350
  1564
						)
webertj@14350
  1565
			end
webertj@14350
  1566
		(* universe list -> int -> bool *)
webertj@14350
  1567
		fun find_model_universes [] cdepth =
webertj@14350
  1568
			(
webertj@14350
  1569
				std_output "\n";
webertj@14350
  1570
				false
webertj@14350
  1571
			)
webertj@14350
  1572
		  | find_model_universes (u::us) cdepth =
webertj@14350
  1573
			(
webertj@14350
  1574
				std_output ".";
webertj@14350
  1575
				((if find_model_universe u cdepth then
webertj@14350
  1576
					(* terminate *)
webertj@14350
  1577
					true
webertj@14350
  1578
				else
webertj@14350
  1579
					(* continue search with the next universe *)
webertj@14350
  1580
					find_model_universes us cdepth)
webertj@14350
  1581
				handle EMPTY_DATATYPE => (std_output "[empty inductive type (constructor depth too small)]\n"; false))
webertj@14350
  1582
			)
webertj@14350
  1583
		(* int * int -> unit *)
webertj@14350
  1584
		fun find_model_from_to (min,max) =
webertj@14350
  1585
			(* 'max=0' means "search for arbitrary large models" *)
webertj@14350
  1586
			if min>max andalso max<>0 then
webertj@14350
  1587
				writeln ("Search terminated: no model found.")
webertj@14350
  1588
			else
webertj@14350
  1589
			(
webertj@14350
  1590
				std_output ("Searching for a model of size " ^ (string_of_int min));
webertj@14350
  1591
				if find_model_universes (make_universes tfrees min) min then
webertj@14350
  1592
					(* terminate *)
webertj@14350
  1593
					()
webertj@14350
  1594
				else
webertj@14350
  1595
					(* continue search with increased size *)
webertj@14350
  1596
					find_model_from_to (min+1, max)
webertj@14350
  1597
			)
webertj@14350
  1598
	in
webertj@14350
  1599
		writeln ("Trying to find a model of: " ^ (Sign.string_of_term sg t));
webertj@14350
  1600
		if tvars<>[] then
webertj@14350
  1601
			(* TODO: deal with schematic type variables in a better way, if possible *)
webertj@14350
  1602
			error "term contains schematic type variables"
webertj@14350
  1603
		else
webertj@14350
  1604
		(
webertj@14350
  1605
			if minsize<1 then
webertj@14350
  1606
				writeln ("'minsize' is less than 1; starting search with size 1.")
webertj@14350
  1607
			else
webertj@14350
  1608
				();
webertj@14350
  1609
			if maxsize<max (minsize,1) andalso maxsize<>0 then
webertj@14350
  1610
				writeln ("'maxsize' is less than 'minsize': no model found.")
webertj@14350
  1611
			else
webertj@14350
  1612
				find_model_from_to (max (minsize,1), maxsize)
webertj@14350
  1613
		)
webertj@14350
  1614
	end;
webertj@14350
  1615
webertj@14350
  1616
(* ------------------------------------------------------------------------- *)
webertj@14350
  1617
(* refute_term: calls 'find_model' on the negation of a term                 *)
webertj@14350
  1618
(* params     : list of '(name, value)' pairs used to override default       *)
webertj@14350
  1619
(*              parameters                                                   *)
webertj@14350
  1620
(* ------------------------------------------------------------------------- *)
webertj@14350
  1621
webertj@14350
  1622
	(* theory -> (string * string) list -> Term.term -> unit *)
webertj@14350
  1623
webertj@14350
  1624
	fun refute_term thy params t =
webertj@14350
  1625
	let
webertj@14350
  1626
		(* TODO: schematic type variables? *)
webertj@14350
  1627
		val negation = close_vars (HOLogic.Not $ t)
webertj@14350
  1628
		(* If 't' is of type 'propT' (rather than 'boolT'), applying *)
webertj@14350
  1629
		(* 'HOLogic.Not' is not type-correct.  However, this isn't   *)
webertj@14350
  1630
		(* really a problem as long as 'find_model' still interprets *)
webertj@14350
  1631
		(* the resulting term correctly, without checking its type.  *)
webertj@14350
  1632
	in
webertj@14350
  1633
		find_model thy params negation
webertj@14350
  1634
	end;
webertj@14350
  1635
webertj@14350
  1636
(* ------------------------------------------------------------------------- *)
webertj@14350
  1637
(* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)
webertj@14350
  1638
(* params        : list of '(name, value)' pairs used to override default    *)
webertj@14350
  1639
(*                 parameters                                                *)
webertj@14350
  1640
(* subgoal       : 0-based index specifying the subgoal number               *)
webertj@14350
  1641
(* ------------------------------------------------------------------------- *)
webertj@14350
  1642
webertj@14350
  1643
	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
webertj@14350
  1644
webertj@14350
  1645
	fun refute_subgoal thy params thm subgoal =
webertj@14350
  1646
		refute_term thy params (nth_elem (subgoal, prems_of thm));
webertj@14350
  1647
webertj@14350
  1648
end