--- a/src/HOL/Tools/refute.ML Wed Mar 10 20:36:11 2004 +0100
+++ b/src/HOL/Tools/refute.ML Wed Mar 10 22:33:48 2004 +0100
@@ -3,526 +3,77 @@
Author: Tjark Weber
Copyright 2003-2004
-Finite model generation for HOL formulae, using an external SAT solver.
+Finite model generation for HOL formulae, using a SAT solver.
*)
(* ------------------------------------------------------------------------- *)
-(* Declares the 'REFUTE' signature as well as a structure 'Refute'. See *)
-(* 'find_model' below for a description of the implemented algorithm, and *)
-(* the Isabelle/Isar theories 'HOL/Refute.thy' and 'HOL/Main.thy' on how to *)
-(* set things up. *)
+(* TODO: Change parameter handling so that only supported parameters can be *)
+(* set, and specify defaults here, rather than in HOL/Main.thy. *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* Declares the 'REFUTE' signature as well as a structure 'Refute'. *)
+(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'. *)
(* ------------------------------------------------------------------------- *)
signature REFUTE =
sig
+ exception REFUTE of string * string
+
+(* ------------------------------------------------------------------------- *)
+(* Model/interpretation related code (translation HOL -> boolean formula) *)
+(* ------------------------------------------------------------------------- *)
+
+ exception CANNOT_INTERPRET
+
+ type interpretation
+ type model
+ type arguments
+
+ val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory
+ val add_printer : string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory
+
+ val interpret : theory -> model -> arguments -> Term.term -> interpretation * model * arguments (* exception CANNOT_INTERPRET *)
+ val is_satisfying_model : model -> interpretation -> bool -> PropLogic.prop_formula
+
+ val print : theory -> model -> Term.term -> interpretation -> (int -> bool) -> string
+ val print_model : theory -> model -> (int -> bool) -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Interface *)
+(* ------------------------------------------------------------------------- *)
+
+ val set_default_param : (string * string) -> theory -> theory
+ val get_default_param : theory -> string -> string option
+ val get_default_params : theory -> (string * string) list
+ val actual_params : theory -> (string * string) list -> (int * int * int * string)
+
+ val find_model : theory -> (int * int * int * string) -> Term.term -> bool -> unit
+
+ val satisfy_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model for a formula *)
+ val refute_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model that refutes a formula *)
+ val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
+
+ val setup : (theory -> theory) list
+end;
+
+structure Refute : REFUTE =
+struct
+
+ open PropLogic;
+
(* We use 'REFUTE' only for internal error conditions that should *)
(* never occur in the first place (i.e. errors caused by bugs in our *)
(* code). Otherwise (e.g. to indicate invalid input data) we use *)
(* 'error'. *)
-
- exception REFUTE of string * string; (* ("in function", "cause") *)
-
- val setup : (theory -> theory) list
-
- val set_default_param : (string * string) -> theory -> theory
- val get_default_param : theory -> string -> string option
- val get_default_params : theory -> (string * string) list
-
- val find_model : theory -> (string * string) list -> Term.term -> unit
-
- val refute_term : theory -> (string * string) list -> Term.term -> unit
- val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
-end;
-
-
-structure Refute : REFUTE =
-struct
- exception REFUTE of string * string;
-
- exception EMPTY_DATATYPE;
-
- structure RefuteDataArgs =
- struct
- val name = "Refute/refute";
- type T = string Symtab.table;
- val empty = Symtab.empty;
- val copy = I;
- val prep_ext = I;
- val merge =
- fn (symTable1, symTable2) =>
- (Symtab.merge (op=) (symTable1, symTable2));
- fun print sg symTable =
- writeln
- ("'refute', default parameters:\n" ^
- (space_implode "\n" (map (fn (name,value) => name ^ " = " ^ value) (Symtab.dest symTable))))
- end;
-
- structure RefuteData = TheoryDataFun(RefuteDataArgs);
-
-
-(* ------------------------------------------------------------------------- *)
-(* INTERFACE, PART 1: INITIALIZATION, PARAMETER MANAGEMENT *)
-(* ------------------------------------------------------------------------- *)
-
-(* ------------------------------------------------------------------------- *)
-(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
-(* structure *)
-(* ------------------------------------------------------------------------- *)
-
- val setup = [RefuteData.init];
-
-(* ------------------------------------------------------------------------- *)
-(* set_default_param: stores the '(name, value)' pair in RefuteData's symbol *)
-(* table *)
-(* ------------------------------------------------------------------------- *)
-
- fun set_default_param (name, value) thy =
- let
- val symTable = RefuteData.get thy
- in
- case Symtab.lookup (symTable, name) of
- None => RefuteData.put (Symtab.extend (symTable, [(name, value)])) thy
- | Some _ => RefuteData.put (Symtab.update ((name, value), symTable)) thy
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* get_default_param: retrieves the value associated with 'name' from *)
-(* RefuteData's symbol table *)
-(* ------------------------------------------------------------------------- *)
-
- fun get_default_param thy name = Symtab.lookup (RefuteData.get thy, name);
-
-(* ------------------------------------------------------------------------- *)
-(* get_default_params: returns a list of all '(name, value)' pairs that are *)
-(* stored in RefuteData's symbol table *)
-(* ------------------------------------------------------------------------- *)
-
- fun get_default_params thy = Symtab.dest (RefuteData.get thy);
-
-
-(* ------------------------------------------------------------------------- *)
-(* PROPOSITIONAL FORMULAS *)
-(* ------------------------------------------------------------------------- *)
-
-(* ------------------------------------------------------------------------- *)
-(* prop_formula: formulas of propositional logic, built from boolean *)
-(* variables (referred to by index) and True/False using *)
-(* not/or/and *)
-(* ------------------------------------------------------------------------- *)
-
- datatype prop_formula =
- True
- | False
- | BoolVar of int
- | Not of prop_formula
- | Or of prop_formula * prop_formula
- | And of prop_formula * prop_formula;
-
- (* the following constructor functions make sure that True and False do *)
- (* not occur within any of the other connectives (i.e. Not, Or, And) *)
-
- (* prop_formula -> prop_formula *)
-
- fun SNot True = False
- | SNot False = True
- | SNot fm = Not fm;
-
- (* prop_formula * prop_formula -> prop_formula *)
-
- fun SOr (True, _) = True
- | SOr (_, True) = True
- | SOr (False, fm) = fm
- | SOr (fm, False) = fm
- | SOr (fm1, fm2) = Or (fm1, fm2);
-
- (* prop_formula * prop_formula -> prop_formula *)
-
- fun SAnd (True, fm) = fm
- | SAnd (fm, True) = fm
- | SAnd (False, _) = False
- | SAnd (_, False) = False
- | SAnd (fm1, fm2) = And (fm1, fm2);
+ exception REFUTE of string * string; (* ("in function", "cause") *)
(* ------------------------------------------------------------------------- *)
-(* list_disjunction: computes the disjunction of a list of propositional *)
-(* formulas *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_formula list -> prop_formula *)
-
- fun list_disjunction [] = False
- | list_disjunction (x::xs) = SOr (x, list_disjunction xs);
-
-(* ------------------------------------------------------------------------- *)
-(* list_conjunction: computes the conjunction of a list of propositional *)
-(* formulas *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_formula list -> prop_formula *)
-
- fun list_conjunction [] = True
- | list_conjunction (x::xs) = SAnd (x, list_conjunction xs);
-
-(* ------------------------------------------------------------------------- *)
-(* prop_formula_dot_product: [x1,...,xn] * [y1,...,yn] -> x1*y1+...+xn*yn *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_formula list * prop_formula list -> prop_formula *)
-
- fun prop_formula_dot_product ([],[]) = False
- | prop_formula_dot_product (x::xs,y::ys) = SOr (SAnd (x,y), prop_formula_dot_product (xs,ys))
- | prop_formula_dot_product (_,_) = raise REFUTE ("prop_formula_dot_product", "lists are of different length");
-
-(* ------------------------------------------------------------------------- *)
-(* prop_formula_to_nnf: computes the negation normal form of a formula 'fm' *)
-(* of propositional logic (i.e. only variables may be *)
-(* negated, but not subformulas) *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_formula -> prop_formula *)
-
- fun prop_formula_to_nnf fm =
- case fm of
- (* constants *)
- True => True
- | False => False
- (* literals *)
- | BoolVar i => BoolVar i
- | Not (BoolVar i) => Not (BoolVar i)
- (* double-negation elimination *)
- | Not (Not fm) => prop_formula_to_nnf fm
- (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
- | Not (Or (fm1,fm2)) => SAnd (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
- | Not (And (fm1,fm2)) => SOr (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
- (* 'or' and 'and' as outermost connectives are left untouched *)
- | Or (fm1,fm2) => SOr (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
- | And (fm1,fm2) => SAnd (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
- (* 'not' + constant *)
- | Not _ => raise REFUTE ("prop_formula_to_nnf", "'True'/'False' not allowed inside of 'Not'");
-
-(* ------------------------------------------------------------------------- *)
-(* prop_formula_nnf_to_cnf: computes the conjunctive normal form of a *)
-(* formula 'fm' of propositional logic that is given in negation normal *)
-(* form. Note that there may occur an exponential blowup of the *)
-(* formula. *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_formula -> prop_formula *)
-
- fun prop_formula_nnf_to_cnf fm =
- case fm of
- (* constants *)
- True => True
- | False => False
- (* literals *)
- | BoolVar i => BoolVar i
- | Not (BoolVar i) => Not (BoolVar i)
- (* pushing 'or' inside of 'and' using distributive laws *)
- | Or (fm1,fm2) =>
- let
- val fm1' = prop_formula_nnf_to_cnf fm1
- val fm2' = prop_formula_nnf_to_cnf fm2
- in
- case fm1' of
- And (fm11,fm12) => prop_formula_nnf_to_cnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2')))
- | _ =>
- (case fm2' of
- And (fm21,fm22) => prop_formula_nnf_to_cnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22)))
- (* neither subformula contains 'and' *)
- | _ => fm)
- end
- (* 'and' as outermost connective is left untouched *)
- | And (fm1,fm2) => SAnd (prop_formula_nnf_to_cnf fm1, prop_formula_nnf_to_cnf fm2)
- (* error *)
- | _ => raise REFUTE ("prop_formula_nnf_to_cnf", "formula is not in negation normal form");
-
-(* ------------------------------------------------------------------------- *)
-(* max: computes the maximum of two integer values 'i' and 'j' *)
-(* ------------------------------------------------------------------------- *)
-
- (* int * int -> int *)
-
- fun max (i,j) =
- if (i>j) then i else j;
-
-(* ------------------------------------------------------------------------- *)
-(* max_var_index: computes the maximal variable index occuring in 'fm', *)
-(* where 'fm' is a formula of propositional logic *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_formula -> int *)
-
- fun max_var_index fm =
- case fm of
- True => 0
- | False => 0
- | BoolVar i => i
- | Not fm1 => max_var_index fm1
- | And (fm1,fm2) => max (max_var_index fm1, max_var_index fm2)
- | Or (fm1,fm2) => max (max_var_index fm1, max_var_index fm2);
-
-(* ------------------------------------------------------------------------- *)
-(* prop_formula_nnf_to_def_cnf: computes the definitional conjunctive normal *)
-(* form of a formula 'fm' of propositional logic that is given in *)
-(* negation normal form. To avoid an exponential blowup of the *)
-(* formula, auxiliary variables may be introduced. The result formula *)
-(* is SAT-equivalent to 'fm' (i.e. it is satisfiable if and only if *)
-(* 'fm' is satisfiable). *)
+(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *)
(* ------------------------------------------------------------------------- *)
- (* prop_formula -> prop_formula *)
-
- fun prop_formula_nnf_to_def_cnf fm =
- let
- (* prop_formula * int -> prop_formula * int *)
- fun prop_formula_nnf_to_def_cnf_new (fm,new) =
- (* 'new' specifies the next index that is available to introduce an auxiliary variable *)
- case fm of
- (* constants *)
- True => (True, new)
- | False => (False, new)
- (* literals *)
- | BoolVar i => (BoolVar i, new)
- | Not (BoolVar i) => (Not (BoolVar i), new)
- (* pushing 'or' inside of 'and' using distributive laws *)
- | Or (fm1,fm2) =>
- let
- val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
- val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
- in
- case fst fm1' of
- And (fm11,fm12) =>
- let
- val aux = BoolVar (snd fm2')
- in
- (* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *)
- prop_formula_nnf_to_def_cnf_new (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fst fm2', Not aux)), (snd fm2')+1)
- end
- | _ =>
- (case fst fm2' of
- And (fm21,fm22) =>
- let
- val aux = BoolVar (snd fm2')
- in
- (* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *)
- prop_formula_nnf_to_def_cnf_new (SAnd (SOr (fst fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), (snd fm2')+1)
- end
- (* neither subformula contains 'and' *)
- | _ => (fm, new))
- end
- (* 'and' as outermost connective is left untouched *)
- | And (fm1,fm2) =>
- let
- val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
- val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
- in
- (SAnd (fst fm1', fst fm2'), snd fm2')
- end
- (* error *)
- | _ => raise REFUTE ("prop_formula_nnf_to_def_cnf", "formula is not in negation normal form")
- in
- fst (prop_formula_nnf_to_def_cnf_new (fm, (max_var_index fm)+1))
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* prop_formula_to_cnf: computes the conjunctive normal form of a formula *)
-(* 'fm' of propositional logic *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_formula -> prop_formula *)
-
- fun prop_formula_to_cnf fm =
- prop_formula_nnf_to_cnf (prop_formula_to_nnf fm);
-
-(* ------------------------------------------------------------------------- *)
-(* prop_formula_to_def_cnf: computes the definitional conjunctive normal *)
-(* form of a formula 'fm' of propositional logic, introducing auxiliary *)
-(* variables if necessary to avoid an exponential blowup of the formula *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_formula -> prop_formula *)
-
- fun prop_formula_to_def_cnf fm =
- prop_formula_nnf_to_def_cnf (prop_formula_to_nnf fm);
-
-(* ------------------------------------------------------------------------- *)
-(* prop_formula_to_dimacs_cnf_format: serializes a formula of propositional *)
-(* logic to a file in DIMACS CNF format (see "Satisfiability Suggested *)
-(* Format", May 8 1993, Section 2.1) *)
-(* fm : formula to be serialized. Note: 'fm' must not contain a variable *)
-(* index less than 1. *)
-(* def : If true, translate 'fm' into definitional CNF. Otherwise translate *)
-(* 'fm' into CNF. *)
-(* path: path of the file to be created *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_formula -> bool -> Path.T -> unit *)
-
- fun prop_formula_to_dimacs_cnf_format fm def path =
- let
- (* prop_formula *)
- val cnf =
- if def then
- prop_formula_to_def_cnf fm
- else
- prop_formula_to_cnf fm
- val fm' =
- case cnf of
- True => Or (BoolVar 1, Not (BoolVar 1))
- | False => And (BoolVar 1, Not (BoolVar 1))
- | _ => cnf (* either 'cnf'=True/False, or 'cnf' does not contain True/False at all *)
- (* prop_formula -> int *)
- fun cnf_number_of_clauses (And (fm1,fm2)) =
- (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
- | cnf_number_of_clauses _ =
- 1
- (* prop_formula -> string *)
- fun cnf_prop_formula_to_string (BoolVar i) =
- if (i<1) then
- raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains a variable index less than 1")
- else
- (string_of_int i)
- | cnf_prop_formula_to_string (Not fm1) =
- "-" ^ (cnf_prop_formula_to_string fm1)
- | cnf_prop_formula_to_string (Or (fm1,fm2)) =
- (cnf_prop_formula_to_string fm1) ^ " " ^ (cnf_prop_formula_to_string fm2)
- | cnf_prop_formula_to_string (And (fm1,fm2)) =
- (cnf_prop_formula_to_string fm1) ^ " 0\n" ^ (cnf_prop_formula_to_string fm2)
- | cnf_prop_formula_to_string _ =
- raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains True/False")
- in
- File.write path ("c This file was generated by prop_formula_to_dimacs_cnf_format\n"
- ^ "c (c) Tjark Weber\n"
- ^ "p cnf " ^ (string_of_int (max_var_index fm')) ^ " " ^ (string_of_int (cnf_number_of_clauses fm')) ^ "\n"
- ^ (cnf_prop_formula_to_string fm') ^ "\n")
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* prop_formula_to_dimacs_sat_format: serializes a formula of propositional *)
-(* logic to a file in DIMACS SAT format (see "Satisfiability Suggested *)
-(* Format", May 8 1993, Section 2.2) *)
-(* fm : formula to be serialized. Note: 'fm' must not contain a variable *)
-(* index less than 1. *)
-(* path: path of the file to be created *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_formula -> Path.T -> unit *)
-
- fun prop_formula_to_dimacs_sat_format fm path =
- let
- fun prop_formula_to_string True =
- "*()"
- | prop_formula_to_string False =
- "+()"
- | prop_formula_to_string (BoolVar i) =
- if (i<1) then
- raise REFUTE ("prop_formula_to_dimacs_sat_format", "formula contains a variable index less than 1")
- else
- (string_of_int i)
- | prop_formula_to_string (Not fm1) =
- "-(" ^ (prop_formula_to_string fm1) ^ ")"
- | prop_formula_to_string (Or (fm1,fm2)) =
- "+(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
- | prop_formula_to_string (And (fm1,fm2)) =
- "*(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
- in
- File.write path ("c This file was generated by prop_formula_to_dimacs_sat_format\n"
- ^ "c (c) Tjark Weber\n"
- ^ "p sat " ^ (string_of_int (max (max_var_index fm, 1))) ^ "\n"
- ^ "(" ^ (prop_formula_to_string fm) ^ ")\n")
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* prop_formula_sat_solver: try to find a satisfying assignment for the *)
-(* boolean variables in a propositional formula, using an external SAT *)
-(* solver. If the SAT solver did not find an assignment, 'None' is *)
-(* returned. Otherwise 'Some (list of integers)' is returned, where *)
-(* i>0 means that the boolean variable i is set to TRUE, and i<0 means *)
-(* that the boolean variable i is set to FALSE. Note that if *)
-(* 'satformat' is 'defcnf', then the assignment returned may contain *)
-(* auxiliary variables that were not present in the original formula *)
-(* 'fm'. *)
-(* fm : formula that is passed to the SAT solver *)
-(* satpath : path of the file used to store the propositional formula, *)
-(* i.e. the input to the SAT solver *)
-(* satformat : format of the SAT solver's input file. Must be either "cnf", *)
-(* "defcnf", or "sat". *)
-(* resultpath: path of the file containing the SAT solver's output *)
-(* success : part of the line in the SAT solver's output that is followed *)
-(* by a line consisting of a list of integers representing the *)
-(* satisfying assignment *)
-(* command : system command used to execute the SAT solver *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_formula -> Path.T -> string -> Path.T -> string -> string -> int list option *)
-
- fun prop_formula_sat_solver fm satpath satformat resultpath success command =
- if File.exists satpath then
- error ("file '" ^ (Path.pack satpath) ^ "' exists, please delete (will not overwrite)")
- else if File.exists resultpath then
- error ("file '" ^ (Path.pack resultpath) ^ "' exists, please delete (will not overwrite)")
- else
- (
- (* serialize the formula 'fm' to a file *)
- if satformat="cnf" then
- prop_formula_to_dimacs_cnf_format fm false satpath
- else if satformat="defcnf" then
- prop_formula_to_dimacs_cnf_format fm true satpath
- else if satformat="sat" then
- prop_formula_to_dimacs_sat_format fm satpath
- else
- error ("invalid argument: satformat='" ^ satformat ^ "' (must be either 'cnf', 'defcnf', or 'sat')");
- (* execute SAT solver *)
- if (system command)<>0 then
- (
- (* error executing SAT solver *)
- File.rm satpath;
- File.rm resultpath;
- error ("system command '" ^ command ^ "' failed (make sure a SAT solver is installed)")
- )
- else
- (
- (* read assignment from the result file *)
- File.rm satpath;
- let
- (* 'a option -> 'a Library.option *)
- fun option (SOME a) =
- Some a
- | option NONE =
- None
- (* string -> int list *)
- fun string_to_int_list s =
- mapfilter (option o Int.fromString) (space_explode " " s)
- (* string -> string -> bool *)
- fun is_substring s1 s2 =
- let
- val length1 = String.size s1
- val length2 = String.size s2
- in
- if length2 < length1 then
- false
- else if s1 = String.substring (s2, 0, length1) then
- true
- else is_substring s1 (String.substring (s2, 1, length2-1))
- end
- (* string list -> int list option *)
- fun extract_solution [] =
- None
- | extract_solution (line::lines) =
- if is_substring success line then
- (* the next line must be a list of integers *)
- Some (string_to_int_list (hd lines))
- else
- extract_solution lines
- val sat_result = File.read resultpath
- in
- File.rm resultpath;
- extract_solution (split_lines sat_result)
- end
- )
- );
-
+ exception CANNOT_INTERPRET;
(* ------------------------------------------------------------------------- *)
(* TREES *)
@@ -537,9 +88,6 @@
Leaf of 'a
| Node of ('a tree) list;
- type prop_tree =
- prop_formula list tree;
-
(* ('a -> 'b) -> 'a tree -> 'b tree *)
fun tree_map f tr =
@@ -571,45 +119,95 @@
Node ys => Node (map tree_pair (xs ~~ ys))
| Leaf _ => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
+
(* ------------------------------------------------------------------------- *)
-(* prop_tree_to_true: returns a propositional formula that is true iff the *)
-(* tree denotes the boolean value TRUE *)
+(* interpretation: a term's interpretation is given by a variable of type *)
+(* 'interpretation' *)
(* ------------------------------------------------------------------------- *)
- (* prop_tree -> prop_formula *)
-
- (* a term of type 'bool' is represented as a 2-element leaf, where *)
- (* the term is true iff the leaf's first element is true *)
-
- fun prop_tree_to_true (Leaf [fm,_]) =
- fm
- | prop_tree_to_true _ =
- raise REFUTE ("prop_tree_to_true", "tree is not a 2-element leaf");
+ type interpretation =
+ prop_formula list tree;
(* ------------------------------------------------------------------------- *)
-(* prop_tree_to_false: returns a propositional formula that is true iff the *)
-(* tree denotes the boolean value FALSE *)
+(* model: a model specifies the size of types and the interpretation of *)
+(* terms *)
(* ------------------------------------------------------------------------- *)
- (* prop_tree -> prop_formula *)
+ type model =
+ (Term.typ * int) list * (Term.term * interpretation) list;
- (* a term of type 'bool' is represented as a 2-element leaf, where *)
- (* the term is false iff the leaf's second element is true *)
+(* ------------------------------------------------------------------------- *)
+(* arguments: additional arguments required during interpretation of terms *)
+(* ------------------------------------------------------------------------- *)
+
+ type arguments =
+ {next_idx: int, bounds: interpretation list, wellformed: prop_formula};
+
- fun prop_tree_to_false (Leaf [_,fm]) =
- fm
- | prop_tree_to_false _ =
- raise REFUTE ("prop_tree_to_false", "tree is not a 2-element leaf");
+ structure RefuteDataArgs =
+ struct
+ val name = "HOL/refute";
+ type T =
+ {interpreters: (string * (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option)) list,
+ printers: (string * (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option)) list,
+ parameters: string Symtab.table};
+ val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
+ val copy = I;
+ val prep_ext = I;
+ fun merge
+ ({interpreters = in1, printers = pr1, parameters = pa1},
+ {interpreters = in2, printers = pr2, parameters = pa2}) =
+ {interpreters = rev (merge_alists (rev in1) (rev in2)),
+ printers = rev (merge_alists (rev pr1) (rev pr2)),
+ parameters = Symtab.merge (op=) (pa1, pa2)};
+ fun print sg {interpreters, printers, parameters} =
+ Pretty.writeln (Pretty.chunks
+ [Pretty.strs ("default parameters:" :: flat (map (fn (name,value) => [name, "=", value]) (Symtab.dest parameters))),
+ Pretty.strs ("interpreters:" :: map fst interpreters),
+ Pretty.strs ("printers:" :: map fst printers)]);
+ end;
+
+ structure RefuteData = TheoryDataFun(RefuteDataArgs);
+
(* ------------------------------------------------------------------------- *)
-(* restrict_to_single_element: returns a propositional formula which is true *)
-(* iff the tree 'tr' describes a single element of its corresponding *)
-(* type, i.e. iff at each leaf, one and only one formula is true *)
+(* interpret: tries to interpret the term 't' using a suitable interpreter; *)
+(* returns the interpretation and a (possibly extended) model *)
+(* that keeps track of the interpretation of subterms *)
+(* Note: exception 'CANNOT_INTERPRETE' is raised if the term cannot be *)
+(* interpreted by any interpreter *)
(* ------------------------------------------------------------------------- *)
- (* prop_tree -> prop_formula *)
+ (* theory -> model -> arguments -> Term.term -> interpretation * model * arguments *)
+
+ fun interpret thy model args t =
+ (case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of
+ None =>
+ (std_output "\n"; warning ("Unable to interpret term:\n" ^ Sign.string_of_term (sign_of thy) t);
+ raise CANNOT_INTERPRET)
+ | Some x => x);
+
+(* ------------------------------------------------------------------------- *)
+(* print: tries to print the constant denoted by the term 't' using a *)
+(* suitable printer *)
+(* ------------------------------------------------------------------------- *)
- fun restrict_to_single_element tr =
+ (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string *)
+
+ fun print thy model t intr assignment =
+ (case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) of
+ None => "<<no printer available>>"
+ | Some s => s);
+
+(* ------------------------------------------------------------------------- *)
+(* is_satisfying_model: returns a propositional formula that is true iff the *)
+(* given interpretation denotes 'satisfy', and the model meets certain *)
+(* well-formedness properties *)
+(* ------------------------------------------------------------------------- *)
+
+ (* model -> interpretation -> bool -> PropLogic.prop_formula *)
+
+ fun is_satisfying_model model intr satisfy =
let
(* prop_formula list -> prop_formula *)
fun allfalse [] = True
@@ -617,290 +215,1347 @@
(* prop_formula list -> prop_formula *)
fun exactly1true [] = False
| exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
+ (* ------------------------------------------------------------------------- *)
+ (* restrict_to_single_element: returns a propositional formula that is true *)
+ (* iff the interpretation denotes a single element of its corresponding *)
+ (* type, i.e. iff at each leaf, one and only one formula is true *)
+ (* ------------------------------------------------------------------------- *)
+ (* interpretation -> prop_formula *)
+ fun restrict_to_single_element (Leaf [BoolVar i, Not (BoolVar j)]) =
+ if (i=j) then
+ True (* optimization for boolean variables *)
+ else
+ raise REFUTE ("is_satisfying_model", "boolean variables in leaf have different indices")
+ | restrict_to_single_element (Leaf xs) =
+ exactly1true xs
+ | restrict_to_single_element (Node trees) =
+ PropLogic.all (map restrict_to_single_element trees)
in
- case tr of
- Leaf [BoolVar _, Not (BoolVar _)] => True (* optimization for boolean variables *)
- | Leaf xs => exactly1true xs
- | Node trees => list_conjunction (map restrict_to_single_element trees)
+ (* a term of type 'bool' is represented as a 2-element leaf, where *)
+ (* the term is true iff the leaf's first element is true, and false *)
+ (* iff the leaf's second element is true *)
+ case intr of
+ Leaf [fmT,fmF] =>
+ (* well-formedness properties and formula 'fmT'/'fmF' *)
+ SAnd (PropLogic.all (map (restrict_to_single_element o snd) (snd model)), if satisfy then fmT else fmF)
+ | _ =>
+ raise REFUTE ("is_satisfying_model", "interpretation does not denote a boolean value")
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* print_model: turns the model into a string, using a fixed interpretation *)
+(* (given by an assignment for boolean variables) and suitable *)
+(* printers *)
+(* ------------------------------------------------------------------------- *)
+
+ fun print_model thy model assignment =
+ let
+ val (typs, terms) = model
+ in
+ (if null typs then
+ "empty universe (no type variables in term)"
+ else
+ "Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs))
+ ^ "\n"
+ ^ (if null terms then
+ "empty interpretation (no free variables in term)"
+ else
+ space_implode "\n" (map
+ (fn (t,intr) =>
+ Sign.string_of_term (sign_of thy) t ^ ": " ^ print thy model t intr assignment)
+ terms)
+ )
+ ^ "\n"
+ end;
+
+
+(* ------------------------------------------------------------------------- *)
+(* PARAMETER MANAGEMENT *)
+(* ------------------------------------------------------------------------- *)
+
+ (* string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory *)
+
+ fun add_interpreter name f thy =
+ let
+ val {interpreters, printers, parameters} = RefuteData.get thy
+ in
+ case assoc (interpreters, name) of
+ None => RefuteData.put {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} thy
+ | Some _ => error ("Interpreter " ^ name ^ " already declared")
+ end;
+
+ (* string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory *)
+
+ fun add_printer name f thy =
+ let
+ val {interpreters, printers, parameters} = RefuteData.get thy
+ in
+ case assoc (printers, name) of
+ None => RefuteData.put {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} thy
+ | Some _ => error ("Printer " ^ name ^ " already declared")
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* set_default_param: stores the '(name, value)' pair in RefuteData's *)
+(* parameter table *)
+(* ------------------------------------------------------------------------- *)
+
+ (* (string * string) -> theory -> theory *)
+
+ fun set_default_param (name, value) thy =
+ let
+ val {interpreters, printers, parameters} = RefuteData.get thy
+ in
+ case Symtab.lookup (parameters, name) of
+ None => RefuteData.put
+ {interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy
+ | Some _ => RefuteData.put
+ {interpreters = interpreters, printers = printers, parameters = Symtab.update ((name, value), parameters)} thy
end;
(* ------------------------------------------------------------------------- *)
-(* HOL FORMULAS *)
+(* get_default_param: retrieves the value associated with 'name' from *)
+(* RefuteData's parameter table *)
+(* ------------------------------------------------------------------------- *)
+
+ (* theory -> string -> string option *)
+
+ fun get_default_param thy name = Symtab.lookup ((#parameters o RefuteData.get) thy, name);
+
+(* ------------------------------------------------------------------------- *)
+(* get_default_params: returns a list of all '(name, value)' pairs that are *)
+(* stored in RefuteData's parameter table *)
+(* ------------------------------------------------------------------------- *)
+
+ (* theory -> (string * string) list *)
+
+ fun get_default_params thy = (Symtab.dest o #parameters o RefuteData.get) thy;
+
+(* ------------------------------------------------------------------------- *)
+(* actual_params: takes a (possibly empty) list 'params' of parameters that *)
+(* override the default parameters currently specified in 'thy', and *)
+(* returns a tuple that can be passed to 'find_model'. *)
+(* *)
+(* The following parameters are supported (and required!): *)
+(* *)
+(* Name Type Description *)
+(* *)
+(* "minsize" int Only search for models with size at least *)
+(* 'minsize'. *)
+(* "maxsize" int If >0, only search for models with size at most *)
+(* 'maxsize'. *)
+(* "maxvars" int If >0, use at most 'maxvars' boolean variables *)
+(* when transforming the term into a propositional *)
+(* formula. *)
+(* "satsolver" string SAT solver to be used. *)
+(* ------------------------------------------------------------------------- *)
+
+ (* theory -> (string * string) list -> (int * int * int * string) *)
+
+ fun actual_params thy params =
+ let
+ (* (string * string) list * string -> int *)
+ fun read_int (parms, name) =
+ case assoc_string (parms, name) of
+ Some s => (case Int.fromString s of
+ SOME i => i
+ | NONE => error ("parameter " ^ quote name ^ " (value is " ^ quote s ^ ") must be an integer value"))
+ | None => error ("parameter " ^ quote name ^ " must be assigned a value")
+ (* (string * string) list * string -> string *)
+ fun read_string (parms, name) =
+ case assoc_string (parms, name) of
+ Some s => s
+ | None => error ("parameter " ^ quote name ^ " must be assigned a value")
+ (* (string * string) list *)
+ val allparams = params @ (get_default_params thy) (* 'params' first, defaults last (to override) *)
+ (* int *)
+ val minsize = read_int (allparams, "minsize")
+ val maxsize = read_int (allparams, "maxsize")
+ val maxvars = read_int (allparams, "maxvars")
+ (* string *)
+ val satsolver = read_string (allparams, "satsolver")
+ in
+ (minsize, maxsize, maxvars, satsolver)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* find_model: repeatedly calls 'invoke_propgen' with appropriate *)
+(* parameters, applies the SAT solver, and (in case a model is *)
+(* found) displays the model to the user *)
+(* thy : the current theory *)
+(* minsize : the minimal size of the model *)
+(* maxsize : the maximal size of the model *)
+(* maxvars : the maximal number of boolean variables to be used *)
+(* satsolver: the name of the SAT solver to be used *)
+(* satisfy : if 'True', search for a model that makes 't' true; otherwise *)
+(* search for a model that makes 't' false *)
+(* ------------------------------------------------------------------------- *)
+
+ (* theory -> (int * int * int * string) -> Term.term -> bool -> unit *)
+
+ fun find_model thy (minsize, maxsize, maxvars, satsolver) t satisfy =
+ let
+ (* Term.typ list *)
+ val tvars = map (fn (i,s) => TVar(i,s)) (term_tvars t)
+ val tfrees = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
+ (* int -> unit *)
+ fun find_model_loop size =
+ (* 'maxsize=0' means "search for arbitrary large models" *)
+ if size>maxsize andalso maxsize<>0 then
+ writeln ("Search terminated: maxsize=" ^ string_of_int maxsize ^ " exceeded.")
+ else
+ let
+ (* ------------------------------------------------------------------------- *)
+ (* make_universes: given a list 'xs' of "types" and a universe size 'size', *)
+ (* this function returns all possible partitions of the universe into *)
+ (* the "types" in 'xs' such that no "type" is empty. If 'size' is less *)
+ (* than 'length xs', the returned list of partitions is empty. *)
+ (* Otherwise, if the list 'xs' is empty, then the returned list of *)
+ (* partitions contains only the empty list, regardless of 'size'. *)
+ (* ------------------------------------------------------------------------- *)
+ (* 'a list -> int -> ('a * int) list list *)
+ fun make_universes xs size =
+ let
+ (* 'a list -> int -> int -> ('a * int) list list *)
+ fun make_partitions_loop (x::xs) 0 total =
+ map (fn us => ((x,0)::us)) (make_partitions xs total)
+ | make_partitions_loop (x::xs) first total =
+ (map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
+ | make_partitions_loop _ _ _ =
+ raise REFUTE ("find_model", "empty list (in make_partitions_loop)")
+ and
+ (* 'a list -> int -> ('a * int) list list *)
+ make_partitions [x] size =
+ (* we must use all remaining elements on the type 'x', so there is only one partition *)
+ [[(x,size)]]
+ | make_partitions (x::xs) 0 =
+ (* there are no elements left in the universe, so there is only one partition *)
+ [map (fn t => (t,0)) (x::xs)]
+ | make_partitions (x::xs) size =
+ (* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
+ make_partitions_loop (x::xs) size size
+ | make_partitions _ _ =
+ raise REFUTE ("find_model", "empty list (in make_partitions)")
+ val len = length xs
+ in
+ if size<len then
+ (* the universe isn't big enough to make every type non-empty *)
+ []
+ else if xs=[] then
+ (* no types: return one universe, regardless of the size *)
+ [[]]
+ else
+ (* partition into possibly empty types, then add 1 element to each type *)
+ map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
+ end
+ (* ('a * int) list -> bool *)
+ fun find_interpretation xs =
+ let
+ val init_model = (xs, [])
+ val init_args = {next_idx = 1, bounds = [], wellformed = True}
+ val (intr, model, args) = interpret thy init_model init_args t
+ val fm = SAnd (#wellformed args, is_satisfying_model model intr satisfy)
+ val usedvars = maxidx fm
+ in
+ (* 'maxvars=0' means "use as many variables as necessary" *)
+ if usedvars>maxvars andalso maxvars<>0 then
+ (writeln ("\nSearch terminated: " ^ string_of_int usedvars ^ " boolean variables used (only " ^ string_of_int maxvars ^ " allowed).");
+ true)
+ else
+ (
+ std_output " invoking SAT solver...";
+ case SatSolver.invoke_solver satsolver fm of
+ None =>
+ (std_output " no model found.\n";
+ false)
+ | Some assignment =>
+ (writeln ("\nModel found:\n" ^ print_model thy model assignment);
+ true)
+ )
+ end handle CANNOT_INTERPRET => true
+ (* TODO: change this to false once the ability to interpret terms depends on the universe *)
+ in
+ case make_universes (tvars@tfrees) size of
+ [] =>
+ (writeln ("Searching for a model of size " ^ string_of_int size ^ ": cannot make every type non-empty (model is too small).");
+ find_model_loop (size+1))
+ | [[]] =>
+ (std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term...");
+ if find_interpretation [] then
+ ()
+ else
+ writeln ("Search terminated: no type variables in term."))
+ | us =>
+ let
+ fun loop [] =
+ find_model_loop (size+1)
+ | loop (u::us) =
+ (std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term...");
+ if find_interpretation u then () else loop us)
+ in
+ loop us
+ end
+ end
+ in
+ writeln ("Trying to find a model that "
+ ^ (if satisfy then "satisfies" else "refutes")
+ ^ ": " ^ (Sign.string_of_term (sign_of thy) t));
+ if minsize<1 then
+ writeln "\"minsize\" is less than 1; starting search with size 1."
+ else ();
+ find_model_loop (Int.max (minsize,1))
+ end;
+
+
+(* ------------------------------------------------------------------------- *)
+(* INTERFACE, PART 2: FINDING A MODEL *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
-(* absvar: form an abstraction over a schematic variable *)
-(* ------------------------------------------------------------------------- *)
-
- (* Term.indexname * Term.typ * Term.term -> Term.term *)
-
- (* this function is similar to Term.absfree, but for schematic *)
- (* variables (rather than free variables) *)
- fun absvar ((x,i),T,body) =
- Abs(x, T, abstract_over (Var((x,i),T), body));
-
-(* ------------------------------------------------------------------------- *)
-(* list_all_var: quantification over a list of schematic variables *)
+(* satisfy_term: calls 'find_model' to find a model that satisfies 't' *)
+(* params : list of '(name, value)' pairs used to override default *)
+(* parameters *)
(* ------------------------------------------------------------------------- *)
- (* (Term.indexname * Term.typ) list * Term.term -> Term.term *)
-
- (* this function is similar to Term.list_all_free, but for schematic *)
- (* variables (rather than free variables) *)
- fun list_all_var ([], t) =
- t
- | list_all_var ((idx,T)::vars, t) =
- (all T) $ (absvar(idx, T, list_all_var(vars,t)));
+ (* theory -> (string * string) list -> Term.term -> unit *)
-(* ------------------------------------------------------------------------- *)
-(* close_vars: close up a formula over all schematic variables by *)
-(* quantification (note that the result term may still contain *)
-(* (non-schematic) free variables) *)
-(* ------------------------------------------------------------------------- *)
-
- (* Term.term -> Term.term *)
-
- (* this function is similar to Logic.close_form, but for schematic *)
- (* variables (rather than free variables) *)
- fun close_vars A =
- list_all_var (sort_wrt (fst o fst) (map dest_Var (term_vars A)), A);
+ fun satisfy_term thy params t =
+ find_model thy (actual_params thy params) t true;
(* ------------------------------------------------------------------------- *)
-(* make_universes: given a list 'xs' of "types" and a universe size 'size', *)
-(* this function returns all possible partitions of the universe into *)
-(* the "types" in 'xs' such that no "type" is empty. If 'size' is less *)
-(* than 'length xs', the returned list of partitions is empty. *)
-(* Otherwise, if the list 'xs' is empty, then the returned list of *)
-(* partitions contains only the empty list, regardless of 'size'. *)
+(* refute_term: calls 'find_model' to find a model that refutes 't' *)
+(* params : list of '(name, value)' pairs used to override default *)
+(* parameters *)
(* ------------------------------------------------------------------------- *)
- (* 'a list -> int -> ('a * int) list list *)
+ (* theory -> (string * string) list -> Term.term -> unit *)
- fun make_universes xs size =
+ fun refute_term thy params t =
let
- (* 'a list -> int -> int -> ('a * int) list list *)
- fun make_partitions_loop (x::xs) 0 total =
- map (fn us => ((x,0)::us)) (make_partitions xs total)
- | make_partitions_loop (x::xs) first total =
- (map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
- | make_partitions_loop _ _ _ =
- raise REFUTE ("make_universes::make_partitions_loop", "empty list")
- and
- (* 'a list -> int -> ('a * int) list list *)
- make_partitions [x] size =
- (* we must use all remaining elements on the type 'x', so there is only one partition *)
- [[(x,size)]]
- | make_partitions (x::xs) 0 =
- (* there are no elements left in the universe, so there is only one partition *)
- [map (fn t => (t,0)) (x::xs)]
- | make_partitions (x::xs) size =
- (* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
- make_partitions_loop (x::xs) size size
- | make_partitions _ _ =
- raise REFUTE ("make_universes::make_partitions", "empty list")
- val len = length xs
+ (* disallow schematic type variables, since we cannot properly negate terms containing them *)
+ val _ = assert (null (term_tvars t)) "Term to be refuted contains schematic type variables"
+ (* existential closure over schematic variables *)
+ (* (Term.indexname * Term.typ) list *)
+ val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
+ (* Term.term *)
+ val ex_closure = foldl
+ (fn (t', ((x,i),T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
+ (t, vars)
+ (* If 't' is of type 'propT' (rather than 'boolT'), applying *)
+ (* 'HOLogic.exists_const' is not type-correct. However, this *)
+ (* isn't really a problem as long as 'find_model' still *)
+ (* interprets the resulting term correctly, without checking *)
+ (* its type. *)
in
- if size<len then
- (* the universe isn't big enough to make every type non-empty *)
- []
- else if xs=[] then
- (* no types: return one universe, regardless of the size *)
- [[]]
- else
- (* partition into possibly empty types, then add 1 element to each type *)
- map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
+ find_model thy (actual_params thy params) ex_closure false
end;
(* ------------------------------------------------------------------------- *)
-(* sum: computes the sum of a list of integers; sum [] = 0 *)
-(* ------------------------------------------------------------------------- *)
-
- (* int list -> int *)
-
- fun sum xs = foldl op+ (0, xs);
-
-(* ------------------------------------------------------------------------- *)
-(* product: computes the product of a list of integers; product [] = 1 *)
+(* refute_subgoal: calls 'refute_term' on a specific subgoal *)
+(* params : list of '(name, value)' pairs used to override default *)
+(* parameters *)
+(* subgoal : 0-based index specifying the subgoal number *)
(* ------------------------------------------------------------------------- *)
- (* int list -> int *)
-
- fun product xs = foldl op* (1, xs);
+ (* theory -> (string * string) list -> Thm.thm -> int -> unit *)
-(* ------------------------------------------------------------------------- *)
-(* power: power(a,b) computes a^b, for a>=0, b>=0 *)
-(* ------------------------------------------------------------------------- *)
+ fun refute_subgoal thy params thm subgoal =
+ refute_term thy params (nth_elem (subgoal, prems_of thm));
- (* int * int -> int *)
-
- fun power (a,0) = 1
- | power (a,1) = a
- | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end;
(* ------------------------------------------------------------------------- *)
-(* size_of_type: returns the size of a type, where 'us' specifies the size *)
-(* of each basic type (i.e. each type variable), and 'cdepth' specifies *)
-(* the maximal constructor depth for inductive datatypes *)
+(* INTERPRETERS *)
(* ------------------------------------------------------------------------- *)
- (* Term.typ -> (Term.typ * int) list -> theory -> int -> int *)
+ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
- fun size_of_type T us thy cdepth =
+ fun var_typevar_interpreter thy model args t =
let
- (* Term.typ -> (Term.typ * int) -> int *)
- fun lookup_size T [] =
- raise REFUTE ("size_of_type", "no size specified for type variable '" ^ (Sign.string_of_typ (sign_of thy) T) ^ "'")
- | lookup_size T ((typ,size)::pairs) =
- if T=typ then size else lookup_size T pairs
+ fun is_var (Free _) = true
+ | is_var (Var _) = true
+ | is_var _ = false
+ fun typeof (Free (_,T)) = T
+ | typeof (Var (_,T)) = T
+ | typeof _ = raise REFUTE ("var_typevar_interpreter", "term is not a variable")
+ fun is_typevar (TFree _) = true
+ | is_typevar (TVar _) = true
+ | is_typevar _ = false
+ val (sizes, intrs) = model
+ in
+ if is_var t andalso is_typevar (typeof t) then
+ (case assoc (intrs, t) of
+ Some intr => Some (intr, model, args)
+ | None =>
+ let
+ val size = (the o assoc) (sizes, typeof t) (* the model MUST specify a size for type variables *)
+ val idx = #next_idx args
+ val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1))))
+ val next = (if size=2 then idx+1 else idx+size)
+ in
+ (* extend the model, increase 'next_idx' *)
+ Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args})
+ end)
+ else
+ None
+ end;
+
+ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
+
+ fun var_funtype_interpreter thy model args t =
+ let
+ fun is_var (Free _) = true
+ | is_var (Var _) = true
+ | is_var _ = false
+ fun typeof (Free (_,T)) = T
+ | typeof (Var (_,T)) = T
+ | typeof _ = raise REFUTE ("var_funtype_interpreter", "term is not a variable")
+ fun stringof (Free (x,_)) = x
+ | stringof (Var ((x,_), _)) = x
+ | stringof _ = raise REFUTE ("var_funtype_interpreter", "term is not a variable")
+ fun is_funtype (Type ("fun", [_,_])) = true
+ | is_funtype _ = false
+ val (sizes, intrs) = model
in
- case T of
- Type ("prop", []) => 2
- | Type ("bool", []) => 2
- | Type ("Product_Type.unit", []) => 1
- | Type ("+", [T1,T2]) => (size_of_type T1 us thy cdepth) + (size_of_type T2 us thy cdepth)
- | Type ("*", [T1,T2]) => (size_of_type T1 us thy cdepth) * (size_of_type T2 us thy cdepth)
- | Type ("fun", [T1,T2]) => power (size_of_type T2 us thy cdepth, size_of_type T1 us thy cdepth)
- | Type ("set", [T1]) => size_of_type (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
- | Type (s, Ts) =>
- (case DatatypePackage.datatype_info thy s of
- Some info => (* inductive datatype *)
- if cdepth>0 then
+ if is_var t andalso is_funtype (typeof t) then
+ (case assoc (intrs, t) of
+ Some intr => Some (intr, model, args)
+ | None =>
+ let
+ val T1 = domain_type (typeof t)
+ val T2 = range_type (typeof t)
+ (* we create 'size_of_interpretation (interpret (... T1))' different copies *)
+ (* of the tree for 'T2', which are then combined into a single new tree *)
+ val (i1, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (stringof t, T1))
+ (* power(a,b) computes a^b, for a>=0, b>=0 *)
+ (* int * int -> int *)
+ fun power (a,0) = 1
+ | power (a,1) = a
+ | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
+ fun size_of_interpretation (Leaf xs) = length xs
+ | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
+ val size = size_of_interpretation i1
+ (* make fresh copies, with different variable indices *)
+ (* int -> int -> (int * interpretation list *)
+ fun make_copies idx 0 =
+ (idx, [])
+ | make_copies idx n =
+ let
+ val (copy, _, args) = interpret thy (sizes, []) {next_idx = idx, bounds = [], wellformed=True} (Free (stringof t, T2))
+ val (next, copies) = make_copies (#next_idx args) (n-1)
+ in
+ (next, copy :: copies)
+ end
+ val (idx, copies) = make_copies (#next_idx args) (size_of_interpretation i1)
+ (* combine copies into a single tree *)
+ val intr = Node copies
+ in
+ (* extend the model, increase 'next_idx' *)
+ Some (intr, (sizes, (t, intr)::intrs), {next_idx = idx, bounds = #bounds args, wellformed = #wellformed args})
+ end)
+ else
+ None
+ end;
+
+ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
+
+ fun var_settype_interpreter thy model args t =
+ let
+ val (sizes, intrs) = model
+ in
+ case t of
+ Free (x, Type ("set", [T])) =>
+ (case assoc (intrs, t) of
+ Some intr => Some (intr, model, args)
+ | None =>
+ let
+ val (intr, _, args') = interpret thy model args (Free (x, Type ("fun", [T, Type ("bool", [])])))
+ in
+ Some (intr, (sizes, (t, intr)::intrs), args')
+ end)
+ | Var ((x,i), Type ("set", [T])) =>
+ (case assoc (intrs, t) of
+ Some intr => Some (intr, model, args)
+ | None =>
+ let
+ val (intr, _, args') = interpret thy model args (Var ((x,i), Type ("fun", [T, Type ("bool", [])])))
+ in
+ Some (intr, (sizes, (t, intr)::intrs), args')
+ end)
+ | _ => None
+ end;
+
+ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
+
+ fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds args), model, args)
+ | boundvar_interpreter thy model args _ = None;
+
+ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
+
+ fun abstraction_interpreter thy model args (Abs (x, T, t)) =
+ let
+ val (sizes, intrs) = model
+ (* create all constants of type T *)
+ val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (x, T))
+ (* returns a list with all unit vectors of length n *)
+ (* int -> interpretation list *)
+ fun unit_vectors n =
+ let
+ (* returns the k-th unit vector of length n *)
+ (* int * int -> interpretation *)
+ fun unit_vector (k,n) =
+ Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
+ (* int -> interpretation list -> interpretation list *)
+ fun unit_vectors_acc k vs =
+ if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
+ in
+ unit_vectors_acc 1 []
+ end
+ (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
+ (* 'a -> 'a list list -> 'a list list *)
+ fun cons_list x xss =
+ map (fn xs => x::xs) xss
+ (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
+ (* int -> 'a list -> 'a list list *)
+ fun pick_all 1 xs =
+ map (fn x => [x]) xs
+ | pick_all n xs =
+ let val rec_pick = pick_all (n-1) xs in
+ foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
+ end
+ (* interpretation -> interpretation list *)
+ fun make_constants (Leaf xs) =
+ unit_vectors (length xs)
+ | make_constants (Node xs) =
+ map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
+ (* interpret the body 't' separately for each constant *)
+ val ((model', args'), bodies) = foldl_map
+ (fn ((m,a), c) =>
+ let
+ (* add 'c' to 'bounds' *)
+ val (i',m',a') = interpret thy m {next_idx = #next_idx a, bounds = c::(#bounds a), wellformed = #wellformed a} t
+ in
+ (* keep the new model m' and 'next_idx', but use old 'bounds' *)
+ ((m',{next_idx = #next_idx a', bounds = #bounds a, wellformed = #wellformed a'}), i')
+ end)
+ ((model,args), make_constants i)
+ in
+ Some (Node bodies, model', args')
+ end
+ | abstraction_interpreter thy model args _ = None;
+
+ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
+
+ fun apply_interpreter thy model args (t1 $ t2) =
+ let
+ (* auxiliary functions *)
+ (* interpretation * interpretation -> interpretation *)
+ fun interpretation_disjunction (tr1,tr2) =
+ tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
+ (* prop_formula * interpretation -> interpretation *)
+ fun prop_formula_times_interpretation (fm,tr) =
+ tree_map (map (fn x => SAnd (fm,x))) tr
+ (* prop_formula list * interpretation list -> interpretation *)
+ fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
+ prop_formula_times_interpretation (fm,tr)
+ | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
+ interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees))
+ | prop_formula_list_dot_product_interpretation_list (_,_) =
+ raise REFUTE ("apply_interpreter", "empty list (in dot product)")
+ (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
+ (* 'a -> 'a list list -> 'a list list *)
+ fun cons_list x xss =
+ map (fn xs => x::xs) xss
+ (* returns a list of lists, each one consisting of one element from each element of 'xss' *)
+ (* 'a list list -> 'a list list *)
+ fun pick_all [xs] =
+ map (fn x => [x]) xs
+ | pick_all (xs::xss) =
+ let val rec_pick = pick_all xss in
+ foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
+ end
+ | pick_all _ =
+ raise REFUTE ("apply_interpreter", "empty list (in pick_all)")
+ (* interpretation -> prop_formula list *)
+ fun interpretation_to_prop_formula_list (Leaf xs) =
+ xs
+ | interpretation_to_prop_formula_list (Node trees) =
+ map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees))
+ (* interpretation * interpretation -> interpretation *)
+ fun interpretation_apply (tr1,tr2) =
+ (case tr1 of
+ Leaf _ =>
+ raise REFUTE ("apply_interpreter", "first interpretation is a leaf")
+ | Node xs =>
+ prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list tr2, xs))
+ (* interpret 't1' and 't2' *)
+ val (intr1, model1, args1) = interpret thy model args t1
+ val (intr2, model2, args2) = interpret thy model1 args1 t2
+ in
+ Some (interpretation_apply (intr1,intr2), model2, args2)
+ end
+ | apply_interpreter thy model args _ = None;
+
+ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
+
+ fun const_unfold_interpreter thy model args t =
+ (* ------------------------------------------------------------------------- *)
+ (* We unfold constants for which a defining equation is given as an axiom. *)
+ (* A polymorphic axiom's type variables are instantiated. Eta-expansion is *)
+ (* performed only if necessary; arguments in the axiom that are present as *)
+ (* actual arguments in 't' are simply substituted. If more actual than *)
+ (* formal arguments are present, the constant is *not* unfolded, so that *)
+ (* other interpreters (that may just not have looked into the term far *)
+ (* enough yet) may be applied first (after 'apply_interpreter' gets rid of *)
+ (* one argument). *)
+ (* ------------------------------------------------------------------------- *)
+ let
+ val (head, actuals) = strip_comb t
+ val actuals_count = length actuals
+ in
+ case head of
+ Const (s,T) =>
+ let
+ (* (string * Term.term) list *)
+ val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
+ (* Term.term * Term.term list * Term.term list -> Term.term *)
+ (* term, formal arguments, actual arguments *)
+ fun normalize (t, [], []) = t
+ | normalize (t, [], y::ys) = raise REFUTE ("const_unfold_interpreter", "more actual than formal parameters")
+ | normalize (t, x::xs, []) = normalize (lambda x t, xs, []) (* eta-expansion *)
+ | normalize (t, x::xs, y::ys) = normalize (betapply (lambda x t, y), xs, ys) (* substitution *)
+ (* string -> Term.typ -> (string * Term.term) list -> Term.term option *)
+ fun get_defn s T [] =
+ None
+ | get_defn s T ((_,ax)::axms) =
+ (let
+ val (lhs, rhs) = Logic.dest_equals ax (* equations only *)
+ val (c, formals) = strip_comb lhs
+ val (s', T') = dest_Const c
+ in
+ if (s=s') andalso (actuals_count <= length formals) then
+ let
+ val varT' = Type.varifyT T' (* for polymorphic definitions *)
+ val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (varT', T))
+ val varRhs = map_term_types Type.varifyT rhs
+ val varFormals = map (map_term_types Type.varifyT) formals
+ val rhs' = normalize (varRhs, varFormals, actuals)
+ val unvarRhs = map_term_types
+ (map_type_tvar
+ (fn (v,_) =>
+ case Vartab.lookup (typeSubs, v) of
+ None =>
+ raise REFUTE ("const_unfold_interpreter", "schematic type variable " ^ (fst v) ^ "not instantiated (in definition of " ^ quote s ^ ")")
+ | Some typ =>
+ typ))
+ rhs'
+ in
+ Some unvarRhs
+ end
+ else
+ get_defn s T axms
+ end
+ handle TERM _ => get_defn s T axms
+ | Type.TYPE_MATCH => get_defn s T axms)
+ in
+ case get_defn s T axioms of
+ Some t' => Some (interpret thy model args t')
+ | None => None
+ end
+ | _ => None
+ end;
+
+ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
+
+ fun Pure_interpreter thy model args t =
+ let
+ fun toTrue (Leaf [fm,_]) = fm
+ | toTrue _ = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value")
+ fun toFalse (Leaf [_,fm]) = fm
+ | toFalse _ = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value")
+ in
+ case t of
+ (*Const ("Goal", _) $ t1 =>
+ Some (interpret thy model args t1) |*)
+ Const ("all", _) $ t1 =>
+ let
+ val (i,m,a) = (interpret thy model args t1)
+ in
+ case i of
+ Node xs =>
+ let
+ val fmTrue = PropLogic.all (map toTrue xs)
+ val fmFalse = PropLogic.exists (map toFalse xs)
+ in
+ Some (Leaf [fmTrue, fmFalse], m, a)
+ end
+ | _ =>
+ raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function")
+ end
+ | Const ("==", _) $ t1 $ t2 =>
+ let
+ val (i1,m1,a1) = interpret thy model args t1
+ val (i2,m2,a2) = interpret thy m1 a1 t2
+ (* interpretation * interpretation -> prop_formula *)
+ fun interpret_equal (tr1,tr2) =
+ (case tr1 of
+ Leaf x =>
+ (case tr2 of
+ Leaf y => PropLogic.dot_product (x,y)
+ | _ => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher"))
+ | Node xs =>
+ (case tr2 of
+ Leaf _ => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher")
+ (* extensionality: two functions are equal iff they are equal for every element *)
+ | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
+ (* interpretation * interpretation -> prop_formula *)
+ fun interpret_unequal (tr1,tr2) =
+ (case tr1 of
+ Leaf x =>
+ (case tr2 of
+ Leaf y =>
+ let
+ fun unequal [] ([],_) =
+ False
+ | unequal (x::xs) (y::ys1, ys2) =
+ SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2))
+ | unequal _ _ =
+ raise REFUTE ("Pure_interpreter", "\"==\": leafs have different width")
+ in
+ unequal x (y,[])
+ end
+ | _ => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher"))
+ | Node xs =>
+ (case tr2 of
+ Leaf _ => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher")
+ (* extensionality: two functions are unequal iff there exist unequal elements *)
+ | Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys))))
+ val fmTrue = interpret_equal (i1,i2)
+ val fmFalse = interpret_unequal (i1,i2)
+ in
+ Some (Leaf [fmTrue, fmFalse], m2, a2)
+ end
+ | Const ("==>", _) $ t1 $ t2 =>
+ let
+ val (i1,m1,a1) = interpret thy model args t1
+ val (i2,m2,a2) = interpret thy m1 a1 t2
+ val fmTrue = SOr (toFalse i1, toTrue i2)
+ val fmFalse = SAnd (toTrue i1, toFalse i2)
+ in
+ Some (Leaf [fmTrue, fmFalse], m2, a2)
+ end
+ | _ => None
+ end;
+
+ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
+
+ fun HOLogic_interpreter thy model args t =
+ (* ------------------------------------------------------------------------- *)
+ (* Providing interpretations directly is more efficient than unfolding the *)
+ (* logical constants; however, we need versions for constants with arguments *)
+ (* (to avoid unfolding) as well as versions for constants without arguments *)
+ (* (since in HOL, logical constants can themselves be arguments) *)
+ (* ------------------------------------------------------------------------- *)
+ let
+ fun eta_expand t i =
+ let
+ val Ts = binder_types (fastype_of t)
+ in
+ foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
+ (take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
+ end
+ val TT = Leaf [True, False]
+ val FF = Leaf [False, True]
+ fun toTrue (Leaf [fm,_]) = fm
+ | toTrue _ = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value")
+ fun toFalse (Leaf [_,fm]) = fm
+ | toFalse _ = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value")
+ in
+ case t of
+ Const ("Trueprop", _) $ t1 =>
+ Some (interpret thy model args t1)
+ | Const ("Trueprop", _) =>
+ Some (Node [TT, FF], model, args)
+ | Const ("Not", _) $ t1 =>
+ apply_interpreter thy model args t
+ | Const ("Not", _) =>
+ Some (Node [FF, TT], model, args)
+ | Const ("True", _) =>
+ Some (TT, model, args)
+ | Const ("False", _) =>
+ Some (FF, model, args)
+ | Const ("arbitrary", T) =>
+ (* treat 'arbitrary' just like a free variable of the same type *)
+ (case assoc (snd model, t) of
+ Some intr =>
+ Some (intr, model, args)
+ | None =>
+ let
+ val (sizes, intrs) = model
+ val (intr, _, a) = interpret thy (sizes, []) args (Free ("<arbitrary>", T))
+ in
+ Some (intr, (sizes, (t,intr)::intrs), a)
+ end)
+ | Const ("The", _) $ t1 =>
+ apply_interpreter thy model args t
+ | Const ("The", T as Type ("fun", [_, T'])) =>
+ (* treat 'The' like a free variable, but with a fixed interpretation for boolean *)
+ (* functions that map exactly one constant of type T' to True *)
+ (case assoc (snd model, t) of
+ Some intr =>
+ Some (intr, model, args)
+ | None =>
+ let
+ val (sizes, intrs) = model
+ val (intr, _, a) = interpret thy (sizes, []) args (Free ("<The>", T))
+ (* create all constants of type T' => bool, ... *)
+ val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<The>", Type ("fun", [T', Type ("bool",[])])))
+ (* ... and all constants of type T' *)
+ val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<The>", T'))
+ (* returns a list with all unit vectors of length n *)
+ (* int -> interpretation list *)
+ fun unit_vectors n =
+ let
+ (* returns the k-th unit vector of length n *)
+ (* int * int -> interpretation *)
+ fun unit_vector (k,n) =
+ Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
+ (* int -> interpretation list -> interpretation list *)
+ fun unit_vectors_acc k vs =
+ if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
+ in
+ unit_vectors_acc 1 []
+ end
+ (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
+ (* 'a -> 'a list list -> 'a list list *)
+ fun cons_list x xss =
+ map (fn xs => x::xs) xss
+ (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
+ (* int -> 'a list -> 'a list list *)
+ fun pick_all 1 xs =
+ map (fn x => [x]) xs
+ | pick_all n xs =
+ let val rec_pick = pick_all (n-1) xs in
+ foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
+ end
+ (* interpretation -> interpretation list *)
+ fun make_constants (Leaf xs) =
+ unit_vectors (length xs)
+ | make_constants (Node xs) =
+ map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
+ val constantsFun = make_constants intrFun
+ val constantsT' = make_constants intrT'
+ (* interpretation -> interpretation list -> interpretation option *)
+ fun the_val (Node xs) cs =
+ let
+ val TrueCount = foldl (fn (n,x) => if toTrue x = True then n+1 else n) (0,xs)
+ fun findThe (x::xs) (c::cs) =
+ if toTrue x = True then
+ c
+ else
+ findThe xs cs
+ | findThe _ _ =
+ raise REFUTE ("HOLogic_interpreter", "\"The\": not found")
+ in
+ if TrueCount=1 then
+ Some (findThe xs cs)
+ else
+ None
+ end
+ | the_val _ _ =
+ raise REFUTE ("HOLogic_interpreter", "\"The\": function interpreted as a leaf")
+ in
+ case intr of
+ Node xs =>
+ let
+ (* replace interpretation 'x' by the interpretation determined by 'f' *)
+ val intrThe = Node (map (fn (x,f) => if_none (the_val f constantsT') x) (xs ~~ constantsFun))
+ in
+ Some (intrThe, (sizes, (t,intrThe)::intrs), a)
+ end
+ | _ =>
+ raise REFUTE ("HOLogic_interpreter", "\"The\": interpretation is a leaf")
+ end)
+ | Const ("Hilbert_Choice.Eps", _) $ t1 =>
+ apply_interpreter thy model args t
+ | Const ("Hilbert_Choice.Eps", T as Type ("fun", [_, T'])) =>
+ (* treat 'The' like a free variable, but with a fixed interpretation for boolean *)
+ (* functions that map exactly one constant of type T' to True *)
+ (case assoc (snd model, t) of
+ Some intr =>
+ Some (intr, model, args)
+ | None =>
+ let
+ val (sizes, intrs) = model
+ val (intr, _, a) = interpret thy (sizes, []) args (Free ("<Eps>", T))
+ (* create all constants of type T' => bool, ... *)
+ val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<Eps>", Type ("fun", [T', Type ("bool",[])])))
+ (* ... and all constants of type T' *)
+ val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<Eps>", T'))
+ (* returns a list with all unit vectors of length n *)
+ (* int -> interpretation list *)
+ fun unit_vectors n =
+ let
+ (* returns the k-th unit vector of length n *)
+ (* int * int -> interpretation *)
+ fun unit_vector (k,n) =
+ Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
+ (* int -> interpretation list -> interpretation list *)
+ fun unit_vectors_acc k vs =
+ if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
+ in
+ unit_vectors_acc 1 []
+ end
+ (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
+ (* 'a -> 'a list list -> 'a list list *)
+ fun cons_list x xss =
+ map (fn xs => x::xs) xss
+ (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
+ (* int -> 'a list -> 'a list list *)
+ fun pick_all 1 xs =
+ map (fn x => [x]) xs
+ | pick_all n xs =
+ let val rec_pick = pick_all (n-1) xs in
+ foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
+ end
+ (* interpretation -> interpretation list *)
+ fun make_constants (Leaf xs) =
+ unit_vectors (length xs)
+ | make_constants (Node xs) =
+ map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
+ val constantsFun = make_constants intrFun
+ val constantsT' = make_constants intrT'
+ (* interpretation -> interpretation list -> interpretation list *)
+ fun true_values (Node xs) cs =
+ mapfilter (fn (x,c) => if toTrue x = True then Some c else None) (xs~~cs)
+ | true_values _ _ =
+ raise REFUTE ("HOLogic_interpreter", "\"Eps\": function interpreted as a leaf")
+ in
+ case intr of
+ Node xs =>
+ let
+ val (wf, intrsEps) = foldl_map (fn (w,(x,f)) =>
+ case true_values f constantsT' of
+ [] => (w, x) (* no value mapped to true -> no restriction *)
+ | [c] => (w, c) (* one value mapped to true -> that's the one *)
+ | cs =>
+ let
+ (* interpretation * interpretation -> prop_formula *)
+ fun interpret_equal (tr1,tr2) =
+ (case tr1 of
+ Leaf x =>
+ (case tr2 of
+ Leaf y => PropLogic.dot_product (x,y)
+ | _ => raise REFUTE ("HOLogic_interpreter", "\"Eps\": second tree is higher"))
+ | Node xs =>
+ (case tr2 of
+ Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"Eps\": first tree is higher")
+ (* extensionality: two functions are equal iff they are equal for every element *)
+ | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
+ in
+ (SAnd (w, PropLogic.exists (map (fn c => interpret_equal (x,c)) cs)), x) (* impose restrictions on x *)
+ end
+ )
+ (#wellformed a, xs ~~ constantsFun)
+ val intrEps = Node intrsEps
+ in
+ Some (intrEps, (sizes, (t,intrEps)::intrs), {next_idx = #next_idx a, bounds = #bounds a, wellformed = wf})
+ end
+ | _ =>
+ raise REFUTE ("HOLogic_interpreter", "\"Eps\": interpretation is a leaf")
+ end)
+ | Const ("All", _) $ t1 =>
+ let
+ val (i,m,a) = interpret thy model args t1
+ in
+ case i of
+ Node xs =>
+ let
+ val fmTrue = PropLogic.all (map toTrue xs)
+ val fmFalse = PropLogic.exists (map toFalse xs)
+ in
+ Some (Leaf [fmTrue, fmFalse], m, a)
+ end
+ | _ =>
+ raise REFUTE ("HOLogic_interpreter", "\"All\" is not followed by a function")
+ end
+ | Const ("All", _) =>
+ Some (interpret thy model args (eta_expand t 1))
+ | Const ("Ex", _) $ t1 =>
+ let
+ val (i,m,a) = interpret thy model args t1
+ in
+ case i of
+ Node xs =>
+ let
+ val fmTrue = PropLogic.exists (map toTrue xs)
+ val fmFalse = PropLogic.all (map toFalse xs)
+ in
+ Some (Leaf [fmTrue, fmFalse], m, a)
+ end
+ | _ =>
+ raise REFUTE ("HOLogic_interpreter", "\"Ex\" is not followed by a function")
+ end
+ | Const ("Ex", _) =>
+ Some (interpret thy model args (eta_expand t 1))
+ | Const ("Ex1", _) $ t1 =>
+ let
+ val (i,m,a) = interpret thy model args t1
+ in
+ case i of
+ Node xs =>
+ let
+ (* interpretation list -> prop_formula *)
+ fun allfalse [] = True
+ | allfalse (x::xs) = SAnd (toFalse x, allfalse xs)
+ (* interpretation list -> prop_formula *)
+ fun exactly1true [] = False
+ | exactly1true (x::xs) = SOr (SAnd (toTrue x, allfalse xs), SAnd (toFalse x, exactly1true xs))
+ (* interpretation list -> prop_formula *)
+ fun atleast2true [] = False
+ | atleast2true (x::xs) = SOr (SAnd (toTrue x, PropLogic.exists (map toTrue xs)), atleast2true xs)
+ val fmTrue = exactly1true xs
+ val fmFalse = SOr (allfalse xs, atleast2true xs)
+ in
+ Some (Leaf [fmTrue, fmFalse], m, a)
+ end
+ | _ =>
+ raise REFUTE ("HOLogic_interpreter", "\"Ex1\" is not followed by a function")
+ end
+ | Const ("Ex1", _) =>
+ Some (interpret thy model args (eta_expand t 1))
+ | Const ("op =", _) $ t1 $ t2 =>
+ let
+ val (i1,m1,a1) = interpret thy model args t1
+ val (i2,m2,a2) = interpret thy m1 a1 t2
+ (* interpretation * interpretation -> prop_formula *)
+ fun interpret_equal (tr1,tr2) =
+ (case tr1 of
+ Leaf x =>
+ (case tr2 of
+ Leaf y => PropLogic.dot_product (x,y)
+ | _ => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher"))
+ | Node xs =>
+ (case tr2 of
+ Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher")
+ (* extensionality: two functions are equal iff they are equal for every element *)
+ | Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
+ (* interpretation * interpretation -> prop_formula *)
+ fun interpret_unequal (tr1,tr2) =
+ (case tr1 of
+ Leaf x =>
+ (case tr2 of
+ Leaf y =>
+ let
+ fun unequal [] ([],_) =
+ False
+ | unequal (x::xs) (y::ys1, ys2) =
+ SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2))
+ | unequal _ _ =
+ raise REFUTE ("HOLogic_interpreter", "\"==\": leafs have different width")
+ in
+ unequal x (y,[])
+ end
+ | _ => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher"))
+ | Node xs =>
+ (case tr2 of
+ Leaf _ => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher")
+ (* extensionality: two functions are unequal iff there exist unequal elements *)
+ | Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys))))
+ val fmTrue = interpret_equal (i1,i2)
+ val fmFalse = interpret_unequal (i1,i2)
+ in
+ Some (Leaf [fmTrue, fmFalse], m2, a2)
+ end
+ | Const ("op =", _) $ t1 =>
+ Some (interpret thy model args (eta_expand t 1))
+ | Const ("op =", _) =>
+ Some (interpret thy model args (eta_expand t 2))
+ | Const ("op &", _) $ t1 $ t2 =>
+ apply_interpreter thy model args t
+ | Const ("op &", _) $ t1 =>
+ apply_interpreter thy model args t
+ | Const ("op &", _) =>
+ Some (Node [Node [TT, FF], Node [FF, FF]], model, args)
+ | Const ("op |", _) $ t1 $ t2 =>
+ apply_interpreter thy model args t
+ | Const ("op |", _) $ t1 =>
+ apply_interpreter thy model args t
+ | Const ("op |", _) =>
+ Some (Node [Node [TT, TT], Node [TT, FF]], model, args)
+ | Const ("op -->", _) $ t1 $ t2 =>
+ apply_interpreter thy model args t
+ | Const ("op -->", _) $ t1 =>
+ apply_interpreter thy model args t
+ | Const ("op -->", _) =>
+ Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
+ | Const ("Collect", _) $ t1 =>
+ (* Collect == identity *)
+ Some (interpret thy model args t1)
+ | Const ("Collect", _) =>
+ Some (interpret thy model args (eta_expand t 1))
+ | Const ("op :", _) $ t1 $ t2 =>
+ (* op: == application *)
+ Some (interpret thy model args (t2 $ t1))
+ | Const ("op :", _) $ t1 =>
+ Some (interpret thy model args (eta_expand t 1))
+ | Const ("op :", _) =>
+ Some (interpret thy model args (eta_expand t 2))
+ | _ => None
+ end;
+
+ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
+
+ fun IDT_interpreter thy model args t =
+ let
+ fun is_var (Free _) = true
+ | is_var (Var _) = true
+ | is_var _ = false
+ fun typeof (Free (_,T)) = T
+ | typeof (Var (_,T)) = T
+ | typeof _ = raise REFUTE ("var_IDT_interpreter", "term is not a variable")
+ val (sizes, intrs) = model
+ (* power(a,b) computes a^b, for a>=0, b>=0 *)
+ (* int * int -> int *)
+ fun power (a,0) = 1
+ | power (a,1) = a
+ | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
+ (* interpretation -> int *)
+ fun size_of_interpretation (Leaf xs) = length xs
+ | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
+ (* Term.typ -> int *)
+ fun size_of_type T =
+ let
+ val (i,_,_) = interpret thy model args (Free ("<IDT>", T))
+ in
+ size_of_interpretation i
+ end
+ (* int list -> int *)
+ fun sum xs = foldl op+ (0, xs)
+ (* int list -> int *)
+ fun product xs = foldl op* (1, xs)
+ (* DatatypeAux.dtyp * Term.typ -> DatatypeAux.dtyp -> Term.typ *)
+ fun typ_of_dtyp typ_assoc (DatatypeAux.DtTFree a) =
+ the (assoc (typ_assoc, DatatypeAux.DtTFree a))
+ | typ_of_dtyp typ_assoc (DatatypeAux.DtRec i) =
+ raise REFUTE ("var_IDT_interpreter", "recursive datatype")
+ | typ_of_dtyp typ_assoc (DatatypeAux.DtType (s, ds)) =
+ Type (s, map (typ_of_dtyp typ_assoc) ds)
+ in
+ if is_var t then
+ (case typeof t of
+ Type (s, Ts) =>
+ (case DatatypePackage.datatype_info thy s of
+ Some info => (* inductive datatype *)
let
val index = #index info
val descr = #descr info
val (_, dtyps, constrs) = the (assoc (descr, index))
- val Typs = dtyps ~~ Ts
- (* DatatypeAux.dtyp -> Term.typ *)
- fun typ_of_dtyp (DatatypeAux.DtTFree a) =
- the (assoc (Typs, DatatypeAux.DtTFree a))
- | typ_of_dtyp (DatatypeAux.DtRec i) =
- let
- val (s, ds, _) = the (assoc (descr, i))
- in
- Type (s, map typ_of_dtyp ds)
- end
- | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
- Type (s, map typ_of_dtyp ds)
in
- sum (map (fn (_,ds) => product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)) constrs)
+ if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
+ raise REFUTE ("var_IDT_interpreter", "recursive datatype argument")
+ else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
+ None (* recursive datatype (requires an infinite model) *)
+ else
+ case assoc (intrs, t) of
+ Some intr => Some (intr, model, args)
+ | None =>
+ let
+ val typ_assoc = dtyps ~~ Ts
+ val size = sum (map (fn (_,ds) =>
+ product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) constrs)
+ val idx = #next_idx args
+ (* for us, an IDT has no "internal structure" -- its interpretation is just a leaf *)
+ val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1))))
+ val next = (if size=2 then idx+1 else idx+size)
+ in
+ (* extend the model, increase 'next_idx' *)
+ Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args})
+ end
end
- else 0
- | None => error ("size_of_type: type contains an unknown type constructor: '" ^ s ^ "'"))
- | TFree _ => lookup_size T us
- | TVar _ => lookup_size T us
+ | None => None)
+ | _ => None)
+ else
+ let
+ val (head, params) = strip_comb t (* look into applications to avoid unfolding *)
+ in
+ (case head of
+ Const (c, T) =>
+ (case body_type T of
+ Type (s, Ts) =>
+ (case DatatypePackage.datatype_info thy s of
+ Some info => (* inductive datatype *)
+ let
+ val index = #index info
+ val descr = #descr info
+ val (_, dtyps, constrs) = the (assoc (descr, index))
+ in
+ if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
+ raise REFUTE ("var_IDT_interpreter", "recursive datatype argument")
+ else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
+ None (* recursive datatype (requires an infinite model) *)
+ else
+ (case take_prefix (fn (c',_) => c' <> c) constrs of
+ (_, []) =>
+ None (* unknown constructor *)
+ | (prevs, _) =>
+ if null params then
+ let
+ val typ_assoc = dtyps ~~ Ts
+ val offset = sum (map (fn (_,ds) =>
+ product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) prevs)
+ val (i,_,_) = interpret thy model args (Free ("<IDT>", T))
+ (* int * interpretation -> int * interpretation *)
+ fun replace (offset, Leaf xs) =
+ (* replace the offset-th element by True, all others by False, inc. offset by 1 *)
+ (offset+1, Leaf (snd (foldl_map (fn (n,_) => (n+1, if n=offset then True else False)) (0, xs))))
+ | replace (offset, Node xs) =
+ let
+ val (offset', xs') = foldl_map replace (offset, xs)
+ in
+ (offset', Node xs')
+ end
+ val (_,intr) = replace (offset, i)
+ in
+ Some (intr, model, args)
+ end
+ else
+ apply_interpreter thy model args t) (* avoid unfolding by calling 'apply_interpreter' directly *)
+ end
+ | None => None)
+ | _ => None)
+ | _ => None)
+ end
end;
+
(* ------------------------------------------------------------------------- *)
-(* type_to_prop_tree: creates a tree of boolean variables that denotes an *)
-(* element of the type 'T'. The height and branching factor of the *)
-(* tree depend on the size and "structure" of 'T'. *)
-(* 'us' : a "universe" specifying the number of elements for each basic type *)
-(* (i.e. each type variable) in 'T' *)
-(* 'cdepth': maximum constructor depth to be used for inductive datatypes *)
-(* 'idx': the next index to be used for a boolean variable *)
+(* PRINTERS *)
(* ------------------------------------------------------------------------- *)
- (* Term.typ -> (Term.typ * int) list -> theory -> int -> int -> prop_tree * int *)
+ (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
- fun type_to_prop_tree T us thy cdepth idx =
+ fun var_typevar_printer thy model t intr assignment =
let
- (* int -> Term.typ -> int -> prop_tree list * int *)
- fun type_to_prop_tree_list 1 T' idx' =
- let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
- ([tr], newidx)
- end
- | type_to_prop_tree_list n T' idx' =
- let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
- let val (trees, lastidx) = type_to_prop_tree_list (n-1) T' newidx in
- (tr::trees, lastidx)
- end
- end
+ fun is_var (Free _) = true
+ | is_var (Var _) = true
+ | is_var _ = false
+ fun typeof (Free (_,T)) = T
+ | typeof (Var (_,T)) = T
+ | typeof _ = raise REFUTE ("var_typevar_printer", "term is not a variable")
+ fun is_typevar (TFree _) = true
+ | is_typevar (TVar _) = true
+ | is_typevar _ = false
in
- case T of
- Type ("prop", []) =>
- (Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
- | Type ("bool", []) =>
- (Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
- | Type ("Product_Type.unit", []) =>
- (Leaf [True], idx)
- | Type ("+", [T1,T2]) =>
+ if is_var t andalso is_typevar (typeof t) then
let
- val s1 = size_of_type T1 us thy cdepth
- val s2 = size_of_type T2 us thy cdepth
- val s = s1 + s2
- in
- if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
- raise EMPTY_DATATYPE
- else
- error "sum types (+) not implemented yet (TODO)"
- end
- | Type ("*", [T1,T2]) =>
- let
- val s1 = size_of_type T1 us thy cdepth
- val s2 = size_of_type T2 us thy cdepth
- val s = s1 * s2
+ (* interpretation -> int *)
+ fun index_from_interpretation (Leaf xs) =
+ let
+ val idx = find_index (PropLogic.eval assignment) xs
+ in
+ if idx<0 then
+ raise REFUTE ("var_typevar_printer", "illegal interpretation: no value assigned")
+ else
+ idx
+ end
+ | index_from_interpretation _ =
+ raise REFUTE ("var_typevar_printer", "interpretation is not a leaf")
+ (* string -> string *)
+ fun strip_leading_quote s =
+ (implode o (fn (x::xs) => if x="'" then xs else (x::xs)) o explode) s
+ (* Term.typ -> string *)
+ fun string_of_typ (TFree (x,_)) = strip_leading_quote x
+ | string_of_typ (TVar ((x,i),_)) = strip_leading_quote x ^ string_of_int i
+ | string_of_typ _ = raise REFUTE ("var_typevar_printer", "type is not a type variable")
in
- if s1=0 orelse s2=0 then
- raise EMPTY_DATATYPE
- else
- error "product types (*) not implemented yet (TODO)"
- end
- | Type ("fun", [T1,T2]) =>
- (* we create 'size_of_type T1' different copies of the tree for 'T2', *)
- (* which are then combined into a single new tree *)
- let
- val s = size_of_type T1 us thy cdepth
- in
- if s=0 then
- raise EMPTY_DATATYPE
- else
- let val (trees, newidx) = type_to_prop_tree_list s T2 idx in
- (Node trees, newidx)
- end
+ Some (string_of_typ (typeof t) ^ string_of_int (index_from_interpretation intr))
end
- | Type ("set", [T1]) =>
- type_to_prop_tree (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth idx
- | Type (s, _) =>
- (case DatatypePackage.constrs_of thy s of
- Some _ => (* inductive datatype *)
- let
- val s = size_of_type T us thy cdepth
- in
- if s=0 then
- raise EMPTY_DATATYPE
- else
- (Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
- end
- | None => error ("type_to_prop_tree: type contains an unknown type constructor: '" ^ s ^ "'"))
- | TFree _ =>
- let val s = size_of_type T us thy cdepth in
- (Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
- end
- | TVar _ =>
- let val s = size_of_type T us thy cdepth in
- (Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
- end
+ else
+ None
end;
-(* ------------------------------------------------------------------------- *)
-(* type_to_constants: creates a list of prop_trees with constants (True, *)
-(* False) rather than boolean variables, one for every element in the *)
-(* type 'T'; c.f. type_to_prop_tree *)
-(* ------------------------------------------------------------------------- *)
+ (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
- (* Term.typ -> (Term.typ * int) list -> theory -> int -> prop_tree list *)
+ fun var_funtype_printer thy model t intr assignment =
+ let
+ fun is_var (Free _) = true
+ | is_var (Var _) = true
+ | is_var _ = false
+ fun typeof (Free (_,T)) = T
+ | typeof (Var (_,T)) = T
+ | typeof _ = raise REFUTE ("var_funtype_printer", "term is not a variable")
+ fun is_funtype (Type ("fun", [_,_])) = true
+ | is_funtype _ = false
+ in
+ if is_var t andalso is_funtype (typeof t) then
+ let
+ val T1 = domain_type (typeof t)
+ val T2 = range_type (typeof t)
+ val (sizes, _) = model
+ (* create all constants of type T1 *)
+ val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_funtype_printer", T1))
+ (* returns a list with all unit vectors of length n *)
+ (* int -> interpretation list *)
+ fun unit_vectors n =
+ let
+ (* returns the k-th unit vector of length n *)
+ (* int * int -> interpretation *)
+ fun unit_vector (k,n) =
+ Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
+ (* int -> interpretation list -> interpretation list *)
+ fun unit_vectors_acc k vs =
+ if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
+ in
+ unit_vectors_acc 1 []
+ end
+ (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
+ (* 'a -> 'a list list -> 'a list list *)
+ fun cons_list x xss =
+ map (fn xs => x::xs) xss
+ (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
+ (* int -> 'a list -> 'a list list *)
+ fun pick_all 1 xs =
+ map (fn x => [x]) xs
+ | pick_all n xs =
+ let val rec_pick = pick_all (n-1) xs in
+ foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
+ end
+ (* interpretation -> interpretation list *)
+ fun make_constants (Leaf xs) =
+ unit_vectors (length xs)
+ | make_constants (Node xs) =
+ map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
+ (* interpretation list *)
+ val results = (case intr of
+ Node xs => xs
+ | _ => raise REFUTE ("var_funtype_printer", "interpretation is a leaf"))
+ (* string list *)
+ val strings = map
+ (fn (argi,resulti) => print thy model (Free ("var_funtype_printer", T1)) argi assignment
+ ^ "\\<mapsto>"
+ ^ print thy model (Free ("var_funtype_printer", T2)) resulti assignment)
+ ((make_constants i) ~~ results)
+ in
+ Some (enclose "(" ")" (commas strings))
+ end
+ else
+ None
+ end;
- fun type_to_constants T us thy cdepth =
+ (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
+
+ fun var_settype_printer thy model t intr assignment =
let
+ val (sizes, _) = model
(* returns a list with all unit vectors of length n *)
- (* int -> prop_tree list *)
+ (* int -> interpretation list *)
fun unit_vectors n =
let
(* returns the k-th unit vector of length n *)
- (* int * int -> prop_tree *)
+ (* int * int -> interpretation *)
fun unit_vector (k,n) =
Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
- (* int -> prop_tree list -> prop_tree list *)
+ (* int -> interpretation list -> interpretation list *)
fun unit_vectors_acc k vs =
if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
in
@@ -918,731 +1573,238 @@
let val rec_pick = pick_all (n-1) xs in
foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
end
+ (* interpretation -> interpretation list *)
+ fun make_constants (Leaf xs) =
+ unit_vectors (length xs)
+ | make_constants (Node xs) =
+ map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
in
- case T of
- Type ("prop", []) => unit_vectors 2
- | Type ("bool", []) => unit_vectors 2
- | Type ("Product_Type.unit", []) => unit_vectors 1
- | Type ("+", [T1,T2]) =>
+ case t of
+ Free (x, Type ("set", [T])) =>
let
- val s1 = size_of_type T1 us thy cdepth
- val s2 = size_of_type T2 us thy cdepth
+ (* interpretation list *)
+ val results = (case intr of
+ Node xs => xs
+ | _ => raise REFUTE ("var_settype_printer", "interpretation is a leaf"))
+ (* create all constants of type T *)
+ val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T))
+ (* string list *)
+ val strings = mapfilter
+ (fn (argi,Leaf [fmTrue,fmFalse]) =>
+ if PropLogic.eval assignment fmTrue then
+ Some (print thy model (Free ("x", T)) argi assignment)
+ else if PropLogic.eval assignment fmFalse then
+ None
+ else
+ raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned"))
+ ((make_constants i) ~~ results)
in
- if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
- raise EMPTY_DATATYPE
- else
- error "sum types (+) not implemented yet (TODO)"
- end
- | Type ("*", [T1,T2]) =>
- let
- val s1 = size_of_type T1 us thy cdepth
- val s2 = size_of_type T2 us thy cdepth
- in
- if s1=0 orelse s2=0 then
- raise EMPTY_DATATYPE
- else
- error "product types (*) not implemented yet (TODO)"
+ Some (enclose "{" "}" (commas strings))
end
- | Type ("fun", [T1,T2]) =>
+ | Var ((x,i), Type ("set", [T])) =>
let
- val s = size_of_type T1 us thy cdepth
+ (* interpretation list *)
+ val results = (case intr of
+ Node xs => xs
+ | _ => raise REFUTE ("var_settype_printer", "interpretation is a leaf"))
+ (* create all constants of type T *)
+ val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T))
+ (* string list *)
+ val strings = mapfilter
+ (fn (argi,Leaf [fmTrue,fmFalse]) =>
+ if PropLogic.eval assignment fmTrue then
+ Some (print thy model (Free ("var_settype_printer", T)) argi assignment)
+ else if PropLogic.eval assignment fmTrue then
+ None
+ else
+ raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned"))
+ ((make_constants i) ~~ results)
in
- if s=0 then
- raise EMPTY_DATATYPE
- else
- map (fn xs => Node xs) (pick_all s (type_to_constants T2 us thy cdepth))
+ Some (enclose "{" "}" (commas strings))
end
- | Type ("set", [T1]) => type_to_constants (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
- | Type (s, _) =>
- (case DatatypePackage.constrs_of thy s of
- Some _ => (* inductive datatype *)
- let
- val s = size_of_type T us thy cdepth
- in
- if s=0 then
- raise EMPTY_DATATYPE
- else
- unit_vectors s
- end
- | None => error ("type_to_constants: type contains an unknown type constructor: '" ^ s ^ "'"))
- | TFree _ => unit_vectors (size_of_type T us thy cdepth)
- | TVar _ => unit_vectors (size_of_type T us thy cdepth)
+ | _ => None
end;
-(* ------------------------------------------------------------------------- *)
-(* prop_tree_equal: returns a propositional formula that is true iff 'tr1' *)
-(* and 'tr2' both denote the same element *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_tree * prop_tree -> prop_formula *)
+ (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
- fun prop_tree_equal (tr1,tr2) =
- case tr1 of
- Leaf x =>
- (case tr2 of
- Leaf y => prop_formula_dot_product (x,y)
- | _ => raise REFUTE ("prop_tree_equal", "second tree is higher"))
- | Node xs =>
- (case tr2 of
- Leaf _ => raise REFUTE ("prop_tree_equal", "first tree is higher")
- (* extensionality: two functions are equal iff they are equal for every element *)
- | Node ys => list_conjunction (map prop_tree_equal (xs ~~ ys)));
+ fun HOLogic_printer thy model t intr assignment =
+ case t of
+ (* 'arbitrary', 'The', 'Hilbert_Choice.Eps' are printed like free variables of the same type *)
+ Const ("arbitrary", T) =>
+ Some (print thy model (Free ("<arbitrary>", T)) intr assignment)
+ | Const ("The", T) =>
+ Some (print thy model (Free ("<The>", T)) intr assignment)
+ | Const ("Hilbert_Choice.Eps", T) =>
+ Some (print thy model (Free ("<Eps>", T)) intr assignment)
+ | _ =>
+ None;
-(* ------------------------------------------------------------------------- *)
-(* prop_tree_apply: returns a tree that denotes the element obtained by *)
-(* applying the function which is denoted by the tree 't1' to the *)
-(* element which is denoted by the tree 't2' *)
-(* ------------------------------------------------------------------------- *)
+ (* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
- (* prop_tree * prop_tree -> prop_tree *)
-
- fun prop_tree_apply (tr1,tr2) =
+ fun var_IDT_printer thy model t intr assignment =
let
- (* prop_tree * prop_tree -> prop_tree *)
- fun prop_tree_disjunction (tr1,tr2) =
- tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
- (* prop_formula * prop_tree -> prop_tree *)
- fun prop_formula_times_prop_tree (fm,tr) =
- tree_map (map (fn x => SAnd (fm,x))) tr
- (* prop_formula list * prop_tree list -> prop_tree *)
- fun prop_formula_list_dot_product_prop_tree_list ([fm],[tr]) =
- prop_formula_times_prop_tree (fm,tr)
- | prop_formula_list_dot_product_prop_tree_list (fm::fms,tr::trees) =
- prop_tree_disjunction (prop_formula_times_prop_tree (fm,tr), prop_formula_list_dot_product_prop_tree_list (fms,trees))
- | prop_formula_list_dot_product_prop_tree_list (_,_) =
- raise REFUTE ("prop_tree_apply::prop_formula_list_dot_product_prop_tree_list", "empty list")
- (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
- (* 'a -> 'a list list -> 'a list list *)
- fun cons_list x xss =
- map (fn xs => x::xs) xss
- (* returns a list of lists, each one consisting of one element from each element of 'xss' *)
- (* 'a list list -> 'a list list *)
- fun pick_all [xs] =
- map (fn x => [x]) xs
- | pick_all (xs::xss) =
- let val rec_pick = pick_all xss in
- foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
- end
- | pick_all _ =
- raise REFUTE ("prop_tree_apply::pick_all", "empty list")
- (* prop_tree -> prop_formula list *)
- fun prop_tree_to_prop_formula_list (Leaf xs) =
- xs
- | prop_tree_to_prop_formula_list (Node trees) =
- map list_conjunction (pick_all (map prop_tree_to_prop_formula_list trees))
+ fun is_var (Free _) = true
+ | is_var (Var _) = true
+ | is_var _ = false
+ fun typeof (Free (_,T)) = T
+ | typeof (Var (_,T)) = T
+ | typeof _ = raise REFUTE ("var_IDT_printer", "term is not a variable")
in
- case tr1 of
- Leaf _ =>
- raise REFUTE ("prop_tree_apply", "first tree is a leaf")
- | Node xs =>
- prop_formula_list_dot_product_prop_tree_list (prop_tree_to_prop_formula_list tr2, xs)
- end
-
-(* ------------------------------------------------------------------------- *)
-(* term_to_prop_tree: translates a HOL term 't' into a tree of propositional *)
-(* formulas; 'us' specifies the number of elements for each type *)
-(* variable in 't'; 'cdepth' specifies the maximal constructor depth *)
-(* for inductive datatypes. Also returns the lowest index that was not *)
-(* used for a boolean variable, and a substitution of terms (free/ *)
-(* schematic variables) by prop_trees. *)
-(* ------------------------------------------------------------------------- *)
-
- (* Term.term -> (Term.typ * int) list -> theory -> int -> prop_tree * (int * (Term.term * prop_tree) list) *)
-
- fun term_to_prop_tree t us thy cdepth =
- let
- (* Term.term -> int * (Term.term * prop_tree) list -> prop_tree * (int * (Term.term * prop_tree) list) *)
- fun variable_to_prop_tree_subst t' (idx,subs) =
- case assoc (subs,t') of
- Some tr =>
- (* return the previously associated tree; the substitution remains unchanged *)
- (tr, (idx,subs))
- | None =>
- (* generate a new tree; update the index; extend the substitution *)
- let
- val T = case t' of
- Free (_,T) => T
- | Var (_,T) => T
- | _ => raise REFUTE ("variable_to_prop_tree_subst", "term is not a (free or schematic) variable")
- val (tr,newidx) = type_to_prop_tree T us thy cdepth idx
- in
- (tr, (newidx, (t',tr)::subs))
- end
- (* Term.term -> int * (Term.term * prop_tree) list -> prop_tree list -> prop_tree * (int * (Term.term * prop_tree) list) *)
- fun term_to_prop_tree_subst t' (idx,subs) bsubs =
- case t' of
- (* meta-logical constants *)
- Const ("Goal", _) $ t1 =>
- term_to_prop_tree_subst t1 (idx,subs) bsubs
- | Const ("all", _) $ t1 =>
- let
- val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
- in
- case tree1 of
- Node xs =>
+ if is_var t then
+ (case typeof t of
+ Type (s, Ts) =>
+ (case DatatypePackage.datatype_info thy s of
+ Some info => (* inductive datatype *)
+ let
+ val index = #index info
+ val descr = #descr info
+ val (_, dtyps, constrs) = the (assoc (descr, index))
+ in
+ if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
+ raise REFUTE ("var_IDT_printer", "recursive datatype argument")
+ else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
+ None (* recursive datatype (requires an infinite model) *)
+ else
let
- val fmTrue = list_conjunction (map prop_tree_to_true xs)
- val fmFalse = list_disjunction (map prop_tree_to_false xs)
+ val (sizes, _) = model
+ val typ_assoc = dtyps ~~ Ts
+ (* interpretation -> int *)
+ fun index_from_interpretation (Leaf xs) =
+ let
+ val idx = find_index (PropLogic.eval assignment) xs
+ in
+ if idx<0 then
+ raise REFUTE ("var_IDT_printer", "illegal interpretation: no value assigned")
+ else
+ idx
+ end
+ | index_from_interpretation _ =
+ raise REFUTE ("var_IDT_printer", "interpretation is not a leaf")
+ (* string -> string *)
+ fun unqualify s =
+ implode (snd (take_suffix (fn c => c <> ".") (explode s)))
+ (* DatatypeAux.dtyp -> Term.typ *)
+ fun typ_of_dtyp (DatatypeAux.DtTFree a) =
+ the (assoc (typ_assoc, DatatypeAux.DtTFree a))
+ | typ_of_dtyp (DatatypeAux.DtRec i) =
+ raise REFUTE ("var_IDT_printer", "recursive datatype")
+ | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
+ Type (s, map typ_of_dtyp ds)
+ fun sum xs = foldl op+ (0, xs)
+ fun product xs = foldl op* (1, xs)
+ (* power(a,b) computes a^b, for a>=0, b>=0 *)
+ (* int * int -> int *)
+ fun power (a,0) = 1
+ | power (a,1) = a
+ | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
+ fun size_of_interpretation (Leaf xs) = length xs
+ | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
+ fun size_of_type T =
+ let
+ val (i,_,_) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<IDT>", T))
+ in
+ size_of_interpretation i
+ end
+ (* returns a list with all unit vectors of length n *)
+ (* int -> interpretation list *)
+ fun unit_vectors n =
+ let
+ (* returns the k-th unit vector of length n *)
+ (* int * int -> interpretation *)
+ fun unit_vector (k,n) =
+ Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
+ (* int -> interpretation list -> interpretation list *)
+ fun unit_vectors_acc k vs =
+ if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
+ in
+ unit_vectors_acc 1 []
+ end
+ (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
+ (* 'a -> 'a list list -> 'a list list *)
+ fun cons_list x xss =
+ map (fn xs => x::xs) xss
+ (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
+ (* int -> 'a list -> 'a list list *)
+ fun pick_all 1 xs =
+ map (fn x => [x]) xs
+ | pick_all n xs =
+ let val rec_pick = pick_all (n-1) xs in
+ foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
+ end
+ (* interpretation -> interpretation list *)
+ fun make_constants (Leaf xs) =
+ unit_vectors (length xs)
+ | make_constants (Node xs) =
+ map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
+ (* DatatypeAux.dtyp list -> int -> string *)
+ fun string_of_inductive_type_cargs [] n =
+ if n<>0 then
+ raise REFUTE ("var_IDT_printer", "internal error computing the element index for an inductive type")
+ else
+ ""
+ | string_of_inductive_type_cargs (d::ds) n =
+ let
+ val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d)) ds)
+ val T = typ_of_dtyp d
+ val (i,_,_) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<IDT>", T))
+ val constants = make_constants i
+ in
+ " "
+ ^ (print thy model (Free ("<IDT>", T)) (nth_elem (n div size_ds, constants)) assignment)
+ ^ (string_of_inductive_type_cargs ds (n mod size_ds))
+ end
+ (* (string * DatatypeAux.dtyp list) list -> int -> string *)
+ fun string_of_inductive_type_constrs [] n =
+ raise REFUTE ("var_IDT_printer", "inductive type has fewer elements than needed")
+ | string_of_inductive_type_constrs ((c,ds)::cs) n =
+ let
+ val size = product (map (fn d => size_of_type (typ_of_dtyp d)) ds)
+ in
+ if n < size then
+ (unqualify c) ^ (string_of_inductive_type_cargs ds n)
+ else
+ string_of_inductive_type_constrs cs (n - size)
+ end
in
- (Leaf [fmTrue, fmFalse], (i1,s1))
+ Some (string_of_inductive_type_constrs constrs (index_from_interpretation intr))
end
- | _ =>
- raise REFUTE ("term_to_prop_tree_subst", "'all' is not followed by a function")
- end
- | Const ("==", _) $ t1 $ t2 =>
- let
- val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
- val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
- val fmTrue = prop_tree_equal (tree1,tree2)
- val fmFalse = SNot fmTrue
- in
- (Leaf [fmTrue, fmFalse], (i2,s2))
- end
- | Const ("==>", _) $ t1 $ t2 =>
- let
- val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
- val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
- val fmTrue = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
- val fmFalse = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
- in
- (Leaf [fmTrue, fmFalse], (i2,s2))
- end
- (* HOL constants *)
- | Const ("Trueprop", _) $ t1 =>
- term_to_prop_tree_subst t1 (idx,subs) bsubs
- | Const ("Not", _) $ t1 =>
- let
- val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
- val fmTrue = prop_tree_to_false tree1
- val fmFalse = prop_tree_to_true tree1
- in
- (Leaf [fmTrue, fmFalse], (i1,s1))
- end
- | Const ("True", _) =>
- (Leaf [True, False], (idx,subs))
- | Const ("False", _) =>
- (Leaf [False, True], (idx,subs))
- | Const ("All", _) $ t1 =>
- let
- val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
- in
- case tree1 of
- Node xs =>
- let
- val fmTrue = list_conjunction (map prop_tree_to_true xs)
- val fmFalse = list_disjunction (map prop_tree_to_false xs)
- in
- (Leaf [fmTrue, fmFalse], (i1,s1))
- end
- | _ =>
- raise REFUTE ("term_to_prop_tree_subst", "'All' is not followed by a function")
- end
- | Const ("Ex", _) $ t1 =>
- let
- val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
- in
- case tree1 of
- Node xs =>
- let
- val fmTrue = list_disjunction (map prop_tree_to_true xs)
- val fmFalse = list_conjunction (map prop_tree_to_false xs)
- in
- (Leaf [fmTrue, fmFalse], (i1,s1))
- end
- | _ =>
- raise REFUTE ("term_to_prop_tree_subst", "'Ex' is not followed by a function")
- end
- | Const ("Ex1", Type ("fun", [Type ("fun", [T, Type ("bool",[])]), Type ("bool",[])])) $ t1 =>
- (* 'Ex1 t1' is equivalent to 'Ex Abs(x,T,t1' x & All Abs(y,T,t1'' y --> x=y))' *)
- let
- val t1' = Term.incr_bv (1, 0, t1)
- val t1'' = Term.incr_bv (2, 0, t1)
- val t_equal = (HOLogic.eq_const T) $ (Bound 1) $ (Bound 0)
- val t_unique = (HOLogic.all_const T) $ Abs("y",T,HOLogic.mk_imp (t1'' $ (Bound 0),t_equal))
- val t_ex1 = (HOLogic.exists_const T) $ Abs("x",T,HOLogic.mk_conj (t1' $ (Bound 0),t_unique))
- in
- term_to_prop_tree_subst t_ex1 (idx,subs) bsubs
- end
- | Const ("op =", _) $ t1 $ t2 =>
- let
- val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
- val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
- val fmTrue = prop_tree_equal (tree1,tree2)
- val fmFalse = SNot fmTrue
- in
- (Leaf [fmTrue, fmFalse], (i2,s2))
- end
- | Const ("op &", _) $ t1 $ t2 =>
- let
- val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
- val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
- val fmTrue = SAnd (prop_tree_to_true tree1, prop_tree_to_true tree2)
- val fmFalse = SOr (prop_tree_to_false tree1, prop_tree_to_false tree2)
- in
- (Leaf [fmTrue, fmFalse], (i2,s2))
- end
- | Const ("op |", _) $ t1 $ t2 =>
- let
- val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
- val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
- val fmTrue = SOr (prop_tree_to_true tree1, prop_tree_to_true tree2)
- val fmFalse = SAnd (prop_tree_to_false tree1, prop_tree_to_false tree2)
- in
- (Leaf [fmTrue, fmFalse], (i2,s2))
- end
- | Const ("op -->", _) $ t1 $ t2 =>
- let
- val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
- val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
- val fmTrue = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
- val fmFalse = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
- in
- (Leaf [fmTrue, fmFalse], (i2,s2))
- end
- (* set constants *)
- | Const ("Collect", _) $ t1 =>
- term_to_prop_tree_subst t1 (idx,subs) bsubs
- | Const ("op :", _) $ t1 $ t2 =>
- term_to_prop_tree_subst (t2 $ t1) (idx,subs) bsubs
- (* datatype constants *)
- | Const ("Product_Type.Unity", _) =>
- (Leaf [True], (idx,subs))
- (* unknown constants *)
- | Const (c, _) =>
- error ("term contains an unknown constant: '" ^ c ^ "'")
- (* abstractions *)
- | Abs (_,T,body) =>
- let
- val constants = type_to_constants T us thy cdepth
- val (trees, substs) = split_list (map (fn c => term_to_prop_tree_subst body (idx,subs) (c::bsubs)) constants)
- in
- (* the substitutions in 'substs' are all identical *)
- (Node trees, hd substs)
- end
- (* (free/schematic) variables *)
- | Free _ =>
- variable_to_prop_tree_subst t' (idx,subs)
- | Var _ =>
- variable_to_prop_tree_subst t' (idx,subs)
- (* bound variables *)
- | Bound i =>
- if (length bsubs) <= i then
- raise REFUTE ("term_to_prop_tree_subst", "term contains a loose bound variable (with index " ^ (string_of_int i) ^ ")")
- else
- (nth_elem (i,bsubs), (idx,subs))
- (* application *)
- | t1 $ t2 =>
- let
- val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
- val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
- in
- (prop_tree_apply (tree1,tree2), (i2,s2))
- end
- in
- term_to_prop_tree_subst t (1,[]) []
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* term_to_prop_formula: translates a HOL formula 't' into a propositional *)
-(* formula that is satisfiable if and only if 't' has a model of "size" *)
-(* 'us' (where 'us' specifies the number of elements for each free type *)
-(* variable in 't') and maximal constructor depth 'cdepth'. *)
-(* ------------------------------------------------------------------------- *)
-
- (* TODO: shouldn't 'us' also specify the number of elements for schematic type variables? (if so, modify the comment above) *)
-
- (* Term.term -> (Term.typ * int) list -> theory -> int -> prop_formula * (int * (Term.term * prop_tree) list) *)
-
- fun term_to_prop_formula t us thy cdepth =
- let
- val (tr, (idx,subs)) = term_to_prop_tree t us thy cdepth
- val fm = prop_tree_to_true tr
- in
- if subs=[] then
- (fm, (idx,subs))
+ end
+ | None => None)
+ | _ => None)
else
- (* make sure every tree that is substituted for a term describes a single element *)
- (SAnd (list_conjunction (map (fn (_,tr) => restrict_to_single_element tr) subs), fm), (idx,subs))
+ None
end;
(* ------------------------------------------------------------------------- *)
-(* INTERFACE, PART 2: FINDING A MODEL *)
+(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
+(* structure *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
-(* string_of_universe: prints a universe, i.e. an assignment of sizes for *)
-(* types *)
-(* thy: the current theory *)
-(* us : a list containing types together with their size *)
-(* ------------------------------------------------------------------------- *)
-
- (* theory -> (Term.typ * int) list -> string *)
-
- fun string_of_universe thy [] =
- "empty universe (no type variables in term)"
- | string_of_universe thy us =
- space_implode ", " (map (fn (T,i) => (Sign.string_of_typ (sign_of thy) T) ^ ": " ^ (string_of_int i)) us);
-
-(* ------------------------------------------------------------------------- *)
-(* string_of_model: prints a model, given by a substitution 'subs' of trees *)
-(* of propositional variables and an assignment 'ass' of truth values *)
-(* for these variables. *)
-(* thy : the current theory *)
-(* us : universe, specifies the "size" of each type (i.e. type variable) *)
-(* cdepth: maximal constructor depth for inductive datatypes *)
-(* subs : substitution of trees of propositional formulas (for variables) *)
-(* ass : assignment of truth values for boolean variables; see function *)
-(* 'truth_value' below for its meaning *)
+(* Note: the interpreters and printers are used in reverse order; however, *)
+(* an interpreter that can handle non-atomic terms ends up being *)
+(* applied before other interpreters are applied to subterms! *)
(* ------------------------------------------------------------------------- *)
- (* theory -> (Term.typ * int) list -> int -> (Term.term * prop_formula tree) list -> int list -> string *)
-
- fun string_of_model thy us cdepth [] ass =
- "empty interpretation (no free variables in term)"
- | string_of_model thy us cdepth subs ass =
- let
- (* Sign.sg *)
- val sg = sign_of thy
- (* int -> bool *)
- fun truth_value i =
- if i mem ass then true
- else if ~i mem ass then false
- else error ("SAT solver assignment does not specify a value for variable " ^ (string_of_int i))
- (* string -> string *)
- fun strip_leading_quote str =
- if nth_elem_string(0,str)="'" then
- String.substring (str, 1, size str - 1)
- else
- str;
- (* prop_formula list -> int *)
- fun true_index xs =
- (* returns the (0-based) index of the first true formula in xs *)
- let fun true_index_acc [] _ =
- raise REFUTE ("string_of_model::true_index", "no variable was set to true")
- | true_index_acc (x::xs) n =
- case x of
- BoolVar i =>
- if truth_value i then n else true_index_acc xs (n+1)
- | True =>
- n
- | False =>
- true_index_acc xs (n+1)
- | _ =>
- raise REFUTE ("string_of_model::true_index", "formula is not a boolean variable/true/false")
- in
- true_index_acc xs 0
- end
- (* Term.typ -> int -> prop_tree -> string *)
- (* prop *)
- fun string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
- if truth_value i then "true" else "false"
- | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [True, False]) =
- "true"
- | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [False, True]) =
- "false"
- (* bool *)
- | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
- if truth_value i then "true" else "false"
- | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [True, False]) =
- "true"
- | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [False, True]) =
- "false"
- (* unit *)
- | string_of_prop_tree (Type ("Product_Type.unit",[])) cdepth (Leaf [True]) =
- "()"
- | string_of_prop_tree (Type (s,Ts)) cdepth (Leaf xs) =
- (case DatatypePackage.datatype_info thy s of
- Some info => (* inductive datatype *)
- let
- val index = #index info
- val descr = #descr info
- val (_, dtyps, constrs) = the (assoc (descr, index))
- val Typs = dtyps ~~ Ts
- (* string -> string *)
- fun unqualify s =
- implode (snd (take_suffix (fn c => c <> ".") (explode s)))
- (* DatatypeAux.dtyp -> Term.typ *)
- fun typ_of_dtyp (DatatypeAux.DtTFree a) =
- the (assoc (Typs, DatatypeAux.DtTFree a))
- | typ_of_dtyp (DatatypeAux.DtRec i) =
- let
- val (s, ds, _) = the (assoc (descr, i))
- in
- Type (s, map typ_of_dtyp ds)
- end
- | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
- Type (s, map typ_of_dtyp ds)
- (* DatatypeAux.dtyp list -> int -> string *)
- fun string_of_inductive_type_cargs [] n =
- if n<>0 then
- raise REFUTE ("string_of_model", "internal error computing the element index for an inductive type")
- else
- ""
- | string_of_inductive_type_cargs (d::ds) n =
- let
- val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
- in
- " " ^ (string_of_prop_tree (typ_of_dtyp d) (cdepth-1) (nth_elem (n div size_ds, type_to_constants (typ_of_dtyp d) us thy (cdepth-1)))) ^ (string_of_inductive_type_cargs ds (n mod size_ds))
- end
- (* (string * DatatypeAux.dtyp list) list -> int -> string *)
- fun string_of_inductive_type_constrs [] n =
- raise REFUTE ("string_of_model", "inductive type has fewer elements than needed")
- | string_of_inductive_type_constrs ((s,ds)::cs) n =
- let
- val size = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
- in
- if n < size then
- (unqualify s) ^ (string_of_inductive_type_cargs ds n)
- else
- string_of_inductive_type_constrs cs (n - size)
- end
- in
- string_of_inductive_type_constrs constrs (true_index xs)
- end
- | None =>
- raise REFUTE ("string_of_model", "type contains an unknown type constructor: '" ^ s ^ "'"))
- (* type variable *)
- | string_of_prop_tree (TFree (s,_)) cdepth (Leaf xs) =
- (strip_leading_quote s) ^ (string_of_int (true_index xs))
- | string_of_prop_tree (TVar ((s,_),_)) cdepth (Leaf xs) =
- (strip_leading_quote s) ^ (string_of_int (true_index xs))
- (* function or set type *)
- | string_of_prop_tree T cdepth (Node xs) =
- case T of
- Type ("fun", [T1,T2]) =>
- let
- val strings = foldl (fn (ss,(c,x)) => ss @ [(string_of_prop_tree T1 cdepth c) ^ "\\<mapsto>" ^ (string_of_prop_tree T2 cdepth x)]) ([], (type_to_constants T1 us thy cdepth) ~~ xs)
- in
- "(" ^ (space_implode ", " strings) ^ ")"
- end
- | Type ("set", [T1]) =>
- let
- val strings = foldl (fn (ss,(c,x)) => if (string_of_prop_tree (Type ("bool",[])) cdepth x)="true" then ss @ [string_of_prop_tree T1 cdepth c] else ss) ([], (type_to_constants T1 us thy cdepth) ~~ xs)
- in
- "{" ^ (space_implode ", " strings) ^ "}"
- end
- | _ => raise REFUTE ("string_of_model::string_of_prop_tree", "not a function/set type")
- (* Term.term * prop_formula tree -> string *)
- fun string_of_term_assignment (t,tr) =
- let
- val T = case t of
- Free (_,T) => T
- | Var (_,T) => T
- | _ => raise REFUTE ("string_of_model::string_of_term_assignment", "term is not a (free or schematic) variable")
- in
- (Sign.string_of_term sg t) ^ " = " ^ (string_of_prop_tree T cdepth tr)
- end
- in
- space_implode "\n" (map string_of_term_assignment subs)
- end;
+ (* (theory -> theory) list *)
-(* ------------------------------------------------------------------------- *)
-(* find_model: repeatedly calls 'prop_formula_sat_solver' with appropriate *)
-(* parameters, and displays the results to the user *)
-(* params : list of '(name, value)' pairs used to override default *)
-(* parameters *)
-(* *)
-(* This is a brief description of the algorithm implemented: *)
-(* *)
-(* 1. Let k = max ('minsize',1). *)
-(* 2. Let the universe have k elements. Find all possible partitions of *)
-(* these elements into the basic types occuring in 't' such that no basic *)
-(* type is empty. *)
-(* 3. Translate 't' into a propositional formula p s.t. 't' has a model wrt. *)
-(* the partition chosen in step (2.) if (actually, if and only if) p is *)
-(* satisfiable. To do this, replace quantification by conjunction/ *)
-(* disjunction over all elements of the type being quantified over. (If *)
-(* p contains more than 'maxvars' boolean variables, terminate.) *)
-(* 4. Serialize p to a file, and try to find a satisfying assignment for p *)
-(* by invoking an external SAT solver. *)
-(* 5. If the SAT solver finds a satisfying assignment for p, translate this *)
-(* assignment back into a model for 't'. Present this model to the user, *)
-(* then terminate. *)
-(* 6. As long as there is another partition left, pick it and go back to *)
-(* step (3.). *)
-(* 7. Increase k by 1. As long as k does not exceed 'maxsize', go back to *)
-(* step (2.). *)
-(* *)
-(* The following parameters are currently supported (and required!): *)
-(* *)
-(* Name Type Description *)
-(* *)
-(* "minsize" int Only search for models with size at least *)
-(* 'minsize'. *)
-(* "maxsize" int If >0, only search for models with size at most *)
-(* 'maxsize'. *)
-(* "maxvars" int If >0, use at most 'maxvars' boolean variables *)
-(* when transforming the term into a propositional *)
-(* formula. *)
-(* "satfile" string Name of the file used to store the propositional *)
-(* formula, i.e. the input to the SAT solver. *)
-(* "satformat" string Format of the SAT solver's input file. Must be *)
-(* either "cnf", "defcnf", or "sat". Since "sat" is *)
-(* not supported by most SAT solvers, and "cnf" can *)
-(* cause exponential blowup of the formula, "defcnf" *)
-(* is recommended. *)
-(* "resultfile" string Name of the file containing the SAT solver's *)
-(* output. *)
-(* "success" string Part of the line in the SAT solver's output that *)
-(* precedes a list of integers representing the *)
-(* satisfying assignment. *)
-(* "command" string System command used to execute the SAT solver. *)
-(* Note that you if you change 'satfile' or *)
-(* 'resultfile', you will also need to change *)
-(* 'command'. *)
-(* *)
-(* See the Isabelle/Isar theory 'Refute.thy' for reasonable default values. *)
-(* ------------------------------------------------------------------------- *)
-
- (* theory -> (string * string) list -> Term.term -> unit *)
-
- fun find_model thy params t =
- let
- (* (string * string) list * (string * string) list -> (string * string) list *)
- fun add_params (parms, []) =
- parms
- | add_params (parms, defparm::defparms) =
- add_params (gen_ins (fn (a, b) => (fst a) = (fst b)) (defparm, parms), defparms)
- (* (string * string) list * string -> int *)
- fun read_int (parms, name) =
- case assoc_string (parms, name) of
- Some s => (case Int.fromString s of
- SOME i => i
- | NONE => error ("parameter '" ^ name ^ "' (value is '" ^ s ^ "') must be an integer value"))
- | None => error ("parameter '" ^ name ^ "' must be assigned a value")
- (* (string * string) list * string -> string *)
- fun read_string (parms, name) =
- case assoc_string (parms, name) of
- Some s => s
- | None => error ("parameter '" ^ name ^ "' must be assigned a value")
- (* (string * string) list *)
- val allparams = add_params (params, get_default_params thy)
- (* int *)
- val minsize = read_int (allparams, "minsize")
- val maxsize = read_int (allparams, "maxsize")
- val maxvars = read_int (allparams, "maxvars")
- (* string *)
- val satfile = read_string (allparams, "satfile")
- val satformat = read_string (allparams, "satformat")
- val resultfile = read_string (allparams, "resultfile")
- val success = read_string (allparams, "success")
- val command = read_string (allparams, "command")
- (* misc *)
- val satpath = Path.unpack satfile
- val resultpath = Path.unpack resultfile
- val sg = sign_of thy
- (* Term.typ list *)
- val tvars = map (fn (i,s) => TVar(i,s)) (term_tvars t)
- val tfrees = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
- (* universe -> int -> bool *)
- fun find_model_universe u cdepth =
- let
- (* given the universe 'u' and constructor depth 'cdepth', translate *)
- (* the term 't' into a propositional formula 'fm' *)
- val (fm,(idx,subs)) = term_to_prop_formula t u thy cdepth
- val usedvars = idx-1
- in
- (* 'maxvars=0' means "use as many variables as necessary" *)
- if usedvars>maxvars andalso maxvars<>0 then
- (
- (* too many variables used: terminate *)
- writeln ("\nSearch terminated: " ^ (string_of_int usedvars) ^ " boolean variables used (only " ^ (string_of_int maxvars) ^ " allowed).");
- true
- )
- else
- (* pass the formula 'fm' to an external SAT solver *)
- case prop_formula_sat_solver fm satpath satformat resultpath success command of
- None =>
- (* no model found *)
- false
- | Some assignment =>
- (* model found: terminate *)
- (
- writeln ("\nModel found:\n" ^ (string_of_universe thy u) ^ "\n" ^ (string_of_model thy u cdepth subs assignment));
- true
- )
- end
- (* universe list -> int -> bool *)
- fun find_model_universes [] cdepth =
- (
- std_output "\n";
- false
- )
- | find_model_universes (u::us) cdepth =
- (
- std_output ".";
- ((if find_model_universe u cdepth then
- (* terminate *)
- true
- else
- (* continue search with the next universe *)
- find_model_universes us cdepth)
- handle EMPTY_DATATYPE => (std_output "[empty inductive type (constructor depth too small)]\n"; false))
- )
- (* int * int -> unit *)
- fun find_model_from_to (min,max) =
- (* 'max=0' means "search for arbitrary large models" *)
- if min>max andalso max<>0 then
- writeln ("Search terminated: no model found.")
- else
- (
- std_output ("Searching for a model of size " ^ (string_of_int min));
- if find_model_universes (make_universes tfrees min) min then
- (* terminate *)
- ()
- else
- (* continue search with increased size *)
- find_model_from_to (min+1, max)
- )
- in
- writeln ("Trying to find a model of: " ^ (Sign.string_of_term sg t));
- if tvars<>[] then
- (* TODO: deal with schematic type variables in a better way, if possible *)
- error "term contains schematic type variables"
- else
- (
- if minsize<1 then
- writeln ("'minsize' is less than 1; starting search with size 1.")
- else
- ();
- if maxsize<max (minsize,1) andalso maxsize<>0 then
- writeln ("'maxsize' is less than 'minsize': no model found.")
- else
- find_model_from_to (max (minsize,1), maxsize)
- )
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* refute_term: calls 'find_model' on the negation of a term *)
-(* params : list of '(name, value)' pairs used to override default *)
-(* parameters *)
-(* ------------------------------------------------------------------------- *)
-
- (* theory -> (string * string) list -> Term.term -> unit *)
-
- fun refute_term thy params t =
- let
- (* TODO: schematic type variables? *)
- val negation = close_vars (HOLogic.Not $ t)
- (* If 't' is of type 'propT' (rather than 'boolT'), applying *)
- (* 'HOLogic.Not' is not type-correct. However, this isn't *)
- (* really a problem as long as 'find_model' still interprets *)
- (* the resulting term correctly, without checking its type. *)
- in
- find_model thy params negation
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* refute_subgoal: calls 'refute_term' on a specific subgoal *)
-(* params : list of '(name, value)' pairs used to override default *)
-(* parameters *)
-(* subgoal : 0-based index specifying the subgoal number *)
-(* ------------------------------------------------------------------------- *)
-
- (* theory -> (string * string) list -> Thm.thm -> int -> unit *)
-
- fun refute_subgoal thy params thm subgoal =
- refute_term thy params (nth_elem (subgoal, prems_of thm));
+ val setup =
+ [RefuteData.init,
+ add_interpreter "var_typevar" var_typevar_interpreter,
+ add_interpreter "var_funtype" var_funtype_interpreter,
+ add_interpreter "var_settype" var_settype_interpreter,
+ add_interpreter "boundvar" boundvar_interpreter,
+ add_interpreter "abstraction" abstraction_interpreter,
+ add_interpreter "apply" apply_interpreter,
+ add_interpreter "const_unfold" const_unfold_interpreter,
+ add_interpreter "Pure" Pure_interpreter,
+ add_interpreter "HOLogic" HOLogic_interpreter,
+ add_interpreter "IDT" IDT_interpreter,
+ add_printer "var_typevar" var_typevar_printer,
+ add_printer "var_funtype" var_funtype_printer,
+ add_printer "var_settype" var_settype_printer,
+ add_printer "HOLogic" HOLogic_printer,
+ add_printer "var_IDT" var_IDT_printer];
end