src/HOL/Tools/refute.ML

Added an exception handler and error msg.

(*  Title:      HOL/Tools/refute.ML
    ID:         $Id$
    Author:     Tjark Weber
    Copyright   2003-2004

Finite model generation for HOL formulae, using an external SAT solver.
*)

(* ------------------------------------------------------------------------- *)
(* Declares the 'REFUTE' signature as well as a structure 'Refute'.  See     *)
(* 'find_model' below for a description of the implemented algorithm, and    *)
(* the Isabelle/Isar theories 'HOL/Refute.thy' and 'HOL/Main.thy' on how to  *)
(* set things up.                                                            *)
(* ------------------------------------------------------------------------- *)

signature REFUTE =
sig

	(* We use 'REFUTE' only for internal error conditions that should    *)
	(* never occur in the first place (i.e. errors caused by bugs in our *)
	(* code).  Otherwise (e.g. to indicate invalid input data) we use    *)
	(* 'error'.                                                          *)

	exception REFUTE of string * string;	(* ("in function", "cause") *)

	val setup : (theory -> theory) list

	val set_default_param : (string * string) -> theory -> theory
	val get_default_param : theory -> string -> string option
	val get_default_params : theory -> (string * string) list

	val find_model : theory -> (string * string) list -> Term.term -> unit

	val refute_term : theory -> (string * string) list -> Term.term -> unit
	val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
end;


structure Refute : REFUTE =
struct
	exception REFUTE of string * string;

	exception EMPTY_DATATYPE;

	structure RefuteDataArgs =
	struct
		val name = "Refute/refute";
		type T = string Symtab.table;
		val empty = Symtab.empty;
		val copy = I;
		val prep_ext = I;
		val merge =
			fn (symTable1, symTable2) =>
				(Symtab.merge (op=) (symTable1, symTable2));
		fun print sg symTable =
			writeln
				("'refute', default parameters:\n" ^
				(space_implode "\n" (map (fn (name,value) => name ^ " = " ^ value) (Symtab.dest symTable))))
	end;

	structure RefuteData = TheoryDataFun(RefuteDataArgs);


