merged
authorwenzelm
Thu, 06 Dec 2012 11:42:23 +0100
changeset 50400 fe9223fdd060
parent 50399 52d9720f7a48 (diff)
parent 50381 d9711842f1f9 (current diff)
child 50401 8e5d7ef3da76
merged
--- a/src/HOL/Probability/Borel_Space.thy	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Thu Dec 06 11:42:23 2012 +0100
@@ -6,7 +6,9 @@
 header {*Borel spaces*}
 
 theory Borel_Space
-  imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
+imports
+  Measurable
+  "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
 begin
 
 section "Generic Borel spaces"
@@ -33,7 +35,7 @@
 lemma space_in_borel[measurable]: "UNIV \<in> sets borel"
   unfolding borel_def by auto
 
-lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
+lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
   unfolding borel_def pred_def by auto
 
 lemma borel_open[measurable (raw generic)]:
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Thu Dec 06 11:42:23 2012 +0100
@@ -513,7 +513,7 @@
 lemma sets_in_Pi[measurable (raw)]:
   "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
   (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
-  Sigma_Algebra.pred N (\<lambda>x. f x \<in> Pi I F)"
+  Measurable.pred N (\<lambda>x. f x \<in> Pi I F)"
   unfolding pred_def
   by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
 
@@ -526,7 +526,7 @@
 qed
 
 lemma sets_in_extensional[measurable (raw)]:
-  "f \<in> measurable N (PiM I M) \<Longrightarrow> Sigma_Algebra.pred N (\<lambda>x. f x \<in> extensional I)"
+  "f \<in> measurable N (PiM I M) \<Longrightarrow> Measurable.pred N (\<lambda>x. f x \<in> extensional I)"
   unfolding pred_def
   by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
 
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Dec 06 11:42:23 2012 +0100
@@ -2274,6 +2274,87 @@
     using int(2) by simp
 qed
 
+lemma integrable_mult_indicator:
+  "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. f x * indicator A x)"
+  by (rule integrable_bound[where f="\<lambda>x. \<bar>f x\<bar>"])
+     (auto intro: integrable_abs split: split_indicator)
+
+lemma tendsto_integral_at_top:
+  fixes M :: "real measure"
+  assumes M: "sets M = sets borel" and f[measurable]: "integrable M f"
+  shows "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
+proof -
+  have M_measure[simp]: "borel_measurable M = borel_measurable borel"
+    using M by (simp add: sets_eq_imp_space_eq measurable_def)
+  { fix f assume f: "integrable M f" "\<And>x. 0 \<le> f x"
+    then have [measurable]: "f \<in> borel_measurable borel"
+      by (simp add: integrable_def)
+    have "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
+    proof (rule tendsto_at_topI_sequentially)
+      have "\<And>j. AE x in M. \<bar>f x * indicator {.. j} x\<bar> \<le> f x"
+        using f(2) by (intro AE_I2) (auto split: split_indicator)
+      have int: "\<And>n. integrable M (\<lambda>x. f x * indicator {.. n} x)"
+        by (rule integrable_mult_indicator) (auto simp: M f)
+      show "(\<lambda>n. \<integral> x. f x * indicator {..real n} x \<partial>M) ----> integral\<^isup>L M f"
+      proof (rule integral_dominated_convergence)
+        { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
+            by (rule eventually_sequentiallyI[of "natceiling x"])
+               (auto split: split_indicator simp: natceiling_le_eq) }
+        from filterlim_cong[OF refl refl this]
+        show "AE x in M. (\<lambda>n. f x * indicator {..real n} x) ----> f x"
+          by (simp add: tendsto_const)
+      qed (fact+, simp)
+      show "mono (\<lambda>y. \<integral> x. f x * indicator {..y} x \<partial>M)"
+        by (intro monoI integral_mono int) (auto split: split_indicator intro: f)
+    qed }
+  note nonneg = this
+  let ?P = "\<lambda>y. \<integral> x. max 0 (f x) * indicator {..y} x \<partial>M"
+  let ?N = "\<lambda>y. \<integral> x. max 0 (- f x) * indicator {..y} x \<partial>M"
+  let ?p = "integral\<^isup>L M (\<lambda>x. max 0 (f x))"
+  let ?n = "integral\<^isup>L M (\<lambda>x. max 0 (- f x))"
+  have "(?P ---> ?p) at_top" "(?N ---> ?n) at_top"
+    by (auto intro!: nonneg integrable_max f)
+  note tendsto_diff[OF this]
+  also have "(\<lambda>y. ?P y - ?N y) = (\<lambda>y. \<integral> x. f x * indicator {..y} x \<partial>M)"
+    by (subst integral_diff(2)[symmetric])
+       (auto intro!: integrable_mult_indicator integrable_max f integral_cong ext
+             simp: M split: split_max)
+  also have "?p - ?n = integral\<^isup>L M f"
+    by (subst integral_diff(2)[symmetric])
+       (auto intro!: integrable_max f integral_cong ext simp: M split: split_max)
+  finally show ?thesis .
+qed
+
+lemma integral_monotone_convergence_at_top:
+  fixes M :: "real measure"
+  assumes M: "sets M = sets borel"
+  assumes nonneg: "AE x in M. 0 \<le> f x"
+  assumes borel: "f \<in> borel_measurable borel"
+  assumes int: "\<And>y. integrable M (\<lambda>x. f x * indicator {.. y} x)"
+  assumes conv: "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> x) at_top"
+  shows "integrable M f" "integral\<^isup>L M f = x"
+proof -
+  from nonneg have "AE x in M. mono (\<lambda>n::nat. f x * indicator {..real n} x)"
+    by (auto split: split_indicator intro!: monoI)
+  { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
+      by (rule eventually_sequentiallyI[of "natceiling x"])
+         (auto split: split_indicator simp: natceiling_le_eq) }
+  from filterlim_cong[OF refl refl this]
+  have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"
+    by (simp add: tendsto_const)
+  have "(\<lambda>i. \<integral> x. f x * indicator {..real i} x \<partial>M) ----> x"
+    using conv filterlim_real_sequentially by (rule filterlim_compose)
+  have M_measure[simp]: "borel_measurable M = borel_measurable borel"
+    using M by (simp add: sets_eq_imp_space_eq measurable_def)
+  have "f \<in> borel_measurable M"
+    using borel by simp
+  show "integrable M f"
+    by (rule integral_monotone_convergence) fact+
+  show "integral\<^isup>L M f = x"
+    by (rule integral_monotone_convergence) fact+
+qed
+
+
 section "Lebesgue integration on countable spaces"
 
 lemma integral_on_countable:
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Thu Dec 06 11:42:23 2012 +0100
@@ -941,8 +941,8 @@
 qed (auto simp: e2p_def)
 
 (* FIXME: conversion in measurable prover *)
-lemma lborelD_Collect[measurable]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
-lemma lborelD[measurable]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
+lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
+lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
 
 lemma measurable_p2e[measurable]:
   "p2e \<in> measurable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure))
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Measurable.thy	Thu Dec 06 11:42:23 2012 +0100
@@ -0,0 +1,247 @@
+(*  Title:      HOL/Probability/measurable.ML
+    Author:     Johannes Hölzl <hoelzl@in.tum.de>
+*)
+theory Measurable
+  imports Sigma_Algebra
+begin
+
+subsection {* Measurability prover *}
+
+lemma (in algebra) sets_Collect_finite_All:
+  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
+  shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
+proof -
+  have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (if S = {} then \<Omega> else \<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"
+    by auto
+  with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
+qed
+
+abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
+
+lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
+proof
+  assume "pred M P"
+  then have "P -` {True} \<inter> space M \<in> sets M"
+    by (auto simp: measurable_count_space_eq2)
+  also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
+  finally show "{x\<in>space M. P x} \<in> sets M" .
+next
+  assume P: "{x\<in>space M. P x} \<in> sets M"
+  moreover
+  { fix X
+    have "X \<in> Pow (UNIV :: bool set)" by simp
+    then have "P -` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}"
+      unfolding UNIV_bool Pow_insert Pow_empty by auto
+    then have "P -` X \<inter> space M \<in> sets M"
+      by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
+  then show "pred M P"
+    by (auto simp: measurable_def)
+qed
+
+lemma pred_sets1: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> f \<in> measurable N M \<Longrightarrow> pred N (\<lambda>x. P (f x))"
+  by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
+
+lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
+  by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
+
+ML_file "measurable.ML"
+
+attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
+attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
+attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover"
+method_setup measurable = {* Measurable.method *} "measurability prover"
+simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
+
+declare
+  measurable_compose_rev[measurable_dest]
+  pred_sets1[measurable_dest]
+  pred_sets2[measurable_dest]
+  sets.sets_into_space[measurable_dest]
+
+declare
+  sets.top[measurable]
+  sets.empty_sets[measurable (raw)]
+  sets.Un[measurable (raw)]
+  sets.Diff[measurable (raw)]
+
+declare
+  measurable_count_space[measurable (raw)]
+  measurable_ident[measurable (raw)]
+  measurable_ident_sets[measurable (raw)]
+  measurable_const[measurable (raw)]
+  measurable_If[measurable (raw)]
+  measurable_comp[measurable (raw)]
+  measurable_sets[measurable (raw)]
+
+lemma predE[measurable (raw)]: 
+  "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
+  unfolding pred_def .
+
+lemma pred_intros_imp'[measurable (raw)]:
+  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
+  by (cases K) auto
+
+lemma pred_intros_conj1'[measurable (raw)]:
+  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
+  by (cases K) auto
+
+lemma pred_intros_conj2'[measurable (raw)]:
+  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
+  by (cases K) auto
+
+lemma pred_intros_disj1'[measurable (raw)]:
+  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
+  by (cases K) auto
+
+lemma pred_intros_disj2'[measurable (raw)]:
+  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
+  by (cases K) auto
+
+lemma pred_intros_logic[measurable (raw)]:
+  "pred M (\<lambda>x. x \<in> space M)"
+  "pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
+  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
+  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
+  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
+  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
+  "pred M (\<lambda>x. f x \<in> UNIV)"
+  "pred M (\<lambda>x. f x \<in> {})"
+  "pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})"
+  "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
+  "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) - (B x))"
+  "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))"
+  "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<union> (B x))"
+  "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
+  by (auto simp: iff_conv_conj_imp pred_def)
+
+lemma pred_intros_countable[measurable (raw)]:
+  fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
+  shows 
+    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
+    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
+  by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
+
+lemma pred_intros_countable_bounded[measurable (raw)]:
+  fixes X :: "'i :: countable set"
+  shows 
+    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>X. N x i))"
+    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>X. N x i))"
+    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
+    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
+  by (auto simp: Bex_def Ball_def)
+
+lemma pred_intros_finite[measurable (raw)]:
+  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))"
+  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))"
+  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)"
+  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)"
+  by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
+
+lemma countable_Un_Int[measurable (raw)]:
+  "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
+  "I \<noteq> {} \<Longrightarrow> (\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Inter>i\<in>I. N i) \<in> sets M"
+  by auto
+
+declare
+  finite_UN[measurable (raw)]
+  finite_INT[measurable (raw)]
+
+lemma sets_Int_pred[measurable (raw)]:
+  assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
+  shows "A \<inter> B \<in> sets M"
+proof -
+  have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
+  also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
+    using space by auto
+  finally show ?thesis .
+qed
+
+lemma [measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N"
+  shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
+    and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
+proof -
+  show "pred M (\<lambda>x. f x = c)"
+  proof cases
+    assume "c \<in> space N"
+    with measurable_sets[OF f c] show ?thesis
+      by (auto simp: Int_def conj_commute pred_def)
+  next
+    assume "c \<notin> space N"
+    with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto
+    then show ?thesis by (auto simp: pred_def cong: conj_cong)
+  qed
+  then show "pred M (\<lambda>x. c = f x)"
+    by (simp add: eq_commute)
+qed
+
+lemma pred_le_const[measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
+  using measurable_sets[OF f c]
+  by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_const_le[measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
+  using measurable_sets[OF f c]
+  by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_less_const[measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
+  using measurable_sets[OF f c]
+  by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_const_less[measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
+  using measurable_sets[OF f c]
+  by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+declare
+  sets.Int[measurable (raw)]
+
+lemma pred_in_If[measurable (raw)]:
+  "(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>
+    pred M (\<lambda>x. x \<in> (if P then A x else B x))"
+  by auto
+
+lemma sets_range[measurable_dest]:
+  "A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"
+  by auto
+
+lemma pred_sets_range[measurable_dest]:
+  "A ` I \<subseteq> sets N \<Longrightarrow> i \<in> I \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
+  using pred_sets2[OF sets_range] by auto
+
+lemma sets_All[measurable_dest]:
+  "\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"
+  by auto
+
+lemma pred_sets_All[measurable_dest]:
+  "\<forall>i. A i \<in> sets (N i) \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
+  using pred_sets2[OF sets_All, of A N f] by auto
+
+lemma sets_Ball[measurable_dest]:
+  "\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"
+  by auto
+
+lemma pred_sets_Ball[measurable_dest]:
+  "\<forall>i\<in>I. A i \<in> sets (N i) \<Longrightarrow> i\<in>I \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
+  using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
+
+lemma measurable_finite[measurable (raw)]:
+  fixes S :: "'a \<Rightarrow> nat set"
+  assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
+  shows "pred M (\<lambda>x. finite (S x))"
+  unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
+
+lemma measurable_Least[measurable]:
+  assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q
+  shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
+  unfolding measurable_def by (safe intro!: sets_Least) simp_all
+
+lemma measurable_count_space_insert[measurable (raw)]:
+  "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
+  by simp
+
+hide_const (open) pred
+
+end
--- a/src/HOL/Probability/Measure_Space.thy	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Thu Dec 06 11:42:23 2012 +0100
@@ -8,7 +8,7 @@
 
 theory Measure_Space
 imports
-  Sigma_Algebra
+  Measurable
   "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
 begin
 
--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Dec 06 11:42:23 2012 +0100
@@ -252,7 +252,7 @@
   "X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }"
   by (auto simp: algebra_iff_Int)
 
-section {* Restricted algebras *}
+subsection {* Restricted algebras *}
 
 abbreviation (in algebra)
   "restricted_space A \<equiv> (op \<inter> A) ` M"
@@ -707,7 +707,7 @@
   qed
 qed
 
-section "Disjoint families"
+subsection "Disjoint families"
 
 definition
   disjoint_family_on  where
@@ -866,7 +866,7 @@
     by (intro disjointD[OF d]) auto
 qed
 
-section {* Ring generated by a semiring *}
+subsection {* Ring generated by a semiring *}
 
 definition (in semiring_of_sets)
   "generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
@@ -996,7 +996,7 @@
     by (blast intro!: sigma_sets_mono elim: generated_ringE)
 qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
 
-section {* Measure type *}
+subsection {* Measure type *}
 
 definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
   "positive M \<mu> \<longleftrightarrow> \<mu> {} = 0 \<and> (\<forall>A\<in>M. 0 \<le> \<mu> A)"
@@ -1138,7 +1138,7 @@
 lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
   by auto
 
-section {* Constructing simple @{typ "'a measure"} *}
+subsection {* Constructing simple @{typ "'a measure"} *}
 
 lemma emeasure_measure_of:
   assumes M: "M = measure_of \<Omega> A \<mu>"
@@ -1231,7 +1231,7 @@
   shows "sigma \<Omega> M = sigma \<Omega> N"
   by (rule measure_eqI) (simp_all add: emeasure_sigma)
 
-section {* Measurable functions *}
+subsection {* Measurable functions *}
 
 definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" where
   "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
@@ -1428,7 +1428,7 @@
     measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"
   using measure_of_subset[of M' \<Omega> M] by (auto simp add: measurable_def)
 
-section {* Counting space *}
+subsection {* Counting space *}
 
 definition count_space :: "'a set \<Rightarrow> 'a measure" where
   "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then ereal (card A) else \<infinity>)"
@@ -1473,45 +1473,6 @@
   finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
 qed
 
-subsection {* Measurable method *}
-
-lemma (in algebra) sets_Collect_finite_All:
-  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
-  shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
-proof -
-  have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (if S = {} then \<Omega> else \<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"
-    by auto
-  with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
-qed
-
-abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
-
-lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
-proof
-  assume "pred M P"
-  then have "P -` {True} \<inter> space M \<in> sets M"
-    by (auto simp: measurable_count_space_eq2)
-  also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
-  finally show "{x\<in>space M. P x} \<in> sets M" .
-next
-  assume P: "{x\<in>space M. P x} \<in> sets M"
-  moreover
-  { fix X
-    have "X \<in> Pow (UNIV :: bool set)" by simp
-    then have "P -` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}"
-      unfolding UNIV_bool Pow_insert Pow_empty by auto
-    then have "P -` X \<inter> space M \<in> sets M"
-      by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
-  then show "pred M P"
-    by (auto simp: measurable_def)
-qed
-
-lemma pred_sets1: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> f \<in> measurable N M \<Longrightarrow> pred N (\<lambda>x. P (f x))"
-  by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
-
-lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
-  by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
-
 lemma measurable_count_space_const:
   "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
   by (simp add: measurable_const)
@@ -1525,418 +1486,6 @@
   shows "(\<lambda>x. f (g x)) \<in> measurable M N"
   using measurable_compose[OF g f] .
 
-ML {*
-
-structure Measurable =
-struct
-
-datatype level = Concrete | Generic;
-
-structure Data = Generic_Data
-(
-  type T = {
-    concrete_thms : thm Item_Net.T,
-    generic_thms : thm Item_Net.T,
-    dest_thms : thm Item_Net.T,
-    app_thms : thm Item_Net.T }
-  val empty = {
-    concrete_thms = Thm.full_rules,
-    generic_thms = Thm.full_rules,
-    dest_thms = Thm.full_rules,
-    app_thms = Thm.full_rules};
-  val extend = I;
-  fun merge ({concrete_thms = ct1, generic_thms = gt1, dest_thms = dt1, app_thms = at1 },
-      {concrete_thms = ct2, generic_thms = gt2, dest_thms = dt2, app_thms = at2 }) = {
-    concrete_thms = Item_Net.merge (ct1, ct2),
-    generic_thms = Item_Net.merge (gt1, gt2),
-    dest_thms = Item_Net.merge (dt1, dt2),
-    app_thms = Item_Net.merge (at1, at2) };
-);
-
-val debug =
-  Attrib.setup_config_bool @{binding measurable_debug} (K false)
-
-val backtrack =
-  Attrib.setup_config_int @{binding measurable_backtrack} (K 20)
-
-val split =
-  Attrib.setup_config_bool @{binding measurable_split} (K true)
-
-fun TAKE n tac = Seq.take n o tac
-
-fun get lv =
-  rev o Item_Net.content o (case lv of Concrete => #concrete_thms | Generic => #generic_thms) o
-  Data.get o Context.Proof;
-
-fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
-
-fun map_data f1 f2 f3 f4
-  {generic_thms = t1,    concrete_thms = t2,    dest_thms = t3,    app_thms = t4} =
-  {generic_thms = f1 t1, concrete_thms = f2 t2, dest_thms = f3 t3, app_thms = f4 t4 }
-
-fun map_concrete_thms f = map_data f I I I
-fun map_generic_thms f = map_data I f I I
-fun map_dest_thms f = map_data I I f I
-fun map_app_thms f = map_data I I I f
-
-fun update f lv = Data.map (case lv of Concrete => map_concrete_thms f | Generic => map_generic_thms f);
-fun add thms' = update (fold Item_Net.update thms');
-
-val get_dest = Item_Net.content o #dest_thms o Data.get;
-val add_dest = Data.map o map_dest_thms o Item_Net.update;
-
-val get_app = Item_Net.content o #app_thms o Data.get;
-val add_app = Data.map o map_app_thms o Item_Net.update;
-
-fun is_too_generic thm =
-  let 
-    val concl = concl_of thm
-    val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
-  in is_Var (head_of concl') end
-
-fun import_theorem ctxt thm = if is_too_generic thm then [] else
-  [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
-
-fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
-
-fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f
-
-fun nth_hol_goal thm i =
-  HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
-
-fun dest_measurable_fun t =
-  (case t of
-    (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
-  | _ => raise (TERM ("not a measurability predicate", [t])))
-
-fun is_cond_formula n thm = if length (prems_of thm) < n then false else
-  (case nth_hol_goal thm n of
-    (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
-  | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
-  | _ => true)
-  handle TERM _ => true;
-
-fun indep (Bound i) t b = i < b orelse t <= i
-  | indep (f $ t) top bot = indep f top bot andalso indep t top bot
-  | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
-  | indep _ _ _ = true;
-
-fun cnt_prefixes ctxt (Abs (n, T, t)) = let
-      fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
-      fun cnt_walk (Abs (ns, T, t)) Ts =
-          map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
-        | cnt_walk (f $ g) Ts = let
-            val n = length Ts - 1
-          in
-            map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
-            map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
-            (if is_countable (type_of1 (Ts, g)) andalso loose_bvar1 (g, n)
-                andalso indep g n 0 andalso g <> Bound n
-              then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
-              else [])
-          end
-        | cnt_walk _ _ = []
-    in map (fn (t1, t2) => let
-        val T1 = type_of1 ([T], t2)
-        val T2 = type_of1 ([T], t)
-      in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
-        [SOME T1, SOME T, SOME T2])
-      end) (cnt_walk t [T])
-    end
-  | cnt_prefixes _ _ = []
-
-val split_countable_tac =
-  Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
-    let
-      val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
-      fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
-      fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
-      val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
-    in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
-    handle TERM _ => no_tac) 1)
-
-fun measurable_tac' ctxt ss facts = let
-
-    val imported_thms =
-      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt
-
-    fun debug_facts msg () =
-      msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
-        (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)));
-
-    val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
-
-    val split_app_tac =
-      Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
-        let
-          fun app_prefixes (Abs (n, T, (f $ g))) = let
-                val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
-              in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
-            | app_prefixes _ = []
-
-          fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
-            | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
-          val thy = Proof_Context.theory_of ctxt
-          val tunify = Sign.typ_unify thy
-          val thms = map
-              (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
-              (get_app (Context.Proof ctxt))
-          fun cert f = map (fn (t, t') => (f thy t, f thy t'))
-          fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
-            let
-              val inst =
-                (Vartab.empty, ~1)
-                |> tunify (T, thmT)
-                |> tunify (Tf, thmTf)
-                |> tunify (Tc, thmTc)
-                |> Vartab.dest o fst
-              val subst = subst_TVars (map (apsnd snd) inst)
-            in
-              Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
-                cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
-            end
-          val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
-        in if null cps then no_tac
-            else debug_tac ctxt (K ("split app fun")) (resolve_tac cps i)
-              ORELSE debug_tac ctxt (fn () => "FAILED") no_tac end
-        handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
-        handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
-
-    val depth_measurable_tac = REPEAT
-      (COND (is_cond_formula 1)
-        (debug_tac ctxt (K "simp") (SOLVED' (asm_full_simp_tac ss) 1))
-        ((debug_tac ctxt (K "single") (resolve_tac imported_thms 1)) APPEND
-          (split_app_tac ctxt 1) APPEND
-          (splitter 1)))
-
-  in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
-
-fun measurable_tac ctxt facts =
-  TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt (simpset_of ctxt) facts);
-
-val attr_add = Thm.declaration_attribute o add_thm;
-
-val attr : attribute context_parser =
-  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
-     Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
-
-val dest_attr : attribute context_parser =
-  Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
-
-val app_attr : attribute context_parser =
-  Scan.lift (Scan.succeed (Thm.declaration_attribute add_app));
-
-val method : (Proof.context -> Method.method) context_parser =
-  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts)));
-
-fun simproc ss redex = let
-    val ctxt = Simplifier.the_context ss;
-    val t = HOLogic.mk_Trueprop (term_of redex);
-    fun tac {context = ctxt, prems = _ } =
-      SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss));
-  in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
-
-end
-
-*}
-
-attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
-attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
-attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover"
-method_setup measurable = {* Measurable.method *} "measurability prover"
-simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
-
-declare
-  measurable_compose_rev[measurable_dest]
-  pred_sets1[measurable_dest]
-  pred_sets2[measurable_dest]
-  sets.sets_into_space[measurable_dest]
-
-declare
-  sets.top[measurable]
-  sets.empty_sets[measurable (raw)]
-  sets.Un[measurable (raw)]
-  sets.Diff[measurable (raw)]
-
-declare
-  measurable_count_space[measurable (raw)]
-  measurable_ident[measurable (raw)]
-  measurable_ident_sets[measurable (raw)]
-  measurable_const[measurable (raw)]
-  measurable_If[measurable (raw)]
-  measurable_comp[measurable (raw)]
-  measurable_sets[measurable (raw)]
-
-lemma predE[measurable (raw)]: 
-  "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
-  unfolding pred_def .
-
-lemma pred_intros_imp'[measurable (raw)]:
-  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
-  by (cases K) auto
-
-lemma pred_intros_conj1'[measurable (raw)]:
-  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
-  by (cases K) auto
-
-lemma pred_intros_conj2'[measurable (raw)]:
-  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
-  by (cases K) auto
-
-lemma pred_intros_disj1'[measurable (raw)]:
-  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
-  by (cases K) auto
-
-lemma pred_intros_disj2'[measurable (raw)]:
-  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
-  by (cases K) auto
-
-lemma pred_intros_logic[measurable (raw)]:
-  "pred M (\<lambda>x. x \<in> space M)"
-  "pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
-  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
-  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
-  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
-  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
-  "pred M (\<lambda>x. f x \<in> UNIV)"
-  "pred M (\<lambda>x. f x \<in> {})"
-  "pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})"
-  "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
-  "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) - (B x))"
-  "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))"
-  "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<union> (B x))"
-  "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
-  by (auto simp: iff_conv_conj_imp pred_def)
-
-lemma pred_intros_countable[measurable (raw)]:
-  fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
-  shows 
-    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
-    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
-  by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
-
-lemma pred_intros_countable_bounded[measurable (raw)]:
-  fixes X :: "'i :: countable set"
-  shows 
-    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>X. N x i))"
-    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>X. N x i))"
-    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
-    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
-  by (auto simp: Bex_def Ball_def)
-
-lemma pred_intros_finite[measurable (raw)]:
-  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))"
-  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))"
-  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)"
-  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)"
-  by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
-
-lemma countable_Un_Int[measurable (raw)]:
-  "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
-  "I \<noteq> {} \<Longrightarrow> (\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Inter>i\<in>I. N i) \<in> sets M"
-  by auto
-
-declare
-  finite_UN[measurable (raw)]
-  finite_INT[measurable (raw)]
-
-lemma sets_Int_pred[measurable (raw)]:
-  assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
-  shows "A \<inter> B \<in> sets M"
-proof -
-  have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
-  also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
-    using space by auto
-  finally show ?thesis .
-qed
-
-lemma [measurable (raw generic)]:
-  assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N"
-  shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
-    and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
-proof -
-  show "pred M (\<lambda>x. f x = c)"
-  proof cases
-    assume "c \<in> space N"
-    with measurable_sets[OF f c] show ?thesis
-      by (auto simp: Int_def conj_commute pred_def)
-  next
-    assume "c \<notin> space N"
-    with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto
-    then show ?thesis by (auto simp: pred_def cong: conj_cong)
-  qed
-  then show "pred M (\<lambda>x. c = f x)"
-    by (simp add: eq_commute)
-qed
-
-lemma pred_le_const[measurable (raw generic)]:
-  assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
-  using measurable_sets[OF f c]
-  by (auto simp: Int_def conj_commute eq_commute pred_def)
-
-lemma pred_const_le[measurable (raw generic)]:
-  assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
-  using measurable_sets[OF f c]
-  by (auto simp: Int_def conj_commute eq_commute pred_def)
-
-lemma pred_less_const[measurable (raw generic)]:
-  assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
-  using measurable_sets[OF f c]
-  by (auto simp: Int_def conj_commute eq_commute pred_def)
-
-lemma pred_const_less[measurable (raw generic)]:
-  assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
-  using measurable_sets[OF f c]
-  by (auto simp: Int_def conj_commute eq_commute pred_def)
-
-declare
-  sets.Int[measurable (raw)]
-
-lemma pred_in_If[measurable (raw)]:
-  "(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>
-    pred M (\<lambda>x. x \<in> (if P then A x else B x))"
-  by auto
-
-lemma sets_range[measurable_dest]:
-  "A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"
-  by auto
-
-lemma pred_sets_range[measurable_dest]:
-  "A ` I \<subseteq> sets N \<Longrightarrow> i \<in> I \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
-  using pred_sets2[OF sets_range] by auto
-
-lemma sets_All[measurable_dest]:
-  "\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"
-  by auto
-
-lemma pred_sets_All[measurable_dest]:
-  "\<forall>i. A i \<in> sets (N i) \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
-  using pred_sets2[OF sets_All, of A N f] by auto
-
-lemma sets_Ball[measurable_dest]:
-  "\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"
-  by auto
-
-lemma pred_sets_Ball[measurable_dest]:
-  "\<forall>i\<in>I. A i \<in> sets (N i) \<Longrightarrow> i\<in>I \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
-  using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
-
-lemma measurable_finite[measurable (raw)]:
-  fixes S :: "'a \<Rightarrow> nat set"
-  assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
-  shows "pred M (\<lambda>x. finite (S x))"
-  unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
-
-lemma measurable_Least[measurable]:
-  assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q
-  shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
-  unfolding measurable_def by (safe intro!: sets_Least) simp_all
-
-lemma measurable_count_space_insert[measurable (raw)]:
-  "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
-  by simp
-
-hide_const (open) pred
 
 subsection {* Extend measure *}
 
