Adding 'refute' to HOL.
authorwebertj
Sat Jan 10 13:35:10 2004 +0100 (2004-01-10)
changeset 1435041b32020d0b3
parent 14349 8d92e426eb38
child 14351 cd3ef10d02be
Adding 'refute' to HOL.
src/HOL/IsaMakefile
src/HOL/Main.thy
src/HOL/Refute.thy
src/HOL/Tools/refute.ML
src/HOL/Tools/refute_isar.ML
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/HOL/IsaMakefile	Sat Jan 10 12:34:50 2004 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Sat Jan 10 13:35:10 2004 +0100
     1.3 @@ -93,7 +93,8 @@
     1.4    Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
     1.5    Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
     1.6    Nat.thy NatArith.ML NatArith.thy Numeral.thy \
     1.7 -  Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML \
     1.8 +  Power.thy PreList.thy Product_Type.ML Product_Type.thy \
     1.9 +  Refute.thy ROOT.ML \
    1.10    Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
    1.11    Relation_Power.thy Ring_and_Field.thy\
    1.12    Set.ML Set.thy SetInterval.ML SetInterval.thy \
    1.13 @@ -103,7 +104,9 @@
    1.14    Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \
    1.15    Tools/meson.ML Tools/numeral_syntax.ML \
    1.16    Tools/primrec_package.ML Tools/recdef_package.ML Tools/recfun_codegen.ML \
    1.17 -  Tools/record_package.ML Tools/rewrite_hol_proof.ML \
    1.18 +  Tools/record_package.ML \
    1.19 +  Tools/refute.ML Tools/refute_isar.ML \
    1.20 +  Tools/rewrite_hol_proof.ML \
    1.21    Tools/specification_package.ML \
    1.22    Tools/split_rule.ML Tools/typedef_package.ML \
    1.23    Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
    1.24 @@ -588,6 +591,7 @@
    1.25    ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
    1.26    ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy ex/Puzzle.thy \
    1.27    ex/Qsort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
    1.28 +  ex/Refute_Examples.thy \
    1.29    ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
    1.30    ex/Tarski.thy ex/Tuple.thy ex/Classical.thy \
    1.31    ex/mesontest2.ML ex/mesontest2.thy ex/set.thy ex/svc_funcs.ML \
     2.1 --- a/src/HOL/Main.thy	Sat Jan 10 12:34:50 2004 +0100
     2.2 +++ b/src/HOL/Main.thy	Sat Jan 10 13:35:10 2004 +0100
     2.3 @@ -1,12 +1,12 @@
     2.4  (*  Title:      HOL/Main.thy
     2.5      ID:         $Id$
     2.6 -    Author:     Stefan Berghofer, Tobias Nipkow and Markus Wenzel, TU Muenchen
     2.7 +    Author:     Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen)
     2.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.9  *)
    2.10  
    2.11  header {* Main HOL *}
    2.12  
    2.13 -theory Main = Map + Hilbert_Choice + Extraction:
    2.14 +theory Main = Map + Hilbert_Choice + Extraction + Refute:
    2.15  
    2.16  text {*
    2.17    Theory @{text Main} includes everything.  Note that theory @{text
    2.18 @@ -91,4 +91,26 @@
    2.19  lemma [code]: "(0 < Suc n) = True" by simp
    2.20  lemmas [code] = Suc_less_eq imp_conv_disj
    2.21  
    2.22 +subsection {* Configuration of the 'refute' command *}
    2.23 +
    2.24 +text {*
    2.25 +  The following are reasonable default parameters (for use with
    2.26 +  ZChaff 2003.12.04).  For an explanation of these parameters,
    2.27 +  see 'HOL/Refute.thy'.
    2.28 +
    2.29 +  \emph{Note}: If you want to use a different SAT solver (or
    2.30 +  install ZChaff to a different location), you will need to
    2.31 +  override at least the values for 'command' and (probably)
    2.32 +  'success' in your own theory file.
    2.33 +*}
    2.34 +
    2.35 +refute_params [minsize=1,
    2.36 +               maxsize=8,
    2.37 +               maxvars=200,
    2.38 +               satfile="refute.cnf",
    2.39 +               satformat="defcnf",
    2.40 +               resultfile="refute.out",
    2.41 +               success="Verify Solution successful. Instance satisfiable",
    2.42 +               command="$HOME/bin/zchaff refute.cnf 60 > refute.out"]
    2.43 +
    2.44  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Refute.thy	Sat Jan 10 13:35:10 2004 +0100
     3.3 @@ -0,0 +1,116 @@
     3.4 +(*  Title:      HOL/Refute.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tjark Weber
     3.7 +    Copyright   2003-2004
     3.8 +
     3.9 +Basic setup and documentation for the 'refute' (and 'refute_params') command.
    3.10 +*)
    3.11 +
    3.12 +(* ------------------------------------------------------------------------- *)
    3.13 +(* REFUTE                                                                    *)
    3.14 +(*                                                                           *)
    3.15 +(* We use a SAT solver to search for a (finite) model that refutes a given   *)
    3.16 +(* HOL formula.                                                              *)
    3.17 +(* ------------------------------------------------------------------------- *)
    3.18 +
    3.19 +(* ------------------------------------------------------------------------- *)
    3.20 +(* INSTALLATION                                                              *)
    3.21 +(*                                                                           *)
    3.22 +(* 1. Install a stand-alone SAT solver.  The default parameters in           *)
    3.23 +(*    'HOL/Main.thy' assume that ZChaff 2003.12.04 (available for Solaris/   *)
    3.24 +(*    Linux/Cygwin/Windows at http://ee.princeton.edu/~chaff/zchaff.php) is  *)
    3.25 +(*    installed as '$HOME/bin/zchaff'.  If you want to use a different SAT   *)
    3.26 +(*    solver (or install ZChaff to a different location), you will need to   *)
    3.27 +(*    modify at least the values for 'command' and (probably) 'success'.     *)
    3.28 +(*                                                                           *)
    3.29 +(* 2. That's it. You can now use the 'refute' command in your own theories.  *)
    3.30 +(* ------------------------------------------------------------------------- *)
    3.31 +
    3.32 +(* ------------------------------------------------------------------------- *)
    3.33 +(* USAGE                                                                     *)
    3.34 +(*                                                                           *)
    3.35 +(* See the file 'HOL/ex/Refute_Examples.thy' for examples.  The supported    *)
    3.36 +(* parameters are explained below.                                           *)
    3.37 +(* ------------------------------------------------------------------------- *)
    3.38 +
    3.39 +(* ------------------------------------------------------------------------- *)
    3.40 +(* CURRENT LIMITATIONS                                                       *)
    3.41 +(*                                                                           *)
    3.42 +(* 'refute' currently accepts formulas of higher-order predicate logic (with *)
    3.43 +(* equality), including free/bound/schematic variables, lambda abstractions, *)
    3.44 +(* sets and set membership.                                                  *)
    3.45 +(*                                                                           *)
    3.46 +(* NOT (YET) SUPPORTED ARE                                                   *)
    3.47 +(*                                                                           *)
    3.48 +(* - schematic type variables                                                *)
    3.49 +(* - type constructors other than =>, set, unit, and inductive datatypes     *)
    3.50 +(* - constants, including constructors of inductive datatypes and recursive  *)
    3.51 +(*   functions on inductive datatypes                                        *)
    3.52 +(*                                                                           *)
    3.53 +(* Unfolding of constants currently needs to be done manually, e.g. using    *)
    3.54 +(* 'apply (unfold xxx_def)'.                                                 *)
    3.55 +(*                                                                           *)
    3.56 +(* For formulas that contain (variables of) an inductive datatype, a         *)
    3.57 +(* spurious countermodel may be returned.  Currently no warning is issued in *)
    3.58 +(* this case.                                                                *)
    3.59 +(* ------------------------------------------------------------------------- *)
    3.60 +
    3.61 +(* ------------------------------------------------------------------------- *)
    3.62 +(* PARAMETERS                                                                *)
    3.63 +(*                                                                           *)
    3.64 +(* The following global parameters are currently supported (and required):   *)
    3.65 +(*                                                                           *)
    3.66 +(* Name          Type    Description                                         *)
    3.67 +(*                                                                           *)
    3.68 +(* "minsize"     int     Only search for models with size at least           *)
    3.69 +(*                       'minsize'.                                          *)
    3.70 +(* "maxsize"     int     If >0, only search for models with size at most     *)
    3.71 +(*                       'maxsize'.                                          *)
    3.72 +(* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
    3.73 +(*                       when transforming the term into a propositional     *)
    3.74 +(*                       formula.                                            *)
    3.75 +(* "satfile"     string  Name of the file used to store the propositional    *)
    3.76 +(*                       formula, i.e. the input to the SAT solver.          *)
    3.77 +(* "satformat"   string  Format of the SAT solver's input file.  Must be     *)
    3.78 +(*                       either "cnf", "defcnf", or "sat".  Since "sat" is   *)
    3.79 +(*                       not supported by most SAT solvers, and "cnf" can    *)
    3.80 +(*                       cause exponential blowup of the formula, "defcnf"   *)
    3.81 +(*                       is recommended.                                     *)
    3.82 +(* "resultfile"  string  Name of the file containing the SAT solver's        *)
    3.83 +(*                       output.                                             *)
    3.84 +(* "success"     string  Part of the line in the SAT solver's output that    *)
    3.85 +(*                       precedes a list of integers representing the        *)
    3.86 +(*                       satisfying assignment.                              *)
    3.87 +(* "command"     string  System command used to execute the SAT solver.      *)
    3.88 +(*                       Note that you if you change 'satfile' or            *)
    3.89 +(*                       'resultfile', you will also need to change          *)
    3.90 +(*                       'command'.                                          *)
    3.91 +(* ------------------------------------------------------------------------- *)
    3.92 +
    3.93 +(* ------------------------------------------------------------------------- *)
    3.94 +(* FILES                                                                     *)
    3.95 +(*                                                                           *)
    3.96 +(* HOL/Tools/refute.ML        Implementation of the algorithm.               *)
    3.97 +(* HOL/Tools/refute_isar.ML   Adds 'refute'/'refute_params' to Isabelle's    *)
    3.98 +(*                            syntax.                                        *)
    3.99 +(* HOL/Refute.thy             This file. Loads the ML files, basic setup,    *)
   3.100 +(*                            documentation.                                 *)
   3.101 +(* HOL/Main.thy               Sets default parameters.                       *)
   3.102 +(* HOL/ex/RefuteExamples.thy  Examples.                                      *)
   3.103 +(* ------------------------------------------------------------------------- *)
   3.104 +
   3.105 +header {* Refute *}
   3.106 +
   3.107 +theory Refute = Map
   3.108 +
   3.109 +files "Tools/refute.ML"
   3.110 +      "Tools/refute_isar.ML":
   3.111 +
   3.112 +(* Setting up the 'refute' and 'refute\_params' commands *)
   3.113 +
   3.114 +use "Tools/refute.ML"
   3.115 +use "Tools/refute_isar.ML"
   3.116 +
   3.117 +setup Refute.setup
   3.118 +
   3.119 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/refute.ML	Sat Jan 10 13:35:10 2004 +0100
     4.3 @@ -0,0 +1,1648 @@
     4.4 +(*  Title:      HOL/Tools/refute.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tjark Weber
     4.7 +    Copyright   2003-2004
     4.8 +
     4.9 +Finite model generation for HOL formulae, using an external SAT solver.
    4.10 +*)
    4.11 +
    4.12 +(* ------------------------------------------------------------------------- *)
    4.13 +(* Declares the 'REFUTE' signature as well as a structure 'Refute'.  See     *)
    4.14 +(* 'find_model' below for a description of the implemented algorithm, and    *)
    4.15 +(* the Isabelle/Isar theories 'HOL/Refute.thy' and 'HOL/Main.thy' on how to  *)
    4.16 +(* set things up.                                                            *)
    4.17 +(* ------------------------------------------------------------------------- *)
    4.18 +
    4.19 +signature REFUTE =
    4.20 +sig
    4.21 +
    4.22 +	(* We use 'REFUTE' only for internal error conditions that should    *)
    4.23 +	(* never occur in the first place (i.e. errors caused by bugs in our *)
    4.24 +	(* code).  Otherwise (e.g. to indicate invalid input data) we use    *)
    4.25 +	(* 'error'.                                                          *)
    4.26 +
    4.27 +	exception REFUTE of string * string;	(* ("in function", "cause") *)
    4.28 +
    4.29 +	val setup : (theory -> theory) list
    4.30 +
    4.31 +	val set_default_param : (string * string) -> theory -> theory
    4.32 +	val get_default_param : theory -> string -> string option
    4.33 +	val get_default_params : theory -> (string * string) list
    4.34 +
    4.35 +	val find_model : theory -> (string * string) list -> Term.term -> unit
    4.36 +
    4.37 +	val refute_term : theory -> (string * string) list -> Term.term -> unit
    4.38 +	val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
    4.39 +end;
    4.40 +
    4.41 +
    4.42 +structure Refute : REFUTE =
    4.43 +struct
    4.44 +	exception REFUTE of string * string;
    4.45 +
    4.46 +	exception EMPTY_DATATYPE;
    4.47 +
    4.48 +	structure RefuteDataArgs =
    4.49 +	struct
    4.50 +		val name = "Refute/refute";
    4.51 +		type T = string Symtab.table;
    4.52 +		val empty = Symtab.empty;
    4.53 +		val copy = I;
    4.54 +		val prep_ext = I;
    4.55 +		val merge =
    4.56 +			fn (symTable1, symTable2) =>
    4.57 +				(Symtab.merge (op =) (symTable1, symTable2));
    4.58 +		fun print sg symTable =
    4.59 +			writeln
    4.60 +				("'refute', default parameters:\n" ^
    4.61 +				(space_implode "\n" (map (fn (name,value) => name ^ " = " ^ value) (Symtab.dest symTable))))
    4.62 +	end;
    4.63 +
    4.64 +	structure RefuteData = TheoryDataFun(RefuteDataArgs);
    4.65 +
    4.66 +
    4.67 +(* ------------------------------------------------------------------------- *)
    4.68 +(* INTERFACE, PART 1: INITIALIZATION, PARAMETER MANAGEMENT                   *)
    4.69 +(* ------------------------------------------------------------------------- *)
    4.70 +
    4.71 +(* ------------------------------------------------------------------------- *)
    4.72 +(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
    4.73 +(* structure                                                                 *)
    4.74 +(* ------------------------------------------------------------------------- *)
    4.75 +
    4.76 +	val setup = [RefuteData.init];
    4.77 +
    4.78 +(* ------------------------------------------------------------------------- *)
    4.79 +(* set_default_param: stores the '(name, value)' pair in RefuteData's symbol *)
    4.80 +(*                    table                                                  *)
    4.81 +(* ------------------------------------------------------------------------- *)
    4.82 +
    4.83 +	fun set_default_param (name, value) thy =
    4.84 +	let
    4.85 +		val symTable = RefuteData.get thy
    4.86 +	in
    4.87 +		case Symtab.lookup (symTable, name) of
    4.88 +			None   => RefuteData.put (Symtab.extend (symTable, [(name, value)])) thy
    4.89 +		|	Some _ => RefuteData.put (Symtab.update ((name, value), symTable)) thy
    4.90 +	end;
    4.91 +
    4.92 +(* ------------------------------------------------------------------------- *)
    4.93 +(* get_default_param: retrieves the value associated with 'name' from        *)
    4.94 +(*                    RefuteData's symbol table                              *)
    4.95 +(* ------------------------------------------------------------------------- *)
    4.96 +
    4.97 +	fun get_default_param thy name = Symtab.lookup (RefuteData.get thy, name);
    4.98 +
    4.99 +(* ------------------------------------------------------------------------- *)
   4.100 +(* get_default_params: returns a list of all '(name, value)' pairs that are  *)
   4.101 +(*                     stored in RefuteData's symbol table                   *)
   4.102 +(* ------------------------------------------------------------------------- *)
   4.103 +
   4.104 +	fun get_default_params thy = Symtab.dest (RefuteData.get thy);
   4.105 +
   4.106 +
   4.107 +(* ------------------------------------------------------------------------- *)
   4.108 +(* PROPOSITIONAL FORMULAS                                                    *)
   4.109 +(* ------------------------------------------------------------------------- *)
   4.110 +
   4.111 +(* ------------------------------------------------------------------------- *)
   4.112 +(* prop_formula: formulas of propositional logic, built from boolean         *)
   4.113 +(*               variables (referred to by index) and True/False using       *)
   4.114 +(*               not/or/and                                                  *)
   4.115 +(* ------------------------------------------------------------------------- *)
   4.116 +
   4.117 +	datatype prop_formula =
   4.118 +		  True
   4.119 +		| False
   4.120 +		| BoolVar of int
   4.121 +		| Not of prop_formula
   4.122 +		| Or of prop_formula * prop_formula
   4.123 +		| And of prop_formula * prop_formula;
   4.124 +
   4.125 +	(* the following constructor functions make sure that True and False do *)
   4.126 +	(* not occur within any of the other connectives (i.e. Not, Or, And)    *)
   4.127 +
   4.128 +	(* prop_formula -> prop_formula *)
   4.129 +
   4.130 +	fun SNot True  = False
   4.131 +	  | SNot False = True
   4.132 +	  | SNot fm    = Not fm;
   4.133 +
   4.134 +	(* prop_formula * prop_formula -> prop_formula *)
   4.135 +
   4.136 +	fun SOr (True, _)   = True
   4.137 +	  | SOr (_, True)   = True
   4.138 +	  | SOr (False, fm) = fm
   4.139 +	  | SOr (fm, False) = fm
   4.140 +	  | SOr (fm1, fm2)  = Or (fm1, fm2);
   4.141 +
   4.142 +	(* prop_formula * prop_formula -> prop_formula *)
   4.143 +
   4.144 +	fun SAnd (True, fm) = fm
   4.145 +	  | SAnd (fm, True) = fm
   4.146 +	  | SAnd (False, _) = False
   4.147 +	  | SAnd (_, False) = False
   4.148 +	  | SAnd (fm1, fm2) = And (fm1, fm2);
   4.149 +
   4.150 +(* ------------------------------------------------------------------------- *)
   4.151 +(* list_disjunction: computes the disjunction of a list of propositional     *)
   4.152 +(*                   formulas                                                *)
   4.153 +(* ------------------------------------------------------------------------- *)
   4.154 +
   4.155 +	(* prop_formula list -> prop_formula *)
   4.156 +
   4.157 +	fun list_disjunction []      = False
   4.158 +	  | list_disjunction (x::xs) = SOr (x, list_disjunction xs);
   4.159 +
   4.160 +(* ------------------------------------------------------------------------- *)
   4.161 +(* list_conjunction: computes the conjunction of a list of propositional     *)
   4.162 +(*                   formulas                                                *)
   4.163 +(* ------------------------------------------------------------------------- *)
   4.164 +
   4.165 +	(* prop_formula list -> prop_formula *)
   4.166 +
   4.167 +	fun list_conjunction []      = True
   4.168 +	  | list_conjunction (x::xs) = SAnd (x, list_conjunction xs);
   4.169 +
   4.170 +(* ------------------------------------------------------------------------- *)
   4.171 +(* prop_formula_dot_product: [x1,...,xn] * [y1,...,yn] -> x1*y1+...+xn*yn    *)
   4.172 +(* ------------------------------------------------------------------------- *)
   4.173 +
   4.174 +	(* prop_formula list * prop_formula list -> prop_formula *)
   4.175 +
   4.176 +	fun prop_formula_dot_product ([],[])       = False
   4.177 +	  | prop_formula_dot_product (x::xs,y::ys) = SOr (SAnd (x,y), prop_formula_dot_product (xs,ys))
   4.178 +	  | prop_formula_dot_product (_,_)         = raise REFUTE ("prop_formula_dot_product", "lists are of different length");
   4.179 +
   4.180 +(* ------------------------------------------------------------------------- *)
   4.181 +(* prop_formula_to_nnf: computes the negation normal form of a formula 'fm'  *)
   4.182 +(*                      of propositional logic (i.e. only variables may be   *)
   4.183 +(*                      negated, but not subformulas)                        *)
   4.184 +(* ------------------------------------------------------------------------- *)
   4.185 +
   4.186 +	(* prop_formula -> prop_formula *)
   4.187 +
   4.188 +	fun prop_formula_to_nnf fm =
   4.189 +		case fm of
   4.190 +		(* constants *)
   4.191 +		  True                => True
   4.192 +		| False               => False
   4.193 +		(* literals *)
   4.194 +		| BoolVar i           => BoolVar i
   4.195 +		| Not (BoolVar i)     => Not (BoolVar i)
   4.196 +		(* double-negation elimination *)
   4.197 +		| Not (Not fm)        => prop_formula_to_nnf fm
   4.198 +		(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
   4.199 +		| Not (Or  (fm1,fm2)) => SAnd (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
   4.200 +		| Not (And (fm1,fm2)) => SOr  (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
   4.201 +		(* 'or' and 'and' as outermost connectives are left untouched *)
   4.202 +		| Or  (fm1,fm2)       => SOr  (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
   4.203 +		| And (fm1,fm2)       => SAnd (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
   4.204 +		(* 'not' + constant *)
   4.205 +		| Not _               => raise REFUTE ("prop_formula_to_nnf", "'True'/'False' not allowed inside of 'Not'");
   4.206 +
   4.207 +(* ------------------------------------------------------------------------- *)
   4.208 +(* prop_formula_nnf_to_cnf: computes the conjunctive normal form of a        *)
   4.209 +(*      formula 'fm' of propositional logic that is given in negation normal *)
   4.210 +(*      form.  Note that there may occur an exponential blowup of the        *)
   4.211 +(*      formula.                                                             *)
   4.212 +(* ------------------------------------------------------------------------- *)
   4.213 +
   4.214 +	(* prop_formula -> prop_formula *)
   4.215 +
   4.216 +	fun prop_formula_nnf_to_cnf fm =
   4.217 +		case fm of
   4.218 +		(* constants *)
   4.219 +		  True            => True
   4.220 +		| False           => False
   4.221 +		(* literals *)
   4.222 +		| BoolVar i       => BoolVar i
   4.223 +		| Not (BoolVar i) => Not (BoolVar i)
   4.224 +		(* pushing 'or' inside of 'and' using distributive laws *)
   4.225 +		| Or (fm1,fm2)    =>
   4.226 +			let
   4.227 +				val fm1' = prop_formula_nnf_to_cnf fm1
   4.228 +				val fm2' = prop_formula_nnf_to_cnf fm2
   4.229 +			in
   4.230 +				case fm1' of
   4.231 +				  And (fm11,fm12) => prop_formula_nnf_to_cnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2')))
   4.232 +				| _               =>
   4.233 +					(case fm2' of
   4.234 +					  And (fm21,fm22) => prop_formula_nnf_to_cnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22)))
   4.235 +					(* neither subformula contains 'and' *)
   4.236 +					| _               => fm)
   4.237 +			end
   4.238 +		(* 'and' as outermost connective is left untouched *)
   4.239 +		| And (fm1,fm2)   => SAnd (prop_formula_nnf_to_cnf fm1, prop_formula_nnf_to_cnf fm2)
   4.240 +		(* error *)
   4.241 +		| _               => raise REFUTE ("prop_formula_nnf_to_cnf", "formula is not in negation normal form");
   4.242 +
   4.243 +(* ------------------------------------------------------------------------- *)
   4.244 +(* max: computes the maximum of two integer values 'i' and 'j'               *)
   4.245 +(* ------------------------------------------------------------------------- *)
   4.246 +
   4.247 +	(* int * int -> int *)
   4.248 +
   4.249 +	fun max (i,j) =
   4.250 +		if (i>j) then i else j;
   4.251 +
   4.252 +(* ------------------------------------------------------------------------- *)
   4.253 +(* max_var_index: computes the maximal variable index occuring in 'fm',      *)
   4.254 +(*      where 'fm' is a formula of propositional logic                       *)
   4.255 +(* ------------------------------------------------------------------------- *)
   4.256 +
   4.257 +	(* prop_formula -> int *)
   4.258 +
   4.259 +	fun max_var_index fm =
   4.260 +		case fm of
   4.261 +		  True          => 0
   4.262 +		| False         => 0
   4.263 +		| BoolVar i     => i
   4.264 +		| Not fm1       => max_var_index fm1
   4.265 +		| And (fm1,fm2) => max (max_var_index fm1, max_var_index fm2)
   4.266 +		| Or (fm1,fm2)  => max (max_var_index fm1, max_var_index fm2);
   4.267 +
   4.268 +(* ------------------------------------------------------------------------- *)
   4.269 +(* prop_formula_nnf_to_def_cnf: computes the definitional conjunctive normal *)
   4.270 +(*      form of a formula 'fm' of propositional logic that is given in       *)
   4.271 +(*      negation normal form.  To avoid an exponential blowup of the         *)
   4.272 +(*      formula, auxiliary variables may be introduced.  The result formula  *)
   4.273 +(*      is SAT-equivalent to 'fm' (i.e. it is satisfiable if and only if     *)
   4.274 +(*      'fm' is satisfiable).                                                *)
   4.275 +(* ------------------------------------------------------------------------- *)
   4.276 +
   4.277 +	(* prop_formula -> prop_formula *)
   4.278 +
   4.279 +	fun prop_formula_nnf_to_def_cnf fm =
   4.280 +	let
   4.281 +		(* prop_formula * int -> prop_formula * int *)
   4.282 +		fun prop_formula_nnf_to_def_cnf_new (fm,new) =
   4.283 +		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
   4.284 +			case fm of
   4.285 +			(* constants *)
   4.286 +			  True            => (True, new)
   4.287 +			| False           => (False, new)
   4.288 +			(* literals *)
   4.289 +			| BoolVar i       => (BoolVar i, new)
   4.290 +			| Not (BoolVar i) => (Not (BoolVar i), new)
   4.291 +			(* pushing 'or' inside of 'and' using distributive laws *)
   4.292 +			| Or (fm1,fm2)    =>
   4.293 +				let
   4.294 +					val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
   4.295 +					val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
   4.296 +				in
   4.297 +					case fst fm1' of
   4.298 +					  And (fm11,fm12) =>
   4.299 +						let
   4.300 +							val aux = BoolVar (snd fm2')
   4.301 +						in
   4.302 +							(* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *)
   4.303 +							prop_formula_nnf_to_def_cnf_new (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fst fm2', Not aux)), (snd fm2')+1)
   4.304 +						end
   4.305 +					| _               =>
   4.306 +						(case fst fm2' of
   4.307 +						  And (fm21,fm22) =>
   4.308 +							let
   4.309 +								val aux = BoolVar (snd fm2')
   4.310 +							in
   4.311 +								(* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *)
   4.312 +								prop_formula_nnf_to_def_cnf_new (SAnd (SOr (fst fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), (snd fm2')+1)
   4.313 +							end
   4.314 +						(* neither subformula contains 'and' *)
   4.315 +						| _               => (fm, new))
   4.316 +				end
   4.317 +			(* 'and' as outermost connective is left untouched *)
   4.318 +			| And (fm1,fm2)   =>
   4.319 +				let
   4.320 +					val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
   4.321 +					val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
   4.322 +				in
   4.323 +					(SAnd (fst fm1', fst fm2'), snd fm2')
   4.324 +				end
   4.325 +			(* error *)
   4.326 +			| _               => raise REFUTE ("prop_formula_nnf_to_def_cnf", "formula is not in negation normal form")
   4.327 +	in
   4.328 +		fst (prop_formula_nnf_to_def_cnf_new (fm, (max_var_index fm)+1))
   4.329 +	end;
   4.330 +
   4.331 +(* ------------------------------------------------------------------------- *)
   4.332 +(* prop_formula_to_cnf: computes the conjunctive normal form of a formula    *)
   4.333 +(*                      'fm' of propositional logic                          *)
   4.334 +(* ------------------------------------------------------------------------- *)
   4.335 +
   4.336 +	(* prop_formula -> prop_formula *)
   4.337 +
   4.338 +	fun prop_formula_to_cnf fm =
   4.339 +		prop_formula_nnf_to_cnf (prop_formula_to_nnf fm);
   4.340 +
   4.341 +(* ------------------------------------------------------------------------- *)
   4.342 +(* prop_formula_to_def_cnf: computes the definitional conjunctive normal     *)
   4.343 +(*      form of a formula 'fm' of propositional logic, introducing auxiliary *)
   4.344 +(*      variables if necessary to avoid an exponential blowup of the formula *)
   4.345 +(* ------------------------------------------------------------------------- *)
   4.346 +
   4.347 +	(* prop_formula -> prop_formula *)
   4.348 +
   4.349 +	fun prop_formula_to_def_cnf fm =
   4.350 +		prop_formula_nnf_to_def_cnf (prop_formula_to_nnf fm);
   4.351 +
   4.352 +(* ------------------------------------------------------------------------- *)
   4.353 +(* prop_formula_to_dimacs_cnf_format: serializes a formula of propositional  *)
   4.354 +(*      logic to a file in DIMACS CNF format (see "Satisfiability Suggested  *)
   4.355 +(*      Format", May 8 1993, Section 2.1)                                    *)
   4.356 +(* fm  : formula to be serialized.  Note: 'fm' must not contain a variable   *)
   4.357 +(*       index less than 1.                                                  *)
   4.358 +(* def : If true, translate 'fm' into definitional CNF.  Otherwise translate *)
   4.359 +(*       'fm' into CNF.                                                      *)
   4.360 +(* path: path of the file to be created                                      *)
   4.361 +(* ------------------------------------------------------------------------- *)
   4.362 +
   4.363 +	(* prop_formula -> bool -> Path.T -> unit *)
   4.364 +
   4.365 +	fun prop_formula_to_dimacs_cnf_format fm def path =
   4.366 +	let
   4.367 +		(* prop_formula *)
   4.368 +		val cnf =
   4.369 +			if def then
   4.370 +				prop_formula_to_def_cnf fm
   4.371 +			else
   4.372 +				prop_formula_to_cnf fm
   4.373 +		val fm' =
   4.374 +			case cnf of
   4.375 +			  True  => Or (BoolVar 1, Not (BoolVar 1))
   4.376 +			| False => And (BoolVar 1, Not (BoolVar 1))
   4.377 +			| _     => cnf (* either 'cnf'=True/False, or 'cnf' does not contain True/False at all *)
   4.378 +		(* prop_formula -> int *)
   4.379 +		fun cnf_number_of_clauses (And (fm1,fm2)) =
   4.380 +			(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
   4.381 +		  | cnf_number_of_clauses _ =
   4.382 +			1
   4.383 +		(* prop_formula -> string *)
   4.384 +		fun cnf_prop_formula_to_string (BoolVar i) =
   4.385 +			if (i<1) then
   4.386 +				raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains a variable index less than 1")
   4.387 +			else
   4.388 +				(string_of_int i)
   4.389 +		  | cnf_prop_formula_to_string (Not fm1) =
   4.390 +			"-" ^ (cnf_prop_formula_to_string fm1)
   4.391 +		  | cnf_prop_formula_to_string (Or (fm1,fm2)) =
   4.392 +			(cnf_prop_formula_to_string fm1) ^ " " ^ (cnf_prop_formula_to_string fm2)
   4.393 +		  | cnf_prop_formula_to_string (And (fm1,fm2)) =
   4.394 +			(cnf_prop_formula_to_string fm1) ^ " 0\n" ^ (cnf_prop_formula_to_string fm2)
   4.395 +		  | cnf_prop_formula_to_string _ =
   4.396 +			raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains True/False")
   4.397 +	in
   4.398 +		File.write path ("c This file was generated by prop_formula_to_dimacs_cnf_format\n"
   4.399 +			^ "c (c) Tjark Weber\n"
   4.400 +			^ "p cnf " ^ (string_of_int (max_var_index fm')) ^ " " ^ (string_of_int (cnf_number_of_clauses fm')) ^ "\n"
   4.401 +			^ (cnf_prop_formula_to_string fm') ^ "\n")
   4.402 +	end;
   4.403 +
   4.404 +(* ------------------------------------------------------------------------- *)
   4.405 +(* prop_formula_to_dimacs_sat_format: serializes a formula of propositional  *)
   4.406 +(*      logic to a file in DIMACS SAT format (see "Satisfiability Suggested  *)
   4.407 +(*      Format", May 8 1993, Section 2.2)                                    *)
   4.408 +(* fm  : formula to be serialized.  Note: 'fm' must not contain a variable   *)
   4.409 +(*       index less than 1.                                                  *)
   4.410 +(* path: path of the file to be created                                      *)
   4.411 +(* ------------------------------------------------------------------------- *)
   4.412 +
   4.413 +	(* prop_formula -> Path.T -> unit *)
   4.414 +
   4.415 +	fun prop_formula_to_dimacs_sat_format fm path =
   4.416 +	let
   4.417 +		fun prop_formula_to_string True =
   4.418 +			"*()"
   4.419 +		  | prop_formula_to_string False =
   4.420 +			"+()"
   4.421 +		  | prop_formula_to_string (BoolVar i) =
   4.422 +			if (i<1) then
   4.423 +				raise REFUTE ("prop_formula_to_dimacs_sat_format", "formula contains a variable index less than 1")
   4.424 +			else
   4.425 +				(string_of_int i)
   4.426 +		  | prop_formula_to_string (Not fm1) =
   4.427 +			"-(" ^ (prop_formula_to_string fm1) ^ ")"
   4.428 +		  | prop_formula_to_string (Or (fm1,fm2)) =
   4.429 +			"+(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
   4.430 +		  | prop_formula_to_string (And (fm1,fm2)) =
   4.431 +			"*(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
   4.432 +	in
   4.433 +		File.write path ("c This file was generated by prop_formula_to_dimacs_sat_format\n"
   4.434 +			^ "c (c) Tjark Weber\n"
   4.435 +			^ "p sat " ^ (string_of_int (max (max_var_index fm, 1))) ^ "\n"
   4.436 +			^ "(" ^ (prop_formula_to_string fm) ^ ")\n")
   4.437 +	end;
   4.438 +
   4.439 +(* ------------------------------------------------------------------------- *)
   4.440 +(* prop_formula_sat_solver: try to find a satisfying assignment for the      *)
   4.441 +(*      boolean variables in a propositional formula, using an external SAT  *)
   4.442 +(*      solver.  If the SAT solver did not find an assignment, 'None' is     *)
   4.443 +(*      returned.  Otherwise 'Some (list of integers)' is returned, where    *)
   4.444 +(*      i>0 means that the boolean variable i is set to TRUE, and i<0 means  *)
   4.445 +(*      that the boolean variable i is set to FALSE.  Note that if           *)
   4.446 +(*      'satformat' is 'defcnf', then the assignment returned may contain    *)
   4.447 +(*      auxiliary variables that were not present in the original formula    *)
   4.448 +(*      'fm'.                                                                *)
   4.449 +(* fm        : formula that is passed to the SAT solver                      *) 
   4.450 +(* satpath   : path of the file used to store the propositional formula,     *)
   4.451 +(*             i.e. the input to the SAT solver                              *)
   4.452 +(* satformat : format of the SAT solver's input file.  Must be either "cnf", *)
   4.453 +(*             "defcnf", or "sat".                                           *)
   4.454 +(* resultpath: path of the file containing the SAT solver's output           *)
   4.455 +(* success   : part of the line in the SAT solver's output that is followed  *)
   4.456 +(*             by a line consisting of a list of integers representing the   *)
   4.457 +(*             satisfying assignment                                         *)
   4.458 +(* command   : system command used to execute the SAT solver                 *)
   4.459 +(* ------------------------------------------------------------------------- *)
   4.460 +
   4.461 +	(* prop_formula -> Path.T -> string -> Path.T -> string -> string -> int list option *)
   4.462 +
   4.463 +	fun prop_formula_sat_solver fm satpath satformat resultpath success command =
   4.464 +		if File.exists satpath then
   4.465 +			error ("file '" ^ (Path.pack satpath) ^ "' exists, please delete (will not overwrite)")
   4.466 +		else if File.exists resultpath then
   4.467 +			error ("file '" ^ (Path.pack resultpath) ^ "' exists, please delete (will not overwrite)")
   4.468 +		else
   4.469 +		(
   4.470 +			(* serialize the formula 'fm' to a file *)
   4.471 +			if satformat="cnf" then
   4.472 +				prop_formula_to_dimacs_cnf_format fm false satpath
   4.473 +			else if satformat="defcnf" then
   4.474 +				prop_formula_to_dimacs_cnf_format fm true satpath
   4.475 +			else if satformat="sat" then
   4.476 +				prop_formula_to_dimacs_sat_format fm satpath
   4.477 +			else
   4.478 +				error ("invalid argument: satformat='" ^ satformat ^ "' (must be either 'cnf', 'defcnf', or 'sat')");
   4.479 +			(* execute SAT solver *)
   4.480 +			if (system command)<>0 then
   4.481 +			(
   4.482 +				(* error executing SAT solver *)
   4.483 +				File.rm satpath;
   4.484 +				File.rm resultpath;
   4.485 +				error ("system command '" ^ command ^ "' failed (make sure a SAT solver is installed)")
   4.486 +			)
   4.487 +			else
   4.488 +			(
   4.489 +				(* read assignment from the result file *)
   4.490 +				File.rm satpath;
   4.491 +				let
   4.492 +					(* 'a option -> 'a Library.option *)
   4.493 +					fun option (SOME a) =
   4.494 +						Some a
   4.495 +					  | option NONE =
   4.496 +						None
   4.497 +					(* string -> int list *)
   4.498 +					fun string_to_int_list s =
   4.499 +						mapfilter (option o LargeInt.fromString) (space_explode " " s)
   4.500 +					(* string -> string -> bool *)
   4.501 +					fun is_substring s1 s2 =
   4.502 +					let
   4.503 +						val length1 = String.size s1
   4.504 +						val length2 = String.size s2
   4.505 +					in
   4.506 +						if length2 < length1 then
   4.507 +							false
   4.508 +						else if s1 = String.substring (s2, 0, length1) then
   4.509 +							true
   4.510 +						else is_substring s1 (String.substring (s2, 1, length2-1))
   4.511 +					end
   4.512 +					(* string list -> int list option *)
   4.513 +					fun extract_solution [] =
   4.514 +						None
   4.515 +					  | extract_solution (line::lines) =
   4.516 +						if is_substring success line then
   4.517 +							(* the next line must be a list of integers *)
   4.518 +							Some (string_to_int_list (hd lines))
   4.519 +						else
   4.520 +							extract_solution lines
   4.521 +					val sat_result = File.read resultpath
   4.522 +				in
   4.523 +					File.rm resultpath;
   4.524 +					extract_solution (split_lines sat_result)
   4.525 +				end
   4.526 +			)
   4.527 +		);
   4.528 +
   4.529 +
   4.530 +(* ------------------------------------------------------------------------- *)
   4.531 +(* TREES                                                                     *)
   4.532 +(* ------------------------------------------------------------------------- *)
   4.533 +
   4.534 +(* ------------------------------------------------------------------------- *)
   4.535 +(* tree: implements an arbitrarily (but finitely) branching tree as a list   *)
   4.536 +(*       of (lists of ...) elements                                          *)
   4.537 +(* ------------------------------------------------------------------------- *)
   4.538 +
   4.539 +	datatype 'a tree =
   4.540 +		  Leaf of 'a
   4.541 +		| Node of ('a tree) list;
   4.542 +
   4.543 +	type prop_tree =
   4.544 +		prop_formula list tree;
   4.545 +
   4.546 +	(* ('a -> 'b) -> 'a tree -> 'b tree *)
   4.547 +
   4.548 +	fun tree_map f tr =
   4.549 +		case tr of
   4.550 +		  Leaf x  => Leaf (f x)
   4.551 +		| Node xs => Node (map (tree_map f) xs);
   4.552 +
   4.553 +	(* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)
   4.554 +
   4.555 +	fun tree_foldl f =
   4.556 +	let
   4.557 +		fun itl (e, Leaf x)  = f(e,x)
   4.558 +		  | itl (e, Node xs) = foldl (tree_foldl f) (e,xs)
   4.559 +	in
   4.560 +		itl
   4.561 +	end;
   4.562 +
   4.563 +	(* 'a tree * 'b tree -> ('a * 'b) tree *)
   4.564 +
   4.565 +	fun tree_pair (t1,t2) =
   4.566 +		case t1 of
   4.567 +		  Leaf x =>
   4.568 +			(case t2 of
   4.569 +				  Leaf y => Leaf (x,y)
   4.570 +				| Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)"))
   4.571 +		| Node xs =>
   4.572 +			(case t2 of
   4.573 +				  (* '~~' will raise an exception if the number of branches in both trees is different at the current node *)
   4.574 +				  Node ys => Node (map tree_pair (xs ~~ ys))
   4.575 +				| Leaf _  => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
   4.576 +
   4.577 +(* ------------------------------------------------------------------------- *)
   4.578 +(* prop_tree_to_true: returns a propositional formula that is true iff the   *)
   4.579 +(*      tree denotes the boolean value TRUE                                  *)
   4.580 +(* ------------------------------------------------------------------------- *)
   4.581 +
   4.582 +	(* prop_tree -> prop_formula *)
   4.583 +
   4.584 +	(* a term of type 'bool' is represented as a 2-element leaf, where *)
   4.585 +	(* the term is true iff the leaf's first element is true           *)
   4.586 +
   4.587 +	fun prop_tree_to_true (Leaf [fm,_]) =
   4.588 +		fm
   4.589 +	  | prop_tree_to_true _ =
   4.590 +		raise REFUTE ("prop_tree_to_true", "tree is not a 2-element leaf");
   4.591 +
   4.592 +(* ------------------------------------------------------------------------- *)
   4.593 +(* prop_tree_to_false: returns a propositional formula that is true iff the  *)
   4.594 +(*      tree denotes the boolean value FALSE                                 *)
   4.595 +(* ------------------------------------------------------------------------- *)
   4.596 +
   4.597 +	(* prop_tree -> prop_formula *)
   4.598 +
   4.599 +	(* a term of type 'bool' is represented as a 2-element leaf, where *)
   4.600 +	(* the term is false iff the leaf's second element is true         *)
   4.601 +
   4.602 +	fun prop_tree_to_false (Leaf [_,fm]) =
   4.603 +		fm
   4.604 +	  | prop_tree_to_false _ =
   4.605 +		raise REFUTE ("prop_tree_to_false", "tree is not a 2-element leaf");
   4.606 +
   4.607 +(* ------------------------------------------------------------------------- *)
   4.608 +(* restrict_to_single_element: returns a propositional formula which is true *)
   4.609 +(*      iff the tree 'tr' describes a single element of its corresponding    *)
   4.610 +(*      type, i.e. iff at each leaf, one and only one formula is true        *)
   4.611 +(* ------------------------------------------------------------------------- *)
   4.612 +
   4.613 +	(* prop_tree -> prop_formula *)
   4.614 +
   4.615 +	fun restrict_to_single_element tr =
   4.616 +	let
   4.617 +		(* prop_formula list -> prop_formula *)
   4.618 +		fun allfalse []      = True
   4.619 +		  | allfalse (x::xs) = SAnd (SNot x, allfalse xs)
   4.620 +		(* prop_formula list -> prop_formula *)
   4.621 +		fun exactly1true []      = False
   4.622 +		  | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
   4.623 +	in
   4.624 +		case tr of
   4.625 +		  Leaf [BoolVar _, Not (BoolVar _)] => True (* optimization for boolean variables *)
   4.626 +		| Leaf xs                           => exactly1true xs
   4.627 +		| Node trees                        => list_conjunction (map restrict_to_single_element trees)
   4.628 +	end;
   4.629 +
   4.630 +(* ------------------------------------------------------------------------- *)
   4.631 +(* HOL FORMULAS                                                              *)
   4.632 +(* ------------------------------------------------------------------------- *)
   4.633 +
   4.634 +(* ------------------------------------------------------------------------- *)
   4.635 +(* absvar: form an abstraction over a schematic variable                     *)
   4.636 +(* ------------------------------------------------------------------------- *)
   4.637 +
   4.638 +	(* Term.indexname * Term.typ * Term.term -> Term.term *)
   4.639 +
   4.640 +	(* this function is similar to Term.absfree, but for schematic       *)
   4.641 +	(* variables (rather than free variables)                            *)
   4.642 +	fun absvar ((x,i),T,body) =
   4.643 +		Abs(x, T, abstract_over (Var((x,i),T), body));
   4.644 +
   4.645 +(* ------------------------------------------------------------------------- *)
   4.646 +(* list_all_var: quantification over a list of schematic variables           *)
   4.647 +(* ------------------------------------------------------------------------- *)
   4.648 +
   4.649 +	(* (Term.indexname * Term.typ) list * Term.term -> Term.term *)
   4.650 +
   4.651 +	(* this function is similar to Term.list_all_free, but for schematic *)
   4.652 +	(* variables (rather than free variables)                            *)
   4.653 +	fun list_all_var ([], t) =
   4.654 +		t
   4.655 +	  | list_all_var ((idx,T)::vars, t) =
   4.656 +		(all T) $ (absvar(idx, T, list_all_var(vars,t)));
   4.657 +
   4.658 +(* ------------------------------------------------------------------------- *)
   4.659 +(* close_vars: close up a formula over all schematic variables by            *)
   4.660 +(*             quantification (note that the result term may still contain   *)
   4.661 +(*             (non-schematic) free variables)                               *)
   4.662 +(* ------------------------------------------------------------------------- *)
   4.663 +
   4.664 +	(* Term.term -> Term.term *)
   4.665 +
   4.666 +	(* this function is similar to Logic.close_form, but for schematic   *)
   4.667 +	(* variables (rather than free variables)                            *)
   4.668 +	fun close_vars A =
   4.669 +		list_all_var (sort_wrt (fst o fst) (map dest_Var (term_vars A)), A);
   4.670 +
   4.671 +(* ------------------------------------------------------------------------- *)
   4.672 +(* make_universes: given a list 'xs' of "types" and a universe size 'size',  *)
   4.673 +(*      this function returns all possible partitions of the universe into   *)
   4.674 +(*      the "types" in 'xs' such that no "type" is empty.  If 'size' is less *)
   4.675 +(*      than 'length xs', the returned list of partitions is empty.          *)
   4.676 +(*      Otherwise, if the list 'xs' is empty, then the returned list of      *)
   4.677 +(*      partitions contains only the empty list, regardless of 'size'.       *)
   4.678 +(* ------------------------------------------------------------------------- *)
   4.679 +
   4.680 +	(* 'a list -> int -> ('a * int) list list *)
   4.681 +
   4.682 +	fun make_universes xs size =
   4.683 +	let
   4.684 +		(* 'a list -> int -> int -> ('a * int) list list *)
   4.685 +		fun make_partitions_loop (x::xs) 0 total =
   4.686 +			map (fn us => ((x,0)::us)) (make_partitions xs total)
   4.687 +		  | make_partitions_loop (x::xs) first total =
   4.688 +			(map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
   4.689 +		  | make_partitions_loop _ _ _ =
   4.690 +			raise REFUTE ("make_universes::make_partitions_loop", "empty list")
   4.691 +		and
   4.692 +		(* 'a list -> int -> ('a * int) list list *)
   4.693 +		make_partitions [x] size =
   4.694 +			(* we must use all remaining elements on the type 'x', so there is only one partition *)
   4.695 +			[[(x,size)]]
   4.696 +		  | make_partitions (x::xs) 0 =
   4.697 +			(* there are no elements left in the universe, so there is only one partition *)
   4.698 +			[map (fn t => (t,0)) (x::xs)]
   4.699 +		  | make_partitions (x::xs) size =
   4.700 +			(* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
   4.701 +			make_partitions_loop (x::xs) size size
   4.702 +		  | make_partitions _ _ =
   4.703 +			raise REFUTE ("make_universes::make_partitions", "empty list")
   4.704 +		val len = length xs
   4.705 +	in
   4.706 +		if size<len then
   4.707 +			(* the universe isn't big enough to make every type non-empty *)
   4.708 +			[]
   4.709 +		else if xs=[] then
   4.710 +			(* no types: return one universe, regardless of the size *)
   4.711 +			[[]]
   4.712 +		else
   4.713 +			(* partition into possibly empty types, then add 1 element to each type *)
   4.714 +			map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
   4.715 +	end;
   4.716 +
   4.717 +(* ------------------------------------------------------------------------- *)
   4.718 +(* sum: computes the sum of a list of integers; sum [] = 0                   *)
   4.719 +(* ------------------------------------------------------------------------- *)
   4.720 +
   4.721 +	(* int list -> int *)
   4.722 +
   4.723 +	fun sum xs = foldl (op +) (0, xs);
   4.724 +
   4.725 +(* ------------------------------------------------------------------------- *)
   4.726 +(* product: computes the product of a list of integers; product [] = 1       *)
   4.727 +(* ------------------------------------------------------------------------- *)
   4.728 +
   4.729 +	(* int list -> int *)
   4.730 +
   4.731 +	fun product xs = foldl (op *) (1, xs);
   4.732 +
   4.733 +(* ------------------------------------------------------------------------- *)
   4.734 +(* power: power(a,b) computes a^b, for a>=0, b>=0                            *)
   4.735 +(* ------------------------------------------------------------------------- *)
   4.736 +
   4.737 +	(* int * int -> int *)
   4.738 +
   4.739 +	fun power (a,0) = 1
   4.740 +	  | power (a,1) = a
   4.741 +	  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end;
   4.742 +
   4.743 +(* ------------------------------------------------------------------------- *)
   4.744 +(* size_of_type: returns the size of a type, where 'us' specifies the size   *)
   4.745 +(*      of each basic type (i.e. each type variable), and 'cdepth' specifies *)
   4.746 +(*      the maximal constructor depth for inductive datatypes                *)
   4.747 +(* ------------------------------------------------------------------------- *)
   4.748 +
   4.749 +	(* Term.typ -> (Term.typ * int) list -> theory -> int -> int *)
   4.750 +
   4.751 +	fun size_of_type T us thy cdepth =
   4.752 +	let
   4.753 +		(* Term.typ -> (Term.typ * int) -> int *)
   4.754 +		fun lookup_size T [] =
   4.755 +			raise REFUTE ("size_of_type", "no size specified for type variable '" ^ (Sign.string_of_typ (sign_of thy) T) ^ "'")
   4.756 +		  | lookup_size T ((typ,size)::pairs) =
   4.757 +			if T=typ then size else lookup_size T pairs
   4.758 +	in
   4.759 +		case T of
   4.760 +		  Type ("prop", [])     => 2
   4.761 +		| Type ("bool", [])     => 2
   4.762 +		| Type ("Product_Type.unit", []) => 1
   4.763 +		| Type ("+", [T1,T2])   => (size_of_type T1 us thy cdepth) + (size_of_type T2 us thy cdepth)
   4.764 +		| Type ("*", [T1,T2])   => (size_of_type T1 us thy cdepth) * (size_of_type T2 us thy cdepth)
   4.765 +		| Type ("fun", [T1,T2]) => power (size_of_type T2 us thy cdepth, size_of_type T1 us thy cdepth)
   4.766 +		| Type ("set", [T1])    => size_of_type (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
   4.767 +		| Type (s, Ts)          =>
   4.768 +			(case DatatypePackage.datatype_info thy s of
   4.769 +			  Some info => (* inductive datatype *)
   4.770 +				if cdepth>0 then
   4.771 +					let
   4.772 +						val index               = #index info
   4.773 +						val descr               = #descr info
   4.774 +						val (_, dtyps, constrs) = the (assoc (descr, index))
   4.775 +						val Typs                = dtyps ~~ Ts
   4.776 +						(* DatatypeAux.dtyp -> Term.typ *)
   4.777 +						fun typ_of_dtyp (DatatypeAux.DtTFree a) =
   4.778 +							the (assoc (Typs, DatatypeAux.DtTFree a))
   4.779 +						  | typ_of_dtyp (DatatypeAux.DtRec i) =
   4.780 +							let
   4.781 +								val (s, ds, _) = the (assoc (descr, i))
   4.782 +							in
   4.783 +								Type (s, map typ_of_dtyp ds)
   4.784 +							end
   4.785 +						  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
   4.786 +							Type (s, map typ_of_dtyp ds)
   4.787 +					in
   4.788 +						sum (map (fn (_,ds) => product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)) constrs)
   4.789 +					end
   4.790 +				else 0
   4.791 +			| None      => error ("size_of_type: type contains an unknown type constructor: '" ^ s ^ "'"))
   4.792 +		| TFree _               => lookup_size T us
   4.793 +		| TVar _                => lookup_size T us
   4.794 +	end;
   4.795 +
   4.796 +(* ------------------------------------------------------------------------- *)
   4.797 +(* type_to_prop_tree: creates a tree of boolean variables that denotes an    *)
   4.798 +(*      element of the type 'T'.  The height and branching factor of the     *)
   4.799 +(*      tree depend on the size and "structure" of 'T'.                      *)
   4.800 +(* 'us' : a "universe" specifying the number of elements for each basic type *)
   4.801 +(*        (i.e. each type variable) in 'T'                                   *)
   4.802 +(* 'cdepth': maximum constructor depth to be used for inductive datatypes    *)
   4.803 +(* 'idx': the next index to be used for a boolean variable                   *)
   4.804 +(* ------------------------------------------------------------------------- *)
   4.805 +
   4.806 +	(* Term.typ -> (Term.typ * int) list -> theory -> int -> int -> prop_tree * int *)
   4.807 +
   4.808 +	fun type_to_prop_tree T us thy cdepth idx =
   4.809 +	let
   4.810 +		(* int -> Term.typ -> int -> prop_tree list * int *)
   4.811 +		fun type_to_prop_tree_list 1 T' idx' =
   4.812 +			let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
   4.813 +				([tr], newidx)
   4.814 +			end
   4.815 +		  | type_to_prop_tree_list n T' idx' =
   4.816 +			let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
   4.817 +				let val (trees, lastidx) = type_to_prop_tree_list (n-1) T' newidx in
   4.818 +					(tr::trees, lastidx)
   4.819 +				end
   4.820 +			end
   4.821 +	in
   4.822 +		case T of
   4.823 +		  Type ("prop", []) =>
   4.824 +			(Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
   4.825 +		| Type ("bool", []) =>
   4.826 +			(Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
   4.827 +		| Type ("Product_Type.unit", []) =>
   4.828 +			(Leaf [True], idx)
   4.829 +		| Type ("+", [T1,T2]) =>
   4.830 +			let
   4.831 +				val s1 = size_of_type T1 us thy cdepth
   4.832 +				val s2 = size_of_type T2 us thy cdepth
   4.833 +				val s  = s1 + s2
   4.834 +			in
   4.835 +				if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
   4.836 +					raise EMPTY_DATATYPE
   4.837 +				else
   4.838 +					error "sum types (+) not implemented yet (TODO)"
   4.839 +			end
   4.840 +		| Type ("*", [T1,T2]) =>
   4.841 +			let
   4.842 +				val s1 = size_of_type T1 us thy cdepth
   4.843 +				val s2 = size_of_type T2 us thy cdepth
   4.844 +				val s  = s1 * s2
   4.845 +			in
   4.846 +				if s1=0 orelse s2=0 then
   4.847 +					raise EMPTY_DATATYPE
   4.848 +				else
   4.849 +					error "product types (*) not implemented yet (TODO)"
   4.850 +			end
   4.851 +		| Type ("fun", [T1,T2]) =>
   4.852 +			(* we create 'size_of_type T1' different copies of the tree for 'T2', *)
   4.853 +			(* which are then combined into a single new tree                     *)
   4.854 +			let
   4.855 +				val s = size_of_type T1 us thy cdepth
   4.856 +			in
   4.857 +				if s=0 then
   4.858 +					raise EMPTY_DATATYPE
   4.859 +				else
   4.860 +					let val (trees, newidx) = type_to_prop_tree_list s T2 idx in
   4.861 +						(Node trees, newidx)
   4.862 +					end
   4.863 +			end
   4.864 +		| Type ("set", [T1]) =>
   4.865 +			type_to_prop_tree (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth idx
   4.866 +		| Type (s, _) =>
   4.867 +			(case DatatypePackage.constrs_of thy s of
   4.868 +			   Some _ => (* inductive datatype *)
   4.869 +					let
   4.870 +						val s = size_of_type T us thy cdepth
   4.871 +					in
   4.872 +						if s=0 then
   4.873 +							raise EMPTY_DATATYPE
   4.874 +						else
   4.875 +							(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
   4.876 +					end
   4.877 +			 | None   => error ("type_to_prop_tree: type contains an unknown type constructor: '" ^ s ^ "'"))
   4.878 +		| TFree _ =>
   4.879 +			let val s = size_of_type T us thy cdepth in
   4.880 +				(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
   4.881 +			end
   4.882 +		| TVar _  =>
   4.883 +			let val s = size_of_type T us thy cdepth in
   4.884 +				(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
   4.885 +			end
   4.886 +	end;
   4.887 +
   4.888 +(* ------------------------------------------------------------------------- *)
   4.889 +(* type_to_constants: creates a list of prop_trees with constants (True,     *)
   4.890 +(*      False) rather than boolean variables, one for every element in the   *)
   4.891 +(*      type 'T'; c.f. type_to_prop_tree                                     *)
   4.892 +(* ------------------------------------------------------------------------- *)
   4.893 +
   4.894 +	(* Term.typ -> (Term.typ * int) list -> theory -> int -> prop_tree list *)
   4.895 +
   4.896 +	fun type_to_constants T us thy cdepth =
   4.897 +	let
   4.898 +		(* returns a list with all unit vectors of length n *)
   4.899 +		(* int -> prop_tree list *)
   4.900 +		fun unit_vectors n =
   4.901 +		let
   4.902 +			(* returns the k-th unit vector of length n *)
   4.903 +			(* int * int -> prop_tree *)
   4.904 +			fun unit_vector (k,n) =
   4.905 +				Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
   4.906 +			(* int -> prop_tree list -> prop_tree list *)
   4.907 +			fun unit_vectors_acc k vs =
   4.908 +				if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
   4.909 +		in
   4.910 +			unit_vectors_acc 1 []
   4.911 +		end
   4.912 +		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
   4.913 +		(* 'a -> 'a list list -> 'a list list *)
   4.914 +		fun cons_list x xss =
   4.915 +			map (fn xs => x::xs) xss
   4.916 +		(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
   4.917 +		(* int -> 'a list -> 'a list list *)
   4.918 +		fun pick_all 1 xs =
   4.919 +			map (fn x => [x]) xs
   4.920 +		  | pick_all n xs =
   4.921 +			let val rec_pick = pick_all (n-1) xs in
   4.922 +				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
   4.923 +			end
   4.924 +	in
   4.925 +		case T of
   4.926 +		  Type ("prop", [])     => unit_vectors 2
   4.927 +		| Type ("bool", [])     => unit_vectors 2
   4.928 +		| Type ("Product_Type.unit", []) => unit_vectors 1
   4.929 +                | Type ("+", [T1,T2])   =>
   4.930 +			let
   4.931 +				val s1 = size_of_type T1 us thy cdepth
   4.932 +				val s2 = size_of_type T2 us thy cdepth
   4.933 +			in
   4.934 +				if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
   4.935 +					raise EMPTY_DATATYPE
   4.936 +				else
   4.937 +					error "sum types (+) not implemented yet (TODO)"
   4.938 +			end
   4.939 +                | Type ("*", [T1,T2])   =>
   4.940 +			let
   4.941 +				val s1 = size_of_type T1 us thy cdepth
   4.942 +				val s2 = size_of_type T2 us thy cdepth
   4.943 +			in
   4.944 +				if s1=0 orelse s2=0 then
   4.945 +					raise EMPTY_DATATYPE
   4.946 +				else
   4.947 +					error "product types (*) not implemented yet (TODO)"
   4.948 +			end
   4.949 +		| Type ("fun", [T1,T2]) =>
   4.950 +			let
   4.951 +				val s = size_of_type T1 us thy cdepth
   4.952 +			in
   4.953 +				if s=0 then
   4.954 +					raise EMPTY_DATATYPE
   4.955 +				else
   4.956 +					map (fn xs => Node xs) (pick_all s (type_to_constants T2 us thy cdepth))
   4.957 +			end
   4.958 +		| Type ("set", [T1])    => type_to_constants (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
   4.959 +		| Type (s, _)           =>
   4.960 +			(case DatatypePackage.constrs_of thy s of
   4.961 +			   Some _ => (* inductive datatype *)
   4.962 +					let
   4.963 +						val s = size_of_type T us thy cdepth
   4.964 +					in
   4.965 +						if s=0 then
   4.966 +							raise EMPTY_DATATYPE
   4.967 +						else
   4.968 +							unit_vectors s
   4.969 +					end
   4.970 +			 | None   => error ("type_to_constants: type contains an unknown type constructor: '" ^ s ^ "'"))
   4.971 +		| TFree _               => unit_vectors (size_of_type T us thy cdepth)
   4.972 +		| TVar _                => unit_vectors (size_of_type T us thy cdepth)
   4.973 +	end;
   4.974 +
   4.975 +(* ------------------------------------------------------------------------- *)
   4.976 +(* prop_tree_equal: returns a propositional formula that is true iff 'tr1'   *)
   4.977 +(*      and 'tr2' both denote the same element                               *)
   4.978 +(* ------------------------------------------------------------------------- *)
   4.979 +
   4.980 +	(* prop_tree * prop_tree -> prop_formula *)
   4.981 +
   4.982 +	fun prop_tree_equal (tr1,tr2) =
   4.983 +		case tr1 of
   4.984 +		  Leaf x =>
   4.985 +			(case tr2 of
   4.986 +			  Leaf y => prop_formula_dot_product (x,y)
   4.987 +			| _      => raise REFUTE ("prop_tree_equal", "second tree is higher"))
   4.988 +		| Node xs =>
   4.989 +			(case tr2 of
   4.990 +			  Leaf _  => raise REFUTE ("prop_tree_equal", "first tree is higher")
   4.991 +			(* extensionality: two functions are equal iff they are equal for every element *)
   4.992 +			| Node ys => list_conjunction (map prop_tree_equal (xs ~~ ys)));
   4.993 +
   4.994 +(* ------------------------------------------------------------------------- *)
   4.995 +(* prop_tree_apply: returns a tree that denotes the element obtained by      *)
   4.996 +(*      applying the function which is denoted by the tree 't1' to the       *)
   4.997 +(*      element which is denoted by the tree 't2'                            *)
   4.998 +(* ------------------------------------------------------------------------- *)
   4.999 +
  4.1000 +	(* prop_tree * prop_tree -> prop_tree *)
  4.1001 +
  4.1002 +	fun prop_tree_apply (tr1,tr2) =
  4.1003 +	let
  4.1004 +		(* prop_tree * prop_tree -> prop_tree *)
  4.1005 +		fun prop_tree_disjunction (tr1,tr2) =
  4.1006 +			tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
  4.1007 +		(* prop_formula * prop_tree -> prop_tree *)
  4.1008 +		fun prop_formula_times_prop_tree (fm,tr) =
  4.1009 +			tree_map (map (fn x => SAnd (fm,x))) tr
  4.1010 +		(* prop_formula list * prop_tree list -> prop_tree *)
  4.1011 +		fun prop_formula_list_dot_product_prop_tree_list ([fm],[tr]) =
  4.1012 +			prop_formula_times_prop_tree (fm,tr)
  4.1013 +		  | prop_formula_list_dot_product_prop_tree_list (fm::fms,tr::trees) =
  4.1014 +			prop_tree_disjunction (prop_formula_times_prop_tree (fm,tr), prop_formula_list_dot_product_prop_tree_list (fms,trees))
  4.1015 +		  | prop_formula_list_dot_product_prop_tree_list (_,_) =
  4.1016 +			raise REFUTE ("prop_tree_apply::prop_formula_list_dot_product_prop_tree_list", "empty list")
  4.1017 +		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  4.1018 +		(* 'a -> 'a list list -> 'a list list *)
  4.1019 +		fun cons_list x xss =
  4.1020 +			map (fn xs => x::xs) xss
  4.1021 +		(* returns a list of lists, each one consisting of one element from each element of 'xss' *)
  4.1022 +		(* 'a list list -> 'a list list *)
  4.1023 +		fun pick_all [xs] =
  4.1024 +			map (fn x => [x]) xs
  4.1025 +		  | pick_all (xs::xss) =
  4.1026 +			let val rec_pick = pick_all xss in
  4.1027 +				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  4.1028 +			end
  4.1029 +		  | pick_all _ =
  4.1030 +			raise REFUTE ("prop_tree_apply::pick_all", "empty list")
  4.1031 +		(* prop_tree -> prop_formula list *)
  4.1032 +		fun prop_tree_to_prop_formula_list (Leaf xs) =
  4.1033 +			xs
  4.1034 +		  | prop_tree_to_prop_formula_list (Node trees) =
  4.1035 +			map list_conjunction (pick_all (map prop_tree_to_prop_formula_list trees))
  4.1036 +	in
  4.1037 +		case tr1 of
  4.1038 +		  Leaf _ =>
  4.1039 +			raise REFUTE ("prop_tree_apply", "first tree is a leaf")
  4.1040 +		| Node xs =>
  4.1041 +			prop_formula_list_dot_product_prop_tree_list (prop_tree_to_prop_formula_list tr2, xs)
  4.1042 +	end
  4.1043 +
  4.1044 +(* ------------------------------------------------------------------------- *)
  4.1045 +(* term_to_prop_tree: translates a HOL term 't' into a tree of propositional *)
  4.1046 +(*      formulas; 'us' specifies the number of elements for each type        *)
  4.1047 +(*      variable in 't'; 'cdepth' specifies the maximal constructor depth    *)
  4.1048 +(*      for inductive datatypes.  Also returns the lowest index that was not *)
  4.1049 +(*      used for a boolean variable, and a substitution of terms (free/      *)
  4.1050 +(*      schematic variables) by prop_trees.                                  *)
  4.1051 +(* ------------------------------------------------------------------------- *)
  4.1052 +
  4.1053 +	(* Term.term -> (Term.typ * int) list -> theory -> int -> prop_tree * (int * (Term.term * prop_tree) list) *)
  4.1054 +
  4.1055 +	fun term_to_prop_tree t us thy cdepth =
  4.1056 +	let
  4.1057 +		(* Term.term -> int * (Term.term * prop_tree) list -> prop_tree * (int * (Term.term * prop_tree) list) *)
  4.1058 +		fun variable_to_prop_tree_subst t' (idx,subs) =
  4.1059 +			case assoc (subs,t') of
  4.1060 +			  Some tr =>
  4.1061 +				(* return the previously associated tree; the substitution remains unchanged *)
  4.1062 +				(tr, (idx,subs))
  4.1063 +			| None =>
  4.1064 +				(* generate a new tree; update the index; extend the substitution *)
  4.1065 +				let
  4.1066 +					val T = case t' of
  4.1067 +						  Free (_,T) => T
  4.1068 +						| Var (_,T)  => T
  4.1069 +						| _          => raise REFUTE ("variable_to_prop_tree_subst", "term is not a (free or schematic) variable")
  4.1070 +					val (tr,newidx) = type_to_prop_tree T us thy cdepth idx
  4.1071 +				in
  4.1072 +					(tr, (newidx, (t',tr)::subs))
  4.1073 +				end
  4.1074 +		(* Term.term -> int * (Term.term * prop_tree) list -> prop_tree list -> prop_tree * (int * (Term.term * prop_tree) list) *)
  4.1075 +		fun term_to_prop_tree_subst t' (idx,subs) bsubs =
  4.1076 +			case t' of
  4.1077 +			(* meta-logical constants *)
  4.1078 +			  Const ("Goal", _) $ t1 =>
  4.1079 +				term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1080 +			| Const ("all", _) $ t1 =>
  4.1081 +				let
  4.1082 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1083 +				in
  4.1084 +					case tree1 of
  4.1085 +					  Node xs =>
  4.1086 +						let
  4.1087 +							val fmTrue  = list_conjunction (map prop_tree_to_true xs)
  4.1088 +							val fmFalse = list_disjunction (map prop_tree_to_false xs)
  4.1089 +						in
  4.1090 +							(Leaf [fmTrue, fmFalse], (i1,s1))
  4.1091 +						end
  4.1092 +					| _ =>
  4.1093 +						raise REFUTE ("term_to_prop_tree_subst", "'all' is not followed by a function")
  4.1094 +				end
  4.1095 +			| Const ("==", _) $ t1 $ t2 =>
  4.1096 +				let
  4.1097 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1098 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  4.1099 +					val fmTrue          = prop_tree_equal (tree1,tree2)
  4.1100 +					val fmFalse         = SNot fmTrue
  4.1101 +				in
  4.1102 +					(Leaf [fmTrue, fmFalse], (i2,s2))
  4.1103 +				end
  4.1104 +			| Const ("==>", _) $ t1 $ t2 =>
  4.1105 +				let
  4.1106 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1107 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  4.1108 +					val fmTrue          = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
  4.1109 +					val fmFalse         = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
  4.1110 +				in
  4.1111 +					(Leaf [fmTrue, fmFalse], (i2,s2))
  4.1112 +				end
  4.1113 +			(* HOL constants *)
  4.1114 +			| Const ("Trueprop", _) $ t1 =>
  4.1115 +				term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1116 +			| Const ("Not", _) $ t1 =>
  4.1117 +				let
  4.1118 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1119 +					val fmTrue          = prop_tree_to_false tree1
  4.1120 +					val fmFalse         = prop_tree_to_true tree1
  4.1121 +				in
  4.1122 +					(Leaf [fmTrue, fmFalse], (i1,s1))
  4.1123 +				end
  4.1124 +			| Const ("True", _) =>
  4.1125 +				(Leaf [True, False], (idx,subs))
  4.1126 +			| Const ("False", _) =>
  4.1127 +				(Leaf [False, True], (idx,subs))
  4.1128 +			| Const ("All", _) $ t1 =>
  4.1129 +				let
  4.1130 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1131 +				in
  4.1132 +					case tree1 of
  4.1133 +					  Node xs =>
  4.1134 +						let
  4.1135 +							val fmTrue  = list_conjunction (map prop_tree_to_true xs)
  4.1136 +							val fmFalse = list_disjunction (map prop_tree_to_false xs)
  4.1137 +						in
  4.1138 +							(Leaf [fmTrue, fmFalse], (i1,s1))
  4.1139 +						end
  4.1140 +					| _ =>
  4.1141 +						raise REFUTE ("term_to_prop_tree_subst", "'All' is not followed by a function")
  4.1142 +				end
  4.1143 +			| Const ("Ex", _) $ t1 =>
  4.1144 +				let
  4.1145 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1146 +				in
  4.1147 +					case tree1 of
  4.1148 +					  Node xs =>
  4.1149 +						let
  4.1150 +							val fmTrue  = list_disjunction (map prop_tree_to_true xs)
  4.1151 +							val fmFalse = list_conjunction (map prop_tree_to_false xs)
  4.1152 +						in
  4.1153 +							(Leaf [fmTrue, fmFalse], (i1,s1))
  4.1154 +						end
  4.1155 +					| _ =>
  4.1156 +						raise REFUTE ("term_to_prop_tree_subst", "'Ex' is not followed by a function")
  4.1157 +				end
  4.1158 +			| Const ("Ex1", Type ("fun", [Type ("fun", [T, Type ("bool",[])]), Type ("bool",[])])) $ t1 =>
  4.1159 +				(* 'Ex1 t1' is equivalent to 'Ex Abs(x,T,t1' x & All Abs(y,T,t1'' y --> x=y))' *)
  4.1160 +				let
  4.1161 +					val t1'      = Term.incr_bv (1, 0, t1)
  4.1162 +					val t1''     = Term.incr_bv (2, 0, t1)
  4.1163 +					val t_equal  = (HOLogic.eq_const T) $ (Bound 1) $ (Bound 0)
  4.1164 +					val t_unique = (HOLogic.all_const T) $ Abs("y",T,HOLogic.mk_imp (t1'' $ (Bound 0),t_equal))
  4.1165 +					val t_ex1    = (HOLogic.exists_const T) $ Abs("x",T,HOLogic.mk_conj (t1' $ (Bound 0),t_unique))
  4.1166 +				in
  4.1167 +					term_to_prop_tree_subst t_ex1 (idx,subs) bsubs
  4.1168 +				end
  4.1169 +			| Const ("op =", _) $ t1 $ t2 =>
  4.1170 +				let
  4.1171 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1172 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  4.1173 +					val fmTrue          = prop_tree_equal (tree1,tree2)
  4.1174 +					val fmFalse         = SNot fmTrue
  4.1175 +				in
  4.1176 +					(Leaf [fmTrue, fmFalse], (i2,s2))
  4.1177 +				end
  4.1178 +			| Const ("op &", _) $ t1 $ t2 =>
  4.1179 +				let
  4.1180 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1181 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  4.1182 +					val fmTrue          = SAnd (prop_tree_to_true tree1, prop_tree_to_true tree2)
  4.1183 +					val fmFalse         = SOr (prop_tree_to_false tree1, prop_tree_to_false tree2)
  4.1184 +				in
  4.1185 +					(Leaf [fmTrue, fmFalse], (i2,s2))
  4.1186 +				end
  4.1187 +			| Const ("op |", _) $ t1 $ t2 =>
  4.1188 +				let
  4.1189 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1190 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  4.1191 +					val fmTrue          = SOr (prop_tree_to_true tree1, prop_tree_to_true tree2)
  4.1192 +					val fmFalse         = SAnd (prop_tree_to_false tree1, prop_tree_to_false tree2)
  4.1193 +				in
  4.1194 +					(Leaf [fmTrue, fmFalse], (i2,s2))
  4.1195 +				end
  4.1196 +			| Const ("op -->", _) $ t1 $ t2 =>
  4.1197 +				let
  4.1198 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1199 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  4.1200 +					val fmTrue          = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
  4.1201 +					val fmFalse         = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
  4.1202 +				in
  4.1203 +					(Leaf [fmTrue, fmFalse], (i2,s2))
  4.1204 +				end
  4.1205 +			(* set constants *)
  4.1206 +			| Const ("Collect", _) $ t1 =>
  4.1207 +				term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1208 +			| Const ("op :", _) $ t1 $ t2 =>
  4.1209 +				term_to_prop_tree_subst (t2 $ t1) (idx,subs) bsubs
  4.1210 +			(* datatype constants *)
  4.1211 +			| Const ("Product_Type.Unity", _) =>
  4.1212 +				(Leaf [True], (idx,subs))
  4.1213 +			(* unknown constants *)
  4.1214 +			| Const (c, _) =>
  4.1215 +				error ("term contains an unknown constant: '" ^ c ^ "'")
  4.1216 +			(* abstractions *)
  4.1217 +			| Abs (_,T,body) =>
  4.1218 +				let
  4.1219 +					val constants       = type_to_constants T us thy cdepth
  4.1220 +					val (trees, substs) = split_list (map (fn c => term_to_prop_tree_subst body (idx,subs) (c::bsubs)) constants)
  4.1221 +				in
  4.1222 +					(* the substitutions in 'substs' are all identical *)
  4.1223 +					(Node trees, hd substs)
  4.1224 +				end
  4.1225 +			(* (free/schematic) variables *)
  4.1226 +			| Free _ =>
  4.1227 +				variable_to_prop_tree_subst t' (idx,subs)
  4.1228 +			| Var _ =>
  4.1229 +				variable_to_prop_tree_subst t' (idx,subs)
  4.1230 +			(* bound variables *)
  4.1231 +			| Bound i =>
  4.1232 +				if (length bsubs) <= i then
  4.1233 +					raise REFUTE ("term_to_prop_tree_subst", "term contains a loose bound variable (with index " ^ (string_of_int i) ^ ")")
  4.1234 +				else
  4.1235 +					(nth_elem (i,bsubs), (idx,subs))
  4.1236 +			(* application *)
  4.1237 +			| t1 $ t2 =>
  4.1238 +				let
  4.1239 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  4.1240 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  4.1241 +				in
  4.1242 +					(prop_tree_apply (tree1,tree2), (i2,s2))
  4.1243 +				end
  4.1244 +	in
  4.1245 +		term_to_prop_tree_subst t (1,[]) []
  4.1246 +	end;
  4.1247 +
  4.1248 +(* ------------------------------------------------------------------------- *)
  4.1249 +(* term_to_prop_formula: translates a HOL formula 't' into a propositional   *)
  4.1250 +(*      formula that is satisfiable if and only if 't' has a model of "size" *)
  4.1251 +(*      'us' (where 'us' specifies the number of elements for each free type *)
  4.1252 +(*      variable in 't') and maximal constructor depth 'cdepth'.             *)
  4.1253 +(* ------------------------------------------------------------------------- *)
  4.1254 +
  4.1255 +	(* TODO: shouldn't 'us' also specify the number of elements for schematic type variables? (if so, modify the comment above) *)
  4.1256 +
  4.1257 +	(* Term.term -> (Term.typ * int) list -> theory -> int -> prop_formula * (int * (Term.term * prop_tree) list) *)
  4.1258 +
  4.1259 +	fun term_to_prop_formula t us thy cdepth =
  4.1260 +	let
  4.1261 +		val (tr, (idx,subs)) = term_to_prop_tree t us thy cdepth
  4.1262 +		val fm               = prop_tree_to_true tr
  4.1263 +	in
  4.1264 +		if subs=[] then
  4.1265 +			(fm, (idx,subs))
  4.1266 +		else
  4.1267 +			(* make sure every tree that is substituted for a term describes a single element *)
  4.1268 +			(SAnd (list_conjunction (map (fn (_,tr) => restrict_to_single_element tr) subs), fm), (idx,subs))
  4.1269 +	end;
  4.1270 +
  4.1271 +
  4.1272 +(* ------------------------------------------------------------------------- *)
  4.1273 +(* INTERFACE, PART 2: FINDING A MODEL                                        *)
  4.1274 +(* ------------------------------------------------------------------------- *)
  4.1275 +
  4.1276 +(* ------------------------------------------------------------------------- *)
  4.1277 +(* string_of_universe: prints a universe, i.e. an assignment of sizes for    *)
  4.1278 +(*                     types                                                 *)
  4.1279 +(* thy: the current theory                                                   *)
  4.1280 +(* us : a list containing types together with their size                     *)
  4.1281 +(* ------------------------------------------------------------------------- *)
  4.1282 +
  4.1283 +	(* theory -> (Term.typ * int) list -> string *)
  4.1284 +
  4.1285 +	fun string_of_universe thy [] =
  4.1286 +		"empty universe (no type variables in term)"
  4.1287 +	  | string_of_universe thy us =
  4.1288 +		space_implode ", " (map (fn (T,i) => (Sign.string_of_typ (sign_of thy) T) ^ ": " ^ (string_of_int i)) us);
  4.1289 +
  4.1290 +(* ------------------------------------------------------------------------- *)
  4.1291 +(* string_of_model: prints a model, given by a substitution 'subs' of trees  *)
  4.1292 +(*      of propositional variables and an assignment 'ass' of truth values   *)
  4.1293 +(*      for these variables.                                                 *)
  4.1294 +(* thy   : the current theory                                                *)
  4.1295 +(* us    : universe, specifies the "size" of each type (i.e. type variable)  *)
  4.1296 +(* cdepth: maximal constructor depth for inductive datatypes                 *)
  4.1297 +(* subs  : substitution of trees of propositional formulas (for variables)   *)
  4.1298 +(* ass   : assignment of truth values for boolean variables; see function    *)
  4.1299 +(*         'truth_value' below for its meaning                               *)
  4.1300 +(* ------------------------------------------------------------------------- *)
  4.1301 +
  4.1302 +	(* theory -> (Term.typ * int) list -> int -> (Term.term * prop_formula tree) list -> int list -> string *)
  4.1303 +
  4.1304 +	fun string_of_model thy us cdepth [] ass =
  4.1305 +		"empty interpretation (no free variables in term)"
  4.1306 +	  | string_of_model thy us cdepth subs ass =
  4.1307 +		let
  4.1308 +			(* Sign.sg *)
  4.1309 +			val sg = sign_of thy
  4.1310 +			(* int -> bool *)
  4.1311 +			fun truth_value i =
  4.1312 +				if i mem ass then true
  4.1313 +				else if ~i mem ass then false
  4.1314 +				else error ("SAT solver assignment does not specify a value for variable " ^ (string_of_int i))
  4.1315 +			(* string -> string *)
  4.1316 +			fun strip_leading_quote str =
  4.1317 +				if nth_elem_string(0,str)="'" then
  4.1318 +					String.substring (str, 1, size str - 1)
  4.1319 +				else
  4.1320 +					str;
  4.1321 +			(* prop_formula list -> int *)
  4.1322 +			fun true_index xs =
  4.1323 +				(* returns the (0-based) index of the first true formula in xs *)
  4.1324 +				let fun true_index_acc [] _ =
  4.1325 +					raise REFUTE ("string_of_model::true_index", "no variable was set to true")
  4.1326 +				      | true_index_acc (x::xs) n =
  4.1327 +					case x of
  4.1328 +					  BoolVar i =>
  4.1329 +						if truth_value i then n else true_index_acc xs (n+1)
  4.1330 +					| True =>
  4.1331 +						n
  4.1332 +					| False =>
  4.1333 +						true_index_acc xs (n+1)
  4.1334 +					| _ =>
  4.1335 +						raise REFUTE ("string_of_model::true_index", "formula is not a boolean variable/true/false")
  4.1336 +				in
  4.1337 +					true_index_acc xs 0
  4.1338 +				end
  4.1339 +			(* Term.typ -> int -> prop_tree -> string *)
  4.1340 +			(* prop *)
  4.1341 +			fun string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
  4.1342 +				if truth_value i then "true" else "false"
  4.1343 +			  | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [True, False]) =
  4.1344 +				"true"
  4.1345 +			  | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [False, True]) =
  4.1346 +				"false"
  4.1347 +			(* bool *)
  4.1348 +			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
  4.1349 +				if truth_value i then "true" else "false"
  4.1350 +			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [True, False]) =
  4.1351 +				"true"
  4.1352 +			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [False, True]) =
  4.1353 +				"false"
  4.1354 +			(* unit *)
  4.1355 +			  | string_of_prop_tree (Type ("Product_Type.unit",[])) cdepth (Leaf [True]) =
  4.1356 +				"()"
  4.1357 +			  | string_of_prop_tree (Type (s,Ts)) cdepth (Leaf xs) =
  4.1358 +				(case DatatypePackage.datatype_info thy s of
  4.1359 +				   Some info => (* inductive datatype *)
  4.1360 +					let
  4.1361 +						val index               = #index info
  4.1362 +						val descr               = #descr info
  4.1363 +						val (_, dtyps, constrs) = the (assoc (descr, index))
  4.1364 +						val Typs                = dtyps ~~ Ts
  4.1365 +						(* string -> string *)
  4.1366 +						fun unqualify s =
  4.1367 +							implode (snd (take_suffix (fn c => c <> ".") (explode s)))
  4.1368 +						(* DatatypeAux.dtyp -> Term.typ *)
  4.1369 +						fun typ_of_dtyp (DatatypeAux.DtTFree a) =
  4.1370 +							the (assoc (Typs, DatatypeAux.DtTFree a))
  4.1371 +						  | typ_of_dtyp (DatatypeAux.DtRec i) =
  4.1372 +							let
  4.1373 +								val (s, ds, _) = the (assoc (descr, i))
  4.1374 +							in
  4.1375 +								Type (s, map typ_of_dtyp ds)
  4.1376 +							end
  4.1377 +						  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
  4.1378 +							Type (s, map typ_of_dtyp ds)
  4.1379 +						(* DatatypeAux.dtyp list -> int -> string *)
  4.1380 +						fun string_of_inductive_type_cargs [] n =
  4.1381 +							if n<>0 then
  4.1382 +								raise REFUTE ("string_of_model", "internal error computing the element index for an inductive type")
  4.1383 +							else
  4.1384 +								""
  4.1385 +						  | string_of_inductive_type_cargs (d::ds) n =
  4.1386 +							let
  4.1387 +								val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
  4.1388 +							in
  4.1389 +								" " ^ (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))
  4.1390 +							end
  4.1391 +						(* (string * DatatypeAux.dtyp list) list -> int -> string *)
  4.1392 +						fun string_of_inductive_type_constrs [] n =
  4.1393 +							raise REFUTE ("string_of_model", "inductive type has fewer elements than needed")
  4.1394 +						  | string_of_inductive_type_constrs ((s,ds)::cs) n =
  4.1395 +							let
  4.1396 +								val size = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
  4.1397 +							in
  4.1398 +								if n < size then
  4.1399 +									(unqualify s) ^ (string_of_inductive_type_cargs ds n)
  4.1400 +								else
  4.1401 +									string_of_inductive_type_constrs cs (n - size)
  4.1402 +							end
  4.1403 +					in
  4.1404 +						string_of_inductive_type_constrs constrs (true_index xs)
  4.1405 +					end
  4.1406 +				 | None =>
  4.1407 +					raise REFUTE ("string_of_model", "type contains an unknown type constructor: '" ^ s ^ "'"))
  4.1408 +			(* type variable *)
  4.1409 +			  | string_of_prop_tree (TFree (s,_)) cdepth (Leaf xs) =
  4.1410 +					(strip_leading_quote s) ^ (string_of_int (true_index xs))
  4.1411 +			  | string_of_prop_tree (TVar ((s,_),_)) cdepth (Leaf xs) =
  4.1412 +					(strip_leading_quote s) ^ (string_of_int (true_index xs))
  4.1413 +			(* function or set type *)
  4.1414 +			  | string_of_prop_tree T cdepth (Node xs) =
  4.1415 +				case T of
  4.1416 +				  Type ("fun", [T1,T2]) =>
  4.1417 +					let
  4.1418 +						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)
  4.1419 +					in
  4.1420 +						"(" ^ (space_implode ", " strings) ^ ")"
  4.1421 +					end
  4.1422 +				| Type ("set", [T1]) =>
  4.1423 +					let
  4.1424 +						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)
  4.1425 +					in
  4.1426 +						"{" ^ (space_implode ", " strings) ^ "}"
  4.1427 +					end
  4.1428 +				| _ => raise REFUTE ("string_of_model::string_of_prop_tree", "not a function/set type")
  4.1429 +			(* Term.term * prop_formula tree -> string *)
  4.1430 +			fun string_of_term_assignment (t,tr) =
  4.1431 +			let
  4.1432 +				val T = case t of
  4.1433 +					  Free (_,T) => T
  4.1434 +					| Var (_,T)  => T
  4.1435 +					| _          => raise REFUTE ("string_of_model::string_of_term_assignment", "term is not a (free or schematic) variable")
  4.1436 +			in
  4.1437 +				(Sign.string_of_term sg t) ^ " = " ^ (string_of_prop_tree T cdepth tr)
  4.1438 +			end
  4.1439 +		in
  4.1440 +			space_implode "\n" (map string_of_term_assignment subs)
  4.1441 +		end;
  4.1442 +
  4.1443 +(* ------------------------------------------------------------------------- *)
  4.1444 +(* find_model: repeatedly calls 'prop_formula_sat_solver' with appropriate   *)
  4.1445 +(*             parameters, and displays the results to the user              *)
  4.1446 +(* params    : list of '(name, value)' pairs used to override default        *)
  4.1447 +(*             parameters                                                    *)
  4.1448 +(*                                                                           *)
  4.1449 +(* This is a brief description of the algorithm implemented:                 *)
  4.1450 +(*                                                                           *)
  4.1451 +(* 1. Let k = max ('minsize',1).                                             *)
  4.1452 +(* 2. Let the universe have k elements.  Find all possible partitions of     *)
  4.1453 +(*    these elements into the basic types occuring in 't' such that no basic *)
  4.1454 +(*    type is empty.                                                         *)
  4.1455 +(* 3. Translate 't' into a propositional formula p s.t. 't' has a model wrt. *)
  4.1456 +(*    the partition chosen in step (2.) if (actually, if and only if) p is   *)
  4.1457 +(*    satisfiable.  To do this, replace quantification by conjunction/       *)
  4.1458 +(*    disjunction over all elements of the type being quantified over.  (If  *)
  4.1459 +(*    p contains more than 'maxvars' boolean variables, terminate.)          *)
  4.1460 +(* 4. Serialize p to a file, and try to find a satisfying assignment for p   *)
  4.1461 +(*    by invoking an external SAT solver.                                    *)
  4.1462 +(* 5. If the SAT solver finds a satisfying assignment for p, translate this  *)
  4.1463 +(*    assignment back into a model for 't'.  Present this model to the user, *)
  4.1464 +(*    then terminate.                                                        *)
  4.1465 +(* 6. As long as there is another partition left, pick it and go back to     *)
  4.1466 +(*    step (3.).                                                             *)
  4.1467 +(* 7. Increase k by 1.  As long as k does not exceed 'maxsize', go back to   *)
  4.1468 +(*    step (2.).                                                             *)
  4.1469 +(*                                                                           *)
  4.1470 +(* The following parameters are currently supported (and required!):         *)
  4.1471 +(*                                                                           *)
  4.1472 +(* Name          Type    Description                                         *)
  4.1473 +(*                                                                           *)
  4.1474 +(* "minsize"     int     Only search for models with size at least           *)
  4.1475 +(*                       'minsize'.                                          *)
  4.1476 +(* "maxsize"     int     If >0, only search for models with size at most     *)
  4.1477 +(*                       'maxsize'.                                          *)
  4.1478 +(* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
  4.1479 +(*                       when transforming the term into a propositional     *)
  4.1480 +(*                       formula.                                            *)
  4.1481 +(* "satfile"     string  Name of the file used to store the propositional    *)
  4.1482 +(*                       formula, i.e. the input to the SAT solver.          *)
  4.1483 +(* "satformat"   string  Format of the SAT solver's input file.  Must be     *)
  4.1484 +(*                       either "cnf", "defcnf", or "sat".  Since "sat" is   *)
  4.1485 +(*                       not supported by most SAT solvers, and "cnf" can    *)
  4.1486 +(*                       cause exponential blowup of the formula, "defcnf"   *)
  4.1487 +(*                       is recommended.                                     *)
  4.1488 +(* "resultfile"  string  Name of the file containing the SAT solver's        *)
  4.1489 +(*                       output.                                             *)
  4.1490 +(* "success"     string  Part of the line in the SAT solver's output that    *)
  4.1491 +(*                       precedes a list of integers representing the        *)
  4.1492 +(*                       satisfying assignment.                              *)
  4.1493 +(* "command"     string  System command used to execute the SAT solver.      *)
  4.1494 +(*                       Note that you if you change 'satfile' or            *)
  4.1495 +(*                       'resultfile', you will also need to change          *)
  4.1496 +(*                       'command'.                                          *)
  4.1497 +(*                                                                           *)
  4.1498 +(* See the Isabelle/Isar theory 'Refute.thy' for reasonable default values.  *)
  4.1499 +(* ------------------------------------------------------------------------- *)
  4.1500 +
  4.1501 +	(* theory -> (string * string) list -> Term.term -> unit *)
  4.1502 +
  4.1503 +	fun find_model thy params t =
  4.1504 +	let
  4.1505 +		(* (string * string) list * (string * string) list -> (string * string) list *)
  4.1506 +		fun add_params (parms, []) =
  4.1507 +			parms
  4.1508 +		  | add_params (parms, defparm::defparms) =
  4.1509 +			add_params (gen_ins (fn (a, b) => (fst a) = (fst b)) (defparm, parms), defparms)
  4.1510 +		(* (string * string) list * string -> int *)
  4.1511 +		fun read_int (parms, name) =
  4.1512 +			case assoc_string (parms, name) of
  4.1513 +			  Some s => (case LargeInt.fromString s of
  4.1514 +				  SOME i => i
  4.1515 +				| NONE   => error ("parameter '" ^ name ^ "' (value is '" ^ s ^ "') must be an integer value"))
  4.1516 +			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")
  4.1517 +		(* (string * string) list * string -> string *)
  4.1518 +		fun read_string (parms, name) =
  4.1519 +			case assoc_string (parms, name) of
  4.1520 +			  Some s => s
  4.1521 +			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")
  4.1522 +		(* (string * string) list *)
  4.1523 +		val allparams  = add_params (params, get_default_params thy)
  4.1524 +		(* int *)
  4.1525 +		val minsize    = read_int (allparams, "minsize")
  4.1526 +		val maxsize    = read_int (allparams, "maxsize")
  4.1527 +		val maxvars    = read_int (allparams, "maxvars")
  4.1528 +		(* string *)
  4.1529 +		val satfile    = read_string (allparams, "satfile")
  4.1530 +		val satformat  = read_string (allparams, "satformat")
  4.1531 +		val resultfile = read_string (allparams, "resultfile")
  4.1532 +		val success    = read_string (allparams, "success")
  4.1533 +		val command    = read_string (allparams, "command")
  4.1534 +		(* misc *)
  4.1535 +		val satpath    = Path.unpack satfile
  4.1536 +		val resultpath = Path.unpack resultfile
  4.1537 +		val sg         = sign_of thy
  4.1538 +		(* Term.typ list *)
  4.1539 +		val tvars      = map (fn (i,s) => TVar(i,s)) (term_tvars t)
  4.1540 +		val tfrees     = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
  4.1541 +		(* universe -> int -> bool *)
  4.1542 +		fun find_model_universe u cdepth =
  4.1543 +			let
  4.1544 +				(* given the universe 'u' and constructor depth 'cdepth', translate *)
  4.1545 +        	                (* the term 't' into a propositional formula 'fm'                   *)
  4.1546 +				val (fm,(idx,subs)) = term_to_prop_formula t u thy cdepth
  4.1547 +				val usedvars        = idx-1
  4.1548 +			in
  4.1549 +				(* 'maxvars=0' means "use as many variables as necessary" *)
  4.1550 +				if usedvars>maxvars andalso maxvars<>0 then
  4.1551 +					(
  4.1552 +						(* too many variables used: terminate *)
  4.1553 +						writeln ("\nSearch terminated: " ^ (string_of_int usedvars) ^ " boolean variables used (only " ^ (string_of_int maxvars) ^ " allowed).");
  4.1554 +						true
  4.1555 +					)
  4.1556 +				else
  4.1557 +					(* pass the formula 'fm' to an external SAT solver *)
  4.1558 +					case prop_formula_sat_solver fm satpath satformat resultpath success command of
  4.1559 +					  None =>
  4.1560 +						(* no model found *)
  4.1561 +						false
  4.1562 +					| Some assignment =>
  4.1563 +						(* model found: terminate *)
  4.1564 +						(
  4.1565 +							writeln ("\nModel found:\n" ^ (string_of_universe thy u) ^ "\n" ^ (string_of_model thy u cdepth subs assignment));
  4.1566 +							true
  4.1567 +						)
  4.1568 +			end
  4.1569 +		(* universe list -> int -> bool *)
  4.1570 +		fun find_model_universes [] cdepth =
  4.1571 +			(
  4.1572 +				std_output "\n";
  4.1573 +				false
  4.1574 +			)
  4.1575 +		  | find_model_universes (u::us) cdepth =
  4.1576 +			(
  4.1577 +				std_output ".";
  4.1578 +				((if find_model_universe u cdepth then
  4.1579 +					(* terminate *)
  4.1580 +					true
  4.1581 +				else
  4.1582 +					(* continue search with the next universe *)
  4.1583 +					find_model_universes us cdepth)
  4.1584 +				handle EMPTY_DATATYPE => (std_output "[empty inductive type (constructor depth too small)]\n"; false))
  4.1585 +			)
  4.1586 +		(* int * int -> unit *)
  4.1587 +		fun find_model_from_to (min,max) =
  4.1588 +			(* 'max=0' means "search for arbitrary large models" *)
  4.1589 +			if min>max andalso max<>0 then
  4.1590 +				writeln ("Search terminated: no model found.")
  4.1591 +			else
  4.1592 +			(
  4.1593 +				std_output ("Searching for a model of size " ^ (string_of_int min));
  4.1594 +				if find_model_universes (make_universes tfrees min) min then
  4.1595 +					(* terminate *)
  4.1596 +					()
  4.1597 +				else
  4.1598 +					(* continue search with increased size *)
  4.1599 +					find_model_from_to (min+1, max)
  4.1600 +			)
  4.1601 +	in
  4.1602 +		writeln ("Trying to find a model of: " ^ (Sign.string_of_term sg t));
  4.1603 +		if tvars<>[] then
  4.1604 +			(* TODO: deal with schematic type variables in a better way, if possible *)
  4.1605 +			error "term contains schematic type variables"
  4.1606 +		else
  4.1607 +		(
  4.1608 +			if minsize<1 then
  4.1609 +				writeln ("'minsize' is less than 1; starting search with size 1.")
  4.1610 +			else
  4.1611 +				();
  4.1612 +			if maxsize<max (minsize,1) andalso maxsize<>0 then
  4.1613 +				writeln ("'maxsize' is less than 'minsize': no model found.")
  4.1614 +			else
  4.1615 +				find_model_from_to (max (minsize,1), maxsize)
  4.1616 +		)
  4.1617 +	end;
  4.1618 +
  4.1619 +(* ------------------------------------------------------------------------- *)
  4.1620 +(* refute_term: calls 'find_model' on the negation of a term                 *)
  4.1621 +(* params     : list of '(name, value)' pairs used to override default       *)
  4.1622 +(*              parameters                                                   *)
  4.1623 +(* ------------------------------------------------------------------------- *)
  4.1624 +
  4.1625 +	(* theory -> (string * string) list -> Term.term -> unit *)
  4.1626 +
  4.1627 +	fun refute_term thy params t =
  4.1628 +	let
  4.1629 +		(* TODO: schematic type variables? *)
  4.1630 +		val negation = close_vars (HOLogic.Not $ t)
  4.1631 +		(* If 't' is of type 'propT' (rather than 'boolT'), applying *)
  4.1632 +		(* 'HOLogic.Not' is not type-correct.  However, this isn't   *)
  4.1633 +		(* really a problem as long as 'find_model' still interprets *)
  4.1634 +		(* the resulting term correctly, without checking its type.  *)
  4.1635 +	in
  4.1636 +		find_model thy params negation
  4.1637 +	end;
  4.1638 +
  4.1639 +(* ------------------------------------------------------------------------- *)
  4.1640 +(* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)
  4.1641 +(* params        : list of '(name, value)' pairs used to override default    *)
  4.1642 +(*                 parameters                                                *)
  4.1643 +(* subgoal       : 0-based index specifying the subgoal number               *)
  4.1644 +(* ------------------------------------------------------------------------- *)
  4.1645 +
  4.1646 +	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
  4.1647 +
  4.1648 +	fun refute_subgoal thy params thm subgoal =
  4.1649 +		refute_term thy params (nth_elem (subgoal, prems_of thm));
  4.1650 +
  4.1651 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/refute_isar.ML	Sat Jan 10 13:35:10 2004 +0100
     5.3 @@ -0,0 +1,102 @@
     5.4 +(*  Title:      HOL/Tools/refute_isar.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Tjark Weber
     5.7 +    Copyright   2003-2004
     5.8 +
     5.9 +Adds the 'refute' and 'refute_params' commands to Isabelle/Isar's outer
    5.10 +syntax.
    5.11 +*)
    5.12 +
    5.13 +structure RefuteIsar =
    5.14 +struct
    5.15 +
    5.16 +(* ------------------------------------------------------------------------- *)
    5.17 +(* common functions for argument parsing/scanning                            *)
    5.18 +(* ------------------------------------------------------------------------- *)
    5.19 +
    5.20 +(* ------------------------------------------------------------------------- *)
    5.21 +(* both 'refute' and 'refute_params' take an optional list of arguments of   *)
    5.22 +(* the form [name1=value1, name2=value2, ...]                                *)
    5.23 +(* ------------------------------------------------------------------------- *)
    5.24 +
    5.25 +	fun repeatd delim scan = scan -- Scan.repeat (OuterParse.$$$ delim |-- scan) >> op :: || Scan.succeed [];
    5.26 +
    5.27 +	val scan_parm = (OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name));
    5.28 +
    5.29 +	val scan_parms = Scan.option (OuterParse.$$$ "[" |-- (repeatd "," scan_parm) --| OuterParse.$$$ "]");
    5.30 +
    5.31 +(* ------------------------------------------------------------------------- *)
    5.32 +(* set up the 'refute' command                                               *)
    5.33 +(* ------------------------------------------------------------------------- *)
    5.34 +
    5.35 +(* ------------------------------------------------------------------------- *)
    5.36 +(* 'refute' takes an optional list of parameters, followed by an optional    *)
    5.37 +(* subgoal number                                                            *)
    5.38 +(* ------------------------------------------------------------------------- *)
    5.39 +
    5.40 +	val refute_scan_args = scan_parms -- (Scan.option OuterParse.nat);
    5.41 +
    5.42 +(* ------------------------------------------------------------------------- *)
    5.43 +(* the 'refute' command is mapped to 'Refute.refute_subgoal'                 *)
    5.44 +(* ------------------------------------------------------------------------- *)
    5.45 +
    5.46 +	fun refute_trans args =
    5.47 +		Toplevel.keep
    5.48 +			(fn state =>
    5.49 +				(let
    5.50 +					val (parms, subgoal) = args
    5.51 +					val thy              = (Toplevel.theory_of state)
    5.52 +					val thm              = ((snd o snd) (Proof.get_goal (Toplevel.proof_of state)))
    5.53 +				in
    5.54 +					Refute.refute_subgoal thy (if_none parms []) thm ((if_none subgoal 1)-1)
    5.55 +				end)
    5.56 +			);
    5.57 +
    5.58 +	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
    5.59 +
    5.60 +	val refute_cmd = OuterSyntax.improper_command "refute" "try to find a model that refutes a given subgoal" OuterSyntax.Keyword.diag refute_parser;
    5.61 +
    5.62 +(* ------------------------------------------------------------------------- *)
    5.63 +(* set up the 'refute_params' command                                        *)
    5.64 +(* ------------------------------------------------------------------------- *)
    5.65 +
    5.66 +(* ------------------------------------------------------------------------- *)
    5.67 +(* 'refute_params' takes an optional list of parameters                      *)
    5.68 +(* ------------------------------------------------------------------------- *)
    5.69 +
    5.70 +	val refute_params_scan_args = scan_parms;
    5.71 +
    5.72 +(* ------------------------------------------------------------------------- *)
    5.73 +(* the 'refute_params' command is mapped to (multiple calls of)              *)
    5.74 +(* 'Refute.set_default_param'; then the (new) default parameters are         *)
    5.75 +(* displayed                                                                 *)
    5.76 +(* ------------------------------------------------------------------------- *)
    5.77 +
    5.78 +	fun refute_params_trans args =
    5.79 +		let
    5.80 +			fun add_params (thy, []) = thy
    5.81 +				| add_params (thy, p::ps) = add_params (Refute.set_default_param p thy, ps)
    5.82 +		in
    5.83 +			Toplevel.theory (fn thy =>
    5.84 +				let
    5.85 +					val thy'               = add_params (thy, (if_none args []))
    5.86 +					val new_default_params = Refute.get_default_params thy'
    5.87 +					val output             = if new_default_params=[] then "none" else (space_implode "\n" (map (fn (name,value) => name ^ "=" ^ value) new_default_params))
    5.88 +				in
    5.89 +					writeln ("Default parameters for 'refute':\n" ^ output);
    5.90 +					thy'
    5.91 +				end)
    5.92 +		end;
    5.93 +
    5.94 +	fun refute_params_parser tokens = (refute_params_scan_args tokens) |>> refute_params_trans;
    5.95 +
    5.96 +	val refute_params_cmd = OuterSyntax.command "refute_params" "show/store default parameters for the 'refute' command" OuterSyntax.Keyword.thy_decl refute_params_parser;
    5.97 +
    5.98 +end;
    5.99 +
   5.100 +(* ------------------------------------------------------------------------- *)
   5.101 +(* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's  *)
   5.102 +(* outer syntax                                                              *)
   5.103 +(* ------------------------------------------------------------------------- *)
   5.104 +
   5.105 +OuterSyntax.add_parsers [RefuteIsar.refute_cmd, RefuteIsar.refute_params_cmd];
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/ex/Refute_Examples.thy	Sat Jan 10 13:35:10 2004 +0100
     6.3 @@ -0,0 +1,523 @@
     6.4 +(*  Title:      HOL/ex/Refute_Examples.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Tjark Weber
     6.7 +    Copyright   2003-2004
     6.8 +*)
     6.9 +
    6.10 +(* See 'HOL/Refute.thy' for help. *)
    6.11 +
    6.12 +header {* Examples for the 'refute' command *}
    6.13 +
    6.14 +theory Refute_Examples = Main:
    6.15 +
    6.16 +section {* 'refute': General usage *}
    6.17 +
    6.18 +lemma "P"
    6.19 +  refute
    6.20 +oops
    6.21 +
    6.22 +lemma "P \<and> Q"
    6.23 +  apply (rule conjI)
    6.24 +  refute 1  -- {* refutes @{term "P"} *}
    6.25 +  refute 2  -- {* refutes @{term "Q"} *}
    6.26 +  refute    -- {* equivalent to 'refute 1' *}
    6.27 +  -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
    6.28 +  refute [maxsize=5]     -- {* we can override parameters \<dots> *}
    6.29 +  refute [satformat="cnf"] 2  -- {* \<dots> and specify a subgoal at the same time *}
    6.30 +oops
    6.31 +
    6.32 +section {* Examples / Test cases *}
    6.33 +
    6.34 +subsection {* Propositional logic *}
    6.35 +
    6.36 +lemma "True"
    6.37 +  refute
    6.38 +  apply auto
    6.39 +done
    6.40 +
    6.41 +lemma "False"
    6.42 +  refute
    6.43 +oops
    6.44 +
    6.45 +lemma "P"
    6.46 +  refute
    6.47 +oops
    6.48 +
    6.49 +lemma "~ P"
    6.50 +  refute
    6.51 +oops
    6.52 +
    6.53 +lemma "P & Q"
    6.54 +  refute
    6.55 +oops
    6.56 +
    6.57 +lemma "P | Q"
    6.58 +  refute
    6.59 +oops
    6.60 +
    6.61 +lemma "P \<longrightarrow> Q"
    6.62 +  refute
    6.63 +oops
    6.64 +
    6.65 +lemma "(P::bool) = Q"
    6.66 +  refute
    6.67 +oops
    6.68 +
    6.69 +lemma "(P | Q) \<longrightarrow> (P & Q)"
    6.70 +  refute
    6.71 +oops
    6.72 +
    6.73 +subsection {* Predicate logic *}
    6.74 +
    6.75 +lemma "P x"
    6.76 +  refute
    6.77 +oops
    6.78 +
    6.79 +lemma "P a b c d"
    6.80 +  refute
    6.81 +oops
    6.82 +
    6.83 +lemma "P x y \<longrightarrow> P y x"
    6.84 +  refute
    6.85 +oops
    6.86 +
    6.87 +subsection {* Equality *}
    6.88 +
    6.89 +lemma "P = True"
    6.90 +  refute
    6.91 +oops
    6.92 +
    6.93 +lemma "P = False"
    6.94 +  refute
    6.95 +oops
    6.96 +
    6.97 +lemma "x = y"
    6.98 +  refute
    6.99 +oops
   6.100 +
   6.101 +lemma "f x = g x"
   6.102 +  refute
   6.103 +oops
   6.104 +
   6.105 +lemma "(f::'a\<Rightarrow>'b) = g"
   6.106 +  refute
   6.107 +oops
   6.108 +
   6.109 +lemma "(f::('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
   6.110 +  refute
   6.111 +oops
   6.112 +
   6.113 +lemma "distinct [a,b]"
   6.114 +  apply simp
   6.115 +  refute
   6.116 +oops
   6.117 +
   6.118 +subsection {* First-Order Logic *}
   6.119 +
   6.120 +lemma "\<exists>x. P x"
   6.121 +  refute
   6.122 +oops
   6.123 +
   6.124 +lemma "\<forall>x. P x"
   6.125 +  refute
   6.126 +oops
   6.127 +
   6.128 +lemma "EX! x. P x"
   6.129 +  refute
   6.130 +oops
   6.131 +
   6.132 +lemma "Ex P"
   6.133 +  refute
   6.134 +oops
   6.135 +
   6.136 +lemma "All P"
   6.137 +  refute
   6.138 +oops
   6.139 +
   6.140 +lemma "Ex1 P"
   6.141 +  refute
   6.142 +oops
   6.143 +
   6.144 +lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
   6.145 +  refute
   6.146 +oops
   6.147 +
   6.148 +lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
   6.149 +  refute
   6.150 +oops
   6.151 +
   6.152 +lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
   6.153 +  refute
   6.154 +oops
   6.155 +
   6.156 +text {* A true statement (also testing names of free and bound variables being identical) *}
   6.157 +
   6.158 +lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
   6.159 +  refute [maxsize=6]
   6.160 +  apply fast
   6.161 +done
   6.162 +
   6.163 +text {* "A type has at most 3 elements." *}
   6.164 +
   6.165 +lemma "\<forall>a b c d. a=b | a=c | a=d | b=c | b=d | c=d"
   6.166 +  refute
   6.167 +oops
   6.168 +
   6.169 +text {* "Every reflexive and symmetric relation is transitive." *}
   6.170 +
   6.171 +lemma "\<lbrakk> \<forall>x. P x x; \<forall>x y. P x y \<longrightarrow> P y x \<rbrakk> \<Longrightarrow> P x y \<longrightarrow> P y z \<longrightarrow> P x z"
   6.172 +  refute
   6.173 +oops
   6.174 +
   6.175 +text {* The "Drinker's theorem" \<dots> *}
   6.176 +
   6.177 +lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
   6.178 +  refute
   6.179 +  apply (auto simp add: ext)
   6.180 +done
   6.181 +
   6.182 +text {* \<dots> and an incorrect version of it *}
   6.183 +
   6.184 +lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
   6.185 +  refute
   6.186 +oops
   6.187 +
   6.188 +text {* "Every function has a fixed point." *}
   6.189 +
   6.190 +lemma "\<exists>x. f x = x"
   6.191 +  refute
   6.192 +oops
   6.193 +
   6.194 +text {* "Function composition is commutative." *}
   6.195 +
   6.196 +lemma "f (g x) = g (f x)"
   6.197 +  refute
   6.198 +oops
   6.199 +
   6.200 +text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *}
   6.201 +
   6.202 +lemma "((P::('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
   6.203 +  refute
   6.204 +oops
   6.205 +
   6.206 +subsection {* Higher-Order Logic *}
   6.207 +
   6.208 +lemma "\<exists>P. P"
   6.209 +  refute
   6.210 +  apply auto
   6.211 +done
   6.212 +
   6.213 +lemma "\<forall>P. P"
   6.214 +  refute
   6.215 +oops
   6.216 +
   6.217 +lemma "EX! P. P"
   6.218 +  refute
   6.219 +  apply auto
   6.220 +done
   6.221 +
   6.222 +lemma "EX! P. P x"
   6.223 +  refute
   6.224 +oops
   6.225 +
   6.226 +lemma "P Q | Q x"
   6.227 +  refute
   6.228 +oops
   6.229 +
   6.230 +text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
   6.231 +
   6.232 +constdefs
   6.233 +  "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   6.234 +  "trans P == (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
   6.235 +  "subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   6.236 +  "subset P Q == (ALL x y. P x y \<longrightarrow> Q x y)"
   6.237 +  "trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   6.238 +  "trans_closure P Q == (subset Q P) & (trans P) & (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
   6.239 +
   6.240 +lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
   6.241 +  apply (unfold trans_closure_def subset_def trans_def)
   6.242 +  refute
   6.243 +oops
   6.244 +
   6.245 +text {* "The union of transitive closures is equal to the transitive closure of unions." *}
   6.246 +
   6.247 +lemma "(\<forall>x y. (P x y | R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y | R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
   6.248 +        \<longrightarrow> trans_closure TP P
   6.249 +        \<longrightarrow> trans_closure TR R
   6.250 +        \<longrightarrow> (T x y = (TP x y | TR x y))"
   6.251 +  apply (unfold trans_closure_def trans_def subset_def)
   6.252 +  refute
   6.253 +oops
   6.254 +
   6.255 +text {* "Every surjective function is invertible." *}
   6.256 +
   6.257 +lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
   6.258 +  refute
   6.259 +oops
   6.260 +
   6.261 +text {* "Every invertible function is surjective." *}
   6.262 +
   6.263 +lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
   6.264 +  refute
   6.265 +oops
   6.266 +
   6.267 +text {* Every point is a fixed point of some function. *}
   6.268 +
   6.269 +lemma "\<exists>f. f x = x"
   6.270 +  refute [maxsize=5]
   6.271 +  apply (rule_tac x="\<lambda>x. x" in exI)
   6.272 +  apply simp
   6.273 +done
   6.274 +
   6.275 +text {* Axiom of Choice: first an incorrect version \<dots> *}
   6.276 +
   6.277 +lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
   6.278 +  refute
   6.279 +oops
   6.280 +
   6.281 +text {* \<dots> and now two correct ones *}
   6.282 +
   6.283 +lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
   6.284 +  refute
   6.285 +  apply (simp add: choice)
   6.286 +done
   6.287 +
   6.288 +lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
   6.289 +  refute [maxsize=5]
   6.290 +  apply auto
   6.291 +    apply (simp add: ex1_implies_ex choice)
   6.292 +  apply (fast intro: ext)
   6.293 +done
   6.294 +
   6.295 +subsection {* Meta-logic *}
   6.296 +
   6.297 +lemma "!!x. P x"
   6.298 +  refute
   6.299 +oops
   6.300 +
   6.301 +lemma "f x == g x"
   6.302 +  refute
   6.303 +oops
   6.304 +
   6.305 +lemma "P \<Longrightarrow> Q"
   6.306 +  refute
   6.307 +oops
   6.308 +
   6.309 +lemma "\<lbrakk> P; Q; R \<rbrakk> \<Longrightarrow> S"
   6.310 +  refute
   6.311 +oops
   6.312 +
   6.313 +subsection {* Schematic variables *}
   6.314 +
   6.315 +lemma "?P"
   6.316 +  refute
   6.317 +  apply auto
   6.318 +done
   6.319 +
   6.320 +lemma "x = ?y"
   6.321 +  refute
   6.322 +  apply auto
   6.323 +done
   6.324 +
   6.325 +subsection {* Abstractions *}
   6.326 +
   6.327 +lemma "(\<lambda>x. x) = (\<lambda>x. y)"
   6.328 +  refute
   6.329 +oops
   6.330 +
   6.331 +lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
   6.332 +  refute
   6.333 +oops
   6.334 +
   6.335 +lemma "(\<lambda>x. x) = (\<lambda>y. y)"
   6.336 +  refute
   6.337 +  apply simp
   6.338 +done
   6.339 +
   6.340 +subsection {* Sets *}
   6.341 +
   6.342 +lemma "P (A::'a set)"
   6.343 +  refute
   6.344 +oops
   6.345 +
   6.346 +lemma "P (A::'a set set)"
   6.347 +  refute
   6.348 +oops
   6.349 +
   6.350 +lemma "{x. P x} = {y. P y}"
   6.351 +  refute
   6.352 +  apply simp
   6.353 +done
   6.354 +
   6.355 +lemma "x : {x. P x}"
   6.356 +  refute
   6.357 +oops
   6.358 +
   6.359 +lemma "A Un B = A Int B"
   6.360 +  apply (unfold Un_def Int_def)
   6.361 +  refute
   6.362 +oops
   6.363 +
   6.364 +lemma "(A Int B) Un C = (A Un C) Int B"
   6.365 +  apply (unfold Un_def Int_def)
   6.366 +  refute
   6.367 +oops
   6.368 +
   6.369 +lemma "Ball A P \<longrightarrow> Bex A P"
   6.370 +  apply (unfold Ball_def Bex_def)
   6.371 +  refute
   6.372 +oops
   6.373 +
   6.374 +subsection {* (Inductive) Datatypes *}
   6.375 +
   6.376 +subsubsection {* unit *}
   6.377 +
   6.378 +lemma "P (x::unit)"
   6.379 +  refute
   6.380 +oops
   6.381 +
   6.382 +lemma "\<forall>x::unit. P x"
   6.383 +  refute
   6.384 +oops
   6.385 +
   6.386 +lemma "P ()"
   6.387 +  refute
   6.388 +oops
   6.389 +
   6.390 +subsubsection {* * *}
   6.391 +
   6.392 +lemma "P (x::'a*'b)"
   6.393 +oops
   6.394 +
   6.395 +lemma "\<forall>x::'a*'b. P x"
   6.396 +oops
   6.397 +
   6.398 +lemma "P (x,y)"
   6.399 +oops
   6.400 +
   6.401 +lemma "P (fst x)"
   6.402 +oops
   6.403 +
   6.404 +lemma "P (snd x)"
   6.405 +oops
   6.406 +
   6.407 +subsubsection {* + *}
   6.408 +
   6.409 +lemma "P (x::'a+'b)"
   6.410 +oops
   6.411 +
   6.412 +lemma "\<forall>x::'a+'b. P x"
   6.413 +oops
   6.414 +
   6.415 +lemma "P (Inl x)"
   6.416 +oops
   6.417 +
   6.418 +lemma "P (Inr x)"
   6.419 +oops
   6.420 +
   6.421 +subsubsection {* Non-recursive datatypes *}
   6.422 +
   6.423 +datatype T1 = C1
   6.424 +
   6.425 +lemma "P (x::T1)"
   6.426 +  refute
   6.427 +oops
   6.428 +
   6.429 +lemma "\<forall>x::T1. P x"
   6.430 +  refute
   6.431 +oops
   6.432 +
   6.433 +lemma "P C"
   6.434 +oops
   6.435 +
   6.436 +datatype T2 = C2 T1
   6.437 +
   6.438 +lemma "P (x::T2)"
   6.439 +  refute
   6.440 +oops
   6.441 +
   6.442 +lemma "\<forall>x::T2. P x"
   6.443 +  refute
   6.444 +oops
   6.445 +
   6.446 +lemma "P (C2 C1)"
   6.447 +oops
   6.448 +
   6.449 +lemma "P (C2 x)"
   6.450 +oops
   6.451 +
   6.452 +datatype 'a T3 = C3 'a
   6.453 +
   6.454 +lemma "P (x::'a T3)"
   6.455 +  refute
   6.456 +oops
   6.457 +
   6.458 +lemma "\<forall>x::'a T3. P x"
   6.459 +  refute
   6.460 +oops
   6.461 +
   6.462 +lemma "P (C3 x)"
   6.463 +oops
   6.464 +
   6.465 +subsubsection {* Recursive datatypes *}
   6.466 +
   6.467 +datatype Nat = Zero | Suc Nat
   6.468 +
   6.469 +lemma "P (x::Nat)"
   6.470 +  refute
   6.471 +oops
   6.472 +
   6.473 +lemma "\<forall>x::Nat. P x"
   6.474 +  refute
   6.475 +oops
   6.476 +
   6.477 +lemma "P (Suc Zero)"
   6.478 +oops
   6.479 +
   6.480 +datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
   6.481 +
   6.482 +lemma "P (x::'a BinTree)"
   6.483 +  refute
   6.484 +oops
   6.485 +
   6.486 +lemma "\<forall>x::'a BinTree. P x"
   6.487 +  refute
   6.488 +oops
   6.489 +
   6.490 +subsubsection {* Mutually recursive datatypes *}
   6.491 +
   6.492 +datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
   6.493 +     and 'a bexp = Equal "'a aexp" "'a aexp"
   6.494 +
   6.495 +lemma "P (x::'a aexp)"
   6.496 +  refute
   6.497 +oops
   6.498 +
   6.499 +lemma "\<forall>x::'a aexp. P x"
   6.500 +  refute
   6.501 +oops
   6.502 +
   6.503 +lemma "P (x::'a bexp)"
   6.504 +  refute
   6.505 +oops
   6.506 +
   6.507 +lemma "\<forall>x::'a bexp. P x"
   6.508 +  refute
   6.509 +oops
   6.510 +
   6.511 +lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
   6.512 +oops
   6.513 +
   6.514 +subsubsection {* Other datatype examples *}
   6.515 +
   6.516 +datatype InfTree = Leaf | Node "Nat \<Rightarrow> InfTree"
   6.517 +
   6.518 +lemma "P (x::InfTree)"
   6.519 +oops
   6.520 +
   6.521 +datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
   6.522 +
   6.523 +lemma "P (x::'a lambda)"
   6.524 +oops
   6.525 +
   6.526 +end