(* ------------------------------------------------------------------------- *)
(* INTERFACE, PART 1: INITIALIZATION, PARAMETER MANAGEMENT                   *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
(* structure                                                                 *)
(* ------------------------------------------------------------------------- *)

	val setup = [RefuteData.init];

(* ------------------------------------------------------------------------- *)
(* set_default_param: stores the '(name, value)' pair in RefuteData's symbol *)
(*                    table                                                  *)
(* ------------------------------------------------------------------------- *)

	fun set_default_param (name, value) thy =
	let
		val symTable = RefuteData.get thy
	in
		case Symtab.lookup (symTable, name) of
			None   => RefuteData.put (Symtab.extend (symTable, [(name, value)])) thy
		|	Some _ => RefuteData.put (Symtab.update ((name, value), symTable)) thy
	end;

(* ------------------------------------------------------------------------- *)
(* get_default_param: retrieves the value associated with 'name' from        *)
(*                    RefuteData's symbol table                              *)
(* ------------------------------------------------------------------------- *)

	fun get_default_param thy name = Symtab.lookup (RefuteData.get thy, name);

(* ------------------------------------------------------------------------- *)
(* get_default_params: returns a list of all '(name, value)' pairs that are  *)
(*                     stored in RefuteData's symbol table                   *)
(* ------------------------------------------------------------------------- *)

	fun get_default_params thy = Symtab.dest (RefuteData.get thy);


(* ------------------------------------------------------------------------- *)
(* PROPOSITIONAL FORMULAS                                                    *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* prop_formula: formulas of propositional logic, built from boolean         *)
(*               variables (referred to by index) and True/False using       *)
(*               not/or/and                                                  *)
(* ------------------------------------------------------------------------- *)

	datatype prop_formula =
		  True
		| False
		| BoolVar of int
		| Not of prop_formula
		| Or of prop_formula * prop_formula
		| And of prop_formula * prop_formula;

	(* the following constructor functions make sure that True and False do *)
	(* not occur within any of the other connectives (i.e. Not, Or, And)    *)

	(* prop_formula -> prop_formula *)

	fun SNot True  = False
	  | SNot False = True
	  | SNot fm    = Not fm;

	(* prop_formula * prop_formula -> prop_formula *)

	fun SOr (True, _)   = True
	  | SOr (_, True)   = True
	  | SOr (False, fm) = fm
	  | SOr (fm, False) = fm
	  | SOr (fm1, fm2)  = Or (fm1, fm2);

	(* prop_formula * prop_formula -> prop_formula *)

	fun SAnd (True, fm) = fm
	  | SAnd (fm, True) = fm
	  | SAnd (False, _) = False
	  | SAnd (_, False) = False
	  | SAnd (fm1, fm2) = And (fm1, fm2);

(* ------------------------------------------------------------------------- *)
(* list_disjunction: computes the disjunction of a list of propositional     *)
(*                   formulas                                                *)
(* ------------------------------------------------------------------------- *)

	(* prop_formula list -> prop_formula *)

	fun list_disjunction []      = False
	  | list_disjunction (x::xs) = SOr (x, list_disjunction xs);

(* ------------------------------------------------------------------------- *)
(* list_conjunction: computes the conjunction of a list of propositional     *)
(*                   formulas                                                *)
(* ------------------------------------------------------------------------- *)

	(* prop_formula list -> prop_formula *)

	fun list_conjunction []      = True
	  | list_conjunction (x::xs) = SAnd (x, list_conjunction xs);

(* ------------------------------------------------------------------------- *)
(* prop_formula_dot_product: [x1,...,xn] * [y1,...,yn] -> x1*y1+...+xn*yn    *)
(* ------------------------------------------------------------------------- *)

	(* prop_formula list * prop_formula list -> prop_formula *)

	fun prop_formula_dot_product ([],[])       = False
	  | prop_formula_dot_product (x::xs,y::ys) = SOr (SAnd (x,y), prop_formula_dot_product (xs,ys))
	  | prop_formula_dot_product (_,_)         = raise REFUTE ("prop_formula_dot_product", "lists are of different length");

(* ------------------------------------------------------------------------- *)
(* prop_formula_to_nnf: computes the negation normal form of a formula 'fm'  *)
(*                      of propositional logic (i.e. only variables may be   *)
(*                      negated, but not subformulas)                        *)
(* ------------------------------------------------------------------------- *)

	(* prop_formula -> prop_formula *)

	fun prop_formula_to_nnf fm =
		case fm of
		(* constants *)
		  True                => True
		| False               => False
		(* literals *)
		| BoolVar i           => BoolVar i
		| Not (BoolVar i)     => Not (BoolVar i)
		(* double-negation elimination *)
		| Not (Not fm)        => prop_formula_to_nnf fm
		(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
		| Not (Or  (fm1,fm2)) => SAnd (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
		| Not (And (fm1,fm2)) => SOr  (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
		(* 'or' and 'and' as outermost connectives are left untouched *)
		| Or  (fm1,fm2)       => SOr  (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
		| And (fm1,fm2)       => SAnd (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
		(* 'not' + constant *)
		| Not _               => raise REFUTE ("prop_formula_to_nnf", "'True'/'False' not allowed inside of 'Not'");

(* ------------------------------------------------------------------------- *)
(* prop_formula_nnf_to_cnf: computes the conjunctive normal form of a        *)
(*      formula 'fm' of propositional logic that is given in negation normal *)
(*      form.  Note that there may occur an exponential blowup of the        *)
(*      formula.                                                             *)
(* ------------------------------------------------------------------------- *)

	(* prop_formula -> prop_formula *)

	fun prop_formula_nnf_to_cnf fm =
		case fm of
		(* constants *)
		  True            => True
		| False           => False
		(* literals *)
		| BoolVar i       => BoolVar i
		| Not (BoolVar i) => Not (BoolVar i)
		(* pushing 'or' inside of 'and' using distributive laws *)
		| Or (fm1,fm2)    =>
			let
				val fm1' = prop_formula_nnf_to_cnf fm1
				val fm2' = prop_formula_nnf_to_cnf fm2
			in
				case fm1' of
				  And (fm11,fm12) => prop_formula_nnf_to_cnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2')))
				| _               =>
					(case fm2' of
					  And (fm21,fm22) => prop_formula_nnf_to_cnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22)))
					(* neither subformula contains 'and' *)
					| _               => fm)
			end
		(* 'and' as outermost connective is left untouched *)
		| And (fm1,fm2)   => SAnd (prop_formula_nnf_to_cnf fm1, prop_formula_nnf_to_cnf fm2)
		(* error *)
		| _               => raise REFUTE ("prop_formula_nnf_to_cnf", "formula is not in negation normal form");

(* ------------------------------------------------------------------------- *)
(* max: computes the maximum of two integer values 'i' and 'j'               *)
(* ------------------------------------------------------------------------- *)

	(* int * int -> int *)

	fun max (i,j) =
		if (i>j) then i else j;

(* ------------------------------------------------------------------------- *)
(* max_var_index: computes the maximal variable index occuring in 'fm',      *)
(*      where 'fm' is a formula of propositional logic                       *)
(* ------------------------------------------------------------------------- *)

	(* prop_formula -> int *)

	fun max_var_index fm =
		case fm of
		  True          => 0
		| False         => 0
		| BoolVar i     => i
		| Not fm1       => max_var_index fm1
		| And (fm1,fm2) => max (max_var_index fm1, max_var_index fm2)
		| Or (fm1,fm2)  => max (max_var_index fm1, max_var_index fm2);

(* ------------------------------------------------------------------------- *)
(* prop_formula_nnf_to_def_cnf: computes the definitional conjunctive normal *)
(*      form of a formula 'fm' of propositional logic that is given in       *)
(*      negation normal form.  To avoid an exponential blowup of the         *)
(*      formula, auxiliary variables may be introduced.  The result formula  *)
(*      is SAT-equivalent to 'fm' (i.e. it is satisfiable if and only if     *)
(*      'fm' is satisfiable).                                                *)
(* ------------------------------------------------------------------------- *)

	(* prop_formula -> prop_formula *)

	fun prop_formula_nnf_to_def_cnf fm =
	let
		(* prop_formula * int -> prop_formula * int *)
		fun prop_formula_nnf_to_def_cnf_new (fm,new) =
		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
			case fm of
			(* constants *)
			  True            => (True, new)
			| False           => (False, new)
			(* literals *)
			| BoolVar i       => (BoolVar i, new)
			| Not (BoolVar i) => (Not (BoolVar i), new)
			(* pushing 'or' inside of 'and' using distributive laws *)
			| Or (fm1,fm2)    =>
				let
					val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
					val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
				in
					case fst fm1' of
					  And (fm11,fm12) =>
						let
							val aux = BoolVar (snd fm2')
						in
							(* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *)
							prop_formula_nnf_to_def_cnf_new (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fst fm2', Not aux)), (snd fm2')+1)
						end
					| _               =>
						(case fst fm2' of
						  And (fm21,fm22) =>
							let
								val aux = BoolVar (snd fm2')
							in
								(* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *)
								prop_formula_nnf_to_def_cnf_new (SAnd (SOr (fst fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), (snd fm2')+1)
							end
						(* neither subformula contains 'and' *)
						| _               => (fm, new))
				end
			(* 'and' as outermost connective is left untouched *)
			| And (fm1,fm2)   =>
				let
					val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
					val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
				in
					(SAnd (fst fm1', fst fm2'), snd fm2')
				end
			(* error *)
			| _               => raise REFUTE ("prop_formula_nnf_to_def_cnf", "formula is not in negation normal form")
	in
		fst (prop_formula_nnf_to_def_cnf_new (fm, (max_var_index fm)+1))
	end;

(* ------------------------------------------------------------------------- *)
(* prop_formula_to_cnf: computes the conjunctive normal form of a formula    *)
(*                      'fm' of propositional logic                          *)
(* ------------------------------------------------------------------------- *)

	(* prop_formula -> prop_formula *)

	fun prop_formula_to_cnf fm =
		prop_formula_nnf_to_cnf (prop_formula_to_nnf fm);

(* ------------------------------------------------------------------------- *)
(* prop_formula_to_def_cnf: computes the definitional conjunctive normal     *)
(*      form of a formula 'fm' of propositional logic, introducing auxiliary *)
(*      variables if necessary to avoid an exponential blowup of the formula *)
(* ------------------------------------------------------------------------- *)

	(* prop_formula -> prop_formula *)

	fun prop_formula_to_def_cnf fm =
		prop_formula_nnf_to_def_cnf (prop_formula_to_nnf fm);

(* ------------------------------------------------------------------------- *)
(* prop_formula_to_dimacs_cnf_format: serializes a formula of propositional  *)
(*      logic to a file in DIMACS CNF format (see "Satisfiability Suggested  *)
(*      Format", May 8 1993, Section 2.1)                                    *)
(* fm  : formula to be serialized.  Note: 'fm' must not contain a variable   *)
(*       index less than 1.                                                  *)
(* def : If true, translate 'fm' into definitional CNF.  Otherwise translate *)
(*       'fm' into CNF.                                                      *)
(* path: path of the file to be created                                      *)
(* ------------------------------------------------------------------------- *)

	(* prop_formula -> bool -> Path.T -> unit *)

	fun prop_formula_to_dimacs_cnf_format fm def path =
	let
		(* prop_formula *)
		val cnf =
			if def then
				prop_formula_to_def_cnf fm
			else
				prop_formula_to_cnf fm
		val fm' =
			case cnf of
			  True  => Or (BoolVar 1, Not (BoolVar 1))
			| False => And (BoolVar 1, Not (BoolVar 1))
			| _     => cnf (* either 'cnf'=True/False, or 'cnf' does not contain True/False at all *)
		(* prop_formula -> int *)
		fun cnf_number_of_clauses (And (fm1,fm2)) =
			(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
		  | cnf_number_of_clauses _ =
			1
		(* prop_formula -> string *)
		fun cnf_prop_formula_to_string (BoolVar i) =
			if (i<1) then
				raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains a variable index less than 1")
			else
				(string_of_int i)
		  | cnf_prop_formula_to_string (Not fm1) =
			"-" ^ (cnf_prop_formula_to_string fm1)
		  | cnf_prop_formula_to_string (Or (fm1,fm2)) =
			(cnf_prop_formula_to_string fm1) ^ " " ^ (cnf_prop_formula_to_string fm2)
		  | cnf_prop_formula_to_string (And (fm1,fm2)) =
			(cnf_prop_formula_to_string fm1) ^ " 0\n" ^ (cnf_prop_formula_to_string fm2)
		  | cnf_prop_formula_to_string _ =
			raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains True/False")
	in
		File.write path ("c This file was generated by prop_formula_to_dimacs_cnf_format\n"
			^ "c (c) Tjark Weber\n"
			^ "p cnf " ^ (string_of_int (max_var_index fm')) ^ " " ^ (string_of_int (cnf_number_of_clauses fm')) ^ "\n"
			^ (cnf_prop_formula_to_string fm') ^ "\n")
	end;

(* ------------------------------------------------------------------------- *)
(* prop_formula_to_dimacs_sat_format: serializes a formula of propositional  *)
(*      logic to a file in DIMACS SAT format (see "Satisfiability Suggested  *)
(*      Format", May 8 1993, Section 2.2)                                    *)
(* fm  : formula to be serialized.  Note: 'fm' must not contain a variable   *)
(*       index less than 1.                                                  *)
(* path: path of the file to be created                                      *)
(* ------------------------------------------------------------------------- *)

	(* prop_formula -> Path.T -> unit *)

	fun prop_formula_to_dimacs_sat_format fm path =
	let
		fun prop_formula_to_string True =
			"*()"
		  | prop_formula_to_string False =
			"+()"
		  | prop_formula_to_string (BoolVar i) =
			if (i<1) then
				raise REFUTE ("prop_formula_to_dimacs_sat_format", "formula contains a variable index less than 1")
			else
				(string_of_int i)
		  | prop_formula_to_string (Not fm1) =
			"-(" ^ (prop_formula_to_string fm1) ^ ")"
		  | prop_formula_to_string (Or (fm1,fm2)) =
			"+(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
		  | prop_formula_to_string (And (fm1,fm2)) =
			"*(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
	in
		File.write path ("c This file was generated by prop_formula_to_dimacs_sat_format\n"
			^ "c (c) Tjark Weber\n"
			^ "p sat " ^ (string_of_int (max (max_var_index fm, 1))) ^ "\n"
			^ "(" ^ (prop_formula_to_string fm) ^ ")\n")
	end;

(* ------------------------------------------------------------------------- *)
(* prop_formula_sat_solver: try to find a satisfying assignment for the      *)
(*      boolean variables in a propositional formula, using an external SAT  *)
(*      solver.  If the SAT solver did not find an assignment, 'None' is     *)
(*      returned.  Otherwise 'Some (list of integers)' is returned, where    *)
(*      i>0 means that the boolean variable i is set to TRUE, and i<0 means  *)
(*      that the boolean variable i is set to FALSE.  Note that if           *)
(*      'satformat' is 'defcnf', then the assignment returned may contain    *)
(*      auxiliary variables that were not present in the original formula    *)
(*      'fm'.                                                                *)
(* fm        : formula that is passed to the SAT solver                      *) 
(* satpath   : path of the file used to store the propositional formula,     *)
(*             i.e. the input to the SAT solver                              *)
(* satformat : format of the SAT solver's input file.  Must be either "cnf", *)
(*             "defcnf", or "sat".                                           *)
(* resultpath: path of the file containing the SAT solver's output           *)
(* success   : part of the line in the SAT solver's output that is followed  *)
(*             by a line consisting of a list of integers representing the   *)
(*             satisfying assignment                                         *)
(* command   : system command used to execute the SAT solver                 *)
(* ------------------------------------------------------------------------- *)

	(* prop_formula -> Path.T -> string -> Path.T -> string -> string -> int list option *)

	fun prop_formula_sat_solver fm satpath satformat resultpath success command =
		if File.exists satpath then
			error ("file '" ^ (Path.pack satpath) ^ "' exists, please delete (will not overwrite)")
		else if File.exists resultpath then
			error ("file '" ^ (Path.pack resultpath) ^ "' exists, please delete (will not overwrite)")
		else
		(
			(* serialize the formula 'fm' to a file *)
			if satformat="cnf" then
				prop_formula_to_dimacs_cnf_format fm false satpath
			else if satformat="defcnf" then
				prop_formula_to_dimacs_cnf_format fm true satpath
			else if satformat="sat" then
				prop_formula_to_dimacs_sat_format fm satpath
			else
				error ("invalid argument: satformat='" ^ satformat ^ "' (must be either 'cnf', 'defcnf', or 'sat')");
			(* execute SAT solver *)
			if (system command)<>0 then
			(
				(* error executing SAT solver *)
				File.rm satpath;
				File.rm resultpath;
				error ("system command '" ^ command ^ "' failed (make sure a SAT solver is installed)")
			)
			else
			(
				(* read assignment from the result file *)
				File.rm satpath;
				let
					(* 'a option -> 'a Library.option *)
					fun option (SOME a) =
						Some a
					  | option NONE =
						None
					(* string -> int list *)
					fun string_to_int_list s =
						mapfilter (option o Int.fromString) (space_explode " " s)
					(* string -> string -> bool *)
					fun is_substring s1 s2 =
					let
						val length1 = String.size s1
						val length2 = String.size s2
					in
						if length2 < length1 then
							false
						else if s1 = String.substring (s2, 0, length1) then
							true
						else is_substring s1 (String.substring (s2, 1, length2-1))
					end
					(* string list -> int list option *)
					fun extract_solution [] =
						None
					  | extract_solution (line::lines) =
						if is_substring success line then
							(* the next line must be a list of integers *)
							Some (string_to_int_list (hd lines))
						else
							extract_solution lines
					val sat_result = File.read resultpath
				in
					File.rm resultpath;
					extract_solution (split_lines sat_result)
				end
			)
		);


(* ------------------------------------------------------------------------- *)
(* TREES                                                                     *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* tree: implements an arbitrarily (but finitely) branching tree as a list   *)
(*       of (lists of ...) elements                                          *)
(* ------------------------------------------------------------------------- *)

	datatype 'a tree =
		  Leaf of 'a
		| Node of ('a tree) list;

	type prop_tree =
		prop_formula list tree;

	(* ('a -> 'b) -> 'a tree -> 'b tree *)

	fun tree_map f tr =
		case tr of
		  Leaf x  => Leaf (f x)
		| Node xs => Node (map (tree_map f) xs);

	(* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)

	fun tree_foldl f =
	let
		fun itl (e, Leaf x)  = f(e,x)
		  | itl (e, Node xs) = foldl (tree_foldl f) (e,xs)
	in
		itl
	end;

	(* 'a tree * 'b tree -> ('a * 'b) tree *)

	fun tree_pair (t1,t2) =
		case t1 of
		  Leaf x =>
			(case t2 of
				  Leaf y => Leaf (x,y)
				| Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)"))
		| Node xs =>
			(case t2 of
				  (* '~~' will raise an exception if the number of branches in both trees is different at the current node *)
				  Node ys => Node (map tree_pair (xs ~~ ys))
				| Leaf _  => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));

(* ------------------------------------------------------------------------- *)
(* prop_tree_to_true: returns a propositional formula that is true iff the   *)
(*      tree denotes the boolean value TRUE                                  *)
(* ------------------------------------------------------------------------- *)

	(* prop_tree -> prop_formula *)

	(* a term of type 'bool' is represented as a 2-element leaf, where *)
	(* the term is true iff the leaf's first element is true           *)

	fun prop_tree_to_true (Leaf [fm,_]) =
		fm
	  | prop_tree_to_true _ =
		raise REFUTE ("prop_tree_to_true", "tree is not a 2-element leaf");

(* ------------------------------------------------------------------------- *)
(* prop_tree_to_false: returns a propositional formula that is true iff the  *)
(*      tree denotes the boolean value FALSE                                 *)
(* ------------------------------------------------------------------------- *)

	(* prop_tree -> prop_formula *)

	(* a term of type 'bool' is represented as a 2-element leaf, where *)
	(* the term is false iff the leaf's second element is true         *)

	fun prop_tree_to_false (Leaf [_,fm]) =
		fm
	  | prop_tree_to_false _ =
		raise REFUTE ("prop_tree_to_false", "tree is not a 2-element leaf");

(* ------------------------------------------------------------------------- *)
(* restrict_to_single_element: returns a propositional formula which is true *)
(*      iff the tree 'tr' describes a single element of its corresponding    *)
(*      type, i.e. iff at each leaf, one and only one formula is true        *)
(* ------------------------------------------------------------------------- *)

	(* prop_tree -> prop_formula *)

	fun restrict_to_single_element tr =
	let
		(* prop_formula list -> prop_formula *)
		fun allfalse []      = True
		  | allfalse (x::xs) = SAnd (SNot x, allfalse xs)
		(* prop_formula list -> prop_formula *)
		fun exactly1true []      = False
		  | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
	in
		case tr of
		  Leaf [BoolVar _, Not (BoolVar _)] => True (* optimization for boolean variables *)
		| Leaf xs                           => exactly1true xs
		| Node trees                        => list_conjunction (map restrict_to_single_element trees)
	end;

(* ------------------------------------------------------------------------- *)
(* HOL FORMULAS                                                              *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* absvar: form an abstraction over a schematic variable                     *)
(* ------------------------------------------------------------------------- *)

	(* Term.indexname * Term.typ * Term.term -> Term.term *)

	(* this function is similar to Term.absfree, but for schematic       *)
	(* variables (rather than free variables)                            *)
	fun absvar ((x,i),T,body) =
		Abs(x, T, abstract_over (Var((x,i),T), body));

(* ------------------------------------------------------------------------- *)
(* list_all_var: quantification over a list of schematic variables           *)
(* ------------------------------------------------------------------------- *)

	(* (Term.indexname * Term.typ) list * Term.term -> Term.term *)

	(* this function is similar to Term.list_all_free, but for schematic *)
	(* variables (rather than free variables)                            *)
	fun list_all_var ([], t) =
		t
	  | list_all_var ((idx,T)::vars, t) =
		(all T) $ (absvar(idx, T, list_all_var(vars,t)));

(* ------------------------------------------------------------------------- *)
(* close_vars: close up a formula over all schematic variables by            *)
(*             quantification (note that the result term may still contain   *)
(*             (non-schematic) free variables)                               *)
(* ------------------------------------------------------------------------- *)

	(* Term.term -> Term.term *)

	(* this function is similar to Logic.close_form, but for schematic   *)
	(* variables (rather than free variables)                            *)
	fun close_vars A =
		list_all_var (sort_wrt (fst o fst) (map dest_Var (term_vars A)), A);

(* ------------------------------------------------------------------------- *)
(* make_universes: given a list 'xs' of "types" and a universe size 'size',  *)
(*      this function returns all possible partitions of the universe into   *)
(*      the "types" in 'xs' such that no "type" is empty.  If 'size' is less *)
(*      than 'length xs', the returned list of partitions is empty.          *)
(*      Otherwise, if the list 'xs' is empty, then the returned list of      *)
(*      partitions contains only the empty list, regardless of 'size'.       *)
(* ------------------------------------------------------------------------- *)

	(* 'a list -> int -> ('a * int) list list *)

	fun make_universes xs size =
	let
		(* 'a list -> int -> int -> ('a * int) list list *)
		fun make_partitions_loop (x::xs) 0 total =
			map (fn us => ((x,0)::us)) (make_partitions xs total)
		  | make_partitions_loop (x::xs) first total =
			(map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
		  | make_partitions_loop _ _ _ =
			raise REFUTE ("make_universes::make_partitions_loop", "empty list")
		and
		(* 'a list -> int -> ('a * int) list list *)
		make_partitions [x] size =
			(* we must use all remaining elements on the type 'x', so there is only one partition *)
			[[(x,size)]]
		  | make_partitions (x::xs) 0 =
			(* there are no elements left in the universe, so there is only one partition *)
			[map (fn t => (t,0)) (x::xs)]
		  | make_partitions (x::xs) size =
			(* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
			make_partitions_loop (x::xs) size size
		  | make_partitions _ _ =
			raise REFUTE ("make_universes::make_partitions", "empty list")
		val len = length xs
	in
		if size<len then
			(* the universe isn't big enough to make every type non-empty *)
			[]
		else if xs=[] then
			(* no types: return one universe, regardless of the size *)
			[[]]
		else
			(* partition into possibly empty types, then add 1 element to each type *)
			map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
	end;

(* ------------------------------------------------------------------------- *)
(* sum: computes the sum of a list of integers; sum [] = 0                   *)
(* ------------------------------------------------------------------------- *)

	(* int list -> int *)

	fun sum xs = foldl op+ (0, xs);

(* ------------------------------------------------------------------------- *)
(* product: computes the product of a list of integers; product [] = 1       *)
(* ------------------------------------------------------------------------- *)

	(* int list -> int *)

	fun product xs = foldl op* (1, xs);

(* ------------------------------------------------------------------------- *)
(* power: power(a,b) computes a^b, for a>=0, b>=0                            *)
(* ------------------------------------------------------------------------- *)

	(* int * int -> int *)

	fun power (a,0) = 1
	  | power (a,1) = a
	  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end;

(* ------------------------------------------------------------------------- *)
(* size_of_type: returns the size of a type, where 'us' specifies the size   *)
(*      of each basic type (i.e. each type variable), and 'cdepth' specifies *)
(*      the maximal constructor depth for inductive datatypes                *)
(* ------------------------------------------------------------------------- *)

	(* Term.typ -> (Term.typ * int) list -> theory -> int -> int *)

	fun size_of_type T us thy cdepth =
	let
		(* Term.typ -> (Term.typ * int) -> int *)
		fun lookup_size T [] =
			raise REFUTE ("size_of_type", "no size specified for type variable '" ^ (Sign.string_of_typ (sign_of thy) T) ^ "'")
		  | lookup_size T ((typ,size)::pairs) =
			if T=typ then size else lookup_size T pairs
	in
		case T of
		  Type ("prop", [])     => 2
		| Type ("bool", [])     => 2
		| Type ("Product_Type.unit", []) => 1
		| Type ("+", [T1,T2])   => (size_of_type T1 us thy cdepth) + (size_of_type T2 us thy cdepth)
		| Type ("*", [T1,T2])   => (size_of_type T1 us thy cdepth) * (size_of_type T2 us thy cdepth)
		| Type ("fun", [T1,T2]) => power (size_of_type T2 us thy cdepth, size_of_type T1 us thy cdepth)
		| Type ("set", [T1])    => size_of_type (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
		| Type (s, Ts)          =>
			(case DatatypePackage.datatype_info thy s of
			  Some info => (* inductive datatype *)
				if cdepth>0 then
					let
						val index               = #index info
						val descr               = #descr info
						val (_, dtyps, constrs) = the (assoc (descr, index))
						val Typs                = dtyps ~~ Ts
						(* DatatypeAux.dtyp -> Term.typ *)
						fun typ_of_dtyp (DatatypeAux.DtTFree a) =
							the (assoc (Typs, DatatypeAux.DtTFree a))
						  | typ_of_dtyp (DatatypeAux.DtRec i) =
							let
								val (s, ds, _) = the (assoc (descr, i))
							in
								Type (s, map typ_of_dtyp ds)
							end
						  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
							Type (s, map typ_of_dtyp ds)
					in
						sum (map (fn (_,ds) => product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)) constrs)
					end
				else 0
			| None      => error ("size_of_type: type contains an unknown type constructor: '" ^ s ^ "'"))
		| TFree _               => lookup_size T us
		| TVar _                => lookup_size T us
	end;

(* ------------------------------------------------------------------------- *)
(* type_to_prop_tree: creates a tree of boolean variables that denotes an    *)
(*      element of the type 'T'.  The height and branching factor of the     *)
(*      tree depend on the size and "structure" of 'T'.                      *)
(* 'us' : a "universe" specifying the number of elements for each basic type *)
(*        (i.e. each type variable) in 'T'                                   *)
(* 'cdepth': maximum constructor depth to be used for inductive datatypes    *)
(* 'idx': the next index to be used for a boolean variable                   *)
(* ------------------------------------------------------------------------- *)

	(* Term.typ -> (Term.typ * int) list -> theory -> int -> int -> prop_tree * int *)

	fun type_to_prop_tree T us thy cdepth idx =
	let
		(* int -> Term.typ -> int -> prop_tree list * int *)
		fun type_to_prop_tree_list 1 T' idx' =
			let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
				([tr], newidx)
			end
		  | type_to_prop_tree_list n T' idx' =
			let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
				let val (trees, lastidx) = type_to_prop_tree_list (n-1) T' newidx in
					(tr::trees, lastidx)
				end
			end
	in
		case T of
		  Type ("prop", []) =>
			(Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
		| Type ("bool", []) =>
			(Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
		| Type ("Product_Type.unit", []) =>
			(Leaf [True], idx)
		| Type ("+", [T1,T2]) =>
			let
				val s1 = size_of_type T1 us thy cdepth
				val s2 = size_of_type T2 us thy cdepth
				val s  = s1 + s2
			in
				if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
					raise EMPTY_DATATYPE
				else
					error "sum types (+) not implemented yet (TODO)"
			end
		| Type ("*", [T1,T2]) =>
			let
				val s1 = size_of_type T1 us thy cdepth
				val s2 = size_of_type T2 us thy cdepth
				val s  = s1 * s2
			in
				if s1=0 orelse s2=0 then
					raise EMPTY_DATATYPE
				else
					error "product types (*) not implemented yet (TODO)"
			end
		| Type ("fun", [T1,T2]) =>
			(* we create 'size_of_type T1' different copies of the tree for 'T2', *)
			(* which are then combined into a single new tree                     *)
			let
				val s = size_of_type T1 us thy cdepth
			in
				if s=0 then
					raise EMPTY_DATATYPE
				else
					let val (trees, newidx) = type_to_prop_tree_list s T2 idx in
						(Node trees, newidx)
					end
			end
		| Type ("set", [T1]) =>
			type_to_prop_tree (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth idx
		| Type (s, _) =>
			(case DatatypePackage.constrs_of thy s of
			   Some _ => (* inductive datatype *)
					let
						val s = size_of_type T us thy cdepth
					in
						if s=0 then
							raise EMPTY_DATATYPE
						else
							(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
					end
			 | None   => error ("type_to_prop_tree: type contains an unknown type constructor: '" ^ s ^ "'"))
		| TFree _ =>
			let val s = size_of_type T us thy cdepth in
				(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
			end
		| TVar _  =>
			let val s = size_of_type T us thy cdepth in
				(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
			end
	end;

(* ------------------------------------------------------------------------- *)
(* type_to_constants: creates a list of prop_trees with constants (True,     *)
(*      False) rather than boolean variables, one for every element in the   *)
(*      type 'T'; c.f. type_to_prop_tree                                     *)
(* ------------------------------------------------------------------------- *)

	(* Term.typ -> (Term.typ * int) list -> theory -> int -> prop_tree list *)

	fun type_to_constants T us thy cdepth =
	let
		(* returns a list with all unit vectors of length n *)
		(* int -> prop_tree list *)
		fun unit_vectors n =
		let
			(* returns the k-th unit vector of length n *)
			(* int * int -> prop_tree *)
			fun unit_vector (k,n) =
				Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
			(* int -> prop_tree list -> prop_tree list *)
			fun unit_vectors_acc k vs =
				if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
		in
			unit_vectors_acc 1 []
		end
		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
		(* 'a -> 'a list list -> 'a list list *)
		fun cons_list x xss =
			map (fn xs => x::xs) xss
		(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
		(* int -> 'a list -> 'a list list *)
		fun pick_all 1 xs =
			map (fn x => [x]) xs
		  | pick_all n xs =
			let val rec_pick = pick_all (n-1) xs in
				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
			end
	in
		case T of
		  Type ("prop", [])     => unit_vectors 2
		| Type ("bool", [])     => unit_vectors 2
		| Type ("Product_Type.unit", []) => unit_vectors 1
                | Type ("+", [T1,T2])   =>
			let
				val s1 = size_of_type T1 us thy cdepth
				val s2 = size_of_type T2 us thy cdepth
			in
				if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
					raise EMPTY_DATATYPE
				else
					error "sum types (+) not implemented yet (TODO)"
			end
                | Type ("*", [T1,T2])   =>
			let
				val s1 = size_of_type T1 us thy cdepth
				val s2 = size_of_type T2 us thy cdepth
			in
				if s1=0 orelse s2=0 then
					raise EMPTY_DATATYPE
				else
					error "product types (*) not implemented yet (TODO)"
			end
		| Type ("fun", [T1,T2]) =>
			let
				val s = size_of_type T1 us thy cdepth
			in
				if s=0 then
					raise EMPTY_DATATYPE
				else
					map (fn xs => Node xs) (pick_all s (type_to_constants T2 us thy cdepth))
			end
		| Type ("set", [T1])    => type_to_constants (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
		| Type (s, _)           =>
			(case DatatypePackage.constrs_of thy s of
			   Some _ => (* inductive datatype *)
					let
						val s = size_of_type T us thy cdepth
					in
						if s=0 then
							raise EMPTY_DATATYPE
						else
							unit_vectors s
					end
			 | None   => error ("type_to_constants: type contains an unknown type constructor: '" ^ s ^ "'"))
		| TFree _               => unit_vectors (size_of_type T us thy cdepth)
		| TVar _                => unit_vectors (size_of_type T us thy cdepth)
	end;

(* ------------------------------------------------------------------------- *)
(* prop_tree_equal: returns a propositional formula that is true iff 'tr1'   *)
(*      and 'tr2' both denote the same element                               *)
(* ------------------------------------------------------------------------- *)

	(* prop_tree * prop_tree -> prop_formula *)

	fun prop_tree_equal (tr1,tr2) =
		case tr1 of
		  Leaf x =>
			(case tr2 of
			  Leaf y => prop_formula_dot_product (x,y)
			| _      => raise REFUTE ("prop_tree_equal", "second tree is higher"))
		| Node xs =>
			(case tr2 of
			  Leaf _  => raise REFUTE ("prop_tree_equal", "first tree is higher")
			(* extensionality: two functions are equal iff they are equal for every element *)
			| Node ys => list_conjunction (map prop_tree_equal (xs ~~ ys)));

(* ------------------------------------------------------------------------- *)
(* prop_tree_apply: returns a tree that denotes the element obtained by      *)
(*      applying the function which is denoted by the tree 't1' to the       *)
(*      element which is denoted by the tree 't2'                            *)
(* ------------------------------------------------------------------------- *)

	(* prop_tree * prop_tree -> prop_tree *)

	fun prop_tree_apply (tr1,tr2) =
	let
		(* prop_tree * prop_tree -> prop_tree *)
		fun prop_tree_disjunction (tr1,tr2) =
			tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
		(* prop_formula * prop_tree -> prop_tree *)
		fun prop_formula_times_prop_tree (fm,tr) =
			tree_map (map (fn x => SAnd (fm,x))) tr
		(* prop_formula list * prop_tree list -> prop_tree *)
		fun prop_formula_list_dot_product_prop_tree_list ([fm],[tr]) =
			prop_formula_times_prop_tree (fm,tr)
		  | prop_formula_list_dot_product_prop_tree_list (fm::fms,tr::trees) =
			prop_tree_disjunction (prop_formula_times_prop_tree (fm,tr), prop_formula_list_dot_product_prop_tree_list (fms,trees))
		  | prop_formula_list_dot_product_prop_tree_list (_,_) =
			raise REFUTE ("prop_tree_apply::prop_formula_list_dot_product_prop_tree_list", "empty list")
		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
		(* 'a -> 'a list list -> 'a list list *)
		fun cons_list x xss =
			map (fn xs => x::xs) xss
		(* returns a list of lists, each one consisting of one element from each element of 'xss' *)
		(* 'a list list -> 'a list list *)
		fun pick_all [xs] =
			map (fn x => [x]) xs
		  | pick_all (xs::xss) =
			let val rec_pick = pick_all xss in
				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
			end
		  | pick_all _ =
			raise REFUTE ("prop_tree_apply::pick_all", "empty list")
		(* prop_tree -> prop_formula list *)
		fun prop_tree_to_prop_formula_list (Leaf xs) =
			xs
		  | prop_tree_to_prop_formula_list (Node trees) =
			map list_conjunction (pick_all (map prop_tree_to_prop_formula_list trees))
	in
		case tr1 of
		  Leaf _ =>
			raise REFUTE ("prop_tree_apply", "first tree is a leaf")
		| Node xs =>
			prop_formula_list_dot_product_prop_tree_list (prop_tree_to_prop_formula_list tr2, xs)
	end

(* ------------------------------------------------------------------------- *)
(* term_to_prop_tree: translates a HOL term 't' into a tree of propositional *)
(*      formulas; 'us' specifies the number of elements for each type        *)
(*      variable in 't'; 'cdepth' specifies the maximal constructor depth    *)
(*      for inductive datatypes.  Also returns the lowest index that was not *)
(*      used for a boolean variable, and a substitution of terms (free/      *)
(*      schematic variables) by prop_trees.                                  *)
(* ------------------------------------------------------------------------- *)

	(* Term.term -> (Term.typ * int) list -> theory -> int -> prop_tree * (int * (Term.term * prop_tree) list) *)

	fun term_to_prop_tree t us thy cdepth =
	let
		(* Term.term -> int * (Term.term * prop_tree) list -> prop_tree * (int * (Term.term * prop_tree) list) *)
		fun variable_to_prop_tree_subst t' (idx,subs) =
			case assoc (subs,t') of
			  Some tr =>
				(* return the previously associated tree; the substitution remains unchanged *)
				(tr, (idx,subs))
			| None =>
				(* generate a new tree; update the index; extend the substitution *)
				let
					val T = case t' of
						  Free (_,T) => T
						| Var (_,T)  => T
						| _          => raise REFUTE ("variable_to_prop_tree_subst", "term is not a (free or schematic) variable")
					val (tr,newidx) = type_to_prop_tree T us thy cdepth idx
				in
					(tr, (newidx, (t',tr)::subs))
				end
		(* Term.term -> int * (Term.term * prop_tree) list -> prop_tree list -> prop_tree * (int * (Term.term * prop_tree) list) *)
		fun term_to_prop_tree_subst t' (idx,subs) bsubs =
			case t' of
			(* meta-logical constants *)
			  Const ("Goal", _) $ t1 =>
				term_to_prop_tree_subst t1 (idx,subs) bsubs
			| Const ("all", _) $ t1 =>
				let
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
				in
					case tree1 of
					  Node xs =>
						let
							val fmTrue  = list_conjunction (map prop_tree_to_true xs)
							val fmFalse = list_disjunction (map prop_tree_to_false xs)
						in
							(Leaf [fmTrue, fmFalse], (i1,s1))
						end
					| _ =>
						raise REFUTE ("term_to_prop_tree_subst", "'all' is not followed by a function")
				end
			| Const ("==", _) $ t1 $ t2 =>
				let
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
					val fmTrue          = prop_tree_equal (tree1,tree2)
					val fmFalse         = SNot fmTrue
				in
					(Leaf [fmTrue, fmFalse], (i2,s2))
				end
			| Const ("==>", _) $ t1 $ t2 =>
				let
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
					val fmTrue          = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
					val fmFalse         = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
				in
					(Leaf [fmTrue, fmFalse], (i2,s2))
				end
			(* HOL constants *)
			| Const ("Trueprop", _) $ t1 =>
				term_to_prop_tree_subst t1 (idx,subs) bsubs
			| Const ("Not", _) $ t1 =>
				let
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
					val fmTrue          = prop_tree_to_false tree1
					val fmFalse         = prop_tree_to_true tree1
				in
					(Leaf [fmTrue, fmFalse], (i1,s1))
				end
			| Const ("True", _) =>
				(Leaf [True, False], (idx,subs))
			| Const ("False", _) =>
				(Leaf [False, True], (idx,subs))
			| Const ("All", _) $ t1 =>
				let
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
				in
					case tree1 of
					  Node xs =>
						let
							val fmTrue  = list_conjunction (map prop_tree_to_true xs)
							val fmFalse = list_disjunction (map prop_tree_to_false xs)
						in
							(Leaf [fmTrue, fmFalse], (i1,s1))
						end
					| _ =>
						raise REFUTE ("term_to_prop_tree_subst", "'All' is not followed by a function")
				end
			| Const ("Ex", _) $ t1 =>
				let
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
				in
					case tree1 of
					  Node xs =>
						let
							val fmTrue  = list_disjunction (map prop_tree_to_true xs)
							val fmFalse = list_conjunction (map prop_tree_to_false xs)
						in
							(Leaf [fmTrue, fmFalse], (i1,s1))
						end
					| _ =>
						raise REFUTE ("term_to_prop_tree_subst", "'Ex' is not followed by a function")
				end
			| Const ("Ex1", Type ("fun", [Type ("fun", [T, Type ("bool",[])]), Type ("bool",[])])) $ t1 =>
				(* 'Ex1 t1' is equivalent to 'Ex Abs(x,T,t1' x & All Abs(y,T,t1'' y --> x=y))' *)
				let
					val t1'      = Term.incr_bv (1, 0, t1)
					val t1''     = Term.incr_bv (2, 0, t1)
					val t_equal  = (HOLogic.eq_const T) $ (Bound 1) $ (Bound 0)
					val t_unique = (HOLogic.all_const T) $ Abs("y",T,HOLogic.mk_imp (t1'' $ (Bound 0),t_equal))
					val t_ex1    = (HOLogic.exists_const T) $ Abs("x",T,HOLogic.mk_conj (t1' $ (Bound 0),t_unique))
				in
					term_to_prop_tree_subst t_ex1 (idx,subs) bsubs
				end
			| Const ("op =", _) $ t1 $ t2 =>
				let
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
					val fmTrue          = prop_tree_equal (tree1,tree2)
					val fmFalse         = SNot fmTrue
				in
					(Leaf [fmTrue, fmFalse], (i2,s2))
				end
			| Const ("op &", _) $ t1 $ t2 =>
				let
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
					val fmTrue          = SAnd (prop_tree_to_true tree1, prop_tree_to_true tree2)
					val fmFalse         = SOr (prop_tree_to_false tree1, prop_tree_to_false tree2)
				in
					(Leaf [fmTrue, fmFalse], (i2,s2))
				end
			| Const ("op |", _) $ t1 $ t2 =>
				let
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
					val fmTrue          = SOr (prop_tree_to_true tree1, prop_tree_to_true tree2)
					val fmFalse         = SAnd (prop_tree_to_false tree1, prop_tree_to_false tree2)
				in
					(Leaf [fmTrue, fmFalse], (i2,s2))
				end
			| Const ("op -->", _) $ t1 $ t2 =>
				let
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
					val fmTrue          = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
					val fmFalse         = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
				in
					(Leaf [fmTrue, fmFalse], (i2,s2))
				end
			(* set constants *)
			| Const ("Collect", _) $ t1 =>
				term_to_prop_tree_subst t1 (idx,subs) bsubs
			| Const ("op :", _) $ t1 $ t2 =>
				term_to_prop_tree_subst (t2 $ t1) (idx,subs) bsubs
			(* datatype constants *)
			| Const ("Product_Type.Unity", _) =>
				(Leaf [True], (idx,subs))
			(* unknown constants *)
			| Const (c, _) =>
				error ("term contains an unknown constant: '" ^ c ^ "'")
			(* abstractions *)
			| Abs (_,T,body) =>
				let
					val constants       = type_to_constants T us thy cdepth
					val (trees, substs) = split_list (map (fn c => term_to_prop_tree_subst body (idx,subs) (c::bsubs)) constants)
				in
					(* the substitutions in 'substs' are all identical *)
					(Node trees, hd substs)
				end
			(* (free/schematic) variables *)
			| Free _ =>
				variable_to_prop_tree_subst t' (idx,subs)
			| Var _ =>
				variable_to_prop_tree_subst t' (idx,subs)
			(* bound variables *)
			| Bound i =>
				if (length bsubs) <= i then
					raise REFUTE ("term_to_prop_tree_subst", "term contains a loose bound variable (with index " ^ (string_of_int i) ^ ")")
				else
					(nth_elem (i,bsubs), (idx,subs))
			(* application *)
			| t1 $ t2 =>
				let
					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
				in
					(prop_tree_apply (tree1,tree2), (i2,s2))
				end
	in
		term_to_prop_tree_subst t (1,[]) []
	end;

(* ------------------------------------------------------------------------- *)
(* term_to_prop_formula: translates a HOL formula 't' into a propositional   *)
(*      formula that is satisfiable if and only if 't' has a model of "size" *)
(*      'us' (where 'us' specifies the number of elements for each free type *)
(*      variable in 't') and maximal constructor depth 'cdepth'.             *)
(* ------------------------------------------------------------------------- *)

	(* TODO: shouldn't 'us' also specify the number of elements for schematic type variables? (if so, modify the comment above) *)

	(* Term.term -> (Term.typ * int) list -> theory -> int -> prop_formula * (int * (Term.term * prop_tree) list) *)

	fun term_to_prop_formula t us thy cdepth =
	let
		val (tr, (idx,subs)) = term_to_prop_tree t us thy cdepth
		val fm               = prop_tree_to_true tr
	in
		if subs=[] then
			(fm, (idx,subs))
		else
			(* make sure every tree that is substituted for a term describes a single element *)
			(SAnd (list_conjunction (map (fn (_,tr) => restrict_to_single_element tr) subs), fm), (idx,subs))
	end;


(* ------------------------------------------------------------------------- *)
(* INTERFACE, PART 2: FINDING A MODEL                                        *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* string_of_universe: prints a universe, i.e. an assignment of sizes for    *)
(*                     types                                                 *)
(* thy: the current theory                                                   *)
(* us : a list containing types together with their size                     *)
(* ------------------------------------------------------------------------- *)

	(* theory -> (Term.typ * int) list -> string *)

	fun string_of_universe thy [] =
		"empty universe (no type variables in term)"
	  | string_of_universe thy us =
		space_implode ", " (map (fn (T,i) => (Sign.string_of_typ (sign_of thy) T) ^ ": " ^ (string_of_int i)) us);

(* ------------------------------------------------------------------------- *)
(* string_of_model: prints a model, given by a substitution 'subs' of trees  *)
(*      of propositional variables and an assignment 'ass' of truth values   *)
(*      for these variables.                                                 *)
(* thy   : the current theory                                                *)
(* us    : universe, specifies the "size" of each type (i.e. type variable)  *)
(* cdepth: maximal constructor depth for inductive datatypes                 *)
(* subs  : substitution of trees of propositional formulas (for variables)   *)
(* ass   : assignment of truth values for boolean variables; see function    *)
(*         'truth_value' below for its meaning                               *)
(* ------------------------------------------------------------------------- *)

	(* theory -> (Term.typ * int) list -> int -> (Term.term * prop_formula tree) list -> int list -> string *)

	fun string_of_model thy us cdepth [] ass =
		"empty interpretation (no free variables in term)"
	  | string_of_model thy us cdepth subs ass =
		let
			(* Sign.sg *)
			val sg = sign_of thy
			(* int -> bool *)
			fun truth_value i =
				if i mem ass then true
				else if ~i mem ass then false
				else error ("SAT solver assignment does not specify a value for variable " ^ (string_of_int i))
			(* string -> string *)
			fun strip_leading_quote str =
				if nth_elem_string(0,str)="'" then
					String.substring (str, 1, size str - 1)
				else
					str;
			(* prop_formula list -> int *)
			fun true_index xs =
				(* returns the (0-based) index of the first true formula in xs *)
				let fun true_index_acc [] _ =
					raise REFUTE ("string_of_model::true_index", "no variable was set to true")
				      | true_index_acc (x::xs) n =
					case x of
					  BoolVar i =>
						if truth_value i then n else true_index_acc xs (n+1)
					| True =>
						n
					| False =>
						true_index_acc xs (n+1)
					| _ =>
						raise REFUTE ("string_of_model::true_index", "formula is not a boolean variable/true/false")
				in
					true_index_acc xs 0
				end
			(* Term.typ -> int -> prop_tree -> string *)
			(* prop *)
			fun string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
				if truth_value i then "true" else "false"
			  | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [True, False]) =
				"true"
			  | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [False, True]) =
				"false"
			(* bool *)
			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
				if truth_value i then "true" else "false"
			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [True, False]) =
				"true"
			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [False, True]) =
				"false"
			(* unit *)
			  | string_of_prop_tree (Type ("Product_Type.unit",[])) cdepth (Leaf [True]) =
				"()"
			  | string_of_prop_tree (Type (s,Ts)) cdepth (Leaf xs) =
				(case DatatypePackage.datatype_info thy s of
				   Some info => (* inductive datatype *)
					let
						val index               = #index info
						val descr               = #descr info
						val (_, dtyps, constrs) = the (assoc (descr, index))
						val Typs                = dtyps ~~ Ts
						(* string -> string *)
						fun unqualify s =
							implode (snd (take_suffix (fn c => c <> ".") (explode s)))
						(* DatatypeAux.dtyp -> Term.typ *)
						fun typ_of_dtyp (DatatypeAux.DtTFree a) =
							the (assoc (Typs, DatatypeAux.DtTFree a))
						  | typ_of_dtyp (DatatypeAux.DtRec i) =
							let
								val (s, ds, _) = the (assoc (descr, i))
							in
								Type (s, map typ_of_dtyp ds)
							end
						  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
							Type (s, map typ_of_dtyp ds)
						(* DatatypeAux.dtyp list -> int -> string *)
						fun string_of_inductive_type_cargs [] n =
							if n<>0 then
								raise REFUTE ("string_of_model", "internal error computing the element index for an inductive type")
							else
								""
						  | string_of_inductive_type_cargs (d::ds) n =
							let
								val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
							in
								" " ^ (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))
							end
						(* (string * DatatypeAux.dtyp list) list -> int -> string *)
						fun string_of_inductive_type_constrs [] n =
							raise REFUTE ("string_of_model", "inductive type has fewer elements than needed")
						  | string_of_inductive_type_constrs ((s,ds)::cs) n =
							let
								val size = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
							in
								if n < size then
									(unqualify s) ^ (string_of_inductive_type_cargs ds n)
								else
									string_of_inductive_type_constrs cs (n - size)
							end
					in
						string_of_inductive_type_constrs constrs (true_index xs)
					end
				 | None =>
					raise REFUTE ("string_of_model", "type contains an unknown type constructor: '" ^ s ^ "'"))
			(* type variable *)
			  | string_of_prop_tree (TFree (s,_)) cdepth (Leaf xs) =
					(strip_leading_quote s) ^ (string_of_int (true_index xs))
			  | string_of_prop_tree (TVar ((s,_),_)) cdepth (Leaf xs) =
					(strip_leading_quote s) ^ (string_of_int (true_index xs))
			(* function or set type *)
			  | string_of_prop_tree T cdepth (Node xs) =
				case T of
				  Type ("fun", [T1,T2]) =>
					let
						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)
					in
						"(" ^ (space_implode ", " strings) ^ ")"
					end
				| Type ("set", [T1]) =>
					let
						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)
					in
						"{" ^ (space_implode ", " strings) ^ "}"
					end
				| _ => raise REFUTE ("string_of_model::string_of_prop_tree", "not a function/set type")
			(* Term.term * prop_formula tree -> string *)
			fun string_of_term_assignment (t,tr) =
			let
				val T = case t of
					  Free (_,T) => T
					| Var (_,T)  => T
					| _          => raise REFUTE ("string_of_model::string_of_term_assignment", "term is not a (free or schematic) variable")
			in
				(Sign.string_of_term sg t) ^ " = " ^ (string_of_prop_tree T cdepth tr)
			end
		in
			space_implode "\n" (map string_of_term_assignment subs)
		end;

(* ------------------------------------------------------------------------- *)
(* find_model: repeatedly calls 'prop_formula_sat_solver' with appropriate   *)
(*             parameters, and displays the results to the user              *)
(* params    : list of '(name, value)' pairs used to override default        *)
(*             parameters                                                    *)
(*                                                                           *)
(* This is a brief description of the algorithm implemented:                 *)
(*                                                                           *)
(* 1. Let k = max ('minsize',1).                                             *)
(* 2. Let the universe have k elements.  Find all possible partitions of     *)
(*    these elements into the basic types occuring in 't' such that no basic *)
(*    type is empty.                                                         *)
(* 3. Translate 't' into a propositional formula p s.t. 't' has a model wrt. *)
(*    the partition chosen in step (2.) if (actually, if and only if) p is   *)
(*    satisfiable.  To do this, replace quantification by conjunction/       *)
(*    disjunction over all elements of the type being quantified over.  (If  *)
(*    p contains more than 'maxvars' boolean variables, terminate.)          *)
(* 4. Serialize p to a file, and try to find a satisfying assignment for p   *)
(*    by invoking an external SAT solver.                                    *)
(* 5. If the SAT solver finds a satisfying assignment for p, translate this  *)
(*    assignment back into a model for 't'.  Present this model to the user, *)
(*    then terminate.                                                        *)
(* 6. As long as there is another partition left, pick it and go back to     *)
(*    step (3.).                                                             *)
(* 7. Increase k by 1.  As long as k does not exceed 'maxsize', go back to   *)
(*    step (2.).                                                             *)
(*                                                                           *)
(* The following parameters are currently supported (and required!):         *)
(*                                                                           *)
(* Name          Type    Description                                         *)
(*                                                                           *)
(* "minsize"     int     Only search for models with size at least           *)
(*                       'minsize'.                                          *)
(* "maxsize"     int     If >0, only search for models with size at most     *)
(*                       'maxsize'.                                          *)
(* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
(*                       when transforming the term into a propositional     *)
(*                       formula.                                            *)
(* "satfile"     string  Name of the file used to store the propositional    *)
(*                       formula, i.e. the input to the SAT solver.          *)
(* "satformat"   string  Format of the SAT solver's input file.  Must be     *)
(*                       either "cnf", "defcnf", or "sat".  Since "sat" is   *)
(*                       not supported by most SAT solvers, and "cnf" can    *)
(*                       cause exponential blowup of the formula, "defcnf"   *)
(*                       is recommended.                                     *)
(* "resultfile"  string  Name of the file containing the SAT solver's        *)
(*                       output.                                             *)
(* "success"     string  Part of the line in the SAT solver's output that    *)
(*                       precedes a list of integers representing the        *)
(*                       satisfying assignment.                              *)
(* "command"     string  System command used to execute the SAT solver.      *)
(*                       Note that you if you change 'satfile' or            *)
(*                       'resultfile', you will also need to change          *)
(*                       'command'.                                          *)
(*                                                                           *)
(* See the Isabelle/Isar theory 'Refute.thy' for reasonable default values.  *)
(* ------------------------------------------------------------------------- *)

	(* theory -> (string * string) list -> Term.term -> unit *)

	fun find_model thy params t =
	let
		(* (string * string) list * (string * string) list -> (string * string) list *)
		fun add_params (parms, []) =
			parms
		  | add_params (parms, defparm::defparms) =
			add_params (gen_ins (fn (a, b) => (fst a) = (fst b)) (defparm, parms), defparms)
		(* (string * string) list * string -> int *)
		fun read_int (parms, name) =
			case assoc_string (parms, name) of
			  Some s => (case Int.fromString s of
				  SOME i => i
				| NONE   => error ("parameter '" ^ name ^ "' (value is '" ^ s ^ "') must be an integer value"))
			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")
		(* (string * string) list * string -> string *)
		fun read_string (parms, name) =
			case assoc_string (parms, name) of
			  Some s => s
			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")
		(* (string * string) list *)
		val allparams  = add_params (params, get_default_params thy)
		(* int *)
		val minsize    = read_int (allparams, "minsize")
		val maxsize    = read_int (allparams, "maxsize")
		val maxvars    = read_int (allparams, "maxvars")
		(* string *)
		val satfile    = read_string (allparams, "satfile")
		val satformat  = read_string (allparams, "satformat")
		val resultfile = read_string (allparams, "resultfile")
		val success    = read_string (allparams, "success")
		val command    = read_string (allparams, "command")
		(* misc *)
		val satpath    = Path.unpack satfile
		val resultpath = Path.unpack resultfile
		val sg         = sign_of thy
		(* Term.typ list *)
		val tvars      = map (fn (i,s) => TVar(i,s)) (term_tvars t)
		val tfrees     = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
		(* universe -> int -> bool *)
		fun find_model_universe u cdepth =
			let
				(* given the universe 'u' and constructor depth 'cdepth', translate *)
        	                (* the term 't' into a propositional formula 'fm'                   *)
				val (fm,(idx,subs)) = term_to_prop_formula t u thy cdepth
				val usedvars        = idx-1
			in
				(* 'maxvars=0' means "use as many variables as necessary" *)
				if usedvars>maxvars andalso maxvars<>0 then
					(
						(* too many variables used: terminate *)
						writeln ("\nSearch terminated: " ^ (string_of_int usedvars) ^ " boolean variables used (only " ^ (string_of_int maxvars) ^ " allowed).");
						true
					)
				else
					(* pass the formula 'fm' to an external SAT solver *)
					case prop_formula_sat_solver fm satpath satformat resultpath success command of
					  None =>
						(* no model found *)
						false
					| Some assignment =>
						(* model found: terminate *)
						(
							writeln ("\nModel found:\n" ^ (string_of_universe thy u) ^ "\n" ^ (string_of_model thy u cdepth subs assignment));
							true
						)
			end
		(* universe list -> int -> bool *)
		fun find_model_universes [] cdepth =
			(
				std_output "\n";
				false
			)
		  | find_model_universes (u::us) cdepth =
			(
				std_output ".";
				((if find_model_universe u cdepth then
					(* terminate *)
					true
				else
					(* continue search with the next universe *)
					find_model_universes us cdepth)
				handle EMPTY_DATATYPE => (std_output "[empty inductive type (constructor depth too small)]\n"; false))
			)
		(* int * int -> unit *)
		fun find_model_from_to (min,max) =
			(* 'max=0' means "search for arbitrary large models" *)
			if min>max andalso max<>0 then
				writeln ("Search terminated: no model found.")
			else
			(
				std_output ("Searching for a model of size " ^ (string_of_int min));
				if find_model_universes (make_universes tfrees min) min then
					(* terminate *)
					()
				else
					(* continue search with increased size *)
					find_model_from_to (min+1, max)
			)
	in
		writeln ("Trying to find a model of: " ^ (Sign.string_of_term sg t));
		if tvars<>[] then
			(* TODO: deal with schematic type variables in a better way, if possible *)
			error "term contains schematic type variables"
		else
		(
			if minsize<1 then
				writeln ("'minsize' is less than 1; starting search with size 1.")
			else
				();
			if maxsize<max (minsize,1) andalso maxsize<>0 then
				writeln ("'maxsize' is less than 'minsize': no model found.")
			else
				find_model_from_to (max (minsize,1), maxsize)
		)
	end;

(* ------------------------------------------------------------------------- *)
(* refute_term: calls 'find_model' on the negation of a term                 *)
(* params     : list of '(name, value)' pairs used to override default       *)
(*              parameters                                                   *)
(* ------------------------------------------------------------------------- *)

	(* theory -> (string * string) list -> Term.term -> unit *)

	fun refute_term thy params t =
	let
		(* TODO: schematic type variables? *)
		val negation = close_vars (HOLogic.Not $ t)
		(* If 't' is of type 'propT' (rather than 'boolT'), applying *)
		(* 'HOLogic.Not' is not type-correct.  However, this isn't   *)
		(* really a problem as long as 'find_model' still interprets *)
		(* the resulting term correctly, without checking its type.  *)
	in
		find_model thy params negation
	end;

(* ------------------------------------------------------------------------- *)
(* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)
(* params        : list of '(name, value)' pairs used to override default    *)
(*                 parameters                                                *)
(* subgoal       : 0-based index specifying the subgoal number               *)
(* ------------------------------------------------------------------------- *)

	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)

	fun refute_subgoal thy params thm subgoal =
		refute_term thy params (nth_elem (subgoal, prems_of thm));

end