@@ -2363,7 +1912,7 @@
     by blast
 qed
 
-section {* Dynkin systems *}
+subsection {* Dynkin systems *}
 
 locale dynkin_system = subset_class +
   assumes space: "\<Omega> \<in> M"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/measurable.ML	Thu Dec 06 11:42:23 2012 +0100
@@ -0,0 +1,238 @@
+(*  Title:      HOL/Probability/measurable.ML
+    Author:     Johannes Hölzl <hoelzl@in.tum.de>
+
+Measurability prover.
+*)
+
+signature MEASURABLE = 
+sig
+  datatype level = Concrete | Generic
+
+  val simproc : simpset -> cterm -> thm option
+  val method : (Proof.context -> Method.method) context_parser
+  val measurable_tac : Proof.context -> thm list -> tactic
+
+  val attr : attribute context_parser
+  val dest_attr : attribute context_parser
+  val app_attr : attribute context_parser
+
+  val get : level -> Proof.context -> thm list
+  val get_all : Proof.context -> thm list
+
+  val update : (thm Item_Net.T -> thm Item_Net.T) -> level -> Context.generic -> Context.generic
+
+end ;
+
+structure Measurable : MEASURABLE =
+struct
+
+datatype level = Concrete | Generic;
+
+structure Data = Generic_Data
+(
+  type T = {
+    concrete_thms : thm Item_Net.T,
+    generic_thms : thm Item_Net.T,
+    dest_thms : thm Item_Net.T,
+    app_thms : thm Item_Net.T }
+  val empty = {
+    concrete_thms = Thm.full_rules,
+    generic_thms = Thm.full_rules,
+    dest_thms = Thm.full_rules,
+    app_thms = Thm.full_rules};
+  val extend = I;
+  fun merge ({concrete_thms = ct1, generic_thms = gt1, dest_thms = dt1, app_thms = at1 },
+      {concrete_thms = ct2, generic_thms = gt2, dest_thms = dt2, app_thms = at2 }) = {
+    concrete_thms = Item_Net.merge (ct1, ct2),
+    generic_thms = Item_Net.merge (gt1, gt2),
+    dest_thms = Item_Net.merge (dt1, dt2),
+    app_thms = Item_Net.merge (at1, at2) };
+);
+
+val debug =
+  Attrib.setup_config_bool @{binding measurable_debug} (K false)
+
+val backtrack =
+  Attrib.setup_config_int @{binding measurable_backtrack} (K 20)
+
+val split =
+  Attrib.setup_config_bool @{binding measurable_split} (K true)
+
+fun TAKE n tac = Seq.take n o tac
+
+fun get lv =
+  rev o Item_Net.content o (case lv of Concrete => #concrete_thms | Generic => #generic_thms) o
+  Data.get o Context.Proof;
+
+fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
+
+fun map_data f1 f2 f3 f4
+  {generic_thms = t1,    concrete_thms = t2,    dest_thms = t3,    app_thms = t4} =
+  {generic_thms = f1 t1, concrete_thms = f2 t2, dest_thms = f3 t3, app_thms = f4 t4 }
+
+fun map_concrete_thms f = map_data f I I I
+fun map_generic_thms f = map_data I f I I
+fun map_dest_thms f = map_data I I f I
+fun map_app_thms f = map_data I I I f
+
+fun update f lv = Data.map (case lv of Concrete => map_concrete_thms f | Generic => map_generic_thms f);
+fun add thms' = update (fold Item_Net.update thms');
+
+val get_dest = Item_Net.content o #dest_thms o Data.get;
+val add_dest = Data.map o map_dest_thms o Item_Net.update;
+
+val get_app = Item_Net.content o #app_thms o Data.get;
+val add_app = Data.map o map_app_thms o Item_Net.update;
+
+fun is_too_generic thm =
+  let 
+    val concl = concl_of thm
+    val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
+  in is_Var (head_of concl') end
+
+fun import_theorem ctxt thm = if is_too_generic thm then [] else
+  [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
+
+fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
+
+fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f
+
+fun nth_hol_goal thm i =
+  HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
+
+fun dest_measurable_fun t =
+  (case t of
+    (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
+  | _ => raise (TERM ("not a measurability predicate", [t])))
+
+fun is_cond_formula n thm = if length (prems_of thm) < n then false else
+  (case nth_hol_goal thm n of
+    (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
+  | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
+  | _ => true)
+  handle TERM _ => true;
+
+fun indep (Bound i) t b = i < b orelse t <= i
+  | indep (f $ t) top bot = indep f top bot andalso indep t top bot
+  | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
+  | indep _ _ _ = true;
+
+fun cnt_prefixes ctxt (Abs (n, T, t)) = let
+      fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
+      fun cnt_walk (Abs (ns, T, t)) Ts =
+          map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
+        | cnt_walk (f $ g) Ts = let
+            val n = length Ts - 1
+          in
+            map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
+            map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
+            (if is_countable (type_of1 (Ts, g)) andalso loose_bvar1 (g, n)
+                andalso indep g n 0 andalso g <> Bound n
+              then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
+              else [])
+          end
+        | cnt_walk _ _ = []
+    in map (fn (t1, t2) => let
+        val T1 = type_of1 ([T], t2)
+        val T2 = type_of1 ([T], t)
+      in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
+        [SOME T1, SOME T, SOME T2])
+      end) (cnt_walk t [T])
+    end
+  | cnt_prefixes _ _ = []
+
+val split_countable_tac =
+  Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
+    let
+      val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
+      fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
+      fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
+      val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
+    in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
+    handle TERM _ => no_tac) 1)
+
+fun measurable_tac' ctxt ss facts = let
+
+    val imported_thms =
+      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt
+
+    fun debug_facts msg () =
+      msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
+        (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)));
+
+    val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
+
+    val split_app_tac =
+      Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
+        let
+          fun app_prefixes (Abs (n, T, (f $ g))) = let
+                val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
+              in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
+            | app_prefixes _ = []
+
+          fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
+            | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
+          val thy = Proof_Context.theory_of ctxt
+          val tunify = Sign.typ_unify thy
+          val thms = map
+              (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
+              (get_app (Context.Proof ctxt))
+          fun cert f = map (fn (t, t') => (f thy t, f thy t'))
+          fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
+            let
+              val inst =
+                (Vartab.empty, ~1)
+                |> tunify (T, thmT)
+                |> tunify (Tf, thmTf)
+                |> tunify (Tc, thmTc)
+                |> Vartab.dest o fst
+              val subst = subst_TVars (map (apsnd snd) inst)
+            in
+              Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
+                cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
+            end
+          val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
+        in if null cps then no_tac
+            else debug_tac ctxt (K ("split app fun")) (resolve_tac cps i)
+              ORELSE debug_tac ctxt (fn () => "FAILED") no_tac end
+        handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
+        handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
+
+    fun REPEAT_cnt f n st = ((f n THEN REPEAT_cnt f (n + 1)) ORELSE all_tac) st
+
+    val depth_measurable_tac = REPEAT_cnt (fn n =>
+       (COND (is_cond_formula 1)
+        (debug_tac ctxt (K ("simp " ^ string_of_int n)) (SOLVED' (asm_full_simp_tac ss) 1))
+        ((debug_tac ctxt (K ("single " ^ string_of_int n)) (resolve_tac imported_thms 1)) APPEND
+          (split_app_tac ctxt 1) APPEND
+          (splitter 1)))) 0
+
+  in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
+
+fun measurable_tac ctxt facts =
+  TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt (simpset_of ctxt) facts);
+
+val attr_add = Thm.declaration_attribute o add_thm;
+
+val attr : attribute context_parser =
+  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
+     Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
+
+val dest_attr : attribute context_parser =
+  Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
+
+val app_attr : attribute context_parser =
+  Scan.lift (Scan.succeed (Thm.declaration_attribute add_app));
+
+val method : (Proof.context -> Method.method) context_parser =
+  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts)));
+
+fun simproc ss redex = let
+    val ctxt = Simplifier.the_context ss;
+    val t = HOLogic.mk_Trueprop (term_of redex);
+    fun tac {context = ctxt, prems = _ } =
+      SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss));
+  in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
+
+end
+
--- a/src/HOL/SEQ.thy	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/SEQ.thy	Thu Dec 06 11:42:23 2012 +0100
@@ -911,4 +911,33 @@
 lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
   by (rule LIMSEQ_power_zero) simp
 
