# HG changeset patch # User nipkow # Date 1380024443 -7200 # Node ID 9bae89bb032ce816b0a417e51fa0f1f79e227f18 # Parent e55d641d0a706d1c6a3330a9291d1ec43452c702# Parent 9c7e97d67b456167c6b48547f796b262425a88dc merged diff -r 9c7e97d67b45 -r 9bae89bb032c Admin/isatest/isatest-stats --- a/Admin/isatest/isatest-stats Tue Sep 24 13:35:27 2013 +0200 +++ b/Admin/isatest/isatest-stats Tue Sep 24 14:07:23 2013 +0200 @@ -14,6 +14,7 @@ HOL-Auth HOL-BNF HOL-BNF-Examples + HOL-BNF-Nitpick_Examples HOL-BNF-LFP HOL-Bali HOL-Boogie @@ -45,7 +46,6 @@ HOL-NSA HOL-NSA-Examples HOL-NanoJava - HOL-Nitpick_Examples HOL-Nominal HOL-Nominal-Examples HOL-Number_Theory diff -r 9c7e97d67b45 -r 9bae89bb032c src/HOL/Probability/Sigma_Algebra.thy --- a/src/HOL/Probability/Sigma_Algebra.thy Tue Sep 24 13:35:27 2013 +0200 +++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Sep 24 14:07:23 2013 +0200 @@ -74,6 +74,9 @@ qed qed +lemma disjoint_singleton [simp]: "disjoint {A}" +by(simp add: disjoint_def) + locale semiring_of_sets = subset_class + assumes empty_sets[iff]: "{} \ M" assumes Int[intro]: "\a b. a \ M \ b \ M \ a \ b \ M" @@ -1085,7 +1088,7 @@ using measure_space[of M] by (auto simp: measure_space_def) definition measure_of :: "'a set \ 'a set set \ ('a set \ ereal) \ 'a measure" where - "measure_of \ A \ = Abs_measure (\, sigma_sets \ A, + "measure_of \ A \ = Abs_measure (\, if A \ Pow \ then sigma_sets \ A else {{}, \}, \a. if a \ sigma_sets \ A \ measure_space \ (sigma_sets \ A) \ then \ a else 0)" abbreviation "sigma \ A \ measure_of \ A (\x. 0)" @@ -1094,6 +1097,20 @@ unfolding measure_space_def by (auto intro!: sigma_algebra_sigma_sets simp: positive_def countably_additive_def) +lemma sigma_algebra_trivial: "sigma_algebra \ {{}, \}" +by unfold_locales(fastforce intro: exI[where x="{{}}"] exI[where x="{\}"])+ + +lemma measure_space_0': "measure_space \ {{}, \} (\x. 0)" +by(simp add: measure_space_def positive_def countably_additive_def sigma_algebra_trivial) + +lemma measure_space_closed: + assumes "measure_space \ M \" + shows "M \ Pow \" +proof - + interpret sigma_algebra \ M using assms by(simp add: measure_space_def) + show ?thesis by(rule space_closed) +qed + lemma (in ring_of_sets) positive_cong_eq: "(\a. a \ M \ \' a = \ a) \ positive M \' = positive M \" by (auto simp add: positive_def) @@ -1123,26 +1140,37 @@ qed lemma - assumes A: "A \ Pow \" - shows sets_measure_of[simp]: "sets (measure_of \ A \) = sigma_sets \ A" (is ?sets) - and space_measure_of[simp]: "space (measure_of \ A \) = \" (is ?space) + shows space_measure_of_conv: "space (measure_of \ A \) = \" (is ?space) + and sets_measure_of_conv: + "sets (measure_of \ A \) = (if A \ Pow \ then sigma_sets \ A else {{}, \})" (is ?sets) + and emeasure_measure_of_conv: + "emeasure (measure_of \ A \) = + (\B. if B \ sigma_sets \ A \ measure_space \ (sigma_sets \ A) \ then \ B else 0)" (is ?emeasure) proof - - have "?sets \ ?space" - proof cases - assume "measure_space \ (sigma_sets \ A) \" - moreover have "measure_space \ (sigma_sets \ A) \ = measure_space \ (sigma_sets \ A) - (\a. if a \ sigma_sets \ A then \ a else 0)" - using A by (rule measure_space_eq) auto - ultimately show "?sets \ ?space" - by (auto simp: Abs_measure_inverse measure_of_def sets_def space_def) + have "?space \ ?sets \ ?emeasure" + proof(cases "measure_space \ (sigma_sets \ A) \") + case True + from measure_space_closed[OF this] sigma_sets_superset_generator[of A \] + have "A \ Pow \" by simp + hence "measure_space \ (sigma_sets \ A) \ = measure_space \ (sigma_sets \ A) + (\a. if a \ sigma_sets \ A then \ a else 0)" + by(rule measure_space_eq) auto + with True `A \ Pow \` show ?thesis + by(simp add: measure_of_def space_def sets_def emeasure_def Abs_measure_inverse) next - assume "\ measure_space \ (sigma_sets \ A) \" - with A show "?sets \ ?space" - by (auto simp: Abs_measure_inverse measure_of_def sets_def space_def measure_space_0) + case False thus ?thesis + by(cases "A \ Pow \")(simp_all add: Abs_measure_inverse measure_of_def sets_def space_def emeasure_def measure_space_0 measure_space_0') qed - then show ?sets ?space by auto + thus ?space ?sets ?emeasure by simp_all qed +lemma [simp]: + assumes A: "A \ Pow \" + shows sets_measure_of: "sets (measure_of \ A \) = sigma_sets \ A" + and space_measure_of: "space (measure_of \ A \) = \" +using assms +by(simp_all add: sets_measure_of_conv space_measure_of_conv) + lemma (in sigma_algebra) sets_measure_of_eq[simp]: "sets (measure_of \ M \) = M" using space_closed by (auto intro!: sigma_sets_eq) @@ -1193,14 +1221,8 @@ interpret sigma_algebra \ "sigma_sets \ A" by (rule sigma_algebra_sigma_sets) fact have "measure_space \ (sigma_sets \ A) \" using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets) - moreover have "measure_space \ (sigma_sets \ A) (\a. if a \ sigma_sets \ A then \ a else 0) - = measure_space \ (sigma_sets \ A) \" - using ms(1) by (rule measure_space_eq) auto - moreover have "X \ sigma_sets \ A" - using X M ms by simp - ultimately show ?thesis - unfolding emeasure_def measure_of_def M - by (subst Abs_measure_inverse) (simp_all add: sigma_sets_eq) + thus ?thesis using X ms + by(simp add: M emeasure_measure_of_conv sets_measure_of_conv) qed lemma emeasure_measure_of_sigma: @@ -1211,12 +1233,7 @@ interpret sigma_algebra \ M by fact have "measure_space \ (sigma_sets \ M) \" using ms sigma_sets_eq by (simp add: measure_space_def) - moreover have "measure_space \ (sigma_sets \ M) (\a. if a \ sigma_sets \ M then \ a else 0) - = measure_space \ (sigma_sets \ M) \" - using space_closed by (rule measure_space_eq) auto - ultimately show ?thesis using A - unfolding emeasure_def measure_of_def - by (subst Abs_measure_inverse) (simp_all add: sigma_sets_eq) + thus ?thesis by(simp add: emeasure_measure_of_conv A) qed lemma measure_cases[cases type: measure]: diff -r 9c7e97d67b45 -r 9bae89bb032c src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 24 13:35:27 2013 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 24 14:07:23 2013 +0200 @@ -273,7 +273,7 @@ "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n else "goal")) [Logic.list_implies (nondef_assm_ts, orig_t)])) - val _ = spying spy (fn () => "starting " ^ @{make_string} mode ^ " mode") + val _ = spying spy (fn () => (state, i, "starting " ^ @{make_string} mode ^ " mode")) val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S" o Date.fromTimeLocal o Time.now) val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) @@ -1055,7 +1055,7 @@ val _ = print_v (fn () => "Total time: " ^ string_of_time (Timer.checkRealTimer timer) ^ ".") - val _ = spying spy (fn () => "outcome: " ^ outcome_code) + val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code)) in (outcome_code, !state_ref) end (* Give the inner timeout a chance. *) diff -r 9c7e97d67b45 -r 9bae89bb032c src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 24 13:35:27 2013 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 24 14:07:23 2013 +0200 @@ -629,7 +629,6 @@ fun register_codatatype_generic co_T case_name constr_xs generic = let - val ctxt = Context.proof_of generic val thy = Context.theory_of generic val {frac_types, ersatz_table, codatatypes} = Data.get generic val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs diff -r 9c7e97d67b45 -r 9bae89bb032c src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Sep 24 13:35:27 2013 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Sep 24 14:07:23 2013 +0200 @@ -53,7 +53,6 @@ val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option val string_of_time : Time.time -> string - val spying : bool -> (unit -> string) -> unit val nat_subscript : int -> string val flip_polarity : polarity -> polarity val prop_T : typ @@ -79,6 +78,7 @@ val unyxml : string -> string val pretty_maybe_quote : Pretty.T -> Pretty.T val hash_term : term -> int + val spying : bool -> (unit -> Proof.state * int * string) -> unit end; structure Nitpick_Util : NITPICK_UTIL = @@ -242,15 +242,6 @@ val parse_time_option = Sledgehammer_Util.parse_time_option val string_of_time = ATP_Util.string_of_time -val spying_version = "a" - -fun spying false _ = () - | spying true f = - let val message = f () in - File.append (Path.explode "$ISABELLE_HOME_USER/spy_nitpick") - (spying_version ^ " " ^ timestamp () ^ ": " ^ message ^ "\n") - end - val subscript = implode o map (prefix "\<^sub>") o Symbol.explode fun nat_subscript n = n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript @@ -325,4 +316,20 @@ val hash_term = Word.toInt o hashw_term +val hackish_string_of_term = Sledgehammer_Util.hackish_string_of_term + +val spying_version = "b" + +fun spying false _ = () + | spying true f = + let + val (state, i, message) = f () + val ctxt = Proof.context_of state + val goal = Logic.get_goal (prop_of (#goal (Proof.goal state))) i + val hash = String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12) + in + File.append (Path.explode "$ISABELLE_HOME_USER/spy_nitpick") + (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ message ^ "\n") + end + end; diff -r 9c7e97d67b45 -r 9bae89bb032c src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Sep 24 13:35:27 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Sep 24 14:07:23 2013 +0200 @@ -271,9 +271,6 @@ is_package_def name orelse exists (fn s => String.isSuffix s name) blist in is_blisted end -fun hackish_string_of_term ctxt = - with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces - (* This is a terrible hack. Free variables are sometimes coded as "M__" when they are displayed as "M" and we want to avoid clashes with these. But sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all diff -r 9c7e97d67b45 -r 9bae89bb032c src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Sep 24 13:35:27 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Sep 24 14:07:23 2013 +0200 @@ -50,6 +50,7 @@ end val mash_unlearn : Proof.context -> params -> unit + val is_mash_enabled : unit -> bool val nickname_of_thm : thm -> string val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list @@ -89,7 +90,7 @@ -> unit val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit - val is_mash_enabled : unit -> bool + val mash_can_suggest_facts : Proof.context -> bool -> bool val generous_max_facts : int -> int val mepo_weight : real @@ -460,6 +461,8 @@ (*** Isabelle helpers ***) +fun is_mash_enabled () = (getenv "MASH" = "yes") + val local_prefix = "local" ^ Long_Name.separator fun elided_backquote_thm threshold th = @@ -1042,25 +1045,28 @@ fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts used_ths = - launch_thread (timeout |> the_default one_day) (fn () => - let - val thy = Proof_Context.theory_of ctxt - val name = freshish_name () - val feats = - features_of ctxt prover thy 0 Symtab.empty (Local, General) [t] - |> map fst - in - peek_state ctxt overlord (fn {access_G, ...} => - let - val parents = maximal_wrt_access_graph access_G facts - val deps = - used_ths |> filter (is_fact_in_graph access_G) - |> map nickname_of_thm - in - MaSh.learn ctxt overlord true [(name, parents, feats, deps)] - end); - (true, "") - end) + if is_mash_enabled () then + launch_thread (timeout |> the_default one_day) (fn () => + let + val thy = Proof_Context.theory_of ctxt + val name = freshish_name () + val feats = + features_of ctxt prover thy 0 Symtab.empty (Local, General) [t] + |> map fst + in + peek_state ctxt overlord (fn {access_G, ...} => + let + val parents = maximal_wrt_access_graph access_G facts + val deps = + used_ths |> filter (is_fact_in_graph access_G) + |> map nickname_of_thm + in + MaSh.learn ctxt overlord true [(name, parents, feats, deps)] + end); + (true, "") + end) + else + () fun sendback sub = Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub) @@ -1264,7 +1270,6 @@ learn 0 false) end -fun is_mash_enabled () = (getenv "MASH" = "yes") fun mash_can_suggest_facts ctxt overlord = not (Graph.is_empty (#access_G (peek_state ctxt overlord I))) @@ -1310,7 +1315,7 @@ else () fun maybe_learn () = - if learn then + if is_mash_enabled () andalso learn then let val {access_G, num_known_facts, ...} = peek_state ctxt overlord I val is_in_access_G = is_fact_in_graph access_G o snd diff -r 9c7e97d67b45 -r 9bae89bb032c src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Sep 24 13:35:27 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Sep 24 14:07:23 2013 +0200 @@ -73,7 +73,7 @@ val ctxt = Proof.context_of state val hard_timeout = time_mult 3.0 (timeout |> the_default one_day) - val _ = spying spy (fn () => (name, "launched")); + val _ = spying spy (fn () => (state, subgoal, name, "launched")); val birth_time = Time.now () val death_time = Time.+ (birth_time, hard_timeout) val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt slice name) @@ -100,7 +100,7 @@ " proof (of " ^ string_of_int (length facts) ^ "): ") "." |> Output.urgent_message - fun spying_str_of_res {outcome = NONE, used_facts, ...} = + fun spying_str_of_res ({outcome = NONE, used_facts, ...} : prover_result) = let val num_used_facts = length used_facts in "success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^ plural_s num_used_facts @@ -116,7 +116,7 @@ print_used_facts used_facts used_from | _ => ()) |> spy - ? tap (fn res => spying spy (fn () => (name, spying_str_of_res res))) + ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) |> (fn {outcome, preplay, message, message_tail, ...} => (if outcome = SOME ATP_Proof.TimedOut then timeoutN else if is_some outcome then noneN @@ -225,7 +225,8 @@ SOME name => error ("No such prover: " ^ name ^ ".") | NONE => () val _ = print "Sledgehammering..." - val _ = spying spy (fn () => ("***", "starting " ^ @{make_string} mode ^ " mode")) + val _ = + spying spy (fn () => (state, i, "***", "starting " ^ @{make_string} mode ^ " mode")) val (smts, (ueq_atps, full_atps)) = provers |> List.partition (is_smt_prover ctxt) ||> List.partition (is_unit_equational_atp ctxt) @@ -242,8 +243,8 @@ 0 |> fold (Integer.max o default_max_facts_of_prover ctxt slice) provers |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) - val _ = spying spy (fn () => - (label ^ "s", "filtering " ^ string_of_int (length all_facts) ^ " facts")); + val _ = spying spy (fn () => (state, i, label ^ "s", + "filtering " ^ string_of_int (length all_facts) ^ " facts")); in all_facts |> (case is_appropriate_prop of @@ -259,7 +260,8 @@ else ()) |> spy ? tap (fn factss => - spying spy (fn () => (label ^ "s", "selected facts: " ^ spying_str_of_factss factss))) + spying spy (fn () => + (state, i, label ^ "s", "selected facts: " ^ spying_str_of_factss factss))) end fun launch_provers state label is_appropriate_prop provers = diff -r 9c7e97d67b45 -r 9bae89bb032c src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Sep 24 13:35:27 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Sep 24 14:07:23 2013 +0200 @@ -17,7 +17,6 @@ val time_mult : real -> Time.time -> Time.time val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option - val spying : bool -> (unit -> string * string) -> unit val subgoal_count : Proof.state -> int val reserved_isar_keyword_table : unit -> unit Symtab.table val thms_in_proof : @@ -27,6 +26,8 @@ val one_year : Time.time val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b + val hackish_string_of_term : Proof.context -> term -> string + val spying : bool -> (unit -> Proof.state * int * string * string) -> unit (** extrema **) val max : ('a * 'a -> order) -> 'a -> 'a -> 'a @@ -88,15 +89,6 @@ SOME (seconds (the secs)) end -val spying_version = "a" - -fun spying false _ = () - | spying true f = - let val (tool, message) = f () in - File.append (Path.explode "$ISABELLE_HOME_USER/spy_sledgehammer") - (spying_version ^ " " ^ timestamp () ^ ": " ^ tool ^ ": " ^ message ^ "\n") - end - val subgoal_count = Try.subgoal_count fun reserved_isar_keyword_table () = @@ -167,6 +159,23 @@ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x +fun hackish_string_of_term ctxt = + with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces + +val spying_version = "b" + +fun spying false _ = () + | spying true f = + let + val (state, i, tool, message) = f () + val ctxt = Proof.context_of state + val goal = Logic.get_goal (prop_of (#goal (Proof.goal state))) i + val hash = String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12) + in + File.append (Path.explode "$ISABELLE_HOME_USER/spy_sledgehammer") + (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ tool ^ ": " ^ message ^ "\n") + end + (** extrema **) fun max ord x y = case ord(x,y) of LESS => y | _ => x