--- a/NEWS Thu Mar 08 16:43:29 2012 +0000
+++ b/NEWS Thu Mar 08 16:49:24 2012 +0000
@@ -83,11 +83,15 @@
used as predicates by "%x. x : S" and predicates P accidentally used
as sets by "{x. P x}". Corresponding proofs in a first step should be
pruned from any tinkering with former theorems mem_def and
-Collect_def. For developments which deliberately mixed predicates and
+Collect_def as far as possible.
+For developments which deliberately mixed predicates and
sets, a planning step is necessary to determine what should become a
predicate and what a set. It can be helpful to carry out that step in
Isabelle2011-1 before jumping right into the current release.
+* Code generation by default implements sets as container type rather
+than predicates. INCOMPATIBILITY.
+
* New type synonym 'a rel = ('a * 'a) set
* More default pred/set conversions on a couple of relation operations
--- a/src/HOL/IsaMakefile Thu Mar 08 16:43:29 2012 +0000
+++ b/src/HOL/IsaMakefile Thu Mar 08 16:49:24 2012 +0000
@@ -41,7 +41,6 @@
HOL-HOL4 \
HOL-HOL4-Imported \
HOL-HOL_Light \
-# HOL-HOL_Light-Imported \ FIXME not operative at the moment \
HOL-IMPP \
HOL-IOA \
IOA-ABP \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 08 16:43:29 2012 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 08 16:49:24 2012 +0000
@@ -17,12 +17,14 @@
val force_sosK = "force_sos"
val max_relevantK = "max_relevant"
val max_callsK = "max_calls"
-val minimizeK = "minimize"
+val minimizeK = "minimize" (*refers to minimization attempted by Mirabelle*)
val minimize_timeoutK = "minimize_timeout"
val metis_ftK = "metis_ft"
val reconstructorK = "reconstructor"
-
-val preplay_timeout = "4"
+val preplay_timeoutK = "preplay_timeout"
+val sh_minimizeK = "sh_minimize" (*refers to minimizer run within Sledgehammer*)
+val max_new_mono_instancesK = "max_new_mono_instances"
+val max_mono_itersK = "max_mono_iters"
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
@@ -31,6 +33,17 @@
val separator = "-----"
+val preplay_timeout_default = "4"
+(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*)
+
+(*If a key is present in args then augment a list with its pair*)
+(*This is used to avoid fixing default values at the Mirabelle level, and
+ instead use the default values of the tool (Sledgehammer in this case).*)
+fun available_parameter args key label list =
+ let
+ val value = AList.lookup (op =) args key
+ in if is_some value then (label, the value) :: list else list end
+
datatype sh_data = ShData of {
calls: int,
@@ -363,8 +376,9 @@
SH_ERROR
fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans
- uncurried_aliases e_weight_method force_sos hard_timeout timeout dir pos
- st =
+ uncurried_aliases e_weight_method force_sos hard_timeout timeout
+ preplay_timeout sh_minimizeLST max_new_mono_instancesLST max_mono_itersLST
+ dir pos st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val i = 1
@@ -385,7 +399,7 @@
force_sos |> the_default I))
val params as {relevance_thresholds, max_relevant, slice, ...} =
Sledgehammer_Isar.default_params ctxt
- [("verbose", "true"),
+ ([("verbose", "true"),
("type_enc", type_enc),
("strict", strict),
("lam_trans", lam_trans |> the_default "smart"),
@@ -394,6 +408,9 @@
("slice", slice),
("timeout", string_of_int timeout),
("preplay_timeout", preplay_timeout)]
+ |> sh_minimizeLST (*don't confuse the two minimization flags*)
+ |> max_new_mono_instancesLST
+ |> max_mono_itersLST)
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
prover_name
@@ -481,11 +498,18 @@
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
(* always use a hard timeout, but give some slack so that the automatic
minimizer has a chance to do its magic *)
+ val preplay_timeout = AList.lookup (op =) args preplay_timeoutK
+ |> the_default preplay_timeout_default
+ val sh_minimizeLST = available_parameter args sh_minimizeK "minimize"
+ val max_new_mono_instancesLST =
+ available_parameter args max_new_mono_instancesK max_new_mono_instancesK
+ val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
run_sh prover_name prover type_enc strict max_relevant slice lam_trans
- uncurried_aliases e_weight_method force_sos hard_timeout timeout dir pos
- st
+ uncurried_aliases e_weight_method force_sos hard_timeout timeout
+ preplay_timeout sh_minimizeLST max_new_mono_instancesLST max_mono_itersLST
+ dir pos st
in
case result of
SH_OK (time_isa, time_prover, names) =>
@@ -526,13 +550,22 @@
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *)
|> the_default 5
+ val preplay_timeout = AList.lookup (op =) args preplay_timeoutK
+ |> the_default preplay_timeout_default
+ val sh_minimizeLST = available_parameter args sh_minimizeK "minimize"
+ val max_new_mono_instancesLST =
+ available_parameter args max_new_mono_instancesK max_new_mono_instancesK
+ val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
val params = Sledgehammer_Isar.default_params ctxt
- [("provers", prover_name),
+ ([("provers", prover_name),
("verbose", "true"),
("type_enc", type_enc),
("strict", strict),
("timeout", string_of_int timeout),
("preplay_timeout", preplay_timeout)]
+ |> sh_minimizeLST (*don't confuse the two minimization flags*)
+ |> max_new_mono_instancesLST
+ |> max_mono_itersLST)
val minimize =
Sledgehammer_Minimize.minimize_facts prover_name params
true 1 (Sledgehammer_Util.subgoal_count st)
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Thu Mar 08 16:43:29 2012 +0000
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Thu Mar 08 16:49:24 2012 +0000
@@ -26,7 +26,7 @@
echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)"
echo " -O DIR output directory for test data (default $out)"
echo " -t TIMEOUT timeout for each action in seconds (default $timeout)"
- echo " -q be quiet (suppress output of Isabelle process)"
+ echo " -q be quiet (suppress output of Isabelle process)"
echo
echo " Apply the given actions (i.e., automated proof tools)"
echo " at all proof steps in the given theory files."
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu Mar 08 16:43:29 2012 +0000
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu Mar 08 16:49:24 2012 +0000
@@ -67,7 +67,7 @@
$tools
begin
-setup {*
+setup {*
Config.put_global Mirabelle.logfile "$log_file" #>
Config.put_global Mirabelle.timeout $timeout #>
Config.put_global Mirabelle.start_line $start_line #>
@@ -76,7 +76,9 @@
END
-foreach (reverse(split(/:/, $actions))) {
+@action_list = split(/:/, $actions);
+
+foreach (reverse(@action_list)) {
if (m/([^[]*)(?:\[(.*)\])?/) {
my ($name, $settings_str) = ($1, $2 || "");
$name =~ s/^([a-z])/\U$1/;
@@ -88,8 +90,8 @@
$sep = ", ";
}
elsif (m/\s*(.*)\s*/) {
- print SETUP_FILE "$sep(\"$1\", \"\")";
- $sep = ", ";
+ print SETUP_FILE "$sep(\"$1\", \"\")";
+ $sep = ", ";
}
}
print SETUP_FILE "] *}\n";
@@ -121,8 +123,8 @@
open(LOG_FILE, ">$log_file");
print LOG_FILE "Run of $new_thy_file with:\n";
-foreach $name (@action_names) {
- print LOG_FILE " $name\n";
+foreach $action (@action_list) {
+ print LOG_FILE " $action\n";
}
close(LOG_FILE);
--- a/src/HOL/Relation.thy Thu Mar 08 16:43:29 2012 +0000
+++ b/src/HOL/Relation.thy Thu Mar 08 16:49:24 2012 +0000
@@ -60,16 +60,16 @@
subsubsection {* Conversions between set and predicate relations *}
-lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
+lemma pred_equals_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S) \<longleftrightarrow> R = S"
by (simp add: set_eq_iff fun_eq_iff)
-lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
+lemma pred_equals_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S) \<longleftrightarrow> R = S"
by (simp add: set_eq_iff fun_eq_iff)
-lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
+lemma pred_subset_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S) \<longleftrightarrow> R \<subseteq> S"
by (simp add: subset_iff le_fun_def)
-lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
+lemma pred_subset_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S) \<longleftrightarrow> R \<subseteq> S"
by (simp add: subset_iff le_fun_def)
lemma bot_empty_eq (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x. x \<in> {})"
@@ -96,12 +96,54 @@
lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
by (simp add: sup_fun_def)
+lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
+ by (simp add: fun_eq_iff Inf_apply)
+
+(* CANDIDATE
+lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
+ by (simp add: fun_eq_iff INF_apply)
+
+lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (prod_case ` S) Collect)"
+ by (simp add: fun_eq_iff Inf_apply INF_apply)
+
+lemma INF_Int_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Inter>S)"
+ by (simp add: fun_eq_iff INF_apply)
+
+lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> UNION S Collect)"
+ by (simp add: fun_eq_iff Sup_apply)
+
+lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)"
+ by (simp add: fun_eq_iff SUP_apply)
+
+lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (prod_case ` S) Collect)"
+ by (simp add: fun_eq_iff Sup_apply SUP_apply)
+
+lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
+ by (simp add: fun_eq_iff SUP_apply)
+*)
+
+(* CANDIDATE prefer those generalized versions:
+lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i\<in>S. r i))"
+ by (simp add: INF_apply fun_eq_iff)
+
+lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))"
+ by (simp add: INF_apply fun_eq_iff)
+*)
+
lemma INF_INT_eq (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
by (simp add: INF_apply fun_eq_iff)
lemma INF_INT_eq2 (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
by (simp add: INF_apply fun_eq_iff)
+(* CANDIDATE prefer those generalized versions:
+lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i\<in>S. r i))"
+ by (simp add: SUP_apply fun_eq_iff)
+
+lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))"
+ by (simp add: SUP_apply fun_eq_iff)
+*)
+
lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
by (simp add: SUP_apply fun_eq_iff)
--- a/src/HOL/Tools/inductive_set.ML Thu Mar 08 16:43:29 2012 +0000
+++ b/src/HOL/Tools/inductive_set.ML Thu Mar 08 16:49:24 2012 +0000
@@ -227,12 +227,16 @@
fun mk_to_pred_inst thy fs =
map (fn (x, ps) =>
let
- val U = HOLogic.dest_setT (fastype_of x);
- val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
+ val (Ts, T) = strip_type (fastype_of x);
+ val U = HOLogic.dest_setT T;
+ val x' = map_type
+ (K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
in
(cterm_of thy x,
- cterm_of thy (HOLogic.Collect_const U $
- HOLogic.mk_psplits ps U HOLogic.boolT x'))
+ cterm_of thy (fold_rev (Term.abs o pair "x") Ts
+ (HOLogic.Collect_const U $
+ HOLogic.mk_psplits ps U HOLogic.boolT
+ (list_comb (x', map Bound (length Ts - 1 downto 0))))))
end) fs;
fun mk_to_pred_eq p fs optfs' T thm =
@@ -366,12 +370,16 @@
val insts = map (fn (x, ps) =>
let
val Ts = binder_types (fastype_of x);
- val T = HOLogic.mk_ptupleT ps Ts;
- val x' = map_type (K (HOLogic.mk_setT T)) x
+ val l = length Ts;
+ val k = length ps;
+ val (Rs, Us) = chop (l - k - 1) Ts;
+ val T = HOLogic.mk_ptupleT ps Us;
+ val x' = map_type (K (Rs ---> HOLogic.mk_setT T)) x
in
(cterm_of thy x,
cterm_of thy (fold_rev (Term.abs o pair "x") Ts
- (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
+ (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (k downto 0)),
+ list_comb (x', map Bound (l - 1 downto k + 1))))))
end) fs;
in
thm |>
--- a/src/Pure/General/properties.ML Thu Mar 08 16:43:29 2012 +0000
+++ b/src/Pure/General/properties.ML Thu Mar 08 16:49:24 2012 +0000
@@ -6,30 +6,21 @@
signature PROPERTIES =
sig
- type entry = string * string
- type T = entry list
+ type T = (string * string) list
val defined: T -> string -> bool
val get: T -> string -> string option
- val get_int: T -> string -> int option
- val put: entry -> T -> T
- val put_int: string * int -> T -> T
+ val put: string * string -> T -> T
val remove: string -> T -> T
end;
structure Properties: PROPERTIES =
struct
-type entry = string * string;
-type T = entry list;
+type T = (string * string) list;
fun defined (props: T) name = AList.defined (op =) props name;
-
fun get (props: T) name = AList.lookup (op =) props name;
-fun get_int props name = (case get props name of NONE => NONE | SOME s => Int.fromString s);
-
fun put entry (props: T) = AList.update (op =) entry props;
-fun put_int (name, i) = put (name, signed_string_of_int i);
-
fun remove name (props: T) = AList.delete (op =) name props;
end;
--- a/src/Pure/PIDE/yxml.ML Thu Mar 08 16:43:29 2012 +0000
+++ b/src/Pure/PIDE/yxml.ML Thu Mar 08 16:49:24 2012 +0000
@@ -21,7 +21,6 @@
val embed_controls: string -> string
val detect: string -> bool
val output_markup: Markup.T -> string * string
- val element: string -> XML.attributes -> string list -> string
val string_of_body: XML.body -> string
val string_of: XML.tree -> string
val parse_body: string -> XML.body
@@ -62,15 +61,9 @@
if Markup.is_empty markup then Markup.no_output
else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
-fun element name atts body =
- let val (pre, post) = output_markup (name, atts)
- in pre ^ implode body ^ post end;
-
fun string_of_body body =
let
- fun attrib (a, x) =
- Buffer.add Y #>
- Buffer.add a #> Buffer.add "=" #> Buffer.add x;
+ fun attrib (a, x) = Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
fun tree (XML.Elem ((name, atts), ts)) =
Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
trees ts #>
@@ -99,7 +92,7 @@
(* structural errors *)
-fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
+fun err msg = raise Fail ("Malformed YXML: " ^ msg);
fun err_attribute () = err "bad attribute";
fun err_element () = err "bad element";
fun err_unbalanced "" = err "unbalanced element"
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 08 16:43:29 2012 +0000
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 08 16:49:24 2012 +0000
@@ -104,6 +104,9 @@
[Isabelle_Markup.tfreeN, Isabelle_Markup.tvarN, Isabelle_Markup.freeN,
Isabelle_Markup.boundN, Isabelle_Markup.varN, Isabelle_Markup.skolemN];
+fun get_int props name =
+ (case Properties.get props name of NONE => NONE | SOME s => Int.fromString s);
+
in
fun pgml_terms (XML.Elem ((name, atts), body)) =
@@ -114,9 +117,9 @@
let val content = maps pgml_terms body in
if name = Isabelle_Markup.blockN then
[Pgml.Box {orient = NONE,
- indent = Properties.get_int atts Isabelle_Markup.indentN, content = content}]
+ indent = get_int atts Isabelle_Markup.indentN, content = content}]
else if name = Isabelle_Markup.breakN then
- [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Isabelle_Markup.widthN}]
+ [Pgml.Break {mandatory = NONE, indent = get_int atts Isabelle_Markup.widthN}]
else content
end
| pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
--- a/src/Pure/more_thm.ML Thu Mar 08 16:43:29 2012 +0000
+++ b/src/Pure/more_thm.ML Thu Mar 08 16:49:24 2012 +0000
@@ -79,9 +79,9 @@
val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
val no_attributes: 'a -> 'a * 'b list
val simple_fact: 'a -> ('a * 'b list) list
- val tag_rule: Properties.entry -> thm -> thm
+ val tag_rule: string * string -> thm -> thm
val untag_rule: string -> thm -> thm
- val tag: Properties.entry -> attribute
+ val tag: string * string -> attribute
val untag: string -> attribute
val def_name: string -> string
val def_name_optional: string -> string -> string