# HG changeset patch # User webertj # Date 1078954428 -3600 # Node ID cca28ec5f9a60ce8be6337633894e3e068121b3e # Parent 5c4a1e96efd6c8015c7a5fa93c82193a38277e08 support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps diff -r 5c4a1e96efd6 -r cca28ec5f9a6 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Wed Mar 10 20:36:11 2004 +0100 +++ b/src/HOL/Tools/refute.ML Wed Mar 10 22:33:48 2004 +0100 @@ -3,526 +3,77 @@ Author: Tjark Weber Copyright 2003-2004 -Finite model generation for HOL formulae, using an external SAT solver. +Finite model generation for HOL formulae, using a 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. *) +(* TODO: Change parameter handling so that only supported parameters can be *) +(* set, and specify defaults here, rather than in HOL/Main.thy. *) +(* ------------------------------------------------------------------------- *) + +(* ------------------------------------------------------------------------- *) +(* Declares the 'REFUTE' signature as well as a structure 'Refute'. *) +(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'. *) (* ------------------------------------------------------------------------- *) signature REFUTE = sig + exception REFUTE of string * string + +(* ------------------------------------------------------------------------- *) +(* Model/interpretation related code (translation HOL -> boolean formula) *) +(* ------------------------------------------------------------------------- *) + + exception CANNOT_INTERPRET + + type interpretation + type model + type arguments + + val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory + val add_printer : string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory + + val interpret : theory -> model -> arguments -> Term.term -> interpretation * model * arguments (* exception CANNOT_INTERPRET *) + val is_satisfying_model : model -> interpretation -> bool -> PropLogic.prop_formula + + val print : theory -> model -> Term.term -> interpretation -> (int -> bool) -> string + val print_model : theory -> model -> (int -> bool) -> string + +(* ------------------------------------------------------------------------- *) +(* Interface *) +(* ------------------------------------------------------------------------- *) + + 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 actual_params : theory -> (string * string) list -> (int * int * int * string) + + val find_model : theory -> (int * int * int * string) -> Term.term -> bool -> unit + + val satisfy_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model for a formula *) + val refute_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model that refutes a formula *) + val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit + + val setup : (theory -> theory) list +end; + +structure Refute : REFUTE = +struct + + open PropLogic; + (* 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); + exception REFUTE of string * string; (* ("in function", "cause") *) (* ------------------------------------------------------------------------- *) -(* 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). *) +(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) (* ------------------------------------------------------------------------- *) - (* 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 - ) - ); - + exception CANNOT_INTERPRET; (* ------------------------------------------------------------------------- *) (* TREES *) @@ -537,9 +88,6 @@ 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 = @@ -571,45 +119,95 @@ 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 *) +(* interpretation: a term's interpretation is given by a variable of type *) +(* 'interpretation' *) (* ------------------------------------------------------------------------- *) - (* 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"); + type interpretation = + prop_formula list tree; (* ------------------------------------------------------------------------- *) -(* prop_tree_to_false: returns a propositional formula that is true iff the *) -(* tree denotes the boolean value FALSE *) +(* model: a model specifies the size of types and the interpretation of *) +(* terms *) (* ------------------------------------------------------------------------- *) - (* prop_tree -> prop_formula *) + type model = + (Term.typ * int) list * (Term.term * interpretation) list; - (* 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 *) +(* ------------------------------------------------------------------------- *) +(* arguments: additional arguments required during interpretation of terms *) +(* ------------------------------------------------------------------------- *) + + type arguments = + {next_idx: int, bounds: interpretation list, wellformed: prop_formula}; + - 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"); + structure RefuteDataArgs = + struct + val name = "HOL/refute"; + type T = + {interpreters: (string * (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option)) list, + printers: (string * (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option)) list, + parameters: string Symtab.table}; + val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; + val copy = I; + val prep_ext = I; + fun merge + ({interpreters = in1, printers = pr1, parameters = pa1}, + {interpreters = in2, printers = pr2, parameters = pa2}) = + {interpreters = rev (merge_alists (rev in1) (rev in2)), + printers = rev (merge_alists (rev pr1) (rev pr2)), + parameters = Symtab.merge (op=) (pa1, pa2)}; + fun print sg {interpreters, printers, parameters} = + Pretty.writeln (Pretty.chunks + [Pretty.strs ("default parameters:" :: flat (map (fn (name,value) => [name, "=", value]) (Symtab.dest parameters))), + Pretty.strs ("interpreters:" :: map fst interpreters), + Pretty.strs ("printers:" :: map fst printers)]); + end; + + structure RefuteData = TheoryDataFun(RefuteDataArgs); + (* ------------------------------------------------------------------------- *) -(* 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 *) +(* interpret: tries to interpret the term 't' using a suitable interpreter; *) +(* returns the interpretation and a (possibly extended) model *) +(* that keeps track of the interpretation of subterms *) +(* Note: exception 'CANNOT_INTERPRETE' is raised if the term cannot be *) +(* interpreted by any interpreter *) (* ------------------------------------------------------------------------- *) - (* prop_tree -> prop_formula *) + (* theory -> model -> arguments -> Term.term -> interpretation * model * arguments *) + + fun interpret thy model args t = + (case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of + None => + (std_output "\n"; warning ("Unable to interpret term:\n" ^ Sign.string_of_term (sign_of thy) t); + raise CANNOT_INTERPRET) + | Some x => x); + +(* ------------------------------------------------------------------------- *) +(* print: tries to print the constant denoted by the term 't' using a *) +(* suitable printer *) +(* ------------------------------------------------------------------------- *) - fun restrict_to_single_element tr = + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string *) + + fun print thy model t intr assignment = + (case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) of + None => "<>" + | Some s => s); + +(* ------------------------------------------------------------------------- *) +(* is_satisfying_model: returns a propositional formula that is true iff the *) +(* given interpretation denotes 'satisfy', and the model meets certain *) +(* well-formedness properties *) +(* ------------------------------------------------------------------------- *) + + (* model -> interpretation -> bool -> PropLogic.prop_formula *) + + fun is_satisfying_model model intr satisfy = let (* prop_formula list -> prop_formula *) fun allfalse [] = True @@ -617,290 +215,1347 @@ (* prop_formula list -> prop_formula *) fun exactly1true [] = False | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs)) + (* ------------------------------------------------------------------------- *) + (* restrict_to_single_element: returns a propositional formula that is true *) + (* iff the interpretation denotes a single element of its corresponding *) + (* type, i.e. iff at each leaf, one and only one formula is true *) + (* ------------------------------------------------------------------------- *) + (* interpretation -> prop_formula *) + fun restrict_to_single_element (Leaf [BoolVar i, Not (BoolVar j)]) = + if (i=j) then + True (* optimization for boolean variables *) + else + raise REFUTE ("is_satisfying_model", "boolean variables in leaf have different indices") + | restrict_to_single_element (Leaf xs) = + exactly1true xs + | restrict_to_single_element (Node trees) = + PropLogic.all (map restrict_to_single_element trees) 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) + (* 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, and false *) + (* iff the leaf's second element is true *) + case intr of + Leaf [fmT,fmF] => + (* well-formedness properties and formula 'fmT'/'fmF' *) + SAnd (PropLogic.all (map (restrict_to_single_element o snd) (snd model)), if satisfy then fmT else fmF) + | _ => + raise REFUTE ("is_satisfying_model", "interpretation does not denote a boolean value") + end; + +(* ------------------------------------------------------------------------- *) +(* print_model: turns the model into a string, using a fixed interpretation *) +(* (given by an assignment for boolean variables) and suitable *) +(* printers *) +(* ------------------------------------------------------------------------- *) + + fun print_model thy model assignment = + let + val (typs, terms) = model + in + (if null typs then + "empty universe (no type variables in term)" + else + "Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs)) + ^ "\n" + ^ (if null terms then + "empty interpretation (no free variables in term)" + else + space_implode "\n" (map + (fn (t,intr) => + Sign.string_of_term (sign_of thy) t ^ ": " ^ print thy model t intr assignment) + terms) + ) + ^ "\n" + end; + + +(* ------------------------------------------------------------------------- *) +(* PARAMETER MANAGEMENT *) +(* ------------------------------------------------------------------------- *) + + (* string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory *) + + fun add_interpreter name f thy = + let + val {interpreters, printers, parameters} = RefuteData.get thy + in + case assoc (interpreters, name) of + None => RefuteData.put {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} thy + | Some _ => error ("Interpreter " ^ name ^ " already declared") + end; + + (* string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory *) + + fun add_printer name f thy = + let + val {interpreters, printers, parameters} = RefuteData.get thy + in + case assoc (printers, name) of + None => RefuteData.put {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} thy + | Some _ => error ("Printer " ^ name ^ " already declared") + end; + +(* ------------------------------------------------------------------------- *) +(* set_default_param: stores the '(name, value)' pair in RefuteData's *) +(* parameter table *) +(* ------------------------------------------------------------------------- *) + + (* (string * string) -> theory -> theory *) + + fun set_default_param (name, value) thy = + let + val {interpreters, printers, parameters} = RefuteData.get thy + in + case Symtab.lookup (parameters, name) of + None => RefuteData.put + {interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy + | Some _ => RefuteData.put + {interpreters = interpreters, printers = printers, parameters = Symtab.update ((name, value), parameters)} thy end; (* ------------------------------------------------------------------------- *) -(* HOL FORMULAS *) +(* get_default_param: retrieves the value associated with 'name' from *) +(* RefuteData's parameter table *) +(* ------------------------------------------------------------------------- *) + + (* theory -> string -> string option *) + + fun get_default_param thy name = Symtab.lookup ((#parameters o RefuteData.get) thy, name); + +(* ------------------------------------------------------------------------- *) +(* get_default_params: returns a list of all '(name, value)' pairs that are *) +(* stored in RefuteData's parameter table *) +(* ------------------------------------------------------------------------- *) + + (* theory -> (string * string) list *) + + fun get_default_params thy = (Symtab.dest o #parameters o RefuteData.get) thy; + +(* ------------------------------------------------------------------------- *) +(* actual_params: takes a (possibly empty) list 'params' of parameters that *) +(* override the default parameters currently specified in 'thy', and *) +(* returns a tuple that can be passed to 'find_model'. *) +(* *) +(* The following parameters are 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. *) +(* "satsolver" string SAT solver to be used. *) +(* ------------------------------------------------------------------------- *) + + (* theory -> (string * string) list -> (int * int * int * string) *) + + fun actual_params thy params = + let + (* (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 " ^ quote name ^ " (value is " ^ quote s ^ ") must be an integer value")) + | None => error ("parameter " ^ quote 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 " ^ quote name ^ " must be assigned a value") + (* (string * string) list *) + val allparams = params @ (get_default_params thy) (* 'params' first, defaults last (to override) *) + (* int *) + val minsize = read_int (allparams, "minsize") + val maxsize = read_int (allparams, "maxsize") + val maxvars = read_int (allparams, "maxvars") + (* string *) + val satsolver = read_string (allparams, "satsolver") + in + (minsize, maxsize, maxvars, satsolver) + end; + +(* ------------------------------------------------------------------------- *) +(* find_model: repeatedly calls 'invoke_propgen' with appropriate *) +(* parameters, applies the SAT solver, and (in case a model is *) +(* found) displays the model to the user *) +(* thy : the current theory *) +(* minsize : the minimal size of the model *) +(* maxsize : the maximal size of the model *) +(* maxvars : the maximal number of boolean variables to be used *) +(* satsolver: the name of the SAT solver to be used *) +(* satisfy : if 'True', search for a model that makes 't' true; otherwise *) +(* search for a model that makes 't' false *) +(* ------------------------------------------------------------------------- *) + + (* theory -> (int * int * int * string) -> Term.term -> bool -> unit *) + + fun find_model thy (minsize, maxsize, maxvars, satsolver) t satisfy = + let + (* 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) + (* int -> unit *) + fun find_model_loop size = + (* 'maxsize=0' means "search for arbitrary large models" *) + if size>maxsize andalso maxsize<>0 then + writeln ("Search terminated: maxsize=" ^ string_of_int maxsize ^ " exceeded.") + else + let + (* ------------------------------------------------------------------------- *) + (* 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 ("find_model", "empty list (in make_partitions_loop)") + 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 ("find_model", "empty list (in make_partitions)") + val len = length xs + in + if size map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len)) + end + (* ('a * int) list -> bool *) + fun find_interpretation xs = + let + val init_model = (xs, []) + val init_args = {next_idx = 1, bounds = [], wellformed = True} + val (intr, model, args) = interpret thy init_model init_args t + val fm = SAnd (#wellformed args, is_satisfying_model model intr satisfy) + val usedvars = maxidx fm + in + (* 'maxvars=0' means "use as many variables as necessary" *) + if usedvars>maxvars andalso maxvars<>0 then + (writeln ("\nSearch terminated: " ^ string_of_int usedvars ^ " boolean variables used (only " ^ string_of_int maxvars ^ " allowed)."); + true) + else + ( + std_output " invoking SAT solver..."; + case SatSolver.invoke_solver satsolver fm of + None => + (std_output " no model found.\n"; + false) + | Some assignment => + (writeln ("\nModel found:\n" ^ print_model thy model assignment); + true) + ) + end handle CANNOT_INTERPRET => true + (* TODO: change this to false once the ability to interpret terms depends on the universe *) + in + case make_universes (tvars@tfrees) size of + [] => + (writeln ("Searching for a model of size " ^ string_of_int size ^ ": cannot make every type non-empty (model is too small)."); + find_model_loop (size+1)) + | [[]] => + (std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term..."); + if find_interpretation [] then + () + else + writeln ("Search terminated: no type variables in term.")) + | us => + let + fun loop [] = + find_model_loop (size+1) + | loop (u::us) = + (std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term..."); + if find_interpretation u then () else loop us) + in + loop us + end + end + in + writeln ("Trying to find a model that " + ^ (if satisfy then "satisfies" else "refutes") + ^ ": " ^ (Sign.string_of_term (sign_of thy) t)); + if minsize<1 then + writeln "\"minsize\" is less than 1; starting search with size 1." + else (); + find_model_loop (Int.max (minsize,1)) + end; + + +(* ------------------------------------------------------------------------- *) +(* INTERFACE, PART 2: FINDING A MODEL *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) -(* 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 *) +(* satisfy_term: calls 'find_model' to find a model that satisfies 't' *) +(* params : list of '(name, value)' pairs used to override default *) +(* parameters *) (* ------------------------------------------------------------------------- *) - (* (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))); + (* theory -> (string * string) list -> Term.term -> unit *) -(* ------------------------------------------------------------------------- *) -(* 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); + fun satisfy_term thy params t = + find_model thy (actual_params thy params) t true; (* ------------------------------------------------------------------------- *) -(* 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'. *) +(* refute_term: calls 'find_model' to find a model that refutes 't' *) +(* params : list of '(name, value)' pairs used to override default *) +(* parameters *) (* ------------------------------------------------------------------------- *) - (* 'a list -> int -> ('a * int) list list *) + (* theory -> (string * string) list -> Term.term -> unit *) - fun make_universes xs size = + fun refute_term thy params t = 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 + (* disallow schematic type variables, since we cannot properly negate terms containing them *) + val _ = assert (null (term_tvars t)) "Term to be refuted contains schematic type variables" + (* existential closure over schematic variables *) + (* (Term.indexname * Term.typ) list *) + val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t)) + (* Term.term *) + val ex_closure = foldl + (fn (t', ((x,i),T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var((x,i),T), t'))) + (t, vars) + (* If 't' is of type 'propT' (rather than 'boolT'), applying *) + (* 'HOLogic.exists_const' 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 - if size map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len)) + find_model thy (actual_params thy params) ex_closure false 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 *) +(* 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 *) (* ------------------------------------------------------------------------- *) - (* int list -> int *) - - fun product xs = foldl op* (1, xs); + (* theory -> (string * string) list -> Thm.thm -> int -> unit *) -(* ------------------------------------------------------------------------- *) -(* power: power(a,b) computes a^b, for a>=0, b>=0 *) -(* ------------------------------------------------------------------------- *) + fun refute_subgoal thy params thm subgoal = + refute_term thy params (nth_elem (subgoal, prems_of thm)); - (* 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 *) +(* INTERPRETERS *) (* ------------------------------------------------------------------------- *) - (* Term.typ -> (Term.typ * int) list -> theory -> int -> int *) + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - fun size_of_type T us thy cdepth = + fun var_typevar_interpreter thy model args t = 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 + fun is_var (Free _) = true + | is_var (Var _) = true + | is_var _ = false + fun typeof (Free (_,T)) = T + | typeof (Var (_,T)) = T + | typeof _ = raise REFUTE ("var_typevar_interpreter", "term is not a variable") + fun is_typevar (TFree _) = true + | is_typevar (TVar _) = true + | is_typevar _ = false + val (sizes, intrs) = model + in + if is_var t andalso is_typevar (typeof t) then + (case assoc (intrs, t) of + Some intr => Some (intr, model, args) + | None => + let + val size = (the o assoc) (sizes, typeof t) (* the model MUST specify a size for type variables *) + val idx = #next_idx args + val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1)))) + val next = (if size=2 then idx+1 else idx+size) + in + (* extend the model, increase 'next_idx' *) + Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args}) + end) + else + None + end; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun var_funtype_interpreter thy model args t = + let + fun is_var (Free _) = true + | is_var (Var _) = true + | is_var _ = false + fun typeof (Free (_,T)) = T + | typeof (Var (_,T)) = T + | typeof _ = raise REFUTE ("var_funtype_interpreter", "term is not a variable") + fun stringof (Free (x,_)) = x + | stringof (Var ((x,_), _)) = x + | stringof _ = raise REFUTE ("var_funtype_interpreter", "term is not a variable") + fun is_funtype (Type ("fun", [_,_])) = true + | is_funtype _ = false + val (sizes, intrs) = model 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 + if is_var t andalso is_funtype (typeof t) then + (case assoc (intrs, t) of + Some intr => Some (intr, model, args) + | None => + let + val T1 = domain_type (typeof t) + val T2 = range_type (typeof t) + (* we create 'size_of_interpretation (interpret (... T1))' different copies *) + (* of the tree for 'T2', which are then combined into a single new tree *) + val (i1, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (stringof t, T1)) + (* 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 + fun size_of_interpretation (Leaf xs) = length xs + | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs) + val size = size_of_interpretation i1 + (* make fresh copies, with different variable indices *) + (* int -> int -> (int * interpretation list *) + fun make_copies idx 0 = + (idx, []) + | make_copies idx n = + let + val (copy, _, args) = interpret thy (sizes, []) {next_idx = idx, bounds = [], wellformed=True} (Free (stringof t, T2)) + val (next, copies) = make_copies (#next_idx args) (n-1) + in + (next, copy :: copies) + end + val (idx, copies) = make_copies (#next_idx args) (size_of_interpretation i1) + (* combine copies into a single tree *) + val intr = Node copies + in + (* extend the model, increase 'next_idx' *) + Some (intr, (sizes, (t, intr)::intrs), {next_idx = idx, bounds = #bounds args, wellformed = #wellformed args}) + end) + else + None + end; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun var_settype_interpreter thy model args t = + let + val (sizes, intrs) = model + in + case t of + Free (x, Type ("set", [T])) => + (case assoc (intrs, t) of + Some intr => Some (intr, model, args) + | None => + let + val (intr, _, args') = interpret thy model args (Free (x, Type ("fun", [T, Type ("bool", [])]))) + in + Some (intr, (sizes, (t, intr)::intrs), args') + end) + | Var ((x,i), Type ("set", [T])) => + (case assoc (intrs, t) of + Some intr => Some (intr, model, args) + | None => + let + val (intr, _, args') = interpret thy model args (Var ((x,i), Type ("fun", [T, Type ("bool", [])]))) + in + Some (intr, (sizes, (t, intr)::intrs), args') + end) + | _ => None + end; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds args), model, args) + | boundvar_interpreter thy model args _ = None; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun abstraction_interpreter thy model args (Abs (x, T, t)) = + let + val (sizes, intrs) = model + (* create all constants of type T *) + val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (x, T)) + (* returns a list with all unit vectors of length n *) + (* int -> interpretation list *) + fun unit_vectors n = + let + (* returns the k-th unit vector of length n *) + (* int * int -> interpretation *) + fun unit_vector (k,n) = + Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) + (* int -> interpretation list -> interpretation 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 + (* interpretation -> interpretation list *) + fun make_constants (Leaf xs) = + unit_vectors (length xs) + | make_constants (Node xs) = + map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) + (* interpret the body 't' separately for each constant *) + val ((model', args'), bodies) = foldl_map + (fn ((m,a), c) => + let + (* add 'c' to 'bounds' *) + val (i',m',a') = interpret thy m {next_idx = #next_idx a, bounds = c::(#bounds a), wellformed = #wellformed a} t + in + (* keep the new model m' and 'next_idx', but use old 'bounds' *) + ((m',{next_idx = #next_idx a', bounds = #bounds a, wellformed = #wellformed a'}), i') + end) + ((model,args), make_constants i) + in + Some (Node bodies, model', args') + end + | abstraction_interpreter thy model args _ = None; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun apply_interpreter thy model args (t1 $ t2) = + let + (* auxiliary functions *) + (* interpretation * interpretation -> interpretation *) + fun interpretation_disjunction (tr1,tr2) = + tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2)) + (* prop_formula * interpretation -> interpretation *) + fun prop_formula_times_interpretation (fm,tr) = + tree_map (map (fn x => SAnd (fm,x))) tr + (* prop_formula list * interpretation list -> interpretation *) + fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) = + prop_formula_times_interpretation (fm,tr) + | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) = + interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees)) + | prop_formula_list_dot_product_interpretation_list (_,_) = + raise REFUTE ("apply_interpreter", "empty list (in dot product)") + (* 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 ("apply_interpreter", "empty list (in pick_all)") + (* interpretation -> prop_formula list *) + fun interpretation_to_prop_formula_list (Leaf xs) = + xs + | interpretation_to_prop_formula_list (Node trees) = + map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees)) + (* interpretation * interpretation -> interpretation *) + fun interpretation_apply (tr1,tr2) = + (case tr1 of + Leaf _ => + raise REFUTE ("apply_interpreter", "first interpretation is a leaf") + | Node xs => + prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list tr2, xs)) + (* interpret 't1' and 't2' *) + val (intr1, model1, args1) = interpret thy model args t1 + val (intr2, model2, args2) = interpret thy model1 args1 t2 + in + Some (interpretation_apply (intr1,intr2), model2, args2) + end + | apply_interpreter thy model args _ = None; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun const_unfold_interpreter thy model args t = + (* ------------------------------------------------------------------------- *) + (* We unfold constants for which a defining equation is given as an axiom. *) + (* A polymorphic axiom's type variables are instantiated. Eta-expansion is *) + (* performed only if necessary; arguments in the axiom that are present as *) + (* actual arguments in 't' are simply substituted. If more actual than *) + (* formal arguments are present, the constant is *not* unfolded, so that *) + (* other interpreters (that may just not have looked into the term far *) + (* enough yet) may be applied first (after 'apply_interpreter' gets rid of *) + (* one argument). *) + (* ------------------------------------------------------------------------- *) + let + val (head, actuals) = strip_comb t + val actuals_count = length actuals + in + case head of + Const (s,T) => + let + (* (string * Term.term) list *) + val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy)) + (* Term.term * Term.term list * Term.term list -> Term.term *) + (* term, formal arguments, actual arguments *) + fun normalize (t, [], []) = t + | normalize (t, [], y::ys) = raise REFUTE ("const_unfold_interpreter", "more actual than formal parameters") + | normalize (t, x::xs, []) = normalize (lambda x t, xs, []) (* eta-expansion *) + | normalize (t, x::xs, y::ys) = normalize (betapply (lambda x t, y), xs, ys) (* substitution *) + (* string -> Term.typ -> (string * Term.term) list -> Term.term option *) + fun get_defn s T [] = + None + | get_defn s T ((_,ax)::axms) = + (let + val (lhs, rhs) = Logic.dest_equals ax (* equations only *) + val (c, formals) = strip_comb lhs + val (s', T') = dest_Const c + in + if (s=s') andalso (actuals_count <= length formals) then + let + val varT' = Type.varifyT T' (* for polymorphic definitions *) + val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (varT', T)) + val varRhs = map_term_types Type.varifyT rhs + val varFormals = map (map_term_types Type.varifyT) formals + val rhs' = normalize (varRhs, varFormals, actuals) + val unvarRhs = map_term_types + (map_type_tvar + (fn (v,_) => + case Vartab.lookup (typeSubs, v) of + None => + raise REFUTE ("const_unfold_interpreter", "schematic type variable " ^ (fst v) ^ "not instantiated (in definition of " ^ quote s ^ ")") + | Some typ => + typ)) + rhs' + in + Some unvarRhs + end + else + get_defn s T axms + end + handle TERM _ => get_defn s T axms + | Type.TYPE_MATCH => get_defn s T axms) + in + case get_defn s T axioms of + Some t' => Some (interpret thy model args t') + | None => None + end + | _ => None + end; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun Pure_interpreter thy model args t = + let + fun toTrue (Leaf [fm,_]) = fm + | toTrue _ = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value") + fun toFalse (Leaf [_,fm]) = fm + | toFalse _ = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value") + in + case t of + (*Const ("Goal", _) $ t1 => + Some (interpret thy model args t1) |*) + Const ("all", _) $ t1 => + let + val (i,m,a) = (interpret thy model args t1) + in + case i of + Node xs => + let + val fmTrue = PropLogic.all (map toTrue xs) + val fmFalse = PropLogic.exists (map toFalse xs) + in + Some (Leaf [fmTrue, fmFalse], m, a) + end + | _ => + raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function") + end + | Const ("==", _) $ t1 $ t2 => + let + val (i1,m1,a1) = interpret thy model args t1 + val (i2,m2,a2) = interpret thy m1 a1 t2 + (* interpretation * interpretation -> prop_formula *) + fun interpret_equal (tr1,tr2) = + (case tr1 of + Leaf x => + (case tr2 of + Leaf y => PropLogic.dot_product (x,y) + | _ => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher")) + | Node xs => + (case tr2 of + Leaf _ => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher") + (* extensionality: two functions are equal iff they are equal for every element *) + | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys)))) + (* interpretation * interpretation -> prop_formula *) + fun interpret_unequal (tr1,tr2) = + (case tr1 of + Leaf x => + (case tr2 of + Leaf y => + let + fun unequal [] ([],_) = + False + | unequal (x::xs) (y::ys1, ys2) = + SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2)) + | unequal _ _ = + raise REFUTE ("Pure_interpreter", "\"==\": leafs have different width") + in + unequal x (y,[]) + end + | _ => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher")) + | Node xs => + (case tr2 of + Leaf _ => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher") + (* extensionality: two functions are unequal iff there exist unequal elements *) + | Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys)))) + val fmTrue = interpret_equal (i1,i2) + val fmFalse = interpret_unequal (i1,i2) + in + Some (Leaf [fmTrue, fmFalse], m2, a2) + end + | Const ("==>", _) $ t1 $ t2 => + let + val (i1,m1,a1) = interpret thy model args t1 + val (i2,m2,a2) = interpret thy m1 a1 t2 + val fmTrue = SOr (toFalse i1, toTrue i2) + val fmFalse = SAnd (toTrue i1, toFalse i2) + in + Some (Leaf [fmTrue, fmFalse], m2, a2) + end + | _ => None + end; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun HOLogic_interpreter thy model args t = + (* ------------------------------------------------------------------------- *) + (* Providing interpretations directly is more efficient than unfolding the *) + (* logical constants; however, we need versions for constants with arguments *) + (* (to avoid unfolding) as well as versions for constants without arguments *) + (* (since in HOL, logical constants can themselves be arguments) *) + (* ------------------------------------------------------------------------- *) + let + fun eta_expand t i = + let + val Ts = binder_types (fastype_of t) + in + foldr (fn (T, t) => Abs ("", T, t)) + (take (i, Ts), list_comb (t, map Bound (i-1 downto 0))) + end + val TT = Leaf [True, False] + val FF = Leaf [False, True] + fun toTrue (Leaf [fm,_]) = fm + | toTrue _ = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value") + fun toFalse (Leaf [_,fm]) = fm + | toFalse _ = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value") + in + case t of + Const ("Trueprop", _) $ t1 => + Some (interpret thy model args t1) + | Const ("Trueprop", _) => + Some (Node [TT, FF], model, args) + | Const ("Not", _) $ t1 => + apply_interpreter thy model args t + | Const ("Not", _) => + Some (Node [FF, TT], model, args) + | Const ("True", _) => + Some (TT, model, args) + | Const ("False", _) => + Some (FF, model, args) + | Const ("arbitrary", T) => + (* treat 'arbitrary' just like a free variable of the same type *) + (case assoc (snd model, t) of + Some intr => + Some (intr, model, args) + | None => + let + val (sizes, intrs) = model + val (intr, _, a) = interpret thy (sizes, []) args (Free ("", T)) + in + Some (intr, (sizes, (t,intr)::intrs), a) + end) + | Const ("The", _) $ t1 => + apply_interpreter thy model args t + | Const ("The", T as Type ("fun", [_, T'])) => + (* treat 'The' like a free variable, but with a fixed interpretation for boolean *) + (* functions that map exactly one constant of type T' to True *) + (case assoc (snd model, t) of + Some intr => + Some (intr, model, args) + | None => + let + val (sizes, intrs) = model + val (intr, _, a) = interpret thy (sizes, []) args (Free ("", T)) + (* create all constants of type T' => bool, ... *) + val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("", Type ("fun", [T', Type ("bool",[])]))) + (* ... and all constants of type T' *) + val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("", T')) + (* returns a list with all unit vectors of length n *) + (* int -> interpretation list *) + fun unit_vectors n = + let + (* returns the k-th unit vector of length n *) + (* int * int -> interpretation *) + fun unit_vector (k,n) = + Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) + (* int -> interpretation list -> interpretation 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 + (* interpretation -> interpretation list *) + fun make_constants (Leaf xs) = + unit_vectors (length xs) + | make_constants (Node xs) = + map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) + val constantsFun = make_constants intrFun + val constantsT' = make_constants intrT' + (* interpretation -> interpretation list -> interpretation option *) + fun the_val (Node xs) cs = + let + val TrueCount = foldl (fn (n,x) => if toTrue x = True then n+1 else n) (0,xs) + fun findThe (x::xs) (c::cs) = + if toTrue x = True then + c + else + findThe xs cs + | findThe _ _ = + raise REFUTE ("HOLogic_interpreter", "\"The\": not found") + in + if TrueCount=1 then + Some (findThe xs cs) + else + None + end + | the_val _ _ = + raise REFUTE ("HOLogic_interpreter", "\"The\": function interpreted as a leaf") + in + case intr of + Node xs => + let + (* replace interpretation 'x' by the interpretation determined by 'f' *) + val intrThe = Node (map (fn (x,f) => if_none (the_val f constantsT') x) (xs ~~ constantsFun)) + in + Some (intrThe, (sizes, (t,intrThe)::intrs), a) + end + | _ => + raise REFUTE ("HOLogic_interpreter", "\"The\": interpretation is a leaf") + end) + | Const ("Hilbert_Choice.Eps", _) $ t1 => + apply_interpreter thy model args t + | Const ("Hilbert_Choice.Eps", T as Type ("fun", [_, T'])) => + (* treat 'The' like a free variable, but with a fixed interpretation for boolean *) + (* functions that map exactly one constant of type T' to True *) + (case assoc (snd model, t) of + Some intr => + Some (intr, model, args) + | None => + let + val (sizes, intrs) = model + val (intr, _, a) = interpret thy (sizes, []) args (Free ("", T)) + (* create all constants of type T' => bool, ... *) + val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("", Type ("fun", [T', Type ("bool",[])]))) + (* ... and all constants of type T' *) + val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("", T')) + (* returns a list with all unit vectors of length n *) + (* int -> interpretation list *) + fun unit_vectors n = + let + (* returns the k-th unit vector of length n *) + (* int * int -> interpretation *) + fun unit_vector (k,n) = + Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) + (* int -> interpretation list -> interpretation 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 + (* interpretation -> interpretation list *) + fun make_constants (Leaf xs) = + unit_vectors (length xs) + | make_constants (Node xs) = + map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) + val constantsFun = make_constants intrFun + val constantsT' = make_constants intrT' + (* interpretation -> interpretation list -> interpretation list *) + fun true_values (Node xs) cs = + mapfilter (fn (x,c) => if toTrue x = True then Some c else None) (xs~~cs) + | true_values _ _ = + raise REFUTE ("HOLogic_interpreter", "\"Eps\": function interpreted as a leaf") + in + case intr of + Node xs => + let + val (wf, intrsEps) = foldl_map (fn (w,(x,f)) => + case true_values f constantsT' of + [] => (w, x) (* no value mapped to true -> no restriction *) + | [c] => (w, c) (* one value mapped to true -> that's the one *) + | cs => + let + (* interpretation * interpretation -> prop_formula *) + fun interpret_equal (tr1,tr2) = + (case tr1 of + Leaf x => + (case tr2 of + Leaf y => PropLogic.dot_product (x,y) + | _ => raise REFUTE ("HOLogic_interpreter", "\"Eps\": second tree is higher")) + | Node xs => + (case tr2 of + Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"Eps\": first tree is higher") + (* extensionality: two functions are equal iff they are equal for every element *) + | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys)))) + in + (SAnd (w, PropLogic.exists (map (fn c => interpret_equal (x,c)) cs)), x) (* impose restrictions on x *) + end + ) + (#wellformed a, xs ~~ constantsFun) + val intrEps = Node intrsEps + in + Some (intrEps, (sizes, (t,intrEps)::intrs), {next_idx = #next_idx a, bounds = #bounds a, wellformed = wf}) + end + | _ => + raise REFUTE ("HOLogic_interpreter", "\"Eps\": interpretation is a leaf") + end) + | Const ("All", _) $ t1 => + let + val (i,m,a) = interpret thy model args t1 + in + case i of + Node xs => + let + val fmTrue = PropLogic.all (map toTrue xs) + val fmFalse = PropLogic.exists (map toFalse xs) + in + Some (Leaf [fmTrue, fmFalse], m, a) + end + | _ => + raise REFUTE ("HOLogic_interpreter", "\"All\" is not followed by a function") + end + | Const ("All", _) => + Some (interpret thy model args (eta_expand t 1)) + | Const ("Ex", _) $ t1 => + let + val (i,m,a) = interpret thy model args t1 + in + case i of + Node xs => + let + val fmTrue = PropLogic.exists (map toTrue xs) + val fmFalse = PropLogic.all (map toFalse xs) + in + Some (Leaf [fmTrue, fmFalse], m, a) + end + | _ => + raise REFUTE ("HOLogic_interpreter", "\"Ex\" is not followed by a function") + end + | Const ("Ex", _) => + Some (interpret thy model args (eta_expand t 1)) + | Const ("Ex1", _) $ t1 => + let + val (i,m,a) = interpret thy model args t1 + in + case i of + Node xs => + let + (* interpretation list -> prop_formula *) + fun allfalse [] = True + | allfalse (x::xs) = SAnd (toFalse x, allfalse xs) + (* interpretation list -> prop_formula *) + fun exactly1true [] = False + | exactly1true (x::xs) = SOr (SAnd (toTrue x, allfalse xs), SAnd (toFalse x, exactly1true xs)) + (* interpretation list -> prop_formula *) + fun atleast2true [] = False + | atleast2true (x::xs) = SOr (SAnd (toTrue x, PropLogic.exists (map toTrue xs)), atleast2true xs) + val fmTrue = exactly1true xs + val fmFalse = SOr (allfalse xs, atleast2true xs) + in + Some (Leaf [fmTrue, fmFalse], m, a) + end + | _ => + raise REFUTE ("HOLogic_interpreter", "\"Ex1\" is not followed by a function") + end + | Const ("Ex1", _) => + Some (interpret thy model args (eta_expand t 1)) + | Const ("op =", _) $ t1 $ t2 => + let + val (i1,m1,a1) = interpret thy model args t1 + val (i2,m2,a2) = interpret thy m1 a1 t2 + (* interpretation * interpretation -> prop_formula *) + fun interpret_equal (tr1,tr2) = + (case tr1 of + Leaf x => + (case tr2 of + Leaf y => PropLogic.dot_product (x,y) + | _ => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher")) + | Node xs => + (case tr2 of + Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher") + (* extensionality: two functions are equal iff they are equal for every element *) + | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys)))) + (* interpretation * interpretation -> prop_formula *) + fun interpret_unequal (tr1,tr2) = + (case tr1 of + Leaf x => + (case tr2 of + Leaf y => + let + fun unequal [] ([],_) = + False + | unequal (x::xs) (y::ys1, ys2) = + SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2)) + | unequal _ _ = + raise REFUTE ("HOLogic_interpreter", "\"==\": leafs have different width") + in + unequal x (y,[]) + end + | _ => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher")) + | Node xs => + (case tr2 of + Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher") + (* extensionality: two functions are unequal iff there exist unequal elements *) + | Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys)))) + val fmTrue = interpret_equal (i1,i2) + val fmFalse = interpret_unequal (i1,i2) + in + Some (Leaf [fmTrue, fmFalse], m2, a2) + end + | Const ("op =", _) $ t1 => + Some (interpret thy model args (eta_expand t 1)) + | Const ("op =", _) => + Some (interpret thy model args (eta_expand t 2)) + | Const ("op &", _) $ t1 $ t2 => + apply_interpreter thy model args t + | Const ("op &", _) $ t1 => + apply_interpreter thy model args t + | Const ("op &", _) => + Some (Node [Node [TT, FF], Node [FF, FF]], model, args) + | Const ("op |", _) $ t1 $ t2 => + apply_interpreter thy model args t + | Const ("op |", _) $ t1 => + apply_interpreter thy model args t + | Const ("op |", _) => + Some (Node [Node [TT, TT], Node [TT, FF]], model, args) + | Const ("op -->", _) $ t1 $ t2 => + apply_interpreter thy model args t + | Const ("op -->", _) $ t1 => + apply_interpreter thy model args t + | Const ("op -->", _) => + Some (Node [Node [TT, FF], Node [TT, TT]], model, args) + | Const ("Collect", _) $ t1 => + (* Collect == identity *) + Some (interpret thy model args t1) + | Const ("Collect", _) => + Some (interpret thy model args (eta_expand t 1)) + | Const ("op :", _) $ t1 $ t2 => + (* op: == application *) + Some (interpret thy model args (t2 $ t1)) + | Const ("op :", _) $ t1 => + Some (interpret thy model args (eta_expand t 1)) + | Const ("op :", _) => + Some (interpret thy model args (eta_expand t 2)) + | _ => None + end; + + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + + fun IDT_interpreter thy model args t = + let + fun is_var (Free _) = true + | is_var (Var _) = true + | is_var _ = false + fun typeof (Free (_,T)) = T + | typeof (Var (_,T)) = T + | typeof _ = raise REFUTE ("var_IDT_interpreter", "term is not a variable") + val (sizes, intrs) = model + (* 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 + (* interpretation -> int *) + fun size_of_interpretation (Leaf xs) = length xs + | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs) + (* Term.typ -> int *) + fun size_of_type T = + let + val (i,_,_) = interpret thy model args (Free ("", T)) + in + size_of_interpretation i + end + (* int list -> int *) + fun sum xs = foldl op+ (0, xs) + (* int list -> int *) + fun product xs = foldl op* (1, xs) + (* DatatypeAux.dtyp * Term.typ -> DatatypeAux.dtyp -> Term.typ *) + fun typ_of_dtyp typ_assoc (DatatypeAux.DtTFree a) = + the (assoc (typ_assoc, DatatypeAux.DtTFree a)) + | typ_of_dtyp typ_assoc (DatatypeAux.DtRec i) = + raise REFUTE ("var_IDT_interpreter", "recursive datatype") + | typ_of_dtyp typ_assoc (DatatypeAux.DtType (s, ds)) = + Type (s, map (typ_of_dtyp typ_assoc) ds) + in + if is_var t then + (case typeof t of + Type (s, Ts) => + (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 - (* 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) + if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then + raise REFUTE ("var_IDT_interpreter", "recursive datatype argument") + else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then + None (* recursive datatype (requires an infinite model) *) + else + case assoc (intrs, t) of + Some intr => Some (intr, model, args) + | None => + let + val typ_assoc = dtyps ~~ Ts + val size = sum (map (fn (_,ds) => + product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) constrs) + val idx = #next_idx args + (* for us, an IDT has no "internal structure" -- its interpretation is just a leaf *) + val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1)))) + val next = (if size=2 then idx+1 else idx+size) + in + (* extend the model, increase 'next_idx' *) + Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args}) + end 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 + | None => None) + | _ => None) + else + let + val (head, params) = strip_comb t (* look into applications to avoid unfolding *) + in + (case head of + Const (c, T) => + (case body_type T of + Type (s, Ts) => + (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)) + in + if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then + raise REFUTE ("var_IDT_interpreter", "recursive datatype argument") + else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then + None (* recursive datatype (requires an infinite model) *) + else + (case take_prefix (fn (c',_) => c' <> c) constrs of + (_, []) => + None (* unknown constructor *) + | (prevs, _) => + if null params then + let + val typ_assoc = dtyps ~~ Ts + val offset = sum (map (fn (_,ds) => + product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) prevs) + val (i,_,_) = interpret thy model args (Free ("", T)) + (* int * interpretation -> int * interpretation *) + fun replace (offset, Leaf xs) = + (* replace the offset-th element by True, all others by False, inc. offset by 1 *) + (offset+1, Leaf (snd (foldl_map (fn (n,_) => (n+1, if n=offset then True else False)) (0, xs)))) + | replace (offset, Node xs) = + let + val (offset', xs') = foldl_map replace (offset, xs) + in + (offset', Node xs') + end + val (_,intr) = replace (offset, i) + in + Some (intr, model, args) + end + else + apply_interpreter thy model args t) (* avoid unfolding by calling 'apply_interpreter' directly *) + end + | None => None) + | _ => None) + | _ => None) + end 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 *) +(* PRINTERS *) (* ------------------------------------------------------------------------- *) - (* Term.typ -> (Term.typ * int) list -> theory -> int -> int -> prop_tree * int *) + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *) - fun type_to_prop_tree T us thy cdepth idx = + fun var_typevar_printer thy model t intr assignment = 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 + fun is_var (Free _) = true + | is_var (Var _) = true + | is_var _ = false + fun typeof (Free (_,T)) = T + | typeof (Var (_,T)) = T + | typeof _ = raise REFUTE ("var_typevar_printer", "term is not a variable") + fun is_typevar (TFree _) = true + | is_typevar (TVar _) = true + | is_typevar _ = false 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]) => + if is_var t andalso is_typevar (typeof t) then 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 + (* interpretation -> int *) + fun index_from_interpretation (Leaf xs) = + let + val idx = find_index (PropLogic.eval assignment) xs + in + if idx<0 then + raise REFUTE ("var_typevar_printer", "illegal interpretation: no value assigned") + else + idx + end + | index_from_interpretation _ = + raise REFUTE ("var_typevar_printer", "interpretation is not a leaf") + (* string -> string *) + fun strip_leading_quote s = + (implode o (fn (x::xs) => if x="'" then xs else (x::xs)) o explode) s + (* Term.typ -> string *) + fun string_of_typ (TFree (x,_)) = strip_leading_quote x + | string_of_typ (TVar ((x,i),_)) = strip_leading_quote x ^ string_of_int i + | string_of_typ _ = raise REFUTE ("var_typevar_printer", "type is not a type variable") 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 + Some (string_of_typ (typeof t) ^ string_of_int (index_from_interpretation intr)) 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 + else + None 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 *) -(* ------------------------------------------------------------------------- *) + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *) - (* Term.typ -> (Term.typ * int) list -> theory -> int -> prop_tree list *) + fun var_funtype_printer thy model t intr assignment = + let + fun is_var (Free _) = true + | is_var (Var _) = true + | is_var _ = false + fun typeof (Free (_,T)) = T + | typeof (Var (_,T)) = T + | typeof _ = raise REFUTE ("var_funtype_printer", "term is not a variable") + fun is_funtype (Type ("fun", [_,_])) = true + | is_funtype _ = false + in + if is_var t andalso is_funtype (typeof t) then + let + val T1 = domain_type (typeof t) + val T2 = range_type (typeof t) + val (sizes, _) = model + (* create all constants of type T1 *) + val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_funtype_printer", T1)) + (* returns a list with all unit vectors of length n *) + (* int -> interpretation list *) + fun unit_vectors n = + let + (* returns the k-th unit vector of length n *) + (* int * int -> interpretation *) + fun unit_vector (k,n) = + Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) + (* int -> interpretation list -> interpretation 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 + (* interpretation -> interpretation list *) + fun make_constants (Leaf xs) = + unit_vectors (length xs) + | make_constants (Node xs) = + map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) + (* interpretation list *) + val results = (case intr of + Node xs => xs + | _ => raise REFUTE ("var_funtype_printer", "interpretation is a leaf")) + (* string list *) + val strings = map + (fn (argi,resulti) => print thy model (Free ("var_funtype_printer", T1)) argi assignment + ^ "\\" + ^ print thy model (Free ("var_funtype_printer", T2)) resulti assignment) + ((make_constants i) ~~ results) + in + Some (enclose "(" ")" (commas strings)) + end + else + None + end; - fun type_to_constants T us thy cdepth = + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *) + + fun var_settype_printer thy model t intr assignment = let + val (sizes, _) = model (* returns a list with all unit vectors of length n *) - (* int -> prop_tree list *) + (* int -> interpretation list *) fun unit_vectors n = let (* returns the k-th unit vector of length n *) - (* int * int -> prop_tree *) + (* int * int -> interpretation *) fun unit_vector (k,n) = Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) - (* int -> prop_tree list -> prop_tree list *) + (* int -> interpretation list -> interpretation list *) fun unit_vectors_acc k vs = if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs) in @@ -918,731 +1573,238 @@ let val rec_pick = pick_all (n-1) xs in foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs) end + (* interpretation -> interpretation list *) + fun make_constants (Leaf xs) = + unit_vectors (length xs) + | make_constants (Node xs) = + map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) in - case T of - Type ("prop", []) => unit_vectors 2 - | Type ("bool", []) => unit_vectors 2 - | Type ("Product_Type.unit", []) => unit_vectors 1 - | Type ("+", [T1,T2]) => + case t of + Free (x, Type ("set", [T])) => let - val s1 = size_of_type T1 us thy cdepth - val s2 = size_of_type T2 us thy cdepth + (* interpretation list *) + val results = (case intr of + Node xs => xs + | _ => raise REFUTE ("var_settype_printer", "interpretation is a leaf")) + (* create all constants of type T *) + val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T)) + (* string list *) + val strings = mapfilter + (fn (argi,Leaf [fmTrue,fmFalse]) => + if PropLogic.eval assignment fmTrue then + Some (print thy model (Free ("x", T)) argi assignment) + else if PropLogic.eval assignment fmFalse then + None + else + raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned")) + ((make_constants i) ~~ results) 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)" + Some (enclose "{" "}" (commas strings)) end - | Type ("fun", [T1,T2]) => + | Var ((x,i), Type ("set", [T])) => let - val s = size_of_type T1 us thy cdepth + (* interpretation list *) + val results = (case intr of + Node xs => xs + | _ => raise REFUTE ("var_settype_printer", "interpretation is a leaf")) + (* create all constants of type T *) + val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T)) + (* string list *) + val strings = mapfilter + (fn (argi,Leaf [fmTrue,fmFalse]) => + if PropLogic.eval assignment fmTrue then + Some (print thy model (Free ("var_settype_printer", T)) argi assignment) + else if PropLogic.eval assignment fmTrue then + None + else + raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned")) + ((make_constants i) ~~ results) in - if s=0 then - raise EMPTY_DATATYPE - else - map (fn xs => Node xs) (pick_all s (type_to_constants T2 us thy cdepth)) + Some (enclose "{" "}" (commas strings)) 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) + | _ => None 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 *) + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *) - 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))); + fun HOLogic_printer thy model t intr assignment = + case t of + (* 'arbitrary', 'The', 'Hilbert_Choice.Eps' are printed like free variables of the same type *) + Const ("arbitrary", T) => + Some (print thy model (Free ("", T)) intr assignment) + | Const ("The", T) => + Some (print thy model (Free ("", T)) intr assignment) + | Const ("Hilbert_Choice.Eps", T) => + Some (print thy model (Free ("", T)) intr assignment) + | _ => + None; -(* ------------------------------------------------------------------------- *) -(* 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' *) -(* ------------------------------------------------------------------------- *) + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *) - (* prop_tree * prop_tree -> prop_tree *) - - fun prop_tree_apply (tr1,tr2) = + fun var_IDT_printer thy model t intr assignment = 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)) + fun is_var (Free _) = true + | is_var (Var _) = true + | is_var _ = false + fun typeof (Free (_,T)) = T + | typeof (Var (_,T)) = T + | typeof _ = raise REFUTE ("var_IDT_printer", "term is not a variable") 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 => + if is_var t then + (case typeof t of + Type (s, Ts) => + (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)) + in + if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then + raise REFUTE ("var_IDT_printer", "recursive datatype argument") + else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then + None (* recursive datatype (requires an infinite model) *) + else let - val fmTrue = list_conjunction (map prop_tree_to_true xs) - val fmFalse = list_disjunction (map prop_tree_to_false xs) + val (sizes, _) = model + val typ_assoc = dtyps ~~ Ts + (* interpretation -> int *) + fun index_from_interpretation (Leaf xs) = + let + val idx = find_index (PropLogic.eval assignment) xs + in + if idx<0 then + raise REFUTE ("var_IDT_printer", "illegal interpretation: no value assigned") + else + idx + end + | index_from_interpretation _ = + raise REFUTE ("var_IDT_printer", "interpretation is not a leaf") + (* 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 (typ_assoc, DatatypeAux.DtTFree a)) + | typ_of_dtyp (DatatypeAux.DtRec i) = + raise REFUTE ("var_IDT_printer", "recursive datatype") + | typ_of_dtyp (DatatypeAux.DtType (s, ds)) = + Type (s, map typ_of_dtyp ds) + fun sum xs = foldl op+ (0, xs) + fun product xs = foldl op* (1, xs) + (* 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 + fun size_of_interpretation (Leaf xs) = length xs + | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs) + fun size_of_type T = + let + val (i,_,_) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("", T)) + in + size_of_interpretation i + end + (* returns a list with all unit vectors of length n *) + (* int -> interpretation list *) + fun unit_vectors n = + let + (* returns the k-th unit vector of length n *) + (* int * int -> interpretation *) + fun unit_vector (k,n) = + Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) + (* int -> interpretation list -> interpretation 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 + (* interpretation -> interpretation list *) + fun make_constants (Leaf xs) = + unit_vectors (length xs) + | make_constants (Node xs) = + map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs))) + (* DatatypeAux.dtyp list -> int -> string *) + fun string_of_inductive_type_cargs [] n = + if n<>0 then + raise REFUTE ("var_IDT_printer", "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)) ds) + val T = typ_of_dtyp d + val (i,_,_) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("", T)) + val constants = make_constants i + in + " " + ^ (print thy model (Free ("", T)) (nth_elem (n div size_ds, constants)) assignment) + ^ (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 ("var_IDT_printer", "inductive type has fewer elements than needed") + | string_of_inductive_type_constrs ((c,ds)::cs) n = + let + val size = product (map (fn d => size_of_type (typ_of_dtyp d)) ds) + in + if n < size then + (unqualify c) ^ (string_of_inductive_type_cargs ds n) + else + string_of_inductive_type_constrs cs (n - size) + end in - (Leaf [fmTrue, fmFalse], (i1,s1)) + Some (string_of_inductive_type_constrs constrs (index_from_interpretation intr)) 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)) + end + | None => None) + | _ => None) 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)) + None end; (* ------------------------------------------------------------------------- *) -(* INTERFACE, PART 2: FINDING A MODEL *) +(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *) +(* structure *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) -(* 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 *) +(* Note: the interpreters and printers are used in reverse order; however, *) +(* an interpreter that can handle non-atomic terms ends up being *) +(* applied before other interpreters are applied to subterms! *) (* ------------------------------------------------------------------------- *) - (* 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) ^ "\\" ^ (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; + (* (theory -> theory) list *) -(* ------------------------------------------------------------------------- *) -(* 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 maxsize0 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)); + val setup = + [RefuteData.init, + add_interpreter "var_typevar" var_typevar_interpreter, + add_interpreter "var_funtype" var_funtype_interpreter, + add_interpreter "var_settype" var_settype_interpreter, + add_interpreter "boundvar" boundvar_interpreter, + add_interpreter "abstraction" abstraction_interpreter, + add_interpreter "apply" apply_interpreter, + add_interpreter "const_unfold" const_unfold_interpreter, + add_interpreter "Pure" Pure_interpreter, + add_interpreter "HOLogic" HOLogic_interpreter, + add_interpreter "IDT" IDT_interpreter, + add_printer "var_typevar" var_typevar_printer, + add_printer "var_funtype" var_funtype_printer, + add_printer "var_settype" var_settype_printer, + add_printer "HOLogic" HOLogic_printer, + add_printer "var_IDT" var_IDT_printer]; end