+lemma tendsto_at_topI_sequentially:
+  fixes f :: "real \<Rightarrow> real"
+  assumes mono: "mono f"
+  assumes limseq: "(\<lambda>n. f (real n)) ----> y"
+  shows "(f ---> y) at_top"
+proof (rule tendstoI)
+  fix e :: real assume "0 < e"
+  with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
+    by (auto simp: LIMSEQ_def dist_real_def)
+  { fix x :: real
+    from ex_le_of_nat[of x] guess n ..
+    note monoD[OF mono this]
+    also have "f (real_of_nat n) \<le> y"
+      by (rule LIMSEQ_le_const[OF limseq])
+         (auto intro: exI[of _ n] monoD[OF mono] simp: real_eq_of_nat[symmetric])
+    finally have "f x \<le> y" . }
+  note le = this
+  have "eventually (\<lambda>x. real N \<le> x) at_top"
+    by (rule eventually_ge_at_top)
+  then show "eventually (\<lambda>x. dist (f x) y < e) at_top"
+  proof eventually_elim
+    fix x assume N': "real N \<le> x"
+    with N[of N] le have "y - f (real N) < e" by auto
+    moreover note monoD[OF mono N']
+    ultimately show "dist (f x) y < e"
+      using le[of x] by (auto simp: dist_real_def field_simps)
+  qed
+qed
+
 end
--- a/src/HOL/TPTP/mash_eval.ML	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Thu Dec 06 11:42:23 2012 +0100
@@ -79,7 +79,7 @@
               slack_max_facts NONE hyp_ts concl_t facts
           |> Sledgehammer_MePo.weight_mepo_facts
         val mash_facts = suggested_facts suggs facts
-        val mess = [(mepo_facts, []), (mash_facts, [])]
+        val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, []))]
         val mesh_facts = mesh_facts slack_max_facts mess
         val isar_facts = suggested_facts (map (rpair 1.0) isar_deps) facts
         fun prove ok heading get facts =
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py	Thu Dec 06 11:42:23 2012 +0100
@@ -21,12 +21,12 @@
 -------- Example Usage ---------------\n\
 ./compareStats.py --statFiles ../tmp/natISANB.stats ../tmp/natATPNB.stats -b 30\n\n\
 Author: Daniel Kuehlwein, July 2012',formatter_class=RawDescriptionHelpFormatter)
