--- a/src/HOL/Library/Old_Recdef.thy Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Library/Old_Recdef.thy Thu Sep 04 14:02:37 2014 +0200
@@ -20,6 +20,9 @@
apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
done
+lemma tfl_cut_def: "cut f r x \<equiv> (\<lambda>y. if (y,x) \<in> r then f y else undefined)"
+ unfolding cut_def .
+
lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
apply clarify
apply (rule cut_apply, assumption)
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Sep 04 14:02:37 2014 +0200
@@ -200,7 +200,7 @@
(* case class G x = None *)
apply (simp (no_asm_simp) add: class_rec_def comp_subcls1
- wfrec [where r="(subcls1 G)^-1", simplified])
+ wfrec [where R="(subcls1 G)^-1", simplified])
apply (simp add: comp_class_None)
(* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)
--- a/src/HOL/MicroJava/J/TypeRel.thy Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Thu Sep 04 14:02:37 2014 +0200
@@ -66,14 +66,8 @@
assumes wf: "wf ((subcls1 G)^-1)"
and cls: "class G C = Some (D, fs, ms)"
shows "class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)"
-proof -
- from wf have step: "\<And>H a. wfrec ((subcls1 G)\<inverse>) H a =
- H (cut (wfrec ((subcls1 G)\<inverse>) H) ((subcls1 G)\<inverse>) a) a"
- by (rule wfrec)
- have cut: "\<And>f. C \<noteq> Object \<Longrightarrow> cut f ((subcls1 G)\<inverse>) C D = f D"
- by (rule cut_apply [where r="(subcls1 G)^-1", simplified, OF subcls1I, OF cls])
- from cls show ?thesis by (simp add: step cut class_rec_def)
-qed
+ by (subst wfrec_def_adm[OF class_rec_def])
+ (auto simp: assms adm_wf_def fun_eq_iff subcls1I split: option.split)
definition
"wf_class G = wf ((subcls1 G)^-1)"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Sep 04 14:02:37 2014 +0200
@@ -3734,64 +3734,39 @@
shows "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
-subsubsection{* Total boundedness *}
+subsubsection{* Totally bounded *}
lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
unfolding Cauchy_def by metis
-fun helper_1 :: "('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a"
-where
- "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
-declare helper_1.simps[simp del]
-
lemma seq_compact_imp_totally_bounded:
assumes "seq_compact s"
- shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))"
-proof (rule, rule, rule ccontr)
- fix e::real
- assume "e > 0"
- assume assm: "\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` k))"
- def x \<equiv> "helper_1 s e"
- {
- fix n
- have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
- proof (induct n rule: nat_less_induct)
- fix n
- def Q \<equiv> "(\<lambda>y. y \<in> s \<and> (\<forall>m<n. \<not> dist (x m) y < e))"
- assume as: "\<forall>m<n. x m \<in> s \<and> (\<forall>ma<m. \<not> dist (x ma) (x m) < e)"
- have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
- using assm
- apply simp
- apply (erule_tac x="x ` {0 ..< n}" in allE)
- using as
- apply auto
- done
+ shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
+proof -
+ { fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)"
+ let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
+ have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
+ proof (rule dependent_wellorder_choice)
+ fix n x assume "\<And>y. y < n \<Longrightarrow> ?Q x y (x y)"
+ then have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
+ using *[of "x ` {0 ..< n}"] by (auto simp: subset_eq)
then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)"
unfolding subset_eq by auto
- have "Q (x n)"
- unfolding x_def and helper_1.simps[of s e n]
- apply (rule someI2[where a=z])
- unfolding x_def[symmetric] and Q_def
- using z
- apply auto
- done
- then show "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
- unfolding Q_def by auto
- qed
- }
- then have "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)"
- by blast+
- then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially"
- using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto
- from this(3) have "Cauchy (x \<circ> r)"
- using LIMSEQ_imp_Cauchy by auto
- then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e"
- unfolding cauchy_def using `e>0` by auto
- show False
- using N[THEN spec[where x=N], THEN spec[where x="N+1"]]
- using r[unfolded subseq_def, THEN spec[where x=N], THEN spec[where x="N+1"]]
- using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]]
- by auto
+ show "\<exists>r. ?Q x n r"
+ using z by auto
+ qed simp
+ then obtain x where "\<forall>n::nat. x n \<in> s" and x:"\<And>n m. m < n \<Longrightarrow> \<not> (dist (x m) (x n) < e)"
+ by blast
+ then obtain l r where "l \<in> s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially"
+ using assms by (metis seq_compact_def)
+ from this(3) have "Cauchy (x \<circ> r)"
+ using LIMSEQ_imp_Cauchy by auto
+ then obtain N::nat where "\<And>m n. N \<le> m \<Longrightarrow> N \<le> n \<Longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e"
+ unfolding cauchy_def using `e > 0` by blast
+ then have False
+ using x[of "r N" "r (N+1)"] r by (auto simp: subseq_def) }
+ then show ?thesis
+ by metis
qed
subsubsection{* Heine-Borel theorem *}
@@ -3802,7 +3777,7 @@
shows "compact s"
proof -
from seq_compact_imp_totally_bounded[OF `seq_compact s`]
- obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` f e)"
+ obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>f e. ball x e)"
unfolding choice_iff' ..
def K \<equiv> "(\<lambda>(x, r). ball x r) ` ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)"
have "countably_compact s"
@@ -4137,7 +4112,7 @@
qed
lemma compact_eq_totally_bounded:
- "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
+ "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
(is "_ \<longleftrightarrow> ?rhs")
proof
assume assms: "?rhs"
--- a/src/HOL/Order_Relation.thy Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Order_Relation.thy Thu Sep 04 14:02:37 2014 +0200
@@ -319,27 +319,6 @@
*}
-subsubsection {* Well-founded recursion via genuine fixpoints *}
-
-lemma wfrec_fixpoint:
-fixes r :: "('a * 'a) set" and
- H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-assumes WF: "wf r" and ADM: "adm_wf r H"
-shows "wfrec r H = H (wfrec r H)"
-proof(rule ext)
- fix x
- have "wfrec r H x = H (cut (wfrec r H) r x) x"
- using wfrec[of r H] WF by simp
- also
- {have "\<And> y. (y,x) : r \<Longrightarrow> (cut (wfrec r H) r x) y = (wfrec r H) y"
- by (auto simp add: cut_apply)
- hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x"
- using ADM adm_wf_def[of r H] by auto
- }
- finally show "wfrec r H x = H (wfrec r H) x" .
-qed
-
-
subsubsection {* Characterizations of well-foundedness *}
text {* A transitive relation is well-founded iff it is ``locally'' well-founded,
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Thu Sep 04 14:02:37 2014 +0200
@@ -184,70 +184,51 @@
let ?q = "\<lambda>k n y. \<mu>G (?M (J k) (A n) y)"
- have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_lower)
- from Ex_w[OF A(1,2) this J(1-3), of 0] guess w0 .. note w0 = this
-
- let ?P =
- "\<lambda>k wk w. w \<in> space (Pi\<^sub>M (J (Suc k)) M) \<and> restrict w (J k) = wk \<and>
- (\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n w)"
- def w \<equiv> "rec_nat w0 (\<lambda>k wk. Eps (?P k wk))"
-
- { fix k have w: "w k \<in> space (Pi\<^sub>M (J k) M) \<and>
- (\<forall>n. ?a / 2 ^ (k + 1) \<le> ?q k n (w k)) \<and> (k \<noteq> 0 \<longrightarrow> restrict (w k) (J (k - 1)) = w (k - 1))"
- proof (induct k)
- case 0 with w0 show ?case
- unfolding w_def nat.rec(1) by auto
+ let ?P = "\<lambda>w k. w \<in> space (Pi\<^sub>M (J k) M) \<and> (\<forall>n. ?a / 2 ^ (Suc k) \<le> ?q k n w)"
+ have "\<exists>w. \<forall>k. ?P (w k) k \<and> restrict (w (Suc k)) (J k) = w k"
+ proof (rule dependent_nat_choice)
+ have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_lower)
+ from Ex_w[OF A(1,2) this J(1-3), of 0] show "\<exists>w. ?P w 0" by auto
+ next
+ fix w k assume Suc: "?P w k"
+ show "\<exists>w'. ?P w' (Suc k) \<and> restrict w' (J k) = w"
+ proof cases
+ assume [simp]: "J k = J (Suc k)"
+ have "?a / 2 ^ (Suc (Suc k)) \<le> ?a / 2 ^ (k + 1)"
+ using `0 < ?a` `?a \<le> 1` by (cases ?a) (auto simp: field_simps)
+ with Suc show ?thesis
+ by (auto intro!: exI[of _ w] simp: extensional_restrict space_PiM intro: order_trans)
next
- case (Suc k)
- then have wk: "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
- have "\<exists>w'. ?P k (w k) w'"
- proof cases
- assume [simp]: "J k = J (Suc k)"
- show ?thesis
- proof (intro exI[of _ "w k"] conjI allI)
- fix n
- have "?a / 2 ^ (Suc k + 1) \<le> ?a / 2 ^ (k + 1)"
- using `0 < ?a` `?a \<le> 1` by (cases ?a) (auto simp: field_simps)
- also have "\<dots> \<le> ?q k n (w k)" using Suc by auto
- finally show "?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n (w k)" by simp
- next
- show "w k \<in> space (Pi\<^sub>M (J (Suc k)) M)"
- using Suc by simp
- then show "restrict (w k) (J k) = w k"
- by (simp add: extensional_restrict space_PiM)
- qed
- next
- assume "J k \<noteq> J (Suc k)"
- with J_mono[of k "Suc k"] have "J (Suc k) - J k \<noteq> {}" (is "?D \<noteq> {}") by auto
- have "range (\<lambda>n. ?M (J k) (A n) (w k)) \<subseteq> ?G"
- "decseq (\<lambda>n. ?M (J k) (A n) (w k))"
- "\<forall>n. ?a / 2 ^ (k + 1) \<le> \<mu>G (?M (J k) (A n) (w k))"
- using `decseq A` fold(4)[OF J(1-3) A_eq(2), of "w k" k] Suc
- by (auto simp: decseq_def)
- from Ex_w[OF this `?D \<noteq> {}`] J[of "Suc k"]
- obtain w' where w': "w' \<in> space (Pi\<^sub>M ?D M)"
- "\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> \<mu>G (?M ?D (?M (J k) (A n) (w k)) w')" by auto
- let ?w = "merge (J k) ?D (w k, w')"
- have [simp]: "\<And>x. merge (J k) (I - J k) (w k, merge ?D (I - ?D) (w', x)) =
- merge (J (Suc k)) (I - (J (Suc k))) (?w, x)"
- using J(3)[of "Suc k"] J(3)[of k] J_mono[of k "Suc k"]
- by (auto intro!: ext split: split_merge)
- have *: "\<And>n. ?M ?D (?M (J k) (A n) (w k)) w' = ?M (J (Suc k)) (A n) ?w"
- using w'(1) J(3)[of "Suc k"]
- by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+
- show ?thesis
- using w' J_mono[of k "Suc k"] wk unfolding *
- by (intro exI[of _ ?w])
- (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
- qed
- then have "?P k (w k) (w (Suc k))"
- unfolding w_def nat.rec(2) unfolding w_def[symmetric]
- by (rule someI_ex)
- then show ?case by auto
+ assume "J k \<noteq> J (Suc k)"
+ with J_mono[of k "Suc k"] have "J (Suc k) - J k \<noteq> {}" (is "?D \<noteq> {}") by auto
+ have "range (\<lambda>n. ?M (J k) (A n) w) \<subseteq> ?G" "decseq (\<lambda>n. ?M (J k) (A n) w)"
+ "\<forall>n. ?a / 2 ^ (k + 1) \<le> \<mu>G (?M (J k) (A n) w)"
+ using `decseq A` fold(4)[OF J(1-3) A_eq(2), of w k] Suc
+ by (auto simp: decseq_def)
+ from Ex_w[OF this `?D \<noteq> {}`] J[of "Suc k"]
+ obtain w' where w': "w' \<in> space (Pi\<^sub>M ?D M)"
+ "\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> \<mu>G (?M ?D (?M (J k) (A n) w) w')" by auto
+ let ?w = "merge (J k) ?D (w, w')"
+ have [simp]: "\<And>x. merge (J k) (I - J k) (w, merge ?D (I - ?D) (w', x)) =
+ merge (J (Suc k)) (I - (J (Suc k))) (?w, x)"
+ using J(3)[of "Suc k"] J(3)[of k] J_mono[of k "Suc k"]
+ by (auto intro!: ext split: split_merge)
+ have *: "\<And>n. ?M ?D (?M (J k) (A n) w) w' = ?M (J (Suc k)) (A n) ?w"
+ using w'(1) J(3)[of "Suc k"]
+ by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+
+ show ?thesis
+ using Suc w' J_mono[of k "Suc k"] unfolding *
+ by (intro exI[of _ ?w])
+ (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
qed
- moreover
- from w have "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
- moreover
+ qed
+ then obtain w where w:
+ "\<And>k. w k \<in> space (Pi\<^sub>M (J k) M)"
+ "\<And>k n. ?a / 2 ^ (Suc k) \<le> ?q k n (w k)"
+ "\<And>k. restrict (w (Suc k)) (J k) = w k"
+ by metis
+
+ { fix k
from w have "?a / 2 ^ (k + 1) \<le> ?q k k (w k)" by auto
then have "?M (J k) (A k) (w k) \<noteq> {}"
using positive_mu_G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \<le> 1`
@@ -256,19 +237,15 @@
then have "merge (J k) (I - J k) (w k, x) \<in> A k" by auto
then have "\<exists>x\<in>A k. restrict x (J k) = w k"
using `w k \<in> space (Pi\<^sub>M (J k) M)`
- by (intro rev_bexI) (auto intro!: ext simp: extensional_def space_PiM)
- ultimately have "w k \<in> space (Pi\<^sub>M (J k) M)"
- "\<exists>x\<in>A k. restrict x (J k) = w k"
- "k \<noteq> 0 \<Longrightarrow> restrict (w k) (J (k - 1)) = w (k - 1)"
- by auto }
- note w = this
+ by (intro rev_bexI) (auto intro!: ext simp: extensional_def space_PiM) }
+ note w_ext = this
{ fix k l i assume "k \<le> l" "i \<in> J k"
{ fix l have "w k i = w (k + l) i"
proof (induct l)
case (Suc l)
from `i \<in> J k` J_mono[of k "k + l"] have "i \<in> J (k + l)" by auto
- with w(3)[of "k + Suc l"]
+ with w(3)[of "k + l"]
have "w (k + l) i = w (k + Suc l) i"
by (auto simp: restrict_def fun_eq_iff split: split_if_asm)
with Suc show ?case by simp
@@ -297,7 +274,8 @@
{ fix n
have "restrict w' (J n) = w n" using w(1)[of n]
by (auto simp add: fun_eq_iff space_PiM)
- with w[of n] obtain x where "x \<in> A n" "restrict x (J n) = restrict w' (J n)" by auto
+ with w_ext[of n] obtain x where "x \<in> A n" "restrict x (J n) = restrict w' (J n)"
+ by auto
then have "w' \<in> A n" unfolding A_eq using w' by (auto simp: prod_emb_def space_PiM) }
then have "w' \<in> (\<Inter>i. A i)" by auto
with `(\<Inter>i. A i) = {}` show False by auto
--- a/src/HOL/Probability/Radon_Nikodym.thy Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Thu Sep 04 14:02:37 2014 +0200
@@ -233,42 +233,34 @@
proof -
interpret N: finite_measure N by fact
let ?d = "\<lambda>A. measure M A - measure N A"
- let ?P = "\<lambda>A B n. A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
- let ?r = "\<lambda>S. restricted_space S"
- { fix S n assume S: "S \<in> sets M"
- then have "finite_measure (density M (indicator S))" "0 < 1 / real (Suc n)"
- "finite_measure (density N (indicator S))" "sets (density N (indicator S)) = sets (density M (indicator S))"
+ let ?P = "\<lambda>A n. if n = 0 then A = space M else (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
+ let ?Q = "\<lambda>A B. A \<subseteq> B \<and> ?d B \<le> ?d A"
+
+ have "\<exists>A. \<forall>n. (A n \<in> sets M \<and> ?P (A n) n) \<and> ?Q (A (Suc n)) (A n)"
+ proof (rule dependent_nat_choice)
+ show "\<exists>A. A \<in> sets M \<and> ?P A 0"
+ by auto
+ next
+ fix A n assume "A \<in> sets M \<and> ?P A n"
+ then have A: "A \<in> sets M" by auto
+ then have "finite_measure (density M (indicator A))" "0 < 1 / real (Suc (Suc n))"
+ "finite_measure (density N (indicator A))" "sets (density N (indicator A)) = sets (density M (indicator A))"
by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq)
from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this
- with S have "?P (S \<inter> X) S n"
+ with A have "A \<inter> X \<in> sets M \<and> ?P (A \<inter> X) (Suc n) \<and> ?Q (A \<inter> X) A"
by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2)
- hence "\<exists>A. ?P A S n" .. }
- note Ex_P = this
- def A \<equiv> "rec_nat (space M) (\<lambda>n A. SOME B. ?P B A n)"
- have A_Suc: "\<And>n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def)
- have A_0[simp]: "A 0 = space M" unfolding A_def by simp
- { fix i have "A i \<in> sets M" unfolding A_def
- proof (induct i)
- case (Suc i)
- from Ex_P[OF this, of i] show ?case unfolding nat.rec(2)
- by (rule someI2_ex) simp
- qed simp }
- note A_in_sets = this
- { fix n have "?P (A (Suc n)) (A n) n"
- using Ex_P[OF A_in_sets] unfolding A_Suc
- by (rule someI2_ex) simp }
- note P_A = this
- have "range A \<subseteq> sets M" using A_in_sets by auto
- have A_mono: "\<And>i. A (Suc i) \<subseteq> A i" using P_A by simp
- have mono_dA: "mono (\<lambda>i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc)
- have epsilon: "\<And>C i. \<lbrakk> C \<in> sets M; C \<subseteq> A (Suc i) \<rbrakk> \<Longrightarrow> - 1 / real (Suc i) < ?d C"
- using P_A by auto
+ then show "\<exists>B. (B \<in> sets M \<and> ?P B (Suc n)) \<and> ?Q B A"
+ by blast
+ qed
+ then obtain A where A: "\<And>n. A n \<in> sets M" "\<And>n. ?P (A n) n" "\<And>n. ?Q (A (Suc n)) (A n)"
+ by metis
+ then have mono_dA: "mono (\<lambda>i. ?d (A i))" and A_0[simp]: "A 0 = space M"
+ by (auto simp add: mono_iff_le_Suc)
show ?thesis
proof (safe intro!: bexI[of _ "\<Inter>i. A i"])
- show "(\<Inter>i. A i) \<in> sets M" using A_in_sets by auto
- have A: "decseq A" using A_mono by (auto intro!: decseq_SucI)
- from `range A \<subseteq> sets M`
- finite_Lim_measure_decseq[OF _ A] N.finite_Lim_measure_decseq[OF _ A]
+ show "(\<Inter>i. A i) \<in> sets M" using `\<And>n. A n \<in> sets M` by auto
+ have "decseq A" using A by (auto intro!: decseq_SucI)
+ from A(1) finite_Lim_measure_decseq[OF _ this] N.finite_Lim_measure_decseq[OF _ this]
have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (auto intro!: tendsto_diff simp: sets_eq)
thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
by (rule_tac LIMSEQ_le_const) auto
@@ -280,10 +272,11 @@
hence "0 < - ?d B" by auto
from ex_inverse_of_nat_Suc_less[OF this]
obtain n where *: "?d B < - 1 / real (Suc n)"
- by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
- have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.rec(2))
- from epsilon[OF B(1) this] *
- show False by auto
+ by (auto simp: real_eq_of_nat field_simps)
+ also have "\<dots> \<le> - 1 / real (Suc (Suc n))"
+ by (auto simp: field_simps)
+ finally show False
+ using * A(2)[of "Suc n"] B by (auto elim!: ballE[of _ _ B])
qed
qed
qed
--- a/src/HOL/Probability/Regularity.thy Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Probability/Regularity.thy Thu Sep 04 14:02:37 2014 +0200
@@ -163,7 +163,7 @@
by blast
then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
\<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
- apply atomize_elim unfolding bchoice_iff .
+ by metis
hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
\<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
unfolding Ball_def by blast
@@ -209,8 +209,8 @@
from nat_approx_posE[OF this] guess n . note n = this
let ?k = "from_nat_into X ` {0..k e (Suc n)}"
have "finite ?k" by simp
- moreover have "K \<subseteq> \<Union>((\<lambda>x. ball x e') ` ?k)" unfolding K_def B_def using n by force
- ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>((\<lambda>x. ball x e') ` k)" by blast
+ moreover have "K \<subseteq> (\<Union>x\<in>?k. ball x e')" unfolding K_def B_def using n by force
+ ultimately show "\<exists>k. finite k \<and> K \<subseteq> (\<Union>x\<in>k. ball x e')" by blast
qed
ultimately
show "?thesis e " by (auto simp: sU)
--- a/src/HOL/Tools/TFL/thms.ML Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Tools/TFL/thms.ML Thu Sep 04 14:02:37 2014 +0200
@@ -7,7 +7,7 @@
struct
val WFREC_COROLLARY = @{thm tfl_wfrec};
val WF_INDUCTION_THM = @{thm tfl_wf_induct};
- val CUT_DEF = @{thm cut_def};
+ val CUT_DEF = @{thm tfl_cut_def};
val eqT = @{thm tfl_eq_True};
val rev_eq_mp = @{thm tfl_rev_eq_mp};
val simp_thm = @{thm tfl_simp_thm};
--- a/src/HOL/Wfrec.thy Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Wfrec.thy Thu Sep 04 14:02:37 2014 +0200
@@ -10,86 +10,88 @@
imports Wellfounded
begin
-inductive
- wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
- for R :: "('a * 'a) set"
- and F :: "('a => 'b) => 'a => 'b"
-where
- wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
- wfrec_rel R F x (F g x)"
+inductive wfrec_rel :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" for R F where
+ wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)"
-definition
- cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
- "cut f r x == (%y. if (y,x):r then f y else undefined)"
+definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b" where
+ "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
+
+definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool" where
+ "adm_wf R F \<longleftrightarrow> (\<forall>f g x. (\<forall>z. (z, x) \<in> R \<longrightarrow> f z = g z) \<longrightarrow> F f x = F g x)"
-definition
- adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
- "adm_wf R F == ALL f g x.
- (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
+definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)" where
+ "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
-definition
- wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
- "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+lemma cuts_eq: "(cut f R x = cut g R x) \<longleftrightarrow> (\<forall>y. (y, x) \<in> R \<longrightarrow> f y = g y)"
+ by (simp add: fun_eq_iff cut_def)
-lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
-by (simp add: fun_eq_iff cut_def)
-
-lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
-by (simp add: cut_def)
+lemma cut_apply: "(x, a) \<in> R \<Longrightarrow> cut f R a x = f x"
+ by (simp add: cut_def)
text{*Inductive characterization of wfrec combinator; for details see:
John Harrison, "Inductive definitions: automation and application"*}
-lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
-apply (simp add: adm_wf_def)
-apply (erule_tac a=x in wf_induct)
-apply (rule ex1I)
-apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
-apply (fast dest!: theI')
-apply (erule wfrec_rel.cases, simp)
-apply (erule allE, erule allE, erule allE, erule mp)
-apply (blast intro: the_equality [symmetric])
-done
+lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P"
+ by (auto intro: the_equality[symmetric] theI)
-lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
-apply (simp add: adm_wf_def)
-apply (intro strip)
-apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
-apply (rule refl)
-done
+lemma wfrec_unique: assumes "adm_wf R F" "wf R" shows "\<exists>!y. wfrec_rel R F x y"
+ using `wf R`
+proof induct
+ def f \<equiv> "\<lambda>y. THE z. wfrec_rel R F y z"
+ case (less x)
+ then have "\<And>y z. (y, x) \<in> R \<Longrightarrow> wfrec_rel R F y z \<longleftrightarrow> z = f y"
+ unfolding f_def by (rule theI_unique)
+ with `adm_wf R F` show ?case
+ by (subst wfrec_rel.simps) (auto simp: adm_wf_def)
+qed
-lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
+lemma adm_lemma: "adm_wf R (\<lambda>f x. F (cut f R x) x)"
+ by (auto simp add: adm_wf_def
+ intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
+
+lemma wfrec: "wf R \<Longrightarrow> wfrec R F a = F (cut (wfrec R F) R a) a"
apply (simp add: wfrec_def)
apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
apply (rule wfrec_rel.wfrecI)
-apply (intro strip)
apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
done
text{** This form avoids giant explosions in proofs. NOTE USE OF ==*}
-lemma def_wfrec: "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a"
-apply auto
-apply (blast intro: wfrec)
-done
+lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a"
+ by (auto intro: wfrec)
+
+
+subsubsection {* Well-founded recursion via genuine fixpoints *}
+lemma wfrec_fixpoint:
+ assumes WF: "wf R" and ADM: "adm_wf R F"
+ shows "wfrec R F = F (wfrec R F)"
+proof (rule ext)
+ fix x
+ have "wfrec R F x = F (cut (wfrec R F) R x) x"
+ using wfrec[of R F] WF by simp
+ also
+ { have "\<And> y. (y,x) \<in> R \<Longrightarrow> (cut (wfrec R F) R x) y = (wfrec R F) y"
+ by (auto simp add: cut_apply)
+ hence "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
+ using ADM adm_wf_def[of R F] by auto }
+ finally show "wfrec R F x = F (wfrec R F) x" .
+qed
subsection {* Wellfoundedness of @{text same_fst} *}
-definition
- same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
-where
- "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
- --{*For @{text rec_def} declarations where the first n parameters
+definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" where
+ "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
+ --{*For @{const wfrec} declarations where the first n parameters
stay unchanged in the recursive call. *}
-lemma same_fstI [intro!]:
- "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
-by (simp add: same_fst_def)
+lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
+ by (simp add: same_fst_def)
lemma wf_same_fst:
- assumes prem: "(!!x. P x ==> wf(R x))"
- shows "wf(same_fst P R)"
+ assumes prem: "\<And>x. P x \<Longrightarrow> wf (R x)"
+ shows "wf (same_fst P R)"
apply (simp cong del: imp_cong add: wf_def same_fst_def)
apply (intro strip)
apply (rename_tac a b)
--- a/src/HOL/Zorn.thy Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Zorn.thy Thu Sep 04 14:02:37 2014 +0200
@@ -720,4 +720,36 @@
with 1 show ?thesis by auto
qed
+(* Move this to Hilbert Choice and wfrec to Wellfounded*)
+
+lemma wfrec_def_adm: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> adm_wf R F \<Longrightarrow> f = F f"
+ using wfrec_fixpoint by simp
+
+lemma dependent_wf_choice:
+ fixes P :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
+ assumes "wf R" and adm: "\<And>f g x r. (\<And>z. (z, x) \<in> R \<Longrightarrow> f z = g z) \<Longrightarrow> P f x r = P g x r"
+ assumes P: "\<And>x f. (\<And>y. (y, x) \<in> R \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
+ shows "\<exists>f. \<forall>x. P f x (f x)"
+proof (intro exI allI)
+ fix x
+ def f \<equiv> "wfrec R (\<lambda>f x. SOME r. P f x r)"
+ from `wf R` show "P f x (f x)"
+ proof (induct x)
+ fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> P f y (f y)"
+ show "P f x (f x)"
+ proof (subst (2) wfrec_def_adm[OF f_def `wf R`])
+ show "adm_wf R (\<lambda>f x. SOME r. P f x r)"
+ by (auto simp add: adm_wf_def intro!: arg_cong[where f=Eps] ext adm)
+ show "P f x (Eps (P f x))"
+ using P by (rule someI_ex) fact
+ qed
+ qed
+qed
+
+lemma (in wellorder) dependent_wellorder_choice:
+ assumes "\<And>r f g x. (\<And>y. y < x \<Longrightarrow> f y = g y) \<Longrightarrow> P f x r = P g x r"
+ assumes P: "\<And>x f. (\<And>y. y < x \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
+ shows "\<exists>f. \<forall>x. P f x (f x)"
+ using wf by (rule dependent_wf_choice) (auto intro!: assms)
+
end