# HG changeset patch # User paulson # Date 1498146541 -3600 # Node ID 48cfbccaf3f459ac3782e37959a01a9106834e4e # Parent 2d79288b042c851f6b4fad082a7850036644b1f7# Parent 45d3d43abee7147fd43e63a6b4ba6340a5d4b74f Merge diff -r 2d79288b042c -r 48cfbccaf3f4 src/HOL/Filter.thy --- 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 \Contravariant map function for filters\ + +definition filtercomap :: "('a \ 'b) \ 'b filter \ 'a filter" where + "filtercomap f F = Abs_filter (\P. \Q. eventually Q F \ (\x. Q (f x) \ P x))" + +lemma eventually_filtercomap: + "eventually P (filtercomap f F) \ (\Q. eventually Q F \ (\x. Q (f x) \ P x))" + unfolding filtercomap_def +proof (intro eventually_Abs_filter, unfold_locales, goal_cases) + case 1 + show ?case by (auto intro!: exI[of _ "\_. 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 _ "\x. P' x \ Q' x"]) + (insert P' Q', auto intro!: eventually_conj) +next + case (3 P Q) + thus ?case by blast +qed + +lemma filtercomap_ident: "filtercomap (\x. x) F = F" + by (auto simp: filter_eq_iff eventually_filtercomap elim!: eventually_mono) + +lemma filtercomap_filtercomap: "filtercomap f (filtercomap g F) = filtercomap (\x. g (f x)) F" + unfolding filter_eq_iff by (auto simp: eventually_filtercomap) + +lemma filtercomap_mono: "F \ F' \ filtercomap f F \ 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 \ F2))" + then obtain Q R S where *: + "eventually Q F1" "eventually R F2" "\x. Q x \ R x \ S x" "\x. S (f x) \ P x" + unfolding eventually_filtercomap eventually_inf by blast + from * have "eventually (\x. Q (f x)) (filtercomap f F1)" + "eventually (\x. R (f x)) (filtercomap f F2)" + by (auto simp: eventually_filtercomap) + with * show "eventually P (filtercomap f F1 \ 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" "\x. Q (f x) \ Q' x" "\x. R (f x) \ R' x" + "\x. Q' x \ R' x \ P x" + unfolding eventually_filtercomap eventually_inf by blast + from * have "eventually (\x. Q x \ R x) (F1 \ F2)" by (auto simp: eventually_inf) + with * show "eventually P (filtercomap f (F1 \ F2))" + by (auto simp: eventually_filtercomap) +qed + +lemma filtercomap_sup: "filtercomap f (sup F1 F2) \ 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)) \ + (\X. (X \ B \ finite X) \ eventually P (\b\X. filtercomap f (F b)))" + by (subst eventually_INF) blast + also have "\ \ (\X. (X \ B \ finite X) \ eventually P (filtercomap f (INF b:X. F b)))" + by (rule ex_cong) (simp add: *) + also have "\ \ 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 (\b\B. filtercomap f (F b))" .. + qed +qed + +lemma filtercomap_SUP_finite: + "finite B \ filtercomap f (SUP b:B. F b) \ (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 (\x. P (f x)) (filtercomap f F)" + using assms by (auto simp: eventually_filtercomap) + +lemma filtermap_filtercomap: "filtermap f (filtercomap f F) \ F" + by (auto simp: le_filter_def eventually_filtermap eventually_filtercomap) + +lemma filtercomap_filtermap: "filtercomap f (filtermap f F) \ F" + unfolding le_filter_def eventually_filtermap eventually_filtercomap + by (auto elim!: eventually_mono) + + subsubsection \Standard filters\ definition principal :: "'a set \ '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 \Order filters\ @@ -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) \ (\N::'a::linorder. \x. f x \ N \ P x)" + by (auto simp: eventually_filtercomap eventually_at_top_linorder) + lemma eventually_at_top_linorderI: fixes c::"'a::linorder" assumes "\x. c \ x \ 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) \ (\N::'a::{no_top, linorder}. \x. f x > N \ P x)" + by (auto simp: eventually_filtercomap eventually_at_top_dense) lemma eventually_at_top_not_equal [simp]: "eventually (\x::'a::{no_top, linorder}. x \ 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) \ (\N::'a::linorder. \x. f x \ N \ P x)" + by (auto simp: eventually_filtercomap eventually_at_bot_linorder) + lemma eventually_le_at_bot [simp]: "eventually (\x. x \ (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) \ (\N::'a::{no_bot, linorder}. \x. f x < N \ P x)" + by (auto simp: eventually_filtercomap eventually_at_bot_dense) + lemma eventually_at_bot_not_equal [simp]: "eventually (\x::'a::{no_bot, linorder}. x \ c) at_bot" unfolding eventually_at_bot_dense by auto @@ -1201,6 +1330,9 @@ fixes f :: "'a \ ('b::unbounded_dense_linorder)" and c :: "'b" shows "(LIM x F. f x :> at_bot) \ (\Zx. Z \ 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 \Setup @{typ "'a filter"} for lifting and transfer\ @@ -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 \ 'b \ 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] diff -r 2d79288b042c -r 48cfbccaf3f4 src/HOL/Nunchaku/Nunchaku.thy --- 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 diff -r 2d79288b042c -r 48cfbccaf3f4 src/HOL/Nunchaku/Tools/nunchaku.ML --- 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 diff -r 2d79288b042c -r 48cfbccaf3f4 src/HOL/Nunchaku/Tools/nunchaku_commands.ML --- 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 = diff -r 2d79288b042c -r 48cfbccaf3f4 src/HOL/Nunchaku/Tools/nunchaku_tool.ML --- 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; diff -r 2d79288b042c -r 48cfbccaf3f4 src/HOL/Topological_Spaces.thy --- 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 _ "{.. (\S. open S \ x \ S \ (\x. f x \ S \ P x))" + unfolding eventually_filtercomap eventually_nhds by auto + +lemma eventually_filtercomap_at_topological: + "eventually P (filtercomap f (at A within B)) \ + (\S. open S \ A \ S \ (\x. f x \ S \ B - {A} \ P x))" (is "?lhs = ?rhs") + unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal + eventually_filtercomap_nhds eventually_principal by blast + + subsubsection \Tendsto\