--- 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
--- 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]: "{} \<in> M"
assumes Int[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M"
@@ -1085,7 +1088,7 @@
using measure_space[of M] by (auto simp: measure_space_def)
definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
- "measure_of \<Omega> A \<mu> = Abs_measure (\<Omega>, sigma_sets \<Omega> A,
+ "measure_of \<Omega> A \<mu> = Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>},
\<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)"
abbreviation "sigma \<Omega> A \<equiv> measure_of \<Omega> A (\<lambda>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 \<Omega> {{}, \<Omega>}"
+by unfold_locales(fastforce intro: exI[where x="{{}}"] exI[where x="{\<Omega>}"])+
+
+lemma measure_space_0': "measure_space \<Omega> {{}, \<Omega>} (\<lambda>x. 0)"
+by(simp add: measure_space_def positive_def countably_additive_def sigma_algebra_trivial)
+
+lemma measure_space_closed:
+ assumes "measure_space \<Omega> M \<mu>"
+ shows "M \<subseteq> Pow \<Omega>"
+proof -
+ interpret sigma_algebra \<Omega> M using assms by(simp add: measure_space_def)
+ show ?thesis by(rule space_closed)
+qed
+
lemma (in ring_of_sets) positive_cong_eq:
"(\<And>a. a \<in> M \<Longrightarrow> \<mu>' a = \<mu> a) \<Longrightarrow> positive M \<mu>' = positive M \<mu>"
by (auto simp add: positive_def)
@@ -1123,26 +1140,37 @@
qed
lemma
- assumes A: "A \<subseteq> Pow \<Omega>"
- shows sets_measure_of[simp]: "sets (measure_of \<Omega> A \<mu>) = sigma_sets \<Omega> A" (is ?sets)
- and space_measure_of[simp]: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space)
+ shows space_measure_of_conv: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space)
+ and sets_measure_of_conv:
+ "sets (measure_of \<Omega> A \<mu>) = (if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>})" (is ?sets)
+ and emeasure_measure_of_conv:
+ "emeasure (measure_of \<Omega> A \<mu>) =
+ (\<lambda>B. if B \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> B else 0)" (is ?emeasure)
proof -
- have "?sets \<and> ?space"
- proof cases
- assume "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
- moreover have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A)
- (\<lambda>a. if a \<in> sigma_sets \<Omega> A then \<mu> a else 0)"
- using A by (rule measure_space_eq) auto
- ultimately show "?sets \<and> ?space"
- by (auto simp: Abs_measure_inverse measure_of_def sets_def space_def)
+ have "?space \<and> ?sets \<and> ?emeasure"
+ proof(cases "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>")
+ case True
+ from measure_space_closed[OF this] sigma_sets_superset_generator[of A \<Omega>]
+ have "A \<subseteq> Pow \<Omega>" by simp
+ hence "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A)
+ (\<lambda>a. if a \<in> sigma_sets \<Omega> A then \<mu> a else 0)"
+ by(rule measure_space_eq) auto
+ with True `A \<subseteq> Pow \<Omega>` show ?thesis
+ by(simp add: measure_of_def space_def sets_def emeasure_def Abs_measure_inverse)
next
- assume "\<not> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
- with A show "?sets \<and> ?space"
- by (auto simp: Abs_measure_inverse measure_of_def sets_def space_def measure_space_0)
+ case False thus ?thesis
+ by(cases "A \<subseteq> Pow \<Omega>")(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 \<subseteq> Pow \<Omega>"
+ shows sets_measure_of: "sets (measure_of \<Omega> A \<mu>) = sigma_sets \<Omega> A"
+ and space_measure_of: "space (measure_of \<Omega> A \<mu>) = \<Omega>"
+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 \<Omega> M \<mu>) = M"
using space_closed by (auto intro!: sigma_sets_eq)
@@ -1193,14 +1221,8 @@
interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)
- moreover have "measure_space \<Omega> (sigma_sets \<Omega> A) (\<lambda>a. if a \<in> sigma_sets \<Omega> A then \<mu> a else 0)
- = measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
- using ms(1) by (rule measure_space_eq) auto
- moreover have "X \<in> sigma_sets \<Omega> 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 \<Omega> M by fact
have "measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
using ms sigma_sets_eq by (simp add: measure_space_def)
- moreover have "measure_space \<Omega> (sigma_sets \<Omega> M) (\<lambda>a. if a \<in> sigma_sets \<Omega> M then \<mu> a else 0)
- = measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
- 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]:
--- 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. *)
--- 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
--- 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;
--- 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
--- 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
--- 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 =
--- 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