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