-parser.add_argument('--statFiles', default=None, nargs='+', 
+parser.add_argument('--statFiles', default=None, nargs='+',
                     help='The names of the saved statistic files.')
 parser.add_argument('-b','--bins',default=50,help="Number of bins for the AUC histogram. Default=50.",type=int)
 
 def main(argv = sys.argv[1:]):
-    args = parser.parse_args(argv)  
+    args = parser.parse_args(argv)
     if args.statFiles == None:
         print 'Filenames missing.'
         sys.exit(-1)
@@ -56,11 +56,10 @@
     legend(loc='upper left')
     ylabel('Problems')
     xlabel('AUC')
-        
+
     show()
 
 if __name__ == '__main__':
     #args = ['--statFiles','../tmp/natISANB.stats','../tmp/natATPNB.stats','-b','30']
     #sys.exit(main(args))
     sys.exit(main())
-    
\ No newline at end of file
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py	Thu Dec 06 11:42:23 2012 +0100
@@ -33,18 +33,18 @@
         self.accessibleDict = {}
         self.expandedAccessibles = {}
         self.changed = True
-    
+
     """
     Init functions. Side Effect: nameIdDict, idNameDict, featureIdDict get filled!
-    """    
+    """
     def init_featureDict(self,featureFile):
         self.featureDict,self.maxNameId,self.maxFeatureId = create_feature_dict(self.nameIdDict,self.idNameDict,self.maxNameId,self.featureIdDict,\
-                                                                                self.maxFeatureId,featureFile)        
+                                                                                self.maxFeatureId,featureFile)
     def init_dependenciesDict(self,depFile):
         self.dependenciesDict = create_dependencies_dict(self.nameIdDict,depFile)
     def init_accessibleDict(self,accFile):
         self.accessibleDict,self.maxNameId = create_accessible_dict(self.nameIdDict,self.idNameDict,self.maxNameId,accFile)
-    
+
     def init_all(self,inputFolder,featureFileName = 'mash_features',depFileName='mash_dependencies',accFileName = 'mash_accessibility'):
         featureFile = join(inputFolder,featureFileName)
         depFile = join(inputFolder,depFileName)
@@ -54,7 +54,7 @@
         self.init_dependenciesDict(depFile)
         self.expandedAccessibles = {}
         self.changed = True
-        
+
     def get_name_id(self,name):
         """
         Return the Id for a name.
@@ -66,7 +66,7 @@
             self.nameIdDict[name] = self.maxNameId
             self.idNameDict[self.maxNameId] = name
             nameId = self.maxNameId
-            self.maxNameId += 1 
+            self.maxNameId += 1
             self.changed = True
         return nameId
 
@@ -74,8 +74,23 @@
         if not self.featureIdDict.has_key(featureName):
             self.featureIdDict[featureName] = self.maxFeatureId
             self.maxFeatureId += 1
-            self.changed = True 
-            
+            self.changed = True
+        return self.featureIdDict[featureName]
+
+    def get_features(self,line):
+        # Feature Ids
+        featureNames = [f.strip() for f in line[1].split()]
+        features = []
+        for fn in featureNames:
+            tmp = fn.split('=')
+            if len(tmp) == 2:
+                fId = self.add_feature(tmp[0])
+                features.append((fId,float(tmp[1])))
+            else:
+                fId = self.add_feature(fn)
+                features.append((fId,1.0))
+        return features
+
     def expand_accessibles(self,acc):
         accessibles = set(acc)
         unexpandedQueue = Queue()
@@ -86,71 +101,67 @@
                 unexpandedQueue.put(a)
         while not unexpandedQueue.empty():
             nextUnExp = unexpandedQueue.get()
-            nextUnExpAcc = self.accessibleDict[nextUnExp]            
+            nextUnExpAcc = self.accessibleDict[nextUnExp]
             for a in nextUnExpAcc:
                 if not a in accessibles:
                     accessibles = accessibles.union([a])
                     if self.expandedAccessibles.has_key(a):
                         accessibles = accessibles.union(self.expandedAccessibles[a])
                     else:
-                        unexpandedQueue.put(a)                    
+                        unexpandedQueue.put(a)
         return list(accessibles)
-            
+
     def parse_fact(self,line):
         """
         Parses a single line, extracting accessibles, features, and dependencies.
         """
         assert line.startswith('! ')
         line = line[2:]
-        
+
         # line = name:accessibles;features;dependencies
         line = line.split(':')
         name = line[0].strip()
         nameId = self.get_name_id(name)
-    
-        line = line[1].split(';')       
+
+        line = line[1].split(';')
         # Accessible Ids
         unExpAcc = [self.nameIdDict[a.strip()] for a in line[0].split()]
         self.accessibleDict[nameId] = unExpAcc
-        # Feature Ids
-        featureNames = [f.strip() for f in line[1].split()]
-        for fn in featureNames:
-            self.add_feature(fn)
-        self.featureDict[nameId] = [self.featureIdDict[fn] for fn in featureNames]
+        self.featureDict[nameId] = self.get_features(line)
         self.dependenciesDict[nameId] = [self.nameIdDict[d.strip()] for d in line[2].split()]
         self.changed = True
         return nameId
-    
+
     def parse_overwrite(self,line):
         """
         Parses a single line, extracts the problemId and the Ids of the dependencies.
         """
         assert line.startswith('p ')
         line = line[2:]
-        
+
         # line = name:dependencies
         line = line.split(':')
         name = line[0].strip()
         nameId = self.get_name_id(name)
-    
+
         dependencies = [self.nameIdDict[d.strip()] for d in line[1].split()]
         self.changed = True
         return nameId,dependencies
-    
+
     def parse_problem(self,line):
         """
-        Parses a problem and returns the features and the accessibles. 
+        Parses a problem and returns the features and the accessibles.
         """
         assert line.startswith('? ')
         line = line[2:]
         name = None
-        
+
         # Check whether there is a problem name:
         tmp = line.split(':')
         if len(tmp) == 2:
             name = tmp[0].strip()
             line = tmp[1]
-        
+
         # line = accessibles;features
         line = line.split(';')
         # Accessible Ids, expand and store the accessibles.
@@ -164,13 +175,14 @@
                 self.expandedAccessibles[accId] = self.expand_accessibles(accIdAcc)
                 self.changed = True
         accessibles = self.expand_accessibles(unExpAcc)
-        # Feature Ids
-        featureNames = [f.strip() for f in line[1].split()]
-        for fn in featureNames:
-            self.add_feature(fn)
-        features = [self.featureIdDict[fn] for fn in featureNames]
-        return name,features,accessibles    
-    
+#        # Feature Ids
+#        featureNames = [f.strip() for f in line[1].split()]
+#        for fn in featureNames:
+#            self.add_feature(fn)
+#        features = [self.featureIdDict[fn] for fn in featureNames]
+        features = self.get_features(line)
+        return name,features,accessibles
+
     def save(self,fileName):
         if self.changed:
             dictsStream = open(fileName, 'wb')
@@ -179,10 +191,8 @@
             self.changed = False
             dictsStream.close()
     def load(self,fileName):
-        dictsStream = open(fileName, 'rb')        
+        dictsStream = open(fileName, 'rb')
         self.accessibleDict,self.dependenciesDict,self.expandedAccessibles,self.featureDict,\
               self.featureIdDict,self.idNameDict,self.maxFeatureId,self.maxNameId,self.nameIdDict = load(dictsStream)
         self.changed = False
         dictsStream.close()
-    
-            
\ No newline at end of file
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Thu Dec 06 11:42:23 2012 +0100
@@ -20,6 +20,7 @@
 from time import time
 from stats import Statistics
 from dictionaries import Dictionaries
+#from fullNaiveBayes import NBClassifier
 from naiveBayes import NBClassifier
 from snow import SNoW
 from predefined import Predefined
@@ -34,7 +35,7 @@
 Author: Daniel Kuehlwein, July 2012',formatter_class=RawDescriptionHelpFormatter)
 parser.add_argument('-i','--inputFile',help='File containing all problems to be solved.')
 parser.add_argument('-o','--outputDir', default='../tmp/',help='Directory where all created files are stored. Default=../tmp/.')
-parser.add_argument('-p','--predictions',default='../tmp/%s.predictions' % datetime.datetime.now(), 
+parser.add_argument('-p','--predictions',default='../tmp/%s.predictions' % datetime.datetime.now(),
                     help='File where the predictions stored. Default=../tmp/dateTime.predictions.')
 parser.add_argument('--numberOfPredictions',default=200,help="Number of premises to write in the output. Default=200.",type=int)
 
@@ -48,7 +49,7 @@
 parser.add_argument('--nb',default=False,action='store_true',help="Use Naive Bayes for learning. This is the default learning method.")
 parser.add_argument('--snow',default=False,action='store_true',help="Use SNoW's naive bayes instead of Naive Bayes for learning.")
 parser.add_argument('--predef',default=False,action='store_true',\
-                    help="Use predefined predictions. Used only for comparison with the actual learning. Expects mash_meng_paulson_suggestions in inputDir.")
+                    help="Use predefined predictions. Used only for comparison with the actual learning. Expects mash_mepo_suggestions in inputDir.")
 parser.add_argument('--statistics',default=False,action='store_true',help="Create and show statistics for the top CUTOFF predictions.\
                     WARNING: This will make the program a lot slower! Default=False.")
 parser.add_argument('--saveStats',default=None,help="If defined, stores the statistics in the filename provided.")
@@ -56,11 +57,11 @@
 parser.add_argument('-l','--log', default='../tmp/%s.log' % datetime.datetime.now(), help='Log file name. Default=../tmp/dateTime.log')
 parser.add_argument('-q','--quiet',default=False,action='store_true',help="If enabled, only print warnings. Default=False.")
 
-def main(argv = sys.argv[1:]):        
+def main(argv = sys.argv[1:]):
     # Initializing command-line arguments
     args = parser.parse_args(argv)
 
-    # Set up logging 
+    # Set up logging
     logging.basicConfig(level=logging.DEBUG,
                         format='%(asctime)s %(name)-12s %(levelname)-8s %(message)s',
                         datefmt='%d-%m %H:%M:%S',
@@ -81,8 +82,8 @@
     logger.info('Using the following settings: %s',args)
     # Pick algorithm
     if args.nb:
-        logger.info('Using Naive Bayes for learning.')        
-        model = NBClassifier() 
+        logger.info('Using Naive Bayes for learning.')
+        model = NBClassifier()
         modelFile = os.path.join(args.outputDir,'NB.pickle')
     elif args.snow:
         logger.info('Using naive bayes (SNoW) for learning.')
@@ -90,72 +91,77 @@
         modelFile = os.path.join(args.outputDir,'SNoW.pickle')
     elif args.predef:
         logger.info('Using predefined predictions.')
-        predictionFile = os.path.join(args.inputDir,'mash_meng_paulson_suggestions') 
+        #predictionFile = os.path.join(args.inputDir,'mash_meng_paulson_suggestions') 
+        predictionFile = os.path.join(args.inputDir,'mash_mepo_suggestions')
         model = Predefined(predictionFile)
-        modelFile = os.path.join(args.outputDir,'isabelle.pickle')        
+        modelFile = os.path.join(args.outputDir,'mepo.pickle')        
     else:
-        logger.info('No algorithm specified. Using Naive Bayes.')        
-        model = NBClassifier() 
-        modelFile = os.path.join(args.outputDir,'NB.pickle')    
-    dictsFile = os.path.join(args.outputDir,'dicts.pickle')    
-    
+        logger.info('No algorithm specified. Using Naive Bayes.')
+        model = NBClassifier()
+        modelFile = os.path.join(args.outputDir,'NB.pickle')
+    dictsFile = os.path.join(args.outputDir,'dicts.pickle')
+
     # Initializing model
-    if args.init:        
+    if args.init:
         logger.info('Initializing Model.')
         startTime = time()
-        
-        # Load all data        
+
+        # Load all data
         dicts = Dictionaries()
         dicts.init_all(args.inputDir,depFileName=args.depFile)
-        
+
         # Create Model
         trainData = dicts.featureDict.keys()
         if args.predef:
             dicts = model.initializeModel(trainData,dicts)
         else:
             model.initializeModel(trainData,dicts)
-        
+
         model.save(modelFile)
         dicts.save(dictsFile)
 
         logger.info('All Done. %s seconds needed.',round(time()-startTime,2))
         return 0
-    # Create predictions and/or update model       
+    # Create predictions and/or update model
     else:
-        lineCounter = 0
+        lineCounter = 1
+        statementCounter = 1
+        computeStats = False
         dicts = Dictionaries()
         # Load Files
         if os.path.isfile(dictsFile):
             dicts.load(dictsFile)
         if os.path.isfile(modelFile):
             model.load(modelFile)
-        
+
         # IO Streams
         OS = open(args.predictions,'a')
         IS = open(args.inputFile,'r')
-        
+
         # Statistics
         if args.statistics:
             stats = Statistics(args.cutOff)
-        
+
         predictions = None
         #Reading Input File
         for line in IS:
- #           try:
+#           try:
             if True:
                 if line.startswith('!'):
                     problemId = dicts.parse_fact(line)
                     # Statistics
-                    if args.statistics:
+                    if args.statistics and computeStats:
+                        computeStats = False
                         acc = dicts.accessibleDict[problemId]
                         if args.predef:
-                            predictions = model.predict[problemId]
+                            predictions = model.predict(problemId)
                         else:
-                            predictions,_predictionsValues = model.predict(dicts.featureDict[problemId],dicts.expand_accessibles(acc))        
-                        stats.update(predictions,dicts.dependenciesDict[problemId])
+                            predictions,_predictionsValues = model.predict(dicts.featureDict[problemId],dicts.expand_accessibles(acc))
+                        stats.update(predictions,dicts.dependenciesDict[problemId],statementCounter)
                         if not stats.badPreds == []:
                             bp = string.join([str(dicts.idNameDict[x]) for x in stats.badPreds], ',')
-                            logger.debug('Bad predictions: %s',bp)    
+                            logger.debug('Bad predictions: %s',bp)
+                    statementCounter += 1
                     # Update Dependencies, p proves p
                     dicts.dependenciesDict[problemId] = [problemId]+dicts.dependenciesDict[problemId]
                     model.update(problemId,dicts.featureDict[problemId],dicts.dependenciesDict[problemId])
@@ -165,41 +171,41 @@
                     newDependencies = [problemId]+newDependencies
                     model.overwrite(problemId,newDependencies,dicts)
                     dicts.dependenciesDict[problemId] = newDependencies
-                elif line.startswith('?'):
+                elif line.startswith('?'):                    
                     startTime = time()
+                    computeStats = True
                     if args.predef:
                         continue
                     name,features,accessibles = dicts.parse_problem(line)
                     # Create predictions
-                    logger.info('Starting computation for problem on line %s',lineCounter)                
-                    predictions,predictionValues = model.predict(features,accessibles)        
+                    logger.info('Starting computation for problem on line %s',lineCounter)
+                    predictions,predictionValues = model.predict(features,accessibles)
                     assert len(predictions) == len(predictionValues)
                     logger.info('Done. %s seconds needed.',round(time()-startTime,2))
-                    
                     # Output        
                     predictionNames = [str(dicts.idNameDict[p]) for p in predictions[:args.numberOfPredictions]]
-                    predictionValues = [str(x) for x in predictionValues[:args.numberOfPredictions]]                    
-                    predictionsStringList = ['%s=%s' % (predictionNames[i],predictionValues[i]) for i in range(len(predictionNames))]                
+                    predictionValues = [str(x) for x in predictionValues[:args.numberOfPredictions]]
+                    predictionsStringList = ['%s=%s' % (predictionNames[i],predictionValues[i]) for i in range(len(predictionNames))]
                     predictionsString = string.join(predictionsStringList,' ')
                     outString = '%s: %s' % (name,predictionsString)
                     OS.write('%s\n' % outString)
-                    lineCounter += 1
                 else:
                     logger.warning('Unspecified input format: \n%s',line)
                     sys.exit(-1)
+                lineCounter += 1
             """
             except:
                 logger.warning('An error occurred on line %s .',line)
                 lineCounter += 1
                 continue
-            """    
+            """
         OS.close()
         IS.close()
-        
+
         # Statistics
         if args.statistics:
             stats.printAvg()
-        
+
         # Save
         if args.saveModel:
             model.save(modelFile)
@@ -214,15 +220,29 @@
     # Nat
     #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Nat/','--predef']
     #args = ['-i', '../data/Nat/mash_commands','-p','../tmp/testIsabelle.pred','-l','testIsabelle.log','--predef','-o','../tmp/','--statistics','--saveStats','../tmp/natATPMP.stats']
-    #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Nat/']    
+    #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Nat/']
     #args = ['-i', '../data/Nat/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/natATPNB.stats','--cutOff','500']
-    # BUG
+    # List
     #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/List/','--isabelle']
     #args = ['-i', '../data/List/mash_commands','-p','../tmp/testIsabelle.pred','-l','testIsabelle.log','--isabelle','-o','../tmp/','--statistics']
-    #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../bug/init','--init']
-    #args = ['-i', '../bug/adds/mash_commands','-p','../tmp/testNB.pred','-l','testNB.log','--nb','-o','../tmp/']
+    # Huffmann
+    #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Huffman/','--depFile','mash_atp_dependencies']
+    #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Huffman/']
+    #args = ['-i', '../data/Huffman/mash_commands','-p','../tmp/testNB.pred','-l','testNB.log','--nb','-o','../tmp/','--statistics']
+    # Arrow
+    #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Arrow_Order/']    
+    #args = ['-i', '../data/Arrow_Order/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/arrowIsarNB.stats','--cutOff','500']
+    # Fundamental_Theorem_Algebra
+    #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Fundamental_Theorem_Algebra/']    
+    #args = ['-i', '../data/Fundamental_Theorem_Algebra/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/Fundamental_Theorem_AlgebraIsarNB.stats','--cutOff','500']
+    #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Fundamental_Theorem_Algebra/','--predef']
+    #args = ['-i', '../data/Fundamental_Theorem_Algebra/mash_commands','-p','../tmp/Fundamental_Theorem_AlgebraMePo.pred','-l','testIsabelle.log','--predef','-o','../tmp/','--statistics','--saveStats','../tmp/Fundamental_Theorem_AlgebraMePo.stats']
+    # Jinja
+    #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Jinja/']    
+    #args = ['-i', '../data/Jinja/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/JinjaIsarNB.stats','--cutOff','500']
+
+    
     #startTime = time()
     #sys.exit(main(args))
-    #print 'New ' + str(round(time()-startTime,2))    
+    #print 'New ' + str(round(time()-startTime,2))
     sys.exit(main())
-    
\ No newline at end of file
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/naiveBayes.py	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/naiveBayes.py	Thu Dec 06 11:42:23 2012 +0100
@@ -24,46 +24,46 @@
         Constructor
         '''
         self.counts = {}
-    
+
     def initializeModel(self,trainData,dicts):
         """
         Build basic model from training data.
-        """        
+        """
         for d in trainData:
             dPosCount = 0
-            dFeatureCounts = {}            
+            dFeatureCounts = {}
             self.counts[d] = [dPosCount,dFeatureCounts]
-        
+
         for key in dicts.dependenciesDict.keys():
             # Add p proves p
             keyDeps = [key]+dicts.dependenciesDict[key]
-            
+
             for dep in keyDeps:
                 self.counts[dep][0] += 1
                 depFeatures = dicts.featureDict[key]
-                for f in depFeatures:
+                for f,_w in depFeatures:
                     if self.counts[dep][1].has_key(f):
                         self.counts[dep][1][f] += 1
                     else:
                         self.counts[dep][1][f] = 1
 
-    
+
     def update(self,dataPoint,features,dependencies):
         """
         Updates the Model.
         """
         if not self.counts.has_key(dataPoint):
             dPosCount = 0
-            dFeatureCounts = {}            
+            dFeatureCounts = {}
             self.counts[dataPoint] = [dPosCount,dFeatureCounts]
         for dep in dependencies:
             self.counts[dep][0] += 1
-            for f in features:
+            for f,_w in features:
                 if self.counts[dep][1].has_key(f):
                     self.counts[dep][1][f] += 1
                 else:
                     self.counts[dep][1][f] = 1
- 
+
     def delete(self,dataPoint,features,dependencies):
         """
         Deletes a single datapoint from the model.
@@ -73,7 +73,7 @@
             for f in features:
                 self.counts[dep][1][f] -= 1
 
-            
+
     def overwrite(self,problemId,newDependencies,dicts):
         """
         Deletes the old dependencies of problemId and replaces them with the new ones. Updates the model accordingly.
@@ -83,45 +83,45 @@
         features = dicts.featureDict[problemId]
         self.delete(problemId,features,oldDeps)
         self.update(problemId,features,newDependencies)
-    
+
     def predict(self,features,accessibles):
         """
         For each accessible, predicts the probability of it being useful given the features.
         Returns a ranking of the accessibles.
         """
         predictions = []
-        for a in accessibles:            
+        for a in accessibles:
             posA = self.counts[a][0]
             fA = set(self.counts[a][1].keys())
             fWeightsA = self.counts[a][1]
-            resultA = log(posA) 
-            for f in features:
+            resultA = log(posA)
+            for f,w in features:
                 if f in fA:
                     if fWeightsA[f] == 0:
-                        resultA -= 15
+                        resultA -= w*15
                     else:
                         assert fWeightsA[f] <= posA
-                        resultA += log(float(fWeightsA[f])/posA)
+                        resultA += w*log(float(fWeightsA[f])/posA)
                 else:
-                    resultA -= 15
+                    resultA -= w*15
             predictions.append(resultA)
         #expPredictions = array([exp(x) for x in predictions])
         predictions = array(predictions)
-        perm = (-predictions).argsort()        
-        #return array(accessibles)[perm],expPredictions[perm] 
+        perm = (-predictions).argsort()
+        #return array(accessibles)[perm],expPredictions[perm]
         return array(accessibles)[perm],predictions[perm]
-    
+
     def save(self,fileName):
         OStream = open(fileName, 'wb')
-        dump(self.counts,OStream)        
+        dump(self.counts,OStream)
         OStream.close()
-        
+
     def load(self,fileName):
         OStream = open(fileName, 'rb')
-        self.counts = load(OStream)      
+        self.counts = load(OStream)
         OStream.close()
 
-    
+
 if __name__ == '__main__':
     featureDict = {0:[0,1,2],1:[3,2,1]}
     dependenciesDict = {0:[0],1:[0,1]}
@@ -136,4 +136,4 @@
     d.loadModel('x')
     print c.counts
     print d.counts
-    print 'Done'
\ No newline at end of file
+    print 'Done'
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/predefined.py	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/predefined.py	Thu Dec 06 11:42:23 2012 +0100
@@ -23,11 +23,11 @@
         Constructor
         '''
         self.predictionFile = mpPredictionFile
-    
+
     def initializeModel(self,_trainData,dicts):
         """
         Load predictions.
-        """        
+        """
         self.predictions = {}
         IS = open(self.predictionFile,'r')
         for line in IS:
@@ -39,28 +39,27 @@
             self.predictions[predId] = preds
         IS.close()
         return dicts
-    
+
     def update(self,dataPoint,features,dependencies):
         """
         Updates the Model.
         """
         # No Update needed since we assume that we got all predictions
         pass
-            
-    
+
+
     def predict(self,problemId):
         """
         Return the saved predictions.
         """
-        return self.predictions[problemId] 
-    
+        return self.predictions[problemId]
+
     def save(self,fileName):
         OStream = open(fileName, 'wb')
-        dump((self.predictionFile,self.predictions),OStream)        
+        dump((self.predictionFile,self.predictions),OStream)
         OStream.close()
-        
+
     def load(self,fileName):
         OStream = open(fileName, 'rb')
-        self.predictionFile,self.predictions = load(OStream)      
+        self.predictionFile,self.predictions = load(OStream)
         OStream.close()
-
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/readData.py	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/readData.py	Thu Dec 06 11:42:23 2012 +0100
@@ -15,12 +15,12 @@
 import sys,logging
 
 def create_feature_dict(nameIdDict,idNameDict,maxNameId,featureIdDict,maxFeatureId,inputFile):
-    logger = logging.getLogger('create_feature_dict')    
+    logger = logging.getLogger('create_feature_dict')
     featureDict = {}
-    IS = open(inputFile,'r') 
+    IS = open(inputFile,'r')
     for line in IS:
         line = line.split(':')
-        name = line[0]        
+        name = line[0]
         # Name Id
         if nameIdDict.has_key(name):
             logger.warning('%s appears twice in the feature file. Aborting.',name)
@@ -29,33 +29,41 @@
             nameIdDict[name] = maxNameId
             idNameDict[maxNameId] = name
             nameId = maxNameId
-            maxNameId += 1            
+            maxNameId += 1
         # Feature Ids
-        featureNames = [f.strip() for f in line[1].split()]             
+        featureNames = [f.strip() for f in line[1].split()]
+        features = []
         for fn in featureNames:
-            if not featureIdDict.has_key(fn):
-                featureIdDict[fn] = maxFeatureId
-                maxFeatureId += 1
-        featureIds = [featureIdDict[fn] for fn in featureNames]
+            tmp = fn.split('=')
+            if len(tmp) == 2:
+                if not featureIdDict.has_key(tmp[0]):
+                    featureIdDict[tmp[0]] = maxFeatureId
+                    maxFeatureId += 1
+                features.append((featureIdDict[tmp[0]],float(tmp[1])))
+            else:
+                if not featureIdDict.has_key(fn):
+                    featureIdDict[fn] = maxFeatureId
+                    maxFeatureId += 1
+                features.append((featureIdDict[fn],1.0))
         # Store results
-        featureDict[nameId] = featureIds
+        featureDict[nameId] = features
     IS.close()
     return featureDict,maxNameId,maxFeatureId
-     
+
 def create_dependencies_dict(nameIdDict,inputFile):
     logger = logging.getLogger('create_dependencies_dict')
     dependenciesDict = {}
     IS = open(inputFile,'r')
     for line in IS:
         line = line.split(':')
-        name = line[0]        
+        name = line[0]
         # Name Id
         if not nameIdDict.has_key(name):
             logger.warning('%s is missing in nameIdDict. Aborting.',name)
             sys.exit(-1)
 
         nameId = nameIdDict[name]
-        dependenciesIds = [nameIdDict[f.strip()] for f in line[1].split()]             
+        dependenciesIds = [nameIdDict[f.strip()] for f in line[1].split()]
         # Store results, add p proves p
         dependenciesDict[nameId] = [nameId] + dependenciesIds
     IS.close()
@@ -67,19 +75,17 @@
     IS = open(inputFile,'r')
     for line in IS:
         line = line.split(':')
-        name = line[0]     
+        name = line[0]
         # Name Id
         if not nameIdDict.has_key(name):
             logger.warning('%s is missing in nameIdDict. Adding it as theory.',name)
             nameIdDict[name] = maxNameId
             idNameDict[maxNameId] = name
             nameId = maxNameId
-            maxNameId += 1  
+            maxNameId += 1
         else:
             nameId = nameIdDict[name]
         accessibleStrings = line[1].split()
         accessibleDict[nameId] = [nameIdDict[a.strip()] for a in accessibleStrings]
     IS.close()
     return accessibleDict,maxNameId
-        
-    
\ No newline at end of file
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/snow.py	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/snow.py	Thu Dec 06 11:42:23 2012 +0100
@@ -27,13 +27,13 @@
         '''
         self.logger = logging.getLogger('SNoW')
         self.SNoWTrainFile = '../tmp/snow.train'
-        self.SNoWTestFile = '../snow.test'  
-        self.SNoWNetFile = '../tmp/snow.net' 
-    
+        self.SNoWTestFile = '../snow.test'
+        self.SNoWNetFile = '../tmp/snow.net'
+
     def initializeModel(self,trainData,dicts):
         """
         Build basic model from training data.
-        """     
+        """
         # Prepare input files
         self.logger.debug('Creating IO Files')
         OS = open(self.SNoWTrainFile,'w')
@@ -44,60 +44,60 @@
             dependencies = dicts.dependenciesDict[nameId]
             dependencies = map(str,dependencies)
             dependenciesString = string.join(dependencies,',')
-            snowString = string.join([featureString,dependenciesString],',')+':\n' 
+            snowString = string.join([featureString,dependenciesString],',')+':\n'
             OS.write(snowString)
         OS.close()
 
         # Build Model
         self.logger.debug('Building Model START.')
-        snowTrainCommand = '../bin/snow -train -M+ -I %s -F %s -g- -B :0-%s' % (self.SNoWTrainFile,self.SNoWNetFile,dicts.maxNameId-1)    
+        snowTrainCommand = '../bin/snow -train -M+ -I %s -F %s -g- -B :0-%s' % (self.SNoWTrainFile,self.SNoWNetFile,dicts.maxNameId-1)
         args = shlex.split(snowTrainCommand)
-        p = subprocess.Popen(args,stdout=subprocess.PIPE,stderr=subprocess.STDOUT)    
+        p = subprocess.Popen(args,stdout=subprocess.PIPE,stderr=subprocess.STDOUT)
         p.wait()
-        self.logger.debug('Building Model END.')   
+        self.logger.debug('Building Model END.')
 
-    
+
     def update(self,dataPoint,features,dependencies,dicts):
         """
         Updates the Model.
         THIS IS NOT WORKING ATM< BUT WE DONT CARE
-        """        
-        self.logger.debug('Updating Model START') 
-        trainData = dicts.featureDict.keys()       
+        """
+        self.logger.debug('Updating Model START')
+        trainData = dicts.featureDict.keys()
         self.initializeModel(trainData,dicts)
         self.logger.debug('Updating Model END')
-            
-    
+
+
     def predict(self,features,accessibles,dicts):
         logger = logging.getLogger('predict_SNoW')
-         
+
         OS = open(self.SNoWTestFile,'w')
         features = map(str,features)
         featureString = string.join(features, ',')
         snowString = featureString+':'
         OS.write(snowString)
-        OS.close() 
-        
+        OS.close()
+
         snowTestCommand = '../bin/snow -test -I %s -F %s -o allboth' % (self.SNoWTestFile,self.SNoWNetFile)
         args = shlex.split(snowTestCommand)
-        p = subprocess.Popen(args,stdout=subprocess.PIPE,stderr=subprocess.STDOUT)    
+        p = subprocess.Popen(args,stdout=subprocess.PIPE,stderr=subprocess.STDOUT)
         (lines, _stderrdata) = p.communicate()
         logger.debug('SNoW finished.')
-        lines = lines.split('\n')    
+        lines = lines.split('\n')
         assert lines[9].startswith('Example ')
         assert lines[-4] == ''
-        predictionsCon = []    
+        predictionsCon = []
         for line in lines[10:-4]:
             premiseId = int(line.split()[0][:-1])
             predictionsCon.append(premiseId)
         return predictionsCon
-    
+
     def save(self,fileName):
         OStream = open(fileName, 'wb')
-        dump(self.counts,OStream)        
+        dump(self.counts,OStream)
         OStream.close()
-        
+
     def load(self,fileName):
         OStream = open(fileName, 'rb')
-        self.counts = load(OStream)      
-        OStream.close()
\ No newline at end of file
+        self.counts = load(OStream)
+        OStream.close()
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/stats.py	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/stats.py	Thu Dec 06 11:42:23 2012 +0100
@@ -32,18 +32,38 @@
         self.recallData = [0]*cutOff
         self.recall100Data = [0]*cutOff
         self.aucData = []
-        
-    def update(self,predictions,dependencies):
+        self.premiseOccurenceCounter = {}
+        self.firstDepAppearance = {}
+        self.depAppearances = []
+
+    def update(self,predictions,dependencies,statementCounter):
         """
         Evaluates AUC, dependencies, recall100 and number of available premises of a prediction.
         """
-
         available = len(predictions)
         predictions = predictions[:self.cutOff]
         dependencies = set(dependencies)
+        # No Stats for if no dependencies
+        if len(dependencies) == 0:
+            self.logger.debug('No Dependencies for statement %s' % statementCounter )
+            self.badPreds = []
+            return
+        if len(predictions) < self.cutOff:
+            for i in range(len(predictions),self.cutOff):
+                self.recall100Data[i] += 1
+                self.recallData[i] += 1
+        for d in dependencies:
+            if self.premiseOccurenceCounter.has_key(d):
+                self.premiseOccurenceCounter[d] += 1
+            else:
+                self.premiseOccurenceCounter[d] = 1
+            if self.firstDepAppearance.has_key(d):
+                self.depAppearances.append(statementCounter-self.firstDepAppearance[d])
+            else:
+                self.firstDepAppearance[d] = statementCounter
         depNr = len(dependencies)
-        aucSum = 0.    
-        posResults = 0.        
+        aucSum = 0.
+        posResults = 0.
         positives, negatives = 0, 0
         recall100 = 0.0
         badPreds = []
@@ -56,7 +76,7 @@
                 depsFound.append(pId)
                 if index > 200:
                     badPreds.append(pId)
-            else:            
+            else:
                 aucSum += posResults
                 negatives+=1
             # Update Recall and Recall100 stats
@@ -66,7 +86,7 @@
                 self.recallData[index] += 1
             else:
                 self.recallData[index] += float(positives)/depNr
-    
+
         if not depNr == positives:
             depsFound = set(depsFound)
             missing = []
@@ -78,28 +98,29 @@
                     positives+=1
             self.logger.debug('Dependencies missing for %s in accessibles! Estimating Statistics.',\
                               string.join([str(dep) for dep in missing],','))
-    
+
         if positives == 0 or negatives == 0:
             auc = 1.0
-        else:            
+        else:
             auc = aucSum/(negatives*positives)
-        
+
         self.aucData.append(auc)
         self.avgAUC += auc
         self.avgRecall100 += recall100
         self.problems += 1
         self.badPreds = badPreds
-        self.avgAvailable += available 
+        self.avgAvailable += available
         self.avgDepNr += depNr
-        self.logger.info('AUC: %s \t Needed: %s \t Recall100: %s \t Available: %s \t cutOff:%s',\
-                          round(100*auc,2),depNr,recall100,available,self.cutOff)        
-        
+        self.logger.info('Statement: %s: AUC: %s \t Needed: %s \t Recall100: %s \t Available: %s \t cutOff:%s',\
+                          statementCounter,round(100*auc,2),depNr,recall100,available,self.cutOff)
+
     def printAvg(self):
         self.logger.info('Average results:')
         self.logger.info('avgAUC: %s \t avgDepNr: %s \t avgRecall100: %s \t cutOff:%s', \
-                         round(100*self.avgAUC/self.problems,2),round(self.avgDepNr/self.problems,2),self.avgRecall100/self.problems,self.cutOff)
+                         round(100*self.avgAUC/self.problems,2),round(self.avgDepNr/self.problems,2),round(self.avgRecall100/self.problems,2),self.cutOff)
 
-        try:
+        #try:
+        if True:
             from matplotlib.pyplot import plot,figure,show,xlabel,ylabel,axis,hist
             avgRecall = [float(x)/self.problems for x in self.recallData]
             figure('Recall')
@@ -116,15 +137,30 @@
             hist(self.aucData,bins=100)
             ylabel('Problems')
             xlabel('AUC')
+            maxCount = max(self.premiseOccurenceCounter.values())
+            minCount = min(self.premiseOccurenceCounter.values())
+            figure('Dependency Occurances')
+            hist(self.premiseOccurenceCounter.values(),bins=range(minCount,maxCount+2),align = 'left')
+            #ylabel('Occurences')
+            xlabel('Number of Times a Dependency Occurs')
+            figure('Dependency Appearance in Problems after Introduction.')
+            hist(self.depAppearances,bins=50)
+            figure('Dependency Appearance in Problems after Introduction in Percent.')
+            xAxis = range(max(self.depAppearances)+1)
+            yAxis = [0] * (max(self.depAppearances)+1)
+            for val in self.depAppearances:
+                yAxis[val] += 1
+            yAxis = [float(x)/len(self.firstDepAppearance.keys()) for x in yAxis]
+            plot(xAxis,yAxis)
             show()
-        except:
-            self.logger.warning('Matplotlib module missing. Skipping graphs.')
-    
-    def save(self,fileName):       
+        #except:
+        #    self.logger.warning('Matplotlib module missing. Skipping graphs.')
+
+    def save(self,fileName):
         oStream = open(fileName, 'wb')
-        dump((self.avgAUC,self.avgRecall100,self.avgAvailable,self.avgDepNr,self.problems,self.cutOff,self.recallData,self.recall100Data,self.aucData),oStream)
+        dump((self.avgAUC,self.avgRecall100,self.avgAvailable,self.avgDepNr,self.problems,self.cutOff,self.recallData,self.recall100Data,self.aucData,self.premiseOccurenceCounter),oStream)
         oStream.close()
     def load(self,fileName):
-        iStream = open(fileName, 'rb')        
-        self.avgAUC,self.avgRecall100,self.avgAvailable,self.avgDepNr,self.problems,self.cutOff,self.recallData,self.recall100Data,self.aucData = load(iStream)
-        iStream.close()
\ No newline at end of file
+        iStream = open(fileName, 'rb')
+        self.avgAUC,self.avgRecall100,self.avgAvailable,self.avgDepNr,self.problems,self.cutOff,self.recallData,self.recall100Data,self.aucData,self.premiseOccurenceCounter = load(iStream)
+        iStream.close()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:42:23 2012 +0100
@@ -44,7 +44,8 @@
   val suggested_facts :
     (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list
   val mesh_facts :
-    int -> ((('a * thm) * real) list * ('a * thm) list) list -> ('a * thm) list
+    int -> (real * ((('a * thm) * real) list * ('a * thm) list)) list
+    -> ('a * thm) list
   val theory_ord : theory * theory -> order
   val thm_ord : thm * thm -> order
   val goal_of_thm : theory -> thm -> thm
@@ -57,9 +58,10 @@
   val atp_dependencies_of :
     Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
     -> thm -> bool * string list option
+  val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list
   val mash_suggested_facts :
-    Proof.context -> params -> string -> int -> term list -> term
-    -> fact list -> (fact * real) list * fact list
+    Proof.context -> params -> string -> int -> term list -> term -> fact list
+    -> fact list
   val mash_learn_proof :
     Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
     -> unit
@@ -178,18 +180,9 @@
 val unescape_metas =
   space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
 
-val supports_weights = false
-
 fun encode_feature (name, weight) =
-  let val s = escape_meta name in
-    if Real.== (weight, 1.0) then
-      s
-    else if supports_weights then
-      s ^ "=" ^ Real.toString weight
-    else
-      map (prefix (s ^ ".") o string_of_int) (1 upto Real.ceil weight)
-      |> space_implode " "
-  end
+  escape_meta name ^
+  (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
 
 val encode_features = map encode_feature #> space_implode " "
 
@@ -297,7 +290,7 @@
 
 local
 
-val version = "*** MaSh version 20121204a ***"
+val version = "*** MaSh version 20121205c ***"
 
 exception Too_New of unit
 
@@ -424,43 +417,57 @@
       Symtab.lookup tab name |> Option.map (rpair weight)
   in map_filter find_sugg suggs end
 
-fun sum_avg [] = 0
-  | sum_avg xs =
+fun scaled_avg [] = 0
+  | scaled_avg xs =
     Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
 
-fun normalize_scores [] = []
-  | normalize_scores ((fact, score) :: tail) =
-    (fact, 1.0) :: map (apsnd (curry Real.* (1.0 / score))) tail
+fun avg [] = 0.0
+  | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs)
 
-fun mesh_facts max_facts [(sels, unks)] =
+fun normalize_scores _ [] = []
+  | normalize_scores max_facts xs =
+    let val avg = avg (map snd (take max_facts xs)) in
+      map (apsnd (curry Real.* (1.0 / avg))) xs
+    end
+
+fun mesh_facts max_facts [(_, (sels, unks))] =
     map fst (take max_facts sels) @ take (max_facts - length sels) unks
   | mesh_facts max_facts mess =
     let
-      val mess = mess |> map (apfst (normalize_scores #> `length))
+      val mess =
+        mess |> map (apsnd (apfst (normalize_scores max_facts #> `length)))
       val fact_eq = Thm.eq_thm o pairself snd
-      fun score_at sels = try (nth sels) #> Option.map snd
-      fun score_in fact ((sel_len, sels), unks) =
-        case find_index (curry fact_eq fact o fst) sels of
-          ~1 => (case find_index (curry fact_eq fact) unks of
-                   ~1 => score_at sels sel_len
-                 | _ => NONE)
-        | rank => score_at sels rank
-      fun weight_of fact = mess |> map_filter (score_in fact) |> sum_avg
+      fun score_in fact (global_weight, ((sel_len, sels), unks)) =
+        let
+          fun score_at j =
+            case try (nth sels) j of
+              SOME (_, score) => SOME (global_weight * score)
+            | NONE => NONE
+        in
+          case find_index (curry fact_eq fact o fst) sels of
+            ~1 => (case find_index (curry fact_eq fact) unks of
+                     ~1 => score_at sel_len
+                   | _ => NONE)
+          | rank => score_at rank
+        end
+      fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
       val facts =
-        fold (union fact_eq o map fst o take max_facts o snd o fst) mess []
+        fold (union fact_eq o map fst o take max_facts o snd o fst o snd) mess
+             []
     in
       facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
             |> map snd |> take max_facts
     end
 
-fun thy_feature_of s = ("y" ^ s, 1.0 (* FUDGE *))
-fun term_feature_of s = ("c" ^ s, 1.0 (* FUDGE *))
-fun type_feature_of s = ("t" ^ s, 1.0 (* FUDGE *))
-fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
-fun status_feature_of status = (string_of_status status, 1.0 (* FUDGE *))
-val local_feature = ("local", 20.0 (* FUDGE *))
-val lams_feature = ("lams", 1.0 (* FUDGE *))
-val skos_feature = ("skos", 1.0 (* FUDGE *))
+fun thy_feature_of s = ("y" ^ s, 0.5 (* FUDGE *))
+fun const_feature_of s = ("c" ^ s, 1.0 (* FUDGE *))
+fun free_feature_of s = ("f" ^ s, 2.0 (* FUDGE *))
+fun type_feature_of s = ("t" ^ s, 0.5 (* FUDGE *))
+fun class_feature_of s = ("s" ^ s, 0.25 (* FUDGE *))
+fun status_feature_of status = (string_of_status status, 0.5 (* FUDGE *))
+val local_feature = ("local", 2.0 (* FUDGE *))
+val lams_feature = ("lams", 0.5 (* FUDGE *))
+val skos_feature = ("skos", 0.5 (* FUDGE *))
 
 fun theory_ord p =
   if Theory.eq_thy p then
@@ -473,11 +480,11 @@
     EQUAL => string_ord (pairself Context.theory_name p)
   | order => order
 
-fun thm_ord thp =
-  case theory_ord (pairself theory_of_thm thp) of
+fun thm_ord p =
+  case theory_ord (pairself theory_of_thm p) of
     EQUAL =>
     (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
-    string_ord (pairself nickname_of (swap thp))
+    string_ord (pairself nickname_of (swap p))
   | ord => ord
 
 val freezeT = Type.legacy_freeze_type
@@ -507,14 +514,22 @@
 val logical_consts =
   [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts
 
-fun interesting_terms_types_and_classes ctxt prover term_max_depth
+fun interesting_terms_types_and_classes ctxt thy_name prover term_max_depth
                                         type_max_depth ts =
   let
+    val thy = Proof_Context.theory_of ctxt
+    val fixes = map snd (Variable.dest_fixes ctxt)
+    val classes = Sign.classes_of thy
     fun is_bad_const (x as (s, _)) args =
       member (op =) logical_consts s orelse
       fst (is_built_in_const_for_prover ctxt prover x args)
     fun add_classes @{sort type} = I
-      | add_classes S = union (op = o pairself fst) (map class_feature_of S)
+      | add_classes S =
+        fold (`(Sorts.super_classes classes)
+              #> swap #> op ::
+              #> subtract (op =) @{sort type}
+              #> map class_feature_of
+              #> union (op = o pairself fst)) S
     fun do_add_type (Type (s, Ts)) =
         (not (member (op =) bad_types s)
          ? insert (op = o pairself fst) (type_feature_of s))
@@ -525,24 +540,30 @@
     fun patternify_term _ ~1 _ = []
       | patternify_term args _ (Const (x as (s, _))) =
         if is_bad_const x args then [] else [s]
+      | patternify_term _ depth (Free (s, _)) =
+        if depth = term_max_depth andalso member (op =) fixes s then
+          [thy_name ^ Long_Name.separator ^ s]
+        else
+          []
       | patternify_term _ 0 _ = []
       | patternify_term args depth (t $ u) =
         let
           val ps = patternify_term (u :: args) depth t
           val qs = "" :: patternify_term [] (depth - 1) u
-        in map_product (fn p => fn "" => p | q => "(" ^ q ^ ")") ps qs end
+        in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end
       | patternify_term _ _ _ = []
-    val add_term_pattern =
-      union (op = o pairself fst) o map term_feature_of oo patternify_term []
-    fun add_term_patterns ~1 _ = I
-      | add_term_patterns depth t =
-        add_term_pattern depth t #> add_term_patterns (depth - 1) t
-    val add_term = add_term_patterns term_max_depth
+    fun add_term_pattern feature_of =
+      union (op = o pairself fst) o map feature_of oo patternify_term []
+    fun add_term_patterns _ ~1 _ = I
+      | add_term_patterns feature_of depth t =
+        add_term_pattern feature_of depth t
+        #> add_term_patterns feature_of (depth - 1) t
+    fun add_term feature_of = add_term_patterns feature_of term_max_depth
     fun add_patterns t =
       let val (head, args) = strip_comb t in
         (case head of
-           Const (_, T) => add_term t #> add_type T
-         | Free (_, T) => add_type T
+           Const (_, T) => add_term const_feature_of t #> add_type T
+         | Free (_, T) => add_term free_feature_of t #> add_type T
          | Var (_, T) => add_type T
          | Abs (_, T, body) => add_type T #> add_patterns body
          | _ => I)
@@ -552,22 +573,24 @@
 
 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
 
-val term_max_depth = 2
-val type_max_depth = 2
+val term_max_depth = 1
+val type_max_depth = 1
 
 (* TODO: Generate type classes for types? *)
 fun features_of ctxt prover thy (scope, status) ts =
-  thy_feature_of (Context.theory_name thy) ::
-  interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
-                                      ts
-  |> status <> General ? cons (status_feature_of status)
-  |> scope <> Global ? cons local_feature
-  |> exists (not o is_lambda_free) ts ? cons lams_feature
-  |> exists (exists_Const is_exists) ts ? cons skos_feature
+  let val thy_name = Context.theory_name thy in
+    thy_feature_of thy_name ::
+    interesting_terms_types_and_classes ctxt thy_name prover term_max_depth
+        type_max_depth ts
+    |> status <> General ? cons (status_feature_of status)
+    |> scope <> Global ? cons local_feature
+    |> exists (not o is_lambda_free) ts ? cons lams_feature
+    |> exists (exists_Const is_exists) ts ? cons skos_feature
+  end
 
 (* Too many dependencies is a sign that a crazy decision procedure is at work.
    There isn't much to learn from such proofs. *)
-val max_dependencies = 100
+val max_dependencies = 10
 val atp_dependency_default_max_facts = 50
 
 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
@@ -691,23 +714,23 @@
                                       (Graph.imm_preds fact_G new) news))
   in find_maxes Symtab.empty ([], Graph.maximals fact_G) end
 
-(* Generate more suggestions than requested, because some might be thrown out
-   later for various reasons and "meshing" gives better results with some
-   slack. *)
-fun max_suggs_of max_facts = max_facts + Int.min (50, max_facts)
-
 fun is_fact_in_graph fact_G (_, th) =
   can (Graph.get_node fact_G) (nickname_of th)
 
-fun interleave 0 _ _ = []
-  | interleave n [] ys = take n ys
-  | interleave n xs [] = take n xs
-  | interleave 1 (x :: _) _ = [x]
-  | interleave n (x :: xs) (y :: ys) = x :: y :: interleave (n - 2) xs ys
-
 (* factor that controls whether unknown global facts should be included *)
 val include_unk_global_factor = 15
 
+(* use MePo weights for now *)
+val weight_raw_mash_facts = weight_mepo_facts
+val weight_mash_facts = weight_raw_mash_facts
+
+(* FUDGE *)
+fun weight_of_proximity_fact rank =
+  Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
+
+fun weight_proximity_facts facts =
+  facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
+
 fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                          concl_t facts =
   let
@@ -722,28 +745,21 @@
               val feats =
                 features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
             in
-              (fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts)
-                                  (parents, feats))
+              (fact_G, mash_QUERY ctxt overlord max_facts (parents, feats))
             end)
-    val (chained, unchained) =
-      List.partition (fn ((_, (scope, _)), _) => scope = Chained) facts
-    val sels =
+    val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
+    val raw_mash =
       facts |> suggested_facts suggs
             (* The weights currently returned by "mash.py" are too spaced out to
                make any sense. *)
             |> map fst
-            |> filter_out (member (Thm.eq_thm_prop o pairself snd) chained)
-    val (unk_global, unk_local) =
-      unchained |> filter_out (is_fact_in_graph fact_G)
-                |> List.partition (fn ((_, (scope, _)), _) => scope = Global)
-    val (small_unk_global, big_unk_global) =
-      ([], unk_global)
-      |> include_unk_global_factor * length unk_global <= max_facts ? swap
-  in
-    (interleave max_facts (chained @ unk_local @ small_unk_global) sels
-     |> weight_mepo_facts (* use MePo weights for now *),
-     big_unk_global)
-  end
+    val proximity = facts |> sort (thm_ord o pairself snd o swap)
+    val unknown = facts |> filter_out (is_fact_in_graph fact_G)
+    val mess =
+      [(0.8000 (* FUDGE *), (map (rpair 1.0) chained, [])),
+       (0.1333 (* FUDGE *), (weight_raw_mash_facts raw_mash, unknown)),
+       (0.0667 (* FUDGE *), (weight_proximity_facts proximity, []))]
+  in mesh_facts max_facts mess end
 
 fun add_wrt_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
   let
@@ -993,6 +1009,10 @@
 fun is_mash_enabled () = (getenv "MASH" = "yes")
 fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt)))
 
+(* Generate more suggestions than requested, because some might be thrown out
+   later for various reasons. *)
+fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts)
+
 (* The threshold should be large enough so that MaSh doesn't kick in for Auto
    Sledgehammer and Try. *)
 val min_secs_for_learning = 15
@@ -1034,14 +1054,16 @@
          (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
         |> take max_facts
       fun mepo () =
-        facts |> mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts
-                                      concl_t
-              |> weight_mepo_facts
+        mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t
+                             facts
+        |> weight_mepo_facts
       fun mash () =
-        mash_suggested_facts ctxt params prover max_facts hyp_ts concl_t facts
+        mash_suggested_facts ctxt params prover (generous_max_facts max_facts)
+            hyp_ts concl_t facts
+        |> weight_mash_facts
       val mess =
-        [] |> (if fact_filter <> mashN then cons (mepo (), []) else I)
-           |> (if fact_filter <> mepoN then cons (mash ()) else I)
+        [] |> (if fact_filter <> mashN then cons (0.5, (mepo (), [])) else I)
+           |> (if fact_filter <> mepoN then cons (0.5, (mash (), [])) else I)
     in
       mesh_facts max_facts mess
       |> not (null add_ths) ? prepend_facts add_ths
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Dec 06 11:37:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Dec 06 11:42:23 2012 +0100
@@ -18,10 +18,10 @@
   val const_names_in_fact :
     theory -> (string * typ -> term list -> bool * term list) -> term
     -> string list
+  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
   val mepo_suggested_facts :
     Proof.context -> params -> string -> int -> relevance_fudge option
     -> term list -> term -> fact list -> fact list
-  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
 end;
 
 structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
@@ -509,6 +509,14 @@
                       "Total relevant: " ^ string_of_int (length accepts)))
   end
 
+(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
+(* FUDGE *)
+fun weight_of_mepo_fact rank =
+  Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
+
+fun weight_mepo_facts facts =
+  facts ~~ map weight_of_mepo_fact (0 upto length facts - 1)
+
 fun mepo_suggested_facts ctxt
         ({fact_thresholds = (thres0, thres1), ...} : params) prover
         max_facts fudge hyp_ts concl_t facts =
@@ -535,10 +543,4 @@
            (concl_t |> theory_constify fudge (Context.theory_name thy)))
   end
 
-(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
-fun weight_of_fact rank = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
-
-fun weight_mepo_facts facts =
-  facts ~~ map weight_of_fact (0 upto length facts - 1)
-
 end;