--- a/src/HOL/Filter.thy Thu Jun 22 16:31:29 2017 +0100
+++ b/src/HOL/Filter.thy Thu Jun 22 16:49:01 2017 +0100
@@ -556,6 +556,116 @@
by (subst (1 2) eventually_INF) auto
qed
+
+subsubsection \<open>Contravariant map function for filters\<close>
+
+definition filtercomap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter" where
+ "filtercomap f F = Abs_filter (\<lambda>P. \<exists>Q. eventually Q F \<and> (\<forall>x. Q (f x) \<longrightarrow> P x))"
+
+lemma eventually_filtercomap:
+ "eventually P (filtercomap f F) \<longleftrightarrow> (\<exists>Q. eventually Q F \<and> (\<forall>x. Q (f x) \<longrightarrow> P x))"
+ unfolding filtercomap_def
+proof (intro eventually_Abs_filter, unfold_locales, goal_cases)
+ case 1
+ show ?case by (auto intro!: exI[of _ "\<lambda>_. True"])
+next
+ case (2 P Q)
+ from 2(1) guess P' by (elim exE conjE) note P' = this
+ from 2(2) guess Q' by (elim exE conjE) note Q' = this
+ show ?case
+ by (rule exI[of _ "\<lambda>x. P' x \<and> Q' x"])
+ (insert P' Q', auto intro!: eventually_conj)
+next
+ case (3 P Q)
+ thus ?case by blast
+qed
+
+lemma filtercomap_ident: "filtercomap (\<lambda>x. x) F = F"
+ by (auto simp: filter_eq_iff eventually_filtercomap elim!: eventually_mono)
+
+lemma filtercomap_filtercomap: "filtercomap f (filtercomap g F) = filtercomap (\<lambda>x. g (f x)) F"
+ unfolding filter_eq_iff by (auto simp: eventually_filtercomap)
+
+lemma filtercomap_mono: "F \<le> F' \<Longrightarrow> filtercomap f F \<le> filtercomap f F'"
+ by (auto simp: eventually_filtercomap le_filter_def)
+
+lemma filtercomap_bot [simp]: "filtercomap f bot = bot"
+ by (auto simp: filter_eq_iff eventually_filtercomap)
+
+lemma filtercomap_top [simp]: "filtercomap f top = top"
+ by (auto simp: filter_eq_iff eventually_filtercomap)
+
+lemma filtercomap_inf: "filtercomap f (inf F1 F2) = inf (filtercomap f F1) (filtercomap f F2)"
+ unfolding filter_eq_iff
+proof safe
+ fix P
+ assume "eventually P (filtercomap f (F1 \<sqinter> F2))"
+ then obtain Q R S where *:
+ "eventually Q F1" "eventually R F2" "\<And>x. Q x \<Longrightarrow> R x \<Longrightarrow> S x" "\<And>x. S (f x) \<Longrightarrow> P x"
+ unfolding eventually_filtercomap eventually_inf by blast
+ from * have "eventually (\<lambda>x. Q (f x)) (filtercomap f F1)"
+ "eventually (\<lambda>x. R (f x)) (filtercomap f F2)"
+ by (auto simp: eventually_filtercomap)
+ with * show "eventually P (filtercomap f F1 \<sqinter> filtercomap f F2)"
+ unfolding eventually_inf by blast
+next
+ fix P
+ assume "eventually P (inf (filtercomap f F1) (filtercomap f F2))"
+ then obtain Q Q' R R' where *:
+ "eventually Q F1" "eventually R F2" "\<And>x. Q (f x) \<Longrightarrow> Q' x" "\<And>x. R (f x) \<Longrightarrow> R' x"
+ "\<And>x. Q' x \<Longrightarrow> R' x \<Longrightarrow> P x"
+ unfolding eventually_filtercomap eventually_inf by blast
+ from * have "eventually (\<lambda>x. Q x \<and> R x) (F1 \<sqinter> F2)" by (auto simp: eventually_inf)
+ with * show "eventually P (filtercomap f (F1 \<sqinter> F2))"
+ by (auto simp: eventually_filtercomap)
+qed
+
+lemma filtercomap_sup: "filtercomap f (sup F1 F2) \<ge> sup (filtercomap f F1) (filtercomap f F2)"
+ unfolding le_filter_def
+proof safe
+ fix P
+ assume "eventually P (filtercomap f (sup F1 F2))"
+ thus "eventually P (sup (filtercomap f F1) (filtercomap f F2))"
+ by (auto simp: filter_eq_iff eventually_filtercomap eventually_sup)
+qed
+
+lemma filtercomap_INF: "filtercomap f (INF b:B. F b) = (INF b:B. filtercomap f (F b))"
+proof -
+ have *: "filtercomap f (INF b:B. F b) = (INF b:B. filtercomap f (F b))" if "finite B" for B
+ using that by induction (simp_all add: filtercomap_inf)
+ show ?thesis unfolding filter_eq_iff
+ proof
+ fix P
+ have "eventually P (INF b:B. filtercomap f (F b)) \<longleftrightarrow>
+ (\<exists>X. (X \<subseteq> B \<and> finite X) \<and> eventually P (\<Sqinter>b\<in>X. filtercomap f (F b)))"
+ by (subst eventually_INF) blast
+ also have "\<dots> \<longleftrightarrow> (\<exists>X. (X \<subseteq> B \<and> finite X) \<and> eventually P (filtercomap f (INF b:X. F b)))"
+ by (rule ex_cong) (simp add: *)
+ also have "\<dots> \<longleftrightarrow> eventually P (filtercomap f (INFIMUM B F))"
+ unfolding eventually_filtercomap by (subst eventually_INF) blast
+ finally show "eventually P (filtercomap f (INFIMUM B F)) =
+ eventually P (\<Sqinter>b\<in>B. filtercomap f (F b))" ..
+ qed
+qed
+
+lemma filtercomap_SUP_finite:
+ "finite B \<Longrightarrow> filtercomap f (SUP b:B. F b) \<ge> (SUP b:B. filtercomap f (F b))"
+ by (induction B rule: finite_induct)
+ (auto intro: order_trans[OF _ order_trans[OF _ filtercomap_sup]] filtercomap_mono)
+
+lemma eventually_filtercomapI [intro]:
+ assumes "eventually P F"
+ shows "eventually (\<lambda>x. P (f x)) (filtercomap f F)"
+ using assms by (auto simp: eventually_filtercomap)
+
+lemma filtermap_filtercomap: "filtermap f (filtercomap f F) \<le> F"
+ by (auto simp: le_filter_def eventually_filtermap eventually_filtercomap)
+
+lemma filtercomap_filtermap: "filtercomap f (filtermap f F) \<ge> F"
+ unfolding le_filter_def eventually_filtermap eventually_filtercomap
+ by (auto elim!: eventually_mono)
+
+
subsubsection \<open>Standard filters\<close>
definition principal :: "'a set \<Rightarrow> 'a filter" where
@@ -605,6 +715,9 @@
lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
+
+lemma filtercomap_principal[simp]: "filtercomap f (principal A) = principal (f -` A)"
+ unfolding filter_eq_iff eventually_filtercomap eventually_principal by fast
subsubsection \<open>Order filters\<close>
@@ -618,6 +731,10 @@
unfolding at_top_def
by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
+lemma eventually_filtercomap_at_top_linorder:
+ "eventually P (filtercomap f at_top) \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>x. f x \<ge> N \<longrightarrow> P x)"
+ by (auto simp: eventually_filtercomap eventually_at_top_linorder)
+
lemma eventually_at_top_linorderI:
fixes c::"'a::linorder"
assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
@@ -637,6 +754,10 @@
by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
finally show ?thesis .
qed
+
+lemma eventually_filtercomap_at_top_dense:
+ "eventually P (filtercomap f at_top) \<longleftrightarrow> (\<exists>N::'a::{no_top, linorder}. \<forall>x. f x > N \<longrightarrow> P x)"
+ by (auto simp: eventually_filtercomap eventually_at_top_dense)
lemma eventually_at_top_not_equal [simp]: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
unfolding eventually_at_top_dense by auto
@@ -664,6 +785,10 @@
unfolding at_bot_def
by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
+lemma eventually_filtercomap_at_bot_linorder:
+ "eventually P (filtercomap f at_bot) \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>x. f x \<le> N \<longrightarrow> P x)"
+ by (auto simp: eventually_filtercomap eventually_at_bot_linorder)
+
lemma eventually_le_at_bot [simp]:
"eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
unfolding eventually_at_bot_linorder by auto
@@ -678,6 +803,10 @@
finally show ?thesis .
qed
+lemma eventually_filtercomap_at_bot_dense:
+ "eventually P (filtercomap f at_bot) \<longleftrightarrow> (\<exists>N::'a::{no_bot, linorder}. \<forall>x. f x < N \<longrightarrow> P x)"
+ by (auto simp: eventually_filtercomap eventually_at_bot_dense)
+
lemma eventually_at_bot_not_equal [simp]: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
unfolding eventually_at_bot_dense by auto
@@ -1201,6 +1330,9 @@
fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
+
+lemma filterlim_filtercomap [intro]: "filterlim f F (filtercomap f F)"
+ unfolding filterlim_def by (rule filtermap_filtercomap)
subsection \<open>Setup @{typ "'a filter"} for lifting and transfer\<close>
@@ -1390,6 +1522,25 @@
show "rel_filter A (principal S) (principal S')"
by(simp add: rel_filter_eventually eventually_principal) transfer_prover
qed
+
+lemma filtermap_parametric [transfer_rule]:
+ "((A ===> B) ===> rel_filter A ===> rel_filter B) filtermap filtermap"
+proof (intro rel_funI)
+ fix f g F G assume [transfer_rule]: "(A ===> B) f g" "rel_filter A F G"
+ show "rel_filter B (filtermap f F) (filtermap g G)"
+ unfolding rel_filter_eventually eventually_filtermap by transfer_prover
+qed
+
+(* TODO: Are those assumptions needed? *)
+lemma filtercomap_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique B" "bi_total A"
+ shows "((A ===> B) ===> rel_filter B ===> rel_filter A) filtercomap filtercomap"
+proof (intro rel_funI)
+ fix f g F G assume [transfer_rule]: "(A ===> B) f g" "rel_filter B F G"
+ show "rel_filter A (filtercomap f F) (filtercomap g G)"
+ unfolding rel_filter_eventually eventually_filtercomap by transfer_prover
+qed
+
context
fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
@@ -1443,6 +1594,7 @@
declare filterlim_principal [code]
declare principal_prod_principal [code]
declare filtermap_principal [code]
+declare filtercomap_principal [code]
declare eventually_principal [code]
declare inf_principal [code]
declare sup_principal [code]
--- a/src/HOL/Nunchaku/Nunchaku.thy Thu Jun 22 16:31:29 2017 +0100
+++ b/src/HOL/Nunchaku/Nunchaku.thy Thu Jun 22 16:49:01 2017 +0100
@@ -11,7 +11,7 @@
The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
the directory containing the "nunchaku" executable. The Isabelle components
-for CVC4 and Kodkodi are necessary to use these backends.
+for CVC4 and Kodkodi are necessary to use these backend solvers.
*)
theory Nunchaku
--- a/src/HOL/Nunchaku/Tools/nunchaku.ML Thu Jun 22 16:31:29 2017 +0100
+++ b/src/HOL/Nunchaku/Tools/nunchaku.ML Thu Jun 22 16:49:01 2017 +0100
@@ -12,7 +12,8 @@
datatype mode = Auto_Try | Try | Normal
type mode_of_operation_params =
- {falsify: bool,
+ {solvers: string list,
+ falsify: bool,
assms: bool,
spy: bool,
overlord: bool,
@@ -74,7 +75,8 @@
datatype mode = Auto_Try | Try | Normal;
type mode_of_operation_params =
- {falsify: bool,
+ {solvers: string list,
+ falsify: bool,
assms: bool,
spy: bool,
overlord: bool,
@@ -138,7 +140,7 @@
val timeout_slack = seconds 1.0;
fun run_chaku_on_prop state
- ({mode_of_operation_params = {falsify, assms, spy, overlord, expect},
+ ({mode_of_operation_params = {solvers, falsify, assms, spy, overlord, expect},
scope_of_search_params = {wfs, whacks, cards, monos},
output_format_params = {verbose, debug, evals, atomss, ...},
optimization_params = {specialize, ...},
@@ -157,8 +159,9 @@
val das_wort_Model = if falsify then "Countermodel" else "Model";
val das_wort_model = if falsify then "countermodel" else "model";
- val tool_params = {overlord = overlord, debug = debug, specialize = specialize,
- timeout = timeout};
+ val tool_params =
+ {solvers = solvers, overlord = overlord, debug = debug, specialize = specialize,
+ timeout = timeout};
fun run () =
let
--- a/src/HOL/Nunchaku/Tools/nunchaku_commands.ML Thu Jun 22 16:31:29 2017 +0100
+++ b/src/HOL/Nunchaku/Tools/nunchaku_commands.ML Thu Jun 22 16:49:01 2017 +0100
@@ -27,6 +27,7 @@
("max_genuine", "1"),
("max_potential", "1"),
("overlord", "false"),
+ ("solvers", "cvc4 kodkod paradox smbc"),
("specialize", "true"),
("spy", "false"),
("timeout", "30"),
@@ -100,6 +101,7 @@
val raw_lookup = AList.lookup (op =) raw_params;
val lookup = Option.map stringify_raw_param_value o raw_lookup;
val lookup_string = the_default "" o lookup;
+ val lookup_strings = these o Option.map (space_explode " ") o lookup;
fun general_lookup_bool option default_value name =
(case lookup name of
@@ -161,28 +163,33 @@
Const x => x
| t => error ("Not a constant: " ^ Syntax.string_of_term ctxt t));
+ val solvers = lookup_strings "solvers";
+ val falsify = lookup_bool "falsify";
+ val assms = lookup_bool "assms";
+ val spy = getenv "NUNCHAKU_SPY" = "yes" orelse lookup_bool "spy";
+ val overlord = lookup_bool "overlord";
+ val expect = lookup_string "expect";
+
val wfs = lookup_bool_option_assigns read_const_polymorphic "wf";
val whacks = lookup_bool_assigns read_term_polymorphic "whack";
val cards = lookup_int_range_assigns read_type_polymorphic "card";
val monos = lookup_bool_option_assigns read_type_polymorphic "mono";
- val falsify = lookup_bool "falsify";
+
val debug = (mode <> Auto_Try andalso lookup_bool "debug");
val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose");
- val overlord = lookup_bool "overlord";
- val spy = getenv "NUNCHAKU_SPY" = "yes" orelse lookup_bool "spy";
- val assms = lookup_bool "assms";
+ val max_potential = if mode = Normal then Int.max (0, lookup_int "max_potential") else 0;
+ val max_genuine = Int.max (0, lookup_int "max_genuine");
+ val evals = these (lookup_term_list_option_polymorphic "eval");
+ val atomss = lookup_strings_assigns read_type_polymorphic "atoms";
+
val specialize = lookup_bool "specialize";
+ val multithread = mode = Normal andalso lookup_bool "multithread";
+
val timeout = lookup_time "timeout";
val wf_timeout = lookup_time "wf_timeout";
- val multithread = mode = Normal andalso lookup_bool "multithread";
- val evals = these (lookup_term_list_option_polymorphic "eval");
- val atomss = lookup_strings_assigns read_type_polymorphic "atoms";
- val max_potential = if mode = Normal then Int.max (0, lookup_int "max_potential") else 0;
- val max_genuine = Int.max (0, lookup_int "max_genuine");
- val expect = lookup_string "expect";
val mode_of_operation_params =
- {falsify = falsify, assms = assms, spy = spy, overlord = overlord,
+ {solvers = solvers, falsify = falsify, assms = assms, spy = spy, overlord = overlord,
expect = expect};
val scope_of_search_params =
--- a/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Thu Jun 22 16:31:29 2017 +0100
+++ b/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Thu Jun 22 16:49:01 2017 +0100
@@ -12,7 +12,8 @@
type nun_problem = Nunchaku_Problem.nun_problem
type tool_params =
- {overlord: bool,
+ {solvers: string list,
+ overlord: bool,
debug: bool,
specialize: bool,
timeout: Time.time}
@@ -45,7 +46,8 @@
open Nunchaku_Problem;
type tool_params =
- {overlord: bool,
+ {solvers: string list,
+ overlord: bool,
debug: bool,
specialize: bool,
timeout: Time.time};
@@ -73,10 +75,10 @@
val nunchaku_home_env_var = "NUNCHAKU_HOME";
-val cached_outcome =
- Synchronized.var "Nunchaku_Tool.cached_outcome" (NONE : (nun_problem * nun_outcome) option);
+val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome"
+ (NONE : ((string list * nun_problem) * nun_outcome) option);
-fun uncached_solve_nun_problem ({overlord, specialize, timeout, ...} : tool_params)
+fun uncached_solve_nun_problem ({solvers, overlord, specialize, timeout, ...} : tool_params)
(problem as {sound, complete, ...}) =
with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path =>
if getenv nunchaku_home_env_var = "" then
@@ -87,6 +89,7 @@
"PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^
nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
(if specialize then "" else "--no-specialize ") ^
+ "--solvers \"" ^ Bash_Syntax.string (space_implode " " solvers) ^ "\" " ^
"--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
File.bash_path prob_path;
val comments =
@@ -114,23 +117,25 @@
simplify_spaces (elide_string 1000 (if error <> "" then error else output)))
end);
-fun solve_nun_problem (params as {overlord, debug, ...}) problem =
- (case (overlord orelse debug,
- AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) problem) of
- (false, SOME outcome) => outcome
- | _ =>
- let
- val outcome = uncached_solve_nun_problem params problem;
+fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem =
+ let val key = (solvers, problem) in
+ (case (overlord orelse debug,
+ AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) key) of
+ (false, SOME outcome) => outcome
+ | _ =>
+ let
+ val outcome = uncached_solve_nun_problem params problem;
- fun update_cache () =
- Synchronized.change cached_outcome (K (SOME (problem, outcome)));
- in
- (case outcome of
- Unsat => update_cache ()
- | Sat _ => update_cache ()
- | Unknown _ => update_cache ()
- | _ => ());
- outcome
- end);
+ fun update_cache () =
+ Synchronized.change cached_outcome (K (SOME (key, outcome)));
+ in
+ (case outcome of
+ Unsat => update_cache ()
+ | Sat _ => update_cache ()
+ | Unknown _ => update_cache ()
+ | _ => ());
+ outcome
+ end)
+ end;
end;
--- a/src/HOL/Topological_Spaces.thy Thu Jun 22 16:31:29 2017 +0100
+++ b/src/HOL/Topological_Spaces.thy Thu Jun 22 16:49:01 2017 +0100
@@ -662,6 +662,17 @@
shows "eventually P (at_right a)"
using assms unfolding eventually_at_topological by (intro exI[of _ "{..<b}"]) auto
+lemma eventually_filtercomap_nhds:
+ "eventually P (filtercomap f (nhds x)) \<longleftrightarrow> (\<exists>S. open S \<and> x \<in> S \<and> (\<forall>x. f x \<in> S \<longrightarrow> P x))"
+ unfolding eventually_filtercomap eventually_nhds by auto
+
+lemma eventually_filtercomap_at_topological:
+ "eventually P (filtercomap f (at A within B)) \<longleftrightarrow>
+ (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))" (is "?lhs = ?rhs")
+ unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal
+ eventually_filtercomap_nhds eventually_principal by blast
+
+
subsubsection \<open>Tendsto\<close>