--- a/Admin/mira.py Tue Mar 22 20:44:47 2011 +0100
+++ b/Admin/mira.py Tue Mar 22 21:22:50 2011 +0100
@@ -294,21 +294,11 @@
return (some_success, '', data, raw_attachments, None)
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_Arrow(*args):
- """Judgement Day regression suite Arrow"""
- return judgement_day('Afp/thys/ArrowImpossibilityGS/Thys', 'Arrow_Order', 'prover_timeout=10', *args)
-
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
def JD_NS(*args):
"""Judgement Day regression suite NS"""
return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args)
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_FFT(*args):
- """Judgement Day regression suite FFT"""
- return judgement_day('Afp/thys/FFT', 'FFT', 'prover_timeout=10', *args)
-
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
def JD_FTA(*args):
"""Judgement Day regression suite FTA"""
@@ -317,25 +307,10 @@
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
def JD_Hoare(*args):
"""Judgement Day regression suite Hoare"""
- return judgement_day('Isabelle/src/HOL/IMP', 'Hoare', 'prover_timeout=10', *args)
-
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_Jinja(*args):
- """Judgement Day regression suite Jinja"""
- return judgement_day('Afp/thys/Jinja/J', 'TypeSafe', 'prover_timeout=10', *args)
+ return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args)
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
def JD_SN(*args):
"""Judgement Day regression suite SN"""
- return judgement_day('Isabelle/src/HOL/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
+ return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_QE(*args):
- """Judgement Day regression suite QE"""
- return judgement_day('Afp/thys/LinearQuantifierElim/Thys', 'QEpres', 'prover_timeout=10', *args)
-
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_S2S(*args):
- """Judgement Day regression suite S2S"""
- return judgement_day('Afp/thys/SumSquares', 'TwoSquares', 'prover_timeout=10', *args)
-
--- a/src/HOL/IsaMakefile Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/IsaMakefile Tue Mar 22 21:22:50 2011 +0100
@@ -319,6 +319,7 @@
Tools/Nitpick/nitpick_scope.ML \
Tools/Nitpick/nitpick_tests.ML \
Tools/Nitpick/nitpick_util.ML \
+ Tools/Nitpick/nitrox.ML \
Tools/numeral.ML \
Tools/numeral_simprocs.ML \
Tools/numeral_syntax.ML \
@@ -466,8 +467,8 @@
Library/Sublist_Order.thy Library/Sum_of_Squares.thy \
Library/Sum_of_Squares/sos_wrapper.ML \
Library/Sum_of_Squares/sum_of_squares.ML \
- Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \
- Library/While_Combinator.thy Library/Zorn.thy \
+ Library/TPTP.thy Library/Transitive_Closure_Table.thy \
+ Library/Univ_Poly.thy Library/While_Combinator.thy Library/Zorn.thy \
$(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \
Library/reflection.ML Library/reify_data.ML \
Library/Quickcheck_Narrowing.thy \
--- a/src/HOL/Library/README.html Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Library/README.html Tue Mar 22 21:22:50 2011 +0100
@@ -12,8 +12,7 @@
<h1>HOL-Library: supplemental theories for main Isabelle/HOL</h1>
This is a collection of generic theories that may be used together
-with main Isabelle/HOL. Note that theory loader path already includes
-this directory by default.
+with main Isabelle/HOL.
<p>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/TPTP.thy Tue Mar 22 21:22:50 2011 +0100
@@ -0,0 +1,50 @@
+theory TPTP
+imports Main
+uses "~~/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML"
+begin
+
+declare mem_def [simp add]
+
+declare [[smt_oracle]]
+
+ML {* proofs := 0 *}
+
+ML {*
+fun SOLVE_TIMEOUT seconds name tac st =
+ let
+ val result =
+ TimeLimit.timeLimit (Time.fromSeconds seconds)
+ (fn () => SINGLE (SOLVE tac) st) ()
+ handle TimeLimit.TimeOut => NONE
+ | ERROR _ => NONE
+ in
+ (case result of
+ NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
+ | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
+ end
+*}
+
+ML {*
+fun isabellep_tac max_secs =
+ SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
+ (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset}))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset}))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset}
+ THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} []))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset}))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset}))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset}))
+ ORELSE
+ SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset}))
+*}
+
+end
--- a/src/HOL/Nitpick.thy Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Nitpick.thy Tue Mar 22 21:22:50 2011 +0100
@@ -24,8 +24,10 @@
("Tools/Nitpick/nitpick.ML")
("Tools/Nitpick/nitpick_isar.ML")
("Tools/Nitpick/nitpick_tests.ML")
+ ("Tools/Nitpick/nitrox.ML")
begin
+typedecl iota (* for Nitrox *)
typedecl bisim_iterator
axiomatization unknown :: 'a
@@ -231,6 +233,7 @@
use "Tools/Nitpick/nitpick.ML"
use "Tools/Nitpick/nitpick_isar.ML"
use "Tools/Nitpick/nitpick_tests.ML"
+use "Tools/Nitpick/nitrox.ML"
setup {* Nitpick_Isar.setup *}
@@ -239,7 +242,8 @@
fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
number_of_frac inverse_frac less_frac less_eq_frac of_frac
-hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
+hide_type (open) iota bisim_iterator fun_box pair_box unsigned_bit signed_bit
+ word
hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
prod_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold
--- a/src/HOL/Probability/Borel_Space.thy Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Tue Mar 22 21:22:50 2011 +0100
@@ -1,4 +1,7 @@
-(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
+(* Title: HOL/Probability/Lebesgue_Integration.thy
+ Author: Johannes Hölzl, TU München
+ Author: Armin Heller, TU München
+*)
header {*Borel spaces*}
--- a/src/HOL/Probability/Caratheodory.thy Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Tue Mar 22 21:22:50 2011 +0100
@@ -1,9 +1,18 @@
+(* Title: HOL/Probability/Caratheodory.thy
+ Author: Lawrence C Paulson
+ Author: Johannes Hölzl, TU München
+*)
+
header {*Caratheodory Extension Theorem*}
theory Caratheodory
imports Sigma_Algebra Extended_Real_Limits
begin
+text {*
+ Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
+*}
+
lemma suminf_extreal_2dimen:
fixes f:: "nat \<times> nat \<Rightarrow> extreal"
assumes pos: "\<And>p. 0 \<le> f p"
@@ -36,8 +45,6 @@
SUPR_extreal_setsum[symmetric] incseq_setsumI setsum_nonneg)
qed
-text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
-
subsection {* Measure Spaces *}
record 'a measure_space = "'a algebra" +
@@ -148,7 +155,7 @@
lemma (in algebra) lambda_system_empty:
"positive M f \<Longrightarrow> {} \<in> lambda_system M f"
- by (auto simp add: positive_def lambda_system_eq algebra_def)
+ by (auto simp add: positive_def lambda_system_eq)
lemma lambda_system_sets:
"x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M"
@@ -217,7 +224,7 @@
lemma (in algebra) lambda_system_algebra:
"positive M f \<Longrightarrow> algebra (M\<lparr>sets := lambda_system M f\<rparr>)"
- apply (auto simp add: algebra_def)
+ apply (auto simp add: algebra_iff_Un)
apply (metis lambda_system_sets set_mp sets_into_space)
apply (metis lambda_system_empty)
apply (metis lambda_system_Compl)
@@ -332,9 +339,10 @@
by (force simp add: disjoint_family_on_def neq_iff)
have 3: "A n \<in> lambda_system M f" using A
by blast
+ interpret l: algebra "M\<lparr>sets := lambda_system M f\<rparr>"
+ using f by (rule lambda_system_algebra)
have 4: "UNION {0..<n} A \<in> lambda_system M f"
- using A algebra.UNION_in_sets [OF local.lambda_system_algebra, of f, OF f]
- by simp
+ using A l.UNION_in_sets by simp
from Suc.hyps show ?case
by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
qed
@@ -352,8 +360,8 @@
by (metis countably_subadditive_subadditive csa pos)
have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A
by simp
- have alg_ls: "algebra (M(|sets := lambda_system M f|))"
- by (rule lambda_system_algebra) (rule pos)
+ interpret ls: algebra "M\<lparr>sets := lambda_system M f\<rparr>"
+ using pos by (rule lambda_system_algebra)
have A'': "range A \<subseteq> sets M"
by (metis A image_subset_iff lambda_system_sets)
@@ -366,7 +374,7 @@
have *: "\<And>i. 0 \<le> f (A i)" using pos A'' unfolding positive_def by auto
have dis: "\<And>N. disjoint_family_on A {..<N}" by (intro disjoint_family_on_mono[OF _ disj]) auto
show "(\<Sum>i. f (A i)) \<le> f (\<Union>i. A i)"
- using algebra.additive_sum [OF alg_ls lambda_system_positive[OF pos] lambda_system_additive _ A' dis]
+ using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis]
using A''
by (intro suminf_bound[OF _ *]) (auto intro!: increasingD[OF inc] allI countable_UN)
qed
@@ -401,8 +409,7 @@
have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
- using algebra.UNION_in_sets [OF lambda_system_algebra [of f, OF pos]]
- by (simp add: A)
+ using ls.UNION_in_sets by (simp add: A)
hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
by (simp add: lambda_system_eq UNION_in)
have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
@@ -441,8 +448,8 @@
by (metis oms outer_measure_space_def)
have alg: "algebra ?M"
using lambda_system_algebra [of f, OF pos]
- by (simp add: algebra_def)
- then moreover
+ by (simp add: algebra_iff_Un)
+ then
have "sigma_algebra ?M"
using lambda_system_caratheodory [OF oms]
by (simp add: sigma_algebra_disjoint_iff)
@@ -453,10 +460,10 @@
countably_additive_def o_def)
ultimately
show ?thesis
- by intro_locales (auto simp add: sigma_algebra_def)
+ by (simp add: measure_space_def)
qed
-lemma (in algebra) additive_increasing:
+lemma (in ring_of_sets) additive_increasing:
assumes posf: "positive M f" and addf: "additive M f"
shows "increasing M f"
proof (auto simp add: increasing_def)
@@ -472,7 +479,7 @@
finally show "f x \<le> f y" by simp
qed
-lemma (in algebra) countably_additive_additive:
+lemma (in ring_of_sets) countably_additive_additive:
assumes posf: "positive M f" and ca: "countably_additive M f"
shows "additive M f"
proof (auto simp add: additive_def)
@@ -506,7 +513,7 @@
simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
qed
-lemma (in algebra) inf_measure_agrees:
+lemma (in ring_of_sets) inf_measure_agrees:
assumes posf: "positive M f" and ca: "countably_additive M f"
and s: "s \<in> sets M"
shows "Inf (measure_set M f s) = f s"
@@ -575,7 +582,7 @@
inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
qed (rule inf_measure_pos[OF posf])
-lemma (in algebra) inf_measure_positive:
+lemma (in ring_of_sets) inf_measure_positive:
assumes p: "positive M f" and "{} \<in> sets M"
shows "positive M (\<lambda>x. Inf (measure_set M f x))"
proof (unfold positive_def, intro conjI ballI)
@@ -583,7 +590,7 @@
fix A assume "A \<in> sets M"
qed (rule inf_measure_pos[OF p])
-lemma (in algebra) inf_measure_increasing:
+lemma (in ring_of_sets) inf_measure_increasing:
assumes posf: "positive M f"
shows "increasing \<lparr> space = space M, sets = Pow (space M) \<rparr>
(\<lambda>x. Inf (measure_set M f x))"
@@ -593,7 +600,7 @@
apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast)
done
-lemma (in algebra) inf_measure_le:
+lemma (in ring_of_sets) inf_measure_le:
assumes posf: "positive M f" and inc: "increasing M f"
and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M \<and> s \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) = r}"
shows "Inf (measure_set M f s) \<le> x"
@@ -620,73 +627,63 @@
by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower)
qed
-lemma (in algebra) inf_measure_close:
+lemma (in ring_of_sets) inf_measure_close:
fixes e :: extreal
- assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
+ assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)" and "Inf (measure_set M f s) \<noteq> \<infinity>"
shows "\<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and>
(\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e"
-proof (cases "Inf (measure_set M f s) = \<infinity>")
- case False
- then have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>"
+proof -
+ from `Inf (measure_set M f s) \<noteq> \<infinity>` have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>"
using inf_measure_pos[OF posf, of s] by auto
obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e"
using Inf_extreal_close[OF fin e] by auto
thus ?thesis
by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
-next
- case True
- have "measure_set M f s \<noteq> {}"
- by (metis emptyE ss inf_measure_nonempty [of _ f, OF posf top _ empty_sets])
- then obtain l where "l \<in> measure_set M f s" by auto
- moreover from True have "l \<le> Inf (measure_set M f s) + e" by simp
- ultimately show ?thesis
- by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
qed
-lemma (in algebra) inf_measure_countably_subadditive:
+lemma (in ring_of_sets) inf_measure_countably_subadditive:
assumes posf: "positive M f" and inc: "increasing M f"
shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
(\<lambda>x. Inf (measure_set M f x))"
- unfolding countably_subadditive_def o_def
-proof (safe, simp, rule extreal_le_epsilon, safe)
- fix A :: "nat \<Rightarrow> 'a set" and e :: extreal
- let "?outer n" = "Inf (measure_set M f (A n))"
+proof (simp add: countably_subadditive_def, safe)
+ fix A :: "nat \<Rightarrow> 'a set"
+ let "?outer B" = "Inf (measure_set M f B)"
assume A: "range A \<subseteq> Pow (space M)"
and disj: "disjoint_family A"
and sb: "(\<Union>i. A i) \<subseteq> space M"
- and e: "0 < e"
- hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
- A n \<subseteq> (\<Union>i. BB n i) \<and>
- (\<Sum>i. f (BB n i)) \<le> ?outer n + e * (1/2)^(Suc n)"
- apply (safe intro!: choice inf_measure_close [of f, OF posf])
- using e sb by (cases e) (auto simp add: not_le mult_pos_pos one_extreal_def)
- then obtain BB
- where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
+
+ { fix e :: extreal assume e: "0 < e" and "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
+ hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
+ A n \<subseteq> (\<Union>i. BB n i) \<and> (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
+ apply (safe intro!: choice inf_measure_close [of f, OF posf])
+ using e sb by (auto simp: extreal_zero_less_0_iff one_extreal_def)
+ then obtain BB
+ where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
and disjBB: "\<And>n. disjoint_family (BB n)"
and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)"
- and BBle: "\<And>n. (\<Sum>i. f (BB n i)) \<le> ?outer n + e * (1/2)^(Suc n)"
- by auto blast
- have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> suminf ?outer + e"
+ and BBle: "\<And>n. (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
+ by auto blast
+ have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n)) + e"
proof -
have sum_eq_1: "(\<Sum>n. e*(1/2) ^ Suc n) = e"
using suminf_half_series_extreal e
by (simp add: extreal_zero_le_0_iff zero_le_divide_extreal suminf_cmult_extreal)
have "\<And>n i. 0 \<le> f (BB n i)" using posf[unfolded positive_def] BB by auto
then have "\<And>n. 0 \<le> (\<Sum>i. f (BB n i))" by (rule suminf_0_le)
- then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer n + e*(1/2) ^ Suc n)"
+ then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n) + e*(1/2) ^ Suc n)"
by (rule suminf_le_pos[OF BBle])
- also have "... = suminf ?outer + e"
+ also have "... = (\<Sum>n. ?outer (A n)) + e"
using sum_eq_1 inf_measure_pos[OF posf] e
by (subst suminf_add_extreal) (auto simp add: extreal_zero_le_0_iff)
finally show ?thesis .
qed
- def C \<equiv> "(split BB) o prod_decode"
- have C: "!!n. C n \<in> sets M"
- apply (rule_tac p="prod_decode n" in PairE)
- apply (simp add: C_def)
- apply (metis BB subsetD rangeI)
- done
- have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
+ def C \<equiv> "(split BB) o prod_decode"
+ have C: "!!n. C n \<in> sets M"
+ apply (rule_tac p="prod_decode n" in PairE)
+ apply (simp add: C_def)
+ apply (metis BB subsetD rangeI)
+ done
+ have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
proof (auto simp add: C_def)
fix x i
assume x: "x \<in> A i"
@@ -695,23 +692,39 @@
thus "\<exists>i. x \<in> split BB (prod_decode i)"
by (metis prod_encode_inverse prod.cases)
qed
- have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
- by (rule ext) (auto simp add: C_def)
- moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle
- using BB posf[unfolded positive_def]
- by (force intro!: suminf_extreal_2dimen simp: o_def)
- ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def)
- have "Inf (measure_set M f (\<Union>i. A i)) \<le> (\<Sum>n. \<Sum>i. f (BB n i))"
- apply (rule inf_measure_le [OF posf(1) inc], auto)
- apply (rule_tac x="C" in exI)
- apply (auto simp add: C sbC Csums)
- done
- also have "... \<le> (\<Sum>n. Inf (measure_set M f (A n))) + e" using sll
- by blast
- finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ?outer + e" .
+ have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
+ by (rule ext) (auto simp add: C_def)
+ moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle
+ using BB posf[unfolded positive_def]
+ by (force intro!: suminf_extreal_2dimen simp: o_def)
+ ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def)
+ have "?outer (\<Union>i. A i) \<le> (\<Sum>n. \<Sum>i. f (BB n i))"
+ apply (rule inf_measure_le [OF posf(1) inc], auto)
+ apply (rule_tac x="C" in exI)
+ apply (auto simp add: C sbC Csums)
+ done
+ also have "... \<le> (\<Sum>n. ?outer (A n)) + e" using sll
+ by blast
+ finally have "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n)) + e" . }
+ note for_finite_Inf = this
+
+ show "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n))"
+ proof cases
+ assume "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
+ with for_finite_Inf show ?thesis
+ by (intro extreal_le_epsilon) auto
+ next
+ assume "\<not> (\<forall>i. ?outer (A i) \<noteq> \<infinity>)"
+ then have "\<exists>i. ?outer (A i) = \<infinity>"
+ by auto
+ then have "(\<Sum>n. ?outer (A n)) = \<infinity>"
+ using suminf_PInfty[OF inf_measure_pos, OF posf]
+ by metis
+ then show ?thesis by simp
+ qed
qed
-lemma (in algebra) inf_measure_outer:
+lemma (in ring_of_sets) inf_measure_outer:
"\<lbrakk> positive M f ; increasing M f \<rbrakk>
\<Longrightarrow> outer_measure_space \<lparr> space = space M, sets = Pow (space M) \<rparr>
(\<lambda>x. Inf (measure_set M f x))"
@@ -719,12 +732,10 @@
by (simp add: outer_measure_space_def inf_measure_empty
inf_measure_increasing inf_measure_countably_subadditive positive_def)
-(*MOVE UP*)
-
-lemma (in algebra) algebra_subset_lambda_system:
+lemma (in ring_of_sets) algebra_subset_lambda_system:
assumes posf: "positive M f" and inc: "increasing M f"
and add: "additive M f"
- shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
+ shows "sets M \<subseteq> lambda_system \<lparr> space = space M, sets = Pow (space M) \<rparr>
(\<lambda>x. Inf (measure_set M f x))"
proof (auto dest: sets_into_space
simp add: algebra.lambda_system_eq [OF algebra_Pow])
@@ -735,50 +746,42 @@
by blast
have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
\<le> Inf (measure_set M f s)"
- proof (rule extreal_le_epsilon, intro allI impI)
- fix e :: extreal
- assume e: "0 < e"
- from inf_measure_close [of f, OF posf e s]
- obtain A where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
- and sUN: "s \<subseteq> (\<Union>i. A i)"
- and l: "(\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e"
- by auto
- have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
- (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
- by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
- have [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
- by (subst additiveD [OF add, symmetric])
- (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
- { fix u
- assume u: "u \<in> sets M"
- have [simp]: "\<And>n. f (A n \<inter> u) \<le> f (A n)"
- by (simp add: increasingD [OF inc] u Int range_subsetD [OF A])
- have 2: "Inf (measure_set M f (s \<inter> u)) \<le> (\<Sum>i. f (A i \<inter> u))"
- proof (rule complete_lattice_class.Inf_lower)
- show "(\<Sum>i. f (A i \<inter> u)) \<in> measure_set M f (s \<inter> u)"
- apply (simp add: measure_set_def)
- apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI)
- apply (auto simp add: disjoint_family_subset [OF disj] o_def)
- apply (blast intro: u range_subsetD [OF A])
- apply (blast dest: subsetD [OF sUN])
- done
- qed
- } note lesum = this
- have [simp]: "\<And>i. A i \<inter> (space M - x) = A i - x" using A sets_into_space by auto
- have inf1: "Inf (measure_set M f (s\<inter>x)) \<le> (\<Sum>i. f (A i \<inter> x))"
- and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
- \<le> (\<Sum>i. f (A i \<inter> (space M - x)))"
- by (metis Diff lesum top x)+
- hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
- \<le> (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))"
- by (simp add: add_mono x)
- also have "... \<le> (\<Sum>i. f (A i))" using posf[unfolded positive_def] A x
- by (subst suminf_add_extreal[symmetric]) auto
- also have "... \<le> Inf (measure_set M f s) + e"
- by (rule l)
- finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
- \<le> Inf (measure_set M f s) + e" .
+ proof cases
+ assume "Inf (measure_set M f s) = \<infinity>" then show ?thesis by simp
+ next
+ assume fin: "Inf (measure_set M f s) \<noteq> \<infinity>"
+ then have "measure_set M f s \<noteq> {}"
+ by (auto simp: top_extreal_def)
+ show ?thesis
+ proof (rule complete_lattice_class.Inf_greatest)
+ fix r assume "r \<in> measure_set M f s"
+ then obtain A where A: "disjoint_family A" "range A \<subseteq> sets M" "s \<subseteq> (\<Union>i. A i)"
+ and r: "r = (\<Sum>i. f (A i))" unfolding measure_set_def by auto
+ have "Inf (measure_set M f (s \<inter> x)) \<le> (\<Sum>i. f (A i \<inter> x))"
+ unfolding measure_set_def
+ proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i \<inter> x"])
+ from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)"
+ by (rule disjoint_family_on_bisimulation) auto
+ qed (insert x A, auto)
+ moreover
+ have "Inf (measure_set M f (s - x)) \<le> (\<Sum>i. f (A i - x))"
+ unfolding measure_set_def
+ proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i - x"])
+ from A(1) show "disjoint_family (\<lambda>i. A i - x)"
+ by (rule disjoint_family_on_bisimulation) auto
+ qed (insert x A, auto)
+ ultimately have "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le>
+ (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono)
+ also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))"
+ using A(2) x posf by (subst suminf_add_extreal) (auto simp: positive_def)
+ also have "\<dots> = (\<Sum>i. f (A i))"
+ using A x
+ by (subst add[THEN additiveD, symmetric])
+ (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f])
+ finally show "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le> r"
+ using r by simp
qed
+ qed
moreover
have "Inf (measure_set M f s)
\<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
@@ -805,7 +808,7 @@
countably_additive_def)
blast
-theorem (in algebra) caratheodory:
+theorem (in ring_of_sets) caratheodory:
assumes posf: "positive M f" and ca: "countably_additive M f"
shows "\<exists>\<mu> :: 'a set \<Rightarrow> extreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and>
measure_space \<lparr> space = space M, sets = sets (sigma M), measure = \<mu> \<rparr>"
--- a/src/HOL/Probability/Information.thy Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Probability/Information.thy Tue Mar 22 21:22:50 2011 +0100
@@ -1,3 +1,10 @@
+(* Title: HOL/Probability/Information.thy
+ Author: Johannes Hölzl, TU München
+ Author: Armin Heller, TU München
+*)
+
+header {*Information theory*}
+
theory Information
imports
Probability_Space
--- a/src/HOL/Probability/Lebesgue_Integration.thy Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Mar 22 21:22:50 2011 +0100
@@ -1,4 +1,7 @@
-(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
+(* Title: HOL/Probability/Lebesgue_Integration.thy
+ Author: Johannes Hölzl, TU München
+ Author: Armin Heller, TU München
+*)
header {*Lebesgue Integration*}
--- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Mar 22 21:22:50 2011 +0100
@@ -1,5 +1,10 @@
-(* Author: Robert Himmelmann, TU Muenchen *)
+(* Title: HOL/Probability/Lebesgue_Measure.thy
+ Author: Johannes Hölzl, TU München
+ Author: Robert Himmelmann, TU München
+*)
+
header {* Lebsegue measure *}
+
theory Lebesgue_Measure
imports Product_Measure
begin
--- a/src/HOL/Probability/Measure.thy Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Probability/Measure.thy Tue Mar 22 21:22:50 2011 +0100
@@ -1,4 +1,10 @@
-(* Author: Lawrence C Paulson; Armin Heller, Johannes Hoelzl, TU Muenchen *)
+(* Title: HOL/Probability/Measure.thy
+ Author: Lawrence C Paulson
+ Author: Johannes Hölzl, TU München
+ Author: Armin Heller, TU München
+*)
+
+header {* Properties about measure spaces *}
theory Measure
imports Caratheodory
@@ -18,7 +24,7 @@
lemma algebra_measure_update[simp]:
"algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> algebra M'"
- unfolding algebra_def by simp
+ unfolding algebra_iff_Un by simp
lemma sigma_algebra_measure_update[simp]:
"sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> sigma_algebra M'"
@@ -107,10 +113,7 @@
qed
lemma (in measure_space) additive: "additive M \<mu>"
-proof (rule algebra.countably_additive_additive [OF _ _ ca])
- show "algebra M" by default
- show "positive M \<mu>" by (simp add: positive_def)
-qed
+ using ca by (auto intro!: countably_additive_additive simp: positive_def)
lemma (in measure_space) measure_additive:
"a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {}
--- a/src/HOL/Probability/Probability_Space.thy Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Probability/Probability_Space.thy Tue Mar 22 21:22:50 2011 +0100
@@ -1,3 +1,10 @@
+(* Title: HOL/Probability/Probability_Space.thy
+ Author: Johannes Hölzl, TU München
+ Author: Armin Heller, TU München
+*)
+
+header {*Probability spaces*}
+
theory Probability_Space
imports Lebesgue_Integration Radon_Nikodym Product_Measure
begin
--- a/src/HOL/Probability/Product_Measure.thy Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Probability/Product_Measure.thy Tue Mar 22 21:22:50 2011 +0100
@@ -1,3 +1,9 @@
+(* Title: HOL/Probability/Product_Measure.thy
+ Author: Johannes Hölzl, TU München
+*)
+
+header {*Product measure spaces*}
+
theory Product_Measure
imports Lebesgue_Integration
begin
--- a/src/HOL/Probability/Radon_Nikodym.thy Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Mar 22 21:22:50 2011 +0100
@@ -1,3 +1,9 @@
+(* Title: HOL/Probability/Radon_Nikodym.thy
+ Author: Johannes Hölzl, TU München
+*)
+
+header {*Radon-Nikod{\'y}m derivative*}
+
theory Radon_Nikodym
imports Lebesgue_Integration
begin
--- a/src/HOL/Probability/Sigma_Algebra.thy Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Mar 22 21:22:50 2011 +0100
@@ -1,5 +1,6 @@
(* Title: HOL/Probability/Sigma_Algebra.thy
- Author: Stefan Richter, Markus Wenzel, TU Muenchen
+ Author: Stefan Richter, Markus Wenzel, TU München
+ Author: Johannes Hölzl, TU München
Plus material from the Hurd/Coble measure theory development,
translated by Lawrence Paulson.
*)
@@ -28,89 +29,111 @@
space :: "'a set"
sets :: "'a set set"
-locale algebra =
+locale subset_class =
fixes M :: "('a, 'b) algebra_scheme"
assumes space_closed: "sets M \<subseteq> Pow (space M)"
- and empty_sets [iff]: "{} \<in> sets M"
- and compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
- and Un [intro]: "!!a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
-lemma (in algebra) top [iff]: "space M \<in> sets M"
- by (metis Diff_empty compl_sets empty_sets)
-
-lemma (in algebra) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
+lemma (in subset_class) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
by (metis PowD contra_subsetD space_closed)
-lemma (in algebra) Int [intro]:
+locale ring_of_sets = subset_class +
+ assumes empty_sets [iff]: "{} \<in> sets M"
+ and Diff [intro]: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a - b \<in> sets M"
+ and Un [intro]: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
+
+lemma (in ring_of_sets) Int [intro]:
assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M"
proof -
- have "((space M - a) \<union> (space M - b)) \<in> sets M"
- by (metis a b compl_sets Un)
- moreover
- have "a \<inter> b = space M - ((space M - a) \<union> (space M - b))"
- using space_closed a b
- by blast
- ultimately show ?thesis
- by (metis compl_sets)
+ have "a \<inter> b = a - (a - b)"
+ by auto
+ then show "a \<inter> b \<in> sets M"
+ using a b by auto
qed
-lemma (in algebra) Diff [intro]:
- assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a - b \<in> sets M"
-proof -
- have "(a \<inter> (space M - b)) \<in> sets M"
- by (metis a b compl_sets Int)
- moreover
- have "a - b = (a \<inter> (space M - b))"
- by (metis Int_Diff Int_absorb1 Int_commute a sets_into_space)
- ultimately show ?thesis
- by metis
-qed
-
-lemma (in algebra) finite_union [intro]:
+lemma (in ring_of_sets) finite_Union [intro]:
"finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
by (induct set: finite) (auto simp add: Un)
-lemma (in algebra) finite_UN[intro]:
+lemma (in ring_of_sets) finite_UN[intro]:
assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
shows "(\<Union>i\<in>I. A i) \<in> sets M"
using assms by induct auto
-lemma (in algebra) finite_INT[intro]:
+lemma (in ring_of_sets) finite_INT[intro]:
assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
shows "(\<Inter>i\<in>I. A i) \<in> sets M"
using assms by (induct rule: finite_ne_induct) auto
-lemma algebra_iff_Int:
- "algebra M \<longleftrightarrow>
- sets M \<subseteq> Pow (space M) & {} \<in> sets M &
- (\<forall>a \<in> sets M. space M - a \<in> sets M) &
- (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
-proof (auto simp add: algebra.Int, auto simp add: algebra_def)
- fix a b
- assume ab: "sets M \<subseteq> Pow (space M)"
- "\<forall>a\<in>sets M. space M - a \<in> sets M"
- "\<forall>a\<in>sets M. \<forall>b\<in>sets M. a \<inter> b \<in> sets M"
- "a \<in> sets M" "b \<in> sets M"
- hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
- by blast
- also have "... \<in> sets M"
- by (metis ab)
- finally show "a \<union> b \<in> sets M" .
-qed
-
-lemma (in algebra) insert_in_sets:
+lemma (in ring_of_sets) insert_in_sets:
assumes "{x} \<in> sets M" "A \<in> sets M" shows "insert x A \<in> sets M"
proof -
have "{x} \<union> A \<in> sets M" using assms by (rule Un)
thus ?thesis by auto
qed
-lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
+lemma (in ring_of_sets) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
by (metis Int_absorb1 sets_into_space)
-lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
+lemma (in ring_of_sets) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
by (metis Int_absorb2 sets_into_space)
+locale algebra = ring_of_sets +
+ assumes top [iff]: "space M \<in> sets M"
+
+lemma (in algebra) compl_sets [intro]:
+ "a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
+ by auto
+
+lemma algebra_iff_Un:
+ "algebra M \<longleftrightarrow>
+ sets M \<subseteq> Pow (space M) &
+ {} \<in> sets M &
+ (\<forall>a \<in> sets M. space M - a \<in> sets M) &
+ (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<union> b \<in> sets M)" (is "_ \<longleftrightarrow> ?Un")
+proof
+ assume "algebra M"
+ then interpret algebra M .
+ show ?Un using sets_into_space by auto
+next
+ assume ?Un
+ show "algebra M"
+ proof
+ show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M" "space M \<in> sets M"
+ using `?Un` by auto
+ fix a b assume a: "a \<in> sets M" and b: "b \<in> sets M"
+ then show "a \<union> b \<in> sets M" using `?Un` by auto
+ have "a - b = space M - ((space M - a) \<union> b)"
+ using space a b by auto
+ then show "a - b \<in> sets M"
+ using a b `?Un` by auto
+ qed
+qed
+
+lemma algebra_iff_Int:
+ "algebra M \<longleftrightarrow>
+ sets M \<subseteq> Pow (space M) & {} \<in> sets M &
+ (\<forall>a \<in> sets M. space M - a \<in> sets M) &
+ (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)" (is "_ \<longleftrightarrow> ?Int")
+proof
+ assume "algebra M"
+ then interpret algebra M .
+ show ?Int using sets_into_space by auto
+next
+ assume ?Int
+ show "algebra M"
+ proof (unfold algebra_iff_Un, intro conjI ballI)
+ show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M"
+ using `?Int` by auto
+ from `?Int` show "\<And>a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M" by auto
+ fix a b assume sets: "a \<in> sets M" "b \<in> sets M"
+ hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
+ using space by blast
+ also have "... \<in> sets M"
+ using sets `?Int` by auto
+ finally show "a \<union> b \<in> sets M" .
+ qed
+qed
+
section {* Restricted algebras *}
abbreviation (in algebra)
@@ -174,7 +197,7 @@
lemma algebra_Pow:
"algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
- by (auto simp add: algebra_def)
+ by (auto simp add: algebra_iff_Un)
lemma sigma_algebra_Pow:
"sigma_algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
@@ -205,7 +228,7 @@
{} \<in> sets M \<and> (\<forall>s \<in> sets M. space M - s \<in> sets M) \<and>
(\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
- algebra_def Un_range_binary)
+ algebra_iff_Un Un_range_binary)
subsection {* Initial Sigma Algebra *}
@@ -513,7 +536,7 @@
thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<in> sets M` by auto
qed
-lemma (in algebra) measurable_ident[intro, simp]: "id \<in> measurable M M"
+lemma (in ring_of_sets) measurable_ident[intro, simp]: "id \<in> measurable M M"
by (auto simp add: measurable_def)
lemma measurable_comp[intro]:
@@ -666,7 +689,7 @@
lemma disjointed_subset: "disjointed A n \<subseteq> A n"
by (auto simp add: disjointed_def)
-lemma (in algebra) UNION_in_sets:
+lemma (in ring_of_sets) UNION_in_sets:
fixes A:: "nat \<Rightarrow> 'a set"
assumes A: "range A \<subseteq> sets M "
shows "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
@@ -678,7 +701,7 @@
by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
qed
-lemma (in algebra) range_disjointed_sets:
+lemma (in ring_of_sets) range_disjointed_sets:
assumes A: "range A \<subseteq> sets M "
shows "range (disjointed A) \<subseteq> sets M"
proof (auto simp add: disjointed_def)
@@ -687,6 +710,10 @@
by (metis A Diff UNIV_I image_subset_iff)
qed
+lemma (in algebra) range_disjointed_sets':
+ "range A \<subseteq> sets M \<Longrightarrow> range (disjointed A) \<subseteq> sets M"
+ using range_disjointed_sets .
+
lemma sigma_algebra_disjoint_iff:
"sigma_algebra M \<longleftrightarrow>
algebra M &
@@ -702,7 +729,7 @@
disjoint_family (disjointed A) \<longrightarrow>
(\<Union>i. disjointed A i) \<in> sets M" by blast
hence "(\<Union>i. disjointed A i) \<in> sets M"
- by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed)
+ by (simp add: algebra.range_disjointed_sets' M A disjoint_family_disjointed)
thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
qed
@@ -868,7 +895,6 @@
(\<Union>i. A i) \<in> sets M) &
(\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
-
inductive_set
smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
for M
@@ -1117,17 +1143,12 @@
section {* Dynkin systems *}
-locale dynkin_system =
- fixes M :: "('a, 'b) algebra_scheme"
- assumes space_closed: "sets M \<subseteq> Pow (space M)"
- and space: "space M \<in> sets M"
+locale dynkin_system = subset_class +
+ assumes space: "space M \<in> sets M"
and compl[intro!]: "\<And>A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
and UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
\<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
-lemma (in dynkin_system) sets_into_space: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
- using space_closed by auto
-
lemma (in dynkin_system) empty[intro, simp]: "{} \<in> sets M"
using space compl[of "space M"] by simp
@@ -1156,7 +1177,7 @@
assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
\<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
shows "dynkin_system M"
- using assms by (auto simp: dynkin_system_def)
+ using assms by (auto simp: dynkin_system_def dynkin_system_axioms_def subset_class_def)
lemma dynkin_system_trivial:
shows "dynkin_system \<lparr> space = A, sets = Pow A \<rparr>"
@@ -1184,7 +1205,7 @@
next
assume "Int_stable M"
show "sigma_algebra M"
- unfolding sigma_algebra_disjoint_iff algebra_def
+ unfolding sigma_algebra_disjoint_iff algebra_iff_Un
proof (intro conjI ballI allI impI)
show "sets M \<subseteq> Pow (space M)" using sets_into_space by auto
next
@@ -1211,13 +1232,12 @@
fix A assume "A \<in> sets (dynkin M)"
moreover
{ fix D assume "A \<in> D" and d: "dynkin_system \<lparr> space = space M, sets = D \<rparr>"
- from dynkin_system.sets_into_space[OF d] `A \<in> D`
- have "A \<subseteq> space M" by auto }
+ then have "A \<subseteq> space M" by (auto simp: dynkin_system_def subset_class_def) }
moreover have "{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D} \<noteq> {}"
using assms dynkin_system_trivial by fastsimp
ultimately show "A \<subseteq> space (dynkin M)"
unfolding dynkin_def using assms
- by simp (metis dynkin_system.sets_into_space in_mono mem_def)
+ by simp (metis dynkin_system_def subset_class_def in_mono mem_def)
next
show "space (dynkin M) \<in> sets (dynkin M)"
unfolding dynkin_def using dynkin_system.space by fastsimp
@@ -1277,7 +1297,7 @@
proof -
have "dynkin_system M" by default
then have "dynkin_system \<lparr>space = space N, sets = sets M \<rparr>"
- using assms unfolding dynkin_system_def by simp
+ using assms unfolding dynkin_system_def dynkin_system_axioms_def subset_class_def by simp
with `sets N \<subseteq> sets M` show ?thesis by (auto simp add: dynkin_def)
qed
--- a/src/HOL/Product_Type.thy Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Product_Type.thy Tue Mar 22 21:22:50 2011 +0100
@@ -261,6 +261,27 @@
in [(@{const_syntax prod_case}, split_guess_names_tr')] end
*}
+(* Force eta-contraction for terms of the form "Q A (%p. prod_case P p)"
+ where Q is some bounded quantifier or set operator.
+ Reason: the above prints as "Q p : A. case p of (x,y) \<Rightarrow> P x y"
+ whereas we want "Q (x,y):A. P x y".
+ Otherwise prevent eta-contraction.
+*)
+print_translation {*
+let
+ fun contract Q f ts =
+ case ts of
+ [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)]
+ => if loose_bvar1 (t,0) then f ts else Syntax.const Q $ A $ s
+ | _ => f ts;
+ fun contract2 (Q,f) = (Q, contract Q f);
+ val pairs =
+ [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
+ Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
+ Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
+ Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
+in map contract2 pairs end
+*}
subsubsection {* Code generator setup *}
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Mar 22 21:22:50 2011 +0100
@@ -32,8 +32,8 @@
val extract_known_failure :
(failure * string) list -> string -> failure option
val extract_tstplike_proof_and_outcome :
- bool -> bool -> int -> (string * string) list -> (failure * string) list
- -> string -> string * failure option
+ bool -> bool -> bool -> int -> (string * string) list
+ -> (failure * string) list -> string -> string * failure option
val is_same_step : step_name * step_name -> bool
val atp_proof_from_tstplike_string : bool -> string -> string proof
val map_term_names_in_atp_proof :
@@ -80,7 +80,10 @@
else
s
fun short_output verbose output =
- if verbose then elide_string 1000 output else ""
+ if verbose then
+ if output = "" then "No details available" else elide_string 1000 output
+ else
+ ""
val missing_message_tail =
" appears to be missing. You will need to install it if you want to invoke \
@@ -154,17 +157,19 @@
|> find_first (fn (_, pattern) => String.isSubstring pattern output)
|> Option.map fst
-fun extract_tstplike_proof_and_outcome verbose complete res_code proof_delims
- known_failures output =
+fun extract_tstplike_proof_and_outcome debug verbose complete res_code
+ proof_delims known_failures output =
case extract_known_failure known_failures output of
- NONE => (case extract_tstplike_proof proof_delims output of
- "" => ("", SOME (if res_code = 0 andalso output = "" then
- ProofMissing
- else
- UnknownError (short_output verbose output)))
- | tstplike_proof =>
- if res_code = 0 then (tstplike_proof, NONE)
- else ("", SOME (UnknownError (short_output verbose output))))
+ NONE =>
+ (case extract_tstplike_proof proof_delims output of
+ "" =>
+ ("", SOME (if res_code = 0 andalso (not debug orelse output = "") then
+ ProofMissing
+ else
+ UnknownError (short_output verbose output)))
+ | tstplike_proof =>
+ if res_code = 0 then (tstplike_proof, NONE)
+ else ("", SOME (UnknownError (short_output verbose output))))
| SOME failure =>
("", SOME (if failure = IncompleteUnprovable andalso complete then
Unprovable
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Nitpick/etc/settings Tue Mar 22 21:22:50 2011 +0100
@@ -0,0 +1,1 @@
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Nitpick/lib/Tools/nitrox Tue Mar 22 21:22:50 2011 +0100
@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+#
+# Author: Jasmin Blanchette
+#
+# DESCRIPTION: TPTP FOF version of Nitpick
+
+
+PRG="$(basename "$0")"
+
+function usage() {
+ echo
+ echo "Usage: isabelle $PRG FILES"
+ echo
+ echo " Runs Nitrox on a FOF or CNF TPTP problem."
+ echo
+ exit 1
+}
+
+for FILE in "$@"
+do
+ (echo "theory Nitrox_Run imports Main begin" &&
+ echo "ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *}" &&
+ echo "end;") | isabelle tty
+done
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Nitpick/nitrox.ML Tue Mar 22 21:22:50 2011 +0100
@@ -0,0 +1,210 @@
+(* Title: HOL/Tools/Nitpick/nitrox.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2010, 2011
+
+Finite model generation for TPTP first-order formulas via Nitpick.
+*)
+
+signature NITROX =
+sig
+ val pick_nits_in_fof_file : string -> string
+end;
+
+structure Nitrox : NITROX =
+struct
+
+datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+datatype quantifier = AForall | AExists
+datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
+datatype 'a formula =
+ AQuant of quantifier * 'a list * 'a formula |
+ AConn of connective * 'a formula list |
+ APred of 'a fo_term
+
+exception SYNTAX of string
+
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+
+fun takewhile _ [] = []
+ | takewhile p (x :: xs) = if p x then x :: takewhile p xs else []
+
+fun dropwhile _ [] = []
+ | dropwhile p (x :: xs) = if p x then dropwhile p xs else x :: xs
+
+fun strip_c_style_comment [] = ""
+ | strip_c_style_comment (#"*" :: #"/" :: cs) = strip_spaces_in_list cs
+ | strip_c_style_comment (_ :: cs) = strip_c_style_comment cs
+and strip_spaces_in_list [] = ""
+ | strip_spaces_in_list (#"%" :: cs) =
+ strip_spaces_in_list (dropwhile (not_equal #"\n") cs)
+ | strip_spaces_in_list (#"/" :: #"*" :: cs) = strip_c_style_comment cs
+ | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
+ | strip_spaces_in_list [c1, c2] =
+ strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
+ | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
+ if Char.isSpace c1 then
+ strip_spaces_in_list (c2 :: c3 :: cs)
+ else if Char.isSpace c2 then
+ if Char.isSpace c3 then
+ strip_spaces_in_list (c1 :: c3 :: cs)
+ else
+ str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
+ strip_spaces_in_list (c3 :: cs)
+ else
+ str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
+val strip_spaces = strip_spaces_in_list o String.explode
+
+val parse_keyword = Scan.this_string
+
+fun parse_file_path ("'" :: ss) =
+ (takewhile (not_equal "'") ss |> implode,
+ List.drop (dropwhile (not_equal "'") ss, 1))
+ | parse_file_path ("\"" :: ss) =
+ (takewhile (not_equal "\"") ss |> implode,
+ List.drop (dropwhile (not_equal "\"") ss, 1))
+ | parse_file_path _ = raise SYNTAX "invalid file path"
+
+fun parse_include x =
+ let
+ val (file_name, rest) =
+ (parse_keyword "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
+ --| $$ ".") x
+ in
+ ((), raw_explode (strip_spaces (File.read (Path.explode file_name))) @ rest)
+ end
+
+fun mk_anot phi = AConn (ANot, [phi])
+fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
+
+val parse_dollar_name =
+ Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
+
+fun parse_term x =
+ (parse_dollar_name
+ -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> ATerm) x
+and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
+
+(* Apply equal or not-equal to a term. *)
+val parse_predicate_term =
+ parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
+ >> (fn (u, NONE) => APred u
+ | (u1, SOME (NONE, u2)) => APred (ATerm ("=", [u1, u2]))
+ | (u1, SOME (SOME _, u2)) => mk_anot (APred (ATerm ("=", [u1, u2]))))
+
+fun fo_term_head (ATerm (s, _)) = s
+
+fun parse_formula x =
+ (($$ "(" |-- parse_formula --| $$ ")"
+ || ($$ "!" >> K AForall || $$ "?" >> K AExists)
+ --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_formula
+ >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
+ || $$ "~" |-- parse_formula >> mk_anot
+ || parse_predicate_term)
+ -- Scan.option ((Scan.this_string "=>" >> K AImplies
+ || Scan.this_string "<=>" >> K AIff
+ || Scan.this_string "<~>" >> K ANotIff
+ || Scan.this_string "<=" >> K AIf
+ || $$ "|" >> K AOr || $$ "&" >> K AAnd) -- parse_formula)
+ >> (fn (phi1, NONE) => phi1
+ | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
+
+val parse_fof_or_cnf =
+ (parse_keyword "fof" || parse_keyword "cnf") |-- $$ "(" |--
+ Scan.many (not_equal ",") |-- $$ "," |--
+ (parse_keyword "axiom" || parse_keyword "definition"
+ || parse_keyword "theorem" || parse_keyword "lemma"
+ || parse_keyword "hypothesis" || parse_keyword "conjecture"
+ || parse_keyword "negated_conjecture") --| $$ "," -- parse_formula
+ --| $$ ")" --| $$ "."
+ >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
+
+val parse_problem =
+ Scan.repeat parse_include
+ |-- Scan.repeat (parse_fof_or_cnf --| Scan.repeat parse_include)
+
+val parse_tptp_problem =
+ Scan.finite Symbol.stopper
+ (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
+ parse_problem))
+ o raw_explode o strip_spaces
+
+val boolT = @{typ bool}
+val iotaT = @{typ iota}
+val quantT = (iotaT --> boolT) --> boolT
+
+fun is_variable s = Char.isUpper (String.sub (s, 0))
+
+fun hol_term_from_fo_term res_T (ATerm (x, us)) =
+ let val ts = map (hol_term_from_fo_term iotaT) us in
+ list_comb ((case x of
+ "$true" => @{const_name True}
+ | "$false" => @{const_name False}
+ | "=" => @{const_name HOL.eq}
+ | _ => x, map fastype_of ts ---> res_T)
+ |> (if is_variable x then Free else Const), ts)
+ end
+
+fun hol_prop_from_formula phi =
+ case phi of
+ AQuant (_, [], phi') => hol_prop_from_formula phi'
+ | AQuant (q, x :: xs, phi') =>
+ Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
+ quantT)
+ $ lambda (Free (x, iotaT)) (hol_prop_from_formula (AQuant (q, xs, phi')))
+ | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
+ | AConn (c, [u1, u2]) =>
+ pairself hol_prop_from_formula (u1, u2)
+ |> (case c of
+ AAnd => HOLogic.mk_conj
+ | AOr => HOLogic.mk_disj
+ | AImplies => HOLogic.mk_imp
+ | AIf => HOLogic.mk_imp o swap
+ | AIff => HOLogic.mk_eq
+ | ANotIff => HOLogic.mk_not o HOLogic.mk_eq
+ | ANot => raise Fail "binary \"ANot\"")
+ | AConn _ => raise Fail "malformed AConn"
+ | APred u => hol_term_from_fo_term boolT u
+
+fun mk_all x t = Const (@{const_name All}, quantT) $ lambda x t
+
+fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
+
+fun pick_nits_in_fof_file file_name =
+ case parse_tptp_problem (File.read (Path.explode file_name)) of
+ (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
+ | (phis, []) =>
+ let
+ val ts = map (HOLogic.mk_Trueprop o close_hol_prop
+ o hol_prop_from_formula) phis
+(*
+ val _ = warning (PolyML.makestring phis)
+ val _ = app (warning o Syntax.string_of_term @{context}) ts
+*)
+ val state = Proof.init @{context}
+ val params =
+ [("card iota", "1\<midarrow>100"),
+ ("card", "1\<midarrow>8"),
+ ("box", "false"),
+ ("sat_solver", "smart"),
+ ("max_threads", "1"),
+ ("batch_size", "10"),
+ (* ("debug", "true"), *)
+ ("verbose", "true"),
+ (* ("overlord", "true"), *)
+ ("show_consts", "true"),
+ ("format", "1000"),
+ ("max_potential", "0"),
+ (* ("timeout", "240 s"), *)
+ ("expect", "genuine")]
+ |> Nitpick_Isar.default_params @{theory}
+ val auto = false
+ val i = 1
+ val n = 1
+ val step = 0
+ val subst = []
+ in
+ Nitpick.pick_nits_in_term state params auto i n step subst ts
+ @{prop False} |> fst
+ end
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Mar 22 21:22:50 2011 +0100
@@ -62,7 +62,7 @@
(concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
end
val params =
- {debug = debug, verbose = false, overlord = overlord, blocking = true,
+ {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Mar 22 20:44:47 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Mar 22 21:22:50 2011 +0100
@@ -403,8 +403,8 @@
I)
|>> (if measure_run_time then split_time else rpair NONE)
val (tstplike_proof, outcome) =
- extract_tstplike_proof_and_outcome verbose complete res_code
- proof_delims known_failures output
+ extract_tstplike_proof_and_outcome debug verbose complete
+ res_code proof_delims known_failures output
in (output, msecs, tstplike_proof, outcome) end
val run_twice =
has_incomplete_mode andalso not auto andalso
@@ -495,8 +495,6 @@
val smt_failures =
remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
-val internal_error_prefix = "Internal error: "
-
fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
| failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
| failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
@@ -506,8 +504,7 @@
string_of_int code ^ "."))
| failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
| failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
- if String.isPrefix internal_error_prefix msg then InternalError
- else UnknownError msg
+ UnknownError msg
(* FUDGE *)
val smt_max_iters = Unsynchronized.ref 8
@@ -565,7 +562,7 @@
handle exn => if Exn.is_interrupt exn then
reraise exn
else
- (internal_error_prefix ^ ML_Compiler.exn_message exn
+ (ML_Compiler.exn_message exn
|> SMT_Failure.Other_Failure |> SOME, [])
val death = Timer.checkRealTimer timer
val _ =