--- 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;