--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/refute.ML Sat Jan 10 13:35:10 2004 +0100
@@ -0,0 +1,1648 @@
+(* Title: HOL/Tools/refute.ML
+ ID: $Id$
+ Author: Tjark Weber
+ Copyright 2003-2004
+
+Finite model generation for HOL formulae, using an external SAT solver.
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Declares the 'REFUTE' signature as well as a structure 'Refute'. See *)
+(* 'find_model' below for a description of the implemented algorithm, and *)
+(* the Isabelle/Isar theories 'HOL/Refute.thy' and 'HOL/Main.thy' on how to *)
+(* set things up. *)
+(* ------------------------------------------------------------------------- *)
+
+signature REFUTE =
+sig
+
+ (* We use 'REFUTE' only for internal error conditions that should *)
+ (* never occur in the first place (i.e. errors caused by bugs in our *)
+ (* code). Otherwise (e.g. to indicate invalid input data) we use *)
+ (* 'error'. *)
+
+ exception REFUTE of string * string; (* ("in function", "cause") *)
+
+ val setup : (theory -> theory) list
+
+ val set_default_param : (string * string) -> theory -> theory
+ val get_default_param : theory -> string -> string option
+ val get_default_params : theory -> (string * string) list
+
+ val find_model : theory -> (string * string) list -> Term.term -> unit
+
+ val refute_term : theory -> (string * string) list -> Term.term -> unit
+ val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
+end;
+
+
+structure Refute : REFUTE =
+struct
+ exception REFUTE of string * string;
+
+ exception EMPTY_DATATYPE;
+
+ structure RefuteDataArgs =
+ struct
+ val name = "Refute/refute";
+ type T = string Symtab.table;
+ val empty = Symtab.empty;
+ val copy = I;
+ val prep_ext = I;
+ val merge =
+ fn (symTable1, symTable2) =>
+ (Symtab.merge (op =) (symTable1, symTable2));
+ fun print sg symTable =
+ writeln
+ ("'refute', default parameters:\n" ^
+ (space_implode "\n" (map (fn (name,value) => name ^ " = " ^ value) (Symtab.dest symTable))))
+ end;
+
+ structure RefuteData = TheoryDataFun(RefuteDataArgs);
+
+
+(* ------------------------------------------------------------------------- *)
+(* INTERFACE, PART 1: INITIALIZATION, PARAMETER MANAGEMENT *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
+(* structure *)
+(* ------------------------------------------------------------------------- *)
+
+ val setup = [RefuteData.init];
+
+(* ------------------------------------------------------------------------- *)
+(* set_default_param: stores the '(name, value)' pair in RefuteData's symbol *)
+(* table *)
+(* ------------------------------------------------------------------------- *)
+
+ fun set_default_param (name, value) thy =
+ let
+ val symTable = RefuteData.get thy
+ in
+ case Symtab.lookup (symTable, name) of
+ None => RefuteData.put (Symtab.extend (symTable, [(name, value)])) thy
+ | Some _ => RefuteData.put (Symtab.update ((name, value), symTable)) thy
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* get_default_param: retrieves the value associated with 'name' from *)
+(* RefuteData's symbol table *)
+(* ------------------------------------------------------------------------- *)
+
+ fun get_default_param thy name = Symtab.lookup (RefuteData.get thy, name);
+
+(* ------------------------------------------------------------------------- *)
+(* get_default_params: returns a list of all '(name, value)' pairs that are *)
+(* stored in RefuteData's symbol table *)
+(* ------------------------------------------------------------------------- *)
+
+ fun get_default_params thy = Symtab.dest (RefuteData.get thy);
+
+
+(* ------------------------------------------------------------------------- *)
+(* PROPOSITIONAL FORMULAS *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* prop_formula: formulas of propositional logic, built from boolean *)
+(* variables (referred to by index) and True/False using *)
+(* not/or/and *)
+(* ------------------------------------------------------------------------- *)
+
+ datatype prop_formula =
+ True
+ | False
+ | BoolVar of int
+ | Not of prop_formula
+ | Or of prop_formula * prop_formula
+ | And of prop_formula * prop_formula;
+
+ (* the following constructor functions make sure that True and False do *)
+ (* not occur within any of the other connectives (i.e. Not, Or, And) *)
+
+ (* prop_formula -> prop_formula *)
+
+ fun SNot True = False
+ | SNot False = True
+ | SNot fm = Not fm;
+
+ (* prop_formula * prop_formula -> prop_formula *)
+
+ fun SOr (True, _) = True
+ | SOr (_, True) = True
+ | SOr (False, fm) = fm
+ | SOr (fm, False) = fm
+ | SOr (fm1, fm2) = Or (fm1, fm2);
+
+ (* prop_formula * prop_formula -> prop_formula *)
+
+ fun SAnd (True, fm) = fm
+ | SAnd (fm, True) = fm
+ | SAnd (False, _) = False
+ | SAnd (_, False) = False
+ | SAnd (fm1, fm2) = And (fm1, fm2);
+
+(* ------------------------------------------------------------------------- *)
+(* list_disjunction: computes the disjunction of a list of propositional *)
+(* formulas *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_formula list -> prop_formula *)
+
+ fun list_disjunction [] = False
+ | list_disjunction (x::xs) = SOr (x, list_disjunction xs);
+
+(* ------------------------------------------------------------------------- *)
+(* list_conjunction: computes the conjunction of a list of propositional *)
+(* formulas *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_formula list -> prop_formula *)
+
+ fun list_conjunction [] = True
+ | list_conjunction (x::xs) = SAnd (x, list_conjunction xs);
+
+(* ------------------------------------------------------------------------- *)
+(* prop_formula_dot_product: [x1,...,xn] * [y1,...,yn] -> x1*y1+...+xn*yn *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_formula list * prop_formula list -> prop_formula *)
+
+ fun prop_formula_dot_product ([],[]) = False
+ | prop_formula_dot_product (x::xs,y::ys) = SOr (SAnd (x,y), prop_formula_dot_product (xs,ys))
+ | prop_formula_dot_product (_,_) = raise REFUTE ("prop_formula_dot_product", "lists are of different length");
+
+(* ------------------------------------------------------------------------- *)
+(* prop_formula_to_nnf: computes the negation normal form of a formula 'fm' *)
+(* of propositional logic (i.e. only variables may be *)
+(* negated, but not subformulas) *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_formula -> prop_formula *)
+
+ fun prop_formula_to_nnf fm =
+ case fm of
+ (* constants *)
+ True => True
+ | False => False
+ (* literals *)
+ | BoolVar i => BoolVar i
+ | Not (BoolVar i) => Not (BoolVar i)
+ (* double-negation elimination *)
+ | Not (Not fm) => prop_formula_to_nnf fm
+ (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
+ | Not (Or (fm1,fm2)) => SAnd (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
+ | Not (And (fm1,fm2)) => SOr (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
+ (* 'or' and 'and' as outermost connectives are left untouched *)
+ | Or (fm1,fm2) => SOr (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
+ | And (fm1,fm2) => SAnd (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
+ (* 'not' + constant *)
+ | Not _ => raise REFUTE ("prop_formula_to_nnf", "'True'/'False' not allowed inside of 'Not'");
+
+(* ------------------------------------------------------------------------- *)
+(* prop_formula_nnf_to_cnf: computes the conjunctive normal form of a *)
+(* formula 'fm' of propositional logic that is given in negation normal *)
+(* form. Note that there may occur an exponential blowup of the *)
+(* formula. *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_formula -> prop_formula *)
+
+ fun prop_formula_nnf_to_cnf fm =
+ case fm of
+ (* constants *)
+ True => True
+ | False => False
+ (* literals *)
+ | BoolVar i => BoolVar i
+ | Not (BoolVar i) => Not (BoolVar i)
+ (* pushing 'or' inside of 'and' using distributive laws *)
+ | Or (fm1,fm2) =>
+ let
+ val fm1' = prop_formula_nnf_to_cnf fm1
+ val fm2' = prop_formula_nnf_to_cnf fm2
+ in
+ case fm1' of
+ And (fm11,fm12) => prop_formula_nnf_to_cnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2')))
+ | _ =>
+ (case fm2' of
+ And (fm21,fm22) => prop_formula_nnf_to_cnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22)))
+ (* neither subformula contains 'and' *)
+ | _ => fm)
+ end
+ (* 'and' as outermost connective is left untouched *)
+ | And (fm1,fm2) => SAnd (prop_formula_nnf_to_cnf fm1, prop_formula_nnf_to_cnf fm2)
+ (* error *)
+ | _ => raise REFUTE ("prop_formula_nnf_to_cnf", "formula is not in negation normal form");
+
+(* ------------------------------------------------------------------------- *)
+(* max: computes the maximum of two integer values 'i' and 'j' *)
+(* ------------------------------------------------------------------------- *)
+
+ (* int * int -> int *)
+
+ fun max (i,j) =
+ if (i>j) then i else j;
+
+(* ------------------------------------------------------------------------- *)
+(* max_var_index: computes the maximal variable index occuring in 'fm', *)
+(* where 'fm' is a formula of propositional logic *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_formula -> int *)
+
+ fun max_var_index fm =
+ case fm of
+ True => 0
+ | False => 0
+ | BoolVar i => i
+ | Not fm1 => max_var_index fm1
+ | And (fm1,fm2) => max (max_var_index fm1, max_var_index fm2)
+ | Or (fm1,fm2) => max (max_var_index fm1, max_var_index fm2);
+
+(* ------------------------------------------------------------------------- *)
+(* prop_formula_nnf_to_def_cnf: computes the definitional conjunctive normal *)
+(* form of a formula 'fm' of propositional logic that is given in *)
+(* negation normal form. To avoid an exponential blowup of the *)
+(* formula, auxiliary variables may be introduced. The result formula *)
+(* is SAT-equivalent to 'fm' (i.e. it is satisfiable if and only if *)
+(* 'fm' is satisfiable). *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_formula -> prop_formula *)
+
+ fun prop_formula_nnf_to_def_cnf fm =
+ let
+ (* prop_formula * int -> prop_formula * int *)
+ fun prop_formula_nnf_to_def_cnf_new (fm,new) =
+ (* 'new' specifies the next index that is available to introduce an auxiliary variable *)
+ case fm of
+ (* constants *)
+ True => (True, new)
+ | False => (False, new)
+ (* literals *)
+ | BoolVar i => (BoolVar i, new)
+ | Not (BoolVar i) => (Not (BoolVar i), new)
+ (* pushing 'or' inside of 'and' using distributive laws *)
+ | Or (fm1,fm2) =>
+ let
+ val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
+ val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
+ in
+ case fst fm1' of
+ And (fm11,fm12) =>
+ let
+ val aux = BoolVar (snd fm2')
+ in
+ (* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *)
+ prop_formula_nnf_to_def_cnf_new (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fst fm2', Not aux)), (snd fm2')+1)
+ end
+ | _ =>
+ (case fst fm2' of
+ And (fm21,fm22) =>
+ let
+ val aux = BoolVar (snd fm2')
+ in
+ (* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *)
+ prop_formula_nnf_to_def_cnf_new (SAnd (SOr (fst fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), (snd fm2')+1)
+ end
+ (* neither subformula contains 'and' *)
+ | _ => (fm, new))
+ end
+ (* 'and' as outermost connective is left untouched *)
+ | And (fm1,fm2) =>
+ let
+ val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
+ val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
+ in
+ (SAnd (fst fm1', fst fm2'), snd fm2')
+ end
+ (* error *)
+ | _ => raise REFUTE ("prop_formula_nnf_to_def_cnf", "formula is not in negation normal form")
+ in
+ fst (prop_formula_nnf_to_def_cnf_new (fm, (max_var_index fm)+1))
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* prop_formula_to_cnf: computes the conjunctive normal form of a formula *)
+(* 'fm' of propositional logic *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_formula -> prop_formula *)
+
+ fun prop_formula_to_cnf fm =
+ prop_formula_nnf_to_cnf (prop_formula_to_nnf fm);
+
+(* ------------------------------------------------------------------------- *)
+(* prop_formula_to_def_cnf: computes the definitional conjunctive normal *)
+(* form of a formula 'fm' of propositional logic, introducing auxiliary *)
+(* variables if necessary to avoid an exponential blowup of the formula *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_formula -> prop_formula *)
+
+ fun prop_formula_to_def_cnf fm =
+ prop_formula_nnf_to_def_cnf (prop_formula_to_nnf fm);
+
+(* ------------------------------------------------------------------------- *)
+(* prop_formula_to_dimacs_cnf_format: serializes a formula of propositional *)
+(* logic to a file in DIMACS CNF format (see "Satisfiability Suggested *)
+(* Format", May 8 1993, Section 2.1) *)
+(* fm : formula to be serialized. Note: 'fm' must not contain a variable *)
+(* index less than 1. *)
+(* def : If true, translate 'fm' into definitional CNF. Otherwise translate *)
+(* 'fm' into CNF. *)
+(* path: path of the file to be created *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_formula -> bool -> Path.T -> unit *)
+
+ fun prop_formula_to_dimacs_cnf_format fm def path =
+ let
+ (* prop_formula *)
+ val cnf =
+ if def then
+ prop_formula_to_def_cnf fm
+ else
+ prop_formula_to_cnf fm
+ val fm' =
+ case cnf of
+ True => Or (BoolVar 1, Not (BoolVar 1))
+ | False => And (BoolVar 1, Not (BoolVar 1))
+ | _ => cnf (* either 'cnf'=True/False, or 'cnf' does not contain True/False at all *)
+ (* prop_formula -> int *)
+ fun cnf_number_of_clauses (And (fm1,fm2)) =
+ (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
+ | cnf_number_of_clauses _ =
+ 1
+ (* prop_formula -> string *)
+ fun cnf_prop_formula_to_string (BoolVar i) =
+ if (i<1) then
+ raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains a variable index less than 1")
+ else
+ (string_of_int i)
+ | cnf_prop_formula_to_string (Not fm1) =
+ "-" ^ (cnf_prop_formula_to_string fm1)
+ | cnf_prop_formula_to_string (Or (fm1,fm2)) =
+ (cnf_prop_formula_to_string fm1) ^ " " ^ (cnf_prop_formula_to_string fm2)
+ | cnf_prop_formula_to_string (And (fm1,fm2)) =
+ (cnf_prop_formula_to_string fm1) ^ " 0\n" ^ (cnf_prop_formula_to_string fm2)
+ | cnf_prop_formula_to_string _ =
+ raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains True/False")
+ in
+ File.write path ("c This file was generated by prop_formula_to_dimacs_cnf_format\n"
+ ^ "c (c) Tjark Weber\n"
+ ^ "p cnf " ^ (string_of_int (max_var_index fm')) ^ " " ^ (string_of_int (cnf_number_of_clauses fm')) ^ "\n"
+ ^ (cnf_prop_formula_to_string fm') ^ "\n")
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* prop_formula_to_dimacs_sat_format: serializes a formula of propositional *)
+(* logic to a file in DIMACS SAT format (see "Satisfiability Suggested *)
+(* Format", May 8 1993, Section 2.2) *)
+(* fm : formula to be serialized. Note: 'fm' must not contain a variable *)
+(* index less than 1. *)
+(* path: path of the file to be created *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_formula -> Path.T -> unit *)
+
+ fun prop_formula_to_dimacs_sat_format fm path =
+ let
+ fun prop_formula_to_string True =
+ "*()"
+ | prop_formula_to_string False =
+ "+()"
+ | prop_formula_to_string (BoolVar i) =
+ if (i<1) then
+ raise REFUTE ("prop_formula_to_dimacs_sat_format", "formula contains a variable index less than 1")
+ else
+ (string_of_int i)
+ | prop_formula_to_string (Not fm1) =
+ "-(" ^ (prop_formula_to_string fm1) ^ ")"
+ | prop_formula_to_string (Or (fm1,fm2)) =
+ "+(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
+ | prop_formula_to_string (And (fm1,fm2)) =
+ "*(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
+ in
+ File.write path ("c This file was generated by prop_formula_to_dimacs_sat_format\n"
+ ^ "c (c) Tjark Weber\n"
+ ^ "p sat " ^ (string_of_int (max (max_var_index fm, 1))) ^ "\n"
+ ^ "(" ^ (prop_formula_to_string fm) ^ ")\n")
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* prop_formula_sat_solver: try to find a satisfying assignment for the *)
+(* boolean variables in a propositional formula, using an external SAT *)
+(* solver. If the SAT solver did not find an assignment, 'None' is *)
+(* returned. Otherwise 'Some (list of integers)' is returned, where *)
+(* i>0 means that the boolean variable i is set to TRUE, and i<0 means *)
+(* that the boolean variable i is set to FALSE. Note that if *)
+(* 'satformat' is 'defcnf', then the assignment returned may contain *)
+(* auxiliary variables that were not present in the original formula *)
+(* 'fm'. *)
+(* fm : formula that is passed to the SAT solver *)
+(* satpath : path of the file used to store the propositional formula, *)
+(* i.e. the input to the SAT solver *)
+(* satformat : format of the SAT solver's input file. Must be either "cnf", *)
+(* "defcnf", or "sat". *)
+(* resultpath: path of the file containing the SAT solver's output *)
+(* success : part of the line in the SAT solver's output that is followed *)
+(* by a line consisting of a list of integers representing the *)
+(* satisfying assignment *)
+(* command : system command used to execute the SAT solver *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_formula -> Path.T -> string -> Path.T -> string -> string -> int list option *)
+
+ fun prop_formula_sat_solver fm satpath satformat resultpath success command =
+ if File.exists satpath then
+ error ("file '" ^ (Path.pack satpath) ^ "' exists, please delete (will not overwrite)")
+ else if File.exists resultpath then
+ error ("file '" ^ (Path.pack resultpath) ^ "' exists, please delete (will not overwrite)")
+ else
+ (
+ (* serialize the formula 'fm' to a file *)
+ if satformat="cnf" then
+ prop_formula_to_dimacs_cnf_format fm false satpath
+ else if satformat="defcnf" then
+ prop_formula_to_dimacs_cnf_format fm true satpath
+ else if satformat="sat" then
+ prop_formula_to_dimacs_sat_format fm satpath
+ else
+ error ("invalid argument: satformat='" ^ satformat ^ "' (must be either 'cnf', 'defcnf', or 'sat')");
+ (* execute SAT solver *)
+ if (system command)<>0 then
+ (
+ (* error executing SAT solver *)
+ File.rm satpath;
+ File.rm resultpath;
+ error ("system command '" ^ command ^ "' failed (make sure a SAT solver is installed)")
+ )
+ else
+ (
+ (* read assignment from the result file *)
+ File.rm satpath;
+ let
+ (* 'a option -> 'a Library.option *)
+ fun option (SOME a) =
+ Some a
+ | option NONE =
+ None
+ (* string -> int list *)
+ fun string_to_int_list s =
+ mapfilter (option o LargeInt.fromString) (space_explode " " s)
+ (* string -> string -> bool *)
+ fun is_substring s1 s2 =
+ let
+ val length1 = String.size s1
+ val length2 = String.size s2
+ in
+ if length2 < length1 then
+ false
+ else if s1 = String.substring (s2, 0, length1) then
+ true
+ else is_substring s1 (String.substring (s2, 1, length2-1))
+ end
+ (* string list -> int list option *)
+ fun extract_solution [] =
+ None
+ | extract_solution (line::lines) =
+ if is_substring success line then
+ (* the next line must be a list of integers *)
+ Some (string_to_int_list (hd lines))
+ else
+ extract_solution lines
+ val sat_result = File.read resultpath
+ in
+ File.rm resultpath;
+ extract_solution (split_lines sat_result)
+ end
+ )
+ );
+
+
+(* ------------------------------------------------------------------------- *)
+(* TREES *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* tree: implements an arbitrarily (but finitely) branching tree as a list *)
+(* of (lists of ...) elements *)
+(* ------------------------------------------------------------------------- *)
+
+ datatype 'a tree =
+ Leaf of 'a
+ | Node of ('a tree) list;
+
+ type prop_tree =
+ prop_formula list tree;
+
+ (* ('a -> 'b) -> 'a tree -> 'b tree *)
+
+ fun tree_map f tr =
+ case tr of
+ Leaf x => Leaf (f x)
+ | Node xs => Node (map (tree_map f) xs);
+
+ (* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)
+
+ fun tree_foldl f =
+ let
+ fun itl (e, Leaf x) = f(e,x)
+ | itl (e, Node xs) = foldl (tree_foldl f) (e,xs)
+ in
+ itl
+ end;
+
+ (* 'a tree * 'b tree -> ('a * 'b) tree *)
+
+ fun tree_pair (t1,t2) =
+ case t1 of
+ Leaf x =>
+ (case t2 of
+ Leaf y => Leaf (x,y)
+ | Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)"))
+ | Node xs =>
+ (case t2 of
+ (* '~~' will raise an exception if the number of branches in both trees is different at the current node *)
+ Node ys => Node (map tree_pair (xs ~~ ys))
+ | Leaf _ => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
+
+(* ------------------------------------------------------------------------- *)
+(* prop_tree_to_true: returns a propositional formula that is true iff the *)
+(* tree denotes the boolean value TRUE *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_tree -> prop_formula *)
+
+ (* a term of type 'bool' is represented as a 2-element leaf, where *)
+ (* the term is true iff the leaf's first element is true *)
+
+ fun prop_tree_to_true (Leaf [fm,_]) =
+ fm
+ | prop_tree_to_true _ =
+ raise REFUTE ("prop_tree_to_true", "tree is not a 2-element leaf");
+
+(* ------------------------------------------------------------------------- *)
+(* prop_tree_to_false: returns a propositional formula that is true iff the *)
+(* tree denotes the boolean value FALSE *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_tree -> prop_formula *)
+
+ (* a term of type 'bool' is represented as a 2-element leaf, where *)
+ (* the term is false iff the leaf's second element is true *)
+
+ fun prop_tree_to_false (Leaf [_,fm]) =
+ fm
+ | prop_tree_to_false _ =
+ raise REFUTE ("prop_tree_to_false", "tree is not a 2-element leaf");
+
+(* ------------------------------------------------------------------------- *)
+(* restrict_to_single_element: returns a propositional formula which is true *)
+(* iff the tree 'tr' describes a single element of its corresponding *)
+(* type, i.e. iff at each leaf, one and only one formula is true *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_tree -> prop_formula *)
+
+ fun restrict_to_single_element tr =
+ let
+ (* prop_formula list -> prop_formula *)
+ fun allfalse [] = True
+ | allfalse (x::xs) = SAnd (SNot x, allfalse xs)
+ (* prop_formula list -> prop_formula *)
+ fun exactly1true [] = False
+ | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
+ in
+ case tr of
+ Leaf [BoolVar _, Not (BoolVar _)] => True (* optimization for boolean variables *)
+ | Leaf xs => exactly1true xs
+ | Node trees => list_conjunction (map restrict_to_single_element trees)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* HOL FORMULAS *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* absvar: form an abstraction over a schematic variable *)
+(* ------------------------------------------------------------------------- *)
+
+ (* Term.indexname * Term.typ * Term.term -> Term.term *)
+
+ (* this function is similar to Term.absfree, but for schematic *)
+ (* variables (rather than free variables) *)
+ fun absvar ((x,i),T,body) =
+ Abs(x, T, abstract_over (Var((x,i),T), body));
+
+(* ------------------------------------------------------------------------- *)
+(* list_all_var: quantification over a list of schematic variables *)
+(* ------------------------------------------------------------------------- *)
+
+ (* (Term.indexname * Term.typ) list * Term.term -> Term.term *)
+
+ (* this function is similar to Term.list_all_free, but for schematic *)
+ (* variables (rather than free variables) *)
+ fun list_all_var ([], t) =
+ t
+ | list_all_var ((idx,T)::vars, t) =
+ (all T) $ (absvar(idx, T, list_all_var(vars,t)));
+
+(* ------------------------------------------------------------------------- *)
+(* close_vars: close up a formula over all schematic variables by *)
+(* quantification (note that the result term may still contain *)
+(* (non-schematic) free variables) *)
+(* ------------------------------------------------------------------------- *)
+
+ (* Term.term -> Term.term *)
+
+ (* this function is similar to Logic.close_form, but for schematic *)
+ (* variables (rather than free variables) *)
+ fun close_vars A =
+ list_all_var (sort_wrt (fst o fst) (map dest_Var (term_vars A)), A);
+
+(* ------------------------------------------------------------------------- *)
+(* make_universes: given a list 'xs' of "types" and a universe size 'size', *)
+(* this function returns all possible partitions of the universe into *)
+(* the "types" in 'xs' such that no "type" is empty. If 'size' is less *)
+(* than 'length xs', the returned list of partitions is empty. *)
+(* Otherwise, if the list 'xs' is empty, then the returned list of *)
+(* partitions contains only the empty list, regardless of 'size'. *)
+(* ------------------------------------------------------------------------- *)
+
+ (* 'a list -> int -> ('a * int) list list *)
+
+ fun make_universes xs size =
+ let
+ (* 'a list -> int -> int -> ('a * int) list list *)
+ fun make_partitions_loop (x::xs) 0 total =
+ map (fn us => ((x,0)::us)) (make_partitions xs total)
+ | make_partitions_loop (x::xs) first total =
+ (map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
+ | make_partitions_loop _ _ _ =
+ raise REFUTE ("make_universes::make_partitions_loop", "empty list")
+ and
+ (* 'a list -> int -> ('a * int) list list *)
+ make_partitions [x] size =
+ (* we must use all remaining elements on the type 'x', so there is only one partition *)
+ [[(x,size)]]
+ | make_partitions (x::xs) 0 =
+ (* there are no elements left in the universe, so there is only one partition *)
+ [map (fn t => (t,0)) (x::xs)]
+ | make_partitions (x::xs) size =
+ (* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
+ make_partitions_loop (x::xs) size size
+ | make_partitions _ _ =
+ raise REFUTE ("make_universes::make_partitions", "empty list")
+ val len = length xs
+ in
+ if size<len then
+ (* the universe isn't big enough to make every type non-empty *)
+ []
+ else if xs=[] then
+ (* no types: return one universe, regardless of the size *)
+ [[]]
+ else
+ (* partition into possibly empty types, then add 1 element to each type *)
+ map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* sum: computes the sum of a list of integers; sum [] = 0 *)
+(* ------------------------------------------------------------------------- *)
+
+ (* int list -> int *)
+
+ fun sum xs = foldl (op +) (0, xs);
+
+(* ------------------------------------------------------------------------- *)
+(* product: computes the product of a list of integers; product [] = 1 *)
+(* ------------------------------------------------------------------------- *)
+
+ (* int list -> int *)
+
+ fun product xs = foldl (op *) (1, xs);
+
+(* ------------------------------------------------------------------------- *)
+(* power: power(a,b) computes a^b, for a>=0, b>=0 *)
+(* ------------------------------------------------------------------------- *)
+
+ (* int * int -> int *)
+
+ fun power (a,0) = 1
+ | power (a,1) = a
+ | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end;
+
+(* ------------------------------------------------------------------------- *)
+(* size_of_type: returns the size of a type, where 'us' specifies the size *)
+(* of each basic type (i.e. each type variable), and 'cdepth' specifies *)
+(* the maximal constructor depth for inductive datatypes *)
+(* ------------------------------------------------------------------------- *)
+
+ (* Term.typ -> (Term.typ * int) list -> theory -> int -> int *)
+
+ fun size_of_type T us thy cdepth =
+ let
+ (* Term.typ -> (Term.typ * int) -> int *)
+ fun lookup_size T [] =
+ raise REFUTE ("size_of_type", "no size specified for type variable '" ^ (Sign.string_of_typ (sign_of thy) T) ^ "'")
+ | lookup_size T ((typ,size)::pairs) =
+ if T=typ then size else lookup_size T pairs
+ in
+ case T of
+ Type ("prop", []) => 2
+ | Type ("bool", []) => 2
+ | Type ("Product_Type.unit", []) => 1
+ | Type ("+", [T1,T2]) => (size_of_type T1 us thy cdepth) + (size_of_type T2 us thy cdepth)
+ | Type ("*", [T1,T2]) => (size_of_type T1 us thy cdepth) * (size_of_type T2 us thy cdepth)
+ | Type ("fun", [T1,T2]) => power (size_of_type T2 us thy cdepth, size_of_type T1 us thy cdepth)
+ | Type ("set", [T1]) => size_of_type (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
+ | Type (s, Ts) =>
+ (case DatatypePackage.datatype_info thy s of
+ Some info => (* inductive datatype *)
+ if cdepth>0 then
+ let
+ val index = #index info
+ val descr = #descr info
+ val (_, dtyps, constrs) = the (assoc (descr, index))
+ val Typs = dtyps ~~ Ts
+ (* DatatypeAux.dtyp -> Term.typ *)
+ fun typ_of_dtyp (DatatypeAux.DtTFree a) =
+ the (assoc (Typs, DatatypeAux.DtTFree a))
+ | typ_of_dtyp (DatatypeAux.DtRec i) =
+ let
+ val (s, ds, _) = the (assoc (descr, i))
+ in
+ Type (s, map typ_of_dtyp ds)
+ end
+ | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
+ Type (s, map typ_of_dtyp ds)
+ in
+ sum (map (fn (_,ds) => product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)) constrs)
+ end
+ else 0
+ | None => error ("size_of_type: type contains an unknown type constructor: '" ^ s ^ "'"))
+ | TFree _ => lookup_size T us
+ | TVar _ => lookup_size T us
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* type_to_prop_tree: creates a tree of boolean variables that denotes an *)
+(* element of the type 'T'. The height and branching factor of the *)
+(* tree depend on the size and "structure" of 'T'. *)
+(* 'us' : a "universe" specifying the number of elements for each basic type *)
+(* (i.e. each type variable) in 'T' *)
+(* 'cdepth': maximum constructor depth to be used for inductive datatypes *)
+(* 'idx': the next index to be used for a boolean variable *)
+(* ------------------------------------------------------------------------- *)
+
+ (* Term.typ -> (Term.typ * int) list -> theory -> int -> int -> prop_tree * int *)
+
+ fun type_to_prop_tree T us thy cdepth idx =
+ let
+ (* int -> Term.typ -> int -> prop_tree list * int *)
+ fun type_to_prop_tree_list 1 T' idx' =
+ let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
+ ([tr], newidx)
+ end
+ | type_to_prop_tree_list n T' idx' =
+ let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
+ let val (trees, lastidx) = type_to_prop_tree_list (n-1) T' newidx in
+ (tr::trees, lastidx)
+ end
+ end
+ in
+ case T of
+ Type ("prop", []) =>
+ (Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
+ | Type ("bool", []) =>
+ (Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
+ | Type ("Product_Type.unit", []) =>
+ (Leaf [True], idx)
+ | Type ("+", [T1,T2]) =>
+ let
+ val s1 = size_of_type T1 us thy cdepth
+ val s2 = size_of_type T2 us thy cdepth
+ val s = s1 + s2
+ in
+ if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
+ raise EMPTY_DATATYPE
+ else
+ error "sum types (+) not implemented yet (TODO)"
+ end
+ | Type ("*", [T1,T2]) =>
+ let
+ val s1 = size_of_type T1 us thy cdepth
+ val s2 = size_of_type T2 us thy cdepth
+ val s = s1 * s2
+ in
+ if s1=0 orelse s2=0 then
+ raise EMPTY_DATATYPE
+ else
+ error "product types (*) not implemented yet (TODO)"
+ end
+ | Type ("fun", [T1,T2]) =>
+ (* we create 'size_of_type T1' different copies of the tree for 'T2', *)
+ (* which are then combined into a single new tree *)
+ let
+ val s = size_of_type T1 us thy cdepth
+ in
+ if s=0 then
+ raise EMPTY_DATATYPE
+ else
+ let val (trees, newidx) = type_to_prop_tree_list s T2 idx in
+ (Node trees, newidx)
+ end
+ end
+ | Type ("set", [T1]) =>
+ type_to_prop_tree (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth idx
+ | Type (s, _) =>
+ (case DatatypePackage.constrs_of thy s of
+ Some _ => (* inductive datatype *)
+ let
+ val s = size_of_type T us thy cdepth
+ in
+ if s=0 then
+ raise EMPTY_DATATYPE
+ else
+ (Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
+ end
+ | None => error ("type_to_prop_tree: type contains an unknown type constructor: '" ^ s ^ "'"))
+ | TFree _ =>
+ let val s = size_of_type T us thy cdepth in
+ (Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
+ end
+ | TVar _ =>
+ let val s = size_of_type T us thy cdepth in
+ (Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* type_to_constants: creates a list of prop_trees with constants (True, *)
+(* False) rather than boolean variables, one for every element in the *)
+(* type 'T'; c.f. type_to_prop_tree *)
+(* ------------------------------------------------------------------------- *)
+
+ (* Term.typ -> (Term.typ * int) list -> theory -> int -> prop_tree list *)
+
+ fun type_to_constants T us thy cdepth =
+ let
+ (* returns a list with all unit vectors of length n *)
+ (* int -> prop_tree list *)
+ fun unit_vectors n =
+ let
+ (* returns the k-th unit vector of length n *)
+ (* int * int -> prop_tree *)
+ fun unit_vector (k,n) =
+ Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
+ (* int -> prop_tree list -> prop_tree list *)
+ fun unit_vectors_acc k vs =
+ if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
+ in
+ unit_vectors_acc 1 []
+ end
+ (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
+ (* 'a -> 'a list list -> 'a list list *)
+ fun cons_list x xss =
+ map (fn xs => x::xs) xss
+ (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
+ (* int -> 'a list -> 'a list list *)
+ fun pick_all 1 xs =
+ map (fn x => [x]) xs
+ | pick_all n xs =
+ let val rec_pick = pick_all (n-1) xs in
+ foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
+ end
+ in
+ case T of
+ Type ("prop", []) => unit_vectors 2
+ | Type ("bool", []) => unit_vectors 2
+ | Type ("Product_Type.unit", []) => unit_vectors 1
+ | Type ("+", [T1,T2]) =>
+ let
+ val s1 = size_of_type T1 us thy cdepth
+ val s2 = size_of_type T2 us thy cdepth
+ in
+ if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
+ raise EMPTY_DATATYPE
+ else
+ error "sum types (+) not implemented yet (TODO)"
+ end
+ | Type ("*", [T1,T2]) =>
+ let
+ val s1 = size_of_type T1 us thy cdepth
+ val s2 = size_of_type T2 us thy cdepth
+ in
+ if s1=0 orelse s2=0 then
+ raise EMPTY_DATATYPE
+ else
+ error "product types (*) not implemented yet (TODO)"
+ end
+ | Type ("fun", [T1,T2]) =>
+ let
+ val s = size_of_type T1 us thy cdepth
+ in
+ if s=0 then
+ raise EMPTY_DATATYPE
+ else
+ map (fn xs => Node xs) (pick_all s (type_to_constants T2 us thy cdepth))
+ end
+ | Type ("set", [T1]) => type_to_constants (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
+ | Type (s, _) =>
+ (case DatatypePackage.constrs_of thy s of
+ Some _ => (* inductive datatype *)
+ let
+ val s = size_of_type T us thy cdepth
+ in
+ if s=0 then
+ raise EMPTY_DATATYPE
+ else
+ unit_vectors s
+ end
+ | None => error ("type_to_constants: type contains an unknown type constructor: '" ^ s ^ "'"))
+ | TFree _ => unit_vectors (size_of_type T us thy cdepth)
+ | TVar _ => unit_vectors (size_of_type T us thy cdepth)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* prop_tree_equal: returns a propositional formula that is true iff 'tr1' *)
+(* and 'tr2' both denote the same element *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_tree * prop_tree -> prop_formula *)
+
+ fun prop_tree_equal (tr1,tr2) =
+ case tr1 of
+ Leaf x =>
+ (case tr2 of
+ Leaf y => prop_formula_dot_product (x,y)
+ | _ => raise REFUTE ("prop_tree_equal", "second tree is higher"))
+ | Node xs =>
+ (case tr2 of
+ Leaf _ => raise REFUTE ("prop_tree_equal", "first tree is higher")
+ (* extensionality: two functions are equal iff they are equal for every element *)
+ | Node ys => list_conjunction (map prop_tree_equal (xs ~~ ys)));
+
+(* ------------------------------------------------------------------------- *)
+(* prop_tree_apply: returns a tree that denotes the element obtained by *)
+(* applying the function which is denoted by the tree 't1' to the *)
+(* element which is denoted by the tree 't2' *)
+(* ------------------------------------------------------------------------- *)
+
+ (* prop_tree * prop_tree -> prop_tree *)
+
+ fun prop_tree_apply (tr1,tr2) =
+ let
+ (* prop_tree * prop_tree -> prop_tree *)
+ fun prop_tree_disjunction (tr1,tr2) =
+ tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
+ (* prop_formula * prop_tree -> prop_tree *)
+ fun prop_formula_times_prop_tree (fm,tr) =
+ tree_map (map (fn x => SAnd (fm,x))) tr
+ (* prop_formula list * prop_tree list -> prop_tree *)
+ fun prop_formula_list_dot_product_prop_tree_list ([fm],[tr]) =
+ prop_formula_times_prop_tree (fm,tr)
+ | prop_formula_list_dot_product_prop_tree_list (fm::fms,tr::trees) =
+ prop_tree_disjunction (prop_formula_times_prop_tree (fm,tr), prop_formula_list_dot_product_prop_tree_list (fms,trees))
+ | prop_formula_list_dot_product_prop_tree_list (_,_) =
+ raise REFUTE ("prop_tree_apply::prop_formula_list_dot_product_prop_tree_list", "empty list")
+ (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
+ (* 'a -> 'a list list -> 'a list list *)
+ fun cons_list x xss =
+ map (fn xs => x::xs) xss
+ (* returns a list of lists, each one consisting of one element from each element of 'xss' *)
+ (* 'a list list -> 'a list list *)
+ fun pick_all [xs] =
+ map (fn x => [x]) xs
+ | pick_all (xs::xss) =
+ let val rec_pick = pick_all xss in
+ foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
+ end
+ | pick_all _ =
+ raise REFUTE ("prop_tree_apply::pick_all", "empty list")
+ (* prop_tree -> prop_formula list *)
+ fun prop_tree_to_prop_formula_list (Leaf xs) =
+ xs
+ | prop_tree_to_prop_formula_list (Node trees) =
+ map list_conjunction (pick_all (map prop_tree_to_prop_formula_list trees))
+ in
+ case tr1 of
+ Leaf _ =>
+ raise REFUTE ("prop_tree_apply", "first tree is a leaf")
+ | Node xs =>
+ prop_formula_list_dot_product_prop_tree_list (prop_tree_to_prop_formula_list tr2, xs)
+ end
+
+(* ------------------------------------------------------------------------- *)
+(* term_to_prop_tree: translates a HOL term 't' into a tree of propositional *)
+(* formulas; 'us' specifies the number of elements for each type *)
+(* variable in 't'; 'cdepth' specifies the maximal constructor depth *)
+(* for inductive datatypes. Also returns the lowest index that was not *)
+(* used for a boolean variable, and a substitution of terms (free/ *)
+(* schematic variables) by prop_trees. *)
+(* ------------------------------------------------------------------------- *)
+
+ (* Term.term -> (Term.typ * int) list -> theory -> int -> prop_tree * (int * (Term.term * prop_tree) list) *)
+
+ fun term_to_prop_tree t us thy cdepth =
+ let
+ (* Term.term -> int * (Term.term * prop_tree) list -> prop_tree * (int * (Term.term * prop_tree) list) *)
+ fun variable_to_prop_tree_subst t' (idx,subs) =
+ case assoc (subs,t') of
+ Some tr =>
+ (* return the previously associated tree; the substitution remains unchanged *)
+ (tr, (idx,subs))
+ | None =>
+ (* generate a new tree; update the index; extend the substitution *)
+ let
+ val T = case t' of
+ Free (_,T) => T
+ | Var (_,T) => T
+ | _ => raise REFUTE ("variable_to_prop_tree_subst", "term is not a (free or schematic) variable")
+ val (tr,newidx) = type_to_prop_tree T us thy cdepth idx
+ in
+ (tr, (newidx, (t',tr)::subs))
+ end
+ (* Term.term -> int * (Term.term * prop_tree) list -> prop_tree list -> prop_tree * (int * (Term.term * prop_tree) list) *)
+ fun term_to_prop_tree_subst t' (idx,subs) bsubs =
+ case t' of
+ (* meta-logical constants *)
+ Const ("Goal", _) $ t1 =>
+ term_to_prop_tree_subst t1 (idx,subs) bsubs
+ | Const ("all", _) $ t1 =>
+ let
+ val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
+ in
+ case tree1 of
+ Node xs =>
+ let
+ val fmTrue = list_conjunction (map prop_tree_to_true xs)
+ val fmFalse = list_disjunction (map prop_tree_to_false xs)
+ in
+ (Leaf [fmTrue, fmFalse], (i1,s1))
+ end
+ | _ =>
+ raise REFUTE ("term_to_prop_tree_subst", "'all' is not followed by a function")
+ end
+ | Const ("==", _) $ t1 $ t2 =>
+ let
+ val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
+ val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
+ val fmTrue = prop_tree_equal (tree1,tree2)
+ val fmFalse = SNot fmTrue
+ in
+ (Leaf [fmTrue, fmFalse], (i2,s2))
+ end
+ | Const ("==>", _) $ t1 $ t2 =>
+ let
+ val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
+ val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
+ val fmTrue = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
+ val fmFalse = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
+ in
+ (Leaf [fmTrue, fmFalse], (i2,s2))
+ end
+ (* HOL constants *)
+ | Const ("Trueprop", _) $ t1 =>
+ term_to_prop_tree_subst t1 (idx,subs) bsubs
+ | Const ("Not", _) $ t1 =>
+ let
+ val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
+ val fmTrue = prop_tree_to_false tree1
+ val fmFalse = prop_tree_to_true tree1
+ in
+ (Leaf [fmTrue, fmFalse], (i1,s1))
+ end
+ | Const ("True", _) =>
+ (Leaf [True, False], (idx,subs))
+ | Const ("False", _) =>
+ (Leaf [False, True], (idx,subs))
+ | Const ("All", _) $ t1 =>
+ let
+ val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
+ in
+ case tree1 of
+ Node xs =>
+ let
+ val fmTrue = list_conjunction (map prop_tree_to_true xs)
+ val fmFalse = list_disjunction (map prop_tree_to_false xs)
+ in
+ (Leaf [fmTrue, fmFalse], (i1,s1))
+ end
+ | _ =>
+ raise REFUTE ("term_to_prop_tree_subst", "'All' is not followed by a function")
+ end
+ | Const ("Ex", _) $ t1 =>
+ let
+ val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
+ in
+ case tree1 of
+ Node xs =>
+ let
+ val fmTrue = list_disjunction (map prop_tree_to_true xs)
+ val fmFalse = list_conjunction (map prop_tree_to_false xs)
+ in
+ (Leaf [fmTrue, fmFalse], (i1,s1))
+ end
+ | _ =>
+ raise REFUTE ("term_to_prop_tree_subst", "'Ex' is not followed by a function")
+ end
+ | Const ("Ex1", Type ("fun", [Type ("fun", [T, Type ("bool",[])]), Type ("bool",[])])) $ t1 =>
+ (* 'Ex1 t1' is equivalent to 'Ex Abs(x,T,t1' x & All Abs(y,T,t1'' y --> x=y))' *)
+ let
+ val t1' = Term.incr_bv (1, 0, t1)
+ val t1'' = Term.incr_bv (2, 0, t1)
+ val t_equal = (HOLogic.eq_const T) $ (Bound 1) $ (Bound 0)
+ val t_unique = (HOLogic.all_const T) $ Abs("y",T,HOLogic.mk_imp (t1'' $ (Bound 0),t_equal))
+ val t_ex1 = (HOLogic.exists_const T) $ Abs("x",T,HOLogic.mk_conj (t1' $ (Bound 0),t_unique))
+ in
+ term_to_prop_tree_subst t_ex1 (idx,subs) bsubs
+ end
+ | Const ("op =", _) $ t1 $ t2 =>
+ let
+ val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
+ val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
+ val fmTrue = prop_tree_equal (tree1,tree2)
+ val fmFalse = SNot fmTrue
+ in
+ (Leaf [fmTrue, fmFalse], (i2,s2))
+ end
+ | Const ("op &", _) $ t1 $ t2 =>
+ let
+ val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
+ val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
+ val fmTrue = SAnd (prop_tree_to_true tree1, prop_tree_to_true tree2)
+ val fmFalse = SOr (prop_tree_to_false tree1, prop_tree_to_false tree2)
+ in
+ (Leaf [fmTrue, fmFalse], (i2,s2))
+ end
+ | Const ("op |", _) $ t1 $ t2 =>
+ let
+ val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
+ val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
+ val fmTrue = SOr (prop_tree_to_true tree1, prop_tree_to_true tree2)
+ val fmFalse = SAnd (prop_tree_to_false tree1, prop_tree_to_false tree2)
+ in
+ (Leaf [fmTrue, fmFalse], (i2,s2))
+ end
+ | Const ("op -->", _) $ t1 $ t2 =>
+ let
+ val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
+ val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
+ val fmTrue = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
+ val fmFalse = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
+ in
+ (Leaf [fmTrue, fmFalse], (i2,s2))
+ end
+ (* set constants *)
+ | Const ("Collect", _) $ t1 =>
+ term_to_prop_tree_subst t1 (idx,subs) bsubs
+ | Const ("op :", _) $ t1 $ t2 =>
+ term_to_prop_tree_subst (t2 $ t1) (idx,subs) bsubs
+ (* datatype constants *)
+ | Const ("Product_Type.Unity", _) =>
+ (Leaf [True], (idx,subs))
+ (* unknown constants *)
+ | Const (c, _) =>
+ error ("term contains an unknown constant: '" ^ c ^ "'")
+ (* abstractions *)
+ | Abs (_,T,body) =>
+ let
+ val constants = type_to_constants T us thy cdepth
+ val (trees, substs) = split_list (map (fn c => term_to_prop_tree_subst body (idx,subs) (c::bsubs)) constants)
+ in
+ (* the substitutions in 'substs' are all identical *)
+ (Node trees, hd substs)
+ end
+ (* (free/schematic) variables *)
+ | Free _ =>
+ variable_to_prop_tree_subst t' (idx,subs)
+ | Var _ =>
+ variable_to_prop_tree_subst t' (idx,subs)
+ (* bound variables *)
+ | Bound i =>
+ if (length bsubs) <= i then
+ raise REFUTE ("term_to_prop_tree_subst", "term contains a loose bound variable (with index " ^ (string_of_int i) ^ ")")
+ else
+ (nth_elem (i,bsubs), (idx,subs))
+ (* application *)
+ | t1 $ t2 =>
+ let
+ val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
+ val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
+ in
+ (prop_tree_apply (tree1,tree2), (i2,s2))
+ end
+ in
+ term_to_prop_tree_subst t (1,[]) []
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* term_to_prop_formula: translates a HOL formula 't' into a propositional *)
+(* formula that is satisfiable if and only if 't' has a model of "size" *)
+(* 'us' (where 'us' specifies the number of elements for each free type *)
+(* variable in 't') and maximal constructor depth 'cdepth'. *)
+(* ------------------------------------------------------------------------- *)
+
+ (* TODO: shouldn't 'us' also specify the number of elements for schematic type variables? (if so, modify the comment above) *)
+
+ (* Term.term -> (Term.typ * int) list -> theory -> int -> prop_formula * (int * (Term.term * prop_tree) list) *)
+
+ fun term_to_prop_formula t us thy cdepth =
+ let
+ val (tr, (idx,subs)) = term_to_prop_tree t us thy cdepth
+ val fm = prop_tree_to_true tr
+ in
+ if subs=[] then
+ (fm, (idx,subs))
+ else
+ (* make sure every tree that is substituted for a term describes a single element *)
+ (SAnd (list_conjunction (map (fn (_,tr) => restrict_to_single_element tr) subs), fm), (idx,subs))
+ end;
+
+
+(* ------------------------------------------------------------------------- *)
+(* INTERFACE, PART 2: FINDING A MODEL *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* string_of_universe: prints a universe, i.e. an assignment of sizes for *)
+(* types *)
+(* thy: the current theory *)
+(* us : a list containing types together with their size *)
+(* ------------------------------------------------------------------------- *)
+
+ (* theory -> (Term.typ * int) list -> string *)
+
+ fun string_of_universe thy [] =
+ "empty universe (no type variables in term)"
+ | string_of_universe thy us =
+ space_implode ", " (map (fn (T,i) => (Sign.string_of_typ (sign_of thy) T) ^ ": " ^ (string_of_int i)) us);
+
+(* ------------------------------------------------------------------------- *)
+(* string_of_model: prints a model, given by a substitution 'subs' of trees *)
+(* of propositional variables and an assignment 'ass' of truth values *)
+(* for these variables. *)
+(* thy : the current theory *)
+(* us : universe, specifies the "size" of each type (i.e. type variable) *)
+(* cdepth: maximal constructor depth for inductive datatypes *)
+(* subs : substitution of trees of propositional formulas (for variables) *)
+(* ass : assignment of truth values for boolean variables; see function *)
+(* 'truth_value' below for its meaning *)
+(* ------------------------------------------------------------------------- *)
+
+ (* theory -> (Term.typ * int) list -> int -> (Term.term * prop_formula tree) list -> int list -> string *)
+
+ fun string_of_model thy us cdepth [] ass =
+ "empty interpretation (no free variables in term)"
+ | string_of_model thy us cdepth subs ass =
+ let
+ (* Sign.sg *)
+ val sg = sign_of thy
+ (* int -> bool *)
+ fun truth_value i =
+ if i mem ass then true
+ else if ~i mem ass then false
+ else error ("SAT solver assignment does not specify a value for variable " ^ (string_of_int i))
+ (* string -> string *)
+ fun strip_leading_quote str =
+ if nth_elem_string(0,str)="'" then
+ String.substring (str, 1, size str - 1)
+ else
+ str;
+ (* prop_formula list -> int *)
+ fun true_index xs =
+ (* returns the (0-based) index of the first true formula in xs *)
+ let fun true_index_acc [] _ =
+ raise REFUTE ("string_of_model::true_index", "no variable was set to true")
+ | true_index_acc (x::xs) n =
+ case x of
+ BoolVar i =>
+ if truth_value i then n else true_index_acc xs (n+1)
+ | True =>
+ n
+ | False =>
+ true_index_acc xs (n+1)
+ | _ =>
+ raise REFUTE ("string_of_model::true_index", "formula is not a boolean variable/true/false")
+ in
+ true_index_acc xs 0
+ end
+ (* Term.typ -> int -> prop_tree -> string *)
+ (* prop *)
+ fun string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
+ if truth_value i then "true" else "false"
+ | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [True, False]) =
+ "true"
+ | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [False, True]) =
+ "false"
+ (* bool *)
+ | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
+ if truth_value i then "true" else "false"
+ | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [True, False]) =
+ "true"
+ | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [False, True]) =
+ "false"
+ (* unit *)
+ | string_of_prop_tree (Type ("Product_Type.unit",[])) cdepth (Leaf [True]) =
+ "()"
+ | string_of_prop_tree (Type (s,Ts)) cdepth (Leaf xs) =
+ (case DatatypePackage.datatype_info thy s of
+ Some info => (* inductive datatype *)
+ let
+ val index = #index info
+ val descr = #descr info
+ val (_, dtyps, constrs) = the (assoc (descr, index))
+ val Typs = dtyps ~~ Ts
+ (* string -> string *)
+ fun unqualify s =
+ implode (snd (take_suffix (fn c => c <> ".") (explode s)))
+ (* DatatypeAux.dtyp -> Term.typ *)
+ fun typ_of_dtyp (DatatypeAux.DtTFree a) =
+ the (assoc (Typs, DatatypeAux.DtTFree a))
+ | typ_of_dtyp (DatatypeAux.DtRec i) =
+ let
+ val (s, ds, _) = the (assoc (descr, i))
+ in
+ Type (s, map typ_of_dtyp ds)
+ end
+ | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
+ Type (s, map typ_of_dtyp ds)
+ (* DatatypeAux.dtyp list -> int -> string *)
+ fun string_of_inductive_type_cargs [] n =
+ if n<>0 then
+ raise REFUTE ("string_of_model", "internal error computing the element index for an inductive type")
+ else
+ ""
+ | string_of_inductive_type_cargs (d::ds) n =
+ let
+ val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
+ in
+ " " ^ (string_of_prop_tree (typ_of_dtyp d) (cdepth-1) (nth_elem (n div size_ds, type_to_constants (typ_of_dtyp d) us thy (cdepth-1)))) ^ (string_of_inductive_type_cargs ds (n mod size_ds))
+ end
+ (* (string * DatatypeAux.dtyp list) list -> int -> string *)
+ fun string_of_inductive_type_constrs [] n =
+ raise REFUTE ("string_of_model", "inductive type has fewer elements than needed")
+ | string_of_inductive_type_constrs ((s,ds)::cs) n =
+ let
+ val size = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
+ in
+ if n < size then
+ (unqualify s) ^ (string_of_inductive_type_cargs ds n)
+ else
+ string_of_inductive_type_constrs cs (n - size)
+ end
+ in
+ string_of_inductive_type_constrs constrs (true_index xs)
+ end
+ | None =>
+ raise REFUTE ("string_of_model", "type contains an unknown type constructor: '" ^ s ^ "'"))
+ (* type variable *)
+ | string_of_prop_tree (TFree (s,_)) cdepth (Leaf xs) =
+ (strip_leading_quote s) ^ (string_of_int (true_index xs))
+ | string_of_prop_tree (TVar ((s,_),_)) cdepth (Leaf xs) =
+ (strip_leading_quote s) ^ (string_of_int (true_index xs))
+ (* function or set type *)
+ | string_of_prop_tree T cdepth (Node xs) =
+ case T of
+ Type ("fun", [T1,T2]) =>
+ let
+ val strings = foldl (fn (ss,(c,x)) => ss @ [(string_of_prop_tree T1 cdepth c) ^ "\\<mapsto>" ^ (string_of_prop_tree T2 cdepth x)]) ([], (type_to_constants T1 us thy cdepth) ~~ xs)
+ in
+ "(" ^ (space_implode ", " strings) ^ ")"
+ end
+ | Type ("set", [T1]) =>
+ let
+ val strings = foldl (fn (ss,(c,x)) => if (string_of_prop_tree (Type ("bool",[])) cdepth x)="true" then ss @ [string_of_prop_tree T1 cdepth c] else ss) ([], (type_to_constants T1 us thy cdepth) ~~ xs)
+ in
+ "{" ^ (space_implode ", " strings) ^ "}"
+ end
+ | _ => raise REFUTE ("string_of_model::string_of_prop_tree", "not a function/set type")
+ (* Term.term * prop_formula tree -> string *)
+ fun string_of_term_assignment (t,tr) =
+ let
+ val T = case t of
+ Free (_,T) => T
+ | Var (_,T) => T
+ | _ => raise REFUTE ("string_of_model::string_of_term_assignment", "term is not a (free or schematic) variable")
+ in
+ (Sign.string_of_term sg t) ^ " = " ^ (string_of_prop_tree T cdepth tr)
+ end
+ in
+ space_implode "\n" (map string_of_term_assignment subs)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* find_model: repeatedly calls 'prop_formula_sat_solver' with appropriate *)
+(* parameters, and displays the results to the user *)
+(* params : list of '(name, value)' pairs used to override default *)
+(* parameters *)
+(* *)
+(* This is a brief description of the algorithm implemented: *)
+(* *)
+(* 1. Let k = max ('minsize',1). *)
+(* 2. Let the universe have k elements. Find all possible partitions of *)
+(* these elements into the basic types occuring in 't' such that no basic *)
+(* type is empty. *)
+(* 3. Translate 't' into a propositional formula p s.t. 't' has a model wrt. *)
+(* the partition chosen in step (2.) if (actually, if and only if) p is *)
+(* satisfiable. To do this, replace quantification by conjunction/ *)
+(* disjunction over all elements of the type being quantified over. (If *)
+(* p contains more than 'maxvars' boolean variables, terminate.) *)
+(* 4. Serialize p to a file, and try to find a satisfying assignment for p *)
+(* by invoking an external SAT solver. *)
+(* 5. If the SAT solver finds a satisfying assignment for p, translate this *)
+(* assignment back into a model for 't'. Present this model to the user, *)
+(* then terminate. *)
+(* 6. As long as there is another partition left, pick it and go back to *)
+(* step (3.). *)
+(* 7. Increase k by 1. As long as k does not exceed 'maxsize', go back to *)
+(* step (2.). *)
+(* *)
+(* The following parameters are currently supported (and required!): *)
+(* *)
+(* Name Type Description *)
+(* *)
+(* "minsize" int Only search for models with size at least *)
+(* 'minsize'. *)
+(* "maxsize" int If >0, only search for models with size at most *)
+(* 'maxsize'. *)
+(* "maxvars" int If >0, use at most 'maxvars' boolean variables *)
+(* when transforming the term into a propositional *)
+(* formula. *)
+(* "satfile" string Name of the file used to store the propositional *)
+(* formula, i.e. the input to the SAT solver. *)
+(* "satformat" string Format of the SAT solver's input file. Must be *)
+(* either "cnf", "defcnf", or "sat". Since "sat" is *)
+(* not supported by most SAT solvers, and "cnf" can *)
+(* cause exponential blowup of the formula, "defcnf" *)
+(* is recommended. *)
+(* "resultfile" string Name of the file containing the SAT solver's *)
+(* output. *)
+(* "success" string Part of the line in the SAT solver's output that *)
+(* precedes a list of integers representing the *)
+(* satisfying assignment. *)
+(* "command" string System command used to execute the SAT solver. *)
+(* Note that you if you change 'satfile' or *)
+(* 'resultfile', you will also need to change *)
+(* 'command'. *)
+(* *)
+(* See the Isabelle/Isar theory 'Refute.thy' for reasonable default values. *)
+(* ------------------------------------------------------------------------- *)
+
+ (* theory -> (string * string) list -> Term.term -> unit *)
+
+ fun find_model thy params t =
+ let
+ (* (string * string) list * (string * string) list -> (string * string) list *)
+ fun add_params (parms, []) =
+ parms
+ | add_params (parms, defparm::defparms) =
+ add_params (gen_ins (fn (a, b) => (fst a) = (fst b)) (defparm, parms), defparms)
+ (* (string * string) list * string -> int *)
+ fun read_int (parms, name) =
+ case assoc_string (parms, name) of
+ Some s => (case LargeInt.fromString s of
+ SOME i => i
+ | NONE => error ("parameter '" ^ name ^ "' (value is '" ^ s ^ "') must be an integer value"))
+ | None => error ("parameter '" ^ name ^ "' must be assigned a value")
+ (* (string * string) list * string -> string *)
+ fun read_string (parms, name) =
+ case assoc_string (parms, name) of
+ Some s => s
+ | None => error ("parameter '" ^ name ^ "' must be assigned a value")
+ (* (string * string) list *)
+ val allparams = add_params (params, get_default_params thy)
+ (* int *)
+ val minsize = read_int (allparams, "minsize")
+ val maxsize = read_int (allparams, "maxsize")
+ val maxvars = read_int (allparams, "maxvars")
+ (* string *)
+ val satfile = read_string (allparams, "satfile")
+ val satformat = read_string (allparams, "satformat")
+ val resultfile = read_string (allparams, "resultfile")
+ val success = read_string (allparams, "success")
+ val command = read_string (allparams, "command")
+ (* misc *)
+ val satpath = Path.unpack satfile
+ val resultpath = Path.unpack resultfile
+ val sg = sign_of thy
+ (* Term.typ list *)
+ val tvars = map (fn (i,s) => TVar(i,s)) (term_tvars t)
+ val tfrees = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
+ (* universe -> int -> bool *)
+ fun find_model_universe u cdepth =
+ let
+ (* given the universe 'u' and constructor depth 'cdepth', translate *)
+ (* the term 't' into a propositional formula 'fm' *)
+ val (fm,(idx,subs)) = term_to_prop_formula t u thy cdepth
+ val usedvars = idx-1
+ in
+ (* 'maxvars=0' means "use as many variables as necessary" *)
+ if usedvars>maxvars andalso maxvars<>0 then
+ (
+ (* too many variables used: terminate *)
+ writeln ("\nSearch terminated: " ^ (string_of_int usedvars) ^ " boolean variables used (only " ^ (string_of_int maxvars) ^ " allowed).");
+ true
+ )
+ else
+ (* pass the formula 'fm' to an external SAT solver *)
+ case prop_formula_sat_solver fm satpath satformat resultpath success command of
+ None =>
+ (* no model found *)
+ false
+ | Some assignment =>
+ (* model found: terminate *)
+ (
+ writeln ("\nModel found:\n" ^ (string_of_universe thy u) ^ "\n" ^ (string_of_model thy u cdepth subs assignment));
+ true
+ )
+ end
+ (* universe list -> int -> bool *)
+ fun find_model_universes [] cdepth =
+ (
+ std_output "\n";
+ false
+ )
+ | find_model_universes (u::us) cdepth =
+ (
+ std_output ".";
+ ((if find_model_universe u cdepth then
+ (* terminate *)
+ true
+ else
+ (* continue search with the next universe *)
+ find_model_universes us cdepth)
+ handle EMPTY_DATATYPE => (std_output "[empty inductive type (constructor depth too small)]\n"; false))
+ )
+ (* int * int -> unit *)
+ fun find_model_from_to (min,max) =
+ (* 'max=0' means "search for arbitrary large models" *)
+ if min>max andalso max<>0 then
+ writeln ("Search terminated: no model found.")
+ else
+ (
+ std_output ("Searching for a model of size " ^ (string_of_int min));
+ if find_model_universes (make_universes tfrees min) min then
+ (* terminate *)
+ ()
+ else
+ (* continue search with increased size *)
+ find_model_from_to (min+1, max)
+ )
+ in
+ writeln ("Trying to find a model of: " ^ (Sign.string_of_term sg t));
+ if tvars<>[] then
+ (* TODO: deal with schematic type variables in a better way, if possible *)
+ error "term contains schematic type variables"
+ else
+ (
+ if minsize<1 then
+ writeln ("'minsize' is less than 1; starting search with size 1.")
+ else
+ ();
+ if maxsize<max (minsize,1) andalso maxsize<>0 then
+ writeln ("'maxsize' is less than 'minsize': no model found.")
+ else
+ find_model_from_to (max (minsize,1), maxsize)
+ )
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* refute_term: calls 'find_model' on the negation of a term *)
+(* params : list of '(name, value)' pairs used to override default *)
+(* parameters *)
+(* ------------------------------------------------------------------------- *)
+
+ (* theory -> (string * string) list -> Term.term -> unit *)
+
+ fun refute_term thy params t =
+ let
+ (* TODO: schematic type variables? *)
+ val negation = close_vars (HOLogic.Not $ t)
+ (* If 't' is of type 'propT' (rather than 'boolT'), applying *)
+ (* 'HOLogic.Not' is not type-correct. However, this isn't *)
+ (* really a problem as long as 'find_model' still interprets *)
+ (* the resulting term correctly, without checking its type. *)
+ in
+ find_model thy params negation
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* refute_subgoal: calls 'refute_term' on a specific subgoal *)
+(* params : list of '(name, value)' pairs used to override default *)
+(* parameters *)
+(* subgoal : 0-based index specifying the subgoal number *)
+(* ------------------------------------------------------------------------- *)
+
+ (* theory -> (string * string) list -> Thm.thm -> int -> unit *)
+
+ fun refute_subgoal thy params thm subgoal =
+ refute_term thy params (nth_elem (subgoal, prems_of thm));
+
+end