1.1 --- a/src/HOL/Tools/refute.ML Wed Mar 10 20:36:11 2004 +0100
1.2 +++ b/src/HOL/Tools/refute.ML Wed Mar 10 22:33:48 2004 +0100
1.3 @@ -3,526 +3,77 @@
1.4 Author: Tjark Weber
1.5 Copyright 2003-2004
1.6
1.7 -Finite model generation for HOL formulae, using an external SAT solver.
1.8 +Finite model generation for HOL formulae, using a SAT solver.
1.9 *)
1.10
1.11 (* ------------------------------------------------------------------------- *)
1.12 -(* Declares the 'REFUTE' signature as well as a structure 'Refute'. See *)
1.13 -(* 'find_model' below for a description of the implemented algorithm, and *)
1.14 -(* the Isabelle/Isar theories 'HOL/Refute.thy' and 'HOL/Main.thy' on how to *)
1.15 -(* set things up. *)
1.16 +(* TODO: Change parameter handling so that only supported parameters can be *)
1.17 +(* set, and specify defaults here, rather than in HOL/Main.thy. *)
1.18 +(* ------------------------------------------------------------------------- *)
1.19 +
1.20 +(* ------------------------------------------------------------------------- *)
1.21 +(* Declares the 'REFUTE' signature as well as a structure 'Refute'. *)
1.22 +(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'. *)
1.23 (* ------------------------------------------------------------------------- *)
1.24
1.25 signature REFUTE =
1.26 sig
1.27
1.28 + exception REFUTE of string * string
1.29 +
1.30 +(* ------------------------------------------------------------------------- *)
1.31 +(* Model/interpretation related code (translation HOL -> boolean formula) *)
1.32 +(* ------------------------------------------------------------------------- *)
1.33 +
1.34 + exception CANNOT_INTERPRET
1.35 +
1.36 + type interpretation
1.37 + type model
1.38 + type arguments
1.39 +
1.40 + val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory
1.41 + val add_printer : string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory
1.42 +
1.43 + val interpret : theory -> model -> arguments -> Term.term -> interpretation * model * arguments (* exception CANNOT_INTERPRET *)
1.44 + val is_satisfying_model : model -> interpretation -> bool -> PropLogic.prop_formula
1.45 +
1.46 + val print : theory -> model -> Term.term -> interpretation -> (int -> bool) -> string
1.47 + val print_model : theory -> model -> (int -> bool) -> string
1.48 +
1.49 +(* ------------------------------------------------------------------------- *)
1.50 +(* Interface *)
1.51 +(* ------------------------------------------------------------------------- *)
1.52 +
1.53 + val set_default_param : (string * string) -> theory -> theory
1.54 + val get_default_param : theory -> string -> string option
1.55 + val get_default_params : theory -> (string * string) list
1.56 + val actual_params : theory -> (string * string) list -> (int * int * int * string)
1.57 +
1.58 + val find_model : theory -> (int * int * int * string) -> Term.term -> bool -> unit
1.59 +
1.60 + val satisfy_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model for a formula *)
1.61 + val refute_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model that refutes a formula *)
1.62 + val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
1.63 +
1.64 + val setup : (theory -> theory) list
1.65 +end;
1.66 +
1.67 +structure Refute : REFUTE =
1.68 +struct
1.69 +
1.70 + open PropLogic;
1.71 +
1.72 (* We use 'REFUTE' only for internal error conditions that should *)
1.73 (* never occur in the first place (i.e. errors caused by bugs in our *)
1.74 (* code). Otherwise (e.g. to indicate invalid input data) we use *)
1.75 (* 'error'. *)
1.76 -
1.77 - exception REFUTE of string * string; (* ("in function", "cause") *)
1.78 -
1.79 - val setup : (theory -> theory) list
1.80 -
1.81 - val set_default_param : (string * string) -> theory -> theory
1.82 - val get_default_param : theory -> string -> string option
1.83 - val get_default_params : theory -> (string * string) list
1.84 -
1.85 - val find_model : theory -> (string * string) list -> Term.term -> unit
1.86 -
1.87 - val refute_term : theory -> (string * string) list -> Term.term -> unit
1.88 - val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
1.89 -end;
1.90 -
1.91 -
1.92 -structure Refute : REFUTE =
1.93 -struct
1.94 - exception REFUTE of string * string;
1.95 -
1.96 - exception EMPTY_DATATYPE;
1.97 -
1.98 - structure RefuteDataArgs =
1.99 - struct
1.100 - val name = "Refute/refute";
1.101 - type T = string Symtab.table;
1.102 - val empty = Symtab.empty;
1.103 - val copy = I;
1.104 - val prep_ext = I;
1.105 - val merge =
1.106 - fn (symTable1, symTable2) =>
1.107 - (Symtab.merge (op=) (symTable1, symTable2));
1.108 - fun print sg symTable =
1.109 - writeln
1.110 - ("'refute', default parameters:\n" ^
1.111 - (space_implode "\n" (map (fn (name,value) => name ^ " = " ^ value) (Symtab.dest symTable))))
1.112 - end;
1.113 -
1.114 - structure RefuteData = TheoryDataFun(RefuteDataArgs);
1.115 -
1.116 -
1.117 -(* ------------------------------------------------------------------------- *)
1.118 -(* INTERFACE, PART 1: INITIALIZATION, PARAMETER MANAGEMENT *)
1.119 -(* ------------------------------------------------------------------------- *)
1.120 -
1.121 -(* ------------------------------------------------------------------------- *)
1.122 -(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
1.123 -(* structure *)
1.124 -(* ------------------------------------------------------------------------- *)
1.125 -
1.126 - val setup = [RefuteData.init];
1.127 -
1.128 -(* ------------------------------------------------------------------------- *)
1.129 -(* set_default_param: stores the '(name, value)' pair in RefuteData's symbol *)
1.130 -(* table *)
1.131 -(* ------------------------------------------------------------------------- *)
1.132 -
1.133 - fun set_default_param (name, value) thy =
1.134 - let
1.135 - val symTable = RefuteData.get thy
1.136 - in
1.137 - case Symtab.lookup (symTable, name) of
1.138 - None => RefuteData.put (Symtab.extend (symTable, [(name, value)])) thy
1.139 - | Some _ => RefuteData.put (Symtab.update ((name, value), symTable)) thy
1.140 - end;
1.141 -
1.142 -(* ------------------------------------------------------------------------- *)
1.143 -(* get_default_param: retrieves the value associated with 'name' from *)
1.144 -(* RefuteData's symbol table *)
1.145 -(* ------------------------------------------------------------------------- *)
1.146 -
1.147 - fun get_default_param thy name = Symtab.lookup (RefuteData.get thy, name);
1.148 -
1.149 -(* ------------------------------------------------------------------------- *)
1.150 -(* get_default_params: returns a list of all '(name, value)' pairs that are *)
1.151 -(* stored in RefuteData's symbol table *)
1.152 -(* ------------------------------------------------------------------------- *)
1.153 -
1.154 - fun get_default_params thy = Symtab.dest (RefuteData.get thy);
1.155 -
1.156 -
1.157 -(* ------------------------------------------------------------------------- *)
1.158 -(* PROPOSITIONAL FORMULAS *)
1.159 -(* ------------------------------------------------------------------------- *)
1.160 -
1.161 -(* ------------------------------------------------------------------------- *)
1.162 -(* prop_formula: formulas of propositional logic, built from boolean *)
1.163 -(* variables (referred to by index) and True/False using *)
1.164 -(* not/or/and *)
1.165 -(* ------------------------------------------------------------------------- *)
1.166 -
1.167 - datatype prop_formula =
1.168 - True
1.169 - | False
1.170 - | BoolVar of int
1.171 - | Not of prop_formula
1.172 - | Or of prop_formula * prop_formula
1.173 - | And of prop_formula * prop_formula;
1.174 -
1.175 - (* the following constructor functions make sure that True and False do *)
1.176 - (* not occur within any of the other connectives (i.e. Not, Or, And) *)
1.177 -
1.178 - (* prop_formula -> prop_formula *)
1.179 -
1.180 - fun SNot True = False
1.181 - | SNot False = True
1.182 - | SNot fm = Not fm;
1.183 -
1.184 - (* prop_formula * prop_formula -> prop_formula *)
1.185 -
1.186 - fun SOr (True, _) = True
1.187 - | SOr (_, True) = True
1.188 - | SOr (False, fm) = fm
1.189 - | SOr (fm, False) = fm
1.190 - | SOr (fm1, fm2) = Or (fm1, fm2);
1.191 -
1.192 - (* prop_formula * prop_formula -> prop_formula *)
1.193 -
1.194 - fun SAnd (True, fm) = fm
1.195 - | SAnd (fm, True) = fm
1.196 - | SAnd (False, _) = False
1.197 - | SAnd (_, False) = False
1.198 - | SAnd (fm1, fm2) = And (fm1, fm2);
1.199 + exception REFUTE of string * string; (* ("in function", "cause") *)
1.200
1.201 (* ------------------------------------------------------------------------- *)
1.202 -(* list_disjunction: computes the disjunction of a list of propositional *)
1.203 -(* formulas *)
1.204 -(* ------------------------------------------------------------------------- *)
1.205 -
1.206 - (* prop_formula list -> prop_formula *)
1.207 -
1.208 - fun list_disjunction [] = False
1.209 - | list_disjunction (x::xs) = SOr (x, list_disjunction xs);
1.210 -
1.211 -(* ------------------------------------------------------------------------- *)
1.212 -(* list_conjunction: computes the conjunction of a list of propositional *)
1.213 -(* formulas *)
1.214 -(* ------------------------------------------------------------------------- *)
1.215 -
1.216 - (* prop_formula list -> prop_formula *)
1.217 -
1.218 - fun list_conjunction [] = True
1.219 - | list_conjunction (x::xs) = SAnd (x, list_conjunction xs);
1.220 -
1.221 -(* ------------------------------------------------------------------------- *)
1.222 -(* prop_formula_dot_product: [x1,...,xn] * [y1,...,yn] -> x1*y1+...+xn*yn *)
1.223 -(* ------------------------------------------------------------------------- *)
1.224 -
1.225 - (* prop_formula list * prop_formula list -> prop_formula *)
1.226 -
1.227 - fun prop_formula_dot_product ([],[]) = False
1.228 - | prop_formula_dot_product (x::xs,y::ys) = SOr (SAnd (x,y), prop_formula_dot_product (xs,ys))
1.229 - | prop_formula_dot_product (_,_) = raise REFUTE ("prop_formula_dot_product", "lists are of different length");
1.230 -
1.231 -(* ------------------------------------------------------------------------- *)
1.232 -(* prop_formula_to_nnf: computes the negation normal form of a formula 'fm' *)
1.233 -(* of propositional logic (i.e. only variables may be *)
1.234 -(* negated, but not subformulas) *)
1.235 -(* ------------------------------------------------------------------------- *)
1.236 -
1.237 - (* prop_formula -> prop_formula *)
1.238 -
1.239 - fun prop_formula_to_nnf fm =
1.240 - case fm of
1.241 - (* constants *)
1.242 - True => True
1.243 - | False => False
1.244 - (* literals *)
1.245 - | BoolVar i => BoolVar i
1.246 - | Not (BoolVar i) => Not (BoolVar i)
1.247 - (* double-negation elimination *)
1.248 - | Not (Not fm) => prop_formula_to_nnf fm
1.249 - (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
1.250 - | Not (Or (fm1,fm2)) => SAnd (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
1.251 - | Not (And (fm1,fm2)) => SOr (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
1.252 - (* 'or' and 'and' as outermost connectives are left untouched *)
1.253 - | Or (fm1,fm2) => SOr (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
1.254 - | And (fm1,fm2) => SAnd (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
1.255 - (* 'not' + constant *)
1.256 - | Not _ => raise REFUTE ("prop_formula_to_nnf", "'True'/'False' not allowed inside of 'Not'");
1.257 -
1.258 -(* ------------------------------------------------------------------------- *)
1.259 -(* prop_formula_nnf_to_cnf: computes the conjunctive normal form of a *)
1.260 -(* formula 'fm' of propositional logic that is given in negation normal *)
1.261 -(* form. Note that there may occur an exponential blowup of the *)
1.262 -(* formula. *)
1.263 -(* ------------------------------------------------------------------------- *)
1.264 -
1.265 - (* prop_formula -> prop_formula *)
1.266 -
1.267 - fun prop_formula_nnf_to_cnf fm =
1.268 - case fm of
1.269 - (* constants *)
1.270 - True => True
1.271 - | False => False
1.272 - (* literals *)
1.273 - | BoolVar i => BoolVar i
1.274 - | Not (BoolVar i) => Not (BoolVar i)
1.275 - (* pushing 'or' inside of 'and' using distributive laws *)
1.276 - | Or (fm1,fm2) =>
1.277 - let
1.278 - val fm1' = prop_formula_nnf_to_cnf fm1
1.279 - val fm2' = prop_formula_nnf_to_cnf fm2
1.280 - in
1.281 - case fm1' of
1.282 - And (fm11,fm12) => prop_formula_nnf_to_cnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2')))
1.283 - | _ =>
1.284 - (case fm2' of
1.285 - And (fm21,fm22) => prop_formula_nnf_to_cnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22)))
1.286 - (* neither subformula contains 'and' *)
1.287 - | _ => fm)
1.288 - end
1.289 - (* 'and' as outermost connective is left untouched *)
1.290 - | And (fm1,fm2) => SAnd (prop_formula_nnf_to_cnf fm1, prop_formula_nnf_to_cnf fm2)
1.291 - (* error *)
1.292 - | _ => raise REFUTE ("prop_formula_nnf_to_cnf", "formula is not in negation normal form");
1.293 -
1.294 -(* ------------------------------------------------------------------------- *)
1.295 -(* max: computes the maximum of two integer values 'i' and 'j' *)
1.296 -(* ------------------------------------------------------------------------- *)
1.297 -
1.298 - (* int * int -> int *)
1.299 -
1.300 - fun max (i,j) =
1.301 - if (i>j) then i else j;
1.302 -
1.303 -(* ------------------------------------------------------------------------- *)
1.304 -(* max_var_index: computes the maximal variable index occuring in 'fm', *)
1.305 -(* where 'fm' is a formula of propositional logic *)
1.306 -(* ------------------------------------------------------------------------- *)
1.307 -
1.308 - (* prop_formula -> int *)
1.309 -
1.310 - fun max_var_index fm =
1.311 - case fm of
1.312 - True => 0
1.313 - | False => 0
1.314 - | BoolVar i => i
1.315 - | Not fm1 => max_var_index fm1
1.316 - | And (fm1,fm2) => max (max_var_index fm1, max_var_index fm2)
1.317 - | Or (fm1,fm2) => max (max_var_index fm1, max_var_index fm2);
1.318 -
1.319 -(* ------------------------------------------------------------------------- *)
1.320 -(* prop_formula_nnf_to_def_cnf: computes the definitional conjunctive normal *)
1.321 -(* form of a formula 'fm' of propositional logic that is given in *)
1.322 -(* negation normal form. To avoid an exponential blowup of the *)
1.323 -(* formula, auxiliary variables may be introduced. The result formula *)
1.324 -(* is SAT-equivalent to 'fm' (i.e. it is satisfiable if and only if *)
1.325 -(* 'fm' is satisfiable). *)
1.326 +(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *)
1.327 (* ------------------------------------------------------------------------- *)
1.328
1.329 - (* prop_formula -> prop_formula *)
1.330 -
1.331 - fun prop_formula_nnf_to_def_cnf fm =
1.332 - let
1.333 - (* prop_formula * int -> prop_formula * int *)
1.334 - fun prop_formula_nnf_to_def_cnf_new (fm,new) =
1.335 - (* 'new' specifies the next index that is available to introduce an auxiliary variable *)
1.336 - case fm of
1.337 - (* constants *)
1.338 - True => (True, new)
1.339 - | False => (False, new)
1.340 - (* literals *)
1.341 - | BoolVar i => (BoolVar i, new)
1.342 - | Not (BoolVar i) => (Not (BoolVar i), new)
1.343 - (* pushing 'or' inside of 'and' using distributive laws *)
1.344 - | Or (fm1,fm2) =>
1.345 - let
1.346 - val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
1.347 - val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
1.348 - in
1.349 - case fst fm1' of
1.350 - And (fm11,fm12) =>
1.351 - let
1.352 - val aux = BoolVar (snd fm2')
1.353 - in
1.354 - (* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *)
1.355 - prop_formula_nnf_to_def_cnf_new (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fst fm2', Not aux)), (snd fm2')+1)
1.356 - end
1.357 - | _ =>
1.358 - (case fst fm2' of
1.359 - And (fm21,fm22) =>
1.360 - let
1.361 - val aux = BoolVar (snd fm2')
1.362 - in
1.363 - (* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *)
1.364 - prop_formula_nnf_to_def_cnf_new (SAnd (SOr (fst fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), (snd fm2')+1)
1.365 - end
1.366 - (* neither subformula contains 'and' *)
1.367 - | _ => (fm, new))
1.368 - end
1.369 - (* 'and' as outermost connective is left untouched *)
1.370 - | And (fm1,fm2) =>
1.371 - let
1.372 - val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
1.373 - val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
1.374 - in
1.375 - (SAnd (fst fm1', fst fm2'), snd fm2')
1.376 - end
1.377 - (* error *)
1.378 - | _ => raise REFUTE ("prop_formula_nnf_to_def_cnf", "formula is not in negation normal form")
1.379 - in
1.380 - fst (prop_formula_nnf_to_def_cnf_new (fm, (max_var_index fm)+1))
1.381 - end;
1.382 -
1.383 -(* ------------------------------------------------------------------------- *)
1.384 -(* prop_formula_to_cnf: computes the conjunctive normal form of a formula *)
1.385 -(* 'fm' of propositional logic *)
1.386 -(* ------------------------------------------------------------------------- *)
1.387 -
1.388 - (* prop_formula -> prop_formula *)
1.389 -
1.390 - fun prop_formula_to_cnf fm =
1.391 - prop_formula_nnf_to_cnf (prop_formula_to_nnf fm);
1.392 -
1.393 -(* ------------------------------------------------------------------------- *)
1.394 -(* prop_formula_to_def_cnf: computes the definitional conjunctive normal *)
1.395 -(* form of a formula 'fm' of propositional logic, introducing auxiliary *)
1.396 -(* variables if necessary to avoid an exponential blowup of the formula *)
1.397 -(* ------------------------------------------------------------------------- *)
1.398 -
1.399 - (* prop_formula -> prop_formula *)
1.400 -
1.401 - fun prop_formula_to_def_cnf fm =
1.402 - prop_formula_nnf_to_def_cnf (prop_formula_to_nnf fm);
1.403 -
1.404 -(* ------------------------------------------------------------------------- *)
1.405 -(* prop_formula_to_dimacs_cnf_format: serializes a formula of propositional *)
1.406 -(* logic to a file in DIMACS CNF format (see "Satisfiability Suggested *)
1.407 -(* Format", May 8 1993, Section 2.1) *)
1.408 -(* fm : formula to be serialized. Note: 'fm' must not contain a variable *)
1.409 -(* index less than 1. *)
1.410 -(* def : If true, translate 'fm' into definitional CNF. Otherwise translate *)
1.411 -(* 'fm' into CNF. *)
1.412 -(* path: path of the file to be created *)
1.413 -(* ------------------------------------------------------------------------- *)
1.414 -
1.415 - (* prop_formula -> bool -> Path.T -> unit *)
1.416 -
1.417 - fun prop_formula_to_dimacs_cnf_format fm def path =
1.418 - let
1.419 - (* prop_formula *)
1.420 - val cnf =
1.421 - if def then
1.422 - prop_formula_to_def_cnf fm
1.423 - else
1.424 - prop_formula_to_cnf fm
1.425 - val fm' =
1.426 - case cnf of
1.427 - True => Or (BoolVar 1, Not (BoolVar 1))
1.428 - | False => And (BoolVar 1, Not (BoolVar 1))
1.429 - | _ => cnf (* either 'cnf'=True/False, or 'cnf' does not contain True/False at all *)
1.430 - (* prop_formula -> int *)
1.431 - fun cnf_number_of_clauses (And (fm1,fm2)) =
1.432 - (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
1.433 - | cnf_number_of_clauses _ =
1.434 - 1
1.435 - (* prop_formula -> string *)
1.436 - fun cnf_prop_formula_to_string (BoolVar i) =
1.437 - if (i<1) then
1.438 - raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains a variable index less than 1")
1.439 - else
1.440 - (string_of_int i)
1.441 - | cnf_prop_formula_to_string (Not fm1) =
1.442 - "-" ^ (cnf_prop_formula_to_string fm1)
1.443 - | cnf_prop_formula_to_string (Or (fm1,fm2)) =
1.444 - (cnf_prop_formula_to_string fm1) ^ " " ^ (cnf_prop_formula_to_string fm2)
1.445 - | cnf_prop_formula_to_string (And (fm1,fm2)) =
1.446 - (cnf_prop_formula_to_string fm1) ^ " 0\n" ^ (cnf_prop_formula_to_string fm2)
1.447 - | cnf_prop_formula_to_string _ =
1.448 - raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains True/False")
1.449 - in
1.450 - File.write path ("c This file was generated by prop_formula_to_dimacs_cnf_format\n"
1.451 - ^ "c (c) Tjark Weber\n"
1.452 - ^ "p cnf " ^ (string_of_int (max_var_index fm')) ^ " " ^ (string_of_int (cnf_number_of_clauses fm')) ^ "\n"
1.453 - ^ (cnf_prop_formula_to_string fm') ^ "\n")
1.454 - end;
1.455 -
1.456 -(* ------------------------------------------------------------------------- *)
1.457 -(* prop_formula_to_dimacs_sat_format: serializes a formula of propositional *)
1.458 -(* logic to a file in DIMACS SAT format (see "Satisfiability Suggested *)
1.459 -(* Format", May 8 1993, Section 2.2) *)
1.460 -(* fm : formula to be serialized. Note: 'fm' must not contain a variable *)
1.461 -(* index less than 1. *)
1.462 -(* path: path of the file to be created *)
1.463 -(* ------------------------------------------------------------------------- *)
1.464 -
1.465 - (* prop_formula -> Path.T -> unit *)
1.466 -
1.467 - fun prop_formula_to_dimacs_sat_format fm path =
1.468 - let
1.469 - fun prop_formula_to_string True =
1.470 - "*()"
1.471 - | prop_formula_to_string False =
1.472 - "+()"
1.473 - | prop_formula_to_string (BoolVar i) =
1.474 - if (i<1) then
1.475 - raise REFUTE ("prop_formula_to_dimacs_sat_format", "formula contains a variable index less than 1")
1.476 - else
1.477 - (string_of_int i)
1.478 - | prop_formula_to_string (Not fm1) =
1.479 - "-(" ^ (prop_formula_to_string fm1) ^ ")"
1.480 - | prop_formula_to_string (Or (fm1,fm2)) =
1.481 - "+(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
1.482 - | prop_formula_to_string (And (fm1,fm2)) =
1.483 - "*(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
1.484 - in
1.485 - File.write path ("c This file was generated by prop_formula_to_dimacs_sat_format\n"
1.486 - ^ "c (c) Tjark Weber\n"
1.487 - ^ "p sat " ^ (string_of_int (max (max_var_index fm, 1))) ^ "\n"
1.488 - ^ "(" ^ (prop_formula_to_string fm) ^ ")\n")
1.489 - end;
1.490 -
1.491 -(* ------------------------------------------------------------------------- *)
1.492 -(* prop_formula_sat_solver: try to find a satisfying assignment for the *)
1.493 -(* boolean variables in a propositional formula, using an external SAT *)
1.494 -(* solver. If the SAT solver did not find an assignment, 'None' is *)
1.495 -(* returned. Otherwise 'Some (list of integers)' is returned, where *)
1.496 -(* i>0 means that the boolean variable i is set to TRUE, and i<0 means *)
1.497 -(* that the boolean variable i is set to FALSE. Note that if *)
1.498 -(* 'satformat' is 'defcnf', then the assignment returned may contain *)
1.499 -(* auxiliary variables that were not present in the original formula *)
1.500 -(* 'fm'. *)
1.501 -(* fm : formula that is passed to the SAT solver *)
1.502 -(* satpath : path of the file used to store the propositional formula, *)
1.503 -(* i.e. the input to the SAT solver *)
1.504 -(* satformat : format of the SAT solver's input file. Must be either "cnf", *)
1.505 -(* "defcnf", or "sat". *)
1.506 -(* resultpath: path of the file containing the SAT solver's output *)
1.507 -(* success : part of the line in the SAT solver's output that is followed *)
1.508 -(* by a line consisting of a list of integers representing the *)
1.509 -(* satisfying assignment *)
1.510 -(* command : system command used to execute the SAT solver *)
1.511 -(* ------------------------------------------------------------------------- *)
1.512 -
1.513 - (* prop_formula -> Path.T -> string -> Path.T -> string -> string -> int list option *)
1.514 -
1.515 - fun prop_formula_sat_solver fm satpath satformat resultpath success command =
1.516 - if File.exists satpath then
1.517 - error ("file '" ^ (Path.pack satpath) ^ "' exists, please delete (will not overwrite)")
1.518 - else if File.exists resultpath then
1.519 - error ("file '" ^ (Path.pack resultpath) ^ "' exists, please delete (will not overwrite)")
1.520 - else
1.521 - (
1.522 - (* serialize the formula 'fm' to a file *)
1.523 - if satformat="cnf" then
1.524 - prop_formula_to_dimacs_cnf_format fm false satpath
1.525 - else if satformat="defcnf" then
1.526 - prop_formula_to_dimacs_cnf_format fm true satpath
1.527 - else if satformat="sat" then
1.528 - prop_formula_to_dimacs_sat_format fm satpath
1.529 - else
1.530 - error ("invalid argument: satformat='" ^ satformat ^ "' (must be either 'cnf', 'defcnf', or 'sat')");
1.531 - (* execute SAT solver *)
1.532 - if (system command)<>0 then
1.533 - (
1.534 - (* error executing SAT solver *)
1.535 - File.rm satpath;
1.536 - File.rm resultpath;
1.537 - error ("system command '" ^ command ^ "' failed (make sure a SAT solver is installed)")
1.538 - )
1.539 - else
1.540 - (
1.541 - (* read assignment from the result file *)
1.542 - File.rm satpath;
1.543 - let
1.544 - (* 'a option -> 'a Library.option *)
1.545 - fun option (SOME a) =
1.546 - Some a
1.547 - | option NONE =
1.548 - None
1.549 - (* string -> int list *)
1.550 - fun string_to_int_list s =
1.551 - mapfilter (option o Int.fromString) (space_explode " " s)
1.552 - (* string -> string -> bool *)
1.553 - fun is_substring s1 s2 =
1.554 - let
1.555 - val length1 = String.size s1
1.556 - val length2 = String.size s2
1.557 - in
1.558 - if length2 < length1 then
1.559 - false
1.560 - else if s1 = String.substring (s2, 0, length1) then
1.561 - true
1.562 - else is_substring s1 (String.substring (s2, 1, length2-1))
1.563 - end
1.564 - (* string list -> int list option *)
1.565 - fun extract_solution [] =
1.566 - None
1.567 - | extract_solution (line::lines) =
1.568 - if is_substring success line then
1.569 - (* the next line must be a list of integers *)
1.570 - Some (string_to_int_list (hd lines))
1.571 - else
1.572 - extract_solution lines
1.573 - val sat_result = File.read resultpath
1.574 - in
1.575 - File.rm resultpath;
1.576 - extract_solution (split_lines sat_result)
1.577 - end
1.578 - )
1.579 - );
1.580 -
1.581 + exception CANNOT_INTERPRET;
1.582
1.583 (* ------------------------------------------------------------------------- *)
1.584 (* TREES *)
1.585 @@ -537,9 +88,6 @@
1.586 Leaf of 'a
1.587 | Node of ('a tree) list;
1.588
1.589 - type prop_tree =
1.590 - prop_formula list tree;
1.591 -
1.592 (* ('a -> 'b) -> 'a tree -> 'b tree *)
1.593
1.594 fun tree_map f tr =
1.595 @@ -571,45 +119,95 @@
1.596 Node ys => Node (map tree_pair (xs ~~ ys))
1.597 | Leaf _ => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
1.598
1.599 +
1.600 (* ------------------------------------------------------------------------- *)
1.601 -(* prop_tree_to_true: returns a propositional formula that is true iff the *)
1.602 -(* tree denotes the boolean value TRUE *)
1.603 +(* interpretation: a term's interpretation is given by a variable of type *)
1.604 +(* 'interpretation' *)
1.605 (* ------------------------------------------------------------------------- *)
1.606
1.607 - (* prop_tree -> prop_formula *)
1.608 -
1.609 - (* a term of type 'bool' is represented as a 2-element leaf, where *)
1.610 - (* the term is true iff the leaf's first element is true *)
1.611 -
1.612 - fun prop_tree_to_true (Leaf [fm,_]) =
1.613 - fm
1.614 - | prop_tree_to_true _ =
1.615 - raise REFUTE ("prop_tree_to_true", "tree is not a 2-element leaf");
1.616 + type interpretation =
1.617 + prop_formula list tree;
1.618
1.619 (* ------------------------------------------------------------------------- *)
1.620 -(* prop_tree_to_false: returns a propositional formula that is true iff the *)
1.621 -(* tree denotes the boolean value FALSE *)
1.622 +(* model: a model specifies the size of types and the interpretation of *)
1.623 +(* terms *)
1.624 (* ------------------------------------------------------------------------- *)
1.625
1.626 - (* prop_tree -> prop_formula *)
1.627 + type model =
1.628 + (Term.typ * int) list * (Term.term * interpretation) list;
1.629
1.630 - (* a term of type 'bool' is represented as a 2-element leaf, where *)
1.631 - (* the term is false iff the leaf's second element is true *)
1.632 +(* ------------------------------------------------------------------------- *)
1.633 +(* arguments: additional arguments required during interpretation of terms *)
1.634 +(* ------------------------------------------------------------------------- *)
1.635 +
1.636 + type arguments =
1.637 + {next_idx: int, bounds: interpretation list, wellformed: prop_formula};
1.638 +
1.639
1.640 - fun prop_tree_to_false (Leaf [_,fm]) =
1.641 - fm
1.642 - | prop_tree_to_false _ =
1.643 - raise REFUTE ("prop_tree_to_false", "tree is not a 2-element leaf");
1.644 + structure RefuteDataArgs =
1.645 + struct
1.646 + val name = "HOL/refute";
1.647 + type T =
1.648 + {interpreters: (string * (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option)) list,
1.649 + printers: (string * (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option)) list,
1.650 + parameters: string Symtab.table};
1.651 + val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
1.652 + val copy = I;
1.653 + val prep_ext = I;
1.654 + fun merge
1.655 + ({interpreters = in1, printers = pr1, parameters = pa1},
1.656 + {interpreters = in2, printers = pr2, parameters = pa2}) =
1.657 + {interpreters = rev (merge_alists (rev in1) (rev in2)),
1.658 + printers = rev (merge_alists (rev pr1) (rev pr2)),
1.659 + parameters = Symtab.merge (op=) (pa1, pa2)};
1.660 + fun print sg {interpreters, printers, parameters} =
1.661 + Pretty.writeln (Pretty.chunks
1.662 + [Pretty.strs ("default parameters:" :: flat (map (fn (name,value) => [name, "=", value]) (Symtab.dest parameters))),
1.663 + Pretty.strs ("interpreters:" :: map fst interpreters),
1.664 + Pretty.strs ("printers:" :: map fst printers)]);
1.665 + end;
1.666 +
1.667 + structure RefuteData = TheoryDataFun(RefuteDataArgs);
1.668 +
1.669
1.670 (* ------------------------------------------------------------------------- *)
1.671 -(* restrict_to_single_element: returns a propositional formula which is true *)
1.672 -(* iff the tree 'tr' describes a single element of its corresponding *)
1.673 -(* type, i.e. iff at each leaf, one and only one formula is true *)
1.674 +(* interpret: tries to interpret the term 't' using a suitable interpreter; *)
1.675 +(* returns the interpretation and a (possibly extended) model *)
1.676 +(* that keeps track of the interpretation of subterms *)
1.677 +(* Note: exception 'CANNOT_INTERPRETE' is raised if the term cannot be *)
1.678 +(* interpreted by any interpreter *)
1.679 (* ------------------------------------------------------------------------- *)
1.680
1.681 - (* prop_tree -> prop_formula *)
1.682 + (* theory -> model -> arguments -> Term.term -> interpretation * model * arguments *)
1.683 +
1.684 + fun interpret thy model args t =
1.685 + (case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of
1.686 + None =>
1.687 + (std_output "\n"; warning ("Unable to interpret term:\n" ^ Sign.string_of_term (sign_of thy) t);
1.688 + raise CANNOT_INTERPRET)
1.689 + | Some x => x);
1.690 +
1.691 +(* ------------------------------------------------------------------------- *)
1.692 +(* print: tries to print the constant denoted by the term 't' using a *)
1.693 +(* suitable printer *)
1.694 +(* ------------------------------------------------------------------------- *)
1.695
1.696 - fun restrict_to_single_element tr =
1.697 + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string *)
1.698 +
1.699 + fun print thy model t intr assignment =
1.700 + (case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) of
1.701 + None => "<<no printer available>>"
1.702 + | Some s => s);
1.703 +
1.704 +(* ------------------------------------------------------------------------- *)
1.705 +(* is_satisfying_model: returns a propositional formula that is true iff the *)
1.706 +(* given interpretation denotes 'satisfy', and the model meets certain *)
1.707 +(* well-formedness properties *)
1.708 +(* ------------------------------------------------------------------------- *)
1.709 +
1.710 + (* model -> interpretation -> bool -> PropLogic.prop_formula *)
1.711 +
1.712 + fun is_satisfying_model model intr satisfy =
1.713 let
1.714 (* prop_formula list -> prop_formula *)
1.715 fun allfalse [] = True
1.716 @@ -617,290 +215,1347 @@
1.717 (* prop_formula list -> prop_formula *)
1.718 fun exactly1true [] = False
1.719 | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
1.720 + (* ------------------------------------------------------------------------- *)
1.721 + (* restrict_to_single_element: returns a propositional formula that is true *)
1.722 + (* iff the interpretation denotes a single element of its corresponding *)
1.723 + (* type, i.e. iff at each leaf, one and only one formula is true *)
1.724 + (* ------------------------------------------------------------------------- *)
1.725 + (* interpretation -> prop_formula *)
1.726 + fun restrict_to_single_element (Leaf [BoolVar i, Not (BoolVar j)]) =
1.727 + if (i=j) then
1.728 + True (* optimization for boolean variables *)
1.729 + else
1.730 + raise REFUTE ("is_satisfying_model", "boolean variables in leaf have different indices")
1.731 + | restrict_to_single_element (Leaf xs) =
1.732 + exactly1true xs
1.733 + | restrict_to_single_element (Node trees) =
1.734 + PropLogic.all (map restrict_to_single_element trees)
1.735 in
1.736 - case tr of
1.737 - Leaf [BoolVar _, Not (BoolVar _)] => True (* optimization for boolean variables *)
1.738 - | Leaf xs => exactly1true xs
1.739 - | Node trees => list_conjunction (map restrict_to_single_element trees)
1.740 + (* a term of type 'bool' is represented as a 2-element leaf, where *)
1.741 + (* the term is true iff the leaf's first element is true, and false *)
1.742 + (* iff the leaf's second element is true *)
1.743 + case intr of
1.744 + Leaf [fmT,fmF] =>
1.745 + (* well-formedness properties and formula 'fmT'/'fmF' *)
1.746 + SAnd (PropLogic.all (map (restrict_to_single_element o snd) (snd model)), if satisfy then fmT else fmF)
1.747 + | _ =>
1.748 + raise REFUTE ("is_satisfying_model", "interpretation does not denote a boolean value")
1.749 + end;
1.750 +
1.751 +(* ------------------------------------------------------------------------- *)
1.752 +(* print_model: turns the model into a string, using a fixed interpretation *)
1.753 +(* (given by an assignment for boolean variables) and suitable *)
1.754 +(* printers *)
1.755 +(* ------------------------------------------------------------------------- *)
1.756 +
1.757 + fun print_model thy model assignment =
1.758 + let
1.759 + val (typs, terms) = model
1.760 + in
1.761 + (if null typs then
1.762 + "empty universe (no type variables in term)"
1.763 + else
1.764 + "Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs))
1.765 + ^ "\n"
1.766 + ^ (if null terms then
1.767 + "empty interpretation (no free variables in term)"
1.768 + else
1.769 + space_implode "\n" (map
1.770 + (fn (t,intr) =>
1.771 + Sign.string_of_term (sign_of thy) t ^ ": " ^ print thy model t intr assignment)
1.772 + terms)
1.773 + )
1.774 + ^ "\n"
1.775 + end;
1.776 +
1.777 +
1.778 +(* ------------------------------------------------------------------------- *)
1.779 +(* PARAMETER MANAGEMENT *)
1.780 +(* ------------------------------------------------------------------------- *)
1.781 +
1.782 + (* string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory *)
1.783 +
1.784 + fun add_interpreter name f thy =
1.785 + let
1.786 + val {interpreters, printers, parameters} = RefuteData.get thy
1.787 + in
1.788 + case assoc (interpreters, name) of
1.789 + None => RefuteData.put {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} thy
1.790 + | Some _ => error ("Interpreter " ^ name ^ " already declared")
1.791 + end;
1.792 +
1.793 + (* string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory *)
1.794 +
1.795 + fun add_printer name f thy =
1.796 + let
1.797 + val {interpreters, printers, parameters} = RefuteData.get thy
1.798 + in
1.799 + case assoc (printers, name) of
1.800 + None => RefuteData.put {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} thy
1.801 + | Some _ => error ("Printer " ^ name ^ " already declared")
1.802 + end;
1.803 +
1.804 +(* ------------------------------------------------------------------------- *)
1.805 +(* set_default_param: stores the '(name, value)' pair in RefuteData's *)
1.806 +(* parameter table *)
1.807 +(* ------------------------------------------------------------------------- *)
1.808 +
1.809 + (* (string * string) -> theory -> theory *)
1.810 +
1.811 + fun set_default_param (name, value) thy =
1.812 + let
1.813 + val {interpreters, printers, parameters} = RefuteData.get thy
1.814 + in
1.815 + case Symtab.lookup (parameters, name) of
1.816 + None => RefuteData.put
1.817 + {interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy
1.818 + | Some _ => RefuteData.put
1.819 + {interpreters = interpreters, printers = printers, parameters = Symtab.update ((name, value), parameters)} thy
1.820 end;
1.821
1.822 (* ------------------------------------------------------------------------- *)
1.823 -(* HOL FORMULAS *)
1.824 +(* get_default_param: retrieves the value associated with 'name' from *)
1.825 +(* RefuteData's parameter table *)
1.826 +(* ------------------------------------------------------------------------- *)
1.827 +
1.828 + (* theory -> string -> string option *)
1.829 +
1.830 + fun get_default_param thy name = Symtab.lookup ((#parameters o RefuteData.get) thy, name);
1.831 +
1.832 +(* ------------------------------------------------------------------------- *)
1.833 +(* get_default_params: returns a list of all '(name, value)' pairs that are *)
1.834 +(* stored in RefuteData's parameter table *)
1.835 +(* ------------------------------------------------------------------------- *)
1.836 +
1.837 + (* theory -> (string * string) list *)
1.838 +
1.839 + fun get_default_params thy = (Symtab.dest o #parameters o RefuteData.get) thy;
1.840 +
1.841 +(* ------------------------------------------------------------------------- *)
1.842 +(* actual_params: takes a (possibly empty) list 'params' of parameters that *)
1.843 +(* override the default parameters currently specified in 'thy', and *)
1.844 +(* returns a tuple that can be passed to 'find_model'. *)
1.845 +(* *)
1.846 +(* The following parameters are supported (and required!): *)
1.847 +(* *)
1.848 +(* Name Type Description *)
1.849 +(* *)
1.850 +(* "minsize" int Only search for models with size at least *)
1.851 +(* 'minsize'. *)
1.852 +(* "maxsize" int If >0, only search for models with size at most *)
1.853 +(* 'maxsize'. *)
1.854 +(* "maxvars" int If >0, use at most 'maxvars' boolean variables *)
1.855 +(* when transforming the term into a propositional *)
1.856 +(* formula. *)
1.857 +(* "satsolver" string SAT solver to be used. *)
1.858 +(* ------------------------------------------------------------------------- *)
1.859 +
1.860 + (* theory -> (string * string) list -> (int * int * int * string) *)
1.861 +
1.862 + fun actual_params thy params =
1.863 + let
1.864 + (* (string * string) list * string -> int *)
1.865 + fun read_int (parms, name) =
1.866 + case assoc_string (parms, name) of
1.867 + Some s => (case Int.fromString s of
1.868 + SOME i => i
1.869 + | NONE => error ("parameter " ^ quote name ^ " (value is " ^ quote s ^ ") must be an integer value"))
1.870 + | None => error ("parameter " ^ quote name ^ " must be assigned a value")
1.871 + (* (string * string) list * string -> string *)
1.872 + fun read_string (parms, name) =
1.873 + case assoc_string (parms, name) of
1.874 + Some s => s
1.875 + | None => error ("parameter " ^ quote name ^ " must be assigned a value")
1.876 + (* (string * string) list *)
1.877 + val allparams = params @ (get_default_params thy) (* 'params' first, defaults last (to override) *)
1.878 + (* int *)
1.879 + val minsize = read_int (allparams, "minsize")
1.880 + val maxsize = read_int (allparams, "maxsize")
1.881 + val maxvars = read_int (allparams, "maxvars")
1.882 + (* string *)
1.883 + val satsolver = read_string (allparams, "satsolver")
1.884 + in
1.885 + (minsize, maxsize, maxvars, satsolver)
1.886 + end;
1.887 +
1.888 +(* ------------------------------------------------------------------------- *)
1.889 +(* find_model: repeatedly calls 'invoke_propgen' with appropriate *)
1.890 +(* parameters, applies the SAT solver, and (in case a model is *)
1.891 +(* found) displays the model to the user *)
1.892 +(* thy : the current theory *)
1.893 +(* minsize : the minimal size of the model *)
1.894 +(* maxsize : the maximal size of the model *)
1.895 +(* maxvars : the maximal number of boolean variables to be used *)
1.896 +(* satsolver: the name of the SAT solver to be used *)
1.897 +(* satisfy : if 'True', search for a model that makes 't' true; otherwise *)
1.898 +(* search for a model that makes 't' false *)
1.899 +(* ------------------------------------------------------------------------- *)
1.900 +
1.901 + (* theory -> (int * int * int * string) -> Term.term -> bool -> unit *)
1.902 +
1.903 + fun find_model thy (minsize, maxsize, maxvars, satsolver) t satisfy =
1.904 + let
1.905 + (* Term.typ list *)
1.906 + val tvars = map (fn (i,s) => TVar(i,s)) (term_tvars t)
1.907 + val tfrees = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
1.908 + (* int -> unit *)
1.909 + fun find_model_loop size =
1.910 + (* 'maxsize=0' means "search for arbitrary large models" *)
1.911 + if size>maxsize andalso maxsize<>0 then
1.912 + writeln ("Search terminated: maxsize=" ^ string_of_int maxsize ^ " exceeded.")
1.913 + else
1.914 + let
1.915 + (* ------------------------------------------------------------------------- *)
1.916 + (* make_universes: given a list 'xs' of "types" and a universe size 'size', *)
1.917 + (* this function returns all possible partitions of the universe into *)
1.918 + (* the "types" in 'xs' such that no "type" is empty. If 'size' is less *)
1.919 + (* than 'length xs', the returned list of partitions is empty. *)
1.920 + (* Otherwise, if the list 'xs' is empty, then the returned list of *)
1.921 + (* partitions contains only the empty list, regardless of 'size'. *)
1.922 + (* ------------------------------------------------------------------------- *)
1.923 + (* 'a list -> int -> ('a * int) list list *)
1.924 + fun make_universes xs size =
1.925 + let
1.926 + (* 'a list -> int -> int -> ('a * int) list list *)
1.927 + fun make_partitions_loop (x::xs) 0 total =
1.928 + map (fn us => ((x,0)::us)) (make_partitions xs total)
1.929 + | make_partitions_loop (x::xs) first total =
1.930 + (map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
1.931 + | make_partitions_loop _ _ _ =
1.932 + raise REFUTE ("find_model", "empty list (in make_partitions_loop)")
1.933 + and
1.934 + (* 'a list -> int -> ('a * int) list list *)
1.935 + make_partitions [x] size =
1.936 + (* we must use all remaining elements on the type 'x', so there is only one partition *)
1.937 + [[(x,size)]]
1.938 + | make_partitions (x::xs) 0 =
1.939 + (* there are no elements left in the universe, so there is only one partition *)
1.940 + [map (fn t => (t,0)) (x::xs)]
1.941 + | make_partitions (x::xs) size =
1.942 + (* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
1.943 + make_partitions_loop (x::xs) size size
1.944 + | make_partitions _ _ =
1.945 + raise REFUTE ("find_model", "empty list (in make_partitions)")
1.946 + val len = length xs
1.947 + in
1.948 + if size<len then
1.949 + (* the universe isn't big enough to make every type non-empty *)
1.950 + []
1.951 + else if xs=[] then
1.952 + (* no types: return one universe, regardless of the size *)
1.953 + [[]]
1.954 + else
1.955 + (* partition into possibly empty types, then add 1 element to each type *)
1.956 + map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
1.957 + end
1.958 + (* ('a * int) list -> bool *)
1.959 + fun find_interpretation xs =
1.960 + let
1.961 + val init_model = (xs, [])
1.962 + val init_args = {next_idx = 1, bounds = [], wellformed = True}
1.963 + val (intr, model, args) = interpret thy init_model init_args t
1.964 + val fm = SAnd (#wellformed args, is_satisfying_model model intr satisfy)
1.965 + val usedvars = maxidx fm
1.966 + in
1.967 + (* 'maxvars=0' means "use as many variables as necessary" *)
1.968 + if usedvars>maxvars andalso maxvars<>0 then
1.969 + (writeln ("\nSearch terminated: " ^ string_of_int usedvars ^ " boolean variables used (only " ^ string_of_int maxvars ^ " allowed).");
1.970 + true)
1.971 + else
1.972 + (
1.973 + std_output " invoking SAT solver...";
1.974 + case SatSolver.invoke_solver satsolver fm of
1.975 + None =>
1.976 + (std_output " no model found.\n";
1.977 + false)
1.978 + | Some assignment =>
1.979 + (writeln ("\nModel found:\n" ^ print_model thy model assignment);
1.980 + true)
1.981 + )
1.982 + end handle CANNOT_INTERPRET => true
1.983 + (* TODO: change this to false once the ability to interpret terms depends on the universe *)
1.984 + in
1.985 + case make_universes (tvars@tfrees) size of
1.986 + [] =>
1.987 + (writeln ("Searching for a model of size " ^ string_of_int size ^ ": cannot make every type non-empty (model is too small).");
1.988 + find_model_loop (size+1))
1.989 + | [[]] =>
1.990 + (std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term...");
1.991 + if find_interpretation [] then
1.992 + ()
1.993 + else
1.994 + writeln ("Search terminated: no type variables in term."))
1.995 + | us =>
1.996 + let
1.997 + fun loop [] =
1.998 + find_model_loop (size+1)
1.999 + | loop (u::us) =
1.1000 + (std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term...");
1.1001 + if find_interpretation u then () else loop us)
1.1002 + in
1.1003 + loop us
1.1004 + end
1.1005 + end
1.1006 + in
1.1007 + writeln ("Trying to find a model that "
1.1008 + ^ (if satisfy then "satisfies" else "refutes")
1.1009 + ^ ": " ^ (Sign.string_of_term (sign_of thy) t));
1.1010 + if minsize<1 then
1.1011 + writeln "\"minsize\" is less than 1; starting search with size 1."
1.1012 + else ();
1.1013 + find_model_loop (Int.max (minsize,1))
1.1014 + end;
1.1015 +
1.1016 +
1.1017 +(* ------------------------------------------------------------------------- *)
1.1018 +(* INTERFACE, PART 2: FINDING A MODEL *)
1.1019 (* ------------------------------------------------------------------------- *)
1.1020
1.1021 (* ------------------------------------------------------------------------- *)
1.1022 -(* absvar: form an abstraction over a schematic variable *)
1.1023 -(* ------------------------------------------------------------------------- *)
1.1024 -
1.1025 - (* Term.indexname * Term.typ * Term.term -> Term.term *)
1.1026 -
1.1027 - (* this function is similar to Term.absfree, but for schematic *)
1.1028 - (* variables (rather than free variables) *)
1.1029 - fun absvar ((x,i),T,body) =
1.1030 - Abs(x, T, abstract_over (Var((x,i),T), body));
1.1031 -
1.1032 -(* ------------------------------------------------------------------------- *)
1.1033 -(* list_all_var: quantification over a list of schematic variables *)
1.1034 +(* satisfy_term: calls 'find_model' to find a model that satisfies 't' *)
1.1035 +(* params : list of '(name, value)' pairs used to override default *)
1.1036 +(* parameters *)
1.1037 (* ------------------------------------------------------------------------- *)
1.1038
1.1039 - (* (Term.indexname * Term.typ) list * Term.term -> Term.term *)
1.1040 -
1.1041 - (* this function is similar to Term.list_all_free, but for schematic *)
1.1042 - (* variables (rather than free variables) *)
1.1043 - fun list_all_var ([], t) =
1.1044 - t
1.1045 - | list_all_var ((idx,T)::vars, t) =
1.1046 - (all T) $ (absvar(idx, T, list_all_var(vars,t)));
1.1047 + (* theory -> (string * string) list -> Term.term -> unit *)
1.1048
1.1049 -(* ------------------------------------------------------------------------- *)
1.1050 -(* close_vars: close up a formula over all schematic variables by *)
1.1051 -(* quantification (note that the result term may still contain *)
1.1052 -(* (non-schematic) free variables) *)
1.1053 -(* ------------------------------------------------------------------------- *)
1.1054 -
1.1055 - (* Term.term -> Term.term *)
1.1056 -
1.1057 - (* this function is similar to Logic.close_form, but for schematic *)
1.1058 - (* variables (rather than free variables) *)
1.1059 - fun close_vars A =
1.1060 - list_all_var (sort_wrt (fst o fst) (map dest_Var (term_vars A)), A);
1.1061 + fun satisfy_term thy params t =
1.1062 + find_model thy (actual_params thy params) t true;
1.1063
1.1064 (* ------------------------------------------------------------------------- *)
1.1065 -(* make_universes: given a list 'xs' of "types" and a universe size 'size', *)
1.1066 -(* this function returns all possible partitions of the universe into *)
1.1067 -(* the "types" in 'xs' such that no "type" is empty. If 'size' is less *)
1.1068 -(* than 'length xs', the returned list of partitions is empty. *)
1.1069 -(* Otherwise, if the list 'xs' is empty, then the returned list of *)
1.1070 -(* partitions contains only the empty list, regardless of 'size'. *)
1.1071 +(* refute_term: calls 'find_model' to find a model that refutes 't' *)
1.1072 +(* params : list of '(name, value)' pairs used to override default *)
1.1073 +(* parameters *)
1.1074 (* ------------------------------------------------------------------------- *)
1.1075
1.1076 - (* 'a list -> int -> ('a * int) list list *)
1.1077 + (* theory -> (string * string) list -> Term.term -> unit *)
1.1078
1.1079 - fun make_universes xs size =
1.1080 + fun refute_term thy params t =
1.1081 let
1.1082 - (* 'a list -> int -> int -> ('a * int) list list *)
1.1083 - fun make_partitions_loop (x::xs) 0 total =
1.1084 - map (fn us => ((x,0)::us)) (make_partitions xs total)
1.1085 - | make_partitions_loop (x::xs) first total =
1.1086 - (map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
1.1087 - | make_partitions_loop _ _ _ =
1.1088 - raise REFUTE ("make_universes::make_partitions_loop", "empty list")
1.1089 - and
1.1090 - (* 'a list -> int -> ('a * int) list list *)
1.1091 - make_partitions [x] size =
1.1092 - (* we must use all remaining elements on the type 'x', so there is only one partition *)
1.1093 - [[(x,size)]]
1.1094 - | make_partitions (x::xs) 0 =
1.1095 - (* there are no elements left in the universe, so there is only one partition *)
1.1096 - [map (fn t => (t,0)) (x::xs)]
1.1097 - | make_partitions (x::xs) size =
1.1098 - (* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
1.1099 - make_partitions_loop (x::xs) size size
1.1100 - | make_partitions _ _ =
1.1101 - raise REFUTE ("make_universes::make_partitions", "empty list")
1.1102 - val len = length xs
1.1103 + (* disallow schematic type variables, since we cannot properly negate terms containing them *)
1.1104 + val _ = assert (null (term_tvars t)) "Term to be refuted contains schematic type variables"
1.1105 + (* existential closure over schematic variables *)
1.1106 + (* (Term.indexname * Term.typ) list *)
1.1107 + val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
1.1108 + (* Term.term *)
1.1109 + val ex_closure = foldl
1.1110 + (fn (t', ((x,i),T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
1.1111 + (t, vars)
1.1112 + (* If 't' is of type 'propT' (rather than 'boolT'), applying *)
1.1113 + (* 'HOLogic.exists_const' is not type-correct. However, this *)
1.1114 + (* isn't really a problem as long as 'find_model' still *)
1.1115 + (* interprets the resulting term correctly, without checking *)
1.1116 + (* its type. *)
1.1117 in
1.1118 - if size<len then
1.1119 - (* the universe isn't big enough to make every type non-empty *)
1.1120 - []
1.1121 - else if xs=[] then
1.1122 - (* no types: return one universe, regardless of the size *)
1.1123 - [[]]
1.1124 - else
1.1125 - (* partition into possibly empty types, then add 1 element to each type *)
1.1126 - map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
1.1127 + find_model thy (actual_params thy params) ex_closure false
1.1128 end;
1.1129
1.1130 (* ------------------------------------------------------------------------- *)
1.1131 -(* sum: computes the sum of a list of integers; sum [] = 0 *)
1.1132 -(* ------------------------------------------------------------------------- *)
1.1133 -
1.1134 - (* int list -> int *)
1.1135 -
1.1136 - fun sum xs = foldl op+ (0, xs);
1.1137 -
1.1138 -(* ------------------------------------------------------------------------- *)
1.1139 -(* product: computes the product of a list of integers; product [] = 1 *)
1.1140 +(* refute_subgoal: calls 'refute_term' on a specific subgoal *)
1.1141 +(* params : list of '(name, value)' pairs used to override default *)
1.1142 +(* parameters *)
1.1143 +(* subgoal : 0-based index specifying the subgoal number *)
1.1144 (* ------------------------------------------------------------------------- *)
1.1145
1.1146 - (* int list -> int *)
1.1147 -
1.1148 - fun product xs = foldl op* (1, xs);
1.1149 + (* theory -> (string * string) list -> Thm.thm -> int -> unit *)
1.1150
1.1151 -(* ------------------------------------------------------------------------- *)
1.1152 -(* power: power(a,b) computes a^b, for a>=0, b>=0 *)
1.1153 -(* ------------------------------------------------------------------------- *)
1.1154 + fun refute_subgoal thy params thm subgoal =
1.1155 + refute_term thy params (nth_elem (subgoal, prems_of thm));
1.1156
1.1157 - (* int * int -> int *)
1.1158 -
1.1159 - fun power (a,0) = 1
1.1160 - | power (a,1) = a
1.1161 - | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end;
1.1162
1.1163 (* ------------------------------------------------------------------------- *)
1.1164 -(* size_of_type: returns the size of a type, where 'us' specifies the size *)
1.1165 -(* of each basic type (i.e. each type variable), and 'cdepth' specifies *)
1.1166 -(* the maximal constructor depth for inductive datatypes *)
1.1167 +(* INTERPRETERS *)
1.1168 (* ------------------------------------------------------------------------- *)
1.1169
1.1170 - (* Term.typ -> (Term.typ * int) list -> theory -> int -> int *)
1.1171 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1172
1.1173 - fun size_of_type T us thy cdepth =
1.1174 + fun var_typevar_interpreter thy model args t =
1.1175 let
1.1176 - (* Term.typ -> (Term.typ * int) -> int *)
1.1177 - fun lookup_size T [] =
1.1178 - raise REFUTE ("size_of_type", "no size specified for type variable '" ^ (Sign.string_of_typ (sign_of thy) T) ^ "'")
1.1179 - | lookup_size T ((typ,size)::pairs) =
1.1180 - if T=typ then size else lookup_size T pairs
1.1181 + fun is_var (Free _) = true
1.1182 + | is_var (Var _) = true
1.1183 + | is_var _ = false
1.1184 + fun typeof (Free (_,T)) = T
1.1185 + | typeof (Var (_,T)) = T
1.1186 + | typeof _ = raise REFUTE ("var_typevar_interpreter", "term is not a variable")
1.1187 + fun is_typevar (TFree _) = true
1.1188 + | is_typevar (TVar _) = true
1.1189 + | is_typevar _ = false
1.1190 + val (sizes, intrs) = model
1.1191 + in
1.1192 + if is_var t andalso is_typevar (typeof t) then
1.1193 + (case assoc (intrs, t) of
1.1194 + Some intr => Some (intr, model, args)
1.1195 + | None =>
1.1196 + let
1.1197 + val size = (the o assoc) (sizes, typeof t) (* the model MUST specify a size for type variables *)
1.1198 + val idx = #next_idx args
1.1199 + val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1))))
1.1200 + val next = (if size=2 then idx+1 else idx+size)
1.1201 + in
1.1202 + (* extend the model, increase 'next_idx' *)
1.1203 + Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args})
1.1204 + end)
1.1205 + else
1.1206 + None
1.1207 + end;
1.1208 +
1.1209 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1210 +
1.1211 + fun var_funtype_interpreter thy model args t =
1.1212 + let
1.1213 + fun is_var (Free _) = true
1.1214 + | is_var (Var _) = true
1.1215 + | is_var _ = false
1.1216 + fun typeof (Free (_,T)) = T
1.1217 + | typeof (Var (_,T)) = T
1.1218 + | typeof _ = raise REFUTE ("var_funtype_interpreter", "term is not a variable")
1.1219 + fun stringof (Free (x,_)) = x
1.1220 + | stringof (Var ((x,_), _)) = x
1.1221 + | stringof _ = raise REFUTE ("var_funtype_interpreter", "term is not a variable")
1.1222 + fun is_funtype (Type ("fun", [_,_])) = true
1.1223 + | is_funtype _ = false
1.1224 + val (sizes, intrs) = model
1.1225 in
1.1226 - case T of
1.1227 - Type ("prop", []) => 2
1.1228 - | Type ("bool", []) => 2
1.1229 - | Type ("Product_Type.unit", []) => 1
1.1230 - | Type ("+", [T1,T2]) => (size_of_type T1 us thy cdepth) + (size_of_type T2 us thy cdepth)
1.1231 - | Type ("*", [T1,T2]) => (size_of_type T1 us thy cdepth) * (size_of_type T2 us thy cdepth)
1.1232 - | Type ("fun", [T1,T2]) => power (size_of_type T2 us thy cdepth, size_of_type T1 us thy cdepth)
1.1233 - | Type ("set", [T1]) => size_of_type (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
1.1234 - | Type (s, Ts) =>
1.1235 - (case DatatypePackage.datatype_info thy s of
1.1236 - Some info => (* inductive datatype *)
1.1237 - if cdepth>0 then
1.1238 + if is_var t andalso is_funtype (typeof t) then
1.1239 + (case assoc (intrs, t) of
1.1240 + Some intr => Some (intr, model, args)
1.1241 + | None =>
1.1242 + let
1.1243 + val T1 = domain_type (typeof t)
1.1244 + val T2 = range_type (typeof t)
1.1245 + (* we create 'size_of_interpretation (interpret (... T1))' different copies *)
1.1246 + (* of the tree for 'T2', which are then combined into a single new tree *)
1.1247 + val (i1, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (stringof t, T1))
1.1248 + (* power(a,b) computes a^b, for a>=0, b>=0 *)
1.1249 + (* int * int -> int *)
1.1250 + fun power (a,0) = 1
1.1251 + | power (a,1) = a
1.1252 + | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
1.1253 + fun size_of_interpretation (Leaf xs) = length xs
1.1254 + | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
1.1255 + val size = size_of_interpretation i1
1.1256 + (* make fresh copies, with different variable indices *)
1.1257 + (* int -> int -> (int * interpretation list *)
1.1258 + fun make_copies idx 0 =
1.1259 + (idx, [])
1.1260 + | make_copies idx n =
1.1261 + let
1.1262 + val (copy, _, args) = interpret thy (sizes, []) {next_idx = idx, bounds = [], wellformed=True} (Free (stringof t, T2))
1.1263 + val (next, copies) = make_copies (#next_idx args) (n-1)
1.1264 + in
1.1265 + (next, copy :: copies)
1.1266 + end
1.1267 + val (idx, copies) = make_copies (#next_idx args) (size_of_interpretation i1)
1.1268 + (* combine copies into a single tree *)
1.1269 + val intr = Node copies
1.1270 + in
1.1271 + (* extend the model, increase 'next_idx' *)
1.1272 + Some (intr, (sizes, (t, intr)::intrs), {next_idx = idx, bounds = #bounds args, wellformed = #wellformed args})
1.1273 + end)
1.1274 + else
1.1275 + None
1.1276 + end;
1.1277 +
1.1278 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1279 +
1.1280 + fun var_settype_interpreter thy model args t =
1.1281 + let
1.1282 + val (sizes, intrs) = model
1.1283 + in
1.1284 + case t of
1.1285 + Free (x, Type ("set", [T])) =>
1.1286 + (case assoc (intrs, t) of
1.1287 + Some intr => Some (intr, model, args)
1.1288 + | None =>
1.1289 + let
1.1290 + val (intr, _, args') = interpret thy model args (Free (x, Type ("fun", [T, Type ("bool", [])])))
1.1291 + in
1.1292 + Some (intr, (sizes, (t, intr)::intrs), args')
1.1293 + end)
1.1294 + | Var ((x,i), Type ("set", [T])) =>
1.1295 + (case assoc (intrs, t) of
1.1296 + Some intr => Some (intr, model, args)
1.1297 + | None =>
1.1298 + let
1.1299 + val (intr, _, args') = interpret thy model args (Var ((x,i), Type ("fun", [T, Type ("bool", [])])))
1.1300 + in
1.1301 + Some (intr, (sizes, (t, intr)::intrs), args')
1.1302 + end)
1.1303 + | _ => None
1.1304 + end;
1.1305 +
1.1306 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1307 +
1.1308 + fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds args), model, args)
1.1309 + | boundvar_interpreter thy model args _ = None;
1.1310 +
1.1311 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1312 +
1.1313 + fun abstraction_interpreter thy model args (Abs (x, T, t)) =
1.1314 + let
1.1315 + val (sizes, intrs) = model
1.1316 + (* create all constants of type T *)
1.1317 + val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (x, T))
1.1318 + (* returns a list with all unit vectors of length n *)
1.1319 + (* int -> interpretation list *)
1.1320 + fun unit_vectors n =
1.1321 + let
1.1322 + (* returns the k-th unit vector of length n *)
1.1323 + (* int * int -> interpretation *)
1.1324 + fun unit_vector (k,n) =
1.1325 + Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.1326 + (* int -> interpretation list -> interpretation list *)
1.1327 + fun unit_vectors_acc k vs =
1.1328 + if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
1.1329 + in
1.1330 + unit_vectors_acc 1 []
1.1331 + end
1.1332 + (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.1333 + (* 'a -> 'a list list -> 'a list list *)
1.1334 + fun cons_list x xss =
1.1335 + map (fn xs => x::xs) xss
1.1336 + (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
1.1337 + (* int -> 'a list -> 'a list list *)
1.1338 + fun pick_all 1 xs =
1.1339 + map (fn x => [x]) xs
1.1340 + | pick_all n xs =
1.1341 + let val rec_pick = pick_all (n-1) xs in
1.1342 + foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.1343 + end
1.1344 + (* interpretation -> interpretation list *)
1.1345 + fun make_constants (Leaf xs) =
1.1346 + unit_vectors (length xs)
1.1347 + | make_constants (Node xs) =
1.1348 + map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.1349 + (* interpret the body 't' separately for each constant *)
1.1350 + val ((model', args'), bodies) = foldl_map
1.1351 + (fn ((m,a), c) =>
1.1352 + let
1.1353 + (* add 'c' to 'bounds' *)
1.1354 + val (i',m',a') = interpret thy m {next_idx = #next_idx a, bounds = c::(#bounds a), wellformed = #wellformed a} t
1.1355 + in
1.1356 + (* keep the new model m' and 'next_idx', but use old 'bounds' *)
1.1357 + ((m',{next_idx = #next_idx a', bounds = #bounds a, wellformed = #wellformed a'}), i')
1.1358 + end)
1.1359 + ((model,args), make_constants i)
1.1360 + in
1.1361 + Some (Node bodies, model', args')
1.1362 + end
1.1363 + | abstraction_interpreter thy model args _ = None;
1.1364 +
1.1365 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1366 +
1.1367 + fun apply_interpreter thy model args (t1 $ t2) =
1.1368 + let
1.1369 + (* auxiliary functions *)
1.1370 + (* interpretation * interpretation -> interpretation *)
1.1371 + fun interpretation_disjunction (tr1,tr2) =
1.1372 + tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
1.1373 + (* prop_formula * interpretation -> interpretation *)
1.1374 + fun prop_formula_times_interpretation (fm,tr) =
1.1375 + tree_map (map (fn x => SAnd (fm,x))) tr
1.1376 + (* prop_formula list * interpretation list -> interpretation *)
1.1377 + fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
1.1378 + prop_formula_times_interpretation (fm,tr)
1.1379 + | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
1.1380 + interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees))
1.1381 + | prop_formula_list_dot_product_interpretation_list (_,_) =
1.1382 + raise REFUTE ("apply_interpreter", "empty list (in dot product)")
1.1383 + (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.1384 + (* 'a -> 'a list list -> 'a list list *)
1.1385 + fun cons_list x xss =
1.1386 + map (fn xs => x::xs) xss
1.1387 + (* returns a list of lists, each one consisting of one element from each element of 'xss' *)
1.1388 + (* 'a list list -> 'a list list *)
1.1389 + fun pick_all [xs] =
1.1390 + map (fn x => [x]) xs
1.1391 + | pick_all (xs::xss) =
1.1392 + let val rec_pick = pick_all xss in
1.1393 + foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.1394 + end
1.1395 + | pick_all _ =
1.1396 + raise REFUTE ("apply_interpreter", "empty list (in pick_all)")
1.1397 + (* interpretation -> prop_formula list *)
1.1398 + fun interpretation_to_prop_formula_list (Leaf xs) =
1.1399 + xs
1.1400 + | interpretation_to_prop_formula_list (Node trees) =
1.1401 + map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees))
1.1402 + (* interpretation * interpretation -> interpretation *)
1.1403 + fun interpretation_apply (tr1,tr2) =
1.1404 + (case tr1 of
1.1405 + Leaf _ =>
1.1406 + raise REFUTE ("apply_interpreter", "first interpretation is a leaf")
1.1407 + | Node xs =>
1.1408 + prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list tr2, xs))
1.1409 + (* interpret 't1' and 't2' *)
1.1410 + val (intr1, model1, args1) = interpret thy model args t1
1.1411 + val (intr2, model2, args2) = interpret thy model1 args1 t2
1.1412 + in
1.1413 + Some (interpretation_apply (intr1,intr2), model2, args2)
1.1414 + end
1.1415 + | apply_interpreter thy model args _ = None;
1.1416 +
1.1417 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1418 +
1.1419 + fun const_unfold_interpreter thy model args t =
1.1420 + (* ------------------------------------------------------------------------- *)
1.1421 + (* We unfold constants for which a defining equation is given as an axiom. *)
1.1422 + (* A polymorphic axiom's type variables are instantiated. Eta-expansion is *)
1.1423 + (* performed only if necessary; arguments in the axiom that are present as *)
1.1424 + (* actual arguments in 't' are simply substituted. If more actual than *)
1.1425 + (* formal arguments are present, the constant is *not* unfolded, so that *)
1.1426 + (* other interpreters (that may just not have looked into the term far *)
1.1427 + (* enough yet) may be applied first (after 'apply_interpreter' gets rid of *)
1.1428 + (* one argument). *)
1.1429 + (* ------------------------------------------------------------------------- *)
1.1430 + let
1.1431 + val (head, actuals) = strip_comb t
1.1432 + val actuals_count = length actuals
1.1433 + in
1.1434 + case head of
1.1435 + Const (s,T) =>
1.1436 + let
1.1437 + (* (string * Term.term) list *)
1.1438 + val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
1.1439 + (* Term.term * Term.term list * Term.term list -> Term.term *)
1.1440 + (* term, formal arguments, actual arguments *)
1.1441 + fun normalize (t, [], []) = t
1.1442 + | normalize (t, [], y::ys) = raise REFUTE ("const_unfold_interpreter", "more actual than formal parameters")
1.1443 + | normalize (t, x::xs, []) = normalize (lambda x t, xs, []) (* eta-expansion *)
1.1444 + | normalize (t, x::xs, y::ys) = normalize (betapply (lambda x t, y), xs, ys) (* substitution *)
1.1445 + (* string -> Term.typ -> (string * Term.term) list -> Term.term option *)
1.1446 + fun get_defn s T [] =
1.1447 + None
1.1448 + | get_defn s T ((_,ax)::axms) =
1.1449 + (let
1.1450 + val (lhs, rhs) = Logic.dest_equals ax (* equations only *)
1.1451 + val (c, formals) = strip_comb lhs
1.1452 + val (s', T') = dest_Const c
1.1453 + in
1.1454 + if (s=s') andalso (actuals_count <= length formals) then
1.1455 + let
1.1456 + val varT' = Type.varifyT T' (* for polymorphic definitions *)
1.1457 + val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (varT', T))
1.1458 + val varRhs = map_term_types Type.varifyT rhs
1.1459 + val varFormals = map (map_term_types Type.varifyT) formals
1.1460 + val rhs' = normalize (varRhs, varFormals, actuals)
1.1461 + val unvarRhs = map_term_types
1.1462 + (map_type_tvar
1.1463 + (fn (v,_) =>
1.1464 + case Vartab.lookup (typeSubs, v) of
1.1465 + None =>
1.1466 + raise REFUTE ("const_unfold_interpreter", "schematic type variable " ^ (fst v) ^ "not instantiated (in definition of " ^ quote s ^ ")")
1.1467 + | Some typ =>
1.1468 + typ))
1.1469 + rhs'
1.1470 + in
1.1471 + Some unvarRhs
1.1472 + end
1.1473 + else
1.1474 + get_defn s T axms
1.1475 + end
1.1476 + handle TERM _ => get_defn s T axms
1.1477 + | Type.TYPE_MATCH => get_defn s T axms)
1.1478 + in
1.1479 + case get_defn s T axioms of
1.1480 + Some t' => Some (interpret thy model args t')
1.1481 + | None => None
1.1482 + end
1.1483 + | _ => None
1.1484 + end;
1.1485 +
1.1486 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1487 +
1.1488 + fun Pure_interpreter thy model args t =
1.1489 + let
1.1490 + fun toTrue (Leaf [fm,_]) = fm
1.1491 + | toTrue _ = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value")
1.1492 + fun toFalse (Leaf [_,fm]) = fm
1.1493 + | toFalse _ = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value")
1.1494 + in
1.1495 + case t of
1.1496 + (*Const ("Goal", _) $ t1 =>
1.1497 + Some (interpret thy model args t1) |*)
1.1498 + Const ("all", _) $ t1 =>
1.1499 + let
1.1500 + val (i,m,a) = (interpret thy model args t1)
1.1501 + in
1.1502 + case i of
1.1503 + Node xs =>
1.1504 + let
1.1505 + val fmTrue = PropLogic.all (map toTrue xs)
1.1506 + val fmFalse = PropLogic.exists (map toFalse xs)
1.1507 + in
1.1508 + Some (Leaf [fmTrue, fmFalse], m, a)
1.1509 + end
1.1510 + | _ =>
1.1511 + raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function")
1.1512 + end
1.1513 + | Const ("==", _) $ t1 $ t2 =>
1.1514 + let
1.1515 + val (i1,m1,a1) = interpret thy model args t1
1.1516 + val (i2,m2,a2) = interpret thy m1 a1 t2
1.1517 + (* interpretation * interpretation -> prop_formula *)
1.1518 + fun interpret_equal (tr1,tr2) =
1.1519 + (case tr1 of
1.1520 + Leaf x =>
1.1521 + (case tr2 of
1.1522 + Leaf y => PropLogic.dot_product (x,y)
1.1523 + | _ => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher"))
1.1524 + | Node xs =>
1.1525 + (case tr2 of
1.1526 + Leaf _ => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher")
1.1527 + (* extensionality: two functions are equal iff they are equal for every element *)
1.1528 + | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
1.1529 + (* interpretation * interpretation -> prop_formula *)
1.1530 + fun interpret_unequal (tr1,tr2) =
1.1531 + (case tr1 of
1.1532 + Leaf x =>
1.1533 + (case tr2 of
1.1534 + Leaf y =>
1.1535 + let
1.1536 + fun unequal [] ([],_) =
1.1537 + False
1.1538 + | unequal (x::xs) (y::ys1, ys2) =
1.1539 + SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2))
1.1540 + | unequal _ _ =
1.1541 + raise REFUTE ("Pure_interpreter", "\"==\": leafs have different width")
1.1542 + in
1.1543 + unequal x (y,[])
1.1544 + end
1.1545 + | _ => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher"))
1.1546 + | Node xs =>
1.1547 + (case tr2 of
1.1548 + Leaf _ => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher")
1.1549 + (* extensionality: two functions are unequal iff there exist unequal elements *)
1.1550 + | Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys))))
1.1551 + val fmTrue = interpret_equal (i1,i2)
1.1552 + val fmFalse = interpret_unequal (i1,i2)
1.1553 + in
1.1554 + Some (Leaf [fmTrue, fmFalse], m2, a2)
1.1555 + end
1.1556 + | Const ("==>", _) $ t1 $ t2 =>
1.1557 + let
1.1558 + val (i1,m1,a1) = interpret thy model args t1
1.1559 + val (i2,m2,a2) = interpret thy m1 a1 t2
1.1560 + val fmTrue = SOr (toFalse i1, toTrue i2)
1.1561 + val fmFalse = SAnd (toTrue i1, toFalse i2)
1.1562 + in
1.1563 + Some (Leaf [fmTrue, fmFalse], m2, a2)
1.1564 + end
1.1565 + | _ => None
1.1566 + end;
1.1567 +
1.1568 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1569 +
1.1570 + fun HOLogic_interpreter thy model args t =
1.1571 + (* ------------------------------------------------------------------------- *)
1.1572 + (* Providing interpretations directly is more efficient than unfolding the *)
1.1573 + (* logical constants; however, we need versions for constants with arguments *)
1.1574 + (* (to avoid unfolding) as well as versions for constants without arguments *)
1.1575 + (* (since in HOL, logical constants can themselves be arguments) *)
1.1576 + (* ------------------------------------------------------------------------- *)
1.1577 + let
1.1578 + fun eta_expand t i =
1.1579 + let
1.1580 + val Ts = binder_types (fastype_of t)
1.1581 + in
1.1582 + foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
1.1583 + (take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
1.1584 + end
1.1585 + val TT = Leaf [True, False]
1.1586 + val FF = Leaf [False, True]
1.1587 + fun toTrue (Leaf [fm,_]) = fm
1.1588 + | toTrue _ = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value")
1.1589 + fun toFalse (Leaf [_,fm]) = fm
1.1590 + | toFalse _ = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value")
1.1591 + in
1.1592 + case t of
1.1593 + Const ("Trueprop", _) $ t1 =>
1.1594 + Some (interpret thy model args t1)
1.1595 + | Const ("Trueprop", _) =>
1.1596 + Some (Node [TT, FF], model, args)
1.1597 + | Const ("Not", _) $ t1 =>
1.1598 + apply_interpreter thy model args t
1.1599 + | Const ("Not", _) =>
1.1600 + Some (Node [FF, TT], model, args)
1.1601 + | Const ("True", _) =>
1.1602 + Some (TT, model, args)
1.1603 + | Const ("False", _) =>
1.1604 + Some (FF, model, args)
1.1605 + | Const ("arbitrary", T) =>
1.1606 + (* treat 'arbitrary' just like a free variable of the same type *)
1.1607 + (case assoc (snd model, t) of
1.1608 + Some intr =>
1.1609 + Some (intr, model, args)
1.1610 + | None =>
1.1611 + let
1.1612 + val (sizes, intrs) = model
1.1613 + val (intr, _, a) = interpret thy (sizes, []) args (Free ("<arbitrary>", T))
1.1614 + in
1.1615 + Some (intr, (sizes, (t,intr)::intrs), a)
1.1616 + end)
1.1617 + | Const ("The", _) $ t1 =>
1.1618 + apply_interpreter thy model args t
1.1619 + | Const ("The", T as Type ("fun", [_, T'])) =>
1.1620 + (* treat 'The' like a free variable, but with a fixed interpretation for boolean *)
1.1621 + (* functions that map exactly one constant of type T' to True *)
1.1622 + (case assoc (snd model, t) of
1.1623 + Some intr =>
1.1624 + Some (intr, model, args)
1.1625 + | None =>
1.1626 + let
1.1627 + val (sizes, intrs) = model
1.1628 + val (intr, _, a) = interpret thy (sizes, []) args (Free ("<The>", T))
1.1629 + (* create all constants of type T' => bool, ... *)
1.1630 + val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<The>", Type ("fun", [T', Type ("bool",[])])))
1.1631 + (* ... and all constants of type T' *)
1.1632 + val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<The>", T'))
1.1633 + (* returns a list with all unit vectors of length n *)
1.1634 + (* int -> interpretation list *)
1.1635 + fun unit_vectors n =
1.1636 + let
1.1637 + (* returns the k-th unit vector of length n *)
1.1638 + (* int * int -> interpretation *)
1.1639 + fun unit_vector (k,n) =
1.1640 + Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.1641 + (* int -> interpretation list -> interpretation list *)
1.1642 + fun unit_vectors_acc k vs =
1.1643 + if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
1.1644 + in
1.1645 + unit_vectors_acc 1 []
1.1646 + end
1.1647 + (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.1648 + (* 'a -> 'a list list -> 'a list list *)
1.1649 + fun cons_list x xss =
1.1650 + map (fn xs => x::xs) xss
1.1651 + (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
1.1652 + (* int -> 'a list -> 'a list list *)
1.1653 + fun pick_all 1 xs =
1.1654 + map (fn x => [x]) xs
1.1655 + | pick_all n xs =
1.1656 + let val rec_pick = pick_all (n-1) xs in
1.1657 + foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.1658 + end
1.1659 + (* interpretation -> interpretation list *)
1.1660 + fun make_constants (Leaf xs) =
1.1661 + unit_vectors (length xs)
1.1662 + | make_constants (Node xs) =
1.1663 + map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.1664 + val constantsFun = make_constants intrFun
1.1665 + val constantsT' = make_constants intrT'
1.1666 + (* interpretation -> interpretation list -> interpretation option *)
1.1667 + fun the_val (Node xs) cs =
1.1668 + let
1.1669 + val TrueCount = foldl (fn (n,x) => if toTrue x = True then n+1 else n) (0,xs)
1.1670 + fun findThe (x::xs) (c::cs) =
1.1671 + if toTrue x = True then
1.1672 + c
1.1673 + else
1.1674 + findThe xs cs
1.1675 + | findThe _ _ =
1.1676 + raise REFUTE ("HOLogic_interpreter", "\"The\": not found")
1.1677 + in
1.1678 + if TrueCount=1 then
1.1679 + Some (findThe xs cs)
1.1680 + else
1.1681 + None
1.1682 + end
1.1683 + | the_val _ _ =
1.1684 + raise REFUTE ("HOLogic_interpreter", "\"The\": function interpreted as a leaf")
1.1685 + in
1.1686 + case intr of
1.1687 + Node xs =>
1.1688 + let
1.1689 + (* replace interpretation 'x' by the interpretation determined by 'f' *)
1.1690 + val intrThe = Node (map (fn (x,f) => if_none (the_val f constantsT') x) (xs ~~ constantsFun))
1.1691 + in
1.1692 + Some (intrThe, (sizes, (t,intrThe)::intrs), a)
1.1693 + end
1.1694 + | _ =>
1.1695 + raise REFUTE ("HOLogic_interpreter", "\"The\": interpretation is a leaf")
1.1696 + end)
1.1697 + | Const ("Hilbert_Choice.Eps", _) $ t1 =>
1.1698 + apply_interpreter thy model args t
1.1699 + | Const ("Hilbert_Choice.Eps", T as Type ("fun", [_, T'])) =>
1.1700 + (* treat 'The' like a free variable, but with a fixed interpretation for boolean *)
1.1701 + (* functions that map exactly one constant of type T' to True *)
1.1702 + (case assoc (snd model, t) of
1.1703 + Some intr =>
1.1704 + Some (intr, model, args)
1.1705 + | None =>
1.1706 + let
1.1707 + val (sizes, intrs) = model
1.1708 + val (intr, _, a) = interpret thy (sizes, []) args (Free ("<Eps>", T))
1.1709 + (* create all constants of type T' => bool, ... *)
1.1710 + val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<Eps>", Type ("fun", [T', Type ("bool",[])])))
1.1711 + (* ... and all constants of type T' *)
1.1712 + val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<Eps>", T'))
1.1713 + (* returns a list with all unit vectors of length n *)
1.1714 + (* int -> interpretation list *)
1.1715 + fun unit_vectors n =
1.1716 + let
1.1717 + (* returns the k-th unit vector of length n *)
1.1718 + (* int * int -> interpretation *)
1.1719 + fun unit_vector (k,n) =
1.1720 + Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.1721 + (* int -> interpretation list -> interpretation list *)
1.1722 + fun unit_vectors_acc k vs =
1.1723 + if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
1.1724 + in
1.1725 + unit_vectors_acc 1 []
1.1726 + end
1.1727 + (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.1728 + (* 'a -> 'a list list -> 'a list list *)
1.1729 + fun cons_list x xss =
1.1730 + map (fn xs => x::xs) xss
1.1731 + (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
1.1732 + (* int -> 'a list -> 'a list list *)
1.1733 + fun pick_all 1 xs =
1.1734 + map (fn x => [x]) xs
1.1735 + | pick_all n xs =
1.1736 + let val rec_pick = pick_all (n-1) xs in
1.1737 + foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.1738 + end
1.1739 + (* interpretation -> interpretation list *)
1.1740 + fun make_constants (Leaf xs) =
1.1741 + unit_vectors (length xs)
1.1742 + | make_constants (Node xs) =
1.1743 + map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.1744 + val constantsFun = make_constants intrFun
1.1745 + val constantsT' = make_constants intrT'
1.1746 + (* interpretation -> interpretation list -> interpretation list *)
1.1747 + fun true_values (Node xs) cs =
1.1748 + mapfilter (fn (x,c) => if toTrue x = True then Some c else None) (xs~~cs)
1.1749 + | true_values _ _ =
1.1750 + raise REFUTE ("HOLogic_interpreter", "\"Eps\": function interpreted as a leaf")
1.1751 + in
1.1752 + case intr of
1.1753 + Node xs =>
1.1754 + let
1.1755 + val (wf, intrsEps) = foldl_map (fn (w,(x,f)) =>
1.1756 + case true_values f constantsT' of
1.1757 + [] => (w, x) (* no value mapped to true -> no restriction *)
1.1758 + | [c] => (w, c) (* one value mapped to true -> that's the one *)
1.1759 + | cs =>
1.1760 + let
1.1761 + (* interpretation * interpretation -> prop_formula *)
1.1762 + fun interpret_equal (tr1,tr2) =
1.1763 + (case tr1 of
1.1764 + Leaf x =>
1.1765 + (case tr2 of
1.1766 + Leaf y => PropLogic.dot_product (x,y)
1.1767 + | _ => raise REFUTE ("HOLogic_interpreter", "\"Eps\": second tree is higher"))
1.1768 + | Node xs =>
1.1769 + (case tr2 of
1.1770 + Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"Eps\": first tree is higher")
1.1771 + (* extensionality: two functions are equal iff they are equal for every element *)
1.1772 + | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
1.1773 + in
1.1774 + (SAnd (w, PropLogic.exists (map (fn c => interpret_equal (x,c)) cs)), x) (* impose restrictions on x *)
1.1775 + end
1.1776 + )
1.1777 + (#wellformed a, xs ~~ constantsFun)
1.1778 + val intrEps = Node intrsEps
1.1779 + in
1.1780 + Some (intrEps, (sizes, (t,intrEps)::intrs), {next_idx = #next_idx a, bounds = #bounds a, wellformed = wf})
1.1781 + end
1.1782 + | _ =>
1.1783 + raise REFUTE ("HOLogic_interpreter", "\"Eps\": interpretation is a leaf")
1.1784 + end)
1.1785 + | Const ("All", _) $ t1 =>
1.1786 + let
1.1787 + val (i,m,a) = interpret thy model args t1
1.1788 + in
1.1789 + case i of
1.1790 + Node xs =>
1.1791 + let
1.1792 + val fmTrue = PropLogic.all (map toTrue xs)
1.1793 + val fmFalse = PropLogic.exists (map toFalse xs)
1.1794 + in
1.1795 + Some (Leaf [fmTrue, fmFalse], m, a)
1.1796 + end
1.1797 + | _ =>
1.1798 + raise REFUTE ("HOLogic_interpreter", "\"All\" is not followed by a function")
1.1799 + end
1.1800 + | Const ("All", _) =>
1.1801 + Some (interpret thy model args (eta_expand t 1))
1.1802 + | Const ("Ex", _) $ t1 =>
1.1803 + let
1.1804 + val (i,m,a) = interpret thy model args t1
1.1805 + in
1.1806 + case i of
1.1807 + Node xs =>
1.1808 + let
1.1809 + val fmTrue = PropLogic.exists (map toTrue xs)
1.1810 + val fmFalse = PropLogic.all (map toFalse xs)
1.1811 + in
1.1812 + Some (Leaf [fmTrue, fmFalse], m, a)
1.1813 + end
1.1814 + | _ =>
1.1815 + raise REFUTE ("HOLogic_interpreter", "\"Ex\" is not followed by a function")
1.1816 + end
1.1817 + | Const ("Ex", _) =>
1.1818 + Some (interpret thy model args (eta_expand t 1))
1.1819 + | Const ("Ex1", _) $ t1 =>
1.1820 + let
1.1821 + val (i,m,a) = interpret thy model args t1
1.1822 + in
1.1823 + case i of
1.1824 + Node xs =>
1.1825 + let
1.1826 + (* interpretation list -> prop_formula *)
1.1827 + fun allfalse [] = True
1.1828 + | allfalse (x::xs) = SAnd (toFalse x, allfalse xs)
1.1829 + (* interpretation list -> prop_formula *)
1.1830 + fun exactly1true [] = False
1.1831 + | exactly1true (x::xs) = SOr (SAnd (toTrue x, allfalse xs), SAnd (toFalse x, exactly1true xs))
1.1832 + (* interpretation list -> prop_formula *)
1.1833 + fun atleast2true [] = False
1.1834 + | atleast2true (x::xs) = SOr (SAnd (toTrue x, PropLogic.exists (map toTrue xs)), atleast2true xs)
1.1835 + val fmTrue = exactly1true xs
1.1836 + val fmFalse = SOr (allfalse xs, atleast2true xs)
1.1837 + in
1.1838 + Some (Leaf [fmTrue, fmFalse], m, a)
1.1839 + end
1.1840 + | _ =>
1.1841 + raise REFUTE ("HOLogic_interpreter", "\"Ex1\" is not followed by a function")
1.1842 + end
1.1843 + | Const ("Ex1", _) =>
1.1844 + Some (interpret thy model args (eta_expand t 1))
1.1845 + | Const ("op =", _) $ t1 $ t2 =>
1.1846 + let
1.1847 + val (i1,m1,a1) = interpret thy model args t1
1.1848 + val (i2,m2,a2) = interpret thy m1 a1 t2
1.1849 + (* interpretation * interpretation -> prop_formula *)
1.1850 + fun interpret_equal (tr1,tr2) =
1.1851 + (case tr1 of
1.1852 + Leaf x =>
1.1853 + (case tr2 of
1.1854 + Leaf y => PropLogic.dot_product (x,y)
1.1855 + | _ => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher"))
1.1856 + | Node xs =>
1.1857 + (case tr2 of
1.1858 + Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher")
1.1859 + (* extensionality: two functions are equal iff they are equal for every element *)
1.1860 + | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
1.1861 + (* interpretation * interpretation -> prop_formula *)
1.1862 + fun interpret_unequal (tr1,tr2) =
1.1863 + (case tr1 of
1.1864 + Leaf x =>
1.1865 + (case tr2 of
1.1866 + Leaf y =>
1.1867 + let
1.1868 + fun unequal [] ([],_) =
1.1869 + False
1.1870 + | unequal (x::xs) (y::ys1, ys2) =
1.1871 + SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2))
1.1872 + | unequal _ _ =
1.1873 + raise REFUTE ("HOLogic_interpreter", "\"==\": leafs have different width")
1.1874 + in
1.1875 + unequal x (y,[])
1.1876 + end
1.1877 + | _ => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher"))
1.1878 + | Node xs =>
1.1879 + (case tr2 of
1.1880 + Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher")
1.1881 + (* extensionality: two functions are unequal iff there exist unequal elements *)
1.1882 + | Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys))))
1.1883 + val fmTrue = interpret_equal (i1,i2)
1.1884 + val fmFalse = interpret_unequal (i1,i2)
1.1885 + in
1.1886 + Some (Leaf [fmTrue, fmFalse], m2, a2)
1.1887 + end
1.1888 + | Const ("op =", _) $ t1 =>
1.1889 + Some (interpret thy model args (eta_expand t 1))
1.1890 + | Const ("op =", _) =>
1.1891 + Some (interpret thy model args (eta_expand t 2))
1.1892 + | Const ("op &", _) $ t1 $ t2 =>
1.1893 + apply_interpreter thy model args t
1.1894 + | Const ("op &", _) $ t1 =>
1.1895 + apply_interpreter thy model args t
1.1896 + | Const ("op &", _) =>
1.1897 + Some (Node [Node [TT, FF], Node [FF, FF]], model, args)
1.1898 + | Const ("op |", _) $ t1 $ t2 =>
1.1899 + apply_interpreter thy model args t
1.1900 + | Const ("op |", _) $ t1 =>
1.1901 + apply_interpreter thy model args t
1.1902 + | Const ("op |", _) =>
1.1903 + Some (Node [Node [TT, TT], Node [TT, FF]], model, args)
1.1904 + | Const ("op -->", _) $ t1 $ t2 =>
1.1905 + apply_interpreter thy model args t
1.1906 + | Const ("op -->", _) $ t1 =>
1.1907 + apply_interpreter thy model args t
1.1908 + | Const ("op -->", _) =>
1.1909 + Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
1.1910 + | Const ("Collect", _) $ t1 =>
1.1911 + (* Collect == identity *)
1.1912 + Some (interpret thy model args t1)
1.1913 + | Const ("Collect", _) =>
1.1914 + Some (interpret thy model args (eta_expand t 1))
1.1915 + | Const ("op :", _) $ t1 $ t2 =>
1.1916 + (* op: == application *)
1.1917 + Some (interpret thy model args (t2 $ t1))
1.1918 + | Const ("op :", _) $ t1 =>
1.1919 + Some (interpret thy model args (eta_expand t 1))
1.1920 + | Const ("op :", _) =>
1.1921 + Some (interpret thy model args (eta_expand t 2))
1.1922 + | _ => None
1.1923 + end;
1.1924 +
1.1925 + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
1.1926 +
1.1927 + fun IDT_interpreter thy model args t =
1.1928 + let
1.1929 + fun is_var (Free _) = true
1.1930 + | is_var (Var _) = true
1.1931 + | is_var _ = false
1.1932 + fun typeof (Free (_,T)) = T
1.1933 + | typeof (Var (_,T)) = T
1.1934 + | typeof _ = raise REFUTE ("var_IDT_interpreter", "term is not a variable")
1.1935 + val (sizes, intrs) = model
1.1936 + (* power(a,b) computes a^b, for a>=0, b>=0 *)
1.1937 + (* int * int -> int *)
1.1938 + fun power (a,0) = 1
1.1939 + | power (a,1) = a
1.1940 + | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
1.1941 + (* interpretation -> int *)
1.1942 + fun size_of_interpretation (Leaf xs) = length xs
1.1943 + | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
1.1944 + (* Term.typ -> int *)
1.1945 + fun size_of_type T =
1.1946 + let
1.1947 + val (i,_,_) = interpret thy model args (Free ("<IDT>", T))
1.1948 + in
1.1949 + size_of_interpretation i
1.1950 + end
1.1951 + (* int list -> int *)
1.1952 + fun sum xs = foldl op+ (0, xs)
1.1953 + (* int list -> int *)
1.1954 + fun product xs = foldl op* (1, xs)
1.1955 + (* DatatypeAux.dtyp * Term.typ -> DatatypeAux.dtyp -> Term.typ *)
1.1956 + fun typ_of_dtyp typ_assoc (DatatypeAux.DtTFree a) =
1.1957 + the (assoc (typ_assoc, DatatypeAux.DtTFree a))
1.1958 + | typ_of_dtyp typ_assoc (DatatypeAux.DtRec i) =
1.1959 + raise REFUTE ("var_IDT_interpreter", "recursive datatype")
1.1960 + | typ_of_dtyp typ_assoc (DatatypeAux.DtType (s, ds)) =
1.1961 + Type (s, map (typ_of_dtyp typ_assoc) ds)
1.1962 + in
1.1963 + if is_var t then
1.1964 + (case typeof t of
1.1965 + Type (s, Ts) =>
1.1966 + (case DatatypePackage.datatype_info thy s of
1.1967 + Some info => (* inductive datatype *)
1.1968 let
1.1969 val index = #index info
1.1970 val descr = #descr info
1.1971 val (_, dtyps, constrs) = the (assoc (descr, index))
1.1972 - val Typs = dtyps ~~ Ts
1.1973 - (* DatatypeAux.dtyp -> Term.typ *)
1.1974 - fun typ_of_dtyp (DatatypeAux.DtTFree a) =
1.1975 - the (assoc (Typs, DatatypeAux.DtTFree a))
1.1976 - | typ_of_dtyp (DatatypeAux.DtRec i) =
1.1977 - let
1.1978 - val (s, ds, _) = the (assoc (descr, i))
1.1979 - in
1.1980 - Type (s, map typ_of_dtyp ds)
1.1981 - end
1.1982 - | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
1.1983 - Type (s, map typ_of_dtyp ds)
1.1984 in
1.1985 - sum (map (fn (_,ds) => product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)) constrs)
1.1986 + if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
1.1987 + raise REFUTE ("var_IDT_interpreter", "recursive datatype argument")
1.1988 + else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
1.1989 + None (* recursive datatype (requires an infinite model) *)
1.1990 + else
1.1991 + case assoc (intrs, t) of
1.1992 + Some intr => Some (intr, model, args)
1.1993 + | None =>
1.1994 + let
1.1995 + val typ_assoc = dtyps ~~ Ts
1.1996 + val size = sum (map (fn (_,ds) =>
1.1997 + product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) constrs)
1.1998 + val idx = #next_idx args
1.1999 + (* for us, an IDT has no "internal structure" -- its interpretation is just a leaf *)
1.2000 + val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1))))
1.2001 + val next = (if size=2 then idx+1 else idx+size)
1.2002 + in
1.2003 + (* extend the model, increase 'next_idx' *)
1.2004 + Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args})
1.2005 + end
1.2006 end
1.2007 - else 0
1.2008 - | None => error ("size_of_type: type contains an unknown type constructor: '" ^ s ^ "'"))
1.2009 - | TFree _ => lookup_size T us
1.2010 - | TVar _ => lookup_size T us
1.2011 + | None => None)
1.2012 + | _ => None)
1.2013 + else
1.2014 + let
1.2015 + val (head, params) = strip_comb t (* look into applications to avoid unfolding *)
1.2016 + in
1.2017 + (case head of
1.2018 + Const (c, T) =>
1.2019 + (case body_type T of
1.2020 + Type (s, Ts) =>
1.2021 + (case DatatypePackage.datatype_info thy s of
1.2022 + Some info => (* inductive datatype *)
1.2023 + let
1.2024 + val index = #index info
1.2025 + val descr = #descr info
1.2026 + val (_, dtyps, constrs) = the (assoc (descr, index))
1.2027 + in
1.2028 + if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
1.2029 + raise REFUTE ("var_IDT_interpreter", "recursive datatype argument")
1.2030 + else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
1.2031 + None (* recursive datatype (requires an infinite model) *)
1.2032 + else
1.2033 + (case take_prefix (fn (c',_) => c' <> c) constrs of
1.2034 + (_, []) =>
1.2035 + None (* unknown constructor *)
1.2036 + | (prevs, _) =>
1.2037 + if null params then
1.2038 + let
1.2039 + val typ_assoc = dtyps ~~ Ts
1.2040 + val offset = sum (map (fn (_,ds) =>
1.2041 + product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) prevs)
1.2042 + val (i,_,_) = interpret thy model args (Free ("<IDT>", T))
1.2043 + (* int * interpretation -> int * interpretation *)
1.2044 + fun replace (offset, Leaf xs) =
1.2045 + (* replace the offset-th element by True, all others by False, inc. offset by 1 *)
1.2046 + (offset+1, Leaf (snd (foldl_map (fn (n,_) => (n+1, if n=offset then True else False)) (0, xs))))
1.2047 + | replace (offset, Node xs) =
1.2048 + let
1.2049 + val (offset', xs') = foldl_map replace (offset, xs)
1.2050 + in
1.2051 + (offset', Node xs')
1.2052 + end
1.2053 + val (_,intr) = replace (offset, i)
1.2054 + in
1.2055 + Some (intr, model, args)
1.2056 + end
1.2057 + else
1.2058 + apply_interpreter thy model args t) (* avoid unfolding by calling 'apply_interpreter' directly *)
1.2059 + end
1.2060 + | None => None)
1.2061 + | _ => None)
1.2062 + | _ => None)
1.2063 + end
1.2064 end;
1.2065
1.2066 +
1.2067 (* ------------------------------------------------------------------------- *)
1.2068 -(* type_to_prop_tree: creates a tree of boolean variables that denotes an *)
1.2069 -(* element of the type 'T'. The height and branching factor of the *)
1.2070 -(* tree depend on the size and "structure" of 'T'. *)
1.2071 -(* 'us' : a "universe" specifying the number of elements for each basic type *)
1.2072 -(* (i.e. each type variable) in 'T' *)
1.2073 -(* 'cdepth': maximum constructor depth to be used for inductive datatypes *)
1.2074 -(* 'idx': the next index to be used for a boolean variable *)
1.2075 +(* PRINTERS *)
1.2076 (* ------------------------------------------------------------------------- *)
1.2077
1.2078 - (* Term.typ -> (Term.typ * int) list -> theory -> int -> int -> prop_tree * int *)
1.2079 + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
1.2080
1.2081 - fun type_to_prop_tree T us thy cdepth idx =
1.2082 + fun var_typevar_printer thy model t intr assignment =
1.2083 let
1.2084 - (* int -> Term.typ -> int -> prop_tree list * int *)
1.2085 - fun type_to_prop_tree_list 1 T' idx' =
1.2086 - let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
1.2087 - ([tr], newidx)
1.2088 - end
1.2089 - | type_to_prop_tree_list n T' idx' =
1.2090 - let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
1.2091 - let val (trees, lastidx) = type_to_prop_tree_list (n-1) T' newidx in
1.2092 - (tr::trees, lastidx)
1.2093 - end
1.2094 - end
1.2095 + fun is_var (Free _) = true
1.2096 + | is_var (Var _) = true
1.2097 + | is_var _ = false
1.2098 + fun typeof (Free (_,T)) = T
1.2099 + | typeof (Var (_,T)) = T
1.2100 + | typeof _ = raise REFUTE ("var_typevar_printer", "term is not a variable")
1.2101 + fun is_typevar (TFree _) = true
1.2102 + | is_typevar (TVar _) = true
1.2103 + | is_typevar _ = false
1.2104 in
1.2105 - case T of
1.2106 - Type ("prop", []) =>
1.2107 - (Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
1.2108 - | Type ("bool", []) =>
1.2109 - (Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
1.2110 - | Type ("Product_Type.unit", []) =>
1.2111 - (Leaf [True], idx)
1.2112 - | Type ("+", [T1,T2]) =>
1.2113 + if is_var t andalso is_typevar (typeof t) then
1.2114 let
1.2115 - val s1 = size_of_type T1 us thy cdepth
1.2116 - val s2 = size_of_type T2 us thy cdepth
1.2117 - val s = s1 + s2
1.2118 - in
1.2119 - if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
1.2120 - raise EMPTY_DATATYPE
1.2121 - else
1.2122 - error "sum types (+) not implemented yet (TODO)"
1.2123 - end
1.2124 - | Type ("*", [T1,T2]) =>
1.2125 - let
1.2126 - val s1 = size_of_type T1 us thy cdepth
1.2127 - val s2 = size_of_type T2 us thy cdepth
1.2128 - val s = s1 * s2
1.2129 + (* interpretation -> int *)
1.2130 + fun index_from_interpretation (Leaf xs) =
1.2131 + let
1.2132 + val idx = find_index (PropLogic.eval assignment) xs
1.2133 + in
1.2134 + if idx<0 then
1.2135 + raise REFUTE ("var_typevar_printer", "illegal interpretation: no value assigned")
1.2136 + else
1.2137 + idx
1.2138 + end
1.2139 + | index_from_interpretation _ =
1.2140 + raise REFUTE ("var_typevar_printer", "interpretation is not a leaf")
1.2141 + (* string -> string *)
1.2142 + fun strip_leading_quote s =
1.2143 + (implode o (fn (x::xs) => if x="'" then xs else (x::xs)) o explode) s
1.2144 + (* Term.typ -> string *)
1.2145 + fun string_of_typ (TFree (x,_)) = strip_leading_quote x
1.2146 + | string_of_typ (TVar ((x,i),_)) = strip_leading_quote x ^ string_of_int i
1.2147 + | string_of_typ _ = raise REFUTE ("var_typevar_printer", "type is not a type variable")
1.2148 in
1.2149 - if s1=0 orelse s2=0 then
1.2150 - raise EMPTY_DATATYPE
1.2151 - else
1.2152 - error "product types (*) not implemented yet (TODO)"
1.2153 - end
1.2154 - | Type ("fun", [T1,T2]) =>
1.2155 - (* we create 'size_of_type T1' different copies of the tree for 'T2', *)
1.2156 - (* which are then combined into a single new tree *)
1.2157 - let
1.2158 - val s = size_of_type T1 us thy cdepth
1.2159 - in
1.2160 - if s=0 then
1.2161 - raise EMPTY_DATATYPE
1.2162 - else
1.2163 - let val (trees, newidx) = type_to_prop_tree_list s T2 idx in
1.2164 - (Node trees, newidx)
1.2165 - end
1.2166 + Some (string_of_typ (typeof t) ^ string_of_int (index_from_interpretation intr))
1.2167 end
1.2168 - | Type ("set", [T1]) =>
1.2169 - type_to_prop_tree (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth idx
1.2170 - | Type (s, _) =>
1.2171 - (case DatatypePackage.constrs_of thy s of
1.2172 - Some _ => (* inductive datatype *)
1.2173 - let
1.2174 - val s = size_of_type T us thy cdepth
1.2175 - in
1.2176 - if s=0 then
1.2177 - raise EMPTY_DATATYPE
1.2178 - else
1.2179 - (Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
1.2180 - end
1.2181 - | None => error ("type_to_prop_tree: type contains an unknown type constructor: '" ^ s ^ "'"))
1.2182 - | TFree _ =>
1.2183 - let val s = size_of_type T us thy cdepth in
1.2184 - (Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
1.2185 - end
1.2186 - | TVar _ =>
1.2187 - let val s = size_of_type T us thy cdepth in
1.2188 - (Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
1.2189 - end
1.2190 + else
1.2191 + None
1.2192 end;
1.2193
1.2194 -(* ------------------------------------------------------------------------- *)
1.2195 -(* type_to_constants: creates a list of prop_trees with constants (True, *)
1.2196 -(* False) rather than boolean variables, one for every element in the *)
1.2197 -(* type 'T'; c.f. type_to_prop_tree *)
1.2198 -(* ------------------------------------------------------------------------- *)
1.2199 + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
1.2200
1.2201 - (* Term.typ -> (Term.typ * int) list -> theory -> int -> prop_tree list *)
1.2202 + fun var_funtype_printer thy model t intr assignment =
1.2203 + let
1.2204 + fun is_var (Free _) = true
1.2205 + | is_var (Var _) = true
1.2206 + | is_var _ = false
1.2207 + fun typeof (Free (_,T)) = T
1.2208 + | typeof (Var (_,T)) = T
1.2209 + | typeof _ = raise REFUTE ("var_funtype_printer", "term is not a variable")
1.2210 + fun is_funtype (Type ("fun", [_,_])) = true
1.2211 + | is_funtype _ = false
1.2212 + in
1.2213 + if is_var t andalso is_funtype (typeof t) then
1.2214 + let
1.2215 + val T1 = domain_type (typeof t)
1.2216 + val T2 = range_type (typeof t)
1.2217 + val (sizes, _) = model
1.2218 + (* create all constants of type T1 *)
1.2219 + val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_funtype_printer", T1))
1.2220 + (* returns a list with all unit vectors of length n *)
1.2221 + (* int -> interpretation list *)
1.2222 + fun unit_vectors n =
1.2223 + let
1.2224 + (* returns the k-th unit vector of length n *)
1.2225 + (* int * int -> interpretation *)
1.2226 + fun unit_vector (k,n) =
1.2227 + Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.2228 + (* int -> interpretation list -> interpretation list *)
1.2229 + fun unit_vectors_acc k vs =
1.2230 + if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
1.2231 + in
1.2232 + unit_vectors_acc 1 []
1.2233 + end
1.2234 + (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.2235 + (* 'a -> 'a list list -> 'a list list *)
1.2236 + fun cons_list x xss =
1.2237 + map (fn xs => x::xs) xss
1.2238 + (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
1.2239 + (* int -> 'a list -> 'a list list *)
1.2240 + fun pick_all 1 xs =
1.2241 + map (fn x => [x]) xs
1.2242 + | pick_all n xs =
1.2243 + let val rec_pick = pick_all (n-1) xs in
1.2244 + foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.2245 + end
1.2246 + (* interpretation -> interpretation list *)
1.2247 + fun make_constants (Leaf xs) =
1.2248 + unit_vectors (length xs)
1.2249 + | make_constants (Node xs) =
1.2250 + map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.2251 + (* interpretation list *)
1.2252 + val results = (case intr of
1.2253 + Node xs => xs
1.2254 + | _ => raise REFUTE ("var_funtype_printer", "interpretation is a leaf"))
1.2255 + (* string list *)
1.2256 + val strings = map
1.2257 + (fn (argi,resulti) => print thy model (Free ("var_funtype_printer", T1)) argi assignment
1.2258 + ^ "\\<mapsto>"
1.2259 + ^ print thy model (Free ("var_funtype_printer", T2)) resulti assignment)
1.2260 + ((make_constants i) ~~ results)
1.2261 + in
1.2262 + Some (enclose "(" ")" (commas strings))
1.2263 + end
1.2264 + else
1.2265 + None
1.2266 + end;
1.2267
1.2268 - fun type_to_constants T us thy cdepth =
1.2269 + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
1.2270 +
1.2271 + fun var_settype_printer thy model t intr assignment =
1.2272 let
1.2273 + val (sizes, _) = model
1.2274 (* returns a list with all unit vectors of length n *)
1.2275 - (* int -> prop_tree list *)
1.2276 + (* int -> interpretation list *)
1.2277 fun unit_vectors n =
1.2278 let
1.2279 (* returns the k-th unit vector of length n *)
1.2280 - (* int * int -> prop_tree *)
1.2281 + (* int * int -> interpretation *)
1.2282 fun unit_vector (k,n) =
1.2283 Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.2284 - (* int -> prop_tree list -> prop_tree list *)
1.2285 + (* int -> interpretation list -> interpretation list *)
1.2286 fun unit_vectors_acc k vs =
1.2287 if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
1.2288 in
1.2289 @@ -918,731 +1573,238 @@
1.2290 let val rec_pick = pick_all (n-1) xs in
1.2291 foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.2292 end
1.2293 + (* interpretation -> interpretation list *)
1.2294 + fun make_constants (Leaf xs) =
1.2295 + unit_vectors (length xs)
1.2296 + | make_constants (Node xs) =
1.2297 + map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.2298 in
1.2299 - case T of
1.2300 - Type ("prop", []) => unit_vectors 2
1.2301 - | Type ("bool", []) => unit_vectors 2
1.2302 - | Type ("Product_Type.unit", []) => unit_vectors 1
1.2303 - | Type ("+", [T1,T2]) =>
1.2304 + case t of
1.2305 + Free (x, Type ("set", [T])) =>
1.2306 let
1.2307 - val s1 = size_of_type T1 us thy cdepth
1.2308 - val s2 = size_of_type T2 us thy cdepth
1.2309 + (* interpretation list *)
1.2310 + val results = (case intr of
1.2311 + Node xs => xs
1.2312 + | _ => raise REFUTE ("var_settype_printer", "interpretation is a leaf"))
1.2313 + (* create all constants of type T *)
1.2314 + val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T))
1.2315 + (* string list *)
1.2316 + val strings = mapfilter
1.2317 + (fn (argi,Leaf [fmTrue,fmFalse]) =>
1.2318 + if PropLogic.eval assignment fmTrue then
1.2319 + Some (print thy model (Free ("x", T)) argi assignment)
1.2320 + else if PropLogic.eval assignment fmFalse then
1.2321 + None
1.2322 + else
1.2323 + raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned"))
1.2324 + ((make_constants i) ~~ results)
1.2325 in
1.2326 - if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
1.2327 - raise EMPTY_DATATYPE
1.2328 - else
1.2329 - error "sum types (+) not implemented yet (TODO)"
1.2330 - end
1.2331 - | Type ("*", [T1,T2]) =>
1.2332 - let
1.2333 - val s1 = size_of_type T1 us thy cdepth
1.2334 - val s2 = size_of_type T2 us thy cdepth
1.2335 - in
1.2336 - if s1=0 orelse s2=0 then
1.2337 - raise EMPTY_DATATYPE
1.2338 - else
1.2339 - error "product types (*) not implemented yet (TODO)"
1.2340 + Some (enclose "{" "}" (commas strings))
1.2341 end
1.2342 - | Type ("fun", [T1,T2]) =>
1.2343 + | Var ((x,i), Type ("set", [T])) =>
1.2344 let
1.2345 - val s = size_of_type T1 us thy cdepth
1.2346 + (* interpretation list *)
1.2347 + val results = (case intr of
1.2348 + Node xs => xs
1.2349 + | _ => raise REFUTE ("var_settype_printer", "interpretation is a leaf"))
1.2350 + (* create all constants of type T *)
1.2351 + val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T))
1.2352 + (* string list *)
1.2353 + val strings = mapfilter
1.2354 + (fn (argi,Leaf [fmTrue,fmFalse]) =>
1.2355 + if PropLogic.eval assignment fmTrue then
1.2356 + Some (print thy model (Free ("var_settype_printer", T)) argi assignment)
1.2357 + else if PropLogic.eval assignment fmTrue then
1.2358 + None
1.2359 + else
1.2360 + raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned"))
1.2361 + ((make_constants i) ~~ results)
1.2362 in
1.2363 - if s=0 then
1.2364 - raise EMPTY_DATATYPE
1.2365 - else
1.2366 - map (fn xs => Node xs) (pick_all s (type_to_constants T2 us thy cdepth))
1.2367 + Some (enclose "{" "}" (commas strings))
1.2368 end
1.2369 - | Type ("set", [T1]) => type_to_constants (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
1.2370 - | Type (s, _) =>
1.2371 - (case DatatypePackage.constrs_of thy s of
1.2372 - Some _ => (* inductive datatype *)
1.2373 - let
1.2374 - val s = size_of_type T us thy cdepth
1.2375 - in
1.2376 - if s=0 then
1.2377 - raise EMPTY_DATATYPE
1.2378 - else
1.2379 - unit_vectors s
1.2380 - end
1.2381 - | None => error ("type_to_constants: type contains an unknown type constructor: '" ^ s ^ "'"))
1.2382 - | TFree _ => unit_vectors (size_of_type T us thy cdepth)
1.2383 - | TVar _ => unit_vectors (size_of_type T us thy cdepth)
1.2384 + | _ => None
1.2385 end;
1.2386
1.2387 -(* ------------------------------------------------------------------------- *)
1.2388 -(* prop_tree_equal: returns a propositional formula that is true iff 'tr1' *)
1.2389 -(* and 'tr2' both denote the same element *)
1.2390 -(* ------------------------------------------------------------------------- *)
1.2391 -
1.2392 - (* prop_tree * prop_tree -> prop_formula *)
1.2393 + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
1.2394
1.2395 - fun prop_tree_equal (tr1,tr2) =
1.2396 - case tr1 of
1.2397 - Leaf x =>
1.2398 - (case tr2 of
1.2399 - Leaf y => prop_formula_dot_product (x,y)
1.2400 - | _ => raise REFUTE ("prop_tree_equal", "second tree is higher"))
1.2401 - | Node xs =>
1.2402 - (case tr2 of
1.2403 - Leaf _ => raise REFUTE ("prop_tree_equal", "first tree is higher")
1.2404 - (* extensionality: two functions are equal iff they are equal for every element *)
1.2405 - | Node ys => list_conjunction (map prop_tree_equal (xs ~~ ys)));
1.2406 + fun HOLogic_printer thy model t intr assignment =
1.2407 + case t of
1.2408 + (* 'arbitrary', 'The', 'Hilbert_Choice.Eps' are printed like free variables of the same type *)
1.2409 + Const ("arbitrary", T) =>
1.2410 + Some (print thy model (Free ("<arbitrary>", T)) intr assignment)
1.2411 + | Const ("The", T) =>
1.2412 + Some (print thy model (Free ("<The>", T)) intr assignment)
1.2413 + | Const ("Hilbert_Choice.Eps", T) =>
1.2414 + Some (print thy model (Free ("<Eps>", T)) intr assignment)
1.2415 + | _ =>
1.2416 + None;
1.2417
1.2418 -(* ------------------------------------------------------------------------- *)
1.2419 -(* prop_tree_apply: returns a tree that denotes the element obtained by *)
1.2420 -(* applying the function which is denoted by the tree 't1' to the *)
1.2421 -(* element which is denoted by the tree 't2' *)
1.2422 -(* ------------------------------------------------------------------------- *)
1.2423 + (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
1.2424
1.2425 - (* prop_tree * prop_tree -> prop_tree *)
1.2426 -
1.2427 - fun prop_tree_apply (tr1,tr2) =
1.2428 + fun var_IDT_printer thy model t intr assignment =
1.2429 let
1.2430 - (* prop_tree * prop_tree -> prop_tree *)
1.2431 - fun prop_tree_disjunction (tr1,tr2) =
1.2432 - tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
1.2433 - (* prop_formula * prop_tree -> prop_tree *)
1.2434 - fun prop_formula_times_prop_tree (fm,tr) =
1.2435 - tree_map (map (fn x => SAnd (fm,x))) tr
1.2436 - (* prop_formula list * prop_tree list -> prop_tree *)
1.2437 - fun prop_formula_list_dot_product_prop_tree_list ([fm],[tr]) =
1.2438 - prop_formula_times_prop_tree (fm,tr)
1.2439 - | prop_formula_list_dot_product_prop_tree_list (fm::fms,tr::trees) =
1.2440 - prop_tree_disjunction (prop_formula_times_prop_tree (fm,tr), prop_formula_list_dot_product_prop_tree_list (fms,trees))
1.2441 - | prop_formula_list_dot_product_prop_tree_list (_,_) =
1.2442 - raise REFUTE ("prop_tree_apply::prop_formula_list_dot_product_prop_tree_list", "empty list")
1.2443 - (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.2444 - (* 'a -> 'a list list -> 'a list list *)
1.2445 - fun cons_list x xss =
1.2446 - map (fn xs => x::xs) xss
1.2447 - (* returns a list of lists, each one consisting of one element from each element of 'xss' *)
1.2448 - (* 'a list list -> 'a list list *)
1.2449 - fun pick_all [xs] =
1.2450 - map (fn x => [x]) xs
1.2451 - | pick_all (xs::xss) =
1.2452 - let val rec_pick = pick_all xss in
1.2453 - foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.2454 - end
1.2455 - | pick_all _ =
1.2456 - raise REFUTE ("prop_tree_apply::pick_all", "empty list")
1.2457 - (* prop_tree -> prop_formula list *)
1.2458 - fun prop_tree_to_prop_formula_list (Leaf xs) =
1.2459 - xs
1.2460 - | prop_tree_to_prop_formula_list (Node trees) =
1.2461 - map list_conjunction (pick_all (map prop_tree_to_prop_formula_list trees))
1.2462 + fun is_var (Free _) = true
1.2463 + | is_var (Var _) = true
1.2464 + | is_var _ = false
1.2465 + fun typeof (Free (_,T)) = T
1.2466 + | typeof (Var (_,T)) = T
1.2467 + | typeof _ = raise REFUTE ("var_IDT_printer", "term is not a variable")
1.2468 in
1.2469 - case tr1 of
1.2470 - Leaf _ =>
1.2471 - raise REFUTE ("prop_tree_apply", "first tree is a leaf")
1.2472 - | Node xs =>
1.2473 - prop_formula_list_dot_product_prop_tree_list (prop_tree_to_prop_formula_list tr2, xs)
1.2474 - end
1.2475 -
1.2476 -(* ------------------------------------------------------------------------- *)
1.2477 -(* term_to_prop_tree: translates a HOL term 't' into a tree of propositional *)
1.2478 -(* formulas; 'us' specifies the number of elements for each type *)
1.2479 -(* variable in 't'; 'cdepth' specifies the maximal constructor depth *)
1.2480 -(* for inductive datatypes. Also returns the lowest index that was not *)
1.2481 -(* used for a boolean variable, and a substitution of terms (free/ *)
1.2482 -(* schematic variables) by prop_trees. *)
1.2483 -(* ------------------------------------------------------------------------- *)
1.2484 -
1.2485 - (* Term.term -> (Term.typ * int) list -> theory -> int -> prop_tree * (int * (Term.term * prop_tree) list) *)
1.2486 -
1.2487 - fun term_to_prop_tree t us thy cdepth =
1.2488 - let
1.2489 - (* Term.term -> int * (Term.term * prop_tree) list -> prop_tree * (int * (Term.term * prop_tree) list) *)
1.2490 - fun variable_to_prop_tree_subst t' (idx,subs) =
1.2491 - case assoc (subs,t') of
1.2492 - Some tr =>
1.2493 - (* return the previously associated tree; the substitution remains unchanged *)
1.2494 - (tr, (idx,subs))
1.2495 - | None =>
1.2496 - (* generate a new tree; update the index; extend the substitution *)
1.2497 - let
1.2498 - val T = case t' of
1.2499 - Free (_,T) => T
1.2500 - | Var (_,T) => T
1.2501 - | _ => raise REFUTE ("variable_to_prop_tree_subst", "term is not a (free or schematic) variable")
1.2502 - val (tr,newidx) = type_to_prop_tree T us thy cdepth idx
1.2503 - in
1.2504 - (tr, (newidx, (t',tr)::subs))
1.2505 - end
1.2506 - (* Term.term -> int * (Term.term * prop_tree) list -> prop_tree list -> prop_tree * (int * (Term.term * prop_tree) list) *)
1.2507 - fun term_to_prop_tree_subst t' (idx,subs) bsubs =
1.2508 - case t' of
1.2509 - (* meta-logical constants *)
1.2510 - Const ("Goal", _) $ t1 =>
1.2511 - term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2512 - | Const ("all", _) $ t1 =>
1.2513 - let
1.2514 - val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2515 - in
1.2516 - case tree1 of
1.2517 - Node xs =>
1.2518 + if is_var t then
1.2519 + (case typeof t of
1.2520 + Type (s, Ts) =>
1.2521 + (case DatatypePackage.datatype_info thy s of
1.2522 + Some info => (* inductive datatype *)
1.2523 + let
1.2524 + val index = #index info
1.2525 + val descr = #descr info
1.2526 + val (_, dtyps, constrs) = the (assoc (descr, index))
1.2527 + in
1.2528 + if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
1.2529 + raise REFUTE ("var_IDT_printer", "recursive datatype argument")
1.2530 + else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
1.2531 + None (* recursive datatype (requires an infinite model) *)
1.2532 + else
1.2533 let
1.2534 - val fmTrue = list_conjunction (map prop_tree_to_true xs)
1.2535 - val fmFalse = list_disjunction (map prop_tree_to_false xs)
1.2536 + val (sizes, _) = model
1.2537 + val typ_assoc = dtyps ~~ Ts
1.2538 + (* interpretation -> int *)
1.2539 + fun index_from_interpretation (Leaf xs) =
1.2540 + let
1.2541 + val idx = find_index (PropLogic.eval assignment) xs
1.2542 + in
1.2543 + if idx<0 then
1.2544 + raise REFUTE ("var_IDT_printer", "illegal interpretation: no value assigned")
1.2545 + else
1.2546 + idx
1.2547 + end
1.2548 + | index_from_interpretation _ =
1.2549 + raise REFUTE ("var_IDT_printer", "interpretation is not a leaf")
1.2550 + (* string -> string *)
1.2551 + fun unqualify s =
1.2552 + implode (snd (take_suffix (fn c => c <> ".") (explode s)))
1.2553 + (* DatatypeAux.dtyp -> Term.typ *)
1.2554 + fun typ_of_dtyp (DatatypeAux.DtTFree a) =
1.2555 + the (assoc (typ_assoc, DatatypeAux.DtTFree a))
1.2556 + | typ_of_dtyp (DatatypeAux.DtRec i) =
1.2557 + raise REFUTE ("var_IDT_printer", "recursive datatype")
1.2558 + | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
1.2559 + Type (s, map typ_of_dtyp ds)
1.2560 + fun sum xs = foldl op+ (0, xs)
1.2561 + fun product xs = foldl op* (1, xs)
1.2562 + (* power(a,b) computes a^b, for a>=0, b>=0 *)
1.2563 + (* int * int -> int *)
1.2564 + fun power (a,0) = 1
1.2565 + | power (a,1) = a
1.2566 + | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
1.2567 + fun size_of_interpretation (Leaf xs) = length xs
1.2568 + | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
1.2569 + fun size_of_type T =
1.2570 + let
1.2571 + val (i,_,_) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<IDT>", T))
1.2572 + in
1.2573 + size_of_interpretation i
1.2574 + end
1.2575 + (* returns a list with all unit vectors of length n *)
1.2576 + (* int -> interpretation list *)
1.2577 + fun unit_vectors n =
1.2578 + let
1.2579 + (* returns the k-th unit vector of length n *)
1.2580 + (* int * int -> interpretation *)
1.2581 + fun unit_vector (k,n) =
1.2582 + Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.2583 + (* int -> interpretation list -> interpretation list *)
1.2584 + fun unit_vectors_acc k vs =
1.2585 + if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
1.2586 + in
1.2587 + unit_vectors_acc 1 []
1.2588 + end
1.2589 + (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.2590 + (* 'a -> 'a list list -> 'a list list *)
1.2591 + fun cons_list x xss =
1.2592 + map (fn xs => x::xs) xss
1.2593 + (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
1.2594 + (* int -> 'a list -> 'a list list *)
1.2595 + fun pick_all 1 xs =
1.2596 + map (fn x => [x]) xs
1.2597 + | pick_all n xs =
1.2598 + let val rec_pick = pick_all (n-1) xs in
1.2599 + foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.2600 + end
1.2601 + (* interpretation -> interpretation list *)
1.2602 + fun make_constants (Leaf xs) =
1.2603 + unit_vectors (length xs)
1.2604 + | make_constants (Node xs) =
1.2605 + map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
1.2606 + (* DatatypeAux.dtyp list -> int -> string *)
1.2607 + fun string_of_inductive_type_cargs [] n =
1.2608 + if n<>0 then
1.2609 + raise REFUTE ("var_IDT_printer", "internal error computing the element index for an inductive type")
1.2610 + else
1.2611 + ""
1.2612 + | string_of_inductive_type_cargs (d::ds) n =
1.2613 + let
1.2614 + val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d)) ds)
1.2615 + val T = typ_of_dtyp d
1.2616 + val (i,_,_) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<IDT>", T))
1.2617 + val constants = make_constants i
1.2618 + in
1.2619 + " "
1.2620 + ^ (print thy model (Free ("<IDT>", T)) (nth_elem (n div size_ds, constants)) assignment)
1.2621 + ^ (string_of_inductive_type_cargs ds (n mod size_ds))
1.2622 + end
1.2623 + (* (string * DatatypeAux.dtyp list) list -> int -> string *)
1.2624 + fun string_of_inductive_type_constrs [] n =
1.2625 + raise REFUTE ("var_IDT_printer", "inductive type has fewer elements than needed")
1.2626 + | string_of_inductive_type_constrs ((c,ds)::cs) n =
1.2627 + let
1.2628 + val size = product (map (fn d => size_of_type (typ_of_dtyp d)) ds)
1.2629 + in
1.2630 + if n < size then
1.2631 + (unqualify c) ^ (string_of_inductive_type_cargs ds n)
1.2632 + else
1.2633 + string_of_inductive_type_constrs cs (n - size)
1.2634 + end
1.2635 in
1.2636 - (Leaf [fmTrue, fmFalse], (i1,s1))
1.2637 + Some (string_of_inductive_type_constrs constrs (index_from_interpretation intr))
1.2638 end
1.2639 - | _ =>
1.2640 - raise REFUTE ("term_to_prop_tree_subst", "'all' is not followed by a function")
1.2641 - end
1.2642 - | Const ("==", _) $ t1 $ t2 =>
1.2643 - let
1.2644 - val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2645 - val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.2646 - val fmTrue = prop_tree_equal (tree1,tree2)
1.2647 - val fmFalse = SNot fmTrue
1.2648 - in
1.2649 - (Leaf [fmTrue, fmFalse], (i2,s2))
1.2650 - end
1.2651 - | Const ("==>", _) $ t1 $ t2 =>
1.2652 - let
1.2653 - val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2654 - val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.2655 - val fmTrue = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
1.2656 - val fmFalse = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
1.2657 - in
1.2658 - (Leaf [fmTrue, fmFalse], (i2,s2))
1.2659 - end
1.2660 - (* HOL constants *)
1.2661 - | Const ("Trueprop", _) $ t1 =>
1.2662 - term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2663 - | Const ("Not", _) $ t1 =>
1.2664 - let
1.2665 - val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2666 - val fmTrue = prop_tree_to_false tree1
1.2667 - val fmFalse = prop_tree_to_true tree1
1.2668 - in
1.2669 - (Leaf [fmTrue, fmFalse], (i1,s1))
1.2670 - end
1.2671 - | Const ("True", _) =>
1.2672 - (Leaf [True, False], (idx,subs))
1.2673 - | Const ("False", _) =>
1.2674 - (Leaf [False, True], (idx,subs))
1.2675 - | Const ("All", _) $ t1 =>
1.2676 - let
1.2677 - val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2678 - in
1.2679 - case tree1 of
1.2680 - Node xs =>
1.2681 - let
1.2682 - val fmTrue = list_conjunction (map prop_tree_to_true xs)
1.2683 - val fmFalse = list_disjunction (map prop_tree_to_false xs)
1.2684 - in
1.2685 - (Leaf [fmTrue, fmFalse], (i1,s1))
1.2686 - end
1.2687 - | _ =>
1.2688 - raise REFUTE ("term_to_prop_tree_subst", "'All' is not followed by a function")
1.2689 - end
1.2690 - | Const ("Ex", _) $ t1 =>
1.2691 - let
1.2692 - val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2693 - in
1.2694 - case tree1 of
1.2695 - Node xs =>
1.2696 - let
1.2697 - val fmTrue = list_disjunction (map prop_tree_to_true xs)
1.2698 - val fmFalse = list_conjunction (map prop_tree_to_false xs)
1.2699 - in
1.2700 - (Leaf [fmTrue, fmFalse], (i1,s1))
1.2701 - end
1.2702 - | _ =>
1.2703 - raise REFUTE ("term_to_prop_tree_subst", "'Ex' is not followed by a function")
1.2704 - end
1.2705 - | Const ("Ex1", Type ("fun", [Type ("fun", [T, Type ("bool",[])]), Type ("bool",[])])) $ t1 =>
1.2706 - (* 'Ex1 t1' is equivalent to 'Ex Abs(x,T,t1' x & All Abs(y,T,t1'' y --> x=y))' *)
1.2707 - let
1.2708 - val t1' = Term.incr_bv (1, 0, t1)
1.2709 - val t1'' = Term.incr_bv (2, 0, t1)
1.2710 - val t_equal = (HOLogic.eq_const T) $ (Bound 1) $ (Bound 0)
1.2711 - val t_unique = (HOLogic.all_const T) $ Abs("y",T,HOLogic.mk_imp (t1'' $ (Bound 0),t_equal))
1.2712 - val t_ex1 = (HOLogic.exists_const T) $ Abs("x",T,HOLogic.mk_conj (t1' $ (Bound 0),t_unique))
1.2713 - in
1.2714 - term_to_prop_tree_subst t_ex1 (idx,subs) bsubs
1.2715 - end
1.2716 - | Const ("op =", _) $ t1 $ t2 =>
1.2717 - let
1.2718 - val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2719 - val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.2720 - val fmTrue = prop_tree_equal (tree1,tree2)
1.2721 - val fmFalse = SNot fmTrue
1.2722 - in
1.2723 - (Leaf [fmTrue, fmFalse], (i2,s2))
1.2724 - end
1.2725 - | Const ("op &", _) $ t1 $ t2 =>
1.2726 - let
1.2727 - val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2728 - val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.2729 - val fmTrue = SAnd (prop_tree_to_true tree1, prop_tree_to_true tree2)
1.2730 - val fmFalse = SOr (prop_tree_to_false tree1, prop_tree_to_false tree2)
1.2731 - in
1.2732 - (Leaf [fmTrue, fmFalse], (i2,s2))
1.2733 - end
1.2734 - | Const ("op |", _) $ t1 $ t2 =>
1.2735 - let
1.2736 - val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2737 - val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.2738 - val fmTrue = SOr (prop_tree_to_true tree1, prop_tree_to_true tree2)
1.2739 - val fmFalse = SAnd (prop_tree_to_false tree1, prop_tree_to_false tree2)
1.2740 - in
1.2741 - (Leaf [fmTrue, fmFalse], (i2,s2))
1.2742 - end
1.2743 - | Const ("op -->", _) $ t1 $ t2 =>
1.2744 - let
1.2745 - val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2746 - val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.2747 - val fmTrue = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
1.2748 - val fmFalse = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
1.2749 - in
1.2750 - (Leaf [fmTrue, fmFalse], (i2,s2))
1.2751 - end
1.2752 - (* set constants *)
1.2753 - | Const ("Collect", _) $ t1 =>
1.2754 - term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2755 - | Const ("op :", _) $ t1 $ t2 =>
1.2756 - term_to_prop_tree_subst (t2 $ t1) (idx,subs) bsubs
1.2757 - (* datatype constants *)
1.2758 - | Const ("Product_Type.Unity", _) =>
1.2759 - (Leaf [True], (idx,subs))
1.2760 - (* unknown constants *)
1.2761 - | Const (c, _) =>
1.2762 - error ("term contains an unknown constant: '" ^ c ^ "'")
1.2763 - (* abstractions *)
1.2764 - | Abs (_,T,body) =>
1.2765 - let
1.2766 - val constants = type_to_constants T us thy cdepth
1.2767 - val (trees, substs) = split_list (map (fn c => term_to_prop_tree_subst body (idx,subs) (c::bsubs)) constants)
1.2768 - in
1.2769 - (* the substitutions in 'substs' are all identical *)
1.2770 - (Node trees, hd substs)
1.2771 - end
1.2772 - (* (free/schematic) variables *)
1.2773 - | Free _ =>
1.2774 - variable_to_prop_tree_subst t' (idx,subs)
1.2775 - | Var _ =>
1.2776 - variable_to_prop_tree_subst t' (idx,subs)
1.2777 - (* bound variables *)
1.2778 - | Bound i =>
1.2779 - if (length bsubs) <= i then
1.2780 - raise REFUTE ("term_to_prop_tree_subst", "term contains a loose bound variable (with index " ^ (string_of_int i) ^ ")")
1.2781 - else
1.2782 - (nth_elem (i,bsubs), (idx,subs))
1.2783 - (* application *)
1.2784 - | t1 $ t2 =>
1.2785 - let
1.2786 - val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.2787 - val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.2788 - in
1.2789 - (prop_tree_apply (tree1,tree2), (i2,s2))
1.2790 - end
1.2791 - in
1.2792 - term_to_prop_tree_subst t (1,[]) []
1.2793 - end;
1.2794 -
1.2795 -(* ------------------------------------------------------------------------- *)
1.2796 -(* term_to_prop_formula: translates a HOL formula 't' into a propositional *)
1.2797 -(* formula that is satisfiable if and only if 't' has a model of "size" *)
1.2798 -(* 'us' (where 'us' specifies the number of elements for each free type *)
1.2799 -(* variable in 't') and maximal constructor depth 'cdepth'. *)
1.2800 -(* ------------------------------------------------------------------------- *)
1.2801 -
1.2802 - (* TODO: shouldn't 'us' also specify the number of elements for schematic type variables? (if so, modify the comment above) *)
1.2803 -
1.2804 - (* Term.term -> (Term.typ * int) list -> theory -> int -> prop_formula * (int * (Term.term * prop_tree) list) *)
1.2805 -
1.2806 - fun term_to_prop_formula t us thy cdepth =
1.2807 - let
1.2808 - val (tr, (idx,subs)) = term_to_prop_tree t us thy cdepth
1.2809 - val fm = prop_tree_to_true tr
1.2810 - in
1.2811 - if subs=[] then
1.2812 - (fm, (idx,subs))
1.2813 + end
1.2814 + | None => None)
1.2815 + | _ => None)
1.2816 else
1.2817 - (* make sure every tree that is substituted for a term describes a single element *)
1.2818 - (SAnd (list_conjunction (map (fn (_,tr) => restrict_to_single_element tr) subs), fm), (idx,subs))
1.2819 + None
1.2820 end;
1.2821
1.2822
1.2823 (* ------------------------------------------------------------------------- *)
1.2824 -(* INTERFACE, PART 2: FINDING A MODEL *)
1.2825 +(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
1.2826 +(* structure *)
1.2827 (* ------------------------------------------------------------------------- *)
1.2828
1.2829 (* ------------------------------------------------------------------------- *)
1.2830 -(* string_of_universe: prints a universe, i.e. an assignment of sizes for *)
1.2831 -(* types *)
1.2832 -(* thy: the current theory *)
1.2833 -(* us : a list containing types together with their size *)
1.2834 -(* ------------------------------------------------------------------------- *)
1.2835 -
1.2836 - (* theory -> (Term.typ * int) list -> string *)
1.2837 -
1.2838 - fun string_of_universe thy [] =
1.2839 - "empty universe (no type variables in term)"
1.2840 - | string_of_universe thy us =
1.2841 - space_implode ", " (map (fn (T,i) => (Sign.string_of_typ (sign_of thy) T) ^ ": " ^ (string_of_int i)) us);
1.2842 -
1.2843 -(* ------------------------------------------------------------------------- *)
1.2844 -(* string_of_model: prints a model, given by a substitution 'subs' of trees *)
1.2845 -(* of propositional variables and an assignment 'ass' of truth values *)
1.2846 -(* for these variables. *)
1.2847 -(* thy : the current theory *)
1.2848 -(* us : universe, specifies the "size" of each type (i.e. type variable) *)
1.2849 -(* cdepth: maximal constructor depth for inductive datatypes *)
1.2850 -(* subs : substitution of trees of propositional formulas (for variables) *)
1.2851 -(* ass : assignment of truth values for boolean variables; see function *)
1.2852 -(* 'truth_value' below for its meaning *)
1.2853 +(* Note: the interpreters and printers are used in reverse order; however, *)
1.2854 +(* an interpreter that can handle non-atomic terms ends up being *)
1.2855 +(* applied before other interpreters are applied to subterms! *)
1.2856 (* ------------------------------------------------------------------------- *)
1.2857
1.2858 - (* theory -> (Term.typ * int) list -> int -> (Term.term * prop_formula tree) list -> int list -> string *)
1.2859 -
1.2860 - fun string_of_model thy us cdepth [] ass =
1.2861 - "empty interpretation (no free variables in term)"
1.2862 - | string_of_model thy us cdepth subs ass =
1.2863 - let
1.2864 - (* Sign.sg *)
1.2865 - val sg = sign_of thy
1.2866 - (* int -> bool *)
1.2867 - fun truth_value i =
1.2868 - if i mem ass then true
1.2869 - else if ~i mem ass then false
1.2870 - else error ("SAT solver assignment does not specify a value for variable " ^ (string_of_int i))
1.2871 - (* string -> string *)
1.2872 - fun strip_leading_quote str =
1.2873 - if nth_elem_string(0,str)="'" then
1.2874 - String.substring (str, 1, size str - 1)
1.2875 - else
1.2876 - str;
1.2877 - (* prop_formula list -> int *)
1.2878 - fun true_index xs =
1.2879 - (* returns the (0-based) index of the first true formula in xs *)
1.2880 - let fun true_index_acc [] _ =
1.2881 - raise REFUTE ("string_of_model::true_index", "no variable was set to true")
1.2882 - | true_index_acc (x::xs) n =
1.2883 - case x of
1.2884 - BoolVar i =>
1.2885 - if truth_value i then n else true_index_acc xs (n+1)
1.2886 - | True =>
1.2887 - n
1.2888 - | False =>
1.2889 - true_index_acc xs (n+1)
1.2890 - | _ =>
1.2891 - raise REFUTE ("string_of_model::true_index", "formula is not a boolean variable/true/false")
1.2892 - in
1.2893 - true_index_acc xs 0
1.2894 - end
1.2895 - (* Term.typ -> int -> prop_tree -> string *)
1.2896 - (* prop *)
1.2897 - fun string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
1.2898 - if truth_value i then "true" else "false"
1.2899 - | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [True, False]) =
1.2900 - "true"
1.2901 - | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [False, True]) =
1.2902 - "false"
1.2903 - (* bool *)
1.2904 - | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
1.2905 - if truth_value i then "true" else "false"
1.2906 - | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [True, False]) =
1.2907 - "true"
1.2908 - | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [False, True]) =
1.2909 - "false"
1.2910 - (* unit *)
1.2911 - | string_of_prop_tree (Type ("Product_Type.unit",[])) cdepth (Leaf [True]) =
1.2912 - "()"
1.2913 - | string_of_prop_tree (Type (s,Ts)) cdepth (Leaf xs) =
1.2914 - (case DatatypePackage.datatype_info thy s of
1.2915 - Some info => (* inductive datatype *)
1.2916 - let
1.2917 - val index = #index info
1.2918 - val descr = #descr info
1.2919 - val (_, dtyps, constrs) = the (assoc (descr, index))
1.2920 - val Typs = dtyps ~~ Ts
1.2921 - (* string -> string *)
1.2922 - fun unqualify s =
1.2923 - implode (snd (take_suffix (fn c => c <> ".") (explode s)))
1.2924 - (* DatatypeAux.dtyp -> Term.typ *)
1.2925 - fun typ_of_dtyp (DatatypeAux.DtTFree a) =
1.2926 - the (assoc (Typs, DatatypeAux.DtTFree a))
1.2927 - | typ_of_dtyp (DatatypeAux.DtRec i) =
1.2928 - let
1.2929 - val (s, ds, _) = the (assoc (descr, i))
1.2930 - in
1.2931 - Type (s, map typ_of_dtyp ds)
1.2932 - end
1.2933 - | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
1.2934 - Type (s, map typ_of_dtyp ds)
1.2935 - (* DatatypeAux.dtyp list -> int -> string *)
1.2936 - fun string_of_inductive_type_cargs [] n =
1.2937 - if n<>0 then
1.2938 - raise REFUTE ("string_of_model", "internal error computing the element index for an inductive type")
1.2939 - else
1.2940 - ""
1.2941 - | string_of_inductive_type_cargs (d::ds) n =
1.2942 - let
1.2943 - val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
1.2944 - in
1.2945 - " " ^ (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))
1.2946 - end
1.2947 - (* (string * DatatypeAux.dtyp list) list -> int -> string *)
1.2948 - fun string_of_inductive_type_constrs [] n =
1.2949 - raise REFUTE ("string_of_model", "inductive type has fewer elements than needed")
1.2950 - | string_of_inductive_type_constrs ((s,ds)::cs) n =
1.2951 - let
1.2952 - val size = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
1.2953 - in
1.2954 - if n < size then
1.2955 - (unqualify s) ^ (string_of_inductive_type_cargs ds n)
1.2956 - else
1.2957 - string_of_inductive_type_constrs cs (n - size)
1.2958 - end
1.2959 - in
1.2960 - string_of_inductive_type_constrs constrs (true_index xs)
1.2961 - end
1.2962 - | None =>
1.2963 - raise REFUTE ("string_of_model", "type contains an unknown type constructor: '" ^ s ^ "'"))
1.2964 - (* type variable *)
1.2965 - | string_of_prop_tree (TFree (s,_)) cdepth (Leaf xs) =
1.2966 - (strip_leading_quote s) ^ (string_of_int (true_index xs))
1.2967 - | string_of_prop_tree (TVar ((s,_),_)) cdepth (Leaf xs) =
1.2968 - (strip_leading_quote s) ^ (string_of_int (true_index xs))
1.2969 - (* function or set type *)
1.2970 - | string_of_prop_tree T cdepth (Node xs) =
1.2971 - case T of
1.2972 - Type ("fun", [T1,T2]) =>
1.2973 - let
1.2974 - val strings = foldl (fn (ss,(c,x)) => ss @ [(string_of_prop_tree T1 cdepth c) ^ "\\<mapsto>" ^ (string_of_prop_tree T2 cdepth x)]) ([], (type_to_constants T1 us thy cdepth) ~~ xs)
1.2975 - in
1.2976 - "(" ^ (space_implode ", " strings) ^ ")"
1.2977 - end
1.2978 - | Type ("set", [T1]) =>
1.2979 - let
1.2980 - 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)
1.2981 - in
1.2982 - "{" ^ (space_implode ", " strings) ^ "}"
1.2983 - end
1.2984 - | _ => raise REFUTE ("string_of_model::string_of_prop_tree", "not a function/set type")
1.2985 - (* Term.term * prop_formula tree -> string *)
1.2986 - fun string_of_term_assignment (t,tr) =
1.2987 - let
1.2988 - val T = case t of
1.2989 - Free (_,T) => T
1.2990 - | Var (_,T) => T
1.2991 - | _ => raise REFUTE ("string_of_model::string_of_term_assignment", "term is not a (free or schematic) variable")
1.2992 - in
1.2993 - (Sign.string_of_term sg t) ^ " = " ^ (string_of_prop_tree T cdepth tr)
1.2994 - end
1.2995 - in
1.2996 - space_implode "\n" (map string_of_term_assignment subs)
1.2997 - end;
1.2998 + (* (theory -> theory) list *)
1.2999
1.3000 -(* ------------------------------------------------------------------------- *)
1.3001 -(* find_model: repeatedly calls 'prop_formula_sat_solver' with appropriate *)
1.3002 -(* parameters, and displays the results to the user *)
1.3003 -(* params : list of '(name, value)' pairs used to override default *)
1.3004 -(* parameters *)
1.3005 -(* *)
1.3006 -(* This is a brief description of the algorithm implemented: *)
1.3007 -(* *)
1.3008 -(* 1. Let k = max ('minsize',1). *)
1.3009 -(* 2. Let the universe have k elements. Find all possible partitions of *)
1.3010 -(* these elements into the basic types occuring in 't' such that no basic *)
1.3011 -(* type is empty. *)
1.3012 -(* 3. Translate 't' into a propositional formula p s.t. 't' has a model wrt. *)
1.3013 -(* the partition chosen in step (2.) if (actually, if and only if) p is *)
1.3014 -(* satisfiable. To do this, replace quantification by conjunction/ *)
1.3015 -(* disjunction over all elements of the type being quantified over. (If *)
1.3016 -(* p contains more than 'maxvars' boolean variables, terminate.) *)
1.3017 -(* 4. Serialize p to a file, and try to find a satisfying assignment for p *)
1.3018 -(* by invoking an external SAT solver. *)
1.3019 -(* 5. If the SAT solver finds a satisfying assignment for p, translate this *)
1.3020 -(* assignment back into a model for 't'. Present this model to the user, *)
1.3021 -(* then terminate. *)
1.3022 -(* 6. As long as there is another partition left, pick it and go back to *)
1.3023 -(* step (3.). *)
1.3024 -(* 7. Increase k by 1. As long as k does not exceed 'maxsize', go back to *)
1.3025 -(* step (2.). *)
1.3026 -(* *)
1.3027 -(* The following parameters are currently supported (and required!): *)
1.3028 -(* *)
1.3029 -(* Name Type Description *)
1.3030 -(* *)
1.3031 -(* "minsize" int Only search for models with size at least *)
1.3032 -(* 'minsize'. *)
1.3033 -(* "maxsize" int If >0, only search for models with size at most *)
1.3034 -(* 'maxsize'. *)
1.3035 -(* "maxvars" int If >0, use at most 'maxvars' boolean variables *)
1.3036 -(* when transforming the term into a propositional *)
1.3037 -(* formula. *)
1.3038 -(* "satfile" string Name of the file used to store the propositional *)
1.3039 -(* formula, i.e. the input to the SAT solver. *)
1.3040 -(* "satformat" string Format of the SAT solver's input file. Must be *)
1.3041 -(* either "cnf", "defcnf", or "sat". Since "sat" is *)
1.3042 -(* not supported by most SAT solvers, and "cnf" can *)
1.3043 -(* cause exponential blowup of the formula, "defcnf" *)
1.3044 -(* is recommended. *)
1.3045 -(* "resultfile" string Name of the file containing the SAT solver's *)
1.3046 -(* output. *)
1.3047 -(* "success" string Part of the line in the SAT solver's output that *)
1.3048 -(* precedes a list of integers representing the *)
1.3049 -(* satisfying assignment. *)
1.3050 -(* "command" string System command used to execute the SAT solver. *)
1.3051 -(* Note that you if you change 'satfile' or *)
1.3052 -(* 'resultfile', you will also need to change *)
1.3053 -(* 'command'. *)
1.3054 -(* *)
1.3055 -(* See the Isabelle/Isar theory 'Refute.thy' for reasonable default values. *)
1.3056 -(* ------------------------------------------------------------------------- *)
1.3057 -
1.3058 - (* theory -> (string * string) list -> Term.term -> unit *)
1.3059 -
1.3060 - fun find_model thy params t =
1.3061 - let
1.3062 - (* (string * string) list * (string * string) list -> (string * string) list *)
1.3063 - fun add_params (parms, []) =
1.3064 - parms
1.3065 - | add_params (parms, defparm::defparms) =
1.3066 - add_params (gen_ins (fn (a, b) => (fst a) = (fst b)) (defparm, parms), defparms)
1.3067 - (* (string * string) list * string -> int *)
1.3068 - fun read_int (parms, name) =
1.3069 - case assoc_string (parms, name) of
1.3070 - Some s => (case Int.fromString s of
1.3071 - SOME i => i
1.3072 - | NONE => error ("parameter '" ^ name ^ "' (value is '" ^ s ^ "') must be an integer value"))
1.3073 - | None => error ("parameter '" ^ name ^ "' must be assigned a value")
1.3074 - (* (string * string) list * string -> string *)
1.3075 - fun read_string (parms, name) =
1.3076 - case assoc_string (parms, name) of
1.3077 - Some s => s
1.3078 - | None => error ("parameter '" ^ name ^ "' must be assigned a value")
1.3079 - (* (string * string) list *)
1.3080 - val allparams = add_params (params, get_default_params thy)
1.3081 - (* int *)
1.3082 - val minsize = read_int (allparams, "minsize")
1.3083 - val maxsize = read_int (allparams, "maxsize")
1.3084 - val maxvars = read_int (allparams, "maxvars")
1.3085 - (* string *)
1.3086 - val satfile = read_string (allparams, "satfile")
1.3087 - val satformat = read_string (allparams, "satformat")
1.3088 - val resultfile = read_string (allparams, "resultfile")
1.3089 - val success = read_string (allparams, "success")
1.3090 - val command = read_string (allparams, "command")
1.3091 - (* misc *)
1.3092 - val satpath = Path.unpack satfile
1.3093 - val resultpath = Path.unpack resultfile
1.3094 - val sg = sign_of thy
1.3095 - (* Term.typ list *)
1.3096 - val tvars = map (fn (i,s) => TVar(i,s)) (term_tvars t)
1.3097 - val tfrees = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
1.3098 - (* universe -> int -> bool *)
1.3099 - fun find_model_universe u cdepth =
1.3100 - let
1.3101 - (* given the universe 'u' and constructor depth 'cdepth', translate *)
1.3102 - (* the term 't' into a propositional formula 'fm' *)
1.3103 - val (fm,(idx,subs)) = term_to_prop_formula t u thy cdepth
1.3104 - val usedvars = idx-1
1.3105 - in
1.3106 - (* 'maxvars=0' means "use as many variables as necessary" *)
1.3107 - if usedvars>maxvars andalso maxvars<>0 then
1.3108 - (
1.3109 - (* too many variables used: terminate *)
1.3110 - writeln ("\nSearch terminated: " ^ (string_of_int usedvars) ^ " boolean variables used (only " ^ (string_of_int maxvars) ^ " allowed).");
1.3111 - true
1.3112 - )
1.3113 - else
1.3114 - (* pass the formula 'fm' to an external SAT solver *)
1.3115 - case prop_formula_sat_solver fm satpath satformat resultpath success command of
1.3116 - None =>
1.3117 - (* no model found *)
1.3118 - false
1.3119 - | Some assignment =>
1.3120 - (* model found: terminate *)
1.3121 - (
1.3122 - writeln ("\nModel found:\n" ^ (string_of_universe thy u) ^ "\n" ^ (string_of_model thy u cdepth subs assignment));
1.3123 - true
1.3124 - )
1.3125 - end
1.3126 - (* universe list -> int -> bool *)
1.3127 - fun find_model_universes [] cdepth =
1.3128 - (
1.3129 - std_output "\n";
1.3130 - false
1.3131 - )
1.3132 - | find_model_universes (u::us) cdepth =
1.3133 - (
1.3134 - std_output ".";
1.3135 - ((if find_model_universe u cdepth then
1.3136 - (* terminate *)
1.3137 - true
1.3138 - else
1.3139 - (* continue search with the next universe *)
1.3140 - find_model_universes us cdepth)
1.3141 - handle EMPTY_DATATYPE => (std_output "[empty inductive type (constructor depth too small)]\n"; false))
1.3142 - )
1.3143 - (* int * int -> unit *)
1.3144 - fun find_model_from_to (min,max) =
1.3145 - (* 'max=0' means "search for arbitrary large models" *)
1.3146 - if min>max andalso max<>0 then
1.3147 - writeln ("Search terminated: no model found.")
1.3148 - else
1.3149 - (
1.3150 - std_output ("Searching for a model of size " ^ (string_of_int min));
1.3151 - if find_model_universes (make_universes tfrees min) min then
1.3152 - (* terminate *)
1.3153 - ()
1.3154 - else
1.3155 - (* continue search with increased size *)
1.3156 - find_model_from_to (min+1, max)
1.3157 - )
1.3158 - in
1.3159 - writeln ("Trying to find a model of: " ^ (Sign.string_of_term sg t));
1.3160 - if tvars<>[] then
1.3161 - (* TODO: deal with schematic type variables in a better way, if possible *)
1.3162 - error "term contains schematic type variables"
1.3163 - else
1.3164 - (
1.3165 - if minsize<1 then
1.3166 - writeln ("'minsize' is less than 1; starting search with size 1.")
1.3167 - else
1.3168 - ();
1.3169 - if maxsize<max (minsize,1) andalso maxsize<>0 then
1.3170 - writeln ("'maxsize' is less than 'minsize': no model found.")
1.3171 - else
1.3172 - find_model_from_to (max (minsize,1), maxsize)
1.3173 - )
1.3174 - end;
1.3175 -
1.3176 -(* ------------------------------------------------------------------------- *)
1.3177 -(* refute_term: calls 'find_model' on the negation of a term *)
1.3178 -(* params : list of '(name, value)' pairs used to override default *)
1.3179 -(* parameters *)
1.3180 -(* ------------------------------------------------------------------------- *)
1.3181 -
1.3182 - (* theory -> (string * string) list -> Term.term -> unit *)
1.3183 -
1.3184 - fun refute_term thy params t =
1.3185 - let
1.3186 - (* TODO: schematic type variables? *)
1.3187 - val negation = close_vars (HOLogic.Not $ t)
1.3188 - (* If 't' is of type 'propT' (rather than 'boolT'), applying *)
1.3189 - (* 'HOLogic.Not' is not type-correct. However, this isn't *)
1.3190 - (* really a problem as long as 'find_model' still interprets *)
1.3191 - (* the resulting term correctly, without checking its type. *)
1.3192 - in
1.3193 - find_model thy params negation
1.3194 - end;
1.3195 -
1.3196 -(* ------------------------------------------------------------------------- *)
1.3197 -(* refute_subgoal: calls 'refute_term' on a specific subgoal *)
1.3198 -(* params : list of '(name, value)' pairs used to override default *)
1.3199 -(* parameters *)
1.3200 -(* subgoal : 0-based index specifying the subgoal number *)
1.3201 -(* ------------------------------------------------------------------------- *)
1.3202 -
1.3203 - (* theory -> (string * string) list -> Thm.thm -> int -> unit *)
1.3204 -
1.3205 - fun refute_subgoal thy params thm subgoal =
1.3206 - refute_term thy params (nth_elem (subgoal, prems_of thm));
1.3207 + val setup =
1.3208 + [RefuteData.init,
1.3209 + add_interpreter "var_typevar" var_typevar_interpreter,
1.3210 + add_interpreter "var_funtype" var_funtype_interpreter,
1.3211 + add_interpreter "var_settype" var_settype_interpreter,
1.3212 + add_interpreter "boundvar" boundvar_interpreter,
1.3213 + add_interpreter "abstraction" abstraction_interpreter,
1.3214 + add_interpreter "apply" apply_interpreter,
1.3215 + add_interpreter "const_unfold" const_unfold_interpreter,
1.3216 + add_interpreter "Pure" Pure_interpreter,
1.3217 + add_interpreter "HOLogic" HOLogic_interpreter,
1.3218 + add_interpreter "IDT" IDT_interpreter,
1.3219 + add_printer "var_typevar" var_typevar_printer,
1.3220 + add_printer "var_funtype" var_funtype_printer,
1.3221 + add_printer "var_settype" var_settype_printer,
1.3222 + add_printer "HOLogic" HOLogic_printer,
1.3223 + add_printer "var_IDT" var_IDT_printer];
1.3224
1.3225 end